don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
--- 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
--- 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.
*}
--- 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);
--- 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);