From 0f4a4801ed67826dc82015d39ce8fd05e7950035 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 17 Jan 2020 18:42:13 +0000
Subject: Replace all bulk shifting by a single shift

---
 dhall/src/semantics/core/context.rs | 15 ++++---------
 dhall/src/semantics/core/value.rs   | 45 -------------------------------------
 dhall/src/semantics/core/var.rs     | 20 ++++-------------
 dhall/src/syntax/ast/expr.rs        | 26 ---------------------
 4 files changed, 8 insertions(+), 98 deletions(-)

(limited to 'dhall')

diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index f8d6ff0..47d2d2d 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -1,5 +1,3 @@
-use std::collections::HashMap;
-
 use crate::error::TypeError;
 use crate::semantics::core::value::Value;
 use crate::semantics::core::value::ValueKind;
@@ -40,7 +38,7 @@ impl TyCtx {
     }
     pub fn lookup(&self, var: &V<Label>) -> Option<Value> {
         let mut var = var.clone();
-        let mut shift_map: HashMap<Label, usize> = HashMap::new();
+        let mut shift_delta: isize = 0;
         let mut rev_ctx = self.ctx.iter().rev().map(|(b, i)| (b.to_label(), i));
 
         let found_item = loop {
@@ -50,7 +48,7 @@ impl TyCtx {
                     None => break item,
                 };
                 if let CtxItem::Kept(_, _) = item {
-                    *shift_map.entry(label).or_insert(0) += 1;
+                    shift_delta += 1;
                 }
             } else {
                 // Unbound variable
@@ -65,13 +63,8 @@ impl TyCtx {
             ),
             CtxItem::Replaced(v) => v.clone(),
         };
-
-        let v = v.under_multiple_binders(&shift_map);
-        // for (x, n) in shift_map {
-        //     let x: AlphaVar = (&x).into();
-        //     // Can't fail since delta is positive
-        //     v = v.shift(n as isize, &x).unwrap();
-        // }
+        // Can't fail because delta is positive
+        let v = v.shift(shift_delta, &AlphaVar::default()).unwrap();
         return Some(v);
     }
     // pub fn lookup_alpha(&self, var: &AlphaVar) -> Option<Value> {
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index d843a1b..6ae0a90 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -255,14 +255,6 @@ impl Value {
         // 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 {
-        self.as_internal()
-            .under_multiple_binders(shift_map)
-            .into_value()
-    }
     pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         match &*self.as_kind() {
             // If the var matches, we can just reuse the provided value instead of copying it.
@@ -369,20 +361,6 @@ impl ValueInternal {
             span: self.span.clone(),
         })
     }
-    fn under_multiple_binders(
-        &self,
-        shift_map: &HashMap<Label, usize>,
-    ) -> Self {
-        ValueInternal {
-            form: self.form,
-            kind: self.kind.under_multiple_binders(shift_map),
-            ty: match &self.ty {
-                None => None,
-                Some(ty) => Some(ty.under_multiple_binders(shift_map)),
-            },
-            span: self.span.clone(),
-        }
-    }
     fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         ValueInternal {
             // The resulting value may not stay in wnhf after substitution
@@ -482,29 +460,6 @@ impl ValueKind<Value> {
             )?,
         })
     }
-    #[allow(dead_code)]
-    fn under_multiple_binders(
-        &self,
-        shift_map: &HashMap<Label, usize>,
-    ) -> Self {
-        match self {
-            ValueKind::Var(v) => {
-                ValueKind::Var(v.under_multiple_binders(shift_map))
-            }
-            _ => self.map_ref_with_special_handling_of_binders(
-                |v| v.under_multiple_binders(shift_map),
-                |b, _, v| {
-                    let mut v = v.clone();
-                    for (x, n) in shift_map {
-                        let x: AlphaVar = x.into();
-                        // Can't fail since delta is positive
-                        v = v.shift(*n as isize, &x.under_binder(b)).unwrap();
-                    }
-                    v
-                },
-            ),
-        }
-    }
     fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         match self {
             ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(),
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index f3475e7..93776bf 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -1,5 +1,3 @@
-use std::collections::HashMap;
-
 use crate::syntax::{Label, V};
 
 /// Stores an alpha-normalized variable.
@@ -16,6 +14,9 @@ pub struct Binder {
 }
 
 impl AlphaVar {
+    pub(crate) fn default() -> Self {
+        AlphaVar { alpha: V((), 0) }
+    }
     pub(crate) fn idx(&self) -> usize {
         self.alpha.idx()
     }
@@ -35,14 +36,6 @@ impl AlphaVar {
     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 {
-        AlphaVar {
-            alpha: self.alpha.under_multiple_binders(shift_map),
-        }
-    }
 }
 
 impl Binder {
@@ -89,11 +82,6 @@ impl std::fmt::Debug for Binder {
     }
 }
 
-impl<'a> From<&'a Label> for AlphaVar {
-    fn from(x: &'a Label) -> AlphaVar {
-        AlphaVar { alpha: V((), 0) }
-    }
-}
 impl From<Binder> for AlphaVar {
     fn from(x: Binder) -> AlphaVar {
         AlphaVar { alpha: V((), 0) }
@@ -101,7 +89,7 @@ impl From<Binder> for AlphaVar {
 }
 impl<'a> From<&'a Binder> for AlphaVar {
     fn from(x: &'a Binder) -> AlphaVar {
-        x.clone().into()
+        AlphaVar { alpha: V((), 0) }
     }
 }
 
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 2372b0a..170cbe7 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -1,5 +1,3 @@
-use std::collections::HashMap;
-
 use crate::syntax::map::{DupTreeMap, DupTreeSet};
 use crate::syntax::visitor::{self, ExprKindMutVisitor, ExprKindVisitor};
 use crate::syntax::*;
@@ -319,30 +317,6 @@ impl<Label: PartialEq + Clone> V<Label> {
     }
 }
 
-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,
-- 
cgit v1.2.3