summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/core/var.rs
diff options
context:
space:
mode:
authorNadrieril2020-01-17 18:19:33 +0000
committerNadrieril2020-01-17 18:19:33 +0000
commit3881d36335fca6d72b0dd447130d6c1ce7ccbfee (patch)
tree13cfafcf28866b4ac6c79cb4d4acfae1d6c941e2 /dhall/src/semantics/core/var.rs
parent37acac4b972b38e8dbe2d174dae1031e5a8eda67 (diff)
Implement bulk shifting
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/var.rs16
1 files changed, 7 insertions, 9 deletions
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 7c2c4de..d7666e3 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -40,19 +40,17 @@ impl AlphaVar {
// Can't fail since delta is positive
self.shift(1, &x.into()).unwrap()
}
+ pub(crate) fn over_binder(&self, x: &AlphaVar) -> Option<Self> {
+ self.shift(-1, x)
+ }
pub(crate) fn under_multiple_binders(
&self,
shift_map: &HashMap<Label, usize>,
- ) -> Self
- where
- Self: Clone,
- {
- let mut v = self.clone();
- for (x, n) in shift_map {
- // Can't fail since delta is positive
- v = v.shift(*n as isize, &x.into()).unwrap();
+ ) -> Self {
+ AlphaVar {
+ normal: self.normal.under_multiple_binders(shift_map),
+ alpha: self.alpha.under_multiple_binders(shift_map),
}
- v
}
}