michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/export): export the whole environment when using "--expor-all"

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-30 14:59:57 -07:00
parent bed751a2d7
commit 9bf64c10fd
1 changed files with 39 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

64
src/library/export.cpp
View file

@ -187,15 +187,15 @@ class exporter {
for_each(e, [&](expr const & e, unsigned) { for_each(e, [&](expr const & e, unsigned) {
if (is_constant(e)) { if (is_constant(e)) {
name const & n = const_name(e); name const & n = const_name(e);
if (!inductive::is_intro_rule(m_env, n) && export_declaration(n);
!inductive::is_elim_rule(m_env, n))
export_declaration(n);
} }
return true; return true;
}); });
} }
void export_definition(declaration const & d) { void export_definition(declaration const & d) {
if (inductive::is_intro_rule(m_env, d.get_name()) || inductive::is_elim_rule(m_env, d.get_name()))
return;
if (already_exported(d.get_name())) if (already_exported(d.get_name()))
return; return;
mark(d.get_name()); mark(d.get_name());
@ -284,35 +284,50 @@ class exporter {
} }
void export_declarations() { void export_declarations() {
buffer<name> ns; if (m_all) {
to_buffer(get_curr_module_decl_names(m_env), ns); m_env.for_each_declaration([&](declaration const & d) {
std::reverse(ns.begin(), ns.end()); export_declaration(d.get_name());
for (name const & n : ns) { });
export_declaration(n); } else {
buffer<name> ns;
to_buffer(get_curr_module_decl_names(m_env), ns);
std::reverse(ns.begin(), ns.end());
for (name const & n : ns) {
export_declaration(n);
}
} }
} }
void export_direct_imports() { void export_direct_imports() {
buffer<module_name> imports; if (!m_all) {
to_buffer(get_curr_module_imports(m_env), imports); buffer<module_name> imports;
std::reverse(imports.begin(), imports.end()); to_buffer(get_curr_module_imports(m_env), imports);
for (module_name const & m : imports) { std::reverse(imports.begin(), imports.end());
unsigned n = export_name(m.get_name()); for (module_name const & m : imports) {
if (m.is_relative()) { unsigned n = export_name(m.get_name());
m_out << "#RI " << *m.get_k() << " " << n << "\n"; if (m.is_relative()) {
} else { m_out << "#RI " << *m.get_k() << " " << n << "\n";
m_out << "#DI " << n << "\n"; } else {
m_out << "#DI " << n << "\n";
}
} }
} }
} }
void export_global_universes() { void export_global_universes() {
buffer<name> ns; if (m_all) {
to_buffer(get_curr_module_univ_names(m_env), ns); m_env.for_each_universe([&](name const & u) {
std::reverse(ns.begin(), ns.end()); unsigned n = export_name(u);
for (name const & u : ns) { m_out << "#UNI " << n << "\n";
unsigned n = export_name(u); });
m_out << "#UNI " << n << "\n"; } else {
buffer<name> ns;
to_buffer(get_curr_module_univ_names(m_env), ns);
std::reverse(ns.begin(), ns.end());
for (name const & u : ns) {
unsigned n = export_name(u);
m_out << "#UNI " << n << "\n";
}
} }
} }
@ -322,8 +337,7 @@ public:
void operator()() { void operator()() {
m_name2idx.insert(mk_pair(name(), 0)); m_name2idx.insert(mk_pair(name(), 0));
m_level2idx.insert(mk_pair(level(), 0)); m_level2idx.insert(mk_pair(level(), 0));
if (!m_all) export_direct_imports();
export_direct_imports();
export_global_universes(); export_global_universes();
export_declarations(); export_declarations();
} }