22 |
* free variables remain unchanged except for the renaming specified |
* free variables remain unchanged except for the renaming specified |
23 |
* in the first (types) and second (values) argument *) |
* in the first (types) and second (values) argument *) |
24 |
val copy : (FLINT.tvar * FLINT.tyc) list -> |
val copy : (FLINT.tvar * FLINT.tyc) list -> |
25 |
FLINT.lvar IntmapF.intmap -> |
FLINT.lvar IntBinaryMap.map -> |
26 |
FLINT.lexp -> FLINT.lexp |
FLINT.lexp -> FLINT.lexp |
27 |
val copyfdec : FLINT.fundec -> FLINT.fundec |
val copyfdec : FLINT.fundec -> FLINT.fundec |
28 |
|
|
29 |
val freevars : FLINT.lexp -> IntSetF.intset |
val freevars : FLINT.lexp -> IntBinarySet.set |
30 |
|
|
31 |
val dcon_eq : FLINT.dcon * FLINT.dcon -> bool |
val dcon_eq : FLINT.dcon * FLINT.dcon -> bool |
32 |
|
|
40 |
structure LT = LtyExtern |
structure LT = LtyExtern |
41 |
structure PO = PrimOp |
structure PO = PrimOp |
42 |
structure DA = Access |
structure DA = Access |
43 |
structure M = IntmapF |
structure M = IntBinaryMap |
44 |
structure A = Access |
structure A = Access |
45 |
structure O = Option |
structure O = Option |
46 |
structure S = IntSetF |
structure S = IntBinarySet |
47 |
structure F = FLINT |
structure F = FLINT |
48 |
open FLINT |
open FLINT |
49 |
in |
in |
103 |
val tc_subst = LT.tc_nvar_subst_gen() |
val tc_subst = LT.tc_nvar_subst_gen() |
104 |
val lt_subst = LT.lt_nvar_subst_gen() |
val lt_subst = LT.lt_nvar_subst_gen() |
105 |
|
|
106 |
val tmap_sort = Sort.sort (fn ((v1,_),(v2,_)) => v1 > v2) |
val tmap_sort = ListMergeSort.sort (fn ((v1,_),(v2,_)) => v1 > v2) |
107 |
|
|
108 |
fun substvar alpha lv = ((M.lookup alpha lv) handle M.IntmapF => lv) |
fun substvar alpha lv = case M.find(alpha,lv) of SOME(lv) => lv | NOE => lv |
109 |
fun substval alpha (VAR lv) = VAR(substvar alpha lv) |
fun substval alpha (VAR lv) = VAR(substvar alpha lv) |
110 |
| substval alpha v = v |
| substval alpha v = v |
111 |
fun newv (lv,alpha) = |
fun newv (lv,alpha) = |
112 |
let val nlv = cplv lv in (nlv, M.add(alpha,lv,nlv)) end |
let val nlv = cplv lv in (nlv, M.insert(alpha,lv,nlv)) end |
113 |
fun newvs (lvs,alpha) = |
fun newvs (lvs,alpha) = |
114 |
foldr (fn (lv,(lvs,alpha)) => |
foldr (fn (lv,(lvs,alpha)) => |
115 |
let val (nlv,nalpha) = newv(lv,alpha) in (nlv::lvs,nalpha) end) |
let val (nlv,nalpha) = newv(lv,alpha) in (nlv::lvs,nalpha) end) |
214 |
fun freevars lexp = let |
fun freevars lexp = let |
215 |
val loop = freevars |
val loop = freevars |
216 |
|
|
217 |
fun addv (s,F.VAR lv) = S.add(lv, s) |
fun addv (s,F.VAR lv) = S.add(s, lv) |
218 |
| addv (s,_) = s |
| addv (s,_) = s |
219 |
fun addvs (s,vs) = foldl (fn (v,s) => addv(s, v)) s vs |
fun addvs (s,vs) = foldl (fn (v,s) => addv(s, v)) s vs |
220 |
fun rmvs (s,lvs) = foldl S.rmv s lvs |
fun rmvs (s,lvs) = foldl (fn (l,s) => S.delete (s, l)) s lvs |
221 |
fun singleton (F.VAR v) = S.singleton v |
fun singleton (F.VAR v) = S.singleton v |
222 |
| singleton _ = S.empty |
| singleton _ = S.empty |
223 |
|
|
237 |
(loop le) fdecs), |
(loop le) fdecs), |
238 |
map #2 fdecs) |
map #2 fdecs) |
239 |
| F.APP (f,args) => addvs(S.empty, f::args) |
| F.APP (f,args) => addvs(S.empty, f::args) |
240 |
| F.TFN ((tfk,f,args,body),le) => S.union(S.rmv(f, loop le), loop body) |
| F.TFN ((tfk,f,args,body),le) => S.union(S.delete(loop le, f), loop body) |
241 |
| F.TAPP (f,args) => singleton f |
| F.TAPP (f,args) => singleton f |
242 |
| F.SWITCH (v,ac,arms,def) => |
| F.SWITCH (v,ac,arms,def) => |
243 |
let fun farm ((dc,le),fv) = |
let fun farm ((dc,le),fv) = |
244 |
let val fvle = loop le |
let val fvle = loop le |
245 |
in S.union(fv, |
in S.union(fv, |
246 |
case dc |
case dc |
247 |
of F.DATAcon(dc,_,lv) => fdcon(S.rmv(lv, fvle),dc) |
of F.DATAcon(dc,_,lv) => fdcon(S.delete(fvle, lv),dc) |
248 |
| _ => fvle) |
| _ => fvle) |
249 |
end |
end |
250 |
val fvs = case def of NONE => singleton v |
val fvs = case def of NONE => singleton v |
251 |
| SOME le => addv(loop le, v) |
| SOME le => addv(loop le, v) |
252 |
in foldl farm fvs arms |
in foldl farm fvs arms |
253 |
end |
end |
254 |
| F.CON (dc,tycs,v,lv,le) => fdcon(addv(S.rmv(lv, loop le), v),dc) |
| F.CON (dc,tycs,v,lv,le) => fdcon(addv(S.delete(loop le, lv), v),dc) |
255 |
| F.RECORD (rk,vs,lv,le) => addvs(S.rmv(lv, loop le), vs) |
| F.RECORD (rk,vs,lv,le) => addvs(S.delete(loop le, lv), vs) |
256 |
| F.SELECT (v,i,lv,le) => addv(S.rmv(lv, loop le), v) |
| F.SELECT (v,i,lv,le) => addv(S.delete(loop le, lv), v) |
257 |
| F.RAISE (v,ltys) => singleton v |
| F.RAISE (v,ltys) => singleton v |
258 |
| F.HANDLE (le,v) => addv(loop le, v) |
| F.HANDLE (le,v) => addv(loop le, v) |
259 |
| F.BRANCH (po,vs,le1,le2) => fpo(addvs(S.union(loop le1, loop le2), vs), po) |
| F.BRANCH (po,vs,le1,le2) => fpo(addvs(S.union(loop le1, loop le2), vs), po) |
260 |
| F.PRIMOP (po,vs,lv,le) => fpo(addvs(S.rmv(lv, loop le), vs),po) |
| F.PRIMOP (po,vs,lv,le) => fpo(addvs(S.delete(loop le, lv), vs),po) |
261 |
end |
end |
262 |
|
|
263 |
end (* top-level local *) |
end (* top-level local *) |