# HG changeset patch # User wenzelm # Date 1413218748 -7200 # Node ID 6c9821c32dd57b327fed2ff784978266081cb5ec # Parent 9002fe021e2f89b02254789cb97dfe655a07104c Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings; diff -r 9002fe021e2f -r 6c9821c32dd5 src/Doc/Datatypes/Datatypes.thy --- 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 diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Ctr_Sugar.thy --- 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 @@ "\ Q \ P \ Q \ P \ 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" diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Enum.thy --- 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") diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/HOL.thy --- 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 \Plugin_Name.declare_setup @{binding extraction}\ + +ML \ + 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}; +\ +ML \ + Plugin_Name.define_setup @{binding quickcheck} + [@{plugin quickcheck_exhaustive}, + @{plugin quickcheck_random}, + @{plugin quickcheck_bounded_forall}, + @{plugin quickcheck_full_exhaustive}, + @{plugin quickcheck_narrowing}] +\ + + subsection {* Primitive logic *} subsubsection {* Core syntax *} diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Library/bnf_axiomatization.ML --- 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 -- diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Tools/BNF/bnf_def.ML --- 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; diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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; diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- 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]}; diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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; diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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; diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML --- 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*) diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Tools/Ctr_Sugar/local_interpretation.ML --- 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; diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Tools/Lifting/lifting_bnf.ML --- 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 diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- 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)) diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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))) diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Tools/Quickcheck/random_generators.ML --- 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))); diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Tools/Transfer/transfer_bnf.ML --- 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 diff -r 9002fe021e2f -r 6c9821c32dd5 src/HOL/Tools/datatype_realizer.ML --- 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;