diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp index c36a7fb409..e68789f925 100644 --- a/src/library/compiler/compiler.cpp +++ b/src/library/compiler/compiler.cpp @@ -20,6 +20,7 @@ Author: Leonardo de Moura #include "library/compiler/erase_irrelevant.h" #include "library/compiler/specialize.h" #include "library/compiler/eager_lambda_lifting.h" +#include "library/compiler/implemented_by_attribute.h" #include "library/compiler/lambda_lifting.h" #include "library/compiler/extract_closed.h" #include "library/compiler/reduce_arity.h" @@ -185,7 +186,9 @@ environment compile(environment const & env, options const & opts, names cs) { if (length(cs) == 1) { name c = get_real_name(head(cs)); - if (skip_code_generation(env, c)) { + if (has_implemented_by_attribute(env, c)) + return env; + if (is_extern_or_init_constant(env, c)) { /* Generate boxed version for extern/native constant if needed. */ return ir::add_extern(env, c); } diff --git a/src/library/compiler/extern_attribute.cpp b/src/library/compiler/extern_attribute.cpp index ee88f206b4..447f892920 100644 --- a/src/library/compiler/extern_attribute.cpp +++ b/src/library/compiler/extern_attribute.cpp @@ -31,8 +31,8 @@ bool is_extern_constant(environment const & env, name const & c) { return static_cast(get_extern_attr_data(env, c)); } -bool skip_code_generation(environment const & env, name const & c) { - if (is_extern_constant(env, c) || has_implemented_by_attribute(env, c)) { +bool is_extern_or_init_constant(environment const & env, name const & c) { + if (is_extern_constant(env, c)) { return true; } else if (auto info = env.find(c)) { // `declarations marked with `init` @@ -81,7 +81,7 @@ bool get_extern_borrowed_info(environment const & env, name const & c, buffer get_extern_constant_ll_type(environment const & env, name const & c) { - if (skip_code_generation(env, c)) { + if (is_extern_or_init_constant(env, c)) { unsigned arity = 0; expr type = env.get(c).get_type(); type_checker::state st(env); diff --git a/src/library/compiler/extern_attribute.h b/src/library/compiler/extern_attribute.h index db6ed58817..84c6d3194b 100644 --- a/src/library/compiler/extern_attribute.h +++ b/src/library/compiler/extern_attribute.h @@ -9,7 +9,7 @@ Authors: Leonardo de Moura #include "kernel/environment.h" namespace lean { bool is_extern_constant(environment const & env, name const & c); -bool skip_code_generation(environment const & env, name const & c); +bool is_extern_or_init_constant(environment const & env, name const & c); optional get_extern_constant_ll_type(environment const & env, name const & c); optional get_extern_constant_arity(environment const & env, name const & c); typedef object_ref extern_attr_data_value;