feat(kernel,frontends/lean/builtin_cmds): allow kernel extensions to report their builtin constants

src/frontends/lean/builtin_cmds.cpp

@@ -71,12 +71,7 @@ static void print_axioms(parser & p) {
     environment const & env = p.env();
     env.for_each_declaration([&](declaration const & d) {
             name const & n = d.get_name();
-            if (!d.is_definition() &&
-                !is_quotient_decl(env, n) &&
-                !is_hits_decl(env, n) &&
-                !inductive::is_inductive_decl(env, n) &&
-                !inductive::is_elim_rule(env, n) &&
-                !inductive::is_intro_rule(env, n)) {
+            if (!d.is_definition() && !env.is_builtin(n)) {
                 p.regular_stream() << n << " : " << d.get_type() << endl;
                 has_axioms = true;
             }

src/kernel/environment.h

@@ -57,6 +57,7 @@ public:
     bool impredicative() const { return m_impredicative; }
     normalizer_extension const & norm_ext() const { return *(m_norm_ext.get()); }
     bool is_recursor(environment const & env, name const & n) const { return m_norm_ext->is_recursor(env, n); }
+    bool is_builtin(environment const & env, name const & n) const { return m_norm_ext->is_builtin(env, n); }
 };
 
 class environment_extension {
@@ -137,6 +138,8 @@ public:
 
     bool is_recursor(name const & n) const { return m_header->is_recursor(*this, n); }
 
+    bool is_builtin(name const & n) const { return m_header->is_builtin(*this, n); }
+
     /** \brief Return true iff the environment treats universe level 0 as an impredicative Prop */
     bool impredicative() const { return m_header->impredicative(); }
 

src/kernel/hits/hits.cpp

@@ -133,6 +133,10 @@ bool hits_normalizer_extension::is_recursor(environment const &, name const & n)
     return n == *g_trunc_rec || n == *g_type_quotient_rec;
 }
 
+bool hits_normalizer_extension::is_builtin(environment const & env, name const & n) const {
+    return is_hits_decl(env, n);
+}
+
 bool is_hits_decl(environment const & env, name const & n) {
     if (!get_extension(env).m_initialized)
         return false;

src/kernel/hits/hits.h

@@ -18,6 +18,7 @@ public:
     virtual optional<expr> is_stuck(expr const & e, extension_context & ctx) const;
     virtual bool supports(name const & feature) const;
     virtual bool is_recursor(environment const & env, name const & n) const;
+    virtual bool is_builtin(environment const & env, name const & n) const;
 };
 
 /** \brief The following function must be invoked to register the builtin HITs computation rules in the kernel. */

src/kernel/inductive/inductive.cpp

@@ -957,6 +957,10 @@ bool inductive_normalizer_extension::is_recursor(environment const & env, name c
     return static_cast<bool>(is_elim_rule(env, n));
 }
 
+bool inductive_normalizer_extension::is_builtin(environment const & env, name const & n) const {
+    return is_inductive_decl(env, n) || is_elim_rule(env, n) || is_intro_rule(env, n);
+}
+
 template<typename Ctx>
 optional<expr> is_elim_meta_app_core(Ctx & ctx, expr const & e) {
     inductive_env_ext const & ext = get_extension(ctx.env());

src/kernel/inductive/inductive.h

@@ -20,6 +20,7 @@ public:
     virtual optional<expr> is_stuck(expr const & e, extension_context & ctx) const;
     virtual bool supports(name const & feature) const;
     virtual bool is_recursor(environment const & env, name const & n) const;
+    virtual bool is_builtin(environment const & env, name const & n) const;
 };
 
 /** \brief Introduction rule */

src/kernel/normalizer_extension.cpp

@@ -15,6 +15,7 @@ public:
     virtual optional<expr> is_stuck(expr const &, extension_context &) const { return none_expr(); }
     virtual bool supports(name const &) const { return false; }
     virtual bool is_recursor(environment const &, name const &) const { return false; }
+    virtual bool is_builtin(environment const &, name const &) const { return false; }
 };
 
 std::unique_ptr<normalizer_extension> mk_id_normalizer_extension() {
@@ -49,6 +50,10 @@ public:
     virtual bool is_recursor(environment const & env, name const & n) const {
         return m_ext1->is_recursor(env, n) || m_ext2->is_recursor(env, n);
     }
+
+    virtual bool is_builtin(environment const & env, name const & n) const {
+        return m_ext1->is_builtin(env, n) || m_ext2->is_builtin(env, n);
+    }
 };
 
 std::unique_ptr<normalizer_extension> compose(std::unique_ptr<normalizer_extension> && ext1, std::unique_ptr<normalizer_extension> && ext2) {

src/kernel/normalizer_extension.h

@@ -26,6 +26,7 @@ public:
         this method is only used for sanity checking. */
     virtual bool supports(name const & feature) const = 0;
     virtual bool is_recursor(environment const & env, name const & n) const = 0;
+    virtual bool is_builtin(environment const & env, name const & n) const = 0;
 };
 
 inline optional<pair<expr, constraint_seq>> none_ecs() { return optional<pair<expr, constraint_seq>>(); }

src/kernel/quotient/quotient.cpp

@@ -126,6 +126,10 @@ bool quotient_normalizer_extension::is_recursor(environment const &, name const
     return n == *g_quotient_lift || n == *g_quotient_ind;
 }
 
+bool quotient_normalizer_extension::is_builtin(environment const & env, name const & n) const {
+    return is_quotient_decl(env, n);
+}
+
 bool is_quotient_decl(environment const & env, name const & n) {
     if (!get_extension(env).m_initialized)
         return false;

src/kernel/quotient/quotient.h

@@ -16,6 +16,7 @@ public:
     virtual optional<expr> is_stuck(expr const & e, extension_context & ctx) const;
     virtual bool supports(name const & feature) const;
     virtual bool is_recursor(environment const & env, name const & n) const;
+    virtual bool is_builtin(environment const & env, name const & n) const;
 };
 
 /** \brief The following function must be invoked to register the quotient type computation rules in the kernel. */

src/tests/kernel/environment.cpp

@@ -137,6 +137,7 @@ public:
     virtual optional<expr> is_stuck(expr const &, extension_context &) const { return none_expr(); }
     virtual bool supports(name const &) const { return false; }
     virtual bool is_recursor(environment const &, name const &) const { return false; }
+    virtual bool is_builtin(environment const &, name const &) const { return false; }
 };
 
 static void tst3() {