(* * 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 * Modified by: Aleksey Nogin *) (*: All of Huang's modifications of this file are quoted or denoted by comments followed by a colon. :*) (*: open Mp_debug open Refiner.Refiner open Term open TermType open TermOp open TermSubst open TermMan open RefineError open Opname :*) open Jterm open Opname open Jlogic open Jtunify let ruletable = Jlogic.ruletable (*: let free_var_op = make_opname ["free_variable";"Jprover"] let jprover_op = make_opname ["string";"Jprover"] :*) let free_var_op = make_opname ["free_variable"; "Jprover"] let jprover_op = make_opname ["jprover"; "string"] module JProver (JLogic : JLogicSig) = struct type polarity = I | O type connective = And | Or | Neg | Imp | All | Ex | At | Null type ptype = Alpha | Beta | Gamma | Delta | Phi | Psi | PNull type stype = Alpha_1 | Alpha_2 | Beta_1 | Beta_2 | Gamma_0 | Delta_0 | Phi_0 | Psi_0 | PNull_0 type pos = {name : string; address : int list; op : connective; pol : polarity; pt : ptype; st : stype; label : term} type 'pos ftree = Empty | NodeAt of 'pos | NodeA of 'pos * ('pos ftree) array type atom = {aname : string; aaddress : int list; aprefix : string list; apredicate : operator; apol : polarity; ast : stype; alabel : term} type atom_relations = atom * atom list * atom list (* all atoms except atom occur in [alpha_set] and [beta_set] of atom*) (* beta proofs *) type bproof = BEmpty | RNode of string list * bproof | CNode of (string * string) | BNode of string * (string list * bproof) * (string list * bproof) | AtNode of string * (string * string) (* Assume only constants for instantiations, not adapted to terms yet *) type inf = rule * term * term (* proof tree for pretty print and permutation *) type 'inf ptree = PEmpty | PNodeAx of 'inf | PNodeA of 'inf * 'inf ptree | PNodeB of 'inf * 'inf ptree * 'inf ptree module OrderedAtom = struct type t = atom let compare a1 a2 = if (a1.aname) = (a2.aname) then 0 else if (a1.aname) < (a2.aname) then -1 else 1 end module AtomSet = Set.Make(OrderedAtom) module OrderedString = struct type t = string let compare a1 a2 = if a1 = a2 then 0 else if a1 < a2 then -1 else 1 end module StringSet = Set.Make(OrderedString) (*i let _ = show_loading "Loading Jall%t" i*) let debug_jprover = create_debug (**) { debug_name = "jprover"; debug_description = "Display Jprover operations"; debug_value = false } let jprover_bug = Invalid_argument "Jprover bug (Jall module)" (*****************************************************************) (************* printing function *************************************) (************ printing T-string unifiers ****************************) (* ******* printing ********** *) let rec list_to_string s = match s with [] -> "" | f::r -> f^"."^(list_to_string r) let rec print_eqlist eqlist = match eqlist with [] -> print_endline "" | (atnames,f)::r -> let (s,t) = f in let ls = list_to_string s and lt = list_to_string t in begin print_endline ("Atom names: "^(list_to_string atnames)); print_endline (ls^" = "^lt); print_eqlist r end let print_equations eqlist = begin Format.open_box 0; Format.force_newline (); print_endline "Equations:"; print_eqlist eqlist; Format.force_newline (); end let rec print_subst sigma = match sigma with [] -> print_endline "" | f::r -> let (v,s) = f in let ls = list_to_string s in begin print_endline (v^" = "^ls); print_subst r end let print_tunify sigma = let (n,subst) = sigma in begin print_endline " "; print_endline ("MaxVar = "^(string_of_int (n-1))); print_endline " "; print_endline "Substitution:"; print_subst subst; print_endline " " end (*****************************************************) (********* printing atoms and their relations ***********************) let print_stype st = match st with Alpha_1 -> Format.print_string "Alpha_1" | Alpha_2 -> Format.print_string "Alpha_2" | Beta_1 -> Format.print_string "Beta_1" | Beta_2 -> Format.print_string "Beta_2" | Gamma_0 -> Format.print_string "Gamma_0" | Delta_0 -> Format.print_string "Delta_0" | Phi_0 -> Format.print_string "Phi_0" | Psi_0 -> Format.print_string "Psi_0" | PNull_0 -> Format.print_string "PNull_0" let print_pol pol = if pol = O then Format.print_string "O" else Format.print_string "I" let rec print_address int_list = match int_list with [] -> Format.print_string "" | hd::rest -> begin Format.print_int hd; print_address rest end let rec print_prefix prefix_list = match prefix_list with [] -> Format.print_string "" | f::r -> begin Format.print_string f; print_prefix r end let print_atom at tab = let ({aname=x; aaddress=y; aprefix=z; apredicate=p; apol=a; ast=b; alabel=label}) = at in begin Format.print_string ("{aname="^x^"; address="); print_address y; Format.print_string "; "; Format.force_newline (); Format.print_break (tab+1) (tab+1); Format.print_string "prefix="; print_prefix z; Format.print_string "; predicate=; "; 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=[]"; Format.print_string "\n alabel="; print_term stdout label; Format.print_string "}" end let rec print_atom_list set tab = match set with [] -> Format.print_string "" | (f::r) -> begin Format.force_newline (); Format.print_break (tab) (tab); print_atom f tab; print_atom_list r (tab) end let rec print_atom_info atom_relation = match atom_relation with [] -> Format.print_string "" | (a,b,c)::r -> begin Format.print_string "atom:"; Format.force_newline (); Format.print_break 3 3; print_atom a 3; Format.force_newline (); Format.print_break 0 0; Format.print_string "alpha_set:"; print_atom_list b 3; Format.force_newline (); Format.print_break 0 0; Format.print_string "beta_set:"; print_atom_list c 3; Format.force_newline (); Format.force_newline (); Format.print_break 0 0; print_atom_info r end (*************** print formula tree, tree ordering etc. ***********) let print_ptype pt = match pt with Alpha -> Format.print_string "Alpha" | Beta -> Format.print_string "Beta" | Gamma -> Format.print_string "Gamma" | Delta -> Format.print_string "Delta" | Phi -> Format.print_string "Phi" | Psi -> Format.print_string "Psi" | PNull -> Format.print_string "PNull" let print_op op = match op with At -> Format.print_string "Atom" | Neg -> Format.print_string "Neg" | And -> Format.print_string "And" | Or -> Format.print_string "Or" | Imp -> Format.print_string "Imp" | Ex -> Format.print_string "Ex" | All -> Format.print_string "All" | Null -> Format.print_string "Null" let print_position position tab = let ({name=x; address=y; op=z; pol=a; pt=b; st=c; label=t}) = position in begin Format.print_string ("{name="^x^"; address="); print_address y; Format.print_string "; "; Format.force_newline (); Format.print_break (tab+1) 0; (* Format.print_break 0 3; *) Format.print_string "op="; print_op z; Format.print_string "; pol="; print_pol a; Format.print_string "; ptype="; print_ptype b; Format.print_string "; stype="; print_stype c; Format.print_string ";"; Format.force_newline (); Format.print_break (tab+1) 0; Format.print_string "label="; Format.print_break 0 0; Format.force_newline (); Format.print_break tab 0; print_term stdout t; Format.print_string "}" end let rec pp_ftree_list tree_list tab = let rec pp_ftree ftree new_tab = let dummy = String.make (new_tab-2) ' ' in match ftree with Empty -> Format.print_string "" | NodeAt(position) -> begin Format.force_newline (); Format.print_break new_tab 0; print_string (dummy^"AtomNode: "); (* Format.force_newline (); Format.print_break 0 3; *) print_position position new_tab; Format.force_newline (); Format.print_break new_tab 0 end | NodeA(position,subtrees) -> let tree_list = Array.to_list subtrees in begin Format.force_newline (); Format.print_break new_tab 0; Format.print_break 0 0; print_string (dummy^"InnerNode: "); print_position position new_tab; Format.force_newline (); Format.print_break 0 0; pp_ftree_list tree_list (new_tab-3) end in let new_tab = tab+5 in match tree_list with [] -> Format.print_string "" | first::rest -> begin pp_ftree first new_tab; pp_ftree_list rest tab end let print_ftree ftree = begin Format.open_box 0; Format.print_break 3 0; pp_ftree_list [ftree] 0; Format.print_flush () end let rec stringlist_to_string stringlist = match stringlist with [] -> "." | f::r -> let rest_s = stringlist_to_string r in (f^"."^rest_s) let rec print_stringlist slist = match slist with [] -> Format.print_string "" | f::r -> begin Format.print_string (f^"."); print_stringlist r end let rec pp_bproof_list tree_list tab = let rec pp_bproof ftree new_tab = let dummy = String.make (new_tab-2) ' ' in match ftree with BEmpty -> Format.print_string "" | CNode((c1,c2)) -> begin Format.open_box 0; Format.force_newline (); Format.print_break (new_tab-10) 0; Format.open_box 0; Format.force_newline (); Format.print_string (dummy^"CloseNode: connection = ("^c1^","^c2^")"); Format.print_flush(); (* Format.force_newline (); Format.print_break 0 3; *) Format.open_box 0; Format.print_break new_tab 0; Format.print_flush() end | AtNode(posname,(c1,c2)) -> begin Format.open_box 0; Format.force_newline (); Format.print_break (new_tab-10) 0; Format.open_box 0; Format.force_newline (); Format.print_string (dummy^"AtNode: pos = "^posname^" conneciton = ("^c1^","^c2^")"); Format.print_flush(); (* Format.force_newline (); Format.print_break 0 3; *) Format.open_box 0; Format.print_break new_tab 0; Format.print_flush() end | RNode(alpha_layer,bproof) -> let alpha_string = stringlist_to_string alpha_layer in begin Format.open_box 0; Format.force_newline (); Format.print_break new_tab 0; Format.print_break 0 0; Format.force_newline (); Format.print_flush(); Format.open_box 0; print_string (dummy^"RootNode: "^alpha_string); Format.print_flush(); Format.open_box 0; Format.print_break 0 0; Format.print_flush(); pp_bproof_list [bproof] (new_tab-3) end | BNode(posname,(alph1,bproof1),(alph2,bproof2)) -> let alpha_string1 = stringlist_to_string alph1 and alpha_string2 = stringlist_to_string alph2 in begin Format.open_box 0; Format.force_newline (); Format.print_break new_tab 0; Format.print_break 0 0; Format.force_newline (); Format.print_flush(); Format.open_box 0; print_string (dummy^"BetaNode: pos = "^posname^" layer1 = "^alpha_string1^" layer2 = "^alpha_string2); Format.print_flush(); Format.open_box 0; Format.print_break 0 0; Format.print_flush(); pp_bproof_list [bproof1;bproof2] (new_tab-3) end in let new_tab = tab+5 in match tree_list with [] -> Format.print_string "" | first::rest -> begin pp_bproof first new_tab; pp_bproof_list rest tab end let rec print_pairlist pairlist = match pairlist with [] -> Format.print_string "" | (a,b)::rest -> begin Format.print_break 1 1; Format.print_string ("("^a^","^b^")"); print_pairlist rest end let print_beta_proof bproof = begin Format.open_box 0; Format.force_newline (); Format.force_newline (); Format.print_break 3 0; pp_bproof_list [bproof] 0; Format.force_newline (); Format.force_newline (); Format.force_newline (); Format.print_flush () end let rec print_treelist treelist = match treelist with [] -> print_endline "END"; | f::r -> begin print_ftree f; Format.open_box 0; print_endline ""; print_endline ""; print_endline "NEXT TREE"; print_endline ""; print_endline ""; print_treelist r; Format.print_flush () end let rec print_set_list set_list = match set_list with [] -> "" | f::r -> (f.aname)^" "^(print_set_list r) let print_set set = let set_list = AtomSet.elements set in if set_list = [] then "empty" else print_set_list set_list let print_string_set set = let set_list = StringSet.elements set in print_stringlist set_list let rec print_list_sets list_of_sets = match list_of_sets with [] -> Format.print_string "" | (pos,fset)::r -> begin Format.print_string (pos^": "); (* first element = node which successors depend on *) print_stringlist (StringSet.elements fset); Format.force_newline (); print_list_sets r end let print_ordering list_of_sets = begin Format.open_box 0; print_list_sets list_of_sets; Format.print_flush () end let rec print_triplelist triplelist = match triplelist with [] -> Format.print_string "" | ((a,b),i)::rest -> begin Format.print_break 1 1; Format.print_string ("(("^a^","^b^"),"^(string_of_int i)^")"); print_triplelist rest end let print_pos_n pos_n = Format.print_int pos_n let print_formula_info ftree ordering pos_n = begin print_ftree ftree; Format.open_box 0; Format.force_newline (); print_ordering ordering; Format.force_newline (); Format.force_newline (); Format.print_string "number of positions: "; print_pos_n pos_n; Format.force_newline (); print_endline ""; print_endline ""; Format.print_flush () end (* print sequent proof tree *) let pp_rule (pos,r,formula,term) tab = let rep = ruletable r in if List.mem rep ["Alll";"Allr";"Exl";"Exr"] then begin Format.open_box 0; (* Format.force_newline (); *) Format.print_break tab 0; Format.print_string (pos^": "^rep^" "); Format.print_flush (); (* Format.print_break tab 0; Format.force_newline (); Format.print_break tab 0; *) Format.open_box 0; print_term stdout formula; Format.print_flush (); Format.open_box 0; Format.print_string " "; Format.print_flush (); Format.open_box 0; print_term stdout term; Format.force_newline (); Format.force_newline (); Format.print_flush () end else begin Format.open_box 0; Format.print_break tab 0; Format.print_string (pos^": "^rep^" "); Format.print_flush (); Format.open_box 0; (* Format.print_break tab 0; *) Format.force_newline (); (* Format.print_break tab 0; *) print_term stdout formula; Format.force_newline () end let last addr = if addr = "" then "" else String.make 1 (String.get addr (String.length addr-1)) let rest addr = if addr = "" then "" else String.sub addr 0 ((String.length addr) - 1) let rec get_r_chain addr = if addr = "" then 0 else let l = last addr in if l = "l" then 0 else (* l = "r" *) let rs = rest addr in 1 + (get_r_chain rs) let rec tpp seqtree tab addr = match seqtree with | PEmpty -> raise jprover_bug | PNodeAx(rule) -> let (pos,r,p,pa) = rule in begin pp_rule (pos,r,p,pa) tab; (* Format.force_newline (); *) (* let mult = get_r_chain addr in *) (* Format.print_break 100 (tab - (3 * mult)) *) end | PNodeA(rule,left) -> let (pos,r,p,pa) = rule in begin pp_rule (pos,r,p,pa) tab; tpp left tab addr end | PNodeB(rule,left,right) -> let (pos,r,p,pa) = rule in let newtab = tab + 3 in begin pp_rule (pos,r,p,pa) tab; (* Format.force_newline (); *) (* Format.print_break 100 newtab; *) (tpp left newtab (addr^"l")); (tpp right newtab (addr^"r")) end let tt seqtree = begin Format.open_box 0; tpp seqtree 0 ""; Format.force_newline (); Format.close_box (); Format.print_newline () end (************ END printing functions *********************************) (************ Beta proofs and redundancy deletion **********************) let rec remove_dups_connections connection_list = match connection_list with [] -> [] | (c1,c2)::r -> if (List.mem (c1,c2) r) or (List.mem (c2,c1) r) then (* only one direction variant of a connection stays *) remove_dups_connections r else (c1,c2)::(remove_dups_connections r) let rec remove_dups_list list = match list with [] -> [] | f::r -> if List.mem f r then remove_dups_list r else f::(remove_dups_list r) let beta_pure alpha_layer connections beta_expansions = let (l1,l2) = List.split connections in let test_list = l1 @ l2 @ beta_expansions in begin (* Format.open_box 0; print_endline ""; print_stringlist alpha_layer; Format.print_flush(); Format.open_box 0; print_endline ""; print_stringlist test_list; print_endline ""; Format.print_flush(); *) not (List.exists (fun x -> (List.mem x test_list)) alpha_layer) end let rec apply_bproof_purity bproof = match bproof with BEmpty -> raise jprover_bug | CNode((c1,c2)) -> bproof,[(c1,c2)],[] | AtNode(_,(c1,c2)) -> bproof,[(c1,c2)],[] | RNode(alpha_layer,subproof) -> let (opt_subproof,min_connections,beta_expansions) = apply_bproof_purity subproof in (RNode(alpha_layer,opt_subproof),min_connections,beta_expansions) | BNode(pos,(alph1,subp1),(alph2,subp2)) -> let (opt_subp1,min_conn1,beta_exp1) = apply_bproof_purity subp1 in if beta_pure alph1 min_conn1 beta_exp1 then begin (* print_endline ("Left layer of "^pos); *) (opt_subp1,min_conn1,beta_exp1) end else let (opt_subp2,min_conn2,beta_exp2) = apply_bproof_purity subp2 in if beta_pure alph2 min_conn2 beta_exp2 then begin (* print_endline ("Right layer of "^pos); *) (opt_subp2,min_conn2,beta_exp2) end else let min_conn = remove_dups_connections (min_conn1 @ min_conn2) and beta_exp = remove_dups_list ([pos] @ beta_exp1 @ beta_exp2) in (BNode(pos,(alph1,opt_subp1),(alph2,opt_subp2)),min_conn,beta_exp) let bproof_purity bproof = let (opt_bproof,min_connections,_) = apply_bproof_purity bproof in opt_bproof,min_connections (*********** split permutation *****************) let rec apply_permutation bproof rep_name direction act_blayer = match bproof with BEmpty | RNode(_,_) -> raise jprover_bug | AtNode(cx,(c1,c2)) -> bproof,act_blayer | CNode((c1,c2)) -> bproof,act_blayer | BNode(pos,(alph1,subp1),(alph2,subp2)) -> if rep_name = pos then let (new_blayer,replace_branch) = if direction = "left" then (alph1,subp1) else (* direciton = "right" *) (alph2,subp2) in (match replace_branch with CNode((c1,c2)) -> (AtNode(c1,(c1,c2))),new_blayer (* perform atom expansion at c1 *) | _ -> replace_branch,new_blayer ) else let pproof1,new_blayer1 = apply_permutation subp1 rep_name direction act_blayer in let pproof2,new_blayer2 = apply_permutation subp2 rep_name direction new_blayer1 in (BNode(pos,(alph1,pproof1),(alph2,pproof2))),new_blayer2 let split_permutation pname opt_bproof = match opt_bproof with RNode(alayer,BNode(pos,(alph1,opt_subp1),(alph2,opt_subp2))) -> if pos = pname then (* if topmost beta expansion agrees with pname, then *) (* only split the beta proof and give back the two subproofs *) let (osubp1,min_con1) = bproof_purity opt_subp1 and (osubp2,min_con2) = bproof_purity opt_subp2 in (* there will be no purity reductions in the beta subproofs. We use this *) (* predicate to collect the set of used leaf-connections in each subproof*) ((RNode((alayer @ alph1),osubp1),min_con1), (RNode((alayer @ alph2),osubp2),min_con2) ) (* we combine the branch after topmost beta expansion at pos into one root alpha layer *) (* -- the beta expansion node pos will not be needed in this root layer *) else let perm_bproof1,balph1 = apply_permutation (BNode(pos,(alph1,opt_subp1),(alph2,opt_subp2))) pname "left" [] and perm_bproof2,balph2 = apply_permutation (BNode(pos,(alph1,opt_subp1),(alph2,opt_subp2))) pname "right" [] in begin (* print_endline " "; print_beta_proof perm_bproof1; print_endline" " ; print_beta_proof perm_bproof2; print_endline" "; *) let (osubp1,min_con1) = bproof_purity perm_bproof1 and (osubp2,min_con2) = bproof_purity perm_bproof2 in ((RNode((alayer @ balph1),osubp1),min_con1), (RNode((alayer @ balph2),osubp2),min_con2) ) end (* we combine the branch after the NEW topmost beta expansion at bpos *) (* into one root alpha layer -- the beta expansion node bpos will not be *) (* needed in this root layer *) | _ -> raise jprover_bug (*********** END split permutation *****************) let rec list_del list_el el_list = match el_list with [] -> raise jprover_bug | f::r -> if list_el = f then r else f::(list_del list_el r) let rec list_diff del_list check_list = match del_list with [] -> [] | f::r -> if List.mem f check_list then list_diff r check_list else f::(list_diff r check_list) (* let rec compute_alpha_layer ftree_list = match ftree_list with [] -> [],[],[] | f::r -> (match f with Empty -> raise jprover_bug | NodeAt(pos) -> let pn = pos.name and (rnode,ratom,borderings) = compute_alpha_layer r in ((pn::rnode),(pn::ratom),borderings) | NodeA(pos,suctrees) -> let pn = pos.name in if pos.pt = Beta then let (rnode,ratom,borderings) = compute_alpha_layer r in ((pn::rnode),(ratom),(f::borderings)) else let suclist = Array.to_list suctrees in compute_alpha_layer (suclist @ r) ) let rec compute_connection alpha_layer union_atoms connections = match connections with [] -> ("none","none") | (c,d)::r -> if (List.mem c union_atoms) & (List.mem d union_atoms) then let (c1,c2) = if List.mem c alpha_layer then (c,d) else if List.mem d alpha_layer then (d,c) (* then, d is supposed to occur in [alpha_layer] *) else raise (Invalid_argument "Jprover bug: connection match failure") in (c1,c2) else compute_connection alpha_layer union_atoms r let get_beta_suctrees btree = match btree with Empty | NodeAt(_) -> raise jprover_bug | NodeA(pos,suctrees) -> let b1tree = suctrees.(0) and b2tree = suctrees.(1) in (pos.name,b1tree,b2tree) let rec build_beta_proof alpha_layer union_atoms beta_orderings connections = let (c1,c2) = compute_connection alpha_layer union_atoms connections in (* [c1] is supposed to occur in the lowmost alpha layer of the branch, *) (* i.e. [aplha_layer] *) if (c1,c2) = ("none","none") then (match beta_orderings with [] -> raise jprover_bug | btree::r -> let (beta_pos,suctree1,suctree2) = get_beta_suctrees btree in let (alpha_layer1, atoms1, bordering1) = compute_alpha_layer [suctree1] and (alpha_layer2, atoms2, bordering2) = compute_alpha_layer [suctree2] in let bproof1,beta1,closure1 = build_beta_proof alpha_layer1 (atoms1 @ union_atoms) (bordering1 @ r) connections in let bproof2,beta2,closure2 = build_beta_proof alpha_layer2 (atoms2 @ union_atoms) (bordering2 @ r) connections in (BNode(beta_pos,(alpha_layer1,bproof1),(alpha_layer2,bproof2))),(1+beta1+beta2),(closure1+closure2) ) else CNode((c1,c2)),0,1 let construct_beta_proof ftree connections = let (root_node,root_atoms,beta_orderings) = compute_alpha_layer [ftree] in let beta_proof,beta_exp,closures = build_beta_proof root_node root_atoms beta_orderings connections in (RNode(root_node,beta_proof)),beta_exp,closures *) (* *********** New Version with direct computation from extension proof **** *) (* follows a DIRECT step from proof histories via pr-connection orderings to opt. beta-proofs *) let rec compute_alpha_layer ftree_list = match ftree_list with [] -> [] | f::r -> (match f with Empty -> raise jprover_bug | NodeAt(pos) -> let rnode = compute_alpha_layer r in (pos.name::rnode) | NodeA(pos,suctrees) -> if pos.pt = Beta then let rnode = compute_alpha_layer r in (pos.name::rnode) else let suclist = Array.to_list suctrees in compute_alpha_layer (suclist @ r) ) let rec compute_beta_difference c1_context c2_context act_context = match c1_context,c2_context with ([],c2_context) -> (list_diff c2_context act_context) (* both connection partners in the same submatrix; [c1] already isolated *) | ((fc1::rc1),[]) -> [] (* [c2] is a reduction step, i.e. isolated before [c1] *) | ((fc1::rc1),(fc2::rc2)) -> if fc1 = fc2 then (* common initial beta-expansions *) compute_beta_difference rc1 rc2 act_context else (list_diff c2_context act_context) let rec non_closed beta_proof_list = match beta_proof_list with [] -> false | bpf::rbpf -> (match bpf with RNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") | AtNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") | BEmpty -> true | CNode(_) -> non_closed rbpf | BNode(pos,(_,bp1),(_,bp2)) -> non_closed ([bp1;bp2] @ rbpf) ) let rec cut_context pos context = match context with [] -> raise (Invalid_argument "Jprover bug: invalid context element") | (f,num)::r -> if pos = f then context else cut_context pos r let compute_tree_difference beta_proof c1_context = match beta_proof with RNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") | CNode(_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") | AtNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") | BEmpty -> c1_context | BNode(pos,_,_) -> (* print_endline ("actual root: "^pos); *) cut_context pos c1_context let print_context conn bcontext = begin Format.open_box 0; Format.print_string conn; Format.print_string ": "; List.iter (fun x -> let (pos,num) = x in Format.print_string (pos^" "^(string_of_int num)^"")) bcontext; print_endline " "; Format.print_flush () end let rec build_opt_beta_proof beta_proof ext_proof beta_atoms beta_layer_list act_context = let rec add_c2_tree (c1,c2) c2_diff_context = match c2_diff_context with [] -> (CNode(c1,c2),0) | (f,num)::c2_diff_r -> let next_beta_proof,next_exp = add_c2_tree (c1,c2) c2_diff_r in let (layer1,layer2) = List.assoc f beta_layer_list in let new_bproof = if num = 1 then BNode(f,(layer1,next_beta_proof),(layer2,BEmpty)) else (* num = 2*) BNode(f,(layer1,BEmpty),(layer2,next_beta_proof)) in (new_bproof,(next_exp+1)) in let rec add_beta_expansions (c1,c2) rest_ext_proof c1_diff_context c2_diff_context new_act_context = match c1_diff_context with [] -> let (n_c1,n_c2) = if c2_diff_context = [] then (* make sure that leaf-connection is first element *) (c1,c2) else (c2,c1) in let c2_bproof,c2_exp = add_c2_tree (n_c1,n_c2) c2_diff_context in if c2_exp <> 0 then (* at least one open branch was generated to isloate [c2] *) begin (* print_endline "start with new beta-proof"; *) let new_bproof,new_exp,new_closures,new_rest_proof = build_opt_beta_proof c2_bproof rest_ext_proof beta_atoms beta_layer_list (act_context @ new_act_context) in (new_bproof,(new_exp+c2_exp),(new_closures+1),new_rest_proof) end else begin (* print_endline "proceed with old beta-proof"; *) (c2_bproof,c2_exp,1,rest_ext_proof) end | (f,num)::c1_diff_r -> let (layer1,layer2) = List.assoc f beta_layer_list in let next_beta_proof,next_exp,next_closures,next_ext_proof = add_beta_expansions (c1,c2) rest_ext_proof c1_diff_r c2_diff_context new_act_context in let new_bproof = if num = 1 then BNode(f,(layer1,next_beta_proof),(layer2,BEmpty)) else (* num = 2*) BNode(f,(layer1,BEmpty),(layer2,next_beta_proof)) in (new_bproof,(next_exp+1),next_closures,next_ext_proof) in let rec insert_connection beta_proof (c1,c2) rest_ext_proof c1_diff_context c2_diff_context act_context = begin (* print_context c1 c1_diff_context; print_endline ""; print_context c2 c2_diff_context; print_endline ""; *) match beta_proof with RNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") | CNode(_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") | AtNode(_,_) -> raise (Invalid_argument "Jprover bug: invalid beta-proof") | BEmpty -> add_beta_expansions (c1,c2) rest_ext_proof c1_diff_context c2_diff_context act_context | BNode(pos,(layer1,sproof1),(layer2,sproof2)) -> (* print_endline (c1^" "^c2^" "^pos); *) (match c1_diff_context with [] -> raise (Invalid_argument "Jprover bug: invalid beta-proof") | (f,num)::rest_context -> (* f = pos must hold!! *) if num = 1 then let (next_bproof,next_exp,next_closure,next_ext_proof) = insert_connection sproof1 (c1,c2) rest_ext_proof rest_context c2_diff_context act_context in (BNode(pos,(layer1,next_bproof),(layer2,sproof2)),next_exp,next_closure,next_ext_proof) else (* num = 2 *) let (next_bproof,next_exp,next_closure,next_ext_proof) = insert_connection sproof2 (c1,c2) rest_ext_proof rest_context c2_diff_context act_context in (BNode(pos,(layer1,sproof1),(layer2,next_bproof)),next_exp,next_closure,next_ext_proof) ) end in match ext_proof with [] -> beta_proof,0,0,[] | (c1,c2)::rproof -> (* print_endline ("actual connection: "^c1^" "^c2); *) let c1_context = List.assoc c1 beta_atoms and c2_context = List.assoc c2 beta_atoms in let c2_diff_context = compute_beta_difference c1_context c2_context act_context and c1_diff_context = compute_tree_difference beta_proof c1_context in (* wrt. actual beta-proof *) let (next_beta_proof,next_exp,next_closures,next_ext_proof) = insert_connection beta_proof (c1,c2) rproof c1_diff_context c2_diff_context c1_diff_context in if non_closed [next_beta_proof] then (* at least one branch was generated to isolate [c1] *) let rest_beta_proof,rest_exp,rest_closures,rest_ext_proof = build_opt_beta_proof next_beta_proof next_ext_proof beta_atoms beta_layer_list act_context in rest_beta_proof,(next_exp+rest_exp),(next_closures+rest_closures),rest_ext_proof else next_beta_proof,next_exp,next_closures,next_ext_proof let rec annotate_atoms beta_context atlist treelist = let rec annotate_tree beta_context tree atlist = match tree with Empty -> (atlist,[],[]) | NodeAt(pos) -> if List.mem pos.name atlist then let new_atlist = list_del pos.name atlist in (new_atlist,[(pos.name,beta_context)],[]) else (atlist,[],[]) | NodeA(pos,suctrees) -> if pos.pt = Beta then let s1,s2 = suctrees.(0),suctrees.(1) in let alayer1 = compute_alpha_layer [s1] and alayer2 = compute_alpha_layer [s2] and new_beta_context1 = beta_context @ [(pos.name,1)] and new_beta_context2 = beta_context @ [(pos.name,2)] in let atlist1,annotates1,blayer_list1 = annotate_atoms new_beta_context1 atlist [s1] in let atlist2,annotates2,blayer_list2 = annotate_atoms new_beta_context2 atlist1 [s2] in (atlist2,(annotates1 @ annotates2),((pos.name,(alayer1,alayer2))::(blayer_list1 @ blayer_list2))) else annotate_atoms beta_context atlist (Array.to_list suctrees) in match treelist with [] -> (atlist,[],[]) | f::r -> let (next_atlist,f_annotates,f_beta_layers) = annotate_tree beta_context f atlist in let (rest_atlist,rest_annotates,rest_beta_layers) = (annotate_atoms beta_context next_atlist r) in (rest_atlist, (f_annotates @ rest_annotates),(f_beta_layers @ rest_beta_layers)) let construct_opt_beta_proof ftree ext_proof = let con1,con2 = List.split ext_proof in let con_atoms = remove_dups_list (con1 @ con2) in let (empty_atoms,beta_atoms,beta_layer_list) = annotate_atoms [] con_atoms [ftree] in let root_node = compute_alpha_layer [ftree] in let (beta_proof,beta_exp,closures,_) = build_opt_beta_proof BEmpty ext_proof beta_atoms beta_layer_list [] in (RNode(root_node,beta_proof)),beta_exp,closures (************* permutation ljmc -> lj *********************************) (* REAL PERMUTATION STAFF *) let subf1 n m subrel = List.mem ((n,m),1) subrel let subf2 n m subrel = List.mem ((n,m),2) subrel let tsubf n m tsubrel = List.mem (n,m) tsubrel (* Transforms all normal form layers in an LJ proof *) let rec modify prooftree (subrel,tsubrel) = match prooftree with PEmpty -> raise jprover_bug | PNodeAx((pos,inf,form,term)) -> prooftree,pos | PNodeA((pos,inf,form,term),left) -> let t,qpos = modify left (subrel,tsubrel) in if List.mem inf [Impr;Negr;Allr] then PNodeA((pos,inf,form,term),t),pos (* layer bound *) else if qpos = "Orl-True" then PNodeA((pos,inf,form,term),t),qpos else if List.mem inf [Andl;Alll;Exl] then PNodeA((pos,inf,form,term),t),qpos (* simply propagation *) else if inf = Exr then if (subf1 pos qpos subrel) then PNodeA((pos,inf,form,term),t),pos else t,qpos else if inf = Negl then if (subf1 pos qpos subrel) then PNodeA((pos,inf,form,term),t),"" (* empty string *) else t,qpos else (* x = Orr *) if (subf1 pos qpos subrel) then PNodeA((pos,Orr1,form,term),t),pos (* make Orr for LJ *) else if (subf2 pos qpos subrel) then PNodeA((pos,Orr2,form,term),t),pos (* make Orr for LJ *) else t,qpos | PNodeB((pos,inf,form,term),left,right) -> let t,qpos = modify left (subrel,tsubrel) in if inf = Andr then if (or) (qpos = "Orl-True") (subf1 pos qpos subrel) then let s,rpos = modify right (subrel,tsubrel) in (* Orl-True -> subf *) if (or) (rpos = "Orl-True") (subf2 pos rpos subrel) then PNodeB((pos,inf,form,term),t,s),pos else s,rpos else t,qpos (* not subf -> not Orl-True *) else if inf = Impl then if (subf1 pos qpos subrel) then let s,rpos = modify right (subrel,tsubrel) in PNodeB((pos,inf,form,term),t,s),"" (* empty string *) else t,qpos else (* x = Orl *) let s,rpos = modify right (subrel,tsubrel) in PNodeB((pos,inf,form,term),t,s),"Orl-True" (* transforms the subproof into an LJ proof between the beta-inference rule (excluded) and layer boundary in the branch ptree *) let rec rec_modify ptree (subrel,tsubrel) = match ptree with PEmpty -> raise jprover_bug | PNodeAx((pos,inf,form,term)) -> ptree,pos | PNodeA((pos,inf,form,term),left) -> if List.mem inf [Impr;Negr;Allr] then ptree,pos (* layer bound, stop transforming! *) else let t,qpos = rec_modify left (subrel,tsubrel) in if List.mem inf [Andl;Alll;Exl] then PNodeA((pos,inf,form,term),t),qpos (* simply propagation*) else if inf = Exr then if (subf1 pos qpos subrel) then PNodeA((pos,inf,form,term),t),pos else t,qpos else if inf = Negl then if (subf1 pos qpos subrel) then PNodeA((pos,inf,form,term),t),"" (* empty string *) else t,qpos else (* x = Orr *) if (subf1 pos qpos subrel) then PNodeA((pos,Orr1,form,term),t),pos (* make Orr for LJ *) else if (subf2 pos qpos subrel) then PNodeA((pos,Orr2,form,term),t),pos (* make Orr for LJ *) else t,qpos | PNodeB((pos,inf,form,term),left,right) -> let t,qpos = rec_modify left (subrel,tsubrel) in if inf = Andr then if (subf1 pos qpos subrel) then let s,rpos = rec_modify right (subrel,tsubrel) in if (subf2 pos rpos subrel) then PNodeB((pos,inf,form,term),t,s),pos else s,rpos else t,qpos else (* x = Impl since x= Orl cannot occur in the partial layer ptree *) if (subf1 pos qpos subrel) then let s,rpos = rec_modify right (subrel,tsubrel) in PNodeB((pos,inf,form,term),t,s),"" (* empty string *) else t,qpos let weak_modify rule ptree (subrel,tsubrel) = (* recall rule = or_l *) let (pos,inf,formlua,term) = rule in if inf = Orl then ptree,true else let ptreem,qpos = rec_modify ptree (subrel,tsubrel) in if (subf1 pos qpos subrel) then (* weak_modify will always be applied on left branches *) ptreem,true else ptreem,false (* Now, the permutation stuff .... *) (* Permutation schemes *) (* corresponds to local permutation lemma -- Lemma 3 in the paper -- *) (* with eigenvariablen renaming and branch modification *) (* eigenvariablen renaming and branch modification over *) (* the whole proofs, i.e. over layer boundaries, too *) (* global variable vor eigenvariable renaming during permutations *) let eigen_counter = ref 1 (* append renamed paramater "r" to non-quantifier subformulae of renamed quantifier formulae *) (*: BUG :*) (*: let make_new_eigenvariable term = let op = (dest_term term).term_op in let opn = (dest_op op).op_name in let opnam = dest_opname opn in match opnam with [] -> raise jprover_bug | ofirst::orest -> let ofname = List.hd orest in let new_eigen_var = (ofname^"_r"^(string_of_int (!eigen_counter))) in eigen_counter := !eigen_counter + 1; (* print_endline ("New Counter :"^(string_of_int (!eigen_counter))); *) mk_string_term jprover_op new_eigen_var :*) let make_new_eigenvariable term = let op = (dest_term term).term_op in let opa = (dest_op op).op_params in let oppar = dest_param opa in match oppar with | String ofname::_ -> let new_eigen_var = (ofname^"_r"^(string_of_int (!eigen_counter))) in eigen_counter := !eigen_counter + 1; mk_string_term jprover_op new_eigen_var | _ -> raise jprover_bug let replace_subterm term oldt rept = let v_term = var_subst term oldt "dummy_var" in subst1 v_term "dummy_var" rept let rec eigen_rename old_parameter new_parameter ptree = match ptree with PEmpty -> raise jprover_bug | PNodeAx((pos,inf,form,term)) -> let new_form = replace_subterm form old_parameter new_parameter in PNodeAx((pos,inf,new_form,term)) | PNodeA((pos,inf,form,term), left) -> let new_form = replace_subterm form old_parameter new_parameter and new_term = replace_subterm term old_parameter new_parameter in let ren_left = eigen_rename old_parameter new_parameter left in PNodeA((pos,inf,new_form,new_term), ren_left) | PNodeB((pos,inf,form,term),left, right) -> let new_form = replace_subterm form old_parameter new_parameter in let ren_left = eigen_rename old_parameter new_parameter left in let ren_right = eigen_rename old_parameter new_parameter right in PNodeB((pos,inf,new_form,term), ren_left, ren_right) let rec update_ptree rule subtree direction tsubrel = match subtree with PEmpty -> raise jprover_bug | PNodeAx(r) -> subtree | PNodeA((pos,inf,formula,term), left) -> if (pos,inf,formula,term) = rule then left (* don't delete rule if subformula belongs to renamed instance of quantifiers; *) (* but this can never occur now since (renamed) formula is part of rule *) else let (posn,infn,formn,termn) = rule in if (&) (List.mem infn [Exl;Allr] ) (term = termn) then (* this can only occur if eigenvariable rule with same term as termn has been permuted; *) (* the application of the same eigenvariable introduction on the same subformula with *) (* different instantiated variables might occur! *) (* termn cannot occur in terms of permuted quantifier rules due to substitution split *) (* during reconstruciton of the ljmc proof *) let new_term = make_new_eigenvariable term in (* print_endline "Eigenvariable renaming!!!"; *) eigen_rename termn new_term subtree else let left_del = update_ptree rule left direction tsubrel in PNodeA((pos,inf,formula,term), left_del) | PNodeB((pos,inf,formula,term), left, right) -> if (pos,inf,formula,term) = rule then if direction = "l" then left else right (* direction = "r" *) else let left_del = update_ptree rule left direction tsubrel in let right_del = update_ptree rule right direction tsubrel in PNodeB((pos,inf,formula,term),left_del,right_del) let permute r1 r2 ptree la tsubrel = (* print_endline "permute in"; *) match ptree,la with PNodeA(r1, PNodeA(r2,left)),la -> (* print_endline "1-o-1"; *) PNodeA(r2, PNodeA(r1,left)) (* one-over-one *) | PNodeA(r1, PNodeB(r2,left,right)),la -> (* print_endline "1-o-2"; *) PNodeB(r2, PNodeA(r1,left), PNodeA(r1,right)) (* one-over-two *) | PNodeB(r1, PNodeA(r2,left), right),"l" -> (* print_endline "2-o-1 left"; *) let right_u = update_ptree r2 right "l" tsubrel in PNodeA(r2, PNodeB(r1, left, right_u)) (* two-over-one left *) | PNodeB(r1, left, PNodeA(r2,right)),"r" -> (* print_endline "2-o-1 right"; *) let left_u = update_ptree r2 left "l" tsubrel in PNodeA(r2, PNodeB(r1, left_u, right)) (* two-over-one right *) | PNodeB(r1, PNodeB(r2,left2,right2), right),"l" -> (* print_endline "2-o-2 left"; *) let right_ul = update_ptree r2 right "l" tsubrel in let right_ur = update_ptree r2 right "r" tsubrel in PNodeB(r2,PNodeB(r1,left2,right_ul),PNodeB(r1,right2,right_ur)) (* two-over-two left *) | PNodeB(r1, left, PNodeB(r2,left2,right2)),"r" -> (* print_endline "2-o-2 right"; *) let left_ul = update_ptree r2 left "l" tsubrel in let left_ur = update_ptree r2 left "r" tsubrel in PNodeB(r2,PNodeB(r1,left_ul,left2),PNodeB(r1,left_ur, right2)) (* two-over-two right *) | _ -> raise jprover_bug (* permute layers, isolate addmissible branches *) (* computes if an Andr is d-generatives *) let layer_bound rule = let (pos,inf,formula,term) = rule in if List.mem inf [Impr;Negr;Allr] then true else false let rec orl_free ptree = match ptree with PEmpty -> raise jprover_bug | PNodeAx(rule) -> true | PNodeA(rule,left) -> if layer_bound rule then true else orl_free left | PNodeB(rule,left,right) -> let (pos,inf,formula,term) = rule in if inf = Orl then false else (&) (orl_free left) (orl_free right) let rec dgenerative rule dglist ptree tsubrel = let (pos,inf,formula,term) = rule in if List.mem inf [Exr;Orr;Negl] then true else if inf = Andr then if dglist = [] then false else let first,rest = (List.hd dglist),(List.tl dglist) in let (pos1,inf1,formula1,term1) = first in if tsubf pos1 pos tsubrel then true else dgenerative rule rest ptree tsubrel else if inf = Impl then not (orl_free ptree) else false (* to compute a topmost addmissible pair r,o with the address addr of r in the proof tree *) let rec top_addmissible_pair ptree dglist act_r act_o act_addr tsubrel dummyt = let rec search_pair ptree dglist act_r act_o act_addr tsubrel = match ptree with PEmpty -> raise jprover_bug | PNodeAx(_) -> raise jprover_bug | PNodeA(rule, left) -> (* print_endline "alpha"; *) if (dgenerative rule dglist left tsubrel) then (* r = Exr,Orr,Negl *) let newdg = (@) [rule] dglist in search_pair left newdg act_r rule act_addr tsubrel else (* Impr, Allr, Notr only for test *) search_pair left dglist act_r act_o act_addr tsubrel | PNodeB(rule,left,right) -> (* print_endline "beta"; *) let (pos,inf,formula,term) = rule in if List.mem inf [Andr;Impl] then let bool = dgenerative rule dglist left tsubrel in let newdg,newrule = if bool then ((@) [rule] dglist),rule else dglist,act_o in if orl_free left then search_pair right newdg act_r newrule (act_addr^"r") tsubrel else (* not orl_free *) let left_r,left_o,left_addr = search_pair left newdg act_r newrule (act_addr^"l") tsubrel in if left_o = ("",Orr,dummyt,dummyt) then top_addmissible_pair right dglist act_r act_o (act_addr^"r") tsubrel dummyt else left_r,left_o,left_addr else (* r = Orl *) if orl_free left then top_addmissible_pair right dglist rule act_o (act_addr^"r") tsubrel dummyt else let left_r,left_o,left_addr = search_pair left dglist rule act_o (act_addr^"l") tsubrel in if left_o = ("",Orr,dummyt,dummyt) then top_addmissible_pair right dglist rule act_o (act_addr^"r") tsubrel dummyt else left_r,left_o,left_addr in (* print_endline "top_addmissible_pair in"; *) if orl_free ptree then (* there must be a orl BELOW an layer bound *) begin (* print_endline "orl_free"; *) act_r,act_o,act_addr end else begin (* print_endline "orl_full"; *) search_pair ptree dglist act_r act_o act_addr tsubrel end let next_direction addr act_addr = String.make 1 (String.get addr (String.length act_addr)) (* get starts with count 0*) let change_last addr d = let split = (String.length addr) - 1 in let prec,last = (String.sub addr 0 split),(String.sub addr split 1) in prec^d^last let last addr = if addr = "" then "" else String.make 1 (String.get addr (String.length addr-1)) let rest addr = if addr = "" then "" else String.sub addr 0 ((String.length addr) - 1) let rec permute_layer ptree dglist (subrel,tsubrel) = let rec permute_branch r addr act_addr ptree dglist (subrel,tsubrel) = (* print_endline "pbranch in"; *) let la = last act_addr in (* no ensure uniqueness at 2-over-x *) match ptree,la with PNodeA(o,PNodeA(rule,left)),la -> (* one-over-one *) (* print_endline " one-over-one "; *) let permute_result = permute o rule ptree la tsubrel in begin match permute_result with PNodeA(r2,left2) -> let pbleft = permute_branch r addr act_addr left2 dglist (subrel,tsubrel) in PNodeA(r2,pbleft) | _ -> raise jprover_bug end | PNodeA(o,PNodeB(rule,left,right)),la -> (* one-over-two *) (* print_endline " one-over-two "; *) if rule = r then (* left,right are or_l free *) permute o rule ptree la tsubrel (* first termination case *) else let d = next_direction addr act_addr in if d = "l" then let permute_result = permute o rule ptree la tsubrel in (match permute_result with PNodeB(r2,left2,right2) -> let pbleft = permute_branch r addr (act_addr^d) left2 dglist (subrel,tsubrel) in let plright = permute_layer right2 dglist (subrel,tsubrel) in PNodeB(r2,pbleft,plright) | _ -> raise jprover_bug ) else (* d = "r", that is left of rule is or_l free *) let left1,bool = weak_modify rule left (subrel,tsubrel) in if bool then (* rule is relevant *) let permute_result = permute o rule (PNodeA(o,PNodeB(rule,left1,right))) la tsubrel in (match permute_result with PNodeB(r2,left2,right2) -> let pbright = permute_branch r addr (act_addr^d) right2 dglist (subrel,tsubrel) in PNodeB(r2,left2,pbright) | _ -> raise jprover_bug ) else (* rule is not relevant *) PNodeA(o,left1) (* optimized termination case (1) *) | PNodeB(o,PNodeA(rule,left),right1),"l" -> (* two-over-one, left *) (* print_endline " two-over-one, left "; *) let permute_result = permute o rule ptree la tsubrel in (match permute_result with PNodeA(r2,left2) -> let pbleft = permute_branch r addr act_addr left2 dglist (subrel,tsubrel) in PNodeA(r2,pbleft) | _ -> raise jprover_bug ) | PNodeB(o,left1,PNodeA(rule,left)),"r" -> (* two-over-one, right *) (* left of o is or_l free *) (* print_endline " two-over-one, right"; *) let leftm,bool = weak_modify o left1 (subrel,tsubrel) in if bool then (* rule is relevant *) let permute_result = permute o rule (PNodeB(o,leftm,PNodeA(rule,left))) la tsubrel in (match permute_result with PNodeA(r2,left2) -> let pbleft = permute_branch r addr act_addr left2 dglist (subrel,tsubrel) in PNodeA(r2,pbleft) | _ -> raise jprover_bug ) else (* rule is not relevant *) leftm (* optimized termination case (2) *) | PNodeB(o,PNodeB(rule,left,right),right1),"l" -> (* two-over-two, left *) (* print_endline " two-over-two, left"; *) if rule = r then (* left,right are or_l free *) let permute_result = permute o rule ptree la tsubrel in (match permute_result with PNodeB(r2,PNodeB(r3,left3,right3),PNodeB(r4,left4,right4)) -> (* print_endline "permute 2-o-2, left ok"; *) let leftm3,bool3 = weak_modify r3 left3 (subrel,tsubrel) in let leftm4,bool4 = weak_modify r4 left4 (subrel,tsubrel) in let plleft,plright = if (&) bool3 bool4 then (* r3 and r4 are relevant *) (permute_layer (PNodeB(r3,leftm3,right3)) dglist (subrel,tsubrel)), (permute_layer (PNodeB(r4,leftm4,right4)) dglist (subrel,tsubrel)) else if (&) bool3 (not bool4) then (* only r3 is relevant *) begin (* print_endline "two-over-two left: bool3 and not bool4"; *) (permute_layer (PNodeB(r3,leftm3,right3)) dglist (subrel,tsubrel)), leftm4 end else if (&) (not bool3) bool4 then (* only r4 is relevant *) leftm3, (permute_layer (PNodeB(r4,leftm4,right4)) dglist (subrel,tsubrel)) else (* neither r3 nor r4 are relevant *) leftm3,leftm4 in PNodeB(r2,plleft,plright) | _ -> raise jprover_bug ) else let d = next_direction addr act_addr in let newadd = change_last act_addr d in if d = "l" then let permute_result = permute o rule ptree la tsubrel in (match permute_result with PNodeB(r2,left2,right2) -> let pbleft = permute_branch r addr newadd left2 dglist (subrel,tsubrel) in let plright = permute_layer right2 dglist (subrel,tsubrel) in PNodeB(r2,pbleft,plright) | _ -> raise jprover_bug ) else (* d = "r", that is left is or_l free *) let left1,bool = weak_modify rule left (subrel,tsubrel) in if bool then (* rule is relevant *) let permute_result = permute o rule (PNodeB(o,PNodeB(rule,left1,right),right1)) la tsubrel in (match permute_result with PNodeB(r2,PNodeB(r3,left3,right3),right2) -> let pbright = permute_branch r addr newadd right2 dglist (subrel,tsubrel) in let leftm3,bool3 = weak_modify r3 left3 (subrel,tsubrel) in let plleft = if bool3 (* r3 relevant *) then permute_layer (PNodeB(r3,leftm3,right3)) dglist (subrel,tsubrel) else (* r3 redundant *) leftm3 in PNodeB(r2,plleft,pbright) (* further opt. NOT possible *) | _ -> raise jprover_bug ) else (* rule is not relevant *) permute_layer (PNodeB(o,left1,right1)) dglist (subrel,tsubrel) (* further opt. possible *) (* combine with orl_free *) | PNodeB(o,left1,PNodeB(rule,left,right)),"r" -> (* two-over-two, right *) (* print_endline " two-over-two, right"; *) let leftm1,bool = weak_modify o left1 (subrel,tsubrel) in (* left1 is or_l free *) if bool then (* o is relevant, even after permutations *) if rule = r then (* left, right or_l free *) permute o rule (PNodeB(o,leftm1,PNodeB(rule,left,right))) la tsubrel else let d = next_direction addr act_addr in let newadd = change_last act_addr d in if d = "l" then let permute_result = permute o rule (PNodeB(o,leftm1,PNodeB(rule,left,right))) la tsubrel in (match permute_result with PNodeB(r2,left2,right2) -> let pbleft = permute_branch r addr newadd left2 dglist (subrel,tsubrel) in let plright = permute_layer right2 dglist (subrel,tsubrel) in PNodeB(r2,pbleft,plright) | _ -> raise jprover_bug ) else (* d = "r", that is left is or_l free *) let leftm,bool = weak_modify rule left (subrel,tsubrel) in if bool then (* rule is relevant *) let permute_result = permute o rule (PNodeB(o,leftm1,PNodeB(rule,left,right))) la tsubrel in (match permute_result with PNodeB(r2,left2,right2) -> let pbright = permute_branch r addr newadd right2 dglist (subrel,tsubrel) in PNodeB(r2,left2,pbright) (* left2 or_l free *) | _ -> raise jprover_bug ) else (* rule is not relevant *) PNodeB(o,leftm1,leftm) else leftm1 | _ -> raise jprover_bug in let rec trans_add_branch r o addr act_addr ptree dglist (subrel,tsubrel) = match ptree with (PEmpty| PNodeAx(_)) -> raise jprover_bug | PNodeA(rule,left) -> if (dgenerative rule dglist left tsubrel) then let newdg = (@) [rule] dglist in if rule = o then begin (* print_endline "one-rule is o"; *) permute_branch r addr act_addr ptree dglist (subrel,tsubrel) end else begin (* print_endline "alpha - but not o"; *) let tptree = trans_add_branch r o addr act_addr left newdg (subrel,tsubrel) in permute_layer (PNodeA(rule,tptree)) dglist (subrel,tsubrel) (* r may not longer be valid for rule *) end else let tptree = trans_add_branch r o addr act_addr left dglist (subrel,tsubrel) in PNodeA(rule,tptree) | PNodeB(rule,left,right) -> let d = next_direction addr act_addr in let bool = (dgenerative rule dglist left tsubrel) in if rule = o then begin (* print_endline "two-rule is o"; *) permute_branch r addr (act_addr^d) ptree dglist (subrel,tsubrel) end else begin (* print_endline ("beta - but not o: address "^d); *) let dbranch = if d = "l" then left else (* d = "r" *) right in let tptree = if bool then let newdg = (@) [rule] dglist in (trans_add_branch r o addr (act_addr^d) dbranch newdg (subrel,tsubrel)) else (trans_add_branch r o addr (act_addr^d) dbranch dglist (subrel,tsubrel)) in if d = "l" then permute_layer (PNodeB(rule,tptree,right)) dglist (subrel,tsubrel) else (* d = "r" *) begin (* print_endline "prob. a redundant call"; *) let back = permute_layer (PNodeB(rule,left,tptree)) dglist (subrel,tsubrel) in (* print_endline "SURELY a redundant call"; *) back end end in (* print_endline "permute_layer in"; *) let dummyt = mk_var_term "dummy" in let r,o,addr = top_addmissible_pair ptree dglist ("",Orl,dummyt,dummyt) ("",Orr,dummyt,dummyt) "" tsubrel dummyt in if r = ("",Orl,dummyt,dummyt) then ptree else if o = ("",Orr,dummyt,dummyt) then (* Orr is a dummy for no d-gen. rule *) ptree else let (x1,x2,x3,x4) = r and (y1,y2,y3,y4) = o in (* print_endline ("top or_l: "^x1); print_endline ("or_l address: "^addr); print_endline ("top dgen-rule: "^y1); *) trans_add_branch r o addr "" ptree dglist (subrel,tsubrel) (* Isolate layer and outer recursion structure *) (* uses weaker layer boundaries: ONLY critical inferences *) let rec trans_layer ptree (subrel,tsubrel) = let rec isol_layer ptree (subrel,tsubrel) = match ptree with PEmpty -> raise jprover_bug | PNodeAx(inf) -> ptree | PNodeA((pos,rule,formula,term),left) -> if List.mem rule [Allr;Impr;Negr] then let tptree = trans_layer left (subrel,tsubrel) in PNodeA((pos,rule,formula,term),tptree) else let tptree = isol_layer left (subrel,tsubrel) in PNodeA((pos,rule,formula,term),tptree) | PNodeB(rule,left,right) -> let tptree_l = isol_layer left (subrel,tsubrel) and tptree_r = isol_layer right (subrel,tsubrel) in PNodeB(rule,tptree_l,tptree_r) in begin (* print_endline "trans_layer in"; *) let top_tree = isol_layer ptree (subrel,tsubrel) in let back = permute_layer top_tree [] (subrel,tsubrel) in (* print_endline "translauer out"; *) back end (* REAL PERMUTATION STAFF --- End *) (* build the proof tree from a list of inference rules *) let rec unclosed subtree = match subtree with PEmpty -> true | PNodeAx(y) -> false | PNodeA(y,left) -> (unclosed left) | PNodeB(y,left,right) -> (or) (unclosed left) (unclosed right) let rec extend prooftree element = match prooftree with PEmpty -> let (pos,rule,formula,term) = element in if rule = Ax then PNodeAx(element) else if List.mem rule [Andr; Orl; Impl] then PNodeB(element,PEmpty,PEmpty) else PNodeA(element,PEmpty) | PNodeAx(y) -> PEmpty (* that's only for exhaustive pattern matching *) | PNodeA(y, left) -> PNodeA(y, (extend left element)) | PNodeB(y, left, right) -> if (unclosed left) then PNodeB(y, (extend left element), right) else PNodeB(y, left, (extend right element)) let rec bptree prooftree nodelist nax= match nodelist with [] -> prooftree,nax | ((_,pos),(rule,formula,term))::rest -> (* kick away the first argument *) let newax = if rule = Ax then 1 else 0 in bptree (extend prooftree (pos,rule,formula,term)) rest (nax+newax) let bproof nodelist = bptree PEmpty nodelist 0 let rec get_successor_pos treelist = match treelist with [] -> [] | f::r -> ( match f with Empty -> get_successor_pos r | NodeAt(_) -> raise jprover_bug | NodeA(pos,_) -> pos::(get_successor_pos r) ) let rec get_formula_tree ftreelist f predflag = match ftreelist with [] -> raise jprover_bug | ftree::rest_trees -> (match ftree with Empty -> get_formula_tree rest_trees f predflag | NodeAt(_) -> get_formula_tree rest_trees f predflag | NodeA(pos,suctrees) -> if predflag = "pred" then if pos.pt = Gamma then let succs = get_successor_pos (Array.to_list suctrees) in if List.mem f succs then NodeA(pos,suctrees),succs else get_formula_tree ((Array.to_list suctrees) @ rest_trees) f predflag else get_formula_tree ((Array.to_list suctrees) @ rest_trees) f predflag else (* predflag = "" *) if pos = f then NodeA(pos,suctrees),[] else get_formula_tree ((Array.to_list suctrees) @ rest_trees) f predflag ) let rec get_formula_treelist ftree po = match po with [] -> [] | f::r -> (* a posistion in po has either stype Gamma_0,Psi_0,Phi_0 (non-atomic), or it has *) (* ptype Alpha (or on the right), since there was a deadlock for proof reconstruction in LJ*) if List.mem f.st [Phi_0;Psi_0] then let (stree,_) = get_formula_tree [ftree] f "" in stree::(get_formula_treelist ftree r) else if f.st = Gamma_0 then let (predtree,succs) = get_formula_tree [ftree] f "pred" in let new_po = list_diff r succs in predtree::(get_formula_treelist ftree new_po) else if f.pt = Alpha then (* same as first case, or on the right *) let (stree,_) = get_formula_tree [ftree] f "" in stree::(get_formula_treelist ftree r) else raise (Invalid_argument "Jprover bug: non-admissible open position") let rec build_formula_rel dir_treelist slist predname = let rec build_renamed_gamma_rel dtreelist predname posname d = match dtreelist with [] -> [],[] | (x,ft)::rdtlist -> let rest_rel,rest_ren = build_renamed_gamma_rel rdtlist predname posname d in ( match ft with Empty -> (* may have empty successors due to purity in former reconstruction steps *) rest_rel,rest_ren | NodeAt(_) -> raise jprover_bug (* gamma_0 position never is atomic *) | NodeA(spos,suctrees) -> if List.mem spos.name slist then (* the gamma_0 position is really unsolved *) (* this is only relevant for the gamma_0 positions in po *) let new_name = (posname^"_"^spos.name) (* make new unique gamma name *) in let new_srel_el = ((predname,new_name),d) and new_rename_el = (spos.name,new_name) (* gamma_0 position as key first *) in let (srel,sren) = build_formula_rel [(x,ft)] slist new_name in ((new_srel_el::srel) @ rest_rel),((new_rename_el::sren) @ rest_ren) else rest_rel,rest_ren ) in match dir_treelist with [] -> [],[] | (d,f)::dir_r -> let (rest_rel,rest_renlist) = build_formula_rel dir_r slist predname in match f with Empty -> print_endline "Hello, an empty subtree!!!!!!"; rest_rel,rest_renlist | NodeAt(pos) -> (((predname,pos.name),d)::rest_rel),rest_renlist | NodeA(pos,suctrees) -> (match pos.pt with Alpha | Beta -> let dtreelist = if (pos.pt = Alpha) & (pos.op = Neg) then [(1,suctrees.(0))] else let st1 = suctrees.(0) and st2 = suctrees.(1) in [(1,st1);(2,st2)] in let (srel,sren) = build_formula_rel dtreelist slist pos.name in ((((predname,pos.name),d)::srel) @ rest_rel),(sren @ rest_renlist) | Delta -> let st1 = suctrees.(0) in let (srel,sren) = build_formula_rel [(1,st1)] slist pos.name in ((((predname,pos.name),d)::srel) @ rest_rel),(sren @ rest_renlist) | Psi| Phi -> let succlist = Array.to_list suctrees in let dtreelist = (List.map (fun x -> (d,x)) succlist) in let (srel,sren) = build_formula_rel dtreelist slist predname in (srel @ rest_rel),(sren @ rest_renlist) | Gamma -> let n = Array.length suctrees and succlist = (Array.to_list suctrees) in let dtreelist = (List.map (fun x -> (1,x)) succlist) in (* if (nonemptys suctrees 0 n) = 1 then let (srel,sren) = build_formula_rel dtreelist slist pos.name in ((((predname,pos.name),d)::srel) @ rest_rel),(sren @ rest_renlist) else (* we have more than one gamma instance, which means renaming *) *) let (srel,sren) = build_renamed_gamma_rel dtreelist predname pos.name d in (srel @ rest_rel),(sren @ rest_renlist) | PNull -> raise jprover_bug ) let rec rename_gamma ljmc_proof rename_list = match ljmc_proof with [] -> [] | ((inst,pos),(rule,formula,term))::r -> if List.mem rule [Alll;Exr] then let new_gamma = List.assoc inst rename_list in ((inst,new_gamma),(rule,formula,term))::(rename_gamma r rename_list) else ((inst,pos),(rule,formula,term))::(rename_gamma r rename_list) let rec compare_pair (s,sf) list = if list = [] then list else let (s_1,sf_1),restlist = (List.hd list),(List.tl list) in if sf = s_1 then (@) [(s,sf_1)] (compare_pair (s,sf) restlist) else compare_pair (s,sf) restlist let rec compare_pairlist list1 list2 = if list1 = [] then list1 else let (s1,sf1),restlist1 = (List.hd list1),(List.tl list1) in (@) (compare_pair (s1,sf1) list2) (compare_pairlist restlist1 list2) let rec trans_rec pairlist translist = let tlist = compare_pairlist pairlist translist in if tlist = [] then translist else (@) (trans_rec pairlist tlist) translist let transitive_closure subrel = let pairlist,nlist = List.split subrel in trans_rec pairlist pairlist let pt ptree subrel = let tsubrel = transitive_closure subrel in let transptree = trans_layer ptree (subrel,tsubrel) in print_endline ""; fst (modify transptree (subrel,tsubrel)) (* let mtree = fst (modify transptree (subrel,tsubrel)) in *) (* pretty_print mtree ax *) let rec make_node_list ljproof = match ljproof with PEmpty -> raise jprover_bug | PNodeAx((pos,inf,form,term)) -> [(("",pos),(inf,form,term))] | PNodeA((pos,inf,form,term),left) -> let left_list = make_node_list left in (("",pos),(inf,form,term))::left_list | PNodeB((pos,inf,form,term),left,right) -> let left_list = make_node_list left and right_list = make_node_list right in (("",pos),(inf,form,term))::(left_list @ right_list) let permute_ljmc ftree po slist ljmc_proof = (* ftree/po are the formula tree / open positions of the sequent that caused deadlock and permutation *) (* print_endline "!!!!!!!!!!!!!Permutation TO DO!!!!!!!!!"; *) (* the open positions in po are either phi_0, psi_0, or gamma_0 positions *) (* since proof reconstruction was a deadlock in LJ *) let po_treelist = get_formula_treelist ftree po in let dir_treelist = List.map (fun x -> (1,x)) po_treelist in let (formula_rel,rename_list) = build_formula_rel dir_treelist slist "dummy" in let renamed_ljmc_proof = rename_gamma ljmc_proof rename_list in let (ptree,ax) = bproof renamed_ljmc_proof in let ljproof = pt ptree formula_rel in (* this is a direct formula relation, comprising left/right subformula *) begin (* print_treelist po_treelist; *) (* print_endline ""; print_endline ""; *) (* print_triplelist formula_rel; *) (* print_endline ""; print_endline ""; tt ljproof; *) (* print_pairlist rename_list; *) (* print_endline ""; print_endline ""; *) make_node_list ljproof end (************** PROOF RECONSTRUCTION without redundancy deletion ******************************) let rec init_unsolved treelist = match treelist with [] -> [] | f::r -> begin match f with Empty -> [] | NodeAt(pos) -> (pos.name)::(init_unsolved r) | NodeA(pos,suctrees) -> let new_treelist = (Array.to_list suctrees) @ r in (pos.name)::(init_unsolved new_treelist) end (* only the unsolved positions will be represented --> skip additional root position *) let build_unsolved ftree = match ftree with Empty | NodeAt _ -> raise jprover_bug | NodeA(pos,suctrees) -> ((pos.name),init_unsolved (Array.to_list suctrees)) (* let rec collect_variables tree_list = match tree_list with [] -> [] | f::r -> begin match f with Empty -> [] | NodeAt(pos) -> if pos.st = Gamma_0 then pos.name::collect_variables r else collect_variables r | NodeA(pos,suctrees) -> let new_tree_list = (Array.to_list suctrees) @ r in if pos.st = Gamma_0 then pos.name::collect_variables new_tree_list else collect_variables new_tree_list end let rec extend_sigmaQ sigmaQ vlist = match vlist with [] -> [] | f::r -> let vf = mk_var_term f in if List.exists (fun x -> (fst x = vf)) sigmaQ then extend_sigmaQ sigmaQ r else (* first and second component are var terms in meta-prl *) [(vf,vf)] @ (extend_sigmaQ sigmaQ r) let build_sigmaQ sigmaQ ftree = let vlist = collect_variables [ftree] in sigmaQ @ (extend_sigmaQ sigmaQ vlist) *) (* subformula relation subrel is assumed to be represented in pairs (a,b) *) let rec delete e list = (* e must not necessarily occur in list *) match list with [] -> [] (* e must not necessarily occur in list *) | first::rest -> if e = first then rest else first::(delete e rest) let rec key_delete fname pos_list = (* in key_delete, f is a pos name (key) but sucs is a list of positions *) match pos_list with [] -> [] (* the position with name f must not necessarily occur in pos_list *) | f::r -> if fname = f.name then r else f::(key_delete fname r) let rec get_roots treelist = match treelist with [] -> [] | f::r -> match f with Empty -> (get_roots r) (* Empty is posible below alpha-nodes after purity *) | NodeAt(pos) -> pos::(get_roots r) | NodeA(pos,trees) -> pos::(get_roots r) let rec comp_ps padd ftree = match ftree with Empty -> raise (Invalid_argument "Jprover bug: empty formula tree") | NodeAt(pos) -> [] | NodeA(pos,strees) -> match padd with [] -> get_roots (Array.to_list strees) | f::r -> if r = [] then pos::(comp_ps r (Array.get strees (f-1))) else comp_ps r (Array.get strees (f-1)) (* computes a list: first element predecessor, next elements successoes of p *) let tpredsucc p ftree = let padd = p.address in comp_ps padd ftree (* set an element in an array, without side effects *) let myset array int element = let length = Array.length array in let firstpart = Array.sub array 0 (int) in let secondpart = Array.sub array (int+1) (length-(int+1)) in (Array.append firstpart (Array.append [|element|] secondpart)) let rec compute_open treelist slist = match treelist with [] -> [] | first::rest -> let elements = match first with Empty -> [] | NodeAt(pos) -> if (List.mem (pos.name) slist) then [pos] else [] | NodeA(pos,suctrees) -> if (List.mem (pos.name) slist) then [pos] else compute_open (Array.to_list suctrees) slist in elements @ (compute_open rest slist) let rec select_connection pname connections slist = match connections with [] -> ("none","none") | f::r -> let partner = if (fst f) = pname then (snd f) else if (snd f) = pname then (fst f) else "none" in if ((partner = "none") or (List.mem partner slist)) then select_connection pname r slist else f let rec replace_element element element_set redord = match redord with [] -> raise jprover_bug (* element occurs in redord *) | (f,fset)::r -> if f = element then (f,element_set)::r else (f,fset)::(replace_element element element_set r) let rec collect_succ_sets sucs redord = match redord with [] -> StringSet.empty | (f,fset)::r -> let new_sucs = key_delete f sucs in if (List.length sucs) = (List.length new_sucs) then (* position with name f did not occur in sucs -- no deletion *) (collect_succ_sets sucs r) else StringSet.union (StringSet.add f fset) (collect_succ_sets new_sucs r) let replace_ordering psucc_name sucs redord = let new_psucc_set = collect_succ_sets sucs redord in (* print_string_set new_psucc_set; *) replace_element psucc_name new_psucc_set redord let rec update pname redord = match redord with [] -> [] | (f,fset)::r -> if pname=f then r else (f,fset)::(update pname r) (* rule construction *) let rec selectQ_rec spos_var csigmaQ = match csigmaQ with [] -> mk_var_term spos_var (* dynamic completion of csigmaQ *) | (var,term)::r -> if spos_var=var then term else selectQ_rec spos_var r let selectQ spos_name csigmaQ = let spos_var = spos_name^"_jprover" in selectQ_rec spos_var csigmaQ let apply_sigmaQ term sigmaQ = let sigma_vars,sigma_terms = List.split sigmaQ in (subst term sigma_vars sigma_terms) let build_rule pos spos csigmaQ orr_flag calculus = let inst_label = apply_sigmaQ (pos.label) csigmaQ in match pos.op,pos.pol with Null,_ -> raise (Invalid_argument "Jprover: no rule") | At,O -> Ax,(inst_label),xnil_term (* to give back a term *) | At,I -> Ax,(inst_label),xnil_term | And,O -> Andr,(inst_label),xnil_term | And,I -> Andl,(inst_label),xnil_term | Or,O -> if calculus = "LJ" then let or_rule = if orr_flag = 1 then Orr1 else Orr2 in or_rule,(inst_label),xnil_term else Orr,(inst_label),xnil_term | Or,I -> Orl,(inst_label),xnil_term | Neg,O -> Negr,(inst_label),xnil_term | Neg,I -> Negl,(inst_label),xnil_term | Imp,O -> Impr,(inst_label),xnil_term | Imp,I -> Impl,(inst_label),xnil_term | All,I -> Alll,(inst_label),(selectQ spos.name csigmaQ) (* elements of csigmaQ is (string * term) *) | Ex,O -> Exr,(inst_label), (selectQ spos.name csigmaQ) | All,O -> Allr,(inst_label),(mk_string_term jprover_op spos.name) (* must be a proper term *) | Ex,I -> Exl,(inst_label),(mk_string_term jprover_op spos.name) (* must be a proper term *) (* %%%%%%%%%%%%%%%%%%%% Split begin %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) let rec nonemptys treearray j n = if j = n then 0 else let count = if (Array.get treearray j) <> Empty then 1 else 0 in count + (nonemptys treearray (j+1) n) let rec collect_pure ftreelist (flist,slist) = let rec collect_itpure ftree (flist,slist) = match ftree with Empty -> (* assumed that not all brother trees are Empty *) [] | NodeAt(pos) -> (* that may NOT longer be an inner node *) if ((List.mem (pos.name) flist) or (List.mem (pos.name) slist)) then [] else [pos] | NodeA(pos,treearray) -> collect_pure (Array.to_list treearray) (flist,slist) in match ftreelist with [] -> [] | f::r -> (collect_itpure f (flist,slist)) @ (collect_pure r (flist,slist)) let rec update_list testlist list = match testlist with [] -> list | f::r -> let newlist = delete f list in (* f may not occur in list; then newlist=list *) update_list r newlist let rec update_pairlist p pairlist = match pairlist with [] -> [] | f::r -> if ((fst f) = p) or ((snd f) = p) then update_pairlist p r else f::(update_pairlist p r) let rec update_connections slist connections = match slist with [] -> connections | f::r -> let connew = update_pairlist f connections in update_connections r connew let rec update_redord delset redord = (* delset is the set of positions to be deleted *) match redord with [] -> [] | (f,fset)::r -> if (StringSet.mem f delset) then update_redord delset r (* delete all key elements f from redord which are in delset *) else let new_fset = StringSet.diff fset delset in (* no successor of f from delset should remain in fset *) (f,new_fset)::(update_redord delset r) let rec get_position_names treelist = match treelist with [] -> [] | deltree::rests -> match deltree with Empty -> get_position_names rests | NodeAt(pos) -> (pos.name)::get_position_names rests | NodeA(pos,strees) -> (pos.name)::(get_position_names ((Array.to_list strees) @ rests)) let rec slist_to_set slist = match slist with [] -> StringSet.empty | f::r -> StringSet.add f (slist_to_set r) let rec print_purelist pr = match pr with [] -> begin print_string "."; print_endline " "; end | f::r -> print_string ((f.name)^", "); print_purelist r let update_relations deltree redord connections unsolved_list = let pure_names = get_position_names [deltree] in begin (* print_ftree deltree; Format.open_box 0; print_endline " "; print_stringlist pure_names; Format.force_newline (); Format.print_flush (); *) let rednew = update_redord (slist_to_set pure_names) redord and connew = update_connections pure_names connections and unsolnew = update_list pure_names unsolved_list in (rednew,connew,unsolnew) end let rec collect_qpos ftreelist uslist = match ftreelist with [] -> [],[] | ftree::rest -> match ftree with Empty -> collect_qpos rest uslist | NodeAt(pos) -> let (rest_delta,rest_gamma) = collect_qpos rest uslist in if (pos.st = Gamma_0) & (List.mem pos.name uslist) then rest_delta,(pos.name::rest_gamma) else if (pos.st = Delta_0) & (List.mem pos.name uslist) then (pos.name::rest_delta),rest_gamma else rest_delta,rest_gamma | NodeA(pos,suctrees) -> let (rest_delta,rest_gamma) = collect_qpos ((Array.to_list suctrees) @ rest) uslist in if (pos.st = Gamma_0) & (List.mem pos.name uslist) then rest_delta,(pos.name::rest_gamma) else if (pos.st = Delta_0) & (List.mem pos.name uslist) then (pos.name::rest_delta),rest_gamma else rest_delta,rest_gamma let rec do_split gamma_diff sigmaQ = match sigmaQ with [] -> [] | (v,term)::r -> if (List.mem (String.sub v 0 (String.index v '_')) gamma_diff) then do_split gamma_diff r else (v,term)::(do_split gamma_diff r) (* make a term list out of a bterm list *) let rec collect_subterms = function [] -> [] | bt::r -> let dbt = dest_bterm bt in (dbt.bterm)::(collect_subterms r) (*: Bug! :*) (*: let rec collect_delta_terms = function [] -> [] | t::r -> let dt = dest_term t in let top = dt.term_op and tterms = dt.term_terms in let dop = dest_op top in let don = dest_opname dop.op_name in match don with [] -> let sub_terms = collect_subterms tterms in collect_delta_terms (sub_terms @ r) | op1::opr -> if op1 = "jprover" then match opr with [] -> raise (Invalid_argument "Jprover: delta position missing") | delta::_ -> delta::(collect_delta_terms r) else let sub_terms = collect_subterms tterms in collect_delta_terms (sub_terms @ r) :*) let rec collect_delta_terms = function [] -> [] | t::r -> let dt = dest_term t in let top = dt.term_op and tterms = dt.term_terms in let dop = dest_op top in let don = dest_opname dop.op_name in let doa = dest_param dop.op_params in match don with [] -> let sub_terms = collect_subterms tterms in collect_delta_terms (sub_terms @ r) | op1::opr -> if op1 = "jprover" then match doa with [] -> raise (Invalid_argument "Jprover: delta position missing") | String delta::_ -> delta::(collect_delta_terms r) | _ -> raise (Invalid_argument "Jprover: delta position error") else let sub_terms = collect_subterms tterms in collect_delta_terms (sub_terms @ r) let rec check_delta_terms (v,term) ass_delta_diff dterms = match ass_delta_diff with [] -> term,[] | (var,dname)::r -> if List.mem dname dterms then let new_var = if var = "" then v else var in let replace_term = mk_string_term jprover_op dname in let next_term = var_subst term replace_term new_var in let (new_term,next_diffs) = check_delta_terms (v,next_term) r dterms in (new_term,((new_var,dname)::next_diffs)) else let (new_term,next_diffs) = check_delta_terms (v,term) r dterms in (new_term,((var,dname)::next_diffs)) let rec localize_sigma zw_sigma ass_delta_diff = match zw_sigma with [] -> [] | (v,term)::r -> let dterms = collect_delta_terms [term] in let (new_term,new_ass_delta_diff) = check_delta_terms (v,term) ass_delta_diff dterms in (v,new_term)::(localize_sigma r new_ass_delta_diff) let subst_split ft1 ft2 ftree uslist1 uslist2 uslist sigmaQ = let delta,gamma = collect_qpos [ftree] uslist and delta1,gamma1 = collect_qpos [ft1] uslist1 and delta2,gamma2 = collect_qpos [ft2] uslist2 in let delta_diff1 = list_diff delta delta1 and delta_diff2 = list_diff delta delta2 and gamma_diff1 = list_diff gamma gamma1 and gamma_diff2 = list_diff gamma gamma2 in let zw_sigma1 = do_split gamma_diff1 sigmaQ and zw_sigma2 = do_split gamma_diff2 sigmaQ in let ass_delta_diff1 = List.map (fun x -> ("",x)) delta_diff1 and ass_delta_diff2 = List.map (fun x -> ("",x)) delta_diff2 in let sigmaQ1 = localize_sigma zw_sigma1 ass_delta_diff1 and sigmaQ2 = localize_sigma zw_sigma2 ass_delta_diff2 in (sigmaQ1,sigmaQ2) let rec reduce_tree addr actual_node ftree beta_flag = match addr with [] -> (ftree,Empty,actual_node,beta_flag) | a::radd -> match ftree with Empty -> print_endline "Empty purity tree"; raise jprover_bug | NodeAt(_) -> print_endline "Atom purity tree"; raise jprover_bug | NodeA(pos,strees) -> (* print_endline pos.name; *) (* the associated node occurs above f (or the empty address) and hence, is neither atom nor empty tree *) let nexttree = (Array.get strees (a-1)) in if (nonemptys strees 0 (Array.length strees)) < 2 then begin (* print_endline "strees 1 or non-empties < 2"; *) let (ft,dt,an,bf) = reduce_tree radd actual_node nexttree beta_flag in let nstrees = myset strees (a-1) ft in (* print_endline ("way back "^pos.name); *) (NodeA(pos,nstrees),dt,an,bf) end else (* nonemptys >= 2 *) begin (* print_endline "nonempties >= 2 "; *) let (new_act,new_bf) = if pos.pt = Beta then (actual_node,true) else ((pos.name),false) in let (ft,dt,an,bf) = reduce_tree radd new_act nexttree new_bf in if an = pos.name then let nstrees = myset strees (a-1) Empty in (* print_endline ("way back assocnode "^pos.name); *) (NodeA(pos,nstrees),nexttree,an,bf) else (* has been replaced / will be replaced below / above pos *) let nstrees = myset strees (a-1) ft in (* print_endline ("way back "^pos.name); *) (NodeA(pos,nstrees),dt,an,bf) end let rec purity ftree redord connections unsolved_list = let rec purity_reduction pr ftree redord connections unsolved_list = begin (* Format.open_box 0; print_endline " "; print_purelist pr; Format.force_newline (); Format.print_flush (); *) match pr with [] -> (ftree,redord,connections,unsolved_list) | f::r -> (* print_endline ("pure position "^(f.name)); *) let (ftnew,deltree,assocn,beta_flag) = reduce_tree f.address "" ftree false in (* print_endline ("assoc node "^assocn); *) if assocn = "" then (Empty,[],[],[]) (* should not occur in the final version *) else let (rednew,connew,unsolnew) = update_relations deltree redord connections unsolved_list in begin (* Format.open_box 0; print_endline " "; print_pairlist connew; Format.force_newline (); Format.print_flush (); *) if beta_flag = true then begin (* print_endline "beta_flag true"; *) purity ftnew rednew connew unsolnew (* new pure positions may occur; old ones may not longer exist *) end else purity_reduction r ftnew rednew connew unsolnew (* let's finish the old pure positions *) end end in let flist,slist = List.split connections in let pr = collect_pure [ftree] (flist,slist) in purity_reduction pr ftree redord connections unsolved_list let rec betasplit addr ftree redord connections unsolved_list = match ftree with Empty -> print_endline "bsplit Empty tree"; raise jprover_bug | NodeAt(_) -> print_endline "bsplit Atom tree"; raise jprover_bug (* the beta-node should actually occur! *) | NodeA(pos,strees) -> match addr with [] -> (* we are at the beta node under consideration *) let st1tree = (Array.get strees 0) and st2tree = (Array.get strees 1) in let (zw1red,zw1conn,zw1uslist) = update_relations st2tree redord connections unsolved_list and (zw2red,zw2conn,zw2uslist) = update_relations st1tree redord connections unsolved_list in ((NodeA(pos,[|st1tree;Empty|])),zw1red,zw1conn,zw1uslist), ((NodeA(pos,[|Empty;st2tree|])),zw2red,zw2conn,zw2uslist) | f::rest -> let nexttree = Array.get strees (f-1) in let (zw1ft,zw1red,zw1conn,zw1uslist),(zw2ft,zw2red,zw2conn,zw2uslist) = betasplit rest nexttree redord connections unsolved_list in (* let scopytrees = Array.copy strees in *) let zw1trees = myset strees (f-1) zw1ft and zw2trees = myset strees (f-1) zw2ft in (NodeA(pos,zw1trees),zw1red,zw1conn,zw1uslist),(NodeA(pos,zw2trees),zw2red,zw2conn,zw2uslist) let split addr pname ftree redord connections unsolved_list opt_bproof = let (opt_bp1,min_con1),(opt_bp2,min_con2) = split_permutation pname opt_bproof in begin (* print_endline "Beta proof 1: "; print_endline ""; print_beta_proof opt_bp1; print_endline ""; print_endline ("Beta proof 1 connections: "); Format.open_box 0; print_pairlist min_con1; print_endline "."; Format.print_flush(); print_endline ""; print_endline ""; print_endline "Beta proof 2: "; print_endline ""; print_beta_proof opt_bp2; print_endline ""; print_endline ("Beta proof 2 connections: "); Format.open_box 0; print_pairlist min_con2; print_endline "."; Format.print_flush(); print_endline ""; *) let (zw1ft,zw1red,zw1conn,zw1uslist),(zw2ft,zw2red,zw2conn,zw2uslist) = betasplit addr ftree redord connections unsolved_list in (* zw1conn and zw2conn are not longer needed when using beta proofs *) (* print_endline "betasp_out"; *) let ft1,red1,conn1,uslist1 = purity zw1ft zw1red min_con1 zw1uslist in (* print_endline "purity_one_out"; *) let ft2,red2,conn2,uslist2 = purity zw2ft zw2red min_con2 zw2uslist in (* print_endline "purity_two_out"; *) (* again, min_con1 = conn1 and min_con2 = conn2 should hold *) begin (* print_endline ""; print_endline ""; print_endline ("Purity 1 connections: "); Format.open_box 0; print_pairlist conn1; print_endline "."; print_endline ""; Format.print_flush(); print_endline ""; print_endline ""; print_endline ("Purity 2 connections: "); Format.open_box 0; print_pairlist conn2; print_endline "."; print_endline ""; Format.print_flush(); print_endline ""; print_endline ""; *) (ft1,red1,conn1,uslist1,opt_bp1),(ft2,red2,conn2,uslist2,opt_bp2) end end (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Splitting end %%%%%%%%%%%%%%%% *) (* for wait labels we collect all solved atoms with pol=0 *) let rec collect_solved_O_At ftreelist slist = match ftreelist with [] -> [] | f::r -> match f with Empty -> (* may become possible after purity *) collect_solved_O_At r slist | NodeAt(pos) -> if ((List.mem (pos.name) slist) or (pos.pol = I)) then (* recall slist is the unsolved list *) collect_solved_O_At r slist else (* here, we have pos solved and pos.pol = O) *) pos::(collect_solved_O_At r slist) | NodeA(pos,treearray) -> collect_solved_O_At ((Array.to_list treearray) @ r) slist let rec red_ord_block pname redord = match redord with [] -> false | (f,fset)::r -> if ((f = pname) or (not (StringSet.mem pname fset))) then red_ord_block pname r else true (* then, we have (StringSet.mem pname fset) *) let rec check_wait_succ_LJ faddress ftree = match ftree with Empty -> raise jprover_bug | NodeAt(pos) -> raise jprover_bug (* we have an gamma_0 position or an or-formula *) | NodeA(pos,strees) -> match faddress with [] -> if pos.op = Or then match (strees.(0),strees.(1)) with (Empty,Empty) -> raise (Invalid_argument "Jprover: redundancies occur") | (Empty,_) -> (false,2) (* determines the Orr2 rule *) | (_,Empty) -> (false,1) (* determines the Orr1 ruke *) | (_,_) -> (true,0) (* wait-label is set *) else (false,0) | f::r -> if r = [] then if (pos.pt = Gamma) & ((nonemptys strees 0 (Array.length strees)) > 1) then (true,0) (* we are at a gamma position (exr) with one than one successor -- wait label in LJ*) else check_wait_succ_LJ r (Array.get strees (f-1)) else check_wait_succ_LJ r (Array.get strees (f-1)) let blocked f po redord ftree connections slist logic calculus opt_bproof = (* print_endline ("Blocking check "^(f.name)); *) if (red_ord_block (f.name) redord) then begin (* print_endline "wait-1 check positive"; *) true,0 end else if logic = "C" then false,0 (* ready, in C only redord counts *) else let pa_O = collect_solved_O_At [ftree] slist (* solved atoms in ftree *) and po_test = (delete f po) in if calculus = "LJmc" then (* we provide dynamic wait labels for both sequent calculi *) (* print_endline "wait-2 check"; *) if (f.st = Psi_0) & (f.pt <> PNull) & ((pa_O <> []) or (List.exists (fun x -> x.pol = O) po_test)) then begin (* print_endline "wait-2 positive"; *) true,0 (* wait_2 label *) end else begin (* print_endline "wait-2 negative"; *) false,0 end else (* calculus is supposed to be LJ *) if calculus = "LJ" then if ((f.st = Phi_0) & ((f.op=Neg) or (f.op=Imp)) & ((pa_O <> []) or (List.exists (fun x -> x.pol = O) po_test)) ) (* this would cause an impl or negl rule with an non-empty succedent *) then if (f.op=Neg) then true,0 else (* (f.op=Imp) *) (* In case of an impl rule on A => B, the wait_label must NOT be set iff all succedent formulae depend exclusively on B. For this, we perform a split operation and determine, if in the A-subgoal all succedent formulae are pure, i.e.~have been deleted from treds. Otherwise, in case of A-dependent succedent formulae, the wait_label must be set. *) let ((_,min_con1),_) = split_permutation f.name opt_bproof in let slist_fake = delete f.name slist in let ((zw1ft,zw1red,_,zw1uslist),_) = betasplit (f.address) ftree redord connections slist_fake in let ft1,_,_,uslist1 = purity zw1ft zw1red min_con1 zw1uslist in (* print_endline "wait label purity_one_out"; *) let ft1_root = (List.hd (List.tl (tpredsucc f ft1))) in (* print_endline ("wait-root "^(ft1_root.name)); *) let po_fake = compute_open [ft1] uslist1 in let po_fake_test = delete ft1_root po_fake and pa_O_fake = collect_solved_O_At [ft1] uslist1 in (* print_purelist (po_fake_test @ pa_O_fake); *) if ((pa_O_fake <> []) or (List.exists (fun x -> x.pol = O) po_fake_test)) then true,0 else false,0 else if ((f.pol=O) & ((f.st=Gamma_0) or (f.op=Or))) then let (bool,orr_flag) = check_wait_succ_LJ f.address ftree in (bool,orr_flag) (* here is determined if orr1 or orr2 will be performed, provided bool=false) *) (* orr_flag can be 1 or 2 *) else false,0 else raise (Invalid_argument "Jprover: calculus should be LJmc or LJ") let rec get_beta_preference list actual = match list with [] -> actual | (f,int)::r -> if f.op = Imp then (f,int) else (* if f.op = Or then get_beta_preference r (f,int) else *) get_beta_preference r actual exception Gamma_deadlock let rec select_pos search_po po redord ftree connections slist logic calculus candidates opt_bproof = match search_po with [] -> (match candidates with [] -> if calculus = "LJ" then raise Gamma_deadlock (* permutation may be necessary *) else raise (Invalid_argument "Jprover bug: overall deadlock") (* this case should not occur *) | c::rest -> get_beta_preference (c::rest) c ) | f::r -> (* there exist an open position *) let (bool,orr_flag) = (blocked f po redord ftree connections slist logic calculus opt_bproof) in if (bool = true) then select_pos r po redord ftree connections slist logic calculus candidates opt_bproof else if f.pt = Beta then (* search for non-splitting rules first *) (* let beta_candidate = if candidates = [] then [(f,orr_flag)] else !!!! but preserve first found candidate !!!!!!! candidates in !!!!!!! this strategy is not sure the best -- back to old !!!!!!!!! *) select_pos r po redord ftree connections slist logic calculus ((f,orr_flag)::candidates) opt_bproof else (f,orr_flag) (* let rec get_position_in_tree pname treelist = match treelist with [] -> raise jprover_bug | f::r -> begin match f with Empty -> get_position_in_tree pname r | NodeAt(pos) -> if pos.name = pname then pos else get_position_in_tree pname r | NodeA(pos,suctrees) -> get_position_in_tree pname ((Array.to_list suctrees) @ r) end *) (* total corresponds to tot in the thesis, tot simulates the while-loop, solve is the rest *) let rec total ftree redord connections csigmaQ slist logic calculus opt_bproof = let rec tot ftree redord connections po slist = let rec solve ftree redord connections p po slist (pred,succs) orr_flag = let newslist = delete (p.name) slist in let rback = if p.st = Gamma_0 then begin (* print_endline "that's the gamma rule"; *) [((p.name,pred.name),(build_rule pred p csigmaQ orr_flag calculus))] end else [] in (* print_endline "gamma check finish"; *) let pnew = if p.pt <> Beta then succs @ (delete p po) else po in match p.pt with Gamma -> rback @ (tot ftree redord connections pnew newslist) | Psi -> if p.op = At then let succ = List.hd succs in rback @ (solve ftree redord connections succ pnew newslist (p,[]) orr_flag) (* solve atoms immediately *) else rback @ (tot ftree redord connections pnew newslist) | Phi -> if p.op = At then let succ = List.hd succs in rback @ (solve ftree redord connections succ pnew newslist (p,[]) orr_flag) (* solve atoms immediately *) else rback @ (tot ftree redord connections pnew newslist) | PNull -> let new_redord = update p.name redord in let (c1,c2) = select_connection (p.name) connections newslist in if (c1= "none" & c2 ="none") then rback @ (tot ftree new_redord connections pnew newslist) else let (ass_pos,inst_pos) = (* need the pol=O position ass_pos of the connection for later permutation *) (* need the pol=I position inst_pos for NuPRL instantiation *) if p.name = c1 then if p.pol = O then (c1,c2) else (c2,c1) else (* p.name = c2 *) if p.pol = O then (c2,c1) else (c1,c2) in rback @ [(("",ass_pos),(build_rule p p csigmaQ orr_flag calculus))] (* one possibility of recursion end *) | Alpha -> rback @ ((("",p.name),(build_rule p p csigmaQ orr_flag calculus))::(tot ftree redord connections pnew newslist)) | Delta -> let sp = List.hd succs in rback @ ((("",p.name),(build_rule p sp csigmaQ orr_flag calculus))::(tot ftree redord connections pnew newslist)) | Beta -> (* print_endline "split_in"; *) let (ft1,red1,conn1,uslist1,opt_bproof1),(ft2,red2,conn2,uslist2,opt_bproof2) = split (p.address) (p.name) ftree redord connections newslist opt_bproof in let (sigmaQ1,sigmaQ2) = subst_split ft1 ft2 ftree uslist1 uslist2 newslist csigmaQ in (* print_endline "split_out"; *) let p1 = total ft1 red1 conn1 sigmaQ1 uslist1 logic calculus opt_bproof1 in (* print_endline "compute p1 out"; *) let p2 = total ft2 red2 conn2 sigmaQ2 uslist2 logic calculus opt_bproof2 in (* print_endline "compute p2 out"; *) rback @ [(("",p.name),(build_rule p p csigmaQ orr_flag calculus))] @ p1 @ p2 (* second possibility of recursion end *) in begin try let (p,orr_flag) = select_pos po po redord ftree connections slist logic calculus [] opt_bproof (* last argument for guiding selection strategy *) in (* print_endline ((p.name)^" "^(string_of_int orr_flag)); *) let predsuccs = tpredsucc p ftree in let pred = List.hd predsuccs and succs = List.tl predsuccs in let redpo = update (p.name) redord in (* deletes the entry (p,psuccset) from the redord *) let rednew = if (p.pt = Delta) then (* keep the tree ordering for the successor position only *) let psucc = List.hd succs in let ppsuccs = tpredsucc psucc ftree in let pre = List.hd ppsuccs and sucs = List.tl ppsuccs in replace_ordering (psucc.name) sucs redpo (* union the succsets of psucc *) else redpo in (* print_endline "update ok"; *) solve ftree rednew connections p po slist (pred,succs) orr_flag with Gamma_deadlock -> let ljmc_subproof = total ftree redord connections csigmaQ slist "J" "LJmc" opt_bproof in eigen_counter := 1; permute_ljmc ftree po slist ljmc_subproof (* the permuaiton result will be appended to the lj proof constructed so far *) end in let po = compute_open [ftree] slist in tot ftree redord connections po slist let reconstruct ftree redord sigmaQ ext_proof logic calculus = let min_connections = remove_dups_connections ext_proof in let (opt_bproof,beta_exp,closures) = construct_opt_beta_proof ftree ext_proof in (* let connections = remove_dups_connections ext_proof in let bproof,beta_exp,closures = construct_beta_proof ftree connections in let (opt_bproof,min_connections) = bproof_purity bproof in *) if !debug_jprover then begin print_endline ""; print_endline ("Beta proof with number of closures = "^(string_of_int closures)^" and number of beta expansions = "^(string_of_int beta_exp)); (* print_endline ""; print_endline ""; print_beta_proof bproof; print_endline ""; print_endline ""; print_endline "Optimal beta proof: "; print_endline ""; print_endline ""; print_beta_proof opt_bproof; print_endline ""; print_endline ""; print_endline ("Beta proof connections: "); Format.open_box 0; print_pairlist min_connections; print_endline "."; Format.print_flush(); *) print_endline ""; end; let (newroot_name,unsolved_list) = build_unsolved ftree in let redord2 = (update newroot_name redord) in (* otherwise we would have a deadlock *) let (init_tree,init_redord,init_connections,init_unsolved_list) = purity ftree redord2 min_connections unsolved_list in begin (* print_endline ""; print_endline ""; print_endline ("Purity connections: "); Format.open_box 0; print_pairlist init_connections; print_endline "."; print_endline ""; Format.print_flush(); print_endline ""; print_endline ""; *) (* it should hold: min_connections = init_connections *) total init_tree init_redord init_connections sigmaQ init_unsolved_list logic calculus opt_bproof end (* ***************** REDUCTION ORDERING -- both types **************************** *) exception Reflexive let rec transitive_irreflexive_closure addset const ordering = match ordering with [] -> [] | (pos,fset)::r -> if (pos = const) or (StringSet.mem const fset) then (* check reflexsivity during transitive closure wrt. addset ONLY!!! *) if StringSet.mem pos addset then raise Reflexive else (pos,(StringSet.union fset addset))::(transitive_irreflexive_closure addset const r) else (pos,fset)::(transitive_irreflexive_closure addset const r) let rec search_set var ordering = (* print_endline var; *) match ordering with [] -> raise (Invalid_argument "Jprover: element in ordering missing") | (pos,fset)::r -> if pos = var then StringSet.add pos fset else search_set var r let add_sets var const ordering = let addset = search_set var ordering in transitive_irreflexive_closure addset const ordering (* ************* J ordering ********************************************** *) let rec add_arrowsJ (v,vlist) ordering = match vlist with [] -> ordering | f::r -> if ((String.get f 0)='c') then let new_ordering = add_sets v f ordering in add_arrowsJ (v,r) new_ordering else add_arrowsJ (v,r) ordering let rec add_substJ replace_vars replace_string ordering atom_rel = match replace_vars with [] -> ordering | v::r -> if (String.get v 1 = 'n') (* don't integrate new variables *) or (List.exists (fun (x,_,_) -> (x.aname = v)) atom_rel) then (* no reduction ordering at atoms *) (add_substJ r replace_string ordering atom_rel) else let next_ordering = add_arrowsJ (v,replace_string) ordering in (add_substJ r replace_string next_ordering atom_rel) let build_orderingJ replace_vars replace_string ordering atom_rel = try add_substJ replace_vars replace_string ordering atom_rel with Reflexive -> (* only possible in the FO case *) raise Not_unifiable (*search for alternative string unifiers *) let rec build_orderingJ_list substJ ordering atom_rel = match substJ with [] -> ordering | (v,vlist)::r -> let next_ordering = build_orderingJ [v] vlist ordering atom_rel in build_orderingJ_list r next_ordering atom_rel (* ************* J ordering END ********************************************** *) (* ************* quantifier ordering ********************************************** *) let rec add_arrowsQ v clist ordering = match clist with [] -> ordering | f::r -> let new_ordering = add_sets v f ordering in add_arrowsQ v r new_ordering let rec print_sigmaQ sigmaQ = match sigmaQ with [] -> print_endline "." | (v,term)::r -> begin Format.open_box 0; print_endline " "; print_string (v^" = "); print_term stdout term; Format.force_newline (); Format.print_flush (); print_sigmaQ r end let rec print_term_list tlist = match tlist with [] -> print_string "." | t::r -> begin print_term stdout t; print_string " "; print_term_list r end let rec add_sigmaQ new_elements ordering = match new_elements with [] -> ([],ordering) | (v,termlist)::r -> let dterms = collect_delta_terms termlist in begin (*: print_stringlist dterms; mbreak "add_sigmaQ:1\n"; Format.open_box 0; print_endline " "; print_endline "sigmaQ: "; print_string (v^" = "); print_term_list termlist; Format.force_newline (); print_stringlist dterms; Format.force_newline (); Format.print_flush (); mbreak "add_sigmaQ:2\n"; :*) let new_ordering = add_arrowsQ v dterms ordering in (*: print_ordering new_ordering; mbreak "add_sigmaQ:3\n"; :*) let (rest_pairs,rest_ordering) = add_sigmaQ r new_ordering in ((v,dterms)::rest_pairs),rest_ordering end let build_orderingQ new_elements ordering = (* new_elements is of type (string * term list) list, since one variable can receive more than *) (* a single term due to substitution multiplication *) try (* print_endline "build orderingQ in"; *) (* apple *) add_sigmaQ new_elements ordering; with Reflexive -> raise Failed (* new connection, please *) (* ************* quantifier ordering END ********************************************** *) (* ****** Quantifier unification ************** *) (* For multiplication we assume always idempotent substitutions sigma, tau! *) let rec collect_assoc inst_vars tauQ = match inst_vars with [] -> [] | f::r -> let f_term = List.assoc f tauQ in f_term::(collect_assoc r tauQ) let rec rec_apply sigmaQ tauQ tau_vars tau_terms = match sigmaQ with [] -> [],[] | (v,term)::r -> let app_term = subst term tau_vars tau_terms in let old_free = free_vars_list term and new_free = free_vars_list app_term in let inst_vars = list_diff old_free new_free in let inst_terms = collect_assoc inst_vars tauQ in let (rest_sigma,rest_sigma_ordering) = rec_apply r tauQ tau_vars tau_terms in if inst_terms = [] then ((v,app_term)::rest_sigma),rest_sigma_ordering else let ordering_v = String.sub v 0 (String.index v '_') in ((v,app_term)::rest_sigma),((ordering_v,inst_terms)::rest_sigma_ordering) (* let multiply sigmaQ tauQ = let tau_vars,tau_terms = List.split tauQ and sigma_vars,sigma_terms = List.split sigmaQ in let apply_terms = rec_apply sigma_terms tau_vars tau_terms in (List.combine sigma_vars apply_terms) @ tauQ *) let multiply sigmaQ tauQ = let (tau_vars,tau_terms) = List.split tauQ in let (new_sigmaQ,sigma_ordering) = rec_apply sigmaQ tauQ tau_vars tau_terms in let tau_ordering_terms = (List.map (fun x -> [x]) tau_terms) (* for extending ordering_elements *) in let tau_ordering_vars = (List.map (fun x -> String.sub x 0 (String.index x '_')) tau_vars) in let tau_ordering = (List.combine tau_ordering_vars tau_ordering_terms) in ((new_sigmaQ @ tauQ), (sigma_ordering @ tau_ordering) ) let apply_2_sigmaQ term1 term2 sigmaQ = let sigma_vars,sigma_terms = List.split sigmaQ in (subst term1 sigma_vars sigma_terms),(subst term2 sigma_vars sigma_terms) let jqunify term1 term2 sigmaQ = let app_term1,app_term2 = apply_2_sigmaQ term1 term2 sigmaQ in try (*: let tauQ = unify_mm app_term1 app_term2 String_set.StringSet.empty in :*) let tauQ = unify_mm app_term1 app_term2 StringSet.empty in let (mult,oel) = multiply sigmaQ tauQ in (mult,oel) with RefineError _ -> (* any unification failure *) (* print_endline "fo-unification fail"; *) raise Failed (* new connection, please *) (* ************ T-STRING UNIFICATION ******************************** *) let rec combine subst (ov,oslist) = match subst with [] -> [],[] | f::r -> let (v,slist) = f in let rest_vlist,rest_combine = (combine r (ov,oslist)) in if (List.mem ov slist) then (* subst assumed to be idemponent *) let com_element = com_subst slist (ov,oslist) in (v::rest_vlist),((v,com_element)::rest_combine) else (rest_vlist,(f::rest_combine)) let compose sigma one_subst = let (n,subst)=sigma and (ov,oslist) = one_subst in let (trans_vars,com) = combine subst (ov,oslist) in (* begin print_endline "!!!!!!!!!test print!!!!!!!!!!"; print_subst [one_subst]; print_subst subst; print_endline "!!!!!!!!! END test print!!!!!!!!!!"; *) if List.mem one_subst subst then (trans_vars,(n,com)) else (* ov may multiply as variable in subst with DIFFERENT values *) (* in order to avoid explicit atom instances!!! *) (trans_vars,(n,(com @ [one_subst]))) (* end *) let rec apply_element fs ft (v,slist) = match (fs,ft) with ([],[]) -> ([],[]) | ([],(ft_first::ft_rest)) -> let new_ft_first = if ft_first = v then slist else [ft_first] in let (emptylist,new_ft_rest) = apply_element [] ft_rest (v,slist) in (emptylist,(new_ft_first @ new_ft_rest)) | ((fs_first::fs_rest),[]) -> let new_fs_first = if fs_first = v then slist else [fs_first] in let (new_fs_rest,emptylist) = apply_element fs_rest [] (v,slist) in ((new_fs_first @ new_fs_rest),emptylist) | ((fs_first::fs_rest),(ft_first::ft_rest)) -> let new_fs_first = if fs_first = v then slist else [fs_first] and new_ft_first = if ft_first = v then slist else [ft_first] in let (new_fs_rest,new_ft_rest) = apply_element fs_rest ft_rest (v,slist) in ((new_fs_first @ new_fs_rest),(new_ft_first @ new_ft_rest)) let rec shorten us ut = match (us,ut) with ([],_) -> (us,ut) | (_,[]) -> (us,ut) | ((fs::rs),(ft::rt)) -> if fs = ft then shorten rs rt else (us,ut) let rec apply_subst_list eq_rest (v,slist) = match eq_rest with [] -> (true,[]) | (atomnames,(fs,ft))::r -> let (n_fs,n_ft) = apply_element fs ft (v,slist) in let (new_fs,new_ft) = shorten n_fs n_ft in (* delete equal first elements *) match (new_fs,new_ft) with [],[] -> let (bool,new_eq_rest) = apply_subst_list r (v,slist) in (bool,((atomnames,([],[]))::new_eq_rest)) | [],(fft::rft) -> if (is_const fft) then (false,[]) else let (bool,new_eq_rest) = apply_subst_list r (v,slist) in (bool,((atomnames,([],new_ft))::new_eq_rest)) | (ffs::rfs),[] -> if (is_const ffs) then (false,[]) else let (bool,new_eq_rest) = apply_subst_list r (v,slist) in (bool,((atomnames,(new_fs,[]))::new_eq_rest)) | (ffs::rfs),(fft::rft) -> if (is_const ffs) & (is_const fft) then (false,[]) (* different first constants cause local fail *) else (* at least one of firsts is a variable *) let (bool,new_eq_rest) = apply_subst_list r (v,slist) in (bool,((atomnames,(new_fs,new_ft))::new_eq_rest)) let apply_subst eq_rest (v,slist) atomnames = if (List.mem v atomnames) then (* don't apply subst to atom variables !! *) (true,eq_rest) else apply_subst_list eq_rest (v,slist) let all_variable_check eqlist = false (* needs some discussion with Jens! -- NOT done *) (* let rec all_variable_check eqlist = match eqlist with [] -> true | ((_,(fs,ft))::rest_eq) -> if (fs <> []) & (ft <> []) then let fs_first = List.hd fs and ft_first = List.hd ft in if (is_const fs_first) or (is_const ft_first) then false else all_variable_check rest_eq else false *) let rec tunify_list eqlist init_sigma orderingQ atom_rel = let rec tunify atomnames fs ft rt rest_eq sigma ordering = let apply_r1 fs ft rt rest_eq sigma = (* print_endline "r1"; *) tunify_list rest_eq sigma ordering atom_rel in let apply_r2 fs ft rt rest_eq sigma = (* print_endline "r2"; *) tunify atomnames rt fs ft rest_eq sigma ordering in let apply_r3 fs ft rt rest_eq sigma = (* print_endline "r3"; *) let rfs = (List.tl fs) and rft = (List.tl rt) in tunify atomnames rfs ft rft rest_eq sigma ordering in let apply_r4 fs ft rt rest_eq sigma = (* print_endline "r4"; *) tunify atomnames rt ft fs rest_eq sigma ordering in let apply_r5 fs ft rt rest_eq sigma = (* print_endline "r5"; *) let v = (List.hd fs) in let (compose_vars,new_sigma) = compose sigma (v,ft) in let (bool,new_rest_eq) = apply_subst rest_eq (v,ft) atomnames in if (bool=false) then raise Not_unifiable else let new_ordering = build_orderingJ (v::compose_vars) ft ordering atom_rel in tunify atomnames (List.tl fs) rt rt new_rest_eq new_sigma new_ordering in let apply_r6 fs ft rt rest_eq sigma = (* print_endline "r6"; *) let v = (List.hd fs) in let (_,new_sigma) = (compose sigma (v,[])) in let (bool,new_rest_eq) = apply_subst rest_eq (v,[]) atomnames in if (bool=false) then raise Not_unifiable else (* no relation update since [] has been replaced for v *) tunify atomnames (List.tl fs) ft rt new_rest_eq new_sigma ordering in let apply_r7 fs ft rt rest_eq sigma = (* print_endline "r7"; *) let v = (List.hd fs) and c1 = (List.hd rt) and c2t =(List.tl rt) in let (compose_vars,new_sigma) = (compose sigma (v,(ft @ [c1]))) in let (bool,new_rest_eq) = apply_subst rest_eq (v,(ft @ [c1])) atomnames in if bool=false then raise Not_unifiable else let new_ordering = build_orderingJ (v::compose_vars) (ft @ [c1]) ordering atom_rel in tunify atomnames (List.tl fs) [] c2t new_rest_eq new_sigma new_ordering in let apply_r8 fs ft rt rest_eq sigma = (* print_endline "r8"; *) tunify atomnames rt [(List.hd fs)] (List.tl fs) rest_eq sigma ordering in let apply_r9 fs ft rt rest_eq sigma = (* print_endline "r9"; *) let v = (List.hd fs) and (max,subst) = sigma in let v_new = ("vnew"^(string_of_int max)) in let (compose_vars,new_sigma) = (compose ((max+1),subst) (v,(ft @ [v_new]))) in let (bool,new_rest_eq) = apply_subst rest_eq (v,(ft @ [v_new])) atomnames in if (bool=false) then raise Not_unifiable else let new_ordering = build_orderingJ (v::compose_vars) (ft @ [v_new]) ordering atom_rel in tunify atomnames rt [v_new] (List.tl fs) new_rest_eq new_sigma new_ordering in let apply_r10 fs ft rt rest_eq sigma = (* print_endline "r10"; *) let x = List.hd rt in tunify atomnames fs (ft @ [x]) (List.tl rt) rest_eq sigma ordering in if r_1 fs ft rt then apply_r1 fs ft rt rest_eq sigma else if r_2 fs ft rt then apply_r2 fs ft rt rest_eq sigma else if r_3 fs ft rt then apply_r3 fs ft rt rest_eq sigma else if r_4 fs ft rt then apply_r4 fs ft rt rest_eq sigma else if r_5 fs ft rt then apply_r5 fs ft rt rest_eq sigma else if r_6 fs ft rt then (try apply_r6 fs ft rt rest_eq sigma with Not_unifiable -> if r_7 fs ft rt then (* r7 applicable if r6 was and tr6 = C2t' *) (try apply_r7 fs ft rt rest_eq sigma with Not_unifiable -> apply_r10 fs ft rt rest_eq sigma (* r10 always applicable if r6 was *) ) else (* r10 could be represented only once if we would try it before r7.*) (* but looking at the transformation rules, r10 should be tried at last in any case *) apply_r10 fs ft rt rest_eq sigma (* r10 always applicable r6 was *) ) else if r_7 fs ft rt then (* not r6 and r7 possible if z <> [] *) (try apply_r7 fs ft rt rest_eq sigma with Not_unifiable -> apply_r10 fs ft rt rest_eq sigma (* r10 always applicable if r7 was *) ) else if r_8 fs ft rt then (try apply_r8 fs ft rt rest_eq sigma with Not_unifiable -> if r_10 fs ft rt then (* r10 applicable if r8 was and tr8 <> [] *) apply_r10 fs ft rt rest_eq sigma else raise Not_unifiable (* simply back propagation *) ) else if r_9 fs ft rt then (try apply_r9 fs ft rt rest_eq sigma with Not_unifiable -> if r_10 fs ft rt then (* r10 applicable if r9 was and tr9 <> [] *) apply_r10 fs ft rt rest_eq sigma else raise Not_unifiable (* simply back propagation *) ) else if r_10 fs ft rt then (* not ri, i<10, and r10 possible if for instance *) (* (s=[] and x=v1) or (z<>[] and xt=C1V1t') *) apply_r10 fs ft rt rest_eq sigma else (* NO rule applicable *) raise Not_unifiable in match eqlist with [] -> init_sigma,orderingQ | f::rest_eq -> begin (* Format.open_box 0; print_equations [f]; Format.print_flush (); *) let (atomnames,(fs,ft)) = f in tunify atomnames fs [] ft rest_eq init_sigma orderingQ end let rec test_apply_eq atomnames eqs eqt subst = match subst with [] -> (eqs,eqt) | (f,flist)::r -> let (first_appl_eqs,first_appl_eqt) = if List.mem f atomnames then (eqs,eqt) else (apply_element eqs eqt (f,flist)) in test_apply_eq atomnames first_appl_eqs first_appl_eqt r let rec test_apply_eqsubst eqlist subst = match eqlist with [] -> [] | f::r -> let (atomnames,(eqs,eqt)) = f in let applied_element = test_apply_eq atomnames eqs eqt subst in (atomnames,applied_element)::(test_apply_eqsubst r subst) let ttest us ut ns nt eqlist orderingQ atom_rel = let (short_us,short_ut) = shorten us ut in (* apply intial rule R3 *) (* to eliminate common beginning *) let new_element = ([ns;nt],(short_us,short_ut)) in let full_eqlist = if List.mem new_element eqlist then eqlist else new_element::eqlist in let (sigma,_) = tunify_list full_eqlist (1,[]) orderingQ atom_rel in let (n,subst) = sigma in let test_apply = test_apply_eqsubst full_eqlist subst in begin print_endline ""; print_endline "Final equations:"; print_equations full_eqlist; print_endline ""; print_endline "Final substitution:"; print_tunify sigma; print_endline ""; print_endline "Applied equations:"; print_equations test_apply end let do_stringunify us ut ns nt equations fo_eqlist orderingQ atom_rel qmax = let (short_us,short_ut) = shorten us ut in (* apply intial rule R3 to eliminate common beginning *) let new_element = ([ns;nt],(short_us,short_ut)) in let full_eqlist = if List.mem new_element equations then equations @ fo_eqlist else (new_element::equations) @ fo_eqlist in try (* print_equations full_eqlist; *) (* max-1 new variables have been used for the domain equations *) let (new_sigma,new_ordering) = tunify_list full_eqlist (1,[]) orderingQ atom_rel in (* sigmaQ will not be returned in eqlist *) (new_sigma,(qmax,full_eqlist),new_ordering) with Not_unifiable -> raise Failed (* new connection please *) let rec one_equation gprefix dlist delta_0_prefixes n = match dlist with [] -> ([],n) | f::r -> let fprefix = List.assoc f delta_0_prefixes in let (sf1,sg) = shorten fprefix gprefix and v_new = ("vnewq"^(string_of_int n)) in let fnew = sf1 @ [v_new] in let (rest_equations,new_n) = one_equation gprefix r delta_0_prefixes (n+1) in (([],(fnew,sg))::rest_equations),new_n let rec make_domain_equations fo_pairs (gamma_0_prefixes,delta_0_prefixes) n = match fo_pairs with [] -> ([],n) | (g,dlist)::r -> let gprefix = List.assoc g gamma_0_prefixes in let (gequations,max) = one_equation gprefix dlist delta_0_prefixes n in let (rest_equations,new_max) = make_domain_equations r (gamma_0_prefixes,delta_0_prefixes) max in (gequations @ rest_equations),new_max (* type of one unifier: int * ((string * string list) list) *) (* global failure: (0,[]) *) let stringunify ext_atom try_one eqlist fo_pairs logic orderingQ atom_rel qprefixes = if logic = "C" then ((0,[]),(0,[]),orderingQ) else let (qmax,equations) = eqlist and us = ext_atom.aprefix and ut = try_one.aprefix and ns = ext_atom.aname and nt = try_one.aname in if qprefixes = ([],[]) then (* prop case *) begin (* print_endline "This is the prop case"; *) let (new_sigma,new_eqlist) = Jtunify.do_stringunify us ut ns nt equations (* prop unification only *) in (new_sigma,new_eqlist,[]) (* assume the empty reduction ordering during proof search *) end else begin (* print_endline "This is the FO case"; *) (* fo_eqlist encodes the domain condition on J quantifier substitutions *) (* Again, always computed for the whole substitution sigmaQ *) let (fo_eqlist,new_max) = make_domain_equations fo_pairs qprefixes qmax in begin (* Format.open_box 0; print_string "domain equations in"; print_equations fo_eqlist; print_string "domain equations out"; Format.print_flush (); *) do_stringunify us ut ns nt equations fo_eqlist orderingQ atom_rel new_max end end (**************************************** add multiplicity *********************************) let rec subst_replace subst_list t = match subst_list with [] -> t | (old_t,new_t)::r -> let inter_term = var_subst t old_t "dummy" in (*: print_string "("; print_term stdout old_t; print_string " --> "; print_term stdout new_t; print_string ")\n"; print_term stdout t; print_newline (); print_term stdout inter_term; print_newline (); :*) let new_term = subst1 inter_term "dummy" new_t in (*: print_term stdout new_term; print_newline (); mbreak "\n+++========----- ---------..........\n"; :*) subst_replace r new_term let rename_pos x m = let pref = String.get x 0 in (Char.escaped pref)^(string_of_int m) let update_position position m replace_n subst_list mult = let ({name=x; address=y; op=z; pol=p; pt=a; st=b; label=t}) = position in let nx = rename_pos x m in let nsubst_list = if b=Gamma_0 then let vx = mk_var_term (x^"_jprover") and vnx = mk_var_term (nx^"_jprover") in (vx,vnx)::subst_list else if b=Delta_0 then let sx = mk_string_term jprover_op x and snx = mk_string_term jprover_op nx in (sx,snx)::subst_list else subst_list in let nt = subst_replace nsubst_list t in let add_array = Array.of_list y in let _ = (add_array.(replace_n) <- mult) in let new_add = Array.to_list add_array in ({name=nx; address=new_add; op=z; pol=p; pt=a; st=b; label=nt},m,nsubst_list) let rec append_orderings list_of_lists = match list_of_lists with [] -> [] | f::r -> f @ (append_orderings r) let rec union_orderings first_orderings = match first_orderings with [] -> StringSet.empty | (pos,fset)::r -> StringSet.union (StringSet.add pos fset) (union_orderings r) let rec select_orderings add_orderings = match add_orderings with [] -> [] | f::r -> (List.hd f)::select_orderings r let combine_ordering_list add_orderings pos_name = let first_orderings = select_orderings add_orderings in let pos_succs = union_orderings first_orderings in let rest_orderings = append_orderings add_orderings in (pos_name,pos_succs)::rest_orderings let rec copy_and_rename_tree last_tree replace_n pos_n mult subst_list = let rec rename_subtrees tree_list nposition s_pos_n nsubst_list = match tree_list with [] -> ([||],[],s_pos_n) | f::r -> let (f_subtree,f_ordering,f_pos_n) = copy_and_rename_tree f replace_n s_pos_n mult nsubst_list in let (r_subtrees,r_ordering_list,r_pos_n) = rename_subtrees r nposition f_pos_n nsubst_list in ((Array.append [|f_subtree|] r_subtrees),(f_ordering::r_ordering_list),r_pos_n) in match last_tree with Empty -> raise (Invalid_argument "Jprover: copy tree") | NodeAt(position) -> (* can never be a Gamma_0 position -> no replacements *) let (nposition,npos_n,_) = update_position position (pos_n+1) replace_n subst_list mult in ((NodeAt(nposition)),[(nposition.name,StringSet.empty)],npos_n) | NodeA(position, suctrees) -> let (nposition,npos_n,nsubst_list) = update_position position (pos_n+1) replace_n subst_list mult in let (new_suctrees, new_ordering_list, new_pos_n) = rename_subtrees (Array.to_list suctrees) nposition npos_n nsubst_list in let new_ordering = combine_ordering_list new_ordering_list (nposition.name) in ((NodeA(nposition,new_suctrees)),new_ordering,new_pos_n) (* we construct for each pos a list orderings representing and correspondning to the array of succtrees *) let rec add_multiplicity ftree pos_n mult logic = let rec parse_subtrees tree_list s_pos_n = match tree_list with [] -> ([||],[],s_pos_n) | f::r -> let (f_subtree,f_ordering,f_pos_n) = add_multiplicity f s_pos_n mult logic in let (r_subtrees,r_ordering_list,r_pos_n) = parse_subtrees r f_pos_n in ((Array.append [|f_subtree|] r_subtrees),(f_ordering::r_ordering_list),r_pos_n) in match ftree with Empty -> raise (Invalid_argument "Jprover: add mult") | NodeAt(pos) -> (ftree,[(pos.name,StringSet.empty)],pos_n) | NodeA(pos,suctrees) -> let (new_suctrees, new_ordering_list, new_pos_n) = parse_subtrees (Array.to_list suctrees) pos_n in if (((pos.pt = Phi) & (((pos.op <> At) & (logic="J")) or ((pos.op = All) & (logic = "C")))) (* no explicit atom-instances *) or ((pos.pt = Gamma) & (pos.st <> Phi_0))) then (* universal quantifiers are copied *) (* at their Phi positions *) let replace_n = (List.length pos.address) (* points to the following argument in the array_of_address *) and last = (Array.length new_suctrees) - 1 in (* array first element has index 0 *) let last_tree = new_suctrees.(last) in let (add_tree,add_ordering,final_pos_n) = copy_and_rename_tree last_tree replace_n new_pos_n mult [] in let final_suctrees = Array.append new_suctrees [|add_tree|] and add_orderings = List.append new_ordering_list [add_ordering] in let final_ordering = combine_ordering_list add_orderings (pos.name) in ((NodeA(pos,final_suctrees)),final_ordering,final_pos_n) else let final_ordering = combine_ordering_list new_ordering_list (pos.name) in ((NodeA(pos,new_suctrees)),final_ordering,new_pos_n) (************** Path checker ****************************************************) let rec get_sets atom atom_sets = match atom_sets with [] -> raise (Invalid_argument "Jprover bug: atom not found") | f::r -> let (a,b,c) = f in if atom = a then f else get_sets atom r let rec get_connections a alpha tabulist = match alpha with [] -> [] | f::r -> if (a.apredicate = f.apredicate) & (a.apol <> f.apol) & (not (List.mem f tabulist)) then (a,f)::(get_connections a r tabulist) else (get_connections a r tabulist) let rec connections atom_rel tabulist = match atom_rel with [] -> [] | f::r -> let (a,alpha,beta) = f in (get_connections a alpha tabulist) @ (connections r (a::tabulist)) let check_alpha_relation atom set atom_sets = let (a,alpha,beta) = get_sets atom atom_sets in AtomSet.subset set alpha let rec extset atom_sets path closed = match atom_sets with [] -> AtomSet.empty | f::r -> let (at,alpha,beta) = f in if (AtomSet.subset path alpha) & (AtomSet.subset closed beta) then AtomSet.add at (extset r path closed) else (extset r path closed) let rec check_ext_list ext_list fail_set atom_sets = (* fail_set consists of one atom only *) match ext_list with [] -> AtomSet.empty | f::r -> if (check_alpha_relation f fail_set atom_sets) then AtomSet.add f (check_ext_list r fail_set atom_sets) else (check_ext_list r fail_set atom_sets) let fail_ext_set ext_atom ext_set atom_sets = let ext_list = AtomSet.elements ext_set and fail_set = AtomSet.add ext_atom AtomSet.empty in check_ext_list ext_list fail_set atom_sets let rec ext_partners con path ext_atom (reduction_partners,extension_partners) atom_sets = match con with [] -> (reduction_partners,extension_partners) | f::r -> let (a,b) = f in if List.mem ext_atom [a;b] then let ext_partner = if ext_atom = a then b else a in let (new_red_partners,new_ext_partners) = (* force reduction steps first *) if (AtomSet.mem ext_partner path) then ((AtomSet.add ext_partner reduction_partners),extension_partners) else if (check_alpha_relation ext_partner path atom_sets) then (reduction_partners,(AtomSet.add ext_partner extension_partners)) else (reduction_partners,extension_partners) in ext_partners r path ext_atom (new_red_partners,new_ext_partners) atom_sets else ext_partners r path ext_atom (reduction_partners,extension_partners) atom_sets exception Failed_connections let path_checker atom_rel atom_sets qprefixes init_ordering logic = let con = connections atom_rel [] in (*: print_endline ""; print_endline ("number of connections: "^(string_of_int (List.length con))); mbreak "#connec\n"; :*) let rec provable path closed (orderingQ,reduction_ordering) eqlist (sigmaQ,sigmaJ) = let rec check_connections (reduction_partners,extension_partners) ext_atom = let try_one = if reduction_partners = AtomSet.empty then if extension_partners = AtomSet.empty then raise Failed_connections else AtomSet.choose extension_partners else (* force reduction steps always first!! *) AtomSet.choose reduction_partners in (* print_endline ("connection partner "^(try_one.aname)); *) (* print_endline ("partner path "^(print_set path)); *) (try let (new_sigmaQ,new_ordering_elements) = jqunify (ext_atom.alabel) (try_one.alabel) sigmaQ in (* build the orderingQ incrementally from the new added substitution tau of new_sigmaQ *) let (relate_pairs,new_orderingQ) = build_orderingQ new_ordering_elements orderingQ in (* we make in incremental reflexivity test during the string unification *) let (new_sigmaJ,new_eqlist,new_red_ordering) = (* new_red_ordering = [] in propositional case *) stringunify ext_atom try_one eqlist relate_pairs logic new_orderingQ atom_rel qprefixes in (* print_endline ("make reduction ordering "^((string_of_int (List.length new_ordering)))); *) let new_closed = AtomSet.add ext_atom closed in let ((next_orderingQ,next_red_ordering),next_eqlist,(next_sigmaQ,next_sigmaJ),subproof) = if AtomSet.mem try_one path then provable path new_closed (new_orderingQ,new_red_ordering) new_eqlist (new_sigmaQ,new_sigmaJ) (* always use old first-order ordering for recursion *) else let new_path = AtomSet.add ext_atom path and extension = AtomSet.add try_one AtomSet.empty in let ((norderingQ,nredordering),neqlist,(nsigmaQ,nsigmaJ),p1) = provable new_path extension (new_orderingQ,new_red_ordering) new_eqlist (new_sigmaQ,new_sigmaJ) in let ((nnorderingQ,nnredordering),nneqlist,(nnsigmaQ,nnsigmaJ),p2) = provable path new_closed (norderingQ,nredordering) neqlist (nsigmaQ,nsigmaJ) in ((nnorderingQ,nnredordering),nneqlist,(nnsigmaQ,nnsigmaJ),(p1 @ p2)) (* first the extension subgoals = depth first; then other subgoals in same clause *) in ((next_orderingQ,next_red_ordering),next_eqlist,(next_sigmaQ,next_sigmaJ),(((ext_atom.aname),(try_one.aname))::subproof)) with Failed -> (* print_endline ("new connection for "^(ext_atom.aname)); *) (* print_endline ("Failed"); *) check_connections ((AtomSet.remove try_one reduction_partners), (AtomSet.remove try_one extension_partners) ) ext_atom ) in let rec check_extension extset = if extset = AtomSet.empty then raise Failed (* go directly to a new entry connection *) else let select_one = AtomSet.choose extset in (* print_endline ("extension literal "^(select_one.aname)); *) (* print_endline ("extension path "^(print_set path));*) let (reduction_partners,extension_partners) = ext_partners con path select_one (AtomSet.empty,AtomSet.empty) atom_sets in (try check_connections (reduction_partners,extension_partners) select_one with Failed_connections -> (* print_endline ("no connections for subgoal "^(select_one.aname)); *) (* print_endline ("Failed_connections"); *) let fail_ext_set = fail_ext_set select_one extset atom_sets in check_extension fail_ext_set ) in let extset = extset atom_sets path closed in if extset = AtomSet.empty then ((orderingQ,reduction_ordering),eqlist,(sigmaQ,sigmaJ),[]) else check_extension extset in if qprefixes = ([],[]) then begin (* print_endline "!!!!!!!!!!! prop prover !!!!!!!!!!!!!!!!!!"; *) (* in the propositional case, the reduction ordering will be computed AFTER proof search *) let (_,eqlist,(_,(n,substJ)),ext_proof) = provable AtomSet.empty AtomSet.empty ([],[]) (1,[]) ([],(1,[])) in let orderingJ = build_orderingJ_list substJ init_ordering atom_rel in ((init_ordering,orderingJ),eqlist,([],(n,substJ)),ext_proof) end else provable AtomSet.empty AtomSet.empty (init_ordering,[]) (1,[]) ([],(1,[])) (*************************** prepare and init prover *******************************************************) let rec list_to_set list = match list with [] -> AtomSet.empty | f::r -> let rest_set = list_to_set r in AtomSet.add f rest_set let rec make_atom_sets atom_rel = match atom_rel with [] -> [] | f::r -> let (a,alpha,beta) = f in (a,(list_to_set alpha),(list_to_set beta))::(make_atom_sets r) let rec predecessor address_1 address_2 ftree = match ftree with Empty -> PNull (* should not occur since every pair of atoms have a common predecessor *) | NodeAt(position) -> PNull (* should not occur as above *) | NodeA(position,suctrees) -> match address_1,address_2 with [],_ -> raise (Invalid_argument "Jprover: predecessors left") | _,[] -> raise (Invalid_argument "Jprover: predecessors right") | (f1::r1),(f2::r2) -> if f1 = f2 then predecessor r1 r2 (suctrees.(f1-1)) else position.pt let rec compute_sets element ftree alist = match alist with [] -> [],[] | first::rest -> if first = element then compute_sets element ftree rest (* element is neithes alpha- nor beta-related to itself*) else let (alpha_rest,beta_rest) = compute_sets element ftree rest in if predecessor (element.aaddress) (first.aaddress) ftree = Beta then (alpha_rest,(first::beta_rest)) else ((first::alpha_rest),beta_rest) let rec compute_atomlist_relations worklist ftree alist = (* last version of alist for total comparison *) let rec compute_atom_relations element ftree alist = let alpha_set,beta_set = compute_sets element ftree alist in (element,alpha_set,beta_set) in match worklist with [] -> [] | first::rest -> let first_relations = compute_atom_relations first ftree alist in first_relations::(compute_atomlist_relations rest ftree alist) let atom_record position prefix = let aname = (position.name) in let aprefix = (List.append prefix [aname]) in (* atom position is last element in prefix *) let aop = (dest_term position.label).term_op in ({aname=aname; aaddress=(position.address); aprefix=aprefix; apredicate=aop; apol=(position.pol); ast=(position.st); alabel=(position.label)}) let rec select_atoms_treelist treelist prefix = let rec select_atoms ftree prefix = match ftree with Empty -> [],[],[] | NodeAt(position) -> [(atom_record position prefix)],[],[] | NodeA(position,suctrees) -> let treelist = Array.to_list suctrees in let new_prefix = let prefix_element = if List.mem (position.st) [Psi_0;Phi_0] then [(position.name)] else [] in (List.append prefix prefix_element) in let (gamma_0_element,delta_0_element) = if position.st = Gamma_0 then begin (* Format.open_box 0; print_endline "gamma_0 prefixes "; print_string (position.name^" :"); print_stringlist prefix; print_endline " "; Format.force_newline (); Format.print_flush (); *) [(position.name,prefix)],[] end else if position.st = Delta_0 then begin (* Format.open_box 0; print_endline "delta_0 prefixes "; print_string (position.name^" :"); print_stringlist prefix; print_endline " "; Format.force_newline (); Format.print_flush (); *) [],[(position.name,prefix)] end else [],[] in let (rest_alist,rest_gamma_0_prefixes,rest_delta_0_prefixes) = select_atoms_treelist treelist new_prefix in (rest_alist,(rest_gamma_0_prefixes @ gamma_0_element), (rest_delta_0_prefixes @ delta_0_element)) in match treelist with [] -> [],[],[] | first::rest -> let (first_alist,first_gprefixes,first_dprefixes) = select_atoms first prefix and (rest_alist,rest_gprefixes,rest_dprefixes) = select_atoms_treelist rest prefix in ((first_alist @ rest_alist),(first_gprefixes @ rest_gprefixes), (first_dprefixes @ rest_dprefixes)) let prepare_prover ftree = let alist,gamma_0_prefixes,delta_0_prefixes = select_atoms_treelist [ftree] [] in let atom_rel = compute_atomlist_relations alist ftree alist in (atom_rel,(gamma_0_prefixes,delta_0_prefixes)) (* ************************ Build intial formula tree and relations *********************************** *) (* Building a formula tree and the tree ordering from the input formula, i.e. OCaml term *) let make_position_name stype pos_n = let prefix = if List.mem stype [Phi_0;Gamma_0] then "v" else if List.mem stype [Psi_0;Delta_0] then "c" else "a" in prefix^(string_of_int pos_n) let dual_pol pol = if pol = O then I else O let check_subst_term (variable,old_term) pos_name stype = if (List.mem stype [Gamma_0;Delta_0]) then let new_variable = if stype = Gamma_0 then (mk_var_term (pos_name^"_jprover")) else (mk_string_term jprover_op pos_name) in (subst1 old_term variable new_variable) (* replace variable (non-empty) in t by pos_name *) (* pos_name is either a variable term or a constant, f.i. a string term *) (* !!! check unification module how handling eingenvariables as constants !!! *) else old_term let rec build_ftree (variable,old_term) pol stype address pos_n = let pos_name = make_position_name stype pos_n in let term = check_subst_term (variable,old_term) pos_name stype in if JLogic.is_and_term term then let s,t = JLogic.dest_and term in let ptype,stype_1,stype_2 = if pol = O then Beta,Beta_1,Beta_2 else Alpha,Alpha_1,Alpha_2 in let position = {name=pos_name; address=address; op=And; pol=pol; pt=ptype; st=stype; label=term} in let subtree_left,ordering_left,posn_left = build_ftree ("",s) pol stype_1 (address@[1]) (pos_n+1) in let subtree_right,ordering_right,posn_right = build_ftree ("",t) pol stype_2 (address@[2]) (posn_left+1) in let (succ_left,whole_left) = List.hd ordering_left and (succ_right,whole_right) = List.hd ordering_right in let pos_succs = (StringSet.add succ_left (StringSet.add succ_right (StringSet.union whole_left whole_right))) in (NodeA(position,[|subtree_left;subtree_right|]), ((position.name,pos_succs)::(ordering_left @ ordering_right)), posn_right ) else if JLogic.is_or_term term then let s,t = JLogic.dest_or term in let ptype,stype_1,stype_2 = if pol = O then Alpha,Alpha_1,Alpha_2 else Beta,Beta_1,Beta_2 in let position = {name=pos_name; address=address; op=Or; pol=pol; pt=ptype; st=stype; label=term} in let subtree_left,ordering_left,posn_left = build_ftree ("",s) pol stype_1 (address@[1]) (pos_n+1) in let subtree_right,ordering_right,posn_right = build_ftree ("",t) pol stype_2 (address@[2]) (posn_left+1) in let (succ_left,whole_left) = List.hd ordering_left and (succ_right,whole_right) = List.hd ordering_right in let pos_succs = StringSet.add succ_left (StringSet.add succ_right (StringSet.union whole_left whole_right)) in (NodeA(position,[|subtree_left;subtree_right|]), ((position.name),pos_succs) :: (ordering_left @ ordering_right), posn_right ) else if JLogic.is_implies_term term then let s,t = JLogic.dest_implies term in let ptype_0,stype_0,ptype,stype_1,stype_2 = if pol = O then Psi,Psi_0,Alpha,Alpha_1,Alpha_2 else Phi,Phi_0,Beta,Beta_1,Beta_2 in let pos2_name = make_position_name stype_0 (pos_n+1) in let sposition = {name=pos_name; address=address; op=Imp; pol=pol; pt=ptype_0; st=stype; label=term} and position = {name=pos2_name; address=address@[1]; op=Imp; pol=pol; pt=ptype; st=stype_0; label=term} in let subtree_left,ordering_left,posn_left = build_ftree ("",s) (dual_pol pol) stype_1 (address@[1;1]) (pos_n+2) in let subtree_right,ordering_right,posn_right = build_ftree ("",t) pol stype_2 (address@[1;2]) (posn_left+1) in let (succ_left,whole_left) = List.hd ordering_left and (succ_right,whole_right) = List.hd ordering_right in let pos_succs = StringSet.add succ_left (StringSet.add succ_right (StringSet.union whole_left whole_right)) in let pos_ordering = (position.name,pos_succs) :: (ordering_left @ ordering_right) in (NodeA(sposition,[|NodeA(position,[|subtree_left;subtree_right|])|]), ((sposition.name,(StringSet.add position.name pos_succs))::pos_ordering), posn_right ) else if JLogic.is_not_term term then let s = JLogic.dest_not term in let ptype_0,stype_0,ptype,stype_1= if pol = O then Psi,Psi_0,Alpha,Alpha_1 else Phi,Phi_0,Alpha,Alpha_1 in let pos2_name = make_position_name stype_0 (pos_n+1) in let sposition = {name=pos_name; address=address; op=Neg; pol=pol; pt=ptype_0; st=stype; label=term} and position = {name=pos2_name; address=address@[1]; op=Neg; pol=pol; pt=ptype; st=stype_0; label=term} in let subtree_left,ordering_left,posn_left = build_ftree ("",s) (dual_pol pol) stype_1 (address@[1;1]) (pos_n+2) in let (succ_left,whole_left) = List.hd ordering_left in let pos_succs = StringSet.add succ_left whole_left in let pos_ordering = (position.name,pos_succs) :: ordering_left in (NodeA(sposition,[|NodeA(position,[| subtree_left|])|]), ((sposition.name,(StringSet.add position.name pos_succs))::pos_ordering), posn_left ) else if JLogic.is_exists_term term then let v,s,t = JLogic.dest_exists term in (* s is type of v and will be supressed here *) let ptype,stype_1 = if pol = O then Gamma,Gamma_0 else Delta,Delta_0 in let position = {name=pos_name; address=address; op=Ex; pol=pol; pt=ptype; st=stype; label=term} in let subtree_left,ordering_left,posn_left = build_ftree (v,t) pol stype_1 (address@[1]) (pos_n+1) in let (succ_left,whole_left) = List.hd ordering_left in let pos_succs = StringSet.add succ_left whole_left in (NodeA(position,[|subtree_left|]), ((position.name,pos_succs) :: ordering_left), posn_left ) else if JLogic.is_all_term term then let v,s,t = JLogic.dest_all term in (* s is type of v and will be supressed here *) let ptype_0,stype_0,ptype,stype_1= if pol = O then Psi,Psi_0,Delta,Delta_0 else Phi,Phi_0,Gamma,Gamma_0 in let pos2_name = make_position_name stype_0 (pos_n+1) in let sposition = {name=pos_name; address=address; op=All; pol=pol; pt=ptype_0; st=stype; label=term} and position = {name=pos2_name; address=address@[1]; op=All; pol=pol; pt=ptype; st=stype_0; label=term} in let subtree_left,ordering_left,posn_left = build_ftree (v,t) pol stype_1 (address@[1;1]) (pos_n+2) in let (succ_left,whole_left) = List.hd ordering_left in let pos_succs = StringSet.add succ_left whole_left in let pos_ordering = (position.name,pos_succs) :: ordering_left in (NodeA(sposition,[|NodeA(position,[|subtree_left|])|]), ((sposition.name,(StringSet.add position.name pos_succs))::pos_ordering), posn_left ) else (* finally, term is atomic *) let ptype_0,stype_0 = if pol = O then Psi,Psi_0 else Phi,Phi_0 in let pos2_name = make_position_name stype_0 (pos_n+1) in let sposition = {name=pos_name; address=address; op=At; pol=pol; pt=ptype_0; st=stype; label=term} and position = {name=pos2_name; address=address@[1]; op=At; pol=pol; pt=PNull; st=stype_0; label=term} in (NodeA(sposition,[|NodeAt(position)|]), [(sposition.name,(StringSet.add position.name StringSet.empty));(position.name,StringSet.empty)], pos_n+1 ) let rec construct_ftree termlist treelist orderinglist pos_n goal = match termlist with [] -> let new_root = {name="w"; address=[]; op=Null; pol=O; pt=Psi; st=PNull_0; label=goal} and treearray = Array.of_list treelist in NodeA(new_root,treearray),(("w",(union_orderings orderinglist))::orderinglist),pos_n | ft::rest_terms -> let next_address = [((List.length treelist)+1)] and next_pol,next_goal = if rest_terms = [] then O,ft (* construct tree for the conclusion *) else I,goal in let new_tree,new_ordering,new_pos_n = build_ftree ("",ft) next_pol Alpha_1 next_address (pos_n+1) in construct_ftree rest_terms (treelist @ [new_tree]) (orderinglist @ new_ordering) new_pos_n next_goal (*************************** Main LOOP ************************************) let unprovable = RefineError ("Jprover", StringError "formula is not provable") let mult_limit_exn = RefineError ("Jprover", StringError "multiplicity limit reached") let coq_exn = RefineError ("Jprover", StringError "interface for coq: error on ") let init_prover ftree = let atom_relation,qprefixes = prepare_prover ftree in (* print_atom_info atom_relation; *) (* apple *) let atom_sets = make_atom_sets atom_relation in (atom_relation,atom_sets,qprefixes) let rec try_multiplicity mult_limit ftree ordering pos_n mult logic = try let (atom_relation,atom_sets,qprefixes) = init_prover ftree in let ((orderingQ,red_ordering),eqlist,unifier,ext_proof) = path_checker atom_relation atom_sets qprefixes ordering logic in (ftree,red_ordering,eqlist,unifier,ext_proof) (* orderingQ is not needed as return value *) with Failed -> match mult_limit with Some m when m == mult -> raise mult_limit_exn | _ -> let new_mult = mult+1 in begin Pp.msgnl (Pp.(++) (Pp.str "Multiplicity Fail: Trying new multiplicity ") (Pp.int new_mult)); (* Format.open_box 0; Format.force_newline (); Format.print_string "Multiplicity Fail: "; Format.print_string ("Try new multiplicity "^(string_of_int new_mult)); Format.force_newline (); Format.print_flush (); *) let (new_ftree,new_ordering,new_pos_n) = add_multiplicity ftree pos_n new_mult logic in if (new_ftree = ftree) then raise unprovable else (* print_formula_info new_ftree new_ordering new_pos_n; *) (* apple *) try_multiplicity mult_limit new_ftree new_ordering new_pos_n new_mult logic end let prove mult_limit termlist logic = let (ftree,ordering,pos_n) = construct_ftree termlist [] [] 0 (mk_var_term "dummy") in (* pos_n = number of positions without new root "w" *) (* print_formula_info ftree ordering pos_n; *) (* apple *) try_multiplicity mult_limit ftree ordering pos_n 1 logic (********** first-order type theory interface *******************) let rec renam_free_vars termlist = match termlist with [] -> [],[] | f::r -> let var_names = free_vars_list f in let string_terms = List.map (fun x -> (mk_string_term free_var_op x)) var_names in let mapping = List.combine var_names string_terms and new_f = subst f var_names string_terms in let (rest_mapping,rest_renamed) = renam_free_vars r in let unique_mapping = remove_dups_list (mapping @ rest_mapping) in (unique_mapping,(new_f::rest_renamed)) let rec apply_var_subst term var_subst_list = match var_subst_list with [] -> term | (v,t)::r -> let next_term = var_subst term t v in apply_var_subst next_term r let rec make_equal_list n list_object = if n = 0 then [] else list_object::(make_equal_list (n-1) list_object) let rec create_output rule_list input_map = match rule_list with [] -> JLogic.empty_inf | f::r -> let (pos,(rule,term1,term2)) = f in let delta1_names = collect_delta_terms [term1] and delta2_names = collect_delta_terms [term2] in let unique_deltas = remove_dups_list (delta1_names @ delta2_names) in let delta_terms = List.map (fun x -> (mk_string_term jprover_op x)) unique_deltas in let delta_vars = List.map (fun x -> (x^"_jprover")) unique_deltas in let delta_map = List.combine delta_vars delta_terms in let var_mapping = (input_map @ delta_map) in let frees1 = free_vars_list term1 and frees2 = free_vars_list term2 in let unique_object = mk_var_term "v0_jprover" in let unique_list1 = make_equal_list (List.length frees1) unique_object and unique_list2 = make_equal_list (List.length frees2) unique_object in let next_term1 = subst term1 frees1 unique_list1 and next_term2 = subst term2 frees2 unique_list2 in let new_term1 = apply_var_subst next_term1 var_mapping and new_term2 = apply_var_subst next_term2 var_mapping and (a,b) = pos in (*: print_string (a^"+++"^b^"\n"); :*) (* kick away the first argument, the position *) (JLogic.append_inf (create_output r input_map) (b,new_term1) (a,new_term2) rule) let rec make_test_interface rule_list input_map = match rule_list with [] -> [] | f::r -> let (pos,(rule,term1,term2)) = f in let delta1_names = collect_delta_terms [term1] and delta2_names = collect_delta_terms [term2] in let unique_deltas = remove_dups_list (delta1_names @ delta2_names) in let delta_terms = List.map (fun x -> (mk_string_term jprover_op x)) unique_deltas in let delta_vars = List.map (fun x -> (x^"_jprover")) unique_deltas in let delta_map = List.combine delta_vars delta_terms in let var_mapping = (input_map @ delta_map) in let frees1 = free_vars_list term1 and frees2 = free_vars_list term2 in let unique_object = mk_var_term "v0_jprover" in let unique_list1 = make_equal_list (List.length frees1) unique_object and unique_list2 = make_equal_list (List.length frees2) unique_object in begin (* print_endline ""; print_endline ""; print_stringlist frees1; print_endline ""; print_stringlist frees2; print_endline ""; print_endline ""; *) let next_term1 = subst term1 frees1 unique_list1 and next_term2 = subst term2 frees2 unique_list2 in let new_term1 = apply_var_subst next_term1 var_mapping and new_term2 = apply_var_subst next_term2 var_mapping in (pos,(rule,new_term1,new_term2))::(make_test_interface r input_map) end (**************************************************************) (*: modified for Coq :*) let decomp_pos pos = let {name=n; address=a; label=l} = pos in (n,(a,l)) let rec build_formula_id ftree = let rec build_fid_list = function [] -> [] | t::rest -> (build_formula_id t)@(build_fid_list rest) in match ftree with Empty -> [] | NodeAt(position) -> [decomp_pos position] | NodeA(position,subtrees) -> let tree_list = Array.to_list subtrees in (decomp_pos position)::(build_fid_list tree_list) let rec encode1 = function (* normal *) [] -> "" | i::r -> "_"^(string_of_int i)^(encode1 r) let rec encode2 = function (* move up *) [i] -> "" | i::r -> "_"^(string_of_int i)^(encode2 r) | _ -> raise coq_exn let rec encode3 = function (* move down *) [] -> "_1" | i::r -> "_"^(string_of_int i)^(encode3 r) let lookup_coq str map = try let (il,t) = List.assoc str map in il with Not_found -> raise coq_exn let create_coq_input inf map = let rec rec_coq_part inf = match inf with [] -> [] | (rule, (s1, t1), ((s2, t2) as k))::r -> begin match rule with Andl | Andr | Orl | Orr1 | Orr2 -> (rule, (encode1 (lookup_coq s1 map), t1), k)::(rec_coq_part r) | Impr | Impl | Negr | Negl | Ax -> (rule, (encode2 (lookup_coq s1 map), t1), k)::(rec_coq_part r) | Exr -> (rule, (encode1 (lookup_coq s1 map), t1), (encode1 (lookup_coq s2 map), t2))::(rec_coq_part r) | Exl -> (rule, (encode1 (lookup_coq s1 map), t1), (encode3 (lookup_coq s1 map), t2))::(rec_coq_part r) | Allr | Alll -> (rule, (encode2 (lookup_coq s1 map), t1), (* (s2, t2))::(rec_coq_part r) *) (encode3 (lookup_coq s1 map), t2))::(rec_coq_part r) | _ -> raise coq_exn end in rec_coq_part inf let gen_prover mult_limit logic calculus hyps concls = let (input_map,renamed_termlist) = renam_free_vars (hyps @ concls) in let (ftree,red_ordering,eqlist,(sigmaQ,sigmaJ),ext_proof) = prove mult_limit renamed_termlist logic in let sequent_proof = reconstruct ftree red_ordering sigmaQ ext_proof logic calculus in let (ptree,count_ax) = bproof sequent_proof in let idl = build_formula_id ftree in (* print_ftree ftree; apple *) (* transform types and rename constants *) (* we can transform the eigenvariables AFTER proof reconstruction since *) (* new delta_0 constants may have been constructed during rule permutation *) (* from the LJmc to the LJ proof *) create_coq_input (create_output sequent_proof input_map) idl (*: end of coq modification :*) let prover mult_limit hyps concl = gen_prover mult_limit "J" "LJ" hyps [concl] (************* test with propositional proof reconstruction ************) let rec count_axioms seq_list = match seq_list with [] -> 0 | f::r -> let (rule,_,_) = f in if rule = Ax then 1 + count_axioms r else count_axioms r let do_prove mult_limit termlist logic calculus = try begin let (input_map,renamed_termlist) = renam_free_vars termlist in let (ftree,red_ordering,eqlist,(sigmaQ,sigmaJ),ext_proof) = prove mult_limit renamed_termlist logic in Format.open_box 0; Format.force_newline (); Format.force_newline (); Format.print_string "Extension proof ready"; Format.force_newline (); Format.force_newline (); Format.print_string ("Length of Extension proof: "^((string_of_int (List.length ext_proof)))^ " Axioms"); Format.force_newline (); Format.force_newline (); print_endline "Extension proof:"; Format.open_box 0; print_pairlist ext_proof; (* print list of type (string * string) list *) Format.force_newline (); Format.force_newline (); Format.force_newline (); Format.print_flush (); Format.print_flush (); Format.open_box 0; print_ordering red_ordering; Format.print_flush (); Format.open_box 0; Format.force_newline (); (* ----------------------------------------------- *) Format.open_box 0; print_tunify sigmaJ; Format.print_flush (); print_endline ""; print_endline ""; print_sigmaQ sigmaQ; print_endline ""; print_endline ""; Format.open_box 0; let (qmax,equations) = eqlist in print_endline ("number of quantifier domains : "^(string_of_int (qmax-1))); print_endline ""; print_equations equations; Format.print_flush (); print_endline ""; print_endline ""; print_endline ("Length of equations : "^((string_of_int (List.length equations)))); print_endline ""; print_endline ""; (* --------------------------------------------------------- *) Format.print_string "Break ... "; print_endline ""; print_endline ""; Format.print_flush (); (*: let _ = input_char stdin in :*) let reconstr_proof = reconstruct ftree red_ordering sigmaQ ext_proof logic calculus in let sequent_proof = make_test_interface reconstr_proof input_map in Format.open_box 0; Format.force_newline (); Format.force_newline (); Format.print_string "Sequent proof ready"; Format.force_newline (); Format.force_newline (); Format.print_flush (); let (ptree,count_ax) = bproof sequent_proof in Format.open_box 0; Format.print_string ("Length of sequent proof: "^((string_of_int count_ax))^" Axioms"); Format.force_newline (); Format.force_newline (); Format.force_newline (); Format.force_newline (); Format.print_flush (); tt ptree; (*: print proof tree :*) Format.print_flush (); print_endline ""; print_endline "" end with exn -> begin print_endline "Jprover got an exception:"; print_endline (Printexc.to_string exn) end let test concl logic calculus = (* calculus should be LJmc or LJ for J, and LK for C *) do_prove None [concl] logic calculus (* for sequents *) let seqtest list_term logic calculus = let bterms = (dest_term list_term).term_terms in let termlist = collect_subterms bterms in do_prove None termlist logic calculus (*****************************************************************) end (* of struct *)