summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--dhall/src/semantics/core/value.rs76
-rw-r--r--dhall/src/semantics/core/var.rs6
2 files changed, 74 insertions, 8 deletions
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<V> ValueKind<V> {
}
}
-// #[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<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.iter().cloned().chain(Some(binder)).collect(),
+ ),
+ },
+ )
+ }
+
+ fn lookup(ctx: &Vec<&Binder>, binder: &Binder) -> Option<usize> {
+ 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<Self> {
@@ -593,10 +654,9 @@ 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 {
- *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()