From eace1bacb3375de9f5cfd57362246d8a20e96dae Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 24 Jan 2019 13:57:13 -0800
Subject: [PATCH] refactor(library/compiler): move name mangling procedures to
 separate file

We will need them to implement the LLVM IR backend.
---
 src/library/compiler/CMakeLists.txt    |  2 +-
 src/library/compiler/emit_cpp.cpp      | 54 ---------------------
 src/library/compiler/name_mangling.cpp | 65 ++++++++++++++++++++++++++
 src/library/compiler/name_mangling.h   | 12 +++++
 4 files changed, 78 insertions(+), 55 deletions(-)
 create mode 100644 src/library/compiler/name_mangling.cpp
 create mode 100644 src/library/compiler/name_mangling.h

diff --git a/src/library/compiler/CMakeLists.txt b/src/library/compiler/CMakeLists.txt
index 3845361667..79a9c7b049 100644
--- a/src/library/compiler/CMakeLists.txt
+++ b/src/library/compiler/CMakeLists.txt
@@ -4,4 +4,4 @@ add_library(compiler OBJECT
   util.cpp lcnf.cpp csimp.cpp elim_dead_let.cpp cse.cpp erase_irrelevant.cpp
   specialize.cpp compiler.cpp lambda_lifting.cpp extract_closed.cpp
   simp_app_args.cpp llnf.cpp ll_infer_type.cpp reduce_arity.cpp
-  closed_term_cache.cpp builtin.cpp emit_cpp.cpp)
+  closed_term_cache.cpp builtin.cpp name_mangling.cpp emit_cpp.cpp)
diff --git a/src/library/compiler/emit_cpp.cpp b/src/library/compiler/emit_cpp.cpp
index edfb92fbdc..f61ae360a7 100644
--- a/src/library/compiler/emit_cpp.cpp
+++ b/src/library/compiler/emit_cpp.cpp
@@ -10,60 +10,6 @@ Author: Leonardo de Moura
 #include "library/compiler/emit_cpp.h"
 
 namespace lean {
-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;
diff --git a/src/library/compiler/name_mangling.cpp b/src/library/compiler/name_mangling.cpp
new file mode 100644
index 0000000000..5a5ae1a6c2
--- /dev/null
+++ b/src/library/compiler/name_mangling.cpp
@@ -0,0 +1,65 @@
+/*
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <fstream>
+#include "runtime/utf8.h"
+#include "util/name.h"
+
+namespace lean {
+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;
+}
+}
diff --git a/src/library/compiler/name_mangling.h b/src/library/compiler/name_mangling.h
new file mode 100644
index 0000000000..1028d1ed59
--- /dev/null
+++ b/src/library/compiler/name_mangling.h
@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/name.h"
+
+namespace lean {
+std::string mangle(name const & n);
+}