feat(library/compiler): better support for numeric constants

src/library/compiler/CMakeLists.txt

@@ -1,4 +1,4 @@
 add_library(compiler OBJECT util.cpp eta_expansion.cpp simp_pr1_rec.cpp preprocess.cpp
   compiler_step_visitor.cpp elim_recursors.cpp comp_irrelevant.cpp
   inliner.cpp rec_fn_macro.cpp erase_irrelevant.cpp reduce_arity.cpp
-  lambda_lifting.cpp simp_inductive.cpp vm_compiler.cpp init_module.cpp)
+  lambda_lifting.cpp simp_inductive.cpp nat_value.cpp vm_compiler.cpp init_module.cpp)

src/library/compiler/init_module.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/compiler/preprocess.h"
+#include "library/compiler/nat_value.h"
 #include "library/compiler/comp_irrelevant.h"
 #include "library/compiler/inliner.h"
 #include "library/compiler/rec_fn_macro.h"
@@ -15,6 +16,7 @@ Author: Leonardo de Moura
 namespace lean {
 void initialize_compiler_module() {
     initialize_preprocess();
+    initialize_nat_value();
     initialize_comp_irrelevant();
     initialize_inliner();
     initialize_rec_fn_macro();
@@ -29,6 +31,7 @@ void finalize_compiler_module() {
     finalize_rec_fn_macro();
     finalize_inliner();
     finalize_comp_irrelevant();
+    finalize_nat_value();
     finalize_preprocess();
 }
 }

src/library/compiler/nat_value.cpp

@@ -0,0 +1,86 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/numerics/mpz.h"
+#include "kernel/expr.h"
+#include "library/constants.h"
+#include "library/num.h"
+#include "library/compiler/compiler_step_visitor.h"
+
+namespace lean {
+static expr * g_nat        = nullptr;
+static name * g_nat_macro  = nullptr;
+
+/** \brief Auxiliary macro used during compilation */
+class nat_value_macro : public macro_definition_cell {
+    mpz m_value;
+public:
+    nat_value_macro(mpz const & v):m_value(v) {}
+    virtual bool lt(macro_definition_cell const & d) const {
+        return m_value < static_cast<nat_value_macro const &>(d).m_value;
+    }
+    virtual name get_name() const { return *g_nat_macro; }
+    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();
+    }
+    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);
+        return other_ptr && m_value == other_ptr->m_value;
+    }
+    virtual void display(std::ostream & out) const {
+        out << m_value;
+    }
+    virtual bool is_atomic_pp(bool, bool) const { return true; }
+    virtual unsigned hash() const { return m_value.hash(); }
+    virtual void write(serializer &) const { lean_unreachable(); }
+    mpz const & get_value() const { return m_value; }
+};
+
+expr mk_nat_value(mpz const & v) {
+    return mk_macro(macro_definition(new nat_value_macro(v)));
+}
+
+bool is_nat_value(expr const & e) {
+    return is_macro(e) && dynamic_cast<nat_value_macro const *>(macro_def(e).raw()) != nullptr;
+}
+
+mpz const & get_nat_value_value(expr const & e) {
+    lean_assert(is_nat_value(e));
+    return static_cast<nat_value_macro const *>(macro_def(e).raw())->get_value();
+}
+
+class find_nat_values_fn : public compiler_step_visitor {
+    expr visit_app(expr const & e) override {
+        if (optional<mpz> v = to_num(e)) {
+            expr type = ctx().whnf(ctx().infer(e));
+            if (is_constant(type, get_nat_name())) {
+                return mk_nat_value(*v);
+            }
+        }
+        return compiler_step_visitor::visit_app(e);
+    }
+public:
+    find_nat_values_fn(environment const & env):compiler_step_visitor(env) {}
+};
+
+expr find_nat_values(environment const & env, expr const & e) {
+    return find_nat_values_fn(env)(e);
+}
+
+void initialize_nat_value() {
+    g_nat_macro  = new name("nat_value_macro");
+    g_nat        = new expr(Const(get_nat_name()));
+}
+
+void finalize_nat_value() {
+    delete g_nat_macro;
+    delete g_nat;
+}
+}

src/library/compiler/nat_value.h

@@ -0,0 +1,23 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+
+namespace lean {
+/** \brief Replace nat numerals encoded using bit0, bit1, one with an auxiliary nat_value macro.
+    This macro wraps a mpz number. */
+expr find_nat_values(environment const & env, expr const & e);
+/** \brief Create a nat_value macro expression. This macro should only be used in the compiler. */
+expr mk_nat_value(mpz const & v);
+/** \brief Return true iff \c e is a nat_value macro expression. */
+bool is_nat_value(expr const & e);
+/** \brief Return the mpz stored in the nat_value macro.
+    \pre is_nat_value(e) */
+mpz const & get_nat_value_value(expr const & e);
+void initialize_nat_value();
+void finalize_nat_value();
+}

src/library/compiler/preprocess.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/compiler/util.h"
 #include "library/compiler/compiler_step_visitor.h"
 #include "library/compiler/comp_irrelevant.h"
+#include "library/compiler/nat_value.h"
 #include "library/compiler/eta_expansion.h"
 #include "library/compiler/simp_pr1_rec.h"
 #include "library/compiler/inliner.h"
@@ -120,6 +121,8 @@ 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 = eta_expand(m_env, v);

src/library/compiler/vm_compiler.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/compiler/simp_inductive.h"
 #include "library/compiler/erase_irrelevant.h"
+#include "library/compiler/nat_value.h"
 #include "library/compiler/preprocess.h"
 
 namespace lean {
@@ -215,14 +216,22 @@ class vm_compiler_fn {
         emit(mk_drop_instr(counter));
     }
 
+    void compile_macro(expr const & e) {
+        if (is_nat_value(e)) {
+            emit(mk_num_instr(get_nat_value_value(e)));
+        } else {
+            throw exception("code generation failed, unexpected kind of macro has been found");
+        }
+    }
+
     void compile(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
         switch (e.kind()) {
         case expr_kind::Var:      lean_unreachable();
         case expr_kind::Sort:     lean_unreachable();
         case expr_kind::Meta:     lean_unreachable();
         case expr_kind::Pi:       lean_unreachable();
-        case expr_kind::Macro:    lean_unreachable();
         case expr_kind::Lambda:   lean_unreachable();
+        case expr_kind::Macro:    compile_macro(e);          break;
         case expr_kind::Constant: compile_constant(e);       break;
         case expr_kind::Local:    compile_local(e, m);       break;
         case expr_kind::App:      compile_app(e, bpz, m);    break;