6 files changed, 115 insertions, 227 deletions

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)
-    }
 }
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 28f8e37..ad03187 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
 
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::context::TyCtx;
-use crate::semantics::core::var::{AlphaVar, Binder, Shift, Subst};
+use crate::semantics::core::var::{AlphaVar, Binder};
 use crate::semantics::phase::normalize::{apply_any, normalize_whnf};
 use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value};
 use crate::semantics::phase::{Normalized, NormalizedExpr, Typed};
@@ -238,6 +238,40 @@ impl Value {
         self.get_type()
             .expect("Internal type error: value is `Sort` but shouldn't be")
     }
+
+    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+        Some(Value(Rc::new(RefCell::new(
+            self.0.borrow().shift(delta, var)?,
+        ))))
+    }
+    pub(crate) fn over_binder<T>(&self, x: T) -> Option<Self>
+    where
+        T: Into<AlphaVar>,
+    {
+        self.shift(-1, &x.into())
+    }
+    pub(crate) fn under_binder<T>(&self, x: T) -> Self
+    where
+        T: Into<AlphaVar>,
+    {
+        // Can't fail since delta is positive
+        self.shift(1, &x.into()).unwrap()
+    }
+    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.
+            // We also check that the types match, if in debug mode.
+            ValueKind::Var(v) if v == var => {
+                if let Ok(self_ty) = self.get_type() {
+                    val.check_type(&self_ty.subst_shift(var, val));
+                }
+                val.clone()
+            }
+            _ => Value(Rc::new(RefCell::new(
+                self.0.borrow().subst_shift(var, val),
+            ))),
+        }
+    }
 }
 
 impl ValueInternal {
@@ -298,6 +332,27 @@ impl ValueInternal {
             None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)),
         }
     }
+
+    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+        Some(ValueInternal {
+            form: self.form,
+            kind: self.kind.shift(delta, var)?,
+            ty: match &self.ty {
+                None => None,
+                Some(ty) => Some(ty.shift(delta, var)?),
+            },
+            span: self.span.clone(),
+        })
+    }
+    pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+        ValueInternal {
+            // The resulting value may not stay in wnhf after substitution
+            form: Unevaled,
+            kind: self.kind.subst_shift(var, val),
+            ty: self.ty.as_ref().map(|x| x.subst_shift(var, val)),
+            span: self.span.clone(),
+        }
+    }
 }
 
 impl ValueKind<Value> {
@@ -378,6 +433,28 @@ impl ValueKind<Value> {
     pub(crate) fn from_builtin(b: Builtin) -> ValueKind<Value> {
         ValueKind::AppliedBuiltin(b, vec![])
     }
+
+    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+        Some(match self {
+            ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?),
+            _ => self.traverse_ref_with_special_handling_of_binders(
+                |x| Ok(x.shift(delta, var)?),
+                |b, x| Ok(x.shift(delta, &var.under_binder(b))?),
+            )?,
+        })
+    }
+    pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+        match self {
+            ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(),
+            ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()),
+            _ => self.map_ref_with_special_handling_of_binders(
+                |x| x.subst_shift(var, val),
+                |b, x| {
+                    x.subst_shift(&var.under_binder(b), &val.under_binder(b))
+                },
+            ),
+        }
+    }
 }
 
 impl<V> ValueKind<V> {
@@ -418,85 +495,6 @@ impl<V> ValueKind<V> {
     }
 }
 
