From d1ad0a2036ce689d4a6b5f38a1641b9ce475df9e Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 23 Apr 2019 22:37:05 +0200
Subject: Fix shifting under Pi

---
 dhall/src/typecheck.rs | 42 +++++++++++++++++++++++++++++-------------
 1 file changed, 29 insertions(+), 13 deletions(-)

(limited to 'dhall')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index d45b93c..0ee481f 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -57,6 +57,13 @@ impl<'a> Normalized<'a> {
             self.2,
         )
     }
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        Normalized(
+            shift(delta, var, &self.0),
+            self.1.as_ref().map(|t| t.shift(delta, var)),
+            self.2,
+        )
+    }
     pub(crate) fn into_type(self) -> Result<Type<'a>, TypeError> {
         self.into_type_ctx(&TypecheckContext::new())
     }
@@ -118,19 +125,10 @@ impl<'a> Type<'a> {
         &self.0
     }
     fn shift0(&self, delta: isize, label: &Label) -> Self {
-        use TypeInternal::*;
-        Type(match &self.0 {
-            Expr(e) => Expr(Box::new(e.shift0(delta, label))),
-            Pi(ctx, c, x, t, e) => Pi(
-                ctx.clone(),
-                *c,
-                x.clone(),
-                Box::new(t.shift0(delta, label)),
-                Box::new(e.shift0(delta, label)),
-            ),
-            Const(c) => Const(*c),
-            SuperType => SuperType,
-        })
+        Type(self.0.shift0(delta, label))
+    }
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        Type(self.0.shift(delta, var))
     }
 
     fn const_sort() -> Self {
@@ -192,6 +190,24 @@ impl<'a> TypeInternal<'a> {
             )),
         }
     }
+    fn shift0(&self, delta: isize, label: &Label) -> Self {
+        self.shift(delta, &V(label.clone(), 0))
+    }
+    fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        use TypeInternal::*;
+        match self {
+            Expr(e) => Expr(Box::new(e.shift(delta, var))),
+            Pi(ctx, c, x, t, e) => Pi(
+                ctx.clone(),
+                *c,
+                x.clone(),
+                Box::new(t.shift(delta, var)),
+                Box::new(e.shift(delta, &var.shift0(1, x))),
+            ),
+            Const(c) => Const(*c),
+            SuperType => SuperType,
+        }
+    }
 }
 
 #[derive(Debug, Clone)]
-- 
cgit v1.2.3