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