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

refactor(library/attribute_manger): simplify: make every attribute prioritizable

Browse source
This commit is contained in:
Sebastian Ullrich 2016-08-16 11:31:59 -04:00 • committed by Leonardo de Moura
parent 7669e18c77
commit 34e00cd5a2
15 changed files with 65 additions and 96 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -48,12 +48,8 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c
while (i > 0) {
--i;
auto const & entry = entries[i];
if (auto prio_attr = dynamic_cast<prio_attribute const *>(entry.m_attr)) {
unsigned prio = m_prio ? *m_prio : LEAN_DEFAULT_PRIORITY;
env = prio_attr->set(env, ios, d, prio, m_persistent);
} else {
env = entry.m_attr->set_untyped(env, ios, d, entry.m_params, m_persistent);
}
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;
}

4
src/frontends/lean/old_attributes.cpp
View file

@ -8,10 +8,10 @@ Author: Leonardo de Moura
namespace lean {
void initialize_old_attributes() {
register_attribute(prio_attribute("elim", "elimination rule that is eagerly applied by blast grinder"));
register_attribute(prio_attribute("intro!", "introduction rule that is eagerly applied by blast grinder"));
register_attribute(basic_attribute("elim", "elimination rule that is eagerly applied by blast grinder"));
register_attribute(basic_attribute("no_pattern", "do not consider terms containing this declaration in the pattern inference procedure"));
register_attribute(prio_attribute("forward", "forward chaining"));
register_attribute(basic_attribute("forward", "forward chaining"));
}
void finalize_old_attributes() {}
}

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

@ -259,7 +259,7 @@ static void print_attributes(parser const & p, name const & n) {
out << " [" << attr->get_name();
data->print(out);
out << "]";
unsigned prio = get_attribute_prio(env, attr->get_name(), n);
unsigned prio = attr->get_prio(env, n);
if (prio != LEAN_DEFAULT_PRIORITY)
out << " [priority " << prio << "]";
}

2
src/library/abbreviation.cpp
View file

