Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
--- a/src/Doc/Datatypes/Datatypes.thy Mon Oct 13 17:04:25 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Oct 13 18:45:48 2014 +0200
@@ -500,8 +500,10 @@
\item
The @{text "plugins"} option indicates which plugins should be enabled
-(@{text only}) or disabled (@{text del}). Wildcards (``@{text "*"}'') are
-allowed (e.g., @{text "quickcheck_*"}). By default, all plugins are enabled.
+(@{text only}) or disabled (@{text del}). Some plugin names are defined
+as indirection to a group of sub-plugins (notably @{text "quickcheck"}
+based on @{text quickcheck_random}, @{text quickcheck_exhaustive}, \dots).
+By default, all plugins are enabled.
\item
The @{text "discs_sels"} option indicates that discriminators and selectors
@@ -2794,7 +2796,7 @@
For example:
*}
- datatype (plugins del: code "quickcheck_*") color = Red | Black
+ datatype (plugins del: code "quickcheck") color = Red | Black
subsection {* Code Generator
--- a/src/HOL/Ctr_Sugar.thy Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Ctr_Sugar.thy Mon Oct 13 18:45:48 2014 +0200
@@ -37,7 +37,6 @@
"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
by blast+
-ML_file "Tools/Ctr_Sugar/local_interpretation.ML"
ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML"
ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML"
ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML"
--- a/src/HOL/Enum.thy Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Enum.thy Mon Oct 13 18:45:48 2014 +0200
@@ -493,7 +493,7 @@
text {* We define small finite types for use in Quickcheck *}
-datatype (plugins only: code "quickcheck*" extraction) finite_1 =
+datatype (plugins only: code "quickcheck" extraction) finite_1 =
a\<^sub>1
notation (output) a\<^sub>1 ("a\<^sub>1")
@@ -596,7 +596,7 @@
declare [[simproc del: finite_1_eq]]
hide_const (open) a\<^sub>1
-datatype (plugins only: code "quickcheck*" extraction) finite_2 =
+datatype (plugins only: code "quickcheck" extraction) finite_2 =
a\<^sub>1 | a\<^sub>2
notation (output) a\<^sub>1 ("a\<^sub>1")
@@ -711,7 +711,7 @@
hide_const (open) a\<^sub>1 a\<^sub>2
-datatype (plugins only: code "quickcheck*" extraction) finite_3 =
+datatype (plugins only: code "quickcheck" extraction) finite_3 =
a\<^sub>1 | a\<^sub>2 | a\<^sub>3
notation (output) a\<^sub>1 ("a\<^sub>1")
@@ -838,7 +838,7 @@
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
-datatype (plugins only: code "quickcheck*" extraction) finite_4 =
+datatype (plugins only: code "quickcheck" extraction) finite_4 =
a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
notation (output) a\<^sub>1 ("a\<^sub>1")
@@ -940,7 +940,7 @@
hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
-datatype (plugins only: code "quickcheck*" extraction) finite_5 =
+datatype (plugins only: code "quickcheck" extraction) finite_5 =
a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
notation (output) a\<^sub>1 ("a\<^sub>1")
--- a/src/HOL/HOL.thy Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/HOL.thy Mon Oct 13 18:45:48 2014 +0200
@@ -40,6 +40,25 @@
#> Case_Product.setup
*}
+ML \<open>Plugin_Name.declare_setup @{binding extraction}\<close>
+
+ML \<open>
+ Plugin_Name.declare_setup @{binding quickcheck_random};
+ Plugin_Name.declare_setup @{binding quickcheck_exhaustive};
+ Plugin_Name.declare_setup @{binding quickcheck_bounded_forall};
+ Plugin_Name.declare_setup @{binding quickcheck_full_exhaustive};
+ Plugin_Name.declare_setup @{binding quickcheck_narrowing};
+\<close>
+ML \<open>
+ Plugin_Name.define_setup @{binding quickcheck}
+ [@{plugin quickcheck_exhaustive},
+ @{plugin quickcheck_random},
+ @{plugin quickcheck_bounded_forall},
+ @{plugin quickcheck_full_exhaustive},
+ @{plugin quickcheck_narrowing}]
+\<close>
+
+
subsection {* Primitive logic *}
subsubsection {* Core syntax *}
--- a/src/HOL/Library/bnf_axiomatization.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Library/bnf_axiomatization.ML Mon Oct 13 18:45:48 2014 +0200
@@ -17,9 +17,11 @@
open BNF_Util
open BNF_Def
-fun prepare_decl prepare_constraint prepare_typ plugins raw_vars b mx user_mapb user_relb user_witTs
- lthy =
+fun prepare_decl prepare_plugins prepare_constraint prepare_typ
+ raw_plugins raw_vars b mx user_mapb user_relb user_witTs lthy =
let
+ val plugins = prepare_plugins lthy raw_plugins;
+
fun prepare_type_arg (set_opt, (ty, c)) =
let val s = fst (dest_TFree (prepare_typ lthy ty)) in
(set_opt, (s, prepare_constraint lthy c))
@@ -95,12 +97,12 @@
(bnf, register_bnf plugins key bnf lthy')
end;
-val bnf_axiomatization = prepare_decl (K I) (K I);
+val bnf_axiomatization = prepare_decl (K I) (K I) (K I);
fun read_constraint _ NONE = @{sort type}
| read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
-val bnf_axiomatization_cmd = prepare_decl read_constraint Syntax.read_typ;
+val bnf_axiomatization_cmd = prepare_decl Plugin_Name.make_filter read_constraint Syntax.read_typ;
val parse_witTs =
@{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ
@@ -109,7 +111,7 @@
@{keyword "]"} || Scan.succeed [];
val parse_bnf_axiomatization_options =
- Scan.optional (@{keyword "("} |-- parse_plugins --| @{keyword ")"}) (K true);
+ Scan.optional (@{keyword "("} |-- Plugin_Name.parse_filter --| @{keyword ")"}) (K (K true));
val parse_bnf_axiomatization =
parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding --
--- a/src/HOL/Tools/BNF/bnf_def.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Oct 13 18:45:48 2014 +0200
@@ -17,8 +17,7 @@
val transfer_bnf: theory -> bnf -> bnf
val bnf_of: Proof.context -> string -> bnf option
val bnf_of_global: theory -> string -> bnf option
- val bnf_interpretation: string -> (bnf -> theory -> theory) ->
- (bnf -> local_theory -> local_theory) -> theory -> theory
+ val bnf_interpretation: string -> (bnf -> local_theory -> local_theory) -> theory -> theory
val interpret_bnf: (string -> bool) -> bnf -> local_theory -> local_theory
val register_bnf_raw: string -> bnf -> local_theory -> local_theory
val register_bnf: (string -> bool) -> string -> bnf -> local_theory -> local_theory
@@ -1514,18 +1513,13 @@
(key, goals, wit_goalss, after_qed, lthy, one_step_defs)
end;
-structure BNF_Interpretation = Local_Interpretation
-(
- type T = bnf;
- val eq: T * T -> bool = op = o pairself T_of_bnf;
-);
+structure BNF_Plugin = Plugin(type T = bnf);
-fun with_transfer_bnf g bnf thy = g (transfer_bnf thy bnf) thy;
+fun bnf_interpretation name f =
+ BNF_Plugin.interpretation name
+ (fn bnf => fn lthy => f (transfer_bnf (Proof_Context.theory_of lthy) bnf) lthy);
-fun bnf_interpretation name =
- BNF_Interpretation.interpretation name o with_transfer_bnf;
-
-val interpret_bnf = BNF_Interpretation.data;
+val interpret_bnf = BNF_Plugin.data;
fun register_bnf_raw key bnf =
Local_Theory.declaration {syntax = false, pervasive = true}
@@ -1557,9 +1551,10 @@
end) o prepare_def const_policy fact_policy internal qualify (K I) (K I) Ds map_b rel_b set_bs
raw_csts;
-fun bnf_cmd (raw_csts, plugins) =
+fun bnf_cmd (raw_csts, raw_plugins) =
(fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) =>
let
+ val plugins = raw_plugins lthy;
val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
fun mk_triv_wit_thms tac set_maps =
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
@@ -1619,9 +1614,7 @@
Scan.repeat1 (Scan.unless (Parse.reserved "rel" ||
Parse.reserved "plugins") Parse.term)) [] --
Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term) --
- Scan.optional parse_plugins (K true)
+ Scan.optional Plugin_Name.parse_filter (K (K true))
>> bnf_cmd);
-val _ = Context.>> (Context.map_theory BNF_Interpretation.init);
-
end;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 13 18:45:48 2014 +0200
@@ -67,7 +67,7 @@
val fp_sugar_of_global: theory -> string -> fp_sugar option
val fp_sugars_of: Proof.context -> fp_sugar list
val fp_sugars_of_global: theory -> fp_sugar list
- val fp_sugars_interpretation: string -> (fp_sugar list -> theory -> theory) ->
+ val fp_sugars_interpretation: string ->
(fp_sugar list -> local_theory -> local_theory)-> theory -> theory
val interpret_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory
val register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory
@@ -316,18 +316,14 @@
fun co_induct_of (i :: _) = i;
fun strong_co_induct_of [_, s] = s;
-structure FP_Sugar_Interpretation = Local_Interpretation
-(
- type T = fp_sugar list;
- val eq: T * T -> bool = op = o pairself (map #T);
-);
+structure FP_Sugar_Plugin = Plugin(type T = fp_sugar list);
-fun with_transfer_fp_sugars g fp_sugars thy = g (map (transfer_fp_sugar thy) fp_sugars) thy;
+fun fp_sugars_interpretation name f =
+ FP_Sugar_Plugin.interpretation name
+ (fn fp_sugars => fn lthy =>
+ f (map (transfer_fp_sugar (Proof_Context.theory_of lthy)) fp_sugars) lthy);
-fun fp_sugars_interpretation name =
- FP_Sugar_Interpretation.interpretation name o with_transfer_fp_sugars;
-
-val interpret_fp_sugars = FP_Sugar_Interpretation.data;
+val interpret_fp_sugars = FP_Sugar_Plugin.data;
fun register_fp_sugars_raw fp_sugars =
fold (fn fp_sugar as {T = Type (s, _), ...} =>
@@ -984,7 +980,7 @@
|> map Thm.close_derivation
end;
- val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
+ val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else [];
val anonymous_notes =
[(rel_code_thms, code_attrs @ nitpicksimp_attrs)]
@@ -1417,7 +1413,7 @@
val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms;
- val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
+ val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else [];
in
((induct_thms, induct_thm, mk_induct_attrs ctrss),
(rec_thmss, code_attrs @ nitpicksimp_attrs @ simp_attrs))
@@ -1828,11 +1824,12 @@
(corec_sel_thmsss, simp_attrs))
end;
-fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
- ((plugins, discs_sels0), specs) no_defs_lthy =
+fun define_co_datatypes prepare_plugins prepare_constraint prepare_typ prepare_term fp construct_fp
+ ((raw_plugins, discs_sels0), specs) no_defs_lthy =
let
(* TODO: sanity checks on arguments *)
+ val plugins = prepare_plugins no_defs_lthy raw_plugins;
val discs_sels = discs_sels0 orelse fp = Greatest_FP;
val nn = length specs;
@@ -2010,7 +2007,7 @@
val fpTs = map (domain_type o fastype_of) dtors;
val fpBTs = map B_ify_T fpTs;
- val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
+ val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else [];
val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss;
val ns = map length ctr_Tsss;
@@ -2375,10 +2372,11 @@
timer; lthy''
end;
-fun co_datatypes x = define_co_datatypes (K I) (K I) (K I) x;
+fun co_datatypes x = define_co_datatypes (K I) (K I) (K I) (K I) x;
fun co_datatype_cmd x =
- define_co_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term x;
+ define_co_datatypes Plugin_Name.make_filter Typedecl.read_constraint
+ Syntax.parse_typ Syntax.parse_term x;
val parse_ctr_arg =
@{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"}
@@ -2395,6 +2393,4 @@
fun parse_co_datatype_cmd fp construct_fp = parse_co_datatype >> co_datatype_cmd fp construct_fp;
-val _ = Theory.setup FP_Sugar_Interpretation.init;
-
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Oct 13 18:45:48 2014 +0200
@@ -451,10 +451,8 @@
end;
fun interpretation name prefs f =
- let val new_f = new_interpretation_of prefs f in
- Old_Datatype_Data.interpretation (old_interpretation_of prefs f)
- #> fp_sugars_interpretation name new_f (Local_Theory.background_theory o new_f)
- end;
+ Old_Datatype_Data.interpretation (old_interpretation_of prefs f)
+ #> fp_sugars_interpretation name (Local_Theory.background_theory o new_interpretation_of prefs f);
val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]};
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Oct 13 18:45:48 2014 +0200
@@ -7,7 +7,6 @@
signature BNF_LFP_SIZE =
sig
- val size_plugin: string
val register_size: string -> string -> thm list -> thm list -> local_theory -> local_theory
val register_size_global: string -> string -> thm list -> thm list -> theory -> theory
val size_of: Proof.context -> string -> (string * (thm list * thm list)) option
@@ -22,8 +21,6 @@
open BNF_Def
open BNF_FP_Def_Sugar
-val size_plugin = "size";
-
val size_N = "size_";
val rec_o_mapN = "rec_o_map";
@@ -396,7 +393,7 @@
end
| generate_datatype_size _ lthy = lthy;
-val _ = Theory.setup (fp_sugars_interpretation size_plugin
- (map_local_theory o generate_datatype_size) generate_datatype_size);
+val size_plugin = Plugin_Name.declare_setup @{binding size};
+val _ = Theory.setup (fp_sugars_interpretation size_plugin generate_datatype_size);
end;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Oct 13 18:45:48 2014 +0200
@@ -7,8 +7,6 @@
signature CTR_SUGAR =
sig
- val code_plugin: string
-
type ctr_sugar =
{T: typ,
ctrs: term list,
@@ -46,7 +44,7 @@
val ctr_sugars_of_global: theory -> ctr_sugar list
val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option
- val ctr_sugar_interpretation: string -> (ctr_sugar -> theory -> theory) ->
+ val ctr_sugar_interpretation: string ->
(ctr_sugar -> local_theory -> local_theory) -> theory -> theory
val interpret_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory
val register_ctr_sugar_raw: ctr_sugar -> local_theory -> local_theory
@@ -72,14 +70,16 @@
val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list
type ctr_options = (string -> bool) * bool
+ type ctr_options_cmd = (Proof.context -> string -> bool) * bool
val fake_local_theory_for_sel_defaults: (binding * typ) list -> Proof.context -> Proof.context
val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
((ctr_options * binding) * (term, binding) ctr_spec list) * term list -> local_theory ->
ctr_sugar * local_theory
val default_ctr_options: ctr_options
+ val default_ctr_options_cmd: ctr_options_cmd
val parse_bound_term: (binding * string) parser
- val parse_ctr_options: ctr_options parser
+ val parse_ctr_options: ctr_options_cmd parser
val parse_ctr_spec: 'c parser -> 'a parser -> ('c, 'a) ctr_spec parser
val parse_sel_default_eqs: string list parser
end;
@@ -91,8 +91,6 @@
open Ctr_Sugar_Tactics
open Ctr_Sugar_Code
-val code_plugin = "code";
-
type ctr_sugar =
{T: typ,
ctrs: term list,
@@ -183,18 +181,14 @@
val ctr_sugar_of_case = ctr_sugar_of_case_generic o Context.Proof;
val ctr_sugar_of_case_global = ctr_sugar_of_case_generic o Context.Theory;
-structure Ctr_Sugar_Interpretation = Local_Interpretation
-(
- type T = ctr_sugar;
- val eq: T * T -> bool = op = o pairself #ctrs;
-);
+structure Ctr_Sugar_Plugin = Plugin(type T = ctr_sugar);
-fun with_transfer_ctr_sugar g ctr_sugar thy = g (transfer_ctr_sugar thy ctr_sugar) thy;
+fun ctr_sugar_interpretation name f =
+ Ctr_Sugar_Plugin.interpretation name
+ (fn ctr_sugar => fn lthy =>
+ f (transfer_ctr_sugar (Proof_Context.theory_of lthy) ctr_sugar) lthy);
-fun ctr_sugar_interpretation name =
- Ctr_Sugar_Interpretation.interpretation name o with_transfer_ctr_sugar;
-
-val interpret_ctr_sugar = Ctr_Sugar_Interpretation.data;
+val interpret_ctr_sugar = Ctr_Sugar_Plugin.data;
fun register_ctr_sugar_raw (ctr_sugar as {T = Type (s, _), ...}) =
Local_Theory.declaration {syntax = false, pervasive = true}
@@ -210,7 +204,9 @@
else
thy
|> Context.theory_map (Data.put (Symtab.update_new (s, ctr_sugar) tab))
- |> Ctr_Sugar_Interpretation.data_global plugins ctr_sugar
+ |> Named_Target.theory_init
+ |> Ctr_Sugar_Plugin.data plugins ctr_sugar
+ |> Local_Theory.exit_global
end;
val isN = "is_";
@@ -364,9 +360,15 @@
fun ctr_of_ctr_spec ((_, ctr), _) = ctr;
fun args_of_ctr_spec (_, args) = args;
-fun prepare_free_constructors prep_term ((((plugins, discs_sels), raw_case_binding), ctr_specs),
- sel_default_eqs) no_defs_lthy =
+val code_plugin = Plugin_Name.declare_setup @{binding code};
+
+fun prepare_free_constructors prep_plugins prep_term
+ ((((raw_plugins, discs_sels), raw_case_binding), ctr_specs),
+ sel_default_eqs) no_defs_lthy =
let
+ val plugins = prep_plugins no_defs_lthy raw_plugins;
+
+
(* TODO: sanity checks on arguments *)
val raw_ctrs = map ctr_of_ctr_spec ctr_specs;
@@ -1056,24 +1058,27 @@
fun free_constructors tacss = (fn (goalss, after_qed, lthy) =>
map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss
- |> (fn thms => after_qed thms lthy)) oo prepare_free_constructors (K I);
+ |> (fn thms => after_qed thms lthy)) oo prepare_free_constructors (K I) (K I);
val free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
- prepare_free_constructors Syntax.read_term;
+ prepare_free_constructors Plugin_Name.make_filter Syntax.read_term;
val parse_bound_term = Parse.binding --| @{keyword ":"} -- Parse.term;
type ctr_options = (string -> bool) * bool;
+type ctr_options_cmd = (Proof.context -> string -> bool) * bool;
-val default_ctr_options = (K true, false) : ctr_options;
+val default_ctr_options : ctr_options = (K true, false);
+val default_ctr_options_cmd : ctr_options_cmd = (K (K true), false);
val parse_ctr_options =
Scan.optional (@{keyword "("} |-- Parse.list1
- (parse_plugins >> (apfst o K) || Parse.reserved "discs_sels" >> (apsnd o K o K true)) --|
+ (Plugin_Name.parse_filter >> (apfst o K) ||
+ Parse.reserved "discs_sels" >> (apsnd o K o K true)) --|
@{keyword ")"}
- >> (fn fs => fold I fs default_ctr_options))
- default_ctr_options;
+ >> (fn fs => fold I fs default_ctr_options_cmd))
+ default_ctr_options_cmd;
fun parse_ctr_spec parse_ctr parse_arg =
parse_opt_binding_colon -- parse_ctr -- Scan.repeat parse_arg;
@@ -1088,6 +1093,4 @@
-- parse_sel_default_eqs
>> free_constructors_cmd);
-val _ = Theory.setup Ctr_Sugar_Interpretation.init;
-
end;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Mon Oct 13 18:45:48 2014 +0200
@@ -71,7 +71,6 @@
val standard_binding: binding
val parse_binding_colon: binding parser
val parse_opt_binding_colon: binding parser
- val parse_plugins: (string -> bool) parser
val ss_only: thm list -> Proof.context -> Proof.context
@@ -87,18 +86,6 @@
structure Ctr_Sugar_Util : CTR_SUGAR_UTIL =
struct
-fun match_entire_string pat s =
- let
- fun match [] [] = true
- | match [] _ = false
- | match (ps as #"*" :: ps') cs =
- match ps' cs orelse (not (null cs) andalso match ps (tl cs))
- | match _ [] = false
- | match (p :: ps) (c :: cs) = p = c andalso match ps cs;
- in
- match (String.explode pat) (String.explode s)
- end;
-
fun map_prod f g (x, y) = (f x, g y);
fun seq_conds f n k xs =
@@ -262,12 +249,6 @@
val parse_binding_colon = Parse.binding --| @{keyword ":"};
val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
-val parse_plugins =
- Parse.reserved "plugins" |--
- ((Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) --| @{keyword ":"}
- -- Scan.repeat (Parse.short_ident || Parse.string))
- >> (fn (modif, pats) => modif o member (uncurry match_entire_string o swap) pats);
-
fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;
(*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
--- a/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML Mon Oct 13 17:04:25 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-(* Title: HOL/Tools/Ctr_Sugar/local_interpretation.ML
- Author: Jasmin Blanchette, TU Muenchen
-
-Generic interpretation of local theory data -- ad hoc. Based on
-
- Title: Pure/interpretation.ML
- Author: Florian Haftmann and Makarius
-*)
-
-signature LOCAL_INTERPRETATION =
-sig
- type T
- val result: theory -> T list
- val interpretation: string -> (T -> theory -> theory) -> (T -> local_theory -> local_theory) ->
- theory -> theory
- val data: (string -> bool) -> T -> local_theory -> local_theory
- val data_global: (string -> bool) -> T -> theory -> theory
- val init: theory -> theory
-end;
-
-functor Local_Interpretation(type T val eq: T * T -> bool): LOCAL_INTERPRETATION =
-struct
-
-type T = T;
-
-structure Interp = Theory_Data
-(
- type T =
- ((Name_Space.naming * (string -> bool)) * T) list
- * ((((T -> theory -> theory) * (T -> local_theory -> local_theory)) * (string * stamp))
- * ((Name_Space.naming * (string -> bool)) * T) list) list;
- val empty = ([], []);
- val extend = I;
- fun merge ((data1, interps1), (data2, interps2)) : T =
- (Library.merge (eq_snd eq) (data1, data2),
- AList.join (eq_snd (op =)) (K (Library.merge (eq_snd eq))) (interps1, interps2));
-);
-
-val result = map snd o fst o Interp.get;
-
-fun consolidate_common g_or_f lift_lthy thy thy_or_lthy =
- let
- val (data, interps) = Interp.get thy;
-
- fun unfinished_of ((gf, (name, _)), data') =
- (g_or_f gf,
- if eq_list (eq_snd eq) (data', data) then
- []
- else
- subtract (eq_snd eq) data' data
- |> map_filter (fn ((naming, keep), x) => if keep name then SOME (naming, x) else NONE));
-
- val unfinished = map unfinished_of interps;
- val finished = map (apsnd (K data)) interps;
- in
- if forall (null o #2) unfinished then
- NONE
- else
- SOME (thy_or_lthy |> fold_rev (uncurry fold_rev) unfinished
- |> lift_lthy (Interp.put (data, finished)))
- end;
-
-fun consolidate lthy =
- consolidate_common (fn (_, g) => fn (_, x) => g x) Local_Theory.background_theory
- (Proof_Context.theory_of lthy) lthy;
-
-fun consolidate_global thy =
- consolidate_common (fn (f, _) => fn (naming, x) => fn thy =>
- thy |> Sign.map_naming (K naming) |> f x |> Sign.restore_naming thy) I thy thy;
-
-fun interpretation name g f =
- Interp.map (apsnd (cons (((g, f), (name, stamp ())), []))) #> perhaps consolidate_global;
-
-fun data keep x =
- Local_Theory.background_theory
- (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy)
- #> perhaps consolidate;
-
-fun data_global keep x =
- (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy)
- #> perhaps consolidate_global;
-
-val init = Theory.at_begin consolidate_global;
-
-end;
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Mon Oct 13 18:45:48 2014 +0200
@@ -6,7 +6,6 @@
signature LIFTING_BNF =
sig
- val lifting_plugin: string
end
structure Lifting_BNF : LIFTING_BNF =
@@ -16,8 +15,6 @@
open BNF_Def
open Transfer_BNF
-val lifting_plugin = "lifting"
-
(* Quotient map theorem *)
fun Quotient_tac bnf ctxt i =
@@ -120,8 +117,10 @@
lthy |> fold (perhaps o try o (snd oo Local_Theory.notes)) notess
end
-val _ = Theory.setup (bnf_interpretation lifting_plugin
- (bnf_only_type_ctr (BNF_Util.map_local_theory o lifting_bnf_interpretation))
- (bnf_only_type_ctr lifting_bnf_interpretation))
+val lifting_plugin = Plugin_Name.declare_setup @{binding lifting}
+
+val _ =
+ Theory.setup
+ (bnf_interpretation lifting_plugin (bnf_only_type_ctr lifting_bnf_interpretation))
end
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Oct 13 18:45:48 2014 +0200
@@ -6,10 +6,6 @@
signature EXHAUSTIVE_GENERATORS =
sig
- val exhaustive_plugin: string
- val bounded_forall_plugin: string
- val full_exhaustive_plugin: string
-
val compile_generator_expr:
Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
@@ -39,11 +35,6 @@
(* basics *)
-val exhaustive_plugin = "quickcheck_exhaustive"
-val bounded_forall_plugin = "quickcheck_bounded_forall"
-val full_exhaustive_plugin = "quickcheck_full_exhaustive"
-
-
(** dynamic options **)
val smart_quantifier = Attrib.setup_config_bool @{binding quickcheck_smart_quantifier} (K true)
@@ -544,11 +535,11 @@
(* setup *)
val setup_exhaustive_datatype_interpretation =
- Quickcheck_Common.datatype_interpretation exhaustive_plugin
+ Quickcheck_Common.datatype_interpretation @{plugin quickcheck_exhaustive}
(@{sort exhaustive}, instantiate_exhaustive_datatype)
val setup_bounded_forall_datatype_interpretation =
- BNF_LFP_Compat.interpretation bounded_forall_plugin Quickcheck_Common.compat_prefs
+ BNF_LFP_Compat.interpretation @{plugin quickcheck_bounded_forall} Quickcheck_Common.compat_prefs
(Quickcheck_Common.ensure_sort
(((@{sort type}, @{sort type}), @{sort bounded_forall}),
(fn thy => BNF_LFP_Compat.the_descr thy Quickcheck_Common.compat_prefs,
@@ -557,7 +548,7 @@
val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
val setup =
- Quickcheck_Common.datatype_interpretation full_exhaustive_plugin
+ Quickcheck_Common.datatype_interpretation @{plugin quickcheck_full_exhaustive}
(@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
#> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
#> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Oct 13 18:45:48 2014 +0200
@@ -6,7 +6,6 @@
signature NARROWING_GENERATORS =
sig
- val narrowing_plugin: string
val allow_existentials : bool Config.T
val finite_functions : bool Config.T
val overlord : bool Config.T
@@ -23,8 +22,6 @@
structure Narrowing_Generators : NARROWING_GENERATORS =
struct
-val narrowing_plugin = "quickcheck_narrowing"
-
(* configurations *)
val allow_existentials = Attrib.setup_config_bool @{binding quickcheck_allow_existentials} (K true)
@@ -528,7 +525,7 @@
val setup =
Code.datatype_interpretation ensure_partial_term_of
#> Code.datatype_interpretation ensure_partial_term_of_code
- #> Quickcheck_Common.datatype_interpretation narrowing_plugin
+ #> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing}
(@{sort narrowing}, instantiate_narrowing_datatype)
#> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon Oct 13 18:45:48 2014 +0200
@@ -7,7 +7,6 @@
signature RANDOM_GENERATORS =
sig
type seed = Random_Engine.seed
- val random_plugin: string
val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
-> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
-> seed -> (('a -> 'b) * (unit -> term)) * seed
@@ -25,8 +24,6 @@
structure Random_Generators : RANDOM_GENERATORS =
struct
-val random_plugin = "quickcheck_random";
-
(** abstract syntax **)
fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
@@ -473,7 +470,7 @@
val active = Attrib.setup_config_bool @{binding quickcheck_random_active} (K false);
val setup =
- Quickcheck_Common.datatype_interpretation random_plugin
+ Quickcheck_Common.datatype_interpretation @{plugin quickcheck_random}
(@{sort random}, instantiate_random_datatype)
#> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Mon Oct 13 18:45:48 2014 +0200
@@ -6,7 +6,6 @@
signature TRANSFER_BNF =
sig
- val transfer_plugin: string
val base_name_of_bnf: BNF_Def.bnf -> binding
val type_name_of_bnf: BNF_Def.bnf -> string
val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data
@@ -21,8 +20,6 @@
open BNF_FP_Util
open BNF_FP_Def_Sugar
-val transfer_plugin = "transfer"
-
(* util functions *)
fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf))
@@ -282,6 +279,8 @@
(* BNF interpretation *)
+val transfer_plugin = Plugin_Name.declare_setup @{binding transfer}
+
fun transfer_bnf_interpretation bnf lthy =
let
val dead = dead_of_bnf bnf
@@ -294,9 +293,9 @@
|> predicator bnf
end
-val _ = Theory.setup (bnf_interpretation transfer_plugin
- (bnf_only_type_ctr (BNF_Util.map_local_theory o transfer_bnf_interpretation))
- (bnf_only_type_ctr transfer_bnf_interpretation))
+val _ =
+ Theory.setup
+ (bnf_interpretation transfer_plugin (bnf_only_type_ctr transfer_bnf_interpretation))
(* simplification rules for the predicator *)
@@ -370,8 +369,8 @@
snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
end
-val _ = Theory.setup (fp_sugars_interpretation transfer_plugin
- (fp_sugar_only_type_ctr (map_local_theory o fold transfer_fp_sugars_interpretation))
- (fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation)))
+val _ =
+ Theory.setup (fp_sugars_interpretation transfer_plugin
+ (fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation)))
end
--- a/src/HOL/Tools/datatype_realizer.ML Mon Oct 13 17:04:25 2014 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Mon Oct 13 18:45:48 2014 +0200
@@ -7,15 +7,12 @@
signature DATATYPE_REALIZER =
sig
- val extraction_plugin: string
val add_dt_realizers: Old_Datatype_Aux.config -> string list -> theory -> theory
end;
structure Datatype_Realizer : DATATYPE_REALIZER =
struct
-val extraction_plugin = "extraction";
-
fun subsets i j =
if i <= j then
let val is = subsets (i+1) j
@@ -241,6 +238,6 @@
|> fold_rev (perhaps o try o make_casedists) infos
end;
-val _ = Theory.setup (BNF_LFP_Compat.interpretation extraction_plugin [] add_dt_realizers);
+val _ = Theory.setup (BNF_LFP_Compat.interpretation @{plugin extraction} [] add_dt_realizers);
end;