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