(* Expressions de type *)
#open "divers";;

exception TypeCirculaire;;
exception Unification;;

(* Types sommes *)
type TypeInter =
  TIProd    of TypeInter*TypeInter
| TIFleche  of TypeInter*TypeInter
| TISomme   of TypeSomme*(TypeInter vect)
| TIVar     of int

and TypeConstr == TypeInter option
and TypeSomme  = {TSid:string; TSvars:int; TSconstrs:TypeConstr vect}
;;



type TypeExpr =
  Type_alpha of mutable TypeAlpha
| Type_fonct of TypeExpr*TypeExpr
| Type_prod  of TypeExpr*TypeExpr
| Type_ref   of TypeExpr
| Type_liste of TypeExpr
| Type_base  of TypeBase
| Type_somme of TypeSomme*(TypeExpr vect)
and TypeBase = Base_Bool | Base_Int | Base_Car | Base_Chaine | Base_Unit
and TypeAlpha  = AlphaLibre of int | AlphaLien of TypeExpr | AlphaUniv;;

let base_bool = Type_base Base_Bool
and base_int  = Type_base Base_Int
and base_car  = Type_base Base_Car
and base_chaine=Type_base Base_Chaine
and base_unit = Type_base Base_Unit;;

let types_base = 
["int",base_int; "bool",base_bool; 
"char", base_car; "string", base_chaine;
"unit", base_unit];;

type Construct = 
| CCst of int*TypeExpr
| CBloc of int*TypeExpr*TypeExpr;;




let niveau_courant = ref 0;;

let fraiche_alpha () = Type_alpha (AlphaLibre !niveau_courant);;
let fraiche_alpha_univ () = Type_alpha AlphaUniv;;


let rec alpha_repr = function
  Type_alpha (AlphaLien t as lien)->
     let pere=alpha_repr t in
     lien <- AlphaLien pere;
     pere
| t -> t;;

let rec abaisse_niveau t = match alpha_repr t with
  Type_alpha ((AlphaLibre niveau) as alpha) -> if niveau > !niveau_courant then alpha<-AlphaLibre !niveau_courant
| Type_fonct (a,b) -> abaisse_niveau a; abaisse_niveau b
| Type_prod  (a,b) -> abaisse_niveau a; abaisse_niveau b
| Type_liste a     -> abaisse_niveau a
| Type_ref   a     -> abaisse_niveau a
| Type_somme (_,p) -> do_vect abaisse_niveau p
| _ -> ();;

let rec generalise t = match alpha_repr t with
  Type_alpha ((AlphaLibre niveau) as alpha) -> if niveau > !niveau_courant then alpha<-AlphaUniv
| Type_fonct (a,b) -> generalise a; generalise b
| Type_prod  (a,b) -> generalise a; generalise b
| Type_liste a     -> generalise a
| Type_ref a       -> generalise a
| Type_somme (_,p) -> do_vect generalise p
| _ -> ();;


let dico_instanc = ref [];;
let rec aux_instancier t = let t = alpha_repr t in match t with
  Type_alpha (AlphaUniv as alpha) ->
     (
        try strict_assoc t !dico_instanc with
        Not_found ->
            let nouvelle=fraiche_alpha () in
            dico_instanc:=(t,nouvelle)::!dico_instanc;
            nouvelle
     )
| Type_fonct (a,b) ->
        let aa=aux_instancier a and bb=aux_instancier b in
        if a=aa && b=bb then t else Type_fonct (aa,bb)
| Type_prod  (a,b) ->
        let aa=aux_instancier a and bb=aux_instancier b in
        if a=aa && b=bb then t else Type_prod (aa,bb)
| Type_liste a ->
        let aa=aux_instancier a in
        if a=aa then t else Type_liste aa
| Type_ref a ->
        let aa=aux_instancier a in
        if a=aa then t else Type_ref aa
| Type_somme (ts,p) ->
        let pp=map_vect aux_instancier p in
        Type_somme (ts,pp)
| _ -> t
;;

let instancier t = let r=aux_instancier t in dico_instanc:=[]; r;;
let instancier2 t1 t2 = 
  let r=(aux_instancier t1, aux_instancier t2) in 
  dico_instanc:=[];
  r;;


(* est-ce que t1 (qui est du type Type_alpha) apparait dans t2 ? *)
let rec occur t1 niv t2 =
 let rec aux t2 = let t2=alpha_repr t2 in if t1==t2 then true else match t2 with
  Type_fonct (a,b) -> aux a || aux b
| Type_prod  (a,b) -> aux a || aux b
| Type_liste a     -> aux a
| Type_alpha n     -> if n>niv then n<-niv; false
| Type_ref   a     -> aux a
| Type_somme (ts,p)-> exists_vect aux  p
| _ -> false
in aux t2;;


let dico=ref [];;
let afficher_typeexpr t =
let rec aux t = let t=alpha_repr t in match t with
  Type_alpha alpha ->
     let nom=
     (
        try strict_assoc t !dico
        with Not_found ->
         let nom="#"^(string_of_int (list_length !dico)) in
         dico:=(t,nom)::(!dico); nom;
     ) in
     (
        match alpha with
          AlphaLibre n -> pr nom ;(* pr ":"; print_int n*)
        | AlphaLien l  -> pr nom; pr "=>";  aux l
        | AlphaUniv    -> pr nom; pr "!";
     )
 
| Type_fonct (a,b) ->
        pr "("; aux a; pr " -> "; aux b; pr ")"
| Type_prod (a,b) ->
        pr "("; aux a; pr " * "; aux b; pr ")"
| Type_liste a ->
        aux a; pr " list";
| Type_ref a -> aux a; pr " ref"
| Type_somme (s,p) -> pr "["; do_list_sep aux (fun x->pr ",") (list_of_vect p); pr "] "; pr s.TSid
| Type_base b -> begin
  match b with
  Base_Bool -> pr "bool"
| Base_Int -> pr "int"
| Base_Unit -> pr "unit"
| Base_Car -> pr "char"
| Base_Chaine -> pr "string"
  end
in aux t;;

let rec unifier t1 t2 =
(* pr "unifier:"; afficher_typeexpr t1; pr " et: "; afficher_typeexpr t2; pr "\n"; *)
let t1=alpha_repr t1 and t2=alpha_repr t2 in
  if (t1==t2) then () else
match (t1,t2) with
  (Type_alpha ((AlphaLibre n) as l1), Type_alpha ((AlphaLibre p) as l2)) ->
        if n>p then l1 <- AlphaLien t2 else l2 <- AlphaLien t1
| (Type_alpha l1,_) -> if occur t1 l1 t2 then raise TypeCirculaire else l1 <- AlphaLien t2
| (_,Type_alpha l2) -> if occur t2 l2 t1 then raise TypeCirculaire else l2 <- AlphaLien t1
| (Type_fonct (a1,b1), Type_fonct (a2,b2)) -> unifier a1 a2; unifier b1 b2
| (Type_prod (a1,b1), Type_prod (a2,b2)) -> unifier a1 a2; unifier b1 b2
| (Type_liste a1, Type_liste a2) -> unifier a1 a2
| (Type_base b1, Type_base b2) when b1=b2 -> ()
| (Type_ref a1, Type_ref a2) -> unifier a1 a2
| (Type_somme (ts1,p1), Type_somme (ts2,p2)) -> if ts1 != ts2 then raise Unification
     else (do_vect2 unifier p1 p2)
| _ -> raise Unification;;