summaryrefslogtreecommitdiff
path: root/contrib/jprover/jtunify.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/jprover/jtunify.ml')
-rw-r--r--contrib/jprover/jtunify.ml507
1 files changed, 507 insertions, 0 deletions
diff --git a/contrib/jprover/jtunify.ml b/contrib/jprover/jtunify.ml
new file mode 100644
index 00000000..2295e62c
--- /dev/null
+++ b/contrib/jprover/jtunify.ml
@@ -0,0 +1,507 @@
+(*
+ * Unification procedures for JProver. See jall.mli for more
+ * information on JProver.
+ *
+ * ----------------------------------------------------------------
+ *
+ * This file is part of MetaPRL, a modular, higher order
+ * logical framework that provides a logical programming
+ * environment for OCaml and other languages.
+ *
+ * See the file doc/index.html for information on Nuprl,
+ * OCaml, and more information about this system.
+ *
+ * Copyright (C) 2000 Stephan Schmitt
+ *
+ * This program is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software
+ * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+ *
+ * Author: Stephan Schmitt <schmitts@spmail.slu.edu>
+ * Modified by: Aleksey Nogin <nogin@cs.cornell.edu>
+ *)
+
+exception Not_unifiable
+exception Failed
+
+let jprover_bug = Invalid_argument "Jprover bug (Jtunify module)"
+
+(* ************ T-STRING UNIFICATION *********************************)
+
+
+(* ******* printing ********** *)
+
+let rec list_to_string s =
+ match s with
+ [] -> ""
+ | f::r ->
+ f^"."^(list_to_string r)
+
+let rec print_eqlist eqlist =
+ match eqlist with
+ [] ->
+ print_endline ""
+ | (atnames,f)::r ->
+ let (s,t) = f in
+ let ls = list_to_string s
+ and lt = list_to_string t in
+ begin
+ print_endline ("Atom names: "^(list_to_string atnames));
+ print_endline (ls^" = "^lt);
+ print_eqlist r
+ end
+
+let print_equations eqlist =
+ begin
+ Format.open_box 0;
+ Format.force_newline ();
+ print_endline "Equations:";
+ print_eqlist eqlist;
+ Format.force_newline ();
+ end
+
+let rec print_subst sigma =
+ match sigma with
+ [] ->
+ print_endline ""
+ | f::r ->
+ let (v,s) = f in
+ let ls = list_to_string s in
+ begin
+ print_endline (v^" = "^ls);
+ print_subst r
+ end
+
+let print_tunify sigma =
+ let (n,subst) = sigma in
+ begin
+ print_endline " ";
+ print_endline ("MaxVar = "^(string_of_int (n-1)));
+ print_endline " ";
+ print_endline "Substitution:";
+ print_subst subst;
+ print_endline " "
+ end
+
+ (*****************************************************)
+
+let is_const name =
+ (String.get name 0) = 'c'
+
+let is_var name =
+ (String.get name 0) = 'v'
+
+let r_1 s ft rt =
+ (s = []) && (ft = []) && (rt = [])
+
+let r_2 s ft rt =
+ (s = []) && (ft = []) && (List.length rt >= 1)
+
+let r_3 s ft rt =
+ ft=[] && (List.length s >= 1) && (List.length rt >= 1) && (List.hd s = List.hd rt)
+
+let r_4 s ft rt =
+ ft=[]
+ && (List.length s >= 1)
+ && (List.length rt >= 1)
+ && is_const (List.hd s)
+ && is_var (List.hd rt)
+
+let r_5 s ft rt =
+ rt=[]
+ && (List.length s >= 1)
+ && is_var (List.hd s)
+
+let r_6 s ft rt =
+ ft=[]
+ && (List.length s >= 1)
+ && (List.length rt >= 1)
+ && is_var (List.hd s)
+ && is_const (List.hd rt)
+
+let r_7 s ft rt =
+ List.length s >= 1
+ && (List.length rt >= 2)
+ && is_var (List.hd s)
+ && is_const (List.hd rt)
+ && is_const (List.hd (List.tl rt))
+
+let r_8 s ft rt =
+ ft=[]
+ && List.length s >= 2
+ && List.length rt >= 1
+ && let v = List.hd s
+ and v1 = List.hd rt in
+ (is_var v) & (is_var v1) & (v <> v1)
+
+let r_9 s ft rt =
+ (List.length s >= 2) && (List.length ft >= 1) && (List.length rt >= 1)
+ && let v = (List.hd s)
+ and v1 = (List.hd rt) in
+ (is_var v) & (is_var v1) & (v <> v1)
+
+let r_10 s ft rt =
+ (List.length s >= 1) && (List.length rt >= 1)
+ && let v = List.hd s
+ and x = List.hd rt in
+ (is_var v) && (v <> x)
+ && (((List.tl s) =[]) or (is_const x) or ((List.tl rt) <> []))
+
+let rec com_subst slist ((ov,ovlist) as one_subst) =
+ match slist with
+ [] -> raise jprover_bug
+ | f::r ->
+ if f = ov then
+ (ovlist @ r)
+ else
+ f::(com_subst r one_subst)
+
+let rec combine subst ((ov,oslist) as one_subst) =
+ match subst with
+ [] -> []
+ | ((v, slist) as f) :: r ->
+ let rest_combine = (combine r one_subst) in
+ if (List.mem ov slist) then (* subst assumed to be idemponent *)
+ let com_element = com_subst slist one_subst in
+ ((v,com_element)::rest_combine)
+ else
+ (f::rest_combine)
+
+let compose ((n,subst) as sigma) ((ov,oslist) as one_subst) =
+ let com = combine subst one_subst in
+(* begin
+ print_endline "!!!!!!!!!test print!!!!!!!!!!";
+ print_subst [one_subst];
+ print_subst subst;
+ print_endline "!!!!!!!!! END test print!!!!!!!!!!";
+*)
+ if List.mem one_subst subst then
+ (n,com)
+ else
+(* ov may multiply as variable in subst with DIFFERENT values *)
+(* in order to avoid explicit atom instances!!! *)
+ (n,(com @ [one_subst]))
+(* end *)
+
+let rec apply_element fs ft (v,slist) =
+ match (fs,ft) with
+ ([],[]) ->
+ ([],[])
+ | ([],(ft_first::ft_rest)) ->
+ let new_ft_first =
+ if ft_first = v then
+ slist
+ else
+ [ft_first]
+ in
+ let (emptylist,new_ft_rest) = apply_element [] ft_rest (v,slist) in
+ (emptylist,(new_ft_first @ new_ft_rest))
+ | ((fs_first::fs_rest),[]) ->
+ let new_fs_first =
+ if fs_first = v then
+ slist
+ else
+ [fs_first]
+ in
+ let (new_fs_rest,emptylist) = apply_element fs_rest [] (v,slist) in
+ ((new_fs_first @ new_fs_rest),emptylist)
+ | ((fs_first::fs_rest),(ft_first::ft_rest)) ->
+ let new_fs_first =
+ if fs_first = v then
+ slist
+ else
+ [fs_first]
+ and new_ft_first =
+ if ft_first = v then
+ slist
+ else
+ [ft_first]
+ in
+ let (new_fs_rest,new_ft_rest) = apply_element fs_rest ft_rest (v,slist) in
+ ((new_fs_first @ new_fs_rest),(new_ft_first @ new_ft_rest))
+
+let rec shorten us ut =
+ match (us,ut) with
+ ([],_) | (_,[]) -> (us,ut) (*raise jprover_bug*)
+ | ((fs::rs),(ft::rt)) ->
+ if fs = ft then
+ shorten rs rt
+ else
+ (us,ut)
+
+let rec apply_subst_list eq_rest (v,slist) =
+ match eq_rest with
+ [] ->
+ (true,[])
+ | (atomnames,(fs,ft))::r ->
+ let (n_fs,n_ft) = apply_element fs ft (v,slist) in
+ let (new_fs,new_ft) = shorten n_fs n_ft in (* delete equal first elements *)
+ match (new_fs,new_ft) with
+ [],[] ->
+ let (bool,new_eq_rest) = apply_subst_list r (v,slist) in
+ (bool,((atomnames,([],[]))::new_eq_rest))
+ | [],(fft::rft) ->
+ if (is_const fft) then
+ (false,[])
+ else
+ let (bool,new_eq_rest) = apply_subst_list r (v,slist) in
+ (bool,((atomnames,([],new_ft))::new_eq_rest))
+ | (ffs::rfs),[] ->
+ if (is_const ffs) then
+ (false,[])
+ else
+ let (bool,new_eq_rest) = apply_subst_list r (v,slist) in
+ (bool,((atomnames,(new_fs,[]))::new_eq_rest))
+ | (ffs::rfs),(fft::rft) ->
+ if (is_const ffs) & (is_const fft) then
+ (false,[])
+ (* different first constants cause local fail *)
+ else
+ (* at least one of firsts is a variable *)
+ let (bool,new_eq_rest) = apply_subst_list r (v,slist) in
+ (bool,((atomnames,(new_fs,new_ft))::new_eq_rest))
+
+let apply_subst eq_rest (v,slist) atomnames =
+ if (List.mem v atomnames) then (* don't apply subst to atom variables !! *)
+ (true,eq_rest)
+ else
+ apply_subst_list eq_rest (v,slist)
+
+
+(* let all_variable_check eqlist = false needs some discussion with Jens! -- NOT done *)
+
+(*
+ let rec all_variable_check eqlist =
+ match eqlist with
+ [] -> true
+ | ((_,(fs,ft))::rest_eq) ->
+ if (fs <> []) & (ft <> []) then
+ let fs_first = List.hd fs
+ and ft_first = List.hd ft
+ in
+ if (is_const fs_first) or (is_const ft_first) then
+ false
+ else
+ all_variable_check rest_eq
+ else
+ false
+*)
+
+let rec tunify_list eqlist init_sigma =
+ let rec tunify atomnames fs ft rt rest_eq sigma =
+ let apply_r1 fs ft rt rest_eq sigma =
+ (* print_endline "r1"; *)
+ tunify_list rest_eq sigma
+
+ in
+ let apply_r2 fs ft rt rest_eq sigma =
+ (* print_endline "r2"; *)
+ tunify atomnames rt fs ft rest_eq sigma
+
+ in
+ let apply_r3 fs ft rt rest_eq sigma =
+ (* print_endline "r3"; *)
+ let rfs = (List.tl fs)
+ and rft = (List.tl rt) in
+ tunify atomnames rfs ft rft rest_eq sigma
+
+ in
+ let apply_r4 fs ft rt rest_eq sigma =
+ (* print_endline "r4"; *)
+ tunify atomnames rt ft fs rest_eq sigma
+
+ in
+ let apply_r5 fs ft rt rest_eq sigma =
+ (* print_endline "r5"; *)
+ let v = (List.hd fs) in
+ let new_sigma = compose sigma (v,ft) in
+ let (bool,new_rest_eq) = apply_subst rest_eq (v,ft) atomnames in
+ if (bool=false) then
+ raise Not_unifiable
+ else
+ tunify atomnames (List.tl fs) rt rt new_rest_eq new_sigma
+
+ in
+ let apply_r6 fs ft rt rest_eq sigma =
+ (* print_endline "r6"; *)
+ let v = (List.hd fs) in
+ let new_sigma = (compose sigma (v,[])) in
+ let (bool,new_rest_eq) = apply_subst rest_eq (v,[]) atomnames in
+ if (bool=false) then
+ raise Not_unifiable
+ else
+ tunify atomnames (List.tl fs) ft rt new_rest_eq new_sigma
+
+ in
+ let apply_r7 fs ft rt rest_eq sigma =
+ (* print_endline "r7"; *)
+ let v = (List.hd fs)
+ and c1 = (List.hd rt)
+ and c2t =(List.tl rt) in
+ let new_sigma = (compose sigma (v,(ft @ [c1]))) in
+ let (bool,new_rest_eq) = apply_subst rest_eq (v,(ft @ [c1])) atomnames in
+ if bool=false then
+ raise Not_unifiable
+ else
+ tunify atomnames (List.tl fs) [] c2t new_rest_eq new_sigma
+ in
+ let apply_r8 fs ft rt rest_eq sigma =
+ (* print_endline "r8"; *)
+ tunify atomnames rt [(List.hd fs)] (List.tl fs) rest_eq sigma
+
+ in
+ let apply_r9 fs ft rt rest_eq sigma =
+ (* print_endline "r9"; *)
+ let v = (List.hd fs)
+ and (max,subst) = sigma in
+ let v_new = ("vnew"^(string_of_int max)) in
+ let new_sigma = (compose ((max+1),subst) (v,(ft @ [v_new]))) in
+ let (bool,new_rest_eq) = apply_subst rest_eq (v,(ft @ [v_new])) atomnames in
+ if (bool=false) then
+ raise Not_unifiable
+ else
+ tunify atomnames rt [v_new] (List.tl fs) new_rest_eq new_sigma
+
+ in
+ let apply_r10 fs ft rt rest_eq sigma =
+ (* print_endline "r10"; *)
+ let x = List.hd rt in
+ tunify atomnames fs (ft @ [x]) (List.tl rt) rest_eq sigma
+
+ in
+ if r_1 fs ft rt then
+ apply_r1 fs ft rt rest_eq sigma
+ else if r_2 fs ft rt then
+ apply_r2 fs ft rt rest_eq sigma
+ else if r_3 fs ft rt then
+ apply_r3 fs ft rt rest_eq sigma
+ else if r_4 fs ft rt then
+ apply_r4 fs ft rt rest_eq sigma
+ else if r_5 fs ft rt then
+ apply_r5 fs ft rt rest_eq sigma
+ else if r_6 fs ft rt then
+ (try
+ apply_r6 fs ft rt rest_eq sigma
+ with Not_unifiable ->
+ if r_7 fs ft rt then (* r7 applicable if r6 was and tr6 = C2t' *)
+ (try
+ apply_r7 fs ft rt rest_eq sigma
+ with Not_unifiable ->
+ apply_r10 fs ft rt rest_eq sigma (* r10 always applicable if r6 was *)
+ )
+ else
+ (* r10 could be represented only once if we would try it before r7.*)
+ (* but looking at the transformation rules, r10 should be tried at last in any case *)
+ apply_r10 fs ft rt rest_eq sigma (* r10 always applicable r6 was *)
+ )
+ else if r_7 fs ft rt then (* not r6 and r7 possible if z <> [] *)
+ (try
+ apply_r7 fs ft rt rest_eq sigma
+ with Not_unifiable ->
+ apply_r10 fs ft rt rest_eq sigma (* r10 always applicable if r7 was *)
+ )
+ else if r_8 fs ft rt then
+ (try
+ apply_r8 fs ft rt rest_eq sigma
+ with Not_unifiable ->
+ if r_10 fs ft rt then (* r10 applicable if r8 was and tr8 <> [] *)
+ apply_r10 fs ft rt rest_eq sigma
+ else
+ raise Not_unifiable (* simply back propagation *)
+ )
+ else if r_9 fs ft rt then
+ (try
+ apply_r9 fs ft rt rest_eq sigma
+ with Not_unifiable ->
+ if r_10 fs ft rt then (* r10 applicable if r9 was and tr9 <> [] *)
+ apply_r10 fs ft rt rest_eq sigma
+ else
+ raise Not_unifiable (* simply back propagation *)
+ )
+ else if r_10 fs ft rt then (* not ri, i<10, and r10 possible if for instance *)
+ (* (s=[] and x=v1) or (z<>[] and xt=C1V1t') *)
+ apply_r10 fs ft rt rest_eq sigma
+ else (* NO rule applicable *)
+ raise Not_unifiable
+ in
+ match eqlist with
+ [] ->
+ init_sigma
+ | f::rest_eq ->
+ let (atomnames,(fs,ft)) = f in
+ tunify atomnames fs [] ft rest_eq init_sigma
+
+let rec test_apply_eq atomnames eqs eqt subst =
+ match subst with
+ [] -> (eqs,eqt)
+ | (f,flist)::r ->
+ let (first_appl_eqs,first_appl_eqt) =
+ if List.mem f atomnames then
+ (eqs,eqt)
+ else
+ (apply_element eqs eqt (f,flist))
+ in
+ test_apply_eq atomnames first_appl_eqs first_appl_eqt r
+
+let rec test_apply_eqsubst eqlist subst =
+ match eqlist with
+ [] -> []
+ | f::r ->
+ let (atomnames,(eqs,eqt)) = f in
+ let applied_element = test_apply_eq atomnames eqs eqt subst in
+ (atomnames,applied_element)::(test_apply_eqsubst r subst)
+
+let ttest us ut ns nt eqlist orderingQ atom_rel =
+ let (short_us,short_ut) = shorten us ut in (* apply intial rule R3 *)
+ (* to eliminate common beginning *)
+ let new_element = ([ns;nt],(short_us,short_ut)) in
+ let full_eqlist =
+ if List.mem new_element eqlist then
+ eqlist
+ else
+ new_element::eqlist
+ in
+ let sigma = tunify_list full_eqlist (1,[]) in
+ let (n,subst) = sigma in
+ let test_apply = test_apply_eqsubst full_eqlist subst in
+ begin
+ print_endline "";
+ print_endline "Final equations:";
+ print_equations full_eqlist;
+ print_endline "";
+ print_endline "Final substitution:";
+ print_tunify sigma;
+ print_endline "";
+ print_endline "Applied equations:";
+ print_equations test_apply
+ end
+
+let do_stringunify us ut ns nt equations =
+ let (short_us,short_ut) = shorten us ut in (* apply intial rule R3 to eliminate common beginning *)
+ let new_element = ([ns;nt],(short_us,short_ut)) in
+ let full_eqlist =
+ if List.mem new_element equations then
+ equations
+ else
+ new_element::equations
+ in
+(* print_equations full_eqlist; *)
+ (try
+ let new_sigma = tunify_list full_eqlist (1,[]) in
+ (new_sigma,(1,full_eqlist))
+ with Not_unifiable ->
+ raise Failed (* new connection please *)
+ )
+
+
+(* type of one unifier: int * (string * string) list *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 02:59:56 +0000