michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/blast/state): make sure the type/value of hypotheses and target is a closed term.

Browse source
This commit is contained in:
Leonardo de Moura 2015-09-29 12:42:20 -07:00
parent 352d81e56a
commit bce193ed2d
2 changed files with 18 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/library/blast/state.cpp
View file

@ -101,7 +101,8 @@ void state::display(environment const & env, io_state const & ios) const {
} }
#ifdef LEAN_DEBUG #ifdef LEAN_DEBUG
bool state::check_deps(expr const & e, branch const & b, unsigned hidx, hypothesis const & h) const { bool state::check_hypothesis(expr const & e, branch const & b, unsigned hidx, hypothesis const & h) const {
lean_assert(closed(e));
for_each(e, [&](expr const & n, unsigned) { for_each(e, [&](expr const & n, unsigned) {
lean_assert(!blast::is_local(n)); lean_assert(!blast::is_local(n));
if (is_href(n)) { if (is_href(n)) {
@ -116,16 +117,14 @@ bool state::check_deps(expr const & e, branch const & b, unsigned hidx, hypothes
return true; return true;
} }
bool state::check_deps(branch const & b, unsigned hidx, hypothesis const & h) const { bool state::check_hypothesis(branch const & b, unsigned hidx, hypothesis const & h) const {
lean_assert(check_deps(h.get_type(), b, hidx, h)); lean_assert(check_hypothesis(h.get_type(), b, hidx, h));
lean_assert(!h.get_value() || check_deps(*h.get_value(), b, hidx, h)); lean_assert(!h.get_value() || check_hypothesis(*h.get_value(), b, hidx, h));
return true; return true;
} }
bool state::check_invariant(branch const & b) const { bool state::check_target(branch const & b) const {
b.for_each_hypothesis([&](unsigned hidx, hypothesis const & h) { lean_assert(closed(b.get_target()));
lean_assert(check_deps(b, hidx, h));
});
for_each(b.get_target(), [&](expr const & n, unsigned) { for_each(b.get_target(), [&](expr const & n, unsigned) {
lean_assert(!blast::is_local(n)); lean_assert(!blast::is_local(n));
if (is_href(n)) { if (is_href(n)) {
@ -139,6 +138,14 @@ bool state::check_invariant(branch const & b) const {
return true; return true;
} }
bool state::check_invariant(branch const & b) const {
b.for_each_hypothesis([&](unsigned hidx, hypothesis const & h) {
lean_assert(check_hypothesis(b, hidx, h));
});
lean_assert(check_target(b));
return true;
}
bool state::check_invariant() const { bool state::check_invariant() const {
return check_invariant(m_main); return check_invariant(m_main);
} }

5
src/library/blast/state.h
View file

@ -38,8 +38,9 @@ class state {
goal to_goal(branch const &) const; goal to_goal(branch const &) const;
#ifdef LEAN_DEBUG #ifdef LEAN_DEBUG
bool check_deps(expr const & e, branch const & b, unsigned hidx, hypothesis const & h) const; bool check_hypothesis(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_hypothesis(branch const & b, unsigned hidx, hypothesis const & h) const;
bool check_target(branch const & b) const;
bool check_invariant(branch const &) const; bool check_invariant(branch const &) const;
#endif #endif
public: public: