summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/core/var.rs
diff options
context:
space:
mode:
authorNadrieril2020-01-17 11:26:34 +0000
committerNadrieril2020-01-17 11:26:34 +0000
commit06f619e8b1654e506840d17dc1cbff4f2d9795c3 (patch)
tree52270f8b0bc5a13d694fdf8d21b5ccf8e546325a /dhall/src/semantics/core/var.rs
parent72d1e3c339cf550fa5af9981af6078a813feb80a (diff)
Simplify a bit
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/var.rs16
1 files changed, 16 insertions, 0 deletions
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index a110632..7c2c4de 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -1,3 +1,5 @@
+use std::collections::HashMap;
+
use crate::syntax::{Label, V};
/// Stores a pair of variables: a normal one and one
@@ -38,6 +40,20 @@ impl AlphaVar {
// Can't fail since delta is positive
self.shift(1, &x.into()).unwrap()
}
+ 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();
+ }
+ v
+ }
}
impl Binder {