feat(library/blast): do not display inactive hypotheses when displaying failure states

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) {

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);
 

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<expr> hidx2local;
     metavar_idx_map<expr>    midx2meta;
     hypothesis_idx_buffer hidxs;
     get_sorted_hypotheses(hidxs);
     buffer<expr> 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) {

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;

src/library/blast/strategy.cpp

@@ -79,7 +79,8 @@ optional<expr> 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();
             }