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

chore(library/scoped_ext): remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-03 12:57:18 -07:00
parent 224203f215
commit 5e237f1c47
3 changed files with 8 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/library/aliases.cpp
View file

@ -95,11 +95,6 @@ struct aliases_ext : public environment_extension {
return env;
}
static environment export_namespace(environment const & env, io_state const &, name const &) {
// do nothing, aliases are treated in a special way in the frontend.
return env;
}
static environment push_scope(environment const & env, io_state const &, scope_kind k) {
aliases_ext ext = get_extension(env);
ext.push(k != scope_kind::Namespace);
@ -119,9 +114,7 @@ static name * g_aliases = nullptr;
struct aliases_ext_reg {
unsigned m_ext_id;
aliases_ext_reg() {
register_scoped_ext(*g_aliases,
aliases_ext::using_namespace, aliases_ext::export_namespace,
aliases_ext::push_scope, aliases_ext::pop_scope);
register_scoped_ext(*g_aliases, aliases_ext::using_namespace, aliases_ext::push_scope, aliases_ext::pop_scope);
m_ext_id = environment::register_extension(std::make_shared<aliases_ext>());
}
};

25
src/library/scoped_ext.cpp
View file

@ -11,13 +11,13 @@ Author: Leonardo de Moura
#include "library/scoped_ext.h"
namespace lean {
typedef std::tuple<name, using_namespace_fn, export_namespace_fn, push_scope_fn, pop_scope_fn> entry;
typedef std::tuple<name, using_namespace_fn, push_scope_fn, pop_scope_fn> entry;
typedef std::vector<entry> scoped_exts;
static scoped_exts * g_exts = nullptr;
static scoped_exts & get_exts() { return *g_exts; }
void register_scoped_ext(name const & c, using_namespace_fn use, export_namespace_fn ex, push_scope_fn push, pop_scope_fn pop) {
get_exts().emplace_back(c, use, ex, push, pop);
void register_scoped_ext(name const & c, using_namespace_fn use, push_scope_fn push, pop_scope_fn pop) {
get_exts().emplace_back(c, use, push, pop);
}
struct scope_mng_ext : public environment_extension {
@ -96,21 +96,6 @@ environment using_namespace(environment const & env, io_state const & ios, name
return using_namespace(env, ios, n, metaclasses);
}
environment export_namespace(environment const & env, io_state const & ios, name const & n, buffer<name> const & metaclasses) {
environment r = env;
for (auto const & t : get_exts()) {
if (metaclasses.empty() ||
std::find(metaclasses.begin(), metaclasses.end(), std::get<0>(t)) != metaclasses.end())
r = std::get<2>(t)(r, ios, n);
}
return r;
}
environment export_namespace(environment const & env, io_state const & ios, name const & n) {
buffer<name> metaclasses;
return export_namespace(env, ios, n, metaclasses);
}
optional<name> to_valid_namespace_name(environment const & env, name const & n) {
scope_mng_ext const & ext = get_extension(env);
if (ext.m_namespace_set.contains(n))
@ -157,7 +142,7 @@ environment push_scope(environment const & env, io_state const & ios, scope_kind
ext.m_scope_kinds = cons(k, ext.m_scope_kinds);
environment r = update(env, ext);
for (auto const & t : get_exts()) {
r = std::get<3>(t)(r, ios, k);
r = std::get<2>(t)(r, ios, k);
}
if (k == scope_kind::Namespace)
r = using_namespace(r, ios, new_n);
@ -188,7 +173,7 @@ environment pop_scope_core(environment const & env, io_state const & ios) {
ext.m_scope_kinds = tail(ext.m_scope_kinds);
environment r = update(env, ext);
for (auto const & t : get_exts()) {
r = std::get<4>(t)(r, ios, k);
r = std::get<3>(t)(r, ios, k);
}
return r;
}

27
src/library/scoped_ext.h
View file

@ -17,19 +17,14 @@ Author: Leonardo de Moura
namespace lean {
enum class scope_kind { Namespace, Section };
typedef environment (*using_namespace_fn)(environment const &, io_state const &, name const &);
typedef environment (*export_namespace_fn)(environment const &, io_state const &, name const &);
typedef environment (*push_scope_fn)(environment const &, io_state const &, scope_kind);
typedef environment (*pop_scope_fn)(environment const &, io_state const &, scope_kind);
void register_scoped_ext(name const & n, using_namespace_fn use, export_namespace_fn ex, push_scope_fn push, pop_scope_fn pop);
void register_scoped_ext(name const & n, using_namespace_fn use, push_scope_fn push, pop_scope_fn pop);
/** \brief Use objects defined in the namespace \c n.
If \c metaclasses is not empty, then only objects in the given "metaclasses" \c c are considered. */
environment using_namespace(environment const & env, io_state const & ios, name const & n, buffer<name> const & metaclasses);
environment using_namespace(environment const & env, io_state const & ios, name const & n);
/** \brief Export objects defined in the namespace \c n to current namespace.
If \c metaclasses is not empty, then only objects in the given "metaclasses" \c c are considered. */
environment export_namespace(environment const & env, io_state const & ios, name const & n, buffer<name> const & metaclasses);
environment export_namespace(environment const & env, io_state const & ios, name const & n);
/** \brief Create a new scope, all scoped extensions are notified. */
environment push_scope(environment const & env, io_state const & ios, scope_kind k, name const & n = name());
@ -207,21 +202,6 @@ public:
return r;
}
/** \brief Copy entries from the given namespace to the current namespace. */
environment export_namespace(environment env, io_state const & ios, name const & ns) const {
if (auto it = m_entries_map.find(ns)) {
buffer<entry> entries;
to_buffer(*it, entries);
unsigned i = entries.size();
name current_ns = get_namespace(env);
while (i > 0) {
--i;
env = add_entry(env, ios, entries[i], current_ns, true);
}
}
return env;
}
/** \brief Open a namespace/section. It return the new updated state. */
scoped_ext push() const {
scoped_ext r(*this);
@ -253,7 +233,7 @@ public:
struct reg {
unsigned m_ext_id;
reg() {
register_scoped_ext(get_class_name(), using_namespace_fn, export_namespace_fn, push_fn, pop_fn);
register_scoped_ext(get_class_name(), using_namespace_fn, push_fn, pop_fn);
register_module_object_reader(get_serialization_key(), reader);
m_ext_id = environment::register_extension(std::make_shared<scoped_ext>());
}
@ -272,9 +252,6 @@ public:
static environment using_namespace_fn(environment const & env, io_state const & ios, name const & n) {
return update(env, get(env).using_namespace(env, ios, n));
}
static environment export_namespace_fn(environment const & env, io_state const & ios, name const & n) {
return get(env).export_namespace(env, ios, n);
}
static environment push_fn(environment const & env, io_state const &, scope_kind) {
return update(env, get(env).push());
}