Simple Lambda calculus evaluator in Idris

lamcalc1.idr

-- evaluation using environments

mutual
    data Lc = Ident String
            | Lambda String Lc
            | Call Lc Lc
            | Closure Env String Lc

    data Env = Empty | Entry String Lc Env


stringify : Lc -> String
stringify (Ident x) = x
stringify (Lambda x y) = "(lambda (" ++ x ++ ") " ++ (stringify y) ++ ")"
stringify (Call x y) = "(" ++ (stringify x) ++ " "++ (stringify y) ++ ")"
stringify (Closure x y z) = "<CLOSURE>"


eval : Lc -> Env -> Lc
eval (Ident i) Empty = Ident i
eval (Ident i) (Entry e v next) = if i == e then v
                                            else eval (Ident i) next
eval (Lambda p b) env = Closure env p b
eval x@(Call f a) env = case eval f env of
                             (Closure cls p b) => eval b (Entry p (eval a env) cls)
                             _ => x
eval x _ = x

lamcalc2.idr

-- evaluation using substitution

mutual
    data Lc = Ident String
            | Lambda String Lc
            | Call Lc Lc

    data Env = Empty | Entry String Lc Env


stringify : Lc -> String
stringify (Ident x) = x
stringify (Lambda x y) = "(lambda (" ++ x ++ ") " ++ (stringify y) ++ ")"
stringify (Call x y) = "(" ++ (stringify x) ++ " "++ (stringify y) ++ ")"


substitute : String -> Lc -> Lc -> Lc
substitute x v (Ident y) = if x == y then v
                                     else (Ident y)
substitute x v (Lambda p b) = if x == p then (Lambda p b)
                                        else (Lambda p (substitute x v b))
substitute x v (Call f a) = (Call (substitute x v f) (substitute x v a))


eval : Lc -> Lc
eval (Call (Ident x) a) = Call (Ident x) (eval a)
eval (Call (Lambda p b) a) = eval (substitute p a b)
eval (Call f a) = eval (Call (eval f) (eval a))
eval x = x