michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/meng_paulson): ignore class and class-instances when computing set of relevant theorems

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-14 20:46:03 -07:00
parent 023ec1ba76
commit ee347772d7
5 changed files with 101 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/builtin_cmds.cpp
View file

@ -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;
}

9
src/library/class.cpp
View file

@ -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<name> & 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;
}

35
src/library/decl_stats.cpp
View file

@ -4,12 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <string>
#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<unsigned> m_num_occs;
name_map<name_set> m_use_set;
name_map<name_set> 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<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> &) {
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;
}
}

6
src/library/decl_stats.h
View file

@ -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();
}

60
src/library/meng_paulson.cpp
View file

@ -14,8 +14,11 @@ the approach described at
#include <math.h>
#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;