centrally construct expensive data structures

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -459,9 +459,12 @@
         val _ = if is_appropriate_prop concl_t then ()
                 else raise Fail "inappropriate"
         val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
+        val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
+        val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
         val facts =
           Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
-              Sledgehammer_Fact.no_fact_override chained_ths hyp_ts concl_t
+              Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
+              hyp_ts concl_t
           |> filter (is_appropriate_prop o prop_of o snd)
           |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params prover_name
                  (the_default default_max_facts max_facts)

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -126,9 +126,12 @@
          val subgoal = 1
          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
          val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
+         val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
+         val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
          val facts =
            Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
-               Sledgehammer_Fact.no_fact_override chained_ths hyp_ts concl_t
+               Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
+               hyp_ts concl_t
            |> filter (is_appropriate_prop o prop_of o snd)
            |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
                   default_prover (the_default default_max_facts max_facts)

--- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:03 2012 +0200
@@ -26,21 +26,21 @@
 
 ML {*
 if do_it then
-  generate_accessibility thy false "/tmp/mash_accessibility"
+  generate_accessibility @{context} thy false "/tmp/mash_accessibility"
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_features thy false "/tmp/mash_features"
+  generate_features @{context} thy false "/tmp/mash_features"
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_isa_dependencies thy false "/tmp/mash_isa_dependencies"
+  generate_isa_dependencies @{context} thy false "/tmp/mash_isa_dependencies"
 else
   ()
 *}
@@ -54,7 +54,7 @@
 
 ML {*
 if do_it then
-  generate_commands thy "/tmp/mash_commands"
+  generate_commands @{context} thy "/tmp/mash_commands"
 else
   ()
 *}

--- a/src/HOL/TPTP/atp_theory_export.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -105,12 +105,13 @@
 
 fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
   let
+    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val type_enc = type_enc |> type_enc_from_string Strict
                             |> adjust_type_enc format
     val mono = not (is_type_enc_polymorphic type_enc)
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val facts = Sledgehammer_Fact.all_facts_of thy
+    val facts = Sledgehammer_Fact.all_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:03 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -45,7 +45,8 @@
     val prover_name = hd provers
     val path = file_name |> Path.explode
     val lines = path |> File.read_lines
-    val facts = all_non_tautological_facts_of thy
+    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+    val facts = all_non_tautological_facts_of thy css_table
     val all_names = facts |> map (Thm.get_name_hint o snd)
     val iter_ok = Unsynchronized.ref 0
     val mash_ok = Unsynchronized.ref 0

--- a/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -9,7 +9,7 @@
 sig
   type params = Sledgehammer_Provers.params
 
-  val generate_commands : theory -> string -> unit
+  val generate_commands : Proof.context -> theory -> string -> unit
   val generate_iter_suggestions :
     Proof.context -> params -> theory -> int -> string -> unit
 end;
@@ -19,11 +19,12 @@
 
 open Sledgehammer_Filter_MaSh
 
-fun generate_commands thy file_name =
+fun generate_commands ctxt thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val facts = all_non_tautological_facts_of thy
+    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+    val facts = all_non_tautological_facts_of thy css_table
     val (new_facts, old_facts) =
       facts |> List.partition (has_thy thy o snd)
             |>> sort (thm_ord o pairself snd)
@@ -51,7 +52,8 @@
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val facts = all_non_tautological_facts_of thy
+    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+    val facts = all_non_tautological_facts_of thy css_table
     val (new_facts, old_facts) =
       facts |> List.partition (has_thy thy o snd)
             |>> sort (thm_ord o pairself snd)

--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -18,29 +18,34 @@
 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
 struct
 
+open Sledgehammer_Util
 open Sledgehammer_Fact
+open Sledgehammer_Provers
+open Sledgehammer_Filter_MaSh
+open Sledgehammer_Isar
 
 fun run_prover override_params fact_override i n ctxt goal =
   let
-    val mode = Sledgehammer_Provers.Normal
+    val mode = Normal
     val params as {provers, max_facts, slice, ...} =
-      Sledgehammer_Isar.default_params ctxt override_params
+      default_params ctxt override_params
     val name = hd provers
-    val prover = Sledgehammer_Provers.get_prover ctxt mode name
-    val default_max_facts =
-      Sledgehammer_Provers.default_max_facts_for_prover ctxt slice name
+    val prover = get_prover ctxt mode name
+    val default_max_facts = default_max_facts_for_prover ctxt slice name
     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
-    val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
+    val ho_atp = exists (is_ho_atp ctxt) provers
+    val reserved = reserved_isar_keyword_table ()
+    val css_table = clasimpset_rule_table_of ctxt
     val facts =
-      Sledgehammer_Fact.nearly_all_facts ctxt ho_atp fact_override []
-                                         hyp_ts concl_t
-      |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params name
+      nearly_all_facts ctxt ho_atp fact_override reserved css_table [] hyp_ts
+                       concl_t
+      |> relevant_facts ctxt params name
              (the_default default_max_facts max_facts) fact_override hyp_ts
              concl_t
     val problem =
       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
        facts = facts |> map (apfst (apfst (fn name => name ())))
