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

feat(library): remove decl_stats

Browse source 
We are not using (and will not use) this module in the blast proof procedures
This commit is contained in:
Leonardo de Moura 2016-01-02 12:59:42 -08:00
parent befe41e8f5
commit 155df48665
10 changed files with 4 additions and 465 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -22,8 +22,6 @@ Author: Leonardo de Moura
#include "library/pp_options.h"
#include "library/aux_recursors.h"
#include "library/private.h"
#include "library/decl_stats.h"
#include "library/meng_paulson.h"
#include "library/fun_info_manager.h"
#include "library/congr_lemma_manager.h"
#include "library/abstract_expr_manager.h"
@ -551,54 +549,6 @@ 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();
io_state_stream out = p.regular_stream();
out << "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()));
});
out << "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;
}
static environment relevant_thms_cmd(parser & p) {
environment const & env = p.env();
name_set R;
while (p.curr_is_identifier()) {
R.insert(p.check_constant_next("invalid #relevant_thms command, constant expected"));
}
name_set TS = get_relevant_thms(env, p.get_options(), R);
io_state_stream out = p.regular_stream();
TS.for_each([&](name const & T) {
out << T << "\n";
});
return env;
}
static void check_expr_and_print(parser & p, expr const & e) {
environment const & env = p.env();
type_checker tc(env);
@ -903,8 +853,6 @@ void init_cmd_table(cmd_table & r) {
add_cmd(r, cmd_info("#congr_rel", "(for debugging purposes)", congr_rel_cmd));
add_cmd(r, cmd_info("#normalizer", "(for debugging purposes)", normalizer_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));
add_cmd(r, cmd_info("#relevant_thms", "(for debugging purposes) select relevant theorems using Meng&Paulson heuristic", relevant_thms_cmd));
add_cmd(r, cmd_info("#simplify", "(for debugging purposes) simplify given expression", simplify_cmd));
add_cmd(r, cmd_info("#abstract_expr", "(for debugging purposes) call abstract expr methods", abstract_expr_cmd));

3
src/library/CMakeLists.txt
View file

@ -15,8 +15,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp
relation_manager.cpp export.cpp user_recursors.cpp idx_metavar.cpp
composition_manager.cpp tc_multigraph.cpp noncomputable.cpp
aux_recursors.cpp norm_num.cpp decl_stats.cpp meng_paulson.cpp
norm_num.cpp class_instance_resolution.cpp type_context.cpp
aux_recursors.cpp norm_num.cpp norm_num.cpp class_instance_resolution.cpp type_context.cpp
tmp_type_context.cpp fun_info_manager.cpp congr_lemma_manager.cpp
abstract_expr_manager.cpp light_lt_manager.cpp trace.cpp
attribute_manager.cpp error_handling.cpp)

11
src/library/class.cpp
View file

@ -15,7 +15,6 @@ Author: Leonardo de Moura
#include "library/tc_multigraph.h"
#include "library/protected.h"
#include "library/class.h"
#include "library/decl_stats.h"
#include "library/attribute_manager.h"
namespace lean {
@ -234,8 +233,7 @@ name get_class_name(environment const & env, expr const & e) {
environment add_class(environment const & env, name const & n, name const & ns, bool persistent) {
check_class(env, n);
environment new_env = class_ext::add_entry(env, get_dummy_ios(), class_entry(n), ns, persistent);
return mark_class_instance_somewhere(new_env, n);
return class_ext::add_entry(env, get_dummy_ios(), class_entry(n), ns, persistent);
}
void get_classes(environment const & env, buffer<name> & classes) {
@ -272,9 +270,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);
environment new_env = class_ext::add_entry(env, get_dummy_ios(), class_entry(class_entry_kind::Instance, c, n, priority),
ns, persistent);
return mark_class_instance_somewhere(new_env, n);
return class_ext::add_entry(env, get_dummy_ios(), class_entry(class_entry_kind::Instance, c, n, priority),
ns, persistent);
}
environment add_instance(environment const & env, name const & n, name const & ns, bool persistent) {
@ -314,13 +311,11 @@ 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), ns, 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), ns, persistent);
new_env = set_reducible(new_env, edge.m_cnst, reducible_status::Reducible, ns, persistent);
new_env = add_protected(new_env, edge.m_cnst);
new_env = mark_class_instance_somewhere(new_env, edge.m_cnst);
}
return new_env;
}

157
src/library/decl_stats.cpp
View file

