From 752c81a166489694245bbc2ec19754998320e70c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 May 2016 12:50:28 -0700
Subject: [PATCH] fix(library/compiler/nat_value): add expand method, otherwise
 we may fail to type check terms using nat_value_macro

---
 src/library/compiler/nat_value.cpp  | 24 ++++++++++++++++++++++--
 src/library/compiler/preprocess.cpp |  4 ++--
 2 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/src/library/compiler/nat_value.cpp b/src/library/compiler/nat_value.cpp
index dee1e7175a..ac64f41f57 100644
--- a/src/library/compiler/nat_value.cpp
+++ b/src/library/compiler/nat_value.cpp
@@ -26,9 +26,29 @@ public:
     virtual expr check_type(expr const &, abstract_type_context &, bool) const {
         return *g_nat;
     }
-    virtual optional<expr> expand(expr const &, abstract_type_context &) const {
-        return none_expr();
+
+    static expr convert(mpz const & n, expr const & one, expr const & add) {
+        if (n == 0) {
+            return mk_constant(get_nat_zero_name());
+        } else if (n == 1) {
+            return one;
+        } else {
+            expr r = convert(n/2, one, add);
+            r = mk_app(add, r, r);
+            if (n % mpz(2) == 1)
+                return mk_app(add, r, one);
+            else
+                return r;
+        }
     }
+
+    virtual optional<expr> expand(expr const &, abstract_type_context &) const {
+        expr one = mk_app(mk_constant(get_nat_succ_name()), mk_constant(get_nat_zero_name()));
+        expr add = mk_constant(get_nat_add_name());
+        expr r = convert(m_value, one, add);
+        return optional<expr>(r);
+    }
+
     virtual unsigned trust_level() const { return 0; }
     virtual bool operator==(macro_definition_cell const & other) const {
         nat_value_macro const * other_ptr = dynamic_cast<nat_value_macro const *>(&other);
diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp
index b5a1b57d04..37762a557d 100644
--- a/src/library/compiler/preprocess.cpp
+++ b/src/library/compiler/preprocess.cpp
@@ -121,10 +121,10 @@ public:
         v = expand_aux_recursors(m_env, v);
         lean_assert(check(d, v));
         lean_trace(name({"compiler", "expand_aux_recursors"}), tout() << "\n" << v << "\n";)
-        v = find_nat_values(m_env, v);
-        lean_assert(check(d, v));
         v = mark_comp_irrelevant_subterms(m_env, v);
         lean_assert(check(d, v));
+        v = find_nat_values(m_env, v);
+        lean_assert(check(d, v));
         v = eta_expand(m_env, v);
         lean_assert(check(d, v));
         lean_trace(name({"compiler", "eta_expansion"}), tout() << "\n" << v << "\n";)