# HG changeset patch # User blanchet # Date 1402395382 -7200 # Node ID aab87ffa60cc8a78e758b1c35f8ccb7e30082554 # Parent 472360558b225a8ab6bfc3d82b77ef253f4a887a use 'where' clause for selector default value syntax diff -r 472360558b22 -r aab87ffa60cc src/Doc/Datatypes/Datatypes.thy --- 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 "\xs. \ 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 "\xs. xs = Nil"} as a discriminator. This is the default behavior @@ -470,7 +472,8 @@ @{rail \ @@{command datatype_new} target? @{syntax dt_options}? \ - (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') + @'and') + (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') + @'and') \ + (@'where' (@{syntax prop} + '|'))? ; @{syntax_def dt_options}: '(' (('discs_sels' | 'no_code') + ',') ')' \} @@ -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 \) = \"}, 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 \ - @{syntax_def dt_ctor}: (name ':')? name (@{syntax dt_ctor_arg} * ) \ - @{syntax dt_sel_defaults}? mixfix? + @{syntax_def dt_ctor}: (name ':')? name (@{syntax dt_ctor_arg} * ) mixfix? \} \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 \ - @{syntax_def dt_sel_defaults}: '(' 'defaults' (name ':' term +) ')' -\} - -\medskip - -\noindent -Given a constructor -@{text "C \ \\<^sub>1 \ \ \ \\<^sub>p \ \"}, -default values can be specified for any selector -@{text "un_D \ \ \ \"} -associated with other constructors. The specified default value must be of type -@{text "\\<^sub>1 \ \ \ \\<^sub>p \ \"} -(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: "\_ 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 \ @@{command free_constructors} target? @{syntax dt_options} \ - name 'for' (@{syntax fc_ctor} + '|') + name 'for' (@{syntax fc_ctor} + '|') \ + (@'where' (@{syntax prop} + '|'))? ; - @{syntax_def fc_ctor}: (name ':')? term (name * ) \ - @{syntax dt_sel_defaults}? + @{syntax_def fc_ctor}: (name ':')? term (name * ) \} \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 diff -r 472360558b22 -r aab87ffa60cc src/HOL/BNF_Examples/ListF.thy --- 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 diff -r 472360558b22 -r aab87ffa60cc src/HOL/List.thy --- 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 diff -r 472360558b22 -r aab87ffa60cc src/HOL/Nat.thy --- 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 \ nat" (defaults pred: "0 \ nat") + "0 \ nat" | Suc pred +where + "pred (0 \ nat) = (0 \ 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 diff -r 472360558b22 -r aab87ffa60cc src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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; diff -r 472360558b22 -r aab87ffa60cc src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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);