Simplify

5 files changed, 34 insertions, 56 deletions

diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 47d2d2d..8c64c26 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -6,7 +6,9 @@ use crate::syntax::{Label, V};
 
 #[derive(Debug, Clone)]
 enum CtxItem {
-    Kept(AlphaVar, Value),
+    // Variable is bound with given type
+    Kept(Value),
+    // Variable has been replaced by corresponding value
     Replaced(Value),
 }
 
@@ -24,7 +26,7 @@ impl TyCtx {
     }
     pub fn insert_type(&self, x: &Binder, t: Value) -> Self {
         let mut vec = self.ctx.clone();
-        vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x))));
+        vec.push((x.clone(), CtxItem::Kept(t.under_binder())));
         self.with_vec(vec)
     }
     pub fn insert_value(
@@ -47,7 +49,7 @@ impl TyCtx {
                     Some(newvar) => newvar,
                     None => break item,
                 };
-                if let CtxItem::Kept(_, _) = item {
+                if let CtxItem::Kept(_) = item {
                     shift_delta += 1;
                 }
             } else {
@@ -57,8 +59,8 @@ impl TyCtx {
         };
 
         let v = match found_item {
-            CtxItem::Kept(newvar, t) => Value::from_kind_and_type(
-                ValueKind::Var(newvar.clone()),
+            CtxItem::Kept(t) => Value::from_kind_and_type(
+                ValueKind::Var(AlphaVar::default()),
                 t.clone(),
             ),
             CtxItem::Replaced(v) => v.clone(),
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 6ae0a90..8b3ada1 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -209,9 +209,9 @@ impl Value {
 
     pub(crate) fn app(&self, v: Value) -> Value {
         let body_t = match &*self.get_type_not_sort().as_whnf() {
-            ValueKind::Pi(x, t, e) => {
+            ValueKind::Pi(_, t, e) => {
                 v.check_type(t);
-                e.subst_shift(&x.into(), &v)
+                e.subst_shift(&AlphaVar::default(), &v)
             }
             _ => unreachable!("Internal type error"),
         };
@@ -242,18 +242,12 @@ impl Value {
     pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(self.as_internal().shift(delta, var)?.into_value())
     }
-    pub(crate) fn over_binder<T>(&self, x: T) -> Option<Self>
-    where
-        T: Into<AlphaVar>,
-    {
-        self.shift(-1, &x.into())
+    pub(crate) fn over_binder(&self) -> Option<Self> {
+        self.shift(-1, &AlphaVar::default())
     }
-    pub(crate) fn under_binder<T>(&self, x: T) -> Self
-    where
-        T: Into<AlphaVar>,
-    {
+    pub(crate) fn under_binder(&self) -> Self {
         // Can't fail since delta is positive
-        self.shift(1, &x.into()).unwrap()
+        self.shift(1, &AlphaVar::default()).unwrap()
     }
     pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         match &*self.as_kind() {
@@ -456,18 +450,18 @@ impl ValueKind<Value> {
             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))?),
+                |_, _, x| Ok(x.shift(delta, &var.under_binder())?),
             )?,
         })
     }
     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.over_binder(var).unwrap()),
+            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))
+                |_, _, x| {
+                    x.subst_shift(&var.under_binder(), &val.under_binder())
                 },
             ),
         }
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 93776bf..b336c66 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -26,15 +26,9 @@ impl AlphaVar {
             alpha: self.alpha.shift(delta, &var.alpha)?,
         })
     }
-    pub(crate) fn under_binder<T>(&self, x: T) -> Self
-    where
-        T: Into<AlphaVar>,
-    {
+    pub(crate) fn under_binder(&self) -> Self {
         // Can't fail since delta is positive
-        self.shift(1, &x.into()).unwrap()
-    }
-    pub(crate) fn over_binder(&self, x: &AlphaVar) -> Option<Self> {
-        self.shift(-1, x)
+        self.shift(1, &AlphaVar::default()).unwrap()
     }
 }
 
@@ -82,17 +76,6 @@ impl std::fmt::Debug for Binder {
     }
 }
 
