From 3881d36335fca6d72b0dd447130d6c1ce7ccbfee Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 17 Jan 2020 18:19:33 +0000
Subject: Implement bulk shifting

---
 dhall/src/semantics/core/var.rs | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

(limited to 'dhall/src/semantics/core/var.rs')

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
     }
 }
 
-- 
cgit v1.2.3