1 (* Title: Pure/Tools/codegen_serializer.ML |
1 (* Title: Pure/Tools/codegen_serializer.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Florian Haftmann, TU Muenchen |
3 Author: Florian Haftmann, TU Muenchen |
4 |
4 |
5 Serializer from intermediate language ("Thin-gol") to |
5 Serializer from intermediate language ("Thin-gol") to |
6 target languages (like ML or Haskell) |
6 target languages (like ML or Haskell). |
7 *) |
7 *) |
8 |
8 |
9 signature CODEGEN_SERIALIZER = |
9 signature CODEGEN_SERIALIZER = |
10 sig |
10 sig |
11 val bot: unit; |
11 type primitives; |
|
12 val empty_prims: primitives; |
|
13 val add_prim: string * (string * string list) -> primitives -> primitives; |
|
14 val merge_prims: primitives * primitives -> primitives; |
|
15 val has_prim: primitives -> string -> bool; |
|
16 val mk_prims: primitives -> string; |
|
17 |
|
18 type 'a pretty_syntax = string -> Pretty.T list -> ('a -> Pretty.T) |
|
19 -> (string list * Pretty.T) option; |
|
20 type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax |
|
21 -> primitives -> CodegenThingol.module -> Pretty.T; |
|
22 |
|
23 val ml_from_thingol: string list list -> string -> serializer; |
12 end; |
24 end; |
13 |
25 |
14 structure CodegenSerializer: CODEGEN_SERIALIZER = |
26 structure CodegenSerializer: CODEGEN_SERIALIZER = |
15 struct |
27 struct |
16 |
28 |
17 val bot = (); |
29 open CodegenThingol; |
18 |
30 |
19 end; (* structure *) |
31 |
|
32 (** target language primitives **) |
|
33 |
|
34 type primitives = string Graph.T; |
|
35 |
|
36 val empty_prims = Graph.empty; |
|
37 |
|
38 fun add_prim (f, (def, deps)) prims = |
|
39 prims |
|
40 |> Graph.new_node (f, def) |
|
41 |> fold (fn dep => Graph.add_edge (f, dep)) deps; |
|
42 |
|
43 val merge_prims = Graph.merge (op =) : primitives * primitives -> primitives; |
|
44 |
|
45 val has_prim : primitives -> string -> bool = can o Graph.get_node; |
|
46 |
|
47 fun get_prims prims defs = |
|
48 defs |
|
49 |> filter (can (Graph.get_node prims)) |
|
50 |> `I |
|
51 ||> Graph.all_succs prims |
|
52 ||> (fn gr => Graph.subgraph gr prims) |
|
53 ||> Graph.strong_conn |
|
54 ||> rev |
|
55 ||> Library.flat |
|
56 ||> map (Graph.get_node prims) |
|
57 ||> separate "" |
|
58 ||> cat_lines |
|
59 ||> suffix "\n"; |
|
60 |
|
61 fun mk_prims prims = get_prims prims (Graph.keys prims) |> snd; |
|
62 |
|
63 |
|
64 (** generic serialization **) |
|
65 |
|
66 type 'a pretty_syntax = string -> Pretty.T list -> ('a -> Pretty.T) |
|
67 -> (string list * Pretty.T) option; |
|
68 type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax |
|
69 -> primitives -> CodegenThingol.module -> Pretty.T; |
|
70 |
|
71 datatype lrx = L | R | X; |
|
72 |
|
73 datatype brack = |
|
74 BR |
|
75 | NOBR |
|
76 | INFX of (int * lrx); |
|
77 |
|
78 fun eval_lrx L L = false |
|
79 | eval_lrx R R = false |
|
80 | eval_lrx _ _ = true; |
|
81 |
|
82 fun eval_br BR _ = true |
|
83 | eval_br NOBR _ = false |
|
84 | eval_br (INFX (pr1, lr1)) (INFX (pr2, lr2)) = |
|
85 pr1 > pr2 |
|
86 orelse pr1 = pr2 |
|
87 andalso eval_lrx lr1 lr2 |
|
88 | eval_br (INFX _) _ = false; |
|
89 |
|
90 fun eval_br_postfix BR _ = false |
|
91 | eval_br_postfix NOBR _ = false |
|
92 | eval_br_postfix (INFX (pr1, lr1)) (INFX (pr2, lr2)) = |
|
93 pr1 > pr2 |
|
94 orelse pr1 = pr2 |
|
95 andalso eval_lrx lr1 lr2 |
|
96 | eval_br_postfix (INFX _) _ = false; |
|
97 |
|
98 fun brackify _ [p] = p |
|
99 | brackify true (ps as _::_) = Pretty.enclose "(" ")" (Pretty.breaks ps) |
|
100 | brackify false (ps as _::_) = Pretty.block (Pretty.breaks ps); |
|
101 |
|
102 fun postify [] f = [f] |
|
103 | postify [p] f = [p, Pretty.brk 1, f] |
|
104 | postify (ps as _::_) f = [Pretty.list "(" ")" ps, Pretty.brk 1, f]; |
|
105 |
|
106 fun praetify [] f = [f] |
|
107 | praetify [p] f = [f, Pretty.str " of ", p] |
|
108 |
|
109 |
|
110 (** ML serializer **) |
|
111 |
|
112 local |
|
113 |
|
114 fun ml_validator prims name = |
|
115 let |
|
116 fun replace_invalid c = |
|
117 if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'" |
|
118 andalso not (NameSpace.separator = c) |
|
119 then c |
|
120 else "_" |
|
121 fun suffix_it name = |
|
122 name |
|
123 |> member (op =) ThmDatabase.ml_reserved ? suffix "'" |
|
124 |> member (op =) CodegenThingol.prims ? suffix "'" |
|
125 |> has_prim prims ? suffix "'" |
|
126 |> (fn name' => if name = name' then name else suffix_it name') |
|
127 in |
|
128 name |
|
129 |> translate_string replace_invalid |
|
130 |> suffix_it |
|
131 |> (fn name' => if name = name' then NONE else SOME name') |
|
132 end; |
|
133 |
|
134 val ml_label_uniq = translate_string (fn "'" => "''" | "." => "'" | c => c); |
|
135 |
|
136 fun ml_from_defs styco sconst resolv ds = |
|
137 let |
|
138 fun chunk_defs ps = |
|
139 let |
|
140 val (p_init, p_last) = split_last ps |
|
141 in |
|
142 Pretty.chunks (p_init @ [Pretty.block ([p_last, Pretty.str ";"])]) |
|
143 end; |
|
144 fun ml_from_typ br (IType ("Pair", [t1, t2])) = |
|
145 brackify (eval_br_postfix br (INFX (2, L))) [ |
|
146 ml_from_typ (INFX (2, X)) t1, |
|
147 Pretty.str "*", |
|
148 ml_from_typ (INFX (2, X)) t2 |
|
149 ] |
|
150 | ml_from_typ br (IType ("Bool", [])) = |
|
151 Pretty.str "bool" |
|
152 | ml_from_typ br (IType ("Integer", [])) = |
|
153 Pretty.str "IntInf.int" |
|
154 | ml_from_typ br (IType ("List", [ty])) = |
|
155 postify ([ml_from_typ BR ty]) (Pretty.str "list") |
|
156 |> Pretty.block |
|
157 | ml_from_typ br (IType (tyco, typs)) = |
|
158 let |
|
159 val tyargs = (map (ml_from_typ BR) typs) |
|
160 in |
|
161 case styco tyco tyargs (ml_from_typ BR) |
|
162 of NONE => |
|
163 postify tyargs ((Pretty.str o resolv) tyco) |
|
164 |> Pretty.block |
|
165 | SOME ([], p) => |
|
166 p |
|
167 | SOME (_, p) => |
|
168 error ("cannot serialize partial type application to ML, while serializing " |
|
169 ^ quote (tyco ^ " " ^ Pretty.output (Pretty.list "(" ")" tyargs))) |
|
170 end |
|
171 | ml_from_typ br (IFun (t1, t2)) = |
|
172 brackify (eval_br_postfix br (INFX (1, R))) [ |
|
173 ml_from_typ (INFX (1, X)) t1, |
|
174 Pretty.str "->", |
|
175 ml_from_typ (INFX (1, R)) t2 |
|
176 ] |
|
177 | ml_from_typ _ (IVarT (v, [])) = |
|
178 Pretty.str ("'" ^ v) |
|
179 | ml_from_typ _ (IVarT (_, sort)) = |
|
180 "cannot serialize sort constrained type variable to ML: " ^ commas sort |> error |
|
181 | ml_from_typ _ (IDictT fs) = |
|
182 (Pretty.enclose "{" "}" o Pretty.breaks) ( |
|
183 map (fn (f, ty) => |
|
184 Pretty.block [Pretty.str (ml_label_uniq f ^ ": "), ml_from_typ NOBR ty]) fs |
|
185 ); |
|
186 fun ml_from_pat br (ICons (("True", []), _)) = |
|
187 Pretty.str "true" |
|
188 | ml_from_pat br (ICons (("False", []), _)) = |
|
189 Pretty.str "false" |
|
190 | ml_from_pat br (ICons (("Pair", ps), _)) = |
|
191 ps |
|
192 |> map (ml_from_pat NOBR) |
|
193 |> Pretty.list "(" ")" |
|
194 | ml_from_pat br (ICons (("Nil", []), _)) = |
|
195 Pretty.str "[]" |
|
196 | ml_from_pat br (p as ICons (("Cons", _), _)) = |
|
197 let |
|
198 fun dest_cons (ICons (("Cons", [ICons (("Pair", [p1, p2]), _)]), _)) = SOME (p1, p2) |
|
199 | dest_cons p = NONE |
|
200 in |
|
201 case unfoldr dest_cons p |
|
202 of (ps, (ICons (("Nil", []), _))) => |
|
203 ps |
|
204 |> map (ml_from_pat NOBR) |
|
205 |> Pretty.list "[" "]" |
|
206 | (ps, p) => |
|
207 (ps @ [p]) |
|
208 |> map (ml_from_pat (INFX (5, X))) |
|
209 |> separate (Pretty.str "::") |
|
210 |> brackify (eval_br br (INFX (5, R))) |
|
211 end |
|
212 | ml_from_pat br (ICons ((f, ps), ty)) = |
|
213 ps |
|
214 |> map (ml_from_pat BR) |
|
215 |> cons ((Pretty.str o resolv) f) |
|
216 |> brackify (eval_br br BR) |
|
217 | ml_from_pat br (IVarP (v, IType ("Integer", []))) = |
|
218 Pretty.str ("(" ^ v ^ ":IntInf.int)") |
|
219 | ml_from_pat br (IVarP (v, _)) = |
|
220 Pretty.str v; |
|
221 fun ml_from_iexpr br (e as (IApp (IConst ("Cons", _), _))) = |
|
222 let |
|
223 fun dest_cons (IApp (IConst ("Cons", _), |
|
224 IApp (IApp (IConst ("Pair", _), e1), e2))) = SOME (e1, e2) |
|
225 | dest_cons p = NONE |
|
226 in |
|
227 case unfoldr dest_cons e |
|
228 of (es, (IConst ("Nil", _))) => |
|
229 es |
|
230 |> map (ml_from_iexpr NOBR) |
|
231 |> Pretty.list "[" "]" |
|
232 | (es, e) => |
|
233 (es @ [e]) |
|
234 |> map (ml_from_iexpr (INFX (5, X))) |
|
235 |> separate (Pretty.str "::") |
|
236 |> brackify (eval_br br (INFX (5, R))) |
|
237 end |
|
238 | ml_from_iexpr br (e as IApp (e1, e2)) = |
|
239 (case (unfold_app e) |
|
240 of (e as (IConst (f, _)), es) => |
|
241 ml_from_app br (f, es) |
|
242 | _ => |
|
243 brackify (eval_br br BR) [ |
|
244 ml_from_iexpr NOBR e1, |
|
245 ml_from_iexpr BR e2 |
|
246 ]) |
|
247 | ml_from_iexpr br (e as IConst (f, _)) = |
|
248 ml_from_app br (f, []) |
|
249 | ml_from_iexpr br (IVarE (v, _)) = |
|
250 Pretty.str v |
|
251 | ml_from_iexpr br (IAbs ((v, _), e)) = |
|
252 brackify (eval_br br BR) [ |
|
253 Pretty.str ("fn " ^ v ^ " =>"), |
|
254 ml_from_iexpr BR e |
|
255 ] |
|
256 | ml_from_iexpr br (e as ICase (_, [_])) = |
|
257 let |
|
258 val (ps, e) = unfold_let e; |
|
259 fun mk_val (p, e) = Pretty.block [ |
|
260 Pretty.str "val ", |
|
261 ml_from_pat BR p, |
|
262 Pretty.str " =", |
|
263 Pretty.brk 1, |
|
264 ml_from_iexpr NOBR e, |
|
265 Pretty.str ";" |
|
266 ] |
|
267 in Pretty.chunks [ |
|
268 [Pretty.str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block, |
|
269 [Pretty.str ("in"), Pretty.fbrk, ml_from_iexpr NOBR e] |> Pretty.block, |
|
270 Pretty.str ("end") |
|
271 ] end |
|
272 | ml_from_iexpr br (ICase (e, c::cs)) = |
|
273 let |
|
274 fun mk_clause definer (p, e) = |
|
275 Pretty.block [ |
|
276 Pretty.str definer, |
|
277 ml_from_pat NOBR p, |
|
278 Pretty.str " =>", |
|
279 Pretty.brk 1, |
|
280 ml_from_iexpr NOBR e |
|
281 ] |
|
282 in brackify (eval_br br BR) ( |
|
283 Pretty.str "case " |
|
284 :: ml_from_iexpr NOBR e |
|
285 :: mk_clause "of " c |
|
286 :: map (mk_clause "|") cs |
|
287 ) end |
|
288 | ml_from_iexpr br (IInst _) = |
|
289 error "cannot serialize poly instant to ML" |
|
290 | ml_from_iexpr br (IDictE fs) = |
|
291 (Pretty.enclose "{" "}" o Pretty.breaks) ( |
|
292 map (fn (f, e) => |
|
293 Pretty.block [Pretty.str (ml_label_uniq f ^ " = "), ml_from_iexpr NOBR e]) fs |
|
294 ) |
|
295 | ml_from_iexpr br (ILookup (ls, v)) = |
|
296 brackify (eval_br br BR) [ |
|
297 Pretty.str "(", |
|
298 ls |> map ((fn s => "#" ^ s) o ml_label_uniq) |> foldr1 (fn (l, e) => l ^ " o " ^ e) |> Pretty.str, |
|
299 Pretty.str ")", |
|
300 Pretty.str " ", |
|
301 Pretty.str v |
|
302 ] |
|
303 and mk_app_p br p args = |
|
304 brackify (eval_br br BR) |
|
305 (p :: map (ml_from_iexpr BR) args) |
|
306 and ml_from_app br ("Nil", []) = |
|
307 Pretty.str "[]" |
|
308 | ml_from_app br ("True", []) = |
|
309 Pretty.str "true" |
|
310 | ml_from_app br ("False", []) = |
|
311 Pretty.str "false" |
|
312 | ml_from_app br ("primeq", [e1, e2]) = |
|
313 brackify (eval_br br (INFX (4, L))) [ |
|
314 ml_from_iexpr (INFX (4, L)) e1, |
|
315 Pretty.str "=", |
|
316 ml_from_iexpr (INFX (4, X)) e2 |
|
317 ] |
|
318 | ml_from_app br ("Pair", [e1, e2]) = |
|
319 Pretty.list "(" ")" [ |
|
320 ml_from_iexpr NOBR e1, |
|
321 ml_from_iexpr NOBR e2 |
|
322 ] |
|
323 | ml_from_app br ("and", [e1, e2]) = |
|
324 brackify (eval_br br (INFX (~1, L))) [ |
|
325 ml_from_iexpr (INFX (~1, L)) e1, |
|
326 Pretty.str "andalso", |
|
327 ml_from_iexpr (INFX (~1, X)) e2 |
|
328 ] |
|
329 | ml_from_app br ("or", [e1, e2]) = |
|
330 brackify (eval_br br (INFX (~2, L))) [ |
|
331 ml_from_iexpr (INFX (~2, L)) e1, |
|
332 Pretty.str "orelse", |
|
333 ml_from_iexpr (INFX (~2, X)) e2 |
|
334 ] |
|
335 | ml_from_app br ("if", [b, e1, e2]) = |
|
336 brackify (eval_br br BR) [ |
|
337 Pretty.str "if", |
|
338 ml_from_iexpr BR b, |
|
339 Pretty.str "then", |
|
340 ml_from_iexpr BR e1, |
|
341 Pretty.str "else", |
|
342 ml_from_iexpr BR e2 |
|
343 ] |
|
344 | ml_from_app br ("add", [e1, e2]) = |
|
345 brackify (eval_br br (INFX (6, L))) [ |
|
346 ml_from_iexpr (INFX (6, L)) e1, |
|
347 Pretty.str "+", |
|
348 ml_from_iexpr (INFX (6, X)) e2 |
|
349 ] |
|
350 | ml_from_app br ("mult", [e1, e2]) = |
|
351 brackify (eval_br br (INFX (7, L))) [ |
|
352 ml_from_iexpr (INFX (7, L)) e1, |
|
353 Pretty.str "+", |
|
354 ml_from_iexpr (INFX (7, X)) e2 |
|
355 ] |
|
356 | ml_from_app br ("lt", [e1, e2]) = |
|
357 brackify (eval_br br (INFX (4, L))) [ |
|
358 ml_from_iexpr (INFX (4, L)) e1, |
|
359 Pretty.str "<", |
|
360 ml_from_iexpr (INFX (4, X)) e2 |
|
361 ] |
|
362 | ml_from_app br ("le", [e1, e2]) = |
|
363 brackify (eval_br br (INFX (7, L))) [ |
|
364 ml_from_iexpr (INFX (4, L)) e1, |
|
365 Pretty.str "<=", |
|
366 ml_from_iexpr (INFX (4, X)) e2 |
|
367 ] |
|
368 | ml_from_app br ("minus", es) = |
|
369 mk_app_p br (Pretty.str "~") es |
|
370 | ml_from_app br ("wfrec", es) = |
|
371 mk_app_p br (Pretty.str "wfrec") es |
|
372 | ml_from_app br (f, es) = |
|
373 let |
|
374 val args = map (ml_from_iexpr BR) es |
|
375 val brackify' = K (eval_br br BR) ? (single #> Pretty.enclose "(" ")") |
|
376 fun prepend_abs v body = |
|
377 Pretty.block [Pretty.str ("fn " ^ v ^ " =>"), Pretty.brk 1, body] |
|
378 in |
|
379 case sconst f args (ml_from_iexpr BR) |
|
380 of NONE => |
|
381 brackify (eval_br br BR) (Pretty.str (resolv f) :: args) |
|
382 | SOME ([], p) => |
|
383 brackify' p |
|
384 | SOME (vars, p) => |
|
385 p |
|
386 |> fold_rev prepend_abs vars |
|
387 |> brackify' |
|
388 end; |
|
389 fun ml_from_funs (ds as d::ds_tl) = |
|
390 let |
|
391 fun mk_definer [] = "val" |
|
392 | mk_definer _ = "fun" |
|
393 fun check_args (_, Fun ((pats, _)::_, _)) NONE = |
|
394 SOME (mk_definer pats) |
|
395 | check_args (_, Fun ((pats, _)::_, _)) (SOME definer) = |
|
396 if mk_definer pats = definer |
|
397 then SOME definer |
|
398 else error ("Mixing simultaneous vals and funs not implemented") |
|
399 | check_args _ _ = |
|
400 error ("Function definition block containing other definitions than functions") |
|
401 val definer = the (fold check_args ds NONE); |
|
402 fun mk_eq definer f' ty (pats, expr) = |
|
403 let |
|
404 val lhs = [Pretty.str (definer ^ " " ^ f')] |
|
405 @ (if null pats |
|
406 then [Pretty.str ":", ml_from_typ NOBR ty] |
|
407 else map (ml_from_pat BR) pats) |
|
408 val rhs = [Pretty.str "=", ml_from_iexpr NOBR expr] |
|
409 in |
|
410 Pretty.block (separate (Pretty.brk 1) (lhs @ rhs)) |
|
411 end |
|
412 fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (_, ty))) = |
|
413 let |
|
414 val (pats_hd::pats_tl) = (fst o split_list) eqs |
|
415 val _ = fold (fn x => fn y => (x ~~ y; y)) pats_tl pats_hd |
|
416 (*check for equal length of argument lists*) |
|
417 in (Pretty.block o Pretty.fbreaks) ( |
|
418 (*Pretty.block [ |
|
419 Pretty.brk 1, |
|
420 Pretty.str ": ", |
|
421 ml_from_typ NOBR ty |
|
422 ]*) |
|
423 mk_eq definer f ty eq |
|
424 :: map (mk_eq "|" f ty) eq_tl |
|
425 ) |
|
426 end |
|
427 in |
|
428 chunk_defs ( |
|
429 mk_fun definer d |
|
430 :: map (mk_fun "and") ds_tl |
|
431 ) |
|
432 end; |
|
433 fun ml_from_datatypes ds = |
|
434 let |
|
435 val _ = debug 9 (fn _ => map (pretty_def o snd) ds |> Pretty.chunks |> Pretty.output) (); |
|
436 fun check_typ_dup ty xs = |
|
437 if AList.defined (op =) xs ty |
|
438 then error ("double datatype definition: " ^ quote ty) |
|
439 else xs |
|
440 fun check_typ_miss ty xs = |
|
441 if AList.defined (op =) xs ty |
|
442 then xs |
|
443 else error ("missing datatype definition: " ^ quote ty) |
|
444 fun group (name, Datatype (vs, _, _)) ts = |
|
445 (map (fn (_, []) => () | _ => error "can't serialize sort constrained datatype declaration to ML") vs; |
|
446 ts |
|
447 |> apsnd (check_typ_dup name) |
|
448 |> apsnd (AList.update (op =) (name, (vs, [])))) |
|
449 | group (_, Datatypecons (_, _::_::_)) _ = |
|
450 error ("Datatype constructor containing more than one parameter") |
|
451 | group (name, Datatypecons (ty, tys)) ts = |
|
452 ts |
|
453 |> apfst (AList.default (op =) (resolv ty, [])) |
|
454 |> apfst (AList.map_entry (op =) (resolv ty) (cons (name, tys))) |
|
455 | group _ _ = |
|
456 error ("Datatype block containing other statements than datatype or constructor definitions") |
|
457 fun group_cons (ty, co) ts = |
|
458 ts |
|
459 |> check_typ_miss ty |
|
460 |> AList.map_entry (op =) ty (rpair co o fst) |
|
461 fun mk_datatypes (ds as d::ds_tl) = |
|
462 let |
|
463 fun mk_cons (co, typs) = |
|
464 (Pretty.block oo praetify) |
|
465 (map (ml_from_typ NOBR) typs) |
|
466 (Pretty.str (resolv co)) |
|
467 fun mk_datatype definer (t, (vs, cs)) = |
|
468 Pretty.block ( |
|
469 [Pretty.str definer] |
|
470 @ postify (map (ml_from_typ BR o IVarT) vs) |
|
471 (Pretty.str t) |
|
472 @ [Pretty.str " =", |
|
473 Pretty.brk 1] |
|
474 @ separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons cs) |
|
475 ) |
|
476 in |
|
477 chunk_defs ( |
|
478 mk_datatype "datatype " d |
|
479 :: map (mk_datatype "and ") ds_tl |
|
480 ) |
|
481 end; |
|
482 in |
|
483 ([], []) |
|
484 |> fold group ds |
|
485 |-> (fn cons => fold group_cons cons) |
|
486 |> mk_datatypes |
|
487 end; |
|
488 fun ml_from_def (name, Typesyn (vs, ty)) = |
|
489 (map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs; |
|
490 Pretty.block ( |
|
491 Pretty.str "type " |
|
492 :: postify (map (Pretty.str o fst) vs) (Pretty.str name) |
|
493 @ [Pretty.str " =", |
|
494 Pretty.brk 1, |
|
495 ml_from_typ NOBR ty, |
|
496 Pretty.str ";" |
|
497 ])) |
|
498 | ml_from_def (name, Nop) = |
|
499 if exists (fn query => (is_some o query) name) |
|
500 [(fn name => styco name [] (ml_from_typ NOBR)), |
|
501 (fn name => sconst name [] (ml_from_iexpr NOBR))] |
|
502 then Pretty.str "" |
|
503 else error ("empty statement during serialization: " ^ quote name) |
|
504 | ml_from_def (name, Class _) = |
|
505 error ("can't serialize class declaration " ^ quote name ^ " to ML") |
|
506 | ml_from_def (name, Classinst _) = |
|
507 error ("can't serialize instance declaration " ^ quote name ^ " to ML") |
|
508 in case (snd o hd) ds |
|
509 of Fun _ => ml_from_funs ds |
|
510 | Datatypecons _ => ml_from_datatypes ds |
|
511 | Datatype _ => ml_from_datatypes ds |
|
512 | _ => (case ds of [d] => ml_from_def d) |
|
513 end; |
|
514 |
|
515 in |
|
516 |
|
517 fun ml_from_thingol nspgrp name_root styco sconst prims module = |
|
518 let |
|
519 fun ml_from_module (name, ps) = |
|
520 Pretty.chunks ([ |
|
521 Pretty.str ("structure " ^ name ^ " = "), |
|
522 Pretty.str "struct", |
|
523 Pretty.str "" |
|
524 ] @ ps @ [ |
|
525 Pretty.str "", |
|
526 Pretty.str ("end; (* struct " ^ name ^ " *)") |
|
527 ]); |
|
528 fun eta_expander "Pair" = 2 |
|
529 | eta_expander "Cons" = 2 |
|
530 | eta_expander "primeq" = 2 |
|
531 | eta_expander "and" = 2 |
|
532 | eta_expander "or" = 2 |
|
533 | eta_expander "if" = 3 |
|
534 | eta_expander "add" = 2 |
|
535 | eta_expander "mult" = 2 |
|
536 | eta_expander "lt" = 2 |
|
537 | eta_expander "le" = 2 |
|
538 | eta_expander s = |
|
539 if NameSpace.is_qualified s |
|
540 then case get_def module s |
|
541 of Datatypecons (_ , tys) => |
|
542 if length tys >= 2 then length tys else 0 |
|
543 | _ => |
|
544 (case sconst s [] (K (Pretty.str "")) |
|
545 of NONE => 0 |
|
546 | SOME (xs, _) => length xs) |
|
547 else 0 |
|
548 in |
|
549 module |
|
550 |> debug 5 (Pretty.output o pretty_module) |
|
551 |> debug 3 (fn _ => "connecting datatypes and classdecls...") |
|
552 |> connect_datatypes_clsdecls |
|
553 |> debug 3 (fn _ => "selecting submodule...") |
|
554 |> I (*! HIER SOLLTE DAS TATSÄCHLICH STATTFINDEN !*) |
|
555 |> debug 3 (fn _ => "eta-expanding...") |
|
556 |> eta_expand eta_expander |
|
557 |> debug 5 (Pretty.output o pretty_module) |
|
558 |> debug 3 (fn _ => "tupelizing datatypes...") |
|
559 |> tupelize_cons |
|
560 |> debug 3 (fn _ => "eliminating classes...") |
|
561 |> eliminate_classes |
|
562 |> debug 3 (fn _ => "generating...") |
|
563 |> serialize (ml_from_defs styco sconst) ml_from_module (ml_validator prims) nspgrp name_root |
|
564 end; |
|
565 |
|
566 (* ML infix precedence |
|
567 7 / * div mod |
|
568 6 + - ^ |
|
569 5 :: @ |
|
570 4 = <> < > <= >= |
|
571 3 := o *) |
|
572 |
|
573 end; (* local *) |
|
574 |
|
575 end; (* struct *) |
|
576 |