summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-04-06 11:09:23 +0200
committerNadrieril2019-04-06 11:09:23 +0200
commit0cf4d3845e75ac25e35c5e73eb2dfd58c5450af6 (patch)
tree4cf5119a66fc7baeb66cb44a171d5a290429da18
parent5b0e81c215fa6323635ca1bf49a86aeef0ba80f8 (diff)
Factor out shift/subst/shift dance
-rw-r--r--dhall/src/normalize.rs13
-rw-r--r--dhall/src/typecheck.rs5
-rw-r--r--dhall_core/src/core.rs10
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)
+}