From ca8be3857ce33b035be11036d43c4568ff46b779 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 16 Aug 2016 17:51:33 -0400 Subject: [PATCH] feat(library/user_attribute): add user-defined attributes and make attribute_manager environment-aware --- library/init/meta/attribute.lean | 14 +++ library/init/meta/default.lean | 2 +- src/frontends/lean/decl_attributes.cpp | 4 +- src/frontends/lean/old_attributes.cpp | 7 +- src/frontends/lean/pattern_attribute.cpp | 4 +- src/frontends/lean/print_cmd.cpp | 8 +- src/library/abbreviation.cpp | 14 ++- src/library/attribute_manager.cpp | 91 ++++++++++----- src/library/attribute_manager.h | 31 ++++-- src/library/class.cpp | 16 ++- src/library/compiler/inliner.cpp | 15 ++- src/library/constants.cpp | 4 + src/library/constants.h | 1 + src/library/constants.txt | 1 + src/library/init_module.cpp | 12 +- src/library/normalize.cpp | 9 +- src/library/reducible.cpp | 10 +- src/library/relation_manager.cpp | 32 ++++-- .../tactic/backward/backward_lemmas.cpp | 23 ++-- .../defeq_simplifier/defeq_simp_lemmas.cpp | 2 +- src/library/tactic/simplifier/simp_lemmas.cpp | 4 +- src/library/unification_hint.cpp | 2 +- src/library/user_recursors.cpp | 13 ++- src/library/vm/CMakeLists.txt | 2 +- src/library/vm/init_module.cpp | 3 + src/library/vm/user_attribute.cpp | 105 ++++++++++++++++++ src/library/vm/user_attribute.h | 12 ++ tests/lean/user_attribute.lean | 38 +++++++ tests/lean/user_attribute.lean.expected.out | 64 +++++++++++ 29 files changed, 428 insertions(+), 115 deletions(-) create mode 100644 library/init/meta/attribute.lean create mode 100644 src/library/vm/user_attribute.cpp create mode 100644 src/library/vm/user_attribute.h create mode 100644 tests/lean/user_attribute.lean create mode 100644 tests/lean/user_attribute.lean.expected.out diff --git a/library/init/meta/attribute.lean b/library/init/meta/attribute.lean new file mode 100644 index 0000000000..65d0d61dc8 --- /dev/null +++ b/library/init/meta/attribute.lean @@ -0,0 +1,14 @@ +/- +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Ullrich +-/ +prelude +import init.meta.environment + +meta_constant attribute.get_instances : environment → name → list name + +/- The structure of a user-defined attribute. To declare a new attribute, define an instance of this + structure and annotate it with the (built-in) [user_attribute] attribute. -/ +structure user_attribute := +(descr : string) diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean index 5094e46c5e..170483c465 100644 --- a/library/init/meta/default.lean +++ b/library/init/meta/default.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ prelude import init.meta.name init.meta.options init.meta.format init.meta.rb_map -import init.meta.level init.meta.expr init.meta.environment +import init.meta.level init.meta.expr init.meta.environment init.meta.attribute import init.meta.tactic init.meta.contradiction_tactic init.meta.constructor_tactic import init.meta.injection_tactic init.meta.relation_tactics init.meta.fun_info import init.meta.congr_lemma init.meta.match_tactic init.meta.ac_tactics diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index 46ee43c34d..00fe33a279 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -36,10 +36,10 @@ void decl_attributes::parse(parser & p) { throw parser_error("invalid 'priority', argument does not evaluate to a numeral", pos); } } else { - if (!is_attribute(name)) + if (!is_attribute(p.env(), name)) throw parser_error(sstream() << "unknown attribute [" << name << "]", pos); - auto const & attr = get_attribute(name); + auto const & attr = get_attribute(p.env(), name); for (auto const & entry : m_entries) { if (are_incompatible(*entry.m_attr, attr)) { throw parser_error(sstream() << "invalid attribute [" << name diff --git a/src/frontends/lean/old_attributes.cpp b/src/frontends/lean/old_attributes.cpp index 59fb157502..e83cfb9b6e 100644 --- a/src/frontends/lean/old_attributes.cpp +++ b/src/frontends/lean/old_attributes.cpp @@ -8,9 +8,10 @@ Author: Leonardo de Moura namespace lean { void initialize_old_attributes() { - register_attribute(basic_attribute("elim", "elimination rule that is eagerly applied by blast grinder")); - register_attribute(basic_attribute("no_pattern", "do not consider terms containing this declaration in the pattern inference procedure")); - register_attribute(basic_attribute("forward", "forward chaining")); + register_system_attribute(basic_attribute("elim", "elimination rule that is eagerly applied by blast grinder")); + register_system_attribute(basic_attribute("no_pattern", + "do not consider terms containing this declaration in the pattern inference procedure")); + register_system_attribute(basic_attribute("forward", "forward chaining")); } void finalize_old_attributes() {} } diff --git a/src/frontends/lean/pattern_attribute.cpp b/src/frontends/lean/pattern_attribute.cpp index 9d76872829..933b5db1a6 100644 --- a/src/frontends/lean/pattern_attribute.cpp +++ b/src/frontends/lean/pattern_attribute.cpp @@ -12,8 +12,8 @@ bool has_pattern_attribute(environment const & env, name const & d) { } void initialize_pattern_attribute() { - register_attribute(basic_attribute("pattern", "mark that a definition can be used in a pattern" - "(remark: the dependent pattern matching compiler will unfold the definition)")); + register_system_attribute(basic_attribute("pattern", "mark that a definition can be used in a pattern" + "(remark: the dependent pattern matching compiler will unfold the definition)")); } void finalize_pattern_attribute() { diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index c8c1128296..ea3f576cc3 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -248,7 +248,7 @@ static void print_attributes(parser const & p, name const & n) { environment const & env = p.env(); std::ostream & out = p.ios().get_regular_stream(); buffer attrs; - get_attributes(attrs); + get_attributes(p.env(), attrs); std::sort(attrs.begin(), attrs.end(), [](attribute const * a1, attribute const * a2) { return a1->get_name() < a2->get_name(); }); @@ -621,7 +621,7 @@ environment print_cmd(parser & p) { } else if (p.curr_is_token_or_id(get_attributes_tk())) { p.next(); buffer attrs; - get_attributes(attrs); + get_attributes(p.env(), attrs); std::sort(attrs.begin(), attrs.end(), [](attribute const * a1, attribute const * a2) { return a1->get_name() < a2->get_name(); }); @@ -671,9 +671,9 @@ environment print_cmd(parser & p) { else if (name == "light") { // print_light_rules(p); } else { - if (!is_attribute(name)) + if (!is_attribute(p.env(), name)) throw parser_error(sstream() << "unknown attribute [" << name << "]", pos); - auto const & attr = get_attribute(name); + auto const & attr = get_attribute(p.env(), name); print_attribute(p, attr); } } else if (print_polymorphic(p)) { diff --git a/src/library/abbreviation.cpp b/src/library/abbreviation.cpp index 514eb699e2..5727e9504c 100644 --- a/src/library/abbreviation.cpp +++ b/src/library/abbreviation.cpp @@ -116,11 +116,15 @@ void initialize_abbreviation() { g_class_name = new name("abbreviation"); g_key = new std::string("ABBREV"); abbrev_ext::initialize(); - register_attribute(basic_attribute("parsing_only", "parsing-only abbreviation", [](environment const & env, io_state const &, name const & d, unsigned, bool) { - if (!is_abbreviation(env, d)) - throw exception(sstream() << "invalid '[parsing_only]' attribute, " << d << " is not an abbreviation"); - return env; - })); + register_system_attribute(basic_attribute("parsing_only", "parsing-only abbreviation", + [](environment const & env, io_state const &, name const & d, unsigned, + bool) { + if (!is_abbreviation(env, d)) + throw exception( + sstream() << "invalid '[parsing_only]' attribute, " << d + << " is not an abbreviation"); + return env; + })); } void finalize_abbreviation() { diff --git a/src/library/attribute_manager.cpp b/src/library/attribute_manager.cpp index 5e56a271ef..62583e5160 100644 --- a/src/library/attribute_manager.cpp +++ b/src/library/attribute_manager.cpp @@ -15,29 +15,47 @@ Author: Leonardo de Moura namespace lean { -static name_map * g_attributes; +static name_map * g_system_attributes; +static std::unique_ptr g_user_attribute_ext; + +name_map user_attribute_ext::get_attributes(environment const &) { + return {}; +} +void set_user_attribute_ext(std::unique_ptr ext) { + g_user_attribute_ext = std::move(ext); +} + static std::vector> * g_incomp = nullptr; static std::string * g_key = nullptr; -void register_attribute(attribute_ptr attr) { - lean_assert(!is_attribute(attr->get_name())); - (*g_attributes)[attr->get_name()] = attr; +static bool is_system_attribute(name const & attr) { + return g_system_attributes->find(attr) != nullptr; +} +void register_system_attribute(attribute_ptr attr) { + lean_assert(!is_system_attribute(attr->get_name())); + (*g_system_attributes)[attr->get_name()] = attr; } -bool is_attribute(name const & attr) { - return g_attributes->find(attr) != nullptr; +bool is_attribute(environment const & env, name const & attr) { + return is_system_attribute(attr) || g_user_attribute_ext->get_attributes(env).find(attr) != nullptr; } -[[ noreturn ]] void throw_unknown_attribute(name const & attr) { - throw exception(sstream() << "unknown attribute '" << attr << "'"); -} - -attribute const & get_attribute(name const & attr) { - auto it = g_attributes->find(attr); +attribute const & get_system_attribute(name const & attr) { + auto it = g_system_attributes->find(attr); if (it) return **it; - throw_unknown_attribute(attr); + throw exception(sstream() << "unknown system attribute '" << attr << "'"); +} + +attribute const & get_attribute(environment const & env, name const & attr) { + auto it = g_system_attributes->find(attr); + if (it) + return **it; + it = g_user_attribute_ext->get_attributes(env).find(attr); + if (it) + return **it; + throw exception(sstream() << "unknown attribute '" << attr << "'"); } struct attr_record { @@ -64,7 +82,7 @@ struct attr_record_cmp { }; struct attr_entry { - name m_attr; + name m_attr; unsigned m_prio; attr_record m_record; @@ -92,12 +110,20 @@ struct attr_config { static void write_entry(serializer & s, entry const & e) { s << e.m_attr << e.m_prio << e.m_record.m_decl; lean_assert(e.m_record.m_data); - get_attribute(e.m_attr).write_entry(s, *e.m_record.m_data); + if (is_system_attribute(e.m_attr)) + get_system_attribute(e.m_attr).write_entry(s, *e.m_record.m_data); + else + // dispatch over the extension, since we can't call get_attribute without an env + g_user_attribute_ext->write_entry(s, *e.m_record.m_data); } static entry read_entry(deserializer & d) { entry e; d >> e.m_attr >> e.m_prio >> e.m_record.m_decl; - e.m_record.m_data = get_attribute(e.m_attr).read_entry(d); + if (is_system_attribute(e.m_attr)) + e.m_record.m_data = get_system_attribute(e.m_attr).read_entry(d); + else + // dispatch over the extension, since we can't call get_attribute without an env + e.m_record.m_data = g_user_attribute_ext->read_entry(d); return e; } static optional get_fingerprint(entry const & e) { @@ -156,8 +182,8 @@ void indices_attribute_data::parse(abstract_parser & p) { } void register_incompatible(char const * attr1, char const * attr2) { - lean_assert(is_attribute(attr1)); - lean_assert(is_attribute(attr2)); + lean_assert(is_system_attribute(attr1)); + lean_assert(is_system_attribute(attr2)); name s1(attr1); name s2(attr2); if (s1 > s2) @@ -165,18 +191,21 @@ void register_incompatible(char const * attr1, char const * attr2) { g_incomp->emplace_back(s1, s2); } -void get_attributes(buffer & r) { - g_attributes->for_each([&](name const &, attribute_ptr const & attr) { +void get_attributes(environment const & env, buffer & r) { + g_system_attributes->for_each([&](name const &, attribute_ptr const & attr) { + r.push_back(&*attr); + }); + g_user_attribute_ext->get_attributes(env).for_each([&](name const &, attribute_ptr const & attr) { r.push_back(&*attr); }); } bool has_attribute(environment const & env, char const * attr, name const & d) { - return static_cast(get_attribute(attr).get(env, d)); + return static_cast(get_attribute(env, attr).get(env, d)); } void get_attribute_instances(environment const & env, char const * attr, buffer & r) { - return get_attribute(attr).get_instances(env, r); + return get_attribute(env, attr).get_instances(env, r); } priority_queue get_attribute_instances_by_prio(environment const & env, name const & attr) { @@ -188,14 +217,14 @@ priority_queue get_attribute_instances_by_prio(environment environment set_attribute(environment const & env, io_state const & ios, char const * name, lean::name const & d, unsigned prio, list const & params, bool persistent) { - auto const & attr = get_attribute(name); + auto const & attr = get_attribute(env, name); lean_assert(dynamic_cast(&attr)); return static_cast(attr).set(env, ios, d, prio, {params}, persistent); } environment set_attribute(environment const & env, io_state const & ios, char const * name, lean::name const & d, unsigned prio, bool persistent) { - auto const & attr = get_attribute(name); + auto const & attr = get_attribute(env, name); lean_assert(dynamic_cast(&attr)); return static_cast(attr).set(env, ios, d, prio, persistent); } @@ -205,11 +234,11 @@ environment set_attribute(environment const & env, io_state const & ios, char co } unsigned get_attribute_prio(environment const & env, name const & attr, name const & d) { - return get_attribute(attr).get_prio(env, d); + return get_attribute(env, attr).get_prio(env, d); } list get_attribute_params(environment const & env, name const & attr, name const & d) { - if (auto attribute = dynamic_cast(&get_attribute(attr))) { + if (auto attribute = dynamic_cast(&get_attribute(env, attr))) { auto data = attribute->get_data(env, d); lean_assert(data); return data->m_idxs; @@ -226,9 +255,10 @@ bool are_incompatible(attribute const & attr1, attribute const & attr2) { } void initialize_attribute_manager() { - g_attributes = new name_map(); - g_incomp = new std::vector>(); - g_key = new std::string("ATTR"); + g_system_attributes = new name_map(); + g_user_attribute_ext.reset(new user_attribute_ext()); + g_incomp = new std::vector>(); + g_key = new std::string("ATTR"); attribute_ext::initialize(); } @@ -236,6 +266,7 @@ void finalize_attribute_manager() { attribute_ext::finalize(); delete g_key; delete g_incomp; - delete g_attributes; + g_user_attribute_ext.release(); + delete g_system_attributes; } } diff --git a/src/library/attribute_manager.h b/src/library/attribute_manager.h index 126a9329da..a714721015 100644 --- a/src/library/attribute_manager.h +++ b/src/library/attribute_manager.h @@ -100,9 +100,9 @@ protected: return attr_data_ptr(data); } public: - typed_attribute(char const * id, char const * descr, on_set_proc on_set) : attribute(id, descr), + typed_attribute(name const & id, char const * descr, on_set_proc on_set) : attribute(id, descr), m_on_set(on_set) {} - typed_attribute(char const * id, char const * descr) : typed_attribute(id, descr, {}) {} + typed_attribute(name const & id, char const * descr) : typed_attribute(id, descr, {}) {} virtual attr_data_ptr parse_data(abstract_parser & p) const final override { auto data = new Data; @@ -155,20 +155,31 @@ template class typed_attribute; /** \brief Attribute that represents a list of indices. input and output are 1-indexed for convenience. */ typedef typed_attribute indices_attribute; -void register_attribute(attribute_ptr); -attribute const & get_attribute(name const & attr); -void get_attributes(buffer &); +class user_attribute_ext { +public: + virtual name_map get_attributes(environment const & env); + virtual void write_entry(serializer &, attr_data const &) {} + virtual attr_data_ptr read_entry(deserializer &) { + return attr_data_ptr(new attr_data); + } +}; +/** \brief Register the user_attribute handlers, if included in the compilation */ +void set_user_attribute_ext(std::unique_ptr); + +void register_system_attribute(attribute_ptr); template -void register_attribute(Attribute attr) { - register_attribute(attribute_ptr(new Attribute(attr))); +void register_system_attribute(Attribute attr) { + register_system_attribute(attribute_ptr(new Attribute(attr))); } - void register_incompatible(char const * attr1, char const * attr2); -// TODO(sullrich): all of these should become members of/return attribute or a subclass -bool is_attribute(name const & attr); +bool is_attribute(environment const & env, name const & attr); +attribute const & get_attribute(environment const & env, name const & attr); +attribute const & get_system_attribute(name const & attr); +void get_attributes(environment const & env, buffer &); +// TODO(sullrich): all of these should become members of/return attribute or a subclass environment set_attribute(environment const & env, io_state const & ios, char const * attr, name const & d, unsigned prio, list const & params, bool persistent); environment set_attribute(environment const & env, io_state const & ios, char const * attr, diff --git a/src/library/class.cpp b/src/library/class.cpp index 8e289f1338..4117abfcb2 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -320,13 +320,17 @@ void initialize_class() { g_key = new std::string("class"); class_ext::initialize(); - register_attribute(basic_attribute("class", "type class", [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) { - return add_class(env, d, persistent); - })); + register_system_attribute(basic_attribute("class", "type class", + [](environment const & env, io_state const &, name const & d, unsigned, + bool persistent) { + return add_class(env, d, persistent); + })); - register_attribute(basic_attribute("instance", "type class instance", [](environment const & env, io_state const &, name const & d, unsigned prio, bool persistent) { - return add_instance(env, d, prio, persistent); - })); + register_system_attribute(basic_attribute("instance", "type class instance", + [](environment const & env, io_state const &, name const & d, + unsigned prio, bool persistent) { + return add_instance(env, d, prio, persistent); + })); } void finalize_class() { diff --git a/src/library/compiler/inliner.cpp b/src/library/compiler/inliner.cpp index c9434ef97b..bac5fdf618 100644 --- a/src/library/compiler/inliner.cpp +++ b/src/library/compiler/inliner.cpp @@ -21,12 +21,15 @@ bool is_inline(environment const & env, name const & n) { } void initialize_inliner() { - register_attribute(basic_attribute("inline", "mark definition to always be inlined", [](environment const & env, io_state const &, name const & d, unsigned, bool) { - auto decl = env.get(d); - if (!decl.is_definition() || decl.is_theorem()) - throw exception("invalid 'inline' use, only definitions can be marked as inline"); - return env; - })); + register_system_attribute(basic_attribute("inline", "mark definition to always be inlined", + [](environment const & env, io_state const &, name const & d, unsigned, + bool) { + auto decl = env.get(d); + if (!decl.is_definition() || decl.is_theorem()) + throw exception( + "invalid 'inline' use, only definitions can be marked as inline"); + return env; + })); } void finalize_inliner() { diff --git a/src/library/constants.cpp b/src/library/constants.cpp index b966c6b2eb..e18d87608b 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -323,6 +323,7 @@ name const * g_unification_constraint = nullptr; name const * g_unification_constraint_mk = nullptr; name const * g_unit = nullptr; name const * g_unit_star = nullptr; +name const * g_user_attribute = nullptr; name const * g_weak_order = nullptr; name const * g_well_founded = nullptr; name const * g_xor = nullptr; @@ -651,6 +652,7 @@ void initialize_constants() { g_unification_constraint_mk = new name{"unification_constraint", "mk"}; g_unit = new name{"unit"}; g_unit_star = new name{"unit", "star"}; + g_user_attribute = new name{"user_attribute"}; g_weak_order = new name{"weak_order"}; g_well_founded = new name{"well_founded"}; g_xor = new name{"xor"}; @@ -980,6 +982,7 @@ void finalize_constants() { delete g_unification_constraint_mk; delete g_unit; delete g_unit_star; + delete g_user_attribute; delete g_weak_order; delete g_well_founded; delete g_xor; @@ -1308,6 +1311,7 @@ name const & get_unification_constraint_name() { return *g_unification_constrain name const & get_unification_constraint_mk_name() { return *g_unification_constraint_mk; } name const & get_unit_name() { return *g_unit; } name const & get_unit_star_name() { return *g_unit_star; } +name const & get_user_attribute_name() { return *g_user_attribute; } name const & get_weak_order_name() { return *g_weak_order; } name const & get_well_founded_name() { return *g_well_founded; } name const & get_xor_name() { return *g_xor; } diff --git a/src/library/constants.h b/src/library/constants.h index ed947c776a..df4a9c12ab 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -325,6 +325,7 @@ name const & get_unification_constraint_name(); name const & get_unification_constraint_mk_name(); name const & get_unit_name(); name const & get_unit_star_name(); +name const & get_user_attribute_name(); name const & get_weak_order_name(); name const & get_well_founded_name(); name const & get_xor_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 073c72ff25..800a61256e 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -318,6 +318,7 @@ unification_constraint unification_constraint.mk unit unit.star +user_attribute weak_order well_founded xor diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index c0676e621e..e112c80e8f 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -67,9 +67,15 @@ namespace lean { void initialize_library_core_module() { initialize_constants(); initialize_trace(); + initialize_module(); + initialize_scoped_ext(); + initialize_attribute_manager(); } void finalize_library_core_module() { + finalize_attribute_manager(); + finalize_scoped_ext(); + finalize_module(); finalize_trace(); finalize_constants(); } @@ -98,11 +104,8 @@ void initialize_library_module() { initialize_annotation(); initialize_quote(); initialize_explicit(); - initialize_module(); initialize_protected(); initialize_private(); - initialize_scoped_ext(); - initialize_attribute_manager(); initialize_reducible(); initialize_aliases(); initialize_export_decl(); @@ -160,10 +163,8 @@ void finalize_library_module() { finalize_export_decl(); finalize_aliases(); finalize_reducible(); - finalize_scoped_ext(); finalize_private(); finalize_protected(); - finalize_module(); finalize_explicit(); finalize_quote(); finalize_annotation(); @@ -179,7 +180,6 @@ void finalize_library_module() { finalize_placeholder(); finalize_print(); finalize_fingerprint(); - finalize_attribute_manager(); finalize_metavar_context(); finalize_local_context(); diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index 3c7d3df6e9..05d21320ee 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -49,9 +49,12 @@ bool has_constructor_hint(environment const & env, name const & d) { } void initialize_normalize() { - register_attribute(indices_attribute("unfold", "unfold definition when the given positions are constructors")); - register_attribute(basic_attribute("unfold_full", "instructs normalizer (and simplifier) that function application (f a_1 ... a_n) should be unfolded when it is fully applied")); - register_attribute(basic_attribute("constructor", "instructs normalizer (and simplifier) that function application (f ...) should be unfolded when it is the major premise of a constructor like operator")); + register_system_attribute( + indices_attribute("unfold", "unfold definition when the given positions are constructors")); + register_system_attribute(basic_attribute("unfold_full", + "instructs normalizer (and simplifier) that function application (f a_1 ... a_n) should be unfolded when it is fully applied")); + register_system_attribute(basic_attribute("constructor", + "instructs normalizer (and simplifier) that function application (f ...) should be unfolded when it is the major premise of a constructor like operator")); } void finalize_normalize() { diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp index ba3e8d8aab..72ee4d5d5d 100644 --- a/src/library/reducible.cpp +++ b/src/library/reducible.cpp @@ -36,7 +36,7 @@ template class typed_attribute; typedef typed_attribute reducibility_attribute; static reducibility_attribute const & get_reducibility_attribute() { - return static_cast(get_attribute("reducibility")); + return static_cast(get_system_attribute("reducibility")); } class proxy_attribute : public basic_attribute { @@ -70,11 +70,11 @@ public: }; void initialize_reducible() { - register_attribute(reducibility_attribute("reducibility", "internal attribute for storing reducibility")); + register_system_attribute(reducibility_attribute("reducibility", "internal attribute for storing reducibility")); - register_attribute(proxy_attribute("reducible", "reducible", reducible_status::Reducible)); - register_attribute(proxy_attribute("semireducible", "semireducible", reducible_status::Semireducible)); - register_attribute(proxy_attribute("irreducible", "irreducible", reducible_status::Irreducible)); + register_system_attribute(proxy_attribute("reducible", "reducible", reducible_status::Reducible)); + register_system_attribute(proxy_attribute("semireducible", "semireducible", reducible_status::Semireducible)); + register_system_attribute(proxy_attribute("irreducible", "irreducible", reducible_status::Irreducible)); register_incompatible("reducible", "semireducible"); register_incompatible("reducible", "irreducible"); diff --git a/src/library/relation_manager.cpp b/src/library/relation_manager.cpp index 810d546138..46d62c0853 100644 --- a/src/library/relation_manager.cpp +++ b/src/library/relation_manager.cpp @@ -325,21 +325,29 @@ is_relation_pred mk_is_relation_pred(environment const & env) { void initialize_relation_manager() { g_key = new std::string("REL"); rel_ext::initialize(); - register_attribute(basic_attribute("refl", "reflexive relation", [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) { - return add_refl(env, d, persistent); - })); + register_system_attribute(basic_attribute("refl", "reflexive relation", + [](environment const & env, io_state const &, name const & d, unsigned, + bool persistent) { + return add_refl(env, d, persistent); + })); - register_attribute(basic_attribute("symm", "symmetric relation", [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) { - return add_symm(env, d, persistent); - })); + register_system_attribute(basic_attribute("symm", "symmetric relation", + [](environment const & env, io_state const &, name const & d, unsigned, + bool persistent) { + return add_symm(env, d, persistent); + })); - register_attribute(basic_attribute("trans", "transitive relation", [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) { - return add_trans(env, d, persistent); - })); + register_system_attribute(basic_attribute("trans", "transitive relation", + [](environment const & env, io_state const &, name const & d, unsigned, + bool persistent) { + return add_trans(env, d, persistent); + })); - register_attribute(basic_attribute("subst", "substitution", [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) { - return add_subst(env, d, persistent); - })); + register_system_attribute(basic_attribute("subst", "substitution", + [](environment const & env, io_state const &, name const & d, unsigned, + bool persistent) { + return add_subst(env, d, persistent); + })); } void finalize_relation_manager() { diff --git a/src/library/tactic/backward/backward_lemmas.cpp b/src/library/tactic/backward/backward_lemmas.cpp index b773b867ec..5358c1acfa 100644 --- a/src/library/tactic/backward/backward_lemmas.cpp +++ b/src/library/tactic/backward/backward_lemmas.cpp @@ -163,16 +163,19 @@ vm_obj tactic_backward_lemmas_find(vm_obj const & lemmas, vm_obj const & h, vm_o void initialize_backward_lemmas() { register_trace_class(name{"tactic", "back_chaining"}); - register_attribute(intro_attribute("intro", "introduction rule for backward chaining", [](environment const & env, io_state const & ios, name const & c, unsigned, intro_attr_data data, bool) { - if (data.m_eager) - return env; // FIXME: support old blast attributes - aux_type_context ctx(env, ios.get_options()); - auto index = get_backward_target(ctx, c); - if (!index || index->kind() != expr_kind::Constant) - throw exception(sstream() << "invalid [intro] attribute for '" << c - << "', head symbol of resulting type must be a constant"); - return env; - })); + register_system_attribute(intro_attribute("intro", "introduction rule for backward chaining", + [](environment const & env, io_state const & ios, name const & c, + unsigned, intro_attr_data data, bool) { + if (data.m_eager) + return env; // FIXME: support old blast attributes + aux_type_context ctx(env, ios.get_options()); + auto index = get_backward_target(ctx, c); + if (!index || index->kind() != expr_kind::Constant) + throw exception( + sstream() << "invalid [intro] attribute for '" << c + << "', head symbol of resulting type must be a constant"); + return env; + })); DECLARE_VM_BUILTIN(name({"tactic", "mk_back_lemmas_core"}), tactic_mk_backward_lemmas); DECLARE_VM_BUILTIN(name({"tactic", "back_lemmas_insert_core"}), tactic_backward_lemmas_insert); DECLARE_VM_BUILTIN(name({"tactic", "back_lemmas_find"}), tactic_backward_lemmas_find); diff --git a/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp b/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp index 946919f6a7..e445ba9a7d 100644 --- a/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp +++ b/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp @@ -146,7 +146,7 @@ void initialize_defeq_simp_lemmas() { defeq_simp_lemmas_ext::initialize(); - register_attribute(basic_attribute("defeq", "defeq simp lemma", add_defeq_simp_lemma)); + register_system_attribute(basic_attribute("defeq", "defeq simp lemma", add_defeq_simp_lemma)); } void finalize_defeq_simp_lemmas() { diff --git a/src/library/tactic/simplifier/simp_lemmas.cpp b/src/library/tactic/simplifier/simp_lemmas.cpp index d2f20f63be..cbc88836ce 100644 --- a/src/library/tactic/simplifier/simp_lemmas.cpp +++ b/src/library/tactic/simplifier/simp_lemmas.cpp @@ -671,8 +671,8 @@ void initialize_simp_lemmas() { DECLARE_VM_BUILTIN(name({"tactic", "mk_empy_simp_lemmas"}), tactic_mk_empty_simp_lemmas); DECLARE_VM_BUILTIN(name({"tactic", "simp_lemmas_insert_core"}), tactic_simp_lemmas_insert); - register_attribute(basic_attribute("simp", "simplification lemma", on_add_simp_lemma)); - register_attribute(basic_attribute("congr", "congruence lemma", on_add_congr_lemma)); + register_system_attribute(basic_attribute("simp", "simplification lemma", on_add_simp_lemma)); + register_system_attribute(basic_attribute("congr", "congruence lemma", on_add_congr_lemma)); } void finalize_simp_lemmas() { diff --git a/src/library/unification_hint.cpp b/src/library/unification_hint.cpp index 0e47270430..22c938a53b 100644 --- a/src/library/unification_hint.cpp +++ b/src/library/unification_hint.cpp @@ -204,7 +204,7 @@ void initialize_unification_hint() { unification_hint_ext::initialize(); - register_attribute(basic_attribute("unify", "unification hint", add_unification_hint)); + register_system_attribute(basic_attribute("unify", "unification hint", add_unification_hint)); } void finalize_unification_hint() { diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index a3e7988d27..ff16a26ac7 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -344,11 +344,14 @@ has_recursors_pred::has_recursors_pred(environment const & env): void initialize_user_recursors() { g_key = new std::string("UREC"); recursor_ext::initialize(); - register_attribute(indices_attribute("recursor", "user defined recursor", [](environment const & env, io_state const &, name const & n, unsigned, indices_attribute_data const & data, bool persistent) { - if (data.m_idxs && tail(data.m_idxs)) - throw exception(sstream() << "invalid [recursor] declaration, expected at most one parameter"); - return add_user_recursor(env, n, head_opt(data.m_idxs), persistent); - })); + register_system_attribute(indices_attribute("recursor", "user defined recursor", + [](environment const & env, io_state const &, name const & n, unsigned, + indices_attribute_data const & data, bool persistent) { + if (data.m_idxs && tail(data.m_idxs)) + throw exception(sstream() + << "invalid [recursor] declaration, expected at most one parameter"); + return add_user_recursor(env, n, head_opt(data.m_idxs), persistent); + })); } void finalize_user_recursors() { diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt index 7118ca8b92..19216e66b5 100644 --- a/src/library/vm/CMakeLists.txt +++ b/src/library/vm/CMakeLists.txt @@ -1,3 +1,3 @@ add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp vm_options.cpp vm_format.cpp vm_rb_map.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp - vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp init_module.cpp) \ No newline at end of file + vm_declaration.cpp vm_environment.cpp vm_list.cpp vm_pexpr.cpp user_attribute.cpp init_module.cpp) diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp index 0bfeb71523..6c49ecd7e5 100644 --- a/src/library/vm/init_module.cpp +++ b/src/library/vm/init_module.cpp @@ -19,6 +19,7 @@ Author: Leonardo de Moura #include "library/vm/vm_exceptional.h" #include "library/vm/vm_declaration.h" #include "library/vm/vm_environment.h" +#include "library/vm/user_attribute.h" namespace lean { void initialize_vm_core_module() { @@ -37,8 +38,10 @@ void initialize_vm_core_module() { initialize_vm_exceptional(); initialize_vm_declaration(); initialize_vm_environment(); + initialize_user_attribute(); } void finalize_vm_core_module() { + finalize_user_attribute(); finalize_vm_environment(); finalize_vm_declaration(); finalize_vm_exceptional(); diff --git a/src/library/vm/user_attribute.cpp b/src/library/vm/user_attribute.cpp new file mode 100644 index 0000000000..b9b94cb646 --- /dev/null +++ b/src/library/vm/user_attribute.cpp @@ -0,0 +1,105 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Sebastian Ullrich +*/ +#include +#include "library/attribute_manager.h" +#include "library/constants.h" +#include "library/scoped_ext.h" +#include "library/vm/vm_environment.h" +#include "library/vm/vm_list.h" +#include "library/vm/vm_name.h" +#include "library/vm/vm_string.h" +#include "util/sstream.h" + +namespace lean { + +static std::string * g_key = nullptr; + +struct user_attr_data : public attr_data { + // to be filled + + void write(serializer &) const { + lean_unreachable(); + } + void read(deserializer &) { + lean_unreachable(); + } +}; + +class user_attribute : public typed_attribute { +public: + user_attribute(name const & id, char const * descr) : typed_attribute(id, descr) {} +}; + +typedef name_map user_attribute_state; + +struct user_attribute_config { + typedef name entry; + typedef user_attribute_state state; + + static void add_entry(environment const & env, io_state const &, state & s, entry const & e) { + if (is_attribute(env, e)) + throw exception(sstream() << "an attribute named [" << e << "] has already been registered"); + auto const & ty = env.get(e).get_type(); + if (!is_constant(ty, get_user_attribute_name())) + throw exception("malformed [user_attribute] application, definition must be an instance of user_attribute"); + + vm_state vm(env); + vm_decl const & vm_decl = *vm.get_decl(e); + vm_obj const & o = vm.invoke(e, {}); + std::string descr = to_string(o); + s.insert(e, attribute_ptr(new user_attribute(e, descr.c_str()))); + } + + static std::string const & get_serialization_key() { + return *g_key; + } + static void write_entry(serializer & s, entry const & e) { + s << e; + } + static entry read_entry(deserializer & d) { + name e; + d >> e; + return e; + } + static optional get_fingerprint(entry const & e) { + return some(e.hash()); + } +}; + +typedef scoped_ext scope_ext; + +class actual_user_attribute_ext : public user_attribute_ext { +public: + virtual name_map get_attributes(environment const & env) override { + return scope_ext::get_state(env); + } +}; + +static vm_obj attribute_get_instances(vm_obj const & vm_env, vm_obj const & vm_n) { + auto const & env = to_env(vm_env); + buffer b; + get_attribute(env, to_name(vm_n)).get_instances(env, b); + return to_obj(b); +} + +void initialize_user_attribute() { + DECLARE_VM_BUILTIN(name({"attribute", "get_instances"}), attribute_get_instances); + + g_key = new std::string("USR_ATTR"); + scope_ext::initialize(); + register_system_attribute(basic_attribute("user_attribute", "declare user-defined attribute", + [](environment const & env, io_state const & ios, name const & d, unsigned, + bool persistent) { + return scope_ext::add_entry(env, ios, d, persistent); + })); + set_user_attribute_ext(std::unique_ptr(new actual_user_attribute_ext)); +} +void finalize_user_attribute() { + scope_ext::finalize(); + delete g_key; +} +} diff --git a/src/library/vm/user_attribute.h b/src/library/vm/user_attribute.h new file mode 100644 index 0000000000..cd68215d26 --- /dev/null +++ b/src/library/vm/user_attribute.h @@ -0,0 +1,12 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Sebastian Ullrich +*/ +#pragma once + +namespace lean { +void initialize_user_attribute(); +void finalize_user_attribute(); +} diff --git a/tests/lean/user_attribute.lean b/tests/lean/user_attribute.lean new file mode 100644 index 0000000000..3ea9cc631e --- /dev/null +++ b/tests/lean/user_attribute.lean @@ -0,0 +1,38 @@ +attribute [user_attribute] +definition foo := ⦃user_attribute, descr := "bar"⦄ + +print attributes + +attribute [foo] eq.refl + +print [foo] +print eq.refl + + +-- compound names +attribute [user_attribute] +definition foo.baz := ⦃user_attribute, descr := "bar"⦄ + +print attributes + +attribute [foo.baz] eq.refl + +print [foo.baz] +print eq.refl + + +-- can't redeclare attributes +attribute [user_attribute] +definition reducible := ⦃user_attribute, descr := "bar"⦄ + + +-- wrong type +attribute [user_attribute] +definition bar := "bar" + +section + variable x : string + + attribute [user_attribute] + definition bar := ⦃user_attribute, descr := x⦄ +end diff --git a/tests/lean/user_attribute.lean.expected.out b/tests/lean/user_attribute.lean.expected.out new file mode 100644 index 0000000000..76df1eb471 --- /dev/null +++ b/tests/lean/user_attribute.lean.expected.out @@ -0,0 +1,64 @@ +[class] type class +[congr] congruence lemma +[constructor] instructs normalizer (and simplifier) that function application (f ...) should be unfolded when it is the major premise of a constructor like operator +[defeq] defeq simp lemma +[elim] elimination rule that is eagerly applied by blast grinder +[foo] bar +[forward] forward chaining +[inline] mark definition to always be inlined +[instance] type class instance +[intro] introduction rule for backward chaining +[irreducible] irreducible +[no_pattern] do not consider terms containing this declaration in the pattern inference procedure +[parsing_only] parsing-only abbreviation +[pattern] mark that a definition can be used in a pattern(remark: the dependent pattern matching compiler will unfold the definition) +[recursor] user defined recursor +[reducibility] internal attribute for storing reducibility +[reducible] reducible +[refl] reflexive relation +[semireducible] semireducible +[simp] simplification lemma +[subst] substitution +[symm] symmetric relation +[trans] transitive relation +[unfold] unfold definition when the given positions are constructors +[unfold_full] instructs normalizer (and simplifier) that function application (f a_1 ... a_n) should be unfolded when it is fully applied +[unify] unification hint +[user_attribute] declare user-defined attribute +eq.refl +attribute [foo, refl] +constructor eq.refl : ∀ {A : Type} (a : A), a = a +[class] type class +[congr] congruence lemma +[constructor] instructs normalizer (and simplifier) that function application (f ...) should be unfolded when it is the major premise of a constructor like operator +[defeq] defeq simp lemma +[elim] elimination rule that is eagerly applied by blast grinder +[foo] bar +[foo.baz] bar +[forward] forward chaining +[inline] mark definition to always be inlined +[instance] type class instance +[intro] introduction rule for backward chaining +[irreducible] irreducible +[no_pattern] do not consider terms containing this declaration in the pattern inference procedure +[parsing_only] parsing-only abbreviation +[pattern] mark that a definition can be used in a pattern(remark: the dependent pattern matching compiler will unfold the definition) +[recursor] user defined recursor +[reducibility] internal attribute for storing reducibility +[reducible] reducible +[refl] reflexive relation +[semireducible] semireducible +[simp] simplification lemma +[subst] substitution +[symm] symmetric relation +[trans] transitive relation +[unfold] unfold definition when the given positions are constructors +[unfold_full] instructs normalizer (and simplifier) that function application (f a_1 ... a_n) should be unfolded when it is fully applied +[unify] unification hint +[user_attribute] declare user-defined attribute +eq.refl +attribute [foo, foo.baz, refl] +constructor eq.refl : ∀ {A : Type} (a : A), a = a +user_attribute.lean:25:0: error: an attribute named [reducible] has already been registered +user_attribute.lean:30:0: error: malformed [user_attribute] application, definition must be an instance of user_attribute +user_attribute.lean:36:2: error: malformed [user_attribute] application, definition must be an instance of user_attribute