--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 05 00:41:01 2014 +0200
@@ -1166,7 +1166,7 @@
end;
fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
- ((plugins, (discs_sels0, no_code)), specs) no_defs_lthy0 =
+ ((plugins, discs_sels0), specs) no_defs_lthy0 =
let
(* TODO: sanity checks on arguments *)
@@ -1458,8 +1458,8 @@
fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs);
val ctr_specs = map3 ctr_spec_of disc_bindings ctrs0 sel_bindingss;
in
- free_constructors tacss ((((plugins, (discs_sels, no_code)), standard_binding),
- ctr_specs), sel_default_eqs) lthy
+ free_constructors tacss ((((plugins, discs_sels), standard_binding), ctr_specs),
+ sel_default_eqs) lthy
end;
fun derive_maps_sets_rels (ctr_sugar as {casex, case_cong, case_thms, discs, selss, ctrs,
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Sep 05 00:41:01 2014 +0200
@@ -7,7 +7,7 @@
signature BNF_LFP_SIZE =
sig
- val size_interpretation: string
+ 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,7 +22,7 @@
open BNF_Def
open BNF_FP_Def_Sugar
-val size_interpretation = "size"
+val size_plugin = "size"
val size_N = "size_"
@@ -376,7 +376,7 @@
end
| generate_datatype_size _ lthy = lthy;
-val _ = Theory.setup (fp_sugars_interpretation size_interpretation
+val _ = Theory.setup (fp_sugars_interpretation size_plugin
(map_local_theory o generate_datatype_size) generate_datatype_size);
end;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 05 00:41:01 2014 +0200
@@ -7,6 +7,8 @@
signature CTR_SUGAR =
sig
+ val code_plugin: string
+
type ctr_sugar =
{T: typ,
ctrs: term list,
@@ -69,7 +71,7 @@
val ctr_of_ctr_spec: ('c, 'a) ctr_spec -> 'c
val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list
- type ctr_options = (string -> bool) * (bool * bool)
+ type ctr_options = (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 ->
@@ -89,6 +91,8 @@
open Ctr_Sugar_Tactics
open Ctr_Sugar_Code
+val code_plugin = "code"
+
type ctr_sugar =
{T: typ,
ctrs: term list,
@@ -362,8 +366,8 @@
fun ctr_of_ctr_spec ((_, ctr), _) = ctr;
fun args_of_ctr_spec (_, args) = args;
-fun prepare_free_constructors prep_term ((((plugins, (discs_sels, no_code)), raw_case_binding),
- ctr_specs), sel_default_eqs) no_defs_lthy =
+fun prepare_free_constructors prep_term ((((plugins, discs_sels), raw_case_binding), ctr_specs),
+ sel_default_eqs) no_defs_lthy =
let
(* TODO: sanity checks on arguments *)
@@ -1025,7 +1029,7 @@
(fn phi => Case_Translation.register
(Morphism.term phi casex) (map (Morphism.term phi) ctrs))
|> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs])
- |> not no_code ?
+ |> plugins code_plugin ?
Local_Theory.declaration {syntax = false, pervasive = false}
(fn phi => Context.mapping
(add_ctr_code fcT_name (map (Morphism.typ phi) As)
@@ -1064,15 +1068,13 @@
val parse_bound_term = Parse.binding --| @{keyword ":"} -- Parse.term;
-type ctr_options = (string -> bool) * (bool * bool)
+type ctr_options = (string -> bool) * bool
-val default_ctr_options = (K true, (false, false));
+val default_ctr_options = (K true, false);
val parse_ctr_options =
Scan.optional (@{keyword "("} |-- Parse.list1
- (parse_plugins >> (apfst o K)
- || Parse.reserved "discs_sels" >> (apsnd o apfst o K o K true)
- || Parse.reserved "no_code" >> (apsnd o apsnd o K o K true)) --|
+ (parse_plugins >> (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;
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Fri Sep 05 00:41:01 2014 +0200
@@ -6,7 +6,7 @@
signature LIFTING_BNF =
sig
- val lifting_interpretation: string
+ val lifting_plugin: string
end
structure Lifting_BNF : LIFTING_BNF =
@@ -16,7 +16,7 @@
open BNF_Def
open Transfer_BNF
-val lifting_interpretation = "lifting"
+val lifting_plugin = "lifting"
(* Quotient map theorem *)
@@ -118,7 +118,7 @@
snd (Local_Theory.notes notes lthy)
end
-val _ = Theory.setup (bnf_interpretation lifting_interpretation
+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))
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Sep 05 00:41:01 2014 +0200
@@ -6,9 +6,9 @@
signature EXHAUSTIVE_GENERATORS =
sig
- val exhaustive_interpretation: string
- val bounded_forall_interpretation: string
- val full_exhaustive_interpretation: string
+ 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
@@ -39,9 +39,9 @@
(* basics *)
-val exhaustive_interpretation = "exhaustive"
-val bounded_forall_interpretation = "bounded_forall"
-val full_exhaustive_interpretation = "full_exhaustive"
+val exhaustive_plugin = "exhaustive"
+val bounded_forall_plugin = "bounded_forall"
+val full_exhaustive_plugin = "full_exhaustive"
(** dynamic options **)
@@ -543,11 +543,11 @@
(* setup *)
val setup_exhaustive_datatype_interpretation =
- Quickcheck_Common.datatype_interpretation exhaustive_interpretation
+ Quickcheck_Common.datatype_interpretation exhaustive_plugin
(@{sort exhaustive}, instantiate_exhaustive_datatype)
val setup_bounded_forall_datatype_interpretation =
- BNF_LFP_Compat.interpretation bounded_forall_interpretation BNF_LFP_Compat.Keep_Nesting
+ BNF_LFP_Compat.interpretation bounded_forall_plugin BNF_LFP_Compat.Keep_Nesting
(Quickcheck_Common.ensure_sort
(((@{sort type}, @{sort type}), @{sort bounded_forall}),
(fn thy => BNF_LFP_Compat.the_descr thy BNF_LFP_Compat.Keep_Nesting, instantiate_bounded_forall_datatype)))
@@ -555,7 +555,7 @@
val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
val setup =
- Quickcheck_Common.datatype_interpretation full_exhaustive_interpretation
+ Quickcheck_Common.datatype_interpretation full_exhaustive_plugin
(@{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 Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Sep 05 00:41:01 2014 +0200
@@ -6,7 +6,7 @@
signature NARROWING_GENERATORS =
sig
- val narrowing_interpretation: string
+ val narrowing_plugin: string
val allow_existentials : bool Config.T
val finite_functions : bool Config.T
val overlord : bool Config.T
@@ -23,7 +23,7 @@
structure Narrowing_Generators : NARROWING_GENERATORS =
struct
-val narrowing_interpretation = "narrowing"
+val narrowing_plugin = "narrowing"
(* configurations *)
@@ -528,7 +528,7 @@
val setup =
Code.datatype_interpretation ensure_partial_term_of
#> Code.datatype_interpretation ensure_partial_term_of_code
- #> Quickcheck_Common.datatype_interpretation narrowing_interpretation
+ #> Quickcheck_Common.datatype_interpretation narrowing_plugin
(@{sort narrowing}, instantiate_narrowing_datatype)
#> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Sep 05 00:41:01 2014 +0200
@@ -7,7 +7,7 @@
signature RANDOM_GENERATORS =
sig
type seed = Random_Engine.seed
- val random_interpretation: string
+ 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,7 +25,7 @@
structure Random_Generators : RANDOM_GENERATORS =
struct
-val random_interpretation = "random";
+val random_plugin = "random";
(** abstract syntax **)
@@ -474,7 +474,7 @@
val active = Attrib.setup_config_bool @{binding quickcheck_random_active} (K false);
val setup =
- Quickcheck_Common.datatype_interpretation random_interpretation
+ Quickcheck_Common.datatype_interpretation random_plugin
(@{sort random}, instantiate_random_datatype)
#> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Sep 05 00:41:01 2014 +0200
@@ -6,7 +6,7 @@
signature TRANSFER_BNF =
sig
- val transfer_interpretation: string
+ 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,7 +21,7 @@
open BNF_FP_Util
open BNF_FP_Def_Sugar
-val transfer_interpretation = "transfer"
+val transfer_plugin = "transfer"
(* util functions *)
@@ -290,7 +290,7 @@
snd (Local_Theory.notes (constr_notes @ relator_eq_notes @ pred_notes) lthy)
end
-val _ = Theory.setup (bnf_interpretation transfer_interpretation
+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)))
@@ -361,7 +361,7 @@
snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
end
-val _ = Theory.setup (fp_sugars_interpretation transfer_interpretation
+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)))