feat(kernel/trace): add function depends_on for trace objects

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/trace.cpp

@@ -4,12 +4,42 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <set>
+#include "util/buffer.h"
 #include "kernel/trace.h"
 
 namespace lean {
 bool trace::has_children() const {
-    buffer<trace> r;
+    buffer<trace_cell *> r;
     get_children(r);
     return !r.empty();
 }
+
+bool depends_on(trace const & t, trace const & d) {
+    buffer<trace_cell *>   todo;
+    std::set<trace_cell *> visited;
+    buffer<trace_cell *>   children;
+    todo.push_back(t.raw());
+    while (todo.empty()) {
+        trace_cell * curr = todo.back();
+        todo.pop_back();
+        if (curr == d.raw()) {
+            return true;
+        } else {
+            children.clear();
+            curr->get_children(children);
+            for (trace_cell * child : children) {
+                if (child->is_shared()) {
+                    if (visited.find(child) == visited.end()) {
+                        visited.insert(child);
+                        todo.push_back(child);
+                    }
+                } else {
+                    todo.push_back(child);
+                }
+            }
+        }
+    }
+    return false;
+}
 }

src/kernel/trace.h

@@ -28,8 +28,9 @@ public:
     trace_cell():m_rc(0) {}
     virtual ~trace_cell() {}
     virtual format pp(formatter const & fmt, options const & opts) const = 0;
-    virtual void get_children(buffer<trace> & r) const = 0;
+    virtual void get_children(buffer<trace_cell*> & r) const = 0;
     virtual expr const & get_main_expr() const { return expr::null(); }
+    bool is_shared() const { return get_rc() > 1; }
 };
 
 /**
@@ -54,7 +55,13 @@ public:
     trace & operator=(trace && s) { LEAN_MOVE_REF(trace, s); }
     format pp(formatter const & fmt, options const & opts) const { lean_assert(m_ptr); return m_ptr->pp(fmt, opts); }
     expr const & get_main_expr() const { return m_ptr ? m_ptr->get_main_expr() : expr::null(); }
-    void get_children(buffer<trace> & r) const { if (m_ptr) m_ptr->get_children(r); }
+    void get_children(buffer<trace_cell*> & r) const { if (m_ptr) m_ptr->get_children(r); }
     bool has_children() const;
 };
+
+/**
+   \brief Return true iff \c t depends on \c d.
+   That is \c t is a descendant of \c d.
+*/
+bool depends_on(trace const & t, trace const & d);
 }

src/kernel/type_checker_trace.cpp

@@ -20,7 +20,7 @@ format function_expected_trace_cell::pp(formatter const & fmt, options const & o
     return r;
 }
 
-void function_expected_trace_cell::get_children(buffer<trace> &) const {
+void function_expected_trace_cell::get_children(buffer<trace_cell*> &) const {
 }
 
 expr const & function_expected_trace_cell::get_main_expr() const {
@@ -48,7 +48,7 @@ format app_type_match_trace_cell::pp(formatter const & fmt, options const & opts
     return r;
 }
 
-void app_type_match_trace_cell::get_children(buffer<trace> &) const {
+void app_type_match_trace_cell::get_children(buffer<trace_cell*> &) const {
 }
 
 expr const & app_type_match_trace_cell::get_main_expr() const {
@@ -67,7 +67,7 @@ format type_expected_trace_cell::pp(formatter const & fmt, options const & opts)
     return r;
 }
 
-void type_expected_trace_cell::get_children(buffer<trace> &) const {
+void type_expected_trace_cell::get_children(buffer<trace_cell*> &) const {
 }
 
 expr const & type_expected_trace_cell::get_main_expr() const {
@@ -85,7 +85,7 @@ format def_type_match_trace_cell::pp(formatter const &, options const &) const {
     return r;
 }
 
-void def_type_match_trace_cell::get_children(buffer<trace> &) const {
+void def_type_match_trace_cell::get_children(buffer<trace_cell*> &) const {
 }
 
 expr const & def_type_match_trace_cell::get_main_expr() const {

src/kernel/type_checker_trace.h

@@ -28,7 +28,7 @@ public:
     function_expected_trace_cell(context const & c, expr const & app):m_ctx(c), m_app(app) {}
     virtual ~function_expected_trace_cell();
     virtual format pp(formatter const & fmt, options const & opts) const;
-    virtual void get_children(buffer<trace> &) const;
+    virtual void get_children(buffer<trace_cell*> &) const;
     virtual expr const & get_main_expr() const;
     context const & get_context() const { return m_ctx; }
     expr const & get_app() const { return m_app; }
@@ -53,7 +53,7 @@ public:
     app_type_match_trace_cell(context const & c, expr const & a, unsigned i):m_ctx(c), m_app(a), m_i(i) {}
     virtual ~app_type_match_trace_cell();
     virtual format pp(formatter const & fmt, options const & opts) const;
-    virtual void get_children(buffer<trace> &) const;
+    virtual void get_children(buffer<trace_cell*> &) const;
     virtual expr const & get_main_expr() const;
     context const & get_context() const { return m_ctx; }
     expr const & get_app() const { return m_app; }
@@ -76,7 +76,7 @@ public:
     type_expected_trace_cell(context const & c, expr const & t):m_ctx(c), m_type(t) {}
     virtual ~type_expected_trace_cell();
     virtual format pp(formatter const & fmt, options const & opts) const;
-    virtual void get_children(buffer<trace> &) const;
+    virtual void get_children(buffer<trace_cell*> &) const;
     virtual expr const & get_main_expr() const;
     context const & get_context() const { return m_ctx; }
     expr const & get_type() const { return m_type; }
@@ -113,7 +113,7 @@ public:
     def_type_match_trace_cell(context const & c, name const & n, expr const & v):m_ctx(c), m_name(n), m_value(v) {}
     virtual ~def_type_match_trace_cell();
     virtual format pp(formatter const & fmt, options const & opts) const;
-    virtual void get_children(buffer<trace> &) const;
+    virtual void get_children(buffer<trace_cell*> &) const;
     virtual expr const & get_main_expr() const;
     context const & get_context() const { return m_ctx; }
     name const & get_name() const { return m_name; }