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

chore(library/compiler/emit_cpp): just store a list of decls

Browse source
This commit is contained in:
Leonardo de Moura 2019-01-25 10:22:30 -08:00
parent 2d9a16fd24
commit 4b66b442c9
1 changed files with 9 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/library/compiler/emit_cpp.cpp
View file

@ -38,7 +38,7 @@ optional<name> get_cppname_for(environment const & env, name const & n) {
}
struct emit_cpp_ext : public environment_extension {
name_map<expr> m_code;
comp_decls m_code;
};
struct emit_cpp_ext_reg {
@ -60,23 +60,20 @@ environment emit_cpp(environment const & env, comp_decls const & ds) {
Reason: the attributes for `ds` are only applied after the compiler is executed,
and we need to be able to access the `[cppname]` attribute. */
emit_cpp_ext ext = get_extension(env);
for (comp_decl const & d : ds) {
ext.m_code.insert(d.fst(), d.snd());
}
return update(env, ext);
ext.m_code = append(ext.m_code, ds);
return update(env, ext);
}
void print_cpp_code(std::ofstream & out, environment const & env, module_name const & m, list<module_name> const & deps) {
out << "// Lean compiler output\n";
out << "// Module: " << m << "\n";
out << "// Imports:"; for (module_name const & d : deps) out << " " << d; out << "\n";
name_map<expr> code = get_extension(env).m_code;
// TODO(Leo)
for_each(code, [&](name const & n, expr const &) {
out << "// " << n;
if (optional<name> c = get_cppname_for(env, n)) out << " ==> " << *c;
out << "\n";
});
comp_decls ds = get_extension(env).m_code;
for (comp_decl const & d : ds) {
out << "// " << d.fst();
if (optional<name> c = get_cppname_for(env, d.fst())) out << " ==> " << *c;
out << "\n";
}
}
void initialize_emit_cpp() {