Mercurial > urweb

comparison src/unnest.sml @ 490:366676f7bc88

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More ThreadedBlog progress
author Adam Chlipala <adamc@hcoop.net>
date Tue, 11 Nov 2008 16:27:51 -0500
parents 33d5bd69da00
children 588b9d16b00a
comparison
equal deleted inserted replaced
489:463dad880470 490:366676f7bc88
204 | EDValRec vis => 204 | EDValRec vis =>
205 let 205 let
206 val loc = #2 ed 206 val loc = #2 ed
207 207
208 val nr = length vis 208 val nr = length vis
209 val subsLocal = List.filter (fn (_, (ERel _, _)) => false
210 | _ => true) subs
211 val subsLocal = map (fn (n, e) => (n + nr, liftExpInExp nr 0 e))
212 subsLocal
213
214 val vis = map (fn (x, t, e) =>
215 (x, t, doSubst' (e, subsLocal))) vis
216
209 val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) => 217 val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) =>
210 let 218 let
211 val (cfv', efv') = fvsExp nr e 219 val (cfv', efv') = fvsExp nr e
212 (*val () = Print.prefaces "fvsExp" 220 (*val () = Print.prefaces "fvsExp"
213 [("e", ElabPrint.p_exp E.empty e), 221 [("e", ElabPrint.p_exp E.empty e),
241 ListUtil.foldlMap (fn ((x, t, e), maxName) => 249 ListUtil.foldlMap (fn ((x, t, e), maxName) =>
242 ((x, maxName, t, e), 250 ((x, maxName, t, e),
243 maxName + 1)) 251 maxName + 1))
244 maxName vis 252 maxName vis
245 253
246
247
248 val subs = map (fn (n, e) => (n + nr, 254 val subs = map (fn (n, e) => (n + nr,
249 case e of 255 case e of
250 (ERel _, _) => e 256 (ERel _, _) => e
251 | _ => liftExpInExp nr 0 e)) 257 | _ => liftExpInExp nr 0 e))
252 subs 258 subs
253
254 259
255 val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) => 260 val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) =>
256 let 261 let
257 val e = (ENamed n, loc) 262 val e = (ENamed n, loc)
258 263
276 281
277 val vis = map (fn (x, n, t, e) => 282 val vis = map (fn (x, n, t, e) =>
278 let 283 let
279 (*val () = Print.prefaces "preSubst" 284 (*val () = Print.prefaces "preSubst"
280 [("e", ElabPrint.p_exp E.empty e)]*) 285 [("e", ElabPrint.p_exp E.empty e)]*)
281 val e = doSubst' (e, subs) 286 val e = doSubst' (e, subs')
282 287
283 (*val () = Print.prefaces "squishCon" 288 (*val () = Print.prefaces "squishCon"
284 [("t", ElabPrint.p_con E.empty t)]*) 289 [("t", ElabPrint.p_con E.empty t)]*)
285 val t = squishCon cfv t 290 val t = squishCon cfv t
286 (*val () = Print.prefaces "squishExp" 291 (*val () = Print.prefaces "squishExp"