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

feat: expose mkModuleInitializationFunctionName

Browse source 
cc @Kha

for https://github.com/leanprover/lean4/issues/185
This commit is contained in:
Leonardo de Moura 2020-09-21 08:26:15 -07:00
parent 30a1e0228b
commit aa6d6c4dda
2 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Compiler/IR/EmitC.lean
View file

@ -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;

4
src/Lean/Compiler/NameMangling.lean
View file

@ -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