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

chore(stage0): update

Browse source
This commit is contained in:
Leonardo de Moura 2019-09-19 10:48:37 -07:00
parent b147ebad67
commit ac2871e15c
19 changed files with 9540 additions and 2251 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

284
src/stage0/init/control/combinators.c
View file

@ -14,6 +14,7 @@
extern "C" {
#endif
lean_object* l_List_mfoldl___main(lean_object*);
lean_object* l_Nat_mforRevAux___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_mforAux___main(lean_object*);
lean_object* l_List_mmap(lean_object*);
lean_object* l_Nat_mforAux___boxed(lean_object*);
@ -29,6 +30,7 @@ lean_object* l_List_mexists___boxed(lean_object*);
lean_object* l_Nat_mforAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_mcond___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_mjoin___rarg___closed__1;
lean_object* l_Nat_mforRev___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_mcond___rarg___lambda__1(lean_object*, lean_object*, uint8_t);
lean_object* l_Nat_mfold___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mfilter___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -42,9 +44,16 @@ lean_object* l_when___boxed(lean_object*);
lean_object* l_List_mmap___main___boxed(lean_object*);
lean_object* l_List_mmap___boxed(lean_object*);
lean_object* l_List_mfor___main___boxed(lean_object*);
lean_object* l_Nat_mforRev(lean_object*);
lean_object* l_Nat_mfoldRevAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_mforRevAux___boxed(lean_object*);
lean_object* l_Nat_mfoldAux___main(lean_object*, lean_object*);
lean_object* l_Nat_mfoldRevAux(lean_object*, lean_object*);
lean_object* l_List_mfirst___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mfoldr(lean_object*);
lean_object* l_Nat_mfoldRevAux___main(lean_object*, lean_object*);
lean_object* l_Nat_mforRevAux___main(lean_object*);
lean_object* l_Nat_mfoldRevAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mfilter___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_mcond___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_when___rarg(lean_object*, lean_object*, uint8_t, lean_object*);
@ -55,15 +64,18 @@ lean_object* l_List_mmap___main___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_List_mfoldl___main___boxed(lean_object*);
lean_object* l_mwhen___rarg___lambda__1(lean_object*, lean_object*, uint8_t);
lean_object* l_List_mfoldr___main(lean_object*);
lean_object* l_Nat_mforRev___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_List_mfoldl___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mfirst___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mforall___main___boxed(lean_object*);
lean_object* l_Nat_mfoldRevAux___main___boxed(lean_object*, lean_object*);
lean_object* l_List_mforall___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_unless___rarg(lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* l_List_mfoldr___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Nat_mfoldAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_mfor(lean_object*);
lean_object* l_Nat_mfoldRevAux___boxed(lean_object*, lean_object*);
lean_object* l_List_mmap___main(lean_object*);
lean_object* l_List_mexists___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_mfoldAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -73,16 +85,22 @@ lean_object* l_when___rarg___boxed(lean_object*, lean_object*, lean_object*, lea
lean_object* l_List_mfoldl___boxed(lean_object*);
lean_object* l_List_mfoldl___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_mjoin___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_mfoldRevAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mfilter___main___boxed(lean_object*);
lean_object* l_mjoin(lean_object*);
lean_object* l_List_mfor___main(lean_object*);
lean_object* l_Nat_mforAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_mforRevAux___main___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_mwhen___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_mfoldAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mforall(lean_object*);
lean_object* l_Nat_mforRevAux___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_mforRevAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_List_mfor___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_mfold___boxed(lean_object*, lean_object*);
lean_object* l_Nat_mfoldRev___boxed(lean_object*, lean_object*);
lean_object* l_List_mforall___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Nat_mfoldRevAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_mfold(lean_object*, lean_object*);
lean_object* l_Nat_mforAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mfilter(lean_object*);
@ -94,11 +112,15 @@ lean_object* l_Nat_mfoldAux___rarg(lean_object*, lean_object*, lean_object*, lea
lean_object* l_unless___boxed(lean_object*);
lean_object* l_List_mfirst(lean_object*, lean_object*);
lean_object* l_List_mfoldr___main___boxed(lean_object*);
lean_object* l_Nat_mforRev___boxed(lean_object*);
lean_object* l_List_mfilter___main___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_mfoldRev(lean_object*, lean_object*);
lean_object* l_List_mfilter___main(lean_object*);
lean_object* l_List_mexists___main___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_mfoldRev___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mforall___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mmap___main___rarg___closed__1;
lean_object* l_Nat_mforRevAux___main___boxed(lean_object*);
lean_object* l_List_mforall___boxed(lean_object*);
lean_object* l_List_mfoldl(lean_object*);
lean_object* l_List_mfor(lean_object*);
@ -115,7 +137,9 @@ lean_object* l_when(lean_object*);
lean_object* l_List_mexists___main___boxed(lean_object*);
lean_object* l_List_mexists(lean_object*);
lean_object* l_List_mfor___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_mforRevAux(lean_object*);
lean_object* l_mwhen___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_mfoldRev___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mexists___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_mwhen(lean_object*);
lean_object* l_List_mfirst___main(lean_object*);
@ -510,6 +534,134 @@ lean_dec(x_1);
return x_2;
}
}
lean_object* l_Nat_mforRevAux___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = lean_unsigned_to_nat(0u);
x_5 = lean_nat_dec_eq(x_3, x_4);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_6 = lean_unsigned_to_nat(1u);
x_7 = lean_nat_sub(x_3, x_6);
x_8 = lean_ctor_get(x_1, 4);
lean_inc(x_8);
lean_inc(x_2);
lean_inc(x_7);
x_9 = lean_apply_1(x_2, x_7);
x_10 = l_Nat_mforRevAux___main___rarg(x_1, x_2, x_7);
lean_dec(x_7);
x_11 = lean_apply_4(x_8, lean_box(0), lean_box(0), x_9, x_10);
return x_11;
}
else
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
lean_dec(x_2);
x_12 = lean_ctor_get(x_1, 1);
lean_inc(x_12);
lean_dec(x_1);
x_13 = lean_box(0);
x_14 = lean_apply_2(x_12, lean_box(0), x_13);
return x_14;
}
}
}
lean_object* l_Nat_mforRevAux___main(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Nat_mforRevAux___main___rarg___boxed), 3, 0);
return x_2;
}
}
lean_object* l_Nat_mforRevAux___main___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Nat_mforRevAux___main___rarg(x_1, x_2, x_3);
lean_dec(x_3);
return x_4;
}
}
lean_object* l_Nat_mforRevAux___main___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Nat_mforRevAux___main(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Nat_mforRevAux___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Nat_mforRevAux___main___rarg(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Nat_mforRevAux(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Nat_mforRevAux___rarg___boxed), 3, 0);
return x_2;
}
}
lean_object* l_Nat_mforRevAux___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Nat_mforRevAux___rarg(x_1, x_2, x_3);
lean_dec(x_3);
return x_4;
}
}
lean_object* l_Nat_mforRevAux___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Nat_mforRevAux(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Nat_mforRev___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Nat_mforRevAux___main___rarg(x_1, x_3, x_2);
return x_4;
}
}
lean_object* l_Nat_mforRev(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Nat_mforRev___rarg___boxed), 3, 0);
return x_2;
}
}
lean_object* l_Nat_mforRev___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Nat_mforRev___rarg(x_1, x_2, x_3);
lean_dec(x_2);
return x_4;
}
}
lean_object* l_Nat_mforRev___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Nat_mforRev(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Nat_mfoldAux___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
@ -639,6 +791,138 @@ lean_dec(x_2);
return x_3;
}
}
lean_object* l_Nat_mfoldRevAux___main___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_3, x_5);
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_7 = lean_unsigned_to_nat(1u);
x_8 = lean_nat_sub(x_3, x_7);
x_9 = lean_ctor_get(x_1, 1);
lean_inc(x_9);
lean_inc(x_2);
lean_inc(x_8);
x_10 = lean_apply_2(x_2, x_8, x_4);
x_11 = lean_alloc_closure((void*)(l_Nat_mfoldRevAux___main___rarg___boxed), 4, 3);
lean_closure_set(x_11, 0, x_1);
lean_closure_set(x_11, 1, x_2);
lean_closure_set(x_11, 2, x_8);
x_12 = lean_apply_4(x_9, lean_box(0), lean_box(0), x_10, x_11);
return x_12;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
lean_dec(x_2);
x_13 = lean_ctor_get(x_1, 0);
lean_inc(x_13);
lean_dec(x_1);
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = lean_apply_2(x_14, lean_box(0), x_4);
return x_15;
}
}
}
lean_object* l_Nat_mfoldRevAux___main(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Nat_mfoldRevAux___main___rarg___boxed), 4, 0);
return x_3;
}
}
lean_object* l_Nat_mfoldRevAux___main___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_Nat_mfoldRevAux___main___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_3);
return x_5;
}
}
lean_object* l_Nat_mfoldRevAux___main___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Nat_mfoldRevAux___main(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Nat_mfoldRevAux___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Nat_mfoldRevAux___main___rarg(x_1, x_2, x_3, x_4);
return x_5;
}
}
lean_object* l_Nat_mfoldRevAux(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Nat_mfoldRevAux___rarg___boxed), 4, 0);
return x_3;
}
}
lean_object* l_Nat_mfoldRevAux___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_Nat_mfoldRevAux___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_3);
return x_5;
}
}
lean_object* l_Nat_mfoldRevAux___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Nat_mfoldRevAux(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Nat_mfoldRev___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Nat_mfoldRevAux___main___rarg(x_1, x_2, x_4, x_3);
return x_5;
}
}
lean_object* l_Nat_mfoldRev(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Nat_mfoldRev___rarg___boxed), 4, 0);
return x_3;
}
}
lean_object* l_Nat_mfoldRev___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_Nat_mfoldRev___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_4);
return x_5;
}
}
lean_object* l_Nat_mfoldRev___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Nat_mfoldRev(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_List_mmap___main___rarg___lambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{

60
src/stage0/init/control/estate.c
View file

@ -39,7 +39,6 @@ lean_object* l_EState_adaptExcept___rarg(lean_object*, lean_object*, lean_object
lean_object* l_EState_Result_toString___rarg___closed__1;
lean_object* l_EState_bind(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Except_toString___rarg___closed__2;
lean_object* l_EState_modify(lean_object*, lean_object*);
lean_object* l_EState_unreachableError___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_EState_Monad___closed__2;
@ -50,7 +49,6 @@ lean_object* l_EState_Monad___closed__4;
lean_object* l_EState_HasOrelse(lean_object*, lean_object*, lean_object*);
lean_object* l_EState_Monad___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_EState_MonadExcept___closed__3;
lean_object* l_EState_modify___rarg(lean_object*, lean_object*);
lean_object* l_EState_Monad___closed__10;
lean_object* l_EState_catch___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_EState_get(lean_object*, lean_object*);
@ -60,6 +58,7 @@ lean_object* l_EState_HasRepr(lean_object*, lean_object*, lean_object*);
lean_object* l_EState_MonadState___closed__2;
lean_object* l_EState_Monad___closed__3;
lean_object* l_EState_Monad___closed__9;
lean_object* l_EState_modifyGet___rarg(lean_object*, lean_object*);
lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_EState_Monad___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_EState_Monad___closed__8;
@ -76,6 +75,7 @@ lean_object* l_EState_HasToString___rarg(lean_object*, lean_object*);
lean_object* l_EState_map(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_EState_orelse_x27___rarg(lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* l_EState_Inhabited(lean_object*, lean_object*, lean_object*);
lean_object* l_EState_modifyGet(lean_object*, lean_object*, lean_object*);
lean_object* l_EState_MonadExcept___closed__1;
lean_object* l_EState_MonadExcept(lean_object*, lean_object*);
lean_object* l_EState_catch(lean_object*, lean_object*, lean_object*);
@ -400,44 +400,52 @@ x_3 = lean_alloc_closure((void*)(l_EState_get___rarg), 1, 0);
return x_3;
}
}
lean_object* l_EState_modify___rarg(lean_object* x_1, lean_object* x_2) {
lean_object* l_EState_modifyGet___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = !lean_is_exclusive(x_2);
if (x_3 == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_4 = lean_ctor_get(x_2, 1);
x_5 = lean_ctor_get(x_2, 0);
lean_dec(x_5);
x_6 = lean_apply_1(x_1, x_4);
x_7 = lean_box(0);
lean_ctor_set(x_2, 1, x_6);
x_7 = lean_ctor_get(x_6, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_6, 1);
lean_inc(x_8);
lean_dec(x_6);
lean_ctor_set(x_2, 1, x_8);
lean_ctor_set(x_2, 0, x_7);
return x_2;
}
else
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_8 = lean_ctor_get(x_2, 1);
lean_inc(x_8);
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_9 = lean_ctor_get(x_2, 1);
lean_inc(x_9);
lean_dec(x_2);
x_9 = lean_apply_1(x_1, x_8);
x_10 = lean_box(0);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_11, 1, x_9);
return x_11;
x_10 = lean_apply_1(x_1, x_9);
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_10, 1);
lean_inc(x_12);
lean_dec(x_10);
x_13 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
return x_13;
}
}
}
lean_object* l_EState_modify(lean_object* x_1, lean_object* x_2) {
lean_object* l_EState_modifyGet(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_EState_modify___rarg), 2, 0);
return x_3;
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_EState_modifyGet___rarg), 2, 0);
return x_4;
}
}
lean_object* l_EState_throw___rarg(lean_object* x_1, lean_object* x_2) {
@ -1501,7 +1509,9 @@ lean_object* _init_l_EState_MonadState___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_EState_get___rarg), 1, 0);
x_1 = lean_alloc_closure((void*)(l_EState_modifyGet), 3, 2);
lean_closure_set(x_1, 0, lean_box(0));
lean_closure_set(x_1, 1, lean_box(0));
return x_1;
}
}
@ -1509,7 +1519,7 @@ lean_object* _init_l_EState_MonadState___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_EState_set___rarg), 2, 0);
x_1 = lean_alloc_closure((void*)(l_EState_get___rarg), 1, 0);
return x_1;
}
}
@ -1517,7 +1527,7 @@ lean_object* _init_l_EState_MonadState___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_EState_modify___rarg), 2, 0);
x_1 = lean_alloc_closure((void*)(l_EState_set___rarg), 2, 0);
return x_1;
}
}
@ -1525,9 +1535,9 @@ lean_object* _init_l_EState_MonadState___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_EState_MonadState___closed__1;
x_2 = l_EState_MonadState___closed__2;
x_3 = l_EState_MonadState___closed__3;
x_1 = l_EState_MonadState___closed__2;
x_2 = l_EState_MonadState___closed__3;
x_3 = l_EState_MonadState___closed__1;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);

