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

feat: trace.compiler.inline

Browse source
This commit is contained in:
Sebastian Ullrich 2021-06-16 22:14:49 +02:00
parent 227a67cf8b
commit 2ca4d2693f
2 changed files with 2 additions and 0 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_bool_option(*g_extract_closed, true, "(compiler) enable/disable closed term caching");
register_trace_class("compiler");
register_trace_class({"compiler", "input"});
register_trace_class({"compiler", "inline"});
register_trace_class({"compiler", "eta_expand"});
register_trace_class({"compiler", "lcnf"});
register_trace_class({"compiler", "cce"});

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

@ -1730,6 +1730,7 @@ class csimp_fn {
}
if (!inline_if_reduce_attr && is_recursive(const_name(fn))) return none_expr();
if (uses_unsafe_inductive(c)) return none_expr();
lean_trace(name({"compiler", "inline"}), tout() << const_name(fn) << "\n";);
expr new_fn = instantiate_value_lparams(*info, const_levels(fn));
if (inline_if_reduce_attr && !inline_attr) {
return beta_reduce_if_not_cases(new_fn, e, is_let_val);