From 0cf4d3845e75ac25e35c5e73eb2dfd58c5450af6 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 6 Apr 2019 11:09:23 +0200
Subject: Factor out shift/subst/shift dance

---
 dhall/src/normalize.rs | 13 +++----------
 dhall/src/typecheck.rs |  5 +----
 2 files changed, 4 insertions(+), 14 deletions(-)

(limited to 'dhall')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 7574c2f..24a8601 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -217,13 +217,8 @@ where
     let what_next = match &expr {
         Let(f, _, r, b) => {
             let vf0 = &V(f.clone(), 0);
-            let r2 = shift(1, vf0, &r.roll());
             // TODO: use a context
-            let b2 = subst(vf0, &r2, &b.roll());
-            // TODO: add tests sensitive to shift errors before
-            // trying anything
-            let b3 = shift(-1, vf0, &b2);
-            ContinueSub(b3)
+            ContinueSub(subst_shift(vf0, &r.roll(), &b.roll()))
         }
         Annot(x, _) => DoneRef(x),
         Note(_, e) => DoneRef(e),
@@ -243,10 +238,8 @@ where
             let a = iter.next().unwrap();
             // Beta reduce
             let vx0 = &V(x.clone(), 0);
-            let a2 = shift(1, vx0, &a.roll());
-            let b2 = subst(vx0, &a2, &b);
-            let b3 = shift(-1, vx0, &b2);
-            Continue(App(b3, iter.map(ExprF::roll).collect()))
+            let b2 = subst_shift(vx0, &a.roll(), &b);
+            Continue(App(b2, iter.map(ExprF::roll).collect()))
         }
         BoolIf(BoolLit(true), t, _) => DoneRef(t),
         BoolIf(BoolLit(false), _, f) => DoneRef(f),
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 75e6e1d..145de63 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -268,10 +268,7 @@ where
             let tA2 = normalized_type_with(ctx, a.clone())?;
             if prop_equal(tA.as_ref(), tA2.as_ref()) {
                 let vx0 = &V(x.clone(), 0);
-                let a2 = shift(1, vx0, a);
-                let tB2 = subst(vx0, &a2, &tB);
-                let tB3 = shift(-1, vx0, &tB2);
-                return Ok(tB3);
+                return Ok(subst_shift(vx0, &a, &tB));
             } else {
                 Err(mkerr(TypeMismatch(f.clone(), tA, a.clone(), tA2)))
             }
-- 
cgit v1.2.3