diff --git a/src/library/inductive_compiler/ginductive.cpp b/src/library/inductive_compiler/ginductive.cpp index b2ec0f2542..f36ed0a7c2 100644 --- a/src/library/inductive_compiler/ginductive.cpp +++ b/src/library/inductive_compiler/ginductive.cpp @@ -44,6 +44,8 @@ struct ginductive_entry { list > m_intro_rules; list m_ir_offsets; list > m_idx_to_ir_range; + list m_packs; + list m_unpacks; }; inline serializer & operator<<(serializer & s, ginductive_kind k) { @@ -79,6 +81,9 @@ serializer & operator<<(serializer & s, ginductive_entry const & entry) { write_list(s, entry.m_ir_offsets); write_list >(s, entry.m_idx_to_ir_range); + write_list(s, entry.m_packs); + write_list(s, entry.m_unpacks); + return s; } @@ -96,6 +101,9 @@ ginductive_entry read_ginductive_entry(deserializer & d) { entry.m_ir_offsets = read_list(d); entry.m_idx_to_ir_range = read_list >(d); + + entry.m_packs = read_list(d, read_name); + entry.m_unpacks = read_list(d, read_name); return entry; } @@ -117,6 +125,9 @@ struct ginductive_env_ext : public environment_extension { name_map m_ir_to_simulated_ir_offset; name_map > > m_ind_to_ir_ranges; + name_set m_packs; + name_set m_unpacks; + ginductive_env_ext() {} void register_ginductive_entry(ginductive_entry const & entry) { @@ -152,6 +163,12 @@ struct ginductive_env_ext : public environment_extension { ind_idx++; } + + for (name const & pack : entry.m_packs) + m_packs.insert(pack); + + for (name const & unpack : entry.m_unpacks) + m_unpacks.insert(unpack); } optional is_ginductive(name const & ind_name) const { @@ -188,12 +205,20 @@ struct ginductive_env_ext : public environment_extension { return *mut_ind_names; } - unsigned ir_to_simulated_ir_offset(name basic_ir_name) const { + unsigned ir_to_simulated_ir_offset(name const & basic_ir_name) const { unsigned const * offset = m_ir_to_simulated_ir_offset.find(basic_ir_name); lean_assert(offset); return *offset; } + bool is_pack(name const & n) const { + return m_packs.contains(n); + } + + bool is_unpack(name const & n) const { + return m_unpacks.contains(n); + } + pair ind_indices_to_ir_range(name const & basic_ind_name, buffer const & idxs) const { if (!m_from_mutual.contains(basic_ind_name)) return mk_pair(0, length(get_intro_rules(basic_ind_name))); @@ -275,6 +300,8 @@ environment register_ginductive_decl(environment const & env, ginductive_decl co intro_rules.push_back(to_list(ir_names)); } entry.m_intro_rules = to_list(intro_rules); + entry.m_packs = to_list(decl.get_packs()); + entry.m_unpacks = to_list(decl.get_unpacks()); entry.m_ir_offsets = to_list(decl.get_ir_offsets()); entry.m_idx_to_ir_range = to_list(decl.get_idx_to_ir_range()); @@ -310,6 +337,13 @@ pair ind_indices_to_ir_range(environment const & env, name c return get_extension(env).ind_indices_to_ir_range(basic_ind_name, idxs); } +bool is_ginductive_pack(environment const & env, name const & n) { + return get_extension(env).is_pack(n); +} +bool is_ginductive_unpack(environment const & env, name const & n) { + return get_extension(env).is_unpack(n); +} + list get_ginductive_all_mutual_inds(environment const & env) { return get_extension(env).get_all_mutual_inds(); } diff --git a/src/library/inductive_compiler/ginductive.h b/src/library/inductive_compiler/ginductive.h index 61712cad91..2796319c91 100644 --- a/src/library/inductive_compiler/ginductive.h +++ b/src/library/inductive_compiler/ginductive.h @@ -69,6 +69,9 @@ ind_indices_to_ir_range("foo.basic", {sum.inr ()}) = (2, 2) */ pair ind_indices_to_ir_range(environment const & env, name const & basic_ind_name, buffer const & idxs); +bool is_ginductive_pack(environment const & env, name const & n); +bool is_ginductive_unpack(environment const & env, name const & n); + /* \brief Returns the names of all mutual ginductive types */ list get_ginductive_all_mutual_inds(environment const & env); diff --git a/src/library/inductive_compiler/ginductive_decl.h b/src/library/inductive_compiler/ginductive_decl.h index 134882ea8d..b8fc695a9c 100644 --- a/src/library/inductive_compiler/ginductive_decl.h +++ b/src/library/inductive_compiler/ginductive_decl.h @@ -22,6 +22,9 @@ class ginductive_decl { buffer m_ir_offsets; // # total intro rules @ basic buffer > m_idx_to_ir_range; // # total inds @ mutual + buffer m_packs; + buffer m_unpacks; + optional m_sizeof_lemmas; public: ginductive_decl(unsigned nest_depth, buffer const & lp_names, buffer const & params, buffer const & ir_offsets): @@ -76,6 +79,11 @@ public: buffer > const & get_idx_to_ir_range() const { return m_idx_to_ir_range; } buffer > & get_idx_to_ir_range() { return m_idx_to_ir_range; } + buffer const & get_packs() const { return m_packs; } + buffer & get_packs() { return m_packs; } + buffer const & get_unpacks() const { return m_unpacks; } + buffer & get_unpacks() { return m_unpacks; } + expr mk_const(name const & n) const { return mk_constant(n, get_levels()); } expr mk_const_params(name const & n) const { return mk_app(mk_const(n), m_params); } expr get_c_ind(unsigned ind_idx) const { return mk_const(mlocal_name(m_inds[ind_idx])); } diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index 4d9f31cf2d..2c0ca30341 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -795,6 +795,9 @@ class add_nested_inductive_decl_fn { m_env = set_reducible(m_env, mk_pi_name(fn_type::PACK), reducible_status::Irreducible, true); m_env = set_reducible(m_env, mk_pi_name(fn_type::UNPACK), reducible_status::Irreducible, true); + m_nested_decl.get_packs().push_back(mk_pi_name(fn_type::PACK)); + m_nested_decl.get_unpacks().push_back(mk_pi_name(fn_type::UNPACK)); + m_tctx.set_env(m_env); expr pi_pack = mk_app(m_nested_decl.mk_const_params(mk_pi_name(fn_type::PACK)), ldeps);