feat(library/blast): add 'blast.deadend' tracing option

src/library/blast/actions/recursor_action.cpp

@@ -77,9 +77,12 @@ struct recursor_proof_step_cell : public proof_step_cell {
     expr       m_proof;       // recursor-application (the position where the goal-proofs are marked by the local constants).
     list<expr> m_goals;       // type of each subgoal/branch encoded as a local constant
     list<expr> m_goal_proofs; // proofs generated so far
+    optional<unsigned> m_split_idx;
 
-    recursor_proof_step_cell(bool dep, branch const & b, expr const & pr, list<expr> const & goals, list<expr> const & goal_proofs):
+    recursor_proof_step_cell(bool dep, branch const & b, expr const & pr, list<expr> const & goals, list<expr> const & goal_proofs,
-        m_dep(dep), m_branch(b), m_proof(pr), m_goals(goals), m_goal_proofs(goal_proofs) {
+                             optional<unsigned> const & split_idx):
+        m_dep(dep), m_branch(b), m_proof(pr), m_goals(goals), m_goal_proofs(goal_proofs),
+        m_split_idx(split_idx) {
     }
 
     virtual ~recursor_proof_step_cell() {}
@@ -108,6 +111,9 @@ struct recursor_proof_step_cell : public proof_step_cell {
             }
             if (skip) {
                 lean_assert(closed(it));
+                if (m_split_idx) {
+                    lean_trace_action(tout() << "backjumping recursor (split #" << *m_split_idx << ")\n";);
+                }
                 return action_result::solved(it);
             }
         }
@@ -127,11 +133,15 @@ struct recursor_proof_step_cell : public proof_step_cell {
                 }
             }
             expr result = mk_app(rec, proof_args);
+            if (m_split_idx)
+                lean_trace_action(tout() << "solved recursor (split #" << *m_split_idx << ")\n";);
             return action_result::solved(result);
         } else {
             s.pop_proof_step();
-            s.push_proof_step(new recursor_proof_step_cell(m_dep, m_branch, m_proof, new_goals, new_prs));
+            s.push_proof_step(new recursor_proof_step_cell(m_dep, m_branch, m_proof, new_goals, new_prs, m_split_idx));
             s.set_target(mlocal_type(head(new_goals)));
+            lean_assert(m_split_idx);
+            lean_trace_action(tout() << "recursor (next of split #" << *m_split_idx << ")\n";);
             return action_result::new_branch();
         }
     }
@@ -290,12 +300,20 @@ action_result recursor_action(hypothesis_idx hidx, name const & R) {
         return action_result::failed(); // ill-formed recursor
 
     save_state.commit();
-    lean_trace_action(tout() << "recursor " << R << "\n";);
+    optional<unsigned> split_idx;
+    if (new_goals.size() > 1) {
+        split_idx = mk_split_idx();
+    }
+    lean_trace_action(
+        tout() << "recursor ";
+        if (split_idx)
+            tout () << "(split #" << *split_idx << ") ";
+        tout() << R << " " << h << "\n";);
     if (new_goals.empty()) {
         return action_result::solved(rec);
     }
     s.del_hypothesis(hidx);
-    s.push_proof_step(new recursor_proof_step_cell(rec_info.has_dep_elim(), s.get_branch(), rec, to_list(new_goals), list<expr>()));
+    s.push_proof_step(new recursor_proof_step_cell(rec_info.has_dep_elim(), s.get_branch(), rec, to_list(new_goals), list<expr>(), split_idx));
     s.set_target(mlocal_type(new_goals[0]));
     return action_result::new_branch();
 }

src/library/blast/backward/backward_action.cpp

