added 'no_code' option
authorblanchet
Mon Dec 02 20:31:54 2013 +0100 (2013-12-02)
changeset 546268a5e82425e55
parent 54625 f312a035d0cf
child 54627 8dd1a354ee86
added 'no_code' option
src/Doc/Datatypes/Datatypes.thy
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/Ctr_Sugar.thy
src/HOL/Tools/ctr_sugar.ML
     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"}