From cf2b6b80bb636ee70fae2ef0f2f2dce940befc67 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 24 Sep 2022 20:01:15 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/Lean/Compiler/LCNF/CompilerM.lean | 11 +- .../src/Lean/Compiler/LCNF/PrettyPrinter.lean | 11 +- stage0/src/Lean/Compiler/LCNF/Specialize.lean | 14 +- stage0/stdlib/Lean/Compiler/LCNF/CompilerM.c | 447 +++++++++++------- .../stdlib/Lean/Compiler/LCNF/PrettyPrinter.c | 84 +++- stage0/stdlib/Lean/Compiler/LCNF/Specialize.c | 218 +++++---- 6 files changed, 509 insertions(+), 276 deletions(-) diff --git a/stage0/src/Lean/Compiler/LCNF/CompilerM.lean b/stage0/src/Lean/Compiler/LCNF/CompilerM.lean index 9074e18fef..6c4c26b9e6 100644 --- a/stage0/src/Lean/Compiler/LCNF/CompilerM.lean +++ b/stage0/src/Lean/Compiler/LCNF/CompilerM.lean @@ -119,6 +119,10 @@ def eraseCodeDecl (decl : CodeDecl) : CompilerM Unit := do | .let decl => eraseLetDecl decl | .jp decl | .fun decl => eraseFunDecl decl +def eraseDecl (decl : Decl) : CompilerM Unit := do + eraseParams decl.params + eraseCode decl.value + /-- A free variable substitution. We use these substitutions when inlining definitions and "internalizing" LCNF code into `CompilerM`. @@ -148,6 +152,11 @@ expression to be `f xₙ xₙ`. We use this setting, for example, in the simplif private partial def normExprImp (s : FVarSubst) (e : Expr) (translator : Bool) : Expr := go e where + goApp (e : Expr) : Expr := + match e with + | .app f a => e.updateApp! (goApp f) (go a) + | _ => go e + go (e : Expr) : Expr := if e.hasFVar then match e with @@ -155,7 +164,7 @@ where | some e => if translator then e else go e | none => e | .lit .. | .const .. | .sort .. | .mvar .. | .bvar .. => e - | .app f a => e.updateApp! (go f) (go a) + | .app f a => e.updateApp! (goApp f) (go a) |>.headBeta | .mdata _ b => e.updateMData! (go b) | .proj _ _ b => e.updateProj! (go b) | .forallE _ d b _ => e.updateForallE! (go d) (go b) diff --git a/stage0/src/Lean/Compiler/LCNF/PrettyPrinter.lean b/stage0/src/Lean/Compiler/LCNF/PrettyPrinter.lean index cfeb703226..509e68f003 100644 --- a/stage0/src/Lean/Compiler/LCNF/PrettyPrinter.lean +++ b/stage0/src/Lean/Compiler/LCNF/PrettyPrinter.lean @@ -118,9 +118,18 @@ def ppFunDecl (decl : FunDecl) : CompilerM Format := /-- Similar to `ppDecl`, but in `CoreM`, and it does not assume `decl` has already been internalized. + +This function is used for debugging purposes. -/ def ppDecl' (decl : Decl) : CoreM Format := do - go |>.run {} + /- + We save/restore the state to make sure we do not affect the next free variable id. + -/ + let s ← get + try + go |>.run {} + finally + set s where go : CompilerM Format := do let decl ← decl.internalize diff --git a/stage0/src/Lean/Compiler/LCNF/Specialize.lean b/stage0/src/Lean/Compiler/LCNF/Specialize.lean index 1918d3b348..77973e81d2 100644 --- a/stage0/src/Lean/Compiler/LCNF/Specialize.lean +++ b/stage0/src/Lean/Compiler/LCNF/Specialize.lean @@ -295,9 +295,19 @@ Specialize `decl` using -/ def mkSpecDecl (decl : Decl) (us : List Level) (argMask : Array (Option Expr)) (params : Array Param) (decls : Array CodeDecl) (levelParamsNew : List Name) : SpecializeM Decl := do let nameNew := decl.name ++ `_at_ ++ (← read).declName ++ (`spec).appendIndexAfter (← get).decls.size - go nameNew |>.run' {} + /- + Recall that we have just retrieved `decl` using `getDecl?`, and it may have free variable identifiers that overlap with the free-variables + in `params` and `decls` (i.e., the "closure"). + Recall that `params` and `decls` are internalized, but `decl` is not. + Thus, we internalize `decl` before glueing these "pieces" together. We erase the internalized information after we are done. + -/ + let decl ← decl.internalize + try + go decl nameNew |>.run' {} + finally + eraseDecl decl where - go (nameNew : Name) : InternalizeM Decl := do + go (decl : Decl) (nameNew : Name) : InternalizeM Decl := do let mut params ← params.mapM internalizeParam let decls ← decls.mapM internalizeCodeDecl for param in decl.params, arg in argMask do diff --git a/stage0/stdlib/Lean/Compiler/LCNF/CompilerM.c b/stage0/stdlib/Lean/Compiler/LCNF/CompilerM.c index e4b1dda2e6..018193ff63 100644 --- a/stage0/stdlib/Lean/Compiler/LCNF/CompilerM.c +++ b/stage0/stdlib/Lean/Compiler/LCNF/CompilerM.c @@ -91,6 +91,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_modifyLCtx(lean_object*, uint8_t, lean_object* lean_array_get_size(lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normParams___at_Lean_Compiler_LCNF_normCodeImp___spec__6(uint8_t, uint8_t, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_string_append(lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_goApp___boxed(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normFunDecl(lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Decl_internalize(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normExpr___at_Lean_Compiler_LCNF_normCodeImp___spec__3___rarg(uint8_t, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); @@ -145,6 +146,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normParam___at_Lean_Compiler_LCNF_ LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_updateFunDeclImp___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_Array_BasicAux_0__mapMonoMImp_go___at_Lean_Compiler_LCNF_normFunDeclImp___spec__4(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_modify___at_Lean_Compiler_LCNF_Internalize_instMonadFVarSubstStateInternalizeM___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Expr_headBeta(lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normParam___rarg___lambda__1(lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___closed__4; static lean_object* l_Lean_Compiler_LCNF_getParam___closed__1; @@ -267,6 +269,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_instMonadFVarSubst(uint8_t, lean_o LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_normParams(lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Internalize_internalizeCode___spec__3(size_t, size_t, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Phase_toCtorIdx___boxed(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_findLetDecl_x3f(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_mkFreshFVarId___at_Lean_Compiler_LCNF_mkParam___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_addFVarSubst___rarg(lean_object*, lean_object*, lean_object*); @@ -275,10 +278,12 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_instMonadFVarSubstState___rarg(lea LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_getType(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_nat_mul(lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_Internalize_mkNewFVarId___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseDecl(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_getLetDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_getLetDecl___closed__1; LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Compiler_LCNF_mkParam___spec__2(uint8_t, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_goApp(lean_object*, uint8_t, lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_getLetDecl(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_LetDecl_updateValue___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_ReaderT_read___at_Lean_Compiler_LCNF_instMonadFVarSubstNormalizerM___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -2826,6 +2831,94 @@ lean_dec(x_3); return x_8; } } +LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseDecl(lean_object* x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +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, 3); +lean_inc(x_7); +x_8 = l_Lean_Compiler_LCNF_eraseParams(x_7, x_2, x_3, x_4, x_5, x_6); +lean_dec(x_7); +x_9 = lean_ctor_get(x_8, 1); +lean_inc(x_9); +lean_dec(x_8); +x_10 = lean_ctor_get(x_1, 4); +lean_inc(x_10); +lean_dec(x_1); +x_11 = l_Lean_Compiler_LCNF_eraseCode(x_10, x_2, x_3, x_4, x_5, x_9); +return x_11; +} +} +LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_eraseDecl___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { +_start: +{ +uint8_t x_7; lean_object* x_8; +x_7 = lean_unbox(x_2); +lean_dec(x_2); +x_8 = l_Lean_Compiler_LCNF_eraseDecl(x_1, x_7, x_3, x_4, x_5, x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +return x_8; +} +} +LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_goApp(lean_object* x_1, uint8_t x_2, lean_object* x_3) { +_start: +{ +if (lean_obj_tag(x_3) == 5) +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; size_t x_8; size_t x_9; uint8_t x_10; +x_4 = lean_ctor_get(x_3, 0); +lean_inc(x_4); +x_5 = lean_ctor_get(x_3, 1); +lean_inc(x_5); +lean_inc(x_4); +lean_inc(x_1); +x_6 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_goApp(x_1, x_2, x_4); +lean_inc(x_5); +x_7 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_5); +x_8 = lean_ptr_addr(x_4); +lean_dec(x_4); +x_9 = lean_ptr_addr(x_6); +x_10 = lean_usize_dec_eq(x_8, x_9); +if (x_10 == 0) +{ +lean_object* x_11; +lean_dec(x_5); +lean_dec(x_3); +x_11 = l_Lean_Expr_app___override(x_6, x_7); +return x_11; +} +else +{ +size_t x_12; size_t x_13; uint8_t x_14; +x_12 = lean_ptr_addr(x_5); +lean_dec(x_5); +x_13 = lean_ptr_addr(x_7); +x_14 = lean_usize_dec_eq(x_12, x_13); +if (x_14 == 0) +{ +lean_object* x_15; +lean_dec(x_3); +x_15 = l_Lean_Expr_app___override(x_6, x_7); +return x_15; +} +else +{ +lean_dec(x_7); +lean_dec(x_6); +return x_3; +} +} +} +else +{ +lean_object* x_16; +x_16 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_3); +return x_16; +} +} +} LEAN_EXPORT lean_object* l_Std_AssocList_find_x3f___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___spec__2(lean_object* x_1, lean_object* x_2) { _start: { @@ -2908,7 +3001,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___closed__1; x_2 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___closed__2; -x_3 = lean_unsigned_to_nat(163u); +x_3 = lean_unsigned_to_nat(172u); x_4 = lean_unsigned_to_nat(20u); x_5 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -2972,7 +3065,7 @@ x_11 = lean_ctor_get(x_3, 1); lean_inc(x_11); lean_inc(x_10); lean_inc(x_1); -x_12 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_10); +x_12 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_goApp(x_1, x_2, x_10); lean_inc(x_11); x_13 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_11); x_14 = lean_ptr_addr(x_10); @@ -2981,231 +3074,235 @@ x_15 = lean_ptr_addr(x_12); x_16 = lean_usize_dec_eq(x_14, x_15); if (x_16 == 0) { -lean_object* x_17; +lean_object* x_17; lean_object* x_18; lean_dec(x_11); lean_dec(x_3); x_17 = l_Lean_Expr_app___override(x_12, x_13); -return x_17; +x_18 = l_Lean_Expr_headBeta(x_17); +return x_18; } else { -size_t x_18; size_t x_19; uint8_t x_20; -x_18 = lean_ptr_addr(x_11); +size_t x_19; size_t x_20; uint8_t x_21; +x_19 = lean_ptr_addr(x_11); lean_dec(x_11); -x_19 = lean_ptr_addr(x_13); -x_20 = lean_usize_dec_eq(x_18, x_19); -if (x_20 == 0) +x_20 = lean_ptr_addr(x_13); +x_21 = lean_usize_dec_eq(x_19, x_20); +if (x_21 == 0) { -lean_object* x_21; +lean_object* x_22; lean_object* x_23; lean_dec(x_3); -x_21 = l_Lean_Expr_app___override(x_12, x_13); -return x_21; +x_22 = l_Lean_Expr_app___override(x_12, x_13); +x_23 = l_Lean_Expr_headBeta(x_22); +return x_23; } else { +lean_object* x_24; lean_dec(x_13); lean_dec(x_12); -return x_3; +x_24 = l_Lean_Expr_headBeta(x_3); +return x_24; } } } case 6: { -lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; size_t x_29; size_t x_30; uint8_t x_31; -x_22 = lean_ctor_get(x_3, 0); -lean_inc(x_22); -x_23 = lean_ctor_get(x_3, 1); -lean_inc(x_23); -x_24 = lean_ctor_get(x_3, 2); -lean_inc(x_24); -x_25 = lean_ctor_get_uint8(x_3, sizeof(void*)*3 + 8); +lean_object* x_25; lean_object* x_26; lean_object* x_27; uint8_t x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; size_t x_32; size_t x_33; uint8_t x_34; +x_25 = lean_ctor_get(x_3, 0); +lean_inc(x_25); +x_26 = lean_ctor_get(x_3, 1); +lean_inc(x_26); +x_27 = lean_ctor_get(x_3, 2); +lean_inc(x_27); +x_28 = lean_ctor_get_uint8(x_3, sizeof(void*)*3 + 8); lean_dec(x_3); -lean_inc(x_23); +lean_inc(x_26); lean_inc(x_1); -x_26 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_23); -lean_inc(x_24); -x_27 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_24); -lean_inc(x_24); -lean_inc(x_23); -lean_inc(x_22); -x_28 = l_Lean_Expr_lam___override(x_22, x_23, x_24, x_25); -x_29 = lean_ptr_addr(x_23); -lean_dec(x_23); -x_30 = lean_ptr_addr(x_26); -x_31 = lean_usize_dec_eq(x_29, x_30); -if (x_31 == 0) -{ -lean_object* x_32; -lean_dec(x_28); -lean_dec(x_24); -x_32 = l_Lean_Expr_lam___override(x_22, x_26, x_27, x_25); -return x_32; -} -else -{ -size_t x_33; size_t x_34; uint8_t x_35; -x_33 = lean_ptr_addr(x_24); -lean_dec(x_24); -x_34 = lean_ptr_addr(x_27); -x_35 = lean_usize_dec_eq(x_33, x_34); -if (x_35 == 0) -{ -lean_object* x_36; -lean_dec(x_28); -x_36 = l_Lean_Expr_lam___override(x_22, x_26, x_27, x_25); -return x_36; -} -else -{ -uint8_t x_37; -x_37 = l___private_Lean_Expr_0__Lean_beqBinderInfo____x40_Lean_Expr___hyg_390_(x_25, x_25); -if (x_37 == 0) -{ -lean_object* x_38; -lean_dec(x_28); -x_38 = l_Lean_Expr_lam___override(x_22, x_26, x_27, x_25); -return x_38; -} -else -{ -lean_dec(x_27); +x_29 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_26); +lean_inc(x_27); +x_30 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_27); +lean_inc(x_27); +lean_inc(x_26); +lean_inc(x_25); +x_31 = l_Lean_Expr_lam___override(x_25, x_26, x_27, x_28); +x_32 = lean_ptr_addr(x_26); lean_dec(x_26); -lean_dec(x_22); -return x_28; +x_33 = lean_ptr_addr(x_29); +x_34 = lean_usize_dec_eq(x_32, x_33); +if (x_34 == 0) +{ +lean_object* x_35; +lean_dec(x_31); +lean_dec(x_27); +x_35 = l_Lean_Expr_lam___override(x_25, x_29, x_30, x_28); +return x_35; +} +else +{ +size_t x_36; size_t x_37; uint8_t x_38; +x_36 = lean_ptr_addr(x_27); +lean_dec(x_27); +x_37 = lean_ptr_addr(x_30); +x_38 = lean_usize_dec_eq(x_36, x_37); +if (x_38 == 0) +{ +lean_object* x_39; +lean_dec(x_31); +x_39 = l_Lean_Expr_lam___override(x_25, x_29, x_30, x_28); +return x_39; +} +else +{ +uint8_t x_40; +x_40 = l___private_Lean_Expr_0__Lean_beqBinderInfo____x40_Lean_Expr___hyg_390_(x_28, x_28); +if (x_40 == 0) +{ +lean_object* x_41; +lean_dec(x_31); +x_41 = l_Lean_Expr_lam___override(x_25, x_29, x_30, x_28); +return x_41; +} +else +{ +lean_dec(x_30); +lean_dec(x_29); +lean_dec(x_25); +return x_31; } } } } case 7: { -lean_object* x_39; lean_object* x_40; lean_object* x_41; uint8_t x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; size_t x_46; size_t x_47; uint8_t x_48; -x_39 = lean_ctor_get(x_3, 0); -lean_inc(x_39); -x_40 = lean_ctor_get(x_3, 1); -lean_inc(x_40); -x_41 = lean_ctor_get(x_3, 2); -lean_inc(x_41); -x_42 = lean_ctor_get_uint8(x_3, sizeof(void*)*3 + 8); +lean_object* x_42; lean_object* x_43; lean_object* x_44; uint8_t x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; size_t x_49; size_t x_50; uint8_t x_51; +x_42 = lean_ctor_get(x_3, 0); +lean_inc(x_42); +x_43 = lean_ctor_get(x_3, 1); +lean_inc(x_43); +x_44 = lean_ctor_get(x_3, 2); +lean_inc(x_44); +x_45 = lean_ctor_get_uint8(x_3, sizeof(void*)*3 + 8); lean_dec(x_3); -lean_inc(x_40); +lean_inc(x_43); lean_inc(x_1); -x_43 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_40); -lean_inc(x_41); -x_44 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_41); -lean_inc(x_41); -lean_inc(x_40); -lean_inc(x_39); -x_45 = l_Lean_Expr_forallE___override(x_39, x_40, x_41, x_42); -x_46 = lean_ptr_addr(x_40); -lean_dec(x_40); -x_47 = lean_ptr_addr(x_43); -x_48 = lean_usize_dec_eq(x_46, x_47); -if (x_48 == 0) -{ -lean_object* x_49; -lean_dec(x_45); -lean_dec(x_41); -x_49 = l_Lean_Expr_forallE___override(x_39, x_43, x_44, x_42); -return x_49; -} -else -{ -size_t x_50; size_t x_51; uint8_t x_52; -x_50 = lean_ptr_addr(x_41); -lean_dec(x_41); -x_51 = lean_ptr_addr(x_44); -x_52 = lean_usize_dec_eq(x_50, x_51); -if (x_52 == 0) -{ -lean_object* x_53; -lean_dec(x_45); -x_53 = l_Lean_Expr_forallE___override(x_39, x_43, x_44, x_42); -return x_53; -} -else -{ -uint8_t x_54; -x_54 = l___private_Lean_Expr_0__Lean_beqBinderInfo____x40_Lean_Expr___hyg_390_(x_42, x_42); -if (x_54 == 0) -{ -lean_object* x_55; -lean_dec(x_45); -x_55 = l_Lean_Expr_forallE___override(x_39, x_43, x_44, x_42); -return x_55; -} -else -{ -lean_dec(x_44); +x_46 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_43); +lean_inc(x_44); +x_47 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_44); +lean_inc(x_44); +lean_inc(x_43); +lean_inc(x_42); +x_48 = l_Lean_Expr_forallE___override(x_42, x_43, x_44, x_45); +x_49 = lean_ptr_addr(x_43); lean_dec(x_43); -lean_dec(x_39); -return x_45; +x_50 = lean_ptr_addr(x_46); +x_51 = lean_usize_dec_eq(x_49, x_50); +if (x_51 == 0) +{ +lean_object* x_52; +lean_dec(x_48); +lean_dec(x_44); +x_52 = l_Lean_Expr_forallE___override(x_42, x_46, x_47, x_45); +return x_52; +} +else +{ +size_t x_53; size_t x_54; uint8_t x_55; +x_53 = lean_ptr_addr(x_44); +lean_dec(x_44); +x_54 = lean_ptr_addr(x_47); +x_55 = lean_usize_dec_eq(x_53, x_54); +if (x_55 == 0) +{ +lean_object* x_56; +lean_dec(x_48); +x_56 = l_Lean_Expr_forallE___override(x_42, x_46, x_47, x_45); +return x_56; +} +else +{ +uint8_t x_57; +x_57 = l___private_Lean_Expr_0__Lean_beqBinderInfo____x40_Lean_Expr___hyg_390_(x_45, x_45); +if (x_57 == 0) +{ +lean_object* x_58; +lean_dec(x_48); +x_58 = l_Lean_Expr_forallE___override(x_42, x_46, x_47, x_45); +return x_58; +} +else +{ +lean_dec(x_47); +lean_dec(x_46); +lean_dec(x_42); +return x_48; } } } } case 8: { -lean_object* x_56; lean_object* x_57; +lean_object* x_59; lean_object* x_60; lean_dec(x_3); lean_dec(x_1); -x_56 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___closed__4; -x_57 = l_panic___at_Lean_Expr_getRevArg_x21___spec__1(x_56); -return x_57; +x_59 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___closed__4; +x_60 = l_panic___at_Lean_Expr_getRevArg_x21___spec__1(x_59); +return x_60; } case 10: { -lean_object* x_58; lean_object* x_59; lean_object* x_60; size_t x_61; size_t x_62; uint8_t x_63; -x_58 = lean_ctor_get(x_3, 0); -lean_inc(x_58); -x_59 = lean_ctor_get(x_3, 1); -lean_inc(x_59); -lean_inc(x_59); -x_60 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_59); -x_61 = lean_ptr_addr(x_59); -lean_dec(x_59); -x_62 = lean_ptr_addr(x_60); -x_63 = lean_usize_dec_eq(x_61, x_62); -if (x_63 == 0) +lean_object* x_61; lean_object* x_62; lean_object* x_63; size_t x_64; size_t x_65; uint8_t x_66; +x_61 = lean_ctor_get(x_3, 0); +lean_inc(x_61); +x_62 = lean_ctor_get(x_3, 1); +lean_inc(x_62); +lean_inc(x_62); +x_63 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_62); +x_64 = lean_ptr_addr(x_62); +lean_dec(x_62); +x_65 = lean_ptr_addr(x_63); +x_66 = lean_usize_dec_eq(x_64, x_65); +if (x_66 == 0) { -lean_object* x_64; +lean_object* x_67; lean_dec(x_3); -x_64 = l_Lean_Expr_mdata___override(x_58, x_60); -return x_64; +x_67 = l_Lean_Expr_mdata___override(x_61, x_63); +return x_67; } else { -lean_dec(x_60); -lean_dec(x_58); +lean_dec(x_63); +lean_dec(x_61); return x_3; } } case 11: { -lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; size_t x_69; size_t x_70; uint8_t x_71; -x_65 = lean_ctor_get(x_3, 0); -lean_inc(x_65); -x_66 = lean_ctor_get(x_3, 1); -lean_inc(x_66); -x_67 = lean_ctor_get(x_3, 2); -lean_inc(x_67); -lean_inc(x_67); -x_68 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_67); -x_69 = lean_ptr_addr(x_67); -lean_dec(x_67); -x_70 = lean_ptr_addr(x_68); -x_71 = lean_usize_dec_eq(x_69, x_70); -if (x_71 == 0) +lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; size_t x_72; size_t x_73; uint8_t x_74; +x_68 = lean_ctor_get(x_3, 0); +lean_inc(x_68); +x_69 = lean_ctor_get(x_3, 1); +lean_inc(x_69); +x_70 = lean_ctor_get(x_3, 2); +lean_inc(x_70); +lean_inc(x_70); +x_71 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go(x_1, x_2, x_70); +x_72 = lean_ptr_addr(x_70); +lean_dec(x_70); +x_73 = lean_ptr_addr(x_71); +x_74 = lean_usize_dec_eq(x_72, x_73); +if (x_74 == 0) { -lean_object* x_72; +lean_object* x_75; lean_dec(x_3); -x_72 = l_Lean_Expr_proj___override(x_65, x_66, x_68); -return x_72; +x_75 = l_Lean_Expr_proj___override(x_68, x_69, x_71); +return x_75; } else { +lean_dec(x_71); +lean_dec(x_69); lean_dec(x_68); -lean_dec(x_66); -lean_dec(x_65); return x_3; } } @@ -3218,6 +3315,16 @@ return x_3; } } } +LEAN_EXPORT lean_object* l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_goApp___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint8_t x_4; lean_object* x_5; +x_4 = lean_unbox(x_2); +lean_dec(x_2); +x_5 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_goApp(x_1, x_4, x_3); +return x_5; +} +} LEAN_EXPORT lean_object* l_Std_AssocList_find_x3f___at___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___spec__2___boxed(lean_object* x_1, lean_object* x_2) { _start: { @@ -3325,7 +3432,7 @@ x_12 = l_Lean_Compiler_LCNF_getType___closed__3; x_13 = lean_string_append(x_11, x_12); x_14 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normExprImp_go___closed__1; x_15 = l___private_Lean_Compiler_LCNF_CompilerM_0__Lean_Compiler_LCNF_normFVarImp___closed__2; -x_16 = lean_unsigned_to_nat(182u); +x_16 = lean_unsigned_to_nat(191u); x_17 = lean_unsigned_to_nat(14u); x_18 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_14, x_15, x_16, x_17, x_13); lean_dec(x_13); diff --git a/stage0/stdlib/Lean/Compiler/LCNF/PrettyPrinter.c b/stage0/stdlib/Lean/Compiler/LCNF/PrettyPrinter.c index 6c4c42fd79..6eccbc1992 100644 --- a/stage0/stdlib/Lean/Compiler/LCNF/PrettyPrinter.c +++ b/stage0/stdlib/Lean/Compiler/LCNF/PrettyPrinter.c @@ -138,6 +138,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PP_run___rarg___boxed(lean_object* static lean_object* l_Lean_Compiler_LCNF_PP_ppExpr___closed__15; static lean_object* l_Lean_Compiler_LCNF_PP_ppExpr___closed__3; LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_PP_ppParam___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Expr_isFVar(lean_object*); static lean_object* l_Lean_Compiler_LCNF_PP_ppParam___closed__1; LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_ppFunDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -4071,13 +4072,82 @@ return x_3; LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_ppDecl_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { -lean_object* x_5; lean_object* x_6; uint8_t x_7; lean_object* x_8; -x_5 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_ppDecl_x27_go___boxed), 6, 1); -lean_closure_set(x_5, 0, x_1); -x_6 = l_Lean_Compiler_LCNF_ppDecl_x27___closed__2; -x_7 = 0; -x_8 = l_Lean_Compiler_LCNF_CompilerM_run___rarg(x_5, x_6, x_7, x_2, x_3, x_4); -return x_8; +lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; +x_5 = lean_st_ref_get(x_3, x_4); +x_6 = lean_ctor_get(x_5, 0); +lean_inc(x_6); +x_7 = lean_ctor_get(x_5, 1); +lean_inc(x_7); +lean_dec(x_5); +x_8 = lean_alloc_closure((void*)(l_Lean_Compiler_LCNF_ppDecl_x27_go___boxed), 6, 1); +lean_closure_set(x_8, 0, x_1); +x_9 = l_Lean_Compiler_LCNF_ppDecl_x27___closed__2; +x_10 = 0; +lean_inc(x_3); +x_11 = l_Lean_Compiler_LCNF_CompilerM_run___rarg(x_8, x_9, x_10, x_2, x_3, x_7); +if (lean_obj_tag(x_11) == 0) +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; uint8_t x_15; +x_12 = lean_ctor_get(x_11, 0); +lean_inc(x_12); +x_13 = lean_ctor_get(x_11, 1); +lean_inc(x_13); +lean_dec(x_11); +x_14 = lean_st_ref_set(x_3, x_6, x_13); +lean_dec(x_3); +x_15 = !lean_is_exclusive(x_14); +if (x_15 == 0) +{ +lean_object* x_16; +x_16 = lean_ctor_get(x_14, 0); +lean_dec(x_16); +lean_ctor_set(x_14, 0, x_12); +return x_14; +} +else +{ +lean_object* x_17; lean_object* x_18; +x_17 = lean_ctor_get(x_14, 1); +lean_inc(x_17); +lean_dec(x_14); +x_18 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_18, 0, x_12); +lean_ctor_set(x_18, 1, x_17); +return x_18; +} +} +else +{ +lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; +x_19 = lean_ctor_get(x_11, 0); +lean_inc(x_19); +x_20 = lean_ctor_get(x_11, 1); +lean_inc(x_20); +lean_dec(x_11); +x_21 = lean_st_ref_set(x_3, x_6, x_20); +lean_dec(x_3); +x_22 = !lean_is_exclusive(x_21); +if (x_22 == 0) +{ +lean_object* x_23; +x_23 = lean_ctor_get(x_21, 0); +lean_dec(x_23); +lean_ctor_set_tag(x_21, 1); +lean_ctor_set(x_21, 0, x_19); +return x_21; +} +else +{ +lean_object* x_24; lean_object* x_25; +x_24 = lean_ctor_get(x_21, 1); +lean_inc(x_24); +lean_dec(x_21); +x_25 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_25, 0, x_19); +lean_ctor_set(x_25, 1, x_24); +return x_25; +} +} } } lean_object* initialize_Init(uint8_t builtin, lean_object*); diff --git a/stage0/stdlib/Lean/Compiler/LCNF/Specialize.c b/stage0/stdlib/Lean/Compiler/LCNF/Specialize.c index b73b462305..bbd4264052 100644 --- a/stage0/stdlib/Lean/Compiler/LCNF/Specialize.c +++ b/stage0/stdlib/Lean/Compiler/LCNF/Specialize.c @@ -50,7 +50,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_shouldSpecialize(lean_o LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_Collector_collectCode(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_isTracingEnabledFor___at_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4874_(lean_object*); +LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4898_(lean_object*); lean_object* l_Lean_EnvExtensionInterfaceUnsafe_imp___elambda__2___rarg(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__3___closed__10; LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go___spec__2(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); @@ -72,6 +72,7 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_visitCode___boxed(lean_ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_Collector_State_params___default; lean_object* l_Lean_MessageData_ofList(lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Compiler_LCNF_Decl_internalize(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_getRemainingArgs___boxed(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Specialize_expandCodeDecls___spec__2___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_LCNF_Decl_instantiateValueLevelParams(lean_object*, lean_object*); @@ -99,7 +100,7 @@ LEAN_EXPORT lean_object* l_Lean_ForEachExpr_visit___at_Lean_Compiler_LCNF_Specia LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_specialize___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_specialize___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_specialize___closed__2; -static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4874____closed__1; +static lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4898____closed__1; static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__3___closed__13; LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_mkKey(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkAppN(lean_object*, lean_object*); @@ -259,6 +260,7 @@ lean_object* l_Array_ofSubarray___rarg(lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Decl_specialize___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Compiler_LCNF_Specialize_Collector_collectCode___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Compiler_LCNF_eraseDecl(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_Specialize_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_10____closed__3; lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__5___closed__8; @@ -7295,8 +7297,8 @@ if (x_40 == 0) { lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; x_41 = lean_ctor_get(x_15, 2); -x_42 = lean_ctor_get(x_1, 1); -x_43 = l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParams___spec__1(x_42, x_2, x_41); +x_42 = lean_ctor_get(x_2, 1); +x_43 = l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParams___spec__1(x_42, x_1, x_41); lean_ctor_set(x_15, 2, x_43); x_44 = l_Lean_Compiler_LCNF_Internalize_internalizeParam(x_15, x_7, x_8, x_9, x_10, x_11, x_12); x_45 = lean_ctor_get(x_44, 0); @@ -7323,8 +7325,8 @@ lean_inc(x_51); lean_inc(x_50); lean_inc(x_49); lean_dec(x_15); -x_53 = lean_ctor_get(x_1, 1); -x_54 = l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParams___spec__1(x_53, x_2, x_51); +x_53 = lean_ctor_get(x_2, 1); +x_54 = l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParams___spec__1(x_53, x_1, x_51); x_55 = lean_alloc_ctor(0, 3, 1); lean_ctor_set(x_55, 0, x_49); lean_ctor_set(x_55, 1, x_50); @@ -7415,8 +7417,8 @@ if (lean_is_exclusive(x_15)) { lean_dec_ref(x_15); x_85 = lean_box(0); } -x_86 = lean_ctor_get(x_1, 1); -x_87 = l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParams___spec__1(x_86, x_2, x_83); +x_86 = lean_ctor_get(x_2, 1); +x_87 = l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParams___spec__1(x_86, x_1, x_83); if (lean_is_scalar(x_85)) { x_88 = lean_alloc_ctor(0, 3, 1); } else { @@ -7557,8 +7559,8 @@ if (lean_is_exclusive(x_15)) { lean_dec_ref(x_15); x_127 = lean_box(0); } -x_128 = lean_ctor_get(x_1, 1); -x_129 = l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParams___spec__1(x_128, x_2, x_125); +x_128 = lean_ctor_get(x_2, 1); +x_129 = l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParams___spec__1(x_128, x_1, x_125); if (lean_is_scalar(x_127)) { x_130 = lean_alloc_ctor(0, 3, 1); } else { @@ -7680,8 +7682,8 @@ if (x_17 == 0) { 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; size_t x_25; size_t x_26; x_18 = lean_ctor_get(x_16, 2); -x_19 = lean_ctor_get(x_1, 1); -x_20 = l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParams___spec__1(x_19, x_2, x_18); +x_19 = lean_ctor_get(x_2, 1); +x_20 = l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParams___spec__1(x_19, x_1, x_18); lean_ctor_set(x_16, 2, x_20); x_21 = l_Lean_Compiler_LCNF_Internalize_internalizeParam(x_16, x_7, x_8, x_9, x_10, x_11, x_12); x_22 = lean_ctor_get(x_21, 0); @@ -7708,8 +7710,8 @@ lean_inc(x_30); lean_inc(x_29); lean_inc(x_28); lean_dec(x_16); -x_32 = lean_ctor_get(x_1, 1); -x_33 = l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParams___spec__1(x_32, x_2, x_30); +x_32 = lean_ctor_get(x_2, 1); +x_33 = l_Lean_Expr_instantiateLevelParamsCore_visit___at_Lean_Expr_instantiateLevelParams___spec__1(x_32, x_1, x_30); x_34 = lean_alloc_ctor(0, 3, 1); lean_ctor_set(x_34, 0, x_28); lean_ctor_set(x_34, 1, x_29); @@ -7736,37 +7738,37 @@ LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go(lean_obje _start: { lean_object* x_14; size_t x_15; size_t x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; size_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; lean_object* x_28; lean_object* x_29; lean_object* x_30; size_t x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; size_t x_38; lean_object* x_39; size_t x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; -x_14 = lean_array_get_size(x_4); +x_14 = lean_array_get_size(x_3); x_15 = lean_usize_of_nat(x_14); lean_dec(x_14); x_16 = 0; -x_17 = l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Internalize_internalizeFunDecl___spec__1(x_15, x_16, x_4, x_8, x_9, x_10, x_11, x_12, x_13); +x_17 = l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Internalize_internalizeFunDecl___spec__1(x_15, x_16, x_3, x_8, x_9, x_10, x_11, x_12, x_13); x_18 = lean_ctor_get(x_17, 0); lean_inc(x_18); x_19 = lean_ctor_get(x_17, 1); lean_inc(x_19); lean_dec(x_17); -x_20 = lean_array_get_size(x_5); +x_20 = lean_array_get_size(x_4); x_21 = lean_usize_of_nat(x_20); lean_dec(x_20); -x_22 = l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go___spec__1(x_21, x_16, x_5, x_8, x_9, x_10, x_11, x_12, x_19); +x_22 = l_Array_mapMUnsafe_map___at_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go___spec__1(x_21, x_16, x_4, x_8, x_9, x_10, x_11, x_12, x_19); x_23 = lean_ctor_get(x_22, 0); lean_inc(x_23); x_24 = lean_ctor_get(x_22, 1); lean_inc(x_24); lean_dec(x_22); -x_25 = lean_array_get_size(x_3); +x_25 = lean_array_get_size(x_2); x_26 = lean_unsigned_to_nat(0u); lean_inc(x_25); -x_27 = l_Array_toSubarray___rarg(x_3, x_26, x_25); -x_28 = lean_ctor_get(x_1, 3); +x_27 = l_Array_toSubarray___rarg(x_2, x_26, x_25); +x_28 = lean_ctor_get(x_6, 3); lean_inc(x_28); x_29 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_29, 0, x_27); lean_ctor_set(x_29, 1, x_18); x_30 = lean_array_get_size(x_28); x_31 = lean_usize_of_nat(x_30); -x_32 = l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go___spec__2(x_1, x_2, x_28, x_31, x_16, x_29, x_8, x_9, x_10, x_11, x_12, x_24); +x_32 = l_Array_forInUnsafe_loop___at_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go___spec__2(x_1, x_6, x_28, x_31, x_16, x_29, x_8, x_9, x_10, x_11, x_12, x_24); x_33 = lean_ctor_get(x_32, 0); lean_inc(x_33); x_34 = lean_ctor_get(x_32, 1); @@ -7784,14 +7786,14 @@ x_39 = lean_ctor_get(x_36, 1); lean_inc(x_39); x_40 = lean_usize_of_nat(x_39); lean_dec(x_39); -x_41 = l_Subarray_forInUnsafe_loop___at_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go___spec__3(x_1, x_2, x_36, x_38, x_40, x_35, x_8, x_9, x_10, x_11, x_12, x_34); +x_41 = l_Subarray_forInUnsafe_loop___at_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go___spec__3(x_1, x_6, x_36, x_38, x_40, x_35, x_8, x_9, x_10, x_11, x_12, x_34); lean_dec(x_36); x_42 = lean_ctor_get(x_41, 0); lean_inc(x_42); x_43 = lean_ctor_get(x_41, 1); lean_inc(x_43); lean_dec(x_41); -x_44 = l_Lean_Compiler_LCNF_Decl_instantiateValueLevelParams(x_1, x_2); +x_44 = l_Lean_Compiler_LCNF_Decl_instantiateValueLevelParams(x_6, x_1); x_45 = l_Lean_Compiler_LCNF_Internalize_internalizeCode(x_44, x_8, x_9, x_10, x_11, x_12, x_43); x_46 = lean_ctor_get(x_45, 0); lean_inc(x_46); @@ -7825,7 +7827,7 @@ lean_object* x_54; lean_object* x_55; lean_object* x_56; x_54 = lean_ctor_get(x_52, 0); x_55 = lean_alloc_ctor(0, 5, 0); lean_ctor_set(x_55, 0, x_7); -lean_ctor_set(x_55, 1, x_6); +lean_ctor_set(x_55, 1, x_5); lean_ctor_set(x_55, 2, x_54); lean_ctor_set(x_55, 3, x_42); lean_ctor_set(x_55, 4, x_48); @@ -7843,7 +7845,7 @@ lean_inc(x_57); lean_dec(x_52); x_59 = lean_alloc_ctor(0, 5, 0); lean_ctor_set(x_59, 0, x_7); -lean_ctor_set(x_59, 1, x_6); +lean_ctor_set(x_59, 1, x_5); lean_ctor_set(x_59, 2, x_57); lean_ctor_set(x_59, 3, x_42); lean_ctor_set(x_59, 4, x_48); @@ -7860,7 +7862,7 @@ uint8_t x_62; lean_dec(x_48); lean_dec(x_42); lean_dec(x_7); -lean_dec(x_6); +lean_dec(x_5); x_62 = !lean_is_exclusive(x_52); if (x_62 == 0) { @@ -7890,7 +7892,7 @@ lean_dec(x_12); lean_dec(x_11); lean_dec(x_10); lean_dec(x_7); -lean_dec(x_6); +lean_dec(x_5); x_66 = !lean_is_exclusive(x_49); if (x_66 == 0) { @@ -8022,7 +8024,7 @@ return x_3; LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_Specialize_mkSpecDecl(lean_object* x_1, lean_object* x_2, 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_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) { _start: { -lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; +lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; x_14 = lean_st_ref_get(x_12, x_13); x_15 = lean_ctor_get(x_14, 1); lean_inc(x_15); @@ -8049,77 +8051,103 @@ x_25 = l_Lean_Compiler_LCNF_Specialize_mkSpecDecl___closed__4; x_26 = lean_name_append_index_after(x_25, x_24); x_27 = l_Lean_Name_append(x_23, x_26); lean_dec(x_23); -x_28 = lean_st_ref_get(x_12, x_18); -x_29 = lean_ctor_get(x_28, 1); -lean_inc(x_29); -lean_dec(x_28); -x_30 = l_Lean_Compiler_LCNF_Specialize_Collector_collectExpr___closed__1; -x_31 = lean_st_mk_ref(x_30, x_29); -x_32 = lean_ctor_get(x_31, 0); -lean_inc(x_32); -x_33 = lean_ctor_get(x_31, 1); +x_28 = l_Lean_Compiler_LCNF_Specialize_Collector_collectExpr___closed__1; +x_29 = l_Lean_Compiler_LCNF_Decl_internalize(x_1, x_28, x_9, x_10, x_11, x_12, x_18); +x_30 = lean_ctor_get(x_29, 0); +lean_inc(x_30); +x_31 = lean_ctor_get(x_29, 1); +lean_inc(x_31); +lean_dec(x_29); +x_32 = lean_st_ref_get(x_12, x_31); +x_33 = lean_ctor_get(x_32, 1); lean_inc(x_33); -lean_dec(x_31); -lean_inc(x_12); -x_34 = l_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go(x_1, x_2, x_3, x_4, x_5, x_6, x_27, x_32, x_9, x_10, x_11, x_12, x_33); -if (lean_obj_tag(x_34) == 0) -{ -lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; uint8_t x_40; +lean_dec(x_32); +x_34 = lean_st_mk_ref(x_28, x_33); x_35 = lean_ctor_get(x_34, 0); lean_inc(x_35); x_36 = lean_ctor_get(x_34, 1); lean_inc(x_36); lean_dec(x_34); -x_37 = lean_st_ref_get(x_12, x_36); -lean_dec(x_12); -x_38 = lean_ctor_get(x_37, 1); +lean_inc(x_12); +lean_inc(x_11); +lean_inc(x_10); +lean_inc(x_30); +x_37 = l_Lean_Compiler_LCNF_Specialize_mkSpecDecl_go(x_2, x_3, x_4, x_5, x_6, x_30, x_27, x_35, x_9, x_10, x_11, x_12, x_36); +if (lean_obj_tag(x_37) == 0) +{ +lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; uint8_t x_45; +x_38 = lean_ctor_get(x_37, 0); lean_inc(x_38); +x_39 = lean_ctor_get(x_37, 1); +lean_inc(x_39); lean_dec(x_37); -x_39 = lean_st_ref_get(x_32, x_38); -lean_dec(x_32); -x_40 = !lean_is_exclusive(x_39); -if (x_40 == 0) -{ -lean_object* x_41; -x_41 = lean_ctor_get(x_39, 0); -lean_dec(x_41); -lean_ctor_set(x_39, 0, x_35); -return x_39; -} -else -{ -lean_object* x_42; lean_object* x_43; -x_42 = lean_ctor_get(x_39, 1); -lean_inc(x_42); -lean_dec(x_39); -x_43 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_43, 0, x_35); -lean_ctor_set(x_43, 1, x_42); -return x_43; -} -} -else -{ -uint8_t x_44; -lean_dec(x_32); +x_40 = lean_st_ref_get(x_12, x_39); +x_41 = lean_ctor_get(x_40, 1); +lean_inc(x_41); +lean_dec(x_40); +x_42 = lean_st_ref_get(x_35, x_41); +lean_dec(x_35); +x_43 = lean_ctor_get(x_42, 1); +lean_inc(x_43); +lean_dec(x_42); +x_44 = l_Lean_Compiler_LCNF_eraseDecl(x_30, x_9, x_10, x_11, x_12, x_43); lean_dec(x_12); -x_44 = !lean_is_exclusive(x_34); -if (x_44 == 0) +lean_dec(x_11); +lean_dec(x_10); +x_45 = !lean_is_exclusive(x_44); +if (x_45 == 0) { -return x_34; +lean_object* x_46; +x_46 = lean_ctor_get(x_44, 0); +lean_dec(x_46); +lean_ctor_set(x_44, 0, x_38); +return x_44; } else { -lean_object* x_45; lean_object* x_46; lean_object* x_47; -x_45 = lean_ctor_get(x_34, 0); -x_46 = lean_ctor_get(x_34, 1); -lean_inc(x_46); -lean_inc(x_45); -lean_dec(x_34); -x_47 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_47, 0, x_45); -lean_ctor_set(x_47, 1, x_46); -return x_47; +lean_object* x_47; lean_object* x_48; +x_47 = lean_ctor_get(x_44, 1); +lean_inc(x_47); +lean_dec(x_44); +x_48 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_48, 0, x_38); +lean_ctor_set(x_48, 1, x_47); +return x_48; +} +} +else +{ +lean_object* x_49; lean_object* x_50; lean_object* x_51; uint8_t x_52; +lean_dec(x_35); +x_49 = lean_ctor_get(x_37, 0); +lean_inc(x_49); +x_50 = lean_ctor_get(x_37, 1); +lean_inc(x_50); +lean_dec(x_37); +x_51 = l_Lean_Compiler_LCNF_eraseDecl(x_30, x_9, x_10, x_11, x_12, x_50); +lean_dec(x_12); +lean_dec(x_11); +lean_dec(x_10); +x_52 = !lean_is_exclusive(x_51); +if (x_52 == 0) +{ +lean_object* x_53; +x_53 = lean_ctor_get(x_51, 0); +lean_dec(x_53); +lean_ctor_set_tag(x_51, 1); +lean_ctor_set(x_51, 0, x_49); +return x_51; +} +else +{ +lean_object* x_54; lean_object* x_55; +x_54 = lean_ctor_get(x_51, 1); +lean_inc(x_54); +lean_dec(x_51); +x_55 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_55, 0, x_49); +lean_ctor_set(x_55, 1, x_54); +return x_55; } } } @@ -9352,7 +9380,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l_Lean_Compiler_LCNF_Specialize_Collector_collectFVar___closed__1; x_2 = l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__3___closed__11; -x_3 = lean_unsigned_to_nat(353u); +x_3 = lean_unsigned_to_nat(363u); x_4 = lean_unsigned_to_nat(4u); x_5 = l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__3___closed__10; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -9383,7 +9411,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l_Lean_Compiler_LCNF_Specialize_Collector_collectFVar___closed__1; x_2 = l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__3___closed__11; -x_3 = lean_unsigned_to_nat(352u); +x_3 = lean_unsigned_to_nat(362u); x_4 = lean_unsigned_to_nat(4u); x_5 = l_Lean_Compiler_LCNF_Specialize_specializeApp_x3f___lambda__3___closed__14; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -14041,7 +14069,7 @@ lean_dec(x_1); return x_8; } } -static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4874____closed__1() { +static lean_object* _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4898____closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -14051,7 +14079,7 @@ x_3 = l_Lean_Name_str___override(x_1, x_2); return x_3; } } -LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4874_(lean_object* x_1) { +LEAN_EXPORT lean_object* l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4898_(lean_object* x_1) { _start: { lean_object* x_2; uint8_t x_3; lean_object* x_4; @@ -14073,7 +14101,7 @@ lean_object* x_9; lean_object* x_10; lean_object* x_11; x_9 = lean_ctor_get(x_8, 1); lean_inc(x_9); lean_dec(x_8); -x_10 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4874____closed__1; +x_10 = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4898____closed__1; x_11 = l_Lean_registerTraceClass(x_10, x_7, x_9); return x_11; } @@ -14318,9 +14346,9 @@ l_Lean_Compiler_LCNF_specialize___closed__3 = _init_l_Lean_Compiler_LCNF_special lean_mark_persistent(l_Lean_Compiler_LCNF_specialize___closed__3); l_Lean_Compiler_LCNF_specialize = _init_l_Lean_Compiler_LCNF_specialize(); lean_mark_persistent(l_Lean_Compiler_LCNF_specialize); -l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4874____closed__1 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4874____closed__1(); -lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4874____closed__1); -res = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4874_(lean_io_mk_world()); +l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4898____closed__1 = _init_l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4898____closed__1(); +lean_mark_persistent(l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4898____closed__1); +res = l_Lean_Compiler_LCNF_initFn____x40_Lean_Compiler_LCNF_Specialize___hyg_4898_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); return lean_io_result_mk_ok(lean_box(0));