diff options
| -rw-r--r-- | dhall/src/normalize.rs | 13 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 5 | ||||
| -rw-r--r-- | dhall_core/src/core.rs | 10 |
3 files changed, 14 insertions, 14 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 7574c2f..24a8601 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -217,13 +217,8 @@ where let what_next = match &expr { Let(f, _, r, b) => { let vf0 = &V(f.clone(), 0); - let r2 = shift(1, vf0, &r.roll()); // TODO: use a context - let b2 = subst(vf0, &r2, &b.roll()); - // TODO: add tests sensitive to shift errors before - // trying anything - let b3 = shift(-1, vf0, &b2); - ContinueSub(b3) + ContinueSub(subst_shift(vf0, &r.roll(), &b.roll())) } Annot(x, _) => DoneRef(x), Note(_, e) => DoneRef(e), @@ -243,10 +238,8 @@ where let a = iter.next().unwrap(); // Beta reduce let vx0 = &V(x.clone(), 0); - let a2 = shift(1, vx0, &a.roll()); - let b2 = subst(vx0, &a2, &b); - let b3 = shift(-1, vx0, &b2); - Continue(App(b3, iter.map(ExprF::roll).collect())) + let b2 = subst_shift(vx0, &a.roll(), &b); + Continue(App(b2, iter.map(ExprF::roll).collect())) } BoolIf(BoolLit(true), t, _) => DoneRef(t), BoolIf(BoolLit(false), _, f) => DoneRef(f), diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 75e6e1d..145de63 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -268,10 +268,7 @@ where let tA2 = normalized_type_with(ctx, a.clone())?; if prop_equal(tA.as_ref(), tA2.as_ref()) { let vx0 = &V(x.clone(), 0); - let a2 = shift(1, vx0, a); - let tB2 = subst(vx0, &a2, &tB); - let tB3 = shift(-1, vx0, &tB2); - return Ok(tB3); + return Ok(subst_shift(vx0, &a, &tB)); } else { Err(mkerr(TypeMismatch(f.clone(), tA, a.clone(), tA2))) } diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index 3d1b9f3..2f15217 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -739,3 +739,13 @@ pub fn subst<S, A>( _ => in_expr.map_ref(|e| subst(var, value, e), under_binder), } } + +pub fn subst_shift<S, A>( + var: &V<Label>, + value: &SubExpr<S, A>, + in_expr: &SubExpr<S, A>, +) -> SubExpr<S, A> { + let value = shift(1, var, value); + let expr = subst(var, &value, in_expr); + shift(-1, var, &expr) +} |