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

refactor(library/blast): ppb is not necessary anymore

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-26 15:51:46 -08:00
parent eee74ef1b4
commit 2fd5347901
12 changed files with 53 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/abstract_type_context.h
View file

@ -29,7 +29,7 @@ public:
\remark Default implementation just invokes \c infer. */ \remark Default implementation just invokes \c infer. */
virtual expr check(expr const & e) { return infer(e); } virtual expr check(expr const & e) { return infer(e); }
virtual optional<expr> is_stuck(expr const &) { return none_expr(); } virtual optional<expr> is_stuck(expr const &) { return none_expr(); }
virtual name get_local_pp_name(expr const & e) { return local_pp_name(e); } virtual name get_local_pp_name(expr const & e) const { return local_pp_name(e); }
virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) { virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) {
return mk_local(mk_fresh_name(), pp_name, type, bi); return mk_local(mk_fresh_name(), pp_name, type, bi);
} }

10
src/library/blast/blast.cpp
View file

@ -279,6 +279,16 @@ class blastenv {
virtual void commit() override { virtual void commit() override {
m_stack.pop_back(); m_stack.pop_back();
} }
virtual name get_local_pp_name(expr const & e) const override {
if (is_href(e)) {
state const & s = m_benv.m_curr_state;
hypothesis const & h = s.get_hypothesis_decl(e);
return h.get_name();
} else {
return local_pp_name(e);
}
}
}; };
class to_blast_expr_fn : public replace_visitor { class to_blast_expr_fn : public replace_visitor {

12
src/library/blast/congruence_closure.cpp
View file

@ -1136,7 +1136,7 @@ void congruence_closure::propagate_no_confusion_eq(expr const & e1, expr const &
expr pr = *get_eqv_proof(get_eq_name(), e1, e2); expr pr = *get_eqv_proof(get_eq_name(), e1, e2);
expr H = s.mk_hypothesis(type, pr); expr H = s.mk_hypothesis(type, pr);
lean_trace(name({"cc", "propagation"}), lean_trace(name({"cc", "propagation"}),
tout() << "no confusion eq: " << ppb(H) << " : " << ppb(infer_type(H)) << "\n";); tout() << "no confusion eq: " << H << " : " << infer_type(H) << "\n";);
} }
/* Remark: If added_prop is not none, then it contains the proposition provided to ::add. /* Remark: If added_prop is not none, then it contains the proposition provided to ::add.
@ -1284,7 +1284,7 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con
} }
expr H = s.mk_hypothesis(type, pr); expr H = s.mk_hypothesis(type, pr);
lean_trace(name({"cc", "propagation"}), lean_trace(name({"cc", "propagation"}),
tout() << ppb(H) << " : " << ppb(infer_type(H)) << "\n";); tout() << H << " : " << infer_type(H) << "\n";);
} }
} }
} }
@ -1297,7 +1297,7 @@ void congruence_closure::add_eqv_step(name const & R, expr e1, expr e2, expr con
if (R == get_eq_name()) { if (R == get_eq_name()) {
check_new_subsingleton_eq(e1_root, e2_root); check_new_subsingleton_eq(e1_root, e2_root);
} }
lean_trace(name({"cc", "merge"}), tout() << ppb(e1_root) << " [" << R << "] " << ppb(e2_root) << "\n";); lean_trace(name({"cc", "merge"}), tout() << e1_root << " [" << R << "] " << e2_root << "\n";);
lean_trace(name({"cc", "state"}), trace();); lean_trace(name({"cc", "state"}), trace(););
} }
@ -1913,7 +1913,7 @@ void congruence_closure::trace_eqc(name const & R, expr const & e) const {
do { do {
auto it_n = m_entries.find(eqc_key(R, it)); auto it_n = m_entries.find(eqc_key(R, it));
if (first) first = false; else out << ", "; if (first) first = false; else out << ", ";
out << ppb(it); out << it;
it = it_n->m_next; it = it_n->m_next;
} while (it != e); } while (it != e);
out << "}"; out << "}";
@ -1938,13 +1938,13 @@ void congruence_closure::trace_parents() const {
auto out = tout(); auto out = tout();
m_parents.for_each([&](child_key const & k, parent_occ_set const & ps) { m_parents.for_each([&](child_key const & k, parent_occ_set const & ps) {
trace_rel(out, k.m_R); trace_rel(out, k.m_R);
out << ppb(k.m_expr); out << k.m_expr;
out << ", parents: {"; out << ", parents: {";
bool first = true; bool first = true;
ps.for_each([&](parent_occ const & o) { ps.for_each([&](parent_occ const & o) {
if (first) first = false; else out << ", "; if (first) first = false; else out << ", ";
trace_rel(out, o.m_R); trace_rel(out, o.m_R);
out << ppb(o.m_expr); out << o.m_expr;
}); });
out << "}\n"; out << "}\n";
}); });

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

@ -399,7 +399,7 @@ void discr_tree::node::trace(optional<edge> const & e, unsigned depth, bool disj
first = true; first = true;
m_ptr->m_values.for_each([&](expr const & v) { m_ptr->m_values.for_each([&](expr const & v) {
if (first) first = false; else tout() << ", "; if (first) first = false; else tout() << ", ";
tout() << ppb(v); tout() << v;
}); });
tout() << "}"; tout() << "}";
} }

34
src/library/blast/forward/ematch.cpp
View file

@ -425,8 +425,8 @@ struct ematch_fn {
expr new_p = m_ctx->instantiate_uvars_mvars(p); expr new_p = m_ctx->instantiate_uvars_mvars(p);
expr new_p_type = m_ctx->instantiate_uvars_mvars(m_ctx->infer(p)); expr new_p_type = m_ctx->instantiate_uvars_mvars(m_ctx->infer(p));
expr t_type = m_ctx->infer(t); expr t_type = m_ctx->infer(t);
tout() << "try process_match: " << ppb(p) << " ::= " << ppb(new_p) << " : " << ppb(new_p_type) << " <=?=> " tout() << "try process_match: " << p << " ::= " << new_p << " : " << new_p_type << " <=?=> "
<< ppb(t) << " : " << ppb(t_type) << "\n";); << t << " : " << t_type << "\n";);
if (!is_app(p)) { if (!is_app(p)) {
bool success = match_leaf(R, p, t); bool success = match_leaf(R, p, t);
return success; return success;
@ -448,7 +448,7 @@ struct ematch_fn {
ok = true; ok = true;
candidates.push_back(it); candidates.push_back(it);
} }
lean_trace_debug_ematch(tout() << "candidate: " << ppb(it) << "..." << (ok ? "ok" : "skip") << "\n";); lean_trace_debug_ematch(tout() << "candidate: " << it << "..." << (ok ? "ok" : "skip") << "\n";);
it = m_cc.get_next(R, it); it = m_cc.get_next(R, it);
} while (it != t); } while (it != t);
if (candidates.empty()) { if (candidates.empty()) {
@ -459,7 +459,7 @@ struct ematch_fn {
for (expr const & c : candidates) { for (expr const & c : candidates) {
state new_state = m_state; state new_state = m_state;
if (match_args(new_state, R, p_args, c)) { if (match_args(new_state, R, p_args, c)) {
lean_trace_debug_ematch(tout() << "match: " << ppb(c) << "\n";); lean_trace_debug_ematch(tout() << "match: " << c << "\n";);
new_states.push_back(new_state); new_states.push_back(new_state);
} }
} }
@ -468,7 +468,7 @@ struct ematch_fn {
} }
bool process_continue(name const & R, expr const & p) { bool process_continue(name const & R, expr const & p) {
lean_trace_debug_ematch(tout() << "process_continue: " << ppb(p) << "\n";); lean_trace_debug_ematch(tout() << "process_continue: " << p << "\n";);
buffer<expr> p_args; buffer<expr> p_args;
expr const & f = get_app_args(p, p_args); expr const & f = get_app_args(p, p_args);
buffer<state> new_states; buffer<state> new_states;
@ -506,8 +506,8 @@ struct ematch_fn {
expr new_p = m_ctx->instantiate_uvars_mvars(p); expr new_p = m_ctx->instantiate_uvars_mvars(p);
expr new_p_type = m_ctx->instantiate_uvars_mvars(m_ctx->infer(p)); expr new_p_type = m_ctx->instantiate_uvars_mvars(m_ctx->infer(p));
expr t_type = m_ctx->infer(t); expr t_type = m_ctx->infer(t);
tout() << "process_matchss: " << ppb(p) << " ::= " << ppb(new_p) << " : " << ppb(new_p_type) << " <=?=> " tout() << "process_matchss: " << p << " ::= " << new_p << " : " << new_p_type << " <=?=> "
<< ppb(t) << " : " << ppb(t_type) << "\n";); << t << " : " << t_type << "\n";);
if (!is_metavar(p)) { if (!is_metavar(p)) {
/* If p is not a metavariable we simply ignore it. /* If p is not a metavariable we simply ignore it.
We should improve this case in the future. */ We should improve this case in the future. */
@ -539,7 +539,7 @@ struct ematch_fn {
name R; frame_kind kind; expr p, t; name R; frame_kind kind; expr p, t;
std::tie(R, kind, p, t) = head(m_state); std::tie(R, kind, p, t) = head(m_state);
m_state = tail(m_state); m_state = tail(m_state);
// diagnostic(env(), ios()) << ">> " << R << ", " << ppb(p) << " =?= " << ppb(t) << "\n"; // diagnostic(env(), ios()) << ">> " << R << ", " << p << " =?= " << t << "\n";
bool success; bool success;
switch (kind) { switch (kind) {
case DefEqOnly: case DefEqOnly:
@ -548,8 +548,8 @@ struct ematch_fn {
expr new_p = m_ctx->instantiate_uvars_mvars(p); expr new_p = m_ctx->instantiate_uvars_mvars(p);
expr new_p_type = m_ctx->instantiate_uvars_mvars(m_ctx->infer(p)); expr new_p_type = m_ctx->instantiate_uvars_mvars(m_ctx->infer(p));
expr t_type = m_ctx->infer(t); expr t_type = m_ctx->infer(t);
tout() << "must be def-eq: " << ppb(new_p) << " : " << ppb(new_p_type) tout() << "must be def-eq: " << new_p << " : " << new_p_type
<< " =?= " << ppb(t) << " : " << ppb(t_type) << " =?= " << t << " : " << t_type
<< " ... " << (success ? "succeeded" : "failed") << "\n";); << " ... " << (success ? "succeeded" : "failed") << "\n";);
return success; return success;
case Match: case Match:
@ -560,8 +560,8 @@ struct ematch_fn {
expr new_p = m_ctx->instantiate_uvars_mvars(p); expr new_p = m_ctx->instantiate_uvars_mvars(p);
expr new_p_type = m_ctx->instantiate_uvars_mvars(m_ctx->infer(p)); expr new_p_type = m_ctx->instantiate_uvars_mvars(m_ctx->infer(p));
expr t_type = m_ctx->infer(t); expr t_type = m_ctx->infer(t);
tout() << "must be eqv: " << ppb(new_p) << " : " << ppb(new_p_type) << " =?= " tout() << "must be eqv: " << new_p << " : " << new_p_type << " =?= "
<< ppb(t) << " : " << ppb(t_type) << " ... " << (success ? "succeeded" : "failed") << "\n";); << t << " : " << t_type << " ... " << (success ? "succeeded" : "failed") << "\n";);
return success; return success;
case MatchSS: case MatchSS:
return process_matchss(p, t); return process_matchss(p, t);
@ -590,16 +590,16 @@ struct ematch_fn {
for (expr const & mvar : lemma.m_mvars) { for (expr const & mvar : lemma.m_mvars) {
if (!m_ctx->get_assignment(mvar)) { if (!m_ctx->get_assignment(mvar)) {
if (!head(*it)) { if (!head(*it)) {
lean_trace_debug_ematch(tout() << "unassigned argument not inst-implicit: " << ppb(m_ctx->infer(mvar)) << "\n";); lean_trace_debug_ematch(tout() << "unassigned argument not inst-implicit: " << m_ctx->infer(mvar) << "\n";);
return; // fail, argument is not instance implicit return; // fail, argument is not instance implicit
} }
auto new_val = m_ctx->mk_class_instance(m_ctx->infer(mvar)); auto new_val = m_ctx->mk_class_instance(m_ctx->infer(mvar));
if (!new_val) { if (!new_val) {
lean_trace_debug_ematch(tout() << "cannot synthesize unassigned inst-implicit argument: " << ppb(m_ctx->infer(mvar)) << "\n";); lean_trace_debug_ematch(tout() << "cannot synthesize unassigned inst-implicit argument: " << m_ctx->infer(mvar) << "\n";);
return; // fail, instance could not be generated return; // fail, instance could not be generated
} }
if (!m_ctx->assign(mvar, *new_val)) { if (!m_ctx->assign(mvar, *new_val)) {
lean_trace_debug_ematch(tout() << "unable to assign inst-implicit argument: " << ppb(*new_val) << " : " << ppb(m_ctx->infer(mvar)) << "\n";); lean_trace_debug_ematch(tout() << "unable to assign inst-implicit argument: " << *new_val << " : " << m_ctx->infer(mvar) << "\n";);
return; // fail, type error return; // fail, type error
} }
} }
@ -613,7 +613,7 @@ struct ematch_fn {
if (!m_new_instances) { if (!m_new_instances) {
trace_action("ematch"); trace_action("ematch");
} }
lean_trace_ematch(tout() << "instance [" << ppb(lemma.m_expr) << "]: " << ppb(new_inst) << "\n";); lean_trace_ematch(tout() << "instance [" << lemma.m_expr << "]: " << new_inst << "\n";);
m_new_instances = true; m_new_instances = true;
expr new_proof = m_ctx->instantiate_uvars_mvars(lemma.m_proof); expr new_proof = m_ctx->instantiate_uvars_mvars(lemma.m_proof);
curr_state().mk_hypothesis(new_inst, new_proof); curr_state().mk_hypothesis(new_inst, new_proof);
@ -643,7 +643,7 @@ struct ematch_fn {
if (auto s = m_inst_ext.get_apps().find(head_index(f))) { if (auto s = m_inst_ext.get_apps().find(head_index(f))) {
s->for_each([&](expr const & t) { s->for_each([&](expr const & t) {
if ((m_cc.is_congr_root(R, t) || m_cc.eq_class_heterogeneous(t)) && (!filter || m_cc.get_mt(R, t) == gmt)) { if ((m_cc.is_congr_root(R, t) || m_cc.eq_class_heterogeneous(t)) && (!filter || m_cc.get_mt(R, t) == gmt)) {
lean_trace_debug_ematch(tout() << "ematch " << ppb(get_app_fn(lemma.m_proof)) << " [using] " << ppb(t) << "\n";); lean_trace_debug_ematch(tout() << "ematch " << get_app_fn(lemma.m_proof) << " [using] " << t << "\n";);
m_ctx->clear(); m_ctx->clear();
m_ctx->set_next_uvar_idx(lemma.m_num_uvars); m_ctx->set_next_uvar_idx(lemma.m_num_uvars);
m_ctx->set_next_mvar_idx(lemma.m_num_mvars); m_ctx->set_next_mvar_idx(lemma.m_num_mvars);

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

@ -37,7 +37,7 @@ std::ostream & operator<<(std::ostream & out, gexpr const & ge) {
} }
io_state_stream const & operator<<(io_state_stream const & out, gexpr const & ge) { io_state_stream const & operator<<(io_state_stream const & out, gexpr const & ge) {
out << ppb(ge.m_expr); out << ge.m_expr;
if (ge.is_universe_polymorphic()) out << " (poly)"; if (ge.is_universe_polymorphic()) out << " (poly)";
return out; return out;
} }

6
src/library/blast/recursor/recursor_strategy.cpp
View file

@ -95,7 +95,7 @@ public:
action_result r = try_hypothesis(hidx); action_result r = try_hypothesis(hidx);
if (!failed(r)) { if (!failed(r)) {
lean_trace_search(tout() << "next of choice #" << m_choice_idx lean_trace_search(tout() << "next of choice #" << m_choice_idx
<< ", recurse " << ppb(mk_href(hidx)) << "\n";); << ", recurse " << mk_href(hidx) << "\n";);
return r; return r;
} }
} }
@ -121,9 +121,9 @@ action_result rec_action(rec_candidate_selector const & selector) {
// create choice point // create choice point
unsigned cidx = mk_choice_point_idx(); unsigned cidx = mk_choice_point_idx();
push_choice_point(choice_point(new rec_choice_point_cell(s, hidx_list, cidx))); push_choice_point(choice_point(new rec_choice_point_cell(s, hidx_list, cidx)));
lean_trace_search(tout() << "recurse " << ppb(mk_href(hidx)) << " (choice #" << cidx << ")\n";); lean_trace_search(tout() << "recurse " << mk_href(hidx) << " (choice #" << cidx << ")\n";);
} else { } else {
lean_trace_search(tout() << "recurse " << ppb(mk_href(hidx)) << "\n";); lean_trace_search(tout() << "recurse " << mk_href(hidx) << "\n";);
} }
return r; return r;
} }

16
src/library/blast/simplifier/simplifier.cpp
View file

@ -384,7 +384,7 @@ result simplifier::simplify(expr const & e, bool is_root) {
check_system("simplifier"); check_system("simplifier");
m_num_steps++; m_num_steps++;
lean_trace_inc_depth("simplifier"); lean_trace_inc_depth("simplifier");
lean_trace_d("simplifier", tout() << m_rel << ": " << ppb(e) << "\n";); lean_trace_d("simplifier", tout() << m_rel << ": " << e << "\n";);
if (m_num_steps > m_max_steps) if (m_num_steps > m_max_steps)
throw blast_exception("simplifier failed, maximum number of steps exceeded", e); throw blast_exception("simplifier failed, maximum number of steps exceeded", e);
@ -627,7 +627,7 @@ result simplifier::rewrite(expr const & e, simp_lemma const & sr) {
expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs()); expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs());
expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs()); expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
tout() << "(" << sr.get_id() << ") " tout() << "(" << sr.get_id() << ") "
<< "[" << ppb(new_lhs) << " --> " << ppb(new_rhs) << "]\n";); << "[" << new_lhs << " --> " << new_rhs << "]\n";);
if (!instantiate_emetas(tmp_tctx, sr.get_num_emeta(), sr.get_emetas(), sr.get_instances())) return result(e); if (!instantiate_emetas(tmp_tctx, sr.get_num_emeta(), sr.get_emetas(), sr.get_instances())) return result(e);
@ -720,7 +720,7 @@ result simplifier::try_congr(expr const & e, user_congr_lemma const & cr) {
expr new_rhs = tmp_tctx->instantiate_uvars_mvars(cr.get_rhs()); expr new_rhs = tmp_tctx->instantiate_uvars_mvars(cr.get_rhs());
diagnostic(env(), ios(), get_type_context()) diagnostic(env(), ios(), get_type_context())
<< "(" << cr.get_id() << ") " << "(" << cr.get_id() << ") "
<< "[" << ppb(new_lhs) << " =?= " << ppb(new_rhs) << "]\n";); << "[" << new_lhs << " =?= " << new_rhs << "]\n";);
/* First, iterate over the congruence hypotheses */ /* First, iterate over the congruence hypotheses */
bool failed = false; bool failed = false;
@ -787,13 +787,13 @@ bool simplifier::instantiate_emetas(blast_tmp_type_context & tmp_tctx, unsigned
if (auto v = tmp_tctx->mk_class_instance(m_type)) { if (auto v = tmp_tctx->mk_class_instance(m_type)) {
if (!tmp_tctx->assign(m, *v)) { if (!tmp_tctx->assign(m, *v)) {
lean_trace(name({"simplifier", "failure"}), lean_trace(name({"simplifier", "failure"}),
tout() << "unable to assign instance for: " << ppb(m_type) << "\n";); tout() << "unable to assign instance for: " << m_type << "\n";);
failed = true; failed = true;
return; return;
} }
} else { } else {
lean_trace(name({"simplifier", "failure"}), lean_trace(name({"simplifier", "failure"}),
tout() << "unable to synthesize instance for: " << ppb(m_type) << "\n";); tout() << "unable to synthesize instance for: " << m_type << "\n";);
failed = true; failed = true;
return; return;
} }
@ -809,7 +809,7 @@ bool simplifier::instantiate_emetas(blast_tmp_type_context & tmp_tctx, unsigned
} }
lean_trace(name({"simplifier", "failure"}), lean_trace(name({"simplifier", "failure"}),
tout() << "failed to assign: " << m << " : " << ppb(m_type) << "\n";); tout() << "failed to assign: " << m << " : " << m_type << "\n";);
failed = true; failed = true;
return; return;
@ -1081,7 +1081,7 @@ result simplifier::fuse(expr const & e) {
get_simp_lemmas(g_ac_key)); get_simp_lemmas(g_ac_key));
if (!pf_1_3) { if (!pf_1_3) {
diagnostic(env(), ios(), get_type_context()) << ppb(e) << "\n\n =?=\n\n" << ppb(e_grp) << "\n"; diagnostic(env(), ios(), get_type_context()) << e << "\n\n =?=\n\n" << e_grp << "\n";
throw blast_exception("Failed to prove (1) == (3) during fusion", e); throw blast_exception("Failed to prove (1) == (3) during fusion", e);
} }
@ -1090,7 +1090,7 @@ result simplifier::fuse(expr const & e) {
get_simp_lemmas(g_som_key)); get_simp_lemmas(g_som_key));
if (!pf_4_5) { if (!pf_4_5) {
diagnostic(env(), ios(), get_type_context()) << ppb(e_grp_ls) << "\n\n =?=\n\n" << ppb(e_fused_ls) << "\n"; diagnostic(env(), ios(), get_type_context()) << e_grp_ls << "\n\n =?=\n\n" << e_fused_ls << "\n";
throw blast_exception("Failed to prove (4) == (5) during fusion", e); throw blast_exception("Failed to prove (4) == (5) during fusion", e);
} }

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

@ -886,7 +886,7 @@ optional<unsigned> state::select_hypothesis_to_activate() {
void state::activate_hypothesis(hypothesis_idx hidx) { void state::activate_hypothesis(hypothesis_idx hidx) {
lean_trace_search( lean_trace_search(
hypothesis const & h = get_hypothesis_decl(hidx); hypothesis const & h = get_hypothesis_decl(hidx);
tout() << "activate " << h.get_name() << " : " << ppb(h.get_type()) << "\n";); tout() << "activate " << h.get_name() << " : " << h.get_type() << "\n";);
lean_assert(!get_hypothesis_decl(hidx).is_dead()); lean_assert(!get_hypothesis_decl(hidx).is_dead());
m_branch.m_active.insert(hidx); m_branch.m_active.insert(hidx);
update_indices(hidx); update_indices(hidx);

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

@ -19,7 +19,7 @@ MK_THREAD_LOCAL_GET_DEF(expr, get_last_target);
void trace_target() { void trace_target() {
if (lean_is_trace_enabled(name({"blast", "search"})) && if (lean_is_trace_enabled(name({"blast", "search"})) &&
curr_state().get_target() != get_last_target()) { curr_state().get_target() != get_last_target()) {
lean_trace_search(tout() << "target " << ppb(curr_state().get_target()) << "\n";); lean_trace_search(tout() << "target " << curr_state().get_target() << "\n";);
get_last_target() = curr_state().get_target(); get_last_target() = curr_state().get_target();
} }
} }
@ -83,14 +83,8 @@ void trace_curr_state_if(action_result r) {
trace_curr_state(); trace_curr_state();
} }
io_state_stream const & operator<<(io_state_stream const & out, ppb const & e) {
expr tmp = curr_state().to_kernel_expr(e.m_expr);
out << tmp;
return out;
}
io_state_stream const & operator<<(io_state_stream const & out, hypothesis const & h) { io_state_stream const & operator<<(io_state_stream const & out, hypothesis const & h) {
out << ppb(h.get_self()); out << h.get_self();
return out; return out;
} }
}} }}

9
src/library/blast/trace.h
View file

@ -24,14 +24,5 @@ void trace_curr_state_if(action_result r);
#define lean_trace_search(Code) lean_trace(name({"blast", "search"}), Code) #define lean_trace_search(Code) lean_trace(name({"blast", "search"}), Code)
#define lean_trace_deadend(Code) lean_trace(name({"blast", "deadend"}), 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
into an expression that can be processed by the pretty printer */
struct ppb {
expr m_expr;
explicit ppb(expr const & e):m_expr(e) {}
};
io_state_stream const & operator<<(io_state_stream const & out, ppb const & e);
io_state_stream const & operator<<(io_state_stream const & out, hypothesis const & h); io_state_stream const & operator<<(io_state_stream const & out, hypothesis const & h);
}} }}