120
src/stage0/init/control/state.c
View file

@ -60,23 +60,25 @@ lean_object* l_StateT_set___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_failure(lean_object*, lean_object*, lean_object*);
lean_object* l_getModify(lean_object*, lean_object*);
lean_object* l_monadStateRunnerTrans___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_modifyGet___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_MonadStateAdapter_adaptState_x27___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_MonadExcept___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
lean_object* l_monadStateRunnerTrans___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_orelse___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_MonadExcept(lean_object*, lean_object*);
lean_object* l_StateT_modifyGet(lean_object*, lean_object*);
lean_object* l_monadStateRunnerTrans(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_HasMonadLift___rarg(lean_object*);
lean_object* l_StateT_set___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_getModify___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_monadStateAdapterTrans(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_monadStateTrans___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
lean_object* l_monadStateTrans___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_Monad___rarg___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_Monad___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_monadStateAdapterTrans___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_modify___boxed(lean_object*, lean_object*);
lean_object* l_StateT_MonadExcept___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_run___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_modify___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_map___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_run_x27___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_MonadStateAdapter_adaptState_x27___rarg___lambda__1(lean_object*, lean_object*);
@ -89,15 +91,19 @@ lean_object* l_monadStateTrans___rarg___lambda__1(lean_object*, lean_object*, le
lean_object* l_StateT_MonadFunctor___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_MonadStateAdapter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_MonadFunctor___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_modify___rarg(lean_object*, lean_object*);
lean_object* l_StateT_set___boxed(lean_object*, lean_object*);
lean_object* l_StateT_run(lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_MonadRun(lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_map___boxed(lean_object*, lean_object*);
lean_object* l_getModify___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_modify___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_StateT_MonadStateAdapter(lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_bind(lean_object*, lean_object*);
lean_object* l_StateT_HasMonadLift(lean_object*, lean_object*);
lean_object* l_StateT_modifyGet___boxed(lean_object*, lean_object*);
lean_object* l_StateT_MonadExcept___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_modify(lean_object*, lean_object*);
lean_object* l_StateT_failure___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_map(lean_object*, lean_object*);
lean_object* l_StateT_Alternative(lean_object*, lean_object*);
@ -108,11 +114,9 @@ lean_object* l_StateT_Monad___rarg___lambda__3(lean_object*, lean_object*, lean_
lean_object* l_StateT_MonadState(lean_object*, lean_object*);
lean_object* l_StateT_pure(lean_object*, lean_object*);
lean_object* l_StateT_failure___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_modify___boxed(lean_object*, lean_object*);
lean_object* l_StateT_get___rarg(lean_object*, lean_object*);
lean_object* l_StateT_Monad___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_StateT_Alternative___rarg(lean_object*, lean_object*);
lean_object* l_StateT_modify(lean_object*, lean_object*);
lean_object* l_StateT_run_x27___rarg___lambda__1(lean_object*);
lean_object* l_StateT_MonadState___rarg(lean_object*);
lean_object* l_StateT_MonadStateRunner(lean_object*, lean_object*);
@ -741,38 +745,34 @@ lean_dec(x_2);
return x_3;
}
}
lean_object* l_StateT_modify___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_StateT_modifyGet___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_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;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_ctor_get(x_4, 1);
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_5 = lean_ctor_get(x_1, 0);
lean_inc(x_5);
lean_dec(x_4);
x_6 = lean_apply_1(x_2, x_3);
x_7 = lean_box(0);
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_6);
x_9 = lean_apply_2(x_5, lean_box(0), x_8);
return x_9;
lean_dec(x_1);
x_6 = lean_ctor_get(x_5, 1);
lean_inc(x_6);
lean_dec(x_5);
x_7 = lean_apply_1(x_3, x_4);
x_8 = lean_apply_2(x_6, lean_box(0), x_7);
return x_8;
}
}
lean_object* l_StateT_modify(lean_object* x_1, lean_object* x_2) {
lean_object* l_StateT_modifyGet(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_StateT_modify___rarg), 3, 0);
x_3 = lean_alloc_closure((void*)(l_StateT_modifyGet___rarg), 4, 0);
return x_3;
}
}
lean_object* l_StateT_modify___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l_StateT_modifyGet___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_StateT_modify(x_1, x_2);
x_3 = l_StateT_modifyGet(x_1, x_2);
lean_dec(x_2);
return x_3;
}
@ -1034,6 +1034,48 @@ lean_dec(x_2);
return x_3;
}
}
lean_object* l_modify___rarg___lambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = lean_apply_1(x_1, x_2);
x_4 = lean_box(0);
x_5 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_5, 0, x_4);
lean_ctor_set(x_5, 1, x_3);
return x_5;
}
}
lean_object* l_modify___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, 2);
lean_inc(x_3);
lean_dec(x_1);
x_4 = lean_alloc_closure((void*)(l_modify___rarg___lambda__1), 2, 1);
lean_closure_set(x_4, 0, x_2);
x_5 = lean_apply_2(x_3, lean_box(0), x_4);
return x_5;
}
}
lean_object* l_modify(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_modify___rarg), 2, 0);
return x_3;
}
}
lean_object* l_modify___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_modify(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_getModify___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -1051,16 +1093,18 @@ return x_6;
lean_object* l_getModify___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_6 = lean_ctor_get(x_1, 2);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_apply_1(x_6, x_2);
x_8 = lean_alloc_closure((void*)(l_getModify___rarg___lambda__1___boxed), 3, 2);
lean_closure_set(x_8, 0, x_3);
lean_closure_set(x_8, 1, x_5);
x_9 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_7, x_8);
return x_9;
x_7 = lean_alloc_closure((void*)(l_modify___rarg___lambda__1), 2, 1);
lean_closure_set(x_7, 0, x_2);
x_8 = lean_apply_2(x_6, lean_box(0), x_7);
x_9 = lean_alloc_closure((void*)(l_getModify___rarg___lambda__1___boxed), 3, 2);
lean_closure_set(x_9, 0, x_3);
lean_closure_set(x_9, 1, x_5);
x_10 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_8, x_9);
return x_10;
}
}
lean_object* l_getModify___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@ -1119,16 +1163,16 @@ x_6 = lean_apply_2(x_2, lean_box(0), x_5);
return x_6;
}
}
lean_object* l_monadStateTrans___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_monadStateTrans___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_1, 2);
lean_inc(x_4);
lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = lean_ctor_get(x_1, 2);
lean_inc(x_5);
lean_dec(x_1);
x_5 = lean_apply_1(x_4, x_3);
x_6 = lean_apply_2(x_2, lean_box(0), x_5);
return x_6;
x_6 = lean_apply_2(x_5, lean_box(0), x_4);
x_7 = lean_apply_2(x_2, lean_box(0), x_6);
return x_7;
}
}
lean_object* l_monadStateTrans___rarg(lean_object* x_1, lean_object* x_2) {
@ -1144,7 +1188,7 @@ lean_inc(x_2);
x_5 = lean_alloc_closure((void*)(l_monadStateTrans___rarg___lambda__1), 3, 2);
lean_closure_set(x_5, 0, x_2);
lean_closure_set(x_5, 1, x_1);
x_6 = lean_alloc_closure((void*)(l_monadStateTrans___rarg___lambda__2), 3, 2);
x_6 = lean_alloc_closure((void*)(l_monadStateTrans___rarg___lambda__2), 4, 2);
lean_closure_set(x_6, 0, x_2);
lean_closure_set(x_6, 1, x_1);
x_7 = lean_alloc_ctor(0, 3, 0);
@ -1182,7 +1226,7 @@ lean_closure_set(x_2, 0, x_1);
lean_inc(x_1);
x_3 = lean_alloc_closure((void*)(l_StateT_set___rarg___boxed), 3, 1);
lean_closure_set(x_3, 0, x_1);
x_4 = lean_alloc_closure((void*)(l_StateT_modify___rarg), 3, 1);
x_4 = lean_alloc_closure((void*)(l_StateT_modifyGet___rarg), 4, 1);
lean_closure_set(x_4, 0, x_1);
x_5 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_5, 0, x_2);

433
src/stage0/init/data/array/basic.c
View file

