9 |
9 |
10 |
10 |
11 ML {* |
11 ML {* |
12 (* nominal datatype parser *) |
12 (* nominal datatype parser *) |
13 local |
13 local |
14 structure P = OuterParse; |
14 structure P = Parse; |
15 structure S = Scan |
15 structure S = Scan |
16 |
16 |
17 fun triple1 ((x, y), z) = (x, y, z) |
17 fun triple1 ((x, y), z) = (x, y, z) |
18 fun triple2 (x, (y, z)) = (x, y, z) |
18 fun triple2 (x, (y, z)) = (x, y, z) |
19 fun tuple ((x, y, z), u) = (x, y, z, u) |
19 fun tuple ((x, y, z), u) = (x, y, z, u) |
20 fun tswap (((x, y), z), u) = (x, y, u, z) |
20 fun tswap (((x, y), z), u) = (x, y, u, z) |
21 in |
21 in |
22 |
22 |
23 val _ = OuterKeyword.keyword "bind" |
23 val _ = Keyword.keyword "bind" |
24 val _ = OuterKeyword.keyword "bind_set" |
24 val _ = Keyword.keyword "bind_set" |
25 val _ = OuterKeyword.keyword "bind_res" |
25 val _ = Keyword.keyword "bind_res" |
26 |
26 |
27 val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ |
27 val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ |
28 |
28 |
29 val bind_mode = P.$$$ "bind" || P.$$$ "bind_set" || P.$$$ "bind_res" |
29 val bind_mode = P.$$$ "bind" || P.$$$ "bind_set" || P.$$$ "bind_res" |
30 |
30 |
39 (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- |
39 (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- |
40 (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple |
40 (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple |
41 |
41 |
42 (* binding function parser *) |
42 (* binding function parser *) |
43 val bnfun_parser = |
43 val bnfun_parser = |
44 S.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([], []) |
44 S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], []) |
45 |
45 |
46 (* main parser *) |
46 (* main parser *) |
47 val main_parser = |
47 val main_parser = |
48 P.and_list1 dt_parser -- bnfun_parser >> triple2 |
48 P.and_list1 dt_parser -- bnfun_parser >> triple2 |
49 |
49 |