1 (* Title: Pure/Tools/codegen_thingol.ML |
|
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
|
4 |
|
5 Intermediate language ("Thin-gol") representing executable code. |
|
6 *) |
|
7 |
|
8 infix 8 `%%; |
|
9 infixr 6 `->; |
|
10 infixr 6 `-->; |
|
11 infix 4 `$; |
|
12 infix 4 `$$; |
|
13 infixr 3 `|->; |
|
14 infixr 3 `|-->; |
|
15 |
|
16 signature BASIC_CODEGEN_THINGOL = |
|
17 sig |
|
18 type vname = string; |
|
19 datatype dict = |
|
20 DictConst of string * dict list list |
|
21 | DictVar of string list * (vname * (int * int)); |
|
22 datatype itype = |
|
23 `%% of string * itype list |
|
24 | ITyVar of vname; |
|
25 datatype iterm = |
|
26 IConst of string * (dict list list * itype list (*types of arguments*)) |
|
27 | IVar of vname |
|
28 | `$ of iterm * iterm |
|
29 | `|-> of (vname * itype) * iterm |
|
30 | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; |
|
31 (*((term, type), [(selector pattern, body term )]), primitive term)*) |
|
32 val `-> : itype * itype -> itype; |
|
33 val `--> : itype list * itype -> itype; |
|
34 val `$$ : iterm * iterm list -> iterm; |
|
35 val `|--> : (vname * itype) list * iterm -> iterm; |
|
36 type typscheme = (vname * sort) list * itype; |
|
37 end; |
|
38 |
|
39 signature CODEGEN_THINGOL = |
|
40 sig |
|
41 include BASIC_CODEGEN_THINGOL; |
|
42 val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list; |
|
43 val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a; |
|
44 val unfold_fun: itype -> itype list * itype; |
|
45 val unfold_app: iterm -> iterm * iterm list; |
|
46 val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option; |
|
47 val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm; |
|
48 val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option; |
|
49 val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm; |
|
50 val unfold_const_app: iterm -> |
|
51 ((string * (dict list list * itype list)) * iterm list) option; |
|
52 val collapse_let: ((vname * itype) * iterm) * iterm |
|
53 -> (iterm * itype) * (iterm * iterm) list; |
|
54 val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm; |
|
55 val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; |
|
56 val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; |
|
57 val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; |
|
58 |
|
59 datatype def = |
|
60 Bot |
|
61 | Fun of (iterm list * iterm) list * typscheme |
|
62 | Datatype of (vname * sort) list * (string * itype list) list |
|
63 | Datatypecons of string |
|
64 | Class of (class * string) list * (vname * (string * itype) list) |
|
65 | Classop of class |
|
66 | Classrel of class * class |
|
67 | Classinst of (class * (string * (vname * sort) list)) |
|
68 * ((class * (string * (string * dict list list))) list |
|
69 * (string * iterm) list); |
|
70 type code = def Graph.T; |
|
71 type transact; |
|
72 val empty_code: code; |
|
73 val merge_code: code * code -> code; |
|
74 val project_code: bool (*delete empty funs*) |
|
75 -> string list (*hidden*) -> string list option (*selected*) |
|
76 -> code -> code; |
|
77 val empty_funs: code -> string list; |
|
78 val is_cons: code -> string -> bool; |
|
79 val add_eval_def: string (*bind name*) * iterm -> code -> code; |
|
80 |
|
81 val ensure_def: (string -> string) -> (transact -> def * code) -> string |
|
82 -> string -> transact -> transact; |
|
83 val succeed: 'a -> transact -> 'a * code; |
|
84 val fail: string -> transact -> 'a * code; |
|
85 val message: string -> (transact -> 'a) -> transact -> 'a; |
|
86 val start_transact: (transact -> 'a * transact) -> code -> 'a * code; |
|
87 |
|
88 val trace: bool ref; |
|
89 val tracing: ('a -> string) -> 'a -> 'a; |
|
90 end; |
|
91 |
|
92 structure CodegenThingol: CODEGEN_THINGOL = |
|
93 struct |
|
94 |
|
95 (** auxiliary **) |
|
96 |
|
97 val trace = ref false; |
|
98 fun tracing f x = (if !trace then Output.tracing (f x) else (); x); |
|
99 |
|
100 fun unfoldl dest x = |
|
101 case dest x |
|
102 of NONE => (x, []) |
|
103 | SOME (x1, x2) => |
|
104 let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end; |
|
105 |
|
106 fun unfoldr dest x = |
|
107 case dest x |
|
108 of NONE => ([], x) |
|
109 | SOME (x1, x2) => |
|
110 let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end; |
|
111 |
|
112 |
|
113 (** language core - types, pattern, expressions **) |
|
114 |
|
115 (* language representation *) |
|
116 |
|
117 type vname = string; |
|
118 |
|
119 datatype dict = |
|
120 DictConst of string * dict list list |
|
121 | DictVar of string list * (vname * (int * int)); |
|
122 |
|
123 datatype itype = |
|
124 `%% of string * itype list |
|
125 | ITyVar of vname; |
|
126 |
|
127 datatype iterm = |
|
128 IConst of string * (dict list list * itype list) |
|
129 | IVar of vname |
|
130 | `$ of iterm * iterm |
|
131 | `|-> of (vname * itype) * iterm |
|
132 | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; |
|
133 (*see also signature*) |
|
134 |
|
135 (* |
|
136 variable naming conventions |
|
137 |
|
138 bare names: |
|
139 variable names v |
|
140 class names class |
|
141 type constructor names tyco |
|
142 datatype names dtco |
|
143 const names (general) c |
|
144 constructor names co |
|
145 class operation names clsop (op) |
|
146 arbitrary name s |
|
147 |
|
148 v, c, co, clsop also annotated with types etc. |
|
149 |
|
150 constructs: |
|
151 sort sort |
|
152 type parameters vs |
|
153 type ty |
|
154 type schemes tysm |
|
155 term t |
|
156 (term as pattern) p |
|
157 instance (class, tyco) inst |
|
158 *) |
|
159 |
|
160 fun ty1 `-> ty2 = "fun" `%% [ty1, ty2]; |
|
161 val op `--> = Library.foldr (op `->); |
|
162 val op `$$ = Library.foldl (op `$); |
|
163 val op `|--> = Library.foldr (op `|->); |
|
164 |
|
165 val unfold_fun = unfoldr |
|
166 (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2) |
|
167 | _ => NONE); |
|
168 |
|
169 val unfold_app = unfoldl |
|
170 (fn op `$ t => SOME t |
|
171 | _ => NONE); |
|
172 |
|
173 val split_abs = |
|
174 (fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) => |
|
175 if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t) |
|
176 | (v, ty) `|-> t => SOME (((v, NONE), ty), t) |
|
177 | _ => NONE); |
|
178 |
|
179 val unfold_abs = unfoldr split_abs; |
|
180 |
|
181 val split_let = |
|
182 (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t) |
|
183 | _ => NONE); |
|
184 |
|
185 val unfold_let = unfoldr split_let; |
|
186 |
|
187 fun unfold_const_app t = |
|
188 case unfold_app t |
|
189 of (IConst c, ts) => SOME (c, ts) |
|
190 | _ => NONE; |
|
191 |
|
192 fun fold_aiterms f (t as IConst _) = f t |
|
193 | fold_aiterms f (t as IVar _) = f t |
|
194 | fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2 |
|
195 | fold_aiterms f (t as _ `|-> t') = f t #> fold_aiterms f t' |
|
196 | fold_aiterms f (ICase (_, t)) = fold_aiterms f t; |
|
197 |
|
198 fun fold_constnames f = |
|
199 let |
|
200 fun add (IConst (c, _)) = f c |
|
201 | add _ = I; |
|
202 in fold_aiterms add end; |
|
203 |
|
204 fun fold_varnames f = |
|
205 let |
|
206 fun add (IVar v) = f v |
|
207 | add ((v, _) `|-> _) = f v |
|
208 | add _ = I; |
|
209 in fold_aiterms add end; |
|
210 |
|
211 fun fold_unbound_varnames f = |
|
212 let |
|
213 fun add _ (IConst _) = I |
|
214 | add vs (IVar v) = if not (member (op =) vs v) then f v else I |
|
215 | add vs (t1 `$ t2) = add vs t1 #> add vs t2 |
|
216 | add vs ((v, _) `|-> t) = add (insert (op =) v vs) t |
|
217 | add vs (ICase (_, t)) = add vs t; |
|
218 in add [] end; |
|
219 |
|
220 fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) = |
|
221 let |
|
222 fun exists_v t = fold_unbound_varnames (fn w => fn b => |
|
223 b orelse v = w) t false; |
|
224 in if v = w andalso forall (fn (t1, t2) => |
|
225 exists_v t1 orelse not (exists_v t2)) ds |
|
226 then ((se, ty), ds) |
|
227 else ((se, ty), [(IVar v, be)]) |
|
228 end |
|
229 | collapse_let (((v, ty), se), be) = |
|
230 ((se, ty), [(IVar v, be)]) |
|
231 |
|
232 fun eta_expand (c as (_, (_, tys)), ts) k = |
|
233 let |
|
234 val j = length ts; |
|
235 val l = k - j; |
|
236 val ctxt = (fold o fold_varnames) Name.declare ts Name.context; |
|
237 val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys); |
|
238 in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end; |
|
239 |
|
240 |
|
241 (** definitions, transactions **) |
|
242 |
|
243 (* type definitions *) |
|
244 |
|
245 type typscheme = (vname * sort) list * itype; |
|
246 datatype def = |
|
247 Bot |
|
248 | Fun of (iterm list * iterm) list * typscheme |
|
249 | Datatype of (vname * sort) list * (string * itype list) list |
|
250 | Datatypecons of string |
|
251 | Class of (class * string) list * (vname * (string * itype) list) |
|
252 | Classop of class |
|
253 | Classrel of class * class |
|
254 | Classinst of (class * (string * (vname * sort) list)) |
|
255 * ((class * (string * (string * dict list list))) list |
|
256 * (string * iterm) list); |
|
257 |
|
258 type code = def Graph.T; |
|
259 type transact = Graph.key option * code; |
|
260 exception FAIL of string list; |
|
261 |
|
262 |
|
263 (* abstract code *) |
|
264 |
|
265 val empty_code = Graph.empty : code; (*read: "depends on"*) |
|
266 |
|
267 fun ensure_bot name = Graph.default_node (name, Bot); |
|
268 |
|
269 fun add_def_incr (name, Bot) code = |
|
270 (case the_default Bot (try (Graph.get_node code) name) |
|
271 of Bot => error "Attempted to add Bot to code" |
|
272 | _ => code) |
|
273 | add_def_incr (name, def) code = |
|
274 (case try (Graph.get_node code) name |
|
275 of NONE => Graph.new_node (name, def) code |
|
276 | SOME Bot => Graph.map_node name (K def) code |
|
277 | SOME _ => error ("Tried to overwrite definition " ^ quote name)); |
|
278 |
|
279 fun add_dep (dep as (name1, name2)) = |
|
280 if name1 = name2 then I else Graph.add_edge dep; |
|
281 |
|
282 val merge_code : code * code -> code = Graph.merge (K true); |
|
283 |
|
284 fun project_code delete_empty_funs hidden raw_selected code = |
|
285 let |
|
286 fun is_empty_fun name = case Graph.get_node code name |
|
287 of Fun ([], _) => true |
|
288 | _ => false; |
|
289 val names = subtract (op =) hidden (Graph.keys code); |
|
290 val deleted = Graph.all_preds code (filter is_empty_fun names); |
|
291 val selected = case raw_selected |
|
292 of NONE => names |> subtract (op =) deleted |
|
293 | SOME sel => sel |
|
294 |> delete_empty_funs ? subtract (op =) deleted |
|
295 |> subtract (op =) hidden |
|
296 |> Graph.all_succs code |
|
297 |> delete_empty_funs ? subtract (op =) deleted |
|
298 |> subtract (op =) hidden; |
|
299 in |
|
300 code |
|
301 |> Graph.subgraph (member (op =) selected) |
|
302 end; |
|
303 |
|
304 fun empty_funs code = |
|
305 Graph.fold (fn (name, (Fun ([], _), _)) => cons name |
|
306 | _ => I) code []; |
|
307 |
|
308 fun is_cons code name = case Graph.get_node code name |
|
309 of Datatypecons _ => true |
|
310 | _ => false; |
|
311 |
|
312 fun check_samemodule names = |
|
313 fold (fn name => |
|
314 let |
|
315 val module_name = (NameSpace.qualifier o NameSpace.qualifier) name |
|
316 in |
|
317 fn NONE => SOME module_name |
|
318 | SOME module_name' => if module_name = module_name' then SOME module_name |
|
319 else error ("Inconsistent name prefix for simultanous names: " ^ commas_quote names) |
|
320 end |
|
321 ) names NONE; |
|
322 |
|
323 fun check_funeqs eqs = |
|
324 (fold (fn (pats, _) => |
|
325 let |
|
326 val l = length pats |
|
327 in |
|
328 fn NONE => SOME l |
|
329 | SOME l' => if l = l' then SOME l |
|
330 else error "Function definition with different number of arguments" |
|
331 end |
|
332 ) eqs NONE; eqs); |
|
333 |
|
334 fun check_prep_def code Bot = |
|
335 Bot |
|
336 | check_prep_def code (Fun (eqs, d)) = |
|
337 Fun (check_funeqs eqs, d) |
|
338 | check_prep_def code (d as Datatype _) = |
|
339 d |
|
340 | check_prep_def code (Datatypecons dtco) = |
|
341 error "Attempted to add bare term constructor" |
|
342 | check_prep_def code (d as Class _) = |
|
343 d |
|
344 | check_prep_def code (Classop _) = |
|
345 error "Attempted to add bare class operation" |
|
346 | check_prep_def code (Classrel _) = |
|
347 error "Attempted to add bare class relation" |
|
348 | check_prep_def code (d as Classinst ((class, (tyco, arity)), (_, inst_classops))) = |
|
349 let |
|
350 val Class (_, (_, classops)) = Graph.get_node code class; |
|
351 val _ = if length inst_classops > length classops |
|
352 then error "Too many class operations given" |
|
353 else (); |
|
354 fun check_classop (f, _) = |
|
355 if AList.defined (op =) inst_classops f |
|
356 then () else error ("Missing definition for class operation " ^ quote f); |
|
357 val _ = map check_classop classops; |
|
358 in d end; |
|
359 |
|
360 fun postprocess_def (name, Datatype (_, constrs)) = |
|
361 tap (fn _ => check_samemodule (name :: map fst constrs)) |
|
362 #> fold (fn (co, _) => |
|
363 add_def_incr (co, Datatypecons name) |
|
364 #> add_dep (co, name) |
|
365 #> add_dep (name, co) |
|
366 ) constrs |
|
367 | postprocess_def (name, Class (classrels, (_, classops))) = |
|
368 tap (fn _ => check_samemodule (name :: map fst classops @ map snd classrels)) |
|
369 #> fold (fn (f, _) => |
|
370 add_def_incr (f, Classop name) |
|
371 #> add_dep (f, name) |
|
372 #> add_dep (name, f) |
|
373 ) classops |
|
374 #> fold (fn (superclass, classrel) => |
|
375 add_def_incr (classrel, Classrel (name, superclass)) |
|
376 #> add_dep (classrel, name) |
|
377 #> add_dep (name, classrel) |
|
378 ) classrels |
|
379 | postprocess_def _ = |
|
380 I; |
|
381 |
|
382 |
|
383 (* transaction protocol *) |
|
384 |
|
385 fun ensure_def labelled_name defgen msg name (dep, code) = |
|
386 let |
|
387 val msg' = (case dep |
|
388 of NONE => msg |
|
389 | SOME dep => msg ^ ", required for " ^ labelled_name dep); |
|
390 fun add_dp NONE = I |
|
391 | add_dp (SOME dep) = |
|
392 tracing (fn _ => "adding dependency " ^ labelled_name dep |
|
393 ^ " -> " ^ labelled_name name) |
|
394 #> add_dep (dep, name); |
|
395 fun prep_def def code = |
|
396 (check_prep_def code def, code); |
|
397 fun invoke_generator name defgen code = |
|
398 defgen (SOME name, code) handle FAIL msgs => raise FAIL (msg' :: msgs); |
|
399 fun add_def false = |
|
400 ensure_bot name |
|
401 #> add_dp dep |
|
402 #> invoke_generator name defgen |
|
403 #-> (fn def => prep_def def) |
|
404 #-> (fn def => add_def_incr (name, def) |
|
405 #> postprocess_def (name, def)) |
|
406 | add_def true = |
|
407 add_dp dep; |
|
408 in |
|
409 code |
|
410 |> add_def (can (Graph.get_node code) name) |
|
411 |> pair dep |
|
412 end; |
|
413 |
|
414 fun succeed some (_, code) = (some, code); |
|
415 |
|
416 fun fail msg (_, code) = raise FAIL [msg]; |
|
417 |
|
418 fun message msg f trns = |
|
419 f trns handle FAIL msgs => |
|
420 raise FAIL (msg :: msgs); |
|
421 |
|
422 fun start_transact f code = |
|
423 let |
|
424 fun handle_fail f x = |
|
425 (f x |
|
426 handle FAIL msgs => |
|
427 (error o cat_lines) ("Code generation failed, while:" :: msgs)) |
|
428 in |
|
429 (NONE, code) |
|
430 |> handle_fail f |
|
431 |-> (fn x => fn (_, code) => (x, code)) |
|
432 end; |
|
433 |
|
434 fun add_eval_def (name, t) code = |
|
435 code |
|
436 |> Graph.new_node (name, Fun ([([], t)], ([("_", [])], ITyVar "_"))) |
|
437 |> fold (curry Graph.add_edge name) (Graph.keys code); |
|
438 |
|
439 end; (*struct*) |
|
440 |
|
441 |
|
442 structure BasicCodegenThingol: BASIC_CODEGEN_THINGOL = CodegenThingol; |
|