@ -18,9 +18,13 @@ lean_object* l_Array_anyMAux___main___at_Array_any___spec__1(lean_object*);
lean_object* l_Array_extractAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_ummapAux___main___at_Array_map___spec__1(lean_object*, lean_object*);
lean_object* l_Array_append(lean_object*);
lean_object* l_Array_mk___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlFrom___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldr___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_ummap___boxed(lean_object*, lean_object*);
lean_object* l_Array_foldr___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateRev___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_iterateFrom___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_shrink___main___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Array_mfindRevAux___main___at_Array_findRev___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -35,11 +39,10 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Array_anyMAux___main___at_Array_all___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_getOpt(lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_foldlFrom___spec__1(lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___at_Array_toList___spec__1(lean_object*);
lean_object* l_Array_any(lean_object*);
lean_object* l_List_repr___rarg(lean_object*, lean_object*);
lean_object* l_Array_swap___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_revFoldl(lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___boxed(lean_object*, lean_object*);
lean_object* l_Array_mfor___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_extract___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterate___boxed(lean_object*, lean_object*);
@ -48,23 +51,22 @@ lean_object* l_Array_iterate___rarg___boxed(lean_object*, lean_object*, lean_obj
lean_object* l_Array_mfoldl___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_iterateFrom___spec__1(lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_iterate___spec__1(lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_foldlFrom___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_reverse(lean_object*);
lean_object* l_Array_filter(lean_object*);
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___at_Array_toList___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyMAux___main___at_Array_allM___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mfoldl_u2082___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__revIterateAux(lean_object*, lean_object*);
lean_object* l_Array_ummapAux___main___at_Array_ummap___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_all___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_mfoldlFrom___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_mfoldlFrom___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Array_shrink___rarg(lean_object*, lean_object*);
lean_object* l_Array_fswap___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_mfoldr___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Array_extractAux(lean_object*);
lean_object* l_Array_HasRepr(lean_object*);
lean_object* l_Array_ummapAux___main___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_iterateRev___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_allM___boxed(lean_object*, lean_object*);
lean_object* l_Array_eraseIdxAux___rarg(lean_object*, lean_object*);
lean_object* l_Array_iterate_u2082___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -77,14 +79,16 @@ lean_object* l_Array_mfoldlFrom___boxed(lean_object*, lean_object*);
lean_object* l_Array_HasBeq(lean_object*);
lean_object* l_Array_ummapAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_ummapIdx(lean_object*, lean_object*);
lean_object* l_Array_mfoldr(lean_object*, lean_object*);
lean_object* l_Array_size___boxed(lean_object*, lean_object*);
lean_object* l_Array_uset___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__revIterateAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_iterateFrom___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mfindRevAux(lean_object*, lean_object*);
lean_object* l_Array_anyMAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_iterateRev___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_toArrayAux___main___rarg(lean_object*, lean_object*);
lean_object* l_Array_isEqv___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_mfoldr___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_fswapAt___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mfoldlFrom___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_uget(lean_object*, lean_object*, size_t, lean_object*);
@ -97,7 +101,6 @@ lean_object* l_Array_miterateAux___main___at_Array_mfoldlFrom___spec__1___rarg__
lean_object* l_List_redLength___main___rarg(lean_object*);
lean_object* l_Array_indexOfAux___main(lean_object*);
lean_object* l_Array_fswap(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__revIterateAux___main(lean_object*, lean_object*);
lean_object* l_Array_mfoldl___boxed(lean_object*, lean_object*);
lean_object* l_Array_mfind(lean_object*, lean_object*);
lean_object* l_Array_mfindAux___main___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -110,6 +113,7 @@ lean_object* l_Array_miterateAux___main___at_Array_mfoldl___spec__1(lean_object*
lean_object* l_Array_miterateAux___main___at_Array_iterate___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_pop___boxed(lean_object*, lean_object*);
lean_object* l_Array_eraseIdxSzAux(lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlFrom___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyMAux___main___at_Array_all___spec__1(lean_object*);
lean_object* l_Array_mfindRevAux___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -119,12 +123,14 @@ lean_object* l_Array_indexOfAux(lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_mmapIdx___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_List_redLength(lean_object*);
lean_object* l_Array_mkEmpty(lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_ummap___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterate_u2082Aux___main___at_Array_mfoldl_u2082___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_List_toArrayAux(lean_object*);
lean_object* l_Array_eraseIdxSzAuxInstance(lean_object*);
lean_object* l_Array_feraseIdx(lean_object*);
lean_object* l_Array_mkArray___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateRev___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_extract(lean_object*);
lean_object* l_Array_eraseIdx(lean_object*);
lean_object* l_Array_mfindAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -133,6 +139,7 @@ lean_object* l_Array_map___rarg(lean_object*, lean_object*);
lean_object* l_Array_feraseIdx___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Array_empty(lean_object*);
lean_object* l_Array_swap(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_HasEmptyc(lean_object*);
lean_object* l_Array_extractAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_redLength___main___rarg___boxed(lean_object*);
@ -146,12 +153,15 @@ lean_object* l_Array_indexOfAux___rarg(lean_object*, lean_object*, lean_object*,
lean_object* l_Array_get___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mfindRev___boxed(lean_object*, lean_object*);
lean_object* l_Array_miterate_u2082Aux___boxed(lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_mfoldr___spec__1(lean_object*, lean_object*);
lean_object* l_Array_eraseIdx_x27___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Array_mmapIdx___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterate(lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_mmap___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mfindAux___boxed(lean_object*, lean_object*);
lean_object* l_Array_mfor(lean_object*);
lean_object* l_Array_mfoldr___boxed(lean_object*, lean_object*);
lean_object* l_Array_mfindAux___main___at_Array_find___spec__1(lean_object*, lean_object*);
lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_mfoldl___spec__1___boxed(lean_object*, lean_object*);
@ -164,14 +174,17 @@ lean_object* l_Array_isEqv(lean_object*);
lean_object* l_Array_mfind___boxed(lean_object*, lean_object*);
lean_object* l_Array_mfindAux___main(lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_mmapIdx___spec__1(lean_object*, lean_object*);
lean_object* l_Array_miterateRev___boxed(lean_object*, lean_object*);
lean_object* l_Array_miterateAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mfindAux___main___boxed(lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_foldr___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_toString___rarg(lean_object*, lean_object*);
lean_object* l_Array_miterate_u2082Aux(lean_object*, lean_object*);
lean_object* l_Array_revFoldl___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_foldlFrom___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_swapAt___rarg___boxed(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Array_mk(lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_foldr___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterate_u2082(lean_object*, lean_object*);
lean_object* l_Array_mfindRevAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main(lean_object*, lean_object*);
@ -185,29 +198,31 @@ lean_object* l_Array_miterate_u2082Aux___main___at_Array_mfoldl_u2082___spec__1_
lean_object* l_Array_mfindAux___main___at_Array_find___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_ummapAux(lean_object*, lean_object*);
lean_object* l_Array_mfindRevAux___main___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___at_Array_revFoldl___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyMAux___main___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_filterAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_mmap___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateRev(lean_object*, lean_object*);
lean_object* l_Array_fget(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mforAux___main___boxed(lean_object*);
lean_object* l_Array_singleton___rarg(lean_object*);
lean_object* l_Array_mfindRevAux___boxed(lean_object*, lean_object*);
lean_object* l_Array_mmapIdx___boxed(lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___at_Array_toList___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Array_anyMAux___main___at_Array_all___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_filter___rarg(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Array_findRev___rarg(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_mfoldr___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Array_isEmpty___rarg(lean_object*);
uint8_t l_Array_any___rarg(lean_object*, lean_object*);
lean_object* l_Array_ummapAux___main___at_Array_mapIdx___spec__1(lean_object*, lean_object*);
lean_object* l_Array_push(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateFrom(lean_object*, lean_object*);
lean_object* l_Array_foldr(lean_object*, lean_object*);
lean_object* l_Array_anyMAux___main(lean_object*, lean_object*);
lean_object* l_Array_eraseIdxAux___main(lean_object*);
lean_object* l_Array_mforAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_iterateRev___spec__1(lean_object*, lean_object*);
lean_object* l_Array_indexOfAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_eraseIdx___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Array_push___boxed(lean_object*, lean_object*, lean_object*);
@ -230,9 +245,8 @@ lean_object* l_Array_iterateFrom___rarg___boxed(lean_object*, lean_object*, lean
lean_object* l_Array_back(lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_mmap___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_ummapAux___main___at_Array_map___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___at_Array_revFoldl___spec__1(lean_object*, lean_object*);
lean_object* l_Array_isEqvAux___main(lean_object*);
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___at_Array_revFoldl___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_data(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyMAux___main___at_Array_allM___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Array_ummapAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_ummapIdx___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -252,7 +266,6 @@ lean_object* l_Array_sz___boxed(lean_object*, lean_object*);
lean_object* l_Array_Inhabited(lean_object*);
lean_object* l_Array_miterate_u2082Aux___main___at_Array_iterate_u2082___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_modify___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_revIterate___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_HasRepr___rarg___closed__1;
lean_object* l_Array_HasToString(lean_object*);
lean_object* l_Array_singleton(lean_object*);
@ -274,17 +287,22 @@ lean_object* l_Array_reverseAux___main___rarg(lean_object*, lean_object*);
lean_object* l_Array_anyMAux___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Array_eraseIdxSzAuxInstance___rarg(lean_object*);
lean_object* l_Array_pop(lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main(lean_object*, lean_object*);
lean_object* l_Array_findRev___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Array_sz(lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_toList___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux(lean_object*, lean_object*);
lean_object* l_Array_extractAux___main(lean_object*);
lean_object* l_Array_miterate_u2082Aux___main___at_Array_iterate_u2082___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_ummapAux___boxed(lean_object*, lean_object*);
lean_object* l_Array_mfindAux___main___at_Array_find___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_modify___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateRev___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_size(lean_object*, lean_object*);
lean_object* l_Array_eraseIdx_x27___rarg(lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_foldr___spec__1(lean_object*, lean_object*);
lean_object* l_Array_mforAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_toList___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_isEmpty(lean_object*);
lean_object* l_Array_eraseIdxSzAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mfoldl_u2082___boxed(lean_object*, lean_object*);
@ -315,7 +333,6 @@ uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Array_iterate_u2082___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mfoldlFrom(lean_object*, lean_object*);
lean_object* l_Array_iterate_u2082(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_revIterate___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_foldl___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_ummapAux___main___at_Array_ummap___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_any___rarg___boxed(lean_object*, lean_object*);
@ -327,10 +344,11 @@ lean_object* l_Array_miterateAux___main___at_Array_append___spec__1___rarg___box
lean_object* lean_nat_div(lean_object*, lean_object*);
lean_object* l_Array_isEqvAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_append___spec__1(lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_toList___spec__1(lean_object*);
lean_object* l_Array_mfindRevAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_feraseIdx___rarg(lean_object*, lean_object*);
lean_object* l_Array_HasToString___rarg(lean_object*);
lean_object* l___private_init_data_array_basic_2__revIterateAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mfoldr___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_mfoldl___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_reverse___rarg(lean_object*);
lean_object* l_Array_mfor___boxed(lean_object*);
@ -339,13 +357,13 @@ lean_object* l_Array_mmap___boxed(lean_object*, lean_object*);
lean_object* l_Array_set(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_find(lean_object*, lean_object*);
lean_object* l_Array_swapAt___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux___boxed(lean_object*, lean_object*);
lean_object* l_Array_eraseIdxSzAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_mmap___spec__1(lean_object*, lean_object*);
lean_object* l_Array_miterate_u2082Aux___main___at_Array_mfoldl_u2082___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterate_u2082Aux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyMAux___main___at_Array_allM___spec__1(lean_object*, lean_object*);
lean_object* l_Array_revIterate(lean_object*, lean_object*);
lean_object* l_Array_mforAux___boxed(lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_mfoldl___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_getOpt___rarg___boxed(lean_object*, lean_object*);
@ -358,19 +376,20 @@ lean_object* l_Array_mfindRevAux___main___at_Array_findRev___spec__1(lean_object
lean_object* l_Array_find___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Array_toList(lean_object*);
lean_object* l_Array_set___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_data___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_append___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_indexOf___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_revFoldl___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_reverseAux(lean_object*);
lean_object* l_Array_foldl___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterate_u2082Aux___main___at_Array_mfoldl_u2082___spec__1(lean_object*, lean_object*);
lean_object* l_Array_isEqvAux(lean_object*);
lean_object* l_List_toArrayAux___main(lean_object*);
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_redLength___rarg___boxed(lean_object*);
lean_object* l___private_init_data_array_basic_2__miterateRevAux(lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Array_foldl___spec__1(lean_object*, lean_object*);
lean_object* l_Array_ummapAux___main___boxed(lean_object*, lean_object*);
lean_object* l_Array_indexOfAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateRev(lean_object*, lean_object*);
lean_object* l_Array_HasAppend(lean_object*);
lean_object* l_Array_modify(lean_object*);
lean_object* l_Array_mfindAux(lean_object*, lean_object*);
@ -389,6 +408,22 @@ lean_object* l_Array_back___rarg(lean_object*, lean_object*);
lean_object* l_List_redLength___rarg(lean_object*);
lean_object* l_Array_anyMAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mforAux___main(lean_object*);
lean_object* l_Array_mk___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_array_mk(x_2, x_3);
return x_4;
}
}
lean_object* l_Array_data___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_array_data(x_2, x_3);
return x_4;
}
}
lean_object* l_Array_sz___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -2831,104 +2866,235 @@ x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___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_6; uint8_t x_7;
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_nat_dec_eq(x_3, x_6);
if (x_7 == 0)
lean_object* x_8; uint8_t x_9;
x_8 = lean_unsigned_to_nat(0u);
x_9 = lean_nat_dec_eq(x_5, x_8);
if (x_9 == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_8 = lean_unsigned_to_nat(1u);
x_9 = lean_nat_sub(x_3, x_8);
lean_dec(x_3);
x_10 = lean_array_fget(x_1, x_9);
lean_inc(x_2);
lean_inc(x_9);
x_11 = lean_apply_3(x_2, x_9, x_10, x_5);
x_3 = x_9;
x_4 = lean_box(0);
x_5 = x_11;
goto _start;
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;
x_10 = lean_unsigned_to_nat(1u);
x_11 = lean_nat_sub(x_5, x_10);
x_12 = lean_ctor_get(x_1, 1);
lean_inc(x_12);
x_13 = lean_array_fget(x_3, x_11);
lean_inc(x_4);
lean_inc(x_11);
x_14 = lean_apply_3(x_4, x_11, x_13, x_7);
x_15 = lean_alloc_closure((void*)(l___private_init_data_array_basic_2__miterateRevAux___main___rarg___boxed), 7, 6);
lean_closure_set(x_15, 0, x_1);
lean_closure_set(x_15, 1, lean_box(0));
lean_closure_set(x_15, 2, x_3);
lean_closure_set(x_15, 3, x_4);
lean_closure_set(x_15, 4, x_11);
lean_closure_set(x_15, 5, lean_box(0));
x_16 = lean_apply_4(x_12, lean_box(0), lean_box(0), x_14, x_15);
return x_16;
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19;
lean_dec(x_4);
lean_dec(x_3);
x_17 = lean_ctor_get(x_1, 0);
lean_inc(x_17);
lean_dec(x_1);
x_18 = lean_ctor_get(x_17, 1);
lean_inc(x_18);
lean_dec(x_17);
x_19 = lean_apply_2(x_18, lean_box(0), x_7);
return x_19;
}
}
}
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l___private_init_data_array_basic_2__miterateRevAux___main___rarg___boxed), 7, 0);
return x_3;
}
}
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___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_array_basic_2__miterateRevAux___main___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_5);
return x_8;
}
}
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l___private_init_data_array_basic_2__miterateRevAux___main(x_1, x_2);
lean_dec(x_2);
return x_5;
}
}
}
lean_object* l___private_init_data_array_basic_2__revIterateAux___main(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l___private_init_data_array_basic_2__revIterateAux___main___rarg___boxed), 5, 0);
return x_3;
}
}
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l___private_init_data_array_basic_2__miterateRevAux___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_6;
x_6 = l___private_init_data_array_basic_2__revIterateAux___main___rarg(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_1);
return x_6;
lean_object* x_8;
x_8 = l___private_init_data_array_basic_2__miterateRevAux___main___rarg(x_1, lean_box(0), x_3, x_4, x_5, lean_box(0), x_7);
return x_8;
}
}
lean_object* l___private_init_data_array_basic_2__revIterateAux___rarg(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_init_data_array_basic_2__revIterateAux___main___rarg(x_1, x_2, x_3, lean_box(0), x_5);
return x_6;
}
}
lean_object* l___private_init_data_array_basic_2__revIterateAux(lean_object* x_1, lean_object* x_2) {
lean_object* l___private_init_data_array_basic_2__miterateRevAux(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l___private_init_data_array_basic_2__revIterateAux___rarg___boxed), 5, 0);
x_3 = lean_alloc_closure((void*)(l___private_init_data_array_basic_2__miterateRevAux___rarg___boxed), 7, 0);
return x_3;
}
}
lean_object* l___private_init_data_array_basic_2__revIterateAux___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l___private_init_data_array_basic_2__miterateRevAux___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_6;
x_6 = l___private_init_data_array_basic_2__revIterateAux___rarg(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_1);
return x_6;
lean_object* x_8;
x_8 = l___private_init_data_array_basic_2__miterateRevAux___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_5);
return x_8;
}
}
lean_object* l_Array_revIterate___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_array_get_size(x_1);
x_5 = l___private_init_data_array_basic_2__revIterateAux___main___rarg(x_1, x_3, x_4, lean_box(0), x_2);
return x_5;
}
}
lean_object* l_Array_revIterate(lean_object* x_1, lean_object* x_2) {
lean_object* l___private_init_data_array_basic_2__miterateRevAux___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Array_revIterate___rarg___boxed), 3, 0);
x_3 = l___private_init_data_array_basic_2__miterateRevAux(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Array_revIterate___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Array_miterateRev___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_4;
x_4 = l_Array_revIterate___rarg(x_1, x_2, x_3);
lean_object* x_6; lean_object* x_7;
x_6 = lean_array_get_size(x_3);
x_7 = l___private_init_data_array_basic_2__miterateRevAux___main___rarg(x_1, lean_box(0), x_3, x_5, x_6, lean_box(0), x_4);
lean_dec(x_6);
return x_7;
}
}
lean_object* l_Array_miterateRev(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Array_miterateRev___rarg), 5, 0);
return x_3;
}
}
lean_object* l_Array_miterateRev___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Array_miterateRev(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_mfoldr___spec__1___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 = lean_unsigned_to_nat(0u);
x_10 = lean_nat_dec_eq(x_6, x_9);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_11 = lean_unsigned_to_nat(1u);
x_12 = lean_nat_sub(x_6, x_11);
x_13 = lean_ctor_get(x_1, 1);
lean_inc(x_13);
x_14 = lean_array_fget(x_5, x_12);
lean_inc(x_3);
x_15 = lean_apply_2(x_3, x_14, x_8);
x_16 = lean_alloc_closure((void*)(l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_mfoldr___spec__1___rarg___boxed), 8, 7);
lean_closure_set(x_16, 0, x_1);
lean_closure_set(x_16, 1, lean_box(0));
lean_closure_set(x_16, 2, x_3);
lean_closure_set(x_16, 3, x_4);
lean_closure_set(x_16, 4, x_5);
lean_closure_set(x_16, 5, x_12);
lean_closure_set(x_16, 6, lean_box(0));
x_17 = lean_apply_4(x_13, lean_box(0), lean_box(0), x_15, x_16);
return x_17;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_18 = lean_ctor_get(x_1, 0);
lean_inc(x_18);
lean_dec(x_1);
return x_4;
x_19 = lean_ctor_get(x_18, 1);
lean_inc(x_19);
lean_dec(x_18);
x_20 = lean_apply_2(x_19, lean_box(0), x_8);
return x_20;
}
}
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___at_Array_revFoldl___spec__1___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* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_mfoldr___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_mfoldr___spec__1___rarg___boxed), 8, 0);
return x_3;
}
}
lean_object* l_Array_mfoldr___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7;
x_6 = lean_array_get_size(x_5);
lean_inc(x_5);
x_7 = l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_mfoldr___spec__1___rarg(x_1, lean_box(0), x_3, x_5, x_5, x_6, lean_box(0), x_4);
lean_dec(x_6);
return x_7;
}
}
lean_object* l_Array_mfoldr(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Array_mfoldr___rarg), 5, 0);
return x_3;
}
}
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_mfoldr___spec__1___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_array_basic_2__miterateRevAux___main___at_Array_mfoldr___spec__1___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_6);
return x_9;
}
}
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_mfoldr___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_mfoldr___spec__1(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Array_mfoldr___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Array_mfoldr(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_iterateRev___spec__1___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;
@ -2942,7 +3108,8 @@ x_10 = lean_nat_sub(x_4, x_9);
lean_dec(x_4);
x_11 = lean_array_fget(x_3, x_10);
lean_inc(x_2);
x_12 = lean_apply_2(x_2, x_11, x_6);
lean_inc(x_10);
x_12 = lean_apply_3(x_2, x_10, x_11, x_6);
x_4 = x_10;
x_5 = lean_box(0);
x_6 = x_12;
@ -2956,51 +3123,123 @@ return x_6;
}
}
}
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___at_Array_revFoldl___spec__1(lean_object* x_1, lean_object* x_2) {
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_iterateRev___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l___private_init_data_array_basic_2__revIterateAux___main___at_Array_revFoldl___spec__1___rarg___boxed), 6, 0);
x_3 = lean_alloc_closure((void*)(l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_iterateRev___spec__1___rarg___boxed), 6, 0);
return x_3;
}
}
lean_object* l_Array_revFoldl___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Array_iterateRev___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_array_get_size(x_1);
x_5 = l___private_init_data_array_basic_2__revIterateAux___main___at_Array_revFoldl___spec__1___rarg(x_1, x_3, x_1, x_4, lean_box(0), x_2);
x_5 = l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_iterateRev___spec__1___rarg(x_1, x_3, x_1, x_4, lean_box(0), x_2);
return x_5;
}
}
lean_object* l_Array_revFoldl(lean_object* x_1, lean_object* x_2) {
lean_object* l_Array_iterateRev(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Array_revFoldl___rarg___boxed), 3, 0);
x_3 = lean_alloc_closure((void*)(l_Array_iterateRev___rarg___boxed), 3, 0);
return x_3;
}
}
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___at_Array_revFoldl___spec__1___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* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_iterateRev___spec__1___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_array_basic_2__revIterateAux___main___at_Array_revFoldl___spec__1___rarg(x_1, x_2, x_3, x_4, x_5, x_6);
x_7 = l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_iterateRev___spec__1___rarg(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_3);
lean_dec(x_1);
return x_7;
}
}
lean_object* l_Array_revFoldl___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Array_iterateRev___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Array_revFoldl___rarg(x_1, x_2, x_3);
x_4 = l_Array_iterateRev___rarg(x_1, x_2, x_3);
lean_dec(x_1);
return x_4;
}
}
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___at_Array_toList___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_foldr___spec__1___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 = lean_unsigned_to_nat(0u);
x_8 = lean_nat_dec_eq(x_4, x_7);
if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_unsigned_to_nat(1u);
x_10 = lean_nat_sub(x_4, x_9);
lean_dec(x_4);
x_11 = lean_array_fget(x_3, x_10);
lean_inc(x_1);
x_12 = lean_apply_2(x_1, x_11, x_6);
x_4 = x_10;
x_5 = lean_box(0);
x_6 = x_12;
goto _start;
}
else
{
lean_dec(x_4);
lean_dec(x_1);
return x_6;
}
}
}
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_foldr___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_foldr___spec__1___rarg___boxed), 6, 0);
return x_3;
}
}
lean_object* l_Array_foldr___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_array_get_size(x_3);
x_5 = l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_foldr___spec__1___rarg(x_1, x_3, x_3, x_4, lean_box(0), x_2);
return x_5;
}
}
lean_object* l_Array_foldr(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Array_foldr___rarg___boxed), 3, 0);
return x_3;
}
}
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_foldr___spec__1___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_array_basic_2__miterateRevAux___main___at_Array_foldr___spec__1___rarg(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_3);
lean_dec(x_2);
return x_7;
}
}
lean_object* l_Array_foldr___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Array_foldr___rarg(x_1, x_2, x_3);
lean_dec(x_3);
return x_4;
}
}
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_toList___spec__1___rarg(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; uint8_t x_7;
@ -3028,11 +3267,11 @@ return x_5;
}
}
}
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___at_Array_toList___spec__1(lean_object* x_1) {
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_toList___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_init_data_array_basic_2__revIterateAux___main___at_Array_toList___spec__1___rarg___boxed), 5, 0);
x_2 = lean_alloc_closure((void*)(l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_toList___spec__1___rarg___boxed), 5, 0);
return x_2;
}
}
@ -3042,7 +3281,7 @@ _start:
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = lean_box(0);
x_3 = lean_array_get_size(x_1);
x_4 = l___private_init_data_array_basic_2__revIterateAux___main___at_Array_toList___spec__1___rarg(x_1, x_1, x_3, lean_box(0), x_2);
x_4 = l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_toList___spec__1___rarg(x_1, x_1, x_3, lean_box(0), x_2);
return x_4;
}
}
@ -3054,11 +3293,11 @@ x_2 = lean_alloc_closure((void*)(l_Array_toList___rarg___boxed), 1, 0);
return x_2;
}
}
lean_object* l___private_init_data_array_basic_2__revIterateAux___main___at_Array_toList___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_toList___spec__1___rarg___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_init_data_array_basic_2__revIterateAux___main___at_Array_toList___spec__1___rarg(x_1, x_2, x_3, x_4, x_5);
x_6 = l___private_init_data_array_basic_2__miterateRevAux___main___at_Array_toList___spec__1___rarg(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_6;

73
src/stage0/init/data/nat/basic.c
View file

@ -39,20 +39,25 @@ lean_object* l_Nat_pred(lean_object*);
lean_object* l_Nat_sub___boxed(lean_object*, lean_object*);
lean_object* l_Nat_foldAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_mul___boxed(lean_object*, lean_object*);
lean_object* l_Nat_foldRev(lean_object*);
lean_object* l_Nat_all___boxed(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Nat_ble___boxed(lean_object*, lean_object*);
uint8_t l_Nat_anyAux___main___at_Prod_allI___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_foldRevAux___main___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_HasSub___closed__1;
lean_object* l_Nat_foldRev___rarg(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
uint8_t l_Nat_anyAux___main(lean_object*, lean_object*, lean_object*);
uint8_t l_Nat_anyAux(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_HasPow___closed__1;
lean_object* l_Nat_foldRevAux(lean_object*);
lean_object* l_Nat_repeat___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_foldAux(lean_object*);
lean_object* l_Prod_anyI___boxed(lean_object*, lean_object*);
lean_object* l_Nat_pow___main(lean_object*, lean_object*);
lean_object* l_Nat_HasSub;
lean_object* l_Nat_foldRevAux___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_decLt___boxed(lean_object*, lean_object*);
lean_object* l_Nat_pow___main___boxed(lean_object*, lean_object*);
lean_object* l_Nat_beq___boxed(lean_object*, lean_object*);
@ -73,6 +78,7 @@ uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Nat_anyAux___main___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_repeat(lean_object*);
lean_object* l_Nat_DecidableEq___closed__1;
lean_object* l_Nat_foldRevAux___main(lean_object*);
lean_object* l_Nat_max___boxed(lean_object*, lean_object*);
lean_object* l_Nat_max(lean_object*, lean_object*);
lean_object* l_Nat_DecidableEq;
@ -286,6 +292,73 @@ x_2 = lean_alloc_closure((void*)(l_Nat_fold___rarg), 3, 0);
return x_2;
}
}
lean_object* l_Nat_foldRevAux___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = lean_unsigned_to_nat(0u);
x_5 = lean_nat_dec_eq(x_2, x_4);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = lean_unsigned_to_nat(1u);
x_7 = lean_nat_sub(x_2, x_6);
lean_dec(x_2);
lean_inc(x_1);
lean_inc(x_7);
x_8 = lean_apply_2(x_1, x_7, x_3);
x_2 = x_7;
x_3 = x_8;
goto _start;
}
else
{
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
}
lean_object* l_Nat_foldRevAux___main(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Nat_foldRevAux___main___rarg), 3, 0);
return x_2;
}
}
lean_object* l_Nat_foldRevAux___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Nat_foldRevAux___main___rarg(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Nat_foldRevAux(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Nat_foldRevAux___rarg), 3, 0);
return x_2;
}
}
lean_object* l_Nat_foldRev___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Nat_foldRevAux___main___rarg(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Nat_foldRev(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Nat_foldRev___rarg), 3, 0);
return x_2;
}
}
uint8_t l_Nat_anyAux___main(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{

46
src/stage0/init/data/repr.c
View file

@ -28,7 +28,6 @@ lean_object* l_Sigma_HasRepr___rarg___closed__1;
lean_object* l_List_repr___rarg(lean_object*, lean_object*);
uint8_t l_String_isEmpty(lean_object*);
lean_object* l_List_repr___rarg___closed__3;
lean_object* l_String_Iterator_HasRepr___boxed(lean_object*);
lean_object* l_charToHex(uint32_t);
lean_object* l_Substring_HasRepr(lean_object*);
lean_object* l_Subtype_HasRepr(lean_object*, lean_object*);
@ -84,6 +83,7 @@ lean_object* l_Char_quoteCore___closed__5;
lean_object* l_id_HasRepr___rarg(lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Option_HasRepr(lean_object*);
lean_object* l_String_Iterator_HasRepr___closed__2;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Prod_HasRepr___rarg___closed__1;
lean_object* l_Unit_HasRepr(lean_object*);
@ -127,7 +127,6 @@ lean_object* l_Fin_HasRepr(lean_object*);
lean_object* l_Nat_HasRepr___closed__1;
lean_object* l_String_Iterator_HasRepr(lean_object*);
lean_object* l_Unit_HasRepr___closed__1;
lean_object* l_String_Iterator_remainingToString(lean_object*);
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l_Char_quoteCore___closed__4;
lean_object* l_id_HasRepr___rarg(lean_object* x_1) {
@ -1354,28 +1353,39 @@ lean_object* _init_l_String_Iterator_HasRepr___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string(".mkIterator");
x_1 = lean_mk_string("(String.Iterator.mk ");
return x_1;
}
}
lean_object* _init_l_String_Iterator_HasRepr___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string(" ");
return x_1;
}
}
lean_object* l_String_Iterator_HasRepr(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_String_Iterator_remainingToString(x_1);
x_3 = l_String_quote(x_2);
x_4 = l_String_Iterator_HasRepr___closed__1;
x_5 = lean_string_append(x_3, x_4);
return x_5;
}
}
lean_object* l_String_Iterator_HasRepr___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_String_Iterator_HasRepr(x_1);
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = lean_ctor_get(x_1, 1);
lean_inc(x_3);
lean_dec(x_1);
return x_2;
x_4 = l_String_quote(x_2);
x_5 = l_String_Iterator_HasRepr___closed__1;
x_6 = lean_string_append(x_5, x_4);
lean_dec(x_4);
x_7 = l_String_Iterator_HasRepr___closed__2;
x_8 = lean_string_append(x_6, x_7);
x_9 = l_Nat_repr(x_3);
x_10 = lean_string_append(x_8, x_9);
lean_dec(x_9);
x_11 = l_Option_HasRepr___rarg___closed__3;
x_12 = lean_string_append(x_10, x_11);
return x_12;
}
}
lean_object* l_Fin_HasRepr___rarg(lean_object* x_1) {
@ -1573,6 +1583,8 @@ l_Substring_HasRepr___closed__1 = _init_l_Substring_HasRepr___closed__1();
lean_mark_persistent(l_Substring_HasRepr___closed__1);
l_String_Iterator_HasRepr___closed__1 = _init_l_String_Iterator_HasRepr___closed__1();
lean_mark_persistent(l_String_Iterator_HasRepr___closed__1);
l_String_Iterator_HasRepr___closed__2 = _init_l_String_Iterator_HasRepr___closed__2();
lean_mark_persistent(l_String_Iterator_HasRepr___closed__2);
return w;
}
#ifdef __cplusplus

