Introduce a notion of binder

4 files changed, 42 insertions, 33 deletions

diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index ed63b63..3a7930e 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -3,7 +3,7 @@ use std::collections::HashMap;
 use crate::error::TypeError;
 use crate::semantics::core::value::Value;
 use crate::semantics::core::value::ValueKind;
-use crate::semantics::core::var::{AlphaVar, Shift, Subst};
+use crate::semantics::core::var::{AlphaVar, Binder, Shift, Subst};
 use crate::syntax::{Label, V};
 
 #[derive(Debug, Clone)]
@@ -14,22 +14,26 @@ enum CtxItem {
 
 #[derive(Debug, Clone)]
 pub(crate) struct TyCtx {
-    ctx: Vec<(Label, CtxItem)>,
+    ctx: Vec<(Binder, CtxItem)>,
 }
 
 impl TyCtx {
     pub fn new() -> Self {
         TyCtx { ctx: Vec::new() }
     }
-    fn with_vec(&self, vec: Vec<(Label, CtxItem)>) -> Self {
+    fn with_vec(&self, vec: Vec<(Binder, CtxItem)>) -> Self {
         TyCtx { ctx: vec }
     }
-    pub fn insert_type(&self, x: &Label, t: Value) -> Self {
+    pub fn insert_type(&self, x: &Binder, t: Value) -> Self {
         let mut vec = self.ctx.clone();
         vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x))));
         self.with_vec(vec)
     }