-impl Shift for Value {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(Value(Rc::new(RefCell::new(
-            self.0.borrow().shift(delta, var)?,
-        ))))
-    }
-}
-
-impl Shift for ValueInternal {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(ValueInternal {
-            form: self.form,
-            kind: self.kind.shift(delta, var)?,
-            ty: match &self.ty {
-                None => None,
-                Some(ty) => Some(ty.shift(delta, var)?),
-            },
-            span: self.span.clone(),
-        })
-    }
-}
-
-impl Shift for ValueKind<Value> {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(match self {
-            ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?),
-            _ => self.traverse_ref_with_special_handling_of_binders(
-                |x| Ok(x.shift(delta, var)?),
-                |b, x| Ok(x.shift(delta, &var.under_binder(b))?),
-            )?,
-        })
-    }
-}
-
-impl Subst<Value> for Value {
-    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.
-            // We also check that the types match, if in debug mode.
-            ValueKind::Var(v) if v == var => {
-                if let Ok(self_ty) = self.get_type() {
-                    val.check_type(&self_ty.subst_shift(var, val));
-                }
-                val.clone()
-            }
-            _ => Value(Rc::new(RefCell::new(
-                self.0.borrow().subst_shift(var, val),
-            ))),
-        }
-    }
-}
-
-impl Subst<Value> for ValueInternal {
-    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
-        ValueInternal {
-            // The resulting value may not stay in wnhf after substitution
-            form: Unevaled,
-            kind: self.kind.subst_shift(var, val),
-            ty: self.ty.as_ref().map(|x| x.subst_shift(var, val)),
-            span: self.span.clone(),
-        }
-    }
-}
-
-impl Subst<Value> for ValueKind<Value> {
-    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
-        match self {
-            ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(),
-            ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()),
-            _ => self.map_ref_with_special_handling_of_binders(
-                |x| x.subst_shift(var, val),
-                |b, x| {
-                    x.subst_shift(&var.under_binder(b), &val.under_binder(b))
-                },
-            ),
-        }
-    }
-}
-
 // TODO: use Rc comparison to shortcut on identical pointers
 impl std::cmp::PartialEq for Value {
     fn eq(&self, other: &Self) -> bool {
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index c21e53e..a110632 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 a pair of variables: a normal one and one
@@ -18,44 +16,6 @@ pub struct Binder {
     name: Label,
 }
 
-pub(crate) trait Shift: Sized {
-    // Shift an expression to move it around binders without changing the meaning of its free
-    // variables. Shift by 1 to move an expression under a binder. Shift by -1 to extract an
-    // expression from under a binder, if the expression does not refer to that bound variable.
-    // Returns None if delta was negative and the variable was free in the expression.
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self>;
-
-    fn over_binder<T>(&self, x: T) -> Option<Self>
-    where
-        T: Into<AlphaVar>,
-    {
-        self.shift(-1, &x.into())
-    }
-
-    fn under_binder<T>(&self, x: T) -> Self
-    where
-        T: Into<AlphaVar>,
-    {
-        // Can't fail since delta is positive
-        self.shift(1, &x.into()).unwrap()
-    }
-
-    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
-    }
-}
-
-pub(crate) trait Subst<S> {
-    fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self;
-}
-
 impl AlphaVar {
     pub(crate) fn to_var_maybe_alpha(&self, alpha: bool) -> V<Label> {
         if alpha {
@@ -64,6 +24,20 @@ impl AlphaVar {
             self.normal.clone()
         }
     }
+
+    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+        Some(AlphaVar {
+            normal: self.normal.shift(delta, &var.normal)?,
+            alpha: self.alpha.shift(delta, &var.alpha)?,
+        })
+    }
+    pub(crate) fn under_binder<T>(&self, x: T) -> Self
+    where
+        T: Into<AlphaVar>,
+    {
+        // Can't fail since delta is positive
+        self.shift(1, &x.into()).unwrap()
+    }
 }
 
 impl Binder {
@@ -82,15 +56,6 @@ impl Binder {
     }
 }
 
-impl Shift for AlphaVar {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(AlphaVar {
-            normal: self.normal.shift(delta, &var.normal)?,
-            alpha: self.alpha.shift(delta, &var.alpha)?,
-        })
-    }
-}
-
 /// Equality up to alpha-equivalence
 impl std::cmp::PartialEq for AlphaVar {
     fn eq(&self, other: &Self) -> bool {
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index 5d17338..6afed88 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -4,7 +4,6 @@ use std::path::Path;
 use crate::error::{EncodeError, Error, ImportError, TypeError};
 use crate::semantics::core::value::Value;
 use crate::semantics::core::value::ValueKind;
-use crate::semantics::core::var::{AlphaVar, Shift};
 use crate::semantics::to_expr::ToExprOptions;
 use crate::syntax::binary;
 use crate::syntax::{Builtin, Const, Expr};
@@ -191,18 +190,6 @@ impl Normalized {
     }
 }
 
-impl Shift for Typed {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(Typed(self.0.shift(delta, var)?))
-    }
-}
-
-impl Shift for Normalized {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(Normalized(self.0.shift(delta, var)?))
-    }
-}
-
 macro_rules! derive_traits_for_wrapper_struct {
     ($ty:ident) => {
         impl std::cmp::PartialEq for $ty {
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 7b4b37f..615b2ff 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -3,7 +3,6 @@ use std::convert::TryInto;
 
 use crate::semantics::core::value::Value;
 use crate::semantics::core::value::ValueKind;
-use crate::semantics::core::var::Subst;
 use crate::semantics::phase::typecheck::{rc, typecheck};
 use crate::semantics::phase::Normalized;
 use crate::syntax;
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 7e408eb..c77d9c4 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -6,7 +6,7 @@ use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::context::TyCtx;
 use crate::semantics::phase::normalize::merge_maps;
 use crate::semantics::phase::Normalized;
-use crate::semantics::{Binder, Shift, Subst, Value, ValueKind};
+use crate::semantics::{Binder, Value, ValueKind};
 use crate::syntax;
 use crate::syntax::{
     Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span,