author | paulson |
Mon, 30 Jan 2006 10:13:28 +0100 | |
changeset 18853 | afe45058241a |
parent 18850 | 92ef83e5eaea |
child 18865 | 31aed965135c |
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 |
18702 | 11 |
type 'a pretty_syntax; |
12 |
type serializer = |
|
13 |
string list list |
|
18756 | 14 |
-> OuterParse.token list -> |
15 |
((string -> CodegenThingol.itype pretty_syntax option) |
|
18702 | 16 |
* (string -> CodegenThingol.iexpr pretty_syntax option) |
17 |
-> string list option |
|
18756 | 18 |
-> CodegenThingol.module -> unit) |
19 |
* OuterParse.token list; |
|
18702 | 20 |
val parse_syntax: (string -> 'b -> 'a * 'b) -> OuterParse.token list -> |
21 |
('b -> 'a pretty_syntax * 'b) * OuterParse.token list; |
|
22 |
val parse_targetdef: (string -> string) -> string -> string; |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
23 |
val pretty_list: string -> string -> int * string -> CodegenThingol.iexpr pretty_syntax; |
18702 | 24 |
val serializers: { |
25 |
ml: string * (string * string * string -> serializer), |
|
26 |
haskell: string * (string -> serializer) |
|
27 |
} |
|
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 |
|
18850 | 33 |
open CodegenThingol; |
18702 | 34 |
infix 8 `%%; |
35 |
infixr 6 `->; |
|
36 |
infixr 6 `-->; |
|
37 |
infix 4 `$; |
|
38 |
infix 4 `$$; |
|
39 |
infixr 5 `|->; |
|
40 |
infixr 5 `|-->; |
|
18216 | 41 |
|
18850 | 42 |
|
18216 | 43 |
(** generic serialization **) |
44 |
||
18702 | 45 |
(* precedences *) |
46 |
||
18216 | 47 |
datatype lrx = L | R | X; |
48 |
||
18516 | 49 |
datatype fixity = |
18216 | 50 |
BR |
51 |
| NOBR |
|
52 |
| INFX of (int * lrx); |
|
53 |
||
18702 | 54 |
datatype 'a mixfix = |
55 |
Arg of fixity |
|
56 |
| Ignore |
|
57 |
| Pretty of Pretty.T |
|
58 |
| Quote of 'a; |
|
18516 | 59 |
|
18702 | 60 |
type 'a pretty_syntax = (int * int) * (fixity -> (fixity -> 'a -> Pretty.T) -> 'a list -> Pretty.T); |
18516 | 61 |
|
18216 | 62 |
fun eval_lrx L L = false |
63 |
| eval_lrx R R = false |
|
64 |
| eval_lrx _ _ = true; |
|
65 |
||
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
66 |
fun eval_fxy NOBR _ = false |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
67 |
| eval_fxy _ BR = true |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
68 |
| eval_fxy _ NOBR = false |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
69 |
| eval_fxy (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
70 |
pr < pr_ctxt |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
71 |
orelse pr = pr_ctxt |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
72 |
andalso eval_lrx lr lr_ctxt |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
73 |
| eval_fxy _ (INFX _) = false; |
18216 | 74 |
|
18702 | 75 |
val str = setmp print_mode [] Pretty.str; |
18216 | 76 |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
77 |
fun gen_brackify _ [p] = p |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
78 |
| gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
79 |
| gen_brackify false (ps as _::_) = Pretty.block ps; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
80 |
|
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
81 |
fun brackify fxy_ctxt ps = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
82 |
gen_brackify (eval_fxy BR fxy_ctxt) (Pretty.breaks ps); |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
83 |
|
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
84 |
fun brackify_infix infx fxy_ctxt ps = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
85 |
gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps); |
18216 | 86 |
|
18702 | 87 |
fun from_app mk_app from_expr const_syntax fxy (f, es) = |
88 |
let |
|
89 |
fun mk NONE es = |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
90 |
brackify fxy (mk_app f es) |
18702 | 91 |
| mk (SOME ((i, k), pr)) es = |
92 |
let |
|
93 |
val (es1, es2) = splitAt (i, es); |
|
94 |
in |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
95 |
brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2) |
18702 | 96 |
end; |
97 |
in mk (const_syntax f) es end; |
|
98 |
||
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
99 |
fun fillin_mixfix fxy_this ms fxy_ctxt pr args = |
18702 | 100 |
let |
101 |
fun fillin [] [] = |
|
102 |
[] |
|
103 |
| fillin (Arg fxy :: ms) (a :: args) = |
|
104 |
pr fxy a :: fillin ms args |
|
105 |
| fillin (Ignore :: ms) args = |
|
106 |
fillin ms args |
|
107 |
| fillin (Pretty p :: ms) args = |
|
108 |
p :: fillin ms args |
|
109 |
| fillin (Quote q :: ms) args = |
|
110 |
pr BR q :: fillin ms args; |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
111 |
in gen_brackify (eval_fxy fxy_this fxy_ctxt) (fillin ms args) end; |
18702 | 112 |
|
113 |
||
114 |
(* user-defined syntax *) |
|
115 |
||
116 |
val (atomK, infixK, infixlK, infixrK) = |
|
18756 | 117 |
("target_atom", "infix", "infixl", "infixr"); |
118 |
val _ = OuterSyntax.add_keywords [atomK, infixK, infixlK, infixrK]; |
|
18216 | 119 |
|
18702 | 120 |
fun parse_infix (fixity as INFX (i, x)) s = |
121 |
let |
|
122 |
val l = case x of L => fixity |
|
123 |
| _ => INFX (i, X); |
|
124 |
val r = case x of R => fixity |
|
125 |
| _ => INFX (i, X); |
|
126 |
in |
|
127 |
pair [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r] |
|
128 |
end; |
|
129 |
||
130 |
fun parse_mixfix reader s ctxt = |
|
18335 | 131 |
let |
18702 | 132 |
fun sym s = Scan.lift ($$ s); |
133 |
fun lift_reader ctxt s = |
|
134 |
ctxt |
|
135 |
|> reader s |
|
136 |
|-> (fn x => pair (Quote x)); |
|
137 |
val sym_any = Scan.lift (Scan.one Symbol.not_eof); |
|
138 |
val parse = Scan.repeat ( |
|
139 |
(sym "_" -- sym "_" >> K (Arg NOBR)) |
|
140 |
|| (sym "_" >> K (Arg BR)) |
|
141 |
|| (sym "?" >> K Ignore) |
|
142 |
|| (sym "/" |-- Scan.repeat (sym " ") >> (Pretty o Pretty.brk o length)) |
|
143 |
|| Scan.depend (fn ctxt => $$ "{" |-- $$ "*" |-- Scan.repeat1 |
|
144 |
( $$ "'" |-- Scan.one Symbol.not_eof |
|
145 |
|| Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --| |
|
146 |
$$ "*" --| $$ "}" >> (implode #> lift_reader ctxt #> swap)) |
|
147 |
|| (Scan.repeat1 |
|
148 |
( sym "'" |-- sym_any |
|
149 |
|| Scan.unless (sym "_" || sym "?" || sym "/" || sym "{" |-- sym "*") |
|
150 |
sym_any) >> (Pretty o str o implode))); |
|
151 |
in case Scan.finite' Symbol.stopper parse (ctxt, Symbol.explode s) |
|
152 |
of (p, (ctxt, [])) => (p, ctxt) |
|
153 |
| _ => error ("Malformed mixfix annotation: " ^ quote s) |
|
154 |
end; |
|
155 |
||
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
156 |
fun parse_nonatomic_mixfix reader s ctxt = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
157 |
case parse_mixfix reader s ctxt |
18850 | 158 |
of ([Pretty _], _) => error ("mixfix contains just one pretty element; either declare as " ^ quote atomK ^ " or consider adding a break") |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
159 |
| x => x; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
160 |
|
18702 | 161 |
fun parse_syntax_proto reader = OuterParse.$$$ "(" |-- ( |
162 |
OuterParse.$$$ infixK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X))) |
|
163 |
|| OuterParse.$$$ infixlK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L))) |
|
164 |
|| OuterParse.$$$ infixrK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R))) |
|
165 |
|| OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR) |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
166 |
|| pair (parse_nonatomic_mixfix reader, BR) |
18702 | 167 |
) -- OuterParse.string --| OuterParse.$$$ ")" >> (fn ((p, fxy), s) => (p s, fxy)); |
18282 | 168 |
|
18702 | 169 |
fun parse_syntax reader = |
18335 | 170 |
let |
18702 | 171 |
fun is_arg (Arg _) = true |
172 |
| is_arg Ignore = true |
|
173 |
| is_arg _ = false; |
|
174 |
fun mk fixity mfx = |
|
175 |
let |
|
176 |
val i = length (List.filter is_arg mfx) |
|
177 |
in ((i, i), fillin_mixfix fixity mfx) end; |
|
178 |
in |
|
179 |
parse_syntax_proto reader |
|
180 |
#-> (fn (mfx_reader, fixity) : ('Z -> 'Y mixfix list * 'Z) * fixity => |
|
181 |
pair (mfx_reader #-> (fn mfx => pair (mk fixity mfx))) |
|
182 |
) |
|
183 |
end; |
|
184 |
||
185 |
fun newline_correct s = |
|
186 |
s |
|
187 |
|> Symbol.strip_blanks |
|
188 |
|> space_explode "\n" |
|
189 |
|> map (implode o (fn [] => [] |
|
190 |
| (" "::xs) => xs |
|
191 |
| xs => xs) o explode) |
|
192 |
|> space_implode "\n"; |
|
193 |
||
194 |
fun parse_named_quote resolv s = |
|
195 |
case Scan.finite Symbol.stopper (Scan.repeat ( |
|
196 |
($$ "`" |-- $$ "`") |
|
197 |
|| ($$ "`" |-- Scan.repeat1 (Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) |
|
198 |
--| $$ "`" >> (resolv o implode)) |
|
199 |
|| Scan.repeat1 |
|
200 |
(Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) >> implode |
|
201 |
) >> implode) (Symbol.explode s) |
|
202 |
of (p, []) => p |
|
203 |
| (p, ss) => error ("Malformed definition: " ^ quote p ^ " - " ^ commas ss); |
|
204 |
||
205 |
fun parse_targetdef resolv = parse_named_quote resolv o newline_correct; |
|
206 |
||
207 |
||
208 |
(* abstract serializer *) |
|
18282 | 209 |
|
18702 | 210 |
type serializer = |
211 |
string list list |
|
18756 | 212 |
-> OuterParse.token list -> |
213 |
((string -> CodegenThingol.itype pretty_syntax option) |
|
18702 | 214 |
* (string -> CodegenThingol.iexpr pretty_syntax option) |
215 |
-> string list option |
|
18756 | 216 |
-> CodegenThingol.module -> unit) |
217 |
* OuterParse.token list; |
|
18702 | 218 |
|
18850 | 219 |
fun pretty_of_prim target resolv (name, primdef) = |
220 |
let |
|
221 |
fun pr (CodegenThingol.Pretty p) = p |
|
222 |
| pr (CodegenThingol.Name s) = resolv s; |
|
223 |
in case AList.lookup (op = : string * string -> bool) primdef target |
|
224 |
of NONE => error ("no primitive definition for " ^ quote name) |
|
225 |
| SOME ps => (Pretty.block o map pr) ps |
|
226 |
end; |
|
227 |
||
228 |
fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator) |
|
229 |
postprocess preprocess (tyco_syntax, const_syntax) select module = |
|
18702 | 230 |
let |
231 |
fun from_prim (name, prim) = |
|
18756 | 232 |
case AList.lookup (op = : string * string -> bool) prim target |
18702 | 233 |
of NONE => error ("no primitive definition for " ^ quote name) |
234 |
| SOME p => p; |
|
18850 | 235 |
fun from_module' imps ((name_qual, name), defs) = |
236 |
from_module imps ((name_qual, name), defs) |> postprocess name_qual; |
|
18702 | 237 |
in |
238 |
module |
|
239 |
|> debug 3 (fn _ => "selecting submodule...") |
|
240 |
|> (if is_some select then (partof o the) select else I) |
|
241 |
|> tap (Pretty.writeln o pretty_deps) |
|
242 |
|> debug 3 (fn _ => "preprocessing...") |
|
243 |
|> preprocess |
|
244 |
|> debug 3 (fn _ => "serializing...") |
|
245 |
|> serialize (from_defs (from_prim, (tyco_syntax, const_syntax))) |
|
18850 | 246 |
from_module' validator nspgrp name_root |
247 |
|> K () |
|
18702 | 248 |
end; |
249 |
||
250 |
fun abstract_validator keywords name = |
|
251 |
let |
|
252 |
fun replace_invalid c = |
|
253 |
if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'" |
|
254 |
andalso not (NameSpace.separator = c) |
|
255 |
then c |
|
256 |
else "_" |
|
257 |
fun suffix_it name = |
|
258 |
name |
|
259 |
|> member (op =) keywords ? suffix "'" |
|
260 |
|> (fn name' => if name = name' then name else suffix_it name') |
|
261 |
in |
|
262 |
name |
|
263 |
|> translate_string replace_invalid |
|
264 |
|> suffix_it |
|
265 |
|> (fn name' => if name = name' then NONE else SOME name') |
|
266 |
end; |
|
267 |
||
18850 | 268 |
fun write_file mkdir path p = ( |
269 |
if mkdir |
|
270 |
then |
|
271 |
File.mkdir (Path.dir path) |
|
272 |
else (); |
|
273 |
File.write path (Pretty.output p ^ "\n"); |
|
274 |
p |
|
275 |
); |
|
276 |
||
277 |
fun mk_module_file postprocess_module ext path name p = |
|
278 |
let |
|
279 |
val prfx = Path.dir path; |
|
280 |
val name' = case name |
|
281 |
of "" => Path.base path |
|
282 |
| _ => (Path.ext ext o Path.unpack o implode o separate "/" o NameSpace.unpack) name; |
|
283 |
in |
|
284 |
p |
|
285 |
|> write_file true (Path.append prfx name') |
|
286 |
|> postprocess_module name |
|
287 |
end; |
|
288 |
||
18756 | 289 |
fun parse_single_file serializer = |
18850 | 290 |
OuterParse.path |
291 |
>> (fn path => serializer |
|
292 |
(fn "" => write_file false path #> K NONE |
|
293 |
| _ => SOME)); |
|
294 |
||
295 |
fun parse_multi_file postprocess_module ext serializer = |
|
296 |
OuterParse.path |
|
297 |
>> (fn path => (serializer o mk_module_file postprocess_module ext) path); |
|
18702 | 298 |
|
18756 | 299 |
fun parse_internal serializer = |
300 |
OuterParse.name |
|
18850 | 301 |
>> (fn "-" => serializer |
302 |
(fn "" => (fn p => (use_text Context.ml_output false (Pretty.output p); NONE)) |
|
303 |
| _ => SOME) |
|
18756 | 304 |
| _ => Scan.fail ()); |
18702 | 305 |
|
18282 | 306 |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
307 |
(* list serializer *) |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
308 |
|
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
309 |
fun pretty_list thingol_nil thingol_cons (target_pred, target_cons) = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
310 |
let |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
311 |
fun dest_cons (IApp (IApp (IConst (c, _), e1), e2)) = |
18850 | 312 |
if c = thingol_cons |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
313 |
then SOME (e1, e2) |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
314 |
else NONE |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
315 |
| dest_cons _ = NONE; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
316 |
fun pretty_default fxy pr e1 e2 = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
317 |
brackify_infix (target_pred, R) fxy [ |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
318 |
pr (INFX (target_pred, X)) e1, |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
319 |
str target_cons, |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
320 |
pr (INFX (target_pred, R)) e2 |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
321 |
]; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
322 |
fun pretty_compact fxy pr [e1, e2] = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
323 |
case unfoldr dest_cons e2 |
18850 | 324 |
of (es, IConst (c, _)) => |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
325 |
if c = thingol_nil |
18812 | 326 |
then Pretty.enum "," "[" "]" (map (pr NOBR) (e1::es)) |
18853 | 327 |
else pretty_default fxy pr e1 e2 |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
328 |
| _ => pretty_default fxy pr e1 e2; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
329 |
in ((2, 2), pretty_compact) end; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
330 |
|
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
331 |
|
18216 | 332 |
|
333 |
(** ML serializer **) |
|
334 |
||
335 |
local |
|
336 |
||
18702 | 337 |
fun ml_from_defs (is_cons, needs_type) |
338 |
(from_prim, (tyco_syntax, const_syntax)) resolv defs = |
|
18216 | 339 |
let |
18282 | 340 |
fun chunk_defs ps = |
18216 | 341 |
let |
342 |
val (p_init, p_last) = split_last ps |
|
343 |
in |
|
18702 | 344 |
Pretty.chunks (p_init @ [Pretty.block ([p_last, str ";"])]) |
18216 | 345 |
end; |
18515 | 346 |
fun ml_from_label s = |
347 |
let |
|
348 |
val s' = NameSpace.unpack s; |
|
349 |
in |
|
350 |
NameSpace.pack (Library.drop (length s' - 2, s')) |
|
351 |
|> translate_string (fn "_" => "__" | "." => "_" | c => c) |
|
352 |
end; |
|
18702 | 353 |
fun ml_from_type fxy (IType (tyco, tys)) = |
354 |
(case tyco_syntax tyco |
|
355 |
of NONE => |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
356 |
let |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
357 |
val f' = (str o resolv) tyco |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
358 |
in case map (ml_from_type BR) tys |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
359 |
of [] => f' |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
360 |
| [p] => Pretty.block [p, Pretty.brk 1, f'] |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
361 |
| (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, f'] |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
362 |
end |
18702 | 363 |
| SOME ((i, k), pr) => |
364 |
if not (i <= length tys andalso length tys <= k) |
|
365 |
then error ("number of argument mismatch in customary serialization: " |
|
366 |
^ (string_of_int o length) tys ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k |
|
367 |
^ " expected") |
|
368 |
else pr fxy ml_from_type tys) |
|
369 |
| ml_from_type fxy (IFun (t1, t2)) = |
|
18216 | 370 |
let |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
371 |
val brackify = gen_brackify |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
372 |
(case fxy |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
373 |
of BR => false |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
374 |
| _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks; |
18216 | 375 |
in |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
376 |
brackify [ |
18702 | 377 |
ml_from_type (INFX (1, X)) t1, |
378 |
str "->", |
|
379 |
ml_from_type (INFX (1, R)) t2 |
|
380 |
] |
|
18216 | 381 |
end |
18282 | 382 |
| ml_from_type _ (IVarT (v, [])) = |
18702 | 383 |
str ("'" ^ v) |
18282 | 384 |
| ml_from_type _ (IVarT (_, sort)) = |
18216 | 385 |
"cannot serialize sort constrained type variable to ML: " ^ commas sort |> error |
18282 | 386 |
| ml_from_type _ (IDictT fs) = |
18812 | 387 |
Pretty.enum "," "{" "}" ( |
18216 | 388 |
map (fn (f, ty) => |
18702 | 389 |
Pretty.block [str (ml_from_label f ^ ": "), ml_from_type NOBR ty]) fs |
18216 | 390 |
); |
18702 | 391 |
fun ml_from_pat fxy (ICons ((f, ps), ty)) = |
392 |
(case const_syntax f |
|
393 |
of NONE => if length ps <= 1 |
|
394 |
then |
|
395 |
ps |
|
396 |
|> map (ml_from_pat BR) |
|
397 |
|> cons ((str o resolv) f) |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
398 |
|> brackify fxy |
18702 | 399 |
else |
18216 | 400 |
ps |
18702 | 401 |
|> map (ml_from_pat BR) |
18812 | 402 |
|> Pretty.enum "," "(" ")" |
18702 | 403 |
|> single |
404 |
|> cons ((str o resolv) f) |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
405 |
|> brackify fxy |
18702 | 406 |
| SOME ((i, k), pr) => |
407 |
if not (i <= length ps andalso length ps <= k) |
|
408 |
then error ("number of argument mismatch in customary serialization: " |
|
409 |
^ (string_of_int o length) ps ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k |
|
410 |
^ " expected") |
|
411 |
else pr fxy ml_from_expr (map iexpr_of_ipat ps)) |
|
412 |
| ml_from_pat fxy (IVarP (v, ty)) = |
|
413 |
if needs_type ty |
|
18515 | 414 |
then |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
415 |
brackify fxy [ |
18702 | 416 |
str v, |
417 |
str ":", |
|
18515 | 418 |
ml_from_type NOBR ty |
419 |
] |
|
420 |
else |
|
18702 | 421 |
str v |
422 |
and ml_from_expr fxy (e as IApp (e1, e2)) = |
|
18216 | 423 |
(case (unfold_app e) |
424 |
of (e as (IConst (f, _)), es) => |
|
18702 | 425 |
ml_from_app fxy (f, es) |
18282 | 426 |
| _ => |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
427 |
brackify fxy [ |
18282 | 428 |
ml_from_expr NOBR e1, |
429 |
ml_from_expr BR e2 |
|
18216 | 430 |
]) |
18702 | 431 |
| ml_from_expr fxy (e as IConst (f, _)) = |
432 |
ml_from_app fxy (f, []) |
|
433 |
| ml_from_expr fxy (IVarE (v, _)) = |
|
434 |
str v |
|
435 |
| ml_from_expr fxy (IAbs ((v, _), e)) = |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
436 |
brackify fxy [ |
18702 | 437 |
str ("fn " ^ v ^ " =>"), |
18282 | 438 |
ml_from_expr NOBR e |
18216 | 439 |
] |
18702 | 440 |
| ml_from_expr fxy (e as ICase (_, [_])) = |
18216 | 441 |
let |
442 |
val (ps, e) = unfold_let e; |
|
443 |
fun mk_val (p, e) = Pretty.block [ |
|
18702 | 444 |
str "val ", |
445 |
ml_from_pat fxy p, |
|
446 |
str " =", |
|
18216 | 447 |
Pretty.brk 1, |
18282 | 448 |
ml_from_expr NOBR e, |
18702 | 449 |
str ";" |
18216 | 450 |
] |
451 |
in Pretty.chunks [ |
|
18702 | 452 |
[str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block, |
453 |
[str ("in"), Pretty.fbrk, ml_from_expr NOBR e] |> Pretty.block, |
|
454 |
str ("end") |
|
18216 | 455 |
] end |
18702 | 456 |
| ml_from_expr fxy (ICase (e, c::cs)) = |
18216 | 457 |
let |
458 |
fun mk_clause definer (p, e) = |
|
459 |
Pretty.block [ |
|
18702 | 460 |
str definer, |
18216 | 461 |
ml_from_pat NOBR p, |
18702 | 462 |
str " =>", |
18216 | 463 |
Pretty.brk 1, |
18282 | 464 |
ml_from_expr NOBR e |
18216 | 465 |
] |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
466 |
in brackify fxy ( |
18702 | 467 |
str "case" |
18282 | 468 |
:: ml_from_expr NOBR e |
18216 | 469 |
:: mk_clause "of " c |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
470 |
:: map (mk_clause "| ") cs |
18216 | 471 |
) end |
18702 | 472 |
| ml_from_expr fxy (IInst _) = |
18216 | 473 |
error "cannot serialize poly instant to ML" |
18702 | 474 |
| ml_from_expr fxy (IDictE fs) = |
18812 | 475 |
Pretty.enum "," "{" "}" ( |
18216 | 476 |
map (fn (f, e) => |
18702 | 477 |
Pretty.block [str (ml_from_label f ^ " = "), ml_from_expr NOBR e]) fs |
18216 | 478 |
) |
18702 | 479 |
| ml_from_expr fxy (ILookup ([], v)) = |
480 |
str v |
|
481 |
| ml_from_expr fxy (ILookup ([l], v)) = |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
482 |
brackify fxy [ |
18702 | 483 |
str ("#" ^ (ml_from_label l)), |
484 |
str v |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
485 |
] |
18702 | 486 |
| ml_from_expr fxy (ILookup (ls, v)) = |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
487 |
brackify fxy [ |
18702 | 488 |
str ("(" |
18515 | 489 |
^ (ls |> map ((fn s => "#" ^ s) o ml_from_label) |> foldr1 (fn (l, e) => l ^ " o " ^ e)) |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
490 |
^ ")"), |
18702 | 491 |
str v |
18216 | 492 |
] |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
493 |
| ml_from_expr _ e = |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
494 |
error ("dubious expression: " ^ (Pretty.output o pretty_iexpr) e) |
18702 | 495 |
and ml_mk_app f es = |
496 |
if is_cons f andalso length es > 1 |
|
497 |
then |
|
18812 | 498 |
[(str o resolv) f, Pretty.enum " *" "(" ")" (map (ml_from_expr BR) es)] |
18702 | 499 |
else |
500 |
(str o resolv) f :: map (ml_from_expr BR) es |
|
501 |
and ml_from_app fxy = |
|
502 |
from_app ml_mk_app ml_from_expr const_syntax fxy; |
|
18216 | 503 |
fun ml_from_funs (ds as d::ds_tl) = |
504 |
let |
|
505 |
fun mk_definer [] = "val" |
|
18702 | 506 |
| mk_definer _ = "fun"; |
18216 | 507 |
fun check_args (_, Fun ((pats, _)::_, _)) NONE = |
508 |
SOME (mk_definer pats) |
|
509 |
| check_args (_, Fun ((pats, _)::_, _)) (SOME definer) = |
|
510 |
if mk_definer pats = definer |
|
511 |
then SOME definer |
|
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
512 |
else error ("mixing simultaneous vals and funs not implemented") |
18216 | 513 |
| check_args _ _ = |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
514 |
error ("function definition block containing other definitions than functions") |
18216 | 515 |
val definer = the (fold check_args ds NONE); |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
516 |
fun mk_eq definer f ty (pats, expr) = |
18216 | 517 |
let |
18702 | 518 |
val lhs = [str (definer ^ " " ^ f)] |
18216 | 519 |
@ (if null pats |
18702 | 520 |
then [str ":", ml_from_type NOBR ty] |
18515 | 521 |
else map (ml_from_pat BR) pats) |
18702 | 522 |
val rhs = [str "=", ml_from_expr NOBR expr] |
18216 | 523 |
in |
524 |
Pretty.block (separate (Pretty.brk 1) (lhs @ rhs)) |
|
525 |
end |
|
526 |
fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (_, ty))) = |
|
527 |
let |
|
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
528 |
val (pats_hd::pats_tl) = (fst o split_list) eqs; |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
529 |
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
|
530 |
in (Pretty.block o Pretty.fbreaks o shift) ( |
18216 | 531 |
mk_eq definer f ty eq |
532 |
:: map (mk_eq "|" f ty) eq_tl |
|
533 |
) |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
534 |
end; |
18216 | 535 |
in |
536 |
chunk_defs ( |
|
537 |
mk_fun definer d |
|
538 |
:: map (mk_fun "and") ds_tl |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
539 |
) |> SOME |
18216 | 540 |
end; |
18282 | 541 |
fun ml_from_datatypes defs = |
18216 | 542 |
let |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
543 |
val defs' = List.mapPartial |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
544 |
(fn (name, Datatype info) => SOME (name, info) |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
545 |
| (name, Datatypecons _) => NONE |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
546 |
| (name, def) => error ("datatype block containing illegal def: " ^ (Pretty.output o pretty_def) def) |
18702 | 547 |
) defs |
548 |
fun mk_cons (co, []) = |
|
549 |
str (resolv co) |
|
550 |
| mk_cons (co, tys) = |
|
551 |
Pretty.block ( |
|
552 |
str (resolv co) |
|
553 |
:: str " of" |
|
554 |
:: Pretty.brk 1 |
|
555 |
:: separate (Pretty.block [str " *", Pretty.brk 1]) (map (ml_from_type NOBR) tys) |
|
556 |
) |
|
557 |
fun mk_datatype definer (t, ((vs, cs), _)) = |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
558 |
Pretty.block ( |
18702 | 559 |
str definer |
560 |
:: ml_from_type NOBR (t `%% map IVarT vs) |
|
561 |
:: str " =" |
|
562 |
:: Pretty.brk 1 |
|
563 |
:: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons cs) |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
564 |
) |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
565 |
in |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
566 |
case defs' |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
567 |
of d::ds_tl => |
18216 | 568 |
chunk_defs ( |
569 |
mk_datatype "datatype " d |
|
570 |
:: map (mk_datatype "and ") ds_tl |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
571 |
) |> SOME |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
572 |
| _ => NONE |
18702 | 573 |
end |
574 |
fun ml_from_def (name, Undef) = |
|
575 |
error ("empty definition during serialization: " ^ quote name) |
|
18516 | 576 |
| ml_from_def (name, Prim prim) = |
18702 | 577 |
from_prim (name, prim) |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
578 |
| ml_from_def (name, Typesyn (vs, ty)) = |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
579 |
(map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs; |
18702 | 580 |
Pretty.block [ |
581 |
str "type ", |
|
582 |
ml_from_type NOBR (name `%% map IVarT vs), |
|
583 |
str " =", |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
584 |
Pretty.brk 1, |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
585 |
ml_from_type NOBR ty, |
18702 | 586 |
str ";" |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
587 |
] |
18702 | 588 |
) |> SOME |
18216 | 589 |
| ml_from_def (name, Class _) = |
590 |
error ("can't serialize class declaration " ^ quote name ^ " to ML") |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
591 |
| ml_from_def (_, Classmember _) = |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
592 |
NONE |
18216 | 593 |
| ml_from_def (name, Classinst _) = |
594 |
error ("can't serialize instance declaration " ^ quote name ^ " to ML") |
|
18850 | 595 |
in case defs |
18702 | 596 |
of (_, Fun _)::_ => ml_from_funs defs |
597 |
| (_, Datatypecons _)::_ => ml_from_datatypes defs |
|
598 |
| (_, Datatype _)::_ => ml_from_datatypes defs |
|
18850 | 599 |
| [def] => ml_from_def def |
18216 | 600 |
end; |
601 |
||
602 |
in |
|
603 |
||
18756 | 604 |
fun ml_from_thingol target (nsp_dtcon, nsp_class, int_tyco) nspgrp = |
18216 | 605 |
let |
18702 | 606 |
val reserved_ml = ThmDatabase.ml_reserved @ [ |
607 |
"bool", "int", "list", "true", "false" |
|
608 |
]; |
|
18850 | 609 |
fun ml_from_module _ ((_, name), ps) = |
18756 | 610 |
Pretty.chunks ([ |
18702 | 611 |
str ("structure " ^ name ^ " = "), |
612 |
str "struct", |
|
613 |
str "" |
|
614 |
] @ separate (str "") ps @ [ |
|
615 |
str "", |
|
616 |
str ("end; (* struct " ^ name ^ " *)") |
|
18756 | 617 |
]); |
18702 | 618 |
fun needs_type (IType (tyco, _)) = |
18516 | 619 |
has_nsp tyco nsp_class |
18702 | 620 |
orelse tyco = int_tyco |
621 |
| needs_type (IDictT _) = |
|
18516 | 622 |
true |
18702 | 623 |
| needs_type _ = |
18516 | 624 |
false; |
18702 | 625 |
fun is_cons c = has_nsp c nsp_dtcon; |
18756 | 626 |
val serializer = abstract_serializer (target, nspgrp) |
18850 | 627 |
"ROOT" (ml_from_defs (is_cons, needs_type), ml_from_module, abstract_validator reserved_ml); |
18756 | 628 |
fun eta_expander module const_syntax s = |
18702 | 629 |
case const_syntax s |
630 |
of SOME ((i, _), _) => i |
|
631 |
| _ => if has_nsp s nsp_dtcon |
|
632 |
then case get_def module s |
|
633 |
of Datatypecons dtname => case get_def module dtname |
|
634 |
of Datatype ((_, cs), _) => |
|
635 |
let val l = AList.lookup (op =) cs s |> the |> length |
|
636 |
in if l >= 2 then l else 0 end |
|
637 |
else 0; |
|
18756 | 638 |
fun preprocess const_syntax module = |
18702 | 639 |
module |
640 |
|> tap (Pretty.writeln o pretty_deps) |
|
641 |
|> debug 3 (fn _ => "eta-expanding...") |
|
18756 | 642 |
|> eta_expand (eta_expander module const_syntax) |
18702 | 643 |
|> debug 3 (fn _ => "eta-expanding polydefs...") |
644 |
|> eta_expand_poly |
|
645 |
|> debug 3 (fn _ => "eliminating classes...") |
|
18756 | 646 |
|> eliminate_classes; |
18850 | 647 |
val parse_multi = |
648 |
OuterParse.name |
|
649 |
#-> (fn "dir" => |
|
650 |
parse_multi_file |
|
651 |
(K o SOME o str o suffix ";" o prefix "val _ = use " |
|
652 |
o quote o suffix ".ML" o translate_string (fn "." => "/" | s => s)) "ML" serializer |
|
653 |
| _ => Scan.fail ()); |
|
18282 | 654 |
in |
18850 | 655 |
(parse_multi |
656 |
|| parse_internal serializer |
|
657 |
|| parse_single_file serializer) |
|
18756 | 658 |
>> (fn seri => fn (tyco_syntax, const_syntax) => seri |
659 |
(preprocess const_syntax) (tyco_syntax, const_syntax)) |
|
18216 | 660 |
end; |
661 |
||
662 |
end; (* local *) |
|
663 |
||
18282 | 664 |
local |
665 |
||
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
666 |
fun hs_from_defs is_cons (from_prim, (tyco_syntax, const_syntax)) resolv defs = |
18282 | 667 |
let |
18702 | 668 |
fun upper_first s = |
669 |
let |
|
670 |
val (pr, b) = split_last (NameSpace.unpack s); |
|
671 |
val (c::cs) = String.explode b; |
|
672 |
in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end; |
|
673 |
fun lower_first s = |
|
674 |
let |
|
675 |
val (pr, b) = split_last (NameSpace.unpack s); |
|
676 |
val (c::cs) = String.explode b; |
|
677 |
in NameSpace.pack (pr @ [String.implode (Char.toLower c :: cs)]) end; |
|
18282 | 678 |
val resolv = fn s => |
679 |
let |
|
680 |
val (prfix, base) = (split_last o NameSpace.unpack o resolv) s |
|
681 |
in |
|
682 |
NameSpace.pack (map upper_first prfix @ [base]) |
|
683 |
end; |
|
684 |
fun resolv_const f = |
|
18335 | 685 |
if NameSpace.is_qualified f |
686 |
then |
|
687 |
if is_cons f |
|
688 |
then (upper_first o resolv) f |
|
689 |
else (lower_first o resolv) f |
|
690 |
else |
|
691 |
f; |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
692 |
fun hs_from_sctxt vs = |
18282 | 693 |
let |
18702 | 694 |
fun from_sctxt [] = str "" |
18282 | 695 |
| from_sctxt vs = |
696 |
vs |
|
18702 | 697 |
|> map (fn (v, cls) => str ((upper_first o resolv) cls ^ " " ^ lower_first v)) |
18812 | 698 |
|> Pretty.enum "," "(" ")" |
18702 | 699 |
|> (fn p => Pretty.block [p, str " => "]) |
18282 | 700 |
in |
701 |
vs |
|
702 |
|> map (fn (v, sort) => map (pair v) sort) |
|
703 |
|> Library.flat |
|
704 |
|> from_sctxt |
|
705 |
end; |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
706 |
fun hs_from_type fxy ty = |
18282 | 707 |
let |
18702 | 708 |
fun from_itype fxy (IType (tyco, tys)) sctxt = |
709 |
(case tyco_syntax tyco |
|
710 |
of NONE => |
|
711 |
sctxt |
|
712 |
|> fold_map (from_itype BR) tys |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
713 |
|-> (fn tyargs => pair (brackify fxy ((str o upper_first o resolv) tyco :: tyargs))) |
18702 | 714 |
| SOME ((i, k), pr) => |
715 |
if not (i <= length tys andalso length tys <= k) |
|
716 |
then error ("number of argument mismatch in customary serialization: " |
|
717 |
^ (string_of_int o length) tys ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k |
|
718 |
^ " expected") |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
719 |
else (pr fxy hs_from_type tys, sctxt)) |
18702 | 720 |
| from_itype fxy (IFun (t1, t2)) sctxt = |
18282 | 721 |
sctxt |
722 |
|> from_itype (INFX (1, X)) t1 |
|
723 |
||>> from_itype (INFX (1, R)) t2 |
|
724 |
|-> (fn (p1, p2) => pair ( |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
725 |
brackify_infix (1, R) fxy [ |
18282 | 726 |
p1, |
18702 | 727 |
str "->", |
18282 | 728 |
p2 |
729 |
] |
|
730 |
)) |
|
18702 | 731 |
| from_itype fxy (IVarT (v, [])) sctxt = |
18282 | 732 |
sctxt |
18702 | 733 |
|> pair ((str o lower_first) v) |
734 |
| from_itype fxy (IVarT (v, sort)) sctxt = |
|
18282 | 735 |
sctxt |
736 |
|> AList.default (op =) (v, []) |
|
737 |
|> AList.map_entry (op =) v (fold (insert (op =)) sort) |
|
18702 | 738 |
|> pair ((str o lower_first) v) |
739 |
| from_itype fxy (IDictT _) _ = |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
740 |
error "cannot serialize dictionary type to hs" |
18282 | 741 |
in |
742 |
[] |
|
18702 | 743 |
|> from_itype fxy ty |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
744 |
||> hs_from_sctxt |
18282 | 745 |
|> (fn (pty, pctxt) => Pretty.block [pctxt, pty]) |
746 |
end; |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
747 |
fun hs_from_pat fxy (ICons ((f, ps), _)) = |
18335 | 748 |
(case const_syntax f |
749 |
of NONE => |
|
18702 | 750 |
ps |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
751 |
|> map (hs_from_pat BR) |
18702 | 752 |
|> cons ((str o resolv_const) f) |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
753 |
|> brackify fxy |
18702 | 754 |
| SOME ((i, k), pr) => |
755 |
if not (i <= length ps andalso length ps <= k) |
|
756 |
then error ("number of argument mismatch in customary serialization: " |
|
757 |
^ (string_of_int o length) ps ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k |
|
758 |
^ " expected") |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
759 |
else pr fxy hs_from_expr (map iexpr_of_ipat ps)) |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
760 |
| hs_from_pat fxy (IVarP (v, _)) = |
18702 | 761 |
(str o lower_first) v |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
762 |
and hs_from_expr fxy (e as IApp (e1, e2)) = |
18282 | 763 |
(case (unfold_app e) |
764 |
of (e as (IConst (f, _)), es) => |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
765 |
hs_from_app fxy (f, es) |
18282 | 766 |
| _ => |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
767 |
brackify fxy [ |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
768 |
hs_from_expr NOBR e1, |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
769 |
hs_from_expr BR e2 |
18282 | 770 |
]) |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
771 |
| hs_from_expr fxy (e as IConst (f, _)) = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
772 |
hs_from_app fxy (f, []) |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
773 |
| hs_from_expr fxy (IVarE (v, _)) = |
18702 | 774 |
(str o lower_first) v |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
775 |
| hs_from_expr fxy (e as IAbs _) = |
18282 | 776 |
let |
777 |
val (vs, body) = unfold_abs e |
|
778 |
in |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
779 |
brackify fxy ( |
18702 | 780 |
str "\\" |
781 |
:: map (str o lower_first o fst) vs @ [ |
|
782 |
str "->", |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
783 |
hs_from_expr NOBR body |
18282 | 784 |
]) |
785 |
end |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
786 |
| hs_from_expr fxy (e as ICase (_, [_])) = |
18282 | 787 |
let |
788 |
val (ps, body) = unfold_let e; |
|
789 |
fun mk_bind (p, e) = Pretty.block [ |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
790 |
hs_from_pat BR p, |
18702 | 791 |
str " =", |
18282 | 792 |
Pretty.brk 1, |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
793 |
hs_from_expr NOBR e |
18282 | 794 |
]; |
795 |
in Pretty.chunks [ |
|
18702 | 796 |
[str ("let"), Pretty.fbrk, map mk_bind ps |> Pretty.chunks] |> Pretty.block, |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
797 |
[str ("in "), hs_from_expr NOBR body] |> Pretty.block |
18282 | 798 |
] end |
18850 | 799 |
| hs_from_expr fxy (ICase (e, cs)) = |
18282 | 800 |
let |
18850 | 801 |
fun mk_clause (p, e) = |
18282 | 802 |
Pretty.block [ |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
803 |
hs_from_pat NOBR p, |
18702 | 804 |
str " ->", |
18282 | 805 |
Pretty.brk 1, |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
806 |
hs_from_expr NOBR e |
18282 | 807 |
] |
18850 | 808 |
in Pretty.block [ |
809 |
str "case", |
|
810 |
Pretty.brk 1, |
|
811 |
hs_from_expr NOBR e, |
|
812 |
Pretty.brk 1, |
|
813 |
str "of", |
|
814 |
Pretty.fbrk, |
|
815 |
(Pretty.chunks o map mk_clause) cs |
|
816 |
] end |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
817 |
| hs_from_expr fxy (IInst (e, _)) = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
818 |
hs_from_expr fxy e |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
819 |
| hs_from_expr fxy (IDictE _) = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
820 |
error "cannot serialize dictionary expression to hs" |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
821 |
| hs_from_expr fxy (ILookup _) = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
822 |
error "cannot serialize lookup expression to hs" |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
823 |
and hs_mk_app f es = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
824 |
(str o resolv_const) f :: map (hs_from_expr BR) es |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
825 |
and hs_from_app fxy = |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
826 |
from_app hs_mk_app hs_from_expr const_syntax fxy; |
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
827 |
fun hs_from_def (name, Undef) = |
18702 | 828 |
error ("empty statement during serialization: " ^ quote name) |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
829 |
| hs_from_def (name, Prim prim) = |
18702 | 830 |
from_prim (name, prim) |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
831 |
| hs_from_def (name, Fun (eqs, (_, ty))) = |
18282 | 832 |
let |
833 |
fun from_eq name (args, rhs) = |
|
834 |
Pretty.block [ |
|
18702 | 835 |
str (lower_first name), |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
836 |
Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, hs_from_pat BR p]) args), |
18282 | 837 |
Pretty.brk 1, |
18702 | 838 |
str ("="), |
18282 | 839 |
Pretty.brk 1, |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
840 |
hs_from_expr NOBR rhs |
18454 | 841 |
] |
18282 | 842 |
in |
843 |
Pretty.chunks [ |
|
844 |
Pretty.block [ |
|
18702 | 845 |
str (lower_first name ^ " ::"), |
18282 | 846 |
Pretty.brk 1, |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
847 |
hs_from_type NOBR ty |
18282 | 848 |
], |
849 |
Pretty.chunks (map (from_eq name) eqs) |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
850 |
] |> SOME |
18282 | 851 |
end |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
852 |
| hs_from_def (name, Typesyn (vs, ty)) = |
18282 | 853 |
Pretty.block [ |
18702 | 854 |
str "type ", |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
855 |
hs_from_sctxt vs, |
18702 | 856 |
str (upper_first name), |
857 |
Pretty.block (map (fn (v, _) => str (" " ^ (lower_first) v)) vs), |
|
858 |
str " =", |
|
18282 | 859 |
Pretty.brk 1, |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
860 |
hs_from_type NOBR ty |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
861 |
] |> SOME |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
862 |
| hs_from_def (name, Datatype ((vars, constrs), _)) = |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
863 |
let |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
864 |
fun mk_cons (co, tys) = |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
865 |
(Pretty.block o Pretty.breaks) ( |
18702 | 866 |
str ((upper_first o resolv) co) |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
867 |
:: map (hs_from_type NOBR) tys |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
868 |
) |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
869 |
in |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
870 |
Pretty.block ( |
18702 | 871 |
str "data " |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
872 |
:: hs_from_sctxt vars |
18702 | 873 |
:: str (upper_first name) |
874 |
:: Pretty.block (map (fn (v, _) => str (" " ^ (lower_first) v)) vars) |
|
875 |
:: str " =" |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
876 |
:: Pretty.brk 1 |
18702 | 877 |
:: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs) |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
878 |
) |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
879 |
end |> SOME |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
880 |
| hs_from_def (_, Datatypecons _) = |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
881 |
NONE |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
882 |
| hs_from_def (name, Class ((supclasss, (v, membrs)), _)) = |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
883 |
let |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
884 |
fun mk_member (m, (_, ty)) = |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
885 |
Pretty.block [ |
18702 | 886 |
str (resolv m ^ " ::"), |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
887 |
Pretty.brk 1, |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
888 |
hs_from_type NOBR ty |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
889 |
] |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
890 |
in |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
891 |
Pretty.block [ |
18702 | 892 |
str "class ", |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
893 |
hs_from_sctxt (map (fn class => (v, [class])) supclasss), |
18702 | 894 |
str ((upper_first name) ^ " " ^ v), |
895 |
str " where", |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
896 |
Pretty.fbrk, |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
897 |
Pretty.chunks (map mk_member membrs) |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
898 |
] |> SOME |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
899 |
end |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
900 |
| hs_from_def (name, Classmember _) = |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
901 |
NONE |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
902 |
| hs_from_def (_, Classinst ((clsname, (tyco, arity)), memdefs)) = |
18385 | 903 |
Pretty.block [ |
18702 | 904 |
str "instance ", |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
905 |
hs_from_sctxt arity, |
18702 | 906 |
str ((upper_first o resolv) clsname), |
907 |
str " ", |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
908 |
hs_from_type NOBR (IType (tyco, (map (IVarT o rpair [] o fst)) arity)), |
18702 | 909 |
str " where", |
18385 | 910 |
Pretty.fbrk, |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
911 |
Pretty.chunks (map (fn (m, funn) => hs_from_def (m, Fun funn) |> the) memdefs) |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
912 |
] |> SOME |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
913 |
in |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
914 |
case List.mapPartial (fn (name, def) => hs_from_def (name, def)) defs |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
915 |
of [] => NONE |
18702 | 916 |
| l => (SOME o Pretty.chunks o separate (str "")) l |
18282 | 917 |
end; |
918 |
||
919 |
in |
|
920 |
||
18756 | 921 |
fun hs_from_thingol target nsp_dtcon nspgrp = |
18282 | 922 |
let |
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
923 |
val reserved_hs = [ |
18702 | 924 |
"hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr", |
925 |
"import", "default", "forall", "let", "in", "class", "qualified", "data", |
|
926 |
"newtype", "instance", "if", "then", "else", "type", "as", "do", "module" |
|
927 |
] @ [ |
|
928 |
"Bool", "fst", "snd", "Integer", "True", "False", "negate" |
|
929 |
]; |
|
930 |
fun upper_first s = |
|
931 |
let |
|
932 |
val (pr, b) = split_last (NameSpace.unpack s); |
|
933 |
val (c::cs) = String.explode b; |
|
934 |
in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end; |
|
18850 | 935 |
fun hs_from_module imps ((_, name), ps) = |
936 |
(Pretty.block o Pretty.fbreaks) ( |
|
937 |
str ("module " ^ (upper_first name) ^ " where") |
|
938 |
:: map (str o prefix "import ") imps @ [ |
|
939 |
str "", |
|
18702 | 940 |
Pretty.chunks (separate (str "") ps) |
18850 | 941 |
]); |
18702 | 942 |
fun is_cons c = has_nsp c nsp_dtcon; |
18756 | 943 |
val serializer = abstract_serializer (target, nspgrp) |
18850 | 944 |
"Main" (hs_from_defs is_cons, hs_from_module, abstract_validator reserved_hs); |
18756 | 945 |
fun eta_expander const_syntax c = |
18702 | 946 |
const_syntax c |
947 |
|> Option.map (fst o fst) |
|
948 |
|> the_default 0; |
|
18756 | 949 |
fun preprocess const_syntax module = |
18702 | 950 |
module |
951 |
|> tap (Pretty.writeln o pretty_deps) |
|
952 |
|> debug 3 (fn _ => "eta-expanding...") |
|
18756 | 953 |
|> eta_expand (eta_expander const_syntax); |
18282 | 954 |
in |
18850 | 955 |
parse_multi_file ((K o K) NONE) "hs" serializer |
18756 | 956 |
>> (fn seri => fn (tyco_syntax, const_syntax) => seri |
957 |
(preprocess const_syntax) (tyco_syntax, const_syntax)) |
|
18282 | 958 |
end; |
959 |
||
960 |
end; (* local *) |
|
961 |
||
18702 | 962 |
|
963 |
(** lookup record **) |
|
964 |
||
965 |
val serializers = |
|
966 |
let |
|
967 |
fun seri s f = (s, f s); |
|
968 |
in { |
|
969 |
ml = seri "ml" ml_from_thingol, |
|
18704
2c86ced392a8
substantial improvement in serialization handling
haftmann
parents:
18702
diff
changeset
|
970 |
haskell = seri "haskell" hs_from_thingol |
18702 | 971 |
} end; |
972 |
||
18216 | 973 |
end; (* struct *) |