From 459ab7f4489529d3df24debf60e2b7223fb4bfe2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Sep 2019 10:55:21 -0700 Subject: [PATCH] chore(stage0): update --- src/stage0/init/control/combinators.c | 28 +- src/stage0/init/data/array/basic.c | 28 +- src/stage0/init/data/nat/bitwise.c | 32 +- src/stage0/init/data/option/basic.c | 60 +- .../init/data/persistenthashmap/basic.c | 76 +- src/stage0/init/lean/compiler/constfolding.c | 28 +- src/stage0/init/lean/compiler/inlineattrs.c | 84 +- src/stage0/init/lean/compiler/ir/borrow.c | 28 +- src/stage0/init/lean/compiler/ir/boxing.c | 718 ++++++++++-------- src/stage0/init/lean/compiler/ir/compilerm.c | 16 +- src/stage0/init/lean/compiler/ir/emitc.c | 28 +- src/stage0/init/lean/compiler/ir/emitutil.c | 58 +- src/stage0/init/lean/compiler/ir/livevars.c | 28 +- src/stage0/init/lean/compiler/ir/normids.c | 154 +--- src/stage0/init/lean/compiler/ir/resetreuse.c | 42 +- src/stage0/init/lean/compiler/specialize.c | 56 +- src/stage0/init/lean/elaborator/basic.c | 54 +- .../init/lean/elaborator/elabstrategyattrs.c | 70 +- src/stage0/init/lean/kvmap.c | 14 +- src/stage0/init/lean/localcontext.c | 62 +- src/stage0/init/lean/metavarcontext.c | 62 +- src/stage0/init/lean/parser/module.c | 40 +- src/stage0/init/lean/parser/term.c | 14 +- src/stage0/init/lean/reducibilityattrs.c | 70 +- 24 files changed, 580 insertions(+), 1270 deletions(-) diff --git a/src/stage0/init/control/combinators.c b/src/stage0/init/control/combinators.c index 27864b624c..348ef65c03 100644 --- a/src/stage0/init/control/combinators.c +++ b/src/stage0/init/control/combinators.c @@ -45,7 +45,6 @@ lean_object* l_List_mfor___main___boxed(lean_object*); lean_object* l_Nat_mfoldAux___main(lean_object*, lean_object*); lean_object* l_List_mfirst___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_mfoldr(lean_object*); -lean_object* l_List_mforall___main___rarg___boxed__const__1; lean_object* l_List_mfilter___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_mcond___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_when___rarg(lean_object*, lean_object*, uint8_t, lean_object*); @@ -55,7 +54,6 @@ lean_object* l_Nat_mfoldAux___main___boxed(lean_object*, lean_object*); lean_object* l_List_mmap___main___rarg___lambda__1(lean_object*, lean_object*); lean_object* l_List_mfoldl___main___boxed(lean_object*); lean_object* l_mwhen___rarg___lambda__1(lean_object*, lean_object*, uint8_t); -lean_object* l_List_mexists___main___rarg___boxed__const__1; lean_object* l_List_mfoldr___main(lean_object*); lean_object* l_List_mfoldl___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_mfirst___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1228,15 +1226,6 @@ return x_9; } } } -lean_object* _init_l_List_mexists___main___rarg___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_List_mexists___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { @@ -1251,7 +1240,7 @@ x_6 = lean_ctor_get(x_5, 1); lean_inc(x_6); lean_dec(x_5); x_7 = 0; -x_8 = l_List_mexists___main___rarg___boxed__const__1; +x_8 = lean_box(x_7); x_9 = lean_apply_2(x_6, lean_box(0), x_8); return x_9; } @@ -1354,15 +1343,6 @@ return x_9; } } } -lean_object* _init_l_List_mforall___main___rarg___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_List_mforall___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { @@ -1377,7 +1357,7 @@ x_6 = lean_ctor_get(x_5, 1); lean_inc(x_6); lean_dec(x_5); x_7 = 1; -x_8 = l_List_mforall___main___rarg___boxed__const__1; +x_8 = lean_box(x_7); x_9 = lean_apply_2(x_6, lean_box(0), x_8); return x_9; } @@ -1472,10 +1452,6 @@ l_mjoin___rarg___closed__1 = _init_l_mjoin___rarg___closed__1(); lean_mark_persistent(l_mjoin___rarg___closed__1); l_List_mmap___main___rarg___closed__1 = _init_l_List_mmap___main___rarg___closed__1(); lean_mark_persistent(l_List_mmap___main___rarg___closed__1); -l_List_mexists___main___rarg___boxed__const__1 = _init_l_List_mexists___main___rarg___boxed__const__1(); -lean_mark_persistent(l_List_mexists___main___rarg___boxed__const__1); -l_List_mforall___main___rarg___boxed__const__1 = _init_l_List_mforall___main___rarg___boxed__const__1(); -lean_mark_persistent(l_List_mforall___main___rarg___boxed__const__1); return w; } #ifdef __cplusplus diff --git a/src/stage0/init/data/array/basic.c b/src/stage0/init/data/array/basic.c index e92120fc6d..bb601c5a3a 100644 --- a/src/stage0/init/data/array/basic.c +++ b/src/stage0/init/data/array/basic.c @@ -149,7 +149,6 @@ lean_object* l_Array_miterate_u2082Aux___boxed(lean_object*, lean_object*); lean_object* l_Array_eraseIdx_x27___rarg___boxed(lean_object*, lean_object*); lean_object* l_Array_mmapIdx___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_iterate(lean_object*, lean_object*); -lean_object* l_Array_anyMAux___main___rarg___boxed__const__1; lean_object* l_Array_miterateAux___main___at_Array_mmap___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_mfindAux___boxed(lean_object*, lean_object*); lean_object* l_Array_mfor(lean_object*); @@ -332,7 +331,6 @@ lean_object* l_Array_mfindRevAux___main___rarg(lean_object*, lean_object*, lean_ lean_object* l_Array_feraseIdx___rarg(lean_object*, lean_object*); lean_object* l_Array_HasToString___rarg(lean_object*); lean_object* l___private_init_data_array_basic_2__revIterateAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Array_anyMAux___main___at_Array_allM___spec__1___rarg___boxed__const__1; lean_object* l_Array_miterateAux___main___at_Array_mfoldl___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_reverse___rarg(lean_object*); lean_object* l_Array_mfor___boxed(lean_object*); @@ -2347,15 +2345,6 @@ return x_12; } } } -lean_object* _init_l_Array_anyMAux___main___rarg___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Array_anyMAux___main___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { @@ -2376,7 +2365,7 @@ x_8 = lean_ctor_get(x_7, 1); lean_inc(x_8); lean_dec(x_7); x_9 = 0; -x_10 = l_Array_anyMAux___main___rarg___boxed__const__1; +x_10 = lean_box(x_9); x_11 = lean_apply_2(x_8, lean_box(0), x_10); return x_11; } @@ -2507,15 +2496,6 @@ return x_14; } } } -lean_object* _init_l_Array_anyMAux___main___at_Array_allM___spec__1___rarg___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Array_anyMAux___main___at_Array_allM___spec__1___rarg(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: { @@ -2538,7 +2518,7 @@ x_10 = lean_ctor_get(x_9, 1); lean_inc(x_10); lean_dec(x_9); x_11 = 0; -x_12 = l_Array_anyMAux___main___at_Array_allM___spec__1___rarg___boxed__const__1; +x_12 = lean_box(x_11); x_13 = lean_apply_2(x_10, lean_box(0), x_12); return x_13; } @@ -4963,10 +4943,6 @@ w = initialize_init_util(w); if (lean_io_result_is_error(w)) return w; l_Array_empty___closed__1 = _init_l_Array_empty___closed__1(); lean_mark_persistent(l_Array_empty___closed__1); -l_Array_anyMAux___main___rarg___boxed__const__1 = _init_l_Array_anyMAux___main___rarg___boxed__const__1(); -lean_mark_persistent(l_Array_anyMAux___main___rarg___boxed__const__1); -l_Array_anyMAux___main___at_Array_allM___spec__1___rarg___boxed__const__1 = _init_l_Array_anyMAux___main___at_Array_allM___spec__1___rarg___boxed__const__1(); -lean_mark_persistent(l_Array_anyMAux___main___at_Array_allM___spec__1___rarg___boxed__const__1); l_Array_allM___rarg___closed__1 = _init_l_Array_allM___rarg___closed__1(); lean_mark_persistent(l_Array_allM___rarg___closed__1); l_Array_HasRepr___rarg___closed__1 = _init_l_Array_HasRepr___rarg___closed__1(); diff --git a/src/stage0/init/data/nat/bitwise.c b/src/stage0/init/data/nat/bitwise.c index 64f5316998..b8554bcbdb 100644 --- a/src/stage0/init/data/nat/bitwise.c +++ b/src/stage0/init/data/nat/bitwise.c @@ -15,9 +15,7 @@ extern "C" { #endif lean_object* l_Nat_bitwise___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Nat_bitwise___main(lean_object*, lean_object*, lean_object*); -lean_object* l_Nat_bitwise___main___boxed__const__1; lean_object* l_Nat_bitwise___main___boxed(lean_object*, lean_object*, lean_object*); -lean_object* l_Nat_bitwise___main___boxed__const__2; lean_object* lean_nat_mod(lean_object*, lean_object*); lean_object* lean_nat_add(lean_object*, lean_object*); lean_object* l_Nat_land___boxed(lean_object*, lean_object*); @@ -27,24 +25,6 @@ lean_object* lean_nat_land(lean_object*, lean_object*); lean_object* l_Nat_lor___boxed(lean_object*, lean_object*); lean_object* lean_nat_div(lean_object*, lean_object*); lean_object* lean_nat_lor(lean_object*, lean_object*); -lean_object* _init_l_Nat_bitwise___main___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l_Nat_bitwise___main___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Nat_bitwise___main(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -99,8 +79,8 @@ else uint8_t x_23; uint8_t x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; uint8_t x_28; x_23 = 1; x_24 = 0; -x_25 = l_Nat_bitwise___main___boxed__const__1; -x_26 = l_Nat_bitwise___main___boxed__const__2; +x_25 = lean_box(x_23); +x_26 = lean_box(x_24); x_27 = lean_apply_2(x_1, x_25, x_26); x_28 = lean_unbox(x_27); lean_dec(x_27); @@ -122,8 +102,8 @@ else uint8_t x_30; uint8_t x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; uint8_t x_35; x_30 = 0; x_31 = 1; -x_32 = l_Nat_bitwise___main___boxed__const__2; -x_33 = l_Nat_bitwise___main___boxed__const__1; +x_32 = lean_box(x_30); +x_33 = lean_box(x_31); x_34 = lean_apply_2(x_1, x_32, x_33); x_35 = lean_unbox(x_34); lean_dec(x_34); @@ -199,10 +179,6 @@ w = initialize_init_data_nat_div(w); if (lean_io_result_is_error(w)) return w; w = initialize_init_coe(w); if (lean_io_result_is_error(w)) return w; -l_Nat_bitwise___main___boxed__const__1 = _init_l_Nat_bitwise___main___boxed__const__1(); -lean_mark_persistent(l_Nat_bitwise___main___boxed__const__1); -l_Nat_bitwise___main___boxed__const__2 = _init_l_Nat_bitwise___main___boxed__const__2(); -lean_mark_persistent(l_Nat_bitwise___main___boxed__const__2); return w; } #ifdef __cplusplus diff --git a/src/stage0/init/data/option/basic.c b/src/stage0/init/data/option/basic.c index 63e1b0af4f..1de1c351cb 100644 --- a/src/stage0/init/data/option/basic.c +++ b/src/stage0/init/data/option/basic.c @@ -32,11 +32,8 @@ lean_object* l_Option_decidableRelLt___boxed(lean_object*, lean_object*); lean_object* l_Option_Monad___lambda__2(lean_object*, lean_object*); lean_object* l_Option_bind___rarg(lean_object*, lean_object*); lean_object* l_Option_Monad___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Option_HasBeq___rarg___boxed__const__1; lean_object* l_Option_isNone___rarg___boxed(lean_object*); lean_object* l_Option_Monad___closed__1; -lean_object* l_Option_HasBeq___rarg___boxed__const__2; -lean_object* l_Option_decidableRelLt___rarg___boxed__const__2; lean_object* l_Option_toMonad___boxed(lean_object*, lean_object*); lean_object* l_Option_map___rarg(lean_object*, lean_object*); lean_object* l_Option_orelse___rarg___boxed(lean_object*, lean_object*); @@ -45,7 +42,6 @@ lean_object* l_Option_Monad___lambda__1(lean_object*, lean_object*, lean_object* uint8_t l_Option_toBool___rarg(lean_object*); lean_object* l_Option_HasBeq___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Option_toMonad___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_Option_decidableRelLt___rarg___boxed__const__1; lean_object* l_Option_HasLess(lean_object*, lean_object*); lean_object* l_Option_Monad___closed__2; lean_object* l_Option_Alternative___lambda__1(lean_object*); @@ -757,24 +753,6 @@ lean_dec(x_2); return x_4; } } -lean_object* _init_l_Option_decidableRelLt___rarg___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l_Option_decidableRelLt___rarg___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Option_decidableRelLt___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -785,7 +763,7 @@ if (lean_obj_tag(x_3) == 0) { uint8_t x_4; lean_object* x_5; x_4 = 0; -x_5 = l_Option_decidableRelLt___rarg___boxed__const__1; +x_5 = lean_box(x_4); return x_5; } else @@ -793,7 +771,7 @@ else uint8_t x_6; lean_object* x_7; lean_dec(x_3); x_6 = 1; -x_7 = l_Option_decidableRelLt___rarg___boxed__const__2; +x_7 = lean_box(x_6); return x_7; } } @@ -805,7 +783,7 @@ uint8_t x_8; lean_object* x_9; lean_dec(x_2); lean_dec(x_1); x_8 = 0; -x_9 = l_Option_decidableRelLt___rarg___boxed__const__1; +x_9 = lean_box(x_8); return x_9; } else @@ -923,24 +901,6 @@ x_5 = lean_box(x_4); return x_5; } } -lean_object* _init_l_Option_HasBeq___rarg___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l_Option_HasBeq___rarg___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Option_HasBeq___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -951,7 +911,7 @@ if (lean_obj_tag(x_3) == 0) { uint8_t x_4; lean_object* x_5; x_4 = 1; -x_5 = l_Option_HasBeq___rarg___boxed__const__1; +x_5 = lean_box(x_4); return x_5; } else @@ -959,7 +919,7 @@ else uint8_t x_6; lean_object* x_7; lean_dec(x_3); x_6 = 0; -x_7 = l_Option_HasBeq___rarg___boxed__const__2; +x_7 = lean_box(x_6); return x_7; } } @@ -971,7 +931,7 @@ uint8_t x_8; lean_object* x_9; lean_dec(x_2); lean_dec(x_1); x_8 = 0; -x_9 = l_Option_HasBeq___rarg___boxed__const__2; +x_9 = lean_box(x_8); return x_9; } else @@ -1061,14 +1021,6 @@ l_Option_Alternative___closed__3 = _init_l_Option_Alternative___closed__3(); lean_mark_persistent(l_Option_Alternative___closed__3); l_Option_Alternative = _init_l_Option_Alternative(); lean_mark_persistent(l_Option_Alternative); -l_Option_decidableRelLt___rarg___boxed__const__1 = _init_l_Option_decidableRelLt___rarg___boxed__const__1(); -lean_mark_persistent(l_Option_decidableRelLt___rarg___boxed__const__1); -l_Option_decidableRelLt___rarg___boxed__const__2 = _init_l_Option_decidableRelLt___rarg___boxed__const__2(); -lean_mark_persistent(l_Option_decidableRelLt___rarg___boxed__const__2); -l_Option_HasBeq___rarg___boxed__const__1 = _init_l_Option_HasBeq___rarg___boxed__const__1(); -lean_mark_persistent(l_Option_HasBeq___rarg___boxed__const__1); -l_Option_HasBeq___rarg___boxed__const__2 = _init_l_Option_HasBeq___rarg___boxed__const__2(); -lean_mark_persistent(l_Option_HasBeq___rarg___boxed__const__2); return w; } #ifdef __cplusplus diff --git a/src/stage0/init/data/persistenthashmap/basic.c b/src/stage0/init/data/persistenthashmap/basic.c index 9d73798492..e8ab5ad5f4 100644 --- a/src/stage0/init/data/persistenthashmap/basic.c +++ b/src/stage0/init/data/persistenthashmap/basic.c @@ -37,7 +37,6 @@ size_t l_USize_shift__right(size_t, size_t); lean_object* l_PersistentHashMap_contains(lean_object*, lean_object*); lean_object* l_PersistentHashMap_findAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_PersistentHashMap_insert___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2; lean_object* l_Array_miterateAux___main___at_PersistentHashMap_foldl___spec__3(lean_object*, lean_object*, lean_object*); lean_object* l_PersistentHashMap_mfoldlAux___main___at_PersistentHashMap_foldl___spec__2(lean_object*, lean_object*, lean_object*); lean_object* l_PersistentHashMap_mfoldl___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -87,7 +86,6 @@ lean_object* l_PersistentHashMap_insertAux___main___rarg___boxed(lean_object*, l lean_object* l_PersistentHashMap_mod2Shift___boxed(lean_object*, lean_object*); lean_object* l_Array_miterateAux___main___at_PersistentHashMap_insertAux___main___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_PersistentHashMap_containsAux___rarg(lean_object*, lean_object*, size_t, lean_object*); -lean_object* l_PersistentHashMap_containsAux___main___rarg___boxed__const__1; lean_object* l_PersistentHashMap_contains___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_PersistentHashMap_foldl___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* lean_string_append(lean_object*, lean_object*); @@ -129,7 +127,6 @@ lean_object* l_PersistentHashMap_empty___closed__2; lean_object* l_Array_miterateAux___main___at_PersistentHashMap_toList___spec__3(lean_object*, lean_object*); lean_object* l_PersistentHashMap_HasToString; size_t l_PersistentHashMap_shift; -lean_object* l_PersistentHashMap_eraseAux___main___rarg___boxed__const__1; size_t l_PersistentHashMap_insertAux___main___rarg___closed__2; lean_object* l_PersistentHashMap_mfoldlAux___main___at_PersistentHashMap_foldl___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Array_miterateAux___main___at_PersistentHashMap_mfoldlAux___main___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1495,15 +1492,6 @@ x_8 = lean_box(x_7); return x_8; } } -lean_object* _init_l_PersistentHashMap_containsAux___main___rarg___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_PersistentHashMap_containsAux___main___rarg(lean_object* x_1, lean_object* x_2, size_t x_3, lean_object* x_4) { _start: { @@ -1545,7 +1533,7 @@ uint8_t x_17; lean_object* x_18; lean_dec(x_4); lean_dec(x_1); x_17 = 0; -x_18 = l_PersistentHashMap_containsAux___main___rarg___boxed__const__1; +x_18 = lean_box(x_17); return x_18; } } @@ -1810,24 +1798,6 @@ lean_dec(x_1); return x_2; } } -lean_object* _init_l_PersistentHashMap_eraseAux___main___rarg___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_PersistentHashMap_eraseAux___main___rarg(lean_object* x_1, lean_object* x_2, size_t x_3, lean_object* x_4) { _start: { @@ -1858,7 +1828,7 @@ uint8_t x_15; lean_object* x_16; lean_object* x_17; lean_dec(x_9); lean_dec(x_5); x_15 = 0; -x_16 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__1; +x_16 = lean_box(x_15); x_17 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_17, 0, x_2); lean_ctor_set(x_17, 1, x_16); @@ -1877,7 +1847,7 @@ x_20 = lean_array_set(x_5, x_9, x_10); lean_dec(x_9); lean_ctor_set(x_2, 0, x_20); x_21 = 1; -x_22 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2; +x_22 = lean_box(x_21); x_23 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_23, 0, x_2); lean_ctor_set(x_23, 1, x_22); @@ -1892,7 +1862,7 @@ lean_dec(x_9); x_25 = lean_alloc_ctor(0, 1, 0); lean_ctor_set(x_25, 0, x_24); x_26 = 1; -x_27 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2; +x_27 = lean_box(x_26); x_28 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_28, 0, x_25); lean_ctor_set(x_28, 1, x_27); @@ -1930,7 +1900,7 @@ lean_dec(x_37); x_38 = lean_ctor_get(x_33, 0); lean_dec(x_38); x_39 = 0; -x_40 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__1; +x_40 = lean_box(x_39); lean_ctor_set(x_33, 1, x_40); lean_ctor_set(x_33, 0, x_2); return x_33; @@ -1940,7 +1910,7 @@ else uint8_t x_41; lean_object* x_42; lean_object* x_43; lean_dec(x_33); x_41 = 0; -x_42 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__1; +x_42 = lean_box(x_41); x_43 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_43, 0, x_2); lean_ctor_set(x_43, 1, x_42); @@ -1972,7 +1942,7 @@ x_50 = lean_array_set(x_31, x_9, x_11); lean_dec(x_9); lean_ctor_set(x_2, 0, x_50); x_51 = 1; -x_52 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2; +x_52 = lean_box(x_51); lean_ctor_set(x_33, 1, x_52); lean_ctor_set(x_33, 0, x_2); return x_33; @@ -1999,7 +1969,7 @@ x_58 = lean_array_set(x_31, x_9, x_57); lean_dec(x_9); lean_ctor_set(x_2, 0, x_58); x_59 = 1; -x_60 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2; +x_60 = lean_box(x_59); lean_ctor_set(x_53, 1, x_60); lean_ctor_set(x_53, 0, x_2); return x_53; @@ -2019,7 +1989,7 @@ x_64 = lean_array_set(x_31, x_9, x_63); lean_dec(x_9); lean_ctor_set(x_2, 0, x_64); x_65 = 1; -x_66 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2; +x_66 = lean_box(x_65); x_67 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_67, 0, x_2); lean_ctor_set(x_67, 1, x_66); @@ -2042,7 +2012,7 @@ x_70 = lean_array_set(x_31, x_9, x_11); lean_dec(x_9); lean_ctor_set(x_2, 0, x_70); x_71 = 1; -x_72 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2; +x_72 = lean_box(x_71); x_73 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_73, 0, x_2); lean_ctor_set(x_73, 1, x_72); @@ -2075,7 +2045,7 @@ x_79 = lean_array_set(x_31, x_9, x_78); lean_dec(x_9); lean_ctor_set(x_2, 0, x_79); x_80 = 1; -x_81 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2; +x_81 = lean_box(x_80); if (lean_is_scalar(x_77)) { x_82 = lean_alloc_ctor(0, 2, 0); } else { @@ -2111,7 +2081,7 @@ lean_dec(x_9); x_87 = lean_alloc_ctor(0, 1, 0); lean_ctor_set(x_87, 0, x_86); x_88 = 1; -x_89 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2; +x_89 = lean_box(x_88); if (lean_is_scalar(x_84)) { x_90 = lean_alloc_ctor(0, 2, 0); } else { @@ -2150,7 +2120,7 @@ lean_dec(x_9); x_97 = lean_alloc_ctor(0, 1, 0); lean_ctor_set(x_97, 0, x_96); x_98 = 1; -x_99 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2; +x_99 = lean_box(x_98); if (lean_is_scalar(x_94)) { x_100 = lean_alloc_ctor(0, 2, 0); } else { @@ -2190,7 +2160,7 @@ if (lean_is_exclusive(x_104)) { x_107 = lean_box(0); } x_108 = 0; -x_109 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__1; +x_109 = lean_box(x_108); if (lean_is_scalar(x_107)) { x_110 = lean_alloc_ctor(0, 2, 0); } else { @@ -2235,7 +2205,7 @@ if (lean_is_scalar(x_111)) { } lean_ctor_set(x_117, 0, x_116); x_118 = 1; -x_119 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2; +x_119 = lean_box(x_118); if (lean_is_scalar(x_113)) { x_120 = lean_alloc_ctor(0, 2, 0); } else { @@ -2277,7 +2247,7 @@ if (lean_is_scalar(x_111)) { } lean_ctor_set(x_127, 0, x_126); x_128 = 1; -x_129 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2; +x_129 = lean_box(x_128); if (lean_is_scalar(x_124)) { x_130 = lean_alloc_ctor(0, 2, 0); } else { @@ -2298,7 +2268,7 @@ lean_dec(x_5); lean_dec(x_4); lean_dec(x_1); x_131 = 0; -x_132 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__1; +x_132 = lean_box(x_131); x_133 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_133, 0, x_2); lean_ctor_set(x_133, 1, x_132); @@ -2321,7 +2291,7 @@ uint8_t x_138; lean_object* x_139; lean_object* x_140; lean_dec(x_135); lean_dec(x_134); x_138 = 0; -x_139 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__1; +x_139 = lean_box(x_138); x_140 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_140, 0, x_2); lean_ctor_set(x_140, 1, x_139); @@ -2347,7 +2317,7 @@ lean_dec(x_144); lean_ctor_set(x_2, 1, x_146); lean_ctor_set(x_2, 0, x_145); x_147 = 1; -x_148 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2; +x_148 = lean_box(x_147); x_149 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_149, 0, x_2); lean_ctor_set(x_149, 1, x_148); @@ -2367,7 +2337,7 @@ x_153 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_153, 0, x_151); lean_ctor_set(x_153, 1, x_152); x_154 = 1; -x_155 = l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2; +x_155 = lean_box(x_154); x_156 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_156, 0, x_153); lean_ctor_set(x_156, 1, x_155); @@ -3651,12 +3621,6 @@ l_PersistentHashMap_insertAux___main___rarg___closed__1 = _init_l_PersistentHash l_PersistentHashMap_insertAux___main___rarg___closed__2 = _init_l_PersistentHashMap_insertAux___main___rarg___closed__2(); l_PersistentHashMap_insertAux___main___rarg___closed__3 = _init_l_PersistentHashMap_insertAux___main___rarg___closed__3(); lean_mark_persistent(l_PersistentHashMap_insertAux___main___rarg___closed__3); -l_PersistentHashMap_containsAux___main___rarg___boxed__const__1 = _init_l_PersistentHashMap_containsAux___main___rarg___boxed__const__1(); -lean_mark_persistent(l_PersistentHashMap_containsAux___main___rarg___boxed__const__1); -l_PersistentHashMap_eraseAux___main___rarg___boxed__const__1 = _init_l_PersistentHashMap_eraseAux___main___rarg___boxed__const__1(); -lean_mark_persistent(l_PersistentHashMap_eraseAux___main___rarg___boxed__const__1); -l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2 = _init_l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2(); -lean_mark_persistent(l_PersistentHashMap_eraseAux___main___rarg___boxed__const__2); l_PersistentHashMap_stats___rarg___closed__1 = _init_l_PersistentHashMap_stats___rarg___closed__1(); lean_mark_persistent(l_PersistentHashMap_stats___rarg___closed__1); l_PersistentHashMap_Stats_toString___closed__1 = _init_l_PersistentHashMap_Stats_toString___closed__1(); diff --git a/src/stage0/init/lean/compiler/constfolding.c b/src/stage0/init/lean/compiler/constfolding.c index 2c89b741e4..da4b91b502 100644 --- a/src/stage0/init/lean/compiler/constfolding.c +++ b/src/stage0/init/lean/compiler/constfolding.c @@ -135,7 +135,6 @@ lean_object* l_Lean_Compiler_isOfNat___boxed(lean_object*); lean_object* l_Lean_Compiler_foldCharOfNat___closed__1; lean_object* l_Lean_Compiler_findUnFoldFn(lean_object*); lean_object* l_Lean_Compiler_foldNatAdd___rarg(lean_object*, lean_object*); -lean_object* l_Lean_Compiler_getBoolLit___closed__5___boxed__const__1; lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__6; lean_object* l_Lean_Compiler_boolFoldFns___closed__7; lean_object* lean_string_append(lean_object*, lean_object*); @@ -315,7 +314,6 @@ lean_object* l_Lean_Compiler_foldNatMul___rarg___boxed(lean_object*, lean_object lean_object* l_Lean_Compiler_mkNatEq___closed__7; lean_object* l_Lean_Compiler_numScalarTypes___closed__28; lean_object* l_Lean_Compiler_mkNatEq___closed__4; -lean_object* l_Lean_Compiler_getBoolLit___closed__6___boxed__const__1; extern lean_object* l_Bool_HasRepr___closed__1; lean_object* l_Lean_Compiler_foldUIntSub(uint8_t, lean_object*, lean_object*); extern lean_object* l_Nat_HasAdd___closed__1; @@ -3001,41 +2999,23 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Compiler_getBoolLit___closed__5___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_Compiler_getBoolLit___closed__5() { _start: { uint8_t x_1; lean_object* x_2; lean_object* x_3; x_1 = 0; -x_2 = l_Lean_Compiler_getBoolLit___closed__5___boxed__const__1; +x_2 = lean_box(x_1); x_3 = lean_alloc_ctor(1, 1, 0); lean_ctor_set(x_3, 0, x_2); return x_3; } } -lean_object* _init_l_Lean_Compiler_getBoolLit___closed__6___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_Compiler_getBoolLit___closed__6() { _start: { uint8_t x_1; lean_object* x_2; lean_object* x_3; x_1 = 1; -x_2 = l_Lean_Compiler_getBoolLit___closed__6___boxed__const__1; +x_2 = lean_box(x_1); x_3 = lean_alloc_ctor(1, 1, 0); lean_ctor_set(x_3, 0, x_2); return x_3; @@ -4529,12 +4509,8 @@ l_Lean_Compiler_getBoolLit___closed__3 = _init_l_Lean_Compiler_getBoolLit___clos lean_mark_persistent(l_Lean_Compiler_getBoolLit___closed__3); l_Lean_Compiler_getBoolLit___closed__4 = _init_l_Lean_Compiler_getBoolLit___closed__4(); lean_mark_persistent(l_Lean_Compiler_getBoolLit___closed__4); -l_Lean_Compiler_getBoolLit___closed__5___boxed__const__1 = _init_l_Lean_Compiler_getBoolLit___closed__5___boxed__const__1(); -lean_mark_persistent(l_Lean_Compiler_getBoolLit___closed__5___boxed__const__1); l_Lean_Compiler_getBoolLit___closed__5 = _init_l_Lean_Compiler_getBoolLit___closed__5(); lean_mark_persistent(l_Lean_Compiler_getBoolLit___closed__5); -l_Lean_Compiler_getBoolLit___closed__6___boxed__const__1 = _init_l_Lean_Compiler_getBoolLit___closed__6___boxed__const__1(); -lean_mark_persistent(l_Lean_Compiler_getBoolLit___closed__6___boxed__const__1); l_Lean_Compiler_getBoolLit___closed__6 = _init_l_Lean_Compiler_getBoolLit___closed__6(); lean_mark_persistent(l_Lean_Compiler_getBoolLit___closed__6); l_Lean_Compiler_boolFoldFns___closed__1 = _init_l_Lean_Compiler_boolFoldFns___closed__1(); diff --git a/src/stage0/init/lean/compiler/inlineattrs.c b/src/stage0/init/lean/compiler/inlineattrs.c index 501a6cfd12..e7085da941 100644 --- a/src/stage0/init/lean/compiler/inlineattrs.c +++ b/src/stage0/init/lean/compiler/inlineattrs.c @@ -16,7 +16,6 @@ extern "C" { lean_object* l_Array_anyMAux___main___at_Lean_Compiler_mkInlineAttrs___spec__6___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_mkInlineAttrs___closed__23; -lean_object* l_Lean_Compiler_mkInlineAttrs___closed__21___boxed__const__1; uint8_t lean_name_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_Compiler_mkInlineAttrs___closed__19; lean_object* l_Lean_EnumAttributes_getValue___at___private_init_lean_compiler_inlineattrs_1__hasInlineAttrAux___main___spec__1(lean_object*, lean_object*, lean_object*); @@ -37,10 +36,8 @@ lean_object* l_Lean_Compiler_InlineAttributeKind_HasBeq___closed__1; lean_object* l_Lean_Compiler_mkInlineAttrs___closed__10; lean_object* l_Lean_Compiler_mkInlineAttrs___closed__12; lean_object* l_Lean_Compiler_mkInlineAttrs___closed__8; -lean_object* l_Lean_Compiler_mkInlineAttrs___closed__6___boxed__const__1; lean_object* l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkInlineAttrs___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_mkInlineAttrs___closed__27; -lean_object* l_Lean_Compiler_mkInlineAttrs___closed__16___boxed__const__1; extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__4; lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*); lean_object* l_Lean_Compiler_hasNoInlineAttribute___boxed(lean_object*, lean_object*); @@ -92,7 +89,6 @@ lean_object* l_Lean_Compiler_mkInlineAttrs___closed__4; lean_object* lean_nat_add(lean_object*, lean_object*); lean_object* l_Lean_PersistentEnvExtension_getModuleEntries___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_RBNode_fold___main___at_Lean_Compiler_mkInlineAttrs___spec__2(lean_object*, lean_object*); -lean_object* l_Lean_Compiler_mkInlineAttrs___closed__11___boxed__const__1; lean_object* l_List_map___main___at_Lean_Compiler_mkInlineAttrs___spec__8___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__3; uint8_t lean_nat_dec_eq(lean_object*, lean_object*); @@ -103,7 +99,6 @@ lean_object* l_Array_push(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Compiler_mkInlineAttrs___closed__21; lean_object* l_Lean_Compiler_mkInlineAttrs___closed__22; lean_object* l_RBNode_find___main___at___private_init_lean_compiler_inlineattrs_1__hasInlineAttrAux___main___spec__2(lean_object*, lean_object*); -lean_object* l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkInlineAttrs___spec__4___closed__1___boxed__const__1; lean_object* l_Lean_registerEnumAttributes___at_Lean_Compiler_mkInlineAttrs___spec__1___closed__1; lean_object* l_RBNode_find___main___at___private_init_lean_compiler_inlineattrs_1__hasInlineAttrAux___main___spec__2___boxed(lean_object*, lean_object*); lean_object* l_EState_bind___rarg(lean_object*, lean_object*, lean_object*); @@ -142,7 +137,6 @@ lean_object* l_Lean_registerEnumAttributes___at_Lean_Compiler_mkInlineAttrs___sp uint8_t lean_has_inline_attribute(lean_object*, lean_object*); extern lean_object* l_Lean_registerTagAttribute___closed__1; extern lean_object* l_Lean_registerEnvExtensionUnsafe___rarg___closed__1; -lean_object* l_Lean_EnumAttributes_getValue___at___private_init_lean_compiler_inlineattrs_1__hasInlineAttrAux___main___spec__1___boxed__const__1; lean_object* l_IO_Prim_Ref_reset(lean_object*, lean_object*, lean_object*); extern lean_object* l___private_init_lean_environment_5__envExtensionsRef; lean_object* l_Array_binSearchAux___main___at___private_init_lean_compiler_inlineattrs_1__hasInlineAttrAux___main___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -291,22 +285,13 @@ goto _start; } } } -lean_object* _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkInlineAttrs___spec__4___closed__1___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = l_Lean_Compiler_InlineAttributeKind_Inhabited; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkInlineAttrs___spec__4___closed__1() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Inhabited; x_2 = l_Lean_Compiler_InlineAttributeKind_Inhabited; -x_3 = l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkInlineAttrs___spec__4___closed__1___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -2823,22 +2808,13 @@ x_1 = lean_mk_string("mark definition to always be inlined"); return x_1; } } -lean_object* _init_l_Lean_Compiler_mkInlineAttrs___closed__6___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_Compiler_mkInlineAttrs___closed__6() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Compiler_mkInlineAttrs___closed__5; x_2 = 0; -x_3 = l_Lean_Compiler_mkInlineAttrs___closed__6___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -2883,22 +2859,13 @@ x_1 = lean_mk_string("mark definition to be inlined when resultant term after re return x_1; } } -lean_object* _init_l_Lean_Compiler_mkInlineAttrs___closed__11___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 3; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_Compiler_mkInlineAttrs___closed__11() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Compiler_mkInlineAttrs___closed__10; x_2 = 3; -x_3 = l_Lean_Compiler_mkInlineAttrs___closed__11___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -2943,22 +2910,13 @@ x_1 = lean_mk_string("mark definition to never be inlined"); return x_1; } } -lean_object* _init_l_Lean_Compiler_mkInlineAttrs___closed__16___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_Compiler_mkInlineAttrs___closed__16() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Compiler_mkInlineAttrs___closed__15; x_2 = 1; -x_3 = l_Lean_Compiler_mkInlineAttrs___closed__16___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -3003,22 +2961,13 @@ x_1 = lean_mk_string("mark definition to always be inlined before ANF conversion return x_1; } } -lean_object* _init_l_Lean_Compiler_mkInlineAttrs___closed__21___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 2; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_Compiler_mkInlineAttrs___closed__21() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Compiler_mkInlineAttrs___closed__20; x_2 = 2; -x_3 = l_Lean_Compiler_mkInlineAttrs___closed__21___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -3299,15 +3248,6 @@ goto _start; } } } -lean_object* _init_l_Lean_EnumAttributes_getValue___at___private_init_lean_compiler_inlineattrs_1__hasInlineAttrAux___main___spec__1___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Lean_EnumAttributes_getValue___at___private_init_lean_compiler_inlineattrs_1__hasInlineAttrAux___main___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -3337,7 +3277,7 @@ lean_dec(x_1); x_10 = l_Lean_PersistentEnvExtension_getModuleEntries___rarg(x_9, x_2, x_8); lean_dec(x_8); x_11 = 0; -x_12 = l_Lean_EnumAttributes_getValue___at___private_init_lean_compiler_inlineattrs_1__hasInlineAttrAux___main___spec__1___boxed__const__1; +x_12 = lean_box(x_11); x_13 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_13, 0, x_3); lean_ctor_set(x_13, 1, x_12); @@ -3592,8 +3532,6 @@ l_Lean_Compiler_InlineAttributeKind_HasBeq___closed__1 = _init_l_Lean_Compiler_I lean_mark_persistent(l_Lean_Compiler_InlineAttributeKind_HasBeq___closed__1); l_Lean_Compiler_InlineAttributeKind_HasBeq = _init_l_Lean_Compiler_InlineAttributeKind_HasBeq(); lean_mark_persistent(l_Lean_Compiler_InlineAttributeKind_HasBeq); -l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkInlineAttrs___spec__4___closed__1___boxed__const__1 = _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkInlineAttrs___spec__4___closed__1___boxed__const__1(); -lean_mark_persistent(l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkInlineAttrs___spec__4___closed__1___boxed__const__1); l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkInlineAttrs___spec__4___closed__1 = _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkInlineAttrs___spec__4___closed__1(); lean_mark_persistent(l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkInlineAttrs___spec__4___closed__1); l_Lean_registerEnumAttributes___at_Lean_Compiler_mkInlineAttrs___spec__1___closed__1 = _init_l_Lean_registerEnumAttributes___at_Lean_Compiler_mkInlineAttrs___spec__1___closed__1(); @@ -3610,8 +3548,6 @@ l_Lean_Compiler_mkInlineAttrs___closed__4 = _init_l_Lean_Compiler_mkInlineAttrs_ lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__4); l_Lean_Compiler_mkInlineAttrs___closed__5 = _init_l_Lean_Compiler_mkInlineAttrs___closed__5(); lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__5); -l_Lean_Compiler_mkInlineAttrs___closed__6___boxed__const__1 = _init_l_Lean_Compiler_mkInlineAttrs___closed__6___boxed__const__1(); -lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__6___boxed__const__1); l_Lean_Compiler_mkInlineAttrs___closed__6 = _init_l_Lean_Compiler_mkInlineAttrs___closed__6(); lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__6); l_Lean_Compiler_mkInlineAttrs___closed__7 = _init_l_Lean_Compiler_mkInlineAttrs___closed__7(); @@ -3622,8 +3558,6 @@ l_Lean_Compiler_mkInlineAttrs___closed__9 = _init_l_Lean_Compiler_mkInlineAttrs_ lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__9); l_Lean_Compiler_mkInlineAttrs___closed__10 = _init_l_Lean_Compiler_mkInlineAttrs___closed__10(); lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__10); -l_Lean_Compiler_mkInlineAttrs___closed__11___boxed__const__1 = _init_l_Lean_Compiler_mkInlineAttrs___closed__11___boxed__const__1(); -lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__11___boxed__const__1); l_Lean_Compiler_mkInlineAttrs___closed__11 = _init_l_Lean_Compiler_mkInlineAttrs___closed__11(); lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__11); l_Lean_Compiler_mkInlineAttrs___closed__12 = _init_l_Lean_Compiler_mkInlineAttrs___closed__12(); @@ -3634,8 +3568,6 @@ l_Lean_Compiler_mkInlineAttrs___closed__14 = _init_l_Lean_Compiler_mkInlineAttrs lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__14); l_Lean_Compiler_mkInlineAttrs___closed__15 = _init_l_Lean_Compiler_mkInlineAttrs___closed__15(); lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__15); -l_Lean_Compiler_mkInlineAttrs___closed__16___boxed__const__1 = _init_l_Lean_Compiler_mkInlineAttrs___closed__16___boxed__const__1(); -lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__16___boxed__const__1); l_Lean_Compiler_mkInlineAttrs___closed__16 = _init_l_Lean_Compiler_mkInlineAttrs___closed__16(); lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__16); l_Lean_Compiler_mkInlineAttrs___closed__17 = _init_l_Lean_Compiler_mkInlineAttrs___closed__17(); @@ -3646,8 +3578,6 @@ l_Lean_Compiler_mkInlineAttrs___closed__19 = _init_l_Lean_Compiler_mkInlineAttrs lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__19); l_Lean_Compiler_mkInlineAttrs___closed__20 = _init_l_Lean_Compiler_mkInlineAttrs___closed__20(); lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__20); -l_Lean_Compiler_mkInlineAttrs___closed__21___boxed__const__1 = _init_l_Lean_Compiler_mkInlineAttrs___closed__21___boxed__const__1(); -lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__21___boxed__const__1); l_Lean_Compiler_mkInlineAttrs___closed__21 = _init_l_Lean_Compiler_mkInlineAttrs___closed__21(); lean_mark_persistent(l_Lean_Compiler_mkInlineAttrs___closed__21); l_Lean_Compiler_mkInlineAttrs___closed__22 = _init_l_Lean_Compiler_mkInlineAttrs___closed__22(); @@ -3666,8 +3596,6 @@ w = l_Lean_Compiler_mkInlineAttrs(w); if (lean_io_result_is_error(w)) return w; l_Lean_Compiler_inlineAttrs = lean_io_result_get_value(w); lean_mark_persistent(l_Lean_Compiler_inlineAttrs); -l_Lean_EnumAttributes_getValue___at___private_init_lean_compiler_inlineattrs_1__hasInlineAttrAux___main___spec__1___boxed__const__1 = _init_l_Lean_EnumAttributes_getValue___at___private_init_lean_compiler_inlineattrs_1__hasInlineAttrAux___main___spec__1___boxed__const__1(); -lean_mark_persistent(l_Lean_EnumAttributes_getValue___at___private_init_lean_compiler_inlineattrs_1__hasInlineAttrAux___main___spec__1___boxed__const__1); return w; } #ifdef __cplusplus diff --git a/src/stage0/init/lean/compiler/ir/borrow.c b/src/stage0/init/lean/compiler/ir/borrow.c index 855c5496ec..1947b77e3f 100644 --- a/src/stage0/init/lean/compiler/ir/borrow.c +++ b/src/stage0/init/lean/compiler/ir/borrow.c @@ -44,7 +44,6 @@ lean_object* l_Lean_IR_Borrow_preserveTailCall(lean_object*, lean_object*, lean_ lean_object* l_Lean_IR_FnBody_body(lean_object*); lean_object* l_Lean_IR_Borrow_InitParamMap_visitDecls(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_Borrow_Lean_HasFormat; -lean_object* l_Lean_IR_Borrow_isOwned___boxed__const__1; lean_object* l_Array_miterateAux___main___at_Lean_IR_Borrow_updateParamSet___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_Borrow_ParamMap_fmt___closed__1; lean_object* l_Lean_IR_Borrow_updateParamMap___boxed(lean_object*, lean_object*, lean_object*); @@ -69,7 +68,6 @@ lean_object* l_Lean_IR_Borrow_ownArgsIfParam___boxed(lean_object*, lean_object*, lean_object* l_Lean_IR_Borrow_preserveTailCall___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_Borrow_whileModifingOwnedAux___main(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_Borrow_getParamInfo(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_IR_Borrow_isOwned___boxed__const__2; lean_object* l_Array_mforAux___main___at_Lean_IR_Borrow_InitParamMap_visitDecls___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_Borrow_applyParamMap___boxed(lean_object*, lean_object*); lean_object* l_Lean_IR_Borrow_isOwned___boxed(lean_object*, lean_object*, lean_object*); @@ -1775,24 +1773,6 @@ lean_dec(x_1); return x_4; } } -lean_object* _init_l_Lean_IR_Borrow_isOwned___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l_Lean_IR_Borrow_isOwned___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Lean_IR_Borrow_isOwned(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -1805,7 +1785,7 @@ if (lean_obj_tag(x_5) == 0) { uint8_t x_6; lean_object* x_7; lean_object* x_8; x_6 = 0; -x_7 = l_Lean_IR_Borrow_isOwned___boxed__const__1; +x_7 = lean_box(x_6); x_8 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_8, 0, x_7); lean_ctor_set(x_8, 1, x_3); @@ -1816,7 +1796,7 @@ else uint8_t x_9; lean_object* x_10; lean_object* x_11; lean_dec(x_5); x_9 = 1; -x_10 = l_Lean_IR_Borrow_isOwned___boxed__const__2; +x_10 = lean_box(x_9); x_11 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_11, 0, x_10); lean_ctor_set(x_11, 1, x_3); @@ -3930,10 +3910,6 @@ l_Lean_IR_Borrow_Lean_HasFormat = _init_l_Lean_IR_Borrow_Lean_HasFormat(); lean_mark_persistent(l_Lean_IR_Borrow_Lean_HasFormat); l_Lean_IR_Borrow_mkInitParamMap___closed__1 = _init_l_Lean_IR_Borrow_mkInitParamMap___closed__1(); lean_mark_persistent(l_Lean_IR_Borrow_mkInitParamMap___closed__1); -l_Lean_IR_Borrow_isOwned___boxed__const__1 = _init_l_Lean_IR_Borrow_isOwned___boxed__const__1(); -lean_mark_persistent(l_Lean_IR_Borrow_isOwned___boxed__const__1); -l_Lean_IR_Borrow_isOwned___boxed__const__2 = _init_l_Lean_IR_Borrow_isOwned___boxed__const__2(); -lean_mark_persistent(l_Lean_IR_Borrow_isOwned___boxed__const__2); return w; } #ifdef __cplusplus diff --git a/src/stage0/init/lean/compiler/ir/boxing.c b/src/stage0/init/lean/compiler/ir/boxing.c index 35715eabb9..fff2b44c4d 100644 --- a/src/stage0/init/lean/compiler/ir/boxing.c +++ b/src/stage0/init/lean/compiler/ir/boxing.c @@ -34,13 +34,13 @@ lean_object* l_Lean_IR_explicitBoxing___boxed(lean_object*, lean_object*, lean_o lean_object* l_Array_ummapAux___main___at_Lean_IR_ExplicitBoxing_visitFnBody___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_mkBoxedName(lean_object*); lean_object* l_AssocList_find___main___at_Lean_IR_ExplicitBoxing_mkCast___spec__1(lean_object*, lean_object*); +lean_object* l___private_init_lean_compiler_ir_boxing_2__isExpensiveConstantValueBoxing___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Nat_mfoldAux___main___at_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_unboxResultIfNeeded(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Nat_mfoldAux___main___at_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_getScrutineeType___boxed(lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_mkCast___closed__2; lean_object* l_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___closed__1; -lean_object* l_Lean_IR_ExplicitBoxing_getVarType___boxed__const__1; uint8_t l_Lean_IR_ExplicitBoxing_isBoxedName(lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_run(lean_object*, lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_mkBoxedVersion___boxed(lean_object*); @@ -52,7 +52,6 @@ lean_object* l_Array_miterateAux___main___at_Lean_IR_ExplicitBoxing_visitVDeclEx lean_object* l_Lean_IR_ExplicitBoxing_castArgIfNeeded___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_withVDecl(lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_castArgsIfNeededAux___at_Lean_IR_ExplicitBoxing_visitVDeclExpr___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l___private_init_lean_compiler_ir_boxing_2__isConstantValue___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Array_miterateAux___main___at_Lean_IR_ExplicitBoxing_run___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_unboxResultIfNeeded___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_miterateAux___main___at_Lean_IR_ExplicitBoxing_castArgsIfNeeded___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -79,7 +78,6 @@ lean_object* l_Lean_IR_ExplicitBoxing_mkCast___closed__1; lean_object* l_Lean_IR_ExplicitBoxing_mkBoxedVersionAux(lean_object*, lean_object*); lean_object* l_Array_anyMAux___main___at_Lean_IR_ExplicitBoxing_getScrutineeType___spec__1___boxed(lean_object*, lean_object*); lean_object* lean_nat_add(lean_object*, lean_object*); -lean_object* l_Lean_IR_ExplicitBoxing_mkCast___closed__5; lean_object* l_Array_miterateAux___main___at_Lean_IR_ExplicitBoxing_visitFnBody___main___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_IR_CtorInfo_isScalar(lean_object*); uint8_t lean_nat_dec_eq(lean_object*, lean_object*); @@ -100,7 +98,6 @@ lean_object* l_Array_miterateAux___main___at_Lean_IR_ExplicitBoxing_visitFnBody_ lean_object* l_Lean_IR_Decl_params(lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_castResultIfNeeded___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_castArgsIfNeededAux(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l___private_init_lean_compiler_ir_boxing_2__isConstantValue(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_getJPParams___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_getLocalContext(lean_object*, lean_object*); extern lean_object* l_Lean_closureMaxArgs; @@ -128,6 +125,7 @@ extern lean_object* l_Lean_IR_Decl_Inhabited___closed__1; lean_object* l_Lean_IR_ExplicitBoxing_getDecl___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_getJPParams(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_addBoxedVersions(lean_object*, lean_object*); +lean_object* l___private_init_lean_compiler_ir_boxing_2__isExpensiveConstantValueBoxing(lean_object*, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_requiresBoxedVersion___boxed(lean_object*, lean_object*); lean_object* l_Lean_IR_ExplicitBoxing_castArgsIfNeededAux___at_Lean_IR_ExplicitBoxing_boxArgsIfNeeded___spec__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Array_miterateAux___main___at_Lean_IR_ExplicitBoxing_addBoxedVersions___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1347,15 +1345,6 @@ lean_dec(x_1); return x_3; } } -lean_object* _init_l_Lean_IR_ExplicitBoxing_getVarType___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 7; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Lean_IR_ExplicitBoxing_getVarType(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -1372,7 +1361,7 @@ if (lean_obj_tag(x_7) == 0) { uint8_t x_8; lean_object* x_9; x_8 = 7; -x_9 = l_Lean_IR_ExplicitBoxing_getVarType___boxed__const__1; +x_9 = lean_box(x_8); lean_ctor_set(x_4, 0, x_9); return x_4; } @@ -1400,7 +1389,7 @@ if (lean_obj_tag(x_13) == 0) { uint8_t x_14; lean_object* x_15; lean_object* x_16; x_14 = 7; -x_15 = l_Lean_IR_ExplicitBoxing_getVarType___boxed__const__1; +x_15 = lean_box(x_14); x_16 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_16, 0, x_15); lean_ctor_set(x_16, 1, x_12); @@ -1703,159 +1692,224 @@ x_2 = lean_alloc_closure((void*)(l_Lean_IR_ExplicitBoxing_withJDecl___rarg), 6, return x_2; } } -lean_object* l___private_init_lean_compiler_ir_boxing_2__isConstantValue(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l___private_init_lean_compiler_ir_boxing_2__isExpensiveConstantValueBoxing(lean_object* x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4) { _start: { -lean_object* x_4; uint8_t x_5; -x_4 = l_Lean_IR_ExplicitBoxing_getLocalContext(x_2, x_3); -x_5 = !lean_is_exclusive(x_4); -if (x_5 == 0) +lean_object* x_5; uint8_t x_33; +x_33 = l_Lean_IR_IRType_isScalar(x_2); +if (x_33 == 0) { -lean_object* x_6; lean_object* x_7; -x_6 = lean_ctor_get(x_4, 0); -x_7 = l_Lean_IR_LocalContext_getValue(x_6, x_1); -lean_dec(x_6); -if (lean_obj_tag(x_7) == 0) -{ -lean_ctor_set(x_4, 0, x_7); -return x_4; +lean_object* x_34; lean_object* x_35; +x_34 = lean_box(0); +x_35 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_35, 0, x_34); +lean_ctor_set(x_35, 1, x_4); +return x_35; } else { -lean_object* x_8; -x_8 = lean_ctor_get(x_7, 0); -lean_inc(x_8); -switch (lean_obj_tag(x_8)) { +uint8_t x_36; uint8_t x_37; +x_36 = 4; +x_37 = l_Lean_IR_IRType_beq(x_2, x_36); +if (x_37 == 0) +{ +uint8_t x_38; uint8_t x_39; +x_38 = 3; +x_39 = l_Lean_IR_IRType_beq(x_2, x_38); +if (x_39 == 0) +{ +uint8_t x_40; uint8_t x_41; +x_40 = 5; +x_41 = l_Lean_IR_IRType_beq(x_2, x_40); +if (x_41 == 0) +{ +lean_object* x_42; lean_object* x_43; +x_42 = lean_box(0); +x_43 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_43, 0, x_42); +lean_ctor_set(x_43, 1, x_4); +return x_43; +} +else +{ +lean_object* x_44; +x_44 = lean_box(0); +x_5 = x_44; +goto block_32; +} +} +else +{ +lean_object* x_45; +x_45 = lean_box(0); +x_5 = x_45; +goto block_32; +} +} +else +{ +lean_object* x_46; +x_46 = lean_box(0); +x_5 = x_46; +goto block_32; +} +} +block_32: +{ +lean_object* x_6; uint8_t x_7; +lean_dec(x_5); +x_6 = l_Lean_IR_ExplicitBoxing_getLocalContext(x_3, x_4); +x_7 = !lean_is_exclusive(x_6); +if (x_7 == 0) +{ +lean_object* x_8; lean_object* x_9; +x_8 = lean_ctor_get(x_6, 0); +x_9 = l_Lean_IR_LocalContext_getValue(x_8, x_1); +lean_dec(x_8); +if (lean_obj_tag(x_9) == 0) +{ +lean_ctor_set(x_6, 0, x_9); +return x_6; +} +else +{ +lean_object* x_10; +x_10 = lean_ctor_get(x_9, 0); +lean_inc(x_10); +switch (lean_obj_tag(x_10)) { case 6: { -lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12; -x_9 = lean_ctor_get(x_8, 1); -lean_inc(x_9); -lean_dec(x_8); -x_10 = lean_array_get_size(x_9); -lean_dec(x_9); -x_11 = lean_unsigned_to_nat(0u); -x_12 = lean_nat_dec_eq(x_10, x_11); +lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; +x_11 = lean_ctor_get(x_10, 1); +lean_inc(x_11); lean_dec(x_10); -if (x_12 == 0) +x_12 = lean_array_get_size(x_11); +lean_dec(x_11); +x_13 = lean_unsigned_to_nat(0u); +x_14 = lean_nat_dec_eq(x_12, x_13); +lean_dec(x_12); +if (x_14 == 0) { -lean_object* x_13; -lean_dec(x_7); -x_13 = lean_box(0); -lean_ctor_set(x_4, 0, x_13); -return x_4; +lean_object* x_15; +lean_dec(x_9); +x_15 = lean_box(0); +lean_ctor_set(x_6, 0, x_15); +return x_6; } else { -lean_ctor_set(x_4, 0, x_7); -return x_4; +lean_ctor_set(x_6, 0, x_9); +return x_6; } } case 11: { -lean_dec(x_8); -lean_ctor_set(x_4, 0, x_7); -return x_4; +lean_dec(x_10); +lean_ctor_set(x_6, 0, x_9); +return x_6; } default: { -lean_object* x_14; -lean_dec(x_8); -lean_dec(x_7); -x_14 = lean_box(0); -lean_ctor_set(x_4, 0, x_14); -return x_4; +lean_object* x_16; +lean_dec(x_10); +lean_dec(x_9); +x_16 = lean_box(0); +lean_ctor_set(x_6, 0, x_16); +return x_6; } } } } else { -lean_object* x_15; lean_object* x_16; lean_object* x_17; -x_15 = lean_ctor_get(x_4, 0); -x_16 = lean_ctor_get(x_4, 1); -lean_inc(x_16); -lean_inc(x_15); -lean_dec(x_4); -x_17 = l_Lean_IR_LocalContext_getValue(x_15, x_1); -lean_dec(x_15); -if (lean_obj_tag(x_17) == 0) +lean_object* x_17; lean_object* x_18; lean_object* x_19; +x_17 = lean_ctor_get(x_6, 0); +x_18 = lean_ctor_get(x_6, 1); +lean_inc(x_18); +lean_inc(x_17); +lean_dec(x_6); +x_19 = l_Lean_IR_LocalContext_getValue(x_17, x_1); +lean_dec(x_17); +if (lean_obj_tag(x_19) == 0) { -lean_object* x_18; -x_18 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_18, 0, x_17); -lean_ctor_set(x_18, 1, x_16); -return x_18; +lean_object* x_20; +x_20 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_20, 0, x_19); +lean_ctor_set(x_20, 1, x_18); +return x_20; } else { -lean_object* x_19; -x_19 = lean_ctor_get(x_17, 0); -lean_inc(x_19); -switch (lean_obj_tag(x_19)) { +lean_object* x_21; +x_21 = lean_ctor_get(x_19, 0); +lean_inc(x_21); +switch (lean_obj_tag(x_21)) { case 6: { -lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; -x_20 = lean_ctor_get(x_19, 1); -lean_inc(x_20); -lean_dec(x_19); -x_21 = lean_array_get_size(x_20); -lean_dec(x_20); -x_22 = lean_unsigned_to_nat(0u); -x_23 = lean_nat_dec_eq(x_21, x_22); +lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25; +x_22 = lean_ctor_get(x_21, 1); +lean_inc(x_22); lean_dec(x_21); -if (x_23 == 0) +x_23 = lean_array_get_size(x_22); +lean_dec(x_22); +x_24 = lean_unsigned_to_nat(0u); +x_25 = lean_nat_dec_eq(x_23, x_24); +lean_dec(x_23); +if (x_25 == 0) { -lean_object* x_24; lean_object* x_25; -lean_dec(x_17); -x_24 = lean_box(0); -x_25 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_25, 0, x_24); -lean_ctor_set(x_25, 1, x_16); -return x_25; -} -else -{ -lean_object* x_26; -x_26 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_26, 0, x_17); -lean_ctor_set(x_26, 1, x_16); -return x_26; -} -} -case 11: -{ -lean_object* x_27; +lean_object* x_26; lean_object* x_27; lean_dec(x_19); +x_26 = lean_box(0); x_27 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_27, 0, x_17); -lean_ctor_set(x_27, 1, x_16); +lean_ctor_set(x_27, 0, x_26); +lean_ctor_set(x_27, 1, x_18); return x_27; } -default: +else { -lean_object* x_28; lean_object* x_29; -lean_dec(x_19); -lean_dec(x_17); -x_28 = lean_box(0); +lean_object* x_28; +x_28 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_28, 0, x_19); +lean_ctor_set(x_28, 1, x_18); +return x_28; +} +} +case 11: +{ +lean_object* x_29; +lean_dec(x_21); x_29 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_29, 0, x_28); -lean_ctor_set(x_29, 1, x_16); +lean_ctor_set(x_29, 0, x_19); +lean_ctor_set(x_29, 1, x_18); return x_29; } +default: +{ +lean_object* x_30; lean_object* x_31; +lean_dec(x_21); +lean_dec(x_19); +x_30 = lean_box(0); +x_31 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_31, 0, x_30); +lean_ctor_set(x_31, 1, x_18); +return x_31; } } } } } -lean_object* l___private_init_lean_compiler_ir_boxing_2__isConstantValue___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +} +} +lean_object* l___private_init_lean_compiler_ir_boxing_2__isExpensiveConstantValueBoxing___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { -lean_object* x_4; -x_4 = l___private_init_lean_compiler_ir_boxing_2__isConstantValue(x_1, x_2, x_3); +uint8_t x_5; lean_object* x_6; +x_5 = lean_unbox(x_2); lean_dec(x_2); +x_6 = l___private_init_lean_compiler_ir_boxing_2__isExpensiveConstantValueBoxing(x_1, x_5, x_3, x_4); +lean_dec(x_3); lean_dec(x_1); -return x_4; +return x_6; } } lean_object* l_AssocList_find___main___at_Lean_IR_ExplicitBoxing_mkCast___spec__1(lean_object* x_1, lean_object* x_2) { @@ -1901,34 +1955,6 @@ return x_9; lean_object* _init_l_Lean_IR_ExplicitBoxing_mkCast___closed__1() { _start: { -lean_object* x_1; -x_1 = lean_mk_string("_boxed_const"); -return x_1; -} -} -lean_object* _init_l_Lean_IR_ExplicitBoxing_mkCast___closed__2() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_IR_ExplicitBoxing_mkCast___closed__1; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_IR_ExplicitBoxing_mkCast___closed__3() { -_start: -{ -lean_object* x_1; lean_object* x_2; -x_1 = lean_unsigned_to_nat(1u); -x_2 = lean_alloc_ctor(10, 1, 0); -lean_ctor_set(x_2, 0, x_1); -return x_2; -} -} -lean_object* _init_l_Lean_IR_ExplicitBoxing_mkCast___closed__4() { -_start: -{ lean_object* x_1; lean_object* x_2; x_1 = lean_unsigned_to_nat(2u); x_2 = lean_alloc_ctor(0, 1, 0); @@ -1936,21 +1962,39 @@ lean_ctor_set(x_2, 0, x_1); return x_2; } } -lean_object* _init_l_Lean_IR_ExplicitBoxing_mkCast___closed__5() { +lean_object* _init_l_Lean_IR_ExplicitBoxing_mkCast___closed__2() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_IR_ExplicitBoxing_mkCast___closed__4; +x_1 = l_Lean_IR_ExplicitBoxing_mkCast___closed__1; x_2 = lean_alloc_ctor(11, 1, 0); lean_ctor_set(x_2, 0, x_1); return x_2; } } +lean_object* _init_l_Lean_IR_ExplicitBoxing_mkCast___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("_boxed_const"); +return x_1; +} +} +lean_object* _init_l_Lean_IR_ExplicitBoxing_mkCast___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_IR_ExplicitBoxing_mkCast___closed__3; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} lean_object* l_Lean_IR_ExplicitBoxing_mkCast(lean_object* x_1, uint8_t x_2, uint8_t x_3, lean_object* x_4, lean_object* x_5) { _start: { lean_object* x_6; lean_object* x_7; -x_6 = l___private_init_lean_compiler_ir_boxing_2__isConstantValue(x_1, x_4, x_5); +x_6 = l___private_init_lean_compiler_ir_boxing_2__isExpensiveConstantValueBoxing(x_1, x_2, x_4, x_5); x_7 = lean_ctor_get(x_6, 0); lean_inc(x_7); if (lean_obj_tag(x_7) == 0) @@ -2013,171 +2057,245 @@ return x_18; } else { -lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23; lean_object* x_24; +uint8_t x_19; lean_dec(x_1); -x_19 = lean_ctor_get(x_6, 1); -lean_inc(x_19); -if (lean_is_exclusive(x_6)) { - lean_ctor_release(x_6, 0); - lean_ctor_release(x_6, 1); - x_20 = x_6; -} else { - lean_dec_ref(x_6); - x_20 = lean_box(0); -} -x_21 = lean_ctor_get(x_7, 0); -lean_inc(x_21); +x_19 = !lean_is_exclusive(x_6); +if (x_19 == 0) +{ +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; +x_20 = lean_ctor_get(x_6, 1); +x_21 = lean_ctor_get(x_6, 0); +lean_dec(x_21); +x_22 = lean_ctor_get(x_7, 0); +lean_inc(x_22); lean_dec(x_7); -x_22 = l_Lean_IR_IRType_isScalar(x_2); -x_23 = lean_ctor_get(x_19, 2); -lean_inc(x_23); -if (x_22 == 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; -x_54 = lean_unsigned_to_nat(2u); -x_55 = l_Lean_IR_ExplicitBoxing_mkCast___closed__3; -x_56 = l_Lean_IR_ExplicitBoxing_mkCast___closed__5; -x_57 = lean_alloc_ctor(0, 3, 1); -lean_ctor_set(x_57, 0, x_54); -lean_ctor_set(x_57, 1, x_55); -lean_ctor_set(x_57, 2, x_56); -lean_ctor_set_uint8(x_57, sizeof(void*)*3, x_3); -x_58 = lean_unsigned_to_nat(1u); -x_59 = lean_alloc_ctor(0, 3, 1); -lean_ctor_set(x_59, 0, x_58); -lean_ctor_set(x_59, 1, x_21); -lean_ctor_set(x_59, 2, x_57); -lean_ctor_set_uint8(x_59, sizeof(void*)*3, x_2); -x_24 = x_59; -goto block_53; -} -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; -x_60 = lean_unsigned_to_nat(1u); -x_61 = lean_alloc_ctor(9, 1, 1); -lean_ctor_set(x_61, 0, x_60); -lean_ctor_set_uint8(x_61, sizeof(void*)*1, x_2); -x_62 = lean_unsigned_to_nat(2u); -x_63 = l_Lean_IR_ExplicitBoxing_mkCast___closed__5; -x_64 = lean_alloc_ctor(0, 3, 1); -lean_ctor_set(x_64, 0, x_62); -lean_ctor_set(x_64, 1, x_61); -lean_ctor_set(x_64, 2, x_63); -lean_ctor_set_uint8(x_64, sizeof(void*)*3, x_3); -x_65 = lean_alloc_ctor(0, 3, 1); -lean_ctor_set(x_65, 0, x_60); -lean_ctor_set(x_65, 1, x_21); -lean_ctor_set(x_65, 2, x_64); -lean_ctor_set_uint8(x_65, sizeof(void*)*3, x_2); -x_24 = x_65; -goto block_53; -} -block_53: -{ -lean_object* x_25; -lean_inc(x_23); -lean_inc(x_24); -x_25 = l_AssocList_find___main___at_Lean_IR_ExplicitBoxing_mkCast___spec__1(x_24, x_23); -if (lean_obj_tag(x_25) == 0) -{ -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; uint8_t x_34; -x_26 = lean_ctor_get(x_4, 0); -x_27 = lean_ctor_get(x_19, 3); -lean_inc(x_27); -x_28 = l_Lean_IR_ExplicitBoxing_mkCast___closed__2; -lean_inc(x_27); -x_29 = l_Lean_Name_appendIndexAfter(x_28, x_27); -x_30 = l_Lean_Name_append___main(x_26, x_29); -x_31 = l_Array_empty___closed__1; +x_23 = lean_unsigned_to_nat(1u); +x_24 = lean_alloc_ctor(9, 1, 1); +lean_ctor_set(x_24, 0, x_23); +lean_ctor_set_uint8(x_24, sizeof(void*)*1, x_2); +x_25 = lean_unsigned_to_nat(2u); +x_26 = l_Lean_IR_ExplicitBoxing_mkCast___closed__2; +x_27 = lean_alloc_ctor(0, 3, 1); +lean_ctor_set(x_27, 0, x_25); +lean_ctor_set(x_27, 1, x_24); +lean_ctor_set(x_27, 2, x_26); +lean_ctor_set_uint8(x_27, sizeof(void*)*3, x_3); +x_28 = lean_alloc_ctor(0, 3, 1); +lean_ctor_set(x_28, 0, x_23); +lean_ctor_set(x_28, 1, x_22); +lean_ctor_set(x_28, 2, x_27); +lean_ctor_set_uint8(x_28, sizeof(void*)*3, x_2); +x_29 = lean_ctor_get(x_20, 0); +lean_inc(x_29); +x_30 = lean_ctor_get(x_20, 1); lean_inc(x_30); -x_32 = lean_alloc_ctor(6, 2, 0); -lean_ctor_set(x_32, 0, x_30); -lean_ctor_set(x_32, 1, x_31); -lean_inc(x_24); -x_33 = lean_alloc_ctor(0, 3, 1); -lean_ctor_set(x_33, 0, x_30); -lean_ctor_set(x_33, 1, x_31); -lean_ctor_set(x_33, 2, x_24); -lean_ctor_set_uint8(x_33, sizeof(void*)*3, x_3); -x_34 = !lean_is_exclusive(x_19); +x_31 = lean_ctor_get(x_20, 2); +lean_inc(x_31); +x_32 = lean_ctor_get(x_20, 3); +lean_inc(x_32); +lean_inc(x_31); +lean_inc(x_28); +x_33 = l_AssocList_find___main___at_Lean_IR_ExplicitBoxing_mkCast___spec__1(x_28, x_31); +if (lean_obj_tag(x_33) == 0) +{ +uint8_t x_34; +x_34 = !lean_is_exclusive(x_20); if (x_34 == 0) { -lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; -x_35 = lean_ctor_get(x_19, 1); -x_36 = lean_ctor_get(x_19, 3); +lean_object* x_35; lean_object* x_36; lean_object* x_37; 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; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; +x_35 = lean_ctor_get(x_20, 3); +lean_dec(x_35); +x_36 = lean_ctor_get(x_20, 2); lean_dec(x_36); -x_37 = lean_ctor_get(x_19, 2); +x_37 = lean_ctor_get(x_20, 1); lean_dec(x_37); -x_38 = lean_array_push(x_35, x_33); +x_38 = lean_ctor_get(x_20, 0); +lean_dec(x_38); +x_39 = lean_ctor_get(x_4, 0); +x_40 = l_Lean_IR_ExplicitBoxing_mkCast___closed__4; lean_inc(x_32); -x_39 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_39, 0, x_24); -lean_ctor_set(x_39, 1, x_32); -lean_ctor_set(x_39, 2, x_23); -x_40 = lean_unsigned_to_nat(1u); -x_41 = lean_nat_add(x_27, x_40); -lean_dec(x_27); -lean_ctor_set(x_19, 3, x_41); -lean_ctor_set(x_19, 2, x_39); -lean_ctor_set(x_19, 1, x_38); -if (lean_is_scalar(x_20)) { - x_42 = lean_alloc_ctor(0, 2, 0); -} else { - x_42 = x_20; -} -lean_ctor_set(x_42, 0, x_32); -lean_ctor_set(x_42, 1, x_19); -return x_42; -} -else -{ -lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; -x_43 = lean_ctor_get(x_19, 0); -x_44 = lean_ctor_get(x_19, 1); +x_41 = l_Lean_Name_appendIndexAfter(x_40, x_32); +x_42 = l_Lean_Name_append___main(x_39, x_41); +x_43 = l_Array_empty___closed__1; +lean_inc(x_42); +x_44 = lean_alloc_ctor(6, 2, 0); +lean_ctor_set(x_44, 0, x_42); +lean_ctor_set(x_44, 1, x_43); +lean_inc(x_28); +x_45 = lean_alloc_ctor(0, 3, 1); +lean_ctor_set(x_45, 0, x_42); +lean_ctor_set(x_45, 1, x_43); +lean_ctor_set(x_45, 2, x_28); +lean_ctor_set_uint8(x_45, sizeof(void*)*3, x_3); +x_46 = lean_array_push(x_30, x_45); lean_inc(x_44); -lean_inc(x_43); -lean_dec(x_19); -x_45 = lean_array_push(x_44, x_33); -lean_inc(x_32); -x_46 = lean_alloc_ctor(1, 3, 0); -lean_ctor_set(x_46, 0, x_24); -lean_ctor_set(x_46, 1, x_32); -lean_ctor_set(x_46, 2, x_23); -x_47 = lean_unsigned_to_nat(1u); -x_48 = lean_nat_add(x_27, x_47); -lean_dec(x_27); -x_49 = lean_alloc_ctor(0, 4, 0); -lean_ctor_set(x_49, 0, x_43); -lean_ctor_set(x_49, 1, x_45); -lean_ctor_set(x_49, 2, x_46); -lean_ctor_set(x_49, 3, x_48); -if (lean_is_scalar(x_20)) { - x_50 = lean_alloc_ctor(0, 2, 0); -} else { - x_50 = x_20; +x_47 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_47, 0, x_28); +lean_ctor_set(x_47, 1, x_44); +lean_ctor_set(x_47, 2, x_31); +x_48 = lean_nat_add(x_32, x_23); +lean_dec(x_32); +lean_ctor_set(x_20, 3, x_48); +lean_ctor_set(x_20, 2, x_47); +lean_ctor_set(x_20, 1, x_46); +lean_ctor_set(x_6, 0, x_44); +return x_6; } -lean_ctor_set(x_50, 0, x_32); -lean_ctor_set(x_50, 1, x_49); -return x_50; +else +{ +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; lean_object* x_59; +lean_dec(x_20); +x_49 = lean_ctor_get(x_4, 0); +x_50 = l_Lean_IR_ExplicitBoxing_mkCast___closed__4; +lean_inc(x_32); +x_51 = l_Lean_Name_appendIndexAfter(x_50, x_32); +x_52 = l_Lean_Name_append___main(x_49, x_51); +x_53 = l_Array_empty___closed__1; +lean_inc(x_52); +x_54 = lean_alloc_ctor(6, 2, 0); +lean_ctor_set(x_54, 0, x_52); +lean_ctor_set(x_54, 1, x_53); +lean_inc(x_28); +x_55 = lean_alloc_ctor(0, 3, 1); +lean_ctor_set(x_55, 0, x_52); +lean_ctor_set(x_55, 1, x_53); +lean_ctor_set(x_55, 2, x_28); +lean_ctor_set_uint8(x_55, sizeof(void*)*3, x_3); +x_56 = lean_array_push(x_30, x_55); +lean_inc(x_54); +x_57 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_57, 0, x_28); +lean_ctor_set(x_57, 1, x_54); +lean_ctor_set(x_57, 2, x_31); +x_58 = lean_nat_add(x_32, x_23); +lean_dec(x_32); +x_59 = lean_alloc_ctor(0, 4, 0); +lean_ctor_set(x_59, 0, x_29); +lean_ctor_set(x_59, 1, x_56); +lean_ctor_set(x_59, 2, x_57); +lean_ctor_set(x_59, 3, x_58); +lean_ctor_set(x_6, 1, x_59); +lean_ctor_set(x_6, 0, x_54); +return x_6; } } else { -lean_object* x_51; lean_object* x_52; -lean_dec(x_24); -lean_dec(x_23); -x_51 = lean_ctor_get(x_25, 0); -lean_inc(x_51); -lean_dec(x_25); -if (lean_is_scalar(x_20)) { - x_52 = lean_alloc_ctor(0, 2, 0); -} else { - x_52 = x_20; +lean_object* x_60; +lean_dec(x_32); +lean_dec(x_31); +lean_dec(x_30); +lean_dec(x_29); +lean_dec(x_28); +x_60 = lean_ctor_get(x_33, 0); +lean_inc(x_60); +lean_dec(x_33); +lean_ctor_set(x_6, 0, x_60); +return x_6; } -lean_ctor_set(x_52, 0, x_51); -lean_ctor_set(x_52, 1, x_19); -return x_52; +} +else +{ +lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; 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_object* x_72; lean_object* x_73; +x_61 = lean_ctor_get(x_6, 1); +lean_inc(x_61); +lean_dec(x_6); +x_62 = lean_ctor_get(x_7, 0); +lean_inc(x_62); +lean_dec(x_7); +x_63 = lean_unsigned_to_nat(1u); +x_64 = lean_alloc_ctor(9, 1, 1); +lean_ctor_set(x_64, 0, x_63); +lean_ctor_set_uint8(x_64, sizeof(void*)*1, x_2); +x_65 = lean_unsigned_to_nat(2u); +x_66 = l_Lean_IR_ExplicitBoxing_mkCast___closed__2; +x_67 = lean_alloc_ctor(0, 3, 1); +lean_ctor_set(x_67, 0, x_65); +lean_ctor_set(x_67, 1, x_64); +lean_ctor_set(x_67, 2, x_66); +lean_ctor_set_uint8(x_67, sizeof(void*)*3, x_3); +x_68 = lean_alloc_ctor(0, 3, 1); +lean_ctor_set(x_68, 0, x_63); +lean_ctor_set(x_68, 1, x_62); +lean_ctor_set(x_68, 2, x_67); +lean_ctor_set_uint8(x_68, sizeof(void*)*3, x_2); +x_69 = lean_ctor_get(x_61, 0); +lean_inc(x_69); +x_70 = lean_ctor_get(x_61, 1); +lean_inc(x_70); +x_71 = lean_ctor_get(x_61, 2); +lean_inc(x_71); +x_72 = lean_ctor_get(x_61, 3); +lean_inc(x_72); +lean_inc(x_71); +lean_inc(x_68); +x_73 = l_AssocList_find___main___at_Lean_IR_ExplicitBoxing_mkCast___spec__1(x_68, x_71); +if (lean_obj_tag(x_73) == 0) +{ +lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; +if (lean_is_exclusive(x_61)) { + lean_ctor_release(x_61, 0); + lean_ctor_release(x_61, 1); + lean_ctor_release(x_61, 2); + lean_ctor_release(x_61, 3); + x_74 = x_61; +} else { + lean_dec_ref(x_61); + x_74 = lean_box(0); +} +x_75 = lean_ctor_get(x_4, 0); +x_76 = l_Lean_IR_ExplicitBoxing_mkCast___closed__4; +lean_inc(x_72); +x_77 = l_Lean_Name_appendIndexAfter(x_76, x_72); +x_78 = l_Lean_Name_append___main(x_75, x_77); +x_79 = l_Array_empty___closed__1; +lean_inc(x_78); +x_80 = lean_alloc_ctor(6, 2, 0); +lean_ctor_set(x_80, 0, x_78); +lean_ctor_set(x_80, 1, x_79); +lean_inc(x_68); +x_81 = lean_alloc_ctor(0, 3, 1); +lean_ctor_set(x_81, 0, x_78); +lean_ctor_set(x_81, 1, x_79); +lean_ctor_set(x_81, 2, x_68); +lean_ctor_set_uint8(x_81, sizeof(void*)*3, x_3); +x_82 = lean_array_push(x_70, x_81); +lean_inc(x_80); +x_83 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_83, 0, x_68); +lean_ctor_set(x_83, 1, x_80); +lean_ctor_set(x_83, 2, x_71); +x_84 = lean_nat_add(x_72, x_63); +lean_dec(x_72); +if (lean_is_scalar(x_74)) { + x_85 = lean_alloc_ctor(0, 4, 0); +} else { + x_85 = x_74; +} +lean_ctor_set(x_85, 0, x_69); +lean_ctor_set(x_85, 1, x_82); +lean_ctor_set(x_85, 2, x_83); +lean_ctor_set(x_85, 3, x_84); +x_86 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_86, 0, x_80); +lean_ctor_set(x_86, 1, x_85); +return x_86; +} +else +{ +lean_object* x_87; lean_object* x_88; +lean_dec(x_72); +lean_dec(x_71); +lean_dec(x_70); +lean_dec(x_69); +lean_dec(x_68); +x_87 = lean_ctor_get(x_73, 0); +lean_inc(x_87); +lean_dec(x_73); +x_88 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_88, 0, x_87); +lean_ctor_set(x_88, 1, x_61); +return x_88; } } } @@ -7176,8 +7294,6 @@ l_Lean_IR_ExplicitBoxing_mkBoxedName___closed__1 = _init_l_Lean_IR_ExplicitBoxin lean_mark_persistent(l_Lean_IR_ExplicitBoxing_mkBoxedName___closed__1); l_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___closed__1 = _init_l_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___closed__1(); lean_mark_persistent(l_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___closed__1); -l_Lean_IR_ExplicitBoxing_getVarType___boxed__const__1 = _init_l_Lean_IR_ExplicitBoxing_getVarType___boxed__const__1(); -lean_mark_persistent(l_Lean_IR_ExplicitBoxing_getVarType___boxed__const__1); l_Lean_IR_ExplicitBoxing_mkCast___closed__1 = _init_l_Lean_IR_ExplicitBoxing_mkCast___closed__1(); lean_mark_persistent(l_Lean_IR_ExplicitBoxing_mkCast___closed__1); l_Lean_IR_ExplicitBoxing_mkCast___closed__2 = _init_l_Lean_IR_ExplicitBoxing_mkCast___closed__2(); @@ -7186,8 +7302,6 @@ l_Lean_IR_ExplicitBoxing_mkCast___closed__3 = _init_l_Lean_IR_ExplicitBoxing_mkC lean_mark_persistent(l_Lean_IR_ExplicitBoxing_mkCast___closed__3); l_Lean_IR_ExplicitBoxing_mkCast___closed__4 = _init_l_Lean_IR_ExplicitBoxing_mkCast___closed__4(); lean_mark_persistent(l_Lean_IR_ExplicitBoxing_mkCast___closed__4); -l_Lean_IR_ExplicitBoxing_mkCast___closed__5 = _init_l_Lean_IR_ExplicitBoxing_mkCast___closed__5(); -lean_mark_persistent(l_Lean_IR_ExplicitBoxing_mkCast___closed__5); return w; } #ifdef __cplusplus diff --git a/src/stage0/init/lean/compiler/ir/compilerm.c b/src/stage0/init/lean/compiler/ir/compilerm.c index cee1d1b37e..c162950914 100644 --- a/src/stage0/init/lean/compiler/ir/compilerm.c +++ b/src/stage0/init/lean/compiler/ir/compilerm.c @@ -210,7 +210,6 @@ lean_object* l_List_foldl___main___at___private_init_lean_compiler_ir_compilerm_ lean_object* l_Lean_IR_containsDecl_x27___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_registerSimplePersistentEnvExtension___at_Lean_IR_mkDeclMapExtension___spec__9(lean_object*, lean_object*); lean_object* l_IO_Prim_Ref_reset(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_IR_containsDecl_x27___boxed__const__1; extern lean_object* l___private_init_lean_environment_5__envExtensionsRef; lean_object* l_Lean_IR_logDecls___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_declMapExt___elambda__1___boxed(lean_object*); @@ -7066,15 +7065,6 @@ return x_9; } } } -lean_object* _init_l_Lean_IR_containsDecl_x27___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Lean_IR_containsDecl_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { @@ -7132,7 +7122,7 @@ lean_object* x_23; uint8_t x_24; lean_object* x_25; x_23 = lean_ctor_get(x_4, 0); lean_dec(x_23); x_24 = 1; -x_25 = l_Lean_IR_containsDecl_x27___boxed__const__1; +x_25 = lean_box(x_24); lean_ctor_set(x_4, 0, x_25); return x_4; } @@ -7143,7 +7133,7 @@ x_26 = lean_ctor_get(x_4, 1); lean_inc(x_26); lean_dec(x_4); x_27 = 1; -x_28 = l_Lean_IR_containsDecl_x27___boxed__const__1; +x_28 = lean_box(x_27); x_29 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_29, 0, x_28); lean_ctor_set(x_29, 1, x_26); @@ -7365,8 +7355,6 @@ l_Lean_IR_declMapExt = lean_io_result_get_value(w); lean_mark_persistent(l_Lean_IR_declMapExt); l_Lean_IR_getDecl___closed__1 = _init_l_Lean_IR_getDecl___closed__1(); lean_mark_persistent(l_Lean_IR_getDecl___closed__1); -l_Lean_IR_containsDecl_x27___boxed__const__1 = _init_l_Lean_IR_containsDecl_x27___boxed__const__1(); -lean_mark_persistent(l_Lean_IR_containsDecl_x27___boxed__const__1); return w; } #ifdef __cplusplus diff --git a/src/stage0/init/lean/compiler/ir/emitc.c b/src/stage0/init/lean/compiler/ir/emitc.c index 6013154ae9..5ff5dd4721 100644 --- a/src/stage0/init/lean/compiler/ir/emitc.c +++ b/src/stage0/init/lean/compiler/ir/emitc.c @@ -316,7 +316,6 @@ uint32_t lean_string_utf8_get(lean_object*, lean_object*); lean_object* l_Lean_IR_EmitC_emitAllocCtor___boxed(lean_object*, lean_object*, lean_object*); uint8_t l_Lean_IR_EmitC_overwriteParam(lean_object*, lean_object*); lean_object* l_Lean_IR_EmitC_argToCString(lean_object*); -lean_object* l_Lean_IR_EmitC_isTailCall___boxed__const__1; lean_object* l_Lean_IR_EmitC_emitSSet___closed__1; lean_object* l_Lean_IR_EmitC_emitMainFn___closed__41; lean_object* l_Lean_IR_EmitC_emitIf___closed__3; @@ -17513,15 +17512,6 @@ lean_dec(x_4); return x_7; } } -lean_object* _init_l_Lean_IR_EmitC_isTailCall___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Lean_IR_EmitC_isTailCall(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { @@ -17548,7 +17538,7 @@ if (x_12 == 0) { uint8_t x_13; lean_object* x_14; x_13 = 0; -x_14 = l_Lean_IR_EmitC_isTailCall___boxed__const__1; +x_14 = lean_box(x_13); lean_ctor_set(x_5, 0, x_14); return x_5; } @@ -17575,7 +17565,7 @@ if (x_21 == 0) { uint8_t x_22; lean_object* x_23; lean_object* x_24; x_22 = 0; -x_23 = l_Lean_IR_EmitC_isTailCall___boxed__const__1; +x_23 = lean_box(x_22); x_24 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_24, 0, x_23); lean_ctor_set(x_24, 1, x_17); @@ -17603,7 +17593,7 @@ lean_object* x_29; uint8_t x_30; lean_object* x_31; x_29 = lean_ctor_get(x_5, 0); lean_dec(x_29); x_30 = 0; -x_31 = l_Lean_IR_EmitC_isTailCall___boxed__const__1; +x_31 = lean_box(x_30); lean_ctor_set(x_5, 0, x_31); return x_5; } @@ -17614,7 +17604,7 @@ x_32 = lean_ctor_get(x_5, 1); lean_inc(x_32); lean_dec(x_5); x_33 = 0; -x_34 = l_Lean_IR_EmitC_isTailCall___boxed__const__1; +x_34 = lean_box(x_33); x_35 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_35, 0, x_34); lean_ctor_set(x_35, 1, x_32); @@ -17632,7 +17622,7 @@ lean_object* x_37; uint8_t x_38; lean_object* x_39; x_37 = lean_ctor_get(x_5, 0); lean_dec(x_37); x_38 = 0; -x_39 = l_Lean_IR_EmitC_isTailCall___boxed__const__1; +x_39 = lean_box(x_38); lean_ctor_set(x_5, 0, x_39); return x_5; } @@ -17643,7 +17633,7 @@ x_40 = lean_ctor_get(x_5, 1); lean_inc(x_40); lean_dec(x_5); x_41 = 0; -x_42 = l_Lean_IR_EmitC_isTailCall___boxed__const__1; +x_42 = lean_box(x_41); x_43 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_43, 0, x_42); lean_ctor_set(x_43, 1, x_40); @@ -17661,7 +17651,7 @@ lean_object* x_45; uint8_t x_46; lean_object* x_47; x_45 = lean_ctor_get(x_5, 0); lean_dec(x_45); x_46 = 0; -x_47 = l_Lean_IR_EmitC_isTailCall___boxed__const__1; +x_47 = lean_box(x_46); lean_ctor_set(x_5, 0, x_47); return x_5; } @@ -17672,7 +17662,7 @@ x_48 = lean_ctor_get(x_5, 1); lean_inc(x_48); lean_dec(x_5); x_49 = 0; -x_50 = l_Lean_IR_EmitC_isTailCall___boxed__const__1; +x_50 = lean_box(x_49); x_51 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_51, 0, x_50); lean_ctor_set(x_51, 1, x_48); @@ -27628,8 +27618,6 @@ l_Lean_IR_EmitC_emitNumLit___closed__4 = _init_l_Lean_IR_EmitC_emitNumLit___clos lean_mark_persistent(l_Lean_IR_EmitC_emitNumLit___closed__4); l_Lean_IR_EmitC_emitLit___closed__1 = _init_l_Lean_IR_EmitC_emitLit___closed__1(); lean_mark_persistent(l_Lean_IR_EmitC_emitLit___closed__1); -l_Lean_IR_EmitC_isTailCall___boxed__const__1 = _init_l_Lean_IR_EmitC_isTailCall___boxed__const__1(); -lean_mark_persistent(l_Lean_IR_EmitC_isTailCall___boxed__const__1); l_Nat_mforAux___main___at_Lean_IR_EmitC_emitTailCall___spec__2___closed__1 = _init_l_Nat_mforAux___main___at_Lean_IR_EmitC_emitTailCall___spec__2___closed__1(); lean_mark_persistent(l_Nat_mforAux___main___at_Lean_IR_EmitC_emitTailCall___spec__2___closed__1); l_Nat_mforAux___main___at_Lean_IR_EmitC_emitTailCall___spec__3___closed__1 = _init_l_Nat_mforAux___main___at_Lean_IR_EmitC_emitTailCall___spec__3___closed__1(); diff --git a/src/stage0/init/lean/compiler/ir/emitutil.c b/src/stage0/init/lean/compiler/ir/emitutil.c index f0cffe8330..bd886706bc 100644 --- a/src/stage0/init/lean/compiler/ir/emitutil.c +++ b/src/stage0/init/lean/compiler/ir/emitutil.c @@ -13,7 +13,6 @@ #ifdef __cplusplus extern "C" { #endif -lean_object* l_Lean_IR_UsesLeanNamespace_visitFnBody___main___boxed__const__2; uint8_t lean_name_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_IR_CollectMaps_collectFnBody___main(lean_object*, lean_object*); lean_object* l_HashMapImp_moveEntries___main___at_Lean_IR_CollectMaps_collectJP___spec__4(lean_object*, lean_object*, lean_object*); @@ -30,7 +29,6 @@ lean_object* l_Lean_IR_FnBody_body(lean_object*); lean_object* l_Array_miterateAux___main___at_Lean_IR_CollectMaps_collectFnBody___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_uget(lean_object*, lean_object*, size_t, lean_object*); lean_object* l_Lean_IR_CollectUsedDecls_collect___boxed(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_IR_usesLeanNamespace___boxed__const__1; lean_object* l_Array_uset(lean_object*, lean_object*, size_t, lean_object*, lean_object*); lean_object* l_AssocList_replace___main___at_Lean_IR_CollectMaps_collectJP___spec__6(lean_object*, lean_object*, lean_object*); lean_object* l_HashMapImp_insert___at_Lean_IR_CollectMaps_collectVar___spec__1(lean_object*, lean_object*, uint8_t); @@ -73,7 +71,6 @@ lean_object* l_Lean_IR_CollectMaps_collectVar(lean_object*, uint8_t, lean_object lean_object* l_Array_miterateAux___main___at_Lean_IR_CollectMaps_collectParams___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_IR_FnBody_isTerminal(lean_object*); lean_object* l_Lean_IR_usesLeanNamespace___boxed(lean_object*, lean_object*); -lean_object* l_Array_anyMAux___main___at_Lean_IR_UsesLeanNamespace_visitFnBody___main___spec__1___boxed__const__1; lean_object* l_Lean_IR_CollectMaps_collectFnBody(lean_object*, lean_object*); lean_object* l_Lean_IR_usesLeanNamespace(lean_object*, lean_object*); lean_object* l_Lean_IR_findEnvDecl(lean_object*, lean_object*); @@ -93,7 +90,6 @@ uint8_t l_Lean_Name_isPrefixOf___main(lean_object*, lean_object*); lean_object* l_HashMapImp_insert___at_Lean_IR_CollectMaps_collectJP___spec__1(lean_object*, lean_object*, lean_object*); lean_object* lean_nat_mul(lean_object*, lean_object*); lean_object* l_AssocList_replace___main___at_Lean_IR_CollectMaps_collectVar___spec__6(lean_object*, uint8_t, lean_object*); -lean_object* l_Lean_IR_UsesLeanNamespace_visitFnBody___main___boxed__const__1; extern lean_object* l_Lean_Syntax_formatStx___main___rarg___closed__4; lean_object* l_Lean_IR_UsesLeanNamespace_leanNameSpacePrefix; lean_object* l_Lean_IR_CollectMaps_collectParams(lean_object*, lean_object*); @@ -180,15 +176,6 @@ x_1 = l_Lean_Syntax_formatStx___main___rarg___closed__4; return x_1; } } -lean_object* _init_l_Array_anyMAux___main___at_Lean_IR_UsesLeanNamespace_visitFnBody___main___spec__1___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Array_anyMAux___main___at_Lean_IR_UsesLeanNamespace_visitFnBody___main___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { @@ -201,7 +188,7 @@ if (x_6 == 0) uint8_t x_7; lean_object* x_8; lean_object* x_9; lean_dec(x_2); x_7 = 0; -x_8 = l_Array_anyMAux___main___at_Lean_IR_UsesLeanNamespace_visitFnBody___main___spec__1___boxed__const__1; +x_8 = lean_box(x_7); x_9 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_9, 0, x_8); lean_ctor_set(x_9, 1, x_4); @@ -258,24 +245,6 @@ return x_22; } } } -lean_object* _init_l_Lean_IR_UsesLeanNamespace_visitFnBody___main___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l_Lean_IR_UsesLeanNamespace_visitFnBody___main___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Lean_IR_UsesLeanNamespace_visitFnBody___main(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -390,7 +359,7 @@ uint8_t x_35; lean_object* x_36; lean_object* x_37; lean_dec(x_14); lean_dec(x_13); x_35 = 1; -x_36 = l_Lean_IR_UsesLeanNamespace_visitFnBody___main___boxed__const__2; +x_36 = lean_box(x_35); x_37 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_37, 0, x_36); lean_ctor_set(x_37, 1, x_3); @@ -500,7 +469,7 @@ uint8_t x_60; lean_object* x_61; lean_object* x_62; lean_dec(x_39); lean_dec(x_38); x_60 = 1; -x_61 = l_Lean_IR_UsesLeanNamespace_visitFnBody___main___boxed__const__2; +x_61 = lean_box(x_60); x_62 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_62, 0, x_61); lean_ctor_set(x_62, 1, x_3); @@ -604,7 +573,7 @@ else uint8_t x_8; lean_object* x_9; lean_object* x_10; lean_dec(x_1); x_8 = 0; -x_9 = l_Lean_IR_UsesLeanNamespace_visitFnBody___main___boxed__const__1; +x_9 = lean_box(x_8); x_10 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_10, 0, x_9); lean_ctor_set(x_10, 1, x_3); @@ -649,15 +618,6 @@ lean_dec(x_2); return x_4; } } -lean_object* _init_l_Lean_IR_usesLeanNamespace___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Lean_IR_usesLeanNamespace(lean_object* x_1, lean_object* x_2) { _start: { @@ -679,7 +639,7 @@ else uint8_t x_7; lean_object* x_8; lean_dec(x_2); x_7 = 0; -x_8 = l_Lean_IR_usesLeanNamespace___boxed__const__1; +x_8 = lean_box(x_7); return x_8; } } @@ -2129,14 +2089,6 @@ w = initialize_init_lean_compiler_ir_compilerm(w); if (lean_io_result_is_error(w)) return w; l_Lean_IR_UsesLeanNamespace_leanNameSpacePrefix = _init_l_Lean_IR_UsesLeanNamespace_leanNameSpacePrefix(); lean_mark_persistent(l_Lean_IR_UsesLeanNamespace_leanNameSpacePrefix); -l_Array_anyMAux___main___at_Lean_IR_UsesLeanNamespace_visitFnBody___main___spec__1___boxed__const__1 = _init_l_Array_anyMAux___main___at_Lean_IR_UsesLeanNamespace_visitFnBody___main___spec__1___boxed__const__1(); -lean_mark_persistent(l_Array_anyMAux___main___at_Lean_IR_UsesLeanNamespace_visitFnBody___main___spec__1___boxed__const__1); -l_Lean_IR_UsesLeanNamespace_visitFnBody___main___boxed__const__1 = _init_l_Lean_IR_UsesLeanNamespace_visitFnBody___main___boxed__const__1(); -lean_mark_persistent(l_Lean_IR_UsesLeanNamespace_visitFnBody___main___boxed__const__1); -l_Lean_IR_UsesLeanNamespace_visitFnBody___main___boxed__const__2 = _init_l_Lean_IR_UsesLeanNamespace_visitFnBody___main___boxed__const__2(); -lean_mark_persistent(l_Lean_IR_UsesLeanNamespace_visitFnBody___main___boxed__const__2); -l_Lean_IR_usesLeanNamespace___boxed__const__1 = _init_l_Lean_IR_usesLeanNamespace___boxed__const__1(); -lean_mark_persistent(l_Lean_IR_usesLeanNamespace___boxed__const__1); l_Lean_IR_mkVarJPMaps___closed__1 = _init_l_Lean_IR_mkVarJPMaps___closed__1(); lean_mark_persistent(l_Lean_IR_mkVarJPMaps___closed__1); l_Lean_IR_mkVarJPMaps___closed__2 = _init_l_Lean_IR_mkVarJPMaps___closed__2(); diff --git a/src/stage0/init/lean/compiler/ir/livevars.c b/src/stage0/init/lean/compiler/ir/livevars.c index 88df5efeee..48b44d27c6 100644 --- a/src/stage0/init/lean/compiler/ir/livevars.c +++ b/src/stage0/init/lean/compiler/ir/livevars.c @@ -32,7 +32,6 @@ lean_object* l_RBNode_del___main___at___private_init_lean_compiler_ir_livevars_8 lean_object* l___private_init_lean_compiler_ir_livevars_4__collectArray___at_Lean_IR_LiveVars_collectFnBody___main___spec__3(lean_object*, lean_object*, lean_object*); lean_object* l_Array_miterateAux___main___at___private_init_lean_compiler_ir_livevars_9__bindParams___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_init_lean_compiler_ir_livevars_5__collectArgs(lean_object*, lean_object*); -lean_object* l_Lean_IR_IsLive_visitFnBody___main___boxed__const__1; lean_object* l___private_init_lean_compiler_ir_livevars_1__skip(lean_object*); lean_object* l_Lean_IR_IsLive_visitExpr___boxed(lean_object*, lean_object*, lean_object*); lean_object* l___private_init_lean_compiler_ir_livevars_4__collectArray___rarg(lean_object*, lean_object*, lean_object*); @@ -99,7 +98,6 @@ lean_object* l_Array_miterateAux___main___at___private_init_lean_compiler_ir_liv lean_object* l_RBNode_erase___at___private_init_lean_compiler_ir_livevars_8__bindVar___spec__1___boxed(lean_object*, lean_object*); uint8_t l_Lean_IR_HasIndex_visitArg(lean_object*, lean_object*); lean_object* l_Lean_IR_mkLiveVarSet(lean_object*); -lean_object* l_Array_anyMAux___main___at_Lean_IR_IsLive_visitFnBody___main___spec__1___boxed__const__1; lean_object* l_RBNode_ins___main___at_Lean_IR_mkLiveVarSet___spec__2(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_IsLive_visitArg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_IsLive_visitVar(lean_object* x_1, lean_object* x_2, lean_object* x_3) { @@ -213,15 +211,6 @@ lean_dec(x_1); return x_4; } } -lean_object* _init_l_Array_anyMAux___main___at_Lean_IR_IsLive_visitFnBody___main___spec__1___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Array_anyMAux___main___at_Lean_IR_IsLive_visitFnBody___main___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { @@ -234,7 +223,7 @@ if (x_6 == 0) uint8_t x_7; lean_object* x_8; lean_object* x_9; lean_dec(x_3); x_7 = 0; -x_8 = l_Array_anyMAux___main___at_Lean_IR_IsLive_visitFnBody___main___spec__1___boxed__const__1; +x_8 = lean_box(x_7); x_9 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_9, 0, x_8); lean_ctor_set(x_9, 1, x_4); @@ -292,15 +281,6 @@ return x_22; } } } -lean_object* _init_l_Lean_IR_IsLive_visitFnBody___main___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Lean_IR_IsLive_visitFnBody___main(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -586,7 +566,7 @@ case 13: { uint8_t x_82; lean_object* x_83; lean_object* x_84; x_82 = 0; -x_83 = l_Lean_IR_IsLive_visitFnBody___main___boxed__const__1; +x_83 = lean_box(x_82); x_84 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_84, 0, x_83); lean_ctor_set(x_84, 1, x_3); @@ -6600,10 +6580,6 @@ w = initialize_init_control_reader(w); if (lean_io_result_is_error(w)) return w; w = initialize_init_control_conditional(w); if (lean_io_result_is_error(w)) return w; -l_Array_anyMAux___main___at_Lean_IR_IsLive_visitFnBody___main___spec__1___boxed__const__1 = _init_l_Array_anyMAux___main___at_Lean_IR_IsLive_visitFnBody___main___spec__1___boxed__const__1(); -lean_mark_persistent(l_Array_anyMAux___main___at_Lean_IR_IsLive_visitFnBody___main___spec__1___boxed__const__1); -l_Lean_IR_IsLive_visitFnBody___main___boxed__const__1 = _init_l_Lean_IR_IsLive_visitFnBody___main___boxed__const__1(); -lean_mark_persistent(l_Lean_IR_IsLive_visitFnBody___main___boxed__const__1); l_Lean_IR_LiveVarSet_inhabited = _init_l_Lean_IR_LiveVarSet_inhabited(); lean_mark_persistent(l_Lean_IR_LiveVarSet_inhabited); l___private_init_lean_compiler_ir_livevars_6__accumulate___closed__1 = _init_l___private_init_lean_compiler_ir_livevars_6__accumulate___closed__1(); diff --git a/src/stage0/init/lean/compiler/ir/normids.c b/src/stage0/init/lean/compiler/ir/normids.c index e6ab10a0a0..f0cc1978cb 100644 --- a/src/stage0/init/lean/compiler/ir/normids.c +++ b/src/stage0/init/lean/compiler/ir/normids.c @@ -16,11 +16,8 @@ extern "C" { lean_object* l_Lean_IR_MapVars_mapExpr(lean_object*, lean_object*); lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_NormalizeIds_withVar___rarg(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_IR_UniqueIds_checkParams___boxed__const__1; -lean_object* l_Lean_IR_UniqueIds_checkId___boxed__const__2; lean_object* l_Lean_IR_UniqueIds_checkParams___boxed(lean_object*, lean_object*); lean_object* l_Lean_IR_NormalizeIds_normArg(lean_object*, lean_object*); -lean_object* l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1___boxed__const__1; lean_object* l_Lean_IR_MapVars_mapArgs___at_Lean_IR_FnBody_replaceVar___spec__5___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1(lean_object*, lean_object*, lean_object*); extern lean_object* l_Array_empty___closed__1; @@ -43,12 +40,9 @@ lean_object* l_Lean_IR_Decl_uniqueIds(lean_object*); lean_object* l_Lean_IR_NormalizeIds_normArgs___boxed(lean_object*, lean_object*); lean_object* l_Array_ummapAux___main___at_Lean_IR_NormalizeIds_normFnBody___main___spec__2___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_RBNode_findCore___main___at_Lean_IR_UniqueIds_checkId___spec__1(lean_object*, lean_object*); -lean_object* l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1___boxed__const__1; lean_object* l_Lean_IR_UniqueIds_checkFnBody(lean_object*, lean_object*); lean_object* l_Lean_IR_MapVars_mapArgs___at_Lean_IR_FnBody_replaceVar___spec__14___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_MapVars_mapFnBody___main___at_Lean_IR_FnBody_replaceVar___spec__1(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_IR_UniqueIds_checkFnBody___main___boxed__const__1; -lean_object* l_Lean_IR_UniqueIds_checkParams___boxed__const__2; lean_object* l_Lean_IR_NormalizeIds_normVar(lean_object*, lean_object*); lean_object* l_Lean_IR_MapVars_mapArgs___at_Lean_IR_FnBody_replaceVar___spec__3(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_NormalizeIds_normArg___boxed(lean_object*, lean_object*); @@ -63,7 +57,6 @@ lean_object* l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1 lean_object* l_Lean_IR_MapVars_mapFnBody___main___at_Lean_IR_FnBody_replaceVar___spec__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_AltCore_body(lean_object*); lean_object* l_Array_ummapAux___main___at_Lean_IR_NormalizeIds_normFnBody___main___spec__3(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_IR_UniqueIds_checkId___boxed__const__1; lean_object* l_Array_miterateAux___main___at_Lean_IR_NormalizeIds_normFnBody___main___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_UniqueIds_checkDecl(lean_object*, lean_object*); lean_object* l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1(lean_object*, lean_object*, lean_object*); @@ -78,7 +71,6 @@ lean_object* lean_nat_add(lean_object*, lean_object*); lean_object* l_Array_ummapAux___main___at_Lean_IR_FnBody_replaceVar___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_nat_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_IR_NormalizeIds_normArgs(lean_object*, lean_object*); -lean_object* l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1___boxed__const__2; lean_object* l_Lean_IR_NormalizeIds_normExpr(lean_object*, lean_object*); lean_object* l_Array_ummapAux___main___at_Lean_IR_FnBody_replaceVar___spec__10(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_MapVars_mapArgs___at_Lean_IR_FnBody_replaceVar___spec__11___boxed(lean_object*, lean_object*, lean_object*); @@ -86,7 +78,6 @@ lean_object* l_Lean_IR_NormalizeIds_normIndex___boxed(lean_object*, lean_object* lean_object* l_Lean_IR_MapVars_mapFnBody___main(lean_object*, lean_object*); lean_object* l_Lean_IR_MapVars_mapArgs___at_Lean_IR_FnBody_replaceVar___spec__3___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Array_ummapAux___main___at_Lean_IR_FnBody_replaceVar___spec__13___boxed(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1___boxed__const__2; lean_object* l_RBNode_findCore___main___at_Lean_IR_UniqueIds_checkId___spec__1___boxed(lean_object*, lean_object*); lean_object* l_Array_ummapAux___main___at_Lean_IR_FnBody_replaceVar___spec__13(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_IR_FnBody_isTerminal(lean_object*); @@ -118,7 +109,6 @@ lean_object* l_Array_ummapAux___main___at_Lean_IR_NormalizeIds_withParams___spec lean_object* l_Lean_IR_MapVars_mapArg(lean_object*, lean_object*); lean_object* l_RBNode_insert___at_Lean_IR_addVarRename___spec__1(lean_object*, lean_object*, lean_object*); lean_object* l_Array_ummapAux___main___at_Lean_IR_FnBody_replaceVar___spec__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_IR_UniqueIds_checkFnBody___main___boxed__const__2; lean_object* l_Lean_IR_NormalizeIds_withJP___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_UniqueIds_checkId(lean_object*, lean_object*); lean_object* l_Lean_IR_MapVars_mapArgs___at_Lean_IR_FnBody_replaceVar___spec__14(lean_object*, lean_object*, lean_object*); @@ -176,24 +166,6 @@ goto _start; } } } -lean_object* _init_l_Lean_IR_UniqueIds_checkId___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l_Lean_IR_UniqueIds_checkId___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Lean_IR_UniqueIds_checkId(lean_object* x_1, lean_object* x_2) { _start: { @@ -205,7 +177,7 @@ lean_object* x_4; lean_object* x_5; uint8_t x_6; lean_object* x_7; lean_object* x_4 = lean_box(0); x_5 = l_RBNode_insert___at_Lean_IR_mkIndexSet___spec__1(x_2, x_1, x_4); x_6 = 1; -x_7 = l_Lean_IR_UniqueIds_checkId___boxed__const__1; +x_7 = lean_box(x_6); x_8 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_8, 0, x_7); lean_ctor_set(x_8, 1, x_5); @@ -217,7 +189,7 @@ uint8_t x_9; lean_object* x_10; lean_object* x_11; lean_dec(x_3); lean_dec(x_1); x_9 = 0; -x_10 = l_Lean_IR_UniqueIds_checkId___boxed__const__2; +x_10 = lean_box(x_9); x_11 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_11, 0, x_10); lean_ctor_set(x_11, 1, x_2); @@ -235,24 +207,6 @@ lean_dec(x_1); return x_3; } } -lean_object* _init_l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -265,7 +219,7 @@ if (x_5 == 0) uint8_t x_6; lean_object* x_7; lean_object* x_8; lean_dec(x_2); x_6 = 0; -x_7 = l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1___boxed__const__1; +x_7 = lean_box(x_6); x_8 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_8, 0, x_7); lean_ctor_set(x_8, 1, x_3); @@ -294,7 +248,7 @@ lean_object* x_15; uint8_t x_16; lean_object* x_17; x_15 = lean_ctor_get(x_11, 0); lean_dec(x_15); x_16 = 1; -x_17 = l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1___boxed__const__2; +x_17 = lean_box(x_16); lean_ctor_set(x_11, 0, x_17); return x_11; } @@ -305,7 +259,7 @@ x_18 = lean_ctor_get(x_11, 1); lean_inc(x_18); lean_dec(x_11); x_19 = 1; -x_20 = l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1___boxed__const__2; +x_20 = lean_box(x_19); x_21 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_21, 0, x_20); lean_ctor_set(x_21, 1, x_18); @@ -328,24 +282,6 @@ goto _start; } } } -lean_object* _init_l_Lean_IR_UniqueIds_checkParams___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l_Lean_IR_UniqueIds_checkParams___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Lean_IR_UniqueIds_checkParams(lean_object* x_1, lean_object* x_2) { _start: { @@ -366,7 +302,7 @@ lean_object* x_8; uint8_t x_9; lean_object* x_10; x_8 = lean_ctor_get(x_4, 0); lean_dec(x_8); x_9 = 1; -x_10 = l_Lean_IR_UniqueIds_checkParams___boxed__const__1; +x_10 = lean_box(x_9); lean_ctor_set(x_4, 0, x_10); return x_4; } @@ -377,7 +313,7 @@ x_11 = lean_ctor_get(x_4, 1); lean_inc(x_11); lean_dec(x_4); x_12 = 1; -x_13 = l_Lean_IR_UniqueIds_checkParams___boxed__const__1; +x_13 = lean_box(x_12); x_14 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_14, 0, x_13); lean_ctor_set(x_14, 1, x_11); @@ -394,7 +330,7 @@ lean_object* x_16; uint8_t x_17; lean_object* x_18; x_16 = lean_ctor_get(x_4, 0); lean_dec(x_16); x_17 = 0; -x_18 = l_Lean_IR_UniqueIds_checkParams___boxed__const__2; +x_18 = lean_box(x_17); lean_ctor_set(x_4, 0, x_18); return x_4; } @@ -405,7 +341,7 @@ x_19 = lean_ctor_get(x_4, 1); lean_inc(x_19); lean_dec(x_4); x_20 = 0; -x_21 = l_Lean_IR_UniqueIds_checkParams___boxed__const__2; +x_21 = lean_box(x_20); x_22 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_22, 0, x_21); lean_ctor_set(x_22, 1, x_19); @@ -432,24 +368,6 @@ lean_dec(x_1); return x_3; } } -lean_object* _init_l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -462,7 +380,7 @@ if (x_5 == 0) uint8_t x_6; lean_object* x_7; lean_object* x_8; lean_dec(x_2); x_6 = 0; -x_7 = l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1___boxed__const__1; +x_7 = lean_box(x_6); x_8 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_8, 0, x_7); lean_ctor_set(x_8, 1, x_3); @@ -490,7 +408,7 @@ lean_object* x_15; uint8_t x_16; lean_object* x_17; x_15 = lean_ctor_get(x_11, 0); lean_dec(x_15); x_16 = 1; -x_17 = l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1___boxed__const__2; +x_17 = lean_box(x_16); lean_ctor_set(x_11, 0, x_17); return x_11; } @@ -501,7 +419,7 @@ x_18 = lean_ctor_get(x_11, 1); lean_inc(x_18); lean_dec(x_11); x_19 = 1; -x_20 = l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1___boxed__const__2; +x_20 = lean_box(x_19); x_21 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_21, 0, x_20); lean_ctor_set(x_21, 1, x_18); @@ -524,24 +442,6 @@ goto _start; } } } -lean_object* _init_l_Lean_IR_UniqueIds_checkFnBody___main___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l_Lean_IR_UniqueIds_checkFnBody___main___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Lean_IR_UniqueIds_checkFnBody___main(lean_object* x_1, lean_object* x_2) { _start: { @@ -706,7 +606,7 @@ lean_object* x_48; uint8_t x_49; lean_object* x_50; x_48 = lean_ctor_get(x_44, 0); lean_dec(x_48); x_49 = 1; -x_50 = l_Lean_IR_UniqueIds_checkFnBody___main___boxed__const__1; +x_50 = lean_box(x_49); lean_ctor_set(x_44, 0, x_50); return x_44; } @@ -717,7 +617,7 @@ x_51 = lean_ctor_get(x_44, 1); lean_inc(x_51); lean_dec(x_44); x_52 = 1; -x_53 = l_Lean_IR_UniqueIds_checkFnBody___main___boxed__const__1; +x_53 = lean_box(x_52); x_54 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_54, 0, x_53); lean_ctor_set(x_54, 1, x_51); @@ -734,7 +634,7 @@ lean_object* x_56; uint8_t x_57; lean_object* x_58; x_56 = lean_ctor_get(x_44, 0); lean_dec(x_56); x_57 = 0; -x_58 = l_Lean_IR_UniqueIds_checkFnBody___main___boxed__const__2; +x_58 = lean_box(x_57); lean_ctor_set(x_44, 0, x_58); return x_44; } @@ -745,7 +645,7 @@ x_59 = lean_ctor_get(x_44, 1); lean_inc(x_59); lean_dec(x_44); x_60 = 0; -x_61 = l_Lean_IR_UniqueIds_checkFnBody___main___boxed__const__2; +x_61 = lean_box(x_60); x_62 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_62, 0, x_61); lean_ctor_set(x_62, 1, x_59); @@ -779,7 +679,7 @@ else uint8_t x_7; lean_object* x_8; lean_object* x_9; lean_dec(x_1); x_7 = 1; -x_8 = l_Lean_IR_UniqueIds_checkFnBody___main___boxed__const__1; +x_8 = lean_box(x_7); x_9 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_9, 0, x_8); lean_ctor_set(x_9, 1, x_2); @@ -6680,26 +6580,6 @@ w = initialize_init_control_conditional(w); if (lean_io_result_is_error(w)) return w; w = initialize_init_lean_compiler_ir_basic(w); if (lean_io_result_is_error(w)) return w; -l_Lean_IR_UniqueIds_checkId___boxed__const__1 = _init_l_Lean_IR_UniqueIds_checkId___boxed__const__1(); -lean_mark_persistent(l_Lean_IR_UniqueIds_checkId___boxed__const__1); -l_Lean_IR_UniqueIds_checkId___boxed__const__2 = _init_l_Lean_IR_UniqueIds_checkId___boxed__const__2(); -lean_mark_persistent(l_Lean_IR_UniqueIds_checkId___boxed__const__2); -l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1___boxed__const__1 = _init_l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1___boxed__const__1(); -lean_mark_persistent(l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1___boxed__const__1); -l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1___boxed__const__2 = _init_l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1___boxed__const__2(); -lean_mark_persistent(l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkParams___spec__1___boxed__const__2); -l_Lean_IR_UniqueIds_checkParams___boxed__const__1 = _init_l_Lean_IR_UniqueIds_checkParams___boxed__const__1(); -lean_mark_persistent(l_Lean_IR_UniqueIds_checkParams___boxed__const__1); -l_Lean_IR_UniqueIds_checkParams___boxed__const__2 = _init_l_Lean_IR_UniqueIds_checkParams___boxed__const__2(); -lean_mark_persistent(l_Lean_IR_UniqueIds_checkParams___boxed__const__2); -l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1___boxed__const__1 = _init_l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1___boxed__const__1(); -lean_mark_persistent(l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1___boxed__const__1); -l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1___boxed__const__2 = _init_l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1___boxed__const__2(); -lean_mark_persistent(l_Array_anyMAux___main___at_Lean_IR_UniqueIds_checkFnBody___main___spec__1___boxed__const__2); -l_Lean_IR_UniqueIds_checkFnBody___main___boxed__const__1 = _init_l_Lean_IR_UniqueIds_checkFnBody___main___boxed__const__1(); -lean_mark_persistent(l_Lean_IR_UniqueIds_checkFnBody___main___boxed__const__1); -l_Lean_IR_UniqueIds_checkFnBody___main___boxed__const__2 = _init_l_Lean_IR_UniqueIds_checkFnBody___main___boxed__const__2(); -lean_mark_persistent(l_Lean_IR_UniqueIds_checkFnBody___main___boxed__const__2); return w; } #ifdef __cplusplus diff --git a/src/stage0/init/lean/compiler/ir/resetreuse.c b/src/stage0/init/lean/compiler/ir/resetreuse.c index 52fba61623..460307c917 100644 --- a/src/stage0/init/lean/compiler/ir/resetreuse.c +++ b/src/stage0/init/lean/compiler/ir/resetreuse.c @@ -17,7 +17,6 @@ lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object* lean_object* l_Lean_IR_FnBody_setBody(lean_object*, lean_object*); uint8_t lean_name_dec_eq(lean_object*, lean_object*); extern lean_object* l_Array_empty___closed__1; -lean_object* l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__1; lean_object* l_Lean_IR_ResetReuse_R___main(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_MaxIndex_collectDecl(lean_object*, lean_object*); lean_object* l___private_init_lean_compiler_ir_resetreuse_3__mkFresh___boxed(lean_object*); @@ -37,7 +36,6 @@ lean_object* l___private_init_lean_compiler_ir_resetreuse_9__D(lean_object*, lea lean_object* l_Lean_Name_getPrefix(lean_object*); lean_object* l_Array_fget(lean_object*, lean_object*, lean_object*); lean_object* lean_nat_add(lean_object*, lean_object*); -lean_object* l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__2; uint8_t l_Lean_IR_CtorInfo_isScalar(lean_object*); uint8_t lean_nat_dec_eq(lean_object*, lean_object*); uint8_t l___private_init_lean_compiler_ir_resetreuse_6__argsContainsVar(lean_object*, lean_object*); @@ -924,24 +922,6 @@ goto _start; } } } -lean_object* _init_l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { @@ -1138,7 +1118,7 @@ lean_dec(x_135); lean_dec(x_4); lean_dec(x_1); x_140 = 0; -x_141 = l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__2; +x_141 = lean_box(x_140); x_142 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_142, 0, x_3); lean_ctor_set(x_142, 1, x_141); @@ -1170,7 +1150,7 @@ x_151 = lean_ctor_get(x_149, 0); x_152 = lean_ctor_get(x_149, 1); lean_ctor_set(x_3, 2, x_151); x_153 = 1; -x_154 = l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__1; +x_154 = lean_box(x_153); lean_ctor_set(x_149, 1, x_154); lean_ctor_set(x_149, 0, x_3); x_155 = lean_alloc_ctor(0, 2, 0); @@ -1188,7 +1168,7 @@ lean_inc(x_156); lean_dec(x_149); lean_ctor_set(x_3, 2, x_156); x_158 = 1; -x_159 = l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__1; +x_159 = lean_box(x_158); x_160 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_160, 0, x_3); lean_ctor_set(x_160, 1, x_159); @@ -1221,7 +1201,7 @@ lean_ctor_set(x_167, 0, x_135); lean_ctor_set(x_167, 1, x_136); lean_ctor_set(x_167, 2, x_164); x_168 = 1; -x_169 = l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__1; +x_169 = lean_box(x_168); if (lean_is_scalar(x_166)) { x_170 = lean_alloc_ctor(0, 2, 0); } else { @@ -1311,7 +1291,7 @@ x_26 = lean_ctor_get(x_24, 0); x_27 = lean_ctor_get(x_24, 1); x_28 = l_Lean_IR_FnBody_setBody(x_10, x_26); x_29 = 1; -x_30 = l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__1; +x_30 = lean_box(x_29); lean_ctor_set(x_24, 1, x_30); lean_ctor_set(x_24, 0, x_28); lean_ctor_set(x_13, 1, x_27); @@ -1328,7 +1308,7 @@ lean_inc(x_31); lean_dec(x_24); x_33 = l_Lean_IR_FnBody_setBody(x_10, x_31); x_34 = 1; -x_35 = l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__1; +x_35 = lean_box(x_34); x_36 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_36, 0, x_33); lean_ctor_set(x_36, 1, x_35); @@ -1378,7 +1358,7 @@ if (lean_is_exclusive(x_41)) { } x_45 = l_Lean_IR_FnBody_setBody(x_10, x_42); x_46 = 1; -x_47 = l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__1; +x_47 = lean_box(x_46); if (lean_is_scalar(x_44)) { x_48 = lean_alloc_ctor(0, 2, 0); } else { @@ -1448,7 +1428,7 @@ if (lean_is_exclusive(x_57)) { } x_61 = l_Lean_IR_FnBody_setBody(x_10, x_58); x_62 = 1; -x_63 = l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__1; +x_63 = lean_box(x_62); if (lean_is_scalar(x_60)) { x_64 = lean_alloc_ctor(0, 2, 0); } else { @@ -1542,7 +1522,7 @@ lean_dec(x_8); lean_dec(x_4); lean_dec(x_1); x_81 = 1; -x_82 = l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__1; +x_82 = lean_box(x_81); x_83 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_83, 0, x_3); lean_ctor_set(x_83, 1, x_82); @@ -2075,10 +2055,6 @@ w = initialize_init_lean_compiler_ir_livevars(w); if (lean_io_result_is_error(w)) return w; w = initialize_init_lean_compiler_ir_format(w); if (lean_io_result_is_error(w)) return w; -l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__1 = _init_l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__1(); -lean_mark_persistent(l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__1); -l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__2 = _init_l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__2(); -lean_mark_persistent(l___private_init_lean_compiler_ir_resetreuse_8__Dmain___main___boxed__const__2); return w; } #ifdef __cplusplus diff --git a/src/stage0/init/lean/compiler/specialize.c b/src/stage0/init/lean/compiler/specialize.c index a418cc2c31..36f13f7b96 100644 --- a/src/stage0/init/lean/compiler/specialize.c +++ b/src/stage0/init/lean/compiler/specialize.c @@ -27,7 +27,6 @@ extern lean_object* l_Array_empty___closed__1; lean_object* l_RBNode_fold___main___at_Lean_Compiler_mkSpecializeAttrs___spec__2(lean_object*, lean_object*); lean_object* lean_nat_sub(lean_object*, lean_object*); extern lean_object* l_Lean_registerEnvExtensionUnsafe___rarg___closed__2; -lean_object* l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkSpecializeAttrs___spec__4___closed__1___boxed__const__1; lean_object* l_Lean_Compiler_mkSpecExtension___closed__2; lean_object* l_Lean_SMap_find___at_Lean_Compiler_getCachedSpecialization___spec__1(lean_object*, lean_object*); lean_object* l_Lean_Compiler_specExtension___closed__2; @@ -130,7 +129,6 @@ lean_object* l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_ lean_object* l_Lean_Compiler_specExtension___closed__3; lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Compiler_SpecializeAttributeKind_Inhabited; -lean_object* l_Lean_Compiler_mkSpecializeAttrs___closed__6___boxed__const__1; lean_object* lean_cache_specialization(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Name_getPrefix(lean_object*); lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Compiler_mkSpecExtension___spec__7___closed__2; @@ -146,7 +144,6 @@ lean_object* l_Lean_Compiler_mkSpecializeAttrs___closed__7; extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__3; uint8_t lean_nat_dec_eq(lean_object*, lean_object*); lean_object* l_HashMapImp_expand___at_Lean_Compiler_SpecState_addEntry___spec__15(lean_object*, lean_object*); -lean_object* l_Lean_Compiler_mkSpecializeAttrs___closed__11___boxed__const__1; lean_object* l_Lean_Compiler_specExtension___closed__6; lean_object* l_Array_push(lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Compiler_SpecializeAttributeKind_beq(uint8_t, uint8_t); @@ -196,7 +193,6 @@ lean_object* l_Array_fset(lean_object*, lean_object*, lean_object*, lean_object* lean_object* l_Array_get(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_mkHashMapImp___rarg(lean_object*); lean_object* l_RBNode_setBlack___rarg(lean_object*); -lean_object* l_Lean_EnumAttributes_getValue___at___private_init_lean_compiler_specialize_1__hasSpecializeAttrAux___main___spec__1___boxed__const__1; lean_object* l_Array_miterateAux___main___at_Lean_Compiler_mkSpecExtension___spec__3(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_map___main___at_Lean_Compiler_mkSpecializeAttrs___spec__8___lambda__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*); extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__5; @@ -342,22 +338,13 @@ goto _start; } } } -lean_object* _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkSpecializeAttrs___spec__4___closed__1___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = l_Lean_Compiler_SpecializeAttributeKind_Inhabited; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkSpecializeAttrs___spec__4___closed__1() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Inhabited; x_2 = l_Lean_Compiler_SpecializeAttributeKind_Inhabited; -x_3 = l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkSpecializeAttrs___spec__4___closed__1___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -2874,22 +2861,13 @@ x_1 = lean_mk_string("mark definition to always be inlined"); return x_1; } } -lean_object* _init_l_Lean_Compiler_mkSpecializeAttrs___closed__6___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_Compiler_mkSpecializeAttrs___closed__6() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Compiler_mkSpecializeAttrs___closed__5; x_2 = 0; -x_3 = l_Lean_Compiler_mkSpecializeAttrs___closed__6___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -2934,22 +2912,13 @@ x_1 = lean_mk_string("mark definition to never be inlined"); return x_1; } } -lean_object* _init_l_Lean_Compiler_mkSpecializeAttrs___closed__11___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_Compiler_mkSpecializeAttrs___closed__11() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Compiler_mkSpecializeAttrs___closed__10; x_2 = 1; -x_3 = l_Lean_Compiler_mkSpecializeAttrs___closed__11___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -3206,15 +3175,6 @@ goto _start; } } } -lean_object* _init_l_Lean_EnumAttributes_getValue___at___private_init_lean_compiler_specialize_1__hasSpecializeAttrAux___main___spec__1___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Lean_EnumAttributes_getValue___at___private_init_lean_compiler_specialize_1__hasSpecializeAttrAux___main___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -3244,7 +3204,7 @@ lean_dec(x_1); x_10 = l_Lean_PersistentEnvExtension_getModuleEntries___rarg(x_9, x_2, x_8); lean_dec(x_8); x_11 = 0; -x_12 = l_Lean_EnumAttributes_getValue___at___private_init_lean_compiler_specialize_1__hasSpecializeAttrAux___main___spec__1___boxed__const__1; +x_12 = lean_box(x_11); x_13 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_13, 0, x_3); lean_ctor_set(x_13, 1, x_12); @@ -11938,8 +11898,6 @@ l_Lean_Compiler_SpecializeAttributeKind_HasBeq___closed__1 = _init_l_Lean_Compil lean_mark_persistent(l_Lean_Compiler_SpecializeAttributeKind_HasBeq___closed__1); l_Lean_Compiler_SpecializeAttributeKind_HasBeq = _init_l_Lean_Compiler_SpecializeAttributeKind_HasBeq(); lean_mark_persistent(l_Lean_Compiler_SpecializeAttributeKind_HasBeq); -l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkSpecializeAttrs___spec__4___closed__1___boxed__const__1 = _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkSpecializeAttrs___spec__4___closed__1___boxed__const__1(); -lean_mark_persistent(l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkSpecializeAttrs___spec__4___closed__1___boxed__const__1); l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkSpecializeAttrs___spec__4___closed__1 = _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkSpecializeAttrs___spec__4___closed__1(); lean_mark_persistent(l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_Compiler_mkSpecializeAttrs___spec__4___closed__1); l_Lean_registerEnumAttributes___at_Lean_Compiler_mkSpecializeAttrs___spec__1___closed__1 = _init_l_Lean_registerEnumAttributes___at_Lean_Compiler_mkSpecializeAttrs___spec__1___closed__1(); @@ -11956,8 +11914,6 @@ l_Lean_Compiler_mkSpecializeAttrs___closed__4 = _init_l_Lean_Compiler_mkSpeciali lean_mark_persistent(l_Lean_Compiler_mkSpecializeAttrs___closed__4); l_Lean_Compiler_mkSpecializeAttrs___closed__5 = _init_l_Lean_Compiler_mkSpecializeAttrs___closed__5(); lean_mark_persistent(l_Lean_Compiler_mkSpecializeAttrs___closed__5); -l_Lean_Compiler_mkSpecializeAttrs___closed__6___boxed__const__1 = _init_l_Lean_Compiler_mkSpecializeAttrs___closed__6___boxed__const__1(); -lean_mark_persistent(l_Lean_Compiler_mkSpecializeAttrs___closed__6___boxed__const__1); l_Lean_Compiler_mkSpecializeAttrs___closed__6 = _init_l_Lean_Compiler_mkSpecializeAttrs___closed__6(); lean_mark_persistent(l_Lean_Compiler_mkSpecializeAttrs___closed__6); l_Lean_Compiler_mkSpecializeAttrs___closed__7 = _init_l_Lean_Compiler_mkSpecializeAttrs___closed__7(); @@ -11968,8 +11924,6 @@ l_Lean_Compiler_mkSpecializeAttrs___closed__9 = _init_l_Lean_Compiler_mkSpeciali lean_mark_persistent(l_Lean_Compiler_mkSpecializeAttrs___closed__9); l_Lean_Compiler_mkSpecializeAttrs___closed__10 = _init_l_Lean_Compiler_mkSpecializeAttrs___closed__10(); lean_mark_persistent(l_Lean_Compiler_mkSpecializeAttrs___closed__10); -l_Lean_Compiler_mkSpecializeAttrs___closed__11___boxed__const__1 = _init_l_Lean_Compiler_mkSpecializeAttrs___closed__11___boxed__const__1(); -lean_mark_persistent(l_Lean_Compiler_mkSpecializeAttrs___closed__11___boxed__const__1); l_Lean_Compiler_mkSpecializeAttrs___closed__11 = _init_l_Lean_Compiler_mkSpecializeAttrs___closed__11(); lean_mark_persistent(l_Lean_Compiler_mkSpecializeAttrs___closed__11); l_Lean_Compiler_mkSpecializeAttrs___closed__12 = _init_l_Lean_Compiler_mkSpecializeAttrs___closed__12(); @@ -11984,8 +11938,6 @@ w = l_Lean_Compiler_mkSpecializeAttrs(w); if (lean_io_result_is_error(w)) return w; l_Lean_Compiler_specializeAttrs = lean_io_result_get_value(w); lean_mark_persistent(l_Lean_Compiler_specializeAttrs); -l_Lean_EnumAttributes_getValue___at___private_init_lean_compiler_specialize_1__hasSpecializeAttrAux___main___spec__1___boxed__const__1 = _init_l_Lean_EnumAttributes_getValue___at___private_init_lean_compiler_specialize_1__hasSpecializeAttrAux___main___spec__1___boxed__const__1(); -lean_mark_persistent(l_Lean_EnumAttributes_getValue___at___private_init_lean_compiler_specialize_1__hasSpecializeAttrAux___main___spec__1___boxed__const__1); l_Lean_Compiler_SpecState_Inhabited___closed__1 = _init_l_Lean_Compiler_SpecState_Inhabited___closed__1(); lean_mark_persistent(l_Lean_Compiler_SpecState_Inhabited___closed__1); l_Lean_Compiler_SpecState_Inhabited___closed__2 = _init_l_Lean_Compiler_SpecState_Inhabited___closed__2(); diff --git a/src/stage0/init/lean/elaborator/basic.c b/src/stage0/init/lean/elaborator/basic.c index f56afc9d78..5452e73bf9 100644 --- a/src/stage0/init/lean/elaborator/basic.c +++ b/src/stage0/init/lean/elaborator/basic.c @@ -251,7 +251,6 @@ uint8_t l_Lean_Parser_isEOI(lean_object*); lean_object* l_Lean_mkElabAttribute(lean_object*); lean_object* l_HashMapImp_contains___at_Lean_addBuiltinTermElab___spec__2___boxed(lean_object*, lean_object*); lean_object* l_Lean_registerBuiltinTermElabAttr___lambda__1___closed__5; -lean_object* l_Lean_Elab_processCommand___boxed__const__1; lean_object* l_Array_miterateAux___main___at_Lean_Elab_processHeaderAux___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkCommandElabAttribute(lean_object*); lean_object* l_Lean_syntaxNodeKindOfAttrParam___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -295,7 +294,6 @@ lean_object* l_Lean_Elab_getElabContext(lean_object*, lean_object*); lean_object* l_Lean_registerBuiltinTermElabAttr___closed__2; lean_object* l_HashMapImp_moveEntries___main___at_Lean_addBuiltinTermElab___spec__10(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_runBuiltinParserUnsafe___closed__2; -lean_object* l_Lean_Elab_processCommand___boxed__const__2; lean_object* l_RBNode_find___main___at_Lean_addBuiltinTermElab___spec__4___boxed(lean_object*, lean_object*); extern lean_object* l_Lean_AttributeImpl_inhabited___closed__6; lean_object* l_Lean_addBuiltinCommandElab___closed__1; @@ -15880,24 +15878,6 @@ return x_58; } } } -lean_object* _init_l_Lean_Elab_processCommand___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l_Lean_Elab_processCommand___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Lean_Elab_processCommand(lean_object* x_1, lean_object* x_2) { _start: { @@ -15966,7 +15946,7 @@ lean_object* x_23; uint8_t x_24; lean_object* x_25; x_23 = lean_ctor_get(x_21, 0); lean_dec(x_23); x_24 = 0; -x_25 = l_Lean_Elab_processCommand___boxed__const__1; +x_25 = lean_box(x_24); lean_ctor_set(x_21, 0, x_25); return x_21; } @@ -15977,7 +15957,7 @@ x_26 = lean_ctor_get(x_21, 1); lean_inc(x_26); lean_dec(x_21); x_27 = 0; -x_28 = l_Lean_Elab_processCommand___boxed__const__1; +x_28 = lean_box(x_27); x_29 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_29, 0, x_28); lean_ctor_set(x_29, 1, x_26); @@ -16006,7 +15986,7 @@ lean_object* x_34; uint8_t x_35; lean_object* x_36; x_34 = lean_ctor_get(x_32, 0); lean_dec(x_34); x_35 = 0; -x_36 = l_Lean_Elab_processCommand___boxed__const__1; +x_36 = lean_box(x_35); lean_ctor_set(x_32, 0, x_36); return x_32; } @@ -16017,7 +15997,7 @@ x_37 = lean_ctor_get(x_32, 1); lean_inc(x_37); lean_dec(x_32); x_38 = 0; -x_39 = l_Lean_Elab_processCommand___boxed__const__1; +x_39 = lean_box(x_38); x_40 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_40, 0, x_39); lean_ctor_set(x_40, 1, x_37); @@ -16074,7 +16054,7 @@ if (lean_is_exclusive(x_48)) { x_50 = lean_box(0); } x_51 = 0; -x_52 = l_Lean_Elab_processCommand___boxed__const__1; +x_52 = lean_box(x_51); if (lean_is_scalar(x_50)) { x_53 = lean_alloc_ctor(0, 2, 0); } else { @@ -16118,7 +16098,7 @@ lean_dec(x_3); lean_dec(x_14); lean_dec(x_1); x_58 = 1; -x_59 = l_Lean_Elab_processCommand___boxed__const__2; +x_59 = lean_box(x_58); x_60 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_60, 0, x_59); lean_ctor_set(x_60, 1, x_17); @@ -16132,7 +16112,7 @@ lean_dec(x_3); lean_dec(x_14); lean_dec(x_1); x_61 = 1; -x_62 = l_Lean_Elab_processCommand___boxed__const__2; +x_62 = lean_box(x_61); x_63 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_63, 0, x_62); lean_ctor_set(x_63, 1, x_17); @@ -16207,7 +16187,7 @@ if (lean_is_exclusive(x_80)) { x_82 = lean_box(0); } x_83 = 0; -x_84 = l_Lean_Elab_processCommand___boxed__const__1; +x_84 = lean_box(x_83); if (lean_is_scalar(x_82)) { x_85 = lean_alloc_ctor(0, 2, 0); } else { @@ -16256,7 +16236,7 @@ if (lean_is_exclusive(x_90)) { x_92 = lean_box(0); } x_93 = 0; -x_94 = l_Lean_Elab_processCommand___boxed__const__1; +x_94 = lean_box(x_93); if (lean_is_scalar(x_92)) { x_95 = lean_alloc_ctor(0, 2, 0); } else { @@ -16299,7 +16279,7 @@ lean_dec(x_3); lean_dec(x_72); lean_dec(x_1); x_100 = 1; -x_101 = l_Lean_Elab_processCommand___boxed__const__2; +x_101 = lean_box(x_100); x_102 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_102, 0, x_101); lean_ctor_set(x_102, 1, x_76); @@ -16313,7 +16293,7 @@ lean_dec(x_3); lean_dec(x_72); lean_dec(x_1); x_103 = 1; -x_104 = l_Lean_Elab_processCommand___boxed__const__2; +x_104 = lean_box(x_103); x_105 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_105, 0, x_104); lean_ctor_set(x_105, 1, x_76); @@ -16413,7 +16393,7 @@ if (lean_is_exclusive(x_127)) { x_129 = lean_box(0); } x_130 = 0; -x_131 = l_Lean_Elab_processCommand___boxed__const__1; +x_131 = lean_box(x_130); if (lean_is_scalar(x_129)) { x_132 = lean_alloc_ctor(0, 2, 0); } else { @@ -16462,7 +16442,7 @@ if (lean_is_exclusive(x_137)) { x_139 = lean_box(0); } x_140 = 0; -x_141 = l_Lean_Elab_processCommand___boxed__const__1; +x_141 = lean_box(x_140); if (lean_is_scalar(x_139)) { x_142 = lean_alloc_ctor(0, 2, 0); } else { @@ -16505,7 +16485,7 @@ lean_dec(x_124); lean_dec(x_118); lean_dec(x_1); x_147 = 1; -x_148 = l_Lean_Elab_processCommand___boxed__const__2; +x_148 = lean_box(x_147); x_149 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_149, 0, x_148); lean_ctor_set(x_149, 1, x_122); @@ -16519,7 +16499,7 @@ lean_dec(x_124); lean_dec(x_118); lean_dec(x_1); x_150 = 1; -x_151 = l_Lean_Elab_processCommand___boxed__const__2; +x_151 = lean_box(x_150); x_152 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_152, 0, x_151); lean_ctor_set(x_152, 1, x_122); @@ -20043,10 +20023,6 @@ l_Lean_Elab_elabCommand___closed__2 = _init_l_Lean_Elab_elabCommand___closed__2( lean_mark_persistent(l_Lean_Elab_elabCommand___closed__2); l_Lean_Elab_elabCommand___closed__3 = _init_l_Lean_Elab_elabCommand___closed__3(); lean_mark_persistent(l_Lean_Elab_elabCommand___closed__3); -l_Lean_Elab_processCommand___boxed__const__1 = _init_l_Lean_Elab_processCommand___boxed__const__1(); -lean_mark_persistent(l_Lean_Elab_processCommand___boxed__const__1); -l_Lean_Elab_processCommand___boxed__const__2 = _init_l_Lean_Elab_processCommand___boxed__const__2(); -lean_mark_persistent(l_Lean_Elab_processCommand___boxed__const__2); l_Lean_Elab_absolutizeModuleName___closed__1 = _init_l_Lean_Elab_absolutizeModuleName___closed__1(); lean_mark_persistent(l_Lean_Elab_absolutizeModuleName___closed__1); l_Lean_Elab_processHeaderAux___closed__1 = _init_l_Lean_Elab_processHeaderAux___closed__1(); diff --git a/src/stage0/init/lean/elaborator/elabstrategyattrs.c b/src/stage0/init/lean/elaborator/elabstrategyattrs.c index 26204d3d69..05b6da23b0 100644 --- a/src/stage0/init/lean/elaborator/elabstrategyattrs.c +++ b/src/stage0/init/lean/elaborator/elabstrategyattrs.c @@ -14,7 +14,6 @@ extern "C" { #endif uint8_t l_Lean_ElaboratorStrategy_inhabited; -lean_object* l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkElaboratorStrategyAttrs___spec__4___closed__1___boxed__const__1; lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_name_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_mkElaboratorStrategyAttrs___closed__10; @@ -62,13 +61,10 @@ lean_object* l_List_mfor___main___at_Lean_registerEnumAttributes___spec__11(lean uint8_t l_Array_anyMAux___main___at_Lean_mkElaboratorStrategyAttrs___spec__6(lean_object*, lean_object*, lean_object*); lean_object* l_Array_qsortAux___main___at_Lean_mkElaboratorStrategyAttrs___spec__3(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Environment_getModuleIdxFor(lean_object*, lean_object*); -lean_object* l_Lean_mkElaboratorStrategyAttrs___closed__16___boxed__const__1; extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__1; lean_object* lean_string_append(lean_object*, lean_object*); lean_object* l_Lean_mkElaboratorStrategyAttrs___closed__2; -lean_object* l_Lean_EnumAttributes_getValue___at_Lean_getElaboratorStrategy___spec__1___boxed__const__1; lean_object* l_Lean_mkElaboratorStrategyAttrs___closed__17; -lean_object* l_Lean_mkElaboratorStrategyAttrs___closed__11___boxed__const__1; lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_mkElaboratorStrategyAttrs___spec__7(lean_object*, lean_object*); uint8_t lean_nat_dec_lt(lean_object*, lean_object*); lean_object* l_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*); @@ -82,7 +78,6 @@ lean_object* l_List_map___main___at_Lean_mkElaboratorStrategyAttrs___spec__8___l extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__3; uint8_t lean_nat_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_registerEnumAttributes___at_Lean_mkElaboratorStrategyAttrs___spec__1___lambda__2(lean_object*); -lean_object* l_Lean_mkElaboratorStrategyAttrs___closed__6___boxed__const__1; lean_object* l_Array_push(lean_object*, lean_object*, lean_object*); lean_object* l_RBNode_find___main___at_Lean_getElaboratorStrategy___spec__2(lean_object*, lean_object*); lean_object* l_Lean_registerEnumAttributes___at_Lean_mkElaboratorStrategyAttrs___spec__1___closed__2; @@ -158,22 +153,13 @@ goto _start; } } } -lean_object* _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkElaboratorStrategyAttrs___spec__4___closed__1___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = l_Lean_ElaboratorStrategy_inhabited; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkElaboratorStrategyAttrs___spec__4___closed__1() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Inhabited; x_2 = l_Lean_ElaboratorStrategy_inhabited; -x_3 = l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkElaboratorStrategyAttrs___spec__4___closed__1___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -2700,22 +2686,13 @@ x_1 = lean_mk_string("instructs elaborator that the arguments of the function ap return x_1; } } -lean_object* _init_l_Lean_mkElaboratorStrategyAttrs___closed__6___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_mkElaboratorStrategyAttrs___closed__6() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_mkElaboratorStrategyAttrs___closed__5; x_2 = 1; -x_3 = l_Lean_mkElaboratorStrategyAttrs___closed__6___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -2760,22 +2737,13 @@ x_1 = lean_mk_string("instructs elaborator that the arguments of the function ap return x_1; } } -lean_object* _init_l_Lean_mkElaboratorStrategyAttrs___closed__11___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_mkElaboratorStrategyAttrs___closed__11() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_mkElaboratorStrategyAttrs___closed__10; x_2 = 0; -x_3 = l_Lean_mkElaboratorStrategyAttrs___closed__11___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -2820,22 +2788,13 @@ x_1 = lean_mk_string("instructs elaborator that the arguments of the function ap return x_1; } } -lean_object* _init_l_Lean_mkElaboratorStrategyAttrs___closed__16___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 2; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_mkElaboratorStrategyAttrs___closed__16() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_mkElaboratorStrategyAttrs___closed__15; x_2 = 2; -x_3 = l_Lean_mkElaboratorStrategyAttrs___closed__16___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -3106,15 +3065,6 @@ goto _start; } } } -lean_object* _init_l_Lean_EnumAttributes_getValue___at_Lean_getElaboratorStrategy___spec__1___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Lean_EnumAttributes_getValue___at_Lean_getElaboratorStrategy___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -3144,7 +3094,7 @@ lean_dec(x_1); x_10 = l_Lean_PersistentEnvExtension_getModuleEntries___rarg(x_9, x_2, x_8); lean_dec(x_8); x_11 = 1; -x_12 = l_Lean_EnumAttributes_getValue___at_Lean_getElaboratorStrategy___spec__1___boxed__const__1; +x_12 = lean_box(x_11); x_13 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_13, 0, x_3); lean_ctor_set(x_13, 1, x_12); @@ -3241,8 +3191,6 @@ if (lean_io_result_is_error(w)) return w; w = initialize_init_lean_attributes(w); if (lean_io_result_is_error(w)) return w; l_Lean_ElaboratorStrategy_inhabited = _init_l_Lean_ElaboratorStrategy_inhabited(); -l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkElaboratorStrategyAttrs___spec__4___closed__1___boxed__const__1 = _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkElaboratorStrategyAttrs___spec__4___closed__1___boxed__const__1(); -lean_mark_persistent(l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkElaboratorStrategyAttrs___spec__4___closed__1___boxed__const__1); l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkElaboratorStrategyAttrs___spec__4___closed__1 = _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkElaboratorStrategyAttrs___spec__4___closed__1(); lean_mark_persistent(l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkElaboratorStrategyAttrs___spec__4___closed__1); l_Lean_registerEnumAttributes___at_Lean_mkElaboratorStrategyAttrs___spec__1___closed__1 = _init_l_Lean_registerEnumAttributes___at_Lean_mkElaboratorStrategyAttrs___spec__1___closed__1(); @@ -3261,8 +3209,6 @@ l_Lean_mkElaboratorStrategyAttrs___closed__4 = _init_l_Lean_mkElaboratorStrategy lean_mark_persistent(l_Lean_mkElaboratorStrategyAttrs___closed__4); l_Lean_mkElaboratorStrategyAttrs___closed__5 = _init_l_Lean_mkElaboratorStrategyAttrs___closed__5(); lean_mark_persistent(l_Lean_mkElaboratorStrategyAttrs___closed__5); -l_Lean_mkElaboratorStrategyAttrs___closed__6___boxed__const__1 = _init_l_Lean_mkElaboratorStrategyAttrs___closed__6___boxed__const__1(); -lean_mark_persistent(l_Lean_mkElaboratorStrategyAttrs___closed__6___boxed__const__1); l_Lean_mkElaboratorStrategyAttrs___closed__6 = _init_l_Lean_mkElaboratorStrategyAttrs___closed__6(); lean_mark_persistent(l_Lean_mkElaboratorStrategyAttrs___closed__6); l_Lean_mkElaboratorStrategyAttrs___closed__7 = _init_l_Lean_mkElaboratorStrategyAttrs___closed__7(); @@ -3273,8 +3219,6 @@ l_Lean_mkElaboratorStrategyAttrs___closed__9 = _init_l_Lean_mkElaboratorStrategy lean_mark_persistent(l_Lean_mkElaboratorStrategyAttrs___closed__9); l_Lean_mkElaboratorStrategyAttrs___closed__10 = _init_l_Lean_mkElaboratorStrategyAttrs___closed__10(); lean_mark_persistent(l_Lean_mkElaboratorStrategyAttrs___closed__10); -l_Lean_mkElaboratorStrategyAttrs___closed__11___boxed__const__1 = _init_l_Lean_mkElaboratorStrategyAttrs___closed__11___boxed__const__1(); -lean_mark_persistent(l_Lean_mkElaboratorStrategyAttrs___closed__11___boxed__const__1); l_Lean_mkElaboratorStrategyAttrs___closed__11 = _init_l_Lean_mkElaboratorStrategyAttrs___closed__11(); lean_mark_persistent(l_Lean_mkElaboratorStrategyAttrs___closed__11); l_Lean_mkElaboratorStrategyAttrs___closed__12 = _init_l_Lean_mkElaboratorStrategyAttrs___closed__12(); @@ -3285,8 +3229,6 @@ l_Lean_mkElaboratorStrategyAttrs___closed__14 = _init_l_Lean_mkElaboratorStrateg lean_mark_persistent(l_Lean_mkElaboratorStrategyAttrs___closed__14); l_Lean_mkElaboratorStrategyAttrs___closed__15 = _init_l_Lean_mkElaboratorStrategyAttrs___closed__15(); lean_mark_persistent(l_Lean_mkElaboratorStrategyAttrs___closed__15); -l_Lean_mkElaboratorStrategyAttrs___closed__16___boxed__const__1 = _init_l_Lean_mkElaboratorStrategyAttrs___closed__16___boxed__const__1(); -lean_mark_persistent(l_Lean_mkElaboratorStrategyAttrs___closed__16___boxed__const__1); l_Lean_mkElaboratorStrategyAttrs___closed__16 = _init_l_Lean_mkElaboratorStrategyAttrs___closed__16(); lean_mark_persistent(l_Lean_mkElaboratorStrategyAttrs___closed__16); l_Lean_mkElaboratorStrategyAttrs___closed__17 = _init_l_Lean_mkElaboratorStrategyAttrs___closed__17(); @@ -3303,8 +3245,6 @@ w = l_Lean_mkElaboratorStrategyAttrs(w); if (lean_io_result_is_error(w)) return w; l_Lean_elaboratorStrategyAttrs = lean_io_result_get_value(w); lean_mark_persistent(l_Lean_elaboratorStrategyAttrs); -l_Lean_EnumAttributes_getValue___at_Lean_getElaboratorStrategy___spec__1___boxed__const__1 = _init_l_Lean_EnumAttributes_getValue___at_Lean_getElaboratorStrategy___spec__1___boxed__const__1(); -lean_mark_persistent(l_Lean_EnumAttributes_getValue___at_Lean_getElaboratorStrategy___spec__1___boxed__const__1); return w; } #ifdef __cplusplus diff --git a/src/stage0/init/lean/kvmap.c b/src/stage0/init/lean/kvmap.c index 7d27273dda..4d98e255b5 100644 --- a/src/stage0/init/lean/kvmap.c +++ b/src/stage0/init/lean/kvmap.c @@ -63,7 +63,6 @@ lean_object* l_Lean_KVMap_find___boxed(lean_object*, lean_object*); lean_object* l_Lean_int2DataValue(lean_object*); uint8_t lean_string_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_KVMap_get___rarg(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_KVMap_boolVal___closed__3___boxed__const__1; lean_object* l_Lean_KVMap_eqv___boxed(lean_object*, lean_object*); lean_object* l_Lean_bool2DataValue___boxed(lean_object*); uint8_t l_Lean_KVMap_subsetAux(lean_object*, lean_object*); @@ -955,15 +954,6 @@ x_1 = lean_alloc_closure((void*)(l_Lean_KVMap_getBool___boxed), 3, 0); return x_1; } } -lean_object* _init_l_Lean_KVMap_boolVal___closed__3___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_KVMap_boolVal___closed__3() { _start: { @@ -971,7 +961,7 @@ uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_1 = 0; x_2 = l_Lean_KVMap_boolVal___closed__1; x_3 = l_Lean_KVMap_boolVal___closed__2; -x_4 = l_Lean_KVMap_boolVal___closed__3___boxed__const__1; +x_4 = lean_box(x_1); x_5 = lean_alloc_ctor(0, 3, 0); lean_ctor_set(x_5, 0, x_4); lean_ctor_set(x_5, 1, x_2); @@ -1165,8 +1155,6 @@ l_Lean_KVMap_boolVal___closed__1 = _init_l_Lean_KVMap_boolVal___closed__1(); lean_mark_persistent(l_Lean_KVMap_boolVal___closed__1); l_Lean_KVMap_boolVal___closed__2 = _init_l_Lean_KVMap_boolVal___closed__2(); lean_mark_persistent(l_Lean_KVMap_boolVal___closed__2); -l_Lean_KVMap_boolVal___closed__3___boxed__const__1 = _init_l_Lean_KVMap_boolVal___closed__3___boxed__const__1(); -lean_mark_persistent(l_Lean_KVMap_boolVal___closed__3___boxed__const__1); l_Lean_KVMap_boolVal___closed__3 = _init_l_Lean_KVMap_boolVal___closed__3(); lean_mark_persistent(l_Lean_KVMap_boolVal___closed__3); l_Lean_KVMap_boolVal = _init_l_Lean_KVMap_boolVal(); diff --git a/src/stage0/init/lean/localcontext.c b/src/stage0/init/lean/localcontext.c index bf6e862400..87ac2d4c13 100644 --- a/src/stage0/init/lean/localcontext.c +++ b/src/stage0/init/lean/localcontext.c @@ -218,7 +218,6 @@ lean_object* l_PersistentArray_mfoldlFromAux___main___at_Lean_LocalContext_foldl lean_object* l_Array_mfindRevAux___main___at_Lean_LocalContext_findFromUserName___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_PersistentArray_mfoldlFromAux___main___at_Lean_LocalContext_foldlFrom___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_LocalContext_mfoldlFrom___at_Lean_LocalContext_foldlFrom___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2; lean_object* l_Lean_LocalDecl_type(lean_object*); lean_object* l_Array_miterateAux___main___at_Lean_LocalContext_foldlFrom___spec__6(lean_object*); lean_object* l_Array_mfindRevAux___main___at_Lean_LocalContext_mfindDeclRev___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -229,7 +228,6 @@ lean_object* l_Lean_LocalContext_mfoldl___at_Lean_LocalContext_foldl___spec__1__ lean_object* l_Array_miterateAux___main___at_Lean_LocalContext_mfoldlFrom___spec__2___boxed(lean_object*); lean_object* l_PersistentArray_mfor___at_Lean_LocalContext_mfor___spec__1(lean_object*); lean_object* l_PersistentArray_mfoldlFrom___at_Lean_LocalContext_mfoldlFrom___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__1; lean_object* l_Array_mforAux___main___at_Lean_LocalContext_mfor___spec__4___boxed(lean_object*); lean_object* l_Lean_LocalContext_mfoldl___boxed(lean_object*); lean_object* l_Array_mfindAux___main___at_Lean_LocalContext_mfindDecl___spec__4___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1698,24 +1696,6 @@ return x_12; } } } -lean_object* _init_l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2(lean_object* x_1, size_t x_2, lean_object* x_3) { _start: { @@ -1745,7 +1725,7 @@ uint8_t x_13; lean_object* x_14; lean_object* x_15; lean_dec(x_8); lean_dec(x_4); x_13 = 0; -x_14 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__1; +x_14 = lean_box(x_13); x_15 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_15, 0, x_1); lean_ctor_set(x_15, 1, x_14); @@ -1764,7 +1744,7 @@ x_18 = lean_array_set(x_4, x_8, x_9); lean_dec(x_8); lean_ctor_set(x_1, 0, x_18); x_19 = 1; -x_20 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2; +x_20 = lean_box(x_19); x_21 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_21, 0, x_1); lean_ctor_set(x_21, 1, x_20); @@ -1779,7 +1759,7 @@ lean_dec(x_8); x_23 = lean_alloc_ctor(0, 1, 0); lean_ctor_set(x_23, 0, x_22); x_24 = 1; -x_25 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2; +x_25 = lean_box(x_24); x_26 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_26, 0, x_23); lean_ctor_set(x_26, 1, x_25); @@ -1817,7 +1797,7 @@ lean_dec(x_35); x_36 = lean_ctor_get(x_31, 0); lean_dec(x_36); x_37 = 0; -x_38 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__1; +x_38 = lean_box(x_37); lean_ctor_set(x_31, 1, x_38); lean_ctor_set(x_31, 0, x_1); return x_31; @@ -1827,7 +1807,7 @@ else uint8_t x_39; lean_object* x_40; lean_object* x_41; lean_dec(x_31); x_39 = 0; -x_40 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__1; +x_40 = lean_box(x_39); x_41 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_41, 0, x_1); lean_ctor_set(x_41, 1, x_40); @@ -1859,7 +1839,7 @@ x_48 = lean_array_set(x_29, x_8, x_10); lean_dec(x_8); lean_ctor_set(x_1, 0, x_48); x_49 = 1; -x_50 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2; +x_50 = lean_box(x_49); lean_ctor_set(x_31, 1, x_50); lean_ctor_set(x_31, 0, x_1); return x_31; @@ -1886,7 +1866,7 @@ x_56 = lean_array_set(x_29, x_8, x_55); lean_dec(x_8); lean_ctor_set(x_1, 0, x_56); x_57 = 1; -x_58 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2; +x_58 = lean_box(x_57); lean_ctor_set(x_51, 1, x_58); lean_ctor_set(x_51, 0, x_1); return x_51; @@ -1906,7 +1886,7 @@ x_62 = lean_array_set(x_29, x_8, x_61); lean_dec(x_8); lean_ctor_set(x_1, 0, x_62); x_63 = 1; -x_64 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2; +x_64 = lean_box(x_63); x_65 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_65, 0, x_1); lean_ctor_set(x_65, 1, x_64); @@ -1929,7 +1909,7 @@ x_68 = lean_array_set(x_29, x_8, x_10); lean_dec(x_8); lean_ctor_set(x_1, 0, x_68); x_69 = 1; -x_70 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2; +x_70 = lean_box(x_69); x_71 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_71, 0, x_1); lean_ctor_set(x_71, 1, x_70); @@ -1962,7 +1942,7 @@ x_77 = lean_array_set(x_29, x_8, x_76); lean_dec(x_8); lean_ctor_set(x_1, 0, x_77); x_78 = 1; -x_79 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2; +x_79 = lean_box(x_78); if (lean_is_scalar(x_75)) { x_80 = lean_alloc_ctor(0, 2, 0); } else { @@ -1998,7 +1978,7 @@ lean_dec(x_8); x_85 = lean_alloc_ctor(0, 1, 0); lean_ctor_set(x_85, 0, x_84); x_86 = 1; -x_87 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2; +x_87 = lean_box(x_86); if (lean_is_scalar(x_82)) { x_88 = lean_alloc_ctor(0, 2, 0); } else { @@ -2037,7 +2017,7 @@ lean_dec(x_8); x_95 = lean_alloc_ctor(0, 1, 0); lean_ctor_set(x_95, 0, x_94); x_96 = 1; -x_97 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2; +x_97 = lean_box(x_96); if (lean_is_scalar(x_92)) { x_98 = lean_alloc_ctor(0, 2, 0); } else { @@ -2077,7 +2057,7 @@ if (lean_is_exclusive(x_102)) { x_105 = lean_box(0); } x_106 = 0; -x_107 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__1; +x_107 = lean_box(x_106); if (lean_is_scalar(x_105)) { x_108 = lean_alloc_ctor(0, 2, 0); } else { @@ -2122,7 +2102,7 @@ if (lean_is_scalar(x_109)) { } lean_ctor_set(x_115, 0, x_114); x_116 = 1; -x_117 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2; +x_117 = lean_box(x_116); if (lean_is_scalar(x_111)) { x_118 = lean_alloc_ctor(0, 2, 0); } else { @@ -2164,7 +2144,7 @@ if (lean_is_scalar(x_109)) { } lean_ctor_set(x_125, 0, x_124); x_126 = 1; -x_127 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2; +x_127 = lean_box(x_126); if (lean_is_scalar(x_122)) { x_128 = lean_alloc_ctor(0, 2, 0); } else { @@ -2183,7 +2163,7 @@ uint8_t x_129; lean_object* x_130; lean_object* x_131; lean_dec(x_8); lean_dec(x_4); x_129 = 0; -x_130 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__1; +x_130 = lean_box(x_129); x_131 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_131, 0, x_1); lean_ctor_set(x_131, 1, x_130); @@ -2206,7 +2186,7 @@ uint8_t x_136; lean_object* x_137; lean_object* x_138; lean_dec(x_133); lean_dec(x_132); x_136 = 0; -x_137 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__1; +x_137 = lean_box(x_136); x_138 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_138, 0, x_1); lean_ctor_set(x_138, 1, x_137); @@ -2232,7 +2212,7 @@ lean_dec(x_142); lean_ctor_set(x_1, 1, x_144); lean_ctor_set(x_1, 0, x_143); x_145 = 1; -x_146 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2; +x_146 = lean_box(x_145); x_147 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_147, 0, x_1); lean_ctor_set(x_147, 1, x_146); @@ -2252,7 +2232,7 @@ x_151 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_151, 0, x_149); lean_ctor_set(x_151, 1, x_150); x_152 = 1; -x_153 = l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2; +x_153 = lean_box(x_152); x_154 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_154, 0, x_151); lean_ctor_set(x_154, 1, x_153); @@ -6609,10 +6589,6 @@ l_Lean_LocalContext_Inhabited = _init_l_Lean_LocalContext_Inhabited(); lean_mark_persistent(l_Lean_LocalContext_Inhabited); l_Lean_LocalContext_empty = _init_l_Lean_LocalContext_empty(); lean_mark_persistent(l_Lean_LocalContext_empty); -l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__1 = _init_l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__1(); -lean_mark_persistent(l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__1); -l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2 = _init_l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2(); -lean_mark_persistent(l_PersistentHashMap_eraseAux___main___at_Lean_LocalContext_erase___spec__2___boxed__const__2); return w; } #ifdef __cplusplus diff --git a/src/stage0/init/lean/metavarcontext.c b/src/stage0/init/lean/metavarcontext.c index b743768386..1047a2e22d 100644 --- a/src/stage0/init/lean/metavarcontext.c +++ b/src/stage0/init/lean/metavarcontext.c @@ -21,7 +21,6 @@ lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_MetavarContext_findD lean_object* l_PersistentHashMap_find___at_Lean_MetavarContext_findDecl___spec__1___boxed(lean_object*, lean_object*); uint8_t l_PersistentHashMap_contains___at_Lean_MetavarContext_isExprAssigned___spec__1(lean_object*, lean_object*); lean_object* lean_nat_sub(lean_object*, lean_object*); -lean_object* l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2; lean_object* l_PersistentHashMap_insertAux___main___at_Lean_MetavarContext_assignExpr___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_PersistentHashMap_find___at_Lean_MetavarContext_getExprAssignment___spec__1___boxed(lean_object*, lean_object*); lean_object* l_Array_miterateAux___main___at_Lean_MetavarContext_mkDecl___spec__4(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -36,7 +35,6 @@ lean_object* lean_metavar_ctx_get_delayed_assignment(lean_object*, lean_object*) size_t l_USize_sub(size_t, size_t); lean_object* l_Lean_MetavarContext_mkMetavarContext___closed__1; uint8_t l_PersistentHashMap_contains___at_Lean_MetavarContext_isDelayedAssigned___spec__1(lean_object*, lean_object*); -lean_object* l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__1; lean_object* l_Array_miterateAux___main___at_Lean_MetavarContext_assignLevel___spec__4(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_PersistentHashMap_insertAux___main___at_Lean_MetavarContext_mkDecl___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_metavar_ctx_get_expr_assignment(lean_object*, lean_object*); @@ -3370,24 +3368,6 @@ x_4 = lean_box(x_3); return x_4; } } -lean_object* _init_l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2(lean_object* x_1, size_t x_2, lean_object* x_3) { _start: { @@ -3417,7 +3397,7 @@ uint8_t x_13; lean_object* x_14; lean_object* x_15; lean_dec(x_8); lean_dec(x_4); x_13 = 0; -x_14 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__1; +x_14 = lean_box(x_13); x_15 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_15, 0, x_1); lean_ctor_set(x_15, 1, x_14); @@ -3436,7 +3416,7 @@ x_18 = lean_array_set(x_4, x_8, x_9); lean_dec(x_8); lean_ctor_set(x_1, 0, x_18); x_19 = 1; -x_20 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2; +x_20 = lean_box(x_19); x_21 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_21, 0, x_1); lean_ctor_set(x_21, 1, x_20); @@ -3451,7 +3431,7 @@ lean_dec(x_8); x_23 = lean_alloc_ctor(0, 1, 0); lean_ctor_set(x_23, 0, x_22); x_24 = 1; -x_25 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2; +x_25 = lean_box(x_24); x_26 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_26, 0, x_23); lean_ctor_set(x_26, 1, x_25); @@ -3489,7 +3469,7 @@ lean_dec(x_35); x_36 = lean_ctor_get(x_31, 0); lean_dec(x_36); x_37 = 0; -x_38 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__1; +x_38 = lean_box(x_37); lean_ctor_set(x_31, 1, x_38); lean_ctor_set(x_31, 0, x_1); return x_31; @@ -3499,7 +3479,7 @@ else uint8_t x_39; lean_object* x_40; lean_object* x_41; lean_dec(x_31); x_39 = 0; -x_40 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__1; +x_40 = lean_box(x_39); x_41 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_41, 0, x_1); lean_ctor_set(x_41, 1, x_40); @@ -3531,7 +3511,7 @@ x_48 = lean_array_set(x_29, x_8, x_10); lean_dec(x_8); lean_ctor_set(x_1, 0, x_48); x_49 = 1; -x_50 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2; +x_50 = lean_box(x_49); lean_ctor_set(x_31, 1, x_50); lean_ctor_set(x_31, 0, x_1); return x_31; @@ -3558,7 +3538,7 @@ x_56 = lean_array_set(x_29, x_8, x_55); lean_dec(x_8); lean_ctor_set(x_1, 0, x_56); x_57 = 1; -x_58 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2; +x_58 = lean_box(x_57); lean_ctor_set(x_51, 1, x_58); lean_ctor_set(x_51, 0, x_1); return x_51; @@ -3578,7 +3558,7 @@ x_62 = lean_array_set(x_29, x_8, x_61); lean_dec(x_8); lean_ctor_set(x_1, 0, x_62); x_63 = 1; -x_64 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2; +x_64 = lean_box(x_63); x_65 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_65, 0, x_1); lean_ctor_set(x_65, 1, x_64); @@ -3601,7 +3581,7 @@ x_68 = lean_array_set(x_29, x_8, x_10); lean_dec(x_8); lean_ctor_set(x_1, 0, x_68); x_69 = 1; -x_70 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2; +x_70 = lean_box(x_69); x_71 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_71, 0, x_1); lean_ctor_set(x_71, 1, x_70); @@ -3634,7 +3614,7 @@ x_77 = lean_array_set(x_29, x_8, x_76); lean_dec(x_8); lean_ctor_set(x_1, 0, x_77); x_78 = 1; -x_79 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2; +x_79 = lean_box(x_78); if (lean_is_scalar(x_75)) { x_80 = lean_alloc_ctor(0, 2, 0); } else { @@ -3670,7 +3650,7 @@ lean_dec(x_8); x_85 = lean_alloc_ctor(0, 1, 0); lean_ctor_set(x_85, 0, x_84); x_86 = 1; -x_87 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2; +x_87 = lean_box(x_86); if (lean_is_scalar(x_82)) { x_88 = lean_alloc_ctor(0, 2, 0); } else { @@ -3709,7 +3689,7 @@ lean_dec(x_8); x_95 = lean_alloc_ctor(0, 1, 0); lean_ctor_set(x_95, 0, x_94); x_96 = 1; -x_97 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2; +x_97 = lean_box(x_96); if (lean_is_scalar(x_92)) { x_98 = lean_alloc_ctor(0, 2, 0); } else { @@ -3749,7 +3729,7 @@ if (lean_is_exclusive(x_102)) { x_105 = lean_box(0); } x_106 = 0; -x_107 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__1; +x_107 = lean_box(x_106); if (lean_is_scalar(x_105)) { x_108 = lean_alloc_ctor(0, 2, 0); } else { @@ -3794,7 +3774,7 @@ if (lean_is_scalar(x_109)) { } lean_ctor_set(x_115, 0, x_114); x_116 = 1; -x_117 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2; +x_117 = lean_box(x_116); if (lean_is_scalar(x_111)) { x_118 = lean_alloc_ctor(0, 2, 0); } else { @@ -3836,7 +3816,7 @@ if (lean_is_scalar(x_109)) { } lean_ctor_set(x_125, 0, x_124); x_126 = 1; -x_127 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2; +x_127 = lean_box(x_126); if (lean_is_scalar(x_122)) { x_128 = lean_alloc_ctor(0, 2, 0); } else { @@ -3855,7 +3835,7 @@ uint8_t x_129; lean_object* x_130; lean_object* x_131; lean_dec(x_8); lean_dec(x_4); x_129 = 0; -x_130 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__1; +x_130 = lean_box(x_129); x_131 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_131, 0, x_1); lean_ctor_set(x_131, 1, x_130); @@ -3878,7 +3858,7 @@ uint8_t x_136; lean_object* x_137; lean_object* x_138; lean_dec(x_133); lean_dec(x_132); x_136 = 0; -x_137 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__1; +x_137 = lean_box(x_136); x_138 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_138, 0, x_1); lean_ctor_set(x_138, 1, x_137); @@ -3904,7 +3884,7 @@ lean_dec(x_142); lean_ctor_set(x_1, 1, x_144); lean_ctor_set(x_1, 0, x_143); x_145 = 1; -x_146 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2; +x_146 = lean_box(x_145); x_147 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_147, 0, x_1); lean_ctor_set(x_147, 1, x_146); @@ -3924,7 +3904,7 @@ x_151 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_151, 0, x_149); lean_ctor_set(x_151, 1, x_150); x_152 = 1; -x_153 = l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2; +x_153 = lean_box(x_152); x_154 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_154, 0, x_151); lean_ctor_set(x_154, 1, x_153); @@ -4082,10 +4062,6 @@ w = initialize_init_lean_localcontext(w); if (lean_io_result_is_error(w)) return w; l_Lean_MetavarContext_mkMetavarContext___closed__1 = _init_l_Lean_MetavarContext_mkMetavarContext___closed__1(); lean_mark_persistent(l_Lean_MetavarContext_mkMetavarContext___closed__1); -l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__1 = _init_l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__1(); -lean_mark_persistent(l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__1); -l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2 = _init_l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2(); -lean_mark_persistent(l_PersistentHashMap_eraseAux___main___at_Lean_MetavarContext_eraseDelayed___spec__2___boxed__const__2); return w; } #ifdef __cplusplus diff --git a/src/stage0/init/lean/parser/module.c b/src/stage0/init/lean/parser/module.c index d5287a5f42..c2b8e5cf5d 100644 --- a/src/stage0/init/lean/parser/module.c +++ b/src/stage0/init/lean/parser/module.c @@ -23,7 +23,6 @@ lean_object* lean_io_realpath(lean_object*, lean_object*); extern lean_object* l_Array_empty___closed__1; lean_object* l_Lean_Parser_whitespace___main(lean_object*, lean_object*); lean_object* l_Lean_Format_pretty(lean_object*, lean_object*); -lean_object* l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__1; lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Module_importPath___elambda__1___closed__1; lean_object* l_Array_mkArray(lean_object*, lean_object*, lean_object*); @@ -70,7 +69,6 @@ lean_object* l___private_init_lean_parser_module_3__consumeInput(lean_object*, l lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Module_import___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Module_header___closed__1; -lean_object* l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__2; lean_object* l___private_init_lean_parser_module_4__testModuleParserAux___main(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Module_import___closed__3; lean_object* l_Lean_Parser_Module_header___elambda__1___closed__1; @@ -2078,24 +2076,6 @@ return x_23; } } } -lean_object* _init_l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} -lean_object* _init_l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__2() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l___private_init_lean_parser_module_4__testModuleParserAux___main(lean_object* x_1, lean_object* x_2, uint8_t x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) { _start: { @@ -2242,14 +2222,14 @@ if (x_40 == 0) { uint8_t x_41; lean_object* x_42; x_41 = 1; -x_42 = l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__1; +x_42 = lean_box(x_41); lean_ctor_set(x_36, 0, x_42); return x_36; } else { lean_object* x_43; -x_43 = l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__2; +x_43 = lean_box(x_39); lean_ctor_set(x_36, 0, x_43); return x_36; } @@ -2267,7 +2247,7 @@ if (x_46 == 0) { uint8_t x_47; lean_object* x_48; lean_object* x_49; x_47 = 1; -x_48 = l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__1; +x_48 = lean_box(x_47); x_49 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_49, 0, x_48); lean_ctor_set(x_49, 1, x_44); @@ -2276,7 +2256,7 @@ return x_49; else { lean_object* x_50; lean_object* x_51; -x_50 = l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__2; +x_50 = lean_box(x_45); x_51 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_51, 0, x_50); lean_ctor_set(x_51, 1, x_44); @@ -2335,14 +2315,14 @@ if (x_61 == 0) { uint8_t x_62; lean_object* x_63; x_62 = 1; -x_63 = l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__1; +x_63 = lean_box(x_62); lean_ctor_set(x_57, 0, x_63); return x_57; } else { lean_object* x_64; -x_64 = l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__2; +x_64 = lean_box(x_60); lean_ctor_set(x_57, 0, x_64); return x_57; } @@ -2360,7 +2340,7 @@ if (x_67 == 0) { uint8_t x_68; lean_object* x_69; lean_object* x_70; x_68 = 1; -x_69 = l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__1; +x_69 = lean_box(x_68); x_70 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_70, 0, x_69); lean_ctor_set(x_70, 1, x_65); @@ -2369,7 +2349,7 @@ return x_70; else { lean_object* x_71; lean_object* x_72; -x_71 = l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__2; +x_71 = lean_box(x_66); x_72 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_72, 0, x_71); lean_ctor_set(x_72, 1, x_65); @@ -3010,10 +2990,6 @@ l___private_init_lean_parser_module_2__mkEOI___closed__2 = _init_l___private_ini lean_mark_persistent(l___private_init_lean_parser_module_2__mkEOI___closed__2); l___private_init_lean_parser_module_2__mkEOI___closed__3 = _init_l___private_init_lean_parser_module_2__mkEOI___closed__3(); lean_mark_persistent(l___private_init_lean_parser_module_2__mkEOI___closed__3); -l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__1 = _init_l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__1(); -lean_mark_persistent(l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__1); -l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__2 = _init_l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__2(); -lean_mark_persistent(l___private_init_lean_parser_module_4__testModuleParserAux___main___boxed__const__2); l_Lean_Parser_testModuleParser___closed__1 = _init_l_Lean_Parser_testModuleParser___closed__1(); lean_mark_persistent(l_Lean_Parser_testModuleParser___closed__1); l_Lean_Parser_testModuleParser___closed__2 = _init_l_Lean_Parser_testModuleParser___closed__2(); diff --git a/src/stage0/init/lean/parser/term.c b/src/stage0/init/lean/parser/term.c index 7d2ed4841e..c588f6bd0f 100644 --- a/src/stage0/init/lean/parser/term.c +++ b/src/stage0/init/lean/parser/term.c @@ -247,7 +247,6 @@ lean_object* l_Lean_Parser_Term_bnot; lean_object* l_Lean_Parser_orelseInfo(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_doPat___closed__5; lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___rarg___closed__9; -lean_object* l_Lean_Parser_Term_explicitBinder___closed__3___boxed__const__1; lean_object* l_Lean_Parser_Term_show___closed__3; lean_object* l_Lean_Parser_Term_dollar; lean_object* l_Lean_Parser_Term_sorry___elambda__1___rarg___closed__6; @@ -13488,22 +13487,13 @@ lean_closure_set(x_2, 0, x_1); return x_2; } } -lean_object* _init_l_Lean_Parser_Term_explicitBinder___closed__3___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_Parser_Term_explicitBinder___closed__3() { _start: { uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = 0; x_2 = l_Lean_Parser_Term_binderIdent___closed__2; -x_3 = l_Lean_Parser_Term_explicitBinder___closed__3___boxed__const__1; +x_3 = lean_box(x_1); x_4 = lean_alloc_closure((void*)(l_Lean_Parser_many1Fn___boxed), 5, 2); lean_closure_set(x_4, 0, x_3); lean_closure_set(x_4, 1, x_2); @@ -29469,8 +29459,6 @@ l_Lean_Parser_Term_explicitBinder___closed__1 = _init_l_Lean_Parser_Term_explici lean_mark_persistent(l_Lean_Parser_Term_explicitBinder___closed__1); l_Lean_Parser_Term_explicitBinder___closed__2 = _init_l_Lean_Parser_Term_explicitBinder___closed__2(); lean_mark_persistent(l_Lean_Parser_Term_explicitBinder___closed__2); -l_Lean_Parser_Term_explicitBinder___closed__3___boxed__const__1 = _init_l_Lean_Parser_Term_explicitBinder___closed__3___boxed__const__1(); -lean_mark_persistent(l_Lean_Parser_Term_explicitBinder___closed__3___boxed__const__1); l_Lean_Parser_Term_explicitBinder___closed__3 = _init_l_Lean_Parser_Term_explicitBinder___closed__3(); lean_mark_persistent(l_Lean_Parser_Term_explicitBinder___closed__3); l_Lean_Parser_Term_explicitBinder___closed__4 = _init_l_Lean_Parser_Term_explicitBinder___closed__4(); diff --git a/src/stage0/init/lean/reducibilityattrs.c b/src/stage0/init/lean/reducibilityattrs.c index b10782c2d1..2a7a047bff 100644 --- a/src/stage0/init/lean/reducibilityattrs.c +++ b/src/stage0/init/lean/reducibilityattrs.c @@ -31,12 +31,9 @@ lean_object* l_Lean_mkReducibilityAttrs___closed__12; lean_object* l_RBNode_find___main___at_Lean_getReducibilityStatus___spec__2(lean_object*, lean_object*); extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__2; lean_object* l_Lean_mkReducibilityAttrs(lean_object*); -lean_object* l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkReducibilityAttrs___spec__4___closed__1___boxed__const__1; uint8_t l_Array_anyMAux___main___at_Lean_mkReducibilityAttrs___spec__6(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_AttributeImpl_inhabited___closed__5; extern lean_object* l_Lean_registerTagAttribute___lambda__4___closed__4; -lean_object* l_Lean_mkReducibilityAttrs___closed__9___boxed__const__1; -lean_object* l_Lean_EnumAttributes_getValue___at_Lean_getReducibilityStatus___spec__1___boxed__const__1; lean_object* l_Lean_setReducibilityStatus___boxed(lean_object*, lean_object*, lean_object*); lean_object* l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkReducibilityAttrs___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_binSearchAux___main___at_Lean_getReducibilityStatus___spec__3(lean_object*, lean_object*, lean_object*, lean_object*); @@ -55,7 +52,6 @@ lean_object* l_Array_swap(lean_object*, lean_object*, lean_object*, lean_object* extern lean_object* l_Lean_AttributeImpl_inhabited___closed__4; lean_object* lean_set_reducibility_status(lean_object*, lean_object*, uint8_t); lean_object* l_Lean_registerTagAttribute___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_mkReducibilityAttrs___closed__5___boxed__const__1; lean_object* l_List_map___main___at_Lean_mkReducibilityAttrs___spec__8___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_EnumAttributes_Inhabited___closed__1; lean_object* l_Lean_mkReducibilityAttrs___closed__8; @@ -87,7 +83,6 @@ lean_object* l_List_map___main___at_Lean_mkReducibilityAttrs___spec__8(lean_obje lean_object* l_Array_qsortAux___main___at_Lean_mkReducibilityAttrs___spec__3(lean_object*, lean_object*, lean_object*); lean_object* l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkReducibilityAttrs___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_getReducibilityStatus___boxed(lean_object*, lean_object*); -lean_object* l_Lean_mkReducibilityAttrs___closed__13___boxed__const__1; lean_object* l_Lean_registerEnumAttributes___at_Lean_mkReducibilityAttrs___spec__1___closed__1; uint8_t l_Lean_ReducibilityStatus_inhabited; lean_object* l_Lean_registerEnumAttributes___at_Lean_mkReducibilityAttrs___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); @@ -159,22 +154,13 @@ goto _start; } } } -lean_object* _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkReducibilityAttrs___spec__4___closed__1___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = l_Lean_ReducibilityStatus_inhabited; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkReducibilityAttrs___spec__4___closed__1() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Inhabited; x_2 = l_Lean_ReducibilityStatus_inhabited; -x_3 = l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkReducibilityAttrs___spec__4___closed__1___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -2693,22 +2679,13 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_mkReducibilityAttrs___closed__5___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 0; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_mkReducibilityAttrs___closed__5() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_mkReducibilityAttrs___closed__3; x_2 = 0; -x_3 = l_Lean_mkReducibilityAttrs___closed__5___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -2745,22 +2722,13 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_mkReducibilityAttrs___closed__9___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_mkReducibilityAttrs___closed__9() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_mkReducibilityAttrs___closed__7; x_2 = 1; -x_3 = l_Lean_mkReducibilityAttrs___closed__9___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -2797,22 +2765,13 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_mkReducibilityAttrs___closed__13___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 2; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* _init_l_Lean_mkReducibilityAttrs___closed__13() { _start: { lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_mkReducibilityAttrs___closed__11; x_2 = 2; -x_3 = l_Lean_mkReducibilityAttrs___closed__13___boxed__const__1; +x_3 = lean_box(x_2); x_4 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_3); @@ -3083,15 +3042,6 @@ goto _start; } } } -lean_object* _init_l_Lean_EnumAttributes_getValue___at_Lean_getReducibilityStatus___spec__1___boxed__const__1() { -_start: -{ -uint8_t x_1; lean_object* x_2; -x_1 = 1; -x_2 = lean_box(x_1); -return x_2; -} -} lean_object* l_Lean_EnumAttributes_getValue___at_Lean_getReducibilityStatus___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -3121,7 +3071,7 @@ lean_dec(x_1); x_10 = l_Lean_PersistentEnvExtension_getModuleEntries___rarg(x_9, x_2, x_8); lean_dec(x_8); x_11 = 1; -x_12 = l_Lean_EnumAttributes_getValue___at_Lean_getReducibilityStatus___spec__1___boxed__const__1; +x_12 = lean_box(x_11); x_13 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_13, 0, x_3); lean_ctor_set(x_13, 1, x_12); @@ -3276,8 +3226,6 @@ if (lean_io_result_is_error(w)) return w; w = initialize_init_lean_attributes(w); if (lean_io_result_is_error(w)) return w; l_Lean_ReducibilityStatus_inhabited = _init_l_Lean_ReducibilityStatus_inhabited(); -l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkReducibilityAttrs___spec__4___closed__1___boxed__const__1 = _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkReducibilityAttrs___spec__4___closed__1___boxed__const__1(); -lean_mark_persistent(l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkReducibilityAttrs___spec__4___closed__1___boxed__const__1); l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkReducibilityAttrs___spec__4___closed__1 = _init_l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkReducibilityAttrs___spec__4___closed__1(); lean_mark_persistent(l___private_init_data_array_qsort_1__partitionAux___main___at_Lean_mkReducibilityAttrs___spec__4___closed__1); l_Lean_registerEnumAttributes___at_Lean_mkReducibilityAttrs___spec__1___closed__1 = _init_l_Lean_registerEnumAttributes___at_Lean_mkReducibilityAttrs___spec__1___closed__1(); @@ -3294,8 +3242,6 @@ l_Lean_mkReducibilityAttrs___closed__3 = _init_l_Lean_mkReducibilityAttrs___clos lean_mark_persistent(l_Lean_mkReducibilityAttrs___closed__3); l_Lean_mkReducibilityAttrs___closed__4 = _init_l_Lean_mkReducibilityAttrs___closed__4(); lean_mark_persistent(l_Lean_mkReducibilityAttrs___closed__4); -l_Lean_mkReducibilityAttrs___closed__5___boxed__const__1 = _init_l_Lean_mkReducibilityAttrs___closed__5___boxed__const__1(); -lean_mark_persistent(l_Lean_mkReducibilityAttrs___closed__5___boxed__const__1); l_Lean_mkReducibilityAttrs___closed__5 = _init_l_Lean_mkReducibilityAttrs___closed__5(); lean_mark_persistent(l_Lean_mkReducibilityAttrs___closed__5); l_Lean_mkReducibilityAttrs___closed__6 = _init_l_Lean_mkReducibilityAttrs___closed__6(); @@ -3304,8 +3250,6 @@ l_Lean_mkReducibilityAttrs___closed__7 = _init_l_Lean_mkReducibilityAttrs___clos lean_mark_persistent(l_Lean_mkReducibilityAttrs___closed__7); l_Lean_mkReducibilityAttrs___closed__8 = _init_l_Lean_mkReducibilityAttrs___closed__8(); lean_mark_persistent(l_Lean_mkReducibilityAttrs___closed__8); -l_Lean_mkReducibilityAttrs___closed__9___boxed__const__1 = _init_l_Lean_mkReducibilityAttrs___closed__9___boxed__const__1(); -lean_mark_persistent(l_Lean_mkReducibilityAttrs___closed__9___boxed__const__1); l_Lean_mkReducibilityAttrs___closed__9 = _init_l_Lean_mkReducibilityAttrs___closed__9(); lean_mark_persistent(l_Lean_mkReducibilityAttrs___closed__9); l_Lean_mkReducibilityAttrs___closed__10 = _init_l_Lean_mkReducibilityAttrs___closed__10(); @@ -3314,8 +3258,6 @@ l_Lean_mkReducibilityAttrs___closed__11 = _init_l_Lean_mkReducibilityAttrs___clo lean_mark_persistent(l_Lean_mkReducibilityAttrs___closed__11); l_Lean_mkReducibilityAttrs___closed__12 = _init_l_Lean_mkReducibilityAttrs___closed__12(); lean_mark_persistent(l_Lean_mkReducibilityAttrs___closed__12); -l_Lean_mkReducibilityAttrs___closed__13___boxed__const__1 = _init_l_Lean_mkReducibilityAttrs___closed__13___boxed__const__1(); -lean_mark_persistent(l_Lean_mkReducibilityAttrs___closed__13___boxed__const__1); l_Lean_mkReducibilityAttrs___closed__13 = _init_l_Lean_mkReducibilityAttrs___closed__13(); lean_mark_persistent(l_Lean_mkReducibilityAttrs___closed__13); l_Lean_mkReducibilityAttrs___closed__14 = _init_l_Lean_mkReducibilityAttrs___closed__14(); @@ -3332,8 +3274,6 @@ w = l_Lean_mkReducibilityAttrs(w); if (lean_io_result_is_error(w)) return w; l_Lean_reducibilityAttrs = lean_io_result_get_value(w); lean_mark_persistent(l_Lean_reducibilityAttrs); -l_Lean_EnumAttributes_getValue___at_Lean_getReducibilityStatus___spec__1___boxed__const__1 = _init_l_Lean_EnumAttributes_getValue___at_Lean_getReducibilityStatus___spec__1___boxed__const__1(); -lean_mark_persistent(l_Lean_EnumAttributes_getValue___at_Lean_getReducibilityStatus___spec__1___boxed__const__1); return w; } #ifdef __cplusplus