From ecff0ecd47bb38937fb43e60b8d78ea92e2af01c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 21 Apr 2019 22:52:00 +0200
Subject: Prepare for interop between two contexts

---
 dhall_core/src/core.rs | 34 +++++++++++++++++++++-------------
 1 file changed, 21 insertions(+), 13 deletions(-)

(limited to 'dhall_core')

diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index fa6fca4..03974eb 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -468,15 +468,24 @@ fn add_ui(u: usize, i: isize) -> usize {
     }
 }
 
-/// Applies `shift` to a single var.
-/// The first var is the var to shift away from; the second is the variable to shift
-fn shift_var(delta: isize, var: &V<Label>, in_expr: &V<Label>) -> V<Label> {
-    let V(x, n) = var;
-    let V(y, m) = in_expr;
-    if x == y && n <= m {
-        V(y.clone(), add_ui(*m, delta))
-    } else {
-        V(y.clone(), *m)
+impl<Label: PartialEq + Clone> V<Label> {
+    pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        let V(x, n) = var;
+        let V(y, m) = self;
+        if x == y && n <= m {
+            V(y.clone(), add_ui(*m, delta))
+        } else {
+            V(y.clone(), *m)
+        }
+    }
+
+    pub fn shift0(&self, delta: isize, x: &Label) -> Self {
+        let V(y, m) = self;
+        if x == y {
+            V(y.clone(), add_ui(*m, delta))
+        } else {
+            V(y.clone(), *m)
+        }
     }
 }
 
@@ -492,12 +501,11 @@ pub fn shift<N, E>(
 ) -> SubExpr<N, E> {
     use crate::ExprF::*;
     match in_expr.as_ref() {
-        Var(v) => rc(Var(shift_var(delta, var, v))),
+        Var(v) => rc(Var(v.shift(delta, var))),
         _ => in_expr.map_subexprs_with_special_handling_of_binders(
             |e| shift(delta, var, e),
             |l: &Label, e| {
-                let vl = V(l.clone(), 0);
-                let newvar = shift_var(1, &vl, var);
+                let newvar = var.shift0(1, l);
                 shift(delta, &newvar, e)
             },
         ),
@@ -567,7 +575,7 @@ fn subst_shift_inner<N, E>(
     let actual_var = V(x.clone(), add_ui(*n, *dn));
     match in_expr.as_ref() {
         Var(v) if v == &actual_var => shift0_multiple(ctx, value),
-        Var(v) => rc(Var(shift_var(-1, &actual_var, v))),
+        Var(v) => rc(Var(v.shift(-1, &actual_var))),
         _ => in_expr.map_subexprs_with_special_handling_of_binders(
             |e| subst_shift_inner(ctx, var, value, e),
             |l: &Label, e| {
-- 
cgit v1.2.3


From 0f334c9d112e3ee961eb35c09c85140fdf2aa8f6 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 22 Apr 2019 00:08:46 +0200
Subject: Remove now obsolete subst_shift

---
 dhall_core/src/core.rs | 43 +------------------------------------------
 1 file changed, 1 insertion(+), 42 deletions(-)

(limited to 'dhall_core')

diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index 03974eb..72b42f8 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -520,7 +520,7 @@ pub fn shift0<N, E>(
     shift(delta, &V(label.clone(), 0), in_expr)
 }
 
-fn shift0_multiple<N, E>(
+pub fn shift0_multiple<N, E>(
     deltas: &HashMap<Label, isize>,
     in_expr: &SubExpr<N, E>,
 ) -> SubExpr<N, E> {
@@ -546,44 +546,3 @@ fn shift0_multiple_inner<N, E>(
         ),
     }
 }
-
-/// Substitute all occurrences of a variable with an expression, and
-/// removes the variable from the environment by shifting the indices
-/// of other variables appropriately.
-///
-/// ```text
-/// subst_shift(x, v, e) = ↑(-1, x, e[x := ↑(1, x, v)])
-/// ```
-///
-pub fn subst_shift<N, E>(
-    var: &V<Label>,
-    value: &SubExpr<N, E>,
-    in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E> {
-    subst_shift_inner(&HashMap::new(), var, value, in_expr)
-}
-
-fn subst_shift_inner<N, E>(
-    ctx: &HashMap<Label, isize>,
-    var: &V<Label>,
-    value: &SubExpr<N, E>,
-    in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E> {
-    use crate::ExprF::*;
-    let V(x, n) = var;
-    let dn = ctx.get(x).unwrap_or(&0);
-    let actual_var = V(x.clone(), add_ui(*n, *dn));
-    match in_expr.as_ref() {
-        Var(v) if v == &actual_var => shift0_multiple(ctx, value),
-        Var(v) => rc(Var(v.shift(-1, &actual_var))),
-        _ => in_expr.map_subexprs_with_special_handling_of_binders(
-            |e| subst_shift_inner(ctx, var, value, e),
-            |l: &Label, e| {
-                let mut ctx = ctx.clone();
-                let count = ctx.entry(l.clone()).or_insert(0);
-                *count += 1;
-                subst_shift_inner(&ctx, var, value, e)
-            },
-        ),
-    }
-}
-- 
cgit v1.2.3


From 5c16a75c6dc01bbd0bfe36be4a9b337a762632a8 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 29 Apr 2019 16:27:14 +0200
Subject: Properly substitute when typing App

---
 dhall_core/src/core.rs | 23 +++++++++++++++--------
 1 file changed, 15 insertions(+), 8 deletions(-)

(limited to 'dhall_core')

diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index 72b42f8..a20f6d1 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -433,6 +433,17 @@ impl<N, E> SubExpr<N, E> {
     {
         rc(self.as_ref().visit(&mut visitor::UnNoteVisitor))
     }
+
+    pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self {
+        match self.as_ref() {
+            ExprF::Var(v) if v == var => val.clone(),
+            ExprF::Var(v) => rc(ExprF::Var(v.shift(-1, var))),
+            _ => self.map_subexprs_with_special_handling_of_binders(
+                |e| e.subst_shift(var, val),
+                |x: &Label, e| e.subst_shift(&var.shift0(1, x), val),
+            ),
+        }
+    }
 }
 
 impl<N: Clone> SubExpr<N, X> {
@@ -499,15 +510,11 @@ pub fn shift<N, E>(
     var: &V<Label>,
     in_expr: &SubExpr<N, E>,
 ) -> SubExpr<N, E> {
-    use crate::ExprF::*;
     match in_expr.as_ref() {
-        Var(v) => rc(Var(v.shift(delta, var))),
+        ExprF::Var(v) => rc(ExprF::Var(v.shift(delta, var))),
         _ => in_expr.map_subexprs_with_special_handling_of_binders(
             |e| shift(delta, var, e),
-            |l: &Label, e| {
-                let newvar = var.shift0(1, l);
-                shift(delta, &newvar, e)
-            },
+            |x: &Label, e| shift(delta, &var.shift0(1, x), e),
         ),
     }
 }
@@ -540,8 +547,8 @@ fn shift0_multiple_inner<N, E>(
         }
         _ => in_expr.map_subexprs_with_special_handling_of_binders(
             |e| shift0_multiple_inner(ctx, deltas, e),
-            |l: &Label, e| {
-                shift0_multiple_inner(&ctx.insert(l.clone(), ()), deltas, e)
+            |x: &Label, e| {
+                shift0_multiple_inner(&ctx.insert(x.clone(), ()), deltas, e)
             },
         ),
     }
-- 
cgit v1.2.3


From 439947345ef52ce04a66b1d4fa9c05d2b6964fa1 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 29 Apr 2019 21:52:47 +0200
Subject: Don't shift by mutable ref

---
 dhall_core/src/core.rs | 26 +++++++++++++++++++-------
 1 file changed, 19 insertions(+), 7 deletions(-)

(limited to 'dhall_core')

diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index a20f6d1..54d7cee 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -434,6 +434,24 @@ impl<N, E> SubExpr<N, E> {
         rc(self.as_ref().visit(&mut visitor::UnNoteVisitor))
     }
 
+    /// `shift` is used by both normalization and type-checking to avoid variable
+    /// capture by shifting variable indices
+    /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
+    /// for details
+    pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+        match self.as_ref() {
+            ExprF::Var(v) => rc(ExprF::Var(v.shift(delta, var))),
+            _ => self.map_subexprs_with_special_handling_of_binders(
+                |e| e.shift(delta, var),
+                |x: &Label, e| e.shift(delta, &var.shift0(1, x)),
+            ),
+        }
+    }
+
+    pub fn shift0(&self, delta: isize, label: &Label) -> Self {
+        self.shift(delta, &V(label.clone(), 0))
+    }
+
     pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self {
         match self.as_ref() {
             ExprF::Var(v) if v == var => val.clone(),
@@ -510,13 +528,7 @@ pub fn shift<N, E>(
     var: &V<Label>,
     in_expr: &SubExpr<N, E>,
 ) -> SubExpr<N, E> {
-    match in_expr.as_ref() {
-        ExprF::Var(v) => rc(ExprF::Var(v.shift(delta, var))),
-        _ => in_expr.map_subexprs_with_special_handling_of_binders(
-            |e| shift(delta, var, e),
-            |x: &Label, e| shift(delta, &var.shift0(1, x), e),
-        ),
-    }
+    in_expr.shift(delta, var)
 }
 
 pub fn shift0<N, E>(
-- 
cgit v1.2.3


From 8a846a6b0af141b45e7f92da7ecad32c89d581f8 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 30 Apr 2019 21:13:00 +0200
Subject: Fix shifting. This completely destroys sharing so performance is
 dead.

---
 dhall_core/src/core.rs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'dhall_core')

diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index 54d7cee..ebd95e7 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -458,7 +458,9 @@ impl<N, E> SubExpr<N, E> {
             ExprF::Var(v) => rc(ExprF::Var(v.shift(-1, var))),
             _ => self.map_subexprs_with_special_handling_of_binders(
                 |e| e.subst_shift(var, val),
-                |x: &Label, e| e.subst_shift(&var.shift0(1, x), val),
+                |x: &Label, e| {
+                    e.subst_shift(&var.shift0(1, x), &val.shift0(1, x))
+                },
             ),
         }
     }
-- 
cgit v1.2.3


From 17ab417aeb5aea6cd21240a491607b9017194737 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 2 May 2019 17:18:52 +0200
Subject: Remove shift0

---
 dhall_core/src/core.rs | 40 +++++++++++++++++-----------------------
 1 file changed, 17 insertions(+), 23 deletions(-)

(limited to 'dhall_core')

diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index ebd95e7..3db07dd 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -62,6 +62,18 @@ pub enum Const {
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub struct V<Label>(pub Label, pub usize);
 
+// This is only for the specific `Label` type, not generic
+impl From<Label> for V<Label> {
+    fn from(x: Label) -> V<Label> {
+        V(x, 0)
+    }
+}
+impl<'a> From<&'a Label> for V<Label> {
+    fn from(x: &'a Label) -> V<Label> {
+        V(x.clone(), 0)
+    }
+}
+
 // Definition order must match precedence order for
 // pretty-printing to work correctly
 #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)]
@@ -443,15 +455,11 @@ impl<N, E> SubExpr<N, E> {
             ExprF::Var(v) => rc(ExprF::Var(v.shift(delta, var))),
             _ => self.map_subexprs_with_special_handling_of_binders(
                 |e| e.shift(delta, var),
-                |x: &Label, e| e.shift(delta, &var.shift0(1, x)),
+                |x: &Label, e| e.shift(delta, &var.shift(1, &x.into())),
             ),
         }
     }
 
-    pub fn shift0(&self, delta: isize, label: &Label) -> Self {
-        self.shift(delta, &V(label.clone(), 0))
-    }
-
     pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self {
         match self.as_ref() {
             ExprF::Var(v) if v == var => val.clone(),
@@ -459,7 +467,10 @@ impl<N, E> SubExpr<N, E> {
             _ => self.map_subexprs_with_special_handling_of_binders(
                 |e| e.subst_shift(var, val),
                 |x: &Label, e| {
-                    e.subst_shift(&var.shift0(1, x), &val.shift0(1, x))
+                    e.subst_shift(
+                        &var.shift(1, &x.into()),
+                        &val.shift(1, &x.into()),
+                    )
                 },
             ),
         }
@@ -509,15 +520,6 @@ impl<Label: PartialEq + Clone> V<Label> {
             V(y.clone(), *m)
         }
     }
-
-    pub fn shift0(&self, delta: isize, x: &Label) -> Self {
-        let V(y, m) = self;
-        if x == y {
-            V(y.clone(), add_ui(*m, delta))
-        } else {
-            V(y.clone(), *m)
-        }
-    }
 }
 
 /// `shift` is used by both normalization and type-checking to avoid variable
@@ -533,14 +535,6 @@ pub fn shift<N, E>(
     in_expr.shift(delta, var)
 }
 
-pub fn shift0<N, E>(
-    delta: isize,
-    label: &Label,
-    in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E> {
-    shift(delta, &V(label.clone(), 0), in_expr)
-}
-
 pub fn shift0_multiple<N, E>(
     deltas: &HashMap<Label, isize>,
     in_expr: &SubExpr<N, E>,
-- 
cgit v1.2.3