large-star-collider/ocaml/Unification.ml

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)  

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

(* Résout une liste d'équations *)

let rec solve eq sub = 
  match eq with
  | [] -> Some sub
  | (Var(x), term)::t -> if Var(x) = term then Some (solve t sub) else Some (elim x term t sub) (* Si x = x c'est une équation inutile, on passe donc à la suite *)
  | (term, Var(x))::t -> Some (elim x term t sub) (*Inutile de vérifier si term = Var(x) ici car c'est déjà vérifié à la ligne ci-dessus*)
  | (Func(f, fs), Func(g, gs))::t -> if f = g then Some (solve ((List.combine fs gs)@t) sub) else None (*si f et g ne sont pas égaux, on ne peut pas résoudre l'équation*)

and elim id term eq sub =
  if eq = [] then Some sub
  else if occurs id term then None (* l'équation n'est pas soluble, car on aurait quelque chose de la forme x = f(x) *)
  else let sigma_xy = [(id, term)] in
  Some (solve (List.map (fun (a,b) -> (substit a sigma_xy, substit b sigma_xy)) eq) (sigma_xy@sub)) (* On substitue toutes les occurences d'id dans le système d'équation et on ajoute cette solution au système *)

  (* ========================================
      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) ;;

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

let terme3 = Func("f",[ melina ; sieg; Func("g",[Func("h",[hyetta]); adeline])]) ;;

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