diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index 00fe33a279..489829650c 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -21,8 +21,13 @@ void decl_attributes::parse(parser & p) { p.next(); while (true) { auto pos = p.pos(); + bool deleted = p.curr_is_token_or_id(get_sub_tk()); + if (deleted) + p.next(); auto name = p.check_id_next("invalid attribute declaration, identifier expected"); if (name == "priority") { + if (deleted) + throw parser_error("cannot remove priority attribute", pos); auto pos = p.pos(); expr pre_val = p.parse_expr(); pre_val = mk_typed_expr(mk_constant(get_num_name()), pre_val); @@ -40,14 +45,17 @@ void decl_attributes::parse(parser & p) { throw parser_error(sstream() << "unknown attribute [" << name << "]", pos); 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 - << "], declaration was already marked with [" << entry.m_attr->get_name() - << "]", pos); + if (!deleted) { + for (auto const & entry : m_entries) { + if (!entry.deleted() && are_incompatible(*entry.m_attr, attr)) { + throw parser_error(sstream() << "invalid attribute [" << name + << "], declaration was already marked with [" + << entry.m_attr->get_name() + << "]", pos); + } } } - auto data = attr.parse_data(p); + auto data = deleted ? attr_data_ptr() : attr.parse_data(p); m_entries = cons({&attr, data}, m_entries); if (name == "parsing_only") m_parsing_only = true; @@ -71,22 +79,29 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c while (i > 0) { --i; auto const & entry = entries[i]; - unsigned prio = m_prio ? *m_prio : LEAN_DEFAULT_PRIORITY; - env = entry.m_attr->set_untyped(env, ios, d, prio, entry.m_params, m_persistent); + if (entry.deleted()) { + if (!entry.m_attr->is_instance(env, d)) + throw exception(sstream() << "cannot remove attribute [" << entry.m_attr->get_name() + << "]: no prior declaration on " << d); + env = entry.m_attr->unset(env, ios, d, m_persistent); + } else { + unsigned prio = m_prio ? *m_prio : LEAN_DEFAULT_PRIORITY; + env = entry.m_attr->set_untyped(env, ios, d, prio, entry.m_params, m_persistent); + } } return env; } bool decl_attributes::ok_for_inductive_type() const { for (entry const & e : m_entries) - if (e.m_attr->get_name() != "class") + if (e.m_attr->get_name() != "class" || e.deleted()) return false; return true; } bool decl_attributes::has_class() const { for (entry const & e : m_entries) - if (e.m_attr->get_name() == "class") + if (e.m_attr->get_name() == "class" && !e.deleted()) return true; return false; } diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h index 065a3801f9..70554c0a6b 100644 --- a/src/frontends/lean/decl_attributes.h +++ b/src/frontends/lean/decl_attributes.h @@ -16,6 +16,10 @@ public: struct entry { attribute const * m_attr; attr_data_ptr m_params; + + bool deleted() const { + return !static_cast(m_params); + } }; private: bool m_persistent; diff --git a/src/library/attribute_manager.cpp b/src/library/attribute_manager.cpp index 1191d529c2..c022d701eb 100644 --- a/src/library/attribute_manager.cpp +++ b/src/library/attribute_manager.cpp @@ -60,7 +60,7 @@ attribute const & get_attribute(environment const & env, name const & attr) { struct attr_record { name m_decl; - attr_data_ptr m_data; + attr_data_ptr m_data; // no data -> deleted attr_record() {} attr_record(name decl, attr_data_ptr data): @@ -72,6 +72,10 @@ struct attr_record { h = ::lean::hash(h, m_data->hash()); return h; } + + bool deleted() const { + return !static_cast(m_data); + } }; struct attr_record_cmp { @@ -119,23 +123,26 @@ 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); - 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); + s << e.m_attr << e.m_prio << e.m_record.m_decl << e.m_record.deleted(); + if (!e.m_record.deleted()) { + 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; - 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); + entry e; bool deleted; + d >> e.m_attr >> e.m_prio >> e.m_record.m_decl >> deleted; + if (!deleted) { + 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; } @@ -154,6 +161,17 @@ environment attribute::set_core(environment const & env, io_state const & ios, n env2 = m_after_set(env2, ios, n, prio, persistent); return env2; } + +environment attribute::unset(environment env, io_state const & ios, name const & n, bool persistent) const { + if (m_before_unset) { + env = m_before_unset(env, n, persistent); + } else { + if (m_after_set) + throw exception(sstream() << "cannot remove attribute [" << get_name() << "]"); + } + return attribute_ext::add_entry(env, ios, attr_entry(m_id, get_prio(env, n), attr_record(n, {})), persistent); +} + attr_data_ptr attribute::get_untyped(environment const & env, name const & n) const { if (auto p = attribute_ext::get_state(env).find(m_id)) { attr_records const & records = p->first; diff --git a/src/library/attribute_manager.h b/src/library/attribute_manager.h index 99f266408e..d1b132b55e 100644 --- a/src/library/attribute_manager.h +++ b/src/library/attribute_manager.h @@ -30,14 +30,16 @@ typedef std::shared_ptr attr_data_ptr; struct attr_config; typedef std::function after_set_proc; +typedef std::function before_unset_proc; class attribute { friend struct attr_config; friend class decl_attributes; private: - name m_id; - std::string m_descr; - after_set_proc m_after_set; + name m_id; + std::string m_descr; + after_set_proc m_after_set; + before_unset_proc m_before_unset; protected: environment set_core(environment const &, io_state const &, name const &, unsigned, attr_data_ptr, bool) const; @@ -45,8 +47,8 @@ protected: virtual void write_entry(serializer &, attr_data const &) const = 0; virtual attr_data_ptr read_entry(deserializer &) const = 0; public: - attribute(name const & id, char const * descr, after_set_proc after_set = {}) : m_id(id), m_descr(descr), - m_after_set(after_set) {} + attribute(name const & id, char const * descr, after_set_proc after_set = {}, before_unset_proc before_unset = {}) : + m_id(id), m_descr(descr), m_after_set(after_set), m_before_unset(before_unset) {} virtual ~attribute() {} name const & get_name() const { return m_id; } @@ -61,6 +63,7 @@ public: priority_queue get_instances_by_prio(environment const &) const; virtual attr_data_ptr parse_data(abstract_parser &) const; + virtual environment unset(environment env, io_state const & ios, name const & n, bool persistent) const; virtual unsigned get_fingerprint(environment const & env) const; }; @@ -76,8 +79,8 @@ protected: return set(env, ios, n, prio, persistent); } public: - basic_attribute(name const & id, char const * descr, after_set_proc after_set = {}) : - attribute(id, descr, after_set) {} + basic_attribute(name const & id, char const * descr, after_set_proc after_set = {}, before_unset_proc before_unset = {}) : + attribute(id, descr, after_set, before_unset) {} virtual environment set(environment const & env, io_state const & ios, name const & n, unsigned prio, bool persistent) const { return set_core(env, ios, n, prio, attr_data_ptr(new attr_data), persistent); } @@ -102,8 +105,8 @@ protected: return attr_data_ptr(data); } public: - typed_attribute(name const & id, char const * descr, after_set_proc after_set = {}) : - attribute(id, descr, after_set) {} + typed_attribute(name const & id, char const * descr, after_set_proc after_set = {}, before_unset_proc before_unset = {}) : + attribute(id, descr, after_set, before_unset) {} virtual attr_data_ptr parse_data(abstract_parser & p) const final override { auto data = new Data; diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp index 27ad06b041..ab8f2ebd46 100644 --- a/src/library/reducible.cpp +++ b/src/library/reducible.cpp @@ -60,6 +60,9 @@ public: throw exception(sstream() << "invalid reducible command, '" << n << "' is not a definition"); return get_reducibility_attribute().set(env, ios, n, prio, {m_status}, persistent); } + virtual environment unset(environment, io_state const &, name const &, bool) const override { + throw exception(sstream() << "cannot remove attribute [" << get_name() << "]"); + } virtual void get_instances(environment const & env, buffer & r) const override { buffer tmp; diff --git a/tests/lean/attributes.lean b/tests/lean/attributes.lean new file mode 100644 index 0000000000..8e04c13d74 --- /dev/null +++ b/tests/lean/attributes.lean @@ -0,0 +1,29 @@ +definition foo (A : Type) := A + +attribute [-unfold] foo + +attribute [unfold 1] foo + +section + local attribute [-unfold] foo + print foo +end +print foo + +attribute [-unfold] foo +print foo + +attribute [-unfold] foo + +attribute [unfold] foo +print foo + +-- + +attribute [reducible] foo +attribute [-reducible] foo -- use [semireducible] instead +print foo + +-- + +attribute [-instance] nat_has_one diff --git a/tests/lean/attributes.lean.expected.out b/tests/lean/attributes.lean.expected.out new file mode 100644 index 0000000000..26a6247eed --- /dev/null +++ b/tests/lean/attributes.lean.expected.out @@ -0,0 +1,17 @@ +attributes.lean:3:0: error: cannot remove attribute [unfold]: no prior declaration on foo +definition foo : Type → Type := +λ A, A +attribute [unfold 1] +definition foo : Type → Type := +λ A, A +definition foo : Type → Type := +λ A, A +attributes.lean:16:0: error: cannot remove attribute [unfold]: no prior declaration on foo +attribute [unfold] +definition foo : Type → Type := +λ A, A +attributes.lean:24:0: error: cannot remove attribute [reducible] +attribute [reducible, unfold] +definition foo : Type → Type := +λ A, A +attributes.lean:29:0: error: cannot remove attribute [instance]