From fc1d7b758008643447f17bc9d05adb128d1567cc Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 17 Jan 2020 10:25:28 +0000
Subject: Remove binder ids

The underlying purpose of them turned out to be unsound
---
 dhall/src/semantics/core/context.rs | 53 ++---------------------------
 dhall/src/semantics/core/value.rs   | 67 +++----------------------------------
 dhall/src/semantics/core/var.rs     | 32 +++++-------------
 dhall/src/semantics/to_expr.rs      | 23 ++-----------
 dhall/src/syntax/ast/expr.rs        |  9 +++++
 5 files changed, 28 insertions(+), 156 deletions(-)

(limited to 'dhall/src')

diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 826ba15..3a7930e 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -1,6 +1,4 @@
-use std::cell::RefCell;
 use std::collections::HashMap;
-use std::rc::Rc;
 
 use crate::error::TypeError;
 use crate::semantics::core::value::Value;
@@ -17,28 +15,14 @@ enum CtxItem {
 #[derive(Debug, Clone)]
 pub(crate) struct TyCtx {
     ctx: Vec<(Binder, CtxItem)>,
-    /// Keeps track of the next free binder id to assign. Shared among all the contexts to ensure
-    /// unicity across the expression.
-    next_uid: Rc<RefCell<u64>>,
-}
-
-#[derive(Debug, Clone)]
-pub(crate) struct VarCtx<'b> {
-    ctx: Vec<&'b Binder>,
 }
 
 impl TyCtx {
     pub fn new() -> Self {
-        TyCtx {
-            ctx: Vec::new(),
-            next_uid: Rc::new(RefCell::new(0)),
-        }
+        TyCtx { ctx: Vec::new() }
     }
     fn with_vec(&self, vec: Vec<(Binder, CtxItem)>) -> Self {
-        TyCtx {
-            ctx: vec,
-            next_uid: self.next_uid.clone(),
-        }
+        TyCtx { ctx: vec }
     }
     pub fn insert_type(&self, x: &Binder, t: Value) -> Self {
         let mut vec = self.ctx.clone();
@@ -79,10 +63,7 @@ impl TyCtx {
         None
     }
     pub fn new_binder(&self, l: &Label) -> Binder {
-        let mut next_uid = self.next_uid.borrow_mut();
-        let uid = *next_uid;
-        *next_uid += 1;
-        Binder::new(l.clone(), uid)
+        Binder::new(l.clone())
     }
 
     /// Given a var that makes sense in the current context, map the given function in such a way
@@ -133,34 +114,6 @@ impl TyCtx {
     }
 }
 
-impl<'b> VarCtx<'b> {
-    pub fn new() -> Self {
-        VarCtx { ctx: Vec::new() }
-    }
-    pub fn insert(&self, binder: &'b Binder) -> Self {
-        VarCtx {
-            ctx: self.ctx.iter().copied().chain(Some(binder)).collect(),
-        }
-    }
-    pub fn lookup(&self, binder: &Binder) -> Option<usize> {
-        self.ctx
-            .iter()
-            .rev()
-            .enumerate()
-            .find(|(_, other)| binder.same_binder(other))
-            .map(|(i, _)| i)
-    }
-    pub fn lookup_by_name(&self, binder: &Binder) -> Option<usize> {
-        self.ctx
-            .iter()
-            .rev()
-            .filter(|other| binder.name() == other.name())
-            .enumerate()
-            .find(|(_, other)| binder.same_binder(other))
-            .map(|(i, _)| i)
-    }
-}
-
 impl Shift for CtxItem {
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(match self {
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 26b8672..b4e4e61 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -1,10 +1,9 @@
-use std::borrow::Cow;
 use std::cell::{Ref, RefCell, RefMut};
 use std::collections::HashMap;
 use std::rc::Rc;
 
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::core::context::{TyCtx, VarCtx};
+use crate::semantics::core::context::TyCtx;
 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};
@@ -164,7 +163,7 @@ impl Value {
         &self,
         opts: to_expr::ToExprOptions,
     ) -> NormalizedExpr {
-        to_expr::value_to_expr(&VarCtx::new(), self, opts)
+        to_expr::value_to_expr(self, opts)
     }
     pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind<Value> {
         self.as_whnf().clone()
@@ -410,65 +409,6 @@ impl<V> ValueKind<V> {
     }
 }
 
-/// Compare two values for equality modulo alpha/beta-equivalence.
-// TODO: use Rc comparison to shortcut on identical pointers
-fn equiv(val1: &Value, val2: &Value) -> bool {
-    struct ValueWithCtx<'v, 'c> {
-        val: &'v Value,
-        ctx: Cow<'c, VarCtx<'v>>,
-    }
-    impl<'v, 'c> PartialEq for ValueWithCtx<'v, 'c> {
-        fn eq(&self, other: &ValueWithCtx<'v, 'c>) -> bool {
-            equiv_with_ctx(&*self.ctx, self.val, &*other.ctx, other.val)
-        }
-    }
-    // Push the given context into every subnode of the ValueKind. That way, normal equality of the
-    // resulting value will take into account the context.
-    fn push_context_through<'v, 'c>(
-        ctx: &'c VarCtx<'v>,
-        kind: &'v ValueKind<Value>,
-    ) -> ValueKind<ValueWithCtx<'v, 'c>> {
-        kind.map_ref_with_special_handling_of_binders(
-            |val| ValueWithCtx {
-                val,
-                ctx: Cow::Borrowed(ctx),
-            },
-            |binder, val| ValueWithCtx {
-                val,
-                ctx: Cow::Owned(ctx.insert(binder)),
-            },
-        )
-    }
-
-    fn equiv_with_ctx<'v, 'c>(
-        ctx1: &'c VarCtx<'v>,
-        val1: &'v Value,
-        ctx2: &'c VarCtx<'v>,
-        val2: &'v Value,
-    ) -> bool {
-        use ValueKind::Var;
-        let kind1 = val1.as_whnf();
-        let kind2 = val2.as_whnf();
-
-        if let (Var(v1), Var(v2)) = (&*kind1, &*kind2) {
-            let b1 = v1.binder();
-            let b2 = v2.binder();
-            if b1.same_binder(&b2) {
-                return true;
-            }
-            match (ctx1.lookup(&b1), ctx2.lookup(&b2)) {
-                (Some(i), Some(j)) => i == j,
-                _ => false,
-            }
-        } else {
-            push_context_through(ctx1, &*kind1)
-                == push_context_through(ctx2, &*kind2)
-        }
-    }
-
-    equiv_with_ctx(&VarCtx::new(), val1, &VarCtx::new(), val2)
-}
-
 impl Shift for Value {
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(Value(self.0.shift(delta, var)?))
@@ -646,9 +586,10 @@ impl Subst<Value> for ValueKind<Value> {
     }
 }
 
+// TODO: use Rc comparison to shortcut on identical pointers
 impl std::cmp::PartialEq for Value {
     fn eq(&self, other: &Self) -> bool {
-        equiv(self, other)
+        *self.as_whnf() == *other.as_whnf()
     }
 }
 impl std::cmp::Eq for Value {}
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index d21fa80..99d3125 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -9,21 +9,13 @@ use crate::syntax::{ExprKind, InterpolatedTextContents, Label, V};
 pub struct AlphaVar {
     normal: V<Label>,
     alpha: V<()>,
-    /// Id of the corresponding binder.
-    binder_uid: BinderUID,
 }
 
-type BinderUID = u64;
-
 // Exactly like a Label, but equality returns always true.
 // This is so that ValueKind equality is exactly alpha-equivalence.
 #[derive(Clone, Eq)]
 pub struct Binder {
     name: Label,
-    /// Id of the binder, unique across the current expression. Used to distinguish bindersinstead
-    /// of their name. The id won't actually be unique when there are imports around, but
-    /// typechecking ensures this can't cause a conflict.
-    uid: BinderUID,
 }
 
 pub(crate) trait Shift: Sized {
@@ -65,20 +57,18 @@ pub(crate) trait Subst<S> {
 }
 
 impl AlphaVar {
-    pub(crate) fn binder(&self) -> Binder {
-        Binder::new(self.normal.0.clone(), self.binder_uid)
+    pub(crate) fn to_var_maybe_alpha(&self, alpha: bool) -> V<Label> {
+        if alpha {
+            V("_".into(), self.alpha.idx())
+        } else {
+            self.normal.clone()
+        }
     }
 }
 
 impl Binder {
-    pub(crate) fn new(name: Label, uid: BinderUID) -> Self {
-        Binder { name, uid }
-    }
-    pub(crate) fn name(&self) -> &Label {
-        &self.name
-    }
-    pub(crate) fn same_binder(&self, other: &Binder) -> bool {
-        self.uid == other.uid
+    pub(crate) fn new(name: Label) -> Self {
+        Binder { name }
     }
     pub(crate) fn to_label_maybe_alpha(&self, alpha: bool) -> Label {
         if alpha {
@@ -97,7 +87,6 @@ impl Shift for AlphaVar {
         Some(AlphaVar {
             normal: self.normal.shift(delta, &var.normal)?,
             alpha: self.alpha.shift(delta, &var.alpha)?,
-            binder_uid: self.binder_uid,
         })
     }
 }
@@ -108,6 +97,7 @@ impl std::cmp::PartialEq for AlphaVar {
         self.alpha == other.alpha
     }
 }
+/// Equality up to alpha-equivalence
 impl std::cmp::PartialEq for Binder {
     fn eq(&self, _other: &Self) -> bool {
         true
@@ -131,18 +121,14 @@ impl<'a> From<&'a Label> for AlphaVar {
         AlphaVar {
             normal: V(x.clone(), 0),
             alpha: V((), 0),
-            // TODO: evil evil but only used in shift
-            binder_uid: 0,
         }
     }
 }
 impl From<Binder> for AlphaVar {
     fn from(x: Binder) -> AlphaVar {
-        let binder_uid = x.uid;
         AlphaVar {
             normal: V(x.into(), 0),
             alpha: V((), 0),
-            binder_uid,
         }
     }
 }
diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs
index 1ece1cc..1adfd49 100644
--- a/dhall/src/semantics/to_expr.rs
+++ b/dhall/src/semantics/to_expr.rs
@@ -1,9 +1,8 @@
-use crate::semantics::core::context::VarCtx;
 use crate::semantics::phase::typecheck::rc;
 use crate::semantics::phase::NormalizedExpr;
 use crate::semantics::{Value, ValueKind};
 use crate::syntax;
-use crate::syntax::{Builtin, ExprKind, V};
+use crate::syntax::{Builtin, ExprKind};
 
 /// Controls conversion from `Value` to `Expr`
 #[derive(Copy, Clone)]
@@ -16,7 +15,6 @@ pub(crate) struct ToExprOptions {
 
 /// Converts a value back to the corresponding AST expression.
 pub(crate) fn value_to_expr(
-    ctx: &VarCtx,
     val: &Value,
     opts: ToExprOptions,
 ) -> NormalizedExpr {
@@ -25,25 +23,10 @@ pub(crate) fn value_to_expr(
     }
 
     let kind = val.as_kind();
-    let kind = kind.map_ref_with_special_handling_of_binders(
-        |v| value_to_expr(ctx, v, opts),
-        |binder, v| value_to_expr(&ctx.insert(binder), v, opts),
-    );
+    let kind = kind.map_ref(|v| value_to_expr(v, opts));
     match kind {
         ValueKind::Var(v) => {
-            let b = v.binder();
-            let (idx, name) = if opts.alpha {
-                (ctx.lookup(&b), "_".into())
-            } else {
-                (ctx.lookup_by_name(&b), b.name().clone())
-            };
-            match idx {
-                Some(idx) => rc(ExprKind::Var(V(name, idx))),
-                None => panic!(
-                    "internal error: binder {:?} not found in environment",
-                    b
-                ),
-            }
+            rc(ExprKind::Var(v.to_var_maybe_alpha(opts.alpha)))
         }
         ValueKind::Lam(x, t, e) => {
             rc(ExprKind::Lam(x.to_label_maybe_alpha(opts.alpha), t, e))
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 376480f..0ac31a5 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -173,6 +173,15 @@ pub enum ExprKind<SubExpr, Embed> {
     Embed(Embed),
 }
 
+impl<Label> V<Label> {
+    pub(crate) fn name(&self) -> &Label {
+        &self.0
+    }
+    pub(crate) fn idx(&self) -> usize {
+        self.1
+    }
+}
+
 impl<SE, E> ExprKind<SE, E> {
     pub fn traverse_ref_with_special_handling_of_binders<'a, SE2, Err>(
         &'a self,
-- 
cgit v1.2.3