max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(boot): update

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-11 12:54:41 -08:00
parent 57411ed039
commit 57ed6fea3a
11 changed files with 391 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
src/boot/init/core.cpp
View file

@ -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<void*>(lean::nat_add), 2, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_nat_add___boxed), 2, 0);
return x_0;
}
}

71
src/boot/init/data/int/basic.cpp
View file

@ -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<void*>(lean::int_neg), 1, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(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<void*>(lean::int_add), 2, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(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<void*>(lean::int_mul), 2, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(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<void*>(lean::int_sub), 2, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(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:
{

22
src/boot/init/data/nat/basic.cpp
View file

@ -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<void*>(lean::nat_sub), 2, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(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<void*>(lean::nat_mul), 2, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_nat_mul___boxed), 2, 0);
return x_0;
}
}

22
src/boot/init/data/nat/div.cpp
View file

@ -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<void*>(lean::nat_div), 2, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(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<void*>(lean::nat_mod), 2, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_nat_mod___boxed), 2, 0);
return x_0;
}
}

130
src/boot/init/data/string/basic.cpp
View file

@ -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<void*>(lean::string_length), 1, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(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<void*>(lean::string_append), 2, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_string_append___boxed), 2, 0);
return x_0;
}
}

72
src/boot/init/io.cpp
View file

@ -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<void*>(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<void*>(lean::io_prim_put_str), 2, 1);
x_5 = lean::alloc_closure(reinterpret_cast<void*>(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<void*>(lean::io_prim_put_str), 2, 1);
x_5 = lean::alloc_closure(reinterpret_cast<void*>(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<void*>(lean::io_prim_handle_is_eof), 2, 1);
x_5 = lean::alloc_closure(reinterpret_cast<void*>(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<void*>(lean::io_prim_handle_flush), 2, 1);
x_5 = lean::alloc_closure(reinterpret_cast<void*>(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<void*>(lean::io_prim_handle_flush), 2, 1);
x_5 = lean::alloc_closure(reinterpret_cast<void*>(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<void*>(lean::io_prim_handle_get_line), 2, 1);
x_5 = lean::alloc_closure(reinterpret_cast<void*>(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<void*>(lean::io_prim_handle_is_eof), 2, 1);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(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<void*>(lean::io_prim_handle_get_line), 2, 1);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(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<void*>(lean::io_prim_put_str), 2, 1);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(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;

39
src/boot/init/lean/elaborator.cpp
View file

@ -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();

3
src/boot/init/lean/frontend.cpp
View file

@ -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<void*>(lean::io_prim_put_str), 2, 1);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(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;

3
src/boot/init/lean/parser/identifier.cpp
View file

@ -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<void*>(lean::string_append), 2, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_string_append___boxed), 2, 0);
return x_0;
}
}

6
src/boot/init/lean/parser/parsec.cpp
View file

@ -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<void*>(lean::string_iterator_remaining), 1, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(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<void*>(lean::string_iterator_offset), 1, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_string_iterator_offset___boxed), 1, 0);
return x_0;
}
}

2
src/boot/init/version.cpp
View file

@ -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;
}
}