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