From 463e4a2cf370d812d7329ef4189f3bc7fb251b94 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 6 Jul 2016 17:39:06 -0700 Subject: [PATCH] refactor(library/reducible): replace ext with attribute_manager --- src/frontends/lean/print_cmd.cpp | 6 -- src/library/attribute_manager.cpp | 11 ++++ src/library/attribute_manager.h | 3 + src/library/reducible.cpp | 99 +++++-------------------------- 4 files changed, 29 insertions(+), 90 deletions(-) diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index 374ff9361e..dd64ed924d 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -641,12 +641,6 @@ environment print_cmd(parser & p) { } else if (p.curr_is_token_or_id(get_no_pattern_attr_tk())) { p.next(); print_no_patterns(p); - } else if (p.curr_is_token_or_id(get_reducible_tk())) { - p.next(); - print_reducible_info(p, reducible_status::Reducible); - } else if (p.curr_is_token_or_id(get_irreducible_tk())) { - p.next(); - print_reducible_info(p, reducible_status::Irreducible); } else if (p.curr_is_token_or_id(get_options_tk())) { p.next(); out << p.ios().get_options() << endl; diff --git a/src/library/attribute_manager.cpp b/src/library/attribute_manager.cpp index c6ec45f42d..608df4b34b 100644 --- a/src/library/attribute_manager.cpp +++ b/src/library/attribute_manager.cpp @@ -122,6 +122,12 @@ void register_no_params_attribute(char const * attr, char const * descr, set_no_ return on_set(env, ios, d, ns, persistent); }); } +void register_no_params_attribute(char const * attr, char const * descr) { + register_no_params_attribute(attr, descr, + [](environment const & env, io_state const &, name const &, name const &, bool) { + return env; + }); +} void register_prio_attribute(char const * attr, char const * descr, set_prio_attribute_proc const & on_set) { register_attribute(attr, descr, @@ -232,6 +238,11 @@ environment set_attribute(environment const & env, io_state const & ios, char co throw_unknown_attribute(attr); } +environment set_attribute(environment const & env, io_state const & ios, char const * attr, + name const & d, name const & ns, bool persistent) { + return set_attribute(env, ios, attr, d, LEAN_DEFAULT_PRIORITY, list(), ns, persistent); +} + unsigned get_attribute_prio(environment const & env, name const & attr, name const & d) { if (auto it = attribute_ext::get_state(env).find(attr)) { optional prio = it->get_prio({d, list()}); diff --git a/src/library/attribute_manager.h b/src/library/attribute_manager.h index babad4a574..0bc4dfaf2d 100644 --- a/src/library/attribute_manager.h +++ b/src/library/attribute_manager.h @@ -28,6 +28,7 @@ typedef std::function const & params, name const & ns, bool persistent); +environment set_attribute(environment const & env, io_state const & ios, char const * attr, + name const & d, name const & ns, bool persistent); bool has_attribute(environment const & env, char const * attr, name const & d); void get_attribute_instances(environment const & env, name const & attr, buffer &); diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp index 85c82594d2..a79fd4a558 100644 --- a/src/library/reducible.cpp +++ b/src/library/reducible.cpp @@ -14,76 +14,10 @@ Author: Leonardo de Moura #include "library/attribute_manager.h" namespace lean { -struct reducible_entry { - reducible_status m_status; - name m_name; - reducible_entry():m_status(reducible_status::Semireducible) {} - reducible_entry(reducible_status s, name const & n):m_status(s), m_name(n) {} -}; - -typedef name_map reducible_state; - -static reducible_status get_status(reducible_state const & s, name const & n) { - if (auto it = s.find(n)) - return *it; - else - return reducible_status::Semireducible; -} - -static name * g_class_name = nullptr; -static std::string * g_key = nullptr; - -struct reducible_config { - typedef reducible_state state; - typedef reducible_entry entry; - static void add_entry(environment const &, io_state const &, state & s, entry const & e) { - s.insert(e.m_name, e.m_status); - } - static name const & get_class_name() { - return *g_class_name; - } - static std::string const & get_serialization_key() { - return *g_key; - } - static void write_entry(serializer & s, entry const & e) { - s << static_cast(e.m_status) << e.m_name; - } - static entry read_entry(deserializer & d) { - entry e; char s; - d >> s >> e.m_name; - e.m_status = static_cast(s); - return e; - } - static optional get_fingerprint(entry const & e) { - return some(hash(static_cast(e.m_status), e.m_name.hash())); - } -}; - -template class scoped_ext; -typedef scoped_ext reducible_ext; - void initialize_reducible() { - g_class_name = new name("reducible"); - g_key = new std::string("REDU"); - reducible_ext::initialize(); - - register_no_params_attribute("reducible", "reducible", - [](environment const & env, io_state const &, name const & d, name const & ns, - bool persistent) { - return set_reducible(env, d, reducible_status::Reducible, ns, persistent); - }); - - register_no_params_attribute("semireducible", "semireducible", - [](environment const & env, io_state const &, name const & d, name const & ns, - bool persistent) { - return set_reducible(env, d, reducible_status::Semireducible, ns, persistent); - }); - - register_no_params_attribute("irreducible", "irreducible", - [](environment const & env, io_state const &, name const & d, name const & ns, - bool persistent) { - return set_reducible(env, d, reducible_status::Irreducible, ns, persistent); - }); + register_no_params_attribute("reducible", "reducible"); + register_no_params_attribute("semireducible", "semireducible"); + register_no_params_attribute("irreducible", "irreducible"); register_incompatible("reducible", "semireducible"); register_incompatible("reducible", "irreducible"); @@ -91,14 +25,6 @@ void initialize_reducible() { } void finalize_reducible() { - reducible_ext::finalize(); - delete g_key; - delete g_class_name; -} - -void for_each_reducible(environment const & env, std::function const & fn) { - reducible_state m_state = reducible_ext::get_state(env); - m_state.for_each(fn); } static void check_declaration(environment const & env, name const & n) { @@ -109,25 +35,30 @@ static void check_declaration(environment const & env, name const & n) { environment set_reducible(environment const & env, name const & n, reducible_status s, name const & ns, bool persistent) { check_declaration(env, n); - return reducible_ext::add_entry(env, get_dummy_ios(), reducible_entry(s, n), ns, persistent); + return set_attribute(env, get_dummy_ios(), + s == reducible_status::Reducible ? "reducible" : + s == reducible_status::Irreducible ? "irreducible" : + "semireducible", n, ns, persistent); } reducible_status get_reducible_status(environment const & env, name const & n) { - reducible_state const & s = reducible_ext::get_state(env); - return get_status(s, n); + if (has_attribute(env, "reducible", n)) + return reducible_status::Reducible; + else if (has_attribute(env, "irreducible", n)) + return reducible_status::Irreducible; + else + return reducible_status::Semireducible; } name_predicate mk_not_reducible_pred(environment const & env) { - reducible_state m_state = reducible_ext::get_state(env); return [=](name const & n) { // NOLINT - return get_status(m_state, n) != reducible_status::Reducible; + return !has_attribute(env, "reducible", n); }; } name_predicate mk_irreducible_pred(environment const & env) { - reducible_state m_state = reducible_ext::get_state(env); return [=](name const & n) { // NOLINT - return get_status(m_state, n) == reducible_status::Irreducible; + return has_attribute(env, "irreducible", n); }; }