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-17 08:27:43 -08:00
parent b78ac59523
commit 5aa2b06bf4
13 changed files with 1328 additions and 770 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -74,6 +74,7 @@ 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*);
lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__4;
extern lean_object* l_Lean_mkLevelOne;
lean_object* l_Lean_Compiler_foldStrictOr___boxed(lean_object*);
lean_object* l_List_lookup___main___at_Lean_Compiler_findBinFoldFn___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_foldNatMod___boxed(lean_object*);
@ -125,7 +126,6 @@ lean_object* l_Lean_Compiler_foldUIntDiv___lambda__1(lean_object*, uint8_t, lean
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* 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*);
lean_object* l_Lean_Compiler_foldNatDecEq___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Compiler_natFoldFns___closed__3;
@ -180,6 +180,7 @@ lean_object* l_Lean_Compiler_foldNatPow(uint8_t);
lean_object* l_Lean_Compiler_boolFoldFns___closed__5;
lean_object* l_Lean_Compiler_natFoldFns___closed__10;
lean_object* l_Lean_Compiler_foldUnOp___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkLevelZero;
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Compiler_getBoolLit___boxed(lean_object*);
lean_object* l_Lean_Compiler_numScalarTypes___closed__14;
@ -2055,7 +2056,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Level_one;
x_2 = l_Lean_mkLevelOne;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
@ -2156,7 +2157,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = lean_box(0);
x_2 = l_Lean_mkLevelZero;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);

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

@ -36,6 +36,7 @@ lean_object* l_Lean_mkAsPattern___closed__1;
lean_object* l_Lean_Format_pretty(lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_convertHole(lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLevelMax(lean_object*, lean_object*);
lean_object* l_Lean_Elab_runIOUnsafe___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_array(lean_object*, lean_object*);
lean_object* l_IO_println___at_HasRepr_HasEval___spec__1___boxed(lean_object*, lean_object*);
@ -67,7 +68,6 @@ lean_object* l_Lean_registerAttribute(lean_object*, lean_object*);
lean_object* l_Lean_Elab_logError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elaborator_PreTerm_4__processBinder___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_convertSortApp___closed__2;
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;
@ -77,6 +77,7 @@ lean_object* l_Lean_mkPreTypeAscriptionIfSome(lean_object*, lean_object*);
lean_object* l_Lean_Elab_convertId(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_toLevel___main___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_KVMap_setNat(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkLevelOne;
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_toLevel___main___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_convertType(lean_object*, lean_object*);
lean_object* l_Lean_Elab_convertForall(lean_object*, lean_object*, lean_object*);
@ -140,6 +141,7 @@ 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;
lean_object* l_Lean_registerBuiltinPreTermElabAttr___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLevelParam(lean_object*);
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*);
@ -178,7 +180,6 @@ lean_object* l_Lean_addBuiltinPreTermElab___boxed(lean_object*, lean_object*, le
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elaborator_PreTerm_4__processBinder___spec__1___closed__5;
lean_object* l___private_Init_Lean_Elaborator_PreTerm_2__mkHoleFor___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_AssocList_find___main___at_Lean_Elab_toPreTerm___spec__2___boxed(lean_object*, lean_object*);
lean_object* lean_level_mk_imax(lean_object*, lean_object*);
lean_object* l_Lean_syntaxNodeKindOfAttrParam(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elaborator_PreTerm_1__setPos(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_convertSorry___closed__3;
@ -194,17 +195,14 @@ 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_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* 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;
lean_object* l___private_Init_Lean_Elaborator_PreTerm_2__mkHoleFor___closed__1;
lean_object* lean_level_mk_succ(lean_object*);
lean_object* l_Lean_mkAsIs___closed__1;
extern lean_object* l_System_FilePath_dirName___closed__1;
lean_object* l_panic(lean_object*, lean_object*, lean_object*);
@ -230,6 +228,7 @@ lean_object* l_Lean_Level_addOffsetAux___main(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_Elab_convertSorry___rarg(lean_object*);
lean_object* l_Lean_Elab_toLevel(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLevelSucc(lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_convertHole___closed__1;
lean_object* l___private_Init_Lean_Elaborator_PreTerm_4__processBinder___closed__3;
lean_object* lean_array_fget(lean_object*, lean_object*);
@ -253,9 +252,11 @@ 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* l_Lean_mkLevelIMax(lean_object*, lean_object*);
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
lean_object* l_AssocList_replace___main___at_Lean_addBuiltinPreTermElab___spec__7(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_convertProp___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkLevelMVar(lean_object*);
lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
lean_object* l_Lean_declareBuiltinElab(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_tail_x21___rarg(lean_object*);
@ -281,7 +282,6 @@ lean_object* l_Lean_mkAsIs(lean_object*);
lean_object* l_Lean_Elab_convertType___rarg___closed__1;
lean_object* l_Lean_Elab_convertForall___boxed(lean_object*, lean_object*, lean_object*);
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;
@ -1407,7 +1407,7 @@ lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 1);
lean_inc(x_15);
lean_dec(x_13);
x_16 = lean_level_mk_imax(x_4, x_14);
x_16 = l_Lean_mkLevelIMax(x_4, x_14);
x_3 = x_12;
x_4 = x_16;
x_6 = x_15;
@ -1472,7 +1472,7 @@ lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 1);
lean_inc(x_15);
lean_dec(x_13);
x_16 = lean_level_mk_max(x_4, x_14);
x_16 = l_Lean_mkLevelMax(x_4, x_14);
x_3 = x_12;
x_4 = x_16;
x_6 = x_15;
@ -1536,7 +1536,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_box(0);
x_2 = lean_level_mk_mvar(x_1);
x_2 = l_Lean_mkLevelMVar(x_1);
return x_2;
}
}
@ -1711,7 +1711,7 @@ else
{
lean_object* x_61;
lean_dec(x_1);
x_61 = lean_level_mk_param(x_42);
x_61 = l_Lean_mkLevelParam(x_42);
lean_ctor_set(x_43, 0, x_61);
return x_43;
}
@ -1762,7 +1762,7 @@ else
{
lean_object* x_76; lean_object* x_77;
lean_dec(x_1);
x_76 = lean_level_mk_param(x_42);
x_76 = l_Lean_mkLevelParam(x_42);
x_77 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_77, 0, x_76);
lean_ctor_set(x_77, 1, x_63);
@ -2321,7 +2321,7 @@ lean_object* _init_l_Lean_Elab_convertType___rarg___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Level_one___closed__1;
x_1 = l_Lean_mkLevelOne;
x_2 = l_Lean_mkSort(x_1);
return x_2;
}
@ -2574,7 +2574,7 @@ return x_10;
else
{
lean_object* x_16; lean_object* x_17;
x_16 = lean_level_mk_succ(x_12);
x_16 = l_Lean_mkLevelSucc(x_12);
x_17 = l_Lean_mkSort(x_16);
lean_ctor_set(x_10, 0, x_17);
return x_10;
@ -2603,7 +2603,7 @@ return x_23;
else
{
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = lean_level_mk_succ(x_18);
x_24 = l_Lean_mkLevelSucc(x_18);
x_25 = l_Lean_mkSort(x_24);
x_26 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_26, 0, x_25);

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

@ -78,7 +78,7 @@ size_t l_List_hash___at_Lean_mkConst___spec__1(lean_object*);
extern lean_object* l_List_get_x21___main___rarg___closed__2;
lean_object* l_Lean_Expr_updateLambda_x21___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_hasLooseBVar___boxed(lean_object*, lean_object*);
uint8_t lean_level_has_mvar(lean_object*);
uint8_t l_Lean_Level_hasMVar(lean_object*);
uint64_t l_Lean_Expr_mkData___closed__1;
lean_object* l_Lean_ExprStructEq_Hashable;
lean_object* lean_expr_dbg_to_string(lean_object*);
@ -213,6 +213,7 @@ uint8_t lean_expr_equal(lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateSort_x21___closed__2;
lean_object* l_Lean_Expr_instantiateRev___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkSort(lean_object*);
extern lean_object* l_Lean_Level_mkData___closed__1;
lean_object* l_Lean_Expr_appFn_x21___closed__1;
lean_object* l_Lean_Expr_Data_binderInfo___boxed(lean_object*);
uint64_t l_Lean_Expr_mkDataForLet(size_t, lean_object*, uint8_t, uint8_t, uint8_t, uint8_t, uint8_t);
@ -247,6 +248,7 @@ lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_ExprStructEq_beq___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Expr_8__etaExpandedBody___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_HasRepr;
extern lean_object* l_Lean_mkLevelZero;
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateApp_x21___closed__1;
lean_object* l_Lean_Expr_constLevels_x21___closed__1;
@ -254,7 +256,7 @@ lean_object* l_Lean_mkAppB(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLambda(lean_object*, uint8_t, lean_object*, lean_object*);
uint8_t l_Lean_BinderInfo_beq(uint8_t, uint8_t);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
uint8_t lean_level_has_param(lean_object*);
uint8_t l_Lean_Level_hasParam(lean_object*);
lean_object* l_Lean_Expr_updateLet___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_mkDataForBinder___boxed__const__1;
uint8_t lean_expr_has_mvar(lean_object*);
@ -298,7 +300,7 @@ lean_object* l_Lean_Expr_getRevArg_x21(lean_object*, lean_object*);
lean_object* l_Lean_Expr_hasFVar___boxed(lean_object*);
lean_object* l_Lean_Expr_HasToString;
uint8_t l_Lean_Expr_isAppOfArity___main(lean_object*, lean_object*, lean_object*);
size_t lean_level_hash(lean_object*);
size_t l_Lean_Level_hash(lean_object*);
uint8_t l_Lean_Expr_isBinding(lean_object*);
lean_object* l_Lean_Expr_mvarId_x21___closed__2;
lean_object* l_Lean_Expr_appFn_x21___closed__2;
@ -437,7 +439,6 @@ uint64_t l_UInt64_land(uint64_t, uint64_t);
lean_object* l_Lean_Expr_mkAppRevRange___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Expr_5__withAppRevAux___main(lean_object*);
lean_object* l_Lean_Expr_bindingBody_x21___closed__1;
lean_object* l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__4;
lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
lean_object* l_Lean_Expr_isMVar___boxed(lean_object*);
lean_object* l_Lean_ExprStructEq_Inhabited;
@ -1004,22 +1005,12 @@ return x_4;
lean_object* _init_l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(16777216u);
x_2 = lean_unsigned_to_nat(1u);
x_3 = lean_nat_sub(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Init.Lean.Expr");
return x_1;
}
}
lean_object* _init_l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__3() {
lean_object* _init_l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__2() {
_start:
{
lean_object* x_1;
@ -1027,14 +1018,14 @@ x_1 = lean_mk_string("bound variable index is too big");
return x_1;
}
}
lean_object* _init_l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__4() {
lean_object* _init_l___private_Init_Lean_Expr_1__Expr_mkDataCore___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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(122u);
x_3 = lean_unsigned_to_nat(42u);
x_4 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__3;
x_4 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__2;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
return x_5;
}
@ -1052,7 +1043,7 @@ uint64_t l___private_Init_Lean_Expr_1__Expr_mkDataCore(size_t x_1, lean_object*
_start:
{
lean_object* x_9; uint8_t x_10;
x_9 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_9 = l_Lean_Level_mkData___closed__1;
x_10 = lean_nat_dec_lt(x_9, x_2);
if (x_10 == 0)
{
@ -1092,7 +1083,7 @@ return x_40;
else
{
lean_object* x_41; lean_object* x_42; lean_object* x_43; uint64_t x_44;
x_41 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__4;
x_41 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__3;
x_42 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___boxed__const__1;
x_43 = lean_panic_fn(x_41);
x_44 = lean_unbox_uint64(x_43);
@ -1176,7 +1167,7 @@ uint64_t l_Lean_Expr_mkData(size_t x_1, lean_object* x_2, uint8_t x_3, uint8_t x
_start:
{
lean_object* x_7; uint8_t x_8;
x_7 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_7 = l_Lean_Level_mkData___closed__1;
x_8 = lean_nat_dec_lt(x_7, x_2);
if (x_8 == 0)
{
@ -1212,7 +1203,7 @@ return x_34;
else
{
lean_object* x_35; lean_object* x_36; lean_object* x_37; uint64_t x_38;
x_35 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__4;
x_35 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__3;
x_36 = l_Lean_Expr_mkData___boxed__const__1;
x_37 = lean_panic_fn(x_35);
x_38 = lean_unbox_uint64(x_37);
@ -1254,7 +1245,7 @@ uint64_t l_Lean_Expr_mkDataForBinder(size_t x_1, lean_object* x_2, uint8_t x_3,
_start:
{
lean_object* x_8; uint8_t x_9;
x_8 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_8 = l_Lean_Level_mkData___closed__1;
x_9 = lean_nat_dec_lt(x_8, x_2);
if (x_9 == 0)
{
@ -1292,7 +1283,7 @@ return x_37;
else
{
lean_object* x_38; lean_object* x_39; lean_object* x_40; uint64_t x_41;
x_38 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__4;
x_38 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__3;
x_39 = l_Lean_Expr_mkDataForBinder___boxed__const__1;
x_40 = lean_panic_fn(x_38);
x_41 = lean_unbox_uint64(x_40);
@ -1336,7 +1327,7 @@ uint64_t l_Lean_Expr_mkDataForLet(size_t x_1, lean_object* x_2, uint8_t x_3, uin
_start:
{
lean_object* x_8; uint8_t x_9;
x_8 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_8 = l_Lean_Level_mkData___closed__1;
x_9 = lean_nat_dec_lt(x_8, x_2);
if (x_9 == 0)
{
@ -1374,7 +1365,7 @@ return x_37;
else
{
lean_object* x_38; lean_object* x_39; lean_object* x_40; uint64_t x_41;
x_38 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__4;
x_38 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__3;
x_39 = l_Lean_Expr_mkDataForLet___boxed__const__1;
x_40 = lean_panic_fn(x_38);
x_41 = lean_unbox_uint64(x_40);
@ -1410,7 +1401,7 @@ _start:
{
uint64_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = 0;
x_2 = lean_box(0);
x_2 = l_Lean_mkLevelZero;
x_3 = lean_alloc_ctor(3, 1, 8);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint64(x_3, sizeof(void*)*1, x_1);
@ -2441,7 +2432,7 @@ else
lean_object* x_3; lean_object* x_4; size_t x_5; size_t x_6;
x_3 = lean_ctor_get(x_2, 0);
x_4 = lean_ctor_get(x_2, 1);
x_5 = lean_level_hash(x_3);
x_5 = l_Lean_Level_hash(x_3);
x_6 = lean_usize_mix_hash(x_1, x_5);
x_1 = x_6;
x_2 = x_4;
@ -2469,12 +2460,9 @@ else
{
lean_object* x_3; lean_object* x_4; uint8_t x_5; uint8_t x_6;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_2);
x_5 = l_List_foldr___main___at_Lean_mkConst___spec__3(x_1, x_4);
x_6 = lean_level_has_mvar(x_3);
x_6 = l_Lean_Level_hasMVar(x_3);
if (x_6 == 0)
{
return x_5;
@ -2499,12 +2487,9 @@ else
{
lean_object* x_3; lean_object* x_4; uint8_t x_5; uint8_t x_6;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_2);
x_5 = l_List_foldr___main___at_Lean_mkConst___spec__4(x_1, x_4);
x_6 = lean_level_has_param(x_3);
x_6 = l_Lean_Level_hasParam(x_3);
if (x_6 == 0)
{
return x_5;
@ -2528,9 +2513,7 @@ x_5 = l_List_hash___at_Lean_mkConst___spec__1(x_2);
x_6 = lean_usize_mix_hash(x_4, x_5);
x_7 = lean_usize_mix_hash(x_3, x_6);
x_8 = 0;
lean_inc(x_2);
x_9 = l_List_foldr___main___at_Lean_mkConst___spec__3(x_8, x_2);
lean_inc(x_2);
x_10 = l_List_foldr___main___at_Lean_mkConst___spec__4(x_8, x_2);
x_11 = lean_unsigned_to_nat(0u);
x_12 = l_Lean_Expr_mkData(x_7, x_11, x_8, x_8, x_9, x_10);
@ -2570,6 +2553,7 @@ uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = l_List_foldr___main___at_Lean_mkConst___spec__3(x_3, x_2);
lean_dec(x_2);
x_5 = lean_box(x_4);
return x_5;
}
@ -2581,6 +2565,7 @@ uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = l_List_foldr___main___at_Lean_mkConst___spec__4(x_3, x_2);
lean_dec(x_2);
x_5 = lean_box(x_4);
return x_5;
}
@ -2699,12 +2684,10 @@ _start:
{
size_t x_2; size_t x_3; size_t x_4; uint8_t x_5; uint8_t x_6; lean_object* x_7; uint8_t x_8; uint64_t x_9; lean_object* x_10;
x_2 = 11;
x_3 = lean_level_hash(x_1);
x_3 = l_Lean_Level_hash(x_1);
x_4 = lean_usize_mix_hash(x_2, x_3);
lean_inc(x_1);
x_5 = lean_level_has_mvar(x_1);
lean_inc(x_1);
x_6 = lean_level_has_param(x_1);
x_5 = l_Lean_Level_hasMVar(x_1);
x_6 = l_Lean_Level_hasParam(x_1);
x_7 = lean_unsigned_to_nat(0u);
x_8 = 0;
x_9 = l_Lean_Expr_mkData(x_4, x_7, x_8, x_8, x_5, x_6);
@ -4966,7 +4949,7 @@ lean_object* _init_l_Lean_Expr_getAppArgs___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_box(0);
x_1 = l_Lean_mkLevelZero;
x_2 = l_Lean_mkSort(x_1);
return x_2;
}
@ -5242,7 +5225,7 @@ lean_object* _init_l_Lean_Expr_getRevArg_x21___main___closed__1() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(452u);
x_3 = lean_unsigned_to_nat(20u);
x_4 = l_List_get_x21___main___rarg___closed__2;
@ -5496,7 +5479,7 @@ lean_object* _init_l_Lean_Expr_appFn_x21___closed__2() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(472u);
x_3 = lean_unsigned_to_nat(15u);
x_4 = l_Lean_Expr_appFn_x21___closed__1;
@ -5537,7 +5520,7 @@ lean_object* _init_l_Lean_Expr_appArg_x21___closed__1() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(476u);
x_3 = lean_unsigned_to_nat(15u);
x_4 = l_Lean_Expr_appFn_x21___closed__1;
@ -5586,7 +5569,7 @@ lean_object* _init_l_Lean_Expr_constName_x21___closed__2() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(480u);
x_3 = lean_unsigned_to_nat(17u);
x_4 = l_Lean_Expr_constName_x21___closed__1;
@ -5627,7 +5610,7 @@ lean_object* _init_l_Lean_Expr_constLevels_x21___closed__1() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(484u);
x_3 = lean_unsigned_to_nat(18u);
x_4 = l_Lean_Expr_constName_x21___closed__1;
@ -5676,7 +5659,7 @@ lean_object* _init_l_Lean_Expr_bvarIdx_x21___closed__2() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(488u);
x_3 = lean_unsigned_to_nat(16u);
x_4 = l_Lean_Expr_bvarIdx_x21___closed__1;
@ -5725,7 +5708,7 @@ lean_object* _init_l_Lean_Expr_fvarId_x21___closed__2() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(492u);
x_3 = lean_unsigned_to_nat(14u);
x_4 = l_Lean_Expr_fvarId_x21___closed__1;
@ -5774,7 +5757,7 @@ lean_object* _init_l_Lean_Expr_mvarId_x21___closed__2() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(496u);
x_3 = lean_unsigned_to_nat(14u);
x_4 = l_Lean_Expr_mvarId_x21___closed__1;
@ -5823,7 +5806,7 @@ lean_object* _init_l_Lean_Expr_bindingName_x21___closed__2() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(501u);
x_3 = lean_unsigned_to_nat(21u);
x_4 = l_Lean_Expr_bindingName_x21___closed__1;
@ -5873,7 +5856,7 @@ lean_object* _init_l_Lean_Expr_bindingDomain_x21___closed__1() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(506u);
x_3 = lean_unsigned_to_nat(21u);
x_4 = l_Lean_Expr_bindingName_x21___closed__1;
@ -5923,7 +5906,7 @@ lean_object* _init_l_Lean_Expr_bindingBody_x21___closed__1() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(511u);
x_3 = lean_unsigned_to_nat(21u);
x_4 = l_Lean_Expr_bindingName_x21___closed__1;
@ -5981,7 +5964,7 @@ lean_object* _init_l_Lean_Expr_letName_x21___closed__2() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(515u);
x_3 = lean_unsigned_to_nat(20u);
x_4 = l_Lean_Expr_letName_x21___closed__1;
@ -6787,7 +6770,7 @@ lean_object* _init_l_Lean_Expr_updateApp_x21___closed__1() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(681u);
x_3 = lean_unsigned_to_nat(18u);
x_4 = l_Lean_Expr_appFn_x21___closed__1;
@ -6829,7 +6812,7 @@ lean_object* _init_l_Lean_Expr_updateConst_x21___closed__1() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(690u);
x_3 = lean_unsigned_to_nat(18u);
x_4 = l_Lean_Expr_constName_x21___closed__1;
@ -6878,7 +6861,7 @@ lean_object* _init_l_Lean_Expr_updateSort_x21___closed__2() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(699u);
x_3 = lean_unsigned_to_nat(14u);
x_4 = l_Lean_Expr_updateSort_x21___closed__1;
@ -6935,7 +6918,7 @@ lean_object* _init_l_Lean_Expr_updateMData_x21___closed__2() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(716u);
x_3 = lean_unsigned_to_nat(17u);
x_4 = l_Lean_Expr_updateMData_x21___closed__1;
@ -6976,7 +6959,7 @@ lean_object* _init_l_Lean_Expr_updateProj_x21___closed__2() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(721u);
x_3 = lean_unsigned_to_nat(18u);
x_4 = l_Lean_Expr_updateProj_x21___closed__1;
@ -7027,7 +7010,7 @@ lean_object* _init_l_Lean_Expr_updateForall_x21___closed__2() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(730u);
x_3 = lean_unsigned_to_nat(21u);
x_4 = l_Lean_Expr_updateForall_x21___closed__1;
@ -7071,7 +7054,7 @@ lean_object* _init_l_Lean_Expr_updateForallE_x21___closed__1() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(735u);
x_3 = lean_unsigned_to_nat(21u);
x_4 = l_Lean_Expr_updateForall_x21___closed__1;
@ -7125,7 +7108,7 @@ lean_object* _init_l_Lean_Expr_updateLambda_x21___closed__2() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(744u);
x_3 = lean_unsigned_to_nat(17u);
x_4 = l_Lean_Expr_updateLambda_x21___closed__1;
@ -7169,7 +7152,7 @@ lean_object* _init_l_Lean_Expr_updateLambdaE_x21___closed__1() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(749u);
x_3 = lean_unsigned_to_nat(17u);
x_4 = l_Lean_Expr_updateLambda_x21___closed__1;
@ -7213,7 +7196,7 @@ lean_object* _init_l_Lean_Expr_updateLet_x21___closed__1() {
_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_Expr_1__Expr_mkDataCore___closed__2;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(758u);
x_3 = lean_unsigned_to_nat(20u);
x_4 = l_Lean_Expr_letName_x21___closed__1;
@ -7348,8 +7331,6 @@ l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__2 = _init_l___private_In
lean_mark_persistent(l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__2);
l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__3 = _init_l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__3();
lean_mark_persistent(l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__3);
l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__4 = _init_l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__4();
lean_mark_persistent(l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__4);
l___private_Init_Lean_Expr_1__Expr_mkDataCore___boxed__const__1 = _init_l___private_Init_Lean_Expr_1__Expr_mkDataCore___boxed__const__1();
lean_mark_persistent(l___private_Init_Lean_Expr_1__Expr_mkDataCore___boxed__const__1);
l_Lean_Expr_mkData___closed__1 = _init_l_Lean_Expr_mkData___closed__1();

1520
stage0/library/Init/Lean/Level.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -53,7 +53,6 @@ lean_object* l___private_Init_Lean_Meta_Default_3__auxFixpoint___main___boxed(le
lean_object* l_Lean_Meta_isPropAux___at_Lean_Meta_isProp___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_InferType_7__inferLambdaType___at_Lean_Meta_isProp___spec__3(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__40(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_level_mk_mvar(lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___main___at_Lean_Meta_isProp___spec__20(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_instantiate_rev_range(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_WHNF_8__deltaDefinition___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__15(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -171,7 +170,6 @@ lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux__
lean_object* l___private_Init_Lean_Meta_InferType_4__inferProjType___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__52(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_isProp___spec__11___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_whnfEasyCases___main___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__11___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_level_mk_imax(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___main___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__37___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyRangeMAux___main___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_InferType_2__inferAppType___at_Lean_Meta_isProp___spec__14(lean_object*, lean_object*, lean_object*, lean_object*);
@ -189,7 +187,6 @@ lean_object* l_Nat_foldMAux___main___at___private_Init_Lean_Meta_Default_3__auxF
lean_object* l_Lean_Meta_instantiateLevelMVars(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___main___at_Lean_Meta_getFunInfo___spec__5(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_instantiate_lparams(lean_object*, lean_object*, lean_object*);
lean_object* lean_level_mk_succ(lean_object*);
lean_object* l_Array_shrink___main___rarg(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_find___at___private_Init_Lean_Meta_FunInfo_1__checkFunInfoCache___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__50___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*);
@ -214,6 +211,7 @@ lean_object* l___private_Init_Lean_Meta_InferType_3__inferConstType(lean_object*
lean_object* l_Lean_mkProj(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_Meta_getFunInfoNArgs(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLevelSucc(lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__51(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isDefEq(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Array_anyRangeMAux___main___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -243,9 +241,11 @@ lean_object* l___private_Init_Lean_WHNF_9__deltaBetaDefinition___at___private_In
lean_object* l_Lean_Meta_lambdaTelescope___at_Lean_Meta_isProp___spec__4(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_isClassQuick___main___closed__1;
lean_object* l_Lean_Meta_withNewLocalInstances___main___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__40___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLevelIMax(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_8__forallTelescopeReducingAux___at_Lean_Meta_getFunInfo___spec__4___closed__1;
lean_object* l_Lean_Meta_withNewLocalInstances___main___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__39___lambda__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_hasExprMVar(lean_object*);
lean_object* l_Lean_mkLevelMVar(lean_object*);
lean_object* l___private_Init_Lean_WHNF_9__deltaBetaDefinition___at___private_Init_Lean_Meta_Default_3__auxFixpoint___main___spec__24(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_isProp___spec__22___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_unreachable_x21___rarg(lean_object*);
@ -275,27 +275,16 @@ _start:
{
if (lean_obj_tag(x_1) == 3)
{
lean_object* x_2;
x_2 = lean_ctor_get(x_1, 0);
if (lean_obj_tag(x_2) == 0)
uint8_t x_2;
x_2 = 0;
return x_2;
}
else
{
uint8_t x_3;
x_3 = 0;
x_3 = 1;
return x_3;
}
else
{
uint8_t x_4;
x_4 = 1;
return x_4;
}
}
else
{
uint8_t x_5;
x_5 = 1;
return x_5;
}
}
}
lean_object* l___private_Init_Lean_Meta_Default_1__exprToBool___boxed(lean_object* x_1) {
@ -10096,7 +10085,7 @@ lean_inc(x_23);
x_24 = lean_ctor_get(x_22, 1);
lean_inc(x_24);
lean_dec(x_22);
x_25 = lean_level_mk_mvar(x_23);
x_25 = l_Lean_mkLevelMVar(x_23);
lean_inc(x_25);
x_26 = l_Lean_mkSort(x_25);
x_27 = l_Lean_Meta_assignExprMVar(x_17, x_26, x_2, x_24);
@ -10403,7 +10392,7 @@ lean_inc(x_94);
x_95 = lean_ctor_get(x_93, 1);
lean_inc(x_95);
lean_dec(x_93);
x_96 = lean_level_mk_mvar(x_94);
x_96 = l_Lean_mkLevelMVar(x_94);
lean_inc(x_96);
x_97 = l_Lean_mkSort(x_96);
x_98 = l_Lean_Meta_assignExprMVar(x_88, x_97, x_2, x_95);
@ -10676,7 +10665,7 @@ lean_inc(x_17);
x_18 = lean_ctor_get(x_16, 1);
lean_inc(x_18);
lean_dec(x_16);
x_19 = lean_level_mk_imax(x_17, x_5);
x_19 = l_Lean_mkLevelIMax(x_17, x_5);
x_3 = x_11;
x_4 = lean_box(0);
x_5 = x_19;
@ -14099,7 +14088,7 @@ lean_dec(x_2);
x_62 = lean_ctor_get(x_1, 0);
lean_inc(x_62);
lean_dec(x_1);
x_63 = lean_level_mk_succ(x_62);
x_63 = l_Lean_mkLevelSucc(x_62);
x_64 = l_Lean_mkSort(x_63);
x_65 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_65, 0, x_64);
@ -18710,7 +18699,7 @@ lean_inc(x_23);
x_24 = lean_ctor_get(x_22, 1);
lean_inc(x_24);
lean_dec(x_22);
x_25 = lean_level_mk_mvar(x_23);
x_25 = l_Lean_mkLevelMVar(x_23);
lean_inc(x_25);
x_26 = l_Lean_mkSort(x_25);
x_27 = l_Lean_Meta_assignExprMVar(x_17, x_26, x_2, x_24);
@ -19017,7 +19006,7 @@ lean_inc(x_94);
x_95 = lean_ctor_get(x_93, 1);
lean_inc(x_95);
lean_dec(x_93);
x_96 = lean_level_mk_mvar(x_94);
x_96 = l_Lean_mkLevelMVar(x_94);
lean_inc(x_96);
x_97 = l_Lean_mkSort(x_96);
x_98 = l_Lean_Meta_assignExprMVar(x_88, x_97, x_2, x_95);
@ -19290,7 +19279,7 @@ lean_inc(x_17);
x_18 = lean_ctor_get(x_16, 1);
lean_inc(x_18);
lean_dec(x_16);
x_19 = lean_level_mk_imax(x_17, x_5);
x_19 = l_Lean_mkLevelIMax(x_17, x_5);
x_3 = x_11;
x_4 = lean_box(0);
x_5 = x_19;
@ -22713,7 +22702,7 @@ lean_dec(x_2);
x_62 = lean_ctor_get(x_1, 0);
lean_inc(x_62);
lean_dec(x_1);
x_63 = lean_level_mk_succ(x_62);
x_63 = l_Lean_mkLevelSucc(x_62);
x_64 = l_Lean_mkSort(x_63);
x_65 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_65, 0, x_64);

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

@ -45,7 +45,6 @@ lean_object* l_Nat_foldMAux___main___at_Lean_Meta_inferTypeAux___spec__15(lean_o
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_inferTypeAux___spec__29___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_inferTypeAux___spec__10___lambda__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_InferType_2__inferAppType___at_Lean_Meta_inferTypeAux___spec__13(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_level_mk_mvar(lean_object*);
lean_object* lean_expr_instantiate_rev_range(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isClassQuick___main(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_InferType_13__isArrowProp___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -122,7 +121,6 @@ lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* l_Lean_Meta_getLocalDecl(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_inferTypeAux___spec__25___lambda__1___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_isClassExpensive___main___at_Lean_Meta_inferTypeAux___spec__6(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_level_mk_imax(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_8__forallTelescopeReducingAux___at_Lean_Meta_inferTypeAux___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern size_t l_PersistentHashMap_insertAux___main___rarg___closed__2;
lean_object* l___private_Init_Lean_Meta_InferType_6__inferForallType___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -140,7 +138,6 @@ lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_inferTypeAu
lean_object* l_Lean_Meta_instantiateLevelMVars(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_InferType_8__withLocalDecl___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_7__forallTelescopeReducingAuxAux___main___at_Lean_Meta_inferTypeAux___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_level_mk_succ(lean_object*);
lean_object* l___private_Init_Lean_Meta_InferType_6__inferForallType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentHashMap_insertAux___main___at___private_Init_Lean_Meta_InferType_11__checkInferTypeCache___spec__5(lean_object*, size_t, size_t, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_InferType_13__isArrowProp(lean_object*, lean_object*, lean_object*, lean_object*);
@ -157,6 +154,7 @@ lean_object* l_Lean_mkProj(lean_object*, lean_object*, lean_object*);
extern lean_object* l_PersistentHashMap_insertAux___main___rarg___closed__3;
lean_object* lean_array_get_size(lean_object*);
lean_object* l_Nat_foldMAux___main___at_Lean_Meta_inferTypeAux___spec__34(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLevelSucc(lean_object*);
extern lean_object* l_EIO_Monad___closed__1;
lean_object* l___private_Init_Lean_Meta_InferType_4__inferProjType___at_Lean_Meta_inferTypeAux___spec__31(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_inferTypeAux___spec__9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -177,8 +175,10 @@ lean_object* l___private_Init_Lean_Meta_InferType_5__getLevel___at_Lean_Meta_inf
uint8_t l_USize_decLe(size_t, size_t);
extern lean_object* l_Lean_Meta_isClassQuick___main___closed__1;
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_inferTypeAux___spec__28(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLevelIMax(lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_inferTypeAux___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLevelMVar(lean_object*);
lean_object* l___private_Init_Lean_Meta_InferType_13__isArrowProp___main(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_unreachable_x21___rarg(lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_inferTypeAux___spec__10(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1832,7 +1832,7 @@ lean_inc(x_18);
x_19 = lean_ctor_get(x_17, 1);
lean_inc(x_19);
lean_dec(x_17);
x_20 = lean_level_mk_mvar(x_18);
x_20 = l_Lean_mkLevelMVar(x_18);
lean_inc(x_20);
x_21 = l_Lean_mkSort(x_20);
x_22 = l_Lean_Meta_assignExprMVar(x_12, x_21, x_4, x_19);
@ -2132,7 +2132,7 @@ if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_11, 0);
x_14 = lean_level_mk_imax(x_13, x_5);
x_14 = l_Lean_mkLevelIMax(x_13, x_5);
lean_ctor_set(x_11, 0, x_14);
return x_11;
}
@ -2144,7 +2144,7 @@ x_16 = lean_ctor_get(x_11, 1);
lean_inc(x_16);
lean_inc(x_15);
lean_dec(x_11);
x_17 = lean_level_mk_imax(x_15, x_5);
x_17 = l_Lean_mkLevelIMax(x_15, x_5);
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_16);
@ -3947,7 +3947,7 @@ lean_dec(x_1);
x_66 = lean_ctor_get(x_2, 0);
lean_inc(x_66);
lean_dec(x_2);
x_67 = lean_level_mk_succ(x_66);
x_67 = l_Lean_mkLevelSucc(x_66);
x_68 = l_Lean_mkSort(x_67);
x_69 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_69, 0, x_68);
@ -8203,7 +8203,7 @@ lean_inc(x_23);
x_24 = lean_ctor_get(x_22, 1);
lean_inc(x_24);
lean_dec(x_22);
x_25 = lean_level_mk_mvar(x_23);
x_25 = l_Lean_mkLevelMVar(x_23);
lean_inc(x_25);
x_26 = l_Lean_mkSort(x_25);
x_27 = l_Lean_Meta_assignExprMVar(x_17, x_26, x_3, x_24);
@ -8507,7 +8507,7 @@ lean_inc(x_93);
x_94 = lean_ctor_get(x_92, 1);
lean_inc(x_94);
lean_dec(x_92);
x_95 = lean_level_mk_mvar(x_93);
x_95 = l_Lean_mkLevelMVar(x_93);
lean_inc(x_95);
x_96 = l_Lean_mkSort(x_95);
x_97 = l_Lean_Meta_assignExprMVar(x_87, x_96, x_3, x_94);
@ -8820,7 +8820,7 @@ lean_inc(x_23);
x_24 = lean_ctor_get(x_22, 1);
lean_inc(x_24);
lean_dec(x_22);
x_25 = lean_level_mk_mvar(x_23);
x_25 = l_Lean_mkLevelMVar(x_23);
lean_inc(x_25);
x_26 = l_Lean_mkSort(x_25);
x_27 = l_Lean_Meta_assignExprMVar(x_17, x_26, x_3, x_24);
@ -9124,7 +9124,7 @@ lean_inc(x_93);
x_94 = lean_ctor_get(x_92, 1);
lean_inc(x_94);
lean_dec(x_92);
x_95 = lean_level_mk_mvar(x_93);
x_95 = l_Lean_mkLevelMVar(x_93);
lean_inc(x_95);
x_96 = l_Lean_mkSort(x_95);
x_97 = l_Lean_Meta_assignExprMVar(x_87, x_96, x_3, x_94);
@ -9400,7 +9400,7 @@ lean_inc(x_18);
x_19 = lean_ctor_get(x_17, 1);
lean_inc(x_19);
lean_dec(x_17);
x_20 = lean_level_mk_imax(x_18, x_6);
x_20 = l_Lean_mkLevelIMax(x_18, x_6);
x_4 = x_12;
x_5 = lean_box(0);
x_6 = x_20;
@ -15408,7 +15408,7 @@ lean_dec(x_1);
x_63 = lean_ctor_get(x_2, 0);
lean_inc(x_63);
lean_dec(x_2);
x_64 = lean_level_mk_succ(x_63);
x_64 = l_Lean_mkLevelSucc(x_63);
x_65 = l_Lean_mkSort(x_64);
x_66 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_66, 0, x_65);

14
stage0/library/Init/Lean/Meta/LevelDefEq.c generated
View file

@ -19,6 +19,7 @@ lean_object* l___private_Init_Lean_Meta_LevelDefEq_1__strictOccursMaxAux___main_
extern lean_object* l_Array_empty___closed__1;
lean_object* l___private_Init_Lean_Meta_LevelDefEq_3__mkMaxArgsDiff___main___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___closed__3;
lean_object* l_Lean_mkLevelMax(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_5__postponeIsLevelDefEq(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_13__restore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_5__postponeIsLevelDefEq___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -29,7 +30,6 @@ lean_object* l___private_Init_Lean_Meta_LevelDefEq_7__isLevelDefEqAux___main___c
lean_object* l___private_Init_Lean_Meta_LevelDefEq_7__isLevelDefEqAux___main___closed__6;
lean_object* l___private_Init_Lean_Meta_LevelDefEq_11__processPostponedAux___main___closed__6;
lean_object* l___private_Init_Lean_Trace_3__addTrace___at___private_Init_Lean_Meta_LevelDefEq_7__isLevelDefEqAux___main___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_level_mk_mvar(lean_object*);
lean_object* l___private_Init_Lean_Trace_2__getResetTraces___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__6___rarg(lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkFreshLevelMVarId___rarg(lean_object*);
@ -113,6 +113,7 @@ lean_object* l___private_Init_Lean_Meta_LevelDefEq_8__getNumPostponed___boxed(le
uint8_t l_Lean_MetavarContext_hasAssignableLevelMVar___main(lean_object*, lean_object*);
uint8_t l_Lean_Level_isMVar(lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_3__mkMaxArgsDiff___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLevelMVar(lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_6__getLevelConstraintKind(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_12__processPostponed___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_7__isLevelDefEqAux___main___closed__3;
@ -122,7 +123,6 @@ lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_8__getNumPostponed___rarg(lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_2__strictOccursMax___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_9__getResetPostponed___rarg(lean_object*);
lean_object* lean_level_mk_max(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_LevelDefEq_7__isLevelDefEqAux___main___closed__4;
lean_object* l___private_Init_Lean_Meta_LevelDefEq_12__processPostponed(uint8_t, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Trace_1__addNode___at___private_Init_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -273,7 +273,7 @@ lean_dec(x_8);
if (x_9 == 0)
{
lean_object* x_10;
x_10 = lean_level_mk_max(x_3, x_2);
x_10 = l_Lean_mkLevelMax(x_3, x_2);
return x_10;
}
else
@ -285,7 +285,7 @@ return x_3;
default:
{
lean_object* x_11;
x_11 = lean_level_mk_max(x_3, x_2);
x_11 = l_Lean_mkLevelMax(x_3, x_2);
return x_11;
}
}
@ -328,7 +328,7 @@ x_6 = lean_ctor_get(x_4, 1);
lean_inc(x_6);
lean_dec(x_4);
lean_inc(x_5);
x_7 = lean_level_mk_mvar(x_5);
x_7 = l_Lean_mkLevelMVar(x_5);
x_8 = l___private_Init_Lean_Meta_LevelDefEq_3__mkMaxArgsDiff___main(x_5, x_1, x_7);
x_9 = l_Lean_Meta_assignLevelMVar(x_5, x_8, x_2, x_6);
return x_9;
@ -895,12 +895,10 @@ lean_dec(x_14);
lean_dec(x_9);
x_19 = lean_ctor_get(x_13, 1);
lean_inc(x_19);
lean_inc(x_1);
x_196 = l_Lean_MetavarContext_hasAssignableLevelMVar___main(x_19, x_1);
if (x_196 == 0)
{
uint8_t x_197;
lean_inc(x_2);
x_197 = l_Lean_MetavarContext_hasAssignableLevelMVar___main(x_19, x_2);
lean_dec(x_19);
if (x_197 == 0)
@ -1666,12 +1664,10 @@ lean_dec(x_204);
lean_dec(x_9);
x_209 = lean_ctor_get(x_203, 1);
lean_inc(x_209);
lean_inc(x_1);
x_309 = l_Lean_MetavarContext_hasAssignableLevelMVar___main(x_209, x_1);
if (x_309 == 0)
{
uint8_t x_310;
lean_inc(x_2);
x_310 = l_Lean_MetavarContext_hasAssignableLevelMVar___main(x_209, x_2);
lean_dec(x_209);
if (x_310 == 0)

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

@ -85,7 +85,7 @@ lean_object* l_PersistentArray_foldlFromM___at___private_Init_Lean_MetavarContex
lean_object* l_Array_anyRangeMAux___main___at___private_Init_Lean_MetavarContext_13__collectDeps___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_monadInhabited___rarg(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_find___at_Lean_MetavarContext_findLevelDepth___spec__1___boxed(lean_object*, lean_object*);
uint8_t lean_level_has_mvar(lean_object*);
uint8_t l_Lean_Level_hasMVar(lean_object*);
lean_object* l_PersistentHashMap_containsAux___main___at_Lean_MetavarContext_isDelayedAssigned___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_MetavarContext_assignExpr___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MetavarContext_isLevelAssignable___closed__2;
@ -5358,8 +5358,7 @@ lean_object* x_3; uint8_t x_4;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
lean_dec(x_2);
lean_inc(x_3);
x_4 = lean_level_has_mvar(x_3);
x_4 = l_Lean_Level_hasMVar(x_3);
if (x_4 == 0)
{
uint8_t x_5;
@ -5382,14 +5381,12 @@ lean_inc(x_7);
x_8 = lean_ctor_get(x_2, 1);
lean_inc(x_8);
lean_dec(x_2);
lean_inc(x_7);
x_9 = lean_level_has_mvar(x_7);
x_9 = l_Lean_Level_hasMVar(x_7);
if (x_9 == 0)
{
uint8_t x_10;
lean_dec(x_7);
lean_inc(x_8);
x_10 = lean_level_has_mvar(x_8);
x_10 = l_Lean_Level_hasMVar(x_8);
if (x_10 == 0)
{
uint8_t x_11;
@ -5412,8 +5409,7 @@ x_13 = l_Lean_MetavarContext_hasAssignedLevelMVar___main(x_1, x_7);
if (x_13 == 0)
{
uint8_t x_14;
lean_inc(x_8);
x_14 = lean_level_has_mvar(x_8);
x_14 = l_Lean_Level_hasMVar(x_8);
if (x_14 == 0)
{
lean_dec(x_8);
@ -5444,14 +5440,12 @@ lean_inc(x_17);
x_18 = lean_ctor_get(x_2, 1);
lean_inc(x_18);
lean_dec(x_2);
lean_inc(x_17);
x_19 = lean_level_has_mvar(x_17);
x_19 = l_Lean_Level_hasMVar(x_17);
if (x_19 == 0)
{
uint8_t x_20;
lean_dec(x_17);
lean_inc(x_18);
x_20 = lean_level_has_mvar(x_18);
x_20 = l_Lean_Level_hasMVar(x_18);
if (x_20 == 0)
{
uint8_t x_21;
@ -5474,8 +5468,7 @@ x_23 = l_Lean_MetavarContext_hasAssignedLevelMVar___main(x_1, x_17);
if (x_23 == 0)
{
uint8_t x_24;
lean_inc(x_18);
x_24 = lean_level_has_mvar(x_18);
x_24 = l_Lean_Level_hasMVar(x_18);
if (x_24 == 0)
{
lean_dec(x_18);
@ -6049,14 +6042,10 @@ case 1:
{
lean_object* x_3; uint8_t x_4;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
lean_dec(x_2);
lean_inc(x_3);
x_4 = lean_level_has_mvar(x_3);
x_4 = l_Lean_Level_hasMVar(x_3);
if (x_4 == 0)
{
uint8_t x_5;
lean_dec(x_3);
x_5 = 0;
return x_5;
}
@ -6070,22 +6059,15 @@ case 2:
{
lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_7 = lean_ctor_get(x_2, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_2, 1);
lean_inc(x_8);
lean_dec(x_2);
lean_inc(x_7);
x_9 = lean_level_has_mvar(x_7);
x_9 = l_Lean_Level_hasMVar(x_7);
if (x_9 == 0)
{
uint8_t x_10;
lean_dec(x_7);
lean_inc(x_8);
x_10 = lean_level_has_mvar(x_8);
x_10 = l_Lean_Level_hasMVar(x_8);
if (x_10 == 0)
{
uint8_t x_11;
lean_dec(x_8);
x_11 = 0;
return x_11;
}
@ -6102,11 +6084,9 @@ x_13 = l_Lean_MetavarContext_hasAssignableLevelMVar___main(x_1, x_7);
if (x_13 == 0)
{
uint8_t x_14;
lean_inc(x_8);
x_14 = lean_level_has_mvar(x_8);
x_14 = l_Lean_Level_hasMVar(x_8);
if (x_14 == 0)
{
lean_dec(x_8);
return x_13;
}
else
@ -6118,7 +6098,6 @@ goto _start;
else
{
uint8_t x_16;
lean_dec(x_8);
x_16 = 1;
return x_16;
}
@ -6128,22 +6107,15 @@ case 3:
{
lean_object* x_17; lean_object* x_18; uint8_t x_19;
x_17 = lean_ctor_get(x_2, 0);
lean_inc(x_17);
x_18 = lean_ctor_get(x_2, 1);
lean_inc(x_18);
lean_dec(x_2);
lean_inc(x_17);
x_19 = lean_level_has_mvar(x_17);
x_19 = l_Lean_Level_hasMVar(x_17);
if (x_19 == 0)
{
uint8_t x_20;
lean_dec(x_17);
lean_inc(x_18);
x_20 = lean_level_has_mvar(x_18);
x_20 = l_Lean_Level_hasMVar(x_18);
if (x_20 == 0)
{
uint8_t x_21;
lean_dec(x_18);
x_21 = 0;
return x_21;
}
@ -6160,11 +6132,9 @@ x_23 = l_Lean_MetavarContext_hasAssignableLevelMVar___main(x_1, x_17);
if (x_23 == 0)
{
uint8_t x_24;
lean_inc(x_18);
x_24 = lean_level_has_mvar(x_18);
x_24 = l_Lean_Level_hasMVar(x_18);
if (x_24 == 0)
{
lean_dec(x_18);
return x_23;
}
else
@ -6176,7 +6146,6 @@ goto _start;
else
{
uint8_t x_26;
lean_dec(x_18);
x_26 = 1;
return x_26;
}
@ -6186,16 +6155,12 @@ case 5:
{
lean_object* x_27; uint8_t x_28;
x_27 = lean_ctor_get(x_2, 0);
lean_inc(x_27);
lean_dec(x_2);
x_28 = l_Lean_MetavarContext_isLevelAssignable(x_1, x_27);
lean_dec(x_27);
return x_28;
}
default:
{
uint8_t x_29;
lean_dec(x_2);
x_29 = 0;
return x_29;
}
@ -6207,6 +6172,7 @@ _start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Lean_MetavarContext_hasAssignableLevelMVar___main(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
@ -6225,6 +6191,7 @@ _start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Lean_MetavarContext_hasAssignableLevelMVar(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
@ -6366,8 +6333,7 @@ lean_dec(x_1);
x_43 = lean_ctor_get(x_41, 0);
lean_inc(x_43);
lean_dec(x_41);
lean_inc(x_43);
x_44 = lean_level_has_mvar(x_43);
x_44 = l_Lean_Level_hasMVar(x_43);
if (x_44 == 0)
{
lean_object* x_45;

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

@ -33,11 +33,12 @@ lean_object* l_Lean_TypeClass_Context__u03b1Norm___closed__1;
lean_object* l_Lean_Format_pretty(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eInfer(lean_object*, lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLevelMax(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eMetaIdx(lean_object*);
lean_object* lean_mk_array(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_uAssignIdx___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_monadInhabited___rarg(lean_object*, lean_object*);
uint8_t lean_level_has_mvar(lean_object*);
uint8_t l_Lean_Level_hasMVar(lean_object*);
lean_object* l_PersistentArray_get_x21___at_Lean_TypeClass_Context_eLookupIdx___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context__u03b1Norm(lean_object*);
lean_object* lean_expr_dbg_to_string(lean_object*);
@ -51,9 +52,9 @@ lean_object* l_Lean_TypeClass_Context_uUnify___main___closed__4;
uint8_t l_Lean_TypeClass_Context_eFind(lean_object*, lean_object*);
lean_object* l_PersistentArray_get_x21___at_Lean_TypeClass_Context_uLookupIdx___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eAssign___closed__3;
lean_object* lean_level_mk_mvar(lean_object*);
lean_object* l_Lean_TypeClass_Context_eFind___main___boxed(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eInferIdx(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_uInstantiate___boxed(lean_object*, lean_object*);
size_t l_USize_sub(size_t, size_t);
lean_object* l_Lean_TypeClass_Context_eShallowInstantiate(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_uMetaNormalizeCore(lean_object*);
@ -104,6 +105,7 @@ lean_object* l_Lean_TypeClass_Context_eIsMeta___boxed(lean_object*);
lean_object* l_Lean_TypeClass_Context__u03b1Norm___lambda__2(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_uIsMeta___boxed(lean_object*);
uint8_t lean_expr_eqv(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_uInstantiate___main___boxed(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eUnify___main___closed__4;
lean_object* l_List_map___main___at_Lean_TypeClass_Context_eInstantiate___main___spec__1(lean_object*, lean_object*);
lean_object* l_Nat_forMAux___main___at_Lean_TypeClass_Context_eUnify___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -145,7 +147,6 @@ extern lean_object* l_unreachable_x21___rarg___closed__2;
lean_object* l_PersistentArray_getAux___main___at_Lean_TypeClass_Context_eLookupIdx___spec__2(lean_object*, size_t, size_t);
lean_object* l_Lean_mkForall(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eAssignIdx(lean_object*, lean_object*, lean_object*);
lean_object* lean_level_mk_imax(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isFVar(lean_object*);
lean_object* l_PersistentArray_getAux___main___at_Lean_TypeClass_Context_eInferIdx___spec__2(lean_object*, size_t, size_t);
lean_object* l___private_Init_Util_1__mkPanicMessage(lean_object*, lean_object*, lean_object*, lean_object*);
@ -160,7 +161,6 @@ uint8_t l_Lean_Expr_isMVar(lean_object*);
lean_object* l_Lean_TypeClass_Context_eUnify(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context__u03b1Norm___lambda__3(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eInfer___closed__1;
lean_object* lean_level_mk_succ(lean_object*);
lean_object* l_panic(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_eInstantiate___main(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Expr_3__getAppArgsAux___main(lean_object*, lean_object*, lean_object*);
@ -183,6 +183,7 @@ lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_TypeClass_Context_eUnify___main(lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentArray_get_x21___at_Lean_TypeClass_Context_uLookupIdx___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_internalize___closed__1;
lean_object* l_Lean_mkLevelSucc(lean_object*);
lean_object* l_Lean_TypeClass_Context_eInfer___boxed(lean_object*, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_metaPrefix;
@ -215,7 +216,9 @@ lean_object* l_PersistentArray_getAux___main___at_Lean_TypeClass_Context_uLookup
lean_object* l_Lean_TypeClass_Context_eMetaNormalizeCore___main(lean_object*);
lean_object* l_Lean_TypeClass_Context_uAssign(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isBVar(lean_object*);
lean_object* l_Lean_mkLevelIMax(lean_object*, lean_object*);
lean_object* l_RBNode_ins___main___at_Lean_TypeClass_Context__u03b1Norm___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLevelMVar(lean_object*);
lean_object* l_PersistentArray_getAux___main___at_Lean_TypeClass_Context_uLookupIdx___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context_uUnify___main(lean_object*, lean_object*, lean_object*);
size_t l_USize_land(size_t, size_t);
@ -228,7 +231,6 @@ lean_object* l_Lean_TypeClass_Context_uUnify___main___closed__2;
uint8_t l_Lean_TypeClass_Context_eHasTmpMVar___lambda__1(lean_object*);
lean_object* l_Lean_TypeClass_Context_eHasTmpMVar___lambda__1___boxed(lean_object*);
lean_object* l_Lean_TypeClass_Context_internalize___closed__3;
lean_object* lean_level_mk_max(lean_object*, lean_object*);
lean_object* l_Lean_TypeClass_Context__u03b1Norm___closed__2;
lean_object* l_Lean_TypeClass_Context_uAssign___closed__1;
lean_object* l_Lean_TypeClass_Context_uUnify___main___closed__5;
@ -1265,7 +1267,7 @@ x_6 = l_PersistentArray_push___rarg(x_3, x_5);
lean_ctor_set(x_1, 0, x_6);
x_7 = l_Lean_TypeClass_Context_metaPrefix;
x_8 = lean_name_mk_numeral(x_7, x_4);
x_9 = lean_level_mk_mvar(x_8);
x_9 = l_Lean_mkLevelMVar(x_8);
x_10 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_10, 0, x_9);
lean_ctor_set(x_10, 1, x_1);
@ -1291,7 +1293,7 @@ lean_ctor_set(x_17, 1, x_12);
lean_ctor_set(x_17, 2, x_13);
x_18 = l_Lean_TypeClass_Context_metaPrefix;
x_19 = lean_name_mk_numeral(x_18, x_14);
x_20 = lean_level_mk_mvar(x_19);
x_20 = l_Lean_mkLevelMVar(x_19);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_17);
@ -1928,6 +1930,8 @@ case 0:
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_11; lean_object* x_12;
lean_dec(x_8);
lean_dec(x_5);
x_11 = lean_box(0);
x_12 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_12, 0, x_11);
@ -2273,11 +2277,11 @@ lean_object* l_Lean_TypeClass_Context_uInstantiate___main(lean_object* x_1, lean
_start:
{
uint8_t x_3;
lean_inc(x_2);
x_3 = lean_level_has_mvar(x_2);
x_3 = l_Lean_Level_hasMVar(x_2);
if (x_3 == 0)
{
lean_dec(x_1);
lean_inc(x_2);
return x_2;
}
else
@ -2291,43 +2295,36 @@ case 1:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = lean_ctor_get(x_2, 0);
lean_inc(x_5);
lean_dec(x_2);
x_6 = l_Lean_TypeClass_Context_uInstantiate___main(x_1, x_5);
x_7 = lean_level_mk_succ(x_6);
x_7 = l_Lean_mkLevelSucc(x_6);
return x_7;
}
case 2:
{
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_2, 0);
lean_inc(x_8);
x_9 = lean_ctor_get(x_2, 1);
lean_inc(x_9);
lean_dec(x_2);
lean_inc(x_1);
x_10 = l_Lean_TypeClass_Context_uInstantiate___main(x_1, x_8);
x_11 = l_Lean_TypeClass_Context_uInstantiate___main(x_1, x_9);
x_12 = lean_level_mk_max(x_10, x_11);
x_12 = l_Lean_mkLevelMax(x_10, x_11);
return x_12;
}
case 3:
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_13 = lean_ctor_get(x_2, 0);
lean_inc(x_13);
x_14 = lean_ctor_get(x_2, 1);
lean_inc(x_14);
lean_dec(x_2);
lean_inc(x_1);
x_15 = l_Lean_TypeClass_Context_uInstantiate___main(x_1, x_13);
x_16 = l_Lean_TypeClass_Context_uInstantiate___main(x_1, x_14);
x_17 = lean_level_mk_imax(x_15, x_16);
x_17 = l_Lean_mkLevelIMax(x_15, x_16);
return x_17;
}
default:
{
lean_dec(x_1);
lean_inc(x_2);
return x_2;
}
}
@ -2347,22 +2344,32 @@ lean_dec(x_19);
if (lean_obj_tag(x_20) == 0)
{
lean_dec(x_1);
lean_inc(x_2);
return x_2;
}
else
{
lean_object* x_21;
lean_dec(x_2);
lean_object* x_21; lean_object* x_22;
x_21 = lean_ctor_get(x_20, 0);
lean_inc(x_21);
lean_dec(x_20);
x_2 = x_21;
goto _start;
x_22 = l_Lean_TypeClass_Context_uInstantiate___main(x_1, x_21);
lean_dec(x_21);
return x_22;
}
}
}
}
}
lean_object* l_Lean_TypeClass_Context_uInstantiate___main___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_TypeClass_Context_uInstantiate___main(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Lean_TypeClass_Context_uInstantiate(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -2371,6 +2378,15 @@ x_3 = l_Lean_TypeClass_Context_uInstantiate___main(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_TypeClass_Context_uInstantiate___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_TypeClass_Context_uInstantiate(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
uint8_t l_List_foldr___main___at_Lean_TypeClass_Context_eHasTmpMVar___spec__1(uint8_t x_1, lean_object* x_2) {
_start:
{
@ -3651,6 +3667,7 @@ x_5 = lean_ctor_get(x_2, 0);
x_6 = lean_ctor_get(x_2, 1);
lean_inc(x_1);
x_7 = l_Lean_TypeClass_Context_uInstantiate___main(x_1, x_5);
lean_dec(x_5);
x_8 = l_List_map___main___at_Lean_TypeClass_Context_eInstantiate___main___spec__1(x_1, x_6);
lean_ctor_set(x_2, 1, x_8);
lean_ctor_set(x_2, 0, x_7);
@ -3666,6 +3683,7 @@ lean_inc(x_9);
lean_dec(x_2);
lean_inc(x_1);
x_11 = l_Lean_TypeClass_Context_uInstantiate___main(x_1, x_9);
lean_dec(x_9);
x_12 = l_List_map___main___at_Lean_TypeClass_Context_eInstantiate___main___spec__1(x_1, x_10);
x_13 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_13, 0, x_11);
@ -3847,8 +3865,7 @@ lean_object* l_Lean_TypeClass_Context_uMetaNormalizeCore___main___rarg(lean_obje
_start:
{
uint8_t x_4;
lean_inc(x_2);
x_4 = lean_level_has_mvar(x_2);
x_4 = l_Lean_Level_hasMVar(x_2);
if (x_4 == 0)
{
lean_object* x_5;
@ -3873,7 +3890,7 @@ if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10;
x_9 = lean_ctor_get(x_7, 0);
x_10 = lean_level_mk_succ(x_9);
x_10 = l_Lean_mkLevelSucc(x_9);
lean_ctor_set(x_7, 0, x_10);
return x_7;
}
@ -3885,7 +3902,7 @@ x_12 = lean_ctor_get(x_7, 1);
lean_inc(x_12);
lean_inc(x_11);
lean_dec(x_7);
x_13 = lean_level_mk_succ(x_11);
x_13 = l_Lean_mkLevelSucc(x_11);
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_12);
@ -3913,7 +3930,7 @@ if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23;
x_22 = lean_ctor_get(x_20, 0);
x_23 = lean_level_mk_max(x_18, x_22);
x_23 = l_Lean_mkLevelMax(x_18, x_22);
lean_ctor_set(x_20, 0, x_23);
return x_20;
}
@ -3925,7 +3942,7 @@ x_25 = lean_ctor_get(x_20, 1);
lean_inc(x_25);
lean_inc(x_24);
lean_dec(x_20);
x_26 = lean_level_mk_max(x_18, x_24);
x_26 = l_Lean_mkLevelMax(x_18, x_24);
x_27 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_27, 0, x_26);
lean_ctor_set(x_27, 1, x_25);
@ -3953,7 +3970,7 @@ if (x_34 == 0)
{
lean_object* x_35; lean_object* x_36;
x_35 = lean_ctor_get(x_33, 0);
x_36 = lean_level_mk_imax(x_31, x_35);
x_36 = l_Lean_mkLevelIMax(x_31, x_35);
lean_ctor_set(x_33, 0, x_36);
return x_33;
}
@ -3965,7 +3982,7 @@ x_38 = lean_ctor_get(x_33, 1);
lean_inc(x_38);
lean_inc(x_37);
lean_dec(x_33);
x_39 = lean_level_mk_imax(x_31, x_37);
x_39 = l_Lean_mkLevelIMax(x_31, x_37);
x_40 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_38);
@ -6854,7 +6871,7 @@ x_6 = l_RBNode_fold___main___at_RBMap_size___spec__1___rarg(x_5, x_4);
x_7 = l_Lean_TypeClass_Context_alphaMetaPrefix;
lean_inc(x_6);
x_8 = lean_name_mk_numeral(x_7, x_6);
x_9 = lean_level_mk_mvar(x_8);
x_9 = l_Lean_mkLevelMVar(x_8);
x_10 = l_RBNode_insert___at_Lean_TypeClass_Context__u03b1Norm___spec__1(x_4, x_1, x_6);
lean_ctor_set(x_2, 2, x_10);
x_11 = lean_alloc_ctor(0, 2, 0);
@ -6877,7 +6894,7 @@ x_16 = l_RBNode_fold___main___at_RBMap_size___spec__1___rarg(x_15, x_14);
x_17 = l_Lean_TypeClass_Context_alphaMetaPrefix;
lean_inc(x_16);
x_18 = lean_name_mk_numeral(x_17, x_16);
x_19 = lean_level_mk_mvar(x_18);
x_19 = l_Lean_mkLevelMVar(x_18);
x_20 = l_RBNode_insert___at_Lean_TypeClass_Context__u03b1Norm___spec__1(x_14, x_1, x_16);
x_21 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_21, 0, x_12);
@ -6896,7 +6913,7 @@ _start:
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = l_Lean_TypeClass_Context_alphaMetaPrefix;
x_4 = lean_name_mk_numeral(x_3, x_1);
x_5 = lean_level_mk_mvar(x_4);
x_5 = l_Lean_mkLevelMVar(x_4);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_5);
lean_ctor_set(x_6, 1, x_2);
@ -7315,7 +7332,7 @@ _start:
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = l_Lean_TypeClass_Context_metaPrefix;
x_4 = lean_name_mk_numeral(x_3, x_1);
x_5 = lean_level_mk_mvar(x_4);
x_5 = l_Lean_mkLevelMVar(x_4);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_5);
lean_ctor_set(x_6, 1, x_2);

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

@ -32,7 +32,7 @@ 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;
uint8_t lean_level_has_mvar(lean_object*);
uint8_t l_Lean_Level_hasMVar(lean_object*);
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;
@ -4065,8 +4065,7 @@ lean_inc(x_7);
x_8 = lean_ctor_get(x_1, 1);
lean_inc(x_8);
lean_dec(x_1);
lean_inc(x_7);
x_9 = lean_level_has_mvar(x_7);
x_9 = l_Lean_Level_hasMVar(x_7);
if (x_9 == 0)
{
lean_object* x_10;

165
stage0/src/kernel/level.cpp generated
View file

@ -17,147 +17,29 @@ Author: Leonardo de Moura
#include "kernel/environment.h"
namespace lean {
constexpr unsigned g_level_num_scalars = 2*sizeof(unsigned) + 2*sizeof(unsigned char);
inline static void set_level_scalar_fields(object * lvl, unsigned num_objs, unsigned hash, unsigned depth, bool has_param, bool has_meta) {
cnstr_set_scalar<unsigned>(lvl, num_objs*sizeof(object*), hash);
cnstr_set_scalar<unsigned>(lvl, num_objs*sizeof(object*) + sizeof(unsigned), depth);
cnstr_set_scalar<unsigned char>(lvl, num_objs*sizeof(object*) + 2*sizeof(unsigned), has_param);
cnstr_set_scalar<unsigned char>(lvl, num_objs*sizeof(object*) + 2*sizeof(unsigned) + sizeof(unsigned char), has_meta);
}
extern "C" usize lean_level_hash(obj_arg l);
extern "C" unsigned lean_level_depth(obj_arg l);
extern "C" uint8 lean_level_has_mvar(obj_arg l);
extern "C" uint8 lean_level_has_param(obj_arg l);
inline static unsigned get_hash(object * lvl, unsigned num_objs) { return cnstr_get_scalar<unsigned>(lvl, num_objs*sizeof(object*)); }
inline static unsigned get_depth(object * lvl, unsigned num_objs) { return cnstr_get_scalar<unsigned>(lvl, num_objs*sizeof(object*) + sizeof(unsigned)); }
inline static bool get_has_param(object * lvl, unsigned num_objs) { return cnstr_get_scalar<unsigned char>(lvl, num_objs*sizeof(object*) + 2*sizeof(unsigned)); }
inline static bool get_has_mvar(object * lvl, unsigned num_objs) { return cnstr_get_scalar<unsigned char>(lvl, num_objs*sizeof(object*) + 2*sizeof(unsigned) + sizeof(unsigned char)); }
extern "C" object * lean_level_mk_zero(object*);
extern "C" object * lean_level_mk_succ(obj_arg);
extern "C" object * lean_level_mk_mvar(obj_arg);
extern "C" object * lean_level_mk_param(obj_arg);
extern "C" object * lean_level_mk_max(obj_arg, obj_arg);
extern "C" object * lean_level_mk_imax(obj_arg, obj_arg);
static inline level_kind get_level_kind(obj_arg l) { return static_cast<level_kind>(obj_tag(l)); }
level mk_succ(level const & l) { return level(lean_level_mk_succ(l.to_obj_arg())); }
level mk_max_core(level const & l1, level const & l2) { return level(lean_level_mk_max(l1.to_obj_arg(), l2.to_obj_arg())); }
level mk_imax_core(level const & l1, level const & l2) { return level(lean_level_mk_imax(l1.to_obj_arg(), l2.to_obj_arg())); }
level mk_univ_param(name const & n) { return level(lean_level_mk_param(n.to_obj_arg())); }
level mk_univ_mvar(name const & n) { return level(lean_level_mk_mvar(n.to_obj_arg())); }
unsigned level::hash(b_obj_arg l) {
switch (get_level_kind(l)) {
case level_kind::Zero:
return 31;
case level_kind::Param: case level_kind::MVar:
return name::hash(cnstr_get(l, 0));
case level_kind::Succ:
return get_hash(l, 1);
case level_kind::Max: case level_kind::IMax:
return get_hash(l, 2);
}
lean_unreachable(); // LCOV_EXCL_LINE
}
extern "C" size_t lean_level_hash(b_obj_arg l) { return level::hash(l); }
unsigned level_depth(b_obj_arg l) {
switch (get_level_kind(l)) {
case level_kind::Zero: case level_kind::Param: case level_kind::MVar:
return 1;
case level_kind::Succ:
return get_depth(l, 1);
case level_kind::Max: case level_kind::IMax:
return get_depth(l, 2);
}
lean_unreachable(); // LCOV_EXCL_LINE
}
extern "C" object * lean_level_depth(b_obj_arg l) { return mk_nat_obj(level_depth(l)); }
extern "C" uint8 lean_level_has_param(b_obj_arg l) {
switch (get_level_kind(l)) {
case level_kind::Zero: case level_kind::MVar:
return false;
case level_kind::Param:
return true;
case level_kind::Succ:
return get_has_param(l, 1);
case level_kind::Max: case level_kind::IMax:
return get_has_param(l, 2);
}
lean_unreachable(); // LCOV_EXCL_LINE
}
extern "C" uint8 lean_level_has_mvar(b_obj_arg l) {
switch (get_level_kind(l)) {
case level_kind::Zero: case level_kind::Param:
return false;
case level_kind::MVar:
return true;
case level_kind::Succ:
return get_has_mvar(l, 1);
case level_kind::Max: case level_kind::IMax:
return get_has_mvar(l, 2);
}
lean_unreachable(); // LCOV_EXCL_LINE
}
extern "C" object * lean_level_mk_succ(obj_arg l) {
object * r = alloc_cnstr(static_cast<unsigned>(level_kind::Succ), 1, g_level_num_scalars);
cnstr_set(r, 0, l);
set_level_scalar_fields(r, 1, hash(level::hash(l), 17u), level_depth(l)+1, lean_level_has_param(l), lean_level_has_mvar(l));
return r;
}
template<level_kind k> object * level_mk_max_imax(obj_arg l1, obj_arg l2) {
object * r = alloc_cnstr(static_cast<unsigned>(k), 2, g_level_num_scalars);
cnstr_set(r, 0, l1);
cnstr_set(r, 1, l2);
set_level_scalar_fields(r, 2,
hash(level::hash(l1), level::hash(l2)),
std::max(level_depth(l1), level_depth(l2)) + 1,
lean_level_has_param(l1) || lean_level_has_param(l2),
lean_level_has_mvar(l1) || lean_level_has_mvar(l2));
return r;
}
extern "C" object * lean_level_mk_max(obj_arg l1, obj_arg l2) {
return level_mk_max_imax<level_kind::Max>(l1, l2);
}
extern "C" object * lean_level_mk_imax(obj_arg l1, obj_arg l2) {
return level_mk_max_imax<level_kind::IMax>(l1, l2);
}
extern "C" object * lean_level_mk_param(obj_arg n) {
object * r = alloc_cnstr(static_cast<unsigned>(level_kind::Param), 1, 0);
cnstr_set(r, 0, n);
return r;
}
extern "C" object * lean_level_mk_mvar(obj_arg n) {
object * r = alloc_cnstr(static_cast<unsigned>(level_kind::MVar), 1, 0);
cnstr_set(r, 0, n);
return r;
}
level mk_succ(level const & l) {
inc(l.raw());
return level(lean_level_mk_succ(l.raw()));
}
level mk_max_core(level const & l1, level const & l2) {
inc(l1.raw()); inc(l2.raw());
return level(lean_level_mk_max(l1.raw(), l2.raw()));
}
level mk_imax_core(level const & l1, level const & l2) {
inc(l1.raw()); inc(l2.raw());
return level(lean_level_mk_imax(l1.raw(), l2.raw()));
}
level mk_univ_param(name const & n) {
inc(n.raw());
return level(lean_level_mk_param(n.raw()));
}
level mk_univ_mvar(name const & n) {
inc(n.raw());
return level(lean_level_mk_mvar(n.raw()));
}
unsigned get_depth(level const & l) { return level_depth(l.raw()); }
bool has_param(level const & l) { return lean_level_has_param(l.raw()); }
bool has_mvar(level const & l) { return lean_level_has_mvar(l.raw()); }
unsigned level::hash() const { return lean_level_hash(to_obj_arg()); }
unsigned get_depth(level const & l) { return lean_level_depth(l.to_obj_arg()); }
bool has_param(level const & l) { return lean_level_has_param(l.to_obj_arg()); }
bool has_mvar(level const & l) { return lean_level_has_mvar(l.to_obj_arg()); }
bool is_explicit(level const & l) {
switch (kind(l)) {
@ -477,7 +359,7 @@ static void print_child(std::ostream & out, level const & l) {
static void print(std::ostream & out, level l) {
if (is_explicit(l)) {
lean_assert(get_depth(l) > 0);
out << get_depth(l) - 1;
out << get_depth(l);
} else {
switch (kind(l)) {
case level_kind::Zero:
@ -525,7 +407,7 @@ static format pp_child(level const & l, bool unicode, unsigned indent) {
format pp(level l, bool unicode, unsigned indent) {
if (is_explicit(l)) {
lean_assert(get_depth(l) > 0);
return format(get_depth(l) - 1);
return format(get_depth(l));
} else {
switch (kind(l)) {
case level_kind::Zero:
@ -731,8 +613,11 @@ levels lparams_to_levels(names const & ps) {
return levels(ls);
}
level::level():level(*g_level_zero) {
}
void initialize_level() {
g_level_zero = new level();
g_level_zero = new level(lean_level_mk_zero(box(0)));
g_level_one = new level(mk_succ(*g_level_zero));
}

11
stage0/src/kernel/level.h generated
View file

@ -40,14 +40,13 @@ class level : public object_ref {
explicit level(object_ref && o):object_ref(o) {}
public:
/** \brief Universe zero */
level():object_ref(box(static_cast<unsigned>(level_kind::Zero))) {}
level();
explicit level(obj_arg o):object_ref(o) {}
explicit level(b_obj_arg o, bool b):object_ref(o, b) {}
level(level const & other):object_ref(other) {}
level(level && other):object_ref(other) {}
level_kind kind() const { return static_cast<level_kind>(obj_tag(raw())); }
static unsigned hash(b_obj_arg l);
unsigned hash() const { return hash(raw()); }
level_kind kind() const { return static_cast<level_kind>(lean_ptr_tag(raw())); }
unsigned hash() const;
level & operator=(level const & other) { object_ref::operator=(other); return *this; }
level & operator=(level && other) { object_ref::operator=(other); return *this; }
@ -56,7 +55,7 @@ public:
void serialize(serializer & s) const { s.write_object(raw()); }
static level deserialize(deserializer & d) { return level(d.read_object(), true); }
bool is_zero() const { lean_assert((kind() == level_kind::Zero) == is_scalar(raw())); return is_scalar(raw()); }
bool is_zero() const { return kind() == level_kind::Zero; }
bool is_succ() const { return kind() == level_kind::Succ; }
bool is_max() const { return kind() == level_kind::Max; }
bool is_imax() const { return kind() == level_kind::IMax; }
@ -160,8 +159,6 @@ bool levels_has_mvar(object * ls);
bool has_mvar(levels const & ls);
bool levels_has_param(object * ls);
bool has_param(levels const & ls);
extern "C" uint8 lean_level_has_mvar(b_obj_arg l);
extern "C" uint8 lean_level_has_param(b_obj_arg l);
/** \brief An arbitrary (monotonic) total order on universe level terms. */
bool is_lt(level const & l1, level const & l2, bool use_hash);

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_level_name() ||
n == get_task_name() ||
n == get_array_name() ||
n == get_byte_array_name() ||