1 theory Nominal2 |
1 theory Nominal2 |
2 imports |
2 imports |
3 Nominal2_Base Nominal2_Abs Nominal2_FCB |
3 Nominal2_Base Nominal2_Abs Nominal2_FCB |
|
4 keywords |
|
5 "nominal_datatype" :: thy_decl and |
|
6 "nominal_primrec" "nominal_inductive" :: thy_goal and |
|
7 "avoids" "binds" |
4 uses ("nominal_dt_rawfuns.ML") |
8 uses ("nominal_dt_rawfuns.ML") |
5 ("nominal_dt_alpha.ML") |
9 ("nominal_dt_alpha.ML") |
6 ("nominal_dt_quot.ML") |
10 ("nominal_dt_quot.ML") |
7 ("nominal_induct.ML") |
11 ("nominal_induct.ML") |
8 ("nominal_inductive.ML") |
12 ("nominal_inductive.ML") |
708 |
712 |
709 val _ = Keyword.keyword "binds" |
713 val _ = Keyword.keyword "binds" |
710 |
714 |
711 val opt_name = Scan.option (P.binding --| Args.colon) |
715 val opt_name = Scan.option (P.binding --| Args.colon) |
712 |
716 |
713 val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ |
717 val anno_typ = S.option (P.name --| @{keyword "::"}) -- P.typ |
714 |
718 |
715 val bind_mode = P.$$$ "binds" |-- |
719 val bind_mode = @{keyword "binds"} |-- |
716 S.optional (Args.parens |
720 S.optional (Args.parens |
717 (Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst |
721 (Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst |
718 |
722 |
719 val bind_clauses = |
723 val bind_clauses = |
720 P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1) |
724 P.enum "," (bind_mode -- S.repeat1 P.term -- (@{keyword "in"} |-- S.repeat1 P.name) >> triple1) |
721 |
725 |
722 val cnstr_parser = |
726 val cnstr_parser = |
723 P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tuple2 |
727 P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tuple2 |
724 |
728 |
725 (* datatype parser *) |
729 (* datatype parser *) |
726 val dt_parser = |
730 val dt_parser = |
727 (P.type_args_constrained -- P.binding -- P.opt_mixfix >> triple2) -- |
731 (P.type_args_constrained -- P.binding -- P.opt_mixfix >> triple2) -- |
728 (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) |
732 (@{keyword "="} |-- P.enum1 "|" cnstr_parser) |
729 |
733 |
730 (* binding function parser *) |
734 (* binding function parser *) |
731 val bnfun_parser = |
735 val bnfun_parser = |
732 S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], []) |
736 S.optional (@{keyword "binder"} |-- P.fixes -- Parse_Spec.where_alt_specs) ([], []) |
733 |
737 |
734 (* main parser *) |
738 (* main parser *) |
735 val main_parser = |
739 val main_parser = |
736 opt_name -- P.and_list1 dt_parser -- bnfun_parser >> tuple3 |
740 opt_name -- P.and_list1 dt_parser -- bnfun_parser >> tuple3 |
737 |
741 |