Start rewriting value comparison

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 {