-    pub fn insert_value(&self, x: &Label, e: Value) -> Result<Self, TypeError> {
+    pub fn insert_value(
+        &self,
+        x: &Binder,
+        e: Value,
+    ) -> Result<Self, TypeError> {
         let mut vec = self.ctx.clone();
         vec.push((x.clone(), CtxItem::Replaced(e)));
         Ok(self.with_vec(vec))
@@ -37,8 +41,9 @@ 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 (l, i) in self.ctx.iter().rev() {
-            match var.over_binder(l) {
+        for (b, i) in self.ctx.iter().rev() {
+            let l = b.to_label();
+            match var.over_binder(&l) {
                 None => {
                     let i = i.under_multiple_binders(&shift_map);
                     return Some(match i {
@@ -51,12 +56,16 @@ impl TyCtx {
                 Some(newvar) => var = newvar,
             };
             if let CtxItem::Kept(_, _) = i {
-                *shift_map.entry(l.clone()).or_insert(0) += 1;
+                *shift_map.entry(l).or_insert(0) += 1;
             }
         }
         // Unbound variable
         None
     }
+    pub fn new_binder(&self, l: &Label) -> Binder {
+        Binder::new(l.clone())
+    }
+
     /// Given a var that makes sense in the current context, map the given function in such a way
     /// that the passed variable always makes sense in the context of the passed item.
     /// Once we pass the variable definition, the variable doesn't make sense anymore so we just
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index f7c2fbf..687fcfe 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
 
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::context::TyCtx;
-use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
+use crate::semantics::core::var::{AlphaVar, Binder, Shift, Subst};
 use crate::semantics::phase::normalize::{apply_any, normalize_whnf};
 use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value};
 use crate::semantics::phase::{Normalized, NormalizedExpr, Typed};
@@ -54,8 +54,8 @@ pub(crate) enum Form {
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) enum ValueKind<Value> {
     /// Closures
-    Lam(AlphaLabel, Value, Value),
-    Pi(AlphaLabel, Value, Value),
+    Lam(Binder, Value, Value),
+    Pi(Binder, Value, Value),
     // Invariant: in whnf, the evaluation must not be able to progress further.
     AppliedBuiltin(Builtin, Vec<Value>),
 
@@ -393,7 +393,7 @@ 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 AlphaLabel, &'a V) -> V2,
+        mut map_under_binder: impl FnMut(&'a Binder, &'a V) -> V2,
     ) -> ValueKind<V2> {
         use crate::semantics::visitor;
         use crate::syntax::trivial_result;
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 017a689..add0500 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -14,7 +14,9 @@ pub struct AlphaVar {
 // Exactly like a Label, but equality returns always true.
 // This is so that ValueKind equality is exactly alpha-equivalence.
 #[derive(Clone, Eq)]
-pub struct AlphaLabel(Label);
+pub struct Binder {
+    name: Label,
+}
 
 pub(crate) trait Shift: Sized {
     // Shift an expression to move it around binders without changing the meaning of its free
@@ -64,7 +66,10 @@ impl AlphaVar {
     }
 }
 
-impl AlphaLabel {
+impl Binder {
+    pub(crate) fn new(name: Label) -> Self {
+        Binder { name }
+    }
     pub(crate) fn to_label_maybe_alpha(&self, alpha: bool) -> Label {
         if alpha {
             "_".into()
@@ -92,7 +97,7 @@ impl std::cmp::PartialEq for AlphaVar {
         self.alpha == other.alpha
     }
 }
-impl std::cmp::PartialEq for AlphaLabel {
+impl std::cmp::PartialEq for Binder {
     fn eq(&self, _other: &Self) -> bool {
         true
     }
@@ -104,9 +109,9 @@ impl std::fmt::Debug for AlphaVar {
     }
 }
 
-impl std::fmt::Debug for AlphaLabel {
+impl std::fmt::Debug for Binder {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        write!(f, "AlphaLabel({})", &self.0)
+        write!(f, "Binder({})", &self.name)
     }
 }
 
@@ -123,26 +128,21 @@ impl<'a> From<&'a Label> for AlphaVar {
         x.clone().into()
     }
 }
-impl From<AlphaLabel> for AlphaVar {
-    fn from(x: AlphaLabel) -> AlphaVar {
+impl From<Binder> for AlphaVar {
+    fn from(x: Binder) -> AlphaVar {
         let l: Label = x.into();
         l.into()
     }
 }
-impl<'a> From<&'a AlphaLabel> for AlphaVar {
-    fn from(x: &'a AlphaLabel) -> AlphaVar {
+impl<'a> From<&'a Binder> for AlphaVar {
+    fn from(x: &'a Binder) -> AlphaVar {
         x.clone().into()
     }
 }
 
-impl From<Label> for AlphaLabel {
-    fn from(x: Label) -> AlphaLabel {
-        AlphaLabel(x)
-    }
-}
-impl From<AlphaLabel> for Label {
-    fn from(x: AlphaLabel) -> Label {
-        x.0
+impl From<Binder> for Label {
+    fn from(x: Binder) -> Label {
+        x.name
     }
 }
 impl Shift for () {
diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs
index c7cf79e..2c9ba92 100644
--- a/dhall/src/semantics/core/visitor.rs
+++ b/dhall/src/semantics/core/visitor.rs
@@ -1,6 +1,6 @@
 use std::iter::FromIterator;
 
-use crate::semantics::{AlphaLabel, ValueKind};
+use crate::semantics::{Binder, ValueKind};
 use crate::syntax::Label;
 
 /// A visitor trait that can be used to traverse `ValueKind`s. We need this pattern so that Rust lets
@@ -12,7 +12,7 @@ pub(crate) trait ValueKindVisitor<'a, V1, V2>: Sized {
     fn visit_val(&mut self, val: &'a V1) -> Result<V2, Self::Error>;
     fn visit_val_under_binder(
         mut self,
-        _label: &'a AlphaLabel,
+        _label: &'a Binder,
         val: &'a V1,
     ) -> Result<V2, Self::Error> {
         self.visit_val(val)
@@ -117,7 +117,7 @@ impl<'a, V1, V2, Err, F1, F2> ValueKindVisitor<'a, V1, V2>
 where
     V1: 'a,
     F1: FnMut(&'a V1) -> Result<V2, Err>,
-    F2: FnOnce(&'a AlphaLabel, &'a V1) -> Result<V2, Err>,
+    F2: FnOnce(&'a Binder, &'a V1) -> Result<V2, Err>,
 {
     type Error = Err;
 
@@ -126,7 +126,7 @@ where
     }
     fn visit_val_under_binder(
         self,
-        label: &'a AlphaLabel,
+        label: &'a Binder,
         val: &'a V1,
     ) -> Result<V2, Self::Error> {
         (self.visit_under_binder)(label, val)