diff --git a/src/library/compiler/emit_cpp.cpp b/src/library/compiler/emit_cpp.cpp index 0417bff752..edfb92fbdc 100644 --- a/src/library/compiler/emit_cpp.cpp +++ b/src/library/compiler/emit_cpp.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include "runtime/utf8.h" +#include "library/module.h" #include "library/compiler/emit_cpp.h" namespace lean { @@ -68,8 +69,10 @@ environment emit_cpp(environment const & env, comp_decls const & /* ds */) { return env; } -void print_cpp_code(std::ofstream & out, environment const & /* env */) { +void print_cpp_code(std::ofstream & out, environment const & /* env */, module_name const & m, list const & deps) { out << "// Lean compiler output\n"; + out << "// Module: " << m << "\n"; + out << "// Imports:"; for (module_name const & d : deps) out << " " << d; out << "\n"; // TODO(Leo) } } diff --git a/src/library/compiler/emit_cpp.h b/src/library/compiler/emit_cpp.h index 49a44ccfa8..3e9130cb2c 100644 --- a/src/library/compiler/emit_cpp.h +++ b/src/library/compiler/emit_cpp.h @@ -5,10 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include "util/lean_path.h" #include "kernel/environment.h" #include "library/compiler/util.h" namespace lean { environment emit_cpp(environment const & env, comp_decls const & ds); -void print_cpp_code(std::ofstream & out, environment const & env); +void print_cpp_code(std::ofstream & out, environment const & env, module_name const & m, list const & deps); } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index f0601b69a9..9a9f42334e 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -577,8 +577,17 @@ int main(int argc, char ** argv) { display_cumulative_profiling_times(std::cerr); if (cpp_output) { + if (mods.size() != 1) { + std::cerr << "Error, option `--cpp=` expects one and only one input module\n"; + return 1; + } + module_name mod_name = mods[0].m_mod_info->m_name; + buffer dep_names; + for (auto d : mods[0].m_mod_info->m_deps) { + dep_names.push_back(d.m_mod_info->m_name); + } std::ofstream out(*cpp_output); - print_cpp_code(out, env); + print_cpp_code(out, env, mod_name, to_list(dep_names)); } if (!test_suite) {