diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-11-11 16:27:51 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-11-11 16:27:51 -0500 |
| commit | 4ec6c9e24ebb58cd62b6f9d69447fae314aac82d (patch) | |
| tree | dfc7ea6b8feefe15f51e0581c1556cbf85763c2d /src/unnest.sml | |
| parent | cb961c521e9aee367e2d8f3ede63bcf191c53f05 (diff) | |
More ThreadedBlog progress
Diffstat (limited to 'src/unnest.sml')
| -rw-r--r-- | src/unnest.sml | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/unnest.sml b/src/unnest.sml index fe63f9fe..8e363301 100644 --- a/src/unnest.sml +++ b/src/unnest.sml @@ -206,6 +206,14 @@ fun exp ((ks, ts), e as old, st : state) = 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 @@ fun exp ((ks, ts), e as old, st : state) = 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 @@ fun exp ((ks, ts), e as old, st : state) = 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)]*) |