fix(frontends/lean/builtin_cmds): 'print axioms' and theorem queue

src/frontends/lean/builtin_cmds.cpp

@@ -107,22 +107,25 @@ struct print_axioms_deps {
     }
 };
 
-static void print_axioms(parser & p) {
+static environment print_axioms(parser & p) {
     if (p.curr_is_identifier()) {
         name c = p.check_constant_next("invalid 'print axioms', constant expected");
+        environment new_env = p.reveal_all_theorems();
         print_axioms_deps(p.env(), p.regular_stream())(c);
+        return new_env;
     } else {
         bool has_axioms = false;
         environment const & env = p.env();
         env.for_each_declaration([&](declaration const & d) {
                 name const & n = d.get_name();
-                if (!d.is_definition() && !env.is_builtin(n)) {
+                if (!d.is_definition() && !env.is_builtin(n) && !p.in_theorem_queue(n)) {
                     p.regular_stream() << n << " : " << d.get_type() << endl;
                     has_axioms = true;
                 }
             });
         if (!has_axioms)
             p.regular_stream() << "no axioms" << endl;
+        return p.env();
     }
 }
 
@@ -566,7 +569,7 @@ environment print_cmd(parser & p) {
         print_metaclasses(p);
     } else if (p.curr_is_token_or_id(get_axioms_tk())) {
         p.next();
-        print_axioms(p);
+        return print_axioms(p);
     } else if (p.curr_is_token_or_id(get_fields_tk())) {
         p.next();
         auto pos = p.pos();

src/frontends/lean/parser.cpp

@@ -2056,12 +2056,12 @@ void parser::replace_theorem(certified_declaration const & thm) {
     }
 }
 
-environment parser::reveal_theorems(buffer<name> const & ds) {
+environment parser::reveal_theorems_core(buffer<name> const & ds, bool all) {
     m_theorem_queue.for_each([&](certified_declaration const & thm) {
             if (keep_new_thms()) {
                 name const & thm_name = thm.get_declaration().get_name();
                 if (m_env.get(thm_name).is_axiom() &&
-                    std::any_of(ds.begin(), ds.end(), [&](name const & n) { return n == thm_name; })) {
+                    (all || std::any_of(ds.begin(), ds.end(), [&](name const & n) { return n == thm_name; }))) {
                     replace_theorem(thm);
                     m_theorem_queue_set.erase(thm_name);
                 }
@@ -2070,6 +2070,14 @@ environment parser::reveal_theorems(buffer<name> const & ds) {
     return m_env;
 }
 
+environment parser::reveal_theorems(buffer<name> const & ds) {
+    return reveal_theorems_core(ds, false);
+}
+
+environment parser::reveal_all_theorems() {
+    return reveal_theorems_core(buffer<name>(), true);
+}
+
 void parser::save_snapshot() {
     m_pre_info_manager.clear();
     if (!m_snapshot_vector)

src/frontends/lean/parser.h

@@ -263,6 +263,7 @@ class parser {
     void init_stop_at(options const & opts);
 
     void replace_theorem(certified_declaration const & thm);
+    environment reveal_theorems_core(buffer<name> const & ds, bool all);
 
 public:
     parser(environment const & env, io_state const & ios,
@@ -333,6 +334,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);
+    environment reveal_all_theorems();
     bool in_theorem_queue(name const & n) const { return m_theorem_queue_set.contains(n); }
 
     /** \brief Read the next token. */

tests/lean/print_ax3.lean

@@ -0,0 +1,17 @@
+theorem foo1 : 0 = 0 :=
+rfl
+
+theorem foo2 : 0 = 0 :=
+rfl
+
+theorem foo3 : 0 = 0 :=
+foo2
+
+definition foo4 : 0 = 0 :=
+eq.trans foo2 foo1
+
+print axioms foo4
+print "------"
+print axioms
+print "------"
+print foo3

tests/lean/print_ax3.lean.expected.out

@@ -0,0 +1,7 @@
+no axioms
+------
+quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, setoid.r a b → quot.mk a = quot.mk b
+propext : ∀ {a b : Prop}, (a ↔ b) → a = b
+------
+theorem foo3 : 0 = 0 :=
+foo2