From 8663ac550f933d0cc97a4933fdf6e51997143a3c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Oct 2013 11:50:51 -0700 Subject: [PATCH] feat(kernel/trace): add function depends_on for trace objects Signed-off-by: Leonardo de Moura --- src/kernel/trace.cpp | 32 ++++++++++++++++++++++++++++++- src/kernel/trace.h | 11 +++++++++-- src/kernel/type_checker_trace.cpp | 8 ++++---- src/kernel/type_checker_trace.h | 8 ++++---- 4 files changed, 48 insertions(+), 11 deletions(-) diff --git a/src/kernel/trace.cpp b/src/kernel/trace.cpp index 35c2dda0d..381afd512 100644 --- a/src/kernel/trace.cpp +++ b/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 +#include "util/buffer.h" #include "kernel/trace.h" namespace lean { bool trace::has_children() const { - buffer r; + buffer r; get_children(r); return !r.empty(); } + +bool depends_on(trace const & t, trace const & d) { + buffer todo; + std::set visited; + buffer 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; +} } diff --git a/src/kernel/trace.h b/src/kernel/trace.h index babaf3c7c..49fda4d04 100644 --- a/src/kernel/trace.h +++ b/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 & r) const = 0; + virtual void get_children(buffer & 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 & r) const { if (m_ptr) m_ptr->get_children(r); } + void get_children(buffer & 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); } diff --git a/src/kernel/type_checker_trace.cpp b/src/kernel/type_checker_trace.cpp index ed4899fc4..6223980c4 100644 --- a/src/kernel/type_checker_trace.cpp +++ b/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 &) const { +void function_expected_trace_cell::get_children(buffer &) 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 &) const { +void app_type_match_trace_cell::get_children(buffer &) 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 &) const { +void type_expected_trace_cell::get_children(buffer &) 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 &) const { +void def_type_match_trace_cell::get_children(buffer &) const { } expr const & def_type_match_trace_cell::get_main_expr() const { diff --git a/src/kernel/type_checker_trace.h b/src/kernel/type_checker_trace.h index 4e5370a5f..aeab22a2d 100644 --- a/src/kernel/type_checker_trace.h +++ b/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 &) const; + virtual void get_children(buffer &) 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 &) const; + virtual void get_children(buffer &) 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 &) const; + virtual void get_children(buffer &) 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 &) const; + virtual void get_children(buffer &) const; virtual expr const & get_main_expr() const; context const & get_context() const { return m_ctx; } name const & get_name() const { return m_name; }