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