# HG changeset patch
# User blanchet
# Date 1401204762 -7200
# Node ID 589ec121ce1a84d43da3a1b26da1e0fb4937ac13
# Parent  c46fe1cb1d9418d9b9bc8c061aa33b057e4120bb
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it

diff -r c46fe1cb1d94 -r 589ec121ce1a NEWS
--- a/NEWS	Mon May 26 16:58:38 2014 +0200
+++ b/NEWS	Tue May 27 17:32:42 2014 +0200
@@ -319,6 +319,10 @@
   * No discriminators are generated for nullary constructors by default,
     eliminating the need for the odd "=:" syntax.
     INCOMPATIBILITY.
+  * No discriminators or selectors are generated by default by
+    "datatype_new", unless custom names are specified or the new
+    "discs_sels" option is passed.
+    INCOMPATIBILITY.
 
 * Old datatype package:
   * The generated theorems "xxx.cases" and "xxx.recs" have been renamed
diff -r c46fe1cb1d94 -r 589ec121ce1a src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon May 26 16:58:38 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue May 27 17:32:42 2014 +0200
@@ -472,7 +472,7 @@
   @@{command datatype_new} target? @{syntax dt_options}? \<newline>
     (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') + @'and')
   ;
-  @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code') + ',') ')'
+  @{syntax_def dt_options}: '(' (('discs_sels' | 'no_code') + ',') ')'
 \<close>}
 
 \medskip
@@ -491,8 +491,9 @@
 \setlength{\itemsep}{0pt}
 
 \item
-The @{text "no_discs_sels"} option indicates that no discriminators or selectors
-should be generated.
+The @{text "discs_sels"} option indicates that discriminators and selectors
+should be generated. The option is implicitly enabled if names are specified for
+discriminators or selectors.
 
 \item
 The @{text "no_code"} option indicates that the datatype should not be
@@ -1648,8 +1649,9 @@
 
 \noindent
 Definitions of codatatypes have almost exactly the same syntax as for datatypes
-(Section~\ref{ssec:datatype-command-syntax}). The @{text "no_discs_sels"} option
-is not available, because destructors are a crucial notion for codatatypes.
+(Section~\ref{ssec:datatype-command-syntax}). The @{text "discs_sels"} option
+is superfluous because discriminators and selectors are always generated for
+codatatypes.
 *}
 
 
diff -r c46fe1cb1d94 -r 589ec121ce1a src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon May 26 16:58:38 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue May 27 17:32:42 2014 +0200
@@ -829,14 +829,11 @@
   end;
 
 fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
-    (wrap_opts as (no_discs_sels, _), specs) no_defs_lthy0 =
+    ((discs_sels0, no_code), specs) no_defs_lthy0 =
   let
     (* TODO: sanity checks on arguments *)
 
-    val _ = if fp = Greatest_FP andalso no_discs_sels then
-        error "Cannot define codatatypes without discriminators and selectors"
-      else
-        ();
+    val discs_sels = discs_sels0 orelse fp = Greatest_FP;
 
     val nn = length specs;
     val fp_bs = map type_binding_of_spec specs;
@@ -1115,7 +1112,7 @@
             fun ctr_spec_of disc_b ctr0 sel_bs sel_defs = (((disc_b, ctr0), sel_bs), sel_defs);
             val ctr_specs = map4 ctr_spec_of disc_bindings ctrs0 sel_bindingss sel_defaultss;
           in
-            free_constructors tacss ((wrap_opts, standard_binding), ctr_specs) lthy
+            free_constructors tacss (((discs_sels, no_code), standard_binding), ctr_specs) lthy
           end;
 
         fun derive_maps_sets_rels
@@ -1193,22 +1190,26 @@
                     ||>> yield_singleton (mk_Frees "a") TA;
                   val map_term = mk_map_of_bnf Ds As Bs fp_bnf;
                   val discsA = map (mk_disc_or_sel ADs) discs;
+
                   fun is_t_eq_t T t term =
                     let
                       val (head, tail) = Term.strip_comb term;
                     in
                       head aconv HOLogic.eq_const T andalso forall (fn u => u = t) tail
                     end;
+
                   val disc_map_iff_thms =
                     let
                       val discsB = map (mk_disc_or_sel BDs) discs;
                       val discsA_t = map (fn disc1 => Term.betapply (disc1, ta)) discsA;
+
                       fun mk_goal (discA_t, discB) =
-                          if head_of discA_t aconv @{const Not} orelse is_t_eq_t TA ta discA_t then
-                            NONE
-                          else
-                            SOME (mk_Trueprop_eq
-                              (betapply (discB, (Term.list_comb (map_term, fs) $ ta)), discA_t));
+                        if head_of discA_t aconv @{const Not} orelse is_t_eq_t TA ta discA_t then
+                          NONE
+                        else
+                          SOME (mk_Trueprop_eq
+                            (betapply (discB, (Term.list_comb (map_term, fs) $ ta)), discA_t));
+
                       val goals = map_filter mk_goal (discsA_t ~~ discsB);
                     in
                       if null goals then []
