From 3deba604bfdd0803c0a6ba31be75f9ff2770d6da Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Feb 2026 19:56:33 -0800 Subject: [PATCH] feat: cache output universe parameter positions (#12285) This PR implements a cache for the positions of class universe level parameters that only appear in output parameter types. During type class resolution, the cache key for a query like `HAppend.{0, 0, ?u} (BitVec 8) (BitVec 8) ?m` should be independent of the specific metavariable IDs in output parameter positions. To achieve this, output parameter arguments are erased from the cache key. However, universe levels that only appear in output parameter types (e.g., `?u` corresponding to the result type's universe) must also be erased to avoid cache misses when the same query is issued with different universe metavariable IDs. This function identifies which universe level parameter positions are "output-only" by collecting all level param names that appear in non-output parameter domains, then returning the positions of any level params not in that set. **Remark**: This PR requires a manual update stage0 because it changes the structure of our .olean files. --- src/Lean/Class.lean | 72 ++- stage0/stdlib/Lean/Class.c | 953 +++++++++++++++++++++++++++++-------- 2 files changed, 821 insertions(+), 204 deletions(-) diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean index 65927edbee..8f9d3e1f14 100644 --- a/src/Lean/Class.lean +++ b/src/Lean/Class.lean @@ -4,12 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Lean.Attributes - +import Lean.Util.CollectLevelParams public section - namespace Lean /-- An entry for the persistent environment extension for declared type classes -/ @@ -17,14 +15,21 @@ structure ClassEntry where /-- Class name. -/ name : Name /-- - Position of the class `outParams`. - For example, for class - ``` - class GetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) where - ``` - `outParams := #[2, 3]` + Position of the class `outParams`. + For example, for class + ``` + class GetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) where + ``` + `outParams := #[2, 3]` -/ outParams : Array Nat + /-- + Positions of universe level parameters that only appear in output parameter types. + For example, for `HAdd (α : Type u) (β : Type v) (γ : outParam (Type w))`, + `outLevelParams := #[2]` since universe `w` only appears in the output parameter `γ`. + This is used to normalize TC resolution cache keys. + -/ + outLevelParams : Array Nat namespace ClassEntry @@ -36,12 +41,15 @@ end ClassEntry /-- State of the type class environment extension. -/ structure ClassState where outParamMap : SMap Name (Array Nat) := SMap.empty + outLevelParamMap : SMap Name (Array Nat) := SMap.empty deriving Inhabited namespace ClassState def addEntry (s : ClassState) (entry : ClassEntry) : ClassState := - { s with outParamMap := s.outParamMap.insert entry.name entry.outParams } + { s with + outParamMap := s.outParamMap.insert entry.name entry.outParams + outLevelParamMap := s.outLevelParamMap.insert entry.name entry.outLevelParams } /-- Switch the state into persistent mode. We switch to this mode after @@ -49,7 +57,9 @@ we read all imported .olean files. Recall that we use a `SMap` for implementing the state of the type class environment extension. -/ def switch (s : ClassState) : ClassState := - { s with outParamMap := s.outParamMap.switch } + { s with + outParamMap := s.outParamMap.switch + outLevelParamMap := s.outLevelParamMap.switch } end ClassState @@ -79,6 +89,10 @@ def hasOutParams (env : Environment) (declName : Name) : Bool := | some outParams => !outParams.isEmpty | none => false +/-- If `declName` is a class, return the positions of universe level parameters that only appear in output parameter types. -/ +def getOutLevelParamPositions? (env : Environment) (declName : Name) : Option (Array Nat) := + (classExtension.getState env).outLevelParamMap.find? declName + /-- Auxiliary function for collection the position class `outParams`, and checking whether they are being correctly used. @@ -146,6 +160,39 @@ where keepBinderInfo () | _ => type +/-- +Compute positions of universe level parameters that only appear in output parameter types. + +During type class resolution, the cache key for a query like +`HAppend.{0, 0, ?u} (BitVec 8) (BitVec 8) ?m` should be independent of the specific +metavariable IDs in output parameter positions. To achieve this, output parameter arguments +are erased from the cache key. However, universe levels that only appear in output parameter +types (e.g., `?u` corresponding to the result type's universe) must also be erased to avoid +cache misses when the same query is issued with different universe metavariable IDs. + +This function identifies which universe level parameter positions are "output-only" by +collecting all level param names that appear in non-output parameter domains, then returning +the positions of any level params not in that set. +-/ +private partial def computeOutLevelParams (type : Expr) (outParams : Array Nat) (levelParams : List Name) : Array Nat := Id.run do + let nonOutLevels := go type 0 {} |>.params + let mut result := #[] + let mut i := 0 + for name in levelParams do + unless nonOutLevels.contains name do + result := result.push i + i := i + 1 + result +where + go (type : Expr) (i : Nat) (s : CollectLevelParams.State) : CollectLevelParams.State := + match type with + | .forallE _ d b _ => + if outParams.contains i then + go b (i + 1) s + else + go b (i + 1) (collectLevelParams s d) + | _ => s + /-- Add a new type class with the given name to the environment. `declName` must not be the name of an existing type class, @@ -161,7 +208,8 @@ def addClass (env : Environment) (clsName : Name) : Except MessageData Environme unless decl matches .inductInfo .. | .axiomInfo .. do throw m!"invalid 'class', declaration '{.ofConstName clsName}' must be inductive datatype, structure, or constant" let outParams ← checkOutParam 0 #[] #[] decl.type - return classExtension.addEntry env { name := clsName, outParams } + let outLevelParams := computeOutLevelParams decl.type outParams decl.levelParams + return classExtension.addEntry env { name := clsName, outParams, outLevelParams } /-- Registers an inductive type or structure as a type class. Using `class` or `class inductive` is diff --git a/stage0/stdlib/Lean/Class.c b/stage0/stdlib/Lean/Class.c index 556e575659..aa6e1ced3f 100644 --- a/stage0/stdlib/Lean/Class.c +++ b/stage0/stdlib/Lean/Class.c @@ -1,6 +1,6 @@ // Lean compiler output // Module: Lean.Class -// Imports: public import Lean.Attributes +// Imports: public import Lean.Attributes import Lean.Util.CollectLevelParams #include #if defined(__clang__) #pragma clang diagnostic ignored "-Wunused-parameter" @@ -23,6 +23,7 @@ lean_object* l_Lean_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_obj static lean_object* l_Lean_instInhabitedClassState_default___closed__2; static lean_object* l_Lean_instInhabitedClassState_default___closed__3; static lean_object* l_Lean_instInhabitedClassState_default___closed__4; +static lean_object* l_Lean_instInhabitedClassState_default___closed__5; LEAN_EXPORT lean_object* l_Lean_instInhabitedClassState_default; LEAN_EXPORT lean_object* l_Lean_instInhabitedClassState; lean_object* lean_array_get_size(lean_object*); @@ -105,6 +106,7 @@ LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_foldlMUnsafe LEAN_EXPORT lean_object* l_Lean_mkStateFromImportedEntries___at___00Lean_initFn_00___x40_Lean_Class_903839608____hygCtx___hyg_2__spec__1(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_mkStateFromImportedEntries___at___00Lean_initFn_00___x40_Lean_Class_903839608____hygCtx___hyg_2__spec__1___boxed(lean_object*, lean_object*); static lean_object* l_Lean_initFn___lam__1___closed__0_00___x40_Lean_Class_903839608____hygCtx___hyg_2_; +static lean_object* l_Lean_initFn___lam__1___closed__1_00___x40_Lean_Class_903839608____hygCtx___hyg_2_; LEAN_EXPORT lean_object* l_Lean_initFn___lam__1_00___x40_Lean_Class_903839608____hygCtx___hyg_2_(lean_object*); LEAN_EXPORT lean_object* l_Lean_initFn___lam__1_00___x40_Lean_Class_903839608____hygCtx___hyg_2____boxed(lean_object*); static const lean_closure_object l_Lean_initFn___closed__0_00___x40_Lean_Class_903839608____hygCtx___hyg_2__value = {.m_header = {.m_rc = 0, .m_cs_sz = sizeof(lean_closure_object) + sizeof(void*)*0, .m_other = 0, .m_tag = 245}, .m_fun = (void*)l_Lean_initFn___lam__0_00___x40_Lean_Class_903839608____hygCtx___hyg_2_, .m_arity = 1, .m_num_fixed = 0, .m_objs = {} }; @@ -180,6 +182,8 @@ LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAtAux___at___00Lean_Persis uint8_t l_Array_isEmpty___redArg(lean_object*); LEAN_EXPORT uint8_t lean_has_out_params(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_hasOutParams___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_getOutLevelParamPositions_x3f(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_getOutLevelParamPositions_x3f___boxed(lean_object*, lean_object*); uint8_t l_Lean_instBEqFVarId_beq(lean_object*, lean_object*); LEAN_EXPORT uint8_t l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___00Array_contains___at___00__private_Lean_Class_0__Lean_checkOutParam_spec__0_spec__0(lean_object*, lean_object*, size_t, size_t); LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___00Array_contains___at___00__private_Lean_Class_0__Lean_checkOutParam_spec__0_spec__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -232,6 +236,28 @@ lean_object* l_Lean_Expr_appArg_x21(lean_object*); lean_object* lean_mk_empty_array_with_capacity(lean_object*); static lean_object* l_Lean_mkOutParamArgsImplicit___closed__0; LEAN_EXPORT lean_object* lean_mk_outparam_args_implicit(lean_object*); +uint8_t lean_nat_dec_eq(lean_object*, lean_object*); +LEAN_EXPORT uint8_t l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___00Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_go_spec__0_spec__0(lean_object*, lean_object*, size_t, size_t); +LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___00Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_go_spec__0_spec__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT uint8_t l_Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_go_spec__0(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_go_spec__0___boxed(lean_object*, lean_object*); +lean_object* l_Lean_collectLevelParams(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Lean_Class_0__Lean_computeOutLevelParams_go(lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Lean_Class_0__Lean_computeOutLevelParams_go___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT uint8_t l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___00Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__0_spec__0(lean_object*, lean_object*, size_t, size_t); +LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___00Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__0_spec__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT uint8_t l_Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__0(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__0___boxed(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_List_forIn_x27_loop___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__1___redArg(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_List_forIn_x27_loop___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__1___redArg___boxed(lean_object*, lean_object*, lean_object*); +static lean_object* l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__0; +static lean_object* l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__1; +static lean_object* l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__2; +static lean_object* l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__3; +LEAN_EXPORT lean_object* l___private_Lean_Class_0__Lean_computeOutLevelParams(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Lean_Class_0__Lean_computeOutLevelParams___boxed(lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_List_forIn_x27_loop___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_List_forIn_x27_loop___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static const lean_string_object l_Lean_addClass___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 31, .m_capacity = 31, .m_length = 30, .m_data = "invalid 'class', declaration '"}; static const lean_object* l_Lean_addClass___closed__0 = (const lean_object*)&l_Lean_addClass___closed__0_value; static lean_object* l_Lean_addClass___closed__1; @@ -249,6 +275,7 @@ static const lean_object* l_Lean_addClass___closed__8 = (const lean_object*)&l_L static lean_object* l_Lean_addClass___closed__9; lean_object* l_Lean_Environment_find_x3f(lean_object*, lean_object*, uint8_t); lean_object* l_Lean_ConstantInfo_type(lean_object*); +lean_object* l_Lean_ConstantInfo_levelParams(lean_object*); lean_object* l_Lean_PersistentEnvExtension_addEntry___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_MessageData_ofConstName(lean_object*, uint8_t); lean_object* l_Lean_MessageData_ofName(lean_object*); @@ -427,11 +454,22 @@ lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_3); return x_4; } } +static lean_object* _init_l_Lean_instInhabitedClassState_default___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_instInhabitedClassState_default___closed__4; +x_2 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_2, 0, x_1); +lean_ctor_set(x_2, 1, x_1); +return x_2; +} +} static lean_object* _init_l_Lean_instInhabitedClassState_default() { _start: { lean_object* x_1; -x_1 = l_Lean_instInhabitedClassState_default___closed__4; +x_1 = l_Lean_instInhabitedClassState_default___closed__5; return x_1; } } @@ -1343,14 +1381,50 @@ return x_18; LEAN_EXPORT lean_object* l_Lean_ClassState_addEntry(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_2, 0); -lean_inc(x_3); -x_4 = lean_ctor_get(x_2, 1); -lean_inc_ref(x_4); +uint8_t x_3; +x_3 = !lean_is_exclusive(x_1); +if (x_3 == 0) +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; +x_4 = lean_ctor_get(x_1, 0); +x_5 = lean_ctor_get(x_1, 1); +x_6 = lean_ctor_get(x_2, 0); +lean_inc(x_6); +x_7 = lean_ctor_get(x_2, 1); +lean_inc_ref(x_7); +x_8 = lean_ctor_get(x_2, 2); +lean_inc_ref(x_8); lean_dec_ref(x_2); -x_5 = l_Lean_SMap_insert___at___00Lean_ClassState_addEntry_spec__0___redArg(x_1, x_3, x_4); -return x_5; +lean_inc(x_6); +x_9 = l_Lean_SMap_insert___at___00Lean_ClassState_addEntry_spec__0___redArg(x_4, x_6, x_7); +x_10 = l_Lean_SMap_insert___at___00Lean_ClassState_addEntry_spec__0___redArg(x_5, x_6, x_8); +lean_ctor_set(x_1, 1, x_10); +lean_ctor_set(x_1, 0, x_9); +return x_1; +} +else +{ +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; lean_object* x_18; +x_11 = lean_ctor_get(x_1, 0); +x_12 = lean_ctor_get(x_1, 1); +lean_inc(x_12); +lean_inc(x_11); +lean_dec(x_1); +x_13 = lean_ctor_get(x_2, 0); +lean_inc(x_13); +x_14 = lean_ctor_get(x_2, 1); +lean_inc_ref(x_14); +x_15 = lean_ctor_get(x_2, 2); +lean_inc_ref(x_15); +lean_dec_ref(x_2); +lean_inc(x_13); +x_16 = l_Lean_SMap_insert___at___00Lean_ClassState_addEntry_spec__0___redArg(x_11, x_13, x_14); +x_17 = l_Lean_SMap_insert___at___00Lean_ClassState_addEntry_spec__0___redArg(x_12, x_13, x_15); +x_18 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_18, 0, x_16); +lean_ctor_set(x_18, 1, x_17); +return x_18; +} } } LEAN_EXPORT lean_object* l_Lean_SMap_insert___at___00Lean_ClassState_addEntry_spec__0(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { @@ -1533,9 +1607,34 @@ return x_3; LEAN_EXPORT lean_object* l_Lean_ClassState_switch(lean_object* x_1) { _start: { -lean_object* x_2; -x_2 = l_Lean_SMap_switch___at___00Lean_ClassState_switch_spec__0___redArg(x_1); -return x_2; +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; +x_3 = lean_ctor_get(x_1, 0); +x_4 = lean_ctor_get(x_1, 1); +x_5 = l_Lean_SMap_switch___at___00Lean_ClassState_switch_spec__0___redArg(x_3); +x_6 = l_Lean_SMap_switch___at___00Lean_ClassState_switch_spec__0___redArg(x_4); +lean_ctor_set(x_1, 1, x_6); +lean_ctor_set(x_1, 0, x_5); +return x_1; +} +else +{ +lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; +x_7 = lean_ctor_get(x_1, 0); +x_8 = lean_ctor_get(x_1, 1); +lean_inc(x_8); +lean_inc(x_7); +lean_dec(x_1); +x_9 = l_Lean_SMap_switch___at___00Lean_ClassState_switch_spec__0___redArg(x_7); +x_10 = l_Lean_SMap_switch___at___00Lean_ClassState_switch_spec__0___redArg(x_8); +x_11 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_11, 0, x_9); +lean_ctor_set(x_11, 1, x_10); +return x_11; +} } } static lean_object* _init_l_Lean_SMap_empty___at___00Lean_initFn_00___x40_Lean_Class_903839608____hygCtx___hyg_2__spec__0___closed__0() { @@ -1760,13 +1859,24 @@ x_1 = l_Lean_SMap_empty___at___00Lean_initFn_00___x40_Lean_Class_903839608____hy return x_1; } } +static lean_object* _init_l_Lean_initFn___lam__1___closed__1_00___x40_Lean_Class_903839608____hygCtx___hyg_2_() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_initFn___lam__1___closed__0_00___x40_Lean_Class_903839608____hygCtx___hyg_2_; +x_2 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_2, 0, x_1); +lean_ctor_set(x_2, 1, x_1); +return x_2; +} +} LEAN_EXPORT lean_object* l_Lean_initFn___lam__1_00___x40_Lean_Class_903839608____hygCtx___hyg_2_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_2 = l_Lean_initFn___lam__1___closed__0_00___x40_Lean_Class_903839608____hygCtx___hyg_2_; +x_2 = l_Lean_initFn___lam__1___closed__1_00___x40_Lean_Class_903839608____hygCtx___hyg_2_; x_3 = l_Lean_mkStateFromImportedEntries___at___00Lean_initFn_00___x40_Lean_Class_903839608____hygCtx___hyg_2__spec__1(x_2, x_1); -x_4 = l_Lean_SMap_switch___at___00Lean_ClassState_switch_spec__0___redArg(x_3); +x_4 = l_Lean_ClassState_switch(x_3); return x_4; } } @@ -2019,7 +2129,7 @@ return x_4; LEAN_EXPORT uint8_t lean_is_class(lean_object* x_1, lean_object* x_2) { _start: { -lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9; +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; x_3 = l_Lean_classExtension; x_4 = lean_ctor_get(x_3, 0); lean_inc_ref(x_4); @@ -2030,9 +2140,12 @@ x_6 = l_Lean_instInhabitedClassState_default; x_7 = lean_box(0); x_8 = l_Lean_SimplePersistentEnvExtension_getState___redArg(x_6, x_3, x_1, x_5, x_7); lean_dec(x_5); -x_9 = l_Lean_SMap_contains___at___00Lean_isClass_spec__0___redArg(x_8, x_2); +x_9 = lean_ctor_get(x_8, 0); +lean_inc_ref(x_9); +lean_dec(x_8); +x_10 = l_Lean_SMap_contains___at___00Lean_isClass_spec__0___redArg(x_9, x_2); lean_dec(x_2); -return x_9; +return x_10; } } LEAN_EXPORT lean_object* l_Lean_isClass___boxed(lean_object* x_1, lean_object* x_2) { @@ -2489,7 +2602,7 @@ return x_3; LEAN_EXPORT lean_object* l_Lean_getOutParamPositions_x3f(lean_object* x_1, lean_object* x_2) { _start: { -lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; x_3 = l_Lean_classExtension; x_4 = lean_ctor_get(x_3, 0); lean_inc_ref(x_4); @@ -2500,8 +2613,11 @@ x_6 = l_Lean_instInhabitedClassState_default; x_7 = lean_box(0); x_8 = l_Lean_SimplePersistentEnvExtension_getState___redArg(x_6, x_3, x_1, x_5, x_7); lean_dec(x_5); -x_9 = l_Lean_SMap_find_x3f___at___00Lean_getOutParamPositions_x3f_spec__0___redArg(x_8, x_2); -return x_9; +x_9 = lean_ctor_get(x_8, 0); +lean_inc_ref(x_9); +lean_dec(x_8); +x_10 = l_Lean_SMap_find_x3f___at___00Lean_getOutParamPositions_x3f_spec__0___redArg(x_9, x_2); +return x_10; } } LEAN_EXPORT lean_object* l_Lean_getOutParamPositions_x3f___boxed(lean_object* x_1, lean_object* x_2) { @@ -2665,6 +2781,36 @@ x_4 = lean_box(x_3); return x_4; } } +LEAN_EXPORT lean_object* l_Lean_getOutLevelParamPositions_x3f(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; +x_3 = l_Lean_classExtension; +x_4 = lean_ctor_get(x_3, 0); +lean_inc_ref(x_4); +x_5 = lean_ctor_get(x_4, 2); +lean_inc(x_5); +lean_dec_ref(x_4); +x_6 = l_Lean_instInhabitedClassState_default; +x_7 = lean_box(0); +x_8 = l_Lean_SimplePersistentEnvExtension_getState___redArg(x_6, x_3, x_1, x_5, x_7); +lean_dec(x_5); +x_9 = lean_ctor_get(x_8, 1); +lean_inc_ref(x_9); +lean_dec(x_8); +x_10 = l_Lean_SMap_find_x3f___at___00Lean_getOutParamPositions_x3f_spec__0___redArg(x_9, x_2); +return x_10; +} +} +LEAN_EXPORT lean_object* l_Lean_getOutLevelParamPositions_x3f___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; +x_3 = l_Lean_getOutLevelParamPositions_x3f(x_1, x_2); +lean_dec(x_2); +return x_3; +} +} LEAN_EXPORT uint8_t l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___00Array_contains___at___00__private_Lean_Class_0__Lean_checkOutParam_spec__0_spec__0(lean_object* x_1, lean_object* x_2, size_t x_3, size_t x_4) { _start: { @@ -3038,7 +3184,7 @@ return x_6; LEAN_EXPORT lean_object* l___private_Lean_Class_0__Lean_mkOutParamArgsImplicit_go(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { -lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7; uint8_t x_8; lean_object* x_13; lean_object* x_14; uint8_t x_15; uint8_t x_16; lean_object* x_17; uint8_t x_18; +lean_object* x_4; uint8_t x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8; uint8_t x_13; uint8_t x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; if (lean_obj_tag(x_2) == 7) { lean_object* x_23; lean_object* x_24; uint8_t x_25; lean_object* x_42; uint8_t x_65; @@ -3104,10 +3250,10 @@ x_35 = lean_usize_dec_eq(x_33, x_34); if (x_35 == 0) { lean_inc(x_26); -x_4 = x_31; -x_5 = x_32; -x_6 = x_26; -x_7 = x_29; +x_4 = x_32; +x_5 = x_29; +x_6 = x_31; +x_7 = x_26; x_8 = x_35; goto block_12; } @@ -3118,10 +3264,10 @@ x_36 = lean_ptr_addr(x_28); x_37 = lean_ptr_addr(x_31); x_38 = lean_usize_dec_eq(x_36, x_37); lean_inc(x_26); -x_4 = x_31; -x_5 = x_32; -x_6 = x_26; -x_7 = x_29; +x_4 = x_32; +x_5 = x_29; +x_6 = x_31; +x_7 = x_26; x_8 = x_38; goto block_12; } @@ -3164,11 +3310,11 @@ x_58 = lean_usize_dec_eq(x_56, x_57); if (x_58 == 0) { lean_inc(x_43); -x_13 = x_54; -x_14 = x_42; -x_15 = x_46; -x_16 = x_55; -x_17 = x_43; +x_13 = x_55; +x_14 = x_46; +x_15 = x_42; +x_16 = x_43; +x_17 = x_54; x_18 = x_58; goto block_22; } @@ -3179,11 +3325,11 @@ x_59 = lean_ptr_addr(x_45); x_60 = lean_ptr_addr(x_54); x_61 = lean_usize_dec_eq(x_59, x_60); lean_inc(x_43); -x_13 = x_54; -x_14 = x_42; -x_15 = x_46; -x_16 = x_55; -x_17 = x_43; +x_13 = x_55; +x_14 = x_46; +x_15 = x_42; +x_16 = x_43; +x_17 = x_54; x_18 = x_61; goto block_22; } @@ -3213,24 +3359,24 @@ if (x_8 == 0) { lean_object* x_9; lean_dec_ref(x_1); -x_9 = l_Lean_Expr_forallE___override(x_6, x_5, x_4, x_7); +x_9 = l_Lean_Expr_forallE___override(x_7, x_4, x_6, x_5); return x_9; } else { uint8_t x_10; -x_10 = l_Lean_instBEqBinderInfo_beq(x_7, x_7); +x_10 = l_Lean_instBEqBinderInfo_beq(x_5, x_5); if (x_10 == 0) { lean_object* x_11; lean_dec_ref(x_1); -x_11 = l_Lean_Expr_forallE___override(x_6, x_5, x_4, x_7); +x_11 = l_Lean_Expr_forallE___override(x_7, x_4, x_6, x_5); return x_11; } else { -lean_dec(x_6); -lean_dec_ref(x_5); +lean_dec(x_7); +lean_dec_ref(x_6); lean_dec_ref(x_4); return x_1; } @@ -3242,25 +3388,25 @@ if (x_18 == 0) { lean_object* x_19; lean_dec_ref(x_1); -x_19 = l_Lean_Expr_forallE___override(x_17, x_14, x_13, x_16); +x_19 = l_Lean_Expr_forallE___override(x_16, x_15, x_17, x_13); return x_19; } else { uint8_t x_20; -x_20 = l_Lean_instBEqBinderInfo_beq(x_15, x_16); +x_20 = l_Lean_instBEqBinderInfo_beq(x_14, x_13); if (x_20 == 0) { lean_object* x_21; lean_dec_ref(x_1); -x_21 = l_Lean_Expr_forallE___override(x_17, x_14, x_13, x_16); +x_21 = l_Lean_Expr_forallE___override(x_16, x_15, x_17, x_13); return x_21; } else { -lean_dec(x_17); -lean_dec_ref(x_14); -lean_dec_ref(x_13); +lean_dec_ref(x_17); +lean_dec(x_16); +lean_dec_ref(x_15); return x_1; } } @@ -3286,6 +3432,394 @@ x_3 = l___private_Lean_Class_0__Lean_mkOutParamArgsImplicit_go(x_1, x_1, x_2); return x_3; } } +LEAN_EXPORT uint8_t l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___00Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_go_spec__0_spec__0(lean_object* x_1, lean_object* x_2, size_t x_3, size_t x_4) { +_start: +{ +uint8_t x_5; +x_5 = lean_usize_dec_eq(x_3, x_4); +if (x_5 == 0) +{ +lean_object* x_6; uint8_t x_7; +x_6 = lean_array_uget(x_2, x_3); +x_7 = lean_nat_dec_eq(x_1, x_6); +lean_dec(x_6); +if (x_7 == 0) +{ +size_t x_8; size_t x_9; +x_8 = 1; +x_9 = lean_usize_add(x_3, x_8); +x_3 = x_9; +goto _start; +} +else +{ +return x_7; +} +} +else +{ +uint8_t x_11; +x_11 = 0; +return x_11; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___00Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_go_spec__0_spec__0___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +size_t x_5; size_t x_6; uint8_t x_7; lean_object* x_8; +x_5 = lean_unbox_usize(x_3); +lean_dec(x_3); +x_6 = lean_unbox_usize(x_4); +lean_dec(x_4); +x_7 = l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___00Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_go_spec__0_spec__0(x_1, x_2, x_5, x_6); +lean_dec_ref(x_2); +lean_dec(x_1); +x_8 = lean_box(x_7); +return x_8; +} +} +LEAN_EXPORT uint8_t l_Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_go_spec__0(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; uint8_t x_5; +x_3 = lean_unsigned_to_nat(0u); +x_4 = lean_array_get_size(x_1); +x_5 = lean_nat_dec_lt(x_3, x_4); +if (x_5 == 0) +{ +return x_5; +} +else +{ +if (x_5 == 0) +{ +return x_5; +} +else +{ +size_t x_6; size_t x_7; uint8_t x_8; +x_6 = 0; +x_7 = lean_usize_of_nat(x_4); +x_8 = l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___00Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_go_spec__0_spec__0(x_2, x_1, x_6, x_7); +return x_8; +} +} +} +} +LEAN_EXPORT lean_object* l_Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_go_spec__0___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +uint8_t x_3; lean_object* x_4; +x_3 = l_Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_go_spec__0(x_1, x_2); +lean_dec(x_2); +lean_dec_ref(x_1); +x_4 = lean_box(x_3); +return x_4; +} +} +LEAN_EXPORT lean_object* l___private_Lean_Class_0__Lean_computeOutLevelParams_go(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +if (lean_obj_tag(x_2) == 7) +{ +lean_object* x_5; lean_object* x_6; uint8_t x_7; +x_5 = lean_ctor_get(x_2, 1); +lean_inc_ref(x_5); +x_6 = lean_ctor_get(x_2, 2); +lean_inc_ref(x_6); +lean_dec_ref(x_2); +x_7 = l_Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_go_spec__0(x_1, x_3); +if (x_7 == 0) +{ +lean_object* x_8; lean_object* x_9; lean_object* x_10; +x_8 = lean_unsigned_to_nat(1u); +x_9 = lean_nat_add(x_3, x_8); +lean_dec(x_3); +x_10 = l_Lean_collectLevelParams(x_4, x_5); +x_2 = x_6; +x_3 = x_9; +x_4 = x_10; +goto _start; +} +else +{ +lean_object* x_12; lean_object* x_13; +lean_dec_ref(x_5); +x_12 = lean_unsigned_to_nat(1u); +x_13 = lean_nat_add(x_3, x_12); +lean_dec(x_3); +x_2 = x_6; +x_3 = x_13; +goto _start; +} +} +else +{ +lean_dec(x_3); +lean_dec_ref(x_2); +return x_4; +} +} +} +LEAN_EXPORT lean_object* l___private_Lean_Class_0__Lean_computeOutLevelParams_go___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; +x_5 = l___private_Lean_Class_0__Lean_computeOutLevelParams_go(x_1, x_2, x_3, x_4); +lean_dec_ref(x_1); +return x_5; +} +} +LEAN_EXPORT uint8_t l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___00Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__0_spec__0(lean_object* x_1, lean_object* x_2, size_t x_3, size_t x_4) { +_start: +{ +uint8_t x_5; +x_5 = lean_usize_dec_eq(x_3, x_4); +if (x_5 == 0) +{ +lean_object* x_6; uint8_t x_7; +x_6 = lean_array_uget(x_2, x_3); +x_7 = lean_name_eq(x_1, x_6); +lean_dec(x_6); +if (x_7 == 0) +{ +size_t x_8; size_t x_9; +x_8 = 1; +x_9 = lean_usize_add(x_3, x_8); +x_3 = x_9; +goto _start; +} +else +{ +return x_7; +} +} +else +{ +uint8_t x_11; +x_11 = 0; +return x_11; +} +} +} +LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___00Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__0_spec__0___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +size_t x_5; size_t x_6; uint8_t x_7; lean_object* x_8; +x_5 = lean_unbox_usize(x_3); +lean_dec(x_3); +x_6 = lean_unbox_usize(x_4); +lean_dec(x_4); +x_7 = l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___00Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__0_spec__0(x_1, x_2, x_5, x_6); +lean_dec_ref(x_2); +lean_dec(x_1); +x_8 = lean_box(x_7); +return x_8; +} +} +LEAN_EXPORT uint8_t l_Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__0(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; uint8_t x_5; +x_3 = lean_unsigned_to_nat(0u); +x_4 = lean_array_get_size(x_1); +x_5 = lean_nat_dec_lt(x_3, x_4); +if (x_5 == 0) +{ +return x_5; +} +else +{ +if (x_5 == 0) +{ +return x_5; +} +else +{ +size_t x_6; size_t x_7; uint8_t x_8; +x_6 = 0; +x_7 = lean_usize_of_nat(x_4); +x_8 = l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___00Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__0_spec__0(x_2, x_1, x_6, x_7); +return x_8; +} +} +} +} +LEAN_EXPORT lean_object* l_Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__0___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +uint8_t x_3; lean_object* x_4; +x_3 = l_Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__0(x_1, x_2); +lean_dec(x_2); +lean_dec_ref(x_1); +x_4 = lean_box(x_3); +return x_4; +} +} +LEAN_EXPORT lean_object* l_List_forIn_x27_loop___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__1___redArg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_2) == 0) +{ +return x_3; +} +else +{ +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_15; +x_4 = lean_ctor_get(x_2, 0); +x_5 = lean_ctor_get(x_2, 1); +x_6 = lean_ctor_get(x_3, 0); +lean_inc(x_6); +x_7 = lean_ctor_get(x_3, 1); +lean_inc(x_7); +if (lean_is_exclusive(x_3)) { + lean_ctor_release(x_3, 0); + lean_ctor_release(x_3, 1); + x_8 = x_3; +} else { + lean_dec_ref(x_3); + x_8 = lean_box(0); +} +x_15 = l_Array_contains___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__0(x_1, x_4); +if (x_15 == 0) +{ +lean_object* x_16; +lean_inc(x_6); +x_16 = lean_array_push(x_7, x_6); +x_9 = x_16; +goto block_14; +} +else +{ +x_9 = x_7; +goto block_14; +} +block_14: +{ +lean_object* x_10; lean_object* x_11; lean_object* x_12; +x_10 = lean_unsigned_to_nat(1u); +x_11 = lean_nat_add(x_6, x_10); +lean_dec(x_6); +if (lean_is_scalar(x_8)) { + x_12 = lean_alloc_ctor(0, 2, 0); +} else { + x_12 = x_8; +} +lean_ctor_set(x_12, 0, x_11); +lean_ctor_set(x_12, 1, x_9); +x_2 = x_5; +x_3 = x_12; +goto _start; +} +} +} +} +LEAN_EXPORT lean_object* l_List_forIn_x27_loop___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__1___redArg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l_List_forIn_x27_loop___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__1___redArg(x_1, x_2, x_3); +lean_dec(x_2); +lean_dec_ref(x_1); +return x_4; +} +} +static lean_object* _init_l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__0() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = lean_unsigned_to_nat(16u); +x_3 = lean_mk_array(x_2, x_1); +return x_3; +} +} +static lean_object* _init_l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__0; +x_2 = lean_unsigned_to_nat(0u); +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; +} +} +static lean_object* _init_l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_mkOutParamArgsImplicit___closed__0; +x_2 = l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__1; +x_3 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_3, 0, x_2); +lean_ctor_set(x_3, 1, x_2); +lean_ctor_set(x_3, 2, x_1); +return x_3; +} +} +static lean_object* _init_l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_mkOutParamArgsImplicit___closed__0; +x_2 = lean_unsigned_to_nat(0u); +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_EXPORT lean_object* l___private_Lean_Class_0__Lean_computeOutLevelParams(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; +x_4 = lean_unsigned_to_nat(0u); +x_5 = l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__2; +x_6 = l___private_Lean_Class_0__Lean_computeOutLevelParams_go(x_2, x_1, x_4, x_5); +x_7 = lean_ctor_get(x_6, 2); +lean_inc_ref(x_7); +lean_dec_ref(x_6); +x_8 = l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__3; +x_9 = l_List_forIn_x27_loop___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__1___redArg(x_7, x_3, x_8); +lean_dec_ref(x_7); +x_10 = lean_ctor_get(x_9, 1); +lean_inc(x_10); +lean_dec_ref(x_9); +return x_10; +} +} +LEAN_EXPORT lean_object* l___private_Lean_Class_0__Lean_computeOutLevelParams___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l___private_Lean_Class_0__Lean_computeOutLevelParams(x_1, x_2, x_3); +lean_dec(x_3); +lean_dec_ref(x_2); +return x_4; +} +} +LEAN_EXPORT lean_object* l_List_forIn_x27_loop___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +_start: +{ +lean_object* x_6; +x_6 = l_List_forIn_x27_loop___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__1___redArg(x_1, x_3, x_4); +return x_6; +} +} +LEAN_EXPORT lean_object* l_List_forIn_x27_loop___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +_start: +{ +lean_object* x_6; +x_6 = l_List_forIn_x27_loop___at___00__private_Lean_Class_0__Lean_computeOutLevelParams_spec__1(x_1, x_2, x_3, x_4, x_5); +lean_dec(x_3); +lean_dec(x_2); +lean_dec_ref(x_1); +return x_6; +} +} static lean_object* _init_l_Lean_addClass___closed__1() { _start: { @@ -3356,51 +3890,53 @@ switch (lean_obj_tag(x_6)) { case 5: { lean_free_object(x_4); -goto block_30; +goto block_34; } case 0: { lean_free_object(x_4); -goto block_30; +goto block_34; } default: { if (x_3 == 0) { -lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; +lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_dec(x_6); lean_dec_ref(x_1); -x_31 = l_Lean_addClass___closed__1; -x_32 = l_Lean_MessageData_ofConstName(x_2, x_3); -x_33 = lean_alloc_ctor(7, 2, 0); -lean_ctor_set(x_33, 0, x_31); -lean_ctor_set(x_33, 1, x_32); -x_34 = l_Lean_addClass___closed__3; -x_35 = lean_alloc_ctor(7, 2, 0); -lean_ctor_set(x_35, 0, x_33); -lean_ctor_set(x_35, 1, x_34); +x_35 = l_Lean_addClass___closed__1; +x_36 = l_Lean_MessageData_ofConstName(x_2, x_3); +x_37 = lean_alloc_ctor(7, 2, 0); +lean_ctor_set(x_37, 0, x_35); +lean_ctor_set(x_37, 1, x_36); +x_38 = l_Lean_addClass___closed__3; +x_39 = lean_alloc_ctor(7, 2, 0); +lean_ctor_set(x_39, 0, x_37); +lean_ctor_set(x_39, 1, x_38); lean_ctor_set_tag(x_4, 0); -lean_ctor_set(x_4, 0, x_35); +lean_ctor_set(x_4, 0, x_39); return x_4; } else { lean_free_object(x_4); -goto block_30; +goto block_34; } } } -block_30: +block_34: { lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; x_7 = lean_unsigned_to_nat(0u); x_8 = l_Lean_mkOutParamArgsImplicit___closed__0; x_9 = l_Lean_ConstantInfo_type(x_6); -lean_dec(x_6); +lean_inc_ref(x_9); x_10 = l___private_Lean_Class_0__Lean_checkOutParam(x_7, x_8, x_8, x_9); if (lean_obj_tag(x_10) == 0) { uint8_t x_11; +lean_dec_ref(x_9); +lean_dec(x_6); lean_dec(x_2); lean_dec_ref(x_1); x_11 = !lean_is_exclusive(x_10); @@ -3425,7 +3961,7 @@ uint8_t x_14; x_14 = !lean_is_exclusive(x_10); if (x_14 == 0) { -lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; +lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; x_15 = lean_ctor_get(x_10, 0); x_16 = l_Lean_classExtension; x_17 = lean_ctor_get(x_16, 0); @@ -3433,157 +3969,78 @@ lean_inc_ref(x_17); x_18 = lean_ctor_get(x_17, 2); lean_inc(x_18); lean_dec_ref(x_17); -x_19 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_19, 0, x_2); -lean_ctor_set(x_19, 1, x_15); -x_20 = lean_box(0); -x_21 = l_Lean_PersistentEnvExtension_addEntry___redArg(x_16, x_1, x_19, x_18, x_20); +x_19 = l_Lean_ConstantInfo_levelParams(x_6); +lean_dec(x_6); +x_20 = l___private_Lean_Class_0__Lean_computeOutLevelParams(x_9, x_15, x_19); +lean_dec(x_19); +x_21 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_21, 0, x_2); +lean_ctor_set(x_21, 1, x_15); +lean_ctor_set(x_21, 2, x_20); +x_22 = lean_box(0); +x_23 = l_Lean_PersistentEnvExtension_addEntry___redArg(x_16, x_1, x_21, x_18, x_22); lean_dec(x_18); -lean_ctor_set(x_10, 0, x_21); +lean_ctor_set(x_10, 0, x_23); return x_10; } else { -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; -x_22 = lean_ctor_get(x_10, 0); -lean_inc(x_22); +lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; +x_24 = lean_ctor_get(x_10, 0); +lean_inc(x_24); lean_dec(x_10); -x_23 = l_Lean_classExtension; -x_24 = lean_ctor_get(x_23, 0); -lean_inc_ref(x_24); -x_25 = lean_ctor_get(x_24, 2); -lean_inc(x_25); -lean_dec_ref(x_24); -x_26 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_26, 0, x_2); -lean_ctor_set(x_26, 1, x_22); -x_27 = lean_box(0); -x_28 = l_Lean_PersistentEnvExtension_addEntry___redArg(x_23, x_1, x_26, x_25, x_27); -lean_dec(x_25); -x_29 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_29, 0, x_28); -return x_29; +x_25 = l_Lean_classExtension; +x_26 = lean_ctor_get(x_25, 0); +lean_inc_ref(x_26); +x_27 = lean_ctor_get(x_26, 2); +lean_inc(x_27); +lean_dec_ref(x_26); +x_28 = l_Lean_ConstantInfo_levelParams(x_6); +lean_dec(x_6); +x_29 = l___private_Lean_Class_0__Lean_computeOutLevelParams(x_9, x_24, x_28); +lean_dec(x_28); +x_30 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_30, 0, x_2); +lean_ctor_set(x_30, 1, x_24); +lean_ctor_set(x_30, 2, x_29); +x_31 = lean_box(0); +x_32 = l_Lean_PersistentEnvExtension_addEntry___redArg(x_25, x_1, x_30, x_27, x_31); +lean_dec(x_27); +x_33 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_33, 0, x_32); +return x_33; } } } } else { -lean_object* x_36; -x_36 = lean_ctor_get(x_4, 0); -lean_inc(x_36); +lean_object* x_40; +x_40 = lean_ctor_get(x_4, 0); +lean_inc(x_40); lean_dec(x_4); -switch (lean_obj_tag(x_36)) { +switch (lean_obj_tag(x_40)) { case 5: { -goto block_53; +goto block_59; } case 0: { -goto block_53; +goto block_59; } default: { if (x_3 == 0) { -lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; -lean_dec(x_36); -lean_dec_ref(x_1); -x_54 = l_Lean_addClass___closed__1; -x_55 = l_Lean_MessageData_ofConstName(x_2, x_3); -x_56 = lean_alloc_ctor(7, 2, 0); -lean_ctor_set(x_56, 0, x_54); -lean_ctor_set(x_56, 1, x_55); -x_57 = l_Lean_addClass___closed__3; -x_58 = lean_alloc_ctor(7, 2, 0); -lean_ctor_set(x_58, 0, x_56); -lean_ctor_set(x_58, 1, x_57); -x_59 = lean_alloc_ctor(0, 1, 0); -lean_ctor_set(x_59, 0, x_58); -return x_59; -} -else -{ -goto block_53; -} -} -} -block_53: -{ -lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; -x_37 = lean_unsigned_to_nat(0u); -x_38 = l_Lean_mkOutParamArgsImplicit___closed__0; -x_39 = l_Lean_ConstantInfo_type(x_36); -lean_dec(x_36); -x_40 = l___private_Lean_Class_0__Lean_checkOutParam(x_37, x_38, x_38, x_39); -if (lean_obj_tag(x_40) == 0) -{ -lean_object* x_41; lean_object* x_42; lean_object* x_43; -lean_dec(x_2); -lean_dec_ref(x_1); -x_41 = lean_ctor_get(x_40, 0); -lean_inc(x_41); -if (lean_is_exclusive(x_40)) { - lean_ctor_release(x_40, 0); - x_42 = x_40; -} else { - lean_dec_ref(x_40); - x_42 = lean_box(0); -} -if (lean_is_scalar(x_42)) { - x_43 = lean_alloc_ctor(0, 1, 0); -} else { - x_43 = x_42; -} -lean_ctor_set(x_43, 0, x_41); -return x_43; -} -else -{ -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; lean_object* x_51; lean_object* x_52; -x_44 = lean_ctor_get(x_40, 0); -lean_inc(x_44); -if (lean_is_exclusive(x_40)) { - lean_ctor_release(x_40, 0); - x_45 = x_40; -} else { - lean_dec_ref(x_40); - x_45 = lean_box(0); -} -x_46 = l_Lean_classExtension; -x_47 = lean_ctor_get(x_46, 0); -lean_inc_ref(x_47); -x_48 = lean_ctor_get(x_47, 2); -lean_inc(x_48); -lean_dec_ref(x_47); -x_49 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_49, 0, x_2); -lean_ctor_set(x_49, 1, x_44); -x_50 = lean_box(0); -x_51 = l_Lean_PersistentEnvExtension_addEntry___redArg(x_46, x_1, x_49, x_48, x_50); -lean_dec(x_48); -if (lean_is_scalar(x_45)) { - x_52 = lean_alloc_ctor(1, 1, 0); -} else { - x_52 = x_45; -} -lean_ctor_set(x_52, 0, x_51); -return x_52; -} -} -} -} -else -{ lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; -lean_dec(x_4); +lean_dec(x_40); lean_dec_ref(x_1); -x_60 = l_Lean_addClass___closed__5; -x_61 = l_Lean_MessageData_ofName(x_2); +x_60 = l_Lean_addClass___closed__1; +x_61 = l_Lean_MessageData_ofConstName(x_2, x_3); x_62 = lean_alloc_ctor(7, 2, 0); lean_ctor_set(x_62, 0, x_60); lean_ctor_set(x_62, 1, x_61); -x_63 = l_Lean_addClass___closed__7; +x_63 = l_Lean_addClass___closed__3; x_64 = lean_alloc_ctor(7, 2, 0); lean_ctor_set(x_64, 0, x_62); lean_ctor_set(x_64, 1, x_63); @@ -3591,13 +4048,91 @@ x_65 = lean_alloc_ctor(0, 1, 0); lean_ctor_set(x_65, 0, x_64); return x_65; } +else +{ +goto block_59; +} +} +} +block_59: +{ +lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; +x_41 = lean_unsigned_to_nat(0u); +x_42 = l_Lean_mkOutParamArgsImplicit___closed__0; +x_43 = l_Lean_ConstantInfo_type(x_40); +lean_inc_ref(x_43); +x_44 = l___private_Lean_Class_0__Lean_checkOutParam(x_41, x_42, x_42, x_43); +if (lean_obj_tag(x_44) == 0) +{ +lean_object* x_45; lean_object* x_46; lean_object* x_47; +lean_dec_ref(x_43); +lean_dec(x_40); +lean_dec(x_2); +lean_dec_ref(x_1); +x_45 = lean_ctor_get(x_44, 0); +lean_inc(x_45); +if (lean_is_exclusive(x_44)) { + lean_ctor_release(x_44, 0); + x_46 = x_44; +} else { + lean_dec_ref(x_44); + x_46 = lean_box(0); +} +if (lean_is_scalar(x_46)) { + x_47 = lean_alloc_ctor(0, 1, 0); +} else { + x_47 = x_46; +} +lean_ctor_set(x_47, 0, x_45); +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_object* x_56; lean_object* x_57; lean_object* x_58; +x_48 = lean_ctor_get(x_44, 0); +lean_inc(x_48); +if (lean_is_exclusive(x_44)) { + lean_ctor_release(x_44, 0); + x_49 = x_44; +} else { + lean_dec_ref(x_44); + x_49 = lean_box(0); +} +x_50 = l_Lean_classExtension; +x_51 = lean_ctor_get(x_50, 0); +lean_inc_ref(x_51); +x_52 = lean_ctor_get(x_51, 2); +lean_inc(x_52); +lean_dec_ref(x_51); +x_53 = l_Lean_ConstantInfo_levelParams(x_40); +lean_dec(x_40); +x_54 = l___private_Lean_Class_0__Lean_computeOutLevelParams(x_43, x_48, x_53); +lean_dec(x_53); +x_55 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_55, 0, x_2); +lean_ctor_set(x_55, 1, x_48); +lean_ctor_set(x_55, 2, x_54); +x_56 = lean_box(0); +x_57 = l_Lean_PersistentEnvExtension_addEntry___redArg(x_50, x_1, x_55, x_52, x_56); +lean_dec(x_52); +if (lean_is_scalar(x_49)) { + x_58 = lean_alloc_ctor(1, 1, 0); +} else { + x_58 = x_49; +} +lean_ctor_set(x_58, 0, x_57); +return x_58; +} +} +} } else { lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; +lean_dec(x_4); lean_dec_ref(x_1); -x_66 = l_Lean_addClass___closed__9; -x_67 = l_Lean_MessageData_ofConstName(x_2, x_3); +x_66 = l_Lean_addClass___closed__5; +x_67 = l_Lean_MessageData_ofName(x_2); x_68 = lean_alloc_ctor(7, 2, 0); lean_ctor_set(x_68, 0, x_66); lean_ctor_set(x_68, 1, x_67); @@ -3610,6 +4145,24 @@ lean_ctor_set(x_71, 0, x_70); return x_71; } } +else +{ +lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; +lean_dec_ref(x_1); +x_72 = l_Lean_addClass___closed__9; +x_73 = l_Lean_MessageData_ofConstName(x_2, x_3); +x_74 = lean_alloc_ctor(7, 2, 0); +lean_ctor_set(x_74, 0, x_72); +lean_ctor_set(x_74, 1, x_73); +x_75 = l_Lean_addClass___closed__7; +x_76 = lean_alloc_ctor(7, 2, 0); +lean_ctor_set(x_76, 0, x_74); +lean_ctor_set(x_76, 1, x_75); +x_77 = lean_alloc_ctor(0, 1, 0); +lean_ctor_set(x_77, 0, x_76); +return x_77; +} +} } static lean_object* _init_l_Lean_setEnv___at___00__private_Lean_Class_0__Lean_init_spec__2___redArg___closed__0() { _start: @@ -4255,6 +4808,7 @@ return x_2; } } lean_object* initialize_Lean_Attributes(uint8_t builtin); +lean_object* initialize_Lean_Util_CollectLevelParams(uint8_t builtin); static bool _G_initialized = false; LEAN_EXPORT lean_object* initialize_Lean_Class(uint8_t builtin) { lean_object * res; @@ -4263,6 +4817,9 @@ _G_initialized = true; res = initialize_Lean_Attributes(builtin); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +res = initialize_Lean_Util_CollectLevelParams(builtin); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); l_Lean_instInhabitedClassState_default___closed__0 = _init_l_Lean_instInhabitedClassState_default___closed__0(); lean_mark_persistent(l_Lean_instInhabitedClassState_default___closed__0); l_Lean_instInhabitedClassState_default___closed__1 = _init_l_Lean_instInhabitedClassState_default___closed__1(); @@ -4273,6 +4830,8 @@ l_Lean_instInhabitedClassState_default___closed__3 = _init_l_Lean_instInhabitedC lean_mark_persistent(l_Lean_instInhabitedClassState_default___closed__3); l_Lean_instInhabitedClassState_default___closed__4 = _init_l_Lean_instInhabitedClassState_default___closed__4(); lean_mark_persistent(l_Lean_instInhabitedClassState_default___closed__4); +l_Lean_instInhabitedClassState_default___closed__5 = _init_l_Lean_instInhabitedClassState_default___closed__5(); +lean_mark_persistent(l_Lean_instInhabitedClassState_default___closed__5); l_Lean_instInhabitedClassState_default = _init_l_Lean_instInhabitedClassState_default(); lean_mark_persistent(l_Lean_instInhabitedClassState_default); l_Lean_instInhabitedClassState = _init_l_Lean_instInhabitedClassState(); @@ -4289,6 +4848,8 @@ l_Lean_SMap_empty___at___00Lean_initFn_00___x40_Lean_Class_903839608____hygCtx__ lean_mark_persistent(l_Lean_SMap_empty___at___00Lean_initFn_00___x40_Lean_Class_903839608____hygCtx___hyg_2__spec__0___closed__2); l_Lean_initFn___lam__1___closed__0_00___x40_Lean_Class_903839608____hygCtx___hyg_2_ = _init_l_Lean_initFn___lam__1___closed__0_00___x40_Lean_Class_903839608____hygCtx___hyg_2_(); lean_mark_persistent(l_Lean_initFn___lam__1___closed__0_00___x40_Lean_Class_903839608____hygCtx___hyg_2_); +l_Lean_initFn___lam__1___closed__1_00___x40_Lean_Class_903839608____hygCtx___hyg_2_ = _init_l_Lean_initFn___lam__1___closed__1_00___x40_Lean_Class_903839608____hygCtx___hyg_2_(); +lean_mark_persistent(l_Lean_initFn___lam__1___closed__1_00___x40_Lean_Class_903839608____hygCtx___hyg_2_); if (builtin) {res = l_Lean_initFn_00___x40_Lean_Class_903839608____hygCtx___hyg_2_(); if (lean_io_result_is_error(res)) return res; l_Lean_classExtension = lean_io_result_get_value(res); @@ -4304,6 +4865,14 @@ l___private_Lean_Class_0__Lean_mkOutParamArgsImplicit_go___closed__5 = _init_l__ lean_mark_persistent(l___private_Lean_Class_0__Lean_mkOutParamArgsImplicit_go___closed__5); l_Lean_mkOutParamArgsImplicit___closed__0 = _init_l_Lean_mkOutParamArgsImplicit___closed__0(); lean_mark_persistent(l_Lean_mkOutParamArgsImplicit___closed__0); +l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__0 = _init_l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__0(); +lean_mark_persistent(l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__0); +l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__1 = _init_l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__1(); +lean_mark_persistent(l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__1); +l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__2 = _init_l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__2(); +lean_mark_persistent(l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__2); +l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__3 = _init_l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__3(); +lean_mark_persistent(l___private_Lean_Class_0__Lean_computeOutLevelParams___closed__3); l_Lean_addClass___closed__1 = _init_l_Lean_addClass___closed__1(); lean_mark_persistent(l_Lean_addClass___closed__1); l_Lean_addClass___closed__3 = _init_l_Lean_addClass___closed__3();