feat(library): add declaration statistics

src/frontends/lean/builtin_cmds.cpp

@@ -37,6 +37,7 @@ Author: Leonardo de Moura
 #include "library/relation_manager.h"
 #include "library/projection.h"
 #include "library/private.h"
+#include "library/decl_stats.h"
 #include "library/definitional/projection.h"
 #include "library/simplifier/simp_rule_set.h"
 #include "compiler/preprocess_rec.h"
@@ -1088,6 +1089,39 @@ static environment accessible_cmd(parser & p) {
     return env;
 }
 
+static void display_name_set(parser & p, name const & n, name_set const & s) {
+    if (s.empty())
+        return;
+    io_state_stream out = p.regular_stream();
+    out << "  " << n << " := {";
+    bool first = true;
+    s.for_each([&](name const & n2) {
+            if (is_private(p.env(), n2))
+                return;
+            if (first)
+                first = false;
+            else
+                out << ", ";
+            out << n2;
+        });
+    out << "}\n";
+}
+
+static environment decl_stats_cmd(parser & p) {
+    environment const & env = p.env();
+    std::cout << "Use sets\n";
+    env.for_each_declaration([&](declaration const & d) {
+            if ((d.is_theorem() || d.is_axiom()) && !is_private(env, d.get_name()))
+                display_name_set(p, d.get_name(), get_use_set(env, d.get_name()));
+        });
+    std::cout << "Used-by sets\n";
+    env.for_each_declaration([&](declaration const & d) {
+            if (!d.is_theorem() && !d.is_axiom() && !is_private(env, d.get_name()))
+                display_name_set(p, d.get_name(), get_used_by_set(env, d.get_name()));
+        });
+    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));
@@ -1113,6 +1147,8 @@ void init_cmd_table(cmd_table & r) {
     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));
+    add_cmd(r, cmd_info("#decl_stats",   "(for debugging purposes) display declaration statistics", decl_stats_cmd));
+
     register_decl_cmds(r);
     register_inductive_cmd(r);
     register_structure_cmd(r);

src/frontends/lean/token_table.cpp

@@ -119,7 +119,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", "#accessible", nullptr};
+         "#compile", "#accessible", "#decl_stats", nullptr};
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

src/library/CMakeLists.txt

@@ -15,4 +15,5 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp
   relation_manager.cpp export.cpp user_recursors.cpp
   class_instance_synth.cpp idx_metavar.cpp composition_manager.cpp
-  tc_multigraph.cpp noncomputable.cpp aux_recursors.cpp norm_num.cpp)
+  tc_multigraph.cpp noncomputable.cpp aux_recursors.cpp norm_num.cpp
+  decl_stats.cpp)

src/library/decl_stats.cpp

@@ -0,0 +1,124 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/environment.h"
+#include "kernel/for_each_fn.h"
+#include "library/reducible.h"
+
+namespace lean {
+struct decl_stats_ext : public environment_extension {
+    name_map<unsigned> m_num_occs;
+    name_map<name_set> m_use_set;
+    name_map<name_set> m_used_by_set;
+
+    void inc_num_occs(name const & n) {
+        if (auto v = m_num_occs.find(n)) {
+            m_num_occs.insert(n, *v+1);
+        } else {
+            m_num_occs.insert(n, 1);
+        }
+    }
+
+    static void updt(name_map<name_set> & s, name const & k, name const & v) {
+        name_set new_set_v;
+        if (auto set_v = s.find(k))
+            new_set_v = *set_v;
+        new_set_v.insert(v);
+        s.insert(k, new_set_v);
+    }
+
+    void updt(name const & user, name const & used) {
+        inc_num_occs(used);
+        updt(m_use_set,     user, used);
+        updt(m_used_by_set, used, user);
+    }
+};
+
+struct decl_stats_ext_reg {
+    unsigned m_ext_id;
+    decl_stats_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<decl_stats_ext>()); }
+};
+
+static decl_stats_ext_reg * g_ext = nullptr;
+static decl_stats_ext const & get_extension(environment const & env) {
+    return static_cast<decl_stats_ext const &>(env.get_extension(g_ext->m_ext_id));
+}
+static environment update(environment const & env, decl_stats_ext const & ext) {
+    return env.update(g_ext->m_ext_id, std::make_shared<decl_stats_ext>(ext));
+}
+
+class update_decl_stats_fn {
+    environment const & m_env;
+    decl_stats_ext      m_ext;
+    name                m_name;
+    name_set            m_visited;
+    name_predicate      m_not_reducible_pred;
+
+    void visit(expr const & e) {
+        for_each(e, [&](expr const & e, unsigned) {
+                if (!is_constant(e))
+                    return true;
+                name const & n = const_name(e);
+                if (m_visited.contains(n))
+                    return true;
+                m_visited.insert(n);
+                if (m_not_reducible_pred(n)) {
+                    m_ext.updt(m_name, n);
+                } else {
+                    // pretend the reducible definition was expanded.
+                    declaration d = m_env.get(n);
+                    visit(d.get_value());
+                }
+                return true;
+            });
+    }
+
+public:
+    update_decl_stats_fn(environment const & env):
+        m_env(env),
+        m_ext(get_extension(env)),
+        m_not_reducible_pred(mk_not_reducible_pred(env)) {}
+
+    environment operator()(declaration const & d) {
+        m_name = d.get_name();
+        visit(d.get_type());
+        return update(m_env, m_ext);
+    }
+};
+
+environment update_decl_stats(environment const & env, declaration const & d) {
+    return update_decl_stats_fn(env)(d);
+}
+
+unsigned get_num_occs(environment const & env, name const & n) {
+    if (auto v = get_extension(env).m_num_occs.find(n))
+        return *v;
+    else
+        return 0;
+}
+
+name_set get_use_set(environment const & env, name const & n) {
+    if (auto v = get_extension(env).m_use_set.find(n))
+        return *v;
+    else
+        return name_set();
+}
+
+name_set get_used_by_set(environment const & env, name const & n) {
+    if (auto v = get_extension(env).m_used_by_set.find(n))
+        return *v;
+    else
+        return name_set();
+}
+
+void initialize_decl_stats() {
+    g_ext     = new decl_stats_ext_reg();
+}
+
+void finalize_decl_stats() {
+    delete g_ext;
+}
+}

