summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--dhall_core/src/core.rs30
1 files changed, 13 insertions, 17 deletions
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index 2f15217..a9033f3 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -716,36 +716,32 @@ pub fn shift<S, A>(
}
}
-/// Substitute all occurrences of a variable with an expression
+/// Substitute all occurrences of a variable with an expression, and
+/// removes the variable from the environment by shifting the indices
+/// of other variables appropriately.
///
/// ```c
-/// subst x C B ~ B[x := C]
+/// subst_shift(x, v, e) ~ ↑(-1, x, e[x := ↑(1, x, v)])
/// ```
///
-pub fn subst<S, A>(
+pub fn subst_shift<S, A>(
var: &V<Label>,
value: &SubExpr<S, A>,
in_expr: &SubExpr<S, A>,
) -> SubExpr<S, A> {
use crate::ExprF::*;
+ let V(x, n) = var;
let under_binder = |y: &Label, e: &SubExpr<_, _>| {
- let V(x, n) = var;
let n = if x == y { n + 1 } else { *n };
let newvar = &V(x.clone(), n);
- subst(newvar, &shift(1, &V(y.clone(), 0), value), e)
+ subst_shift(newvar, &shift(1, &V(y.clone(), 0), value), e)
};
match in_expr.as_ref() {
- Var(v) if var == v => SubExpr::clone(value),
- _ => in_expr.map_ref(|e| subst(var, value, e), under_binder),
+ Var(V(y, m)) if x == y && m == n => SubExpr::clone(value),
+ Var(V(y, m)) if x == y && m > n => {
+ let m = add_ui(*m, -1);
+ rc(Var(V(x.clone(), m)))
+ }
+ _ => in_expr.map_ref(|e| subst_shift(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)
-}