From 4dc195c8d8a2ef03621fb73d15df2c66ad68be2c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 18:28:33 +0000 Subject: Use binder ids for Value equality --- dhall/src/semantics/core/value.rs | 76 ++++++++++++++++++++++++++++++++++----- dhall/src/semantics/core/var.rs | 6 ++++ 2 files changed, 74 insertions(+), 8 deletions(-) (limited to 'dhall') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 687fcfe..9b64bd2 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -1,3 +1,4 @@ +use std::borrow::Cow; use std::cell::{Ref, RefCell, RefMut}; use std::collections::HashMap; use std::rc::Rc; @@ -408,13 +409,73 @@ impl ValueKind { } } -// #[allow(dead_code)] -// fn equiv(x: &Value, y:&Value) -> bool { -// let map = |kind| { +/// 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, Vec<&'v Binder>>, + } + 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<'v, 'c>( + ctx: &'c Vec<&'v Binder>, + kind: &'v ValueKind, + ) -> ValueKind> { + kind.map_ref_with_special_handling_of_binders( + |val| ValueWithCtx { + val, + ctx: Cow::Borrowed(ctx), + }, + |binder, val| ValueWithCtx { + val, + ctx: Cow::Owned( + ctx.iter().cloned().chain(Some(binder)).collect(), + ), + }, + ) + } + + fn lookup(ctx: &Vec<&Binder>, binder: &Binder) -> Option { + ctx.iter() + .rev() + .enumerate() + .find(|(_, other)| binder.same_binder(other)) + .map(|(i, _)| i) + } -// }; -// map(x) == map(y) -// } + fn equiv_with_ctx<'v, 'c>( + ctx1: &'c Vec<&'v Binder>, + val1: &'v Value, + ctx2: &'c Vec<&'v Binder>, + 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 (lookup(ctx1, &b1), lookup(ctx2, &b2)) { + (Some(i), Some(j)) => i == j, + _ => false, + } + } else { + push_context(ctx1, &*kind1) == push_context(ctx2, &*kind2) + } + } + + equiv_with_ctx(&Vec::new(), val1, &Vec::new(), val2) +} impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { @@ -593,10 +654,9 @@ impl Subst for ValueKind { } } -// TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { - *self.as_whnf() == *other.as_whnf() + equiv(self, other) } } impl std::cmp::Eq for Value {} diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index 98b315e..4245e40 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -72,12 +72,18 @@ impl AlphaVar { self.normal.clone() } } + pub(crate) fn binder(&self) -> Binder { + Binder::new(self.normal.0.clone(), self.binder_uid) + } } impl Binder { pub(crate) fn new(name: Label, uid: BinderUID) -> Self { Binder { name, uid } } + pub(crate) fn same_binder(&self, other: &Binder) -> bool { + self.uid == other.uid + } pub(crate) fn to_label_maybe_alpha(&self, alpha: bool) -> Label { if alpha { "_".into() -- cgit v1.2.3