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

feat(frontends/lean/decl_attributes, library/attribute_manager): implement attribute removal

Browse source
This commit is contained in:
Sebastian Ullrich 2016-08-23 16:14:49 -04:00 • committed by Leonardo de Moura
parent a4f338889d
commit abd040589f
7 changed files with 123 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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

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

@ -16,6 +16,10 @@ public:
struct entry {
attribute const * m_attr;
attr_data_ptr m_params;
bool deleted() const {
return !static_cast<bool>(m_params);
}
};
private:
bool m_persistent;

48
src/library/attribute_manager.cpp
View file

@ -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<bool>(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;

21
src/library/attribute_manager.h
View file

@ -30,14 +30,16 @@ typedef std::shared_ptr<attr_data> attr_data_ptr;
struct attr_config;
typedef std::function<environment(environment const &, io_state const &, name const &, unsigned, bool)> after_set_proc;
typedef std::function<environment(environment const &, name const &, bool)> 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<name, name_quick_cmp> 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;

3
src/library/reducible.cpp
View file

@ -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<name> & r) const override {
buffer<name> tmp;

29
tests/lean/attributes.lean Normal file
View file

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

17
tests/lean/attributes.lean.expected.out Normal file
View file

@ -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]