HaskellLambda

import Data.List

prelude = map (\(a,b) -> (a,parse b))
             [("if", "\\f.\\x.\\y.f x y"),
              ("true", "\\x.\\y.x"),
              ("false", "\\x.\\y.y"),
              ("and", "\\a.\\b.a b false"),
              ("or", "\\a.\\b.a true b"),
              ("not", "\\a.a false true"),
              ("fst", "\\p.p true"),
              ("snd", "\\p.p false"),
              ("pair", "\\x.\\y.\\f.f x y"),
              ("nil", "pair true true"),
              ("isnil", "fst"),
              ("cons", "\\h.\\t.pair false (pair h t)"),
              ("head", "\\z.fst (snd z)"),
              ("tail", "\\z.snd (snd z)"),
              ("zero", "\\f.\\x.x"),
              ("succ", "\\n.\\f.\\x.f (n f x)"),
              ("plus", "\\n.\\m.\\f.\\x.n f (m f x)"),
              ("fix", "\\f.(\\x.f (x x)) (\\x.f (x x))")]

main = main' prelude

main' ctx = do
            line <- getLine
            let declFlag = ('=' `elem` line)
            let (ctx', line') = let (ident, rest) = biteId line
                                    term = tail $ tail rest in
                                if declFlag
                                then (updateCtx ctx ident (parse term), term)
                                else (ctx, line)
            putStrLn $ "=> " ++ (show $ (if declFlag then id else eval ctx') $ parse line')
            main' ctx'

data Lexp = Var String
          | App Lexp Lexp
          | Lambda String Lexp
          deriving Eq

instance Show Lexp where
  show (Var x) = x
  show (App l1 (l@(App l2 l3))) = show l1 ++ " (" ++ (show l) ++ ")"
  show (App l1 l2) = show l1 ++ " " ++ (show l2)
  show (Lambda x l) = "(" ++ "λ" ++ args ++ "." ++ (show body) ++ ")"
                      where (vars, body) = unlambda (Lambda x l)
                            args = concat $ intersperse " " vars

type Context = [(String, Lexp)]

updateCtx :: Context -> String -> Lexp -> Context
updateCtx xs s l = (s,l) : xs

getFromCtx :: Context -> String -> Lexp
getFromCtx [] s = error $ s ++ " not found in context"
getFromCtx (x:xs) s = if (fst x == s) then snd x else getFromCtx xs s

alphanumeric :: Char -> Bool
alphanumeric c = c `elem` ['a'..'z'] || c `elem` ['0'..'9']

biteId :: String -> (String, String)
biteId s = if (null $ fst res) then error "Identifier expected" else res
           where res = break (\c -> not $ alphanumeric c) s

biteBrackets :: String -> (String, String)
biteBrackets ('(' : s) = helper [] s 1
                         where helper acc rest 0 = (reverse $ tail acc, rest)
                               helper acc ('(' : r) n = helper ('(' : acc) r (n+1)
                               helper acc (')' : r) n = helper (')' : acc) r (n-1)
                               helper acc (c : r) n = helper (c : acc) r n
                               helper acc [] _ = error "Brackets mismatch"

bite :: String -> (String, String)
bite ('(' : s) = biteBrackets ('(' : s)
bite s = biteId s

cut :: String -> [String]
cut [] = []
cut s = bit : (cut $ dropWhile (== ' ') rest)
        where (bit, rest) = bite s

parse :: String -> Lexp
parse [] = error "Empty query"
parse (' ' : s) = parse s
parse ('\\' : s) = if (null rest || (head rest /= '.'))
                   then error "Point after lambda expected"
                   else Lambda ident (parse $ tail rest)
                   where (ident, rest) = biteId s

parse s = if (null(tail $ cut s) && head s /= '(')
          then Var $ fst $ biteId s
          else apply $ map parse (cut s)
          where apply (l : []) = l
                apply (f : x : ls) = apply $ App f x : ls

remove :: Eq a => a -> [a] -> [a]
remove _ [] = []
remove x (y:ys) = if (x == y) then remove x ys else y : (remove x ys)

freevars :: Lexp -> [String]
freevars (Var x) = [x]
freevars (App l1 l2) = freevars l1 ++ (freevars l2)
freevars (Lambda x l) = remove x (freevars l)

substitute :: Lexp -> String -> Lexp -> Lexp
substitute (Var x) y l = if (x == y) then l else (Var x)
substitute (App l1 l2) x l = App (substitute l1 x l) (substitute l2 x l)
substitute (Lambda x l1) y l2 = if (x == y)
                                then (Lambda x l1)
                                else if (x `elem` (freevars l2))
                                     then Lambda x' $ substitute (substitute l1 x (Var x')) y l2
                                     else Lambda x $ substitute l1 y l2
                                where x' = x ++ "'"

reduce :: Lexp -> Lexp
reduce (Var x) = Var x
reduce (App (Lambda x l1) l2) = substitute l1 x l2
reduce (App l1 l2) = App (reduce l1) (reduce l2)
reduce (Lambda x l) = Lambda x (reduce l)

beta :: Lexp -> Lexp
beta l = if (normal l) then l else (beta $ reduce l)

normal :: Lexp -> Bool
normal (Var _) = True
normal (App (Lambda _ _) _) = False
normal (App f x) = normal f && (normal x)
normal (Lambda _ fx) = normal fx

eval :: Context -> Lexp -> Lexp
eval ctx l = if (null fv)
             then beta l
             else eval ctx $ foldl (\e v -> substitute e v (getFromCtx ctx v)) l (nub fv)
             where fv = freevars l

unlambda :: Lexp -> ([String], Lexp)
unlambda (Lambda x l) = (x : vars, rest)
                        where (vars, rest) = unlambda l
unlambda l = ([], l)