feat(library/class): add is_derived_trans_instance predicate

src/library/class.cpp

@@ -54,6 +54,7 @@ struct class_state {
     class_instances       m_instances;
     class_instances       m_derived_trans_instances;
     instance_priorities   m_priorities;
+    name_set              m_derived_trans_instance_set;
     name_set              m_multiple; // set of classes that allow multiple solutions/instances
     tc_multigraph         m_mgraph;
 
@@ -70,6 +71,10 @@ struct class_state {
         return m_priorities.contains(i);
     }
 
+    bool is_derived_trans_instance(name const & i) const {
+        return m_derived_trans_instance_set.contains(i);
+    }
+
     bool try_multiple_instances(name const & c) const {
         return m_multiple.contains(c);
     }
@@ -113,6 +118,7 @@ struct class_state {
             auto lst = filter(*it, [&](name const & i1) { return i1 != i; });
             m_derived_trans_instances.insert(tgt, cons(i, lst));
         }
+        m_derived_trans_instance_set.insert(i);
         m_mgraph.add1(env, src, i, tgt);
     }
 
@@ -335,6 +341,11 @@ bool is_instance(environment const & env, name const & i) {
     return s.is_instance(i);
 }
 
+bool is_derived_trans_instance(environment const & env, name const & i) {
+    class_state const & s = class_ext::get_state(env);
+    return s.is_derived_trans_instance(i);
+}
+
 list<name> get_class_instances(environment const & env, name const & c) {
     class_state const & s = class_ext::get_state(env);
     return ptr_to_list(s.m_instances.find(c));

src/library/class.h

@@ -23,6 +23,8 @@ environment add_trans_instance(environment const & env, name const & n, unsigned
 bool is_class(environment const & env, name const & c);
 /** \brief Return true iff \c i was declared with \c add_instance. */
 bool is_instance(environment const & env, name const & i);
+/** \brief Return true iff \c i is a derived transitive instance. */
+bool is_derived_trans_instance(environment const & env, name const & i);
 /** \brief Return the instances of the given class. */
 list<name> get_class_instances(environment const & env, name const & c);
 /** \brief Return instances from the transitive closure graph of instances added using add_trans_instance */