max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(inductive_compiler): get_ginductive_num_indices

Browse source
This commit is contained in:
Daniel Selsam 2017-03-06 07:50:45 -08:00 • committed by Leonardo de Moura
parent 4608782669
commit d461cb001e
7 changed files with 64 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/inductive_compiler/add_decl.cpp
View file

@ -16,12 +16,12 @@ environment add_inductive_declaration(environment const & old_env, options const
buffer<name> const & lp_names, buffer<expr> const & params,
buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules,
bool is_trusted) {
ginductive_decl decl(0, lp_names, params, inds, intro_rules);
ginductive_decl decl(old_env, 0, lp_names, params, inds, intro_rules);
environment env = add_inner_inductive_declaration(old_env, opts, implicit_infer_map, decl, is_trusted);
return env;
}
environment add_structure_declaration_aux(environment const & env, options const &,
environment add_structure_declaration_aux(environment const & old_env, options const &,
buffer<name> const & lp_names, buffer<expr> const & params,
expr const & ind, expr const & intro_rule) {
buffer<expr> inds;
@ -31,13 +31,13 @@ environment add_structure_declaration_aux(environment const & env, options const
intro_rules.emplace_back();
intro_rules.back().push_back(intro_rule);
ginductive_decl decl(0, lp_names, params, inds, intro_rules);
ginductive_decl decl(old_env, 0, lp_names, params, inds, intro_rules);
environment new_env = env;
environment env = old_env;
if (mlocal_name(ind) != get_has_sizeof_name())
new_env = mk_has_sizeof(new_env, mlocal_name(ind));
env = mk_has_sizeof(env, mlocal_name(ind));
return register_ginductive_decl(new_env, decl, ginductive_kind::BASIC);
return register_ginductive_decl(env, decl, ginductive_kind::BASIC);
}
}

19
src/library/inductive_compiler/ginductive.cpp
View file

@ -48,6 +48,7 @@ struct ginductive_entry {
ginductive_kind m_kind;
bool m_from_mutual;
unsigned m_num_params;
list<unsigned> m_num_indices;
list<name> m_inds;
list<list<name> > m_intro_rules;
list<unsigned> m_ir_offsets;
@ -82,6 +83,7 @@ serializer & operator<<(serializer & s, ginductive_entry const & entry) {
s << entry.m_kind;
s << entry.m_from_mutual;
s << entry.m_num_params;
write_list<unsigned>(s, entry.m_num_indices);
write_list<name>(s, entry.m_inds);
for (list<name> const & irs : reverse(entry.m_intro_rules))
write_list<name>(s, irs);
@ -100,6 +102,7 @@ ginductive_entry read_ginductive_entry(deserializer & d) {
d >> entry.m_kind;
d >> entry.m_from_mutual;
d >> entry.m_num_params;
entry.m_num_indices = read_list<unsigned>(d);
entry.m_inds = read_list<name>(d, read_name);
unsigned num_inds = length(entry.m_inds);
@ -127,6 +130,7 @@ struct ginductive_env_ext : public environment_extension {
name_map<list<name> > m_ind_to_mut_inds;
name_map<ginductive_kind> m_ind_to_kind;
name_map<unsigned> m_num_params;
name_map<unsigned> m_num_indices;
name_map<name> m_ir_to_ind;
name_set m_from_mutual;
@ -139,6 +143,9 @@ struct ginductive_env_ext : public environment_extension {
ginductive_env_ext() {}
void register_ginductive_entry(ginductive_entry const & entry) {
buffer<unsigned> num_indices;
to_buffer(entry.m_num_indices, num_indices);
buffer<list<name> > intro_rules;
to_buffer(entry.m_intro_rules, intro_rules);
@ -161,6 +168,7 @@ struct ginductive_env_ext : public environment_extension {
m_ind_to_mut_inds.insert(ind, entry.m_inds);
m_ind_to_kind.insert(ind, entry.m_kind);
m_num_params.insert(ind, entry.m_num_params);
m_num_indices.insert(ind, num_indices[ind_idx]);
for (name const & ir : intro_rules[ind_idx]) {
m_ir_to_ind.insert(ir, ind);
m_ir_to_simulated_ir_offset.insert(ir, ir_offsets[acc_ir_idx]);
@ -207,6 +215,12 @@ struct ginductive_env_ext : public environment_extension {
return *num_params;
}
unsigned get_num_indices(name const & ind_name) const {
unsigned const * num_indices = m_num_indices.find(ind_name);
lean_assert(num_indices);
return *num_indices;
}
list<name> get_mut_ind_names(name const & ind_name) const {
list<name> const * mut_ind_names = m_ind_to_mut_inds.find(ind_name);
lean_assert(mut_ind_names);
@ -293,6 +307,7 @@ environment register_ginductive_decl(environment const & env, ginductive_decl co
entry.m_kind = k;
entry.m_from_mutual = decl.is_from_mutual();
entry.m_num_params = decl.get_num_params();
entry.m_num_indices = to_list(decl.get_num_indices());
buffer<name> inds;
for (expr const & ind : decl.get_inds()) {
@ -333,6 +348,10 @@ unsigned get_ginductive_num_params(environment const & env, name const & ind_nam
return get_extension(env).get_num_params(ind_name);
}
unsigned get_ginductive_num_indices(environment const & env, name const & ind_name) {
return get_extension(env).get_num_indices(ind_name);
}
list<name> get_ginductive_mut_ind_names(environment const & env, name const & ind_name) {
return get_extension(env).get_mut_ind_names(ind_name);
}

3
src/library/inductive_compiler/ginductive.h
View file

@ -26,6 +26,9 @@ optional<name> is_ginductive_intro_rule(environment const & env, name const & ir
/* \brief Returns the number of parameters for the given inductive type \e ind_name. */
unsigned get_ginductive_num_params(environment const & env, name const & ind_name);
/* \brief Returns the number of indices for the given inductive type \e ind_name. */
unsigned get_ginductive_num_indices(environment const & env, name const & ind_name);
/* \brief Returns the names of all types that are mutually inductive with \e ind_name */
list<name> get_ginductive_mut_ind_names(environment const & env, name const & ind_name);

21
src/library/inductive_compiler/ginductive_decl.h
View file

@ -8,6 +8,7 @@ Author: Daniel Selsam
#include "kernel/environment.h"
#include "kernel/find_fn.h"
#include "library/tactic/simp_lemmas.h"
#include "library/inductive_compiler/util.h"
namespace lean {
@ -18,6 +19,7 @@ class ginductive_decl {
buffer<expr> m_params;
buffer<expr> m_inds;
buffer<buffer<expr> > m_intro_rules;
buffer<unsigned> m_num_indices;
buffer<unsigned> m_ir_offsets; // # total intro rules @ basic
buffer<pair<unsigned, unsigned> > m_idx_to_ir_range; // # total inds @ mutual
@ -27,13 +29,23 @@ class ginductive_decl {
optional<simp_lemmas> m_sizeof_lemmas;
public:
ginductive_decl(unsigned nest_depth, buffer<name> const & lp_names, buffer<expr> const & params, buffer<unsigned> const & ir_offsets):
m_nest_depth(nest_depth), m_from_mutual(true), m_lp_names(lp_names), m_params(params), m_ir_offsets(ir_offsets) {}
ginductive_decl(unsigned nest_depth, buffer<name> const & lp_names, buffer<expr> const & params,
buffer<unsigned> const & num_indices, buffer<unsigned> const & ir_offsets):
m_nest_depth(nest_depth), m_from_mutual(true), m_lp_names(lp_names), m_params(params), m_num_indices(num_indices), m_ir_offsets(ir_offsets) {}
ginductive_decl(unsigned nest_depth, buffer<name> const & lp_names, buffer<expr> const & params, buffer<unsigned> const & ir_offsets):
m_nest_depth(nest_depth), m_from_mutual(true), m_lp_names(lp_names), m_params(params), m_ir_offsets(ir_offsets) {
m_num_indices.emplace_back(1);
}
ginductive_decl(environment const & env, unsigned nest_depth, buffer<name> const & lp_names, buffer<expr> const & params,
buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules):
m_nest_depth(nest_depth), m_from_mutual(false), m_lp_names(lp_names), m_params(params), m_inds(inds), m_intro_rules(intro_rules) {
// Two things to do:
// 1. initialize num_indices
// 2. initialize ir_offsets
for (unsigned ind_idx = 0; ind_idx < inds.size(); ++ind_idx) {
m_num_indices.emplace_back(::lean::get_num_indices(env, inds[ind_idx]));
for (unsigned ir_idx = 0; ir_idx < intro_rules[ind_idx].size(); ++ir_idx) {
m_ir_offsets.emplace_back(0);
}
@ -73,6 +85,9 @@ public:
buffer<expr> & get_inds() { return m_inds; }
buffer<buffer<expr> > & get_intro_rules() { return m_intro_rules; }
buffer<unsigned> const & get_num_indices() const { return m_num_indices; }
buffer<unsigned> & get_num_indices() { return m_num_indices; }
buffer<unsigned> const & get_ir_offsets() const { return m_ir_offsets; }
buffer<unsigned> & get_ir_offsets() { return m_ir_offsets; }

4
src/library/inductive_compiler/nested.cpp
View file

@ -628,6 +628,7 @@ class add_nested_inductive_decl_fn {
expr mimic_ind_type = update_result_sort(m_tctx.infer(c_mimic_ind), m_nested_decl.get_result_level(m_env));
expr mimic_ind = mk_local(mk_inner_name(mimic_name), mimic_ind_type);
m_inner_decl.get_inds().push_back(mimic_ind);
m_inner_decl.get_num_indices().push_back(get_num_indices(m_env, mimic_ind));
lean_trace(name({"inductive_compiler", "nested", "mimic", "ind"}),
tout() << mlocal_name(mimic_ind) << " : " << mlocal_type(mimic_ind) << "\n";);
@ -1807,7 +1808,8 @@ public:
ginductive_decl & nested_decl, bool is_trusted):
m_env(env), m_opts(opts), m_implicit_infer_map(implicit_infer_map),
m_nested_decl(nested_decl), m_is_trusted(is_trusted),
m_inner_decl(m_nested_decl.get_nest_depth() + 1, m_nested_decl.get_lp_names(), m_nested_decl.get_params(), m_nested_decl.get_ir_offsets()),
m_inner_decl(m_nested_decl.get_nest_depth() + 1, m_nested_decl.get_lp_names(), m_nested_decl.get_params(),
m_nested_decl.get_num_indices(), m_nested_decl.get_ir_offsets()),
m_tctx(env, opts, transparency_mode::Semireducible) { }
optional<environment> operator()() {

14
src/library/inductive_compiler/util.cpp
View file

@ -24,6 +24,20 @@ implicit_infer_kind get_implicit_infer_kind(name_map<implicit_infer_kind> const
return implicit_infer_kind::Implicit;
}
unsigned get_num_indices(environment const & env, expr const & ind) {
unsigned num_indices = 0;
type_context tctx(env);
expr ind_type = tctx.relaxed_whnf(tctx.infer(ind));
type_context::tmp_locals locals(tctx);
while (is_pi(ind_type)) {
ind_type = instantiate(binding_body(ind_type), locals.push_local_from_binding(ind_type));
ind_type = tctx.relaxed_whnf(ind_type);
num_indices++;
}
lean_assert(is_sort(ind_type));
return num_indices;
}
expr get_ind_result_type(type_context & tctx, expr const & ind) {
expr ind_type = tctx.relaxed_whnf(tctx.infer(ind));
type_context::tmp_locals locals(tctx);

1
src/library/inductive_compiler/util.h
View file

@ -12,6 +12,7 @@ Author: Daniel Selsam
namespace lean {
implicit_infer_kind get_implicit_infer_kind(name_map<implicit_infer_kind> const & implicit_infer_map, name const & n);
unsigned get_num_indices(environment const & env, expr const & ind_type);
expr get_ind_result_type(type_context & tctx, expr const & ind);
void assert_def_eq(environment const & env, expr const & e1, expr const & e2);
void assert_type_correct(environment const & env, expr const & e);