From a24f2d1367b2848779014c7bb3ecfe6bfbcff7d7 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 Jan 2020 18:38:30 +0000
Subject: Fix some variable shifting failures

---
 dhall/src/semantics/core/context.rs | 17 +++++++++++++++--
 dhall/src/semantics/core/value.rs   | 18 +++++++++++-------
 2 files changed, 26 insertions(+), 9 deletions(-)

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

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())?),
-- 
cgit v1.2.3