168
src/stage0/init/data/string/basic.c
View file

@ -49,8 +49,6 @@ uint8_t l_String_isEmpty(lean_object*);
lean_object* l_String_trim___boxed(lean_object*);
lean_object* l_String_foldrAux(lean_object*);
lean_object* l_String_intercalate(lean_object*, lean_object*);
lean_object* l___private_init_data_string_basic_8__lineColumnAux___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_String_lineColumn(lean_object*, lean_object*);
lean_object* l_Nat_repeatAux___main___at_String_pushn___spec__1(uint32_t, lean_object*, lean_object*);
lean_object* l_Substring_prev(lean_object*, lean_object*);
lean_object* l_String_Iterator_hasPrev___boxed(lean_object*);
@ -99,9 +97,7 @@ lean_object* l_Substring_toString(lean_object*);
uint8_t l_String_any(lean_object*, lean_object*);
lean_object* l_Substring_takeRightWhileAux___main___at_Substring_trimRight___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_String_Inhabited;
lean_object* l___private_init_data_string_basic_8__lineColumnAux(lean_object*, lean_object*, lean_object*);
lean_object* l_Substring_next(lean_object*, lean_object*);
lean_object* l___private_init_data_string_basic_8__lineColumnAux___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Substring_trimRight(lean_object*);
lean_object* l_String_anyAux___main___at_Substring_contains___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Substring_extract(lean_object*, lean_object*, lean_object*);
@ -197,7 +193,6 @@ lean_object* l_Substring_drop___boxed(lean_object*, lean_object*);
lean_object* l_String_trimRight___boxed(lean_object*);
lean_object* l_Substring_splitAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_String_singleton(uint32_t);
lean_object* l___private_init_data_string_basic_8__lineColumnAux___main___boxed(lean_object*, lean_object*, lean_object*);
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
lean_object* l_String_anyAux___main___at_String_all___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -304,7 +299,6 @@ lean_object* l_Substring_prev___boxed(lean_object*, lean_object*);
lean_object* l_Substring_take(lean_object*, lean_object*);
uint8_t l_String_anyAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Substring_foldr___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_String_lineColumn___closed__1;
lean_object* l_String_trimRight(lean_object*);
lean_object* l_Substring_takeRight___boxed(lean_object*, lean_object*);
uint32_t l_String_back(lean_object*);
@ -314,7 +308,6 @@ lean_object* l_String_Iterator_remainingToString(lean_object*);
lean_object* l_String_splitAux___main___closed__1;
lean_object* lean_string_utf8_set(lean_object*, lean_object*, uint32_t);
lean_object* lean_string_length(lean_object*);
lean_object* l_String_lineColumn___boxed(lean_object*, lean_object*);
lean_object* l_String_mk___boxed(lean_object* x_1) {
_start:
{
@ -2093,165 +2086,6 @@ x_3 = l_String_Iterator_prevn___main(x_1, x_2);
return x_3;
}
}
lean_object* l___private_init_data_string_basic_8__lineColumnAux___main(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; uint8_t x_6;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_ctor_get(x_3, 1);
lean_inc(x_5);
x_6 = lean_string_utf8_at_end(x_1, x_2);
if (x_6 == 0)
{
uint8_t x_7;
x_7 = !lean_is_exclusive(x_3);
if (x_7 == 0)
{
lean_object* x_8; lean_object* x_9; uint32_t x_10; uint32_t x_11; uint8_t x_12;
x_8 = lean_ctor_get(x_3, 1);
lean_dec(x_8);
x_9 = lean_ctor_get(x_3, 0);
lean_dec(x_9);
x_10 = lean_string_utf8_get(x_1, x_2);
x_11 = 10;
x_12 = x_10 == x_11;
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_13 = lean_string_utf8_next(x_1, x_2);
lean_dec(x_2);
x_14 = lean_unsigned_to_nat(1u);
x_15 = lean_nat_add(x_5, x_14);
lean_dec(x_5);
lean_ctor_set(x_3, 1, x_15);
x_2 = x_13;
goto _start;
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_dec(x_5);
x_17 = lean_string_utf8_next(x_1, x_2);
lean_dec(x_2);
x_18 = lean_unsigned_to_nat(1u);
x_19 = lean_nat_add(x_4, x_18);
lean_dec(x_4);
x_20 = lean_unsigned_to_nat(0u);
lean_ctor_set(x_3, 1, x_20);
lean_ctor_set(x_3, 0, x_19);
x_2 = x_17;
goto _start;
}
}
else
{
uint32_t x_22; uint32_t x_23; uint8_t x_24;
lean_dec(x_3);
x_22 = lean_string_utf8_get(x_1, x_2);
x_23 = 10;
x_24 = x_22 == x_23;
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_25 = lean_string_utf8_next(x_1, x_2);
lean_dec(x_2);
x_26 = lean_unsigned_to_nat(1u);
x_27 = lean_nat_add(x_5, x_26);
lean_dec(x_5);
x_28 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_28, 0, x_4);
lean_ctor_set(x_28, 1, x_27);
x_2 = x_25;
x_3 = x_28;
goto _start;
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34;
lean_dec(x_5);
x_30 = lean_string_utf8_next(x_1, x_2);
lean_dec(x_2);
x_31 = lean_unsigned_to_nat(1u);
x_32 = lean_nat_add(x_4, x_31);
lean_dec(x_4);
x_33 = lean_unsigned_to_nat(0u);
x_34 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_34, 0, x_32);
lean_ctor_set(x_34, 1, x_33);
x_2 = x_30;
x_3 = x_34;
goto _start;
}
}
}
else
{
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
return x_3;
}
}
}
lean_object* l___private_init_data_string_basic_8__lineColumnAux___main___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l___private_init_data_string_basic_8__lineColumnAux___main(x_1, x_2, x_3);
lean_dec(x_1);
return x_4;
}
}
lean_object* l___private_init_data_string_basic_8__lineColumnAux(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l___private_init_data_string_basic_8__lineColumnAux___main(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l___private_init_data_string_basic_8__lineColumnAux___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l___private_init_data_string_basic_8__lineColumnAux(x_1, x_2, x_3);
lean_dec(x_1);
return x_4;
}
}
lean_object* _init_l_String_lineColumn___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1u);
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_String_lineColumn(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = lean_unsigned_to_nat(0u);
x_4 = l_String_lineColumn___closed__1;
x_5 = l___private_init_data_string_basic_8__lineColumnAux___main(x_1, x_3, x_4);
return x_5;
}
}
lean_object* l_String_lineColumn___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_String_lineColumn(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_String_offsetOfPosAux___main(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -4914,8 +4748,6 @@ l_String_HasAppend___closed__1 = _init_l_String_HasAppend___closed__1();
lean_mark_persistent(l_String_HasAppend___closed__1);
l_String_HasAppend = _init_l_String_HasAppend();
lean_mark_persistent(l_String_HasAppend);
l_String_lineColumn___closed__1 = _init_l_String_lineColumn___closed__1();
lean_mark_persistent(l_String_lineColumn___closed__1);
l_Substring_drop___closed__1 = _init_l_Substring_drop___closed__1();
lean_mark_persistent(l_Substring_drop___closed__1);
l_Substring_drop___closed__2 = _init_l_Substring_drop___closed__2();

30
src/stage0/init/lean/compiler/ir/emitc.c
View file

@ -280,6 +280,7 @@ lean_object* l_Lean_IR_EmitC_throwUnknownVar(lean_object*);
lean_object* l_Lean_IR_EmitC_emitMainFn___closed__13;
lean_object* l_Lean_IR_EmitC_emitSet___closed__1;
lean_object* l_Nat_mforAux___main___at_Lean_IR_EmitC_emitReset___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_String_Iterator_HasRepr___closed__2;
lean_object* l_Lean_IR_EmitC_emitLit(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_anyAux___main___at_Lean_IR_EmitC_overwriteParam___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
@ -302,7 +303,6 @@ lean_object* l_Lean_IR_EmitC_emitBoxFn___boxed(lean_object*, lean_object*, lean_
lean_object* l_Lean_IR_EmitC_toHexDigit(lean_object*);
lean_object* l_Lean_IR_EmitC_emitSProj___closed__3;
lean_object* l_Lean_IR_EmitC_emitLn(lean_object*);
extern lean_object* l_Lean_Format_flatten___main___closed__1;
lean_object* l_Lean_IR_EmitC_emitDeclInit___closed__4;
extern lean_object* l_Lean_IR_altInh;
lean_object* l_Lean_IR_EmitC_emitUnbox___closed__4;
@ -2012,7 +2012,7 @@ block_63:
uint8_t x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_9 = l_Lean_IR_Decl_resultType(x_1);
x_10 = l_Lean_IR_EmitC_toCType(x_9);
x_11 = l_Lean_Format_flatten___main___closed__1;
x_11 = l_String_Iterator_HasRepr___closed__2;
x_12 = lean_string_append(x_10, x_11);
x_13 = lean_string_append(x_12, x_2);
x_14 = lean_string_append(x_8, x_13);
@ -5512,7 +5512,7 @@ x_18 = lean_nat_add(x_2, x_17);
lean_dec(x_2);
x_19 = l_System_FilePath_dirName___closed__1;
x_20 = l_Lean_Name_toStringWithSep___main(x_19, x_16);
x_21 = l_Lean_Format_flatten___main___closed__1;
x_21 = l_String_Iterator_HasRepr___closed__2;
x_22 = lean_string_append(x_21, x_20);
lean_dec(x_20);
x_23 = lean_string_append(x_14, x_22);
@ -5535,7 +5535,7 @@ x_29 = lean_nat_add(x_2, x_28);
lean_dec(x_2);
x_30 = l_System_FilePath_dirName___closed__1;
x_31 = l_Lean_Name_toStringWithSep___main(x_30, x_27);
x_32 = l_Lean_Format_flatten___main___closed__1;
x_32 = l_String_Iterator_HasRepr___closed__2;
x_33 = lean_string_append(x_32, x_31);
lean_dec(x_31);
x_34 = lean_string_append(x_26, x_33);
@ -6475,7 +6475,7 @@ lean_dec(x_7);
x_8 = l_Lean_IR_EmitC_toCType(x_2);
x_9 = lean_string_append(x_6, x_8);
lean_dec(x_8);
x_10 = l_Lean_Format_flatten___main___closed__1;
x_10 = l_String_Iterator_HasRepr___closed__2;
x_11 = lean_string_append(x_9, x_10);
x_12 = l_Nat_repr(x_1);
x_13 = l_Lean_IR_VarId_HasToString___closed__1;
@ -6499,7 +6499,7 @@ lean_dec(x_4);
x_20 = l_Lean_IR_EmitC_toCType(x_2);
x_21 = lean_string_append(x_19, x_20);
lean_dec(x_20);
x_22 = l_Lean_Format_flatten___main___closed__1;
x_22 = l_String_Iterator_HasRepr___closed__2;
x_23 = lean_string_append(x_21, x_22);
x_24 = l_Nat_repr(x_1);
x_25 = l_Lean_IR_VarId_HasToString___closed__1;
@ -11824,7 +11824,7 @@ lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean
x_22 = lean_ctor_get(x_20, 1);
x_23 = lean_ctor_get(x_20, 0);
lean_dec(x_23);
x_24 = l_Lean_Format_flatten___main___closed__1;
x_24 = l_String_Iterator_HasRepr___closed__2;
x_25 = lean_string_append(x_22, x_24);
lean_ctor_set(x_20, 1, x_25);
lean_ctor_set(x_20, 0, x_19);
@ -12029,7 +12029,7 @@ lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103;
x_100 = lean_ctor_get(x_20, 1);
lean_inc(x_100);
lean_dec(x_20);
x_101 = l_Lean_Format_flatten___main___closed__1;
x_101 = l_String_Iterator_HasRepr___closed__2;
x_102 = lean_string_append(x_100, x_101);
x_103 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_103, 0, x_19);
@ -12215,7 +12215,7 @@ if (lean_is_exclusive(x_157)) {
lean_dec_ref(x_157);
x_159 = lean_box(0);
}
x_160 = l_Lean_Format_flatten___main___closed__1;
x_160 = l_String_Iterator_HasRepr___closed__2;
x_161 = lean_string_append(x_158, x_160);
if (lean_is_scalar(x_159)) {
x_162 = lean_alloc_ctor(0, 2, 0);
@ -12429,7 +12429,7 @@ x_17 = l_Lean_IR_EmitC_emitReset___closed__2;
x_18 = lean_string_append(x_16, x_17);
x_19 = l_IO_println___rarg___closed__1;
x_20 = lean_string_append(x_18, x_19);
x_21 = l_Lean_Format_flatten___main___closed__1;
x_21 = l_String_Iterator_HasRepr___closed__2;
x_22 = lean_string_append(x_20, x_21);
x_23 = lean_box(0);
lean_ctor_set(x_7, 1, x_22);
@ -12956,7 +12956,7 @@ x_199 = l_Lean_IR_EmitC_emitReset___closed__2;
x_200 = lean_string_append(x_198, x_199);
x_201 = l_IO_println___rarg___closed__1;
x_202 = lean_string_append(x_200, x_201);
x_203 = l_Lean_Format_flatten___main___closed__1;
x_203 = l_String_Iterator_HasRepr___closed__2;
x_204 = lean_string_append(x_202, x_203);
x_205 = lean_box(0);
x_206 = lean_alloc_ctor(0, 2, 0);
@ -21266,7 +21266,7 @@ x_15 = lean_ctor_get_uint8(x_14, sizeof(void*)*1 + 1);
x_16 = l_Lean_IR_EmitC_toCType(x_15);
x_17 = lean_string_append(x_12, x_16);
lean_dec(x_16);
x_18 = l_Lean_Format_flatten___main___closed__1;
x_18 = l_String_Iterator_HasRepr___closed__2;
x_19 = lean_string_append(x_17, x_18);
x_20 = lean_ctor_get(x_14, 0);
lean_inc(x_20);
@ -21426,7 +21426,7 @@ if (lean_is_exclusive(x_22)) {
x_26 = l_Lean_IR_EmitC_toCType(x_16);
x_27 = lean_string_append(x_24, x_26);
lean_dec(x_26);
x_28 = l_Lean_Format_flatten___main___closed__1;
x_28 = l_String_Iterator_HasRepr___closed__2;
x_29 = lean_string_append(x_27, x_28);
x_30 = lean_array_get_size(x_15);
x_128 = lean_unsigned_to_nat(0u);
@ -21966,7 +21966,7 @@ if (lean_is_exclusive(x_165)) {
x_169 = l_Lean_IR_EmitC_toCType(x_16);
x_170 = lean_string_append(x_167, x_169);
lean_dec(x_169);
x_171 = l_Lean_Format_flatten___main___closed__1;
x_171 = l_String_Iterator_HasRepr___closed__2;
x_172 = lean_string_append(x_170, x_171);
x_173 = lean_array_get_size(x_15);
x_239 = lean_unsigned_to_nat(0u);
@ -22527,7 +22527,7 @@ if (lean_is_exclusive(x_295)) {
x_299 = l_Lean_IR_EmitC_toCType(x_287);
x_300 = lean_string_append(x_297, x_299);
lean_dec(x_299);
x_301 = l_Lean_Format_flatten___main___closed__1;
x_301 = l_String_Iterator_HasRepr___closed__2;
x_302 = lean_string_append(x_300, x_301);
x_303 = lean_array_get_size(x_286);
x_369 = lean_unsigned_to_nat(0u);

24
src/stage0/init/lean/compiler/ir/format.c
View file

@ -135,6 +135,7 @@ lean_object* l_Lean_IR_formatFnBody___main___closed__2;
lean_object* l___private_init_lean_compiler_ir_format_3__formatLitVal(lean_object*);
lean_object* l___private_init_lean_compiler_ir_format_4__formatCtorInfo___closed__3;
lean_object* l___private_init_lean_compiler_ir_format_2__formatArray___rarg___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Format_flatten___main___closed__1;
lean_object* l_Array_miterateAux___main___at___private_init_lean_compiler_ir_format_5__formatExpr___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_formatFnBodyHead___closed__34;
lean_object* l_Lean_IR_declHasFormat___closed__1;
@ -166,7 +167,6 @@ lean_object* l___private_init_lean_compiler_ir_format_5__formatExpr___closed__24
lean_object* l_Lean_IR_formatFnBodyHead___closed__14;
extern lean_object* l_Lean_formatEntry___closed__2;
lean_object* l_Array_size(lean_object*, lean_object*);
extern lean_object* l_Lean_Format_flatten___main___closed__2;
lean_object* l___private_init_lean_compiler_ir_format_5__formatExpr___closed__19;
lean_object* l_Lean_IR_exprHasFormat;
lean_object* l_Lean_IR_formatParams(lean_object*);
@ -276,7 +276,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;
x_8 = lean_array_fget(x_3, x_4);
x_9 = 0;
x_10 = l_Lean_Format_flatten___main___closed__2;
x_10 = l_Lean_Format_flatten___main___closed__1;
x_11 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_11, 0, x_5);
lean_ctor_set(x_11, 1, x_10);
@ -621,7 +621,7 @@ else
lean_object* x_7; uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_7 = lean_array_fget(x_2, x_3);
x_8 = 0;
x_9 = l_Lean_Format_flatten___main___closed__2;
x_9 = l_Lean_Format_flatten___main___closed__1;
x_10 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_10, 0, x_4);
lean_ctor_set(x_10, 1, x_9);
@ -742,7 +742,7 @@ _start:
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = 0;
x_2 = l___private_init_lean_compiler_ir_format_5__formatExpr___closed__9;
x_3 = l_Lean_Format_flatten___main___closed__2;
x_3 = l_Lean_Format_flatten___main___closed__1;
x_4 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
@ -788,7 +788,7 @@ _start:
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = 0;
x_2 = l___private_init_lean_compiler_ir_format_5__formatExpr___closed__13;
x_3 = l_Lean_Format_flatten___main___closed__2;
x_3 = l_Lean_Format_flatten___main___closed__1;
x_4 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
@ -1888,7 +1888,7 @@ else
lean_object* x_7; uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_7 = lean_array_fget(x_2, x_3);
x_8 = 0;
x_9 = l_Lean_Format_flatten___main___closed__2;
x_9 = l_Lean_Format_flatten___main___closed__1;
x_10 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_10, 0, x_4);
lean_ctor_set(x_10, 1, x_9);
@ -2137,7 +2137,7 @@ _start:
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = 0;
x_2 = l_Lean_IR_formatFnBodyHead___closed__19;
x_3 = l_Lean_Format_flatten___main___closed__2;
x_3 = l_Lean_Format_flatten___main___closed__1;
x_4 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
@ -2183,7 +2183,7 @@ _start:
uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = 0;
x_2 = l_Lean_IR_formatFnBodyHead___closed__23;
x_3 = l_Lean_Format_flatten___main___closed__2;
x_3 = l_Lean_Format_flatten___main___closed__1;
x_4 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
@ -2642,7 +2642,7 @@ x_138 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_138, 0, x_137);
lean_ctor_set(x_138, 1, x_136);
lean_ctor_set_uint8(x_138, sizeof(void*)*2, x_129);
x_139 = l_Lean_Format_flatten___main___closed__2;
x_139 = l_Lean_Format_flatten___main___closed__1;
x_140 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_140, 0, x_138);
lean_ctor_set(x_140, 1, x_139);
@ -2709,7 +2709,7 @@ x_164 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_164, 0, x_163);
lean_ctor_set(x_164, 1, x_162);
lean_ctor_set_uint8(x_164, sizeof(void*)*2, x_155);
x_165 = l_Lean_Format_flatten___main___closed__2;
x_165 = l_Lean_Format_flatten___main___closed__1;
x_166 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_166, 0, x_164);
lean_ctor_set(x_166, 1, x_165);
@ -3388,7 +3388,7 @@ x_188 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_188, 0, x_187);
lean_ctor_set(x_188, 1, x_186);
lean_ctor_set_uint8(x_188, sizeof(void*)*2, x_179);
x_189 = l_Lean_Format_flatten___main___closed__2;
x_189 = l_Lean_Format_flatten___main___closed__1;
x_190 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_190, 0, x_188);
lean_ctor_set(x_190, 1, x_189);
@ -3486,7 +3486,7 @@ x_226 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_226, 0, x_225);
lean_ctor_set(x_226, 1, x_224);
lean_ctor_set_uint8(x_226, sizeof(void*)*2, x_217);
x_227 = l_Lean_Format_flatten___main___closed__2;
x_227 = l_Lean_Format_flatten___main___closed__1;
x_228 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_228, 0, x_226);
lean_ctor_set(x_228, 1, x_227);

3485
src/stage0/init/lean/elaborator/basic.c
View file

File diff suppressed because it is too large Load diff

2535
src/stage0/init/lean/elaborator/command.c
View file

File diff suppressed because it is too large Load diff

2793
src/stage0/init/lean/elaborator/preterm.c
View file

File diff suppressed because it is too large Load diff

1119
src/stage0/init/lean/elaborator/term.c
View file

File diff suppressed because it is too large Load diff

40
src/stage0/init/lean/expr.c
View file

@ -34,6 +34,7 @@ lean_object* l_Lean_mkApp(lean_object*, lean_object*);
lean_object* l_Lean_Expr_eqv___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkDecIsTrue___closed__4;
lean_object* lean_expr_mk_pi(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* lean_expr_instantiate(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppNumArgsAux___boxed(lean_object*, lean_object*);
lean_object* lean_expr_local(lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* lean_expr_mk_app(lean_object*, lean_object*);
@ -56,6 +57,8 @@ lean_object* l_Lean_Expr_Hashable___closed__1;
uint8_t lean_expr_eqv(lean_object*, lean_object*);
lean_object* l_Lean_MData_HasEmptyc;
lean_object* l_Lean_Expr_dbgToString___boxed(lean_object*);
lean_object* l_Lean_Expr_instantiateRev___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_instantiate___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_elet___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppNumArgs(lean_object*);
lean_object* l_Lean_mkDecIsTrue___closed__1;
@ -68,16 +71,20 @@ uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Expr_app___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkDecIsTrue___closed__2;
lean_object* l_Lean_Expr_getAppFn___main___boxed(lean_object*);
lean_object* lean_expr_instantiate_rev(lean_object*, lean_object*);
lean_object* l_Lean_mkCApp(lean_object*, lean_object*);
lean_object* l_Lean_mkDecIsTrue___closed__5;
uint8_t l_Lean_Expr_isAppOfArity___main(lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_mk_mvar(lean_object*);
lean_object* lean_expr_mk_bvar(lean_object*);
lean_object* lean_expr_abstract_range(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_proj___boxed(lean_object*, lean_object*, lean_object*);
uint8_t lean_expr_lt(lean_object*, lean_object*);
lean_object* l_Lean_mkDecIsTrue(lean_object*, lean_object*);
lean_object* l_Lean_Expr_abstract___boxed(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isAppOf(lean_object*, lean_object*);
lean_object* l_Lean_Expr_const___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_abstractRange___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_fvar___boxed(lean_object*);
lean_object* lean_expr_mk_lambda(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Expr_mdata___boxed(lean_object*, lean_object*);
@ -85,6 +92,7 @@ lean_object* l_Lean_Expr_HasBeq;
lean_object* l_Lean_Expr_Hashable;
lean_object* l_Lean_Expr_getAppNumArgs___boxed(lean_object*);
lean_object* l_Lean_Expr_mvar___boxed(lean_object*);
lean_object* lean_expr_abstract(lean_object*, lean_object*);
lean_object* l_Lean_Expr_local___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn___boxed(lean_object*);
uint8_t l_Lean_Expr_isAppOfArity(lean_object*, lean_object*, lean_object*);
@ -592,6 +600,38 @@ x_5 = lean_box(x_4);
return x_5;
}
}
lean_object* l_Lean_Expr_instantiate___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_expr_instantiate(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Expr_instantiateRev___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_expr_instantiate_rev(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Expr_abstract___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_expr_abstract(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Expr_abstractRange___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_expr_abstract_range(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_mkConst(lean_object* x_1, lean_object* x_2) {
_start:
{

16
src/stage0/init/lean/format.c
View file

@ -117,6 +117,7 @@ lean_object* l_Lean_Format_paren___closed__3;
lean_object* l_Lean_Format_repr___main___closed__10;
lean_object* l_Lean_Format_Inhabited;
lean_object* l_Lean_Format_getWidth___closed__4;
extern lean_object* l_String_Iterator_HasRepr___closed__2;
extern lean_object* l_Prod_HasRepr___rarg___closed__1;
lean_object* l_Lean_Format_repr___main___closed__12;
lean_object* l_Lean_Format_indentOption(lean_object*);
@ -167,7 +168,6 @@ lean_object* l_Lean_Format_defWidth;
lean_object* l_Lean_Format_unicodeOption(lean_object*);
lean_object* l_Lean_formatEntry___closed__2;
lean_object* l_Array_size(lean_object*, lean_object*);
lean_object* l_Lean_Format_flatten___main___closed__2;
lean_object* l_Lean_Format_repr___main___closed__9;
lean_object* l_Lean_Format_widthOption___closed__2;
lean_object* l_Lean_Format_prefixJoin(lean_object*);
@ -347,16 +347,8 @@ return x_3;
lean_object* _init_l_Lean_Format_flatten___main___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string(" ");
return x_1;
}
}
lean_object* _init_l_Lean_Format_flatten___main___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Format_flatten___main___closed__1;
x_1 = l_String_Iterator_HasRepr___closed__2;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -369,7 +361,7 @@ switch (lean_obj_tag(x_1)) {
case 1:
{
lean_object* x_2;
x_2 = l_Lean_Format_flatten___main___closed__2;
x_2 = l_Lean_Format_flatten___main___closed__1;
return x_2;
}
case 3:
@ -3318,8 +3310,6 @@ l_Lean_Format_join___closed__1 = _init_l_Lean_Format_join___closed__1();
lean_mark_persistent(l_Lean_Format_join___closed__1);
l_Lean_Format_flatten___main___closed__1 = _init_l_Lean_Format_flatten___main___closed__1();
lean_mark_persistent(l_Lean_Format_flatten___main___closed__1);
l_Lean_Format_flatten___main___closed__2 = _init_l_Lean_Format_flatten___main___closed__2();
lean_mark_persistent(l_Lean_Format_flatten___main___closed__2);
l_Lean_Format_spaceUptoLine___main___closed__1 = _init_l_Lean_Format_spaceUptoLine___main___closed__1();
lean_mark_persistent(l_Lean_Format_spaceUptoLine___main___closed__1);
l_Lean_Format_spaceUptoLine___main___closed__2 = _init_l_Lean_Format_spaceUptoLine___main___closed__2();

307
src/stage0/init/lean/localcontext.c
View file

@ -58,6 +58,7 @@ lean_object* lean_local_ctx_mk_let_decl(lean_object*, lean_object*, lean_object*
lean_object* l_Lean_LocalDecl_binderInfo___boxed(lean_object*);
lean_object* l_Array_miterateAux___main___at_Lean_LocalContext_foldlFrom___spec__7___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Lean_LocalContext_mfoldlFrom___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_exprIsInhabited;
lean_object* l_PersistentArray_getAux___main___at___private_init_lean_localcontext_1__popTailNoneAux___main___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentArray_mfindAux___main___at_Lean_LocalContext_mfindDecl___spec__2(lean_object*);
lean_object* l_PersistentArray_mfindRev___at_Lean_LocalContext_findFromUserName___spec__1___boxed(lean_object*, lean_object*);
@ -72,6 +73,7 @@ lean_object* l_Array_mfindAux___main___at_Lean_LocalContext_mfindDecl___spec__4_
lean_object* l_Array_mfindAux___main___at_Lean_LocalContext_findDecl___spec__4(lean_object*);
lean_object* l_Lean_LocalDecl_name___boxed(lean_object*);
lean_object* l_Lean_LocalContext_mfor___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_mk_pi(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Array_mfindRevAux___main___at_Lean_LocalContext_mfindDeclRev___spec__5(lean_object*);
lean_object* l_Array_mfindRevAux___main___at_Lean_LocalContext_mfindDeclRev___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_Inhabited___closed__1;
@ -82,6 +84,7 @@ lean_object* l_Lean_LocalDecl_valueOpt___boxed(lean_object*);
lean_object* l_Array_mfindAux___main___at_Lean_LocalContext_mfindDecl___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mfindRevAux___main___at_Lean_LocalContext_mfindDeclRev___spec__2___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mforAux___main___at_Lean_LocalContext_mfor___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_mk_let(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mforAux___main___at_Lean_LocalContext_mfor___spec__3(lean_object*);
size_t l_USize_sub(size_t, size_t);
lean_object* l_Array_miterateAux___main___at_Lean_LocalContext_mfoldl___spec__4(lean_object*);
@ -98,6 +101,7 @@ lean_object* l_Lean_LocalContext_findDeclRev(lean_object*);
lean_object* l_PersistentArray_mfindRev___at_Lean_LocalContext_findDeclRev___spec__2___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Lean_LocalContext_mfoldlFrom___spec__3___boxed(lean_object*);
lean_object* l_Array_mfindAux___main___at_Lean_LocalContext_findDecl___spec__5___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_mkBinding(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_mfor___boxed(lean_object*);
lean_object* l_PersistentArray_mfindAux___main___at_Lean_LocalContext_findDecl___spec__3___rarg(lean_object*, lean_object*);
lean_object* l_Array_mfindRevAux___main___at_Lean_LocalContext_mfindDeclRev___spec__5___boxed(lean_object*);
@ -119,6 +123,7 @@ lean_object* l___private_init_lean_localcontext_1__popTailNoneAux___main(lean_ob
lean_object* l_PersistentArray_mfind___at_Lean_LocalContext_mfindDecl___spec__1___boxed(lean_object*);
lean_object* l_Lean_LocalContext_mkLocalDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentArray_mfor___at_Lean_LocalContext_mfor___spec__1___boxed(lean_object*);
lean_object* l_Lean_LocalContext_mkLambda(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mfindRevAux___main___at_Lean_LocalContext_findFromUserName___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Lean_LocalContext_mfoldlFrom___spec__3(lean_object*);
lean_object* l_PersistentArray_pop___rarg(lean_object*);
@ -179,6 +184,7 @@ uint8_t l_Lean_LocalDecl_binderInfo(lean_object*);
lean_object* l_Array_mforAux___main___at_Lean_LocalContext_mfor___spec__4(lean_object*);
lean_object* l_PersistentArray_mfoldlFrom___at_Lean_LocalContext_mfoldlFrom___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_mkBinding___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mfindRevAux___main___at_Lean_LocalContext_mfindDeclRev___spec__2(lean_object*);
lean_object* l_PersistentHashMap_findAux___main___at_Lean_LocalContext_find___spec__2(lean_object*, size_t, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
@ -228,7 +234,9 @@ lean_object* l_Lean_LocalContext_mfoldl___at_Lean_LocalContext_foldl___spec__1__
lean_object* l_Array_miterateAux___main___at_Lean_LocalContext_mfoldlFrom___spec__2___boxed(lean_object*);
lean_object* l_PersistentArray_mfor___at_Lean_LocalContext_mfor___spec__1(lean_object*);
lean_object* l_PersistentArray_mfoldlFrom___at_Lean_LocalContext_mfoldlFrom___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkBinding___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mforAux___main___at_Lean_LocalContext_mfor___spec__4___boxed(lean_object*);
lean_object* lean_expr_abstract_range(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_mfoldl___boxed(lean_object*);
lean_object* l_Array_mfindAux___main___at_Lean_LocalContext_mfindDecl___spec__4___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mforAux___main___at_Lean_LocalContext_mfor___spec__5___boxed(lean_object*);
@ -275,6 +283,7 @@ lean_object* l_Array_mfindAux___main___at_Lean_LocalContext_mfindDecl___spec__3_
lean_object* l_Array_miterateAux___main___at_Lean_LocalContext_mfoldl___spec__4___boxed(lean_object*);
lean_object* l_Lean_LocalContext_isSubPrefixOfAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentArray_mfindRev___at_Lean_LocalContext_mfindDeclRev___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkForall___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_local_ctx_erase(lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_foldl___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Lean_LocalContext_foldl___spec__6___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -291,6 +300,7 @@ lean_object* l_Array_mforAux___main___at_Lean_LocalContext_mfor___spec__3___boxe
lean_object* l_Array_mfindAux___main___at_Lean_LocalContext_mfindDecl___spec__3___boxed(lean_object*);
lean_object* l_PersistentArray_mfindRev___at_Lean_LocalContext_mfindDeclRev___spec__1___boxed(lean_object*);
lean_object* l_Lean_LocalContext_isEmpty___boxed(lean_object*);
lean_object* lean_expr_mk_lambda(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_mfoldlFrom___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalDecl_index(lean_object*);
lean_object* l_Array_miterateAux___main___at_Lean_LocalContext_foldl___spec__5(lean_object*);
@ -311,6 +321,7 @@ lean_object* l_Array_set(lean_object*, lean_object*, lean_object*, lean_object*)
lean_object* l_Array_mforAux___main___at_Lean_LocalContext_mfor___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mfindRevAux___main___at_Lean_LocalContext_findDeclRev___spec__5(lean_object*);
lean_object* l_Lean_LocalDecl_userName___boxed(lean_object*);
lean_object* lean_expr_abstract(lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_getUnusedNameAux(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Lean_LocalContext_foldl___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_miterateAux___main___at_Lean_LocalContext_foldlFrom___spec__6___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -323,6 +334,7 @@ lean_object* l_Array_miterateAux___main___at_Lean_LocalContext_mfoldl___spec__5_
lean_object* l_PersistentArray_mfindRevAux___main___at_Lean_LocalContext_mfindDeclRev___spec__3(lean_object*);
lean_object* lean_usize_to_nat(size_t);
lean_object* l_PersistentHashMap_findAux___main___at_Lean_LocalContext_find___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkBinding___spec__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentArray_mfoldlAux___main___at_Lean_LocalContext_foldlFrom___spec__4___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentHashMap_insertAux___main___at_Lean_LocalContext_mkLocalDecl___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*);
lean_object* l_Array_mfindAux___main___at_Lean_LocalContext_findDecl___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*);
@ -333,6 +345,8 @@ lean_object* l_Array_mfindRevAux___main___at_Lean_LocalContext_findFromUserName_
lean_object* l_Array_miterateAux___main___at_Lean_LocalContext_foldlFrom___spec__8(lean_object*);
lean_object* l_Lean_LocalContext_mfindDeclRev(lean_object*);
lean_object* l_Array_mfindAux___main___at_Lean_LocalContext_mfindDecl___spec__5(lean_object*);
lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkLambda___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_mkForall(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_exprIsInhabited___closed__1;
lean_object* l_PersistentHashMap_find___at_Lean_LocalContext_find___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_PersistentArray_mfindRevAux___main___at_Lean_LocalContext_findFromUserName___spec__3(lean_object*, lean_object*);
@ -6565,6 +6579,299 @@ x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkBinding___spec__1(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; uint8_t x_7;
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_nat_dec_eq(x_4, x_6);
if (x_7 == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_8 = lean_unsigned_to_nat(1u);
x_9 = lean_nat_sub(x_4, x_8);
lean_dec(x_4);
x_10 = l_Lean_exprIsInhabited;
x_11 = lean_array_get(x_10, x_3, x_9);
lean_inc(x_2);
x_12 = l_Lean_LocalContext_findFVar(x_2, x_11);
if (lean_obj_tag(x_12) == 0)
{
x_4 = x_9;
goto _start;
}
else
{
lean_object* x_14;
x_14 = lean_ctor_get(x_12, 0);
lean_inc(x_14);
lean_dec(x_12);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_15; lean_object* x_16; uint8_t x_17; lean_object* x_18;
x_15 = lean_ctor_get(x_14, 2);
lean_inc(x_15);
x_16 = lean_ctor_get(x_14, 3);
lean_inc(x_16);
x_17 = lean_ctor_get_uint8(x_14, sizeof(void*)*4);
lean_dec(x_14);
lean_inc(x_3);
lean_inc(x_9);
x_18 = lean_expr_abstract_range(x_16, x_9, x_3);
if (x_1 == 0)
{
lean_object* x_19;
x_19 = lean_expr_mk_pi(x_15, x_17, x_18, x_5);
x_4 = x_9;
x_5 = x_19;
goto _start;
}
else
{
lean_object* x_21;
x_21 = lean_expr_mk_lambda(x_15, x_17, x_18, x_5);
x_4 = x_9;
x_5 = x_21;
goto _start;
}
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_23 = lean_ctor_get(x_14, 2);
lean_inc(x_23);
x_24 = lean_ctor_get(x_14, 3);
lean_inc(x_24);
x_25 = lean_ctor_get(x_14, 4);
lean_inc(x_25);
lean_dec(x_14);
lean_inc(x_3);
lean_inc(x_9);
x_26 = lean_expr_abstract_range(x_24, x_9, x_3);
lean_inc(x_3);
lean_inc(x_9);
x_27 = lean_expr_abstract_range(x_25, x_9, x_3);
x_28 = lean_expr_mk_let(x_23, x_26, x_27, x_5);
x_4 = x_9;
x_5 = x_28;
goto _start;
}
}
}
else
{
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_5;
}
}
}
lean_object* l_Lean_LocalContext_mkBinding(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
lean_inc(x_3);
x_5 = lean_expr_abstract(x_4, x_3);
x_6 = lean_array_get_size(x_3);
x_7 = l_Nat_foldRevAux___main___at_Lean_LocalContext_mkBinding___spec__1(x_1, x_2, x_3, x_6, x_5);
return x_7;
}
}
lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkBinding___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
uint8_t x_6; lean_object* x_7;
x_6 = lean_unbox(x_1);
lean_dec(x_1);
x_7 = l_Nat_foldRevAux___main___at_Lean_LocalContext_mkBinding___spec__1(x_6, x_2, x_3, x_4, x_5);
return x_7;
}
}
lean_object* l_Lean_LocalContext_mkBinding___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5; lean_object* x_6;
x_5 = lean_unbox(x_1);
lean_dec(x_1);
x_6 = l_Lean_LocalContext_mkBinding(x_5, x_2, x_3, x_4);
return x_6;
}
}
lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkLambda___spec__1(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_3, x_5);
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_7 = lean_unsigned_to_nat(1u);
x_8 = lean_nat_sub(x_3, x_7);
lean_dec(x_3);
x_9 = l_Lean_exprIsInhabited;
x_10 = lean_array_get(x_9, x_2, x_8);
lean_inc(x_1);
x_11 = l_Lean_LocalContext_findFVar(x_1, x_10);
if (lean_obj_tag(x_11) == 0)
{
x_3 = x_8;
goto _start;
}
else
{
lean_object* x_13;
x_13 = lean_ctor_get(x_11, 0);
lean_inc(x_13);
lean_dec(x_11);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18;
x_14 = lean_ctor_get(x_13, 2);
lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 3);
lean_inc(x_15);
x_16 = lean_ctor_get_uint8(x_13, sizeof(void*)*4);
lean_dec(x_13);
lean_inc(x_2);
lean_inc(x_8);
x_17 = lean_expr_abstract_range(x_15, x_8, x_2);
x_18 = lean_expr_mk_lambda(x_14, x_16, x_17, x_4);
x_3 = x_8;
x_4 = x_18;
goto _start;
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_20 = lean_ctor_get(x_13, 2);
lean_inc(x_20);
x_21 = lean_ctor_get(x_13, 3);
lean_inc(x_21);
x_22 = lean_ctor_get(x_13, 4);
lean_inc(x_22);
lean_dec(x_13);
lean_inc(x_2);
lean_inc(x_8);
x_23 = lean_expr_abstract_range(x_21, x_8, x_2);
lean_inc(x_2);
lean_inc(x_8);
x_24 = lean_expr_abstract_range(x_22, x_8, x_2);
x_25 = lean_expr_mk_let(x_20, x_23, x_24, x_4);
x_3 = x_8;
x_4 = x_25;
goto _start;
}
}
}
else
{
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_4;
}
}
}
lean_object* l_Lean_LocalContext_mkLambda(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_inc(x_2);
x_4 = lean_expr_abstract(x_3, x_2);
x_5 = lean_array_get_size(x_2);
x_6 = l_Nat_foldRevAux___main___at_Lean_LocalContext_mkLambda___spec__1(x_1, x_2, x_5, x_4);
return x_6;
}
}
lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkForall___spec__1(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_3, x_5);
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_7 = lean_unsigned_to_nat(1u);
x_8 = lean_nat_sub(x_3, x_7);
lean_dec(x_3);
x_9 = l_Lean_exprIsInhabited;
x_10 = lean_array_get(x_9, x_2, x_8);
lean_inc(x_1);
x_11 = l_Lean_LocalContext_findFVar(x_1, x_10);
if (lean_obj_tag(x_11) == 0)
{
x_3 = x_8;
goto _start;
}
else
{
lean_object* x_13;
x_13 = lean_ctor_get(x_11, 0);
lean_inc(x_13);
lean_dec(x_11);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18;
x_14 = lean_ctor_get(x_13, 2);
lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 3);
lean_inc(x_15);
x_16 = lean_ctor_get_uint8(x_13, sizeof(void*)*4);
lean_dec(x_13);
lean_inc(x_2);
lean_inc(x_8);
x_17 = lean_expr_abstract_range(x_15, x_8, x_2);
x_18 = lean_expr_mk_pi(x_14, x_16, x_17, x_4);
x_3 = x_8;
x_4 = x_18;
goto _start;
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_20 = lean_ctor_get(x_13, 2);
lean_inc(x_20);
x_21 = lean_ctor_get(x_13, 3);
lean_inc(x_21);
x_22 = lean_ctor_get(x_13, 4);
lean_inc(x_22);
lean_dec(x_13);
lean_inc(x_2);
lean_inc(x_8);
x_23 = lean_expr_abstract_range(x_21, x_8, x_2);
lean_inc(x_2);
lean_inc(x_8);
x_24 = lean_expr_abstract_range(x_22, x_8, x_2);
x_25 = lean_expr_mk_let(x_20, x_23, x_24, x_4);
x_3 = x_8;
x_4 = x_25;
goto _start;
}
}
}
else
{
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_4;
}
}
}
lean_object* l_Lean_LocalContext_mkForall(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_inc(x_2);
x_4 = lean_expr_abstract(x_3, x_2);
x_5 = lean_array_get_size(x_2);
x_6 = l_Nat_foldRevAux___main___at_Lean_LocalContext_mkForall___spec__1(x_1, x_2, x_5, x_4);
return x_6;
}
}
lean_object* initialize_init_data_persistentarray_basic(lean_object*);
lean_object* initialize_init_data_persistenthashmap_basic(lean_object*);
lean_object* initialize_init_lean_expr(lean_object*);

4
src/stage0/init/lean/message.c
View file

@ -33,8 +33,8 @@ uint8_t l_Lean_MessageLog_isEmpty(lean_object*);
lean_object* l_Lean_Message_toString___closed__4;
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_List_append___rarg(lean_object*, lean_object*);
extern lean_object* l_String_Iterator_HasRepr___closed__2;
uint8_t l_List_isEmpty___rarg(lean_object*);
extern lean_object* l_Lean_Format_flatten___main___closed__1;
lean_object* l_Lean_Message_HasToString___closed__1;
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_mkErrorStringWithPos___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -70,7 +70,7 @@ x_9 = lean_string_append(x_8, x_5);
x_10 = l_Nat_repr(x_3);
x_11 = lean_string_append(x_9, x_10);
lean_dec(x_10);
x_12 = l_Lean_Format_flatten___main___closed__1;
x_12 = l_String_Iterator_HasRepr___closed__2;
x_13 = lean_string_append(x_11, x_12);
x_14 = lean_string_append(x_13, x_4);
return x_14;

70
src/stage0/init/lean/parser/term.c
View file

@ -66,6 +66,7 @@ lean_object* l_Lean_Parser_Term_optType___closed__3;
lean_object* l_Lean_Parser_Term_match___closed__1;
lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__10;
lean_object* l_Lean_Parser_Term_structInstSource___elambda__1___rarg___closed__2;
lean_object* l_List_foldl___main___at_Lean_Parser_mkAppStx___spec__1___rarg___closed__1;
lean_object* l_Lean_Parser_Term_parser_x21___closed__4;
lean_object* l___regBuiltinParser_Lean_Parser_Term_borrowed(lean_object*);
lean_object* l_Lean_Parser_Term_doPat___elambda__1___rarg___closed__1;
@ -206,6 +207,7 @@ lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_list___closed__4;
lean_object* l_Lean_Parser_Term_mod___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_list___elambda__1___closed__10;
lean_object* l_List_foldl___main___at_Lean_Parser_mkAppStx___spec__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_anonymousCtor___closed__4;
lean_object* l_Lean_Parser_Term_quotedName___elambda__1___rarg___closed__1;
lean_object* l_Lean_Parser_Term_show___closed__4;
@ -545,6 +547,7 @@ lean_object* l_Lean_Parser_Term_do___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_type___elambda__1___rarg___closed__1;
lean_object* l_Lean_Parser_Term_match___elambda__1___closed__6;
extern lean_object* l_Lean_Parser_Level_paren___closed__4;
lean_object* l_Array_mkEmpty(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_add___closed__1;
lean_object* l_Lean_Parser_Term_arrow___closed__2;
lean_object* l_Lean_Parser_Term_letIdLhs___closed__3;
@ -569,6 +572,7 @@ lean_object* l_Lean_Parser_Term_type___closed__2;
lean_object* l_Lean_Parser_Term_doPat___closed__3;
lean_object* l_Lean_Parser_Term_modN___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letEqns___elambda__1___spec__1___closed__1;
lean_object* l_Lean_Parser_mkAppStx(lean_object*);
lean_object* l_Lean_Parser_Term_le___closed__3;
lean_object* l_Lean_Parser_Term_if___elambda__1___rarg___closed__2;
lean_object* l_Lean_Parser_Term_mul___elambda__1___closed__3;
@ -738,6 +742,7 @@ lean_object* l_Lean_Parser_Term_let___closed__5;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___rarg___closed__2;
lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_sub___elambda__1___closed__2;
lean_object* l_List_foldl___main___at_Lean_Parser_mkAppStx___spec__1(lean_object*);
lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Term_array(lean_object*);
@ -926,6 +931,7 @@ lean_object* l_Lean_Parser_Term_bracketedDoSeq___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_structInst___elambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_cons___closed__3;
lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___rarg___closed__5;
lean_object* l_Array_push(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_seqRight___closed__1;
lean_object* l_Lean_Parser_Term_prop___elambda__1___rarg___closed__7;
lean_object* l_Lean_Parser_Term_heq___elambda__1___closed__2;
@ -1314,6 +1320,7 @@ lean_object* l_Lean_Parser_Term_inaccessible;
lean_object* l_Lean_Parser_Term_if___elambda__1___rarg___closed__10;
lean_object* l_Lean_Parser_Term_unicodeInfixR___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___rarg___closed__7;
lean_object* l_Lean_Parser_mkAppStx___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_let___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___rarg___closed__5;
lean_object* l_Lean_Parser_Term_namedPattern___elambda__1___rarg___closed__8;
@ -28412,6 +28419,67 @@ x_5 = l_Lean_Parser_addBuiltinTrailingParser(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l_List_foldl___main___at_Lean_Parser_mkAppStx___spec__1___rarg___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(2u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
lean_object* l_List_foldl___main___at_Lean_Parser_mkAppStx___spec__1___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
return x_1;
}
else
{
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_2, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_2);
x_5 = l_List_foldl___main___at_Lean_Parser_mkAppStx___spec__1___rarg___closed__1;
x_6 = lean_array_push(x_5, x_1);
x_7 = lean_array_push(x_6, x_3);
x_8 = l_Lean_Parser_Term_app___elambda__1___closed__2;
x_9 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_9, 0, x_8);
lean_ctor_set(x_9, 1, x_7);
x_1 = x_9;
x_2 = x_4;
goto _start;
}
}
}
lean_object* l_List_foldl___main___at_Lean_Parser_mkAppStx___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_List_foldl___main___at_Lean_Parser_mkAppStx___spec__1___rarg), 2, 0);
return x_2;
}
}
lean_object* l_Lean_Parser_mkAppStx___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_List_foldl___main___at_Lean_Parser_mkAppStx___spec__1___rarg(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Parser_mkAppStx(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_mkAppStx___rarg), 2, 0);
return x_2;
}
}
lean_object* initialize_init_lean_parser_parser(lean_object*);
lean_object* initialize_init_lean_parser_level(lean_object*);
static bool _G_initialized = false;
@ -31053,6 +31121,8 @@ l_Lean_Parser_Term_mapConstRev = _init_l_Lean_Parser_Term_mapConstRev();
lean_mark_persistent(l_Lean_Parser_Term_mapConstRev);
w = l___regBuiltinParser_Lean_Parser_Term_mapConstRev(w);
if (lean_io_result_is_error(w)) return w;
l_List_foldl___main___at_Lean_Parser_mkAppStx___spec__1___rarg___closed__1 = _init_l_List_foldl___main___at_Lean_Parser_mkAppStx___spec__1___rarg___closed__1();
lean_mark_persistent(l_List_foldl___main___at_Lean_Parser_mkAppStx___spec__1___rarg___closed__1);
return w;
}
#ifdef __cplusplus

