# HG changeset patch # User blanchet # Date 1366970991 -7200 # Node ID 22517d04d20bdea20850f58c0108e28ad4dc0fe0 # Parent 75b92ff1d8533a79e4bed33a598ea3252b897b05 more intuitive syntax for equality-style discriminators of nullary constructors diff -r 75b92ff1d853 -r 22517d04d20b src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Fri Apr 26 11:04:47 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Fri Apr 26 12:09:51 2013 +0200 @@ -1320,7 +1320,7 @@ val _ = Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type" - ((parse_opt_binding_colon Binding.empty -- Parse.term -- + ((parse_opt_binding_colon -- Parse.term -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Scan.option Parse.term) >> bnf_def_cmd); diff -r 75b92ff1d853 -r 22517d04d20b src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Apr 26 11:04:47 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Apr 26 12:09:51 2013 +0200 @@ -1222,17 +1222,16 @@ @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"}; val parse_type_arg_constrained = - Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort) + Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort); -val parse_type_arg_named_constrained = - parse_opt_binding_colon Binding.empty -- parse_type_arg_constrained +val parse_type_arg_named_constrained = parse_opt_binding_colon -- parse_type_arg_constrained; val parse_type_args_named_constrained = parse_type_arg_constrained >> (single o pair Binding.empty) || @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) || Scan.succeed []; -val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- Parse.binding; +val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- parse_binding; val no_map_rel = (Binding.empty, Binding.empty); @@ -1249,11 +1248,11 @@ Scan.succeed no_map_rel; val parse_ctr_spec = - parse_opt_binding_colon smart_binding -- Parse.binding -- Scan.repeat parse_ctr_arg -- + parse_opt_binding_colon -- parse_binding -- Scan.repeat parse_ctr_arg -- Scan.optional parse_defaults [] -- Parse.opt_mixfix; val parse_spec = - parse_type_args_named_constrained -- Parse.binding -- parse_map_rel_bindings -- + parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings -- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec); val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_spec; diff -r 75b92ff1d853 -r 22517d04d20b src/HOL/BNF/Tools/bnf_util.ML --- a/src/HOL/BNF/Tools/bnf_util.ML Fri Apr 26 11:04:47 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_util.ML Fri Apr 26 12:09:51 2013 +0200 @@ -160,10 +160,10 @@ val certify: Proof.context -> term -> cterm val standard_binding: binding - val smart_binding: binding - val binding_eq: binding * binding -> bool + val equal_binding: binding + val parse_binding: Token.T list -> binding * Token.T list val parse_binding_colon: Token.T list -> binding * Token.T list - val parse_opt_binding_colon: binding -> Token.T list -> binding * Token.T list + val parse_opt_binding_colon: Token.T list -> binding * Token.T list val typedef: binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory @@ -305,16 +305,15 @@ fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt); fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt); -val binding_eq = (op =) o pairself Binding.dest - (* The standard binding stands for a name generated following the canonical convention (e.g. "is_Nil" from "Nil"). The smart binding is either the standard binding or no binding at all, depending on the context. *) val standard_binding = @{binding _}; -val smart_binding = Binding.conceal standard_binding; +val equal_binding = @{binding "="}; -val parse_binding_colon = Parse.binding --| @{keyword ":"}; -val parse_opt_binding_colon = Scan.optional parse_binding_colon; +val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding; +val parse_binding_colon = parse_binding --| @{keyword ":"}; +val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty; (*TODO: is this really different from Typedef.add_typedef_global?*) fun typedef typ set opt_morphs tac lthy = diff -r 75b92ff1d853 -r 22517d04d20b src/HOL/BNF/Tools/bnf_wrap.ML --- a/src/HOL/BNF/Tools/bnf_wrap.ML Fri Apr 26 11:04:47 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_wrap.ML Fri Apr 26 12:09:51 2013 +0200 @@ -157,38 +157,33 @@ val ms = map length ctr_Tss; - val raw_disc_bindings' = pad_list smart_binding n raw_disc_bindings; - - fun can_really_rely_on_disc k = - not (Binding.is_empty (nth raw_disc_bindings' (k - 1))) orelse nth ms (k - 1) = 0; - fun can_rely_on_disc k = - can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2)); - fun can_omit_disc_binding k m = - m = 0 orelse n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k)); + val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings; - fun should_really_rely_on_disc k = - let val b = nth raw_disc_bindings' (k - 1) in - not (Binding.is_empty b orelse binding_eq (b, smart_binding)) - end; - fun should_rely_on_disc k = - should_really_rely_on_disc k orelse (k = 1 andalso not (should_really_rely_on_disc 2)); + fun can_definitely_rely_on_disc k = + not (Binding.is_empty (nth raw_disc_bindings' (k - 1))); + fun can_rely_on_disc k = + can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2)); fun should_omit_disc_binding k = - n = 1 orelse (n = 2 andalso should_rely_on_disc (3 - k)); + n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k)); + + fun is_disc_binding_valid b = + not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding)); val standard_disc_binding = qualify false o Binding.name o prefix isN o base_name_of_ctr; val disc_bindings = raw_disc_bindings' |> map4 (fn k => fn m => fn ctr => fn disc => - Option.map (qualify false) + qualify false (if Binding.is_empty disc then - if can_omit_disc_binding k m then NONE else error "Cannot omit discriminator name" - else if binding_eq (disc, smart_binding) then - if should_omit_disc_binding k then NONE else SOME (standard_disc_binding ctr) - else if binding_eq (disc, standard_binding) then - SOME (standard_disc_binding ctr) + if should_omit_disc_binding k then disc else standard_disc_binding ctr + else if Binding.eq_name (disc, equal_binding) then + if m = 0 then disc + else error "Cannot use \"=\" syntax for discriminating nonnullary constructor" + else if Binding.eq_name (disc, standard_binding) then + standard_disc_binding ctr else - SOME disc)) ks ms ctrs0; + disc)) ks ms ctrs0; fun standard_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr; @@ -196,7 +191,7 @@ pad_list [] n raw_sel_bindingss |> map3 (fn ctr => fn m => map2 (fn l => fn sel => qualify false - (if Binding.is_empty sel orelse binding_eq (sel, standard_binding) then + (if Binding.is_empty sel orelse Binding.eq_name (sel, standard_binding) then standard_sel_binding m l ctr else sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms; @@ -250,9 +245,9 @@ fun alternate_disc_lhs get_udisc k = HOLogic.mk_not - (case nth disc_bindings (k - 1) of - NONE => nth exist_xs_u_eq_ctrs (k - 1) - | SOME b => get_udisc b (k - 1)); + (let val b = nth disc_bindings (k - 1) in + if is_disc_binding_valid b then get_udisc b (k - 1) else nth exist_xs_u_eq_ctrs (k - 1) + end); val (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs, sel_defss, lthy') = @@ -314,18 +309,15 @@ val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = no_defs_lthy - |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_u_eq_ctr => - fn NONE => - if n = 1 then - pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def) - else if n = 2 andalso should_omit_disc_binding k then - pair (alternate_disc k, alternate_disc_no_def) - else if m = 0 then - pair (Term.lambda u exist_xs_u_eq_ctr, refl) - else - raise Fail "missing discriminator" - | SOME b => Specification.definition (SOME (b, NONE, NoSyn), - ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd) + |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_u_eq_ctr => fn b => + if Binding.is_empty b then + if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def) + else pair (alternate_disc k, alternate_disc_no_def) + else if Binding.eq_name (b, equal_binding) then + pair (Term.lambda u exist_xs_u_eq_ctr, refl) + else + Specification.definition (SOME (b, NONE, NoSyn), + ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd) ks ms exist_xs_u_eq_ctrs disc_bindings ||>> apfst split_list o fold_map (fn (b, proto_sels) => Specification.definition (SOME (b, NONE, NoSyn), @@ -493,7 +485,8 @@ map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose end; - val disc_thms = flat (map2 (fn NONE => K [] | SOME _ => I) disc_bindings disc_thmss); + val disc_thms = flat (map2 (fn b => if is_disc_binding_valid b then I else K []) + disc_bindings disc_thmss); val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) = let @@ -694,10 +687,10 @@ fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --| @{keyword "]"}; -val parse_bindings = parse_bracket_list Parse.binding; +val parse_bindings = parse_bracket_list parse_binding; val parse_bindingss = parse_bracket_list parse_bindings; -val parse_bound_term = (Parse.binding --| @{keyword ":"}) -- Parse.term; +val parse_bound_term = (parse_binding --| @{keyword ":"}) -- Parse.term; val parse_bound_terms = parse_bracket_list parse_bound_term; val parse_bound_termss = parse_bracket_list parse_bound_terms;