# HG changeset patch
# User blanchet
# Date 1409870461 -7200
# Node ID b3c71d630777c6a93913d5ebe78e1baf3da62db8
# Parent  89034dc402476e2e7e8b8ddeb8dc722fc37fa1d8
pretend code generation is a ctr_sugar plugin

diff -r 89034dc40247 -r b3c71d630777 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- 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,
diff -r 89034dc40247 -r b3c71d630777 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- 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;
diff -r 89034dc40247 -r b3c71d630777 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- 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;
diff -r 89034dc40247 -r b3c71d630777 src/HOL/Tools/Lifting/lifting_bnf.ML
--- 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))
 
diff -r 89034dc40247 -r b3c71d630777 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- 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))
diff -r 89034dc40247 -r b3c71d630777 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- 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)))
     
diff -r 89034dc40247 -r b3c71d630777 src/HOL/Tools/Quickcheck/random_generators.ML
--- 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)));
 
diff -r 89034dc40247 -r b3c71d630777 src/HOL/Tools/Transfer/transfer_bnf.ML
--- 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)))