From a02ea6b751b0c15d0f26bd0ea35bfaf008f25c58 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Tue, 18 Jul 2017 22:53:03 +0100
Subject: [PATCH] Unfold macros using the full typechecker in normalize.

Fix #7. The problem (as I understand it) was that macros were expanded using a typechecker which didn't unfold (semireducible) definitions, which led to the macros not being unfolded correctly.
Many many many thanks to @gebner!
---
 src/library/definitional/projection.cpp |  2 +-
 src/library/normalize.cpp               | 10 ++++++++++
 tests/lean/run/7.hlean                  | 23 +++++++++++++++++++++++
 3 files changed, 34 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/7.hlean

diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp
index 64572d497..dc851677a 100644
--- a/src/library/definitional/projection.cpp
+++ b/src/library/definitional/projection.cpp
@@ -126,7 +126,7 @@ public:
                 return none_expr();
             buffer<expr> args;
             expr const & I = get_app_args(s_type, args);
-            if (!is_constant(I) || length(m_ps) != length(const_levels(I)))
+            if (!is_constant(I) || length(m_ps) != length(const_levels(I)) || const_name(I) != m_I_name)
                 return none_expr();
             expr r = instantiate_univ_params(m_val, m_ps, const_levels(I));
             args.push_back(new_s);
diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index 0fd21aa0b..754ba20e5 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -382,6 +382,16 @@ class normalize_fn {
         check_system("normalize");
         if (!m_pred(e))
             return e;
+        /* The following is an ugly hack to solve issue #7.
+            The problem was that the type of macros was not unfolded correctly,
+            and the type was used to figure out what the macro meant */
+        buffer<expr> args;
+        auto fn = get_app_args(e, args);
+        if (is_macro(fn)) {
+            if (auto fn2 = m_full_tc.expand_macro(fn)) {
+                e = mk_app(*fn2, args);
+            }
+        }
         auto w = m_tc.whnf(e);
         e = w.first;
         if (m_save_cnstrs)
diff --git a/tests/lean/run/7.hlean b/tests/lean/run/7.hlean
new file mode 100644
index 000000000..162bd5af5
--- /dev/null
+++ b/tests/lean/run/7.hlean
@@ -0,0 +1,23 @@
+open unit pointed eq bool
+
+structure foo (u v : unit) :=
+ (b : bool → bool)
+
+definition bar := foo star
+definition bar.mk  [constructor] : bar star := foo.mk star star (λx, tt)
+definition bar.mk2 [constructor] : bar star := bar.mk
+
+example : foo.b bar.mk2 ff = tt :=
+begin esimp end
+
+definition my_ppi_const [constructor] {A : Type*} (P : A → Type*) : ppi P :=
+ppi.mk (λa, pt) idp
+
+definition my_pconst [constructor] (A B : Type*) : ppi (λ(a : A), B) :=
+!my_ppi_const
+
+example {A : Type*} (P : A → Type*) (a : A) : ppi_gen.to_fun (my_ppi_const P) a = pt :=
+begin esimp, end
+
+example {A B : Type*} (a : A) : my_pconst A B a = pt :=
+begin esimp end