From 95447deea3c00f1bb777cc6130d717d19fc8a35c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 4 Aug 2013 14:54:33 -0700
Subject: [PATCH] Add normalization a = b for values (aka semantic attachments)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/normalize.cpp   |  3 ++-
 src/tests/kernel/arith.cpp | 10 ++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/kernel/normalize.cpp b/src/kernel/normalize.cpp
index 9dd87f2c39..325182146b 100644
--- a/src/kernel/normalize.cpp
+++ b/src/kernel/normalize.cpp
@@ -169,8 +169,9 @@ class normalize_fn {
             expr new_r = reify(normalize(eq_rhs(a), s, k), k);
             if (new_l == new_r) {
                 return svalue(bool_value(true));
+            } else if (is_value(new_l) && is_value(new_r)) {
+                return svalue(bool_value(false));
             } else {
-                // TODO: Invoke semantic attachments.
                 return svalue(eq(new_l, new_r));
             }
         }
diff --git a/src/tests/kernel/arith.cpp b/src/tests/kernel/arith.cpp
index f9d7864a03..c94676d656 100644
--- a/src/tests/kernel/arith.cpp
+++ b/src/tests/kernel/arith.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "environment.h"
 #include "type_check.h"
+#include "builtin.h"
 #include "arith.h"
 #include "normalize.h"
 #include "abstract.h"
@@ -74,11 +75,20 @@ static void tst4() {
     lean_assert(normalize(e2, env) == fun("a", int_type(), app(int_sub(), constant("a"), int_value(-20))));
 }
 
+static void tst5() {
+    environment env;
+    expr e = eq(int_value(3), int_value(4));
+    std::cout << e << " --> " << normalize(e, env) << "\n";
+    lean_assert(normalize(e, env) == bool_value(false));
+    lean_assert(normalize(eq(constant("a"), int_value(3)), env) == eq(constant("a"), int_value(3)));
+}
+
 int main() {
     continue_on_violation(true);
     tst1();
     tst2();
     tst3();
     tst4();
+    tst5();
     return has_violations() ? 1 : 0;
 }