From 654d752c65f0e221d225ed045a0aee62f223855e Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 27 Dec 2019 16:05:47 +0000
Subject: Introduce a notion of binder

---
 dhall/src/semantics/core/context.rs    | 25 +++++++++++++++++--------
 dhall/src/semantics/core/value.rs      |  8 ++++----
 dhall/src/semantics/core/var.rs        | 34 +++++++++++++++++-----------------
 dhall/src/semantics/core/visitor.rs    |  8 ++++----
 dhall/src/semantics/phase/typecheck.rs | 27 ++++++++++++++-------------
 5 files changed, 56 insertions(+), 46 deletions(-)

(limited to 'dhall/src')

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)
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 2e1cc02..926598d 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -4,11 +4,9 @@ use std::collections::HashMap;
 
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::context::TyCtx;
-use crate::semantics::core::value::Value;
-use crate::semantics::core::value::ValueKind;
-use crate::semantics::core::var::{Shift, Subst};
 use crate::semantics::phase::normalize::merge_maps;
 use crate::semantics::phase::Normalized;
+use crate::semantics::{Binder, Shift, Subst, Value, ValueKind};
 use crate::syntax;
 use crate::syntax::{
     Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span,
@@ -17,12 +15,12 @@ use crate::syntax::{
 
 fn tck_pi_type(
     ctx: &TyCtx,
-    x: Label,
+    binder: Binder,
     tx: Value,
     te: Value,
 ) -> Result<Value, TypeError> {
     use TypeMessage::*;
-    let ctx2 = ctx.insert_type(&x, tx.clone());
+    let ctx2 = ctx.insert_type(&binder, tx.clone());
 
     let ka = match tx.get_type()?.as_const() {
         Some(k) => k,
@@ -42,7 +40,7 @@ fn tck_pi_type(
     let k = function_check(ka, kb);
 
     Ok(Value::from_kind_and_type(
-        ValueKind::Pi(x.into(), tx, te),
+        ValueKind::Pi(binder, tx, te),
         Value::from_const(k),
     ))
 }
@@ -307,21 +305,23 @@ fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> {
 
     match e.as_ref() {
         Lam(var, annot, body) => {
+            let binder = ctx.new_binder(var);
             let annot = type_with(ctx, annot.clone())?;
             annot.normalize_nf();
-            let ctx2 = ctx.insert_type(var, annot.clone());
+            let ctx2 = ctx.insert_type(&binder, annot.clone());
             let body = type_with(&ctx2, body.clone())?;
             let body_type = body.get_type()?;
             Ok(Value::from_kind_and_type(
-                ValueKind::Lam(var.clone().into(), annot.clone(), body),
-                tck_pi_type(ctx, var.clone(), annot, body_type)?,
+                ValueKind::Lam(binder.clone(), annot.clone(), body),
+                tck_pi_type(ctx, binder, annot, body_type)?,
             ))
         }
         Pi(x, ta, tb) => {
+            let binder = ctx.new_binder(x);
             let ta = type_with(ctx, ta.clone())?;
-            let ctx2 = ctx.insert_type(x, ta.clone());
+            let ctx2 = ctx.insert_type(&binder, ta.clone());
             let tb = type_with(&ctx2, tb.clone())?;
-            tck_pi_type(ctx, x.clone(), ta, tb)
+            tck_pi_type(ctx, binder, ta, tb)
         }
         Let(x, t, v, e) => {
             let v = if let Some(t) = t {
@@ -331,7 +331,8 @@ fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> {
             };
 
             let v = type_with(ctx, v)?;
-            type_with(&ctx.insert_value(x, v.clone())?, e.clone())
+            let binder = ctx.new_binder(x);
+            type_with(&ctx.insert_value(&binder, v.clone())?, e.clone())
         }
         Embed(p) => Ok(p.clone().into_typed().into_value()),
         Var(var) => match ctx.lookup(&var) {
@@ -496,7 +497,7 @@ fn type_last_layer(
                                 RetTypeOnly(
                                     tck_pi_type(
                                         ctx,
-                                        x.clone(),
+                                        ctx.new_binder(x),
                                         t.clone(),
                                         r.under_binder(x),
                                     )?
-- 
cgit v1.2.3