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

chore(library/compiler): remove [inline2] attribute

Browse source 
We may add it back in the future if we find compelling applications for
it. Right now, we don't have any.
This commit is contained in:
Leonardo de Moura 2019-04-18 13:23:50 -07:00
parent 2eed00039a
commit 35d54c17bd
3 changed files with 2 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1555,13 +1555,8 @@ class csimp_fn {
optional<constant_info> info = env().find(c);
if (!info || !info->is_definition()) return none_expr();
unsigned arity = get_num_nested_lambdas(info->get_value());
if (get_app_num_args(e) < arity) return none_expr();
bool inline2_attr = has_inline2_attribute(env(), const_name(fn));
if (!inline2_attr &&
(get_lcnf_size(env(), info->get_value()) > m_cfg.m_inline_threshold ||
is_constant(e))) { /* We only inline constants if they are marked with `[inline2]` attribute */
return none_expr();
}
if (get_app_num_args(e) < arity || arity == 0) return none_expr();
if (get_lcnf_size(env(), info->get_value()) > m_cfg.m_inline_threshold) return none_expr();
if (is_recursive(c)) return none_expr();
if (uses_unsafe_inductive(c)) return none_expr();
return some_expr(beta_reduce(info->get_value(), e, is_let_val));

21
src/library/compiler/util.cpp
View file

@ -101,19 +101,6 @@ bool has_inline_attribute(environment const & env, name const & n) {
return false;
}
bool has_inline2_attribute(environment const & env, name const & n) {
if (is_lambda_lifting_name(n) || is_elambda_lifting_name(n))
return false; // don't undo lambda lifting
if (has_attribute(env, "inline2", n))
return true;
if (is_internal_name(n) && !n.is_atomic()) {
/* Auxiliary declarations such as `f._main` are considered to be marked as `@[inline2]`
if `f` is marked. */
return has_inline2_attribute(env, n.get_prefix());
}
return false;
}
bool has_inline_if_reduce_attribute(environment const & env, name const & n) {
if (is_elambda_lifting_name(n))
return false; // don't undo lambda lifting
@ -673,14 +660,6 @@ void initialize_compiler_util() {
throw exception("invalid 'inline' use, only definitions can be marked as [inline]");
}));
register_system_attribute(basic_attribute::with_check(
"inline2", "mark definition to always be inlined at stage 2",
[](environment const & env, name const & d, bool) -> void {
auto decl = env.get(d);
if (!decl.is_definition())
throw exception("invalid 'inline2' use, only definitions can be marked as [inline2]");
}));
register_system_attribute(basic_attribute::with_check(
"inlineIfReduce", "mark definition to be inlined when resultant term after reduction is not a `cases_on` application.",
[](environment const & env, name const & d, bool) -> void {

1
src/library/compiler/util.h
View file

@ -33,7 +33,6 @@ bool is_lcnf_atom(expr const & e);
expr elim_trivial_let_decls(expr const & e);
bool has_inline_attribute(environment const & env, name const & n);
bool has_inline2_attribute(environment const & env, name const & n);
bool has_noinline_attribute(environment const & env, name const & n);
bool has_inline_if_reduce_attribute(environment const & env, name const & n);