From ba286dee8eb30fe6efda1c7744d5fac4def44212 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Oct 2019 17:44:41 -0700 Subject: [PATCH] chore: update stage0 --- src/kernel/expr.cpp | 4 - src/stage0/Init/Lean/Elaborator/Basic.c | 124 +- src/stage0/Init/Lean/Expr.c | 77 +- src/stage0/Init/Lean/TypeClass/Context.c | 491 +++++--- src/stage0/Init/Lean/TypeClass/Synth.c | 81 +- src/stage0/Init/Lean/TypeContext.c | 1461 +++++++++++++++++++++- 6 files changed, 1938 insertions(+), 300 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index a1028f0ebb..1cc6260e01 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -867,10 +867,6 @@ expr infer_implicit(expr const & t, bool strict) { // ======================================= // Extra exports -extern "C" uint8 lean_expr_has_mvar(b_obj_arg o) { - return has_mvar(TO_REF(expr, o)); -} - extern "C" uint8 lean_expr_has_expr_mvar(b_obj_arg o) { return has_expr_mvar(TO_REF(expr, o)); } diff --git a/src/stage0/Init/Lean/Elaborator/Basic.c b/src/stage0/Init/Lean/Elaborator/Basic.c index 7f6da9fc6b..41aa5bbc80 100644 --- a/src/stage0/Init/Lean/Elaborator/Basic.c +++ b/src/stage0/Init/Lean/Elaborator/Basic.c @@ -162,7 +162,6 @@ extern lean_object* l_List_get_x21___main___rarg___closed__1; lean_object* lean_mk_empty_environment(uint32_t, lean_object*); lean_object* l_Lean_LocalContext_mkLambda(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_termElabAttribute; -lean_object* l_Lean_NameGenerator_next(lean_object*); lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main___at_Lean_addBuiltinCommandElab___spec__9(lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_AttributeImpl_inhabited___closed__4; lean_object* l_Lean_Elab_logErrorUsingCmdPos___boxed(lean_object*, lean_object*, lean_object*); @@ -330,7 +329,6 @@ lean_object* l_Lean_Elab_runElab___at_Lean_Elab_elabCommandAtFrontend___spec__1( lean_object* l_Lean_registerBuiltinCommandElabAttr___closed__4; lean_object* l_Lean_declareBuiltinElab___closed__2; lean_object* l_Lean_Name_replacePrefix___main(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_NameGenerator_curr(lean_object*); lean_object* l_Lean_ElabException_Inhabited___closed__2; extern lean_object* l_System_FilePath_dirName___closed__1; lean_object* l_panic(lean_object*, lean_object*, lean_object*); @@ -345,6 +343,7 @@ lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkTermElabAttribute___s size_t lean_usize_modn(size_t, lean_object*); lean_object* l_Lean_ParametricAttribute_setParam___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_registerBuiltinTermElabAttr___lambda__1___closed__3; +lean_object* lean_name_mk_numeral(lean_object*, lean_object*); extern lean_object* l_Array_mfindAux___main___at_Lean_findFile___spec__2___closed__1; lean_object* l_Lean_ConstantInfo_type(lean_object*); lean_object* lean_environment_find(lean_object*, lean_object*); @@ -10060,47 +10059,102 @@ uint8_t x_2; x_2 = !lean_is_exclusive(x_1); if (x_2 == 0) { -lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; +lean_object* x_3; uint8_t x_4; x_3 = lean_ctor_get(x_1, 3); -lean_inc(x_3); -x_4 = l_Lean_NameGenerator_curr(x_3); -x_5 = l_Lean_NameGenerator_next(x_3); -lean_ctor_set(x_1, 3, x_5); -x_6 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_6, 0, x_4); -lean_ctor_set(x_6, 1, x_1); -return x_6; +x_4 = !lean_is_exclusive(x_3); +if (x_4 == 0) +{ +lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; +x_5 = lean_ctor_get(x_3, 0); +x_6 = lean_ctor_get(x_3, 1); +lean_inc(x_6); +lean_inc(x_5); +x_7 = lean_name_mk_numeral(x_5, x_6); +x_8 = lean_unsigned_to_nat(1u); +x_9 = lean_nat_add(x_6, x_8); +lean_dec(x_6); +lean_ctor_set(x_3, 1, x_9); +x_10 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_10, 0, x_7); +lean_ctor_set(x_10, 1, x_1); +return x_10; } else { -lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; -x_7 = lean_ctor_get(x_1, 0); -x_8 = lean_ctor_get(x_1, 1); -x_9 = lean_ctor_get(x_1, 2); -x_10 = lean_ctor_get(x_1, 3); -x_11 = lean_ctor_get(x_1, 4); -x_12 = lean_ctor_get(x_1, 5); +lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; +x_11 = lean_ctor_get(x_3, 0); +x_12 = lean_ctor_get(x_3, 1); lean_inc(x_12); lean_inc(x_11); -lean_inc(x_10); -lean_inc(x_9); -lean_inc(x_8); -lean_inc(x_7); -lean_dec(x_1); -lean_inc(x_10); -x_13 = l_Lean_NameGenerator_curr(x_10); -x_14 = l_Lean_NameGenerator_next(x_10); -x_15 = lean_alloc_ctor(0, 6, 0); -lean_ctor_set(x_15, 0, x_7); -lean_ctor_set(x_15, 1, x_8); -lean_ctor_set(x_15, 2, x_9); -lean_ctor_set(x_15, 3, x_14); -lean_ctor_set(x_15, 4, x_11); -lean_ctor_set(x_15, 5, x_12); +lean_dec(x_3); +lean_inc(x_12); +lean_inc(x_11); +x_13 = lean_name_mk_numeral(x_11, x_12); +x_14 = lean_unsigned_to_nat(1u); +x_15 = lean_nat_add(x_12, x_14); +lean_dec(x_12); x_16 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_16, 0, x_13); +lean_ctor_set(x_16, 0, x_11); lean_ctor_set(x_16, 1, x_15); -return x_16; +lean_ctor_set(x_1, 3, x_16); +x_17 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_17, 0, x_13); +lean_ctor_set(x_17, 1, x_1); +return x_17; +} +} +else +{ +lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; +x_18 = lean_ctor_get(x_1, 3); +x_19 = lean_ctor_get(x_1, 0); +x_20 = lean_ctor_get(x_1, 1); +x_21 = lean_ctor_get(x_1, 2); +x_22 = lean_ctor_get(x_1, 4); +x_23 = lean_ctor_get(x_1, 5); +lean_inc(x_23); +lean_inc(x_22); +lean_inc(x_18); +lean_inc(x_21); +lean_inc(x_20); +lean_inc(x_19); +lean_dec(x_1); +x_24 = lean_ctor_get(x_18, 0); +lean_inc(x_24); +x_25 = lean_ctor_get(x_18, 1); +lean_inc(x_25); +if (lean_is_exclusive(x_18)) { + lean_ctor_release(x_18, 0); + lean_ctor_release(x_18, 1); + x_26 = x_18; +} else { + lean_dec_ref(x_18); + x_26 = lean_box(0); +} +lean_inc(x_25); +lean_inc(x_24); +x_27 = lean_name_mk_numeral(x_24, x_25); +x_28 = lean_unsigned_to_nat(1u); +x_29 = lean_nat_add(x_25, x_28); +lean_dec(x_25); +if (lean_is_scalar(x_26)) { + x_30 = lean_alloc_ctor(0, 2, 0); +} else { + x_30 = x_26; +} +lean_ctor_set(x_30, 0, x_24); +lean_ctor_set(x_30, 1, x_29); +x_31 = lean_alloc_ctor(0, 6, 0); +lean_ctor_set(x_31, 0, x_19); +lean_ctor_set(x_31, 1, x_20); +lean_ctor_set(x_31, 2, x_21); +lean_ctor_set(x_31, 3, x_30); +lean_ctor_set(x_31, 4, x_22); +lean_ctor_set(x_31, 5, x_23); +x_32 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_32, 0, x_27); +lean_ctor_set(x_32, 1, x_31); +return x_32; } } } diff --git a/src/stage0/Init/Lean/Expr.c b/src/stage0/Init/Lean/Expr.c index 3e5c248c13..5686ce9704 100644 --- a/src/stage0/Init/Lean/Expr.c +++ b/src/stage0/Init/Lean/Expr.c @@ -64,6 +64,7 @@ lean_object* l_Lean_Expr_fvarName___closed__1; lean_object* lean_expr_local(lean_object*, lean_object*, lean_object*, uint8_t); lean_object* lean_expr_mk_app(lean_object*, lean_object*); lean_object* l_Lean_Expr_quickLt___boxed(lean_object*, lean_object*); +lean_object* l_Lean_Expr_hasExprMVar___boxed(lean_object*); lean_object* l_Lean_Expr_bindingBody(lean_object*); lean_object* l_Lean_Expr_isAppOf___boxed(lean_object*, lean_object*); lean_object* l_Lean_Expr_updateLet_x21(lean_object*, lean_object*, lean_object*, lean_object*); @@ -178,6 +179,7 @@ lean_object* l_Lean_BinderInfo_HasBeq___closed__1; uint8_t lean_expr_lt(lean_object*, lean_object*); lean_object* l_Lean_Expr_updateApp___boxed(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Expr_isApp(lean_object*); +lean_object* l_Lean_Expr_hasLevelMVar___boxed(lean_object*); lean_object* lean_array_get_size(lean_object*); lean_object* l_Lean_mkDecIsTrue(lean_object*, lean_object*); lean_object* l_Lean_Expr_updateForall___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -190,7 +192,7 @@ lean_object* l_Lean_Expr_updateProj_x21(lean_object*, lean_object*); lean_object* l_Lean_Expr_const___boxed(lean_object*, lean_object*); lean_object* l_Lean_Expr_constLevels(lean_object*); lean_object* l_Lean_Expr_updateApp_x21(lean_object*, lean_object*, lean_object*); -uint8_t lean_expr_has_mvar(lean_object*); +uint8_t l_Lean_Expr_hasMVar(lean_object*); lean_object* l_Lean_Expr_isFVar___boxed(lean_object*); lean_object* l_Lean_Expr_abstractRange___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_fvar___boxed(lean_object*); @@ -206,6 +208,7 @@ lean_object* l_Lean_Expr_bindingName___closed__1; uint8_t l_Lean_Expr_isBVar(lean_object*); lean_object* l_Lean_Expr_updateSort_x21___closed__1; lean_object* l_Lean_Expr_isBinding___boxed(lean_object*); +uint8_t lean_expr_has_expr_mvar(lean_object*); lean_object* l_Lean_Expr_Hashable; lean_object* l_Lean_Expr_getAppNumArgs___boxed(lean_object*); lean_object* l_Lean_Expr_bindingBody___boxed(lean_object*); @@ -234,6 +237,7 @@ lean_object* l_Lean_Expr_isConst___boxed(lean_object*); lean_object* l_Lean_Expr_lt___boxed(lean_object*, lean_object*); lean_object* l_Lean_ExprStructEq_Hashable___closed__1; lean_object* lean_expr_update_let(lean_object*, lean_object*, lean_object*, lean_object*); +uint8_t lean_expr_has_level_mvar(lean_object*); uint8_t l_Lean_Expr_isLambda(lean_object*); lean_object* l_panicWithPos___at_Array_findIdx_x21___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_BinderInfo_isInstImplicit(uint8_t x_1) { @@ -706,11 +710,50 @@ x_4 = lean_box(x_3); return x_4; } } +lean_object* l_Lean_Expr_hasExprMVar___boxed(lean_object* x_1) { +_start: +{ +uint8_t x_2; lean_object* x_3; +x_2 = lean_expr_has_expr_mvar(x_1); +lean_dec(x_1); +x_3 = lean_box(x_2); +return x_3; +} +} +lean_object* l_Lean_Expr_hasLevelMVar___boxed(lean_object* x_1) { +_start: +{ +uint8_t x_2; lean_object* x_3; +x_2 = lean_expr_has_level_mvar(x_1); +lean_dec(x_1); +x_3 = lean_box(x_2); +return x_3; +} +} +uint8_t l_Lean_Expr_hasMVar(lean_object* x_1) { +_start: +{ +uint8_t x_2; +x_2 = lean_expr_has_expr_mvar(x_1); +if (x_2 == 0) +{ +uint8_t x_3; +x_3 = lean_expr_has_level_mvar(x_1); +return x_3; +} +else +{ +uint8_t x_4; +x_4 = 1; +return x_4; +} +} +} lean_object* l_Lean_Expr_hasMVar___boxed(lean_object* x_1) { _start: { uint8_t x_2; lean_object* x_3; -x_2 = lean_expr_has_mvar(x_1); +x_2 = l_Lean_Expr_hasMVar(x_1); lean_dec(x_1); x_3 = lean_box(x_2); return x_3; @@ -1410,7 +1453,7 @@ else { lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; x_3 = l_Lean_Expr_constName___closed__1; -x_4 = lean_unsigned_to_nat(205u); +x_4 = lean_unsigned_to_nat(211u); x_5 = lean_unsigned_to_nat(15u); x_6 = l_Lean_Expr_constName___closed__2; x_7 = l_panicWithPos___at_Lean_Expr_constName___spec__1(x_3, x_4, x_5, x_6); @@ -1475,7 +1518,7 @@ else { lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; x_3 = l_Lean_Expr_constName___closed__1; -x_4 = lean_unsigned_to_nat(209u); +x_4 = lean_unsigned_to_nat(215u); x_5 = lean_unsigned_to_nat(16u); x_6 = l_Lean_Expr_constName___closed__2; x_7 = l_panicWithPos___at_Lean_Expr_constLevels___spec__1(x_3, x_4, x_5, x_6); @@ -1524,7 +1567,7 @@ else { lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; x_3 = l_Lean_Expr_constName___closed__1; -x_4 = lean_unsigned_to_nat(213u); +x_4 = lean_unsigned_to_nat(219u); x_5 = lean_unsigned_to_nat(14u); x_6 = l_Lean_Expr_bvarIdx___closed__1; x_7 = l_panicWithPos___at_Array_findIdx_x21___spec__1(x_3, x_4, x_5, x_6); @@ -1563,7 +1606,7 @@ else { lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; x_3 = l_Lean_Expr_constName___closed__1; -x_4 = lean_unsigned_to_nat(217u); +x_4 = lean_unsigned_to_nat(223u); x_5 = lean_unsigned_to_nat(12u); x_6 = l_Lean_Expr_fvarName___closed__1; x_7 = l_panicWithPos___at_Lean_Expr_constName___spec__1(x_3, x_4, x_5, x_6); @@ -1610,7 +1653,7 @@ default: { lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; x_4 = l_Lean_Expr_constName___closed__1; -x_5 = lean_unsigned_to_nat(222u); +x_5 = lean_unsigned_to_nat(228u); x_6 = lean_unsigned_to_nat(21u); x_7 = l_Lean_Expr_bindingName___closed__1; x_8 = l_panicWithPos___at_Lean_Expr_constName___spec__1(x_4, x_5, x_6, x_7); @@ -1674,7 +1717,7 @@ default: { lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; x_4 = l_Lean_Expr_constName___closed__1; -x_5 = lean_unsigned_to_nat(227u); +x_5 = lean_unsigned_to_nat(233u); x_6 = lean_unsigned_to_nat(21u); x_7 = l_Lean_Expr_bindingName___closed__1; x_8 = l_panicWithPos___at_Lean_Expr_bindingDomain___spec__1(x_4, x_5, x_6, x_7); @@ -1724,7 +1767,7 @@ default: { lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; x_4 = l_Lean_Expr_constName___closed__1; -x_5 = lean_unsigned_to_nat(232u); +x_5 = lean_unsigned_to_nat(238u); x_6 = lean_unsigned_to_nat(21u); x_7 = l_Lean_Expr_bindingName___closed__1; x_8 = l_panicWithPos___at_Lean_Expr_bindingDomain___spec__1(x_4, x_5, x_6, x_7); @@ -1764,7 +1807,7 @@ else { lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; x_3 = l_Lean_Expr_constName___closed__1; -x_4 = lean_unsigned_to_nat(236u); +x_4 = lean_unsigned_to_nat(242u); x_5 = lean_unsigned_to_nat(18u); x_6 = l_Lean_Expr_letName___closed__1; x_7 = l_panicWithPos___at_Lean_Expr_constName___spec__1(x_3, x_4, x_5, x_6); @@ -2123,7 +2166,7 @@ lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); x_5 = l_Lean_Expr_constName___closed__1; -x_6 = lean_unsigned_to_nat(327u); +x_6 = lean_unsigned_to_nat(333u); x_7 = lean_unsigned_to_nat(16u); x_8 = l_Lean_Expr_updateApp_x21___closed__1; x_9 = l_panicWithPos___at_Lean_Expr_bindingDomain___spec__1(x_5, x_6, x_7, x_8); @@ -2154,7 +2197,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_obj lean_dec(x_2); lean_dec(x_1); x_4 = l_Lean_Expr_constName___closed__1; -x_5 = lean_unsigned_to_nat(336u); +x_5 = lean_unsigned_to_nat(342u); x_6 = lean_unsigned_to_nat(16u); x_7 = l_Lean_Expr_constName___closed__2; x_8 = l_panicWithPos___at_Lean_Expr_bindingDomain___spec__1(x_4, x_5, x_6, x_7); @@ -2193,7 +2236,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_obj lean_dec(x_2); lean_dec(x_1); x_4 = l_Lean_Expr_constName___closed__1; -x_5 = lean_unsigned_to_nat(345u); +x_5 = lean_unsigned_to_nat(351u); x_6 = lean_unsigned_to_nat(12u); x_7 = l_Lean_Expr_updateSort_x21___closed__1; x_8 = l_panicWithPos___at_Lean_Expr_bindingDomain___spec__1(x_4, x_5, x_6, x_7); @@ -2232,7 +2275,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_obj lean_dec(x_2); lean_dec(x_1); x_4 = l_Lean_Expr_constName___closed__1; -x_5 = lean_unsigned_to_nat(356u); +x_5 = lean_unsigned_to_nat(362u); x_6 = lean_unsigned_to_nat(16u); x_7 = l_Lean_Expr_updateProj_x21___closed__1; x_8 = l_panicWithPos___at_Lean_Expr_bindingDomain___spec__1(x_4, x_5, x_6, x_7); @@ -2274,7 +2317,7 @@ lean_dec(x_4); lean_dec(x_3); lean_dec(x_1); x_6 = l_Lean_Expr_constName___closed__1; -x_7 = lean_unsigned_to_nat(365u); +x_7 = lean_unsigned_to_nat(371u); x_8 = lean_unsigned_to_nat(22u); x_9 = l_Lean_Expr_updateForall_x21___closed__1; x_10 = l_panicWithPos___at_Lean_Expr_bindingDomain___spec__1(x_6, x_7, x_8, x_9); @@ -2326,7 +2369,7 @@ lean_dec(x_4); lean_dec(x_3); lean_dec(x_1); x_6 = l_Lean_Expr_constName___closed__1; -x_7 = lean_unsigned_to_nat(374u); +x_7 = lean_unsigned_to_nat(380u); x_8 = lean_unsigned_to_nat(18u); x_9 = l_Lean_Expr_updateLambda_x21___closed__1; x_10 = l_panicWithPos___at_Lean_Expr_bindingDomain___spec__1(x_6, x_7, x_8, x_9); @@ -2369,7 +2412,7 @@ lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); x_6 = l_Lean_Expr_constName___closed__1; -x_7 = lean_unsigned_to_nat(383u); +x_7 = lean_unsigned_to_nat(389u); x_8 = lean_unsigned_to_nat(18u); x_9 = l_Lean_Expr_letName___closed__1; x_10 = l_panicWithPos___at_Lean_Expr_bindingDomain___spec__1(x_6, x_7, x_8, x_9); diff --git a/src/stage0/Init/Lean/TypeClass/Context.c b/src/stage0/Init/Lean/TypeClass/Context.c index 34867dac22..618044439c 100644 --- a/src/stage0/Init/Lean/TypeClass/Context.c +++ b/src/stage0/Init/Lean/TypeClass/Context.c @@ -180,7 +180,6 @@ lean_object* l_Lean_TypeClass_Context_eInferIdx___boxed(lean_object*, lean_objec uint8_t lean_nat_dec_le(lean_object*, lean_object*); lean_object* l_Lean_TypeClass_Context_metaPrefix___closed__2; lean_object* l_Lean_TypeClass_Context_eFind___boxed(lean_object*, lean_object*); -uint8_t lean_expr_has_mvar(lean_object*); uint8_t l_Lean_TypeClass_Context_eOccursIn___lambda__1(lean_object*, lean_object*); lean_object* l_panicWithPos___at_Lean_TypeClass_Context_eAssign___spec__1___closed__1; size_t lean_usize_of_nat(lean_object*); @@ -195,6 +194,7 @@ lean_object* l_PersistentArray_getAux___main___at_Lean_TypeClass_Context_uLookup lean_object* l_Lean_TypeClass_Context_uAssign(lean_object*, lean_object*, lean_object*); size_t l_USize_shift__left(size_t, size_t); uint8_t l_Lean_Expr_isBVar(lean_object*); +uint8_t lean_expr_has_expr_mvar(lean_object*); lean_object* l_Lean_TypeClass_Context_uAlphaNormalizeCore(lean_object*, 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_panicWithPos___at_Lean_Expr_bindingDomain___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); @@ -213,6 +213,7 @@ extern lean_object* l_Lean_exprIsInhabited___closed__1; lean_object* level_mk_max(lean_object*, lean_object*); lean_object* l_Lean_TypeClass_Context_uAssign___closed__1; lean_object* l_Lean_TypeClass_Context_uUnify___main___closed__5; +uint8_t lean_expr_has_level_mvar(lean_object*); lean_object* _init_l_Lean_TypeClass_Context_Inhabited___closed__1() { _start: { @@ -2447,20 +2448,32 @@ uint8_t l_Lean_TypeClass_Context_eHasTmpMVar(lean_object* x_1) { _start: { uint8_t x_2; -x_2 = lean_expr_has_mvar(x_1); +x_2 = lean_expr_has_expr_mvar(x_1); if (x_2 == 0) { uint8_t x_3; +x_3 = lean_expr_has_level_mvar(x_1); +if (x_3 == 0) +{ +uint8_t x_4; lean_dec(x_1); -x_3 = 0; -return x_3; +x_4 = 0; +return x_4; } else { -lean_object* x_4; uint8_t x_5; -x_4 = l_Lean_TypeClass_Context_eHasTmpMVar___closed__1; -x_5 = l_Lean_TypeClass_Context_eFind___main(x_4, x_1); -return x_5; +lean_object* x_5; uint8_t x_6; +x_5 = l_Lean_TypeClass_Context_eHasTmpMVar___closed__1; +x_6 = l_Lean_TypeClass_Context_eFind___main(x_5, x_1); +return x_6; +} +} +else +{ +lean_object* x_7; uint8_t x_8; +x_7 = l_Lean_TypeClass_Context_eHasTmpMVar___closed__1; +x_8 = l_Lean_TypeClass_Context_eFind___main(x_7, x_1); +return x_8; } } } @@ -2824,59 +2837,83 @@ lean_object* l_Lean_TypeClass_Context_eUnify___main(lean_object* x_1, lean_objec _start: { lean_object* x_4; uint8_t x_190; -x_190 = lean_expr_has_mvar(x_1); +x_190 = lean_expr_has_expr_mvar(x_1); if (x_190 == 0) { uint8_t x_191; -x_191 = lean_expr_has_mvar(x_2); +x_191 = lean_expr_has_level_mvar(x_1); if (x_191 == 0) { uint8_t x_192; -x_192 = lean_expr_eqv(x_1, x_2); +x_192 = lean_expr_has_expr_mvar(x_2); if (x_192 == 0) { -lean_object* x_193; lean_object* x_194; lean_object* x_195; lean_object* x_196; lean_object* x_197; lean_object* x_198; lean_object* x_199; lean_object* x_200; -x_193 = lean_expr_dbg_to_string(x_1); -lean_dec(x_1); -x_194 = l_Lean_TypeClass_Context_eUnify___main___closed__1; -x_195 = lean_string_append(x_194, x_193); -lean_dec(x_193); -x_196 = l_Lean_TypeClass_Context_uUnify___main___closed__2; -x_197 = lean_string_append(x_195, x_196); -x_198 = lean_expr_dbg_to_string(x_2); -lean_dec(x_2); -x_199 = lean_string_append(x_197, x_198); -lean_dec(x_198); -x_200 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_200, 0, x_199); -lean_ctor_set(x_200, 1, x_3); -return x_200; -} -else +uint8_t x_193; +x_193 = lean_expr_has_level_mvar(x_2); +if (x_193 == 0) { -lean_object* x_201; lean_object* x_202; -lean_dec(x_2); +uint8_t x_194; +x_194 = lean_expr_eqv(x_1, x_2); +if (x_194 == 0) +{ +lean_object* x_195; lean_object* x_196; lean_object* x_197; lean_object* x_198; lean_object* x_199; lean_object* x_200; lean_object* x_201; lean_object* x_202; +x_195 = lean_expr_dbg_to_string(x_1); lean_dec(x_1); -x_201 = lean_box(0); -x_202 = lean_alloc_ctor(0, 2, 0); +x_196 = l_Lean_TypeClass_Context_eUnify___main___closed__1; +x_197 = lean_string_append(x_196, x_195); +lean_dec(x_195); +x_198 = l_Lean_TypeClass_Context_uUnify___main___closed__2; +x_199 = lean_string_append(x_197, x_198); +x_200 = lean_expr_dbg_to_string(x_2); +lean_dec(x_2); +x_201 = lean_string_append(x_199, x_200); +lean_dec(x_200); +x_202 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_202, 0, x_201); lean_ctor_set(x_202, 1, x_3); return x_202; } +else +{ +lean_object* x_203; lean_object* x_204; +lean_dec(x_2); +lean_dec(x_1); +x_203 = lean_box(0); +x_204 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_204, 0, x_203); +lean_ctor_set(x_204, 1, x_3); +return x_204; +} } else { -lean_object* x_203; -x_203 = lean_box(0); -x_4 = x_203; +lean_object* x_205; +x_205 = lean_box(0); +x_4 = x_205; goto block_189; } } else { -lean_object* x_204; -x_204 = lean_box(0); -x_4 = x_204; +lean_object* x_206; +x_206 = lean_box(0); +x_4 = x_206; +goto block_189; +} +} +else +{ +lean_object* x_207; +x_207 = lean_box(0); +x_4 = x_207; +goto block_189; +} +} +else +{ +lean_object* x_208; +x_208 = lean_box(0); +x_4 = x_208; goto block_189; } block_189: @@ -3705,15 +3742,35 @@ return x_13; lean_object* l_Lean_TypeClass_Context_eInstantiate___main(lean_object* x_1, lean_object* x_2) { _start: { -uint8_t x_3; -x_3 = lean_expr_has_mvar(x_2); -if (x_3 == 0) +lean_object* x_3; uint8_t x_34; +x_34 = lean_expr_has_expr_mvar(x_2); +if (x_34 == 0) +{ +uint8_t x_35; +x_35 = lean_expr_has_level_mvar(x_2); +if (x_35 == 0) { lean_dec(x_1); return x_2; } else { +lean_object* x_36; +x_36 = lean_box(0); +x_3 = x_36; +goto block_33; +} +} +else +{ +lean_object* x_37; +x_37 = lean_box(0); +x_3 = x_37; +goto block_33; +} +block_33: +{ +lean_dec(x_3); switch (lean_obj_tag(x_2)) { case 4: { @@ -6518,214 +6575,234 @@ return x_3; lean_object* l_Lean_TypeClass_Context_eAlphaNormalizeCore___main(lean_object* x_1, lean_object* x_2) { _start: { -uint8_t x_3; -x_3 = l_Lean_Expr_isConst(x_1); -if (x_3 == 0) +lean_object* x_3; uint8_t x_62; +x_62 = l_Lean_Expr_isConst(x_1); +if (x_62 == 0) { -uint8_t x_4; -x_4 = l_Lean_Expr_isFVar(x_1); -if (x_4 == 0) +uint8_t x_63; +x_63 = l_Lean_Expr_isFVar(x_1); +if (x_63 == 0) { -uint8_t x_5; -x_5 = lean_expr_has_mvar(x_1); -if (x_5 == 0) +uint8_t x_64; +x_64 = lean_expr_has_expr_mvar(x_1); +if (x_64 == 0) { -lean_object* x_6; -x_6 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_6, 0, x_1); -lean_ctor_set(x_6, 1, x_2); -return x_6; +uint8_t x_65; +x_65 = lean_expr_has_level_mvar(x_1); +if (x_65 == 0) +{ +lean_object* x_66; +x_66 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_66, 0, x_1); +lean_ctor_set(x_66, 1, x_2); +return x_66; } else { +lean_object* x_67; +x_67 = lean_box(0); +x_3 = x_67; +goto block_61; +} +} +else +{ +lean_object* x_68; +x_68 = lean_box(0); +x_3 = x_68; +goto block_61; +} +} +else +{ +lean_object* x_69; +x_69 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_69, 0, x_1); +lean_ctor_set(x_69, 1, x_2); +return x_69; +} +} +else +{ +lean_object* x_70; +x_70 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_70, 0, x_1); +lean_ctor_set(x_70, 1, x_2); +return x_70; +} +block_61: +{ +lean_dec(x_3); switch (lean_obj_tag(x_1)) { case 5: { -lean_object* 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; -x_7 = lean_ctor_get(x_1, 0); -lean_inc(x_7); -x_8 = lean_ctor_get(x_1, 1); -lean_inc(x_8); +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; +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_9 = l_Lean_TypeClass_Context_eAlphaNormalizeCore___main(x_7, x_2); -x_10 = lean_ctor_get(x_9, 0); -lean_inc(x_10); -x_11 = lean_ctor_get(x_9, 1); -lean_inc(x_11); -lean_dec(x_9); -x_12 = l_Lean_TypeClass_Context_eAlphaNormalizeCore___main(x_8, x_11); -x_13 = !lean_is_exclusive(x_12); -if (x_13 == 0) +x_6 = l_Lean_TypeClass_Context_eAlphaNormalizeCore___main(x_4, x_2); +x_7 = lean_ctor_get(x_6, 0); +lean_inc(x_7); +x_8 = lean_ctor_get(x_6, 1); +lean_inc(x_8); +lean_dec(x_6); +x_9 = l_Lean_TypeClass_Context_eAlphaNormalizeCore___main(x_5, x_8); +x_10 = !lean_is_exclusive(x_9); +if (x_10 == 0) { -lean_object* x_14; lean_object* x_15; -x_14 = lean_ctor_get(x_12, 0); -x_15 = lean_expr_mk_app(x_10, x_14); -lean_ctor_set(x_12, 0, x_15); -return x_12; +lean_object* x_11; lean_object* x_12; +x_11 = lean_ctor_get(x_9, 0); +x_12 = lean_expr_mk_app(x_7, x_11); +lean_ctor_set(x_9, 0, x_12); +return x_9; } else { -lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; -x_16 = lean_ctor_get(x_12, 0); -x_17 = lean_ctor_get(x_12, 1); -lean_inc(x_17); -lean_inc(x_16); -lean_dec(x_12); -x_18 = lean_expr_mk_app(x_10, x_16); -x_19 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_19, 0, x_18); -lean_ctor_set(x_19, 1, x_17); -return x_19; +lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; +x_13 = lean_ctor_get(x_9, 0); +x_14 = lean_ctor_get(x_9, 1); +lean_inc(x_14); +lean_inc(x_13); +lean_dec(x_9); +x_15 = lean_expr_mk_app(x_7, x_13); +x_16 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_16, 0, x_15); +lean_ctor_set(x_16, 1, x_14); +return x_16; } } case 7: { -lean_object* x_20; uint8_t x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; uint8_t x_28; -x_20 = lean_ctor_get(x_1, 0); +lean_object* x_17; uint8_t x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25; +x_17 = lean_ctor_get(x_1, 0); +lean_inc(x_17); +x_18 = lean_ctor_get_uint8(x_1, sizeof(void*)*3); +x_19 = lean_ctor_get(x_1, 1); +lean_inc(x_19); +x_20 = lean_ctor_get(x_1, 2); lean_inc(x_20); -x_21 = lean_ctor_get_uint8(x_1, sizeof(void*)*3); -x_22 = lean_ctor_get(x_1, 1); -lean_inc(x_22); -x_23 = lean_ctor_get(x_1, 2); -lean_inc(x_23); lean_dec(x_1); -x_24 = l_Lean_TypeClass_Context_eAlphaNormalizeCore___main(x_22, x_2); -x_25 = lean_ctor_get(x_24, 0); -lean_inc(x_25); -x_26 = lean_ctor_get(x_24, 1); -lean_inc(x_26); -lean_dec(x_24); -x_27 = l_Lean_TypeClass_Context_eAlphaNormalizeCore___main(x_23, x_26); -x_28 = !lean_is_exclusive(x_27); -if (x_28 == 0) +x_21 = l_Lean_TypeClass_Context_eAlphaNormalizeCore___main(x_19, x_2); +x_22 = lean_ctor_get(x_21, 0); +lean_inc(x_22); +x_23 = lean_ctor_get(x_21, 1); +lean_inc(x_23); +lean_dec(x_21); +x_24 = l_Lean_TypeClass_Context_eAlphaNormalizeCore___main(x_20, x_23); +x_25 = !lean_is_exclusive(x_24); +if (x_25 == 0) { -lean_object* x_29; lean_object* x_30; -x_29 = lean_ctor_get(x_27, 0); -x_30 = lean_expr_mk_forall(x_20, x_21, x_25, x_29); -lean_ctor_set(x_27, 0, x_30); -return x_27; +lean_object* x_26; lean_object* x_27; +x_26 = lean_ctor_get(x_24, 0); +x_27 = lean_expr_mk_forall(x_17, x_18, x_22, x_26); +lean_ctor_set(x_24, 0, x_27); +return x_24; } else { -lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; -x_31 = lean_ctor_get(x_27, 0); -x_32 = lean_ctor_get(x_27, 1); -lean_inc(x_32); -lean_inc(x_31); -lean_dec(x_27); -x_33 = lean_expr_mk_forall(x_20, x_21, x_25, x_31); -x_34 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_34, 0, x_33); -lean_ctor_set(x_34, 1, x_32); -return x_34; +lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; +x_28 = lean_ctor_get(x_24, 0); +x_29 = lean_ctor_get(x_24, 1); +lean_inc(x_29); +lean_inc(x_28); +lean_dec(x_24); +x_30 = lean_expr_mk_forall(x_17, x_18, x_22, x_28); +x_31 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_31, 0, x_30); +lean_ctor_set(x_31, 1, x_29); +return x_31; } } default: { -lean_object* x_35; -x_35 = l_Lean_TypeClass_Context_eMetaIdx(x_1); -if (lean_obj_tag(x_35) == 0) +lean_object* x_32; +x_32 = l_Lean_TypeClass_Context_eMetaIdx(x_1); +if (lean_obj_tag(x_32) == 0) { -lean_object* x_36; -x_36 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_36, 0, x_1); -lean_ctor_set(x_36, 1, x_2); -return x_36; +lean_object* x_33; +x_33 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_33, 0, x_1); +lean_ctor_set(x_33, 1, x_2); +return x_33; } else { -lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; +lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_dec(x_1); -x_37 = lean_ctor_get(x_35, 0); -lean_inc(x_37); -lean_dec(x_35); -x_38 = lean_ctor_get(x_2, 0); -lean_inc(x_38); +x_34 = lean_ctor_get(x_32, 0); +lean_inc(x_34); +lean_dec(x_32); +x_35 = lean_ctor_get(x_2, 0); +lean_inc(x_35); +x_36 = lean_ctor_get(x_2, 1); +lean_inc(x_36); +x_37 = l_RBNode_find___main___at_Lean_TypeClass_Context_uAlphaNormalizeCore___main___spec__1(x_35, x_34); +if (lean_obj_tag(x_37) == 0) +{ +uint8_t x_38; +x_38 = !lean_is_exclusive(x_2); +if (x_38 == 0) +{ +lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; x_39 = lean_ctor_get(x_2, 1); -lean_inc(x_39); -x_40 = l_RBNode_find___main___at_Lean_TypeClass_Context_uAlphaNormalizeCore___main___spec__1(x_38, x_37); -if (lean_obj_tag(x_40) == 0) -{ -uint8_t x_41; -x_41 = !lean_is_exclusive(x_2); -if (x_41 == 0) -{ -lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; -x_42 = lean_ctor_get(x_2, 1); -lean_dec(x_42); -x_43 = lean_ctor_get(x_2, 0); -lean_dec(x_43); -x_44 = lean_unsigned_to_nat(0u); -x_45 = l_RBNode_fold___main___at_RBMap_size___spec__1___rarg(x_44, x_38); -x_46 = l_Lean_TypeClass_Context_alphaMetaPrefix; -lean_inc(x_45); -x_47 = lean_name_mk_numeral(x_46, x_45); -x_48 = lean_expr_mk_mvar(x_47); -x_49 = l_RBNode_insert___at_Lean_TypeClass_Context_uAlphaNormalizeCore___main___spec__2(x_38, x_37, x_45); -lean_ctor_set(x_2, 0, x_49); -x_50 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_50, 0, x_48); -lean_ctor_set(x_50, 1, x_2); -return x_50; -} -else -{ -lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; -lean_dec(x_2); -x_51 = lean_unsigned_to_nat(0u); -x_52 = l_RBNode_fold___main___at_RBMap_size___spec__1___rarg(x_51, x_38); -x_53 = l_Lean_TypeClass_Context_alphaMetaPrefix; -lean_inc(x_52); -x_54 = lean_name_mk_numeral(x_53, x_52); -x_55 = lean_expr_mk_mvar(x_54); -x_56 = l_RBNode_insert___at_Lean_TypeClass_Context_uAlphaNormalizeCore___main___spec__2(x_38, x_37, x_52); -x_57 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_57, 0, x_56); -lean_ctor_set(x_57, 1, x_39); -x_58 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_58, 0, x_55); -lean_ctor_set(x_58, 1, x_57); -return x_58; -} -} -else -{ -lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_dec(x_39); -lean_dec(x_38); -lean_dec(x_37); -x_59 = lean_ctor_get(x_40, 0); -lean_inc(x_59); +x_40 = lean_ctor_get(x_2, 0); lean_dec(x_40); -x_60 = l_Lean_TypeClass_Context_alphaMetaPrefix; -x_61 = lean_name_mk_numeral(x_60, x_59); -x_62 = lean_expr_mk_mvar(x_61); -x_63 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_63, 0, x_62); -lean_ctor_set(x_63, 1, x_2); -return x_63; -} -} -} +x_41 = lean_unsigned_to_nat(0u); +x_42 = l_RBNode_fold___main___at_RBMap_size___spec__1___rarg(x_41, x_35); +x_43 = l_Lean_TypeClass_Context_alphaMetaPrefix; +lean_inc(x_42); +x_44 = lean_name_mk_numeral(x_43, x_42); +x_45 = lean_expr_mk_mvar(x_44); +x_46 = l_RBNode_insert___at_Lean_TypeClass_Context_uAlphaNormalizeCore___main___spec__2(x_35, x_34, x_42); +lean_ctor_set(x_2, 0, x_46); +x_47 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_47, 0, x_45); +lean_ctor_set(x_47, 1, x_2); +return x_47; } +else +{ +lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; +lean_dec(x_2); +x_48 = lean_unsigned_to_nat(0u); +x_49 = l_RBNode_fold___main___at_RBMap_size___spec__1___rarg(x_48, x_35); +x_50 = l_Lean_TypeClass_Context_alphaMetaPrefix; +lean_inc(x_49); +x_51 = lean_name_mk_numeral(x_50, x_49); +x_52 = lean_expr_mk_mvar(x_51); +x_53 = l_RBNode_insert___at_Lean_TypeClass_Context_uAlphaNormalizeCore___main___spec__2(x_35, x_34, x_49); +x_54 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_54, 0, x_53); +lean_ctor_set(x_54, 1, x_36); +x_55 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_55, 0, x_52); +lean_ctor_set(x_55, 1, x_54); +return x_55; } } else { -lean_object* x_64; -x_64 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_64, 0, x_1); -lean_ctor_set(x_64, 1, x_2); -return x_64; +lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; +lean_dec(x_36); +lean_dec(x_35); +lean_dec(x_34); +x_56 = lean_ctor_get(x_37, 0); +lean_inc(x_56); +lean_dec(x_37); +x_57 = l_Lean_TypeClass_Context_alphaMetaPrefix; +x_58 = lean_name_mk_numeral(x_57, x_56); +x_59 = lean_expr_mk_mvar(x_58); +x_60 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_60, 0, x_59); +lean_ctor_set(x_60, 1, x_2); +return x_60; +} +} } } -else -{ -lean_object* x_65; -x_65 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_65, 0, x_1); -lean_ctor_set(x_65, 1, x_2); -return x_65; } } } diff --git a/src/stage0/Init/Lean/TypeClass/Synth.c b/src/stage0/Init/Lean/TypeClass/Synth.c index 02cd9a8021..fd5e022abf 100644 --- a/src/stage0/Init/Lean/TypeClass/Synth.c +++ b/src/stage0/Init/Lean/TypeClass/Synth.c @@ -164,7 +164,6 @@ lean_object* l_Array_miterateAux___main___at_Lean_TypeClass_newSubgoal___spec__5 lean_object* l_Lean_Expr_constLevels(lean_object*); lean_object* l_Stack_modify___at_Lean_TypeClass_generate___spec__4(lean_object*, lean_object*); lean_object* l_Lean_TypeClass_introduceMVars___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -uint8_t lean_expr_has_mvar(lean_object*); lean_object* l_Array_miterateAux___main___at_Lean_TypeClass_consume___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Stack_pop___at_Lean_TypeClass_generate___spec__3(lean_object*); lean_object* l_Lean_TypeClass_generate___lambda__1(lean_object*, lean_object*); @@ -175,6 +174,7 @@ lean_object* l_Lean_TypeClass_resume(lean_object*); extern lean_object* l_panicWithPos___rarg___closed__2; lean_object* l_Lean_TypeClass_collectUReplacements___main(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_TypeClass_newAnswer___closed__1; +uint8_t lean_expr_has_expr_mvar(lean_object*); lean_object* l_List_foldl___main___at_Lean_TypeClass_constNameToTypedExpr___spec__1(lean_object*, lean_object*); lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*); lean_object* l_Array_back___at_Lean_TypeClass_consume___spec__2(lean_object*); @@ -194,6 +194,7 @@ extern lean_object* l_Lean_exprIsInhabited___closed__1; lean_object* l_Array_back___at_Lean_TypeClass_generate___spec__2___boxed(lean_object*); lean_object* l_Lean_TypeClass_synth___closed__3; lean_object* l_Lean_TypeClass_constNameToTypedExpr___closed__2; +uint8_t lean_expr_has_level_mvar(lean_object*); uint8_t l_Lean_Expr_isLambda(lean_object*); lean_object* _init_l_Lean_TypeClass_TypedExpr_HasToString___closed__1() { _start: @@ -4326,49 +4327,44 @@ lean_object* l_Lean_TypeClass_preprocessForOutParams(lean_object* x_1, lean_obje _start: { lean_object* x_3; uint8_t x_279; -x_279 = lean_expr_has_mvar(x_2); +x_279 = lean_expr_has_expr_mvar(x_2); if (x_279 == 0) { -lean_object* x_280; uint8_t x_281; -x_280 = l_Lean_Expr_getAppFn___main(x_2); -x_281 = l_Lean_Expr_isConst(x_280); -if (x_281 == 0) +uint8_t x_280; +x_280 = lean_expr_has_level_mvar(x_2); +if (x_280 == 0) { -lean_object* x_282; -lean_dec(x_280); -x_282 = lean_box(0); -x_3 = x_282; +lean_object* x_281; uint8_t x_282; +x_281 = l_Lean_Expr_getAppFn___main(x_2); +x_282 = l_Lean_Expr_isConst(x_281); +if (x_282 == 0) +{ +lean_object* x_283; +lean_dec(x_281); +x_283 = lean_box(0); +x_3 = x_283; goto block_278; } else { -lean_object* x_283; uint8_t x_284; -x_283 = l_Lean_Expr_constName(x_280); -lean_dec(x_280); +lean_object* x_284; uint8_t x_285; +x_284 = l_Lean_Expr_constName(x_281); +lean_dec(x_281); lean_inc(x_1); -x_284 = lean_has_out_params(x_1, x_283); -if (x_284 == 0) +x_285 = lean_has_out_params(x_1, x_284); +if (x_285 == 0) { -lean_object* x_285; lean_object* x_286; lean_object* x_287; lean_object* x_288; +lean_object* x_286; lean_object* x_287; lean_object* x_288; lean_object* x_289; lean_dec(x_1); -x_285 = l_panicWithPos___at_Lean_TypeClass_collectEReplacements___main___spec__1___closed__1; -x_286 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_286, 0, x_2); -lean_ctor_set(x_286, 1, x_285); -x_287 = l_Lean_TypeClass_Context_Inhabited___closed__1; -x_288 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_288, 0, x_287); -lean_ctor_set(x_288, 1, x_286); -return x_288; -} -else -{ -lean_object* x_289; -x_289 = lean_box(0); -x_3 = x_289; -goto block_278; -} -} +x_286 = l_panicWithPos___at_Lean_TypeClass_collectEReplacements___main___spec__1___closed__1; +x_287 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_287, 0, x_2); +lean_ctor_set(x_287, 1, x_286); +x_288 = l_Lean_TypeClass_Context_Inhabited___closed__1; +x_289 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_289, 0, x_288); +lean_ctor_set(x_289, 1, x_287); +return x_289; } else { @@ -4377,6 +4373,23 @@ x_290 = lean_box(0); x_3 = x_290; goto block_278; } +} +} +else +{ +lean_object* x_291; +x_291 = lean_box(0); +x_3 = x_291; +goto block_278; +} +} +else +{ +lean_object* x_292; +x_292 = lean_box(0); +x_3 = x_292; +goto block_278; +} block_278: { lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; diff --git a/src/stage0/Init/Lean/TypeContext.c b/src/stage0/Init/Lean/TypeContext.c index f6a2377a23..d6c567f976 100644 --- a/src/stage0/Init/Lean/TypeContext.c +++ b/src/stage0/Init/Lean/TypeContext.c @@ -1,6 +1,6 @@ // Lean compiler output // Module: Init.Lean.TypeContext -// Imports: Init.Lean.Expr +// Imports: Init.Control.Reader Init.Lean.NameGenerator Init.Lean.Environment Init.Lean.LocalContext Init.Lean.Trace #include "runtime/lean.h" #if defined(__clang__) #pragma clang diagnostic ignored "-Wunused-parameter" @@ -13,15 +13,1470 @@ #ifdef __cplusplus extern "C" { #endif -lean_object* initialize_Init_Lean_Expr(lean_object*); +lean_object* l_Lean_TypeContext_hasAssignedLevelMVar___main___rarg___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l___private_Init_Lean_TypeContext_1__getOptions(lean_object*, lean_object*); +lean_object* l_Lean_TypeContext_hasAssignedLevelMVar___rarg___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_TypeContext_tracer___closed__2; +uint8_t l_Lean_TypeContext_isLevelAssigned___rarg(lean_object*, lean_object*, lean_object*); +uint8_t l_Lean_TypeContext_hasAssignedLevelMVar___main___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_TypeContext_isLevelAssigned(lean_object*); +lean_object* l_Lean_TypeContext_tracer(lean_object*, lean_object*); +uint8_t l_Lean_Level_hasMVar___main(lean_object*); +lean_object* l_Lean_TCState_backtrackable___lambda__2(lean_object*, lean_object*); +lean_object* l_Lean_TCState_backtrackable___lambda__1___boxed(lean_object*); +uint8_t l_Lean_TypeContext_hasAssignedMVar___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l___private_Init_Lean_TypeContext_2__getTraceState(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_TypeContext_hasAssignedMVar___main(lean_object*); +lean_object* l_Lean_TypeContext_hasAssignedMVar___main___rarg___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l___private_Init_Lean_TypeContext_2__getTraceState___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_TypeContext_hasAssignedLevelMVar(lean_object*); +lean_object* l___private_Init_Lean_TypeContext_1__getOptions___rarg___boxed(lean_object*, lean_object*); +lean_object* l_Lean_TCState_backtrackable___closed__3; +lean_object* l_Lean_TypeContext_isLevelAssigned___rarg___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_TCState_backtrackable___lambda__1(lean_object*); +uint8_t l_List_foldr___main___at_Lean_TypeContext_hasAssignedMVar___main___spec__1___rarg(lean_object*, lean_object*, uint8_t, lean_object*); +lean_object* l___private_Init_Lean_TypeContext_1__getOptions___rarg(lean_object*, lean_object*); +lean_object* l_Lean_TypeContext_tracer___lambda__1___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_TCState_backtrackable___closed__2; +lean_object* l_List_foldr___main___at_Lean_TypeContext_hasAssignedMVar___main___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_TypeContext_tracer___lambda__1(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_TypeContext_hasAssignedMVar(lean_object*); +lean_object* l_Lean_TypeContext_tracer___closed__4; +lean_object* l_Lean_TypeContext_hasAssignedMVar___rarg___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_List_foldr___main___at_Lean_TypeContext_hasAssignedMVar___main___spec__1(lean_object*); +lean_object* l_Lean_TypeContext_isExprAssigned___rarg___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_TypeContext_tracer___closed__1; +lean_object* l_Lean_TCState_backtrackable___closed__1; +lean_object* l_Lean_TCState_backtrackable(lean_object*, lean_object*); +lean_object* l___private_Init_Lean_TypeContext_2__getTraceState___rarg(lean_object*); +uint8_t l_Lean_TypeContext_hasAssignedLevelMVar___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_TypeContext_hasAssignedLevelMVar___main(lean_object*); +uint8_t lean_expr_has_expr_mvar(lean_object*); +lean_object* l_Lean_TypeContext_tracer___closed__3; +lean_object* l_Lean_TypeContext_isExprAssigned(lean_object*); +uint8_t l_Lean_TypeContext_isExprAssigned___rarg(lean_object*, lean_object*, lean_object*); +uint8_t l_Lean_TypeContext_hasAssignedMVar___main___rarg(lean_object*, lean_object*, lean_object*); +uint8_t lean_expr_has_level_mvar(lean_object*); +lean_object* l_Lean_TCState_backtrackable___lambda__1(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +return x_2; +} +} +lean_object* l_Lean_TCState_backtrackable___lambda__2(lean_object* x_1, lean_object* x_2) { +_start: +{ +uint8_t x_3; +x_3 = !lean_is_exclusive(x_1); +if (x_3 == 0) +{ +lean_object* x_4; +x_4 = lean_ctor_get(x_1, 0); +lean_dec(x_4); +lean_ctor_set(x_1, 0, x_2); +return x_1; +} +else +{ +lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9; lean_object* x_10; +x_5 = lean_ctor_get(x_1, 1); +x_6 = lean_ctor_get(x_1, 2); +x_7 = lean_ctor_get(x_1, 3); +x_8 = lean_ctor_get_uint8(x_1, sizeof(void*)*5); +x_9 = lean_ctor_get(x_1, 4); +lean_inc(x_9); +lean_inc(x_7); +lean_inc(x_6); +lean_inc(x_5); +lean_dec(x_1); +x_10 = lean_alloc_ctor(0, 5, 1); +lean_ctor_set(x_10, 0, x_2); +lean_ctor_set(x_10, 1, x_5); +lean_ctor_set(x_10, 2, x_6); +lean_ctor_set(x_10, 3, x_7); +lean_ctor_set(x_10, 4, x_9); +lean_ctor_set_uint8(x_10, sizeof(void*)*5, x_8); +return x_10; +} +} +} +lean_object* _init_l_Lean_TCState_backtrackable___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_TCState_backtrackable___lambda__1___boxed), 1, 0); +return x_1; +} +} +lean_object* _init_l_Lean_TCState_backtrackable___closed__2() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_TCState_backtrackable___lambda__2), 2, 0); +return x_1; +} +} +lean_object* _init_l_Lean_TCState_backtrackable___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_TCState_backtrackable___closed__1; +x_2 = l_Lean_TCState_backtrackable___closed__2; +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* l_Lean_TCState_backtrackable(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l_Lean_TCState_backtrackable___closed__3; +return x_3; +} +} +lean_object* l_Lean_TCState_backtrackable___lambda__1___boxed(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = l_Lean_TCState_backtrackable___lambda__1(x_1); +lean_dec(x_1); +return x_2; +} +} +uint8_t l_Lean_TypeContext_isLevelAssigned___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; lean_object* x_5; +x_4 = lean_ctor_get(x_1, 1); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_2(x_4, x_2, x_3); +if (lean_obj_tag(x_5) == 0) +{ +uint8_t x_6; +x_6 = 0; +return x_6; +} +else +{ +uint8_t x_7; +lean_dec(x_5); +x_7 = 1; +return x_7; +} +} +} +lean_object* l_Lean_TypeContext_isLevelAssigned(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l_Lean_TypeContext_isLevelAssigned___rarg___boxed), 3, 0); +return x_2; +} +} +lean_object* l_Lean_TypeContext_isLevelAssigned___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint8_t x_4; lean_object* x_5; +x_4 = l_Lean_TypeContext_isLevelAssigned___rarg(x_1, x_2, x_3); +x_5 = lean_box(x_4); +return x_5; +} +} +uint8_t l_Lean_TypeContext_isExprAssigned___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; lean_object* x_5; +x_4 = lean_ctor_get(x_1, 4); +lean_inc(x_4); +lean_dec(x_1); +x_5 = lean_apply_2(x_4, x_2, x_3); +if (lean_obj_tag(x_5) == 0) +{ +uint8_t x_6; +x_6 = 0; +return x_6; +} +else +{ +uint8_t x_7; +lean_dec(x_5); +x_7 = 1; +return x_7; +} +} +} +lean_object* l_Lean_TypeContext_isExprAssigned(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l_Lean_TypeContext_isExprAssigned___rarg___boxed), 3, 0); +return x_2; +} +} +lean_object* l_Lean_TypeContext_isExprAssigned___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint8_t x_4; lean_object* x_5; +x_4 = l_Lean_TypeContext_isExprAssigned___rarg(x_1, x_2, x_3); +x_5 = lean_box(x_4); +return x_5; +} +} +uint8_t l_Lean_TypeContext_hasAssignedLevelMVar___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +switch (lean_obj_tag(x_3)) { +case 1: +{ +lean_object* x_4; uint8_t x_5; +x_4 = lean_ctor_get(x_3, 0); +lean_inc(x_4); +lean_dec(x_3); +x_5 = l_Lean_Level_hasMVar___main(x_4); +if (x_5 == 0) +{ +uint8_t x_6; +lean_dec(x_4); +lean_dec(x_2); +lean_dec(x_1); +x_6 = 0; +return x_6; +} +else +{ +x_3 = x_4; +goto _start; +} +} +case 2: +{ +lean_object* x_8; lean_object* x_9; uint8_t x_10; +x_8 = lean_ctor_get(x_3, 0); +lean_inc(x_8); +x_9 = lean_ctor_get(x_3, 1); +lean_inc(x_9); +lean_dec(x_3); +x_10 = l_Lean_Level_hasMVar___main(x_8); +if (x_10 == 0) +{ +uint8_t x_11; +lean_dec(x_8); +x_11 = l_Lean_Level_hasMVar___main(x_9); +if (x_11 == 0) +{ +uint8_t x_12; +lean_dec(x_9); +lean_dec(x_2); +lean_dec(x_1); +x_12 = 0; +return x_12; +} +else +{ +x_3 = x_9; +goto _start; +} +} +else +{ +uint8_t x_14; +lean_inc(x_2); +lean_inc(x_1); +x_14 = l_Lean_TypeContext_hasAssignedLevelMVar___main___rarg(x_1, x_2, x_8); +if (x_14 == 0) +{ +uint8_t x_15; +x_15 = l_Lean_Level_hasMVar___main(x_9); +if (x_15 == 0) +{ +lean_dec(x_9); +lean_dec(x_2); +lean_dec(x_1); +return x_14; +} +else +{ +x_3 = x_9; +goto _start; +} +} +else +{ +uint8_t x_17; +lean_dec(x_9); +lean_dec(x_2); +lean_dec(x_1); +x_17 = 1; +return x_17; +} +} +} +case 3: +{ +lean_object* x_18; lean_object* x_19; uint8_t x_20; +x_18 = lean_ctor_get(x_3, 0); +lean_inc(x_18); +x_19 = lean_ctor_get(x_3, 1); +lean_inc(x_19); +lean_dec(x_3); +x_20 = l_Lean_Level_hasMVar___main(x_18); +if (x_20 == 0) +{ +uint8_t x_21; +lean_dec(x_18); +x_21 = l_Lean_Level_hasMVar___main(x_19); +if (x_21 == 0) +{ +uint8_t x_22; +lean_dec(x_19); +lean_dec(x_2); +lean_dec(x_1); +x_22 = 0; +return x_22; +} +else +{ +x_3 = x_19; +goto _start; +} +} +else +{ +uint8_t x_24; +lean_inc(x_2); +lean_inc(x_1); +x_24 = l_Lean_TypeContext_hasAssignedLevelMVar___main___rarg(x_1, x_2, x_18); +if (x_24 == 0) +{ +uint8_t x_25; +x_25 = l_Lean_Level_hasMVar___main(x_19); +if (x_25 == 0) +{ +lean_dec(x_19); +lean_dec(x_2); +lean_dec(x_1); +return x_24; +} +else +{ +x_3 = x_19; +goto _start; +} +} +else +{ +uint8_t x_27; +lean_dec(x_19); +lean_dec(x_2); +lean_dec(x_1); +x_27 = 1; +return x_27; +} +} +} +case 5: +{ +lean_object* x_28; lean_object* x_29; lean_object* x_30; +x_28 = lean_ctor_get(x_3, 0); +lean_inc(x_28); +lean_dec(x_3); +x_29 = lean_ctor_get(x_1, 1); +lean_inc(x_29); +lean_dec(x_1); +x_30 = lean_apply_2(x_29, x_2, x_28); +if (lean_obj_tag(x_30) == 0) +{ +uint8_t x_31; +x_31 = 0; +return x_31; +} +else +{ +uint8_t x_32; +lean_dec(x_30); +x_32 = 1; +return x_32; +} +} +default: +{ +uint8_t x_33; +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_33 = 0; +return x_33; +} +} +} +} +lean_object* l_Lean_TypeContext_hasAssignedLevelMVar___main(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l_Lean_TypeContext_hasAssignedLevelMVar___main___rarg___boxed), 3, 0); +return x_2; +} +} +lean_object* l_Lean_TypeContext_hasAssignedLevelMVar___main___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint8_t x_4; lean_object* x_5; +x_4 = l_Lean_TypeContext_hasAssignedLevelMVar___main___rarg(x_1, x_2, x_3); +x_5 = lean_box(x_4); +return x_5; +} +} +uint8_t l_Lean_TypeContext_hasAssignedLevelMVar___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint8_t x_4; +x_4 = l_Lean_TypeContext_hasAssignedLevelMVar___main___rarg(x_1, x_2, x_3); +return x_4; +} +} +lean_object* l_Lean_TypeContext_hasAssignedLevelMVar(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l_Lean_TypeContext_hasAssignedLevelMVar___rarg___boxed), 3, 0); +return x_2; +} +} +lean_object* l_Lean_TypeContext_hasAssignedLevelMVar___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint8_t x_4; lean_object* x_5; +x_4 = l_Lean_TypeContext_hasAssignedLevelMVar___rarg(x_1, x_2, x_3); +x_5 = lean_box(x_4); +return x_5; +} +} +uint8_t l_List_foldr___main___at_Lean_TypeContext_hasAssignedMVar___main___spec__1___rarg(lean_object* x_1, lean_object* x_2, uint8_t x_3, lean_object* x_4) { +_start: +{ +if (lean_obj_tag(x_4) == 0) +{ +lean_dec(x_2); +lean_dec(x_1); +return x_3; +} +else +{ +lean_object* x_5; lean_object* x_6; uint8_t x_7; uint8_t x_8; +x_5 = lean_ctor_get(x_4, 0); +lean_inc(x_5); +x_6 = lean_ctor_get(x_4, 1); +lean_inc(x_6); +lean_dec(x_4); +lean_inc(x_2); +lean_inc(x_1); +x_7 = l_List_foldr___main___at_Lean_TypeContext_hasAssignedMVar___main___spec__1___rarg(x_1, x_2, x_3, x_6); +x_8 = l_Lean_TypeContext_hasAssignedLevelMVar___main___rarg(x_1, x_2, x_5); +if (x_8 == 0) +{ +return x_7; +} +else +{ +uint8_t x_9; +x_9 = 1; +return x_9; +} +} +} +} +lean_object* l_List_foldr___main___at_Lean_TypeContext_hasAssignedMVar___main___spec__1(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l_List_foldr___main___at_Lean_TypeContext_hasAssignedMVar___main___spec__1___rarg___boxed), 4, 0); +return x_2; +} +} +uint8_t l_Lean_TypeContext_hasAssignedMVar___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +switch (lean_obj_tag(x_3)) { +case 2: +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_4 = lean_ctor_get(x_3, 0); +lean_inc(x_4); +lean_dec(x_3); +x_5 = lean_ctor_get(x_1, 4); +lean_inc(x_5); +lean_dec(x_1); +x_6 = lean_apply_2(x_5, x_2, x_4); +if (lean_obj_tag(x_6) == 0) +{ +uint8_t x_7; +x_7 = 0; +return x_7; +} +else +{ +uint8_t x_8; +lean_dec(x_6); +x_8 = 1; +return x_8; +} +} +case 3: +{ +lean_object* x_9; uint8_t x_10; +x_9 = lean_ctor_get(x_3, 0); +lean_inc(x_9); +lean_dec(x_3); +x_10 = l_Lean_TypeContext_hasAssignedLevelMVar___main___rarg(x_1, x_2, x_9); +return x_10; +} +case 4: +{ +lean_object* x_11; uint8_t x_12; uint8_t x_13; +x_11 = lean_ctor_get(x_3, 1); +lean_inc(x_11); +lean_dec(x_3); +x_12 = 0; +x_13 = l_List_foldr___main___at_Lean_TypeContext_hasAssignedMVar___main___spec__1___rarg(x_1, x_2, x_12, x_11); +return x_13; +} +case 5: +{ +lean_object* x_14; lean_object* x_15; uint8_t x_16; +x_14 = lean_ctor_get(x_3, 0); +lean_inc(x_14); +x_15 = lean_ctor_get(x_3, 1); +lean_inc(x_15); +lean_dec(x_3); +x_16 = lean_expr_has_expr_mvar(x_14); +if (x_16 == 0) +{ +uint8_t x_17; +x_17 = lean_expr_has_level_mvar(x_14); +if (x_17 == 0) +{ +uint8_t x_18; +lean_dec(x_14); +x_18 = lean_expr_has_expr_mvar(x_15); +if (x_18 == 0) +{ +uint8_t x_19; +x_19 = lean_expr_has_level_mvar(x_15); +if (x_19 == 0) +{ +uint8_t x_20; +lean_dec(x_15); +lean_dec(x_2); +lean_dec(x_1); +x_20 = 0; +return x_20; +} +else +{ +x_3 = x_15; +goto _start; +} +} +else +{ +x_3 = x_15; +goto _start; +} +} +else +{ +uint8_t x_23; +lean_inc(x_2); +lean_inc(x_1); +x_23 = l_Lean_TypeContext_hasAssignedMVar___main___rarg(x_1, x_2, x_14); +if (x_23 == 0) +{ +uint8_t x_24; +x_24 = lean_expr_has_expr_mvar(x_15); +if (x_24 == 0) +{ +uint8_t x_25; +x_25 = lean_expr_has_level_mvar(x_15); +if (x_25 == 0) +{ +lean_dec(x_15); +lean_dec(x_2); +lean_dec(x_1); +return x_23; +} +else +{ +x_3 = x_15; +goto _start; +} +} +else +{ +x_3 = x_15; +goto _start; +} +} +else +{ +uint8_t x_28; +lean_dec(x_15); +lean_dec(x_2); +lean_dec(x_1); +x_28 = 1; +return x_28; +} +} +} +else +{ +uint8_t x_29; +lean_inc(x_2); +lean_inc(x_1); +x_29 = l_Lean_TypeContext_hasAssignedMVar___main___rarg(x_1, x_2, x_14); +if (x_29 == 0) +{ +uint8_t x_30; +x_30 = lean_expr_has_expr_mvar(x_15); +if (x_30 == 0) +{ +uint8_t x_31; +x_31 = lean_expr_has_level_mvar(x_15); +if (x_31 == 0) +{ +lean_dec(x_15); +lean_dec(x_2); +lean_dec(x_1); +return x_29; +} +else +{ +x_3 = x_15; +goto _start; +} +} +else +{ +x_3 = x_15; +goto _start; +} +} +else +{ +uint8_t x_34; +lean_dec(x_15); +lean_dec(x_2); +lean_dec(x_1); +x_34 = 1; +return x_34; +} +} +} +case 6: +{ +lean_object* x_35; lean_object* x_36; uint8_t x_37; +x_35 = lean_ctor_get(x_3, 1); +lean_inc(x_35); +x_36 = lean_ctor_get(x_3, 2); +lean_inc(x_36); +lean_dec(x_3); +x_37 = lean_expr_has_expr_mvar(x_35); +if (x_37 == 0) +{ +uint8_t x_38; +x_38 = lean_expr_has_level_mvar(x_35); +if (x_38 == 0) +{ +uint8_t x_39; +lean_dec(x_35); +x_39 = lean_expr_has_expr_mvar(x_36); +if (x_39 == 0) +{ +uint8_t x_40; +x_40 = lean_expr_has_level_mvar(x_36); +if (x_40 == 0) +{ +uint8_t x_41; +lean_dec(x_36); +lean_dec(x_2); +lean_dec(x_1); +x_41 = 0; +return x_41; +} +else +{ +x_3 = x_36; +goto _start; +} +} +else +{ +x_3 = x_36; +goto _start; +} +} +else +{ +uint8_t x_44; +lean_inc(x_2); +lean_inc(x_1); +x_44 = l_Lean_TypeContext_hasAssignedMVar___main___rarg(x_1, x_2, x_35); +if (x_44 == 0) +{ +uint8_t x_45; +x_45 = lean_expr_has_expr_mvar(x_36); +if (x_45 == 0) +{ +uint8_t x_46; +x_46 = lean_expr_has_level_mvar(x_36); +if (x_46 == 0) +{ +lean_dec(x_36); +lean_dec(x_2); +lean_dec(x_1); +return x_44; +} +else +{ +x_3 = x_36; +goto _start; +} +} +else +{ +x_3 = x_36; +goto _start; +} +} +else +{ +uint8_t x_49; +lean_dec(x_36); +lean_dec(x_2); +lean_dec(x_1); +x_49 = 1; +return x_49; +} +} +} +else +{ +uint8_t x_50; +lean_inc(x_2); +lean_inc(x_1); +x_50 = l_Lean_TypeContext_hasAssignedMVar___main___rarg(x_1, x_2, x_35); +if (x_50 == 0) +{ +uint8_t x_51; +x_51 = lean_expr_has_expr_mvar(x_36); +if (x_51 == 0) +{ +uint8_t x_52; +x_52 = lean_expr_has_level_mvar(x_36); +if (x_52 == 0) +{ +lean_dec(x_36); +lean_dec(x_2); +lean_dec(x_1); +return x_50; +} +else +{ +x_3 = x_36; +goto _start; +} +} +else +{ +x_3 = x_36; +goto _start; +} +} +else +{ +uint8_t x_55; +lean_dec(x_36); +lean_dec(x_2); +lean_dec(x_1); +x_55 = 1; +return x_55; +} +} +} +case 7: +{ +lean_object* x_56; lean_object* x_57; uint8_t x_58; +x_56 = lean_ctor_get(x_3, 1); +lean_inc(x_56); +x_57 = lean_ctor_get(x_3, 2); +lean_inc(x_57); +lean_dec(x_3); +x_58 = lean_expr_has_expr_mvar(x_56); +if (x_58 == 0) +{ +uint8_t x_59; +x_59 = lean_expr_has_level_mvar(x_56); +if (x_59 == 0) +{ +uint8_t x_60; +lean_dec(x_56); +x_60 = lean_expr_has_expr_mvar(x_57); +if (x_60 == 0) +{ +uint8_t x_61; +x_61 = lean_expr_has_level_mvar(x_57); +if (x_61 == 0) +{ +uint8_t x_62; +lean_dec(x_57); +lean_dec(x_2); +lean_dec(x_1); +x_62 = 0; +return x_62; +} +else +{ +x_3 = x_57; +goto _start; +} +} +else +{ +x_3 = x_57; +goto _start; +} +} +else +{ +uint8_t x_65; +lean_inc(x_2); +lean_inc(x_1); +x_65 = l_Lean_TypeContext_hasAssignedMVar___main___rarg(x_1, x_2, x_56); +if (x_65 == 0) +{ +uint8_t x_66; +x_66 = lean_expr_has_expr_mvar(x_57); +if (x_66 == 0) +{ +uint8_t x_67; +x_67 = lean_expr_has_level_mvar(x_57); +if (x_67 == 0) +{ +lean_dec(x_57); +lean_dec(x_2); +lean_dec(x_1); +return x_65; +} +else +{ +x_3 = x_57; +goto _start; +} +} +else +{ +x_3 = x_57; +goto _start; +} +} +else +{ +uint8_t x_70; +lean_dec(x_57); +lean_dec(x_2); +lean_dec(x_1); +x_70 = 1; +return x_70; +} +} +} +else +{ +uint8_t x_71; +lean_inc(x_2); +lean_inc(x_1); +x_71 = l_Lean_TypeContext_hasAssignedMVar___main___rarg(x_1, x_2, x_56); +if (x_71 == 0) +{ +uint8_t x_72; +x_72 = lean_expr_has_expr_mvar(x_57); +if (x_72 == 0) +{ +uint8_t x_73; +x_73 = lean_expr_has_level_mvar(x_57); +if (x_73 == 0) +{ +lean_dec(x_57); +lean_dec(x_2); +lean_dec(x_1); +return x_71; +} +else +{ +x_3 = x_57; +goto _start; +} +} +else +{ +x_3 = x_57; +goto _start; +} +} +else +{ +uint8_t x_76; +lean_dec(x_57); +lean_dec(x_2); +lean_dec(x_1); +x_76 = 1; +return x_76; +} +} +} +case 8: +{ +lean_object* x_77; lean_object* x_78; lean_object* x_79; uint8_t x_80; uint8_t x_101; +x_77 = lean_ctor_get(x_3, 1); +lean_inc(x_77); +x_78 = lean_ctor_get(x_3, 2); +lean_inc(x_78); +x_79 = lean_ctor_get(x_3, 3); +lean_inc(x_79); +lean_dec(x_3); +x_101 = lean_expr_has_expr_mvar(x_77); +if (x_101 == 0) +{ +uint8_t x_102; +x_102 = lean_expr_has_level_mvar(x_77); +if (x_102 == 0) +{ +uint8_t x_103; +lean_dec(x_77); +x_103 = 0; +x_80 = x_103; +goto block_100; +} +else +{ +uint8_t x_104; +lean_inc(x_2); +lean_inc(x_1); +x_104 = l_Lean_TypeContext_hasAssignedMVar___main___rarg(x_1, x_2, x_77); +if (x_104 == 0) +{ +x_80 = x_104; +goto block_100; +} +else +{ +uint8_t x_105; +lean_dec(x_79); +lean_dec(x_78); +lean_dec(x_2); +lean_dec(x_1); +x_105 = 1; +return x_105; +} +} +} +else +{ +uint8_t x_106; +lean_inc(x_2); +lean_inc(x_1); +x_106 = l_Lean_TypeContext_hasAssignedMVar___main___rarg(x_1, x_2, x_77); +if (x_106 == 0) +{ +x_80 = x_106; +goto block_100; +} +else +{ +uint8_t x_107; +lean_dec(x_79); +lean_dec(x_78); +lean_dec(x_2); +lean_dec(x_1); +x_107 = 1; +return x_107; +} +} +block_100: +{ +uint8_t x_81; +x_81 = lean_expr_has_expr_mvar(x_78); +if (x_81 == 0) +{ +uint8_t x_82; +x_82 = lean_expr_has_level_mvar(x_78); +if (x_82 == 0) +{ +lean_dec(x_78); +if (x_80 == 0) +{ +uint8_t x_83; +x_83 = lean_expr_has_expr_mvar(x_79); +if (x_83 == 0) +{ +uint8_t x_84; +x_84 = lean_expr_has_level_mvar(x_79); +if (x_84 == 0) +{ +lean_dec(x_79); +lean_dec(x_2); +lean_dec(x_1); +return x_80; +} +else +{ +x_3 = x_79; +goto _start; +} +} +else +{ +x_3 = x_79; +goto _start; +} +} +else +{ +uint8_t x_87; +lean_dec(x_79); +lean_dec(x_2); +lean_dec(x_1); +x_87 = 1; +return x_87; +} +} +else +{ +uint8_t x_88; +lean_inc(x_2); +lean_inc(x_1); +x_88 = l_Lean_TypeContext_hasAssignedMVar___main___rarg(x_1, x_2, x_78); +if (x_88 == 0) +{ +uint8_t x_89; +x_89 = lean_expr_has_expr_mvar(x_79); +if (x_89 == 0) +{ +uint8_t x_90; +x_90 = lean_expr_has_level_mvar(x_79); +if (x_90 == 0) +{ +lean_dec(x_79); +lean_dec(x_2); +lean_dec(x_1); +return x_88; +} +else +{ +x_3 = x_79; +goto _start; +} +} +else +{ +x_3 = x_79; +goto _start; +} +} +else +{ +uint8_t x_93; +lean_dec(x_79); +lean_dec(x_2); +lean_dec(x_1); +x_93 = 1; +return x_93; +} +} +} +else +{ +uint8_t x_94; +lean_inc(x_2); +lean_inc(x_1); +x_94 = l_Lean_TypeContext_hasAssignedMVar___main___rarg(x_1, x_2, x_78); +if (x_94 == 0) +{ +uint8_t x_95; +x_95 = lean_expr_has_expr_mvar(x_79); +if (x_95 == 0) +{ +uint8_t x_96; +x_96 = lean_expr_has_level_mvar(x_79); +if (x_96 == 0) +{ +lean_dec(x_79); +lean_dec(x_2); +lean_dec(x_1); +return x_94; +} +else +{ +x_3 = x_79; +goto _start; +} +} +else +{ +x_3 = x_79; +goto _start; +} +} +else +{ +uint8_t x_99; +lean_dec(x_79); +lean_dec(x_2); +lean_dec(x_1); +x_99 = 1; +return x_99; +} +} +} +} +case 10: +{ +lean_object* x_108; uint8_t x_109; +x_108 = lean_ctor_get(x_3, 1); +lean_inc(x_108); +lean_dec(x_3); +x_109 = lean_expr_has_expr_mvar(x_108); +if (x_109 == 0) +{ +uint8_t x_110; +x_110 = lean_expr_has_level_mvar(x_108); +if (x_110 == 0) +{ +uint8_t x_111; +lean_dec(x_108); +lean_dec(x_2); +lean_dec(x_1); +x_111 = 0; +return x_111; +} +else +{ +x_3 = x_108; +goto _start; +} +} +else +{ +x_3 = x_108; +goto _start; +} +} +case 11: +{ +lean_object* x_114; uint8_t x_115; +x_114 = lean_ctor_get(x_3, 2); +lean_inc(x_114); +lean_dec(x_3); +x_115 = lean_expr_has_expr_mvar(x_114); +if (x_115 == 0) +{ +uint8_t x_116; +x_116 = lean_expr_has_level_mvar(x_114); +if (x_116 == 0) +{ +uint8_t x_117; +lean_dec(x_114); +lean_dec(x_2); +lean_dec(x_1); +x_117 = 0; +return x_117; +} +else +{ +x_3 = x_114; +goto _start; +} +} +else +{ +x_3 = x_114; +goto _start; +} +} +default: +{ +uint8_t x_120; +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_120 = 0; +return x_120; +} +} +} +} +lean_object* l_Lean_TypeContext_hasAssignedMVar___main(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l_Lean_TypeContext_hasAssignedMVar___main___rarg___boxed), 3, 0); +return x_2; +} +} +lean_object* l_List_foldr___main___at_Lean_TypeContext_hasAssignedMVar___main___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +uint8_t x_5; uint8_t x_6; lean_object* x_7; +x_5 = lean_unbox(x_3); +lean_dec(x_3); +x_6 = l_List_foldr___main___at_Lean_TypeContext_hasAssignedMVar___main___spec__1___rarg(x_1, x_2, x_5, x_4); +x_7 = lean_box(x_6); +return x_7; +} +} +lean_object* l_Lean_TypeContext_hasAssignedMVar___main___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint8_t x_4; lean_object* x_5; +x_4 = l_Lean_TypeContext_hasAssignedMVar___main___rarg(x_1, x_2, x_3); +x_5 = lean_box(x_4); +return x_5; +} +} +uint8_t l_Lean_TypeContext_hasAssignedMVar___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint8_t x_4; +x_4 = l_Lean_TypeContext_hasAssignedMVar___main___rarg(x_1, x_2, x_3); +return x_4; +} +} +lean_object* l_Lean_TypeContext_hasAssignedMVar(lean_object* x_1) { +_start: +{ +lean_object* x_2; +x_2 = lean_alloc_closure((void*)(l_Lean_TypeContext_hasAssignedMVar___rarg___boxed), 3, 0); +return x_2; +} +} +lean_object* l_Lean_TypeContext_hasAssignedMVar___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint8_t x_4; lean_object* x_5; +x_4 = l_Lean_TypeContext_hasAssignedMVar___rarg(x_1, x_2, x_3); +x_5 = lean_box(x_4); +return x_5; +} +} +lean_object* l___private_Init_Lean_TypeContext_1__getOptions___rarg(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_3 = lean_ctor_get(x_1, 3); +x_4 = lean_ctor_get(x_3, 0); +lean_inc(x_4); +x_5 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_5, 0, x_4); +lean_ctor_set(x_5, 1, x_2); +return x_5; +} +} +lean_object* l___private_Init_Lean_TypeContext_1__getOptions(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = lean_alloc_closure((void*)(l___private_Init_Lean_TypeContext_1__getOptions___rarg___boxed), 2, 0); +return x_3; +} +} +lean_object* l___private_Init_Lean_TypeContext_1__getOptions___rarg___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l___private_Init_Lean_TypeContext_1__getOptions___rarg(x_1, x_2); +lean_dec(x_1); +return x_3; +} +} +lean_object* l___private_Init_Lean_TypeContext_2__getTraceState___rarg(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; +x_2 = lean_ctor_get(x_1, 3); +lean_inc(x_2); +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_2); +lean_ctor_set(x_3, 1, x_1); +return x_3; +} +} +lean_object* l___private_Init_Lean_TypeContext_2__getTraceState(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = lean_alloc_closure((void*)(l___private_Init_Lean_TypeContext_2__getTraceState___rarg), 1, 0); +return x_4; +} +} +lean_object* l___private_Init_Lean_TypeContext_2__getTraceState___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l___private_Init_Lean_TypeContext_2__getTraceState(x_1, x_2, x_3); +lean_dec(x_3); +return x_4; +} +} +lean_object* l_Lean_TypeContext_tracer___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint8_t x_4; +x_4 = !lean_is_exclusive(x_3); +if (x_4 == 0) +{ +lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; +x_5 = lean_ctor_get(x_3, 3); +x_6 = lean_apply_1(x_1, x_5); +lean_ctor_set(x_3, 3, x_6); +x_7 = lean_box(0); +x_8 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_8, 0, x_7); +lean_ctor_set(x_8, 1, x_3); +return x_8; +} +else +{ +lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; +x_9 = lean_ctor_get(x_3, 0); +x_10 = lean_ctor_get(x_3, 1); +x_11 = lean_ctor_get(x_3, 2); +x_12 = lean_ctor_get(x_3, 3); +x_13 = lean_ctor_get_uint8(x_3, sizeof(void*)*5); +x_14 = lean_ctor_get(x_3, 4); +lean_inc(x_14); +lean_inc(x_12); +lean_inc(x_11); +lean_inc(x_10); +lean_inc(x_9); +lean_dec(x_3); +x_15 = lean_apply_1(x_1, x_12); +x_16 = lean_alloc_ctor(0, 5, 1); +lean_ctor_set(x_16, 0, x_9); +lean_ctor_set(x_16, 1, x_10); +lean_ctor_set(x_16, 2, x_11); +lean_ctor_set(x_16, 3, x_15); +lean_ctor_set(x_16, 4, x_14); +lean_ctor_set_uint8(x_16, sizeof(void*)*5, x_13); +x_17 = lean_box(0); +x_18 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_18, 0, x_17); +lean_ctor_set(x_18, 1, x_16); +return x_18; +} +} +} +lean_object* _init_l_Lean_TypeContext_tracer___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l___private_Init_Lean_TypeContext_2__getTraceState___boxed), 3, 2); +lean_closure_set(x_1, 0, lean_box(0)); +lean_closure_set(x_1, 1, lean_box(0)); +return x_1; +} +} +lean_object* _init_l_Lean_TypeContext_tracer___closed__2() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l___private_Init_Lean_TypeContext_1__getOptions___rarg___boxed), 2, 0); +return x_1; +} +} +lean_object* _init_l_Lean_TypeContext_tracer___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_TypeContext_tracer___lambda__1___boxed), 3, 0); +return x_1; +} +} +lean_object* _init_l_Lean_TypeContext_tracer___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_TypeContext_tracer___closed__2; +x_2 = l_Lean_TypeContext_tracer___closed__3; +x_3 = l_Lean_TypeContext_tracer___closed__1; +x_4 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_4, 0, x_1); +lean_ctor_set(x_4, 1, x_2); +lean_ctor_set(x_4, 2, x_3); +return x_4; +} +} +lean_object* l_Lean_TypeContext_tracer(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l_Lean_TypeContext_tracer___closed__4; +return x_3; +} +} +lean_object* l_Lean_TypeContext_tracer___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l_Lean_TypeContext_tracer___lambda__1(x_1, x_2, x_3); +lean_dec(x_2); +return x_4; +} +} +lean_object* initialize_Init_Control_Reader(lean_object*); +lean_object* initialize_Init_Lean_NameGenerator(lean_object*); +lean_object* initialize_Init_Lean_Environment(lean_object*); +lean_object* initialize_Init_Lean_LocalContext(lean_object*); +lean_object* initialize_Init_Lean_Trace(lean_object*); static bool _G_initialized = false; lean_object* initialize_Init_Lean_TypeContext(lean_object* w) { lean_object * res; if (_G_initialized) return lean_mk_io_result(lean_box(0)); _G_initialized = true; -res = initialize_Init_Lean_Expr(lean_io_mk_world()); +res = initialize_Init_Control_Reader(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +res = initialize_Init_Lean_NameGenerator(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +res = initialize_Init_Lean_Environment(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +res = initialize_Init_Lean_LocalContext(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +res = initialize_Init_Lean_Trace(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +l_Lean_TCState_backtrackable___closed__1 = _init_l_Lean_TCState_backtrackable___closed__1(); +lean_mark_persistent(l_Lean_TCState_backtrackable___closed__1); +l_Lean_TCState_backtrackable___closed__2 = _init_l_Lean_TCState_backtrackable___closed__2(); +lean_mark_persistent(l_Lean_TCState_backtrackable___closed__2); +l_Lean_TCState_backtrackable___closed__3 = _init_l_Lean_TCState_backtrackable___closed__3(); +lean_mark_persistent(l_Lean_TCState_backtrackable___closed__3); +l_Lean_TypeContext_tracer___closed__1 = _init_l_Lean_TypeContext_tracer___closed__1(); +lean_mark_persistent(l_Lean_TypeContext_tracer___closed__1); +l_Lean_TypeContext_tracer___closed__2 = _init_l_Lean_TypeContext_tracer___closed__2(); +lean_mark_persistent(l_Lean_TypeContext_tracer___closed__2); +l_Lean_TypeContext_tracer___closed__3 = _init_l_Lean_TypeContext_tracer___closed__3(); +lean_mark_persistent(l_Lean_TypeContext_tracer___closed__3); +l_Lean_TypeContext_tracer___closed__4 = _init_l_Lean_TypeContext_tracer___closed__4(); +lean_mark_persistent(l_Lean_TypeContext_tracer___closed__4); return lean_mk_io_result(lean_box(0)); } #ifdef __cplusplus