From 34e00cd5a2435fca70a6b44eacddf243be52427e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 16 Aug 2016 11:31:59 -0400 Subject: [PATCH] refactor(library/attribute_manger): simplify: make every attribute prioritizable --- src/frontends/lean/decl_attributes.cpp | 8 +-- src/frontends/lean/old_attributes.cpp | 4 +- src/frontends/lean/print_cmd.cpp | 2 +- src/library/abbreviation.cpp | 2 +- src/library/attribute_manager.cpp | 51 +++++++-------- src/library/attribute_manager.h | 62 +++++++------------ src/library/class.cpp | 4 +- src/library/compiler/inliner.cpp | 2 +- src/library/reducible.cpp | 6 +- src/library/relation_manager.cpp | 8 +-- .../tactic/backward/backward_lemmas.cpp | 2 +- .../defeq_simplifier/defeq_simp_lemmas.cpp | 2 +- src/library/tactic/simplifier/simp_lemmas.cpp | 4 +- src/library/unification_hint.cpp | 2 +- src/library/user_recursors.cpp | 2 +- 15 files changed, 65 insertions(+), 96 deletions(-) diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index d481fc250b..50d60cb9b2 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -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(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; } diff --git a/src/frontends/lean/old_attributes.cpp b/src/frontends/lean/old_attributes.cpp index cbbaa46936..6b92bc5a1d 100644 --- a/src/frontends/lean/old_attributes.cpp +++ b/src/frontends/lean/old_attributes.cpp @@ -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() {} } diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index b2e5c0d87c..669e1256e2 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -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 << "]"; } diff --git a/src/library/abbreviation.cpp b/src/library/abbreviation.cpp index 76553d89dd..514eb699e2 100644 --- a/src/library/abbreviation.cpp +++ b/src/library/abbreviation.cpp @@ -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; diff --git a/src/library/attribute_manager.cpp b/src/library/attribute_manager.cpp index 5b0c270fab..6118ae4c34 100644 --- a/src/library/attribute_manager.cpp +++ b/src/library/attribute_manager.cpp @@ -108,9 +108,9 @@ struct attr_config { template class scoped_ext; typedef scoped_ext 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 & 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 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 const & params, bool persistent) { auto const & attr = get_attribute(name); - if (auto prio_attr = dynamic_cast(&attr)) { - lean_assert(!params); - return prio_attr->set(env, ios, d, prio, persistent); - } - if (auto params_attr = dynamic_cast(&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(&attr)); + return static_cast(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(&attr)); - return static_cast(attr).set(env, ios, d, persistent); + return static_cast(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 get_attribute_params(environment const & env, std::string const & attr, name const & d) { diff --git a/src/library/attribute_manager.h b/src/library/attribute_manager.h index 944ebd8358..de4ddb274e 100644 --- a/src/library/attribute_manager.h +++ b/src/library/attribute_manager.h @@ -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 &) const; virtual attr_data_ptr parse_data(abstract_parser &) const; }; typedef std::shared_ptr 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 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 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 class typed_attribute : public attribute { public: - typedef std::function + typedef std::function 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)); - return set(env, ios, n, static_cast(*data), persistent); + return set(env, ios, n, prio, static_cast(*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(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(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 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 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); diff --git a/src/library/class.cpp b/src/library/class.cpp index 9db019e10f..8e289f1338 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -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); })); } diff --git a/src/library/compiler/inliner.cpp b/src/library/compiler/inliner.cpp index 076b1ea3d2..c9434ef97b 100644 --- a/src/library/compiler/inliner.cpp +++ b/src/library/compiler/inliner.cpp @@ -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"); diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp index 212638b368..ba3e8d8aab 100644 --- a/src/library/reducible.cpp +++ b/src/library/reducible.cpp @@ -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 & 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) { diff --git a/src/library/relation_manager.cpp b/src/library/relation_manager.cpp index b1311fec51..810d546138 100644 --- a/src/library/relation_manager.cpp +++ b/src/library/relation_manager.cpp @@ -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); })); } diff --git a/src/library/tactic/backward/backward_lemmas.cpp b/src/library/tactic/backward/backward_lemmas.cpp index 9d04be012b..3c2c419112 100644 --- a/src/library/tactic/backward/backward_lemmas.cpp +++ b/src/library/tactic/backward/backward_lemmas.cpp @@ -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) diff --git a/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp b/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp index 5f72f81172..946919f6a7 100644 --- a/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp +++ b/src/library/tactic/defeq_simplifier/defeq_simp_lemmas.cpp @@ -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() { diff --git a/src/library/tactic/simplifier/simp_lemmas.cpp b/src/library/tactic/simplifier/simp_lemmas.cpp index a9e0ea101c..d2f20f63be 100644 --- a/src/library/tactic/simplifier/simp_lemmas.cpp +++ b/src/library/tactic/simplifier/simp_lemmas.cpp @@ -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() { diff --git a/src/library/unification_hint.cpp b/src/library/unification_hint.cpp index 35f0838188..0e47270430 100644 --- a/src/library/unification_hint.cpp +++ b/src/library/unification_hint.cpp @@ -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() { diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index 7c48328e13..a3e7988d27 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -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);