From 3881d36335fca6d72b0dd447130d6c1ce7ccbfee Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 17 Jan 2020 18:19:33 +0000
Subject: Implement bulk shifting

---
 dhall/src/semantics/core/context.rs | 57 ++++++++++++---------
 dhall/src/semantics/core/value.rs   | 98 +++++++++++++++++++++++++++++--------
 dhall/src/semantics/core/var.rs     | 16 +++---
 dhall/src/semantics/core/visitor.rs | 26 ++++++----
 dhall/src/syntax/ast/expr.rs        | 33 +++++++++++--
 5 files changed, 163 insertions(+), 67 deletions(-)

(limited to 'dhall')

diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index a6ab79e..f8d6ff0 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -40,32 +40,43 @@ impl TyCtx {
     }
     pub fn lookup(&self, var: &V<Label>) -> Option<Value> {
         let mut var = var.clone();
-        let mut shift_map: HashMap<Label, _> = HashMap::new();
-        for (b, i) in self.ctx.iter().rev() {
-            let l = b.to_label();
-            match var.over_binder(&l) {
-                None => {
-                    return Some(match i {
-                        CtxItem::Kept(newvar, t) => Value::from_kind_and_type(
-                            ValueKind::Var(
-                                newvar.under_multiple_binders(&shift_map),
-                            ),
-                            t.under_multiple_binders(&shift_map),
-                        ),
-                        CtxItem::Replaced(v) => {
-                            v.under_multiple_binders(&shift_map)
-                        }
-                    });
+        let mut shift_map: HashMap<Label, usize> = HashMap::new();
+        let mut rev_ctx = self.ctx.iter().rev().map(|(b, i)| (b.to_label(), i));
+
+        let found_item = loop {
+            if let Some((label, item)) = rev_ctx.next() {
+                var = match var.over_binder(&label) {
+                    Some(newvar) => newvar,
+                    None => break item,
+                };
+                if let CtxItem::Kept(_, _) = item {
+                    *shift_map.entry(label).or_insert(0) += 1;
                 }
-                Some(newvar) => var = newvar,
-            };
-            if let CtxItem::Kept(_, _) = i {
-                *shift_map.entry(l).or_insert(0) += 1;
+            } else {
+                // Unbound variable
+                return None;
             }
-        }
-        // Unbound variable
-        None
+        };
+
+        let v = match found_item {
+            CtxItem::Kept(newvar, t) => Value::from_kind_and_type(
+                ValueKind::Var(newvar.clone()),
+                t.clone(),
+            ),
+            CtxItem::Replaced(v) => v.clone(),
+        };
+
+        let v = v.under_multiple_binders(&shift_map);
+        // for (x, n) in shift_map {
+        //     let x: AlphaVar = (&x).into();
+        //     // Can't fail since delta is positive
+        //     v = v.shift(n as isize, &x).unwrap();
+        // }
+        return Some(v);
     }
+    // pub fn lookup_alpha(&self, var: &AlphaVar) -> Option<Value> {
+    //     self.lookup(&var.normal)
+    // }
     pub fn new_binder(&self, l: &Label) -> Binder {
         Binder::new(l.clone())
     }
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 049c2a9..5aa337d 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -240,7 +240,7 @@ impl Value {
     }
 
     pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(self.0.borrow().shift(delta, var)?.into_value())
+        Some(self.as_internal().shift(delta, var)?.into_value())
     }
     pub(crate) fn over_binder<T>(&self, x: T) -> Option<Self>
     where
@@ -258,16 +258,10 @@ impl Value {
     pub(crate) fn under_multiple_binders(
         &self,
         shift_map: &HashMap<Label, usize>,
-    ) -> Self
-    where
-        Self: Clone,
-    {
-        let mut v = self.clone();
-        for (x, n) in shift_map {
-            // Can't fail since delta is positive
-            v = v.shift(*n as isize, &x.into()).unwrap();
-        }
-        v
+    ) -> Self {
+        self.as_internal()
+            .under_multiple_binders(shift_map)
+            .into_value()
     }
     pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         match &*self.as_kind() {
@@ -279,9 +273,30 @@ impl Value {
                 }
                 val.clone()
             }
-            _ => self.0.borrow().subst_shift(var, val).into_value(),
+            _ => self.as_internal().subst_shift(var, val).into_value(),
         }
     }
+    // pub(crate) fn subst_ctx(&self, ctx: &TyCtx) -> Self {
+    //     match &*self.as_kind() {
+    //         ValueKind::Var(var) => match ctx.lookup_alpha(var) {
+    //             Some(val) => val,
+    //             None => unreachable!("Internal type error"),
+    //         },
+    //         kind => {
+    //             let kind = kind.map_ref_with_special_handling_of_binders(
+    //                 |x| x.subst_ctx(ctx),
+    //                 |b, t, x| x.subst_ctx(&ctx.insert_type(b, t.clone())),
+    //             );
+    //             ValueInternal {
+    //                 form: Unevaled,
+    //                 kind,
+    //                 ty: self.as_internal().ty.clone(),
+    //                 span: self.as_internal().span.clone(),
+    //             }
+    //             .into_value()
+    //         }
+    //     }
+    // }
 }
 
 impl ValueInternal {
@@ -343,7 +358,7 @@ impl ValueInternal {
         }
     }
 
