michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/blast): refine trace messages

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-09 18:38:20 -08:00
parent 34e85be970
commit 1f8de7b50b
4 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/blast/actions/recursor_action.cpp
View file

@ -112,7 +112,7 @@ 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";);
lean_trace_search(tout() << "backjumping split #" << *m_split_idx << "\n";);
}
return action_result::solved(it);
}
@ -134,14 +134,14 @@ 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";);
lean_trace_search(tout() << "solved 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, 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";);
lean_trace_search(tout() << "next of split #" << *m_split_idx << "\n";);
return action_result::new_branch();
}
}
@ -304,7 +304,7 @@ action_result recursor_action(hypothesis_idx hidx, name const & R) {
if (new_goals.size() > 1) {
split_idx = mk_split_idx();
}
lean_trace_action(
lean_trace_search(
tout() << "recursor ";
if (split_idx)
tout () << "(split #" << *split_idx << ") ";

7
src/library/blast/backward/backward_action.cpp
View file

@ -111,7 +111,8 @@ 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 of choice #" << m_choice_idx << ") " << lemma << "\n";);
lean_trace_search(tout() << "next of choice #" << m_choice_idx
<< ", " << m_action_name << " " << lemma << "\n";);
return r;
}
}
@ -131,9 +132,9 @@ action_result backward_action_core(list<gexpr> const & lemmas, bool prop_only_br
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";);
lean_trace_search(tout() << action_name << " (choice #" << cidx << ") " << H << "\n";);
} else {
lean_trace_action(tout() << action_name << " " << H << "\n";);
lean_trace_search(tout() << action_name << " " << H << "\n";);
}
return r;
}

1
src/library/blast/strategy.cpp
View file

@ -89,7 +89,6 @@ optional<expr> strategy_fn::search() {
lean_trace_search(tout() << "strategy '" << get_name() << "' succeeded, proof found\n";);
return some_expr(unfold_hypotheses_ge(curr_state(), r.get_proof(), init_proof_depth));
}
trace_search("* next branch");
break;
case action_result::NewBranch:
r = next_action();

2
src/library/blast/trace.cpp
View file

@ -67,7 +67,7 @@ void trace_depth_nchoices() {
p.second == get_num_choice_points())
return;
p = mk_pair(curr_state().get_proof_depth(), get_num_choice_points());
lean_trace_search(tout() << "depth: " << p.first << ", #choice: " << p.second << "\n";);
lean_trace_search(tout() << "depth: " << p.first << ", #choices: " << p.second << "\n";);
}
void trace_search(char const * msg) {