From 3e3d3c83802adeaa17918335b2b2133ceba0efd5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 May 2014 15:44:15 -0700 Subject: [PATCH] feat(kernel/inductive): check in add_inductive whether the environment supports inductive datatypes or not Signed-off-by: Leonardo de Moura --- src/kernel/inductive/inductive.cpp | 109 ++++++++++++++--------------- src/kernel/inductive/inductive.h | 7 +- src/kernel/standard/standard.cpp | 5 +- tests/lua/ind2.lua | 8 ++- 4 files changed, 67 insertions(+), 62 deletions(-) diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index a3e96c250e..1c821a68ee 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -678,6 +678,8 @@ struct add_inductive_fn { } environment operator()() { + if (!dynamic_cast(&m_env.norm_ext())) + throw kernel_exception(m_env, "environment does not support inductive datatypes"); if (get_num_its() == 0) throw kernel_exception(m_env, "at least one inductive datatype declaration expected"); check_inductive_types(); @@ -702,66 +704,57 @@ environment add_inductive(environment const & env, name const & ind_name, level_ return add_inductive(env, level_params, num_params, list(inductive_decl(ind_name, type, intro_rules))); } - -/** \brief Normalizer extension for applying inductive datatype computational rules. */ -class inductive_normalizer_extension : public normalizer_extension { -public: - virtual optional operator()(expr const & e, extension_context & ctx) const { - // Reduce terms \c e of the form - // elim_k A C e p[A,b] (intro_k_i A b u) - inductive_env_ext const & ext = get_extension(ctx.env()); - expr const & elim_fn = get_app_fn(e); - if (!is_constant(elim_fn)) - return none_expr(); - auto it1 = ext.m_elim_info.find(const_name(elim_fn)); - if (!it1) - return none_expr(); // it is not an eliminator - buffer elim_args; - get_app_args(e, elim_args); - if (elim_args.size() != it1->m_num_ACe + it1->m_num_indices + 1) - return none_expr(); // number of arguments does not match - expr intro_app = ctx.whnf(elim_args.back()); - expr const & intro_fn = get_app_fn(intro_app); - // Last argument must be a constant and an application of a constant. - if (!is_constant(intro_fn)) - return none_expr(); - // Check if intro_fn is an introduction rule matching elim_fn - auto it2 = ext.m_comp_rules.find(const_name(intro_fn)); - if (!it2 || it2->m_elim_name != const_name(elim_fn)) - return none_expr(); - buffer intro_args; - get_app_args(intro_app, intro_args); - // Check intro num_args - if (intro_args.size() != it1->m_num_params + it2->m_num_bu) - return none_expr(); - // std::cout << "Candidate: " << e << "\n"; - if (it1->m_num_params > 0) { - // Global parameters of elim and intro be definitionally equal - delayed_justification jst([=]() { return mk_justification("elim/intro global parameters must match", some_expr(e)); }); - for (unsigned i = 0; i < it1->m_num_params; i++) { - if (!ctx.is_def_eq(elim_args[i], intro_args[i], jst)) - return none_expr(); - } +optional inductive_normalizer_extension::operator()(expr const & e, extension_context & ctx) const { + // Reduce terms \c e of the form + // elim_k A C e p[A,b] (intro_k_i A b u) + inductive_env_ext const & ext = get_extension(ctx.env()); + expr const & elim_fn = get_app_fn(e); + if (!is_constant(elim_fn)) + return none_expr(); + auto it1 = ext.m_elim_info.find(const_name(elim_fn)); + if (!it1) + return none_expr(); // it is not an eliminator + buffer elim_args; + get_app_args(e, elim_args); + if (elim_args.size() != it1->m_num_ACe + it1->m_num_indices + 1) + return none_expr(); // number of arguments does not match + expr intro_app = ctx.whnf(elim_args.back()); + expr const & intro_fn = get_app_fn(intro_app); + // Last argument must be a constant and an application of a constant. + if (!is_constant(intro_fn)) + return none_expr(); + // Check if intro_fn is an introduction rule matching elim_fn + auto it2 = ext.m_comp_rules.find(const_name(intro_fn)); + if (!it2 || it2->m_elim_name != const_name(elim_fn)) + return none_expr(); + buffer intro_args; + get_app_args(intro_app, intro_args); + // Check intro num_args + if (intro_args.size() != it1->m_num_params + it2->m_num_bu) + return none_expr(); + // std::cout << "Candidate: " << e << "\n"; + if (it1->m_num_params > 0) { + // Global parameters of elim and intro be definitionally equal + delayed_justification jst([=]() { return mk_justification("elim/intro global parameters must match", some_expr(e)); }); + for (unsigned i = 0; i < it1->m_num_params; i++) { + if (!ctx.is_def_eq(elim_args[i], intro_args[i], jst)) + return none_expr(); } - // std::cout << "global params matched\n"; - // Number of universe levels must match. - if (length(const_levels(elim_fn)) != length(it1->m_level_names)) - return none_expr(); - buffer ACebu; - for (unsigned i = 0; i < it1->m_num_ACe; i++) - ACebu.push_back(elim_args[i]); - for (unsigned i = 0; i < it2->m_num_bu; i++) - ACebu.push_back(intro_args[it1->m_num_params + i]); - std::reverse(ACebu.begin(), ACebu.end()); - expr r = instantiate(it2->m_comp_rhs_body, ACebu.size(), ACebu.data()); - r = instantiate_params(r, it1->m_level_names, const_levels(elim_fn)); - // std::cout << "ELIM/INTRO: " << e << " ==> " << r << "\n"; - return some_expr(r); } -}; - -std::unique_ptr mk_extension() { - return std::unique_ptr(new inductive_normalizer_extension()); + // std::cout << "global params matched\n"; + // Number of universe levels must match. + if (length(const_levels(elim_fn)) != length(it1->m_level_names)) + return none_expr(); + buffer ACebu; + for (unsigned i = 0; i < it1->m_num_ACe; i++) + ACebu.push_back(elim_args[i]); + for (unsigned i = 0; i < it2->m_num_bu; i++) + ACebu.push_back(intro_args[it1->m_num_params + i]); + std::reverse(ACebu.begin(), ACebu.end()); + expr r = instantiate(it2->m_comp_rhs_body, ACebu.size(), ACebu.data()); + r = instantiate_params(r, it1->m_level_names, const_levels(elim_fn)); + // std::cout << "ELIM/INTRO: " << e << " ==> " << r << "\n"; + return some_expr(r); } } } diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h index 0f729c878e..e8f7e7142b 100644 --- a/src/kernel/inductive/inductive.h +++ b/src/kernel/inductive/inductive.h @@ -13,8 +13,11 @@ Author: Leonardo de Moura namespace lean { namespace inductive { -/** \brief Return a normalizer extension for inductive dataypes. */ -std::unique_ptr mk_extension(); +/** \brief Normalizer extension for applying inductive datatype computational rules. */ +class inductive_normalizer_extension : public normalizer_extension { +public: + virtual optional operator()(expr const & e, extension_context & ctx) const; +}; /** \brief Introduction rule */ typedef std::pair intro_rule; diff --git a/src/kernel/standard/standard.cpp b/src/kernel/standard/standard.cpp index 99f2cab70d..2e0b18dd6e 100644 --- a/src/kernel/standard/standard.cpp +++ b/src/kernel/standard/standard.cpp @@ -7,6 +7,8 @@ Author: Leonardo de Moura #include "kernel/inductive/inductive.h" namespace lean { +using inductive::inductive_normalizer_extension; + /** \brief Create standard Lean environment */ environment mk_environment(unsigned trust_lvl) { return environment(trust_lvl, @@ -14,6 +16,7 @@ environment mk_environment(unsigned trust_lvl) { true /* Eta */, true /* Type.{0} is impredicative */, list() /* No type class has proof irrelevance */, - inductive::mk_extension() /* builtin support for inductive datatypes */); + /* builtin support for inductive datatypes */ + std::unique_ptr(new inductive_normalizer_extension())); } } diff --git a/tests/lua/ind2.lua b/tests/lua/ind2.lua index 47b556f893..b5db2e96aa 100644 --- a/tests/lua/ind2.lua +++ b/tests/lua/ind2.lua @@ -1,4 +1,4 @@ -local env = empty_environment() +local env = environment() function bad_add_inductive(...) arg = {...} @@ -101,3 +101,9 @@ bad_add_inductive(env, "nat2", Type, "zero2", Nat2, "succ2", Pi(a, Nat2, mk_arrow(eq(Nat2, a, a), Nat2))) + +local env = empty_environment() +bad_add_inductive(env, -- Environment does not support inductive datatypes + "nat", Type, + "zero", Nat, + "succ", mk_arrow(Nat, Nat))