184
src/stage0/init/lean/syntax.c
View file

@ -23,6 +23,7 @@ lean_object* l_Array_ummapAux___main___at_Lean_Syntax_mrewriteBottomUp___main___
lean_object* l_Lean_Syntax_toNat___rarg___boxed(lean_object*);
lean_object* l_Array_miterateAux___main___at_Lean_Syntax_reprint___main___spec__1(lean_object*);
uint8_t lean_name_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_mkAtomFrom___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getHeadInfo___main___rarg___boxed(lean_object*);
lean_object* l_Lean_Syntax_getNumArgs(lean_object*);
lean_object* l_Lean_Syntax_setTailInfo___rarg(lean_object*, lean_object*);
@ -32,6 +33,7 @@ lean_object* l_Lean_Syntax_isNatLit(lean_object*);
extern lean_object* l_Array_empty___closed__1;
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_ifNode(lean_object*, lean_object*);
lean_object* l_Lean_mkAtomFrom(lean_object*);
lean_object* l_Lean_nullKind___closed__2;
lean_object* l_Lean_stxInh(lean_object*);
lean_object* l_Lean_Syntax_setArg(lean_object*);
@ -55,6 +57,7 @@ lean_object* l_Function_comp___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_reprint___main(lean_object*);
lean_object* l_Lean_nullKind___closed__1;
lean_object* l_Array_miterateAux___main___at_Lean_Syntax_reprint___main___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkIdentFrom___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isNatLitAux___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_formatStx___main(lean_object*);
lean_object* l_Lean_numLitKind;
@ -62,6 +65,7 @@ lean_object* l_Lean_Syntax_asNode___rarg(lean_object*);
uint8_t l_Lean_Syntax_isIdent___rarg(lean_object*);
lean_object* l_Array_miterateAux___main___at_Lean_Syntax_reprint___main___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Format_joinSep___main___at_Lean_Syntax_formatStx___main___spec__2(lean_object*, lean_object*);
lean_object* l_List_toArrayAux___main___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_updateTrailing(lean_object*);
lean_object* l___private_init_lean_syntax_3__updateLast___main___at_Lean_Syntax_setTailInfoAux___main___spec__1(lean_object*);
lean_object* l_Lean_SyntaxNode_withArgs___rarg(lean_object*, lean_object*);
@ -69,12 +73,17 @@ lean_object* l_Lean_SyntaxNode_getArg(lean_object*);
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
lean_object* l___private_init_lean_syntax_2__updateLeadingAux___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_updateTrailing___main(lean_object*);
lean_object* l_Lean_mkNode___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_ifNode___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_lean_syntax_7__decodeHexLitAux___main(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Format_sbracket___closed__1;
lean_object* l_Lean_mkOptionalNode___rarg(lean_object*);
lean_object* l_List_redLength___main___rarg(lean_object*);
lean_object* l_Lean_mkOptionalNode(lean_object*);
lean_object* l_Lean_SyntaxNode_getNumArgs___rarg(lean_object*);
lean_object* l_Lean_Syntax_modifyArg___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_charLitKind___closed__2;
lean_object* l_Lean_mkIdentFrom(lean_object*);
lean_object* l_Lean_Syntax_setTailInfo(lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*);
lean_object* l_Array_ummapAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___boxed(lean_object*, lean_object*);
@ -85,6 +94,7 @@ lean_object* l_Lean_Syntax_formatStx___main___rarg___closed__2;
lean_object* l_Array_miterateAux___main___at_Lean_Syntax_reprint___main___spec__2(lean_object*);
lean_object* l_Lean_Syntax_mrewriteBottomUp___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mrewriteBottomUp(lean_object*, lean_object*);
lean_object* l_Array_mkEmpty(lean_object*, lean_object*);
lean_object* l_Lean_mkNumLit(lean_object*, lean_object*);
lean_object* l_Lean_SyntaxNode_withArgs(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_setTailInfoAux___rarg(lean_object*, lean_object*);
@ -105,6 +115,7 @@ lean_object* l_Lean_Syntax_setArg___rarg(lean_object*, lean_object*, lean_object
lean_object* l_Array_mfindRevAux___main___at_Lean_Syntax_getTailInfo___main___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_lean_syntax_9__decodeNatLitVal___closed__1;
lean_object* l_Lean_Syntax_getIdAt(lean_object*);
lean_object* l_Lean_mkAtomFrom___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mreplace___main___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_updateTrailing___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mreplace___boxed(lean_object*, lean_object*);
@ -114,6 +125,7 @@ lean_object* l_Lean_SyntaxNode_getKind(lean_object*);
lean_object* l_Lean_Syntax_Lean_HasFormat___closed__1;
lean_object* l_Lean_Syntax_updateTrailing___main___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_ifNodeKind(lean_object*, lean_object*);
lean_object* l_Lean_mkNode(lean_object*);
lean_object* l_Lean_Syntax_setAtomVal(lean_object*);
lean_object* l_List_map___main___at_Lean_Syntax_formatStx___main___spec__1(lean_object*);
lean_object* l_Lean_Syntax_Lean_HasFormat(lean_object*);
@ -128,6 +140,7 @@ lean_object* l_Lean_SourceInfo_appendToLeading(lean_object*, lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mrewriteBottomUp___main___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SyntaxNode_getArg___rarg(lean_object*, lean_object*);
lean_object* l_Lean_mkAtom(lean_object*);
uint8_t l_UInt32_decLe(uint32_t, uint32_t);
uint8_t l_Lean_Syntax_isOfKind___rarg(lean_object*, lean_object*);
lean_object* l___private_init_lean_syntax_2__updateLeadingAux(lean_object*);
@ -141,6 +154,7 @@ lean_object* l_Lean_Syntax_getHeadInfo___main(lean_object*);
lean_object* l_Lean_SyntaxNode_getIdAt___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getNumArgs___rarg___boxed(lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* lean_mk_syntax_atom(lean_object*);
lean_object* l_Lean_SourceInfo_truncateTrailing(lean_object*);
lean_object* l_Lean_Syntax_isStrLit___rarg(lean_object*);
lean_object* l_Array_miterateAux___main___at_Lean_Syntax_reprint___main___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -217,12 +231,14 @@ lean_object* l___private_init_lean_syntax_8__decodeDecimalLitAux___main___boxed(
uint8_t l_Char_isDigit(uint32_t);
lean_object* l_Lean_Syntax_modifyArgs___rarg(lean_object*, lean_object*);
lean_object* l___private_init_lean_syntax_3__updateLast___main___at_Lean_Syntax_setTailInfoAux___main___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkNullNode(lean_object*);
lean_object* l_Lean_Syntax_modifyArgs(lean_object*);
lean_object* l_Array_ummapAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_init_lean_syntax_3__updateLast___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getIdAt___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_reprint___main___rarg___closed__1;
lean_object* l_Lean_Syntax_getArgs___rarg___boxed(lean_object*);
lean_object* l_Lean_mkAtom___rarg(lean_object*);
lean_object* l_Lean_Name_replacePrefix___main(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Format_sbracket___closed__3;
lean_object* l_Lean_Syntax_rewriteBottomUp___rarg(lean_object*, lean_object*);
@ -233,6 +249,7 @@ extern lean_object* l_Lean_HasRepr___closed__1;
lean_object* l___private_init_lean_syntax_3__updateLast___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_formatStx___main___rarg___closed__1;
lean_object* lean_mk_syntax_list(lean_object*);
lean_object* l_Lean_mkNullNode___rarg(lean_object*);
lean_object* l_Array_ummapAux___main___at_Lean_Syntax_rewriteBottomUp___spec__2___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_formatDataValue___closed__2;
lean_object* lean_format_group(lean_object*);
@ -295,7 +312,6 @@ lean_object* l_Lean_SyntaxNode_getArgs___rarg(lean_object*);
lean_object* l_Lean_Syntax_mreplace(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_rewriteBottomUp(lean_object*);
lean_object* l_Lean_Syntax_isNatLitAux(lean_object*);
lean_object* lean_mk_syntax_atom(lean_object*);
lean_object* l_Lean_Syntax_mreplace___main(lean_object*, lean_object*);
lean_object* l_Lean_numLitKind___closed__1;
lean_object* l_Lean_Syntax_ifNodeKind___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -303,6 +319,7 @@ lean_object* l_Lean_mkLit(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_mul(lean_object*, lean_object*);
lean_object* l___private_init_lean_syntax_5__decodeBinLitAux___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mrewriteBottomUp___main___at_Lean_Syntax_rewriteBottomUp___spec__1(lean_object*);
lean_object* l_Lean_mkIdentFrom___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_modifyArg___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getTailInfo___rarg___boxed(lean_object*);
lean_object* l_Lean_Syntax_setArg___rarg___boxed(lean_object*, lean_object*, lean_object*);
@ -4674,6 +4691,103 @@ lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_mkAtom___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_box(0);
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_mkAtom(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_mkAtom___rarg), 1, 0);
return x_2;
}
}
lean_object* l_Lean_mkNode___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 = l_List_redLength___main___rarg(x_2);
x_4 = lean_mk_empty_array_with_capacity(x_3);
lean_dec(x_3);
x_5 = l_List_toArrayAux___main___rarg(x_2, x_4);
x_6 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_5);
return x_6;
}
}
lean_object* l_Lean_mkNode(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_mkNode___rarg), 2, 0);
return x_2;
}
}
lean_object* l_Lean_mkNullNode___rarg(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 = l_List_redLength___main___rarg(x_1);
x_3 = lean_mk_empty_array_with_capacity(x_2);
lean_dec(x_2);
x_4 = l_List_toArrayAux___main___rarg(x_1, x_3);
x_5 = l_Lean_nullKind;
x_6 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_6, 0, x_5);
lean_ctor_set(x_6, 1, x_4);
return x_6;
}
}
lean_object* l_Lean_mkNullNode(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_mkNullNode___rarg), 1, 0);
return x_2;
}
}
lean_object* l_Lean_mkOptionalNode___rarg(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_2;
x_2 = l_Lean_Syntax_asNode___rarg___closed__1;
return x_2;
}
else
{
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);
lean_dec(x_1);
x_4 = lean_unsigned_to_nat(1u);
x_5 = lean_mk_array(x_4, x_3);
x_6 = l_Lean_nullKind;
x_7 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_5);
return x_7;
}
}
}
lean_object* l_Lean_mkOptionalNode(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_mkOptionalNode___rarg), 1, 0);
return x_2;
}
}
lean_object* l_Lean_mkLit(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -5705,6 +5819,74 @@ lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_mkIdentFrom___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; lean_object* x_10;
x_3 = l_Lean_Syntax_getHeadInfo___main___rarg(x_1);
x_4 = l_System_FilePath_dirName___closed__1;
lean_inc(x_2);
x_5 = l_Lean_Name_toStringWithSep___main(x_4, x_2);
x_6 = lean_string_utf8_byte_size(x_5);
x_7 = lean_unsigned_to_nat(0u);
x_8 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_8, 0, x_5);
lean_ctor_set(x_8, 1, x_7);
lean_ctor_set(x_8, 2, x_6);
x_9 = lean_box(0);
x_10 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_10, 0, x_3);
lean_ctor_set(x_10, 1, x_8);
lean_ctor_set(x_10, 2, x_2);
lean_ctor_set(x_10, 3, x_9);
return x_10;
}
}
lean_object* l_Lean_mkIdentFrom(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_mkIdentFrom___rarg___boxed), 2, 0);
return x_2;
}
}
lean_object* l_Lean_mkIdentFrom___rarg___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_mkIdentFrom___rarg(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_mkAtomFrom___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = l_Lean_Syntax_getHeadInfo___main___rarg(x_1);
x_4 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_4, 0, x_3);
lean_ctor_set(x_4, 1, x_2);
return x_4;
}
}
lean_object* l_Lean_mkAtomFrom(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_mkAtomFrom___rarg___boxed), 2, 0);
return x_2;
}
}
lean_object* l_Lean_mkAtomFrom___rarg___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_mkAtomFrom___rarg(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* initialize_init_lean_name(lean_object*);
lean_object* initialize_init_lean_format(lean_object*);
lean_object* initialize_init_data_array_default(lean_object*);