(* Type checker *)

type var_name = string
type type_expr = Int | Bool | Fun of (type_expr * type_expr)
type expr = IntConst  of int
          | BoolConst of bool
          | Var       of var_name
          | Add       of (expr * expr)
          | Equals    of (expr * expr)
          | Apply     of (expr * expr)
          | Lambda    of (var_name * type_expr * expr)
          | LetRec    of (var_name * type_expr * expr * expr)
type type_env = (string * type_expr) list
exception TypeError

let rec lookup te x =
	match te with
	  [] -> raise TypeError
	| (y, t)::te2 -> if (x = y) then t else lookup te2 x

let rec type_of te e =
	match e with
	  IntConst  i -> Int
	| BoolConst b -> Bool
	| Var x       -> lookup te x
	| Add (e1, e2) -> if ((type_of te e1) = Int) && ((type_of te e2) = Int)
	                  then Int else raise TypeError
	| Equals (e1, e2) -> if (type_of te e1) = (type_of te e2)
	                  then Bool else raise TypeError
	| Apply (e1, e2) -> let t1 = type_of te e1
	                    and t2 = type_of te e2 in
	                    	(match t1 with
	                    	  Fun (ta, tr) ->
	                    		if ta = t2 then tr
	                    		else raise TypeError
	                    	| _ -> raise TypeError)
	| Lambda (x, ta, e) -> let tr = type_of ((x, ta)::te) e in Fun (ta, tr)
	| LetRec (x, t, e1, e2) -> if (type_of ((x, t)::te) e1) = t then
	                           	type_of ((x, t)::te) e2
	                           else raise TypeError