From 95b3ad69f990e083ddb2cd7fc16d63d07e6232b1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Jun 2019 15:01:03 -0700 Subject: [PATCH] chore(frontends/lean): remove `parsing_only` and `prio` from old attribute parser This is a preparation for adding new attribute manager to the old frontend. --- src/frontends/lean/decl_attributes.cpp | 62 +++++++++++--------------- src/frontends/lean/decl_attributes.h | 6 +-- src/frontends/lean/decl_cmds.cpp | 2 - src/frontends/lean/notation_cmd.cpp | 2 - 4 files changed, 28 insertions(+), 44 deletions(-) diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index eeea79891a..4891c5ae29 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -43,48 +43,40 @@ void decl_attributes::parse_core(parser & p, bool compact) { } else { id = p.check_id_next("invalid attribute declaration, identifier expected"); } - if (id == "priority") { - if (deleted) - throw parser_error("cannot remove priority attribute", pos); - throw parser_error("'priority' has been temporarily disabled", pos); - } else { - if (!is_attribute(p.env(), id)) - throw parser_error(sstream() << "unknown attribute [" << id << "]", pos); + if (!is_attribute(p.env(), id)) + throw parser_error(sstream() << "unknown attribute [" << id << "]", pos); - auto const & attr = ::lean::get_attribute(p.env(), id); - if (!deleted) { - for (auto const & entry : m_entries) { - if (!entry.deleted() && are_incompatible(*entry.m_attr, attr)) { - throw parser_error(sstream() << "invalid attribute [" << id - << "], declaration was already marked with [" - << entry.m_attr->get_name() - << "]", pos); - } + auto const & attr = ::lean::get_attribute(p.env(), id); + if (!deleted) { + for (auto const & entry : m_entries) { + if (!entry.deleted() && are_incompatible(*entry.m_attr, attr)) { + throw parser_error(sstream() << "invalid attribute [" << id + << "], declaration was already marked with [" + << entry.m_attr->get_name() + << "]", pos); } } - attr_data_ptr data; - if (!deleted) { - // not all identifiers in attributes are actual Lean declarations - parser::undef_id_to_local_scope scope(p); - expr e = mk_const(id); - while (!p.curr_is_token("]") && !p.curr_is_token(",")) { - expr arg = p.parse_expr(get_max_prec()); - if (has_sorry(arg)) - break; - e = mk_app(e, arg); - } - // the new frontend uses consts instead of locals for unknown names... - e = replace(e, [](expr const & e) { + } + attr_data_ptr data; + if (!deleted) { + // not all identifiers in attributes are actual Lean declarations + parser::undef_id_to_local_scope scope(p); + expr e = mk_const(id); + while (!p.curr_is_token("]") && !p.curr_is_token(",")) { + expr arg = p.parse_expr(get_max_prec()); + if (has_sorry(arg)) + break; + e = mk_app(e, arg); + } + // the new frontend uses consts instead of locals for unknown names... + e = replace(e, [](expr const & e) { if (is_local(e)) return some_expr(mk_const(local_name(e))); return none_expr(); }); - data = attr.parse_data(e); - } - m_entries = cons({&attr, data}, m_entries); - if (id == "parsing_only") - m_parsing_only = true; + data = attr.parse_data(e); } + m_entries = cons({&attr, data}, m_entries); if (p.curr_is_token(get_comma_tk())) { p.next(); } else { @@ -142,7 +134,7 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c << "]: no prior declaration on " << d); env = entry.m_attr->unset(env, ios, d, m_persistent); } else { - unsigned prio = m_prio ? *m_prio : get_default_priority(ios.get_options()); + unsigned prio = get_default_priority(ios.get_options()); env = entry.m_attr->set_untyped(env, ios, d, prio, entry.m_params, m_persistent); } } diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h index cebb2e7199..f8bfdbc0ba 100644 --- a/src/frontends/lean/decl_attributes.h +++ b/src/frontends/lean/decl_attributes.h @@ -21,12 +21,10 @@ public: }; private: bool m_persistent; - bool m_parsing_only; list m_entries; - optional m_prio; void parse_core(parser & p, bool compact); public: - decl_attributes(bool persistent = true): m_persistent(persistent), m_parsing_only(false) {} + decl_attributes(bool persistent = true): m_persistent(persistent) {} void set_attribute(environment const & env, name const & attr_name, attr_data_ptr data = get_default_attr_data()); attr_data_ptr get_attribute(environment const & env, name const & attr_name) const; /* attributes: zero-or-more [ ... ] */ @@ -35,8 +33,6 @@ public: void parse_compact(parser & p); environment apply(environment env, io_state const & ios, name const & d) const; list const & get_entries() const { return m_entries; } - bool is_parsing_only() const { return m_parsing_only; } - optional get_priority() const { return m_prio; } void set_persistent(bool persistent) { m_persistent = persistent; } bool ok_for_inductive_type() const; bool has_class() const; diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 45d43df43f..0e7afdfe08 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -487,8 +487,6 @@ static environment attribute_cmd_core(parser & p, bool persistent) { name d = p.check_constant_next("invalid 'attribute' command, constant expected"); ds.push_back(d); } while (p.curr_is_identifier()); - if (attributes.is_parsing_only()) - throw exception(sstream() << "invalid [parsing_only] attribute, can only be applied at declaration time"); environment env = p.env(); for (name const & d : ds) env = attributes.apply(env, p.ios(), d); diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index bc540d00ad..d2919b5df7 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -684,8 +684,6 @@ struct notation_modifiers { throw parser_error(sstream() << "invalid notation: unexpected attribute [" << entry.m_attr->get_name() << "]", pos); } - if (attrs.get_priority()) - m_priority = *attrs.get_priority(); } };