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

feat(library/compiler/inliner): add [macro_inline] attribute

Browse source 
For the old compiler stack, it behaves like `[inline]`.
For the new compiler stack, it instructs the compiler to inline
definitions before LCNF/ANF conversion.
This commit is contained in:
Leonardo de Moura 2018-09-23 11:29:46 -07:00
parent 41c0bc87fd
commit 3473822c01
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/library/compiler/inliner.cpp
View file

@ -19,6 +19,9 @@ bool is_inline(environment const & env, name const & n) {
if (has_attribute(env, "inline", n)) {
return true;
}
if (has_attribute(env, "macro_inline", n)) {
return true;
}
// decl._main is an auxiliary declaration, check decl instead
if (n.is_string() && n.get_string().data()[0] == '_') {
return is_inline(env, n.get_prefix());
@ -34,6 +37,14 @@ void initialize_inliner() {
if (!decl.is_definition())
throw exception("invalid 'inline' use, only definitions can be marked as inline");
}));
register_system_attribute(basic_attribute::with_check(
"macro_inline", "mark definition to always be inlined before ANF conversion",
[](environment const & env, name const & d, bool) -> void {
auto decl = env.get(d);
if (!decl.is_definition())
throw exception("invalid 'macro_inline' use, only definitions can be marked as inline");
}));
}
void finalize_inliner() {