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

chore: update stage0

Browse source
This commit is contained in:
Sebastian Ullrich 2021-09-20 11:27:49 +02:00
parent 35ffae6f54
commit f5aa8ea4f5
4 changed files with 236 additions and 190 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/CMakeLists.txt generated
View file

@ -181,7 +181,7 @@ endif()
set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules")
# Initialize CXXFLAGS.
set(CMAKE_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\"")
set(CMAKE_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\" -DLEAN_EXPORTING")
set(CMAKE_CXX_FLAGS_DEBUG "-DLEAN_DEBUG -DLEAN_TRACE")
set(CMAKE_CXX_FLAGS_MINSIZEREL "-DNDEBUG")
set(CMAKE_CXX_FLAGS_RELEASE "-DNDEBUG")

17
stage0/src/Lean/Compiler/IR/EmitC.lean generated
View file

@ -90,12 +90,15 @@ def toCInitName (n : Name) : M String := do
def emitCInitName (n : Name) : M Unit :=
toCInitName n >>= emit
def emitFnDeclAux (decl : Decl) (cppBaseName : String) (addExternForConsts : Bool) : M Unit := do
def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M Unit := do
let ps := decl.params
let env ← getEnv
if ps.isEmpty then
if isClosedTermName env decl.name then emit "static "
else if addExternForConsts then emit "extern "
else if isExternal then emit "extern "
else emit "LEAN_EXPORT "
else
if !isExternal then emit "LEAN_EXPORT "
emit (toCType decl.resultType ++ " " ++ cppBaseName)
unless ps.isEmpty do
emit "("
@ -110,15 +113,15 @@ def emitFnDeclAux (decl : Decl) (cppBaseName : String) (addExternForConsts : Boo
emit ")"
emitLn ";"
def emitFnDecl (decl : Decl) (addExternForConsts : Bool) : M Unit := do
def emitFnDecl (decl : Decl) (isExternal : Bool) : M Unit := do
let cppBaseName ← toCName decl.name
emitFnDeclAux decl cppBaseName addExternForConsts
emitFnDeclAux decl cppBaseName isExternal
def emitExternDeclAux (decl : Decl) (cNameStr : String) : M Unit := do
let cName := Name.mkSimple cNameStr
let env ← getEnv
let extC := isExternC env decl.name
emitFnDeclAux decl cNameStr (!extC)
emitFnDeclAux decl cNameStr extC
def emitFnDecls : M Unit := do
let env ← getEnv
@ -643,6 +646,8 @@ def emitDeclAux (d : Decl) : M Unit := do
let baseName ← toCName f;
if xs.size == 0 then
emit "static "
else
emit "LEAN_EXPORT " -- make symbol visible to the interpreter
emit (toCType t); emit " ";
if xs.size > 0 then
emit baseName;
@ -709,7 +714,7 @@ def emitInitFn : M Unit := do
env.imports.forM fun imp => emitLn ("lean_object* " ++ mkModuleInitializationFunctionName imp.module ++ "(lean_object*);")
emitLns [
"static bool _G_initialized = false;",
"lean_object* " ++ mkModuleInitializationFunctionName modName ++ "(lean_object* w) {",
"LEAN_EXPORT 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;"

13
stage0/src/include/lean/lean.h generated
View file

@ -46,6 +46,19 @@ extern "C" {
#define LEAN_ALWAYS_INLINE
#endif
#ifdef _WIN32
#define LEAN_EXPORT __declspec(dllexport)
#else
#define LEAN_EXPORT
#endif
// We set `LEAN_EXPORTING` when compiling objects of libleanshared, but not when including this header in any other context.
#if defined LEAN_EXPORTING
#define LEAN_SHARED LEAN_EXPORT
#else
#define LEAN_SHARED
#endif
#ifdef LEAN_RUNTIME_STATS
#define LEAN_RUNTIME_STAT_CODE(c) c
#else

394
stage0/stdlib/Lean/Compiler/IR/EmitC.c generated
View file

@ -470,6 +470,7 @@ lean_object* l_Nat_forM_loop___at_Lean_IR_EmitC_emitArgs___spec__1___lambda__1__
lean_object* l_Nat_foldM_loop___at_Lean_IR_EmitC_emitSimpleExternalCall___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_foldM_loop___at_Lean_IR_EmitC_emitSimpleExternalCall___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitTag(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_IR_EmitC_emitInitFn___closed__11;
lean_object* l_Lean_IR_EmitC_emitDecl(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_throwUnknownVar(lean_object*);
lean_object* l_Lean_IR_EmitC_isIf(lean_object*);
@ -528,6 +529,7 @@ lean_object* l_Lean_IR_EmitC_emitFullApp(lean_object*, lean_object*, lean_object
uint8_t l_Lean_IR_usesModuleFrom(lean_object*, lean_object*);
static lean_object* l_Lean_IR_EmitC_emitMainFn___lambda__2___closed__30;
static lean_object* l_Lean_IR_EmitC_declareVar___closed__1;
static lean_object* l_Lean_IR_EmitC_emitFnDeclAux___closed__3;
lean_object* l_Lean_IR_EmitC_declareVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitSSet(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_mod(lean_object*, lean_object*);
@ -2123,7 +2125,7 @@ static lean_object* _init_l_Lean_IR_EmitC_emitFnDeclAux___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("extern ");
x_1 = lean_mk_string("LEAN_EXPORT ");
return x_1;
}
}
@ -2131,6 +2133,14 @@ static lean_object* _init_l_Lean_IR_EmitC_emitFnDeclAux___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("extern ");
return x_1;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitFnDeclAux___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("static ");
return x_1;
}
@ -2149,44 +2159,58 @@ lean_dec(x_7);
x_10 = l_Array_isEmpty___rarg(x_6);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12;
x_11 = lean_box(0);
x_12 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_11, x_4, x_9);
return x_12;
if (x_3 == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_11 = l_Lean_IR_EmitC_emitFnDeclAux___closed__1;
x_12 = lean_string_append(x_9, x_11);
x_13 = lean_box(0);
x_14 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_13, x_4, x_12);
return x_14;
}
else
{
lean_object* x_13; uint8_t x_14;
x_13 = l_Lean_IR_Decl_name(x_1);
x_14 = l_Lean_isClosedTermName(x_8, x_13);
lean_dec(x_13);
if (x_14 == 0)
{
if (x_3 == 0)
{
lean_object* x_15; lean_object* x_16;
x_15 = lean_box(0);
x_16 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_15, x_4, x_9);
return x_16;
}
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_17 = l_Lean_IR_EmitC_emitFnDeclAux___closed__1;
x_18 = lean_string_append(x_9, x_17);
x_19 = lean_box(0);
x_20 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_19, x_4, x_18);
return x_20;
lean_object* x_17; uint8_t x_18;
x_17 = l_Lean_IR_Decl_name(x_1);
x_18 = l_Lean_isClosedTermName(x_8, x_17);
lean_dec(x_17);
if (x_18 == 0)
{
if (x_3 == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_19 = l_Lean_IR_EmitC_emitFnDeclAux___closed__1;
x_20 = lean_string_append(x_9, x_19);
x_21 = lean_box(0);
x_22 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_21, x_4, x_20);
return x_22;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_23 = l_Lean_IR_EmitC_emitFnDeclAux___closed__2;
x_24 = lean_string_append(x_9, x_23);
x_25 = lean_box(0);
x_26 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_25, x_4, x_24);
return x_26;
}
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_21 = l_Lean_IR_EmitC_emitFnDeclAux___closed__2;
x_22 = lean_string_append(x_9, x_21);
x_23 = lean_box(0);
x_24 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_23, x_4, x_22);
return x_24;
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_27 = l_Lean_IR_EmitC_emitFnDeclAux___closed__3;
x_28 = lean_string_append(x_9, x_27);
x_29 = lean_box(0);
x_30 = l_Lean_IR_EmitC_emitFnDeclAux___lambda__3(x_1, x_2, x_6, x_8, x_29, x_4, x_28);
return x_30;
}
}
}
@ -2332,7 +2356,7 @@ return x_6;
lean_object* l_Lean_IR_EmitC_emitExternDeclAux(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9;
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9; lean_object* x_10;
x_5 = l_Lean_IR_EmitC_getEnv(x_3, x_4);
x_6 = lean_ctor_get(x_5, 0);
lean_inc(x_6);
@ -2341,20 +2365,8 @@ lean_inc(x_7);
lean_dec(x_5);
x_8 = l_Lean_IR_Decl_name(x_1);
x_9 = l_Lean_isExternC(x_6, x_8);
if (x_9 == 0)
{
uint8_t x_10; lean_object* x_11;
x_10 = 1;
x_11 = l_Lean_IR_EmitC_emitFnDeclAux(x_1, x_2, x_10, x_3, x_7);
return x_11;
}
else
{
uint8_t x_12; lean_object* x_13;
x_12 = 0;
x_13 = l_Lean_IR_EmitC_emitFnDeclAux(x_1, x_2, x_12, x_3, x_7);
return x_13;
}
x_10 = l_Lean_IR_EmitC_emitFnDeclAux(x_1, x_2, x_9, x_3, x_7);
return x_10;
}
}
lean_object* l_List_foldl___at_Lean_IR_EmitC_emitFnDecls___spec__1(lean_object* x_1, lean_object* x_2) {
@ -11629,19 +11641,19 @@ lean_inc(x_10);
x_11 = l_Lean_hasInitAttr(x_5, x_10);
if (x_11 == 0)
{
uint8_t x_61;
x_61 = 0;
x_12 = x_61;
goto block_60;
uint8_t x_65;
x_65 = 0;
x_12 = x_65;
goto block_64;
}
else
{
uint8_t x_62;
x_62 = 1;
x_12 = x_62;
goto block_60;
uint8_t x_66;
x_66 = 1;
x_12 = x_66;
goto block_64;
}
block_60:
block_64:
{
if (x_12 == 0)
{
@ -11681,168 +11693,172 @@ x_24 = lean_nat_dec_eq(x_22, x_23);
lean_dec(x_22);
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26;
x_25 = lean_box(0);
x_26 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_20, x_25, x_2, x_21);
return x_26;
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_25 = l_Lean_IR_EmitC_emitFnDeclAux___closed__1;
x_26 = lean_string_append(x_21, x_25);
x_27 = lean_box(0);
x_28 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_20, x_27, x_2, x_26);
return x_28;
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_27 = l_Lean_IR_EmitC_emitFnDeclAux___closed__2;
x_28 = lean_string_append(x_21, x_27);
x_29 = lean_box(0);
x_30 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_20, x_29, x_2, x_28);
return x_30;
lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_29 = l_Lean_IR_EmitC_emitFnDeclAux___closed__3;
x_30 = lean_string_append(x_21, x_29);
x_31 = lean_box(0);
x_32 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_20, x_31, x_2, x_30);
return x_32;
}
}
else
{
uint8_t x_31;
uint8_t x_33;
lean_dec(x_2);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_10);
x_31 = !lean_is_exclusive(x_19);
if (x_31 == 0)
x_33 = !lean_is_exclusive(x_19);
if (x_33 == 0)
{
return x_19;
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34;
x_32 = lean_ctor_get(x_19, 0);
x_33 = lean_ctor_get(x_19, 1);
lean_inc(x_33);
lean_inc(x_32);
lean_object* x_34; lean_object* x_35; lean_object* x_36;
x_34 = lean_ctor_get(x_19, 0);
x_35 = lean_ctor_get(x_19, 1);
lean_inc(x_35);
lean_inc(x_34);
lean_dec(x_19);
x_34 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_34, 0, x_32);
lean_ctor_set(x_34, 1, x_33);
return x_34;
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_34);
lean_ctor_set(x_36, 1, x_35);
return x_36;
}
}
}
else
{
lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40;
x_35 = lean_ctor_get(x_2, 0);
x_36 = lean_ctor_get(x_2, 1);
x_37 = lean_ctor_get(x_2, 3);
x_38 = lean_ctor_get(x_2, 4);
lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42;
x_37 = lean_ctor_get(x_2, 0);
x_38 = lean_ctor_get(x_2, 1);
x_39 = lean_ctor_get(x_2, 3);
x_40 = lean_ctor_get(x_2, 4);
lean_inc(x_40);
lean_inc(x_39);
lean_inc(x_38);
lean_inc(x_37);
lean_inc(x_36);
lean_inc(x_35);
lean_dec(x_2);
x_39 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_39, 0, x_35);
lean_ctor_set(x_39, 1, x_36);
lean_ctor_set(x_39, 2, x_9);
lean_ctor_set(x_39, 3, x_37);
lean_ctor_set(x_39, 4, x_38);
x_41 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_41, 0, x_37);
lean_ctor_set(x_41, 1, x_38);
lean_ctor_set(x_41, 2, x_9);
lean_ctor_set(x_41, 3, x_39);
lean_ctor_set(x_41, 4, x_40);
lean_inc(x_13);
x_40 = l_Lean_IR_EmitC_toCName(x_13, x_39, x_6);
if (lean_obj_tag(x_40) == 0)
x_42 = l_Lean_IR_EmitC_toCName(x_13, x_41, x_6);
if (lean_obj_tag(x_42) == 0)
{
lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; uint8_t x_45;
x_41 = lean_ctor_get(x_40, 0);
lean_inc(x_41);
x_42 = lean_ctor_get(x_40, 1);
lean_inc(x_42);
lean_dec(x_40);
x_43 = lean_array_get_size(x_14);
x_44 = lean_unsigned_to_nat(0u);
x_45 = lean_nat_dec_eq(x_43, x_44);
lean_dec(x_43);
if (x_45 == 0)
{
lean_object* x_46; lean_object* x_47;
x_46 = lean_box(0);
x_47 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_41, x_46, x_39, x_42);
return x_47;
}
else
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; uint8_t x_47;
x_43 = lean_ctor_get(x_42, 0);
lean_inc(x_43);
x_44 = lean_ctor_get(x_42, 1);
lean_inc(x_44);
lean_dec(x_42);
x_45 = lean_array_get_size(x_14);
x_46 = lean_unsigned_to_nat(0u);
x_47 = lean_nat_dec_eq(x_45, x_46);
lean_dec(x_45);
if (x_47 == 0)
{
lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51;
x_48 = l_Lean_IR_EmitC_emitFnDeclAux___closed__2;
x_49 = lean_string_append(x_42, x_48);
x_48 = l_Lean_IR_EmitC_emitFnDeclAux___closed__1;
x_49 = lean_string_append(x_44, x_48);
x_50 = lean_box(0);
x_51 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_41, x_50, x_39, x_49);
x_51 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_43, x_50, x_41, x_49);
return x_51;
}
}
else
{
lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55;
lean_dec(x_39);
x_52 = l_Lean_IR_EmitC_emitFnDeclAux___closed__3;
x_53 = lean_string_append(x_44, x_52);
x_54 = lean_box(0);
x_55 = l_Lean_IR_EmitC_emitDeclAux___lambda__3(x_15, x_13, x_14, x_16, x_10, x_43, x_54, x_41, x_53);
return x_55;
}
}
else
{
lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59;
lean_dec(x_41);
lean_dec(x_16);
lean_dec(x_15);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_10);
x_52 = lean_ctor_get(x_40, 0);
lean_inc(x_52);
x_53 = lean_ctor_get(x_40, 1);
lean_inc(x_53);
if (lean_is_exclusive(x_40)) {
lean_ctor_release(x_40, 0);
lean_ctor_release(x_40, 1);
x_54 = x_40;
x_56 = lean_ctor_get(x_42, 0);
lean_inc(x_56);
x_57 = lean_ctor_get(x_42, 1);
lean_inc(x_57);
if (lean_is_exclusive(x_42)) {
lean_ctor_release(x_42, 0);
lean_ctor_release(x_42, 1);
x_58 = x_42;
} else {
lean_dec_ref(x_40);
x_54 = lean_box(0);
lean_dec_ref(x_42);
x_58 = lean_box(0);
}
if (lean_is_scalar(x_54)) {
x_55 = lean_alloc_ctor(1, 2, 0);
if (lean_is_scalar(x_58)) {
x_59 = lean_alloc_ctor(1, 2, 0);
} else {
x_55 = x_54;
x_59 = x_58;
}
lean_ctor_set(x_55, 0, x_52);
lean_ctor_set(x_55, 1, x_53);
return x_55;
}
}
}
else
{
lean_object* x_56; lean_object* x_57;
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_2);
lean_dec(x_1);
x_56 = lean_box(0);
if (lean_is_scalar(x_7)) {
x_57 = lean_alloc_ctor(0, 2, 0);
} else {
x_57 = x_7;
}
lean_ctor_set(x_57, 0, x_56);
lean_ctor_set(x_57, 1, x_6);
return x_57;
}
}
else
{
lean_object* x_58; lean_object* x_59;
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_2);
lean_dec(x_1);
x_58 = lean_box(0);
if (lean_is_scalar(x_7)) {
x_59 = lean_alloc_ctor(0, 2, 0);
} else {
x_59 = x_7;
}
lean_ctor_set(x_59, 0, x_58);
lean_ctor_set(x_59, 1, x_6);
lean_ctor_set(x_59, 0, x_56);
lean_ctor_set(x_59, 1, x_57);
return x_59;
}
}
}
else
{
lean_object* x_60; lean_object* x_61;
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_2);
lean_dec(x_1);
x_60 = lean_box(0);
if (lean_is_scalar(x_7)) {
x_61 = lean_alloc_ctor(0, 2, 0);
} else {
x_61 = x_7;
}
lean_ctor_set(x_61, 0, x_60);
lean_ctor_set(x_61, 1, x_6);
return x_61;
}
}
else
{
lean_object* x_62; lean_object* x_63;
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_2);
lean_dec(x_1);
x_62 = lean_box(0);
if (lean_is_scalar(x_7)) {
x_63 = lean_alloc_ctor(0, 2, 0);
} else {
x_63 = x_7;
}
lean_ctor_set(x_63, 0, x_62);
lean_ctor_set(x_63, 1, x_6);
return x_63;
}
}
}
}
lean_object* l_Nat_forM_loop___at_Lean_IR_EmitC_emitDeclAux___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
@ -12999,7 +13015,7 @@ static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("(lean_object* w) {");
x_1 = lean_mk_string("LEAN_EXPORT lean_object* ");
return x_1;
}
}
@ -13007,23 +13023,31 @@ static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("_G_initialized = true;");
x_1 = lean_mk_string("(lean_object* w) {");
return x_1;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("_G_initialized = true;");
return x_1;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_IR_EmitC_emitInitFn___closed__2;
x_2 = l_Lean_IR_EmitC_emitInitFn___closed__3;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__4() {
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__5() {
_start:
{
lean_object* x_1;
@ -13031,19 +13055,19 @@ x_1 = lean_mk_string("if (_G_initialized) return lean_io_result_mk_ok(lean_box(0
return x_1;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__5() {
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_IR_EmitC_emitInitFn___closed__4;
x_2 = l_Lean_IR_EmitC_emitInitFn___closed__3;
x_1 = l_Lean_IR_EmitC_emitInitFn___closed__5;
x_2 = l_Lean_IR_EmitC_emitInitFn___closed__4;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__6() {
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__7() {
_start:
{
lean_object* x_1;
@ -13051,19 +13075,19 @@ x_1 = lean_mk_string("lean_object * res;");
return x_1;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__7() {
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_IR_EmitC_emitInitFn___closed__6;
x_2 = l_Lean_IR_EmitC_emitInitFn___closed__5;
x_1 = l_Lean_IR_EmitC_emitInitFn___closed__7;
x_2 = l_Lean_IR_EmitC_emitInitFn___closed__6;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__8() {
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__9() {
_start:
{
lean_object* x_1;
@ -13071,7 +13095,7 @@ x_1 = lean_mk_string("static bool _G_initialized = false;");
return x_1;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__9() {
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__10() {
_start:
{
lean_object* x_1;
@ -13079,11 +13103,11 @@ x_1 = lean_mk_string("return lean_io_result_mk_ok(lean_box(0));");
return x_1;
}
}
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__10() {
static lean_object* _init_l_Lean_IR_EmitC_emitInitFn___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_IR_EmitC_emitInitFn___closed__9;
x_1 = l_Lean_IR_EmitC_emitInitFn___closed__10;
x_2 = l_Lean_IR_EmitC_emitMainFn___lambda__2___closed__14;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -13143,17 +13167,17 @@ block_65:
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25;
x_12 = lean_mk_module_initialization_function_name(x_7);
x_13 = l_Nat_forM_loop___at_Lean_IR_EmitC_emitDeclAux___spec__1___closed__1;
x_13 = l_Lean_IR_EmitC_emitInitFn___closed__1;
x_14 = lean_string_append(x_13, x_12);
lean_dec(x_12);
x_15 = l_Lean_IR_EmitC_emitInitFn___closed__1;
x_15 = l_Lean_IR_EmitC_emitInitFn___closed__2;
x_16 = lean_string_append(x_14, x_15);
x_17 = lean_box(0);
x_18 = l_Lean_IR_EmitC_emitInitFn___closed__7;
x_18 = l_Lean_IR_EmitC_emitInitFn___closed__8;
x_19 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_19, 0, x_16);
lean_ctor_set(x_19, 1, x_18);
x_20 = l_Lean_IR_EmitC_emitInitFn___closed__8;
x_20 = l_Lean_IR_EmitC_emitInitFn___closed__9;
x_21 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
@ -13181,7 +13205,7 @@ lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_30 = lean_ctor_get(x_29, 1);
lean_inc(x_30);
lean_dec(x_29);
x_31 = l_Lean_IR_EmitC_emitInitFn___closed__10;
x_31 = l_Lean_IR_EmitC_emitInitFn___closed__11;
x_32 = l_List_forM___at_Lean_IR_EmitC_emitMainFn___spec__3(x_31, x_1, x_30);
return x_32;
}
@ -13229,7 +13253,7 @@ lean_object* x_42; lean_object* x_43; lean_object* x_44;
x_42 = lean_ctor_get(x_41, 1);
lean_inc(x_42);
lean_dec(x_41);
x_43 = l_Lean_IR_EmitC_emitInitFn___closed__10;
x_43 = l_Lean_IR_EmitC_emitInitFn___closed__11;
x_44 = l_List_forM___at_Lean_IR_EmitC_emitMainFn___spec__3(x_43, x_1, x_42);
return x_44;
}
@ -13280,7 +13304,7 @@ lean_object* x_58; lean_object* x_59; lean_object* x_60;
x_58 = lean_ctor_get(x_57, 1);
lean_inc(x_58);
lean_dec(x_57);
x_59 = l_Lean_IR_EmitC_emitInitFn___closed__10;
x_59 = l_Lean_IR_EmitC_emitInitFn___closed__11;
x_60 = l_List_forM___at_Lean_IR_EmitC_emitMainFn___spec__3(x_59, x_1, x_58);
return x_60;
}
@ -13656,6 +13680,8 @@ l_Lean_IR_EmitC_emitFnDeclAux___closed__1 = _init_l_Lean_IR_EmitC_emitFnDeclAux_
lean_mark_persistent(l_Lean_IR_EmitC_emitFnDeclAux___closed__1);
l_Lean_IR_EmitC_emitFnDeclAux___closed__2 = _init_l_Lean_IR_EmitC_emitFnDeclAux___closed__2();
lean_mark_persistent(l_Lean_IR_EmitC_emitFnDeclAux___closed__2);
l_Lean_IR_EmitC_emitFnDeclAux___closed__3 = _init_l_Lean_IR_EmitC_emitFnDeclAux___closed__3();
lean_mark_persistent(l_Lean_IR_EmitC_emitFnDeclAux___closed__3);
l_List_forM___at_Lean_IR_EmitC_emitFnDecls___spec__5___closed__1 = _init_l_List_forM___at_Lean_IR_EmitC_emitFnDecls___spec__5___closed__1();
lean_mark_persistent(l_List_forM___at_Lean_IR_EmitC_emitFnDecls___spec__5___closed__1);
l_List_forM___at_Lean_IR_EmitC_emitFnDecls___spec__5___closed__2 = _init_l_List_forM___at_Lean_IR_EmitC_emitFnDecls___spec__5___closed__2();
@ -14068,6 +14094,8 @@ l_Lean_IR_EmitC_emitInitFn___closed__9 = _init_l_Lean_IR_EmitC_emitInitFn___clos
lean_mark_persistent(l_Lean_IR_EmitC_emitInitFn___closed__9);
l_Lean_IR_EmitC_emitInitFn___closed__10 = _init_l_Lean_IR_EmitC_emitInitFn___closed__10();
lean_mark_persistent(l_Lean_IR_EmitC_emitInitFn___closed__10);
l_Lean_IR_EmitC_emitInitFn___closed__11 = _init_l_Lean_IR_EmitC_emitInitFn___closed__11();
lean_mark_persistent(l_Lean_IR_EmitC_emitInitFn___closed__11);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus