diff --git a/src/library/compiler/emit_cpp.cpp b/src/library/compiler/emit_cpp.cpp index 50ebba577d..8b98a1dbaf 100644 --- a/src/library/compiler/emit_cpp.cpp +++ b/src/library/compiler/emit_cpp.cpp @@ -812,14 +812,14 @@ static void emit_fns(std::ostream & out, environment const & env) { static void emit_initialize(std::ostream & out, environment const & env, module_name const & m, list const & deps) { for (module_name const & d : deps) { - out << "void _l_initialize_" << mangle(d) << "();\n"; + out << "void initialize_" << mangle(d, false) << "();\n"; } out << "static bool _G_initialized = false;\n"; - out << "void _l_initialize_" << mangle(m) << "() {\n"; + out << "void initialize_" << mangle(m, false) << "() {\n"; out << " if (_G_initialized) return;\n"; out << " _G_initialized = true;\n"; for (module_name const & d : deps) { - out << " _l_initialize_" << mangle(d) << "();\n"; + out << " initialize_" << mangle(d, false) << "();\n"; } comp_decls ds = get_extension(env).m_code; for (comp_decl const & d : ds) { diff --git a/src/library/compiler/name_mangling.cpp b/src/library/compiler/name_mangling.cpp index 5a5ae1a6c2..5e87d0683e 100644 --- a/src/library/compiler/name_mangling.cpp +++ b/src/library/compiler/name_mangling.cpp @@ -20,12 +20,12 @@ static std::string mangle(std::string const & s) { } else if (c == '_') { out += "__"; } else { - out += "_x"; + out += "_x_"; out += ('0' + (c / 16)); out += ('0' + (c % 16)); } } else { - out += "_u"; + out += "_u_"; out += ('0' + (c / 4096)); c %= 4096; out += ('0' + (c / 256)); @@ -47,18 +47,17 @@ static void mangle(name const & n, std::string & out) { out += "_"; } else { lean_assert(n.is_string()); - mangle(n.get_prefix(), out); - out += "_s"; - std::string s = mangle(n.get_string().to_std_string()); - unsigned len = s.size(); - out += std::to_string(len); - out += "_"; - out += s; + if (!n.get_prefix().is_anonymous()) { + mangle(n.get_prefix(), out); + out += "_"; + } + out += mangle(n.get_string().to_std_string()); } } -std::string mangle(name const & n) { - std::string out("_l"); +std::string mangle(name const & n, bool add_prefix) { + std::string out; + if (add_prefix) out += "l_"; mangle(n, out); return out; } diff --git a/src/library/compiler/name_mangling.h b/src/library/compiler/name_mangling.h index 1028d1ed59..811b88e1ba 100644 --- a/src/library/compiler/name_mangling.h +++ b/src/library/compiler/name_mangling.h @@ -8,5 +8,5 @@ Author: Leonardo de Moura #include "util/name.h" namespace lean { -std::string mangle(name const & n); +std::string mangle(name const & n, bool add_prefix = true); }