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

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

     3.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:03 2012 +0200
     3.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 18 08:44:03 2012 +0200
     3.3 @@ -26,21 +26,21 @@
     3.4  
     3.5  ML {*
     3.6  if do_it then
     3.7 -  generate_accessibility thy false "/tmp/mash_accessibility"
     3.8 +  generate_accessibility @{context} thy false "/tmp/mash_accessibility"
     3.9  else
    3.10    ()
    3.11  *}
    3.12  
    3.13  ML {*
    3.14  if do_it then
    3.15 -  generate_features thy false "/tmp/mash_features"
    3.16 +  generate_features @{context} thy false "/tmp/mash_features"
    3.17  else
    3.18    ()
    3.19  *}
    3.20  
    3.21  ML {*
    3.22  if do_it then
    3.23 -  generate_isa_dependencies thy false "/tmp/mash_isa_dependencies"
    3.24 +  generate_isa_dependencies @{context} thy false "/tmp/mash_isa_dependencies"
    3.25  else
    3.26    ()
    3.27  *}
    3.28 @@ -54,7 +54,7 @@
    3.29  
    3.30  ML {*
    3.31  if do_it then
    3.32 -  generate_commands thy "/tmp/mash_commands"
    3.33 +  generate_commands @{context} thy "/tmp/mash_commands"
    3.34  else
    3.35    ()
    3.36  *}

     4.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Wed Jul 18 08:44:03 2012 +0200
     4.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Wed Jul 18 08:44:03 2012 +0200
     4.3 @@ -105,12 +105,13 @@
     4.4  
     4.5  fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
     4.6    let
     4.7 +    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     4.8      val type_enc = type_enc |> type_enc_from_string Strict
     4.9                              |> adjust_type_enc format
    4.10      val mono = not (is_type_enc_polymorphic type_enc)
    4.11      val path = file_name |> Path.explode
    4.12      val _ = File.write path ""
    4.13 -    val facts = Sledgehammer_Fact.all_facts_of thy
    4.14 +    val facts = Sledgehammer_Fact.all_facts_of thy css_table
    4.15      val atp_problem =
    4.16        facts
    4.17        |> map (fn ((_, loc), th) =>

     5.1 --- a/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:03 2012 +0200
     5.2 +++ b/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:03 2012 +0200
     5.3 @@ -45,7 +45,8 @@
     5.4      val prover_name = hd provers
     5.5      val path = file_name |> Path.explode
     5.6      val lines = path |> File.read_lines
     5.7 -    val facts = all_non_tautological_facts_of thy
     5.8 +    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     5.9 +    val facts = all_non_tautological_facts_of thy css_table
    5.10      val all_names = facts |> map (Thm.get_name_hint o snd)
    5.11      val iter_ok = Unsynchronized.ref 0
    5.12      val mash_ok = Unsynchronized.ref 0

     6.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
     6.2 +++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
     6.3 @@ -9,7 +9,7 @@
     6.4  sig
     6.5    type params = Sledgehammer_Provers.params
     6.6  
     6.7 -  val generate_commands : theory -> string -> unit
     6.8 +  val generate_commands : Proof.context -> theory -> string -> unit
     6.9    val generate_iter_suggestions :
    6.10      Proof.context -> params -> theory -> int -> string -> unit
    6.11  end;
    6.12 @@ -19,11 +19,12 @@
    6.13  
    6.14  open Sledgehammer_Filter_MaSh
    6.15  
    6.16 -fun generate_commands thy file_name =
    6.17 +fun generate_commands ctxt thy file_name =
    6.18    let
    6.19      val path = file_name |> Path.explode
    6.20      val _ = File.write path ""
    6.21 -    val facts = all_non_tautological_facts_of thy
    6.22 +    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    6.23 +    val facts = all_non_tautological_facts_of thy css_table
    6.24      val (new_facts, old_facts) =
    6.25        facts |> List.partition (has_thy thy o snd)
    6.26              |>> sort (thm_ord o pairself snd)
    6.27 @@ -51,7 +52,8 @@
    6.28    let
    6.29      val path = file_name |> Path.explode
    6.30      val _ = File.write path ""
    6.31 -    val facts = all_non_tautological_facts_of thy
    6.32 +    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    6.33 +    val facts = all_non_tautological_facts_of thy css_table
    6.34      val (new_facts, old_facts) =
    6.35        facts |> List.partition (has_thy thy o snd)
    6.36              |>> sort (thm_ord o pairself snd)

     7.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 18 08:44:03 2012 +0200
     7.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Jul 18 08:44:03 2012 +0200
     7.3 @@ -18,29 +18,34 @@
     7.4  structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
     7.5  struct
     7.6  
     7.7 +open Sledgehammer_Util
     7.8  open Sledgehammer_Fact
     7.9 +open Sledgehammer_Provers
    7.10 +open Sledgehammer_Filter_MaSh
    7.11 +open Sledgehammer_Isar
    7.12  
    7.13  fun run_prover override_params fact_override i n ctxt goal =
    7.14    let
    7.15 -    val mode = Sledgehammer_Provers.Normal
    7.16 +    val mode = Normal
    7.17      val params as {provers, max_facts, slice, ...} =
    7.18 -      Sledgehammer_Isar.default_params ctxt override_params
    7.19 +      default_params ctxt override_params
    7.20      val name = hd provers
    7.21 -    val prover = Sledgehammer_Provers.get_prover ctxt mode name
    7.22 -    val default_max_facts =
    7.23 -      Sledgehammer_Provers.default_max_facts_for_prover ctxt slice name
    7.24 +    val prover = get_prover ctxt mode name
    7.25 +    val default_max_facts = default_max_facts_for_prover ctxt slice name
    7.26      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
    7.27 -    val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
    7.28 +    val ho_atp = exists (is_ho_atp ctxt) provers
    7.29 +    val reserved = reserved_isar_keyword_table ()
    7.30 +    val css_table = clasimpset_rule_table_of ctxt
    7.31      val facts =
    7.32 -      Sledgehammer_Fact.nearly_all_facts ctxt ho_atp fact_override []
    7.33 -                                         hyp_ts concl_t
    7.34 -      |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params name
    7.35 +      nearly_all_facts ctxt ho_atp fact_override reserved css_table [] hyp_ts
    7.36 +                       concl_t
    7.37 +      |> relevant_facts ctxt params name
    7.38               (the_default default_max_facts max_facts) fact_override hyp_ts
    7.39               concl_t
    7.40      val problem =
    7.41        {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
    7.42         facts = facts |> map (apfst (apfst (fn name => name ())))
    7.43 -                     |> map Sledgehammer_Provers.Untranslated_Fact}
    7.44 +                     |> map Untranslated_Fact}
    7.45    in
    7.46      (case prover params (K (K (K ""))) problem of
    7.47        {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME

     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:03 2012 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Jul 18 08:44:03 2012 +0200
     8.3 @@ -28,10 +28,10 @@
     8.4      Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
     8.5      -> (((unit -> string) * 'a) * thm) list
     8.6    val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
     8.7 -  val all_facts_of : theory -> fact list
     8.8 +  val all_facts_of : theory -> status Termtab.table -> fact list
     8.9    val nearly_all_facts :
    8.10 -    Proof.context -> bool -> fact_override -> thm list -> term list -> term
    8.11 -    -> fact list
    8.12 +    Proof.context -> bool -> fact_override -> unit Symtab.table
    8.13 +    -> status Termtab.table -> thm list -> term list -> term -> fact list
    8.14  end;
    8.15  
    8.16  structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
    8.17 @@ -417,14 +417,14 @@
    8.18               |> op @
    8.19    end
    8.20  
    8.21 -fun all_facts_of thy =
    8.22 +fun all_facts_of thy css_table =
    8.23    let val ctxt = Proof_Context.init_global thy in
    8.24 -    all_facts ctxt false Symtab.empty true [] []
    8.25 -              (clasimpset_rule_table_of ctxt)
    8.26 +    all_facts ctxt false Symtab.empty true [] [] css_table
    8.27      |> rev (* try to restore the original order of facts, for MaSh *)
    8.28    end
    8.29  
    8.30 -fun nearly_all_facts ctxt ho_atp {add, del, only} chained_ths hyp_ts concl_t =
    8.31 +fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css_table chained_ths
    8.32 +                     hyp_ts concl_t =
    8.33    if only andalso null add then
    8.34      []
    8.35    else
    8.36 @@ -432,8 +432,6 @@
    8.37        val chained_ths =
    8.38          chained_ths
    8.39          |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
    8.40 -      val reserved = reserved_isar_keyword_table ()
    8.41 -      val css_table = clasimpset_rule_table_of ctxt
    8.42      in
    8.43        (if only then
    8.44           maps (map (fn ((name, stature), th) => ((K name, stature), th))

     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:03 2012 +0200
     9.3 @@ -15,7 +15,8 @@
     9.4    type prover_result = Sledgehammer_Provers.prover_result
     9.5  
     9.6    val fact_name_of : string -> string
     9.7 -  val all_non_tautological_facts_of : theory -> fact list
     9.8 +  val all_non_tautological_facts_of :
     9.9 +    theory -> status Termtab.table -> fact list
    9.10    val theory_ord : theory * theory -> order
    9.11    val thm_ord : thm * thm -> order
    9.12    val thms_by_thy : ('a * thm) list -> (string * thm list) list
    9.13 @@ -25,9 +26,10 @@
    9.14    val isabelle_dependencies_of : string list -> thm -> string list
    9.15    val goal_of_thm : theory -> thm -> thm
    9.16    val run_prover : Proof.context -> params -> fact list -> thm -> prover_result
    9.17 -  val generate_accessibility : theory -> bool -> string -> unit
    9.18 -  val generate_features : theory -> bool -> string -> unit
    9.19 -  val generate_isa_dependencies : theory -> bool -> string -> unit
    9.20 +  val generate_accessibility : Proof.context -> theory -> bool -> string -> unit
    9.21 +  val generate_features : Proof.context -> theory -> bool -> string -> unit
    9.22 +  val generate_isa_dependencies :
    9.23 +    Proof.context -> theory -> bool -> string -> unit
    9.24    val generate_atp_dependencies :
    9.25      Proof.context -> params -> theory -> bool -> string -> unit
    9.26    val mash_reset : unit -> unit
    9.27 @@ -181,8 +183,8 @@
    9.28  fun is_too_meta thy th =
    9.29    fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool}
    9.30  
    9.31 -fun all_non_tautological_facts_of thy =
    9.32 -  all_facts_of thy
    9.33 +fun all_non_tautological_facts_of thy css_table =
    9.34 +  all_facts_of thy css_table
    9.35    |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd)
    9.36  
    9.37  fun theory_ord p =
    9.38 @@ -262,17 +264,18 @@
    9.39            Sledgehammer_Provers.Normal (hd provers)
    9.40    in prover params (K (K (K ""))) problem end
    9.41  
    9.42 -fun generate_accessibility thy include_thy file_name =
    9.43 +fun generate_accessibility ctxt thy include_thy file_name =
    9.44    let
    9.45      val path = file_name |> Path.explode
    9.46      val _ = File.write path ""
    9.47 +    val css_table = clasimpset_rule_table_of ctxt
    9.48      fun do_thm th prevs =
    9.49        let
    9.50          val s = th ^ ": " ^ space_implode " " prevs ^ "\n"
    9.51          val _ = File.append path s
    9.52        in [th] end
    9.53      val thy_ths =
    9.54 -      all_non_tautological_facts_of thy
    9.55 +      all_non_tautological_facts_of thy css_table
    9.56        |> not include_thy ? filter_out (has_thy thy o snd)
    9.57        |> thms_by_thy
    9.58      fun do_thy ths =
    9.59 @@ -283,12 +286,13 @@
    9.60        in fold do_thm ths parents; () end
    9.61    in List.app (do_thy o snd) thy_ths end
    9.62  
    9.63 -fun generate_features thy include_thy file_name =
    9.64 +fun generate_features ctxt thy include_thy file_name =
    9.65    let
    9.66      val path = file_name |> Path.explode
    9.67      val _ = File.write path ""
    9.68 +    val css_table = clasimpset_rule_table_of ctxt
    9.69      val facts =
    9.70 -      all_non_tautological_facts_of thy
    9.71 +      all_non_tautological_facts_of thy css_table
    9.72        |> not include_thy ? filter_out (has_thy thy o snd)
    9.73      fun do_fact ((_, (_, status)), th) =
    9.74        let
    9.75 @@ -298,12 +302,13 @@
    9.76        in File.append path s end
    9.77    in List.app do_fact facts end
    9.78  
    9.79 -fun generate_isa_dependencies thy include_thy file_name =
    9.80 +fun generate_isa_dependencies ctxt thy include_thy file_name =
    9.81    let
    9.82      val path = file_name |> Path.explode
    9.83      val _ = File.write path ""
    9.84 +    val css_table = clasimpset_rule_table_of ctxt
    9.85      val ths =
    9.86 -      all_non_tautological_facts_of thy
    9.87 +      all_non_tautological_facts_of thy css_table
    9.88        |> not include_thy ? filter_out (has_thy thy o snd)
    9.89        |> map snd
    9.90      val all_names = ths |> map Thm.get_name_hint
    9.91 @@ -320,8 +325,9 @@
    9.92    let
    9.93      val path = file_name |> Path.explode
    9.94      val _ = File.write path ""
    9.95 +    val css_table = clasimpset_rule_table_of ctxt
    9.96      val facts =
    9.97 -      all_non_tautological_facts_of thy
    9.98 +      all_non_tautological_facts_of thy css_table
    9.99        |> not include_thy ? filter_out (has_thy thy o snd)
   9.100      val ths = facts |> map snd
   9.101      val all_names = ths |> map Thm.get_name_hint

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