summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2020-01-17 10:25:28 +0000
committerNadrieril2020-01-17 10:28:37 +0000
commitfc1d7b758008643447f17bc9d05adb128d1567cc (patch)
treec782fd543a22c3ae7ff4d9f95dfbc7966e8e1899 /dhall
parent763a810358f15a8bac6973ac4b273f517729cc84 (diff)
Remove binder ids
The underlying purpose of them turned out to be unsound
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/context.rs53
-rw-r--r--dhall/src/semantics/core/value.rs67
-rw-r--r--dhall/src/semantics/core/var.rs32
-rw-r--r--dhall/src/semantics/to_expr.rs23
-rw-r--r--dhall/src/syntax/ast/expr.rs9
5 files changed, 28 insertions, 156 deletions
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,