chore: update stage0
This commit is contained in:
parent
e8cee6c56f
commit
a735778ae0
13 changed files with 4919 additions and 73645 deletions
979
stage0/library/Init/Data/PersistentArray/Basic.c
generated
979
stage0/library/Init/Data/PersistentArray/Basic.c
generated
File diff suppressed because it is too large
Load diff
225
stage0/library/Init/Data/PersistentHashMap/Basic.c
generated
225
stage0/library/Init/Data/PersistentHashMap/Basic.c
generated
|
|
@ -41,15 +41,14 @@ lean_object* l_PersistentHashMap_insert___rarg(lean_object*, lean_object*, lean_
|
|||
lean_object* l_PersistentHashMap_empty___rarg___closed__2;
|
||||
lean_object* l_PersistentHashMap_eraseAux___rarg(lean_object*, lean_object*, size_t, lean_object*);
|
||||
lean_object* l_PersistentHashMap_isEmpty(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_findAtAux___main(lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_insertAtCollisionNode(lean_object*, lean_object*);
|
||||
size_t l_USize_sub(size_t, size_t);
|
||||
lean_object* l_PersistentHashMap_Stats_toString(lean_object*);
|
||||
lean_object* l_PersistentHashMap_HasEmptyc(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_insertAtCollisionNodeAux(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_toList___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_findAtAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_mkCollisionNode___rarg___closed__1;
|
||||
lean_object* l_PersistentHashMap_foldlM___at_PersistentHashMap_toList___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -57,6 +56,7 @@ lean_object* l_PersistentHashMap_isUnaryEntries___rarg(lean_object*, lean_object
|
|||
lean_object* l_PersistentHashMap_containsAtAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_toList(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_getCollisionNodeSize(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_foldlMAux___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_findAtAux(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_getCollisionNodeSize___rarg(lean_object*);
|
||||
lean_object* l_PersistentHashMap_containsAux(lean_object*, lean_object*);
|
||||
|
|
@ -73,13 +73,11 @@ lean_object* l_PersistentHashMap_foldlMAux___main(lean_object*, lean_object*, le
|
|||
lean_object* l_PersistentHashMap_empty___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Nat_repr(lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_toList___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__2(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_findAux___rarg(lean_object*, lean_object*, size_t, lean_object*);
|
||||
lean_object* l_PersistentHashMap_find_x21___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_foldlMAux(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_insertAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_mod2Shift___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_containsAux___rarg(lean_object*, lean_object*, size_t, lean_object*);
|
||||
|
|
@ -104,8 +102,8 @@ lean_object* l_PersistentHashMap_foldlM___at_PersistentHashMap_toList___spec__1_
|
|||
lean_object* l_PersistentHashMap_findD___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_div2Shift___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_collectStats___main___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_foldlMAux___main___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_stats___rarg___closed__1;
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_containsAux___main(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_isUnaryEntries___main___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_collectStats___main___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -116,12 +114,10 @@ lean_object* l_PersistentHashMap_collectStats___rarg(lean_object*, lean_object*,
|
|||
lean_object* l_PersistentHashMap_Stats_toString___closed__1;
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_toList___spec__4(lean_object*, lean_object*);
|
||||
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__2___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_isEmpty___rarg___boxed(lean_object*);
|
||||
lean_object* l_PersistentHashMap_insertAux___main___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*);
|
||||
lean_object* lean_array_push(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_foldlM___at_PersistentHashMap_toList___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_indexOfAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_insertAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_empty___rarg(lean_object*, lean_object*);
|
||||
|
|
@ -174,6 +170,7 @@ lean_object* l_PersistentHashMap_isUnaryNode(lean_object*, lean_object*);
|
|||
lean_object* l_PersistentHashMap_insertAtCollisionNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_insertAux___main___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_containsAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_foldlMAux___main___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_USize_decLe(size_t, size_t);
|
||||
lean_object* l_PersistentHashMap_insertAux___main(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_eraseAux___main(lean_object*, lean_object*);
|
||||
|
|
@ -192,13 +189,13 @@ size_t l_PersistentHashMap_div2Shift(size_t, size_t);
|
|||
lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Nat_max(lean_object*, lean_object*);
|
||||
lean_object* lean_usize_to_nat(size_t);
|
||||
lean_object* l_PersistentHashMap_foldlMAux___main___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_findAux___main___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_mkCollisionNode(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_insertAux(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_foldlM(lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_PersistentHashMap_isEmpty___rarg(lean_object*);
|
||||
uint8_t l_PersistentHashMap_containsAtAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_insertAux___main___spec__1___rarg(lean_object*, lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_findAux(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_Inhabited___rarg(lean_object*, lean_object*);
|
||||
|
|
@ -2659,148 +2656,54 @@ x_3 = lean_alloc_closure((void*)(l_PersistentHashMap_erase___rarg), 4, 0);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___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* l_PersistentHashMap_foldlMAux___main___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_8; uint8_t x_9;
|
||||
x_8 = lean_array_get_size(x_5);
|
||||
x_9 = lean_nat_dec_lt(x_6, x_8);
|
||||
lean_dec(x_8);
|
||||
if (x_9 == 0)
|
||||
{
|
||||
lean_object* x_10; lean_object* x_11; lean_object* x_12;
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
x_10 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_10);
|
||||
lean_dec(x_1);
|
||||
x_11 = lean_ctor_get(x_10, 1);
|
||||
lean_inc(x_11);
|
||||
lean_dec(x_10);
|
||||
x_12 = lean_apply_2(x_11, lean_box(0), x_7);
|
||||
return x_12;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
|
||||
x_13 = lean_ctor_get(x_1, 1);
|
||||
lean_inc(x_13);
|
||||
x_14 = lean_array_fget(x_5, x_6);
|
||||
x_15 = lean_unsigned_to_nat(1u);
|
||||
x_16 = lean_nat_add(x_6, x_15);
|
||||
lean_inc(x_3);
|
||||
lean_inc(x_1);
|
||||
x_17 = lean_alloc_closure((void*)(l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__1___rarg___boxed), 7, 6);
|
||||
lean_closure_set(x_17, 0, x_1);
|
||||
lean_closure_set(x_17, 1, lean_box(0));
|
||||
lean_closure_set(x_17, 2, x_3);
|
||||
lean_closure_set(x_17, 3, x_4);
|
||||
lean_closure_set(x_17, 4, x_5);
|
||||
lean_closure_set(x_17, 5, x_16);
|
||||
switch (lean_obj_tag(x_14)) {
|
||||
switch (lean_obj_tag(x_4)) {
|
||||
case 0:
|
||||
{
|
||||
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
|
||||
lean_dec(x_1);
|
||||
x_18 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_18);
|
||||
x_19 = lean_ctor_get(x_14, 1);
|
||||
lean_inc(x_19);
|
||||
lean_dec(x_14);
|
||||
x_20 = lean_apply_3(x_3, x_7, x_18, x_19);
|
||||
x_21 = lean_apply_4(x_13, lean_box(0), lean_box(0), x_20, x_17);
|
||||
return x_21;
|
||||
lean_object* x_6; lean_object* x_7; lean_object* x_8;
|
||||
lean_dec(x_2);
|
||||
x_6 = lean_ctor_get(x_4, 0);
|
||||
lean_inc(x_6);
|
||||
x_7 = lean_ctor_get(x_4, 1);
|
||||
lean_inc(x_7);
|
||||
lean_dec(x_4);
|
||||
x_8 = lean_apply_3(x_1, x_5, x_6, x_7);
|
||||
return x_8;
|
||||
}
|
||||
case 1:
|
||||
{
|
||||
lean_object* x_22; lean_object* x_23; lean_object* x_24;
|
||||
x_22 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_22);
|
||||
lean_dec(x_14);
|
||||
x_23 = l_PersistentHashMap_foldlMAux___main___rarg(x_1, lean_box(0), x_3, x_22, x_7);
|
||||
x_24 = lean_apply_4(x_13, lean_box(0), lean_box(0), x_23, x_17);
|
||||
return x_24;
|
||||
lean_object* x_9; lean_object* x_10;
|
||||
x_9 = lean_ctor_get(x_4, 0);
|
||||
lean_inc(x_9);
|
||||
lean_dec(x_4);
|
||||
x_10 = l_PersistentHashMap_foldlMAux___main___rarg(x_2, lean_box(0), x_1, x_9, x_5);
|
||||
return x_10;
|
||||
}
|
||||
default:
|
||||
{
|
||||
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
|
||||
lean_dec(x_3);
|
||||
x_25 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_25);
|
||||
lean_dec(x_1);
|
||||
x_26 = lean_ctor_get(x_25, 1);
|
||||
lean_inc(x_26);
|
||||
lean_dec(x_25);
|
||||
x_27 = lean_apply_2(x_26, lean_box(0), x_7);
|
||||
x_28 = lean_apply_4(x_13, lean_box(0), lean_box(0), x_27, x_17);
|
||||
return x_28;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = lean_alloc_closure((void*)(l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__1___rarg___boxed), 7, 0);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__2___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_array_get_size(x_6);
|
||||
x_10 = lean_nat_dec_lt(x_7, x_9);
|
||||
lean_dec(x_9);
|
||||
if (x_10 == 0)
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
x_11 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_11);
|
||||
lean_dec(x_1);
|
||||
x_11 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_11);
|
||||
lean_dec(x_2);
|
||||
x_12 = lean_ctor_get(x_11, 1);
|
||||
lean_inc(x_12);
|
||||
lean_dec(x_11);
|
||||
x_13 = lean_apply_2(x_12, lean_box(0), x_8);
|
||||
x_13 = lean_apply_2(x_12, lean_box(0), x_5);
|
||||
return x_13;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
|
||||
x_14 = lean_ctor_get(x_1, 1);
|
||||
lean_inc(x_14);
|
||||
x_15 = lean_array_fget(x_6, x_7);
|
||||
x_16 = lean_array_fget(x_5, x_7);
|
||||
lean_inc(x_3);
|
||||
x_17 = lean_apply_3(x_3, x_8, x_15, x_16);
|
||||
x_18 = lean_unsigned_to_nat(1u);
|
||||
x_19 = lean_nat_add(x_7, x_18);
|
||||
x_20 = lean_alloc_closure((void*)(l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__2___rarg___boxed), 8, 7);
|
||||
lean_closure_set(x_20, 0, x_1);
|
||||
lean_closure_set(x_20, 1, lean_box(0));
|
||||
lean_closure_set(x_20, 2, x_3);
|
||||
lean_closure_set(x_20, 3, x_4);
|
||||
lean_closure_set(x_20, 4, x_5);
|
||||
lean_closure_set(x_20, 5, x_6);
|
||||
lean_closure_set(x_20, 6, x_19);
|
||||
x_21 = lean_apply_4(x_14, lean_box(0), lean_box(0), x_17, x_20);
|
||||
return x_21;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_PersistentHashMap_foldlMAux___main___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_4;
|
||||
x_4 = lean_alloc_closure((void*)(l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__2___rarg___boxed), 8, 0);
|
||||
return x_4;
|
||||
lean_object* x_6; lean_object* x_7;
|
||||
x_6 = lean_array_fget(x_1, x_3);
|
||||
x_7 = lean_apply_3(x_2, x_5, x_4, x_6);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentHashMap_foldlMAux___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
|
|
@ -2808,27 +2711,32 @@ _start:
|
|||
{
|
||||
if (lean_obj_tag(x_4) == 0)
|
||||
{
|
||||
lean_object* x_6; lean_object* x_7; lean_object* x_8;
|
||||
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
|
||||
x_6 = lean_ctor_get(x_4, 0);
|
||||
lean_inc(x_6);
|
||||
lean_dec(x_4);
|
||||
x_7 = lean_unsigned_to_nat(0u);
|
||||
lean_inc(x_6);
|
||||
x_8 = l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__1___rarg(x_1, lean_box(0), x_3, x_6, x_6, x_7, x_5);
|
||||
return x_8;
|
||||
lean_inc(x_1);
|
||||
x_7 = lean_alloc_closure((void*)(l_PersistentHashMap_foldlMAux___main___rarg___lambda__1___boxed), 5, 2);
|
||||
lean_closure_set(x_7, 0, x_3);
|
||||
lean_closure_set(x_7, 1, x_1);
|
||||
x_8 = lean_unsigned_to_nat(0u);
|
||||
x_9 = l_Array_iterateMAux___main___rarg(x_1, lean_box(0), x_6, x_7, x_8, x_5);
|
||||
return x_9;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
|
||||
x_9 = lean_ctor_get(x_4, 0);
|
||||
lean_inc(x_9);
|
||||
x_10 = lean_ctor_get(x_4, 1);
|
||||
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
|
||||
x_10 = lean_ctor_get(x_4, 0);
|
||||
lean_inc(x_10);
|
||||
x_11 = lean_ctor_get(x_4, 1);
|
||||
lean_inc(x_11);
|
||||
lean_dec(x_4);
|
||||
x_11 = lean_unsigned_to_nat(0u);
|
||||
lean_inc(x_9);
|
||||
x_12 = l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__2___rarg(x_1, lean_box(0), x_3, x_9, x_10, x_9, x_11, x_5);
|
||||
return x_12;
|
||||
x_12 = lean_alloc_closure((void*)(l_PersistentHashMap_foldlMAux___main___rarg___lambda__2___boxed), 5, 2);
|
||||
lean_closure_set(x_12, 0, x_11);
|
||||
lean_closure_set(x_12, 1, x_3);
|
||||
x_13 = lean_unsigned_to_nat(0u);
|
||||
x_14 = l_Array_iterateMAux___main___rarg(x_1, lean_box(0), x_10, x_12, x_13, x_5);
|
||||
return x_14;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -2840,40 +2748,23 @@ x_4 = lean_alloc_closure((void*)(l_PersistentHashMap_foldlMAux___main___rarg), 5
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___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* l_PersistentHashMap_foldlMAux___main___rarg___lambda__1___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_8;
|
||||
x_8 = l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__1___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
|
||||
lean_dec(x_6);
|
||||
return x_8;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__1(x_1, x_2, x_3);
|
||||
lean_object* x_6;
|
||||
x_6 = l_PersistentHashMap_foldlMAux___main___rarg___lambda__1(x_1, x_2, x_3, x_4, x_5);
|
||||
lean_dec(x_3);
|
||||
return x_4;
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__2___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) {
|
||||
lean_object* l_PersistentHashMap_foldlMAux___main___rarg___lambda__2___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_9;
|
||||
x_9 = l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__2___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
lean_dec(x_7);
|
||||
return x_9;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_Array_iterateMAux___main___at_PersistentHashMap_foldlMAux___main___spec__2(x_1, x_2, x_3);
|
||||
lean_object* x_6;
|
||||
x_6 = l_PersistentHashMap_foldlMAux___main___rarg___lambda__2(x_1, x_2, x_3, x_4, x_5);
|
||||
lean_dec(x_3);
|
||||
return x_4;
|
||||
lean_dec(x_1);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_PersistentHashMap_foldlMAux___main___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
|
|
|
|||
304
stage0/library/Init/Lean/Compiler/IR/NormIds.c
generated
304
stage0/library/Init/Lean/Compiler/IR/NormIds.c
generated
|
|
@ -96,15 +96,16 @@ lean_object* l_Lean_IR_MapVars_mapArgs___at_Lean_IR_FnBody_replaceVar___spec__11
|
|||
lean_object* l_Lean_IR_MapVars_mapArgs___at_Lean_IR_FnBody_replaceVar___spec__9(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_array_get_size(lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_IR_NormalizeIds_withParams___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_IR_MapVars_mapFnBody___main___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_IR_FnBody_replaceVar___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_IR_NormalizeIds_withJP(lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_IR_NormalizeIds_normArgs___spec__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_IR_MapVars_mapFnBody___main___spec__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_IR_NormalizeIds_MtoN___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_array_fget(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_IR_NormalizeIds_normIndex(lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_IR_FnBody_replaceVar___spec__15(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_IR_MapVars_mapFnBody___main___lambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_IR_FnBody_replaceVar___spec__6(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_IR_MapVars_mapFnBody(lean_object*, lean_object*);
|
||||
|
|
@ -3442,66 +3443,58 @@ return x_99;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_IR_MapVars_mapFnBody___main___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_Lean_IR_MapVars_mapFnBody___main___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; uint8_t x_5;
|
||||
x_4 = lean_array_get_size(x_3);
|
||||
x_5 = lean_nat_dec_lt(x_2, x_4);
|
||||
lean_dec(x_4);
|
||||
if (x_5 == 0)
|
||||
if (lean_obj_tag(x_3) == 0)
|
||||
{
|
||||
lean_object* x_6; lean_object* x_7;
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_6 = l_Array_empty___closed__1;
|
||||
x_7 = x_3;
|
||||
return x_7;
|
||||
uint8_t x_4;
|
||||
x_4 = !lean_is_exclusive(x_3);
|
||||
if (x_4 == 0)
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6;
|
||||
x_5 = lean_ctor_get(x_3, 1);
|
||||
x_6 = l_Lean_IR_MapVars_mapFnBody___main(x_1, x_5);
|
||||
lean_ctor_set(x_3, 1, x_6);
|
||||
return x_3;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
x_8 = lean_array_fget(x_3, x_2);
|
||||
x_9 = lean_box(0);
|
||||
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
x_7 = lean_ctor_get(x_3, 0);
|
||||
x_8 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_8);
|
||||
x_10 = x_9;
|
||||
x_11 = lean_array_fset(x_3, x_2, x_10);
|
||||
x_12 = lean_unsigned_to_nat(1u);
|
||||
x_13 = lean_nat_add(x_2, x_12);
|
||||
if (lean_obj_tag(x_8) == 0)
|
||||
{
|
||||
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
|
||||
x_14 = lean_ctor_get(x_8, 0);
|
||||
lean_inc(x_14);
|
||||
x_15 = lean_ctor_get(x_8, 1);
|
||||
lean_inc(x_15);
|
||||
lean_inc(x_1);
|
||||
x_16 = l_Lean_IR_MapVars_mapFnBody___main(x_1, x_15);
|
||||
x_17 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_17, 0, x_14);
|
||||
lean_ctor_set(x_17, 1, x_16);
|
||||
x_18 = x_17;
|
||||
x_19 = lean_array_fset(x_11, x_2, x_18);
|
||||
lean_dec(x_2);
|
||||
x_2 = x_13;
|
||||
x_3 = x_19;
|
||||
goto _start;
|
||||
lean_inc(x_7);
|
||||
lean_dec(x_3);
|
||||
x_9 = l_Lean_IR_MapVars_mapFnBody___main(x_1, x_8);
|
||||
x_10 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_10, 0, x_7);
|
||||
lean_ctor_set(x_10, 1, x_9);
|
||||
return x_10;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
|
||||
x_21 = lean_ctor_get(x_8, 0);
|
||||
lean_inc(x_21);
|
||||
lean_inc(x_1);
|
||||
x_22 = l_Lean_IR_MapVars_mapFnBody___main(x_1, x_21);
|
||||
x_23 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_23, 0, x_22);
|
||||
x_24 = x_23;
|
||||
x_25 = lean_array_fset(x_11, x_2, x_24);
|
||||
lean_dec(x_2);
|
||||
x_2 = x_13;
|
||||
x_3 = x_25;
|
||||
goto _start;
|
||||
uint8_t x_11;
|
||||
x_11 = !lean_is_exclusive(x_3);
|
||||
if (x_11 == 0)
|
||||
{
|
||||
lean_object* x_12; lean_object* x_13;
|
||||
x_12 = lean_ctor_get(x_3, 0);
|
||||
x_13 = l_Lean_IR_MapVars_mapFnBody___main(x_1, x_12);
|
||||
lean_ctor_set(x_3, 0, x_13);
|
||||
return x_3;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_14; lean_object* x_15; lean_object* x_16;
|
||||
x_14 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_14);
|
||||
lean_dec(x_3);
|
||||
x_15 = l_Lean_IR_MapVars_mapFnBody___main(x_1, x_14);
|
||||
x_16 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_16, 0, x_15);
|
||||
return x_16;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -3972,144 +3965,150 @@ uint8_t x_137;
|
|||
x_137 = !lean_is_exclusive(x_2);
|
||||
if (x_137 == 0)
|
||||
{
|
||||
lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142;
|
||||
lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144;
|
||||
x_138 = lean_ctor_get(x_2, 1);
|
||||
x_139 = lean_ctor_get(x_2, 3);
|
||||
lean_inc(x_1);
|
||||
x_140 = lean_apply_1(x_1, x_138);
|
||||
x_141 = lean_unsigned_to_nat(0u);
|
||||
x_142 = l_Array_umapMAux___main___at_Lean_IR_MapVars_mapFnBody___main___spec__1(x_1, x_141, x_139);
|
||||
lean_ctor_set(x_2, 3, x_142);
|
||||
x_141 = lean_alloc_closure((void*)(l_Lean_IR_MapVars_mapFnBody___main___lambda__1___boxed), 3, 1);
|
||||
lean_closure_set(x_141, 0, x_1);
|
||||
x_142 = l_Id_Monad;
|
||||
x_143 = lean_unsigned_to_nat(0u);
|
||||
x_144 = l_Array_umapMAux___main___rarg(x_142, lean_box(0), x_141, x_143, x_139);
|
||||
lean_ctor_set(x_2, 3, x_144);
|
||||
lean_ctor_set(x_2, 1, x_140);
|
||||
return x_2;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_143; lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; lean_object* x_150;
|
||||
x_143 = lean_ctor_get(x_2, 0);
|
||||
x_144 = lean_ctor_get(x_2, 1);
|
||||
x_145 = lean_ctor_get(x_2, 2);
|
||||
x_146 = lean_ctor_get(x_2, 3);
|
||||
lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151; lean_object* x_152; lean_object* x_153; lean_object* x_154;
|
||||
x_145 = lean_ctor_get(x_2, 0);
|
||||
x_146 = lean_ctor_get(x_2, 1);
|
||||
x_147 = lean_ctor_get(x_2, 2);
|
||||
x_148 = lean_ctor_get(x_2, 3);
|
||||
lean_inc(x_148);
|
||||
lean_inc(x_147);
|
||||
lean_inc(x_146);
|
||||
lean_inc(x_145);
|
||||
lean_inc(x_144);
|
||||
lean_inc(x_143);
|
||||
lean_dec(x_2);
|
||||
lean_inc(x_1);
|
||||
x_147 = lean_apply_1(x_1, x_144);
|
||||
x_148 = lean_unsigned_to_nat(0u);
|
||||
x_149 = l_Array_umapMAux___main___at_Lean_IR_MapVars_mapFnBody___main___spec__1(x_1, x_148, x_146);
|
||||
x_150 = lean_alloc_ctor(10, 4, 0);
|
||||
lean_ctor_set(x_150, 0, x_143);
|
||||
lean_ctor_set(x_150, 1, x_147);
|
||||
lean_ctor_set(x_150, 2, x_145);
|
||||
lean_ctor_set(x_150, 3, x_149);
|
||||
return x_150;
|
||||
x_149 = lean_apply_1(x_1, x_146);
|
||||
x_150 = lean_alloc_closure((void*)(l_Lean_IR_MapVars_mapFnBody___main___lambda__1___boxed), 3, 1);
|
||||
lean_closure_set(x_150, 0, x_1);
|
||||
x_151 = l_Id_Monad;
|
||||
x_152 = lean_unsigned_to_nat(0u);
|
||||
x_153 = l_Array_umapMAux___main___rarg(x_151, lean_box(0), x_150, x_152, x_148);
|
||||
x_154 = lean_alloc_ctor(10, 4, 0);
|
||||
lean_ctor_set(x_154, 0, x_145);
|
||||
lean_ctor_set(x_154, 1, x_149);
|
||||
lean_ctor_set(x_154, 2, x_147);
|
||||
lean_ctor_set(x_154, 3, x_153);
|
||||
return x_154;
|
||||
}
|
||||
}
|
||||
case 11:
|
||||
{
|
||||
uint8_t x_151;
|
||||
x_151 = !lean_is_exclusive(x_2);
|
||||
if (x_151 == 0)
|
||||
uint8_t x_155;
|
||||
x_155 = !lean_is_exclusive(x_2);
|
||||
if (x_155 == 0)
|
||||
{
|
||||
lean_object* x_152;
|
||||
x_152 = lean_ctor_get(x_2, 0);
|
||||
if (lean_obj_tag(x_152) == 0)
|
||||
lean_object* x_156;
|
||||
x_156 = lean_ctor_get(x_2, 0);
|
||||
if (lean_obj_tag(x_156) == 0)
|
||||
{
|
||||
uint8_t x_153;
|
||||
x_153 = !lean_is_exclusive(x_152);
|
||||
if (x_153 == 0)
|
||||
uint8_t x_157;
|
||||
x_157 = !lean_is_exclusive(x_156);
|
||||
if (x_157 == 0)
|
||||
{
|
||||
lean_object* x_154; lean_object* x_155;
|
||||
x_154 = lean_ctor_get(x_152, 0);
|
||||
x_155 = lean_apply_1(x_1, x_154);
|
||||
lean_ctor_set(x_152, 0, x_155);
|
||||
lean_object* x_158; lean_object* x_159;
|
||||
x_158 = lean_ctor_get(x_156, 0);
|
||||
x_159 = lean_apply_1(x_1, x_158);
|
||||
lean_ctor_set(x_156, 0, x_159);
|
||||
return x_2;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_156; lean_object* x_157; lean_object* x_158;
|
||||
x_156 = lean_ctor_get(x_152, 0);
|
||||
lean_inc(x_156);
|
||||
lean_dec(x_152);
|
||||
x_157 = lean_apply_1(x_1, x_156);
|
||||
x_158 = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(x_158, 0, x_157);
|
||||
lean_ctor_set(x_2, 0, x_158);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_159;
|
||||
x_159 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_159);
|
||||
lean_dec(x_2);
|
||||
if (lean_obj_tag(x_159) == 0)
|
||||
{
|
||||
lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164;
|
||||
x_160 = lean_ctor_get(x_159, 0);
|
||||
lean_object* x_160; lean_object* x_161; lean_object* x_162;
|
||||
x_160 = lean_ctor_get(x_156, 0);
|
||||
lean_inc(x_160);
|
||||
if (lean_is_exclusive(x_159)) {
|
||||
lean_ctor_release(x_159, 0);
|
||||
x_161 = x_159;
|
||||
} else {
|
||||
lean_dec_ref(x_159);
|
||||
x_161 = lean_box(0);
|
||||
lean_dec(x_156);
|
||||
x_161 = lean_apply_1(x_1, x_160);
|
||||
x_162 = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(x_162, 0, x_161);
|
||||
lean_ctor_set(x_2, 0, x_162);
|
||||
return x_2;
|
||||
}
|
||||
x_162 = lean_apply_1(x_1, x_160);
|
||||
if (lean_is_scalar(x_161)) {
|
||||
x_163 = lean_alloc_ctor(0, 1, 0);
|
||||
} else {
|
||||
x_163 = x_161;
|
||||
}
|
||||
lean_ctor_set(x_163, 0, x_162);
|
||||
x_164 = lean_alloc_ctor(11, 1, 0);
|
||||
lean_ctor_set(x_164, 0, x_163);
|
||||
return x_164;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_165;
|
||||
lean_dec(x_1);
|
||||
x_165 = lean_alloc_ctor(11, 1, 0);
|
||||
lean_ctor_set(x_165, 0, x_159);
|
||||
return x_165;
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_163;
|
||||
x_163 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_163);
|
||||
lean_dec(x_2);
|
||||
if (lean_obj_tag(x_163) == 0)
|
||||
{
|
||||
lean_object* x_164; lean_object* x_165; lean_object* x_166; lean_object* x_167; lean_object* x_168;
|
||||
x_164 = lean_ctor_get(x_163, 0);
|
||||
lean_inc(x_164);
|
||||
if (lean_is_exclusive(x_163)) {
|
||||
lean_ctor_release(x_163, 0);
|
||||
x_165 = x_163;
|
||||
} else {
|
||||
lean_dec_ref(x_163);
|
||||
x_165 = lean_box(0);
|
||||
}
|
||||
x_166 = lean_apply_1(x_1, x_164);
|
||||
if (lean_is_scalar(x_165)) {
|
||||
x_167 = lean_alloc_ctor(0, 1, 0);
|
||||
} else {
|
||||
x_167 = x_165;
|
||||
}
|
||||
lean_ctor_set(x_167, 0, x_166);
|
||||
x_168 = lean_alloc_ctor(11, 1, 0);
|
||||
lean_ctor_set(x_168, 0, x_167);
|
||||
return x_168;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_169;
|
||||
lean_dec(x_1);
|
||||
x_169 = lean_alloc_ctor(11, 1, 0);
|
||||
lean_ctor_set(x_169, 0, x_163);
|
||||
return x_169;
|
||||
}
|
||||
}
|
||||
}
|
||||
case 12:
|
||||
{
|
||||
uint8_t x_166;
|
||||
x_166 = !lean_is_exclusive(x_2);
|
||||
if (x_166 == 0)
|
||||
uint8_t x_170;
|
||||
x_170 = !lean_is_exclusive(x_2);
|
||||
if (x_170 == 0)
|
||||
{
|
||||
lean_object* x_167; lean_object* x_168;
|
||||
x_167 = lean_ctor_get(x_2, 1);
|
||||
x_168 = l_Lean_IR_MapVars_mapArgs(x_1, x_167);
|
||||
lean_ctor_set(x_2, 1, x_168);
|
||||
lean_object* x_171; lean_object* x_172;
|
||||
x_171 = lean_ctor_get(x_2, 1);
|
||||
x_172 = l_Lean_IR_MapVars_mapArgs(x_1, x_171);
|
||||
lean_ctor_set(x_2, 1, x_172);
|
||||
return x_2;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_169; lean_object* x_170; lean_object* x_171; lean_object* x_172;
|
||||
x_169 = lean_ctor_get(x_2, 0);
|
||||
x_170 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_170);
|
||||
lean_inc(x_169);
|
||||
lean_object* x_173; lean_object* x_174; lean_object* x_175; lean_object* x_176;
|
||||
x_173 = lean_ctor_get(x_2, 0);
|
||||
x_174 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_174);
|
||||
lean_inc(x_173);
|
||||
lean_dec(x_2);
|
||||
x_171 = l_Lean_IR_MapVars_mapArgs(x_1, x_170);
|
||||
x_172 = lean_alloc_ctor(12, 2, 0);
|
||||
lean_ctor_set(x_172, 0, x_169);
|
||||
lean_ctor_set(x_172, 1, x_171);
|
||||
return x_172;
|
||||
x_175 = l_Lean_IR_MapVars_mapArgs(x_1, x_174);
|
||||
x_176 = lean_alloc_ctor(12, 2, 0);
|
||||
lean_ctor_set(x_176, 0, x_173);
|
||||
lean_ctor_set(x_176, 1, x_175);
|
||||
return x_176;
|
||||
}
|
||||
}
|
||||
default:
|
||||
|
|
@ -4120,6 +4119,15 @@ return x_2;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_IR_MapVars_mapFnBody___main___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_Lean_IR_MapVars_mapFnBody___main___lambda__1(x_1, x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_IR_MapVars_mapFnBody(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
|
|
|
|||
4
stage0/library/Init/Lean/Environment.c
generated
4
stage0/library/Init/Lean/Environment.c
generated
|
|
@ -147,6 +147,7 @@ lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Environment_10_
|
|||
lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__3(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_matchConst(lean_object*);
|
||||
lean_object* l_Lean_regNamespacesExtension___lambda__1(lean_object*);
|
||||
lean_object* l_PersistentArray_foldlMAux___main___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_EnvExtension_setState___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Environment_find___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_io_initializing(lean_object*);
|
||||
|
|
@ -394,7 +395,6 @@ lean_object* l_Lean_mkEmptyEnvironment___boxed(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_registerPersistentEnvExtension___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
|
||||
extern lean_object* l_Lean_Name_toString___closed__1;
|
||||
lean_object* l_PersistentArray_foldlM___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyMAux___main___at_Lean_registerSimplePersistentEnvExtension___spec__2(lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Environment_contains(lean_object*, lean_object*);
|
||||
|
|
@ -4820,7 +4820,7 @@ lean_object* l_Lean_mkStateFromImportedEntries___rarg___lambda__1(lean_object* x
|
|||
_start:
|
||||
{
|
||||
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
|
||||
x_5 = lean_alloc_closure((void*)(l_PersistentArray_foldlM___rarg___lambda__1___boxed), 4, 1);
|
||||
x_5 = lean_alloc_closure((void*)(l_PersistentArray_foldlMAux___main___rarg___lambda__2___boxed), 4, 1);
|
||||
lean_closure_set(x_5, 0, x_1);
|
||||
x_6 = l_Id_Monad;
|
||||
x_7 = lean_unsigned_to_nat(0u);
|
||||
|
|
|
|||
3144
stage0/library/Init/Lean/Meta/Basic.c
generated
3144
stage0/library/Init/Lean/Meta/Basic.c
generated
File diff suppressed because it is too large
Load diff
1566
stage0/library/Init/Lean/Meta/Default.c
generated
1566
stage0/library/Init/Lean/Meta/Default.c
generated
File diff suppressed because it is too large
Load diff
42194
stage0/library/Init/Lean/Meta/ExprDefEq.c
generated
42194
stage0/library/Init/Lean/Meta/ExprDefEq.c
generated
File diff suppressed because it is too large
Load diff
5849
stage0/library/Init/Lean/Meta/InferType.c
generated
5849
stage0/library/Init/Lean/Meta/InferType.c
generated
File diff suppressed because it is too large
Load diff
11320
stage0/library/Init/Lean/Meta/WHNF.c
generated
11320
stage0/library/Init/Lean/Meta/WHNF.c
generated
File diff suppressed because it is too large
Load diff
2690
stage0/library/Init/Lean/MetavarContext.c
generated
2690
stage0/library/Init/Lean/MetavarContext.c
generated
File diff suppressed because it is too large
Load diff
277
stage0/library/Init/Lean/Syntax.c
generated
277
stage0/library/Init/Lean/Syntax.c
generated
|
|
@ -19,6 +19,7 @@ lean_object* l_List_map___main___at_Lean_Syntax_formatStx___main___spec__3(lean_
|
|||
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_setTailInfoAux(lean_object*);
|
||||
lean_object* l_Lean_Syntax_setTailInfoAux___main(lean_object*);
|
||||
lean_object* l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_toNat___rarg___boxed(lean_object*);
|
||||
uint8_t lean_name_dec_eq(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkAtomFrom___rarg___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -35,9 +36,9 @@ lean_object* l_Lean_mkAtomFrom(lean_object*);
|
|||
lean_object* l_Lean_nullKind___closed__2;
|
||||
lean_object* l_Lean_stxInh(lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_rewriteBottomUp___spec__2___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_setArg(lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Format_paren___closed__2;
|
||||
lean_object* l___private_Init_Lean_Syntax_4__reprintLeaf___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_unreachIsNodeOther(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -49,7 +50,6 @@ lean_object* l___private_Init_Lean_Syntax_5__decodeBinLitAux(lean_object*, lean_
|
|||
lean_object* l_Lean_Syntax_getTailInfo___main___rarg___boxed(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getId(lean_object*);
|
||||
lean_object* l_Lean_Syntax_toNat(lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkStrLit(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_strLitKind___closed__1;
|
||||
lean_object* l_Lean_Syntax_reprint___main___rarg(lean_object*);
|
||||
|
|
@ -61,7 +61,6 @@ 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___private_Init_Lean_Syntax_3__updateLast___main(lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___boxed(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*);
|
||||
|
|
@ -94,6 +93,7 @@ lean_object* l___private_Init_Lean_Syntax_9__decodeNatLitVal(lean_object*);
|
|||
lean_object* l_Lean_Syntax_getArg(lean_object*);
|
||||
lean_object* l_Lean_Syntax_setAtomVal___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_HasToString(lean_object*);
|
||||
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getHeadInfo___rarg___boxed(lean_object*);
|
||||
lean_object* l_Array_findRevMAux___main___at_Lean_Syntax_getTailInfo___main___spec__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_formatStx___main___rarg___closed__2;
|
||||
|
|
@ -102,29 +102,24 @@ lean_object* l_Lean_Syntax_mrewriteBottomUp(lean_object*, lean_object*);
|
|||
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
|
||||
lean_object* l_Lean_mkNumLit(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_withArgs(lean_object*, lean_object*);
|
||||
lean_object* l_Array_umapMAux___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_Lean_Syntax_setTailInfoAux___rarg(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Syntax_9__decodeNatLitVal___boxed(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getHeadInfo___rarg(lean_object*);
|
||||
lean_object* l_Lean_Syntax_isNatLit___rarg___boxed(lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_SourceInfo_updateTrailing(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getTailInfo___main___rarg(lean_object*);
|
||||
lean_object* l_Array_toList___rarg(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Syntax_2__updateLeadingAux(lean_object*);
|
||||
lean_object* l_Lean_Syntax_lift(lean_object*, lean_object*);
|
||||
lean_object* l_Nat_repr(lean_object*);
|
||||
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__3(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_formatStx___main___rarg___closed__3;
|
||||
lean_object* l_Lean_Syntax_formatStx___rarg(lean_object*);
|
||||
extern lean_object* l_Lean_Format_sbracket___closed__2;
|
||||
lean_object* l_Lean_Syntax_setArg___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
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_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1(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*);
|
||||
lean_object* l_Lean_numLitKind___closed__2;
|
||||
|
|
@ -172,7 +167,7 @@ lean_object* l_Lean_Syntax_getPos___rarg___boxed(lean_object*);
|
|||
lean_object* l_Lean_Syntax_getHeadInfo___main___rarg(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getId___rarg(lean_object*);
|
||||
lean_object* l_Lean_unreachIsNodeAtom(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findMAux___main___at_Lean_Syntax_getHeadInfo___main___spec__1(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Syntax_5__decodeBinLitAux___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_name_mk_string(lean_object*, lean_object*);
|
||||
|
|
@ -205,6 +200,7 @@ lean_object* l___private_Init_Lean_Syntax_6__decodeOctalLitAux(lean_object*, lea
|
|||
lean_object* l_List_map___main___at_Lean_Syntax_formatStx___main___spec__1___rarg(lean_object*);
|
||||
lean_object* l_Lean_Syntax_setArgs(lean_object*);
|
||||
lean_object* l_Lean_choiceKind___closed__2;
|
||||
lean_object* l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_reprint(lean_object*);
|
||||
lean_object* l_Lean_fieldIdxKind___closed__2;
|
||||
lean_object* l_Lean_Syntax_getHeadInfo(lean_object*);
|
||||
|
|
@ -234,7 +230,6 @@ lean_object* l_Lean_SyntaxNode_getArg___rarg___boxed(lean_object*, lean_object*)
|
|||
lean_object* l_Lean_Syntax_setArgs___rarg(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Lean_Syntax_7__decodeHexLitAux___main___boxed(lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Char_isDigit(uint32_t);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_modifyArgs___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkNullNode(lean_object*);
|
||||
lean_object* l_Lean_Syntax_modifyArgs(lean_object*);
|
||||
|
|
@ -257,7 +252,6 @@ lean_object* l_Lean_mkNullNode___rarg(lean_object*);
|
|||
extern lean_object* l_Lean_formatDataValue___closed__2;
|
||||
lean_object* lean_format_group(lean_object*);
|
||||
lean_object* l_Lean_Syntax_isIdOrAtom___rarg(lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_getArgs(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getIdAt___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_isStrLit(lean_object*);
|
||||
|
|
@ -266,7 +260,7 @@ lean_object* l_Lean_Syntax_getArg___rarg___boxed(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Syntax_updateLeading___rarg(lean_object*);
|
||||
lean_object* lean_mk_syntax_num_lit(lean_object*);
|
||||
lean_object* l_Lean_Syntax_getPos(lean_object*);
|
||||
lean_object* l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_reprint___main___rarg___boxed(lean_object*);
|
||||
lean_object* l___private_Init_Lean_Syntax_7__decodeHexLitAux___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_SourceInfo_appendToTrailing(lean_object*, lean_object*);
|
||||
|
|
@ -283,6 +277,7 @@ lean_object* l_Lean_Syntax_isFieldIdx___rarg(lean_object*);
|
|||
lean_object* lean_string_utf8_next(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_getIdAt___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_updateLeading___spec__2(lean_object*);
|
||||
lean_object* l_Lean_Syntax_ifNodeKind___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_reprint___main___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -1695,74 +1690,6 @@ lean_dec(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
|
||||
x_7 = lean_unsigned_to_nat(1u);
|
||||
x_8 = lean_nat_add(x_1, x_7);
|
||||
x_9 = x_6;
|
||||
x_10 = lean_array_fset(x_3, x_1, x_9);
|
||||
x_11 = l_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1___rarg(x_4, x_5, x_8, x_10);
|
||||
return x_11;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1___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_array_get_size(x_4);
|
||||
x_6 = lean_nat_dec_lt(x_3, x_5);
|
||||
lean_dec(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_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
x_7 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_7);
|
||||
lean_dec(x_1);
|
||||
x_8 = lean_ctor_get(x_7, 1);
|
||||
lean_inc(x_8);
|
||||
lean_dec(x_7);
|
||||
x_9 = l_Array_empty___closed__1;
|
||||
x_10 = x_4;
|
||||
x_11 = lean_apply_2(x_8, lean_box(0), x_10);
|
||||
return x_11;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
|
||||
x_12 = lean_array_fget(x_4, x_3);
|
||||
x_13 = lean_box(0);
|
||||
lean_inc(x_12);
|
||||
x_14 = x_13;
|
||||
x_15 = lean_array_fset(x_4, x_3, x_14);
|
||||
x_16 = lean_ctor_get(x_1, 1);
|
||||
lean_inc(x_16);
|
||||
lean_inc(x_12);
|
||||
lean_inc(x_2);
|
||||
lean_inc(x_1);
|
||||
x_17 = l_Lean_Syntax_mreplace___main___rarg(x_1, x_2, x_12);
|
||||
x_18 = lean_alloc_closure((void*)(l_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1___rarg___lambda__1___boxed), 6, 5);
|
||||
lean_closure_set(x_18, 0, x_3);
|
||||
lean_closure_set(x_18, 1, x_12);
|
||||
lean_closure_set(x_18, 2, x_15);
|
||||
lean_closure_set(x_18, 3, x_1);
|
||||
lean_closure_set(x_18, 4, x_2);
|
||||
x_19 = lean_apply_4(x_16, lean_box(0), lean_box(0), x_17, x_18);
|
||||
return x_19;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_alloc_closure((void*)(l_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1___rarg), 4, 0);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -1796,7 +1723,15 @@ return x_10;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Lean_Syntax_mreplace___main___rarg(x_1, x_2, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
|
||||
|
|
@ -1813,39 +1748,43 @@ x_7 = lean_apply_2(x_5, lean_box(0), x_6);
|
|||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__3(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_Lean_Syntax_mreplace___main___rarg___lambda__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
|
||||
_start:
|
||||
{
|
||||
if (lean_obj_tag(x_6) == 0)
|
||||
{
|
||||
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
x_7 = lean_unsigned_to_nat(0u);
|
||||
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
|
||||
lean_inc(x_1);
|
||||
x_8 = l_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1___rarg(x_1, x_2, x_7, x_3);
|
||||
x_9 = lean_alloc_closure((void*)(l_Lean_Syntax_mreplace___main___rarg___lambda__2), 3, 2);
|
||||
lean_closure_set(x_9, 0, x_1);
|
||||
lean_closure_set(x_9, 1, x_4);
|
||||
x_10 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_8, x_9);
|
||||
return x_10;
|
||||
x_7 = lean_alloc_closure((void*)(l_Lean_Syntax_mreplace___main___rarg___lambda__2___boxed), 4, 2);
|
||||
lean_closure_set(x_7, 0, x_1);
|
||||
lean_closure_set(x_7, 1, x_2);
|
||||
x_8 = lean_unsigned_to_nat(0u);
|
||||
lean_inc(x_1);
|
||||
x_9 = l_Array_umapMAux___main___rarg(x_1, lean_box(0), x_7, x_8, x_3);
|
||||
x_10 = lean_alloc_closure((void*)(l_Lean_Syntax_mreplace___main___rarg___lambda__3), 3, 2);
|
||||
lean_closure_set(x_10, 0, x_1);
|
||||
lean_closure_set(x_10, 1, x_4);
|
||||
x_11 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_9, x_10);
|
||||
return x_11;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
|
||||
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
x_11 = lean_ctor_get(x_6, 0);
|
||||
lean_inc(x_11);
|
||||
lean_dec(x_6);
|
||||
x_12 = lean_ctor_get(x_1, 0);
|
||||
x_12 = lean_ctor_get(x_6, 0);
|
||||
lean_inc(x_12);
|
||||
lean_dec(x_1);
|
||||
x_13 = lean_ctor_get(x_12, 1);
|
||||
lean_dec(x_6);
|
||||
x_13 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_13);
|
||||
lean_dec(x_12);
|
||||
x_14 = lean_apply_2(x_13, lean_box(0), x_11);
|
||||
return x_14;
|
||||
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_12);
|
||||
return x_15;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1865,7 +1804,7 @@ lean_inc(x_12);
|
|||
lean_inc(x_2);
|
||||
x_13 = lean_apply_1(x_2, x_3);
|
||||
lean_inc(x_12);
|
||||
x_14 = lean_alloc_closure((void*)(l_Lean_Syntax_mreplace___main___rarg___lambda__3), 6, 5);
|
||||
x_14 = lean_alloc_closure((void*)(l_Lean_Syntax_mreplace___main___rarg___lambda__4), 6, 5);
|
||||
lean_closure_set(x_14, 0, x_1);
|
||||
lean_closure_set(x_14, 1, x_2);
|
||||
lean_closure_set(x_14, 2, x_11);
|
||||
|
|
@ -1905,22 +1844,13 @@ x_3 = lean_alloc_closure((void*)(l_Lean_Syntax_mreplace___main___rarg), 3, 0);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1___rarg___lambda__1___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_Lean_Syntax_mreplace___main___rarg___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = l_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1___rarg___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean_dec(x_1);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Array_umapMAux___main___at_Lean_Syntax_mreplace___main___spec__1(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
return x_3;
|
||||
lean_object* x_5;
|
||||
x_5 = l_Lean_Syntax_mreplace___main___rarg___lambda__2(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_3);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_mreplace___main___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
|
|
@ -1957,75 +1887,15 @@ lean_dec(x_2);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___rarg___lambda__1(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_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
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_add(x_1, x_7);
|
||||
x_9 = x_6;
|
||||
x_10 = lean_array_fset(x_3, x_1, x_9);
|
||||
x_11 = l_Array_umapMAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___rarg(x_4, x_5, x_8, x_10);
|
||||
return x_11;
|
||||
lean_object* x_5;
|
||||
x_5 = l_Lean_Syntax_mrewriteBottomUp___main___rarg(x_1, x_2, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___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_array_get_size(x_4);
|
||||
x_6 = lean_nat_dec_lt(x_3, x_5);
|
||||
lean_dec(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_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
x_7 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_7);
|
||||
lean_dec(x_1);
|
||||
x_8 = lean_ctor_get(x_7, 1);
|
||||
lean_inc(x_8);
|
||||
lean_dec(x_7);
|
||||
x_9 = l_Array_empty___closed__1;
|
||||
x_10 = x_4;
|
||||
x_11 = lean_apply_2(x_8, lean_box(0), x_10);
|
||||
return x_11;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
|
||||
x_12 = lean_array_fget(x_4, x_3);
|
||||
x_13 = lean_box(0);
|
||||
lean_inc(x_12);
|
||||
x_14 = x_13;
|
||||
x_15 = lean_array_fset(x_4, x_3, x_14);
|
||||
x_16 = lean_ctor_get(x_1, 1);
|
||||
lean_inc(x_16);
|
||||
lean_inc(x_12);
|
||||
lean_inc(x_2);
|
||||
lean_inc(x_1);
|
||||
x_17 = l_Lean_Syntax_mrewriteBottomUp___main___rarg(x_1, x_2, x_12);
|
||||
x_18 = lean_alloc_closure((void*)(l_Array_umapMAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___rarg___lambda__1___boxed), 6, 5);
|
||||
lean_closure_set(x_18, 0, x_3);
|
||||
lean_closure_set(x_18, 1, x_12);
|
||||
lean_closure_set(x_18, 2, x_15);
|
||||
lean_closure_set(x_18, 3, x_1);
|
||||
lean_closure_set(x_18, 4, x_2);
|
||||
x_19 = lean_apply_4(x_16, lean_box(0), lean_box(0), x_17, x_18);
|
||||
return x_19;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_alloc_closure((void*)(l_Array_umapMAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___rarg), 4, 0);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5;
|
||||
|
|
@ -2041,7 +1911,7 @@ _start:
|
|||
{
|
||||
if (lean_obj_tag(x_3) == 1)
|
||||
{
|
||||
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_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;
|
||||
x_4 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_4);
|
||||
x_5 = lean_ctor_get(x_3, 1);
|
||||
|
|
@ -2049,21 +1919,25 @@ lean_inc(x_5);
|
|||
lean_dec(x_3);
|
||||
x_6 = lean_ctor_get(x_1, 1);
|
||||
lean_inc(x_6);
|
||||
x_7 = lean_unsigned_to_nat(0u);
|
||||
lean_inc(x_2);
|
||||
x_8 = l_Array_umapMAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___rarg(x_1, x_2, x_7, x_5);
|
||||
x_9 = lean_alloc_closure((void*)(l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__1), 3, 2);
|
||||
lean_closure_set(x_9, 0, x_4);
|
||||
lean_closure_set(x_9, 1, x_2);
|
||||
x_10 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_8, x_9);
|
||||
return x_10;
|
||||
lean_inc(x_1);
|
||||
x_7 = lean_alloc_closure((void*)(l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__1___boxed), 4, 2);
|
||||
lean_closure_set(x_7, 0, x_1);
|
||||
lean_closure_set(x_7, 1, x_2);
|
||||
x_8 = lean_unsigned_to_nat(0u);
|
||||
x_9 = l_Array_umapMAux___main___rarg(x_1, lean_box(0), x_7, x_8, x_5);
|
||||
x_10 = lean_alloc_closure((void*)(l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__2), 3, 2);
|
||||
lean_closure_set(x_10, 0, x_4);
|
||||
lean_closure_set(x_10, 1, x_2);
|
||||
x_11 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_9, x_10);
|
||||
return x_11;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_11;
|
||||
lean_object* x_12;
|
||||
lean_dec(x_1);
|
||||
x_11 = lean_apply_1(x_2, x_3);
|
||||
return x_11;
|
||||
x_12 = lean_apply_1(x_2, x_3);
|
||||
return x_12;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -2075,22 +1949,13 @@ x_3 = lean_alloc_closure((void*)(l_Lean_Syntax_mrewriteBottomUp___main___rarg),
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___rarg___lambda__1___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_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_7;
|
||||
x_7 = l_Array_umapMAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___rarg___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6);
|
||||
lean_dec(x_1);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_umapMAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Array_umapMAux___main___at_Lean_Syntax_mrewriteBottomUp___main___spec__1(x_1, x_2);
|
||||
lean_dec(x_2);
|
||||
return x_3;
|
||||
lean_object* x_5;
|
||||
x_5 = l_Lean_Syntax_mrewriteBottomUp___main___rarg___lambda__1(x_1, x_2, x_3, x_4);
|
||||
lean_dec(x_3);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_mrewriteBottomUp___main___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
|
|
|
|||
4
stage0/library/Init/Lean/TypeClass/Context.c
generated
4
stage0/library/Init/Lean/TypeClass/Context.c
generated
|
|
@ -67,7 +67,6 @@ lean_object* l_Lean_TypeClass_Context_uNewMeta(lean_object*);
|
|||
lean_object* l_Lean_TypeClass_Context_uUnify___main___closed__3;
|
||||
lean_object* l_Lean_TypeClass_Context_eAssign(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_TypeClass_Context__u03b1Norm___closed__5;
|
||||
extern lean_object* l_panicWithPos___at___private_Init_Lean_MetavarContext_5__instantiateDelayedAux___main___spec__1___closed__1;
|
||||
lean_object* l_Lean_Expr_getAppNumArgsAux___main(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Options_empty;
|
||||
lean_object* l_RBNode_fold___main___at_RBMap_size___spec__1___rarg(lean_object*, lean_object*);
|
||||
|
|
@ -131,6 +130,7 @@ lean_object* l_Lean_TypeClass_Context_eMetaIdx___boxed(lean_object*);
|
|||
lean_object* l_Lean_TypeClass_Context_eAssignIdx___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_name_mk_string(lean_object*, lean_object*);
|
||||
uint8_t l_List_foldr___main___at_Lean_TypeClass_Context_eHasTmpMVar___spec__1(uint8_t, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_MetavarContext_5__instantiateDelayedAux___main___closed__1;
|
||||
lean_object* l_PersistentArray_getAux___main___at_Lean_TypeClass_Context_eInferIdx___spec__2___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_nat_add(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_TypeClass_Context_slowWhnfApp___main___boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -851,7 +851,7 @@ lean_object* _init_l_panicWithPos___at_Lean_TypeClass_Context_eAssign___spec__1_
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_panicWithPos___at___private_Init_Lean_MetavarContext_5__instantiateDelayedAux___main___spec__1___closed__1;
|
||||
x_1 = l___private_Init_Lean_MetavarContext_5__instantiateDelayedAux___main___closed__1;
|
||||
x_2 = l_PUnit_Inhabited;
|
||||
x_3 = l_monadInhabited___rarg(x_1, x_2);
|
||||
return x_3;
|
||||
|
|
|
|||
10008
stage0/library/Init/Lean/WHNF.c
generated
10008
stage0/library/Init/Lean/WHNF.c
generated
File diff suppressed because it is too large
Load diff
Loading…
Add table
Reference in a new issue