diff --git a/src/stage0/init/core.cpp b/src/stage0/init/core.cpp index 53590ee280..e07448c2a2 100644 --- a/src/stage0/init/core.cpp +++ b/src/stage0/init/core.cpp @@ -14,19 +14,17 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #pragma GCC diagnostic ignored "-Wunused-label" #pragma GCC diagnostic ignored "-Wunused-but-set-variable" #endif +uint8 l_xor(uint8, uint8); obj* l_cast___rarg(obj*); obj* l_Or_Decidable___rarg___boxed(obj*, obj*); obj* l_Sum_DecidableEq___boxed(obj*, obj*); obj* l_Eq_ndrecOn___boxed(obj*, obj*, obj*, obj*, obj*); obj* l_Iff_Decidable(obj*, obj*); obj* l_Prod_DecidableEq(obj*, obj*); -uint8 l_bor___main(uint8, uint8); obj* l_Quot_recOnSubsingleton___boxed(obj*, obj*, obj*, obj*); -obj* l_bor___boxed(obj*, obj*); obj* l_Quotient_liftOn___rarg(obj*, obj*, obj*); obj* l_Sigma_sizeof___main___rarg(obj*, obj*, obj*); obj* l_Prod_sizeof___main(obj*, obj*); -uint8 l_band___main(uint8, uint8); obj* l_Function_onFun(obj*, obj*, obj*); obj* l_PSigma_sizeof___main___at_PSigma_HasSizeof___spec__2(obj*, obj*); obj* l_idDelta___rarg___boxed(obj*); @@ -40,8 +38,8 @@ obj* l_Fun_Inhabited___rarg___boxed(obj*, obj*); obj* l_Quot_rec___rarg___boxed(obj*, obj*, obj*); obj* l_Not_Decidable(obj*); obj* l_Decidable_recOnTrue___rarg___boxed(obj*, obj*, obj*, obj*, obj*); -obj* l_bxor___boxed(obj*, obj*); obj* l_cond___boxed(obj*); +uint8 l_or(uint8, uint8); obj* l_prodHasDecidableLt(obj*, obj*, obj*, obj*); obj* l_ite_Decidable___boxed(obj*, obj*, obj*); obj* l_Xor_Decidable___boxed(obj*, obj*); @@ -58,6 +56,7 @@ uint8 l_Bool_DecidableEq(uint8, uint8); obj* l_Function_onFun___boxed(obj*, obj*, obj*); obj* l_inline(obj*); obj* l_Nat_HasSizeof; +obj* l_beqOfEq(obj*); obj* l_List_sizeof___main___boxed(obj*); obj* l_PSum_HasSizeof___rarg(obj*, obj*); obj* l_Sigma_sizeof___boxed(obj*, obj*); @@ -84,14 +83,12 @@ obj* l_arbitrary___rarg___boxed(obj*); obj* l_Sigma_sizeof___rarg(obj*, obj*, obj*); obj* l_Sigma_sizeof___main(obj*, obj*); obj* l_cast___rarg___boxed(obj*); -obj* l_bxor___main___boxed(obj*, obj*); obj* l_Function_onFun___rarg(obj*, obj*, obj*, obj*); obj* l_Prod_map___main___boxed(obj*, obj*, obj*, obj*); obj* l_Thunk_map___boxed(obj*, obj*, obj*, obj*); obj* l_Quotient_hrecOn___rarg(obj*, obj*, obj*); obj* l_Prod_HasLt___boxed(obj*, obj*, obj*, obj*); obj* l_Function_comp___rarg(obj*, obj*, obj*); -obj* l_bor___main___boxed(obj*, obj*); obj* l_List_sizeof___main(obj*); obj* l_inferInstanceAs___boxed(obj*); obj* l_Sum_inhabitedRight___rarg(obj*); @@ -108,13 +105,14 @@ obj* l_singleton___rarg(obj*, obj*, obj*); obj* l_decidableOfDecidableOfIff___rarg___boxed(obj*, obj*); obj* l_True_Decidable___boxed; obj* l_decidableOfDecidableEq___boxed(obj*); +uint8 l_and(uint8, uint8); obj* l_ite___rarg___boxed(obj*, obj*, obj*, obj*); +obj* l_or___main___boxed(obj*, obj*); obj* l___private_init_core_22__extfunApp(obj*, obj*); obj* l_Option_HasSizeof___rarg(obj*); obj* l_Subtype_sizeof___main___rarg(obj*, obj*, obj*); obj* l_Not_Decidable___rarg___boxed(obj*); obj* l_id___rarg___boxed(obj*); -uint8 l_bxor___main(uint8, uint8); obj* l_PSum_sizeof___main___boxed(obj*, obj*); obj* l_setoidHasEquiv(obj*, obj*); obj* l_Nat_sizeof___main___boxed(obj*); @@ -128,6 +126,7 @@ obj* l_default_sizeof___boxed(obj*, obj*); obj* l_decidableOfDecidableOfEq___rarg___boxed(obj*, obj*); obj* l_dite_Decidable___rarg(uint8, obj*, obj*); obj* l_PUnit_sizeof___main___boxed(obj*); +obj* l_beqOfEq___boxed(obj*); obj* l_typedExpr(obj*); obj* l_dite_Decidable___boxed(obj*, obj*, obj*); obj* l_Eq_mpr(obj*, obj*, obj*); @@ -147,14 +146,12 @@ obj* l_Sigma_HasSizeof___boxed(obj*, obj*); obj* l___private_init_core_22__extfunApp___boxed(obj*, obj*); obj* l_std_priority_default; obj* l_Quotient_DecidableEq___rarg(obj*, obj*, obj*, obj*); -obj* l_Unit_star; obj* l_arbitrary___rarg(obj*); obj* l_Prod_HasSizeof(obj*, obj*); obj* l_Prod_DecidableEq___boxed(obj*, obj*); obj* l_Subtype_sizeof___main(obj*); obj* l_Quot_recOnSubsingleton(obj*, obj*, obj*, obj*); obj* l_Prod_HasSizeof___boxed(obj*, obj*); -obj* l_band___boxed(obj*, obj*); obj* l_Quotient_liftOn___boxed(obj*, obj*, obj*); obj* l_PSum_sizeof(obj*, obj*); obj* l_Task_map___boxed(obj*, obj*, obj*, obj*); @@ -174,6 +171,7 @@ obj* l_Fun_Inhabited___boxed(obj*, obj*); obj* l_dite___rarg___boxed(obj*, obj*, obj*, obj*); obj* l_List_sizeof___boxed(obj*); obj* l_Quotient_lift_u_2082___boxed(obj*, obj*, obj*, obj*, obj*); +obj* l_Unit_unit; obj* l_idDelta(obj*); obj* l_PUnit_Inhabited; obj* l_Xor_Decidable___rarg___boxed(obj*, obj*); @@ -185,12 +183,13 @@ obj* l_Pi_Inhabited(obj*, obj*); obj* l_Quotient_recOn(obj*, obj*, obj*); obj* l_Subtype_Inhabited___rarg___boxed(obj*, obj*); obj* l_Quot_indep___rarg(obj*, obj*); +obj* l_not___boxed(obj*); obj* l_Nat_sizeof___main(obj*); +obj* l_xor___boxed(obj*, obj*); obj* l_Prod_Inhabited(obj*, obj*); obj* l_PSigma_HasSizeof(obj*, obj*); obj* l_dite_Decidable___rarg___boxed(obj*, obj*, obj*); obj* l_And_Decidable___boxed(obj*, obj*); -uint8 l_bnot___main(uint8); obj* l_Function_comp___boxed(obj*, obj*, obj*); obj* l_Quot_indep(obj*, obj*, obj*); obj* l_Not_Decidable___boxed(obj*); @@ -199,6 +198,7 @@ obj* l_List_HasSizeof___rarg(obj*); obj* l_ite_Decidable___rarg___boxed(obj*, obj*, obj*); obj* l_decidableOfDecidableEq___rarg(obj*, obj*, obj*); obj* l_Subtype_sizeof___main___rarg___boxed(obj*, obj*, obj*); +uint8 l_beqOfEq___rarg(obj*, obj*, obj*); obj* l_default_sizeof___main___boxed(obj*, obj*); obj* l_default___rarg(obj*); obj* l_implies_Decidable___boxed(obj*, obj*); @@ -214,7 +214,6 @@ obj* l_Prod_sizeof___main___rarg(obj*, obj*, obj*); obj* l_Quot_recOn___rarg___boxed(obj*, obj*, obj*); obj* l_Quotient_liftOn___rarg___boxed(obj*, obj*, obj*); obj* l_Prod_Inhabited___boxed(obj*, obj*); -obj* l_band___main___boxed(obj*, obj*); obj* l_Quotient_hrecOn(obj*, obj*, obj*); obj* l_Option_sizeof___main___rarg(obj*, obj*); obj* l_cond___main___boxed(obj*); @@ -256,7 +255,7 @@ obj* nat_add(obj*, obj*); } obj* l_Subtype_sizeof___boxed(obj*); obj* l_PSigma_sizeof___boxed(obj*, obj*); -obj* l_bnot___boxed(obj*); +uint8 l_not___main(uint8); obj* l_Quot_liftOn___rarg___boxed(obj*, obj*, obj*); obj* l_PUnit_sizeof___main(obj*); uint8 l_Or_Decidable___rarg(uint8, uint8); @@ -292,6 +291,7 @@ obj* l_Eq_mpr___rarg___boxed(obj*); obj* l_List_sizeof(obj*); obj* l_Option_sizeof___boxed(obj*); obj* l_decidableOfDecidableEq(obj*); +uint8 l_and___main(uint8, uint8); obj* l_Decidable_byCases___rarg(uint8, obj*, obj*); uint8 l_Iff_Decidable___rarg(uint8, uint8); obj* l_Sum_HasSizeof___boxed(obj*, obj*); @@ -348,8 +348,8 @@ obj* l_Prod_sizeof___main___boxed(obj*, obj*); obj* l_Option_sizeof___rarg(obj*, obj*); obj* l_Sum_DecidableEq___rarg___boxed(obj*, obj*, obj*, obj*); uint8 l_And_Decidable___rarg(uint8, uint8); -uint8 l_band(uint8, uint8); obj* l_flip(obj*, obj*, obj*); +obj* l_not___main___boxed(obj*); obj* l_PSigma_sizeof___at_PSigma_HasSizeof___spec__1___boxed(obj*, obj*); obj* l_std_prec_max; obj* l_True_Inhabited; @@ -357,6 +357,7 @@ obj* l_Bool_sizeof___main___boxed(obj*); obj* l_cond___main(obj*); obj* l_Function_swap___boxed(obj*, obj*, obj*); obj* l_Function_combine___rarg(obj*, obj*, obj*, obj*, obj*); +uint8 l_not(uint8); uint8 l_decidableOfDecidableOfEq___rarg(uint8, obj*); uint8 l_False_Decidable; obj* l_Quotient_rec___rarg(obj*, obj*, obj*); @@ -369,13 +370,14 @@ obj* l_Sum_HasSizeof(obj*, obj*); obj* l_Function_const___rarg(obj*, obj*); obj* l_Eq_ndrec(obj*, obj*, obj*); obj* l_Subtype_HasSizeof___boxed(obj*); +uint8 l_xor___main(uint8, uint8); obj* l_idRhs___rarg___boxed(obj*); obj* l_Quotient_recOnSubsingleton_u_2082___at_Quotient_DecidableEq___spec__1(obj*, obj*); obj* l_Subtype_sizeof___rarg___boxed(obj*, obj*, obj*); -uint8 l_bxor(uint8, uint8); obj* l_default(obj*); obj* l_Quotient_recOn___boxed(obj*, obj*, obj*); obj* l_Ne_Decidable___rarg___boxed(obj*, obj*, obj*); +obj* l_and___boxed(obj*, obj*); obj* l_Subtype_sizeof(obj*); obj* l_inferInstance___boxed(obj*); uint8 l_Subtype_DecidableEq___rarg(obj*, obj*, obj*); @@ -387,6 +389,7 @@ obj* l_Quotient_lift___boxed(obj*, obj*, obj*); obj* l_idRhs(obj*); obj* l_Eq_mp___boxed(obj*, obj*, obj*); obj* l_Quot_hrecOn(obj*, obj*, obj*); +obj* l_and___main___boxed(obj*, obj*); obj* l_List_sizeof___main___rarg(obj*, obj*); obj* l_Quotient_mk___rarg___boxed(obj*); obj* l_Quot_rec___rarg(obj*, obj*, obj*); @@ -406,7 +409,6 @@ obj* l_Decidable_recOnTrue(obj*); obj* l_PSigma_sizeof___main___at_PSigma_HasSizeof___spec__2___rarg(obj*, obj*, obj*); obj* l_Prod_HasLt(obj*, obj*, obj*, obj*); obj* l_Nat_HasAdd; -uint8 l_bor(uint8, uint8); obj* l_Subtype_Inhabited___rarg(obj*, obj*); obj* l_Quot_hrecOn___rarg___boxed(obj*, obj*, obj*); obj* l_PUnit_DecidableEq___boxed(obj*, obj*); @@ -427,14 +429,14 @@ obj* l_Decidable_recOnTrue___rarg(uint8, obj*, obj*, obj*, obj*); obj* l_Eq_mp___rarg___boxed(obj*); obj* l_PSigma_sizeof___main(obj*, obj*); obj* l_inferInstance(obj*); -uint8 l_bnot(uint8); obj* l_absurd(obj*, obj*, obj*, obj*); +obj* l_xor___main___boxed(obj*, obj*); uint8 l_decidableOfDecidableOfIff___rarg(uint8, obj*); obj* l_Decidable_toBool___boxed(obj*); +obj* l_beqOfEq___rarg___boxed(obj*, obj*, obj*); obj* l_PSigma_sizeof___rarg(obj*, obj*, obj*); obj* l_Decidable_byCases(obj*, obj*); obj* l_Ne_Decidable___boxed(obj*); -obj* l_bnot___main___boxed(obj*); obj* l_arbitrary(obj*); obj* l_Sum_sizeof___rarg(obj*, obj*, obj*); obj* l_Quotient_liftOn_u_2082___boxed(obj*, obj*, obj*, obj*, obj*); @@ -450,6 +452,7 @@ obj* l_Sum_inhabitedLeft(obj*, obj*); obj* l_Function_swap___rarg(obj*, obj*, obj*); obj* l_cond(obj*); obj* l_Option_HasSizeof___boxed(obj*); +obj* l_or___boxed(obj*, obj*); obj* l_PSigma_sizeof(obj*, obj*); obj* l_Subtype_Inhabited___boxed(obj*, obj*); obj* l_Decidable_recOnTrue___boxed(obj*); @@ -460,6 +463,7 @@ obj* l_Quot_recOn(obj*, obj*, obj*); obj* l_implies_Decidable(obj*, obj*); obj* l_setoidHasEquiv___boxed(obj*, obj*); obj* l_Sigma_sizeof___at_Sigma_HasSizeof___spec__1___boxed(obj*, obj*); +uint8 l_or___main(uint8, uint8); obj* l___private_init_core_21__funSetoid___boxed(obj*, obj*); obj* l_Or_Decidable___boxed(obj*, obj*); obj* l_Decidable_recOnFalse___boxed(obj*); @@ -657,7 +661,7 @@ lean::dec(x_0); return x_1; } } -obj* _init_l_Unit_star() { +obj* _init_l_Unit_unit() { _start: { obj* x_0; @@ -2243,7 +2247,7 @@ lean::dec(x_0); return x_1; } } -uint8 l_bor___main(uint8 x_0, uint8 x_1) { +uint8 l_or___main(uint8 x_0, uint8 x_1) { _start: { if (x_0 == 0) @@ -2256,18 +2260,18 @@ return x_0; } } } -obj* l_bor___main___boxed(obj* x_0, obj* x_1) { +obj* l_or___main___boxed(obj* x_0, obj* x_1) { _start: { uint8 x_2; uint8 x_3; uint8 x_4; obj* x_5; x_2 = lean::unbox(x_0); x_3 = lean::unbox(x_1); -x_4 = l_bor___main(x_2, x_3); +x_4 = l_or___main(x_2, x_3); x_5 = lean::box(x_4); return x_5; } } -uint8 l_bor(uint8 x_0, uint8 x_1) { +uint8 l_or(uint8 x_0, uint8 x_1) { _start: { if (x_0 == 0) @@ -2280,18 +2284,18 @@ return x_0; } } } -obj* l_bor___boxed(obj* x_0, obj* x_1) { +obj* l_or___boxed(obj* x_0, obj* x_1) { _start: { uint8 x_2; uint8 x_3; uint8 x_4; obj* x_5; x_2 = lean::unbox(x_0); x_3 = lean::unbox(x_1); -x_4 = l_bor(x_2, x_3); +x_4 = l_or(x_2, x_3); x_5 = lean::box(x_4); return x_5; } } -uint8 l_band___main(uint8 x_0, uint8 x_1) { +uint8 l_and___main(uint8 x_0, uint8 x_1) { _start: { if (x_0 == 0) @@ -2304,18 +2308,18 @@ return x_1; } } } -obj* l_band___main___boxed(obj* x_0, obj* x_1) { +obj* l_and___main___boxed(obj* x_0, obj* x_1) { _start: { uint8 x_2; uint8 x_3; uint8 x_4; obj* x_5; x_2 = lean::unbox(x_0); x_3 = lean::unbox(x_1); -x_4 = l_band___main(x_2, x_3); +x_4 = l_and___main(x_2, x_3); x_5 = lean::box(x_4); return x_5; } } -uint8 l_band(uint8 x_0, uint8 x_1) { +uint8 l_and(uint8 x_0, uint8 x_1) { _start: { if (x_0 == 0) @@ -2328,18 +2332,18 @@ return x_1; } } } -obj* l_band___boxed(obj* x_0, obj* x_1) { +obj* l_and___boxed(obj* x_0, obj* x_1) { _start: { uint8 x_2; uint8 x_3; uint8 x_4; obj* x_5; x_2 = lean::unbox(x_0); x_3 = lean::unbox(x_1); -x_4 = l_band(x_2, x_3); +x_4 = l_and(x_2, x_3); x_5 = lean::box(x_4); return x_5; } } -uint8 l_bnot___main(uint8 x_0) { +uint8 l_not___main(uint8 x_0) { _start: { if (x_0 == 0) @@ -2356,17 +2360,17 @@ return x_2; } } } -obj* l_bnot___main___boxed(obj* x_0) { +obj* l_not___main___boxed(obj* x_0) { _start: { uint8 x_1; uint8 x_2; obj* x_3; x_1 = lean::unbox(x_0); -x_2 = l_bnot___main(x_1); +x_2 = l_not___main(x_1); x_3 = lean::box(x_2); return x_3; } } -uint8 l_bnot(uint8 x_0) { +uint8 l_not(uint8 x_0) { _start: { if (x_0 == 0) @@ -2383,17 +2387,17 @@ return x_2; } } } -obj* l_bnot___boxed(obj* x_0) { +obj* l_not___boxed(obj* x_0) { _start: { uint8 x_1; uint8 x_2; obj* x_3; x_1 = lean::unbox(x_0); -x_2 = l_bnot(x_1); +x_2 = l_not(x_1); x_3 = lean::box(x_2); return x_3; } } -uint8 l_bxor___main(uint8 x_0, uint8 x_1) { +uint8 l_xor___main(uint8 x_0, uint8 x_1) { _start: { if (x_0 == 0) @@ -2415,18 +2419,18 @@ return x_2; } } } -obj* l_bxor___main___boxed(obj* x_0, obj* x_1) { +obj* l_xor___main___boxed(obj* x_0, obj* x_1) { _start: { uint8 x_2; uint8 x_3; uint8 x_4; obj* x_5; x_2 = lean::unbox(x_0); x_3 = lean::unbox(x_1); -x_4 = l_bxor___main(x_2, x_3); +x_4 = l_xor___main(x_2, x_3); x_5 = lean::box(x_4); return x_5; } } -uint8 l_bxor(uint8 x_0, uint8 x_1) { +uint8 l_xor(uint8 x_0, uint8 x_1) { _start: { if (x_0 == 0) @@ -2448,13 +2452,13 @@ return x_2; } } } -obj* l_bxor___boxed(obj* x_0, obj* x_1) { +obj* l_xor___boxed(obj* x_0, obj* x_1) { _start: { uint8 x_2; uint8 x_3; uint8 x_4; obj* x_5; x_2 = lean::unbox(x_0); x_3 = lean::unbox(x_1); -x_4 = l_bxor(x_2, x_3); +x_4 = l_xor(x_2, x_3); x_5 = lean::box(x_4); return x_5; } @@ -2642,6 +2646,52 @@ lean::dec(x_0); return x_1; } } +uint8 l_beqOfEq___rarg(obj* x_0, obj* x_1, obj* x_2) { +_start: +{ +obj* x_3; uint8 x_4; +x_3 = lean::apply_2(x_0, x_1, x_2); +x_4 = lean::unbox(x_3); +if (x_4 == 0) +{ +uint8 x_5; +x_5 = 0; +return x_5; +} +else +{ +uint8 x_6; +x_6 = 1; +return x_6; +} +} +} +obj* l_beqOfEq(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::alloc_closure(reinterpret_cast(l_beqOfEq___rarg___boxed), 3, 0); +return x_1; +} +} +obj* l_beqOfEq___rarg___boxed(obj* x_0, obj* x_1, obj* x_2) { +_start: +{ +uint8 x_3; obj* x_4; +x_3 = l_beqOfEq___rarg(x_0, x_1, x_2); +x_4 = lean::box(x_3); +return x_4; +} +} +obj* l_beqOfEq___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = l_beqOfEq(x_0); +lean::dec(x_0); +return x_1; +} +} uint8 _init_l_True_Decidable() { _start: { @@ -5110,8 +5160,8 @@ static bool _G_initialized = false; obj* initialize_init_core(obj* w) { if (_G_initialized) return w; _G_initialized = true; - l_Unit_star = _init_l_Unit_star(); -lean::mark_persistent(l_Unit_star); + l_Unit_unit = _init_l_Unit_unit(); +lean::mark_persistent(l_Unit_unit); l_Nat_HasZero = _init_l_Nat_HasZero(); lean::mark_persistent(l_Nat_HasZero); l_Nat_HasOne = _init_l_Nat_HasOne(); diff --git a/src/stage0/init/data/list/basic.cpp b/src/stage0/init/data/list/basic.cpp index 2088837224..3e266b3e4b 100644 --- a/src/stage0/init/data/list/basic.cpp +++ b/src/stage0/init/data/list/basic.cpp @@ -41,7 +41,6 @@ namespace lean { obj* nat_sub(obj*, obj*); } obj* l_List_length___rarg(obj*); -obj* l_List_bor___boxed(obj*); obj* l_List_updateNth___boxed(obj*); obj* l_List_map_u_2082___main___boxed(obj*, obj*, obj*); uint8 l_List_removeAll___rarg___lambda__1(obj*, obj*, obj*); @@ -59,6 +58,7 @@ uint8 l_List_hasDecEq___main___rarg(obj*, obj*, obj*); obj* l_List_tail___rarg(obj*); obj* l_List_foldr___main___rarg___boxed(obj*, obj*, obj*); obj* l_List_updateNth___main___rarg(obj*, obj*, obj*); +obj* l_List_or___boxed(obj*); obj* l_List_hasDecidableLe(obj*); obj* l_List_ilast___main___boxed(obj*); obj* l_List_head___main(obj*); @@ -68,12 +68,14 @@ obj* l_List_intersperse___main___rarg(obj*, obj*); obj* l_List_drop___main___boxed(obj*); obj* l_List_intersperse___main(obj*); obj* l_List_lengthAux___main(obj*); +obj* l_List_and___boxed(obj*); obj* l_List_ilast___main___rarg(obj*, obj*); obj* l_List_isSuffixOf___boxed(obj*); obj* l_List_insert(obj*); obj* l_List_lengthAux___main___rarg(obj*, obj*); obj* l_List_head___main___rarg___boxed(obj*, obj*); obj* l_List_removeAll___rarg(obj*, obj*, obj*); +uint8 l_List_foldr___main___at_List_or___spec__1(uint8, obj*); obj* l_List_foldr___main___at_List_union___spec__1___boxed(obj*); obj* l_List_decidableMem___boxed(obj*); obj* l_List_last___main___boxed(obj*); @@ -180,15 +182,12 @@ obj* l_List_foldr1Opt___main(obj*); obj* l_List_enumFrom___main___rarg(obj*, obj*); obj* l_List_take___rarg(obj*, obj*); obj* l_List_HasAppend___boxed(obj*); -uint8 l_List_foldr___main___at_List_band___spec__1(uint8, obj*); uint8 l_List_isSuffixOf___rarg(obj*, obj*, obj*); obj* l_List_foldr1Opt___boxed(obj*); obj* l_List_span___rarg(obj*, obj*); obj* l_List_empty(obj*); -uint8 l_List_foldr___main___at_List_bor___spec__1(uint8, obj*); obj* l_List_erase___main___boxed(obj*); obj* l_List_diff___main(obj*); -uint8 l_List_bor(obj*); obj* l_List_tail___main(obj*); obj* l_List_join___main___rarg(obj*); obj* l_List_last___main(obj*); @@ -203,7 +202,6 @@ obj* l_List_map_u_2082___rarg(obj*, obj*, obj*); obj* l_List_enumFrom___main(obj*); uint8 l_List_empty___main___rarg(obj*); obj* l_List_foldl___rarg(obj*, obj*, obj*); -obj* l_List_band___boxed(obj*); obj* l_List_hasDecidableLt___main(obj*); obj* l_List_updateNth(obj*); obj* l_List_assoc___rarg(obj*, obj*, obj*); @@ -254,7 +252,6 @@ obj* l_List_indexOf___rarg___lambda__1___boxed(obj*, obj*, obj*); obj* l_List_take___rarg___boxed(obj*, obj*); obj* l_List_map___rarg(obj*, obj*); obj* l_List_removeNth___rarg___boxed(obj*, obj*); -obj* l_List_foldr___main___at_List_bor___spec__1___boxed(obj*, obj*); obj* l_List_hasDecidableLt___boxed(obj*); obj* l_List_HasMem___boxed(obj*); obj* l_List_take___main___boxed(obj*); @@ -269,7 +266,6 @@ obj* l_List_isPrefixOf___main___rarg___boxed(obj*, obj*, obj*); obj* l_List_last___rarg___boxed(obj*, obj*); obj* l_List_foldr1___main(obj*); obj* l_Nat_repeatCore___main___at_List_repeat___spec__1(obj*); -obj* l_List_foldr___main___at_List_band___spec__1___boxed(obj*, obj*); obj* l_List_lengthAux___rarg___boxed(obj*, obj*); obj* l_List_HasAppend(obj*); obj* l_List_HasEmptyc___boxed(obj*); @@ -285,6 +281,7 @@ obj* l_List_foldr___main___at_List_all___spec__1___rarg___boxed(obj*, obj*, obj* obj* l_List_enumFrom___boxed(obj*); obj* l_List_partition___main___rarg(obj*, obj*); obj* l_List_bagInter___main(obj*); +uint8 l_List_and(obj*); obj* l_List_HasLt___boxed(obj*, obj*); obj* l_List_head(obj*); obj* l_List_map___main(obj*, obj*); @@ -314,12 +311,15 @@ uint8 l_List_all___rarg(obj*, obj*); obj* l_List_ilast___rarg___boxed(obj*, obj*); obj* l_List_intercalate(obj*); obj* l_List_zip(obj*, obj*); +uint8 l_List_or(obj*); obj* l_List_filter___main___rarg(obj*, obj*); obj* l_List_filter(obj*); obj* l_List_nth___main(obj*); +obj* l_List_foldr___main___at_List_and___spec__1___boxed(obj*, obj*); obj* l_List_union___rarg___boxed(obj*, obj*, obj*); obj* l_List_all___rarg___boxed(obj*, obj*); obj* l_List_assoc(obj*, obj*); +uint8 l_List_foldr___main___at_List_and___spec__1(uint8, obj*); obj* l_List_isSuffixOf(obj*); obj* l_List_HasInter(obj*); obj* l_List_decidableMem___rarg___boxed(obj*, obj*, obj*); @@ -360,7 +360,6 @@ obj* l_List_filter___rarg(obj*, obj*); uint8 l_List_hasDecEq___rarg(obj*, obj*, obj*); obj* l_List_foldr1___rarg___boxed(obj*, obj*, obj*); uint8 l_List_hasDecidableLt___rarg(obj*, obj*, obj*, obj*); -uint8 l_List_band(obj*); obj* l_List_any(obj*); obj* l_List_foldr1___main___boxed(obj*); obj* l_List_bind___boxed(obj*, obj*); @@ -402,6 +401,7 @@ obj* l_List_foldl(obj*, obj*); obj* l_List_hasDecidableLt___main___boxed(obj*); obj* l_List_enum(obj*); obj* l_List_unzip___main(obj*, obj*); +obj* l_List_foldr___main___at_List_or___spec__1___boxed(obj*, obj*); obj* l_List_filterMap___main(obj*, obj*); obj* l_List_partition___boxed(obj*); obj* l_List_hasDecidableLt___main___rarg___boxed(obj*, obj*, obj*, obj*); @@ -3556,7 +3556,7 @@ lean::dec(x_0); return x_1; } } -uint8 l_List_foldr___main___at_List_bor___spec__1(uint8 x_0, obj* x_1) { +uint8 l_List_foldr___main___at_List_or___spec__1(uint8 x_0, obj* x_1) { _start: { if (lean::obj_tag(x_1) == 0) @@ -3582,37 +3582,37 @@ return x_3; } } } -uint8 l_List_bor(obj* x_0) { +uint8 l_List_or(obj* x_0) { _start: { uint8 x_1; uint8 x_2; x_1 = 0; -x_2 = l_List_foldr___main___at_List_bor___spec__1(x_1, x_0); +x_2 = l_List_foldr___main___at_List_or___spec__1(x_1, x_0); return x_2; } } -obj* l_List_foldr___main___at_List_bor___spec__1___boxed(obj* x_0, obj* x_1) { +obj* l_List_foldr___main___at_List_or___spec__1___boxed(obj* x_0, obj* x_1) { _start: { uint8 x_2; uint8 x_3; obj* x_4; x_2 = lean::unbox(x_0); -x_3 = l_List_foldr___main___at_List_bor___spec__1(x_2, x_1); +x_3 = l_List_foldr___main___at_List_or___spec__1(x_2, x_1); x_4 = lean::box(x_3); lean::dec(x_1); return x_4; } } -obj* l_List_bor___boxed(obj* x_0) { +obj* l_List_or___boxed(obj* x_0) { _start: { uint8 x_1; obj* x_2; -x_1 = l_List_bor(x_0); +x_1 = l_List_or(x_0); x_2 = lean::box(x_1); lean::dec(x_0); return x_2; } } -uint8 l_List_foldr___main___at_List_band___spec__1(uint8 x_0, obj* x_1) { +uint8 l_List_foldr___main___at_List_and___spec__1(uint8 x_0, obj* x_1) { _start: { if (lean::obj_tag(x_1) == 0) @@ -3638,31 +3638,31 @@ goto _start; } } } -uint8 l_List_band(obj* x_0) { +uint8 l_List_and(obj* x_0) { _start: { uint8 x_1; uint8 x_2; x_1 = 1; -x_2 = l_List_foldr___main___at_List_band___spec__1(x_1, x_0); +x_2 = l_List_foldr___main___at_List_and___spec__1(x_1, x_0); return x_2; } } -obj* l_List_foldr___main___at_List_band___spec__1___boxed(obj* x_0, obj* x_1) { +obj* l_List_foldr___main___at_List_and___spec__1___boxed(obj* x_0, obj* x_1) { _start: { uint8 x_2; uint8 x_3; obj* x_4; x_2 = lean::unbox(x_0); -x_3 = l_List_foldr___main___at_List_band___spec__1(x_2, x_1); +x_3 = l_List_foldr___main___at_List_and___spec__1(x_2, x_1); x_4 = lean::box(x_3); lean::dec(x_1); return x_4; } } -obj* l_List_band___boxed(obj* x_0) { +obj* l_List_and___boxed(obj* x_0) { _start: { uint8 x_1; obj* x_2; -x_1 = l_List_band(x_0); +x_1 = l_List_and(x_0); x_2 = lean::box(x_1); lean::dec(x_0); return x_2; diff --git a/src/stage0/init/data/rbmap/basic.cpp b/src/stage0/init/data/rbmap/basic.cpp index 7a5ada9bb4..c18b2e2452 100644 --- a/src/stage0/init/data/rbmap/basic.cpp +++ b/src/stage0/init/data/rbmap/basic.cpp @@ -60,7 +60,6 @@ obj* l_RBMap_toList___main___boxed(obj*, obj*, obj*); obj* l_RBMap_min(obj*, obj*, obj*); obj* l_RBMap_toList___rarg(obj*); obj* l_RBMap_depth___rarg___boxed(obj*, obj*); -obj* l_RBMap_empty___main___boxed(obj*, obj*, obj*); obj* l_RBNode_isRed___rarg___boxed(obj*); obj* l_RBNode_ins___main___at_rbmapOf___spec__4___rarg(obj*, obj*, obj*, obj*); uint8 l_RBNode_all___rarg(obj*, obj*); @@ -102,7 +101,6 @@ obj* l_RBMap_depth(obj*, obj*, obj*); obj* l_RBNode_max(obj*, obj*); obj* l_RBNode_mfold___main___at_RBMap_mfor___spec__1(obj*, obj*, obj*, obj*); obj* l_RBNode_findCore___main___at_RBMap_findCore___main___spec__1___boxed(obj*, obj*, obj*); -obj* l_RBMap_empty___boxed(obj*, obj*, obj*); obj* l_RBNode_mfold___main___rarg(obj*, obj*, obj*, obj*); obj* l_RBNode_isRed(obj*, obj*); obj* l_RBMap_toList___main(obj*, obj*, obj*); @@ -124,14 +122,14 @@ obj* l_RBNode_mfold___main___at_RBMap_mfor___spec__1___rarg(obj*, obj*, obj*, ob obj* l_List_reprAux___main___at_RBMap_HasRepr___spec__2___boxed(obj*, obj*); obj* l_RBMap_lowerBound(obj*, obj*, obj*); obj* l_RBNode_lowerBound___main___boxed(obj*, obj*, obj*); -obj* l_RBMap_empty___main(obj*, obj*, obj*); obj* l_List_foldl___main___at_rbmapOf___spec__6(obj*, obj*, obj*); +obj* l_RBMap_isEmpty(obj*, obj*, obj*); obj* l_RBNode_setBlack___boxed(obj*, obj*); obj* l_RBNode_balance2___main___rarg(obj*, obj*); -uint8 l_RBMap_empty___main___rarg(obj*); obj* l_RBNode_ins___main___at_RBNode_insert___spec__2___boxed(obj*, obj*, obj*); obj* l_RBMap_mfor___rarg(obj*, obj*, obj*); obj* l_mkRBMap___boxed(obj*, obj*, obj*); +obj* l_RBMap_isEmpty___main___boxed(obj*, obj*, obj*); obj* l_RBNode_insert___at_RBMap_insert___main___spec__1(obj*, obj*, obj*); obj* l_RBMap_toList___main___rarg(obj*); obj* l_RBMap_ofList___main___rarg(obj*, obj*); @@ -190,6 +188,7 @@ obj* l_RBNode_max___boxed(obj*, obj*); namespace lean { obj* nat_add(obj*, obj*); } +obj* l_RBMap_HasEmptyc___boxed(obj*, obj*, obj*); obj* l_RBNode_isRed___main___boxed(obj*, obj*); obj* l_RBMap_HasRepr___rarg(obj*, obj*, obj*); obj* l_RBNode_setBlack___main___boxed(obj*, obj*); @@ -221,8 +220,8 @@ obj* l_RBMap_any___main___boxed(obj*, obj*, obj*); obj* l_RBNode_any___main___rarg___boxed(obj*, obj*); obj* l_RBMap_max___main(obj*, obj*, obj*); obj* l_RBNode_all___main(obj*, obj*); -obj* l_RBMap_empty(obj*, obj*, obj*); obj* l_RBNode_ins___main___at_rbmapOf___spec__5___rarg(obj*, obj*, obj*, obj*); +uint8 l_RBMap_isEmpty___main___rarg(obj*); obj* l_RBNode_max___rarg(obj*); obj* l_RBMap_all___main___boxed(obj*, obj*, obj*); obj* l_List_repr___main___at_RBMap_HasRepr___spec__1(obj*, obj*); @@ -233,6 +232,7 @@ obj* l_RBNode_all___rarg___boxed(obj*, obj*); obj* l_rbmapOf___boxed(obj*, obj*); obj* l_RBNode_depth___main(obj*, obj*); obj* l_RBNode_mfold___main___boxed(obj*, obj*, obj*, obj*); +obj* l_RBMap_isEmpty___main(obj*, obj*, obj*); obj* l_RBNode_find___main___rarg(obj*, obj*, obj*, obj*); obj* l_RBMap_insert___main(obj*, obj*, obj*); obj* l_RBMap_lowerBound___main___boxed(obj*, obj*, obj*); @@ -244,7 +244,6 @@ obj* l_RBMap_mfold___main___boxed(obj*, obj*, obj*, obj*, obj*); obj* l_RBNode_any___main___boxed(obj*, obj*); obj* l_RBMap_fold(obj*, obj*, obj*, obj*); obj* l_List_reprAux___main___at_RBMap_HasRepr___spec__2___rarg___boxed(obj*, obj*, obj*, obj*); -obj* l_RBMap_empty___rarg___boxed(obj*); obj* l_RBNode_ins___main___at_RBMap_insert___main___spec__3___rarg(obj*, obj*, obj*, obj*); obj* l_RBNode_balance1___main(obj*, obj*); obj* l_RBNode_any___boxed(obj*, obj*); @@ -264,6 +263,7 @@ obj* l_RBMap_insert___main___at_RBMap_fromList___spec__1___boxed(obj*, obj*, obj obj* l_RBNode_revFold___main(obj*, obj*, obj*); obj* l_RBNode_revFold___main___at_RBMap_toList___main___spec__1(obj*, obj*); obj* l_RBMap_lowerBound___main___rarg(obj*, obj*, obj*); +obj* l_RBMap_isEmpty___boxed(obj*, obj*, obj*); uint8 l_RBMap_all___main___rarg(obj*, obj*); obj* l_RBNode_mfold___main___at_RBMap_mfor___spec__1___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_RBNode_balance1___boxed(obj*, obj*); @@ -281,13 +281,14 @@ obj* l_RBNode_max___main(obj*, obj*); obj* l_RBNode_setBlack___rarg(obj*); obj* l_RBMap_lowerBound___rarg(obj*, obj*, obj*); obj* l_RBNode_ins___main___at_RBMap_ofList___main___spec__4___boxed(obj*, obj*, obj*); +obj* l_RBMap_HasEmptyc(obj*, obj*, obj*); obj* l_RBMap_insert___main___at_RBMap_ofList___main___spec__1___boxed(obj*, obj*, obj*); obj* l_RBNode_min___main___boxed(obj*, obj*); obj* l_RBMap_insert___main___at_rbmapOf___spec__2(obj*, obj*, obj*); obj* l_RBNode_depth___boxed(obj*, obj*); -uint8 l_RBMap_empty___rarg(obj*); obj* l_RBMap_find___main___rarg(obj*, obj*, obj*); obj* l_RBNode_balance1___main___rarg(obj*, obj*); +obj* l_RBMap_isEmpty___rarg___boxed(obj*); obj* l_rbmapOf___rarg___boxed(obj*, obj*, obj*); obj* l_RBNode_revFold___main___rarg(obj*, obj*, obj*); obj* l_mkRBMap(obj*, obj*, obj*); @@ -315,6 +316,7 @@ obj* l_RBNode_all___main___boxed(obj*, obj*); obj* l_RBNode_mfold(obj*, obj*, obj*, obj*); obj* l_RBNode_insert___at_rbmapOf___spec__3___rarg(obj*, obj*, obj*, obj*); obj* l_RBNode_ins___main___at_RBMap_fromList___spec__4(obj*, obj*, obj*); +obj* l_RBMap_isEmpty___main___rarg___boxed(obj*); obj* l_RBNode_balance1___rarg(obj*, obj*); obj* l_RBMap_find___main(obj*, obj*, obj*); extern obj* l_List_repr___main___rarg___closed__2; @@ -333,8 +335,8 @@ obj* l_RBNode_insert___at_rbmapOf___spec__3(obj*, obj*, obj*); obj* l_RBNode_ins___main___at_RBMap_insert___main___spec__2(obj*, obj*, obj*); obj* l_RBMap_max___rarg(obj*); obj* l_RBMap_max___main___rarg(obj*); +uint8 l_RBMap_isEmpty___rarg(obj*); extern obj* l_String_Iterator_extract___main___closed__1; -obj* l_RBMap_empty___main___rarg___boxed(obj*); obj* l_List_repr___main___at_RBMap_HasRepr___spec__1___rarg(obj*, obj*, obj*); obj* l_List_foldl___main___at_rbmapOf___spec__6___rarg(obj*, obj*, obj*); obj* l_RBNode_mfold___main___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*, obj*); @@ -3676,6 +3678,25 @@ lean::dec(x_2); return x_3; } } +obj* l_RBMap_HasEmptyc(obj* x_0, obj* x_1, obj* x_2) { +_start: +{ +obj* x_3; +x_3 = lean::box(0); +return x_3; +} +} +obj* l_RBMap_HasEmptyc___boxed(obj* x_0, obj* x_1, obj* x_2) { +_start: +{ +obj* x_3; +x_3 = l_RBMap_HasEmptyc(x_0, x_1, x_2); +lean::dec(x_0); +lean::dec(x_1); +lean::dec(x_2); +return x_3; +} +} obj* l_RBMap_depth___rarg(obj* x_0, obj* x_1) { _start: { @@ -4011,7 +4032,7 @@ lean::dec(x_4); return x_5; } } -uint8 l_RBMap_empty___main___rarg(obj* x_0) { +uint8 l_RBMap_isEmpty___main___rarg(obj* x_0) { _start: { if (lean::obj_tag(x_0) == 0) @@ -4028,36 +4049,36 @@ return x_2; } } } -obj* l_RBMap_empty___main(obj* x_0, obj* x_1, obj* x_2) { +obj* l_RBMap_isEmpty___main(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; -x_3 = lean::alloc_closure(reinterpret_cast(l_RBMap_empty___main___rarg___boxed), 1, 0); +x_3 = lean::alloc_closure(reinterpret_cast(l_RBMap_isEmpty___main___rarg___boxed), 1, 0); return x_3; } } -obj* l_RBMap_empty___main___rarg___boxed(obj* x_0) { +obj* l_RBMap_isEmpty___main___rarg___boxed(obj* x_0) { _start: { uint8 x_1; obj* x_2; -x_1 = l_RBMap_empty___main___rarg(x_0); +x_1 = l_RBMap_isEmpty___main___rarg(x_0); x_2 = lean::box(x_1); lean::dec(x_0); return x_2; } } -obj* l_RBMap_empty___main___boxed(obj* x_0, obj* x_1, obj* x_2) { +obj* l_RBMap_isEmpty___main___boxed(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; -x_3 = l_RBMap_empty___main(x_0, x_1, x_2); +x_3 = l_RBMap_isEmpty___main(x_0, x_1, x_2); lean::dec(x_0); lean::dec(x_1); lean::dec(x_2); return x_3; } } -uint8 l_RBMap_empty___rarg(obj* x_0) { +uint8 l_RBMap_isEmpty___rarg(obj* x_0) { _start: { if (lean::obj_tag(x_0) == 0) @@ -4074,29 +4095,29 @@ return x_2; } } } -obj* l_RBMap_empty(obj* x_0, obj* x_1, obj* x_2) { +obj* l_RBMap_isEmpty(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; -x_3 = lean::alloc_closure(reinterpret_cast(l_RBMap_empty___rarg___boxed), 1, 0); +x_3 = lean::alloc_closure(reinterpret_cast(l_RBMap_isEmpty___rarg___boxed), 1, 0); return x_3; } } -obj* l_RBMap_empty___rarg___boxed(obj* x_0) { +obj* l_RBMap_isEmpty___rarg___boxed(obj* x_0) { _start: { uint8 x_1; obj* x_2; -x_1 = l_RBMap_empty___rarg(x_0); +x_1 = l_RBMap_isEmpty___rarg(x_0); x_2 = lean::box(x_1); lean::dec(x_0); return x_2; } } -obj* l_RBMap_empty___boxed(obj* x_0, obj* x_1, obj* x_2) { +obj* l_RBMap_isEmpty___boxed(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; -x_3 = l_RBMap_empty(x_0, x_1, x_2); +x_3 = l_RBMap_isEmpty(x_0, x_1, x_2); lean::dec(x_0); lean::dec(x_1); lean::dec(x_2); diff --git a/src/stage0/init/data/rbtree/basic.cpp b/src/stage0/init/data/rbtree/basic.cpp index dcaf214750..f900f58e02 100644 --- a/src/stage0/init/data/rbtree/basic.cpp +++ b/src/stage0/init/data/rbtree/basic.cpp @@ -18,6 +18,7 @@ obj* l_RBNode_all___main___at_RBTree_subset___spec__4___boxed(obj*, obj*); obj* l_RBTree_min___boxed(obj*, obj*); obj* l_RBNode_ins___main___at_RBTree_insert___spec__4___rarg(obj*, obj*, obj*, obj*); obj* l_RBNode_setBlack___main___rarg(obj*); +obj* l_RBTree_HasEmptyc___boxed(obj*, obj*); uint8 l_RBNode_all___main___at_RBTree_seteq___spec__10___rarg(obj*, obj*, obj*); obj* l_RBNode_ins___main___at_RBTree_fromList___spec__5___boxed(obj*, obj*); obj* l_RBNode_any___main___at_RBTree_any___spec__1(obj*); @@ -57,6 +58,7 @@ obj* l_RBNode_findCore___main___at_RBTree_seteq___spec__9___boxed(obj*, obj*); obj* l_RBMap_findCore___main___at_RBTree_subset___spec__2(obj*, obj*); obj* l_RBNode_findCore___main___at_RBTree_seteq___spec__9___rarg(obj*, obj*, obj*); obj* l_RBTree_any___rarg___boxed(obj*, obj*); +obj* l_RBTree_isEmpty___rarg___boxed(obj*); obj* l_RBNode_ins___main___at_rbtreeOf___spec__6___rarg(obj*, obj*, obj*, obj*); obj* l_RBNode_ins___main___at_RBTree_fromList___spec__4(obj*, obj*); uint8 l_RBTree_all___rarg(obj*, obj*); @@ -79,7 +81,6 @@ obj* l_RBNode_findCore___main___at_RBTree_seteq___spec__4___boxed(obj*, obj*); obj* l_RBNode_mfold___main___at_RBTree_mfold___spec__1___rarg(obj*, obj*, obj*, obj*); obj* l_RBMap_findCore___main___at_RBTree_seteq___spec__3___rarg(obj*, obj*, obj*); obj* l_RBTree_contains___boxed(obj*, obj*); -obj* l_RBTree_empty(obj*, obj*); obj* l_RBTree_toList___rarg(obj*); obj* l_RBNode_ins___main___at_rbtreeOf___spec__5___boxed(obj*, obj*); obj* l_RBTree_HasRepr___boxed(obj*, obj*); @@ -100,7 +101,6 @@ obj* l_RBTree_find___at_RBTree_contains___spec__1___rarg(obj*, obj*, obj*); uint8 l_RBTree_any___rarg(obj*, obj*); obj* l_RBNode_balance2___main___rarg(obj*, obj*); obj* l_RBMap_insert___main___at_RBTree_ofList___main___spec__1___boxed(obj*, obj*); -obj* l_RBTree_empty___boxed(obj*, obj*); obj* l_RBTree_fromList___rarg___boxed(obj*, obj*, obj*); obj* l_RBMap_findCore___main___at_RBTree_contains___spec__2___rarg(obj*, obj*, obj*); obj* l_RBMap_insert___main___at_RBTree_fromList___spec__2___rarg(obj*, obj*, obj*, obj*); @@ -138,13 +138,14 @@ obj* l_RBMap_findCore___main___at_RBTree_contains___spec__2___boxed(obj*, obj*); obj* l_RBTree_fromList___boxed(obj*); obj* l_RBTree_subset___at_RBTree_seteq___spec__1___boxed(obj*, obj*); obj* l_RBTree_seteq(obj*, obj*); +obj* l_RBTree_HasEmptyc(obj*, obj*); obj* l_RBTree_insert___at_RBTree_fromList___spec__1___boxed(obj*, obj*); obj* l_RBNode_all___main___at_RBTree_seteq___spec__10___rarg___boxed(obj*, obj*, obj*); obj* l_RBTree_revFold___boxed(obj*, obj*, obj*); obj* l_RBTree_find___at_RBTree_seteq___spec__7___boxed(obj*, obj*); -obj* l_RBTree_empty___rarg___boxed(obj*); obj* l_RBNode_all___main___at_RBTree_seteq___spec__10___boxed(obj*, obj*); uint8 l_Option_toBool___main___rarg(obj*); +obj* l_RBTree_isEmpty(obj*, obj*); obj* l_List_foldl___main___at_rbtreeOf___spec__7(obj*, obj*); obj* l_RBTree_mfold___boxed(obj*, obj*, obj*, obj*); obj* l_RBNode_revFold___main___at_RBTree_revFold___spec__1(obj*, obj*); @@ -192,7 +193,6 @@ obj* l_RBTree_insert___at_rbtreeOf___spec__2___rarg(obj*, obj*, obj*); obj* l_RBMap_insert___main___at_RBTree_fromList___spec__2(obj*, obj*); obj* l_RBTree_fold(obj*, obj*, obj*); obj* l_RBNode_mfold___main___at_RBTree_mfor___spec__1___rarg(obj*, obj*, obj*, obj*); -uint8 l_RBTree_empty___rarg(obj*); obj* l_RBNode_ins___main___at_RBTree_insert___spec__3___rarg(obj*, obj*, obj*, obj*); obj* l_RBNode_all___main___at_RBTree_all___spec__1___rarg___boxed(obj*, obj*); obj* l_RBTree_contains(obj*, obj*); @@ -213,6 +213,7 @@ obj* l_RBNode_any___main___at_RBTree_any___spec__1___boxed(obj*); obj* l_RBTree_find___at_RBTree_subset___spec__1___rarg(obj*, obj*, obj*); obj* l_RBTree_ofList___main___rarg(obj*, obj*); obj* l_RBMap_findCore___main___at_RBTree_subset___spec__2___boxed(obj*, obj*); +obj* l_RBTree_isEmpty___boxed(obj*, obj*); uint8 l_RBNode_all___main___at_RBTree_seteq___spec__5___rarg(obj*, obj*, obj*); obj* l_RBTree_max___rarg(obj*); obj* l_RBTree_mfold___rarg(obj*, obj*, obj*, obj*); @@ -220,6 +221,7 @@ obj* l_RBTree_insert(obj*, obj*); obj* l_RBNode_revFold___main___at_RBTree_toList___spec__1___boxed(obj*); uint8 l_RBTree_subset___at_RBTree_seteq___spec__6___rarg(obj*, obj*, obj*); obj* l_RBNode_insert___at_rbtreeOf___spec__4(obj*, obj*); +uint8 l_RBTree_isEmpty___rarg(obj*); obj* l_RBTree_ofList(obj*, obj*); obj* l_RBNode_balance1___main___rarg(obj*, obj*); obj* l_RBTree_ofList___main___boxed(obj*, obj*); @@ -271,6 +273,24 @@ lean::dec(x_1); return x_2; } } +obj* l_RBTree_HasEmptyc(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::box(0); +return x_2; +} +} +obj* l_RBTree_HasEmptyc___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = l_RBTree_HasEmptyc(x_0, x_1); +lean::dec(x_0); +lean::dec(x_1); +return x_2; +} +} obj* l_RBTree_depth___rarg(obj* x_0, obj* x_1) { _start: { @@ -680,7 +700,7 @@ lean::dec(x_3); return x_4; } } -uint8 l_RBTree_empty___rarg(obj* x_0) { +uint8 l_RBTree_isEmpty___rarg(obj* x_0) { _start: { if (lean::obj_tag(x_0) == 0) @@ -697,29 +717,29 @@ return x_2; } } } -obj* l_RBTree_empty(obj* x_0, obj* x_1) { +obj* l_RBTree_isEmpty(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = lean::alloc_closure(reinterpret_cast(l_RBTree_empty___rarg___boxed), 1, 0); +x_2 = lean::alloc_closure(reinterpret_cast(l_RBTree_isEmpty___rarg___boxed), 1, 0); return x_2; } } -obj* l_RBTree_empty___rarg___boxed(obj* x_0) { +obj* l_RBTree_isEmpty___rarg___boxed(obj* x_0) { _start: { uint8 x_1; obj* x_2; -x_1 = l_RBTree_empty___rarg(x_0); +x_1 = l_RBTree_isEmpty___rarg(x_0); x_2 = lean::box(x_1); lean::dec(x_0); return x_2; } } -obj* l_RBTree_empty___boxed(obj* x_0, obj* x_1) { +obj* l_RBTree_isEmpty___boxed(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_RBTree_empty(x_0, x_1); +x_2 = l_RBTree_isEmpty(x_0, x_1); lean::dec(x_0); lean::dec(x_1); return x_2; diff --git a/src/stage0/init/data/string/basic.cpp b/src/stage0/init/data/string/basic.cpp index 74f6f014c4..44d2ac3f0a 100644 --- a/src/stage0/init/data/string/basic.cpp +++ b/src/stage0/init/data/string/basic.cpp @@ -17,7 +17,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; obj* l_String_utf8ByteSize___boxed(obj*); uint32 l_String_Iterator_curr___main(obj*); obj* l_String_Iterator_extract(obj*, obj*); -obj* l_String_utf8AtEnd___boxed(obj*, obj*); +obj* l_String_prev___boxed(obj*, obj*); obj* l_String_mkIterator(obj*); obj* l___private_init_data_string_basic_2__utf8ByteSizeAux___main___boxed(obj*, obj*); obj* l___private_init_data_string_basic_4__utf8SetAux(uint32, obj*, usize, usize); @@ -40,19 +40,14 @@ obj* nat_sub(obj*, obj*); } obj* l_String_toNat(obj*); namespace lean { -uint32 string_utf8_get(obj*, usize); +usize string_utf8_prev(obj*, usize); } -obj* l_String_utf8Set___boxed(obj*, obj*, obj*); obj* l_String_trimRightAux___main___boxed(obj*, obj*, obj*); uint8 l_String_isEmpty(obj*); obj* l_String_trim___boxed(obj*); -namespace lean { -usize string_utf8_prev(obj*, usize); -} obj* l_String_intercalate(obj*, obj*); obj* l_String_lineColumn(obj*, obj*); obj* l_String_Iterator_hasPrev___boxed(obj*); -usize l_String_utf8Begin; obj* l_String_Iterator_extract___main(obj*, obj*); obj* l_String_trimRightAux___boxed(obj*, obj*, obj*); obj* l___private_init_data_string_basic_9__toNatCore___main(obj*, obj*, obj*); @@ -60,7 +55,6 @@ obj* l_String_Iterator_toString___main___boxed(obj*); uint8 l_String_Iterator_hasPrev___main(obj*); obj* l_Char_toString___boxed(obj*); obj* l_String_push___boxed(obj*, obj*); -obj* l_String_utf8Get___boxed(obj*, obj*); obj* l_String_Iterator_remaining___main___boxed(obj*); obj* l___private_init_data_string_basic_4__utf8SetAux___main(uint32, obj*, usize, usize); obj* l___private_init_data_string_basic_7__utf8ExtractAux_u_2081(obj*, usize, usize, usize); @@ -69,6 +63,7 @@ obj* l_String_Iterator_isPrefixOfRemaining___boxed(obj*, obj*); usize l_String_Iterator_remainingBytes___main(obj*); obj* l_String_trimLeftAux___boxed(obj*, obj*, obj*); obj* l_String_pushn___boxed(obj*, obj*, obj*); +obj* l_String_get___boxed(obj*, obj*); obj* l___private_init_data_string_basic_2__utf8ByteSizeAux___boxed(obj*, obj*); uint8 l_String_Iterator_hasNext(obj*); obj* l_String_HasAppend; @@ -104,6 +99,9 @@ namespace lean { uint8 string_dec_lt(obj*, obj*); } obj* l_String_Iterator_setCurr___boxed(obj*, obj*); +namespace lean { +uint8 string_utf8_at_end(obj*, usize); +} obj* l_String_decEq___boxed(obj*, obj*); obj* l_String_Iterator_prev(obj*); obj* l_String_str(obj*, uint32); @@ -113,6 +111,7 @@ obj* l_String_Iterator_nextn(obj*, obj*); obj* l_String_Iterator_curr___main___boxed(obj*); obj* l_String_Iterator_toString___boxed(obj*); obj* l_String_trimLeftAux___main___boxed(obj*, obj*, obj*); +obj* l_String_set___boxed(obj*, obj*, obj*); obj* l_String_Iterator_remainingToString___main___boxed(obj*); namespace lean { obj* nat_add(obj*, obj*); @@ -124,16 +123,16 @@ namespace lean { uint8 nat_dec_eq(obj*, obj*); } obj* l_String_append___boxed(obj*, obj*); -namespace lean { -uint8 string_utf8_at_end(obj*, usize); -} obj* l___private_init_data_string_basic_5__utf8PrevAux___boxed(obj*, obj*, obj*); obj* l_String_Iterator_nextn___main(obj*, obj*); obj* l_String_isEmpty___boxed(obj*); obj* l_Nat_repeatCore___main___at_String_pushn___spec__1(uint32, obj*, obj*, obj*); obj* l_List_map___main___at_String_intercalate___spec__1(obj*); obj* l_String_toList(obj*); -obj* l_String_utf8Begin___boxed; +obj* l_String_atEnd___boxed(obj*, obj*); +namespace lean { +uint32 string_utf8_get(obj*, usize); +} obj* l_String_trimRight___boxed(obj*); obj* l_String_singleton(uint32); namespace lean { @@ -147,7 +146,6 @@ obj* l_String_decLt___boxed(obj*, obj*); obj* l_String_DecidableEq; obj* l_String_trim(obj*); obj* l___private_init_data_string_basic_6__utf8ExtractAux_u_2082___boxed(obj*, obj*, obj*); -obj* l_String_utf8Next___boxed(obj*, obj*); obj* l___private_init_data_string_basic_1__csize___boxed(obj*); namespace lean { obj* string_data(obj*); @@ -156,7 +154,6 @@ obj* l_String_extract___boxed(obj*, obj*, obj*); uint32 l_String_Iterator_curr(obj*); obj* l___private_init_data_string_basic_5__utf8PrevAux___main___closed__1___boxed; obj* l_String_pushn(obj*, uint32, obj*); -obj* l_String_utf8Prev___boxed(obj*, obj*); obj* l___private_init_data_string_basic_3__utf8GetAux___boxed(obj*, obj*, obj*); uint8 l_Char_isWhitespace(uint32); obj* l_String_Iterator_remainingBytes___boxed(obj*); @@ -170,6 +167,9 @@ obj* l___private_init_data_string_basic_6__utf8ExtractAux_u_2082___main___boxed( uint32 l_Char_utf8Size(uint32); obj* l_String_Iterator_toEnd___main(obj*); obj* l_String_Iterator_remaining(obj*); +namespace lean { +usize string_utf8_next(obj*, usize); +} obj* l___private_init_data_string_basic_3__utf8GetAux___main___boxed(obj*, obj*, obj*); obj* l_String_Iterator_extract___boxed(obj*, obj*); obj* l___private_init_data_string_basic_7__utf8ExtractAux_u_2081___main___boxed(obj*, obj*, obj*, obj*); @@ -197,13 +197,7 @@ obj* uint32_to_nat(uint32); } obj* l___private_init_data_string_basic_5__utf8PrevAux___main___boxed(obj*, obj*, obj*); obj* l_String_trimLeft___boxed(obj*); -namespace lean { -usize string_utf8_next(obj*, usize); -} uint8 l_String_Iterator_hasPrev(obj*); -namespace lean { -obj* string_utf8_set(obj*, usize, uint32); -} obj* l_List_foldl___main___at_String_join___spec__1(obj*, obj*); usize l_String_trimLeftAux___main(obj*, obj*, usize); obj* l_String_Iterator_setCurr(obj*, uint32); @@ -220,6 +214,7 @@ uint8 l_String_Iterator_isPrefixOfRemaining___main(obj*, obj*); obj* l_String_Iterator_setCurr___main(obj*, uint32); obj* l___private_init_data_string_basic_7__utf8ExtractAux_u_2081___boxed(obj*, obj*, obj*, obj*); obj* l_String_str___boxed(obj*, obj*); +obj* l_String_next___boxed(obj*, obj*); obj* l_String_trimLeft(obj*); usize l___private_init_data_string_basic_2__utf8ByteSizeAux(obj*, usize); obj* l_String_Iterator_extract___main___closed__1; @@ -230,6 +225,9 @@ uint32 l_String_back(obj*); usize l_String_Iterator_remainingBytes(obj*); obj* l_String_Iterator_remainingToString(obj*); namespace lean { +obj* string_utf8_set(obj*, usize, uint32); +} +namespace lean { obj* string_length(obj*); } obj* l_String_decEq___boxed(obj* x_0, obj* x_1) { @@ -411,24 +409,6 @@ lean::dec(x_0); return x_2; } } -usize _init_l_String_utf8Begin() { -_start: -{ -obj* x_0; usize x_1; -x_0 = lean::mk_nat_obj(0u); -x_1 = lean::usize_of_nat(x_0); -return x_1; -} -} -obj* _init_l_String_utf8Begin___boxed() { -_start: -{ -usize x_0; obj* x_1; -x_0 = l_String_utf8Begin; -x_1 = lean::box_size_t(x_0); -return x_1; -} -} uint32 l___private_init_data_string_basic_3__utf8GetAux___main(obj* x_0, usize x_1, usize x_2) { _start: { @@ -495,7 +475,7 @@ lean::dec(x_0); return x_6; } } -obj* l_String_utf8Get___boxed(obj* x_0, obj* x_1) { +obj* l_String_get___boxed(obj* x_0, obj* x_1) { _start: { usize x_2; uint32 x_3; obj* x_4; @@ -592,7 +572,7 @@ x_7 = l___private_init_data_string_basic_4__utf8SetAux(x_4, x_1, x_5, x_6); return x_7; } } -obj* l_String_utf8Set___boxed(obj* x_0, obj* x_1, obj* x_2) { +obj* l_String_set___boxed(obj* x_0, obj* x_1, obj* x_2) { _start: { usize x_3; uint32 x_4; obj* x_5; @@ -602,7 +582,7 @@ x_5 = lean::string_utf8_set(x_0, x_3, x_4); return x_5; } } -obj* l_String_utf8Next___boxed(obj* x_0, obj* x_1) { +obj* l_String_next___boxed(obj* x_0, obj* x_1) { _start: { usize x_2; usize x_3; obj* x_4; @@ -694,7 +674,7 @@ lean::dec(x_0); return x_6; } } -obj* l_String_utf8Prev___boxed(obj* x_0, obj* x_1) { +obj* l_String_prev___boxed(obj* x_0, obj* x_1) { _start: { usize x_2; usize x_3; obj* x_4; @@ -744,7 +724,7 @@ lean::dec(x_0); return x_2; } } -obj* l_String_utf8AtEnd___boxed(obj* x_0, obj* x_1) { +obj* l_String_atEnd___boxed(obj* x_0, obj* x_1) { _start: { usize x_2; uint8 x_3; obj* x_4; @@ -2329,9 +2309,6 @@ w = initialize_init_data_option_basic(w); lean::mark_persistent(l_String_DecidableEq); l_String_HasLt = _init_l_String_HasLt(); lean::mark_persistent(l_String_HasLt); - l_String_utf8Begin = _init_l_String_utf8Begin(); - l_String_utf8Begin___boxed = _init_l_String_utf8Begin___boxed(); -lean::mark_persistent(l_String_utf8Begin___boxed); l___private_init_data_string_basic_5__utf8PrevAux___main___closed__1 = _init_l___private_init_data_string_basic_5__utf8PrevAux___main___closed__1(); l___private_init_data_string_basic_5__utf8PrevAux___main___closed__1___boxed = _init_l___private_init_data_string_basic_5__utf8PrevAux___main___closed__1___boxed(); lean::mark_persistent(l___private_init_data_string_basic_5__utf8PrevAux___main___closed__1___boxed); diff --git a/src/stage0/init/lean/compiler/ir.cpp b/src/stage0/init/lean/compiler/ir.cpp index 442ba1e6e9..91cf8a7adf 100644 --- a/src/stage0/init/lean/compiler/ir.cpp +++ b/src/stage0/init/lean/compiler/ir.cpp @@ -14,95 +14,96 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #pragma GCC diagnostic ignored "-Wunused-label" #pragma GCC diagnostic ignored "-Wunused-but-set-variable" #endif -obj* l_Lean_IR_alts_isPure___main___boxed(obj*); obj* l_RBMap_insert___main___at_Lean_NameMap_insert___spec__1___rarg(obj*, obj*, obj*); obj* l_Lean_IR_Litval_beq___main___boxed(obj*, obj*); extern "C" uint8 lean_name_dec_eq(obj*, obj*); -obj* l_Lean_IR_varid_hasAeqv; -uint8 l_Lean_IR_alt_isPure(obj*); -uint8 l_Lean_IR_alts_isPure___main(obj*); +uint8 l_Lean_IR_Alt_alphaEqv(obj*, obj*, obj*); uint8 l_Lean_IR_IRType_beq(uint8, uint8); -obj* l_Lean_IR_alt_alphaEqv___boxed(obj*, obj*, obj*); uint8 l_Lean_IR_Arg_alphaEqv(obj*, obj*, obj*); -obj* l_Lean_IR_varid_alphaEqv___boxed(obj*, obj*, obj*); -obj* l___private_init_lean_compiler_ir_9__alts_collect(obj*, obj*, obj*); uint8 l_Lean_IR_IRType_beq___main(uint8, uint8); +obj* l_RBMap_find___main___at_Lean_IR_VarId_alphaEqv___spec__1___boxed(obj*, obj*); obj* l_Lean_IR_addParamRename(obj*, obj*, obj*); obj* l_Lean_IR_CtorInfo_HasBeq; +obj* l___private_init_lean_compiler_ir_8__collectExpr___main(obj*, obj*, obj*); +uint8 l_Lean_IR_Alt_isPure___main(obj*); obj* l___private_init_lean_compiler_ir_3__withBv(obj*, obj*, obj*, obj*); obj* l___private_init_lean_compiler_ir_5__Seq(obj*, obj*, obj*, obj*); -uint8 l_Lean_IR_alt_isPure___main(obj*); -obj* l_Lean_IR_alt_ctor(obj*, obj*); -obj* l___private_init_lean_compiler_ir_8__Expr_collect(obj*, obj*, obj*); +uint8 l_Lean_IR_VarId_alphaEqv(obj*, obj*, obj*); obj* l_Lean_IR_insertParams(obj*, obj*); uint8 l_Lean_IR_Fnbody_beq(obj*, obj*); -uint8 l_Lean_Kvmap_eqv(obj*, obj*); -obj* l_Lean_IR_alts_isPure___boxed(obj*); +uint8 l_Lean_IR_Alts_isPure___main(obj*); +obj* l___private_init_lean_compiler_ir_8__collectExpr(obj*, obj*, obj*); uint8 l_Lean_IR_CtorInfo_beq(obj*, obj*); obj* l_Lean_IR_Fnbody_HasBeq; +obj* l___private_init_lean_compiler_ir_9__collectFnBody___main(obj*, obj*, obj*); +obj* l_Lean_IR_Alt_default(obj*); obj* l_Lean_IR_Fnbody_alphaEqv___boxed(obj*, obj*, obj*); obj* l_Lean_IR_Fnbody_isPure___main___boxed(obj*); -uint8 l_Lean_IR_alt_alphaEqv(obj*, obj*, obj*); +obj* l_Lean_IR_Alts_isPure___boxed(obj*); uint8 l_Lean_IR_Fnbody_isPure___main(obj*); +obj* l_Lean_IR_VarId_hasAeqv; uint8 l_Lean_NameSet_contains(obj*, obj*); uint8 l_Lean_IR_Expr_isPure___main(obj*); obj* l___private_init_lean_compiler_ir_1__skip___boxed(obj*); -obj* l___private_init_lean_compiler_ir_2__var_collect(obj*, obj*, obj*); obj* l_Lean_IR_Arg_alphaEqv___boxed(obj*, obj*, obj*); +obj* l___private_init_lean_compiler_ir_2__collectVar(obj*, obj*, obj*); obj* l___private_init_lean_compiler_ir_1__skip(obj*); +obj* l___private_init_lean_compiler_ir_6__collectArg___main(obj*, obj*, obj*); +obj* l___private_init_lean_compiler_ir_6__collectArg(obj*, obj*, obj*); obj* l_Lean_IR_freeVars(obj*); -uint8 l_Lean_IR_varid_alphaEqv(obj*, obj*, obj*); -obj* l___private_init_lean_compiler_ir_9__Fnbody_collect___main(obj*, obj*, obj*); uint8 l_Lean_IR_Litval_beq(obj*, obj*); obj* l_RBNode_find___main___at_Lean_NameMap_contains___spec__2(obj*, obj*, obj*, obj*); -uint8 l_Lean_IR_alts_isPure(obj*); -obj* l_Lean_IR_alts_alphaEqv___main___boxed(obj*, obj*, obj*); -obj* l___private_init_lean_compiler_ir_9__alt_collect(obj*, obj*, obj*); +uint8 l_Lean_IR_Alt_isPure(obj*); +obj* l_Lean_IR_Alt_alphaEqv___boxed(obj*, obj*, obj*); obj* l_Lean_IR_addParamsRename(obj*, obj*, obj*); obj* l_Lean_IR_Expr_alphaEqv___boxed(obj*, obj*, obj*); -obj* l_Lean_IR_alt_default(obj*); +obj* l_Lean_IR_Alt_isPure___boxed(obj*); obj* l_Lean_IR_args_hasAeqv; -obj* l___private_init_lean_compiler_ir_9__alts_collect___main(obj*, obj*, obj*); -obj* l___private_init_lean_compiler_ir_6__Arg_collect___main(obj*, obj*, obj*); +obj* l_Lean_IR_Alts_alphaEqv___main___boxed(obj*, obj*, obj*); obj* l_Lean_IR_args_alphaEqv___boxed(obj*, obj*, obj*); uint8 l_Lean_IR_Expr_alphaEqv(obj*, obj*, obj*); +obj* l_Lean_IR_Alt_alphaEqv___main___boxed(obj*, obj*, obj*); uint8 l_Lean_IR_Fnbody_alphaEqv(obj*, obj*, obj*); -uint8 l_Lean_IR_alt_alphaEqv___main(obj*, obj*, obj*); -obj* l_Lean_IR_alt_alphaEqv___main___boxed(obj*, obj*, obj*); -obj* l_RBMap_find___main___at_Lean_IR_varid_alphaEqv___spec__1___boxed(obj*, obj*); namespace lean { uint8 nat_dec_eq(obj*, obj*); } +uint8 l_Lean_IR_Alts_alphaEqv___main(obj*, obj*, obj*); obj* l_Lean_IR_Litval_HasBeq; -obj* l___private_init_lean_compiler_ir_7__args_collect___main(obj*, obj*, obj*); uint8 l_Lean_IR_Litval_beq___main(obj*, obj*); +uint8 l_Lean_KVMap_eqv(obj*, obj*); obj* l_Lean_IR_Expr_hasAeqv; -uint8 l_Lean_IR_alts_alphaEqv(obj*, obj*, obj*); obj* l_Lean_IR_args_alphaEqv___main___boxed(obj*, obj*, obj*); obj* l_Lean_IR_IRType_HasBeq; +uint8 l_Lean_IR_Alts_alphaEqv(obj*, obj*, obj*); obj* l_Lean_IR_Expr_isPure___boxed(obj*); namespace lean { uint8 string_dec_eq(obj*, obj*); } +obj* l_Lean_IR_Alts_isPure___main___boxed(obj*); obj* l_Lean_IR_Litval_beq___boxed(obj*, obj*); +obj* l_Lean_IR_Alt_isPure___main___boxed(obj*); obj* l_Lean_IR_Arg_alphaEqv___main___boxed(obj*, obj*, obj*); uint8 l_Lean_IR_args_alphaEqv___main(obj*, obj*, obj*); +obj* l___private_init_lean_compiler_ir_7__collectArgs___main(obj*, obj*, obj*); obj* l_Lean_IR_Expr_isPure___main___boxed(obj*); +obj* l_RBMap_find___main___at_Lean_IR_VarId_alphaEqv___spec__1(obj*, obj*); obj* l_Lean_IR_addVarRename(obj*, obj*, obj*); obj* l_Lean_IR_Fnbody_isPure___boxed(obj*); -obj* l_Lean_IR_alt_isPure___main___boxed(obj*); uint8 l_Lean_IR_Arg_alphaEqv___main(obj*, obj*, obj*); +obj* l_Lean_IR_VarId_alphaEqv___boxed(obj*, obj*, obj*); uint8 l_Lean_IR_Fnbody_alphaEqv___main(obj*, obj*, obj*); uint8 l_Lean_IR_CtorInfo_beq___main(obj*, obj*); uint8 l_Lean_IR_args_alphaEqv(obj*, obj*, obj*); +obj* l___private_init_lean_compiler_ir_7__collectArgs(obj*, obj*, obj*); obj* l_Lean_IR_CtorInfo_beq___main___boxed(obj*, obj*); uint8 l_Lean_IR_Expr_alphaEqv___main(obj*, obj*, obj*); uint8 l_Lean_IR_Expr_isPure(obj*); -obj* l___private_init_lean_compiler_ir_9__alt_collect___main(obj*, obj*, obj*); obj* l_List_foldl___main___at_Lean_IR_insertParams___spec__1(obj*, obj*); obj* l_Lean_IR_Arg_hasAeqv; -obj* l_RBMap_find___main___at_Lean_IR_varid_alphaEqv___spec__1(obj*, obj*); -obj* l___private_init_lean_compiler_ir_9__Fnbody_collect(obj*, obj*, obj*); +obj* l_Lean_IR_Alt_ctor(obj*, obj*); +obj* l___private_init_lean_compiler_ir_9__collectAlt___main(obj*, obj*, obj*); +obj* l_Lean_IR_MData_HasEmptyc; +obj* l___private_init_lean_compiler_ir_9__collectFnBody(obj*, obj*, obj*); obj* l_Lean_IR_IRType_beq___boxed(obj*, obj*); obj* l_Lean_IR_Expr_alphaEqv___main___boxed(obj*, obj*, obj*); obj* l_RBMap_insert___main___at_Lean_NameSet_insert___spec__1(obj*, obj*, obj*); @@ -110,17 +111,34 @@ obj* l_Lean_IR_addParamsRename___main(obj*, obj*, obj*); obj* l___private_init_lean_compiler_ir_1__skip___rarg___boxed(obj*); obj* l_Lean_IR_Fnbody_beq___boxed(obj*, obj*); uint8 l_Lean_IR_Fnbody_isPure(obj*); -uint8 l_Lean_IR_alts_alphaEqv___main(obj*, obj*, obj*); +uint8 l_Lean_IR_Alts_isPure(obj*); obj* l___private_init_lean_compiler_ir_4__withParams(obj*, obj*, obj*, obj*); -obj* l_Lean_IR_alts_alphaEqv___boxed(obj*, obj*, obj*); -obj* l_Lean_IR_alt_isPure___boxed(obj*); -obj* l___private_init_lean_compiler_ir_8__Expr_collect___main(obj*, obj*, obj*); obj* l_Lean_IR_CtorInfo_beq___boxed(obj*, obj*); -obj* l___private_init_lean_compiler_ir_7__args_collect(obj*, obj*, obj*); -obj* l___private_init_lean_compiler_ir_6__Arg_collect(obj*, obj*, obj*); +obj* l___private_init_lean_compiler_ir_9__collectAlt(obj*, obj*, obj*); +uint8 l_Lean_IR_Alt_alphaEqv___main(obj*, obj*, obj*); +obj* l_Lean_IR_MData_empty; +obj* l___private_init_lean_compiler_ir_9__collectAlts___main(obj*, obj*, obj*); +obj* l___private_init_lean_compiler_ir_9__collectAlts(obj*, obj*, obj*); obj* l_Lean_IR_IRType_beq___main___boxed(obj*, obj*); +obj* l_Lean_IR_Alts_alphaEqv___boxed(obj*, obj*, obj*); obj* l___private_init_lean_compiler_ir_1__skip___rarg(obj*); obj* l_Lean_IR_Fnbody_alphaEqv___main___boxed(obj*, obj*, obj*); +obj* _init_l_Lean_IR_MData_empty() { +_start: +{ +obj* x_0; +x_0 = lean::box(0); +return x_0; +} +} +obj* _init_l_Lean_IR_MData_HasEmptyc() { +_start: +{ +obj* x_0; +x_0 = lean::box(0); +return x_0; +} +} uint8 l_Lean_IR_IRType_beq___main(uint8 x_0, uint8 x_1) { _start: { @@ -516,7 +534,7 @@ x_0 = lean::alloc_closure(reinterpret_cast(l_Lean_IR_CtorInfo_beq___boxed return x_0; } } -obj* l_Lean_IR_alt_ctor(obj* x_0, obj* x_1) { +obj* l_Lean_IR_Alt_ctor(obj* x_0, obj* x_1) { _start: { obj* x_2; @@ -526,7 +544,7 @@ lean::cnstr_set(x_2, 1, x_1); return x_2; } } -obj* l_Lean_IR_alt_default(obj* x_0) { +obj* l_Lean_IR_Alt_default(obj* x_0) { _start: { obj* x_1; @@ -673,7 +691,7 @@ case 9: { obj* x_15; uint8 x_16; x_15 = lean::cnstr_get(x_0, 2); -x_16 = l_Lean_IR_alts_isPure___main(x_15); +x_16 = l_Lean_IR_Alts_isPure___main(x_15); return x_16; } case 10: @@ -703,7 +721,7 @@ return x_20; } } } -uint8 l_Lean_IR_alts_isPure___main(obj* x_0) { +uint8 l_Lean_IR_Alts_isPure___main(obj* x_0) { _start: { if (lean::obj_tag(x_0) == 0) @@ -717,7 +735,7 @@ else obj* x_2; obj* x_3; uint8 x_4; x_2 = lean::cnstr_get(x_0, 0); x_3 = lean::cnstr_get(x_0, 1); -x_4 = l_Lean_IR_alt_isPure___main(x_2); +x_4 = l_Lean_IR_Alt_isPure___main(x_2); if (x_4 == 0) { return x_4; @@ -730,7 +748,7 @@ goto _start; } } } -uint8 l_Lean_IR_alt_isPure___main(obj* x_0) { +uint8 l_Lean_IR_Alt_isPure___main(obj* x_0) { _start: { if (lean::obj_tag(x_0) == 0) @@ -758,21 +776,21 @@ lean::dec(x_0); return x_2; } } -obj* l_Lean_IR_alts_isPure___main___boxed(obj* x_0) { +obj* l_Lean_IR_Alts_isPure___main___boxed(obj* x_0) { _start: { uint8 x_1; obj* x_2; -x_1 = l_Lean_IR_alts_isPure___main(x_0); +x_1 = l_Lean_IR_Alts_isPure___main(x_0); x_2 = lean::box(x_1); lean::dec(x_0); return x_2; } } -obj* l_Lean_IR_alt_isPure___main___boxed(obj* x_0) { +obj* l_Lean_IR_Alt_isPure___main___boxed(obj* x_0) { _start: { uint8 x_1; obj* x_2; -x_1 = l_Lean_IR_alt_isPure___main(x_0); +x_1 = l_Lean_IR_Alt_isPure___main(x_0); x_2 = lean::box(x_1); lean::dec(x_0); return x_2; @@ -796,43 +814,43 @@ lean::dec(x_0); return x_2; } } -uint8 l_Lean_IR_alts_isPure(obj* x_0) { +uint8 l_Lean_IR_Alts_isPure(obj* x_0) { _start: { uint8 x_1; -x_1 = l_Lean_IR_alts_isPure___main(x_0); +x_1 = l_Lean_IR_Alts_isPure___main(x_0); return x_1; } } -obj* l_Lean_IR_alts_isPure___boxed(obj* x_0) { +obj* l_Lean_IR_Alts_isPure___boxed(obj* x_0) { _start: { uint8 x_1; obj* x_2; -x_1 = l_Lean_IR_alts_isPure(x_0); +x_1 = l_Lean_IR_Alts_isPure(x_0); x_2 = lean::box(x_1); lean::dec(x_0); return x_2; } } -uint8 l_Lean_IR_alt_isPure(obj* x_0) { +uint8 l_Lean_IR_Alt_isPure(obj* x_0) { _start: { uint8 x_1; -x_1 = l_Lean_IR_alt_isPure___main(x_0); +x_1 = l_Lean_IR_Alt_isPure___main(x_0); return x_1; } } -obj* l_Lean_IR_alt_isPure___boxed(obj* x_0) { +obj* l_Lean_IR_Alt_isPure___boxed(obj* x_0) { _start: { uint8 x_1; obj* x_2; -x_1 = l_Lean_IR_alt_isPure(x_0); +x_1 = l_Lean_IR_Alt_isPure(x_0); x_2 = lean::box(x_1); lean::dec(x_0); return x_2; } } -obj* l_RBMap_find___main___at_Lean_IR_varid_alphaEqv___spec__1(obj* x_0, obj* x_1) { +obj* l_RBMap_find___main___at_Lean_IR_VarId_alphaEqv___spec__1(obj* x_0, obj* x_1) { _start: { obj* x_2; obj* x_3; @@ -841,11 +859,11 @@ x_3 = l_RBNode_find___main___at_Lean_NameMap_contains___spec__2(x_2, lean::box(0 return x_3; } } -uint8 l_Lean_IR_varid_alphaEqv(obj* x_0, obj* x_1, obj* x_2) { +uint8 l_Lean_IR_VarId_alphaEqv(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; -x_3 = l_RBMap_find___main___at_Lean_IR_varid_alphaEqv___spec__1(x_0, x_1); +x_3 = l_RBMap_find___main___at_Lean_IR_VarId_alphaEqv___spec__1(x_0, x_1); if (lean::obj_tag(x_3) == 0) { uint8 x_4; @@ -886,31 +904,31 @@ return x_13; } } } -obj* l_RBMap_find___main___at_Lean_IR_varid_alphaEqv___spec__1___boxed(obj* x_0, obj* x_1) { +obj* l_RBMap_find___main___at_Lean_IR_VarId_alphaEqv___spec__1___boxed(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_RBMap_find___main___at_Lean_IR_varid_alphaEqv___spec__1(x_0, x_1); +x_2 = l_RBMap_find___main___at_Lean_IR_VarId_alphaEqv___spec__1(x_0, x_1); lean::dec(x_1); return x_2; } } -obj* l_Lean_IR_varid_alphaEqv___boxed(obj* x_0, obj* x_1, obj* x_2) { +obj* l_Lean_IR_VarId_alphaEqv___boxed(obj* x_0, obj* x_1, obj* x_2) { _start: { uint8 x_3; obj* x_4; -x_3 = l_Lean_IR_varid_alphaEqv(x_0, x_1, x_2); +x_3 = l_Lean_IR_VarId_alphaEqv(x_0, x_1, x_2); x_4 = lean::box(x_3); lean::dec(x_1); lean::dec(x_2); return x_4; } } -obj* _init_l_Lean_IR_varid_hasAeqv() { +obj* _init_l_Lean_IR_VarId_hasAeqv() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(l_Lean_IR_varid_alphaEqv___boxed), 3, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_Lean_IR_VarId_alphaEqv___boxed), 3, 0); return x_0; } } @@ -924,7 +942,7 @@ if (lean::obj_tag(x_2) == 0) obj* x_3; obj* x_4; uint8 x_5; x_3 = lean::cnstr_get(x_1, 0); x_4 = lean::cnstr_get(x_2, 0); -x_5 = l_Lean_IR_varid_alphaEqv(x_0, x_3, x_4); +x_5 = l_Lean_IR_VarId_alphaEqv(x_0, x_3, x_4); return x_5; } else @@ -1125,7 +1143,7 @@ case 1: obj* x_12; obj* x_13; uint8 x_14; x_12 = lean::cnstr_get(x_1, 0); x_13 = lean::cnstr_get(x_2, 0); -x_14 = l_Lean_IR_varid_alphaEqv(x_0, x_12, x_13); +x_14 = l_Lean_IR_VarId_alphaEqv(x_0, x_12, x_13); return x_14; } default: @@ -1150,7 +1168,7 @@ x_20 = lean::cnstr_get(x_2, 0); x_21 = lean::cnstr_get(x_2, 1); x_22 = lean::cnstr_get(x_2, 2); lean::inc(x_0); -x_24 = l_Lean_IR_varid_alphaEqv(x_0, x_17, x_20); +x_24 = l_Lean_IR_VarId_alphaEqv(x_0, x_17, x_20); if (x_24 == 0) { if (x_24 == 0) @@ -1212,7 +1230,7 @@ return x_38; else { uint8 x_39; -x_39 = l_Lean_IR_varid_alphaEqv(x_0, x_33, x_35); +x_39 = l_Lean_IR_VarId_alphaEqv(x_0, x_33, x_35); return x_39; } } @@ -1246,7 +1264,7 @@ return x_48; else { uint8 x_49; -x_49 = l_Lean_IR_varid_alphaEqv(x_0, x_43, x_45); +x_49 = l_Lean_IR_VarId_alphaEqv(x_0, x_43, x_45); return x_49; } } @@ -1280,7 +1298,7 @@ return x_58; else { uint8 x_59; -x_59 = l_Lean_IR_varid_alphaEqv(x_0, x_53, x_55); +x_59 = l_Lean_IR_VarId_alphaEqv(x_0, x_53, x_55); return x_59; } } @@ -1371,7 +1389,7 @@ x_82 = lean::cnstr_get(x_1, 1); x_83 = lean::cnstr_get(x_2, 0); x_84 = lean::cnstr_get(x_2, 1); lean::inc(x_0); -x_86 = l_Lean_IR_varid_alphaEqv(x_0, x_81, x_83); +x_86 = l_Lean_IR_VarId_alphaEqv(x_0, x_81, x_83); if (x_86 == 0) { lean::dec(x_0); @@ -1413,7 +1431,7 @@ return x_95; else { uint8 x_97; -x_97 = l_Lean_IR_varid_alphaEqv(x_0, x_92, x_94); +x_97 = l_Lean_IR_VarId_alphaEqv(x_0, x_92, x_94); return x_97; } } @@ -1434,7 +1452,7 @@ case 10: obj* x_100; obj* x_101; uint8 x_102; x_100 = lean::cnstr_get(x_1, 0); x_101 = lean::cnstr_get(x_2, 0); -x_102 = l_Lean_IR_varid_alphaEqv(x_0, x_100, x_101); +x_102 = l_Lean_IR_VarId_alphaEqv(x_0, x_100, x_101); return x_102; } default: @@ -1474,7 +1492,7 @@ case 12: obj* x_110; obj* x_111; uint8 x_112; x_110 = lean::cnstr_get(x_1, 0); x_111 = lean::cnstr_get(x_2, 0); -x_112 = l_Lean_IR_varid_alphaEqv(x_0, x_110, x_111); +x_112 = l_Lean_IR_VarId_alphaEqv(x_0, x_110, x_111); return x_112; } default: @@ -1494,7 +1512,7 @@ case 13: obj* x_115; obj* x_116; uint8 x_117; x_115 = lean::cnstr_get(x_1, 0); x_116 = lean::cnstr_get(x_2, 0); -x_117 = l_Lean_IR_varid_alphaEqv(x_0, x_115, x_116); +x_117 = l_Lean_IR_VarId_alphaEqv(x_0, x_115, x_116); return x_117; } default: @@ -1998,7 +2016,7 @@ x_121 = lean::cnstr_get(x_2, 3); lean::inc(x_121); lean::dec(x_2); lean::inc(x_0); -x_125 = l_Lean_IR_varid_alphaEqv(x_0, x_106, x_115); +x_125 = l_Lean_IR_VarId_alphaEqv(x_0, x_106, x_115); lean::dec(x_115); lean::dec(x_106); if (x_125 == 0) @@ -2027,7 +2045,7 @@ else { uint8 x_137; lean::inc(x_0); -x_137 = l_Lean_IR_varid_alphaEqv(x_0, x_110, x_119); +x_137 = l_Lean_IR_VarId_alphaEqv(x_0, x_110, x_119); lean::dec(x_119); lean::dec(x_110); if (x_137 == 0) @@ -2064,37 +2082,17 @@ return x_152; } else { -if (x_125 == 0) -{ -lean::dec(x_119); -lean::dec(x_110); -if (x_125 == 0) -{ -lean::dec(x_121); -lean::dec(x_112); -lean::dec(x_0); -return x_125; -} -else -{ -x_1 = x_112; -x_2 = x_121; -goto _start; -} -} -else -{ -uint8 x_160; +uint8 x_154; lean::inc(x_0); -x_160 = l_Lean_IR_varid_alphaEqv(x_0, x_110, x_119); +x_154 = l_Lean_IR_VarId_alphaEqv(x_0, x_110, x_119); lean::dec(x_119); lean::dec(x_110); -if (x_160 == 0) +if (x_154 == 0) { lean::dec(x_121); lean::dec(x_112); lean::dec(x_0); -return x_160; +return x_154; } else { @@ -2105,23 +2103,22 @@ goto _start; } } } -} case 12: { -uint8 x_169; +uint8 x_163; lean::dec(x_1); lean::dec(x_0); -x_169 = 0; -return x_169; +x_163 = 0; +return x_163; } default: { -uint8 x_173; +uint8 x_167; lean::dec(x_1); lean::dec(x_0); lean::dec(x_2); -x_173 = 0; -return x_173; +x_167 = 0; +return x_167; } } } @@ -2130,416 +2127,395 @@ case 3: switch (lean::obj_tag(x_2)) { case 3: { -obj* x_174; obj* x_176; obj* x_178; obj* x_180; obj* x_183; obj* x_185; obj* x_187; obj* x_189; uint8 x_193; -x_174 = lean::cnstr_get(x_1, 0); +obj* x_168; obj* x_170; obj* x_172; obj* x_174; obj* x_177; obj* x_179; obj* x_181; obj* x_183; uint8 x_187; +x_168 = lean::cnstr_get(x_1, 0); +lean::inc(x_168); +x_170 = lean::cnstr_get(x_1, 1); +lean::inc(x_170); +x_172 = lean::cnstr_get(x_1, 2); +lean::inc(x_172); +x_174 = lean::cnstr_get(x_1, 3); lean::inc(x_174); -x_176 = lean::cnstr_get(x_1, 1); -lean::inc(x_176); -x_178 = lean::cnstr_get(x_1, 2); -lean::inc(x_178); -x_180 = lean::cnstr_get(x_1, 3); -lean::inc(x_180); lean::dec(x_1); -x_183 = lean::cnstr_get(x_2, 0); +x_177 = lean::cnstr_get(x_2, 0); +lean::inc(x_177); +x_179 = lean::cnstr_get(x_2, 1); +lean::inc(x_179); +x_181 = lean::cnstr_get(x_2, 2); +lean::inc(x_181); +x_183 = lean::cnstr_get(x_2, 3); lean::inc(x_183); -x_185 = lean::cnstr_get(x_2, 1); -lean::inc(x_185); -x_187 = lean::cnstr_get(x_2, 2); -lean::inc(x_187); -x_189 = lean::cnstr_get(x_2, 3); -lean::inc(x_189); lean::dec(x_2); lean::inc(x_0); -x_193 = l_Lean_IR_varid_alphaEqv(x_0, x_174, x_183); -lean::dec(x_183); +x_187 = l_Lean_IR_VarId_alphaEqv(x_0, x_168, x_177); +lean::dec(x_177); +lean::dec(x_168); +if (x_187 == 0) +{ +lean::dec(x_179); +lean::dec(x_170); +if (x_187 == 0) +{ +lean::dec(x_181); +lean::dec(x_172); +if (x_187 == 0) +{ lean::dec(x_174); -if (x_193 == 0) -{ -lean::dec(x_185); -lean::dec(x_176); -if (x_193 == 0) -{ -lean::dec(x_178); -lean::dec(x_187); -if (x_193 == 0) -{ -lean::dec(x_180); lean::dec(x_0); -lean::dec(x_189); -return x_193; +lean::dec(x_183); +return x_187; } else { -x_1 = x_180; -x_2 = x_189; +x_1 = x_174; +x_2 = x_183; goto _start; } } else { -uint8 x_205; +uint8 x_199; lean::inc(x_0); -x_205 = l_Lean_IR_varid_alphaEqv(x_0, x_178, x_187); -lean::dec(x_187); -lean::dec(x_178); -if (x_205 == 0) +x_199 = l_Lean_IR_VarId_alphaEqv(x_0, x_172, x_181); +lean::dec(x_181); +lean::dec(x_172); +if (x_199 == 0) { -lean::dec(x_180); +lean::dec(x_174); lean::dec(x_0); -lean::dec(x_189); -return x_205; +lean::dec(x_183); +return x_199; } else { -x_1 = x_180; -x_2 = x_189; +x_1 = x_174; +x_2 = x_183; goto _start; } } } else { -uint8 x_212; -x_212 = lean::nat_dec_eq(x_176, x_185); -lean::dec(x_185); -lean::dec(x_176); -if (x_212 == 0) +uint8 x_206; +x_206 = lean::nat_dec_eq(x_170, x_179); +lean::dec(x_179); +lean::dec(x_170); +if (x_206 == 0) { -uint8 x_220; -lean::dec(x_180); -lean::dec(x_178); +uint8 x_214; +lean::dec(x_174); lean::dec(x_0); -lean::dec(x_189); -lean::dec(x_187); -x_220 = 0; -return x_220; +lean::dec(x_183); +lean::dec(x_181); +lean::dec(x_172); +x_214 = 0; +return x_214; } else { -if (x_193 == 0) -{ -lean::dec(x_178); -lean::dec(x_187); -if (x_193 == 0) -{ -lean::dec(x_180); -lean::dec(x_0); -lean::dec(x_189); -return x_193; -} -else -{ -x_1 = x_180; -x_2 = x_189; -goto _start; -} -} -else -{ -uint8 x_228; +uint8 x_216; lean::inc(x_0); -x_228 = l_Lean_IR_varid_alphaEqv(x_0, x_178, x_187); -lean::dec(x_187); -lean::dec(x_178); -if (x_228 == 0) +x_216 = l_Lean_IR_VarId_alphaEqv(x_0, x_172, x_181); +lean::dec(x_181); +lean::dec(x_172); +if (x_216 == 0) { -lean::dec(x_180); +lean::dec(x_174); lean::dec(x_0); -lean::dec(x_189); -return x_228; +lean::dec(x_183); +return x_216; } else { -x_1 = x_180; -x_2 = x_189; +x_1 = x_174; +x_2 = x_183; goto _start; } } } } -} case 12: { -uint8 x_237; +uint8 x_225; lean::dec(x_1); lean::dec(x_0); -x_237 = 0; -return x_237; +x_225 = 0; +return x_225; } default: { -uint8 x_241; +uint8 x_229; lean::dec(x_1); lean::dec(x_0); lean::dec(x_2); -x_241 = 0; -return x_241; +x_229 = 0; +return x_229; } } } case 4: { -uint8 x_242; -x_242 = lean::cnstr_get_scalar(x_1, sizeof(void*)*5); +uint8 x_230; +x_230 = lean::cnstr_get_scalar(x_1, sizeof(void*)*5); switch (lean::obj_tag(x_2)) { case 4: { -obj* x_243; obj* x_245; obj* x_247; obj* x_249; obj* x_251; obj* x_254; obj* x_256; obj* x_258; obj* x_260; uint8 x_262; obj* x_263; uint8 x_266; uint8 x_268; uint8 x_271; -x_243 = lean::cnstr_get(x_1, 0); -lean::inc(x_243); -x_245 = lean::cnstr_get(x_1, 1); -lean::inc(x_245); -x_247 = lean::cnstr_get(x_1, 2); -lean::inc(x_247); -x_249 = lean::cnstr_get(x_1, 3); -lean::inc(x_249); -x_251 = lean::cnstr_get(x_1, 4); -lean::inc(x_251); +obj* x_231; obj* x_233; obj* x_235; obj* x_237; obj* x_239; obj* x_242; obj* x_244; obj* x_246; obj* x_248; uint8 x_250; obj* x_251; uint8 x_254; uint8 x_256; uint8 x_259; +x_231 = lean::cnstr_get(x_1, 0); +lean::inc(x_231); +x_233 = lean::cnstr_get(x_1, 1); +lean::inc(x_233); +x_235 = lean::cnstr_get(x_1, 2); +lean::inc(x_235); +x_237 = lean::cnstr_get(x_1, 3); +lean::inc(x_237); +x_239 = lean::cnstr_get(x_1, 4); +lean::inc(x_239); lean::dec(x_1); -x_254 = lean::cnstr_get(x_2, 0); -lean::inc(x_254); -x_256 = lean::cnstr_get(x_2, 1); -lean::inc(x_256); -x_258 = lean::cnstr_get(x_2, 2); -lean::inc(x_258); -x_260 = lean::cnstr_get(x_2, 3); -lean::inc(x_260); -x_262 = lean::cnstr_get_scalar(x_2, sizeof(void*)*5); -x_263 = lean::cnstr_get(x_2, 4); -lean::inc(x_263); +x_242 = lean::cnstr_get(x_2, 0); +lean::inc(x_242); +x_244 = lean::cnstr_get(x_2, 1); +lean::inc(x_244); +x_246 = lean::cnstr_get(x_2, 2); +lean::inc(x_246); +x_248 = lean::cnstr_get(x_2, 3); +lean::inc(x_248); +x_250 = lean::cnstr_get_scalar(x_2, sizeof(void*)*5); +x_251 = lean::cnstr_get(x_2, 4); +lean::inc(x_251); lean::dec(x_2); lean::inc(x_0); -x_271 = l_Lean_IR_varid_alphaEqv(x_0, x_243, x_254); -lean::dec(x_254); -lean::dec(x_243); -if (x_271 == 0) +x_259 = l_Lean_IR_VarId_alphaEqv(x_0, x_231, x_242); +lean::dec(x_242); +lean::dec(x_231); +if (x_259 == 0) { -lean::dec(x_245); -lean::dec(x_256); -if (x_271 == 0) +lean::dec(x_244); +lean::dec(x_233); +if (x_259 == 0) { -lean::dec(x_247); -lean::dec(x_258); -x_266 = x_271; -goto lbl_267; +lean::dec(x_246); +lean::dec(x_235); +x_254 = x_259; +goto lbl_255; } else { -x_268 = x_271; -goto lbl_269; +x_256 = x_259; +goto lbl_257; } } else { -uint8 x_278; -x_278 = lean::nat_dec_eq(x_245, x_256); -lean::dec(x_256); -lean::dec(x_245); -if (x_278 == 0) -{ -uint8 x_283; -lean::dec(x_247); -lean::dec(x_258); -x_283 = 0; -x_266 = x_283; -goto lbl_267; -} -else -{ -if (x_271 == 0) -{ -lean::dec(x_247); -lean::dec(x_258); -x_266 = x_271; -goto lbl_267; -} -else -{ -x_268 = x_271; -goto lbl_269; -} -} -} -lbl_267: -{ +uint8 x_266; +x_266 = lean::nat_dec_eq(x_233, x_244); +lean::dec(x_244); +lean::dec(x_233); if (x_266 == 0) { -lean::dec(x_260); -lean::dec(x_249); -if (x_266 == 0) +uint8 x_271; +lean::dec(x_246); +lean::dec(x_235); +x_271 = 0; +x_254 = x_271; +goto lbl_255; +} +else { -if (x_266 == 0) +if (x_259 == 0) { +lean::dec(x_246); +lean::dec(x_235); +x_254 = x_259; +goto lbl_255; +} +else +{ +x_256 = x_259; +goto lbl_257; +} +} +} +lbl_255: +{ +if (x_254 == 0) +{ +lean::dec(x_237); +lean::dec(x_248); +if (x_254 == 0) +{ +if (x_254 == 0) +{ +lean::dec(x_239); lean::dec(x_251); -lean::dec(x_263); lean::dec(x_0); -return x_266; +return x_254; } else { -x_1 = x_251; -x_2 = x_263; +x_1 = x_239; +x_2 = x_251; goto _start; } } else { -uint8 x_292; -x_292 = l_Lean_IR_IRType_beq___main(x_242, x_262); -if (x_292 == 0) +uint8 x_280; +x_280 = l_Lean_IR_IRType_beq___main(x_230, x_250); +if (x_280 == 0) { +lean::dec(x_239); lean::dec(x_251); -lean::dec(x_263); lean::dec(x_0); -return x_292; +return x_280; } else { -x_1 = x_251; -x_2 = x_263; +x_1 = x_239; +x_2 = x_251; goto _start; } } } else { +uint8 x_286; +lean::inc(x_0); +x_286 = l_Lean_IR_VarId_alphaEqv(x_0, x_237, x_248); +lean::dec(x_248); +lean::dec(x_237); +if (x_286 == 0) +{ +if (x_286 == 0) +{ +lean::dec(x_239); +lean::dec(x_251); +lean::dec(x_0); +return x_286; +} +else +{ +x_1 = x_239; +x_2 = x_251; +goto _start; +} +} +else +{ +uint8 x_293; +x_293 = l_Lean_IR_IRType_beq___main(x_230, x_250); +if (x_293 == 0) +{ +lean::dec(x_239); +lean::dec(x_251); +lean::dec(x_0); +return x_293; +} +else +{ +x_1 = x_239; +x_2 = x_251; +goto _start; +} +} +} +} +lbl_257: +{ uint8 x_298; -lean::inc(x_0); -x_298 = l_Lean_IR_varid_alphaEqv(x_0, x_249, x_260); -lean::dec(x_260); -lean::dec(x_249); -if (x_298 == 0) -{ +x_298 = lean::nat_dec_eq(x_235, x_246); +lean::dec(x_246); +lean::dec(x_235); if (x_298 == 0) { +uint8 x_306; +lean::dec(x_239); +lean::dec(x_237); +lean::dec(x_248); lean::dec(x_251); -lean::dec(x_263); lean::dec(x_0); -return x_298; +x_306 = 0; +return x_306; } else { -x_1 = x_251; -x_2 = x_263; +if (x_256 == 0) +{ +lean::dec(x_237); +lean::dec(x_248); +if (x_256 == 0) +{ +if (x_256 == 0) +{ +lean::dec(x_239); +lean::dec(x_251); +lean::dec(x_0); +return x_256; +} +else +{ +x_1 = x_239; +x_2 = x_251; goto _start; } } else { -uint8 x_305; -x_305 = l_Lean_IR_IRType_beq___main(x_242, x_262); -if (x_305 == 0) +uint8 x_313; +x_313 = l_Lean_IR_IRType_beq___main(x_230, x_250); +if (x_313 == 0) { +lean::dec(x_239); lean::dec(x_251); -lean::dec(x_263); lean::dec(x_0); -return x_305; +return x_313; } else { -x_1 = x_251; -x_2 = x_263; -goto _start; -} -} -} -} -lbl_269: -{ -uint8 x_310; -x_310 = lean::nat_dec_eq(x_247, x_258); -lean::dec(x_258); -lean::dec(x_247); -if (x_310 == 0) -{ -uint8 x_318; -lean::dec(x_251); -lean::dec(x_263); -lean::dec(x_260); -lean::dec(x_249); -lean::dec(x_0); -x_318 = 0; -return x_318; -} -else -{ -if (x_268 == 0) -{ -lean::dec(x_260); -lean::dec(x_249); -if (x_268 == 0) -{ -if (x_268 == 0) -{ -lean::dec(x_251); -lean::dec(x_263); -lean::dec(x_0); -return x_268; -} -else -{ -x_1 = x_251; -x_2 = x_263; -goto _start; -} -} -else -{ -uint8 x_325; -x_325 = l_Lean_IR_IRType_beq___main(x_242, x_262); -if (x_325 == 0) -{ -lean::dec(x_251); -lean::dec(x_263); -lean::dec(x_0); -return x_325; -} -else -{ -x_1 = x_251; -x_2 = x_263; +x_1 = x_239; +x_2 = x_251; goto _start; } } } else { -uint8 x_331; +uint8 x_319; lean::inc(x_0); -x_331 = l_Lean_IR_varid_alphaEqv(x_0, x_249, x_260); -lean::dec(x_260); -lean::dec(x_249); -if (x_331 == 0) +x_319 = l_Lean_IR_VarId_alphaEqv(x_0, x_237, x_248); +lean::dec(x_248); +lean::dec(x_237); +if (x_319 == 0) { -if (x_331 == 0) +if (x_319 == 0) { +lean::dec(x_239); lean::dec(x_251); -lean::dec(x_263); lean::dec(x_0); -return x_331; +return x_319; } else { -x_1 = x_251; -x_2 = x_263; +x_1 = x_239; +x_2 = x_251; goto _start; } } else { -uint8 x_338; -x_338 = l_Lean_IR_IRType_beq___main(x_242, x_262); -if (x_338 == 0) +uint8 x_326; +x_326 = l_Lean_IR_IRType_beq___main(x_230, x_250); +if (x_326 == 0) { +lean::dec(x_239); lean::dec(x_251); -lean::dec(x_263); lean::dec(x_0); -return x_338; +return x_326; } else { -x_1 = x_251; -x_2 = x_263; +x_1 = x_239; +x_2 = x_251; goto _start; } } @@ -2549,20 +2525,20 @@ goto _start; } case 12: { -uint8 x_345; +uint8 x_333; lean::dec(x_1); lean::dec(x_0); -x_345 = 0; -return x_345; +x_333 = 0; +return x_333; } default: { -uint8 x_349; +uint8 x_337; lean::dec(x_1); lean::dec(x_0); lean::dec(x_2); -x_349 = 0; -return x_349; +x_337 = 0; +return x_337; } } } @@ -2571,242 +2547,222 @@ case 5: switch (lean::obj_tag(x_2)) { case 5: { -obj* x_350; obj* x_352; obj* x_354; obj* x_357; obj* x_359; obj* x_361; uint8 x_365; -x_350 = lean::cnstr_get(x_1, 0); -lean::inc(x_350); -x_352 = lean::cnstr_get(x_1, 1); -lean::inc(x_352); -x_354 = lean::cnstr_get(x_1, 2); -lean::inc(x_354); +obj* x_338; obj* x_340; obj* x_342; obj* x_345; obj* x_347; obj* x_349; uint8 x_353; +x_338 = lean::cnstr_get(x_1, 0); +lean::inc(x_338); +x_340 = lean::cnstr_get(x_1, 1); +lean::inc(x_340); +x_342 = lean::cnstr_get(x_1, 2); +lean::inc(x_342); lean::dec(x_1); -x_357 = lean::cnstr_get(x_2, 0); -lean::inc(x_357); -x_359 = lean::cnstr_get(x_2, 1); -lean::inc(x_359); -x_361 = lean::cnstr_get(x_2, 2); -lean::inc(x_361); +x_345 = lean::cnstr_get(x_2, 0); +lean::inc(x_345); +x_347 = lean::cnstr_get(x_2, 1); +lean::inc(x_347); +x_349 = lean::cnstr_get(x_2, 2); +lean::inc(x_349); lean::dec(x_2); lean::inc(x_0); -x_365 = l_Lean_IR_varid_alphaEqv(x_0, x_350, x_357); -lean::dec(x_357); -lean::dec(x_350); -if (x_365 == 0) +x_353 = l_Lean_IR_VarId_alphaEqv(x_0, x_338, x_345); +lean::dec(x_345); +lean::dec(x_338); +if (x_353 == 0) { -lean::dec(x_359); -lean::dec(x_352); -if (x_365 == 0) +lean::dec(x_340); +lean::dec(x_347); +if (x_353 == 0) { lean::dec(x_0); -lean::dec(x_361); -lean::dec(x_354); -return x_365; +lean::dec(x_342); +lean::dec(x_349); +return x_353; } else { -x_1 = x_354; -x_2 = x_361; +x_1 = x_342; +x_2 = x_349; goto _start; } } else { -uint8 x_374; -x_374 = lean::nat_dec_eq(x_352, x_359); -lean::dec(x_359); -lean::dec(x_352); -if (x_374 == 0) +uint8 x_362; +x_362 = lean::nat_dec_eq(x_340, x_347); +lean::dec(x_347); +lean::dec(x_340); +if (x_362 == 0) { -uint8 x_380; +uint8 x_368; lean::dec(x_0); -lean::dec(x_361); -lean::dec(x_354); -x_380 = 0; -return x_380; +lean::dec(x_342); +lean::dec(x_349); +x_368 = 0; +return x_368; } else { -if (x_365 == 0) -{ -lean::dec(x_0); -lean::dec(x_361); -lean::dec(x_354); -return x_365; -} -else -{ -x_1 = x_354; -x_2 = x_361; +x_1 = x_342; +x_2 = x_349; goto _start; } } } -} case 12: { -uint8 x_387; +uint8 x_372; lean::dec(x_1); lean::dec(x_0); -x_387 = 0; -return x_387; +x_372 = 0; +return x_372; } default: { -uint8 x_391; +uint8 x_376; lean::dec(x_1); lean::dec(x_0); lean::dec(x_2); -x_391 = 0; -return x_391; +x_376 = 0; +return x_376; } } } case 6: { -uint8 x_392; -x_392 = lean::cnstr_get_scalar(x_1, sizeof(void*)*3); +uint8 x_377; +x_377 = lean::cnstr_get_scalar(x_1, sizeof(void*)*3); switch (lean::obj_tag(x_2)) { case 6: { -obj* x_393; obj* x_395; obj* x_397; obj* x_400; obj* x_402; uint8 x_404; obj* x_405; uint8 x_408; uint8 x_411; -x_393 = lean::cnstr_get(x_1, 0); -lean::inc(x_393); -x_395 = lean::cnstr_get(x_1, 1); -lean::inc(x_395); -x_397 = lean::cnstr_get(x_1, 2); -lean::inc(x_397); +obj* x_378; obj* x_380; obj* x_382; obj* x_385; obj* x_387; uint8 x_389; obj* x_390; uint8 x_394; +x_378 = lean::cnstr_get(x_1, 0); +lean::inc(x_378); +x_380 = lean::cnstr_get(x_1, 1); +lean::inc(x_380); +x_382 = lean::cnstr_get(x_1, 2); +lean::inc(x_382); lean::dec(x_1); -x_400 = lean::cnstr_get(x_2, 0); -lean::inc(x_400); -x_402 = lean::cnstr_get(x_2, 1); -lean::inc(x_402); -x_404 = lean::cnstr_get_scalar(x_2, sizeof(void*)*3); -x_405 = lean::cnstr_get(x_2, 2); -lean::inc(x_405); +x_385 = lean::cnstr_get(x_2, 0); +lean::inc(x_385); +x_387 = lean::cnstr_get(x_2, 1); +lean::inc(x_387); +x_389 = lean::cnstr_get_scalar(x_2, sizeof(void*)*3); +x_390 = lean::cnstr_get(x_2, 2); +lean::inc(x_390); lean::dec(x_2); lean::inc(x_0); -x_411 = l_Lean_IR_varid_alphaEqv(x_0, x_393, x_400); -lean::dec(x_400); -lean::dec(x_393); -if (x_411 == 0) +x_394 = l_Lean_IR_VarId_alphaEqv(x_0, x_378, x_385); +lean::dec(x_385); +lean::dec(x_378); +if (x_394 == 0) { -lean::dec(x_395); -lean::dec(x_402); -if (x_411 == 0) +lean::dec(x_380); +lean::dec(x_387); +if (x_394 == 0) { -if (x_411 == 0) +if (x_394 == 0) { -lean::dec(x_405); lean::dec(x_0); -lean::dec(x_397); +lean::dec(x_382); +lean::dec(x_390); +return x_394; +} +else +{ +x_1 = x_382; +x_2 = x_390; +goto _start; +} +} +else +{ +if (x_377 == 0) +{ +if (x_389 == 0) +{ +x_1 = x_382; +x_2 = x_390; +goto _start; +} +else +{ +uint8 x_407; +lean::dec(x_0); +lean::dec(x_382); +lean::dec(x_390); +x_407 = 0; +return x_407; +} +} +else +{ +if (x_389 == 0) +{ +uint8 x_411; +lean::dec(x_0); +lean::dec(x_382); +lean::dec(x_390); +x_411 = 0; return x_411; } else { -x_1 = x_397; -x_2 = x_405; +x_1 = x_382; +x_2 = x_390; goto _start; } } -else -{ -x_408 = x_411; -goto lbl_409; } } else { -uint8 x_420; -x_420 = lean::nat_dec_eq(x_395, x_402); -lean::dec(x_402); -lean::dec(x_395); -if (x_420 == 0) +uint8 x_413; +x_413 = lean::nat_dec_eq(x_380, x_387); +lean::dec(x_387); +lean::dec(x_380); +if (x_413 == 0) { -uint8 x_426; -lean::dec(x_405); +uint8 x_419; lean::dec(x_0); -lean::dec(x_397); -x_426 = 0; -return x_426; +lean::dec(x_382); +lean::dec(x_390); +x_419 = 0; +return x_419; } else { -if (x_411 == 0) +if (x_377 == 0) { -if (x_411 == 0) +if (x_389 == 0) { -lean::dec(x_405); -lean::dec(x_0); -lean::dec(x_397); -return x_411; -} -else -{ -x_1 = x_397; -x_2 = x_405; +x_1 = x_382; +x_2 = x_390; goto _start; } -} else { -x_408 = x_411; -goto lbl_409; -} -} -} -lbl_409: -{ -if (x_392 == 0) -{ -if (x_404 == 0) -{ -if (x_408 == 0) -{ -lean::dec(x_405); +uint8 x_424; lean::dec(x_0); -lean::dec(x_397); -return x_408; -} -else -{ -x_1 = x_397; -x_2 = x_405; -goto _start; +lean::dec(x_382); +lean::dec(x_390); +x_424 = 0; +return x_424; } } else { -uint8 x_438; -lean::dec(x_405); +if (x_389 == 0) +{ +uint8 x_428; lean::dec(x_0); -lean::dec(x_397); -x_438 = 0; -return x_438; -} +lean::dec(x_382); +lean::dec(x_390); +x_428 = 0; +return x_428; } else { -if (x_404 == 0) -{ -uint8 x_442; -lean::dec(x_405); -lean::dec(x_0); -lean::dec(x_397); -x_442 = 0; -return x_442; -} -else -{ -if (x_408 == 0) -{ -lean::dec(x_405); -lean::dec(x_0); -lean::dec(x_397); -return x_408; -} -else -{ -x_1 = x_397; -x_2 = x_405; +x_1 = x_382; +x_2 = x_390; goto _start; } } @@ -2815,170 +2771,160 @@ goto _start; } case 12: { -uint8 x_449; +uint8 x_432; lean::dec(x_1); lean::dec(x_0); -x_449 = 0; -return x_449; +x_432 = 0; +return x_432; } default: { -uint8 x_453; +uint8 x_436; lean::dec(x_1); lean::dec(x_0); lean::dec(x_2); -x_453 = 0; -return x_453; +x_436 = 0; +return x_436; } } } case 7: { -uint8 x_454; -x_454 = lean::cnstr_get_scalar(x_1, sizeof(void*)*3); +uint8 x_437; +x_437 = lean::cnstr_get_scalar(x_1, sizeof(void*)*3); switch (lean::obj_tag(x_2)) { case 7: { -obj* x_455; obj* x_457; obj* x_459; obj* x_462; obj* x_464; uint8 x_466; obj* x_467; uint8 x_470; uint8 x_473; -x_455 = lean::cnstr_get(x_1, 0); -lean::inc(x_455); -x_457 = lean::cnstr_get(x_1, 1); -lean::inc(x_457); -x_459 = lean::cnstr_get(x_1, 2); -lean::inc(x_459); +obj* x_438; obj* x_440; obj* x_442; obj* x_445; obj* x_447; uint8 x_449; obj* x_450; uint8 x_454; +x_438 = lean::cnstr_get(x_1, 0); +lean::inc(x_438); +x_440 = lean::cnstr_get(x_1, 1); +lean::inc(x_440); +x_442 = lean::cnstr_get(x_1, 2); +lean::inc(x_442); lean::dec(x_1); -x_462 = lean::cnstr_get(x_2, 0); -lean::inc(x_462); -x_464 = lean::cnstr_get(x_2, 1); -lean::inc(x_464); -x_466 = lean::cnstr_get_scalar(x_2, sizeof(void*)*3); -x_467 = lean::cnstr_get(x_2, 2); -lean::inc(x_467); +x_445 = lean::cnstr_get(x_2, 0); +lean::inc(x_445); +x_447 = lean::cnstr_get(x_2, 1); +lean::inc(x_447); +x_449 = lean::cnstr_get_scalar(x_2, sizeof(void*)*3); +x_450 = lean::cnstr_get(x_2, 2); +lean::inc(x_450); lean::dec(x_2); lean::inc(x_0); -x_473 = l_Lean_IR_varid_alphaEqv(x_0, x_455, x_462); -lean::dec(x_462); -lean::dec(x_455); -if (x_473 == 0) +x_454 = l_Lean_IR_VarId_alphaEqv(x_0, x_438, x_445); +lean::dec(x_445); +lean::dec(x_438); +if (x_454 == 0) { -lean::dec(x_464); -lean::dec(x_457); -if (x_473 == 0) +lean::dec(x_447); +lean::dec(x_440); +if (x_454 == 0) { -if (x_473 == 0) +if (x_454 == 0) { -lean::dec(x_467); lean::dec(x_0); -lean::dec(x_459); -return x_473; +lean::dec(x_442); +lean::dec(x_450); +return x_454; } else { -x_1 = x_459; -x_2 = x_467; +x_1 = x_442; +x_2 = x_450; goto _start; } } else { -x_470 = x_473; -goto lbl_471; +if (x_437 == 0) +{ +if (x_449 == 0) +{ +x_1 = x_442; +x_2 = x_450; +goto _start; +} +else +{ +uint8 x_467; +lean::dec(x_0); +lean::dec(x_442); +lean::dec(x_450); +x_467 = 0; +return x_467; } } else { -uint8 x_482; -x_482 = lean::nat_dec_eq(x_457, x_464); -lean::dec(x_464); -lean::dec(x_457); -if (x_482 == 0) +if (x_449 == 0) +{ +uint8 x_471; +lean::dec(x_0); +lean::dec(x_442); +lean::dec(x_450); +x_471 = 0; +return x_471; +} +else +{ +x_1 = x_442; +x_2 = x_450; +goto _start; +} +} +} +} +else +{ +uint8 x_473; +x_473 = lean::nat_dec_eq(x_440, x_447); +lean::dec(x_447); +lean::dec(x_440); +if (x_473 == 0) +{ +uint8 x_479; +lean::dec(x_0); +lean::dec(x_442); +lean::dec(x_450); +x_479 = 0; +return x_479; +} +else +{ +if (x_437 == 0) +{ +if (x_449 == 0) +{ +x_1 = x_442; +x_2 = x_450; +goto _start; +} +else +{ +uint8 x_484; +lean::dec(x_0); +lean::dec(x_442); +lean::dec(x_450); +x_484 = 0; +return x_484; +} +} +else +{ +if (x_449 == 0) { uint8 x_488; -lean::dec(x_467); lean::dec(x_0); -lean::dec(x_459); +lean::dec(x_442); +lean::dec(x_450); x_488 = 0; return x_488; } else { -if (x_473 == 0) -{ -if (x_473 == 0) -{ -lean::dec(x_467); -lean::dec(x_0); -lean::dec(x_459); -return x_473; -} -else -{ -x_1 = x_459; -x_2 = x_467; -goto _start; -} -} -else -{ -x_470 = x_473; -goto lbl_471; -} -} -} -lbl_471: -{ -if (x_454 == 0) -{ -if (x_466 == 0) -{ -if (x_470 == 0) -{ -lean::dec(x_467); -lean::dec(x_0); -lean::dec(x_459); -return x_470; -} -else -{ -x_1 = x_459; -x_2 = x_467; -goto _start; -} -} -else -{ -uint8 x_500; -lean::dec(x_467); -lean::dec(x_0); -lean::dec(x_459); -x_500 = 0; -return x_500; -} -} -else -{ -if (x_466 == 0) -{ -uint8 x_504; -lean::dec(x_467); -lean::dec(x_0); -lean::dec(x_459); -x_504 = 0; -return x_504; -} -else -{ -if (x_470 == 0) -{ -lean::dec(x_467); -lean::dec(x_0); -lean::dec(x_459); -return x_470; -} -else -{ -x_1 = x_459; -x_2 = x_467; +x_1 = x_442; +x_2 = x_450; goto _start; } } @@ -2987,20 +2933,20 @@ goto _start; } case 12: { -uint8 x_511; +uint8 x_492; lean::dec(x_1); lean::dec(x_0); -x_511 = 0; -return x_511; +x_492 = 0; +return x_492; } default: { -uint8 x_515; +uint8 x_496; lean::dec(x_1); lean::dec(x_0); lean::dec(x_2); -x_515 = 0; -return x_515; +x_496 = 0; +return x_496; } } } @@ -3009,159 +2955,159 @@ case 8: switch (lean::obj_tag(x_2)) { case 8: { -obj* x_516; obj* x_518; obj* x_521; obj* x_523; uint8 x_526; -x_516 = lean::cnstr_get(x_1, 0); -lean::inc(x_516); -x_518 = lean::cnstr_get(x_1, 1); -lean::inc(x_518); +obj* x_497; obj* x_499; obj* x_502; obj* x_504; uint8 x_507; +x_497 = lean::cnstr_get(x_1, 0); +lean::inc(x_497); +x_499 = lean::cnstr_get(x_1, 1); +lean::inc(x_499); lean::dec(x_1); -x_521 = lean::cnstr_get(x_2, 0); +x_502 = lean::cnstr_get(x_2, 0); +lean::inc(x_502); +x_504 = lean::cnstr_get(x_2, 1); +lean::inc(x_504); +lean::dec(x_2); +x_507 = l_Lean_KVMap_eqv(x_497, x_502); +if (x_507 == 0) +{ +lean::dec(x_0); +lean::dec(x_499); +lean::dec(x_504); +return x_507; +} +else +{ +x_1 = x_499; +x_2 = x_504; +goto _start; +} +} +case 12: +{ +uint8 x_514; +lean::dec(x_1); +lean::dec(x_0); +x_514 = 0; +return x_514; +} +default: +{ +uint8 x_518; +lean::dec(x_1); +lean::dec(x_0); +lean::dec(x_2); +x_518 = 0; +return x_518; +} +} +} +case 9: +{ +switch (lean::obj_tag(x_2)) { +case 9: +{ +obj* x_519; obj* x_521; obj* x_523; obj* x_526; obj* x_528; obj* x_530; uint8 x_533; +x_519 = lean::cnstr_get(x_1, 0); +lean::inc(x_519); +x_521 = lean::cnstr_get(x_1, 1); lean::inc(x_521); -x_523 = lean::cnstr_get(x_2, 1); +x_523 = lean::cnstr_get(x_1, 2); lean::inc(x_523); +lean::dec(x_1); +x_526 = lean::cnstr_get(x_2, 0); +lean::inc(x_526); +x_528 = lean::cnstr_get(x_2, 1); +lean::inc(x_528); +x_530 = lean::cnstr_get(x_2, 2); +lean::inc(x_530); lean::dec(x_2); -x_526 = l_Lean_Kvmap_eqv(x_516, x_521); -if (x_526 == 0) +x_533 = lean_name_dec_eq(x_519, x_526); +lean::dec(x_526); +lean::dec(x_519); +if (x_533 == 0) { +uint8 x_541; lean::dec(x_0); -lean::dec(x_518); +lean::dec(x_530); +lean::dec(x_528); +lean::dec(x_521); lean::dec(x_523); -return x_526; +x_541 = 0; +return x_541; } else { -x_1 = x_518; -x_2 = x_523; -goto _start; +uint8 x_543; +lean::inc(x_0); +x_543 = l_Lean_IR_VarId_alphaEqv(x_0, x_521, x_528); +lean::dec(x_528); +lean::dec(x_521); +if (x_543 == 0) +{ +lean::dec(x_0); +lean::dec(x_530); +lean::dec(x_523); +return x_543; +} +else +{ +uint8 x_549; +x_549 = l_Lean_IR_Alts_alphaEqv___main(x_0, x_523, x_530); +return x_549; +} } } case 12: { -uint8 x_533; +uint8 x_552; lean::dec(x_1); lean::dec(x_0); -x_533 = 0; -return x_533; +x_552 = 0; +return x_552; } default: { -uint8 x_537; +uint8 x_556; lean::dec(x_1); lean::dec(x_0); lean::dec(x_2); -x_537 = 0; -return x_537; +x_556 = 0; +return x_556; } } } -case 9: +case 10: { switch (lean::obj_tag(x_2)) { -case 9: +case 10: { -obj* x_538; obj* x_540; obj* x_542; obj* x_545; obj* x_547; obj* x_549; uint8 x_552; -x_538 = lean::cnstr_get(x_1, 0); -lean::inc(x_538); -x_540 = lean::cnstr_get(x_1, 1); -lean::inc(x_540); -x_542 = lean::cnstr_get(x_1, 2); -lean::inc(x_542); +obj* x_557; obj* x_560; uint8 x_563; +x_557 = lean::cnstr_get(x_1, 0); +lean::inc(x_557); lean::dec(x_1); -x_545 = lean::cnstr_get(x_2, 0); -lean::inc(x_545); -x_547 = lean::cnstr_get(x_2, 1); -lean::inc(x_547); -x_549 = lean::cnstr_get(x_2, 2); -lean::inc(x_549); +x_560 = lean::cnstr_get(x_2, 0); +lean::inc(x_560); lean::dec(x_2); -x_552 = lean_name_dec_eq(x_538, x_545); -lean::dec(x_545); -lean::dec(x_538); -if (x_552 == 0) -{ -uint8 x_560; -lean::dec(x_0); -lean::dec(x_549); -lean::dec(x_547); -lean::dec(x_540); -lean::dec(x_542); -x_560 = 0; -return x_560; +x_563 = l_Lean_IR_VarId_alphaEqv(x_0, x_557, x_560); +lean::dec(x_560); +lean::dec(x_557); +return x_563; } -else -{ -uint8 x_562; -lean::inc(x_0); -x_562 = l_Lean_IR_varid_alphaEqv(x_0, x_540, x_547); -lean::dec(x_547); -lean::dec(x_540); -if (x_562 == 0) -{ -lean::dec(x_0); -lean::dec(x_549); -lean::dec(x_542); -return x_562; -} -else +case 12: { uint8 x_568; -x_568 = l_Lean_IR_alts_alphaEqv___main(x_0, x_542, x_549); +lean::dec(x_1); +lean::dec(x_0); +x_568 = 0; return x_568; } -} -} -case 12: -{ -uint8 x_571; -lean::dec(x_1); -lean::dec(x_0); -x_571 = 0; -return x_571; -} default: { -uint8 x_575; +uint8 x_572; lean::dec(x_1); lean::dec(x_0); lean::dec(x_2); -x_575 = 0; -return x_575; -} -} -} -case 10: -{ -switch (lean::obj_tag(x_2)) { -case 10: -{ -obj* x_576; obj* x_579; uint8 x_582; -x_576 = lean::cnstr_get(x_1, 0); -lean::inc(x_576); -lean::dec(x_1); -x_579 = lean::cnstr_get(x_2, 0); -lean::inc(x_579); -lean::dec(x_2); -x_582 = l_Lean_IR_varid_alphaEqv(x_0, x_576, x_579); -lean::dec(x_579); -lean::dec(x_576); -return x_582; -} -case 12: -{ -uint8 x_587; -lean::dec(x_1); -lean::dec(x_0); -x_587 = 0; -return x_587; -} -default: -{ -uint8 x_591; -lean::dec(x_1); -lean::dec(x_0); -lean::dec(x_2); -x_591 = 0; -return x_591; +x_572 = 0; +return x_572; } } } @@ -3170,54 +3116,54 @@ case 11: switch (lean::obj_tag(x_2)) { case 11: { -obj* x_592; obj* x_594; obj* x_597; obj* x_599; uint8 x_602; -x_592 = lean::cnstr_get(x_1, 0); -lean::inc(x_592); -x_594 = lean::cnstr_get(x_1, 1); -lean::inc(x_594); +obj* x_573; obj* x_575; obj* x_578; obj* x_580; uint8 x_583; +x_573 = lean::cnstr_get(x_1, 0); +lean::inc(x_573); +x_575 = lean::cnstr_get(x_1, 1); +lean::inc(x_575); lean::dec(x_1); -x_597 = lean::cnstr_get(x_2, 0); -lean::inc(x_597); -x_599 = lean::cnstr_get(x_2, 1); -lean::inc(x_599); +x_578 = lean::cnstr_get(x_2, 0); +lean::inc(x_578); +x_580 = lean::cnstr_get(x_2, 1); +lean::inc(x_580); lean::dec(x_2); -x_602 = lean_name_dec_eq(x_592, x_597); -lean::dec(x_597); -lean::dec(x_592); -if (x_602 == 0) +x_583 = lean_name_dec_eq(x_573, x_578); +lean::dec(x_578); +lean::dec(x_573); +if (x_583 == 0) { -uint8 x_608; +uint8 x_589; lean::dec(x_0); -lean::dec(x_599); -lean::dec(x_594); -x_608 = 0; -return x_608; +lean::dec(x_580); +lean::dec(x_575); +x_589 = 0; +return x_589; } else { -uint8 x_609; -x_609 = l_Lean_IR_args_alphaEqv___main(x_0, x_594, x_599); -lean::dec(x_599); -lean::dec(x_594); -return x_609; +uint8 x_590; +x_590 = l_Lean_IR_args_alphaEqv___main(x_0, x_575, x_580); +lean::dec(x_580); +lean::dec(x_575); +return x_590; } } case 12: { -uint8 x_614; +uint8 x_595; lean::dec(x_1); lean::dec(x_0); -x_614 = 0; -return x_614; +x_595 = 0; +return x_595; } default: { -uint8 x_618; +uint8 x_599; lean::dec(x_1); lean::dec(x_0); lean::dec(x_2); -x_618 = 0; -return x_618; +x_599 = 0; +return x_599; } } } @@ -3227,23 +3173,23 @@ lean::dec(x_0); switch (lean::obj_tag(x_2)) { case 12: { -uint8 x_620; -x_620 = 1; -return x_620; +uint8 x_601; +x_601 = 1; +return x_601; } default: { -uint8 x_622; +uint8 x_603; lean::dec(x_2); -x_622 = 0; -return x_622; +x_603 = 0; +return x_603; } } } } } } -uint8 l_Lean_IR_alts_alphaEqv___main(obj* x_0, obj* x_1, obj* x_2) { +uint8 l_Lean_IR_Alts_alphaEqv___main(obj* x_0, obj* x_1, obj* x_2) { _start: { if (lean::obj_tag(x_1) == 0) @@ -3287,7 +3233,7 @@ x_17 = lean::cnstr_get(x_2, 1); lean::inc(x_17); lean::dec(x_2); lean::inc(x_0); -x_21 = l_Lean_IR_alt_alphaEqv___main(x_0, x_10, x_15); +x_21 = l_Lean_IR_Alt_alphaEqv___main(x_0, x_10, x_15); if (x_21 == 0) { lean::dec(x_17); @@ -3305,7 +3251,7 @@ goto _start; } } } -uint8 l_Lean_IR_alt_alphaEqv___main(obj* x_0, obj* x_1, obj* x_2) { +uint8 l_Lean_IR_Alt_alphaEqv___main(obj* x_0, obj* x_1, obj* x_2) { _start: { if (lean::obj_tag(x_1) == 0) @@ -3385,20 +3331,20 @@ x_4 = lean::box(x_3); return x_4; } } -obj* l_Lean_IR_alts_alphaEqv___main___boxed(obj* x_0, obj* x_1, obj* x_2) { +obj* l_Lean_IR_Alts_alphaEqv___main___boxed(obj* x_0, obj* x_1, obj* x_2) { _start: { uint8 x_3; obj* x_4; -x_3 = l_Lean_IR_alts_alphaEqv___main(x_0, x_1, x_2); +x_3 = l_Lean_IR_Alts_alphaEqv___main(x_0, x_1, x_2); x_4 = lean::box(x_3); return x_4; } } -obj* l_Lean_IR_alt_alphaEqv___main___boxed(obj* x_0, obj* x_1, obj* x_2) { +obj* l_Lean_IR_Alt_alphaEqv___main___boxed(obj* x_0, obj* x_1, obj* x_2) { _start: { uint8 x_3; obj* x_4; -x_3 = l_Lean_IR_alt_alphaEqv___main(x_0, x_1, x_2); +x_3 = l_Lean_IR_Alt_alphaEqv___main(x_0, x_1, x_2); x_4 = lean::box(x_3); return x_4; } @@ -3420,36 +3366,36 @@ x_4 = lean::box(x_3); return x_4; } } -uint8 l_Lean_IR_alts_alphaEqv(obj* x_0, obj* x_1, obj* x_2) { +uint8 l_Lean_IR_Alts_alphaEqv(obj* x_0, obj* x_1, obj* x_2) { _start: { uint8 x_3; -x_3 = l_Lean_IR_alts_alphaEqv___main(x_0, x_1, x_2); +x_3 = l_Lean_IR_Alts_alphaEqv___main(x_0, x_1, x_2); return x_3; } } -obj* l_Lean_IR_alts_alphaEqv___boxed(obj* x_0, obj* x_1, obj* x_2) { +obj* l_Lean_IR_Alts_alphaEqv___boxed(obj* x_0, obj* x_1, obj* x_2) { _start: { uint8 x_3; obj* x_4; -x_3 = l_Lean_IR_alts_alphaEqv(x_0, x_1, x_2); +x_3 = l_Lean_IR_Alts_alphaEqv(x_0, x_1, x_2); x_4 = lean::box(x_3); return x_4; } } -uint8 l_Lean_IR_alt_alphaEqv(obj* x_0, obj* x_1, obj* x_2) { +uint8 l_Lean_IR_Alt_alphaEqv(obj* x_0, obj* x_1, obj* x_2) { _start: { uint8 x_3; -x_3 = l_Lean_IR_alt_alphaEqv___main(x_0, x_1, x_2); +x_3 = l_Lean_IR_Alt_alphaEqv___main(x_0, x_1, x_2); return x_3; } } -obj* l_Lean_IR_alt_alphaEqv___boxed(obj* x_0, obj* x_1, obj* x_2) { +obj* l_Lean_IR_Alt_alphaEqv___boxed(obj* x_0, obj* x_1, obj* x_2) { _start: { uint8 x_3; obj* x_4; -x_3 = l_Lean_IR_alt_alphaEqv(x_0, x_1, x_2); +x_3 = l_Lean_IR_Alt_alphaEqv(x_0, x_1, x_2); x_4 = lean::box(x_3); return x_4; } @@ -3513,7 +3459,7 @@ lean::dec(x_0); return x_1; } } -obj* l___private_init_lean_compiler_ir_2__var_collect(obj* x_0, obj* x_1, obj* x_2) { +obj* l___private_init_lean_compiler_ir_2__collectVar(obj* x_0, obj* x_1, obj* x_2) { _start: { uint8 x_3; @@ -3595,7 +3541,7 @@ x_6 = lean::apply_2(x_1, x_2, x_5); return x_6; } } -obj* l___private_init_lean_compiler_ir_6__Arg_collect___main(obj* x_0, obj* x_1, obj* x_2) { +obj* l___private_init_lean_compiler_ir_6__collectArg___main(obj* x_0, obj* x_1, obj* x_2) { _start: { if (lean::obj_tag(x_0) == 0) @@ -3625,15 +3571,15 @@ return x_2; } } } -obj* l___private_init_lean_compiler_ir_6__Arg_collect(obj* x_0, obj* x_1, obj* x_2) { +obj* l___private_init_lean_compiler_ir_6__collectArg(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; -x_3 = l___private_init_lean_compiler_ir_6__Arg_collect___main(x_0, x_1, x_2); +x_3 = l___private_init_lean_compiler_ir_6__collectArg___main(x_0, x_1, x_2); return x_3; } } -obj* l___private_init_lean_compiler_ir_7__args_collect___main(obj* x_0, obj* x_1, obj* x_2) { +obj* l___private_init_lean_compiler_ir_7__collectArgs___main(obj* x_0, obj* x_1, obj* x_2) { _start: { if (lean::obj_tag(x_0) == 0) @@ -3650,22 +3596,22 @@ x_6 = lean::cnstr_get(x_0, 1); lean::inc(x_6); lean::dec(x_0); lean::inc(x_1); -x_10 = l___private_init_lean_compiler_ir_6__Arg_collect___main(x_4, x_1, x_2); +x_10 = l___private_init_lean_compiler_ir_6__collectArg___main(x_4, x_1, x_2); x_0 = x_6; x_2 = x_10; goto _start; } } } -obj* l___private_init_lean_compiler_ir_7__args_collect(obj* x_0, obj* x_1, obj* x_2) { +obj* l___private_init_lean_compiler_ir_7__collectArgs(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; -x_3 = l___private_init_lean_compiler_ir_7__args_collect___main(x_0, x_1, x_2); +x_3 = l___private_init_lean_compiler_ir_7__collectArgs___main(x_0, x_1, x_2); return x_3; } } -obj* l___private_init_lean_compiler_ir_8__Expr_collect___main(obj* x_0, obj* x_1, obj* x_2) { +obj* l___private_init_lean_compiler_ir_8__collectExpr___main(obj* x_0, obj* x_1, obj* x_2) { _start: { switch (lean::obj_tag(x_0)) { @@ -3675,7 +3621,7 @@ obj* x_3; obj* x_6; x_3 = lean::cnstr_get(x_0, 1); lean::inc(x_3); lean::dec(x_0); -x_6 = l___private_init_lean_compiler_ir_7__args_collect___main(x_3, x_1, x_2); +x_6 = l___private_init_lean_compiler_ir_7__collectArgs___main(x_3, x_1, x_2); return x_6; } case 2: @@ -3693,14 +3639,14 @@ if (x_13 == 0) obj* x_14; obj* x_15; obj* x_16; x_14 = lean::box(0); x_15 = l_RBMap_insert___main___at_Lean_NameSet_insert___spec__1(x_2, x_7, x_14); -x_16 = l___private_init_lean_compiler_ir_7__args_collect___main(x_9, x_1, x_15); +x_16 = l___private_init_lean_compiler_ir_7__collectArgs___main(x_9, x_1, x_15); return x_16; } else { obj* x_18; lean::dec(x_7); -x_18 = l___private_init_lean_compiler_ir_7__args_collect___main(x_9, x_1, x_2); +x_18 = l___private_init_lean_compiler_ir_7__collectArgs___main(x_9, x_1, x_2); return x_18; } } @@ -3770,7 +3716,7 @@ obj* x_40; obj* x_43; x_40 = lean::cnstr_get(x_0, 1); lean::inc(x_40); lean::dec(x_0); -x_43 = l___private_init_lean_compiler_ir_7__args_collect___main(x_40, x_1, x_2); +x_43 = l___private_init_lean_compiler_ir_7__collectArgs___main(x_40, x_1, x_2); return x_43; } case 7: @@ -3779,7 +3725,7 @@ obj* x_44; obj* x_47; x_44 = lean::cnstr_get(x_0, 1); lean::inc(x_44); lean::dec(x_0); -x_47 = l___private_init_lean_compiler_ir_7__args_collect___main(x_44, x_1, x_2); +x_47 = l___private_init_lean_compiler_ir_7__collectArgs___main(x_44, x_1, x_2); return x_47; } case 8: @@ -3797,14 +3743,14 @@ if (x_54 == 0) obj* x_55; obj* x_56; obj* x_57; x_55 = lean::box(0); x_56 = l_RBMap_insert___main___at_Lean_NameSet_insert___spec__1(x_2, x_48, x_55); -x_57 = l___private_init_lean_compiler_ir_7__args_collect___main(x_50, x_1, x_56); +x_57 = l___private_init_lean_compiler_ir_7__collectArgs___main(x_50, x_1, x_56); return x_57; } else { obj* x_59; lean::dec(x_48); -x_59 = l___private_init_lean_compiler_ir_7__args_collect___main(x_50, x_1, x_2); +x_59 = l___private_init_lean_compiler_ir_7__collectArgs___main(x_50, x_1, x_2); return x_59; } } @@ -3837,15 +3783,15 @@ return x_2; } } } -obj* l___private_init_lean_compiler_ir_8__Expr_collect(obj* x_0, obj* x_1, obj* x_2) { +obj* l___private_init_lean_compiler_ir_8__collectExpr(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; -x_3 = l___private_init_lean_compiler_ir_8__Expr_collect___main(x_0, x_1, x_2); +x_3 = l___private_init_lean_compiler_ir_8__collectExpr___main(x_0, x_1, x_2); return x_3; } } -obj* l___private_init_lean_compiler_ir_9__Fnbody_collect___main(obj* x_0, obj* x_1, obj* x_2) { +obj* l___private_init_lean_compiler_ir_9__collectFnBody___main(obj* x_0, obj* x_1, obj* x_2) { _start: { switch (lean::obj_tag(x_0)) { @@ -3860,7 +3806,7 @@ x_7 = lean::cnstr_get(x_0, 2); lean::inc(x_7); lean::dec(x_0); lean::inc(x_1); -x_11 = l___private_init_lean_compiler_ir_8__Expr_collect___main(x_5, x_1, x_2); +x_11 = l___private_init_lean_compiler_ir_8__collectExpr___main(x_5, x_1, x_2); x_12 = lean::box(0); x_13 = l_RBMap_insert___main___at_Lean_NameSet_insert___spec__1(x_1, x_3, x_12); x_0 = x_7; @@ -3882,7 +3828,7 @@ lean::inc(x_21); lean::dec(x_0); lean::inc(x_1); x_25 = l_List_foldl___main___at_Lean_IR_insertParams___spec__1(x_1, x_17); -x_26 = l___private_init_lean_compiler_ir_9__Fnbody_collect___main(x_19, x_25, x_2); +x_26 = l___private_init_lean_compiler_ir_9__collectFnBody___main(x_19, x_25, x_2); x_27 = lean::box(0); x_28 = l_RBMap_insert___main___at_Lean_NameSet_insert___spec__1(x_1, x_15, x_27); x_0 = x_21; @@ -4079,14 +4025,14 @@ if (x_109 == 0) obj* x_110; obj* x_111; obj* x_112; x_110 = lean::box(0); x_111 = l_RBMap_insert___main___at_Lean_NameSet_insert___spec__1(x_2, x_103, x_110); -x_112 = l___private_init_lean_compiler_ir_9__alts_collect___main(x_105, x_1, x_111); +x_112 = l___private_init_lean_compiler_ir_9__collectAlts___main(x_105, x_1, x_111); return x_112; } else { obj* x_114; lean::dec(x_103); -x_114 = l___private_init_lean_compiler_ir_9__alts_collect___main(x_105, x_1, x_2); +x_114 = l___private_init_lean_compiler_ir_9__collectAlts___main(x_105, x_1, x_2); return x_114; } } @@ -4125,14 +4071,14 @@ if (x_128 == 0) obj* x_129; obj* x_130; obj* x_131; x_129 = lean::box(0); x_130 = l_RBMap_insert___main___at_Lean_NameSet_insert___spec__1(x_2, x_122, x_129); -x_131 = l___private_init_lean_compiler_ir_7__args_collect___main(x_124, x_1, x_130); +x_131 = l___private_init_lean_compiler_ir_7__collectArgs___main(x_124, x_1, x_130); return x_131; } else { obj* x_133; lean::dec(x_122); -x_133 = l___private_init_lean_compiler_ir_7__args_collect___main(x_124, x_1, x_2); +x_133 = l___private_init_lean_compiler_ir_7__collectArgs___main(x_124, x_1, x_2); return x_133; } } @@ -4170,7 +4116,7 @@ goto _start; } } } -obj* l___private_init_lean_compiler_ir_9__alts_collect___main(obj* x_0, obj* x_1, obj* x_2) { +obj* l___private_init_lean_compiler_ir_9__collectAlts___main(obj* x_0, obj* x_1, obj* x_2) { _start: { if (lean::obj_tag(x_0) == 0) @@ -4187,14 +4133,14 @@ x_6 = lean::cnstr_get(x_0, 1); lean::inc(x_6); lean::dec(x_0); lean::inc(x_1); -x_10 = l___private_init_lean_compiler_ir_9__alt_collect___main(x_4, x_1, x_2); +x_10 = l___private_init_lean_compiler_ir_9__collectAlt___main(x_4, x_1, x_2); x_0 = x_6; x_2 = x_10; goto _start; } } } -obj* l___private_init_lean_compiler_ir_9__alt_collect___main(obj* x_0, obj* x_1, obj* x_2) { +obj* l___private_init_lean_compiler_ir_9__collectAlt___main(obj* x_0, obj* x_1, obj* x_2) { _start: { if (lean::obj_tag(x_0) == 0) @@ -4203,7 +4149,7 @@ obj* x_3; obj* x_6; x_3 = lean::cnstr_get(x_0, 1); lean::inc(x_3); lean::dec(x_0); -x_6 = l___private_init_lean_compiler_ir_9__Fnbody_collect___main(x_3, x_1, x_2); +x_6 = l___private_init_lean_compiler_ir_9__collectFnBody___main(x_3, x_1, x_2); return x_6; } else @@ -4212,32 +4158,32 @@ obj* x_7; obj* x_10; x_7 = lean::cnstr_get(x_0, 0); lean::inc(x_7); lean::dec(x_0); -x_10 = l___private_init_lean_compiler_ir_9__Fnbody_collect___main(x_7, x_1, x_2); +x_10 = l___private_init_lean_compiler_ir_9__collectFnBody___main(x_7, x_1, x_2); return x_10; } } } -obj* l___private_init_lean_compiler_ir_9__Fnbody_collect(obj* x_0, obj* x_1, obj* x_2) { +obj* l___private_init_lean_compiler_ir_9__collectFnBody(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; -x_3 = l___private_init_lean_compiler_ir_9__Fnbody_collect___main(x_0, x_1, x_2); +x_3 = l___private_init_lean_compiler_ir_9__collectFnBody___main(x_0, x_1, x_2); return x_3; } } -obj* l___private_init_lean_compiler_ir_9__alts_collect(obj* x_0, obj* x_1, obj* x_2) { +obj* l___private_init_lean_compiler_ir_9__collectAlts(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; -x_3 = l___private_init_lean_compiler_ir_9__alts_collect___main(x_0, x_1, x_2); +x_3 = l___private_init_lean_compiler_ir_9__collectAlts___main(x_0, x_1, x_2); return x_3; } } -obj* l___private_init_lean_compiler_ir_9__alt_collect(obj* x_0, obj* x_1, obj* x_2) { +obj* l___private_init_lean_compiler_ir_9__collectAlt(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; -x_3 = l___private_init_lean_compiler_ir_9__alt_collect___main(x_0, x_1, x_2); +x_3 = l___private_init_lean_compiler_ir_9__collectAlt___main(x_0, x_1, x_2); return x_3; } } @@ -4246,7 +4192,7 @@ _start: { obj* x_1; obj* x_2; x_1 = lean::box(0); -x_2 = l___private_init_lean_compiler_ir_9__Fnbody_collect___main(x_0, x_1, x_1); +x_2 = l___private_init_lean_compiler_ir_9__collectFnBody___main(x_0, x_1, x_1); return x_2; } } @@ -4263,14 +4209,18 @@ if (io_result_is_error(w)) return w; w = initialize_init_lean_name(w); if (io_result_is_error(w)) return w; w = initialize_init_lean_kvmap(w); + l_Lean_IR_MData_empty = _init_l_Lean_IR_MData_empty(); +lean::mark_persistent(l_Lean_IR_MData_empty); + l_Lean_IR_MData_HasEmptyc = _init_l_Lean_IR_MData_HasEmptyc(); +lean::mark_persistent(l_Lean_IR_MData_HasEmptyc); l_Lean_IR_IRType_HasBeq = _init_l_Lean_IR_IRType_HasBeq(); lean::mark_persistent(l_Lean_IR_IRType_HasBeq); l_Lean_IR_Litval_HasBeq = _init_l_Lean_IR_Litval_HasBeq(); lean::mark_persistent(l_Lean_IR_Litval_HasBeq); l_Lean_IR_CtorInfo_HasBeq = _init_l_Lean_IR_CtorInfo_HasBeq(); lean::mark_persistent(l_Lean_IR_CtorInfo_HasBeq); - l_Lean_IR_varid_hasAeqv = _init_l_Lean_IR_varid_hasAeqv(); -lean::mark_persistent(l_Lean_IR_varid_hasAeqv); + l_Lean_IR_VarId_hasAeqv = _init_l_Lean_IR_VarId_hasAeqv(); +lean::mark_persistent(l_Lean_IR_VarId_hasAeqv); l_Lean_IR_Arg_hasAeqv = _init_l_Lean_IR_Arg_hasAeqv(); lean::mark_persistent(l_Lean_IR_Arg_hasAeqv); l_Lean_IR_args_hasAeqv = _init_l_Lean_IR_args_hasAeqv(); diff --git a/src/stage0/init/lean/elaborator.cpp b/src/stage0/init/lean/elaborator.cpp index 117eeec52f..56897a10b3 100644 --- a/src/stage0/init/lean/elaborator.cpp +++ b/src/stage0/init/lean/elaborator.cpp @@ -48,6 +48,7 @@ extern obj* l_Lean_MessageLog_empty; obj* l_Lean_Elaborator_toPexpr___main___closed__46; extern "C" obj* lean_expr_mk_sort(obj*); obj* l_List_map___main___at_Lean_Elaborator_Declaration_elaborate___spec__7(obj*); +obj* l_Lean_KVMap_setBool(obj*, obj*, uint8); obj* l_Lean_Elaborator_OrderedRBMap_empty___at_Lean_Elaborator_oldElabCommand___spec__7___boxed(obj*); uint8 l_List_foldr___main___at_Lean_Elaborator_matchOpenSpec___spec__1(obj*, uint8, obj*); obj* l_List_mfilter___main___at_Lean_Elaborator_variables_elaborate___spec__9___lambda__1(obj*, uint8, obj*, obj*); @@ -150,6 +151,7 @@ obj* l_Lean_Elaborator_modifyCurrentScope___boxed(obj*, obj*, obj*, obj*); uint8 l_Lean_Parser_Syntax_isOfKind___main(obj*, obj*); extern obj* l_Lean_Parser_command_variables; obj* l_Lean_Elaborator_elabDefLike(obj*, obj*, obj*, obj*, obj*, obj*, obj*); +obj* l_Lean_KVMap_setNat(obj*, obj*, obj*); obj* l_Lean_Elaborator_toPexpr___main___closed__4; obj* l_Lean_Elaborator_declModifiersToPexpr___closed__2; obj* l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__17(obj*, obj*, obj*, obj*); @@ -185,7 +187,6 @@ obj* l_List_map___main___at_Lean_Elaborator_export_elaborate___spec__1(obj*, obj obj* l_Lean_Elaborator_toPexpr___main___closed__45; obj* l_Lean_Elaborator_toLevel___main___boxed(obj*, obj*, obj*, obj*); obj* l_RBNode_insert___at_Lean_Elaborator_OrderedRBMap_ofList___spec__3(obj*, obj*, obj*); -obj* l_Lean_Kvmap_setString(obj*, obj*, obj*); obj* l_RBNode_ins___main___at_Lean_Elaborator_OrderedRBMap_insert___spec__4___rarg(obj*, obj*, obj*, obj*); obj* l_Lean_Elaborator_universe_elaborate___closed__2; obj* l_Lean_Elaborator_toPexpr___main___closed__1; @@ -306,13 +307,13 @@ obj* string_append(obj*, obj*); obj* l_List_mmap___main___at_Lean_Elaborator_CommandParserConfig_registerNotationParser___spec__2___closed__2; obj* l_RBNode_ins___main___at_Lean_Elaborator_elabDefLike___spec__7___boxed(obj*, obj*, obj*, obj*); obj* l_Lean_Elaborator_Declaration_elaborate___lambda__3(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); -obj* l_Lean_Kvmap_setBool(obj*, obj*, uint8); obj* l_RBNode_ins___main___at_Lean_Elaborator_variables_elaborate___spec__8___boxed(obj*, obj*, obj*, obj*); obj* l_Lean_Elaborator_registerNotationMacro(obj*, obj*, obj*, obj*); obj* l_Lean_Elaborator_toPexpr___main___closed__20; extern obj* l_Lean_Parser_command_initQuot; obj* l_List_foldl___main___at_Lean_Elaborator_oldElabCommand___spec__16(obj*, obj*, obj*); obj* l_Lean_Elaborator_toPexpr___main___closed__48; +obj* l_Lean_KVMap_setName(obj*, obj*, obj*); obj* l_Lean_Elaborator_matchSpec___closed__1; extern obj* l_Lean_Parser_command_open_HasView; obj* l_Lean_Elaborator_inferModToPexpr___boxed(obj*); @@ -404,7 +405,6 @@ obj* l_RBNode_ins___main___at_Lean_Elaborator_oldElabCommand___spec__6___boxed(o obj* l_StateT_MonadExcept___rarg(obj*, obj*, obj*); obj* l_Lean_Elaborator_Declaration_elaborate___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_RBMap_insert___main___at_Lean_Elaborator_OrderedRBMap_insert___spec__1___rarg(obj*, obj*, obj*, obj*); -obj* l_Lean_Kvmap_setNat(obj*, obj*, obj*); obj* l_Lean_Elaborator_section_elaborate___closed__1; obj* l_Lean_Elaborator_currentScope___closed__1; uint8 l_RBNode_isRed___main___rarg(obj*); @@ -413,7 +413,6 @@ obj* l_Lean_Elaborator_toPexpr___main___lambda__1___boxed(obj*); obj* l_List_mmap___main___at_Lean_Elaborator_CommandParserConfig_registerNotationParser___spec__2(obj*); obj* l_Lean_Elaborator_setOption_elaborate___lambda__1(obj*, obj*); obj* l_Lean_Elaborator_noKind_elaborate___closed__1; -obj* l_Lean_Kvmap_setName(obj*, obj*, obj*); obj* l_List_foldr___main___at_Lean_Elaborator_toPexpr___main___spec__15___boxed(obj*, obj*); obj* l_RBMap_insert___main___at_Lean_Elaborator_OrderedRBMap_ofList___spec__2___rarg(obj*, obj*, obj*, obj*); obj* l_List_foldl___main___at_Lean_Elaborator_OrderedRBMap_ofList___spec__7___rarg(obj*, obj*, obj*); @@ -498,6 +497,7 @@ obj* l_RBMap_insert___main___at_Lean_Elaborator_oldElabCommand___spec__18(obj*, obj* l_Lean_Elaborator_mkState___closed__5; obj* l_Lean_Expander_error___at_Lean_Elaborator_processCommand___spec__2___rarg___boxed(obj*, obj*, obj*, obj*, obj*); obj* l_RBMap_find___main___at_Lean_Elaborator_OrderedRBMap_find___spec__1(obj*, obj*, obj*); +obj* l_Lean_Elaborator_toPexpr___main___closed__50; obj* l_RBMap_insert___main___at_Lean_Elaborator_registerNotationMacro___spec__1(obj*, obj*, obj*); obj* l_List_mfoldl___main___at_Lean_Elaborator_updateParserConfig___spec__2(obj*, obj*, obj*, obj*, obj*); extern obj* l_Lean_Parser_Term_sortApp_HasView; @@ -552,7 +552,6 @@ obj* l_Lean_Elaborator_getNamespace___boxed(obj*, obj*, obj*); obj* l_RBNode_ins___main___at_Lean_Elaborator_registerNotationMacro___spec__4(obj*, obj*, obj*, obj*); extern obj* l_Lean_Parser_command_universe_HasView; extern "C" obj* lean_name_mk_numeral(obj*, obj*); -obj* l_Lean_Kvmap_insertCore___main(obj*, obj*, obj*); obj* l_RBNode_find___main___at_Lean_Elaborator_variables_elaborate___spec__3(obj*, obj*, obj*, obj*); obj* l_Lean_Elaborator_OrderedRBMap_insert___rarg(obj*, obj*, obj*, obj*); obj* l_Lean_Elaborator_simpleBindersToPexpr(obj*, obj*, obj*, obj*); @@ -596,6 +595,7 @@ extern obj* l_Lean_Parser_Level_leading_HasView; obj* l_Lean_Elaborator_eoi_elaborate___boxed(obj*, obj*, obj*, obj*); obj* l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__5(obj*, obj*, obj*, obj*, obj*); obj* l_Lean_Elaborator_OrderedRBMap_insert___at_Lean_Elaborator_elabDefLike___spec__4(obj*, obj*, obj*); +obj* l_Lean_KVMap_setString(obj*, obj*, obj*); obj* l_Lean_Elaborator_CommandParserConfig_registerNotationParser___closed__1; obj* l_Lean_Parser_RecT_recurse___rarg(obj*, obj*); obj* l_Lean_Elaborator_notation_elaborate___lambda__1(obj*, obj*); @@ -615,6 +615,7 @@ obj* l_List_foldr___main___at_Lean_Elaborator_toPexpr___main___spec__9(obj*, obj obj* l_List_mmap___main___at_Lean_Elaborator_Declaration_elaborate___spec__8___boxed(obj*, obj*, obj*, obj*); obj* l_Lean_Elaborator_variables_elaborate___closed__2; obj* l_Lean_Elaborator_processCommand___lambda__1(obj*, obj*, obj*, obj*); +obj* l_Lean_KVMap_insertCore___main(obj*, obj*, obj*); obj* l_Lean_Elaborator_toPexpr___main___closed__16; obj* l_List_foldl___main___at_Lean_Elaborator_toPexpr___main___spec__22(obj*, obj*); obj* l_RBNode_balance1___main___rarg(obj*, obj*); @@ -4381,7 +4382,7 @@ _start: obj* x_2; obj* x_3; obj* x_4; obj* x_5; x_2 = lean::box(0); x_3 = l_Lean_Elaborator_Expr_mkAnnotation___closed__1; -x_4 = l_Lean_Kvmap_setName(x_2, x_3, x_0); +x_4 = l_Lean_KVMap_setName(x_2, x_3, x_0); x_5 = lean_expr_mk_mdata(x_4, x_1); return x_5; } @@ -5147,7 +5148,7 @@ return x_49; } else { -obj* x_50; obj* x_52; obj* x_53; obj* x_55; obj* x_57; obj* x_58; obj* x_59; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_66; obj* x_67; obj* x_68; +obj* x_50; obj* x_52; obj* x_53; obj* x_55; obj* x_57; obj* x_58; obj* x_61; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_66; obj* x_67; obj* x_68; x_50 = lean::cnstr_get(x_42, 0); if (lean::is_exclusive(x_42)) { x_52 = x_42; @@ -5166,13 +5167,13 @@ if (lean::is_exclusive(x_50)) { lean::dec(x_50); x_57 = lean::box(0); } -x_58 = lean::box(0); -x_59 = lean::cnstr_get(x_18, 0); -lean::inc(x_59); +x_58 = lean::cnstr_get(x_18, 0); +lean::inc(x_58); lean::dec(x_18); -x_62 = l_Lean_Elaborator_mangleIdent(x_59); +x_61 = l_Lean_Elaborator_mangleIdent(x_58); +x_62 = lean::box(0); x_63 = l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__5___closed__1; -x_64 = l_Lean_Kvmap_setName(x_58, x_63, x_62); +x_64 = l_Lean_KVMap_setName(x_62, x_63, x_61); x_65 = lean_expr_mk_mdata(x_64, x_37); if (lean::is_scalar(x_17)) { x_66 = lean::alloc_cnstr(1, 2, 0); @@ -5851,7 +5852,7 @@ return x_49; } else { -obj* x_50; obj* x_52; obj* x_53; obj* x_55; obj* x_57; obj* x_58; obj* x_59; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_66; obj* x_67; obj* x_68; +obj* x_50; obj* x_52; obj* x_53; obj* x_55; obj* x_57; obj* x_58; obj* x_61; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_66; obj* x_67; obj* x_68; x_50 = lean::cnstr_get(x_42, 0); if (lean::is_exclusive(x_42)) { x_52 = x_42; @@ -5870,13 +5871,13 @@ if (lean::is_exclusive(x_50)) { lean::dec(x_50); x_57 = lean::box(0); } -x_58 = lean::box(0); -x_59 = lean::cnstr_get(x_18, 0); -lean::inc(x_59); +x_58 = lean::cnstr_get(x_18, 0); +lean::inc(x_58); lean::dec(x_18); -x_62 = l_Lean_Elaborator_mangleIdent(x_59); +x_61 = l_Lean_Elaborator_mangleIdent(x_58); +x_62 = lean::box(0); x_63 = l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__5___closed__1; -x_64 = l_Lean_Kvmap_setName(x_58, x_63, x_62); +x_64 = l_Lean_KVMap_setName(x_62, x_63, x_61); x_65 = lean_expr_mk_mdata(x_64, x_37); if (lean::is_scalar(x_17)) { x_66 = lean::alloc_cnstr(1, 2, 0); @@ -6555,7 +6556,7 @@ return x_49; } else { -obj* x_50; obj* x_52; obj* x_53; obj* x_55; obj* x_57; obj* x_58; obj* x_59; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_66; obj* x_67; obj* x_68; +obj* x_50; obj* x_52; obj* x_53; obj* x_55; obj* x_57; obj* x_58; obj* x_61; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_66; obj* x_67; obj* x_68; x_50 = lean::cnstr_get(x_42, 0); if (lean::is_exclusive(x_42)) { x_52 = x_42; @@ -6574,13 +6575,13 @@ if (lean::is_exclusive(x_50)) { lean::dec(x_50); x_57 = lean::box(0); } -x_58 = lean::box(0); -x_59 = lean::cnstr_get(x_18, 0); -lean::inc(x_59); +x_58 = lean::cnstr_get(x_18, 0); +lean::inc(x_58); lean::dec(x_18); -x_62 = l_Lean_Elaborator_mangleIdent(x_59); +x_61 = l_Lean_Elaborator_mangleIdent(x_58); +x_62 = lean::box(0); x_63 = l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__5___closed__1; -x_64 = l_Lean_Kvmap_setName(x_58, x_63, x_62); +x_64 = l_Lean_KVMap_setName(x_62, x_63, x_61); x_65 = lean_expr_mk_mdata(x_64, x_37); if (lean::is_scalar(x_17)) { x_66 = lean::alloc_cnstr(1, 2, 0); @@ -7259,7 +7260,7 @@ return x_49; } else { -obj* x_50; obj* x_52; obj* x_53; obj* x_55; obj* x_57; obj* x_58; obj* x_59; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_66; obj* x_67; obj* x_68; +obj* x_50; obj* x_52; obj* x_53; obj* x_55; obj* x_57; obj* x_58; obj* x_61; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_66; obj* x_67; obj* x_68; x_50 = lean::cnstr_get(x_42, 0); if (lean::is_exclusive(x_42)) { x_52 = x_42; @@ -7278,13 +7279,13 @@ if (lean::is_exclusive(x_50)) { lean::dec(x_50); x_57 = lean::box(0); } -x_58 = lean::box(0); -x_59 = lean::cnstr_get(x_18, 0); -lean::inc(x_59); +x_58 = lean::cnstr_get(x_18, 0); +lean::inc(x_58); lean::dec(x_18); -x_62 = l_Lean_Elaborator_mangleIdent(x_59); +x_61 = l_Lean_Elaborator_mangleIdent(x_58); +x_62 = lean::box(0); x_63 = l_List_mmap___main___at_Lean_Elaborator_toPexpr___main___spec__5___closed__1; -x_64 = l_Lean_Kvmap_setName(x_58, x_63, x_62); +x_64 = l_Lean_KVMap_setName(x_62, x_63, x_61); x_65 = lean_expr_mk_mdata(x_64, x_37); if (lean::is_scalar(x_17)) { x_66 = lean::alloc_cnstr(1, 2, 0); @@ -8074,7 +8075,7 @@ lean::inc(x_9); lean::dec(x_2); x_12 = lean::box(0); x_13 = lean_name_mk_numeral(x_12, x_7); -x_14 = l_Lean_Kvmap_setName(x_0, x_13, x_9); +x_14 = l_Lean_KVMap_setName(x_0, x_13, x_9); x_0 = x_14; x_1 = x_4; goto _start; @@ -8237,7 +8238,7 @@ lean::inc(x_9); lean::dec(x_2); x_12 = lean::box(0); x_13 = lean_name_mk_numeral(x_12, x_7); -x_14 = l_Lean_Kvmap_setName(x_0, x_13, x_9); +x_14 = l_Lean_KVMap_setName(x_0, x_13, x_9); x_0 = x_14; x_1 = x_4; goto _start; @@ -8863,7 +8864,21 @@ x_2 = lean::mk_string("annotation"); x_3 = lean_name_mk_string(x_1, x_2); x_4 = lean::mk_string("preresolved"); x_5 = lean_name_mk_string(x_1, x_4); -x_6 = l_Lean_Kvmap_setName(x_0, x_3, x_5); +x_6 = l_Lean_KVMap_setName(x_0, x_3, x_5); +return x_6; +} +} +obj* _init_l_Lean_Elaborator_toPexpr___main___closed__50() { +_start: +{ +obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; +x_0 = lean::box(0); +x_1 = lean::mk_string("annotation"); +x_2 = lean_name_mk_string(x_0, x_1); +x_3 = lean::mk_string("preresolved"); +x_4 = lean_name_mk_string(x_0, x_3); +x_5 = lean::box(0); +x_6 = l_Lean_KVMap_setName(x_5, x_2, x_4); return x_6; } } @@ -9066,7 +9081,7 @@ return x_87; } else { -obj* x_88; obj* x_91; obj* x_94; obj* x_97; obj* x_98; obj* x_99; obj* x_101; obj* x_102; obj* x_103; obj* x_106; obj* x_107; obj* x_108; obj* x_109; obj* x_110; +obj* x_88; obj* x_91; obj* x_94; obj* x_97; obj* x_98; obj* x_100; obj* x_101; obj* x_102; obj* x_103; obj* x_106; obj* x_107; obj* x_108; obj* x_109; obj* x_110; x_88 = lean::cnstr_get(x_83, 0); lean::inc(x_88); lean::dec(x_83); @@ -9077,16 +9092,16 @@ x_94 = lean::cnstr_get(x_91, 2); lean::inc(x_94); lean::dec(x_91); x_97 = l_Lean_FileMap_toPosition(x_94, x_88); -x_98 = lean::box(0); -x_99 = lean::cnstr_get(x_97, 1); -lean::inc(x_99); +x_98 = lean::cnstr_get(x_97, 1); +lean::inc(x_98); +x_100 = lean::box(0); x_101 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_102 = l_Lean_Kvmap_setNat(x_98, x_101, x_99); +x_102 = l_Lean_KVMap_setNat(x_100, x_101, x_98); x_103 = lean::cnstr_get(x_97, 0); lean::inc(x_103); lean::dec(x_97); x_106 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_107 = l_Lean_Kvmap_setNat(x_102, x_106, x_103); +x_107 = l_Lean_KVMap_setNat(x_102, x_106, x_103); x_108 = lean_expr_mk_mdata(x_107, x_78); if (lean::is_scalar(x_82)) { x_109 = lean::alloc_cnstr(0, 2, 0); @@ -9281,7 +9296,7 @@ if (lean::is_exclusive(x_181)) { } x_189 = l_Lean_Elaborator_toPexpr___main___closed__22; x_190 = 1; -x_191 = l_Lean_Kvmap_setBool(x_165, x_189, x_190); +x_191 = l_Lean_KVMap_setBool(x_165, x_189, x_190); x_192 = lean_expr_mk_mdata(x_191, x_167); x_193 = l_List_foldl___main___at_Lean_Expr_mkApp___spec__1(x_192, x_184); if (lean::is_scalar(x_188)) { @@ -9535,14 +9550,14 @@ if (lean::is_exclusive(x_247)) { lean::dec(x_247); x_311 = lean::box(0); } -x_312 = lean::box(0); -x_313 = lean::mk_nat_obj(0u); -x_314 = l_List_lengthAux___main___rarg(x_242, x_313); +x_312 = lean::mk_nat_obj(0u); +x_313 = l_List_lengthAux___main___rarg(x_242, x_312); +x_314 = lean::box(0); x_315 = l_Lean_Elaborator_toPexpr___main___closed__25; -x_316 = l_Lean_Kvmap_setNat(x_312, x_315, x_314); +x_316 = l_Lean_KVMap_setNat(x_314, x_315, x_313); x_317 = l_Lean_Elaborator_toPexpr___main___closed__26; x_318 = 0; -x_319 = l_Lean_Kvmap_setBool(x_316, x_317, x_318); +x_319 = l_Lean_KVMap_setBool(x_316, x_317, x_318); x_320 = lean::cnstr_get(x_210, 1); lean::inc(x_320); lean::dec(x_210); @@ -9554,7 +9569,7 @@ if (lean::obj_tag(x_320) == 0) obj* x_326; obj* x_327; obj* x_328; obj* x_329; obj* x_330; x_326 = l_Lean_Elaborator_toPexpr___main___closed__28; x_327 = l_Lean_Elaborator_toPexpr___main___closed__29; -x_328 = l_Lean_Kvmap_setName(x_319, x_326, x_327); +x_328 = l_Lean_KVMap_setName(x_319, x_326, x_327); x_329 = lean_expr_mk_mdata(x_328, x_325); if (lean::is_scalar(x_311)) { x_330 = lean::alloc_cnstr(0, 2, 0); @@ -9591,7 +9606,7 @@ x_339 = lean::box(0); x_340 = l_Option_getOrElse___main___rarg(x_338, x_339); lean::dec(x_338); x_342 = l_Lean_Elaborator_toPexpr___main___closed__28; -x_343 = l_Lean_Kvmap_setName(x_319, x_342, x_340); +x_343 = l_Lean_KVMap_setName(x_319, x_342, x_340); x_344 = lean_expr_mk_mdata(x_343, x_325); if (lean::is_scalar(x_311)) { x_345 = lean::alloc_cnstr(0, 2, 0); @@ -9873,14 +9888,14 @@ if (lean::is_exclusive(x_407)) { lean::dec(x_407); x_476 = lean::box(0); } -x_477 = lean::box(0); -x_478 = lean::mk_nat_obj(0u); -x_479 = l_List_lengthAux___main___rarg(x_402, x_478); +x_477 = lean::mk_nat_obj(0u); +x_478 = l_List_lengthAux___main___rarg(x_402, x_477); +x_479 = lean::box(0); x_480 = l_Lean_Elaborator_toPexpr___main___closed__25; -x_481 = l_Lean_Kvmap_setNat(x_477, x_480, x_479); +x_481 = l_Lean_KVMap_setNat(x_479, x_480, x_478); x_482 = l_Lean_Elaborator_toPexpr___main___closed__26; x_483 = lean::unbox(x_380); -x_484 = l_Lean_Kvmap_setBool(x_481, x_482, x_483); +x_484 = l_Lean_KVMap_setBool(x_481, x_482, x_483); x_485 = lean::cnstr_get(x_210, 1); lean::inc(x_485); lean::dec(x_210); @@ -9892,7 +9907,7 @@ if (lean::obj_tag(x_485) == 0) obj* x_491; obj* x_492; obj* x_493; obj* x_494; obj* x_495; x_491 = l_Lean_Elaborator_toPexpr___main___closed__28; x_492 = l_Lean_Elaborator_toPexpr___main___closed__29; -x_493 = l_Lean_Kvmap_setName(x_484, x_491, x_492); +x_493 = l_Lean_KVMap_setName(x_484, x_491, x_492); x_494 = lean_expr_mk_mdata(x_493, x_490); if (lean::is_scalar(x_476)) { x_495 = lean::alloc_cnstr(0, 2, 0); @@ -9929,7 +9944,7 @@ x_504 = lean::box(0); x_505 = l_Option_getOrElse___main___rarg(x_503, x_504); lean::dec(x_503); x_507 = l_Lean_Elaborator_toPexpr___main___closed__28; -x_508 = l_Lean_Kvmap_setName(x_484, x_507, x_505); +x_508 = l_Lean_KVMap_setName(x_484, x_507, x_505); x_509 = lean_expr_mk_mdata(x_508, x_490); if (lean::is_scalar(x_476)) { x_510 = lean::alloc_cnstr(0, 2, 0); @@ -10158,14 +10173,14 @@ if (lean::is_exclusive(x_539)) { lean::dec(x_539); x_606 = lean::box(0); } -x_607 = lean::box(0); -x_608 = lean::mk_nat_obj(0u); -x_609 = l_List_lengthAux___main___rarg(x_534, x_608); +x_607 = lean::mk_nat_obj(0u); +x_608 = l_List_lengthAux___main___rarg(x_534, x_607); +x_609 = lean::box(0); x_610 = l_Lean_Elaborator_toPexpr___main___closed__25; -x_611 = l_Lean_Kvmap_setNat(x_607, x_610, x_609); +x_611 = l_Lean_KVMap_setNat(x_609, x_610, x_608); x_612 = l_Lean_Elaborator_toPexpr___main___closed__26; x_613 = 1; -x_614 = l_Lean_Kvmap_setBool(x_611, x_612, x_613); +x_614 = l_Lean_KVMap_setBool(x_611, x_612, x_613); x_615 = lean::cnstr_get(x_210, 1); lean::inc(x_615); lean::dec(x_210); @@ -10177,7 +10192,7 @@ if (lean::obj_tag(x_615) == 0) obj* x_621; obj* x_622; obj* x_623; obj* x_624; obj* x_625; x_621 = l_Lean_Elaborator_toPexpr___main___closed__28; x_622 = l_Lean_Elaborator_toPexpr___main___closed__29; -x_623 = l_Lean_Kvmap_setName(x_614, x_621, x_622); +x_623 = l_Lean_KVMap_setName(x_614, x_621, x_622); x_624 = lean_expr_mk_mdata(x_623, x_620); if (lean::is_scalar(x_606)) { x_625 = lean::alloc_cnstr(0, 2, 0); @@ -10214,7 +10229,7 @@ x_634 = lean::box(0); x_635 = l_Option_getOrElse___main___rarg(x_633, x_634); lean::dec(x_633); x_637 = l_Lean_Elaborator_toPexpr___main___closed__28; -x_638 = l_Lean_Kvmap_setName(x_614, x_637, x_635); +x_638 = l_Lean_KVMap_setName(x_614, x_637, x_635); x_639 = lean_expr_mk_mdata(x_638, x_620); if (lean::is_scalar(x_606)) { x_640 = lean::alloc_cnstr(0, 2, 0); @@ -10489,14 +10504,14 @@ if (lean::is_exclusive(x_698)) { lean::dec(x_698); x_767 = lean::box(0); } -x_768 = lean::box(0); -x_769 = lean::mk_nat_obj(0u); -x_770 = l_List_lengthAux___main___rarg(x_693, x_769); +x_768 = lean::mk_nat_obj(0u); +x_769 = l_List_lengthAux___main___rarg(x_693, x_768); +x_770 = lean::box(0); x_771 = l_Lean_Elaborator_toPexpr___main___closed__25; -x_772 = l_Lean_Kvmap_setNat(x_768, x_771, x_770); +x_772 = l_Lean_KVMap_setNat(x_770, x_771, x_769); x_773 = l_Lean_Elaborator_toPexpr___main___closed__26; x_774 = lean::unbox(x_671); -x_775 = l_Lean_Kvmap_setBool(x_772, x_773, x_774); +x_775 = l_Lean_KVMap_setBool(x_772, x_773, x_774); x_776 = lean::cnstr_get(x_210, 1); lean::inc(x_776); lean::dec(x_210); @@ -10508,7 +10523,7 @@ if (lean::obj_tag(x_776) == 0) obj* x_782; obj* x_783; obj* x_784; obj* x_785; obj* x_786; x_782 = l_Lean_Elaborator_toPexpr___main___closed__28; x_783 = l_Lean_Elaborator_toPexpr___main___closed__29; -x_784 = l_Lean_Kvmap_setName(x_775, x_782, x_783); +x_784 = l_Lean_KVMap_setName(x_775, x_782, x_783); x_785 = lean_expr_mk_mdata(x_784, x_781); if (lean::is_scalar(x_767)) { x_786 = lean::alloc_cnstr(0, 2, 0); @@ -10545,7 +10560,7 @@ x_795 = lean::box(0); x_796 = l_Option_getOrElse___main___rarg(x_794, x_795); lean::dec(x_794); x_798 = l_Lean_Elaborator_toPexpr___main___closed__28; -x_799 = l_Lean_Kvmap_setName(x_775, x_798, x_796); +x_799 = l_Lean_KVMap_setName(x_775, x_798, x_796); x_800 = lean_expr_mk_mdata(x_799, x_781); if (lean::is_scalar(x_767)) { x_801 = lean::alloc_cnstr(0, 2, 0); @@ -10660,18 +10675,18 @@ goto lbl_16; } else { -obj* x_841; obj* x_843; obj* x_846; obj* x_847; obj* x_848; obj* x_850; obj* x_851; obj* x_852; obj* x_853; obj* x_855; obj* x_856; +obj* x_841; obj* x_843; obj* x_846; obj* x_847; obj* x_849; obj* x_850; obj* x_851; obj* x_852; obj* x_853; obj* x_855; obj* x_856; x_841 = lean::cnstr_get(x_821, 0); lean::inc(x_841); x_843 = lean::cnstr_get(x_821, 1); lean::inc(x_843); lean::dec(x_821); -x_846 = lean::box(0); -x_847 = lean::mk_nat_obj(0u); -x_848 = l_List_lengthAux___main___rarg(x_10, x_847); +x_846 = lean::mk_nat_obj(0u); +x_847 = l_List_lengthAux___main___rarg(x_10, x_846); lean::dec(x_10); +x_849 = lean::box(0); x_850 = l_Lean_Elaborator_toPexpr___main___closed__32; -x_851 = l_Lean_Kvmap_setNat(x_846, x_850, x_848); +x_851 = l_Lean_KVMap_setNat(x_849, x_850, x_847); x_852 = l_List_reverse___rarg(x_843); x_853 = l_List_foldr___main___at_Lean_Elaborator_toPexpr___main___spec__18(x_841, x_852); lean::dec(x_841); @@ -10725,7 +10740,7 @@ return x_875; } else { -obj* x_876; obj* x_879; obj* x_882; obj* x_885; obj* x_886; obj* x_887; obj* x_889; obj* x_890; obj* x_891; obj* x_894; obj* x_895; obj* x_896; obj* x_897; obj* x_898; +obj* x_876; obj* x_879; obj* x_882; obj* x_885; obj* x_886; obj* x_888; obj* x_889; obj* x_890; obj* x_891; obj* x_894; obj* x_895; obj* x_896; obj* x_897; obj* x_898; x_876 = lean::cnstr_get(x_871, 0); lean::inc(x_876); lean::dec(x_871); @@ -10736,16 +10751,16 @@ x_882 = lean::cnstr_get(x_879, 2); lean::inc(x_882); lean::dec(x_879); x_885 = l_Lean_FileMap_toPosition(x_882, x_876); -x_886 = lean::box(0); -x_887 = lean::cnstr_get(x_885, 1); -lean::inc(x_887); +x_886 = lean::cnstr_get(x_885, 1); +lean::inc(x_886); +x_888 = lean::box(0); x_889 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_890 = l_Lean_Kvmap_setNat(x_886, x_889, x_887); +x_890 = l_Lean_KVMap_setNat(x_888, x_889, x_886); x_891 = lean::cnstr_get(x_885, 0); lean::inc(x_891); lean::dec(x_885); x_894 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_895 = l_Lean_Kvmap_setNat(x_890, x_894, x_891); +x_895 = l_Lean_KVMap_setNat(x_890, x_894, x_891); x_896 = lean_expr_mk_mdata(x_895, x_870); x_897 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_897, 0, x_896); @@ -10802,7 +10817,7 @@ return x_918; } else { -obj* x_919; obj* x_922; obj* x_925; obj* x_928; obj* x_929; obj* x_930; obj* x_932; obj* x_933; obj* x_934; obj* x_937; obj* x_938; obj* x_939; obj* x_940; obj* x_941; +obj* x_919; obj* x_922; obj* x_925; obj* x_928; obj* x_929; obj* x_931; obj* x_932; obj* x_933; obj* x_934; obj* x_937; obj* x_938; obj* x_939; obj* x_940; obj* x_941; x_919 = lean::cnstr_get(x_914, 0); lean::inc(x_919); lean::dec(x_914); @@ -10813,16 +10828,16 @@ x_925 = lean::cnstr_get(x_922, 2); lean::inc(x_925); lean::dec(x_922); x_928 = l_Lean_FileMap_toPosition(x_925, x_919); -x_929 = lean::box(0); -x_930 = lean::cnstr_get(x_928, 1); -lean::inc(x_930); +x_929 = lean::cnstr_get(x_928, 1); +lean::inc(x_929); +x_931 = lean::box(0); x_932 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_933 = l_Lean_Kvmap_setNat(x_929, x_932, x_930); +x_933 = l_Lean_KVMap_setNat(x_931, x_932, x_929); x_934 = lean::cnstr_get(x_928, 0); lean::inc(x_934); lean::dec(x_928); x_937 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_938 = l_Lean_Kvmap_setNat(x_933, x_937, x_934); +x_938 = l_Lean_KVMap_setNat(x_933, x_937, x_934); x_939 = lean_expr_mk_mdata(x_938, x_913); x_940 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_940, 0, x_939); @@ -10935,7 +10950,7 @@ return x_979; } else { -obj* x_980; obj* x_983; obj* x_986; obj* x_989; obj* x_990; obj* x_991; obj* x_993; obj* x_994; obj* x_995; obj* x_998; obj* x_999; obj* x_1000; obj* x_1001; obj* x_1002; +obj* x_980; obj* x_983; obj* x_986; obj* x_989; obj* x_990; obj* x_992; obj* x_993; obj* x_994; obj* x_995; obj* x_998; obj* x_999; obj* x_1000; obj* x_1001; obj* x_1002; x_980 = lean::cnstr_get(x_975, 0); lean::inc(x_980); lean::dec(x_975); @@ -10946,16 +10961,16 @@ x_986 = lean::cnstr_get(x_983, 2); lean::inc(x_986); lean::dec(x_983); x_989 = l_Lean_FileMap_toPosition(x_986, x_980); -x_990 = lean::box(0); -x_991 = lean::cnstr_get(x_989, 1); -lean::inc(x_991); +x_990 = lean::cnstr_get(x_989, 1); +lean::inc(x_990); +x_992 = lean::box(0); x_993 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_994 = l_Lean_Kvmap_setNat(x_990, x_993, x_991); +x_994 = l_Lean_KVMap_setNat(x_992, x_993, x_990); x_995 = lean::cnstr_get(x_989, 0); lean::inc(x_995); lean::dec(x_989); x_998 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_999 = l_Lean_Kvmap_setNat(x_994, x_998, x_995); +x_999 = l_Lean_KVMap_setNat(x_994, x_998, x_995); x_1000 = lean_expr_mk_mdata(x_999, x_974); if (lean::is_scalar(x_972)) { x_1001 = lean::alloc_cnstr(0, 2, 0); @@ -11085,7 +11100,7 @@ return x_1040; } else { -obj* x_1041; obj* x_1044; obj* x_1047; obj* x_1050; obj* x_1051; obj* x_1052; obj* x_1054; obj* x_1055; obj* x_1056; obj* x_1059; obj* x_1060; obj* x_1061; obj* x_1062; obj* x_1063; +obj* x_1041; obj* x_1044; obj* x_1047; obj* x_1050; obj* x_1051; obj* x_1053; obj* x_1054; obj* x_1055; obj* x_1056; obj* x_1059; obj* x_1060; obj* x_1061; obj* x_1062; obj* x_1063; x_1041 = lean::cnstr_get(x_1036, 0); lean::inc(x_1041); lean::dec(x_1036); @@ -11096,16 +11111,16 @@ x_1047 = lean::cnstr_get(x_1044, 2); lean::inc(x_1047); lean::dec(x_1044); x_1050 = l_Lean_FileMap_toPosition(x_1047, x_1041); -x_1051 = lean::box(0); -x_1052 = lean::cnstr_get(x_1050, 1); -lean::inc(x_1052); +x_1051 = lean::cnstr_get(x_1050, 1); +lean::inc(x_1051); +x_1053 = lean::box(0); x_1054 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_1055 = l_Lean_Kvmap_setNat(x_1051, x_1054, x_1052); +x_1055 = l_Lean_KVMap_setNat(x_1053, x_1054, x_1051); x_1056 = lean::cnstr_get(x_1050, 0); lean::inc(x_1056); lean::dec(x_1050); x_1059 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_1060 = l_Lean_Kvmap_setNat(x_1055, x_1059, x_1056); +x_1060 = l_Lean_KVMap_setNat(x_1055, x_1059, x_1056); x_1061 = lean_expr_mk_mdata(x_1060, x_1035); if (lean::is_scalar(x_1033)) { x_1062 = lean::alloc_cnstr(0, 2, 0); @@ -11246,7 +11261,7 @@ return x_1109; } else { -obj* x_1110; obj* x_1113; obj* x_1116; obj* x_1119; obj* x_1120; obj* x_1121; obj* x_1123; obj* x_1124; obj* x_1125; obj* x_1128; obj* x_1129; obj* x_1130; obj* x_1131; obj* x_1132; +obj* x_1110; obj* x_1113; obj* x_1116; obj* x_1119; obj* x_1120; obj* x_1122; obj* x_1123; obj* x_1124; obj* x_1125; obj* x_1128; obj* x_1129; obj* x_1130; obj* x_1131; obj* x_1132; x_1110 = lean::cnstr_get(x_1105, 0); lean::inc(x_1110); lean::dec(x_1105); @@ -11257,16 +11272,16 @@ x_1116 = lean::cnstr_get(x_1113, 2); lean::inc(x_1116); lean::dec(x_1113); x_1119 = l_Lean_FileMap_toPosition(x_1116, x_1110); -x_1120 = lean::box(0); -x_1121 = lean::cnstr_get(x_1119, 1); -lean::inc(x_1121); +x_1120 = lean::cnstr_get(x_1119, 1); +lean::inc(x_1120); +x_1122 = lean::box(0); x_1123 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_1124 = l_Lean_Kvmap_setNat(x_1120, x_1123, x_1121); +x_1124 = l_Lean_KVMap_setNat(x_1122, x_1123, x_1120); x_1125 = lean::cnstr_get(x_1119, 0); lean::inc(x_1125); lean::dec(x_1119); x_1128 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_1129 = l_Lean_Kvmap_setNat(x_1124, x_1128, x_1125); +x_1129 = l_Lean_KVMap_setNat(x_1124, x_1128, x_1125); x_1130 = lean_expr_mk_mdata(x_1129, x_1104); if (lean::is_scalar(x_1102)) { x_1131 = lean::alloc_cnstr(0, 2, 0); @@ -11385,7 +11400,7 @@ return x_1160; } else { -obj* x_1161; obj* x_1164; obj* x_1167; obj* x_1170; obj* x_1171; obj* x_1172; obj* x_1174; obj* x_1175; obj* x_1176; obj* x_1179; obj* x_1180; obj* x_1181; obj* x_1182; obj* x_1183; +obj* x_1161; obj* x_1164; obj* x_1167; obj* x_1170; obj* x_1171; obj* x_1173; obj* x_1174; obj* x_1175; obj* x_1176; obj* x_1179; obj* x_1180; obj* x_1181; obj* x_1182; obj* x_1183; x_1161 = lean::cnstr_get(x_1156, 0); lean::inc(x_1161); lean::dec(x_1156); @@ -11396,16 +11411,16 @@ x_1167 = lean::cnstr_get(x_1164, 2); lean::inc(x_1167); lean::dec(x_1164); x_1170 = l_Lean_FileMap_toPosition(x_1167, x_1161); -x_1171 = lean::box(0); -x_1172 = lean::cnstr_get(x_1170, 1); -lean::inc(x_1172); +x_1171 = lean::cnstr_get(x_1170, 1); +lean::inc(x_1171); +x_1173 = lean::box(0); x_1174 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_1175 = l_Lean_Kvmap_setNat(x_1171, x_1174, x_1172); +x_1175 = l_Lean_KVMap_setNat(x_1173, x_1174, x_1171); x_1176 = lean::cnstr_get(x_1170, 0); lean::inc(x_1176); lean::dec(x_1170); x_1179 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_1180 = l_Lean_Kvmap_setNat(x_1175, x_1179, x_1176); +x_1180 = l_Lean_KVMap_setNat(x_1175, x_1179, x_1176); x_1181 = lean_expr_mk_mdata(x_1180, x_1155); if (lean::is_scalar(x_1153)) { x_1182 = lean::alloc_cnstr(0, 2, 0); @@ -11524,7 +11539,7 @@ x_1224 = lean::alloc_cnstr(3, 1, 0); lean::cnstr_set(x_1224, 0, x_1221); x_1225 = lean::box(0); x_1226 = l_Lean_Elaborator_toPexpr___main___closed__37; -x_1227 = l_Lean_Kvmap_insertCore___main(x_1225, x_1226, x_1224); +x_1227 = l_Lean_KVMap_insertCore___main(x_1225, x_1226, x_1224); x_1228 = lean_expr_mk_mdata(x_1227, x_1216); if (x_20 == 0) { @@ -11566,12 +11581,12 @@ x_1243 = l_Lean_FileMap_toPosition(x_1240, x_1234); x_1244 = lean::cnstr_get(x_1243, 1); lean::inc(x_1244); x_1246 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_1247 = l_Lean_Kvmap_setNat(x_1225, x_1246, x_1244); +x_1247 = l_Lean_KVMap_setNat(x_1225, x_1246, x_1244); x_1248 = lean::cnstr_get(x_1243, 0); lean::inc(x_1248); lean::dec(x_1243); x_1251 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_1252 = l_Lean_Kvmap_setNat(x_1247, x_1251, x_1248); +x_1252 = l_Lean_KVMap_setNat(x_1247, x_1251, x_1248); x_1253 = lean_expr_mk_mdata(x_1252, x_1228); if (lean::is_scalar(x_1220)) { x_1254 = lean::alloc_cnstr(0, 2, 0); @@ -11673,7 +11688,7 @@ x_1284 = lean::alloc_cnstr(1, 1, 0); lean::cnstr_set(x_1284, 0, x_1283); x_1285 = lean::box(0); x_1286 = l_Lean_Elaborator_toPexpr___main___closed__37; -x_1287 = l_Lean_Kvmap_insertCore___main(x_1285, x_1286, x_1284); +x_1287 = l_Lean_KVMap_insertCore___main(x_1285, x_1286, x_1284); x_1288 = lean_expr_mk_mdata(x_1287, x_1278); if (x_20 == 0) { @@ -11715,12 +11730,12 @@ x_1303 = l_Lean_FileMap_toPosition(x_1300, x_1294); x_1304 = lean::cnstr_get(x_1303, 1); lean::inc(x_1304); x_1306 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_1307 = l_Lean_Kvmap_setNat(x_1285, x_1306, x_1304); +x_1307 = l_Lean_KVMap_setNat(x_1285, x_1306, x_1304); x_1308 = lean::cnstr_get(x_1303, 0); lean::inc(x_1308); lean::dec(x_1303); x_1311 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_1312 = l_Lean_Kvmap_setNat(x_1307, x_1311, x_1308); +x_1312 = l_Lean_KVMap_setNat(x_1307, x_1311, x_1308); x_1313 = lean_expr_mk_mdata(x_1312, x_1288); if (lean::is_scalar(x_1282)) { x_1314 = lean::alloc_cnstr(0, 2, 0); @@ -12212,7 +12227,7 @@ return x_1531; } else { -obj* x_1532; obj* x_1535; obj* x_1538; obj* x_1541; obj* x_1542; obj* x_1543; obj* x_1545; obj* x_1546; obj* x_1547; obj* x_1550; obj* x_1551; obj* x_1552; obj* x_1553; obj* x_1554; +obj* x_1532; obj* x_1535; obj* x_1538; obj* x_1541; obj* x_1542; obj* x_1544; obj* x_1545; obj* x_1546; obj* x_1547; obj* x_1550; obj* x_1551; obj* x_1552; obj* x_1553; obj* x_1554; x_1532 = lean::cnstr_get(x_1527, 0); lean::inc(x_1532); lean::dec(x_1527); @@ -12223,16 +12238,16 @@ x_1538 = lean::cnstr_get(x_1535, 2); lean::inc(x_1538); lean::dec(x_1535); x_1541 = l_Lean_FileMap_toPosition(x_1538, x_1532); -x_1542 = lean::box(0); -x_1543 = lean::cnstr_get(x_1541, 1); -lean::inc(x_1543); +x_1542 = lean::cnstr_get(x_1541, 1); +lean::inc(x_1542); +x_1544 = lean::box(0); x_1545 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_1546 = l_Lean_Kvmap_setNat(x_1542, x_1545, x_1543); +x_1546 = l_Lean_KVMap_setNat(x_1544, x_1545, x_1542); x_1547 = lean::cnstr_get(x_1541, 0); lean::inc(x_1547); lean::dec(x_1541); x_1550 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_1551 = l_Lean_Kvmap_setNat(x_1546, x_1550, x_1547); +x_1551 = l_Lean_KVMap_setNat(x_1546, x_1550, x_1547); x_1552 = lean_expr_mk_mdata(x_1551, x_1526); if (lean::is_scalar(x_1519)) { x_1553 = lean::alloc_cnstr(0, 2, 0); @@ -12778,7 +12793,7 @@ return x_1803; } else { -obj* x_1804; obj* x_1807; obj* x_1810; obj* x_1813; obj* x_1814; obj* x_1815; obj* x_1817; obj* x_1818; obj* x_1819; obj* x_1822; obj* x_1823; obj* x_1824; obj* x_1825; obj* x_1826; obj* x_1827; +obj* x_1804; obj* x_1807; obj* x_1810; obj* x_1813; obj* x_1814; obj* x_1816; obj* x_1817; obj* x_1818; obj* x_1819; obj* x_1822; obj* x_1823; obj* x_1824; obj* x_1825; obj* x_1826; obj* x_1827; x_1804 = lean::cnstr_get(x_1798, 0); lean::inc(x_1804); lean::dec(x_1798); @@ -12789,16 +12804,16 @@ x_1810 = lean::cnstr_get(x_1807, 2); lean::inc(x_1810); lean::dec(x_1807); x_1813 = l_Lean_FileMap_toPosition(x_1810, x_1804); -x_1814 = lean::box(0); -x_1815 = lean::cnstr_get(x_1813, 1); -lean::inc(x_1815); +x_1814 = lean::cnstr_get(x_1813, 1); +lean::inc(x_1814); +x_1816 = lean::box(0); x_1817 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_1818 = l_Lean_Kvmap_setNat(x_1814, x_1817, x_1815); +x_1818 = l_Lean_KVMap_setNat(x_1816, x_1817, x_1814); x_1819 = lean::cnstr_get(x_1813, 0); lean::inc(x_1819); lean::dec(x_1813); x_1822 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_1823 = l_Lean_Kvmap_setNat(x_1818, x_1822, x_1819); +x_1823 = l_Lean_KVMap_setNat(x_1818, x_1822, x_1819); x_1824 = l_Lean_Elaborator_toPexpr___main___closed__44; x_1825 = lean_expr_mk_mdata(x_1823, x_1824); x_1826 = lean::alloc_cnstr(0, 2, 0); @@ -12916,7 +12931,7 @@ return x_1869; } else { -obj* x_1870; obj* x_1873; obj* x_1876; obj* x_1879; obj* x_1880; obj* x_1881; obj* x_1883; obj* x_1884; obj* x_1885; obj* x_1888; obj* x_1889; obj* x_1890; obj* x_1891; obj* x_1892; +obj* x_1870; obj* x_1873; obj* x_1876; obj* x_1879; obj* x_1880; obj* x_1882; obj* x_1883; obj* x_1884; obj* x_1885; obj* x_1888; obj* x_1889; obj* x_1890; obj* x_1891; obj* x_1892; x_1870 = lean::cnstr_get(x_1865, 0); lean::inc(x_1870); lean::dec(x_1865); @@ -12927,16 +12942,16 @@ x_1876 = lean::cnstr_get(x_1873, 2); lean::inc(x_1876); lean::dec(x_1873); x_1879 = l_Lean_FileMap_toPosition(x_1876, x_1870); -x_1880 = lean::box(0); -x_1881 = lean::cnstr_get(x_1879, 1); -lean::inc(x_1881); +x_1880 = lean::cnstr_get(x_1879, 1); +lean::inc(x_1880); +x_1882 = lean::box(0); x_1883 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_1884 = l_Lean_Kvmap_setNat(x_1880, x_1883, x_1881); +x_1884 = l_Lean_KVMap_setNat(x_1882, x_1883, x_1880); x_1885 = lean::cnstr_get(x_1879, 0); lean::inc(x_1885); lean::dec(x_1879); x_1888 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_1889 = l_Lean_Kvmap_setNat(x_1884, x_1888, x_1885); +x_1889 = l_Lean_KVMap_setNat(x_1884, x_1888, x_1885); x_1890 = lean_expr_mk_mdata(x_1889, x_1864); if (lean::is_scalar(x_1862)) { x_1891 = lean::alloc_cnstr(0, 2, 0); @@ -13076,7 +13091,7 @@ return x_1937; } else { -obj* x_1938; obj* x_1941; obj* x_1944; obj* x_1947; obj* x_1948; obj* x_1949; obj* x_1951; obj* x_1952; obj* x_1953; obj* x_1956; obj* x_1957; obj* x_1958; obj* x_1959; obj* x_1960; +obj* x_1938; obj* x_1941; obj* x_1944; obj* x_1947; obj* x_1948; obj* x_1950; obj* x_1951; obj* x_1952; obj* x_1953; obj* x_1956; obj* x_1957; obj* x_1958; obj* x_1959; obj* x_1960; x_1938 = lean::cnstr_get(x_1933, 0); lean::inc(x_1938); lean::dec(x_1933); @@ -13087,16 +13102,16 @@ x_1944 = lean::cnstr_get(x_1941, 2); lean::inc(x_1944); lean::dec(x_1941); x_1947 = l_Lean_FileMap_toPosition(x_1944, x_1938); -x_1948 = lean::box(0); -x_1949 = lean::cnstr_get(x_1947, 1); -lean::inc(x_1949); +x_1948 = lean::cnstr_get(x_1947, 1); +lean::inc(x_1948); +x_1950 = lean::box(0); x_1951 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_1952 = l_Lean_Kvmap_setNat(x_1948, x_1951, x_1949); +x_1952 = l_Lean_KVMap_setNat(x_1950, x_1951, x_1948); x_1953 = lean::cnstr_get(x_1947, 0); lean::inc(x_1953); lean::dec(x_1947); x_1956 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_1957 = l_Lean_Kvmap_setNat(x_1952, x_1956, x_1953); +x_1957 = l_Lean_KVMap_setNat(x_1952, x_1956, x_1953); x_1958 = lean_expr_mk_mdata(x_1957, x_1932); if (lean::is_scalar(x_1931)) { x_1959 = lean::alloc_cnstr(0, 2, 0); @@ -13218,7 +13233,7 @@ return x_1991; } else { -obj* x_1992; obj* x_1995; obj* x_1998; obj* x_2001; obj* x_2002; obj* x_2003; obj* x_2005; obj* x_2006; obj* x_2007; obj* x_2010; obj* x_2011; obj* x_2012; obj* x_2013; obj* x_2014; +obj* x_1992; obj* x_1995; obj* x_1998; obj* x_2001; obj* x_2002; obj* x_2004; obj* x_2005; obj* x_2006; obj* x_2007; obj* x_2010; obj* x_2011; obj* x_2012; obj* x_2013; obj* x_2014; x_1992 = lean::cnstr_get(x_1987, 0); lean::inc(x_1992); lean::dec(x_1987); @@ -13229,16 +13244,16 @@ x_1998 = lean::cnstr_get(x_1995, 2); lean::inc(x_1998); lean::dec(x_1995); x_2001 = l_Lean_FileMap_toPosition(x_1998, x_1992); -x_2002 = lean::box(0); -x_2003 = lean::cnstr_get(x_2001, 1); -lean::inc(x_2003); +x_2002 = lean::cnstr_get(x_2001, 1); +lean::inc(x_2002); +x_2004 = lean::box(0); x_2005 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_2006 = l_Lean_Kvmap_setNat(x_2002, x_2005, x_2003); +x_2006 = l_Lean_KVMap_setNat(x_2004, x_2005, x_2002); x_2007 = lean::cnstr_get(x_2001, 0); lean::inc(x_2007); lean::dec(x_2001); x_2010 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_2011 = l_Lean_Kvmap_setNat(x_2006, x_2010, x_2007); +x_2011 = l_Lean_KVMap_setNat(x_2006, x_2010, x_2007); x_2012 = lean_expr_mk_mdata(x_2011, x_1986); if (lean::is_scalar(x_1984)) { x_2013 = lean::alloc_cnstr(0, 2, 0); @@ -13313,7 +13328,7 @@ return x_2033; } else { -obj* x_2034; obj* x_2037; obj* x_2040; obj* x_2043; obj* x_2044; obj* x_2045; obj* x_2047; obj* x_2048; obj* x_2049; obj* x_2052; obj* x_2053; obj* x_2054; obj* x_2055; obj* x_2056; obj* x_2057; +obj* x_2034; obj* x_2037; obj* x_2040; obj* x_2043; obj* x_2044; obj* x_2046; obj* x_2047; obj* x_2048; obj* x_2049; obj* x_2052; obj* x_2053; obj* x_2054; obj* x_2055; obj* x_2056; obj* x_2057; x_2034 = lean::cnstr_get(x_2028, 0); lean::inc(x_2034); lean::dec(x_2028); @@ -13324,16 +13339,16 @@ x_2040 = lean::cnstr_get(x_2037, 2); lean::inc(x_2040); lean::dec(x_2037); x_2043 = l_Lean_FileMap_toPosition(x_2040, x_2034); -x_2044 = lean::box(0); -x_2045 = lean::cnstr_get(x_2043, 1); -lean::inc(x_2045); +x_2044 = lean::cnstr_get(x_2043, 1); +lean::inc(x_2044); +x_2046 = lean::box(0); x_2047 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_2048 = l_Lean_Kvmap_setNat(x_2044, x_2047, x_2045); +x_2048 = l_Lean_KVMap_setNat(x_2046, x_2047, x_2044); x_2049 = lean::cnstr_get(x_2043, 0); lean::inc(x_2049); lean::dec(x_2043); x_2052 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_2053 = l_Lean_Kvmap_setNat(x_2048, x_2052, x_2049); +x_2053 = l_Lean_KVMap_setNat(x_2048, x_2052, x_2049); x_2054 = l_Lean_Elaborator_toPexpr___main___closed__27; x_2055 = lean_expr_mk_mdata(x_2053, x_2054); x_2056 = lean::alloc_cnstr(0, 2, 0); @@ -13380,7 +13395,7 @@ return x_2069; } else { -obj* x_2070; obj* x_2073; obj* x_2076; obj* x_2079; obj* x_2080; obj* x_2081; obj* x_2083; obj* x_2084; obj* x_2085; obj* x_2088; obj* x_2089; obj* x_2090; obj* x_2091; obj* x_2092; obj* x_2093; +obj* x_2070; obj* x_2073; obj* x_2076; obj* x_2079; obj* x_2080; obj* x_2082; obj* x_2083; obj* x_2084; obj* x_2085; obj* x_2088; obj* x_2089; obj* x_2090; obj* x_2091; obj* x_2092; obj* x_2093; x_2070 = lean::cnstr_get(x_2064, 0); lean::inc(x_2070); lean::dec(x_2064); @@ -13391,16 +13406,16 @@ x_2076 = lean::cnstr_get(x_2073, 2); lean::inc(x_2076); lean::dec(x_2073); x_2079 = l_Lean_FileMap_toPosition(x_2076, x_2070); -x_2080 = lean::box(0); -x_2081 = lean::cnstr_get(x_2079, 1); -lean::inc(x_2081); +x_2080 = lean::cnstr_get(x_2079, 1); +lean::inc(x_2080); +x_2082 = lean::box(0); x_2083 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_2084 = l_Lean_Kvmap_setNat(x_2080, x_2083, x_2081); +x_2084 = l_Lean_KVMap_setNat(x_2082, x_2083, x_2080); x_2085 = lean::cnstr_get(x_2079, 0); lean::inc(x_2085); lean::dec(x_2079); x_2088 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_2089 = l_Lean_Kvmap_setNat(x_2084, x_2088, x_2085); +x_2089 = l_Lean_KVMap_setNat(x_2084, x_2088, x_2085); x_2090 = l_Lean_Elaborator_toPexpr___main___closed__46; x_2091 = lean_expr_mk_mdata(x_2089, x_2090); x_2092 = lean::alloc_cnstr(0, 2, 0); @@ -13903,7 +13918,7 @@ return x_2329; } else { -obj* x_2330; obj* x_2333; obj* x_2336; obj* x_2339; obj* x_2340; obj* x_2341; obj* x_2343; obj* x_2344; obj* x_2345; obj* x_2348; obj* x_2349; obj* x_2350; obj* x_2351; obj* x_2352; +obj* x_2330; obj* x_2333; obj* x_2336; obj* x_2339; obj* x_2340; obj* x_2342; obj* x_2343; obj* x_2344; obj* x_2345; obj* x_2348; obj* x_2349; obj* x_2350; obj* x_2351; obj* x_2352; x_2330 = lean::cnstr_get(x_2325, 0); lean::inc(x_2330); lean::dec(x_2325); @@ -13914,16 +13929,16 @@ x_2336 = lean::cnstr_get(x_2333, 2); lean::inc(x_2336); lean::dec(x_2333); x_2339 = l_Lean_FileMap_toPosition(x_2336, x_2330); -x_2340 = lean::box(0); -x_2341 = lean::cnstr_get(x_2339, 1); -lean::inc(x_2341); +x_2340 = lean::cnstr_get(x_2339, 1); +lean::inc(x_2340); +x_2342 = lean::box(0); x_2343 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_2344 = l_Lean_Kvmap_setNat(x_2340, x_2343, x_2341); +x_2344 = l_Lean_KVMap_setNat(x_2342, x_2343, x_2340); x_2345 = lean::cnstr_get(x_2339, 0); lean::inc(x_2345); lean::dec(x_2339); x_2348 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_2349 = l_Lean_Kvmap_setNat(x_2344, x_2348, x_2345); +x_2349 = l_Lean_KVMap_setNat(x_2344, x_2348, x_2345); x_2350 = lean_expr_mk_mdata(x_2349, x_2324); if (lean::is_scalar(x_2323)) { x_2351 = lean::alloc_cnstr(0, 2, 0); @@ -14030,12 +14045,12 @@ x_2398 = l_Lean_FileMap_toPosition(x_2395, x_2389); x_2399 = lean::cnstr_get(x_2398, 1); lean::inc(x_2399); x_2401 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_2402 = l_Lean_Kvmap_setNat(x_2371, x_2401, x_2399); +x_2402 = l_Lean_KVMap_setNat(x_2371, x_2401, x_2399); x_2403 = lean::cnstr_get(x_2398, 0); lean::inc(x_2403); lean::dec(x_2398); x_2406 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_2407 = l_Lean_Kvmap_setNat(x_2402, x_2406, x_2403); +x_2407 = l_Lean_KVMap_setNat(x_2402, x_2406, x_2403); x_2408 = lean_expr_mk_mdata(x_2407, x_2380); x_2409 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_2409, 0, x_2408); @@ -14127,7 +14142,7 @@ lean::inc(x_2445); lean::dec(x_2415); x_2448 = lean::mk_nat_obj(0u); x_2449 = l_List_enumFrom___main___rarg(x_2448, x_2445); -x_2450 = l_Lean_Elaborator_toPexpr___main___closed__49; +x_2450 = l_Lean_Elaborator_toPexpr___main___closed__50; x_2451 = l_List_foldl___main___at_Lean_Elaborator_toPexpr___main___spec__22(x_2450, x_2449); x_2452 = lean_expr_mk_mdata(x_2451, x_2444); x_2453 = l_Lean_Elaborator_toPexpr___main___closed__2; @@ -14174,12 +14189,12 @@ x_2471 = l_Lean_FileMap_toPosition(x_2468, x_2462); x_2472 = lean::cnstr_get(x_2471, 1); lean::inc(x_2472); x_2474 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_2475 = l_Lean_Kvmap_setNat(x_2456, x_2474, x_2472); +x_2475 = l_Lean_KVMap_setNat(x_2456, x_2474, x_2472); x_2476 = lean::cnstr_get(x_2471, 0); lean::inc(x_2476); lean::dec(x_2471); x_2479 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_2480 = l_Lean_Kvmap_setNat(x_2475, x_2479, x_2476); +x_2480 = l_Lean_KVMap_setNat(x_2475, x_2479, x_2476); x_2481 = lean_expr_mk_mdata(x_2480, x_2452); if (lean::is_scalar(x_2441)) { x_2482 = lean::alloc_cnstr(0, 2, 0); @@ -14297,7 +14312,7 @@ return x_2510; } else { -obj* x_2511; obj* x_2514; obj* x_2517; obj* x_2520; obj* x_2521; obj* x_2522; obj* x_2524; obj* x_2525; obj* x_2526; obj* x_2529; obj* x_2530; obj* x_2531; obj* x_2532; obj* x_2533; +obj* x_2511; obj* x_2514; obj* x_2517; obj* x_2520; obj* x_2521; obj* x_2523; obj* x_2524; obj* x_2525; obj* x_2526; obj* x_2529; obj* x_2530; obj* x_2531; obj* x_2532; obj* x_2533; x_2511 = lean::cnstr_get(x_2506, 0); lean::inc(x_2511); lean::dec(x_2506); @@ -14308,16 +14323,16 @@ x_2517 = lean::cnstr_get(x_2514, 2); lean::inc(x_2517); lean::dec(x_2514); x_2520 = l_Lean_FileMap_toPosition(x_2517, x_2511); -x_2521 = lean::box(0); -x_2522 = lean::cnstr_get(x_2520, 1); -lean::inc(x_2522); +x_2521 = lean::cnstr_get(x_2520, 1); +lean::inc(x_2521); +x_2523 = lean::box(0); x_2524 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_2525 = l_Lean_Kvmap_setNat(x_2521, x_2524, x_2522); +x_2525 = l_Lean_KVMap_setNat(x_2523, x_2524, x_2521); x_2526 = lean::cnstr_get(x_2520, 0); lean::inc(x_2526); lean::dec(x_2520); x_2529 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_2530 = l_Lean_Kvmap_setNat(x_2525, x_2529, x_2526); +x_2530 = l_Lean_KVMap_setNat(x_2525, x_2529, x_2526); x_2531 = lean_expr_mk_mdata(x_2530, x_2498); if (lean::is_scalar(x_2502)) { x_2532 = lean::alloc_cnstr(0, 2, 0); @@ -14397,7 +14412,7 @@ return x_2550; } else { -obj* x_2551; obj* x_2554; obj* x_2557; obj* x_2560; obj* x_2561; obj* x_2562; obj* x_2564; obj* x_2565; obj* x_2566; obj* x_2569; obj* x_2570; obj* x_2571; obj* x_2572; obj* x_2573; +obj* x_2551; obj* x_2554; obj* x_2557; obj* x_2560; obj* x_2561; obj* x_2563; obj* x_2564; obj* x_2565; obj* x_2566; obj* x_2569; obj* x_2570; obj* x_2571; obj* x_2572; obj* x_2573; x_2551 = lean::cnstr_get(x_2546, 0); lean::inc(x_2551); lean::dec(x_2546); @@ -14408,16 +14423,16 @@ x_2557 = lean::cnstr_get(x_2554, 2); lean::inc(x_2557); lean::dec(x_2554); x_2560 = l_Lean_FileMap_toPosition(x_2557, x_2551); -x_2561 = lean::box(0); -x_2562 = lean::cnstr_get(x_2560, 1); -lean::inc(x_2562); +x_2561 = lean::cnstr_get(x_2560, 1); +lean::inc(x_2561); +x_2563 = lean::box(0); x_2564 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_2565 = l_Lean_Kvmap_setNat(x_2561, x_2564, x_2562); +x_2565 = l_Lean_KVMap_setNat(x_2563, x_2564, x_2561); x_2566 = lean::cnstr_get(x_2560, 0); lean::inc(x_2566); lean::dec(x_2560); x_2569 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_2570 = l_Lean_Kvmap_setNat(x_2565, x_2569, x_2566); +x_2570 = l_Lean_KVMap_setNat(x_2565, x_2569, x_2566); x_2571 = lean_expr_mk_mdata(x_2570, x_2538); if (lean::is_scalar(x_2542)) { x_2572 = lean::alloc_cnstr(0, 2, 0); @@ -16533,12 +16548,12 @@ x_23 = l_Lean_FileMap_toPosition(x_17, x_21); x_24 = lean::cnstr_get(x_23, 1); lean::inc(x_24); x_26 = l_Lean_Elaborator_toPexpr___main___closed__3; -x_27 = l_Lean_Kvmap_setNat(x_12, x_26, x_24); +x_27 = l_Lean_KVMap_setNat(x_12, x_26, x_24); x_28 = lean::cnstr_get(x_23, 0); lean::inc(x_28); lean::dec(x_23); x_31 = l_Lean_Elaborator_toPexpr___main___closed__4; -x_32 = l_Lean_Kvmap_setNat(x_27, x_31, x_28); +x_32 = l_Lean_KVMap_setNat(x_27, x_31, x_28); x_33 = lean_expr_mk_mdata(x_32, x_14); x_10 = x_33; goto lbl_11; @@ -17469,7 +17484,7 @@ x_1 = lean::box(0); x_2 = lean::mk_string("private"); x_3 = lean_name_mk_string(x_1, x_2); x_4 = 1; -x_5 = l_Lean_Kvmap_setBool(x_0, x_3, x_4); +x_5 = l_Lean_KVMap_setBool(x_0, x_3, x_4); return x_5; } } @@ -17482,7 +17497,7 @@ x_1 = lean::box(0); x_2 = lean::mk_string("protected"); x_3 = lean_name_mk_string(x_1, x_2); x_4 = 1; -x_5 = l_Lean_Kvmap_setBool(x_0, x_3, x_4); +x_5 = l_Lean_KVMap_setBool(x_0, x_3, x_4); return x_5; } } @@ -17617,7 +17632,7 @@ x_45 = lean::cnstr_get(x_42, 1); lean::inc(x_45); lean::dec(x_42); x_48 = l_Lean_Elaborator_declModifiersToPexpr___closed__5; -x_49 = l_Lean_Kvmap_setString(x_4, x_48, x_45); +x_49 = l_Lean_KVMap_setString(x_4, x_48, x_45); if (lean::obj_tag(x_7) == 0) { x_20 = x_49; @@ -17635,7 +17650,7 @@ obj* x_54; uint8 x_55; obj* x_56; lean::dec(x_50); x_54 = l_Lean_Elaborator_declModifiersToPexpr___closed__6; x_55 = 1; -x_56 = l_Lean_Kvmap_setBool(x_49, x_54, x_55); +x_56 = l_Lean_KVMap_setBool(x_49, x_54, x_55); x_20 = x_56; goto lbl_21; } @@ -17645,7 +17660,7 @@ obj* x_58; uint8 x_59; obj* x_60; lean::dec(x_50); x_58 = l_Lean_Elaborator_declModifiersToPexpr___closed__7; x_59 = 1; -x_60 = l_Lean_Kvmap_setBool(x_49, x_58, x_59); +x_60 = l_Lean_KVMap_setBool(x_49, x_58, x_59); x_20 = x_60; goto lbl_21; } @@ -17656,9 +17671,9 @@ lbl_21: { obj* x_61; obj* x_62; obj* x_63; obj* x_64; x_61 = l_Lean_Elaborator_declModifiersToPexpr___closed__1; -x_62 = l_Lean_Kvmap_setBool(x_20, x_61, x_11); +x_62 = l_Lean_KVMap_setBool(x_20, x_61, x_11); x_63 = l_Lean_Elaborator_declModifiersToPexpr___closed__2; -x_64 = l_Lean_Kvmap_setBool(x_62, x_63, x_15); +x_64 = l_Lean_KVMap_setBool(x_62, x_63, x_15); if (lean::obj_tag(x_17) == 0) { obj* x_65; @@ -19242,12 +19257,12 @@ _start: { obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; x_0 = lean::box(0); -x_1 = lean::box(0); -x_2 = lean::mk_string("command"); -x_3 = lean_name_mk_string(x_1, x_2); -x_4 = lean::mk_string("defs"); -x_5 = lean_name_mk_string(x_1, x_4); -x_6 = l_Lean_Kvmap_setName(x_0, x_3, x_5); +x_1 = lean::mk_string("command"); +x_2 = lean_name_mk_string(x_0, x_1); +x_3 = lean::mk_string("defs"); +x_4 = lean_name_mk_string(x_0, x_3); +x_5 = lean::box(0); +x_6 = l_Lean_KVMap_setName(x_5, x_2, x_4); return x_6; } } @@ -22373,12 +22388,12 @@ _start: { obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; x_0 = lean::box(0); -x_1 = lean::box(0); -x_2 = lean::mk_string("command"); -x_3 = lean_name_mk_string(x_1, x_2); -x_4 = lean::mk_string("axiom"); -x_5 = lean_name_mk_string(x_1, x_4); -x_6 = l_Lean_Kvmap_setName(x_0, x_3, x_5); +x_1 = lean::mk_string("command"); +x_2 = lean_name_mk_string(x_0, x_1); +x_3 = lean::mk_string("axiom"); +x_4 = lean_name_mk_string(x_0, x_3); +x_5 = lean::box(0); +x_6 = l_Lean_KVMap_setName(x_5, x_2, x_4); return x_6; } } @@ -22387,12 +22402,12 @@ _start: { obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; x_0 = lean::box(0); -x_1 = lean::box(0); -x_2 = lean::mk_string("command"); -x_3 = lean_name_mk_string(x_1, x_2); -x_4 = lean::mk_string("inductives"); -x_5 = lean_name_mk_string(x_1, x_4); -x_6 = l_Lean_Kvmap_setName(x_0, x_3, x_5); +x_1 = lean::mk_string("command"); +x_2 = lean_name_mk_string(x_0, x_1); +x_3 = lean::mk_string("inductives"); +x_4 = lean_name_mk_string(x_0, x_3); +x_5 = lean::box(0); +x_6 = l_Lean_KVMap_setName(x_5, x_2, x_4); return x_6; } } @@ -22401,12 +22416,12 @@ _start: { obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; x_0 = lean::box(0); -x_1 = lean::box(0); -x_2 = lean::mk_string("command"); -x_3 = lean_name_mk_string(x_1, x_2); -x_4 = lean::mk_string("structure"); -x_5 = lean_name_mk_string(x_1, x_4); -x_6 = l_Lean_Kvmap_setName(x_0, x_3, x_5); +x_1 = lean::mk_string("command"); +x_2 = lean_name_mk_string(x_0, x_1); +x_3 = lean::mk_string("structure"); +x_4 = lean_name_mk_string(x_0, x_3); +x_5 = lean::box(0); +x_6 = l_Lean_KVMap_setName(x_5, x_2, x_4); return x_6; } } @@ -23934,12 +23949,12 @@ _start: { obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; x_0 = lean::box(0); -x_1 = lean::box(0); -x_2 = lean::mk_string("command"); -x_3 = lean_name_mk_string(x_1, x_2); -x_4 = lean::mk_string("variables"); -x_5 = lean_name_mk_string(x_1, x_4); -x_6 = l_Lean_Kvmap_setName(x_0, x_3, x_5); +x_1 = lean::mk_string("command"); +x_2 = lean_name_mk_string(x_0, x_1); +x_3 = lean::mk_string("variables"); +x_4 = lean_name_mk_string(x_0, x_3); +x_5 = lean::box(0); +x_6 = l_Lean_KVMap_setName(x_5, x_2, x_4); return x_6; } } @@ -29482,12 +29497,12 @@ _start: { obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; x_0 = lean::box(0); -x_1 = lean::box(0); -x_2 = lean::mk_string("command"); -x_3 = lean_name_mk_string(x_1, x_2); -x_4 = lean::mk_string("attribute"); -x_5 = lean_name_mk_string(x_1, x_4); -x_6 = l_Lean_Kvmap_setName(x_0, x_3, x_5); +x_1 = lean::mk_string("command"); +x_2 = lean_name_mk_string(x_0, x_1); +x_3 = lean::mk_string("attribute"); +x_4 = lean_name_mk_string(x_0, x_3); +x_5 = lean::box(0); +x_6 = l_Lean_KVMap_setName(x_5, x_2, x_4); return x_6; } } @@ -29593,7 +29608,7 @@ x_52 = l_Option_isSome___main___rarg(x_49); lean::dec(x_49); x_54 = l_Lean_Elaborator_attribute_elaborate___closed__1; x_55 = l_Lean_Elaborator_attribute_elaborate___closed__2; -x_56 = l_Lean_Kvmap_setBool(x_54, x_55, x_52); +x_56 = l_Lean_KVMap_setBool(x_54, x_55, x_52); x_57 = l_Lean_Elaborator_mkEqns___closed__1; x_58 = l_Lean_Expr_mkCapp(x_57, x_44); x_59 = lean_expr_mk_app(x_24, x_58); @@ -29628,12 +29643,12 @@ _start: { obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; x_0 = lean::box(0); -x_1 = lean::box(0); -x_2 = lean::mk_string("command"); -x_3 = lean_name_mk_string(x_1, x_2); -x_4 = lean::mk_string("#check"); -x_5 = lean_name_mk_string(x_1, x_4); -x_6 = l_Lean_Kvmap_setName(x_0, x_3, x_5); +x_1 = lean::mk_string("command"); +x_2 = lean_name_mk_string(x_0, x_1); +x_3 = lean::mk_string("#check"); +x_4 = lean_name_mk_string(x_0, x_3); +x_5 = lean::box(0); +x_6 = l_Lean_KVMap_setName(x_5, x_2, x_4); return x_6; } } @@ -29927,12 +29942,12 @@ _start: { obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; x_0 = lean::box(0); -x_1 = lean::box(0); -x_2 = lean::mk_string("command"); -x_3 = lean_name_mk_string(x_1, x_2); -x_4 = lean::mk_string("initQuot"); -x_5 = lean_name_mk_string(x_1, x_4); -x_6 = l_Lean_Kvmap_setName(x_0, x_3, x_5); +x_1 = lean::mk_string("command"); +x_2 = lean_name_mk_string(x_0, x_1); +x_3 = lean::mk_string("initQuot"); +x_4 = lean_name_mk_string(x_0, x_3); +x_5 = lean::box(0); +x_6 = l_Lean_KVMap_setName(x_5, x_2, x_4); x_7 = l_Lean_Elaborator_dummy; x_8 = lean_expr_mk_mdata(x_6, x_7); return x_8; @@ -30057,7 +30072,7 @@ x_37 = lean::cnstr_get(x_15, 8); lean::inc(x_37); lean::dec(x_15); x_40 = 1; -x_41 = l_Lean_Kvmap_setBool(x_37, x_34, x_40); +x_41 = l_Lean_KVMap_setBool(x_37, x_34, x_40); x_42 = lean::alloc_closure(reinterpret_cast(l_Lean_Elaborator_setOption_elaborate___lambda__1), 2, 1); lean::closure_set(x_42, 0, x_41); x_43 = l_Lean_Elaborator_modifyCurrentScope(x_42, x_1, x_2, x_17); @@ -30077,7 +30092,7 @@ x_51 = lean::cnstr_get(x_15, 8); lean::inc(x_51); lean::dec(x_15); x_54 = 0; -x_55 = l_Lean_Kvmap_setBool(x_51, x_48, x_54); +x_55 = l_Lean_KVMap_setBool(x_51, x_48, x_54); x_56 = lean::alloc_closure(reinterpret_cast(l_Lean_Elaborator_setOption_elaborate___lambda__1), 2, 1); lean::closure_set(x_56, 0, x_55); x_57 = l_Lean_Elaborator_modifyCurrentScope(x_56, x_1, x_2, x_17); @@ -30115,7 +30130,7 @@ obj* x_74; obj* x_77; obj* x_78; obj* x_79; x_74 = lean::cnstr_get(x_70, 0); lean::inc(x_74); lean::dec(x_70); -x_77 = l_Lean_Kvmap_setString(x_64, x_61, x_74); +x_77 = l_Lean_KVMap_setString(x_64, x_61, x_74); x_78 = lean::alloc_closure(reinterpret_cast(l_Lean_Elaborator_setOption_elaborate___lambda__1), 2, 1); lean::closure_set(x_78, 0, x_77); x_79 = l_Lean_Elaborator_modifyCurrentScope(x_78, x_1, x_2, x_17); @@ -30138,7 +30153,7 @@ x_89 = lean::cnstr_get(x_25, 0); lean::inc(x_89); lean::dec(x_25); x_92 = l_Lean_Parser_number_View_toNat___main(x_89); -x_93 = l_Lean_Kvmap_setNat(x_86, x_83, x_92); +x_93 = l_Lean_KVMap_setNat(x_86, x_83, x_92); x_94 = lean::alloc_closure(reinterpret_cast(l_Lean_Elaborator_setOption_elaborate___lambda__1), 2, 1); lean::closure_set(x_94, 0, x_93); x_95 = l_Lean_Elaborator_modifyCurrentScope(x_94, x_1, x_2, x_17); @@ -33367,6 +33382,8 @@ lean::mark_persistent(l_Lean_Elaborator_toPexpr___main___closed__47); lean::mark_persistent(l_Lean_Elaborator_toPexpr___main___closed__48); l_Lean_Elaborator_toPexpr___main___closed__49 = _init_l_Lean_Elaborator_toPexpr___main___closed__49(); lean::mark_persistent(l_Lean_Elaborator_toPexpr___main___closed__49); + l_Lean_Elaborator_toPexpr___main___closed__50 = _init_l_Lean_Elaborator_toPexpr___main___closed__50(); +lean::mark_persistent(l_Lean_Elaborator_toPexpr___main___closed__50); l_Lean_Elaborator_OrderedRBMap_ofList___at_Lean_Elaborator_oldElabCommand___spec__1___closed__1 = _init_l_Lean_Elaborator_OrderedRBMap_ofList___at_Lean_Elaborator_oldElabCommand___spec__1___closed__1(); lean::mark_persistent(l_Lean_Elaborator_OrderedRBMap_ofList___at_Lean_Elaborator_oldElabCommand___spec__1___closed__1); l_Lean_Elaborator_OrderedRBMap_ofList___at_Lean_Elaborator_oldElabCommand___spec__9___closed__1 = _init_l_Lean_Elaborator_OrderedRBMap_ofList___at_Lean_Elaborator_oldElabCommand___spec__9___closed__1(); diff --git a/src/stage0/init/lean/expander.cpp b/src/stage0/init/lean/expander.cpp index 03f010e296..759bf98263 100644 --- a/src/stage0/init/lean/expander.cpp +++ b/src/stage0/init/lean/expander.cpp @@ -8105,7 +8105,7 @@ obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; x_0 = lean::box(0); x_1 = lean::mk_string("Unit"); x_2 = lean_name_mk_string(x_0, x_1); -x_3 = lean::mk_string("star"); +x_3 = lean::mk_string("unit"); x_4 = lean_name_mk_string(x_2, x_3); x_5 = l_Lean_Expander_globId(x_4); x_6 = lean::alloc_cnstr(1, 1, 0); diff --git a/src/stage0/init/lean/expr.cpp b/src/stage0/init/lean/expr.cpp index 29696dca2a..9d6e241204 100644 --- a/src/stage0/init/lean/expr.cpp +++ b/src/stage0/init/lean/expr.cpp @@ -17,6 +17,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; obj* l_Lean_getAppFn___main(obj*); obj* l_Lean_Expr_hash___boxed(obj*); obj* l_Lean_mkBinApp(obj*, obj*, obj*); +obj* l_Lean_MData_empty; obj* l_Lean_getAppFn(obj*); obj* l_Lean_exprIsInhabited; extern "C" usize lean_expr_hash(obj*); @@ -27,6 +28,7 @@ obj* l_Lean_Expr_mkCapp(obj*, obj*); obj* l_Lean_mkDecIsFalse___closed__1; extern "C" obj* lean_expr_mk_const(obj*, obj*); obj* l_List_foldl___main___at_Lean_Expr_mkApp___spec__1(obj*, obj*); +obj* l_Lean_MData_HasEmptyc; obj* l_Lean_Expr_dbgToString___boxed(obj*); obj* l_Lean_mkDecIsTrue___closed__1; obj* l_Lean_mkDecIsFalse(obj*, obj*); @@ -34,6 +36,22 @@ extern "C" obj* lean_name_mk_string(obj*, obj*); obj* l_Lean_getAppFn___boxed(obj*); obj* l_Lean_mkDecIsTrue(obj*, obj*); obj* l_Lean_Expr_mkApp(obj*, obj*); +obj* _init_l_Lean_MData_empty() { +_start: +{ +obj* x_0; +x_0 = lean::box(0); +return x_0; +} +} +obj* _init_l_Lean_MData_HasEmptyc() { +_start: +{ +obj* x_0; +x_0 = lean::box(0); +return x_0; +} +} obj* _init_l_Lean_exprIsInhabited() { _start: { @@ -213,6 +231,10 @@ if (io_result_is_error(w)) return w; w = initialize_init_lean_level(w); if (io_result_is_error(w)) return w; w = initialize_init_lean_kvmap(w); + l_Lean_MData_empty = _init_l_Lean_MData_empty(); +lean::mark_persistent(l_Lean_MData_empty); + l_Lean_MData_HasEmptyc = _init_l_Lean_MData_HasEmptyc(); +lean::mark_persistent(l_Lean_MData_HasEmptyc); l_Lean_exprIsInhabited = _init_l_Lean_exprIsInhabited(); lean::mark_persistent(l_Lean_exprIsInhabited); l_Lean_mkDecIsTrue___closed__1 = _init_l_Lean_mkDecIsTrue___closed__1(); diff --git a/src/stage0/init/lean/frontend.cpp b/src/stage0/init/lean/frontend.cpp index 87b435544a..4ec502dfdc 100644 --- a/src/stage0/init/lean/frontend.cpp +++ b/src/stage0/init/lean/frontend.cpp @@ -17,6 +17,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; obj* l_IO_Prim_iterate___at_Lean_runFrontend___spec__6___lambda__1(obj*, obj*, obj*); obj* l_IO_Prim_iterate___at_Lean_runFrontend___spec__6___lambda__3___boxed(obj*, obj*, obj*, obj*); obj* l_IO_Prim_iterate___at_Lean_runFrontend___spec__6___lambda__1___boxed(obj*, obj*, obj*); +obj* l_Lean_KVMap_setBool(obj*, obj*, uint8); extern obj* l_Lean_Parser_Term_builtinTrailingParsers_Lean_Parser_HasTokens; extern obj* l_Lean_Parser_Term_builtinLeadingParsers; obj* l_Lean_Elaborator_processCommand(obj*, obj*, obj*); @@ -24,7 +25,6 @@ obj* l_Lean_mkConfig(obj*, obj*); obj* l_Lean_processFile___lambda__1___closed__7; obj* l_IO_Prim_iterate___at_Lean_runFrontend___spec__6___lambda__4___closed__2; obj* l_Lean_processFile___lambda__1___closed__1; -extern obj* l_Lean_Options_mk; obj* l_Lean_runFrontend___closed__1; extern obj* l_Lean_Parser_command_builtinCommandParsers; obj* l_IO_Prim_iterate___at_Lean_runFrontend___spec__6___lambda__4(obj*, obj*, uint8, obj*, obj*, obj*, obj*); @@ -34,6 +34,7 @@ obj* l_Lean_processFile___lambda__1___closed__4; obj* l_ioOfExcept___at_Lean_runFrontend___spec__1(obj*, obj*); obj* l_Lean_Parser_mkTokenTrie(obj*); obj* l_List_mmap_x_27___main___at_Lean_runFrontend___spec__4(obj*, obj*, obj*); +extern obj* l_Lean_Options_empty; extern obj* l_Lean_Parser_Module_header_Parser_Lean_Parser_HasTokens; extern obj* l_Lean_Elaborator_notation_elaborate___closed__1; obj* l_IO_Prim_iterate___at_Lean_runFrontend___spec__6___lambda__4___closed__1; @@ -44,7 +45,6 @@ obj* l_Lean_processFile___closed__1; namespace lean { obj* string_append(obj*, obj*); } -obj* l_Lean_Kvmap_setBool(obj*, obj*, uint8); obj* l_IO_Prim_iterate___at_Lean_runFrontend___spec__6(obj*, uint8, obj*, obj*, obj*, obj*, obj*); extern obj* l_Lean_Expander_builtinTransformers; obj* l_Lean_Elaborator_mkState(obj*, obj*, obj*); @@ -1565,9 +1565,9 @@ x_1 = lean::mk_string("Trace"); x_2 = lean_name_mk_string(x_0, x_1); x_3 = lean::mk_string("asMessages"); x_4 = lean_name_mk_string(x_2, x_3); -x_5 = l_Lean_Options_mk; +x_5 = l_Lean_Options_empty; x_6 = 1; -x_7 = l_Lean_Kvmap_setBool(x_5, x_4, x_6); +x_7 = l_Lean_KVMap_setBool(x_5, x_4, x_6); return x_7; } } diff --git a/src/stage0/init/lean/kvmap.cpp b/src/stage0/init/lean/kvmap.cpp index fa6ce637d6..3649e3fc98 100644 --- a/src/stage0/init/lean/kvmap.cpp +++ b/src/stage0/init/lean/kvmap.cpp @@ -1,6 +1,6 @@ // Lean compiler output // Module: init.lean.kvmap -// Imports: init.lean.name init.data.option.basic +// Imports: init.lean.name init.data.option.basic init.data.int.default #include "runtime/object.h" #include "runtime/apply.h" typedef lean::object obj; typedef lean::usize usize; @@ -14,53 +14,56 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #pragma GCC diagnostic ignored "-Wunused-label" #pragma GCC diagnostic ignored "-Wunused-but-set-variable" #endif -obj* l_Lean_Kvmap_findCore___main___boxed(obj*, obj*); +obj* l_Lean_KVMap_subset___main___boxed(obj*, obj*); extern "C" uint8 lean_name_dec_eq(obj*, obj*); +obj* l_Lean_KVMap_getNat(obj*, obj*); +obj* l_Lean_KVMap_getName(obj*, obj*); +obj* l_Lean_KVMap_setBool(obj*, obj*, uint8); uint8 l_Lean_DataValue_beq(obj*, obj*); -obj* l_Lean_Kvmap_find___main___boxed(obj*, obj*); +obj* l_Lean_KVMap_subset___boxed(obj*, obj*); +obj* l_Lean_KVMap_getInt(obj*, obj*); uint8 l_Option_isSome___main___rarg(obj*); -obj* l_Lean_Kvmap_subset___main___boxed(obj*, obj*); -uint8 l_Lean_Kvmap_subset(obj*, obj*); -uint8 l_Lean_Kvmap_contains(obj*, obj*); +obj* l_Lean_KVMap_getString(obj*, obj*); obj* l_Lean_DataValue_beq___main___boxed(obj*, obj*); -obj* l_Lean_Kvmap_findCore___boxed(obj*, obj*); -uint8 l_Lean_Kvmap_subset___main(obj*, obj*); -uint8 l_Lean_Kvmap_eqv(obj*, obj*); -obj* l_Lean_Kvmap_find___boxed(obj*, obj*); -obj* l_Lean_Kvmap_getBool(obj*, obj*); -obj* l_Lean_Kvmap_setString(obj*, obj*, obj*); -obj* l_Lean_Kvmap_HasBeq; -obj* l_Lean_Kvmap_find(obj*, obj*); -obj* l_Lean_Kvmap_subset___boxed(obj*, obj*); +obj* l_Lean_KVMap_findCore___main(obj*, obj*); +obj* l_Lean_KVMap_findCore(obj*, obj*); +uint8 l_Lean_KVMap_subset___main(obj*, obj*); +obj* l_Lean_KVMap_findCore___boxed(obj*, obj*); +obj* l_Lean_KVMap_setNat(obj*, obj*, obj*); +obj* l_Lean_KVMap_find(obj*, obj*); +obj* l_Lean_KVMap_contains___boxed(obj*, obj*); +obj* l_Lean_KVMap_HasBeq; +obj* l_Lean_KVMap_getBool(obj*, obj*); +uint8 l_Lean_KVMap_contains(obj*, obj*); +uint8 l_Lean_KVMap_subset(obj*, obj*); +obj* l_Lean_KVMap_setInt(obj*, obj*, obj*); +obj* l_Lean_KVMap_insert(obj*, obj*, obj*); obj* l_Lean_DataValue_HasBeq; -obj* l_Lean_Kvmap_setBool(obj*, obj*, uint8); +obj* l_Lean_KVMap_insert___main(obj*, obj*, obj*); obj* l_Lean_DataValue_beq___boxed(obj*, obj*); -obj* l_Lean_Kvmap_getName___boxed(obj*, obj*); -obj* l_Lean_Kvmap_getName(obj*, obj*); +obj* l_Lean_KVMap_setName(obj*, obj*, obj*); +obj* l_Lean_KVMap_setBool___boxed(obj*, obj*, obj*); namespace lean { uint8 nat_dec_eq(obj*, obj*); } -obj* l_Lean_Kvmap_setNat(obj*, obj*, obj*); -obj* l_Lean_Kvmap_setName(obj*, obj*, obj*); -obj* l_Lean_Kvmap_getNat(obj*, obj*); +obj* l_Lean_KVMap_getInt___boxed(obj*, obj*); +uint8 l_Lean_KVMap_eqv(obj*, obj*); +obj* l_Lean_KVMap_find___boxed(obj*, obj*); namespace lean { uint8 string_dec_eq(obj*, obj*); } -obj* l_Lean_Kvmap_findCore(obj*, obj*); -obj* l_Lean_Kvmap_getString___boxed(obj*, obj*); -obj* l_Lean_Kvmap_getString(obj*, obj*); -obj* l_Lean_Kvmap_insertCore___main(obj*, obj*, obj*); -obj* l_Lean_Kvmap_find___main(obj*, obj*); -obj* l_Lean_Kvmap_setBool___boxed(obj*, obj*, obj*); -obj* l_Lean_Kvmap_insertCore(obj*, obj*, obj*); -obj* l_Lean_Kvmap_contains___boxed(obj*, obj*); -obj* l_Lean_Kvmap_findCore___main(obj*, obj*); -obj* l_Lean_Kvmap_getNat___boxed(obj*, obj*); -obj* l_Lean_Kvmap_eqv___boxed(obj*, obj*); -obj* l_Lean_Kvmap_insert___main(obj*, obj*, obj*); +obj* l_Lean_KVMap_find___main(obj*, obj*); +obj* l_Lean_KVMap_eqv___boxed(obj*, obj*); +obj* l_Lean_KVMap_find___main___boxed(obj*, obj*); +obj* l_Lean_KVMap_findCore___main___boxed(obj*, obj*); +obj* l_Lean_KVMap_setString(obj*, obj*, obj*); +obj* l_Lean_KVMap_insertCore___main(obj*, obj*, obj*); +obj* l_Lean_KVMap_getName___boxed(obj*, obj*); +obj* l_Lean_KVMap_getBool___boxed(obj*, obj*); +obj* l_Lean_KVMap_getString___boxed(obj*, obj*); +obj* l_Lean_KVMap_insertCore(obj*, obj*, obj*); +obj* l_Lean_KVMap_getNat___boxed(obj*, obj*); uint8 l_Lean_DataValue_beq___main(obj*, obj*); -obj* l_Lean_Kvmap_getBool___boxed(obj*, obj*); -obj* l_Lean_Kvmap_insert(obj*, obj*, obj*); uint8 l_Lean_DataValue_beq___main(obj* x_0, obj* x_1) { _start: { @@ -219,7 +222,7 @@ x_0 = lean::alloc_closure(reinterpret_cast(l_Lean_DataValue_beq___boxed), return x_0; } } -obj* l_Lean_Kvmap_findCore___main(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_findCore___main(obj* x_0, obj* x_1) { _start: { if (lean::obj_tag(x_0) == 0) @@ -260,67 +263,67 @@ return x_18; } } } -obj* l_Lean_Kvmap_findCore___main___boxed(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_findCore___main___boxed(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_Lean_Kvmap_findCore___main(x_0, x_1); +x_2 = l_Lean_KVMap_findCore___main(x_0, x_1); lean::dec(x_1); return x_2; } } -obj* l_Lean_Kvmap_findCore(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_findCore(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_Lean_Kvmap_findCore___main(x_0, x_1); +x_2 = l_Lean_KVMap_findCore___main(x_0, x_1); return x_2; } } -obj* l_Lean_Kvmap_findCore___boxed(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_findCore___boxed(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_Lean_Kvmap_findCore(x_0, x_1); +x_2 = l_Lean_KVMap_findCore(x_0, x_1); lean::dec(x_1); return x_2; } } -obj* l_Lean_Kvmap_find___main(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_find___main(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_Lean_Kvmap_findCore___main(x_0, x_1); +x_2 = l_Lean_KVMap_findCore___main(x_0, x_1); return x_2; } } -obj* l_Lean_Kvmap_find___main___boxed(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_find___main___boxed(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_Lean_Kvmap_find___main(x_0, x_1); +x_2 = l_Lean_KVMap_find___main(x_0, x_1); lean::dec(x_1); return x_2; } } -obj* l_Lean_Kvmap_find(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_find(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_Lean_Kvmap_findCore___main(x_0, x_1); +x_2 = l_Lean_KVMap_findCore___main(x_0, x_1); return x_2; } } -obj* l_Lean_Kvmap_find___boxed(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_find___boxed(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_Lean_Kvmap_find(x_0, x_1); +x_2 = l_Lean_KVMap_find(x_0, x_1); lean::dec(x_1); return x_2; } } -obj* l_Lean_Kvmap_insertCore___main(obj* x_0, obj* x_1, obj* x_2) { +obj* l_Lean_KVMap_insertCore___main(obj* x_0, obj* x_1, obj* x_2) { _start: { if (lean::obj_tag(x_0) == 0) @@ -356,7 +359,7 @@ if (x_12 == 0) { obj* x_14; obj* x_15; lean::dec(x_10); -x_14 = l_Lean_Kvmap_insertCore___main(x_7, x_1, x_2); +x_14 = l_Lean_KVMap_insertCore___main(x_7, x_1, x_2); if (lean::is_scalar(x_9)) { x_15 = lean::alloc_cnstr(1, 2, 0); } else { @@ -397,55 +400,55 @@ return x_19; } } } -obj* l_Lean_Kvmap_insertCore(obj* x_0, obj* x_1, obj* x_2) { +obj* l_Lean_KVMap_insertCore(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; -x_3 = l_Lean_Kvmap_insertCore___main(x_0, x_1, x_2); +x_3 = l_Lean_KVMap_insertCore___main(x_0, x_1, x_2); return x_3; } } -obj* l_Lean_Kvmap_insert___main(obj* x_0, obj* x_1, obj* x_2) { +obj* l_Lean_KVMap_insert___main(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; -x_3 = l_Lean_Kvmap_insertCore___main(x_0, x_1, x_2); +x_3 = l_Lean_KVMap_insertCore___main(x_0, x_1, x_2); return x_3; } } -obj* l_Lean_Kvmap_insert(obj* x_0, obj* x_1, obj* x_2) { +obj* l_Lean_KVMap_insert(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; -x_3 = l_Lean_Kvmap_insertCore___main(x_0, x_1, x_2); +x_3 = l_Lean_KVMap_insertCore___main(x_0, x_1, x_2); return x_3; } } -uint8 l_Lean_Kvmap_contains(obj* x_0, obj* x_1) { +uint8 l_Lean_KVMap_contains(obj* x_0, obj* x_1) { _start: { obj* x_2; uint8 x_3; -x_2 = l_Lean_Kvmap_findCore___main(x_0, x_1); +x_2 = l_Lean_KVMap_findCore___main(x_0, x_1); x_3 = l_Option_isSome___main___rarg(x_2); lean::dec(x_2); return x_3; } } -obj* l_Lean_Kvmap_contains___boxed(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_contains___boxed(obj* x_0, obj* x_1) { _start: { uint8 x_2; obj* x_3; -x_2 = l_Lean_Kvmap_contains(x_0, x_1); +x_2 = l_Lean_KVMap_contains(x_0, x_1); x_3 = lean::box(x_2); lean::dec(x_1); return x_3; } } -obj* l_Lean_Kvmap_getString(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_getString(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_Lean_Kvmap_findCore___main(x_0, x_1); +x_2 = l_Lean_KVMap_findCore___main(x_0, x_1); if (lean::obj_tag(x_2) == 0) { obj* x_3; @@ -491,20 +494,20 @@ return x_13; } } } -obj* l_Lean_Kvmap_getString___boxed(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_getString___boxed(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_Lean_Kvmap_getString(x_0, x_1); +x_2 = l_Lean_KVMap_getString(x_0, x_1); lean::dec(x_1); return x_2; } } -obj* l_Lean_Kvmap_getNat(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_getNat(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_Lean_Kvmap_findCore___main(x_0, x_1); +x_2 = l_Lean_KVMap_findCore___main(x_0, x_1); if (lean::obj_tag(x_2) == 0) { obj* x_3; @@ -550,20 +553,79 @@ return x_13; } } } -obj* l_Lean_Kvmap_getNat___boxed(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_getNat___boxed(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_Lean_Kvmap_getNat(x_0, x_1); +x_2 = l_Lean_KVMap_getNat(x_0, x_1); lean::dec(x_1); return x_2; } } -obj* l_Lean_Kvmap_getBool(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_getInt(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_Lean_Kvmap_findCore___main(x_0, x_1); +x_2 = l_Lean_KVMap_findCore___main(x_0, x_1); +if (lean::obj_tag(x_2) == 0) +{ +obj* x_3; +x_3 = lean::box(0); +return x_3; +} +else +{ +obj* x_4; obj* x_6; +x_4 = lean::cnstr_get(x_2, 0); +if (lean::is_exclusive(x_2)) { + lean::cnstr_set(x_2, 0, lean::box(0)); + x_6 = x_2; +} else { + lean::inc(x_4); + lean::dec(x_2); + x_6 = lean::box(0); +} +switch (lean::obj_tag(x_4)) { +case 4: +{ +obj* x_7; obj* x_10; +x_7 = lean::cnstr_get(x_4, 0); +lean::inc(x_7); +lean::dec(x_4); +if (lean::is_scalar(x_6)) { + x_10 = lean::alloc_cnstr(1, 1, 0); +} else { + x_10 = x_6; +} +lean::cnstr_set(x_10, 0, x_7); +return x_10; +} +default: +{ +obj* x_13; +lean::dec(x_6); +lean::dec(x_4); +x_13 = lean::box(0); +return x_13; +} +} +} +} +} +obj* l_Lean_KVMap_getInt___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = l_Lean_KVMap_getInt(x_0, x_1); +lean::dec(x_1); +return x_2; +} +} +obj* l_Lean_KVMap_getBool(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = l_Lean_KVMap_findCore___main(x_0, x_1); if (lean::obj_tag(x_2) == 0) { obj* x_3; @@ -609,20 +671,20 @@ return x_13; } } } -obj* l_Lean_Kvmap_getBool___boxed(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_getBool___boxed(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_Lean_Kvmap_getBool(x_0, x_1); +x_2 = l_Lean_KVMap_getBool(x_0, x_1); lean::dec(x_1); return x_2; } } -obj* l_Lean_Kvmap_getName(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_getName(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_Lean_Kvmap_findCore___main(x_0, x_1); +x_2 = l_Lean_KVMap_findCore___main(x_0, x_1); if (lean::obj_tag(x_2) == 0) { obj* x_3; @@ -668,66 +730,76 @@ return x_13; } } } -obj* l_Lean_Kvmap_getName___boxed(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_getName___boxed(obj* x_0, obj* x_1) { _start: { obj* x_2; -x_2 = l_Lean_Kvmap_getName(x_0, x_1); +x_2 = l_Lean_KVMap_getName(x_0, x_1); lean::dec(x_1); return x_2; } } -obj* l_Lean_Kvmap_setString(obj* x_0, obj* x_1, obj* x_2) { +obj* l_Lean_KVMap_setString(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; obj* x_4; x_3 = lean::alloc_cnstr(0, 1, 0); lean::cnstr_set(x_3, 0, x_2); -x_4 = l_Lean_Kvmap_insertCore___main(x_0, x_1, x_3); +x_4 = l_Lean_KVMap_insertCore___main(x_0, x_1, x_3); return x_4; } } -obj* l_Lean_Kvmap_setNat(obj* x_0, obj* x_1, obj* x_2) { +obj* l_Lean_KVMap_setNat(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; obj* x_4; x_3 = lean::alloc_cnstr(1, 1, 0); lean::cnstr_set(x_3, 0, x_2); -x_4 = l_Lean_Kvmap_insertCore___main(x_0, x_1, x_3); +x_4 = l_Lean_KVMap_insertCore___main(x_0, x_1, x_3); return x_4; } } -obj* l_Lean_Kvmap_setBool(obj* x_0, obj* x_1, uint8 x_2) { +obj* l_Lean_KVMap_setInt(obj* x_0, obj* x_1, obj* x_2) { +_start: +{ +obj* x_3; obj* x_4; +x_3 = lean::alloc_cnstr(4, 1, 0); +lean::cnstr_set(x_3, 0, x_2); +x_4 = l_Lean_KVMap_insertCore___main(x_0, x_1, x_3); +return x_4; +} +} +obj* l_Lean_KVMap_setBool(obj* x_0, obj* x_1, uint8 x_2) { _start: { obj* x_3; obj* x_4; obj* x_5; x_3 = lean::alloc_cnstr(2, 0, 1); lean::cnstr_set_scalar(x_3, 0, x_2); x_4 = x_3; -x_5 = l_Lean_Kvmap_insertCore___main(x_0, x_1, x_4); +x_5 = l_Lean_KVMap_insertCore___main(x_0, x_1, x_4); return x_5; } } -obj* l_Lean_Kvmap_setBool___boxed(obj* x_0, obj* x_1, obj* x_2) { +obj* l_Lean_KVMap_setBool___boxed(obj* x_0, obj* x_1, obj* x_2) { _start: { uint8 x_3; obj* x_4; x_3 = lean::unbox(x_2); -x_4 = l_Lean_Kvmap_setBool(x_0, x_1, x_3); +x_4 = l_Lean_KVMap_setBool(x_0, x_1, x_3); return x_4; } } -obj* l_Lean_Kvmap_setName(obj* x_0, obj* x_1, obj* x_2) { +obj* l_Lean_KVMap_setName(obj* x_0, obj* x_1, obj* x_2) { _start: { obj* x_3; obj* x_4; x_3 = lean::alloc_cnstr(3, 1, 0); lean::cnstr_set(x_3, 0, x_2); -x_4 = l_Lean_Kvmap_insertCore___main(x_0, x_1, x_3); +x_4 = l_Lean_KVMap_insertCore___main(x_0, x_1, x_3); return x_4; } } -uint8 l_Lean_Kvmap_subset___main(obj* x_0, obj* x_1) { +uint8 l_Lean_KVMap_subset___main(obj* x_0, obj* x_1) { _start: { if (lean::obj_tag(x_0) == 0) @@ -745,7 +817,7 @@ x_5 = lean::cnstr_get(x_0, 1); x_6 = lean::cnstr_get(x_4, 0); x_7 = lean::cnstr_get(x_4, 1); lean::inc(x_1); -x_9 = l_Lean_Kvmap_findCore___main(x_1, x_6); +x_9 = l_Lean_KVMap_findCore___main(x_1, x_6); if (lean::obj_tag(x_9) == 0) { uint8 x_11; @@ -775,40 +847,40 @@ goto _start; } } } -obj* l_Lean_Kvmap_subset___main___boxed(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_subset___main___boxed(obj* x_0, obj* x_1) { _start: { uint8 x_2; obj* x_3; -x_2 = l_Lean_Kvmap_subset___main(x_0, x_1); +x_2 = l_Lean_KVMap_subset___main(x_0, x_1); x_3 = lean::box(x_2); lean::dec(x_0); return x_3; } } -uint8 l_Lean_Kvmap_subset(obj* x_0, obj* x_1) { +uint8 l_Lean_KVMap_subset(obj* x_0, obj* x_1) { _start: { uint8 x_2; -x_2 = l_Lean_Kvmap_subset___main(x_0, x_1); +x_2 = l_Lean_KVMap_subset___main(x_0, x_1); return x_2; } } -obj* l_Lean_Kvmap_subset___boxed(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_subset___boxed(obj* x_0, obj* x_1) { _start: { uint8 x_2; obj* x_3; -x_2 = l_Lean_Kvmap_subset(x_0, x_1); +x_2 = l_Lean_KVMap_subset(x_0, x_1); x_3 = lean::box(x_2); lean::dec(x_0); return x_3; } } -uint8 l_Lean_Kvmap_eqv(obj* x_0, obj* x_1) { +uint8 l_Lean_KVMap_eqv(obj* x_0, obj* x_1) { _start: { uint8 x_3; lean::inc(x_1); -x_3 = l_Lean_Kvmap_subset___main(x_0, x_1); +x_3 = l_Lean_KVMap_subset___main(x_0, x_1); if (x_3 == 0) { lean::dec(x_1); @@ -818,31 +890,32 @@ return x_3; else { uint8 x_6; -x_6 = l_Lean_Kvmap_subset___main(x_1, x_0); +x_6 = l_Lean_KVMap_subset___main(x_1, x_0); lean::dec(x_1); return x_6; } } } -obj* l_Lean_Kvmap_eqv___boxed(obj* x_0, obj* x_1) { +obj* l_Lean_KVMap_eqv___boxed(obj* x_0, obj* x_1) { _start: { uint8 x_2; obj* x_3; -x_2 = l_Lean_Kvmap_eqv(x_0, x_1); +x_2 = l_Lean_KVMap_eqv(x_0, x_1); x_3 = lean::box(x_2); return x_3; } } -obj* _init_l_Lean_Kvmap_HasBeq() { +obj* _init_l_Lean_KVMap_HasBeq() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(l_Lean_Kvmap_eqv___boxed), 2, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_Lean_KVMap_eqv___boxed), 2, 0); return x_0; } } obj* initialize_init_lean_name(obj*); obj* initialize_init_data_option_basic(obj*); +obj* initialize_init_data_int_default(obj*); static bool _G_initialized = false; obj* initialize_init_lean_kvmap(obj* w) { if (_G_initialized) return w; @@ -851,9 +924,11 @@ if (io_result_is_error(w)) return w; w = initialize_init_lean_name(w); if (io_result_is_error(w)) return w; w = initialize_init_data_option_basic(w); +if (io_result_is_error(w)) return w; +w = initialize_init_data_int_default(w); l_Lean_DataValue_HasBeq = _init_l_Lean_DataValue_HasBeq(); lean::mark_persistent(l_Lean_DataValue_HasBeq); - l_Lean_Kvmap_HasBeq = _init_l_Lean_Kvmap_HasBeq(); -lean::mark_persistent(l_Lean_Kvmap_HasBeq); + l_Lean_KVMap_HasBeq = _init_l_Lean_KVMap_HasBeq(); +lean::mark_persistent(l_Lean_KVMap_HasBeq); return w; } diff --git a/src/stage0/init/lean/name.cpp b/src/stage0/init/lean/name.cpp index 8d23ed5123..f1d96414cc 100644 --- a/src/stage0/init/lean/name.cpp +++ b/src/stage0/init/lean/name.cpp @@ -40,6 +40,7 @@ obj* l_Lean_Name_replacePrefix___boxed(obj*, obj*, obj*); obj* l_RBMap_insert___main___at_Lean_NameMap_insert___spec__1___boxed(obj*); obj* l_Lean_NameMap_contains___boxed(obj*); obj* l_RBNode_ins___main___at_Lean_NameMap_insert___spec__3___boxed(obj*); +obj* l_Lean_NameMap_HasEmptyc(obj*); obj* l_Lean_Name_components(obj*); obj* l_List_reverse___rarg(obj*); obj* l_RBNode_ins___main___at_Lean_NameMap_insert___spec__3___rarg___boxed(obj*, obj*, obj*, obj*); @@ -125,6 +126,7 @@ obj* l_RBMap_find___main___at_Lean_NameMap_find___spec__1___rarg___boxed(obj*, o obj* l_Lean_Name_replacePrefix___main___boxed(obj*, obj*, obj*); obj* l_Lean_Name_HasAppend; obj* l_Lean_NameSet_insert(obj*, obj*); +obj* l_Lean_NameMap_HasEmptyc___boxed(obj*); obj* l_RBMap_insert___main___at_Lean_NameSet_insert___spec__1(obj*, obj*, obj*); obj* l_RBMap_find___main___at_Lean_NameMap_contains___spec__1___rarg(obj*, obj*); obj* l_Lean_NameMap_contains___rarg___boxed(obj*, obj*); @@ -135,6 +137,7 @@ obj* l_Lean_mkNumName(obj*, obj*); obj* l_Lean_Name_toString(obj*); obj* l_RBNode_insert___at_Lean_NameSet_insert___spec__2(obj*, obj*, obj*, obj*); obj* l_RBNode_ins___main___at_Lean_NameMap_insert___spec__3___rarg(obj*, obj*, obj*, obj*); +obj* l_Lean_NameSet_HasEmptyc; obj* l_Lean_NameMap_find___rarg___boxed(obj*, obj*); obj* _init_l_Lean_Inhabited() { _start: @@ -905,6 +908,23 @@ lean::dec(x_0); return x_1; } } +obj* l_Lean_NameMap_HasEmptyc(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::box(0); +return x_1; +} +} +obj* l_Lean_NameMap_HasEmptyc___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = l_Lean_NameMap_HasEmptyc(x_0); +lean::dec(x_0); +return x_1; +} +} obj* l_RBNode_ins___main___at_Lean_NameMap_insert___spec__3___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { _start: { @@ -1732,6 +1752,14 @@ x_0 = lean::box(0); return x_0; } } +obj* _init_l_Lean_NameSet_HasEmptyc() { +_start: +{ +obj* x_0; +x_0 = lean::box(0); +return x_0; +} +} obj* l_RBNode_ins___main___at_Lean_NameSet_insert___spec__3(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { _start: { @@ -2345,5 +2373,7 @@ lean::mark_persistent(l_Lean_Name_toString___closed__1); lean::mark_persistent(l_Lean_Name_HasToString); l_Lean_mkNameSet = _init_l_Lean_mkNameSet(); lean::mark_persistent(l_Lean_mkNameSet); + l_Lean_NameSet_HasEmptyc = _init_l_Lean_NameSet_HasEmptyc(); +lean::mark_persistent(l_Lean_NameSet_HasEmptyc); return w; } diff --git a/src/stage0/init/lean/options.cpp b/src/stage0/init/lean/options.cpp index b8ecd6ee3d..4c0e90fa65 100644 --- a/src/stage0/init/lean/options.cpp +++ b/src/stage0/init/lean/options.cpp @@ -1,6 +1,6 @@ // Lean compiler output // Module: init.lean.options -// Imports: init.lean.kvmap +// Imports: init.lean.kvmap init.io init.control.combinators init.data.tostring #include "runtime/object.h" #include "runtime/apply.h" typedef lean::object obj; typedef lean::usize usize; @@ -14,8 +14,23 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #pragma GCC diagnostic ignored "-Wunused-label" #pragma GCC diagnostic ignored "-Wunused-but-set-variable" #endif -obj* l_Lean_Options_mk; -obj* _init_l_Lean_Options_mk() { +obj* l___private_init_lean_options_1__initOptionDeclsRef(obj*); +obj* l_RBMap_insert___main___at_Lean_NameMap_insert___spec__1___rarg(obj*, obj*, obj*); +obj* l_Lean_Options_HasEmptyc; +obj* l_Lean_Name_toStringWithSep___main(obj*, obj*); +obj* l_Lean_Options_empty; +obj* l_Lean_registerOption___closed__1; +namespace lean { +obj* string_append(obj*, obj*); +} +obj* l_Lean_registerOption(obj*, obj*, obj*); +uint8 l_Lean_NameMap_contains___rarg(obj*, obj*); +obj* l___private_init_lean_options_2__optionDeclsRef; +obj* l_Lean_getOptionDecls(obj*); +extern obj* l_Lean_Name_toString___closed__1; +obj* l_Lean_registerOption___closed__2; +extern obj* l_IO_RefPointed; +obj* _init_l_Lean_Options_empty() { _start: { obj* x_0; @@ -23,14 +38,162 @@ x_0 = lean::box(0); return x_0; } } +obj* _init_l_Lean_Options_HasEmptyc() { +_start: +{ +obj* x_0; +x_0 = l_Lean_Options_empty; +return x_0; +} +} +obj* l___private_init_lean_options_1__initOptionDeclsRef(obj* x_0) { +_start: +{ +obj* x_1; obj* x_2; +x_1 = lean::box(0); +x_2 = lean::io_mk_ref(x_1, x_0); +return x_2; +} +} +obj* _init_l_Lean_registerOption___closed__1() { +_start: +{ +obj* x_0; +x_0 = lean::mk_string("invalid option declaration '"); +return x_0; +} +} +obj* _init_l_Lean_registerOption___closed__2() { +_start: +{ +obj* x_0; +x_0 = lean::mk_string("', option already exists"); +return x_0; +} +} +obj* l_Lean_registerOption(obj* x_0, obj* x_1, obj* x_2) { +_start: +{ +obj* x_3; obj* x_4; +x_3 = l___private_init_lean_options_2__optionDeclsRef; +x_4 = lean::io_ref_get(x_3, x_2); +if (lean::obj_tag(x_4) == 0) +{ +obj* x_5; obj* x_7; obj* x_9; uint8 x_11; +x_5 = lean::cnstr_get(x_4, 0); +x_7 = lean::cnstr_get(x_4, 1); +if (lean::is_exclusive(x_4)) { + lean::cnstr_set(x_4, 0, lean::box(0)); + lean::cnstr_set(x_4, 1, lean::box(0)); + x_9 = x_4; +} else { + lean::inc(x_5); + lean::inc(x_7); + lean::dec(x_4); + x_9 = lean::box(0); +} +lean::inc(x_5); +x_11 = l_Lean_NameMap_contains___rarg(x_5, x_0); +if (x_11 == 0) +{ +obj* x_12; obj* x_13; obj* x_14; obj* x_15; +x_12 = lean::box(0); +if (lean::is_scalar(x_9)) { + x_13 = lean::alloc_cnstr(0, 2, 0); +} else { + x_13 = x_9; +} +lean::cnstr_set(x_13, 0, x_12); +lean::cnstr_set(x_13, 1, x_7); +x_14 = l_RBMap_insert___main___at_Lean_NameMap_insert___spec__1___rarg(x_5, x_0, x_1); +x_15 = lean::io_ref_set(x_3, x_14, x_13); +return x_15; +} +else +{ +obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_23; obj* x_24; obj* x_25; +lean::dec(x_5); +lean::dec(x_1); +x_18 = l_Lean_Name_toString___closed__1; +x_19 = l_Lean_Name_toStringWithSep___main(x_18, x_0); +x_20 = l_Lean_registerOption___closed__1; +x_21 = lean::string_append(x_20, x_19); +lean::dec(x_19); +x_23 = l_Lean_registerOption___closed__2; +x_24 = lean::string_append(x_21, x_23); +if (lean::is_scalar(x_9)) { + x_25 = lean::alloc_cnstr(1, 2, 0); +} else { + x_25 = x_9; + lean::cnstr_set_tag(x_9, 1); +} +lean::cnstr_set(x_25, 0, x_24); +lean::cnstr_set(x_25, 1, x_7); +return x_25; +} +} +else +{ +obj* x_28; obj* x_30; obj* x_32; obj* x_33; +lean::dec(x_1); +lean::dec(x_0); +x_28 = lean::cnstr_get(x_4, 0); +x_30 = lean::cnstr_get(x_4, 1); +if (lean::is_exclusive(x_4)) { + x_32 = x_4; +} else { + lean::inc(x_28); + lean::inc(x_30); + lean::dec(x_4); + x_32 = lean::box(0); +} +if (lean::is_scalar(x_32)) { + x_33 = lean::alloc_cnstr(1, 2, 0); +} else { + x_33 = x_32; +} +lean::cnstr_set(x_33, 0, x_28); +lean::cnstr_set(x_33, 1, x_30); +return x_33; +} +} +} +obj* l_Lean_getOptionDecls(obj* x_0) { +_start: +{ +obj* x_1; obj* x_2; +x_1 = l___private_init_lean_options_2__optionDeclsRef; +x_2 = lean::io_ref_get(x_1, x_0); +return x_2; +} +} obj* initialize_init_lean_kvmap(obj*); +obj* initialize_init_io(obj*); +obj* initialize_init_control_combinators(obj*); +obj* initialize_init_data_tostring(obj*); static bool _G_initialized = false; obj* initialize_init_lean_options(obj* w) { if (_G_initialized) return w; _G_initialized = true; if (io_result_is_error(w)) return w; w = initialize_init_lean_kvmap(w); - l_Lean_Options_mk = _init_l_Lean_Options_mk(); -lean::mark_persistent(l_Lean_Options_mk); +if (io_result_is_error(w)) return w; +w = initialize_init_io(w); +if (io_result_is_error(w)) return w; +w = initialize_init_control_combinators(w); +if (io_result_is_error(w)) return w; +w = initialize_init_data_tostring(w); + l_Lean_Options_empty = _init_l_Lean_Options_empty(); +lean::mark_persistent(l_Lean_Options_empty); + l_Lean_Options_HasEmptyc = _init_l_Lean_Options_HasEmptyc(); +lean::mark_persistent(l_Lean_Options_HasEmptyc); +w = l___private_init_lean_options_1__initOptionDeclsRef(w); +if (io_result_is_error(w)) return w; + l___private_init_lean_options_2__optionDeclsRef = io_result_get_value(w); +lean::mark_persistent(l___private_init_lean_options_2__optionDeclsRef); + l_Lean_registerOption___closed__1 = _init_l_Lean_registerOption___closed__1(); +lean::mark_persistent(l_Lean_registerOption___closed__1); + l_Lean_registerOption___closed__2 = _init_l_Lean_registerOption___closed__2(); +lean::mark_persistent(l_Lean_registerOption___closed__2); return w; } diff --git a/src/stage0/init/lean/trace.cpp b/src/stage0/init/lean/trace.cpp index 55318c2c74..8614b96d61 100644 --- a/src/stage0/init/lean/trace.cpp +++ b/src/stage0/init/lean/trace.cpp @@ -28,7 +28,6 @@ obj* l_Lean_Trace_Lean_Trace_MonadTracer___rarg___lambda__8(obj*, obj*, obj*, ob obj* l_Lean_Trace_Trace___rarg(obj*, obj*, obj*, obj*); obj* l_RBNode_insert___at_Lean_Trace_Lean_Trace_MonadTracer___spec__2(obj*, obj*, obj*); obj* l_Lean_Trace_Lean_Trace_MonadTracer___rarg___lambda__12___boxed(obj*, obj*, obj*, obj*, obj*, obj*); -obj* l_Lean_Kvmap_getBool(obj*, obj*); obj* l_Lean_Trace_TraceT_run___rarg___lambda__1(obj*, obj*); obj* l_Lean_Trace_pp(obj*); obj* l_Lean_Trace_Monad___boxed(obj*); @@ -37,6 +36,7 @@ obj* l_Lean_Trace_Lean_Trace_MonadTracer___rarg___lambda__10(obj*, obj*, obj*, o obj* l_Lean_Trace_Lean_Trace_MonadTracer(obj*); obj* l_RBNode_balance2___main___rarg(obj*, obj*); obj* l_Lean_Trace_Lean_Trace_MonadTracer___rarg___lambda__6___boxed(obj*, obj*, obj*); +obj* l_Lean_KVMap_getBool(obj*, obj*); obj* l_MonadStateAdapter_adaptState_x_27___at_Lean_Trace_Lean_Trace_MonadTracer___spec__4___boxed(obj*); obj* l_Lean_Trace_Lean_Trace_MonadTracer___rarg___lambda__3(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_Lean_Trace_Lean_Trace_MonadTracer___boxed(obj*); @@ -676,7 +676,7 @@ if (lean::is_exclusive(x_6)) { x_12 = lean::cnstr_get(x_7, 0); lean::inc(x_12); lean::dec(x_7); -x_15 = l_Lean_Kvmap_getBool(x_12, x_0); +x_15 = l_Lean_KVMap_getBool(x_12, x_0); if (lean::obj_tag(x_15) == 0) { obj* x_21; obj* x_23; @@ -943,7 +943,7 @@ if (lean::is_exclusive(x_8)) { x_27 = lean::cnstr_get(x_1, 0); lean::inc(x_27); lean::inc(x_27); -x_32 = l_Lean_Kvmap_getBool(x_27, x_4); +x_32 = l_Lean_KVMap_getBool(x_27, x_4); if (lean::obj_tag(x_32) == 0) { obj* x_37;