-- Evaluator for lambda calculus

type Id            = String
type Env           = [(Id,Value)]

data Term          = Var Id
                   | Abs Id Term
                   | App Term Term
                   | Zero
                   | Succ Term

data Value         = Num Int
                   | Fun Id Term Env

instance Eq Value where
  Num m == Num n   =  m == n
  -- equality for functions not defined, since not computable

the                :: [a] -> a
the [v]            =  v

lookUp             :: Env -> Id -> Value
lookUp e x         =  the [ v | (x',v) <- e, x == x' ]

eval               :: Term -> Env -> Value
eval (Var x) e     =  lookUp e x
eval (Abs x t) e   =  Fun x t e
eval (App s t) e   =  app (eval s e) (eval t e)
eval Zero e        =  Num 0
eval (Succ t) e    =  suc (eval t e)

app                :: Value -> Value -> Value
app (Fun x t e) v  =  eval t ((x,v):e)

suc                :: Value -> Value
suc (Num n)        =  Num (n+1)

-- k = \x -> \y -> x
k                  :: Term
k                  =  Abs "x" (Abs "y" (Var "x"))

-- m = 1
m                  :: Term
m                  =  Succ Zero

-- n = 2
n                  :: Term
n                  =  Succ m

-- t = k 1 2
t                  :: Term
t                  =  App (App k m) n

test               :: Bool
test               =  eval n [] == Num 2 && eval t [] == Num 1