From ee347772d78c268004fe2d2d93c62d8000c1c2fa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 Oct 2015 20:46:03 -0700 Subject: [PATCH] feat(library/meng_paulson): ignore class and class-instances when computing set of relevant theorems --- src/frontends/lean/builtin_cmds.cpp | 9 +---- src/library/class.cpp | 9 ++++- src/library/decl_stats.cpp | 35 ++++++++++++++++- src/library/decl_stats.h | 6 +++ src/library/meng_paulson.cpp | 60 +++++++++++++++++++++++++---- 5 files changed, 101 insertions(+), 18 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 8b3b5d665..54e0b9b78 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -1132,16 +1132,9 @@ static environment relevant_thms_cmd(parser & p) { } name_set TS = get_relevant_thms(env, p.get_options(), R); io_state_stream out = p.regular_stream(); - out << "{"; - bool first = true; TS.for_each([&](name const & T) { - if (first) - first = false; - else - out << ", "; - out << T; + out << T << "\n"; }); - out << "}"; return env; } diff --git a/src/library/class.cpp b/src/library/class.cpp index d31aa93ef..0947f022a 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "library/tc_multigraph.h" #include "library/protected.h" #include "library/class.h" +#include "library/decl_stats.h" #ifndef LEAN_INSTANCE_DEFAULT_PRIORITY #define LEAN_INSTANCE_DEFAULT_PRIORITY 1000 @@ -236,7 +237,8 @@ name get_class_name(environment const & env, expr const & e) { environment add_class(environment const & env, name const & n, bool persistent) { check_class(env, n); - return class_ext::add_entry(env, get_dummy_ios(), class_entry(n), persistent); + environment new_env = class_ext::add_entry(env, get_dummy_ios(), class_entry(n), persistent); + return mark_class_instance_somewhere(new_env, n); } void get_classes(environment const & env, buffer & classes) { @@ -273,7 +275,8 @@ environment add_instance(environment const & env, name const & n, unsigned prior } name c = get_class_name(env, get_app_fn(type)); check_is_class(env, c); - return class_ext::add_entry(env, get_dummy_ios(), class_entry(class_entry_kind::Instance, c, n, priority), persistent); + environment new_env = class_ext::add_entry(env, get_dummy_ios(), class_entry(class_entry_kind::Instance, c, n, priority), persistent); + return mark_class_instance_somewhere(new_env, n); } environment add_instance(environment const & env, name const & n, bool persistent) { @@ -313,11 +316,13 @@ environment add_trans_instance(environment const & env, name const & n, unsigned environment new_env = new_env_insts.first; new_env = class_ext::add_entry(new_env, get_dummy_ios(), class_entry::mk_trans_inst(src_tgt.first, src_tgt.second, n, priority), persistent); + new_env = mark_class_instance_somewhere(new_env, n); for (tc_edge const & edge : new_env_insts.second) { new_env = class_ext::add_entry(new_env, get_dummy_ios(), class_entry::mk_derived_trans_inst(edge.m_from, edge.m_to, edge.m_cnst), persistent); new_env = set_reducible(new_env, edge.m_cnst, reducible_status::Reducible, persistent); new_env = add_protected(new_env, edge.m_cnst); + new_env = mark_class_instance_somewhere(new_env, edge.m_cnst); } return new_env; } diff --git a/src/library/decl_stats.cpp b/src/library/decl_stats.cpp index c38d90f62..9520fa079 100644 --- a/src/library/decl_stats.cpp +++ b/src/library/decl_stats.cpp @@ -4,12 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "kernel/environment.h" #include "kernel/for_each_fn.h" #include "library/reducible.h" +#include "library/module.h" namespace lean { struct decl_stats_ext : public environment_extension { + name_set m_class_instance; // set of all classes and class instances declared in some namespace name_map m_num_occs; name_map m_use_set; name_map m_used_by_set; @@ -89,6 +92,33 @@ public: } }; +environment mark_class_instance_somewhere_core(environment const & env, name const & n) { + decl_stats_ext ext = get_extension(env); + ext.m_class_instance.insert(n); + return update(env, ext); +} + +static std::string * g_key = nullptr; + +environment mark_class_instance_somewhere(environment const & env, name const & n) { + environment new_env = mark_class_instance_somewhere_core(env, n); + return module::add(new_env, *g_key, [=](environment const &, serializer & s) { s << n; }); +} + +bool is_class_instance_somewhere(environment const & env, name const & n) { + return get_extension(env).m_class_instance.contains(n); +} + +static void class_instance_mark_reader(deserializer & d, shared_environment & senv, + std::function &, + std::function &) { + name n; + d >> n; + senv.update([=](environment const & env) -> environment { + return mark_class_instance_somewhere_core(env, n); + }); +} + environment update_decl_stats(environment const & env, declaration const & d) { return update_decl_stats_fn(env)(d); } @@ -115,10 +145,13 @@ name_set get_used_by_set(environment const & env, name const & n) { } void initialize_decl_stats() { - g_ext = new decl_stats_ext_reg(); + g_ext = new decl_stats_ext_reg(); + g_key = new std::string("CIGLB"); + register_module_object_reader(*g_key, class_instance_mark_reader); } void finalize_decl_stats() { delete g_ext; + delete g_key; } } diff --git a/src/library/decl_stats.h b/src/library/decl_stats.h index b2a1b41fd..90f7d7f44 100644 --- a/src/library/decl_stats.h +++ b/src/library/decl_stats.h @@ -20,6 +20,12 @@ unsigned get_num_occs(environment const & env, name const & 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); + +/** \brief Mark that \c n is a class or class-instance in some namespace. */ +environment mark_class_instance_somewhere(environment const & env, name const & n); +/** \brief Return true iff \c n is a class or class-instance in some namespace. */ +bool is_class_instance_somewhere(environment const & env, name const & n); + void initialize_decl_stats(); void finalize_decl_stats(); } diff --git a/src/library/meng_paulson.cpp b/src/library/meng_paulson.cpp index 0ed8254cb..a80272d8b 100644 --- a/src/library/meng_paulson.cpp +++ b/src/library/meng_paulson.cpp @@ -14,8 +14,11 @@ the approach described at #include #include "util/sexpr/option_declarations.h" #include "kernel/environment.h" +#include "kernel/inductive/inductive.h" #include "library/decl_stats.h" #include "library/private.h" +#include "library/class.h" +#include "library/constants.h" #ifndef LEAN_DEFAULT_MENG_PAULSON_P #define LEAN_DEFAULT_MENG_PAULSON_P 0.6 @@ -65,17 +68,55 @@ class relevant_thms_fn { return 1.0 + 2.0 / log(r + 1.0); } + bool is_connective(name const & n) const { + return + n == get_or_name() || + n == get_and_name() || + n == get_not_name() || + n == get_iff_name() || + n == get_not_name() || + n == get_ite_name() || + n == get_true_name() || + n == get_false_name(); + } + + // constants symbols in theorem types that should be ignored + bool ignore_F(name const & F) const { + if (is_private(m_env, F)) + return true; // we ignore private decls + if (is_class_instance_somewhere(m_env, F)) + return true; // ignore if F is a class or class-instance in some namespace + if (is_connective(F)) + return true; + return false; + } + + // Theorems/Axioms that should be ignored + bool ignore_T(name const & T) const { + if (is_private(m_env, T)) + return true; + if (inductive::is_elim_rule(m_env, T)) + return true; + if (inductive::is_intro_rule(m_env, T)) + return true; + return false; + } + double get_thm_score(name const & n) const { name_set s = get_use_set(m_env, n); unsigned IR = 0; double M = 0.0; s.for_each([&](name const & F) { + if (ignore_F(F)) + return; if (m_relevant.contains(F)) { M += get_weight(F); } else { + // std::cout << "IR: " << F << "\n"; IR++; } }); + // std::cout << n << " M: " << M << " IR: " << IR << "\n"; if (M > 0.0) return M / (M + IR); else @@ -89,7 +130,9 @@ public: name_set operator()() { name_set A; + // unsigned i = 1; while (true) { + // std::cout << "#" << i << ", p: " << m_p << "\n"; name_set Rel; m_relevant.for_each([&](name const & c) { name_set used_by = get_used_by_set(m_env, c); @@ -99,9 +142,10 @@ public: return; // T is already in the result set if (!T_decl.is_theorem() && !T_decl.is_axiom()) return; // we only care about axioms and theorems - if (is_private(m_env, T)) + if (ignore_T(T)) return; // we ignore private decls double M = get_thm_score(T); + // std::cout << T << " : " << M << "\n"; if (M < m_p) return; // score is to low Rel.insert(T); @@ -114,13 +158,15 @@ public: // include symbols of new theorems in m_relevant Rel.for_each([&](name const & T) { name_set uses = get_use_set(m_env, T); - uses.for_each([&](name const & c) { - declaration const & c_decl = m_env.get(c); - if (c_decl.is_theorem() || c_decl.is_axiom()) + uses.for_each([&](name const & F) { + declaration const & F_decl = m_env.get(F); + if (F_decl.is_theorem() || F_decl.is_axiom()) return; // we ignore theorems occurring in types - if (is_private(m_env, c)) - return; // we ignore private decls - m_relevant.insert(c); + if (ignore_F(F)) + return; + // if (!m_relevant.contains(F)) + // std::cout << "new relevant: " << F << "\n"; + m_relevant.insert(F); }); }); m_p = m_p + (1.0 - m_p) / m_c;