michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel/inductive): check in add_inductive whether the environment supports inductive datatypes or not

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-19 15:44:15 -07:00
parent a7aacaa782
commit 3e3d3c8380
4 changed files with 67 additions and 62 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

109
src/kernel/inductive/inductive.cpp
View file

@ -678,6 +678,8 @@ struct add_inductive_fn {
}
environment operator()() {
if (!dynamic_cast<inductive_normalizer_extension const*>(&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>(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<expr> 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<expr> 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<expr> 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<expr> 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<expr> 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<expr> 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<expr> 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<normalizer_extension> mk_extension() {
return std::unique_ptr<normalizer_extension>(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<expr> 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);
}
}
}

7
src/kernel/inductive/inductive.h
View file

@ -13,8 +13,11 @@ Author: Leonardo de Moura
namespace lean {
namespace inductive {
/** \brief Return a normalizer extension for inductive dataypes. */
std::unique_ptr<normalizer_extension> mk_extension();
/** \brief Normalizer extension for applying inductive datatype computational rules. */
class inductive_normalizer_extension : public normalizer_extension {
public:
virtual optional<expr> operator()(expr const & e, extension_context & ctx) const;
};
/** \brief Introduction rule */
typedef std::pair<name, expr> intro_rule;

5
src/kernel/standard/standard.cpp
View file

@ -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<name>() /* No type class has proof irrelevance */,
inductive::mk_extension() /* builtin support for inductive datatypes */);
/* builtin support for inductive datatypes */
std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()));
}
}

8
tests/lua/ind2.lua
View file

@ -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))