feat(library/blast): basic sanity checking for blast data-structures

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

src/library/blast/branch.cpp

@@ -99,6 +99,14 @@ expr branch::add_hypothesis(expr const & type, optional<expr> 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();

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<expr> const & value, optional<expr> const & jst);
     expr add_hypothesis(expr const & type, optional<expr> const & value, optional<expr> 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<void(unsigned, hypothesis const &)> 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();

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<expr> const & get_value() const { return m_value; }
     optional<expr> 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)); }
 };
 }}

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
 }}

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