# HG changeset patch # User paulson # Date 1121871628 -7200 # Node ID 7e5319d0f41854242fc2c4e3bff44a68b64a74d7 # Parent db2defb39f4c380fbd2fd3f924e25de66eec6013 code streamlining diff -r db2defb39f4c -r 7e5319d0f418 src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Wed Jul 20 15:57:10 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Wed Jul 20 17:00:28 2005 +0200 @@ -185,7 +185,6 @@ ReduceAxiomsN.relevant_filter (!relevant) goal (ResAxioms.claset_rules_of_thy thy); val named_claset = List.filter has_name_pair claset_rules; - val claset_names = map remove_spaces_pair (named_claset) val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []); val simpset_rules = diff -r db2defb39f4c -r 7e5319d0f418 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Wed Jul 20 15:57:10 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Wed Jul 20 17:00:28 2005 +0200 @@ -71,11 +71,14 @@ (**** for Isabelle/ML interface ****) -fun is_proof_char ch = - (33 <= ord ch andalso ord ch <= 126 andalso ord ch <> 63) - orelse ch = " "; +(*Remove unwanted characters such as ? and newline from the textural + representation of a theorem (surely they don't need to be produced in + the first place?) *) -val proofstring = List.filter is_proof_char o explode; +fun is_proof_char ch = (#" " <= ch andalso ch <= #"~" andalso ch <> #"?"); + +val proofstring = + String.translate (fn c => if is_proof_char c then str c else ""); (* @@ -174,41 +177,31 @@ val clasimpfile = (File.platform_path clasimp_file) fun make_atp_list [] sign n = [] - | make_atp_list ((sko_thm, sg_term)::xs) sign n = + | make_atp_list ((sko_thm, sg_term)::xs) sign n = let - val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) - val thmproofstr = proofstring ( skothmstr) - val no_returns = filter_out (equal "\n") thmproofstr - val thmstr = implode no_returns - val _ = warning ("thmstring in make_atp_lists is: "^thmstr) + val thmstr = proofstring (Meson.concat_with_and (map string_of_thm sko_thm)) + val _ = warning ("thmstring in make_atp_lists is " ^ thmstr) - val sgstr = Sign.string_of_term sign sg_term - val goalproofstring = proofstring sgstr - val no_returns = filter_out (equal "\n") goalproofstring - val goalstring = implode no_returns - val _ = warning ("goalstring in make_atp_lists is: "^goalstring) + val goalstring = proofstring (Sign.string_of_term sign sg_term) + val _ = warning ("goalstring in make_atp_lists is " ^ goalstring) - val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) - - val _ = (warning ("prob file in cal_res_tac is: "^probfile)) + val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n) + val _ = warning ("prob file in call_resolve_tac is " ^ probfile) in if !SpassComm.spass then - let val _ = ResLib.helper_path "SPASS_HOME" "SPASS" - in (*We've checked that SPASS is there for ATP/spassshell to run.*) - if !full_spass - then (*Allow SPASS to run in Auto mode, using all its inference rules*) - ([("spass", thmstr, goalstring (*,spass_home*), - - getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*), - "-DocProof%-TimeLimit=60%-SOS", - - clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) - else (*Restrict SPASS to a small set of rules that we can parse*) - ([("spass", thmstr, goalstring (*,spass_home*), - getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*), - ("-" ^ space_implode "%-" (!custom_spass)), - clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) + let val optionline = (*Custom SPASS options, or default?*) + if !full_spass (*Auto mode: all SPASS inference rules*) + then "-DocProof%-TimeLimit=60%-SOS" + else "-" ^ space_implode "%-" (!custom_spass) + val _ = warning ("SPASS option string is " ^ optionline) + val _ = ResLib.helper_path "SPASS_HOME" "SPASS" + (*We've checked that SPASS is there for ATP/spassshell to run.*) + in + ([("spass", thmstr, goalstring, + getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell", + optionline, clasimpfile, axfile, hypsfile, probfile)] @ + (make_atp_list xs sign (n+1))) end else let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel" @@ -219,8 +212,7 @@ end end - val thms_goals = ListPair.zip( thms, sg_terms) - val atp_list = make_atp_list thms_goals sign 1 + val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1 in Watcher.callResProvers(childout,atp_list); warning "Sent commands to watcher!"; @@ -356,7 +348,7 @@ val ax_file = File.platform_path axiom_file val out = TextIO.openOut ax_file in - (ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out) + (ResLib.writeln_strs out clauses_strs; (warning ("axiom file is "^ax_file));TextIO.closeOut out) end; *) diff -r db2defb39f4c -r 7e5319d0f418 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Wed Jul 20 15:57:10 2005 +0200 +++ b/src/HOL/Tools/res_axioms.ML Wed Jul 20 17:00:28 2005 +0200 @@ -16,11 +16,6 @@ val meta_cnf_axiom : thm -> thm list val cnf_rule : thm -> thm list val cnf_rules : (string*thm) list -> thm list -> thm list list * thm list - - val cnf_classical_rules_thy : theory -> thm list list * thm list - - val cnf_simpset_rules_thy : theory -> thm list list * thm list - val rm_Eps : (term * term) list -> thm list -> term list val claset_rules_of_thy : theory -> (string * thm) list val simpset_rules_of_thy : theory -> (string * thm) list @@ -378,14 +373,6 @@ let val (ts,es) = cnf_rules thms err_list in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end; -(* CNF all rules from a given theory's classical reasoner *) -fun cnf_classical_rules_thy thy = - cnf_rules (claset_rules_of_thy thy) []; - -(* CNF all simplifier rules from a given theory's simpset *) -fun cnf_simpset_rules_thy thy = - cnf_rules (simpset_rules_of_thy thy) []; - (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****) @@ -395,18 +382,20 @@ val isa_clauses' = rm_Eps [] isa_clauses val clauses_n = length isa_clauses fun make_axiom_clauses _ [] []= [] - | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls') :: make_axiom_clauses (i+1) clss clss' + | make_axiom_clauses i (cls::clss) (cls'::clss') = + (ResClause.make_axiom_clause cls (thm_name,i), cls') :: + make_axiom_clauses (i+1) clss clss' in make_axiom_clauses 0 isa_clauses' isa_clauses end; fun clausify_rules_pairs [] err_list = ([],err_list) | clausify_rules_pairs ((name,thm)::thms) err_list = - let val (ts,es) = clausify_rules_pairs thms err_list - in - ((clausify_axiom_pairs (name,thm))::ts,es) handle _ => (ts,(thm::es)) - end; -(* classical rules *) + let val (ts,es) = clausify_rules_pairs thms err_list + in + ((clausify_axiom_pairs (name,thm))::ts, es) + handle _ => (ts, (thm::es)) + end; (*Setup function: takes a theory and installs ALL simprules and claset rules