author | haftmann |
Thu, 20 Sep 2007 16:37:34 +0200 | |
changeset 24662 | f79f6061525c |
parent 24591 | 6509626eb2c9 |
child 24811 | 3bf788a0c49a |
permissions | -rw-r--r-- |
24219 | 1 |
(* Title: Tools/code/code_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_CODE_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; |
|
24591 | 25 |
type const = string * (dict list list * itype list (*types of arguments*)) |
24219 | 26 |
datatype iterm = |
24591 | 27 |
IConst of const |
24219 | 28 |
| IVar of vname |
29 |
| `$ of iterm * iterm |
|
30 |
| `|-> of (vname * itype) * iterm |
|
31 |
| ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; |
|
32 |
(*((term, type), [(selector pattern, body term )]), primitive term)*) |
|
33 |
val `-> : itype * itype -> itype; |
|
34 |
val `--> : itype list * itype -> itype; |
|
35 |
val `$$ : iterm * iterm list -> iterm; |
|
36 |
val `|--> : (vname * itype) list * iterm -> iterm; |
|
37 |
type typscheme = (vname * sort) list * itype; |
|
38 |
end; |
|
39 |
||
40 |
signature CODE_THINGOL = |
|
41 |
sig |
|
42 |
include BASIC_CODE_THINGOL; |
|
43 |
val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list; |
|
44 |
val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a; |
|
45 |
val unfold_fun: itype -> itype list * itype; |
|
46 |
val unfold_app: iterm -> iterm * iterm list; |
|
47 |
val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option; |
|
48 |
val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm; |
|
49 |
val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option; |
|
50 |
val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm; |
|
51 |
val unfold_const_app: iterm -> |
|
52 |
((string * (dict list list * itype list)) * iterm list) option; |
|
53 |
val collapse_let: ((vname * itype) * iterm) * iterm |
|
54 |
-> (iterm * itype) * (iterm * iterm) list; |
|
55 |
val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm; |
|
24662
f79f6061525c
more precise treatment of free dictionary parameters for evaluation
haftmann
parents:
24591
diff
changeset
|
56 |
val contains_dictvar: iterm -> bool; |
24219 | 57 |
val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; |
58 |
val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; |
|
59 |
val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; |
|
60 |
||
61 |
datatype def = |
|
62 |
Bot |
|
24591 | 63 |
| Fun of typscheme * ((iterm list * iterm) * thm) list |
24219 | 64 |
| Datatype of (vname * sort) list * (string * itype list) list |
65 |
| Datatypecons of string |
|
66 |
| Class of (class * string) list * (vname * (string * itype) list) |
|
67 |
| Classop of class |
|
68 |
| Classrel of class * class |
|
69 |
| Classinst of (class * (string * (vname * sort) list)) |
|
70 |
* ((class * (string * (string * dict list list))) list |
|
24591 | 71 |
* ((string * const) * thm) list); |
24219 | 72 |
type code = def Graph.T; |
73 |
type transact; |
|
74 |
val empty_code: code; |
|
75 |
val merge_code: code * code -> code; |
|
76 |
val project_code: bool (*delete empty funs*) |
|
77 |
-> string list (*hidden*) -> string list option (*selected*) |
|
78 |
-> code -> code; |
|
79 |
val empty_funs: code -> string list; |
|
80 |
val is_cons: code -> string -> bool; |
|
24283 | 81 |
val add_eval_def: string (*bind name*) * (iterm * itype) -> code -> code; |
24219 | 82 |
|
24252 | 83 |
val ensure_def: (string -> string) -> (transact -> def * transact) -> string |
24219 | 84 |
-> string -> transact -> transact; |
85 |
val start_transact: (transact -> 'a * transact) -> code -> 'a * code; |
|
86 |
end; |
|
87 |
||
88 |
structure CodeThingol: CODE_THINGOL = |
|
89 |
struct |
|
90 |
||
91 |
(** auxiliary **) |
|
92 |
||
93 |
fun unfoldl dest x = |
|
94 |
case dest x |
|
95 |
of NONE => (x, []) |
|
96 |
| SOME (x1, x2) => |
|
97 |
let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end; |
|
98 |
||
99 |
fun unfoldr dest x = |
|
100 |
case dest x |
|
101 |
of NONE => ([], x) |
|
102 |
| SOME (x1, x2) => |
|
103 |
let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end; |
|
104 |
||
105 |
||
106 |
(** language core - types, pattern, expressions **) |
|
107 |
||
108 |
(* language representation *) |
|
109 |
||
110 |
type vname = string; |
|
111 |
||
112 |
datatype dict = |
|
113 |
DictConst of string * dict list list |
|
114 |
| DictVar of string list * (vname * (int * int)); |
|
115 |
||
116 |
datatype itype = |
|
117 |
`%% of string * itype list |
|
118 |
| ITyVar of vname; |
|
119 |
||
24591 | 120 |
type const = string * (dict list list * itype list (*types of arguments*)) |
121 |
||
24219 | 122 |
datatype iterm = |
24591 | 123 |
IConst of const |
24219 | 124 |
| IVar of vname |
125 |
| `$ of iterm * iterm |
|
126 |
| `|-> of (vname * itype) * iterm |
|
127 |
| ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; |
|
128 |
(*see also signature*) |
|
129 |
||
130 |
(* |
|
131 |
variable naming conventions |
|
132 |
||
133 |
bare names: |
|
134 |
variable names v |
|
135 |
class names class |
|
136 |
type constructor names tyco |
|
137 |
datatype names dtco |
|
138 |
const names (general) c |
|
139 |
constructor names co |
|
140 |
class operation names clsop (op) |
|
141 |
arbitrary name s |
|
142 |
||
143 |
v, c, co, clsop also annotated with types etc. |
|
144 |
||
145 |
constructs: |
|
146 |
sort sort |
|
147 |
type parameters vs |
|
148 |
type ty |
|
149 |
type schemes tysm |
|
150 |
term t |
|
151 |
(term as pattern) p |
|
152 |
instance (class, tyco) inst |
|
153 |
*) |
|
154 |
||
155 |
fun ty1 `-> ty2 = "fun" `%% [ty1, ty2]; |
|
156 |
val op `--> = Library.foldr (op `->); |
|
157 |
val op `$$ = Library.foldl (op `$); |
|
158 |
val op `|--> = Library.foldr (op `|->); |
|
159 |
||
160 |
val unfold_fun = unfoldr |
|
161 |
(fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2) |
|
162 |
| _ => NONE); |
|
163 |
||
164 |
val unfold_app = unfoldl |
|
165 |
(fn op `$ t => SOME t |
|
166 |
| _ => NONE); |
|
167 |
||
168 |
val split_abs = |
|
169 |
(fn (v, ty) `|-> (t as ICase (((IVar w, _), [(p, t')]), _)) => |
|
170 |
if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t) |
|
171 |
| (v, ty) `|-> t => SOME (((v, NONE), ty), t) |
|
172 |
| _ => NONE); |
|
173 |
||
174 |
val unfold_abs = unfoldr split_abs; |
|
175 |
||
176 |
val split_let = |
|
177 |
(fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t) |
|
178 |
| _ => NONE); |
|
179 |
||
180 |
val unfold_let = unfoldr split_let; |
|
181 |
||
182 |
fun unfold_const_app t = |
|
183 |
case unfold_app t |
|
184 |
of (IConst c, ts) => SOME (c, ts) |
|
185 |
| _ => NONE; |
|
186 |
||
187 |
fun fold_aiterms f (t as IConst _) = f t |
|
188 |
| fold_aiterms f (t as IVar _) = f t |
|
189 |
| fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2 |
|
190 |
| fold_aiterms f (t as _ `|-> t') = f t #> fold_aiterms f t' |
|
191 |
| fold_aiterms f (ICase (_, t)) = fold_aiterms f t; |
|
192 |
||
193 |
fun fold_constnames f = |
|
194 |
let |
|
195 |
fun add (IConst (c, _)) = f c |
|
196 |
| add _ = I; |
|
197 |
in fold_aiterms add end; |
|
198 |
||
199 |
fun fold_varnames f = |
|
200 |
let |
|
201 |
fun add (IVar v) = f v |
|
202 |
| add ((v, _) `|-> _) = f v |
|
203 |
| add _ = I; |
|
204 |
in fold_aiterms add end; |
|
205 |
||
206 |
fun fold_unbound_varnames f = |
|
207 |
let |
|
208 |
fun add _ (IConst _) = I |
|
209 |
| add vs (IVar v) = if not (member (op =) vs v) then f v else I |
|
210 |
| add vs (t1 `$ t2) = add vs t1 #> add vs t2 |
|
211 |
| add vs ((v, _) `|-> t) = add (insert (op =) v vs) t |
|
212 |
| add vs (ICase (_, t)) = add vs t; |
|
213 |
in add [] end; |
|
214 |
||
215 |
fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) = |
|
216 |
let |
|
217 |
fun exists_v t = fold_unbound_varnames (fn w => fn b => |
|
218 |
b orelse v = w) t false; |
|
219 |
in if v = w andalso forall (fn (t1, t2) => |
|
220 |
exists_v t1 orelse not (exists_v t2)) ds |
|
221 |
then ((se, ty), ds) |
|
222 |
else ((se, ty), [(IVar v, be)]) |
|
223 |
end |
|
224 |
| collapse_let (((v, ty), se), be) = |
|
225 |
((se, ty), [(IVar v, be)]) |
|
226 |
||
227 |
fun eta_expand (c as (_, (_, tys)), ts) k = |
|
228 |
let |
|
229 |
val j = length ts; |
|
230 |
val l = k - j; |
|
231 |
val ctxt = (fold o fold_varnames) Name.declare ts Name.context; |
|
232 |
val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys); |
|
233 |
in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end; |
|
234 |
||
24662
f79f6061525c
more precise treatment of free dictionary parameters for evaluation
haftmann
parents:
24591
diff
changeset
|
235 |
fun contains_dictvar t = |
f79f6061525c
more precise treatment of free dictionary parameters for evaluation
haftmann
parents:
24591
diff
changeset
|
236 |
let |
f79f6061525c
more precise treatment of free dictionary parameters for evaluation
haftmann
parents:
24591
diff
changeset
|
237 |
fun contains (DictConst (_, dss)) = (fold o fold) contains dss |
f79f6061525c
more precise treatment of free dictionary parameters for evaluation
haftmann
parents:
24591
diff
changeset
|
238 |
| contains (DictVar _) = K true; |
f79f6061525c
more precise treatment of free dictionary parameters for evaluation
haftmann
parents:
24591
diff
changeset
|
239 |
in |
f79f6061525c
more precise treatment of free dictionary parameters for evaluation
haftmann
parents:
24591
diff
changeset
|
240 |
fold_aiterms |
f79f6061525c
more precise treatment of free dictionary parameters for evaluation
haftmann
parents:
24591
diff
changeset
|
241 |
(fn IConst (_, (dss, _)) => (fold o fold) contains dss | _ => I) t false |
f79f6061525c
more precise treatment of free dictionary parameters for evaluation
haftmann
parents:
24591
diff
changeset
|
242 |
end; |
f79f6061525c
more precise treatment of free dictionary parameters for evaluation
haftmann
parents:
24591
diff
changeset
|
243 |
|
24219 | 244 |
|
245 |
(** definitions, transactions **) |
|
246 |
||
247 |
type typscheme = (vname * sort) list * itype; |
|
248 |
datatype def = |
|
249 |
Bot |
|
24591 | 250 |
| Fun of typscheme * ((iterm list * iterm) * thm) list |
24219 | 251 |
| Datatype of (vname * sort) list * (string * itype list) list |
252 |
| Datatypecons of string |
|
253 |
| Class of (class * string) list * (vname * (string * itype) list) |
|
254 |
| Classop of class |
|
255 |
| Classrel of class * class |
|
256 |
| Classinst of (class * (string * (vname * sort) list)) |
|
257 |
* ((class * (string * (string * dict list list))) list |
|
24591 | 258 |
* ((string * const) * thm) list); |
24219 | 259 |
|
260 |
type code = def Graph.T; |
|
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 |
|
24381 | 287 |
of Fun (_, []) => true |
24219 | 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 = |
|
24381 | 305 |
Graph.fold (fn (name, (Fun (_, []), _)) => cons name |
24219 | 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 = |
|
24591 | 324 |
(fold (fn ((pats, _), _) => |
24219 | 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 |
|
24381 | 336 |
| check_prep_def code (Fun (d, eqs)) = |
337 |
Fun (d, check_funeqs eqs) |
|
24219 | 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, _) = |
|
24591 | 355 |
if AList.defined (op =) (map fst inst_classops) f |
24219 | 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 |
||
24283 | 385 |
type transact = Graph.key option * code; |
386 |
||
24219 | 387 |
fun ensure_def labelled_name defgen msg name (dep, code) = |
388 |
let |
|
389 |
val msg' = (case dep |
|
390 |
of NONE => msg |
|
391 |
| SOME dep => msg ^ ", required for " ^ labelled_name dep); |
|
392 |
fun add_dp NONE = I |
|
393 |
| add_dp (SOME dep) = add_dep (dep, name); |
|
394 |
fun prep_def def code = |
|
395 |
(check_prep_def code def, code); |
|
396 |
fun add_def false = |
|
397 |
ensure_bot name |
|
398 |
#> add_dp dep |
|
24252 | 399 |
#> curry defgen (SOME name) |
400 |
##> snd |
|
24219 | 401 |
#-> (fn def => prep_def def) |
402 |
#-> (fn def => add_def_incr (name, def) |
|
403 |
#> postprocess_def (name, def)) |
|
404 |
| add_def true = |
|
405 |
add_dp dep; |
|
406 |
in |
|
407 |
code |
|
408 |
|> add_def (can (Graph.get_node code) name) |
|
409 |
|> pair dep |
|
410 |
end; |
|
411 |
||
412 |
fun start_transact f code = |
|
24252 | 413 |
(NONE, code) |
414 |
|> f |
|
415 |
|-> (fn x => fn (_, code) => (x, code)); |
|
24219 | 416 |
|
24283 | 417 |
fun add_eval_def (name, (t, ty)) code = |
24219 | 418 |
code |
24591 | 419 |
|> Graph.new_node (name, Fun (([], ty), [(([], t), Drule.dummy_thm)])) |
24219 | 420 |
|> fold (curry Graph.add_edge name) (Graph.keys code); |
421 |
||
422 |
end; (*struct*) |
|
423 |
||
424 |
||
425 |
structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol; |