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/value.rs | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

(limited to 'dhall/src/semantics/core/value.rs')

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