From d64b410bbd1c19e2a12bc331d1942e59f30a9c50 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 Oct 2015 18:36:41 -0700 Subject: [PATCH] feat(library): add declaration statistics --- src/frontends/lean/builtin_cmds.cpp | 36 ++++++++ src/frontends/lean/token_table.cpp | 2 +- src/library/CMakeLists.txt | 3 +- src/library/decl_stats.cpp | 124 ++++++++++++++++++++++++++++ src/library/decl_stats.h | 25 ++++++ src/library/init_module.cpp | 3 + src/library/module.cpp | 2 + src/library/shared_environment.cpp | 3 + 8 files changed, 196 insertions(+), 2 deletions(-) create mode 100644 src/library/decl_stats.cpp create mode 100644 src/library/decl_stats.h diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 9b82fb1f1..0a8621437 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index d1f1fff11..a1d978e89 100644 --- a/src/frontends/lean/token_table.cpp +++ b/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 aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 1cb422200..8b04fe2f7 100644 --- a/src/library/CMakeLists.txt +++ b/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) diff --git a/src/library/decl_stats.cpp b/src/library/decl_stats.cpp new file mode 100644 index 000000000..c38d90f62 --- /dev/null +++ b/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 m_num_occs; + name_map m_use_set; + name_map 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 & 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()); } +}; + +static decl_stats_ext_reg * g_ext = nullptr; +static decl_stats_ext const & get_extension(environment const & env) { + return static_cast(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(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; +} +} diff --git a/src/library/decl_stats.h b/src/library/decl_stats.h new file mode 100644 index 000000000..b2a1b41fd --- /dev/null +++ b/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(); +} diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index a24daf232..9a2378f96 100644 --- a/src/library/init_module.cpp +++ b/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(); diff --git a/src/library/module.cpp b/src/library/module.cpp index 93769e280..57f82f437 100644 --- a/src/library/module.cpp +++ b/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); diff --git a/src/library/shared_environment.cpp b/src/library/shared_environment.cpp index 96e90ef47..a925c7ed5 100644 --- a/src/library/shared_environment.cpp +++ b/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 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 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) {