137 \end;\n\ |
137 \end;\n\ |
138 \val dummy = Addsimps " ^ tname ^ ".simps;\n"); |
138 \val dummy = Addsimps " ^ tname ^ ".simps;\n"); |
139 |
139 |
140 (*parsers*) |
140 (*parsers*) |
141 val tvars = type_args >> map (cat "dtVar"); |
141 val tvars = type_args >> map (cat "dtVar"); |
|
142 |
|
143 val simple_typ = ident >> (cat "dtTyp" o curry mk_pair "[]" o quote) || |
|
144 type_var >> cat "dtVar"; |
|
145 |
142 fun complex_typ toks = |
146 fun complex_typ toks = |
143 (("(" $$-- complex_typ --$$ ")" >> (fn x => [x]) || tvars) |
147 let val typ = simple_typ || "(" $$-- complex_typ --$$ ")"; |
144 -- (ident>>quote) >> (cat "dtTyp" o mk_pair o apfst mk_list) |
148 val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")"; |
145 || type_var >> cat "dtVar") toks; |
149 in |
146 val simple_typ = ident>>(cat "dtTyp" o curry mk_pair "[]" o quote) || |
150 (typ -- repeat (ident>>quote) >> |
147 type_var >> cat "dtVar"; |
151 (foldl (fn (x,y) => "dtTyp " ^ mk_pair (brackets x, y))) || |
|
152 "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 (ident>>quote)) >> |
|
153 (fn (fst, ids) => foldl (fn (x,y) => "dtTyp " ^ |
|
154 mk_pair (brackets x, y)) (commas fst, ids))) toks |
|
155 end; |
|
156 |
148 val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")")); |
157 val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")")); |
149 val constructor = name -- opt_typs -- opt_mixfix; |
158 val constructor = name -- opt_typs -- opt_mixfix; |
150 in |
159 in |
151 val datatype_decl = |
160 val datatype_decl = |
152 (* FIXME tvars -> type_args *) |
|
153 tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params; |
161 tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params; |
154 end; |
162 end; |
155 |
163 |
156 |
164 |
157 |
165 |