From 48e8b8b8665d9d62e4a78f4efdd91cb07f7cd686 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Sep 2015 18:55:24 -0700 Subject: [PATCH] feat(library/blast): basic sanity checking for blast data-structures --- src/library/blast/blast.cpp | 1 + src/library/blast/branch.cpp | 8 +++++++ src/library/blast/branch.h | 22 ++++++++++++------ src/library/blast/hypothesis.h | 4 +++- src/library/blast/state.cpp | 42 ++++++++++++++++++++++++++++++++++ src/library/blast/state.h | 10 +++++++- 6 files changed, 78 insertions(+), 9 deletions(-) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index 7cbe2af99..9c9eca333 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -195,6 +195,7 @@ class context { expr new_target = to_blast_expr(g.get_type()); s.set_target(new_target); init_mvar2mref(mvar2meta_mref); + lean_assert(s.check_invariant()); return s; } diff --git a/src/library/blast/branch.cpp b/src/library/blast/branch.cpp index d5cf5f7a1..ebf9abdc9 100644 --- a/src/library/blast/branch.cpp +++ b/src/library/blast/branch.cpp @@ -99,6 +99,14 @@ expr branch::add_hypothesis(expr const & type, optional const & value, opt return add_hypothesis(name(*g_prefix, m_next), type, value, jst); } +bool branch::hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const { + if (auto s = m_forward_deps.find(hidx_provider)) { + return s->contains(hidx_user); + } else { + return false; + } +} + void branch::set_target(expr const & t) { m_target = t; m_target_deps.clear(); diff --git a/src/library/blast/branch.h b/src/library/blast/branch.h index 7a63c1946..6160e2d04 100644 --- a/src/library/blast/branch.h +++ b/src/library/blast/branch.h @@ -40,21 +40,29 @@ class branch { public: branch():m_next(0) {} - /** \brief Store in \c r the hypotheses in this branch sorted by depth */ - void get_sorted_hypotheses(hypothesis_idx_buffer & r) const; expr add_hypothesis(name const & n, expr const & type, optional const & value, optional const & jst); expr add_hypothesis(expr const & type, optional const & value, optional const & jst); - void set_target(expr const & t); + /** \brief Return true iff the hypothesis with index \c hidx_user depends on the hypothesis with index + \c hidx_provider. */ + bool hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const; - hypothesis const * get(unsigned idx) const { return m_context.find(idx); } - hypothesis const * get(expr const & e) const { - lean_assert(is_lref(e)); - return get(lref_index(e)); + hypothesis const * get(unsigned hidx) const { return m_context.find(hidx); } + hypothesis const * get(expr const & h) const { + lean_assert(is_lref(h)); + return get(lref_index(h)); } + void for_each_hypothesis(std::function const & fn) const { m_context.for_each(fn); } + /** \brief Store in \c r the hypotheses in this branch sorted by depth */ + void get_sorted_hypotheses(hypothesis_idx_buffer & r) const; + void set_target(expr const & t); expr const & get_target() const { return m_target; } + /** \brief Return true iff the target depends on the given hypothesis */ + bool target_depends_on(expr const & h) const { return m_target_deps.contains(lref_index(h)); } + + bool has_mvar(expr const & e) const { return m_mvar_idxs.contains(mref_index(e)); } }; void initialize_branch(); diff --git a/src/library/blast/hypothesis.h b/src/library/blast/hypothesis.h index 90ed83dd5..28d339c5b 100644 --- a/src/library/blast/hypothesis.h +++ b/src/library/blast/hypothesis.h @@ -7,7 +7,7 @@ Author: Leonardo de Moura #pragma once #include "util/rc.h" #include "util/rb_map.h" -#include "kernel/expr.h" +#include "library/blast/expr.h" namespace lean { namespace blast { @@ -41,5 +41,7 @@ public: optional const & get_value() const { return m_value; } optional const & get_justification() const { return m_justification; } void mark_fixed() { m_fixed = true; } + /** \brief Return true iff this hypothesis depends on \c h. */ + bool depends_on(expr const & h) const { return m_deps.contains(lref_index(h)); } }; }} diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 0f85dc1ea..53ada24d5 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -93,4 +93,46 @@ goal state::to_goal(branch const & b) const { goal state::to_goal() const { return to_goal(m_main); } + +#ifdef LEAN_DEBUG +bool state::check_deps(expr const & e, branch const & b, unsigned hidx, hypothesis const & h) const { + for_each(e, [&](expr const & n, unsigned) { + if (is_lref(n)) { + lean_assert(h.depends_on(n)); + lean_assert(b.hidx_depends_on(hidx, lref_index(n))); + } else if (is_mref(n)) { + // metavariable is in the set of used metavariables + lean_assert(b.has_mvar(n)); + } + return true; + }); + return true; +} + +bool state::check_deps(branch const & b, unsigned hidx, hypothesis const & h) const { + lean_assert(check_deps(h.get_type(), b, hidx, h)); + lean_assert(!h.get_value() || check_deps(*h.get_value(), b, hidx, h)); + return true; +} + +bool state::check_invariant(branch const & b) const { + b.for_each_hypothesis([&](unsigned hidx, hypothesis const & h) { + lean_assert(check_deps(b, hidx, h)); + }); + for_each(b.get_target(), [&](expr const & n, unsigned) { + if (is_lref(n)) { + lean_assert(b.target_depends_on(n)); + } else if (is_mref(n)) { + // metavariable is in the set of used metavariables + lean_assert(b.has_mvar(n)); + } + return true; + }); + return true; +} + +bool state::check_invariant() const { + return check_invariant(m_main); +} +#endif }} diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 4f2f96a86..5cd212d9a 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -37,6 +37,11 @@ class state { unsigned add_metavar_decl(metavar_decl const & decl); goal to_goal(branch const &) const; + #ifdef LEAN_DEBUG + bool check_deps(expr const & e, branch const & b, unsigned hidx, hypothesis const & h) const; + bool check_deps(branch const & b, unsigned hidx, hypothesis const & h) const; + bool check_invariant(branch const &) const; + #endif public: state(); /** \brief Create a new metavariable using the given type and context. @@ -63,12 +68,15 @@ public: } metavar_decl const * get_metavar_decl(unsigned idx) const { return m_metavar_decls.find(idx); } - metavar_decl const * get_metavar_decl(expr const & e) const { return get_metavar_decl(mref_index(e)); } /** \brief Convert main branch to a goal. This is mainly used for pretty printing. However, in the future, we may use this capability to invoke the tactic framework from the blast tactic. */ goal to_goal() const; + + #ifdef LEAN_DEBUG + bool check_invariant() const; + #endif }; }}