From 8a85e4ee875b603faa0293fc58a7cef0934c6a16 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 13 Jun 2015 12:12:22 -0700
Subject: [PATCH] feat(frontends/lean/builtin_cmds): improve `print <id>` when
 `<id>` is a not yet revealed theorem

We add a remark saying the command `reveal <id>` should be used to
access `<id>` definition.
---
 src/frontends/lean/builtin_cmds.cpp    |  8 +++++++-
 src/frontends/lean/parser.cpp          |  3 +++
 src/frontends/lean/parser.h            |  3 ++-
 tests/lean/print_thm.lean              | 10 ++++++++++
 tests/lean/print_thm.lean.expected.out |  4 ++++
 5 files changed, 26 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/print_thm.lean
 create mode 100644 tests/lean/print_thm.lean.expected.out

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index b9ca8457b..672c106c5 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -304,7 +304,13 @@ bool print_polymorphic(parser & p) {
                     } else if (is_hits_decl(env, c)) {
                         print_constant(p, "builtin-HIT-constant", d);
                     } else if (d.is_axiom()) {
-                        print_constant(p, "axiom", d);
+                        if (p.in_theorem_queue(d.get_name())) {
+                            print_constant(p, "theorem", d);
+                            out << "'" << d.get_name() << "' is still in the theorem queue, use command 'reveal "
+                                << d.get_name() << "' to access its definition.\n";
+                        } else {
+                            print_constant(p, "axiom", d);
+                        }
                     } else {
                         print_constant(p, "constant", d);
                     }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 80b38269e..c181d5d23 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1859,10 +1859,12 @@ bool parser::curr_is_command_like() const {
 
 void parser::add_delayed_theorem(environment const & env, name const & n, level_param_names const & ls,
                                  expr const & t, expr const & v) {
+    m_theorem_queue_set.insert(n);
     m_theorem_queue.add(env, n, ls, get_local_level_decls(), t, v);
 }
 
 void parser::add_delayed_theorem(certified_declaration const & cd) {
+    m_theorem_queue_set.insert(cd.get_declaration().get_name());
     m_theorem_queue.add(cd);
 }
 
@@ -1873,6 +1875,7 @@ environment parser::reveal_theorems(buffer<name> const & ds) {
                 if (m_env.get(thm_name).is_axiom() &&
                     std::any_of(ds.begin(), ds.end(), [&](name const & n) { return n == thm_name; })) {
                     m_env = m_env.replace(thm);
+                    m_theorem_queue_set.erase(thm_name);
                 }
             }
         });
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index b904fc68c..05b313048 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -14,7 +14,6 @@ Author: Leonardo de Moura
 #include "util/exception.h"
 #include "util/thread_script_state.h"
 #include "util/script_exception.h"
-#include "util/worker_queue.h"
 #include "util/name_generator.h"
 #include "kernel/environment.h"
 #include "kernel/expr_maps.h"
@@ -123,6 +122,7 @@ class parser {
     optional<bool>          m_has_tactic_decls;
     // We process theorems in parallel
     theorem_queue           m_theorem_queue;
+    name_set                m_theorem_queue_set; // set of theorem names in m_theorem_queue
 
     // info support
     snapshot_vector *       m_snapshot_vector;
@@ -307,6 +307,7 @@ public:
     void add_delayed_theorem(environment const & env, name const & n, level_param_names const & ls, expr const & t, expr const & v);
     void add_delayed_theorem(certified_declaration const & cd);
     environment reveal_theorems(buffer<name> const & ds);
+    bool in_theorem_queue(name const & n) const { return m_theorem_queue_set.contains(n); }
 
     /** \brief Read the next token. */
     void scan() { m_curr = m_scanner.scan(m_env); }
diff --git a/tests/lean/print_thm.lean b/tests/lean/print_thm.lean
new file mode 100644
index 000000000..66dac3d5a
--- /dev/null
+++ b/tests/lean/print_thm.lean
@@ -0,0 +1,10 @@
+open nat
+
+theorem simple (a : nat) : a ≥ 0 :=
+zero_le a
+
+print simple
+
+reveal simple
+
+print simple
diff --git a/tests/lean/print_thm.lean.expected.out b/tests/lean/print_thm.lean.expected.out
new file mode 100644
index 000000000..0181442c3
--- /dev/null
+++ b/tests/lean/print_thm.lean.expected.out
@@ -0,0 +1,4 @@
+theorem simple : ∀ (a : ℕ), a ≥ 0
+'simple' is still in the theorem queue, use command 'reveal simple' to access its definition.
+theorem simple : ∀ (a : ℕ), a ≥ 0 :=
+zero_le