@ -1,157 +0,0 @@
/*
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 <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;
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 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);
}
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();
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;
}
}

31
src/library/decl_stats.h
View file

@ -1,31 +0,0 @@
/*
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);
/** \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();
}

6
src/library/init_module.cpp
View file

@ -42,8 +42,6 @@ Author: Leonardo de Moura
#include "library/composition_manager.h"
#include "library/noncomputable.h"
#include "library/aux_recursors.h"
#include "library/decl_stats.h"
#include "library/meng_paulson.h"
#include "library/class_instance_resolution.h"
#include "library/type_context.h"
#include "library/congr_lemma_manager.h"
@ -90,8 +88,6 @@ void initialize_library_module() {
initialize_composition_manager();
initialize_noncomputable();
initialize_aux_recursors();
initialize_decl_stats();
initialize_meng_paulson();
initialize_class_instance_resolution();
initialize_type_context();
initialize_light_rule_set();
@ -105,8 +101,6 @@ void finalize_library_module() {
finalize_light_rule_set();
finalize_type_context();
finalize_class_instance_resolution();
finalize_meng_paulson();
finalize_decl_stats();
finalize_aux_recursors();
finalize_noncomputable();
finalize_composition_manager();

188
src/library/meng_paulson.cpp
View file

@ -1,188 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
This module implements a heuristic for selecting relevant theorems based on
the approach described at
"Lightweight relevance filtering for machine-generated resolution problems"
Jia Meng and Larry Paulson
Journal of Applied Logic 7 2009
*/
#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
#endif
#ifndef LEAN_DEFAULT_MENG_PAULSON_C
#define LEAN_DEFAULT_MENG_PAULSON_C 2.4
#endif
namespace lean {
static name * g_meng_paulson_p = nullptr;
static name * g_meng_paulson_c = nullptr;
void initialize_meng_paulson() {
g_meng_paulson_p = new name{"meng_paulson", "p"};
g_meng_paulson_c = new name{"meng_paulson", "c"};
register_double_option(*g_meng_paulson_p, LEAN_DEFAULT_MENG_PAULSON_P,
"(theorem selection) control parameter for the Meng&Paulson theorem selection heuristic"
"(for details see paper \"Lightweight relevance filtering for machine-generated resolution problems)\"");
register_double_option(*g_meng_paulson_c, LEAN_DEFAULT_MENG_PAULSON_C,
"(theorem selection) control parameter for the Meng&Paulson theorem selection heuristic"
"(for details see paper \"Lightweight relevance filtering for machine-generated resolution problems)\"");
}
void finalize_meng_paulson() {
delete g_meng_paulson_p;
delete g_meng_paulson_c;
}
double get_meng_paulson_p(options const & o) {
return o.get_double(*g_meng_paulson_p, LEAN_DEFAULT_MENG_PAULSON_P);
}
double get_meng_paulson_c(options const & o) {
return o.get_double(*g_meng_paulson_c, LEAN_DEFAULT_MENG_PAULSON_C);
}
class relevant_thms_fn {
environment m_env;
double m_p;
double m_c;
name_set m_relevant;
double get_weight(name const & n) const {
double r = get_num_occs(m_env, n);
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
return 0.0;
}
public:
relevant_thms_fn(environment const & env, double p, double c, name_set const & rel):
m_env(env), m_p(p), m_c(c), m_relevant(rel) {
lean_assert(c > 0.0);
}
name_set operator()() {
name_set A;
name_set Fs = m_relevant;
// unsigned i = 1;
while (true) {
// std::cout << "#" << i << ", p: " << m_p << "\n";
name_set Rel;
Fs.for_each([&](name const & F) {
name_set used_by = get_used_by_set(m_env, F);
used_by.for_each([&](name const & T) {
declaration const & T_decl = m_env.get(T);
if (A.contains(T))
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 (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);
A.insert(T);
});
});
if (Rel.empty())
break;
// include symbols of new theorems in m_relevant
Fs = name_set(); // reset Fs
Rel.for_each([&](name const & T) {
name_set uses = get_use_set(m_env, T);
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 (ignore_F(F))
return;
// if (!m_relevant.contains(F))
// std::cout << "new relevant: " << F << "\n";
m_relevant.insert(F);
Fs.insert(F);
});
});
m_p = m_p + (1.0 - m_p) / m_c;
}
return A;
}
};
name_set get_relevant_thms(environment const & env, double p, double c,
name_set const & relevant_symbols) {
return relevant_thms_fn(env, p, c, relevant_symbols)();
}
name_set get_relevant_thms(environment const & env, options const & o, name_set const & relevant_symbols) {
return relevant_thms_fn(env, get_meng_paulson_p(o), get_meng_paulson_c(o), relevant_symbols)();
}
}

16
src/library/meng_paulson.h
View file

@ -1,16 +0,0 @@
/*
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
#include "util/name_set.h"
#include "kernel/environment.h"
namespace lean {
name_set get_relevant_thms(environment const & env, double p, double c, name_set const & relevant_symbols);
name_set get_relevant_thms(environment const & env, options const & o, name_set const & relevant_symbols);
void initialize_meng_paulson();
void finalize_meng_paulson();
}

2
src/library/module.cpp
View file

@ -29,7 +29,6 @@ Author: Leonardo de Moura
#include "library/constants.h"
#include "library/kernel_serializer.h"
#include "library/unfold_macros.h"
#include "library/decl_stats.h"
#include "version.h"
#ifndef LEAN_ASYNCH_IMPORT_THEOREM
@ -223,7 +222,6 @@ 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);

3
src/library/shared_environment.cpp
View file

@ -5,7 +5,6 @@ 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() {}
@ -19,13 +18,11 @@ 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) {