summaryrefslogtreecommitdiff
path: root/contrib/jprover
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/jprover')
-rw-r--r--contrib/jprover/README76
-rw-r--r--contrib/jprover/jall.ml4701
-rw-r--r--contrib/jprover/jall.mli339
-rw-r--r--contrib/jprover/jlogic.ml106
-rw-r--r--contrib/jprover/jlogic.mli40
-rw-r--r--contrib/jprover/jprover.ml4565
-rw-r--r--contrib/jprover/jterm.ml872
-rw-r--r--contrib/jprover/jterm.mli110
-rw-r--r--contrib/jprover/jtunify.ml507
-rw-r--r--contrib/jprover/jtunify.mli35
-rw-r--r--contrib/jprover/opname.ml90
-rw-r--r--contrib/jprover/opname.mli15
12 files changed, 7456 insertions, 0 deletions
diff --git a/contrib/jprover/README b/contrib/jprover/README
new file mode 100644
index 00000000..ec654a03
--- /dev/null
+++ b/contrib/jprover/README
@@ -0,0 +1,76 @@
+An intuitionistic first-order theorem prover -- JProver.
+
+Usage:
+
+Require JProver.
+Jp [num].
+
+Whem [num] is provided, proof is done automatically with
+the multiplicity limit [num], otherwise no limit is forced
+and JProver may not terminate.
+
+Example:
+
+Require JProver.
+Coq < Goal (P:Prop) P->P.
+1 subgoal
+
+============================
+ (P:Prop)P->P
+
+Unnamed_thm < Jp 1.
+Proof is built.
+Subtree proved!
+-----------------------------------------
+
+Description:
+JProver is a theorem prover for first-order intuitionistic logic.
+It is originally implemented by Stephan Schmitt and then integrated into
+MetaPRL by Aleksey Nogin (see jall.ml). After this, Huang extracted the
+necessary ML-codes from MetaPRL and then integrated it into Coq.
+The MetaPRL URL is http://metaprl.org/. For more information on
+integrating JProver into interactive proof assistants, please refer to
+
+ "Stephan Schmitt, Lori Lorigo, Christoph Kreitz, and Aleksey Nogin,
+ Jprover: Integrating connection-based theorem proving into interactive
+ proof assistants. In International Joint Conference on Automated
+ Reasoning, volume 2083 of Lecture Notes in Artificial Intelligence,
+ pages 421-426. Springer-Verlag, 2001" -
+ http://www.cs.cornell.edu/nogin/papers/jprover.html
+
+
+Structure of this directory:
+This directory contains
+
+ README ------ this file
+ jall.ml ------ the main module of JProver
+ jtunify.ml ------ string unification procedures for jall.ml
+ jlogic.ml ------ interface module of jall.ml
+ jterm.ml
+ opname.ml ------ implement the infrastructure for jall.ml
+ jprover.ml4 ------ the interface of jall.ml to Coq
+ JProver.v ------ declaration for Coq
+ Makefile ------ the makefile
+ go ------ batch file to load JProver to Coq dynamically
+
+
+Comments:
+1. The original <jall.ml> is located in meta-prl/refiner/reflib of the
+MetaPRL directory. Some parts of this file are modified by Huang.
+
+2. <jtunify.ml> is also located in meta-prl/refiner/reflib with no modification.
+
+3. <jlogic.ml> is modified from meta-prl/refiner/reflib/jlogic_sig.mlz.
+
+4. <jterm.ml> and <opname.ml> are modified from the standard term module
+of MetaPRL in meta-prl/refiner/term_std.
+
+5. The Jp tactic currently cannot prove formula such as
+ ((x:nat) (P x)) -> (EX y:nat| (P y)), which requires extra constants
+in the domain when the left-All rule is applied.
+
+
+
+by Huang Guan-Shieng (Guan-Shieng.Huang@lri.fr), March 2002.
+
+
diff --git a/contrib/jprover/jall.ml b/contrib/jprover/jall.ml
new file mode 100644
index 00000000..876dc6c0
--- /dev/null
+++ b/contrib/jprover/jall.ml
@@ -0,0 +1,4701 @@
+(*
+ * JProver first-order automated prover. See the interface file
+ * for more information and a list of references for 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>
+ *)
+
+(*: All of Huang's modifications of this file are quoted or denoted
+ by comments followed by a colon.
+:*)
+
+(*:
+open Mp_debug
+
+open Refiner.Refiner
+open Term
+open TermType
+open TermOp
+open TermSubst
+open TermMan
+open RefineError
+open Opname
+:*)
+
+open Jterm
+open Opname
+open Jlogic
+open Jtunify
+
+let ruletable = Jlogic.ruletable
+
+(*:
+let free_var_op = make_opname ["free_variable";"Jprover"]
+let jprover_op = make_opname ["string";"Jprover"]
+:*)
+let free_var_op = make_opname ["free_variable"; "Jprover"]
+let jprover_op = make_opname ["jprover"; "string"]
+
+module JProver (JLogic : JLogicSig) =
+struct
+ type polarity = I | O
+
+ type connective = And | Or | Neg | Imp | All | Ex | At | Null
+
+ type ptype = Alpha | Beta | Gamma | Delta | Phi | Psi | PNull
+
+ type stype =
+ Alpha_1 | Alpha_2 | Beta_1 | Beta_2 | Gamma_0 | Delta_0
+ | Phi_0 | Psi_0 | PNull_0
+
+ type pos = {name : string;
+ address : int list;
+ op : connective;
+ pol : polarity;
+ pt : ptype;
+ st : stype;
+ label : term}
+
+ type 'pos ftree =
+ Empty
+ | NodeAt of 'pos
+ | NodeA of 'pos * ('pos ftree) array
+
+ type atom = {aname : string;
+ aaddress : int list;
+ aprefix : string list;
+ apredicate : operator;
+ apol : polarity;
+ ast : stype;
+ alabel : term}
+
+ type atom_relations = atom * atom list * atom list
+(* all atoms except atom occur in [alpha_set] and [beta_set] of atom*)
+
+(* beta proofs *)
+
+ type bproof = BEmpty
+ | RNode of string list * bproof
+ | CNode of (string * string)
+ | BNode of string * (string list * bproof) * (string list * bproof)
+ | AtNode of string * (string * string)
+
+(* Assume only constants for instantiations, not adapted to terms yet *)
+ type inf = rule * term * term
+
+(* proof tree for pretty print and permutation *)
+ type 'inf ptree =
+ PEmpty
+ | PNodeAx of 'inf
+ | PNodeA of 'inf * 'inf ptree
+ | PNodeB of 'inf * 'inf ptree * 'inf ptree
+
+ module OrderedAtom =
+ struct
+ type t = atom
+ let compare a1 a2 = if (a1.aname) = (a2.aname) then 0 else
+ if (a1.aname) < (a2.aname) then -1 else 1
+ end
+
+ module AtomSet = Set.Make(OrderedAtom)
+
+ module OrderedString =
+ struct
+ type t = string
+ let compare a1 a2 = if a1 = a2 then 0 else
+ if a1 < a2 then -1 else 1
+ end
+
+ module StringSet = Set.Make(OrderedString)
+
+(*i let _ =
+ show_loading "Loading Jall%t" i*)
+
+ let debug_jprover =
+ create_debug (**)
+ { debug_name = "jprover";
+ debug_description = "Display Jprover operations";
+ debug_value = false
+ }
+
+ let jprover_bug = Invalid_argument "Jprover bug (Jall module)"
+
+(*****************************************************************)
+
+(************* printing function *************************************)
+
+(************ printing T-string unifiers ****************************)
+
+(* ******* 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
+
+(*****************************************************)
+
+(********* printing atoms and their relations ***********************)
+
+ let print_stype st =
+ match st with
+ Alpha_1 -> Format.print_string "Alpha_1"
+ | Alpha_2 -> Format.print_string "Alpha_2"
+ | Beta_1 -> Format.print_string "Beta_1"
+ | Beta_2 -> Format.print_string "Beta_2"
+ | Gamma_0 -> Format.print_string "Gamma_0"
+ | Delta_0 -> Format.print_string "Delta_0"
+ | Phi_0 -> Format.print_string "Phi_0"
+ | Psi_0 -> Format.print_string "Psi_0"
+ | PNull_0 -> Format.print_string "PNull_0"
+
+ let print_pol pol =
+ if pol = O then
+ Format.print_string "O"
+ else
+ Format.print_string "I"
+
+ let rec print_address int_list =
+ match int_list with
+ [] ->
+ Format.print_string ""
+ | hd::rest ->
+ begin
+ Format.print_int hd;
+ print_address rest
+ end
+
+ let rec print_prefix prefix_list =
+ match prefix_list with
+ [] -> Format.print_string ""
+ | f::r ->
+ begin
+ Format.print_string f;
+ print_prefix r
+ end
+
+ let print_atom at tab =
+ let ({aname=x; aaddress=y; aprefix=z; apredicate=p; apol=a; ast=b; alabel=label}) = at in
+ begin
+ Format.print_string ("{aname="^x^"; address=");
+ print_address y;
+ Format.print_string "; ";
+ Format.force_newline ();
+ Format.print_break (tab+1) (tab+1);
+ Format.print_string "prefix=";
+ print_prefix z;
+ Format.print_string "; predicate=<abstr>; ";
+ Format.print_break (tab+1) (tab+1);
+ Format.print_break (tab+1) (tab+1);
+ Format.print_string "pol=";
+ print_pol a;
+ Format.print_string "; stype=";
+ print_stype b;
+ Format.print_string "; arguments=[<abstr>]";
+ Format.print_string "\n alabel=";
+ print_term stdout label;
+ Format.print_string "}"
+ end
+
+ let rec print_atom_list set tab =
+ match set with
+ [] -> Format.print_string ""
+ | (f::r) ->
+ begin
+ Format.force_newline ();
+ Format.print_break (tab) (tab);
+ print_atom f tab;
+ print_atom_list r (tab)
+ end
+
+ let rec print_atom_info atom_relation =
+ match atom_relation with
+ [] -> Format.print_string ""
+ | (a,b,c)::r ->
+ begin
+ Format.print_string "atom:";
+ Format.force_newline ();
+ Format.print_break 3 3;
+ print_atom a 3;
+ Format.force_newline ();
+ Format.print_break 0 0;
+ Format.print_string "alpha_set:";
+ print_atom_list b 3;
+ Format.force_newline ();
+ Format.print_break 0 0;
+ Format.print_string "beta_set:";
+ print_atom_list c 3;
+ Format.force_newline ();
+ Format.force_newline ();
+ Format.print_break 0 0;
+ print_atom_info r
+ end
+
+(*************** print formula tree, tree ordering etc. ***********)
+
+ let print_ptype pt =
+ match pt with
+ Alpha -> Format.print_string "Alpha"
+ | Beta -> Format.print_string "Beta"
+ | Gamma -> Format.print_string "Gamma"
+ | Delta -> Format.print_string "Delta"
+ | Phi -> Format.print_string "Phi"
+ | Psi -> Format.print_string "Psi"
+ | PNull -> Format.print_string "PNull"
+
+ let print_op op =
+ match op with
+ At -> Format.print_string "Atom"
+ | Neg -> Format.print_string "Neg"
+ | And -> Format.print_string "And"
+ | Or -> Format.print_string "Or"
+ | Imp -> Format.print_string "Imp"
+ | Ex -> Format.print_string "Ex"
+ | All -> Format.print_string "All"
+ | Null -> Format.print_string "Null"
+
+ let print_position position tab =
+ let ({name=x; address=y; op=z; pol=a; pt=b; st=c; label=t}) = position in
+ begin
+ Format.print_string ("{name="^x^"; address=");
+ print_address y;
+ Format.print_string "; ";
+ Format.force_newline ();
+ Format.print_break (tab+1) 0;
+(* Format.print_break 0 3; *)
+ Format.print_string "op=";
+ print_op z;
+ Format.print_string "; pol=";
+ print_pol a;
+ Format.print_string "; ptype=";
+ print_ptype b;
+ Format.print_string "; stype=";
+ print_stype c;
+ Format.print_string ";";
+ Format.force_newline ();
+ Format.print_break (tab+1) 0;
+ Format.print_string "label=";
+ Format.print_break 0 0;
+ Format.force_newline ();
+ Format.print_break tab 0;
+ print_term stdout t;
+ Format.print_string "}"
+ end
+
+ let rec pp_ftree_list tree_list tab =
+ let rec pp_ftree ftree new_tab =
+ let dummy = String.make (new_tab-2) ' ' in
+ match ftree with
+ Empty -> Format.print_string ""
+ | NodeAt(position) ->
+ begin
+ Format.force_newline ();
+ Format.print_break new_tab 0;
+ print_string (dummy^"AtomNode: ");
+(* Format.force_newline ();
+ Format.print_break 0 3;
+*)
+ print_position position new_tab;
+ Format.force_newline ();
+ Format.print_break new_tab 0
+ end
+ | NodeA(position,subtrees) ->
+ let tree_list = Array.to_list subtrees in
+ begin
+ Format.force_newline ();
+ Format.print_break new_tab 0;
+ Format.print_break 0 0;
+ print_string (dummy^"InnerNode: ");
+ print_position position new_tab;
+ Format.force_newline ();
+ Format.print_break 0 0;
+ pp_ftree_list tree_list (new_tab-3)
+ end
+ in
+ let new_tab = tab+5 in
+ match tree_list with
+ [] -> Format.print_string ""
+ | first::rest ->
+ begin
+ pp_ftree first new_tab;
+ pp_ftree_list rest tab
+ end
+
+ let print_ftree ftree =
+ begin
+ Format.open_box 0;
+ Format.print_break 3 0;
+ pp_ftree_list [ftree] 0;
+ Format.print_flush ()
+ end
+
+ let rec stringlist_to_string stringlist =
+ match stringlist with
+ [] -> "."
+ | f::r ->
+ let rest_s = stringlist_to_string r in
+ (f^"."^rest_s)
+
+ let rec print_stringlist slist =
+ match slist with
+ [] ->
+ Format.print_string ""
+ | f::r ->
+ begin
+ Format.print_string (f^".");
+ print_stringlist r
+ end
+
+ let rec pp_bproof_list tree_list tab =
+ let rec pp_bproof ftree new_tab =
+ let dummy = String.make (new_tab-2) ' ' in
+ match ftree with
+ BEmpty -> Format.print_string ""
+ | CNode((c1,c2)) ->
+ begin
+ Format.open_box 0;
+ Format.force_newline ();
+ Format.print_break (new_tab-10) 0;
+ Format.open_box 0;
+ Format.force_newline ();
+ Format.print_string (dummy^"CloseNode: connection = ("^c1^","^c2^")");
+ Format.print_flush();
+(* Format.force_newline ();
+ Format.print_break 0 3;
+*)
+ Format.open_box 0;
+ Format.print_break new_tab 0;
+ Format.print_flush()
+ end
+ | AtNode(posname,(c1,c2)) ->
+ begin
+ Format.open_box 0;
+ Format.force_newline ();
+ Format.print_break (new_tab-10) 0;
+ Format.open_box 0;
+ Format.force_newline ();
+ Format.print_string (dummy^"AtNode: pos = "^posname^" conneciton = ("^c1^","^c2^")");
+ Format.print_flush();
+(* Format.force_newline ();
+ Format.print_break 0 3;
+*)
+ Format.open_box 0;
+ Format.print_break new_tab 0;
+ Format.print_flush()
+ end
+ | RNode(alpha_layer,bproof) ->
+ let alpha_string = stringlist_to_string alpha_layer in
+ begin
+ Format.open_box 0;
+ Format.force_newline ();
+ Format.print_break new_tab 0;
+ Format.print_break 0 0;
+ Format.force_newline ();
+ Format.print_flush();
+ Format.open_box 0;
+ print_string (dummy^"RootNode: "^alpha_string);
+ Format.print_flush();
+ Format.open_box 0;
+ Format.print_break 0 0;
+ Format.print_flush();
+ pp_bproof_list [bproof] (new_tab-3)
+ end
+ | BNode(posname,(alph1,bproof1),(alph2,bproof2)) ->
+ let alpha_string1 = stringlist_to_string alph1
+ and alpha_string2 = stringlist_to_string alph2 in
+ begin
+ Format.open_box 0;
+ Format.force_newline ();
+ Format.print_break new_tab 0;
+ Format.print_break 0 0;
+ Format.force_newline ();
+ Format.print_flush();
+ Format.open_box 0;
+ print_string (dummy^"BetaNode: pos = "^posname^" layer1 = "^alpha_string1^" layer2 = "^alpha_string2);
+ Format.print_flush();
+ Format.open_box 0;
+ Format.print_break 0 0;
+ Format.print_flush();
+ pp_bproof_list [bproof1;bproof2] (new_tab-3)
+ end
+ in
+ let new_tab = tab+5 in
+ match tree_list with
+ [] -> Format.print_string ""
+ | first::rest ->
+ begin
+ pp_bproof first new_tab;
+ pp_bproof_list rest tab
+ end
+
+ let rec print_pairlist pairlist =
+ match pairlist with
+ [] -> Format.print_string ""
+ | (a,b)::rest ->
+ begin
+ Format.print_break 1 1;
+ Format.print_string ("("^a^","^b^")");
+ print_pairlist rest
+ end
+
+ let print_beta_proof bproof =
+ begin
+ Format.open_box 0;
+ Format.force_newline ();
+ Format.force_newline ();
+ Format.print_break 3 0;
+ pp_bproof_list [bproof] 0;
+ Format.force_newline ();
+ Format.force_newline ();
+ Format.force_newline ();
+ Format.print_flush ()
+ end
+
+ let rec print_treelist treelist =
+ match treelist with
+ [] ->
+ print_endline "END";
+ | f::r ->
+ begin
+ print_ftree f;
+ Format.open_box 0;
+ print_endline "";
+ print_endline "";
+ print_endline "NEXT TREE";
+ print_endline "";
+ print_endline "";
+ print_treelist r;
+ Format.print_flush ()
+ end
+
+ let rec print_set_list set_list =
+ match set_list with
+ [] -> ""
+ | f::r ->
+ (f.aname)^" "^(print_set_list r)
+
+ let print_set set =
+ let set_list = AtomSet.elements set in
+ if set_list = [] then "empty"
+ else
+ print_set_list set_list
+
+ let print_string_set set =
+ let set_list = StringSet.elements set in
+ print_stringlist set_list
+
+ let rec print_list_sets list_of_sets =
+ match list_of_sets with
+ [] -> Format.print_string ""
+ | (pos,fset)::r ->
+ begin
+ Format.print_string (pos^": "); (* first element = node which successors depend on *)
+ print_stringlist (StringSet.elements fset);
+ Format.force_newline ();
+ print_list_sets r
+ end
+
+ let print_ordering list_of_sets =
+ begin
+ Format.open_box 0;
+ print_list_sets list_of_sets;
+ Format.print_flush ()
+ end
+
+ let rec print_triplelist triplelist =
+ match triplelist with
+ [] -> Format.print_string ""
+ | ((a,b),i)::rest ->
+ begin
+ Format.print_break 1 1;
+ Format.print_string ("(("^a^","^b^"),"^(string_of_int i)^")");
+ print_triplelist rest
+ end
+
+ let print_pos_n pos_n =
+ Format.print_int pos_n
+
+ let print_formula_info ftree ordering pos_n =
+ begin
+ print_ftree ftree;
+ Format.open_box 0;
+ Format.force_newline ();
+ print_ordering ordering;
+ Format.force_newline ();
+ Format.force_newline ();
+ Format.print_string "number of positions: ";
+ print_pos_n pos_n;
+ Format.force_newline ();
+ print_endline "";
+ print_endline "";
+ Format.print_flush ()
+ end
+
+(* print sequent proof tree *)
+
+ let pp_rule (pos,r,formula,term) tab =
+ let rep = ruletable r in
+ if List.mem rep ["Alll";"Allr";"Exl";"Exr"] then
+ begin
+ Format.open_box 0;
+(* Format.force_newline (); *)
+ Format.print_break tab 0;
+ Format.print_string (pos^": "^rep^" ");
+ Format.print_flush ();
+(* Format.print_break tab 0;
+ Format.force_newline ();
+ Format.print_break tab 0;
+*)
+
+ Format.open_box 0;
+ print_term stdout formula;
+ Format.print_flush ();
+ Format.open_box 0;
+ Format.print_string " ";
+ Format.print_flush ();
+ Format.open_box 0;
+ print_term stdout term;
+ Format.force_newline ();
+ Format.force_newline ();
+ Format.print_flush ()
+ end
+ else
+ begin
+ Format.open_box 0;
+ Format.print_break tab 0;
+ Format.print_string (pos^": "^rep^" ");
+ Format.print_flush ();
+ Format.open_box 0;
+(* Format.print_break tab 0; *)
+ Format.force_newline ();
+(* Format.print_break tab 0; *)
+ print_term stdout formula;
+ Format.force_newline ()
+ end
+
+ let last addr =
+ if addr = ""
+ then ""
+ else
+ String.make 1 (String.get addr (String.length addr-1))
+
+ let rest addr =
+ if addr = ""
+ then ""
+ else
+ String.sub addr 0 ((String.length addr) - 1)
+
+ let rec get_r_chain addr =
+ if addr = "" then
+ 0
+ else
+ let l = last addr in
+ if l = "l" then
+ 0
+ else (* l = "r" *)
+ let rs = rest addr in
+ 1 + (get_r_chain rs)
+
+ let rec tpp seqtree tab addr =
+ match seqtree with
+ | PEmpty -> raise jprover_bug
+ | PNodeAx(rule) ->
+ let (pos,r,p,pa) = rule in
+ begin
+ pp_rule (pos,r,p,pa) tab;
+(* Format.force_newline (); *)
+(* let mult = get_r_chain addr in *)
+(* Format.print_break 100 (tab - (3 * mult)) *)
+ end
+ | PNodeA(rule,left) ->
+ let (pos,r,p,pa) = rule in
+ begin
+ pp_rule (pos,r,p,pa) tab;
+ tpp left tab addr
+ end
+ | PNodeB(rule,left,right) ->
+ let (pos,r,p,pa) = rule in
+ let newtab = tab + 3 in
+ begin
+ pp_rule (pos,r,p,pa) tab;
+(* Format.force_newline (); *)
+(* Format.print_break 100 newtab; *)
+ (tpp left newtab (addr^"l"));
+ (tpp right newtab (addr^"r"))
+ end
+
+ let tt seqtree =
+ begin
+ Format.open_box 0;
+ tpp seqtree 0 "";
+ Format.force_newline ();
+ Format.close_box ();
+ Format.print_newline ()
+ end
+
+(************ END printing functions *********************************)
+
+(************ Beta proofs and redundancy deletion **********************)
+
+ let rec remove_dups_connections connection_list =
+ match connection_list with
+ [] -> []
+ | (c1,c2)::r ->
+ if (List.mem (c1,c2) r) or (List.mem (c2,c1) r) then
+ (* only one direction variant of a connection stays *)
+ remove_dups_connections r
+ else
+ (c1,c2)::(remove_dups_connections r)
+
+ let rec remove_dups_list list =
+ match list with
+ [] -> []
+ | f::r ->
+ if List.mem f r then
+ remove_dups_list r
+ else
+ f::(remove_dups_list r)
+
+ let beta_pure alpha_layer connections beta_expansions =
+ let (l1,l2) = List.split connections in
+ let test_list = l1 @ l2 @ beta_expansions in
+ begin
+(* Format.open_box 0;
+ print_endline "";
+ print_stringlist alpha_layer;
+ Format.print_flush();
+ Format.open_box 0;
+ print_endline "";
+ print_stringlist test_list;
+ print_endline "";
+ Format.print_flush();
+*)
+ not (List.exists (fun x -> (List.mem x test_list)) alpha_layer)
+ end
+
+ let rec apply_bproof_purity bproof =
+ match bproof with
+ BEmpty ->
+ raise jprover_bug
+ | CNode((c1,c2)) ->
+ bproof,[(c1,c2)],[]
+ | AtNode(_,(c1,c2)) ->
+ bproof,[(c1,c2)],[]
+ | RNode(alpha_layer,subproof) ->
+ let (opt_subproof,min_connections,beta_expansions) =
+ apply_bproof_purity subproof in
+ (RNode(alpha_layer,opt_subproof),min_connections,beta_expansions)
+ | BNode(pos,(alph1,subp1),(alph2,subp2)) ->
+ let (opt_subp1,min_conn1,beta_exp1) = apply_bproof_purity subp1 in
+ if beta_pure alph1 min_conn1 beta_exp1 then
+ begin
+(* print_endline ("Left layer of "^pos); *)
+ (opt_subp1,min_conn1,beta_exp1)
+ end
+ else
+ let (opt_subp2,min_conn2,beta_exp2) = apply_bproof_purity subp2 in
+ if beta_pure alph2 min_conn2 beta_exp2 then
+ begin
+(* print_endline ("Right layer of "^pos); *)
+ (opt_subp2,min_conn2,beta_exp2)
+ end
+ else
+ let min_conn = remove_dups_connections (min_conn1 @ min_conn2)
+ and beta_exp = remove_dups_list ([pos] @ beta_exp1 @ beta_exp2) in
+ (BNode(pos,(alph1,opt_subp1),(alph2,opt_subp2)),min_conn,beta_exp)
+
+ let bproof_purity bproof =
+ let (opt_bproof,min_connections,_) = apply_bproof_purity bproof in
+ opt_bproof,min_connections
+
+(*********** split permutation *****************)
+
+ let rec apply_permutation bproof rep_name direction act_blayer =
+ match bproof with
+ BEmpty | RNode(_,_) ->
+ raise jprover_bug
+ | AtNode(cx,(c1,c2)) ->
+ bproof,act_blayer
+ | CNode((c1,c2)) ->
+ bproof,act_blayer
+ | BNode(pos,(alph1,subp1),(alph2,subp2)) ->
+ if rep_name = pos then
+ let (new_blayer,replace_branch) =
+ if direction = "left" then
+ (alph1,subp1)
+ else (* direciton = "right" *)
+ (alph2,subp2)
+ in
+ (match replace_branch with
+ CNode((c1,c2)) ->
+ (AtNode(c1,(c1,c2))),new_blayer (* perform atom expansion at c1 *)
+ | _ ->
+ replace_branch,new_blayer
+ )
+ else
+ let pproof1,new_blayer1 = apply_permutation subp1 rep_name direction act_blayer in
+ let pproof2,new_blayer2 = apply_permutation subp2 rep_name direction new_blayer1 in
+ (BNode(pos,(alph1,pproof1),(alph2,pproof2))),new_blayer2
+
+ let split_permutation pname opt_bproof =
+ match opt_bproof with
+ RNode(alayer,BNode(pos,(alph1,opt_subp1),(alph2,opt_subp2))) ->
+ if pos = pname then
+(* if topmost beta expansion agrees with pname, then *)
+(* only split the beta proof and give back the two subproofs *)
+ let (osubp1,min_con1) = bproof_purity opt_subp1
+ and (osubp2,min_con2) = bproof_purity opt_subp2 in
+(* there will be no purity reductions in the beta subproofs. We use this *)
+(* predicate to collect the set of used leaf-connections in each subproof*)
+ ((RNode((alayer @ alph1),osubp1),min_con1),
+ (RNode((alayer @ alph2),osubp2),min_con2)
+ )
+(* we combine the branch after topmost beta expansion at pos into one root alpha layer *)
+(* -- the beta expansion node pos will not be needed in this root layer *)
+ else
+ let perm_bproof1,balph1 = apply_permutation
+ (BNode(pos,(alph1,opt_subp1),(alph2,opt_subp2))) pname "left" []
+ and perm_bproof2,balph2 = apply_permutation
+ (BNode(pos,(alph1,opt_subp1),(alph2,opt_subp2))) pname "right" [] in
+
+ begin
+(* print_endline " ";
+ print_beta_proof perm_bproof1;
+ print_endline" " ;
+ print_beta_proof perm_bproof2;
+ print_endline" ";
+*)
+ let (osubp1,min_con1) = bproof_purity perm_bproof1
+ and (osubp2,min_con2) = bproof_purity perm_bproof2 in
+ ((RNode((alayer @ balph1),osubp1),min_con1),
+ (RNode((alayer @ balph2),osubp2),min_con2)
+ )
+ end
+(* we combine the branch after the NEW topmost beta expansion at bpos *)
+(* into one root alpha layer -- the beta expansion node bpos will not be *)
+(* needed in this root layer *)
+ | _ ->
+ raise jprover_bug
+
+(*********** END split permutation *****************)
+
+ let rec list_del list_el el_list =
+ match el_list with
+ [] ->
+ raise jprover_bug
+ | f::r ->
+ if list_el = f then
+ r
+ else
+ f::(list_del list_el r)
+
+ let rec list_diff del_list check_list =
+ match del_list with
+ [] ->
+ []
+ | f::r ->
+ if List.mem f check_list then
+ list_diff r check_list
+ else
+ f::(list_diff r check_list)
+
+(* let rec compute_alpha_layer ftree_list =
+ match ftree_list with
+ [] ->
+ [],[],[]
+ | f::r ->
+ (match f with
+ Empty ->
+ raise jprover_bug
+ | NodeAt(pos) ->
+ let pn = pos.name
+ and (rnode,ratom,borderings) = compute_alpha_layer r in
+ ((pn::rnode),(pn::ratom),borderings)
+ | NodeA(pos,suctrees) ->
+ let pn = pos.name in
+ if pos.pt = Beta then
+ let (rnode,ratom,borderings) = compute_alpha_layer r in
+ ((pn::rnode),(ratom),(f::borderings))
+ else
+ let suclist = Array.to_list suctrees in
+ compute_alpha_layer (suclist @ r)
+ )
+
+ let rec compute_connection alpha_layer union_atoms connections =
+ match connections with
+ [] -> ("none","none")
+ | (c,d)::r ->
+ if (List.mem c union_atoms) & (List.mem d union_atoms) then
+ let (c1,c2) =
+ if List.mem c alpha_layer then
+ (c,d)
+ else
+ if List.mem d alpha_layer then
+ (d,c) (* then, d is supposed to occur in [alpha_layer] *)
+ else
+ raise (Invalid_argument "Jprover bug: connection match failure")
+ in
+ (c1,c2)
+ else
+ compute_connection alpha_layer union_atoms r
+
+ let get_beta_suctrees btree =
+ match btree with
+ Empty | NodeAt(_) -> raise jprover_bug
+ | NodeA(pos,suctrees) ->
+ let b1tree = suctrees.(0)
+ and b2tree = suctrees.(1) in
+ (pos.name,b1tree,b2tree)
+
+ let rec build_beta_proof alpha_layer union_atoms beta_orderings connections =
+ let (c1,c2) = compute_connection alpha_layer union_atoms connections in
+(* [c1] is supposed to occur in the lowmost alpha layer of the branch, *)
+(* i.e. [aplha_layer] *)
+ if (c1,c2) = ("none","none") then
+ (match beta_orderings with
+ [] -> raise jprover_bug
+ | btree::r ->
+ let (beta_pos,suctree1,suctree2) = get_beta_suctrees btree in
+ let (alpha_layer1, atoms1, bordering1) = compute_alpha_layer [suctree1]
+ and (alpha_layer2, atoms2, bordering2) = compute_alpha_layer [suctree2] in
+ let bproof1,beta1,closure1 =
+ build_beta_proof alpha_layer1 (atoms1 @ union_atoms)
+ (bordering1 @ r) connections
+ in
+ let bproof2,beta2,closure2 =
+ build_beta_proof alpha_layer2 (atoms2 @ union_atoms)
+ (bordering2 @ r) connections in
+ (BNode(beta_pos,(alpha_layer1,bproof1),(alpha_layer2,bproof2))),(1+beta1+beta2),(closure1+closure2)
+ )
+ else
+ CNode((c1,c2)),0,1
+
+ let construct_beta_proof ftree connections =
+ let (root_node,root_atoms,beta_orderings) = compute_alpha_layer [ftree]
+ in
+ let beta_proof,beta_exp,closures =
+ build_beta_proof root_node root_atoms beta_orderings connections in
+ (RNode(root_node,beta_proof)),beta_exp,closures
+*)
+
+
+(* *********** New Version with direct computation from extension proof **** *)
+(* follows a DIRECT step from proof histories via pr-connection orderings to opt. beta-proofs *)
+
+ let rec compute_alpha_layer ftree_list =
+ match ftree_list with
+ [] ->
+ []
+ | f::r ->
+ (match f with
+ Empty ->
+ raise jprover_bug
+ | NodeAt(pos) ->
+ let rnode = compute_alpha_layer r in
+ (pos.name::rnode)
+ | NodeA(pos,suctrees) ->
+ if pos.pt = Beta then
+ let rnode = compute_alpha_layer r in
+ (pos.name::rnode)
+ else
+ let suclist = Array.to_list suctrees in
+ compute_alpha_layer (suclist @ r)
+ )
+
+ let rec compute_beta_difference c1_context c2_context act_context =
+ match c1_context,c2_context with
+ ([],c2_context) ->
+ (list_diff c2_context act_context)
+(* both connection partners in the same submatrix; [c1] already isolated *)
+ | ((fc1::rc1),[]) ->
+ [] (* [c2] is a reduction step, i.e. isolated before [c1] *)
+ | ((fc1::rc1),(fc2::rc2)) ->
+ if fc1 = fc2 then (* common initial beta-expansions *)
+ compute_beta_difference rc1 rc2 act_context
+ else
+ (list_diff c2_context act_context)
+
+ let rec non_closed beta_proof_list =
+ match beta_proof_list with
+ [] ->
+ false
+ | bpf::rbpf ->
+ (match bpf with
+ RNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof")
+ | AtNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof")
+ | BEmpty -> true
+ | CNode(_) -> non_closed rbpf
+ | BNode(pos,(_,bp1),(_,bp2)) -> non_closed ([bp1;bp2] @ rbpf)
+ )
+
+ let rec cut_context pos context =
+ match context with
+ [] ->
+ raise (Invalid_argument "Jprover bug: invalid context element")
+ | (f,num)::r ->
+ if pos = f then
+ context
+ else
+ cut_context pos r
+
+ let compute_tree_difference beta_proof c1_context =
+ match beta_proof with
+ RNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof")
+ | CNode(_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof")
+ | AtNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof")
+ | BEmpty -> c1_context
+ | BNode(pos,_,_) ->
+(* print_endline ("actual root: "^pos); *)
+ cut_context pos c1_context
+
+ let print_context conn bcontext =
+ begin
+ Format.open_box 0;
+ Format.print_string conn;
+ Format.print_string ": ";
+ List.iter (fun x -> let (pos,num) = x in Format.print_string (pos^" "^(string_of_int num)^"")) bcontext;
+ print_endline " ";
+ Format.print_flush ()
+ end
+
+ let rec build_opt_beta_proof beta_proof ext_proof beta_atoms beta_layer_list act_context =
+ let rec add_c2_tree (c1,c2) c2_diff_context =
+ match c2_diff_context with
+ [] ->
+ (CNode(c1,c2),0)
+ | (f,num)::c2_diff_r ->
+ let next_beta_proof,next_exp =
+ add_c2_tree (c1,c2) c2_diff_r in
+ let (layer1,layer2) = List.assoc f beta_layer_list in
+ let new_bproof =
+ if num = 1 then
+ BNode(f,(layer1,next_beta_proof),(layer2,BEmpty))
+ else (* num = 2*)
+ BNode(f,(layer1,BEmpty),(layer2,next_beta_proof))
+ in
+ (new_bproof,(next_exp+1))
+ in
+ let rec add_beta_expansions (c1,c2) rest_ext_proof c1_diff_context c2_diff_context new_act_context =
+ match c1_diff_context with
+ [] ->
+ let (n_c1,n_c2) =
+ if c2_diff_context = [] then (* make sure that leaf-connection is first element *)
+ (c1,c2)
+ else
+ (c2,c1)
+ in
+ let c2_bproof,c2_exp = add_c2_tree (n_c1,n_c2) c2_diff_context in
+ if c2_exp <> 0 then (* at least one open branch was generated to isloate [c2] *)
+ begin
+(* print_endline "start with new beta-proof"; *)
+ let new_bproof,new_exp,new_closures,new_rest_proof =
+ build_opt_beta_proof c2_bproof rest_ext_proof beta_atoms beta_layer_list (act_context @ new_act_context) in
+ (new_bproof,(new_exp+c2_exp),(new_closures+1),new_rest_proof)
+ end
+ else
+ begin
+(* print_endline "proceed with old beta-proof"; *)
+ (c2_bproof,c2_exp,1,rest_ext_proof)
+ end
+ | (f,num)::c1_diff_r ->
+ let (layer1,layer2) = List.assoc f beta_layer_list in
+ let next_beta_proof,next_exp,next_closures,next_ext_proof =
+ add_beta_expansions (c1,c2) rest_ext_proof c1_diff_r c2_diff_context new_act_context in
+ let new_bproof =
+ if num = 1 then
+ BNode(f,(layer1,next_beta_proof),(layer2,BEmpty))
+ else (* num = 2*)
+ BNode(f,(layer1,BEmpty),(layer2,next_beta_proof))
+ in
+ (new_bproof,(next_exp+1),next_closures,next_ext_proof)
+
+ in
+ let rec insert_connection beta_proof (c1,c2) rest_ext_proof c1_diff_context c2_diff_context act_context =
+ begin
+(* print_context c1 c1_diff_context;
+ print_endline "";
+ print_context c2 c2_diff_context;
+ print_endline "";
+*)
+ match beta_proof with
+ RNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof")
+ | CNode(_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof")
+ | AtNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof")
+ | BEmpty ->
+ add_beta_expansions (c1,c2) rest_ext_proof c1_diff_context c2_diff_context act_context
+ | BNode(pos,(layer1,sproof1),(layer2,sproof2)) ->
+(* print_endline (c1^" "^c2^" "^pos); *)
+ (match c1_diff_context with
+ [] ->
+ raise (Invalid_argument "Jprover bug: invalid beta-proof")
+ | (f,num)::rest_context -> (* f = pos must hold!! *)
+ if num = 1 then
+ let (next_bproof,next_exp,next_closure,next_ext_proof) =
+ insert_connection sproof1 (c1,c2) rest_ext_proof rest_context c2_diff_context act_context in
+ (BNode(pos,(layer1,next_bproof),(layer2,sproof2)),next_exp,next_closure,next_ext_proof)
+ else (* num = 2 *)
+ let (next_bproof,next_exp,next_closure,next_ext_proof) =
+ insert_connection sproof2 (c1,c2) rest_ext_proof rest_context c2_diff_context act_context in
+ (BNode(pos,(layer1,sproof1),(layer2,next_bproof)),next_exp,next_closure,next_ext_proof)
+ )
+ end
+
+ in
+ match ext_proof with
+ [] ->
+ beta_proof,0,0,[]
+ | (c1,c2)::rproof ->
+(* print_endline ("actual connection: "^c1^" "^c2); *)
+ let c1_context = List.assoc c1 beta_atoms
+ and c2_context = List.assoc c2 beta_atoms in
+ let c2_diff_context = compute_beta_difference c1_context c2_context act_context
+ and c1_diff_context = compute_tree_difference beta_proof c1_context in (* wrt. actual beta-proof *)
+ let (next_beta_proof,next_exp,next_closures,next_ext_proof) =
+ insert_connection beta_proof (c1,c2) rproof c1_diff_context c2_diff_context c1_diff_context in
+ if non_closed [next_beta_proof] then (* at least one branch was generated to isolate [c1] *)
+ let rest_beta_proof,rest_exp,rest_closures,rest_ext_proof =
+ build_opt_beta_proof next_beta_proof next_ext_proof beta_atoms beta_layer_list act_context in
+ rest_beta_proof,(next_exp+rest_exp),(next_closures+rest_closures),rest_ext_proof
+ else
+ next_beta_proof,next_exp,next_closures,next_ext_proof
+
+ let rec annotate_atoms beta_context atlist treelist =
+ let rec annotate_tree beta_context tree atlist =
+ match tree with
+ Empty ->
+ (atlist,[],[])
+ | NodeAt(pos) ->
+ if List.mem pos.name atlist then
+ let new_atlist = list_del pos.name atlist in
+ (new_atlist,[(pos.name,beta_context)],[])
+ else
+ (atlist,[],[])
+ | NodeA(pos,suctrees) ->
+ if pos.pt = Beta then
+ let s1,s2 = suctrees.(0),suctrees.(1) in
+ let alayer1 = compute_alpha_layer [s1]
+ and alayer2 = compute_alpha_layer [s2]
+ and new_beta_context1 = beta_context @ [(pos.name,1)]
+ and new_beta_context2 = beta_context @ [(pos.name,2)] in
+ let atlist1,annotates1,blayer_list1 =
+ annotate_atoms new_beta_context1 atlist [s1] in
+ let atlist2,annotates2,blayer_list2 =
+ annotate_atoms new_beta_context2 atlist1 [s2]
+ in
+ (atlist2,(annotates1 @ annotates2),((pos.name,(alayer1,alayer2))::(blayer_list1 @ blayer_list2)))
+ else
+ annotate_atoms beta_context atlist (Array.to_list suctrees)
+ in
+ match treelist with
+ [] -> (atlist,[],[])
+ | f::r ->
+ let (next_atlist,f_annotates,f_beta_layers) = annotate_tree beta_context f atlist in
+ let (rest_atlist,rest_annotates,rest_beta_layers) = (annotate_atoms beta_context next_atlist r)
+ in
+ (rest_atlist, (f_annotates @ rest_annotates),(f_beta_layers @ rest_beta_layers))
+
+ let construct_opt_beta_proof ftree ext_proof =
+ let con1,con2 = List.split ext_proof in
+ let con_atoms = remove_dups_list (con1 @ con2) in
+ let (empty_atoms,beta_atoms,beta_layer_list) = annotate_atoms [] con_atoms [ftree] in
+ let root_node = compute_alpha_layer [ftree] in
+ let (beta_proof,beta_exp,closures,_) =
+ build_opt_beta_proof BEmpty ext_proof beta_atoms beta_layer_list [] in
+ (RNode(root_node,beta_proof)),beta_exp,closures
+
+(************* permutation ljmc -> lj *********************************)
+
+(* REAL PERMUTATION STAFF *)
+
+ let subf1 n m subrel = List.mem ((n,m),1) subrel
+ let subf2 n m subrel = List.mem ((n,m),2) subrel
+ let tsubf n m tsubrel = List.mem (n,m) tsubrel
+
+(* Transforms all normal form layers in an LJ proof *)
+
+ let rec modify prooftree (subrel,tsubrel) =
+ match prooftree with
+ PEmpty ->
+ raise jprover_bug
+ | PNodeAx((pos,inf,form,term)) ->
+ prooftree,pos
+ | PNodeA((pos,inf,form,term),left) ->
+ let t,qpos = modify left (subrel,tsubrel) in
+ if List.mem inf [Impr;Negr;Allr] then
+ PNodeA((pos,inf,form,term),t),pos (* layer bound *)
+ else if qpos = "Orl-True" then
+ PNodeA((pos,inf,form,term),t),qpos
+ else if List.mem inf [Andl;Alll;Exl] then
+ PNodeA((pos,inf,form,term),t),qpos (* simply propagation *)
+ else if inf = Exr then
+ if (subf1 pos qpos subrel) then
+ PNodeA((pos,inf,form,term),t),pos
+ else t,qpos
+ else if inf = Negl then
+ if (subf1 pos qpos subrel) then
+ PNodeA((pos,inf,form,term),t),"" (* empty string *)
+ else t,qpos
+ else (* x = Orr *)
+ if (subf1 pos qpos subrel) then
+ PNodeA((pos,Orr1,form,term),t),pos (* make Orr for LJ *)
+ else if (subf2 pos qpos subrel) then
+ PNodeA((pos,Orr2,form,term),t),pos (* make Orr for LJ *)
+ else t,qpos
+ | PNodeB((pos,inf,form,term),left,right) ->
+ let t,qpos = modify left (subrel,tsubrel) in
+ if inf = Andr then
+ if (or) (qpos = "Orl-True") (subf1 pos qpos subrel) then
+ let s,rpos = modify right (subrel,tsubrel) in (* Orl-True -> subf *)
+ if (or) (rpos = "Orl-True") (subf2 pos rpos subrel) then
+ PNodeB((pos,inf,form,term),t,s),pos
+ else s,rpos
+ else t,qpos (* not subf -> not Orl-True *)
+ else if inf = Impl then
+ if (subf1 pos qpos subrel) then
+ let s,rpos = modify right (subrel,tsubrel) in
+ PNodeB((pos,inf,form,term),t,s),"" (* empty string *)
+ else t,qpos
+ else (* x = Orl *)
+ let s,rpos = modify right (subrel,tsubrel) in
+ PNodeB((pos,inf,form,term),t,s),"Orl-True"
+
+(* transforms the subproof into an LJ proof between
+ the beta-inference rule (excluded) and
+ layer boundary in the branch ptree *)
+
+ let rec rec_modify ptree (subrel,tsubrel) =
+ match ptree with
+ PEmpty ->
+ raise jprover_bug
+ | PNodeAx((pos,inf,form,term)) ->
+ ptree,pos
+ | PNodeA((pos,inf,form,term),left) ->
+ if List.mem inf [Impr;Negr;Allr] then
+ ptree,pos (* layer bound, stop transforming! *)
+ else
+ let t,qpos = rec_modify left (subrel,tsubrel) in
+ if List.mem inf [Andl;Alll;Exl] then
+ PNodeA((pos,inf,form,term),t),qpos (* simply propagation*)
+ else if inf = Exr then
+ if (subf1 pos qpos subrel) then
+ PNodeA((pos,inf,form,term),t),pos
+ else t,qpos
+ else if inf = Negl then
+ if (subf1 pos qpos subrel) then
+ PNodeA((pos,inf,form,term),t),"" (* empty string *)
+ else t,qpos
+ else (* x = Orr *)
+ if (subf1 pos qpos subrel) then
+ PNodeA((pos,Orr1,form,term),t),pos (* make Orr for LJ *)
+ else if (subf2 pos qpos subrel) then
+ PNodeA((pos,Orr2,form,term),t),pos (* make Orr for LJ *)
+ else t,qpos
+ | PNodeB((pos,inf,form,term),left,right) ->
+ let t,qpos = rec_modify left (subrel,tsubrel) in
+ if inf = Andr then
+ if (subf1 pos qpos subrel) then
+ let s,rpos = rec_modify right (subrel,tsubrel) in
+ if (subf2 pos rpos subrel) then
+ PNodeB((pos,inf,form,term),t,s),pos
+ else s,rpos
+ else t,qpos
+ else (* x = Impl since x= Orl cannot occur in the partial layer ptree *)
+
+ if (subf1 pos qpos subrel) then
+ let s,rpos = rec_modify right (subrel,tsubrel) in
+ PNodeB((pos,inf,form,term),t,s),"" (* empty string *)
+ else t,qpos
+
+ let weak_modify rule ptree (subrel,tsubrel) = (* recall rule = or_l *)
+ let (pos,inf,formlua,term) = rule in
+ if inf = Orl then
+ ptree,true
+ else
+ let ptreem,qpos = rec_modify ptree (subrel,tsubrel) in
+ if (subf1 pos qpos subrel) then (* weak_modify will always be applied on left branches *)
+ ptreem,true
+ else
+ ptreem,false
+
+(* Now, the permutation stuff .... *)
+
+(* Permutation schemes *)
+
+(* corresponds to local permutation lemma -- Lemma 3 in the paper -- *)
+(* with eigenvariablen renaming and branch modification *)
+
+(* eigenvariablen renaming and branch modification over *)
+(* the whole proofs, i.e. over layer boundaries, too *)
+
+
+(* global variable vor eigenvariable renaming during permutations *)
+
+ let eigen_counter = ref 1
+
+(* append renamed paramater "r" to non-quantifier subformulae
+ of renamed quantifier formulae *)
+
+(*: BUG :*)
+(*:
+ let make_new_eigenvariable term =
+ let op = (dest_term term).term_op in
+ let opn = (dest_op op).op_name in
+ let opnam = dest_opname opn in
+ match opnam with
+ [] ->
+ raise jprover_bug
+ | ofirst::orest ->
+ let ofname = List.hd orest in
+ let new_eigen_var = (ofname^"_r"^(string_of_int (!eigen_counter))) in
+ eigen_counter := !eigen_counter + 1;
+(* print_endline ("New Counter :"^(string_of_int (!eigen_counter))); *)
+ mk_string_term jprover_op new_eigen_var
+:*)
+
+ let make_new_eigenvariable term =
+ let op = (dest_term term).term_op in
+ let opa = (dest_op op).op_params in
+ let oppar = dest_param opa in
+ match oppar with
+ | String ofname::_ ->
+ let new_eigen_var = (ofname^"_r"^(string_of_int (!eigen_counter))) in
+ eigen_counter := !eigen_counter + 1;
+ mk_string_term jprover_op new_eigen_var
+ | _ -> raise jprover_bug
+
+
+ let replace_subterm term oldt rept =
+ let v_term = var_subst term oldt "dummy_var" in
+ subst1 v_term "dummy_var" rept
+
+ let rec eigen_rename old_parameter new_parameter ptree =
+ match ptree with
+ PEmpty ->
+ raise jprover_bug
+ | PNodeAx((pos,inf,form,term)) ->
+ let new_form = replace_subterm form old_parameter new_parameter in
+ PNodeAx((pos,inf,new_form,term))
+ | PNodeA((pos,inf,form,term), left) ->
+ let new_form = replace_subterm form old_parameter new_parameter
+ and new_term = replace_subterm term old_parameter new_parameter in
+ let ren_left = eigen_rename old_parameter new_parameter left in
+ PNodeA((pos,inf,new_form,new_term), ren_left)
+ | PNodeB((pos,inf,form,term),left, right) ->
+ let new_form = replace_subterm form old_parameter new_parameter in
+ let ren_left = eigen_rename old_parameter new_parameter left in
+ let ren_right = eigen_rename old_parameter new_parameter right in
+ PNodeB((pos,inf,new_form,term), ren_left, ren_right)
+
+ let rec update_ptree rule subtree direction tsubrel =
+ match subtree with
+ PEmpty ->
+ raise jprover_bug
+ | PNodeAx(r) ->
+ subtree
+ | PNodeA((pos,inf,formula,term), left) ->
+ if (pos,inf,formula,term) = rule then
+ left
+ (* don't delete rule if subformula belongs to renamed instance of quantifiers; *)
+ (* but this can never occur now since (renamed) formula is part of rule *)
+ else
+ let (posn,infn,formn,termn) = rule in
+ if (&) (List.mem infn [Exl;Allr] ) (term = termn) then
+ (* this can only occur if eigenvariable rule with same term as termn has been permuted; *)
+ (* the application of the same eigenvariable introduction on the same subformula with *)
+ (* different instantiated variables might occur! *)
+ (* termn cannot occur in terms of permuted quantifier rules due to substitution split *)
+ (* during reconstruciton of the ljmc proof *)
+ let new_term = make_new_eigenvariable term in
+(* print_endline "Eigenvariable renaming!!!"; *)
+ eigen_rename termn new_term subtree
+ else
+ let left_del =
+ update_ptree rule left direction tsubrel
+ in
+ PNodeA((pos,inf,formula,term), left_del)
+ | PNodeB((pos,inf,formula,term), left, right) ->
+ if (pos,inf,formula,term) = rule then
+ if direction = "l" then
+ left
+ else
+ right (* direction = "r" *)
+ else
+ let left_del = update_ptree rule left direction tsubrel in
+ let right_del = update_ptree rule right direction tsubrel in
+ PNodeB((pos,inf,formula,term),left_del,right_del)
+
+ let permute r1 r2 ptree la tsubrel =
+(* print_endline "permute in"; *)
+ match ptree,la with
+ PNodeA(r1, PNodeA(r2,left)),la ->
+(* print_endline "1-o-1"; *)
+ PNodeA(r2, PNodeA(r1,left))
+ (* one-over-one *)
+ | PNodeA(r1, PNodeB(r2,left,right)),la ->
+(* print_endline "1-o-2"; *)
+ PNodeB(r2, PNodeA(r1,left), PNodeA(r1,right))
+ (* one-over-two *)
+ | PNodeB(r1, PNodeA(r2,left), right),"l" ->
+(* print_endline "2-o-1 left"; *)
+ let right_u = update_ptree r2 right "l" tsubrel in
+ PNodeA(r2, PNodeB(r1, left, right_u))
+ (* two-over-one left *)
+ | PNodeB(r1, left, PNodeA(r2,right)),"r" ->
+(* print_endline "2-o-1 right"; *)
+ let left_u = update_ptree r2 left "l" tsubrel in
+ PNodeA(r2, PNodeB(r1, left_u, right))
+ (* two-over-one right *)
+ | PNodeB(r1, PNodeB(r2,left2,right2), right),"l" ->
+(* print_endline "2-o-2 left"; *)
+ let right_ul = update_ptree r2 right "l" tsubrel in
+ let right_ur = update_ptree r2 right "r" tsubrel in
+ PNodeB(r2,PNodeB(r1,left2,right_ul),PNodeB(r1,right2,right_ur))
+ (* two-over-two left *)
+ | PNodeB(r1, left, PNodeB(r2,left2,right2)),"r" ->
+(* print_endline "2-o-2 right"; *)
+ let left_ul = update_ptree r2 left "l" tsubrel in
+ let left_ur = update_ptree r2 left "r" tsubrel in
+ PNodeB(r2,PNodeB(r1,left_ul,left2),PNodeB(r1,left_ur, right2))
+ (* two-over-two right *)
+ | _ -> raise jprover_bug
+
+(* permute layers, isolate addmissible branches *)
+
+(* computes if an Andr is d-generatives *)
+
+ let layer_bound rule =
+ let (pos,inf,formula,term) = rule in
+ if List.mem inf [Impr;Negr;Allr] then
+ true
+ else
+ false
+
+ let rec orl_free ptree =
+ match ptree with
+ PEmpty ->
+ raise jprover_bug
+ | PNodeAx(rule) ->
+ true
+ | PNodeA(rule,left) ->
+ if layer_bound rule then
+ true
+ else
+ orl_free left
+ | PNodeB(rule,left,right) ->
+ let (pos,inf,formula,term) = rule in
+ if inf = Orl then
+ false
+ else
+ (&) (orl_free left) (orl_free right)
+
+ let rec dgenerative rule dglist ptree tsubrel =
+ let (pos,inf,formula,term) = rule in
+ if List.mem inf [Exr;Orr;Negl] then
+ true
+ else if inf = Andr then
+ if dglist = [] then
+ false
+ else
+ let first,rest = (List.hd dglist),(List.tl dglist) in
+ let (pos1,inf1,formula1,term1) = first in
+ if tsubf pos1 pos tsubrel then
+ true
+ else
+ dgenerative rule rest ptree tsubrel
+ else if inf = Impl then
+ not (orl_free ptree)
+ else
+ false
+
+
+(* to compute a topmost addmissible pair r,o with
+ the address addr of r in the proof tree
+*)
+
+ let rec top_addmissible_pair ptree dglist act_r act_o act_addr tsubrel dummyt =
+ let rec search_pair ptree dglist act_r act_o act_addr tsubrel =
+ match ptree with
+ PEmpty -> raise jprover_bug
+ | PNodeAx(_) -> raise jprover_bug
+ | PNodeA(rule, left) ->
+(* print_endline "alpha"; *)
+ if (dgenerative rule dglist left tsubrel) then (* r = Exr,Orr,Negl *)
+ let newdg = (@) [rule] dglist in
+ search_pair left newdg act_r rule act_addr tsubrel
+ else (* Impr, Allr, Notr only for test *)
+ search_pair left dglist act_r act_o act_addr tsubrel
+ | PNodeB(rule,left,right) ->
+(* print_endline "beta"; *)
+ let (pos,inf,formula,term) = rule in
+ if List.mem inf [Andr;Impl] then
+ let bool = dgenerative rule dglist left tsubrel in
+ let newdg,newrule =
+ if bool then
+ ((@) [rule] dglist),rule
+ else
+ dglist,act_o
+ in
+ if orl_free left then
+ search_pair right newdg act_r newrule (act_addr^"r") tsubrel
+ else (* not orl_free *)
+ let left_r,left_o,left_addr =
+ search_pair left newdg act_r newrule (act_addr^"l") tsubrel in
+ if left_o = ("",Orr,dummyt,dummyt) then
+ top_addmissible_pair right dglist act_r act_o (act_addr^"r") tsubrel dummyt
+ else left_r,left_o,left_addr
+ else (* r = Orl *)
+ if orl_free left then
+ top_addmissible_pair right dglist rule act_o (act_addr^"r") tsubrel dummyt
+ else
+ let left_r,left_o,left_addr
+ = search_pair left dglist rule act_o (act_addr^"l") tsubrel in
+ if left_o = ("",Orr,dummyt,dummyt) then
+ top_addmissible_pair right dglist rule act_o (act_addr^"r") tsubrel dummyt
+ else
+ left_r,left_o,left_addr
+ in
+(* print_endline "top_addmissible_pair in"; *)
+ if orl_free ptree then (* there must be a orl BELOW an layer bound *)
+ begin
+(* print_endline "orl_free"; *)
+ act_r,act_o,act_addr
+ end
+ else
+ begin
+(* print_endline "orl_full"; *)
+ search_pair ptree dglist act_r act_o act_addr tsubrel
+ end
+
+ let next_direction addr act_addr =
+ String.make 1 (String.get addr (String.length act_addr))
+ (* get starts with count 0*)
+
+ let change_last addr d =
+ let split = (String.length addr) - 1 in
+ let prec,last =
+ (String.sub addr 0 split),(String.sub addr split 1) in
+ prec^d^last
+
+ let last addr =
+ if addr = ""
+ then ""
+ else
+ String.make 1 (String.get addr (String.length addr-1))
+
+ let rest addr =
+ if addr = ""
+ then ""
+ else
+ String.sub addr 0 ((String.length addr) - 1)
+
+ let rec permute_layer ptree dglist (subrel,tsubrel) =
+ let rec permute_branch r addr act_addr ptree dglist (subrel,tsubrel) =
+(* print_endline "pbranch in"; *)
+ let la = last act_addr in (* no ensure uniqueness at 2-over-x *)
+ match ptree,la with
+ PNodeA(o,PNodeA(rule,left)),la -> (* one-over-one *)
+(* print_endline " one-over-one "; *)
+ let permute_result = permute o rule ptree la tsubrel in
+ begin match permute_result with
+ PNodeA(r2,left2) ->
+ let pbleft = permute_branch r addr act_addr left2 dglist (subrel,tsubrel) in
+ PNodeA(r2,pbleft)
+ | _ -> raise jprover_bug
+ end
+ | PNodeA(o,PNodeB(rule,left,right)),la -> (* one-over-two *)
+(* print_endline " one-over-two "; *)
+ if rule = r then (* left,right are or_l free *)
+ permute o rule ptree la tsubrel (* first termination case *)
+ else
+ let d = next_direction addr act_addr in
+ if d = "l" then
+ let permute_result = permute o rule ptree la tsubrel in
+ (match permute_result with
+ PNodeB(r2,left2,right2) ->
+ let pbleft = permute_branch r addr (act_addr^d) left2 dglist (subrel,tsubrel) in
+ let plright = permute_layer right2 dglist (subrel,tsubrel) in
+ PNodeB(r2,pbleft,plright)
+ | _ -> raise jprover_bug
+ )
+ else (* d = "r", that is left of rule is or_l free *)
+ let left1,bool = weak_modify rule left (subrel,tsubrel) in
+ if bool then (* rule is relevant *)
+ let permute_result = permute o rule (PNodeA(o,PNodeB(rule,left1,right))) la tsubrel in
+ (match permute_result with
+ PNodeB(r2,left2,right2) ->
+ let pbright = permute_branch r addr (act_addr^d) right2 dglist (subrel,tsubrel) in
+ PNodeB(r2,left2,pbright)
+ | _ -> raise jprover_bug
+ )
+ else (* rule is not relevant *)
+ PNodeA(o,left1) (* optimized termination case (1) *)
+ | PNodeB(o,PNodeA(rule,left),right1),"l" -> (* two-over-one, left *)
+(* print_endline " two-over-one, left "; *)
+ let permute_result = permute o rule ptree la tsubrel in
+ (match permute_result with
+ PNodeA(r2,left2) ->
+ let pbleft = permute_branch r addr act_addr left2 dglist (subrel,tsubrel) in
+ PNodeA(r2,pbleft)
+ | _ -> raise jprover_bug
+ )
+ | PNodeB(o,left1,PNodeA(rule,left)),"r" -> (* two-over-one, right *)
+ (* left of o is or_l free *)
+(* print_endline " two-over-one, right"; *)
+ let leftm,bool = weak_modify o left1 (subrel,tsubrel) in
+ if bool then (* rule is relevant *)
+ let permute_result = permute o rule (PNodeB(o,leftm,PNodeA(rule,left))) la tsubrel in
+ (match permute_result with
+ PNodeA(r2,left2) ->
+ let pbleft = permute_branch r addr act_addr left2 dglist (subrel,tsubrel) in
+ PNodeA(r2,pbleft)
+ | _ -> raise jprover_bug
+ )
+ else (* rule is not relevant *)
+ leftm (* optimized termination case (2) *)
+ | PNodeB(o,PNodeB(rule,left,right),right1),"l" -> (* two-over-two, left *)
+(* print_endline " two-over-two, left"; *)
+ if rule = r then (* left,right are or_l free *)
+ let permute_result = permute o rule ptree la tsubrel in
+ (match permute_result with
+ PNodeB(r2,PNodeB(r3,left3,right3),PNodeB(r4,left4,right4)) ->
+(* print_endline "permute 2-o-2, left ok"; *)
+ let leftm3,bool3 = weak_modify r3 left3 (subrel,tsubrel) in
+ let leftm4,bool4 = weak_modify r4 left4 (subrel,tsubrel) in
+ let plleft,plright =
+ if (&) bool3 bool4 then (* r3 and r4 are relevant *)
+ (permute_layer (PNodeB(r3,leftm3,right3)) dglist (subrel,tsubrel)),
+ (permute_layer (PNodeB(r4,leftm4,right4)) dglist (subrel,tsubrel))
+ else if (&) bool3 (not bool4) then (* only r3 is relevant *)
+ begin
+(* print_endline "two-over-two left: bool3 and not bool4"; *)
+ (permute_layer (PNodeB(r3,leftm3,right3)) dglist (subrel,tsubrel)),
+ leftm4
+ end
+ else if (&) (not bool3) bool4 then (* only r4 is relevant *)
+ leftm3,
+ (permute_layer (PNodeB(r4,leftm4,right4)) dglist (subrel,tsubrel))
+ else (* neither r3 nor r4 are relevant *)
+ leftm3,leftm4
+ in
+ PNodeB(r2,plleft,plright)
+ | _ -> raise jprover_bug
+ )
+ else
+ let d = next_direction addr act_addr in
+ let newadd = change_last act_addr d in
+ if d = "l" then
+ let permute_result = permute o rule ptree la tsubrel in
+ (match permute_result with
+ PNodeB(r2,left2,right2) ->
+ let pbleft = permute_branch r addr newadd left2 dglist (subrel,tsubrel) in
+ let plright = permute_layer right2 dglist (subrel,tsubrel) in
+ PNodeB(r2,pbleft,plright)
+ | _ -> raise jprover_bug
+ )
+ else (* d = "r", that is left is or_l free *)
+ let left1,bool = weak_modify rule left (subrel,tsubrel) in
+ if bool then (* rule is relevant *)
+ let permute_result =
+ permute o rule (PNodeB(o,PNodeB(rule,left1,right),right1)) la tsubrel in
+ (match permute_result with
+ PNodeB(r2,PNodeB(r3,left3,right3),right2) ->
+ let pbright = permute_branch r addr newadd right2 dglist (subrel,tsubrel) in
+ let leftm3,bool3 = weak_modify r3 left3 (subrel,tsubrel) in
+ let plleft =
+ if bool3 (* r3 relevant *) then
+ permute_layer (PNodeB(r3,leftm3,right3)) dglist (subrel,tsubrel)
+ else (* r3 redundant *)
+ leftm3
+ in
+ PNodeB(r2,plleft,pbright) (* further opt. NOT possible *)
+ | _ -> raise jprover_bug
+ )
+ else (* rule is not relevant *)
+ permute_layer (PNodeB(o,left1,right1)) dglist (subrel,tsubrel) (* further opt. possible *)
+ (* combine with orl_free *)
+ | PNodeB(o,left1,PNodeB(rule,left,right)),"r" -> (* two-over-two, right *)
+(* print_endline " two-over-two, right"; *)
+ let leftm1,bool = weak_modify o left1 (subrel,tsubrel) in (* left1 is or_l free *)
+ if bool then (* o is relevant, even after permutations *)
+ if rule = r then (* left, right or_l free *)
+ permute o rule (PNodeB(o,leftm1,PNodeB(rule,left,right))) la tsubrel
+ else
+ let d = next_direction addr act_addr in
+ let newadd = change_last act_addr d in
+ if d = "l" then
+ let permute_result =
+ permute o rule (PNodeB(o,leftm1,PNodeB(rule,left,right))) la tsubrel in
+ (match permute_result with
+ PNodeB(r2,left2,right2) ->
+ let pbleft = permute_branch r addr newadd left2 dglist (subrel,tsubrel) in
+ let plright = permute_layer right2 dglist (subrel,tsubrel) in
+ PNodeB(r2,pbleft,plright)
+ | _ -> raise jprover_bug
+ )
+ else (* d = "r", that is left is or_l free *)
+ let leftm,bool = weak_modify rule left (subrel,tsubrel) in
+ if bool then (* rule is relevant *)
+ let permute_result =
+ permute o rule (PNodeB(o,leftm1,PNodeB(rule,left,right))) la tsubrel in
+ (match permute_result with
+ PNodeB(r2,left2,right2) ->
+ let pbright = permute_branch r addr newadd right2 dglist (subrel,tsubrel) in
+ PNodeB(r2,left2,pbright) (* left2 or_l free *)
+ | _ -> raise jprover_bug
+ )
+ else (* rule is not relevant *)
+ PNodeB(o,leftm1,leftm)
+
+ else
+ leftm1
+ | _ -> raise jprover_bug
+ in
+ let rec trans_add_branch r o addr act_addr ptree dglist (subrel,tsubrel) =
+ match ptree with
+ (PEmpty| PNodeAx(_)) -> raise jprover_bug
+ | PNodeA(rule,left) ->
+ if (dgenerative rule dglist left tsubrel) then
+ let newdg = (@) [rule] dglist in
+ if rule = o then
+ begin
+(* print_endline "one-rule is o"; *)
+ permute_branch r addr act_addr ptree dglist (subrel,tsubrel)
+ end
+ else
+ begin
+(* print_endline "alpha - but not o"; *)
+ let tptree = trans_add_branch r o addr act_addr left newdg (subrel,tsubrel) in
+ permute_layer (PNodeA(rule,tptree)) dglist (subrel,tsubrel)
+ (* r may not longer be valid for rule *)
+ end
+ else
+ let tptree = trans_add_branch r o addr act_addr left dglist (subrel,tsubrel) in
+ PNodeA(rule,tptree)
+ | PNodeB(rule,left,right) ->
+ let d = next_direction addr act_addr in
+ let bool = (dgenerative rule dglist left tsubrel) in
+ if rule = o then
+ begin
+(* print_endline "two-rule is o"; *)
+ permute_branch r addr (act_addr^d) ptree dglist (subrel,tsubrel)
+ end
+ else
+ begin
+(* print_endline ("beta - but not o: address "^d); *)
+ let dbranch =
+ if d = "l" then
+ left
+ else (* d = "r" *)
+ right
+ in
+ let tptree =
+ if bool then
+ let newdg = (@) [rule] dglist in
+ (trans_add_branch r o addr (act_addr^d) dbranch newdg (subrel,tsubrel))
+ else
+ (trans_add_branch r o addr (act_addr^d) dbranch dglist (subrel,tsubrel))
+ in
+ if d = "l" then
+ permute_layer (PNodeB(rule,tptree,right)) dglist (subrel,tsubrel)
+ else (* d = "r" *)
+ begin
+(* print_endline "prob. a redundant call"; *)
+ let back = permute_layer (PNodeB(rule,left,tptree)) dglist (subrel,tsubrel) in
+(* print_endline "SURELY a redundant call"; *)
+ back
+ end
+ end
+ in
+(* print_endline "permute_layer in"; *)
+ let dummyt = mk_var_term "dummy" in
+ let r,o,addr =
+ top_addmissible_pair ptree dglist ("",Orl,dummyt,dummyt) ("",Orr,dummyt,dummyt) "" tsubrel dummyt in
+ if r = ("",Orl,dummyt,dummyt) then
+ ptree
+ else if o = ("",Orr,dummyt,dummyt) then (* Orr is a dummy for no d-gen. rule *)
+ ptree
+ else
+ let (x1,x2,x3,x4) = r
+ and (y1,y2,y3,y4) = o in
+(* print_endline ("top or_l: "^x1);
+ print_endline ("or_l address: "^addr);
+ print_endline ("top dgen-rule: "^y1); *)
+ trans_add_branch r o addr "" ptree dglist (subrel,tsubrel)
+
+(* Isolate layer and outer recursion structure *)
+(* uses weaker layer boundaries: ONLY critical inferences *)
+
+ let rec trans_layer ptree (subrel,tsubrel) =
+ let rec isol_layer ptree (subrel,tsubrel) =
+ match ptree with
+ PEmpty -> raise jprover_bug
+ | PNodeAx(inf) ->
+ ptree
+ | PNodeA((pos,rule,formula,term),left) ->
+ if List.mem rule [Allr;Impr;Negr] then
+ let tptree = trans_layer left (subrel,tsubrel) in
+ PNodeA((pos,rule,formula,term),tptree)
+ else
+ let tptree = isol_layer left (subrel,tsubrel) in
+ PNodeA((pos,rule,formula,term),tptree)
+ | PNodeB(rule,left,right) ->
+ let tptree_l = isol_layer left (subrel,tsubrel)
+ and tptree_r = isol_layer right (subrel,tsubrel) in
+ PNodeB(rule,tptree_l,tptree_r)
+ in
+ begin
+(* print_endline "trans_layer in"; *)
+ let top_tree = isol_layer ptree (subrel,tsubrel) in
+ let back = permute_layer top_tree [] (subrel,tsubrel) in
+(* print_endline "translauer out"; *)
+ back
+ end
+
+(* REAL PERMUTATION STAFF --- End *)
+
+(* build the proof tree from a list of inference rules *)
+
+ let rec unclosed subtree =
+ match subtree with
+ PEmpty -> true
+ | PNodeAx(y) -> false
+ | PNodeA(y,left) -> (unclosed left)
+ | PNodeB(y,left,right) -> (or) (unclosed left) (unclosed right)
+
+ let rec extend prooftree element =
+ match prooftree with
+ PEmpty ->
+ let (pos,rule,formula,term) = element in
+ if rule = Ax then
+ PNodeAx(element)
+ else
+ if List.mem rule [Andr; Orl; Impl] then
+ PNodeB(element,PEmpty,PEmpty)
+ else
+ PNodeA(element,PEmpty)
+ | PNodeAx(y) ->
+ PEmpty (* that's only for exhaustive pattern matching *)
+ | PNodeA(y, left) ->
+ PNodeA(y, (extend left element))
+ | PNodeB(y, left, right) ->
+ if (unclosed left) then
+ PNodeB(y, (extend left element), right)
+ else
+ PNodeB(y, left, (extend right element))
+
+ let rec bptree prooftree nodelist nax=
+ match nodelist with
+ [] -> prooftree,nax
+ | ((_,pos),(rule,formula,term))::rest -> (* kick away the first argument *)
+ let newax =
+ if rule = Ax then
+ 1
+ else
+ 0
+ in
+ bptree (extend prooftree (pos,rule,formula,term)) rest (nax+newax)
+
+
+ let bproof nodelist =
+ bptree PEmpty nodelist 0
+
+ let rec get_successor_pos treelist =
+ match treelist with
+ [] -> []
+ | f::r ->
+ (
+ match f with
+ Empty -> get_successor_pos r
+ | NodeAt(_) -> raise jprover_bug
+ | NodeA(pos,_) ->
+ pos::(get_successor_pos r)
+ )
+
+ let rec get_formula_tree ftreelist f predflag =
+ match ftreelist with
+ [] -> raise jprover_bug
+ | ftree::rest_trees ->
+ (match ftree with
+ Empty -> get_formula_tree rest_trees f predflag
+ | NodeAt(_) -> get_formula_tree rest_trees f predflag
+ | NodeA(pos,suctrees) ->
+ if predflag = "pred" then
+ if pos.pt = Gamma then
+ let succs = get_successor_pos (Array.to_list suctrees) in
+ if List.mem f succs then
+ NodeA(pos,suctrees),succs
+ else
+ get_formula_tree ((Array.to_list suctrees) @ rest_trees) f predflag
+ else
+ get_formula_tree ((Array.to_list suctrees) @ rest_trees) f predflag
+ else (* predflag = "" *)
+ if pos = f then
+ NodeA(pos,suctrees),[]
+ else
+ get_formula_tree ((Array.to_list suctrees) @ rest_trees) f predflag
+ )
+
+ let rec get_formula_treelist ftree po =
+ match po with
+ [] -> []
+ | f::r ->
+(* a posistion in po has either stype Gamma_0,Psi_0,Phi_0 (non-atomic), or it has *)
+(* ptype Alpha (or on the right), since there was a deadlock for proof reconstruction in LJ*)
+ if List.mem f.st [Phi_0;Psi_0] then
+ let (stree,_) = get_formula_tree [ftree] f "" in
+ stree::(get_formula_treelist ftree r)
+ else
+ if f.st = Gamma_0 then
+ let (predtree,succs) = get_formula_tree [ftree] f "pred" in
+ let new_po = list_diff r succs in
+ predtree::(get_formula_treelist ftree new_po)
+ else
+ if f.pt = Alpha then (* same as first case, or on the right *)
+ let (stree,_) = get_formula_tree [ftree] f "" in
+ stree::(get_formula_treelist ftree r)
+ else raise (Invalid_argument "Jprover bug: non-admissible open position")
+
+ let rec build_formula_rel dir_treelist slist predname =
+
+ let rec build_renamed_gamma_rel dtreelist predname posname d =
+ match dtreelist with
+ [] -> [],[]
+ | (x,ft)::rdtlist ->
+ let rest_rel,rest_ren = build_renamed_gamma_rel rdtlist predname posname d in
+ (
+ match ft with
+ Empty -> (* may have empty successors due to purity in former reconstruction steps *)
+ rest_rel,rest_ren
+ | NodeAt(_) ->
+ raise jprover_bug (* gamma_0 position never is atomic *)
+ | NodeA(spos,suctrees) ->
+ if List.mem spos.name slist then
+(* the gamma_0 position is really unsolved *)
+(* this is only relevant for the gamma_0 positions in po *)
+ let new_name = (posname^"_"^spos.name) (* make new unique gamma name *) in
+ let new_srel_el = ((predname,new_name),d)
+ and new_rename_el = (spos.name,new_name) (* gamma_0 position as key first *) in
+ let (srel,sren) = build_formula_rel [(x,ft)] slist new_name in
+ ((new_srel_el::srel) @ rest_rel),((new_rename_el::sren) @ rest_ren)
+ else
+ rest_rel,rest_ren
+ )
+
+
+ in
+ match dir_treelist with
+ [] -> [],[]
+ | (d,f)::dir_r ->
+ let (rest_rel,rest_renlist) = build_formula_rel dir_r slist predname in
+ match f with
+ Empty ->
+ print_endline "Hello, an empty subtree!!!!!!";
+ rest_rel,rest_renlist
+ | NodeAt(pos) ->
+ (((predname,pos.name),d)::rest_rel),rest_renlist
+ | NodeA(pos,suctrees) ->
+ (match pos.pt with
+ Alpha | Beta ->
+ let dtreelist =
+ if (pos.pt = Alpha) & (pos.op = Neg) then
+ [(1,suctrees.(0))]
+ else
+ let st1 = suctrees.(0)
+ and st2 = suctrees.(1) in
+ [(1,st1);(2,st2)]
+ in
+ let (srel,sren) = build_formula_rel dtreelist slist pos.name in
+ ((((predname,pos.name),d)::srel) @ rest_rel),(sren @ rest_renlist)
+ | Delta ->
+ let st1 = suctrees.(0) in
+ let (srel,sren) = build_formula_rel [(1,st1)] slist pos.name in
+ ((((predname,pos.name),d)::srel) @ rest_rel),(sren @ rest_renlist)
+ | Psi| Phi ->
+ let succlist = Array.to_list suctrees in
+ let dtreelist = (List.map (fun x -> (d,x)) succlist) in
+ let (srel,sren) = build_formula_rel dtreelist slist predname in
+ (srel @ rest_rel),(sren @ rest_renlist)
+ | Gamma ->
+ let n = Array.length suctrees
+ and succlist = (Array.to_list suctrees) in
+ let dtreelist = (List.map (fun x -> (1,x)) succlist) in
+(* if (nonemptys suctrees 0 n) = 1 then
+ let (srel,sren) = build_formula_rel dtreelist slist pos.name in
+ ((((predname,pos.name),d)::srel) @ rest_rel),(sren @ rest_renlist)
+ else (* we have more than one gamma instance, which means renaming *)
+*)
+ let (srel,sren) = build_renamed_gamma_rel dtreelist predname pos.name d in
+ (srel @ rest_rel),(sren @ rest_renlist)
+ | PNull ->
+ raise jprover_bug
+ )
+
+ let rec rename_gamma ljmc_proof rename_list =
+ match ljmc_proof with
+ [] -> []
+ | ((inst,pos),(rule,formula,term))::r ->
+ if List.mem rule [Alll;Exr] then
+ let new_gamma = List.assoc inst rename_list in
+ ((inst,new_gamma),(rule,formula,term))::(rename_gamma r rename_list)
+ else
+ ((inst,pos),(rule,formula,term))::(rename_gamma r rename_list)
+
+ let rec compare_pair (s,sf) list =
+ if list = [] then
+ list
+ else
+ let (s_1,sf_1),restlist = (List.hd list),(List.tl list) in
+ if sf = s_1 then
+ (@) [(s,sf_1)] (compare_pair (s,sf) restlist)
+ else
+ compare_pair (s,sf) restlist
+
+ let rec compare_pairlist list1 list2 =
+ if list1 = [] then
+ list1
+ else
+ let (s1,sf1),restlist1 = (List.hd list1),(List.tl list1) in
+ (@) (compare_pair (s1,sf1) list2) (compare_pairlist restlist1 list2)
+
+ let rec trans_rec pairlist translist =
+ let tlist = compare_pairlist pairlist translist in
+ if tlist = [] then
+ translist
+ else
+ (@) (trans_rec pairlist tlist) translist
+
+ let transitive_closure subrel =
+ let pairlist,nlist = List.split subrel in
+ trans_rec pairlist pairlist
+
+ let pt ptree subrel =
+ let tsubrel = transitive_closure subrel in
+ let transptree = trans_layer ptree (subrel,tsubrel) in
+ print_endline "";
+ fst (modify transptree (subrel,tsubrel))
+(* let mtree = fst (modify transptree (subrel,tsubrel)) in *)
+(* pretty_print mtree ax *)
+
+ let rec make_node_list ljproof =
+ match ljproof with
+ PEmpty ->
+ raise jprover_bug
+ | PNodeAx((pos,inf,form,term)) ->
+ [(("",pos),(inf,form,term))]
+ | PNodeA((pos,inf,form,term),left) ->
+ let left_list = make_node_list left in
+ (("",pos),(inf,form,term))::left_list
+ | PNodeB((pos,inf,form,term),left,right) ->
+ let left_list = make_node_list left
+ and right_list = make_node_list right in
+ (("",pos),(inf,form,term))::(left_list @ right_list)
+
+ let permute_ljmc ftree po slist ljmc_proof =
+ (* ftree/po are the formula tree / open positions of the sequent that caused deadlock and permutation *)
+(* print_endline "!!!!!!!!!!!!!Permutation TO DO!!!!!!!!!"; *)
+ (* the open positions in po are either phi_0, psi_0, or gamma_0 positions *)
+ (* since proof reconstruction was a deadlock in LJ *)
+ let po_treelist = get_formula_treelist ftree po in
+ let dir_treelist = List.map (fun x -> (1,x)) po_treelist in
+ let (formula_rel,rename_list) = build_formula_rel dir_treelist slist "dummy" in
+ let renamed_ljmc_proof = rename_gamma ljmc_proof rename_list in
+ let (ptree,ax) = bproof renamed_ljmc_proof in
+ let ljproof = pt ptree formula_rel in
+ (* this is a direct formula relation, comprising left/right subformula *)
+ begin
+(* print_treelist po_treelist; *)
+(* print_endline "";
+ print_endline "";
+*)
+(* print_triplelist formula_rel; *)
+(* print_endline "";
+ print_endline "";
+ tt ljproof;
+*)
+(* print_pairlist rename_list; *)
+(* print_endline "";
+ print_endline "";
+*)
+ make_node_list ljproof
+ end
+
+(************** PROOF RECONSTRUCTION without redundancy deletion ******************************)
+
+ let rec init_unsolved treelist =
+ match treelist with
+ [] -> []
+ | f::r ->
+ begin match f with
+ Empty -> []
+ | NodeAt(pos) ->
+ (pos.name)::(init_unsolved r)
+ | NodeA(pos,suctrees) ->
+ let new_treelist = (Array.to_list suctrees) @ r in
+ (pos.name)::(init_unsolved new_treelist)
+ end
+
+(* only the unsolved positions will be represented --> skip additional root position *)
+
+ let build_unsolved ftree =
+ match ftree with
+ Empty | NodeAt _ ->
+ raise jprover_bug
+ | NodeA(pos,suctrees) ->
+ ((pos.name),init_unsolved (Array.to_list suctrees))
+
+(*
+ let rec collect_variables tree_list =
+ match tree_list with
+ [] -> []
+ | f::r ->
+ begin match f with
+ Empty -> []
+ | NodeAt(pos) ->
+ if pos.st = Gamma_0 then
+ pos.name::collect_variables r
+ else
+ collect_variables r
+ | NodeA(pos,suctrees) ->
+ let new_tree_list = (Array.to_list suctrees) @ r in
+ if pos.st = Gamma_0 then
+ pos.name::collect_variables new_tree_list
+ else
+ collect_variables new_tree_list
+ end
+
+ let rec extend_sigmaQ sigmaQ vlist =
+ match vlist with
+ [] -> []
+ | f::r ->
+ let vf = mk_var_term f in
+ if List.exists (fun x -> (fst x = vf)) sigmaQ then
+ extend_sigmaQ sigmaQ r
+ else
+(* first and second component are var terms in meta-prl *)
+ [(vf,vf)] @ (extend_sigmaQ sigmaQ r)
+
+ let build_sigmaQ sigmaQ ftree =
+ let vlist = collect_variables [ftree] in
+ sigmaQ @ (extend_sigmaQ sigmaQ vlist)
+*)
+
+(* subformula relation subrel is assumed to be represented in pairs
+ (a,b) *)
+
+ let rec delete e list = (* e must not necessarily occur in list *)
+ match list with
+ [] -> [] (* e must not necessarily occur in list *)
+ | first::rest ->
+ if e = first then
+ rest
+ else
+ first::(delete e rest)
+
+ let rec key_delete fname pos_list = (* in key_delete, f is a pos name (key) but sucs is a list of positions *)
+ match pos_list with
+ [] -> [] (* the position with name f must not necessarily occur in pos_list *)
+ | f::r ->
+ if fname = f.name then
+ r
+ else
+ f::(key_delete fname r)
+
+ let rec get_roots treelist =
+ match treelist with
+ [] -> []
+ | f::r ->
+ match f with
+ Empty -> (get_roots r) (* Empty is posible below alpha-nodes after purity *)
+ | NodeAt(pos) -> pos::(get_roots r)
+ | NodeA(pos,trees) -> pos::(get_roots r)
+
+ let rec comp_ps padd ftree =
+ match ftree with
+ Empty -> raise (Invalid_argument "Jprover bug: empty formula tree")
+ | NodeAt(pos) ->
+ []
+ | NodeA(pos,strees) ->
+ match padd with
+ [] -> get_roots (Array.to_list strees)
+ | f::r ->
+ if r = [] then
+ pos::(comp_ps r (Array.get strees (f-1)))
+ else
+ comp_ps r (Array.get strees (f-1))
+
+(* computes a list: first element predecessor, next elements successoes of p *)
+
+ let tpredsucc p ftree =
+ let padd = p.address in
+ comp_ps padd ftree
+
+(* set an element in an array, without side effects *)
+
+ let myset array int element =
+ let length = Array.length array in
+ let firstpart = Array.sub array 0 (int) in
+ let secondpart = Array.sub array (int+1) (length-(int+1)) in
+ (Array.append firstpart (Array.append [|element|] secondpart))
+
+ let rec compute_open treelist slist =
+ match treelist with
+ [] -> []
+ | first::rest ->
+ let elements =
+ match first with
+ Empty -> []
+ | NodeAt(pos) ->
+ if (List.mem (pos.name) slist) then
+ [pos]
+ else
+ []
+ | NodeA(pos,suctrees) ->
+ if (List.mem (pos.name) slist) then
+ [pos]
+ else
+ compute_open (Array.to_list suctrees) slist
+ in
+ elements @ (compute_open rest slist)
+
+ let rec select_connection pname connections slist =
+ match connections with
+ [] -> ("none","none")
+ | f::r ->
+ let partner =
+ if (fst f) = pname then
+ (snd f)
+ else
+ if (snd f) = pname then
+ (fst f)
+ else
+ "none"
+ in
+ if ((partner = "none") or (List.mem partner slist)) then
+ select_connection pname r slist
+ else
+ f
+
+ let rec replace_element element element_set redord =
+ match redord with
+ [] -> raise jprover_bug (* element occurs in redord *)
+ | (f,fset)::r ->
+ if f = element then
+ (f,element_set)::r
+ else
+ (f,fset)::(replace_element element element_set r)
+
+ let rec collect_succ_sets sucs redord =
+ match redord with
+ [] -> StringSet.empty
+ | (f,fset)::r ->
+ let new_sucs = key_delete f sucs in
+ if (List.length sucs) = (List.length new_sucs) then (* position with name f did not occur in sucs -- no deletion *)
+ (collect_succ_sets sucs r)
+ else
+ StringSet.union (StringSet.add f fset) (collect_succ_sets new_sucs r)
+
+ let replace_ordering psucc_name sucs redord =
+ let new_psucc_set = collect_succ_sets sucs redord in
+(* print_string_set new_psucc_set; *)
+ replace_element psucc_name new_psucc_set redord
+
+ let rec update pname redord =
+ match redord with
+ [] -> []
+ | (f,fset)::r ->
+ if pname=f then
+ r
+ else
+ (f,fset)::(update pname r)
+
+(* rule construction *)
+
+ let rec selectQ_rec spos_var csigmaQ =
+ match csigmaQ with
+ [] -> mk_var_term spos_var (* dynamic completion of csigmaQ *)
+ | (var,term)::r ->
+ if spos_var=var then
+ term
+ else
+ selectQ_rec spos_var r
+
+ let selectQ spos_name csigmaQ =
+ let spos_var = spos_name^"_jprover" in
+ selectQ_rec spos_var csigmaQ
+
+ let apply_sigmaQ term sigmaQ =
+ let sigma_vars,sigma_terms = List.split sigmaQ in
+ (subst term sigma_vars sigma_terms)
+
+ let build_rule pos spos csigmaQ orr_flag calculus =
+ let inst_label = apply_sigmaQ (pos.label) csigmaQ in
+ match pos.op,pos.pol with
+ Null,_ -> raise (Invalid_argument "Jprover: no rule")
+ | At,O -> Ax,(inst_label),xnil_term (* to give back a term *)
+ | At,I -> Ax,(inst_label),xnil_term
+ | And,O -> Andr,(inst_label),xnil_term
+ | And,I -> Andl,(inst_label),xnil_term
+ | Or,O ->
+ if calculus = "LJ" then
+ let or_rule =
+ if orr_flag = 1 then
+ Orr1
+ else
+ Orr2
+ in
+ or_rule,(inst_label),xnil_term
+ else
+ Orr,(inst_label),xnil_term
+ | Or,I -> Orl,(inst_label),xnil_term
+ | Neg,O -> Negr,(inst_label),xnil_term
+ | Neg,I -> Negl,(inst_label),xnil_term
+ | Imp,O -> Impr,(inst_label),xnil_term
+ | Imp,I -> Impl,(inst_label),xnil_term
+ | All,I -> Alll,(inst_label),(selectQ spos.name csigmaQ) (* elements of csigmaQ is (string * term) *)
+ | Ex,O -> Exr,(inst_label), (selectQ spos.name csigmaQ)
+ | All,O -> Allr,(inst_label),(mk_string_term jprover_op spos.name) (* must be a proper term *)
+ | Ex,I -> Exl,(inst_label),(mk_string_term jprover_op spos.name) (* must be a proper term *)
+
+
+(* %%%%%%%%%%%%%%%%%%%% Split begin %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+
+ let rec nonemptys treearray j n =
+ if j = n then
+ 0
+ else
+ let count =
+ if (Array.get treearray j) <> Empty then
+ 1
+ else
+ 0
+ in
+ count + (nonemptys treearray (j+1) n)
+
+ let rec collect_pure ftreelist (flist,slist) =
+
+ let rec collect_itpure ftree (flist,slist) =
+ match ftree with
+ Empty -> (* assumed that not all brother trees are Empty *)
+ []
+ | NodeAt(pos) -> (* that may NOT longer be an inner node *)
+ if ((List.mem (pos.name) flist) or (List.mem (pos.name) slist)) then
+ []
+ else
+ [pos]
+ | NodeA(pos,treearray) ->
+ collect_pure (Array.to_list treearray) (flist,slist)
+ in
+ match ftreelist with
+ [] -> []
+ | f::r ->
+ (collect_itpure f (flist,slist)) @ (collect_pure r (flist,slist))
+
+ let rec update_list testlist list =
+ match testlist with
+ [] -> list
+ | f::r ->
+ let newlist = delete f list in (* f may not occur in list; then newlist=list *)
+ update_list r newlist
+
+ let rec update_pairlist p pairlist =
+ match pairlist with
+ [] -> []
+ | f::r ->
+ if ((fst f) = p) or ((snd f) = p) then
+ update_pairlist p r
+ else
+ f::(update_pairlist p r)
+
+ let rec update_connections slist connections =
+ match slist with
+ [] -> connections
+ | f::r ->
+ let connew = update_pairlist f connections in
+ update_connections r connew
+
+ let rec update_redord delset redord = (* delset is the set of positions to be deleted *)
+ match redord with
+ [] -> []
+ | (f,fset)::r ->
+ if (StringSet.mem f delset) then
+ update_redord delset r (* delete all key elements f from redord which are in delset *)
+ else
+ let new_fset = StringSet.diff fset delset in (* no successor of f from delset should remain in fset *)
+ (f,new_fset)::(update_redord delset r)
+
+ let rec get_position_names treelist =
+ match treelist with
+ [] -> []
+ | deltree::rests ->
+ match deltree with
+ Empty -> get_position_names rests
+ | NodeAt(pos) ->
+ (pos.name)::get_position_names rests
+ | NodeA(pos,strees) ->
+ (pos.name)::(get_position_names ((Array.to_list strees) @ rests))
+
+ let rec slist_to_set slist =
+ match slist with
+ [] ->
+ StringSet.empty
+ | f::r ->
+ StringSet.add f (slist_to_set r)
+
+ let rec print_purelist pr =
+ match pr with
+ [] ->
+ begin
+ print_string ".";
+ print_endline " ";
+ end
+ | f::r ->
+ print_string ((f.name)^", ");
+ print_purelist r
+
+ let update_relations deltree redord connections unsolved_list =
+ let pure_names = get_position_names [deltree] in
+ begin
+(* print_ftree deltree;
+ Format.open_box 0;
+ print_endline " ";
+ print_stringlist pure_names;
+ Format.force_newline ();
+ Format.print_flush ();
+*)
+ let rednew = update_redord (slist_to_set pure_names) redord
+ and connew = update_connections pure_names connections
+ and unsolnew = update_list pure_names unsolved_list in
+ (rednew,connew,unsolnew)
+ end
+
+ let rec collect_qpos ftreelist uslist =
+ match ftreelist with
+ [] -> [],[]
+ | ftree::rest ->
+ match ftree with
+ Empty ->
+ collect_qpos rest uslist
+ | NodeAt(pos) ->
+ let (rest_delta,rest_gamma) = collect_qpos rest uslist in
+ if (pos.st = Gamma_0) & (List.mem pos.name uslist) then
+ rest_delta,(pos.name::rest_gamma)
+ else
+ if (pos.st = Delta_0) & (List.mem pos.name uslist) then
+ (pos.name::rest_delta),rest_gamma
+ else
+ rest_delta,rest_gamma
+ | NodeA(pos,suctrees) ->
+ let (rest_delta,rest_gamma) = collect_qpos ((Array.to_list suctrees) @ rest) uslist in
+ if (pos.st = Gamma_0) & (List.mem pos.name uslist) then
+ rest_delta,(pos.name::rest_gamma)
+ else
+ if (pos.st = Delta_0) & (List.mem pos.name uslist) then
+ (pos.name::rest_delta),rest_gamma
+ else
+ rest_delta,rest_gamma
+
+ let rec do_split gamma_diff sigmaQ =
+ match sigmaQ with
+ [] -> []
+ | (v,term)::r ->
+ if (List.mem (String.sub v 0 (String.index v '_')) gamma_diff) then
+ do_split gamma_diff r
+ else
+ (v,term)::(do_split gamma_diff r)
+
+(* make a term list out of a bterm list *)
+
+ let rec collect_subterms = function
+ [] -> []
+ | bt::r ->
+ let dbt = dest_bterm bt in
+ (dbt.bterm)::(collect_subterms r)
+
+ (*: Bug! :*)
+(*: let rec collect_delta_terms = function
+ [] -> []
+ | t::r ->
+ let dt = dest_term t in
+ let top = dt.term_op
+ and tterms = dt.term_terms in
+ let dop = dest_op top in
+ let don = dest_opname dop.op_name in
+ match don with
+ [] ->
+ let sub_terms = collect_subterms tterms in
+ collect_delta_terms (sub_terms @ r)
+ | op1::opr ->
+ if op1 = "jprover" then
+ match opr with
+ [] -> raise (Invalid_argument "Jprover: delta position missing")
+ | delta::_ ->
+ delta::(collect_delta_terms r)
+ else
+ let sub_terms = collect_subterms tterms in
+ collect_delta_terms (sub_terms @ r)
+:*)
+
+ let rec collect_delta_terms = function
+ [] -> []
+ | t::r ->
+ let dt = dest_term t in
+ let top = dt.term_op
+ and tterms = dt.term_terms in
+ let dop = dest_op top in
+ let don = dest_opname dop.op_name in
+ let doa = dest_param dop.op_params in
+ match don with
+ [] ->
+ let sub_terms = collect_subterms tterms in
+ collect_delta_terms (sub_terms @ r)
+ | op1::opr ->
+ if op1 = "jprover" then
+ match doa with
+ [] -> raise (Invalid_argument "Jprover: delta position missing")
+ | String delta::_ ->
+ delta::(collect_delta_terms r)
+ | _ -> raise (Invalid_argument "Jprover: delta position error")
+ else
+ let sub_terms = collect_subterms tterms in
+ collect_delta_terms (sub_terms @ r)
+
+
+
+ let rec check_delta_terms (v,term) ass_delta_diff dterms =
+ match ass_delta_diff with
+ [] -> term,[]
+ | (var,dname)::r ->
+ if List.mem dname dterms then
+ let new_var =
+ if var = "" then
+ v
+ else
+ var
+ in
+ let replace_term = mk_string_term jprover_op dname in
+ let next_term = var_subst term replace_term new_var in
+ let (new_term,next_diffs) = check_delta_terms (v,next_term) r dterms in
+ (new_term,((new_var,dname)::next_diffs))
+ else
+ let (new_term,next_diffs) = check_delta_terms (v,term) r dterms in
+ (new_term,((var,dname)::next_diffs))
+
+
+ let rec localize_sigma zw_sigma ass_delta_diff =
+ match zw_sigma with
+ [] -> []
+ | (v,term)::r ->
+ let dterms = collect_delta_terms [term] in
+ let (new_term,new_ass_delta_diff) = check_delta_terms (v,term) ass_delta_diff dterms in
+ (v,new_term)::(localize_sigma r new_ass_delta_diff)
+
+ let subst_split ft1 ft2 ftree uslist1 uslist2 uslist sigmaQ =
+ let delta,gamma = collect_qpos [ftree] uslist
+ and delta1,gamma1 = collect_qpos [ft1] uslist1
+ and delta2,gamma2 = collect_qpos [ft2] uslist2 in
+ let delta_diff1 = list_diff delta delta1
+ and delta_diff2 = list_diff delta delta2
+ and gamma_diff1 = list_diff gamma gamma1
+ and gamma_diff2 = list_diff gamma gamma2 in
+ let zw_sigma1 = do_split gamma_diff1 sigmaQ
+ and zw_sigma2 = do_split gamma_diff2 sigmaQ in
+ let ass_delta_diff1 = List.map (fun x -> ("",x)) delta_diff1
+ and ass_delta_diff2 = List.map (fun x -> ("",x)) delta_diff2 in
+ let sigmaQ1 = localize_sigma zw_sigma1 ass_delta_diff1
+ and sigmaQ2 = localize_sigma zw_sigma2 ass_delta_diff2 in
+ (sigmaQ1,sigmaQ2)
+
+ let rec reduce_tree addr actual_node ftree beta_flag =
+ match addr with
+ [] -> (ftree,Empty,actual_node,beta_flag)
+ | a::radd ->
+ match ftree with
+ Empty ->
+ print_endline "Empty purity tree";
+ raise jprover_bug
+ | NodeAt(_) ->
+ print_endline "Atom purity tree";
+ raise jprover_bug
+ | NodeA(pos,strees) ->
+(* print_endline pos.name; *)
+ (* the associated node occurs above f (or the empty address) and hence, is neither atom nor empty tree *)
+
+ let nexttree = (Array.get strees (a-1)) in
+ if (nonemptys strees 0 (Array.length strees)) < 2 then
+ begin
+(* print_endline "strees 1 or non-empties < 2"; *)
+ let (ft,dt,an,bf) = reduce_tree radd actual_node nexttree beta_flag in
+ let nstrees = myset strees (a-1) ft in
+(* print_endline ("way back "^pos.name); *)
+ (NodeA(pos,nstrees),dt,an,bf)
+ end
+ else (* nonemptys >= 2 *)
+ begin
+(* print_endline "nonempties >= 2 "; *)
+ let (new_act,new_bf) =
+ if pos.pt = Beta then
+ (actual_node,true)
+ else
+ ((pos.name),false)
+ in
+ let (ft,dt,an,bf) = reduce_tree radd new_act nexttree new_bf in
+ if an = pos.name then
+ let nstrees = myset strees (a-1) Empty in
+(* print_endline ("way back assocnode "^pos.name); *)
+ (NodeA(pos,nstrees),nexttree,an,bf)
+ else (* has been replaced / will be replaced below / above pos *)
+ let nstrees = myset strees (a-1) ft in
+(* print_endline ("way back "^pos.name); *)
+ (NodeA(pos,nstrees),dt,an,bf)
+ end
+
+ let rec purity ftree redord connections unsolved_list =
+
+ let rec purity_reduction pr ftree redord connections unsolved_list =
+ begin
+(* Format.open_box 0;
+ print_endline " ";
+ print_purelist pr;
+ Format.force_newline ();
+ Format.print_flush ();
+*)
+ match pr with
+ [] -> (ftree,redord,connections,unsolved_list)
+ | f::r ->
+(* print_endline ("pure position "^(f.name)); *)
+ let (ftnew,deltree,assocn,beta_flag) = reduce_tree f.address "" ftree false
+ in
+(* print_endline ("assoc node "^assocn); *)
+ if assocn = "" then
+ (Empty,[],[],[]) (* should not occur in the final version *)
+ else
+ let (rednew,connew,unsolnew) = update_relations deltree redord connections unsolved_list in
+ begin
+(* Format.open_box 0;
+ print_endline " ";
+ print_pairlist connew;
+ Format.force_newline ();
+ Format.print_flush ();
+*)
+ if beta_flag = true then
+ begin
+(* print_endline "beta_flag true"; *)
+ purity ftnew rednew connew unsolnew
+ (* new pure positions may occur; old ones may not longer exist *)
+ end
+ else
+ purity_reduction r ftnew rednew connew unsolnew (* let's finish the old pure positions *)
+ end
+ end
+
+ in
+ let flist,slist = List.split connections in
+ let pr = collect_pure [ftree] (flist,slist) in
+ purity_reduction pr ftree redord connections unsolved_list
+
+ let rec betasplit addr ftree redord connections unsolved_list =
+ match ftree with
+ Empty ->
+ print_endline "bsplit Empty tree";
+ raise jprover_bug
+ | NodeAt(_) ->
+ print_endline "bsplit Atom tree";
+ raise jprover_bug (* the beta-node should actually occur! *)
+ | NodeA(pos,strees) ->
+ match addr with
+ [] -> (* we are at the beta node under consideration *)
+ let st1tree = (Array.get strees 0)
+ and st2tree = (Array.get strees 1) in
+ let (zw1red,zw1conn,zw1uslist) = update_relations st2tree redord connections unsolved_list
+ and (zw2red,zw2conn,zw2uslist) = update_relations st1tree redord connections unsolved_list in
+ ((NodeA(pos,[|st1tree;Empty|])),zw1red,zw1conn,zw1uslist),
+ ((NodeA(pos,[|Empty;st2tree|])),zw2red,zw2conn,zw2uslist)
+ | f::rest ->
+ let nexttree = Array.get strees (f-1) in
+ let (zw1ft,zw1red,zw1conn,zw1uslist),(zw2ft,zw2red,zw2conn,zw2uslist) =
+ betasplit rest nexttree redord connections unsolved_list in
+(* let scopytrees = Array.copy strees in *)
+ let zw1trees = myset strees (f-1) zw1ft
+ and zw2trees = myset strees (f-1) zw2ft in
+ (NodeA(pos,zw1trees),zw1red,zw1conn,zw1uslist),(NodeA(pos,zw2trees),zw2red,zw2conn,zw2uslist)
+
+
+
+
+ let split addr pname ftree redord connections unsolved_list opt_bproof =
+ let (opt_bp1,min_con1),(opt_bp2,min_con2) = split_permutation pname opt_bproof in
+ begin
+(*
+ print_endline "Beta proof 1: ";
+ print_endline "";
+ print_beta_proof opt_bp1;
+ print_endline "";
+ print_endline ("Beta proof 1 connections: ");
+ Format.open_box 0;
+ print_pairlist min_con1;
+ print_endline ".";
+ Format.print_flush();
+ print_endline "";
+ print_endline "";
+ print_endline "Beta proof 2: ";
+ print_endline "";
+ print_beta_proof opt_bp2;
+ print_endline "";
+ print_endline ("Beta proof 2 connections: ");
+ Format.open_box 0;
+ print_pairlist min_con2;
+ print_endline ".";
+ Format.print_flush();
+ print_endline "";
+*)
+ let (zw1ft,zw1red,zw1conn,zw1uslist),(zw2ft,zw2red,zw2conn,zw2uslist) =
+ betasplit addr ftree redord connections unsolved_list in
+(* zw1conn and zw2conn are not longer needed when using beta proofs *)
+(* print_endline "betasp_out"; *)
+ let ft1,red1,conn1,uslist1 = purity zw1ft zw1red min_con1 zw1uslist in
+(* print_endline "purity_one_out"; *)
+ let ft2,red2,conn2,uslist2 = purity zw2ft zw2red min_con2 zw2uslist in
+(* print_endline "purity_two_out"; *)
+(* again, min_con1 = conn1 and min_con2 = conn2 should hold *)
+ begin
+(* print_endline "";
+ print_endline "";
+ print_endline ("Purity 1 connections: ");
+ Format.open_box 0;
+ print_pairlist conn1;
+ print_endline ".";
+ print_endline "";
+ Format.print_flush();
+ print_endline "";
+ print_endline "";
+ print_endline ("Purity 2 connections: ");
+ Format.open_box 0;
+ print_pairlist conn2;
+ print_endline ".";
+ print_endline "";
+ Format.print_flush();
+ print_endline "";
+ print_endline "";
+*)
+ (ft1,red1,conn1,uslist1,opt_bp1),(ft2,red2,conn2,uslist2,opt_bp2)
+ end
+ end
+
+
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Splitting end %%%%%%%%%%%%%%%% *)
+
+
+(* for wait labels we collect all solved atoms with pol=0 *)
+
+ let rec collect_solved_O_At ftreelist slist =
+ match ftreelist with
+ [] ->
+ []
+ | f::r ->
+ match f with
+ Empty -> (* may become possible after purity *)
+ collect_solved_O_At r slist
+ | NodeAt(pos) ->
+ if ((List.mem (pos.name) slist) or (pos.pol = I)) then (* recall slist is the unsolved list *)
+ collect_solved_O_At r slist
+ else
+ (* here, we have pos solved and pos.pol = O) *)
+ pos::(collect_solved_O_At r slist)
+ | NodeA(pos,treearray) ->
+ collect_solved_O_At ((Array.to_list treearray) @ r) slist
+
+ let rec red_ord_block pname redord =
+ match redord with
+ [] -> false
+ | (f,fset)::r ->
+ if ((f = pname) or (not (StringSet.mem pname fset))) then
+ red_ord_block pname r
+ else
+ true (* then, we have (StringSet.mem pname fset) *)
+
+ let rec check_wait_succ_LJ faddress ftree =
+ match ftree with
+ Empty -> raise jprover_bug
+ | NodeAt(pos) -> raise jprover_bug (* we have an gamma_0 position or an or-formula *)
+ | NodeA(pos,strees) ->
+ match faddress with
+ [] ->
+ if pos.op = Or then
+ match (strees.(0),strees.(1)) with
+ (Empty,Empty) -> raise (Invalid_argument "Jprover: redundancies occur")
+ | (Empty,_) -> (false,2) (* determines the Orr2 rule *)
+ | (_,Empty) -> (false,1) (* determines the Orr1 ruke *)
+ | (_,_) -> (true,0) (* wait-label is set *)
+ else
+ (false,0)
+ | f::r ->
+ if r = [] then
+ if (pos.pt = Gamma) & ((nonemptys strees 0 (Array.length strees)) > 1) then
+ (true,0) (* we are at a gamma position (exr) with one than one successor -- wait label in LJ*)
+ else
+ check_wait_succ_LJ r (Array.get strees (f-1))
+ else
+ check_wait_succ_LJ r (Array.get strees (f-1))
+
+ let blocked f po redord ftree connections slist logic calculus opt_bproof =
+(* print_endline ("Blocking check "^(f.name)); *)
+ if (red_ord_block (f.name) redord) then
+ begin
+(* print_endline "wait-1 check positive"; *)
+ true,0
+ end
+ else
+ if logic = "C" then
+ false,0 (* ready, in C only redord counts *)
+ else
+ let pa_O = collect_solved_O_At [ftree] slist (* solved atoms in ftree *)
+ and po_test = (delete f po) in
+ if calculus = "LJmc" then (* we provide dynamic wait labels for both sequent calculi *)
+(* print_endline "wait-2 check"; *)
+ if (f.st = Psi_0) & (f.pt <> PNull) &
+ ((pa_O <> []) or (List.exists (fun x -> x.pol = O) po_test)) then
+ begin
+(* print_endline "wait-2 positive"; *)
+ true,0 (* wait_2 label *)
+ end
+ else
+ begin
+(* print_endline "wait-2 negative"; *)
+ false,0
+ end
+ else (* calculus is supposed to be LJ *)
+ if calculus = "LJ" then
+ if ((f.st = Phi_0) & ((f.op=Neg) or (f.op=Imp)) &
+ ((pa_O <> []) or (List.exists (fun x -> x.pol = O) po_test))
+ )
+ (* this would cause an impl or negl rule with an non-empty succedent *)
+ then
+ if (f.op=Neg) then
+ true,0
+ else (* (f.op=Imp) *)
+ (* In case of an impl rule on A => B, the wait_label must NOT be set
+ iff all succedent formulae depend exclusively on B. For this, we
+ perform a split operation and determine, if in the A-subgoal
+ all succedent formulae are pure, i.e.~have been deleted from treds.
+ Otherwise, in case of A-dependent succedent formulae, the
+ wait_label must be set.
+ *)
+ let ((_,min_con1),_) = split_permutation f.name opt_bproof in
+ let slist_fake = delete f.name slist in
+ let ((zw1ft,zw1red,_,zw1uslist),_) =
+ betasplit (f.address) ftree redord connections slist_fake in
+ let ft1,_,_,uslist1 = purity zw1ft zw1red min_con1 zw1uslist in
+(* print_endline "wait label purity_one_out"; *)
+ let ft1_root = (List.hd (List.tl (tpredsucc f ft1))) in
+(* print_endline ("wait-root "^(ft1_root.name)); *)
+ let po_fake = compute_open [ft1] uslist1 in
+ let po_fake_test = delete ft1_root po_fake
+ and pa_O_fake = collect_solved_O_At [ft1] uslist1 in
+(* print_purelist (po_fake_test @ pa_O_fake); *)
+ if ((pa_O_fake <> []) or (List.exists (fun x -> x.pol = O) po_fake_test)) then
+ true,0
+ else
+ false,0
+ else
+ if ((f.pol=O) & ((f.st=Gamma_0) or (f.op=Or))) then
+ let (bool,orr_flag) = check_wait_succ_LJ f.address ftree in
+ (bool,orr_flag)
+ (* here is determined if orr1 or orr2 will be performed, provided bool=false) *)
+ (* orr_flag can be 1 or 2 *)
+ else
+ false,0
+ else
+ raise (Invalid_argument "Jprover: calculus should be LJmc or LJ")
+
+ let rec get_beta_preference list actual =
+ match list with
+ [] -> actual
+ | (f,int)::r ->
+ if f.op = Imp then
+ (f,int)
+ else
+(* if f.op = Or then
+ get_beta_preference r (f,int)
+ else
+*)
+ get_beta_preference r actual
+
+ exception Gamma_deadlock
+
+ let rec select_pos search_po po redord ftree connections slist logic calculus candidates
+ opt_bproof =
+ match search_po with
+ [] ->
+ (match candidates with
+ [] ->
+ if calculus = "LJ" then
+ raise Gamma_deadlock (* permutation may be necessary *)
+ else
+ raise (Invalid_argument "Jprover bug: overall deadlock") (* this case should not occur *)
+ | c::rest ->
+ get_beta_preference (c::rest) c
+ )
+ | f::r -> (* there exist an open position *)
+ let (bool,orr_flag) = (blocked f po redord ftree connections slist logic calculus
+ opt_bproof)
+ in
+ if (bool = true) then
+ select_pos r po redord ftree connections slist logic calculus candidates opt_bproof
+ else
+ if f.pt = Beta then
+ (* search for non-splitting rules first *)
+(* let beta_candidate =
+ if candidates = []
+ then
+ [(f,orr_flag)]
+ else
+ !!!! but preserve first found candidate !!!!!!!
+ candidates
+ in
+ !!!!!!! this strategy is not sure the best -- back to old !!!!!!!!!
+*)
+ select_pos r po redord ftree connections slist logic calculus
+ ((f,orr_flag)::candidates) opt_bproof
+ else
+ (f,orr_flag)
+
+(* let rec get_position_in_tree pname treelist =
+ match treelist with
+ [] -> raise jprover_bug
+ | f::r ->
+ begin match f with
+ Empty -> get_position_in_tree pname r
+ | NodeAt(pos) ->
+ if pos.name = pname then
+ pos
+ else
+ get_position_in_tree pname r
+ | NodeA(pos,suctrees) ->
+ get_position_in_tree pname ((Array.to_list suctrees) @ r)
+ end
+*)
+
+(* total corresponds to tot in the thesis,
+ tot simulates the while-loop, solve is the rest *)
+
+ let rec total ftree redord connections csigmaQ slist logic calculus opt_bproof =
+ let rec tot ftree redord connections po slist =
+ let rec solve ftree redord connections p po slist (pred,succs) orr_flag =
+ let newslist = delete (p.name) slist in
+ let rback =
+ if p.st = Gamma_0 then
+ begin
+(* print_endline "that's the gamma rule"; *)
+ [((p.name,pred.name),(build_rule pred p csigmaQ orr_flag calculus))]
+ end
+ else
+ []
+ in
+(* print_endline "gamma check finish"; *)
+ let pnew =
+ if p.pt <> Beta then
+ succs @ (delete p po)
+ else
+ po
+ in
+ match p.pt with
+ Gamma ->
+ rback @ (tot ftree redord connections pnew newslist)
+ | Psi ->
+ if p.op = At then
+ let succ = List.hd succs in
+ rback @ (solve ftree redord connections succ pnew newslist (p,[]) orr_flag) (* solve atoms immediately *)
+ else
+ rback @ (tot ftree redord connections pnew newslist)
+ | Phi ->
+ if p.op = At then
+ let succ = List.hd succs in
+ rback @ (solve ftree redord connections succ pnew newslist (p,[]) orr_flag) (* solve atoms immediately *)
+ else
+ rback @ (tot ftree redord connections pnew newslist)
+ | PNull ->
+ let new_redord = update p.name redord in
+ let (c1,c2) = select_connection (p.name) connections newslist in
+ if (c1= "none" & c2 ="none") then
+ rback @ (tot ftree new_redord connections pnew newslist)
+ else
+ let (ass_pos,inst_pos) =
+(* need the pol=O position ass_pos of the connection for later permutation *)
+(* need the pol=I position inst_pos for NuPRL instantiation *)
+ if p.name = c1 then
+ if p.pol = O then
+ (c1,c2)
+ else
+ (c2,c1)
+ else (* p.name = c2 *)
+ if p.pol = O then
+ (c2,c1)
+ else
+ (c1,c2)
+ in
+ rback @ [(("",ass_pos),(build_rule p p csigmaQ orr_flag calculus))]
+ (* one possibility of recursion end *)
+ | Alpha ->
+ rback @ ((("",p.name),(build_rule p p csigmaQ orr_flag calculus))::(tot ftree redord connections pnew newslist))
+ | Delta ->
+ let sp = List.hd succs in
+ rback @ ((("",p.name),(build_rule p sp csigmaQ orr_flag calculus))::(tot ftree redord connections pnew newslist))
+ | Beta ->
+(* print_endline "split_in"; *)
+ let (ft1,red1,conn1,uslist1,opt_bproof1),(ft2,red2,conn2,uslist2,opt_bproof2) =
+ split (p.address) (p.name) ftree redord connections newslist opt_bproof in
+ let (sigmaQ1,sigmaQ2) = subst_split ft1 ft2 ftree uslist1 uslist2 newslist csigmaQ in
+(* print_endline "split_out"; *)
+ let p1 = total ft1 red1 conn1 sigmaQ1 uslist1 logic calculus opt_bproof1 in
+(* print_endline "compute p1 out"; *)
+ let p2 = total ft2 red2 conn2 sigmaQ2 uslist2 logic calculus opt_bproof2 in
+(* print_endline "compute p2 out"; *)
+ rback @ [(("",p.name),(build_rule p p csigmaQ orr_flag calculus))] @ p1 @ p2 (* second possibility of recursion end *)
+ in
+ begin try
+ let (p,orr_flag) = select_pos po po redord ftree connections slist logic
+ calculus [] opt_bproof
+ (* last argument for guiding selection strategy *)
+ in
+(* print_endline ((p.name)^" "^(string_of_int orr_flag)); *)
+ let predsuccs = tpredsucc p ftree in
+ let pred = List.hd predsuccs
+ and succs = List.tl predsuccs in
+ let redpo = update (p.name) redord in (* deletes the entry (p,psuccset) from the redord *)
+ let rednew =
+ if (p.pt = Delta) then (* keep the tree ordering for the successor position only *)
+ let psucc = List.hd succs in
+ let ppsuccs = tpredsucc psucc ftree in
+ let pre = List.hd ppsuccs
+ and sucs = List.tl ppsuccs in
+ replace_ordering (psucc.name) sucs redpo (* union the succsets of psucc *)
+ else
+ redpo
+ in
+(* print_endline "update ok"; *)
+ solve ftree rednew connections p po slist (pred,succs) orr_flag
+ with Gamma_deadlock ->
+ let ljmc_subproof = total ftree redord connections csigmaQ slist "J" "LJmc" opt_bproof
+ in
+ eigen_counter := 1;
+ permute_ljmc ftree po slist ljmc_subproof
+ (* the permuaiton result will be appended to the lj proof constructed so far *)
+ end
+ in
+ let po = compute_open [ftree] slist in
+ tot ftree redord connections po slist
+
+ let reconstruct ftree redord sigmaQ ext_proof logic calculus =
+ let min_connections = remove_dups_connections ext_proof in
+ let (opt_bproof,beta_exp,closures) = construct_opt_beta_proof ftree ext_proof in
+(* let connections = remove_dups_connections ext_proof in
+ let bproof,beta_exp,closures = construct_beta_proof ftree connections in
+ let (opt_bproof,min_connections) = bproof_purity bproof in
+*)
+ if !debug_jprover then
+ begin
+ print_endline "";
+ print_endline ("Beta proof with number of closures = "^(string_of_int closures)^" and number of beta expansions = "^(string_of_int beta_exp));
+(* print_endline "";
+ print_endline "";
+ print_beta_proof bproof;
+ print_endline "";
+ print_endline "";
+ print_endline "Optimal beta proof: ";
+ print_endline "";
+ print_endline "";
+ print_beta_proof opt_bproof;
+ print_endline "";
+ print_endline "";
+ print_endline ("Beta proof connections: ");
+ Format.open_box 0;
+ print_pairlist min_connections;
+ print_endline ".";
+ Format.print_flush(); *)
+ print_endline "";
+ end;
+ let (newroot_name,unsolved_list) = build_unsolved ftree in
+ let redord2 = (update newroot_name redord) in (* otherwise we would have a deadlock *)
+ let (init_tree,init_redord,init_connections,init_unsolved_list) =
+ purity ftree redord2 min_connections unsolved_list in
+ begin
+(* print_endline "";
+ print_endline "";
+ print_endline ("Purity connections: ");
+ Format.open_box 0;
+ print_pairlist init_connections;
+ print_endline ".";
+ print_endline "";
+ Format.print_flush();
+ print_endline "";
+ print_endline "";
+*)
+(* it should hold: min_connections = init_connections *)
+ total init_tree init_redord init_connections sigmaQ
+ init_unsolved_list logic calculus opt_bproof
+ end
+
+(* ***************** REDUCTION ORDERING -- both types **************************** *)
+
+ exception Reflexive
+
+ let rec transitive_irreflexive_closure addset const ordering =
+ match ordering with
+ [] ->
+ []
+ | (pos,fset)::r ->
+ if (pos = const) or (StringSet.mem const fset) then
+(* check reflexsivity during transitive closure wrt. addset ONLY!!! *)
+ if StringSet.mem pos addset then
+ raise Reflexive
+ else
+ (pos,(StringSet.union fset addset))::(transitive_irreflexive_closure addset const r)
+ else
+ (pos,fset)::(transitive_irreflexive_closure addset const r)
+
+ let rec search_set var ordering =
+(* print_endline var; *)
+ match ordering with
+ [] ->
+ raise (Invalid_argument "Jprover: element in ordering missing")
+ | (pos,fset)::r ->
+ if pos = var then
+ StringSet.add pos fset
+ else
+ search_set var r
+
+ let add_sets var const ordering =
+ let addset = search_set var ordering in
+ transitive_irreflexive_closure addset const ordering
+
+(* ************* J ordering ********************************************** *)
+
+ let rec add_arrowsJ (v,vlist) ordering =
+ match vlist with
+ [] -> ordering
+ | f::r ->
+ if ((String.get f 0)='c') then
+ let new_ordering = add_sets v f ordering in
+ add_arrowsJ (v,r) new_ordering
+ else
+ add_arrowsJ (v,r) ordering
+
+ let rec add_substJ replace_vars replace_string ordering atom_rel =
+ match replace_vars with
+ [] -> ordering
+ | v::r ->
+ if (String.get v 1 = 'n') (* don't integrate new variables *)
+ or (List.exists (fun (x,_,_) -> (x.aname = v)) atom_rel) then (* no reduction ordering at atoms *)
+ (add_substJ r replace_string ordering atom_rel)
+ else
+ let next_ordering = add_arrowsJ (v,replace_string) ordering in
+ (add_substJ r replace_string next_ordering atom_rel)
+
+ let build_orderingJ replace_vars replace_string ordering atom_rel =
+ try
+ add_substJ replace_vars replace_string ordering atom_rel
+ with Reflexive -> (* only possible in the FO case *)
+ raise Not_unifiable (*search for alternative string unifiers *)
+
+ let rec build_orderingJ_list substJ ordering atom_rel =
+ match substJ with
+ [] -> ordering
+ | (v,vlist)::r ->
+ let next_ordering = build_orderingJ [v] vlist ordering atom_rel in
+ build_orderingJ_list r next_ordering atom_rel
+
+(* ************* J ordering END ********************************************** *)
+
+(* ************* quantifier ordering ********************************************** *)
+
+ let rec add_arrowsQ v clist ordering =
+ match clist with
+ [] -> ordering
+ | f::r ->
+ let new_ordering = add_sets v f ordering in
+ add_arrowsQ v r new_ordering
+
+ let rec print_sigmaQ sigmaQ =
+ match sigmaQ with
+ [] ->
+ print_endline "."
+ | (v,term)::r ->
+ begin
+ Format.open_box 0;
+ print_endline " ";
+ print_string (v^" = ");
+ print_term stdout term;
+ Format.force_newline ();
+ Format.print_flush ();
+ print_sigmaQ r
+ end
+
+ let rec print_term_list tlist =
+ match tlist with
+ [] -> print_string "."
+ | t::r ->
+ begin
+ print_term stdout t;
+ print_string " ";
+ print_term_list r
+ end
+
+ let rec add_sigmaQ new_elements ordering =
+ match new_elements with
+ [] -> ([],ordering)
+ | (v,termlist)::r ->
+ let dterms = collect_delta_terms termlist in
+ begin
+(*: print_stringlist dterms;
+ mbreak "add_sigmaQ:1\n";
+ Format.open_box 0;
+ print_endline " ";
+ print_endline "sigmaQ: ";
+ print_string (v^" = ");
+ print_term_list termlist;
+ Format.force_newline ();
+ print_stringlist dterms;
+ Format.force_newline ();
+ Format.print_flush ();
+ mbreak "add_sigmaQ:2\n";
+:*)
+ let new_ordering = add_arrowsQ v dterms ordering in
+(*: print_ordering new_ordering;
+ mbreak "add_sigmaQ:3\n";
+:*)
+ let (rest_pairs,rest_ordering) = add_sigmaQ r new_ordering in
+ ((v,dterms)::rest_pairs),rest_ordering
+ end
+
+ let build_orderingQ new_elements ordering =
+(* new_elements is of type (string * term list) list, since one variable can receive more than *)
+(* a single term due to substitution multiplication *)
+ try
+(* print_endline "build orderingQ in"; *) (* apple *)
+ add_sigmaQ new_elements ordering;
+ with Reflexive ->
+ raise Failed (* new connection, please *)
+
+
+(* ************* quantifier ordering END ********************************************** *)
+
+(* ****** Quantifier unification ************** *)
+
+(* For multiplication we assume always idempotent substitutions sigma, tau! *)
+
+ let rec collect_assoc inst_vars tauQ =
+ match inst_vars with
+ [] -> []
+ | f::r ->
+ let f_term = List.assoc f tauQ in
+ f_term::(collect_assoc r tauQ)
+
+ let rec rec_apply sigmaQ tauQ tau_vars tau_terms =
+ match sigmaQ with
+ [] -> [],[]
+ | (v,term)::r ->
+ let app_term = subst term tau_vars tau_terms in
+ let old_free = free_vars_list term
+ and new_free = free_vars_list app_term in
+ let inst_vars = list_diff old_free new_free in
+ let inst_terms = collect_assoc inst_vars tauQ in
+ let (rest_sigma,rest_sigma_ordering) = rec_apply r tauQ tau_vars tau_terms in
+ if inst_terms = [] then
+ ((v,app_term)::rest_sigma),rest_sigma_ordering
+ else
+ let ordering_v = String.sub v 0 (String.index v '_') in
+ ((v,app_term)::rest_sigma),((ordering_v,inst_terms)::rest_sigma_ordering)
+
+(* let multiply sigmaQ tauQ =
+ let tau_vars,tau_terms = List.split tauQ
+ and sigma_vars,sigma_terms = List.split sigmaQ in
+ let apply_terms = rec_apply sigma_terms tau_vars tau_terms in
+ (List.combine sigma_vars apply_terms) @ tauQ
+*)
+
+ let multiply sigmaQ tauQ =
+ let (tau_vars,tau_terms) = List.split tauQ in
+ let (new_sigmaQ,sigma_ordering) = rec_apply sigmaQ tauQ tau_vars tau_terms in
+ let tau_ordering_terms = (List.map (fun x -> [x]) tau_terms) (* for extending ordering_elements *) in
+ let tau_ordering_vars = (List.map (fun x -> String.sub x 0 (String.index x '_')) tau_vars) in
+ let tau_ordering = (List.combine tau_ordering_vars tau_ordering_terms) in
+ ((new_sigmaQ @ tauQ),
+ (sigma_ordering @ tau_ordering)
+ )
+
+ let apply_2_sigmaQ term1 term2 sigmaQ =
+ let sigma_vars,sigma_terms = List.split sigmaQ in
+ (subst term1 sigma_vars sigma_terms),(subst term2 sigma_vars sigma_terms)
+
+ let jqunify term1 term2 sigmaQ =
+ let app_term1,app_term2 = apply_2_sigmaQ term1 term2 sigmaQ in
+ try
+(*: let tauQ = unify_mm app_term1 app_term2 String_set.StringSet.empty in :*)
+ let tauQ = unify_mm app_term1 app_term2 StringSet.empty in
+ let (mult,oel) = multiply sigmaQ tauQ in
+ (mult,oel)
+ with
+ RefineError _ -> (* any unification failure *)
+(* print_endline "fo-unification fail"; *)
+ raise Failed (* new connection, please *)
+
+(* ************ T-STRING UNIFICATION ******************************** *)
+
+ let rec combine subst (ov,oslist) =
+ match subst with
+ [] -> [],[]
+ | f::r ->
+ let (v,slist) = f in
+ let rest_vlist,rest_combine = (combine r (ov,oslist)) in
+ if (List.mem ov slist) then (* subst assumed to be idemponent *)
+ let com_element = com_subst slist (ov,oslist) in
+ (v::rest_vlist),((v,com_element)::rest_combine)
+ else
+ (rest_vlist,(f::rest_combine))
+
+ let compose sigma one_subst =
+ let (n,subst)=sigma
+ and (ov,oslist) = one_subst in
+ let (trans_vars,com) = combine subst (ov,oslist)
+ 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
+ (trans_vars,(n,com))
+ else
+(* ov may multiply as variable in subst with DIFFERENT values *)
+(* in order to avoid explicit atom instances!!! *)
+ (trans_vars,(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)
+ | (_,[]) -> (us,ut)
+ | ((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 orderingQ atom_rel =
+
+ let rec tunify atomnames fs ft rt rest_eq sigma ordering =
+
+ let apply_r1 fs ft rt rest_eq sigma =
+(* print_endline "r1"; *)
+ tunify_list rest_eq sigma ordering atom_rel
+
+ in
+ let apply_r2 fs ft rt rest_eq sigma =
+(* print_endline "r2"; *)
+ tunify atomnames rt fs ft rest_eq sigma ordering
+
+ 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 ordering
+
+ in
+ let apply_r4 fs ft rt rest_eq sigma =
+(* print_endline "r4"; *)
+ tunify atomnames rt ft fs rest_eq sigma ordering
+
+ in
+ let apply_r5 fs ft rt rest_eq sigma =
+(* print_endline "r5"; *)
+ let v = (List.hd fs) in
+ let (compose_vars,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
+ let new_ordering = build_orderingJ (v::compose_vars) ft ordering atom_rel in
+ tunify atomnames (List.tl fs) rt rt new_rest_eq new_sigma new_ordering
+
+ 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
+ (* no relation update since [] has been replaced for v *)
+ tunify atomnames (List.tl fs) ft rt new_rest_eq new_sigma ordering
+
+ 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 (compose_vars,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
+ let new_ordering = build_orderingJ (v::compose_vars) (ft @ [c1]) ordering atom_rel in
+ tunify atomnames (List.tl fs) [] c2t new_rest_eq new_sigma new_ordering
+
+
+ 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 ordering
+
+ 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 (compose_vars,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
+ let new_ordering =
+ build_orderingJ (v::compose_vars) (ft @ [v_new]) ordering atom_rel in
+ tunify atomnames rt [v_new] (List.tl fs) new_rest_eq new_sigma new_ordering
+
+ 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 ordering
+
+ 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,orderingQ
+ | f::rest_eq ->
+ begin
+(* Format.open_box 0;
+ print_equations [f];
+ Format.print_flush ();
+*)
+ let (atomnames,(fs,ft)) = f in
+ tunify atomnames fs [] ft rest_eq init_sigma orderingQ
+ end
+
+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,[]) orderingQ atom_rel 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 fo_eqlist orderingQ atom_rel qmax =
+ 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 @ fo_eqlist
+ else
+ (new_element::equations) @ fo_eqlist
+ in
+ try
+(* print_equations full_eqlist; *)
+(* max-1 new variables have been used for the domain equations *)
+ let (new_sigma,new_ordering) = tunify_list full_eqlist (1,[]) orderingQ atom_rel in
+(* sigmaQ will not be returned in eqlist *)
+ (new_sigma,(qmax,full_eqlist),new_ordering)
+ with Not_unifiable ->
+ raise Failed (* new connection please *)
+
+let rec one_equation gprefix dlist delta_0_prefixes n =
+ match dlist with
+ [] -> ([],n)
+ | f::r ->
+ let fprefix = List.assoc f delta_0_prefixes in
+ let (sf1,sg) = shorten fprefix gprefix
+ and v_new = ("vnewq"^(string_of_int n)) in
+ let fnew = sf1 @ [v_new] in
+ let (rest_equations,new_n) = one_equation gprefix r delta_0_prefixes (n+1) in
+ (([],(fnew,sg))::rest_equations),new_n
+
+let rec make_domain_equations fo_pairs (gamma_0_prefixes,delta_0_prefixes) n =
+ match fo_pairs with
+ [] -> ([],n)
+ | (g,dlist)::r ->
+ let gprefix = List.assoc g gamma_0_prefixes in
+ let (gequations,max) = one_equation gprefix dlist delta_0_prefixes n in
+ let (rest_equations,new_max) =
+ make_domain_equations r (gamma_0_prefixes,delta_0_prefixes) max in
+ (gequations @ rest_equations),new_max
+
+(* type of one unifier: int * ((string * string list) list) *)
+(* global failure: (0,[]) *)
+
+let stringunify ext_atom try_one eqlist fo_pairs logic orderingQ atom_rel qprefixes =
+ if logic = "C" then
+ ((0,[]),(0,[]),orderingQ)
+ else
+ let (qmax,equations) = eqlist
+ and us = ext_atom.aprefix
+ and ut = try_one.aprefix
+ and ns = ext_atom.aname
+ and nt = try_one.aname in
+ if qprefixes = ([],[]) then (* prop case *)
+ begin
+(* print_endline "This is the prop case"; *)
+ let (new_sigma,new_eqlist) = Jtunify.do_stringunify us ut ns nt equations
+ (* prop unification only *)
+ in
+ (new_sigma,new_eqlist,[]) (* assume the empty reduction ordering during proof search *)
+ end
+ else
+ begin
+(* print_endline "This is the FO case"; *)
+(* fo_eqlist encodes the domain condition on J quantifier substitutions *)
+(* Again, always computed for the whole substitution sigmaQ *)
+ let (fo_eqlist,new_max) = make_domain_equations fo_pairs qprefixes qmax in
+ begin
+(* Format.open_box 0;
+ print_string "domain equations in";
+ print_equations fo_eqlist;
+ print_string "domain equations out";
+ Format.print_flush ();
+*)
+ do_stringunify us ut ns nt equations fo_eqlist orderingQ atom_rel new_max
+ end
+ end
+
+(**************************************** add multiplicity *********************************)
+
+let rec subst_replace subst_list t =
+ match subst_list with
+ [] -> t
+ | (old_t,new_t)::r ->
+ let inter_term = var_subst t old_t "dummy" in
+(*: print_string "(";
+ print_term stdout old_t;
+ print_string " --> ";
+ print_term stdout new_t;
+ print_string ")\n";
+ print_term stdout t;
+ print_newline ();
+ print_term stdout inter_term;
+ print_newline (); :*)
+ let new_term = subst1 inter_term "dummy" new_t in
+(*: print_term stdout new_term;
+ print_newline ();
+ mbreak "\n+++========----- ---------..........\n"; :*)
+ subst_replace r new_term
+
+let rename_pos x m =
+ let pref = String.get x 0 in
+ (Char.escaped pref)^(string_of_int m)
+
+let update_position position m replace_n subst_list mult =
+ let ({name=x; address=y; op=z; pol=p; pt=a; st=b; label=t}) = position in
+ let nx = rename_pos x m in
+ let nsubst_list =
+ if b=Gamma_0 then
+ let vx = mk_var_term (x^"_jprover")
+ and vnx = mk_var_term (nx^"_jprover") in
+ (vx,vnx)::subst_list
+ else
+ if b=Delta_0 then
+ let sx = mk_string_term jprover_op x
+ and snx = mk_string_term jprover_op nx in
+ (sx,snx)::subst_list
+ else
+ subst_list
+ in
+ let nt = subst_replace nsubst_list t in
+ let add_array = Array.of_list y in
+ let _ = (add_array.(replace_n) <- mult) in
+ let new_add = Array.to_list add_array in
+ ({name=nx; address=new_add; op=z; pol=p; pt=a; st=b; label=nt},m,nsubst_list)
+
+let rec append_orderings list_of_lists =
+ match list_of_lists with
+ [] ->
+ []
+ | f::r ->
+ f @ (append_orderings r)
+
+let rec union_orderings first_orderings =
+ match first_orderings with
+ [] ->
+ StringSet.empty
+ | (pos,fset)::r ->
+ StringSet.union (StringSet.add pos fset) (union_orderings r)
+
+let rec select_orderings add_orderings =
+ match add_orderings with
+ [] -> []
+ | f::r ->
+ (List.hd f)::select_orderings r
+
+let combine_ordering_list add_orderings pos_name =
+ let first_orderings = select_orderings add_orderings in
+ let pos_succs = union_orderings first_orderings in
+ let rest_orderings = append_orderings add_orderings in
+ (pos_name,pos_succs)::rest_orderings
+
+let rec copy_and_rename_tree last_tree replace_n pos_n mult subst_list =
+
+ let rec rename_subtrees tree_list nposition s_pos_n nsubst_list =
+ match tree_list with
+ [] -> ([||],[],s_pos_n)
+ | f::r ->
+ let (f_subtree,f_ordering,f_pos_n) =
+ copy_and_rename_tree f replace_n s_pos_n mult nsubst_list in
+ let (r_subtrees,r_ordering_list,r_pos_n) = rename_subtrees r nposition f_pos_n nsubst_list in
+ ((Array.append [|f_subtree|] r_subtrees),(f_ordering::r_ordering_list),r_pos_n)
+
+ in
+ match last_tree with
+ Empty -> raise (Invalid_argument "Jprover: copy tree")
+ | NodeAt(position) -> (* can never be a Gamma_0 position -> no replacements *)
+ let (nposition,npos_n,_) = update_position position (pos_n+1) replace_n subst_list mult in
+ ((NodeAt(nposition)),[(nposition.name,StringSet.empty)],npos_n)
+ | NodeA(position, suctrees) ->
+ let (nposition,npos_n,nsubst_list) = update_position position (pos_n+1) replace_n subst_list mult in
+ let (new_suctrees, new_ordering_list, new_pos_n) =
+ rename_subtrees (Array.to_list suctrees) nposition npos_n nsubst_list in
+ let new_ordering = combine_ordering_list new_ordering_list (nposition.name) in
+ ((NodeA(nposition,new_suctrees)),new_ordering,new_pos_n)
+
+(* we construct for each pos a list orderings representing and correspondning to the array of succtrees *)
+
+let rec add_multiplicity ftree pos_n mult logic =
+ let rec parse_subtrees tree_list s_pos_n =
+ match tree_list with
+ [] -> ([||],[],s_pos_n)
+ | f::r ->
+ let (f_subtree,f_ordering,f_pos_n) = add_multiplicity f s_pos_n mult logic in
+ let (r_subtrees,r_ordering_list,r_pos_n) = parse_subtrees r f_pos_n in
+ ((Array.append [|f_subtree|] r_subtrees),(f_ordering::r_ordering_list),r_pos_n)
+
+ in
+ match ftree with
+ Empty -> raise (Invalid_argument "Jprover: add mult")
+ | NodeAt(pos) -> (ftree,[(pos.name,StringSet.empty)],pos_n)
+ | NodeA(pos,suctrees) ->
+ let (new_suctrees, new_ordering_list, new_pos_n) = parse_subtrees (Array.to_list suctrees) pos_n in
+ if (((pos.pt = Phi) & (((pos.op <> At) & (logic="J")) or ((pos.op = All) & (logic = "C"))))
+ (* no explicit atom-instances *)
+ or ((pos.pt = Gamma) & (pos.st <> Phi_0))) then (* universal quantifiers are copied *)
+ (* at their Phi positions *)
+ let replace_n = (List.length pos.address) (* points to the following argument in the array_of_address *)
+ and last = (Array.length new_suctrees) - 1 in (* array first element has index 0 *)
+ let last_tree = new_suctrees.(last) in
+ let (add_tree,add_ordering,final_pos_n) =
+ copy_and_rename_tree last_tree replace_n new_pos_n mult [] in
+ let final_suctrees = Array.append new_suctrees [|add_tree|]
+ and add_orderings = List.append new_ordering_list [add_ordering] in
+ let final_ordering = combine_ordering_list add_orderings (pos.name) in
+ ((NodeA(pos,final_suctrees)),final_ordering,final_pos_n)
+ else
+ let final_ordering = combine_ordering_list new_ordering_list (pos.name) in
+ ((NodeA(pos,new_suctrees)),final_ordering,new_pos_n)
+
+
+(************** Path checker ****************************************************)
+
+let rec get_sets atom atom_sets =
+ match atom_sets with
+ [] -> raise (Invalid_argument "Jprover bug: atom not found")
+ | f::r ->
+ let (a,b,c) = f in
+ if atom = a then f
+ else
+ get_sets atom r
+
+let rec get_connections a alpha tabulist =
+ match alpha with
+ [] -> []
+ | f::r ->
+ if (a.apredicate = f.apredicate) & (a.apol <> f.apol) & (not (List.mem f tabulist)) then
+ (a,f)::(get_connections a r tabulist)
+ else
+ (get_connections a r tabulist)
+
+let rec connections atom_rel tabulist =
+ match atom_rel with
+ [] -> []
+ | f::r ->
+ let (a,alpha,beta) = f in
+ (get_connections a alpha tabulist) @ (connections r (a::tabulist))
+
+let check_alpha_relation atom set atom_sets =
+ let (a,alpha,beta) = get_sets atom atom_sets in
+ AtomSet.subset set alpha
+
+let rec extset atom_sets path closed =
+ match atom_sets with
+ [] -> AtomSet.empty
+ | f::r ->
+ let (at,alpha,beta) = f in
+ if (AtomSet.subset path alpha) & (AtomSet.subset closed beta) then
+ AtomSet.add at (extset r path closed)
+ else
+ (extset r path closed)
+
+let rec check_ext_list ext_list fail_set atom_sets = (* fail_set consists of one atom only *)
+ match ext_list with
+ [] -> AtomSet.empty
+ | f::r ->
+ if (check_alpha_relation f fail_set atom_sets) then
+ AtomSet.add f (check_ext_list r fail_set atom_sets)
+ else
+ (check_ext_list r fail_set atom_sets)
+
+let fail_ext_set ext_atom ext_set atom_sets =
+ let ext_list = AtomSet.elements ext_set
+ and fail_set = AtomSet.add ext_atom AtomSet.empty in
+ check_ext_list ext_list fail_set atom_sets
+
+let rec ext_partners con path ext_atom (reduction_partners,extension_partners) atom_sets =
+ match con with
+ [] ->
+ (reduction_partners,extension_partners)
+ | f::r ->
+ let (a,b) = f in
+ if List.mem ext_atom [a;b] then
+ let ext_partner =
+ if ext_atom = a then b else a
+ in
+ let (new_red_partners,new_ext_partners) =
+(* force reduction steps first *)
+ if (AtomSet.mem ext_partner path) then
+ ((AtomSet.add ext_partner reduction_partners),extension_partners)
+ else
+ if (check_alpha_relation ext_partner path atom_sets) then
+ (reduction_partners,(AtomSet.add ext_partner extension_partners))
+ else
+ (reduction_partners,extension_partners)
+ in
+ ext_partners r path ext_atom (new_red_partners,new_ext_partners) atom_sets
+ else
+ ext_partners r path ext_atom (reduction_partners,extension_partners) atom_sets
+
+exception Failed_connections
+
+let path_checker atom_rel atom_sets qprefixes init_ordering logic =
+
+ let con = connections atom_rel [] in
+(*: print_endline "";
+ print_endline ("number of connections: "^(string_of_int (List.length con)));
+ mbreak "#connec\n";
+:*)
+ let rec provable path closed (orderingQ,reduction_ordering) eqlist (sigmaQ,sigmaJ) =
+
+ let rec check_connections (reduction_partners,extension_partners) ext_atom =
+ let try_one =
+ if reduction_partners = AtomSet.empty then
+ if extension_partners = AtomSet.empty then
+ raise Failed_connections
+ else
+ AtomSet.choose extension_partners
+ else
+ (* force reduction steps always first!! *)
+ AtomSet.choose reduction_partners
+ in
+(* print_endline ("connection partner "^(try_one.aname)); *)
+(* print_endline ("partner path "^(print_set path));
+*)
+ (try
+ let (new_sigmaQ,new_ordering_elements) = jqunify (ext_atom.alabel) (try_one.alabel) sigmaQ in
+(* build the orderingQ incrementally from the new added substitution tau of new_sigmaQ *)
+ let (relate_pairs,new_orderingQ) = build_orderingQ new_ordering_elements orderingQ in
+(* we make in incremental reflexivity test during the string unification *)
+ let (new_sigmaJ,new_eqlist,new_red_ordering) =
+(* new_red_ordering = [] in propositional case *)
+ stringunify ext_atom try_one eqlist relate_pairs logic new_orderingQ atom_rel qprefixes
+ in
+(* print_endline ("make reduction ordering "^((string_of_int (List.length new_ordering)))); *)
+ let new_closed = AtomSet.add ext_atom closed in
+ let ((next_orderingQ,next_red_ordering),next_eqlist,(next_sigmaQ,next_sigmaJ),subproof) =
+ if AtomSet.mem try_one path then
+ provable path new_closed (new_orderingQ,new_red_ordering) new_eqlist (new_sigmaQ,new_sigmaJ)
+ (* always use old first-order ordering for recursion *)
+ else
+ let new_path = AtomSet.add ext_atom path
+ and extension = AtomSet.add try_one AtomSet.empty in
+ let ((norderingQ,nredordering),neqlist,(nsigmaQ,nsigmaJ),p1) =
+ provable new_path extension (new_orderingQ,new_red_ordering) new_eqlist (new_sigmaQ,new_sigmaJ) in
+ let ((nnorderingQ,nnredordering),nneqlist,(nnsigmaQ,nnsigmaJ),p2) =
+ provable path new_closed (norderingQ,nredordering) neqlist (nsigmaQ,nsigmaJ) in
+ ((nnorderingQ,nnredordering),nneqlist,(nnsigmaQ,nnsigmaJ),(p1 @ p2))
+ (* first the extension subgoals = depth first; then other subgoals in same clause *)
+ in
+ ((next_orderingQ,next_red_ordering),next_eqlist,(next_sigmaQ,next_sigmaJ),(((ext_atom.aname),(try_one.aname))::subproof))
+ with Failed ->
+(* print_endline ("new connection for "^(ext_atom.aname)); *)
+(* print_endline ("Failed"); *)
+ check_connections ((AtomSet.remove try_one reduction_partners),
+ (AtomSet.remove try_one extension_partners)
+ ) ext_atom
+ )
+
+ in
+ let rec check_extension extset =
+ if extset = AtomSet.empty then
+ raise Failed (* go directly to a new entry connection *)
+ else
+ let select_one = AtomSet.choose extset in
+(* print_endline ("extension literal "^(select_one.aname)); *)
+(* print_endline ("extension path "^(print_set path));*)
+ let (reduction_partners,extension_partners) =
+ ext_partners con path select_one (AtomSet.empty,AtomSet.empty) atom_sets in
+ (try
+ check_connections (reduction_partners,extension_partners) select_one
+ with Failed_connections ->
+(* print_endline ("no connections for subgoal "^(select_one.aname)); *)
+(* print_endline ("Failed_connections"); *)
+ let fail_ext_set = fail_ext_set select_one extset atom_sets in
+ check_extension fail_ext_set
+ )
+
+ in
+ let extset = extset atom_sets path closed in
+ if extset = AtomSet.empty then
+ ((orderingQ,reduction_ordering),eqlist,(sigmaQ,sigmaJ),[])
+ else
+ check_extension extset
+ in
+ if qprefixes = ([],[]) then
+ begin
+(* print_endline "!!!!!!!!!!! prop prover !!!!!!!!!!!!!!!!!!"; *)
+(* in the propositional case, the reduction ordering will be computed AFTER proof search *)
+ let (_,eqlist,(_,(n,substJ)),ext_proof) =
+ provable AtomSet.empty AtomSet.empty ([],[]) (1,[]) ([],(1,[])) in
+ let orderingJ = build_orderingJ_list substJ init_ordering atom_rel in
+ ((init_ordering,orderingJ),eqlist,([],(n,substJ)),ext_proof)
+ end
+ else
+ provable AtomSet.empty AtomSet.empty (init_ordering,[]) (1,[]) ([],(1,[]))
+
+(*************************** prepare and init prover *******************************************************)
+
+let rec list_to_set list =
+ match list with
+ [] -> AtomSet.empty
+ | f::r ->
+ let rest_set = list_to_set r in
+ AtomSet.add f rest_set
+
+let rec make_atom_sets atom_rel =
+ match atom_rel with
+ [] -> []
+ | f::r ->
+ let (a,alpha,beta) = f in
+ (a,(list_to_set alpha),(list_to_set beta))::(make_atom_sets r)
+
+let rec predecessor address_1 address_2 ftree =
+ match ftree with
+ Empty -> PNull (* should not occur since every pair of atoms have a common predecessor *)
+ | NodeAt(position) -> PNull (* should not occur as above *)
+ | NodeA(position,suctrees) ->
+ match address_1,address_2 with
+ [],_ -> raise (Invalid_argument "Jprover: predecessors left")
+ | _,[] -> raise (Invalid_argument "Jprover: predecessors right")
+ | (f1::r1),(f2::r2) ->
+ if f1 = f2 then
+ predecessor r1 r2 (suctrees.(f1-1))
+ else
+ position.pt
+
+let rec compute_sets element ftree alist =
+ match alist with
+ [] -> [],[]
+ | first::rest ->
+ if first = element then
+ compute_sets element ftree rest (* element is neithes alpha- nor beta-related to itself*)
+ else
+ let (alpha_rest,beta_rest) = compute_sets element ftree rest in
+ if predecessor (element.aaddress) (first.aaddress) ftree = Beta then
+ (alpha_rest,(first::beta_rest))
+ else
+ ((first::alpha_rest),beta_rest)
+
+let rec compute_atomlist_relations worklist ftree alist = (* last version of alist for total comparison *)
+ let rec compute_atom_relations element ftree alist =
+ let alpha_set,beta_set = compute_sets element ftree alist in
+ (element,alpha_set,beta_set)
+ in
+ match worklist with
+ [] -> []
+ | first::rest ->
+ let first_relations = compute_atom_relations first ftree alist in
+ first_relations::(compute_atomlist_relations rest ftree alist)
+
+let atom_record position prefix =
+ let aname = (position.name) in
+ let aprefix = (List.append prefix [aname]) in (* atom position is last element in prefix *)
+ let aop = (dest_term position.label).term_op in
+ ({aname=aname; aaddress=(position.address); aprefix=aprefix; apredicate=aop;
+ apol=(position.pol); ast=(position.st); alabel=(position.label)})
+
+let rec select_atoms_treelist treelist prefix =
+ let rec select_atoms ftree prefix =
+ match ftree with
+ Empty -> [],[],[]
+ | NodeAt(position) ->
+ [(atom_record position prefix)],[],[]
+ | NodeA(position,suctrees) ->
+ let treelist = Array.to_list suctrees in
+ let new_prefix =
+ let prefix_element =
+ if List.mem (position.st) [Psi_0;Phi_0] then
+ [(position.name)]
+ else
+ []
+ in
+ (List.append prefix prefix_element)
+ in
+ let (gamma_0_element,delta_0_element) =
+ if position.st = Gamma_0 then
+ begin
+(* Format.open_box 0;
+ print_endline "gamma_0 prefixes ";
+ print_string (position.name^" :");
+ print_stringlist prefix;
+ print_endline " ";
+ Format.force_newline ();
+ Format.print_flush ();
+*)
+ [(position.name,prefix)],[]
+ end
+ else
+ if position.st = Delta_0 then
+ begin
+(* Format.open_box 0;
+ print_endline "delta_0 prefixes ";
+ print_string (position.name^" :");
+ print_stringlist prefix;
+ print_endline " ";
+ Format.force_newline ();
+ Format.print_flush ();
+*)
+ [],[(position.name,prefix)]
+ end
+ else
+ [],[]
+ in
+ let (rest_alist,rest_gamma_0_prefixes,rest_delta_0_prefixes) =
+ select_atoms_treelist treelist new_prefix in
+ (rest_alist,(rest_gamma_0_prefixes @ gamma_0_element),
+ (rest_delta_0_prefixes @ delta_0_element))
+
+ in
+ match treelist with
+ [] -> [],[],[]
+ | first::rest ->
+ let (first_alist,first_gprefixes,first_dprefixes) = select_atoms first prefix
+ and (rest_alist,rest_gprefixes,rest_dprefixes) = select_atoms_treelist rest prefix in
+ ((first_alist @ rest_alist),(first_gprefixes @ rest_gprefixes),
+ (first_dprefixes @ rest_dprefixes))
+
+let prepare_prover ftree =
+ let alist,gamma_0_prefixes,delta_0_prefixes = select_atoms_treelist [ftree] [] in
+ let atom_rel = compute_atomlist_relations alist ftree alist in
+ (atom_rel,(gamma_0_prefixes,delta_0_prefixes))
+
+(* ************************ Build intial formula tree and relations *********************************** *)
+(* Building a formula tree and the tree ordering from the input formula, i.e. OCaml term *)
+
+let make_position_name stype pos_n =
+ let prefix =
+ if List.mem stype [Phi_0;Gamma_0]
+ then "v"
+ else
+ if List.mem stype [Psi_0;Delta_0]
+ then "c"
+ else
+ "a"
+ in
+ prefix^(string_of_int pos_n)
+
+let dual_pol pol =
+ if pol = O then I else O
+
+let check_subst_term (variable,old_term) pos_name stype =
+ if (List.mem stype [Gamma_0;Delta_0]) then
+ let new_variable =
+ if stype = Gamma_0 then (mk_var_term (pos_name^"_jprover"))
+ else
+ (mk_string_term jprover_op pos_name)
+ in
+ (subst1 old_term variable new_variable) (* replace variable (non-empty) in t by pos_name *)
+ (* pos_name is either a variable term or a constant, f.i. a string term *)
+ (* !!! check unification module how handling eingenvariables as constants !!! *)
+ else
+ old_term
+
+let rec build_ftree (variable,old_term) pol stype address pos_n =
+ let pos_name = make_position_name stype pos_n in
+ let term = check_subst_term (variable,old_term) pos_name stype in
+ if JLogic.is_and_term term then
+ let s,t = JLogic.dest_and term in
+ let ptype,stype_1,stype_2 =
+ if pol = O
+ then Beta,Beta_1,Beta_2
+ else
+ Alpha,Alpha_1,Alpha_2
+ in
+ let position = {name=pos_name; address=address; op=And; pol=pol; pt=ptype; st=stype; label=term} in
+ let subtree_left,ordering_left,posn_left = build_ftree ("",s) pol stype_1 (address@[1]) (pos_n+1) in
+ let subtree_right,ordering_right,posn_right = build_ftree ("",t) pol stype_2 (address@[2])
+ (posn_left+1) in
+ let (succ_left,whole_left) = List.hd ordering_left
+ and (succ_right,whole_right) = List.hd ordering_right in
+ let pos_succs =
+ (StringSet.add succ_left (StringSet.add succ_right (StringSet.union whole_left whole_right)))
+ in
+ (NodeA(position,[|subtree_left;subtree_right|]),
+ ((position.name,pos_succs)::(ordering_left @ ordering_right)),
+ posn_right
+ )
+ else
+ if JLogic.is_or_term term then
+ let s,t = JLogic.dest_or term in
+ let ptype,stype_1,stype_2 =
+ if pol = O
+ then Alpha,Alpha_1,Alpha_2
+ else
+ Beta,Beta_1,Beta_2
+ in
+ let position = {name=pos_name; address=address; op=Or; pol=pol; pt=ptype; st=stype; label=term} in
+ let subtree_left,ordering_left,posn_left = build_ftree ("",s) pol stype_1 (address@[1]) (pos_n+1) in
+ let subtree_right,ordering_right,posn_right = build_ftree ("",t) pol stype_2 (address@[2])
+ (posn_left+1) in
+ let (succ_left,whole_left) = List.hd ordering_left
+ and (succ_right,whole_right) = List.hd ordering_right in
+ let pos_succs =
+ StringSet.add succ_left (StringSet.add succ_right (StringSet.union whole_left whole_right)) in
+ (NodeA(position,[|subtree_left;subtree_right|]),
+ ((position.name),pos_succs) :: (ordering_left @ ordering_right),
+ posn_right
+ )
+ else
+ if JLogic.is_implies_term term then
+ let s,t = JLogic.dest_implies term in
+ let ptype_0,stype_0,ptype,stype_1,stype_2 =
+ if pol = O
+ then Psi,Psi_0,Alpha,Alpha_1,Alpha_2
+ else
+ Phi,Phi_0,Beta,Beta_1,Beta_2
+ in
+ let pos2_name = make_position_name stype_0 (pos_n+1) in
+ let sposition = {name=pos_name; address=address; op=Imp; pol=pol; pt=ptype_0; st=stype; label=term}
+ and position = {name=pos2_name; address=address@[1]; op=Imp; pol=pol; pt=ptype; st=stype_0; label=term} in
+ let subtree_left,ordering_left,posn_left = build_ftree ("",s) (dual_pol pol) stype_1 (address@[1;1])
+ (pos_n+2) in
+ let subtree_right,ordering_right,posn_right = build_ftree ("",t) pol stype_2 (address@[1;2])
+ (posn_left+1) in
+ let (succ_left,whole_left) = List.hd ordering_left
+ and (succ_right,whole_right) = List.hd ordering_right in
+ let pos_succs =
+ StringSet.add succ_left (StringSet.add succ_right (StringSet.union whole_left whole_right)) in
+ let pos_ordering = (position.name,pos_succs) :: (ordering_left @ ordering_right) in
+ (NodeA(sposition,[|NodeA(position,[|subtree_left;subtree_right|])|]),
+ ((sposition.name,(StringSet.add position.name pos_succs))::pos_ordering),
+ posn_right
+ )
+ else
+ if JLogic.is_not_term term then
+ let s = JLogic.dest_not term in
+ let ptype_0,stype_0,ptype,stype_1=
+ if pol = O
+ then Psi,Psi_0,Alpha,Alpha_1
+ else
+ Phi,Phi_0,Alpha,Alpha_1
+ in
+ let pos2_name = make_position_name stype_0 (pos_n+1) in
+ let sposition = {name=pos_name; address=address; op=Neg; pol=pol; pt=ptype_0; st=stype; label=term}
+ and position = {name=pos2_name; address=address@[1]; op=Neg; pol=pol; pt=ptype; st=stype_0; label=term} in
+ let subtree_left,ordering_left,posn_left = build_ftree ("",s) (dual_pol pol) stype_1 (address@[1;1])
+ (pos_n+2) in
+ let (succ_left,whole_left) = List.hd ordering_left in
+ let pos_succs =
+ StringSet.add succ_left whole_left in
+ let pos_ordering = (position.name,pos_succs) :: ordering_left in
+ (NodeA(sposition,[|NodeA(position,[| subtree_left|])|]),
+ ((sposition.name,(StringSet.add position.name pos_succs))::pos_ordering),
+ posn_left
+ )
+ else
+ if JLogic.is_exists_term term then
+ let v,s,t = JLogic.dest_exists term in (* s is type of v and will be supressed here *)
+ let ptype,stype_1 =
+ if pol = O
+ then Gamma,Gamma_0
+ else
+ Delta,Delta_0
+ in
+ let position = {name=pos_name; address=address; op=Ex; pol=pol; pt=ptype; st=stype; label=term} in
+ let subtree_left,ordering_left,posn_left = build_ftree (v,t) pol stype_1 (address@[1]) (pos_n+1) in
+ let (succ_left,whole_left) = List.hd ordering_left in
+ let pos_succs =
+ StringSet.add succ_left whole_left in
+ (NodeA(position,[|subtree_left|]),
+ ((position.name,pos_succs) :: ordering_left),
+ posn_left
+ )
+ else
+ if JLogic.is_all_term term then
+ let v,s,t = JLogic.dest_all term in
+ (* s is type of v and will be supressed here *)
+ let ptype_0,stype_0,ptype,stype_1=
+ if pol = O
+ then Psi,Psi_0,Delta,Delta_0
+ else
+ Phi,Phi_0,Gamma,Gamma_0
+ in
+ let pos2_name = make_position_name stype_0 (pos_n+1) in
+ let sposition = {name=pos_name; address=address; op=All; pol=pol; pt=ptype_0; st=stype; label=term}
+ and position = {name=pos2_name; address=address@[1]; op=All; pol=pol; pt=ptype; st=stype_0; label=term} in
+ let subtree_left,ordering_left,posn_left = build_ftree (v,t) pol stype_1 (address@[1;1])
+ (pos_n+2) in
+ let (succ_left,whole_left) = List.hd ordering_left in
+ let pos_succs =
+ StringSet.add succ_left whole_left in
+ let pos_ordering = (position.name,pos_succs) :: ordering_left in
+ (NodeA(sposition,[|NodeA(position,[|subtree_left|])|]),
+ ((sposition.name,(StringSet.add position.name pos_succs))::pos_ordering),
+ posn_left
+ )
+ else (* finally, term is atomic *)
+ let ptype_0,stype_0 =
+ if pol = O
+ then Psi,Psi_0
+ else
+ Phi,Phi_0
+ in
+ let pos2_name = make_position_name stype_0 (pos_n+1) in
+ let sposition = {name=pos_name; address=address; op=At; pol=pol; pt=ptype_0; st=stype; label=term}
+ and position = {name=pos2_name; address=address@[1]; op=At; pol=pol; pt=PNull; st=stype_0; label=term} in
+ (NodeA(sposition,[|NodeAt(position)|]),
+ [(sposition.name,(StringSet.add position.name StringSet.empty));(position.name,StringSet.empty)],
+ pos_n+1
+ )
+
+let rec construct_ftree termlist treelist orderinglist pos_n goal =
+ match termlist with
+ [] ->
+ let new_root = {name="w"; address=[]; op=Null; pol=O; pt=Psi; st=PNull_0; label=goal}
+ and treearray = Array.of_list treelist in
+ NodeA(new_root,treearray),(("w",(union_orderings orderinglist))::orderinglist),pos_n
+ | ft::rest_terms ->
+ let next_address = [((List.length treelist)+1)]
+ and next_pol,next_goal =
+ if rest_terms = [] then
+ O,ft (* construct tree for the conclusion *)
+ else
+ I,goal
+ in
+ let new_tree,new_ordering,new_pos_n =
+ build_ftree ("",ft) next_pol Alpha_1 next_address (pos_n+1) in
+ construct_ftree rest_terms (treelist @ [new_tree])
+ (orderinglist @ new_ordering) new_pos_n next_goal
+
+(*************************** Main LOOP ************************************)
+let unprovable = RefineError ("Jprover", StringError "formula is not provable")
+let mult_limit_exn = RefineError ("Jprover", StringError "multiplicity limit reached")
+let coq_exn = RefineError ("Jprover", StringError "interface for coq: error on ")
+
+let init_prover ftree =
+ let atom_relation,qprefixes = prepare_prover ftree in
+(* print_atom_info atom_relation; *) (* apple *)
+ let atom_sets = make_atom_sets atom_relation in
+ (atom_relation,atom_sets,qprefixes)
+
+
+let rec try_multiplicity mult_limit ftree ordering pos_n mult logic =
+ try
+ let (atom_relation,atom_sets,qprefixes) = init_prover ftree in
+ let ((orderingQ,red_ordering),eqlist,unifier,ext_proof) =
+ path_checker atom_relation atom_sets qprefixes ordering logic in
+ (ftree,red_ordering,eqlist,unifier,ext_proof) (* orderingQ is not needed as return value *)
+ with Failed ->
+ match mult_limit with
+ Some m when m == mult ->
+ raise mult_limit_exn
+ | _ ->
+ let new_mult = mult+1 in
+ begin
+ Pp.msgnl (Pp.(++) (Pp.str "Multiplicity Fail: Trying new multiplicity ")
+ (Pp.int new_mult));
+(*
+ Format.open_box 0;
+ Format.force_newline ();
+ Format.print_string "Multiplicity Fail: ";
+ Format.print_string ("Try new multiplicity "^(string_of_int new_mult));
+ Format.force_newline ();
+ Format.print_flush ();
+*)
+ let (new_ftree,new_ordering,new_pos_n) =
+ add_multiplicity ftree pos_n new_mult logic in
+ if (new_ftree = ftree) then
+ raise unprovable
+ else
+(* print_formula_info new_ftree new_ordering new_pos_n; *) (* apple *)
+ try_multiplicity mult_limit new_ftree new_ordering new_pos_n new_mult logic
+ end
+
+let prove mult_limit termlist logic =
+ let (ftree,ordering,pos_n) = construct_ftree termlist [] [] 0 (mk_var_term "dummy") in
+(* pos_n = number of positions without new root "w" *)
+(* print_formula_info ftree ordering pos_n; *) (* apple *)
+ try_multiplicity mult_limit ftree ordering pos_n 1 logic
+
+(********** first-order type theory interface *******************)
+
+let rec renam_free_vars termlist =
+ match termlist
+ with [] -> [],[]
+ | f::r ->
+ let var_names = free_vars_list f in
+ let string_terms =
+ List.map (fun x -> (mk_string_term free_var_op x)) var_names
+ in
+ let mapping = List.combine var_names string_terms
+ and new_f = subst f var_names string_terms in
+ let (rest_mapping,rest_renamed) = renam_free_vars r in
+ let unique_mapping = remove_dups_list (mapping @ rest_mapping) in
+ (unique_mapping,(new_f::rest_renamed))
+
+let rec apply_var_subst term var_subst_list =
+ match var_subst_list with
+ [] -> term
+ | (v,t)::r ->
+ let next_term = var_subst term t v in
+ apply_var_subst next_term r
+
+let rec make_equal_list n list_object =
+ if n = 0 then
+ []
+ else
+ list_object::(make_equal_list (n-1) list_object)
+
+let rec create_output rule_list input_map =
+ match rule_list with
+ [] -> JLogic.empty_inf
+ | f::r ->
+ let (pos,(rule,term1,term2)) = f in
+ let delta1_names = collect_delta_terms [term1]
+ and delta2_names = collect_delta_terms [term2] in
+ let unique_deltas = remove_dups_list (delta1_names @ delta2_names) in
+ let delta_terms =
+ List.map (fun x -> (mk_string_term jprover_op x)) unique_deltas in
+ let delta_vars = List.map (fun x -> (x^"_jprover")) unique_deltas in
+ let delta_map = List.combine delta_vars delta_terms in
+ let var_mapping = (input_map @ delta_map) in
+ let frees1 = free_vars_list term1
+ and frees2 = free_vars_list term2 in
+ let unique_object = mk_var_term "v0_jprover" in
+ let unique_list1 = make_equal_list (List.length frees1) unique_object
+ and unique_list2 = make_equal_list (List.length frees2) unique_object
+ in
+ let next_term1 = subst term1 frees1 unique_list1
+ and next_term2 = subst term2 frees2 unique_list2 in
+ let new_term1 = apply_var_subst next_term1 var_mapping
+ and new_term2 = apply_var_subst next_term2 var_mapping
+ and (a,b) = pos
+ in
+(*: print_string (a^"+++"^b^"\n"); :*)
+
+(* kick away the first argument, the position *)
+ (JLogic.append_inf (create_output r input_map) (b,new_term1) (a,new_term2) rule)
+
+let rec make_test_interface rule_list input_map =
+ match rule_list with
+ [] -> []
+ | f::r ->
+ let (pos,(rule,term1,term2)) = f in
+ let delta1_names = collect_delta_terms [term1]
+ and delta2_names = collect_delta_terms [term2] in
+ let unique_deltas = remove_dups_list (delta1_names @ delta2_names) in
+ let delta_terms =
+ List.map (fun x -> (mk_string_term jprover_op x)) unique_deltas in
+ let delta_vars = List.map (fun x -> (x^"_jprover")) unique_deltas in
+ let delta_map = List.combine delta_vars delta_terms in
+ let var_mapping = (input_map @ delta_map) in
+ let frees1 = free_vars_list term1
+ and frees2 = free_vars_list term2 in
+ let unique_object = mk_var_term "v0_jprover" in
+ let unique_list1 = make_equal_list (List.length frees1) unique_object
+ and unique_list2 = make_equal_list (List.length frees2) unique_object
+ in
+ begin
+(*
+ print_endline "";
+ print_endline "";
+ print_stringlist frees1;
+ print_endline "";
+ print_stringlist frees2;
+ print_endline "";
+ print_endline "";
+*)
+ let next_term1 = subst term1 frees1 unique_list1
+ and next_term2 = subst term2 frees2 unique_list2 in
+ let new_term1 = apply_var_subst next_term1 var_mapping
+ and new_term2 = apply_var_subst next_term2 var_mapping
+ in
+ (pos,(rule,new_term1,new_term2))::(make_test_interface r input_map)
+ end
+
+(**************************************************************)
+
+(*: modified for Coq :*)
+
+let decomp_pos pos =
+ let {name=n; address=a; label=l} = pos in
+ (n,(a,l))
+
+let rec build_formula_id ftree =
+ let rec build_fid_list = function
+ [] -> []
+ | t::rest -> (build_formula_id t)@(build_fid_list rest)
+ in
+ match ftree with
+ Empty -> []
+ | NodeAt(position) ->
+ [decomp_pos position]
+ | NodeA(position,subtrees) ->
+ let tree_list = Array.to_list subtrees in
+ (decomp_pos position)::(build_fid_list tree_list)
+
+let rec encode1 = function (* normal *)
+ [] -> ""
+ | i::r -> "_"^(string_of_int i)^(encode1 r)
+
+let rec encode2 = function (* move up *)
+ [i] -> ""
+ | i::r -> "_"^(string_of_int i)^(encode2 r)
+ | _ -> raise coq_exn
+
+let rec encode3 = function (* move down *)
+ [] -> "_1"
+ | i::r -> "_"^(string_of_int i)^(encode3 r)
+
+let lookup_coq str map =
+ try
+ let (il,t) = List.assoc str map in
+ il
+ with Not_found -> raise coq_exn
+
+let create_coq_input inf map =
+ let rec rec_coq_part inf =
+ match inf with
+ [] -> []
+ | (rule, (s1, t1), ((s2, t2) as k))::r ->
+ begin
+ match rule with
+ Andl | Andr | Orl | Orr1 | Orr2 ->
+ (rule, (encode1 (lookup_coq s1 map), t1), k)::(rec_coq_part r)
+ | Impr | Impl | Negr | Negl | Ax ->
+ (rule, (encode2 (lookup_coq s1 map), t1), k)::(rec_coq_part r)
+ | Exr ->
+ (rule, (encode1 (lookup_coq s1 map), t1),
+ (encode1 (lookup_coq s2 map), t2))::(rec_coq_part r)
+ | Exl ->
+ (rule, (encode1 (lookup_coq s1 map), t1),
+ (encode3 (lookup_coq s1 map), t2))::(rec_coq_part r)
+ | Allr | Alll ->
+ (rule, (encode2 (lookup_coq s1 map), t1),
+ (* (s2, t2))::(rec_coq_part r) *)
+ (encode3 (lookup_coq s1 map), t2))::(rec_coq_part r)
+ | _ -> raise coq_exn
+ end
+ in
+ rec_coq_part inf
+
+let gen_prover mult_limit logic calculus hyps concls =
+ let (input_map,renamed_termlist) = renam_free_vars (hyps @ concls) in
+ let (ftree,red_ordering,eqlist,(sigmaQ,sigmaJ),ext_proof) = prove mult_limit renamed_termlist logic in
+ let sequent_proof = reconstruct ftree red_ordering sigmaQ ext_proof logic calculus in
+ let (ptree,count_ax) = bproof sequent_proof in
+ let idl = build_formula_id ftree in
+(* print_ftree ftree; apple *)
+ (* transform types and rename constants *)
+ (* we can transform the eigenvariables AFTER proof reconstruction since *)
+ (* new delta_0 constants may have been constructed during rule permutation *)
+ (* from the LJmc to the LJ proof *)
+ create_coq_input (create_output sequent_proof input_map) idl
+
+(*: end of coq modification :*)
+
+let prover mult_limit hyps concl = gen_prover mult_limit "J" "LJ" hyps [concl]
+
+(************* test with propositional proof reconstruction ************)
+
+let rec count_axioms seq_list =
+ match seq_list with
+ [] -> 0
+ | f::r ->
+ let (rule,_,_) = f in
+ if rule = Ax then
+ 1 + count_axioms r
+ else
+ count_axioms r
+
+let do_prove mult_limit termlist logic calculus =
+ try begin
+ let (input_map,renamed_termlist) = renam_free_vars termlist in
+ let (ftree,red_ordering,eqlist,(sigmaQ,sigmaJ),ext_proof) = prove mult_limit renamed_termlist logic in
+ Format.open_box 0;
+ Format.force_newline ();
+ Format.force_newline ();
+ Format.print_string "Extension proof ready";
+ Format.force_newline ();
+ Format.force_newline ();
+ Format.print_string ("Length of Extension proof: "^((string_of_int (List.length ext_proof)))^
+ " Axioms");
+ Format.force_newline ();
+ Format.force_newline ();
+ print_endline "Extension proof:";
+ Format.open_box 0;
+ print_pairlist ext_proof; (* print list of type (string * string) list *)
+ Format.force_newline ();
+ Format.force_newline ();
+ Format.force_newline ();
+ Format.print_flush ();
+ Format.print_flush ();
+ Format.open_box 0;
+ print_ordering red_ordering;
+ Format.print_flush ();
+ Format.open_box 0;
+ Format.force_newline ();
+(* ----------------------------------------------- *)
+ Format.open_box 0;
+ print_tunify sigmaJ;
+ Format.print_flush ();
+ print_endline "";
+ print_endline "";
+ print_sigmaQ sigmaQ;
+ print_endline "";
+ print_endline "";
+ Format.open_box 0;
+ let (qmax,equations) = eqlist in
+ print_endline ("number of quantifier domains : "^(string_of_int (qmax-1)));
+ print_endline "";
+ print_equations equations;
+ Format.print_flush ();
+ print_endline "";
+ print_endline "";
+ print_endline ("Length of equations : "^((string_of_int (List.length equations))));
+ print_endline "";
+ print_endline "";
+(* --------------------------------------------------------- *)
+ Format.print_string "Break ... ";
+ print_endline "";
+ print_endline "";
+ Format.print_flush ();
+(*: let _ = input_char stdin in :*)
+ let reconstr_proof = reconstruct ftree red_ordering sigmaQ ext_proof logic calculus in
+ let sequent_proof = make_test_interface reconstr_proof input_map in
+ Format.open_box 0;
+ Format.force_newline ();
+ Format.force_newline ();
+ Format.print_string "Sequent proof ready";
+ Format.force_newline ();
+ Format.force_newline ();
+ Format.print_flush ();
+ let (ptree,count_ax) = bproof sequent_proof in
+ Format.open_box 0;
+ Format.print_string ("Length of sequent proof: "^((string_of_int count_ax))^" Axioms");
+ Format.force_newline ();
+ Format.force_newline ();
+ Format.force_newline ();
+ Format.force_newline ();
+ Format.print_flush ();
+ tt ptree; (*: print proof tree :*)
+ Format.print_flush ();
+ print_endline "";
+ print_endline ""
+ end with exn -> begin
+ print_endline "Jprover got an exception:";
+ print_endline (Printexc.to_string exn)
+ end
+
+let test concl logic calculus = (* calculus should be LJmc or LJ for J, and LK for C *)
+ do_prove None [concl] logic calculus
+
+(* for sequents *)
+
+let seqtest list_term logic calculus =
+ let bterms = (dest_term list_term).term_terms in
+ let termlist = collect_subterms bterms in
+ do_prove None termlist logic calculus
+
+(*****************************************************************)
+
+end (* of struct *)
diff --git a/contrib/jprover/jall.mli b/contrib/jprover/jall.mli
new file mode 100644
index 00000000..1811fe59
--- /dev/null
+++ b/contrib/jprover/jall.mli
@@ -0,0 +1,339 @@
+(* JProver provides an efficient refiner for first-order classical
+ and first-order intuitionistic logic. It consists of two main parts:
+ a proof search procedure and a proof reconstruction procedure.
+
+
+ Proof Search
+ ============
+
+ The proof search process is based on a matrix-based (connection-based)
+ proof procedure, i.e.~a non-normalform extension procedure.
+ Besides the well-known quantifier substitution (Martelli Montanari),
+ a special string unifiation procedure is used in order to
+ efficiently compute intuitionistic rule non-permutabilities.
+
+
+ Proof Reconstruction
+ ====================
+
+ The proof reconstruction process converts machine-generated matrix proofs
+ into cut-free Gentzen-style sequent proofs. For classcal logic "C",
+ Gentzen's sequent calculus "LK" is used as target calculus.
+ For intuitionistic logic "J", either Gentzen's single-conclusioned sequent
+ calculus "LJ" or Fitting's multiply-conclusioned sequent calculus "LJmc"
+ can be used. All sequent claculi are implemented in a set-based formulation
+ in order to avoid structural rules.
+
+ The proof reconstruction procedure combines three main procedures, depending
+ on the selected logics and sequent calculi. It consists of:
+
+ 1) A uniform traversal algorithm for all logics and target sequent calculi.
+ This procedure converts classical (intuitionistic) matrix proofs
+ directly into cut-free "LK" ("LJmc" or "LJ") sequent proofs.
+ However, the direct construction of "LJ" proofs may fail in some cases
+ due to proof theoretical reasons.
+
+ 2) A complete redundancy deletion algorithm, which integrates additional
+ knowledge from the proof search process into the reconstruction process.
+ This procedure is called by the traversal algorithms in order to avoid
+ search and deadlocks during proof reconstruciton.
+
+ 3) A permutation-based proof transformation for converting "LJmc" proofs
+ into "LJ" proofs.
+ This procedure is called by-need, whenever the direct reconstruction
+ of "LJ" proofs from matrix proofs fails.
+
+
+
+
+ Literature:
+ ==========
+
+ JProver system description was presented at CADE 2001:
+ @InProceedings{inp:Schmitt+01a,
+ author = "Stephan Schmitt and Lori Lorigo and Christoph Kreitz and
+ Alexey Nogin",
+ title = "{{\sf JProver}}: Integrating Connection-based Theorem
+ Proving into Interactive Proof Assistants",
+ booktitle = "International Joint Conference on Automated Reasoning",
+ year = "2001",
+ editor = "R. Gore and A. Leitsch and T. Nipkow",
+ volume = 2083,
+ series = LNAI,
+ pages = "421--426",
+ publisher = SPRINGER,
+ language = English,
+ where = OWN,
+ }
+
+ The implementation of JProver is based on the following publications:
+
+
+
+ Slides of PRL-seminar talks:
+ ---------------------------
+
+ An Efficient Refiner for First-order Intuitionistic Logic
+
+ http://www.cs.cornell.edu/Nuprl/PRLSeminar/PRLSeminar99_00/schmitt/feb28.html
+
+
+ An Efficient Refiner for First-order Intuitionistic Logic (Part II)
+
+ http://www.cs.cornell.edu/Nuprl/PRLSeminar/PRLSeminar99_00/schmitt/may22.html
+
+
+
+ Proof search:
+ -------------
+
+
+[1]
+ @InProceedings{inp:OttenKreitz96b,
+ author = "J.~Otten and C.~Kreitz",
+ title = "A uniform proof procedure for classical and
+ non-classical logics",
+ booktitle = "Proceedings of the 20$^{th}$ German Annual Conference on
+ Artificial Intelligence",
+ year = "1996",
+ editor = "G.~G{\"o}rz and S.~H{\"o}lldobler",
+ number = "1137",
+ series = LNAI,
+ pages = "307--319",
+ publisher = SPRINGER
+ }
+
+
+[2]
+ @Article{ar:KreitzOtten99,
+ author = "C.~Kreitz and J.~Otten",
+ title = "Connection-based theorem proving in classical and
+ non-classical logics",
+ journal = "Journal for Universal Computer Science,
+ Special Issue on Integration of Deductive Systems",
+ year = "1999",
+ volume = "5",
+ number = "3",
+ pages = "88--112"
+ }
+
+
+
+
+ Special string unifiation procedure:
+ ------------------------------------
+
+
+[3]
+ @InProceedings{inp:OttenKreitz96a,
+ author = "J.~Otten and C.~Kreitz",
+ titl = "T-string-unification: unifying prefixes in
+ non-classical proof methods",
+ booktitle = "Proceedings of the 5$^{th}$ Workshop on Theorem Proving
+ with Analytic Tableaux and Related Methods",
+ year = 1996,
+ editor = "U.~Moscato",
+ number = "1071",
+ series = LNAI,
+ pages = "244--260",
+ publisher = SPRINGER,
+ month = "May "
+ }
+
+
+
+ Proof reconstruction: Uniform traversal algorithm
+ -------------------------------------------------
+
+
+[4]
+ @InProceedings{inp:SchmittKreitz96a,
+ author = "S.~Schmitt and C.~Kreitz",
+ title = "Converting non-classical matrix proofs into
+ sequent-style systems",
+ booktitle = "Proceedings of the 13$^t{}^h$ Conference on
+ Automated Deduction",
+ editor = M.~A.~McRobbie and J.~K.~Slaney",
+ number = "1104",
+ series = LNAI,
+ pages = "418--432",
+ year = "1996",
+ publisher = SPRINGER,
+ month = "July/August"
+ }
+
+
+[5]
+ @Article{ar:KreitzSchmitt00,
+ author = "C.~Kreitz and S.~Schmitt",
+ title = "A uniform procedure for converting matrix proofs
+ into sequent-style systems",
+ journal = "Journal of Information and Computation",
+ year = "2000",
+ note = "(to appear)"
+ }
+
+
+[6]
+ @Book{bo:Schmitt00,
+ author = "S.~Schmitt",
+ title = "Proof reconstruction in classical and non-classical logics",
+ year = "2000",
+ publisher = "Infix",
+ series = "Dissertationen zur K{\"u}nstlichen Intelleigenz",
+ number = "(to appear)",
+ note = "(Ph.{D}.~{T}hesis, Technische Universit{\"a}t Darmstadt,
+ FG Intellektik, Germany, 1999)"
+ }
+
+ The traversal algorithm is presented in the Chapters 2 and 3 of my thesis.
+ The thesis will be made available for the Department through Christoph Kreitz,
+ Upson 4159, kreitz@cs.cornell.edu
+
+
+
+
+ Proof reconstruction: Complete redundancy deletion
+ --------------------------------------------------
+
+
+[7]
+ @Book{bo:Schmitt00,
+ author = "S.~Schmitt",
+ title = "Proof reconstruction in classical and non-classical logics",
+ year = "2000",
+ publisher = "Infix",
+ series = "Dissertationen zur K{\"u}nstlichen Intelleigenz",
+ note = "(Ph.{D}.~{T}hesis, Technische Universit{\"a}t Darmstadt,
+ FG Intellektik, Germany, 1999)"
+ note = "(to appear)",
+
+ }
+
+ The integration of proof knowledge and complete redundancy deletion is presented
+ in Chapter 4 of my thesis.
+
+
+[8]
+ @InProceedings{inp:Schmitt00,
+ author = "S.~Schmitt",
+ title = "A tableau-like representation framework for efficient
+ proof reconstruction",
+ booktitle = "Proceedings of the International Conference on Theorem Proving
+ with Analytic Tableaux and Related Methods",
+ year = "2000",
+ series = LNAI,
+ publisher = SPRINGER,
+ month = "June"
+ note = "(to appear)",
+ }
+
+
+
+
+ Proof Reconstruction: Permutation-based poof transformations "LJ" -> "LJmc"
+ ---------------------------------------------------------------------------
+
+
+[9]
+ @InProceedings{inp:EglySchmitt98,
+ author = "U.~Egly and S.~Schmitt",
+ title = "Intuitionistic proof transformations and their
+ application to constructive program synthesis",
+ booktitle = "Proceedings of the 4$^{th}$ International Conference
+ on Artificial Intelligence and Symbolic Computation",
+ year = "1998",
+ editor = "J.~Calmet and J.~Plaza",
+ number = "1476",
+ series = LNAI,
+ pages = "132--144",
+ publisher = SPRINGER,
+ month = "September"
+ }
+
+
+[10]
+ @Article{ar:EglySchmitt99,
+ author = "U.~Egly and S.~Schmitt",
+ title = "On intuitionistic proof transformations, their
+ complexity, and application to constructive program synthesis",
+ journal = "Fundamenta Informaticae,
+ Special Issue: Symbolic Computation and Artificial Intelligence",
+ year = "1999",
+ volume = "39",
+ number = "1--2",
+ pages = "59--83"
+ }
+*)
+
+(*: open Refiner.Refiner
+open Refiner.Refiner.Term
+open Refiner.Refiner.TermType
+open Refiner.Refiner.TermSubst
+
+open Jlogic_sig
+:*)
+
+open Jterm
+open Opname
+open Jlogic
+
+val ruletable : rule -> string
+
+module JProver(JLogic: JLogicSig) :
+sig
+ val test : term -> string -> string -> unit
+
+ (* Procedure call: test conclusion logic calculus
+
+ test is applied to a first-order formula. The output is some
+ formatted sequent proof for test / debugging purposes.
+
+ The arguments for test are as follows:
+
+ logic = "C"|"J"
+ i.e. first-order classical logic or first-order intuitionistic logic
+
+ calculus = "LK"|"LJ"|"LJmc"
+ i.e. "LK" for classical logic "C", and either Gentzen's single conclusioned
+ calculus "LJ" or Fittings multiply-conclusioned calculus "LJmc" for
+ intuitionistic logic "J".
+
+ term = first-order formula representing the proof goal.
+ *)
+
+
+
+ val seqtest : term -> string -> string -> unit
+
+ (* seqtest procedure is for debugging purposes only *)
+
+
+ val gen_prover : int option -> string -> string -> term list -> term list -> JLogic.inference
+
+ (* Procedure call: gen_prover mult_limit logic calculus hypothesis conclusion
+
+ The arguments for gen_prover are as follows:
+
+ mult_limit - maximal multiplicity to try, None for unlimited
+
+ logic = same as in test
+
+ calculus = same as in test
+
+ hypothesis = list of first-order terms forming the antecedent of the input sequent
+
+ conclusion = list of first-order terms forming the succedent of the input sequent
+ This list should contain only one element if logic = "J" and calculus = "LJ".
+ *)
+
+
+ val prover : int option -> term list -> term -> JLogic.inference
+
+ (* Procedure call: gen_prover mult_limit "J" "LJ" hyps [concl]
+
+ prover provides the first-order refiner for NuPRL, using
+ a single concluisoned succedent [concl] in the sequent.
+ The result is a sequent proof in the single-conclusioned calculus "LJ".
+ *)
+end
diff --git a/contrib/jprover/jlogic.ml b/contrib/jprover/jlogic.ml
new file mode 100644
index 00000000..c074e93e
--- /dev/null
+++ b/contrib/jprover/jlogic.ml
@@ -0,0 +1,106 @@
+open Opname
+open Jterm
+
+type rule =
+ | Ax | Andr | Andl | Orr | Orr1 | Orr2 | Orl | Impr | Impl | Negr | Negl
+ | Allr | Alll| Exr | Exl | Fail | Falsel | Truer
+
+let ruletable = function
+ | Fail -> "Fail"
+ | Ax -> "Ax"
+ | Negl -> "Negl"
+ | Negr -> "Negr"
+ | Andl -> "Andl"
+ | Andr -> "Andr"
+ | Orl -> "Orl"
+ | Orr -> "Orr"
+ | Orr1 -> "Orr1"
+ | Orr2 -> "Orr2"
+ | Impl -> "Impl"
+ | Impr -> "Impr"
+ | Exl -> "Exl"
+ | Exr -> "Exr"
+ | Alll -> "Alll"
+ | Allr -> "Allr"
+ | Falsel -> "Falsel"
+ | Truer -> "Truer"
+
+module type JLogicSig =
+sig
+ (* understanding the input *)
+ val is_all_term : term -> bool
+ val dest_all : term -> string * term * term
+ val is_exists_term : term -> bool
+ val dest_exists : term -> string * term * term
+ val is_and_term : term -> bool
+ val dest_and : term -> term * term
+ val is_or_term : term -> bool
+ val dest_or : term -> term * term
+ val is_implies_term : term -> bool
+ val dest_implies : term -> term * term
+ val is_not_term : term -> bool
+ val dest_not : term -> term
+
+ (* processing the output *)
+ type inf_step = rule * (string * term) * (string * term)
+ type inference = inf_step list
+(* type inference *)
+ val empty_inf : inference
+ val append_inf : inference -> (string * term) -> (string * term) -> rule -> inference
+ val print_inf : inference -> unit
+end;;
+
+(* Copy from [term_op_std.ml]: *)
+
+ let rec print_address int_list =
+ match int_list with
+ | [] ->
+ Format.print_string ""
+ | hd::rest ->
+ begin
+ Format.print_int hd;
+ print_address rest
+ end
+
+module JLogic: JLogicSig =
+struct
+ let is_all_term = Jterm.is_all_term
+ let dest_all = Jterm.dest_all
+ let is_exists_term = Jterm.is_exists_term
+ let dest_exists = Jterm.dest_exists
+ let is_and_term = Jterm.is_and_term
+ let dest_and = Jterm.dest_and
+ let is_or_term = Jterm.is_or_term
+ let dest_or = Jterm.dest_or
+ let is_implies_term = Jterm.is_implies_term
+ let dest_implies = Jterm.dest_implies
+ let is_not_term = Jterm.is_not_term
+ let dest_not = Jterm.dest_not
+
+ type inf_step = rule * (string * term) * (string * term)
+ type inference = inf_step list
+
+ let empty_inf = []
+ let append_inf inf t1 t2 rule =
+ (rule, t1, t2)::inf
+
+ let rec print_inf inf =
+ match inf with
+ | [] -> print_string "."; Format.print_flush ()
+ | (rule, (n1,t1), (n2,t2))::d ->
+ print_string (ruletable rule);
+ print_string (":("^n1^":");
+ print_term stdout t1;
+ print_string (","^n2^":");
+ print_term stdout t2;
+ print_string ")\n";
+ print_inf d
+end;;
+
+let show_loading s = print_string s
+type my_Debug = { mutable debug_name: string;
+ mutable debug_description: string;
+ debug_value: bool
+ }
+
+let create_debug x = ref false
diff --git a/contrib/jprover/jlogic.mli b/contrib/jprover/jlogic.mli
new file mode 100644
index 00000000..a9079791
--- /dev/null
+++ b/contrib/jprover/jlogic.mli
@@ -0,0 +1,40 @@
+(* The interface to manipulate [jterms], which is
+ extracted and modified from Meta-Prl. *)
+
+type rule =
+ Ax | Andr | Andl | Orr | Orr1 | Orr2 | Orl | Impr | Impl | Negr | Negl
+ | Allr | Alll| Exr | Exl | Fail | Falsel | Truer
+
+module type JLogicSig =
+ sig
+ val is_all_term : Jterm.term -> bool
+ val dest_all : Jterm.term -> string * Jterm.term * Jterm.term
+ val is_exists_term : Jterm.term -> bool
+ val dest_exists : Jterm.term -> string * Jterm.term * Jterm.term
+ val is_and_term : Jterm.term -> bool
+ val dest_and : Jterm.term -> Jterm.term * Jterm.term
+ val is_or_term : Jterm.term -> bool
+ val dest_or : Jterm.term -> Jterm.term * Jterm.term
+ val is_implies_term : Jterm.term -> bool
+ val dest_implies : Jterm.term -> Jterm.term * Jterm.term
+ val is_not_term : Jterm.term -> bool
+ val dest_not : Jterm.term -> Jterm.term
+ type inf_step = rule * (string * Jterm.term) * (string * Jterm.term)
+ type inference = inf_step list
+ val empty_inf : inference
+ val append_inf :
+ inference -> (string * Jterm.term) -> (string * Jterm.term) -> rule -> inference
+ val print_inf : inference -> unit
+ end
+
+module JLogic : JLogicSig
+
+val show_loading : string -> unit
+
+type my_Debug = {
+ mutable debug_name : string;
+ mutable debug_description : string;
+ debug_value : bool;
+}
+val create_debug : 'a -> bool ref
+val ruletable : rule -> string
diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4
new file mode 100644
index 00000000..dd76438f
--- /dev/null
+++ b/contrib/jprover/jprover.ml4
@@ -0,0 +1,565 @@
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+open Jlogic
+
+module JA = Jall
+module JT = Jterm
+module T = Tactics
+module TCL = Tacticals
+module TM = Tacmach
+module N = Names
+module PT = Proof_type
+module HT = Hiddentac
+module PA = Pattern
+module HP = Hipattern
+module TR = Term
+module PR = Printer
+module RO = Reductionops
+module UT = Util
+module RA = Rawterm
+
+module J=JA.JProver(JLogic) (* the JProver *)
+
+(*i
+module NO = Nameops
+module TO = Termops
+module RE = Reduction
+module CL = Coqlib
+module ID = Inductiveops
+module CV = Clenv
+module RF = Refiner
+i*)
+
+(* Interface to JProver: *)
+(* type JLogic.inf_step = rule * (string * Jterm.term) * (string * Jterm.term) *)
+type jp_inf_step = JLogic.inf_step
+type jp_inference = JLogic.inference (* simply a list of [inf_step] *)
+
+(* Definitions for rebuilding proof tree from JProver: *)
+(* leaf, one-branch, two-branch, two-branch, true, false *)
+type jpbranch = JP0 | JP1 | JP2 | JP2' | JPT | JPF
+type jptree = | JPempty (* empty tree *)
+ | JPAx of jp_inf_step (* Axiom node *)
+ | JPA of jp_inf_step * jptree
+ | JPB of jp_inf_step * jptree * jptree
+
+(* Private debugging tools: *)
+(*i*)
+let mbreak s = Format.print_flush (); print_string ("-break at: "^s);
+ Format.print_flush (); let _ = input_char stdin in ()
+(*i*)
+let jp_error re = raise (JT.RefineError ("jprover", JT.StringError re))
+
+(* print Coq constructor *)
+let print_constr ct = Pp.ppnl (PR.prterm ct); Format.print_flush ()
+
+let rec print_constr_list = function
+ | [] -> ()
+ | ct::r -> print_constr ct; print_constr_list r
+
+let print_constr_pair op c1 c2 =
+ print_string (op^"(");
+ print_constr c1;
+ print_string ",";
+ print_constr c2;
+ print_string ")\n"
+
+
+(* Parsing modules for Coq: *)
+(* [is_coq_???] : testing functions *)
+(* [dest_coq_???] : destructors *)
+
+let is_coq_true ct = (HP.is_unit_type ct) && not (HP.is_equation ct)
+
+let is_coq_false = HP.is_empty_type
+
+(* return two subterms *)
+let dest_coq_and ct =
+ match (HP.match_with_conjunction ct) with
+ | Some (hdapp,args) ->
+(*i print_constr hdapp; print_constr_list args; i*)
+ begin
+ match args with
+ | s1::s2::[] ->
+(*i print_constr_pair "and" s1 s2; i*)
+ (s1,s2)
+ | _ -> jp_error "dest_coq_and"
+ end
+ | None -> jp_error "dest_coq_and"
+
+let is_coq_or = HP.is_disjunction
+
+(* return two subterms *)
+let dest_coq_or ct =
+ match (HP.match_with_disjunction ct) with
+ | Some (hdapp,args) ->
+(*i print_constr hdapp; print_constr_list args; i*)
+ begin
+ match args with
+ | s1::s2::[] ->
+(*i print_constr_pair "or" s1 s2; i*)
+ (s1,s2)
+ | _ -> jp_error "dest_coq_or"
+ end
+ | None -> jp_error "dest_coq_or"
+
+let is_coq_not = HP.is_nottype
+
+let dest_coq_not ct =
+ match (HP.match_with_nottype ct) with
+ | Some (hdapp,arg) ->
+(*i print_constr hdapp; print_constr args; i*)
+(*i print_string "not ";
+ print_constr arg; i*)
+ arg
+ | None -> jp_error "dest_coq_not"
+
+
+let is_coq_impl ct =
+ match TR.kind_of_term ct with
+ | TR.Prod (_,_,b) -> (not (Termops.dependent (TR.mkRel 1) b))
+ | _ -> false
+
+
+let dest_coq_impl c =
+ match TR.kind_of_term c with
+ | TR.Prod (_,b,c) ->
+(*i print_constr_pair "impl" b c; i*)
+ (b, c)
+ | _ -> jp_error "dest_coq_impl"
+
+(* provide new variables for renaming of universal variables *)
+let new_counter =
+ let ctr = ref 0 in
+ fun () -> incr ctr;!ctr
+
+(* provide new symbol name for unknown Coq constructors *)
+let new_ecounter =
+ let ectr = ref 0 in
+ fun () -> incr ectr;!ectr
+
+(* provide new variables for address naming *)
+let new_acounter =
+ let actr = ref 0 in
+ fun () -> incr actr;!actr
+
+let is_coq_forall ct =
+ match TR.kind_of_term (RO.whd_betaiota ct) with
+ | TR.Prod (_,_,b) -> Termops.dependent (TR.mkRel 1) b
+ | _ -> false
+
+(* return the bounded variable (as a string) and the bounded term *)
+let dest_coq_forall ct =
+ match TR.kind_of_term (RO.whd_betaiota ct) with
+ | TR.Prod (_,_,b) ->
+ let x ="jp_"^(string_of_int (new_counter())) in
+ let v = TR.mkVar (N.id_of_string x) in
+ let c = TR.subst1 v b in (* substitute de Bruijn variable by [v] *)
+(*i print_constr_pair "forall" v c; i*)
+ (x, c)
+ | _ -> jp_error "dest_coq_forall"
+
+
+(* Apply [ct] to [t]: *)
+let sAPP ct t =
+ match TR.kind_of_term (RO.whd_betaiota ct) with
+ | TR.Prod (_,_,b) ->
+ let c = TR.subst1 t b in
+ c
+ | _ -> jp_error "sAPP"
+
+
+let is_coq_exists ct =
+ if not (HP.is_conjunction ct) then false
+ else let (hdapp,args) = TR.decompose_app ct in
+ match args with
+ | _::la::[] ->
+ begin
+ try
+ match TR.destLambda la with
+ | (N.Name _,_,_) -> true
+ | _ -> false
+ with _ -> false
+ end
+ | _ -> false
+
+(* return the bounded variable (as a string) and the bounded term *)
+let dest_coq_exists ct =
+ let (hdapp,args) = TR.decompose_app ct in
+ match args with
+ | _::la::[] ->
+ begin
+ try
+ match TR.destLambda la with
+ | (N.Name x,t1,t2) ->
+ let v = TR.mkVar x in
+ let t3 = TR.subst1 v t2 in
+(*i print_constr_pair "exists" v t3; i*)
+ (N.string_of_id x, t3)
+ | _ -> jp_error "dest_coq_exists"
+ with _ -> jp_error "dest_coq_exists"
+ end
+ | _ -> jp_error "dest_coq_exists"
+
+
+let is_coq_and ct =
+ if (HP.is_conjunction ct) && not (is_coq_exists ct)
+ && not (is_coq_true ct) then true
+ else false
+
+
+(* Parsing modules: *)
+
+let jtbl = Hashtbl.create 53 (* associate for unknown Coq constr. *)
+let rtbl = Hashtbl.create 53 (* reverse table of [jtbl] *)
+
+let dest_coq_symb ct =
+ N.string_of_id (TR.destVar ct)
+
+(* provide new names for unknown Coq constr. *)
+(* [ct] is the unknown constr., string [s] is appended to the name encoding *)
+let create_coq_name ct s =
+ try
+ Hashtbl.find jtbl ct
+ with Not_found ->
+ let t = ("jp_"^s^(string_of_int (new_ecounter()))) in
+ Hashtbl.add jtbl ct t;
+ Hashtbl.add rtbl t ct;
+ t
+
+let dest_coq_app ct s =
+ let (hd, args) = TR.decompose_app ct in
+(*i print_constr hd;
+ print_constr_list args; i*)
+ if TR.isVar hd then
+ (dest_coq_symb hd, args)
+ else (* unknown constr *)
+ (create_coq_name hd s, args)
+
+let rec parsing2 c = (* for function symbols, variables, constants *)
+ if (TR.isApp c) then (* function symbol? *)
+ let (f,args) = dest_coq_app c "fun_" in
+ JT.fun_ f (List.map parsing2 args)
+ else if TR.isVar c then (* identifiable variable or constant *)
+ JT.var_ (dest_coq_symb c)
+ else (* unknown constr *)
+ JT.var_ (create_coq_name c "var_")
+
+(* the main parsing function *)
+let rec parsing c =
+ let ct = Reduction.whd_betadeltaiota (Global.env ()) c in
+(* let ct = Reduction.whd_betaiotazeta (Global.env ()) c in *)
+ if is_coq_true ct then
+ JT.true_
+ else if is_coq_false ct then
+ JT.false_
+ else if is_coq_not ct then
+ JT.not_ (parsing (dest_coq_not ct))
+ else if is_coq_impl ct then
+ let (t1,t2) = dest_coq_impl ct in
+ JT.imp_ (parsing t1) (parsing t2)
+ else if is_coq_or ct then
+ let (t1,t2) = dest_coq_or ct in
+ JT.or_ (parsing t1) (parsing t2)
+ else if is_coq_and ct then
+ let (t1,t2) = dest_coq_and ct in
+ JT.and_ (parsing t1) (parsing t2)
+ else if is_coq_forall ct then
+ let (v,t) = dest_coq_forall ct in
+ JT.forall v (parsing t)
+ else if is_coq_exists ct then
+ let (v,t) = dest_coq_exists ct in
+ JT.exists v (parsing t)
+ else if TR.isApp ct then (* predicate symbol with arguments *)
+ let (p,args) = dest_coq_app ct "P_" in
+ JT.pred_ p (List.map parsing2 args)
+ else if TR.isVar ct then (* predicate symbol without arguments *)
+ let p = dest_coq_symb ct in
+ JT.pred_ p []
+ else (* unknown predicate *)
+ JT.pred_ (create_coq_name ct "Q_") []
+
+(*i
+ print_string "??";print_constr ct;
+ JT.const_ ("err_"^(string_of_int (new_ecounter())))
+i*)
+
+
+(* Translate JProver terms into Coq constructors: *)
+(* The idea is to retrieve it from [rtbl] if it exists indeed, otherwise
+ create one. *)
+let rec constr_of_jterm t =
+ if (JT.is_var_term t) then (* a variable *)
+ let v = JT.dest_var t in
+ try
+ Hashtbl.find rtbl v
+ with Not_found -> TR.mkVar (N.id_of_string v)
+ else if (JT.is_fun_term t) then (* a function symbol *)
+ let (f,ts) = JT.dest_fun t in
+ let f' = try Hashtbl.find rtbl f with Not_found -> TR.mkVar (N.id_of_string f) in
+ TR.mkApp (f', Array.of_list (List.map constr_of_jterm ts))
+ else jp_error "constr_of_jterm"
+
+
+(* Coq tactics for Sequent Calculus LJ: *)
+(* Note that for left-rule a name indicating the being applied rule
+ in Coq's Hints is required; for right-rule a name is also needed
+ if it will pass some subterm to the left-hand side.
+ However, all of these can be computed by the path [id] of the being
+ applied rule.
+*)
+
+let assoc_addr = Hashtbl.create 97
+
+let short_addr s =
+ let ad =
+ try
+ Hashtbl.find assoc_addr s
+ with Not_found ->
+ let t = ("jp_H"^(string_of_int (new_acounter()))) in
+ Hashtbl.add assoc_addr s t;
+ t
+ in
+ N.id_of_string ad
+
+(* and-right *)
+let dyn_andr =
+ T.split RA.NoBindings
+
+(* For example, the following implements the [and-left] rule: *)
+let dyn_andl id = (* [id1]: left child; [id2]: right child *)
+ let id1 = (short_addr (id^"_1")) and id2 = (short_addr (id^"_2")) in
+ (TCL.tclTHEN (T.simplest_elim (TR.mkVar (short_addr id))) (T.intros_using [id1;id2]))
+
+let dyn_orr1 =
+ T.left RA.NoBindings
+
+let dyn_orr2 =
+ T.right RA.NoBindings
+
+let dyn_orl id =
+ let id1 = (short_addr (id^"_1")) and id2 = (short_addr (id^"_2")) in
+ (TCL.tclTHENS (T.simplest_elim (TR.mkVar (short_addr id)))
+ [T.intro_using id1; T.intro_using id2])
+
+let dyn_negr id =
+ let id1 = id^"_1_1" in
+ HT.h_intro (short_addr id1)
+
+let dyn_negl id =
+ T.simplest_elim (TR.mkVar (short_addr id))
+
+let dyn_impr id =
+ let id1 = id^"_1_1" in
+ HT.h_intro (short_addr id1)
+
+let dyn_impl id gl =
+ let t = TM.pf_get_hyp_typ gl (short_addr id) in
+ let ct = Reduction.whd_betadeltaiota (Global.env ()) t in (* unfolding *)
+ let (_,b) = dest_coq_impl ct in
+ let id2 = (short_addr (id^"_1_2")) in
+ (TCL.tclTHENLAST
+ (TCL.tclTHENS (T.cut b) [T.intro_using id2;TCL.tclIDTAC])
+ (T.apply_term (TR.mkVar (short_addr id))
+ [TR.mkMeta (Clenv.new_meta())])) gl
+
+let dyn_allr c = (* [c] must be an eigenvariable which replaces [v] *)
+ HT.h_intro (N.id_of_string c)
+
+(* [id2] is the path of the instantiated term for [id]*)
+let dyn_alll id id2 t gl =
+ let id' = short_addr id in
+ let id2' = short_addr id2 in
+ let ct = TM.pf_get_hyp_typ gl id' in
+ let ct' = Reduction.whd_betadeltaiota (Global.env ()) ct in (* unfolding *)
+ let ta = sAPP ct' t in
+ TCL.tclTHENS (T.cut ta) [T.intro_using id2'; T.apply (TR.mkVar id')] gl
+
+let dyn_exl id id2 c = (* [c] must be an eigenvariable *)
+ (TCL.tclTHEN (T.simplest_elim (TR.mkVar (short_addr id)))
+ (T.intros_using [(N.id_of_string c);(short_addr id2)]))
+
+let dyn_exr t =
+ T.one_constructor 1 (RA.ImplicitBindings [t])
+
+let dyn_falsel = dyn_negl
+
+let dyn_truer =
+ T.one_constructor 1 RA.NoBindings
+
+(* Do the proof by the guidance of JProver. *)
+
+let do_one_step inf =
+ let (rule, (s1, t1), ((s2, t2) as k)) = inf in
+ begin
+(*i if not (Jterm.is_xnil_term t2) then
+ begin
+ print_string "1: "; JT.print_term stdout t2; print_string "\n";
+ print_string "2: "; print_constr (constr_of_jterm t2); print_string "\n";
+ end;
+i*)
+ match rule with
+ | Andl -> dyn_andl s1
+ | Andr -> dyn_andr
+ | Orl -> dyn_orl s1
+ | Orr1 -> dyn_orr1
+ | Orr2 -> dyn_orr2
+ | Impr -> dyn_impr s1
+ | Impl -> dyn_impl s1
+ | Negr -> dyn_negr s1
+ | Negl -> dyn_negl s1
+ | Allr -> dyn_allr (JT.dest_var t2)
+ | Alll -> dyn_alll s1 s2 (constr_of_jterm t2)
+ | Exr -> dyn_exr (constr_of_jterm t2)
+ | Exl -> dyn_exl s1 s2 (JT.dest_var t2)
+ | Ax -> T.assumption (*i TCL.tclIDTAC i*)
+ | Truer -> dyn_truer
+ | Falsel -> dyn_falsel s1
+ | _ -> jp_error "do_one_step"
+ (* this is impossible *)
+ end
+;;
+
+(* Parameter [tr] is the reconstucted proof tree from output of JProver. *)
+let do_coq_proof tr =
+ let rec rec_do trs =
+ match trs with
+ | JPempty -> TCL.tclIDTAC
+ | JPAx h -> do_one_step h
+ | JPA (h, t) -> TCL.tclTHEN (do_one_step h) (rec_do t)
+ | JPB (h, left, right) -> TCL.tclTHENS (do_one_step h) [rec_do left; rec_do right]
+ in
+ rec_do tr
+
+
+(* Rebuild the proof tree from the output of JProver: *)
+
+(* Since some universal variables are not necessarily first-order,
+ lazy substitution may happen. They are recorded in [rtbl]. *)
+let reg_unif_subst t1 t2 =
+ let (v,_,_) = JT.dest_all t1 in
+ Hashtbl.add rtbl v (TR.mkVar (N.id_of_string (JT.dest_var t2)))
+
+let count_jpbranch one_inf =
+ let (rule, (_, t1), (_, t2)) = one_inf in
+ begin
+ match rule with
+ | Ax -> JP0
+ | Orr1 | Orr2 | Negl | Impr | Alll | Exr | Exl -> JP1
+ | Andr | Orl -> JP2
+ | Negr -> if (JT.is_true_term t1) then JPT else JP1
+ | Andl -> if (JT.is_false_term t1) then JPF else JP1
+ | Impl -> JP2' (* reverse the sons of [Impl] since [dyn_impl] reverses them *)
+ | Allr -> reg_unif_subst t1 t2; JP1
+ | _ -> jp_error "count_jpbranch"
+ end
+
+let replace_by r = function
+ (rule, a, b) -> (r, a, b)
+
+let rec build_jptree inf =
+ match inf with
+ | [] -> ([], JPempty)
+ | h::r ->
+ begin
+ match count_jpbranch h with
+ | JP0 -> (r,JPAx h)
+ | JP1 -> let (r1,left) = build_jptree r in
+ (r1, JPA(h, left))
+ | JP2 -> let (r1,left) = build_jptree r in
+ let (r2,right) = build_jptree r1 in
+ (r2, JPB(h, left, right))
+ | JP2' -> let (r1,left) = build_jptree r in (* for [Impl] *)
+ let (r2,right) = build_jptree r1 in
+ (r2, JPB(h, right, left))
+ | JPT -> let (r1,left) = build_jptree r in (* right True *)
+ (r1, JPAx (replace_by Truer h))
+ | JPF -> let (r1,left) = build_jptree r in (* left False *)
+ (r1, JPAx (replace_by Falsel h))
+ end
+
+
+(* The main function: *)
+(* [limits] is the multiplicity limit. *)
+let jp limits gls =
+ let concl = TM.pf_concl gls in
+ let ct = concl in
+(*i print_constr ct; i*)
+ Hashtbl.clear jtbl; (* empty the hash tables *)
+ Hashtbl.clear rtbl;
+ Hashtbl.clear assoc_addr;
+ let t = parsing ct in
+(*i JT.print_term stdout t; i*)
+ try
+ let p = (J.prover limits [] t) in
+(*i print_string "\n";
+ JLogic.print_inf p; i*)
+ let (il,tr) = build_jptree p in
+ if (il = []) then
+ begin
+ Pp.msgnl (Pp.str "Proof is built.");
+ do_coq_proof tr gls
+ end
+ else UT.error "Cannot reconstruct proof tree from JProver."
+ with e -> Pp.msgnl (Pp.str "JProver fails to prove this:");
+ JT.print_error_msg e;
+ UT.error "JProver terminated."
+
+(* an unfailed generalization procedure *)
+let non_dep_gen b gls =
+ let concl = TM.pf_concl gls in
+ if (not (Termops.dependent b concl)) then
+ T.generalize [b] gls
+ else
+ TCL.tclIDTAC gls
+
+let rec unfail_gen = function
+ | [] -> TCL.tclIDTAC
+ | h::r ->
+ TCL.tclTHEN
+ (TCL.tclORELSE (non_dep_gen h) (TCL.tclIDTAC))
+ (unfail_gen r)
+
+(*
+(* no argument, which stands for no multiplicity limit *)
+let jp gls =
+ let ls = List.map (fst) (TM.pf_hyps_types gls) in
+(*i T.generalize (List.map TR.mkVar ls) gls i*)
+ (* generalize the context *)
+ TCL.tclTHEN (TCL.tclTRY T.red_in_concl)
+ (TCL.tclTHEN (unfail_gen (List.map TR.mkVar ls))
+ (jp None)) gls
+*)
+(*
+let dyn_jp l gls =
+ assert (l = []);
+ jp
+*)
+
+(* one optional integer argument for the multiplicity *)
+let jpn n gls =
+ let ls = List.map (fst) (TM.pf_hyps_types gls) in
+ TCL.tclTHEN (TCL.tclTRY T.red_in_concl)
+ (TCL.tclTHEN (unfail_gen (List.map TR.mkVar ls))
+ (jp n)) gls
+(*
+let dyn_jpn l gls =
+ match l with
+ | [PT.Integer n] -> jpn n
+ | _ -> jp_error "Impossible!!!"
+
+
+let h_jp = TM.hide_tactic "Jp" dyn_jp
+
+let h_jpn = TM.hide_tactic "Jpn" dyn_jpn
+*)
+
+TACTIC EXTEND Jprover
+ [ "Jp" natural_opt(n) ] -> [ jpn n ]
+END
+
+(*
+TACTIC EXTEND Andl
+ [ "Andl" ident(id)] -> [ ... (Andl id) ... ].
+END
+*)
diff --git a/contrib/jprover/jterm.ml b/contrib/jprover/jterm.ml
new file mode 100644
index 00000000..7fc923a5
--- /dev/null
+++ b/contrib/jprover/jterm.ml
@@ -0,0 +1,872 @@
+open Printf
+open Opname
+open List
+
+(* Definitions of [jterm]: *)
+type param = param'
+ and operator = operator'
+ and term = term'
+ and bound_term = bound_term'
+ and param' =
+ | Number of int
+ | String of string
+ | Token of string
+ | Var of string
+ | ParamList of param list
+ and operator' = { op_name : opname; op_params : param list }
+ and term' = { term_op : operator; term_terms : bound_term list }
+ and bound_term' = { bvars : string list; bterm : term }
+;;
+
+(* Debugging tools: *)
+(*i*)
+let mbreak s = Format.print_flush (); print_string ("-break at: "^s);
+ Format.print_flush (); let _ = input_char stdin in ()
+(*i*)
+
+type error_msg =
+ | TermMatchError of term * string
+ | StringError of string
+
+exception RefineError of string * error_msg
+
+let ref_raise = function
+ | RefineError(s,e) -> raise (RefineError(s,e))
+ | _ -> raise (RefineError ("Jterm", StringError "unexpected error"))
+
+(* Printing utilities: *)
+
+let fprint_str ostream s =
+ let _ = fprintf ostream "%s." s in ostream
+
+let fprint_str_list ostream sl =
+ ignore (List.fold_left fprint_str ostream sl);
+ Format.print_flush ()
+
+let fprint_opname ostream = function
+ { opname_token= tk; opname_name = sl } ->
+ fprint_str_list ostream sl
+
+let rec fprint_param ostream = function
+ | Number n -> fprintf ostream " %d " n
+ | String s -> fprint_str_list ostream [s]
+ | Token t -> fprint_str_list ostream [t]
+ | Var v -> fprint_str_list ostream [v]
+ | ParamList ps -> fprint_param_list ostream ps
+and fprint_param_list ostream = function
+ | [] -> ()
+ | param::r -> fprint_param ostream param;
+ fprint_param_list ostream r
+;;
+
+let print_strs = fprint_str_list stdout
+
+
+(* Interface to [Jall.ml]: *)
+(* It is extracted from Meta-Prl's standard implementation. *)
+(*c begin of the extraction *)
+
+type term_subst = (string * term) list
+let mk_term op bterms = { term_op = op; term_terms = bterms }
+let make_term x = x (* external [make_term : term' -> term] = "%identity" *)
+let dest_term x = x (* external [dest_term : term -> term'] = "%identity" *)
+let mk_op name params =
+ { op_name = name; op_params = params }
+
+let make_op x = x (* external [make_op : operator' -> operator] = "%identity" *)
+let dest_op x = x (* external [dest_op : operator -> operator'] = "%identity" *)
+let mk_bterm bvars term = { bvars = bvars; bterm = term }
+let make_bterm x = x (* external [make_bterm : bound_term' -> bound_term] = "%identity" *)
+let dest_bterm x = x (* external [dest_bterm : bound_term -> bound_term'] = "%identity" *)
+let make_param x = x (* external [make_param : param' -> param] = "%identity" *)
+let dest_param x = x (* external [dest_param : param -> param'] = "%identity" *)
+
+(*
+ * Operator names.
+ *)
+let opname_of_term = function
+ { term_op = { op_name = name } } ->
+ name
+
+(*
+ * Get the subterms.
+ * None of the subterms should be bound.
+ *)
+let subterms_of_term t =
+ List.map (fun { bterm = t } -> t) t.term_terms
+
+let subterm_count { term_terms = terms } =
+ List.length terms
+
+let subterm_arities { term_terms = terms } =
+ List.map (fun { bvars = vars } -> List.length vars) terms
+
+(*
+ * Manifest terms are injected into the "perv" module.
+ *)
+let xperv = make_opname ["Perv"]
+let sequent_opname = mk_opname "sequent" xperv
+
+(*
+ * Variables.
+ *)
+
+let var_opname = make_opname ["var"]
+
+(*
+ * See if a term is a variable.
+ *)
+let is_var_term = function
+ | { term_op = { op_name = opname; op_params = [Var v] };
+ term_terms = []
+ } when Opname.eq opname var_opname -> true
+ | _ ->
+ false
+
+(*
+ * Destructor for a variable.
+ *)
+let dest_var = function
+ | { term_op = { op_name = opname; op_params = [Var v] };
+ term_terms = []
+ } when Opname.eq opname var_opname -> v
+ | t ->
+ ref_raise(RefineError ("dest_var", TermMatchError (t, "not a variable")))
+(*
+ * Make a variable.
+ *)
+let mk_var_term v =
+ { term_op = { op_name = var_opname; op_params = [Var v] };
+ term_terms = []
+ }
+
+(*
+ * Simple terms
+ *)
+(*
+ * "Simple" terms have no parameters and no binding variables.
+ *)
+let is_simple_term_opname name = function
+ | { term_op = { op_name = name'; op_params = [] };
+ term_terms = bterms
+ } when Opname.eq name' name ->
+ let rec aux = function
+ | { bvars = []; bterm = _ }::t -> aux t
+ | _::t -> false
+ | [] -> true
+ in
+ aux bterms
+ | _ -> false
+
+let mk_any_term op terms =
+ let aux t =
+ { bvars = []; bterm = t }
+ in
+ { term_op = op; term_terms = List.map aux terms }
+
+let mk_simple_term name terms =
+ mk_any_term { op_name = name; op_params = [] } terms
+
+let dest_simple_term = function
+ | ({ term_op = { op_name = name; op_params = [] };
+ term_terms = bterms
+ } : term) as t ->
+ let aux = function
+ | { bvars = []; bterm = t } ->
+ t
+ | _ ->
+ ref_raise(RefineError ("dest_simple_term", TermMatchError (t, "binding vars exist")))
+ in
+ name, List.map aux bterms
+ | t ->
+ ref_raise(RefineError ("dest_simple_term", TermMatchError (t, "params exist")))
+
+let dest_simple_term_opname name = function
+ | ({ term_op = { op_name = name'; op_params = [] };
+ term_terms = bterms
+ } : term) as t ->
+ if Opname.eq name name' then
+ let aux = function
+ | { bvars = []; bterm = t } -> t
+ | _ -> ref_raise(RefineError ("dest_simple_term_opname", TermMatchError (t, "binding vars exist")))
+ in
+ List.map aux bterms
+ else
+ ref_raise(RefineError ("dest_simple_term_opname", TermMatchError (t, "opname mismatch")))
+ | t ->
+ ref_raise(RefineError ("dest_simple_term_opname", TermMatchError (t, "params exist")))
+
+(*
+ * Bound terms.
+ *)
+let mk_simple_bterm bterm =
+ { bvars = []; bterm = bterm }
+
+let dest_simple_bterm = function
+ | { bvars = []; bterm = bterm } ->
+ bterm
+ | _ ->
+ ref_raise(RefineError ("dest_simple_bterm", StringError ("bterm is not simple")))
+
+(* Copy from [term_op_std.ml]: *)
+(*i modified for Jprover, as a patch... i*)
+let mk_string_term opname s =
+ { term_op = { op_name = opname; op_params = [String s] }; term_terms = [] }
+
+(*i let mk_string_term opname s =
+ let new_opname={opname_token=opname.opname_token; opname_name=(List.tl opname.opname_name)@[s]} in
+ { term_op = { op_name = new_opname; op_params = [String (List.hd opname.opname_name)] }; term_terms = [] }
+i*)
+
+(* Copy from [term_subst_std.ml]: *)
+
+let rec free_vars_term gvars bvars = function
+ | { term_op = { op_name = opname; op_params = [Var v] }; term_terms = bterms } when Opname.eq opname var_opname ->
+ (* This is a variable *)
+ let gvars' =
+ if List.mem v bvars or List.mem v gvars then
+ gvars
+ else
+ v::gvars
+ in
+ free_vars_bterms gvars' bvars bterms
+ | { term_terms = bterms } ->
+ free_vars_bterms gvars bvars bterms
+ and free_vars_bterms gvars bvars = function
+ | { bvars = vars; bterm = term}::l ->
+ let bvars' = vars @ bvars in
+ let gvars' = free_vars_term gvars bvars' term in
+ free_vars_bterms gvars' bvars l
+ | [] ->
+ gvars
+
+let free_vars_list = free_vars_term [] []
+
+
+(* Termop: *)
+
+let is_no_subterms_term opname = function
+ | { term_op = { op_name = opname'; op_params = [] };
+ term_terms = []
+ } ->
+ Opname.eq opname' opname
+ | _ ->
+ false
+
+(*
+ * Terms with one subterm.
+ *)
+let is_dep0_term opname = function
+ | { term_op = { op_name = opname'; op_params = [] };
+ term_terms = [{ bvars = [] }]
+ } -> Opname.eq opname' opname
+ | _ -> false
+
+let mk_dep0_term opname t =
+ { term_op = { op_name = opname; op_params = [] };
+ term_terms = [{ bvars = []; bterm = t }]
+ }
+
+let dest_dep0_term opname = function
+ | { term_op = { op_name = opname'; op_params = [] };
+ term_terms = [{ bvars = []; bterm = t }]
+ } when Opname.eq opname' opname -> t
+ | t -> ref_raise(RefineError ("dest_dep0_term", TermMatchError (t, "not a dep0 term")))
+
+(*
+ * Terms with two subterms.
+ *)
+let is_dep0_dep0_term opname = function
+ | { term_op = { op_name = opname'; op_params = [] };
+ term_terms = [{ bvars = [] }; { bvars = [] }]
+ } -> Opname.eq opname' opname
+ | _ -> false
+
+let mk_dep0_dep0_term opname = fun
+ t1 t2 ->
+ { term_op = { op_name = opname; op_params = [] };
+ term_terms = [{ bvars = []; bterm = t1 };
+ { bvars = []; bterm = t2 }]
+ }
+
+let dest_dep0_dep0_term opname = function
+ | { term_op = { op_name = opname'; op_params = [] };
+ term_terms = [{ bvars = []; bterm = t1 };
+ { bvars = []; bterm = t2 }]
+ } when Opname.eq opname' opname -> t1, t2
+ | t -> ref_raise(RefineError ("dest_dep0_dep0_term", TermMatchError (t, "bad arity")))
+
+(*
+ * Bound term.
+ *)
+
+let is_dep0_dep1_term opname = function
+ | { term_op = { op_name = opname'; op_params = [] };
+ term_terms = [{ bvars = [] }; { bvars = [_] }]
+ } when Opname.eq opname' opname -> true
+ | _ -> false
+
+let is_dep0_dep1_any_term = function
+ | { term_op = { op_params = [] };
+ term_terms = [{ bvars = [] }; { bvars = [_] }]
+ } -> true
+ | _ -> false
+
+let mk_dep0_dep1_term opname = fun
+ v t1 t2 -> { term_op = { op_name = opname; op_params = [] };
+ term_terms = [{ bvars = []; bterm = t1 };
+ { bvars = [v]; bterm = t2 }]
+ }
+
+let dest_dep0_dep1_term opname = function
+ | { term_op = { op_name = opname'; op_params = [] };
+ term_terms = [{ bvars = []; bterm = t1 };
+ { bvars = [v]; bterm = t2 }]
+ } when Opname.eq opname' opname -> v, t1, t2
+ | t -> ref_raise(RefineError ("dest_dep0_dep1_term", TermMatchError (t, "bad arity")))
+
+let rec smap f = function
+ | [] -> []
+ | (hd::tl) as l ->
+ let hd' = f hd in
+ let tl' = smap f tl in
+ if (hd==hd')&&(tl==tl') then l else hd'::tl'
+
+let rec try_check_assoc v v' = function
+ | [] -> raise Not_found
+ | (v1,v2)::tl ->
+ begin match v=v1, v'=v2 with
+ | true, true -> true
+ | false, false -> try_check_assoc v v' tl
+ | _ -> false
+ end
+
+let rec zip_list l l1 l2 = match (l1,l2) with
+ | (h1::t1), (h2::t2) ->
+ zip_list ((h1,h2)::l) t1 t2
+ | [], [] ->
+ l
+ | _ -> raise (Failure "Term.zip_list")
+
+let rec assoc_in_range eq y = function
+ | (_, y')::tl ->
+ (eq y y') || (assoc_in_range eq y tl)
+ | [] ->
+ false
+
+let rec check_assoc v v' = function
+ | [] -> v=v'
+ | (v1,v2)::tl ->
+ begin match v=v1, v'=v2 with
+ | true, true -> true
+ | false, false -> check_assoc v v' tl
+ | _ -> false
+ end
+
+let rec zip a b = match (a,b) with
+ | (h1::t1), (h2::t2) ->
+ (h1, h2) :: zip t1 t2
+ | [], [] ->
+ []
+ |
+ _ -> raise (Failure "Term.zip")
+
+let rec for_all2 f l1 l2 =
+ match (l1,l2) with
+ | h1::t1, h2::t2 -> for_all2 f t1 t2 & f h1 h2
+ | [], [] -> true
+ | _ -> false
+
+let newname v i =
+ v ^ "_" ^ (string_of_int i)
+
+let rec new_var v avoid i =
+ let v' = newname v i in
+ if avoid v'
+ then new_var v avoid (succ i)
+ else v'
+
+let vnewname v avoid = new_var v avoid 1
+
+let rev_mem a b = List.mem b a
+
+let rec find_index_aux v i = function
+ | h::t ->
+ if h = v then
+ i
+ else
+ find_index_aux v (i + 1) t
+ | [] ->
+ raise Not_found
+
+let find_index v l = find_index_aux v 0 l
+
+let rec remove_elements l1 l2 =
+ match l1, l2 with
+ | flag::ft, h::t ->
+ if flag then
+ remove_elements ft t
+ else
+ h :: remove_elements ft t
+ | _, l ->
+ l
+
+let rec subtract l1 l2 =
+ match l1 with
+ | h::t ->
+ if List.mem h l2 then
+ subtract t l2
+ else
+ h :: subtract t l2
+ | [] ->
+ []
+
+let rec fv_mem fv v =
+ match fv with
+ | [] -> false
+ | h::t ->
+ List.mem v h || fv_mem t v
+
+let rec new_vars fv = function
+ | [] -> []
+ | v::t ->
+ (* Rename the first one, then add it to free vars *)
+ let v' = vnewname v (fv_mem fv) in
+ v'::(new_vars ([v']::fv) t)
+
+let rec fsubtract l = function
+ | [] -> l
+ | h::t ->
+ fsubtract (subtract l h) t
+
+let add_renames_fv r l =
+ let rec aux = function
+ | [] -> l
+ | v::t -> [v]::(aux t)
+ in
+ aux r
+
+let add_renames_terms r l =
+ let rec aux = function
+ | [] -> l
+ | v::t -> (mk_var_term v)::(aux t)
+ in
+ aux r
+
+(*
+ * First order simultaneous substitution.
+ *)
+let rec subst_term terms fv vars = function
+ | { term_op = { op_name = opname; op_params = [Var(v)] }; term_terms = [] } as t
+ when Opname.eq opname var_opname->
+ (* Var case *)
+ begin
+ try List.nth terms (find_index v vars) with
+ Not_found ->
+ t
+ end
+ | { term_op = op; term_terms = bterms } ->
+ (* Other term *)
+ { term_op = op; term_terms = subst_bterms terms fv vars bterms }
+
+and subst_bterms terms fv vars bterms =
+ (* When subst through bterms, catch binding occurrences *)
+ let rec subst_bterm = function
+ | { bvars = []; bterm = term } ->
+ (* Optimize the common case *)
+ { bvars = []; bterm = subst_term terms fv vars term }
+
+ | { bvars = bvars; bterm = term } ->
+ (* First subtract bound instances *)
+ let flags = List.map (function v -> List.mem v bvars) vars in
+ let vars' = remove_elements flags vars in
+ let fv' = remove_elements flags fv in
+ let terms' = remove_elements flags terms in
+
+ (* If any of the binding variables are free, rename them *)
+ let renames = subtract bvars (fsubtract bvars fv') in
+ if renames <> [] then
+ let fv'' = (free_vars_list term)::fv' in
+ let renames' = new_vars fv'' renames in
+ { bvars = subst_bvars renames' renames bvars;
+ bterm = subst_term
+ (add_renames_terms renames' terms')
+ (add_renames_fv renames' fv')
+ (renames @ vars')
+ term
+ }
+ else
+ { bvars = bvars;
+ bterm = subst_term terms' fv' vars' term
+ }
+ in
+ List.map subst_bterm bterms
+
+and subst_bvars renames' renames bvars =
+ let subst_bvar v =
+ try List.nth renames' (find_index v renames) with
+ Not_found -> v
+ in
+ List.map subst_bvar bvars
+
+let subst term vars terms =
+ subst_term terms (List.map free_vars_list terms) vars term
+
+(*i bug!!! in the [term_std] module
+ let subst1 t var term =
+ let fv = free_vars_list term in
+ if List.mem var fv then
+ subst_term [term] [fv] [var] t
+ else
+ t
+The following is the correct implementation
+i*)
+
+let subst1 t var term =
+if List.mem var (free_vars_list t) then
+ subst_term [term] [free_vars_list term] [var] t
+else
+ t
+
+let apply_subst t s =
+ let vs,ts = List.split s in
+ subst t vs ts
+
+let rec equal_params p1 p2 =
+ match p1, p2 with
+ | Number n1, Number n2 ->
+ n1 = n2
+ | ParamList pl1, ParamList pl2 ->
+ List.for_all2 equal_params pl1 pl2
+ | _ ->
+ p1 = p2
+
+let rec equal_term vars t t' =
+ match t, t' with
+ | { term_op = { op_name = opname1; op_params = [Var v] };
+ term_terms = []
+ },
+ { term_op = { op_name = opname2; op_params = [Var v'] };
+ term_terms = []
+ } when Opname.eq opname1 var_opname & Opname.eq opname2 var_opname ->
+ check_assoc v v' vars
+ | { term_op = { op_name = name1; op_params = params1 }; term_terms = bterms1 },
+ { term_op = { op_name = name2; op_params = params2 }; term_terms = bterms2 } ->
+ (Opname.eq name1 name2)
+ & (for_all2 equal_params params1 params2)
+ & (equal_bterms vars bterms1 bterms2)
+and equal_bterms vars bterms1 bterms2 =
+ let equal_bterm = fun
+ { bvars = bvars1; bterm = term1 }
+ { bvars = bvars2; bterm = term2 } ->
+ equal_term (zip_list vars bvars1 bvars2) term1 term2
+ in
+ for_all2 equal_bterm bterms1 bterms2
+
+
+let alpha_equal t1 t2 =
+ try equal_term [] t1 t2 with Failure _ -> false
+
+let var_subst t t' v =
+ let { term_op = { op_name = opname } } = t' in
+ let vt = mk_var_term v in
+ let rec subst_term = function
+ { term_op = { op_name = opname'; op_params = params };
+ term_terms = bterms
+ } as t ->
+ (* Check if this is the same *)
+ if Opname.eq opname' opname & alpha_equal t t' then
+ vt
+ else
+ { term_op = { op_name = opname'; op_params = params };
+ term_terms = List.map subst_bterm bterms
+ }
+
+ and subst_bterm { bvars = vars; bterm = term } =
+ if List.mem v vars then
+ let av = vars @ (free_vars_list term) in
+ let v' = vnewname v (fun v -> List.mem v av) in
+ let rename var = if var = v then v' else var in
+ let term = subst1 term v (mk_var_term v') in
+ { bvars = smap rename vars; bterm = subst_term term }
+ else
+ { bvars = vars; bterm = subst_term term }
+ in
+ subst_term t
+
+let xnil_opname = mk_opname "nil" xperv
+let xnil_term = mk_simple_term xnil_opname []
+let is_xnil_term = is_no_subterms_term xnil_opname
+
+(*c End of the extraction from Meta-Prl *)
+
+(* Huang's modification: *)
+let all_opname = make_opname ["quantifier";"all"]
+let is_all_term = is_dep0_dep1_term all_opname
+let dest_all = dest_dep0_dep1_term all_opname
+let mk_all_term = mk_dep0_dep1_term all_opname
+
+let exists_opname = make_opname ["quantifier";"exst"]
+let is_exists_term = is_dep0_dep1_term exists_opname
+let dest_exists = dest_dep0_dep1_term exists_opname
+let mk_exists_term = mk_dep0_dep1_term exists_opname
+
+let or_opname = make_opname ["connective";"or"]
+let is_or_term = is_dep0_dep0_term or_opname
+let dest_or = dest_dep0_dep0_term or_opname
+let mk_or_term = mk_dep0_dep0_term or_opname
+
+let and_opname = make_opname ["connective";"and"]
+let is_and_term = is_dep0_dep0_term and_opname
+let dest_and = dest_dep0_dep0_term and_opname
+let mk_and_term = mk_dep0_dep0_term and_opname
+
+let cor_opname = make_opname ["connective";"cor"]
+let is_cor_term = is_dep0_dep0_term cor_opname
+let dest_cor = dest_dep0_dep0_term cor_opname
+let mk_cor_term = mk_dep0_dep0_term cor_opname
+
+let cand_opname = make_opname ["connective";"cand"]
+let is_cand_term = is_dep0_dep0_term cand_opname
+let dest_cand = dest_dep0_dep0_term cand_opname
+let mk_cand_term = mk_dep0_dep0_term cand_opname
+
+let implies_opname = make_opname ["connective";"=>"]
+let is_implies_term = is_dep0_dep0_term implies_opname
+let dest_implies = dest_dep0_dep0_term implies_opname
+let mk_implies_term = mk_dep0_dep0_term implies_opname
+
+let iff_opname = make_opname ["connective";"iff"]
+let is_iff_term = is_dep0_dep0_term iff_opname
+let dest_iff = dest_dep0_dep0_term iff_opname
+let mk_iff_term = mk_dep0_dep0_term iff_opname
+
+let not_opname = make_opname ["connective";"not"]
+let is_not_term = is_dep0_term not_opname
+let dest_not = dest_dep0_term not_opname
+let mk_not_term = mk_dep0_term not_opname
+
+let var_ = mk_var_term
+let fun_opname = make_opname ["function"]
+let fun_ f ts = mk_any_term {op_name = fun_opname; op_params = [String f] } ts
+
+let is_fun_term = function
+ | { term_op = { op_name = opname; op_params = [String f] }}
+ when Opname.eq opname fun_opname -> true
+ | _ ->
+ false
+
+let dest_fun = function
+ | { term_op = { op_name = opname; op_params = [String f] }; term_terms = ts}
+ when Opname.eq opname fun_opname -> (f, List.map (fun { bterm = t } -> t) ts)
+ | t ->
+ ref_raise(RefineError ("dest_fun", TermMatchError (t, "not a function symbol")))
+
+let const_ c = fun_ c []
+let is_const_term = function
+ | { term_op = { op_name = opname; op_params = [String f] }; term_terms = [] }
+ when Opname.eq opname fun_opname -> true
+ | _ ->
+ false
+
+let dest_const t =
+ let (n, ts) = dest_fun t in n
+
+let pred_opname = make_opname ["predicate"]
+let pred_ p ts = mk_any_term {op_name = pred_opname; op_params = [String p] } ts
+
+let not_ = mk_not_term
+let and_ = mk_and_term
+let or_ = mk_or_term
+let imp_ = mk_implies_term
+let cand_ = mk_cand_term
+let cor_ = mk_cor_term
+let iff_ = mk_iff_term
+let nil_term = {term_op={op_name=nil_opname; op_params=[]}; term_terms=[] }
+let forall v t = mk_all_term v nil_term t
+let exists v t= mk_exists_term v nil_term t
+let rec wbin op = function
+ | [] -> raise (Failure "Term.wbin")
+ | [t] -> t
+ | t::r -> op t (wbin op r)
+
+let wand_ = wbin and_
+let wor_ = wbin or_
+let wimp_ = wbin imp_
+
+(*i let true_opname = make_opname ["bool";"true"]
+let is_true_term = is_no_subterms_term true_opname
+let true_ = mk_simple_term true_opname []
+let false_ = not_ true_
+
+let is_false_term t =
+ if is_not_term t then
+ let t1 = dest_not t in
+ is_true_term t1
+ else
+ false
+i*)
+
+let dummy_false_ = mk_simple_term (make_opname ["bool";"false"]) []
+let dummy_true_ = mk_simple_term (make_opname ["bool";"true"]) []
+let false_ = and_ (dummy_false_) (not_ dummy_false_)
+let true_ = not_ (and_ (dummy_true_) (not_ dummy_true_))
+
+let is_false_term t =
+ if (alpha_equal t false_) then true
+ else false
+
+let is_true_term t =
+ if (alpha_equal t true_) then true
+ else false
+
+(* Print a term [t] via the [ostream]: *)
+let rec fprint_term ostream t prec =
+ let l_print op_prec =
+ if (prec > op_prec) then fprintf ostream "(" in
+ let r_print op_prec =
+ if (prec > op_prec) then fprintf ostream ")" in
+ if is_false_term t then (* false *)
+ fprint_str_list ostream ["False"]
+ else if is_true_term t then (* true *)
+ fprint_str_list ostream ["True"]
+ else if is_all_term t then (* for all *)
+ let v, t1, t2 = dest_all t in
+ fprint_str_list ostream ["A."^v];
+ fprint_term ostream t2 4
+ else if is_exists_term t then (* exists *)
+ let v, t1, t2 = dest_exists t in
+ fprint_str_list ostream ["E."^v];
+ fprint_term ostream t2 4 (* implication *)
+ else if is_implies_term t then
+ let t1, t2 = dest_implies t in
+ l_print 0;
+ fprint_term ostream t1 1;
+ fprint_str_list ostream ["=>"];
+ fprint_term ostream t2 0;
+ r_print 0
+ else if is_and_term t then (* logical and *)
+ let t1, t2 = dest_and t in
+ l_print 3;
+ fprint_term ostream t1 3;
+ fprint_str_list ostream ["&"];
+ fprint_term ostream t2 3;
+ r_print 3
+ else if is_or_term t then (* logical or *)
+ let t1, t2 = dest_or t in
+ l_print 2;
+ fprint_term ostream t1 2;
+ fprint_str_list ostream ["|"];
+ fprint_term ostream t2 2;
+ r_print 2
+ else if is_not_term t then (* logical not *)
+ let t2 = dest_not t in
+ fprint_str_list ostream ["~"];
+ fprint_term ostream t2 4 (* nil term *)
+ else if is_xnil_term t then
+ fprint_str_list ostream ["NIL"]
+ else match t with (* other cases *)
+ { term_op = { op_name = opname; op_params = opparm }; term_terms = bterms} ->
+ if (Opname.eq opname pred_opname) || (Opname.eq opname fun_opname) then
+ begin
+ fprint_param_list ostream opparm;
+ if bterms != [] then
+ begin
+ fprintf ostream "(";
+ fprint_bterm_list ostream prec bterms;
+ fprintf ostream ")";
+ end
+ end else
+ begin
+ fprintf ostream "[";
+(* fprint_opname ostream opname;
+ fprintf ostream ": "; *)
+ fprint_param_list ostream opparm;
+ if bterms != [] then
+ begin
+ fprintf ostream "(";
+ fprint_bterm_list ostream prec bterms;
+ fprintf ostream ")";
+ end;
+ fprintf ostream "]"
+ end
+and fprint_bterm_list ostream prec = function
+ | [] -> ()
+ | {bvars=bv; bterm=bt}::r ->
+ fprint_str_list ostream bv;
+ fprint_term ostream bt prec;
+ if (r<>[]) then fprint_str_list ostream [","];
+ fprint_bterm_list ostream prec r
+;;
+
+
+let print_term ostream t =
+ Format.print_flush ();
+ fprint_term ostream t 0;
+ Format.print_flush ()
+
+let print_error_msg = function
+ | RefineError(s,e) -> print_string ("(module "^s^") ");
+ begin
+ match e with
+ | TermMatchError(t,s) -> print_term stdout t; print_string (s^"\n")
+ | StringError s -> print_string (s^"\n")
+ end
+ | ue -> print_string "Unexpected error for Jp.\n";
+ raise ue
+
+
+(* Naive implementation for [jterm] substitution, unification, etc.: *)
+let substitute subst term =
+ apply_subst term subst
+
+(* A naive unification algorithm: *)
+let compsubst subst1 subst2 =
+ (List.map (fun (v, t) -> (v, substitute subst1 t)) subst2) @ subst1
+;;
+
+let rec extract_terms = function
+ | [] -> []
+ | h::r -> let {bvars=_; bterm=bt}=h in bt::extract_terms r
+
+(* Occurs check: *)
+let occurs v t =
+ let rec occur_rec t =
+ if is_var_term t then v=dest_var t
+ else let { term_op = _ ; term_terms = bterms} = t in
+ let sons = extract_terms bterms in
+ List.exists occur_rec sons
+ in
+ occur_rec t
+
+(* The naive unification algorithm: *)
+let rec unify2 (term1,term2) =
+ if is_var_term term1 then
+ if equal_term [] term1 term2 then []
+ else let v1 = dest_var term1 in
+ if occurs v1 term2 then raise (RefineError ("unify1", StringError ("1")))
+ else [v1,term2]
+ else if is_var_term term2 then
+ let v2 = dest_var term2 in
+ if occurs v2 term1 then raise (RefineError ("unify2", StringError ("2")))
+ else [v2,term1]
+ else
+ let { term_op = { op_name = opname1; op_params = params1 };
+ term_terms = bterms1
+ } = term1
+ in
+ let { term_op = { op_name = opname2; op_params = params2 };
+ term_terms = bterms2
+ } = term2
+ in
+ if Opname.eq opname1 opname2 & params1 = params2 then
+ let sons1 = extract_terms bterms1
+ and sons2 = extract_terms bterms2 in
+ List.fold_left2
+ (fun s t1 t2 -> compsubst
+ (unify2 (substitute s t1, substitute s t2)) s)
+ [] sons1 sons2
+ else raise (RefineError ("unify3", StringError ("3")))
+
+let unify term1 term2 = unify2 (term1, term2)
+let unify_mm term1 term2 _ = unify2 (term1, term2)
diff --git a/contrib/jprover/jterm.mli b/contrib/jprover/jterm.mli
new file mode 100644
index 00000000..0bc42010
--- /dev/null
+++ b/contrib/jprover/jterm.mli
@@ -0,0 +1,110 @@
+(* This module is modified and extracted from Meta-Prl. *)
+
+(* Definitions of [jterm]: *)
+type param = param'
+and operator = operator'
+and term = term'
+and bound_term = bound_term'
+and param' =
+ | Number of int
+ | String of string
+ | Token of string
+ | Var of string
+ | ParamList of param list
+and operator' = { op_name : Opname.opname; op_params : param list; }
+and term' = { term_op : operator; term_terms : bound_term list; }
+and bound_term' = { bvars : string list; bterm : term; }
+type term_subst = (string * term) list
+
+type error_msg = TermMatchError of term * string | StringError of string
+
+exception RefineError of string * error_msg
+
+(* Collect free variables: *)
+val free_vars_list : term -> string list
+
+(* Substitutions: *)
+val subst_term : term list -> string list list -> string list -> term -> term
+val subst : term -> string list -> term list -> term
+val subst1 : term -> string -> term -> term
+val var_subst : term -> term -> string -> term
+val apply_subst : term -> (string * term) list -> term
+
+(* Unification: *)
+val unify_mm : term -> term -> 'a -> (string * term) list
+
+val xnil_term : term'
+
+(* Testing functions: *)
+val is_xnil_term : term' -> bool
+val is_var_term : term' -> bool
+val is_true_term : term' -> bool
+val is_false_term : term' -> bool
+val is_all_term : term' -> bool
+val is_exists_term : term' -> bool
+val is_or_term : term' -> bool
+val is_and_term : term' -> bool
+val is_cor_term : term' -> bool
+val is_cand_term : term' -> bool
+val is_implies_term : term' -> bool
+val is_iff_term : term' -> bool
+val is_not_term : term' -> bool
+val is_fun_term : term -> bool
+val is_const_term : term -> bool
+
+
+(* Constructors for [jterms]: *)
+val var_ : string -> term'
+val fun_ : string -> term list -> term'
+val const_ : string -> term'
+val pred_ : string -> term list -> term'
+val not_ : term -> term'
+val and_ : term -> term -> term'
+val or_ : term -> term -> term'
+val imp_ : term -> term -> term'
+val cand_ : term -> term -> term'
+val cor_ : term -> term -> term'
+val iff_ : term -> term -> term'
+val false_ : term'
+val true_ : term'
+val nil_term : term'
+val forall : string -> term -> term'
+val exists : string -> term -> term'
+
+
+(* Destructors for [jterm]: *)
+val dest_var : term -> string
+val dest_fun : term -> string * term list
+val dest_const : term -> string
+val dest_not : term -> term
+val dest_iff : term -> term * term
+val dest_implies : term -> term * term
+val dest_cand : term -> term * term
+val dest_cor : term -> term * term
+val dest_and : term -> term * term
+val dest_or : term -> term * term
+val dest_exists : term -> string * term * term
+val dest_all : term -> string * term * term
+
+(* Wide-logical connectives: *)
+val wand_ : term list -> term
+val wor_ : term list -> term
+val wimp_ : term list -> term
+
+(* Printing and debugging tools: *)
+val fprint_str_list : out_channel -> string list -> unit
+val mbreak : string -> unit
+val print_strs : string list -> unit
+val print_term : out_channel -> term -> unit
+val print_error_msg : exn -> unit
+
+(* Other exported functions for [jall.ml]: *)
+val make_term : 'a -> 'a
+val dest_term : 'a -> 'a
+val make_op : 'a -> 'a
+val dest_op : 'a -> 'a
+val make_bterm : 'a -> 'a
+val dest_bterm : 'a -> 'a
+val dest_param : 'a -> 'a
+val mk_var_term : string -> term'
+val mk_string_term : Opname.opname -> string -> term'
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 *)
diff --git a/contrib/jprover/jtunify.mli b/contrib/jprover/jtunify.mli
new file mode 100644
index 00000000..0aabc79e
--- /dev/null
+++ b/contrib/jprover/jtunify.mli
@@ -0,0 +1,35 @@
+exception Not_unifiable
+exception Failed
+
+(* Utilities *)
+
+val is_const : string -> bool
+val is_var : string -> bool
+val r_1 : 'a list -> 'b list -> 'c list -> bool
+val r_2 : 'a list -> 'b list -> 'c list -> bool
+val r_3 : 'a list -> 'b list -> 'a list -> bool
+val r_4 : string list -> 'a list -> string list -> bool
+val r_5 : string list -> 'a -> 'b list -> bool
+val r_6 : string list -> 'a list -> string list -> bool
+val r_7 : string list -> 'a -> string list -> bool
+val r_8 : string list -> 'a list -> string list -> bool
+val r_9 : string list -> 'a list -> string list -> bool
+val r_10 : string list -> 'a -> string list -> bool
+val com_subst : 'a list -> 'a * 'a list -> 'a list
+
+(* Debugging *)
+
+val print_equations : (string list * (string list * string list)) list -> unit
+
+val print_tunify : int * (string * string list) list -> unit
+
+(* Main function *)
+
+val do_stringunify : string list ->
+ string list ->
+ string ->
+ string ->
+ (string list * (string list * string list)) list ->
+ (int * (string * string list) list) * (* unifier *)
+ (int * ((string list * (string list * string list)) list)) (* applied new eqlist *)
+
diff --git a/contrib/jprover/opname.ml b/contrib/jprover/opname.ml
new file mode 100644
index 00000000..d0aa9046
--- /dev/null
+++ b/contrib/jprover/opname.ml
@@ -0,0 +1,90 @@
+open Printf
+
+type token = string
+type atom = string list
+
+let opname_token = String.make 4 (Char.chr 0)
+
+type opname =
+ { mutable opname_token : token;
+ mutable opname_name : string list
+ }
+
+let (optable : (string list, opname) Hashtbl.t) = Hashtbl.create 97
+
+(* * Constructors.*)
+let nil_opname = { opname_token = opname_token; opname_name = [] }
+
+let _ = Hashtbl.add optable [] nil_opname
+
+let rec mk_opname s ({ opname_token = token; opname_name = name } as opname) =
+ if token == opname_token then
+ let name = s :: name in
+ try Hashtbl.find optable name with
+ Not_found ->
+ let op = { opname_token = opname_token; opname_name = name } in
+ Hashtbl.add optable name op;
+ op
+ else
+ mk_opname s (normalize_opname opname)
+
+and make_opname = function
+ | [] ->
+ nil_opname
+ | h :: t ->
+ mk_opname h (make_opname t)
+
+and normalize_opname opname =
+ if opname.opname_token == opname_token then
+ (* This opname is already normalized *)
+ opname
+ else
+ let res = make_opname opname.opname_name
+ in
+ opname.opname_name <- res.opname_name;
+ opname.opname_token <- opname_token;
+ res
+
+(* * Atoms are the inner string list. *)
+let intern opname =
+ if opname.opname_token == opname_token then
+ opname.opname_name
+ else
+ let name = (normalize_opname opname).opname_name in
+ opname.opname_token <- opname_token;
+ opname.opname_name <- name;
+ name
+
+let eq_inner op1 op2 =
+ op1.opname_name <- (normalize_opname op1).opname_name;
+ op1.opname_token <- opname_token;
+ op2.opname_name <- (normalize_opname op2).opname_name;
+ op2.opname_token <- opname_token;
+ op1.opname_name == op2.opname_name
+
+let eq op1 op2 =
+ (op1.opname_name == op2.opname_name)
+ or ((op1.opname_token != opname_token or op2.opname_token != opname_token) & eq_inner op1 op2)
+
+(* * Destructor. *)
+let dst_opname = function
+ | { opname_name = n :: name } -> n, { opname_token = opname_token; opname_name = name }
+ | _ -> raise (Invalid_argument "dst_opname")
+
+let dest_opname { opname_name = name } =
+ name
+
+let string_of_opname op =
+ let rec flatten = function
+ | [] ->
+ ""
+ | h::t ->
+ let rec collect s = function
+ | h::t ->
+ collect (h ^ "!" ^ s) t
+ | [] ->
+ s
+ in
+ collect h t
+ in
+ flatten op.opname_name
diff --git a/contrib/jprover/opname.mli b/contrib/jprover/opname.mli
new file mode 100644
index 00000000..56bf84e2
--- /dev/null
+++ b/contrib/jprover/opname.mli
@@ -0,0 +1,15 @@
+(* This module is extracted from Meta-Prl. *)
+
+type token = string
+and atom = string list
+val opname_token : token
+type opname = {
+ mutable opname_token : token;
+ mutable opname_name : string list;
+}
+val nil_opname : opname
+val mk_opname : string -> opname -> opname
+val make_opname : string list -> opname
+val eq : opname -> opname -> bool
+val dest_opname : opname -> string list
+val string_of_opname : opname -> string
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 07:36:46 +0000