author | haftmann |
Fri, 02 Dec 2005 16:05:31 +0100 | |
changeset 18335 | 99baddf6b0d0 |
parent 18304 | 684832c9fa62 |
child 18360 | a2c9506b62a7 |
permissions | -rw-r--r-- |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
1 |
(* Title: Pure/Tools/codegen_serializer.ML |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
2 |
ID: $Id$ |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
3 |
Author: Florian Haftmann, TU Muenchen |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
4 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
5 |
Serializer from intermediate language ("Thin-gol") to |
18216 | 6 |
target languages (like ML or Haskell). |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
7 |
*) |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
8 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
9 |
signature CODEGEN_SERIALIZER = |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
10 |
sig |
18216 | 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 |
||
18304 | 17 |
type 'a pretty_syntax = string |
18 |
-> (int * (Pretty.T list -> ('a -> Pretty.T) -> Pretty.T)) option; |
|
19 |
type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax |
|
18217 | 20 |
-> primitives -> string list option -> CodegenThingol.module -> Pretty.T; |
18216 | 21 |
|
22 |
val ml_from_thingol: string list list -> string -> serializer; |
|
18282 | 23 |
val haskell_from_thingol: string list list -> string -> serializer; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
24 |
end; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
25 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
26 |
structure CodegenSerializer: CODEGEN_SERIALIZER = |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
27 |
struct |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
28 |
|
18216 | 29 |
open CodegenThingol; |
30 |
||
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 |
||
18304 | 64 |
(** keyword arguments **) |
65 |
||
66 |
type kw = (string * string option) list; |
|
67 |
fun kw_make args = |
|
68 |
let |
|
69 |
val parse_keyval = (); |
|
70 |
in |
|
71 |
Args.!!! (Scan.repeat ( |
|
72 |
Args.name |
|
73 |
-- Scan.option (Args.$$$ "=" |-- Args.name) |
|
74 |
) #> fst) args |
|
75 |
end; |
|
76 |
fun kw_get k kw = |
|
77 |
((the o AList.lookup (op =) kw) k, AList.delete (op =) k kw); |
|
78 |
fun kw_has kw k = |
|
79 |
AList.defined (op =) kw k; |
|
80 |
fun kw_done x [] = x |
|
81 |
| kw_done x kw = |
|
82 |
error ("uninterpreted keyword arguments: " ^ (commas o map (quote o fst)) kw); |
|
83 |
||
84 |
||
85 |
||
18216 | 86 |
(** generic serialization **) |
87 |
||
18304 | 88 |
type 'a pretty_syntax = string |
89 |
-> (int * (Pretty.T list -> ('a -> Pretty.T) -> Pretty.T)) option; |
|
90 |
type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax |
|
18217 | 91 |
-> primitives -> string list option -> CodegenThingol.module -> Pretty.T; |
18216 | 92 |
|
93 |
datatype lrx = L | R | X; |
|
94 |
||
95 |
datatype brack = |
|
96 |
BR |
|
97 |
| NOBR |
|
98 |
| INFX of (int * lrx); |
|
99 |
||
100 |
fun eval_lrx L L = false |
|
101 |
| eval_lrx R R = false |
|
102 |
| eval_lrx _ _ = true; |
|
103 |
||
104 |
fun eval_br BR _ = true |
|
105 |
| eval_br NOBR _ = false |
|
106 |
| eval_br (INFX (pr1, lr1)) (INFX (pr2, lr2)) = |
|
107 |
pr1 > pr2 |
|
108 |
orelse pr1 = pr2 |
|
109 |
andalso eval_lrx lr1 lr2 |
|
110 |
| eval_br (INFX _) _ = false; |
|
111 |
||
112 |
fun eval_br_postfix BR _ = false |
|
113 |
| eval_br_postfix NOBR _ = false |
|
114 |
| eval_br_postfix (INFX (pr1, lr1)) (INFX (pr2, lr2)) = |
|
115 |
pr1 > pr2 |
|
116 |
orelse pr1 = pr2 |
|
117 |
andalso eval_lrx lr1 lr2 |
|
118 |
| eval_br_postfix (INFX _) _ = false; |
|
119 |
||
120 |
fun brackify _ [p] = p |
|
121 |
| brackify true (ps as _::_) = Pretty.enclose "(" ")" (Pretty.breaks ps) |
|
122 |
| brackify false (ps as _::_) = Pretty.block (Pretty.breaks ps); |
|
123 |
||
124 |
fun postify [] f = [f] |
|
125 |
| postify [p] f = [p, Pretty.brk 1, f] |
|
126 |
| postify (ps as _::_) f = [Pretty.list "(" ")" ps, Pretty.brk 1, f]; |
|
127 |
||
18282 | 128 |
fun upper_first s = |
18335 | 129 |
let |
130 |
val (pr, b) = split_last (NameSpace.unpack s); |
|
131 |
val (c::cs) = String.explode b; |
|
132 |
in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end; |
|
18282 | 133 |
|
134 |
fun lower_first s = |
|
18335 | 135 |
let |
136 |
val (pr, b) = split_last (NameSpace.unpack s); |
|
137 |
val (c::cs) = String.explode b; |
|
138 |
in NameSpace.pack (pr @ [String.implode (Char.toLower c :: cs)]) end; |
|
18282 | 139 |
|
140 |
||
141 |
(** grouping functions **) |
|
142 |
||
143 |
fun group_datatypes one_arg defs = |
|
144 |
let |
|
18304 | 145 |
fun check_typ_dup dtname ts = |
146 |
if AList.defined (op =) ts dtname |
|
18282 | 147 |
then error ("double datatype definition: " ^ quote dtname) |
18304 | 148 |
else ts |
149 |
fun check_typ_miss dtname ts = |
|
150 |
if AList.defined (op =) ts dtname |
|
151 |
then ts |
|
18282 | 152 |
else error ("missing datatype definition: " ^ quote dtname) |
153 |
fun group (name, Datatype (vs, _, _)) ts = |
|
154 |
(if one_arg |
|
155 |
then map (fn (_, []) => () | _ => error "can't serialize sort constrained datatype declaration to ML") vs |
|
156 |
else []; |
|
157 |
ts |
|
158 |
|> apsnd (check_typ_dup name) |
|
159 |
|> apsnd (AList.update (op =) (name, (vs, [])))) |
|
160 |
| group (name, Datatypecons (dtname, tys as _::_::_)) ts = |
|
161 |
if one_arg |
|
162 |
then error ("datatype constructor containing more than one parameter") |
|
163 |
else |
|
164 |
ts |
|
165 |
|> apfst (AList.default (op =) (NameSpace.base dtname, [])) |
|
166 |
|> apfst (AList.map_entry (op =) (NameSpace.base dtname) (cons (name, tys))) |
|
167 |
| group (name, Datatypecons (dtname, tys)) ts = |
|
168 |
ts |
|
169 |
|> apfst (AList.default (op =) (NameSpace.base dtname, [])) |
|
170 |
|> apfst (AList.map_entry (op =) (NameSpace.base dtname) (cons (name, tys))) |
|
171 |
| group _ _ = |
|
172 |
error ("Datatype block containing other statements than datatype or constructor definitions") |
|
173 |
fun group_cons (dtname, co) ts = |
|
174 |
ts |
|
175 |
|> check_typ_miss dtname |
|
176 |
|> AList.map_entry (op =) dtname (rpair co o fst) |
|
177 |
in |
|
178 |
([], []) |
|
179 |
|> fold group defs |
|
180 |
|-> (fn cons => fold group_cons cons) |
|
181 |
end; |
|
18216 | 182 |
|
18304 | 183 |
fun group_classes defs = |
184 |
let |
|
185 |
fun check_class_dup clsname ts = |
|
186 |
if AList.defined (op =) ts clsname |
|
187 |
then error ("double class definition: " ^ quote clsname) |
|
188 |
else ts |
|
189 |
fun check_clsname_miss clsname ts = |
|
190 |
if AList.defined (op =) ts clsname |
|
191 |
then ts |
|
192 |
else error ("missing class definition: " ^ quote clsname) |
|
193 |
fun group (name, Class (supercls, v, _, _)) ts = |
|
194 |
ts |
|
195 |
|> apsnd (check_class_dup name) |
|
196 |
|> apsnd (AList.update (op =) (name, ((supercls, v), []))) |
|
197 |
| group (name, Classmember (clsname, _, ty)) ts = |
|
198 |
ts |
|
199 |
|> apfst (AList.default (op =) (NameSpace.base clsname, [])) |
|
200 |
|> apfst (AList.map_entry (op =) (NameSpace.base clsname) (cons (name, ty))) |
|
201 |
| group _ _ = |
|
202 |
error ("Datatype block containing other statements than datatype or constructor definitions") |
|
203 |
fun group_members (clsname, member) ts = |
|
204 |
ts |
|
205 |
|> check_clsname_miss clsname |
|
206 |
|> AList.map_entry (op =) clsname (rpair member o fst) |
|
207 |
in |
|
208 |
([], []) |
|
209 |
|> fold group defs |
|
210 |
|-> (fn members => fold group_members members) |
|
211 |
end; |
|
18216 | 212 |
|
213 |
(** ML serializer **) |
|
214 |
||
215 |
local |
|
216 |
||
18304 | 217 |
fun ml_from_defs tyco_syntax const_syntax resolv ds = |
18216 | 218 |
let |
18282 | 219 |
fun chunk_defs ps = |
18216 | 220 |
let |
221 |
val (p_init, p_last) = split_last ps |
|
222 |
in |
|
223 |
Pretty.chunks (p_init @ [Pretty.block ([p_last, Pretty.str ";"])]) |
|
224 |
end; |
|
18282 | 225 |
val ml_label_uniq = translate_string (fn "'" => "''" | "." => "'" | c => c); |
226 |
fun ml_from_type br (IType ("Pair", [t1, t2])) = |
|
18216 | 227 |
brackify (eval_br_postfix br (INFX (2, L))) [ |
18282 | 228 |
ml_from_type (INFX (2, X)) t1, |
18216 | 229 |
Pretty.str "*", |
18282 | 230 |
ml_from_type (INFX (2, X)) t2 |
18216 | 231 |
] |
18282 | 232 |
| ml_from_type br (IType ("Bool", [])) = |
18216 | 233 |
Pretty.str "bool" |
18282 | 234 |
| ml_from_type br (IType ("Integer", [])) = |
18216 | 235 |
Pretty.str "IntInf.int" |
18282 | 236 |
| ml_from_type br (IType ("List", [ty])) = |
237 |
postify ([ml_from_type BR ty]) (Pretty.str "list") |
|
18216 | 238 |
|> Pretty.block |
18282 | 239 |
| ml_from_type br (IType (tyco, typs)) = |
18216 | 240 |
let |
18282 | 241 |
val tyargs = (map (ml_from_type BR) typs) |
18216 | 242 |
in |
18304 | 243 |
case tyco_syntax tyco |
18216 | 244 |
of NONE => |
245 |
postify tyargs ((Pretty.str o resolv) tyco) |
|
246 |
|> Pretty.block |
|
18304 | 247 |
| SOME (i, pr) => |
18282 | 248 |
if i <> length (typs) |
249 |
then error "can only serialize strictly complete type applications to ML" |
|
18304 | 250 |
else pr tyargs (ml_from_type BR) |
18216 | 251 |
end |
18282 | 252 |
| ml_from_type br (IFun (t1, t2)) = |
18216 | 253 |
brackify (eval_br_postfix br (INFX (1, R))) [ |
18282 | 254 |
ml_from_type (INFX (1, X)) t1, |
18216 | 255 |
Pretty.str "->", |
18282 | 256 |
ml_from_type (INFX (1, R)) t2 |
18216 | 257 |
] |
18282 | 258 |
| ml_from_type _ (IVarT (v, [])) = |
18216 | 259 |
Pretty.str ("'" ^ v) |
18282 | 260 |
| ml_from_type _ (IVarT (_, sort)) = |
18216 | 261 |
"cannot serialize sort constrained type variable to ML: " ^ commas sort |> error |
18282 | 262 |
| ml_from_type _ (IDictT fs) = |
18216 | 263 |
(Pretty.enclose "{" "}" o Pretty.breaks) ( |
264 |
map (fn (f, ty) => |
|
18282 | 265 |
Pretty.block [Pretty.str (ml_label_uniq f ^ ": "), ml_from_type NOBR ty]) fs |
18216 | 266 |
); |
267 |
fun ml_from_pat br (ICons (("True", []), _)) = |
|
268 |
Pretty.str "true" |
|
269 |
| ml_from_pat br (ICons (("False", []), _)) = |
|
270 |
Pretty.str "false" |
|
18282 | 271 |
| ml_from_pat br (ICons (("Pair", [p1, p2]), _)) = |
272 |
Pretty.list "(" ")" [ |
|
273 |
ml_from_pat NOBR p1, |
|
274 |
ml_from_pat NOBR p2 |
|
275 |
] |
|
18216 | 276 |
| ml_from_pat br (ICons (("Nil", []), _)) = |
277 |
Pretty.str "[]" |
|
278 |
| ml_from_pat br (p as ICons (("Cons", _), _)) = |
|
279 |
let |
|
280 |
fun dest_cons (ICons (("Cons", [ICons (("Pair", [p1, p2]), _)]), _)) = SOME (p1, p2) |
|
281 |
| dest_cons p = NONE |
|
282 |
in |
|
283 |
case unfoldr dest_cons p |
|
284 |
of (ps, (ICons (("Nil", []), _))) => |
|
285 |
ps |
|
286 |
|> map (ml_from_pat NOBR) |
|
287 |
|> Pretty.list "[" "]" |
|
288 |
| (ps, p) => |
|
289 |
(ps @ [p]) |
|
290 |
|> map (ml_from_pat (INFX (5, X))) |
|
291 |
|> separate (Pretty.str "::") |
|
292 |
|> brackify (eval_br br (INFX (5, R))) |
|
293 |
end |
|
294 |
| ml_from_pat br (ICons ((f, ps), ty)) = |
|
18335 | 295 |
(case const_syntax f |
296 |
of NONE => |
|
297 |
ps |
|
298 |
|> map (ml_from_pat BR) |
|
299 |
|> cons ((Pretty.str o resolv) f) |
|
300 |
|> brackify (eval_br br BR) |
|
301 |
| SOME (i, pr) => |
|
302 |
if i = length ps |
|
303 |
then |
|
304 |
pr (map (ml_from_pat BR) ps) (ml_from_expr BR) |
|
305 |
else |
|
306 |
error "number of argument mismatch in customary serialization") |
|
18216 | 307 |
| ml_from_pat br (IVarP (v, IType ("Integer", []))) = |
18282 | 308 |
brackify (eval_br br BR) [ |
309 |
Pretty.str v, |
|
310 |
Pretty.str ":", |
|
311 |
Pretty.str "IntInf.int" |
|
312 |
] |
|
18216 | 313 |
| ml_from_pat br (IVarP (v, _)) = |
18335 | 314 |
Pretty.str v |
315 |
and ml_from_expr br (e as (IApp (IConst ("Cons", _), _))) = |
|
18216 | 316 |
let |
317 |
fun dest_cons (IApp (IConst ("Cons", _), |
|
318 |
IApp (IApp (IConst ("Pair", _), e1), e2))) = SOME (e1, e2) |
|
319 |
| dest_cons p = NONE |
|
320 |
in |
|
321 |
case unfoldr dest_cons e |
|
322 |
of (es, (IConst ("Nil", _))) => |
|
323 |
es |
|
18282 | 324 |
|> map (ml_from_expr NOBR) |
18216 | 325 |
|> Pretty.list "[" "]" |
326 |
| (es, e) => |
|
327 |
(es @ [e]) |
|
18282 | 328 |
|> map (ml_from_expr (INFX (5, X))) |
18216 | 329 |
|> separate (Pretty.str "::") |
330 |
|> brackify (eval_br br (INFX (5, R))) |
|
331 |
end |
|
18282 | 332 |
| ml_from_expr br (e as IApp (e1, e2)) = |
18216 | 333 |
(case (unfold_app e) |
334 |
of (e as (IConst (f, _)), es) => |
|
335 |
ml_from_app br (f, es) |
|
18282 | 336 |
| _ => |
18216 | 337 |
brackify (eval_br br BR) [ |
18282 | 338 |
ml_from_expr NOBR e1, |
339 |
ml_from_expr BR e2 |
|
18216 | 340 |
]) |
18282 | 341 |
| ml_from_expr br (e as IConst (f, _)) = |
18216 | 342 |
ml_from_app br (f, []) |
18282 | 343 |
| ml_from_expr br (IVarE (v, _)) = |
18216 | 344 |
Pretty.str v |
18282 | 345 |
| ml_from_expr br (IAbs ((v, _), e)) = |
18216 | 346 |
brackify (eval_br br BR) [ |
347 |
Pretty.str ("fn " ^ v ^ " =>"), |
|
18282 | 348 |
ml_from_expr NOBR e |
18216 | 349 |
] |
18282 | 350 |
| ml_from_expr br (e as ICase (_, [_])) = |
18216 | 351 |
let |
352 |
val (ps, e) = unfold_let e; |
|
353 |
fun mk_val (p, e) = Pretty.block [ |
|
354 |
Pretty.str "val ", |
|
355 |
ml_from_pat BR p, |
|
356 |
Pretty.str " =", |
|
357 |
Pretty.brk 1, |
|
18282 | 358 |
ml_from_expr NOBR e, |
18216 | 359 |
Pretty.str ";" |
360 |
] |
|
361 |
in Pretty.chunks [ |
|
362 |
[Pretty.str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block, |
|
18282 | 363 |
[Pretty.str ("in"), Pretty.fbrk, ml_from_expr NOBR e] |> Pretty.block, |
18216 | 364 |
Pretty.str ("end") |
365 |
] end |
|
18282 | 366 |
| ml_from_expr br (ICase (e, c::cs)) = |
18216 | 367 |
let |
368 |
fun mk_clause definer (p, e) = |
|
369 |
Pretty.block [ |
|
370 |
Pretty.str definer, |
|
371 |
ml_from_pat NOBR p, |
|
372 |
Pretty.str " =>", |
|
373 |
Pretty.brk 1, |
|
18282 | 374 |
ml_from_expr NOBR e |
18216 | 375 |
] |
376 |
in brackify (eval_br br BR) ( |
|
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
377 |
Pretty.str "case" |
18282 | 378 |
:: ml_from_expr NOBR e |
18216 | 379 |
:: mk_clause "of " c |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
380 |
:: map (mk_clause "| ") cs |
18216 | 381 |
) end |
18282 | 382 |
| ml_from_expr br (IInst _) = |
18216 | 383 |
error "cannot serialize poly instant to ML" |
18282 | 384 |
| ml_from_expr br (IDictE fs) = |
18216 | 385 |
(Pretty.enclose "{" "}" o Pretty.breaks) ( |
386 |
map (fn (f, e) => |
|
18282 | 387 |
Pretty.block [Pretty.str (ml_label_uniq f ^ " = "), ml_from_expr NOBR e]) fs |
18216 | 388 |
) |
18282 | 389 |
| ml_from_expr br (ILookup (ls, v)) = |
18216 | 390 |
brackify (eval_br br BR) [ |
391 |
Pretty.str "(", |
|
392 |
ls |> map ((fn s => "#" ^ s) o ml_label_uniq) |> foldr1 (fn (l, e) => l ^ " o " ^ e) |> Pretty.str, |
|
393 |
Pretty.str ")", |
|
394 |
Pretty.str " ", |
|
395 |
Pretty.str v |
|
396 |
] |
|
397 |
and mk_app_p br p args = |
|
398 |
brackify (eval_br br BR) |
|
18282 | 399 |
(p :: map (ml_from_expr BR) args) |
18216 | 400 |
and ml_from_app br ("Nil", []) = |
401 |
Pretty.str "[]" |
|
402 |
| ml_from_app br ("True", []) = |
|
403 |
Pretty.str "true" |
|
404 |
| ml_from_app br ("False", []) = |
|
405 |
Pretty.str "false" |
|
406 |
| ml_from_app br ("primeq", [e1, e2]) = |
|
407 |
brackify (eval_br br (INFX (4, L))) [ |
|
18282 | 408 |
ml_from_expr (INFX (4, L)) e1, |
18216 | 409 |
Pretty.str "=", |
18335 | 410 |
ml_from_expr (INFX (4, X)) e2, |
411 |
Pretty.str ":", |
|
412 |
ml_from_type NOBR (itype_of_iexpr e2) |
|
18216 | 413 |
] |
414 |
| ml_from_app br ("Pair", [e1, e2]) = |
|
415 |
Pretty.list "(" ")" [ |
|
18282 | 416 |
ml_from_expr NOBR e1, |
417 |
ml_from_expr NOBR e2 |
|
18216 | 418 |
] |
419 |
| ml_from_app br ("and", [e1, e2]) = |
|
420 |
brackify (eval_br br (INFX (~1, L))) [ |
|
18282 | 421 |
ml_from_expr (INFX (~1, L)) e1, |
18216 | 422 |
Pretty.str "andalso", |
18282 | 423 |
ml_from_expr (INFX (~1, X)) e2 |
18216 | 424 |
] |
425 |
| ml_from_app br ("or", [e1, e2]) = |
|
426 |
brackify (eval_br br (INFX (~2, L))) [ |
|
18282 | 427 |
ml_from_expr (INFX (~2, L)) e1, |
18216 | 428 |
Pretty.str "orelse", |
18282 | 429 |
ml_from_expr (INFX (~2, X)) e2 |
18216 | 430 |
] |
431 |
| ml_from_app br ("if", [b, e1, e2]) = |
|
432 |
brackify (eval_br br BR) [ |
|
433 |
Pretty.str "if", |
|
18282 | 434 |
ml_from_expr NOBR b, |
18216 | 435 |
Pretty.str "then", |
18282 | 436 |
ml_from_expr NOBR e1, |
18216 | 437 |
Pretty.str "else", |
18282 | 438 |
ml_from_expr NOBR e2 |
18216 | 439 |
] |
440 |
| ml_from_app br ("add", [e1, e2]) = |
|
441 |
brackify (eval_br br (INFX (6, L))) [ |
|
18282 | 442 |
ml_from_expr (INFX (6, L)) e1, |
18216 | 443 |
Pretty.str "+", |
18282 | 444 |
ml_from_expr (INFX (6, X)) e2 |
18216 | 445 |
] |
446 |
| ml_from_app br ("mult", [e1, e2]) = |
|
447 |
brackify (eval_br br (INFX (7, L))) [ |
|
18282 | 448 |
ml_from_expr (INFX (7, L)) e1, |
18216 | 449 |
Pretty.str "+", |
18282 | 450 |
ml_from_expr (INFX (7, X)) e2 |
18216 | 451 |
] |
452 |
| ml_from_app br ("lt", [e1, e2]) = |
|
453 |
brackify (eval_br br (INFX (4, L))) [ |
|
18282 | 454 |
ml_from_expr (INFX (4, L)) e1, |
18216 | 455 |
Pretty.str "<", |
18282 | 456 |
ml_from_expr (INFX (4, X)) e2 |
18216 | 457 |
] |
458 |
| ml_from_app br ("le", [e1, e2]) = |
|
459 |
brackify (eval_br br (INFX (7, L))) [ |
|
18282 | 460 |
ml_from_expr (INFX (4, L)) e1, |
18216 | 461 |
Pretty.str "<=", |
18282 | 462 |
ml_from_expr (INFX (4, X)) e2 |
18216 | 463 |
] |
464 |
| ml_from_app br ("minus", es) = |
|
465 |
mk_app_p br (Pretty.str "~") es |
|
466 |
| ml_from_app br ("wfrec", es) = |
|
467 |
mk_app_p br (Pretty.str "wfrec") es |
|
468 |
| ml_from_app br (f, es) = |
|
18304 | 469 |
case const_syntax f |
18282 | 470 |
of NONE => |
18335 | 471 |
(case es |
472 |
of [] => Pretty.str (resolv f) |
|
473 |
| es => |
|
474 |
let |
|
475 |
val (es', e) = split_last es; |
|
476 |
in mk_app_p br (ml_from_app NOBR (f, es')) [e] end) |
|
18304 | 477 |
| SOME (i, pr) => |
18282 | 478 |
let |
479 |
val (es1, es2) = splitAt (i, es); |
|
18304 | 480 |
in mk_app_p br (pr (map (ml_from_expr BR) es1) (ml_from_expr BR)) es2 end; |
18216 | 481 |
fun ml_from_funs (ds as d::ds_tl) = |
482 |
let |
|
483 |
fun mk_definer [] = "val" |
|
484 |
| mk_definer _ = "fun" |
|
485 |
fun check_args (_, Fun ((pats, _)::_, _)) NONE = |
|
486 |
SOME (mk_definer pats) |
|
487 |
| check_args (_, Fun ((pats, _)::_, _)) (SOME definer) = |
|
488 |
if mk_definer pats = definer |
|
489 |
then SOME definer |
|
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
490 |
else error ("mixing simultaneous vals and funs not implemented") |
18216 | 491 |
| check_args _ _ = |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
492 |
error ("function definition block containing other definitions than functions") |
18216 | 493 |
val definer = the (fold check_args ds NONE); |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
494 |
fun mk_eq definer f ty (pats, expr) = |
18216 | 495 |
let |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
496 |
val lhs = [Pretty.str (definer ^ " " ^ f)] |
18216 | 497 |
@ (if null pats |
18282 | 498 |
then [Pretty.str ":", ml_from_type NOBR ty] |
18216 | 499 |
else map (ml_from_pat BR) pats) |
18282 | 500 |
val rhs = [Pretty.str "=", ml_from_expr NOBR expr] |
18216 | 501 |
in |
502 |
Pretty.block (separate (Pretty.brk 1) (lhs @ rhs)) |
|
503 |
end |
|
504 |
fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (_, ty))) = |
|
505 |
let |
|
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
506 |
val (pats_hd::pats_tl) = (fst o split_list) eqs; |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
507 |
val _ = fold (fn x => fn y => (x ~~ y; y)) pats_tl pats_hd; |
18216 | 508 |
(*check for equal length of argument lists*) |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
509 |
val shift = if null eq_tl then I else map (Pretty.block o single); |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
510 |
in (Pretty.block o Pretty.fbreaks o shift) ( |
18216 | 511 |
mk_eq definer f ty eq |
512 |
:: map (mk_eq "|" f ty) eq_tl |
|
513 |
) |
|
514 |
end |
|
515 |
in |
|
516 |
chunk_defs ( |
|
517 |
mk_fun definer d |
|
518 |
:: map (mk_fun "and") ds_tl |
|
519 |
) |
|
520 |
end; |
|
18282 | 521 |
fun ml_from_datatypes defs = |
18216 | 522 |
let |
523 |
fun mk_datatypes (ds as d::ds_tl) = |
|
524 |
let |
|
18282 | 525 |
fun praetify [] f = [f] |
526 |
| praetify [p] f = [f, Pretty.str " of ", p] |
|
18216 | 527 |
fun mk_cons (co, typs) = |
528 |
(Pretty.block oo praetify) |
|
18282 | 529 |
(map (ml_from_type NOBR) typs) |
18216 | 530 |
(Pretty.str (resolv co)) |
531 |
fun mk_datatype definer (t, (vs, cs)) = |
|
532 |
Pretty.block ( |
|
533 |
[Pretty.str definer] |
|
18282 | 534 |
@ postify (map (ml_from_type BR o IVarT) vs) |
535 |
(Pretty.str (resolv t)) |
|
18216 | 536 |
@ [Pretty.str " =", |
537 |
Pretty.brk 1] |
|
538 |
@ separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons cs) |
|
539 |
) |
|
540 |
in |
|
541 |
chunk_defs ( |
|
542 |
mk_datatype "datatype " d |
|
543 |
:: map (mk_datatype "and ") ds_tl |
|
544 |
) |
|
545 |
end; |
|
546 |
in |
|
18282 | 547 |
(mk_datatypes o group_datatypes true) defs |
18216 | 548 |
end; |
549 |
fun ml_from_def (name, Typesyn (vs, ty)) = |
|
550 |
(map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs; |
|
551 |
Pretty.block ( |
|
552 |
Pretty.str "type " |
|
553 |
:: postify (map (Pretty.str o fst) vs) (Pretty.str name) |
|
554 |
@ [Pretty.str " =", |
|
555 |
Pretty.brk 1, |
|
18282 | 556 |
ml_from_type NOBR ty, |
18216 | 557 |
Pretty.str ";" |
558 |
])) |
|
559 |
| ml_from_def (name, Nop) = |
|
18304 | 560 |
if exists (fn query => query name) |
561 |
[(fn name => (is_some o tyco_syntax) name), |
|
562 |
(fn name => (is_some o const_syntax) name)] |
|
18216 | 563 |
then Pretty.str "" |
564 |
else error ("empty statement during serialization: " ^ quote name) |
|
565 |
| ml_from_def (name, Class _) = |
|
566 |
error ("can't serialize class declaration " ^ quote name ^ " to ML") |
|
567 |
| ml_from_def (name, Classinst _) = |
|
568 |
error ("can't serialize instance declaration " ^ quote name ^ " to ML") |
|
18335 | 569 |
in (debug 10 (fn _ => "******************") (); (*map (writeln o Pretty.o)*) |
18282 | 570 |
case (snd o hd) ds |
18216 | 571 |
of Fun _ => ml_from_funs ds |
572 |
| Datatypecons _ => ml_from_datatypes ds |
|
573 |
| Datatype _ => ml_from_datatypes ds |
|
18282 | 574 |
| _ => (case ds of [d] => ml_from_def d)) |
18216 | 575 |
end; |
576 |
||
577 |
in |
|
578 |
||
18304 | 579 |
fun ml_from_thingol nspgrp name_root tyco_syntax const_syntax prims select module = |
18216 | 580 |
let |
18282 | 581 |
fun ml_validator name = |
582 |
let |
|
583 |
fun replace_invalid c = |
|
584 |
if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'" |
|
585 |
andalso not (NameSpace.separator = c) |
|
586 |
then c |
|
587 |
else "_" |
|
588 |
fun suffix_it name = |
|
589 |
name |
|
590 |
|> member (op =) ThmDatabase.ml_reserved ? suffix "'" |
|
591 |
|> member (op =) CodegenThingol.prims ? suffix "'" |
|
592 |
|> has_prim prims ? suffix "'" |
|
593 |
|> (fn name' => if name = name' then name else suffix_it name') |
|
594 |
in |
|
595 |
name |
|
596 |
|> translate_string replace_invalid |
|
597 |
|> suffix_it |
|
598 |
|> (fn name' => if name = name' then NONE else SOME name') |
|
599 |
end; |
|
18216 | 600 |
fun ml_from_module (name, ps) = |
601 |
Pretty.chunks ([ |
|
602 |
Pretty.str ("structure " ^ name ^ " = "), |
|
603 |
Pretty.str "struct", |
|
604 |
Pretty.str "" |
|
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
605 |
] @ separate (Pretty.str "") ps @ [ |
18216 | 606 |
Pretty.str "", |
607 |
Pretty.str ("end; (* struct " ^ name ^ " *)") |
|
608 |
]); |
|
609 |
fun eta_expander "Pair" = 2 |
|
610 |
| eta_expander "Cons" = 2 |
|
611 |
| eta_expander "primeq" = 2 |
|
612 |
| eta_expander "and" = 2 |
|
613 |
| eta_expander "or" = 2 |
|
614 |
| eta_expander "if" = 3 |
|
615 |
| eta_expander "add" = 2 |
|
616 |
| eta_expander "mult" = 2 |
|
617 |
| eta_expander "lt" = 2 |
|
618 |
| eta_expander "le" = 2 |
|
619 |
| eta_expander s = |
|
620 |
if NameSpace.is_qualified s |
|
621 |
then case get_def module s |
|
622 |
of Datatypecons (_ , tys) => |
|
623 |
if length tys >= 2 then length tys else 0 |
|
624 |
| _ => |
|
18304 | 625 |
const_syntax s |
626 |
|> Option.map fst |
|
18282 | 627 |
|> the_default 0 |
18216 | 628 |
else 0 |
18282 | 629 |
in |
18216 | 630 |
module |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
631 |
|> debug 12 (Pretty.output o pretty_module) |
18216 | 632 |
|> debug 3 (fn _ => "connecting datatypes and classdecls...") |
633 |
|> connect_datatypes_clsdecls |
|
634 |
|> debug 3 (fn _ => "selecting submodule...") |
|
18217 | 635 |
|> (if is_some select then (partof o the) select else I) |
18216 | 636 |
|> debug 3 (fn _ => "eta-expanding...") |
637 |
|> eta_expand eta_expander |
|
18231 | 638 |
|> debug 3 (fn _ => "eta-expanding polydefs...") |
639 |
|> eta_expand_poly |
|
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
640 |
|> debug 12 (Pretty.output o pretty_module) |
18216 | 641 |
|> debug 3 (fn _ => "tupelizing datatypes...") |
642 |
|> tupelize_cons |
|
643 |
|> debug 3 (fn _ => "eliminating classes...") |
|
644 |
|> eliminate_classes |
|
645 |
|> debug 3 (fn _ => "generating...") |
|
18282 | 646 |
|> serialize (ml_from_defs tyco_syntax const_syntax) ml_from_module ml_validator nspgrp name_root |
18335 | 647 |
|> (fn p => Pretty.chunks [(Pretty.str o mk_prims) prims, p]) |
18216 | 648 |
end; |
649 |
||
18231 | 650 |
fun ml_from_thingol' nspgrp name_root = |
651 |
Scan.optional ( |
|
652 |
OuterParse.$$$ "(" |-- OuterParse.list1 OuterParse.text --| OuterParse.$$$ ")" |
|
653 |
) [] |
|
654 |
>> (fn _ => ml_from_thingol nspgrp name_root); |
|
655 |
||
18216 | 656 |
(* ML infix precedence |
657 |
7 / * div mod |
|
658 |
6 + - ^ |
|
659 |
5 :: @ |
|
660 |
4 = <> < > <= >= |
|
661 |
3 := o *) |
|
662 |
||
663 |
end; (* local *) |
|
664 |
||
18282 | 665 |
local |
666 |
||
667 |
val bslash = "\\"; |
|
668 |
||
18304 | 669 |
fun haskell_from_defs tyco_syntax const_syntax is_cons resolv defs = |
18282 | 670 |
let |
671 |
val resolv = fn s => |
|
672 |
let |
|
673 |
val (prfix, base) = (split_last o NameSpace.unpack o resolv) s |
|
674 |
in |
|
675 |
NameSpace.pack (map upper_first prfix @ [base]) |
|
676 |
end; |
|
677 |
fun resolv_const f = |
|
18335 | 678 |
if NameSpace.is_qualified f |
679 |
then |
|
680 |
if is_cons f |
|
681 |
then (upper_first o resolv) f |
|
682 |
else (lower_first o resolv) f |
|
683 |
else |
|
684 |
f; |
|
18282 | 685 |
fun haskell_from_sctxt vs = |
686 |
let |
|
687 |
fun from_sctxt [] = Pretty.str "" |
|
688 |
| from_sctxt vs = |
|
689 |
vs |
|
690 |
|> map (fn (v, cls) => Pretty.str ((upper_first o resolv) cls ^ " " ^ lower_first v)) |
|
691 |
|> Pretty.gen_list "," "(" ")" |
|
692 |
|> (fn p => Pretty.block [p, Pretty.str " => "]) |
|
693 |
in |
|
694 |
vs |
|
695 |
|> map (fn (v, sort) => map (pair v) sort) |
|
696 |
|> Library.flat |
|
697 |
|> from_sctxt |
|
698 |
end; |
|
699 |
fun haskell_from_type br ty = |
|
700 |
let |
|
701 |
fun from_itype br (IType ("Pair", [t1, t2])) sctxt = |
|
702 |
sctxt |
|
703 |
|> from_itype NOBR t1 |
|
704 |
||>> from_itype NOBR t2 |
|
705 |
|-> (fn (p1, p2) => pair (Pretty.gen_list "," "(" ")" [p1, p2])) |
|
706 |
| from_itype br (IType ("List", [ty])) sctxt = |
|
707 |
sctxt |
|
708 |
|> from_itype NOBR ty |
|
709 |
|-> (fn p => pair (Pretty.enclose "[" "]" [p])) |
|
710 |
| from_itype br (IType (tyco, tys)) sctxt = |
|
711 |
let |
|
712 |
fun mk_itype NONE tyargs sctxt = |
|
713 |
sctxt |
|
714 |
|> pair (brackify (eval_br br BR) ((Pretty.str o upper_first o resolv) tyco :: tyargs)) |
|
18304 | 715 |
| mk_itype (SOME (i, pr)) tyargs sctxt = |
18282 | 716 |
if i <> length (tys) |
717 |
then error "can only serialize strictly complete type applications to haskell" |
|
718 |
else |
|
719 |
sctxt |
|
18304 | 720 |
|> pair (pr tyargs (haskell_from_type BR)) |
18282 | 721 |
in |
722 |
sctxt |
|
723 |
|> fold_map (from_itype BR) tys |
|
18304 | 724 |
|-> mk_itype (tyco_syntax tyco) |
18282 | 725 |
end |
726 |
| from_itype br (IFun (t1, t2)) sctxt = |
|
727 |
sctxt |
|
728 |
|> from_itype (INFX (1, X)) t1 |
|
729 |
||>> from_itype (INFX (1, R)) t2 |
|
730 |
|-> (fn (p1, p2) => pair ( |
|
731 |
brackify (eval_br br (INFX (1, R))) [ |
|
732 |
p1, |
|
733 |
Pretty.str "->", |
|
734 |
p2 |
|
735 |
] |
|
736 |
)) |
|
737 |
| from_itype br (IVarT (v, [])) sctxt = |
|
738 |
sctxt |
|
739 |
|> pair ((Pretty.str o lower_first) v) |
|
740 |
| from_itype br (IVarT (v, sort)) sctxt = |
|
741 |
sctxt |
|
742 |
|> AList.default (op =) (v, []) |
|
743 |
|> AList.map_entry (op =) v (fold (insert (op =)) sort) |
|
744 |
|> pair ((Pretty.str o lower_first) v) |
|
745 |
| from_itype br (IDictT _) _ = |
|
746 |
error "cannot serialize dictionary type to haskell" |
|
747 |
in |
|
748 |
[] |
|
749 |
|> from_itype br ty |
|
750 |
||> haskell_from_sctxt |
|
751 |
|> (fn (pty, pctxt) => Pretty.block [pctxt, pty]) |
|
752 |
end; |
|
753 |
fun haskell_from_pat br (ICons (("Pair", [p1, p2]), _)) = |
|
754 |
Pretty.list "(" ")" [ |
|
755 |
haskell_from_pat NOBR p1, |
|
756 |
haskell_from_pat NOBR p2 |
|
757 |
] |
|
758 |
| haskell_from_pat br (ICons (("Nil", []), _)) = |
|
759 |
Pretty.str "[]" |
|
760 |
| haskell_from_pat br (p as ICons (("Cons", _), _)) = |
|
761 |
let |
|
762 |
fun dest_cons (ICons (("Cons", [p1, p2]), ty)) = SOME (p1, p2) |
|
763 |
| dest_cons p = NONE |
|
764 |
in |
|
765 |
case unfoldr dest_cons p |
|
766 |
of (ps, (ICons (("Nil", []), _))) => |
|
767 |
ps |
|
768 |
|> map (haskell_from_pat NOBR) |
|
769 |
|> Pretty.list "[" "]" |
|
770 |
| (ps, p) => |
|
771 |
(ps @ [p]) |
|
772 |
|> map (haskell_from_pat (INFX (5, X))) |
|
773 |
|> separate (Pretty.str ":") |
|
774 |
|> brackify (eval_br br (INFX (5, R))) |
|
775 |
end |
|
776 |
| haskell_from_pat br (ICons ((f, ps), _)) = |
|
18335 | 777 |
(case const_syntax f |
778 |
of NONE => |
|
779 |
ps |
|
780 |
|> map (haskell_from_pat BR) |
|
781 |
|> cons ((Pretty.str o resolv_const) f) |
|
782 |
|> brackify (eval_br br BR) |
|
783 |
| SOME (i, pr) => |
|
784 |
if i = length ps |
|
785 |
then |
|
786 |
pr (map (haskell_from_pat BR) ps) (haskell_from_expr BR) |
|
787 |
else |
|
788 |
error "number of argument mismatch in customary serialization") |
|
18282 | 789 |
| haskell_from_pat br (IVarP (v, _)) = |
18335 | 790 |
(Pretty.str o lower_first) v |
791 |
and haskell_from_expr br (e as (IApp (IApp (IConst ("Cons", _), _), _))) = |
|
18282 | 792 |
let |
793 |
fun dest_cons (IApp (IApp (IConst ("Cons", _), e1), e2)) = SOME (e1, e2) |
|
794 |
| dest_cons p = NONE |
|
795 |
in |
|
796 |
case unfoldr dest_cons e |
|
797 |
of (es, (IConst ("Nil", _))) => |
|
798 |
es |
|
799 |
|> map (haskell_from_expr NOBR) |
|
800 |
|> Pretty.list "[" "]" |
|
801 |
| (es, e) => |
|
802 |
(es @ [e]) |
|
803 |
|> map (haskell_from_expr (INFX (5, X))) |
|
804 |
|> separate (Pretty.str ":") |
|
805 |
|> brackify (eval_br br (INFX (5, R))) |
|
806 |
end |
|
807 |
| haskell_from_expr br (e as IApp (e1, e2)) = |
|
808 |
(case (unfold_app e) |
|
809 |
of (e as (IConst (f, _)), es) => |
|
810 |
haskell_from_app br (f, es) |
|
811 |
| _ => |
|
812 |
brackify (eval_br br BR) [ |
|
813 |
haskell_from_expr NOBR e1, |
|
814 |
haskell_from_expr BR e2 |
|
815 |
]) |
|
816 |
| haskell_from_expr br (e as IConst (f, _)) = |
|
817 |
haskell_from_app br (f, []) |
|
818 |
| haskell_from_expr br (IVarE (v, _)) = |
|
819 |
(Pretty.str o lower_first) v |
|
820 |
| haskell_from_expr br (e as IAbs _) = |
|
821 |
let |
|
822 |
val (vs, body) = unfold_abs e |
|
823 |
in |
|
824 |
brackify (eval_br br BR) ( |
|
825 |
Pretty.str bslash |
|
826 |
:: map (Pretty.str o lower_first o fst) vs @ [ |
|
827 |
Pretty.str "->", |
|
828 |
haskell_from_expr NOBR body |
|
829 |
]) |
|
830 |
end |
|
831 |
| haskell_from_expr br (e as ICase (_, [_])) = |
|
832 |
let |
|
833 |
val (ps, body) = unfold_let e; |
|
834 |
fun mk_bind (p, e) = Pretty.block [ |
|
835 |
haskell_from_pat BR p, |
|
836 |
Pretty.str " =", |
|
837 |
Pretty.brk 1, |
|
838 |
haskell_from_expr NOBR e |
|
839 |
]; |
|
840 |
in Pretty.chunks [ |
|
841 |
[Pretty.str ("let"), Pretty.fbrk, map mk_bind ps |> Pretty.chunks] |> Pretty.block, |
|
842 |
[Pretty.str ("in "), haskell_from_expr NOBR body] |> Pretty.block |
|
843 |
] end |
|
844 |
| haskell_from_expr br (ICase (e, c::cs)) = |
|
845 |
let |
|
846 |
fun mk_clause (p, e) = |
|
847 |
Pretty.block [ |
|
848 |
haskell_from_pat NOBR p, |
|
849 |
Pretty.str " ->", |
|
850 |
Pretty.brk 1, |
|
851 |
haskell_from_expr NOBR e |
|
852 |
] |
|
853 |
in (Pretty.block o Pretty.fbreaks) ( |
|
854 |
Pretty.block [Pretty.str "case ", haskell_from_expr NOBR e, Pretty.str " of"] |
|
855 |
:: map (mk_clause) cs |
|
856 |
)end |
|
857 |
| haskell_from_expr br (IInst (e, _)) = |
|
858 |
haskell_from_expr br e |
|
859 |
| haskell_from_expr br (IDictE _) = |
|
860 |
error "cannot serialize dictionary expression to haskell" |
|
861 |
| haskell_from_expr br (ILookup _) = |
|
862 |
error "cannot serialize lookup expression to haskell" |
|
863 |
and mk_app_p br p args = |
|
864 |
brackify (eval_br br BR) |
|
865 |
(p :: map (haskell_from_expr BR) args) |
|
866 |
and haskell_from_app br ("Nil", []) = |
|
867 |
Pretty.str "[]" |
|
868 |
| haskell_from_app br ("Cons", es) = |
|
869 |
mk_app_p br (Pretty.str "(:)") es |
|
870 |
| haskell_from_app br ("primeq", [e1, e2]) = |
|
871 |
brackify (eval_br br (INFX (4, L))) [ |
|
872 |
haskell_from_expr (INFX (4, L)) e1, |
|
873 |
Pretty.str "==", |
|
874 |
haskell_from_expr (INFX (4, X)) e2 |
|
875 |
] |
|
18335 | 876 |
| haskell_from_app br ("eq", [e1, e2]) = |
877 |
brackify (eval_br br (INFX (4, L))) [ |
|
878 |
haskell_from_expr (INFX (4, L)) e1, |
|
879 |
Pretty.str "==", |
|
880 |
haskell_from_expr (INFX (4, X)) e2 |
|
881 |
] |
|
18282 | 882 |
| haskell_from_app br ("Pair", [e1, e2]) = |
883 |
Pretty.list "(" ")" [ |
|
884 |
haskell_from_expr NOBR e1, |
|
885 |
haskell_from_expr NOBR e2 |
|
886 |
] |
|
887 |
| haskell_from_app br ("if", [b, e1, e2]) = |
|
888 |
brackify (eval_br br BR) [ |
|
889 |
Pretty.str "if", |
|
890 |
haskell_from_expr NOBR b, |
|
891 |
Pretty.str "then", |
|
892 |
haskell_from_expr NOBR e1, |
|
893 |
Pretty.str "else", |
|
894 |
haskell_from_expr NOBR e2 |
|
895 |
] |
|
18335 | 896 |
| haskell_from_app br ("and", es) = |
897 |
haskell_from_binop br 3 R "&&" es |
|
898 |
| haskell_from_app br ("or", es) = |
|
899 |
haskell_from_binop br 2 R "||" es |
|
900 |
| haskell_from_app br ("add", es) = |
|
901 |
haskell_from_binop br 6 L "+" es |
|
902 |
| haskell_from_app br ("mult", es) = |
|
903 |
haskell_from_binop br 7 L "*" es |
|
904 |
| haskell_from_app br ("lt", es) = |
|
905 |
haskell_from_binop br 4 L "<" es |
|
906 |
| haskell_from_app br ("le", es) = |
|
907 |
haskell_from_binop br 4 L "<=" es |
|
18282 | 908 |
| haskell_from_app br ("minus", es) = |
909 |
mk_app_p br (Pretty.str "negate") es |
|
910 |
| haskell_from_app br ("wfrec", es) = |
|
911 |
mk_app_p br (Pretty.str "wfrec") es |
|
912 |
| haskell_from_app br (f, es) = |
|
18304 | 913 |
case const_syntax f |
18282 | 914 |
of NONE => |
18335 | 915 |
(case es |
916 |
of [] => Pretty.str (resolv_const f) |
|
917 |
| es => |
|
918 |
let |
|
919 |
val (es', e) = split_last es; |
|
920 |
in mk_app_p br (haskell_from_app NOBR (f, es')) [e] end) |
|
18304 | 921 |
| SOME (i, pr) => |
18282 | 922 |
let |
923 |
val (es1, es2) = splitAt (i, es); |
|
18335 | 924 |
in mk_app_p br (pr (map (haskell_from_expr BR) es1) (haskell_from_expr BR)) es2 end |
925 |
and haskell_from_binop br pr L f [e1, e2] = |
|
926 |
brackify (eval_br br (INFX (pr, L))) [ |
|
927 |
haskell_from_expr (INFX (pr, L)) e1, |
|
928 |
Pretty.str f, |
|
929 |
haskell_from_expr (INFX (pr, X)) e2 |
|
930 |
] |
|
931 |
| haskell_from_binop br pr R f [e1, e2] = |
|
932 |
brackify (eval_br br (INFX (pr, R))) [ |
|
933 |
haskell_from_expr (INFX (pr, X)) e1, |
|
934 |
Pretty.str f, |
|
935 |
haskell_from_expr (INFX (pr, R)) e2 |
|
936 |
] |
|
937 |
| haskell_from_binop br pr ass f args = |
|
938 |
mk_app_p br (Pretty.str ("(" ^ f ^ ")")) args |
|
18282 | 939 |
fun haskell_from_datatypes defs = |
940 |
let |
|
941 |
fun mk_cons (co, typs) = |
|
942 |
(Pretty.block o Pretty.breaks) ( |
|
943 |
Pretty.str ((upper_first o resolv) co) |
|
944 |
:: map (haskell_from_type NOBR) typs |
|
945 |
) |
|
946 |
fun mk_datatype (t, (vs, cs)) = |
|
947 |
Pretty.block ( |
|
948 |
Pretty.str "data " |
|
949 |
:: haskell_from_sctxt vs |
|
950 |
:: Pretty.str (upper_first t) |
|
951 |
:: Pretty.block (map (fn (v, _) => Pretty.str (" " ^ (lower_first) v)) vs) |
|
952 |
:: Pretty.str " =" |
|
953 |
:: Pretty.brk 1 |
|
954 |
:: separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons cs) |
|
955 |
) |
|
956 |
in |
|
957 |
Pretty.chunks ((separate (Pretty.str "") o map mk_datatype o group_datatypes false) defs) |
|
958 |
end; |
|
18304 | 959 |
fun haskell_from_classes defs = |
960 |
let |
|
961 |
fun mk_member (f, ty) = |
|
962 |
Pretty.block [ |
|
963 |
Pretty.str (f ^ " ::"), |
|
964 |
Pretty.brk 1, |
|
965 |
haskell_from_type NOBR ty |
|
966 |
]; |
|
967 |
fun mk_class (clsname, ((supclsnames, v), members)) = |
|
968 |
Pretty.block [ |
|
969 |
Pretty.str "class ", |
|
970 |
haskell_from_sctxt (map (fn class => (v, [class])) supclsnames), |
|
971 |
Pretty.str ((upper_first clsname) ^ " " ^ v), |
|
972 |
Pretty.str " where", |
|
973 |
Pretty.fbrk, |
|
974 |
Pretty.chunks (map mk_member members) |
|
975 |
]; |
|
976 |
in |
|
977 |
Pretty.chunks ((separate (Pretty.str "") o map mk_class o group_classes) defs) |
|
978 |
end; |
|
18282 | 979 |
fun haskell_from_def (name, Nop) = |
18304 | 980 |
if exists (fn query => query name) |
981 |
[(fn name => (is_some o tyco_syntax) name), |
|
982 |
(fn name => (is_some o const_syntax) name)] |
|
18282 | 983 |
then Pretty.str "" |
984 |
else error ("empty statement during serialization: " ^ quote name) |
|
985 |
| haskell_from_def (name, Fun (eqs, (_, ty))) = |
|
986 |
let |
|
987 |
fun from_eq name (args, rhs) = |
|
988 |
Pretty.block [ |
|
989 |
Pretty.str (lower_first name), |
|
990 |
Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, haskell_from_pat BR p]) args), |
|
991 |
Pretty.brk 1, |
|
992 |
Pretty.str ("="), |
|
993 |
Pretty.brk 1, |
|
994 |
haskell_from_expr NOBR rhs |
|
995 |
] |
|
996 |
in |
|
997 |
Pretty.chunks [ |
|
998 |
Pretty.block [ |
|
999 |
Pretty.str (name ^ " ::"), |
|
1000 |
Pretty.brk 1, |
|
1001 |
haskell_from_type NOBR ty |
|
1002 |
], |
|
1003 |
Pretty.chunks (map (from_eq name) eqs) |
|
1004 |
] |
|
1005 |
end |
|
1006 |
| haskell_from_def (name, Typesyn (vs, ty)) = |
|
1007 |
Pretty.block [ |
|
1008 |
Pretty.str "type ", |
|
1009 |
haskell_from_sctxt vs, |
|
1010 |
Pretty.str (upper_first name), |
|
1011 |
Pretty.block (map (fn (v, _) => Pretty.str (" " ^ (lower_first) v)) vs), |
|
1012 |
Pretty.str " =", |
|
1013 |
Pretty.brk 1, |
|
1014 |
haskell_from_type NOBR ty |
|
1015 |
] |
|
1016 |
| haskell_from_def (_, Classinst (clsname, (tyco, arity), instmems)) = |
|
1017 |
Pretty.block [ |
|
1018 |
Pretty.str "instance ", |
|
1019 |
haskell_from_sctxt arity, |
|
1020 |
Pretty.str ((upper_first o resolv) clsname), |
|
1021 |
Pretty.str " ", |
|
1022 |
Pretty.str ((upper_first o resolv) tyco), |
|
1023 |
Pretty.str " where", |
|
1024 |
Pretty.fbrk, |
|
1025 |
Pretty.chunks (map (fn (member, const) => |
|
1026 |
Pretty.str ((lower_first o resolv) member ^ " = " ^ (lower_first o resolv) const) |
|
1027 |
) instmems) |
|
1028 |
]; |
|
1029 |
in case (snd o hd) defs |
|
1030 |
of Datatypecons _ => haskell_from_datatypes defs |
|
1031 |
| Datatype _ => haskell_from_datatypes defs |
|
1032 |
| Class _ => haskell_from_classes defs |
|
1033 |
| Classmember _ => haskell_from_classes defs |
|
1034 |
| _ => Pretty.block (map haskell_from_def defs |> separate (Pretty.str "")) |
|
1035 |
end; |
|
1036 |
||
1037 |
in |
|
1038 |
||
18304 | 1039 |
fun haskell_from_thingol nspgrp name_root tyco_syntax const_syntax prims select module = |
18282 | 1040 |
let |
1041 |
fun haskell_from_module (name, ps) = |
|
1042 |
Pretty.block [ |
|
1043 |
Pretty.str ("module " ^ (upper_first name) ^ " where"), |
|
1044 |
Pretty.fbrk, |
|
1045 |
Pretty.fbrk, |
|
1046 |
Pretty.chunks (separate (Pretty.str "") ps) |
|
1047 |
]; |
|
1048 |
fun haskell_validator s = NONE; |
|
1049 |
fun eta_expander "Pair" = 2 |
|
1050 |
| eta_expander "if" = 3 |
|
1051 |
| eta_expander s = |
|
1052 |
if NameSpace.is_qualified s |
|
1053 |
then case get_def module s |
|
1054 |
of Datatypecons (_ , tys) => |
|
1055 |
if length tys >= 2 then length tys else 0 |
|
1056 |
| _ => |
|
18304 | 1057 |
const_syntax s |
1058 |
|> Option.map fst |
|
18282 | 1059 |
|> the_default 0 |
1060 |
else 0; |
|
1061 |
fun is_cons f = |
|
1062 |
NameSpace.is_qualified f |
|
1063 |
andalso case get_def module f |
|
1064 |
of Datatypecons _ => true |
|
1065 |
| _ => false; |
|
1066 |
in |
|
1067 |
module |
|
1068 |
|> debug 12 (Pretty.output o pretty_module) |
|
1069 |
|> debug 3 (fn _ => "connecting datatypes and classdecls...") |
|
1070 |
|> connect_datatypes_clsdecls |
|
1071 |
|> debug 3 (fn _ => "selecting submodule...") |
|
1072 |
|> (if is_some select then (partof o the) select else I) |
|
1073 |
|> debug 3 (fn _ => "eta-expanding...") |
|
1074 |
|> eta_expand eta_expander |
|
1075 |
|> debug 3 (fn _ => "generating...") |
|
1076 |
|> serialize (haskell_from_defs tyco_syntax const_syntax is_cons) haskell_from_module haskell_validator nspgrp name_root |
|
18335 | 1077 |
|> (fn p => Pretty.chunks [(Pretty.str o mk_prims) prims, p]) |
18282 | 1078 |
end; |
1079 |
||
1080 |
end; (* local *) |
|
1081 |
||
18216 | 1082 |
end; (* struct *) |
1083 |