From 23836f53bbfdfd0d72fadf6f7378f3dfc28aa22b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 30 Dec 2015 12:08:33 -0800 Subject: [PATCH] feat(library/blast): do not display inactive hypotheses when displaying failure states --- src/library/blast/blast.cpp | 4 ++-- src/library/blast/blast.h | 2 +- src/library/blast/state.cpp | 17 ++++++++++------- src/library/blast/state.h | 6 +++--- src/library/blast/strategy.cpp | 3 ++- 5 files changed, 18 insertions(+), 14 deletions(-) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index fee04d6348..ecec827b1f 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -1058,9 +1058,9 @@ void display_at_buffer(sstream const & msg) { g_blastenv->get_buffer_ios().get_diagnostic_channel() << msg.str(); } -void display_curr_state_at_buffer() { +void display_curr_state_at_buffer(bool include_inactive) { lean_assert(g_blastenv); - curr_state().display(g_blastenv->get_env(), g_blastenv->get_buffer_ios()); + curr_state().display(g_blastenv->get_env(), g_blastenv->get_buffer_ios(), include_inactive); } scope_assignment::scope_assignment():m_keep(false) { diff --git a/src/library/blast/blast.h b/src/library/blast/blast.h index 5852a8bc54..4ea0e0a953 100644 --- a/src/library/blast/blast.h +++ b/src/library/blast/blast.h @@ -183,7 +183,7 @@ void display(char const * msg); void display(sstream const & msg); /** \brief Display curr state at buffered diagnostic channel used to craft an exception for user */ -void display_curr_state_at_buffer(); +void display_curr_state_at_buffer(bool include_inactive = true); /** \brief Display msng at buffered diagnostic channel used to craft an exception for user */ void display_at_buffer(sstream const & msg); diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 59384ea3a1..1abd77c1ef 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -256,13 +256,16 @@ expr state::to_kernel_expr(expr const & e) const { return to_kernel_expr(e, hidx2local, midx2meta); } -goal state::to_goal() const { +goal state::to_goal(bool include_inactive) const { hypothesis_idx_map hidx2local; metavar_idx_map midx2meta; hypothesis_idx_buffer hidxs; get_sorted_hypotheses(hidxs); buffer hyps; for (unsigned hidx : hidxs) { + if (!include_inactive && !is_active(hidx)) { + break; // inactive hypotheses occur after active ones after sorting + } hypothesis const & h = get_hypothesis_decl(hidx); // after we add support for let-decls in goals, we must convert back h->get_value() if it is available expr new_h = lean::mk_local(name(name("H"), hidx), @@ -289,14 +292,14 @@ void state::display_active(std::ostream & 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"; +void state::display(io_state_stream const & ios, bool include_inactive) const { + ios << mk_pair(to_goal(include_inactive).pp(ios.get_formatter()), ios.get_options()) << "\n"; } -void state::display(environment const & env, io_state const & ios) const { +void state::display(environment const & env, io_state const & ios, bool include_inactive) 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"; + out << mk_pair(to_goal(include_inactive).pp(fmt), ios.get_options()) << "\n"; } bool state::has_assigned_uref(level const & l) const { @@ -517,8 +520,8 @@ struct hypothesis_dep_depth_lt { bool operator()(unsigned hidx1, unsigned hidx2) const { hypothesis const & h1 = m_state.get_hypothesis_decl(hidx1); hypothesis const & h2 = m_state.get_hypothesis_decl(hidx2); - bool act1 = m_state.is_active(hidx1); - bool act2 = m_state.is_active(hidx2); + bool act1 = true; // m_state.is_active(hidx1); + bool act2 = true; // m_state.is_active(hidx2); if (act1 != act2) { return act1 && !act2; // active hypotheses should occur before non-active ones } else if (act1) { diff --git a/src/library/blast/state.h b/src/library/blast/state.h index bbc93ee00f..44635ff4e4 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -458,14 +458,14 @@ public: /** \brief Convert current branch into a goal. This is mainly used for pretty printing. However, in the future, we may use this capability to invoke the tactic framework from the blast tactic. */ - goal to_goal() const; + goal to_goal(bool include_inactive = true) const; /** \brief Convert expression into a kernel expression that can be pretty printed using better names, 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; + void display(io_state_stream const & ios, bool include_inactive = true) const; + void display(environment const & env, io_state const & ios, bool include_inactive = true) const; #ifdef LEAN_DEBUG bool check_invariant() const; diff --git a/src/library/blast/strategy.cpp b/src/library/blast/strategy.cpp index 93eb2b81e0..084aaa9c3a 100644 --- a/src/library/blast/strategy.cpp +++ b/src/library/blast/strategy.cpp @@ -79,7 +79,8 @@ optional strategy_fn::search() { lean_trace_search(tout() << "strategy '" << get_name() << "' failed, no proof found\n";); if (show_failure()) { display_at_buffer(sstream() << "strategy '" << get_name() << "' failed, no proof found, final state:\n"); - display_curr_state_at_buffer(); + bool include_inactive = false; + display_curr_state_at_buffer(include_inactive); } return none_expr(); }