From 4a4ef483445a0d2bb0a981faf288a96ddbb935f5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 28 Jun 2015 11:28:05 -0700
Subject: [PATCH] fix(frontends/lean/parse_rewrite_tactic): fixes #691

---
 src/frontends/lean/parse_rewrite_tactic.cpp | 13 +++++++++++++
 tests/lean/691.lean                         | 13 +++++++++++++
 tests/lean/691.lean.expected.out            |  4 ++++
 3 files changed, 30 insertions(+)
 create mode 100644 tests/lean/691.lean
 create mode 100644 tests/lean/691.lean.expected.out

diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp
index 6c3d6a401..766195b90 100644
--- a/src/frontends/lean/parse_rewrite_tactic.cpp
+++ b/src/frontends/lean/parse_rewrite_tactic.cpp
@@ -36,19 +36,31 @@ static expr parse_rule(parser & p, bool use_paren) {
     }
 }
 
+static void check_not_in_theorem_queue(parser & p, name const & n, pos_info const & pos) {
+    if (p.in_theorem_queue(n)) {
+        throw parser_error(sstream() << "invalid 'rewrite' tactic, cannot unfold '" << n << "' "
+                           << "which is still in the theorem queue. Use command 'reveal " << n << "' "
+                           << "to access its definition.", pos);
+    }
+}
+
 static expr parse_rewrite_unfold_core(parser & p) {
     buffer<name> to_unfold;
     if (p.curr_is_token(get_lbracket_tk())) {
         p.next();
         while (true) {
+            auto pos = p.pos();
             to_unfold.push_back(p.check_constant_next("invalid unfold rewrite step, identifier expected"));
+            check_not_in_theorem_queue(p, to_unfold.back(), pos);
             if (!p.curr_is_token(get_comma_tk()))
                 break;
             p.next();
         }
         p.check_token_next(get_rbracket_tk(), "invalid unfold rewrite step, ',' or ']' expected");
     } else {
+        auto pos = p.pos();
         to_unfold.push_back(p.check_constant_next("invalid unfold rewrite step, identifier or '[' expected"));
+        check_not_in_theorem_queue(p, to_unfold.back(), pos);
     }
     location loc = parse_tactic_location(p);
     return mk_rewrite_unfold(to_list(to_unfold), loc);
@@ -174,6 +186,7 @@ expr parse_unfold_tactic(parser & p) {
     auto pos = p.pos();
     if (p.curr_is_identifier()) {
         name c       = p.check_constant_next("invalid unfold tactic, identifier expected");
+        check_not_in_theorem_queue(p, c, pos);
         location loc = parse_tactic_location(p);
         elems.push_back(p.save_pos(mk_rewrite_unfold(to_list(c), loc), pos));
     } else if (p.curr_is_token(get_lbracket_tk())) {
diff --git a/tests/lean/691.lean b/tests/lean/691.lean
new file mode 100644
index 000000000..d3dbbb782
--- /dev/null
+++ b/tests/lean/691.lean
@@ -0,0 +1,13 @@
+theorem foo : Type₁ := unit
+
+example : foo = unit :=
+by unfold foo
+
+example : foo = unit :=
+by unfold [foo]
+
+example : foo = unit :=
+by rewrite [↑foo]
+
+example : foo = unit :=
+by rewrite [↑[foo] ]
diff --git a/tests/lean/691.lean.expected.out b/tests/lean/691.lean.expected.out
new file mode 100644
index 000000000..18b2c6eb2
--- /dev/null
+++ b/tests/lean/691.lean.expected.out
@@ -0,0 +1,4 @@
+691.lean:4:10: error: invalid 'rewrite' tactic, cannot unfold 'foo' which is still in the theorem queue. Use command 'reveal foo' to access its definition.
+691.lean:7:11: error: invalid 'rewrite' tactic, cannot unfold 'foo' which is still in the theorem queue. Use command 'reveal foo' to access its definition.
+691.lean:10:13: error: invalid 'rewrite' tactic, cannot unfold 'foo' which is still in the theorem queue. Use command 'reveal foo' to access its definition.
+691.lean:13:14: error: invalid 'rewrite' tactic, cannot unfold 'foo' which is still in the theorem queue. Use command 'reveal foo' to access its definition.