From 6f6672eaaa6eb4caded65c85a5190ae680b8e18b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 26 Jan 2016 18:20:05 -0800
Subject: [PATCH] fix(library/blast/discr_tree): ignore annotations in
 discrimination trees

---
 src/library/blast/discr_tree.cpp               | 16 ++++++++++++----
 tests/lean/run/blast_discr_tree_annot_bug.lean |  4 ++++
 2 files changed, 16 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/blast_discr_tree_annot_bug.lean

diff --git a/src/library/blast/discr_tree.cpp b/src/library/blast/discr_tree.cpp
index 240ca62e40..777a051bc3 100644
--- a/src/library/blast/discr_tree.cpp
+++ b/src/library/blast/discr_tree.cpp
@@ -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:
diff --git a/tests/lean/run/blast_discr_tree_annot_bug.lean b/tests/lean/run/blast_discr_tree_annot_bug.lean
new file mode 100644
index 0000000000..734523e907
--- /dev/null
+++ b/tests/lean/run/blast_discr_tree_annot_bug.lean
@@ -0,0 +1,4 @@
+constants (P : ℕ → Prop) (Q : Prop)
+lemma foo [intro!] [forward] : (: P 0 :) → Q := sorry
+example : P 0 → Q :=
+by grind