Cleanup variable handling

9 files changed, 39 insertions, 63 deletions

diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 7334552..918826b 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -3,7 +3,7 @@ use std::collections::HashMap;
 use std::rc::Rc;
 
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::core::var::{AlphaVar, Binder};
+use crate::semantics::core::var::Binder;
 use crate::semantics::phase::normalize::{apply_any, normalize_whnf};
 use crate::semantics::phase::typecheck::{
     builtin_to_value, builtin_to_value_env, const_to_value,
@@ -83,7 +83,7 @@ pub(crate) enum ValueKind<Value> {
     // Keep env around to construct Foo/build closures; hopefully temporary.
     AppliedBuiltin(Builtin, Vec<Value>, Vec<Value>, NzEnv),
 
-    Var(AlphaVar, NzVar),
+    Var(NzVar),
     Const(Const),
     BoolLit(bool),
     NaturalLit(Natural),
@@ -258,9 +258,7 @@ impl Value {
 
     pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
         let tye = match &*self.as_kind() {
-            // ValueKind::Var(v, _w) => TyExprKind::Var(*v),
-            // TODO: Only works when we don't normalize under lambdas
-            ValueKind::Var(_v, w) => TyExprKind::Var(venv.lookup(w)),
+            ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)),
             ValueKind::LamClosure {
                 binder,
                 annot,
@@ -618,7 +616,7 @@ impl Closure {
         match self {
             Closure::Closure { arg_ty, .. } => {
                 let val = Value::from_kind_and_type(
-                    ValueKind::Var(AlphaVar::default(), var),
+                    ValueKind::Var(var),
                     arg_ty.clone(),
                 );
                 self.apply(val)
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 3458489..264b81d 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -1,16 +1,4 @@
-use crate::syntax::{Label, V};
-
-/// Stores an alpha-normalized variable.
-#[derive(Clone, Copy, Eq)]
-pub struct AlphaVar {
-    alpha: V<()>,
-}
-// TODO: temporary hopefully
-impl std::cmp::PartialEq for AlphaVar {
-    fn eq(&self, _other: &Self) -> bool {
-        true
-    }
-}
+use crate::syntax::Label;
 
 // Exactly like a Label, but equality returns always true.
 // This is so that ValueKind equality is exactly alpha-equivalence.
@@ -19,18 +7,6 @@ pub struct Binder {
     name: Label,
 }
 
-impl AlphaVar {
-    pub(crate) fn new(alpha: V<()>) -> Self {
-        AlphaVar { alpha }
-    }
-    pub(crate) fn default() -> Self {
-        AlphaVar { alpha: V((), 0) }
-    }
-    pub(crate) fn idx(&self) -> usize {
-        self.alpha.idx()
-    }
-}
-
 impl Binder {
     pub(crate) fn new(name: Label) -> Self {
         Binder { name }
@@ -47,12 +23,6 @@ impl std::cmp::PartialEq for Binder {
     }
 }
 
-impl std::fmt::Debug for AlphaVar {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        write!(f, "AlphaVar({})", self.alpha.1)
-    }
-}
-
 impl std::fmt::Debug for Binder {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         write!(f, "Binder({})", &self.name)
diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs
index aec66f8..2191ce3 100644
--- a/dhall/src/semantics/core/visitor.rs
+++ b/dhall/src/semantics/core/visitor.rs
@@ -96,7 +96,7 @@ where
             v.visit_vec(types)?,
             env.clone(),
         ),
-        Var(v, w) => Var(v.clone(), *w),
+        Var(v) => Var(*v),
         Const(k) => Const(*k),
         BoolLit(b) => BoolLit(*b),
         NaturalLit(n) => NaturalLit(*n),
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 203d99a..3c42ee7 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -66,7 +66,7 @@ impl NzEnv {
         let idx = self.items.len() - 1 - var.idx();
         match &self.items[idx] {
             NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf(
-                ValueKind::Var(var.clone(), NzVar::new(idx)),
+                ValueKind::Var(NzVar::new(idx)),
                 ty.clone(),
             ),
             NzEnvItem::Replaced(x) => x.clone(),
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 32c2f21..1276a48 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -37,7 +37,7 @@ impl VarEnv {
     }
     pub fn lookup_fallible(&self, var: &NzVar) -> Option<AlphaVar> {
         let idx = self.size.checked_sub(var.idx() + 1)?;
-        Some(AlphaVar::new(V((), idx)))
+        Some(AlphaVar::new(idx))
     }
 }
 
@@ -68,7 +68,7 @@ impl NameEnv {
         self.names.pop();
     }
 
-    pub fn unlabel_var(&self, var: &V<Label>) -> Option<AlphaVar> {
+    pub fn unlabel_var(&self, var: &V) -> Option<AlphaVar> {
         let V(name, idx) = var;
         let (idx, _) = self
             .names
@@ -77,9 +77,9 @@ impl NameEnv {
             .enumerate()
             .filter(|(_, n)| *n == name)
             .nth(*idx)?;
-        Some(AlphaVar::new(V((), idx)))
+        Some(AlphaVar::new(idx))
     }
-    pub fn label_var(&self, var: &AlphaVar) -> V<Label> {
+    pub fn label_var(&self, var: &AlphaVar) -> V {
         let name = &self.names[self.names.len() - 1 - var.idx()];
         let idx = self
             .names
@@ -129,7 +129,7 @@ impl TyEnv {
             items: self.items.insert_value(e),
         }
     }
-    pub fn lookup(&self, var: &V<Label>) -> Option<(TyExprKind, Type)> {
+    pub fn lookup(&self, var: &V) -> Option<(TyExprKind, Type)> {
         let var = self.names.unlabel_var(var)?;
         let ty = self.items.lookup_val(&var).get_type().unwrap();
         Some((TyExprKind::Var(var), ty))
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 262cda6..114bb14 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,5 +1,4 @@
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::core::var::AlphaVar;
 use crate::semantics::phase::normalize::normalize_tyexpr_whnf;
 use crate::semantics::phase::typecheck::rc;
 use crate::semantics::phase::Normalized;
@@ -9,6 +8,19 @@ use crate::syntax::{ExprKind, Span, V};
 
 pub(crate) type Type = Value;
 
+/// Stores an alpha-normalized variable.
+#[derive(Debug, Clone, Copy)]
+pub struct AlphaVar {
+    idx: usize,
+}
+
+#[derive(Debug, Clone)]
+pub(crate) enum TyExprKind {
+    Var(AlphaVar),
+    // Forbidden ExprKind variants: Var, Import, Embed
+    Expr(ExprKind<TyExpr, Normalized>),
+}
+
 // An expression with inferred types at every node and resolved variables.
 #[derive(Clone)]
 pub(crate) struct TyExpr {
@@ -17,11 +29,13 @@ pub(crate) struct TyExpr {
     span: Span,
 }
 
-#[derive(Debug, Clone)]
-pub(crate) enum TyExprKind {
-    Var(AlphaVar),
-    // Forbidden ExprKind variants: Var, Import, Embed
-    Expr(ExprKind<TyExpr, Normalized>),
+impl AlphaVar {
+    pub(crate) fn new(idx: usize) -> Self {
+        AlphaVar { idx }
+    }
+    pub(crate) fn idx(&self) -> usize {
+        self.idx
+    }
 }
 
 impl TyExpr {
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 424ac34..28a0aee 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -23,8 +23,8 @@ pub enum Const {
 /// The `Label` field is the variable's name (i.e. \"`x`\").
 /// The `Int` field is a DeBruijn index.
 /// See dhall-lang/standard/semantics.md for details
-#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
-pub struct V<Label>(pub Label, pub usize);
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub struct V(pub Label, pub usize);
 
 // Definition order must match precedence order for
 // pretty-printing to work correctly
@@ -112,7 +112,7 @@ pub enum ExprKind<SubExpr, Embed> {
     Const(Const),
     ///  `x`
     ///  `x@n`
-    Var(V<Label>),
+    Var(V),
     ///  `λ(x : A) -> b`
     Lam(Label, SubExpr, SubExpr),
     ///  `A -> B`
@@ -173,12 +173,6 @@ pub enum ExprKind<SubExpr, Embed> {
     Embed(Embed),
 }
 
-impl<Label> V<Label> {
-    pub(crate) fn idx(&self) -> usize {
-        self.1
-    }
-}
-
 impl<SE, E> ExprKind<SE, E> {
     pub fn traverse_ref_maybe_binder<'a, SE2, Err>(
         &'a self,
@@ -356,8 +350,8 @@ impl From<NaiveDouble> for f64 {
     }
 }
 
-impl<Label> From<Label> for V<Label> {
-    fn from(x: Label) -> V<Label> {
+impl From<Label> for V {
+    fn from(x: Label) -> V {
         V(x, 0)
     }
 }
diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs
index ef1471f..681d6dd 100644
--- a/dhall/src/syntax/text/parser.rs
+++ b/dhall/src/syntax/text/parser.rs
@@ -422,7 +422,7 @@ impl DhallParser {
         ))
     }
 
-    fn variable(input: ParseInput) -> ParseResult<V<Label>> {
+    fn variable(input: ParseInput) -> ParseResult<V> {
         Ok(match_nodes!(input.into_children();
             [label(l), natural_literal(idx)] => V(l, idx),
             [label(l)] => V(l, 0),
diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs
index 96f4c2a..06dd70f 100644
--- a/dhall/src/syntax/text/printer.rs
+++ b/dhall/src/syntax/text/printer.rs
@@ -496,7 +496,7 @@ impl Display for Scheme {
     }
 }
 
-impl<Label: Display> Display for V<Label> {
+impl Display for V {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         let V(x, n) = self;
         x.fmt(f)?;