summaryrefslogtreecommitdiff
path: root/dhall_core/src
diff options
context:
space:
mode:
authorNadrieril2019-04-29 16:27:14 +0200
committerNadrieril2019-04-29 16:27:14 +0200
commit5c16a75c6dc01bbd0bfe36be4a9b337a762632a8 (patch)
treed294d816754fa0c168b9abb51795dbb371a9a5d9 /dhall_core/src
parenta594e3aa376aa4bfef3456d336630f7520f3c28b (diff)
Properly substitute when typing App
Diffstat (limited to 'dhall_core/src')
-rw-r--r--dhall_core/src/core.rs23
1 files changed, 15 insertions, 8 deletions
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index 72b42f8..a20f6d1 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -433,6 +433,17 @@ impl<N, E> SubExpr<N, E> {
{
rc(self.as_ref().visit(&mut visitor::UnNoteVisitor))
}
+
+ pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self {
+ match self.as_ref() {
+ ExprF::Var(v) if v == var => val.clone(),
+ ExprF::Var(v) => rc(ExprF::Var(v.shift(-1, var))),
+ _ => self.map_subexprs_with_special_handling_of_binders(
+ |e| e.subst_shift(var, val),
+ |x: &Label, e| e.subst_shift(&var.shift0(1, x), val),
+ ),
+ }
+ }
}
impl<N: Clone> SubExpr<N, X> {
@@ -499,15 +510,11 @@ pub fn shift<N, E>(
var: &V<Label>,
in_expr: &SubExpr<N, E>,
) -> SubExpr<N, E> {
- use crate::ExprF::*;
match in_expr.as_ref() {
- Var(v) => rc(Var(v.shift(delta, var))),
+ ExprF::Var(v) => rc(ExprF::Var(v.shift(delta, var))),
_ => in_expr.map_subexprs_with_special_handling_of_binders(
|e| shift(delta, var, e),
- |l: &Label, e| {
- let newvar = var.shift0(1, l);
- shift(delta, &newvar, e)
- },
+ |x: &Label, e| shift(delta, &var.shift0(1, x), e),
),
}
}
@@ -540,8 +547,8 @@ fn shift0_multiple_inner<N, E>(
}
_ => in_expr.map_subexprs_with_special_handling_of_binders(
|e| shift0_multiple_inner(ctx, deltas, e),
- |l: &Label, e| {
- shift0_multiple_inner(&ctx.insert(l.clone(), ()), deltas, e)
+ |x: &Label, e| {
+ shift0_multiple_inner(&ctx.insert(x.clone(), ()), deltas, e)
},
),
}