prefer explicit Keyword.keywords;
authorwenzelm
Thu Nov 06 13:36:19 2014 +0100 (2014-11-06)
changeset 5891982a71046dce8
parent 58918 8d36bc5eaed3
child 58920 2f8168dc0eac
prefer explicit Keyword.keywords;
src/Doc/antiquote_setup.ML
src/HOL/Tools/ATP/atp_util.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/Pure/Isar/keyword.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Thu Nov 06 11:44:41 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Thu Nov 06 13:36:19 2014 +0100
     1.3 @@ -191,6 +191,9 @@
     1.4  
     1.5  fun no_check _ _ = true;
     1.6  
     1.7 +fun is_keyword _ (name, _) =
     1.8 +  Keyword.is_keyword (Keyword.get_keywords ()) name;
     1.9 +
    1.10  fun check_command ctxt (name, pos) =
    1.11    is_some (Keyword.command_keyword name) andalso
    1.12      let
    1.13 @@ -259,8 +262,8 @@
    1.14    Theory.setup
    1.15     (entity_antiqs no_check "" @{binding syntax} #>
    1.16      entity_antiqs check_command "isacommand" @{binding command} #>
    1.17 -    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding keyword} #>
    1.18 -    entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding element} #>
    1.19 +    entity_antiqs is_keyword "isakeyword" @{binding keyword} #>
    1.20 +    entity_antiqs is_keyword "isakeyword" @{binding element} #>
    1.21      entity_antiqs (can o Method.check_name) "" @{binding method} #>
    1.22      entity_antiqs (can o Attrib.check_name) "" @{binding attribute} #>
    1.23      entity_antiqs no_check "" @{binding fact} #>
     2.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Thu Nov 06 11:44:41 2014 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Nov 06 13:36:19 2014 +0100
     2.3 @@ -140,7 +140,7 @@
     2.4    let val s = unyxml y in
     2.5      y |> ((not (is_long_identifier (unquote_tvar s)) andalso
     2.6             not (is_long_identifier (unquery_var s))) orelse
     2.7 -           Keyword.is_keyword s) ? quote
     2.8 +           Keyword.is_keyword (Keyword.get_keywords ()) s) ? quote
     2.9    end
    2.10  
    2.11  fun string_of_ext_time (plus, time) =
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Nov 06 11:44:41 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Nov 06 13:36:19 2014 +0100
     3.3 @@ -267,10 +267,10 @@
     3.4          val {facts = chained, goal, ...} = Proof.goal state
     3.5          val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
     3.6          val ho_atp = exists (is_ho_atp ctxt) provers
     3.7 -        val reserved = reserved_isar_keyword_table ()
     3.8 +        val keywords = Keyword.get_keywords ()
     3.9          val css = clasimpset_rule_table_of ctxt
    3.10          val all_facts =
    3.11 -          nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts concl_t
    3.12 +          nearly_all_facts ctxt ho_atp fact_override keywords css chained hyp_ts concl_t
    3.13          val _ = () |> not blocking ? kill_provers
    3.14          val _ =
    3.15            (case find_first (not o is_prover_supported ctxt) provers of
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Nov 06 11:44:41 2014 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Nov 06 13:36:19 2014 +0100
     4.3 @@ -21,7 +21,7 @@
     4.4    val instantiate_inducts : bool Config.T
     4.5    val no_fact_override : fact_override
     4.6  
     4.7 -  val fact_of_ref : Proof.context -> unit Symtab.table -> thm list -> status Termtab.table ->
     4.8 +  val fact_of_ref : Proof.context -> Keyword.keywords -> thm list -> status Termtab.table ->
     4.9      Facts.ref * Token.src list -> ((string * stature) * thm) list
    4.10    val backquote_thm : Proof.context -> thm -> string
    4.11    val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
    4.12 @@ -33,9 +33,9 @@
    4.13    val fact_of_raw_fact : raw_fact -> fact
    4.14    val is_useful_unnamed_local_fact : Proof.context -> thm -> bool
    4.15  
    4.16 -  val all_facts : Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list ->
    4.17 +  val all_facts : Proof.context -> bool -> bool -> Keyword.keywords -> thm list -> thm list ->
    4.18      status Termtab.table -> raw_fact list
    4.19 -  val nearly_all_facts : Proof.context -> bool -> fact_override -> unit Symtab.table ->
    4.20 +  val nearly_all_facts : Proof.context -> bool -> fact_override -> Keyword.keywords ->
    4.21      status Termtab.table -> thm list -> term list -> term -> raw_fact list
    4.22    val drop_duplicate_facts : raw_fact list -> raw_fact list
    4.23  end;
    4.24 @@ -66,12 +66,12 @@
    4.25  
    4.26  val no_fact_override = {add = [], del = [], only = false}
    4.27  
    4.28 -fun needs_quoting reserved s =
    4.29 -  Symtab.defined reserved s orelse
    4.30 +fun needs_quoting keywords s =
    4.31 +  Keyword.is_keyword keywords s orelse
    4.32    exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s)
    4.33  
    4.34 -fun make_name reserved multi j name =
    4.35 -  (name |> needs_quoting reserved name ? quote) ^
    4.36 +fun make_name keywords multi j name =
    4.37 +  (name |> needs_quoting keywords name ? quote) ^
    4.38    (if multi then "(" ^ string_of_int j ^ ")" else "")
    4.39  
    4.40  fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
    4.41 @@ -157,7 +157,7 @@
    4.42  fun stature_of_thm global assms chained css name th =
    4.43    (scope_of_thm global assms chained th, status_of_thm css name th)
    4.44  
    4.45 -fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) =
    4.46 +fun fact_of_ref ctxt keywords chained css (xthm as (xref, args)) =
    4.47    let
    4.48      val ths = Attrib.eval_thms ctxt [xthm]
    4.49      val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src ctxt) args)
    4.50 @@ -166,9 +166,9 @@
    4.51        (case xref of
    4.52          Facts.Fact s => backquote (simplify_spaces (unyxml s)) ^ bracket
    4.53        | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
    4.54 -      | Facts.Named ((name, _), NONE) => make_name reserved (length ths > 1) (j + 1) name ^ bracket
    4.55 +      | Facts.Named ((name, _), NONE) => make_name keywords (length ths > 1) (j + 1) name ^ bracket
    4.56        | Facts.Named ((name, _), SOME intervals) =>
    4.57 -        make_name reserved true
    4.58 +        make_name keywords true
    4.59            (nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket)
    4.60  
    4.61      fun add_nth th (j, rest) =
    4.62 @@ -455,7 +455,7 @@
    4.63        forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
    4.64    end
    4.65  
    4.66 -fun all_facts ctxt generous ho_atp reserved add_ths chained css =
    4.67 +fun all_facts ctxt generous ho_atp keywords add_ths chained css =
    4.68    let
    4.69      val thy = Proof_Context.theory_of ctxt
    4.70      val global_facts = Global_Theory.facts_of thy
    4.71 @@ -514,7 +514,7 @@
    4.72                                 name0
    4.73                             end
    4.74                         end
    4.75 -                       |> make_name reserved multi j
    4.76 +                       |> make_name keywords multi j
    4.77                     val stature = stature_of_thm global assms chained css name0 th
    4.78                     val new = ((get_name, stature), th)
    4.79                   in
    4.80 @@ -530,7 +530,7 @@
    4.81      |> op @
    4.82    end
    4.83  
    4.84 -fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts concl_t =
    4.85 +fun nearly_all_facts ctxt ho_atp {add, del, only} keywords css chained hyp_ts concl_t =
    4.86    if only andalso null add then
    4.87      []
    4.88    else
    4.89 @@ -539,12 +539,12 @@
    4.90      in
    4.91        (if only then
    4.92           maps (map (fn ((name, stature), th) => ((K name, stature), th))
    4.93 -           o fact_of_ref ctxt reserved chained css) add
    4.94 +           o fact_of_ref ctxt keywords chained css) add
    4.95         else
    4.96           let
    4.97             val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del)
    4.98             val facts =
    4.99 -             all_facts ctxt false ho_atp reserved add chained css
   4.100 +             all_facts ctxt false ho_atp keywords add chained css
   4.101               |> filter_out ((member Thm.eq_thm_prop del orf
   4.102                 (Named_Theorems.member ctxt @{named_theorems no_atp} andf
   4.103                   not o member Thm.eq_thm_prop add)) o snd)
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Nov 06 11:44:41 2014 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Nov 06 13:36:19 2014 +0100
     5.3 @@ -1467,7 +1467,8 @@
     5.4    let
     5.5      val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     5.6      val ctxt = ctxt |> Config.put instantiate_inducts false
     5.7 -    val facts = nearly_all_facts ctxt false fact_override Symtab.empty css chained [] @{prop True}
     5.8 +    val facts =
     5.9 +      nearly_all_facts ctxt false fact_override Keyword.empty_keywords css chained [] @{prop True}
    5.10        |> sort (crude_thm_ord o pairself snd o swap)
    5.11      val num_facts = length facts
    5.12      val prover = hd provers
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Nov 06 11:44:41 2014 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Nov 06 13:36:19 2014 +0100
     6.3 @@ -17,7 +17,6 @@
     6.4    val parse_bool_option : bool -> string -> string -> bool option
     6.5    val parse_time : string -> string -> Time.time
     6.6    val subgoal_count : Proof.state -> int
     6.7 -  val reserved_isar_keyword_table : unit -> unit Symtab.table
     6.8    val thms_in_proof : int -> (string Symtab.table * string Symtab.table) option -> thm ->
     6.9      string list option
    6.10    val thms_of_name : Proof.context -> string -> thm list
    6.11 @@ -79,9 +78,6 @@
    6.12  
    6.13  val subgoal_count = Try.subgoal_count
    6.14  
    6.15 -fun reserved_isar_keyword_table () =
    6.16 -  Symtab.make_set (Scan.dest_lexicon (Scan.merge_lexicons (Keyword.get_lexicons ())));
    6.17 -
    6.18  exception TOO_MANY of unit
    6.19  
    6.20  (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few fixes that seem to
     7.1 --- a/src/Pure/Isar/keyword.ML	Thu Nov 06 11:44:41 2014 +0100
     7.2 +++ b/src/Pure/Isar/keyword.ML	Thu Nov 06 13:36:19 2014 +0100
     7.3 @@ -43,8 +43,7 @@
     7.4    val add: string * T option -> keywords -> keywords
     7.5    val define: string * T option -> unit
     7.6    val get_keywords: unit -> keywords
     7.7 -  val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
     7.8 -  val is_keyword: string -> bool
     7.9 +  val is_keyword: keywords -> string -> bool
    7.10    val command_keyword: string -> T option
    7.11    val command_files: string -> Path.T -> Path.T list
    7.12    val command_tags: string -> string list
    7.13 @@ -182,18 +181,15 @@
    7.14  
    7.15  end;
    7.16  
    7.17 -fun get_lexicons () =
    7.18 -  let val keywords = get_keywords ()
    7.19 -  in (minor_keywords keywords, major_keywords keywords) end;
    7.20 -
    7.21  fun get_commands () = commands (get_keywords ());
    7.22  
    7.23  
    7.24  (* lookup *)
    7.25  
    7.26 -fun is_keyword s =
    7.27 +fun is_keyword keywords s =
    7.28    let
    7.29 -    val (minor, major) = get_lexicons ();
    7.30 +    val minor = minor_keywords keywords;
    7.31 +    val major = major_keywords keywords;
    7.32      val syms = Symbol.explode s;
    7.33    in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
    7.34