@@ -98,9 +98,11 @@ class backward_choice_point_cell : public choice_point_cell {
     state        m_state;
     list<gexpr>  m_lemmas;
     bool         m_prop_only;
+    unsigned     m_choice_idx;
 public:
-    backward_choice_point_cell(char const * a, state const & s, list<gexpr> const & lemmas, bool prop_only):
+    backward_choice_point_cell(char const * a, state const & s, list<gexpr> const & lemmas, bool prop_only,
-        m_action_name(a), m_state(s), m_lemmas(lemmas), m_prop_only(prop_only) {}
+                               unsigned choice_idx):
+        m_action_name(a), m_state(s), m_lemmas(lemmas), m_prop_only(prop_only), m_choice_idx(choice_idx) {}
 
     virtual action_result next() {
         while (!empty(m_lemmas)) {
@@ -109,7 +111,7 @@ public:
             m_lemmas        = tail(m_lemmas);
             action_result r = try_lemma(lemma, m_prop_only);
             if (!failed(r)) {
-                lean_trace_action(tout() << m_action_name << " (next) " << lemma << "\n";);
+                lean_trace_action(tout() << m_action_name << " (next of choice #" << m_choice_idx << ") " << lemma << "\n";);
                 return r;
             }
         }
@@ -126,9 +128,13 @@ action_result backward_action_core(list<gexpr> const & lemmas, bool prop_only_br
         it              = tail(it);
         if (!failed(r)) {
             // create choice point
-            if (!cut && !empty(it))
+            if (!cut && !empty(it)) {
-                push_choice_point(choice_point(new backward_choice_point_cell(action_name, s, it, prop_only_branches)));
+                unsigned cidx = mk_choice_point_idx();
+                push_choice_point(choice_point(new backward_choice_point_cell(action_name, s, it, prop_only_branches, cidx)));
+                lean_trace_action(tout() << action_name << " (choice #" << cidx << ") " << H << "\n";);
+            } else {
                 lean_trace_action(tout() << action_name << " " << H << "\n";);
+            }
             return r;
         }
         curr_state() = s;

src/library/blast/blast.cpp

@@ -79,6 +79,8 @@ class blastenv {
     unsigned                   m_next_uref_idx{0};
     unsigned                   m_next_mref_idx{0};
     unsigned                   m_next_href_idx{0};
+    unsigned                   m_next_choice_idx{0};
+    unsigned                   m_next_split_idx{0};
     tmp_local_generator        m_tmp_local_generator;
     list<expr>                 m_initial_context; // for setting type_context local instances
     name_set                   m_lemma_hints;
@@ -739,6 +741,18 @@ public:
         m_next_href_idx++;
         return r;
     }
+
+    unsigned mk_choice_point_idx() {
+        unsigned r = m_next_choice_idx;
+        m_next_choice_idx++;
+        return r;
+    }
+
+    unsigned mk_split_idx() {
+        unsigned r = m_next_split_idx;
+        m_next_split_idx++;
+        return r;
+    }
 };
 
 LEAN_THREAD_PTR(blastenv, g_blastenv);
@@ -995,6 +1009,16 @@ bool classical() {
     return g_blastenv->classical();
 }
 
+unsigned mk_choice_point_idx() {
+    lean_assert(g_blastenv);
+    return g_blastenv->mk_choice_point_idx();
+}
+
+unsigned mk_split_idx() {
+    lean_assert(g_blastenv);
+    return g_blastenv->mk_split_idx();
+}
+
 void display_curr_state() {
     curr_state().display(env(), ios());
     display("\n");
@@ -1153,6 +1177,7 @@ void initialize_blast() {
     register_trace_class(name{"blast", "state"});
     register_trace_class(name{"blast", "action"});
     register_trace_class(name{"blast", "search"});
+    register_trace_class(name{"blast", "deadend"});
 
     register_trace_class_alias("app_builder", name({"blast", "event"}));
     register_trace_class_alias(name({"simplifier", "failure"}), name({"blast", "event"}));

src/library/blast/blast.h

@@ -167,6 +167,13 @@ unsigned register_imp_extension(ext_state_maker & state_maker);
     the current blast state. */
 imp_extension_state & get_imp_extension_state(unsigned state_id);
 
+/** \brief Helper procedure for creating unique choice point ids.
+    This is only used for tracing. */
+unsigned mk_choice_point_idx();
+/** \brief Helper procedure for creating unique case-split point ids.
+    This is only used for tracing. */
+unsigned mk_split_idx();
+
 /** \brief Display the current state of the blast tactic in the diagnostic channel. */
 void display_curr_state();
 /** \brief Display the given expression in the diagnostic channel. */

src/library/blast/strategy.cpp

@@ -72,6 +72,7 @@ optional<expr> strategy_fn::search() {
         }
         switch (r.get_kind()) {
         case action_result::Failed:
+            lean_trace_deadend(tout() << "strategy '" << get_name() << "'\n"; curr_state().display(tout()););
             r = next_choice_point(m_init_num_choices);
             if (failed(r)) {
                 // all choice points failed...
@@ -80,7 +81,6 @@ optional<expr> strategy_fn::search() {
                     display_curr_state();
                 return none_expr();
             }
-            trace_search("* next choice point");
             break;
         case action_result::Solved:
             r = next_branch(r.get_proof());

src/library/blast/trace.h

@@ -20,6 +20,7 @@ void trace_curr_state_if(action_result r);
 
 #define lean_trace_action(Code) lean_trace(name({"blast", "action"}), Code)
 #define lean_trace_search(Code) lean_trace(name({"blast", "search"}), Code)
+#define lean_trace_deadend(Code) lean_trace(name({"blast", "deadend"}), Code)
 
 /** \brief Helper class for pretty printing blast expressions.
     It uses state::to_kernel_expr to export a blast expression