Promote shift and subst_shift to traits

7 files changed, 161 insertions, 115 deletions

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index 0466058..e693317 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -6,7 +6,7 @@ use dhall_syntax::{Label, V};
 
 use crate::core::thunk::Thunk;
 use crate::core::value::Value;
-use crate::core::var::AlphaVar;
+use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::phase::{Normalized, Type, Typed};
 
 #[derive(Debug, Clone)]
@@ -27,24 +27,6 @@ pub(crate) enum TyEnvItem {
 #[derive(Debug, Clone)]
 pub(crate) struct TypecheckContext(pub(crate) Context<Label, TyEnvItem>);
 
-impl NzEnvItem {
-    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
-        use NzEnvItem::*;
-        match self {
-            Thunk(e) => Thunk(e.shift(delta, var)),
-            Skip(v) => Skip(v.shift(delta, var)),
-        }
-    }
-
-    pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
-        match self {
-            NzEnvItem::Thunk(e) => NzEnvItem::Thunk(e.subst_shift(var, val)),
-            NzEnvItem::Skip(v) if v == var => NzEnvItem::Thunk(val.to_thunk()),
-            NzEnvItem::Skip(v) => NzEnvItem::Skip(v.shift(-1, var)),
-        }
-    }
-}
-
 impl NormalizationContext {
     pub(crate) fn new() -> Self {
         NormalizationContext(Rc::new(Context::new()))
@@ -79,26 +61,6 @@ impl NormalizationContext {
         }
         NormalizationContext(Rc::new(ctx))
     }
-
-    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
-        NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
-    }
-
-    pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
-        NormalizationContext(Rc::new(
-            self.0.map(|_, e| e.subst_shift(var, val)),
-        ))
-    }
-}
-
-impl TyEnvItem {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
-        use TyEnvItem::*;
-        match self {
-            Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)),
-            Value(e) => Value(e.shift(delta, var)),
-        }
-    }
 }
 
 impl TypecheckContext {
@@ -127,6 +89,50 @@ impl TypecheckContext {
     }
 }
 
+impl Shift for NzEnvItem {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+        use NzEnvItem::*;
+        match self {
+            Thunk(e) => Thunk(e.shift(delta, var)),
+            Skip(v) => Skip(v.shift(delta, var)),
+        }
+    }
+}
+
+impl Shift for NormalizationContext {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+        NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
+    }
+}
+
+impl Shift for TyEnvItem {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+        use TyEnvItem::*;
+        match self {
+            Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)),
+            Value(e) => Value(e.shift(delta, var)),
+        }
+    }
+}
+
+impl Subst<Typed> for NzEnvItem {
+    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+        match self {
+            NzEnvItem::Thunk(e) => NzEnvItem::Thunk(e.subst_shift(var, val)),
+            NzEnvItem::Skip(v) if v == var => NzEnvItem::Thunk(val.to_thunk()),
+            NzEnvItem::Skip(v) => NzEnvItem::Skip(v.shift(-1, var)),
+        }
+    }
+}
+
+impl Subst<Typed> for NormalizationContext {
+    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+        NormalizationContext(Rc::new(
+            self.0.map(|_, e| e.subst_shift(var, val)),
+        ))
+    }
+}
+
 impl PartialEq for TypecheckContext {
     fn eq(&self, _: &Self) -> bool {
         // don't count contexts when comparing stuff
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index 14ef710..b3817dc 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
 use crate::core::context::NormalizationContext;
 use crate::core::context::TypecheckContext;
 use crate::core::value::Value;
-use crate::core::var::AlphaVar;
+use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::TypeError;
 use crate::phase::normalize::{
     apply_any, normalize_whnf, InputSubExpr, OutputSubExpr,
@@ -93,30 +93,6 @@ impl ThunkInternal {
             ThunkInternal::Value(NF, v) => v,
         }
     }
-
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
-        match self {
-            ThunkInternal::Unnormalized(ctx, e) => {
-                ThunkInternal::Unnormalized(ctx.shift(delta, var), e.clone())
-            }
-            ThunkInternal::Value(m, v) => {
-                ThunkInternal::Value(*m, v.shift(delta, var))
-            }
-        }
-    }
-
-    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
-        match self {
-            ThunkInternal::Unnormalized(ctx, e) => ThunkInternal::Unnormalized(
-                ctx.subst_shift(var, val),
-                e.clone(),
-            ),
-            ThunkInternal::Value(_, v) => {
-                // The resulting value may not stay in normal form after substitution
-                ThunkInternal::Value(WHNF, v.subst_shift(var, val))
-            }
-        }
-    }
 }
 
 impl Thunk {
@@ -204,14 +180,6 @@ impl Thunk {
     pub(crate) fn app_thunk(&self, th: Thunk) -> Value {
         apply_any(self.clone(), th)
     }
-
-    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
-        self.0.borrow().shift(delta, var).into_thunk()
-    }
-
-    pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
-        self.0.borrow().subst_shift(var, val).into_thunk()
-    }
 }
 
 impl TypeThunk {
@@ -267,15 +235,59 @@ impl TypeThunk {
     ) -> OutputSubExpr {
         self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
     }
+}
+
+impl Shift for Thunk {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+        self.0.borrow().shift(delta, var).into_thunk()
+    }
+}
+
+impl Shift for ThunkInternal {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+        match self {
+            ThunkInternal::Unnormalized(ctx, e) => {
+                ThunkInternal::Unnormalized(ctx.shift(delta, var), e.clone())
+            }
+            ThunkInternal::Value(m, v) => {
+                ThunkInternal::Value(*m, v.shift(delta, var))
+            }
+        }
+    }
+}
 
