--- a/etc/settings Wed Oct 19 21:53:34 2005 +0200
+++ b/etc/settings Fri Oct 21 02:57:22 2005 +0200
@@ -87,6 +87,10 @@
# The place for user configuration, heap files, etc.
ISABELLE_HOME_USER=~/isabelle
+# The places for external proversetc.
+#VAMPIRE_HOME=~/Vampire
+#E_HOME=~/E
+
# Where to look for isabelle tools (multiple dirs separated by ':').
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
--- a/src/HOL/IsaMakefile Wed Oct 19 21:53:34 2005 +0200
+++ b/src/HOL/IsaMakefile Fri Oct 21 02:57:22 2005 +0200
@@ -113,8 +113,7 @@
Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy \
Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy \
antisym_setup.ML arith_data.ML blastdata.ML cladata.ML \
- document/root.tex eqrule_HOL_data.ML hologic.ML simpdata.ML \
- ResAtpOracle.thy \
+ document/root.tex eqrule_HOL_data.ML hologic.ML simpdata.ML \
ResAtpMethods.thy \
Tools/res_atp_setup.ML Tools/res_atp_provers.ML Tools/res_atp_methods.ML
@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
--- a/src/HOL/ResAtpMethods.thy Wed Oct 19 21:53:34 2005 +0200
+++ b/src/HOL/ResAtpMethods.thy Fri Oct 21 02:57:22 2005 +0200
@@ -5,12 +5,22 @@
*)
theory ResAtpMethods
- imports Reconstruction ResAtpOracle
+ imports Reconstruction
- uses "Tools/res_atp_setup.ML"
- "Tools/res_atp_methods.ML"
+uses ("Tools/res_atp_setup.ML")
+ ("Tools/res_atp_provers.ML")
+ ("Tools/res_atp_methods.ML")
begin
-setup ResAtpMethods.ResAtps_setup
+
+ML{*use "Tools/res_atp_setup.ML"*}
+ML{*use "Tools/res_atp_provers.ML"*}
+oracle vampire_oracle ("string list * int") = {*ResAtpProvers.vampire_o*}
+oracle eprover_oracle ("string list * int") = {*ResAtpProvers.eprover_o*}
+
+
+ML{*use "Tools/res_atp_methods.ML"*}
+
+setup ResAtpMethods.ResAtps_setup
end
--- a/src/HOL/ResAtpOracle.thy Wed Oct 19 21:53:34 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* ID: $Id$
- Author: Jia Meng, NICTA
-
-setup vampire prover as an oracle
-setup E prover as an oracle
-*)
-
-theory ResAtpOracle
- imports HOL
-uses "Tools/res_atp_setup.ML"
- "Tools/res_atp_provers.ML"
-
-begin
-
-
-
-
-oracle vampire_oracle ("string list * int") = {*ResAtpProvers.vampire_o
-*}
-
-
-
-
-oracle eprover_oracle ("string list * int") = {*ResAtpProvers.eprover_o
- *}
-
-
-end
--- a/src/HOL/Tools/res_atp_setup.ML Wed Oct 19 21:53:34 2005 +0200
+++ b/src/HOL/Tools/res_atp_setup.ML Fri Oct 21 02:57:22 2005 +0200
@@ -15,16 +15,6 @@
| writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
-fun no_rep_add x [] = [x]
- | no_rep_add x (y::z) = if x=y then y::z else y::(no_rep_add x z);
-
-fun no_rep_app l1 [] = l1
- | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y;
-
-
-fun flat_noDup [] = []
- | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
-
fun warning_thm thm nm = warning (nm ^ " " ^ (string_of_thm thm));
fun warning_thms_n n thms nm =
@@ -114,7 +104,7 @@
fun tptp_form thms n tfrees =
let val clss = ResClause.make_conjecture_clauses (map prop_of thms)
val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
- val tfree_clss = map ResClause.tfree_clause ((flat_noDup tfree_litss) \\ tfrees)
+ val tfree_clss = map ResClause.tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees)
val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
val out = TextIO.openOut(probfile)
in
@@ -134,7 +124,7 @@
val prems''' = ResAxioms.rm_Eps [] prems''
val clss = ResClause.make_conjecture_clauses prems'''
val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
- val tfree_lits = flat_noDup tfree_litss
+ val tfree_lits = ResClause.union_all tfree_litss
val tfree_clss = map ResClause.tfree_clause tfree_lits
val hypsfile = File.platform_path hyps_file
val out = TextIO.openOut(hypsfile)
@@ -163,7 +153,7 @@
fun write_rules [] file = [](* no rules, then no need to write anything, thus no clasimp file *)
| write_rules rules file =
let val out = TextIO.openOut(file)
- val clss = flat_noDup(ResAxioms.clausify_rules_pairs rules)
+ val clss = ResClause.union_all(ResAxioms.clausify_rules_pairs rules)
val (clss',names) = ListPair.unzip clss
val (tptpclss,_) = ListPair.unzip(map ResClause.clause2tptp clss')
in
@@ -202,12 +192,14 @@
(* setup ATPs as Isabelle methods *)
(***************************************************************)
fun atp_meth' tac prems ctxt =
- let val rules = if !filter_ax then (find_relevant_ax ctxt) else (tptp_cnf_clasimp ctxt (!include_claset, !include_simpset))
+ let val rules = if !filter_ax then find_relevant_ax ctxt
+ else tptp_cnf_clasimp ctxt (!include_claset, !include_simpset)
val (hyps,tfrees) = tptp_hyps (ProofContext.prems_of ctxt)
val files = hyps @ rules
in
Method.METHOD (fn facts =>
- if !debug then ((warning_thms_n (length facts) facts "facts");HEADGOAL (tac ctxt files tfrees)) else (HEADGOAL (tac ctxt files tfrees)))
+ if !debug then (warning_thms_n (length facts) facts "facts";HEADGOAL (tac ctxt files tfrees))
+ else HEADGOAL (tac ctxt files tfrees))
end;
@@ -228,7 +220,9 @@
| rm_tmp_files1 (f::fs) =
(OS.FileSys.remove f; rm_tmp_files1 fs);
-fun cond_rm_tmp files = (if (!keep_atp_input) then (warning "ATP input kept...") else (warning "deleting ATP inputs..."; rm_tmp_files1 files));
+fun cond_rm_tmp files =
+ if !keep_atp_input then warning "ATP input kept..."
+ else (warning "deleting ATP inputs..."; rm_tmp_files1 files);
end