Mercurial > urweb
diff src/unnest.sml @ 490:366676f7bc88
More ThreadedBlog progress
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 11 Nov 2008 16:27:51 -0500 |
| parents | 33d5bd69da00 |
| children | 588b9d16b00a |
line wrap: on
line diff
--- a/src/unnest.sml Tue Nov 11 15:32:10 2008 -0500 +++ b/src/unnest.sml Tue Nov 11 16:27:51 2008 -0500 @@ -206,6 +206,14 @@ val loc = #2 ed val nr = length vis + val subsLocal = List.filter (fn (_, (ERel _, _)) => false + | _ => true) subs + val subsLocal = map (fn (n, e) => (n + nr, liftExpInExp nr 0 e)) + subsLocal + + val vis = map (fn (x, t, e) => + (x, t, doSubst' (e, subsLocal))) vis + val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) => let val (cfv', efv') = fvsExp nr e @@ -243,15 +251,12 @@ maxName + 1)) maxName vis - - val subs = map (fn (n, e) => (n + nr, case e of (ERel _, _) => e | _ => liftExpInExp nr 0 e)) subs - val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) => let val e = (ENamed n, loc) @@ -278,7 +283,7 @@ let (*val () = Print.prefaces "preSubst" [("e", ElabPrint.p_exp E.empty e)]*) - val e = doSubst' (e, subs) + val e = doSubst' (e, subs') (*val () = Print.prefaces "squishCon" [("t", ElabPrint.p_con E.empty t)]*)