@@ -1220,6 +1221,7 @@
                           |> Conjunction.elim_balanced (length goals)
                           |> Proof_Context.export names_lthy lthy
                     end;
+
                   val sel_map_thms =
                     let
                       fun mk_sel_map_goal (discA, selA) =
@@ -1236,11 +1238,10 @@
                             | _ => map_rhs $ (selA $ ta));
                           val conclusion = mk_Trueprop_eq (lhs, rhs);
                         in
-                          if is_t_eq_t TA ta premise then
-                            conclusion
-                          else
-                            Logic.mk_implies (HOLogic.mk_Trueprop premise, conclusion)
+                          if is_t_eq_t TA ta premise then conclusion
+                          else Logic.mk_implies (HOLogic.mk_Trueprop premise, conclusion)
                         end;
+
                       val disc_sel_pairs = flat (map2 (fn disc => fn sels => map (pair disc) sels)
                         discsA (map (map (mk_disc_or_sel ADs)) selss));
                       val goals = map mk_sel_map_goal disc_sel_pairs;
@@ -1258,26 +1259,38 @@
                   (disc_map_iff_thms, sel_map_thms)
                 end;
 
-              val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o
-                binder_types o fastype_of) ctrs;
-              val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets;
-              val setT_names = map (fn T => the_single (Term.add_tfree_namesT T [])) setTs;
-              fun mk_set_empty_goal disc set T = Logic.mk_implies (HOLogic.mk_Trueprop (disc $ u),
-                mk_Trueprop_eq (set $ u, HOLogic.mk_set T []));
-              val goals = map_filter I (flat
-                (map2 (fn names => fn disc =>
-                  map3 (fn name => fn setT => fn set =>
-                    if member (op =) names name then NONE
-                    else SOME (mk_set_empty_goal disc set setT))
-                  setT_names setTs sets)
-                ctr_argT_namess discs));
+              val set_empty_thms =
+                let
+                  val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o
+                    binder_types o fastype_of) ctrs;
+                  val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets;
+                  val setT_names = map (fn T => the_single (Term.add_tfree_namesT T [])) setTs;
+
+                  fun mk_set_empty_goal disc set T =
+                    Logic.mk_implies (HOLogic.mk_Trueprop (disc $ u),
+                      mk_Trueprop_eq (set $ u, HOLogic.mk_set T []));
 
-              val set_empty_thms = if null goals then []
-                else Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
-                  (fn {context = ctxt, prems = _} =>
-                    mk_set_empty_tac ctxt (certify ctxt u) exhaust set_thms (flat disc_thmss))
-                  |> Conjunction.elim_balanced (length goals)
-                  |> Proof_Context.export names_lthy lthy;
+                  val goals =
+                    if null discs then
+                      []
+                    else
+                      map_filter I (flat
+                        (map2 (fn names => fn disc =>
+                          map3 (fn name => fn setT => fn set =>
+                            if member (op =) names name then NONE
+                            else SOME (mk_set_empty_goal disc set setT))
+                          setT_names setTs sets)
+                        ctr_argT_namess discs));
+                in
+                  if null goals then
+                    []
+                  else
+                    Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+                      (fn {context = ctxt, prems = _} =>
+                        mk_set_empty_tac ctxt (certify ctxt u) exhaust set_thms (flat disc_thmss))
+                      |> Conjunction.elim_balanced (length goals)
+                      |> Proof_Context.export names_lthy lthy
+                end;
 
               val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
 
diff -r c46fe1cb1d94 -r 589ec121ce1a src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 26 16:58:38 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue May 27 17:32:42 2014 +0200
@@ -322,7 +322,7 @@
 fun args_of_ctr_spec ((_, args), _) = args;
 fun sel_defaults_of_ctr_spec (_, ds) = ds;
 
-fun prepare_free_constructors prep_term (((no_discs_sels, no_code), raw_case_binding), ctr_specs)
+fun prepare_free_constructors prep_term (((discs_sels, no_code), raw_case_binding), ctr_specs)
     no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
@@ -481,6 +481,11 @@
            if is_disc_binding_valid b then get_udisc b (k - 1) else nth exist_xs_u_eq_ctrs (k - 1)
          end);
 
+    val no_discs_sels =
+      not discs_sels andalso
+      forall (forall Binding.is_empty) (raw_disc_bindings :: raw_sel_bindingss) andalso
+      forall null raw_sel_defaultss;
+
     val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') =
       if no_discs_sels then
         (true, [], [], [], [], [], lthy')
@@ -1010,7 +1015,7 @@
 
 val parse_ctr_options =
   Scan.optional (@{keyword "("} |-- Parse.list1
-        (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
+        (Parse.reserved "discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1) --|
       @{keyword ")"}
       >> (fn js => (member (op =) js 0, member (op =) js 1)))
     (false, false);