From 5051c0031e24ab5cf30c46a0295c37bfbfcb16ef Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 30 Sep 2015 18:50:28 -0700
Subject: [PATCH] feat(frontends/lean): add '#accessible' command for debugging
 purposes

---
 src/frontends/lean/builtin_cmds.cpp | 29 +++++++++++++++++++++++++++++
 src/frontends/lean/token_table.cpp  |  2 +-
 2 files changed, 30 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 5790413af..9b82fb1f1 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -33,6 +33,10 @@ Author: Leonardo de Moura
 #include "library/user_recursors.h"
 #include "library/pp_options.h"
 #include "library/composition_manager.h"
+#include "library/aux_recursors.h"
+#include "library/relation_manager.h"
+#include "library/projection.h"
+#include "library/private.h"
 #include "library/definitional/projection.h"
 #include "library/simplifier/simp_rule_set.h"
 #include "compiler/preprocess_rec.h"
@@ -1060,6 +1064,30 @@ static environment compile_cmd(parser & p) {
     return p.env();
 }
 
+static environment accessible_cmd(parser & p) {
+    environment const & env = p.env();
+    unsigned total               = 0;
+    unsigned accessible          = 0;
+    unsigned accessible_theorems = 0;
+    env.for_each_declaration([&](declaration const & d) {
+            name const & n = d.get_name();
+            total++;
+            if ((d.is_theorem() || d.is_definition()) &&
+                !is_instance(env, n) && !is_simp_rule(env, n) && !is_congr_rule(env, n) &&
+                !is_user_defined_recursor(env, n) && !is_aux_recursor(env, n) &&
+                !is_projection(env, n) && !is_private(env, n) &&
+                !is_user_defined_recursor(env, n) && !is_aux_recursor(env, n) &&
+                !is_subst_relation(env, n) && !is_trans_relation(env, n) &&
+                !is_symm_relation(env, n) && !is_refl_relation(env, n)) {
+                accessible++;
+                if (d.is_theorem())
+                    accessible_theorems++;
+            }
+        });
+    p.regular_stream() << "total: " << total << ", accessible: " << accessible << ", accessible theorems: " << accessible_theorems << "\n";
+    return env;
+}
+
 void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("open",          "create aliases for declarations, and use objects defined in other namespaces",
                         open_cmd));
@@ -1084,6 +1112,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("#projections",  "generate projections for inductive datatype (for debugging purposes)", projections_cmd));
     add_cmd(r, cmd_info("#telescope_eq", "(for debugging purposes)", telescope_eq_cmd));
     add_cmd(r, cmd_info("#compile",      "(for debugging purposes)", compile_cmd));
+    add_cmd(r, cmd_info("#accessible",   "(for debugging purposes) display number of accessible declarations for blast tactic", accessible_cmd));
     register_decl_cmds(r);
     register_inductive_cmd(r);
     register_structure_cmd(r);
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 7a6b4daf7..c06e2788b 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -120,7 +120,7 @@ void init_token_table(token_table & t) {
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
          "multiple_instances", "find_decl", "attribute", "persistent",
          "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",
-         "#compile", nullptr};
+         "#compile", "#accessible", nullptr};
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},