-                     |> map Sledgehammer_Provers.Untranslated_Fact}
+                     |> map Untranslated_Fact}
   in
     (case prover params (K (K (K ""))) problem of
       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -28,10 +28,10 @@
     Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
     -> (((unit -> string) * 'a) * thm) list
   val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
-  val all_facts_of : theory -> fact list
+  val all_facts_of : theory -> status Termtab.table -> fact list
   val nearly_all_facts :
-    Proof.context -> bool -> fact_override -> thm list -> term list -> term
-    -> fact list
+    Proof.context -> bool -> fact_override -> unit Symtab.table
+    -> status Termtab.table -> thm list -> term list -> term -> fact list
 end;
 
 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
@@ -417,14 +417,14 @@
              |> op @
   end
 
-fun all_facts_of thy =
+fun all_facts_of thy css_table =
   let val ctxt = Proof_Context.init_global thy in
-    all_facts ctxt false Symtab.empty true [] []
-              (clasimpset_rule_table_of ctxt)
+    all_facts ctxt false Symtab.empty true [] [] css_table
     |> rev (* try to restore the original order of facts, for MaSh *)
   end
 
-fun nearly_all_facts ctxt ho_atp {add, del, only} chained_ths hyp_ts concl_t =
+fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css_table chained_ths
+                     hyp_ts concl_t =
   if only andalso null add then
     []
   else
@@ -432,8 +432,6 @@
       val chained_ths =
         chained_ths
         |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
-      val reserved = reserved_isar_keyword_table ()
-      val css_table = clasimpset_rule_table_of ctxt
     in
       (if only then
          maps (map (fn ((name, stature), th) => ((K name, stature), th))

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -15,7 +15,8 @@
   type prover_result = Sledgehammer_Provers.prover_result
 
   val fact_name_of : string -> string
-  val all_non_tautological_facts_of : theory -> fact list
+  val all_non_tautological_facts_of :
+    theory -> status Termtab.table -> fact list
   val theory_ord : theory * theory -> order
   val thm_ord : thm * thm -> order
   val thms_by_thy : ('a * thm) list -> (string * thm list) list
@@ -25,9 +26,10 @@
   val isabelle_dependencies_of : string list -> thm -> string list
   val goal_of_thm : theory -> thm -> thm
   val run_prover : Proof.context -> params -> fact list -> thm -> prover_result
-  val generate_accessibility : theory -> bool -> string -> unit
-  val generate_features : theory -> bool -> string -> unit
-  val generate_isa_dependencies : theory -> bool -> string -> unit
+  val generate_accessibility : Proof.context -> theory -> bool -> string -> unit
+  val generate_features : Proof.context -> theory -> bool -> string -> unit
+  val generate_isa_dependencies :
+    Proof.context -> theory -> bool -> string -> unit
   val generate_atp_dependencies :
     Proof.context -> params -> theory -> bool -> string -> unit
   val mash_reset : unit -> unit
@@ -181,8 +183,8 @@
 fun is_too_meta thy th =
   fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool}
 
-fun all_non_tautological_facts_of thy =
-  all_facts_of thy
+fun all_non_tautological_facts_of thy css_table =
+  all_facts_of thy css_table
   |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd)
 
 fun theory_ord p =
@@ -262,17 +264,18 @@
           Sledgehammer_Provers.Normal (hd provers)
   in prover params (K (K (K ""))) problem end
 
-fun generate_accessibility thy include_thy file_name =
+fun generate_accessibility ctxt thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
+    val css_table = clasimpset_rule_table_of ctxt
     fun do_thm th prevs =
       let
         val s = th ^ ": " ^ space_implode " " prevs ^ "\n"
         val _ = File.append path s
       in [th] end
     val thy_ths =
-      all_non_tautological_facts_of thy
+      all_non_tautological_facts_of thy css_table
       |> not include_thy ? filter_out (has_thy thy o snd)
       |> thms_by_thy
     fun do_thy ths =
@@ -283,12 +286,13 @@
       in fold do_thm ths parents; () end
   in List.app (do_thy o snd) thy_ths end
 
-fun generate_features thy include_thy file_name =
+fun generate_features ctxt thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
+    val css_table = clasimpset_rule_table_of ctxt
     val facts =
-      all_non_tautological_facts_of thy
+      all_non_tautological_facts_of thy css_table
       |> not include_thy ? filter_out (has_thy thy o snd)
     fun do_fact ((_, (_, status)), th) =
       let
@@ -298,12 +302,13 @@
       in File.append path s end
   in List.app do_fact facts end
 
-fun generate_isa_dependencies thy include_thy file_name =
+fun generate_isa_dependencies ctxt thy include_thy file_name =
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
+    val css_table = clasimpset_rule_table_of ctxt
     val ths =
-      all_non_tautological_facts_of thy
+      all_non_tautological_facts_of thy css_table
       |> not include_thy ? filter_out (has_thy thy o snd)
       |> map snd
     val all_names = ths |> map Thm.get_name_hint
@@ -320,8 +325,9 @@
   let
     val path = file_name |> Path.explode
     val _ = File.write path ""
+    val css_table = clasimpset_rule_table_of ctxt
     val facts =
-      all_non_tautological_facts_of thy
+      all_non_tautological_facts_of thy css_table
       |> not include_thy ? filter_out (has_thy thy o snd)
     val ths = facts |> map snd
     val all_names = ths |> map Thm.get_name_hint

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:03 2012 +0200
@@ -171,8 +171,11 @@
       val {facts = chained_ths, goal, ...} = Proof.goal state
       val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
       val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
+      val reserved = reserved_isar_keyword_table ()
+      val css_table = clasimpset_rule_table_of ctxt
       val facts =
-        nearly_all_facts ctxt ho_atp fact_override chained_ths hyp_ts concl_t
+        nearly_all_facts ctxt ho_atp fact_override reserved css_table
+                         chained_ths hyp_ts concl_t
       val _ = () |> not blocking ? kill_provers
       val _ = case find_first (not o is_prover_supported ctxt) provers of
                 SOME name => error ("No such prover: " ^ name ^ ".")