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

fix(library/blast/discr_tree): ignore annotations in discrimination trees

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-26 18:20:05 -08:00
parent 3409deecdb
commit 6f6672eaaa
2 changed files with 16 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/library/blast/discr_tree.cpp
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <vector>
#include "util/rb_map.h"
#include "util/memory_pool.h"
#include "library/annotation.h"
#include "library/blast/trace.h"
#include "library/blast/blast.h"
#include "library/blast/discr_tree.h"
@ -200,6 +201,13 @@ auto discr_tree::insert_erase_app(node && n, bool is_root, expr const & e, buffe
}
}
static expr consume_annotations(expr const & e) {
if (is_annotation(e))
return consume_annotations(get_annotation_arg(e));
else
return e;
}
auto discr_tree::insert_erase(node && n, bool is_root, buffer<pair<expr, bool>> & todo,
expr const & v, buffer<pair<node, node>> & skip, bool ins) -> node {
if (todo.empty()) {
@ -213,8 +221,8 @@ auto discr_tree::insert_erase(node && n, bool is_root, buffer<pair<expr, bool>>
pair<expr, bool> p = todo.back();
todo.pop_back();
expr const & e = p.first;
bool fn = p.second;
expr e = consume_annotations(p.first);
bool fn = p.second;
if (is_eqp(e, *g_delimiter)) {
node old_n(n);
@ -316,8 +324,8 @@ bool discr_tree::find(node const & n, list<pair<expr, bool>> todo, std::function
return false; // stop search
pair<expr, bool> const & p = head(todo);
expr const & e = p.first;
bool is_fn = p.second;
expr e = consume_annotations(p.first);
bool is_fn = p.second;
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Local:

4
tests/lean/run/blast_discr_tree_annot_bug.lean Normal file
View file

@ -0,0 +1,4 @@
constants (P : ℕ → Prop) (Q : Prop)
lemma foo [intro!] [forward] : (: P 0 :) → Q := sorry
example : P 0 → Q :=
by grind