# HG changeset patch
# User blanchet
# Date 1342593844 -7200
# Node ID 3ee5b558940249cbf648acbe7acdb82acae0591c
# Parent  7b5f7ca25d17317c5f8fdd7b9e0b6c04365951d9
speed up tautology/metaness check

diff -r 7b5f7ca25d17 -r 3ee5b5589402 src/HOL/TPTP/atp_theory_export.ML
--- 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) =>
diff -r 7b5f7ca25d17 -r 3ee5b5589402 src/HOL/TPTP/mash_eval.ML
--- 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
diff -r 7b5f7ca25d17 -r 3ee5b5589402 src/HOL/TPTP/mash_export.ML
--- 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
diff -r 7b5f7ca25d17 -r 3ee5b5589402 src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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
diff -r 7b5f7ca25d17 -r 3ee5b5589402 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
--- 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