type Id = String

data Exp = Var Id | App Exp Exp | Type | Abs Id Exp | Pi Id Exp Exp | Let Id Exp Exp Exp

data Val = VGen Int | VApp Val Val | VType | VClos Env Exp 

type Env = [(Id,Val)]

update :: Env -> Id -> Val -> Env
update env x u = (x,u):env

lookUp :: Id -> Env -> Val
lookUp x ((y,u):env) =
 if x == y then u
 else lookUp x env
lookUp x [] = error"lookUp"

-- the whnf algorithm

app :: Val -> Val -> Val
eval :: Env -> Exp -> Val

app (VClos env (Abs x e)) u = eval (update env x u) e
app v u = VApp v u

eval env e = case e of
 Var x -> lookUp x env
 App e1 e2 -> app (eval env e1) (eval env e2)
 Let x e1 _ e3 -> eval (update env x (eval env e1)) e3
 Type -> VType
 _ -> VClos env e

-- the conversion algorithm; the integer is
-- used to represent the introduction of a fresh variable

eqVal :: (Int,Val,Val) -> Bool
eqVal (k,u1,u2) =
 case (u1,u2) of
   (VType,VType) -> True
   (VApp t1 w1,VApp t2 w2) -> eqVal (k,t1,t2) && eqVal (k,w1,w2)
   (VGen k1,VGen k2) -> k1 == k2
   (VClos env1 (Abs x1 e1),VClos env2 (Abs x2 e2)) ->
      let v = VGen k 
      in eqVal (k+1,eval (update env1 x1 v) e1,eval (update env2 x2 v) e2)
   (VClos env1 (Pi x1 a1 b1),VClos env2 (Pi x2 a2 b2)) ->
      let v = VGen k 
      in eqVal (k,eval env1 a1,eval env2 a2) &&
         eqVal (k+1,eval (update env1 x1 v) b1,eval (update env2 x2 v) b2)
   _ -> False

-- type-checking and type inference

checkExp :: (Int,Env,Env) -> Exp -> Val -> Bool
inferExp :: (Int,Env,Env) -> Exp -> Val

checkExp (k,rho,gamma) e v =
 case (e,v) of
   (Abs x n,VClos env (Pi y a b)) -> 
        let v = VGen k
        in checkExp (k+1,update rho x v,update gamma x (eval env a))
                    n (eval (update env y v) b)
   (Pi x a b,VType) ->
        checkExp (k,rho,gamma) a VType &&
        checkExp (k+1,update rho x (VGen k),update gamma x (eval rho a))
                        b VType
   _ -> eqVal (k,inferExp (k,rho,gamma) e,v)

inferExp (k,rho,gamma) e =
 case e of
   Var id -> lookUp id gamma
   App e1 e2 ->
      case (inferExp (k,rho,gamma) e1) of
        VClos env (Pi x a b) ->
          if checkExp (k,rho,gamma) e2 (eval env a)
               then eval (update env x (eval rho e2)) b
          else error"application error"
        _ -> error"application, expected Pi"
   Type -> VType
   _ -> error"cannot infer type"