max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/tactic/simplify): better debug.simplify.try_rewrite tracing

Browse source
This commit is contained in:
Daniel Selsam 2016-11-22 09:27:00 -08:00 • committed by Leonardo de Moura
parent a76c2d37a7
commit 7bfe0aedb0
1 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/tactic/simplify.cpp
View file

@ -478,7 +478,6 @@ simp_result simplify_core_fn::rewrite(expr const & e) {
list<simp_lemma> const * srs = sr->find(e);
if (!srs) {
lean_trace_d(name({"debug", "simplify", "try_rewrite"}), tout() << "no simp lemmas for: " << e << "\n";);
return simp_result(e);
}
@ -497,7 +496,11 @@ simp_result simplify_core_fn::rewrite(expr const & e) {
simp_result simplify_core_fn::rewrite(expr const & e, simp_lemma const & sl) {
tmp_type_context tmp_ctx(m_ctx, sl.get_num_umeta(), sl.get_num_emeta());
if (!tmp_ctx.is_def_eq(e, sl.get_lhs())) {
lean_trace_d(name({"debug", "simplify", "try_rewrite"}), tout() << "fail to unify: " << sl.get_id() << "\n";);
lean_trace_d(name({"debug", "simplify", "try_rewrite"}),
tout() << "fail to unify '" << sl.get_id()
<< "':\n------------------------------------------------\n"
<< e << "\n=?=\n" << sl.get_lhs()
<< "\n------------------------------------------------\n";);
return simp_result(e);
}
@ -508,8 +511,11 @@ simp_result simplify_core_fn::rewrite(expr const & e, simp_lemma const & sl) {
}
for (unsigned i = 0; i < sl.get_num_umeta(); i++) {
if (!tmp_ctx.is_uassigned(i))
if (!tmp_ctx.is_uassigned(i)) {
lean_trace_d(name({"debug", "simplify", "try_rewrite"}), tout() << "fail to instantiate umetas: " <<
sl.get_id() << "\n";);
return simp_result(e);
}
}
expr new_lhs = tmp_ctx.instantiate_mvars(sl.get_lhs());