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