# HG changeset patch
# User blanchet
# Date 1386012714 -3600
# Node ID 8a5e82425e557af26956f22882c8082e53f94b82
# Parent  f312a035d0cffa1fc376e212767009c7078aa9c5
added 'no_code' option

diff -r f312a035d0cf -r 8a5e82425e55 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Dec 02 20:31:54 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Dec 02 20:31:54 2013 +0100
@@ -460,7 +460,7 @@
   @@{command datatype_new} target? @{syntax dt_options}? \\
     (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
   ;
-  @{syntax_def dt_options}: '(' (('no_discs_sels' | 'rep_compat') + ',') ')'
+  @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code' | 'rep_compat') + ',') ')'
 "}
 
 The syntactic entity \synt{target} can be used to specify a local
@@ -477,6 +477,10 @@
 should be generated.
 
 \item
+The @{text "no_code"} option indicates that the datatype should not be
+registered for code generation.
+
+\item
 The @{text "rep_compat"} option indicates that the generated names should
 contain optional (and normally not displayed) ``@{text "new."}'' components to
 prevent clashes with a later call to \keyw{rep\_datatype}. See
@@ -2387,7 +2391,7 @@
 %    old \keyw{datatype}
 %
 %  * @{command wrap_free_constructors}
-%    * @{text "no_discs_sels"}, @{text "rep_compat"}
+%    * @{text "no_discs_sels"}, @{text "no_code"}, @{text "rep_compat"}
 %    * hack to have both co and nonco view via locale (cf. ext nats)
 %  * code generator
 %     * eq, refl, simps
@@ -2423,7 +2427,7 @@
   X_list: '[' (X + ',') ']'
 "}
 
-% options: no_discs_sels rep_compat
+% options: no_discs_sels no_code rep_compat
 
 \noindent
 Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
diff -r f312a035d0cf -r 8a5e82425e55 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Dec 02 20:31:54 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Dec 02 20:31:54 2013 +0100
@@ -95,8 +95,8 @@
   val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
       binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
-    (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
-      ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
+    (bool * (bool * bool)) * (((((binding * (typ * sort)) list * binding) * (binding * binding))
+      * mixfix) * ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
         mixfix) list) list ->
     local_theory -> local_theory
   val parse_co_datatype_cmd: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
@@ -975,7 +975,7 @@
   end;
 
 fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
-    (wrap_opts as (no_discs_sels, rep_compat), specs) no_defs_lthy0 =
+    (wrap_opts as (no_discs_sels, (_, rep_compat)), specs) no_defs_lthy0 =
   let
     (* TODO: sanity checks on arguments *)
 
diff -r f312a035d0cf -r 8a5e82425e55 src/HOL/Ctr_Sugar.thy
--- a/src/HOL/Ctr_Sugar.thy	Mon Dec 02 20:31:54 2013 +0100
+++ b/src/HOL/Ctr_Sugar.thy	Mon Dec 02 20:31:54 2013 +0100
@@ -11,9 +11,7 @@
 imports HOL
 keywords
   "print_case_translations" :: diag and
-  "wrap_free_constructors" :: thy_goal and
-  "no_discs_sels" and
-  "rep_compat"
+  "wrap_free_constructors" :: thy_goal
 begin
 
 consts
diff -r f312a035d0cf -r 8a5e82425e55 src/HOL/Tools/ctr_sugar.ML
--- a/src/HOL/Tools/ctr_sugar.ML	Mon Dec 02 20:31:54 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar.ML	Mon Dec 02 20:31:54 2013 +0100
@@ -54,10 +54,10 @@
   val dest_case: Proof.context -> string -> typ list -> term -> (term list * term list) option
 
   val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
-    (((bool * bool) * term list) * binding) *
+    (((bool * (bool * bool)) * term list) * binding) *
       (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
     ctr_sugar * local_theory
-  val parse_wrap_free_constructors_options: (bool * bool) parser
+  val parse_wrap_free_constructors_options: (bool * (bool * bool)) parser
   val parse_bound_term: (binding * string) parser
 end;
 
@@ -286,7 +286,7 @@
 
 fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
 
-fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, rep_compat), raw_ctrs),
+fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, (no_code, rep_compat)), raw_ctrs),
     raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
@@ -931,7 +931,7 @@
                  (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
          |> Local_Theory.notes (anonymous_notes @ notes) |> snd
          |> register_ctr_sugar fcT_name ctr_sugar
-         |> null (Thm.hyps_of (hd case_thms))
+         |> (not no_code andalso null (Thm.hyps_of (hd case_thms)))
            ? Local_Theory.background_theory
              (add_ctr_code fcT_name As (map dest_Const ctrs) inject_thms distinct_thms case_thms))
       end;
@@ -957,9 +957,11 @@
 val parse_bound_termss = parse_bracket_list parse_bound_terms;
 
 val parse_wrap_free_constructors_options =
-  Scan.optional (@{keyword "("} |-- Parse.list1 ((@{keyword "no_discs_sels"} >> K (true, false)) ||
-      (@{keyword "rep_compat"} >> K (false, true))) --| @{keyword ")"}
-    >> (pairself (exists I) o split_list)) (false, false);
+  Scan.optional (@{keyword "("} |-- Parse.list1
+        (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1 ||
+         Parse.reserved "rep_compat" >> K 2) --| @{keyword ")"}
+      >> (fn js => (member (op =) js 0, (member (op =) js 1, member (op =) js 2))))
+    (false, (false, false));
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}