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