(* Unify *) (* Implementation of Hantao Zhang's linear Robinson unification algorithm *) (* $Id: unify.ml,v 1.1 2003/01/12 15:33:00 berke Exp $ *) (* By Berke Durak (April 2001) *) module type SIGMA_TERMS = sig type t (* type of terms *) type s (* type of function and variable names *) val root_symbol : t -> s val arity : s -> int val kth_children : int -> t -> t val is_variable : s -> bool val size : t -> int (* total number of symbols in term *) val dummy : s val construct : s -> t list -> t end module Homogeneous_terms = struct type t = Variable of string | Function of string * t list type s = Variable_name of string | Function_name of string * int let root_symbol = function Variable(v) -> Variable_name(v) | Function(f,l) -> Function_name(f,List.length l) let construct f l = match f with Variable_name(v) -> Variable(v) | Function_name(f,m) -> if m = List.length l then Function(f,l) else raise (Invalid_argument "arity mismatch") let arity = function Variable_name(_) -> raise (Invalid_argument "arity applied to variable name") | Function_name(_,m) -> m let kth_children k = function Variable(_) -> raise (Invalid_argument "kth children applied to variable") | Function(_,l) -> List.nth l k let is_variable = function Variable_name(_) -> true | Function_name(_,_) -> false let rec size = function Variable(_) -> 1 | Function(f,l) -> List.fold_left (fun s t' -> s + size t') 1 l let dummy = Variable_name("dummy") exception Local_parse_failure exception Parse_failure of int let term_of_string s = let i = ref 0 in try let m = String.length s in let peek () = if !i = m then raise Local_parse_failure else s.[!i] and skip () = if !i < m then incr i and at_eof () = !i = m in let scan c = if peek () = c then skip () else raise Local_parse_failure and get () = let c = peek () in skip (); c in let rec parseT () = let c = get () in match c with 'A'..'Z' -> Variable((String.make 1 c)^(parseI ())) | 'a'..'z' -> let f = (String.make 1 c)^(parseI ()) in Function(f, if !i < m && peek () = '(' then begin skip (); let h = parseS () in scan ')'; h end else []) | _ -> raise Local_parse_failure and parseS () = match peek () with ')' -> [] | _ -> let t = parseT () in t::(parseS' ()) and parseS' () = match peek () with ')' -> [] | ',' -> skip (); parseS () | _ -> raise Local_parse_failure and parseI () = if at_eof () then "" else let c = peek () in match c with 'a'..'z'|'A'..'Z'|'0'..'9' -> skip (); (String.make 1 c)^(parseI ()) | _ -> "" and parseX () = let t = parseT () in if !i < m then raise Local_parse_failure else t in parseX () with Local_parse_failure -> raise (Parse_failure !i) let rec string_of_term = function Variable(x) -> x | Function(s,[]) -> s | Function(s,tl) -> (List.fold_left (fun a t -> (if a = "" then s^"(" else a^",") ^(string_of_term t)) "" tl)^")" end module Zhang_linear_unifier(S:SIGMA_TERMS) = struct type nut = { label : S.s; mutable flag : bool; mutable shells : shell list; } and shell = nut ref module VM = Map.Make(struct type t = S.s let compare = compare end) let dummy_shell = ref { label = S.dummy; flag = false; shells = [] } let rec term_of_shell v = if S.is_variable !v.label then S.construct !v.label [] else S.construct !v.label (List.map term_of_shell !v.shells) let graph_of_terms t1 t2 = let m = (S.size t1) + (S.size t2) in let a = Array.make m dummy_shell in let k = ref 0 in let v = ref VM.empty in let rec f t = let x = S.root_symbol t in if S.is_variable x then try VM.find x !v with Not_found -> begin let n = { label = x; flag = false; shells = [] } in let r = ref n in v := VM.add x r !v; r end else ref { label = x; flag = false; shells = begin let m = S.arity x in let rec loop k l = if k = m then l else loop (k + 1) ((f (S.kth_children (m - 1 - k) t))::l) in loop 0 [] end } in let u1 = f t1 and u2 = f t2 in (!v,u1,u2) exception Post_occur_check of shell exception Occur_check of shell exception Clash_failure of shell * shell let append_shells v1 v2 = !v1.shells <- v2::!v1.shells; !v2.shells <- v1::!v2.shells let rec distribute_nut v1 v2 = let n1 = !v1 in v1 := !v2; List.iter (fun v3 -> if not (!v3 == !v2) then distribute_nut v3 v2) n1.shells; n1.shells <- [] (* small error in Hantao Zhang's paper *) let replace_nut v1 v2 = v1 := !v2 let rec almost_unifiable v1 v2 = if not (!v1 == !v2) then begin match (S.is_variable (!v1).label, S.is_variable (!v2).label) with (true,true) -> append_shells v1 v2 | (true,false) -> distribute_nut v1 v2 | (false,true) -> distribute_nut v2 v1 | (false,false) -> if !v1.label <> !v2.label then raise (Clash_failure(v1,v2)) else begin List.iter2 (fun s1 s2 -> if not (!s1 == !s2) then begin if !s1.flag then raise (Occur_check(s1)); if !s2.flag then raise (Occur_check(s2)); !s1.flag <- true; !s2.flag <- true; almost_unifiable s1 s2; !s1.flag <- false; !s2.flag <- false end) !v1.shells !v2.shells; replace_nut v1 v2 end end let rec post_occur_check v1 v2 = let rec loop v = if not (S.is_variable (!v).label) then if (!v).flag then raise (Post_occur_check(v)) else begin (!v).flag <- true; List.iter loop (!v).shells; (!v).flag <- false; end in loop v1; loop v2 let linear_unify t1 t2 = let (v,v1,v2) = graph_of_terms t1 t2 in almost_unifiable v1 v2; post_occur_check v1 v2; let l = ref [] in VM.iter (fun x v -> if not (!v.flag) then begin l := (S.construct x [],(term_of_shell v))::!l; !v.flag <- true; List.iter (fun w -> if not (!w.flag) then begin !w.flag <- true; l := (S.construct !w.label [], (S.construct x []))::!l end) !v.shells; end) v; (!l, term_of_shell v1) end module H = Homogeneous_terms module Z = Zhang_linear_unifier(Homogeneous_terms) type main_options = { opt_mgu : bool ref; opt_print : bool ref; opt_count : bool ref; opt_quiet : bool ref; } let main_options = { opt_mgu = ref false; opt_print = ref false; opt_count = ref false; opt_quiet = ref false; } let main_argspec = let o = main_options in ["-mgu", Arg.Set(o.opt_mgu), "Print most general unifier (beware that the unifier can have size exponential in the initial terms)."; "-print", Arg.Set(o.opt_print), "Print unified term (beware that the unified term can be exponentially longer than the original terms)."; "-info", Arg.Unit(fun () -> print_string ("Terms are written as f(a,X,g(X,a,Y1,Y2)) with function symbols\n"^ "starting with lower-case letters and variables starting with\n"^ "upper-case letters.\n"); exit 0), "Display help information."; "-quiet", Arg.Set(o.opt_quiet), "Don't say whether terms are unifiable or not."] let _ = let o = main_options in let t = ref [] in let process x = t := x::!t in Arg.parse main_argspec process (Printf.sprintf "Usage: %s [options] term1 term2\nUse -info for more information.\n" Sys.argv.(0)); match !t with [s1;s2] -> begin let p w x = try H.term_of_string x with H.Parse_failure i -> Printf.eprintf "Parse error at character %d in %s term.\n" i w; exit 2 in let t1 = p "first" s1 and t2 = p "second" s2 in let h x = Printf.printf "Unification failed because of %s.\n" x; in try let (u,t) = Z.linear_unify t1 t2 in if not !(o.opt_quiet) then Printf.printf "Terms are unifiable.\n"; if !(o.opt_print) then Printf.printf "%s\n" (H.string_of_term t); if !(o.opt_mgu) then List.iter (fun (x,y) -> Printf.printf "%s -> %s\n" (H.string_of_term x) (H.string_of_term y)) (List.rev u) with Z.Occur_check(_) -> h "an occurence failure" | Z.Clash_failure(_) -> h "a clash" | Z.Post_occur_check(_) -> h "a post-occurence failure" end | _ -> Printf.eprintf "Two terms needed, no more, no less.\n"; exit 3