From 429527eb7272aed7b21880be136fa939312e4e6c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 8 Dec 2015 19:37:06 -0800 Subject: [PATCH] refactor(library/blast): move to new tracing infrastructure --- src/library/blast/blast.cpp | 5 ++- src/library/blast/forward/ematch.cpp | 7 ++-- src/library/blast/options.cpp | 24 ----------- src/library/blast/options.h | 2 - src/library/blast/state.cpp | 9 ++++- src/library/blast/state.h | 3 +- .../blast/strategies/preprocess_strategy.cpp | 6 +-- src/library/blast/strategy.cpp | 17 ++++---- src/library/blast/trace.cpp | 40 ++++--------------- src/library/blast/trace.h | 12 +----- src/library/trace.cpp | 33 ++++++++++----- src/library/trace.h | 14 +++++-- 12 files changed, 71 insertions(+), 101 deletions(-) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index e5b6a1a27..94e647d4b 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -1045,7 +1045,6 @@ struct scope_debug::imp { scope_blastenv m_scope2; scope_congruence_closure m_scope3; scope_config m_scope4; - scope_trace m_scope5; imp(environment const & env, io_state const & ios): m_scope1(true), m_benv(env, ios, list(), list()), @@ -1144,13 +1143,15 @@ optional blast_goal(environment const & env, io_state const & ios, list #include "util/interrupt.h" +#include "library/trace.h" #include "library/constants.h" #include "library/idx_metavar.h" #include "library/head_map.h" @@ -122,6 +123,7 @@ struct noop_proof_step_cell : public proof_step_cell { void initialize_ematch() { g_ext_id = register_branch_extension(new ematch_branch_extension()); + register_trace_class(name{"blast", "ematch"}); } void finalize_ematch() {} @@ -303,9 +305,7 @@ struct ematch_fn { if (!m_new_instances) { trace_action("ematch"); } - if (is_trace_enabled()) { - diagnostic(env(), ios()) << "ematch_instance: " << ppb(new_inst) << "\n"; - } + lean_trace(name({"blast", "ematch"}), tout() << "ematch_instance: " << ppb(new_inst) << "\n";); m_new_instances = true; expr new_proof = m_ctx->instantiate_uvars_mvars(lemma.m_proof); m_ext.m_instances.insert(new_inst); @@ -390,7 +390,6 @@ struct ematch_fn { m_cc.inc_gmt(); if (m_new_instances) { curr_state().push_proof_step(new noop_proof_step_cell()); - trace(""); return action_result::new_branch(); } else { return action_result::failed(); diff --git a/src/library/blast/options.cpp b/src/library/blast/options.cpp index 32c05c4c3..a87671660 100644 --- a/src/library/blast/options.cpp +++ b/src/library/blast/options.cpp @@ -17,12 +17,6 @@ Author: Leonardo de Moura #ifndef LEAN_DEFAULT_BLAST_INC_DEPTH #define LEAN_DEFAULT_BLAST_INC_DEPTH 5 #endif -#ifndef LEAN_DEFAULT_BLAST_TRACE -#define LEAN_DEFAULT_BLAST_TRACE false -#endif -#ifndef LEAN_DEFAULT_BLAST_TRACE_PREPROCESSOR -#define LEAN_DEFAULT_BLAST_TRACE_PREPROCESSOR false -#endif #ifndef LEAN_DEFAULT_BLAST_SHOW_FAILURE #define LEAN_DEFAULT_BLAST_SHOW_FAILURE true #endif @@ -57,8 +51,6 @@ namespace blast { static name * g_blast_max_depth = nullptr; static name * g_blast_init_depth = nullptr; static name * g_blast_inc_depth = nullptr; -static name * g_blast_trace = nullptr; -static name * g_blast_trace_pre = nullptr; static name * g_blast_subst = nullptr; static name * g_blast_simp = nullptr; static name * g_blast_cc = nullptr; @@ -78,12 +70,6 @@ unsigned get_blast_init_depth(options const & o) { unsigned get_blast_inc_depth(options const & o) { return o.get_unsigned(*g_blast_inc_depth, LEAN_DEFAULT_BLAST_INC_DEPTH); } -bool get_blast_trace(options const & o) { - return o.get_bool(*g_blast_trace, LEAN_DEFAULT_BLAST_TRACE); -} -bool get_blast_trace_pre(options const & o) { - return o.get_bool(*g_blast_trace_pre, LEAN_DEFAULT_BLAST_TRACE_PREPROCESSOR); -} bool get_blast_subst(options const & o) { return o.get_bool(*g_blast_subst, LEAN_DEFAULT_BLAST_SUBST); } @@ -116,8 +102,6 @@ config::config(options const & o) { m_max_depth = get_blast_max_depth(o); m_init_depth = get_blast_init_depth(o); m_inc_depth = get_blast_inc_depth(o); - m_trace = get_blast_trace(o); - m_trace_pre = get_blast_trace_pre(o); m_subst = get_blast_subst(o); m_simp = get_blast_simp(o); m_cc = get_blast_cc(o); @@ -150,8 +134,6 @@ void initialize_options() { g_blast_max_depth = new name{"blast", "max_depth"}; g_blast_init_depth = new name{"blast", "init_depth"}; g_blast_inc_depth = new name{"blast", "inc_depth"}; - g_blast_trace = new name{"blast", "trace"}; - g_blast_trace_pre = new name{"blast", "trace_preprocessor"}; g_blast_subst = new name{"blast", "subst"}; g_blast_simp = new name{"blast", "simp"}; g_blast_cc = new name{"blast", "cc"}; @@ -168,10 +150,6 @@ void initialize_options() { "(blast) initial search depth for blast (remark: blast uses iteration deepening)"); register_unsigned_option(*blast::g_blast_inc_depth, LEAN_DEFAULT_BLAST_INC_DEPTH, "(blast) search depth increment for blast (remark: blast uses iteration deepening)"); - register_bool_option(*blast::g_blast_trace, LEAN_DEFAULT_BLAST_TRACE, - "(blast) trace"); - register_bool_option(*blast::g_blast_trace_pre, LEAN_DEFAULT_BLAST_TRACE_PREPROCESSOR, - "(blast) trace preprocessor"); register_bool_option(*blast::g_blast_subst, LEAN_DEFAULT_BLAST_SUBST, "(blast) enable subst action"); register_bool_option(*blast::g_blast_simp, LEAN_DEFAULT_BLAST_SIMP, @@ -197,8 +175,6 @@ void finalize_options() { delete g_blast_max_depth; delete g_blast_init_depth; delete g_blast_inc_depth; - delete g_blast_trace; - delete g_blast_trace_pre; delete g_blast_subst; delete g_blast_simp; delete g_blast_cc; diff --git a/src/library/blast/options.h b/src/library/blast/options.h index e16ed4e49..35c41c3be 100644 --- a/src/library/blast/options.h +++ b/src/library/blast/options.h @@ -14,8 +14,6 @@ struct config { unsigned m_max_depth; unsigned m_init_depth; unsigned m_inc_depth; - bool m_trace; - bool m_trace_pre; bool m_subst; bool m_simp; bool m_recursor; diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 4d1f9878e..c49024a5e 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -277,7 +277,7 @@ goal state::to_goal() const { return goal(new_meta, new_target); } -void state::display_active(output_channel & out) const { +void state::display_active(std::ostream & out) const { out << "active := {"; bool first = true; m_branch.m_active.for_each([&](hypothesis_idx hidx) { @@ -287,11 +287,16 @@ void state::display_active(output_channel & out) const { out << "}\n"; } +void state::display(io_state_stream const & ios) const { + ios << mk_pair(to_goal().pp(ios.get_formatter()), ios.get_options()) << "\n"; + display_active(ios.get_stream()); +} + void state::display(environment const & env, io_state const & ios) const { formatter fmt = ios.get_formatter_factory()(env, ios.get_options()); auto & out = ios.get_diagnostic_channel(); out << mk_pair(to_goal().pp(fmt), ios.get_options()) << "\n"; - display_active(out); + display_active(out.get_stream()); } bool state::has_assigned_uref(level const & l) const { diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 4244ea052..0b7617896 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -206,7 +206,7 @@ class state { void del_hypotheses(buffer const & to_delete, hypothesis_idx_set const & to_delete_set); bool safe_to_delete(buffer const & to_delete); - void display_active(output_channel & out) const; + void display_active(std::ostream & out) const; branch_extension * get_extension_core(unsigned i); @@ -463,6 +463,7 @@ public: and types can be inferred by pretty printer. */ expr to_kernel_expr(expr const & e) const; + void display(io_state_stream const & ios) const; void display(environment const & env, io_state const & ios) const; #ifdef LEAN_DEBUG diff --git a/src/library/blast/strategies/preprocess_strategy.cpp b/src/library/blast/strategies/preprocess_strategy.cpp index c56ce1ade..d3de6e5aa 100644 --- a/src/library/blast/strategies/preprocess_strategy.cpp +++ b/src/library/blast/strategies/preprocess_strategy.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "library/trace.h" #include "library/blast/trace.h" #include "library/blast/options.h" #include "library/blast/choice_point.h" @@ -57,7 +58,6 @@ class preprocess_strategy_fn : public strategy_fn { } if (get_num_choice_points() > get_initial_num_choice_points()) throw exception("invalid blast preprocessing action, preprocessing actions should not create choice points"); - scope_trace s(get_config().m_trace); if (optional pf = m_main()) { return action_result::solved(*pf); } return action_result::failed(); } @@ -67,10 +67,10 @@ public: }; strategy preprocess_and_then(strategy const & S) { - return [=]() { scope_trace s(get_config().m_trace_pre); return preprocess_strategy_fn(S, false)(); }; // NOLINT + return [=]() { return preprocess_strategy_fn(S, false)(); }; // NOLINT } strategy basic_preprocess_and_then(strategy const & S) { - return [=]() { scope_trace s(get_config().m_trace_pre); return preprocess_strategy_fn(S, true)(); }; // NOLINT + return [=]() { return preprocess_strategy_fn(S, true)(); }; // NOLINT } }} diff --git a/src/library/blast/strategy.cpp b/src/library/blast/strategy.cpp index 974889032..e3eb8f112 100644 --- a/src/library/blast/strategy.cpp +++ b/src/library/blast/strategy.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/interrupt.h" +#include "library/trace.h" #include "library/blast/strategy.h" #include "library/blast/choice_point.h" #include "library/blast/blast.h" @@ -33,7 +34,7 @@ action_result strategy_fn::next_branch(expr pr) { action_result r = s.resolve(unfold_hypotheses_ge(curr_state(), pr)); switch (r.get_kind()) { case action_result::Failed: - trace(">>> next-branch FAILED <<<"); + trace_search(">>> next-branch FAILED <<<"); return r; case action_result::Solved: pr = r.get_proof(); @@ -56,9 +57,7 @@ optional strategy_fn::search() { m_init_num_choices = get_num_choice_points(); unsigned init_proof_depth = curr_state().get_proof_depth(); unsigned max_depth = get_config().m_max_depth; - if (is_trace_enabled()) { - ios().get_diagnostic_channel() << "* Search upto depth " << max_depth << "\n\n"; - } + lean_trace(name({"blast", "search"}), tout() << "search upto depth " << max_depth << "\n";); trace_curr_state(); action_result r = next_action(); trace_curr_state_if(r); @@ -66,7 +65,7 @@ optional strategy_fn::search() { check_system("blast"); lean_assert(curr_state().check_invariant()); if (curr_state().get_proof_depth() > max_depth) { - trace(">>> maximum search depth reached <<<"); + trace_search(">>> maximum search depth reached <<<"); r = action_result::failed(); } switch (r.get_kind()) { @@ -74,21 +73,21 @@ optional strategy_fn::search() { r = next_choice_point(m_init_num_choices); if (failed(r)) { // all choice points failed... - trace(">>> proof not found, no choice points left <<<"); + trace_search(">>> proof not found, no choice points left <<<"); if (show_failure()) display_curr_state(); return none_expr(); } - trace("* next choice point"); + trace_search("* next choice point"); break; case action_result::Solved: r = next_branch(r.get_proof()); if (r.get_kind() == action_result::Solved) { // all branches have been solved - trace("* found proof"); + trace_search("* found proof"); return some_expr(unfold_hypotheses_ge(curr_state(), r.get_proof(), init_proof_depth)); } - trace("* next branch"); + trace_search("* next branch"); break; case action_result::NewBranch: r = next_action(); diff --git a/src/library/blast/trace.cpp b/src/library/blast/trace.cpp index 6d83708ff..5a5b9b41f 100644 --- a/src/library/blast/trace.cpp +++ b/src/library/blast/trace.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "library/trace.h" #include "library/io_state_stream.h" #include "library/blast/blast.h" #include "library/blast/choice_point.h" @@ -12,50 +13,25 @@ Author: Leonardo de Moura namespace lean { namespace blast { -LEAN_THREAD_VALUE(bool, g_trace, false); - -bool is_trace_enabled() { - return g_trace; -} - void trace_curr_state() { - if (g_trace) { - auto out = diagnostic(env(), ios()); - out << "state [" << curr_state().get_proof_depth() << "], #choice: " << get_num_choice_points() << "\n"; - display_curr_state(); - } + lean_trace(name({"blast", "state"}), + tout() << "[" << curr_state().get_proof_depth() << "], #choice: " << get_num_choice_points() << "\n"; + curr_state().display(tout());); } -void trace(char const * msg) { - if (g_trace) { - ios().get_diagnostic_channel() << msg << "\n\n"; - } +void trace_search(char const * msg) { + lean_trace(name({"blast", "search"}), tout() << msg << "\n";); } void trace_action(char const * a) { - if (g_trace) { - ios().get_diagnostic_channel() << "== action: " << a << " ==>\n\n"; - } + lean_trace(name({"blast", "action"}), tout() << a << "\n";); } void trace_curr_state_if(action_result r) { - if (g_trace && !failed(r) && !solved(r)) + if (!failed(r) && !solved(r)) trace_curr_state(); } -scope_trace::scope_trace(bool enable): - m_old(g_trace) { - g_trace = enable; -} - -scope_trace::scope_trace(): - scope_trace(get_config().m_trace) { -} - -scope_trace::~scope_trace() { - g_trace = m_old; -} - io_state_stream const & operator<<(io_state_stream const & out, ppb const & e) { expr tmp = curr_state().to_kernel_expr(e.m_expr); out << tmp; diff --git a/src/library/blast/trace.h b/src/library/blast/trace.h index f04717ff3..f4590e620 100644 --- a/src/library/blast/trace.h +++ b/src/library/blast/trace.h @@ -4,24 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "library/trace.h" #include "library/blast/action_result.h" #include "library/io_state_stream.h" namespace lean { namespace blast { void trace_curr_state(); -void trace(char const * msg); +void trace_search(char const * msg); void trace_action(char const * a); void trace_curr_state_if(action_result r); -bool is_trace_enabled(); - -class scope_trace { - bool m_old; -public: - scope_trace(); - scope_trace(bool enable); - ~scope_trace(); -}; /** \brief Helper class for pretty printing blast expressions. It uses state::to_kernel_expr to export a blast expression diff --git a/src/library/trace.cpp b/src/library/trace.cpp index b29ec9d9b..9113f9406 100644 --- a/src/library/trace.cpp +++ b/src/library/trace.cpp @@ -58,16 +58,21 @@ bool is_trace_class_enabled(name const & n) { return false; if (is_trace_class_enabled_core(n)) return true; - if (auto s = g_trace_aliases->find(n)) { - bool found = false; - s->for_each([&](name const & alias) { - if (!found && is_trace_class_enabled_core(alias)) - found = true; - }); - if (found) - return true; + auto it = n; + while (true) { + if (auto s = g_trace_aliases->find(it)) { + bool found = false; + s->for_each([&](name const & alias) { + if (!found && is_trace_class_enabled_core(alias)) + found = true; + }); + if (found) + return true; + } + if (it.is_atomic()) + return false; + it = it.get_prefix(); } - return false; } scope_trace_env::scope_trace_env(environment const & env, io_state const & ios) { @@ -129,6 +134,16 @@ struct silent_ios_helper { MK_THREAD_LOCAL_GET_DEF(silent_ios_helper, get_silent_ios_helper); +scope_trace_silent::scope_trace_silent(bool flag) { + m_old_ios = g_ios; + if (flag) + g_ios = &get_silent_ios_helper().m_ios; +} + +scope_trace_silent::~scope_trace_silent() { + g_ios = m_old_ios; +} + io_state_stream tout() { if (g_env) { return diagnostic(*g_env, *g_ios); diff --git a/src/library/trace.h b/src/library/trace.h index bda36eacd..84289602a 100644 --- a/src/library/trace.h +++ b/src/library/trace.h @@ -36,9 +36,9 @@ public: #define LEAN_LABEL_(a) LEAN_MERGE_(unique_name_, a) #define LEAN_UNIQUE_NAME LEAN_LABEL_(__LINE__) -#define lean_trace_inc_depth(CName) \ -scope_trace_inc_depth LEAN_UNIQUE_NAME; \ -if (is_trace_enabled() && is_trace_class_enabled(name(CName))) \ +#define lean_trace_inc_depth(CName) \ +scope_trace_inc_depth LEAN_UNIQUE_NAME; \ +if (::lean::is_trace_enabled() && ::lean::is_trace_class_enabled(name(CName))) \ LEAN_UNIQUE_NAME.activate(); /* Temporarily set an option if it is not already set in the trace environment. */ @@ -56,6 +56,14 @@ if (lean_is_trace_enabled(CName)) { \ LEAN_UNIQUE_NAME.init(Opt, Val); \ } +/* Helper object for temporarily silencing trace messages */ +class scope_trace_silent { + io_state * m_old_ios{nullptr}; +public: + scope_trace_silent(bool flag); + ~scope_trace_silent(); +}; + struct tdepth {}; struct tclass { name m_cls; tclass(name const & c):m_cls(c) {} };