1 |
(* copyright 1998 YALE FLINT PROJECT *) |
(* copyright 1998 YALE FLINT PROJECT *) |
2 |
|
(* monnier@cs.yale.edu *) |
3 |
|
|
4 |
signature FCONTRACT = |
signature FCONTRACT = |
5 |
sig |
sig |
17 |
* be careful to make sure that a dead variable will indeed not appear |
* be careful to make sure that a dead variable will indeed not appear |
18 |
* in the output lexp since it might else reference other dead variables *) |
* in the output lexp since it might else reference other dead variables *) |
19 |
|
|
20 |
|
(* things that fcontract does: |
21 |
|
* - several things not mentioned |
22 |
|
* - elimination of Con(Decon x) |
23 |
|
* - update counts when selecting a SWITCH alternative |
24 |
|
*) |
25 |
|
|
26 |
(* things that lcontract.sml does that fcontract doesn't do (yet): |
(* things that lcontract.sml does that fcontract doesn't do (yet): |
27 |
* - inline across DeBruijn depths |
* - inline across DeBruijn depths (will be solved by named-tvar) |
28 |
* - elimination of let [dead-vs] = pure in body |
* - elimination of let [dead-vs] = pure in body |
29 |
*) |
*) |
30 |
|
|
33 |
*) |
*) |
34 |
|
|
35 |
(* things that cpsopt/contract.sml did that fcontract doesn't do: |
(* things that cpsopt/contract.sml did that fcontract doesn't do: |
36 |
* - IF-idiom |
* - IF-idiom (I still don't know what it is) |
37 |
* - unifying branches |
* - unifying branches |
38 |
* - Handler operations |
* - Handler operations |
39 |
* - primops expressions |
* - primops expressions |
43 |
|
|
44 |
(* things that could also be added: |
(* things that could also be added: |
45 |
* - elimination of dead vars in let (subsumes what lcontract does) |
* - elimination of dead vars in let (subsumes what lcontract does) |
|
* - elimination of Con(Decon x) |
|
46 |
* - elimination of Record(a.1, a.2, ...) |
* - elimination of Record(a.1, a.2, ...) |
|
* - update counts when selecting a SWITCH alternative |
|
47 |
*) |
*) |
48 |
|
|
49 |
(* things that would require some type info: |
(* things that would require some type info: |
71 |
* transfer incremental: each time we apply the substitution, we decrement |
* transfer incremental: each time we apply the substitution, we decrement |
72 |
* f's count and increment g's count. But this can be tricky since the |
* f's count and increment g's count. But this can be tricky since the |
73 |
* elimination of the eta-redex (or the trivial binding) eliminates one of the |
* elimination of the eta-redex (or the trivial binding) eliminates one of the |
74 |
* references to g and if thyis is the only one, we might trigger the killing |
* references to g and if this is the only one, we might trigger the killing |
75 |
* of g even though its count would be later incremented. Similarly, inlining |
* of g even though its count would be later incremented. Similarly, inlining |
76 |
* of g would be dangerous as long as some references to f exist. |
* of g would be dangerous as long as some references to f exist. |
77 |
* So instead we do the transfer once and for all when we see the eta-redex, |
* So instead we do the transfer once and for all when we see the eta-redex, |
84 |
* external counts. |
* external counts. |
85 |
*) |
*) |
86 |
|
|
87 |
|
(* Preventing infinite inlining: |
88 |
|
* - inlining a function in its own body amounts to unrolling which has |
89 |
|
* to be controlled (you only want to unroll some number of times). |
90 |
|
* It's currently simply not allowed. |
91 |
|
* - inlining a recursive function outside of tis body amounts to `peeling' |
92 |
|
* one iteration. Here also, since the inlined body will have yet another |
93 |
|
* call, the inlining risks non-termination. It's hence also |
94 |
|
* not allowed. |
95 |
|
* - inlining a mutually recursive function is just a more general form |
96 |
|
* of the problem above although it can be safe and desirable in some cases. |
97 |
|
* To be safe, you simply need that one of the functions forming the |
98 |
|
* mutual-recursion loop cannot be inlined (to break the loop). This cannot |
99 |
|
* be trivially checked. So we (foolishly?) trust the `inline' bit in |
100 |
|
* those cases. This is mostly used to inline wrappers inside the |
101 |
|
* function they wrap. |
102 |
|
* - even if one only allows inlining of funtions showing no sign of |
103 |
|
* recursion, we can be bitten by a program creating its own Y combinator: |
104 |
|
* datatype dt = F of dt -> int -> int |
105 |
|
* let fun f (F g) x = g (F g) x in f (F f) end |
106 |
|
* To solve this problem, `cexp' has an `ifs' parameter containing the set |
107 |
|
* of funtions that we are inlining in order to detect (and break) cycles. |
108 |
|
* - funnily enough, if we allow inlining recursive functions the cycle |
109 |
|
* detection will ensure that the unrolling (or peeling) will only be done |
110 |
|
* once. In the future, maybe. |
111 |
|
*) |
112 |
|
|
113 |
(* Simple inlining (inlining called-once functions, which doesn't require |
(* Simple inlining (inlining called-once functions, which doesn't require |
114 |
* alpha-renaming) seems inoffensive enough but is not always desirable. |
* alpha-renaming) seems inoffensive enough but is not always desirable. |
115 |
* The typical example is wrapper functions introduced by fexpand: they |
* The typical example is wrapper functions introduced by eta-expand: they |
116 |
* usually (until inlined) contain the only call the the main function, |
* usually (until inlined) contain the only call to the main function, |
117 |
* but inlining the main function in the wrapper defeats the purpose of the |
* but inlining the main function in the wrapper defeats the purpose of the |
118 |
* wrapper. |
* wrapper. |
119 |
* cpsopt dealt with this problem by adding a `NO_INLINE_INTO' hint to the |
* cpsopt dealt with this problem by adding a `NO_INLINE_INTO' hint to the |
120 |
* wrapper function. In this file, the idea is to be careful instead: |
* wrapper function. In this file, the idea is the following: |
121 |
|
* If you have a function declaration like `let f x = body in exp', first |
122 |
|
* contract `exp' and only contract `body' afterwards. This ensures that |
123 |
|
* the eta-wrapper gets a chance to be inlined before it is (potentially) |
124 |
|
* eta-reduced away. Interesting details: |
125 |
* - all functions (even the ones that would have a `NO_INLINE_INTO') are |
* - all functions (even the ones that would have a `NO_INLINE_INTO') are |
126 |
* contracted, because the "aggressive usage count maintenance" makes any |
* contracted, because the "aggressive usage count maintenance" makes any |
127 |
* alternative painful (the collect phase has already assumed that dead code |
* alternative painful (the collect phase has already assumed that dead code |
128 |
* will be eliminated, which means that fcontract should at the very least |
* will be eliminated, which means that fcontract should at the very least |
129 |
* do the dead-code elimination, so you can only avoid fcontracting if you |
* do the dead-code elimination, so you can only avoid fcontracting a |
130 |
* can be sure that the body doesn't contain any dead-code, which is generally |
* a function if you can be sure that the body doesn't contain any dead-code, |
131 |
* not known). |
* which is generally not known). |
132 |
* - once a function is fcontracted it is marked as non-inlinable since |
* - once a function is fcontracted it is marked as non-inlinable since |
133 |
* fcontractiong might have changed its form considerably (via inlining). |
* fcontraction might have changed its shape considerably (via inlining). |
134 |
* - to ensure that this de-inlining doesn't prevent too much inlining, the |
* This means that in the case of |
135 |
* inlineable functions should be contracted late. |
* let fwrap x = body1 and f y = body2 in exp |
136 |
|
* if fwrap is fcontracted before f, then fwrap cannot be inlined in f. |
137 |
|
* To minimize the impact of this problem, we make sure that we fcontract |
138 |
|
* inlinable functions only after fcontracting other mutually recursive |
139 |
|
* functions. |
140 |
* - at the very end of the optimization phase, cpsopt had a special pass |
* - at the very end of the optimization phase, cpsopt had a special pass |
141 |
* that ignored the `NO_INLINE_INTO' hint (since at this stage, inlining |
* that ignored the `NO_INLINE_INTO' hint (since at this stage, inlining |
142 |
* into it doesn't have any undesirable side effects any more). The present |
* into it doesn't have any undesirable side effects any more). The present |
143 |
* code doesn't need such a thing. On another hand, the cpsopt approach |
* code doesn't need such a thing. On another hand, the cpsopt approach |
144 |
* had the advantage of keeping the `inline' bit from one contract phase to |
* had the advantage of keeping the `inline' bit from one contract phase to |
145 |
* the next. If this ends up being important, I could add a global |
* the next. If this ends up being important, one could add a global |
146 |
* "noinline" flag that could be set to true whenever fcontracting an |
* "noinline" flag that could be set to true whenever fcontracting an |
147 |
* inlinable function. |
* inlinable function (this would ensure that fcontracting such an inlinable |
148 |
|
* function can only reduce its size, which would allow keeping the `inline' |
149 |
|
* bit set after fcontracting). |
150 |
*) |
*) |
151 |
|
|
152 |
structure FContract :> FCONTRACT = |
structure FContract :> FCONTRACT = |
154 |
local |
local |
155 |
structure F = FLINT |
structure F = FLINT |
156 |
structure M = IntmapF |
structure M = IntmapF |
157 |
|
structure S = IntSetF |
158 |
structure C = Collect |
structure C = Collect |
159 |
structure DI = DebIndex |
structure DI = DebIndex |
160 |
structure PP = PPFlint |
structure PP = PPFlint |
161 |
structure LV = LambdaVar |
structure FU = FlintUtil |
162 |
|
structure LT = LtyExtern |
163 |
|
structure CTRL = Control.FLINT |
164 |
in |
in |
165 |
|
|
166 |
val say = Control.Print.say |
val say = Control.Print.say |
173 |
fun ASSERT (true,_) = () |
fun ASSERT (true,_) = () |
174 |
| ASSERT (FALSE,msg) = bug ("assertion "^msg^" failed") |
| ASSERT (FALSE,msg) = bug ("assertion "^msg^" failed") |
175 |
|
|
176 |
(* copy an lexp, with alpha renaming. Could be moved to flint.sml |
val cplv = LambdaVar.dupLvar |
|
* since it's very generic (though probably not useful at many other places) *) |
|
|
fun copy alpha le = let |
|
|
fun substvar lv = ((M.lookup alpha lv) handle M.IntmapF => lv) |
|
|
fun substval (F.VAR lv) = F.VAR(substvar lv) |
|
|
| substval v = v |
|
|
fun newv (lv,alpha) = |
|
|
let val nlv = LV.mkLvar() in (nlv, M.add(alpha,lv,nlv)) end |
|
|
fun newvs (lvs,alpha) = |
|
|
foldr (fn (lv,(lvs,alpha)) => |
|
|
let val (nlv,nalpha) = newv(lv,alpha) in (nlv::lvs,nalpha) end) |
|
|
([],alpha) lvs |
|
|
fun cdcon (s,Access.EXN(Access.LVAR lv),lty) = |
|
|
(s, Access.EXN(Access.LVAR(substvar lv)), lty) |
|
|
| cdcon dc = dc |
|
|
fun cpo (SOME{default,table},po,lty,tycs) = |
|
|
(SOME{default=substvar default, |
|
|
table=map (fn (tycs,lv) => (tycs, substvar lv)) table}, |
|
|
po,lty,tycs) |
|
|
| cpo po = po |
|
|
in case le |
|
|
of F.RET vs => F.RET(map substval vs) |
|
|
| F.LET (lvs,le,body) => |
|
|
let val nle = copy alpha le |
|
|
val (nlvs,nalpha) = newvs(lvs,alpha) |
|
|
in F.LET(nlvs, nle, copy nalpha body) |
|
|
end |
|
|
| F.FIX (fdecs,le) => |
|
|
let fun cfun alpha ((fk,f,args,body):F.fundec,nf) = |
|
|
let val (nargs,nalpha) = newvs(map #1 args, alpha) |
|
|
in (fk, nf, ListPair.zip(nargs, (map #2 args)), copy nalpha body) |
|
|
end |
|
|
val (nfs, nalpha) = newvs(map #2 fdecs, alpha) |
|
|
val nfdecs = ListPair.map (cfun nalpha) (fdecs, nfs) |
|
|
in |
|
|
F.FIX(nfdecs, copy nalpha le) |
|
|
end |
|
|
| F.APP (f,args) => F.APP(substval f, map substval args) |
|
|
| F.TFN ((lv,args,body),le) => |
|
|
(* don't forget to rename the tvar also *) |
|
|
let val (nlv,nalpha) = newv(lv,alpha) |
|
|
val (nargs,ialpha) = newvs(map #1 args, nalpha) |
|
|
in F.TFN((nlv, ListPair.zip(nargs, map #2 args), copy ialpha body), |
|
|
copy nalpha le) |
|
|
end |
|
|
| F.TAPP (f,tycs) => F.TAPP(substval f, tycs) |
|
|
| F.SWITCH (v,ac,arms,def) => |
|
|
let fun carm (F.DATAcon(dc,tycs,lv),le) = |
|
|
let val (nlv,nalpha) = newv(lv, alpha) |
|
|
in (F.DATAcon(cdcon dc, tycs, nlv), copy nalpha le) |
|
|
end |
|
|
| carm (con,le) = (con, copy alpha le) |
|
|
in F.SWITCH(substval v, ac, map carm arms, Option.map (copy alpha) def) |
|
|
end |
|
|
| F.CON (dc,tycs,v,lv,le) => |
|
|
let val (nlv,nalpha) = newv(lv, alpha) |
|
|
in F.CON(cdcon dc, tycs, substval v, nlv, copy nalpha le) |
|
|
end |
|
|
| F.RECORD (rk,vs,lv,le) => |
|
|
let val (nlv,nalpha) = newv(lv, alpha) |
|
|
in F.RECORD(rk, map substval vs, nlv, copy nalpha le) |
|
|
end |
|
|
| F.SELECT (v,i,lv,le) => |
|
|
let val (nlv,nalpha) = newv(lv, alpha) |
|
|
in F.SELECT(substval v, i, nlv, copy nalpha le) |
|
|
end |
|
|
| F.RAISE (v,ltys) => F.RAISE(substval v, ltys) |
|
|
| F.HANDLE (le,v) => F.HANDLE(copy alpha le, substval v) |
|
|
| F.BRANCH (po,vs,le1,le2) => |
|
|
F.BRANCH(cpo po, map substval vs, copy alpha le1, copy alpha le2) |
|
|
| F.PRIMOP (po,vs,lv,le) => |
|
|
let val (nlv,nalpha) = newv(lv, alpha) |
|
|
in F.PRIMOP(cpo po, map substval vs, nlv, copy nalpha le) |
|
|
end |
|
|
end |
|
177 |
|
|
178 |
datatype sval |
datatype sval |
179 |
= Val of F.value (* F.value should never be F.VAR lv *) |
= Val of F.value (* F.value should never be F.VAR lv *) |
180 |
| Fun of F.lvar * F.lexp * (F.lvar * F.lty) list * F.fkind * DI.depth |
| Fun of F.lvar * F.lexp * (F.lvar * F.lty) list * F.fkind * DI.depth |
181 |
| TFun of F.lvar * F.lexp * (F.tvar * F.tkind) list * DI.depth |
| TFun of F.lvar * F.lexp * (F.tvar * F.tkind) list * DI.depth |
182 |
| Record of F.lvar * F.value list |
| Record of F.lvar * F.value list |
183 |
| Con of F.lvar * F.value * F.dcon |
| Con of F.lvar * F.value * F.dcon * F.tyc list |
184 |
|
| Decon of F.lvar * F.value * F.dcon * F.tyc list |
185 |
| Select of F.lvar * F.value * int |
| Select of F.lvar * F.value * int |
186 |
| Var of F.lvar * F.lty option (* cop out case *) |
| Var of F.lvar * F.lty option (* cop out case *) |
187 |
|
|
188 |
fun cexp (cfg as (d,od)) m le = let |
fun sval2lty (Var(_,x)) = x |
189 |
|
| sval2lty (Decon(_,_,(_,_,lty),tycs)) = |
190 |
|
SOME(hd(#2 (LT.ltd_arrow (hd(LT.lt_inst(lty, tycs)))))) |
191 |
|
| sval2lty _ = NONE |
192 |
|
|
193 |
|
fun tycs_eq ([],[]) = true |
194 |
|
| tycs_eq (tyc1::tycs1,tyc2::tycs2) = |
195 |
|
LT.tc_eqv(tyc1,tyc2) andalso tycs_eq(tycs1,tycs2) |
196 |
|
| tycs_eq _ = false |
197 |
|
|
198 |
|
(* cfg: is used for deBruijn renumbering when inlining at different depths |
199 |
|
* ifs (inlined functions): records which functions we're currently inlining |
200 |
|
* in order to detect loops |
201 |
|
* m: is a map lvars to their defining expressions (svals) *) |
202 |
|
fun cexp (cfg as (d,od)) ifs m le = let |
203 |
|
|
204 |
val loop = cexp cfg |
val loop = cexp cfg ifs |
205 |
|
|
206 |
fun used lv = C.usenb lv > 0 |
fun used lv = C.usenb lv > 0 |
207 |
|
|
223 |
|
|
224 |
fun sval2val sv = |
fun sval2val sv = |
225 |
case sv |
case sv |
226 |
of (Fun{1=lv,...} | TFun{1=lv,...} | Record{1=lv,...} |
of (Fun{1=lv,...} | TFun{1=lv,...} | Record{1=lv,...} | Decon{1=lv,...} |
227 |
| Con{1=lv,...} | Select{1=lv,...} | Var{1=lv,...}) => F.VAR lv |
| Con{1=lv,...} | Select{1=lv,...} | Var{1=lv,...}) => F.VAR lv |
228 |
| Val v => v |
| Val v => v |
229 |
|
|
250 |
of Var {1=nlv,...} => ASSERT(nlv = lv, "nlv = lv") |
of Var {1=nlv,...} => ASSERT(nlv = lv, "nlv = lv") |
251 |
| Val v => () |
| Val v => () |
252 |
| Fun (lv,le,args,_,_) => |
| Fun (lv,le,args,_,_) => |
253 |
C.unusefdec undertake (lv, map #1 args, le) |
(#2 (C.unuselexp undertake)) (lv, map #1 args, le) |
254 |
| TFun{1=lv,2=le,...} => C.unusefdec undertake (lv, [], le) |
| TFun{1=lv,2=le,...} => (#2 (C.unuselexp undertake)) (lv, [], le) |
255 |
| (Select {2=v,...} | Con {2=v,...}) => unuseval undertake v |
| (Select {2=v,...} | Con {2=v,...}) => unuseval undertake v |
256 |
| Record {2=vs,...} => app (unuseval undertake) vs |
| Record {2=vs,...} => app (unuseval undertake) vs |
257 |
|
(* decon's are implicit so we can't get rid of them *) |
258 |
|
| Decon _ => () |
259 |
end |
end |
260 |
handle M.IntmapF => |
handle M.IntmapF => |
261 |
(say "\nUnable to undertake "; PP.printSval(F.VAR lv)) |
(say "\nUnable to undertake "; PP.printSval(F.VAR lv)) |
289 |
(s, Access.EXN(Access.LVAR(substvar lv)), lty) |
(s, Access.EXN(Access.LVAR(substvar lv)), lty) |
290 |
| cdcon dc = dc |
| cdcon dc = dc |
291 |
|
|
292 |
(* F.APP inlining (if any) *) |
(* F.APP inlining (if any) |
293 |
fun inline (f,vs) = |
* `ifs' is the set of function we are currently inlining |
294 |
|
* `f' is the function, `vs' its arguments. |
295 |
|
* return either (NONE, ifs) if inlining cannot be done or |
296 |
|
* (SOME lexp, nifs) where `lexp' is the expansion of APP(f,vs) and |
297 |
|
* `nifs' is the new set of functions we are currently inlining. |
298 |
|
*) |
299 |
|
fun inline ifs (f,vs) = |
300 |
case ((val2sval m f) handle x => raise x) |
case ((val2sval m f) handle x => raise x) |
301 |
of Fun(g,body,args,F.FK_FUN{isrec,inline,...},od) => |
of Fun(g,body,args,F.FK_FUN{isrec,inline,...},od) => |
302 |
(ASSERT(C.usenb g > 0, "C.usenb g > 0"); |
(ASSERT(C.usenb g > 0, "C.usenb g > 0"); |
308 |
* looks inoffensive enough, but still requires some care: |
* looks inoffensive enough, but still requires some care: |
309 |
* see comments at the begining of this file and in cfun *) |
* see comments at the begining of this file and in cfun *) |
310 |
then (C.unuse (fn _ => ()) true g; ASSERT(not (used g), "killed"); |
then (C.unuse (fn _ => ()) true g; ASSERT(not (used g), "killed"); |
311 |
SOME(F.LET(map #1 args, F.RET vs, body), od)) |
(SOME(F.LET(map #1 args, F.RET vs, body), od), ifs)) |
312 |
|
|
313 |
(* aggressive inlining (but hopefully safe). We allow |
(* aggressive inlining (but hopefully safe). We allow |
314 |
* inlining for mutually recursive functions (isrec) |
* inlining for mutually recursive functions (isrec) |
317 |
* mutually recursive with its main function. On another hand, |
* mutually recursive with its main function. On another hand, |
318 |
* self recursion (C.recursive) is too dangerous to be inlined |
* self recursion (C.recursive) is too dangerous to be inlined |
319 |
* except for loop unrolling which we don't support yet *) |
* except for loop unrolling which we don't support yet *) |
320 |
else if inline andalso od = d andalso not(C.recursive g) then |
else if inline andalso od = d andalso not(S.member ifs g) then |
321 |
let val nle = copy M.empty (F.LET(map #1 args, F.RET vs, body)) |
let val nle = FU.copy M.empty (F.LET(map #1 args, F.RET vs, body)) |
322 |
|
val _ = if C.recursive g then |
323 |
|
(say "\n inlining recursive function "; |
324 |
|
PP.printSval (F.VAR g)) else () |
325 |
in C.uselexp nle; |
in C.uselexp nle; |
326 |
app (unuseval (undertake m)) vs; |
app (unuseval (undertake m)) vs; |
327 |
C.unuse (undertake m) true g; |
C.unuse (undertake m) true g; |
328 |
SOME(nle, od) |
(SOME(nle, od), S.add(g, ifs)) |
329 |
end |
end |
330 |
|
|
331 |
else NONE) |
else (NONE, ifs)) |
332 |
| sv => NONE |
| sv => (NONE, ifs) |
333 |
in |
in |
334 |
case le |
case le |
335 |
of F.RET vs => F.RET((map substval vs) handle x => raise x) |
of F.RET vs => F.RET((map substval vs) handle x => raise x) |
371 |
known le1 andalso known le2 then |
known le1 andalso known le2 then |
372 |
(* here I should also check that le1 != le2 *) |
(* here I should also check that le1 != le2 *) |
373 |
let val nle1 = F.LET([lv], le1, body) |
let val nle1 = F.LET([lv], le1, body) |
374 |
val nlv = LV.mkLvar() |
val nlv = cplv lv |
375 |
val body2 = copy (M.add(M.empty,lv,nlv)) body |
val body2 = FU.copy (M.add(M.empty,lv,nlv)) body |
376 |
val nle2 = F.LET([nlv], le2, body2) |
val nle2 = F.LET([nlv], le2, body2) |
377 |
in C.new false nlv; C.uselexp body2; |
in C.new false nlv; C.uselexp body2; |
378 |
lopm(wrap(F.BRANCH(po, vs, nle1, nle2))) |
lopm(wrap(F.BRANCH(po, vs, nle1, nle2))) |
394 |
in loop (foldl simplesubst m (ListPair.zip(lvs, vs))) body |
in loop (foldl simplesubst m (ListPair.zip(lvs, vs))) body |
395 |
end handle x => raise x) |
end handle x => raise x) |
396 |
| F.APP(f,vs) => |
| F.APP(f,vs) => |
397 |
(case inline(f, vs) |
(case inline ifs (f, vs) |
398 |
of SOME(le,od) => cexp (d,od) m (F.LET(lvs, le, body)) |
of (SOME(le,od),ifs) => cexp (d,od) ifs m (F.LET(lvs, le, body)) |
399 |
| NONE => clet()) |
| (NONE,_) => clet()) |
400 |
| (F.TAPP _ | F.SWITCH _ | F.RAISE _ | F.HANDLE _) => |
| (F.TAPP _ | F.SWITCH _ | F.RAISE _ | F.HANDLE _) => |
401 |
clet() |
clet() |
402 |
end |
end |
514 |
|
|
515 |
| F.APP (f,vs) => |
| F.APP (f,vs) => |
516 |
let val nvs = ((map substval vs) handle x => raise x) |
let val nvs = ((map substval vs) handle x => raise x) |
517 |
in case inline(f, nvs) |
in case inline ifs (f, nvs) |
518 |
of SOME(le,od) => cexp (d,od) m le |
of (SOME(le,od),ifs) => cexp (d,od) ifs m le |
519 |
| NONE => F.APP((substval f) handle x => raise x, nvs) |
| (NONE,_) => F.APP((substval f) handle x => raise x, nvs) |
520 |
end |
end |
521 |
|
|
522 |
| F.TFN ((f,args,body),le) => |
| F.TFN ((f,args,body),le) => |
523 |
if used f then |
if used f then |
524 |
let val nbody = cexp (DI.next d, DI.next od) m body |
let val nbody = cexp (DI.next d, DI.next od) ifs m body |
525 |
val nm = addbind(m, f, TFun(f, nbody, args, od)) |
val nm = addbind(m, f, TFun(f, nbody, args, od)) |
526 |
val nle = loop nm le |
val nle = loop nm le |
527 |
in |
in |
533 |
|
|
534 |
| F.SWITCH (v,ac,arms,def) => |
| F.SWITCH (v,ac,arms,def) => |
535 |
(case ((val2sval m v) handle x => raise x) |
(case ((val2sval m v) handle x => raise x) |
536 |
of sv as (Var{1=lvc,...} | Select{1=lvc,...} | Record{1=lvc,...}) => |
of sv as (Var{1=lvc,...} | Select{1=lvc,...} | Record{1=lvc,...} |
537 |
|
| Decon{1=lvc, ...}) => |
538 |
let fun carm (F.DATAcon(dc,tycs,lv),le) = |
let fun carm (F.DATAcon(dc,tycs,lv),le) = |
539 |
let val ndc = cdcon dc |
let val ndc = cdcon dc |
540 |
(* here I should try to extract the type of lv *) |
(* here I should try to extract the type of lv *) |
541 |
val nm = addbind(m, lv, Var(lv, NONE)) |
val nm = addbind(m, lv, Decon(lv, F.VAR lvc, ndc, tycs)) |
542 |
(* we can rebind lv to a more precise value *) |
(* we can rebind lv to a more precise value *) |
543 |
val nm = addbind(nm, lvc, Con(lvc, F.VAR lv, ndc)) |
val nm = addbind(nm, lvc, Con(lvc, F.VAR lv, ndc, tycs)) |
544 |
in (F.DATAcon(ndc, tycs, lv), loop nm le) |
in (F.DATAcon(ndc, tycs, lv), loop nm le) |
545 |
end |
end |
546 |
| carm (con,le) = (con, loop m le) |
| carm (con,le) = (con, loop m le) |
550 |
F.SWITCH(sval2val sv, ac, narms, ndef) |
F.SWITCH(sval2val sv, ac, narms, ndef) |
551 |
end |
end |
552 |
|
|
553 |
| Con (lvc,v,(_,conrep,_)) => |
| Con (lvc,v,dc1,tycs1) => |
554 |
let fun carm ((F.DATAcon((_,crep,_),tycs,lv),le)::tl) = |
let fun killle le = (#1 (C.unuselexp (undertake m))) le |
555 |
if crep = conrep then |
fun kill lv le = |
556 |
loop (substitute(m, lv, (val2sval m v) handle x => raise x, F.VAR lvc)) le |
(#1 (C.unuselexp (undertake (addbind(m,lv,Var(lv,NONE)))))) le |
557 |
else carm tl |
fun killarm (F.DATAcon(_,_,lv),le) = kill lv le |
558 |
|
| killarm _ = buglexp("bad arm in switch(con)", le) |
559 |
|
|
560 |
|
fun carm ((F.DATAcon(dc2,tycs2,lv),le)::tl) = |
561 |
|
if FU.dcon_eq(dc1, dc2) andalso tycs_eq(tycs1,tycs2) then |
562 |
|
(map killarm tl; (* kill the rest *) |
563 |
|
Option.map killle def; (* and the default case *) |
564 |
|
loop (substitute(m, lv, val2sval m v, F.VAR lvc)) le) |
565 |
|
else |
566 |
|
(* kill this arm and continue with the rest *) |
567 |
|
(kill lv le; carm tl) |
568 |
| carm [] = loop m (Option.valOf def) |
| carm [] = loop m (Option.valOf def) |
569 |
| carm _ = buglexp("unexpected arm in switch(con,...)", le) |
| carm _ = buglexp("unexpected arm in switch(con,...)", le) |
570 |
in carm arms |
in carm arms |
571 |
end |
end |
572 |
|
|
573 |
| Val v => |
| Val v => |
574 |
let fun carm ((con,le)::tl) = |
let fun kill le = (#1 (C.unuselexp (undertake m))) le |
575 |
if eqConV(con, v) then loop m le else carm tl |
fun carm ((con,le)::tl) = |
576 |
|
if eqConV(con, v) then |
577 |
|
(map (kill o #2) tl; Option.map kill def; loop m le) |
578 |
|
else (kill le; carm tl) |
579 |
| carm [] = loop m (Option.valOf def) |
| carm [] = loop m (Option.valOf def) |
580 |
in carm arms |
in carm arms |
581 |
end |
end |
582 |
| sv as (Fun _ | TFun _) => |
| sv as (Fun _ | TFun _) => |
583 |
bugval("unexpected switch arg", sval2val sv)) |
bugval("unexpected switch arg", sval2val sv)) |
584 |
|
|
585 |
| F.CON (dc,tycs,v,lv,le) => |
| F.CON (dc1,tycs1,v,lv,le) => |
586 |
|
(* Here we should try to nullify CON(DECON x) => x *) |
587 |
if used lv then |
if used lv then |
588 |
let val ndc = cdcon dc |
let val ndc = cdcon dc1 |
589 |
val nv = ((substval v) handle x => raise x) |
fun ccon sv = |
590 |
val nm = addbind(m, lv, Con(lv, nv, ndc)) |
let val nv = sval2val sv |
591 |
|
val nm = addbind(m, lv, Con(lv, nv, ndc, tycs1)) |
592 |
val nle = loop nm le |
val nle = loop nm le |
593 |
in if used lv then F.CON(ndc, tycs, nv, lv, nle) else nle |
in if used lv then F.CON(ndc, tycs1, nv, lv, nle) else nle |
594 |
|
end |
595 |
|
in case ((val2sval m v) handle x => raise x) |
596 |
|
of sv as (Decon (lvd,vc,dc2,tycs2)) => |
597 |
|
if FU.dcon_eq(dc1, dc2) andalso tycs_eq(tycs1,tycs2) then |
598 |
|
let val sv = (val2sval m vc) handle x => raise x |
599 |
|
in loop (substitute(m, lv, sv, F.VAR lvd)) le |
600 |
|
end |
601 |
|
else ccon sv |
602 |
|
| sv => ccon sv |
603 |
end |
end |
604 |
else loop m le |
else loop m le |
605 |
|
|
607 |
(* Here I could try to see if I'm reconstructing a preexisting record. |
(* Here I could try to see if I'm reconstructing a preexisting record. |
608 |
* The `lty option' of Var is there just for that purpose *) |
* The `lty option' of Var is there just for that purpose *) |
609 |
if used lv then |
if used lv then |
610 |
let val nvs = ((map substval vs) handle x => raise x) |
(* g: check whether the record already exists *) |
611 |
|
let fun g (n,Select(_,v1,i)::ss) = |
612 |
|
if n = i then |
613 |
|
(case ss |
614 |
|
of Select(_,v2,_)::_ => |
615 |
|
if v1 = v2 then g(n+1, ss) else NONE |
616 |
|
| [] => |
617 |
|
(case sval2lty (val2sval m v1) |
618 |
|
of SOME lty => |
619 |
|
let val ltd = case rk |
620 |
|
of F.RK_STRUCT => LT.ltd_str |
621 |
|
| F.RK_TUPLE _ => LT.ltd_tuple |
622 |
|
| _ => buglexp("bogus rk",le) |
623 |
|
in if length(ltd lty) = n+1 |
624 |
|
then SOME v1 else NONE |
625 |
|
end |
626 |
|
| _ => NONE) (* sad case *) |
627 |
|
| _ => NONE) |
628 |
|
else NONE |
629 |
|
| g _ = NONE |
630 |
|
val svs = ((map (val2sval m) vs) handle x => raise x) |
631 |
|
in case g (0,svs) |
632 |
|
of SOME v => |
633 |
|
let val sv = (val2sval m v) handle x => raise x |
634 |
|
in loop (substitute(m, lv, sv, F.INT 0)) le |
635 |
|
before app (unuseval (undertake m)) vs |
636 |
|
end |
637 |
|
| _ => |
638 |
|
let val nvs = map sval2val svs |
639 |
val nm = addbind(m, lv, Record(lv, nvs)) |
val nm = addbind(m, lv, Record(lv, nvs)) |
640 |
val nle = loop nm le |
val nle = loop nm le |
641 |
in if used lv then F.RECORD(rk, nvs, lv, nle) else nle |
in if used lv then F.RECORD(rk, nvs, lv, nle) else nle |
642 |
end |
end |
643 |
|
end |
644 |
else loop m le |
else loop m le |
645 |
|
|
646 |
| F.SELECT (v,i,lv,le) => |
| F.SELECT (v,i,lv,le) => |
688 |
|
|
689 |
fun contract (fdec as (_,f,_,_)) = |
fun contract (fdec as (_,f,_,_)) = |
690 |
(C.collect fdec; |
(C.collect fdec; |
691 |
case cexp (DI.top,DI.top) M.empty (F.FIX([fdec], F.RET[F.VAR f])) |
case cexp (DI.top,DI.top) S.empty M.empty (F.FIX([fdec], F.RET[F.VAR f])) |
692 |
of F.FIX([fdec], F.RET[F.VAR f]) => fdec |
of F.FIX([fdec], F.RET[F.VAR f]) => fdec |
693 |
| fdec => bug "invalid return fundec") |
| fdec => bug "invalid return fundec") |
694 |
|
|