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

fix(library/blast/backward/backward_action): add missing normalize at backward_action, and remove incorrect fix at discrimination tree

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-26 20:35:57 -08:00
parent 4821af8685
commit 810ee9759c
3 changed files with 11 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/blast/backward/backward_action.cpp
View file

@ -50,7 +50,7 @@ struct backward_proof_step_cell : public proof_step_cell {
static action_result try_lemma(gexpr const & e, bool prop_only_branches) {
state & s = curr_state();
expr f = e.to_expr();
expr type = infer_type(f);
expr type = normalize(infer_type(f));
expr pr = f;
buffer<expr> mvars;
while (true) {

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

@ -201,13 +201,6 @@ 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()) {
@ -221,8 +214,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 e = consume_annotations(p.first);
bool fn = p.second;
expr const & e = p.first;
bool fn = p.second;
if (is_eqp(e, *g_delimiter)) {
node old_n(n);
@ -324,8 +317,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 e = consume_annotations(p.first);
bool is_fn = p.second;
expr const & e = p.first;
bool is_fn = p.second;
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Local:

6
tests/lean/run/blast_backward_action_missing_normalize.lean Normal file
View file

@ -0,0 +1,6 @@
constants (P : ℕ → Prop) (R : Prop)
lemma foo [intro!] : (: P 0 :) → R := sorry
constants (P0 : P 0)
attribute P0 [intro!]
example : R :=
by grind -- fails