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 subst dict =        (* aplică substituția dict unui termen *)
  let rec subd = function        (* folosește dict de mai sus *)
    | 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                
       
let rec occurs v = function        (* apare variabila v în termenul dat? *)
  | V s -> s = v                (* e aceeași variabilă (același nume)? *)
  | F (f, tl) -> List.exists (occurs v) tl        (* apare într-un subtermen? *)

(* unifică t1 cu t2 pornind de la substituția d, returnează noua substituție *)
let rec unif d t1 t2 = match (t1, t2) with
  | (V v, t) | (t, V v) -> let st = subst d t in  (* află substituția lui t *)
                           if (st = V v) then d          (* v = v, nu schimbă *)
                           else if occurs v st then failwith "circular substit."
                           else M.add v st d        (* adaugă noua subst. pt. v *)
  | (F (f1, tl1), F(f2, tl2)) -> if f1 = f2 then List.fold_left2 unif d tl1 tl2
                                 else failwith "not same function"

(* test: unifică f(x, g(y, f(z)), b) cu f(h(y), g(a, u), z) *)
let d = unif M.empty (F ("f", [V "x";
                               F ("g", [V "y"; F("f", [V "z"])]);
                               F ("b", [])]))
             (F ("f", [F("h", [V "y"]); F ("g", [F ("a", []); V "u"]); V "z"]))
let dl = M.bindings d
let sd = M.map (subst d) d  (* substituții complete *)
let sdl = M.bindings sd

This document was generated using caml2html