Implement bulk shifting

1 files changed, 29 insertions, 4 deletions

diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 04b5adc..2372b0a 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -1,3 +1,5 @@
+use std::collections::HashMap;
+
 use crate::syntax::map::{DupTreeMap, DupTreeSet};
 use crate::syntax::visitor::{self, ExprKindMutVisitor, ExprKindVisitor};
 use crate::syntax::*;
@@ -302,7 +304,7 @@ impl<E> Expr<E> {
 }
 
 impl<Label: PartialEq + Clone> V<Label> {
-    pub fn shift(&self, delta: isize, var: &V<Label>) -> Option<Self> {
+    pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Option<Self> {
         let V(x, n) = var;
         let V(y, m) = self;
         Some(if x == y && n <= m {
@@ -312,11 +314,35 @@ impl<Label: PartialEq + Clone> V<Label> {
         })
     }
 
-    pub fn over_binder(&self, x: &Label) -> Option<Self> {
+    pub(crate) fn over_binder(&self, x: &Label) -> Option<Self> {
         self.shift(-1, &V(x.clone(), 0))
     }
 }
 
+impl V<Label> {
+    pub(crate) fn under_multiple_binders(
+        &self,
+        shift_map: &HashMap<Label, usize>,
+    ) -> Self {
+        let name = &self.0;
+        let idx = self.1 + shift_map.get(name).unwrap_or(&0);
+        V(name.clone(), idx)
+    }
+}
+
+impl V<()> {
+    pub(crate) fn under_multiple_binders(
+        &self,
+        shift_map: &HashMap<Label, usize>,
+    ) -> Self {
+        let mut idx = self.1;
+        for (_, n) in shift_map {
+            idx += n;
+        }
+        V((), idx)
+    }
+}
+
 pub fn trivial_result<T>(x: Result<T, !>) -> T {
     match x {
         Ok(x) => x,
@@ -363,8 +389,7 @@ impl From<NaiveDouble> for f64 {
     }
 }
 
-/// This is only for the specific `Label` type, not generic
-impl From<Label> for V<Label> {
+impl<Label> From<Label> for V<Label> {
     fn from(x: Label) -> V<Label> {
         V(x, 0)
     }