-    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+impl Shift for TypeThunk {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
             TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)),
         }
     }
+}
 
-    pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<Typed> for Thunk {
+    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+        self.0.borrow().subst_shift(var, val).into_thunk()
+    }
+}
+
+impl Subst<Typed> for ThunkInternal {
+    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+        match self {
+            ThunkInternal::Unnormalized(ctx, e) => ThunkInternal::Unnormalized(
+                ctx.subst_shift(var, val),
+                e.clone(),
+            ),
+            ThunkInternal::Value(_, v) => {
+                // The resulting value may not stay in normal form after substitution
+                ThunkInternal::Value(WHNF, v.subst_shift(var, val))
+            }
+        }
+    }
+}
+
+impl Subst<Typed> for TypeThunk {
+    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
             TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 4c71778..412fe11 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -7,7 +7,7 @@ use dhall_syntax::{
 };
 
 use crate::core::thunk::{Thunk, TypeThunk};
-use crate::core::var::{AlphaLabel, AlphaVar};
+use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
 use crate::phase::normalize::{
     apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr,
 };
@@ -316,8 +316,10 @@ impl Value {
     pub(crate) fn from_builtin(b: Builtin) -> Value {
         Value::AppliedBuiltin(b, vec![])
     }
+}
 
-    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+impl Shift for Value {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
         match self {
             Value::Lam(x, t, e) => Value::Lam(
                 x.clone(),
@@ -413,8 +415,10 @@ impl Value {
             }
         }
     }
+}
 
-    pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<Typed> for Value {
+    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
         match self {
             // Retry normalizing since substituting may allow progress
             Value::AppliedBuiltin(b, args) => apply_builtin(
diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs
index e431fc2..21bc06b 100644
--- a/dhall/src/core/var.rs
+++ b/dhall/src/core/var.rs
@@ -14,6 +14,14 @@ pub(crate) struct AlphaVar {
 #[derive(Debug, Clone, Eq)]
 pub(crate) struct AlphaLabel(Label);
 
+pub(crate) trait Shift {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Self;
+}
+
+pub(crate) trait Subst<T>: Shift {
+    fn subst_shift(&self, var: &AlphaVar, val: &T) -> Self;
+}
+
 impl AlphaVar {
     pub(crate) fn to_var(&self, alpha: bool) -> V<Label> {
         match (alpha, &self.alpha) {
@@ -27,15 +35,6 @@ impl AlphaVar {
             alpha: None,
         }
     }
-    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
-        AlphaVar {
-            normal: self.normal.shift(delta, &var.normal),
-            alpha: match (&self.alpha, &var.alpha) {
-                (Some(x), Some(v)) => Some(x.shift(delta, v)),
-                _ => None,
-            },
-        }
-    }
 }
 
 impl AlphaLabel {
@@ -51,6 +50,18 @@ impl AlphaLabel {
     }
 }
 
+impl Shift for AlphaVar {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+        AlphaVar {
+            normal: self.normal.shift(delta, &var.normal),
+            alpha: match (&self.alpha, &var.alpha) {
+                (Some(x), Some(v)) => Some(x.shift(delta, v)),
+                _ => None,
+            },
+        }
+    }
+}
+
 impl std::cmp::PartialEq for AlphaVar {
     fn eq(&self, other: &Self) -> bool {
         match (&self.alpha, &other.alpha) {
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 97b8083..5c910bc 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -7,7 +7,7 @@ use dhall_syntax::{Const, Import, Span, SubExpr, X};
 use crate::core::context::TypecheckContext;
 use crate::core::thunk::Thunk;
 use crate::core::value::Value;
-use crate::core::var::AlphaVar;
+use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::{Error, ImportError, TypeError, TypeMessage};
 
 use resolve::ImportRoot;
@@ -168,26 +168,6 @@ impl Typed {
             Typed::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)),
         }
     }
-
-    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
-        match self {
-            Typed::Value(th, t) => Typed::Value(
-                th.shift(delta, var),
-                t.as_ref().map(|x| x.shift(delta, var)),
-            ),
-            Typed::Const(c) => Typed::Const(*c),
-        }
-    }
-
-    pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
-        match self {
-            Typed::Value(th, t) => Typed::Value(
-                th.subst_shift(var, val),
-                t.as_ref().map(|x| x.subst_shift(var, val)),
-            ),
-            Typed::Const(c) => Typed::Const(*c),
-        }
-    }
 }
 
 impl Type {
@@ -226,13 +206,6 @@ impl Type {
     pub(crate) fn from_const(c: Const) -> Self {
         Type(Box::new(Typed::from_const(c)))
     }
-
-    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
-        Type(Box::new(self.0.shift(delta, var)))
-    }
-    pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
-        Type(Box::new(self.0.subst_shift(var, val)))
-    }
 }
 
 impl Normalized {
@@ -259,12 +232,50 @@ impl Normalized {
     pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
         self.0.get_type()
     }
+}
+
+impl Shift for Typed {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+        match self {
+            Typed::Value(th, t) => Typed::Value(
+                th.shift(delta, var),
+                t.as_ref().map(|x| x.shift(delta, var)),
+            ),
+            Typed::Const(c) => Typed::Const(*c),
+        }
+    }
+}
+
+impl Shift for Type {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+        Type(Box::new(self.0.shift(delta, var)))
+    }
+}
 
