698 *} |
698 *} |
699 |
699 |
700 ML {* |
700 ML {* |
701 (* nominal datatype parser *) |
701 (* nominal datatype parser *) |
702 local |
702 local |
703 structure P = Parse; |
|
704 structure S = Scan |
|
705 |
|
706 fun triple1 ((x, y), z) = (x, y, z) |
703 fun triple1 ((x, y), z) = (x, y, z) |
707 fun triple2 ((x, y), z) = (y, x, z) |
704 fun triple2 ((x, y), z) = (y, x, z) |
708 fun tuple2 (((x, y), z), u) = (x, y, u, z) |
705 fun tuple2 (((x, y), z), u) = (x, y, u, z) |
709 fun tuple3 ((x, y), (z, u)) = (x, y, z, u) |
706 fun tuple3 ((x, y), (z, u)) = (x, y, z, u) |
710 in |
707 in |
711 |
708 |
712 val opt_name = Scan.option (P.binding --| Args.colon) |
709 val opt_name = Scan.option (Parse.binding --| Args.colon) |
713 |
710 |
714 val anno_typ = S.option (P.name --| @{keyword "::"}) -- P.typ |
711 val anno_typ = Scan.option (Parse.name --| @{keyword "::"}) -- Parse.typ |
715 |
712 |
716 val bind_mode = @{keyword "binds"} |-- |
713 val bind_mode = @{keyword "binds"} |-- |
717 S.optional (Args.parens |
714 Scan.optional (Args.parens |
718 (Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst |
715 (Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst |
719 |
716 |
720 val bind_clauses = |
717 val bind_clauses = |
721 P.enum "," (bind_mode -- S.repeat1 P.term -- (@{keyword "in"} |-- S.repeat1 P.name) >> triple1) |
718 Parse.enum "," (bind_mode -- Scan.repeat1 Parse.term -- (@{keyword "in"} |-- Scan.repeat1 Parse.name) >> triple1) |
722 |
719 |
723 val cnstr_parser = |
720 val cnstr_parser = |
724 P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tuple2 |
721 Parse.binding -- Scan.repeat anno_typ -- bind_clauses -- Parse.opt_mixfix >> tuple2 |
725 |
722 |
726 (* datatype parser *) |
723 (* datatype parser *) |
727 val dt_parser = |
724 val dt_parser = |
728 (P.type_args_constrained -- P.binding -- P.opt_mixfix >> triple2) -- |
725 (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix >> triple2) -- |
729 (@{keyword "="} |-- P.enum1 "|" cnstr_parser) |
726 (@{keyword "="} |-- Parse.enum1 "|" cnstr_parser) |
730 |
727 |
731 (* binding function parser *) |
728 (* binding function parser *) |
732 val bnfun_parser = |
729 val bnfun_parser = |
733 S.optional (@{keyword "binder"} |-- P.fixes -- Parse_Spec.where_alt_specs) ([], []) |
730 Scan.optional (@{keyword "binder"} |-- Parse.fixes -- Parse_Spec.where_alt_specs) ([], []) |
734 |
731 |
735 (* main parser *) |
732 (* main parser *) |
736 val main_parser = |
733 val main_parser = |
737 opt_name -- P.and_list1 dt_parser -- bnfun_parser >> tuple3 |
734 opt_name -- Parse.and_list1 dt_parser -- bnfun_parser >> tuple3 |
738 |
735 |
739 end |
736 end |
740 |
737 |
741 (* Command Keyword *) |
738 (* Command Keyword *) |
742 val _ = Outer_Syntax.local_theory @{command_spec "nominal_datatype"} |
739 val _ = Outer_Syntax.local_theory @{command_spec "nominal_datatype"} |