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

feat(library/compiler/emit_cpp): add name mangling functions

Browse source
This commit is contained in:
Leonardo de Moura 2019-01-23 14:46:04 -08:00
parent 8bcc965dc0
commit 02849a3cf6
1 changed files with 56 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -5,10 +5,65 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <fstream>
#include "runtime/utf8.h"
#include "library/compiler/emit_cpp.h"
namespace lean {
environment emit_cpp(environment const & env, comp_decls const &) {
static std::string mangle(std::string const & s) {
std::string out;
size_t i = 0;
while (i < s.size()) {
unsigned c = next_utf8(s, i);
if (c < 255) {
if (isalnum(c)) {
out += static_cast<unsigned char>(c);
} else if (c == '_') {
out += "__";
} else {
out += "_x";
out += ('0' + (c / 16));
out += ('0' + (c % 16));
}
} else {
out += "_u";
out += ('0' + (c / 4096));
c %= 4096;
out += ('0' + (c / 256));
c %= 256;
out += ('0' + (c / 16));
out += ('0' + (c % 16));
}
}
return out;
}
static void mangle(name const & n, std::string & out) {
if (n.is_anonymous()) {
return;
} else if (n.is_numeral()) {
mangle(n.get_prefix(), out);
out += "_";
out += n.get_numeral().to_std_string();
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;
}
}
std::string mangle(name const & n) {
std::string out("_l");
mangle(n, out);
return out;
}
environment emit_cpp(environment const & env, comp_decls const & /* ds */) {
// TODO(Leo)
return env;
}