diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-11-01 16:46:16 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-11-01 16:46:16 -0400 |
| commit | 2e59aaacd591f76ba5d509284b835c8c34a034f5 (patch) | |
| tree | 27d86d6061f3e52708492b82d0cfb82157c098cd /src/unnest.sml | |
| parent | 1145290f6ac5b13fe94772c692caa3cdb55bbf5f (diff) | |
Wrapping works in Blog
Diffstat (limited to 'src/unnest.sml')
| -rw-r--r-- | src/unnest.sml | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/src/unnest.sml b/src/unnest.sml index e5eddc42..b305b467 100644 --- a/src/unnest.sml +++ b/src/unnest.sml @@ -206,29 +206,31 @@ fun exp ((ks, ts), e, st : state) = val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) => let - val e = apply (ENamed n, loc) + val dummy = (EError, ErrorMsg.dummySpan) + + fun repeatLift k = + if k = 0 then + apply (ENamed n, loc) + else + E.liftExpInExp 0 (repeatLift (k - 1)) in - (0, E.liftExpInExp (nr - i - 1) e) + (0, repeatLift i) end) - vis + vis + val subs' = rev subs' val cfv = IS.listItems cfv val efv = IS.listItems efv val efn = length efv - (*val subsInner = subs - @ map (fn (i, e) => - (i + efn, - E.liftExpInExp efn e)) subs'*) - val subs = subs @ subs' val vis = map (fn (x, n, t, e) => let (*val () = Print.prefaces "preSubst" [("e", ElabPrint.p_exp E.empty e)]*) - val e = doSubst e subs(*Inner*) + val e = doSubst e subs (*val () = Print.prefaces "squishCon" [("t", ElabPrint.p_con E.empty t)]*) |