From b7d847cc812e6a7ce52354b15a9ed6b41ffeb3b4 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 17 Jan 2020 18:57:52 +0000
Subject: Simplify

---
 dhall/src/semantics/core/context.rs | 12 +++++++-----
 dhall/src/semantics/core/value.rs   | 26 ++++++++++----------------
 dhall/src/semantics/core/var.rs     | 21 ++-------------------
 3 files changed, 19 insertions(+), 40 deletions(-)

(limited to 'dhall/src/semantics/core')

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
-- 
cgit v1.2.3