summaryrefslogtreecommitdiff
path: root/dhall_core/src
diff options
context:
space:
mode:
authorNadrieril2019-04-21 22:52:00 +0200
committerNadrieril2019-04-21 22:52:00 +0200
commitecff0ecd47bb38937fb43e60b8d78ea92e2af01c (patch)
tree00851982d545e10a3bac297b30726603e4f95948 /dhall_core/src
parent20f01b79378a41c6e063d33c584d04c756419a26 (diff)
Prepare for interop between two contexts
Diffstat (limited to 'dhall_core/src')
-rw-r--r--dhall_core/src/core.rs34
1 files changed, 21 insertions, 13 deletions
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index fa6fca4..03974eb 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -468,15 +468,24 @@ fn add_ui(u: usize, i: isize) -> usize {
}
}
-/// Applies `shift` to a single var.
-/// The first var is the var to shift away from; the second is the variable to shift
-fn shift_var(delta: isize, var: &V<Label>, in_expr: &V<Label>) -> V<Label> {
- let V(x, n) = var;
- let V(y, m) = in_expr;
- if x == y && n <= m {
- V(y.clone(), add_ui(*m, delta))
- } else {
- V(y.clone(), *m)
+impl<Label: PartialEq + Clone> V<Label> {
+ pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ let V(x, n) = var;
+ let V(y, m) = self;
+ if x == y && n <= m {
+ V(y.clone(), add_ui(*m, delta))
+ } else {
+ V(y.clone(), *m)
+ }
+ }
+
+ pub fn shift0(&self, delta: isize, x: &Label) -> Self {
+ let V(y, m) = self;
+ if x == y {
+ V(y.clone(), add_ui(*m, delta))
+ } else {
+ V(y.clone(), *m)
+ }
}
}
@@ -492,12 +501,11 @@ pub fn shift<N, E>(
) -> SubExpr<N, E> {
use crate::ExprF::*;
match in_expr.as_ref() {
- Var(v) => rc(Var(shift_var(delta, var, v))),
+ Var(v) => rc(Var(v.shift(delta, var))),
_ => in_expr.map_subexprs_with_special_handling_of_binders(
|e| shift(delta, var, e),
|l: &Label, e| {
- let vl = V(l.clone(), 0);
- let newvar = shift_var(1, &vl, var);
+ let newvar = var.shift0(1, l);
shift(delta, &newvar, e)
},
),
@@ -567,7 +575,7 @@ fn subst_shift_inner<N, E>(
let actual_var = V(x.clone(), add_ui(*n, *dn));
match in_expr.as_ref() {
Var(v) if v == &actual_var => shift0_multiple(ctx, value),
- Var(v) => rc(Var(shift_var(-1, &actual_var, v))),
+ Var(v) => rc(Var(v.shift(-1, &actual_var))),
_ => in_expr.map_subexprs_with_special_handling_of_binders(
|e| subst_shift_inner(ctx, var, value, e),
|l: &Label, e| {