(* $Id$ *)

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


let substitute s t = 
  let rec  sub_rec t = match t with 
     (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 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 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    -> 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 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));; *)