(* Type checker *)

type var_name = string
type type_var = string
type type_expr = Int | Bool | Fun of (type_expr * type_expr) | TV of type_var
type type_schema = TypeSchema of ((type_var list) * 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_schema) list
exception TypeError

let rec fv t =
	match t with
	  Int -> [] | Bool -> []
	| Fun (t1, t2) -> (fv t1) @ (fv t2)
	| TV a -> [a]

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 -> TypeSchema ([], Int)
	| BoolConst b -> TypeSchema ([], Bool)
	| Var x       -> lookup te x
	| Add (e1, e2) -> if ((type_of te e1) = TypeSchema ([], Int))
	                  && ((type_of te e2) = TypeSchema ([], Int))
	                  then TypeSchema ([], Int) else raise TypeError
	| Equals (e1, e2) -> if (type_of te e1) = (type_of te e2)
	                  then TypeSchema ([], 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)
*)
	| Apply _ -> raise TypeError
	| Lambda (x, ta, e) -> let TypeSchema (tvars, tr) = type_of ((x, TypeSchema ([], ta))::te) e in
	                       	TypeSchema (tvars @ (fv ta), 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
*)
	| LetRec _ -> raise TypeError