From 72d1e3c339cf550fa5af9981af6078a813feb80a Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 17 Jan 2020 11:03:40 +0000
Subject: Remove Shift/Subst traits

---
 dhall/src/semantics/core/context.rs | 105 ++++++++----------------------------
 1 file changed, 22 insertions(+), 83 deletions(-)

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

diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 3a7930e..16ea48f 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -3,7 +3,7 @@ use std::collections::HashMap;
 use crate::error::TypeError;
 use crate::semantics::core::value::Value;
 use crate::semantics::core::value::ValueKind;
-use crate::semantics::core::var::{AlphaVar, Binder, Shift, Subst};
+use crate::semantics::core::var::{AlphaVar, Binder};
 use crate::syntax::{Label, V};
 
 #[derive(Debug, Clone)]
@@ -17,6 +17,27 @@ pub(crate) struct TyCtx {
     ctx: Vec<(Binder, CtxItem)>,
 }
 
+impl CtxItem {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+        Some(match self {
+            CtxItem::Kept(v, t) => {
+                CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?)
+            }
+            CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?),
+        })
+    }
+    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 {
+            v = v.shift(*n as isize, &x.into()).unwrap();
+        }
+        v
+    }
+}
+
 impl TyCtx {
     pub fn new() -> Self {
         TyCtx { ctx: Vec::new() }
@@ -65,86 +86,4 @@ impl TyCtx {
     pub fn new_binder(&self, l: &Label) -> Binder {
         Binder::new(l.clone())
     }
-
-    /// Given a var that makes sense in the current context, map the given function in such a way
-    /// that the passed variable always makes sense in the context of the passed item.
-    /// Once we pass the variable definition, the variable doesn't make sense anymore so we just
-    /// copy the remaining items.
-    fn do_with_var<E>(
-        &self,
-        var: &AlphaVar,
-        mut f: impl FnMut(&AlphaVar, &CtxItem) -> Result<CtxItem, E>,
-    ) -> Result<Self, E> {
-        let mut vec = Vec::new();
-        vec.reserve(self.ctx.len());
-        let mut var = var.clone();
-        let mut iter = self.ctx.iter().rev();
-        for (l, i) in iter.by_ref() {
-            vec.push((l.clone(), f(&var, i)?));
-            if let CtxItem::Kept(_, _) = i {
-                match var.over_binder(l) {
-                    None => break,
-                    Some(newvar) => var = newvar,
-                };
-            }
-        }
-        for (l, i) in iter {
-            vec.push((l.clone(), (*i).clone()));
-        }
-        vec.reverse();
-        Ok(self.with_vec(vec))
-    }
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        if delta < 0 {
-            Some(self.do_with_var(var, |var, i| Ok(i.shift(delta, &var)?))?)
-        } else {
-            Some(
-                self.with_vec(
-                    self.ctx
-                        .iter()
-                        .map(|(l, i)| Ok((l.clone(), i.shift(delta, &var)?)))
-                        .collect::<Result<_, _>>()?,
-                ),
-            )
-        }
-    }
-    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
-        self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val)))
-            .unwrap()
-    }
-}
-
-impl Shift for CtxItem {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(match self {
-            CtxItem::Kept(v, t) => {
-                CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?)
-            }
-            CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?),
-        })
-    }
-}
-
-impl Shift for TyCtx {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        self.shift(delta, var)
-    }
-}
-
-impl Subst<Value> for CtxItem {
-    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
-        match self {
-            CtxItem::Replaced(e) => CtxItem::Replaced(e.subst_shift(var, val)),
-            CtxItem::Kept(v, t) => match v.shift(-1, var) {
-                None => CtxItem::Replaced(val.clone()),
-                Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)),
-            },
-        }
-    }
-}
-
-impl Subst<Value> for TyCtx {
-    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
-        self.subst_shift(var, val)
-    }
 }
-- 
cgit v1.2.3