From 34e85be970eb11228ab5c6e13996063cfa75f4f4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 9 Dec 2015 17:45:36 -0800 Subject: [PATCH] feat(library/blast): add 'blast.deadend' tracing option --- src/library/blast/actions/recursor_action.cpp | 28 +++++++++++++++---- .../blast/backward/backward_action.cpp | 18 ++++++++---- src/library/blast/blast.cpp | 25 +++++++++++++++++ src/library/blast/blast.h | 7 +++++ src/library/blast/strategy.cpp | 2 +- src/library/blast/trace.h | 1 + 6 files changed, 69 insertions(+), 12 deletions(-) diff --git a/src/library/blast/actions/recursor_action.cpp b/src/library/blast/actions/recursor_action.cpp index 309611d67..d47b3fcd4 100644 --- a/src/library/blast/actions/recursor_action.cpp +++ b/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 m_goals; // type of each subgoal/branch encoded as a local constant list m_goal_proofs; // proofs generated so far + optional m_split_idx; - recursor_proof_step_cell(bool dep, branch const & b, expr const & pr, list const & goals, list const & goal_proofs): - m_dep(dep), m_branch(b), m_proof(pr), m_goals(goals), m_goal_proofs(goal_proofs) { + recursor_proof_step_cell(bool dep, branch const & b, expr const & pr, list const & goals, list const & goal_proofs, + optional 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 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())); + s.push_proof_step(new recursor_proof_step_cell(rec_info.has_dep_elim(), s.get_branch(), rec, to_list(new_goals), list(), split_idx)); s.set_target(mlocal_type(new_goals[0])); return action_result::new_branch(); } diff --git a/src/library/blast/backward/backward_action.cpp b/src/library/blast/backward/backward_action.cpp index 578a33e6a..73bdfc834 100644 --- a/src/library/blast/backward/backward_action.cpp +++ b/src/library/blast/backward/backward_action.cpp @@ -98,9 +98,11 @@ class backward_choice_point_cell : public choice_point_cell { state m_state; list m_lemmas; bool m_prop_only; + unsigned m_choice_idx; public: - backward_choice_point_cell(char const * a, state const & s, list const & lemmas, bool prop_only): - m_action_name(a), m_state(s), m_lemmas(lemmas), m_prop_only(prop_only) {} + backward_choice_point_cell(char const * a, state const & s, list const & lemmas, bool 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 const & lemmas, bool prop_only_br it = tail(it); if (!failed(r)) { // create choice point - if (!cut && !empty(it)) - push_choice_point(choice_point(new backward_choice_point_cell(action_name, s, it, prop_only_branches))); - lean_trace_action(tout() << action_name << " " << H << "\n";); + if (!cut && !empty(it)) { + 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; diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index b94266df0..ac1909213 100644 --- a/src/library/blast/blast.cpp +++ b/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 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"})); diff --git a/src/library/blast/blast.h b/src/library/blast/blast.h index 12385fe29..9a9518139 100644 --- a/src/library/blast/blast.h +++ b/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. */ diff --git a/src/library/blast/strategy.cpp b/src/library/blast/strategy.cpp index 3a27cd0d2..005252b79 100644 --- a/src/library/blast/strategy.cpp +++ b/src/library/blast/strategy.cpp @@ -72,6 +72,7 @@ optional 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 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()); diff --git a/src/library/blast/trace.h b/src/library/blast/trace.h index 4e65bcf25..d3099fb07 100644 --- a/src/library/blast/trace.h +++ b/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