--- a/src/Doc/Datatypes/Datatypes.thy Tue Jun 10 11:38:53 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Jun 10 12:16:22 2014 +0200
@@ -375,8 +375,10 @@
context early begin
(*>*)
datatype_new (set: 'a) list (map: map rel: list_all2) =
- null: Nil (defaults tl: Nil)
+ null: Nil
| Cons (hd: 'a) (tl: "'a list")
+ where
+ "tl Nil = Nil"
text {*
\noindent
@@ -415,10 +417,10 @@
The discriminator associated with @{const Cons} is simply
@{term "\<lambda>xs. \<not> null xs"}.
-The @{text defaults} clause following the @{const Nil} constructor specifies a
-default value for selectors associated with other constructors. Here, it is used
-to ensure that the tail of the empty list is itself (instead of being left
-unspecified).
+The \keyw{where} clause at the end of the command specifies a default value for
+selectors applied to constructors on which they are not a priori specified.
+Here, it is used to ensure that the tail of the empty list is itself (instead of
+being left unspecified).
Because @{const Nil} is nullary, it is also possible to use
@{term "\<lambda>xs. xs = Nil"} as a discriminator. This is the default behavior
@@ -470,7 +472,8 @@
@{rail \<open>
@@{command datatype_new} target? @{syntax dt_options}? \<newline>
- (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') + @'and')
+ (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') + @'and') \<newline>
+ (@'where' (@{syntax prop} + '|'))?
;
@{syntax_def dt_options}: '(' (('discs_sels' | 'no_code') + ',') ')'
\<close>}
@@ -482,7 +485,8 @@
datatypes specified by their constructors.
The syntactic entity \synt{target} can be used to specify a local
-context---e.g., @{text "(in linorder)"} \cite{isabelle-isar-ref}.
+context (e.g., @{text "(in linorder)"} \cite{isabelle-isar-ref}),
+and \synt{prop} denotes a HOL proposition.
The optional target is optionally followed by one or both of the following
options:
@@ -500,6 +504,11 @@
registered for code generation.
\end{itemize}
+The optional \keyw{where} clause specifies default values for selectors.
+Each proposition must be an equation of the form
+@{text "un_D (C \<dots>) = \<dots>"}, where @{text C} is a constructor and
+@{text un_D} is a selector.
+
The left-hand sides of the datatype equations specify the name of the type to
define, its type parameters, and additional information:
@@ -531,8 +540,7 @@
mention exactly the same type variables in the same order.
@{rail \<open>
- @{syntax_def dt_ctor}: (name ':')? name (@{syntax dt_ctor_arg} * ) \<newline>
- @{syntax dt_sel_defaults}? mixfix?
+ @{syntax_def dt_ctor}: (name ':')? name (@{syntax dt_ctor_arg} * ) mixfix?
\<close>}
\medskip
@@ -557,21 +565,6 @@
name for the corresponding selector to override the default name
(@{text un_C\<^sub>ji}). The same selector names can be reused for several
constructors as long as they share the same type.
-
-@{rail \<open>
- @{syntax_def dt_sel_defaults}: '(' 'defaults' (name ':' term +) ')'
-\<close>}
-
-\medskip
-
-\noindent
-Given a constructor
-@{text "C \<Colon> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<sigma>"},
-default values can be specified for any selector
-@{text "un_D \<Colon> \<sigma> \<Rightarrow> \<tau>"}
-associated with other constructors. The specified default value must be of type
-@{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<tau>"}
-(i.e., it may depend on @{text C}'s arguments).
*}
@@ -1485,13 +1478,19 @@
The following example illustrates this procedure:
*}
+(*<*)
+ hide_const termi
+(*>*)
consts termi\<^sub>0 :: 'a
text {* \blankline *}
datatype_new ('a, 'b) tlist =
- TNil (termi: 'b) (defaults ttl: TNil)
- | TCons (thd: 'a) (ttl : "('a, 'b) tlist") (defaults termi: "\<lambda>_ xs. termi\<^sub>0 xs")
+ TNil (termi: 'b)
+ | TCons (thd: 'a) (ttl: "('a, 'b) tlist")
+ where
+ "ttl (TNil y) = TNil y"
+ | "termi (TCons _ xs) = termi\<^sub>0 xs"
text {* \blankline *}
@@ -1557,8 +1556,10 @@
*}
codatatype (lset: 'a) llist (map: lmap rel: llist_all2) =
- lnull: LNil (defaults ltl: LNil)
+ lnull: LNil
| LCons (lhd: 'a) (ltl: "'a llist")
+ where
+ "ltl LNil = LNil"
text {*
\noindent
@@ -2646,10 +2647,10 @@
@{rail \<open>
@@{command free_constructors} target? @{syntax dt_options} \<newline>
- name 'for' (@{syntax fc_ctor} + '|')
+ name 'for' (@{syntax fc_ctor} + '|') \<newline>
+ (@'where' (@{syntax prop} + '|'))?
;
- @{syntax_def fc_ctor}: (name ':')? term (name * ) \<newline>
- @{syntax dt_sel_defaults}?
+ @{syntax_def fc_ctor}: (name ':')? term (name * )
\<close>}
\medskip
@@ -2661,8 +2662,8 @@
that is queried by various tools (e.g., \keyw{function}).
The syntactic entity \synt{target} can be used to specify a local context,
-\synt{name} denotes an identifier, and \synt{term} denotes a HOL term
-\cite{isabelle-isar-ref}.
+\synt{name} denotes an identifier, \synt{prop} denotes a HOL proposition, and
+\synt{term} denotes a HOL term \cite{isabelle-isar-ref}.
The syntax resembles that of @{command datatype_new} and @{command codatatype}
definitions (Sections
--- a/src/HOL/BNF_Examples/ListF.thy Tue Jun 10 11:38:53 2014 +0200
+++ b/src/HOL/BNF_Examples/ListF.thy Tue Jun 10 12:16:22 2014 +0200
@@ -13,7 +13,10 @@
begin
datatype_new 'a listF (map: mapF rel: relF) =
- NilF (defaults tlF: NilF) | Conss (hdF: 'a) (tlF: "'a listF")
+ NilF
+ | Conss (hdF: 'a) (tlF: "'a listF")
+where
+ "tlF NilF = NilF"
datatype_compat listF
--- a/src/HOL/List.thy Tue Jun 10 11:38:53 2014 +0200
+++ b/src/HOL/List.thy Tue Jun 10 12:16:22 2014 +0200
@@ -9,8 +9,10 @@
begin
datatype_new (set: 'a) list (map: map rel: list_all2) =
- Nil (defaults tl: "[]") ("[]")
+ Nil ("[]")
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
+where
+ "tl [] = []"
datatype_compat list
--- a/src/HOL/Nat.thy Tue Jun 10 11:38:53 2014 +0200
+++ b/src/HOL/Nat.thy Tue Jun 10 12:16:22 2014 +0200
@@ -83,8 +83,10 @@
done
free_constructors case_nat for
- "0 \<Colon> nat" (defaults pred: "0 \<Colon> nat")
+ "0 \<Colon> nat"
| Suc pred
+where
+ "pred (0 \<Colon> nat) = (0 \<Colon> nat)"
apply atomize_elim
apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jun 10 11:38:53 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Jun 10 12:16:22 2014 +0200
@@ -67,15 +67,13 @@
thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list ->
thm list -> (thm list -> thm list) -> Proof.context -> gfp_sugar_thms
- type co_datatype_spec =
- ((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
- * ((binding, binding * typ, term) Ctr_Sugar.ctr_spec * mixfix) list
-
val co_datatypes: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
BNF_FP_Util.fp_result * local_theory) ->
- (bool * bool) * co_datatype_spec list ->
+ (bool * bool)
+ * ((((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
+ * ((binding, binding * typ) Ctr_Sugar.ctr_spec * mixfix) list) * term list) list ->
local_theory -> local_theory
val parse_co_datatype_cmd: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
@@ -250,15 +248,16 @@
handle THM _ => thm;
type co_datatype_spec =
- ((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
- * ((binding, binding * typ, term) ctr_spec * mixfix) list;
+ (((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
+ * ((binding, binding * typ) ctr_spec * mixfix) list) * term list;
-fun type_args_named_constrained_of_spec ((((ncAs, _), _), _), _) = ncAs;
-fun type_binding_of_spec ((((_, b), _), _), _) = b;
-fun map_binding_of_spec (((_, (b, _)), _), _) = b;
-fun rel_binding_of_spec (((_, (_, b)), _), _) = b;
-fun mixfix_of_spec ((_, mx), _) = mx;
-fun mixfixed_ctr_specs_of_spec (_, mx_ctr_specs) = mx_ctr_specs;
+fun type_args_named_constrained_of_spec (((((ncAs, _), _), _), _), _) = ncAs;
+fun type_binding_of_spec (((((_, b), _), _), _), _) = b;
+fun map_binding_of_spec ((((_, (b, _)), _), _), _) = b;
+fun rel_binding_of_spec ((((_, (_, b)), _), _), _) = b;
+fun mixfix_of_spec (((_, mx), _), _) = mx;
+fun mixfixed_ctr_specs_of_spec ((_, mx_ctr_specs), _) = mx_ctr_specs;
+fun sel_default_eqs_of_spec (_, ts) = ts;
fun add_nesty_bnf_names Us =
let
@@ -900,7 +899,7 @@
val sel_bindingsss = map (map (map fst)) ctr_argsss;
val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
- val raw_sel_defaultsss = map (map sel_defaults_of_ctr_spec) ctr_specss;
+ val raw_sel_default_eqss = map sel_default_eqs_of_spec specs;
val (As :: _) :: fake_ctr_Tsss =
burrow (burrow (Syntax.check_typs fake_lthy)) (Ass0 :: fake_ctr_Tsss0);
@@ -1038,7 +1037,7 @@
xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), abs),
abs_inject), abs_inverse), type_definition), ctr_bindings), ctr_mixfixes), ctr_Tss),
- disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
+ disc_bindings), sel_bindingss), raw_sel_default_eqs) no_defs_lthy =
let
val fp_b_name = Binding.name_of fp_b;
@@ -1110,12 +1109,13 @@
val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss;
- val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss
+ val sel_default_eqs = map (prepare_term lthy) raw_sel_default_eqs;
- 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;
+ fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs);
+ val ctr_specs = map3 ctr_spec_of disc_bindings ctrs0 sel_bindingss;
in
- free_constructors tacss (((discs_sels, no_code), standard_binding), ctr_specs) lthy
+ free_constructors tacss ((((discs_sels, no_code), standard_binding), ctr_specs),
+ sel_default_eqs) lthy
end;
fun derive_maps_sets_rels (ctr_sugar as {case_cong, discs, selss, ctrs, exhaust, disc_thmss,
@@ -1525,7 +1525,7 @@
xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~
pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ kss ~~ mss ~~
abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~
- ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
+ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_default_eqss)
|> wrap_types_etc
|> case_fp fp derive_note_induct_recs_thms_for_types
derive_note_coinduct_corecs_thms_for_types;
@@ -1550,7 +1550,7 @@
val parse_spec =
parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings --
- Parse.opt_mixfix -- (@{keyword "="} |-- parse_ctr_specs);
+ Parse.opt_mixfix -- (@{keyword "="} |-- parse_ctr_specs) -- parse_sel_default_eqs;
val parse_co_datatype = parse_ctr_options -- Parse.and_list1 parse_spec;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Jun 10 11:38:53 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Jun 10 12:16:22 2014 +0200
@@ -56,19 +56,19 @@
val dest_case: Proof.context -> string -> typ list -> term ->
(ctr_sugar * term list * term list) option
- type ('c, 'a, 'v) ctr_spec = ((binding * 'c) * 'a list) * (binding * 'v) list
+ type ('c, 'a) ctr_spec = (binding * 'c) * 'a list
- val disc_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> binding
- val ctr_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> 'c
- val args_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> 'a list
- val sel_defaults_of_ctr_spec: ('c, 'a, 'v) ctr_spec -> (binding * 'v) list
+ val disc_of_ctr_spec: ('c, 'a) ctr_spec -> binding
+ val ctr_of_ctr_spec: ('c, 'a) ctr_spec -> 'c
+ val args_of_ctr_spec: ('c, 'a) ctr_spec -> 'a list
val free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
- ((bool * bool) * binding) * (term, binding, term) ctr_spec list -> local_theory ->
+ (((bool * bool) * binding) * (term, binding) ctr_spec list) * term list -> local_theory ->
ctr_sugar * local_theory
val parse_bound_term: (binding * string) parser
val parse_ctr_options: (bool * bool) parser
- val parse_ctr_spec: 'c parser -> 'a parser -> ('c, 'a, string) ctr_spec parser
+ val parse_ctr_spec: 'c parser -> 'a parser -> ('c, 'a) ctr_spec parser
+ val parse_sel_default_eqs: string list parser
end;
structure Ctr_Sugar : CTR_SUGAR =
@@ -313,24 +313,43 @@
| _ => NONE)
| _ => NONE);
-fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
+fun const_or_free_name (Const (s, _)) = Long_Name.base_name s
+ | const_or_free_name (Free (s, _)) = s
+ | const_or_free_name t = raise TERM ("const_or_free_name", [t])
-type ('c, 'a, 'v) ctr_spec = ((binding * 'c) * 'a list) * (binding * 'v) list;
+fun extract_sel_default ctxt t =
+ let
+ fun malformed () =
+ error ("Malformed selector default value equation: " ^ Syntax.string_of_term ctxt t);
-fun disc_of_ctr_spec (((disc, _), _), _) = disc;
-fun ctr_of_ctr_spec (((_, ctr), _), _) = ctr;
-fun args_of_ctr_spec ((_, args), _) = args;
-fun sel_defaults_of_ctr_spec (_, ds) = ds;
+ val ((sel, (ctr, vars)), rhs) =
+ fst (Term.replace_dummy_patterns (Syntax.check_term ctxt t) 0)
+ |> HOLogic.dest_eq
+ |>> (Term.dest_comb
+ #>> const_or_free_name
+ ##> (Term.strip_comb #>> (Term.dest_Const #> fst)))
+ handle TERM _ => malformed ();
+ in
+ if forall (is_Free orf is_Var) vars andalso not (has_duplicates (op aconv) vars) then
+ ((ctr, sel), fold_rev Term.lambda vars rhs)
+ else
+ malformed ()
+ end;
-fun prepare_free_constructors prep_term (((discs_sels, no_code), raw_case_binding), ctr_specs)
- no_defs_lthy =
+type ('c, 'a) ctr_spec = (binding * 'c) * 'a list;
+
+fun disc_of_ctr_spec ((disc, _), _) = disc;
+fun ctr_of_ctr_spec ((_, ctr), _) = ctr;
+fun args_of_ctr_spec (_, args) = args;
+
+fun prepare_free_constructors prep_term
+ ((((discs_sels, no_code), raw_case_binding), ctr_specs), sel_default_eqs) no_defs_lthy =
let
(* TODO: sanity checks on arguments *)
val raw_ctrs = map ctr_of_ctr_spec ctr_specs;
val raw_disc_bindings = map disc_of_ctr_spec ctr_specs;
val raw_sel_bindingss = map args_of_ctr_spec ctr_specs;
- val raw_sel_defaultss = map sel_defaults_of_ctr_spec ctr_specs;
val n = length raw_ctrs;
val ks = 1 upto n;
@@ -338,7 +357,6 @@
val _ = if n > 0 then () else error "No constructors specified";
val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
- val sel_defaultss = map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss;
val Type (fcT_name, As0) = body_type (fastype_of (hd ctrs0));
val fc_b_name = Long_Name.base_name fcT_name;
@@ -424,8 +442,8 @@
(* TODO: Eta-expension is for compatibility with the old datatype package (but it also provides
nicer names). Consider removing. *)
- val eta_fs = map2 eta_expand_arg xss xfs;
- val eta_gs = map2 eta_expand_arg xss xgs;
+ val eta_fs = map2 (fold_rev Term.lambda) xss xfs;
+ val eta_gs = map2 (fold_rev Term.lambda) xss xgs;
val case_binding =
qualify false
@@ -484,13 +502,38 @@
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;
+ null sel_default_eqs;
val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') =
if no_discs_sels then
(true, [], [], [], [], [], lthy')
else
let
+ val sel_bindings = flat sel_bindingss;
+ val uniq_sel_bindings = distinct Binding.eq_name sel_bindings;
+ val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings);
+
+ val sel_binding_index =
+ if all_sels_distinct then 1 upto length sel_bindings
+ else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings;
+
+ val all_proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss);
+ val sel_infos =
+ AList.group (op =) (sel_binding_index ~~ all_proto_sels)
+ |> sort (int_ord o pairself fst)
+ |> map snd |> curry (op ~~) uniq_sel_bindings;
+ val sel_bindings = map fst sel_infos;
+ val sel_Ts = map (curry (op -->) fcT o fastype_of o snd o snd o hd o snd) sel_infos;
+
+ val sel_default_lthy = no_defs_lthy
+ |> Proof_Context.allow_dummies
+ |> Proof_Context.add_fixes
+ (map2 (fn b => fn T => (b, SOME T, NoSyn)) sel_bindings sel_Ts)
+ |> snd;
+
+ val sel_defaults =
+ map (extract_sel_default sel_default_lthy o prep_term sel_default_lthy) sel_default_eqs;
+
fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT);
fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr);
@@ -499,48 +542,33 @@
Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
fun mk_sel_case_args b proto_sels T =
- map2 (fn Ts => fn k =>
+ map3 (fn Const (c, _) => fn Ts => fn k =>
(case AList.lookup (op =) proto_sels k of
NONE =>
- (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
- NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
- | SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term lthy)
- | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
+ (case filter (curry (op =) (c, Binding.name_of b) o fst) sel_defaults of
+ [] => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
+ | [(_, t)] => t
+ | _ => error "Multiple default values for selector/constructor pair")
+ | SOME (xs, x) => fold_rev Term.lambda xs x)) ctrs ctr_Tss ks;
fun sel_spec b proto_sels =
let
val _ =
(case duplicates (op =) (map fst proto_sels) of
k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^
- " for constructor " ^
- quote (Syntax.string_of_term lthy (nth ctrs (k - 1))))
+ " for constructor " ^ quote (Syntax.string_of_term lthy (nth ctrs (k - 1))))
| [] => ())
val T =
(case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of
[T] => T
| T :: T' :: _ => error ("Inconsistent range type for selector " ^
- quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ lthy T) ^ " vs. "
- ^ quote (Syntax.string_of_typ lthy T')));
+ quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ lthy T) ^
+ " vs. " ^ quote (Syntax.string_of_typ lthy T')));
in
mk_Trueprop_eq (Free (Binding.name_of b, fcT --> T) $ u,
Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u)
end;
- val sel_bindings = flat sel_bindingss;
- val uniq_sel_bindings = distinct Binding.eq_name sel_bindings;
- val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings);
-
- val sel_binding_index =
- if all_sels_distinct then 1 upto length sel_bindings
- else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings;
-
- val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss);
- val sel_infos =
- AList.group (op =) (sel_binding_index ~~ proto_sels)
- |> sort (int_ord o pairself fst)
- |> map snd |> curry (op ~~) uniq_sel_bindings;
- val sel_bindings = map fst sel_infos;
-
fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss;
val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
@@ -733,7 +761,7 @@
| _ => false);
val all_sel_thms =
- (if all_sels_distinct andalso forall null sel_defaultss then
+ (if all_sels_distinct andalso null sel_default_eqs then
flat sel_thmss
else
map_product (fn s => fn (xs', c) => make_sel_thm xs' c s) sel_defs
@@ -1020,19 +1048,17 @@
>> (fn js => (member (op =) js 0, member (op =) js 1)))
(false, false);
-val parse_defaults =
- @{keyword "("} |-- Parse.reserved "defaults" |-- Scan.repeat parse_bound_term --| @{keyword ")"};
-
fun parse_ctr_spec parse_ctr parse_arg =
- parse_opt_binding_colon -- parse_ctr -- Scan.repeat parse_arg --
- Scan.optional parse_defaults [];
+ parse_opt_binding_colon -- parse_ctr -- Scan.repeat parse_arg;
val parse_ctr_specs = Parse.enum1 "|" (parse_ctr_spec Parse.term Parse.binding);
+val parse_sel_default_eqs = Scan.optional (@{keyword "where"} |-- Parse.enum1 "|" Parse.prop) [];
val _ =
Outer_Syntax.local_theory_to_proof @{command_spec "free_constructors"}
"register an existing freely generated type's constructors"
(parse_ctr_options -- Parse.binding --| @{keyword "for"} -- parse_ctr_specs
+ -- parse_sel_default_eqs
>> free_constructors_cmd);
val _ = Context.>> (Context.map_theory Ctr_Sugar_Interpretation.init);