From b81d4d50f1198389f8ed0f44ca7c990b1fc5ac03 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Jul 2015 17:06:22 -0700
Subject: [PATCH] feat(frontends/lean/bultin_cmds): add 'print axioms
 <declname>' command that prints axioms a giving declaration depends on

---
 src/frontends/lean/builtin_cmds.cpp    | 66 +++++++++++++++++++++-----
 tests/lean/axioms_of.lean              | 13 +++++
 tests/lean/axioms_of.lean.expected.out | 12 +++++
 3 files changed, 80 insertions(+), 11 deletions(-)
 create mode 100644 tests/lean/axioms_of.lean
 create mode 100644 tests/lean/axioms_of.lean.expected.out

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index c24c8eda2..75d00a8d7 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/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/for_each_fn.h"
 #include "kernel/inductive/inductive.h"
 #include "kernel/quotient/quotient.h"
 #include "kernel/hits/hits.h"
@@ -68,18 +69,61 @@ static void print_coercions(parser & p, optional<name> const & C) {
         });
 }
 
+struct print_axioms_deps {
+    environment     m_env;
+    io_state_stream m_ios;
+    name_set        m_visited;
+    bool            m_use_axioms;
+    print_axioms_deps(environment const & env, io_state_stream const & ios):
+        m_env(env), m_ios(ios), m_use_axioms(false) {}
+
+    void visit(name const & n) {
+        if (m_visited.contains(n))
+            return;
+        m_visited.insert(n);
+        declaration const & d = m_env.get(n);
+        if (!d.is_definition() && !m_env.is_builtin(n)) {
+            m_use_axioms = true;
+            m_ios << d.get_name() << "\n";
+        }
+        visit(d.get_type());
+        if (d.is_definition())
+            visit(d.get_value());
+    }
+
+    void visit(expr const & e) {
+        for_each(e, [&](expr const & e, unsigned) {
+                if (is_constant(e))
+                    visit(const_name(e));
+                return true;
+            });
+    }
+
+    void operator()(name const & n) {
+        visit(n);
+        if (!m_use_axioms)
+            m_ios << "no axioms" << endl;
+    }
+
+};
+
 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() && !env.is_builtin(n)) {
-                p.regular_stream() << n << " : " << d.get_type() << endl;
-                has_axioms = true;
-            }
-        });
-    if (!has_axioms)
-        p.regular_stream() << "no axioms" << endl;
+    if (p.curr_is_identifier()) {
+        name c = p.check_constant_next("invalid 'print axioms', constant expected");
+        print_axioms_deps(p.env(), p.regular_stream())(c);
+    } 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)) {
+                    p.regular_stream() << n << " : " << d.get_type() << endl;
+                    has_axioms = true;
+                }
+            });
+        if (!has_axioms)
+            p.regular_stream() << "no axioms" << endl;
+    }
 }
 
 static void print_prefix(parser & p) {
diff --git a/tests/lean/axioms_of.lean b/tests/lean/axioms_of.lean
new file mode 100644
index 000000000..2ff97f522
--- /dev/null
+++ b/tests/lean/axioms_of.lean
@@ -0,0 +1,13 @@
+import data.finset data.rat
+
+print axioms nat.add
+print "-----"
+print axioms int.add
+print "-----"
+print axioms rat.add
+print "-----"
+print axioms finset.union
+print "-----"
+print axioms finset.mem
+print "-----"
+print axioms finset.union.comm
diff --git a/tests/lean/axioms_of.lean.expected.out b/tests/lean/axioms_of.lean.expected.out
new file mode 100644
index 000000000..798570e85
--- /dev/null
+++ b/tests/lean/axioms_of.lean.expected.out
@@ -0,0 +1,12 @@
+no axioms
+-----
+no axioms
+-----
+quot.sound
+-----
+quot.sound
+-----
+propext
+-----
+quot.sound
+propext