From 7a0e198147f4dab0c4b802dbb9a7b028ae97c57b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 May 2015 16:28:16 -0700 Subject: [PATCH] feat(kernel,frontends/lean/builtin_cmds): allow kernel extensions to report their builtin constants --- src/frontends/lean/builtin_cmds.cpp | 7 +------ src/kernel/environment.h | 3 +++ src/kernel/hits/hits.cpp | 4 ++++ src/kernel/hits/hits.h | 1 + src/kernel/inductive/inductive.cpp | 4 ++++ src/kernel/inductive/inductive.h | 1 + src/kernel/normalizer_extension.cpp | 5 +++++ src/kernel/normalizer_extension.h | 1 + src/kernel/quotient/quotient.cpp | 4 ++++ src/kernel/quotient/quotient.h | 1 + src/tests/kernel/environment.cpp | 1 + 11 files changed, 26 insertions(+), 6 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 57a6c9e5b..2ee9d3334 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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; } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index bd3e586fe..f98ef6c9d 100644 --- a/src/kernel/environment.h +++ b/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(); } diff --git a/src/kernel/hits/hits.cpp b/src/kernel/hits/hits.cpp index ed50b742f..8c70dca73 100644 --- a/src/kernel/hits/hits.cpp +++ b/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; diff --git a/src/kernel/hits/hits.h b/src/kernel/hits/hits.h index 05eecbcfa..59475fba5 100644 --- a/src/kernel/hits/hits.h +++ b/src/kernel/hits/hits.h @@ -18,6 +18,7 @@ public: virtual optional 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. */ diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 01108161c..4a5c4b1b8 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -957,6 +957,10 @@ bool inductive_normalizer_extension::is_recursor(environment const & env, name c return static_cast(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 optional is_elim_meta_app_core(Ctx & ctx, expr const & e) { inductive_env_ext const & ext = get_extension(ctx.env()); diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h index dc9323c40..0430d407c 100644 --- a/src/kernel/inductive/inductive.h +++ b/src/kernel/inductive/inductive.h @@ -20,6 +20,7 @@ public: virtual optional 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 */ diff --git a/src/kernel/normalizer_extension.cpp b/src/kernel/normalizer_extension.cpp index a095b3678..6c134a63e 100644 --- a/src/kernel/normalizer_extension.cpp +++ b/src/kernel/normalizer_extension.cpp @@ -15,6 +15,7 @@ public: virtual optional 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 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 compose(std::unique_ptr && ext1, std::unique_ptr && ext2) { diff --git a/src/kernel/normalizer_extension.h b/src/kernel/normalizer_extension.h index 92b388e2f..d05426fc3 100644 --- a/src/kernel/normalizer_extension.h +++ b/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> none_ecs() { return optional>(); } diff --git a/src/kernel/quotient/quotient.cpp b/src/kernel/quotient/quotient.cpp index a0382b8af..5b3f0046a 100644 --- a/src/kernel/quotient/quotient.cpp +++ b/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; diff --git a/src/kernel/quotient/quotient.h b/src/kernel/quotient/quotient.h index fa885e7c8..21e53fbfe 100644 --- a/src/kernel/quotient/quotient.h +++ b/src/kernel/quotient/quotient.h @@ -16,6 +16,7 @@ public: virtual optional 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. */ diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index c021b2160..e5e0edf37 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -137,6 +137,7 @@ public: virtual optional 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() {