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

refactor(library/export_decl): Re-implement for new scoped_ext

Browse source 
Use environment_extension to persist mapping from namespaces to export
decls, use new scoped_ext to keep track of currently active export decls.
This commit is contained in:
Sebastian Ullrich 2016-07-17 00:02:11 -04:00
parent 6f4a6c39f3
commit e69b508492
4 changed files with 102 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -65,7 +65,7 @@ environment section_cmd(parser & p) {
environment execute_open(environment env, io_state const & ios, export_decl const & edecl);
environment replay_export_decls_core(environment env, io_state const & ios, unsigned old_sz) {
list<export_decl> new_export_decls = get_export_decls(env);
list<export_decl> new_export_decls = get_active_export_decls(env);
unsigned new_sz = length(new_export_decls);
lean_assert(new_sz >= old_sz);
unsigned i = 0;
@ -86,7 +86,8 @@ environment execute_open(environment env, io_state const & ios, export_decl cons
unsigned fingerprint = 0;
name const & ns = edecl.m_ns;
fingerprint = hash(fingerprint, ns.hash());
unsigned old_export_decls_sz = length(get_export_decls(env));
unsigned old_export_decls_sz = length(get_active_export_decls(env));
env = activate_export_decls(env, ns);
for (auto const & p : edecl.m_renames) {
fingerprint = hash(hash(fingerprint, p.first.hash()), p.second.hash());
env = add_expr_alias(env, p.first, p.second);
@ -106,8 +107,9 @@ environment execute_open(environment env, io_state const & ios, export_decl cons
environment namespace_cmd(parser & p) {
name n = p.check_decl_id_next("invalid namespace declaration, identifier expected");
p.push_local_scope();
unsigned old_export_decls_sz = length(get_export_decls(p.env()));
unsigned old_export_decls_sz = length(get_active_export_decls(p.env()));
environment env = push_scope(p.env(), p.ios(), scope_kind::Namespace, n);
env = activate_export_decls(env, get_namespace(env));
return replay_export_decls_core(env, p.ios(), old_export_decls_sz);
}

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

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include <limits>
#include <vector>
#include <util/utf8.h>
#include <library/export_decl.h>
#include "util/interrupt.h"
#include "util/sstream.h"
#include "util/flet.h"
@ -1965,6 +1966,7 @@ void parser::parse_imports() {
m_env = import_modules(m_env, base, olean_files.size(), olean_files.data(), num_threads,
keep_imported_thms, m_ios);
m_env = update_fingerprint(m_env, fingerprint);
m_env = activate_export_decls(m_env, {}); // explicitly activate exports in root namespace
m_env = replay_export_decls_core(m_env, m_ios);
if (imported)
commit_info(1, 0);

122
src/library/export_decl.cpp
View file

@ -10,7 +10,8 @@ Author: Leonardo de Moura
#include "library/scoped_ext.h"
namespace lean {
static std::string * g_key = nullptr;
static std::string * g_export_decl_key = nullptr;
static std::string * g_active_export_decls_key = nullptr;
static void write_pair_name(serializer & s, pair<name, name> const & p) {
s << p.first << p.second;
@ -40,7 +41,65 @@ bool operator!=(export_decl const & d1, export_decl const & d2) {
return !(d1 == d2);
}
struct export_decl_config {
struct export_decl_env_ext : public environment_extension {
name_map<list<export_decl>> m_ns_map;
export_decl_env_ext() {}
export_decl_env_ext(name_map<list<export_decl>> const & ns_map): m_ns_map(ns_map) {}
};
/** \brief Auxiliary object for registering the environment extension */
struct export_decl_env_ext_reg {
unsigned m_ext_id;
export_decl_env_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<export_decl_env_ext>()); }
};
static export_decl_env_ext_reg * g_ext = nullptr;
/** \brief Retrieve environment extension */
static export_decl_env_ext const & get_export_decl_extension(environment const & env) {
return static_cast<export_decl_env_ext const &>(env.get_extension(g_ext->m_ext_id));
}
/** \brief Update environment extension */
static environment update(environment const & env, export_decl_env_ext const & ext) {
return env.update(g_ext->m_ext_id, std::make_shared<export_decl_env_ext>(ext));
}
static void read_export_decls(deserializer & d, shared_environment &,
std::function<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> & add_delayed_update) {
name in_ns;
export_decl e;
d >> in_ns >> e.m_ns >> e.m_as >> e.m_had_explicit;
e.m_except_names = read_list<name>(d, read_name);
e.m_renames = read_list<pair<name, name>>(d, read_pair_name);
add_delayed_update([=](environment const & env, io_state const &) -> environment {
return add_export_decl(env, in_ns, e);
});
}
environment add_export_decl(environment const & env, name const & in_ns, export_decl const & e) {
auto ns_map = get_export_decl_extension(env).m_ns_map;
list<export_decl> decls;
if (ns_map.contains(in_ns))
decls = *ns_map.find(in_ns);
if (std::find(decls.begin(), decls.end(), e) != decls.end())
return env;
auto new_env = update(env, export_decl_env_ext(insert(ns_map, in_ns, cons(e, decls))));
return module::add(new_env, *g_export_decl_key, [=](environment const &, serializer & s) {
s << in_ns << e.m_ns << e.m_as << e.m_had_explicit;
write_list<name>(s, e.m_except_names);
write_list<pair<name, name>>(s, e.m_renames);
});
}
environment add_export_decl(environment const & env, export_decl const & entry) {
return add_export_decl(env, get_namespace(env), entry);
}
struct active_export_decls_config {
typedef export_decl entry;
typedef list<export_decl> state;
@ -49,48 +108,49 @@ struct export_decl_config {
s = cons(e, s);
}
}
static std::string const & get_serialization_key() {
return *g_key;
}
static void write_entry(serializer & s, entry const & e) {
s << e.m_ns << e.m_as << e.m_had_explicit;
write_list<name>(s, e.m_except_names);
write_list<pair<name, name>>(s, e.m_renames);
}
static entry read_entry(deserializer & d) {
entry e;
d >> e.m_ns >> e.m_as >> e.m_had_explicit;
e.m_except_names = read_list<name>(d, read_name);
e.m_renames = read_list<pair<name, name>>(d, read_pair_name);
return e;
}
static optional<unsigned> get_fingerprint(entry const &) {
return optional<unsigned>();
}
// uses local scope only
static std::string const & get_serialization_key() { return *g_active_export_decls_key; }
static void write_entry(serializer &, entry const &) { lean_unreachable(); }
static entry read_entry(deserializer &) { lean_unreachable(); }
};
template class scoped_ext<export_decl_config>;
typedef scoped_ext<export_decl_config> export_decl_ext;
template class scoped_ext<active_export_decls_config>;
typedef scoped_ext<active_export_decls_config> active_export_decls_ext;
environment add_export_decl(environment const & env, export_decl const & entry) {
bool persistent = true;
return export_decl_ext::add_entry(env, get_dummy_ios(), entry, persistent);
environment activate_export_decls(environment env, name ns) {
auto ns_map = get_export_decl_extension(env).m_ns_map;
while (true) {
if (ns_map.contains(ns)) {
for (auto const & e : *ns_map.find(ns))
env = active_export_decls_ext::add_entry(env, get_dummy_ios(), e, false);
}
if (ns.is_anonymous())
break;
ns = ns.get_prefix();
}
return env;
}
list<export_decl> get_export_decls(environment const & env) {
return export_decl_ext::get_state(env);
list<export_decl> get_active_export_decls(environment const & env) {
return active_export_decls_ext::get_state(env);
}
void initialize_export_decl() {
g_key = new std::string("export_decl");
export_decl_ext::initialize();
g_export_decl_key = new std::string("export_decl");
g_active_export_decls_key = new std::string("active_export_decls"); // unused
g_ext = new export_decl_env_ext_reg();
register_module_object_reader(*g_export_decl_key, read_export_decls);
active_export_decls_ext::initialize();
}
void finalize_export_decl() {
delete g_key;
export_decl_ext::finalize();
active_export_decls_ext::finalize();
delete g_active_export_decls_key;
delete g_export_decl_key;
delete g_ext;
}
}

5
src/library/export_decl.h
View file

@ -23,8 +23,11 @@ struct export_decl {
};
/** \brief We store export commands to allow us to replay them whenever the namespace is opened. */
environment add_export_decl(environment const & env, name const & in_ns, export_decl const & e);
environment add_export_decl(environment const & env, export_decl const & entry);
list<export_decl> get_export_decls(environment const & env);
environment activate_export_decls(environment, name);
list<export_decl> get_active_export_decls(environment const & env);
void initialize_export_decl();
void finalize_export_decl();