--- 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 =
--- 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;
*)
--- 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