6
src/library/blast/unit/unit_propagate.cpp
View file

@ -294,7 +294,7 @@ static action_result unit_lemma(hypothesis_idx hidx, expr const & _type, expr co
} }
curr_state().mk_hypothesis(final_type, final_proof); curr_state().mk_hypothesis(final_type, final_proof);
lean_trace_unit_propagate(tout() << ppb(final_type) << "\n";); lean_trace_unit_propagate(tout() << final_type << "\n";);
return action_result::new_branch(); return action_result::new_branch();
} }
@ -316,7 +316,7 @@ static action_result unit_dep_lemma(hypothesis_idx hidx, expr type, expr proof)
if (propagated) { if (propagated) {
curr_state().del_hypothesis(hidx); curr_state().del_hypothesis(hidx);
curr_state().mk_hypothesis(type, proof); curr_state().mk_hypothesis(type, proof);
lean_trace_unit_propagate(tout() << ppb(type) << "\n";); lean_trace_unit_propagate(tout() << type << "\n";);
return action_result::new_branch(); return action_result::new_branch();
} }
lean_assert(is_pi(type)); lean_assert(is_pi(type));
@ -351,7 +351,7 @@ static action_result unit_fact(expr const & type) {
action_result unit_propagate(unsigned hidx) { action_result unit_propagate(unsigned hidx) {
hypothesis const & h = curr_state().get_hypothesis_decl(hidx); hypothesis const & h = curr_state().get_hypothesis_decl(hidx);
expr type = whnf(h.get_type()); expr type = whnf(h.get_type());
lean_trace_debug_unit_propagate(tout() << ppb(type) << "\n";); lean_trace_debug_unit_propagate(tout() << type << "\n";);
if (is_lemma(type)) return unit_lemma(hidx, type, h.get_self()); if (is_lemma(type)) return unit_lemma(hidx, type, h.get_self());
else if (is_dep_lemma(type)) return unit_dep_lemma(hidx, type, h.get_self()); else if (is_dep_lemma(type)) return unit_dep_lemma(hidx, type, h.get_self());
else if (is_fact(type)) return unit_fact(type); else if (is_fact(type)) return unit_fact(type);