From 5aa2b06bf4f1310766a4c8ead232e70dc08a209c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 17 Nov 2019 08:27:43 -0800 Subject: [PATCH] chore: update stage0 --- .../library/Init/Lean/Compiler/ConstFolding.c | 7 +- stage0/library/Init/Lean/Elaborator/PreTerm.c | 28 +- stage0/library/Init/Lean/Expr.c | 117 +- stage0/library/Init/Lean/Level.c | 1520 ++++++++++++----- stage0/library/Init/Lean/Meta/Default.c | 45 +- stage0/library/Init/Lean/Meta/InferType.c | 26 +- stage0/library/Init/Lean/Meta/LevelDefEq.c | 14 +- stage0/library/Init/Lean/MetavarContext.c | 70 +- stage0/library/Init/Lean/TypeClass/Context.c | 89 +- stage0/library/Init/Lean/TypeClass/Synth.c | 5 +- stage0/src/kernel/level.cpp | 165 +- stage0/src/kernel/level.h | 11 +- stage0/src/library/compiler/util.cpp | 1 - 13 files changed, 1328 insertions(+), 770 deletions(-) diff --git a/stage0/library/Init/Lean/Compiler/ConstFolding.c b/stage0/library/Init/Lean/Compiler/ConstFolding.c index bd5f89c138..455ccc388f 100644 --- a/stage0/library/Init/Lean/Compiler/ConstFolding.c +++ b/stage0/library/Init/Lean/Compiler/ConstFolding.c @@ -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); diff --git a/stage0/library/Init/Lean/Elaborator/PreTerm.c b/stage0/library/Init/Lean/Elaborator/PreTerm.c index 50518a8d0e..987afeea1c 100644 --- a/stage0/library/Init/Lean/Elaborator/PreTerm.c +++ b/stage0/library/Init/Lean/Elaborator/PreTerm.c @@ -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); diff --git a/stage0/library/Init/Lean/Expr.c b/stage0/library/Init/Lean/Expr.c index 0006ea7785..61f082d678 100644 --- a/stage0/library/Init/Lean/Expr.c +++ b/stage0/library/Init/Lean/Expr.c @@ -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(); diff --git a/stage0/library/Init/Lean/Level.c b/stage0/library/Init/Lean/Level.c index d360f3ead8..58491ea87d 100644 --- a/stage0/library/Init/Lean/Level.c +++ b/stage0/library/Init/Lean/Level.c @@ -15,10 +15,11 @@ extern "C" { #endif lean_object* l_Lean_Level_normLtAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_qsortAux___main___at_Lean_Level_normalize___main___spec__2___boxed(lean_object*, lean_object*, lean_object*); +uint64_t l_UInt32_toUInt64(uint32_t); lean_object* l___private_Init_Lean_Level_5__mkMaxAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Level_5__mkMaxAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Level_hasMVarEx___boxed(lean_object*); lean_object* l_Lean_Level_getOffset___boxed(lean_object*); -lean_object* l_Lean_Level_getDepth___main___boxed(lean_object*); uint8_t lean_name_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_Level_normLt___boxed(lean_object*, lean_object*); lean_object* l_Lean_Level_LevelToFormat_toResult___main___closed__1; @@ -28,121 +29,150 @@ extern lean_object* l_Array_empty___closed__1; lean_object* lean_nat_sub(lean_object*, lean_object*); lean_object* lean_array_get(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Level_ctorToNat(lean_object*); +lean_object* lean_level_mk_imax(lean_object*, lean_object*); lean_object* l_Lean_Level_LevelToFormat_Result_imax(lean_object*, lean_object*); +lean_object* l_Lean_mkLevelMax(lean_object*, lean_object*); extern lean_object* l_Lean_Format_paren___closed__2; lean_object* l_Lean_Level_instantiate(lean_object*, lean_object*); +uint8_t l_Lean_Level_Data_hasBeq(uint64_t, uint64_t); uint8_t l_Lean_Name_lt___main(lean_object*, lean_object*); +uint8_t lean_level_has_mvar(lean_object*); lean_object* l_Lean_Level_LevelToFormat_toResult(lean_object*); lean_object* l_Lean_Level_normalize___main(lean_object*); -uint8_t lean_level_has_mvar(lean_object*); +uint8_t l_Lean_Level_hasMVar(lean_object*); lean_object* l_Lean_Level_isNeverZero___main___boxed(lean_object*); lean_object* l_Lean_Level_hasMVar___boxed(lean_object*); lean_object* l_Lean_Level_normalize___main___boxed(lean_object*); +lean_object* l_Nat_toLevel(lean_object*); lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__4; +uint8_t l_UInt64_decEq(uint64_t, uint64_t); lean_object* l_Lean_Level_updateIMax___boxed(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* lean_level_mk_mvar(lean_object*); +lean_object* lean_level_mk_param(lean_object*); lean_object* l_Function_comp___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Level_getOffset(lean_object*); lean_object* l_Lean_Level_getLevelOffset___boxed(lean_object*); lean_object* l_Lean_Level_mvarId_x21___closed__2; +lean_object* l_Lean_Level_mkData___closed__2; +lean_object* lean_level_depth(lean_object*); lean_object* l_Lean_fmt___at_Lean_Level_LevelToFormat_Result_format___main___spec__1(lean_object*); lean_object* l_Lean_Level_getLevelOffset___main___boxed(lean_object*); lean_object* l_Lean_Level_LevelToFormat_Result_format___boxed(lean_object*, lean_object*); +lean_object* l_Lean_Level_Hashable___closed__1; +lean_object* l_Lean_mkLevelOne; lean_object* l___private_Init_Lean_Level_4__accMax(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*); uint8_t l_Lean_Level_normLt(lean_object*, lean_object*); +lean_object* l_Lean_Level_mkData___boxed__const__1; extern lean_object* l_Lean_Inhabited; lean_object* l_Lean_Level_beq___boxed(lean_object*, lean_object*); uint8_t l_Lean_Level_isMax(lean_object*); +lean_object* l_Lean_Level_mkData___closed__3; lean_object* l_Lean_Level_HasToString; uint8_t l___private_Init_Lean_Level_1__isAlreadyNormalizedCheap(lean_object*); -lean_object* l_Lean_Level_mvar___boxed(lean_object*); -lean_object* l_Lean_Level_getDepth(lean_object*); +lean_object* l_Lean_Level_Data_hasBeq___boxed(lean_object*, lean_object*); lean_object* l_Lean_Level_isIMax___boxed(lean_object*); +uint64_t l_UInt64_add(uint64_t, uint64_t); lean_object* l_Lean_Level_isNeverZero___boxed(lean_object*); lean_object* l_Nat_imax___boxed(lean_object*, lean_object*); lean_object* l_Lean_Level_isMVar___boxed(lean_object*); +lean_object* l_Nat_toLevel___boxed(lean_object*); lean_object* l_Lean_Level_updateMax_x21___closed__1; +uint64_t l_Bool_toUInt64(uint8_t); lean_object* l_Lean_Level_ofNat___main(lean_object*); lean_object* l_Lean_Level_format(lean_object*); lean_object* l_Lean_Level_ofNat(lean_object*); lean_object* l_Lean_Level_Lean_HasFormat; +lean_object* l_Lean_Level_Data_hash___boxed(lean_object*); +lean_object* lean_level_mk_zero(lean_object*); lean_object* l_Lean_Level_getLevelOffset(lean_object*); lean_object* lean_level_update_succ(lean_object*, lean_object*); +uint64_t l_Lean_Level_mkData(size_t, lean_object*, uint8_t, uint8_t); lean_object* l___private_Init_Lean_Level_3__getMaxArgsAux___main___at_Lean_Level_normalize___main___spec__1(lean_object*, uint8_t, lean_object*); lean_object* l_Lean_Level_instantiate___main(lean_object*, lean_object*); lean_object* l_Nat_repr(lean_object*); lean_object* l___private_Init_Lean_Level_1__isAlreadyNormalizedCheap___boxed(lean_object*); +uint64_t l_UInt64_shiftRight(uint64_t, uint64_t); +extern uint64_t l_UInt64_Inhabited; +uint32_t l_UInt64_toUInt32(uint64_t); lean_object* l_Lean_Level_occurs___boxed(lean_object*, lean_object*); lean_object* l_Lean_Level_HasToString___closed__1; +lean_object* l_Lean_mkLevelZero___closed__2; lean_object* l_Lean_Level_isMaxIMax___boxed(lean_object*); -lean_object* l_Lean_Level_mvarId_x21___closed__3; lean_object* l___private_Init_Lean_Level_6__formatLst(lean_object*, lean_object*); lean_object* l___private_Init_Lean_Level_1__isAlreadyNormalizedCheap___main___boxed(lean_object*); -lean_object* l_Lean_Level_one; +size_t lean_name_hash_usize(lean_object*); uint8_t l_Lean_Level_isExplicit___main(lean_object*); lean_object* l_Lean_Level_LevelToFormat_Result_max(lean_object*, lean_object*); lean_object* l_Lean_Level_hasParam___boxed(lean_object*); lean_object* l___private_Init_Lean_Level_6__formatLst___main___at_Lean_Level_LevelToFormat_Result_format___main___spec__2(lean_object*); +uint64_t l_UInt64_shiftLeft(uint64_t, uint64_t); lean_object* l_Lean_Level_updateSucc_x21(lean_object*, lean_object*); +uint64_t lean_uint64_of_nat(lean_object*); lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__6; +lean_object* l_Lean_Level_mkData___closed__1; lean_object* l_Lean_Level_mvarId_x21___closed__1; lean_object* l_Lean_Level_updateIMax_x21(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_mkLevelParam(lean_object*); lean_object* l_Lean_Level_getOffsetAux___main(lean_object*, lean_object*); lean_object* l___private_Init_Lean_Level_3__getMaxArgsAux___main___at_Lean_Level_normalize___main___spec__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Level_updateIMax_x21___closed__2; extern lean_object* l_Lean_Format_paren___closed__1; lean_object* l_Lean_Level_isMax___boxed(lean_object*); +lean_object* l_Lean_Level_hasParamEx___boxed(lean_object*); +lean_object* l_Lean_Level_mkData___closed__4; uint8_t l_Lean_Level_isMaxIMax(lean_object*); lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__5; lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__2; uint8_t lean_nat_dec_lt(lean_object*, lean_object*); uint8_t l_Lean_Level_isEquiv(lean_object*, lean_object*); lean_object* l_Lean_Level_dec___main___boxed(lean_object*); +lean_object* l_Lean_Level_mkData___boxed(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Level_isSucc(lean_object*); lean_object* l_Lean_Level_dec___main(lean_object*); -lean_object* l_Lean_Level_getDepth___boxed(lean_object*); lean_object* l_Lean_Level_ofNat___boxed(lean_object*); +lean_object* l_Lean_mkLevelZero; lean_object* lean_nat_add(lean_object*, lean_object*); extern lean_object* l_Lean_Format_paren___closed__3; lean_object* l_Lean_Level_toNat(lean_object*); 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_Level_toNat___boxed(lean_object*); lean_object* lean_array_push(lean_object*, lean_object*); lean_object* l_Lean_Level_updateSucc___boxed(lean_object*, lean_object*, lean_object*); +lean_object* lean_level_mk_mvar(lean_object*); +size_t l_UInt32_toUSize(uint32_t); lean_object* l_Lean_Level_getOffsetAux(lean_object*, lean_object*); lean_object* l___private_Init_Lean_Level_5__mkMaxAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Level_3__getMaxArgsAux___main(lean_object*, lean_object*, uint8_t, lean_object*); -lean_object* l_Lean_Level_max___boxed(lean_object*, lean_object*); -lean_object* lean_level_mk_imax(lean_object*, lean_object*); +lean_object* l_Lean_Level_depth(lean_object*); lean_object* l_Lean_Level_LevelToFormat_toResult___main(lean_object*); -lean_object* l_Lean_Level_imax___boxed(lean_object*, lean_object*); +size_t l_Lean_Level_Data_hash(uint64_t); lean_object* l_Lean_Level_mvarId_x21(lean_object*); lean_object* l_Lean_Level_Lean_HasFormat___closed__1; uint8_t l_Lean_Level_occurs___main(lean_object*, lean_object*); lean_object* l___private_Init_Util_1__mkPanicMessage(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Level_3__getMaxArgsAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* lean_level_mk_succ(lean_object*); lean_object* l_Lean_Level_addOffsetAux(lean_object*, lean_object*); lean_object* l_Lean_Level_ofNat___main___boxed(lean_object*); lean_object* l_Lean_Level_LevelToFormat_Result_format___main___boxed(lean_object*, lean_object*); -lean_object* l_Lean_Level_one___closed__1; lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__1; lean_object* l_Lean_Level_Inhabited; -size_t lean_level_hash(lean_object*); +size_t l_Lean_Level_hash(lean_object*); lean_object* l_Lean_Level_dec___boxed(lean_object*); lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__3; -lean_object* lean_level_mk_param(lean_object*); lean_object* l_Lean_Level_updateSucc_x21___closed__1; lean_object* l_Lean_Level_updateSucc_x21___closed__2; lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Level_param___boxed(lean_object*); +uint64_t l_Lean_Level_Data_inhabited; lean_object* l_Lean_Level_isEquiv___boxed(lean_object*, lean_object*); -lean_object* lean_level_mk_succ(lean_object*); +uint8_t lean_level_has_param(lean_object*); extern lean_object* l_System_FilePath_dirName___closed__1; lean_object* l_panic(lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Level_isNeverZero(lean_object*); extern lean_object* l_Lean_HasRepr___closed__1; +uint8_t l_Lean_Level_Data_hasMVar(uint64_t); +uint64_t l_Lean_Level_data(lean_object*); lean_object* l_Lean_Level_updateIMax_x21___closed__1; lean_object* l___private_Init_Lean_Level_3__getMaxArgsAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Name_quickLt(lean_object*, lean_object*); @@ -150,17 +180,20 @@ lean_object* l___private_Init_Lean_Level_2__mkIMaxAux(lean_object*, lean_object* lean_object* lean_level_update_imax(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_fmt___at_Lean_Level_LevelToFormat_toResult___main___spec__1(lean_object*); lean_object* lean_format_group(lean_object*); +lean_object* lean_level_mk_max(lean_object*, lean_object*); uint8_t l_Lean_Level_normLtAux(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Level_getDepth___main(lean_object*); +uint64_t l_Lean_mkLevelZero___closed__1; +size_t lean_usize_mix_hash(size_t, size_t); uint8_t l_Lean_Level_isIMax(lean_object*); +uint8_t l_Lean_Level_Data_hasParam(uint64_t); lean_object* l_Lean_Level_isParam___boxed(lean_object*); lean_object* l_Lean_Level_normLtAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Level_addOffsetAux___main(lean_object*, lean_object*); lean_object* lean_array_get_size(lean_object*); uint8_t l_Lean_Level_normLtAux___main(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Level_hashable___closed__1; -lean_object* l_Lean_Level_hashable; +lean_object* l_Lean_mkLevelOne___closed__1; lean_object* l_Lean_Level_getOffsetAux___main___boxed(lean_object*, lean_object*); +lean_object* l_Lean_mkLevelSucc(lean_object*); lean_object* l_Lean_Level_HasBeq___closed__1; lean_object* l_Array_qsortAux___main___at_Lean_Level_normalize___main___spec__2(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Level_mvarId_x21___boxed(lean_object*); @@ -170,15 +203,17 @@ lean_object* l_Lean_Level_LevelToFormat_Result_format(lean_object*, uint8_t); lean_object* l_Lean_Level_LevelToFormat_parenIfFalse(lean_object*, uint8_t); lean_object* l___private_Init_Lean_Level_6__formatLst___main(lean_object*, lean_object*); lean_object* l_Nat_imax(lean_object*, lean_object*); +lean_object* l_Lean_Level_Data_hasParam___boxed(lean_object*); lean_object* l_Lean_Level_occurs___main___boxed(lean_object*, lean_object*); lean_object* l_Lean_Level_updateMax_x21(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Level_succ___boxed(lean_object*); +lean_object* l_Lean_Level_data___boxed(lean_object*); uint8_t l_Lean_Level_isExplicit(lean_object*); uint8_t lean_nat_dec_le(lean_object*, lean_object*); uint8_t l___private_Init_Lean_Level_1__isAlreadyNormalizedCheap___main(lean_object*); lean_object* l_Lean_Level_LevelToFormat_parenIfFalse___boxed(lean_object*, lean_object*); lean_object* l_Lean_Level_getOffsetAux___boxed(lean_object*, lean_object*); lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_Level_normalize___main___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +uint32_t l_USize_toUInt32(size_t); uint8_t lean_level_eq(lean_object*, lean_object*); lean_object* l_Lean_Level_getLevelOffset___main(lean_object*); lean_object* l_Lean_Level_updateMax_x21___closed__2; @@ -187,19 +222,29 @@ lean_object* lean_nat_div(lean_object*, lean_object*); lean_object* l_Lean_Level_HasBeq; lean_object* l_Lean_Level_isZero___boxed(lean_object*); uint8_t l_Lean_Level_isMVar(lean_object*); +lean_object* lean_uint32_to_nat(uint32_t); +lean_object* l_Lean_mkLevelIMax(lean_object*, lean_object*); +lean_object* l_Lean_Level_Data_depth___boxed(lean_object*); lean_object* lean_level_update_max(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_mkLevelMVar(lean_object*); lean_object* l_Lean_Level_LevelToFormat_Result_format___main(lean_object*, uint8_t); lean_object* l_unreachable_x21___rarg(lean_object*); lean_object* l_Lean_Level_updateMax___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Level_hashEx___boxed(lean_object*); lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_Level_normalize___main___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +uint32_t l_Lean_Level_Data_depth(uint64_t); lean_object* l_Nat_max(lean_object*, lean_object*); lean_object* l___private_Init_Lean_Level_5__mkMaxAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Level_isZero(lean_object*); +size_t lean_level_hash(lean_object*); +lean_object* l_Lean_Level_depth___boxed(lean_object*); lean_object* l_Lean_Level_isExplicit___boxed(lean_object*); +uint64_t l_UInt64_land(uint64_t, uint64_t); lean_object* l_Lean_Level_hash___boxed(lean_object*); +lean_object* l_Lean_Level_Data_hasMVar___boxed(lean_object*); +lean_object* l_Lean_Level_Hashable; uint8_t l_Lean_Level_isNeverZero___main(lean_object*); lean_object* l_Lean_Level_LevelToFormat_Result_succ(lean_object*); -lean_object* lean_level_mk_max(lean_object*, lean_object*); lean_object* l_Lean_Level_isExplicit___main___boxed(lean_object*); uint8_t l_Lean_Level_occurs(lean_object*, lean_object*); lean_object* l_Lean_Level_normalize___boxed(lean_object*); @@ -236,51 +281,836 @@ lean_dec(x_1); return x_3; } } -lean_object* l_Lean_Level_succ___boxed(lean_object* x_1) { +uint64_t _init_l_Lean_Level_Data_inhabited() { _start: { -lean_object* x_2; -x_2 = lean_level_mk_succ(x_1); -return x_2; +uint64_t x_1; +x_1 = l_UInt64_Inhabited; +return x_1; } } -lean_object* l_Lean_Level_max___boxed(lean_object* x_1, lean_object* x_2) { +size_t l_Lean_Level_Data_hash(uint64_t x_1) { _start: { -lean_object* x_3; -x_3 = lean_level_mk_max(x_1, x_2); +uint32_t x_2; size_t x_3; +x_2 = ((uint32_t)x_1); +x_3 = x_2; return x_3; } } -lean_object* l_Lean_Level_imax___boxed(lean_object* x_1, lean_object* x_2) { +lean_object* l_Lean_Level_Data_hash___boxed(lean_object* x_1) { _start: { -lean_object* x_3; -x_3 = lean_level_mk_imax(x_1, x_2); +uint64_t x_2; size_t x_3; lean_object* x_4; +x_2 = lean_unbox_uint64(x_1); +lean_dec(x_1); +x_3 = l_Lean_Level_Data_hash(x_2); +x_4 = lean_box_usize(x_3); +return x_4; +} +} +uint8_t l_Lean_Level_Data_hasBeq(uint64_t x_1, uint64_t x_2) { +_start: +{ +uint8_t x_3; +x_3 = x_1 == x_2; return x_3; } } -lean_object* l_Lean_Level_param___boxed(lean_object* x_1) { +lean_object* l_Lean_Level_Data_hasBeq___boxed(lean_object* x_1, lean_object* x_2) { _start: { -lean_object* x_2; -x_2 = lean_level_mk_param(x_1); +uint64_t x_3; uint64_t x_4; uint8_t x_5; lean_object* x_6; +x_3 = lean_unbox_uint64(x_1); +lean_dec(x_1); +x_4 = lean_unbox_uint64(x_2); +lean_dec(x_2); +x_5 = l_Lean_Level_Data_hasBeq(x_3, x_4); +x_6 = lean_box(x_5); +return x_6; +} +} +uint32_t l_Lean_Level_Data_depth(uint64_t x_1) { +_start: +{ +uint64_t x_2; uint64_t x_3; uint32_t x_4; +x_2 = 40; +x_3 = x_1 >> x_2; +x_4 = ((uint32_t)x_3); +return x_4; +} +} +lean_object* l_Lean_Level_Data_depth___boxed(lean_object* x_1) { +_start: +{ +uint64_t x_2; uint32_t x_3; lean_object* x_4; +x_2 = lean_unbox_uint64(x_1); +lean_dec(x_1); +x_3 = l_Lean_Level_Data_depth(x_2); +x_4 = lean_box_uint32(x_3); +return x_4; +} +} +uint8_t l_Lean_Level_Data_hasMVar(uint64_t x_1) { +_start: +{ +uint64_t x_2; uint64_t x_3; uint64_t x_4; uint64_t x_5; uint8_t x_6; +x_2 = 1; +x_3 = 32; +x_4 = x_1 >> x_3; +x_5 = x_4 & x_2; +x_6 = x_5 == x_2; +return x_6; +} +} +lean_object* l_Lean_Level_Data_hasMVar___boxed(lean_object* x_1) { +_start: +{ +uint64_t x_2; uint8_t x_3; lean_object* x_4; +x_2 = lean_unbox_uint64(x_1); +lean_dec(x_1); +x_3 = l_Lean_Level_Data_hasMVar(x_2); +x_4 = lean_box(x_3); +return x_4; +} +} +uint8_t l_Lean_Level_Data_hasParam(uint64_t x_1) { +_start: +{ +uint64_t x_2; uint64_t x_3; uint64_t x_4; uint64_t x_5; uint8_t x_6; +x_2 = 1; +x_3 = 33; +x_4 = x_1 >> x_3; +x_5 = x_4 & x_2; +x_6 = x_5 == x_2; +return x_6; +} +} +lean_object* l_Lean_Level_Data_hasParam___boxed(lean_object* x_1) { +_start: +{ +uint64_t x_2; uint8_t x_3; lean_object* x_4; +x_2 = lean_unbox_uint64(x_1); +lean_dec(x_1); +x_3 = l_Lean_Level_Data_hasParam(x_2); +x_4 = lean_box(x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Level_mkData___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_Lean_Level_mkData___closed__2() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("Init.Lean.Level"); +return x_1; +} +} +lean_object* _init_l_Lean_Level_mkData___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("universe level depth is too big"); +return x_1; +} +} +lean_object* _init_l_Lean_Level_mkData___closed__4() { +_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_Level_mkData___closed__2; +x_2 = lean_unsigned_to_nat(45u); +x_3 = lean_unsigned_to_nat(33u); +x_4 = l_Lean_Level_mkData___closed__3; +x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4); +return x_5; +} +} +lean_object* _init_l_Lean_Level_mkData___boxed__const__1() { +_start: +{ +uint64_t x_1; lean_object* x_2; +x_1 = l_Lean_Level_Data_inhabited; +x_2 = lean_box_uint64(x_1); return x_2; } } -lean_object* l_Lean_Level_mvar___boxed(lean_object* x_1) { +uint64_t l_Lean_Level_mkData(size_t x_1, lean_object* x_2, uint8_t x_3, uint8_t x_4) { +_start: +{ +lean_object* x_5; uint8_t x_6; +x_5 = l_Lean_Level_mkData___closed__1; +x_6 = lean_nat_dec_lt(x_5, x_2); +if (x_6 == 0) +{ +uint32_t x_7; uint64_t x_8; uint64_t x_9; uint64_t x_10; uint64_t x_11; uint64_t x_12; uint64_t x_13; uint64_t x_14; uint64_t x_15; uint64_t x_16; uint64_t x_17; uint64_t x_18; uint64_t x_19; uint64_t x_20; +x_7 = (uint32_t)x_1; +x_8 = ((uint64_t)x_7); +x_9 = (uint64_t)x_3; +x_10 = 32; +x_11 = x_9 << x_10; +x_12 = x_8 + x_11; +x_13 = (uint64_t)x_4; +x_14 = 33; +x_15 = x_13 << x_14; +x_16 = x_12 + x_15; +x_17 = lean_uint64_of_nat(x_2); +x_18 = 40; +x_19 = x_17 << x_18; +x_20 = x_16 + x_19; +return x_20; +} +else +{ +lean_object* x_21; lean_object* x_22; lean_object* x_23; uint64_t x_24; +x_21 = l_Lean_Level_mkData___closed__4; +x_22 = l_Lean_Level_mkData___boxed__const__1; +x_23 = lean_panic_fn(x_21); +x_24 = lean_unbox_uint64(x_23); +lean_dec(x_23); +return x_24; +} +} +} +lean_object* l_Lean_Level_mkData___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +size_t x_5; uint8_t x_6; uint8_t x_7; uint64_t x_8; lean_object* x_9; +x_5 = lean_unbox_usize(x_1); +lean_dec(x_1); +x_6 = lean_unbox(x_3); +lean_dec(x_3); +x_7 = lean_unbox(x_4); +lean_dec(x_4); +x_8 = l_Lean_Level_mkData(x_5, x_2, x_6, x_7); +lean_dec(x_2); +x_9 = lean_box_uint64(x_8); +return x_9; +} +} +uint64_t l_Lean_Level_data(lean_object* x_1) { +_start: +{ +switch (lean_obj_tag(x_1)) { +case 0: +{ +uint64_t x_2; +x_2 = lean_ctor_get_uint64(x_1, 0); +return x_2; +} +case 2: +{ +uint64_t x_3; +x_3 = lean_ctor_get_uint64(x_1, sizeof(void*)*2); +return x_3; +} +case 3: +{ +uint64_t x_4; +x_4 = lean_ctor_get_uint64(x_1, sizeof(void*)*2); +return x_4; +} +default: +{ +uint64_t x_5; +x_5 = lean_ctor_get_uint64(x_1, sizeof(void*)*1); +return x_5; +} +} +} +} +lean_object* l_Lean_Level_data___boxed(lean_object* x_1) { +_start: +{ +uint64_t x_2; lean_object* x_3; +x_2 = l_Lean_Level_data(x_1); +lean_dec(x_1); +x_3 = lean_box_uint64(x_2); +return x_3; +} +} +size_t l_Lean_Level_hash(lean_object* x_1) { +_start: +{ +switch (lean_obj_tag(x_1)) { +case 0: +{ +uint64_t x_2; size_t x_3; +x_2 = lean_ctor_get_uint64(x_1, 0); +x_3 = l_Lean_Level_Data_hash(x_2); +return x_3; +} +case 2: +{ +uint64_t x_4; size_t x_5; +x_4 = lean_ctor_get_uint64(x_1, sizeof(void*)*2); +x_5 = l_Lean_Level_Data_hash(x_4); +return x_5; +} +case 3: +{ +uint64_t x_6; size_t x_7; +x_6 = lean_ctor_get_uint64(x_1, sizeof(void*)*2); +x_7 = l_Lean_Level_Data_hash(x_6); +return x_7; +} +default: +{ +uint64_t x_8; size_t x_9; +x_8 = lean_ctor_get_uint64(x_1, sizeof(void*)*1); +x_9 = l_Lean_Level_Data_hash(x_8); +return x_9; +} +} +} +} +lean_object* l_Lean_Level_hash___boxed(lean_object* x_1) { +_start: +{ +size_t x_2; lean_object* x_3; +x_2 = l_Lean_Level_hash(x_1); +lean_dec(x_1); +x_3 = lean_box_usize(x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Level_Hashable___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Level_hash___boxed), 1, 0); +return x_1; +} +} +lean_object* _init_l_Lean_Level_Hashable() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Level_Hashable___closed__1; +return x_1; +} +} +lean_object* l_Lean_Level_depth(lean_object* x_1) { +_start: +{ +switch (lean_obj_tag(x_1)) { +case 0: +{ +uint64_t x_2; uint32_t x_3; lean_object* x_4; +x_2 = lean_ctor_get_uint64(x_1, 0); +x_3 = l_Lean_Level_Data_depth(x_2); +x_4 = lean_uint32_to_nat(x_3); +return x_4; +} +case 2: +{ +uint64_t x_5; uint32_t x_6; lean_object* x_7; +x_5 = lean_ctor_get_uint64(x_1, sizeof(void*)*2); +x_6 = l_Lean_Level_Data_depth(x_5); +x_7 = lean_uint32_to_nat(x_6); +return x_7; +} +case 3: +{ +uint64_t x_8; uint32_t x_9; lean_object* x_10; +x_8 = lean_ctor_get_uint64(x_1, sizeof(void*)*2); +x_9 = l_Lean_Level_Data_depth(x_8); +x_10 = lean_uint32_to_nat(x_9); +return x_10; +} +default: +{ +uint64_t x_11; uint32_t x_12; lean_object* x_13; +x_11 = lean_ctor_get_uint64(x_1, sizeof(void*)*1); +x_12 = l_Lean_Level_Data_depth(x_11); +x_13 = lean_uint32_to_nat(x_12); +return x_13; +} +} +} +} +lean_object* l_Lean_Level_depth___boxed(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_level_mk_mvar(x_1); +x_2 = l_Lean_Level_depth(x_1); +lean_dec(x_1); return x_2; } } +uint8_t l_Lean_Level_hasMVar(lean_object* x_1) { +_start: +{ +switch (lean_obj_tag(x_1)) { +case 0: +{ +uint64_t x_2; uint8_t x_3; +x_2 = lean_ctor_get_uint64(x_1, 0); +x_3 = l_Lean_Level_Data_hasMVar(x_2); +return x_3; +} +case 2: +{ +uint64_t x_4; uint8_t x_5; +x_4 = lean_ctor_get_uint64(x_1, sizeof(void*)*2); +x_5 = l_Lean_Level_Data_hasMVar(x_4); +return x_5; +} +case 3: +{ +uint64_t x_6; uint8_t x_7; +x_6 = lean_ctor_get_uint64(x_1, sizeof(void*)*2); +x_7 = l_Lean_Level_Data_hasMVar(x_6); +return x_7; +} +default: +{ +uint64_t x_8; uint8_t x_9; +x_8 = lean_ctor_get_uint64(x_1, sizeof(void*)*1); +x_9 = l_Lean_Level_Data_hasMVar(x_8); +return x_9; +} +} +} +} +lean_object* l_Lean_Level_hasMVar___boxed(lean_object* x_1) { +_start: +{ +uint8_t x_2; lean_object* x_3; +x_2 = l_Lean_Level_hasMVar(x_1); +lean_dec(x_1); +x_3 = lean_box(x_2); +return x_3; +} +} +uint8_t l_Lean_Level_hasParam(lean_object* x_1) { +_start: +{ +switch (lean_obj_tag(x_1)) { +case 0: +{ +uint64_t x_2; uint8_t x_3; +x_2 = lean_ctor_get_uint64(x_1, 0); +x_3 = l_Lean_Level_Data_hasParam(x_2); +return x_3; +} +case 2: +{ +uint64_t x_4; uint8_t x_5; +x_4 = lean_ctor_get_uint64(x_1, sizeof(void*)*2); +x_5 = l_Lean_Level_Data_hasParam(x_4); +return x_5; +} +case 3: +{ +uint64_t x_6; uint8_t x_7; +x_6 = lean_ctor_get_uint64(x_1, sizeof(void*)*2); +x_7 = l_Lean_Level_Data_hasParam(x_6); +return x_7; +} +default: +{ +uint64_t x_8; uint8_t x_9; +x_8 = lean_ctor_get_uint64(x_1, sizeof(void*)*1); +x_9 = l_Lean_Level_Data_hasParam(x_8); +return x_9; +} +} +} +} +lean_object* l_Lean_Level_hasParam___boxed(lean_object* x_1) { +_start: +{ +uint8_t x_2; lean_object* x_3; +x_2 = l_Lean_Level_hasParam(x_1); +lean_dec(x_1); +x_3 = lean_box(x_2); +return x_3; +} +} +size_t lean_level_hash(lean_object* x_1) { +_start: +{ +size_t x_2; +x_2 = l_Lean_Level_hash(x_1); +lean_dec(x_1); +return x_2; +} +} +lean_object* l_Lean_Level_hashEx___boxed(lean_object* x_1) { +_start: +{ +size_t x_2; lean_object* x_3; +x_2 = lean_level_hash(x_1); +x_3 = lean_box_usize(x_2); +return x_3; +} +} +uint8_t lean_level_has_mvar(lean_object* x_1) { +_start: +{ +uint8_t x_2; +x_2 = l_Lean_Level_hasMVar(x_1); +lean_dec(x_1); +return x_2; +} +} +lean_object* l_Lean_Level_hasMVarEx___boxed(lean_object* x_1) { +_start: +{ +uint8_t x_2; lean_object* x_3; +x_2 = lean_level_has_mvar(x_1); +x_3 = lean_box(x_2); +return x_3; +} +} +uint8_t lean_level_has_param(lean_object* x_1) { +_start: +{ +uint8_t x_2; +x_2 = l_Lean_Level_hasParam(x_1); +lean_dec(x_1); +return x_2; +} +} +lean_object* l_Lean_Level_hasParamEx___boxed(lean_object* x_1) { +_start: +{ +uint8_t x_2; lean_object* x_3; +x_2 = lean_level_has_param(x_1); +x_3 = lean_box(x_2); +return x_3; +} +} +lean_object* lean_level_depth(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = l_Lean_Level_depth(x_1); +lean_dec(x_1); +return x_2; +} +} +uint64_t _init_l_Lean_mkLevelZero___closed__1() { +_start: +{ +size_t x_1; lean_object* x_2; uint8_t x_3; uint64_t x_4; +x_1 = 2221; +x_2 = lean_unsigned_to_nat(0u); +x_3 = 0; +x_4 = l_Lean_Level_mkData(x_1, x_2, x_3, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_mkLevelZero___closed__2() { +_start: +{ +uint64_t x_1; lean_object* x_2; +x_1 = l_Lean_mkLevelZero___closed__1; +x_2 = lean_alloc_ctor(0, 0, 8); +lean_ctor_set_uint64(x_2, 0, x_1); +return x_2; +} +} +lean_object* _init_l_Lean_mkLevelZero() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_mkLevelZero___closed__2; +return x_1; +} +} +lean_object* l_Lean_mkLevelMVar(lean_object* x_1) { +_start: +{ +size_t x_2; size_t x_3; size_t x_4; lean_object* x_5; uint8_t x_6; uint8_t x_7; uint64_t x_8; lean_object* x_9; +x_2 = 2237; +x_3 = lean_name_hash_usize(x_1); +x_4 = lean_usize_mix_hash(x_2, x_3); +x_5 = lean_unsigned_to_nat(0u); +x_6 = 1; +x_7 = 0; +x_8 = l_Lean_Level_mkData(x_4, x_5, x_6, x_7); +x_9 = lean_alloc_ctor(5, 1, 8); +lean_ctor_set(x_9, 0, x_1); +lean_ctor_set_uint64(x_9, sizeof(void*)*1, x_8); +return x_9; +} +} +lean_object* l_Lean_mkLevelParam(lean_object* x_1) { +_start: +{ +size_t x_2; size_t x_3; size_t x_4; lean_object* x_5; uint8_t x_6; uint8_t x_7; uint64_t x_8; lean_object* x_9; +x_2 = 2239; +x_3 = lean_name_hash_usize(x_1); +x_4 = lean_usize_mix_hash(x_2, x_3); +x_5 = lean_unsigned_to_nat(0u); +x_6 = 0; +x_7 = 1; +x_8 = l_Lean_Level_mkData(x_4, x_5, x_6, x_7); +x_9 = lean_alloc_ctor(4, 1, 8); +lean_ctor_set(x_9, 0, x_1); +lean_ctor_set_uint64(x_9, sizeof(void*)*1, x_8); +return x_9; +} +} +lean_object* l_Lean_mkLevelSucc(lean_object* x_1) { +_start: +{ +size_t x_2; size_t x_3; size_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; uint8_t x_9; uint64_t x_10; lean_object* x_11; +x_2 = 2243; +x_3 = l_Lean_Level_hash(x_1); +x_4 = lean_usize_mix_hash(x_2, x_3); +x_5 = l_Lean_Level_depth(x_1); +x_6 = lean_unsigned_to_nat(1u); +x_7 = lean_nat_add(x_5, x_6); +lean_dec(x_5); +x_8 = l_Lean_Level_hasMVar(x_1); +x_9 = l_Lean_Level_hasParam(x_1); +x_10 = l_Lean_Level_mkData(x_4, x_7, x_8, x_9); +lean_dec(x_7); +x_11 = lean_alloc_ctor(1, 1, 8); +lean_ctor_set(x_11, 0, x_1); +lean_ctor_set_uint64(x_11, sizeof(void*)*1, x_10); +return x_11; +} +} +lean_object* l_Lean_mkLevelMax(lean_object* x_1, lean_object* x_2) { +_start: +{ +size_t x_3; size_t x_4; size_t x_5; size_t x_6; size_t x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; uint8_t x_14; +x_3 = 2251; +x_4 = l_Lean_Level_hash(x_1); +x_5 = l_Lean_Level_hash(x_2); +x_6 = lean_usize_mix_hash(x_4, x_5); +x_7 = lean_usize_mix_hash(x_3, x_6); +x_8 = l_Lean_Level_depth(x_1); +x_9 = l_Lean_Level_depth(x_2); +x_10 = l_Nat_max(x_8, x_9); +lean_dec(x_9); +lean_dec(x_8); +x_11 = lean_unsigned_to_nat(1u); +x_12 = lean_nat_add(x_10, x_11); +lean_dec(x_10); +x_13 = l_Lean_Level_hasMVar(x_1); +x_14 = l_Lean_Level_hasParam(x_1); +if (x_13 == 0) +{ +uint8_t x_15; +x_15 = l_Lean_Level_hasMVar(x_2); +if (x_14 == 0) +{ +uint8_t x_16; uint64_t x_17; lean_object* x_18; +x_16 = l_Lean_Level_hasParam(x_2); +x_17 = l_Lean_Level_mkData(x_7, x_12, x_15, x_16); +lean_dec(x_12); +x_18 = lean_alloc_ctor(2, 2, 8); +lean_ctor_set(x_18, 0, x_1); +lean_ctor_set(x_18, 1, x_2); +lean_ctor_set_uint64(x_18, sizeof(void*)*2, x_17); +return x_18; +} +else +{ +uint8_t x_19; uint64_t x_20; lean_object* x_21; +x_19 = 1; +x_20 = l_Lean_Level_mkData(x_7, x_12, x_15, x_19); +lean_dec(x_12); +x_21 = lean_alloc_ctor(2, 2, 8); +lean_ctor_set(x_21, 0, x_1); +lean_ctor_set(x_21, 1, x_2); +lean_ctor_set_uint64(x_21, sizeof(void*)*2, x_20); +return x_21; +} +} +else +{ +if (x_14 == 0) +{ +uint8_t x_22; uint8_t x_23; uint64_t x_24; lean_object* x_25; +x_22 = l_Lean_Level_hasParam(x_2); +x_23 = 1; +x_24 = l_Lean_Level_mkData(x_7, x_12, x_23, x_22); +lean_dec(x_12); +x_25 = lean_alloc_ctor(2, 2, 8); +lean_ctor_set(x_25, 0, x_1); +lean_ctor_set(x_25, 1, x_2); +lean_ctor_set_uint64(x_25, sizeof(void*)*2, x_24); +return x_25; +} +else +{ +uint8_t x_26; uint64_t x_27; lean_object* x_28; +x_26 = 1; +x_27 = l_Lean_Level_mkData(x_7, x_12, x_26, x_26); +lean_dec(x_12); +x_28 = lean_alloc_ctor(2, 2, 8); +lean_ctor_set(x_28, 0, x_1); +lean_ctor_set(x_28, 1, x_2); +lean_ctor_set_uint64(x_28, sizeof(void*)*2, x_27); +return x_28; +} +} +} +} +lean_object* l_Lean_mkLevelIMax(lean_object* x_1, lean_object* x_2) { +_start: +{ +size_t x_3; size_t x_4; size_t x_5; size_t x_6; size_t x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; uint8_t x_14; +x_3 = 2267; +x_4 = l_Lean_Level_hash(x_1); +x_5 = l_Lean_Level_hash(x_2); +x_6 = lean_usize_mix_hash(x_4, x_5); +x_7 = lean_usize_mix_hash(x_3, x_6); +x_8 = l_Lean_Level_depth(x_1); +x_9 = l_Lean_Level_depth(x_2); +x_10 = l_Nat_max(x_8, x_9); +lean_dec(x_9); +lean_dec(x_8); +x_11 = lean_unsigned_to_nat(1u); +x_12 = lean_nat_add(x_10, x_11); +lean_dec(x_10); +x_13 = l_Lean_Level_hasMVar(x_1); +x_14 = l_Lean_Level_hasParam(x_1); +if (x_13 == 0) +{ +uint8_t x_15; +x_15 = l_Lean_Level_hasMVar(x_2); +if (x_14 == 0) +{ +uint8_t x_16; uint64_t x_17; lean_object* x_18; +x_16 = l_Lean_Level_hasParam(x_2); +x_17 = l_Lean_Level_mkData(x_7, x_12, x_15, x_16); +lean_dec(x_12); +x_18 = lean_alloc_ctor(3, 2, 8); +lean_ctor_set(x_18, 0, x_1); +lean_ctor_set(x_18, 1, x_2); +lean_ctor_set_uint64(x_18, sizeof(void*)*2, x_17); +return x_18; +} +else +{ +uint8_t x_19; uint64_t x_20; lean_object* x_21; +x_19 = 1; +x_20 = l_Lean_Level_mkData(x_7, x_12, x_15, x_19); +lean_dec(x_12); +x_21 = lean_alloc_ctor(3, 2, 8); +lean_ctor_set(x_21, 0, x_1); +lean_ctor_set(x_21, 1, x_2); +lean_ctor_set_uint64(x_21, sizeof(void*)*2, x_20); +return x_21; +} +} +else +{ +if (x_14 == 0) +{ +uint8_t x_22; uint8_t x_23; uint64_t x_24; lean_object* x_25; +x_22 = l_Lean_Level_hasParam(x_2); +x_23 = 1; +x_24 = l_Lean_Level_mkData(x_7, x_12, x_23, x_22); +lean_dec(x_12); +x_25 = lean_alloc_ctor(3, 2, 8); +lean_ctor_set(x_25, 0, x_1); +lean_ctor_set(x_25, 1, x_2); +lean_ctor_set_uint64(x_25, sizeof(void*)*2, x_24); +return x_25; +} +else +{ +uint8_t x_26; uint64_t x_27; lean_object* x_28; +x_26 = 1; +x_27 = l_Lean_Level_mkData(x_7, x_12, x_26, x_26); +lean_dec(x_12); +x_28 = lean_alloc_ctor(3, 2, 8); +lean_ctor_set(x_28, 0, x_1); +lean_ctor_set(x_28, 1, x_2); +lean_ctor_set_uint64(x_28, sizeof(void*)*2, x_27); +return x_28; +} +} +} +} +lean_object* _init_l_Lean_mkLevelOne___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_mkLevelZero; +x_2 = l_Lean_mkLevelSucc(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_mkLevelOne() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_mkLevelOne___closed__1; +return x_1; +} +} +lean_object* lean_level_mk_zero(lean_object* x_1) { +_start: +{ +lean_object* x_2; +lean_dec(x_1); +x_2 = l_Lean_mkLevelZero; +return x_2; +} +} +lean_object* lean_level_mk_succ(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = l_Lean_mkLevelSucc(x_1); +return x_2; +} +} +lean_object* lean_level_mk_mvar(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = l_Lean_mkLevelMVar(x_1); +return x_2; +} +} +lean_object* lean_level_mk_param(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = l_Lean_mkLevelParam(x_1); +return x_2; +} +} +lean_object* lean_level_mk_max(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l_Lean_mkLevelMax(x_1, x_2); +return x_3; +} +} +lean_object* lean_level_mk_imax(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l_Lean_mkLevelIMax(x_1, x_2); +return x_3; +} +} lean_object* _init_l_Lean_Level_Inhabited() { _start: { lean_object* x_1; -x_1 = lean_box(0); +x_1 = l_Lean_mkLevelZero; return x_1; } } @@ -485,26 +1315,18 @@ lean_object* _init_l_Lean_Level_mvarId_x21___closed__1() { _start: { lean_object* x_1; -x_1 = lean_mk_string("Init.Lean.Level"); +x_1 = lean_mk_string("metavariable expected"); return x_1; } } lean_object* _init_l_Lean_Level_mvarId_x21___closed__2() { _start: { -lean_object* x_1; -x_1 = lean_mk_string("metavariable expected"); -return x_1; -} -} -lean_object* _init_l_Lean_Level_mvarId_x21___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_Lean_Level_mvarId_x21___closed__1; -x_2 = lean_unsigned_to_nat(67u); -x_3 = lean_unsigned_to_nat(17u); -x_4 = l_Lean_Level_mvarId_x21___closed__2; +x_1 = l_Lean_Level_mkData___closed__2; +x_2 = lean_unsigned_to_nat(157u); +x_3 = lean_unsigned_to_nat(19u); +x_4 = l_Lean_Level_mvarId_x21___closed__1; x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4); return x_5; } @@ -523,7 +1345,7 @@ else { lean_object* x_3; lean_object* x_4; lean_object* x_5; x_3 = l_Lean_Inhabited; -x_4 = l_Lean_Level_mvarId_x21___closed__3; +x_4 = l_Lean_Level_mvarId_x21___closed__2; x_5 = lean_panic_fn(x_4); return x_5; } @@ -610,41 +1432,6 @@ x_3 = lean_box(x_2); return x_3; } } -lean_object* _init_l_Lean_Level_one___closed__1() { -_start: -{ -lean_object* x_1; lean_object* x_2; -x_1 = lean_box(0); -x_2 = lean_level_mk_succ(x_1); -return x_2; -} -} -lean_object* _init_l_Lean_Level_one() { -_start: -{ -lean_object* x_1; -x_1 = l_Lean_Level_one___closed__1; -return x_1; -} -} -lean_object* l_Lean_Level_hasParam___boxed(lean_object* x_1) { -_start: -{ -uint8_t x_2; lean_object* x_3; -x_2 = lean_level_has_param(x_1); -x_3 = lean_box(x_2); -return x_3; -} -} -lean_object* l_Lean_Level_hasMVar___boxed(lean_object* x_1) { -_start: -{ -uint8_t x_2; lean_object* x_3; -x_2 = lean_level_has_mvar(x_1); -x_3 = lean_box(x_2); -return x_3; -} -} lean_object* l_Lean_Level_ofNat___main(lean_object* x_1) { _start: { @@ -658,13 +1445,13 @@ x_4 = lean_unsigned_to_nat(1u); x_5 = lean_nat_sub(x_1, x_4); x_6 = l_Lean_Level_ofNat___main(x_5); lean_dec(x_5); -x_7 = lean_level_mk_succ(x_6); +x_7 = l_Lean_mkLevelSucc(x_6); return x_7; } else { lean_object* x_8; -x_8 = lean_box(0); +x_8 = l_Lean_mkLevelZero; return x_8; } } @@ -707,7 +1494,7 @@ lean_object* x_5; lean_object* x_6; lean_object* x_7; x_5 = lean_unsigned_to_nat(1u); x_6 = lean_nat_sub(x_1, x_5); lean_dec(x_1); -x_7 = lean_level_mk_succ(x_2); +x_7 = l_Lean_mkLevelSucc(x_2); x_1 = x_6; x_2 = x_7; goto _start; @@ -747,16 +1534,37 @@ return x_2; } case 1: { -lean_object* x_3; +lean_object* x_3; uint8_t x_4; x_3 = lean_ctor_get(x_1, 0); +x_4 = l_Lean_Level_hasMVar(x_3); +if (x_4 == 0) +{ +uint8_t x_5; +x_5 = l_Lean_Level_hasParam(x_3); +if (x_5 == 0) +{ x_1 = x_3; goto _start; } +else +{ +uint8_t x_7; +x_7 = 0; +return x_7; +} +} +else +{ +uint8_t x_8; +x_8 = 0; +return x_8; +} +} default: { -uint8_t x_5; -x_5 = 0; -return x_5; +uint8_t x_9; +x_9 = 0; +return x_9; } } } @@ -904,6 +1712,7 @@ x_2 = l_Lean_Level_getLevelOffset___main(x_1); if (lean_obj_tag(x_2) == 0) { lean_object* x_3; lean_object* x_4; lean_object* x_5; +lean_dec(x_2); x_3 = lean_unsigned_to_nat(0u); x_4 = l_Lean_Level_getOffsetAux___main(x_1, x_3); x_5 = lean_alloc_ctor(1, 1, 0); @@ -928,85 +1737,6 @@ lean_dec(x_1); return x_2; } } -lean_object* l_Lean_Level_getDepth___main(lean_object* x_1) { -_start: -{ -switch (lean_obj_tag(x_1)) { -case 1: -{ -lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_2 = lean_ctor_get(x_1, 0); -x_3 = l_Lean_Level_getDepth___main(x_2); -x_4 = lean_unsigned_to_nat(1u); -x_5 = lean_nat_add(x_3, x_4); -lean_dec(x_3); -return x_5; -} -case 2: -{ -lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; -x_6 = lean_ctor_get(x_1, 0); -x_7 = lean_ctor_get(x_1, 1); -x_8 = l_Lean_Level_getDepth___main(x_6); -x_9 = l_Lean_Level_getDepth___main(x_7); -x_10 = l_Nat_max(x_8, x_9); -lean_dec(x_9); -lean_dec(x_8); -x_11 = lean_unsigned_to_nat(1u); -x_12 = lean_nat_add(x_10, x_11); -lean_dec(x_10); -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; lean_object* x_18; lean_object* x_19; -x_13 = lean_ctor_get(x_1, 0); -x_14 = lean_ctor_get(x_1, 1); -x_15 = l_Lean_Level_getDepth___main(x_13); -x_16 = l_Lean_Level_getDepth___main(x_14); -x_17 = l_Nat_max(x_15, x_16); -lean_dec(x_16); -lean_dec(x_15); -x_18 = lean_unsigned_to_nat(1u); -x_19 = lean_nat_add(x_17, x_18); -lean_dec(x_17); -return x_19; -} -default: -{ -lean_object* x_20; -x_20 = lean_unsigned_to_nat(0u); -return x_20; -} -} -} -} -lean_object* l_Lean_Level_getDepth___main___boxed(lean_object* x_1) { -_start: -{ -lean_object* x_2; -x_2 = l_Lean_Level_getDepth___main(x_1); -lean_dec(x_1); -return x_2; -} -} -lean_object* l_Lean_Level_getDepth(lean_object* x_1) { -_start: -{ -lean_object* x_2; -x_2 = l_Lean_Level_getDepth___main(x_1); -return x_2; -} -} -lean_object* l_Lean_Level_getDepth___boxed(lean_object* x_1) { -_start: -{ -lean_object* x_2; -x_2 = l_Lean_Level_getDepth(x_1); -lean_dec(x_1); -return x_2; -} -} lean_object* l_Lean_Level_instantiate___main(lean_object* x_1, lean_object* x_2) { _start: { @@ -1018,7 +1748,7 @@ x_3 = lean_ctor_get(x_2, 0); lean_inc(x_3); lean_dec(x_2); x_4 = l_Lean_Level_instantiate___main(x_1, x_3); -x_5 = lean_level_mk_succ(x_4); +x_5 = l_Lean_mkLevelSucc(x_4); return x_5; } case 2: @@ -1032,7 +1762,7 @@ lean_dec(x_2); lean_inc(x_1); x_8 = l_Lean_Level_instantiate___main(x_1, x_6); x_9 = l_Lean_Level_instantiate___main(x_1, x_7); -x_10 = lean_level_mk_max(x_8, x_9); +x_10 = l_Lean_mkLevelMax(x_8, x_9); return x_10; } case 3: @@ -1046,7 +1776,7 @@ lean_dec(x_2); lean_inc(x_1); x_13 = l_Lean_Level_instantiate___main(x_1, x_11); x_14 = l_Lean_Level_instantiate___main(x_1, x_12); -x_15 = lean_level_mk_imax(x_13, x_14); +x_15 = l_Lean_mkLevelIMax(x_13, x_14); return x_15; } case 4: @@ -1085,32 +1815,6 @@ x_3 = l_Lean_Level_instantiate___main(x_1, x_2); return x_3; } } -lean_object* l_Lean_Level_hash___boxed(lean_object* x_1) { -_start: -{ -size_t x_2; lean_object* x_3; -x_2 = lean_level_hash(x_1); -lean_dec(x_1); -x_3 = lean_box_usize(x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Level_hashable___closed__1() { -_start: -{ -lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Level_hash___boxed), 1, 0); -return x_1; -} -} -lean_object* _init_l_Lean_Level_hashable() { -_start: -{ -lean_object* x_1; -x_1 = l_Lean_Level_hashable___closed__1; -return x_1; -} -} lean_object* l_Lean_Level_beq___boxed(lean_object* x_1, lean_object* x_2) { _start: { @@ -1315,124 +2019,99 @@ lean_object* x_5; switch (lean_obj_tag(x_1)) { case 0: { -switch (lean_obj_tag(x_3)) { -case 0: +if (lean_obj_tag(x_3) == 1) { -uint8_t x_12; -x_12 = lean_level_eq(x_3, x_3); -if (x_12 == 0) -{ -lean_object* x_13; uint8_t x_14; +lean_object* x_12; lean_object* x_13; lean_object* x_14; +x_12 = lean_ctor_get(x_3, 0); +x_13 = lean_unsigned_to_nat(1u); +x_14 = lean_nat_add(x_4, x_13); lean_dec(x_4); -lean_dec(x_2); -x_13 = l_Lean_Level_ctorToNat(x_3); -x_14 = lean_nat_dec_lt(x_13, x_13); -lean_dec(x_13); -return x_14; +x_3 = x_12; +x_4 = x_14; +goto _start; } else { -uint8_t x_15; -x_15 = lean_nat_dec_lt(x_2, x_4); -lean_dec(x_4); -lean_dec(x_2); -return x_15; +lean_object* x_16; +x_16 = lean_box(0); +x_5 = x_16; +goto block_11; } } case 1: { -lean_object* x_16; lean_object* x_17; lean_object* x_18; -x_16 = lean_ctor_get(x_3, 0); -x_17 = lean_unsigned_to_nat(1u); -x_18 = lean_nat_add(x_4, x_17); -lean_dec(x_4); -x_3 = x_16; -x_4 = x_18; +lean_object* x_17; lean_object* x_18; lean_object* x_19; +x_17 = lean_ctor_get(x_1, 0); +x_18 = lean_unsigned_to_nat(1u); +x_19 = lean_nat_add(x_2, x_18); +lean_dec(x_2); +x_1 = x_17; +x_2 = x_19; goto _start; } -default: +case 2: { -lean_object* x_20; -x_20 = lean_box(0); -x_5 = x_20; -goto block_11; -} -} -} +switch (lean_obj_tag(x_3)) { case 1: { lean_object* x_21; lean_object* x_22; lean_object* x_23; -x_21 = lean_ctor_get(x_1, 0); +x_21 = lean_ctor_get(x_3, 0); x_22 = lean_unsigned_to_nat(1u); -x_23 = lean_nat_add(x_2, x_22); -lean_dec(x_2); -x_1 = x_21; -x_2 = x_23; +x_23 = lean_nat_add(x_4, x_22); +lean_dec(x_4); +x_3 = x_21; +x_4 = x_23; goto _start; } case 2: { -switch (lean_obj_tag(x_3)) { -case 1: +lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; uint8_t x_29; +x_25 = lean_ctor_get(x_1, 0); +x_26 = lean_ctor_get(x_1, 1); +x_27 = lean_ctor_get(x_3, 0); +x_28 = lean_ctor_get(x_3, 1); +x_29 = lean_level_eq(x_1, x_3); +if (x_29 == 0) { -lean_object* x_25; lean_object* x_26; lean_object* x_27; -x_25 = lean_ctor_get(x_3, 0); -x_26 = lean_unsigned_to_nat(1u); -x_27 = lean_nat_add(x_4, x_26); -lean_dec(x_4); -x_3 = x_25; -x_4 = x_27; -goto _start; -} -case 2: -{ -lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33; -x_29 = lean_ctor_get(x_1, 0); -x_30 = lean_ctor_get(x_1, 1); -x_31 = lean_ctor_get(x_3, 0); -x_32 = lean_ctor_get(x_3, 1); -x_33 = lean_level_eq(x_1, x_3); -if (x_33 == 0) -{ -uint8_t x_34; +uint8_t x_30; lean_dec(x_4); lean_dec(x_2); -x_34 = lean_level_eq(x_29, x_31); -if (x_34 == 0) +x_30 = lean_level_eq(x_25, x_27); +if (x_30 == 0) { -lean_object* x_35; -x_35 = lean_unsigned_to_nat(0u); -x_1 = x_30; -x_2 = x_35; -x_3 = x_32; -x_4 = x_35; +lean_object* x_31; +x_31 = lean_unsigned_to_nat(0u); +x_1 = x_26; +x_2 = x_31; +x_3 = x_28; +x_4 = x_31; goto _start; } else { -lean_object* x_37; -x_37 = lean_unsigned_to_nat(0u); -x_1 = x_29; -x_2 = x_37; -x_3 = x_31; -x_4 = x_37; +lean_object* x_33; +x_33 = lean_unsigned_to_nat(0u); +x_1 = x_25; +x_2 = x_33; +x_3 = x_27; +x_4 = x_33; goto _start; } } else { -uint8_t x_39; -x_39 = lean_nat_dec_lt(x_2, x_4); +uint8_t x_35; +x_35 = lean_nat_dec_lt(x_2, x_4); lean_dec(x_4); lean_dec(x_2); -return x_39; +return x_35; } } default: { -lean_object* x_40; -x_40 = lean_box(0); -x_5 = x_40; +lean_object* x_36; +x_36 = lean_box(0); +x_5 = x_36; goto block_11; } } @@ -1442,64 +2121,64 @@ case 3: switch (lean_obj_tag(x_3)) { case 1: { -lean_object* x_41; lean_object* x_42; lean_object* x_43; -x_41 = lean_ctor_get(x_3, 0); -x_42 = lean_unsigned_to_nat(1u); -x_43 = lean_nat_add(x_4, x_42); +lean_object* x_37; lean_object* x_38; lean_object* x_39; +x_37 = lean_ctor_get(x_3, 0); +x_38 = lean_unsigned_to_nat(1u); +x_39 = lean_nat_add(x_4, x_38); lean_dec(x_4); -x_3 = x_41; -x_4 = x_43; +x_3 = x_37; +x_4 = x_39; goto _start; } case 3: { -lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; uint8_t x_49; -x_45 = lean_ctor_get(x_1, 0); -x_46 = lean_ctor_get(x_1, 1); -x_47 = lean_ctor_get(x_3, 0); -x_48 = lean_ctor_get(x_3, 1); -x_49 = lean_level_eq(x_1, x_3); -if (x_49 == 0) +lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; uint8_t x_45; +x_41 = lean_ctor_get(x_1, 0); +x_42 = lean_ctor_get(x_1, 1); +x_43 = lean_ctor_get(x_3, 0); +x_44 = lean_ctor_get(x_3, 1); +x_45 = lean_level_eq(x_1, x_3); +if (x_45 == 0) { -uint8_t x_50; +uint8_t x_46; lean_dec(x_4); lean_dec(x_2); -x_50 = lean_level_eq(x_45, x_47); -if (x_50 == 0) +x_46 = lean_level_eq(x_41, x_43); +if (x_46 == 0) { -lean_object* x_51; -x_51 = lean_unsigned_to_nat(0u); -x_1 = x_46; -x_2 = x_51; -x_3 = x_48; -x_4 = x_51; +lean_object* x_47; +x_47 = lean_unsigned_to_nat(0u); +x_1 = x_42; +x_2 = x_47; +x_3 = x_44; +x_4 = x_47; goto _start; } else { -lean_object* x_53; -x_53 = lean_unsigned_to_nat(0u); -x_1 = x_45; -x_2 = x_53; -x_3 = x_47; -x_4 = x_53; +lean_object* x_49; +x_49 = lean_unsigned_to_nat(0u); +x_1 = x_41; +x_2 = x_49; +x_3 = x_43; +x_4 = x_49; goto _start; } } else { -uint8_t x_55; -x_55 = lean_nat_dec_lt(x_2, x_4); +uint8_t x_51; +x_51 = lean_nat_dec_lt(x_2, x_4); lean_dec(x_4); lean_dec(x_2); -return x_55; +return x_51; } } default: { -lean_object* x_56; -x_56 = lean_box(0); -x_5 = x_56; +lean_object* x_52; +x_52 = lean_box(0); +x_5 = x_52; goto block_11; } } @@ -1509,43 +2188,43 @@ case 4: switch (lean_obj_tag(x_3)) { case 1: { -lean_object* x_57; lean_object* x_58; lean_object* x_59; -x_57 = lean_ctor_get(x_3, 0); -x_58 = lean_unsigned_to_nat(1u); -x_59 = lean_nat_add(x_4, x_58); +lean_object* x_53; lean_object* x_54; lean_object* x_55; +x_53 = lean_ctor_get(x_3, 0); +x_54 = lean_unsigned_to_nat(1u); +x_55 = lean_nat_add(x_4, x_54); lean_dec(x_4); -x_3 = x_57; -x_4 = x_59; +x_3 = x_53; +x_4 = x_55; goto _start; } case 4: { -lean_object* x_61; lean_object* x_62; uint8_t x_63; -x_61 = lean_ctor_get(x_1, 0); -x_62 = lean_ctor_get(x_3, 0); -x_63 = lean_name_dec_eq(x_61, x_62); -if (x_63 == 0) +lean_object* x_57; lean_object* x_58; uint8_t x_59; +x_57 = lean_ctor_get(x_1, 0); +x_58 = lean_ctor_get(x_3, 0); +x_59 = lean_name_dec_eq(x_57, x_58); +if (x_59 == 0) { -uint8_t x_64; +uint8_t x_60; lean_dec(x_4); lean_dec(x_2); -x_64 = l_Lean_Name_lt___main(x_61, x_62); -return x_64; +x_60 = l_Lean_Name_lt___main(x_57, x_58); +return x_60; } else { -uint8_t x_65; -x_65 = lean_nat_dec_lt(x_2, x_4); +uint8_t x_61; +x_61 = lean_nat_dec_lt(x_2, x_4); lean_dec(x_4); lean_dec(x_2); -return x_65; +return x_61; } } default: { -lean_object* x_66; -x_66 = lean_box(0); -x_5 = x_66; +lean_object* x_62; +x_62 = lean_box(0); +x_5 = x_62; goto block_11; } } @@ -1555,43 +2234,43 @@ default: switch (lean_obj_tag(x_3)) { case 1: { -lean_object* x_67; lean_object* x_68; lean_object* x_69; -x_67 = lean_ctor_get(x_3, 0); -x_68 = lean_unsigned_to_nat(1u); -x_69 = lean_nat_add(x_4, x_68); +lean_object* x_63; lean_object* x_64; lean_object* x_65; +x_63 = lean_ctor_get(x_3, 0); +x_64 = lean_unsigned_to_nat(1u); +x_65 = lean_nat_add(x_4, x_64); lean_dec(x_4); -x_3 = x_67; -x_4 = x_69; +x_3 = x_63; +x_4 = x_65; goto _start; } case 5: { -lean_object* x_71; lean_object* x_72; uint8_t x_73; -x_71 = lean_ctor_get(x_1, 0); -x_72 = lean_ctor_get(x_3, 0); -x_73 = lean_name_dec_eq(x_71, x_72); -if (x_73 == 0) +lean_object* x_67; lean_object* x_68; uint8_t x_69; +x_67 = lean_ctor_get(x_1, 0); +x_68 = lean_ctor_get(x_3, 0); +x_69 = lean_name_dec_eq(x_67, x_68); +if (x_69 == 0) { -uint8_t x_74; +uint8_t x_70; lean_dec(x_4); lean_dec(x_2); -x_74 = l_Lean_Name_quickLt(x_71, x_72); -return x_74; +x_70 = l_Lean_Name_quickLt(x_67, x_68); +return x_70; } else { -uint8_t x_75; -x_75 = lean_nat_dec_lt(x_2, x_4); +uint8_t x_71; +x_71 = lean_nat_dec_lt(x_2, x_4); lean_dec(x_4); lean_dec(x_2); -return x_75; +return x_71; } } default: { -lean_object* x_76; -x_76 = lean_box(0); -x_5 = x_76; +lean_object* x_72; +x_72 = lean_box(0); +x_5 = x_72; goto block_11; } } @@ -1741,6 +2420,7 @@ _start: lean_object* x_3; if (lean_obj_tag(x_1) == 0) { +lean_dec(x_1); return x_2; } else @@ -1766,7 +2446,7 @@ x_4 = lean_level_eq(x_1, x_2); if (x_4 == 0) { lean_object* x_5; -x_5 = lean_level_mk_imax(x_1, x_2); +x_5 = l_Lean_mkLevelIMax(x_1, x_2); return x_5; } else @@ -1853,7 +2533,7 @@ if (x_4 == 0) { lean_object* x_5; lean_object* x_6; x_5 = l_Lean_Level_addOffsetAux___main(x_3, x_2); -x_6 = lean_level_mk_max(x_1, x_5); +x_6 = l_Lean_mkLevelMax(x_1, x_5); return x_6; } else @@ -2209,7 +2889,7 @@ x_17 = lean_array_get(x_16, x_15, x_3); x_18 = l_Lean_Level_getLevelOffset___main(x_17); x_19 = l_Lean_Level_getOffsetAux___main(x_17, x_3); lean_dec(x_17); -x_20 = lean_box(0); +x_20 = l_Lean_mkLevelZero; x_21 = l___private_Init_Lean_Level_5__mkMaxAux___main(x_15, x_4, x_13, x_18, x_19, x_20); lean_dec(x_4); lean_dec(x_15); @@ -2238,7 +2918,7 @@ return x_28; else { lean_object* x_29; lean_object* x_30; lean_object* x_31; -x_29 = lean_level_mk_max(x_22, x_23); +x_29 = l_Lean_mkLevelMax(x_22, x_23); x_30 = l_Lean_Level_normalize___main(x_29); lean_dec(x_29); x_31 = l_Lean_Level_addOffsetAux___main(x_4, x_30); @@ -2399,7 +3079,7 @@ if (x_11 == 0) { lean_object* x_12; lean_object* x_13; x_12 = lean_ctor_get(x_9, 0); -x_13 = lean_level_mk_max(x_8, x_12); +x_13 = l_Lean_mkLevelMax(x_8, x_12); lean_ctor_set(x_9, 0, x_13); return x_9; } @@ -2409,7 +3089,7 @@ lean_object* x_14; lean_object* x_15; lean_object* x_16; x_14 = lean_ctor_get(x_9, 0); lean_inc(x_14); lean_dec(x_9); -x_15 = lean_level_mk_max(x_8, x_14); +x_15 = l_Lean_mkLevelMax(x_8, x_14); x_16 = lean_alloc_ctor(1, 1, 0); lean_ctor_set(x_16, 0, x_15); return x_16; @@ -2451,7 +3131,7 @@ if (x_24 == 0) { lean_object* x_25; lean_object* x_26; x_25 = lean_ctor_get(x_22, 0); -x_26 = lean_level_mk_max(x_21, x_25); +x_26 = l_Lean_mkLevelMax(x_21, x_25); lean_ctor_set(x_22, 0, x_26); return x_22; } @@ -2461,7 +3141,7 @@ lean_object* x_27; lean_object* x_28; lean_object* x_29; x_27 = lean_ctor_get(x_22, 0); lean_inc(x_27); lean_dec(x_22); -x_28 = lean_level_mk_max(x_21, x_27); +x_28 = l_Lean_mkLevelMax(x_21, x_27); x_29 = lean_alloc_ctor(1, 1, 0); lean_ctor_set(x_29, 0, x_28); return x_29; @@ -3027,6 +3707,7 @@ switch (lean_obj_tag(x_1)) { case 0: { lean_object* x_2; +lean_dec(x_1); x_2 = l_Lean_Level_LevelToFormat_toResult___main___closed__1; return x_2; } @@ -3154,9 +3835,9 @@ lean_object* _init_l_Lean_Level_updateSucc_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_Lean_Level_mvarId_x21___closed__1; -x_2 = lean_unsigned_to_nat(354u); -x_3 = lean_unsigned_to_nat(14u); +x_1 = l_Lean_Level_mkData___closed__2; +x_2 = lean_unsigned_to_nat(412u); +x_3 = lean_unsigned_to_nat(16u); x_4 = l_Lean_Level_updateSucc_x21___closed__1; x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4); return x_5; @@ -3203,9 +3884,9 @@ lean_object* _init_l_Lean_Level_updateMax_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_Lean_Level_mvarId_x21___closed__1; -x_2 = lean_unsigned_to_nat(363u); -x_3 = lean_unsigned_to_nat(17u); +x_1 = l_Lean_Level_mkData___closed__2; +x_2 = lean_unsigned_to_nat(421u); +x_3 = lean_unsigned_to_nat(19u); x_4 = l_Lean_Level_updateMax_x21___closed__1; x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4); return x_5; @@ -3253,9 +3934,9 @@ lean_object* _init_l_Lean_Level_updateIMax_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_Lean_Level_mvarId_x21___closed__1; -x_2 = lean_unsigned_to_nat(372u); -x_3 = lean_unsigned_to_nat(17u); +x_1 = l_Lean_Level_mkData___closed__2; +x_2 = lean_unsigned_to_nat(430u); +x_3 = lean_unsigned_to_nat(19u); x_4 = l_Lean_Level_updateIMax_x21___closed__1; x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4); return x_5; @@ -3266,29 +3947,62 @@ _start: { if (lean_obj_tag(x_1) == 2) { -lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; -x_4 = lean_ctor_get(x_1, 0); -lean_inc(x_4); -x_5 = lean_ctor_get(x_1, 1); -lean_inc(x_5); -lean_dec(x_1); -x_6 = lean_level_mk_imax(x_4, x_5); -x_7 = lean_level_update_imax(x_6, x_2, x_3); -return x_7; +uint8_t x_4; +x_4 = !lean_is_exclusive(x_1); +if (x_4 == 0) +{ +lean_object* x_5; +lean_ctor_set_tag(x_1, 3); +x_5 = lean_level_update_imax(x_1, x_2, x_3); +return x_5; } else { -lean_object* x_8; lean_object* x_9; lean_object* x_10; +lean_object* x_6; lean_object* x_7; uint64_t x_8; lean_object* x_9; lean_object* x_10; +x_6 = lean_ctor_get(x_1, 0); +x_7 = lean_ctor_get(x_1, 1); +x_8 = lean_ctor_get_uint64(x_1, sizeof(void*)*2); +lean_inc(x_7); +lean_inc(x_6); +lean_dec(x_1); +x_9 = lean_alloc_ctor(3, 2, 8); +lean_ctor_set(x_9, 0, x_6); +lean_ctor_set(x_9, 1, x_7); +lean_ctor_set_uint64(x_9, sizeof(void*)*2, x_8); +x_10 = lean_level_update_imax(x_9, x_2, x_3); +return x_10; +} +} +else +{ +lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_8 = l_Lean_Level_Inhabited; -x_9 = l_Lean_Level_updateIMax_x21___closed__2; -x_10 = lean_panic_fn(x_9); -return x_10; +x_11 = l_Lean_Level_Inhabited; +x_12 = l_Lean_Level_updateIMax_x21___closed__2; +x_13 = lean_panic_fn(x_12); +return x_13; } } } +lean_object* l_Nat_toLevel(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = l_Lean_Level_ofNat___main(x_1); +return x_2; +} +} +lean_object* l_Nat_toLevel___boxed(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = l_Nat_toLevel(x_1); +lean_dec(x_1); +return x_2; +} +} lean_object* initialize_Init_Data_Option_Basic(lean_object*); lean_object* initialize_Init_Data_HashMap_Default(lean_object*); lean_object* initialize_Init_Data_PersistentHashMap_Default(lean_object*); @@ -3314,22 +4028,36 @@ lean_dec_ref(res); res = initialize_Init_Lean_Format(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +l_Lean_Level_Data_inhabited = _init_l_Lean_Level_Data_inhabited(); +l_Lean_Level_mkData___closed__1 = _init_l_Lean_Level_mkData___closed__1(); +lean_mark_persistent(l_Lean_Level_mkData___closed__1); +l_Lean_Level_mkData___closed__2 = _init_l_Lean_Level_mkData___closed__2(); +lean_mark_persistent(l_Lean_Level_mkData___closed__2); +l_Lean_Level_mkData___closed__3 = _init_l_Lean_Level_mkData___closed__3(); +lean_mark_persistent(l_Lean_Level_mkData___closed__3); +l_Lean_Level_mkData___closed__4 = _init_l_Lean_Level_mkData___closed__4(); +lean_mark_persistent(l_Lean_Level_mkData___closed__4); +l_Lean_Level_mkData___boxed__const__1 = _init_l_Lean_Level_mkData___boxed__const__1(); +lean_mark_persistent(l_Lean_Level_mkData___boxed__const__1); +l_Lean_Level_Hashable___closed__1 = _init_l_Lean_Level_Hashable___closed__1(); +lean_mark_persistent(l_Lean_Level_Hashable___closed__1); +l_Lean_Level_Hashable = _init_l_Lean_Level_Hashable(); +lean_mark_persistent(l_Lean_Level_Hashable); +l_Lean_mkLevelZero___closed__1 = _init_l_Lean_mkLevelZero___closed__1(); +l_Lean_mkLevelZero___closed__2 = _init_l_Lean_mkLevelZero___closed__2(); +lean_mark_persistent(l_Lean_mkLevelZero___closed__2); +l_Lean_mkLevelZero = _init_l_Lean_mkLevelZero(); +lean_mark_persistent(l_Lean_mkLevelZero); +l_Lean_mkLevelOne___closed__1 = _init_l_Lean_mkLevelOne___closed__1(); +lean_mark_persistent(l_Lean_mkLevelOne___closed__1); +l_Lean_mkLevelOne = _init_l_Lean_mkLevelOne(); +lean_mark_persistent(l_Lean_mkLevelOne); l_Lean_Level_Inhabited = _init_l_Lean_Level_Inhabited(); lean_mark_persistent(l_Lean_Level_Inhabited); l_Lean_Level_mvarId_x21___closed__1 = _init_l_Lean_Level_mvarId_x21___closed__1(); lean_mark_persistent(l_Lean_Level_mvarId_x21___closed__1); l_Lean_Level_mvarId_x21___closed__2 = _init_l_Lean_Level_mvarId_x21___closed__2(); lean_mark_persistent(l_Lean_Level_mvarId_x21___closed__2); -l_Lean_Level_mvarId_x21___closed__3 = _init_l_Lean_Level_mvarId_x21___closed__3(); -lean_mark_persistent(l_Lean_Level_mvarId_x21___closed__3); -l_Lean_Level_one___closed__1 = _init_l_Lean_Level_one___closed__1(); -lean_mark_persistent(l_Lean_Level_one___closed__1); -l_Lean_Level_one = _init_l_Lean_Level_one(); -lean_mark_persistent(l_Lean_Level_one); -l_Lean_Level_hashable___closed__1 = _init_l_Lean_Level_hashable___closed__1(); -lean_mark_persistent(l_Lean_Level_hashable___closed__1); -l_Lean_Level_hashable = _init_l_Lean_Level_hashable(); -lean_mark_persistent(l_Lean_Level_hashable); l_Lean_Level_HasBeq___closed__1 = _init_l_Lean_Level_HasBeq___closed__1(); lean_mark_persistent(l_Lean_Level_HasBeq___closed__1); l_Lean_Level_HasBeq = _init_l_Lean_Level_HasBeq(); diff --git a/stage0/library/Init/Lean/Meta/Default.c b/stage0/library/Init/Lean/Meta/Default.c index 30485485f8..1367aa9dee 100644 --- a/stage0/library/Init/Lean/Meta/Default.c +++ b/stage0/library/Init/Lean/Meta/Default.c @@ -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); diff --git a/stage0/library/Init/Lean/Meta/InferType.c b/stage0/library/Init/Lean/Meta/InferType.c index f5330f462f..12486bf3d3 100644 --- a/stage0/library/Init/Lean/Meta/InferType.c +++ b/stage0/library/Init/Lean/Meta/InferType.c @@ -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); diff --git a/stage0/library/Init/Lean/Meta/LevelDefEq.c b/stage0/library/Init/Lean/Meta/LevelDefEq.c index 6d2cb451f2..8ce169f5c9 100644 --- a/stage0/library/Init/Lean/Meta/LevelDefEq.c +++ b/stage0/library/Init/Lean/Meta/LevelDefEq.c @@ -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) diff --git a/stage0/library/Init/Lean/MetavarContext.c b/stage0/library/Init/Lean/MetavarContext.c index 369d0a3d64..45fb3b912b 100644 --- a/stage0/library/Init/Lean/MetavarContext.c +++ b/stage0/library/Init/Lean/MetavarContext.c @@ -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; diff --git a/stage0/library/Init/Lean/TypeClass/Context.c b/stage0/library/Init/Lean/TypeClass/Context.c index 034db59d2f..1293921dd8 100644 --- a/stage0/library/Init/Lean/TypeClass/Context.c +++ b/stage0/library/Init/Lean/TypeClass/Context.c @@ -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); diff --git a/stage0/library/Init/Lean/TypeClass/Synth.c b/stage0/library/Init/Lean/TypeClass/Synth.c index 6c724bc985..9e01544932 100644 --- a/stage0/library/Init/Lean/TypeClass/Synth.c +++ b/stage0/library/Init/Lean/TypeClass/Synth.c @@ -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; diff --git a/stage0/src/kernel/level.cpp b/stage0/src/kernel/level.cpp index 93664af41e..a0b2317f26 100644 --- a/stage0/src/kernel/level.cpp +++ b/stage0/src/kernel/level.cpp @@ -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(lvl, num_objs*sizeof(object*), hash); - cnstr_set_scalar(lvl, num_objs*sizeof(object*) + sizeof(unsigned), depth); - cnstr_set_scalar(lvl, num_objs*sizeof(object*) + 2*sizeof(unsigned), has_param); - cnstr_set_scalar(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(lvl, num_objs*sizeof(object*)); } -inline static unsigned get_depth(object * lvl, unsigned num_objs) { return cnstr_get_scalar(lvl, num_objs*sizeof(object*) + sizeof(unsigned)); } -inline static bool get_has_param(object * lvl, unsigned num_objs) { return cnstr_get_scalar(lvl, num_objs*sizeof(object*) + 2*sizeof(unsigned)); } -inline static bool get_has_mvar(object * lvl, unsigned num_objs) { return cnstr_get_scalar(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(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(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 object * level_mk_max_imax(obj_arg l1, obj_arg l2) { - object * r = alloc_cnstr(static_cast(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(l1, l2); -} - -extern "C" object * lean_level_mk_imax(obj_arg l1, obj_arg l2) { - return level_mk_max_imax(l1, l2); -} - -extern "C" object * lean_level_mk_param(obj_arg n) { - object * r = alloc_cnstr(static_cast(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(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)); } diff --git a/stage0/src/kernel/level.h b/stage0/src/kernel/level.h index 3bb391ae04..bf48d4d3e0 100644 --- a/stage0/src/kernel/level.h +++ b/stage0/src/kernel/level.h @@ -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(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(obj_tag(raw())); } - static unsigned hash(b_obj_arg l); - unsigned hash() const { return hash(raw()); } + level_kind kind() const { return static_cast(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); diff --git a/stage0/src/library/compiler/util.cpp b/stage0/src/library/compiler/util.cpp index c8bfaa1ec6..f4c8c8ce4e 100644 --- a/stage0/src/library/compiler/util.cpp +++ b/stage0/src/library/compiler/util.cpp @@ -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() ||