--- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:04 2012 +0200
@@ -113,14 +113,12 @@
handle TYPE _ => @{prop True}
end
-fun all_non_tautological_facts_of ctxt prover thy css_table =
+fun all_non_tautological_facts_of thy css_table =
Sledgehammer_Fact.all_facts_of thy css_table
- |> filter_out ((Sledgehammer_Filter_MaSh.is_likely_tautology ctxt prover orf
- Sledgehammer_Filter_MaSh.is_too_meta) o snd)
+ |> filter_out (Sledgehammer_Filter_MaSh.is_likely_tautology_or_too_meta o snd)
fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
let
- val atp = atp_for_format format
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val type_enc =
type_enc |> type_enc_from_string Strict
@@ -128,7 +126,7 @@
val mono = not (is_type_enc_polymorphic type_enc)
val path = file_name |> Path.explode
val _ = File.write path ""
- val facts = all_non_tautological_facts_of ctxt atp thy css_table
+ val facts = all_non_tautological_facts_of thy css_table
val atp_problem =
facts
|> map (fn ((_, loc), th) =>
--- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200
@@ -26,8 +26,8 @@
val max_facts_slack = 2
-fun all_names ctxt prover =
- filter_out (is_likely_tautology ctxt prover orf is_too_meta)
+val all_names =
+ filter_out (is_likely_tautology_or_too_meta)
#> map (rpair () o Thm.get_name_hint) #> Symtab.make
fun evaluate_mash_suggestions ctxt params thy file_name =
@@ -40,7 +40,7 @@
val lines = path |> File.read_lines
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val facts = all_facts_of thy css_table
- val all_names = all_names ctxt prover (facts |> map snd)
+ val all_names = all_names (facts |> map snd)
val iter_ok = Unsynchronized.ref 0
val mash_ok = Unsynchronized.ref 0
val mesh_ok = Unsynchronized.ref 0
--- a/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:04 2012 +0200
@@ -13,7 +13,7 @@
val generate_features :
Proof.context -> string -> theory -> bool -> string -> unit
val generate_isa_dependencies :
- Proof.context -> string -> theory -> bool -> string -> unit
+ theory -> bool -> string -> unit
val generate_prover_dependencies :
Proof.context -> params -> theory -> bool -> string -> unit
val generate_commands : Proof.context -> string -> theory -> string -> unit
@@ -49,8 +49,8 @@
val thy_name_of_fact = hd o Long_Name.explode
fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact
-fun all_names ctxt prover =
- filter_out (is_likely_tautology ctxt prover orf is_too_meta)
+val all_names =
+ filter_out (is_likely_tautology_or_too_meta)
#> map (rpair () o Thm.get_name_hint) #> Symtab.make
fun generate_accessibility thy include_thy file_name =
@@ -90,7 +90,7 @@
in File.append path s end
in List.app do_fact facts end
-fun generate_isa_dependencies ctxt prover thy include_thy file_name =
+fun generate_isa_dependencies thy include_thy file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
@@ -98,7 +98,7 @@
all_facts_of thy Termtab.empty
|> not include_thy ? filter_out (has_thy thy o snd)
|> map snd
- val all_names = all_names ctxt prover ths
+ val all_names = all_names ths
fun do_thm th =
let
val name = Thm.get_name_hint th
@@ -117,7 +117,7 @@
all_facts_of thy Termtab.empty
|> not include_thy ? filter_out (has_thy thy o snd)
val ths = facts |> map snd
- val all_names = all_names ctxt prover ths
+ val all_names = all_names ths
fun is_dep dep (_, th) = Thm.get_name_hint th = dep
fun add_isa_dep facts dep accum =
if exists (is_dep dep) accum then
@@ -165,7 +165,7 @@
facts |> List.partition (has_thy thy o snd)
|>> sort (thm_ord o pairself snd)
val ths = facts |> map snd
- val all_names = all_names ctxt prover ths
+ val all_names = all_names ths
fun do_fact ((_, (_, status)), th) prevs =
let
val name = Thm.get_name_hint th
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 18 08:44:04 2012 +0200
@@ -87,6 +87,7 @@
val new_skolem_var_name_from_const : string -> string
val atp_logical_consts : string list
val atp_irrelevant_consts : string list
+ val atp_widely_irrelevant_consts : string list
val atp_schematic_consts_of : term -> typ list Symtab.table
val is_type_enc_higher_order : type_enc -> bool
val is_type_enc_polymorphic : type_enc -> bool
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200
@@ -28,8 +28,7 @@
val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
val mesh_facts :
int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list
- val is_likely_tautology : Proof.context -> string -> thm -> bool
- val is_too_meta : thm -> bool
+ val is_likely_tautology_or_too_meta : thm -> bool
val theory_ord : theory * theory -> order
val thm_ord : thm * thm -> order
val features_of :
@@ -201,6 +200,37 @@
end
+fun is_likely_tautology_or_too_meta th =
+ let
+ val is_boring_const = member (op =) atp_widely_irrelevant_consts
+ fun is_boring_bool t =
+ not (exists_Const (not o is_boring_const o fst) t) orelse
+ exists_type (exists_subtype (curry (op =) @{typ prop})) t
+ fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
+ | is_boring_prop (@{const "==>"} $ t $ u) =
+ is_boring_prop t andalso is_boring_prop u
+ | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) =
+ is_boring_prop t andalso is_boring_prop u
+ | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) =
+ is_boring_bool t andalso is_boring_bool u
+ | is_boring_prop _ = true
+ in
+ is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
+ end
+
+fun theory_ord p =
+ if Theory.eq_thy p then
+ EQUAL
+ else if Theory.subthy p then
+ LESS
+ else if Theory.subthy (swap p) then
+ GREATER
+ else case int_ord (pairself (length o Theory.ancestors_of) p) of
+ EQUAL => string_ord (pairself Context.theory_name p)
+ | order => order
+
+val thm_ord = theory_ord o pairself theory_of_thm
+
fun interesting_terms_types_and_classes ctxt prover term_max_depth
type_max_depth ts =
let
@@ -243,28 +273,6 @@
end
in [] |> fold add_patterns ts |> sort string_ord end
-fun is_likely_tautology ctxt prover th =
- null (interesting_terms_types_and_classes ctxt prover 0 ~1 [prop_of th])
- andalso not (Thm.eq_thm_prop (@{thm ext}, th))
-
-(* ### FIXME: optimize *)
-fun is_too_meta th =
- fastype_of (Object_Logic.atomize_term (theory_of_thm th) (prop_of th))
- <> @{typ bool}
-
-fun theory_ord p =
- if Theory.eq_thy p then
- EQUAL
- else if Theory.subthy p then
- LESS
- else if Theory.subthy (swap p) then
- GREATER
- else case int_ord (pairself (length o Theory.ancestors_of) p) of
- EQUAL => string_ord (pairself Context.theory_name p)
- | order => order
-
-val thm_ord = theory_ord o pairself theory_of_thm
-
fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
val term_max_depth = 1
@@ -545,13 +553,18 @@
facts =
let
val timer = Timer.startRealTimer ()
+fun check_timer s =
+ tracing ("*** " ^ s ^ " " ^ PolyML.makestring (Timer.checkRealTimer timer))
val prover = hd provers
fun timed_out frac =
Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
+val _ = check_timer "begin" (*###*)
val {fact_graph, ...} = mash_get ctxt
+val _ = check_timer " got" (*###*)
val new_facts =
facts |> filter_out (is_fact_in_graph fact_graph)
|> sort (thm_ord o pairself snd)
+val _ = check_timer " new facts" (*###*)
in
if null new_facts then
""
@@ -559,9 +572,10 @@
let
val ths = facts |> map snd
val all_names =
- ths |> filter_out (is_likely_tautology ctxt prover orf is_too_meta)
+ ths |> filter_out is_likely_tautology_or_too_meta
|> map (rpair () o Thm.get_name_hint)
|> Symtab.make
+val _ = check_timer " all names" (*###*)
fun do_fact _ (accum as (_, true)) = accum
| do_fact ((_, (_, status)), th) ((parents, upds), false) =
let
@@ -571,8 +585,10 @@
val upd = (name, parents, feats, deps)
in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end
val parents = parents_wrt_facts ctxt facts fact_graph
+val _ = check_timer " parents" (*###*)
val ((_, upds), _) =
((parents, []), false) |> fold do_fact new_facts |>> apsnd rev
+val _ = check_timer " did facts" (*###*)
val n = length upds
fun trans {thys, fact_graph} =
let
@@ -580,8 +596,10 @@
if Graph.is_empty fact_graph then mash_INIT else mash_ADD
val (upds, fact_graph) =
([], fact_graph) |> fold (update_fact_graph ctxt) upds
+val _ = check_timer " updated" (*###*)
in
(mash_INIT_or_ADD ctxt overlord (rev upds);
+check_timer " inited/added" (*###*);
{thys = thys |> add_thys_for thy,
fact_graph = fact_graph})
end