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

feat(library/defeq_canonizer): add trace.defeq_canonizer

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-08 19:05:13 -08:00
parent 347981097a
commit 7ff91ec1ef
1 changed files with 18 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/library/defeq_canonizer.cpp
View file

@ -6,14 +6,12 @@ Author: Leonardo de Moura
*/
#include "util/list_fn.h"
#include "kernel/instantiate.h"
#include "library/trace.h"
#include "library/locals.h"
#include "library/type_context.h"
#include "library/defeq_canonizer.h"
namespace lean {
void initialize_defeq_canonizer() {}
void finalize_defeq_canonizer() {}
defeq_canonizer::defeq_canonizer(type_context & ctx, state & s):
m_ctx(ctx), m_state(s) {
}
@ -101,13 +99,28 @@ expr defeq_canonizer::canonize_core(expr const & e) {
}
}
static void trace(type_context & ctx, expr const & e, expr const & r) {
lean_trace("defeq_canonizer", scope_trace_env _(ctx.env(), ctx); tout() << "\n" << e << "\n==>\n" << r << "\n";);
}
expr defeq_canonizer::canonize(expr const & e, bool & updated) {
m_updated = &updated;
return canonize_core(e);
expr r = canonize_core(e);
trace(m_ctx, e, r);
return r;
}
expr defeq_canonizer::canonize(expr const & e) {
m_updated = nullptr;
return canonize_core(e);
expr r = canonize_core(e);
trace(m_ctx, e, r);
return r;
}
void initialize_defeq_canonizer() {
register_trace_class("defeq_canonizer");
}
void finalize_defeq_canonizer() {
}
}