diff --git a/src/boot/init/core.cpp b/src/boot/init/core.cpp index 19db686847..aa155cfa50 100644 --- a/src/boot/init/core.cpp +++ b/src/boot/init/core.cpp @@ -52,6 +52,7 @@ obj* l_std_priority_max; obj* l_quot_rec___rarg(obj*, obj*, obj*); obj* l_or_intro__right; obj* l_ne; +obj* l_thunk_pure___boxed(obj*, obj*); obj* l_prod_has__lt(obj*, obj*, obj*, obj*); obj* l_eq_ndrec__on(obj*, obj*, obj*, obj*, obj*); obj* l_inline(obj*); @@ -71,6 +72,7 @@ obj* l_flip___rarg(obj*, obj*, obj*); obj* l_sigma_has__sizeof(obj*, obj*); obj* l_id__delta___rarg(obj*); obj* l_bool_has__sizeof; +obj* l_thunk_get___boxed(obj*, obj*); obj* l_prod_map(obj*, obj*, obj*, obj*); obj* l_subtype_sizeof___main___rarg(obj*, obj*, obj*); obj* l_prod__has__decidable__lt(obj*, obj*, obj*, obj*); @@ -99,6 +101,7 @@ obj* l_or_symm; obj* l_sum_sizeof___main(obj*, obj*); obj* l_prod_decidable__eq___rarg___boxed(obj*, obj*, obj*, obj*); uint8 l_bxor___main(uint8, uint8); +obj* l_nat_add___boxed(obj*, obj*); obj* l_of__as__true; obj* l_quotient_decidable__eq___rarg(obj*, obj*, obj*, obj*); obj* l_sigma_sizeof___main___at_sigma_has__sizeof___spec__2___rarg(obj*, obj*, obj*); @@ -368,6 +371,7 @@ obj* l_psum_sizeof___main(obj*, obj*); obj* l___private_4253352285__extfun__app(obj*, obj*); obj* l_decidable__of__decidable__eq(obj*); obj* l_cond(obj*); +obj* l_thunk_map___boxed(obj*, obj*, obj*, obj*); obj* l_rfl; obj* l_true_inhabited; obj* l_subrelation; @@ -384,6 +388,7 @@ obj* l_forall__prop__decidable(obj*, obj*); uint8 l_and_decidable___rarg(obj*, obj*); obj* l_combinator_K(obj*, obj*); obj* l_quotient_lift__on(obj*, obj*, obj*); +obj* l_thunk_bind___boxed(obj*, obj*, obj*, obj*); obj* l_irreflexive; obj* l_false_elim(obj*, uint8); obj* l_option_sizeof___rarg(obj*, obj*); @@ -517,6 +522,38 @@ x_0 = lean::box(0); return x_0; } } +obj* l_thunk_pure___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::thunk_pure(x_1); +return x_2; +} +} +obj* l_thunk_get___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::thunk_get(x_1); +return x_2; +} +} +obj* l_thunk_map___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { +_start: +{ +obj* x_4; +x_4 = lean::thunk_map(x_2, x_3); +return x_4; +} +} +obj* l_thunk_bind___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { +_start: +{ +obj* x_4; +x_4 = lean::thunk_bind(x_2, x_3); +return x_4; +} +} obj* l_task_pure___rarg(obj* x_0, obj* x_1) { _start: { @@ -846,6 +883,14 @@ return x_0; } } } +obj* l_nat_add___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::nat_add(x_0, x_1); +return x_2; +} +} obj* _init_l_nat_has__zero() { _start: { @@ -866,7 +911,7 @@ obj* _init_l_nat_has__add() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(lean::nat_add), 2, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_nat_add___boxed), 2, 0); return x_0; } } diff --git a/src/boot/init/data/int/basic.cpp b/src/boot/init/data/int/basic.cpp index 77eba6a37d..e9e2f7d635 100644 --- a/src/boot/init/data/int/basic.cpp +++ b/src/boot/init/data/int/basic.cpp @@ -26,13 +26,17 @@ obj* l_int_fdiv___main(obj*, obj*); obj* l_int_has__sub; obj* l_int_mul___main(obj*, obj*); obj* l_int_nat__abs___main(obj*); +obj* l_int_add___boxed(obj*, obj*); extern uint8 l_false_decidable; +obj* l_int_neg___boxed(obj*); obj* l_int_repr___main(obj*); obj* l_int_mod(obj*, obj*); obj* l___private_1805987925__nonneg; obj* l_int_to__nat___main(obj*); obj* l_int_nat__abs___main___closed__1; +obj* l_int_quot___boxed(obj*, obj*); obj* l_int_quot___main(obj*, obj*); +obj* l_int_sub___boxed(obj*, obj*); obj* l___private_3285259795__dec__nonneg___main___boxed(obj*); obj* l_int_has__mul; obj* l___private_1805987925__nonneg___main; @@ -40,8 +44,10 @@ obj* l_int_lt; obj* l_int_neg__of__nat___main(obj*); obj* l_int_has__lt; obj* l_int_add___main(obj*, obj*); +obj* l_int_nat__abs___boxed(obj*); obj* l_int_sub__nat__nat(obj*, obj*); obj* l_int_dec__lt___boxed(obj*, obj*); +obj* l_int_rem___boxed(obj*, obj*); obj* l_int_zero; obj* l_int_has__div; obj* l_int_div___main(obj*, obj*); @@ -66,6 +72,7 @@ obj* l_int_rem___main(obj*, obj*); obj* l_int_has__to__string; obj* l_int_mod___main(obj*, obj*); obj* l_nat_repr(obj*); +obj* l_int_mul___boxed(obj*, obj*); obj* l_int_sign___main(obj*); obj* l_int_has__add; obj* l_int_le; @@ -120,6 +127,14 @@ lean::dec(x_0); return x_1; } } +obj* l_int_nat__abs___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::nat_abs(x_0); +return x_1; +} +} uint8 l_dec__eq(obj* x_0, obj* x_1) { _start: { @@ -420,6 +435,14 @@ return x_14; } } } +obj* l_int_neg___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::int_neg(x_0); +return x_1; +} +} obj* l_int_add___main(obj* x_0, obj* x_1) { _start: { @@ -499,6 +522,14 @@ return x_45; } } } +obj* l_int_add___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::int_add(x_0, x_1); +return x_2; +} +} obj* l_int_mul___main(obj* x_0, obj* x_1) { _start: { @@ -586,11 +617,19 @@ return x_53; } } } +obj* l_int_mul___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::int_mul(x_0, x_1); +return x_2; +} +} obj* _init_l_int_has__neg() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(lean::int_neg), 1, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_int_neg___boxed), 1, 0); return x_0; } } @@ -598,7 +637,7 @@ obj* _init_l_int_has__add() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(lean::int_add), 2, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_int_add___boxed), 2, 0); return x_0; } } @@ -606,15 +645,23 @@ obj* _init_l_int_has__mul() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(lean::int_mul), 2, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_int_mul___boxed), 2, 0); return x_0; } } +obj* l_int_sub___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::int_sub(x_0, x_1); +return x_2; +} +} obj* _init_l_int_has__sub() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(lean::int_sub), 2, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_int_sub___boxed), 2, 0); return x_0; } } @@ -1171,6 +1218,14 @@ return x_59; } } } +obj* l_int_quot___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::int_div(x_0, x_1); +return x_2; +} +} obj* l_int_rem___main(obj* x_0, obj* x_1) { _start: { @@ -1264,6 +1319,14 @@ return x_59; } } } +obj* l_int_rem___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::int_rem(x_0, x_1); +return x_2; +} +} obj* _init_l_int_has__div() { _start: { diff --git a/src/boot/init/data/nat/basic.cpp b/src/boot/init/data/nat/basic.cpp index f51a66686f..38ff6c5f7b 100644 --- a/src/boot/init/data/nat/basic.cpp +++ b/src/boot/init/data/nat/basic.cpp @@ -18,6 +18,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #endif obj* l_nat_mul___main(obj*, obj*); obj* l_nat_has__sub; +obj* l_nat_mul___boxed(obj*, obj*); obj* l_nat_max(obj*, obj*); obj* l_nat_le__refl; obj* l_nat_beq___main(obj*, obj*); @@ -44,6 +45,7 @@ obj* l_nat_dec__le___boxed(obj*, obj*); obj* l_nat_beq(obj*, obj*); obj* l_nat_repeat__core(obj*); obj* l_nat_pred(obj*); +obj* l_nat_sub___boxed(obj*, obj*); obj* l_nat_has__le; obj* l_nat_le; obj* l_nat_ble___main(obj*, obj*); @@ -278,6 +280,14 @@ return x_0; } } } +obj* l_nat_sub___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::nat_sub(x_0, x_1); +return x_2; +} +} obj* l_nat_mul___main(obj* x_0, obj* x_1) { _start: { @@ -309,11 +319,19 @@ return x_16; } } } +obj* l_nat_mul___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::nat_mul(x_0, x_1); +return x_2; +} +} obj* _init_l_nat_has__sub() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(lean::nat_sub), 2, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_nat_sub___boxed), 2, 0); return x_0; } } @@ -321,7 +339,7 @@ obj* _init_l_nat_has__mul() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(lean::nat_mul), 2, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_nat_mul___boxed), 2, 0); return x_0; } } diff --git a/src/boot/init/data/nat/div.cpp b/src/boot/init/data/nat/div.cpp index bd7d8eb132..7ace870e23 100644 --- a/src/boot/init/data/nat/div.cpp +++ b/src/boot/init/data/nat/div.cpp @@ -16,11 +16,13 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #pragma GCC diagnostic ignored "-Wunused-label" #pragma GCC diagnostic ignored "-Wunused-but-set-variable" #endif +obj* l_nat_mod___boxed(obj*, obj*); obj* l___private_578911941__mod_F(obj*, obj*, obj*); obj* l_nat_has__div; obj* l___private_3925169175__div_F(obj*, obj*, obj*); obj* l___private_56172073__div__rec__lemma; obj* l_nat_has__mod; +obj* l_nat_div___boxed(obj*, obj*); obj* _init_l___private_56172073__div__rec__lemma() { _start: { @@ -74,11 +76,19 @@ return x_19; } } } +obj* l_nat_div___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::nat_div(x_0, x_1); +return x_2; +} +} obj* _init_l_nat_has__div() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(lean::nat_div), 2, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_nat_div___boxed), 2, 0); return x_0; } } @@ -116,11 +126,19 @@ return x_13; } } } +obj* l_nat_mod___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::nat_mod(x_0, x_1); +return x_2; +} +} obj* _init_l_nat_has__mod() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(lean::nat_mod), 2, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_nat_mod___boxed), 2, 0); return x_0; } } diff --git a/src/boot/init/data/string/basic.cpp b/src/boot/init/data/string/basic.cpp index 889e0b1baa..9a9b565429 100644 --- a/src/boot/init/data/string/basic.cpp +++ b/src/boot/init/data/string/basic.cpp @@ -17,14 +17,17 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #pragma GCC diagnostic ignored "-Wunused-but-set-variable" #endif obj* l_string_iterator_to__end___main(obj*); +obj* l_string_iterator_next___boxed(obj*); obj* l_string_iterator_has__prev___main___boxed(obj*); obj* l_string_backn(obj*, obj*); obj* l_string_iterator_prevn(obj*, obj*); uint32 l_string_front(obj*); uint8 l_char_is__whitespace(uint32); +obj* l_string_iterator_prev__to__string___boxed(obj*); obj* l_string_pushn___boxed(obj*, obj*, obj*); obj* l_string_has__lt; obj* l___private_3344645481__to__nat__core(obj*, obj*, obj*); +obj* l_string_iterator_remaining___boxed(obj*); obj* l_string_iterator_forward(obj*, obj*); obj* l_string_iterator_extract___main___closed__1; obj* l_string_line__column___closed__1; @@ -50,6 +53,7 @@ obj* l_string_iterator_remaining__to__string___main(obj*); obj* l_string_front___boxed(obj*); uint8 l_string_is__empty(obj*); obj* l_string_mk__iterator___main(obj*); +obj* l_string_iterator_insert___boxed(obj*, obj*); obj* l___private_3868098097__trim__left__aux(obj*, obj*); obj* l___private_104996535__line__column__aux___main(obj*, obj*, obj*); obj* l_string_pop__back(obj*); @@ -61,6 +65,7 @@ uint32 l_string_back(obj*); obj* l_option_get__or__else___main___rarg(obj*, obj*); obj* l_string_iterator_prev___main(obj*); obj* l_string_iterator_to__string___main(obj*); +obj* l_string_append___boxed(obj*, obj*); obj* l_string_str(obj*, uint32); obj* l_string_to__nat(obj*); obj* l_list_drop___main___rarg(obj*, obj*); @@ -68,9 +73,13 @@ obj* l_string_line__column(obj*, obj*); obj* l_string_iterator_set__curr___main(obj*, uint32); obj* l_string_iterator_nextn___main(obj*, obj*); obj* l___private_104996535__line__column__aux(obj*, obj*, obj*); +obj* l_string_length___boxed(obj*); obj* l_string_iterator_has__next___main___boxed(obj*); +obj* l_string_iterator_to__string___boxed(obj*); +obj* l_string_iterator_remove___boxed(obj*, obj*); obj* l_string_join___closed__1; obj* l_list_foldl___main___at_string_join___spec__1(obj*, obj*); +obj* l_string_iterator_offset___boxed(obj*); extern obj* l_char_inhabited; obj* l_string_iterator_insert___main(obj*, obj*); obj* l_string_has__append; @@ -83,6 +92,7 @@ obj* l_string_join(obj*); uint8 l_string_iterator_decidable__rel(obj*, obj*); obj* l_string_push___boxed(obj*, obj*); obj* l_string_dec__eq___boxed(obj*, obj*); +obj* l_string_mk__iterator___boxed(obj*); obj* l_string_iterator_decidable__rel___boxed(obj*, obj*); obj* l_string_append___main(obj*, obj*); obj* l_list_has__dec__eq___main___at_string_iterator_extract__core___main___spec__1___boxed(obj*, obj*); @@ -101,12 +111,16 @@ obj* l_string_iterator_curr___main(obj*); obj* l_string_iterator_set__curr___boxed(obj*, obj*); obj* l_nat_repeat__core___main___at_string_pushn___spec__1___boxed(obj*, obj*, obj*, obj*); uint8 l_string_iterator_has__next___main(obj*); +obj* l_string_iterator_prev___boxed(obj*); obj* l_string_iterator_prev__to__string___main(obj*); obj* l_string_is__empty___boxed(obj*); +obj* l_string_iterator_to__end___boxed(obj*); +obj* l_string_iterator_extract___boxed(obj*, obj*); obj* l_string_iterator_set__curr___main___boxed(obj*, obj*); obj* l_string_trim__left(obj*); obj* l_list_append___rarg(obj*, obj*); obj* l_string_str___boxed(obj*, obj*); +obj* l_string_iterator_remaining__to__string___boxed(obj*); obj* l_string_iterator_remove___main(obj*, obj*); obj* l_string_iterator_next___main(obj*); obj* l_string_iterator_has__prev___boxed(obj*); @@ -156,6 +170,14 @@ x_3 = l_list_length__aux___main___rarg(x_1, x_2); return x_3; } } +obj* l_string_length___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::string_length(x_0); +return x_1; +} +} obj* l_string_push___main(obj* x_0, uint32 x_1) { _start: { @@ -200,6 +222,14 @@ x_5 = lean::string_mk(x_4); return x_5; } } +obj* l_string_append___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::string_append(x_0, x_1); +return x_2; +} +} obj* l_string_to__list(obj* x_0) { _start: { @@ -220,6 +250,14 @@ lean::dec(x_2); return x_3; } } +obj* l_string_mk__iterator___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::string_mk_iterator(x_0); +return x_1; +} +} obj* l_string_iterator_remaining___main(obj* x_0) { _start: { @@ -231,6 +269,14 @@ x_4 = l_list_length__aux___main___rarg(x_1, x_3); return x_4; } } +obj* l_string_iterator_remaining___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::string_iterator_remaining(x_0); +return x_1; +} +} obj* l_string_iterator_offset___main(obj* x_0) { _start: { @@ -242,6 +288,14 @@ x_4 = l_list_length__aux___main___rarg(x_1, x_3); return x_4; } } +obj* l_string_iterator_offset___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::string_iterator_offset(x_0); +return x_1; +} +} obj* l_string_iterator_curr___main(obj* x_0) { _start: { @@ -374,6 +428,14 @@ return x_11; } } } +obj* l_string_iterator_next___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::string_iterator_next(x_0); +return x_1; +} +} obj* l_string_iterator_prev___main(obj* x_0) { _start: { @@ -415,6 +477,14 @@ return x_11; } } } +obj* l_string_iterator_prev___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::string_iterator_prev(x_0); +return x_1; +} +} uint8 l_string_iterator_has__next___main(obj* x_0) { _start: { @@ -510,6 +580,14 @@ lean::dec(x_2); return x_7; } } +obj* l_string_iterator_insert___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::string_iterator_insert(x_0, x_1); +return x_2; +} +} obj* l_string_iterator_remove___main(obj* x_0, obj* x_1) { _start: { @@ -524,6 +602,14 @@ lean::dec(x_2); return x_6; } } +obj* l_string_iterator_remove___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::string_iterator_remove(x_0, x_1); +return x_2; +} +} obj* l_string_iterator_to__string___main(obj* x_0) { _start: { @@ -537,6 +623,14 @@ x_6 = lean::string_mk(x_5); return x_6; } } +obj* l_string_iterator_to__string___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::string_iterator_to_string(x_0); +return x_1; +} +} obj* l_string_iterator_forward___main(obj* x_0, obj* x_1) { _start: { @@ -587,6 +681,14 @@ lean::dec(x_5); return x_7; } } +obj* l_string_iterator_to__end___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::string_iterator_to_end(x_0); +return x_1; +} +} obj* l_string_iterator_remaining__to__string___main(obj* x_0) { _start: { @@ -597,6 +699,14 @@ x_3 = lean::string_mk(x_1); return x_3; } } +obj* l_string_iterator_remaining__to__string___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::string_iterator_remaining_to_string(x_0); +return x_1; +} +} obj* l_string_iterator_prev__to__string___main(obj* x_0) { _start: { @@ -608,6 +718,14 @@ x_4 = lean::string_mk(x_3); return x_4; } } +obj* l_string_iterator_prev__to__string___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::string_iterator_prev_to_string(x_0); +return x_1; +} +} uint8 l_list_has__dec__eq___main___at_string_iterator_extract__core___main___spec__1(obj* x_0, obj* x_1) { _start: { @@ -876,6 +994,14 @@ lean::cnstr_set(x_1, 0, x_0); return x_1; } } +obj* l_string_iterator_extract___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::string_iterator_extract(x_0, x_1); +return x_2; +} +} obj* _init_l_string_iterator_is__prefix__of__remaining() { _start: { @@ -950,7 +1076,7 @@ obj* _init_l_string_has__sizeof() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(lean::string_length), 1, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_string_length___boxed), 1, 0); return x_0; } } @@ -958,7 +1084,7 @@ obj* _init_l_string_has__append() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(lean::string_append), 2, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_string_append___boxed), 2, 0); return x_0; } } diff --git a/src/boot/init/io.cpp b/src/boot/init/io.cpp index 1f8cbb7f50..48cf756da8 100644 --- a/src/boot/init/io.cpp +++ b/src/boot/init/io.cpp @@ -30,10 +30,12 @@ obj* l_io_prim_lift__eio___at_io_fs_handle_read__to__end___spec__7(obj*, obj*); obj* l_io_prim_lift__eio___rarg___lambda__1(obj*, obj*, obj*, obj*); obj* l_io; obj* l_coroutine__io_mk__st(obj*, obj*, obj*); +obj* l_io_prim_handle_get__line___boxed(obj*, obj*); obj* l_coroutine__io_monad___closed__1; obj* l_coroutine__io_pipe___main(obj*, obj*, obj*, obj*); obj* l_io_fs_handle_flush___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_coroutine__io_resume___main(obj*, obj*, obj*); +obj* l_io_prim_handle_flush___boxed(obj*, obj*); obj* l_coroutine__io_yield___rarg(obj*, obj*, obj*); obj* l_io_prim_lift__eio___at_io_fs_handle_is__eof___spec__1___rarg___lambda__1(obj*, obj*, obj*, obj*); obj* l_io_has__eval(obj*); @@ -48,6 +50,8 @@ obj* l_io_prim_iterate___main___at_io_prim_iterate__eio___spec__1___rarg(obj*, o obj* l_io_fs_handle_flush(obj*, obj*); obj* l_io_prim_lift__eio___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_io_prim_iterate___main(obj*, obj*); +obj* l_io_prim_get__line___boxed(obj*); +obj* l_io_prim_handle_is__eof___boxed(obj*, obj*); obj* l_io_prim_handle_mk___boxed(obj*, obj*, obj*, obj*); obj* l_io_fs_read__file___rarg(obj*, obj*, obj*, obj*, obj*, uint8); obj* l_coroutine__io_pure(obj*, obj*, obj*); @@ -73,6 +77,7 @@ obj* l_io_prim_iterate___main___at_io_prim_iterate__eio___spec__1(obj*, obj*, ob obj* l_io_fs_read__file___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_io_fs_handle_read__to__end(obj*, obj*); obj* l_id_bind(obj*, obj*); +obj* l_io_prim_put__str___boxed(obj*, obj*); obj* l_coroutine__io_monad___lambda__7(obj*, obj*, obj*, obj*); obj* l_coroutine__io_bind(obj*, obj*, obj*, obj*); obj* l___private_3644302523__put__str(obj*, obj*); @@ -134,6 +139,7 @@ obj* l_io_fs_handle_read__to__end___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_coroutine__io_bind___main(obj*, obj*, obj*, obj*); obj* l_coroutine__io_resume___main___rarg(obj*, obj*, obj*); extern obj* l_coroutine_yield___rarg___lambda__1___closed__1; +obj* l_io_prim_handle_close___boxed(obj*, obj*); obj* l_io_println(obj*, obj*); obj* l_coroutine__io_monad__io___rarg(obj*, obj*, obj*); obj* l_io_print___at_io_println_x_27___spec__2(obj*, obj*); @@ -435,6 +441,22 @@ x_6 = lean::alloc_closure(reinterpret_cast(l_io_prim_iterate__eio___rarg) return x_6; } } +obj* l_io_prim_put__str___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::io_prim_put_str(x_0, x_1); +return x_2; +} +} +obj* l_io_prim_get__line___boxed(obj* x_0) { +_start: +{ +obj* x_1; +x_1 = lean::io_prim_get_line(x_0); +return x_1; +} +} obj* l_io_prim_handle_mk___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { _start: { @@ -445,6 +467,38 @@ x_6 = lean::io_prim_handle_mk(x_0, x_4, x_5, x_3); return x_6; } } +obj* l_io_prim_handle_is__eof___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::io_prim_handle_is_eof(x_0, x_1); +return x_2; +} +} +obj* l_io_prim_handle_flush___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::io_prim_handle_flush(x_0, x_1); +return x_2; +} +} +obj* l_io_prim_handle_close___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::io_prim_handle_close(x_0, x_1); +return x_2; +} +} +obj* l_io_prim_handle_get__line___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean::io_prim_handle_get_line(x_0, x_1); +return x_2; +} +} obj* l_io_prim_lift__eio___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) { _start: { @@ -536,7 +590,7 @@ obj* l___private_3644302523__put__str___rarg(obj* x_0, obj* x_1, obj* x_2, obj* _start: { obj* x_5; obj* x_6; -x_5 = lean::alloc_closure(reinterpret_cast(lean::io_prim_put_str), 2, 1); +x_5 = lean::alloc_closure(reinterpret_cast(l_io_prim_put__str___boxed), 2, 1); lean::closure_set(x_5, 0, x_4); x_6 = l_io_prim_lift__eio___at___private_3644302523__put__str___spec__1___rarg(x_0, x_1, x_2, x_3, x_5); return x_6; @@ -601,7 +655,7 @@ obj* l___private_3644302523__put__str___at_io_println___spec__1___rarg(obj* x_0, _start: { obj* x_5; obj* x_6; -x_5 = lean::alloc_closure(reinterpret_cast(lean::io_prim_put_str), 2, 1); +x_5 = lean::alloc_closure(reinterpret_cast(l_io_prim_put__str___boxed), 2, 1); lean::closure_set(x_5, 0, x_4); x_6 = l_io_prim_lift__eio___at_io_println___spec__2___rarg(x_0, x_1, x_2, x_3, x_5); return x_6; @@ -781,7 +835,7 @@ obj* l_io_fs_handle_is__eof___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* _start: { obj* x_5; obj* x_6; -x_5 = lean::alloc_closure(reinterpret_cast(lean::io_prim_handle_is_eof), 2, 1); +x_5 = lean::alloc_closure(reinterpret_cast(l_io_prim_handle_is__eof___boxed), 2, 1); lean::closure_set(x_5, 0, x_4); x_6 = l_io_prim_lift__eio___at_io_fs_handle_is__eof___spec__1___rarg(x_0, x_1, x_2, x_3, x_5); return x_6; @@ -826,7 +880,7 @@ obj* l_io_fs_handle_flush___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_ _start: { obj* x_5; obj* x_6; -x_5 = lean::alloc_closure(reinterpret_cast(lean::io_prim_handle_flush), 2, 1); +x_5 = lean::alloc_closure(reinterpret_cast(l_io_prim_handle_flush___boxed), 2, 1); lean::closure_set(x_5, 0, x_4); x_6 = l_io_prim_lift__eio___at_io_fs_handle_flush___spec__1___rarg(x_0, x_1, x_2, x_3, x_5); return x_6; @@ -871,7 +925,7 @@ obj* l_io_fs_handle_close___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_ _start: { obj* x_5; obj* x_6; -x_5 = lean::alloc_closure(reinterpret_cast(lean::io_prim_handle_flush), 2, 1); +x_5 = lean::alloc_closure(reinterpret_cast(l_io_prim_handle_flush___boxed), 2, 1); lean::closure_set(x_5, 0, x_4); x_6 = l_io_prim_lift__eio___at_io_fs_handle_close___spec__1___rarg(x_0, x_1, x_2, x_3, x_5); return x_6; @@ -916,7 +970,7 @@ obj* l_io_fs_handle_get__line___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj _start: { obj* x_5; obj* x_6; -x_5 = lean::alloc_closure(reinterpret_cast(lean::io_prim_handle_get_line), 2, 1); +x_5 = lean::alloc_closure(reinterpret_cast(l_io_prim_handle_get__line___boxed), 2, 1); lean::closure_set(x_5, 0, x_4); x_6 = l_io_prim_lift__eio___at_io_fs_handle_get__line___spec__1___rarg(x_0, x_1, x_2, x_3, x_5); return x_6; @@ -1009,7 +1063,7 @@ obj* l_io_fs_handle_is__eof___at_io_fs_handle_read__to__end___spec__1(obj* x_0, _start: { obj* x_2; obj* x_3; -x_2 = lean::alloc_closure(reinterpret_cast(lean::io_prim_handle_is_eof), 2, 1); +x_2 = lean::alloc_closure(reinterpret_cast(l_io_prim_handle_is__eof___boxed), 2, 1); lean::closure_set(x_2, 0, x_0); x_3 = l_io_prim_lift__eio___at_io_fs_handle_read__to__end___spec__2(x_2, x_1); return x_3; @@ -1092,7 +1146,7 @@ obj* l_io_fs_handle_get__line___at_io_fs_handle_read__to__end___spec__3(obj* x_0 _start: { obj* x_2; obj* x_3; -x_2 = lean::alloc_closure(reinterpret_cast(lean::io_prim_handle_get_line), 2, 1); +x_2 = lean::alloc_closure(reinterpret_cast(l_io_prim_handle_get__line___boxed), 2, 1); lean::closure_set(x_2, 0, x_0); x_3 = l_io_prim_lift__eio___at_io_fs_handle_read__to__end___spec__4(x_2, x_1); return x_3; @@ -1576,7 +1630,7 @@ obj* l___private_3644302523__put__str___at_io_println_x_27___spec__3(obj* x_0, o _start: { obj* x_2; obj* x_3; -x_2 = lean::alloc_closure(reinterpret_cast(lean::io_prim_put_str), 2, 1); +x_2 = lean::alloc_closure(reinterpret_cast(l_io_prim_put__str___boxed), 2, 1); lean::closure_set(x_2, 0, x_0); x_3 = l_io_prim_lift__eio___at_io_println_x_27___spec__4(x_2, x_1); return x_3; diff --git a/src/boot/init/lean/elaborator.cpp b/src/boot/init/lean/elaborator.cpp index 9a2ffc0262..85e5081b2f 100644 --- a/src/boot/init/lean/elaborator.cpp +++ b/src/boot/init/lean/elaborator.cpp @@ -192,6 +192,7 @@ extern obj* l_lean_parser_command_include; obj* l_coe___at_lean_elaborator_command__parser__config_register__notation__parser___spec__4(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_list_mmap___main___at_lean_elaborator_to__pexpr___main___spec__13(obj*, obj*, obj*, obj*); obj* l_lean_elaborator_ordered__rbmap_insert___at_lean_elaborator_variables_elaborate___spec__3(obj*, obj*, obj*); +obj* l_lean_environment_contains___boxed(obj*, obj*); obj* l_list_mmap___main___at_lean_elaborator_to__pexpr___main___spec__17(obj*, obj*, obj*, obj*); extern obj* l_lean_name_to__string___closed__1; obj* l_rbmap_from__list___at_lean_elaborator_elaborators___spec__1___lambda__6(obj*, obj*, obj*); @@ -462,6 +463,7 @@ obj* l_lean_elaborator_infer__mod__to__pexpr___closed__1; extern obj* l_lean_parser_command_section; obj* l_list_mfilter___main___at_lean_elaborator_variables_elaborate___spec__4(obj*, obj*, obj*); obj* l_reader__t_lift(obj*, obj*, obj*, obj*); +obj* l_lean_environment_empty___boxed; obj* l_lean_elaborator_to__pexpr___main___closed__21; obj* l_lean_elaborator_locally___at_lean_elaborator_section_elaborate___spec__2___lambda__4(obj*, obj*, obj*, obj*); extern obj* l_lean_parser_term_struct__inst__item_has__view; @@ -527,10 +529,12 @@ obj* l_lean_expander_mk__notation__transformer(obj*, obj*, obj*); obj* l_rbmap_from__list___at_lean_elaborator_elaborators___spec__1___lambda__2(obj*, obj*, obj*); obj* l_lean_elaborator_ordered__rbmap_insert(obj*, obj*, obj*); obj* l_lean_elaborator_to__pexpr___main___closed__30; +obj* l_lean_expr_local___boxed(obj*, obj*, obj*, obj*); obj* l_lean_elaborator_mk__eqns(obj*, obj*); obj* l_rbmap_insert___main___at_lean_elaborator_old__elab__command___spec__3(obj*, obj*, obj*); obj* l_lean_elaborator_locally___rarg___lambda__1(obj*); obj* l_lean_elaborator_level__add___main(obj*, obj*); +obj* l_lean_elaborator_elaborate__command___boxed(obj*, obj*, obj*); obj* l_reader__t_monad___rarg(obj*); obj* l_lean_expr_mk__capp(obj*, obj*); obj* l_list_foldr___main___at_lean_elaborator_to__level___main___spec__4(obj*, obj*); @@ -638,6 +642,38 @@ obj* l_lean_elaborator_init__quot_elaborate___closed__1; obj* l_lean_elaborator_postprocess__notation__spec___closed__1; obj* l_lean_elaborator_locally___at_lean_elaborator_section_elaborate___spec__2___closed__2; extern obj* l_lean_parser_command_set__option_has__view; +obj* _init_l_lean_environment_empty___boxed() { +_start: +{ +obj* x_0; +x_0 = l_lean_environment_empty; +return x_0; +} +} +obj* l_lean_environment_contains___boxed(obj* x_0, obj* x_1) { +_start: +{ +obj* x_2; +x_2 = lean_environment_contains(x_0, x_1); +return x_2; +} +} +obj* l_lean_expr_local___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { +_start: +{ +obj* x_4; +x_4 = lean_expr_local(x_0, x_1, x_2, x_3); +return x_4; +} +} +obj* l_lean_elaborator_elaborate__command___boxed(obj* x_0, obj* x_1, obj* x_2) { +_start: +{ +obj* x_3; +x_3 = lean_elaborator_elaborate_command(x_0, x_1, x_2); +return x_3; +} +} obj* l_lean_elaborator_ordered__rbmap_empty(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { _start: { @@ -28220,7 +28256,7 @@ obj* _init_l_lean_elaborator_run___closed__2() { _start: { obj* x_0; -x_0 = lean_environment_empty; +x_0 = l_lean_environment_empty; lean::inc(x_0); return x_0; } @@ -28667,6 +28703,7 @@ void initialize_init_lean_elaborator() { initialize_init_lean_expander(); initialize_init_lean_expr(); initialize_init_lean_options(); + l_lean_environment_empty___boxed = _init_l_lean_environment_empty___boxed(); l_lean_elaborator_ordered__rbmap_empty___closed__1 = _init_l_lean_elaborator_ordered__rbmap_empty___closed__1(); l_lean_elaborator_elaborator__t = _init_l_lean_elaborator_elaborator__t(); l_lean_elaborator_elaborator__m = _init_l_lean_elaborator_elaborator__m(); diff --git a/src/boot/init/lean/frontend.cpp b/src/boot/init/lean/frontend.cpp index 034ed89d24..61084f1add 100644 --- a/src/boot/init/lean/frontend.cpp +++ b/src/boot/init/lean/frontend.cpp @@ -42,6 +42,7 @@ obj* l_lean_parser_module_parser(obj*, obj*, obj*); obj* l_io_prim_iterate___main___at_lean_run__frontend___spec__15(obj*, obj*, obj*); extern obj* l_lean_parser_term_builtin__trailing__parsers_lean_parser_has__tokens; extern obj* l_lean_parser_term_builtin__leading__parsers; +obj* l_io_prim_put__str___boxed(obj*, obj*); obj* l_io_prim_iterate___main___at_lean_run__frontend___spec__15___closed__1; obj* l_lean_parser_tokens___rarg(obj*); obj* l_lean_run__elaborator___rarg(obj*, obj*); @@ -503,7 +504,7 @@ obj* l___private_3644302523__put__str___at_lean_run__frontend___spec__5(obj* x_0 _start: { obj* x_2; obj* x_3; -x_2 = lean::alloc_closure(reinterpret_cast(lean::io_prim_put_str), 2, 1); +x_2 = lean::alloc_closure(reinterpret_cast(l_io_prim_put__str___boxed), 2, 1); lean::closure_set(x_2, 0, x_0); x_3 = l_io_prim_lift__eio___at_lean_run__frontend___spec__6(x_2, x_1); return x_3; diff --git a/src/boot/init/lean/parser/identifier.cpp b/src/boot/init/lean/parser/identifier.cpp index faa1c4e62c..f16274cbae 100644 --- a/src/boot/init/lean/parser/identifier.cpp +++ b/src/boot/init/lean/parser/identifier.cpp @@ -91,6 +91,7 @@ obj* l_lean_parser_monad__parsec_foldl__aux___main___at_lean_parser_identifier__ obj* l_lean_parser_id__part__default___rarg(obj*, obj*, obj*); uint8 l_lean_is__id__rest(uint32); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_identifier___spec__16(obj*, obj*); +obj* l_string_append___boxed(obj*, obj*); obj* l_lean_parser_monad__parsec_foldl___at_lean_parser_identifier___spec__19___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*); uint8 l_lean_is__greek(uint32); obj* l_lean_parser_c__identifier___rarg(obj*, obj*, obj*); @@ -4086,7 +4087,7 @@ obj* _init_l_lean_parser_cpp__identifier___rarg___lambda__2___closed__3() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(lean::string_append), 2, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_string_append___boxed), 2, 0); return x_0; } } diff --git a/src/boot/init/lean/parser/parsec.cpp b/src/boot/init/lean/parser/parsec.cpp index 970a245fdb..022e6f5987 100644 --- a/src/boot/init/lean/parser/parsec.cpp +++ b/src/boot/init/lean/parser/parsec.cpp @@ -71,6 +71,7 @@ obj* l_lean_parser_monad__parsec_sep__by1___rarg___closed__1; obj* l_lean_parser_monad__parsec_curr___rarg(obj*, obj*); obj* l_lean_parser_parsec__t_merge(obj*); obj* l_lean_parser_parsec__t_alternative___rarg(obj*, obj*); +obj* l_string_iterator_remaining___boxed(obj*); obj* l_lean_parser_monad__parsec_foldl__aux___main___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_unexpected__at___spec__1(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_longest__match___rarg___lambda__1(obj*, obj*); @@ -255,6 +256,7 @@ obj* l___private_31565857__take__while__aux___rarg(obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_foldr__aux___main___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_sep__by1___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg___lambda__1(obj*, obj*, obj*, obj*); +obj* l_string_iterator_offset___boxed(obj*); obj* l_lean_parser_monad__parsec_not__followed__by___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l___private_31565857__take__while__aux___main___at_lean_parser_monad__parsec_take__until___spec__2___rarg(obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_lower___spec__1(obj*, obj*, obj*); @@ -3112,7 +3114,7 @@ obj* _init_l_lean_parser_monad__parsec_remaining___rarg___closed__1() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(lean::string_iterator_remaining), 1, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_string_iterator_remaining___boxed), 1, 0); return x_0; } } @@ -6711,7 +6713,7 @@ obj* _init_l_lean_parser_monad__parsec_pos___rarg___closed__1() { _start: { obj* x_0; -x_0 = lean::alloc_closure(reinterpret_cast(lean::string_iterator_offset), 1, 0); +x_0 = lean::alloc_closure(reinterpret_cast(l_string_iterator_offset___boxed), 1, 0); return x_0; } } diff --git a/src/boot/init/version.cpp b/src/boot/init/version.cpp index 0a66948b28..f61b1ac5e8 100644 --- a/src/boot/init/version.cpp +++ b/src/boot/init/version.cpp @@ -41,7 +41,7 @@ obj* _init_l_lean_githash() { _start: { obj* x_0; -x_0 = lean::mk_string("1703255330eee84d2847975e3d9b545f22ddcb89"); +x_0 = lean::mk_string("57411ed0390c28a7a3a68617d19658c70e21cfb1"); return x_0; } }