diff options
Diffstat (limited to 'contrib/jprover/jall.ml')
| -rw-r--r-- | contrib/jprover/jall.ml | 4599 |
1 files changed, 0 insertions, 4599 deletions
diff --git a/contrib/jprover/jall.ml b/contrib/jprover/jall.ml deleted file mode 100644 index a9ebe5b6..00000000 --- a/contrib/jprover/jall.ml +++ /dev/null @@ -1,4599 +0,0 @@ -(* - * 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> - *) - -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 ["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 *) - - 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 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) - - 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 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 - let new_ordering = add_arrowsQ v dterms ordering in - 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 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 - let new_term = subst1 inter_term "dummy" new_t in - 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 - 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 - -(* 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 - -(**************************************************************) - -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 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 - -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 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; - 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 *) |