module M = Map.Make(String)

type term = Const of string | Var of string | Fun of string * term list

let find m =            (* finds term t in map m *)
  let rec findm = function
    | Const s as t -> t
    | Fun (f, tl) -> Fun (f, List.map findm tl)
    | Var s as t -> try findm (M.find s m) with Not_found -> t
  in findm

let subst v t m =       (* maps varname v to term t in m *)
  let rec occurcheck = function (* checks for recursive terms *)
    | Fun (_, tl) -> List.iter occurcheck tl
    | Var v1 when v1 = v -> failwith "not unifiable"
    | _ -> ()
  in occurcheck t; M.add v t m

let rec unify m t1 t2 = match (find m t1, find m t2) with (* returns unifier *)
  | (Fun (f1, a1), Fun (f2, a2)) when f1 = f2 -> List.fold_left2 unify m a1 a2
  | (s1, s2) when s1 = s2 -> m
  | (Var v, t) | (t, Var v) -> subst v t m
  | _ -> failwith "not unifiable"

This document was generated using caml2html