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

feat(library/blast/simplifier/simplifier): move to new tracing framework

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-08 12:59:30 -08:00
parent 6b1469264d
commit e5a6bc5b85
5 changed files with 64 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/parser.cpp
View file

@ -1942,6 +1942,7 @@ void parser::parse_command() {
name const & cmd_name = get_token_info().value();
m_cmd_token = get_token_info().token();
if (auto it = cmds().find(cmd_name)) {
scope_trace_env scope(m_env, m_ios);
if (is_notation_cmd(cmd_name)) {
in_notation_ctx ctx(*this);
next();
@ -1950,7 +1951,6 @@ void parser::parse_command() {
} else {
next();
m_local_decls_size_at_beg_cmd = m_local_decls.size();
scope_trace_env scope(m_env, m_ios);
m_env = it->get_fn()(*this);
}
} else {

69
src/library/blast/simplifier/simplifier.cpp
View file

@ -13,6 +13,7 @@ Author: Daniel Selsam
#include "kernel/abstract.h"
#include "kernel/expr_maps.h"
#include "kernel/instantiate.h"
#include "library/trace.h"
#include "library/constants.h"
#include "library/normalize.h"
#include "library/expr_lt.h"
@ -46,9 +47,6 @@ Author: Daniel Selsam
#ifndef LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS
#define LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS false
#endif
#ifndef LEAN_DEFAULT_SIMPLIFY_TRACE
#define LEAN_DEFAULT_SIMPLIFY_TRACE false
#endif
#ifndef LEAN_DEFAULT_SIMPLIFY_FUSE
#define LEAN_DEFAULT_SIMPLIFY_FUSE false
#endif
@ -78,7 +76,6 @@ static name * g_simplify_exhaustive = nullptr;
static name * g_simplify_memoize = nullptr;
static name * g_simplify_contextual = nullptr;
static name * g_simplify_expand_macros = nullptr;
static name * g_simplify_trace = nullptr;
static name * g_simplify_fuse = nullptr;
static name * g_simplify_numerals = nullptr;
@ -106,10 +103,6 @@ bool get_simplify_expand_macros() {
return ios().get_options().get_bool(*g_simplify_expand_macros, LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS);
}
bool get_simplify_trace() {
return ios().get_options().get_bool(*g_simplify_trace, LEAN_DEFAULT_SIMPLIFY_TRACE);
}
bool get_simplify_fuse() {
return ios().get_options().get_bool(*g_simplify_fuse, LEAN_DEFAULT_SIMPLIFY_FUSE);
}
@ -153,7 +146,6 @@ class simplifier {
bool m_memoize{get_simplify_memoize()};
bool m_contextual{get_simplify_contextual()};
bool m_expand_macros{get_simplify_expand_macros()};
bool m_trace{get_simplify_trace()};
bool m_fuse{get_simplify_fuse()};
bool m_numerals{get_simplify_numerals()};
@ -196,9 +188,6 @@ class simplifier {
simp_rule_sets srss = _srss;
for (unsigned i = 0; i < ls.size(); i++) {
expr & l = ls[i];
if (m_trace) {
diagnostic(env(), ios()) << "Local: " << l << " : " << mlocal_type(l) << "\n";
}
tmp_type_context tctx(env(), ios());
try {
// TODO(Leo,Daniel): should we allow the user to set the priority of local lemmas
@ -385,11 +374,8 @@ result simplifier::simplify(expr const & e, simp_rule_sets const & srss) {
result simplifier::simplify(expr const & e, bool is_root) {
check_system("simplifier");
m_num_steps++;
flet<unsigned> inc_depth(m_depth, m_depth+1);
if (m_trace) {
diagnostic(env(), ios()) << m_depth << "." << m_rel << ": " << ppb(e) << "\n";
}
lean_trace_inc_depth("simplifier");
lean_trace_d("simplifier", tout() << m_rel << ": " << ppb(e) << "\n";);
if (m_num_steps > m_max_steps)
throw blast_exception("simplifier failed, maximum number of steps exceeded", e);
@ -613,13 +599,11 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
if (!tmp_tctx->is_def_eq(e, sr.get_lhs())) return result(e);
if (m_trace) {
expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs());
expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
diagnostic(env(), ios())
<< "REW(" << sr.get_id() << ") "
<< "[" << ppb(new_lhs) << " =?= " << ppb(new_rhs) << "]\n";
}
lean_trace(name({"simplifier", "rewrite"}),
expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs());
expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
tout() << "(" << sr.get_id() << ") "
<< "[" << ppb(new_lhs) << " =?= " << ppb(new_rhs) << "]\n";);
if (!instantiate_emetas(tmp_tctx, sr.get_num_emeta(), sr.get_emetas(), sr.get_instances())) return result(e);
@ -707,13 +691,12 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
if (!tmp_tctx->is_def_eq(e, cr.get_lhs())) return result(e);
if (m_trace) {
expr new_lhs = tmp_tctx->instantiate_uvars_mvars(cr.get_lhs());
expr new_rhs = tmp_tctx->instantiate_uvars_mvars(cr.get_rhs());
diagnostic(env(), ios())
<< "CONGR(" << cr.get_id() << ") "
<< "[" << ppb(new_lhs) << " =?= " << ppb(new_rhs) << "]\n";
}
lean_trace(name({"simplifier", "congruence"}),
expr new_lhs = tmp_tctx->instantiate_uvars_mvars(cr.get_lhs());
expr new_rhs = tmp_tctx->instantiate_uvars_mvars(cr.get_rhs());
diagnostic(env(), ios())
<< "(" << cr.get_id() << ") "
<< "[" << ppb(new_lhs) << " =?= " << ppb(new_rhs) << "]\n";);
/* First, iterate over the congruence hypotheses */
bool failed = false;
@ -779,16 +762,14 @@ bool simplifier::instantiate_emetas(blast_tmp_type_context & tmp_tctx, unsigned
if (is_instance) {
if (auto v = tmp_tctx->mk_class_instance(m_type)) {
if (!tmp_tctx->assign(m, *v)) {
if (m_trace) {
diagnostic(env(), ios()) << "unable to assign instance for: " << ppb(m_type) << "\n";
}
lean_trace(name({"simplifier", "failure"}),
tout() << "unable to assign instance for: " << ppb(m_type) << "\n";);
failed = true;
return;
}
} else {
if (m_trace) {
diagnostic(env(), ios()) << "unable to synthesize instance for: " << ppb(m_type) << "\n";
}
lean_trace(name({"simplifier", "failure"}),
tout() << "unable to synthesize instance for: " << ppb(m_type) << "\n";);
failed = true;
return;
}
@ -803,9 +784,8 @@ bool simplifier::instantiate_emetas(blast_tmp_type_context & tmp_tctx, unsigned
}
}
if (m_trace) {
diagnostic(env(), ios()) << "failed to assign: " << m << " : " << ppb(m_type) << "\n";
}
lean_trace(name({"simplifier", "failure"}),
tout() << "failed to assign: " << m << " : " << ppb(m_type) << "\n";);
failed = true;
return;
@ -1071,6 +1051,11 @@ expr_pair simplifier::split_summand(expr const & e, expr const & f_mul, expr con
/* Setup and teardown */
void initialize_simplifier() {
register_trace_class("simplifier");
register_trace_class(name({"simplifier", "rewrite"}));
register_trace_class(name({"simplifier", "congruence"}));
register_trace_class(name({"simplifier", "failure"}));
g_simplify_prove_namespace = new name{"simplifier", "prove"};
g_simplify_neg_namespace = new name{"simplifier", "neg"};
g_simplify_unit_namespace = new name{"simplifier", "unit"};
@ -1084,7 +1069,6 @@ void initialize_simplifier() {
g_simplify_memoize = new name{"simplify", "memoize"};
g_simplify_contextual = new name{"simplify", "contextual"};
g_simplify_expand_macros = new name{"simplify", "expand_macros"};
g_simplify_trace = new name{"simplify", "trace"};
g_simplify_fuse = new name{"simplify", "fuse"};
g_simplify_numerals = new name{"simplify", "numerals"};
@ -1100,8 +1084,6 @@ void initialize_simplifier() {
"(simplify) use contextual simplification");
register_bool_option(*g_simplify_expand_macros, LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS,
"(simplify) expand macros");
register_bool_option(*g_simplify_trace, LEAN_DEFAULT_SIMPLIFY_TRACE,
"(simplify) trace");
register_bool_option(*g_simplify_fuse, LEAN_DEFAULT_SIMPLIFY_FUSE,
"(simplify) fuse addition in distrib structures");
register_bool_option(*g_simplify_numerals, LEAN_DEFAULT_SIMPLIFY_NUMERALS,
@ -1111,7 +1093,6 @@ void initialize_simplifier() {
void finalize_simplifier() {
delete g_simplify_numerals;
delete g_simplify_fuse;
delete g_simplify_trace;
delete g_simplify_expand_macros;
delete g_simplify_contextual;
delete g_simplify_memoize;

21
src/library/trace.cpp
View file

@ -38,14 +38,16 @@ bool is_trace_enabled() {
void enable_trace_class(name const & c) {
std::vector<name> & cs = get_enabled_trace_classes();
if (std::find(cs.begin(), cs.end(), c) == cs.end())
if (std::find(cs.begin(), cs.end(), c) == cs.end()) {
cs.push_back(c);
}
}
bool is_trace_class_enabled_core(name const & n) {
for (name const & p : get_enabled_trace_classes()) {
if (is_prefix_of(p, n))
if (is_prefix_of(p, n)) {
return true;
}
}
return false;
}
@ -99,6 +101,21 @@ scope_trace_inc_depth::~scope_trace_inc_depth() {
g_depth--;
}
scope_trace_init_bool_option::scope_trace_init_bool_option(name const & n, bool v) {
m_old_ios = g_ios;
if (g_env && g_ios) {
m_tmp_ios = *g_ios;
options o = m_tmp_ios.get_options();
o = o.update_if_undef(n, v);
m_tmp_ios.set_options(o);
g_ios = &m_tmp_ios;
}
}
scope_trace_init_bool_option::~scope_trace_init_bool_option() {
g_ios = const_cast<io_state*>(m_old_ios);
}
io_state_stream tout() {
if (g_env) {
return diagnostic(*g_env, *g_ios);

27
src/library/trace.h
View file

@ -29,10 +29,19 @@ public:
void activate();
};
/* Temporarily set an option if it is not already set in the trace environment. */
class scope_trace_init_bool_option {
io_state const * m_old_ios;
io_state m_tmp_ios;
public:
scope_trace_init_bool_option(name const & n, bool v);
~scope_trace_init_bool_option();
};
#define lean_trace_inc_depth(CName) \
scope_trace_inc_depth trace_inc_depth_helper; \
scope_trace_inc_depth trace_inc_depth_helper ## __LINE__; \
if (is_trace_enabled() && is_trace_class_enabled(name(CName))) \
trace_inc_depth_helper.activate();
trace_inc_depth_helper ## __LINE__.activate();
struct tdepth {};
struct tclass { name m_cls; tclass(name const & c):m_cls(c) {} };
@ -41,21 +50,21 @@ io_state_stream tout();
io_state_stream const & operator<<(io_state_stream const & ios, tdepth const &);
io_state_stream const & operator<<(io_state_stream const & ios, tclass const &);
#define lean_is_trace_enabled(CName) (is_trace_enabled() && is_trace_class_enabled(name(CName)))
#define lean_is_trace_enabled(CName) (::lean::is_trace_enabled() && ::lean::is_trace_class_enabled(CName))
#define lean_trace_core(CName, CODE) { \
if (lean_is_trace_class_enabled(CName)) { \
#define lean_trace_plain(CName, CODE) { \
if (lean_is_trace_enabled(CName)) { \
CODE \
}}
#define lean_trace(CName, CODE) { \
if (lean_is_trace_enabled(CName)) { \
tout() << tclass(name(CName)); CODE \
tout() << tclass(CName); CODE \
}}
#define lean_dtrace(CName, CODE) { \
if (lean_is_trace_enabled(CName)) { \
tout() << tdepth() << tclass(name(CName)); CODE \
#define lean_trace_d(CName, CODE) { \
if (lean_is_trace_enabled(CName)) { \
tout() << tdepth() << tclass(CName); CODE \
}}
void initialize_trace();

1
src/library/type_context.cpp
View file

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "kernel/abstract.h"
#include "kernel/for_each_fn.h"
#include "kernel/inductive/inductive.h"
#include "library/trace.h"
#include "library/projection.h"
#include "library/normalize.h"
#include "library/replace_visitor.h"