-impl From<Binder> for AlphaVar {
-    fn from(x: Binder) -> AlphaVar {
-        AlphaVar { alpha: V((), 0) }
-    }
-}
-impl<'a> From<&'a Binder> for AlphaVar {
-    fn from(x: &'a Binder) -> AlphaVar {
-        AlphaVar { alpha: V((), 0) }
-    }
-}
-
 impl From<Binder> for Label {
     fn from(x: Binder) -> Label {
         x.name
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 8f9a58a..541a196 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -1,10 +1,9 @@
 use std::collections::HashMap;
 use std::convert::TryInto;
 
-use crate::semantics::core::value::Value;
-use crate::semantics::core::value::ValueKind;
 use crate::semantics::phase::typecheck::{rc, typecheck};
 use crate::semantics::phase::Normalized;
+use crate::semantics::{AlphaVar, Value, ValueKind};
 use crate::syntax;
 use crate::syntax::Const::Type;
 use crate::syntax::{
@@ -367,9 +366,9 @@ pub(crate) fn apply_builtin(
 pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> {
     let f_borrow = f.as_whnf();
     match &*f_borrow {
-        ValueKind::Lam(x, _, e) => {
-            e.subst_shift(&x.into(), &a).to_whnf_check_type(ty)
-        }
+        ValueKind::Lam(_, _, e) => e
+            .subst_shift(&AlphaVar::default(), &a)
+            .to_whnf_check_type(ty),
         ValueKind::AppliedBuiltin(b, args) => {
             use std::iter::once;
             let args = args.iter().cloned().chain(once(a.clone())).collect();
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 852f41b..15025c1 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, Value, ValueKind};
+use crate::semantics::{AlphaVar, Binder, Value, ValueKind};
 use crate::syntax;
 use crate::syntax::{
     Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span,
@@ -385,15 +385,15 @@ fn type_last_layer(
         App(f, a) => {
             let tf = f.get_type()?;
             let tf_borrow = tf.as_whnf();
-            let (x, tx, tb) = match &*tf_borrow {
-                ValueKind::Pi(x, tx, tb) => (x, tx, tb),
+            let (tx, tb) = match &*tf_borrow {
+                ValueKind::Pi(_, tx, tb) => (tx, tb),
                 _ => return mkerr(NotAFunction(f.clone())),
             };
             if &a.get_type()? != tx {
                 return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone()));
             }
 
-            let ret = tb.subst_shift(&x.into(), a);
+            let ret = tb.subst_shift(&AlphaVar::default(), a);
             ret.normalize_nf();
             RetTypeOnly(ret)
         }
@@ -500,13 +500,12 @@ fn type_last_layer(
                         ValueKind::UnionType(kts) => match kts.get(&x) {
                             // Constructor has type T -> < x: T, ... >
                             Some(Some(t)) => {
-                                let x = ctx.new_binder(x);
                                 RetTypeOnly(
                                     tck_pi_type(
                                         ctx,
-                                        x.clone(),
+                                        ctx.new_binder(x),
                                         t.clone(),
-                                        r.under_binder(x),
+                                        r.under_binder(),
                                     )?
                                 )
                             },
@@ -719,8 +718,8 @@ fn type_last_layer(
                         // Union alternative with type
                         Some(Some(variant_type)) => {
                             let handler_type_borrow = handler_type.as_whnf();
-                            let (x, tx, tb) = match &*handler_type_borrow {
-                                ValueKind::Pi(x, tx, tb) => (x, tx, tb),
+                            let (tx, tb) = match &*handler_type_borrow {
+                                ValueKind::Pi(_, tx, tb) => (tx, tb),
                                 _ => {
                                     return mkerr(NotAFunction(
                                         handler_type.clone(),
@@ -736,8 +735,9 @@ fn type_last_layer(
                                 ));
                             }
 
-                            // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`.
-                            match tb.over_binder(x) {
+                            // Extract `tb` from under the binder. Fails if the variable was used
+                            // in `tb`.
+                            match tb.over_binder() {
                                 Some(x) => x,
                                 None => return mkerr(
                                     MergeHandlerReturnTypeMustNotBeDependent,