1.1 --- a/src/Doc/Datatypes/Datatypes.thy Mon Dec 02 20:31:54 2013 +0100
1.2 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Dec 02 20:31:54 2013 +0100
1.3 @@ -460,7 +460,7 @@
1.4 @@{command datatype_new} target? @{syntax dt_options}? \\
1.5 (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
1.6 ;
1.7 - @{syntax_def dt_options}: '(' (('no_discs_sels' | 'rep_compat') + ',') ')'
1.8 + @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code' | 'rep_compat') + ',') ')'
1.9 "}
1.10
1.11 The syntactic entity \synt{target} can be used to specify a local
1.12 @@ -477,6 +477,10 @@
1.13 should be generated.
1.14
1.15 \item
1.16 +The @{text "no_code"} option indicates that the datatype should not be
1.17 +registered for code generation.
1.18 +
1.19 +\item
1.20 The @{text "rep_compat"} option indicates that the generated names should
1.21 contain optional (and normally not displayed) ``@{text "new."}'' components to
1.22 prevent clashes with a later call to \keyw{rep\_datatype}. See
1.23 @@ -2387,7 +2391,7 @@
1.24 % old \keyw{datatype}
1.25 %
1.26 % * @{command wrap_free_constructors}
1.27 -% * @{text "no_discs_sels"}, @{text "rep_compat"}
1.28 +% * @{text "no_discs_sels"}, @{text "no_code"}, @{text "rep_compat"}
1.29 % * hack to have both co and nonco view via locale (cf. ext nats)
1.30 % * code generator
1.31 % * eq, refl, simps
1.32 @@ -2423,7 +2427,7 @@
1.33 X_list: '[' (X + ',') ']'
1.34 "}
1.35
1.36 -% options: no_discs_sels rep_compat
1.37 +% options: no_discs_sels no_code rep_compat
1.38
1.39 \noindent
1.40 Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
2.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Dec 02 20:31:54 2013 +0100
2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Dec 02 20:31:54 2013 +0100
2.3 @@ -95,8 +95,8 @@
2.4 val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
2.5 binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
2.6 BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) ->
2.7 - (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
2.8 - ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
2.9 + (bool * (bool * bool)) * (((((binding * (typ * sort)) list * binding) * (binding * binding))
2.10 + * mixfix) * ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
2.11 mixfix) list) list ->
2.12 local_theory -> local_theory
2.13 val parse_co_datatype_cmd: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
2.14 @@ -975,7 +975,7 @@
2.15 end;
2.16
2.17 fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
2.18 - (wrap_opts as (no_discs_sels, rep_compat), specs) no_defs_lthy0 =
2.19 + (wrap_opts as (no_discs_sels, (_, rep_compat)), specs) no_defs_lthy0 =
2.20 let
2.21 (* TODO: sanity checks on arguments *)
2.22
3.1 --- a/src/HOL/Ctr_Sugar.thy Mon Dec 02 20:31:54 2013 +0100
3.2 +++ b/src/HOL/Ctr_Sugar.thy Mon Dec 02 20:31:54 2013 +0100
3.3 @@ -11,9 +11,7 @@
3.4 imports HOL
3.5 keywords
3.6 "print_case_translations" :: diag and
3.7 - "wrap_free_constructors" :: thy_goal and
3.8 - "no_discs_sels" and
3.9 - "rep_compat"
3.10 + "wrap_free_constructors" :: thy_goal
3.11 begin
3.12
3.13 consts
4.1 --- a/src/HOL/Tools/ctr_sugar.ML Mon Dec 02 20:31:54 2013 +0100
4.2 +++ b/src/HOL/Tools/ctr_sugar.ML Mon Dec 02 20:31:54 2013 +0100
4.3 @@ -54,10 +54,10 @@
4.4 val dest_case: Proof.context -> string -> typ list -> term -> (term list * term list) option
4.5
4.6 val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
4.7 - (((bool * bool) * term list) * binding) *
4.8 + (((bool * (bool * bool)) * term list) * binding) *
4.9 (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
4.10 ctr_sugar * local_theory
4.11 - val parse_wrap_free_constructors_options: (bool * bool) parser
4.12 + val parse_wrap_free_constructors_options: (bool * (bool * bool)) parser
4.13 val parse_bound_term: (binding * string) parser
4.14 end;
4.15
4.16 @@ -286,7 +286,7 @@
4.17
4.18 fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
4.19
4.20 -fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, rep_compat), raw_ctrs),
4.21 +fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, (no_code, rep_compat)), raw_ctrs),
4.22 raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
4.23 let
4.24 (* TODO: sanity checks on arguments *)
4.25 @@ -931,7 +931,7 @@
4.26 (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
4.27 |> Local_Theory.notes (anonymous_notes @ notes) |> snd
4.28 |> register_ctr_sugar fcT_name ctr_sugar
4.29 - |> null (Thm.hyps_of (hd case_thms))
4.30 + |> (not no_code andalso null (Thm.hyps_of (hd case_thms)))
4.31 ? Local_Theory.background_theory
4.32 (add_ctr_code fcT_name As (map dest_Const ctrs) inject_thms distinct_thms case_thms))
4.33 end;
4.34 @@ -957,9 +957,11 @@
4.35 val parse_bound_termss = parse_bracket_list parse_bound_terms;
4.36
4.37 val parse_wrap_free_constructors_options =
4.38 - Scan.optional (@{keyword "("} |-- Parse.list1 ((@{keyword "no_discs_sels"} >> K (true, false)) ||
4.39 - (@{keyword "rep_compat"} >> K (false, true))) --| @{keyword ")"}
4.40 - >> (pairself (exists I) o split_list)) (false, false);
4.41 + Scan.optional (@{keyword "("} |-- Parse.list1
4.42 + (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1 ||
4.43 + Parse.reserved "rep_compat" >> K 2) --| @{keyword ")"}
4.44 + >> (fn js => (member (op =) js 0, (member (op =) js 1, member (op =) js 2))))
4.45 + (false, (false, false));
4.46
4.47 val _ =
4.48 Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}