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

feat(library/blast/state): add assertion to make sure blast state does not contain local constants.

Browse source
This commit is contained in:
Leonardo de Moura 2015-09-29 12:31:54 -07:00
parent c652eeeac6
commit 352d81e56a
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -103,6 +103,7 @@ 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_deps(expr const & e, branch const & b, unsigned hidx, hypothesis const & h) const {
for_each(e, [&](expr const & n, unsigned) { for_each(e, [&](expr const & n, unsigned) {
lean_assert(!blast::is_local(n));
if (is_href(n)) { if (is_href(n)) {
lean_assert(h.depends_on(n)); lean_assert(h.depends_on(n));
lean_assert(b.hidx_depends_on(hidx, href_index(n))); lean_assert(b.hidx_depends_on(hidx, href_index(n)));
@ -126,6 +127,7 @@ bool state::check_invariant(branch const & b) const {
lean_assert(check_deps(b, hidx, h)); 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));
if (is_href(n)) { if (is_href(n)) {
lean_assert(b.target_depends_on(n)); lean_assert(b.target_depends_on(n));
} else if (is_mref(n)) { } else if (is_mref(n)) {