diff options
Diffstat (limited to 'dhall')
| -rw-r--r-- | dhall/src/semantics/core/value.rs | 107 |
1 files changed, 107 insertions, 0 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index a19cb02..35913cf 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -692,12 +692,119 @@ impl Closure { pub fn apply(&self, val: Value) -> Value { self.body.normalize_whnf(&self.env.insert_value(val)) } + pub fn apply_fresh(&self, env: QuoteEnv) -> Value { + let val = Value::from_kind_and_type( + ValueKind::Var(AlphaVar::default(), NzVar::new(env.size())), + self.arg_ty.clone(), + ); + self.apply(val) + } pub fn normalize(&self) -> Value { self.body .normalize_whnf(&self.env.insert_type(self.arg_ty.clone())) } } +/// 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 ValueWithEnv<'v> { + val: &'v Value, + env: QuoteEnv, + } + impl<'v> PartialEq for ValueWithEnv<'v> { + fn eq(&self, other: &ValueWithEnv<'v>) -> bool { + equiv_with_env(self.env, self.val, other.env, 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>( + env: QuoteEnv, + kind: &'v ValueKind<Value>, + ) -> ValueKind<ValueWithEnv<'v>> { + kind.map_ref_with_special_handling_of_binders( + |val| ValueWithEnv { val, env }, + |_, _, val| ValueWithEnv { + val, + env: env.insert(), + }, + ) + } + + fn equiv_with_env<'v>( + env1: QuoteEnv, + val1: &'v Value, + env2: QuoteEnv, + val2: &'v Value, + ) -> bool { + use ValueKind::Var; + let kind1 = val1.as_whnf(); + let kind2 = val2.as_whnf(); + match (&*kind1, &*kind2) { + (Var(_, v1), Var(_, v2)) => { + v1 == v2 + // match (env1.lookup(v1), env2.lookup(v2)) { + // // Both vars were found in the environment, check they point to the same + // // binder. + // // Does that even make any sense with an incomplete environment ? + // // I have no clue what I'm doing anymore. + // (Some(i), Some(j)) => i == j, + // // Both vars point to outside the environment ???? + // // (None, None) => v1 == v2, + // _ => false, + // } + } + // (Var(_, v1), Var(_, v2)) => env1.lookup(v1) == env2.lookup(v2), + ( + ValueKind::LamClosure { + annot: a1, + closure: cl1, + .. + }, + ValueKind::LamClosure { + annot: a2, + closure: cl2, + .. + }, + ) => { + equiv_with_env(env1, a1, env2, a2) + && equiv_with_env( + env1.insert(), + &cl1.apply_fresh(env1), + env2.insert(), + &cl2.apply_fresh(env2), + ) + } + ( + ValueKind::PiClosure { + annot: a1, + closure: cl1, + .. + }, + ValueKind::PiClosure { + annot: a2, + closure: cl2, + .. + }, + ) => { + equiv_with_env(env1, a1, env2, a2) + && equiv_with_env( + env1.insert(), + &cl1.apply_fresh(env1), + env2.insert(), + &cl2.apply_fresh(env2), + ) + } + (k1, k2) => push_context(env1, k1) == push_context(env2, k2), + } + } + + // TODO: need to use ambiant env instead of creating new one + // Might be possible to generate free variables differently to avoid this + equiv_with_env(QuoteEnv::new(), val1, QuoteEnv::new(), val2) +} + // TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { |