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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-16 12:14:34 -08:00
parent a3ccbe66cf
commit 2bf69c539e
25 changed files with 17200 additions and 24796 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

97
stage0/library/Init/Data/Hashable.c generated
View file

@ -15,20 +15,28 @@ extern "C" {
#endif
lean_object* l_Option_Hashable(lean_object*);
lean_object* l_String_Hashable___closed__1;
lean_object* l_List_hash___rarg___boxed(lean_object*, lean_object*);
lean_object* l_String_Hashable;
size_t l_Nat_hash(lean_object*);
lean_object* l_Prod_Hashable___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_List_Hashable___rarg(lean_object*);
lean_object* l_List_foldl___main___at_List_hash___spec__1(lean_object*);
lean_object* l_List_hash(lean_object*);
size_t l_Prod_Hashable___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Option_hash(lean_object*);
size_t l_Option_hash___rarg(lean_object*, lean_object*);
size_t lean_string_hash(lean_object*);
lean_object* l_String_hash___boxed(lean_object*);
lean_object* l_Nat_Hashable;
size_t l_List_foldl___main___at_List_hash___spec__1___rarg(lean_object*, size_t, lean_object*);
lean_object* l_List_Hashable(lean_object*);
lean_object* l_Prod_Hashable(lean_object*, lean_object*);
lean_object* l_mixHash___boxed(lean_object*, lean_object*);
lean_object* l_List_foldl___main___at_List_hash___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Option_hash___rarg___boxed(lean_object*, lean_object*);
size_t lean_usize_mix_hash(size_t, size_t);
size_t lean_usize_of_nat(lean_object*);
size_t l_List_hash___rarg(lean_object*, lean_object*);
lean_object* l_Nat_hash___boxed(lean_object*);
lean_object* l_Option_Hashable___rarg(lean_object*);
lean_object* l_Nat_Hashable___closed__1;
@ -199,6 +207,95 @@ x_2 = lean_alloc_closure((void*)(l_Option_Hashable___rarg), 1, 0);
return x_2;
}
}
size_t l_List_foldl___main___at_List_hash___spec__1___rarg(lean_object* x_1, size_t x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_3) == 0)
{
lean_dec(x_1);
return x_2;
}
else
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; size_t x_7; size_t x_8;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_ctor_get(x_3, 1);
lean_inc(x_5);
lean_dec(x_3);
lean_inc(x_1);
x_6 = lean_apply_1(x_1, x_4);
x_7 = lean_unbox_usize(x_6);
lean_dec(x_6);
x_8 = lean_usize_mix_hash(x_2, x_7);
x_2 = x_8;
x_3 = x_5;
goto _start;
}
}
}
lean_object* l_List_foldl___main___at_List_hash___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_List_foldl___main___at_List_hash___spec__1___rarg___boxed), 3, 0);
return x_2;
}
}
size_t l_List_hash___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
size_t x_3; size_t x_4;
x_3 = 7;
x_4 = l_List_foldl___main___at_List_hash___spec__1___rarg(x_1, x_3, x_2);
return x_4;
}
}
lean_object* l_List_hash(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_List_hash___rarg___boxed), 2, 0);
return x_2;
}
}
lean_object* l_List_foldl___main___at_List_hash___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
size_t x_4; size_t x_5; lean_object* x_6;
x_4 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_5 = l_List_foldl___main___at_List_hash___spec__1___rarg(x_1, x_4, x_3);
x_6 = lean_box_usize(x_5);
return x_6;
}
}
lean_object* l_List_hash___rarg___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
size_t x_3; lean_object* x_4;
x_3 = l_List_hash___rarg(x_1, x_2);
x_4 = lean_box_usize(x_3);
return x_4;
}
}
lean_object* l_List_Hashable___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_List_hash___rarg___boxed), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_List_Hashable(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_List_Hashable___rarg), 1, 0);
return x_2;
}
}
lean_object* initialize_Init_Data_UInt(lean_object*);
lean_object* initialize_Init_Data_String_Default(lean_object*);
static bool _G_initialized = false;

20
stage0/library/Init/Lean/Compiler/ClosedTermCache.c generated
View file

@ -29,7 +29,7 @@ lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_getClosedTermName___
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__2;
lean_object* lean_mk_array(lean_object*, lean_object*);
lean_object* l_Lean_closedTermCacheExt___elambda__2(lean_object*);
size_t lean_expr_hash(lean_object*);
size_t l_Lean_Expr_hash(lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_mkClosedTermCacheExtension___spec__17(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_closedTermCacheExt___elambda__4___boxed(lean_object*);
lean_object* lean_cache_closed_term_name(lean_object*, lean_object*, lean_object*);
@ -256,7 +256,7 @@ else
lean_object* x_9; lean_object* x_10; size_t x_11; size_t x_12; size_t x_13; size_t x_14; size_t x_15; size_t x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_9 = lean_array_fget(x_4, x_5);
x_10 = lean_array_fget(x_3, x_5);
x_11 = lean_expr_hash(x_9);
x_11 = l_Lean_Expr_hash(x_9);
x_12 = 1;
x_13 = x_1 - x_12;
x_14 = 5;
@ -595,7 +595,7 @@ if (x_4 == 0)
lean_object* x_5; lean_object* x_6; size_t x_7; size_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_5 = lean_ctor_get(x_1, 0);
x_6 = lean_ctor_get(x_1, 1);
x_7 = lean_expr_hash(x_2);
x_7 = l_Lean_Expr_hash(x_2);
x_8 = 1;
x_9 = l_PersistentHashMap_insertAux___main___at_Lean_mkClosedTermCacheExtension___spec__3(x_5, x_7, x_8, x_2, x_3);
x_10 = lean_unsigned_to_nat(1u);
@ -613,7 +613,7 @@ x_13 = lean_ctor_get(x_1, 1);
lean_inc(x_13);
lean_inc(x_12);
lean_dec(x_1);
x_14 = lean_expr_hash(x_2);
x_14 = l_Lean_Expr_hash(x_2);
x_15 = 1;
x_16 = l_PersistentHashMap_insertAux___main___at_Lean_mkClosedTermCacheExtension___spec__3(x_12, x_14, x_15, x_2, x_3);
x_17 = lean_unsigned_to_nat(1u);
@ -672,7 +672,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; size_t x_7; size_t x_8; le
x_4 = lean_ctor_get(x_2, 0);
x_5 = lean_ctor_get(x_2, 2);
x_6 = lean_array_get_size(x_1);
x_7 = lean_expr_hash(x_4);
x_7 = l_Lean_Expr_hash(x_4);
x_8 = lean_usize_modn(x_7, x_6);
lean_dec(x_6);
x_9 = lean_array_uget(x_1, x_8);
@ -693,7 +693,7 @@ lean_inc(x_13);
lean_inc(x_12);
lean_dec(x_2);
x_15 = lean_array_get_size(x_1);
x_16 = lean_expr_hash(x_12);
x_16 = l_Lean_Expr_hash(x_12);
x_17 = lean_usize_modn(x_16, x_15);
lean_dec(x_15);
x_18 = lean_array_uget(x_1, x_17);
@ -840,7 +840,7 @@ lean_object* x_5; lean_object* x_6; lean_object* x_7; size_t x_8; size_t x_9; le
x_5 = lean_ctor_get(x_1, 0);
x_6 = lean_ctor_get(x_1, 1);
x_7 = lean_array_get_size(x_6);
x_8 = lean_expr_hash(x_2);
x_8 = l_Lean_Expr_hash(x_2);
x_9 = lean_usize_modn(x_8, x_7);
x_10 = lean_array_uget(x_6, x_9);
x_11 = l_AssocList_contains___main___at_Lean_mkClosedTermCacheExtension___spec__7(x_2, x_10);
@ -890,7 +890,7 @@ lean_inc(x_21);
lean_inc(x_20);
lean_dec(x_1);
x_22 = lean_array_get_size(x_21);
x_23 = lean_expr_hash(x_2);
x_23 = l_Lean_Expr_hash(x_2);
x_24 = lean_usize_modn(x_23, x_22);
x_25 = lean_array_uget(x_21, x_24);
x_26 = l_AssocList_contains___main___at_Lean_mkClosedTermCacheExtension___spec__7(x_2, x_25);
@ -2428,7 +2428,7 @@ _start:
{
lean_object* x_3; size_t x_4; lean_object* x_5;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_expr_hash(x_2);
x_4 = l_Lean_Expr_hash(x_2);
x_5 = l_PersistentHashMap_findAux___main___at_Lean_getClosedTermName___spec__3(x_3, x_4, x_2);
return x_5;
}
@ -2471,7 +2471,7 @@ _start:
lean_object* x_3; lean_object* x_4; size_t x_5; size_t x_6; lean_object* x_7; lean_object* x_8;
x_3 = lean_ctor_get(x_1, 1);
x_4 = lean_array_get_size(x_3);
x_5 = lean_expr_hash(x_2);
x_5 = l_Lean_Expr_hash(x_2);
x_6 = lean_usize_modn(x_5, x_4);
lean_dec(x_4);
x_7 = lean_array_uget(x_3, x_6);

20
stage0/library/Init/Lean/Compiler/ConstFolding.c generated
View file

@ -56,6 +56,7 @@ lean_object* l_Lean_Compiler_getNumLit___main(lean_object*);
lean_object* l_Lean_Compiler_getBoolLit___closed__2;
lean_object* l_Lean_Compiler_numScalarTypes___closed__5;
lean_object* l_Lean_Compiler_mkNatLe___closed__4;
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_unFoldFns___closed__7;
lean_object* l_Lean_Compiler_natFoldFns___closed__12;
extern lean_object* l_Nat_HasMod___closed__1;
@ -69,7 +70,6 @@ lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__1;
lean_object* l_Lean_Compiler_foldStrictOr(uint8_t);
lean_object* l_Lean_Compiler_foldUIntSub___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_unFoldFns___closed__3;
lean_object* lean_expr_mk_app(lean_object*, lean_object*);
uint8_t l_Lean_Compiler_isToNat(lean_object*);
lean_object* l_Lean_Compiler_foldNatDecLe___closed__2;
lean_object* l_Lean_Compiler_foldBinUInt(lean_object*, uint8_t, lean_object*, lean_object*);
@ -94,6 +94,7 @@ lean_object* l_Lean_Compiler_numScalarTypes___closed__21;
lean_object* l_Lean_Compiler_boolFoldFns___closed__2;
lean_object* l_Lean_Compiler_natFoldFns___closed__39;
lean_object* l_Lean_Compiler_natFoldFns___closed__31;
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_getBoolLit___closed__3;
lean_object* l_Lean_Compiler_foldUIntAdd___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_List_foldl___main___at_Lean_Compiler_uintBinFoldFns___spec__2(lean_object*, lean_object*);
@ -123,7 +124,6 @@ lean_object* l_Lean_Compiler_natFoldFns___closed__16;
lean_object* l_Lean_Compiler_foldUIntDiv___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_natFoldFns___closed__7;
lean_object* l_Lean_Compiler_foldBinOp___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_mk_const(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_getBoolLit___closed__4;
extern lean_object* l_Lean_Level_one;
lean_object* l_List_foldr___main___at_Lean_Compiler_isOfNat___spec__1___boxed(lean_object*, lean_object*, lean_object*);
@ -998,14 +998,14 @@ lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_obj
x_3 = lean_ctor_get(x_1, 2);
lean_inc(x_3);
x_4 = lean_box(0);
x_5 = lean_expr_mk_const(x_3, x_4);
x_5 = l_Lean_mkConst(x_3, x_4);
x_6 = lean_ctor_get(x_1, 4);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_nat_mod(x_2, x_6);
lean_dec(x_6);
x_8 = l_Lean_mkNatLit(x_7);
x_9 = lean_expr_mk_app(x_5, x_8);
x_9 = l_Lean_mkApp(x_5, x_8);
return x_9;
}
}
@ -2068,7 +2068,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_mkNatEq___closed__2;
x_2 = l_Lean_Compiler_mkNatEq___closed__3;
x_3 = lean_expr_mk_const(x_1, x_2);
x_3 = l_Lean_mkConst(x_1, x_2);
return x_3;
}
}
@ -2078,7 +2078,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Literal_type___closed__2;
x_3 = lean_expr_mk_const(x_2, x_1);
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
@ -2169,7 +2169,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_mkNatLt___closed__4;
x_2 = l_Lean_Compiler_mkNatLt___closed__5;
x_3 = lean_expr_mk_const(x_1, x_2);
x_3 = l_Lean_mkConst(x_1, x_2);
return x_3;
}
}
@ -2189,7 +2189,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Compiler_mkNatLt___closed__7;
x_3 = lean_expr_mk_const(x_2, x_1);
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
@ -2251,7 +2251,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_mkNatLe___closed__2;
x_2 = l_Lean_Compiler_mkNatLt___closed__5;
x_3 = lean_expr_mk_const(x_1, x_2);
x_3 = l_Lean_mkConst(x_1, x_2);
return x_3;
}
}
@ -2279,7 +2279,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Compiler_mkNatLe___closed__5;
x_3 = lean_expr_mk_const(x_2, x_1);
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}

20
stage0/library/Init/Lean/Compiler/Specialize.c generated
View file

@ -37,7 +37,7 @@ lean_object* l_Lean_registerEnumAttributes___at_Lean_Compiler_mkSpecializeAttrs_
lean_object* lean_mk_array(lean_object*, lean_object*);
lean_object* l_Lean_registerEnumAttributes___at_Lean_Compiler_mkSpecializeAttrs___spec__1___closed__1;
lean_object* l_Array_iterateMAux___main___at_Lean_Compiler_mkSpecExtension___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_expr_hash(lean_object*);
size_t l_Lean_Expr_hash(lean_object*);
lean_object* l_HashMapImp_find___at_Lean_Compiler_getCachedSpecialization___spec__5(lean_object*, lean_object*);
extern lean_object* l_Lean_EnvExtension_Inhabited___rarg___closed__1;
lean_object* l_Lean_Compiler_SpecState_Inhabited___closed__2;
@ -3366,7 +3366,7 @@ else
lean_object* x_9; lean_object* x_10; size_t x_11; size_t x_12; size_t x_13; size_t x_14; size_t x_15; size_t x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_9 = lean_array_fget(x_4, x_5);
x_10 = lean_array_fget(x_3, x_5);
x_11 = lean_expr_hash(x_9);
x_11 = l_Lean_Expr_hash(x_9);
x_12 = 1;
x_13 = x_1 - x_12;
x_14 = 5;
@ -3705,7 +3705,7 @@ if (x_4 == 0)
lean_object* x_5; lean_object* x_6; size_t x_7; size_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_5 = lean_ctor_get(x_1, 0);
x_6 = lean_ctor_get(x_1, 1);
x_7 = lean_expr_hash(x_2);
x_7 = l_Lean_Expr_hash(x_2);
x_8 = 1;
x_9 = l_PersistentHashMap_insertAux___main___at_Lean_Compiler_SpecState_addEntry___spec__14(x_5, x_7, x_8, x_2, x_3);
x_10 = lean_unsigned_to_nat(1u);
@ -3723,7 +3723,7 @@ x_13 = lean_ctor_get(x_1, 1);
lean_inc(x_13);
lean_inc(x_12);
lean_dec(x_1);
x_14 = lean_expr_hash(x_2);
x_14 = l_Lean_Expr_hash(x_2);
x_15 = 1;
x_16 = l_PersistentHashMap_insertAux___main___at_Lean_Compiler_SpecState_addEntry___spec__14(x_12, x_14, x_15, x_2, x_3);
x_17 = lean_unsigned_to_nat(1u);
@ -3782,7 +3782,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; size_t x_7; size_t x_8; le
x_4 = lean_ctor_get(x_2, 0);
x_5 = lean_ctor_get(x_2, 2);
x_6 = lean_array_get_size(x_1);
x_7 = lean_expr_hash(x_4);
x_7 = l_Lean_Expr_hash(x_4);
x_8 = lean_usize_modn(x_7, x_6);
lean_dec(x_6);
x_9 = lean_array_uget(x_1, x_8);
@ -3803,7 +3803,7 @@ lean_inc(x_13);
lean_inc(x_12);
lean_dec(x_2);
x_15 = lean_array_get_size(x_1);
x_16 = lean_expr_hash(x_12);
x_16 = l_Lean_Expr_hash(x_12);
x_17 = lean_usize_modn(x_16, x_15);
lean_dec(x_15);
x_18 = lean_array_uget(x_1, x_17);
@ -3950,7 +3950,7 @@ lean_object* x_5; lean_object* x_6; lean_object* x_7; size_t x_8; size_t x_9; le
x_5 = lean_ctor_get(x_1, 0);
x_6 = lean_ctor_get(x_1, 1);
x_7 = lean_array_get_size(x_6);
x_8 = lean_expr_hash(x_2);
x_8 = l_Lean_Expr_hash(x_2);
x_9 = lean_usize_modn(x_8, x_7);
x_10 = lean_array_uget(x_6, x_9);
x_11 = l_AssocList_contains___main___at_Lean_Compiler_SpecState_addEntry___spec__18(x_2, x_10);
@ -4000,7 +4000,7 @@ lean_inc(x_21);
lean_inc(x_20);
lean_dec(x_1);
x_22 = lean_array_get_size(x_21);
x_23 = lean_expr_hash(x_2);
x_23 = l_Lean_Expr_hash(x_2);
x_24 = lean_usize_modn(x_23, x_22);
x_25 = lean_array_uget(x_21, x_24);
x_26 = l_AssocList_contains___main___at_Lean_Compiler_SpecState_addEntry___spec__18(x_2, x_25);
@ -5912,7 +5912,7 @@ _start:
{
lean_object* x_3; size_t x_4; lean_object* x_5;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_expr_hash(x_2);
x_4 = l_Lean_Expr_hash(x_2);
x_5 = l_PersistentHashMap_findAux___main___at_Lean_Compiler_getCachedSpecialization___spec__3(x_3, x_4, x_2);
return x_5;
}
@ -5955,7 +5955,7 @@ _start:
lean_object* x_3; lean_object* x_4; size_t x_5; size_t x_6; lean_object* x_7; lean_object* x_8;
x_3 = lean_ctor_get(x_1, 1);
x_4 = lean_array_get_size(x_3);
x_5 = lean_expr_hash(x_2);
x_5 = l_Lean_Expr_hash(x_2);
x_6 = lean_usize_modn(x_5, x_4);
lean_dec(x_4);
x_7 = lean_array_uget(x_3, x_6);

16
stage0/library/Init/Lean/Compiler/Util.c generated
View file

@ -15,15 +15,16 @@ extern "C" {
#endif
uint8_t lean_name_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_atMostOnce_HasAndthen;
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_atMostOnce_seq(lean_object*, lean_object*, lean_object*);
uint8_t l_String_isPrefixOf(lean_object*, lean_object*);
lean_object* l_List_map___main___at___private_Init_Lean_Compiler_Util_1__getDeclNamesForCodeGen___spec__1(lean_object*);
lean_object* l_Lean_Compiler_mkLcProof___closed__3;
lean_object* lean_expr_mk_app(lean_object*, lean_object*);
uint8_t lean_at_most_once(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_atMostOnce_HasAndthen___closed__1;
lean_object* l_Lean_Compiler_atMostOnce_visit___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_unreachableExpr___closed__2;
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
uint8_t l_Lean_Compiler_isEagerLambdaLiftingName___main(lean_object*);
lean_object* l_Lean_Compiler_atMostOnce_visit___main___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_checkIsDefinition___closed__3;
@ -31,7 +32,6 @@ lean_object* l_Lean_Compiler_mkLcProof(lean_object*);
lean_object* l_Lean_Compiler_objectType___closed__3;
lean_object* l_Nat_repr(lean_object*);
lean_object* l_Lean_Compiler_neutralExpr___closed__1;
lean_object* lean_expr_mk_const(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_objectType;
lean_object* l_Lean_Compiler_neutralExpr___closed__3;
lean_object* lean_string_append(lean_object*, lean_object*);
@ -94,7 +94,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Compiler_neutralExpr___closed__2;
x_3 = lean_expr_mk_const(x_2, x_1);
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
@ -130,7 +130,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Compiler_unreachableExpr___closed__2;
x_3 = lean_expr_mk_const(x_2, x_1);
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
@ -166,7 +166,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Compiler_objectType___closed__2;
x_3 = lean_expr_mk_const(x_2, x_1);
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
@ -202,7 +202,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Compiler_voidType___closed__2;
x_3 = lean_expr_mk_const(x_2, x_1);
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
@ -238,7 +238,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Compiler_mkLcProof___closed__2;
x_3 = lean_expr_mk_const(x_2, x_1);
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
@ -247,7 +247,7 @@ _start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Compiler_mkLcProof___closed__3;
x_3 = lean_expr_mk_app(x_2, x_1);
x_3 = l_Lean_mkApp(x_2, x_1);
return x_3;
}
}

4
stage0/library/Init/Lean/Declaration.c generated
View file

@ -28,6 +28,7 @@ lean_object* l_Lean_InductiveVal_nctors___boxed(lean_object*);
lean_object* l_Lean_ConstantInfo_lparams(lean_object*);
lean_object* l_Lean_ConstantInfo_isCtor___boxed(lean_object*);
uint8_t l_Lean_ConstantInfo_hasValue(lean_object*);
extern lean_object* l_Lean_Expr_Inhabited;
lean_object* l_Lean_Name_getPrefix(lean_object*);
uint8_t l_Lean_ConstantInfo_isCtor(lean_object*);
lean_object* lean_instantiate_value_lparams(lean_object*, lean_object*);
@ -40,7 +41,6 @@ lean_object* l_Lean_InductiveVal_nctors(lean_object*);
lean_object* l___private_Init_Util_1__mkPanicMessage(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_RecursorVal_getMajorIdx(lean_object*);
lean_object* l_Lean_ConstantInfo_value_x3f___boxed(lean_object*);
extern lean_object* l_Lean_Expr_inhabited;
lean_object* l_Lean_ConstantInfo_hints(lean_object*);
lean_object* l_Lean_ConstantInfo_value_x21___closed__1;
lean_object* l_Lean_ConstantInfo_toConstantVal___boxed(lean_object*);
@ -321,7 +321,7 @@ return x_6;
default:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = l_Lean_Expr_inhabited;
x_7 = l_Lean_Expr_Inhabited;
x_8 = l_Lean_ConstantInfo_value_x21___closed__3;
x_9 = lean_panic_fn(x_8);
return x_9;

10
stage0/library/Init/Lean/Elaborator/Basic.c generated
View file

@ -145,6 +145,7 @@ lean_object* lean_io_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentHashMap_empty___at_Lean_mkBuiltinTermElabTable___spec__3;
lean_object* l_Lean_Elab_runElab___at_Lean_Elab_processCommand___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_processHeaderAux___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_Elab_updateCmdPos___boxed(lean_object*);
extern lean_object* l_Lean_Options_empty;
lean_object* l_Lean_Elab_anonymousInstNamePrefix;
@ -161,7 +162,6 @@ lean_object* l_Lean_Elab_getEnv___boxed(lean_object*);
lean_object* l_Lean_Elab_getScope(lean_object*);
lean_object* l_PersistentHashMap_containsAtAux___main___at_Lean_addBuiltinTermElab___spec__6___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentHashMap_contains___at_Lean_addBuiltinCommandElab___spec__4___boxed(lean_object*, lean_object*);
lean_object* lean_expr_mk_fvar(lean_object*);
lean_object* lean_local_ctx_mk_local_decl(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* lean_mk_empty_environment(uint32_t, lean_object*);
lean_object* l_Lean_commandElabAttribute___closed__1;
@ -196,7 +196,6 @@ lean_object* l_Lean_Elab_modifyScope___at_Lean_Elab_withInPattern___spec__1(lean
lean_object* l_Lean_Elab_mkMessage___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkBuiltinCommandElabTable(lean_object*);
lean_object* l_Lean_Elab_updateCmdPos(lean_object*);
lean_object* lean_expr_mk_const(lean_object*, lean_object*);
extern lean_object* l_Lean_NameGenerator_Inhabited___closed__3;
lean_object* l_Lean_Elab_getNamespace(lean_object*);
lean_object* l_Lean_Elab_logErrorAt___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -242,6 +241,7 @@ lean_object* l_Lean_addBuiltinTermElab___closed__1;
lean_object* l_Lean_Syntax_getId___rarg(lean_object*);
lean_object* l_Lean_OpenDecl_HasToString___closed__1;
lean_object* l_Lean_addBuiltinTermElab(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkFVar(lean_object*);
lean_object* l_Lean_registerBuiltinCommandElabAttr___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* l_System_FilePath_dirName(lean_object*);
lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
@ -3793,7 +3793,7 @@ x_9 = l_Lean_nameToExprAux___main(x_3);
lean_inc(x_4);
x_10 = l_Lean_nameToExprAux___main(x_4);
lean_inc(x_4);
x_11 = lean_expr_mk_const(x_4, x_8);
x_11 = l_Lean_mkConst(x_4, x_8);
x_12 = l_Lean_Parser_declareBuiltinParser___closed__6;
x_13 = lean_array_push(x_12, x_9);
x_14 = lean_array_push(x_13, x_10);
@ -11118,7 +11118,7 @@ if (x_10 == 0)
lean_object* x_11; lean_object* x_12;
x_11 = lean_ctor_get(x_9, 0);
lean_dec(x_11);
x_12 = lean_expr_mk_fvar(x_7);
x_12 = l_Lean_mkFVar(x_7);
lean_ctor_set(x_9, 0, x_12);
return x_9;
}
@ -11128,7 +11128,7 @@ lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_13 = lean_ctor_get(x_9, 1);
lean_inc(x_13);
lean_dec(x_9);
x_14 = lean_expr_mk_fvar(x_7);
x_14 = l_Lean_mkFVar(x_7);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_13);

102
stage0/library/Init/Lean/Elaborator/PreTerm.c generated
View file

@ -17,7 +17,6 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_convertId(lean_object*);
extern lean_object* l_Lean_Parser_Level_num___elambda__1___rarg___closed__2;
lean_object* l_Lean_mkPreTypeAscription___closed__3;
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elaborator_PreTerm_4__processBinder___spec__1___closed__2;
lean_object* lean_expr_mk_mdata(lean_object*, lean_object*);
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addBuiltinPreTermElab(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_convertSorry___closed__1;
@ -28,9 +27,7 @@ lean_object* l_Lean_registerBuiltinPreTermElabAttr___closed__3;
lean_object* l_Lean_registerBuiltinPreTermElabAttr___closed__5;
uint8_t lean_name_dec_eq(lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elaborator_PreTerm_4__processBinder___spec__1___closed__6;
lean_object* l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__1;
lean_object* lean_local_ctx_find_from_user_name(lean_object*, lean_object*);
lean_object* lean_expr_mk_sort(lean_object*);
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elaborator_PreTerm_4__processBinder___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind___rarg(lean_object*);
lean_object* l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1(lean_object*, lean_object*);
@ -44,6 +41,7 @@ lean_object* lean_mk_array(lean_object*, lean_object*);
lean_object* l_IO_println___at_HasRepr_HasEval___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_builtinPreTermElabTable;
lean_object* l_Lean_Elab_convertType___rarg(lean_object*);
lean_object* l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___boxed(lean_object*);
lean_object* l___private_Init_Lean_Elaborator_PreTerm_1__setPos___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_toLevel___main___closed__4;
lean_object* l_Lean_Elab_mkForall(lean_object*, lean_object*, lean_object*, lean_object*);
@ -55,6 +53,7 @@ extern lean_object* l_Lean_AttributeImpl_inhabited___closed__5;
lean_object* l___private_Init_Lean_Elaborator_PreTerm_4__processBinder___closed__1;
lean_object* l___regBuiltinTermElab_Lean_Elab_convertHole___closed__3;
extern lean_object* l_Lean_Parser_Level_max___elambda__1___closed__1;
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
lean_object* l_HashMapImp_insert___at_Lean_addBuiltinPreTermElab___spec__3(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_addBuiltinTermElab___closed__2;
extern lean_object* l_Lean_Parser_Term_binderDefault___elambda__1___rarg___closed__1;
@ -72,7 +71,6 @@ lean_object* lean_level_mk_mvar(lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_convertSortApp___closed__1;
lean_object* l_Lean_registerBuiltinPreTermElabAttr___closed__7;
lean_object* l___regBuiltinTermElab_Lean_Elab_convertId___closed__3;
lean_object* lean_expr_mk_app(lean_object*, lean_object*);
lean_object* l_Lean_Elab_convertSort___boxed(lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_convertType___closed__5;
lean_object* l_Lean_mkPreTypeAscriptionIfSome(lean_object*, lean_object*);
@ -93,14 +91,15 @@ lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elaborator_PreTerm_5__processBinders___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_AssocList_contains___main___at_Lean_addBuiltinPreTermElab___spec__2(lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_convertProp___closed__1;
lean_object* l_Lean_mkMVar(lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_convertForall___closed__1;
extern lean_object* l_Lean_Parser_Term_sorry___elambda__1___rarg___closed__2;
lean_object* lean_io_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_registerBuiltinPreTermElabAttr___closed__4;
lean_object* l___regBuiltinTermElab_Lean_Elab_convertSortApp___closed__3;
extern lean_object* l_Lean_Options_empty;
lean_object* l_Lean_mkPreTypeAscription___closed__2;
lean_object* l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__3;
extern lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1___closed__2;
lean_object* l_Lean_Elab_toLevel___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_toPreTerm___closed__2;
@ -109,7 +108,6 @@ lean_object* l_Lean_declareBuiltinPreTermElab___closed__2;
lean_object* l___regBuiltinTermElab_Lean_Elab_convertType___closed__1;
lean_object* l_Lean_Level_ofNat___main(lean_object*);
lean_object* l_AssocList_find___main___at_Lean_Elab_toPreTerm___spec__2(lean_object*, lean_object*);
lean_object* lean_expr_mk_fvar(lean_object*);
lean_object* l_IO_Prim_Ref_get___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_convertType___closed__3;
lean_object* l___regBuiltinTermElab_Lean_Elab_convertSort___closed__2;
@ -127,7 +125,6 @@ lean_object* l___private_Init_Lean_Elaborator_PreTerm_1__setPos___closed__1;
lean_object* l_Lean_registerBuiltinPreTermElabAttr___closed__1;
lean_object* l_HashMapImp_find___at_Lean_Elab_toPreTerm___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_registerBuiltinPreTermElabAttr(lean_object*);
lean_object* lean_expr_mk_const(lean_object*, lean_object*);
lean_object* l_Lean_Elab_convertSort(lean_object*, lean_object*);
lean_object* l_Lean_mkAsPattern(lean_object*, lean_object*);
size_t lean_name_hash_usize(lean_object*);
@ -138,6 +135,7 @@ lean_object* lean_old_elaborate(lean_object*, lean_object*, lean_object*, lean_o
lean_object* l_Lean_Syntax_getArg___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_toLevel___main___closed__2;
extern lean_object* l_Lean_Parser_Term_prop___elambda__1___rarg___closed__2;
lean_object* l_Lean_mkSort(lean_object*);
lean_object* l_Lean_Elab_convertSortApp(lean_object*, lean_object*, lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_hole___elambda__1___rarg___closed__1;
@ -146,6 +144,7 @@ lean_object* l_Lean_KVMap_setName(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_sort___elambda__1___rarg___closed__2;
uint8_t l_Lean_Syntax_isOfKind___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_convertHole___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_Inhabited;
extern lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__2;
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elaborator_PreTerm_4__processBinder___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_type___elambda__1___rarg___closed__2;
@ -158,6 +157,7 @@ lean_object* l_Lean_mkPreTypeAscription(lean_object*, lean_object*);
extern lean_object* l_Lean_addBuiltinTermElab___closed__1;
lean_object* l___regBuiltinTermElab_Lean_Elab_convertType___closed__4;
lean_object* l_Lean_Syntax_getId___rarg(lean_object*);
lean_object* l_Lean_mkFVar(lean_object*);
lean_object* l_Lean_Elab_getUniverses___rarg(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elaborator_PreTerm_5__processBinders(lean_object*, lean_object*, lean_object*);
@ -166,11 +166,11 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_convertProp(lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_convertSorry___closed__2;
uint8_t l_HashMapImp_contains___at_Lean_addBuiltinPreTermElab___spec__1(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__2;
extern lean_object* l_Lean_Parser_Term_sortApp___elambda__1___closed__2;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__2;
lean_object* l_Lean_Elab_convertSort___rarg(lean_object*);
lean_object* l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal(lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_toLevel___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_instBinder___elambda__1___rarg___closed__2;
lean_object* l_List_head_x21___at_Lean_Elab_getScope___spec__1(lean_object*);
@ -194,13 +194,12 @@ uint8_t l_List_elem___main___at_Lean_Parser_addBuiltinLeadingParser___spec__4(le
lean_object* l_HashMapImp_expand___at_Lean_addBuiltinPreTermElab___spec__4(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_convertType(lean_object*);
extern lean_object* l_Lean_Expr_inhabited;
extern lean_object* l_Lean_Level_one___closed__1;
lean_object* l_AssocList_foldlM___main___at_Lean_addBuiltinPreTermElab___spec__6(lean_object*, lean_object*);
lean_object* l_Lean_mkAsIs___closed__2;
lean_object* l_HashMapImp_moveEntries___main___at_Lean_addBuiltinPreTermElab___spec__5(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__1;
lean_object* l_Lean_Elab_convertSorry___rarg___closed__2;
lean_object* lean_expr_mk_mvar(lean_object*);
lean_object* l_Lean_Elab_toPreTerm___closed__3;
lean_object* lean_level_mk_param(lean_object*);
extern lean_object* l_Lean_Parser_Term_app___elambda__1___closed__2;
@ -214,7 +213,7 @@ lean_object* l_Lean_Elab_toLevel___main___closed__1;
lean_object* lean_io_ref_get(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elaborator_PreTerm_4__processBinder(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_mkAnnotation___closed__1;
lean_object* l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__2;
lean_object* l_Lean_mkMData(lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elaborator_PreTerm_4__processBinder___spec__1___closed__1;
size_t lean_usize_modn(size_t, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_convertId___closed__1;
@ -237,10 +236,10 @@ lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_Elab_convertType___boxed(lean_object*, lean_object*);
lean_object* l_mkHashMapImp___rarg(lean_object*);
extern lean_object* l_Lean_Parser_Term_binderTactic___elambda__1___rarg___closed__1;
extern lean_object* l_Lean_Expr_getAppArgs___closed__1;
lean_object* l___regBuiltinTermElab_Lean_Elab_convertSortApp(lean_object*);
extern lean_object* l_Lean_Parser_Level_ident___elambda__1___rarg___closed__1;
lean_object* l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__2;
extern lean_object* l_Lean_Expr_inhabited___closed__1;
extern lean_object* l_Lean_nameToExprAux___main___closed__4;
lean_object* l___private_Init_Lean_Elaborator_PreTerm_4__processBinder___closed__2;
extern lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__2;
@ -251,6 +250,7 @@ lean_object* l_Lean_Syntax_toNat___rarg(lean_object*);
lean_object* l_Lean_Syntax_getPos___rarg(lean_object*);
extern lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__1;
lean_object* l___regBuiltinTermElab_Lean_Elab_convertHole___closed__2;
lean_object* l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux(lean_object*);
lean_object* l_Lean_Elab_convertProp(lean_object*, lean_object*);
lean_object* l_Lean_Elab_getScope___rarg(lean_object*);
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
@ -283,12 +283,12 @@ lean_object* l_Lean_Elab_convertForall___boxed(lean_object*, lean_object*, lean_
lean_object* l___private_Init_Lean_Elaborator_PreTerm_4__processBinder___closed__4;
lean_object* lean_level_mk_max(lean_object*, lean_object*);
lean_object* l_Lean_registerBuiltinPreTermElabAttr___lambda__1___closed__5;
lean_object* l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__3;
lean_object* l___regBuiltinTermElab_Lean_Elab_convertProp___closed__3;
lean_object* l_Lean_declareBuiltinPreTermElab(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerTagAttribute___lambda__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elaborator_PreTerm_5__processBinders___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___boxed(lean_object*);
lean_object* l___private_Init_Lean_Elaborator_PreTerm_5__processBinders___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_toPreTerm___closed__4;
lean_object* l_Lean_oldElaborateAux___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
@ -1259,7 +1259,7 @@ lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_box(0);
x_4 = l_Lean_Expr_mkAnnotation___closed__2;
x_5 = l_Lean_KVMap_setName(x_3, x_4, x_1);
x_6 = lean_expr_mk_mdata(x_5, x_2);
x_6 = l_Lean_mkMData(x_5, x_2);
return x_6;
}
}
@ -1312,8 +1312,8 @@ lean_object* l_Lean_mkAsPattern(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_expr_mk_fvar(x_1);
x_4 = lean_expr_mk_app(x_3, x_2);
x_3 = l_Lean_mkFVar(x_1);
x_4 = l_Lean_mkApp(x_3, x_2);
x_5 = l_Lean_mkAsPattern___closed__2;
x_6 = l_Lean_Expr_mkAnnotation(x_5, x_4);
return x_6;
@ -1343,7 +1343,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_mkPreTypeAscription___closed__2;
x_3 = lean_expr_mk_const(x_2, x_1);
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
@ -1352,8 +1352,8 @@ _start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = l_Lean_mkPreTypeAscription___closed__3;
x_4 = lean_expr_mk_app(x_3, x_2);
x_5 = lean_expr_mk_app(x_4, x_1);
x_4 = l_Lean_mkApp(x_3, x_2);
x_5 = l_Lean_mkApp(x_4, x_1);
return x_5;
}
}
@ -2035,7 +2035,7 @@ lean_inc(x_16);
lean_dec(x_11);
x_17 = l___private_Init_Lean_Elaborator_PreTerm_1__setPos___closed__4;
x_18 = l_Lean_KVMap_setNat(x_15, x_17, x_16);
x_19 = lean_expr_mk_mdata(x_18, x_2);
x_19 = l_Lean_mkMData(x_18, x_2);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_4);
@ -2294,7 +2294,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_box(0);
x_2 = lean_expr_mk_mvar(x_1);
x_2 = l_Lean_mkMVar(x_1);
return x_2;
}
}
@ -2322,7 +2322,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Level_one___closed__1;
x_2 = lean_expr_mk_sort(x_1);
x_2 = l_Lean_mkSort(x_1);
return x_2;
}
}
@ -2414,7 +2414,7 @@ lean_object* l_Lean_Elab_convertSort___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Expr_inhabited___closed__1;
x_2 = l_Lean_Expr_getAppArgs___closed__1;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
@ -2480,7 +2480,7 @@ lean_object* l_Lean_Elab_convertProp___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Expr_inhabited___closed__1;
x_2 = l_Lean_Expr_getAppArgs___closed__1;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
@ -2567,7 +2567,7 @@ lean_dec(x_7);
if (x_14 == 0)
{
lean_object* x_15;
x_15 = lean_expr_mk_sort(x_12);
x_15 = l_Lean_mkSort(x_12);
lean_ctor_set(x_10, 0, x_15);
return x_10;
}
@ -2575,7 +2575,7 @@ else
{
lean_object* x_16; lean_object* x_17;
x_16 = lean_level_mk_succ(x_12);
x_17 = lean_expr_mk_sort(x_16);
x_17 = l_Lean_mkSort(x_16);
lean_ctor_set(x_10, 0, x_17);
return x_10;
}
@ -2594,7 +2594,7 @@ lean_dec(x_7);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23;
x_22 = lean_expr_mk_sort(x_18);
x_22 = l_Lean_mkSort(x_18);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_19);
@ -2604,7 +2604,7 @@ else
{
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = lean_level_mk_succ(x_18);
x_25 = lean_expr_mk_sort(x_24);
x_25 = l_Lean_mkSort(x_24);
x_26 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_19);
@ -2684,7 +2684,7 @@ x_5 = l_Lean_addBuiltinPreTermElab(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__1() {
lean_object* _init_l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__1() {
_start:
{
lean_object* x_1;
@ -2692,7 +2692,7 @@ x_1 = lean_mk_string("Init.Lean.Elaborator.PreTerm");
return x_1;
}
}
lean_object* _init_l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__2() {
lean_object* _init_l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__2() {
_start:
{
lean_object* x_1;
@ -2700,33 +2700,33 @@ x_1 = lean_mk_string("to be deleted");
return x_1;
}
}
lean_object* _init_l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__3() {
lean_object* _init_l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__1;
x_1 = l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__1;
x_2 = lean_unsigned_to_nat(141u);
x_3 = lean_unsigned_to_nat(0u);
x_4 = l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__2;
x_4 = l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__2;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
return x_5;
}
}
lean_object* l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal(lean_object* x_1) {
lean_object* l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Expr_inhabited;
x_3 = l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__3;
x_2 = l_Lean_Expr_Inhabited;
x_3 = l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__3;
x_4 = lean_panic_fn(x_3);
return x_4;
}
}
lean_object* l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___boxed(lean_object* x_1) {
lean_object* l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal(x_1);
x_2 = l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux(x_1);
lean_dec(x_1);
return x_2;
}
@ -2781,7 +2781,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Array_umapMAux___main___at___private_Init_Lean_Elaborator_PreTerm_4__processBinder___spec__1___closed__5;
x_3 = lean_expr_mk_const(x_2, x_1);
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
@ -2977,8 +2977,8 @@ x_51 = lean_ctor_get(x_49, 1);
lean_inc(x_51);
lean_dec(x_49);
x_52 = l_Array_umapMAux___main___at___private_Init_Lean_Elaborator_PreTerm_4__processBinder___spec__1___closed__6;
x_53 = lean_expr_mk_app(x_52, x_26);
x_54 = lean_expr_mk_app(x_53, x_50);
x_53 = l_Lean_mkApp(x_52, x_26);
x_54 = l_Lean_mkApp(x_53, x_50);
x_55 = 0;
x_56 = l_Lean_Elab_mkLocalDecl(x_25, x_54, x_55, x_6, x_51);
x_57 = lean_ctor_get(x_56, 0);
@ -3940,7 +3940,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_convertSorry___rarg___closed__2;
x_3 = lean_expr_mk_const(x_2, x_1);
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
@ -3950,7 +3950,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_convertSorry___rarg___closed__3;
x_2 = l___private_Init_Lean_Elaborator_PreTerm_2__mkHoleFor___closed__1;
x_3 = lean_expr_mk_app(x_1, x_2);
x_3 = l_Lean_mkApp(x_1, x_2);
return x_3;
}
}
@ -4068,7 +4068,7 @@ lean_dec(x_12);
x_21 = lean_ctor_get(x_13, 0);
lean_inc(x_21);
lean_dec(x_13);
x_22 = l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal(x_21);
x_22 = l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux(x_21);
lean_dec(x_21);
lean_ctor_set(x_5, 0, x_22);
return x_5;
@ -4109,7 +4109,7 @@ lean_dec(x_28);
x_37 = lean_ctor_get(x_29, 0);
lean_inc(x_37);
lean_dec(x_29);
x_38 = l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal(x_37);
x_38 = l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux(x_37);
lean_dec(x_37);
x_39 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_39, 0, x_38);
@ -4667,12 +4667,12 @@ lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_convertSortApp___closed__3
res = l___regBuiltinTermElab_Lean_Elab_convertSortApp(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__1 = _init_l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__1();
lean_mark_persistent(l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__1);
l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__2 = _init_l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__2();
lean_mark_persistent(l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__2);
l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__3 = _init_l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__3();
lean_mark_persistent(l___private_Init_Lean_Elaborator_PreTerm_3__mkLocal___closed__3);
l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__1 = _init_l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__1();
lean_mark_persistent(l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__1);
l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__2 = _init_l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__2();
lean_mark_persistent(l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__2);
l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__3 = _init_l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__3();
lean_mark_persistent(l___private_Init_Lean_Elaborator_PreTerm_3__mkLocalAux___closed__3);
l_Array_umapMAux___main___at___private_Init_Lean_Elaborator_PreTerm_4__processBinder___spec__1___closed__1 = _init_l_Array_umapMAux___main___at___private_Init_Lean_Elaborator_PreTerm_4__processBinder___spec__1___closed__1();
lean_mark_persistent(l_Array_umapMAux___main___at___private_Init_Lean_Elaborator_PreTerm_4__processBinder___spec__1___closed__1);
l_Array_umapMAux___main___at___private_Init_Lean_Elaborator_PreTerm_4__processBinder___spec__1___closed__2 = _init_l_Array_umapMAux___main___at___private_Init_Lean_Elaborator_PreTerm_4__processBinder___spec__1___closed__2();

3900
stage0/library/Init/Lean/Expr.c generated
View file

File diff suppressed because it is too large Load diff

53
stage0/library/Init/Lean/LocalContext.c generated
View file

@ -38,7 +38,6 @@ lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl___spec__6__
uint8_t l_Lean_LocalContext_isSubPrefixOfAux(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_local_ctx_find_from_user_name(lean_object*, lean_object*);
lean_object* l_Nat_foldRevAux___main___at_Lean_LocalContext_mkLambda___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_mk_forall(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__8(lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__7(lean_object*);
lean_object* l_Lean_LocalContext_forM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -70,7 +69,6 @@ uint8_t l_Array_anyRangeMAux___main___at_Lean_LocalContext_all___spec__4(lean_ob
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldl___spec__6(lean_object*);
lean_object* l_PersistentArray_getAux___main___at___private_Init_Lean_LocalContext_1__popTailNoneAux___main___spec__2(lean_object*, size_t, size_t);
lean_object* l_Lean_LocalContext_allM___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_mk_let(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_PersistentHashMap_empty___rarg___closed__2;
lean_object* l_Lean_LocalContext_foldlM___at_Lean_LocalContext_foldl___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentArray_foldlFromMAux___main___at_Lean_LocalContext_foldlFrom___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -81,6 +79,7 @@ lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldl___spec__5__
lean_object* l_Lean_LocalContext_anyM___boxed(lean_object*);
lean_object* l_Lean_LocalContext_Inhabited___closed__1;
lean_object* l_PersistentArray_anyM___at_Lean_LocalContext_any___spec__1___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_Inhabited___closed__1;
lean_object* l_PersistentArray_findM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_PersistentHashMap_containsAux___main___at_Lean_LocalContext_contains___spec__2(lean_object*, size_t, lean_object*);
lean_object* l_Lean_LocalContext_findFVar___boxed(lean_object*, lean_object*);
@ -89,6 +88,7 @@ lean_object* l_PersistentArray_anyMAux___main___at_Lean_LocalContext_any___spec_
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__4(lean_object*);
size_t l_USize_sub(size_t, size_t);
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__6___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLet(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_LocalContext_findDeclM___at_Lean_LocalContext_findDecl___spec__1(lean_object*);
lean_object* l_PersistentArray_anyM___at_Lean_LocalContext_anyM___spec__1___boxed(lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__10(lean_object*);
@ -120,7 +120,6 @@ lean_object* l___private_Init_Lean_LocalContext_1__popTailNoneAux(lean_object*);
lean_object* l_PersistentHashMap_erase___at_Lean_LocalContext_erase___spec__1(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_insert___at_Lean_LocalContext_mkLocalDecl___spec__1(lean_object*, lean_object*, lean_object*);
uint8_t lean_expr_has_loose_bvar(lean_object*, lean_object*);
lean_object* lean_expr_mk_fvar(lean_object*);
lean_object* lean_local_ctx_mk_local_decl(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_PersistentArray_set___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_any___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -172,6 +171,7 @@ lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec_
lean_object* l_Lean_LocalDecl_updateUserName(lean_object*, lean_object*);
lean_object* l_PersistentArray_anyMAux___main___at_Lean_LocalContext_all___spec__2___boxed(lean_object*, lean_object*);
size_t l_USize_add(size_t, size_t);
extern lean_object* l_Lean_Expr_Inhabited;
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__5___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentArray_anyM___at_Lean_LocalContext_allM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -188,6 +188,7 @@ lean_object* l_Array_indexOfAux___main___at_Lean_LocalContext_erase___spec__3___
lean_object* l_PersistentArray_findMAux___main___at_Lean_LocalContext_findDecl___spec__3(lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__8___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__3___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkFVar(lean_object*);
lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -202,6 +203,7 @@ lean_object* l_Lean_LocalContext_foldlFromM___rarg(lean_object*, lean_object*, l
lean_object* lean_local_ctx_get(lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_mkBinding___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_allM___spec__5___boxed(lean_object*);
lean_object* l_Lean_mkLambda(lean_object*, uint8_t, lean_object*, 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*);
lean_object* l_Array_findRevMAux___main___at_Lean_LocalContext_findDeclRev___spec__5(lean_object*);
@ -218,6 +220,7 @@ lean_object* l_PersistentHashMap_insertAux___main___at_Lean_LocalContext_mkLocal
lean_object* l_Lean_LocalContext_any___boxed(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_findDecl___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkForall(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_PersistentArray_get_x21___at___private_Init_Lean_LocalContext_1__popTailNoneAux___main___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_findDeclRevM___at_Lean_LocalContext_findDeclRev___spec__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_findDeclM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -240,7 +243,6 @@ lean_object* l_Lean_LocalDecl_Inhabited___closed__1;
lean_object* l_Array_findMAux___main___at_Lean_LocalContext_findDecl___spec__6___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
lean_object* l_PersistentArray_foldlFromM___at_Lean_LocalContext_foldlFrom___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_inhabited;
lean_object* l_PersistentArray_foldlMAux___main___at_Lean_LocalContext_foldl___spec__3(lean_object*);
lean_object* l_Lean_LocalDecl_type(lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__9(lean_object*);
@ -304,7 +306,6 @@ lean_object* l_Array_anyRangeMAux___main___at_Lean_LocalContext_anyM___spec__4__
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_PersistentArray_findRevM___at_Lean_LocalContext_findDeclRev___spec__2___rarg___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_inhabited___closed__1;
lean_object* l_Lean_LocalContext_foldlFromM___at_Lean_LocalContext_foldlFrom___spec__1(lean_object*);
uint8_t l_PersistentArray_anyMAux___main___at_Lean_LocalContext_all___spec__2(lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
@ -317,7 +318,6 @@ lean_object* l_Lean_LocalDecl_value___closed__1;
lean_object* l_PersistentArray_findRevMAux___main___at_Lean_LocalContext_findFromUserName___spec__3(lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_isEmpty___boxed(lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_LocalContext_foldlFrom___spec__9___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_mk_lambda(lean_object*, uint8_t, lean_object*, lean_object*);
uint8_t l_PersistentHashMap_isEmpty___at_Lean_LocalContext_isEmpty___spec__1(lean_object*);
lean_object* l_Lean_LocalDecl_index(lean_object*);
lean_object* l_PersistentArray_foldlFromM___at_Lean_LocalContext_foldlFrom___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -384,7 +384,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_box(0);
x_3 = l_Lean_Expr_inhabited___closed__1;
x_3 = l_Lean_Expr_Inhabited___closed__1;
x_4 = lean_alloc_ctor(1, 5, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -591,7 +591,7 @@ _start:
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Expr_inhabited;
x_2 = l_Lean_Expr_Inhabited;
x_3 = l_Lean_LocalDecl_value___closed__3;
x_4 = lean_panic_fn(x_3);
return x_4;
@ -689,7 +689,7 @@ _start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_LocalDecl_name(x_1);
x_3 = lean_expr_mk_fvar(x_2);
x_3 = l_Lean_mkFVar(x_2);
return x_3;
}
}
@ -5147,7 +5147,7 @@ lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_o
x_8 = lean_unsigned_to_nat(1u);
x_9 = lean_nat_sub(x_4, x_8);
lean_dec(x_4);
x_10 = l_Lean_Expr_inhabited;
x_10 = l_Lean_Expr_Inhabited;
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);
@ -5182,7 +5182,7 @@ lean_dec(x_18);
if (x_1 == 0)
{
lean_object* x_21;
x_21 = lean_expr_mk_forall(x_17, x_19, x_20, x_5);
x_21 = l_Lean_mkForall(x_17, x_19, x_20, x_5);
x_4 = x_9;
x_5 = x_21;
goto _start;
@ -5190,7 +5190,7 @@ goto _start;
else
{
lean_object* x_23;
x_23 = lean_expr_mk_lambda(x_17, x_19, x_20, x_5);
x_23 = l_Lean_mkLambda(x_17, x_19, x_20, x_5);
x_4 = x_9;
x_5 = x_23;
goto _start;
@ -5217,14 +5217,15 @@ goto _start;
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32;
lean_object* x_30; lean_object* x_31; uint8_t x_32; lean_object* x_33;
x_30 = lean_expr_abstract_range(x_26, x_9, x_3);
lean_dec(x_26);
x_31 = lean_expr_abstract_range(x_27, x_9, x_3);
lean_dec(x_27);
x_32 = lean_expr_mk_let(x_25, x_30, x_31, x_5);
x_32 = 0;
x_33 = l_Lean_mkLet(x_25, x_30, x_31, x_5, x_32);
x_4 = x_9;
x_5 = x_32;
x_5 = x_33;
goto _start;
}
}
@ -5283,7 +5284,7 @@ lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_ob
x_7 = lean_unsigned_to_nat(1u);
x_8 = lean_nat_sub(x_3, x_7);
lean_dec(x_3);
x_9 = l_Lean_Expr_inhabited;
x_9 = l_Lean_Expr_Inhabited;
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);
@ -5315,7 +5316,7 @@ x_18 = lean_ctor_get_uint8(x_15, sizeof(void*)*4);
lean_dec(x_15);
x_19 = lean_expr_abstract_range(x_17, x_8, x_2);
lean_dec(x_17);
x_20 = lean_expr_mk_lambda(x_16, x_18, x_19, x_4);
x_20 = l_Lean_mkLambda(x_16, x_18, x_19, x_4);
x_3 = x_8;
x_4 = x_20;
goto _start;
@ -5341,14 +5342,15 @@ goto _start;
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
lean_object* x_27; lean_object* x_28; uint8_t x_29; lean_object* x_30;
x_27 = lean_expr_abstract_range(x_23, x_8, x_2);
lean_dec(x_23);
x_28 = lean_expr_abstract_range(x_24, x_8, x_2);
lean_dec(x_24);
x_29 = lean_expr_mk_let(x_22, x_27, x_28, x_4);
x_29 = 0;
x_30 = l_Lean_mkLet(x_22, x_27, x_28, x_4, x_29);
x_3 = x_8;
x_4 = x_29;
x_4 = x_30;
goto _start;
}
}
@ -5403,7 +5405,7 @@ lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_ob
x_7 = lean_unsigned_to_nat(1u);
x_8 = lean_nat_sub(x_3, x_7);
lean_dec(x_3);
x_9 = l_Lean_Expr_inhabited;
x_9 = l_Lean_Expr_Inhabited;
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);
@ -5435,7 +5437,7 @@ x_18 = lean_ctor_get_uint8(x_15, sizeof(void*)*4);
lean_dec(x_15);
x_19 = lean_expr_abstract_range(x_17, x_8, x_2);
lean_dec(x_17);
x_20 = lean_expr_mk_forall(x_16, x_18, x_19, x_4);
x_20 = l_Lean_mkForall(x_16, x_18, x_19, x_4);
x_3 = x_8;
x_4 = x_20;
goto _start;
@ -5461,14 +5463,15 @@ goto _start;
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
lean_object* x_27; lean_object* x_28; uint8_t x_29; lean_object* x_30;
x_27 = lean_expr_abstract_range(x_23, x_8, x_2);
lean_dec(x_23);
x_28 = lean_expr_abstract_range(x_24, x_8, x_2);
lean_dec(x_24);
x_29 = lean_expr_mk_let(x_22, x_27, x_28, x_4);
x_29 = 0;
x_30 = l_Lean_mkLet(x_22, x_27, x_28, x_4, x_29);
x_3 = x_8;
x_4 = x_29;
x_4 = x_30;
goto _start;
}
}

528
stage0/library/Init/Lean/Meta/Basic.c generated
View file

@ -23,7 +23,6 @@ lean_object* l_Lean_Meta_dbgTrace___rarg___lambda__1___boxed(lean_object*, lean_
lean_object* l___private_Init_Lean_Meta_Basic_2__reduceAll_x3f(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkFreshLevelMVarId___boxed(lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isClassQuick___main___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getEnv___boxed(lean_object*);
lean_object* l_Lean_Meta_usingAtLeastTransparency___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___main___at_Lean_Meta_forallTelescope___spec__1(lean_object*);
@ -42,7 +41,7 @@ lean_object* lean_local_ctx_mk_let_decl(lean_object*, lean_object*, lean_object*
lean_object* l_Lean_Meta_withNewLocalInstances___main(lean_object*);
lean_object* l_Lean_Meta_forallTelescopeReducing___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_usingTransparency___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_expr_hash(lean_object*);
size_t l_Lean_Expr_hash(lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_4__getOptions___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_4__getOptions(lean_object*, lean_object*);
lean_object* l_Lean_Meta_getConstNoEx(lean_object*, lean_object*, lean_object*);
@ -54,6 +53,7 @@ lean_object* l___private_Init_Lean_Meta_Basic_9__lambdaTelescopeAux___rarg(lean_
lean_object* l_Lean_Meta_forallBoundedTelescope(lean_object*);
lean_object* lean_dbg_trace(lean_object*, lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_beq___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_Inhabited___closed__1;
lean_object* l_Lean_Meta_throwEx___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_dbgTrace___rarg___closed__1;
lean_object* l_Lean_Meta_assignLevelMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -76,7 +76,6 @@ lean_object* l_Lean_Meta_getMCtx(lean_object*);
lean_object* lean_metavar_ctx_get_expr_assignment(lean_object*, lean_object*);
lean_object* l_Lean_Meta_usingDefault(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_InfoCacheKey_HasBeq___boxed(lean_object*, lean_object*);
lean_object* lean_expr_mk_fvar(lean_object*);
lean_object* lean_local_ctx_mk_local_decl(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_tracer___closed__2;
@ -108,6 +107,7 @@ uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_Meta_resettingTypeClassCache(lean_object*);
lean_object* l_Lean_Meta_isClassExpensive(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isClassQuickConst(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkFVar(lean_object*);
lean_object* l_Lean_Meta_usingTransparency(lean_object*);
lean_object* l_Lean_Meta_getConstAux(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
@ -191,20 +191,20 @@ lean_object* l_Lean_Meta_InfoCacheKey_Inhabited___closed__1;
lean_object* l_Lean_Meta_forallBoundedTelescope___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_MetaM_inhabited(lean_object*, lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_Hashable___closed__1;
extern lean_object* l_Lean_Expr_inhabited___closed__1;
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_throwEx(lean_object*);
uint8_t l_Lean_Expr_hasMVar(lean_object*);
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Option_hash___at_Lean_Meta_InfoCacheKey_Hashable___spec__1___boxed(lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_hash___boxed(lean_object*);
lean_object* l_Lean_Meta_isClassQuick___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isClassQuick___main___closed__1;
lean_object* l_Lean_Meta_isReadOnlyOrSyntheticExprMVar___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MetavarContext_addLevelMVarDecl(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkFreshLevelMVarId(lean_object*);
uint8_t lean_expr_has_expr_mvar(lean_object*);
lean_object* l_Lean_Meta_tracer___closed__3;
lean_object* l_Lean_Meta_liftStateMCtx___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__4___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_unreachable_x21___rarg(lean_object*);
lean_object* l_Lean_Meta_liftStateMCtx___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getMVarDecl(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getMCtx___rarg(lean_object*);
@ -229,7 +229,7 @@ lean_object* l___private_Init_Lean_Meta_Basic_9__lambdaTelescopeAux(lean_object*
lean_object* l_Lean_MetavarContext_MkBinding_mkBinding___at_Lean_MetavarContext_mkBinding___spec__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_MetaM_inhabited___rarg(lean_object*);
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*);
uint8_t lean_expr_has_level_mvar(lean_object*);
uint8_t l_Lean_Expr_CachedData_binderInfo(uint64_t);
uint8_t _init_l_Lean_Meta_TransparencyMode_Inhabited() {
_start:
{
@ -471,7 +471,7 @@ _start:
lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = 1;
x_3 = l_Lean_Expr_inhabited___closed__1;
x_3 = l_Lean_Expr_Inhabited___closed__1;
x_4 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_4, 0, x_3);
lean_ctor_set(x_4, 1, x_1);
@ -515,7 +515,7 @@ x_2 = lean_ctor_get_uint8(x_1, sizeof(void*)*2);
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get(x_1, 1);
x_5 = l_Lean_Meta_TransparencyMode_hash(x_2);
x_6 = lean_expr_hash(x_3);
x_6 = l_Lean_Expr_hash(x_3);
x_7 = l_Option_hash___at_Lean_Meta_InfoCacheKey_Hashable___spec__1(x_4);
x_8 = lean_usize_mix_hash(x_6, x_7);
x_9 = lean_usize_mix_hash(x_5, x_8);
@ -2171,128 +2171,68 @@ lean_object* l_Lean_Meta_instantiateMVars(lean_object* x_1, lean_object* x_2, le
_start:
{
uint8_t x_4;
x_4 = lean_expr_has_expr_mvar(x_1);
x_4 = l_Lean_Expr_hasMVar(x_1);
if (x_4 == 0)
{
uint8_t x_5;
x_5 = lean_expr_has_level_mvar(x_1);
if (x_5 == 0)
{
lean_object* x_6;
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_3);
return x_6;
lean_object* x_5;
x_5 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_3);
return x_5;
}
else
{
uint8_t x_7;
x_7 = !lean_is_exclusive(x_3);
if (x_7 == 0)
uint8_t x_6;
x_6 = !lean_is_exclusive(x_3);
if (x_6 == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_8 = lean_ctor_get(x_3, 1);
x_9 = l_Lean_MetavarContext_instantiateMVars(x_8, x_1);
x_10 = lean_ctor_get(x_9, 0);
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_7 = lean_ctor_get(x_3, 1);
x_8 = l_Lean_MetavarContext_instantiateMVars(x_7, x_1);
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
x_10 = lean_ctor_get(x_8, 1);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
lean_ctor_set(x_3, 1, x_11);
x_12 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_3);
return x_12;
lean_dec(x_8);
lean_ctor_set(x_3, 1, x_10);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_9);
lean_ctor_set(x_11, 1, x_3);
return x_11;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_13 = lean_ctor_get(x_3, 0);
x_14 = lean_ctor_get(x_3, 1);
x_15 = lean_ctor_get(x_3, 2);
x_16 = lean_ctor_get(x_3, 3);
x_17 = lean_ctor_get(x_3, 4);
x_18 = lean_ctor_get(x_3, 5);
lean_inc(x_18);
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_12 = lean_ctor_get(x_3, 0);
x_13 = lean_ctor_get(x_3, 1);
x_14 = lean_ctor_get(x_3, 2);
x_15 = lean_ctor_get(x_3, 3);
x_16 = lean_ctor_get(x_3, 4);
x_17 = lean_ctor_get(x_3, 5);
lean_inc(x_17);
lean_inc(x_16);
lean_inc(x_15);
lean_inc(x_14);
lean_inc(x_13);
lean_inc(x_12);
lean_dec(x_3);
x_19 = l_Lean_MetavarContext_instantiateMVars(x_14, x_1);
x_20 = lean_ctor_get(x_19, 0);
x_18 = l_Lean_MetavarContext_instantiateMVars(x_13, x_1);
x_19 = lean_ctor_get(x_18, 0);
lean_inc(x_19);
x_20 = lean_ctor_get(x_18, 1);
lean_inc(x_20);
x_21 = lean_ctor_get(x_19, 1);
lean_inc(x_21);
lean_dec(x_19);
x_22 = lean_alloc_ctor(0, 6, 0);
lean_ctor_set(x_22, 0, x_13);
lean_dec(x_18);
x_21 = lean_alloc_ctor(0, 6, 0);
lean_ctor_set(x_21, 0, x_12);
lean_ctor_set(x_21, 1, x_20);
lean_ctor_set(x_21, 2, x_14);
lean_ctor_set(x_21, 3, x_15);
lean_ctor_set(x_21, 4, x_16);
lean_ctor_set(x_21, 5, x_17);
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_19);
lean_ctor_set(x_22, 1, x_21);
lean_ctor_set(x_22, 2, x_15);
lean_ctor_set(x_22, 3, x_16);
lean_ctor_set(x_22, 4, x_17);
lean_ctor_set(x_22, 5, x_18);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_20);
lean_ctor_set(x_23, 1, x_22);
return x_23;
}
}
}
else
{
uint8_t x_24;
x_24 = !lean_is_exclusive(x_3);
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_25 = lean_ctor_get(x_3, 1);
x_26 = l_Lean_MetavarContext_instantiateMVars(x_25, x_1);
x_27 = lean_ctor_get(x_26, 0);
lean_inc(x_27);
x_28 = lean_ctor_get(x_26, 1);
lean_inc(x_28);
lean_dec(x_26);
lean_ctor_set(x_3, 1, x_28);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_3);
return x_29;
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40;
x_30 = lean_ctor_get(x_3, 0);
x_31 = lean_ctor_get(x_3, 1);
x_32 = lean_ctor_get(x_3, 2);
x_33 = lean_ctor_get(x_3, 3);
x_34 = lean_ctor_get(x_3, 4);
x_35 = lean_ctor_get(x_3, 5);
lean_inc(x_35);
lean_inc(x_34);
lean_inc(x_33);
lean_inc(x_32);
lean_inc(x_31);
lean_inc(x_30);
lean_dec(x_3);
x_36 = l_Lean_MetavarContext_instantiateMVars(x_31, x_1);
x_37 = lean_ctor_get(x_36, 0);
lean_inc(x_37);
x_38 = lean_ctor_get(x_36, 1);
lean_inc(x_38);
lean_dec(x_36);
x_39 = lean_alloc_ctor(0, 6, 0);
lean_ctor_set(x_39, 0, x_30);
lean_ctor_set(x_39, 1, x_38);
lean_ctor_set(x_39, 2, x_32);
lean_ctor_set(x_39, 3, x_33);
lean_ctor_set(x_39, 4, x_34);
lean_ctor_set(x_39, 5, x_35);
x_40 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_40, 0, x_37);
lean_ctor_set(x_40, 1, x_39);
return x_40;
return x_22;
}
}
}
@ -3790,6 +3730,15 @@ lean_dec(x_2);
return x_4;
}
}
lean_object* _init_l_Lean_Meta_isClassQuick___main___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Meta_MetaM_inhabited___boxed), 2, 1);
lean_closure_set(x_1, 0, lean_box(0));
return x_1;
}
}
lean_object* l_Lean_Meta_isClassQuick___main(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -3806,6 +3755,7 @@ x_6 = lean_metavar_ctx_get_expr_assignment(x_5, x_4);
if (lean_obj_tag(x_6) == 0)
{
lean_object* x_7; lean_object* x_8;
lean_dec(x_2);
x_7 = lean_box(0);
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_7);
@ -3829,6 +3779,7 @@ x_11 = lean_ctor_get(x_1, 0);
lean_inc(x_11);
lean_dec(x_1);
x_12 = l_Lean_Meta_isClassQuickConst(x_11, x_2, x_3);
lean_dec(x_2);
return x_12;
}
case 5:
@ -3847,12 +3798,14 @@ x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
lean_dec(x_14);
x_16 = l_Lean_Meta_isClassQuickConst(x_15, x_2, x_3);
lean_dec(x_2);
return x_16;
}
case 6:
{
lean_object* x_17; lean_object* x_18;
lean_dec(x_14);
lean_dec(x_2);
x_17 = lean_box(2);
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_17);
@ -3863,6 +3816,7 @@ default:
{
lean_object* x_19; lean_object* x_20;
lean_dec(x_14);
lean_dec(x_2);
x_19 = lean_box(0);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_19);
@ -3883,6 +3837,7 @@ goto _start;
case 8:
{
lean_object* x_23; lean_object* x_24;
lean_dec(x_2);
lean_dec(x_1);
x_23 = lean_box(2);
x_24 = lean_alloc_ctor(0, 2, 0);
@ -3902,6 +3857,7 @@ goto _start;
case 11:
{
lean_object* x_27; lean_object* x_28;
lean_dec(x_2);
lean_dec(x_1);
x_27 = lean_box(2);
x_28 = lean_alloc_ctor(0, 2, 0);
@ -3909,26 +3865,27 @@ lean_ctor_set(x_28, 0, x_27);
lean_ctor_set(x_28, 1, x_3);
return x_28;
}
case 12:
{
lean_object* x_29; lean_object* x_30; lean_object* x_31;
lean_dec(x_1);
x_29 = l_Lean_Meta_isClassQuick___main___closed__1;
x_30 = l_unreachable_x21___rarg(x_29);
x_31 = lean_apply_2(x_30, x_2, x_3);
return x_31;
}
default:
{
lean_object* x_29; lean_object* x_30;
lean_dec(x_1);
x_29 = lean_box(0);
x_30 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_30, 0, x_29);
lean_ctor_set(x_30, 1, x_3);
return x_30;
}
}
}
}
lean_object* l_Lean_Meta_isClassQuick___main___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Meta_isClassQuick___main(x_1, x_2, x_3);
lean_object* x_32; lean_object* x_33;
lean_dec(x_2);
return x_4;
lean_dec(x_1);
x_32 = lean_box(0);
x_33 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_3);
return x_33;
}
}
}
}
lean_object* l_Lean_Meta_isClassQuick(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@ -3939,15 +3896,6 @@ x_4 = l_Lean_Meta_isClassQuick___main(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_Meta_isClassQuick___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Meta_isClassQuick(x_1, x_2, x_3);
lean_dec(x_2);
return x_4;
}
}
lean_object* l_Lean_Meta_resettingTypeClassCache___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -4044,6 +3992,7 @@ lean_inc(x_14);
lean_dec(x_12);
x_15 = l_Lean_LocalDecl_type(x_13);
lean_dec(x_13);
lean_inc(x_5);
lean_inc(x_15);
x_16 = l_Lean_Meta_isClassQuick___main(x_15, x_5, x_14);
if (lean_obj_tag(x_16) == 0)
@ -4360,91 +4309,92 @@ _start:
lean_object* x_12;
if (lean_obj_tag(x_9) == 7)
{
lean_object* x_37; uint8_t x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48;
lean_object* x_37; lean_object* x_38; lean_object* x_39; uint64_t x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; uint8_t x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49;
x_37 = lean_ctor_get(x_9, 0);
lean_inc(x_37);
x_38 = lean_ctor_get_uint8(x_9, sizeof(void*)*3);
x_39 = lean_ctor_get(x_9, 1);
x_38 = lean_ctor_get(x_9, 1);
lean_inc(x_38);
x_39 = lean_ctor_get(x_9, 2);
lean_inc(x_39);
x_40 = lean_ctor_get(x_9, 2);
lean_inc(x_40);
x_40 = lean_ctor_get_uint64(x_9, sizeof(void*)*3);
lean_dec(x_9);
x_41 = lean_array_get_size(x_7);
lean_inc(x_7);
x_42 = lean_expr_instantiate_rev_range(x_39, x_8, x_41, x_7);
x_42 = lean_expr_instantiate_rev_range(x_38, x_8, x_41, x_7);
lean_dec(x_41);
lean_dec(x_39);
lean_dec(x_38);
x_43 = l_Lean_Meta_mkFreshId___rarg(x_11);
x_44 = lean_ctor_get(x_43, 0);
lean_inc(x_44);
x_45 = lean_ctor_get(x_43, 1);
lean_inc(x_45);
lean_dec(x_43);
x_46 = (uint8_t)((x_40 << 24) >> 61);
lean_inc(x_44);
x_46 = lean_local_ctx_mk_local_decl(x_6, x_44, x_37, x_42, x_38);
x_47 = lean_expr_mk_fvar(x_44);
x_48 = lean_array_push(x_7, x_47);
x_47 = lean_local_ctx_mk_local_decl(x_6, x_44, x_37, x_42, x_46);
x_48 = l_Lean_mkFVar(x_44);
x_49 = lean_array_push(x_7, x_48);
if (lean_obj_tag(x_4) == 0)
{
x_6 = x_46;
x_7 = x_48;
x_9 = x_40;
x_6 = x_47;
x_7 = x_49;
x_9 = x_39;
x_11 = x_45;
goto _start;
}
else
{
lean_object* x_50; lean_object* x_51; uint8_t x_52;
x_50 = lean_ctor_get(x_4, 0);
lean_inc(x_50);
x_51 = lean_array_get_size(x_48);
x_52 = lean_nat_dec_lt(x_51, x_50);
lean_dec(x_50);
if (x_52 == 0)
lean_object* x_51; lean_object* x_52; uint8_t x_53;
x_51 = lean_ctor_get(x_4, 0);
lean_inc(x_51);
x_52 = lean_array_get_size(x_49);
x_53 = lean_nat_dec_lt(x_52, x_51);
lean_dec(x_51);
if (x_53 == 0)
{
lean_object* x_53; lean_object* x_54; uint8_t x_55;
lean_object* x_54; lean_object* x_55; uint8_t x_56;
lean_dec(x_4);
lean_dec(x_1);
lean_inc(x_48);
x_53 = lean_expr_instantiate_rev_range(x_40, x_8, x_51, x_48);
lean_dec(x_51);
lean_dec(x_40);
lean_inc(x_48);
x_54 = lean_apply_2(x_5, x_48, x_53);
x_55 = !lean_is_exclusive(x_10);
if (x_55 == 0)
lean_inc(x_49);
x_54 = lean_expr_instantiate_rev_range(x_39, x_8, x_52, x_49);
lean_dec(x_52);
lean_dec(x_39);
lean_inc(x_49);
x_55 = lean_apply_2(x_5, x_49, x_54);
x_56 = !lean_is_exclusive(x_10);
if (x_56 == 0)
{
lean_object* x_56; lean_object* x_57;
x_56 = lean_ctor_get(x_10, 1);
lean_dec(x_56);
lean_ctor_set(x_10, 1, x_46);
x_57 = l_Lean_Meta_withNewLocalInstances___main___rarg(x_2, x_48, x_8, x_54, x_10, x_45);
lean_dec(x_48);
return x_57;
lean_object* x_57; lean_object* x_58;
x_57 = lean_ctor_get(x_10, 1);
lean_dec(x_57);
lean_ctor_set(x_10, 1, x_47);
x_58 = l_Lean_Meta_withNewLocalInstances___main___rarg(x_2, x_49, x_8, x_55, x_10, x_45);
lean_dec(x_49);
return x_58;
}
else
{
lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61;
x_58 = lean_ctor_get(x_10, 0);
x_59 = lean_ctor_get(x_10, 2);
lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62;
x_59 = lean_ctor_get(x_10, 0);
x_60 = lean_ctor_get(x_10, 2);
lean_inc(x_60);
lean_inc(x_59);
lean_inc(x_58);
lean_dec(x_10);
x_60 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_60, 0, x_58);
lean_ctor_set(x_60, 1, x_46);
lean_ctor_set(x_60, 2, x_59);
x_61 = l_Lean_Meta_withNewLocalInstances___main___rarg(x_2, x_48, x_8, x_54, x_60, x_45);
lean_dec(x_48);
return x_61;
x_61 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_61, 0, x_59);
lean_ctor_set(x_61, 1, x_47);
lean_ctor_set(x_61, 2, x_60);
x_62 = l_Lean_Meta_withNewLocalInstances___main___rarg(x_2, x_49, x_8, x_55, x_61, x_45);
lean_dec(x_49);
return x_62;
}
}
else
{
lean_dec(x_51);
x_6 = x_46;
x_7 = x_48;
x_9 = x_40;
lean_dec(x_52);
x_6 = x_47;
x_7 = x_49;
x_9 = x_39;
x_11 = x_45;
goto _start;
}
@ -4452,9 +4402,9 @@ goto _start;
}
else
{
lean_object* x_63;
x_63 = lean_box(0);
x_12 = x_63;
lean_object* x_64;
x_64 = lean_box(0);
x_12 = x_64;
goto block_36;
}
block_36:
@ -5094,6 +5044,7 @@ lean_inc(x_19);
lean_dec(x_17);
x_20 = l_Lean_LocalDecl_type(x_18);
lean_dec(x_18);
lean_inc(x_8);
lean_inc(x_20);
x_21 = l_Lean_Meta_isClassQuick___main(x_20, x_8, x_19);
if (lean_obj_tag(x_21) == 0)
@ -5483,6 +5434,7 @@ lean_inc(x_25);
lean_dec(x_23);
x_26 = l_Lean_LocalDecl_type(x_24);
lean_dec(x_24);
lean_inc(x_13);
lean_inc(x_26);
x_27 = l_Lean_Meta_isClassQuick___main(x_26, x_13, x_25);
if (lean_obj_tag(x_27) == 0)
@ -5753,7 +5705,7 @@ _start:
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16;
lean_inc(x_6);
x_11 = lean_expr_mk_fvar(x_6);
x_11 = l_Lean_mkFVar(x_6);
lean_inc(x_3);
x_12 = lean_array_push(x_3, x_11);
x_13 = lean_array_get_size(x_12);
@ -5792,6 +5744,7 @@ lean_inc(x_22);
lean_dec(x_20);
x_23 = l_Lean_LocalDecl_type(x_21);
lean_dec(x_21);
lean_inc(x_9);
lean_inc(x_23);
x_24 = l_Lean_Meta_isClassQuick___main(x_23, x_9, x_22);
if (lean_obj_tag(x_24) == 0)
@ -6054,96 +6007,97 @@ _start:
lean_object* x_11;
if (lean_obj_tag(x_8) == 7)
{
lean_object* x_24; uint8_t x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35;
lean_object* x_24; lean_object* x_25; lean_object* x_26; uint64_t x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
x_24 = lean_ctor_get(x_8, 0);
lean_inc(x_24);
x_25 = lean_ctor_get_uint8(x_8, sizeof(void*)*3);
x_26 = lean_ctor_get(x_8, 1);
x_25 = lean_ctor_get(x_8, 1);
lean_inc(x_25);
x_26 = lean_ctor_get(x_8, 2);
lean_inc(x_26);
x_27 = lean_ctor_get(x_8, 2);
lean_inc(x_27);
x_27 = lean_ctor_get_uint64(x_8, sizeof(void*)*3);
lean_dec(x_8);
x_28 = lean_array_get_size(x_6);
lean_inc(x_6);
x_29 = lean_expr_instantiate_rev_range(x_26, x_7, x_28, x_6);
x_29 = lean_expr_instantiate_rev_range(x_25, x_7, x_28, x_6);
lean_dec(x_28);
lean_dec(x_26);
lean_dec(x_25);
x_30 = l_Lean_Meta_mkFreshId___rarg(x_10);
x_31 = lean_ctor_get(x_30, 0);
lean_inc(x_31);
x_32 = lean_ctor_get(x_30, 1);
lean_inc(x_32);
lean_dec(x_30);
x_33 = (uint8_t)((x_27 << 24) >> 61);
lean_inc(x_31);
x_33 = lean_local_ctx_mk_local_decl(x_5, x_31, x_24, x_29, x_25);
x_34 = lean_local_ctx_mk_local_decl(x_5, x_31, x_24, x_29, x_33);
lean_inc(x_31);
x_34 = lean_expr_mk_fvar(x_31);
x_35 = l_Lean_mkFVar(x_31);
lean_inc(x_6);
x_35 = lean_array_push(x_6, x_34);
x_36 = lean_array_push(x_6, x_35);
if (lean_obj_tag(x_4) == 0)
{
lean_dec(x_31);
lean_dec(x_6);
x_5 = x_33;
x_6 = x_35;
x_8 = x_27;
x_5 = x_34;
x_6 = x_36;
x_8 = x_26;
x_10 = x_32;
goto _start;
}
else
{
lean_object* x_37; lean_object* x_38; uint8_t x_39;
x_37 = lean_ctor_get(x_4, 0);
lean_inc(x_37);
x_38 = lean_array_get_size(x_35);
x_39 = lean_nat_dec_lt(x_38, x_37);
lean_dec(x_37);
lean_object* x_38; lean_object* x_39; uint8_t x_40;
x_38 = lean_ctor_get(x_4, 0);
lean_inc(x_38);
x_39 = lean_array_get_size(x_36);
x_40 = lean_nat_dec_lt(x_39, x_38);
lean_dec(x_38);
if (x_39 == 0)
{
uint8_t x_40;
lean_dec(x_4);
x_40 = !lean_is_exclusive(x_9);
lean_dec(x_39);
if (x_40 == 0)
{
lean_object* x_41; lean_object* x_42;
x_41 = lean_ctor_get(x_9, 1);
lean_dec(x_41);
lean_ctor_set(x_9, 1, x_33);
uint8_t x_41;
lean_dec(x_4);
x_41 = !lean_is_exclusive(x_9);
if (x_41 == 0)
{
lean_object* x_42; lean_object* x_43;
x_42 = lean_ctor_get(x_9, 1);
lean_dec(x_42);
lean_ctor_set(x_9, 1, x_34);
lean_inc(x_7);
x_42 = l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__5___rarg(x_1, x_2, x_6, x_7, x_27, x_31, x_35, x_7, x_9, x_32);
lean_dec(x_35);
lean_dec(x_27);
x_43 = l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__5___rarg(x_1, x_2, x_6, x_7, x_26, x_31, x_36, x_7, x_9, x_32);
lean_dec(x_36);
lean_dec(x_26);
lean_dec(x_7);
return x_42;
return x_43;
}
else
{
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46;
x_43 = lean_ctor_get(x_9, 0);
x_44 = lean_ctor_get(x_9, 2);
lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_44 = lean_ctor_get(x_9, 0);
x_45 = lean_ctor_get(x_9, 2);
lean_inc(x_45);
lean_inc(x_44);
lean_inc(x_43);
lean_dec(x_9);
x_45 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_45, 0, x_43);
lean_ctor_set(x_45, 1, x_33);
lean_ctor_set(x_45, 2, x_44);
x_46 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_46, 0, x_44);
lean_ctor_set(x_46, 1, x_34);
lean_ctor_set(x_46, 2, x_45);
lean_inc(x_7);
x_46 = l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__5___rarg(x_1, x_2, x_6, x_7, x_27, x_31, x_35, x_7, x_45, x_32);
lean_dec(x_35);
lean_dec(x_27);
x_47 = l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__5___rarg(x_1, x_2, x_6, x_7, x_26, x_31, x_36, x_7, x_46, x_32);
lean_dec(x_36);
lean_dec(x_26);
lean_dec(x_7);
return x_46;
return x_47;
}
}
else
{
lean_dec(x_31);
lean_dec(x_6);
x_5 = x_33;
x_6 = x_35;
x_8 = x_27;
x_5 = x_34;
x_6 = x_36;
x_8 = x_26;
x_10 = x_32;
goto _start;
}
@ -6151,9 +6105,9 @@ goto _start;
}
else
{
lean_object* x_48;
x_48 = lean_box(0);
x_11 = x_48;
lean_object* x_49;
x_49 = lean_box(0);
x_11 = x_49;
goto block_23;
}
block_23:
@ -6548,6 +6502,7 @@ lean_object* l_Lean_Meta_isClass(lean_object* x_1, lean_object* x_2, lean_object
_start:
{
lean_object* x_5;
lean_inc(x_3);
lean_inc(x_2);
x_5 = l_Lean_Meta_isClassQuick___main(x_2, x_3, x_4);
if (lean_obj_tag(x_5) == 0)
@ -6667,77 +6622,78 @@ lean_object* x_9;
switch (lean_obj_tag(x_6)) {
case 6:
{
lean_object* x_22; uint8_t x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
lean_object* x_22; lean_object* x_23; lean_object* x_24; uint64_t x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34;
x_22 = lean_ctor_get(x_6, 0);
lean_inc(x_22);
x_23 = lean_ctor_get_uint8(x_6, sizeof(void*)*3);
x_24 = lean_ctor_get(x_6, 1);
x_23 = lean_ctor_get(x_6, 1);
lean_inc(x_23);
x_24 = lean_ctor_get(x_6, 2);
lean_inc(x_24);
x_25 = lean_ctor_get(x_6, 2);
lean_inc(x_25);
x_25 = lean_ctor_get_uint64(x_6, sizeof(void*)*3);
lean_dec(x_6);
x_26 = lean_array_get_size(x_4);
lean_inc(x_4);
x_27 = lean_expr_instantiate_rev_range(x_24, x_5, x_26, x_4);
x_27 = lean_expr_instantiate_rev_range(x_23, x_5, x_26, x_4);
lean_dec(x_26);
lean_dec(x_24);
lean_dec(x_23);
x_28 = l_Lean_Meta_mkFreshId___rarg(x_8);
x_29 = lean_ctor_get(x_28, 0);
lean_inc(x_29);
x_30 = lean_ctor_get(x_28, 1);
lean_inc(x_30);
lean_dec(x_28);
x_31 = (uint8_t)((x_25 << 24) >> 61);
lean_inc(x_29);
x_31 = lean_local_ctx_mk_local_decl(x_3, x_29, x_22, x_27, x_23);
x_32 = lean_expr_mk_fvar(x_29);
x_33 = lean_array_push(x_4, x_32);
x_3 = x_31;
x_4 = x_33;
x_6 = x_25;
x_32 = lean_local_ctx_mk_local_decl(x_3, x_29, x_22, x_27, x_31);
x_33 = l_Lean_mkFVar(x_29);
x_34 = lean_array_push(x_4, x_33);
x_3 = x_32;
x_4 = x_34;
x_6 = x_24;
x_8 = x_30;
goto _start;
}
case 8:
{
lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_35 = lean_ctor_get(x_6, 0);
lean_inc(x_35);
x_36 = lean_ctor_get(x_6, 1);
lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48;
x_36 = lean_ctor_get(x_6, 0);
lean_inc(x_36);
x_37 = lean_ctor_get(x_6, 2);
x_37 = lean_ctor_get(x_6, 1);
lean_inc(x_37);
x_38 = lean_ctor_get(x_6, 3);
x_38 = lean_ctor_get(x_6, 2);
lean_inc(x_38);
x_39 = lean_ctor_get(x_6, 3);
lean_inc(x_39);
lean_dec(x_6);
x_39 = lean_array_get_size(x_4);
x_40 = lean_array_get_size(x_4);
lean_inc(x_4);
x_40 = lean_expr_instantiate_rev_range(x_36, x_5, x_39, x_4);
lean_dec(x_36);
lean_inc(x_4);
x_41 = lean_expr_instantiate_rev_range(x_37, x_5, x_39, x_4);
lean_dec(x_39);
x_41 = lean_expr_instantiate_rev_range(x_37, x_5, x_40, x_4);
lean_dec(x_37);
x_42 = l_Lean_Meta_mkFreshId___rarg(x_8);
x_43 = lean_ctor_get(x_42, 0);
lean_inc(x_43);
x_44 = lean_ctor_get(x_42, 1);
lean_inc(x_4);
x_42 = lean_expr_instantiate_rev_range(x_38, x_5, x_40, x_4);
lean_dec(x_40);
lean_dec(x_38);
x_43 = l_Lean_Meta_mkFreshId___rarg(x_8);
x_44 = lean_ctor_get(x_43, 0);
lean_inc(x_44);
lean_dec(x_42);
lean_inc(x_43);
x_45 = lean_local_ctx_mk_let_decl(x_3, x_43, x_35, x_40, x_41);
x_46 = lean_expr_mk_fvar(x_43);
x_47 = lean_array_push(x_4, x_46);
x_3 = x_45;
x_4 = x_47;
x_6 = x_38;
x_8 = x_44;
x_45 = lean_ctor_get(x_43, 1);
lean_inc(x_45);
lean_dec(x_43);
lean_inc(x_44);
x_46 = lean_local_ctx_mk_let_decl(x_3, x_44, x_36, x_41, x_42);
x_47 = l_Lean_mkFVar(x_44);
x_48 = lean_array_push(x_4, x_47);
x_3 = x_46;
x_4 = x_48;
x_6 = x_39;
x_8 = x_45;
goto _start;
}
default:
{
lean_object* x_49;
x_49 = lean_box(0);
x_9 = x_49;
lean_object* x_50;
x_50 = lean_box(0);
x_9 = x_50;
goto block_21;
}
}
@ -7476,6 +7432,8 @@ l_Lean_Meta_tracer___closed__4 = _init_l_Lean_Meta_tracer___closed__4();
lean_mark_persistent(l_Lean_Meta_tracer___closed__4);
l_Lean_Meta_tracer = _init_l_Lean_Meta_tracer();
lean_mark_persistent(l_Lean_Meta_tracer);
l_Lean_Meta_isClassQuick___main___closed__1 = _init_l_Lean_Meta_isClassQuick___main___closed__1();
lean_mark_persistent(l_Lean_Meta_isClassQuick___main___closed__1);
l_Lean_Meta_isClassExpensive___main___closed__1 = _init_l_Lean_Meta_isClassExpensive___main___closed__1();
lean_mark_persistent(l_Lean_Meta_isClassExpensive___main___closed__1);
return lean_mk_io_result(lean_box(0));

1101
stage0/library/Init/Lean/Meta/Default.c generated
View file

File diff suppressed because it is too large Load diff

4431
stage0/library/Init/Lean/Meta/ExprDefEq.c generated
View file

File diff suppressed because it is too large Load diff

26
stage0/library/Init/Lean/Meta/FunInfo.c generated
View file

@ -16,7 +16,7 @@ extern "C" {
lean_object* l_Lean_Meta_inferTypeAuxAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_foldMAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_expr_has_fvar(lean_object*);
uint8_t l_Lean_Expr_hasFVar(lean_object*);
size_t l_USize_mul(size_t, size_t);
extern lean_object* l_Nat_Inhabited;
lean_object* l_Lean_Meta_getFunInfoAuxAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -25,7 +25,7 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
uint8_t l_Array_contains___at_Lean_Meta_collectDepsAux___main___spec__2(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_findAux___main___at___private_Init_Lean_Meta_FunInfo_1__checkFunInfoCache___spec__2(lean_object*, size_t, lean_object*);
size_t lean_expr_hash(lean_object*);
size_t l_Lean_Expr_hash(lean_object*);
lean_object* l_Lean_Meta_collectDepsAux___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_Meta_collectDeps___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_FunInfo_2__updateHasFwdDeps___boxed(lean_object*, lean_object*);
@ -51,6 +51,7 @@ lean_object* l_Lean_Meta_collectDeps___boxed(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Meta_InferType_1__getForallResultType___closed__1;
lean_object* l___private_Init_Lean_Meta_FunInfo_1__checkFunInfoCache(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t l_USize_add(size_t, size_t);
extern lean_object* l_Lean_Expr_Inhabited;
lean_object* l_Lean_Meta_collectDepsAux___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_qsortAux___main___at_Lean_Meta_collectDeps___spec__1(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
@ -66,7 +67,6 @@ lean_object* l_Lean_Meta_getLocalDecl(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_collectDepsAux(lean_object*, lean_object*, lean_object*);
extern size_t l_PersistentHashMap_insertAux___main___rarg___closed__2;
lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
extern lean_object* l_Lean_Expr_inhabited;
uint8_t l_Array_anyRangeMAux___main___at_Lean_Meta_collectDepsAux___main___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalDecl_type(lean_object*);
size_t l_Option_hash___at_Lean_Meta_InfoCacheKey_Hashable___spec__1(lean_object*);
@ -510,7 +510,7 @@ x_4 = lean_ctor_get_uint8(x_2, sizeof(void*)*2);
x_5 = lean_ctor_get(x_2, 0);
x_6 = lean_ctor_get(x_2, 1);
x_7 = l_Lean_Meta_TransparencyMode_hash(x_4);
x_8 = lean_expr_hash(x_5);
x_8 = l_Lean_Expr_hash(x_5);
x_9 = l_Option_hash___at_Lean_Meta_InfoCacheKey_Hashable___spec__1(x_6);
x_10 = lean_usize_mix_hash(x_8, x_9);
x_11 = lean_usize_mix_hash(x_7, x_10);
@ -750,7 +750,7 @@ lean_inc(x_18);
x_19 = lean_ctor_get(x_9, 1);
lean_inc(x_19);
x_20 = l_Lean_Meta_TransparencyMode_hash(x_17);
x_21 = lean_expr_hash(x_18);
x_21 = l_Lean_Expr_hash(x_18);
lean_dec(x_18);
x_22 = l_Option_hash___at_Lean_Meta_InfoCacheKey_Hashable___spec__1(x_19);
lean_dec(x_19);
@ -1510,7 +1510,7 @@ lean_inc(x_11);
x_12 = lean_ctor_get(x_2, 1);
lean_inc(x_12);
x_13 = l_Lean_Meta_TransparencyMode_hash(x_10);
x_14 = lean_expr_hash(x_11);
x_14 = l_Lean_Expr_hash(x_11);
lean_dec(x_11);
x_15 = l_Option_hash___at_Lean_Meta_InfoCacheKey_Hashable___spec__1(x_12);
lean_dec(x_12);
@ -1539,7 +1539,7 @@ lean_inc(x_25);
x_26 = lean_ctor_get(x_2, 1);
lean_inc(x_26);
x_27 = l_Lean_Meta_TransparencyMode_hash(x_24);
x_28 = lean_expr_hash(x_25);
x_28 = l_Lean_Expr_hash(x_25);
lean_dec(x_25);
x_29 = l_Option_hash___at_Lean_Meta_InfoCacheKey_Hashable___spec__1(x_26);
lean_dec(x_26);
@ -1837,7 +1837,7 @@ lean_object* l_Lean_Meta_whenHasVar___rarg(lean_object* x_1, lean_object* x_2, l
_start:
{
uint8_t x_4;
x_4 = lean_expr_has_fvar(x_1);
x_4 = l_Lean_Expr_hasFVar(x_1);
if (x_4 == 0)
{
lean_dec(x_3);
@ -1991,7 +1991,7 @@ case 5:
lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_9 = lean_ctor_get(x_2, 0);
x_10 = lean_ctor_get(x_2, 1);
x_11 = lean_expr_has_fvar(x_2);
x_11 = l_Lean_Expr_hasFVar(x_2);
if (x_11 == 0)
{
return x_3;
@ -2010,7 +2010,7 @@ case 6:
lean_object* x_14; lean_object* x_15; uint8_t x_16;
x_14 = lean_ctor_get(x_2, 1);
x_15 = lean_ctor_get(x_2, 2);
x_16 = lean_expr_has_fvar(x_2);
x_16 = l_Lean_Expr_hasFVar(x_2);
if (x_16 == 0)
{
return x_3;
@ -2029,7 +2029,7 @@ case 7:
lean_object* x_19; lean_object* x_20; uint8_t x_21;
x_19 = lean_ctor_get(x_2, 1);
x_20 = lean_ctor_get(x_2, 2);
x_21 = lean_expr_has_fvar(x_2);
x_21 = l_Lean_Expr_hasFVar(x_2);
if (x_21 == 0)
{
return x_3;
@ -2049,7 +2049,7 @@ lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27;
x_24 = lean_ctor_get(x_2, 1);
x_25 = lean_ctor_get(x_2, 2);
x_26 = lean_ctor_get(x_2, 3);
x_27 = lean_expr_has_fvar(x_2);
x_27 = l_Lean_Expr_hasFVar(x_2);
if (x_27 == 0)
{
return x_3;
@ -2499,7 +2499,7 @@ lean_object* l_Lean_Meta_getFunInfoAuxAux___lambda__1(lean_object* x_1, lean_obj
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_7 = l_Lean_Expr_inhabited;
x_7 = l_Lean_Expr_Inhabited;
x_8 = lean_array_get(x_7, x_1, x_3);
x_9 = l_Lean_Expr_fvarId_x21(x_8);
lean_dec(x_8);

582
stage0/library/Init/Lean/Meta/InferType.c generated
View file

File diff suppressed because it is too large Load diff

29476
stage0/library/Init/Lean/MetavarContext.c generated
View file

File diff suppressed because it is too large Load diff

14
stage0/library/Init/Lean/Parser/Parser.c generated
View file

@ -127,6 +127,7 @@ lean_object* l_Lean_Parser_ParserAttribute_runParser(lean_object*, lean_object*,
lean_object* l_Lean_Parser_runBuiltinParser___rarg___boxed(lean_object*);
lean_object* l_List_hasDecEq___main___at_Lean_Parser_Error_toString___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkParserContextCore___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
lean_object* l_Lean_Parser_takeUntilFn___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_binNumberFn___spec__3___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_strLitFnAux___boxed(lean_object*, lean_object*, lean_object*);
@ -165,7 +166,6 @@ lean_object* l___private_Init_Lean_Parser_Parser_5__tokenFnAux(lean_object*, lea
lean_object* l_Lean_Syntax_getOptional(lean_object*);
lean_object* l_Lean_Parser_initCacheForInput(lean_object*);
lean_object* l_Lean_Parser_rawFn___boxed(lean_object*);
lean_object* lean_expr_mk_app(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Environment_5__envExtensionsRef;
lean_object* l_Lean_Parser_TokenTableAttribute_inhabited___closed__4;
lean_object* l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_whitespace___main___spec__1(lean_object*, lean_object*);
@ -237,6 +237,7 @@ lean_object* l_List_foldl___main___at_Lean_Parser_addBuiltinLeadingParser___spec
lean_object* l_Lean_Syntax_isNone(lean_object*);
lean_object* l_Lean_Parser_getSyntaxNodeKinds(lean_object*);
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main(uint8_t, lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_Parser_checkWsBeforeFn___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_takeUntilFn___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Options_empty;
@ -330,7 +331,6 @@ lean_object* l_Lean_AttributeImpl_inhabited___lambda__5(lean_object*, lean_objec
lean_object* l_Lean_Parser_currLbp___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_symbolNoWsFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_ParserState_mkEOIError___closed__1;
lean_object* lean_expr_mk_const(lean_object*, lean_object*);
lean_object* l_Lean_Parser_hashOrelse___boxed(lean_object*);
lean_object* l_Lean_Syntax_mfoldArgsAux___main___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_symbolNoWsInfo___elambda__2(lean_object*, lean_object*, lean_object*);
@ -26628,7 +26628,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Init_Lean_Compiler_InitAttr_1__getIOTypeArg___closed__2;
x_3 = lean_expr_mk_const(x_2, x_1);
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
@ -26638,7 +26638,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Init_Lean_Compiler_InitAttr_2__isUnitType___closed__2;
x_3 = lean_expr_mk_const(x_2, x_1);
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
@ -26648,7 +26648,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_declareBuiltinParser___closed__3;
x_2 = l_Lean_Parser_declareBuiltinParser___closed__4;
x_3 = lean_expr_mk_app(x_1, x_2);
x_3 = l_Lean_mkApp(x_1, x_2);
return x_3;
}
}
@ -26677,11 +26677,11 @@ x_6 = l_Lean_Parser_declareBuiltinParser___closed__2;
lean_inc(x_4);
x_7 = l_Lean_Name_append___main(x_6, x_4);
x_8 = lean_box(0);
x_9 = lean_expr_mk_const(x_3, x_8);
x_9 = l_Lean_mkConst(x_3, x_8);
lean_inc(x_4);
x_10 = l_Lean_nameToExprAux___main(x_4);
lean_inc(x_4);
x_11 = lean_expr_mk_const(x_4, x_8);
x_11 = l_Lean_mkConst(x_4, x_8);
x_12 = l_Lean_Parser_declareBuiltinParser___closed__6;
x_13 = lean_array_push(x_12, x_9);
x_14 = lean_array_push(x_13, x_10);

4
stage0/library/Init/Lean/ToExpr.c generated
View file

@ -17,7 +17,7 @@ lean_object* l_Lean_strToExpr;
lean_object* l_Lean_mkStrLit(lean_object*);
lean_object* l_Lean_nameToExprAux___main___closed__3;
lean_object* l_Lean_nameToExprAux___main___closed__1;
lean_object* lean_expr_mk_const(lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_nameToExprAux___main___closed__7;
lean_object* l_Lean_nameToExprAux___main___closed__8;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
@ -171,7 +171,7 @@ x_5 = lean_name_mk_string(x_3, x_4);
x_6 = l_Lean_nameToExprAux___main___closed__3;
x_7 = lean_name_mk_string(x_5, x_6);
x_8 = lean_box(0);
x_9 = lean_expr_mk_const(x_7, x_8);
x_9 = l_Lean_mkConst(x_7, x_8);
return x_9;
}
case 1:

4
stage0/library/Init/Lean/TypeClass/Basic.c generated
View file

@ -15,12 +15,12 @@ extern "C" {
#endif
extern lean_object* l_Array_empty___closed__1;
extern lean_object* l_PersistentHashMap_empty___rarg___closed__2;
extern lean_object* l_Lean_Expr_Inhabited___closed__1;
lean_object* l_Lean_TypeClass_synthCommand___closed__1;
lean_object* l_PersistentHashMap_empty___at_Lean_TypeClass_synthCommand___spec__1___closed__1;
lean_object* l_PersistentHashMap_empty___at_Lean_TypeClass_synthCommand___spec__1;
lean_object* l_Queue_empty(lean_object*);
lean_object* l_Lean_TypeClass_synth(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_inhabited___closed__1;
lean_object* lean_typeclass_synth_command(lean_object*, lean_object*);
lean_object* _init_l_PersistentHashMap_empty___at_Lean_TypeClass_synthCommand___spec__1___closed__1() {
_start:
@ -55,7 +55,7 @@ _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 = lean_box(0);
x_4 = l_Lean_Expr_inhabited___closed__1;
x_4 = l_Lean_Expr_Inhabited___closed__1;
x_5 = l_Array_empty___closed__1;
x_6 = l_Lean_TypeClass_synthCommand___closed__1;
x_7 = l_PersistentHashMap_empty___at_Lean_TypeClass_synthCommand___spec__1;

680
stage0/library/Init/Lean/TypeClass/Context.c generated
View file

File diff suppressed because it is too large Load diff

279
stage0/library/Init/Lean/TypeClass/Synth.c generated
View file

@ -28,7 +28,7 @@ lean_object* l_Lean_TypeClass_synthCore___rarg(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_findAux___main___at_Lean_TypeClass_newAnswer___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_synthCore___main(lean_object*, lean_object*);
lean_object* lean_mk_array(lean_object*, lean_object*);
size_t lean_expr_hash(lean_object*);
size_t l_Lean_Expr_hash(lean_object*);
lean_object* l_Array_back___at_Lean_TypeClass_consume___spec__2___boxed(lean_object*);
lean_object* l_PersistentHashMap_find___at_Lean_TypeClass_newAnswer___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_ConsumerNode_Inhabited;
@ -37,12 +37,13 @@ lean_object* l_Lean_TypeClass_Context__u03b1Norm(lean_object*);
lean_object* lean_expr_dbg_to_string(lean_object*);
lean_object* l_Lean_TypeClass_collectEReplacements___main___closed__5;
lean_object* l_Array_iterateMAux___main___at_Lean_TypeClass_consume___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
lean_object* l_Queue_enqueue___rarg(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_collectEReplacements___main___closed__3;
lean_object* l_Lean_TypeClass_introduceLocals___main___closed__2;
extern lean_object* l_Lean_Expr_Inhabited___closed__1;
lean_object* l_Lean_TypeClass_newAnswer(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_synthCore___main___closed__1;
lean_object* lean_expr_mk_app(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_wakeUp(lean_object*, lean_object*, lean_object*);
size_t l_USize_sub(size_t, size_t);
lean_object* lean_expr_instantiate1(lean_object*, lean_object*);
@ -59,6 +60,7 @@ lean_object* l_Stack_pop___at_Lean_TypeClass_consume___spec__3(lean_object*);
lean_object* l_Lean_TypeClass_TypedExpr_HasToString___boxed(lean_object*);
lean_object* l_Lean_TypeClass_TypedExpr_HasToString___closed__1;
extern lean_object* l_Lean_formatDataValue___closed__1;
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_TypedExpr_Inhabited;
lean_object* l_Lean_Expr_getAppNumArgsAux___main(lean_object*, lean_object*);
lean_object* l_Array_forMAux___main___at_Lean_TypeClass_newAnswer___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
@ -73,7 +75,6 @@ extern lean_object* l_Lean_TypeClass_Context_Inhabited___closed__1;
lean_object* l_Lean_TypeClass_constNameToTypedExpr___closed__1;
lean_object* l_Lean_Expr_constLevels_x21(lean_object*);
lean_object* l_Lean_TypeClass_synthCore___boxed(lean_object*, lean_object*);
lean_object* lean_expr_mk_fvar(lean_object*);
lean_object* lean_local_ctx_mk_local_decl(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_Expr_constName_x21(lean_object*);
lean_object* l_Lean_LocalContext_mkLambda(lean_object*, lean_object*, lean_object*);
@ -84,7 +85,6 @@ lean_object* l_PersistentHashMap_insertAux___main___at_Lean_TypeClass_newSubgoal
lean_object* l_PersistentHashMap_mkCollisionNode___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Node_Inhabited___closed__1;
extern lean_object* l_Lean_TypeClass_Context_Inhabited;
lean_object* lean_expr_mk_const(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_constNameToTypedExpr(lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_TypeClass_newAnswer___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_expr_eqv(lean_object*, lean_object*);
@ -100,12 +100,14 @@ lean_object* lean_string_append(lean_object*, lean_object*);
extern lean_object* l_Lean_mkOptionalNode___rarg___closed__1;
extern lean_object* l_List_reprAux___main___rarg___closed__1;
size_t l_USize_add(size_t, size_t);
extern lean_object* l_Lean_Expr_Inhabited;
lean_object* l_Lean_TypeClass_introduceLocals___main(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_introduceLocals___main___closed__1;
uint8_t l_Lean_TypeClass_Context_eHasTmpMVar(lean_object*);
extern lean_object* l_Option_HasRepr___rarg___closed__3;
uint8_t l_Lean_TypeClass_Waiter_isRoot(lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_mkFVar(lean_object*);
lean_object* l_Lean_TypeClass_collectEReplacements(lean_object*);
lean_object* l_List_append___rarg(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
@ -132,7 +134,6 @@ lean_object* l___private_Init_Util_1__mkPanicMessage(lean_object*, lean_object*,
lean_object* l_Lean_TypeClass_collectUReplacements(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Answer_HasToString___closed__1;
lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main___at_Lean_TypeClass_newSubgoal___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_inhabited;
uint8_t l_Array_anyRangeMAux___main___at_Lean_TypeClass_newAnswer___spec__6(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentHashMap_find___at_Lean_TypeClass_newAnswer___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_newSubgoal___closed__2;
@ -144,6 +145,7 @@ lean_object* l_panic(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_newConsumerNode(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eInstantiate___main(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_generate___closed__1;
lean_object* l___private_Init_Lean_Expr_3__getAppArgsAux___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_introduceMVars___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_pop(lean_object*);
lean_object* lean_instantiate_type_lparams(lean_object*, lean_object*);
@ -166,11 +168,12 @@ lean_object* l_Lean_TypeClass_Context_eUnify___main(lean_object*, lean_object*,
lean_object* l_Lean_TypeClass_synth(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_TypedExpr_HasToString(lean_object*);
extern lean_object* l_Lean_Expr_getAppArgs___closed__1;
lean_object* l_Stack_peek_x21___at_Lean_TypeClass_consume___spec__1___boxed(lean_object*);
extern lean_object* l_Lean_Expr_inhabited___closed__1;
lean_object* l_Stack_modify___at_Lean_TypeClass_generate___spec__4(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_introduceMVars___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_collectEReplacements___main___closed__4;
uint8_t l_Lean_Expr_hasMVar(lean_object*);
lean_object* l_Stack_pop___at_Lean_TypeClass_generate___spec__3(lean_object*);
lean_object* l_Lean_TypeClass_generate___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_newSubgoal___closed__1;
@ -181,14 +184,12 @@ lean_object* l_Lean_TypeClass_resume(lean_object*);
lean_object* l_Lean_TypeClass_collectUReplacements___main(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_newAnswer___closed__1;
lean_object* l_Lean_TypeClass_Answer_HasToString___boxed(lean_object*);
uint8_t lean_expr_has_expr_mvar(lean_object*);
lean_object* l_List_foldl___main___at_Lean_TypeClass_constNameToTypedExpr___spec__1(lean_object*, lean_object*);
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_back___at_Lean_TypeClass_consume___spec__2(lean_object*);
lean_object* l_Lean_TypeClass_quickIsClass(lean_object*, lean_object*);
size_t l_USize_land(size_t, size_t);
lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Expr_4__getAppArgsAux___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_newAnswer___closed__2;
lean_object* l_Lean_TypeClass_GeneratorNode_Inhabited___closed__1;
lean_object* lean_usize_to_nat(size_t);
@ -202,7 +203,7 @@ lean_object* l_Array_back___at_Lean_TypeClass_generate___spec__2___boxed(lean_ob
lean_object* l_Lean_TypeClass_synth___closed__3;
lean_object* l_Lean_TypeClass_constNameToTypedExpr___closed__2;
lean_object* l_Array_anyRangeMAux___main___at_Lean_TypeClass_newAnswer___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_expr_has_level_mvar(lean_object*);
uint8_t l_Lean_Expr_CachedData_binderInfo(uint64_t);
uint8_t l_Lean_Expr_isLambda(lean_object*);
lean_object* _init_l_Lean_TypeClass_TypedExpr_HasToString___closed__1() {
_start:
@ -245,7 +246,7 @@ lean_object* _init_l_Lean_TypeClass_TypedExpr_Inhabited___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Expr_inhabited___closed__1;
x_1 = l_Lean_Expr_Inhabited___closed__1;
x_2 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_2, 0, x_1);
lean_ctor_set(x_2, 1, x_1);
@ -310,7 +311,7 @@ lean_object* _init_l_Lean_TypeClass_Node_Inhabited___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Expr_inhabited___closed__1;
x_1 = l_Lean_Expr_Inhabited___closed__1;
x_2 = l_Lean_TypeClass_Context_Inhabited___closed__1;
x_3 = l_Lean_TypeClass_TypedExpr_Inhabited___closed__1;
x_4 = lean_alloc_ctor(0, 3, 0);
@ -705,7 +706,7 @@ else
lean_object* x_9; lean_object* x_10; size_t x_11; size_t x_12; size_t x_13; size_t x_14; size_t x_15; size_t x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_9 = lean_array_fget(x_4, x_5);
x_10 = lean_array_fget(x_3, x_5);
x_11 = lean_expr_hash(x_9);
x_11 = l_Lean_Expr_hash(x_9);
x_12 = 1;
x_13 = x_1 - x_12;
x_14 = 5;
@ -1044,7 +1045,7 @@ if (x_4 == 0)
lean_object* x_5; lean_object* x_6; size_t x_7; size_t x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_5 = lean_ctor_get(x_1, 0);
x_6 = lean_ctor_get(x_1, 1);
x_7 = lean_expr_hash(x_2);
x_7 = l_Lean_Expr_hash(x_2);
x_8 = 1;
x_9 = l_PersistentHashMap_insertAux___main___at_Lean_TypeClass_newSubgoal___spec__3(x_5, x_7, x_8, x_2, x_3);
x_10 = lean_unsigned_to_nat(1u);
@ -1062,7 +1063,7 @@ x_13 = lean_ctor_get(x_1, 1);
lean_inc(x_13);
lean_inc(x_12);
lean_dec(x_1);
x_14 = lean_expr_hash(x_2);
x_14 = l_Lean_Expr_hash(x_2);
x_15 = 1;
x_16 = l_PersistentHashMap_insertAux___main___at_Lean_TypeClass_newSubgoal___spec__3(x_12, x_14, x_15, x_2, x_3);
x_17 = lean_unsigned_to_nat(1u);
@ -1338,58 +1339,59 @@ _start:
lean_object* x_7;
if (lean_obj_tag(x_5) == 7)
{
uint8_t x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_12 = lean_ctor_get_uint8(x_5, sizeof(void*)*3);
x_13 = lean_ctor_get(x_5, 1);
lean_object* x_12; lean_object* x_13; uint64_t x_14; uint8_t x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_12 = lean_ctor_get(x_5, 1);
lean_inc(x_12);
x_13 = lean_ctor_get(x_5, 2);
lean_inc(x_13);
x_14 = lean_ctor_get(x_5, 2);
lean_inc(x_14);
x_14 = lean_ctor_get_uint64(x_5, sizeof(void*)*3);
lean_dec(x_5);
x_15 = (uint8_t)((x_14 << 24) >> 61);
lean_inc(x_1);
x_15 = l_Lean_LocalContext_mkForall(x_1, x_2, x_13);
lean_dec(x_13);
x_16 = l_Lean_TypeClass_Context_eNewMeta(x_15, x_3);
x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
x_18 = lean_ctor_get(x_16, 1);
x_16 = l_Lean_LocalContext_mkForall(x_1, x_2, x_12);
lean_dec(x_12);
x_17 = l_Lean_TypeClass_Context_eNewMeta(x_16, x_3);
x_18 = lean_ctor_get(x_17, 0);
lean_inc(x_18);
lean_dec(x_16);
x_19 = lean_unsigned_to_nat(0u);
lean_inc(x_17);
x_20 = l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(x_2, x_2, x_19, x_17);
lean_inc(x_20);
x_21 = lean_expr_mk_app(x_4, x_20);
x_22 = lean_expr_instantiate1(x_14, x_20);
lean_dec(x_20);
lean_dec(x_14);
x_23 = l_Lean_BinderInfo_isInstImplicit(x_12);
if (x_23 == 0)
{
x_19 = lean_ctor_get(x_17, 1);
lean_inc(x_19);
lean_dec(x_17);
x_3 = x_18;
x_4 = x_21;
x_5 = x_22;
x_20 = lean_unsigned_to_nat(0u);
lean_inc(x_18);
x_21 = l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(x_2, x_2, x_20, x_18);
lean_inc(x_21);
x_22 = l_Lean_mkApp(x_4, x_21);
x_23 = lean_expr_instantiate1(x_13, x_21);
lean_dec(x_21);
lean_dec(x_13);
x_24 = l_Lean_BinderInfo_isInstImplicit(x_15);
if (x_24 == 0)
{
lean_dec(x_18);
x_3 = x_19;
x_4 = x_22;
x_5 = x_23;
goto _start;
}
else
{
lean_object* x_25;
x_25 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_25, 0, x_17);
lean_ctor_set(x_25, 1, x_6);
x_3 = x_18;
x_4 = x_21;
x_5 = x_22;
x_6 = x_25;
lean_object* x_26;
x_26 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_26, 0, x_18);
lean_ctor_set(x_26, 1, x_6);
x_3 = x_19;
x_4 = x_22;
x_5 = x_23;
x_6 = x_26;
goto _start;
}
}
else
{
lean_object* x_27;
lean_object* x_28;
lean_dec(x_1);
x_27 = lean_box(0);
x_7 = x_27;
x_28 = lean_box(0);
x_7 = x_28;
goto block_11;
}
block_11:
@ -1458,46 +1460,47 @@ _start:
{
if (lean_obj_tag(x_4) == 7)
{
lean_object* x_5; uint8_t x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
lean_object* x_5; lean_object* x_6; lean_object* x_7; uint64_t x_8; uint8_t x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_5 = lean_ctor_get(x_4, 0);
lean_inc(x_5);
x_6 = lean_ctor_get_uint8(x_4, sizeof(void*)*3);
x_7 = lean_ctor_get(x_4, 1);
x_6 = lean_ctor_get(x_4, 1);
lean_inc(x_6);
x_7 = lean_ctor_get(x_4, 2);
lean_inc(x_7);
x_8 = lean_ctor_get(x_4, 2);
lean_inc(x_8);
x_8 = lean_ctor_get_uint64(x_4, sizeof(void*)*3);
lean_dec(x_4);
x_9 = l_Lean_TypeClass_introduceLocals___main___closed__2;
x_9 = (uint8_t)((x_8 << 24) >> 61);
x_10 = l_Lean_TypeClass_introduceLocals___main___closed__2;
lean_inc(x_1);
x_10 = lean_name_mk_numeral(x_9, x_1);
lean_inc(x_10);
x_11 = lean_local_ctx_mk_local_decl(x_2, x_10, x_5, x_7, x_6);
x_12 = lean_expr_mk_fvar(x_10);
x_13 = lean_unsigned_to_nat(1u);
x_14 = lean_nat_add(x_1, x_13);
x_11 = lean_name_mk_numeral(x_10, x_1);
lean_inc(x_11);
x_12 = lean_local_ctx_mk_local_decl(x_2, x_11, x_5, x_6, x_9);
x_13 = l_Lean_mkFVar(x_11);
x_14 = lean_unsigned_to_nat(1u);
x_15 = lean_nat_add(x_1, x_14);
lean_dec(x_1);
lean_inc(x_12);
x_15 = lean_array_push(x_3, x_12);
x_16 = lean_expr_instantiate1(x_8, x_12);
lean_dec(x_12);
lean_dec(x_8);
x_1 = x_14;
x_2 = x_11;
x_3 = x_15;
x_4 = x_16;
lean_inc(x_13);
x_16 = lean_array_push(x_3, x_13);
x_17 = lean_expr_instantiate1(x_7, x_13);
lean_dec(x_13);
lean_dec(x_7);
x_1 = x_15;
x_2 = x_12;
x_3 = x_16;
x_4 = x_17;
goto _start;
}
else
{
lean_object* x_18; lean_object* x_19;
lean_object* x_19; lean_object* x_20;
lean_dec(x_1);
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_4);
lean_ctor_set(x_18, 1, x_3);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_2);
lean_ctor_set(x_19, 1, x_18);
return x_19;
lean_ctor_set(x_19, 0, x_4);
lean_ctor_set(x_19, 1, x_3);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_2);
lean_ctor_set(x_20, 1, x_19);
return x_20;
}
}
}
@ -2406,7 +2409,7 @@ _start:
{
lean_object* x_3; size_t x_4; lean_object* x_5;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_expr_hash(x_2);
x_4 = l_Lean_Expr_hash(x_2);
x_5 = l_PersistentHashMap_findAux___main___at_Lean_TypeClass_newAnswer___spec__2(x_3, x_4, x_2);
return x_5;
}
@ -3367,7 +3370,7 @@ if (x_18 == 0)
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_19 = lean_ctor_get(x_17, 0);
lean_inc(x_19);
x_20 = lean_expr_mk_const(x_2, x_19);
x_20 = l_Lean_mkConst(x_2, x_19);
x_21 = lean_instantiate_type_lparams(x_13, x_19);
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_20);
@ -3387,7 +3390,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_dec(x_17);
lean_inc(x_24);
x_26 = lean_expr_mk_const(x_2, x_24);
x_26 = l_Lean_mkConst(x_2, x_24);
x_27 = lean_instantiate_type_lparams(x_13, x_24);
x_28 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_28, 0, x_26);
@ -4168,7 +4171,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_TypeClass_collectEReplacements___main___closed__3;
x_2 = lean_unsigned_to_nat(287u);
x_2 = lean_unsigned_to_nat(289u);
x_3 = lean_unsigned_to_nat(27u);
x_4 = l_Lean_TypeClass_collectEReplacements___main___closed__4;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -4362,7 +4365,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_TypeClass_collectEReplacements___main___closed__3;
x_2 = lean_unsigned_to_nat(303u);
x_2 = lean_unsigned_to_nat(305u);
x_3 = lean_unsigned_to_nat(16u);
x_4 = l_Lean_TypeClass_preprocessForOutParams___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -4373,44 +4376,49 @@ lean_object* l_Lean_TypeClass_preprocessForOutParams(lean_object* x_1, lean_obje
_start:
{
lean_object* x_3; uint8_t x_267;
x_267 = lean_expr_has_expr_mvar(x_2);
x_267 = l_Lean_Expr_hasMVar(x_2);
if (x_267 == 0)
{
uint8_t x_268;
x_268 = lean_expr_has_level_mvar(x_2);
if (x_268 == 0)
lean_object* x_268; uint8_t x_269;
x_268 = l_Lean_Expr_getAppFn___main(x_2);
x_269 = l_Lean_Expr_isConst(x_268);
if (x_269 == 0)
{
lean_object* x_269; uint8_t x_270;
x_269 = l_Lean_Expr_getAppFn___main(x_2);
x_270 = l_Lean_Expr_isConst(x_269);
if (x_270 == 0)
{
lean_object* x_271;
lean_dec(x_269);
x_271 = lean_box(0);
x_3 = x_271;
lean_object* x_270;
lean_dec(x_268);
x_270 = lean_box(0);
x_3 = x_270;
goto block_266;
}
else
{
lean_object* x_272; uint8_t x_273;
x_272 = l_Lean_Expr_constName_x21(x_269);
lean_dec(x_269);
lean_object* x_271; uint8_t x_272;
x_271 = l_Lean_Expr_constName_x21(x_268);
lean_dec(x_268);
lean_inc(x_1);
x_273 = lean_has_out_params(x_1, x_272);
if (x_273 == 0)
x_272 = lean_has_out_params(x_1, x_271);
if (x_272 == 0)
{
lean_object* x_274; lean_object* x_275; lean_object* x_276; lean_object* x_277;
lean_object* x_273; lean_object* x_274; lean_object* x_275; lean_object* x_276;
lean_dec(x_1);
x_274 = l_Lean_TypeClass_collectEReplacements___main___closed__1;
x_275 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_275, 0, x_2);
lean_ctor_set(x_275, 1, x_274);
x_276 = l_Lean_TypeClass_Context_Inhabited___closed__1;
x_277 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_277, 0, x_276);
lean_ctor_set(x_277, 1, x_275);
return x_277;
x_273 = l_Lean_TypeClass_collectEReplacements___main___closed__1;
x_274 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_274, 0, x_2);
lean_ctor_set(x_274, 1, x_273);
x_275 = l_Lean_TypeClass_Context_Inhabited___closed__1;
x_276 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_276, 0, x_275);
lean_ctor_set(x_276, 1, x_274);
return x_276;
}
else
{
lean_object* x_277;
x_277 = lean_box(0);
x_3 = x_277;
goto block_266;
}
}
}
else
{
@ -4419,23 +4427,6 @@ x_278 = lean_box(0);
x_3 = x_278;
goto block_266;
}
}
}
else
{
lean_object* x_279;
x_279 = lean_box(0);
x_3 = x_279;
goto block_266;
}
}
else
{
lean_object* x_280;
x_280 = lean_box(0);
x_3 = x_280;
goto block_266;
}
block_266:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8;
@ -4460,14 +4451,14 @@ x_13 = lean_ctor_get(x_9, 0);
lean_dec(x_13);
x_14 = l_Lean_Expr_getAppFn___main(x_2);
x_15 = l_Lean_Expr_getAppNumArgsAux___main(x_2, x_4);
x_16 = l_Lean_Expr_inhabited___closed__1;
x_16 = l_Lean_Expr_getAppArgs___closed__1;
lean_inc(x_15);
x_17 = lean_mk_array(x_15, x_16);
x_18 = lean_unsigned_to_nat(1u);
x_19 = lean_nat_sub(x_15, x_18);
lean_dec(x_15);
lean_inc(x_2);
x_20 = l___private_Init_Lean_Expr_4__getAppArgsAux___main(x_2, x_17, x_19);
x_20 = l___private_Init_Lean_Expr_3__getAppArgsAux___main(x_2, x_17, x_19);
x_21 = l_Lean_Expr_isConst(x_14);
if (x_21 == 0)
{
@ -4543,14 +4534,14 @@ lean_dec(x_14);
x_38 = l_Array_toList___rarg(x_34);
lean_dec(x_34);
lean_inc(x_38);
x_39 = lean_expr_mk_const(x_24, x_38);
x_39 = l_Lean_mkConst(x_24, x_38);
x_40 = l_Lean_Expr_constName_x21(x_39);
x_41 = lean_environment_find(x_1, x_40);
if (lean_obj_tag(x_41) == 0)
{
lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73;
lean_dec(x_38);
x_70 = l_Lean_Expr_inhabited;
x_70 = l_Lean_Expr_Inhabited;
x_71 = l_Lean_TypeClass_preprocessForOutParams___closed__2;
x_72 = lean_panic_fn(x_71);
lean_inc(x_11);
@ -4685,7 +4676,7 @@ if (lean_obj_tag(x_77) == 0)
{
lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109;
lean_dec(x_34);
x_106 = l_Lean_Expr_inhabited;
x_106 = l_Lean_Expr_Inhabited;
x_107 = l_Lean_TypeClass_preprocessForOutParams___closed__2;
x_108 = lean_panic_fn(x_107);
lean_inc(x_11);
@ -4826,14 +4817,14 @@ lean_inc(x_115);
lean_dec(x_9);
x_116 = l_Lean_Expr_getAppFn___main(x_2);
x_117 = l_Lean_Expr_getAppNumArgsAux___main(x_2, x_4);
x_118 = l_Lean_Expr_inhabited___closed__1;
x_118 = l_Lean_Expr_getAppArgs___closed__1;
lean_inc(x_117);
x_119 = lean_mk_array(x_117, x_118);
x_120 = lean_unsigned_to_nat(1u);
x_121 = lean_nat_sub(x_117, x_120);
lean_dec(x_117);
lean_inc(x_2);
x_122 = l___private_Init_Lean_Expr_4__getAppArgsAux___main(x_2, x_119, x_121);
x_122 = l___private_Init_Lean_Expr_3__getAppArgsAux___main(x_2, x_119, x_121);
x_123 = l_Lean_Expr_isConst(x_116);
if (x_123 == 0)
{
@ -4912,14 +4903,14 @@ lean_dec(x_116);
x_142 = l_Array_toList___rarg(x_138);
lean_dec(x_138);
lean_inc(x_142);
x_143 = lean_expr_mk_const(x_127, x_142);
x_143 = l_Lean_mkConst(x_127, x_142);
x_144 = l_Lean_Expr_constName_x21(x_143);
x_145 = lean_environment_find(x_1, x_144);
if (lean_obj_tag(x_145) == 0)
{
lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162;
lean_dec(x_142);
x_159 = l_Lean_Expr_inhabited;
x_159 = l_Lean_Expr_Inhabited;
x_160 = l_Lean_TypeClass_preprocessForOutParams___closed__2;
x_161 = lean_panic_fn(x_160);
lean_inc(x_114);
@ -5003,7 +4994,7 @@ if (lean_obj_tag(x_166) == 0)
{
lean_object* x_180; lean_object* x_181; lean_object* x_182; lean_object* x_183;
lean_dec(x_138);
x_180 = l_Lean_Expr_inhabited;
x_180 = l_Lean_Expr_Inhabited;
x_181 = l_Lean_TypeClass_preprocessForOutParams___closed__2;
x_182 = lean_panic_fn(x_181);
lean_inc(x_114);
@ -5105,14 +5096,14 @@ if (lean_is_exclusive(x_188)) {
}
x_192 = l_Lean_Expr_getAppFn___main(x_2);
x_193 = l_Lean_Expr_getAppNumArgsAux___main(x_2, x_4);
x_194 = l_Lean_Expr_inhabited___closed__1;
x_194 = l_Lean_Expr_getAppArgs___closed__1;
lean_inc(x_193);
x_195 = lean_mk_array(x_193, x_194);
x_196 = lean_unsigned_to_nat(1u);
x_197 = lean_nat_sub(x_193, x_196);
lean_dec(x_193);
lean_inc(x_2);
x_198 = l___private_Init_Lean_Expr_4__getAppArgsAux___main(x_2, x_195, x_197);
x_198 = l___private_Init_Lean_Expr_3__getAppArgsAux___main(x_2, x_195, x_197);
x_199 = l_Lean_Expr_isConst(x_192);
if (x_199 == 0)
{
@ -5201,14 +5192,14 @@ lean_dec(x_192);
x_220 = l_Array_toList___rarg(x_216);
lean_dec(x_216);
lean_inc(x_220);
x_221 = lean_expr_mk_const(x_204, x_220);
x_221 = l_Lean_mkConst(x_204, x_220);
x_222 = l_Lean_Expr_constName_x21(x_221);
x_223 = lean_environment_find(x_1, x_222);
if (lean_obj_tag(x_223) == 0)
{
lean_object* x_237; lean_object* x_238; lean_object* x_239; lean_object* x_240;
lean_dec(x_220);
x_237 = l_Lean_Expr_inhabited;
x_237 = l_Lean_Expr_Inhabited;
x_238 = l_Lean_TypeClass_preprocessForOutParams___closed__2;
x_239 = lean_panic_fn(x_238);
lean_inc(x_189);
@ -5292,7 +5283,7 @@ if (lean_obj_tag(x_244) == 0)
{
lean_object* x_258; lean_object* x_259; lean_object* x_260; lean_object* x_261;
lean_dec(x_216);
x_258 = l_Lean_Expr_inhabited;
x_258 = l_Lean_Expr_Inhabited;
x_259 = l_Lean_TypeClass_preprocessForOutParams___closed__2;
x_260 = lean_panic_fn(x_259);
lean_inc(x_189);

112
stage0/library/Init/Lean/WHNF.c generated
View file

@ -42,17 +42,18 @@ lean_object* l_List_lengthAux___main___rarg(lean_object*, lean_object*);
lean_object* l_Lean_matchConstAux___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_WHNF_10__whnfCoreUnstuck___main___boxed(lean_object*);
lean_object* l_Lean_smartUnfoldingSuffix;
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_WHNF_1__getFirstCtor(lean_object*);
lean_object* l_Lean_getStuckMVar___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_WHNF_10__whnfCoreUnstuck(lean_object*);
lean_object* l_Lean_whnfEasyCases___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_mk_app(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_WHNF_5__toCtorWhenK___boxed(lean_object*);
lean_object* l_Lean_Expr_hasExprMVar___boxed(lean_object*);
lean_object* l___private_Init_Lean_WHNF_2__mkNullaryCtor___boxed(lean_object*);
lean_object* l___private_Init_Lean_WHNF_5__toCtorWhenK___rarg___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_whnfCore___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_whnfCore(lean_object*);
lean_object* l___private_Init_Lean_Expr_4__getAppRevArgsAux___main(lean_object*, lean_object*);
lean_object* lean_expr_instantiate1(lean_object*, lean_object*);
lean_object* l_Lean_unfoldDefinitionAux___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
@ -67,6 +68,7 @@ lean_object* l_Lean_unfoldDefinitionAux(lean_object*, lean_object*);
lean_object* l_Lean_whnfCore___main___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Lean_WHNF_6__isIdRhsApp(lean_object*);
lean_object* l___private_Init_Lean_WHNF_4__getRecRuleFor(lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppNumArgsAux___main(lean_object*, lean_object*);
lean_object* l_Lean_whnfEasyCases___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_WHNF_10__whnfCoreUnstuck___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
@ -86,16 +88,15 @@ lean_object* l_Lean_unfoldDefinitionAux___rarg(lean_object*, lean_object*, lean_
lean_object* l_Lean_whnfCore___boxed(lean_object*);
lean_object* l___private_Init_Lean_WHNF_3__toCtorIfLit___closed__1;
lean_object* l_Lean_mkSmartUnfoldingNameFor(lean_object*);
lean_object* lean_expr_mk_const(lean_object*, lean_object*);
lean_object* l_Lean_reduceQuotRec___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_expr_eqv(lean_object*, lean_object*);
lean_object* l_Lean_whnfCore___main___rarg___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_ConstantInfo_hasValue(lean_object*);
lean_object* l_Lean_reduceRec___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_WHNF_6__isIdRhsApp___closed__2;
extern lean_object* l_Lean_Expr_Inhabited;
lean_object* l_Lean_reduceQuotRec___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_whnfEasyCases___main(lean_object*);
lean_object* l___private_Init_Lean_Expr_5__getAppRevArgsAux___main(lean_object*, lean_object*);
lean_object* l_finally___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_WHNF_3__toCtorIfLit___closed__3;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
@ -129,7 +130,6 @@ lean_object* l_Lean_getStuckMVar___rarg(lean_object*, lean_object*, lean_object*
lean_object* l_Lean_RecursorVal_getMajorIdx(lean_object*);
lean_object* l_Lean_reduceQuotRec___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_WHNF_4__getRecRuleFor___lambda__1___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_inhabited;
lean_object* l_Lean_isRecStuck___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getStuckMVar___main___boxed(lean_object*);
lean_object* l___private_Init_Lean_WHNF_3__toCtorIfLit___closed__2;
@ -145,6 +145,7 @@ lean_object* l_Array_shrink___main___rarg(lean_object*, lean_object*);
lean_object* l_Lean_whnfMain(lean_object*);
lean_object* l_Lean_whnfCore___main___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_whnfEasyCases___boxed(lean_object*);
lean_object* l___private_Init_Lean_Expr_3__getAppArgsAux___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkNatLit(lean_object*);
lean_object* l_Lean_whnfCore___main___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalDecl_value_x3f(lean_object*);
@ -159,11 +160,11 @@ uint8_t l_Lean_Expr_isConstOf(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isAppOf(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getRevArgD___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_isRecStuck___boxed(lean_object*);
extern lean_object* l_Lean_Expr_getAppArgs___closed__1;
lean_object* l_Lean_whnfCore___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_whnfCore___main___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
extern lean_object* l_Lean_Expr_inhabited___closed__1;
lean_object* l___private_Init_Lean_Expr_2__mkAppRangeAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_WHNF_5__toCtorWhenK___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Expr_3__mkAppRangeAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_WHNF_6__isIdRhsApp___boxed(lean_object*);
lean_object* l_List_find___main___rarg(lean_object*, lean_object*);
lean_object* l_Lean_reduceRec___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -171,7 +172,7 @@ lean_object* l_Lean_whnfEasyCases___main___rarg___lambda__2(lean_object*, lean_o
lean_object* l_Lean_Expr_updateFn___main(lean_object*, lean_object*);
lean_object* l_Lean_whnfCore___main___rarg___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_whnfCore___main___boxed(lean_object*);
uint8_t lean_expr_has_expr_mvar(lean_object*);
uint8_t l_Lean_Expr_hasExprMVar(lean_object*);
lean_object* l___private_Init_Lean_WHNF_1__getFirstCtor___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_smartUnfoldingSuffix___closed__1;
lean_object* l___private_Init_Lean_WHNF_5__toCtorWhenK___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -181,7 +182,6 @@ lean_object* l_unreachable_x21___rarg(lean_object*);
lean_object* l_Lean_getStuckMVar___boxed(lean_object*);
lean_object* l___private_Init_Lean_WHNF_10__whnfCoreUnstuck___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Expr_4__getAppArgsAux___main(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_WHNF_1__getFirstCtor___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_whnfMain___main___boxed(lean_object*);
lean_object* l_Lean_whnfEasyCases___main___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -495,16 +495,16 @@ lean_dec(x_2);
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = lean_expr_mk_const(x_12, x_3);
x_15 = l_Lean_mkConst(x_12, x_3);
x_16 = lean_unsigned_to_nat(0u);
x_17 = l_Lean_Expr_getAppNumArgsAux___main(x_4, x_16);
x_18 = l_Lean_Expr_inhabited___closed__1;
x_18 = l_Lean_Expr_getAppArgs___closed__1;
lean_inc(x_17);
x_19 = lean_mk_array(x_17, x_18);
x_20 = lean_unsigned_to_nat(1u);
x_21 = lean_nat_sub(x_17, x_20);
lean_dec(x_17);
x_22 = l___private_Init_Lean_Expr_4__getAppArgsAux___main(x_4, x_19, x_21);
x_22 = l___private_Init_Lean_Expr_3__getAppArgsAux___main(x_4, x_19, x_21);
x_23 = l_Array_shrink___main___rarg(x_22, x_5);
x_24 = l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(x_23, x_23, x_16, x_15);
lean_dec(x_23);
@ -524,16 +524,16 @@ lean_dec(x_2);
x_28 = lean_ctor_get(x_27, 1);
lean_inc(x_28);
lean_dec(x_27);
x_29 = lean_expr_mk_const(x_26, x_3);
x_29 = l_Lean_mkConst(x_26, x_3);
x_30 = lean_unsigned_to_nat(0u);
x_31 = l_Lean_Expr_getAppNumArgsAux___main(x_4, x_30);
x_32 = l_Lean_Expr_inhabited___closed__1;
x_32 = l_Lean_Expr_getAppArgs___closed__1;
lean_inc(x_31);
x_33 = lean_mk_array(x_31, x_32);
x_34 = lean_unsigned_to_nat(1u);
x_35 = lean_nat_sub(x_31, x_34);
lean_dec(x_31);
x_36 = l___private_Init_Lean_Expr_4__getAppArgsAux___main(x_4, x_33, x_35);
x_36 = l___private_Init_Lean_Expr_3__getAppArgsAux___main(x_4, x_33, x_35);
x_37 = l_Array_shrink___main___rarg(x_36, x_5);
x_38 = l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(x_37, x_37, x_30, x_29);
lean_dec(x_37);
@ -650,7 +650,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Init_Lean_WHNF_3__toCtorIfLit___closed__2;
x_3 = lean_expr_mk_const(x_2, x_1);
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
@ -678,7 +678,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Init_Lean_WHNF_3__toCtorIfLit___closed__5;
x_3 = lean_expr_mk_const(x_2, x_1);
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
@ -702,7 +702,7 @@ x_6 = lean_unsigned_to_nat(1u);
x_7 = lean_nat_sub(x_3, x_6);
x_8 = l_Lean_mkNatLit(x_7);
x_9 = l___private_Init_Lean_WHNF_3__toCtorIfLit___closed__3;
x_10 = lean_expr_mk_app(x_9, x_8);
x_10 = l_Lean_mkApp(x_9, x_8);
return x_10;
}
else
@ -915,7 +915,7 @@ return x_14;
else
{
uint8_t x_15;
x_15 = lean_expr_has_expr_mvar(x_7);
x_15 = l_Lean_Expr_hasExprMVar(x_7);
if (x_15 == 0)
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
@ -940,14 +940,14 @@ 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; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; uint8_t x_32;
x_20 = lean_unsigned_to_nat(0u);
x_21 = l_Lean_Expr_getAppNumArgsAux___main(x_7, x_20);
x_22 = l_Lean_Expr_inhabited___closed__1;
x_22 = l_Lean_Expr_getAppArgs___closed__1;
lean_inc(x_21);
x_23 = lean_mk_array(x_21, x_22);
x_24 = lean_unsigned_to_nat(1u);
x_25 = lean_nat_sub(x_21, x_24);
lean_dec(x_21);
lean_inc(x_7);
x_26 = l___private_Init_Lean_Expr_4__getAppArgsAux___main(x_7, x_23, x_25);
x_26 = l___private_Init_Lean_Expr_3__getAppArgsAux___main(x_7, x_23, x_25);
x_27 = lean_ctor_get(x_1, 2);
lean_inc(x_27);
lean_dec(x_1);
@ -1088,13 +1088,13 @@ lean_inc(x_13);
lean_dec(x_10);
x_14 = lean_unsigned_to_nat(0u);
x_15 = l_Lean_Expr_getAppNumArgsAux___main(x_9, x_14);
x_16 = l_Lean_Expr_inhabited___closed__1;
x_16 = l_Lean_Expr_getAppArgs___closed__1;
lean_inc(x_15);
x_17 = lean_mk_array(x_15, x_16);
x_18 = lean_unsigned_to_nat(1u);
x_19 = lean_nat_sub(x_15, x_18);
lean_dec(x_15);
x_20 = l___private_Init_Lean_Expr_4__getAppArgsAux___main(x_9, x_17, x_19);
x_20 = l___private_Init_Lean_Expr_3__getAppArgsAux___main(x_9, x_17, x_19);
x_21 = l_List_lengthAux___main___rarg(x_3, x_14);
x_22 = lean_ctor_get(x_1, 0);
lean_inc(x_22);
@ -1138,7 +1138,7 @@ lean_dec(x_1);
x_34 = lean_nat_add(x_32, x_33);
lean_dec(x_33);
lean_dec(x_32);
x_35 = l___private_Init_Lean_Expr_3__mkAppRangeAux___main(x_34, x_4, x_14, x_29);
x_35 = l___private_Init_Lean_Expr_2__mkAppRangeAux___main(x_34, x_4, x_14, x_29);
lean_dec(x_34);
x_36 = lean_array_get_size(x_20);
x_37 = lean_ctor_get(x_13, 1);
@ -1146,11 +1146,11 @@ lean_inc(x_37);
lean_dec(x_13);
x_38 = lean_nat_sub(x_36, x_37);
lean_dec(x_37);
x_39 = l___private_Init_Lean_Expr_3__mkAppRangeAux___main(x_36, x_20, x_38, x_35);
x_39 = l___private_Init_Lean_Expr_2__mkAppRangeAux___main(x_36, x_20, x_38, x_35);
lean_dec(x_20);
lean_dec(x_36);
x_40 = lean_nat_add(x_5, x_18);
x_41 = l___private_Init_Lean_Expr_3__mkAppRangeAux___main(x_6, x_4, x_40, x_39);
x_41 = l___private_Init_Lean_Expr_2__mkAppRangeAux___main(x_6, x_4, x_40, x_39);
x_42 = lean_apply_1(x_7, x_41);
return x_42;
}
@ -1432,12 +1432,12 @@ if (lean_obj_tag(x_14) == 1)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
lean_dec(x_1);
x_15 = l_Lean_Expr_inhabited;
x_15 = l_Lean_Expr_Inhabited;
x_16 = lean_array_get(x_15, x_2, x_3);
x_17 = lean_expr_mk_app(x_16, x_4);
x_17 = l_Lean_mkApp(x_16, x_4);
x_18 = lean_unsigned_to_nat(1u);
x_19 = lean_nat_add(x_5, x_18);
x_20 = l___private_Init_Lean_Expr_3__mkAppRangeAux___main(x_6, x_2, x_19, x_17);
x_20 = l___private_Init_Lean_Expr_2__mkAppRangeAux___main(x_6, x_2, x_19, x_17);
x_21 = lean_apply_1(x_7, x_20);
return x_21;
}
@ -1830,13 +1830,13 @@ lean_closure_set(x_17, 1, x_3);
lean_closure_set(x_17, 2, x_4);
x_18 = lean_unsigned_to_nat(0u);
x_19 = l_Lean_Expr_getAppNumArgsAux___main(x_5, x_18);
x_20 = l_Lean_Expr_inhabited___closed__1;
x_20 = l_Lean_Expr_getAppArgs___closed__1;
lean_inc(x_19);
x_21 = lean_mk_array(x_19, x_20);
x_22 = lean_unsigned_to_nat(1u);
x_23 = lean_nat_sub(x_19, x_22);
lean_dec(x_19);
x_24 = l___private_Init_Lean_Expr_4__getAppArgsAux___main(x_5, x_21, x_23);
x_24 = l___private_Init_Lean_Expr_3__getAppArgsAux___main(x_5, x_21, x_23);
x_25 = l_Lean_isQuotRecStuck___rarg(x_2, x_4, x_17, x_16, x_6, x_24);
lean_dec(x_24);
return x_25;
@ -1853,13 +1853,13 @@ lean_closure_set(x_27, 1, x_3);
lean_closure_set(x_27, 2, x_4);
x_28 = lean_unsigned_to_nat(0u);
x_29 = l_Lean_Expr_getAppNumArgsAux___main(x_5, x_28);
x_30 = l_Lean_Expr_inhabited___closed__1;
x_30 = l_Lean_Expr_getAppArgs___closed__1;
lean_inc(x_29);
x_31 = lean_mk_array(x_29, x_30);
x_32 = lean_unsigned_to_nat(1u);
x_33 = lean_nat_sub(x_29, x_32);
lean_dec(x_29);
x_34 = l___private_Init_Lean_Expr_4__getAppArgsAux___main(x_5, x_31, x_33);
x_34 = l___private_Init_Lean_Expr_3__getAppArgsAux___main(x_5, x_31, x_33);
x_35 = l_Lean_isRecStuck___rarg(x_2, x_4, x_27, x_26, x_6, x_34);
lean_dec(x_34);
return x_35;
@ -2154,7 +2154,7 @@ lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_11 = l_Lean_Expr_inhabited;
x_11 = l_Lean_Expr_Inhabited;
x_12 = l_monadInhabited___rarg(x_1, x_11);
x_13 = l_unreachable_x21___rarg(x_12);
return x_13;
@ -2244,14 +2244,26 @@ lean_dec(x_1);
x_29 = lean_apply_1(x_5, x_4);
return x_29;
}
case 12:
{
lean_object* x_30; lean_object* x_31; lean_object* x_32;
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_30 = l_Lean_Expr_Inhabited;
x_31 = l_monadInhabited___rarg(x_1, x_30);
x_32 = l_unreachable_x21___rarg(x_31);
return x_32;
}
default:
{
lean_object* x_30;
lean_object* x_33;
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
x_30 = lean_box(0);
x_6 = x_30;
x_33 = lean_box(0);
x_6 = x_33;
goto block_10;
}
}
@ -2382,14 +2394,14 @@ 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; lean_object* x_10; lean_object* x_11; uint8_t x_12;
x_3 = lean_unsigned_to_nat(0u);
x_4 = l_Lean_Expr_getAppNumArgsAux___main(x_1, x_3);
x_5 = l_Lean_Expr_inhabited___closed__1;
x_5 = l_Lean_Expr_getAppArgs___closed__1;
lean_inc(x_4);
x_6 = lean_mk_array(x_4, x_5);
x_7 = lean_unsigned_to_nat(1u);
x_8 = lean_nat_sub(x_4, x_7);
lean_dec(x_4);
lean_inc(x_1);
x_9 = l___private_Init_Lean_Expr_4__getAppArgsAux___main(x_1, x_6, x_8);
x_9 = l___private_Init_Lean_Expr_3__getAppArgsAux___main(x_1, x_6, x_8);
x_10 = lean_array_get_size(x_9);
x_11 = lean_unsigned_to_nat(2u);
x_12 = lean_nat_dec_lt(x_10, x_11);
@ -2397,9 +2409,9 @@ if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
lean_dec(x_1);
x_13 = l_Lean_Expr_inhabited;
x_13 = l_Lean_Expr_Inhabited;
x_14 = lean_array_get(x_13, x_9, x_7);
x_15 = l___private_Init_Lean_Expr_3__mkAppRangeAux___main(x_10, x_9, x_11, x_14);
x_15 = l___private_Init_Lean_Expr_2__mkAppRangeAux___main(x_10, x_9, x_11, x_14);
lean_dec(x_9);
lean_dec(x_10);
return x_15;
@ -2580,7 +2592,7 @@ x_24 = lean_unsigned_to_nat(0u);
x_25 = l_Lean_Expr_getAppNumArgsAux___main(x_4, x_24);
x_26 = lean_mk_empty_array_with_capacity(x_25);
lean_dec(x_25);
x_27 = l___private_Init_Lean_Expr_5__getAppRevArgsAux___main(x_4, x_26);
x_27 = l___private_Init_Lean_Expr_4__getAppRevArgsAux___main(x_4, x_26);
x_28 = lean_alloc_closure((void*)(l_Lean_whnfCore___main___rarg), 9, 8);
lean_closure_set(x_28, 0, x_3);
lean_closure_set(x_28, 1, x_5);
@ -2679,13 +2691,13 @@ lean_inc(x_32);
lean_dec(x_27);
x_33 = lean_unsigned_to_nat(0u);
x_34 = l_Lean_Expr_getAppNumArgsAux___main(x_4, x_33);
x_35 = l_Lean_Expr_inhabited___closed__1;
x_35 = l_Lean_Expr_getAppArgs___closed__1;
lean_inc(x_34);
x_36 = lean_mk_array(x_34, x_35);
x_37 = lean_unsigned_to_nat(1u);
x_38 = lean_nat_sub(x_34, x_37);
lean_dec(x_34);
x_39 = l___private_Init_Lean_Expr_4__getAppArgsAux___main(x_4, x_36, x_38);
x_39 = l___private_Init_Lean_Expr_3__getAppArgsAux___main(x_4, x_36, x_38);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_3);
@ -2714,13 +2726,13 @@ lean_inc(x_42);
lean_dec(x_27);
x_43 = lean_unsigned_to_nat(0u);
x_44 = l_Lean_Expr_getAppNumArgsAux___main(x_4, x_43);
x_45 = l_Lean_Expr_inhabited___closed__1;
x_45 = l_Lean_Expr_getAppArgs___closed__1;
lean_inc(x_44);
x_46 = lean_mk_array(x_44, x_45);
x_47 = lean_unsigned_to_nat(1u);
x_48 = lean_nat_sub(x_44, x_47);
lean_dec(x_44);
x_49 = l___private_Init_Lean_Expr_4__getAppArgsAux___main(x_4, x_46, x_48);
x_49 = l___private_Init_Lean_Expr_3__getAppArgsAux___main(x_4, x_46, x_48);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
@ -2884,7 +2896,7 @@ x_31 = lean_unsigned_to_nat(0u);
x_32 = l_Lean_Expr_getAppNumArgsAux___main(x_3, x_31);
x_33 = lean_mk_empty_array_with_capacity(x_32);
lean_dec(x_32);
x_34 = l___private_Init_Lean_Expr_5__getAppRevArgsAux___main(x_3, x_33);
x_34 = l___private_Init_Lean_Expr_4__getAppRevArgsAux___main(x_3, x_33);
x_35 = l_Lean_Expr_betaRev(x_1, x_34);
lean_dec(x_1);
x_36 = l_Lean_whnfCore___main___rarg(x_2, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_35);
@ -3131,7 +3143,7 @@ lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_29 = l_Lean_Expr_inhabited;
x_29 = l_Lean_Expr_Inhabited;
x_30 = l_monadInhabited___rarg(x_1, x_29);
x_31 = l_unreachable_x21___rarg(x_30);
return x_31;
@ -3543,7 +3555,7 @@ x_20 = lean_unsigned_to_nat(0u);
x_21 = l_Lean_Expr_getAppNumArgsAux___main(x_3, x_20);
x_22 = lean_mk_empty_array_with_capacity(x_21);
lean_dec(x_21);
x_23 = l___private_Init_Lean_Expr_5__getAppRevArgsAux___main(x_3, x_22);
x_23 = l___private_Init_Lean_Expr_4__getAppRevArgsAux___main(x_3, x_22);
x_24 = l___private_Init_Lean_WHNF_9__deltaBetaDefinition___rarg(x_1, x_4, x_23, x_2, x_5);
return x_24;
}
@ -3562,7 +3574,7 @@ x_26 = lean_unsigned_to_nat(0u);
x_27 = l_Lean_Expr_getAppNumArgsAux___main(x_3, x_26);
x_28 = lean_mk_empty_array_with_capacity(x_27);
lean_dec(x_27);
x_29 = l___private_Init_Lean_Expr_5__getAppRevArgsAux___main(x_3, x_28);
x_29 = l___private_Init_Lean_Expr_4__getAppRevArgsAux___main(x_3, x_28);
lean_inc(x_2);
x_30 = lean_alloc_closure((void*)(l_Lean_unfoldDefinitionAux___rarg___lambda__3), 13, 12);
lean_closure_set(x_30, 0, x_6);
@ -3613,7 +3625,7 @@ x_35 = lean_unsigned_to_nat(0u);
x_36 = l_Lean_Expr_getAppNumArgsAux___main(x_3, x_35);
x_37 = lean_mk_empty_array_with_capacity(x_36);
lean_dec(x_36);
x_38 = l___private_Init_Lean_Expr_5__getAppRevArgsAux___main(x_3, x_37);
x_38 = l___private_Init_Lean_Expr_4__getAppRevArgsAux___main(x_3, x_37);
x_39 = l___private_Init_Lean_WHNF_9__deltaBetaDefinition___rarg(x_1, x_4, x_38, x_2, x_5);
return x_39;
}

511
stage0/src/kernel/expr.cpp generated
View file

@ -21,10 +21,6 @@ Author: Leonardo de Moura
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#ifndef LEAN_INITIAL_EXPR_CACHE_CAPACITY
#define LEAN_INITIAL_EXPR_CACHE_CAPACITY 1024*16
#endif
namespace lean {
/* Expression literal values */
literal::literal(char const * v):
@ -61,156 +57,6 @@ bool operator<(literal const & a, literal const & b) {
lean_unreachable();
}
static inline unsigned literal_hash(b_obj_arg l) {
switch (literal::kind(l)) {
case literal_kind::Nat: return nat::hash(cnstr_get(l, 0));
case literal_kind::String: return hash_str(string_size(cnstr_get(l, 0)) - 1, string_cstr(cnstr_get(l, 0)), 17);
}
lean_unreachable();
}
static unsigned levels_hash(object * ls) {
unsigned r = 23;
while (!is_scalar(ls)) {
r = hash(level::hash(cnstr_get(ls, 0)), r);
ls = cnstr_get(ls, 1);
}
return r;
}
// =======================================
// Safe arithmetic
static unsigned safe_inc(unsigned w) {
if (w < std::numeric_limits<unsigned>::max())
return w+1;
else
return w;
}
static unsigned safe_dec(unsigned k) {
return k == 0 ? 0 : k - 1;
}
// =======================================
// Scalar data offset calculation and setters/getters
inline constexpr unsigned num_obj_fields(expr_kind k) {
return
k == expr_kind::App ? 2 :
k == expr_kind::Const ? 2 :
k == expr_kind::FVar ? 1 : // TODO(Leo): it should be 1 after we remove support for legacy code
k == expr_kind::Lambda ? 3 :
k == expr_kind::Pi ? 3 :
k == expr_kind::BVar ? 1 :
k == expr_kind::Let ? 4 :
k == expr_kind::MVar ? 1 :
k == expr_kind::Sort ? 1 :
k == expr_kind::Lit ? 1 :
k == expr_kind::MData ? 2 :
k == expr_kind::Proj ? 3 :
k == expr_kind::Local ? 3 : // TODO(Leo): delete we remove support for legacy code
/* k == expr_kind::Quote */ 1;
}
/* Expression scalar data offset. */
inline constexpr unsigned scalar_offset(expr_kind k) { return num_obj_fields(k) * sizeof(object*); }
inline constexpr unsigned binder_info_offset(expr_kind k) {
// Only for: k == expr_kind::Pi || k == expr_kind::Lambda || k == expr_kind::Local
return scalar_offset(k);
}
/* Legacy support */
inline constexpr unsigned reflected_offset(expr_kind k) {
// Only for: k == expr_kind::Quote
return scalar_offset(k);
}
inline constexpr unsigned hash_offset(expr_kind k) {
return
k == expr_kind::Local ? scalar_offset(k) + sizeof(unsigned) : // for binder_info, TODO(Leo): delete after we remove support for legacy code
k == expr_kind::Lambda ? scalar_offset(k) + sizeof(unsigned) : // for binder_info
k == expr_kind::Pi ? scalar_offset(k) + sizeof(unsigned) : // for binder_info
scalar_offset(k);
}
inline constexpr size_t flags_offset(expr_kind k) { return hash_offset(k) + sizeof(unsigned); }
inline constexpr size_t loose_bvar_range_offset(expr_kind k) { return flags_offset(k) + sizeof(unsigned); }
/* Size for scalar value area for non recursive expression. */
inline constexpr size_t expr_scalar_size(expr_kind k) { return flags_offset(k) + sizeof(unsigned); }
/* Size for scalar value area for recursive expression. */
inline constexpr size_t rec_expr_scalar_size(expr_kind k) { return loose_bvar_range_offset(k) + sizeof(unsigned); }
static inline unsigned expr_hash(object * e) { return cnstr_get_scalar<unsigned>(e, hash_offset(expr::kind(e))); }
unsigned hash(expr const & e) { return expr_hash(e.raw()); }
extern "C" size_t lean_expr_hash(object * e) { return expr_hash(e); }
/* Set expr cached hash code and flags. All expressions contain them.
We provide the kind `k` to allow the compiler to compute offsets at compilation time. */
template<expr_kind k> void set_scalar(object * e, unsigned hash, bool has_expr_mvar, bool has_univ_mvar,
bool has_fvar, bool has_univ_param) {
lean_assert(expr::kind(e) == k);
unsigned char d =
(has_expr_mvar ? 1 : 0) +
(has_univ_mvar ? 2 : 0) +
(has_fvar ? 4 : 0) +
(has_univ_param ? 8 : 0);
cnstr_set_scalar<unsigned>(e, hash_offset(k), hash);
cnstr_set_scalar<unsigned char>(e, flags_offset(k), d);
}
/* Set expr cached loose bvar range. We only store this information in recursive expr constructors.
We provide the kind `k` to allow the compiler to compute offsets at compilation time. */
template<expr_kind k> void set_rec_scalar(object * e, unsigned loose_bvar_range) {
lean_assert(expr::kind(e) == k);
cnstr_set_scalar<unsigned>(e, loose_bvar_range_offset(k), loose_bvar_range);
}
template<expr_kind k> void set_binder_info(object * e, binder_info bi) {
lean_assert(expr::kind(e) == k);
cnstr_set_scalar<unsigned char>(e, binder_info_offset(k), static_cast<unsigned char>(bi));
}
static inline unsigned char get_flags(object * e) { return cnstr_get_scalar<unsigned char>(e, flags_offset(expr::kind(e))); }
static inline bool has_expr_mvar(object * e) { return (get_flags(e) & 1) != 0; }
static inline bool has_univ_mvar(object * e) { return (get_flags(e) & 2) != 0; }
static inline bool has_fvar(object * e) { return (get_flags(e) & 4) != 0; }
static inline bool has_univ_param(object * e) { return (get_flags(e) & 8) != 0; }
bool has_expr_mvar(expr const & e) { return has_expr_mvar(e.raw()); }
bool has_univ_mvar(expr const & e) { return has_univ_mvar(e.raw()); }
bool has_fvar(expr const & e) { return has_fvar(e.raw()); }
bool has_univ_param(expr const & e) { return has_univ_param(e.raw()); }
template<expr_kind k> unsigned get_loose_bvar_range_core(object * e) { return cnstr_get_scalar<unsigned>(e, loose_bvar_range_offset(k)); }
unsigned expr_get_loose_bvar_range(object * e) {
switch (expr::kind(e)) {
case expr_kind::Const: case expr_kind::Sort:
case expr_kind::Lit: case expr_kind::MVar:
case expr_kind::FVar:
return 0;
case expr_kind::BVar: {
object * idx = cnstr_get(e, 0);
if (is_scalar(idx))
return safe_inc(unbox(idx));
else
return std::numeric_limits<unsigned>::max();
}
case expr_kind::Local: return get_loose_bvar_range_core<expr_kind::Local>(e);
case expr_kind::Lambda: return get_loose_bvar_range_core<expr_kind::Lambda>(e);
case expr_kind::Pi: return get_loose_bvar_range_core<expr_kind::Pi>(e);
case expr_kind::App: return get_loose_bvar_range_core<expr_kind::App>(e);
case expr_kind::Let: return get_loose_bvar_range_core<expr_kind::Let>(e);
case expr_kind::MData: return get_loose_bvar_range_core<expr_kind::MData>(e);
case expr_kind::Proj: return get_loose_bvar_range_core<expr_kind::Proj>(e);
}
lean_unreachable(); // LCOV_EXCL_LINE
}
extern "C" object * lean_expr_get_loose_bvar_range(b_obj_arg e) { return mk_nat_obj(expr_get_loose_bvar_range(e)); }
bool is_atomic(expr const & e) {
switch (e.kind()) {
case expr_kind::Const: case expr_kind::Sort:
@ -227,28 +73,29 @@ bool is_atomic(expr const & e) {
lean_unreachable(); // LCOV_EXCL_LINE
}
binder_info binding_info(expr const & e) {
lean_assert(is_lambda(e) || is_pi(e));
// Remark: lambda and Pi have the same memory layout
return static_cast<binder_info>(cnstr_get_scalar<unsigned char>(e.raw(), binder_info_offset(expr_kind::Lambda)));
}
extern "C" uint8 lean_expr_binder_info(object * e);
binder_info binding_info(expr const & e) { return static_cast<binder_info>(lean_expr_binder_info(e.to_obj_arg())); }
/* Legacy */
binder_info local_info(expr const & e) {
lean_assert(is_local(e));
return static_cast<binder_info>(cnstr_get_scalar<unsigned char>(e.raw(), binder_info_offset(expr_kind::Local)));
}
extern "C" object * lean_lit_type(obj_arg e);
expr lit_type(expr const & e) { return expr(lean_lit_type(e.to_obj_arg())); }
static expr * g_nat_type = nullptr;
static expr * g_string_type = nullptr;
extern "C" usize lean_expr_hash(obj_arg e);
unsigned hash(expr const & e) { return lean_expr_hash(e.to_obj_arg()); }
expr const & lit_type(expr const & e) {
switch (lit_value(e).kind()) {
case literal_kind::String: return *g_string_type;
case literal_kind::Nat: return *g_nat_type;
}
lean_unreachable();
}
extern "C" uint8 lean_expr_has_fvar(obj_arg e);
bool has_fvar(expr const & e) { return lean_expr_has_fvar(e.to_obj_arg()); }
extern "C" uint8 lean_expr_has_expr_mvar(obj_arg e);
bool has_expr_mvar(expr const & e) { return lean_expr_has_expr_mvar(e.to_obj_arg()); }
extern "C" uint8 lean_expr_has_level_mvar(obj_arg e);
bool has_univ_mvar(expr const & e) { return lean_expr_has_level_mvar(e.to_obj_arg()); }
extern "C" uint8 lean_expr_has_level_param(obj_arg e);
bool has_univ_param(expr const & e) { return lean_expr_has_level_param(e.to_obj_arg()); }
extern "C" unsigned lean_expr_loose_bvar_range(object * e);
unsigned get_loose_bvar_range(expr const & e) { return lean_expr_loose_bvar_range(e.to_obj_arg()); }
// =======================================
// Constructors
@ -264,209 +111,58 @@ static expr const & get_dummy() {
expr::expr():expr(get_dummy()) {}
extern "C" object * lean_expr_mk_lit(obj_arg l) {
object * r = alloc_cnstr(static_cast<unsigned>(expr_kind::Lit), 1, expr_scalar_size(expr_kind::Lit));
cnstr_set(r, 0, l);
set_scalar<expr_kind::Lit>(r, literal_hash(l), false, false, false, false);
return r;
}
extern "C" object * lean_expr_mk_lit(obj_arg l);
expr mk_lit(literal const & l) { return expr(lean_expr_mk_lit(l.to_obj_arg())); }
expr mk_lit(literal const & l) {
inc(l.raw());
return expr(lean_expr_mk_lit(l.raw()));
}
extern "C" object * lean_expr_mk_mdata(obj_arg m, obj_arg e);
expr mk_mdata(kvmap const & m, expr const & e) { return expr(lean_expr_mk_mdata(m.to_obj_arg(), e.to_obj_arg())); }
extern "C" object * lean_expr_mk_mdata(obj_arg m, obj_arg e) {
object * r = alloc_cnstr(static_cast<unsigned>(expr_kind::MData), 2, expr_scalar_size(expr_kind::MData));
cnstr_set(r, 0, m);
cnstr_set(r, 1, e);
unsigned h = expr_hash(e); // Include hash(m)
set_scalar<expr_kind::MData>(r, h, has_expr_mvar(e), has_univ_mvar(e), has_fvar(e), has_univ_param(e));
set_rec_scalar<expr_kind::MData>(r, expr_get_loose_bvar_range(e));
return r;
}
extern "C" object * lean_expr_mk_proj(obj_arg s, obj_arg idx, obj_arg e);
expr mk_proj(name const & s, nat const & idx, expr const & e) { return expr(lean_expr_mk_proj(s.to_obj_arg(), idx.to_obj_arg(), e.to_obj_arg())); }
expr mk_mdata(kvmap const & m, expr const & e) {
inc(m.raw()); inc(e.raw());
return expr(lean_expr_mk_mdata(m.raw(), e.raw()));
}
extern "C" object * lean_expr_mk_bvar(obj_arg idx);
expr mk_bvar(nat const & idx) { return expr(lean_expr_mk_bvar(idx.to_obj_arg())); }
extern "C" object * lean_expr_mk_proj(obj_arg s, obj_arg idx, obj_arg e) {
object * r = alloc_cnstr(static_cast<unsigned>(expr_kind::Proj), 3, rec_expr_scalar_size(expr_kind::Proj));
cnstr_set(r, 0, s);
cnstr_set(r, 1, idx);
cnstr_set(r, 2, e);
unsigned h = hash(expr_hash(e), nat::hash(idx));
set_scalar<expr_kind::Proj>(r, h, has_expr_mvar(e), has_univ_mvar(e), has_fvar(e), has_univ_param(e));
set_rec_scalar<expr_kind::Proj>(r, expr_get_loose_bvar_range(e));
return r;
}
extern "C" object * lean_expr_mk_fvar(obj_arg n);
expr mk_fvar(name const & n) { return expr(lean_expr_mk_fvar(n.to_obj_arg())); }
expr mk_proj(name const & s, nat const & idx, expr const & e) {
inc(s.raw()); inc(idx.raw()); inc(e.raw());
return expr(lean_expr_mk_proj(s.raw(), idx.raw(), e.raw()));
}
extern "C" object * lean_expr_mk_mvar(object * n);
expr mk_mvar(name const & n) { return expr(lean_expr_mk_mvar(n.to_obj_arg())); }
extern "C" object * lean_expr_mk_bvar(obj_arg idx) {
object * r = alloc_cnstr(static_cast<unsigned>(expr_kind::BVar), 1, expr_scalar_size(expr_kind::BVar));
cnstr_set(r, 0, idx);
set_scalar<expr_kind::BVar>(r, nat::hash(idx), false, false, false, false);
return r;
}
extern "C" object * lean_expr_mk_const(obj_arg n, obj_arg ls);
expr mk_const(name const & n, levels const & ls) { return expr(lean_expr_mk_const(n.to_obj_arg(), ls.to_obj_arg())); }
expr mk_bvar(nat const & idx) {
inc(idx.raw());
return expr(lean_expr_mk_bvar(idx.raw()));
}
extern "C" object * lean_expr_mk_app(obj_arg f, obj_arg a);
expr mk_app(expr const & f, expr const & a) { return expr(lean_expr_mk_app(f.to_obj_arg(), a.to_obj_arg())); }
extern "C" object * lean_expr_mk_fvar(obj_arg n) {
object * r = alloc_cnstr(static_cast<unsigned>(expr_kind::FVar), 1, rec_expr_scalar_size(expr_kind::FVar));
cnstr_set(r, 0, n);
set_scalar<expr_kind::FVar>(r, name::hash(n), false, false, true, false);
return r;
}
expr mk_fvar(name const & n) {
return expr(lean_expr_mk_fvar(n.to_obj_arg()));
}
extern "C" object * lean_expr_mk_const(obj_arg n, obj_arg ls) {
object * r = alloc_cnstr(static_cast<unsigned>(expr_kind::Const), 2, expr_scalar_size(expr_kind::Const));
cnstr_set(r, 0, n);
cnstr_set(r, 1, ls);
set_scalar<expr_kind::Const>(r, hash(name::hash(n), levels_hash(ls)), false, levels_has_mvar(ls), false, levels_has_param(ls));
return r;
}
expr mk_const(name const & n, levels const & ls) {
inc(n.raw()); inc(ls.raw());
return expr(lean_expr_mk_const(n.raw(), ls.raw()));
}
extern "C" object * lean_expr_mk_app(obj_arg f, obj_arg a) {
object * r = alloc_cnstr(static_cast<unsigned>(expr_kind::App), 2, rec_expr_scalar_size(expr_kind::App));
cnstr_set(r, 0, f);
cnstr_set(r, 1, a);
unsigned h = hash(expr_hash(f), expr_hash(a));
set_scalar<expr_kind::App>(r, h,
has_expr_mvar(f) || has_expr_mvar(a),
has_univ_mvar(f) || has_univ_mvar(a),
has_fvar(f) || has_fvar(a),
has_univ_param(f) || has_univ_param(a));
set_rec_scalar<expr_kind::App>(r, std::max(expr_get_loose_bvar_range(f), expr_get_loose_bvar_range(a)));
return r;
}
expr mk_app(expr const & f, expr const & a) {
inc(f.raw()); inc(a.raw());
return expr(lean_expr_mk_app(f.raw(), a.raw()));
}
extern "C" object * lean_expr_mk_sort(obj_arg l) {
object * r = alloc_cnstr(static_cast<unsigned>(expr_kind::Sort), 1, expr_scalar_size(expr_kind::Sort));
cnstr_set(r, 0, l);
set_scalar<expr_kind::Sort>(r, level::hash(l), false, lean_level_has_mvar(l), false, lean_level_has_param(l));
return r;
}
expr mk_sort(level const & l) {
inc(l.raw());
return expr(lean_expr_mk_sort(l.raw()));
}
template<expr_kind k>
static object * mk_binding(obj_arg n, obj_arg t, obj_arg e, binder_info bi) {
lean_assert(k == expr_kind::Pi || k == expr_kind::Lambda);
object * r = alloc_cnstr(static_cast<unsigned>(k), 3, rec_expr_scalar_size(k));
cnstr_set(r, 0, n);
cnstr_set(r, 1, t);
cnstr_set(r, 2, e);
unsigned h = hash(expr_hash(t), expr_hash(e));
unsigned lbvr = std::max(expr_get_loose_bvar_range(t), safe_dec(expr_get_loose_bvar_range(e)));
set_binder_info<k>(r, bi);
set_scalar<k>(r, h,
has_expr_mvar(t) || has_expr_mvar(e),
has_univ_mvar(t) || has_univ_mvar(e),
has_fvar(t) || has_fvar(e),
has_univ_param(t) || has_univ_param(e));
set_rec_scalar<k>(r, lbvr);
return r;
}
extern "C" object * lean_expr_mk_lambda(obj_arg n, uint8 bi, obj_arg t, obj_arg e) {
return mk_binding<expr_kind::Lambda>(n, t, e, static_cast<binder_info>(bi));
}
extern "C" object * lean_expr_mk_sort(obj_arg l);
expr mk_sort(level const & l) { return expr(lean_expr_mk_sort(l.to_obj_arg())); }
extern "C" object * lean_expr_mk_lambda(obj_arg n, obj_arg t, obj_arg e, uint8 bi);
expr mk_lambda(name const & n, expr const & t, expr const & e, binder_info bi) {
inc(n.raw()); inc(t.raw()); inc(e.raw());
return expr(mk_binding<expr_kind::Lambda>(n.raw(), t.raw(), e.raw(), bi));
}
extern "C" object * lean_expr_mk_forall(obj_arg n, uint8 bi, obj_arg t, obj_arg e) {
return mk_binding<expr_kind::Pi>(n, t, e, static_cast<binder_info>(bi));
return expr(lean_expr_mk_lambda(n.to_obj_arg(), t.to_obj_arg(), e.to_obj_arg(), static_cast<uint8>(bi)));
}
extern "C" object * lean_expr_mk_forall(obj_arg n, obj_arg t, obj_arg e, uint8 bi);
expr mk_pi(name const & n, expr const & t, expr const & e, binder_info bi) {
inc(n.raw()); inc(t.raw()); inc(e.raw());
return expr(mk_binding<expr_kind::Pi>(n.raw(), t.raw(), e.raw(), bi));
return expr(lean_expr_mk_forall(n.to_obj_arg(), t.to_obj_arg(), e.to_obj_arg(), static_cast<uint8>(bi)));
}
static name * g_default_name = nullptr;
expr mk_arrow(expr const & t, expr const & e) {
return mk_pi(*g_default_name, t, e, mk_binder_info());
}
extern "C" object * lean_expr_mk_let(object * n, object * t, object * v, object * b) {
object * r = alloc_cnstr(static_cast<unsigned>(expr_kind::Let), 4, rec_expr_scalar_size(expr_kind::Let));
cnstr_set(r, 0, n);
cnstr_set(r, 1, t);
cnstr_set(r, 2, v);
cnstr_set(r, 3, b);
unsigned h = hash(hash(expr_hash(t), expr_hash(v)), expr_hash(b));
unsigned lbvr = std::max(expr_get_loose_bvar_range(t), std::max(expr_get_loose_bvar_range(v), safe_dec(expr_get_loose_bvar_range(b))));
set_scalar<expr_kind::Let>(r, h,
has_expr_mvar(t) || has_expr_mvar(v) || has_expr_mvar(b),
has_univ_mvar(t) || has_univ_mvar(v) || has_univ_mvar(b),
has_fvar(t) || has_fvar(v) || has_fvar(b),
has_univ_param(t) || has_univ_param(v) || has_univ_param(b));
set_rec_scalar<expr_kind::Let>(r, lbvr);
return r;
}
extern "C" object * lean_expr_mk_let(object * n, object * t, object * v, object * b);
expr mk_let(name const & n, expr const & t, expr const & v, expr const & b) {
inc(n.raw()); inc(t.raw()); inc(v.raw()); inc(b.raw());
return expr(lean_expr_mk_let(n.raw(), t.raw(), v.raw(), b.raw()));
}
extern "C" object * lean_expr_mk_mvar_core(object * n) {
object * r = alloc_cnstr(static_cast<unsigned>(expr_kind::MVar), 1, rec_expr_scalar_size(expr_kind::MVar));
cnstr_set(r, 0, n);
set_scalar<expr_kind::MVar>(r, name::hash(n), true, false, false, false);
set_rec_scalar<expr_kind::MVar>(r, 0);
return r;
}
extern "C" object * lean_expr_mk_mvar(object * n) {
return lean_expr_mk_mvar_core(n);
}
expr mk_mvar(name const & n) {
inc(n.raw());
return expr(lean_expr_mk_mvar_core(n.raw()));
return expr(lean_expr_mk_let(n.to_obj_arg(), t.to_obj_arg(), v.to_obj_arg(), b.to_obj_arg()));
}
static expr * g_Prop = nullptr;
static expr * g_Type0 = nullptr;
expr mk_Prop() { return *g_Prop; }
expr mk_Type() { return *g_Type0; }
// Legacy
extern "C" obj_res lean_expr_local(obj_arg vm_name, obj_arg vm_pp_name, obj_arg vm_type, uint8 vm_binder_info) {
return mk_local(name(vm_name), name(vm_pp_name), expr(vm_type), static_cast<binder_info>(vm_binder_info)).steal();
}
// =======================================
// Auxiliary constructors and accessors
@ -570,20 +266,6 @@ bool is_default_var_name(name const & n) {
return n == *g_default_name;
}
/* Legacy */
optional<expr> has_expr_metavar_strict(expr const & e) {
if (!has_expr_metavar(e))
return none_expr();
optional<expr> r;
for_each(e, [&](expr const & e, unsigned) {
if (r || !has_expr_metavar(e)) return false;
if (is_metavar_app(e)) { r = e; return false; }
if (is_local(e)) return false; // do not visit type
return true;
});
return r;
}
// =======================================
// Update
@ -643,45 +325,6 @@ expr update_let(expr const & e, expr const & new_type, expr const & new_value, e
return e;
}
/* Legacy */
static inline object * mk_local(obj_arg n, obj_arg pp_n, obj_arg t, binder_info bi) {
object * r = alloc_cnstr(static_cast<unsigned>(expr_kind::Local), 3, rec_expr_scalar_size(expr_kind::Local));
cnstr_set(r, 0, n);
cnstr_set(r, 1, pp_n);
cnstr_set(r, 2, t);
set_binder_info<expr_kind::Local>(r, bi);
set_scalar<expr_kind::Local>(r, name::hash(n), has_expr_mvar(t), has_univ_mvar(t), true, has_univ_param(t));
set_rec_scalar<expr_kind::Local>(r, expr_get_loose_bvar_range(t));
return r;
}
/* Legacy */
expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info bi) {
inc(n.raw()); inc(pp_n.raw()); inc(t.raw());
return expr(mk_local(n.raw(), pp_n.raw(), t.raw(), bi));
}
/* Legacy */
expr update_local(expr const & e, expr const & new_type, binder_info bi) {
if (is_eqp(local_type(e), new_type) && local_info(e) == bi)
return e;
else
return mk_local(local_name(e), local_pp_name(e), new_type, bi);
}
/* Legacy */
expr update_local(expr const & e, binder_info bi) {
return update_local(e, local_type(e), bi);
}
/* Legacy */
expr update_local(expr const & e, expr const & new_type) {
if (is_eqp(local_type(e), new_type))
return e;
else
return mk_local(local_name(e), local_pp_name(e), new_type, local_info(e));
}
extern "C" object * lean_expr_update_mdata(obj_arg e, obj_arg new_expr) {
if (mdata_expr(TO_REF(expr, e)).raw() != new_expr) {
lean_dec_ref(e);
@ -736,8 +379,7 @@ extern "C" object * lean_expr_update_forall(obj_arg e, uint8 new_binfo, obj_arg
if (binding_domain(TO_REF(expr, e)).raw() != new_domain || binding_body(TO_REF(expr, e)).raw() != new_body ||
binding_info(TO_REF(expr, e)) != static_cast<binder_info>(new_binfo)) {
lean_dec_ref(e);
return lean_expr_mk_forall(binding_name(TO_REF(expr, e)).to_obj_arg(),
new_binfo, new_domain, new_body);
return lean_expr_mk_forall(binding_name(TO_REF(expr, e)).to_obj_arg(), new_domain, new_body, new_binfo);
} else {
lean_dec_ref(new_domain); lean_dec_ref(new_body);
return e;
@ -748,8 +390,7 @@ extern "C" object * lean_expr_update_lambda(obj_arg e, uint8 new_binfo, obj_arg
if (binding_domain(TO_REF(expr, e)).raw() != new_domain || binding_body(TO_REF(expr, e)).raw() != new_body ||
binding_info(TO_REF(expr, e)) != static_cast<binder_info>(new_binfo)) {
lean_dec_ref(e);
return lean_expr_mk_lambda(binding_name(TO_REF(expr, e)).to_obj_arg(),
new_binfo, new_domain, new_body);
return lean_expr_mk_lambda(binding_name(TO_REF(expr, e)).to_obj_arg(), new_domain, new_body, new_binfo);
} else {
lean_dec_ref(new_domain); lean_dec_ref(new_body);
return e;
@ -767,7 +408,6 @@ extern "C" object * lean_expr_update_let(obj_arg e, obj_arg new_type, obj_arg ne
}
}
// =======================================
// Loose bound variable management
@ -878,21 +518,6 @@ expr infer_implicit(expr const & t, bool strict) {
return infer_implicit(t, std::numeric_limits<unsigned>::max(), strict);
}
// =======================================
// Extra exports
extern "C" uint8 lean_expr_has_expr_mvar(b_obj_arg o) {
return has_expr_mvar(TO_REF(expr, o));
}
extern "C" uint8 lean_expr_has_level_mvar(b_obj_arg o) {
return has_univ_mvar(TO_REF(expr, o));
}
extern "C" uint8 lean_expr_has_fvar(b_obj_arg o) {
return has_fvar(TO_REF(expr, o));
}
// =======================================
// Initialization & Finalization
@ -903,8 +528,6 @@ void initialize_expr() {
g_Prop = new expr(mk_sort(mk_level_zero()));
/* TODO(Leo): add support for builtin constants in the kernel.
Something similar to what we have in the library directory. */
g_nat_type = new expr(mk_constant("Nat"));
g_string_type = new expr(mk_constant("String"));
}
void finalize_expr() {
@ -912,7 +535,45 @@ void finalize_expr() {
delete g_Type0;
delete g_dummy;
delete g_default_name;
delete g_nat_type;
delete g_string_type;
}
// =======================================
// Legacy
binder_info local_info(expr const & e) { lean_assert(is_local(e)); return static_cast<binder_info>(lean_expr_binder_info(e.to_obj_arg())); }
extern "C" object * lean_expr_mk_local(obj_arg n, obj_arg u, obj_arg t, uint8 bi);
expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info bi) {
return expr(lean_expr_mk_local(n.to_obj_arg(), pp_n.to_obj_arg(), t.to_obj_arg(), static_cast<uint8>(bi)));
}
expr update_local(expr const & e, expr const & new_type, binder_info bi) {
if (is_eqp(local_type(e), new_type) && local_info(e) == bi)
return e;
else
return mk_local(local_name(e), local_pp_name(e), new_type, bi);
}
expr update_local(expr const & e, binder_info bi) {
return update_local(e, local_type(e), bi);
}
expr update_local(expr const & e, expr const & new_type) {
if (is_eqp(local_type(e), new_type))
return e;
else
return mk_local(local_name(e), local_pp_name(e), new_type, local_info(e));
}
optional<expr> has_expr_metavar_strict(expr const & e) {
if (!has_expr_metavar(e))
return none_expr();
optional<expr> r;
for_each(e, [&](expr const & e, unsigned) {
if (r || !has_expr_metavar(e)) return false;
if (is_metavar_app(e)) { r = e; return false; }
if (is_local(e)) return false; // do not visit type
return true;
});
return r;
}
}

5
stage0/src/kernel/expr.h generated
View file

@ -150,8 +150,7 @@ bool has_univ_mvar(expr const & e);
inline bool has_mvar(expr const & e) { return has_expr_mvar(e) || has_univ_mvar(e); }
bool has_fvar(expr const & e);
bool has_univ_param(expr const & e);
unsigned expr_get_loose_bvar_range(object * e);
inline unsigned get_loose_bvar_range(expr const & e) { return expr_get_loose_bvar_range(e.raw()); }
unsigned get_loose_bvar_range(expr const & e);
struct expr_hash { unsigned operator()(expr const & e) const { return hash(e); } };
struct expr_pair_hash {
@ -227,7 +226,7 @@ expr mk_Type();
inline literal const & lit_value(expr const & e) { lean_assert(is_lit(e)); return static_cast<literal const &>(cnstr_get_ref(e, 0)); }
inline bool is_nat_lit(expr const & e) { return is_lit(e) && lit_value(e).kind() == literal_kind::Nat; }
inline bool is_string_lit(expr const & e) { return is_lit(e) && lit_value(e).kind() == literal_kind::String; }
expr const & lit_type(expr const & e);
expr lit_type(expr const & e);
inline kvmap const & mdata_data(expr const & e) { lean_assert(is_mdata(e)); return static_cast<kvmap const &>(cnstr_get_ref(e, 0)); }
inline expr const & mdata_expr(expr const & e) { lean_assert(is_mdata(e)); return static_cast<expr const &>(cnstr_get_ref(e, 1)); }
inline name const & proj_sname(expr const & e) { lean_assert(is_proj(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }

1
stage0/src/library/compiler/util.cpp generated
View file

@ -372,7 +372,6 @@ bool is_runtime_builtin_type(name const & n) {
n == get_usize_name() ||
n == get_thunk_name() ||
n == get_lean_name_name() ||
n == get_lean_expr_name() ||
n == get_lean_level_name() ||
n == get_task_name() ||
n == get_array_name() ||