From aa6d6c4dda71b87abf36fa305e5edeca8aadcbc7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 21 Sep 2020 08:26:15 -0700
Subject: [PATCH] feat: expose `mkModuleInitializationFunctionName`

cc @Kha

for https://github.com/leanprover/lean4/issues/185
---
 src/Lean/Compiler/IR/EmitC.lean     | 8 ++++----
 src/Lean/Compiler/NameMangling.lean | 4 ++++
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean
index a92d1ce7da..e760088496 100644
--- a/src/Lean/Compiler/IR/EmitC.lean
+++ b/src/Lean/Compiler/IR/EmitC.lean
@@ -160,7 +160,7 @@ lean_object* in; lean_object* res;";
   else
     emitLn "lean_initialize_runtime_module();";
   modName ← getModName;
-  emitLn ("res = initialize_" ++ (modName.mangle "") ++ "(lean_io_mk_world());");
+  emitLn ("res = " ++ mkModuleInitializationFunctionName modName ++ "(lean_io_mk_world());");
   emitLns ["lean_io_mark_end_initialization();",
            "if (lean_io_result_is_ok(res)) {",
            "lean_dec_ref(res);",
@@ -691,16 +691,16 @@ if isIOUnitInitFn env n then do {
 def emitInitFn : M Unit := do
 env ← getEnv;
 modName ← getModName;
-env.imports.forM $ fun imp => emitLn ("lean_object* initialize_" ++ imp.module.mangle "" ++ "(lean_object*);");
+env.imports.forM $ fun imp => emitLn ("lean_object* " ++ mkModuleInitializationFunctionName imp.module ++ "(lean_object*);");
 emitLns [
   "static bool _G_initialized = false;",
-  "lean_object* initialize_" ++ modName.mangle "" ++ "(lean_object* w) {",
+  "lean_object* " ++ mkModuleInitializationFunctionName modName ++ "(lean_object* w) {",
   "lean_object * res;",
   "if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));",
   "_G_initialized = true;"
 ];
 env.imports.forM $ fun imp => emitLns [
-  "res = initialize_" ++ imp.module.mangle "" ++ "(lean_io_mk_world());",
+  "res = " ++ mkModuleInitializationFunctionName imp.module ++ "(lean_io_mk_world());",
   "if (lean_io_result_is_error(res)) return res;",
   "lean_dec_ref(res);"];
 let decls := getDecls env;
diff --git a/src/Lean/Compiler/NameMangling.lean b/src/Lean/Compiler/NameMangling.lean
index c8ade51039..8f5c475e3d 100644
--- a/src/Lean/Compiler/NameMangling.lean
+++ b/src/Lean/Compiler/NameMangling.lean
@@ -47,4 +47,8 @@ private def Name.mangleAux : Name → String
 def Name.mangle (n : Name) (pre : String := "l_") : String :=
 pre ++ Name.mangleAux n
 
+@[export lean_mk_module_initialization_function_name]
+def mkModuleInitializationFunctionName (moduleName : Name) : String :=
+"initialize_" ++ moduleName.mangle ""
+
 end Lean