@ -116,7 +116,7 @@ void initialize_abbreviation() {
g_class_name = new name("abbreviation");
g_key = new std::string("ABBREV");
abbrev_ext::initialize();
register_attribute(basic_attribute("parsing_only", "parsing-only abbreviation", [](environment const & env, io_state const &, name const & d, bool) {
register_attribute(basic_attribute("parsing_only", "parsing-only abbreviation", [](environment const & env, io_state const &, name const & d, unsigned, bool) {
if (!is_abbreviation(env, d))
throw exception(sstream() << "invalid '[parsing_only]' attribute, " << d << " is not an abbreviation");
return env;

51
src/library/attribute_manager.cpp
View file

@ -108,9 +108,9 @@ struct attr_config {
template class scoped_ext<attr_config>;
typedef scoped_ext<attr_config> attribute_ext;
environment attribute::set_core(environment const & env, io_state const & ios, name const & n, attr_data_ptr data,
bool persistent) const {
return attribute_ext::add_entry(env, ios, attr_entry(m_id, LEAN_DEFAULT_PRIORITY, attr_record(n, data)), persistent);
environment attribute::set_core(environment const & env, io_state const & ios, name const & n, unsigned prio,
attr_data_ptr data, bool persistent) const {
return attribute_ext::add_entry(env, ios, attr_entry(m_id, prio, attr_record(n, data)), persistent);
}
attr_data_ptr attribute::get(environment const & env, name const & n) const {
if (auto records = attribute_ext::get_state(env).find(m_id))
@ -119,6 +119,13 @@ attr_data_ptr attribute::get(environment const & env, name const & n) const {
return {};
}
unsigned attribute::get_prio(environment const & env, name const & n) const {
if (auto records = attribute_ext::get_state(env).find(get_name()))
if (auto prio = records->get_prio({n, {}}))
return prio.value();
return LEAN_DEFAULT_PRIORITY;
}
void attribute::get_instances(environment const & env, buffer<name> & r) const {
if (auto records = attribute_ext::get_state(env).find(m_id))
records->for_each([&](attr_record const & rec) { r.push_back(rec.m_decl); });
@ -128,17 +135,9 @@ attr_data_ptr attribute::parse_data(abstract_parser &) const {
return lean::attr_data_ptr(new attr_data);
}
environment basic_attribute::set(environment const & env, io_state const & ios, name const & n, bool persistent) const {
auto env2 = set_core(env, ios, n, attr_data_ptr(new attr_data), persistent);
if (m_on_set)
env2 = m_on_set(env2, ios, n, persistent);
return env2;
}
environment prio_attribute::set(environment const & env, io_state const & ios, name const & n, unsigned prio,
bool persistent) const {
auto env2 = attribute_ext::add_entry(env, ios, attr_entry(get_name(), prio, attr_record(n, attr_data_ptr(new attr_data))),
persistent);
environment basic_attribute::set(environment const & env, io_state const & ios, name const & n, unsigned prio,
bool persistent) const {
auto env2 = set_core(env, ios, n, prio, attr_data_ptr(new attr_data), persistent);
if (m_on_set)
env2 = m_on_set(env2, ios, n, prio, persistent);
return env2;
@ -204,29 +203,23 @@ priority_queue<name, name_quick_cmp> get_attribute_instances_by_prio(environment
environment set_attribute(environment const & env, io_state const & ios, char const * name,
lean::name const & d, unsigned prio, list<unsigned> const & params, bool persistent) {
auto const & attr = get_attribute(name);
if (auto prio_attr = dynamic_cast<prio_attribute const *>(&attr)) {
lean_assert(!params);
return prio_attr->set(env, ios, d, prio, persistent);
}
if (auto params_attr = dynamic_cast<indices_attribute const *>(&attr)) {
return params_attr->set(env, ios, d, {params}, persistent);
}
lean_assert(!params);
return set_attribute(env, ios, name, d, persistent);
lean_assert(dynamic_cast<indices_attribute const *>(&attr));
return static_cast<indices_attribute const &>(attr).set(env, ios, d, prio, {params}, persistent);
}
environment set_attribute(environment const & env, io_state const & ios, char const * name, lean::name const & d,
bool persistent) {
unsigned prio, bool persistent) {
auto const & attr = get_attribute(name);
lean_assert(dynamic_cast<basic_attribute const *>(&attr));
return static_cast<basic_attribute const &>(attr).set(env, ios, d, persistent);
return static_cast<basic_attribute const &>(attr).set(env, ios, d, prio, persistent);
}
environment set_attribute(environment const & env, io_state const & ios, char const * attr,
name const & d, bool persistent) {
return set_attribute(env, ios, attr, d, LEAN_DEFAULT_PRIORITY, persistent);
}
unsigned get_attribute_prio(environment const & env, std::string const & attr, name const & d) {
if (auto records = attribute_ext::get_state(env).find(attr))
if (auto prio = records->get_prio({d, {}}))
return prio.value();
return LEAN_DEFAULT_PRIORITY;
return get_attribute(attr).get_prio(env, d);
}
list<unsigned> get_attribute_params(environment const & env, std::string const & attr, name const & d) {

62
src/library/attribute_manager.h
View file

@ -36,9 +36,9 @@ private:
std::string m_descr;
std::string m_token;
protected:
environment set_core(environment const &, io_state const &, name const &, attr_data_ptr, bool) const;
environment set_core(environment const &, io_state const &, name const &, unsigned, attr_data_ptr, bool) const;
virtual environment set_untyped(environment const &, io_state const &, name const &, attr_data_ptr, bool) const = 0;
virtual environment set_untyped(environment const &, io_state const &, name const &, unsigned, attr_data_ptr, bool) const = 0;
virtual void write_entry(serializer &, attr_data const &) const = 0;
virtual attr_data_ptr read_entry(deserializer &) const = 0;
public:
@ -50,35 +50,15 @@ public:
std::string const & get_token() const { return m_token; }
virtual attr_data_ptr get(environment const &, name const &) const;
unsigned get_prio(environment const &, name const &) const;
virtual void get_instances(environment const &, buffer<name> &) const;
virtual attr_data_ptr parse_data(abstract_parser &) const;
};
typedef std::shared_ptr<attribute const> attribute_ptr;
/** \brief An attribute without associated data or priority declaration */
/** \brief An attribute without associated data */
class basic_attribute : public attribute {
public:
typedef std::function<environment(environment const &, io_state const &, name const &, bool)> on_set_proc;
private:
on_set_proc m_on_set;
protected:
virtual void write_entry(serializer &, attr_data const &) const override final {}
virtual attr_data_ptr read_entry(deserializer &) const override final { return attr_data_ptr(new attr_data); }
virtual environment set_untyped(environment const & env, io_state const & ios, name const & n, attr_data_ptr,
bool persistent) const override final {
return set(env, ios, n, persistent);
}
public:
basic_attribute(char const * id, char const * descr, on_set_proc on_set) : attribute(id, descr),
m_on_set(on_set) {}
basic_attribute(char const * id, char const * descr) : basic_attribute(id, descr, {}) {}
virtual environment set(environment const & env, io_state const & ios, name const & n, bool persistent) const;
};
// TODO(sullrich): Let the attribute handle priority parsing itself by introducing a custom
// syntax (something like [attr:prio]?)
class prio_attribute : public attribute {
public:
typedef std::function<environment(environment const &, io_state const &, name const &, unsigned, bool)> on_set_proc;
private:
@ -86,32 +66,29 @@ private:
protected:
virtual void write_entry(serializer &, attr_data const &) const override final {}
virtual attr_data_ptr read_entry(deserializer &) const override final { return attr_data_ptr(new attr_data); }
virtual environment set_untyped(environment const & /*env */, io_state const & /* ios */,
name const & /* n */, attr_data_ptr /* data */,
bool /* persistent */) const override final {
// TODO(sullrich): Use priority from `data` as soon as available
lean_unreachable();
virtual environment set_untyped(environment const & env, io_state const & ios, name const & n, unsigned prio, attr_data_ptr,
bool persistent) const override final {
return set(env, ios, n, prio, persistent);
}
public:
prio_attribute(char const * id, char const * descr, on_set_proc on_set) : attribute(id, descr),
m_on_set(on_set) {}
prio_attribute(char const * id, char const * descr) : prio_attribute(id, descr, {}) {}
virtual environment set(environment const & env, io_state const & ios, name const & n, unsigned prio,
bool persistent) const;
basic_attribute(char const * id, char const * descr, on_set_proc on_set) : attribute(id, descr),
m_on_set(on_set) {}
basic_attribute(char const * id, char const * descr) : basic_attribute(id, descr, {}) {}
virtual environment set(environment const & env, io_state const & ios, name const & n, unsigned, bool persistent) const;
};
template<typename Data>
class typed_attribute : public attribute {
public:
typedef std::function<environment(environment const &, io_state const &, name const &, Data const &, bool)>
typedef std::function<environment(environment const &, io_state const &, name const &, unsigned, Data const &, bool)>
on_set_proc;
private:
on_set_proc m_on_set;
protected:
virtual environment set_untyped(environment const & env, io_state const & ios, name const & n, attr_data_ptr data,
bool persistent) const override final {
virtual environment set_untyped(environment const & env, io_state const & ios, name const & n, unsigned prio,
attr_data_ptr data, bool persistent) const override final {
lean_assert(dynamic_cast<Data const *>(&*data));
return set(env, ios, n, static_cast<Data const &>(*data), persistent);
return set(env, ios, n, prio, static_cast<Data const &>(*data), persistent);
}
virtual void write_entry(serializer & s, attr_data const & data) const final override {
@ -127,10 +104,11 @@ public:
typed_attribute(char const * id, char const * descr, on_set_proc on_set) : attribute(id, descr),
m_on_set(on_set) {}
typed_attribute(char const * id, char const * descr) : typed_attribute(id, descr, {}) {}
virtual environment set(environment const & env, io_state const & ios, name const & n, Data const & data, bool persistent) const {
auto env2 = set_core(env, ios, n, std::unique_ptr<attr_data>(new Data(data)), persistent);
virtual environment set(environment const & env, io_state const & ios, name const & n, unsigned prio,
Data const & data, bool persistent) const {
auto env2 = set_core(env, ios, n, prio, std::unique_ptr<attr_data>(new Data(data)), persistent);
if (m_on_set)
env2 = m_on_set(env2, ios, n, data, persistent);
env2 = m_on_set(env2, ios, n, prio, data, persistent);
return env2;
}
std::shared_ptr<Data> get_data(environment const & env, name const & n) const {
@ -193,6 +171,8 @@ attribute const * get_attribute_from_token(char const * attr_token);
environment set_attribute(environment const & env, io_state const & ios, char const * attr,
name const & d, unsigned prio, list<unsigned> const & params, bool persistent);
environment set_attribute(environment const & env, io_state const & ios, char const * attr,
name const & d, unsigned prio, bool persistent);
environment set_attribute(environment const & env, io_state const & ios, char const * attr,
name const & d, bool persistent);

4
src/library/class.cpp
View file

@ -320,11 +320,11 @@ void initialize_class() {
g_key = new std::string("class");
class_ext::initialize();
register_attribute(basic_attribute("class", "type class", [](environment const & env, io_state const &, name const & d, bool persistent) {
register_attribute(basic_attribute("class", "type class", [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) {
return add_class(env, d, persistent);
}));
register_attribute(prio_attribute("instance", "type class instance", [](environment const & env, io_state const &, name const & d, unsigned prio, bool persistent) {
register_attribute(basic_attribute("instance", "type class instance", [](environment const & env, io_state const &, name const & d, unsigned prio, bool persistent) {
return add_instance(env, d, prio, persistent);
}));
}

2
src/library/compiler/inliner.cpp
View file

@ -21,7 +21,7 @@ bool is_inline(environment const & env, name const & n) {
}
void initialize_inliner() {
register_attribute(basic_attribute("inline", "mark definition to always be inlined", [](environment const & env, io_state const &, name const & d, bool) {
register_attribute(basic_attribute("inline", "mark definition to always be inlined", [](environment const & env, io_state const &, name const & d, unsigned, bool) {
auto decl = env.get(d);
if (!decl.is_definition() || decl.is_theorem())
throw exception("invalid 'inline' use, only definitions can be marked as inline");

6
src/library/reducible.cpp
View file

@ -53,11 +53,11 @@ public:
}
return {};
}
virtual environment set(environment const & env, io_state const & ios, name const & n, bool persistent) const override {
virtual environment set(environment const & env, io_state const & ios, name const & n, unsigned prio, bool persistent) const override {
declaration const & d = env.get(n);
if (!d.is_definition())
throw exception(sstream() << "invalid reducible command, '" << n << "' is not a definition");
return get_reducibility_attribute().set(env, ios, n, { m_status }, persistent);
return get_reducibility_attribute().set(env, ios, n, prio, {m_status}, persistent);
}
virtual void get_instances(environment const & env, buffer<name> & r) const override {
@ -85,7 +85,7 @@ void finalize_reducible() {
}
environment set_reducible(environment const & env, name const & n, reducible_status s, bool persistent) {
return get_reducibility_attribute().set(env, get_dummy_ios(), n, { s }, persistent);
return get_reducibility_attribute().set(env, get_dummy_ios(), n, LEAN_DEFAULT_PRIORITY, {s}, persistent);
}
reducible_status get_reducible_status(environment const & env, name const & n) {

8
src/library/relation_manager.cpp
View file

@ -325,19 +325,19 @@ is_relation_pred mk_is_relation_pred(environment const & env) {
void initialize_relation_manager() {
g_key = new std::string("REL");
rel_ext::initialize();
register_attribute(basic_attribute("refl", "reflexive relation", [](environment const & env, io_state const &, name const & d, bool persistent) {
register_attribute(basic_attribute("refl", "reflexive relation", [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) {
return add_refl(env, d, persistent);
}));
register_attribute(basic_attribute("symm", "symmetric relation", [](environment const & env, io_state const &, name const & d, bool persistent) {
register_attribute(basic_attribute("symm", "symmetric relation", [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) {
return add_symm(env, d, persistent);
}));
register_attribute(basic_attribute("trans", "transitive relation", [](environment const & env, io_state const &, name const & d, bool persistent) {
register_attribute(basic_attribute("trans", "transitive relation", [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) {
return add_trans(env, d, persistent);
}));
register_attribute(basic_attribute("subst", "substitution", [](environment const & env, io_state const &, name const & d, bool persistent) {
register_attribute(basic_attribute("subst", "substitution", [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) {
return add_subst(env, d, persistent);
}));
}

2
src/library/tactic/backward/backward_lemmas.cpp
View file

@ -132,7 +132,7 @@ vm_obj tactic_backward_lemmas_find(vm_obj const & lemmas, vm_obj const & h, vm_o
void initialize_backward_lemmas() {
register_trace_class(name{"tactic", "back_chaining"});
register_attribute(prio_attribute("intro", "introduction rule for backward chaining", [](environment const & env, io_state const & ios, name const & c, unsigned, bool) {
register_attribute(basic_attribute("intro", "introduction rule for backward chaining", [](environment const & env, io_state const & ios, name const & c, unsigned, bool) {
aux_type_context ctx(env, ios.get_options());
auto index = get_backward_target(ctx, c);
if (!index || index->kind() != expr_kind::Constant)

2
src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp
View file

@ -146,7 +146,7 @@ void initialize_defeq_simp_lemmas() {
defeq_simp_lemmas_ext::initialize();
register_attribute(prio_attribute("defeq", "defeq simp lemma", add_defeq_simp_lemma));
register_attribute(basic_attribute("defeq", "defeq simp lemma", add_defeq_simp_lemma));
}
void finalize_defeq_simp_lemmas() {

4
src/library/tactic/simplifier/simp_lemmas.cpp
View file

@ -671,8 +671,8 @@ void initialize_simp_lemmas() {
DECLARE_VM_BUILTIN(name({"tactic", "mk_empy_simp_lemmas"}), tactic_mk_empty_simp_lemmas);
DECLARE_VM_BUILTIN(name({"tactic", "simp_lemmas_insert_core"}), tactic_simp_lemmas_insert);
register_attribute(prio_attribute("simp", "simplification lemma", on_add_simp_lemma));
register_attribute(prio_attribute("congr", "congruence lemma", on_add_congr_lemma));
register_attribute(basic_attribute("simp", "simplification lemma", on_add_simp_lemma));
register_attribute(basic_attribute("congr", "congruence lemma", on_add_congr_lemma));
}
void finalize_simp_lemmas() {

2
src/library/unification_hint.cpp
View file

@ -204,7 +204,7 @@ void initialize_unification_hint() {
unification_hint_ext::initialize();
register_attribute(prio_attribute("unify", "unification hint", add_unification_hint));
register_attribute(basic_attribute("unify", "unification hint", add_unification_hint));
}
void finalize_unification_hint() {

2
src/library/user_recursors.cpp
View file

@ -344,7 +344,7 @@ has_recursors_pred::has_recursors_pred(environment const & env):
void initialize_user_recursors() {
g_key = new std::string("UREC");
recursor_ext::initialize();
register_attribute(indices_attribute("recursor", "user defined recursor", [](environment const & env, io_state const &, name const & n, indices_attribute_data const & data, bool persistent) {
register_attribute(indices_attribute("recursor", "user defined recursor", [](environment const & env, io_state const &, name const & n, unsigned, indices_attribute_data const & data, bool persistent) {
if (data.m_idxs && tail(data.m_idxs))
throw exception(sstream() << "invalid [recursor] declaration, expected at most one parameter");
return add_user_recursor(env, n, head_opt(data.m_idxs), persistent);