aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/unnest.sml
diff options
context:
space:
mode:
Diffstat (limited to 'src/unnest.sml')
-rw-r--r--src/unnest.sml20
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)]*)