(* une substitution est une liste de couples (identificateur,type) *)
(* fonction qui applique une substitution a un type *)
let rec apply_one_subst x s =
  let rec aos_aux = function
      VAR id as t -> begin try List.assoc id s with Not_found -> t end
    | ARR(t1,t2) -> ARR(aos_aux t1,aos_aux t2)
    | t -> t in
  aos_aux x
;;

(* calcule s1 o s2, i.e. on applique d'abord s2, puis s1 *)
let compose_subst s1 s2 =
  (* s2': s2 a laquelle on applique s1 *)
  let s2' = List.map (fun (i,x) -> (i,apply_one_subst x s1)) s2 in
  (* s1': s1 de laquelle on ote les assoc intervenant dans s2 *)
  let s1' = List.fold_right (fun (i,_) -> List.remove_assoc i) s2 s1 in
  s1'@s2'
;;

(* appliquer une substitution à un problème d'unification *)
let apply_subst_unif_pb s =
  List.map (fun (t1,t2) -> (apply_one_subst t1 s,apply_one_subst t2 s))
;;

    
exception Unif_error
;;

(* predicat vrai si l'identificateur i apparait dans une expression de type *)
let rec free_typ_var i = function
    VAR i' -> i=i'
  | ARR(t1,t2) -> (free_typ_var i t1)||(free_typ_var i t2)
  | _ -> false


(* fonction d'unification, qui renvoie une substitution *)
let rec unif s pb = match pb with
  [] -> s
| h::t -> begin
    match h with
    | VAR v,m when (not (free_typ_var v m)) ->
	let s0 = [v,m] in
	let t' = apply_subst_unif_pb s0 t in
	let s' = compose_subst s0 s in
	unif s' t'
    | VAR v,m when (not (m=VAR v)) -> raise Unif_error
    | VAR _,_ -> unif s t
    | m,VAR v -> unif s ((VAR v,m)::t) 
    | ARR(t1,t2),ARR(u1,u2) -> unif s ((t1,u1)::(t2,u2)::t)
    | INT,INT -> unif s t
    | _ -> raise Unif_error
end
;;

(* val unify : (Inf.typ * Inf.typ) list -> (Types.id * Inf.typ) list *)
let unify = unif []
;;