diff --git a/src/Lean/Compiler/InlineAttrs.lean b/src/Lean/Compiler/InlineAttrs.lean index ce785ad3b3..ab377ede67 100644 --- a/src/Lean/Compiler/InlineAttrs.lean +++ b/src/Lean/Compiler/InlineAttrs.lean @@ -12,15 +12,36 @@ inductive InlineAttributeKind where | inline | noinline | macroInline | inlineIfReduce deriving Inhabited, BEq +/-- + This is an approximate test for testing whether `declName` can be annotated with the `[macroInline]` attribute or not. +-/ +private def isValidMacroInline (declName : Name) : CoreM Bool := do + let .defnInfo info ← getConstInfo declName + | return false + unless info.all.length = 1 do + -- We do not allow `[macroInline]` attributes at mutual recursive definitions + return false + let env ← getEnv + let isRec (declName' : Name) : Bool := + isBRecOnRecursor env declName' || + declName' == ``WellFounded.fix || + declName' == declName ++ `_unary -- Auxiliary declaration created by `WF` module + if Option.isSome <| info.value.find? fun e => e.isConst && isRec e.constName! then + -- It contains a `brecOn` or `WellFounded.fix` application. So, it should be recursvie + return false + return true + builtin_initialize inlineAttrs : EnumAttributes InlineAttributeKind ← registerEnumAttributes `inlineAttrs [(`inline, "mark definition to always be inlined", InlineAttributeKind.inline), (`inlineIfReduce, "mark definition to be inlined when resultant term after reduction is not a `cases_on` application", InlineAttributeKind.inlineIfReduce), (`noinline, "mark definition to never be inlined", InlineAttributeKind.noinline), (`macroInline, "mark definition to always be inlined before ANF conversion", InlineAttributeKind.macroInline)] - (fun declName _ => do - let env ← getEnv - ofExcept <| checkIsDefinition env declName) + fun declName kind => do + ofExcept <| checkIsDefinition (← getEnv) declName + if kind matches .macroInline then + unless (← isValidMacroInline declName) do + throwError "invalid use of `[macro_inline]` attribute at `{declName}`, it is not supported in this kind of declaration, declaration must be a non-recursive definition" private partial def hasInlineAttrAux (env : Environment) (kind : InlineAttributeKind) (n : Name) : Bool := /- We never inline auxiliary declarations created by eager lambda lifting -/ diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp index c4e8d9d44e..6730492995 100644 --- a/src/library/compiler/util.cpp +++ b/src/library/compiler/util.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/for_each_fn.h" #include "kernel/replace_fn.h" +#include "kernel/find_fn.h" #include "kernel/inductive.h" #include "kernel/instantiate.h" #include "kernel/kernel_exception.h" @@ -129,6 +130,16 @@ struct unfold_macro_defs_fn : public replace_visitor { unfold_macro_defs_fn(environment const & env):m_env(env) {} + bool should_macro_inline(name const & n) { + if (!has_macro_inline_attribute(m_env, n)) return false; + auto info = m_env.get(n); + if (!info.has_value()) + return false; + bool is_rec = static_cast(find(info.get_value(), [&](expr const & e, unsigned) { return is_const(e, n); })); + // We do not macro_inline recursive definitions. TODO: check that when setting the attribute. + return !is_rec; + } + virtual expr visit_app(expr const & e) override { buffer args; expr const & fn = get_app_args(e, args); @@ -141,7 +152,7 @@ struct unfold_macro_defs_fn : public replace_visitor { } if (is_constant(fn)) { name const & n = const_name(fn); - if (has_macro_inline_attribute(m_env, n)) { + if (should_macro_inline(n)) { expr new_fn = instantiate_value_lparams(m_env.get(n), const_levels(fn)); std::reverse(args.begin(), args.end()); return visit(apply_beta(new_fn, args.size(), args.data())); @@ -156,7 +167,7 @@ struct unfold_macro_defs_fn : public replace_visitor { virtual expr visit_constant(expr const & e) override { name const & n = const_name(e); - if (has_macro_inline_attribute(m_env, n)) { + if (should_macro_inline(n)) { return visit(instantiate_value_lparams(m_env.get(n), const_levels(e))); } else { return e; diff --git a/tests/lean/1363.lean b/tests/lean/1363.lean new file mode 100644 index 0000000000..543a6db5e9 --- /dev/null +++ b/tests/lean/1363.lean @@ -0,0 +1,25 @@ +import Lean.Data.Parsec +open Lean Parsec + +@[macroInline] -- Error +def f : Nat → Nat + | 0 => 0 + | n + 1 => f n + +@[macroInline] -- Error +def g : Nat → Nat + | 0 => 0 + | n + 1 => g n +termination_by g x => x + +@[macroInline] -- Error +def h : Nat → Nat → Nat + | 0, _ => 0 + | n + 1, m => h n m +termination_by h x y => x + +@[macroInline] -- Error +partial def skipMany (p : Parsec α) (it : String.Iterator) : Parsec PUnit := do + match p it with + | .success it _ => skipMany p it + | .error _ _ => pure () diff --git a/tests/lean/1363.lean.expected.out b/tests/lean/1363.lean.expected.out new file mode 100644 index 0000000000..b9c1a7cad7 --- /dev/null +++ b/tests/lean/1363.lean.expected.out @@ -0,0 +1,5 @@ +1363.lean:4:2-4:13: error: invalid use of `[macro_inline]` attribute at `f`, it is not supported in this kind of declaration, declaration must be a non-recursive definition +1363.lean:9:2-9:13: error: invalid use of `[macro_inline]` attribute at `g`, it is not supported in this kind of declaration, declaration must be a non-recursive definition +1363.lean:15:2-15:13: error: invalid use of `[macro_inline]` attribute at `h._unary`, it is not supported in this kind of declaration, declaration must be a non-recursive definition +1363.lean:15:2-15:13: error: invalid use of `[macro_inline]` attribute at `h`, it is not supported in this kind of declaration, declaration must be a non-recursive definition +1363.lean:21:2-21:13: error: invalid use of `[macro_inline]` attribute at `skipMany`, it is not supported in this kind of declaration, declaration must be a non-recursive definition