UntypedLambdaCalc.hs

-- | Untyped lambda calculus 
--

import qualified Data.List as L
import Data.Char
import ParseLib.Abstract
import System.Console.Editline.Readline


-- * Lexer
--
data Token = TLambda 
           | TDot
           | TVariable String
           | TParenOpen 
           | TParenClose
           | TLet 
           | TIn 
           | TEqual
           deriving (Show, Eq)
           

ident :: Parser Char String
ident = greedy1 (satisfy isAlphaNum)


tokenDict :: [(String, Token)]
tokenDict = [("\\", TLambda), ("=", TEqual),
             (".", TDot), ("let", TLet), ("in", TIn),
             ("(", TParenOpen), 
             (")", TParenClose)]


dictParser :: [(String, a)] -> Parser Char a
dictParser = choice . map (\(c,ds) -> ds <$ token c)


lexSymbols :: Parser Char [Token] 
lexSymbols = greedy (whiteSpace *> 
                     choice [dictParser tokenDict, TVariable <$> ident] <* 
                     whiteSpace)

whiteSpace :: Parser Char [Char]
whiteSpace = greedy (satisfy isSpace)

lexer :: String -> [([Token], String)]
lexer = parse lexSymbols 


-- * Parser
--
data Term = Variable String 
          | Application Term Term
          | Lambda String Term
          deriving (Show, Eq) 


parseLambda :: Parser Token Term
parseLambda = Lambda . fromVar <$> 
                (symbol TLambda *> satisfy isVar) <*>
                (symbol TDot *> parseTerm)

fromVar :: Token -> String
fromVar (TVariable a) = a

parseVariable :: Parser Token Term
parseVariable = Variable . fromVar <$> satisfy isVar

parseApplication :: Parser Token Term
parseApplication = (makeA <$> many1 parseAp <*> parseAp)
  where parseAp = parseVariable <<|> parens parseTerm
        makeA (e1:[]) e2 = Application e1 e2
        makeA es e2 = Application (foldl1 Application es) e2


parseTerm :: Parser Token Term
parseTerm = parseLambda <<|> parseApplication <<|> parseVariable 
            <<|> parseLetExpression <<|> parens parseTerm

parseLetExpression :: Parser Token Term
parseLetExpression = let_ <$> (symbol TLet *> parseVariable <* symbol TEqual) <*>
                        parseTerm <*> (symbol TIn *> parseTerm)
  where let_ (Variable v) e1 e2 = Application (Lambda v e2) e1
                        

parens :: Parser Token a -> Parser Token a
parens p = symbol TParenOpen *> p <* symbol TParenClose


isVar :: Token -> Bool
isVar (TVariable _) = True
isVar _             = False

parser :: String -> Maybe Term
parser s = case lexer s of
            [] -> Nothing
            ((a, ""):_) -> case filter (null . snd) $ parse parseTerm a of 
                             [] -> Nothing 
                             ((a, []):_) -> Just a
                             _ -> Nothing
            _ -> Nothing



-- * Variables
--
free :: Term -> [String]
free (Variable v) = [v]
free (Application e1 e2) = L.nub (free e1 ++ free e2)
free (Lambda v e) = filter (/=v) (free e)

variables :: Term -> [String]
variables (Variable v) = [v]
variables (Application e1 e2) = L.nub(variables e1 ++ variables e2)
variables (Lambda v e) = variables e

binders :: Term -> [String]
binders (Variable v) = []
binders (Application e1 e2) = L.nub(binders e1 ++ binders e2)
binders (Lambda v e) = [v] ++ binders e


-- * Reductions
--
normal :: Term -> Term
normal v@(Variable _) = v
normal l@(Lambda v e) = l
normal a@(Application e1 e2) = if new == a then new else normal new
  where new = (betaReduce (normal e1) (normal e2))

betaReduce :: Term -> Term -> Term
betaReduce (Lambda v e1) e2 = substitute e1 v e2
betaReduce v@(Variable _) e2 = Application v e2
betaReduce a@(Application e1 e2) e3 = Application a e3

substitute :: Term -> String -> Term -> Term 
substitute e1 v e2 = if not . null $ isect
                       then substitute (alphaReduce e1 (makeVars isect (binders e1))) v e2 
                       else replace e1 v e2
  where isect = filter (/=v) $ L.intersect (binders e1) (L.nub(binders e2 ++ free e2))

replace :: Term -> String -> Term -> Term
replace (Variable var) v e = if var == v then e else Variable var 
replace (Lambda var e1) v e2 = Lambda var (replace e1 v e2)
replace (Application e1 e2) v e3 = Application (replace e1 v e3) (replace e2 v e3)

alphaReduce :: Term -> [(String, String)] -> Term 
alphaReduce (Variable v) vs = case lookup v vs of 
                                Nothing -> Variable v
                                Just n -> Variable n
alphaReduce (Application e1 e2) vs = Application (alphaReduce e1 vs)
                                                 (alphaReduce e2 vs)
alphaReduce (Lambda v e1) vs = case lookup v vs of 
                                 Nothing -> Lambda v (alphaReduce e1 vs)
                                 Just n -> Lambda n (alphaReduce e1 vs)                      


makeVars :: [String] -> [String] -> [(String, String)]
makeVars replace no = make (map makeS replace)
  where make rs = zip replace (map makeValid rs)
        makeS r = case takeWhile isDigit (reverse r) of 
                    [] -> (r, 1)
                    cs -> (reverse (drop (length cs) (reverse r)), read . reverse $ cs)
        makeValid (r, n) = if all (/=(r ++ show n)) no 
                            then r ++ show n
                            else makeValid (r, n+1)


-- * Read, Eval, Print Loop
--
printTerm :: Term -> String
printTerm (Variable v) = v
printTerm (Application e1 e2) = unwords ["(" ++ printTerm e1, printTerm e2 ++ ")"]
printTerm (Lambda v e) = "(\\" ++ v ++ " . " ++ printTerm e ++ ")"

repl :: IO ()
repl = do line <- readline "> "
          case line of 
            Nothing -> return ()
            Just line -> addHistory line >> putStrLn (maybe "Not a valid lambda expression" 
                      (printTerm . normal) $ parser (prelude ++ line)) >> repl

main = do putStrLn "Untyped lambda calculus - v1.0"
          repl


-- * Prelude
--
prelude = unlines ["let 0 = \\f . \\x . x in ",
                   "let 1 = \\f . \\x . f x in ",
                   "let 2 = \\f . \\x . f (f x) in ",
                   "let 3 = \\f . \\x . f (f (f x)) in ",
                   "let 4 = \\f . \\x . f (f (f (f x))) in ",
                   "let succ = \\n . \\f . \\x . n f x in ",
                   "let pred = \\n . \\f . \\x . n (\\g . \\h . h (g f)) (\\u . x) (\\u . u) in ",
                   "let plus = \\m . \\n . \\f . \\x . m f (n f x) in ", 
                   "let sub = \\m . \\n . n pred m in ", -- BUG? sub 3 2
                   "let mult = \\m . \\n . \\f . m (n f) in ",
                   "let true = \\x . \\y . x in ",
                   "let false = \\x . \\y . y in ",
                   "let and = \\p . \\q . p q p in ", 
                   "let or = \\p . \\q . p p q in ", 
                   "let not = \\p . \\x . \\y . p y x in ",
                   "let if = \\p . \\a . \\b . p a b in "]