data Exp where
    EVar : Char -> Exp
    EInt : Int -> Exp
    EAbs : Char -> Exp -> Exp
    EApp : Exp -> Exp -> Exp
    EAdd : Exp -> Exp -> Exp

data Env where
    Env : List (Pair Char Context) -> Env

data Context where
    VInt : Int -> Context
    VClos : Env -> Char -> Exp -> Context

lookupVar : Char -> Env -> Context
lookupVar ident1 env = case env of
    Env list => case list of
        Cons a as => case a of
            Pair ident2 val => case (asciiCode ident1) == (asciiCode ident2) of
                True => val
                False => lookupVar ident1 (Env as)

insert : Char -> Context -> Env -> Env
insert ident v env = case env of
    Env list => Env (Cons (Pair ident v) list)

interp : Env -> Exp -> Context
interp env exp = case exp of
    EInt i => VInt i
    EAdd e1 e2 => case interp env e1 of
        VInt i => case interp env e2 of
            VInt j => VInt (i + j)
    EAbs ident expr => VClos env ident expr
    EApp e1 e2 => case interp env e1 of
        VClos closEnv ident exp => case interp env e2 of
            v => interp (insert ident v closEnv) exp
    EVar v => lookupVar v env

eval : Context -> Int
eval v = case v of
    VInt i => i
    _ => const (0 - 1) (printStr "Fail: final value is not an integer\n")

expression : Exp
expression = EApp (EAbs 'x' (EVar 'x')) (EApp (EAbs 'x' (EAdd (EVar 'x') (EInt 100))) (EInt 200))
-- (λ x . x) (λ x . x + 100) 200

context : Env
context = Env Nil

main : Int
main = eval (interp context expression)