-    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(ValueInternal {
             form: self.form,
             kind: self.kind.shift(delta, var)?,
@@ -354,7 +369,21 @@ impl ValueInternal {
             span: self.span.clone(),
         })
     }
-    pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+    fn under_multiple_binders(
+        &self,
+        shift_map: &HashMap<Label, usize>,
+    ) -> Self {
+        ValueInternal {
+            form: self.form,
+            kind: self.kind.under_multiple_binders(shift_map),
+            ty: match &self.ty {
+                None => None,
+                Some(ty) => Some(ty.under_multiple_binders(shift_map)),
+            },
+            span: self.span.clone(),
+        }
+    }
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         ValueInternal {
             // The resulting value may not stay in wnhf after substitution
             form: Unevaled,
@@ -449,17 +478,40 @@ impl ValueKind<Value> {
             ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?),
             _ => self.traverse_ref_with_special_handling_of_binders(
                 |x| Ok(x.shift(delta, var)?),
-                |b, x| Ok(x.shift(delta, &var.under_binder(b))?),
+                |b, _, x| Ok(x.shift(delta, &var.under_binder(b))?),
             )?,
         })
     }
+    #[allow(dead_code)]
+    fn under_multiple_binders(
+        &self,
+        shift_map: &HashMap<Label, usize>,
+    ) -> Self {
+        match self {
+            ValueKind::Var(v) => {
+                ValueKind::Var(v.under_multiple_binders(shift_map))
+            }
+            _ => self.map_ref_with_special_handling_of_binders(
+                |v| v.under_multiple_binders(shift_map),
+                |b, _, v| {
+                    let mut v = v.clone();
+                    for (x, n) in shift_map {
+                        let x: AlphaVar = x.into();
+                        // Can't fail since delta is positive
+                        v = v.shift(*n as isize, &x.under_binder(b)).unwrap();
+                    }
+                    v
+                },
+            ),
+        }
+    }
     fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         match self {
             ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(),
-            ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()),
+            ValueKind::Var(v) => ValueKind::Var(v.over_binder(var).unwrap()),
             _ => self.map_ref_with_special_handling_of_binders(
                 |x| x.subst_shift(var, val),
-                |b, x| {
+                |b, _, x| {
                     x.subst_shift(&var.under_binder(b), &val.under_binder(b))
                 },
             ),
@@ -471,7 +523,11 @@ impl<V> ValueKind<V> {
     pub(crate) fn traverse_ref_with_special_handling_of_binders<'a, V2, E>(
         &'a self,
         visit_val: impl FnMut(&'a V) -> Result<V2, E>,
-        visit_under_binder: impl FnMut(&'a Binder, &'a V) -> Result<V2, E>,
+        visit_under_binder: impl for<'b> FnMut(
+            &'a Binder,
+            &'b V,
+            &'a V,
+        ) -> Result<V2, E>,
     ) -> Result<ValueKind<V2>, E> {
         use crate::semantics::visitor;
         use visitor::ValueKindVisitor;
@@ -485,12 +541,12 @@ impl<V> ValueKind<V> {
     pub(crate) fn map_ref_with_special_handling_of_binders<'a, V2>(
         &'a self,
         mut map_val: impl FnMut(&'a V) -> V2,
-        mut map_under_binder: impl FnMut(&'a Binder, &'a V) -> V2,
+        mut map_under_binder: impl for<'b> FnMut(&'a Binder, &'b V, &'a V) -> V2,
     ) -> ValueKind<V2> {
         use crate::syntax::trivial_result;
         trivial_result(self.traverse_ref_with_special_handling_of_binders(
             |x| Ok(map_val(x)),
-            |l, x| Ok(map_under_binder(l, x)),
+            |l, t, x| Ok(map_under_binder(l, t, x)),
         ))
     }
 
@@ -499,7 +555,7 @@ impl<V> ValueKind<V> {
         &'a self,
         map_val: impl Fn(&'a V) -> V2,
     ) -> ValueKind<V2> {
-        self.map_ref_with_special_handling_of_binders(&map_val, |_, x| {
+        self.map_ref_with_special_handling_of_binders(&map_val, |_, _, x| {
             map_val(x)
         })
     }
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 7c2c4de..d7666e3 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -40,19 +40,17 @@ impl AlphaVar {
         // Can't fail since delta is positive
         self.shift(1, &x.into()).unwrap()
     }
+    pub(crate) fn over_binder(&self, x: &AlphaVar) -> Option<Self> {
+        self.shift(-1, x)
+    }
     pub(crate) fn under_multiple_binders(
         &self,
         shift_map: &HashMap<Label, usize>,
-    ) -> Self
-    where
-        Self: Clone,
-    {
-        let mut v = self.clone();
-        for (x, n) in shift_map {
-            // Can't fail since delta is positive
-            v = v.shift(*n as isize, &x.into()).unwrap();
+    ) -> Self {
+        AlphaVar {
+            normal: self.normal.under_multiple_binders(shift_map),
+            alpha: self.alpha.under_multiple_binders(shift_map),
         }
-        v
     }
 }
 
diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs
index 2c9ba92..e61a649 100644
--- a/dhall/src/semantics/core/visitor.rs
+++ b/dhall/src/semantics/core/visitor.rs
@@ -10,12 +10,13 @@ pub(crate) trait ValueKindVisitor<'a, V1, V2>: Sized {
     type Error;
 
     fn visit_val(&mut self, val: &'a V1) -> Result<V2, Self::Error>;
-    fn visit_val_under_binder(
+    fn visit_binder(
         mut self,
         _label: &'a Binder,
+        ty: &'a V1,
         val: &'a V1,
-    ) -> Result<V2, Self::Error> {
-        self.visit_val(val)
+    ) -> Result<(V2, V2), Self::Error> {
+        Ok((self.visit_val(ty)?, self.visit_val(val)?))
     }
     fn visit_vec(&mut self, x: &'a [V1]) -> Result<Vec<V2>, Self::Error> {
         x.iter().map(|e| self.visit_val(e)).collect()
@@ -72,10 +73,12 @@ where
     use ValueKind::*;
     Ok(match input {
         Lam(l, t, e) => {
-            Lam(l.clone(), v.visit_val(t)?, v.visit_val_under_binder(l, e)?)
+            let (t, e) = v.visit_binder(l, t, e)?;
+            Lam(l.clone(), t, e)
         }
         Pi(l, t, e) => {
-            Pi(l.clone(), v.visit_val(t)?, v.visit_val_under_binder(l, e)?)
+            let (t, e) = v.visit_binder(l, t, e)?;
+            Pi(l.clone(), t, e)
         }
         AppliedBuiltin(b, xs) => AppliedBuiltin(*b, v.visit_vec(xs)?),
         Var(v) => Var(v.clone()),
@@ -117,18 +120,21 @@ impl<'a, V1, V2, Err, F1, F2> ValueKindVisitor<'a, V1, V2>
 where
     V1: 'a,
     F1: FnMut(&'a V1) -> Result<V2, Err>,
-    F2: FnOnce(&'a Binder, &'a V1) -> Result<V2, Err>,
+    F2: for<'b> FnOnce(&'a Binder, &'b V1, &'a V1) -> Result<V2, Err>,
 {
     type Error = Err;
 
     fn visit_val(&mut self, val: &'a V1) -> Result<V2, Self::Error> {
         (self.visit_val)(val)
     }
-    fn visit_val_under_binder(
-        self,
+    fn visit_binder<'b>(
+        mut self,
         label: &'a Binder,
+        ty: &'a V1,
         val: &'a V1,
-    ) -> Result<V2, Self::Error> {
-        (self.visit_under_binder)(label, val)
+    ) -> Result<(V2, V2), Self::Error> {
+        let val = (self.visit_under_binder)(label, ty, val)?;
+        let ty = (self.visit_val)(ty)?;
+        Ok((ty, val))
     }
 }
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 04b5adc..2372b0a 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -1,3 +1,5 @@
+use std::collections::HashMap;
+
 use crate::syntax::map::{DupTreeMap, DupTreeSet};
 use crate::syntax::visitor::{self, ExprKindMutVisitor, ExprKindVisitor};
 use crate::syntax::*;
@@ -302,7 +304,7 @@ impl<E> Expr<E> {
 }
 
 impl<Label: PartialEq + Clone> V<Label> {
-    pub fn shift(&self, delta: isize, var: &V<Label>) -> Option<Self> {
+    pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Option<Self> {
         let V(x, n) = var;
         let V(y, m) = self;
         Some(if x == y && n <= m {
@@ -312,11 +314,35 @@ impl<Label: PartialEq + Clone> V<Label> {
         })
     }
 
-    pub fn over_binder(&self, x: &Label) -> Option<Self> {
+    pub(crate) fn over_binder(&self, x: &Label) -> Option<Self> {
         self.shift(-1, &V(x.clone(), 0))
     }
 }
 
+impl V<Label> {
+    pub(crate) fn under_multiple_binders(
+        &self,
+        shift_map: &HashMap<Label, usize>,
+    ) -> Self {
+        let name = &self.0;
+        let idx = self.1 + shift_map.get(name).unwrap_or(&0);
+        V(name.clone(), idx)
+    }
+}
+
+impl V<()> {
+    pub(crate) fn under_multiple_binders(
+        &self,
+        shift_map: &HashMap<Label, usize>,
+    ) -> Self {
+        let mut idx = self.1;
+        for (_, n) in shift_map {
+            idx += n;
+        }
+        V((), idx)
+    }
+}
+
 pub fn trivial_result<T>(x: Result<T, !>) -> T {
     match x {
         Ok(x) => x,
@@ -363,8 +389,7 @@ impl From<NaiveDouble> for f64 {
     }
 }
 
-/// This is only for the specific `Label` type, not generic
-impl From<Label> for V<Label> {
+impl<Label> From<Label> for V<Label> {
     fn from(x: Label) -> V<Label> {
         V(x, 0)
     }
-- 
cgit v1.2.3