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

chore(library/compiler): add trace.compiler.simp_float_cases option

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-05 13:13:18 -07:00
parent fb5fb03f00
commit 99e90f0410
2 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/compiler/compiler.cpp
View file

@ -273,6 +273,7 @@ void initialize_compiler() {
register_trace_class({"compiler", "cce"});
register_trace_class({"compiler", "simp"});
register_trace_class({"compiler", "simp_detail"});
register_trace_class({"compiler", "simp_float_cases"});
register_trace_class({"compiler", "elim_dead_let"});
register_trace_class({"compiler", "cse"});
register_trace_class({"compiler", "specialize"});

4
src/library/compiler/csimp.cpp
View file

@ -456,7 +456,7 @@ class csimp_fn {
}
}
}
lean_trace(name({"compiler", "simp"}),
lean_trace(name({"compiler", "simp_float_cases"}),
tout() << "mk_join " << fvar << "\n" << c << "\n---\n"
<< e << "\n======>\n" << mk_app(fn, args) << "\n";);
return mk_app(fn, args);
@ -653,7 +653,7 @@ class csimp_fn {
new_minor = mk_minor_lambda(zs, new_minor);
c_args[minor_idx] = new_minor;
}
lean_trace(name({"compiler", "simp"}),
lean_trace(name({"compiler", "simp_float_cases"}),
tout() << "float_cases_on [" << get_lcnf_size(env(), e) << "]\n" << c << "\n----\n" << e << "\n=====>\n"
<< mk_app(c_fn, c_args) << "\n";);
return mk_app(c_fn, c_args);