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:
Lean stage0 autoupdater 2025-08-15 12:21:02 +00:00
parent 415a58f9fb
commit 4c562fc1a3
20 changed files with 19475 additions and 10724 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/CMakeLists.txt generated
View file

@ -10,7 +10,7 @@ endif()
include(ExternalProject)
project(LEAN CXX C)
set(LEAN_VERSION_MAJOR 4)
set(LEAN_VERSION_MINOR 23)
set(LEAN_VERSION_MINOR 24)
set(LEAN_VERSION_PATCH 0)
set(LEAN_VERSION_IS_RELEASE 0) # This number is 1 in the release revision, and 0 otherwise.
set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")

2899
stage0/stdlib/Init/NotationExtra.c generated
View file

File diff suppressed because it is too large Load diff

10
stage0/stdlib/Lean/Compiler/LCNF/CSE.c generated
View file

@ -232,6 +232,7 @@ LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAtAux___at___Lean_Persiste
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_CSE_addEntry(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* l_Lean_Expr_hash___boxed(lean_object*);
lean_object* l_Lean_Compiler_LCNF_normFVarImp(lean_object*, lean_object*, uint8_t);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_mkStr1(lean_object*);
size_t lean_usize_shift_left(size_t, size_t);
@ -239,7 +240,6 @@ lean_object* l_Lean_Core_instMonadCoreM___lam__1(lean_object*, lean_object*, lea
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_CSE_replaceFun___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAtCollisionNode___at___Lean_PersistentHashMap_insertAux___at___Lean_PersistentHashMap_insert___at_____private_Lean_Compiler_LCNF_CSE_0__Lean_Compiler_LCNF_Code_cse_go_spec__4_spec__4_spec__4___redArg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(lean_object*, lean_object*, uint8_t);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_AssocList_replace___at___Lean_Compiler_LCNF_CSE_replaceLet_spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
@ -4895,7 +4895,7 @@ lean_inc_ref(x_237);
lean_dec(x_235);
x_238 = 0;
lean_inc(x_232);
x_239 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_237, x_232, x_238);
x_239 = l_Lean_Compiler_LCNF_normFVarImp(x_237, x_232, x_238);
lean_dec_ref(x_237);
if (lean_obj_tag(x_239) == 0)
{
@ -5031,7 +5031,7 @@ lean_inc_ref(x_268);
lean_dec(x_261);
x_269 = 0;
lean_inc(x_265);
x_270 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_268, x_265, x_269);
x_270 = l_Lean_Compiler_LCNF_normFVarImp(x_268, x_265, x_269);
lean_dec_ref(x_268);
if (lean_obj_tag(x_270) == 0)
{
@ -5234,7 +5234,7 @@ lean_inc_ref(x_308);
lean_dec(x_306);
x_309 = 0;
lean_inc(x_303);
x_310 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_308, x_303, x_309);
x_310 = l_Lean_Compiler_LCNF_normFVarImp(x_308, x_303, x_309);
lean_dec_ref(x_308);
if (lean_obj_tag(x_310) == 0)
{
@ -5295,7 +5295,7 @@ lean_inc_ref(x_319);
lean_dec(x_317);
x_320 = 0;
lean_inc(x_303);
x_321 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_319, x_303, x_320);
x_321 = l_Lean_Compiler_LCNF_normFVarImp(x_319, x_303, x_320);
lean_dec_ref(x_319);
if (lean_obj_tag(x_321) == 0)
{

22
stage0/stdlib/Lean/Compiler/LCNF/CompilerM.c generated
View file

@ -278,7 +278,6 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at___Lean_Compiler_LCNF_getType_spe
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_CompilerM_run___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_updateFunDeclImp___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_LCNF_CacheExtension_insert___redArg___closed__2;
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseParam___redArg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_LCNF_LCtx_addFunDecl(lean_object*, lean_object*);
@ -429,11 +428,13 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_replaceExprFVars___boxed(lean_obje
lean_object* l_Lean_Compiler_LCNF_LCtx_eraseParams(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_mkFreshFVarId___at___Lean_Compiler_LCNF_mkParam_spec__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_CacheExtension_insert___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normFVarImp___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_getLetDecl___redArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normLetDecl___at___Lean_Compiler_LCNF_normCodeImp_spec__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* l_Lean_Expr_fvar___override(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normCode___redArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normFVarImp(lean_object*, lean_object*, uint8_t);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_ensureNotAnonymous___redArg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_mkStr1(lean_object*);
@ -458,7 +459,6 @@ lean_object* lean_array_get_size(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_isConstructorApp___redArg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_LCNF_CompilerM_instInhabitedState___closed__5;
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normExpr___redArg___lam__0(uint8_t, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(lean_object*, lean_object*, uint8_t);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_findParam_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_mkAuxParam(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -5282,7 +5282,7 @@ x_1 = l_Lean_Compiler_LCNF_instInhabitedNormFVarResult___closed__0;
return x_1;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(lean_object* x_1, lean_object* x_2, uint8_t x_3) {
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normFVarImp(lean_object* x_1, lean_object* x_2, uint8_t x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; uint64_t x_6; uint64_t x_7; uint64_t x_8; uint64_t x_9; uint64_t x_10; uint64_t x_11; uint64_t x_12; size_t x_13; size_t x_14; size_t x_15; size_t x_16; size_t x_17; lean_object* x_18; lean_object* x_19;
@ -5360,12 +5360,12 @@ return x_27;
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normFVarImp___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = lean_unbox(x_3);
x_5 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_1, x_2, x_4);
x_5 = l_Lean_Compiler_LCNF_normFVarImp(x_1, x_2, x_4);
lean_dec_ref(x_1);
return x_5;
}
@ -5534,7 +5534,7 @@ case 2:
lean_object* x_4; lean_object* x_5;
x_4 = lean_ctor_get(x_2, 2);
lean_inc(x_4);
x_5 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_1, x_4, x_3);
x_5 = l_Lean_Compiler_LCNF_normFVarImp(x_1, x_4, x_3);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_6; lean_object* x_7;
@ -5567,7 +5567,7 @@ lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = lean_ctor_get(x_2, 0);
x_13 = lean_ctor_get(x_2, 1);
lean_inc(x_12);
x_14 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_1, x_12, x_3);
x_14 = l_Lean_Compiler_LCNF_normFVarImp(x_1, x_12, x_3);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
@ -6063,7 +6063,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normFVar___redArg___lam__0(lean_ob
_start:
{
lean_object* x_5; lean_object* x_6;
x_5 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_4, x_1, x_2);
x_5 = l_Lean_Compiler_LCNF_normFVarImp(x_4, x_1, x_2);
x_6 = lean_apply_2(x_3, lean_box(0), x_5);
return x_6;
}
@ -9656,7 +9656,7 @@ lean_object* x_99; lean_object* x_100; lean_object* x_101;
x_99 = lean_ctor_get(x_2, 0);
x_100 = lean_ctor_get(x_2, 1);
lean_inc(x_99);
x_101 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_3, x_99, x_1);
x_101 = l_Lean_Compiler_LCNF_normFVarImp(x_3, x_99, x_1);
if (lean_obj_tag(x_101) == 0)
{
lean_object* x_102; lean_object* x_103;
@ -9815,7 +9815,7 @@ if (lean_is_exclusive(x_125)) {
x_130 = lean_box(0);
}
lean_inc(x_128);
x_131 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_3, x_128, x_1);
x_131 = l_Lean_Compiler_LCNF_normFVarImp(x_3, x_128, x_1);
if (lean_obj_tag(x_131) == 0)
{
lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135;
@ -9991,7 +9991,7 @@ lean_object* x_159; lean_object* x_160;
lean_dec_ref(x_70);
x_159 = lean_ctor_get(x_2, 0);
lean_inc(x_159);
x_160 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_3, x_159, x_1);
x_160 = l_Lean_Compiler_LCNF_normFVarImp(x_3, x_159, x_1);
lean_dec_ref(x_3);
if (lean_obj_tag(x_160) == 0)
{

85
stage0/stdlib/Lean/Compiler/LCNF/ExtractClosed.c generated
View file

@ -1930,6 +1930,11 @@ x_10 = lean_usize_dec_lt(x_2, x_1);
if (x_10 == 0)
{
lean_object* x_11;
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_3);
lean_ctor_set(x_11, 1, x_9);
@ -1939,6 +1944,11 @@ else
{
lean_object* x_12; lean_object* x_13;
x_12 = lean_array_uget(x_3, x_2);
lean_inc(x_8);
lean_inc_ref(x_7);
lean_inc(x_6);
lean_inc_ref(x_5);
lean_inc(x_4);
x_13 = l_Lean_Compiler_LCNF_Internalize_internalizeCodeDecl(x_12, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_13) == 0)
{
@ -1961,6 +1971,11 @@ goto _start;
else
{
uint8_t x_22;
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
lean_dec_ref(x_3);
x_22 = !lean_is_exclusive(x_13);
if (x_22 == 0)
@ -2126,6 +2141,10 @@ x_11 = lean_usize_dec_lt(x_2, x_1);
if (x_11 == 0)
{
lean_object* x_12;
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec_ref(x_4);
x_12 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_12, 0, x_3);
@ -2157,6 +2176,10 @@ goto block_29;
block_29:
{
lean_object* x_17;
lean_inc(x_9);
lean_inc_ref(x_8);
lean_inc(x_7);
lean_inc_ref(x_6);
lean_inc_ref(x_4);
x_17 = l_Lean_Compiler_LCNF_ExtractClosed_visitCode(x_16, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_17) == 0)
@ -2181,6 +2204,10 @@ else
uint8_t x_25;
lean_dec_ref(x_15);
lean_dec(x_13);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec_ref(x_4);
x_25 = !lean_is_exclusive(x_17);
if (x_25 == 0)
@ -2512,6 +2539,11 @@ lean_ctor_set(x_155, 0, x_85);
x_156 = lean_array_push(x_154, x_155);
x_157 = lean_array_size(x_156);
x_158 = 0;
lean_inc(x_7);
lean_inc_ref(x_6);
lean_inc(x_5);
lean_inc_ref(x_4);
lean_inc(x_152);
x_159 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at___Lean_Compiler_LCNF_ExtractClosed_visitCode_spec__1(x_157, x_158, x_156, x_152, x_4, x_5, x_6, x_7, x_153);
if (lean_obj_tag(x_159) == 0)
{
@ -2620,6 +2652,10 @@ else
uint8_t x_200;
lean_dec_ref(x_191);
lean_dec(x_183);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec(x_5);
lean_dec_ref(x_4);
lean_dec_ref(x_2);
lean_dec_ref(x_1);
x_200 = !lean_is_exclusive(x_192);
@ -2672,6 +2708,10 @@ else
{
uint8_t x_207;
lean_dec(x_204);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec(x_5);
lean_dec_ref(x_4);
lean_dec_ref(x_2);
lean_dec_ref(x_1);
x_207 = !lean_is_exclusive(x_205);
@ -2699,6 +2739,10 @@ else
{
uint8_t x_211;
lean_dec(x_152);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec(x_5);
lean_dec_ref(x_4);
lean_dec_ref(x_2);
lean_dec_ref(x_1);
x_211 = !lean_is_exclusive(x_159);
@ -2725,6 +2769,10 @@ else
{
uint8_t x_215;
lean_dec(x_143);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec(x_5);
lean_dec_ref(x_4);
lean_dec_ref(x_2);
lean_dec_ref(x_1);
x_215 = !lean_is_exclusive(x_145);
@ -2751,6 +2799,10 @@ return x_218;
else
{
uint8_t x_219;
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec(x_5);
lean_dec_ref(x_4);
lean_dec_ref(x_2);
lean_dec_ref(x_1);
x_219 = !lean_is_exclusive(x_118);
@ -2835,6 +2887,10 @@ return x_101;
else
{
uint8_t x_110;
lean_dec(x_93);
lean_dec_ref(x_92);
lean_dec(x_91);
lean_dec_ref(x_90);
lean_dec_ref(x_88);
lean_dec_ref(x_1);
x_110 = !lean_is_exclusive(x_98);
@ -3152,6 +3208,10 @@ return x_278;
default:
{
lean_object* x_279;
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec(x_5);
lean_dec_ref(x_4);
lean_dec_ref(x_2);
x_279 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_279, 0, x_1);
@ -3242,6 +3302,10 @@ lean_inc_ref(x_42);
x_43 = lean_ctor_get(x_33, 3);
lean_inc_ref(x_43);
x_44 = lean_ctor_get(x_33, 4);
lean_inc(x_40);
lean_inc_ref(x_39);
lean_inc(x_38);
lean_inc_ref(x_37);
lean_inc_ref(x_35);
lean_inc_ref(x_44);
x_45 = l_Lean_Compiler_LCNF_ExtractClosed_visitCode(x_44, x_35, x_36, x_37, x_38, x_39, x_40, x_41);
@ -3376,6 +3440,10 @@ return x_51;
else
{
uint8_t x_80;
lean_dec(x_40);
lean_dec_ref(x_39);
lean_dec(x_38);
lean_dec_ref(x_37);
lean_dec_ref(x_35);
lean_dec_ref(x_34);
lean_dec_ref(x_1);
@ -3403,6 +3471,10 @@ else
{
lean_dec_ref(x_43);
lean_dec_ref(x_42);
lean_dec(x_40);
lean_dec_ref(x_39);
lean_dec(x_38);
lean_dec_ref(x_37);
lean_dec_ref(x_35);
lean_dec_ref(x_34);
lean_dec_ref(x_33);
@ -3421,11 +3493,6 @@ lean_dec(x_1);
x_11 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_12 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at___Lean_Compiler_LCNF_ExtractClosed_visitCode_spec__1(x_10, x_11, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
return x_12;
}
}
@ -3461,10 +3528,6 @@ lean_dec(x_1);
x_12 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_13 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at___Lean_Compiler_LCNF_ExtractClosed_visitCode_spec__3(x_11, x_12, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec(x_5);
return x_13;
}
@ -3474,10 +3537,6 @@ _start:
{
lean_object* x_9;
x_9 = l_Lean_Compiler_LCNF_ExtractClosed_visitCode(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec(x_5);
lean_dec_ref(x_4);
lean_dec(x_3);
return x_9;
}

7126
stage0/stdlib/Lean/Compiler/LCNF/Internalize.c generated
View file

File diff suppressed because it is too large Load diff

66
stage0/stdlib/Lean/Compiler/LCNF/LambdaLifting.c generated
View file

@ -705,6 +705,11 @@ x_10 = lean_usize_dec_lt(x_2, x_1);
if (x_10 == 0)
{
lean_object* x_11;
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_3);
lean_ctor_set(x_11, 1, x_9);
@ -714,6 +719,11 @@ else
{
lean_object* x_12; lean_object* x_13;
x_12 = lean_array_uget(x_3, x_2);
lean_inc(x_8);
lean_inc_ref(x_7);
lean_inc(x_6);
lean_inc_ref(x_5);
lean_inc(x_4);
x_13 = l_Lean_Compiler_LCNF_Internalize_internalizeParam(x_12, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_13) == 0)
{
@ -736,6 +746,11 @@ goto _start;
else
{
uint8_t x_22;
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
lean_dec_ref(x_3);
x_22 = !lean_is_exclusive(x_13);
if (x_22 == 0)
@ -765,6 +780,11 @@ _start:
size_t x_12; size_t x_13; lean_object* x_14;
x_12 = lean_array_size(x_1);
x_13 = 0;
lean_inc(x_10);
lean_inc_ref(x_9);
lean_inc(x_8);
lean_inc_ref(x_7);
lean_inc(x_6);
x_14 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at_____private_Lean_Compiler_LCNF_LambdaLifting_0__Lean_Compiler_LCNF_LambdaLifting_mkAuxDecl_go_spec__0(x_12, x_13, x_1, x_6, x_7, x_8, x_9, x_10, x_11);
if (lean_obj_tag(x_14) == 0)
{
@ -780,6 +800,11 @@ x_18 = lean_ctor_get(x_2, 4);
lean_inc_ref(x_18);
lean_dec_ref(x_2);
x_19 = lean_array_size(x_17);
lean_inc(x_10);
lean_inc_ref(x_9);
lean_inc(x_8);
lean_inc_ref(x_7);
lean_inc(x_6);
x_20 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at_____private_Lean_Compiler_LCNF_LambdaLifting_0__Lean_Compiler_LCNF_LambdaLifting_mkAuxDecl_go_spec__0(x_19, x_13, x_17, x_6, x_7, x_8, x_9, x_10, x_16);
if (lean_obj_tag(x_20) == 0)
{
@ -789,6 +814,10 @@ lean_inc(x_21);
x_22 = lean_ctor_get(x_20, 1);
lean_inc(x_22);
lean_dec_ref(x_20);
lean_inc(x_10);
lean_inc_ref(x_9);
lean_inc(x_8);
lean_inc_ref(x_7);
x_23 = l_Lean_Compiler_LCNF_Internalize_internalizeCode(x_18, x_6, x_7, x_8, x_9, x_10, x_22);
if (lean_obj_tag(x_23) == 0)
{
@ -812,6 +841,10 @@ x_29 = l_Array_append___redArg(x_15, x_21);
lean_dec(x_21);
lean_inc_ref(x_29);
x_30 = l_Lean_Compiler_LCNF_InferType_mkForallParams___redArg(x_29, x_27, x_7, x_8, x_9, x_10, x_28);
lean_dec(x_10);
lean_dec_ref(x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_27);
if (lean_obj_tag(x_30) == 0)
{
@ -899,6 +932,10 @@ uint8_t x_50;
lean_dec(x_24);
lean_dec(x_21);
lean_dec(x_15);
lean_dec(x_10);
lean_dec_ref(x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_5);
lean_dec(x_3);
x_50 = !lean_is_exclusive(x_26);
@ -926,6 +963,10 @@ else
uint8_t x_54;
lean_dec(x_21);
lean_dec(x_15);
lean_dec(x_10);
lean_dec_ref(x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_5);
lean_dec(x_3);
x_54 = !lean_is_exclusive(x_23);
@ -953,6 +994,11 @@ else
uint8_t x_58;
lean_dec_ref(x_18);
lean_dec(x_15);
lean_dec(x_10);
lean_dec_ref(x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
x_58 = !lean_is_exclusive(x_20);
@ -978,6 +1024,11 @@ return x_61;
else
{
uint8_t x_62;
lean_dec(x_10);
lean_dec_ref(x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
lean_dec_ref(x_2);
@ -1011,11 +1062,6 @@ lean_dec(x_1);
x_11 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_12 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at_____private_Lean_Compiler_LCNF_LambdaLifting_0__Lean_Compiler_LCNF_LambdaLifting_mkAuxDecl_go_spec__0(x_10, x_11, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
return x_12;
}
}
@ -1025,11 +1071,6 @@ _start:
uint8_t x_12; lean_object* x_13;
x_12 = lean_unbox(x_4);
x_13 = l___private_Lean_Compiler_LCNF_LambdaLifting_0__Lean_Compiler_LCNF_LambdaLifting_mkAuxDecl_go(x_1, x_2, x_3, x_12, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
lean_dec(x_10);
lean_dec_ref(x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
return x_13;
}
}
@ -1222,6 +1263,11 @@ lean_inc(x_80);
lean_dec_ref(x_77);
x_81 = lean_ctor_get_uint8(x_78, sizeof(void*)*6 + 1);
lean_dec_ref(x_78);
lean_inc(x_73);
lean_inc_ref(x_72);
lean_inc(x_71);
lean_inc_ref(x_70);
lean_inc(x_79);
lean_inc_ref(x_2);
lean_inc_ref(x_1);
x_82 = l___private_Lean_Compiler_LCNF_LambdaLifting_0__Lean_Compiler_LCNF_LambdaLifting_mkAuxDecl_go(x_1, x_2, x_65, x_81, x_67, x_79, x_70, x_71, x_72, x_73, x_80);

4
stage0/stdlib/Lean/Compiler/LCNF/PrettyPrinter.c generated
View file

@ -6590,6 +6590,10 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_ppCode_x27___lam__0(lean_object* x
_start:
{
lean_object* x_8;
lean_inc(x_6);
lean_inc_ref(x_5);
lean_inc(x_4);
lean_inc_ref(x_3);
x_8 = l_Lean_Compiler_LCNF_Code_internalize(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
if (lean_obj_tag(x_8) == 0)
{

35
stage0/stdlib/Lean/Compiler/LCNF/ReduceArity.c generated
View file

@ -4399,6 +4399,11 @@ x_10 = lean_usize_dec_lt(x_2, x_1);
if (x_10 == 0)
{
lean_object* x_11;
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_3);
lean_ctor_set(x_11, 1, x_9);
@ -4408,6 +4413,11 @@ else
{
lean_object* x_12; lean_object* x_13;
x_12 = lean_array_uget(x_3, x_2);
lean_inc(x_8);
lean_inc_ref(x_7);
lean_inc(x_6);
lean_inc_ref(x_5);
lean_inc(x_4);
x_13 = l_Lean_Compiler_LCNF_Internalize_internalizeParam(x_12, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_13) == 0)
{
@ -4430,6 +4440,11 @@ goto _start;
else
{
uint8_t x_22;
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
lean_dec_ref(x_3);
x_22 = !lean_is_exclusive(x_13);
if (x_22 == 0)
@ -6281,6 +6296,11 @@ if (x_49 == 0)
lean_object* x_50; lean_object* x_51; lean_object* x_52;
x_50 = lean_ctor_get(x_48, 0);
x_51 = lean_ctor_get(x_48, 1);
lean_inc(x_21);
lean_inc_ref(x_24);
lean_inc(x_28);
lean_inc_ref(x_27);
lean_inc(x_50);
x_52 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at___Lean_Compiler_LCNF_Decl_reduceArity_spec__3(x_26, x_22, x_11, x_50, x_27, x_28, x_24, x_21, x_51);
if (lean_obj_tag(x_52) == 0)
{
@ -6699,6 +6719,11 @@ x_140 = lean_ctor_get(x_48, 1);
lean_inc(x_140);
lean_inc(x_139);
lean_dec(x_48);
lean_inc(x_21);
lean_inc_ref(x_24);
lean_inc(x_28);
lean_inc_ref(x_27);
lean_inc(x_139);
x_141 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at___Lean_Compiler_LCNF_Decl_reduceArity_spec__3(x_26, x_22, x_11, x_139, x_27, x_28, x_24, x_21, x_140);
if (lean_obj_tag(x_141) == 0)
{
@ -7168,6 +7193,11 @@ if (lean_is_exclusive(x_221)) {
lean_dec_ref(x_221);
x_224 = lean_box(0);
}
lean_inc(x_21);
lean_inc_ref(x_24);
lean_inc(x_28);
lean_inc_ref(x_27);
lean_inc(x_222);
x_225 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at___Lean_Compiler_LCNF_Decl_reduceArity_spec__3(x_26, x_22, x_11, x_222, x_27, x_28, x_24, x_21, x_223);
if (lean_obj_tag(x_225) == 0)
{
@ -7630,11 +7660,6 @@ lean_dec(x_1);
x_11 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_12 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at___Lean_Compiler_LCNF_Decl_reduceArity_spec__3(x_10, x_11, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
return x_12;
}
}

4
stage0/stdlib/Lean/Compiler/LCNF/Simp/InlineProj.c generated
View file

@ -1631,6 +1631,10 @@ lean_object* x_61; lean_object* x_62; lean_object* x_63;
lean_inc(x_33);
x_61 = l_Lean_Compiler_LCNF_Decl_instantiateParamsLevelParams(x_52, x_33);
x_62 = l___private_Lean_Compiler_LCNF_Basic_0__Lean_Compiler_LCNF_Code_instantiateValueLevelParams_instCode(x_56, x_33, x_57);
lean_inc(x_42);
lean_inc_ref(x_41);
lean_inc(x_40);
lean_inc_ref(x_39);
x_63 = l_Lean_Compiler_LCNF_Simp_betaReduce(x_61, x_62, x_34, x_60, x_36, x_37, x_38, x_39, x_40, x_41, x_42, x_55);
lean_dec_ref(x_61);
if (lean_obj_tag(x_63) == 0)

230
stage0/stdlib/Lean/Compiler/LCNF/Simp/JpCases.c generated
View file

@ -189,7 +189,6 @@ lean_object* lean_panic_fn(lean_object*, lean_object*);
uint8_t l___private_Lean_Compiler_LCNF_DependsOn_0__Lean_Compiler_LCNF_depOn(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_x27_loop___at___List_forIn_x27_loop___at___Lean_Compiler_LCNF_Simp_simpJpCases_x3f_spec__4_spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_reverse___redArg(lean_object*);
LEAN_EXPORT lean_object* l_Std_PRange_RangeIterator_instIteratorLoop_loop___at___Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__2_spec__2___redArg___lam__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
extern lean_object* l_Lean_Compiler_LCNF_instInhabitedParam;
lean_object* l_Array_append___redArg(lean_object*, lean_object*);
@ -1920,6 +1919,11 @@ x_10 = lean_usize_dec_lt(x_2, x_1);
if (x_10 == 0)
{
lean_object* x_11;
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_3);
lean_ctor_set(x_11, 1, x_9);
@ -1929,6 +1933,11 @@ else
{
lean_object* x_12; lean_object* x_13;
x_12 = lean_array_uget(x_3, x_2);
lean_inc(x_8);
lean_inc_ref(x_7);
lean_inc(x_6);
lean_inc_ref(x_5);
lean_inc(x_4);
x_13 = l_Lean_Compiler_LCNF_Internalize_internalizeParam(x_12, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_13) == 0)
{
@ -1951,6 +1960,11 @@ goto _start;
else
{
uint8_t x_22;
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
lean_dec_ref(x_3);
x_22 = !lean_is_exclusive(x_13);
if (x_22 == 0)
@ -1982,6 +1996,11 @@ x_10 = lean_usize_dec_lt(x_2, x_1);
if (x_10 == 0)
{
lean_object* x_11;
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_3);
lean_ctor_set(x_11, 1, x_9);
@ -1991,6 +2010,11 @@ else
{
lean_object* x_12; lean_object* x_13;
x_12 = lean_array_uget(x_3, x_2);
lean_inc(x_8);
lean_inc_ref(x_7);
lean_inc(x_6);
lean_inc_ref(x_5);
lean_inc(x_4);
x_13 = l_Lean_Compiler_LCNF_Internalize_internalizeCodeDecl(x_12, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_13) == 0)
{
@ -2013,6 +2037,11 @@ goto _start;
else
{
uint8_t x_22;
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
lean_dec_ref(x_3);
x_22 = !lean_is_exclusive(x_13);
if (x_22 == 0)
@ -2110,6 +2139,11 @@ x_39 = lean_nat_dec_eq(x_2, x_8);
if (x_39 == 0)
{
lean_object* x_40;
lean_inc(x_13);
lean_inc_ref(x_12);
lean_inc(x_11);
lean_inc_ref(x_10);
lean_inc(x_9);
lean_inc_ref(x_38);
x_40 = l_Lean_Compiler_LCNF_Internalize_internalizeParam(x_38, x_9, x_10, x_11, x_12, x_13, x_14);
if (lean_obj_tag(x_40) == 0)
@ -2128,6 +2162,11 @@ goto block_22;
else
{
uint8_t x_44;
lean_dec(x_13);
lean_dec_ref(x_12);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec_ref(x_4);
@ -2156,6 +2195,11 @@ else
if (x_3 == 0)
{
lean_object* x_48;
lean_inc(x_13);
lean_inc_ref(x_12);
lean_inc(x_11);
lean_inc_ref(x_10);
lean_inc(x_9);
lean_inc_ref(x_4);
x_48 = l_Std_PRange_RangeIterator_instIteratorLoop_loop___at___Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__2_spec__2___redArg___lam__0(x_4, x_7, x_5, x_9, x_10, x_11, x_12, x_13, x_14);
x_23 = x_48;
@ -2164,6 +2208,11 @@ goto block_37;
else
{
lean_object* x_49;
lean_inc(x_13);
lean_inc_ref(x_12);
lean_inc(x_11);
lean_inc_ref(x_10);
lean_inc(x_9);
lean_inc_ref(x_38);
x_49 = l_Lean_Compiler_LCNF_Internalize_internalizeParam(x_38, x_9, x_10, x_11, x_12, x_13, x_14);
if (lean_obj_tag(x_49) == 0)
@ -2175,6 +2224,11 @@ x_51 = lean_ctor_get(x_49, 1);
lean_inc(x_51);
lean_dec_ref(x_49);
x_52 = lean_array_push(x_7, x_50);
lean_inc(x_13);
lean_inc_ref(x_12);
lean_inc(x_11);
lean_inc_ref(x_10);
lean_inc(x_9);
lean_inc_ref(x_4);
x_53 = l_Std_PRange_RangeIterator_instIteratorLoop_loop___at___Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__2_spec__2___redArg___lam__0(x_4, x_52, x_5, x_9, x_10, x_11, x_12, x_13, x_51);
x_23 = x_53;
@ -2183,6 +2237,11 @@ goto block_37;
else
{
uint8_t x_54;
lean_dec(x_13);
lean_dec_ref(x_12);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec_ref(x_4);
@ -2218,6 +2277,11 @@ if (x_19 == 0)
{
lean_object* x_20;
lean_dec(x_18);
lean_dec(x_13);
lean_dec_ref(x_12);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_4);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_15);
@ -2242,6 +2306,11 @@ lean_inc(x_24);
if (lean_obj_tag(x_24) == 0)
{
uint8_t x_25;
lean_dec(x_13);
lean_dec_ref(x_12);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec_ref(x_4);
x_25 = !lean_is_exclusive(x_23);
@ -2288,6 +2357,11 @@ goto block_22;
else
{
uint8_t x_33;
lean_dec(x_13);
lean_dec_ref(x_12);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec_ref(x_4);
x_33 = !lean_is_exclusive(x_23);
@ -2329,6 +2403,11 @@ x_41 = lean_nat_dec_eq(x_2, x_10);
if (x_41 == 0)
{
lean_object* x_42;
lean_inc(x_15);
lean_inc_ref(x_14);
lean_inc(x_13);
lean_inc_ref(x_12);
lean_inc(x_11);
lean_inc_ref(x_40);
x_42 = l_Lean_Compiler_LCNF_Internalize_internalizeParam(x_40, x_11, x_12, x_13, x_14, x_15, x_16);
if (lean_obj_tag(x_42) == 0)
@ -2347,6 +2426,11 @@ goto block_24;
else
{
uint8_t x_46;
lean_dec(x_15);
lean_dec_ref(x_14);
lean_dec(x_13);
lean_dec_ref(x_12);
lean_dec(x_11);
lean_dec_ref(x_9);
lean_dec_ref(x_4);
x_46 = !lean_is_exclusive(x_42);
@ -2374,6 +2458,11 @@ else
if (x_3 == 0)
{
lean_object* x_50;
lean_inc(x_15);
lean_inc_ref(x_14);
lean_inc(x_13);
lean_inc_ref(x_12);
lean_inc(x_11);
lean_inc_ref(x_4);
x_50 = l_Std_PRange_RangeIterator_instIteratorLoop_loop___at___Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__2_spec__2___redArg___lam__0(x_4, x_9, x_5, x_11, x_12, x_13, x_14, x_15, x_16);
x_25 = x_50;
@ -2382,6 +2471,11 @@ goto block_39;
else
{
lean_object* x_51;
lean_inc(x_15);
lean_inc_ref(x_14);
lean_inc(x_13);
lean_inc_ref(x_12);
lean_inc(x_11);
lean_inc_ref(x_40);
x_51 = l_Lean_Compiler_LCNF_Internalize_internalizeParam(x_40, x_11, x_12, x_13, x_14, x_15, x_16);
if (lean_obj_tag(x_51) == 0)
@ -2393,6 +2487,11 @@ x_53 = lean_ctor_get(x_51, 1);
lean_inc(x_53);
lean_dec_ref(x_51);
x_54 = lean_array_push(x_9, x_52);
lean_inc(x_15);
lean_inc_ref(x_14);
lean_inc(x_13);
lean_inc_ref(x_12);
lean_inc(x_11);
lean_inc_ref(x_4);
x_55 = l_Std_PRange_RangeIterator_instIteratorLoop_loop___at___Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__2_spec__2___redArg___lam__0(x_4, x_54, x_5, x_11, x_12, x_13, x_14, x_15, x_53);
x_25 = x_55;
@ -2401,6 +2500,11 @@ goto block_39;
else
{
uint8_t x_56;
lean_dec(x_15);
lean_dec_ref(x_14);
lean_dec(x_13);
lean_dec_ref(x_12);
lean_dec(x_11);
lean_dec_ref(x_9);
lean_dec_ref(x_4);
x_56 = !lean_is_exclusive(x_51);
@ -2434,6 +2538,11 @@ if (x_21 == 0)
{
lean_object* x_22;
lean_dec(x_20);
lean_dec(x_15);
lean_dec_ref(x_14);
lean_dec(x_13);
lean_dec_ref(x_12);
lean_dec(x_11);
lean_dec_ref(x_4);
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_17);
@ -2457,6 +2566,11 @@ lean_inc(x_26);
if (lean_obj_tag(x_26) == 0)
{
uint8_t x_27;
lean_dec(x_15);
lean_dec_ref(x_14);
lean_dec(x_13);
lean_dec_ref(x_12);
lean_dec(x_11);
lean_dec_ref(x_4);
x_27 = !lean_is_exclusive(x_25);
if (x_27 == 0)
@ -2502,6 +2616,11 @@ goto block_24;
else
{
uint8_t x_35;
lean_dec(x_15);
lean_dec_ref(x_14);
lean_dec(x_13);
lean_dec_ref(x_12);
lean_dec(x_11);
lean_dec_ref(x_4);
x_35 = !lean_is_exclusive(x_25);
if (x_35 == 0)
@ -2649,6 +2768,11 @@ block_46:
size_t x_16; size_t x_17; lean_object* x_18;
x_16 = lean_array_size(x_1);
x_17 = 0;
lean_inc(x_11);
lean_inc_ref(x_10);
lean_inc(x_9);
lean_inc_ref(x_8);
lean_inc(x_7);
x_18 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__1(x_16, x_17, x_1, x_7, x_8, x_9, x_10, x_11, x_15);
if (lean_obj_tag(x_18) == 0)
{
@ -2658,6 +2782,10 @@ lean_inc(x_19);
x_20 = lean_ctor_get(x_18, 1);
lean_inc(x_20);
lean_dec_ref(x_18);
lean_inc(x_11);
lean_inc_ref(x_10);
lean_inc(x_9);
lean_inc_ref(x_8);
x_21 = l_Lean_Compiler_LCNF_Internalize_internalizeCode(x_5, x_7, x_8, x_9, x_10, x_11, x_20);
if (lean_obj_tag(x_21) == 0)
{
@ -2671,6 +2799,10 @@ x_24 = l_Lean_Compiler_LCNF_attachCodeDecls(x_19, x_22);
lean_dec(x_19);
x_25 = l___private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go___closed__1;
x_26 = l_Lean_Compiler_LCNF_mkAuxFunDecl(x_14, x_24, x_25, x_8, x_9, x_10, x_11, x_23);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
if (lean_obj_tag(x_26) == 0)
{
uint8_t x_27;
@ -2732,6 +2864,10 @@ else
uint8_t x_38;
lean_dec(x_19);
lean_dec_ref(x_14);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
x_38 = !lean_is_exclusive(x_21);
if (x_38 == 0)
{
@ -2756,6 +2892,11 @@ else
{
uint8_t x_42;
lean_dec_ref(x_14);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec_ref(x_5);
x_42 = !lean_is_exclusive(x_18);
if (x_42 == 0)
@ -2796,6 +2937,11 @@ else
uint8_t x_56; lean_object* x_57; lean_object* x_58;
x_56 = 0;
x_57 = lean_box(0);
lean_inc(x_11);
lean_inc_ref(x_10);
lean_inc(x_9);
lean_inc_ref(x_8);
lean_inc(x_7);
x_58 = l_Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__2___redArg(x_2, x_3, x_53, x_4, x_57, x_56, x_54, x_51, x_52, x_51, x_7, x_8, x_9, x_10, x_11, x_12);
lean_dec(x_54);
if (lean_obj_tag(x_58) == 0)
@ -2814,6 +2960,11 @@ goto block_46;
else
{
uint8_t x_61;
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec_ref(x_5);
lean_dec_ref(x_1);
x_61 = !lean_is_exclusive(x_58);
@ -2848,11 +2999,6 @@ lean_dec(x_1);
x_11 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_12 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__0(x_10, x_11, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
return x_12;
}
}
@ -2865,38 +3011,15 @@ lean_dec(x_1);
x_11 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_12 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__1(x_10, x_11, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
return x_12;
}
}
LEAN_EXPORT lean_object* l_Std_PRange_RangeIterator_instIteratorLoop_loop___at___Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__2_spec__2___redArg___lam__0___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10;
x_10 = l_Std_PRange_RangeIterator_instIteratorLoop_loop___at___Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__2_spec__2___redArg___lam__0(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
return x_10;
}
}
LEAN_EXPORT lean_object* l_Std_PRange_RangeIterator_instIteratorLoop_loop___at___Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__2_spec__2___redArg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14) {
_start:
{
uint8_t x_15; lean_object* x_16;
x_15 = lean_unbox(x_3);
x_16 = l_Std_PRange_RangeIterator_instIteratorLoop_loop___at___Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__2_spec__2___redArg(x_1, x_2, x_15, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14);
lean_dec(x_13);
lean_dec_ref(x_12);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec(x_6);
lean_dec(x_2);
lean_dec_ref(x_1);
@ -2931,11 +3054,6 @@ uint8_t x_22; uint8_t x_23; lean_object* x_24;
x_22 = lean_unbox(x_3);
x_23 = lean_unbox(x_6);
x_24 = l_Std_PRange_RangeIterator_instIteratorLoop_loop___at___Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__2_spec__2(x_1, x_2, x_22, x_4, x_5, x_23, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_17, x_18, x_19, x_20, x_21);
lean_dec(x_20);
lean_dec_ref(x_19);
lean_dec(x_18);
lean_dec_ref(x_17);
lean_dec(x_16);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_2);
@ -2950,11 +3068,6 @@ uint8_t x_17; uint8_t x_18; lean_object* x_19;
x_17 = lean_unbox(x_3);
x_18 = lean_unbox(x_6);
x_19 = l_Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__2___redArg(x_1, x_2, x_17, x_4, x_5, x_18, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16);
lean_dec(x_15);
lean_dec_ref(x_14);
lean_dec(x_13);
lean_dec_ref(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_8);
lean_dec(x_7);
@ -2991,11 +3104,6 @@ uint8_t x_22; uint8_t x_23; lean_object* x_24;
x_22 = lean_unbox(x_3);
x_23 = lean_unbox(x_6);
x_24 = l_Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go_spec__2(x_1, x_2, x_22, x_4, x_5, x_23, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_17, x_18, x_19, x_20, x_21);
lean_dec(x_20);
lean_dec_ref(x_19);
lean_dec(x_18);
lean_dec_ref(x_17);
lean_dec(x_16);
lean_dec(x_13);
lean_dec(x_11);
lean_dec(x_10);
@ -3025,11 +3133,6 @@ _start:
uint8_t x_13; lean_object* x_14;
x_13 = lean_unbox(x_6);
x_14 = l___private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go(x_1, x_2, x_3, x_4, x_5, x_13, x_7, x_8, x_9, x_10, x_11, x_12);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec(x_3);
lean_dec_ref(x_2);
return x_14;
@ -3097,6 +3200,7 @@ lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 1);
lean_inc(x_15);
lean_dec_ref(x_13);
lean_inc(x_14);
x_16 = l___private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go(x_1, x_2, x_3, x_4, x_5, x_6, x_14, x_7, x_8, x_9, x_10, x_15);
if (lean_obj_tag(x_16) == 0)
{
@ -3142,10 +3246,6 @@ _start:
uint8_t x_12; lean_object* x_13;
x_12 = lean_unbox(x_6);
x_13 = l___private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt(x_1, x_2, x_3, x_4, x_5, x_12, x_7, x_8, x_9, x_10, x_11);
lean_dec(x_10);
lean_dec_ref(x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_3);
lean_dec_ref(x_2);
return x_13;
@ -7187,6 +7287,10 @@ else
{
lean_object* x_50; lean_object* x_51;
x_50 = lean_ctor_get(x_3, 2);
lean_inc(x_16);
lean_inc_ref(x_15);
lean_inc(x_14);
lean_inc_ref(x_13);
lean_inc(x_41);
lean_inc_ref(x_34);
lean_inc_ref(x_4);
@ -7518,6 +7622,10 @@ x_116 = lean_ctor_get(x_3, 2);
x_117 = l___private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go___closed__2;
x_118 = lean_unbox(x_114);
lean_dec(x_114);
lean_inc(x_16);
lean_inc_ref(x_15);
lean_inc(x_14);
lean_inc_ref(x_13);
lean_inc(x_86);
lean_inc_ref(x_4);
x_119 = l___private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt(x_4, x_116, x_93, x_117, x_86, x_118, x_13, x_14, x_15, x_16, x_87);
@ -7668,6 +7776,10 @@ x_141 = lean_ctor_get(x_3, 2);
x_142 = l___private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go___closed__2;
x_143 = lean_unbox(x_139);
lean_dec(x_139);
lean_inc(x_16);
lean_inc_ref(x_15);
lean_inc(x_14);
lean_inc_ref(x_13);
lean_inc(x_86);
lean_inc_ref(x_4);
x_144 = l___private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt(x_4, x_141, x_93, x_142, x_86, x_143, x_13, x_14, x_15, x_16, x_87);
@ -7971,6 +8083,10 @@ else
{
lean_object* x_50; lean_object* x_51;
x_50 = lean_ctor_get(x_3, 2);
lean_inc(x_16);
lean_inc_ref(x_15);
lean_inc(x_14);
lean_inc_ref(x_13);
lean_inc(x_41);
lean_inc_ref(x_34);
lean_inc_ref(x_4);
@ -8302,6 +8418,10 @@ x_116 = lean_ctor_get(x_3, 2);
x_117 = l___private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go___closed__2;
x_118 = lean_unbox(x_114);
lean_dec(x_114);
lean_inc(x_16);
lean_inc_ref(x_15);
lean_inc(x_14);
lean_inc_ref(x_13);
lean_inc(x_86);
lean_inc_ref(x_4);
x_119 = l___private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt(x_4, x_116, x_93, x_117, x_86, x_118, x_13, x_14, x_15, x_16, x_87);
@ -8452,6 +8572,10 @@ x_141 = lean_ctor_get(x_3, 2);
x_142 = l___private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt_go___closed__2;
x_143 = lean_unbox(x_139);
lean_dec(x_139);
lean_inc(x_16);
lean_inc_ref(x_15);
lean_inc(x_14);
lean_inc_ref(x_13);
lean_inc(x_86);
lean_inc_ref(x_4);
x_144 = l___private_Lean_Compiler_LCNF_Simp_JpCases_0__Lean_Compiler_LCNF_Simp_mkJpAlt(x_4, x_141, x_93, x_142, x_86, x_143, x_13, x_14, x_15, x_16, x_87);

96
stage0/stdlib/Lean/Compiler/LCNF/Simp/Main.c generated
View file

@ -250,6 +250,7 @@ size_t lean_array_size(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_specializePartialApp___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_LCNF_Simp_inlineApp_x3f___closed__3;
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_simp___lam__0(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_LCNF_normFVarImp(lean_object*, lean_object*, uint8_t);
static lean_object* l_Lean_Compiler_LCNF_Simp_simp___lam__0___closed__1;
lean_object* l_Lean_Compiler_LCNF_isInductiveWithNoCtors___redArg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_LCNF_Simp_specializePartialApp___closed__17;
@ -265,7 +266,6 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normLetDecl___at___Lean_Compiler_L
lean_object* l_Lean_Expr_headBeta(lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* l_Id_instMonad___lam__0(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(lean_object*, lean_object*, uint8_t);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Simp_elimVar_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1723,6 +1723,10 @@ lean_inc(x_44);
x_45 = lean_ctor_get(x_42, 1);
lean_inc(x_45);
lean_dec(x_42);
lean_inc(x_8);
lean_inc_ref(x_7);
lean_inc(x_6);
lean_inc_ref(x_5);
x_46 = l_Lean_Compiler_LCNF_Code_internalize(x_11, x_45, x_5, x_6, x_7, x_8, x_43);
if (lean_obj_tag(x_46) == 0)
{
@ -1743,6 +1747,10 @@ lean_inc(x_51);
lean_dec_ref(x_50);
x_52 = l_Lean_Compiler_LCNF_Simp_specializePartialApp___closed__21;
x_53 = l_Lean_Compiler_LCNF_mkAuxFunDecl(x_44, x_47, x_52, x_5, x_6, x_7, x_8, x_51);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
return x_53;
}
else
@ -1750,6 +1758,10 @@ else
uint8_t x_54;
lean_dec(x_47);
lean_dec(x_44);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
x_54 = !lean_is_exclusive(x_50);
if (x_54 == 0)
{
@ -1774,6 +1786,10 @@ else
{
uint8_t x_58;
lean_dec(x_44);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
x_58 = !lean_is_exclusive(x_46);
if (x_58 == 0)
{
@ -1798,6 +1814,10 @@ else
{
uint8_t x_62;
lean_dec_ref(x_11);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
x_62 = !lean_is_exclusive(x_41);
if (x_62 == 0)
{
@ -1947,10 +1967,6 @@ _start:
{
lean_object* x_10;
x_10 = l_Lean_Compiler_LCNF_Simp_specializePartialApp(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec_ref(x_4);
lean_dec(x_3);
lean_dec_ref(x_2);
@ -1970,6 +1986,10 @@ lean_inc(x_12);
if (lean_obj_tag(x_12) == 0)
{
uint8_t x_13;
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec_ref(x_2);
x_13 = !lean_is_exclusive(x_11);
if (x_13 == 0)
@ -2018,6 +2038,10 @@ if (x_24 == 0)
uint8_t x_25;
lean_free_object(x_12);
lean_dec(x_21);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec_ref(x_2);
x_25 = !lean_is_exclusive(x_22);
if (x_25 == 0)
@ -2119,6 +2143,10 @@ else
uint8_t x_47;
lean_free_object(x_12);
lean_dec(x_21);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec_ref(x_2);
x_47 = !lean_is_exclusive(x_32);
if (x_47 == 0)
@ -2146,6 +2174,10 @@ else
uint8_t x_51;
lean_free_object(x_12);
lean_dec(x_21);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec_ref(x_2);
x_51 = !lean_is_exclusive(x_22);
if (x_51 == 0)
@ -2185,6 +2217,10 @@ if (x_58 == 0)
{
lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62;
lean_dec(x_55);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec_ref(x_2);
x_59 = lean_ctor_get(x_56, 1);
lean_inc(x_59);
@ -2282,6 +2318,10 @@ else
{
lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82;
lean_dec(x_55);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec_ref(x_2);
x_79 = lean_ctor_get(x_64, 0);
lean_inc(x_79);
@ -2310,6 +2350,10 @@ else
{
lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86;
lean_dec(x_55);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec_ref(x_2);
x_83 = lean_ctor_get(x_56, 0);
lean_inc(x_83);
@ -2338,6 +2382,10 @@ return x_86;
else
{
uint8_t x_87;
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec_ref(x_2);
x_87 = !lean_is_exclusive(x_11);
if (x_87 == 0)
@ -2365,10 +2413,6 @@ _start:
{
lean_object* x_11;
x_11 = l_Lean_Compiler_LCNF_Simp_inlineJp_x3f(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec_ref(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
lean_dec_ref(x_3);
@ -5428,7 +5472,7 @@ x_9 = lean_ctor_get(x_8, 0);
lean_inc_ref(x_9);
lean_dec(x_8);
x_10 = 0;
x_11 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_9, x_5, x_10);
x_11 = l_Lean_Compiler_LCNF_normFVarImp(x_9, x_5, x_10);
lean_dec_ref(x_9);
if (lean_obj_tag(x_11) == 0)
{
@ -5462,7 +5506,7 @@ x_18 = lean_ctor_get(x_16, 0);
lean_inc_ref(x_18);
lean_dec(x_16);
x_19 = 0;
x_20 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_18, x_5, x_19);
x_20 = l_Lean_Compiler_LCNF_normFVarImp(x_18, x_5, x_19);
lean_dec_ref(x_18);
if (lean_obj_tag(x_20) == 0)
{
@ -7299,6 +7343,10 @@ lean_inc_ref(x_27);
x_171 = l_Array_toSubarray___redArg(x_27, x_169, x_170);
x_172 = l_Array_ofSubarray___redArg(x_171);
lean_dec_ref(x_171);
lean_inc(x_162);
lean_inc_ref(x_165);
lean_inc(x_167);
lean_inc_ref(x_161);
lean_inc_ref(x_172);
x_173 = l_Lean_Compiler_LCNF_Simp_betaReduce(x_24, x_25, x_172, x_32, x_160, x_166, x_164, x_161, x_167, x_165, x_162, x_168);
lean_dec_ref(x_24);
@ -7549,6 +7597,10 @@ lean_dec_ref(x_31);
lean_dec(x_30);
lean_dec(x_29);
lean_dec(x_22);
lean_inc(x_207);
lean_inc_ref(x_206);
lean_inc(x_205);
lean_inc_ref(x_204);
x_212 = l_Lean_Compiler_LCNF_Simp_specializePartialApp(x_21, x_201, x_202, x_203, x_204, x_205, x_206, x_207, x_208);
if (lean_obj_tag(x_212) == 0)
{
@ -11152,7 +11204,7 @@ x_460 = lean_ctor_get(x_458, 0);
lean_inc_ref(x_460);
lean_dec(x_458);
lean_inc(x_455);
x_461 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_460, x_455, x_53);
x_461 = l_Lean_Compiler_LCNF_normFVarImp(x_460, x_455, x_53);
lean_dec_ref(x_460);
if (lean_obj_tag(x_461) == 0)
{
@ -11174,6 +11226,10 @@ if (lean_is_exclusive(x_463)) {
lean_dec_ref(x_463);
x_466 = lean_box(0);
}
lean_inc(x_8);
lean_inc_ref(x_7);
lean_inc(x_6);
lean_inc_ref(x_5);
lean_inc(x_464);
x_483 = l_Lean_Compiler_LCNF_Simp_inlineJp_x3f(x_462, x_464, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_465);
if (lean_obj_tag(x_483) == 0)
@ -11494,7 +11550,7 @@ x_525 = lean_ctor_get(x_518, 0);
lean_inc_ref(x_525);
lean_dec(x_518);
lean_inc(x_522);
x_526 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_525, x_522, x_53);
x_526 = l_Lean_Compiler_LCNF_normFVarImp(x_525, x_522, x_53);
lean_dec_ref(x_525);
if (lean_obj_tag(x_526) == 0)
{
@ -12771,7 +12827,7 @@ x_728 = lean_ctor_get(x_726, 0);
lean_inc_ref(x_728);
lean_dec(x_726);
lean_inc(x_724);
x_729 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_728, x_724, x_53);
x_729 = l_Lean_Compiler_LCNF_normFVarImp(x_728, x_724, x_53);
lean_dec_ref(x_728);
if (lean_obj_tag(x_729) == 0)
{
@ -14929,7 +14985,7 @@ x_1131 = lean_ctor_get(x_1129, 0);
lean_inc_ref(x_1131);
lean_dec(x_1129);
lean_inc(x_1126);
x_1132 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_1131, x_1126, x_53);
x_1132 = l_Lean_Compiler_LCNF_normFVarImp(x_1131, x_1126, x_53);
lean_dec_ref(x_1131);
if (lean_obj_tag(x_1132) == 0)
{
@ -14951,6 +15007,10 @@ if (lean_is_exclusive(x_1134)) {
lean_dec_ref(x_1134);
x_1137 = lean_box(0);
}
lean_inc(x_8);
lean_inc_ref(x_844);
lean_inc(x_6);
lean_inc_ref(x_5);
lean_inc(x_1135);
x_1151 = l_Lean_Compiler_LCNF_Simp_inlineJp_x3f(x_1133, x_1135, x_2, x_3, x_4, x_5, x_6, x_844, x_8, x_1136);
if (lean_obj_tag(x_1151) == 0)
@ -15266,7 +15326,7 @@ x_1193 = lean_ctor_get(x_1186, 0);
lean_inc_ref(x_1193);
lean_dec(x_1186);
lean_inc(x_1190);
x_1194 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_1193, x_1190, x_53);
x_1194 = l_Lean_Compiler_LCNF_normFVarImp(x_1193, x_1190, x_53);
lean_dec_ref(x_1193);
if (lean_obj_tag(x_1194) == 0)
{
@ -15979,7 +16039,7 @@ x_1303 = lean_ctor_get(x_1301, 0);
lean_inc_ref(x_1303);
lean_dec(x_1301);
lean_inc(x_1299);
x_1304 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_1303, x_1299, x_53);
x_1304 = l_Lean_Compiler_LCNF_normFVarImp(x_1303, x_1299, x_53);
lean_dec_ref(x_1303);
if (lean_obj_tag(x_1304) == 0)
{
@ -17138,7 +17198,7 @@ lean_inc_ref(x_14);
lean_dec(x_11);
x_15 = 0;
lean_inc(x_13);
x_16 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp(x_14, x_13, x_15);
x_16 = l_Lean_Compiler_LCNF_normFVarImp(x_14, x_13, x_15);
lean_dec_ref(x_14);
if (lean_obj_tag(x_16) == 0)
{

16
stage0/stdlib/Lean/Compiler/LCNF/Simp/SimpM.c generated
View file

@ -6963,6 +6963,10 @@ lean_dec_ref(x_20);
x_23 = lean_ctor_get(x_21, 1);
lean_inc(x_23);
lean_dec(x_21);
lean_inc(x_11);
lean_inc_ref(x_10);
lean_inc(x_9);
lean_inc_ref(x_8);
x_24 = l_Lean_Compiler_LCNF_Code_internalize(x_2, x_23, x_8, x_9, x_10, x_11, x_22);
if (lean_obj_tag(x_24) == 0)
{
@ -6974,6 +6978,10 @@ lean_inc(x_26);
lean_dec_ref(x_24);
lean_inc(x_25);
x_27 = l_Lean_Compiler_LCNF_Simp_updateFunDeclInfo___redArg(x_25, x_4, x_6, x_8, x_9, x_10, x_11, x_26);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
if (lean_obj_tag(x_27) == 0)
{
uint8_t x_28;
@ -7024,6 +7032,10 @@ return x_35;
}
else
{
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
return x_24;
}
}
@ -7091,10 +7103,6 @@ _start:
uint8_t x_13; lean_object* x_14;
x_13 = lean_unbox(x_4);
x_14 = l_Lean_Compiler_LCNF_Simp_betaReduce(x_1, x_2, x_3, x_13, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);

173
stage0/stdlib/Lean/Compiler/LCNF/Specialize.c generated
View file

@ -150,7 +150,6 @@ lean_object* l_Lean_Compiler_LCNF_LCtx_toLocalContext(lean_object*);
static lean_object* l_Lean_Compiler_LCNF_Specialize_cacheSpec___redArg___closed__0;
LEAN_EXPORT lean_object* l_Array_filterMapM___at___Lean_Compiler_LCNF_Specialize_specializeApp_x3f_spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_instMonad___redArg(lean_object*);
LEAN_EXPORT lean_object* l_Std_Iterators_IterM_DefaultConsumers_forIn_x27___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__7___redArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_foldlMUnsafe_fold___at___Array_filterMapM___at___Lean_Compiler_LCNF_Specialize_specializeApp_x3f_spec__1_spec__1(lean_object*, size_t, size_t, lean_object*);
static double l_Lean_addTrace___at___Lean_Compiler_LCNF_Specialize_specializeApp_x3f_spec__8___redArg___closed__3;
static lean_object* l___private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_initFn___closed__13____x40_Lean_Compiler_LCNF_Specialize___hyg_4912_;
@ -465,7 +464,6 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_withLetDecl___redArg(le
lean_object* l_Lean_PersistentEnvExtension_addEntry___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Iterators_IterM_DefaultConsumers_forIn_x27___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__7___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_AssocList_replace___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__3___redArg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Iterators_IterM_DefaultConsumers_forIn_x27___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Id_instMonad___lam__6(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_initFn___closed__17____x40_Lean_Compiler_LCNF_Specialize___hyg_4912_;
LEAN_EXPORT lean_object* l_Std_DTreeMap_Internal_Impl_contains___at___Lean_Compiler_LCNF_Specialize_Collector_collect_spec__1___boxed(lean_object*, lean_object*, lean_object*);
@ -7197,6 +7195,11 @@ x_10 = lean_usize_dec_lt(x_2, x_1);
if (x_10 == 0)
{
lean_object* x_11;
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_3);
lean_ctor_set(x_11, 1, x_9);
@ -7206,6 +7209,11 @@ else
{
lean_object* x_12; lean_object* x_13;
x_12 = lean_array_uget(x_3, x_2);
lean_inc(x_8);
lean_inc_ref(x_7);
lean_inc(x_6);
lean_inc_ref(x_5);
lean_inc(x_4);
x_13 = l_Lean_Compiler_LCNF_Internalize_internalizeParam(x_12, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_13) == 0)
{
@ -7228,6 +7236,11 @@ goto _start;
else
{
uint8_t x_22;
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
lean_dec_ref(x_3);
x_22 = !lean_is_exclusive(x_13);
if (x_22 == 0)
@ -7259,6 +7272,11 @@ x_10 = lean_usize_dec_lt(x_2, x_1);
if (x_10 == 0)
{
lean_object* x_11;
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_3);
lean_ctor_set(x_11, 1, x_9);
@ -7268,6 +7286,11 @@ else
{
lean_object* x_12; lean_object* x_13;
x_12 = lean_array_uget(x_3, x_2);
lean_inc(x_8);
lean_inc_ref(x_7);
lean_inc(x_6);
lean_inc_ref(x_5);
lean_inc(x_4);
x_13 = l_Lean_Compiler_LCNF_Internalize_internalizeCodeDecl(x_12, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_13) == 0)
{
@ -7290,6 +7313,11 @@ goto _start;
else
{
uint8_t x_22;
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
lean_dec_ref(x_3);
x_22 = !lean_is_exclusive(x_13);
if (x_22 == 0)
@ -7321,6 +7349,11 @@ x_19 = lean_usize_dec_lt(x_5, x_4);
if (x_19 == 0)
{
lean_object* x_20;
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec(x_2);
lean_dec_ref(x_1);
x_20 = lean_alloc_ctor(0, 2, 0);
@ -7350,6 +7383,11 @@ x_27 = lean_nat_dec_lt(x_25, x_26);
if (x_27 == 0)
{
lean_object* x_28; lean_object* x_29;
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec(x_2);
lean_dec_ref(x_1);
if (lean_is_scalar(x_23)) {
@ -7399,6 +7437,11 @@ lean_inc(x_2);
lean_inc(x_40);
x_41 = l_Lean_Expr_instantiateLevelParamsNoCache(x_39, x_40, x_2);
lean_ctor_set(x_34, 2, x_41);
lean_inc(x_11);
lean_inc_ref(x_10);
lean_inc(x_9);
lean_inc_ref(x_8);
lean_inc(x_7);
x_42 = l_Lean_Compiler_LCNF_Internalize_internalizeParam(x_34, x_7, x_8, x_9, x_10, x_11, x_12);
if (lean_obj_tag(x_42) == 0)
{
@ -7426,6 +7469,11 @@ uint8_t x_47;
lean_dec_ref(x_21);
lean_dec(x_23);
lean_dec(x_22);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec(x_2);
lean_dec_ref(x_1);
x_47 = !lean_is_exclusive(x_42);
@ -7468,6 +7516,11 @@ lean_ctor_set(x_57, 0, x_51);
lean_ctor_set(x_57, 1, x_52);
lean_ctor_set(x_57, 2, x_56);
lean_ctor_set_uint8(x_57, sizeof(void*)*3, x_54);
lean_inc(x_11);
lean_inc_ref(x_10);
lean_inc(x_9);
lean_inc_ref(x_8);
lean_inc(x_7);
x_58 = l_Lean_Compiler_LCNF_Internalize_internalizeParam(x_57, x_7, x_8, x_9, x_10, x_11, x_12);
if (lean_obj_tag(x_58) == 0)
{
@ -7495,6 +7548,11 @@ lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66;
lean_dec_ref(x_21);
lean_dec(x_23);
lean_dec(x_22);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec(x_2);
lean_dec_ref(x_1);
x_63 = lean_ctor_get(x_58, 0);
@ -7760,6 +7818,11 @@ lean_ctor_set(x_161, 0, x_154);
lean_ctor_set(x_161, 1, x_155);
lean_ctor_set(x_161, 2, x_160);
lean_ctor_set_uint8(x_161, sizeof(void*)*3, x_157);
lean_inc(x_11);
lean_inc_ref(x_10);
lean_inc(x_9);
lean_inc_ref(x_8);
lean_inc(x_7);
x_162 = l_Lean_Compiler_LCNF_Internalize_internalizeParam(x_161, x_7, x_8, x_9, x_10, x_11, x_12);
if (lean_obj_tag(x_162) == 0)
{
@ -7787,6 +7850,11 @@ lean_object* x_167; lean_object* x_168; lean_object* x_169; lean_object* x_170;
lean_dec_ref(x_153);
lean_dec(x_23);
lean_dec(x_22);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec(x_2);
lean_dec_ref(x_1);
x_167 = lean_ctor_get(x_162, 0);
@ -7993,6 +8061,11 @@ lean_inc(x_3);
lean_inc(x_17);
x_18 = l_Lean_Expr_instantiateLevelParamsNoCache(x_16, x_17, x_3);
lean_ctor_set(x_13, 2, x_18);
lean_inc(x_10);
lean_inc_ref(x_9);
lean_inc(x_8);
lean_inc_ref(x_7);
lean_inc(x_6);
x_19 = l_Lean_Compiler_LCNF_Internalize_internalizeParam(x_13, x_6, x_7, x_8, x_9, x_10, x_11);
if (lean_obj_tag(x_19) == 0)
{
@ -8012,6 +8085,11 @@ else
{
uint8_t x_24;
lean_dec(x_14);
lean_dec(x_10);
lean_dec_ref(x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_3);
lean_dec_ref(x_2);
@ -8056,6 +8134,11 @@ lean_ctor_set(x_34, 0, x_28);
lean_ctor_set(x_34, 1, x_29);
lean_ctor_set(x_34, 2, x_33);
lean_ctor_set_uint8(x_34, sizeof(void*)*3, x_31);
lean_inc(x_10);
lean_inc_ref(x_9);
lean_inc(x_8);
lean_inc_ref(x_7);
lean_inc(x_6);
x_35 = l_Lean_Compiler_LCNF_Internalize_internalizeParam(x_34, x_6, x_7, x_8, x_9, x_10, x_11);
if (lean_obj_tag(x_35) == 0)
{
@ -8075,6 +8158,11 @@ else
{
lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43;
lean_dec(x_14);
lean_dec(x_10);
lean_dec_ref(x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_3);
lean_dec_ref(x_2);
@ -8114,6 +8202,11 @@ goto _start;
default:
{
lean_object* x_46;
lean_dec(x_10);
lean_dec_ref(x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec(x_3);
lean_dec_ref(x_2);
lean_dec_ref(x_1);
@ -8672,6 +8765,11 @@ if (lean_is_exclusive(x_14)) {
}
x_21 = lean_array_size(x_3);
x_22 = 0;
lean_inc(x_12);
lean_inc_ref(x_11);
lean_inc(x_10);
lean_inc_ref(x_9);
lean_inc(x_8);
x_23 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__4(x_21, x_22, x_3, x_8, x_9, x_10, x_11, x_12, x_13);
if (lean_obj_tag(x_23) == 0)
{
@ -8682,6 +8780,11 @@ x_25 = lean_ctor_get(x_23, 1);
lean_inc(x_25);
lean_dec_ref(x_23);
x_26 = lean_array_size(x_4);
lean_inc(x_12);
lean_inc_ref(x_11);
lean_inc(x_10);
lean_inc_ref(x_9);
lean_inc(x_8);
x_27 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__5(x_26, x_22, x_4, x_8, x_9, x_10, x_11, x_12, x_25);
if (lean_obj_tag(x_27) == 0)
{
@ -8699,6 +8802,11 @@ x_33 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_24);
x_34 = lean_array_size(x_16);
lean_inc(x_12);
lean_inc_ref(x_11);
lean_inc(x_10);
lean_inc_ref(x_9);
lean_inc(x_8);
lean_inc(x_1);
lean_inc_ref(x_6);
x_35 = l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__6___redArg(x_6, x_1, x_16, x_34, x_22, x_33, x_8, x_9, x_10, x_11, x_12, x_29);
@ -8782,6 +8890,11 @@ lean_inc_ref(x_59);
lean_inc_ref(x_40);
x_61 = l_Std_Iterators_Types_ULiftIterator_instIterator___redArg(x_40, x_60, x_59);
x_62 = l_Std_Iterators_instIteratorMap___redArg(x_59, x_61, x_40, x_46);
lean_inc(x_12);
lean_inc_ref(x_11);
lean_inc(x_10);
lean_inc_ref(x_9);
lean_inc(x_8);
lean_inc(x_1);
lean_inc_ref(x_6);
x_63 = l_Std_Iterators_IterM_DefaultConsumers_forIn_x27___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__7___redArg(x_62, x_6, x_1, x_49, x_38, x_8, x_9, x_10, x_11, x_12, x_37);
@ -8810,8 +8923,11 @@ x_72 = lean_ctor_get(x_63, 1);
lean_inc(x_72);
lean_dec_ref(x_63);
x_73 = l___private_Lean_Compiler_LCNF_Basic_0__Lean_Compiler_LCNF_Code_instantiateValueLevelParams_instCode(x_15, x_1, x_19);
lean_inc(x_12);
lean_inc_ref(x_11);
lean_inc(x_10);
lean_inc_ref(x_9);
x_74 = l_Lean_Compiler_LCNF_Internalize_internalizeCode(x_73, x_8, x_9, x_10, x_11, x_12, x_72);
lean_dec(x_8);
if (lean_obj_tag(x_74) == 0)
{
lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78;
@ -9035,8 +9151,11 @@ x_110 = lean_ctor_get(x_63, 1);
lean_inc(x_110);
lean_dec_ref(x_63);
x_111 = l___private_Lean_Compiler_LCNF_Basic_0__Lean_Compiler_LCNF_Code_instantiateValueLevelParams_instCode(x_15, x_1, x_19);
lean_inc(x_12);
lean_inc_ref(x_11);
lean_inc(x_10);
lean_inc_ref(x_9);
x_112 = l_Lean_Compiler_LCNF_Internalize_internalizeCode(x_111, x_8, x_9, x_10, x_11, x_12, x_110);
lean_dec(x_8);
if (lean_obj_tag(x_112) == 0)
{
lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116;
@ -9379,11 +9498,6 @@ lean_dec(x_1);
x_11 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_12 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__4(x_10, x_11, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
return x_12;
}
}
@ -9396,11 +9510,6 @@ lean_dec(x_1);
x_11 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_12 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__5(x_10, x_11, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
return x_12;
}
}
@ -9413,11 +9522,6 @@ lean_dec(x_4);
x_14 = lean_unbox_usize(x_5);
lean_dec(x_5);
x_15 = l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__6___redArg(x_1, x_2, x_3, x_13, x_14, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_8);
lean_dec(x_7);
lean_dec_ref(x_3);
return x_15;
}
@ -9431,43 +9535,12 @@ lean_dec(x_6);
x_16 = lean_unbox_usize(x_7);
lean_dec(x_7);
x_17 = l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__6(x_1, x_2, x_3, x_4, x_5, x_15, x_16, x_8, x_9, x_10, x_11, x_12, x_13, x_14);
lean_dec(x_13);
lean_dec_ref(x_12);
lean_dec(x_11);
lean_dec_ref(x_10);
lean_dec(x_9);
lean_dec_ref(x_5);
lean_dec_ref(x_4);
lean_dec_ref(x_3);
return x_17;
}
}
LEAN_EXPORT lean_object* l_Std_Iterators_IterM_DefaultConsumers_forIn_x27___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__7___redArg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
lean_object* x_12;
x_12 = l_Std_Iterators_IterM_DefaultConsumers_forIn_x27___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__7___redArg(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
lean_dec(x_10);
lean_dec_ref(x_9);
lean_dec(x_8);
lean_dec_ref(x_7);
lean_dec(x_6);
return x_12;
}
}
LEAN_EXPORT lean_object* l_Std_Iterators_IterM_DefaultConsumers_forIn_x27___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__7___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14, lean_object* x_15) {
_start:
{
lean_object* x_16;
x_16 = l_Std_Iterators_IterM_DefaultConsumers_forIn_x27___at_____private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go_spec__7(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15);
lean_dec(x_14);
lean_dec_ref(x_13);
lean_dec(x_12);
lean_dec_ref(x_11);
lean_dec(x_10);
return x_16;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_Specialize_0__Lean_Compiler_LCNF_Specialize_mkSpecDecl_go___lam__0___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{

874
stage0/stdlib/Lean/Elab/Deriving/Basic.c generated
View file

File diff suppressed because it is too large Load diff

4747
stage0/stdlib/Lean/Elab/MutualDef.c generated
View file

File diff suppressed because it is too large Load diff

413
stage0/stdlib/Lean/Elab/Tactic/Do/ProofMode/Delab.c generated
View file

@ -126,6 +126,7 @@ static lean_object* l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Ta
static lean_object* l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses___closed__2;
lean_object* l_Lean_SubExpr_Pos_push(lean_object*, lean_object*);
static lean_object* l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__14;
lean_object* l_Lean_Expr_getAppNumArgs(lean_object*);
lean_object* l_Lean_Syntax_node4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__1;
static lean_object* l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses___closed__1;
@ -180,6 +181,7 @@ LEAN_EXPORT lean_object* l_panic___at___Lean_PrettyPrinter_Delaborator_SubExpr_w
static lean_object* l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal___regBuiltin___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal__1___closed__1;
static lean_object* l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__44;
LEAN_EXPORT lean_object* l_panic___at___Lean_PrettyPrinter_Delaborator_SubExpr_withMDataExpr___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__4_spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabHypMarker___regBuiltin___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabHypMarker__1___closed__0;
static lean_object* l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__38;
@ -2744,197 +2746,260 @@ return x_1;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
x_8 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal___closed__4;
lean_inc(x_6);
lean_inc_ref(x_5);
lean_inc(x_4);
lean_inc_ref(x_3);
lean_inc(x_2);
lean_object* x_8; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; uint8_t x_77;
lean_inc_ref(x_1);
x_9 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__3___redArg(x_8, x_1, x_2, x_3, x_4, x_5, x_6, x_7);
if (lean_obj_tag(x_9) == 0)
x_72 = l_Lean_PrettyPrinter_Delaborator_SubExpr_getExpr___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__0___redArg(x_1, x_7);
x_73 = lean_ctor_get(x_72, 0);
lean_inc(x_73);
x_74 = lean_ctor_get(x_72, 1);
lean_inc(x_74);
lean_dec_ref(x_72);
x_75 = lean_unsigned_to_nat(3u);
x_76 = l_Lean_Expr_getAppNumArgs(x_73);
lean_dec(x_73);
x_77 = lean_nat_dec_le(x_75, x_76);
lean_dec(x_76);
if (x_77 == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
x_12 = lean_ctor_get(x_9, 1);
lean_inc(x_12);
lean_dec_ref(x_9);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses___closed__0;
lean_inc_ref(x_5);
x_15 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__1___redArg(x_14, x_1, x_2, x_3, x_4, x_5, x_6, x_12);
if (lean_obj_tag(x_15) == 0)
lean_object* x_78;
x_78 = l_Lean_PrettyPrinter_Delaborator_failure___redArg(x_74);
if (lean_obj_tag(x_78) == 0)
{
uint8_t x_16;
x_16 = !lean_is_exclusive(x_15);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20;
x_17 = lean_ctor_get(x_15, 0);
x_18 = lean_ctor_get(x_15, 1);
x_19 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg(x_17, x_5, x_18);
x_20 = !lean_is_exclusive(x_19);
if (x_20 == 0)
{
lean_object* x_21; lean_object* x_22; uint8_t x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_21 = lean_ctor_get(x_19, 0);
x_22 = lean_ctor_get(x_5, 5);
lean_inc(x_22);
lean_dec_ref(x_5);
x_23 = 0;
x_24 = l_Lean_SourceInfo_fromRef(x_22, x_23);
lean_dec(x_22);
x_25 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal___closed__6;
x_26 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__44;
x_27 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__48;
x_28 = l_Array_reverse___redArg(x_13);
x_29 = l_Array_append___redArg(x_27, x_28);
lean_dec_ref(x_28);
lean_inc(x_24);
x_30 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_30, 0, x_24);
lean_ctor_set(x_30, 1, x_26);
lean_ctor_set(x_30, 2, x_29);
x_31 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal___closed__7;
lean_inc(x_24);
lean_ctor_set_tag(x_15, 2);
lean_ctor_set(x_15, 1, x_31);
lean_ctor_set(x_15, 0, x_24);
x_32 = l_Lean_Syntax_node3(x_24, x_25, x_30, x_15, x_21);
lean_ctor_set(x_19, 0, x_32);
return x_19;
lean_object* x_79;
x_79 = lean_ctor_get(x_78, 1);
lean_inc(x_79);
lean_dec_ref(x_78);
x_8 = x_79;
goto block_71;
}
else
{
lean_object* x_33; lean_object* x_34; lean_object* x_35; uint8_t x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46;
x_33 = lean_ctor_get(x_19, 0);
x_34 = lean_ctor_get(x_19, 1);
lean_inc(x_34);
lean_inc(x_33);
lean_dec(x_19);
x_35 = lean_ctor_get(x_5, 5);
lean_inc(x_35);
lean_dec_ref(x_5);
x_36 = 0;
x_37 = l_Lean_SourceInfo_fromRef(x_35, x_36);
lean_dec(x_35);
x_38 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal___closed__6;
x_39 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__44;
x_40 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__48;
x_41 = l_Array_reverse___redArg(x_13);
x_42 = l_Array_append___redArg(x_40, x_41);
lean_dec_ref(x_41);
lean_inc(x_37);
x_43 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_43, 0, x_37);
lean_ctor_set(x_43, 1, x_39);
lean_ctor_set(x_43, 2, x_42);
x_44 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal___closed__7;
lean_inc(x_37);
lean_ctor_set_tag(x_15, 2);
lean_ctor_set(x_15, 1, x_44);
lean_ctor_set(x_15, 0, x_37);
x_45 = l_Lean_Syntax_node3(x_37, x_38, x_43, x_15, x_33);
x_46 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_46, 0, x_45);
lean_ctor_set(x_46, 1, x_34);
return x_46;
}
}
else
{
lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; uint8_t x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65;
x_47 = lean_ctor_get(x_15, 0);
x_48 = lean_ctor_get(x_15, 1);
lean_inc(x_48);
lean_inc(x_47);
lean_dec(x_15);
x_49 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg(x_47, x_5, x_48);
x_50 = lean_ctor_get(x_49, 0);
lean_inc(x_50);
x_51 = lean_ctor_get(x_49, 1);
lean_inc(x_51);
if (lean_is_exclusive(x_49)) {
lean_ctor_release(x_49, 0);
lean_ctor_release(x_49, 1);
x_52 = x_49;
} else {
lean_dec_ref(x_49);
x_52 = lean_box(0);
}
x_53 = lean_ctor_get(x_5, 5);
lean_inc(x_53);
lean_dec_ref(x_5);
x_54 = 0;
x_55 = l_Lean_SourceInfo_fromRef(x_53, x_54);
lean_dec(x_53);
x_56 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal___closed__6;
x_57 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__44;
x_58 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__48;
x_59 = l_Array_reverse___redArg(x_13);
x_60 = l_Array_append___redArg(x_58, x_59);
lean_dec_ref(x_59);
lean_inc(x_55);
x_61 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_61, 0, x_55);
lean_ctor_set(x_61, 1, x_57);
lean_ctor_set(x_61, 2, x_60);
x_62 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal___closed__7;
lean_inc(x_55);
x_63 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_63, 0, x_55);
lean_ctor_set(x_63, 1, x_62);
x_64 = l_Lean_Syntax_node3(x_55, x_56, x_61, x_63, x_50);
if (lean_is_scalar(x_52)) {
x_65 = lean_alloc_ctor(0, 2, 0);
} else {
x_65 = x_52;
}
lean_ctor_set(x_65, 0, x_64);
lean_ctor_set(x_65, 1, x_51);
return x_65;
}
}
else
{
lean_dec(x_13);
lean_dec_ref(x_5);
return x_15;
}
}
else
{
uint8_t x_66;
uint8_t x_80;
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
lean_dec_ref(x_3);
lean_dec(x_2);
lean_dec_ref(x_1);
x_66 = !lean_is_exclusive(x_9);
if (x_66 == 0)
x_80 = !lean_is_exclusive(x_78);
if (x_80 == 0)
{
return x_9;
return x_78;
}
else
{
lean_object* x_67; lean_object* x_68; lean_object* x_69;
x_67 = lean_ctor_get(x_9, 0);
x_68 = lean_ctor_get(x_9, 1);
lean_object* x_81; lean_object* x_82; lean_object* x_83;
x_81 = lean_ctor_get(x_78, 0);
x_82 = lean_ctor_get(x_78, 1);
lean_inc(x_82);
lean_inc(x_81);
lean_dec(x_78);
x_83 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_83, 0, x_81);
lean_ctor_set(x_83, 1, x_82);
return x_83;
}
}
}
else
{
x_8 = x_74;
goto block_71;
}
block_71:
{
lean_object* x_9; lean_object* x_10;
x_9 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal___closed__4;
lean_inc(x_6);
lean_inc_ref(x_5);
lean_inc(x_4);
lean_inc_ref(x_3);
lean_inc(x_2);
lean_inc_ref(x_1);
x_10 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__3___redArg(x_9, x_1, x_2, x_3, x_4, x_5, x_6, x_8);
if (lean_obj_tag(x_10) == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_11, 1);
lean_inc(x_12);
lean_dec(x_11);
x_13 = lean_ctor_get(x_10, 1);
lean_inc(x_13);
lean_dec_ref(x_10);
x_14 = lean_ctor_get(x_12, 1);
lean_inc(x_14);
lean_dec(x_12);
x_15 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses___closed__0;
lean_inc_ref(x_5);
x_16 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__1___redArg(x_15, x_1, x_2, x_3, x_4, x_5, x_6, x_13);
if (lean_obj_tag(x_16) == 0)
{
uint8_t x_17;
x_17 = !lean_is_exclusive(x_16);
if (x_17 == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21;
x_18 = lean_ctor_get(x_16, 0);
x_19 = lean_ctor_get(x_16, 1);
x_20 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg(x_18, x_5, x_19);
x_21 = !lean_is_exclusive(x_20);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23; uint8_t x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
x_22 = lean_ctor_get(x_20, 0);
x_23 = lean_ctor_get(x_5, 5);
lean_inc(x_23);
lean_dec_ref(x_5);
x_24 = 0;
x_25 = l_Lean_SourceInfo_fromRef(x_23, x_24);
lean_dec(x_23);
x_26 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal___closed__6;
x_27 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__44;
x_28 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__48;
x_29 = l_Array_reverse___redArg(x_14);
x_30 = l_Array_append___redArg(x_28, x_29);
lean_dec_ref(x_29);
lean_inc(x_25);
x_31 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_31, 0, x_25);
lean_ctor_set(x_31, 1, x_27);
lean_ctor_set(x_31, 2, x_30);
x_32 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal___closed__7;
lean_inc(x_25);
lean_ctor_set_tag(x_16, 2);
lean_ctor_set(x_16, 1, x_32);
lean_ctor_set(x_16, 0, x_25);
x_33 = l_Lean_Syntax_node3(x_25, x_26, x_31, x_16, x_22);
lean_ctor_set(x_20, 0, x_33);
return x_20;
}
else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36; uint8_t x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_34 = lean_ctor_get(x_20, 0);
x_35 = lean_ctor_get(x_20, 1);
lean_inc(x_35);
lean_inc(x_34);
lean_dec(x_20);
x_36 = lean_ctor_get(x_5, 5);
lean_inc(x_36);
lean_dec_ref(x_5);
x_37 = 0;
x_38 = l_Lean_SourceInfo_fromRef(x_36, x_37);
lean_dec(x_36);
x_39 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal___closed__6;
x_40 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__44;
x_41 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__48;
x_42 = l_Array_reverse___redArg(x_14);
x_43 = l_Array_append___redArg(x_41, x_42);
lean_dec_ref(x_42);
lean_inc(x_38);
x_44 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_44, 0, x_38);
lean_ctor_set(x_44, 1, x_40);
lean_ctor_set(x_44, 2, x_43);
x_45 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal___closed__7;
lean_inc(x_38);
lean_ctor_set_tag(x_16, 2);
lean_ctor_set(x_16, 1, x_45);
lean_ctor_set(x_16, 0, x_38);
x_46 = l_Lean_Syntax_node3(x_38, x_39, x_44, x_16, x_34);
x_47 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_47, 0, x_46);
lean_ctor_set(x_47, 1, x_35);
return x_47;
}
}
else
{
lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; uint8_t x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66;
x_48 = lean_ctor_get(x_16, 0);
x_49 = lean_ctor_get(x_16, 1);
lean_inc(x_49);
lean_inc(x_48);
lean_dec(x_16);
x_50 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg(x_48, x_5, x_49);
x_51 = lean_ctor_get(x_50, 0);
lean_inc(x_51);
x_52 = lean_ctor_get(x_50, 1);
lean_inc(x_52);
if (lean_is_exclusive(x_50)) {
lean_ctor_release(x_50, 0);
lean_ctor_release(x_50, 1);
x_53 = x_50;
} else {
lean_dec_ref(x_50);
x_53 = lean_box(0);
}
x_54 = lean_ctor_get(x_5, 5);
lean_inc(x_54);
lean_dec_ref(x_5);
x_55 = 0;
x_56 = l_Lean_SourceInfo_fromRef(x_54, x_55);
lean_dec(x_54);
x_57 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal___closed__6;
x_58 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__44;
x_59 = l_Std_Do_SPred_Notation_unpack___at_____private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal_delabHypotheses_spec__6___redArg___closed__48;
x_60 = l_Array_reverse___redArg(x_14);
x_61 = l_Array_append___redArg(x_59, x_60);
lean_dec_ref(x_60);
lean_inc(x_56);
x_62 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_62, 0, x_56);
lean_ctor_set(x_62, 1, x_58);
lean_ctor_set(x_62, 2, x_61);
x_63 = l___private_Lean_Elab_Tactic_Do_ProofMode_Delab_0__Lean_Elab_Tactic_Do_ProofMode_delabMGoal___closed__7;
lean_inc(x_56);
x_64 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_64, 0, x_56);
lean_ctor_set(x_64, 1, x_63);
x_65 = l_Lean_Syntax_node3(x_56, x_57, x_62, x_64, x_51);
if (lean_is_scalar(x_53)) {
x_66 = lean_alloc_ctor(0, 2, 0);
} else {
x_66 = x_53;
}
lean_ctor_set(x_66, 0, x_65);
lean_ctor_set(x_66, 1, x_52);
return x_66;
}
}
else
{
lean_dec(x_14);
lean_dec_ref(x_5);
return x_16;
}
}
else
{
uint8_t x_67;
lean_dec(x_6);
lean_dec_ref(x_5);
lean_dec(x_4);
lean_dec_ref(x_3);
lean_dec(x_2);
lean_dec_ref(x_1);
x_67 = !lean_is_exclusive(x_10);
if (x_67 == 0)
{
return x_10;
}
else
{
lean_object* x_68; lean_object* x_69; lean_object* x_70;
x_68 = lean_ctor_get(x_10, 0);
x_69 = lean_ctor_get(x_10, 1);
lean_inc(x_69);
lean_inc(x_68);
lean_inc(x_67);
lean_dec(x_9);
x_69 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_69, 0, x_67);
lean_ctor_set(x_69, 1, x_68);
return x_69;
lean_dec(x_10);
x_70 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_70, 0, x_68);
lean_ctor_set(x_70, 1, x_69);
return x_70;
}
}
}
}

7124
stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.c generated
View file

File diff suppressed because it is too large Load diff

5667
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c generated
View file

File diff suppressed because it is too large Load diff

606
stage0/stdlib/Std/Internal/Async/Basic.c generated
View file

@ -22,14 +22,12 @@ LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_instMonadAsyncStateTOfFunctor(l
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_AsyncTask_pure___redArg(lean_object*);
LEAN_EXPORT lean_object* l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instMonadAsyncAsyncTaskError___lam__0(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnitOfInhabited(lean_object*, lean_object*);
static lean_object* l_Std_Internal_IO_Async_EAsync_instOrElse___closed__0;
static lean_object* l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__0;
static lean_object* l_Std_Internal_IO_Async_EAsync_instMonadAwaitETask___closed__0;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_BaseAsync_lift___redArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_MaybeTask_instMonad___lam__8(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_BaseAsync_instMonad___lam__6___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_forIn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_forIn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instMonad(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_race___redArg___lam__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_ETask_instFunctor___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -80,7 +78,6 @@ LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_BaseAsync_instMonad___lam__0(le
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_tryFinally_x27___redArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_MaybeTask_instMonad___lam__0(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_AsyncTask_ofPurePromise(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_forIn___lam__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instInhabited(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_BaseAsync_instMonad___lam__3___boxed(lean_object*, lean_object*, lean_object*);
@ -127,7 +124,6 @@ LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_Async_toIO(lean_object*, lean_o
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_bind(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_ETask_map___redArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_BaseAsync_instInhabited___redArg(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_forIn___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_BaseAsync_bind___redArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_MaybeTask_instMonad___lam__6(lean_object*, lean_object*, lean_object*);
lean_object* lean_io_promise_resolve(lean_object*, lean_object*, lean_object*);
@ -142,7 +138,6 @@ lean_object* lean_task_pure(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_instMonadAwaitExceptTOfMonad___redArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_instMonadAsyncStateTOfFunctor___redArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_AsyncTask_ofPurePromise___boxed(lean_object*, lean_object*);
static lean_object* l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__2;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_MaybeTask_joinTask(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_ETask_bindEIO___redArg___lam__0(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_MaybeTask_map___redArg(lean_object*, lean_object*, uint8_t, lean_object*);
@ -175,6 +170,7 @@ LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_AsyncTask_getState___redArg___b
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_BaseAsync_map___redArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_throw___redArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instMonad___lam__4(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnit___lam__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_MaybeTask_get___redArg(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_BaseAsync_toRawBaseIO(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instOrElse(lean_object*, lean_object*);
@ -198,7 +194,6 @@ LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_MaybeTask_instMonad;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_AsyncTask_ofPromise___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_MaybeTask_bind___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_ofETask(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__1(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_ETask_ofPurePromise___redArg___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_async___redArg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_raceAll(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -238,6 +233,7 @@ LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_raceAll___boxed(lean_object*, l
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instInhabited___redArg(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_MaybeTask_instMonad___lam__4___boxed(lean_object*, lean_object*);
lean_object* lean_task_get_own(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnit(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_instMonadAwaitStateRefT_x27(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instMonadAsyncAsyncTaskError;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_instMonadAwaitExceptTOfMonad___redArg___lam__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -331,7 +327,7 @@ LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_BaseAsync_wait___redArg(lean_ob
LEAN_EXPORT lean_object* l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_BaseAsync_bind_bindAsyncTask___redArg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_instMonadAwaitReaderTOfMonad___redArg___lam__0(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_ETask_bindEIO(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnitOfInhabited___lam__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_BaseIO_chainTask___redArg(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
static lean_object* l_Std_Internal_IO_Async_ETask_ofPurePromise___redArg___closed__0;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_background___redArg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_MaybeTask_instMonad___lam__3(lean_object*, lean_object*, lean_object*, lean_object*);
@ -352,13 +348,12 @@ size_t lean_array_size(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_ETask_instMonad___lam__8(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_MaybeTask_get(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_instMonadAsyncStateTOfFunctor___redArg___lam__0(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnit___lam__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_BaseAsync_await(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_ETask_bind___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_BaseAsync_bind___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_concurrently___redArg___lam__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_BaseAsync_async___redArg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnitOfInhabited___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnitOfInhabited___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_BaseAsync_asTask___redArg(lean_object*, lean_object*, lean_object*);
lean_object* l_Functor_mapRev___redArg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_bind___redArg(lean_object*, lean_object*, lean_object*);
@ -380,7 +375,6 @@ LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_ofTask(lean_object*, lea
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_pure(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_BaseAsync_instInhabited(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_ETask_bind___redArg(lean_object*, lean_object*, lean_object*, uint8_t);
static lean_object* l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__1;
static lean_object* l_Std_Internal_IO_Async_EAsync_instMonadExcept___closed__0;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_race___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_ETask_getState(lean_object*, lean_object*, lean_object*, lean_object*);
@ -394,7 +388,6 @@ LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instMonadExcept___lam__1
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_ETask_getState___redArg___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_bind___redArg___lam__0(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_AsyncTask_bind(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnitOfInhabited___lam__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_ETask_bindEIO___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_AsyncTask_bindIO___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instMonadLiftEIO__1___lam__0(lean_object*, lean_object*, lean_object*);
@ -409,6 +402,7 @@ LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_ETask_instMonad___lam__3(lean_o
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_BaseAsync_mk___redArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_AsyncTask_mapTaskIO___redArg(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
LEAN_EXPORT lean_object* l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_BaseAsync_bind_bindAsyncTask(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnit___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_instMonadAwaitStateTOfMonad___redArg___lam__0(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -7939,41 +7933,6 @@ lean_closure_set(x_3, 0, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__0() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_box(0);
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_box(0);
x_2 = lean_alloc_closure((void*)(l_Function_const___boxed), 4, 3);
lean_closure_set(x_2, 0, lean_box(0));
lean_closure_set(x_2, 1, lean_box(0));
lean_closure_set(x_2, 2, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__1;
x_2 = lean_alloc_closure((void*)(l_Except_map), 5, 4);
lean_closure_set(x_2, 0, lean_box(0));
lean_closure_set(x_2, 1, lean_box(0));
lean_closure_set(x_2, 2, lean_box(0));
lean_closure_set(x_2, 3, x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
@ -7985,204 +7944,129 @@ lean_dec_ref(x_2);
x_6 = !lean_is_exclusive(x_4);
if (x_6 == 0)
{
lean_object* x_7; uint8_t x_8;
lean_ctor_set_tag(x_4, 1);
lean_object* x_7;
x_7 = lean_io_promise_resolve(x_4, x_1, x_5);
lean_dec(x_1);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = lean_ctor_get(x_7, 0);
x_10 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_10, 0, x_9);
x_11 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_7, 0, x_11);
return x_7;
}
else
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_12 = lean_ctor_get(x_7, 0);
x_13 = lean_ctor_get(x_7, 1);
lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_8 = lean_ctor_get(x_4, 0);
lean_inc(x_8);
lean_dec(x_4);
x_9 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_9, 0, x_8);
x_10 = lean_io_promise_resolve(x_9, x_1, x_5);
lean_dec(x_1);
return x_10;
}
}
else
{
uint8_t x_11;
x_11 = !lean_is_exclusive(x_4);
if (x_11 == 0)
{
lean_object* x_12;
x_12 = lean_ctor_get(x_4, 0);
if (lean_obj_tag(x_12) == 0)
{
lean_object* x_13; lean_object* x_14;
lean_dec(x_3);
lean_dec_ref(x_2);
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
lean_inc(x_12);
lean_dec(x_7);
x_14 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_14, 0, x_12);
x_15 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_15, 0, x_14);
x_16 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_16, 0, x_15);
lean_ctor_set(x_16, 1, x_13);
lean_dec_ref(x_12);
lean_ctor_set(x_4, 0, x_13);
x_14 = lean_io_promise_resolve(x_4, x_1, x_5);
lean_dec(x_1);
return x_14;
}
else
{
lean_object* x_15; lean_object* x_16;
lean_free_object(x_4);
x_15 = lean_ctor_get(x_12, 0);
lean_inc(x_15);
lean_dec_ref(x_12);
x_16 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg(x_2, x_3, x_1, x_15, x_5);
return x_16;
}
}
else
{
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; lean_object* x_25;
lean_object* x_17;
x_17 = lean_ctor_get(x_4, 0);
lean_inc(x_17);
lean_dec(x_4);
x_18 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_18, 0, x_17);
x_19 = lean_io_promise_resolve(x_18, x_1, x_5);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_dec(x_3);
lean_dec_ref(x_2);
x_18 = lean_ctor_get(x_17, 0);
lean_inc(x_18);
lean_dec_ref(x_17);
x_19 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_19, 0, x_18);
x_20 = lean_io_promise_resolve(x_19, x_1, x_5);
lean_dec(x_1);
x_20 = lean_ctor_get(x_19, 0);
lean_inc(x_20);
x_21 = lean_ctor_get(x_19, 1);
return x_20;
}
else
{
lean_object* x_21; lean_object* x_22;
x_21 = lean_ctor_get(x_17, 0);
lean_inc(x_21);
if (lean_is_exclusive(x_19)) {
lean_ctor_release(x_19, 0);
lean_ctor_release(x_19, 1);
x_22 = x_19;
} else {
lean_dec_ref(x_19);
x_22 = lean_box(0);
}
x_23 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_23, 0, x_20);
x_24 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_24, 0, x_23);
if (lean_is_scalar(x_22)) {
x_25 = lean_alloc_ctor(0, 2, 0);
} else {
x_25 = x_22;
}
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_21);
return x_25;
lean_dec_ref(x_17);
x_22 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg(x_2, x_3, x_1, x_21, x_5);
return x_22;
}
}
else
{
lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_35;
x_26 = lean_ctor_get(x_4, 0);
lean_inc(x_26);
if (lean_is_exclusive(x_4)) {
lean_ctor_release(x_4, 0);
x_27 = x_4;
} else {
lean_dec_ref(x_4);
x_27 = lean_box(0);
}
x_28 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg(x_2, x_3, x_1, x_26, x_5);
x_29 = lean_ctor_get(x_28, 1);
lean_inc(x_29);
if (lean_is_exclusive(x_28)) {
lean_ctor_release(x_28, 0);
lean_ctor_release(x_28, 1);
x_30 = x_28;
} else {
lean_dec_ref(x_28);
x_30 = lean_box(0);
}
x_35 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__0;
x_31 = x_35;
goto block_34;
block_34:
{
lean_object* x_32; lean_object* x_33;
if (lean_is_scalar(x_27)) {
x_32 = lean_alloc_ctor(0, 1, 0);
} else {
x_32 = x_27;
lean_ctor_set_tag(x_32, 0);
}
lean_ctor_set(x_32, 0, x_31);
if (lean_is_scalar(x_30)) {
x_33 = lean_alloc_ctor(0, 2, 0);
} else {
x_33 = x_30;
}
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_29);
return x_33;
}
}
}
}
LEAN_EXPORT lean_object* l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__1(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
lean_dec_ref(x_1);
x_3 = lean_task_pure(x_2);
return x_3;
}
else
{
lean_object* x_4;
x_4 = lean_ctor_get(x_1, 0);
lean_inc_ref(x_4);
lean_dec_ref(x_1);
return x_4;
}
}
}
LEAN_EXPORT lean_object* l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12;
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_6 = lean_box(0);
lean_inc_ref(x_1);
x_7 = lean_apply_3(x_1, x_6, x_4, x_5);
x_8 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
x_9 = lean_ctor_get(x_7, 1);
lean_inc(x_9);
lean_dec_ref(x_7);
lean_inc(x_2);
lean_inc_ref(x_1);
x_6 = lean_alloc_closure((void*)(l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0), 5, 3);
lean_closure_set(x_6, 0, x_3);
lean_closure_set(x_6, 1, x_1);
lean_closure_set(x_6, 2, x_2);
x_7 = lean_box(0);
x_8 = lean_apply_2(x_1, x_7, x_4);
x_9 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_EAsync_bind), 6, 5);
lean_closure_set(x_9, 0, lean_box(0));
lean_closure_set(x_9, 1, lean_box(0));
lean_closure_set(x_9, 2, lean_box(0));
lean_closure_set(x_9, 3, x_8);
lean_closure_set(x_9, 4, x_6);
x_10 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_BaseAsync_toRawBaseIO), 3, 2);
lean_closure_set(x_10, 0, lean_box(0));
lean_closure_set(x_10, 1, x_9);
x_11 = lean_io_as_task(x_10, x_2, x_5);
x_12 = !lean_is_exclusive(x_11);
if (x_12 == 0)
lean_inc(x_3);
x_10 = lean_alloc_closure((void*)(l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0), 5, 3);
lean_closure_set(x_10, 0, x_3);
lean_closure_set(x_10, 1, x_1);
lean_closure_set(x_10, 2, x_2);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_13 = lean_ctor_get(x_11, 0);
x_14 = lean_alloc_closure((void*)(l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__1), 1, 0);
x_15 = lean_unsigned_to_nat(0u);
x_16 = 1;
x_17 = lean_task_bind(x_13, x_14, x_15, x_16);
x_18 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_18, 0, x_17);
x_19 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_19, 0, x_18);
lean_ctor_set(x_11, 0, x_19);
return x_11;
lean_object* x_11; lean_object* x_12;
lean_dec_ref(x_10);
x_11 = lean_ctor_get(x_8, 0);
lean_inc(x_11);
lean_dec_ref(x_8);
x_12 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0(x_3, x_1, x_2, x_11, x_9);
return x_12;
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_20 = lean_ctor_get(x_11, 0);
x_21 = lean_ctor_get(x_11, 1);
lean_inc(x_21);
lean_inc(x_20);
lean_dec(x_11);
x_22 = lean_alloc_closure((void*)(l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__1), 1, 0);
x_23 = lean_unsigned_to_nat(0u);
x_24 = 1;
x_25 = lean_task_bind(x_20, x_22, x_23, x_24);
x_26 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_26, 0, x_25);
x_27 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_27, 0, x_26);
x_28 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_28, 0, x_27);
lean_ctor_set(x_28, 1, x_21);
return x_28;
lean_object* x_13; uint8_t x_14; lean_object* x_15;
lean_dec(x_3);
lean_dec_ref(x_1);
x_13 = lean_ctor_get(x_8, 0);
lean_inc_ref(x_13);
lean_dec_ref(x_8);
x_14 = 0;
x_15 = l_BaseIO_chainTask___redArg(x_13, x_10, x_2, x_14, x_9);
return x_15;
}
}
}
@ -8279,35 +8163,52 @@ return x_12;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_22; lean_object* x_25;
x_13 = lean_ctor_get(x_4, 0);
lean_inc(x_13);
lean_dec_ref(x_4);
lean_inc(x_13);
x_14 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg(x_1, x_2, x_13, x_3, x_5);
x_15 = lean_ctor_get(x_14, 1);
lean_inc(x_15);
lean_dec_ref(x_14);
x_16 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_EAsync_forIn___redArg___lam__0___boxed), 3, 1);
lean_closure_set(x_16, 0, x_13);
x_25 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__0;
x_22 = x_25;
goto block_24;
block_21:
uint8_t x_13;
x_13 = !lean_is_exclusive(x_4);
if (x_13 == 0)
{
lean_object* x_18; uint8_t x_19; lean_object* x_20;
x_18 = lean_unsigned_to_nat(0u);
x_19 = 0;
x_20 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_BaseAsync_bind_bindAsyncTask___redArg(x_18, x_19, x_17, x_16, x_15);
return x_20;
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; uint8_t x_21; lean_object* x_22;
x_14 = lean_ctor_get(x_4, 0);
lean_inc(x_14);
x_15 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg(x_1, x_2, x_14, x_3, x_5);
x_16 = lean_ctor_get(x_15, 0);
lean_inc(x_16);
x_17 = lean_ctor_get(x_15, 1);
lean_inc(x_17);
lean_dec_ref(x_15);
x_18 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_EAsync_forIn___redArg___lam__0___boxed), 3, 1);
lean_closure_set(x_18, 0, x_14);
lean_ctor_set(x_4, 0, x_16);
x_19 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_19, 0, x_4);
x_20 = lean_unsigned_to_nat(0u);
x_21 = 0;
x_22 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_BaseAsync_bind_bindAsyncTask___redArg(x_20, x_21, x_19, x_18, x_17);
return x_22;
}
block_24:
else
{
lean_object* x_23;
x_23 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_23, 0, x_22);
x_17 = x_23;
goto block_21;
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31; lean_object* x_32;
x_23 = lean_ctor_get(x_4, 0);
lean_inc(x_23);
lean_dec(x_4);
lean_inc(x_23);
x_24 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg(x_1, x_2, x_23, x_3, x_5);
x_25 = lean_ctor_get(x_24, 0);
lean_inc(x_25);
x_26 = lean_ctor_get(x_24, 1);
lean_inc(x_26);
lean_dec_ref(x_24);
x_27 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_EAsync_forIn___redArg___lam__0___boxed), 3, 1);
lean_closure_set(x_27, 0, x_23);
x_28 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_28, 0, x_25);
x_29 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_29, 0, x_28);
x_30 = lean_unsigned_to_nat(0u);
x_31 = 0;
x_32 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_BaseAsync_bind_bindAsyncTask___redArg(x_30, x_31, x_29, x_27, x_26);
return x_32;
}
}
}
@ -8336,100 +8237,28 @@ x_13 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_BaseAsync_b
return x_13;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_forIn___lam__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_forIn(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
if (lean_obj_tag(x_4) == 0)
{
uint8_t x_6;
lean_dec(x_3);
lean_dec(x_2);
lean_dec_ref(x_1);
x_6 = !lean_is_exclusive(x_4);
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8;
x_7 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_7, 0, x_4);
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_5);
return x_8;
}
else
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_4, 0);
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; lean_object* x_15;
x_7 = lean_io_promise_new(x_6);
x_8 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
x_9 = lean_ctor_get(x_7, 1);
lean_inc(x_9);
lean_dec(x_4);
x_10 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_10, 0, x_9);
x_11 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_11, 0, x_10);
x_12 = lean_alloc_ctor(0, 2, 0);
lean_dec_ref(x_7);
x_10 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_EAsync_forIn___redArg___lam__1), 5, 3);
lean_closure_set(x_10, 0, x_4);
lean_closure_set(x_10, 1, x_5);
lean_closure_set(x_10, 2, x_3);
x_11 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_11, 0, x_8);
x_12 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_12, 0, x_11);
lean_ctor_set(x_12, 1, x_5);
return x_12;
}
}
else
{
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_23; lean_object* x_26;
x_13 = lean_ctor_get(x_4, 0);
lean_inc(x_13);
lean_dec_ref(x_4);
lean_inc(x_13);
x_14 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg(x_1, x_2, x_13, x_3, x_5);
x_15 = lean_ctor_get(x_14, 1);
lean_inc(x_15);
lean_dec_ref(x_14);
x_16 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_EAsync_forIn___redArg___lam__0___boxed), 3, 1);
lean_closure_set(x_16, 0, x_13);
x_26 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__0;
x_23 = x_26;
goto block_25;
block_22:
{
lean_object* x_19; uint8_t x_20; lean_object* x_21;
x_19 = lean_unsigned_to_nat(0u);
x_20 = 0;
x_21 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_BaseAsync_bind_bindAsyncTask___redArg(x_19, x_20, x_17, x_16, x_18);
return x_21;
}
block_25:
{
lean_object* x_24;
x_24 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_24, 0, x_23);
x_17 = x_24;
x_18 = x_15;
goto block_22;
}
}
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_forIn(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; uint8_t x_15; lean_object* x_16;
x_8 = lean_io_promise_new(x_7);
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
x_10 = lean_ctor_get(x_8, 1);
lean_inc(x_10);
lean_dec_ref(x_8);
x_11 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_EAsync_forIn___lam__1), 5, 3);
lean_closure_set(x_11, 0, x_5);
lean_closure_set(x_11, 1, x_6);
lean_closure_set(x_11, 2, x_4);
x_12 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_12, 0, x_9);
x_13 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_13, 0, x_12);
x_14 = lean_unsigned_to_nat(0u);
x_15 = 0;
x_16 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_BaseAsync_bind_bindAsyncTask___redArg(x_14, x_15, x_13, x_11, x_10);
return x_16;
x_13 = lean_unsigned_to_nat(0u);
x_14 = 0;
x_15 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_BaseAsync_bind_bindAsyncTask___redArg(x_13, x_14, x_12, x_10, x_9);
return x_15;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_forIn___redArg___lam__0___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@ -8441,16 +8270,7 @@ lean_dec(x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_forIn___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8;
x_8 = l_Std_Internal_IO_Async_EAsync_forIn(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_3);
return x_8;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnitOfInhabited___lam__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnit___lam__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
if (lean_obj_tag(x_4) == 0)
@ -8488,40 +8308,57 @@ return x_12;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_21; lean_object* x_24;
x_13 = lean_ctor_get(x_4, 0);
lean_inc(x_13);
lean_dec_ref(x_4);
lean_inc(x_13);
uint8_t x_13;
x_13 = !lean_is_exclusive(x_4);
if (x_13 == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; lean_object* x_21;
x_14 = lean_ctor_get(x_4, 0);
lean_inc(x_14);
lean_inc(x_2);
x_14 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg(x_1, x_2, x_13, x_3, x_5);
x_15 = lean_ctor_get(x_14, 1);
lean_inc(x_15);
lean_dec_ref(x_14);
x_16 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_EAsync_forIn___redArg___lam__0___boxed), 3, 1);
lean_closure_set(x_16, 0, x_13);
x_24 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__0;
x_21 = x_24;
goto block_23;
block_20:
x_15 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg(x_1, x_2, x_14, x_3, x_5);
x_16 = lean_ctor_get(x_15, 0);
lean_inc(x_16);
x_17 = lean_ctor_get(x_15, 1);
lean_inc(x_17);
lean_dec_ref(x_15);
x_18 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_EAsync_forIn___redArg___lam__0___boxed), 3, 1);
lean_closure_set(x_18, 0, x_14);
lean_ctor_set(x_4, 0, x_16);
x_19 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_19, 0, x_4);
x_20 = 0;
x_21 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_BaseAsync_bind_bindAsyncTask___redArg(x_2, x_20, x_19, x_18, x_17);
return x_21;
}
else
{
uint8_t x_18; lean_object* x_19;
x_18 = 0;
x_19 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_BaseAsync_bind_bindAsyncTask___redArg(x_2, x_18, x_17, x_16, x_15);
return x_19;
}
block_23:
{
lean_object* x_22;
x_22 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_22, 0, x_21);
x_17 = x_22;
goto block_20;
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; uint8_t x_29; lean_object* x_30;
x_22 = lean_ctor_get(x_4, 0);
lean_inc(x_22);
lean_dec(x_4);
lean_inc(x_22);
lean_inc(x_2);
x_23 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg(x_1, x_2, x_22, x_3, x_5);
x_24 = lean_ctor_get(x_23, 0);
lean_inc(x_24);
x_25 = lean_ctor_get(x_23, 1);
lean_inc(x_25);
lean_dec_ref(x_23);
x_26 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_EAsync_forIn___redArg___lam__0___boxed), 3, 1);
lean_closure_set(x_26, 0, x_22);
x_27 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_27, 0, x_24);
x_28 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_28, 0, x_27);
x_29 = 0;
x_30 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_BaseAsync_bind_bindAsyncTask___redArg(x_2, x_29, x_28, x_26, x_25);
return x_30;
}
}
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnitOfInhabited___lam__0(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnit___lam__0(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; lean_object* x_15;
@ -8532,7 +8369,7 @@ x_9 = lean_ctor_get(x_7, 1);
lean_inc(x_9);
lean_dec_ref(x_7);
x_10 = lean_unsigned_to_nat(0u);
x_11 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_EAsync_instForInLoopUnitOfInhabited___lam__1), 5, 3);
x_11 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_EAsync_instForInLoopUnit___lam__1), 5, 3);
lean_closure_set(x_11, 0, x_5);
lean_closure_set(x_11, 1, x_10);
lean_closure_set(x_11, 2, x_4);
@ -8545,32 +8382,23 @@ x_15 = l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_BaseAsync_b
return x_15;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnitOfInhabited(lean_object* x_1, lean_object* x_2) {
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnit(lean_object* x_1) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_EAsync_instForInLoopUnitOfInhabited___lam__0___boxed), 6, 0);
return x_3;
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_EAsync_instForInLoopUnit___lam__0___boxed), 6, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnitOfInhabited___lam__0___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnit___lam__0___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_Std_Internal_IO_Async_EAsync_instForInLoopUnitOfInhabited___lam__0(x_1, x_2, x_3, x_4, x_5, x_6);
x_7 = l_Std_Internal_IO_Async_EAsync_instForInLoopUnit___lam__0(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec_ref(x_2);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_EAsync_instForInLoopUnitOfInhabited___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Std_Internal_IO_Async_EAsync_instForInLoopUnitOfInhabited(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_Async_toIO___redArg(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -8761,7 +8589,7 @@ lean_dec_ref(x_2);
x_8 = lean_ctor_get(x_6, 1);
lean_inc_ref(x_8);
lean_dec_ref(x_6);
x_9 = lean_apply_3(x_7, lean_box(0), x_4, x_3);
x_9 = lean_apply_3(x_7, lean_box(0), x_3, x_4);
x_10 = lean_box(0);
x_11 = lean_apply_4(x_8, lean_box(0), lean_box(0), x_10, x_9);
return x_11;
@ -8783,7 +8611,7 @@ lean_dec_ref(x_5);
x_11 = lean_ctor_get(x_9, 1);
lean_inc_ref(x_11);
lean_dec_ref(x_9);
x_12 = lean_apply_3(x_10, lean_box(0), x_7, x_6);
x_12 = lean_apply_3(x_10, lean_box(0), x_6, x_7);
x_13 = lean_box(0);
x_14 = lean_apply_4(x_11, lean_box(0), lean_box(0), x_13, x_12);
return x_14;
@ -9337,12 +9165,6 @@ l_Std_Internal_IO_Async_EAsync_instMonadAwaitAsyncTaskError = _init_l_Std_Intern
lean_mark_persistent(l_Std_Internal_IO_Async_EAsync_instMonadAwaitAsyncTaskError);
l_Std_Internal_IO_Async_EAsync_instMonadAsyncAsyncTaskError = _init_l_Std_Internal_IO_Async_EAsync_instMonadAsyncAsyncTaskError();
lean_mark_persistent(l_Std_Internal_IO_Async_EAsync_instMonadAsyncAsyncTaskError);
l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__0 = _init_l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__0();
lean_mark_persistent(l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__0);
l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__1 = _init_l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__1();
lean_mark_persistent(l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__1);
l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__2 = _init_l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__2();
lean_mark_persistent(l___private_Std_Internal_Async_Basic_0__Std_Internal_IO_Async_EAsync_forIn_loop___redArg___lam__0___closed__2);
l_Std_Internal_IO_Async_Async_instMonadAsyncAsyncTask = _init_l_Std_Internal_IO_Async_Async_instMonadAsyncAsyncTask();
lean_mark_persistent(l_Std_Internal_IO_Async_Async_instMonadAsyncAsyncTask);
l_Std_Internal_IO_Async_Async_instMonadAwaitAsyncTask = _init_l_Std_Internal_IO_Async_Async_instMonadAwaitAsyncTask();