diff --git a/src/library/inductive_compiler/add_decl.cpp b/src/library/inductive_compiler/add_decl.cpp index 458f1730c2..5097a3a1ed 100644 --- a/src/library/inductive_compiler/add_decl.cpp +++ b/src/library/inductive_compiler/add_decl.cpp @@ -16,12 +16,12 @@ environment add_inductive_declaration(environment const & old_env, options const buffer const & lp_names, buffer const & params, buffer const & inds, buffer > 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 const & lp_names, buffer const & params, expr const & ind, expr const & intro_rule) { buffer 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); } } diff --git a/src/library/inductive_compiler/ginductive.cpp b/src/library/inductive_compiler/ginductive.cpp index ab2574af38..2a9923867a 100644 --- a/src/library/inductive_compiler/ginductive.cpp +++ b/src/library/inductive_compiler/ginductive.cpp @@ -48,6 +48,7 @@ struct ginductive_entry { ginductive_kind m_kind; bool m_from_mutual; unsigned m_num_params; + list m_num_indices; list m_inds; list > m_intro_rules; list 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(s, entry.m_num_indices); write_list(s, entry.m_inds); for (list const & irs : reverse(entry.m_intro_rules)) write_list(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(d); entry.m_inds = read_list(d, read_name); unsigned num_inds = length(entry.m_inds); @@ -127,6 +130,7 @@ struct ginductive_env_ext : public environment_extension { name_map > m_ind_to_mut_inds; name_map m_ind_to_kind; name_map m_num_params; + name_map m_num_indices; name_map 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 num_indices; + to_buffer(entry.m_num_indices, num_indices); + buffer > 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 get_mut_ind_names(name const & ind_name) const { list 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 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 get_ginductive_mut_ind_names(environment const & env, name const & ind_name) { return get_extension(env).get_mut_ind_names(ind_name); } diff --git a/src/library/inductive_compiler/ginductive.h b/src/library/inductive_compiler/ginductive.h index 8818d44db5..b3ad0a0fe2 100644 --- a/src/library/inductive_compiler/ginductive.h +++ b/src/library/inductive_compiler/ginductive.h @@ -26,6 +26,9 @@ optional 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 get_ginductive_mut_ind_names(environment const & env, name const & ind_name); diff --git a/src/library/inductive_compiler/ginductive_decl.h b/src/library/inductive_compiler/ginductive_decl.h index b8fc695a9c..4b5042b283 100644 --- a/src/library/inductive_compiler/ginductive_decl.h +++ b/src/library/inductive_compiler/ginductive_decl.h @@ -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 m_params; buffer m_inds; buffer > m_intro_rules; + buffer m_num_indices; buffer m_ir_offsets; // # total intro rules @ basic buffer > m_idx_to_ir_range; // # total inds @ mutual @@ -27,13 +29,23 @@ class ginductive_decl { optional m_sizeof_lemmas; public: - ginductive_decl(unsigned nest_depth, buffer const & lp_names, buffer const & params, buffer 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 const & lp_names, buffer const & params, + buffer const & num_indices, buffer 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 const & lp_names, buffer const & params, buffer 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 const & lp_names, buffer const & params, buffer const & inds, buffer > 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 & get_inds() { return m_inds; } buffer > & get_intro_rules() { return m_intro_rules; } + buffer const & get_num_indices() const { return m_num_indices; } + buffer & get_num_indices() { return m_num_indices; } + buffer const & get_ir_offsets() const { return m_ir_offsets; } buffer & get_ir_offsets() { return m_ir_offsets; } diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index 2c0ca30341..74fe55b1c7 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -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 operator()() { diff --git a/src/library/inductive_compiler/util.cpp b/src/library/inductive_compiler/util.cpp index a43771d007..646b25074d 100644 --- a/src/library/inductive_compiler/util.cpp +++ b/src/library/inductive_compiler/util.cpp @@ -24,6 +24,20 @@ implicit_infer_kind get_implicit_infer_kind(name_map 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); diff --git a/src/library/inductive_compiler/util.h b/src/library/inductive_compiler/util.h index 251c14263c..f3f7bdcff9 100644 --- a/src/library/inductive_compiler/util.h +++ b/src/library/inductive_compiler/util.h @@ -12,6 +12,7 @@ Author: Daniel Selsam namespace lean { implicit_infer_kind get_implicit_infer_kind(name_map 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);