author | haftmann |
Thu, 04 Oct 2007 19:41:54 +0200 | |
changeset 24840 | 01b14b37eca3 |
parent 24837 | cacc5744be75 |
child 24918 | 22013215eece |
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 |
|
24811 | 66 |
| Class of vname * ((class * string) list * (string * itype) list) |
24219 | 67 |
| Classrel of class * class |
24837 | 68 |
| Classparam of class |
24219 | 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 |
24811 | 84 |
-> transact -> transact; |
24219 | 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 |
|
24837 | 138 |
const names (general) c (const) |
24219 | 139 |
constructor names co |
24837 | 140 |
class parameter names classparam |
24219 | 141 |
arbitrary name s |
142 |
||
24837 | 143 |
v, c, co, classparam also annotated with types etc. |
24219 | 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 |
|
24811 | 253 |
| Class of vname * ((class * string) list * (string * itype) list) |
24219 | 254 |
| Classrel of class * class |
24837 | 255 |
| Classparam of class |
24219 | 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 |
||
24811 | 279 |
fun add_dep (NONE, _) = I |
280 |
| add_dep (SOME name1, name2) = |
|
281 |
if name1 = name2 then I else Graph.add_edge (name1, name2); |
|
24219 | 282 |
|
283 |
val merge_code : code * code -> code = Graph.merge (K true); |
|
284 |
||
285 |
fun project_code delete_empty_funs hidden raw_selected code = |
|
286 |
let |
|
287 |
fun is_empty_fun name = case Graph.get_node code name |
|
24381 | 288 |
of Fun (_, []) => true |
24219 | 289 |
| _ => false; |
290 |
val names = subtract (op =) hidden (Graph.keys code); |
|
291 |
val deleted = Graph.all_preds code (filter is_empty_fun names); |
|
292 |
val selected = case raw_selected |
|
293 |
of NONE => names |> subtract (op =) deleted |
|
294 |
| SOME sel => sel |
|
295 |
|> delete_empty_funs ? subtract (op =) deleted |
|
296 |
|> subtract (op =) hidden |
|
297 |
|> Graph.all_succs code |
|
298 |
|> delete_empty_funs ? subtract (op =) deleted |
|
299 |
|> subtract (op =) hidden; |
|
300 |
in |
|
301 |
code |
|
302 |
|> Graph.subgraph (member (op =) selected) |
|
303 |
end; |
|
304 |
||
305 |
fun empty_funs code = |
|
24381 | 306 |
Graph.fold (fn (name, (Fun (_, []), _)) => cons name |
24219 | 307 |
| _ => I) code []; |
308 |
||
309 |
fun is_cons code name = case Graph.get_node code name |
|
310 |
of Datatypecons _ => true |
|
311 |
| _ => false; |
|
312 |
||
313 |
||
314 |
(* transaction protocol *) |
|
315 |
||
24283 | 316 |
type transact = Graph.key option * code; |
317 |
||
24811 | 318 |
fun ensure_def labelled_name defgen name (dep, code) = |
24219 | 319 |
let |
320 |
fun add_def false = |
|
321 |
ensure_bot name |
|
24811 | 322 |
#> add_dep (dep, name) |
24252 | 323 |
#> curry defgen (SOME name) |
324 |
##> snd |
|
24811 | 325 |
#-> (fn def => add_def_incr (name, def)) |
24219 | 326 |
| add_def true = |
24811 | 327 |
add_dep (dep, name); |
24219 | 328 |
in |
329 |
code |
|
330 |
|> add_def (can (Graph.get_node code) name) |
|
331 |
|> pair dep |
|
332 |
end; |
|
333 |
||
334 |
fun start_transact f code = |
|
24252 | 335 |
(NONE, code) |
336 |
|> f |
|
337 |
|-> (fn x => fn (_, code) => (x, code)); |
|
24219 | 338 |
|
24283 | 339 |
fun add_eval_def (name, (t, ty)) code = |
24219 | 340 |
code |
24591 | 341 |
|> Graph.new_node (name, Fun (([], ty), [(([], t), Drule.dummy_thm)])) |
24219 | 342 |
|> fold (curry Graph.add_edge name) (Graph.keys code); |
343 |
||
344 |
end; (*struct*) |
|
345 |
||
346 |
||
347 |
structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol; |