Fix some variable shifting failures

4 files changed, 53 insertions, 14 deletions

diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 7972a20..0e62fef 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -2,7 +2,8 @@ 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::semantics::nze::{NzVar, QuoteEnv};
+use crate::semantics::phase::normalize::{NzEnv, NzEnvItem};
 use crate::syntax::{Label, V};
 
 #[derive(Debug, Clone)]
@@ -69,7 +70,19 @@ impl TyCtx {
                 ValueKind::Var(AlphaVar::default(), NzVar::new(var_idx)),
                 t.clone(),
             ),
-            CtxItem::Replaced(v) => v.clone(),
+            CtxItem::Replaced(v) => v.clone()
+                // .to_tyexpr(QuoteEnv::construct(var_idx))
+                // .normalize_whnf(&NzEnv::construct(
+                //     self.ctx
+                //         .iter()
+                //         .filter_map(|(_, i)| match i {
+                //             CtxItem::Kept(t) => {
+                //                 Some(NzEnvItem::Kept(t.clone()))
+                //             }
+                //             CtxItem::Replaced(_) => None,
+                //         })
+                //         .collect(),
+                // )),
         };
         // Can't fail because delta is positive
         let v = v.shift(shift_delta, &AlphaVar::default()).unwrap();
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 96bb99a..11d8bd8 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -185,7 +185,7 @@ impl Value {
             self.normalize_nf();
         }
 
-        self.to_tyexpr(QuoteEnv::new()).to_expr(opts)
+        self.to_tyexpr_noenv().to_expr(opts)
     }
     pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind<Value> {
         self.as_whnf().clone()
@@ -292,11 +292,9 @@ impl Value {
 
     pub fn to_tyexpr(&self, qenv: QuoteEnv) -> TyExpr {
         let tye = match &*self.as_kind() {
-            ValueKind::Var(v, _w) => {
-                TyExprKind::Var(*v)
-                // TODO: Only works when we don't normalize under lambdas
-                // TyExprKind::Var(qenv.lookup(w))
-            }
+            // ValueKind::Var(v, _w) => TyExprKind::Var(*v),
+            // TODO: Only works when we don't normalize under lambdas
+            ValueKind::Var(_v, w) => TyExprKind::Var(qenv.lookup(w)),
             ValueKind::LamClosure {
                 binder,
                 annot,
@@ -611,7 +609,13 @@ impl ValueKind<Value> {
 
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(match self {
-            ValueKind::Var(v, w) => ValueKind::Var(v.shift(delta, var)?, *w),
+            ValueKind::Var(v, w) if var.idx() <= v.idx() => {
+                ValueKind::Var(v.shift(delta, var)?, *w)
+            }
+            ValueKind::Var(v, w) => {
+                ValueKind::Var(v.shift(delta, var)?, w.shift(delta))
+            }
+            // 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())?),
diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs
index 723c895..49aa704 100644
--- a/dhall/src/semantics/nze/nzexpr.rs
+++ b/dhall/src/semantics/nze/nzexpr.rs
@@ -217,6 +217,9 @@ impl QuoteEnv {
     pub fn new() -> Self {
         QuoteEnv { size: 0 }
     }
+    pub fn construct(size: usize) -> Self {
+        QuoteEnv { size }
+    }
     pub fn insert(&self) -> Self {
         QuoteEnv {
             size: self.size + 1,
@@ -231,6 +234,11 @@ impl NzVar {
     pub fn new(idx: usize) -> Self {
         NzVar { idx }
     }
+    pub fn shift(&self, delta: isize) -> Self {
+        NzVar {
+            idx: (self.idx as isize + delta) as usize,
+        }
+    }
 }
 
 impl TyExpr {
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index ac60ce0..3ddfb84 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -12,8 +12,8 @@ use crate::semantics::{
 use crate::syntax;
 use crate::syntax::Const::Type;
 use crate::syntax::{
-    BinOp, Builtin, ExprKind, InterpolatedText, InterpolatedTextContents,
-    Label, NaiveDouble,
+    BinOp, Builtin, Const, ExprKind, InterpolatedText,
+    InterpolatedTextContents, Label, NaiveDouble,
 };
 
 // Ad-hoc macro to help construct closures
@@ -822,7 +822,7 @@ pub(crate) fn normalize_whnf(
 }
 
 #[derive(Debug, Clone)]
-enum NzEnvItem {
+pub(crate) enum NzEnvItem {
     // Variable is bound with given type
     Kept(Value),
     // Variable has been replaced by corresponding value
@@ -838,6 +838,9 @@ impl NzEnv {
     pub fn new() -> Self {
         NzEnv { items: Vec::new() }
     }
+    pub fn construct(items: Vec<NzEnvItem>) -> Self {
+        NzEnv { items }
+    }
 
     pub fn insert_type(&self, t: Value) -> Self {
         let mut env = self.clone();
@@ -851,9 +854,16 @@ impl NzEnv {
     }
     pub fn lookup_val(&self, var: &AlphaVar) -> Value {
         let idx = self.items.len() - 1 - var.idx();
+        let var_idx = self.items[..idx]
+            .iter()
+            .filter(|i| match i {
+                NzEnvItem::Kept(_) => true,
+                NzEnvItem::Replaced(_) => false,
+            })
+            .count();
         match &self.items[idx] {
             NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf(
-                ValueKind::Var(var.clone(), NzVar::new(idx)),
+                ValueKind::Var(var.clone(), NzVar::new(var_idx)),
                 ty.clone(),
             ),
             NzEnvItem::Replaced(x) => x.clone(),
@@ -863,7 +873,11 @@ impl NzEnv {
 
 /// Normalize a TyExpr into WHNF
 pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value {
-    let ty = tye.get_type().unwrap();
+    let ty = match tye.get_type() {
+        Ok(ty) => ty,
+        Err(_) => return Value::from_const(Const::Sort),
+    };
+
     let kind = match tye.kind() {
         TyExprKind::Var(var) => return env.lookup_val(var),
         TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => {