--- a/src/HOL/TPTP/MaSh_Export.thy Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy Thu Jul 26 10:48:03 2012 +0200
@@ -23,9 +23,10 @@
val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
val prover = hd provers
*}
+
ML {*
if do_it then
- generate_accessibility thy false "/tmp/mash_accessibility"
+ generate_accessibility @{context} thy false "/tmp/mash_accessibility"
else
()
*}
@@ -39,7 +40,7 @@
ML {*
if do_it then
- generate_isar_dependencies thy false "/tmp/mash_dependencies"
+ generate_isar_dependencies @{context} thy false "/tmp/mash_dependencies"
else
()
*}
--- a/src/HOL/TPTP/mash_export.ML Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML Thu Jul 26 10:48:03 2012 +0200
@@ -37,6 +37,12 @@
fun has_thy thy th =
Context.theory_name thy = Context.theory_name (theory_of_thm th)
+fun all_non_technical_facts ctxt thy =
+ let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
+ all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
+ |> filter_out (is_thm_technical o snd)
+ end
+
fun parent_facts thy thy_map =
let
fun add_last thy =
@@ -65,9 +71,8 @@
val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n"
val _ = File.append path s
in [fact] end
- val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val thy_map =
- all_facts ctxt false Symtab.empty [] [] css
+ all_non_technical_facts ctxt thy
|> not include_thy ? filter_out (has_thy thy o snd)
|> thy_map_from_facts
fun do_thy facts =
@@ -81,9 +86,8 @@
let
val path = file_name |> Path.explode
val _ = File.write path ""
- val css = clasimpset_rule_table_of ctxt
val facts =
- all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
+ all_non_technical_facts ctxt thy
|> not include_thy ? filter_out (has_thy thy o snd)
fun do_fact ((_, stature), th) =
let
@@ -98,9 +102,8 @@
let
val path = file_name |> Path.explode
val _ = File.write path ""
- val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val ths =
- all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
+ all_non_technical_facts ctxt thy
|> not include_thy ? filter_out (has_thy thy o snd)
|> map snd
val all_names = all_names ths
@@ -118,9 +121,8 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val prover = hd provers
- val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val facts =
- all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
+ all_non_technical_facts ctxt thy
|> not include_thy ? filter_out (has_thy thy o snd)
val ths = facts |> map snd
val all_names = all_names ths
@@ -137,9 +139,7 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val prover = hd provers
- val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
- val facts =
- all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
+ val facts = all_non_technical_facts ctxt thy
val (new_facts, old_facts) =
facts |> List.partition (has_thy thy o snd)
|>> sort (thm_ord o pairself snd)
@@ -168,9 +168,7 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val prover = hd provers
- val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
- val facts =
- all_facts (Proof_Context.init_global thy) false Symtab.empty [] [] css
+ val facts = all_non_technical_facts ctxt thy
val (new_facts, old_facts) =
facts |> List.partition (has_thy thy o snd)
|>> sort (thm_ord o pairself snd)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jul 26 10:48:03 2012 +0200
@@ -45,6 +45,7 @@
val atp_dependencies_of :
Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
-> thm -> string list option
+ val is_thm_technical : thm -> bool
val mash_CLEAR : Proof.context -> unit
val mash_ADD :
Proof.context -> bool
@@ -399,6 +400,14 @@
| _ => NONE
end
+val technical_theories =
+ ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick",
+ "New_DSequence", "New_Random_Sequence", "Quickcheck",
+ "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"]
+
+val is_thm_technical =
+ member (op =) technical_theories o Context.theory_name o theory_of_thm
+
(*** Low-level communication with MaSh ***)
@@ -700,14 +709,6 @@
(true, "")
end)
-val evil_theories =
- ["Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Nitpick",
- "New_DSequence", "New_Random_Sequence", "Quickcheck",
- "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence", "SMT"]
-
-fun fact_has_evil_theory (_, th) =
- member (op =) evil_theories (Context.theory_name (theory_of_thm th))
-
fun sendback sub =
Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
@@ -722,7 +723,7 @@
Time.+ (Timer.checkRealTimer timer, commit_timeout)
val {fact_G} = mash_get ctxt
val (old_facts, new_facts) =
- facts |> filter_out fact_has_evil_theory
+ facts |> filter_out (is_thm_technical o snd)
|> List.partition (is_fact_in_graph fact_G)
||> sort (thm_ord o pairself snd)
in