feat(inductive_compiler): is_pack and is_unpack API

src/library/inductive_compiler/ginductive.cpp

@@ -44,6 +44,8 @@ struct ginductive_entry {
     list<list<name> > m_intro_rules;
     list<unsigned> m_ir_offsets;
     list<pair<unsigned, unsigned> > m_idx_to_ir_range;
+    list<name> m_packs;
+    list<name> m_unpacks;
 };
 
 inline serializer & operator<<(serializer & s, ginductive_kind k) {
@@ -79,6 +81,9 @@ serializer & operator<<(serializer & s, ginductive_entry const & entry) {
     write_list<unsigned>(s, entry.m_ir_offsets);
     write_list<pair<unsigned, unsigned> >(s, entry.m_idx_to_ir_range);
 
+    write_list<name>(s, entry.m_packs);
+    write_list<name>(s, entry.m_unpacks);
+
     return s;
 }
 
@@ -96,6 +101,9 @@ ginductive_entry read_ginductive_entry(deserializer & d) {
 
     entry.m_ir_offsets = read_list<unsigned>(d);
     entry.m_idx_to_ir_range = read_list<pair<unsigned, unsigned> >(d);
+
+    entry.m_packs = read_list<name>(d, read_name);
+    entry.m_unpacks = read_list<name>(d, read_name);
     return entry;
 }
 
@@ -117,6 +125,9 @@ struct ginductive_env_ext : public environment_extension {
     name_map<unsigned>                         m_ir_to_simulated_ir_offset;
     name_map<list<pair<unsigned, unsigned> > > 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<ginductive_kind> 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<unsigned, unsigned> ind_indices_to_ir_range(name const & basic_ind_name, buffer<expr> 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<unsigned, unsigned> 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<name> get_ginductive_all_mutual_inds(environment const & env) {
     return get_extension(env).get_all_mutual_inds();
 }

src/library/inductive_compiler/ginductive.h

@@ -69,6 +69,9 @@ ind_indices_to_ir_range("foo.basic", {sum.inr ()}) = (2, 2)
 */
 pair<unsigned, unsigned> ind_indices_to_ir_range(environment const & env, name const & basic_ind_name, buffer<expr> 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<name> get_ginductive_all_mutual_inds(environment const & env);
 

src/library/inductive_compiler/ginductive_decl.h

@@ -22,6 +22,9 @@ class ginductive_decl {
     buffer<unsigned>                  m_ir_offsets; // # total intro rules @ basic
     buffer<pair<unsigned, unsigned> > m_idx_to_ir_range; // # total inds @ mutual
 
+    buffer<name> m_packs;
+    buffer<name> m_unpacks;
+
     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):
@@ -76,6 +79,11 @@ public:
     buffer<pair<unsigned, unsigned> > const & get_idx_to_ir_range() const { return m_idx_to_ir_range; }
     buffer<pair<unsigned, unsigned> > & get_idx_to_ir_range() { return m_idx_to_ir_range; }
 
+    buffer<name> const & get_packs() const { return m_packs; }
+    buffer<name> & get_packs() { return m_packs; }
+    buffer<name> const & get_unpacks() const { return m_unpacks; }
+    buffer<name> & 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])); }

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