src/library/decl_stats.h

@@ -0,0 +1,25 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+
+namespace lean {
+/** \brief Updated internal indices associated with declarations
+    We track which constants occur in the type of other constants (and the inverse map).
+    We also track the number of times a constant occur in the type of other constants.
+
+    \remark This procedure will "unfold" reducible constants when computing statistics.
+*/
+environment update_decl_stats(environment const & env, declaration const & d);
+/** \brief Return the number of constants s.t. \c n occur in their type. */
+unsigned get_num_occs(environment const & env, name const & n);
+/** \brief Return the set of constants that occur in the type of \c n. */
+name_set get_use_set(environment const & env, name const & n);
+/** \brief Return the set of constants s.t. \c n occur in their type. */
+name_set get_used_by_set(environment const & env, name const & n);
+void initialize_decl_stats();
+void finalize_decl_stats();
+}

src/library/init_module.cpp

@@ -41,6 +41,7 @@ Author: Leonardo de Moura
 #include "library/composition_manager.h"
 #include "library/noncomputable.h"
 #include "library/aux_recursors.h"
+#include "library/decl_stats.h"
 
 namespace lean {
 void initialize_library_module() {
@@ -81,9 +82,11 @@ void initialize_library_module() {
     initialize_composition_manager();
     initialize_noncomputable();
     initialize_aux_recursors();
+    initialize_decl_stats();
 }
 
 void finalize_library_module() {
+    finalize_decl_stats();
     finalize_aux_recursors();
     finalize_noncomputable();
     finalize_composition_manager();

src/library/module.cpp

@@ -27,6 +27,7 @@ Author: Leonardo de Moura
 #include "library/sorry.h"
 #include "library/kernel_serializer.h"
 #include "library/unfold_macros.h"
+#include "library/decl_stats.h"
 #include "version.h"
 
 #ifndef LEAN_ASYNCH_IMPORT_THEOREM
@@ -220,6 +221,7 @@ static environment export_decl(environment const & env, declaration const & d) {
 environment add(environment const & env, certified_declaration const & d) {
     environment new_env = env.add(d);
     declaration _d = d.get_declaration();
+    new_env = update_decl_stats(new_env, _d);
     if (!check_computable(new_env, _d.get_name()))
         new_env = mark_noncomputable(new_env, _d.get_name());
     return export_decl(update_module_defs(new_env, _d), _d);

src/library/shared_environment.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/shared_environment.h"
+#include "library/decl_stats.h"
 
 namespace lean {
 shared_environment::shared_environment() {}
@@ -18,11 +19,13 @@ environment shared_environment::get_environment() const {
 void shared_environment::add(certified_declaration const & d) {
     lock_guard<mutex> l(m_mutex);
     m_env = m_env.add(d);
+    m_env = update_decl_stats(m_env, d.get_declaration());
 }
 
 void shared_environment::add(declaration const & d) {
     lock_guard<mutex> l(m_mutex);
     m_env = m_env.add(d);
+    m_env = update_decl_stats(m_env, d);
 }
 
 void shared_environment::replace(certified_declaration const & t) {