-    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+impl Shift for Normalized {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
         Normalized(self.0.shift(delta, var))
     }
 }
 
+impl Subst<Typed> for Typed {
+    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+        match self {
+            Typed::Value(th, t) => Typed::Value(
+                th.subst_shift(var, val),
+                t.as_ref().map(|x| x.subst_shift(var, val)),
+            ),
+            Typed::Const(c) => Typed::Const(*c),
+        }
+    }
+}
+
+impl Subst<Typed> for Type {
+    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+        Type(Box::new(self.0.subst_shift(var, val)))
+    }
+}
+
 macro_rules! derive_traits_for_wrapper_struct {
     ($ty:ident) => {
         impl std::cmp::PartialEq for $ty {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 5dfcfb6..e9fc570 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -5,6 +5,7 @@ use dhall_syntax::{BinOp, Builtin, ExprF, InterpolatedTextContents, Label, X};
 use crate::core::context::NormalizationContext;
 use crate::core::thunk::{Thunk, TypeThunk};
 use crate::core::value::Value;
+use crate::core::var::Subst;
 use crate::phase::{NormalizedSubExpr, ResolvedSubExpr, Typed};
 
 pub(crate) type InputSubExpr = ResolvedSubExpr;
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 32c1531..f8ee559 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -11,6 +11,7 @@ use dhall_syntax::{
 use crate::core::context::{NormalizationContext, TypecheckContext};
 use crate::core::thunk::{Thunk, TypeThunk};
 use crate::core::value::Value;
+use crate::core::var::Subst;
 use crate::error::{TypeError, TypeMessage};
 use crate::phase::{Normalized, Resolved, Type, Typed};