don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
authorblanchet
Tue May 27 17:32:42 2014 +0200 (2014-05-27)
changeset 57094589ec121ce1a
parent 57093 c46fe1cb1d94
child 57095 001ec97c3e59
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
NEWS
src/Doc/Datatypes/Datatypes.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/NEWS	Mon May 26 16:58:38 2014 +0200
     1.2 +++ b/NEWS	Tue May 27 17:32:42 2014 +0200
     1.3 @@ -319,6 +319,10 @@
     1.4    * No discriminators are generated for nullary constructors by default,
     1.5      eliminating the need for the odd "=:" syntax.
     1.6      INCOMPATIBILITY.
     1.7 +  * No discriminators or selectors are generated by default by
     1.8 +    "datatype_new", unless custom names are specified or the new
     1.9 +    "discs_sels" option is passed.
    1.10 +    INCOMPATIBILITY.
    1.11  
    1.12  * Old datatype package:
    1.13    * The generated theorems "xxx.cases" and "xxx.recs" have been renamed
     2.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon May 26 16:58:38 2014 +0200
     2.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Tue May 27 17:32:42 2014 +0200
     2.3 @@ -472,7 +472,7 @@
     2.4    @@{command datatype_new} target? @{syntax dt_options}? \<newline>
     2.5      (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') + @'and')
     2.6    ;
     2.7 -  @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code') + ',') ')'
     2.8 +  @{syntax_def dt_options}: '(' (('discs_sels' | 'no_code') + ',') ')'
     2.9  \<close>}
    2.10  
    2.11  \medskip
    2.12 @@ -491,8 +491,9 @@
    2.13  \setlength{\itemsep}{0pt}
    2.14  
    2.15  \item
    2.16 -The @{text "no_discs_sels"} option indicates that no discriminators or selectors
    2.17 -should be generated.
    2.18 +The @{text "discs_sels"} option indicates that discriminators and selectors
    2.19 +should be generated. The option is implicitly enabled if names are specified for
    2.20 +discriminators or selectors.
    2.21  
    2.22  \item
    2.23  The @{text "no_code"} option indicates that the datatype should not be
    2.24 @@ -1648,8 +1649,9 @@
    2.25  
    2.26  \noindent
    2.27  Definitions of codatatypes have almost exactly the same syntax as for datatypes
    2.28 -(Section~\ref{ssec:datatype-command-syntax}). The @{text "no_discs_sels"} option
    2.29 -is not available, because destructors are a crucial notion for codatatypes.
    2.30 +(Section~\ref{ssec:datatype-command-syntax}). The @{text "discs_sels"} option
    2.31 +is superfluous because discriminators and selectors are always generated for
    2.32 +codatatypes.
    2.33  *}
    2.34  
    2.35  
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon May 26 16:58:38 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue May 27 17:32:42 2014 +0200
     3.3 @@ -829,14 +829,11 @@
     3.4    end;
     3.5  
     3.6  fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
     3.7 -    (wrap_opts as (no_discs_sels, _), specs) no_defs_lthy0 =
     3.8 +    ((discs_sels0, no_code), specs) no_defs_lthy0 =
     3.9    let
    3.10      (* TODO: sanity checks on arguments *)
    3.11  
    3.12 -    val _ = if fp = Greatest_FP andalso no_discs_sels then
    3.13 -        error "Cannot define codatatypes without discriminators and selectors"
    3.14 -      else
    3.15 -        ();
    3.16 +    val discs_sels = discs_sels0 orelse fp = Greatest_FP;
    3.17  
    3.18      val nn = length specs;
    3.19      val fp_bs = map type_binding_of_spec specs;
    3.20 @@ -1115,7 +1112,7 @@
    3.21              fun ctr_spec_of disc_b ctr0 sel_bs sel_defs = (((disc_b, ctr0), sel_bs), sel_defs);
    3.22              val ctr_specs = map4 ctr_spec_of disc_bindings ctrs0 sel_bindingss sel_defaultss;
    3.23            in
    3.24 -            free_constructors tacss ((wrap_opts, standard_binding), ctr_specs) lthy
    3.25 +            free_constructors tacss (((discs_sels, no_code), standard_binding), ctr_specs) lthy
    3.26            end;
    3.27  
    3.28          fun derive_maps_sets_rels
    3.29 @@ -1193,22 +1190,26 @@
    3.30                      ||>> yield_singleton (mk_Frees "a") TA;
    3.31                    val map_term = mk_map_of_bnf Ds As Bs fp_bnf;
    3.32                    val discsA = map (mk_disc_or_sel ADs) discs;
    3.33 +
    3.34                    fun is_t_eq_t T t term =
    3.35                      let
    3.36                        val (head, tail) = Term.strip_comb term;
    3.37                      in
    3.38                        head aconv HOLogic.eq_const T andalso forall (fn u => u = t) tail
    3.39                      end;
    3.40 +
    3.41                    val disc_map_iff_thms =
    3.42                      let
    3.43                        val discsB = map (mk_disc_or_sel BDs) discs;
    3.44                        val discsA_t = map (fn disc1 => Term.betapply (disc1, ta)) discsA;
    3.45 +
    3.46                        fun mk_goal (discA_t, discB) =
    3.47 -                          if head_of discA_t aconv @{const Not} orelse is_t_eq_t TA ta discA_t then
    3.48 -                            NONE
    3.49 -                          else
    3.50 -                            SOME (mk_Trueprop_eq
    3.51 -                              (betapply (discB, (Term.list_comb (map_term, fs) $ ta)), discA_t));
    3.52 +                        if head_of discA_t aconv @{const Not} orelse is_t_eq_t TA ta discA_t then
    3.53 +                          NONE
    3.54 +                        else
    3.55 +                          SOME (mk_Trueprop_eq
    3.56 +                            (betapply (discB, (Term.list_comb (map_term, fs) $ ta)), discA_t));
    3.57 +
    3.58                        val goals = map_filter mk_goal (discsA_t ~~ discsB);
    3.59                      in
    3.60                        if null goals then []
    3.61 @@ -1220,6 +1221,7 @@
    3.62                            |> Conjunction.elim_balanced (length goals)
    3.63                            |> Proof_Context.export names_lthy lthy
    3.64                      end;
    3.65 +
    3.66                    val sel_map_thms =
    3.67                      let
    3.68                        fun mk_sel_map_goal (discA, selA) =
    3.69 @@ -1236,11 +1238,10 @@
    3.70                              | _ => map_rhs $ (selA $ ta));
    3.71                            val conclusion = mk_Trueprop_eq (lhs, rhs);
    3.72                          in
    3.73 -                          if is_t_eq_t TA ta premise then
    3.74 -                            conclusion
    3.75 -                          else
    3.76 -                            Logic.mk_implies (HOLogic.mk_Trueprop premise, conclusion)
    3.77 +                          if is_t_eq_t TA ta premise then conclusion
    3.78 +                          else Logic.mk_implies (HOLogic.mk_Trueprop premise, conclusion)
    3.79                          end;
    3.80 +
    3.81                        val disc_sel_pairs = flat (map2 (fn disc => fn sels => map (pair disc) sels)
    3.82                          discsA (map (map (mk_disc_or_sel ADs)) selss));
    3.83                        val goals = map mk_sel_map_goal disc_sel_pairs;
    3.84 @@ -1258,26 +1259,38 @@
    3.85                    (disc_map_iff_thms, sel_map_thms)
    3.86                  end;
    3.87  
    3.88 -              val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o
    3.89 -                binder_types o fastype_of) ctrs;
    3.90 -              val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets;
    3.91 -              val setT_names = map (fn T => the_single (Term.add_tfree_namesT T [])) setTs;
    3.92 -              fun mk_set_empty_goal disc set T = Logic.mk_implies (HOLogic.mk_Trueprop (disc $ u),
    3.93 -                mk_Trueprop_eq (set $ u, HOLogic.mk_set T []));
    3.94 -              val goals = map_filter I (flat
    3.95 -                (map2 (fn names => fn disc =>
    3.96 -                  map3 (fn name => fn setT => fn set =>
    3.97 -                    if member (op =) names name then NONE
    3.98 -                    else SOME (mk_set_empty_goal disc set setT))
    3.99 -                  setT_names setTs sets)
   3.100 -                ctr_argT_namess discs));
   3.101 +              val set_empty_thms =
   3.102 +                let
   3.103 +                  val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o
   3.104 +                    binder_types o fastype_of) ctrs;
   3.105 +                  val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets;
   3.106 +                  val setT_names = map (fn T => the_single (Term.add_tfree_namesT T [])) setTs;
   3.107 +
   3.108 +                  fun mk_set_empty_goal disc set T =
   3.109 +                    Logic.mk_implies (HOLogic.mk_Trueprop (disc $ u),
   3.110 +                      mk_Trueprop_eq (set $ u, HOLogic.mk_set T []));
   3.111  
   3.112 -              val set_empty_thms = if null goals then []
   3.113 -                else Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
   3.114 -                  (fn {context = ctxt, prems = _} =>
   3.115 -                    mk_set_empty_tac ctxt (certify ctxt u) exhaust set_thms (flat disc_thmss))
   3.116 -                  |> Conjunction.elim_balanced (length goals)
   3.117 -                  |> Proof_Context.export names_lthy lthy;
   3.118 +                  val goals =
   3.119 +                    if null discs then
   3.120 +                      []
   3.121 +                    else
   3.122 +                      map_filter I (flat
   3.123 +                        (map2 (fn names => fn disc =>
   3.124 +                          map3 (fn name => fn setT => fn set =>
   3.125 +                            if member (op =) names name then NONE
   3.126 +                            else SOME (mk_set_empty_goal disc set setT))
   3.127 +                          setT_names setTs sets)
   3.128 +                        ctr_argT_namess discs));
   3.129 +                in
   3.130 +                  if null goals then
   3.131 +                    []
   3.132 +                  else
   3.133 +                    Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
   3.134 +                      (fn {context = ctxt, prems = _} =>
   3.135 +                        mk_set_empty_tac ctxt (certify ctxt u) exhaust set_thms (flat disc_thmss))
   3.136 +                      |> Conjunction.elim_balanced (length goals)
   3.137 +                      |> Proof_Context.export names_lthy lthy
   3.138 +                end;
   3.139  
   3.140                val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
   3.141  
     4.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 26 16:58:38 2014 +0200
     4.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue May 27 17:32:42 2014 +0200
     4.3 @@ -322,7 +322,7 @@
     4.4  fun args_of_ctr_spec ((_, args), _) = args;
     4.5  fun sel_defaults_of_ctr_spec (_, ds) = ds;
     4.6  
     4.7 -fun prepare_free_constructors prep_term (((no_discs_sels, no_code), raw_case_binding), ctr_specs)
     4.8 +fun prepare_free_constructors prep_term (((discs_sels, no_code), raw_case_binding), ctr_specs)
     4.9      no_defs_lthy =
    4.10    let
    4.11      (* TODO: sanity checks on arguments *)
    4.12 @@ -481,6 +481,11 @@
    4.13             if is_disc_binding_valid b then get_udisc b (k - 1) else nth exist_xs_u_eq_ctrs (k - 1)
    4.14           end);
    4.15  
    4.16 +    val no_discs_sels =
    4.17 +      not discs_sels andalso
    4.18 +      forall (forall Binding.is_empty) (raw_disc_bindings :: raw_sel_bindingss) andalso
    4.19 +      forall null raw_sel_defaultss;
    4.20 +
    4.21      val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') =
    4.22        if no_discs_sels then
    4.23          (true, [], [], [], [], [], lthy')
    4.24 @@ -1010,7 +1015,7 @@
    4.25  
    4.26  val parse_ctr_options =
    4.27    Scan.optional (@{keyword "("} |-- Parse.list1
    4.28 -        (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
    4.29 +        (Parse.reserved "discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
    4.30        @{keyword ")"}
    4.31        >> (fn js => (member (op =) js 0, member (op =) js 1)))
    4.32      (false, false);