data List a where
    Nil  : List a
    Cons : a -> List a -> List a

data Pair a b where
    Pair : a -> b -> Pair a b

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

data Val where
    VInt     : Int -> Val
    VClosure : List (Pair Char Val) -> Char -> Exp -> Val

lookup : Char -> List (Pair Char Val) -> Val
lookup x cxt = case cxt of
        Cons p ps => case p of
            Pair y v => case (asciiCode x) == (asciiCode y) of
                True  => v
                False => lookup x ps

insert : Char -> Val -> List (Pair Char Val) -> List (Pair Char Val)
insert x v cxt = Cons (Pair x v) cxt

eval : List (Pair Char Val) -> Exp -> Val
eval cxt exp = case exp of
--  EVar x => case lookup x cxt of
--      VInt i             => VInt i
--      VClosure delta x e => eval delta e
    EAbs x e => VClosure cxt x e
    EApp e1 e2 => case eval cxt e1 of
        -- FIXME segmentation fault när man löser f istället för 1000
        VClosure delta x f => eval delta (EInt 1000)
--  EApp e1 e2 => case eval cxt e1 of
--      VClosure delta x f => 
--          let v = VClosure cxt x e2 in
--          eval (insert x v delta) f
    EInt i => VInt i
--  EAdd e1 e2 => 
--      let i1 = case eval cxt e1 of { VInt i => i } in 
--      let i2 = case eval cxt e2 of { VInt i => i } in 
--      VInt (i1 + i2)

exp = EApp (EAbs 'x' (EInt 40)) (EInt 20)

main : Int
main = case eval Nil exp of
           VInt i => i