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

chore(frontends/lean): remove parsing_only and prio from old attribute parser

Browse source 
This is a preparation for adding new attribute manager to the old frontend.
This commit is contained in:
Leonardo de Moura 2019-06-05 15:01:03 -07:00
parent e90a79f996
commit 95b3ad69f9
4 changed files with 28 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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);
}
}

6
src/frontends/lean/decl_attributes.h
View file

@ -21,12 +21,10 @@ public:
};
private:
bool m_persistent;
bool m_parsing_only;
list<entry> m_entries;
optional<unsigned> 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<entry> const & get_entries() const { return m_entries; }
bool is_parsing_only() const { return m_parsing_only; }
optional<unsigned > get_priority() const { return m_prio; }
void set_persistent(bool persistent) { m_persistent = persistent; }
bool ok_for_inductive_type() const;
bool has_class() const;

2
src/frontends/lean/decl_cmds.cpp
View file

@ -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);

2
src/frontends/lean/notation_cmd.cpp
View file

@ -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();
}
};