From 8f76df4823846914dc4e943154a4df87d2a10dff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 15 Oct 2018 13:02:11 -0700 Subject: [PATCH] feat(library/compiler): add `[specialize]` attribute --- src/library/compiler/specialize.cpp | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp index d3f283769e..f5e26a12fd 100644 --- a/src/library/compiler/specialize.cpp +++ b/src/library/compiler/specialize.cpp @@ -7,11 +7,23 @@ Author: Leonardo de Moura #include "runtime/flet.h" #include "kernel/instantiate.h" #include "library/module.h" +#include "library/attribute_manager.h" #include "library/compiler/util.h" #include "library/trace.h" namespace lean { +bool has_specialize_attribute(environment const & env, name const & n) { + if (has_attribute(env, "specialize", n)) + return true; + if (is_internal_name(n) && !n.is_atomic()) { + /* Auxiliary declarations such as `f._main` are considered to be marked as `@[specialize]` + if `f` is marked. */ + return has_specialize_attribute(env, n.get_prefix()); + } + return false; +} + enum class spec_arg_kind { Fixed, FixedInst, Other }; static spec_arg_kind to_spec_arg_kind(object_ref const & r) { lean_assert(is_scalar(r)); return static_cast(unbox(r.raw())); @@ -305,6 +317,14 @@ void initialize_specialize() { g_ext = new specialize_ext_reg(); spec_info_modification::init(); register_trace_class({"compiler", "spec_info"}); + + register_system_attribute(basic_attribute::with_check( + "specialize", "mark definition to always be specialized", + [](environment const & env, name const & d, bool) -> void { + auto decl = env.get(d); + if (!decl.is_definition()) + throw exception("invalid 'specialize' use, only definitions can be marked as specialize"); + })); } void finalize_specialize() {