diff --git a/stage0/stdlib/Init/Data/AC.c b/stage0/stdlib/Init/Data/AC.c index df3c8b836b..0498160dc4 100644 --- a/stage0/stdlib/Init/Data/AC.c +++ b/stage0/stdlib/Init/Data/AC.c @@ -1324,6 +1324,45 @@ lean_dec(x_3); return x_4; } } +LEAN_EXPORT lean_object* l___private_Init_Data_AC_0__Lean_Data_AC_insert_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_dec(x_3); +lean_inc(x_2); +return x_2; +} +else +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 1); +lean_inc(x_5); +lean_dec(x_1); +x_6 = lean_apply_2(x_3, x_4, x_5); +return x_6; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_AC_0__Lean_Data_AC_insert_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_AC_0__Lean_Data_AC_insert_match__1_splitter___rarg___boxed), 3, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_AC_0__Lean_Data_AC_insert_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l___private_Init_Data_AC_0__Lean_Data_AC_insert_match__1_splitter___rarg(x_1, x_2, x_3); +lean_dec(x_2); +return x_4; +} +} LEAN_EXPORT lean_object* l___private_Init_Data_AC_0__Lean_Data_AC_mergeIdem_loop_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { @@ -1448,45 +1487,6 @@ lean_dec(x_2); return x_5; } } -LEAN_EXPORT lean_object* l___private_Init_Data_AC_0__Lean_Data_AC_insert_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { -_start: -{ -if (lean_obj_tag(x_1) == 0) -{ -lean_dec(x_3); -lean_inc(x_2); -return x_2; -} -else -{ -lean_object* x_4; lean_object* x_5; lean_object* x_6; -x_4 = lean_ctor_get(x_1, 0); -lean_inc(x_4); -x_5 = lean_ctor_get(x_1, 1); -lean_inc(x_5); -lean_dec(x_1); -x_6 = lean_apply_2(x_3, x_4, x_5); -return x_6; -} -} -} -LEAN_EXPORT lean_object* l___private_Init_Data_AC_0__Lean_Data_AC_insert_match__1_splitter(lean_object* x_1) { -_start: -{ -lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l___private_Init_Data_AC_0__Lean_Data_AC_insert_match__1_splitter___rarg___boxed), 3, 0); -return x_2; -} -} -LEAN_EXPORT lean_object* l___private_Init_Data_AC_0__Lean_Data_AC_insert_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { -_start: -{ -lean_object* x_4; -x_4 = l___private_Init_Data_AC_0__Lean_Data_AC_insert_match__1_splitter___rarg(x_1, x_2, x_3); -lean_dec(x_2); -return x_4; -} -} LEAN_EXPORT lean_object* l___private_Init_Data_AC_0__Lean_Data_AC_sort_loop_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { diff --git a/stage0/stdlib/Init/Data/BitVec/Lemmas.c b/stage0/stdlib/Init/Data/BitVec/Lemmas.c index 5a395836b6..0caddd8013 100644 --- a/stage0/stdlib/Init/Data/BitVec/Lemmas.c +++ b/stage0/stdlib/Init/Data/BitVec/Lemmas.c @@ -16,39 +16,19 @@ extern "C" { LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_replicate_match__1_splitter___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_ofBoolListBE_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_replicate_match__1_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_BitVec_intMin___boxed(lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_replicate_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_BitVec_ofNat(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_BitVec_intMax___boxed(lean_object*); +LEAN_EXPORT lean_object* l_BitVec_intMin(lean_object*); LEAN_EXPORT lean_object* l_BitVec_intMax(lean_object*); -lean_object* lean_nat_pow(lean_object*, lean_object*); +lean_object* l_BitVec_twoPow(lean_object*, lean_object*); uint8_t lean_nat_dec_eq(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_ofBoolListBE_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_replicate_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_nat_sub(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_ofBoolListBE_match__1_splitter(lean_object*); -LEAN_EXPORT lean_object* l_BitVec_intMax(lean_object* x_1) { -_start: -{ -lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; -x_2 = lean_unsigned_to_nat(2u); -x_3 = lean_nat_pow(x_2, x_1); -x_4 = lean_unsigned_to_nat(1u); -x_5 = lean_nat_sub(x_3, x_4); -lean_dec(x_3); -x_6 = l_BitVec_ofNat(x_1, x_5); -lean_dec(x_5); -return x_6; -} -} -LEAN_EXPORT lean_object* l_BitVec_intMax___boxed(lean_object* x_1) { -_start: -{ -lean_object* x_2; -x_2 = l_BitVec_intMax(x_1); -lean_dec(x_1); -return x_2; -} -} +lean_object* l_BitVec_sub(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_ofBoolListBE_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -138,6 +118,50 @@ lean_dec(x_1); return x_3; } } +LEAN_EXPORT lean_object* l_BitVec_intMin(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_2 = lean_unsigned_to_nat(1u); +x_3 = lean_nat_sub(x_1, x_2); +x_4 = l_BitVec_twoPow(x_1, x_3); +lean_dec(x_3); +return x_4; +} +} +LEAN_EXPORT lean_object* l_BitVec_intMin___boxed(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = l_BitVec_intMin(x_1); +lean_dec(x_1); +return x_2; +} +} +LEAN_EXPORT lean_object* l_BitVec_intMax(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_2 = lean_unsigned_to_nat(1u); +x_3 = lean_nat_sub(x_1, x_2); +x_4 = l_BitVec_twoPow(x_1, x_3); +lean_dec(x_3); +x_5 = l_BitVec_ofNat(x_1, x_2); +x_6 = l_BitVec_sub(x_1, x_4, x_5); +lean_dec(x_5); +lean_dec(x_4); +return x_6; +} +} +LEAN_EXPORT lean_object* l_BitVec_intMax___boxed(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = l_BitVec_intMax(x_1); +lean_dec(x_1); +return x_2; +} +} lean_object* initialize_Init_Data_Bool(uint8_t builtin, lean_object*); lean_object* initialize_Init_Data_BitVec_Basic(uint8_t builtin, lean_object*); lean_object* initialize_Init_Data_Fin_Lemmas(uint8_t builtin, lean_object*); diff --git a/stage0/stdlib/Init/Data/Fin/Basic.c b/stage0/stdlib/Init/Data/Fin/Basic.c index c936aa0f86..92562d545c 100644 --- a/stage0/stdlib/Init/Data/Fin/Basic.c +++ b/stage0/stdlib/Init/Data/Fin/Basic.c @@ -26,6 +26,7 @@ LEAN_EXPORT lean_object* l_Fin_elim0___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Fin_coeToNat___rarg(lean_object*); LEAN_EXPORT lean_object* l_Fin_shiftLeft(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Fin_last___boxed(lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Fin_Basic_0__Fin_modn_match__1_splitter___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Fin_succ(lean_object*); LEAN_EXPORT lean_object* l_Fin_pred(lean_object*); LEAN_EXPORT lean_object* l_Fin_castAdd(lean_object*, lean_object*); @@ -52,6 +53,8 @@ LEAN_EXPORT lean_object* l_Fin_castSucc___rarg___boxed(lean_object*); lean_object* lean_nat_div(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Fin_cast___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Fin_sub(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Fin_Basic_0__Fin_modn_match__1_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Fin_Basic_0__Fin_modn_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Fin_modn___rarg___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Fin_lor___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Fin_addNat___rarg(lean_object*, lean_object*); @@ -678,6 +681,31 @@ lean_dec(x_1); return x_2; } } +LEAN_EXPORT lean_object* l___private_Init_Data_Fin_Basic_0__Fin_modn_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = lean_apply_3(x_3, x_1, lean_box(0), x_2); +return x_4; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Fin_Basic_0__Fin_modn_match__1_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Init_Data_Fin_Basic_0__Fin_modn_match__1_splitter___rarg), 3, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Fin_Basic_0__Fin_modn_match__1_splitter___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l___private_Init_Data_Fin_Basic_0__Fin_modn_match__1_splitter(x_1, x_2); +lean_dec(x_1); +return x_3; +} +} LEAN_EXPORT lean_object* l_Fin_last(lean_object* x_1) { _start: { diff --git a/stage0/stdlib/Init/Data/Int/DivMod.c b/stage0/stdlib/Init/Data/Int/DivMod.c index 9c58431c70..1886398554 100644 --- a/stage0/stdlib/Init/Data/Int/DivMod.c +++ b/stage0/stdlib/Init/Data/Int/DivMod.c @@ -25,8 +25,11 @@ static lean_object* l_Int_bmod___closed__2; LEAN_EXPORT lean_object* l_Int_fdiv(lean_object*, lean_object*); lean_object* lean_nat_to_int(lean_object*); lean_object* lean_nat_div(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivMod_0__Int_fdiv_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Int_fmod(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivMod_0__Int_fdiv_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Int_fdiv___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivMod_0__Int_fdiv_match__1_splitter(lean_object*); LEAN_EXPORT lean_object* l_Int_bmod___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Int_div___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Int_bmod(lean_object*, lean_object*); @@ -355,6 +358,130 @@ x_1 = l_Int_instMod___closed__1; return x_1; } } +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivMod_0__Int_fdiv_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { +_start: +{ +lean_object* x_9; uint8_t x_10; +x_9 = l_Int_fdiv___closed__1; +x_10 = lean_int_dec_lt(x_1, x_9); +if (x_10 == 0) +{ +lean_object* x_11; lean_object* x_12; uint8_t x_13; +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +x_11 = lean_nat_abs(x_1); +x_12 = lean_unsigned_to_nat(0u); +x_13 = lean_nat_dec_eq(x_11, x_12); +if (x_13 == 0) +{ +lean_object* x_14; lean_object* x_15; uint8_t x_16; +lean_dec(x_3); +x_14 = lean_unsigned_to_nat(1u); +x_15 = lean_nat_sub(x_11, x_14); +x_16 = lean_int_dec_lt(x_2, x_9); +if (x_16 == 0) +{ +lean_object* x_17; lean_object* x_18; +lean_dec(x_15); +lean_dec(x_5); +x_17 = lean_nat_abs(x_2); +lean_dec(x_2); +x_18 = lean_apply_3(x_4, x_11, x_17, lean_box(0)); +return x_18; +} +else +{ +lean_object* x_19; lean_object* x_20; lean_object* x_21; +lean_dec(x_11); +lean_dec(x_4); +x_19 = lean_nat_abs(x_2); +lean_dec(x_2); +x_20 = lean_nat_sub(x_19, x_14); +lean_dec(x_19); +x_21 = lean_apply_2(x_5, x_15, x_20); +return x_21; +} +} +else +{ +lean_object* x_22; +lean_dec(x_11); +lean_dec(x_5); +lean_dec(x_4); +x_22 = lean_apply_1(x_3, x_2); +return x_22; +} +} +else +{ +lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26; +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +x_23 = lean_nat_abs(x_1); +x_24 = lean_unsigned_to_nat(1u); +x_25 = lean_nat_sub(x_23, x_24); +lean_dec(x_23); +x_26 = lean_int_dec_lt(x_2, x_9); +if (x_26 == 0) +{ +lean_object* x_27; lean_object* x_28; uint8_t x_29; +lean_dec(x_8); +x_27 = lean_nat_abs(x_2); +lean_dec(x_2); +x_28 = lean_unsigned_to_nat(0u); +x_29 = lean_nat_dec_eq(x_27, x_28); +if (x_29 == 0) +{ +lean_object* x_30; lean_object* x_31; +lean_dec(x_6); +x_30 = lean_nat_sub(x_27, x_24); +lean_dec(x_27); +x_31 = lean_apply_2(x_7, x_25, x_30); +return x_31; +} +else +{ +lean_object* x_32; +lean_dec(x_27); +lean_dec(x_7); +x_32 = lean_apply_1(x_6, x_25); +return x_32; +} +} +else +{ +lean_object* x_33; lean_object* x_34; lean_object* x_35; +lean_dec(x_7); +lean_dec(x_6); +x_33 = lean_nat_abs(x_2); +lean_dec(x_2); +x_34 = lean_nat_sub(x_33, x_24); +lean_dec(x_33); +x_35 = lean_apply_2(x_8, x_25, x_34); +return x_35; +} +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivMod_0__Int_fdiv_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Int_DivMod_0__Int_fdiv_match__1_splitter___rarg___boxed), 8, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivMod_0__Int_fdiv_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { +_start: +{ +lean_object* x_9; +x_9 = l___private_Init_Data_Int_DivMod_0__Int_fdiv_match__1_splitter___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8); +lean_dec(x_1); +return x_9; +} +} LEAN_EXPORT lean_object* l_Nat_cast___at_Int_bmod___spec__1(lean_object* x_1) { _start: { diff --git a/stage0/stdlib/Init/Data/Int/DivModLemmas.c b/stage0/stdlib/Init/Data/Int/DivModLemmas.c index 05479ca826..fb8c41a88f 100644 --- a/stage0/stdlib/Init/Data/Int/DivModLemmas.c +++ b/stage0/stdlib/Init/Data/Int/DivModLemmas.c @@ -16,10 +16,23 @@ extern "C" { LEAN_EXPORT uint8_t l_Int_decidableDvd(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Int_decidableDvd___boxed(lean_object*, lean_object*); lean_object* lean_int_emod(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_ediv_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter(lean_object*); lean_object* lean_nat_to_int(lean_object*); -static lean_object* l_Int_decidableDvd___closed__1; +static lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter___rarg___closed__1; +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_ediv_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_ediv_match__1_splitter(lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_fmod_match__1_splitter(lean_object*); +lean_object* lean_nat_abs(lean_object*); +uint8_t lean_nat_dec_eq(lean_object*, lean_object*); +uint8_t lean_int_dec_lt(lean_object*, lean_object*); +lean_object* lean_nat_sub(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_fmod_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_int_dec_eq(lean_object*, lean_object*); -static lean_object* _init_l_Int_decidableDvd___closed__1() { +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_fmod_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* _init_l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter___rarg___closed__1() { _start: { lean_object* x_1; lean_object* x_2; @@ -28,12 +41,195 @@ x_2 = lean_nat_to_int(x_1); return x_2; } } +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; uint8_t x_8; +x_7 = l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter___rarg___closed__1; +x_8 = lean_int_dec_lt(x_1, x_7); +if (x_8 == 0) +{ +lean_object* x_9; uint8_t x_10; +lean_dec(x_6); +lean_dec(x_5); +x_9 = lean_nat_abs(x_1); +x_10 = lean_int_dec_lt(x_2, x_7); +if (x_10 == 0) +{ +lean_object* x_11; lean_object* x_12; +lean_dec(x_4); +x_11 = lean_nat_abs(x_2); +x_12 = lean_apply_2(x_3, x_9, x_11); +return x_12; +} +else +{ +lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; +lean_dec(x_3); +x_13 = lean_nat_abs(x_2); +x_14 = lean_unsigned_to_nat(1u); +x_15 = lean_nat_sub(x_13, x_14); +lean_dec(x_13); +x_16 = lean_apply_2(x_4, x_9, x_15); +return x_16; +} +} +else +{ +lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; +lean_dec(x_4); +lean_dec(x_3); +x_17 = lean_nat_abs(x_1); +x_18 = lean_unsigned_to_nat(1u); +x_19 = lean_nat_sub(x_17, x_18); +lean_dec(x_17); +x_20 = lean_int_dec_lt(x_2, x_7); +if (x_20 == 0) +{ +lean_object* x_21; lean_object* x_22; +lean_dec(x_6); +x_21 = lean_nat_abs(x_2); +x_22 = lean_apply_2(x_5, x_19, x_21); +return x_22; +} +else +{ +lean_object* x_23; lean_object* x_24; lean_object* x_25; +lean_dec(x_5); +x_23 = lean_nat_abs(x_2); +x_24 = lean_nat_sub(x_23, x_18); +lean_dec(x_23); +x_25 = lean_apply_2(x_6, x_19, x_24); +return x_25; +} +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter___rarg___boxed), 6, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +x_7 = l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter___rarg(x_1, x_2, x_3, x_4, x_5, x_6); +lean_dec(x_2); +lean_dec(x_1); +return x_7; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_ediv_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { +_start: +{ +lean_object* x_8; uint8_t x_9; +x_8 = l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter___rarg___closed__1; +x_9 = lean_int_dec_lt(x_1, x_8); +if (x_9 == 0) +{ +lean_object* x_10; uint8_t x_11; +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +x_10 = lean_nat_abs(x_1); +x_11 = lean_int_dec_lt(x_2, x_8); +if (x_11 == 0) +{ +lean_object* x_12; lean_object* x_13; +lean_dec(x_4); +x_12 = lean_nat_abs(x_2); +x_13 = lean_apply_2(x_3, x_10, x_12); +return x_13; +} +else +{ +lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; +lean_dec(x_3); +x_14 = lean_nat_abs(x_2); +x_15 = lean_unsigned_to_nat(1u); +x_16 = lean_nat_sub(x_14, x_15); +lean_dec(x_14); +x_17 = lean_apply_2(x_4, x_10, x_16); +return x_17; +} +} +else +{ +lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21; +lean_dec(x_4); +lean_dec(x_3); +x_18 = lean_nat_abs(x_1); +x_19 = lean_unsigned_to_nat(1u); +x_20 = lean_nat_sub(x_18, x_19); +lean_dec(x_18); +x_21 = lean_int_dec_lt(x_2, x_8); +if (x_21 == 0) +{ +lean_object* x_22; lean_object* x_23; uint8_t x_24; +lean_dec(x_7); +x_22 = lean_nat_abs(x_2); +x_23 = lean_unsigned_to_nat(0u); +x_24 = lean_nat_dec_eq(x_22, x_23); +if (x_24 == 0) +{ +lean_object* x_25; lean_object* x_26; +lean_dec(x_5); +x_25 = lean_nat_sub(x_22, x_19); +lean_dec(x_22); +x_26 = lean_apply_2(x_6, x_20, x_25); +return x_26; +} +else +{ +lean_object* x_27; +lean_dec(x_22); +lean_dec(x_6); +x_27 = lean_apply_1(x_5, x_20); +return x_27; +} +} +else +{ +lean_object* x_28; lean_object* x_29; lean_object* x_30; +lean_dec(x_6); +lean_dec(x_5); +x_28 = lean_nat_abs(x_2); +x_29 = lean_nat_sub(x_28, x_19); +lean_dec(x_28); +x_30 = lean_apply_2(x_7, x_20, x_29); +return x_30; +} +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_ediv_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Int_DivModLemmas_0__Int_ediv_match__1_splitter___rarg___boxed), 7, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_ediv_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { +_start: +{ +lean_object* x_8; +x_8 = l___private_Init_Data_Int_DivModLemmas_0__Int_ediv_match__1_splitter___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7); +lean_dec(x_2); +lean_dec(x_1); +return x_8; +} +} LEAN_EXPORT uint8_t l_Int_decidableDvd(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; lean_object* x_4; uint8_t x_5; x_3 = lean_int_emod(x_2, x_1); -x_4 = l_Int_decidableDvd___closed__1; +x_4 = l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter___rarg___closed__1; x_5 = lean_int_dec_eq(x_3, x_4); lean_dec(x_3); return x_5; @@ -50,6 +246,111 @@ x_4 = lean_box(x_3); return x_4; } } +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_fmod_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { +_start: +{ +lean_object* x_8; uint8_t x_9; +x_8 = l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter___rarg___closed__1; +x_9 = lean_int_dec_lt(x_1, x_8); +if (x_9 == 0) +{ +lean_object* x_10; lean_object* x_11; uint8_t x_12; +lean_dec(x_7); +lean_dec(x_6); +x_10 = lean_nat_abs(x_1); +x_11 = lean_unsigned_to_nat(0u); +x_12 = lean_nat_dec_eq(x_10, x_11); +if (x_12 == 0) +{ +lean_object* x_13; lean_object* x_14; uint8_t x_15; +lean_dec(x_3); +x_13 = lean_unsigned_to_nat(1u); +x_14 = lean_nat_sub(x_10, x_13); +x_15 = lean_int_dec_lt(x_2, x_8); +if (x_15 == 0) +{ +lean_object* x_16; lean_object* x_17; +lean_dec(x_14); +lean_dec(x_5); +x_16 = lean_nat_abs(x_2); +lean_dec(x_2); +x_17 = lean_apply_3(x_4, x_10, x_16, lean_box(0)); +return x_17; +} +else +{ +lean_object* x_18; lean_object* x_19; lean_object* x_20; +lean_dec(x_10); +lean_dec(x_4); +x_18 = lean_nat_abs(x_2); +lean_dec(x_2); +x_19 = lean_nat_sub(x_18, x_13); +lean_dec(x_18); +x_20 = lean_apply_2(x_5, x_14, x_19); +return x_20; +} +} +else +{ +lean_object* x_21; +lean_dec(x_10); +lean_dec(x_5); +lean_dec(x_4); +x_21 = lean_apply_1(x_3, x_2); +return x_21; +} +} +else +{ +lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25; +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +x_22 = lean_nat_abs(x_1); +x_23 = lean_unsigned_to_nat(1u); +x_24 = lean_nat_sub(x_22, x_23); +lean_dec(x_22); +x_25 = lean_int_dec_lt(x_2, x_8); +if (x_25 == 0) +{ +lean_object* x_26; lean_object* x_27; +lean_dec(x_7); +x_26 = lean_nat_abs(x_2); +lean_dec(x_2); +x_27 = lean_apply_2(x_6, x_24, x_26); +return x_27; +} +else +{ +lean_object* x_28; lean_object* x_29; lean_object* x_30; +lean_dec(x_6); +x_28 = lean_nat_abs(x_2); +lean_dec(x_2); +x_29 = lean_nat_sub(x_28, x_23); +lean_dec(x_28); +x_30 = lean_apply_2(x_7, x_24, x_29); +return x_30; +} +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_fmod_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Int_DivModLemmas_0__Int_fmod_match__1_splitter___rarg___boxed), 7, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_DivModLemmas_0__Int_fmod_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { +_start: +{ +lean_object* x_8; +x_8 = l___private_Init_Data_Int_DivModLemmas_0__Int_fmod_match__1_splitter___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7); +lean_dec(x_1); +return x_8; +} +} lean_object* initialize_Init_Data_Int_DivMod(uint8_t builtin, lean_object*); lean_object* initialize_Init_Data_Int_Order(uint8_t builtin, lean_object*); lean_object* initialize_Init_Data_Nat_Dvd(uint8_t builtin, lean_object*); @@ -71,8 +372,8 @@ lean_dec_ref(res); res = initialize_Init_RCases(builtin, lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -l_Int_decidableDvd___closed__1 = _init_l_Int_decidableDvd___closed__1(); -lean_mark_persistent(l_Int_decidableDvd___closed__1); +l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter___rarg___closed__1 = _init_l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter___rarg___closed__1(); +lean_mark_persistent(l___private_Init_Data_Int_DivModLemmas_0__Int_div_match__1_splitter___rarg___closed__1); return lean_io_result_mk_ok(lean_box(0)); } #ifdef __cplusplus diff --git a/stage0/stdlib/Init/Data/Int/Order.c b/stage0/stdlib/Init/Data/Int/Order.c index 1c97217e69..ea5d8e65d5 100644 --- a/stage0/stdlib/Init/Data/Int/Order.c +++ b/stage0/stdlib/Init/Data/Int/Order.c @@ -13,10 +13,28 @@ #ifdef __cplusplus extern "C" { #endif +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_toNat_match__1_splitter(lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_neg_match__1_splitter(lean_object*); +lean_object* lean_nat_to_int(lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_sign_match__1_splitter(lean_object*); LEAN_EXPORT lean_object* l_Int_instTransLtLe; +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_sign_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter(lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* lean_nat_abs(lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_neg_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Int_instTransLeLt; +uint8_t lean_nat_dec_eq(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_neg_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Int_instTransLt; +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_sign_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +uint8_t lean_int_dec_lt(lean_object*, lean_object*); +lean_object* lean_nat_sub(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_toNat_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); +static lean_object* l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter___rarg___closed__1; LEAN_EXPORT lean_object* l_Int_instTransLe; +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_toNat_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); static lean_object* _init_l_Int_instTransLe() { _start: { @@ -41,6 +59,246 @@ _start: return lean_box(0); } } +static lean_object* _init_l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter___rarg___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = lean_unsigned_to_nat(0u); +x_2 = lean_nat_to_int(x_1); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; uint8_t x_8; +x_7 = l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter___rarg___closed__1; +x_8 = lean_int_dec_lt(x_1, x_7); +if (x_8 == 0) +{ +lean_object* x_9; uint8_t x_10; +lean_dec(x_6); +lean_dec(x_5); +x_9 = lean_nat_abs(x_1); +x_10 = lean_int_dec_lt(x_2, x_7); +if (x_10 == 0) +{ +lean_object* x_11; lean_object* x_12; +lean_dec(x_4); +x_11 = lean_nat_abs(x_2); +x_12 = lean_apply_2(x_3, x_9, x_11); +return x_12; +} +else +{ +lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; +lean_dec(x_3); +x_13 = lean_nat_abs(x_2); +x_14 = lean_unsigned_to_nat(1u); +x_15 = lean_nat_sub(x_13, x_14); +lean_dec(x_13); +x_16 = lean_apply_2(x_4, x_9, x_15); +return x_16; +} +} +else +{ +lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; +lean_dec(x_4); +lean_dec(x_3); +x_17 = lean_nat_abs(x_1); +x_18 = lean_unsigned_to_nat(1u); +x_19 = lean_nat_sub(x_17, x_18); +lean_dec(x_17); +x_20 = lean_int_dec_lt(x_2, x_7); +if (x_20 == 0) +{ +lean_object* x_21; lean_object* x_22; +lean_dec(x_6); +x_21 = lean_nat_abs(x_2); +x_22 = lean_apply_2(x_5, x_19, x_21); +return x_22; +} +else +{ +lean_object* x_23; lean_object* x_24; lean_object* x_25; +lean_dec(x_5); +x_23 = lean_nat_abs(x_2); +x_24 = lean_nat_sub(x_23, x_18); +lean_dec(x_23); +x_25 = lean_apply_2(x_6, x_19, x_24); +return x_25; +} +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter___rarg___boxed), 6, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +x_7 = l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter___rarg(x_1, x_2, x_3, x_4, x_5, x_6); +lean_dec(x_2); +lean_dec(x_1); +return x_7; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_neg_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; uint8_t x_5; +x_4 = l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter___rarg___closed__1; +x_5 = lean_int_dec_lt(x_1, x_4); +if (x_5 == 0) +{ +lean_object* x_6; lean_object* x_7; +lean_dec(x_3); +x_6 = lean_nat_abs(x_1); +x_7 = lean_apply_1(x_2, x_6); +return x_7; +} +else +{ +lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; +lean_dec(x_2); +x_8 = lean_nat_abs(x_1); +x_9 = lean_unsigned_to_nat(1u); +x_10 = lean_nat_sub(x_8, x_9); +lean_dec(x_8); +x_11 = lean_apply_1(x_3, x_10); +return x_11; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_neg_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Int_Order_0__Int_neg_match__1_splitter___rarg___boxed), 3, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_neg_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l___private_Init_Data_Int_Order_0__Int_neg_match__1_splitter___rarg(x_1, x_2, x_3); +lean_dec(x_1); +return x_4; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_toNat_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; uint8_t x_5; +x_4 = l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter___rarg___closed__1; +x_5 = lean_int_dec_lt(x_1, x_4); +if (x_5 == 0) +{ +lean_object* x_6; lean_object* x_7; +lean_dec(x_3); +x_6 = lean_nat_abs(x_1); +x_7 = lean_apply_1(x_2, x_6); +return x_7; +} +else +{ +lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; +lean_dec(x_2); +x_8 = lean_nat_abs(x_1); +x_9 = lean_unsigned_to_nat(1u); +x_10 = lean_nat_sub(x_8, x_9); +lean_dec(x_8); +x_11 = lean_apply_1(x_3, x_10); +return x_11; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_toNat_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Int_Order_0__Int_toNat_match__1_splitter___rarg___boxed), 3, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_toNat_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l___private_Init_Data_Int_Order_0__Int_toNat_match__1_splitter___rarg(x_1, x_2, x_3); +lean_dec(x_1); +return x_4; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_sign_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; uint8_t x_6; +x_5 = l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter___rarg___closed__1; +x_6 = lean_int_dec_lt(x_1, x_5); +if (x_6 == 0) +{ +lean_object* x_7; lean_object* x_8; uint8_t x_9; +lean_dec(x_4); +x_7 = lean_nat_abs(x_1); +x_8 = lean_unsigned_to_nat(0u); +x_9 = lean_nat_dec_eq(x_7, x_8); +if (x_9 == 0) +{ +lean_object* x_10; lean_object* x_11; lean_object* x_12; +x_10 = lean_unsigned_to_nat(1u); +x_11 = lean_nat_sub(x_7, x_10); +lean_dec(x_7); +x_12 = lean_apply_1(x_2, x_11); +return x_12; +} +else +{ +lean_dec(x_7); +lean_dec(x_2); +lean_inc(x_3); +return x_3; +} +} +else +{ +lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; +lean_dec(x_2); +x_13 = lean_nat_abs(x_1); +x_14 = lean_unsigned_to_nat(1u); +x_15 = lean_nat_sub(x_13, x_14); +lean_dec(x_13); +x_16 = lean_apply_1(x_4, x_15); +return x_16; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_sign_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Int_Order_0__Int_sign_match__1_splitter___rarg___boxed), 4, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Int_Order_0__Int_sign_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; +x_5 = l___private_Init_Data_Int_Order_0__Int_sign_match__1_splitter___rarg(x_1, x_2, x_3, x_4); +lean_dec(x_3); +lean_dec(x_1); +return x_5; +} +} lean_object* initialize_Init_Data_Int_Lemmas(uint8_t builtin, lean_object*); lean_object* initialize_Init_ByCases(uint8_t builtin, lean_object*); static bool _G_initialized = false; @@ -58,6 +316,8 @@ l_Int_instTransLe = _init_l_Int_instTransLe(); l_Int_instTransLtLe = _init_l_Int_instTransLtLe(); l_Int_instTransLeLt = _init_l_Int_instTransLeLt(); l_Int_instTransLt = _init_l_Int_instTransLt(); +l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter___rarg___closed__1 = _init_l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter___rarg___closed__1(); +lean_mark_persistent(l___private_Init_Data_Int_Order_0__Int_add_match__1_splitter___rarg___closed__1); return lean_io_result_mk_ok(lean_box(0)); } #ifdef __cplusplus diff --git a/stage0/stdlib/Init/Data/List/Lemmas.c b/stage0/stdlib/Init/Data/List/Lemmas.c index fcaa5dd2ef..8b5beadc40 100644 --- a/stage0/stdlib/Init/Data/List/Lemmas.c +++ b/stage0/stdlib/Init/Data/List/Lemmas.c @@ -19,6 +19,7 @@ LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_filter_match_ LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_findSome_x3f_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLast_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_replicate_match__1_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__Option_isSome_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_foldlRecOn___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_splitAt_go_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_findSome_x3f_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); @@ -28,13 +29,16 @@ LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_filterMap__re LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_partition_loop_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_any__filterMap_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_foldlRecOn(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLastD_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_filterMap_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_foldl_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLast_x3f_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_foldlRecOn___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLast_x21_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLast_x3f_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_filter_match__1_splitter(lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_replicate_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLastD_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_foldrRecOn(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_foldrRecOn___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_nat_dec_eq(lean_object*, lean_object*); @@ -42,12 +46,16 @@ lean_object* l_List_foldr___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_findSome_x3f_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_any__filterMap_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLast_x3f_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLast_x21_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_foldrRecOn___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_nat_sub(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLast_x21_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_foldl_match__1_splitter(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_filterMap__replicate_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_replicate_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_filter_match__1_splitter___rarg(uint8_t, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__Option_isSome_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__Option_isSome_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_partition_loop_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLast_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_filterMap__replicate_match__1_splitter(lean_object*, lean_object*); @@ -273,6 +281,77 @@ x_3 = lean_alloc_closure((void*)(l___private_Init_Data_List_Lemmas_0__List_getLa return x_3; } } +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLast_x21_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_dec(x_3); +lean_inc(x_2); +return x_2; +} +else +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 1); +lean_inc(x_5); +lean_dec(x_1); +x_6 = lean_apply_2(x_3, x_4, x_5); +return x_6; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLast_x21_match__1_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Init_Data_List_Lemmas_0__List_getLast_x21_match__1_splitter___rarg___boxed), 3, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLast_x21_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l___private_Init_Data_List_Lemmas_0__List_getLast_x21_match__1_splitter___rarg(x_1, x_2, x_3); +lean_dec(x_2); +return x_4; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLastD_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_object* x_5; +lean_dec(x_4); +x_5 = lean_apply_1(x_3, x_2); +return x_5; +} +else +{ +lean_object* x_6; lean_object* x_7; lean_object* x_8; +lean_dec(x_3); +x_6 = lean_ctor_get(x_1, 0); +lean_inc(x_6); +x_7 = lean_ctor_get(x_1, 1); +lean_inc(x_7); +lean_dec(x_1); +x_8 = lean_apply_3(x_4, x_6, x_7, x_2); +return x_8; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_getLastD_match__1_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Init_Data_List_Lemmas_0__List_getLastD_match__1_splitter___rarg), 4, 0); +return x_3; +} +} LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_filter_match__1_splitter___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -345,6 +424,43 @@ lean_dec(x_2); return x_4; } } +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__Option_isSome_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_dec(x_2); +lean_inc(x_3); +return x_3; +} +else +{ +lean_object* x_4; lean_object* x_5; +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_1(x_2, x_4); +return x_5; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__Option_isSome_match__1_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Init_Data_List_Lemmas_0__Option_isSome_match__1_splitter___rarg___boxed), 3, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__Option_isSome_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l___private_Init_Data_List_Lemmas_0__Option_isSome_match__1_splitter___rarg(x_1, x_2, x_3); +lean_dec(x_3); +return x_4; +} +} LEAN_EXPORT lean_object* l___private_Init_Data_List_Lemmas_0__List_findSome_x3f_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { diff --git a/stage0/stdlib/Init/Data/List/MinMax.c b/stage0/stdlib/Init/Data/List/MinMax.c index 1588cd18a8..ff2ad385c0 100644 --- a/stage0/stdlib/Init/Data/List/MinMax.c +++ b/stage0/stdlib/Init/Data/List/MinMax.c @@ -13,6 +13,48 @@ #ifdef __cplusplus extern "C" { #endif +LEAN_EXPORT lean_object* l___private_Init_Data_List_MinMax_0__List_getLast_x3f_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_MinMax_0__List_getLast_x3f_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_MinMax_0__List_getLast_x3f_match__1_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_MinMax_0__List_getLast_x3f_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_dec(x_3); +lean_inc(x_2); +return x_2; +} +else +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 1); +lean_inc(x_5); +lean_dec(x_1); +x_6 = lean_apply_2(x_3, x_4, x_5); +return x_6; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_List_MinMax_0__List_getLast_x3f_match__1_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Init_Data_List_MinMax_0__List_getLast_x3f_match__1_splitter___rarg___boxed), 3, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_List_MinMax_0__List_getLast_x3f_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l___private_Init_Data_List_MinMax_0__List_getLast_x3f_match__1_splitter___rarg(x_1, x_2, x_3); +lean_dec(x_2); +return x_4; +} +} lean_object* initialize_Init_Data_List_Lemmas(uint8_t builtin, lean_object*); static bool _G_initialized = false; LEAN_EXPORT lean_object* initialize_Init_Data_List_MinMax(uint8_t builtin, lean_object* w) { diff --git a/stage0/stdlib/Init/Data/List/Perm.c b/stage0/stdlib/Init/Data/List/Perm.c index 9664e39890..5bff3b8ab9 100644 --- a/stage0/stdlib/Init/Data/List/Perm.c +++ b/stage0/stdlib/Init/Data/List/Perm.c @@ -17,8 +17,10 @@ LEAN_EXPORT uint8_t l_List_decidablePerm___rarg(lean_object*, lean_object*, lean LEAN_EXPORT lean_object* l_List_decidablePerm(lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Perm_0__List_reverseAux_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_decidablePerm___rarg___boxed(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_Perm_0__List_getLast_x3f_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_isPerm___at_List_decidablePerm___spec__1(lean_object*); LEAN_EXPORT lean_object* l_List_erase___at_List_decidablePerm___spec__3(lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_Perm_0__List_getLast_x3f_match__1_splitter(lean_object*, lean_object*); uint8_t l_List_isEmpty___rarg(lean_object*); LEAN_EXPORT uint8_t l_List_isPerm___at_List_decidablePerm___spec__1___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_elem___at_List_decidablePerm___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*); @@ -26,6 +28,7 @@ LEAN_EXPORT lean_object* l_List_elem___at_List_decidablePerm___spec__2(lean_obje LEAN_EXPORT lean_object* l_List_isPerm___at_List_decidablePerm___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_List_elem___at_List_decidablePerm___spec__2___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_erase___at_List_decidablePerm___spec__3___rarg(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_Perm_0__List_getLast_x3f_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_isSetoid(lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Perm_0__List_reverseAux_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_isSetoid(lean_object* x_1) { @@ -68,6 +71,45 @@ x_3 = lean_alloc_closure((void*)(l___private_Init_Data_List_Perm_0__List_reverse return x_3; } } +LEAN_EXPORT lean_object* l___private_Init_Data_List_Perm_0__List_getLast_x3f_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_dec(x_3); +lean_inc(x_2); +return x_2; +} +else +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 1); +lean_inc(x_5); +lean_dec(x_1); +x_6 = lean_apply_2(x_3, x_4, x_5); +return x_6; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_List_Perm_0__List_getLast_x3f_match__1_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Init_Data_List_Perm_0__List_getLast_x3f_match__1_splitter___rarg___boxed), 3, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_List_Perm_0__List_getLast_x3f_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l___private_Init_Data_List_Perm_0__List_getLast_x3f_match__1_splitter___rarg(x_1, x_2, x_3); +lean_dec(x_2); +return x_4; +} +} LEAN_EXPORT uint8_t l_List_elem___at_List_decidablePerm___spec__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { diff --git a/stage0/stdlib/Init/Data/List/TakeDrop.c b/stage0/stdlib/Init/Data/List/TakeDrop.c index 49d26dbe99..63f93e044a 100644 --- a/stage0/stdlib/Init/Data/List/TakeDrop.c +++ b/stage0/stdlib/Init/Data/List/TakeDrop.c @@ -13,6 +13,7 @@ #ifdef __cplusplus extern "C" { #endif +LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__Option_getM_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__List_head_x3f__dropWhile__not_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__List_head_x3f__dropWhile__not_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__List_filterMap_match__1_splitter(lean_object*, lean_object*); @@ -26,10 +27,49 @@ LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__List_getLast_x3f LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__List_take_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_nat_dec_eq(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__List_getLast_x3f_match__1_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__Option_getM_match__1_splitter(lean_object*, lean_object*); lean_object* lean_nat_sub(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__List_filter_match__1_splitter(lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__List_take_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__List_filter_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__Option_getM_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__Option_getM_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_dec(x_3); +lean_inc(x_2); +return x_2; +} +else +{ +lean_object* x_4; lean_object* x_5; +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_1(x_3, x_4); +return x_5; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__Option_getM_match__1_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Init_Data_List_TakeDrop_0__Option_getM_match__1_splitter___rarg___boxed), 3, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__Option_getM_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l___private_Init_Data_List_TakeDrop_0__Option_getM_match__1_splitter___rarg(x_1, x_2, x_3); +lean_dec(x_2); +return x_4; +} +} LEAN_EXPORT lean_object* l___private_Init_Data_List_TakeDrop_0__List_take_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { diff --git a/stage0/stdlib/Init/Data/List/Zip.c b/stage0/stdlib/Init/Data/List/Zip.c index b056ff518e..e766b927e5 100644 --- a/stage0/stdlib/Init/Data/List/Zip.c +++ b/stage0/stdlib/Init/Data/List/Zip.c @@ -14,10 +14,33 @@ extern "C" { #endif LEAN_EXPORT lean_object* l___private_Init_Data_List_Zip_0__List_getElem_x3f__zipWithAll_match__1_splitter(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_Zip_0__instDecidableEqProd_match__2_splitter(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Zip_0__List_getElem_x3f__zipWith_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Zip_0__List_getElem_x3f__zipWithAll_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Zip_0__List_getElem_x3f__zipWith_match__1_splitter(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_List_Zip_0__List_getElem_x3f__zipWithAll_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_Zip_0__instDecidableEqProd_match__2_splitter___rarg(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_List_Zip_0__instDecidableEqProd_match__2_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_2(x_2, x_3, x_4); +return x_5; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_List_Zip_0__instDecidableEqProd_match__2_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = lean_alloc_closure((void*)(l___private_Init_Data_List_Zip_0__instDecidableEqProd_match__2_splitter___rarg), 2, 0); +return x_4; +} +} LEAN_EXPORT lean_object* l___private_Init_Data_List_Zip_0__List_getElem_x3f__zipWith_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { diff --git a/stage0/stdlib/Init/Data/Nat/Div.c b/stage0/stdlib/Init/Data/Nat/Div.c index aeff335117..83b720dab4 100644 --- a/stage0/stdlib/Init/Data/Nat/Div.c +++ b/stage0/stdlib/Init/Data/Nat/Div.c @@ -17,13 +17,17 @@ LEAN_EXPORT lean_object* l_Nat_modCore___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Nat_mod_inductionOn(lean_object*); LEAN_EXPORT lean_object* l_Nat_div_inductionOn(lean_object*); LEAN_EXPORT lean_object* l_Nat_div___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Nat_Div_0__Nat_mod_match__1_splitter(lean_object*); LEAN_EXPORT lean_object* l_Nat_instMod; +LEAN_EXPORT lean_object* l___private_Init_Data_Nat_Div_0__Nat_mod_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_nat_div(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Nat_div_inductionOn___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Nat_mod_inductionOn___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Nat_instDvd; +LEAN_EXPORT lean_object* l___private_Init_Data_Nat_Div_0__Nat_mod_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Nat_instDiv; lean_object* lean_nat_mod(lean_object*, lean_object*); +uint8_t lean_nat_dec_eq(lean_object*, lean_object*); uint8_t lean_nat_dec_lt(lean_object*, lean_object*); lean_object* lean_nat_mod(lean_object*, lean_object*); lean_object* lean_nat_sub(lean_object*, lean_object*); @@ -146,6 +150,47 @@ x_1 = l_Nat_instMod___closed__1; return x_1; } } +LEAN_EXPORT lean_object* l___private_Init_Data_Nat_Div_0__Nat_mod_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; uint8_t x_6; +x_5 = lean_unsigned_to_nat(0u); +x_6 = lean_nat_dec_eq(x_1, x_5); +if (x_6 == 0) +{ +lean_object* x_7; lean_object* x_8; lean_object* x_9; +lean_dec(x_3); +x_7 = lean_unsigned_to_nat(1u); +x_8 = lean_nat_sub(x_1, x_7); +x_9 = lean_apply_2(x_4, x_8, x_2); +return x_9; +} +else +{ +lean_object* x_10; +lean_dec(x_4); +x_10 = lean_apply_1(x_3, x_2); +return x_10; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Nat_Div_0__Nat_mod_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_Nat_Div_0__Nat_mod_match__1_splitter___rarg___boxed), 4, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Nat_Div_0__Nat_mod_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; +x_5 = l___private_Init_Data_Nat_Div_0__Nat_mod_match__1_splitter___rarg(x_1, x_2, x_3, x_4); +lean_dec(x_1); +return x_5; +} +} LEAN_EXPORT lean_object* l_Nat_mod_inductionOn___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { diff --git a/stage0/stdlib/Init/Data/Option/Instances.c b/stage0/stdlib/Init/Data/Option/Instances.c index 807be1362b..ba76a3dbd1 100644 --- a/stage0/stdlib/Init/Data/Option/Instances.c +++ b/stage0/stdlib/Init/Data/Option/Instances.c @@ -20,14 +20,18 @@ LEAN_EXPORT lean_object* l_Option_instDecidableForallForallMemOfDecidablePred___ LEAN_EXPORT lean_object* l_Option_instDecidableMemOfDecidableEq___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Option_decidable__eq__none___rarg(lean_object*); LEAN_EXPORT lean_object* l_Option_decidable__eq__none(lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Instances_0__Option_pmap_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Option_instForM___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Option_pbind(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Instances_0__Option_pmap_match__1_splitter(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Option_instDecidableMemOfDecidableEq(lean_object*); LEAN_EXPORT lean_object* l_Option_forM___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Option_decidable__eq__none___rarg___boxed(lean_object*); LEAN_EXPORT lean_object* l_Option_instForIn_x27InferInstanceMembership(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Instances_0__Option_pbind_match__1_splitter(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Option_instDecidableForallForallMemOfDecidablePred(lean_object*, lean_object*); lean_object* l___private_Init_Data_Option_Basic_0__Option_decEqOption____x40_Init_Data_Option_Basic___hyg_4____rarg(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Instances_0__Option_pbind_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Option_instForIn_x27InferInstanceMembership___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Option_instDecidableExistsAndMemOfDecidablePred(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Option_instForM(lean_object*, lean_object*); @@ -185,6 +189,36 @@ x_3 = lean_alloc_closure((void*)(l_Option_pbind___rarg), 2, 0); return x_3; } } +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Instances_0__Option_pbind_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_object* x_5; +lean_dec(x_4); +x_5 = lean_apply_1(x_3, x_2); +return x_5; +} +else +{ +lean_object* x_6; lean_object* x_7; +lean_dec(x_3); +x_6 = lean_ctor_get(x_1, 0); +lean_inc(x_6); +lean_dec(x_1); +x_7 = lean_apply_2(x_4, x_6, x_2); +return x_7; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Instances_0__Option_pbind_match__1_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = lean_alloc_closure((void*)(l___private_Init_Data_Option_Instances_0__Option_pbind_match__1_splitter___rarg), 4, 0); +return x_4; +} +} LEAN_EXPORT lean_object* l_Option_pmap___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -229,6 +263,36 @@ x_4 = lean_alloc_closure((void*)(l_Option_pmap___rarg), 3, 0); return x_4; } } +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Instances_0__Option_pmap_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_object* x_5; +lean_dec(x_4); +x_5 = lean_apply_1(x_3, lean_box(0)); +return x_5; +} +else +{ +lean_object* x_6; lean_object* x_7; +lean_dec(x_3); +x_6 = lean_ctor_get(x_1, 0); +lean_inc(x_6); +lean_dec(x_1); +x_7 = lean_apply_2(x_4, x_6, lean_box(0)); +return x_7; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Instances_0__Option_pmap_match__1_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = lean_alloc_closure((void*)(l___private_Init_Data_Option_Instances_0__Option_pmap_match__1_splitter___rarg), 4, 0); +return x_4; +} +} LEAN_EXPORT lean_object* l_Option_forM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { diff --git a/stage0/stdlib/Init/Data/Option/Lemmas.c b/stage0/stdlib/Init/Data/Option/Lemmas.c index 4486d0e0c0..7c861d22ed 100644 --- a/stage0/stdlib/Init/Data/Option/Lemmas.c +++ b/stage0/stdlib/Init/Data/Option/Lemmas.c @@ -13,6 +13,150 @@ #ifdef __cplusplus extern "C" { #endif +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_merge_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_merge_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_merge_match__1_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_isSome_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_isSome_match__1_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_bind_match__1_splitter(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_isSome_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_bind_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_isSome_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_dec(x_2); +lean_inc(x_3); +return x_3; +} +else +{ +lean_object* x_4; lean_object* x_5; +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_1(x_2, x_4); +return x_5; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_isSome_match__1_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Init_Data_Option_Lemmas_0__Option_isSome_match__1_splitter___rarg___boxed), 3, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_isSome_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l___private_Init_Data_Option_Lemmas_0__Option_isSome_match__1_splitter___rarg(x_1, x_2, x_3); +lean_dec(x_3); +return x_4; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_bind_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_object* x_5; +lean_dec(x_4); +x_5 = lean_apply_1(x_3, x_2); +return x_5; +} +else +{ +lean_object* x_6; lean_object* x_7; +lean_dec(x_3); +x_6 = lean_ctor_get(x_1, 0); +lean_inc(x_6); +lean_dec(x_1); +x_7 = lean_apply_2(x_4, x_6, x_2); +return x_7; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_bind_match__1_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = lean_alloc_closure((void*)(l___private_Init_Data_Option_Lemmas_0__Option_bind_match__1_splitter___rarg), 4, 0); +return x_4; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_merge_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_dec(x_6); +lean_dec(x_4); +if (lean_obj_tag(x_2) == 0) +{ +lean_dec(x_5); +lean_inc(x_3); +return x_3; +} +else +{ +lean_object* x_7; lean_object* x_8; +x_7 = lean_ctor_get(x_2, 0); +lean_inc(x_7); +lean_dec(x_2); +x_8 = lean_apply_1(x_5, x_7); +return x_8; +} +} +else +{ +lean_dec(x_5); +if (lean_obj_tag(x_2) == 0) +{ +lean_object* x_9; lean_object* x_10; +lean_dec(x_6); +x_9 = lean_ctor_get(x_1, 0); +lean_inc(x_9); +lean_dec(x_1); +x_10 = lean_apply_1(x_4, x_9); +return x_10; +} +else +{ +lean_object* x_11; lean_object* x_12; lean_object* x_13; +lean_dec(x_4); +x_11 = lean_ctor_get(x_1, 0); +lean_inc(x_11); +lean_dec(x_1); +x_12 = lean_ctor_get(x_2, 0); +lean_inc(x_12); +lean_dec(x_2); +x_13 = lean_apply_2(x_6, x_11, x_12); +return x_13; +} +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_merge_match__1_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Init_Data_Option_Lemmas_0__Option_merge_match__1_splitter___rarg___boxed), 6, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Option_Lemmas_0__Option_merge_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +x_7 = l___private_Init_Data_Option_Lemmas_0__Option_merge_match__1_splitter___rarg(x_1, x_2, x_3, x_4, x_5, x_6); +lean_dec(x_3); +return x_7; +} +} lean_object* initialize_Init_Data_Option_BasicAux(uint8_t builtin, lean_object*); lean_object* initialize_Init_Data_Option_Instances(uint8_t builtin, lean_object*); lean_object* initialize_Init_Classical(uint8_t builtin, lean_object*); diff --git a/stage0/stdlib/Init/Data/String/Basic.c b/stage0/stdlib/Init/Data/String/Basic.c index 6338664bab..b137ffb5f2 100644 --- a/stage0/stdlib/Init/Data/String/Basic.c +++ b/stage0/stdlib/Init/Data/String/Basic.c @@ -30,6 +30,7 @@ LEAN_EXPORT lean_object* l_String_join(lean_object*); LEAN_EXPORT lean_object* l_String_extract_go_u2082(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_splitAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Substring_atEnd___boxed(lean_object*, lean_object*); +LEAN_EXPORT uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_4022_(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Substring_takeRightWhileAux(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_intercalate_go___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_String_anyAux___at_String_isNat___spec__1(lean_object*, lean_object*, lean_object*); @@ -40,6 +41,7 @@ LEAN_EXPORT lean_object* l_Substring_toNat_x3f(lean_object*); LEAN_EXPORT lean_object* l_Substring_trimLeft(lean_object*); lean_object* lean_string_utf8_get_opt(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_instOfNatPos; +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_get_x3f_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_revFind___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Substring_takeWhileAux(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_get_x27___boxed(lean_object*, lean_object*, lean_object*); @@ -48,6 +50,7 @@ LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_utf8GetAux LEAN_EXPORT uint8_t l_String_Pos_isValid_go(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_toNat_x3f(lean_object*); LEAN_EXPORT lean_object* l_String_revPosOfAux___boxed(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_push_match__1_splitter(lean_object*); LEAN_EXPORT lean_object* l_String_Iterator_remainingToString___boxed(lean_object*); LEAN_EXPORT lean_object* l_String_append___boxed(lean_object*, lean_object*); LEAN_EXPORT uint8_t l_String_substrEq_loop(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -60,6 +63,7 @@ LEAN_EXPORT lean_object* l_String_Iterator_hasNext___boxed(lean_object*); LEAN_EXPORT lean_object* l_String_foldrAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_String_anyAux___at_String_all___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_revPosOf___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_append_match__1_splitter(lean_object*); LEAN_EXPORT lean_object* l_Substring_takeWhileAux___at_Substring_trimLeft___spec__1___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_set___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_mkIterator(lean_object*); @@ -106,6 +110,7 @@ LEAN_EXPORT lean_object* l_String_dropRightWhile___boxed(lean_object*, lean_obje lean_object* lean_string_push(lean_object*, uint32_t); LEAN_EXPORT lean_object* l_String_pushn(lean_object*, uint32_t, lean_object*); LEAN_EXPORT lean_object* l_String_substrEq___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_length_match__1_splitter(lean_object*); static lean_object* l_String_findLineStart___closed__1; LEAN_EXPORT lean_object* l_String_utf8GetAux___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Substring_next(lean_object*, lean_object*); @@ -151,6 +156,7 @@ LEAN_EXPORT lean_object* l_Substring_splitOn_loop(lean_object*, lean_object*, le LEAN_EXPORT lean_object* l_Substring_takeWhile(lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Substring_contains(lean_object*, uint32_t); LEAN_EXPORT lean_object* l_String_decLE___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__Substring_get_match__1_splitter(lean_object*); LEAN_EXPORT lean_object* l_Substring_get___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Substring_toIterator(lean_object*); LEAN_EXPORT uint8_t l_String_anyAux___at_Substring_contains___spec__1(uint32_t, lean_object*, lean_object*, lean_object*); @@ -159,12 +165,14 @@ LEAN_EXPORT uint8_t l_String_Iterator_hasNext(lean_object*); LEAN_EXPORT lean_object* l_String_mapAux___at_String_toLower___spec__1(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_Iterator_pos___boxed(lean_object*); LEAN_EXPORT lean_object* l_String_str___boxed(lean_object*, lean_object*); -LEAN_EXPORT uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_4020_(lean_object*, lean_object*); lean_object* lean_string_mk(lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_push_match__1_splitter___rarg(lean_object*, uint32_t, lean_object*); LEAN_EXPORT uint8_t l_String_all(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_firstDiffPos(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_takeWhile___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_utf8ByteSize_match__1_splitter(lean_object*); LEAN_EXPORT lean_object* l_String_anyAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__Substring_get_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Substring_any(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_foldlAux___at_String_toNat_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_String_startsWith(lean_object*, lean_object*); @@ -185,7 +193,6 @@ LEAN_EXPORT lean_object* l_Substring_foldr(lean_object*); LEAN_EXPORT lean_object* l_List_foldl___at_String_join___spec__1(lean_object*, lean_object*); LEAN_EXPORT uint8_t l_String_findLineStart___lambda__1(uint32_t); LEAN_EXPORT lean_object* l_String_find___boxed(lean_object*, lean_object*); -LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_4020____boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_utf8GetAux_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_dropWhile(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_foldlAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -216,11 +223,13 @@ LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__Substring_nextn_m LEAN_EXPORT lean_object* l_String_instLT; LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_utf8ByteSize_go_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Substring_prev(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_set_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_toUpper(lean_object*); LEAN_EXPORT lean_object* l_Substring_dropRight(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_Iterator_extract___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_modify(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_revPosOf(lean_object*, uint32_t); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_push_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); uint8_t lean_string_is_valid_pos(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_Iterator_atEnd___boxed(lean_object*); LEAN_EXPORT lean_object* l_Substring_takeWhileAux___at_Substring_trimLeft___spec__1(lean_object*, lean_object*, lean_object*); @@ -234,6 +243,7 @@ LEAN_EXPORT lean_object* l_String_takeRightWhile(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_iter(lean_object*); LEAN_EXPORT lean_object* l_String_Iterator_nextn(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_List_foldl___at_String_join___spec__1___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_get_x3f_match__1_splitter(lean_object*); LEAN_EXPORT uint8_t l_String_any(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__Substring_nextn_match__1_splitter(lean_object*); LEAN_EXPORT lean_object* l_String_Iterator_forward(lean_object*, lean_object*); @@ -277,6 +287,7 @@ LEAN_EXPORT lean_object* l_Substring_drop(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Substring_prevn(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Substring_foldr___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Substring_prev___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_utf8ByteSize_match__1_splitter___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_dropWhile___boxed(lean_object*, lean_object*); LEAN_EXPORT uint8_t l_String_substrEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_nextWhile(lean_object*, lean_object*, lean_object*); @@ -298,8 +309,10 @@ LEAN_EXPORT lean_object* l_String_posOf___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_utf8PrevAux___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_isEmpty___boxed(lean_object*); LEAN_EXPORT lean_object* l_String_intercalate(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_length_match__1_splitter___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_nextUntil___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_offsetOfPos___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_4022____boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_offsetOfPos(lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Substring_beq(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_capitalize(lean_object*); @@ -312,6 +325,7 @@ LEAN_EXPORT lean_object* l_String_Pos_min___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_posOf(lean_object*, uint32_t); LEAN_EXPORT lean_object* l_String_utf8GetAux_x3f(lean_object*, lean_object*, lean_object*); static lean_object* l_Substring_hasBeq___closed__1; +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_set_match__1_splitter___rarg(lean_object*, lean_object*, uint32_t, lean_object*); LEAN_EXPORT uint8_t l_String_Iterator_atEnd(lean_object*); LEAN_EXPORT lean_object* l_Substring_takeWhileAux___at_String_nextUntil___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_trimRight(lean_object*); @@ -322,6 +336,7 @@ LEAN_EXPORT lean_object* l_String_mapAux___at_String_toUpper___spec__1(lean_obje LEAN_EXPORT lean_object* l_String_trimLeft(lean_object*); LEAN_EXPORT lean_object* l_Substring_isEmpty___boxed(lean_object*); LEAN_EXPORT lean_object* l_Substring_splitOn(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_append_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_splitOn___boxed(lean_object*, lean_object*); uint8_t lean_nat_dec_le(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Substring_toIterator___boxed(lean_object*); @@ -330,6 +345,7 @@ LEAN_EXPORT lean_object* l_String_nextWhile___boxed(lean_object*, lean_object*, LEAN_EXPORT lean_object* l_String_findLineStart___lambda__1___boxed(lean_object*); lean_object* lean_nat_add(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_Iterator_setCurr(lean_object*, uint32_t); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_set_match__1_splitter(lean_object*); LEAN_EXPORT lean_object* l_Substring_toString(lean_object*); LEAN_EXPORT lean_object* l_Substring_foldl___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_foldl___rarg(lean_object*, lean_object*, lean_object*); @@ -950,6 +966,23 @@ x_2 = lean_alloc_closure((void*)(l___private_Init_Data_String_Basic_0__String_ut return x_2; } } +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_get_x3f_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; lean_object* x_5; +x_4 = lean_string_data(x_1); +x_5 = lean_apply_2(x_3, x_4, x_2); +return x_5; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_get_x3f_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_String_Basic_0__String_get_x3f_match__1_splitter___rarg), 3, 0); +return x_2; +} +} LEAN_EXPORT lean_object* l_String_posOfAux(lean_object* x_1, uint32_t x_2, lean_object* x_3, lean_object* x_4) { _start: { @@ -1919,7 +1952,7 @@ lean_dec(x_1); return x_3; } } -LEAN_EXPORT uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_4020_(lean_object* x_1, lean_object* x_2) { +LEAN_EXPORT uint8_t l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_4022_(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7; @@ -1942,11 +1975,11 @@ return x_9; } } } -LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_4020____boxed(lean_object* x_1, lean_object* x_2) { +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_4022____boxed(lean_object* x_1, lean_object* x_2) { _start: { uint8_t x_3; lean_object* x_4; -x_3 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_4020_(x_1, x_2); +x_3 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_4022_(x_1, x_2); lean_dec(x_2); lean_dec(x_1); x_4 = lean_box(x_3); @@ -1957,7 +1990,7 @@ LEAN_EXPORT uint8_t l_String_instDecidableEqIterator(lean_object* x_1, lean_obje _start: { uint8_t x_3; -x_3 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_4020_(x_1, x_2); +x_3 = l___private_Init_Data_String_Basic_0__String_decEqIterator____x40_Init_Data_String_Basic___hyg_4022_(x_1, x_2); return x_3; } } @@ -2881,6 +2914,68 @@ x_5 = lean_box(x_4); return x_5; } } +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_length_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; +x_3 = lean_string_data(x_1); +x_4 = lean_apply_1(x_2, x_3); +return x_4; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_length_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_String_Basic_0__String_length_match__1_splitter___rarg), 2, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_set_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, uint32_t x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; lean_object* x_6; lean_object* x_7; +x_5 = lean_string_data(x_1); +x_6 = lean_box_uint32(x_3); +x_7 = lean_apply_3(x_4, x_5, x_2, x_6); +return x_7; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_set_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_String_Basic_0__String_set_match__1_splitter___rarg___boxed), 4, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_set_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +uint32_t x_5; lean_object* x_6; +x_5 = lean_unbox_uint32(x_3); +lean_dec(x_3); +x_6 = l___private_Init_Data_String_Basic_0__String_set_match__1_splitter___rarg(x_1, x_2, x_5, x_4); +return x_6; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_utf8ByteSize_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; +x_3 = lean_string_data(x_1); +x_4 = lean_apply_1(x_2, x_3); +return x_4; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_utf8ByteSize_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_String_Basic_0__String_utf8ByteSize_match__1_splitter___rarg), 2, 0); +return x_2; +} +} LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_utf8ByteSize_go_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -3546,6 +3641,29 @@ lean_dec(x_1); return x_3; } } +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__Substring_get_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 1); +lean_inc(x_5); +x_6 = lean_ctor_get(x_1, 2); +lean_inc(x_6); +lean_dec(x_1); +x_7 = lean_apply_4(x_3, x_4, x_5, x_6, x_2); +return x_7; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__Substring_get_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_String_Basic_0__Substring_get_match__1_splitter___rarg), 3, 0); +return x_2; +} +} LEAN_EXPORT lean_object* l_Substring_prev(lean_object* x_1, lean_object* x_2) { _start: { @@ -6159,6 +6277,34 @@ x_3 = l_Char_toString(x_2); return x_3; } } +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_push_match__1_splitter___rarg(lean_object* x_1, uint32_t x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_4 = lean_string_data(x_1); +x_5 = lean_box_uint32(x_2); +x_6 = lean_apply_2(x_3, x_4, x_5); +return x_6; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_push_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_String_Basic_0__String_push_match__1_splitter___rarg___boxed), 3, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_push_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint32_t x_4; lean_object* x_5; +x_4 = lean_unbox_uint32(x_2); +lean_dec(x_2); +x_5 = l___private_Init_Data_String_Basic_0__String_push_match__1_splitter___rarg(x_1, x_4, x_3); +return x_5; +} +} LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__Nat_fold_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { @@ -6200,6 +6346,24 @@ lean_dec(x_1); return x_5; } } +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_append_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_4 = lean_string_data(x_1); +x_5 = lean_string_data(x_2); +x_6 = lean_apply_2(x_3, x_4, x_5); +return x_6; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__String_append_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_String_Basic_0__String_append_match__1_splitter___rarg), 3, 0); +return x_2; +} +} LEAN_EXPORT lean_object* l___private_Init_Data_String_Basic_0__Substring_nextn_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { diff --git a/stage0/stdlib/Init/Data/String/Extra.c b/stage0/stdlib/Init/Data/String/Extra.c index 7fb717c610..a8666ab002 100644 --- a/stage0/stdlib/Init/Data/String/Extra.c +++ b/stage0/stdlib/Init/Data/String/Extra.c @@ -35,6 +35,7 @@ LEAN_EXPORT lean_object* l_String_fromUTF8_loop___boxed(lean_object*, lean_objec static lean_object* l_String_toNat_x21___closed__1; lean_object* l_String_Iterator_next(lean_object*); static lean_object* l_String___aux__Init__Data__String__Extra______macroRules__tacticDecreasing__trivial__1___closed__3; +LEAN_EXPORT lean_object* l___private_Init_Data_String_Extra_0__String_Iterator_remainingBytes_match__1_splitter___rarg(lean_object*, lean_object*); uint8_t lean_uint8_land(uint8_t, uint8_t); static lean_object* l_String_fromUTF8_x21___closed__2; uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*); @@ -94,11 +95,13 @@ lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_ LEAN_EXPORT lean_object* l_String___aux__Init__Data__String__Extra______macroRules__tacticDecreasing__trivial__1(lean_object*, lean_object*, lean_object*); uint8_t l_String_isNat(lean_object*); lean_object* lean_string_from_utf8_unchecked(lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Extra_0__ByteArray_size_match__1_splitter___rarg(lean_object*, lean_object*); static lean_object* l_String___aux__Init__Data__String__Extra______macroRules__tacticDecreasing__trivial__2___closed__4; static lean_object* l_String___aux__Init__Data__String__Extra______macroRules__tacticDecreasing__trivial__1___closed__20; LEAN_EXPORT lean_object* l___private_Init_Data_String_Extra_0__String_removeNumLeadingSpaces_consumeSpaces(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_validateUTF8___boxed(lean_object*); static lean_object* l_String___aux__Init__Data__String__Extra______macroRules__tacticDecreasing__trivial__1___closed__12; +lean_object* lean_byte_array_data(lean_object*); LEAN_EXPORT lean_object* l_String_toNat_x21___boxed(lean_object*); LEAN_EXPORT lean_object* l_String_fromUTF8_x21___boxed(lean_object*); static lean_object* l_String___aux__Init__Data__String__Extra______macroRules__tacticDecreasing__trivial__2___closed__5; @@ -109,6 +112,7 @@ uint8_t lean_nat_dec_eq(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_fromUTF8___boxed(lean_object*, lean_object*); static lean_object* l_String_toNat_x21___closed__4; uint8_t lean_nat_dec_lt(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Extra_0__ByteArray_size_match__1_splitter(lean_object*); uint8_t lean_uint32_dec_eq(uint32_t, uint32_t); lean_object* l_Lean_Syntax_node1(lean_object*, lean_object*, lean_object*); static lean_object* l_String___aux__Init__Data__String__Extra______macroRules__tacticDecreasing__trivial__1___closed__6; @@ -128,6 +132,7 @@ lean_object* lean_nat_sub(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_String_validateUTF8_loop(lean_object*, lean_object*); static lean_object* l_String___aux__Init__Data__String__Extra______macroRules__tacticDecreasing__trivial__1___closed__27; lean_object* lean_string_utf8_next_fast(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Data_String_Extra_0__String_Iterator_remainingBytes_match__1_splitter(lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_String_Extra_0__List_getLast_x3f_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_String_Extra_0__String_findLeadingSpacesSize_consumeSpaces(lean_object*, lean_object*, lean_object*); static lean_object* l_String___aux__Init__Data__String__Extra______macroRules__tacticDecreasing__trivial__1___closed__19; @@ -1042,6 +1047,23 @@ lean_dec(x_1); return x_2; } } +LEAN_EXPORT lean_object* l___private_Init_Data_String_Extra_0__ByteArray_size_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; +x_3 = lean_byte_array_data(x_1); +x_4 = lean_apply_1(x_2, x_3); +return x_4; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_String_Extra_0__ByteArray_size_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_String_Extra_0__ByteArray_size_match__1_splitter___rarg), 2, 0); +return x_2; +} +} LEAN_EXPORT lean_object* l___private_Init_Data_String_Extra_0__List_getLast_x3f_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -1091,6 +1113,27 @@ x_5 = lean_box(x_4); return x_5; } } +LEAN_EXPORT lean_object* l___private_Init_Data_String_Extra_0__String_Iterator_remainingBytes_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_2(x_2, x_3, x_4); +return x_5; +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_String_Extra_0__String_Iterator_remainingBytes_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Data_String_Extra_0__String_Iterator_remainingBytes_match__1_splitter___rarg), 2, 0); +return x_2; +} +} static lean_object* _init_l_String___aux__Init__Data__String__Extra______macroRules__tacticDecreasing__trivial__1___closed__1() { _start: { diff --git a/stage0/stdlib/Init/Omega/Constraint.c b/stage0/stdlib/Init/Omega/Constraint.c index 58919b7f6a..7331fa9513 100644 --- a/stage0/stdlib/Init/Omega/Constraint.c +++ b/stage0/stdlib/Init/Omega/Constraint.c @@ -101,8 +101,10 @@ LEAN_EXPORT lean_object* l___private_Init_Data_Option_Basic_0__Option_beqOption_ static lean_object* l___private_Init_Omega_Constraint_0__Lean_Omega_reprConstraint____x40_Init_Omega_Constraint___hyg_291____closed__10; lean_object* l_Int_neg___boxed(lean_object*); static lean_object* l___private_Init_Omega_Constraint_0__Lean_Omega_reprConstraint____x40_Init_Omega_Constraint___hyg_291____closed__7; +LEAN_EXPORT lean_object* l___private_Init_Omega_Constraint_0__Lean_Omega_Constraint_isImpossible_match__1_splitter(lean_object*); lean_object* l_Int_mul___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Omega_Constraint_scale(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Init_Omega_Constraint_0__Lean_Omega_Constraint_isImpossible_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Option_min___at_Lean_Omega_Constraint_combine___spec__2(lean_object*, lean_object*); lean_object* l_Repr_addAppParen(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Omega_tidy(lean_object*); @@ -1605,6 +1607,57 @@ x_3 = lean_box(x_2); return x_3; } } +LEAN_EXPORT lean_object* l___private_Init_Omega_Constraint_0__Lean_Omega_Constraint_isImpossible_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +if (lean_obj_tag(x_4) == 0) +{ +lean_object* x_5; +lean_dec(x_2); +x_5 = lean_apply_2(x_3, x_1, lean_box(0)); +return x_5; +} +else +{ +lean_object* x_6; +x_6 = lean_ctor_get(x_1, 1); +lean_inc(x_6); +if (lean_obj_tag(x_6) == 0) +{ +lean_object* x_7; +lean_dec(x_4); +lean_dec(x_2); +x_7 = lean_apply_2(x_3, x_1, lean_box(0)); +return x_7; +} +else +{ +lean_object* x_8; lean_object* x_9; lean_object* x_10; +lean_dec(x_3); +lean_dec(x_1); +x_8 = lean_ctor_get(x_4, 0); +lean_inc(x_8); +lean_dec(x_4); +x_9 = lean_ctor_get(x_6, 0); +lean_inc(x_9); +lean_dec(x_6); +x_10 = lean_apply_2(x_2, x_8, x_9); +return x_10; +} +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Omega_Constraint_0__Lean_Omega_Constraint_isImpossible_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Init_Omega_Constraint_0__Lean_Omega_Constraint_isImpossible_match__1_splitter___rarg), 3, 0); +return x_2; +} +} static lean_object* _init_l_Lean_Omega_Constraint_scale___closed__1() { _start: { diff --git a/stage0/stdlib/Init/WFTactics.c b/stage0/stdlib/Init/WFTactics.c index c1e4233b6e..f614771e70 100644 --- a/stage0/stdlib/Init/WFTactics.c +++ b/stage0/stdlib/Init/WFTactics.c @@ -15,6 +15,7 @@ extern "C" { #endif static lean_object* l_tacticDecreasing__trivial__pre__omega___closed__1; static lean_object* l___aux__Init__WFTactics______macroRules__tacticDecreasing__trivial__pre__omega__1___closed__11; +static lean_object* l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__19; static lean_object* l___aux__Init__WFTactics______macroRules__tacticSimp__wf__1___closed__61; static lean_object* l___aux__Init__WFTactics______macroRules__tacticDecreasing__trivial__1___closed__2; static lean_object* l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__6; @@ -244,6 +245,7 @@ static lean_object* l___aux__Init__WFTactics______macroRules__tacticDecreasing__ static lean_object* l_tacticDecreasing__trivial__pre__omega___closed__4; static lean_object* l___aux__Init__WFTactics______macroRules__tacticDecreasing__with____1___closed__13; static lean_object* l___aux__Init__WFTactics______macroRules__tacticSimp__wf__1___closed__43; +static lean_object* l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__17; static lean_object* l___aux__Init__WFTactics______macroRules__tacticSimp__wf__1___closed__80; static lean_object* l___aux__Init__WFTactics______macroRules__tacticSimp__wf__1___closed__30; static lean_object* l_tacticDecreasing__trivial___closed__5; @@ -283,6 +285,7 @@ static lean_object* l___aux__Init__WFTactics______macroRules__tacticSimp__wf__1_ static lean_object* l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__11; LEAN_EXPORT lean_object* l_tacticSimp__wf; static lean_object* l_tacticDecreasing__tactic___closed__3; +static lean_object* l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__18; static lean_object* _init_l_tacticSimp__wf___closed__1() { _start: { @@ -1861,8 +1864,35 @@ return x_3; static lean_object* _init_l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__16() { _start: { +lean_object* x_1; +x_1 = lean_mk_string_unchecked("reduceCtorEq", 12, 12); +return x_1; +} +} +static lean_object* _init_l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__17() { +_start: +{ lean_object* x_1; lean_object* x_2; -x_1 = lean_unsigned_to_nat(15u); +x_1 = l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__16; +x_2 = l_String_toSubstring_x27(x_1); +return x_2; +} +} +static lean_object* _init_l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__18() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__16; +x_3 = l_Lean_Name_str___override(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__19() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = lean_unsigned_to_nat(17u); x_2 = lean_mk_empty_array_with_capacity(x_1); return x_2; } @@ -1885,7 +1915,7 @@ return x_7; } else { -lean_object* x_8; uint8_t x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; +lean_object* x_8; uint8_t x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; lean_object* x_154; x_8 = lean_ctor_get(x_2, 5); lean_inc(x_8); x_9 = 0; @@ -2157,6 +2187,8 @@ lean_inc_n(x_25, 2); lean_inc(x_10); x_118 = l_Lean_Syntax_node3(x_10, x_81, x_25, x_25, x_117); x_119 = l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__13; +lean_inc(x_11); +lean_inc(x_12); x_120 = l_Lean_addMacroScope(x_12, x_119, x_11); x_121 = l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__12; x_122 = l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__15; @@ -2169,47 +2201,62 @@ lean_ctor_set(x_123, 3, x_122); lean_inc_n(x_25, 2); lean_inc(x_10); x_124 = l_Lean_Syntax_node3(x_10, x_81, x_25, x_25, x_123); -x_125 = l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__16; -x_126 = lean_array_push(x_125, x_82); -lean_inc(x_41); -x_127 = lean_array_push(x_126, x_41); -x_128 = lean_array_push(x_127, x_88); -lean_inc(x_41); -x_129 = lean_array_push(x_128, x_41); -x_130 = lean_array_push(x_129, x_94); -lean_inc(x_41); -x_131 = lean_array_push(x_130, x_41); -x_132 = lean_array_push(x_131, x_100); -lean_inc(x_41); -x_133 = lean_array_push(x_132, x_41); -x_134 = lean_array_push(x_133, x_106); -lean_inc(x_41); -x_135 = lean_array_push(x_134, x_41); -x_136 = lean_array_push(x_135, x_112); -lean_inc(x_41); -x_137 = lean_array_push(x_136, x_41); -x_138 = lean_array_push(x_137, x_118); -x_139 = lean_array_push(x_138, x_41); -x_140 = lean_array_push(x_139, x_124); +x_125 = l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__18; +x_126 = l_Lean_addMacroScope(x_12, x_125, x_11); +x_127 = l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__17; lean_inc(x_10); -x_141 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_141, 0, x_10); -lean_ctor_set(x_141, 1, x_23); -lean_ctor_set(x_141, 2, x_140); -x_142 = l___aux__Init__WFTactics______macroRules__tacticSimp__wf__1___closed__103; +x_128 = lean_alloc_ctor(3, 4, 0); +lean_ctor_set(x_128, 0, x_10); +lean_ctor_set(x_128, 1, x_127); +lean_ctor_set(x_128, 2, x_126); +lean_ctor_set(x_128, 3, x_28); +lean_inc_n(x_25, 2); lean_inc(x_10); -x_143 = lean_alloc_ctor(2, 2, 0); -lean_ctor_set(x_143, 0, x_10); -lean_ctor_set(x_143, 1, x_142); +x_129 = l_Lean_Syntax_node3(x_10, x_81, x_25, x_25, x_128); +x_130 = l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__19; +x_131 = lean_array_push(x_130, x_82); +lean_inc(x_41); +x_132 = lean_array_push(x_131, x_41); +x_133 = lean_array_push(x_132, x_88); +lean_inc(x_41); +x_134 = lean_array_push(x_133, x_41); +x_135 = lean_array_push(x_134, x_94); +lean_inc(x_41); +x_136 = lean_array_push(x_135, x_41); +x_137 = lean_array_push(x_136, x_100); +lean_inc(x_41); +x_138 = lean_array_push(x_137, x_41); +x_139 = lean_array_push(x_138, x_106); +lean_inc(x_41); +x_140 = lean_array_push(x_139, x_41); +x_141 = lean_array_push(x_140, x_112); +lean_inc(x_41); +x_142 = lean_array_push(x_141, x_41); +x_143 = lean_array_push(x_142, x_118); +lean_inc(x_41); +x_144 = lean_array_push(x_143, x_41); +x_145 = lean_array_push(x_144, x_124); +x_146 = lean_array_push(x_145, x_41); +x_147 = lean_array_push(x_146, x_129); lean_inc(x_10); -x_144 = l_Lean_Syntax_node3(x_10, x_23, x_75, x_141, x_143); -x_145 = l___aux__Init__WFTactics______macroRules__tacticSimp__wf__1___closed__14; +x_148 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_148, 0, x_10); +lean_ctor_set(x_148, 1, x_23); +lean_ctor_set(x_148, 2, x_147); +x_149 = l___aux__Init__WFTactics______macroRules__tacticSimp__wf__1___closed__103; +lean_inc(x_10); +x_150 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_150, 0, x_10); +lean_ctor_set(x_150, 1, x_149); +lean_inc(x_10); +x_151 = l_Lean_Syntax_node3(x_10, x_23, x_75, x_148, x_150); +x_152 = l___aux__Init__WFTactics______macroRules__tacticSimp__wf__1___closed__14; lean_inc(x_25); -x_146 = l_Lean_Syntax_node6(x_10, x_145, x_14, x_70, x_25, x_73, x_144, x_25); -x_147 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_147, 0, x_146); -lean_ctor_set(x_147, 1, x_3); -return x_147; +x_153 = l_Lean_Syntax_node6(x_10, x_152, x_14, x_70, x_25, x_73, x_151, x_25); +x_154 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_154, 0, x_153); +lean_ctor_set(x_154, 1, x_3); +return x_154; } } } @@ -4508,6 +4555,12 @@ l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__15 = _ini lean_mark_persistent(l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__15); l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__16 = _init_l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__16(); lean_mark_persistent(l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__16); +l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__17 = _init_l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__17(); +lean_mark_persistent(l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__17); +l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__18 = _init_l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__18(); +lean_mark_persistent(l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__18); +l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__19 = _init_l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__19(); +lean_mark_persistent(l___aux__Init__WFTactics______macroRules__tacticClean__wf__1___closed__19); l_tacticDecreasing__trivial___closed__1 = _init_l_tacticDecreasing__trivial___closed__1(); lean_mark_persistent(l_tacticDecreasing__trivial___closed__1); l_tacticDecreasing__trivial___closed__2 = _init_l_tacticDecreasing__trivial___closed__2(); diff --git a/stage0/stdlib/Lake/Build/Key.c b/stage0/stdlib/Lake/Build/Key.c index bb97267f01..fa25e00d87 100644 --- a/stage0/stdlib/Lake/Build/Key.c +++ b/stage0/stdlib/Lake/Build/Key.c @@ -22,18 +22,24 @@ LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_ma LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_decEqBuildKey____x40_Lake_Build_Key___hyg_325____boxed(lean_object*, lean_object*); uint64_t lean_uint64_mix_hash(uint64_t, uint64_t); lean_object* l_Lean_Name_toString(lean_object*, uint8_t); +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0____private_Lake_Build_Key_0__Lake_reprBuildKey_match__1_splitter____x40_Lake_Build_Key___hyg_92____rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lake_Build_Key_0__Lake_reprBuildKey____x40_Lake_Build_Key___hyg_92____closed__8; static lean_object* l___private_Lake_Build_Key_0__Lake_reprBuildKey____x40_Lake_Build_Key___hyg_92____closed__9; static lean_object* l___private_Lake_Build_Key_0__Lake_reprBuildKey____x40_Lake_Build_Key___hyg_92____closed__14; LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_reprBuildKey____x40_Lake_Build_Key___hyg_92____boxed(lean_object*, lean_object*); static lean_object* l___private_Lake_Build_Key_0__Lake_reprBuildKey____x40_Lake_Build_Key___hyg_92____closed__12; +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0____private_Lake_Build_Key_0__Lake_reprBuildKey_match__1_splitter____x40_Lake_Build_Key___hyg_92_(lean_object*); +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__4_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lake_Build_Key_0__Lake_reprBuildKey____x40_Lake_Build_Key___hyg_92____closed__3; LEAN_EXPORT lean_object* l_Lake_BuildKey_quickCmp___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__5_splitter(lean_object*); static lean_object* l_Lake_instInhabitedBuildKey___closed__1; +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__2_splitter(lean_object*); static lean_object* l_Lake_BuildKey_instLawfulCmpEqQuickCmp___closed__2; lean_object* lean_nat_to_int(lean_object*); LEAN_EXPORT lean_object* l_Lake_instReprBuildKey; static lean_object* l___private_Lake_Build_Key_0__Lake_reprBuildKey____x40_Lake_Build_Key___hyg_92____closed__1; +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__3_splitter(lean_object*); static lean_object* l_Lake_BuildKey_instLawfulCmpEqQuickCmp___closed__1; LEAN_EXPORT uint8_t l___private_Lake_Build_Key_0__Lake_decEqBuildKey____x40_Lake_Build_Key___hyg_325_(lean_object*, lean_object*); lean_object* l_Lean_Name_num___override(lean_object*, lean_object*); @@ -46,8 +52,10 @@ lean_object* l_Lean_Name_str___override(lean_object*, lean_object*); static lean_object* l_Lake_BuildKey_toString___closed__1; LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_reprBuildKey____x40_Lake_Build_Key___hyg_92_(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lake_instInhabitedBuildKey; +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__5_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lake_instHashableBuildKey; LEAN_EXPORT lean_object* l_Lake_instDecidableEqBuildKey___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__3_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lake_BuildKey_instToString(lean_object*); static lean_object* l_Lake_BuildKey_toString___closed__3; static lean_object* l___private_Lake_Build_Key_0__Lake_reprBuildKey____x40_Lake_Build_Key___hyg_92____closed__11; @@ -64,7 +72,9 @@ lean_object* lean_string_append(lean_object*, lean_object*); uint8_t lean_nat_dec_le(lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Lake_BuildKey_quickCmp(lean_object*, lean_object*); static lean_object* l___private_Lake_Build_Key_0__Lake_reprBuildKey____x40_Lake_Build_Key___hyg_92____closed__13; +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__4_splitter(lean_object*); LEAN_EXPORT uint8_t l_Lake_instDecidableEqBuildKey(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__2_splitter___rarg(lean_object*, lean_object*, lean_object*); static lean_object* l_Lake_BuildKey_toString___closed__4; static lean_object* l___private_Lake_Build_Key_0__Lake_reprBuildKey____x40_Lake_Build_Key___hyg_92____closed__5; static lean_object* l_Lake_BuildKey_toString___closed__5; @@ -1384,6 +1394,243 @@ lean_dec(x_2); return x_5; } } +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0____private_Lake_Build_Key_0__Lake_reprBuildKey_match__1_splitter____x40_Lake_Build_Key___hyg_92____rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +_start: +{ +switch (lean_obj_tag(x_1)) { +case 0: +{ +lean_object* x_6; lean_object* x_7; lean_object* x_8; +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +x_6 = lean_ctor_get(x_1, 0); +lean_inc(x_6); +x_7 = lean_ctor_get(x_1, 1); +lean_inc(x_7); +lean_dec(x_1); +x_8 = lean_apply_2(x_2, x_6, x_7); +return x_8; +} +case 1: +{ +lean_object* x_9; lean_object* x_10; lean_object* x_11; +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_2); +x_9 = lean_ctor_get(x_1, 0); +lean_inc(x_9); +x_10 = lean_ctor_get(x_1, 1); +lean_inc(x_10); +lean_dec(x_1); +x_11 = lean_apply_2(x_3, x_9, x_10); +return x_11; +} +case 2: +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; +lean_dec(x_5); +lean_dec(x_3); +lean_dec(x_2); +x_12 = lean_ctor_get(x_1, 0); +lean_inc(x_12); +x_13 = lean_ctor_get(x_1, 1); +lean_inc(x_13); +x_14 = lean_ctor_get(x_1, 2); +lean_inc(x_14); +lean_dec(x_1); +x_15 = lean_apply_3(x_4, x_12, x_13, x_14); +return x_15; +} +default: +{ +lean_object* x_16; lean_object* x_17; lean_object* x_18; +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +x_16 = lean_ctor_get(x_1, 0); +lean_inc(x_16); +x_17 = lean_ctor_get(x_1, 1); +lean_inc(x_17); +lean_dec(x_1); +x_18 = lean_apply_2(x_5, x_16, x_17); +return x_18; +} +} +} +} +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0____private_Lake_Build_Key_0__Lake_reprBuildKey_match__1_splitter____x40_Lake_Build_Key___hyg_92_(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Lake_Build_Key_0____private_Lake_Build_Key_0__Lake_reprBuildKey_match__1_splitter____x40_Lake_Build_Key___hyg_92____rarg), 5, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__2_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; +lean_dec(x_3); +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 1); +lean_inc(x_5); +lean_dec(x_1); +x_6 = lean_apply_2(x_2, x_4, x_5); +return x_6; +} +else +{ +lean_object* x_7; +lean_dec(x_2); +x_7 = lean_apply_2(x_3, x_1, lean_box(0)); +return x_7; +} +} +} +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__2_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__2_splitter___rarg), 3, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__3_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +switch (lean_obj_tag(x_1)) { +case 0: +{ +lean_object* x_5; lean_object* x_6; lean_object* x_7; +lean_dec(x_4); +lean_dec(x_3); +x_5 = lean_ctor_get(x_1, 0); +lean_inc(x_5); +x_6 = lean_ctor_get(x_1, 1); +lean_inc(x_6); +lean_dec(x_1); +x_7 = lean_apply_2(x_2, x_5, x_6); +return x_7; +} +case 1: +{ +lean_object* x_8; lean_object* x_9; lean_object* x_10; +lean_dec(x_4); +lean_dec(x_2); +x_8 = lean_ctor_get(x_1, 0); +lean_inc(x_8); +x_9 = lean_ctor_get(x_1, 1); +lean_inc(x_9); +lean_dec(x_1); +x_10 = lean_apply_2(x_3, x_8, x_9); +return x_10; +} +default: +{ +lean_object* x_11; +lean_dec(x_3); +lean_dec(x_2); +x_11 = lean_apply_3(x_4, x_1, lean_box(0), lean_box(0)); +return x_11; +} +} +} +} +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__3_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__3_splitter___rarg), 4, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__4_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +switch (lean_obj_tag(x_1)) { +case 2: +{ +lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; +lean_dec(x_4); +lean_dec(x_2); +x_5 = lean_ctor_get(x_1, 0); +lean_inc(x_5); +x_6 = lean_ctor_get(x_1, 1); +lean_inc(x_6); +x_7 = lean_ctor_get(x_1, 2); +lean_inc(x_7); +lean_dec(x_1); +x_8 = lean_apply_3(x_3, x_5, x_6, x_7); +return x_8; +} +case 3: +{ +lean_object* x_9; lean_object* x_10; lean_object* x_11; +lean_dec(x_4); +lean_dec(x_3); +x_9 = lean_ctor_get(x_1, 0); +lean_inc(x_9); +x_10 = lean_ctor_get(x_1, 1); +lean_inc(x_10); +lean_dec(x_1); +x_11 = lean_apply_2(x_2, x_9, x_10); +return x_11; +} +default: +{ +lean_object* x_12; +lean_dec(x_3); +lean_dec(x_2); +x_12 = lean_apply_3(x_4, x_1, lean_box(0), lean_box(0)); +return x_12; +} +} +} +} +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__4_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__4_splitter___rarg), 4, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__5_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 3) +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; +lean_dec(x_3); +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 1); +lean_inc(x_5); +lean_dec(x_1); +x_6 = lean_apply_2(x_2, x_4, x_5); +return x_6; +} +else +{ +lean_object* x_7; +lean_dec(x_2); +x_7 = lean_apply_2(x_3, x_1, lean_box(0)); +return x_7; +} +} +} +LEAN_EXPORT lean_object* l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__5_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Lake_Build_Key_0__Lake_BuildKey_quickCmp_match__5_splitter___rarg), 3, 0); +return x_2; +} +} static lean_object* _init_l_Lake_BuildKey_instLawfulCmpEqQuickCmp___closed__1() { _start: { diff --git a/stage0/stdlib/Lean/Elab/GuardMsgs.c b/stage0/stdlib/Lean/Elab/GuardMsgs.c index 4ea4c53e44..8586c0234b 100644 --- a/stage0/stdlib/Lean/Elab/GuardMsgs.c +++ b/stage0/stdlib/Lean/Elab/GuardMsgs.c @@ -9080,7 +9080,7 @@ static lean_object* _init_l_Lean_Elab_Tactic_GuardMsgs_elabGuardMsgs___lambda__1 _start: { lean_object* x_1; -x_1 = lean_mk_string_unchecked("❌ Docstring on `#guard_msgs` does not match generated message:\n\n", 66, 64); +x_1 = lean_mk_string_unchecked("❌️ Docstring on `#guard_msgs` does not match generated message:\n\n", 69, 65); return x_1; } } diff --git a/stage0/stdlib/Lean/Elab/Tactic.c b/stage0/stdlib/Lean/Elab/Tactic.c index b404c6dfac..fa62cabeb0 100644 --- a/stage0/stdlib/Lean/Elab/Tactic.c +++ b/stage0/stdlib/Lean/Elab/Tactic.c @@ -1,6 +1,6 @@ // Lean compiler output // Module: Lean.Elab.Tactic -// Imports: Lean.Elab.Term Lean.Elab.Tactic.Basic Lean.Elab.Tactic.ElabTerm Lean.Elab.Tactic.Induction Lean.Elab.Tactic.Generalize Lean.Elab.Tactic.Injection Lean.Elab.Tactic.Match Lean.Elab.Tactic.Rewrite Lean.Elab.Tactic.Location Lean.Elab.Tactic.SimpTrace Lean.Elab.Tactic.Simp Lean.Elab.Tactic.Simproc Lean.Elab.Tactic.BuiltinTactic Lean.Elab.Tactic.Split Lean.Elab.Tactic.Conv Lean.Elab.Tactic.Delta Lean.Elab.Tactic.Meta Lean.Elab.Tactic.Unfold Lean.Elab.Tactic.Cache Lean.Elab.Tactic.Calc Lean.Elab.Tactic.Congr Lean.Elab.Tactic.Guard Lean.Elab.Tactic.RCases Lean.Elab.Tactic.Repeat Lean.Elab.Tactic.Ext Lean.Elab.Tactic.Change Lean.Elab.Tactic.FalseOrByContra Lean.Elab.Tactic.Omega Lean.Elab.Tactic.Simpa Lean.Elab.Tactic.NormCast Lean.Elab.Tactic.Symm Lean.Elab.Tactic.SolveByElim Lean.Elab.Tactic.LibrarySearch Lean.Elab.Tactic.ShowTerm Lean.Elab.Tactic.Rfl Lean.Elab.Tactic.Rewrites Lean.Elab.Tactic.DiscrTreeKey Lean.Elab.Tactic.BVDecide +// Imports: Lean.Elab.Term Lean.Elab.Tactic.Basic Lean.Elab.Tactic.ElabTerm Lean.Elab.Tactic.Induction Lean.Elab.Tactic.Generalize Lean.Elab.Tactic.Injection Lean.Elab.Tactic.Match Lean.Elab.Tactic.Rewrite Lean.Elab.Tactic.Location Lean.Elab.Tactic.SimpTrace Lean.Elab.Tactic.Simp Lean.Elab.Tactic.Simproc Lean.Elab.Tactic.BuiltinTactic Lean.Elab.Tactic.Split Lean.Elab.Tactic.Conv Lean.Elab.Tactic.Delta Lean.Elab.Tactic.Meta Lean.Elab.Tactic.Unfold Lean.Elab.Tactic.Cache Lean.Elab.Tactic.Calc Lean.Elab.Tactic.Congr Lean.Elab.Tactic.Guard Lean.Elab.Tactic.RCases Lean.Elab.Tactic.Repeat Lean.Elab.Tactic.Ext Lean.Elab.Tactic.Change Lean.Elab.Tactic.FalseOrByContra Lean.Elab.Tactic.Omega Lean.Elab.Tactic.Simpa Lean.Elab.Tactic.NormCast Lean.Elab.Tactic.Symm Lean.Elab.Tactic.SolveByElim Lean.Elab.Tactic.LibrarySearch Lean.Elab.Tactic.ShowTerm Lean.Elab.Tactic.Rfl Lean.Elab.Tactic.Rewrites Lean.Elab.Tactic.DiscrTreeKey Lean.Elab.Tactic.BVDecide Lean.Elab.Tactic.BoolToPropSimps #include #if defined(__clang__) #pragma clang diagnostic ignored "-Wunused-parameter" @@ -51,6 +51,7 @@ lean_object* initialize_Lean_Elab_Tactic_Rfl(uint8_t builtin, lean_object*); lean_object* initialize_Lean_Elab_Tactic_Rewrites(uint8_t builtin, lean_object*); lean_object* initialize_Lean_Elab_Tactic_DiscrTreeKey(uint8_t builtin, lean_object*); lean_object* initialize_Lean_Elab_Tactic_BVDecide(uint8_t builtin, lean_object*); +lean_object* initialize_Lean_Elab_Tactic_BoolToPropSimps(uint8_t builtin, lean_object*); static bool _G_initialized = false; LEAN_EXPORT lean_object* initialize_Lean_Elab_Tactic(uint8_t builtin, lean_object* w) { lean_object * res; @@ -170,6 +171,9 @@ lean_dec_ref(res); res = initialize_Lean_Elab_Tactic_BVDecide(builtin, lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +res = initialize_Lean_Elab_Tactic_BoolToPropSimps(builtin, lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); return lean_io_result_mk_ok(lean_box(0)); } #ifdef __cplusplus diff --git a/stage0/stdlib/Lean/Elab/Tactic/BoolToPropSimps.c b/stage0/stdlib/Lean/Elab/Tactic/BoolToPropSimps.c new file mode 100644 index 0000000000..251e924fb1 --- /dev/null +++ b/stage0/stdlib/Lean/Elab/Tactic/BoolToPropSimps.c @@ -0,0 +1,83 @@ +// Lean compiler output +// Module: Lean.Elab.Tactic.BoolToPropSimps +// Imports: Lean.Meta.Tactic.Simp.Attr +#include +#if defined(__clang__) +#pragma clang diagnostic ignored "-Wunused-parameter" +#pragma clang diagnostic ignored "-Wunused-label" +#elif defined(__GNUC__) && !defined(__CLANG__) +#pragma GCC diagnostic ignored "-Wunused-parameter" +#pragma GCC diagnostic ignored "-Wunused-label" +#pragma GCC diagnostic ignored "-Wunused-but-set-variable" +#endif +#ifdef __cplusplus +extern "C" { +#endif +LEAN_EXPORT lean_object* l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3_(lean_object*); +static lean_object* l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__3; +LEAN_EXPORT lean_object* l_boolToPropSimps; +lean_object* l_Lean_Name_str___override(lean_object*, lean_object*); +lean_object* l_Lean_Meta_registerSimpAttr(lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__1; +static lean_object* l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__2; +static lean_object* _init_l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_unchecked("boolToPropSimps", 15, 15); +return x_1; +} +} +static lean_object* _init_l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__1; +x_3 = l_Lean_Name_str___override(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_unchecked("simp lemmas converting boolean expressions in terms of `decide` into propositional statements", 93, 93); +return x_1; +} +} +LEAN_EXPORT lean_object* l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3_(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_2 = l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__2; +x_3 = l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__3; +x_4 = l_Lean_Meta_registerSimpAttr(x_2, x_3, x_2, x_1); +return x_4; +} +} +lean_object* initialize_Lean_Meta_Tactic_Simp_Attr(uint8_t builtin, lean_object*); +static bool _G_initialized = false; +LEAN_EXPORT lean_object* initialize_Lean_Elab_Tactic_BoolToPropSimps(uint8_t builtin, lean_object* w) { +lean_object * res; +if (_G_initialized) return lean_io_result_mk_ok(lean_box(0)); +_G_initialized = true; +res = initialize_Lean_Meta_Tactic_Simp_Attr(builtin, lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__1 = _init_l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__1(); +lean_mark_persistent(l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__1); +l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__2 = _init_l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__2(); +lean_mark_persistent(l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__2); +l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__3 = _init_l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__3(); +lean_mark_persistent(l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3____closed__3); +if (builtin) {res = l_initFn____x40_Lean_Elab_Tactic_BoolToPropSimps___hyg_3_(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +l_boolToPropSimps = lean_io_result_get_value(res); +lean_mark_persistent(l_boolToPropSimps); +lean_dec_ref(res); +}return lean_io_result_mk_ok(lean_box(0)); +} +#ifdef __cplusplus +} +#endif diff --git a/stage0/stdlib/Lean/Util/Trace.c b/stage0/stdlib/Lean/Util/Trace.c index 86dbb137aa..d6f552ff3a 100644 --- a/stage0/stdlib/Lean/Util/Trace.c +++ b/stage0/stdlib/Lean/Util/Trace.c @@ -7393,7 +7393,7 @@ static lean_object* _init_l_Lean_bombEmoji___closed__1() { _start: { lean_object* x_1; -x_1 = lean_mk_string_unchecked("💥", 4, 1); +x_1 = lean_mk_string_unchecked("💥️", 7, 2); return x_1; } } @@ -7409,7 +7409,7 @@ static lean_object* _init_l_Lean_checkEmoji___closed__1() { _start: { lean_object* x_1; -x_1 = lean_mk_string_unchecked("✅", 3, 1); +x_1 = lean_mk_string_unchecked("✅️", 6, 2); return x_1; } } @@ -7425,7 +7425,7 @@ static lean_object* _init_l_Lean_crossEmoji___closed__1() { _start: { lean_object* x_1; -x_1 = lean_mk_string_unchecked("❌", 3, 1); +x_1 = lean_mk_string_unchecked("❌️", 6, 2); return x_1; } } diff --git a/stage0/stdlib/Std/Data/DHashMap/Internal/Model.c b/stage0/stdlib/Std/Data/DHashMap/Internal/Model.c index 84e7a572d6..56dbf6f975 100644 --- a/stage0/stdlib/Std/Data/DHashMap/Internal/Model.c +++ b/stage0/stdlib/Std/Data/DHashMap/Internal/Model.c @@ -27,6 +27,7 @@ LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_updateBucket___at_Std_DHashMap_ uint8_t lean_usize_dec_eq(size_t, size_t); LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_Raw_u2080_filter_u2098___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_Raw_u2080_insertIfNew_u2098(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_Model_0__Std_DHashMap_Internal_Raw_u2080_Const_get_x3f_match__2_splitter___rarg(lean_object*, lean_object*); lean_object* l_Std_DHashMap_Internal_AssocList_map___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_updateBucket___at_Std_DHashMap_Internal_Raw_u2080_cons_u2098___spec__1(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Std_DHashMap_Internal_updateAllBuckets___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -54,6 +55,7 @@ LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_Raw_u2080_insert_u2098(lean_obj LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_Raw_u2080_filter_u2098(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_Raw_u2080_cons_u2098___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_Raw_u2080_Const_get_x3f_u2098(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_Model_0__Std_DHashMap_Internal_Raw_u2080_expandIfNecessary_match__1_splitter(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_Raw_u2080_insert_u2098___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_updateBucket___at_Std_DHashMap_Internal_Raw_u2080_cons_u2098___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Std_DHashMap_Internal_withComputedSize___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -74,6 +76,7 @@ LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_Raw_u2080_Const_get_x21_u2098__ LEAN_EXPORT uint8_t l_Std_DHashMap_Internal_Raw_u2080_contains_u2098___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_DHashMap_Internal_AssocList_filterMap___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_Raw_u2080_Const_get_x21_u2098___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_Model_0__Std_DHashMap_Internal_Raw_u2080_Const_get_x3f_match__2_splitter(lean_object*, lean_object*, lean_object*); lean_object* l_Std_DHashMap_Internal_AssocList_getCast_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_updateBucket___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_updateAllBuckets___rarg(lean_object*, lean_object*); @@ -85,6 +88,7 @@ uint8_t lean_nat_dec_lt(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_Raw_u2080_Const_getD_u2098___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_Raw_u2080_Const_get_u2098___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_bucket(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_Model_0__Std_DHashMap_Internal_Raw_u2080_expandIfNecessary_match__1_splitter___rarg(lean_object*, lean_object*); static lean_object* l_Std_DHashMap_Internal_Raw_u2080_get_x21_u2098___rarg___closed__1; LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_Model_0__Std_DHashMap_Internal_Raw_u2080_Const_getThenInsertIfNew_x3f_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_withComputedSize(lean_object*, lean_object*); @@ -1235,6 +1239,27 @@ lean_dec(x_4); return x_6; } } +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_Model_0__Std_DHashMap_Internal_Raw_u2080_expandIfNecessary_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_3(x_2, x_3, x_4, lean_box(0)); +return x_5; +} +} +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_Model_0__Std_DHashMap_Internal_Raw_u2080_expandIfNecessary_match__1_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = lean_alloc_closure((void*)(l___private_Std_Data_DHashMap_Internal_Model_0__Std_DHashMap_Internal_Raw_u2080_expandIfNecessary_match__1_splitter___rarg), 2, 0); +return x_4; +} +} LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_Model_0__Std_DHashMap_Internal_Raw_u2080_getThenInsertIfNew_x3f_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -1281,6 +1306,27 @@ lean_dec(x_3); return x_5; } } +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_Model_0__Std_DHashMap_Internal_Raw_u2080_Const_get_x3f_match__2_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_3(x_2, x_3, x_4, lean_box(0)); +return x_5; +} +} +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_Model_0__Std_DHashMap_Internal_Raw_u2080_Const_get_x3f_match__2_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = lean_alloc_closure((void*)(l___private_Std_Data_DHashMap_Internal_Model_0__Std_DHashMap_Internal_Raw_u2080_Const_get_x3f_match__2_splitter___rarg), 2, 0); +return x_4; +} +} LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_Model_0__Std_DHashMap_Internal_Raw_u2080_Const_getThenInsertIfNew_x3f_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { diff --git a/stage0/stdlib/Std/Data/DHashMap/Internal/RawLemmas.c b/stage0/stdlib/Std/Data/DHashMap/Internal/RawLemmas.c index 97be2ce346..02fcd6ff4d 100644 --- a/stage0/stdlib/Std/Data/DHashMap/Internal/RawLemmas.c +++ b/stage0/stdlib/Std/Data/DHashMap/Internal/RawLemmas.c @@ -120,6 +120,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Std_DHashMap_Internal_Raw_u static lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_queryNames___closed__7; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Std_DHashMap_Internal_Raw_u2080___aux__Std__Data__DHashMap__Internal__RawLemmas______macroRules__Std__DHashMap__Internal__Raw_u2080__tacticSimp__to__modelUsing____1___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_DHashMap_Internal_Raw_u2080_tacticWf__trivial; +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_expandIfNecessary_match__1_splitter___rarg(lean_object*, lean_object*); static lean_object* l_Std_DHashMap_Internal_Raw_u2080___aux__Std__Data__DHashMap__Internal__RawLemmas______macroRules__Std__DHashMap__Internal__Raw_u2080__tacticWf__trivial__1___closed__22; static lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_congrNames___closed__16; static lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_congrNames___closed__23; @@ -146,6 +147,7 @@ static lean_object* l_Std_DHashMap_Internal_Raw_u2080___aux__Std__Data__DHashMap static lean_object* l_Std_DHashMap_Internal_Raw_u2080___aux__Std__Data__DHashMap__Internal__RawLemmas______macroRules__Std__DHashMap__Internal__Raw_u2080__tacticWf__trivial__1___closed__64; static lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_congrNames___closed__67; static lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_congrNames___closed__25; +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_Const_get_x3f_match__2_splitter(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Std_DHashMap_Internal_Raw_u2080___aux__Std__Data__DHashMap__Internal__RawLemmas______macroRules__Std__DHashMap__Internal__Raw_u2080__tacticSimp__to__modelUsing____1___spec__7(lean_object*, size_t, size_t, lean_object*); static lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_congrNames___closed__45; static lean_object* l_Std_DHashMap_Internal_Raw_u2080_tacticSimp__to__modelUsing_____closed__16; @@ -190,6 +192,7 @@ uint8_t l_Lean_Syntax_matchesNull(lean_object*, lean_object*); static lean_object* l_Std_DHashMap_Internal_Raw_u2080___aux__Std__Data__DHashMap__Internal__RawLemmas______macroRules__Std__DHashMap__Internal__Raw_u2080__tacticEmpty__1___closed__4; static lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_congrNames___closed__51; static lean_object* l_Std_DHashMap_Internal_Raw_u2080_tacticSimp__to__modelUsing_____closed__11; +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_expandIfNecessary_match__1_splitter(lean_object*, lean_object*, lean_object*); static lean_object* l_Std_DHashMap_Internal_Raw_u2080___aux__Std__Data__DHashMap__Internal__RawLemmas______macroRules__Std__DHashMap__Internal__Raw_u2080__tacticWf__trivial__1___closed__60; static lean_object* l_Std_DHashMap_Internal_Raw_u2080___aux__Std__Data__DHashMap__Internal__RawLemmas______macroRules__Std__DHashMap__Internal__Raw_u2080__tacticWf__trivial__1___closed__25; static lean_object* l_Std_DHashMap_Internal_Raw_u2080___aux__Std__Data__DHashMap__Internal__RawLemmas______macroRules__Std__DHashMap__Internal__Raw_u2080__tacticWf__trivial__1___closed__74; @@ -283,6 +286,7 @@ static lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHas static lean_object* l_Std_DHashMap_Internal_Raw_u2080___aux__Std__Data__DHashMap__Internal__RawLemmas______macroRules__Std__DHashMap__Internal__Raw_u2080__tacticEmpty__1___closed__19; lean_object* l_Lean_Syntax_node8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Std_DHashMap_Internal_Raw_u2080___aux__Std__Data__DHashMap__Internal__RawLemmas______macroRules__Std__DHashMap__Internal__Raw_u2080__tacticWf__trivial__1___closed__38; +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_Const_get_x3f_match__2_splitter___rarg(lean_object*, lean_object*); static lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_congrNames___closed__75; lean_object* lean_array_uget(lean_object*, size_t); size_t lean_array_size(lean_object*); @@ -4845,6 +4849,48 @@ lean_dec(x_1); return x_5; } } +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_expandIfNecessary_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_3(x_2, x_3, x_4, lean_box(0)); +return x_5; +} +} +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_expandIfNecessary_match__1_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = lean_alloc_closure((void*)(l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_expandIfNecessary_match__1_splitter___rarg), 2, 0); +return x_4; +} +} +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_Const_get_x3f_match__2_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_3(x_2, x_3, x_4, lean_box(0)); +return x_5; +} +} +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_Const_get_x3f_match__2_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = lean_alloc_closure((void*)(l___private_Std_Data_DHashMap_Internal_RawLemmas_0__Std_DHashMap_Internal_Raw_u2080_Const_get_x3f_match__2_splitter___rarg), 2, 0); +return x_4; +} +} lean_object* initialize_Std_Data_DHashMap_Internal_WF(uint8_t builtin, lean_object*); static bool _G_initialized = false; LEAN_EXPORT lean_object* initialize_Std_Data_DHashMap_Internal_RawLemmas(uint8_t builtin, lean_object* w) { diff --git a/stage0/stdlib/Std/Data/DHashMap/Internal/WF.c b/stage0/stdlib/Std/Data/DHashMap/Internal/WF.c index b04813b142..16dff3fa92 100644 --- a/stage0/stdlib/Std/Data/DHashMap/Internal/WF.c +++ b/stage0/stdlib/Std/Data/DHashMap/Internal/WF.c @@ -13,6 +13,47 @@ #ifdef __cplusplus extern "C" { #endif +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_WF_0__Std_DHashMap_Internal_Raw_u2080_expandIfNecessary_match__1_splitter___rarg(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_WF_0__Std_DHashMap_Internal_Raw_u2080_reinsertAux_match__2_splitter(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_WF_0__Std_DHashMap_Internal_Raw_u2080_expandIfNecessary_match__1_splitter(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_WF_0__Std_DHashMap_Internal_Raw_u2080_reinsertAux_match__2_splitter___rarg(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_WF_0__Std_DHashMap_Internal_Raw_u2080_reinsertAux_match__2_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_apply_2(x_2, x_1, lean_box(0)); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_WF_0__Std_DHashMap_Internal_Raw_u2080_reinsertAux_match__2_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = lean_alloc_closure((void*)(l___private_Std_Data_DHashMap_Internal_WF_0__Std_DHashMap_Internal_Raw_u2080_reinsertAux_match__2_splitter___rarg), 2, 0); +return x_4; +} +} +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_WF_0__Std_DHashMap_Internal_Raw_u2080_expandIfNecessary_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_3(x_2, x_3, x_4, lean_box(0)); +return x_5; +} +} +LEAN_EXPORT lean_object* l___private_Std_Data_DHashMap_Internal_WF_0__Std_DHashMap_Internal_Raw_u2080_expandIfNecessary_match__1_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = lean_alloc_closure((void*)(l___private_Std_Data_DHashMap_Internal_WF_0__Std_DHashMap_Internal_Raw_u2080_expandIfNecessary_match__1_splitter___rarg), 2, 0); +return x_4; +} +} lean_object* initialize_Std_Data_DHashMap_Basic(uint8_t builtin, lean_object*); lean_object* initialize_Std_Data_DHashMap_Internal_Model(uint8_t builtin, lean_object*); lean_object* initialize_Std_Data_DHashMap_Internal_AssocList_Lemmas(uint8_t builtin, lean_object*); diff --git a/stage0/stdlib/Std/Sat/AIG/CNF.c b/stage0/stdlib/Std/Sat/AIG/CNF.c index 1bc92a5302..63086e1804 100644 --- a/stage0/stdlib/Std/Sat/AIG/CNF.c +++ b/stage0/stdlib/Std/Sat/AIG/CNF.c @@ -19,13 +19,16 @@ LEAN_EXPORT lean_object* l_Std_Sat_AIG_toCNF_Cache_init___boxed(lean_object*); LEAN_EXPORT uint8_t l_Std_Sat_AIG_toCNF_State_eval___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_toCNF_go___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_toCNF_State_eval___boxed(lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CNF_0__Std_Sat_AIG_toCNF_mixAssigns_match__1_splitter___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_Decl_gateToCNF(lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_toCNF_Cache_addGate(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, uint8_t); +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CNF_0__Std_Sat_AIG_toCNF_mixAssigns_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_toCNF_inj___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_toCNF_projectRightAssign___rarg(lean_object*, lean_object*, lean_object*); lean_object* lean_mk_array(lean_object*, lean_object*); lean_object* lean_array_fget(lean_object*, lean_object*); lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CNF_0__Std_Sat_AIG_toCNF_mixAssigns_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_toCNF_Cache_addConst(lean_object*, lean_object*, uint8_t); static lean_object* l_Std_Sat_AIG_toCNF_cnfSatAssignment___lambda__1___closed__2; LEAN_EXPORT lean_object* l_Std_Sat_AIG_toCNF_projectRightAssign___boxed(lean_object*); @@ -498,6 +501,48 @@ lean_dec(x_2); return x_3; } } +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CNF_0__Std_Sat_AIG_toCNF_mixAssigns_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_object* x_4; lean_object* x_5; +lean_dec(x_3); +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_1(x_2, x_4); +return x_5; +} +else +{ +lean_object* x_6; lean_object* x_7; +lean_dec(x_2); +x_6 = lean_ctor_get(x_1, 0); +lean_inc(x_6); +lean_dec(x_1); +x_7 = lean_apply_1(x_3, x_6); +return x_7; +} +} +} +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CNF_0__Std_Sat_AIG_toCNF_mixAssigns_match__1_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Std_Sat_AIG_CNF_0__Std_Sat_AIG_toCNF_mixAssigns_match__1_splitter___rarg), 3, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CNF_0__Std_Sat_AIG_toCNF_mixAssigns_match__1_splitter___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l___private_Std_Sat_AIG_CNF_0__Std_Sat_AIG_toCNF_mixAssigns_match__1_splitter(x_1, x_2); +lean_dec(x_1); +return x_3; +} +} LEAN_EXPORT lean_object* l_Std_Sat_AIG_toCNF_Cache_init(lean_object* x_1) { _start: { diff --git a/stage0/stdlib/Std/Sat/AIG/CachedLemmas.c b/stage0/stdlib/Std/Sat/AIG/CachedLemmas.c index 9e9248eafa..eee409d00c 100644 --- a/stage0/stdlib/Std/Sat/AIG/CachedLemmas.c +++ b/stage0/stdlib/Std/Sat/AIG/CachedLemmas.c @@ -13,9 +13,11 @@ #ifdef __cplusplus extern "C" { #endif +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkAtomCached_match__2_splitter___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_instLawfulOperatorMkAtomCached___rarg___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_instLawfulOperatorBoolMkConstCached___rarg___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_toGraphviz_go_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkGateCached_go_match__2_splitter(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkGateCached_go_match__1_splitter___rarg(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_instLawfulOperatorMkAtomCached___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkAtomCached_match__1_splitter(lean_object*, lean_object*, lean_object*, lean_object*); @@ -23,13 +25,17 @@ LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkA LEAN_EXPORT lean_object* l_Std_Sat_AIG_instLawfulOperatorMkAtomCached(lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_instLawfulOperatorGateInputMkGateCached___rarg___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkAtomCached_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkGateCached_go_match__2_splitter___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_toGraphviz_go_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkGateCached_go_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_instLawfulOperatorGateInputMkGateCached(lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkGateCached_go_match__2_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_instLawfulOperatorBoolMkConstCached___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkAtomCached_match__1_splitter___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkGateCached_go_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_instLawfulOperatorGateInputMkGateCached___rarg(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkAtomCached_match__2_splitter(lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkAtomCached_match__2_splitter___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_instLawfulOperatorBoolMkConstCached(lean_object*); LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_toGraphviz_go_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: @@ -85,6 +91,37 @@ x_3 = lean_alloc_closure((void*)(l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat return x_3; } } +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkAtomCached_match__2_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_3(x_2, x_3, x_4, lean_box(0)); +return x_5; +} +} +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkAtomCached_match__2_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; +x_5 = lean_alloc_closure((void*)(l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkAtomCached_match__2_splitter___rarg), 2, 0); +return x_5; +} +} +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkAtomCached_match__2_splitter___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; +x_5 = l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkAtomCached_match__2_splitter(x_1, x_2, x_3, x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_5; +} +} LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkAtomCached_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -908,6 +945,37 @@ lean_dec(x_1); return x_3; } } +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkGateCached_go_match__2_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 1); +lean_inc(x_5); +lean_dec(x_1); +x_6 = lean_apply_4(x_3, x_4, x_5, lean_box(0), x_2); +return x_6; +} +} +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkGateCached_go_match__2_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; +x_5 = lean_alloc_closure((void*)(l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkGateCached_go_match__2_splitter___rarg), 3, 0); +return x_5; +} +} +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkGateCached_go_match__2_splitter___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; +x_5 = l___private_Std_Sat_AIG_CachedLemmas_0__Std_Sat_AIG_mkGateCached_go_match__2_splitter(x_1, x_2, x_3, x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_5; +} +} lean_object* initialize_Init(uint8_t builtin, lean_object*); lean_object* initialize_Std_Sat_AIG_Cached(uint8_t builtin, lean_object*); static bool _G_initialized = false; diff --git a/stage0/stdlib/Std/Sat/AIG/RefVec.c b/stage0/stdlib/Std/Sat/AIG/RefVec.c index 921f7dd7c7..1436c5a063 100644 --- a/stage0/stdlib/Std/Sat/AIG/RefVec.c +++ b/stage0/stdlib/Std/Sat/AIG/RefVec.c @@ -21,18 +21,23 @@ LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_cast_x27___rarg___boxed(lean_objec LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_append(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_append___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_cast___rarg___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_RefVec_get_match__1_splitter___rarg(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_RefVec_get_match__1_splitter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_array_push(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_push(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_array_fget(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_empty___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_BinaryRefVec_cast_match__1_splitter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_BinaryRefVec_cast___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_get___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_cast___rarg(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_RefVec_get_match__1_splitter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_empty(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_getD___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_append___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_append___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_getD(lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_BinaryRefVec_cast_match__1_splitter___rarg(lean_object*, lean_object*); static lean_object* l_Std_Sat_AIG_RefVec_empty___closed__1; LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_getD___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_getD___rarg(lean_object*, lean_object*, lean_object*, lean_object*); @@ -47,6 +52,7 @@ LEAN_EXPORT lean_object* l_Std_Sat_AIG_BinaryRefVec_cast(lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_push___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_append___rarg___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_BinaryRefVec_cast___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_BinaryRefVec_cast_match__1_splitter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* _init_l_Std_Sat_AIG_RefVec_empty___closed__1() { _start: { @@ -215,6 +221,34 @@ lean_dec(x_2); return x_6; } } +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_RefVec_get_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_apply_3(x_2, x_1, lean_box(0), lean_box(0)); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_RefVec_get_match__1_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +x_7 = lean_alloc_closure((void*)(l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_RefVec_get_match__1_splitter___rarg), 2, 0); +return x_7; +} +} +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_RefVec_get_match__1_splitter___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +x_7 = l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_RefVec_get_match__1_splitter(x_1, x_2, x_3, x_4, x_5, x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_7; +} +} LEAN_EXPORT lean_object* l_Std_Sat_AIG_RefVec_append___rarg(lean_object* x_1, lean_object* x_2) { _start: { @@ -347,6 +381,39 @@ lean_dec(x_1); return x_8; } } +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_BinaryRefVec_cast_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_2(x_2, x_3, x_4); +return x_5; +} +} +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_BinaryRefVec_cast_match__1_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +x_7 = lean_alloc_closure((void*)(l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_BinaryRefVec_cast_match__1_splitter___rarg), 2, 0); +return x_7; +} +} +LEAN_EXPORT lean_object* l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_BinaryRefVec_cast_match__1_splitter___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +x_7 = l___private_Std_Sat_AIG_RefVec_0__Std_Sat_AIG_BinaryRefVec_cast_match__1_splitter(x_1, x_2, x_3, x_4, x_5, x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_7; +} +} lean_object* initialize_Init(uint8_t builtin, lean_object*); lean_object* initialize_Std_Sat_AIG_LawfulOperator(uint8_t builtin, lean_object*); lean_object* initialize_Std_Sat_AIG_CachedGatesLemmas(uint8_t builtin, lean_object*); diff --git a/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.c b/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.c index 32ec38a982..abfce3f72b 100644 --- a/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.c +++ b/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.c @@ -16,6 +16,7 @@ extern "C" { LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_blastAdd_go___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_instLawfulOperatorFullAdderInputMkFullAdderOut___rarg(lean_object*, lean_object*); lean_object* lean_mk_empty_array_with_capacity(lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_mkFullAdder___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_mkFullAdderOut(lean_object*); lean_object* lean_array_push(lean_object*, lean_object*); @@ -28,11 +29,13 @@ LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_instLawfulOperato LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_blastAdd___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast(lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_blastAdd_go(lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_instLawfulOperatorFullAdderInputMkFullAdderOut(lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_blastAdd_instLawfulVecOperatorBinaryRefVec___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_mkFullAdderOut___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_blastAdd(lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_instLawfulOperatorFullAdderInputMkFullAdderCarry(lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_instLawfulOperatorFullAdderInputMkFullAdderCarry___rarg(lean_object*, lean_object*); uint8_t lean_nat_dec_lt(lean_object*, lean_object*); @@ -96,6 +99,40 @@ lean_dec(x_1); return x_7; } } +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 2); +lean_inc(x_5); +lean_dec(x_1); +x_6 = lean_apply_3(x_2, x_3, x_4, x_5); +return x_6; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +_start: +{ +lean_object* x_6; +x_6 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter___rarg), 2, 0); +return x_6; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +_start: +{ +lean_object* x_6; +x_6 = l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter(x_1, x_2, x_3, x_4, x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_6; +} +} LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_mkFullAdderOut___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { diff --git a/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Append.c b/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Append.c index be8b5f54d8..088997cfa0 100644 --- a/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Append.c +++ b/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Append.c @@ -15,11 +15,14 @@ extern "C" { #endif LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_instLawfulVecOperatorAppendTargetBlastAppend(lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_blastAppend(lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Append_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastAppend_match__1_splitter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_instLawfulVecOperatorAppendTargetBlastAppend___rarg(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Append_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastAppend_match__1_splitter___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_blastAppend___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_append___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_blastAppend___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_instLawfulVecOperatorAppendTargetBlastAppend___rarg___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Append_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastAppend_match__1_splitter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_blastAppend___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { @@ -56,6 +59,43 @@ lean_dec(x_1); return x_6; } } +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Append_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastAppend_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 2); +lean_inc(x_5); +x_6 = lean_ctor_get(x_1, 3); +lean_inc(x_6); +lean_dec(x_1); +x_7 = lean_apply_5(x_2, x_3, x_4, x_5, x_6, lean_box(0)); +return x_7; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Append_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastAppend_match__1_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +x_7 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Append_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastAppend_match__1_splitter___rarg), 2, 0); +return x_7; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Append_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastAppend_match__1_splitter___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +x_7 = l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Append_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastAppend_match__1_splitter(x_1, x_2, x_3, x_4, x_5, x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_7; +} +} LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_instLawfulVecOperatorAppendTargetBlastAppend___rarg(lean_object* x_1, lean_object* x_2) { _start: { diff --git a/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.c b/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.c index d8a87d5bd3..b67e11e1d4 100644 --- a/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.c +++ b/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.c @@ -19,9 +19,12 @@ LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_instLawfulVecOper LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_blastReplicate(lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_instLawfulVecOperatorReplicateTargetBlastReplicate___rarg___boxed(lean_object*, lean_object*); static lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_blastReplicate___rarg___closed__1; +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Replicate_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastReplicate_match__1_splitter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_append___rarg(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Replicate_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastReplicate_match__1_splitter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_blastReplicate___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_nat_dec_lt(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Replicate_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastReplicate_match__1_splitter___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_blastReplicate_go___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_nat_add(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_blastReplicate_go___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -118,6 +121,41 @@ lean_dec(x_1); return x_6; } } +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Replicate_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastReplicate_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 2); +lean_inc(x_5); +lean_dec(x_1); +x_6 = lean_apply_4(x_2, x_3, x_4, x_5, lean_box(0)); +return x_6; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Replicate_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastReplicate_match__1_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +x_7 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Replicate_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastReplicate_match__1_splitter___rarg), 2, 0); +return x_7; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Replicate_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastReplicate_match__1_splitter___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +lean_object* x_7; +x_7 = l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Replicate_0__Std_Tactic_BVDecide_BVExpr_bitblast_blastReplicate_match__1_splitter(x_1, x_2, x_3, x_4, x_5, x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_7; +} +} LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_instLawfulVecOperatorReplicateTargetBlastReplicate___rarg(lean_object* x_1, lean_object* x_2) { _start: { diff --git a/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.c b/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.c index ba1ad80a51..62ffb1b790 100644 --- a/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.c +++ b/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.c @@ -14,6 +14,7 @@ extern "C" { #endif lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_blastNot___at_Std_Tactic_BVDecide_BVExpr_bitblast_go___spec__7(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Pred_0__Std_Tactic_BVDecide_BVPred_bitblast_match__2_splitter(lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_mkOverflowBit_go___at_Std_Tactic_BVDecide_BVPred_bitblast___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_Sat_AIG_RefVec_zip___at_Std_Tactic_BVDecide_BVExpr_bitblast_go___spec__5(lean_object*, lean_object*, lean_object*); lean_object* lean_array_fget(lean_object*, lean_object*); @@ -21,13 +22,16 @@ LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVPred_instLawfulOperatorBVBitBit lean_object* l_Std_Sat_AIG_mkAndCached___at_Std_Tactic_BVDecide_BVExpr_bitblast_blastMul_go___spec__25(lean_object*, lean_object*); lean_object* l_Std_Sat_AIG_mkConstCached___at_Std_Tactic_BVDecide_BVExpr_bitblast_blastMul_go___spec__4(lean_object*, uint8_t); lean_object* l_Std_Sat_AIG_instLawfulOperatorBinaryInputMkAndCached___rarg(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Pred_0__Std_Tactic_BVDecide_BVPred_bitblast_match__1_splitter(lean_object*); static lean_object* l_Std_Tactic_BVDecide_BVPred_mkEq___at_Std_Tactic_BVDecide_BVPred_bitblast___spec__1___closed__2; static lean_object* l_Std_Tactic_BVDecide_BVPred_mkEq___at_Std_Tactic_BVDecide_BVPred_bitblast___spec__1___closed__4; lean_object* l_Std_Sat_AIG_mkNotCached___at_Std_Tactic_BVDecide_BVExpr_bitblast_blastMul_go___spec__30(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Pred_0__Std_Tactic_BVDecide_BVPred_bitblast_match__1_splitter___rarg(uint8_t, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVPred_blastGetLsb___at_Std_Tactic_BVDecide_BVPred_bitblast___spec__8(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_mkOverflowBit___at_Std_Tactic_BVDecide_BVPred_bitblast___spec__6(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Sat_AIG_mkBEqCached___at_Std_Tactic_BVDecide_BVPred_bitblast___spec__2(lean_object*, lean_object*); lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_go(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Pred_0__Std_Tactic_BVDecide_BVPred_bitblast_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Std_Tactic_BVDecide_BVExpr_bitblast_mkFullAdderCarry___at_Std_Tactic_BVDecide_BVExpr_bitblast_blastMul_go___spec__24(lean_object*, lean_object*); lean_object* l_Std_Tactic_BVDecide_instDecidableEqBVBit___boxed(lean_object*, lean_object*); static lean_object* l_Std_Tactic_BVDecide_BVPred_mkEq___at_Std_Tactic_BVDecide_BVPred_bitblast___spec__1___closed__1; @@ -37,6 +41,7 @@ LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVPred_mkEq___at_Std_Tactic_BVDec uint8_t lean_nat_dec_lt(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVPred_blastGetLsb___at_Std_Tactic_BVDecide_BVPred_bitblast___spec__8___boxed(lean_object*, lean_object*); lean_object* l_Std_Sat_AIG_mkGateCached___at_Std_Tactic_BVDecide_BVExpr_bitblast_blastMul_go___spec__21(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Pred_0__Std_Tactic_BVDecide_BVPred_bitblast_match__2_splitter___rarg(lean_object*, lean_object*, lean_object*); static lean_object* l_Std_Sat_AIG_mkBEqCached___at_Std_Tactic_BVDecide_BVPred_bitblast___spec__2___closed__1; static lean_object* l_Std_Tactic_BVDecide_BVPred_mkEq___at_Std_Tactic_BVDecide_BVPred_bitblast___spec__1___closed__3; LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVPred_bitblast(lean_object*, lean_object*); @@ -620,6 +625,84 @@ lean_dec(x_2); return x_3; } } +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Pred_0__Std_Tactic_BVDecide_BVPred_bitblast_match__2_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 0) +{ +lean_object* x_4; lean_object* x_5; uint8_t x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; +lean_dec(x_3); +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 1); +lean_inc(x_5); +x_6 = lean_ctor_get_uint8(x_1, sizeof(void*)*3); +x_7 = lean_ctor_get(x_1, 2); +lean_inc(x_7); +lean_dec(x_1); +x_8 = lean_box(x_6); +x_9 = lean_apply_4(x_2, x_4, x_5, x_8, x_7); +return x_9; +} +else +{ +lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; +lean_dec(x_2); +x_10 = lean_ctor_get(x_1, 0); +lean_inc(x_10); +x_11 = lean_ctor_get(x_1, 1); +lean_inc(x_11); +x_12 = lean_ctor_get(x_1, 2); +lean_inc(x_12); +lean_dec(x_1); +x_13 = lean_apply_3(x_3, x_10, x_11, x_12); +return x_13; +} +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Pred_0__Std_Tactic_BVDecide_BVPred_bitblast_match__2_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Pred_0__Std_Tactic_BVDecide_BVPred_bitblast_match__2_splitter___rarg), 3, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Pred_0__Std_Tactic_BVDecide_BVPred_bitblast_match__1_splitter___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (x_1 == 0) +{ +lean_inc(x_2); +return x_2; +} +else +{ +lean_inc(x_3); +return x_3; +} +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Pred_0__Std_Tactic_BVDecide_BVPred_bitblast_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Pred_0__Std_Tactic_BVDecide_BVPred_bitblast_match__1_splitter___rarg___boxed), 3, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Pred_0__Std_Tactic_BVDecide_BVPred_bitblast_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint8_t x_4; lean_object* x_5; +x_4 = lean_unbox(x_1); +lean_dec(x_1); +x_5 = l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Pred_0__Std_Tactic_BVDecide_BVPred_bitblast_match__1_splitter___rarg(x_4, x_2, x_3); +lean_dec(x_3); +lean_dec(x_2); +return x_5; +} +} static lean_object* _init_l_Std_Tactic_BVDecide_BVPred_instLawfulOperatorBVBitBitblast___closed__1() { _start: { diff --git a/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.c b/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.c index f7133db283..0c0cfd5793 100644 --- a/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.c +++ b/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.c @@ -13,6 +13,43 @@ #ifdef __cplusplus extern "C" { #endif +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Lemmas_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Lemmas_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Lemmas_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter___rarg(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Lemmas_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 2); +lean_inc(x_5); +lean_dec(x_1); +x_6 = lean_apply_3(x_2, x_3, x_4, x_5); +return x_6; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Lemmas_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +_start: +{ +lean_object* x_6; +x_6 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Lemmas_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter___rarg), 2, 0); +return x_6; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Lemmas_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +_start: +{ +lean_object* x_6; +x_6 = l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Lemmas_Operations_Add_0__Std_Tactic_BVDecide_BVExpr_bitblast_FullAdderInput_cast_match__1_splitter(x_1, x_2, x_3, x_4, x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_6; +} +} lean_object* initialize_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Lemmas_Basic(uint8_t builtin, lean_object*); lean_object* initialize_Std_Tactic_BVDecide_Bitblast_BVExpr_Circuit_Impl_Operations_Add(uint8_t builtin, lean_object*); static bool _G_initialized = false; diff --git a/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.c b/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.c index a90005041a..0d856d6ffa 100644 --- a/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.c +++ b/stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.c @@ -14,6 +14,8 @@ extern "C" { #endif LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BoolExpr_toString(lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BoolExpr_Basic_0__Std_Tactic_BVDecide_Gate_toString_match__1_splitter(lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BoolExpr_Basic_0__Std_Tactic_BVDecide_Gate_toString_match__1_splitter___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BoolExpr_eval___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BoolExpr_size___rarg___boxed(lean_object*); static lean_object* l_Std_Tactic_BVDecide_Gate_toString___closed__2; @@ -37,6 +39,7 @@ LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BoolExpr_toString___rarg(lean_obj static lean_object* l_Std_Tactic_BVDecide_Gate_toString___closed__3; LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BoolExpr_instToString___rarg(lean_object*); LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BoolExpr_size(lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BoolExpr_Basic_0__Std_Tactic_BVDecide_Gate_toString_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BoolExpr_Basic_0__Std_Tactic_BVDecide_BoolExpr_toString_match__1_splitter(lean_object*, lean_object*); static lean_object* l_Std_Tactic_BVDecide_BoolExpr_toString___rarg___closed__4; LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_Gate_noConfusion___rarg___lambda__1(lean_object*); @@ -686,6 +689,61 @@ x_2 = lean_alloc_closure((void*)(l_Std_Tactic_BVDecide_BoolExpr_eval___rarg), 2, return x_2; } } +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BoolExpr_Basic_0__Std_Tactic_BVDecide_Gate_toString_match__1_splitter___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +switch (x_1) { +case 0: +{ +lean_inc(x_2); +return x_2; +} +case 1: +{ +lean_inc(x_3); +return x_3; +} +case 2: +{ +lean_inc(x_4); +return x_4; +} +case 3: +{ +lean_inc(x_5); +return x_5; +} +default: +{ +lean_inc(x_6); +return x_6; +} +} +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BoolExpr_Basic_0__Std_Tactic_BVDecide_Gate_toString_match__1_splitter(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_Bitblast_BoolExpr_Basic_0__Std_Tactic_BVDecide_Gate_toString_match__1_splitter___rarg___boxed), 6, 0); +return x_2; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BoolExpr_Basic_0__Std_Tactic_BVDecide_Gate_toString_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +uint8_t x_7; lean_object* x_8; +x_7 = lean_unbox(x_1); +lean_dec(x_1); +x_8 = l___private_Std_Tactic_BVDecide_Bitblast_BoolExpr_Basic_0__Std_Tactic_BVDecide_Gate_toString_match__1_splitter___rarg(x_7, x_2, x_3, x_4, x_5, x_6); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +return x_8; +} +} lean_object* initialize_Init_Notation(uint8_t builtin, lean_object*); lean_object* initialize_Init_Data_Bool(uint8_t builtin, lean_object*); static bool _G_initialized = false; diff --git a/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.c b/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.c index 21fe82760a..caef223fd8 100644 --- a/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.c +++ b/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.c @@ -14,20 +14,57 @@ extern "C" { #endif LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_deleteOne_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__cond_match__1_splitter___rarg(uint8_t, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_deleteOne_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_ofArray__fold__fn_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_deleteOne_match__1_splitter___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__cond_match__1_splitter(lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_ofArray__fold__fn_match__2_splitter___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_ofArray__fold__fn_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_ofArray__fold__fn_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_ofArray__fold__fn_match__2_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_deleteOne_match__1_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_ofArray__fold__fn_match__1_splitter___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_ofArray__fold__fn_match__2_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__cond_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_ofArray__fold__fn_match__2_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 2); +lean_inc(x_5); +x_6 = lean_ctor_get(x_1, 3); +lean_inc(x_6); +lean_dec(x_1); +x_7 = lean_apply_4(x_2, x_3, x_4, x_5, x_6); +return x_7; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter___rarg), 2, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter(x_1, x_2); +lean_dec(x_1); +return x_3; +} +} LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_Lemmas_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_ofArray__fold__fn_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { diff --git a/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.c b/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.c index c4cc5cf537..1603d7da44 100644 --- a/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.c +++ b/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.c @@ -13,10 +13,89 @@ #ifdef __cplusplus extern "C" { #endif +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_performRatCheck_match__2_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_performRatCheck_match__1_splitter___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_performRatCheck_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_performRatCheck_match__2_splitter___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_performRatCheck_match__1_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_performRatCheck_match__2_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_performRatCheck_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter___rarg(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 2); +lean_inc(x_5); +x_6 = lean_ctor_get(x_1, 3); +lean_inc(x_6); +lean_dec(x_1); +x_7 = lean_apply_4(x_2, x_3, x_4, x_5, x_6); +return x_7; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter___rarg), 2, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter(x_1, x_2); +lean_dec(x_1); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_performRatCheck_match__2_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 1); +lean_inc(x_5); +x_6 = lean_ctor_get(x_1, 2); +lean_inc(x_6); +x_7 = lean_ctor_get(x_1, 3); +lean_inc(x_7); +lean_dec(x_1); +x_8 = lean_ctor_get(x_2, 0); +lean_inc(x_8); +x_9 = lean_ctor_get(x_2, 1); +lean_inc(x_9); +lean_dec(x_2); +x_10 = lean_apply_6(x_3, x_4, x_5, x_6, x_7, x_8, x_9); +return x_10; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_performRatCheck_match__2_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_performRatCheck_match__2_splitter___rarg), 3, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_performRatCheck_match__2_splitter___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_performRatCheck_match__2_splitter(x_1, x_2); +lean_dec(x_1); +return x_3; +} +} LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RatAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_performRatCheck_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { diff --git a/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.c b/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.c index 1954944cf9..5a10f23130 100644 --- a/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.c +++ b/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.c @@ -13,14 +13,198 @@ #ifdef __cplusplus extern "C" { #endif +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__2_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__3_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__1_splitter___rarg(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_clearUnit_match__1_splitter___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__1_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__2_splitter___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__2_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__3_splitter___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_clearUnit_match__1_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__2_splitter___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__1_splitter___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__2_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__2_splitter___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_clearUnit_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__2_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__3_splitter___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__1_splitter___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__1_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__2_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; +x_3 = lean_ctor_get(x_1, 1); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_ctor_get(x_3, 0); +lean_inc(x_5); +x_6 = lean_ctor_get(x_3, 1); +lean_inc(x_6); +lean_dec(x_3); +x_7 = lean_apply_3(x_2, x_4, x_5, x_6); +return x_7; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__2_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__2_splitter___rarg), 2, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__2_splitter___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__2_splitter(x_1, x_2); +lean_dec(x_1); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_2(x_2, x_3, x_4); +return x_5; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__1_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__1_splitter___rarg), 2, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__1_splitter___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insertUnit_match__1_splitter(x_1, x_2); +lean_dec(x_1); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_clearUnit_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_4 = lean_ctor_get(x_2, 0); +lean_inc(x_4); +x_5 = lean_ctor_get(x_2, 1); +lean_inc(x_5); +lean_dec(x_2); +x_6 = lean_apply_3(x_3, x_1, x_4, x_5); +return x_6; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_clearUnit_match__1_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_clearUnit_match__1_splitter___rarg), 3, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_clearUnit_match__1_splitter___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_clearUnit_match__1_splitter(x_1, x_2); +lean_dec(x_1); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; +x_3 = lean_ctor_get(x_1, 0); +lean_inc(x_3); +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 2); +lean_inc(x_5); +x_6 = lean_ctor_get(x_1, 3); +lean_inc(x_6); +lean_dec(x_1); +x_7 = lean_apply_4(x_2, x_3, x_4, x_5, x_6); +return x_7; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter___rarg), 2, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_insert_match__1_splitter(x_1, x_2); +lean_dec(x_1); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__3_splitter___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; +x_3 = lean_ctor_get(x_1, 1); +lean_inc(x_3); +x_4 = lean_ctor_get(x_3, 1); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 0); +lean_inc(x_5); +lean_dec(x_1); +x_6 = lean_ctor_get(x_3, 0); +lean_inc(x_6); +lean_dec(x_3); +x_7 = lean_ctor_get(x_4, 0); +lean_inc(x_7); +x_8 = lean_ctor_get(x_4, 1); +lean_inc(x_8); +lean_dec(x_4); +x_9 = lean_apply_4(x_2, x_5, x_6, x_7, x_8); +return x_9; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__3_splitter(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__3_splitter___rarg), 2, 0); +return x_3; +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__3_splitter___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__3_splitter(x_1, x_2); +lean_dec(x_1); +return x_3; +} +} LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_Formula_RupAddResult_0__Std_Tactic_BVDecide_LRAT_Internal_DefaultFormula_confirmRupHint_match__2_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { diff --git a/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.c b/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.c index 7c2e10daa1..782c289c2b 100644 --- a/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.c +++ b/stage0/stdlib/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.c @@ -15,8 +15,10 @@ extern "C" { #endif LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_LRATCheckerSound_0__Std_Tactic_BVDecide_LRAT_Internal_lratChecker_match__2_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_LRATCheckerSound_0__Std_Tactic_BVDecide_LRAT_Internal_lratChecker_match__1_splitter___rarg(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_LRATCheckerSound_0__Std_Tactic_BVDecide_LRAT_Internal_WellFormedAction_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_LRATCheckerSound_0__Std_Tactic_BVDecide_LRAT_Internal_lratChecker_match__2_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_LRATCheckerSound_0__Std_Tactic_BVDecide_LRAT_Internal_lratChecker_match__2_splitter(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_LRATCheckerSound_0__Std_Tactic_BVDecide_LRAT_Internal_WellFormedAction_match__1_splitter(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_LRATCheckerSound_0__Std_Tactic_BVDecide_LRAT_Internal_lratChecker_match__1_splitter(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_LRATCheckerSound_0__Std_Tactic_BVDecide_LRAT_Internal_lratChecker_match__2_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { _start: @@ -152,6 +154,44 @@ x_3 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_LRAT_Internal_L return x_3; } } +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_LRATCheckerSound_0__Std_Tactic_BVDecide_LRAT_Internal_WellFormedAction_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_1) == 2) +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; +lean_dec(x_3); +x_4 = lean_ctor_get(x_1, 0); +lean_inc(x_4); +x_5 = lean_ctor_get(x_1, 1); +lean_inc(x_5); +x_6 = lean_ctor_get(x_1, 2); +lean_inc(x_6); +x_7 = lean_ctor_get(x_1, 3); +lean_inc(x_7); +x_8 = lean_ctor_get(x_1, 4); +lean_inc(x_8); +lean_dec(x_1); +x_9 = lean_apply_5(x_2, x_4, x_5, x_6, x_7, x_8); +return x_9; +} +else +{ +lean_object* x_10; +lean_dec(x_2); +x_10 = lean_apply_2(x_3, x_1, lean_box(0)); +return x_10; +} +} +} +LEAN_EXPORT lean_object* l___private_Std_Tactic_BVDecide_LRAT_Internal_LRATCheckerSound_0__Std_Tactic_BVDecide_LRAT_Internal_WellFormedAction_match__1_splitter(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = lean_alloc_closure((void*)(l___private_Std_Tactic_BVDecide_LRAT_Internal_LRATCheckerSound_0__Std_Tactic_BVDecide_LRAT_Internal_WellFormedAction_match__1_splitter___rarg), 3, 0); +return x_4; +} +} lean_object* initialize_Std_Tactic_BVDecide_LRAT_Internal_LRATChecker(uint8_t builtin, lean_object*); lean_object* initialize_Std_Tactic_BVDecide_LRAT_Internal_CNF(uint8_t builtin, lean_object*); lean_object* initialize_Std_Tactic_BVDecide_LRAT_Internal_Actions(uint8_t builtin, lean_object*);