diff --git a/src/library/export.cpp b/src/library/export.cpp index aae5f1f6f..9b7b73738 100644 --- a/src/library/export.cpp +++ b/src/library/export.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include "kernel/expr_maps.h" +#include "kernel/for_each_fn.h" #include "kernel/inductive/inductive.h" #include "library/max_sharing.h" #include "library/module.h" @@ -22,11 +23,21 @@ using name_hmap = typename std::unordered_map; class exporter { std::ostream & m_out; environment m_env; + bool m_all; + name_set m_exported; max_sharing_fn m_max_sharing; name_hmap m_name2idx; level_map m_level2idx; expr_map m_expr2idx; + void mark(name const & n) { + m_exported.insert(n); + } + + bool already_exported(name const & n) { + return m_exported.contains(n); + } + unsigned export_name(name const & n) { auto it = m_name2idx.find(n); if (it != m_name2idx.end()) @@ -172,9 +183,28 @@ class exporter { return export_expr(m_max_sharing(unfold_all_macros(m_env, e))); } + void export_dependencies(expr const & e) { + for_each(e, [&](expr const & e, unsigned) { + if (is_constant(e)) { + name const & n = const_name(e); + if (!inductive::is_intro_rule(m_env, n) && + !inductive::is_elim_rule(m_env, n)) + export_declaration(n); + } + return true; + }); + } + void export_definition(declaration const & d) { + if (already_exported(d.get_name())) + return; + mark(d.get_name()); unsigned n = export_name(d.get_name()); buffer ps; + if (m_all) { + export_dependencies(d.get_type()); + export_dependencies(d.get_value()); + } for (name const & p : d.get_univ_params()) ps.push_back(export_name(p)); unsigned t = export_root_expr(d.get_type()); @@ -186,8 +216,13 @@ class exporter { } void export_axiom(declaration const & d) { + if (already_exported(d.get_name())) + return; + mark(d.get_name()); unsigned n = export_name(d.get_name()); buffer ps; + if (m_all) + export_dependencies(d.get_type()); for (name const & p : d.get_univ_params()) ps.push_back(export_name(p)); unsigned t = export_root_expr(d.get_type()); @@ -198,8 +233,19 @@ class exporter { } void export_inductive(name const & n) { + if (already_exported(n)) + return; + mark(n); std::tuple> decls = *inductive::is_inductive_decl(m_env, n); + if (m_all) { + for (inductive::inductive_decl const & d : std::get<2>(decls)) { + export_dependencies(inductive::inductive_decl_type(d)); + for (inductive::intro_rule const & c : inductive::inductive_decl_intros(d)) { + export_dependencies(inductive::intro_rule_type(c)); + } + } + } for (name const & p : std::get<0>(decls)) export_name(p); for (inductive::inductive_decl const & d : std::get<2>(decls)) { @@ -241,8 +287,9 @@ class exporter { buffer ns; to_buffer(get_curr_module_decl_names(m_env), ns); std::reverse(ns.begin(), ns.end()); - for (name const & n : ns) + for (name const & n : ns) { export_declaration(n); + } } void export_direct_imports() { @@ -270,18 +317,23 @@ class exporter { } public: - exporter(std::ostream & out, environment const & env):m_out(out), m_env(env) {} + exporter(std::ostream & out, environment const & env, bool all):m_out(out), m_env(env), m_all(all) {} void operator()() { m_name2idx.insert(mk_pair(name(), 0)); m_level2idx.insert(mk_pair(level(), 0)); - export_direct_imports(); + if (!m_all) + export_direct_imports(); export_global_universes(); export_declarations(); } }; void export_module_as_lowtext(std::ostream & out, environment const & env) { - exporter(out, env)(); + exporter(out, env, false)(); +} + +void export_all_as_lowtext(std::ostream & out, environment const & env) { + exporter(out, env, true)(); } } diff --git a/src/library/export.h b/src/library/export.h index caa9a9c80..871fe6e75 100644 --- a/src/library/export.h +++ b/src/library/export.h @@ -8,4 +8,5 @@ Author: Leonardo de Moura #include "kernel/environment.h" namespace lean { void export_module_as_lowtext(std::ostream & out, environment const & env); +void export_all_as_lowtext(std::ostream & out, environment const & env); } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 796b0ebe4..71cc34c11 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -132,6 +132,7 @@ static void display_help(std::ostream & out) { std::cout << " --goal display goal at close to given position\n"; std::cout << " --hole display type of the \"hole\" in the given posivition\n"; std::cout << " --export=file -E export final environment as textual low-level file\n"; + std::cout << " --export-all=file -A export final environment (and all dependencies) as textual low-level file\n"; } static char const * get_file_extension(char const * fname) { @@ -160,6 +161,7 @@ static struct option g_long_options[] = { {"githash", no_argument, 0, 'g'}, {"output", required_argument, 0, 'o'}, {"export", required_argument, 0, 'E'}, + {"export-all", required_argument, 0, 'A'}, {"memory", required_argument, 0, 'M'}, {"trust", required_argument, 0, 't'}, {"discard", no_argument, 0, 'r'}, @@ -184,7 +186,7 @@ static struct option g_long_options[] = { {0, 0, 0, 0} }; -#define OPT_STR "PHRXFdD:qrlupgvhk:012t:012o:E:c:i:L:012O:012GZ" +#define OPT_STR "PHRXFdD:qrlupgvhk:012t:012o:E:c:i:L:012O:012GZA" #if defined(LEAN_TRACK_MEMORY) #define OPT_STR2 OPT_STR "M:012" @@ -261,6 +263,7 @@ int main(int argc, char ** argv) { optional line; optional column; optional export_txt; + optional export_all_txt; bool show_goal = false; bool show_hole = false; input_kind default_k = input_kind::Unspecified; @@ -368,6 +371,9 @@ int main(int argc, char ** argv) { case 'E': export_txt = std::string(optarg); break; + case 'A': + export_all_txt = std::string(optarg); + break; default: std::cerr << "Unknown command line option\n"; display_help(std::cerr); @@ -518,6 +524,10 @@ int main(int argc, char ** argv) { std::ofstream out(*export_txt); export_module_as_lowtext(out, env); } + if (export_all_txt) { + std::ofstream out(*export_all_txt); + export_all_as_lowtext(out, env); + } return ok ? 0 : 1; } catch (lean::throwable & ex) { lean::display_error(diagnostic(env, ios), nullptr, ex);