feat(frontends/lean): add 'print axioms' command, close #251

src/frontends/lean/builtin_cmds.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
+#include "kernel/inductive/inductive.h"
 #include "library/io_state_stream.h"
 #include "library/scoped_ext.h"
 #include "library/aliases.h"
@@ -53,6 +54,23 @@ static void print_coercions(parser & p, optional<name> const & C) {
         });
 }
 
+static void print_axioms(parser & p) {
+    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() &&
+                !inductive::is_inductive_decl(env, n) &&
+                !inductive::is_elim_rule(env, n) &&
+                !inductive::is_intro_rule(env, n)) {
+                p.regular_stream() << n << " : " << d.get_type() << endl;
+                has_axioms = true;
+            }
+        });
+    if (!has_axioms)
+        p.regular_stream() << "no axioms" << endl;
+}
+
 environment print_cmd(parser & p) {
     if (p.curr() == scanner::token_kind::String) {
         p.regular_stream() << p.get_str_val() << endl;
@@ -98,6 +116,9 @@ environment print_cmd(parser & p) {
         if (p.curr_is_identifier())
             C = p.check_constant_next("invalid 'print coercions', constant expected");
         print_coercions(p, C);
+    } else if (p.curr_is_token_or_id(get_axioms_tk())) {
+        p.next();
+        print_axioms(p);
     } else {
         throw parser_error("invalid print command", p.pos());
     }

src/frontends/lean/tokens.cpp

@@ -65,6 +65,7 @@ static name * g_end          = nullptr;
 static name * g_definition   = nullptr;
 static name * g_theorem      = nullptr;
 static name * g_axiom        = nullptr;
+static name * g_axioms       = nullptr;
 static name * g_variable     = nullptr;
 static name * g_variables    = nullptr;
 static name * g_opaque       = nullptr;
@@ -150,6 +151,7 @@ void initialize_tokens() {
     g_theorem      = new name("theorem");
     g_opaque       = new name("opaque");
     g_axiom        = new name("axiom");
+    g_axioms       = new name("axioms");
     g_variable     = new name("variable");
     g_variables    = new name("variables");
     g_instance     = new name("[instance]");
@@ -197,6 +199,7 @@ void finalize_tokens() {
     delete g_theorem;
     delete g_opaque;
     delete g_axiom;
+    delete g_axioms;
     delete g_variables;
     delete g_variable;
     delete g_instance;
@@ -318,6 +321,7 @@ name const & get_end_tk() { return *g_end; }
 name const & get_definition_tk() { return *g_definition; }
 name const & get_theorem_tk() { return *g_theorem; }
 name const & get_axiom_tk() { return *g_axiom; }
+name const & get_axioms_tk() { return *g_axiom; }
 name const & get_variable_tk() { return *g_variable; }
 name const & get_variables_tk() { return *g_variables; }
 name const & get_opaque_tk() { return *g_opaque; }

src/frontends/lean/tokens.h

@@ -67,6 +67,7 @@ name const & get_end_tk();
 name const & get_definition_tk();
 name const & get_theorem_tk();
 name const & get_axiom_tk();
+name const & get_axioms_tk();
 name const & get_variable_tk();
 name const & get_variables_tk();
 name const & get_opaque_tk();

tests/lean/print_ax1.lean

@@ -0,0 +1,3 @@
+import data.nat.basic
+
+print axioms

tests/lean/print_ax1.lean.expected.out

@@ -0,0 +1 @@
+no axioms

tests/lean/print_ax2.lean

@@ -0,0 +1,3 @@
+import logic.axioms.hilbert logic.axioms.funext
+
+print axioms

tests/lean/print_ax2.lean.expected.out

@@ -0,0 +1,2 @@
+funext : ∀ {A : Type} {B : A → Type} {f g : Π (x : A), B x}, (∀ (x : A), f x = g x) → f = g
+strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A), (∃ (x : A), P x) → P x }