author | haftmann |
Fri, 12 Jan 2007 09:58:31 +0100 | |
changeset 22062 | f4cfc4101c8f |
parent 22037 | fbf0a12d053f |
child 22076 | 42ae57200d96 |
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 |
|
20855 | 5 |
Intermediate language ("Thin-gol") representing extracted 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; |
20456 | 19 |
datatype inst = |
20 |
Instance of string * inst list list |
|
21911
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21838
diff
changeset
|
21 |
| Context of (class list * int) * (vname * 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 = |
20456 | 26 |
IConst of string * (inst list list * itype) |
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 |
| INum of IntInf.int |
31 |
| IChar of string (*length one!*) |
|
32 |
| ICase of (iterm * itype) * (iterm * iterm) list; |
|
33 |
(*(discriminendum term (td), discriminendum type (ty)), |
|
34 |
[(selector pattern (p), body term (t))] (bs))*) |
|
21123 | 35 |
val `-> : itype * itype -> itype; |
20896 | 36 |
val `--> : itype list * itype -> itype; |
37 |
val `$$ : iterm * iterm list -> iterm; |
|
38 |
val `|--> : (vname * itype) list * iterm -> iterm; |
|
39 |
type typscheme = (vname * sort) list * itype; |
|
19136 | 40 |
end; |
41 |
||
42 |
signature CODEGEN_THINGOL = |
|
43 |
sig |
|
44 |
include BASIC_CODEGEN_THINGOL; |
|
18216 | 45 |
val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list; |
46 |
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
|
47 |
val unfold_fun: itype -> itype list * itype; |
20105 | 48 |
val unfold_app: iterm -> iterm * iterm list; |
22062 | 49 |
val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option; |
21012 | 50 |
val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm; |
22062 | 51 |
val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option; |
20105 | 52 |
val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm; |
53 |
val unfold_const_app: iterm -> |
|
20456 | 54 |
((string * (inst list list * itype)) * iterm list) option; |
55 |
val eta_expand: (string * (inst list list * itype)) * iterm list -> int -> iterm; |
|
20896 | 56 |
val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; |
57 |
val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; |
|
58 |
val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a; |
|
18170 | 59 |
|
60 |
datatype def = |
|
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19785
diff
changeset
|
61 |
Bot |
20456 | 62 |
| Fun of (iterm list * iterm) list * typscheme |
63 |
| Datatype of (vname * sort) list * (string * itype list) list |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
64 |
| Datatypecons of string |
20456 | 65 |
| Class of class list * (vname * (string * itype) list) |
21082 | 66 |
| Classop of class |
20389 | 67 |
| Classinst of (class * (string * (vname * sort) list)) |
20466 | 68 |
* ((class * (string * inst 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; |
20896 | 84 |
val start_transact: string option -> (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 |
|
20456 | 117 |
datatype inst = |
118 |
Instance of string * inst list list |
|
21911
e29bcab0c81c
added OCaml code generation (without dictionaries)
haftmann
parents:
21838
diff
changeset
|
119 |
| Context of (class list * int) * (vname * 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 = |
20456 | 126 |
IConst of string * (inst list list * itype) |
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 |
| INum of IntInf.int |
131 |
| IChar of string |
|
132 |
| ICase of (iterm * itype) * (iterm * iterm) list; |
|
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
133 |
(*see also signature*) |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
134 |
|
18380
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 |
variable naming conventions |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
137 |
|
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
138 |
bare names: |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
139 |
variable names v |
20439 | 140 |
class names class |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
141 |
type constructor names tyco |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
142 |
datatype names dtco |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
143 |
const names (general) c |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
144 |
constructor names co |
20439 | 145 |
class operation names clsop (op) |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
146 |
arbitrary name s |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
147 |
|
20896 | 148 |
v, c, co, clsop also annotated with types etc. |
20439 | 149 |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
150 |
constructs: |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
151 |
sort sort |
20456 | 152 |
type parameters vs |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
153 |
type ty |
20456 | 154 |
type schemes tysm |
20439 | 155 |
term t |
156 |
(term as pattern) p |
|
21838 | 157 |
instance (class, tyco) inst |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
158 |
*) |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
159 |
|
21123 | 160 |
fun ty1 `-> ty2 = "fun" `%% [ty1, ty2]; |
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
161 |
val op `--> = Library.foldr (op `->); |
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
162 |
val op `$$ = Library.foldl (op `$); |
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19150
diff
changeset
|
163 |
val op `|--> = Library.foldr (op `|->); |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
164 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
165 |
val unfold_fun = unfoldr |
21123 | 166 |
(fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2) |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
167 |
| _ => NONE); |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
168 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
169 |
val unfold_app = unfoldl |
20439 | 170 |
(fn op `$ t => SOME t |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
171 |
| _ => NONE); |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
172 |
|
22062 | 173 |
val split_abs = |
21012 | 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) |
|
22062 | 177 |
| _ => NONE); |
18282 | 178 |
|
22062 | 179 |
val unfold_abs = unfoldr split_abs; |
180 |
||
181 |
val split_let = |
|
21012 | 182 |
(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
|
183 |
| _ => NONE); |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
184 |
|
22062 | 185 |
val unfold_let = unfoldr split_let; |
186 |
||
20439 | 187 |
fun unfold_const_app t = |
188 |
case unfold_app t |
|
189 |
of (IConst c, ts) => SOME (c, ts) |
|
18865 | 190 |
| _ => NONE; |
191 |
||
20896 | 192 |
fun fold_aiterms f (t as IConst _) = |
193 |
f t |
|
194 |
| fold_aiterms f (t as IVar _) = |
|
195 |
f t |
|
196 |
| fold_aiterms f (t1 `$ t2) = |
|
197 |
fold_aiterms f t1 #> fold_aiterms f t2 |
|
198 |
| fold_aiterms f (t as _ `|-> t') = |
|
199 |
f t #> fold_aiterms f t' |
|
21012 | 200 |
| fold_aiterms f (t as INum _) = |
201 |
f t |
|
202 |
| fold_aiterms f (t as IChar _) = |
|
203 |
f t |
|
204 |
| fold_aiterms f (ICase ((td, _), bs)) = |
|
205 |
fold_aiterms f td #> fold (fn (p, t) => fold_aiterms f p #> fold_aiterms f t) bs; |
|
19202 | 206 |
|
20896 | 207 |
fun fold_constnames f = |
208 |
let |
|
209 |
fun add (IConst (c, _)) = f c |
|
210 |
| add _ = I; |
|
211 |
in fold_aiterms add end; |
|
18885 | 212 |
|
20896 | 213 |
fun fold_varnames f = |
214 |
let |
|
215 |
fun add (IVar v) = f v |
|
216 |
| add ((v, _) `|-> _) = f v |
|
217 |
| add _ = I; |
|
218 |
in fold_aiterms add end; |
|
20709 | 219 |
|
20896 | 220 |
fun fold_unbound_varnames f = |
18885 | 221 |
let |
20896 | 222 |
fun add _ (IConst _) = |
223 |
I |
|
224 |
| add vs (IVar v) = |
|
225 |
if not (member (op =) vs v) then f v else I |
|
226 |
| add vs (t1 `$ t2) = |
|
227 |
add vs t1 #> add vs t2 |
|
228 |
| add vs ((v, _) `|-> t) = |
|
229 |
add (insert (op =) v vs) t |
|
21012 | 230 |
| add vs (INum _) = |
231 |
I |
|
232 |
| add vs (IChar _) = |
|
233 |
I |
|
234 |
| add vs (ICase ((td, _), bs)) = |
|
235 |
add vs td #> fold (fn (p, t) => add vs p #> add vs t) bs; |
|
20896 | 236 |
in add [] end; |
20105 | 237 |
|
20439 | 238 |
fun eta_expand (c as (_, (_, ty)), ts) k = |
19607
07eeb832f28d
introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents:
19597
diff
changeset
|
239 |
let |
20439 | 240 |
val j = length ts; |
19607
07eeb832f28d
introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents:
19597
diff
changeset
|
241 |
val l = k - j; |
07eeb832f28d
introduced characters for code generator; some improved code lemmas for some list functions
haftmann
parents:
19597
diff
changeset
|
242 |
val tys = (curry Library.take l o curry Library.drop j o fst o unfold_fun) ty; |
20896 | 243 |
val ctxt = (fold o fold_varnames) Name.declare ts Name.context; |
244 |
val vs_tys = Name.names ctxt "a" tys; |
|
20439 | 245 |
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
|
246 |
|
18304 | 247 |
|
20896 | 248 |
(** definitions, transactions **) |
18170 | 249 |
|
250 |
(* type definitions *) |
|
251 |
||
20456 | 252 |
type typscheme = (vname * sort) list * itype; |
18170 | 253 |
datatype def = |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19785
diff
changeset
|
254 |
Bot |
20456 | 255 |
| Fun of (iterm list * iterm) list * typscheme |
256 |
| Datatype of (vname * sort) list * (string * itype list) list |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
257 |
| Datatypecons of string |
20456 | 258 |
| Class of class list * (vname * (string * itype) list) |
21082 | 259 |
| Classop of class |
20389 | 260 |
| Classinst of (class * (string * (vname * sort) list)) |
20466 | 261 |
* ((class * (string * inst list list)) list |
20456 | 262 |
* (string * iterm) list); |
19597 | 263 |
val eq_def = (op =) : def * def -> bool; |
18170 | 264 |
|
20896 | 265 |
type code = def Graph.T; |
266 |
type transact = Graph.key option * code; |
|
21012 | 267 |
exception FAIL of string list; |
18360 | 268 |
|
18170 | 269 |
|
20896 | 270 |
(* abstract code *) |
18170 | 271 |
|
20896 | 272 |
val empty_code = Graph.empty : code; (*read: "depends on"*) |
18170 | 273 |
|
20896 | 274 |
val get_def = Graph.get_node; |
18170 | 275 |
|
20896 | 276 |
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
|
277 |
|
20896 | 278 |
fun add_def_incr strict (name, Bot) code = |
279 |
(case the_default Bot (try (get_def code) name) |
|
280 |
of Bot => if strict then error "Attempted to add Bot to code" |
|
281 |
else Graph.map_node name (K Bot) code |
|
282 |
| _ => code) |
|
283 |
| add_def_incr _ (name, def) code = |
|
284 |
(case try (get_def code) name |
|
285 |
of NONE => Graph.new_node (name, def) code |
|
286 |
| 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
|
287 |
| SOME def' => if eq_def (def, def') |
20896 | 288 |
then code |
20389 | 289 |
else error ("Tried to overwrite definition " ^ quote name)); |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19785
diff
changeset
|
290 |
|
20896 | 291 |
fun add_dep (dep as (name1, name2)) = |
292 |
if name1 = name2 then I else Graph.add_edge dep; |
|
18170 | 293 |
|
20896 | 294 |
val merge_code = Graph.join (fn _ => fn def12 => if eq_def def12 then fst def12 else Bot); |
18170 | 295 |
|
21012 | 296 |
fun project_code hidden raw_selected code = |
20466 | 297 |
let |
20896 | 298 |
fun is_bot name = case get_def code name |
299 |
of Bot => true |
|
300 |
| _ => false; |
|
301 |
val names = subtract (op =) hidden (Graph.keys code); |
|
21012 | 302 |
val deleted = Graph.all_preds code (filter is_bot names); |
303 |
val selected = case raw_selected |
|
304 |
of NONE => names |> subtract (op =) deleted |
|
305 |
| SOME sel => sel |
|
306 |
|> subtract (op =) deleted |
|
307 |
|> subtract (op =) hidden |
|
308 |
|> Graph.all_succs code |
|
309 |
|> subtract (op =) deleted |
|
310 |
|> subtract (op =) hidden; |
|
20191 | 311 |
in |
21012 | 312 |
code |
21937 | 313 |
|> Graph.subgraph (member (op =) selected) |
20191 | 314 |
end; |
315 |
||
18702 | 316 |
fun check_samemodule names = |
317 |
fold (fn name => |
|
318 |
let |
|
20896 | 319 |
val module_name = (NameSpace.qualifier o NameSpace.qualifier) name |
18702 | 320 |
in |
20896 | 321 |
fn NONE => SOME module_name |
322 |
| SOME module_name' => if module_name = module_name' then SOME module_name |
|
20386 | 323 |
else error ("Inconsistent name prefix for simultanous names: " ^ commas_quote names) |
18702 | 324 |
end |
325 |
) names NONE; |
|
326 |
||
327 |
fun check_funeqs eqs = |
|
328 |
(fold (fn (pats, _) => |
|
329 |
let |
|
330 |
val l = length pats |
|
331 |
in |
|
332 |
fn NONE => SOME l |
|
18850 | 333 |
| SOME l' => if l = l' then SOME l |
20389 | 334 |
else error "Function definition with different number of arguments" |
18702 | 335 |
end |
336 |
) eqs NONE; eqs); |
|
337 |
||
21082 | 338 |
fun check_prep_def code Bot = |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19785
diff
changeset
|
339 |
Bot |
21082 | 340 |
| check_prep_def code (Fun (eqs, d)) = |
18702 | 341 |
Fun (check_funeqs eqs, d) |
21082 | 342 |
| check_prep_def code (d as Datatype _) = |
19038 | 343 |
d |
21082 | 344 |
| check_prep_def code (Datatypecons dtco) = |
20389 | 345 |
error "Attempted to add bare datatype constructor" |
21082 | 346 |
| check_prep_def code (d as Class _) = |
19038 | 347 |
d |
21082 | 348 |
| check_prep_def code (Classop _) = |
20389 | 349 |
error "Attempted to add bare class member" |
21082 | 350 |
| check_prep_def code (d as Classinst ((class, (tyco, arity)), (_, memdefs))) = |
18170 | 351 |
let |
21082 | 352 |
val Class (_, (v, membrs)) = get_def code class; |
18702 | 353 |
val _ = if length memdefs > length memdefs |
20389 | 354 |
then error "Too many member definitions given" |
18702 | 355 |
else (); |
20389 | 356 |
fun check_memdef (m, _) = |
357 |
if AList.defined (op =) memdefs m |
|
358 |
then () else error ("Missing definition for member " ^ quote m); |
|
359 |
val _ = map check_memdef memdefs; |
|
360 |
in d end |
|
21082 | 361 |
| check_prep_def code Classinstmember = |
20389 | 362 |
error "Attempted to add bare class instance member"; |
18170 | 363 |
|
19038 | 364 |
fun postprocess_def (name, Datatype (_, constrs)) = |
18702 | 365 |
(check_samemodule (name :: map fst constrs); |
366 |
fold (fn (co, _) => |
|
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19785
diff
changeset
|
367 |
add_def_incr true (co, Datatypecons name) |
18702 | 368 |
#> add_dep (co, name) |
369 |
#> add_dep (name, co) |
|
370 |
) constrs |
|
371 |
) |
|
19038 | 372 |
| postprocess_def (name, Class (_, (_, membrs))) = |
18702 | 373 |
(check_samemodule (name :: map fst membrs); |
374 |
fold (fn (m, _) => |
|
21082 | 375 |
add_def_incr true (m, Classop name) |
18702 | 376 |
#> add_dep (m, name) |
377 |
#> add_dep (name, m) |
|
378 |
) membrs |
|
379 |
) |
|
380 |
| postprocess_def _ = |
|
381 |
I; |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
382 |
|
19884 | 383 |
|
384 |
(* transaction protocol *) |
|
18170 | 385 |
|
22037 | 386 |
fun ensure_def labelled_name defgen strict msg name (dep, code) = |
18170 | 387 |
let |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19785
diff
changeset
|
388 |
val msg' = (case dep |
18702 | 389 |
of NONE => msg |
22037 | 390 |
| SOME dep => msg ^ ", required for " ^ labelled_name dep) |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19785
diff
changeset
|
391 |
^ (if strict then " (strict)" else " (non-strict)"); |
18702 | 392 |
fun add_dp NONE = I |
393 |
| add_dp (SOME dep) = |
|
22037 | 394 |
tracing (fn _ => "adding dependency " ^ labelled_name dep |
395 |
^ " -> " ^ labelled_name name) |
|
18702 | 396 |
#> add_dep (dep, name); |
21082 | 397 |
fun prep_def def code = |
398 |
(check_prep_def code def, code); |
|
399 |
fun invoke_generator name defgen code = |
|
400 |
defgen (SOME name, code) |
|
21012 | 401 |
handle FAIL msgs => |
402 |
if strict then raise FAIL (msg' :: msgs) |
|
21082 | 403 |
else (Bot, code); |
18170 | 404 |
in |
21082 | 405 |
code |
406 |
|> (if can (get_def code) name |
|
18702 | 407 |
then |
22037 | 408 |
tracing (fn _ => "asserting definition " ^ labelled_name name) |
18702 | 409 |
#> add_dp dep |
410 |
else |
|
22037 | 411 |
tracing (fn _ => "allocating definition " ^ labelled_name name |
412 |
^ (if strict then " (strict)" else " (non-strict)")) |
|
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19785
diff
changeset
|
413 |
#> ensure_bot name |
18702 | 414 |
#> add_dp dep |
22037 | 415 |
#> tracing (fn _ => "creating definition " ^ labelled_name name) |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19785
diff
changeset
|
416 |
#> invoke_generator name defgen |
18702 | 417 |
#-> (fn def => prep_def def) |
418 |
#-> (fn def => |
|
20896 | 419 |
tracing (fn _ => "adding") |
19816
a8c8ed1c85e0
removed 'primitive definitions' added (non)strict generation, minor fixes
haftmann
parents:
19785
diff
changeset
|
420 |
#> add_def_incr strict (name, def) |
20835 | 421 |
#> tracing (fn _ => "postprocessing") |
18702 | 422 |
#> postprocess_def (name, def) |
20835 | 423 |
#> tracing (fn _ => "adding done") |
18702 | 424 |
)) |
425 |
|> pair dep |
|
18170 | 426 |
end; |
427 |
||
21082 | 428 |
fun succeed some (_, code) = (some, code); |
19884 | 429 |
|
21082 | 430 |
fun fail msg (_, code) = raise FAIL [msg]; |
19884 | 431 |
|
432 |
fun message msg f trns = |
|
21012 | 433 |
f trns handle FAIL msgs => |
434 |
raise FAIL (msg :: msgs); |
|
19884 | 435 |
|
21082 | 436 |
fun start_transact init f code = |
18231 | 437 |
let |
18963 | 438 |
fun handle_fail f x = |
439 |
(f x |
|
21012 | 440 |
handle FAIL msgs => |
20389 | 441 |
(error o cat_lines) ("Code generation failed, while:" :: msgs)) |
18231 | 442 |
in |
21082 | 443 |
code |
19884 | 444 |
|> (if is_some init then ensure_bot (the init) else I) |
445 |
|> pair init |
|
18231 | 446 |
|> handle_fail f |
21082 | 447 |
|-> (fn x => fn (_, code) => (x, code)) |
18231 | 448 |
end; |
18172 | 449 |
|
21160 | 450 |
fun add_eval_def (name, t) code = |
451 |
code |
|
452 |
|> Graph.new_node (name, Fun ([([], t)], ([("_", [])], ITyVar "_"))) |
|
453 |
|> fold (curry Graph.add_edge name) (Graph.keys code); |
|
18172 | 454 |
|
20896 | 455 |
end; (*struct*) |
18885 | 456 |
|
18216 | 457 |
|
19300 | 458 |
structure BasicCodegenThingol: BASIC_CODEGEN_THINGOL = CodegenThingol; |