type oType = Tvar of string | Arrow of oType * oType
;;

exception Not_Found
;;


let rec assoc x l = 
  match l with 
    | [] -> raise Not_Found
    | (h1,h2)::t   -> if x = h1 then h2 else assoc x t
;;
 

let substitute s t = 
  let rec  sub_rec t = 
    match t with 
      | (Tvar a)  -> (try assoc a s with Not_found -> t)
      | Arrow(oT1,oT2)    -> Arrow(sub_rec oT1, sub_rec oT2)
  in sub_rec t
;;

let compsubst s t = 
  (List.map (function (a,oT) -> (a,substitute s oT)) t) @ s;;

let occur v t = 
  let rec occ_rec t = 
    match t with 
      | Tvar b -> b=v
      | Arrow(oT1,oT2) -> occ_rec oT1 or occ_rec oT2
  in occ_rec t
;;

let rec unify c = 
  match c with 
    |  (Tvar a), oT -> 
          if oT=Tvar a then [] 
          else 
            if occur a oT then raise (Failure "unify")
            else [a,oT]
    | oT,Tvar a -> 
      if occur a oT then raise (Failure "unify")
      else [a,oT]
    | Arrow(oS1,oS2), Arrow(oT1,oT2) -> 
      let s=unify(oS1,oT1)  in
          compsubst   (unify(substitute s oS2,
                             substitute s oT2)) s
;;


let oT1=(Tvar "x") ;;
let oT2=(Tvar "y") ;;
let s1 = unify (oT1,oT2) ;;
substitute s1 oT1 = substitute s1 oT2 ;;

let oT3 = (Arrow (Tvar "a", Arrow (Tvar "b",Tvar "c"))) ;;
let oT4 = (Arrow (Arrow (Tvar "d",Tvar "e"), (Arrow (Tvar "f",Tvar "g")))) ;;
let s2 = unify (oT3,oT4) ;;
substitute s2 oT3 ;;
substitute s2 oT4 ;;

let oT5 = (Arrow (Arrow (Tvar "d",Tvar "a"), (Arrow (Tvar "a",Tvar "g")))) ;;
let oT6 = (Arrow (Arrow (Tvar "a",Tvar "e"), (Arrow (Tvar "a",Tvar "d")))) ;;
let s3 = unify (oT5,oT6) ;;
substitute s3 oT5 = substitute s3 oT6 ;;

(* unify (oT3,oT4);; *)
(* unify (oT3,oT5);; *)

type term= Var of string | Abs of string * term | App of term * term ;;

let string_of_int i = sprintf "%d" i ;;

let c = ref 0 ;;
let gensym s =  (c:=!c+1 ;s^(string_of_int !c)) ;;
let reset () = c := 0 ;;

let rec oTYPE oC t = 
  match t with
    |   Var x    -> assoc x oC , []
    |  Abs(x,oM) -> 
       let alpha=gensym "a" in
         let (sigma,s) = oTYPE ((x,Tvar alpha)::oC) oM in
           Arrow( (try assoc alpha s with _ ->  Tvar alpha), 
                          sigma), s
    |  App(oM,oN) -> 
       let (sigma,s)=oTYPE oC oM in
         let (tau,t) = oTYPE (List.map (function (x,phi) ->
                                (x,substitute s phi)) oC) oN   in
           let alpha=gensym "a" in 
             let u= unify(substitute t sigma, Arrow(tau,Tvar alpha))  in
               (try assoc alpha u with _ ->  Tvar alpha),
                          compsubst u (compsubst t s)
;;

let print_string s = printf "%s" s ;;
let print_newline () = printf "\n" ;;

let print_type t = 
  let rec ptype t = 
  match t with 
    | Tvar x -> print_string x
    | Arrow (x,y) -> ( print_string "("; ptype x; print_string " -> ";
                       ptype y;print_string ")" )
  in 
    ptype t;print_newline()
;;

let oA = Abs ( "x" , Abs ("y" , App (Var "x", Var "y") ));;
oTYPE [] oA;;
print_type (fst (oTYPE [] oA));;

let oS = Abs(  "x" , 
            Abs ( "y" , 
                Abs ( "z", App ( App (Var "x" , Var "z" ) , 
                                    App (Var "y",Var "z") ) )));;
print_type (fst (oTYPE [] oS));;


let delta = Abs ( "x" , App (Var "x" , Var "x" ));;

(* print_type (fst (oTYPE [] oS));; *)
(* print_type (fst (oTYPE [] delta));; *)