Prepare Value for reverse variables

I thought it would work ><. It's a bit too early

5 files changed, 49 insertions, 19 deletions

diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 8c64c26..7972a20 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -2,6 +2,7 @@ use crate::error::TypeError;
 use crate::semantics::core::value::Value;
 use crate::semantics::core::value::ValueKind;
 use crate::semantics::core::var::{AlphaVar, Binder};
+use crate::semantics::nze::NzVar;
 use crate::syntax::{Label, V};
 
 #[derive(Debug, Clone)]
@@ -42,7 +43,6 @@ impl TyCtx {
         let mut var = var.clone();
         let mut shift_delta: isize = 0;
         let mut rev_ctx = self.ctx.iter().rev().map(|(b, i)| (b.to_label(), i));
-
         let found_item = loop {
             if let Some((label, item)) = rev_ctx.next() {
                 var = match var.over_binder(&label) {
@@ -57,10 +57,16 @@ impl TyCtx {
                 return None;
             }
         };
+        let var_idx = rev_ctx
+            .filter(|(_, i)| match i {
+                CtxItem::Kept(_) => true,
+                CtxItem::Replaced(_) => false,
+            })
+            .count();
 
         let v = match found_item {
             CtxItem::Kept(t) => Value::from_kind_and_type(
-                ValueKind::Var(AlphaVar::default()),
+                ValueKind::Var(AlphaVar::default(), NzVar::new(var_idx)),
                 t.clone(),
             ),
             CtxItem::Replaced(v) => v.clone(),
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index dc6a116..a7c207d 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -4,6 +4,7 @@ use std::rc::Rc;
 
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::var::{AlphaVar, Binder};
+use crate::semantics::nze::{NzVar, QuoteEnv};
 use crate::semantics::phase::normalize::{apply_any, normalize_whnf};
 use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value};
 use crate::semantics::phase::{
@@ -60,7 +61,7 @@ pub(crate) enum ValueKind<Value> {
     // Invariant: in whnf, the evaluation must not be able to progress further.
     AppliedBuiltin(Builtin, Vec<Value>),
 
-    Var(AlphaVar),
+    Var(AlphaVar, NzVar),
     Const(Const),
     BoolLit(bool),
     NaturalLit(Natural),
@@ -167,7 +168,7 @@ impl Value {
             self.normalize_nf();
         }
 
-        self.to_tyexpr().to_expr(opts)
+        self.to_tyexpr(QuoteEnv::new()).to_expr(opts)
     }
     pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind<Value> {
         self.as_whnf().clone()
@@ -257,7 +258,7 @@ impl Value {
         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 => {
+            ValueKind::Var(v, _) if v == var => {
                 if let Ok(self_ty) = self.get_type() {
                     val.check_type(&self_ty.subst_shift(var, val));
                 }
@@ -288,18 +289,27 @@ impl Value {
     //     }
     // }
 
-    pub fn to_tyexpr(&self) -> TyExpr {
+    pub fn to_tyexpr(&self, qenv: QuoteEnv) -> TyExpr {
         let self_kind = self.as_kind();
         let self_ty = self.as_internal().ty.clone();
         let self_span = self.as_internal().span.clone();
-        if let ValueKind::Var(v) = &*self_kind {
-            return TyExpr::new(TyExprKind::Var(*v), self_ty, self_span);
+        if let ValueKind::Var(v, _w) = &*self_kind {
+            return TyExpr::new(
+                // TODO: Only works when we don't normalize under lambdas
+                // TyExprKind::Var(qenv.lookup(w)),
+                TyExprKind::Var(*v),
+                self_ty,
+                self_span,
+            );
         }
 
         // TODO: properly recover intermediate types; `None` is a time-bomb here.
-        let self_kind = self_kind.map_ref(|v| v.to_tyexpr());
+        let self_kind = self_kind.map_ref_with_special_handling_of_binders(
+            |v| v.to_tyexpr(qenv),
+            |_, _, v| v.to_tyexpr(qenv.insert()),
+        );
         let expr = match self_kind {
-            ValueKind::Var(_) => unreachable!(),
+            ValueKind::Var(..) => unreachable!(),
             ValueKind::Lam(x, t, e) => ExprKind::Lam(x.to_label(), t, e),
             ValueKind::Pi(x, t, e) => ExprKind::Pi(x.to_label(), t, e),
             ValueKind::AppliedBuiltin(b, args) => {
@@ -320,13 +330,13 @@ impl Value {
             ValueKind::IntegerLit(n) => ExprKind::IntegerLit(n),
             ValueKind::DoubleLit(n) => ExprKind::DoubleLit(n),
             ValueKind::EmptyOptionalLit(n) => ExprKind::App(
-                builtin_to_value(Builtin::OptionalNone).to_tyexpr(),
+                builtin_to_value(Builtin::OptionalNone).to_tyexpr(qenv),
                 n,
             ),
             ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n),
             ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(TyExpr::new(
                 TyExprKind::Expr(ExprKind::App(
-                    builtin_to_value(Builtin::List).to_tyexpr(),
+                    builtin_to_value(Builtin::List).to_tyexpr(qenv),
                     n,
                 )),
                 Some(const_to_value(Const::Type)),
@@ -470,7 +480,7 @@ impl ValueKind<Value> {
 
     pub(crate) fn normalize_mut(&mut self) {
         match self {
-            ValueKind::Var(_)
+            ValueKind::Var(..)
             | ValueKind::Const(_)
             | ValueKind::BoolLit(_)
             | ValueKind::NaturalLit(_)
@@ -545,7 +555,7 @@ impl ValueKind<Value> {
 
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(match self {
-            ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?),
+            ValueKind::Var(v, w) => ValueKind::Var(v.shift(delta, var)?, *w),
             _ => self.traverse_ref_with_special_handling_of_binders(
                 |x| Ok(x.shift(delta, var)?),
                 |_, _, x| Ok(x.shift(delta, &var.under_binder())?),
@@ -554,8 +564,10 @@ impl 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()),
+            ValueKind::Var(v, _) if v == var => val.to_whnf_ignore_type(),
+            ValueKind::Var(v, w) => {
+                ValueKind::Var(v.shift(-1, var).unwrap(), *w)
+            }
             _ => self.map_ref_with_special_handling_of_binders(
                 |x| x.subst_shift(var, val),
                 |_, _, x| {
diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs
index a449f6c..5a04747 100644
--- a/dhall/src/semantics/core/visitor.rs
+++ b/dhall/src/semantics/core/visitor.rs
@@ -81,7 +81,7 @@ where
             Pi(l.clone(), t, e)
         }
         AppliedBuiltin(b, xs) => AppliedBuiltin(*b, v.visit_vec(xs)?),
-        Var(v) => Var(v.clone()),
+        Var(v, w) => Var(v.clone(), *w),
         Const(k) => Const(*k),
         BoolLit(b) => BoolLit(*b),
         NaturalLit(n) => NaturalLit(*n),
diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs
index ef8918f..213404c 100644
--- a/dhall/src/semantics/nze/mod.rs
+++ b/dhall/src/semantics/nze/mod.rs
@@ -1,2 +1,2 @@
 pub mod nzexpr;
-// pub(crate) use nzexpr::*;
+pub(crate) use nzexpr::*;
diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs
index 3a5a1f9..1256ea0 100644
--- a/dhall/src/semantics/nze/nzexpr.rs
+++ b/dhall/src/semantics/nze/nzexpr.rs
@@ -82,10 +82,16 @@ pub(crate) struct QuoteEnv {
 }
 
 // Reverse-debruijn index: counts number of binders from the bottom of the stack.
-#[derive(Debug, Clone, Copy)]
+#[derive(Debug, Clone, Copy, Eq)]
 pub(crate) struct NzVar {
     idx: usize,
 }
+// TODO: temporary hopefully
+impl std::cmp::PartialEq for NzVar {
+    fn eq(&self, _other: &Self) -> bool {
+        true
+    }
+}
 
 impl TyEnv {
     pub fn new() -> Self {
@@ -219,6 +225,12 @@ impl QuoteEnv {
     }
 }
 
+impl NzVar {
+    pub fn new(idx: usize) -> Self {
+        NzVar { idx }
+    }
+}
+
 impl TyExpr {
     pub fn new(kind: TyExprKind, ty: Option<Type>) -> Self {
         TyExpr {