open List
(* ========================================
     Definitions
   ========================================
 *)

type id = string
type term = Var of id | Func of (id * term list)

type subst = id * term list
type equation = term * term

(*
Affiche un term
*)

let print_term t =
   let rec aux t =
   match t with
   | Var id -> id
   | Func(f, tl) -> f ^ "(" ^
     let rec aux2 vl =
      match vl with
      | [] -> ""
      | h::[] -> aux h
      | h::t -> (aux h) ^ "," ^ (aux2 t) 
      in (aux2 tl) ^ ")"
   in print_string (aux t)

(*
Fonction de comparaison entre deux termes sur l'ordre lexicographique
*)

let rec compare_term t1 t2 =
   match t1, t2 with
   | Var(id1), Var(id2) -> String.compare id1 id2
   | Var(_), Func(_,_) -> -1
   | Func(_,_), Var(_) -> 1
   | Func(f, fs), Func(g, gs) -> let comp = String.compare f g in if comp > 0 then 1 
   else if comp < 0 then -1 
   else List.compare compare_term fs gs

(*
indom regarde si une variable est dans le domaine d'une substitution
*)

let rec indom t sl = 
  match t with
  | Var id -> List.exists (fun (a,_) -> a = id ) sl
  | Func(_, tl) -> List.exists (fun a -> indom a sl) tl

(*
occurs regarde si une variable apparaît dans un term
 *)

let rec occurs id t =
  match t with
  | Var i -> i = id 
  | Func(_, tl) -> List.exists (fun a -> occurs id a) tl

(*
extends_varname ajoute un suffixe à toutes les variables
*)

let rec extends_varname t ext =
  match t with
  | Var id -> Var(id ^ ext)
  | Func(f, tl) -> Func(f, List.map (fun a -> extends_varname a ext) tl)


(*
vars renvoie la liste de toutes les variables d'un term
*)

let rec vars t =
  match t with
  | Var id -> [id]
  | Func(_, tl) -> List.fold_left (fun a b -> (vars b)@a) [] tl

  (* ========================================
      Substitution
     ======================================== *)

(*
apply applique une substitution à une variable
*)

let apply id sub = let (_,s) = try List.find (fun (a,_) -> a = id ) sub with Not_found -> (id,Var(id)) in s

(*
subst applique une substitution sur un terme
 *)

let rec substit trm sub =
  match trm with
  | Var id -> apply id sub
  | Func(f,tl) -> Func(f,List.map (fun a -> substit a sub) tl)  

  (* ========================================
      Tests
     ======================================== *)

let x = Var("x")
let v = Var("v")
let z = Var("z")
let y = Var("y")

let f x y z = Func("f", [x; y; z]);;

let terme = Func("f",[x; v; Func("g",[z; y])]) ;;

let terme2 = Func("g",[z; Func("h",[x; v; y]); y]) ;;

let subd = [("x", Func("Malenia",[y])); ("y", Func("Ranni",[z]))];;


print_term terme ;;
print_term terme2 ;;

compare_term terme terme2 ;;
compare_term terme2 terme ;;
compare_term terme terme ;;

print_term (extends_varname terme "cc") ;;

occurs "x" terme ;;

vars terme ;;
apply "x" subd ;;
print_term terme ;;
print_term (substit terme subd) ;;

  (* ========================================
      Unification
     ======================================== *)

(*Résout une liste d'équations, à modifier avec option*)

let rec solve eq sub = 
  match eq with
  | [] -> sub
  | (Var(x), term)::t -> if Var(x) = term then solve t sub else elim x term t sub
  | (term, Var(x))::t -> elim x term t sub
  | (Func(f, fs), Func(g, gs))::t -> if f = g then solve ((List.combine fs gs)@t) sub else []

and elim id term eq sub =
  if eq = [] then sub
  else if occurs id term then []
  else let sigma_xy = [(id, term)] in
  solve (List.map (fun (a,b) -> (substit a sigma_xy, substit b sigma_xy)) eq) (sigma_xy@sub) 

let melina = Var("Melina")
let sieg = Var("Sieg")
let hyetta = Var("Hyetta")
let adeline = Var("Adeline")

let terme = Func("f",[x; v; Func("g",[z; y])]) ;;
let terme3 = Func("f",[ melina ; sieg; Func("g",[Func("h",[hyetta]); adeline])]) ;;

solve [(terme,terme3)] [] ;;