diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp index b1c487b669..0c72523585 100644 --- a/src/library/compiler/csimp.cpp +++ b/src/library/compiler/csimp.cpp @@ -1555,13 +1555,8 @@ class csimp_fn { optional 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)); diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp index bb762cc598..2700778f5e 100644 --- a/src/library/compiler/util.cpp +++ b/src/library/compiler/util.cpp @@ -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 { diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h index 73b4e0d62e..75c0ec6058 100644 --- a/src/library/compiler/util.h +++ b/src/library/compiler/util.h @@ -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);