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

feat(library/compiler/util): switch to new attributes implemented in Lean

Browse source
This commit is contained in:
Leonardo de Moura 2019-06-06 15:40:39 -07:00
parent b292fc13cc
commit 0553d60dbf
2 changed files with 18 additions and 82 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/frontends/lean/decl_attributes.cpp
View file

@ -152,11 +152,17 @@ void decl_attributes::parse_compact(parser & p) {
}
void decl_attributes::set_attribute(environment const & env, name const & attr_name, attr_data_ptr data) {
if (!is_attribute(env, attr_name))
if (is_attribute(env, attr_name)) {
auto const & attr = ::lean::get_attribute(env, attr_name);
entry e = {&attr, data};
m_entries = append(m_entries, to_list(e));
} else if (is_new_attribute(env, attr_name)) {
// Temporary Hack... ignore attr_data_ptr
syntax args(box(0));
m_new_entries = cons({attr_name, false, false, args}, m_new_entries);
} else {
throw exception(sstream() << "unknown attribute [" << attr_name << "]");
auto const & attr = ::lean::get_attribute(env, attr_name);
entry e = {&attr, data};
m_entries = append(m_entries, to_list(e));
}
}
attr_data_ptr decl_attributes::get_attribute(environment const & env, name const & attr_name) const {

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

@ -88,53 +88,15 @@ unsigned get_num_nested_lambdas(expr e) {
return r;
}
bool has_inline_attribute(environment const & env, name const & n) {
if (is_elambda_lifting_name(n))
return false; // don't undo lambda lifting
if (has_attribute(env, "inline", n))
return true;
if (is_internal_name(n) && !n.is_atomic()) {
/* Auxiliary declarations such as `f._main` are considered to be marked as `@[inline]`
if `f` is marked. */
return has_inline_attribute(env, n.get_prefix());
}
return false;
}
uint8 has_inline_attribute_core(object* env, object* n);
uint8 has_inline_if_reduce_attribute_core(object* env, object* n);
uint8 has_macro_inline_attribute_core(object* env, object* n);
uint8 has_noinline_attribute_core(object* env, object* n);
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
if (has_attribute(env, "inlineIfReduce", n))
return true;
if (is_internal_name(n) && !n.is_atomic()) {
/* Auxiliary declarations such as `f._main` are considered to be marked as `@[inlineIfReduce]`
if `f` is marked. */
return has_inline_if_reduce_attribute(env, n.get_prefix());
}
return false;
}
bool has_macro_inline_attribute(environment const & env, name const & n) {
if (has_attribute(env, "macroInline", n))
return true;
if (is_internal_name(n) && !n.is_atomic()) {
/* Auxiliary declarations such as `f._main` are considered to be marked as `@[macroInline]`
if `f` is marked. */
return has_macro_inline_attribute(env, n.get_prefix());
}
return false;
}
bool has_noinline_attribute(environment const & env, name const & n) {
if (has_attribute(env, "noinline", n))
return true;
if (is_internal_name(n) && !n.is_atomic()) {
/* Auxiliary declarations such as `f._main` are considered to be marked as `@[noinline]`
if `f` is marked. */
return has_noinline_attribute(env, n.get_prefix());
}
return false;
}
bool has_inline_attribute(environment const & env, name const & n) { return has_inline_attribute_core(env.to_obj_arg(), n.to_obj_arg()); }
bool has_inline_if_reduce_attribute(environment const & env, name const & n) { return has_inline_if_reduce_attribute_core(env.to_obj_arg(), n.to_obj_arg()); }
bool has_macro_inline_attribute(environment const & env, name const & n) { return has_macro_inline_attribute_core(env.to_obj_arg(), n.to_obj_arg()); }
bool has_noinline_attribute(environment const & env, name const & n) { return has_noinline_attribute_core(env.to_obj_arg(), n.to_obj_arg()); }
bool is_lcnf_atom(expr const & e) {
switch (e.kind()) {
@ -688,38 +650,6 @@ void initialize_compiler_util() {
g_builtin_scalar_size->emplace_back(get_uint16_name(), 2);
g_builtin_scalar_size->emplace_back(get_uint32_name(), 4);
g_builtin_scalar_size->emplace_back(get_uint64_name(), 8);
register_system_attribute(basic_attribute::with_check(
"inline", "mark definition to always be inlined",
[](environment const & env, name const & d, bool) -> void {
auto decl = env.get(d);
if (!decl.is_definition())
throw exception("invalid 'inline' use, only definitions can be marked as [inline]");
}));
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 {
auto decl = env.get(d);
if (!decl.is_definition())
throw exception("invalid 'inline_if_reduce' use, only definitions can be marked as [inlineIfReduce]");
}));
register_system_attribute(basic_attribute::with_check(
"noinline", "mark definition to never be inlined",
[](environment const & env, name const & d, bool) -> void {
auto decl = env.get(d);
if (!decl.is_definition())
throw exception("invalid 'noinline' use, only definitions can be marked as [noinline]");
}));
register_system_attribute(basic_attribute::with_check(
"macroInline", "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 'macroInline' use, only definitions can be marked as [macroInline]");
}));
}
void finalize_compiler_util() {