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