michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): remove unnecessary flag

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-17 17:23:20 -07:00
parent ce8f2a1674
commit 2109dff46a
3 changed files with 6 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -20,9 +20,8 @@ Author: Leonardo de Moura
#include "frontends/lean/util.h"
namespace lean {
decl_attributes::decl_attributes(bool def_only, bool is_abbrev, bool persistent):
decl_attributes::decl_attributes(bool is_abbrev, bool persistent):
m_priority() {
m_def_only = def_only;
m_is_abbrev = is_abbrev;
m_persistent = persistent;
m_is_instance = false;
@ -117,8 +116,6 @@ void decl_attributes::parse(buffer<name> const & ns, parser & p) {
m_is_class = true;
p.next();
} else if (p.curr_is_token(get_multiple_instances_tk())) {
if (m_def_only)
throw parser_error("invalid '[multiple-instances]' attribute, only classes can have this attribute", pos);
m_has_multiple_instances = true;
p.next();
} else if (auto it = parse_instance_priority(p)) {
@ -246,7 +243,7 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c
}
void decl_attributes::write(serializer & s) const {
s << m_def_only << m_is_abbrev << m_persistent << m_is_instance << m_is_coercion
s << m_is_abbrev << m_persistent << m_is_instance << m_is_coercion
<< m_is_reducible << m_is_irreducible << m_is_semireducible << m_is_quasireducible
<< m_is_class << m_is_parsing_only << m_has_multiple_instances << m_unfold_f_hint
<< m_constructor_hint << m_symm << m_trans << m_refl << m_subst << m_recursor
@ -254,7 +251,7 @@ void decl_attributes::write(serializer & s) const {
}
void decl_attributes::read(deserializer & d) {
d >> m_def_only >> m_is_abbrev >> m_persistent >> m_is_instance >> m_is_coercion
d >> m_is_abbrev >> m_persistent >> m_is_instance >> m_is_coercion
>> m_is_reducible >> m_is_irreducible >> m_is_semireducible >> m_is_quasireducible
>> m_is_class >> m_is_parsing_only >> m_has_multiple_instances >> m_unfold_f_hint
>> m_constructor_hint >> m_symm >> m_trans >> m_refl >> m_subst >> m_recursor

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

@ -10,7 +10,6 @@ Author: Leonardo de Moura
namespace lean {
class parser;
class decl_attributes {
bool m_def_only; // if true only definition attributes are allowed
bool m_is_abbrev; // if true only abbreviation attributes are allowed
bool m_persistent;
bool m_is_instance;
@ -38,7 +37,7 @@ class decl_attributes {
void parse(name const & n, parser & p);
public:
decl_attributes(bool def_only = true, bool is_abbrev = false, bool persistent = true);
decl_attributes(bool is_abbrev = false, bool persistent = true);
void parse(buffer<name> const & ns, parser & p);
void parse(parser & p);
environment apply(environment env, io_state const & ios, name const & d) const;

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

@ -1056,7 +1056,7 @@ public:
definition_cmd_fn(parser & p, def_cmd_kind kind, bool is_private, bool is_protected):
m_p(p), m_env(m_p.env()), m_kind(kind),
m_is_private(is_private), m_is_protected(is_protected),
m_pos(p.pos()), m_attributes(true, kind == Abbreviation || kind == LocalAbbreviation) {
m_pos(p.pos()), m_attributes(kind == Abbreviation || kind == LocalAbbreviation) {
lean_assert(!(m_is_private && m_is_protected));
}
@ -1183,9 +1183,8 @@ static environment attribute_cmd_core(parser & p, bool persistent) {
while (p.curr_is_identifier()) {
ds.push_back(p.check_constant_next("invalid 'attribute' command, constant expected"));
}
bool decl_only = false;
bool abbrev = false;
decl_attributes attributes(decl_only, abbrev, persistent);
decl_attributes attributes(abbrev, persistent);
attributes.parse(ds, p);
environment env = p.env();
for (name const & d : ds)