5 "Perm" "Equivp" "Rsp" "Lift" |
5 "Perm" "Equivp" "Rsp" "Lift" |
6 begin |
6 begin |
7 |
7 |
8 section{* Interface for nominal_datatype *} |
8 section{* Interface for nominal_datatype *} |
9 |
9 |
10 text {* |
|
11 |
|
12 Nominal-Datatype-part: |
|
13 |
|
14 |
|
15 1nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list |
|
16 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
|
17 type(s) to be defined constructors list |
|
18 (ty args, name, syn) (name, typs, syn) |
|
19 |
|
20 Binder-Function-part: |
|
21 |
|
22 2rd Arg: (binding * typ option * mixfix) list |
|
23 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
|
24 binding function(s) |
|
25 to be defined |
|
26 (name, type, syn) |
|
27 |
|
28 3th Arg: term list |
|
29 ^^^^^^^^^ |
|
30 the equations of the binding functions |
|
31 (Trueprop equations) |
|
32 *} |
|
33 |
|
34 text {*****************************************************} |
|
35 ML {* OuterParse.triple2 *} |
|
36 |
10 |
37 ML {* |
11 ML {* |
38 (* nominal datatype parser *) |
12 (* nominal datatype parser *) |
39 local |
13 local |
40 structure P = OuterParse; |
14 structure P = OuterParse; |
48 |
22 |
49 val _ = OuterKeyword.keyword "bind" |
23 val _ = OuterKeyword.keyword "bind" |
50 val _ = OuterKeyword.keyword "bind_set" |
24 val _ = OuterKeyword.keyword "bind_set" |
51 val _ = OuterKeyword.keyword "bind_res" |
25 val _ = OuterKeyword.keyword "bind_res" |
52 |
26 |
53 val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ |
27 val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ |
54 |
28 |
55 val bind_mode = P.$$$ "bind" || P.$$$ "bind_set" || P.$$$ "bind_res" |
29 val bind_mode = P.$$$ "bind" || P.$$$ "bind_set" || P.$$$ "bind_res" |
56 |
30 |
57 val bind_clauses = |
31 val bind_clauses = |
58 P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1) |
32 P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1) |
59 |
33 |
60 val cnstr_parser = |
34 val cnstr_parser = |
61 P.binding -- Scan.repeat anno_typ |
35 P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap |
62 |
36 |
63 (* datatype parser *) |
37 (* datatype parser *) |
64 val dt_parser = |
38 val dt_parser = |
65 (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- |
39 (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- |
66 (P.$$$ "=" |-- P.enum1 "|" (cnstr_parser -- bind_clauses -- P.opt_mixfix >> tswap)) >> tuple |
40 (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple |
67 |
41 |
68 (* binding function parser *) |
42 (* binding function parser *) |
69 val bnfun_parser = |
43 val bnfun_parser = |
70 Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[]) |
44 S.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[]) |
71 |
45 |
72 (* main parser *) |
46 (* main parser *) |
73 val main_parser = |
47 val main_parser = |
74 (P.and_list1 dt_parser) -- bnfun_parser >> triple2 |
48 (P.and_list1 dt_parser) -- bnfun_parser >> triple2 |
75 |
49 |
183 |
157 |
184 fun rawify_bclause (BEmy n) = BEmy n |
158 fun rawify_bclause (BEmy n) = BEmy n |
185 | rawify_bclause (BLst (bnds, bdys)) = BLst (rawify_bnds bnds, bdys) |
159 | rawify_bclause (BLst (bnds, bdys)) = BLst (rawify_bnds bnds, bdys) |
186 | rawify_bclause (BSet (bnds, bdys)) = BSet (rawify_bnds bnds, bdys) |
160 | rawify_bclause (BSet (bnds, bdys)) = BSet (rawify_bnds bnds, bdys) |
187 | rawify_bclause (BRes (bnds, bdys)) = BRes (rawify_bnds bnds, bdys) |
161 | rawify_bclause (BRes (bnds, bdys)) = BRes (rawify_bnds bnds, bdys) |
188 |
|
189 in |
162 in |
190 map (map (map rawify_bclause)) bclauses |
163 map (map (map rawify_bclause)) bclauses |
191 end |
164 end |
192 *} |
165 *} |
193 |
166 |