An intuitionistic first-order theorem prover -- JProver.

See the "README" file for more information.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2563 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 507 insertions, 0 deletions

diff --git a/contrib/jprover/jtunify.ml b/contrib/jprover/jtunify.ml
new file mode 100644
index 000000000..6a173e86d
--- /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
+      ([],_) | (_,[])  -> 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  *)