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