(**TD06**)
open T
open Type

exception Error of string

type eqs = (Type.t * Type.t) list
type subst = (int * Type.t) list

(***********************)
(* Quelques afficheurs *)
(***********************)

open  Printf

let print_eq chan (t1,t2) =
  fprintf chan "%a = %a" Type.print t1 Type.print t2

let print_eqs chan eqs =
  List.iter
    (fun eq -> fprintf chan "%a\n" print_eq eq)
    eqs ;
  flush chan

let print_subst chan s =
  print_eqs chan
    (List.map (fun (n,t) -> Tvar n,t) s) ;
  flush chan


(***************************************)
(* Algorithme d'unification de Robison *)
(***************************************)

(* occur_check, comme le nom l'indique *)
let rec occur_check n t = match t with
| Nat -> ()
| Arrow (t1,t2) -> occur_check n t1 ; occur_check n t2
| Tvar m -> if n=m then raise (Error "Occur")

(** Appliquer une substitution à une variable *)
let subst s x = try List.assoc x s with Not_found -> Tvar x

(** 'subst_type s t' applique la substitution 's' au type 't' *)
let rec subst_type s t = match t with
  | Nat -> Nat
  | Tvar x -> subst s x
  | Arrow (t1, t2) ->
      Arrow (subst_type s t1, subst_type s t2)

(** Appliquer une substitution à un ensemble d'équations *)
let rec subst_eqs s eqs =
  List.map (fun (t1,t2) -> subst_type s t1, subst_type s t2) eqs

(** Et à une substitution *)
let rec subst_subst s0 s1 =
  List.map (fun (x,t) -> x, subst_type s0 t) s1


(*****************************************)
(* Algorithme de Robinson proprement dit *)
(*****************************************)

(*
   Les arguments de unif :
  - eqs est la liste des équations non-examinées.
  - r est la liste des équations examinées (sous forme de substitution)
*)
let rec unif eqs r = match eqs with
| [] -> r
| (t1,t2)::eqs -> unif_rec t1 t2 eqs r

(* Traiter l'équation t1=t2, il reste eqs à examiner,
   r sont déjà examinées *)
and unif_rec t1 t2 eqs r = match t1,t2 with
(* Chouette or-pat *)
| (Nat,Arrow (_,_))|(Arrow (_,_),Nat) -> raise (Error "Nat against A->B")
| Arrow (t1,t2),Arrow (t3,t4) ->
    unif_rec t1 t3 ((t2,t4)::eqs) r
| Nat,Nat -> unif eqs r
(* Noter la garde 'when' *)
| Tvar n, Tvar m when n=m -> unif eqs r
(* Encore un or-pat, encore plus chouette *)
| (Tvar n,t)|(t,Tvar n) ->
    occur_check n t ;
    (* Tout est là : bien prendre garde de remplacer n par t PARTOUT *)
    unif (subst_eqs [n,t] eqs) ((n,t)::subst_subst [n,t] r)

(* 'verbose' est 'true' si on a donné l'option "-v" sur la ligne de commande *)
let verbose = List.mem "-v" (Array.to_list Sys.argv)

let mgu eqs =
  if verbose then begin
    prerr_endline "*** EQS ***" ;
    print_eqs stderr eqs
  end ;
  let s = unif eqs [] in
  if verbose then begin
    prerr_endline "*** SUBST ***" ;
    print_subst stderr s ; flush stderr
  end ;
  s

(* Un truc simple pour avoir des variables « fraîches » *)
let fresh_var =
  let c = ref 0 in
  fun () -> let r = !c in incr c ; r

let mgu_incr t1 t2 s =
  if verbose then begin
    prerr_endline "*** EQ ***" ;
    print_eq stderr (t1,t2) ;
    eprintf "\n + SUBST\n" ;
    print_subst stderr s ;
    flush stderr
  end ;
  let s = unif_rec (subst_type s t1) (subst_type s t2) [] s in
  if verbose then begin
    prerr_endline "*** RESULT ***" ;
    print_subst stderr s ;
    prerr_endline "** END **"
  end ;
  s

(**END**)