module M = Map.Make(String)
                   
type term = V of string | F of string * term list

(* o substituție e un dicționar: string (variabilă) -> termen *)
                                             
let rec apare v = function        (* apare variabila v în termenul dat? *)
  | V s -> s = v                (* e aceeași variabilă (același nume)? *)
  | F (f, tl) -> List.exists (apare v) tl        (* apare într-un subtermen? *)

let subst dict =                (* aplică substituția până la capăt *)
  let rec subd = function
    | F (f, tl) -> F (f, List.map subd tl)        (* aplică la toți termenii *)
    | V v -> try subd (M.find v dict)        (* aplică recursiv la termenul găsit *)
             with Not_found -> V v        (* până variabila nu are substituție *)
  in subd                
       
(* unifică t1 cu t2 pornind de la substituția d, returnează noua substituție *)
let rec unify d t1 t2 = match (subst d t1, subst d t2) with
  | (V v, t) | (t, V v) -> if t = V v then d   (* v = v, nu schimbă *)
                           else if apare v t then failwith "subst.circulara"
                           else M.add v t d        (* adaugă noua subst. pt. v *)
  | (F (f1, tl1), F(f2, tl2)) -> if f1 = f2 then List.fold_left2 unify d tl1 tl2
                                 else failwith "functii diferite"

(*************** aici se termină algoritmul propriu-zis **************)
                               
(* test: unifică f(x, g(x, h(z)), b) cu f(h(y), g(h(b), u), z) *)
let t1 = F ("f", [V "x"; F ("g", [V "x"; F("f", [V "z"])]); F ("b", [])])
let t2 = F ("f", [F("h", [V "y"]); F ("g", [F ("h", [F("b", [])]); V "u"]); V "z"])

let d = unify M.empty t1 t2        (* substitutia unificatoare *)
let dlist = M.bindings d        (* lista pentru vizualizare *)

let ds = M.map (subst d) d          (* substituții până la capăt *)
let dslist = M.bindings ds        (* lista și pentru ele *)

let ts1 = subst d t1                (* termenii unificați *)
let ts2 = subst d t2
let test = ts1 = ts2                (* ar trebui să fie egali *)

let rec pr_term = function        (* tipărim frumos un termen *)
  | V v -> print_string v
  | F (f, tl) -> print_string f;
                 match tl with
                 | [] -> ()
                 | h :: t -> print_char '('; pr_term h;
                             List.iter (fun e -> print_char ','; pr_term e) t;
                             print_char ')'
                            
let _ = pr_term ts1; print_newline()
let _ = pr_term ts2; print_newline()
      

This document was generated using caml2html