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


let substitute s = 
  let rec  sub_rec = function
     (Tvar a) as alpha -> (try List.assoc a s with Not_found -> alpha)
   | Arrow(oT1,oT2)      -> Arrow(sub_rec oT1, sub_rec oT2)
  in sub_rec
;;


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


let occur a = 
  let rec occ_rec = function
    Tvar b -> b=a
  | Arrow(oT1,oT2) -> occ_rec oT1 or occ_rec oT2
  in occ_rec
;;


let rec unify = function
    (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 (T3,T5);; *)



type term= Var of string 
     | Abs of string * term 
     | App of term * term;;
let gensym = 
  let c = ref 0 in 
  function s -> (c:=!c+1 ;s^(string_of_int !c));;


let rec oTYPE oC = function
   Var x    -> List.assoc x oC , []
|  Abs(x,oM) -> let alpha=gensym "a" 
               in
                 let (sigma,s) = oTYPE ((x,Tvar alpha)::oC) oM 
                 in
                   Arrow( (try List.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 List.assoc alpha u with _ ->  Tvar alpha),
                          compsubst u (compsubst t s)
;;


let print_type t = 
  let rec ptype = function 
    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 (TYPE [] delta));; *)