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-03-12 14:11:27 -07:00
parent 62df218a8e
commit 907627ee9e
15 changed files with 15927 additions and 17508 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/boot/init/lean/compiler/ir.cpp
View file

@ -15,7 +15,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
uint8 l_lean_ir_alts_is__pure(obj*);
obj* l_rbnode_find___main___at_lean_name__map_contains___spec__2(obj*, obj*, obj*, obj*, obj*);
obj* l_rbnode_find___main___at_lean_name__map_contains___spec__2(obj*, obj*, obj*, obj*);
obj* l_list_foldl___main___at_lean_ir_insert__params___spec__1(obj*, obj*);
uint8 l_lean_ir_ctor__info_beq___main(obj*, obj*);
obj* l_lean_ir_expr_has__aeqv;
@ -837,7 +837,7 @@ _start:
{
obj* x_2; obj* x_3;
x_2 = lean::box(0);
x_3 = l_rbnode_find___main___at_lean_name__map_contains___spec__2(x_2, lean::box(0), lean::box(0), x_0, x_1);
x_3 = l_rbnode_find___main___at_lean_name__map_contains___spec__2(x_2, lean::box(0), x_0, x_1);
return x_3;
}
}

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

File diff suppressed because it is too large Load diff

5063
src/boot/init/lean/expander.cpp
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

2175
src/boot/init/lean/name.cpp
View file

File diff suppressed because it is too large Load diff

2184
src/boot/init/lean/parser/basic.cpp
View file

File diff suppressed because it is too large Load diff

184
src/boot/init/lean/parser/combinators.cpp
View file

@ -25,7 +25,6 @@ obj* l_lean_parser_combinators_node_tokens(obj*, obj*, obj*, obj*, obj*, obj*, o
obj* l_lean_parser_combinators_node_tokens___rarg(obj*);
obj* l_lean_parser_combinators_sep__by1___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_combinators_sep__by___boxed(obj*);
obj* l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_combinators_choice_tokens___rarg___boxed(obj*);
obj* l_lean_parser_combinators_node_view___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_error___at___private_init_lean_parser_combinators_2__sep__by__aux___main___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
@ -49,7 +48,7 @@ obj* l___private_init_lean_parser_combinators_3__sep__by_view__aux___main___rarg
obj* l_lean_parser_monad__parsec_error___at_lean_parser_combinators_longest__choice___spec__2___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_combinators_longest__match_tokens(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_combinators_coe_view___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_error___at_lean_parser_combinators_choice__aux___main___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_combinators_longest__choice_tokens(obj*, obj*, obj*, obj*, obj*, obj*);
namespace lean {
@ -82,7 +81,7 @@ obj* l_lean_parser_combinators_optional_tokens___rarg___boxed(obj*);
obj* l_list_reverse___rarg(obj*);
obj* l_lean_parser_monad__parsec_error___at_lean_parser_combinators_sep__by___spec__2(obj*, obj*);
obj* l_lean_parser_combinators_label_tokens___rarg___boxed(obj*);
obj* l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg___lambda__3(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg___lambda__3(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_error___at_lean_parser_combinators_sep__by1___spec__2___boxed(obj*, obj*);
obj* l_list_map___main___at_lean_parser_combinators_sep__by1_view___spec__1___boxed(obj*, obj*, obj*);
obj* l_lean_parser_combinators_node___boxed(obj*);
@ -126,7 +125,7 @@ obj* l_lean_parser_combinators_try_view___boxed(obj*, obj*, obj*, obj*);
obj* l___private_init_lean_parser_combinators_2__sep__by__aux___main___at_lean_parser_combinators_sep__by___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_combinators_many___boxed(obj*);
obj* l_lean_parser_combinators_longest__match_view(obj*);
obj* l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1___rarg(obj*, obj*, obj*, obj*, obj*);
obj* l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1___rarg(obj*, obj*, obj*);
obj* l_lean_parser_combinators_many1_tokens___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_error___at_lean_parser_combinators_longest__choice___spec__2___boxed(obj*, obj*);
obj* l_lean_parser_combinators_monad__lift_tokens___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
@ -411,70 +410,68 @@ x_10 = lean::apply_2(x_6, lean::box(0), x_9);
return x_10;
}
}
obj* l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg___lambda__3(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7) {
obj* l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg___lambda__3(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
_start:
{
obj* x_8;
x_8 = l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg(x_0, x_1, x_2, x_3, x_4, x_5, x_7, x_6);
return x_8;
obj* x_7;
x_7 = l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg(x_0, x_1, x_2, x_3, x_4, x_6, x_5);
return x_7;
}
}
obj* l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7) {
obj* l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
_start:
{
if (lean::obj_tag(x_7) == 0)
if (lean::obj_tag(x_6) == 0)
{
obj* x_13; obj* x_16; obj* x_19;
lean::dec(x_5);
obj* x_11; obj* x_14; obj* x_17;
lean::dec(x_4);
lean::dec(x_1);
lean::dec(x_3);
lean::dec(x_2);
x_13 = lean::cnstr_get(x_0, 0);
lean::inc(x_13);
x_11 = lean::cnstr_get(x_0, 0);
lean::inc(x_11);
lean::dec(x_0);
x_16 = lean::cnstr_get(x_13, 1);
lean::inc(x_16);
lean::dec(x_13);
x_19 = lean::apply_2(x_16, lean::box(0), x_6);
return x_19;
x_14 = lean::cnstr_get(x_11, 1);
lean::inc(x_14);
lean::dec(x_11);
x_17 = lean::apply_2(x_14, lean::box(0), x_5);
return x_17;
}
else
{
obj* x_20; obj* x_22; obj* x_25; obj* x_27; obj* x_32; obj* x_33; obj* x_35; obj* x_37; obj* x_38; obj* x_39;
x_20 = lean::cnstr_get(x_7, 0);
obj* x_18; obj* x_20; obj* x_23; obj* x_25; obj* x_30; obj* x_31; obj* x_33; obj* x_35; obj* x_36; obj* x_37;
x_18 = lean::cnstr_get(x_6, 0);
lean::inc(x_18);
x_20 = lean::cnstr_get(x_6, 1);
lean::inc(x_20);
x_22 = lean::cnstr_get(x_7, 1);
lean::inc(x_22);
lean::dec(x_7);
x_25 = lean::cnstr_get(x_0, 1);
lean::dec(x_6);
x_23 = lean::cnstr_get(x_0, 1);
lean::inc(x_23);
x_25 = lean::cnstr_get(x_1, 1);
lean::inc(x_25);
x_27 = lean::cnstr_get(x_1, 1);
lean::inc(x_27);
lean::inc(x_3);
lean::inc(x_1);
lean::inc(x_6);
x_32 = lean::alloc_closure(reinterpret_cast<void*>(l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg___lambda__1), 4, 3);
lean::closure_set(x_32, 0, x_6);
lean::closure_set(x_32, 1, x_1);
lean::closure_set(x_32, 2, x_3);
x_33 = lean::apply_3(x_27, lean::box(0), x_20, x_32);
lean::inc(x_2);
x_35 = lean::alloc_closure(reinterpret_cast<void*>(l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg___lambda__2), 3, 2);
lean::closure_set(x_35, 0, x_2);
lean::closure_set(x_35, 1, x_6);
lean::inc(x_5);
x_37 = lean::apply_4(x_5, lean::box(0), lean::box(0), x_33, x_35);
x_38 = lean::alloc_closure(reinterpret_cast<void*>(l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg___lambda__3), 8, 7);
lean::closure_set(x_38, 0, x_0);
lean::closure_set(x_38, 1, x_1);
lean::closure_set(x_38, 2, x_2);
lean::closure_set(x_38, 3, x_3);
lean::closure_set(x_38, 4, x_4);
lean::closure_set(x_38, 5, x_5);
lean::closure_set(x_38, 6, x_22);
x_39 = lean::apply_4(x_25, lean::box(0), lean::box(0), x_37, x_38);
return x_39;
x_30 = lean::alloc_closure(reinterpret_cast<void*>(l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg___lambda__1), 4, 3);
lean::closure_set(x_30, 0, x_5);
lean::closure_set(x_30, 1, x_1);
lean::closure_set(x_30, 2, x_3);
x_31 = lean::apply_3(x_25, lean::box(0), x_18, x_30);
lean::inc(x_2);
x_33 = lean::alloc_closure(reinterpret_cast<void*>(l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg___lambda__2), 3, 2);
lean::closure_set(x_33, 0, x_2);
lean::closure_set(x_33, 1, x_5);
lean::inc(x_4);
x_35 = lean::apply_4(x_4, lean::box(0), lean::box(0), x_31, x_33);
x_36 = lean::alloc_closure(reinterpret_cast<void*>(l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg___lambda__3), 7, 6);
lean::closure_set(x_36, 0, x_0);
lean::closure_set(x_36, 1, x_1);
lean::closure_set(x_36, 2, x_2);
lean::closure_set(x_36, 3, x_3);
lean::closure_set(x_36, 4, x_4);
lean::closure_set(x_36, 5, x_20);
x_37 = lean::apply_4(x_23, lean::box(0), lean::box(0), x_35, x_36);
return x_37;
}
}
}
@ -482,7 +479,7 @@ obj* l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1(obj* x_0)
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg), 8, 0);
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg), 7, 0);
return x_1;
}
}
@ -505,20 +502,19 @@ return x_11;
obj* l_lean_parser_combinators_node___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
_start:
{
obj* x_6; obj* x_8; obj* x_13; obj* x_14; obj* x_15;
obj* x_6; obj* x_8; obj* x_12; obj* x_13; obj* x_14;
x_6 = lean::cnstr_get(x_0, 1);
lean::inc(x_6);
x_8 = lean::box(0);
lean::inc(x_6);
lean::inc(x_6);
lean::inc(x_4);
lean::inc(x_3);
x_13 = l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg(x_0, x_1, x_3, x_4, x_6, x_6, x_8, x_5);
x_14 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_parser_combinators_node___rarg___lambda__1), 3, 2);
lean::closure_set(x_14, 0, x_3);
lean::closure_set(x_14, 1, x_4);
x_15 = lean::apply_4(x_6, lean::box(0), lean::box(0), x_13, x_14);
return x_15;
x_12 = l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1___rarg(x_0, x_1, x_3, x_4, x_6, x_8, x_5);
x_13 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_parser_combinators_node___rarg___lambda__1), 3, 2);
lean::closure_set(x_13, 0, x_3);
lean::closure_set(x_13, 1, x_4);
x_14 = lean::apply_4(x_6, lean::box(0), lean::box(0), x_12, x_13);
return x_14;
}
}
obj* l_lean_parser_combinators_node(obj* x_0) {
@ -4007,50 +4003,50 @@ lean::dec(x_5);
return x_6;
}
}
obj* l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
obj* l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1___rarg(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
if (lean::obj_tag(x_4) == 0)
if (lean::obj_tag(x_2) == 0)
{
obj* x_7;
obj* x_5;
lean::dec(x_1);
lean::dec(x_3);
x_7 = lean::box(0);
return x_7;
lean::dec(x_0);
x_5 = lean::box(0);
return x_5;
}
else
{
obj* x_8; obj* x_10; obj* x_12; obj* x_13; obj* x_15; obj* x_20; obj* x_21; obj* x_22; obj* x_23;
x_8 = lean::cnstr_get(x_4, 0);
x_10 = lean::cnstr_get(x_4, 1);
if (lean::is_exclusive(x_4)) {
x_12 = x_4;
obj* x_6; obj* x_8; obj* x_10; obj* x_11; obj* x_13; obj* x_18; obj* x_19; obj* x_20; obj* x_21;
x_6 = lean::cnstr_get(x_2, 0);
x_8 = lean::cnstr_get(x_2, 1);
if (lean::is_exclusive(x_2)) {
x_10 = x_2;
} else {
lean::inc(x_6);
lean::inc(x_8);
lean::inc(x_10);
lean::dec(x_4);
x_12 = lean::box(0);
lean::dec(x_2);
x_10 = lean::box(0);
}
x_13 = lean::cnstr_get(x_8, 0);
x_11 = lean::cnstr_get(x_6, 0);
lean::inc(x_11);
x_13 = lean::cnstr_get(x_6, 1);
lean::inc(x_13);
x_15 = lean::cnstr_get(x_8, 1);
lean::inc(x_15);
lean::dec(x_8);
lean::inc(x_3);
lean::dec(x_6);
lean::inc(x_1);
x_20 = l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1___rarg(x_0, x_1, x_2, x_3, x_10);
x_21 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_parser_combinators_choice__aux___main___rarg___lambda__1), 3, 2);
lean::closure_set(x_21, 0, x_1);
lean::closure_set(x_21, 1, x_13);
x_22 = lean::apply_4(x_3, lean::box(0), lean::box(0), x_15, x_21);
if (lean::is_scalar(x_12)) {
x_23 = lean::alloc_cnstr(1, 2, 0);
lean::inc(x_0);
x_18 = l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1___rarg(x_0, x_1, x_8);
x_19 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_parser_combinators_choice__aux___main___rarg___lambda__1), 3, 2);
lean::closure_set(x_19, 0, x_0);
lean::closure_set(x_19, 1, x_11);
x_20 = lean::apply_4(x_1, lean::box(0), lean::box(0), x_13, x_19);
if (lean::is_scalar(x_10)) {
x_21 = lean::alloc_cnstr(1, 2, 0);
} else {
x_23 = x_12;
x_21 = x_10;
}
lean::cnstr_set(x_23, 0, x_22);
lean::cnstr_set(x_23, 1, x_20);
return x_23;
lean::cnstr_set(x_21, 0, x_20);
lean::cnstr_set(x_21, 1, x_18);
return x_21;
}
}
}
@ -4058,7 +4054,7 @@ obj* l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1(ob
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1___rarg___boxed), 5, 0);
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1___rarg), 3, 0);
return x_1;
}
}
@ -4127,7 +4123,7 @@ x_7 = lean::mk_nat_obj(0u);
x_8 = l_list_enum__from___main___rarg(x_7, x_4);
lean::inc(x_5);
lean::inc(x_3);
x_11 = l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1___rarg(x_0, x_3, x_5, x_5, x_8);
x_11 = l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1___rarg(x_3, x_5, x_8);
lean::inc(x_2);
lean::inc(x_0);
x_14 = l_lean_parser_monad__parsec_longest__match___rarg(x_0, x_2, lean::box(0), x_1, x_11);
@ -4147,16 +4143,6 @@ x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_parser_combinators_long
return x_1;
}
}
obj* l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
_start:
{
obj* x_5;
x_5 = l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1___rarg(x_0, x_1, x_2, x_3, x_4);
lean::dec(x_0);
lean::dec(x_2);
return x_5;
}
}
obj* l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1___boxed(obj* x_0) {
_start:
{

64
src/boot/init/lean/parser/command.cpp
View file

@ -20,7 +20,7 @@ obj* l_lean_parser_command_section_has__view_x_27___lambda__2(obj*);
obj* l_lean_parser_command_variables_parser___closed__1;
obj* l_lean_parser_command_variables_has__view_x_27___lambda__1___closed__1;
obj* l_lean_parser_command_check_parser_lean_parser_has__tokens;
obj* l_rbnode_find___main___at_lean_name__map_contains___spec__2(obj*, obj*, obj*, obj*, obj*);
obj* l_rbnode_find___main___at_lean_name__map_contains___spec__2(obj*, obj*, obj*, obj*);
obj* l_lean_parser_command_check_parser(obj*, obj*, obj*, obj*);
extern obj* l_lean_parser_command_reserve__mixfix_parser_lean_parser_has__tokens;
obj* l_list_map___main___at_lean_parser_command_omit_has__view_x_27___spec__2(obj*);
@ -115,7 +115,6 @@ obj* l_lean_parser_monad__parsec_error___at_lean_parser_command__parser_run___sp
extern obj* l_lean_parser_command__parser__m_monad___closed__1;
obj* l_lean_parser_command_open__spec_hiding_has__view_x_27___lambda__1(obj*);
obj* l_lean_parser_combinators_many1___at_lean_parser_command_attr__instance_parser_lean_parser_has__tokens___spec__3(obj*, obj*, obj*, obj*, obj*);
obj* l_list_foldl___main___at_lean_parser_command_universe_parser___spec__3___boxed(obj*);
obj* l_list_map___main___at_lean_parser_command_omit_has__view_x_27___spec__1(obj*);
obj* l_lean_parser_command_parser_lean_parser_has__view;
obj* l_lean_parser_command_option__value_has__view_x_27___lambda__1___closed__2;
@ -310,7 +309,6 @@ obj* l_lean_parser_command_include_has__view_x_27;
obj* l_lean_parser_command_section_parser_lean_parser_has__tokens;
obj* l_lean_parser_command_open__spec_hiding_has__view_x_27;
obj* l_lean_parser_command_attribute_parser_lean_parser_has__tokens;
obj* l_list_foldl___main___at_lean_parser_command_universe_parser___spec__3___rarg(obj*, obj*);
obj* l_lean_parser_command_open__spec_parser___closed__1;
obj* l_lean_parser_command_open__spec_renaming_has__view_x_27___lambda__1___closed__2;
obj* l_lean_parser_combinators_many___at_lean_parser_command_attr__instance_parser_lean_parser_has__tokens___spec__2(obj*, obj*, obj*, obj*, obj*);
@ -377,7 +375,7 @@ extern obj* l_lean_parser_combinators_any__of___rarg___closed__1;
extern obj* l_lean_parser_raw_view___rarg___lambda__2___closed__1;
obj* l_lean_parser_command_section_has__view_x_27___lambda__1(obj*);
obj* l_lean_parser_command_open_has__view_x_27___lambda__2(obj*);
obj* l_list_foldl___main___at_lean_parser_command_universe_parser___spec__3(obj*);
obj* l_list_foldl___main___at_lean_parser_command_universe_parser___spec__3(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_rbmap_find___main___at_lean_parser_command__parser_run___spec__6(obj*);
obj* l_rbmap_find___main___at_lean_parser_command__parser_run___spec__6___boxed(obj*);
obj* l_list_map___main___at_lean_parser_command_include_has__view_x_27___spec__1(obj*);
@ -11271,38 +11269,32 @@ x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_reader__t_orelse___at_lean_p
return x_1;
}
}
obj* l_list_foldl___main___at_lean_parser_command_universe_parser___spec__3___rarg(obj* x_0, obj* x_1) {
obj* l_list_foldl___main___at_lean_parser_command_universe_parser___spec__3(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
_start:
{
if (lean::obj_tag(x_1) == 0)
{
return x_0;
obj* x_6;
x_6 = lean::apply_4(x_0, x_2, x_3, x_4, x_5);
return x_6;
}
else
{
obj* x_2; obj* x_4; obj* x_7;
x_2 = lean::cnstr_get(x_1, 0);
lean::inc(x_2);
x_4 = lean::cnstr_get(x_1, 1);
lean::inc(x_4);
obj* x_7; obj* x_9; obj* x_12;
x_7 = lean::cnstr_get(x_1, 0);
lean::inc(x_7);
x_9 = lean::cnstr_get(x_1, 1);
lean::inc(x_9);
lean::dec(x_1);
x_7 = lean::alloc_closure(reinterpret_cast<void*>(l_reader__t_orelse___at_lean_parser_command_universe_parser___spec__2___rarg), 6, 2);
lean::closure_set(x_7, 0, x_0);
lean::closure_set(x_7, 1, x_2);
x_0 = x_7;
x_1 = x_4;
x_12 = lean::alloc_closure(reinterpret_cast<void*>(l_reader__t_orelse___at_lean_parser_command_universe_parser___spec__2___rarg), 6, 2);
lean::closure_set(x_12, 0, x_0);
lean::closure_set(x_12, 1, x_7);
x_0 = x_12;
x_1 = x_9;
goto _start;
}
}
}
obj* l_list_foldl___main___at_lean_parser_command_universe_parser___spec__3(obj* x_0) {
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_list_foldl___main___at_lean_parser_command_universe_parser___spec__3___rarg), 2, 0);
return x_1;
}
}
obj* l_lean_parser_combinators_any__of___at_lean_parser_command_universe_parser___spec__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
_start:
{
@ -11320,15 +11312,14 @@ return x_8;
}
else
{
obj* x_12; obj* x_14; obj* x_17; obj* x_18;
obj* x_12; obj* x_14; obj* x_17;
x_12 = lean::cnstr_get(x_0, 0);
lean::inc(x_12);
x_14 = lean::cnstr_get(x_0, 1);
lean::inc(x_14);
lean::dec(x_0);
x_17 = l_list_foldl___main___at_lean_parser_command_universe_parser___spec__3___rarg(x_12, x_14);
x_18 = lean::apply_4(x_17, x_1, x_2, x_3, x_4);
return x_18;
x_17 = l_list_foldl___main___at_lean_parser_command_universe_parser___spec__3(x_12, x_14, x_1, x_2, x_3, x_4);
return x_17;
}
}
}
@ -11409,15 +11400,6 @@ lean::dec(x_0);
return x_1;
}
}
obj* l_list_foldl___main___at_lean_parser_command_universe_parser___spec__3___boxed(obj* x_0) {
_start:
{
obj* x_1;
x_1 = l_list_foldl___main___at_lean_parser_command_universe_parser___spec__3(x_0);
lean::dec(x_0);
return x_1;
}
}
obj* _init_l_lean_parser_command_check() {
_start:
{
@ -16258,7 +16240,7 @@ _start:
{
obj* x_2; obj* x_3;
x_2 = lean::box(0);
x_3 = l_rbnode_find___main___at_lean_name__map_contains___spec__2(x_2, lean::box(0), lean::box(0), x_0, x_1);
x_3 = l_rbnode_find___main___at_lean_name__map_contains___spec__2(x_2, lean::box(0), x_0, x_1);
return x_3;
}
}
@ -16275,7 +16257,7 @@ _start:
{
obj* x_2; obj* x_3;
x_2 = lean::box(0);
x_3 = l_rbnode_find___main___at_lean_name__map_contains___spec__2(x_2, lean::box(0), lean::box(0), x_0, x_1);
x_3 = l_rbnode_find___main___at_lean_name__map_contains___spec__2(x_2, lean::box(0), x_0, x_1);
return x_3;
}
}
@ -16292,7 +16274,7 @@ _start:
{
obj* x_2; obj* x_3;
x_2 = lean::box(0);
x_3 = l_rbnode_find___main___at_lean_name__map_contains___spec__2(x_2, lean::box(0), lean::box(0), x_0, x_1);
x_3 = l_rbnode_find___main___at_lean_name__map_contains___spec__2(x_2, lean::box(0), x_0, x_1);
return x_3;
}
}
@ -16309,7 +16291,7 @@ _start:
{
obj* x_2; obj* x_3;
x_2 = lean::box(0);
x_3 = l_rbnode_find___main___at_lean_name__map_contains___spec__2(x_2, lean::box(0), lean::box(0), x_0, x_1);
x_3 = l_rbnode_find___main___at_lean_name__map_contains___spec__2(x_2, lean::box(0), x_0, x_1);
return x_3;
}
}

7204
src/boot/init/lean/parser/declaration.cpp
View file

File diff suppressed because it is too large Load diff

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

@ -197,7 +197,7 @@ obj* l_lean_parser_monad__parsec_curr(obj*, obj*);
obj* l_lean_parser_parsec__t_labels__mk__res___rarg(obj*, obj*);
obj* l_lean_parser_parsec__t_lookahead___rarg___lambda__1(obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_take__while___at_lean_parser_monad__parsec_take__until___spec__1(obj*, obj*, obj*);
obj* l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_cond___boxed(obj*, obj*);
obj* l_lean_parser_parsec_result_mk__eps(obj*, obj*);
obj* l_lean_parser_monad__parsec_fix__aux___main___boxed(obj*, obj*);
@ -458,7 +458,7 @@ obj* l_lean_parser_monad__parsec_take__until___rarg___boxed(obj*, obj*, obj*);
obj* l_lean_parser_parsec__t_bind(obj*);
obj* l_lean_parser_monad__parsec_take__until1___boxed(obj*, obj*);
obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_any___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_unexpected___rarg___boxed(obj*, obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_eoi___at_lean_parser_parsec__t_parse__with__eoi___spec__1___boxed(obj*, obj*);
obj* l_lean_parser_monad__parsec_foldr___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*);
@ -620,7 +620,7 @@ obj* l___private_init_lean_parser_parsec_6__take__while__aux_x_27___main___rarg(
obj* l_lean_parser_monad__parsec_cond___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_take__while1_x_27___spec__2___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_lower___spec__2___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_longest__match___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_longest__match___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_sep__by1___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_ch___spec__1(obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_fix(obj*, obj*);
@ -784,7 +784,6 @@ obj* l_char_quote__core(uint32);
obj* l_lean_parser_monad__parsec_fix__aux___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_parsec__t_parse__with__left__over___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec__trans___boxed(obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_longest__match___rarg___lambda__2___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_parser_monad__parsec_many_x_27___rarg(obj*, obj*, obj*, obj*, obj*);
namespace lean {
uint8 nat_dec_lt(obj*, obj*);
@ -11030,57 +11029,57 @@ x_0 = lean::mk_string("longest_match: empty list");
return x_0;
}
}
obj* l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8, obj* x_9, obj* x_10) {
obj* l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7) {
_start:
{
if (lean::obj_tag(x_10) == 0)
if (lean::obj_tag(x_7) == 0)
{
obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_20; obj* x_23; obj* x_26;
obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_17; obj* x_20; obj* x_23;
lean::dec(x_5);
lean::dec(x_8);
lean::dec(x_4);
lean::dec(x_1);
lean::dec(x_3);
x_15 = lean::box(0);
x_16 = l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg___closed__1;
x_17 = l_mjoin___rarg___closed__1;
x_18 = l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_longest__match___spec__1___rarg(x_16, x_17, x_15, x_15, x_9);
lean::dec(x_9);
x_20 = lean::cnstr_get(x_0, 0);
lean::inc(x_20);
x_12 = lean::box(0);
x_13 = l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg___closed__1;
x_14 = l_mjoin___rarg___closed__1;
x_15 = l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_longest__match___spec__1___rarg(x_13, x_14, x_12, x_12, x_6);
lean::dec(x_6);
x_17 = lean::cnstr_get(x_0, 0);
lean::inc(x_17);
lean::dec(x_0);
x_23 = lean::cnstr_get(x_20, 1);
lean::inc(x_23);
lean::dec(x_20);
x_26 = lean::apply_2(x_23, lean::box(0), x_18);
return x_26;
x_20 = lean::cnstr_get(x_17, 1);
lean::inc(x_20);
lean::dec(x_17);
x_23 = lean::apply_2(x_20, lean::box(0), x_15);
return x_23;
}
else
{
obj* x_27; obj* x_29; obj* x_32; obj* x_40; obj* x_41; obj* x_42;
x_27 = lean::cnstr_get(x_10, 0);
lean::inc(x_27);
x_29 = lean::cnstr_get(x_10, 1);
obj* x_24; obj* x_26; obj* x_29; obj* x_37; obj* x_38; obj* x_39;
x_24 = lean::cnstr_get(x_7, 0);
lean::inc(x_24);
x_26 = lean::cnstr_get(x_7, 1);
lean::inc(x_26);
lean::dec(x_7);
x_29 = lean::cnstr_get(x_0, 1);
lean::inc(x_29);
lean::dec(x_10);
x_32 = lean::cnstr_get(x_0, 1);
lean::inc(x_32);
lean::inc(x_9);
lean::inc(x_8);
lean::inc(x_6);
lean::inc(x_5);
lean::inc(x_4);
lean::inc(x_3);
lean::inc(x_1);
lean::inc(x_0);
x_40 = l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg(x_0, x_1, lean::box(0), x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_29);
x_41 = lean::alloc_closure(reinterpret_cast<void*>(l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg___lambda__4), 8, 7);
lean::closure_set(x_41, 0, x_3);
lean::closure_set(x_41, 1, x_0);
lean::closure_set(x_41, 2, x_5);
lean::closure_set(x_41, 3, x_8);
lean::closure_set(x_41, 4, x_27);
lean::closure_set(x_41, 5, x_9);
lean::closure_set(x_41, 6, x_1);
x_42 = lean::apply_4(x_32, lean::box(0), lean::box(0), x_40, x_41);
return x_42;
x_37 = l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg(x_0, x_1, lean::box(0), x_3, x_4, x_5, x_6, x_26);
x_38 = lean::alloc_closure(reinterpret_cast<void*>(l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg___lambda__4), 8, 7);
lean::closure_set(x_38, 0, x_3);
lean::closure_set(x_38, 1, x_0);
lean::closure_set(x_38, 2, x_4);
lean::closure_set(x_38, 3, x_5);
lean::closure_set(x_38, 4, x_24);
lean::closure_set(x_38, 5, x_6);
lean::closure_set(x_38, 6, x_1);
x_39 = lean::apply_4(x_29, lean::box(0), lean::box(0), x_37, x_38);
return x_39;
}
}
}
@ -11088,7 +11087,7 @@ obj* l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__
_start:
{
obj* x_2;
x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg___boxed), 11, 0);
x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg___boxed), 8, 0);
return x_2;
}
}
@ -11102,16 +11101,16 @@ x_3 = lean::apply_2(x_0, lean::box(0), x_2);
return x_3;
}
}
obj* l_lean_parser_monad__parsec_longest__match___rarg___lambda__2(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8) {
obj* l_lean_parser_monad__parsec_longest__match___rarg___lambda__2(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7) {
_start:
{
obj* x_10; obj* x_11; obj* x_12;
obj* x_9; obj* x_10; obj* x_11;
lean::inc(x_3);
x_10 = l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg(x_0, x_1, lean::box(0), x_2, x_3, x_3, x_4, x_5, x_6, x_8, x_7);
x_11 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_parser_monad__parsec_longest__match___rarg___lambda__1), 2, 1);
lean::closure_set(x_11, 0, x_4);
x_12 = lean::apply_4(x_3, lean::box(0), lean::box(0), x_10, x_11);
return x_12;
x_9 = l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg(x_0, x_1, lean::box(0), x_2, x_3, x_4, x_7, x_5);
x_10 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_parser_monad__parsec_longest__match___rarg___lambda__1), 2, 1);
lean::closure_set(x_10, 0, x_6);
x_11 = lean::apply_4(x_3, lean::box(0), lean::box(0), x_9, x_10);
return x_11;
}
}
obj* l_lean_parser_monad__parsec_longest__match___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
@ -11127,15 +11126,14 @@ lean::inc(x_7);
x_11 = lean::apply_2(x_7, lean::box(0), x_9);
lean::inc(x_11);
lean::inc(x_5);
x_14 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_parser_monad__parsec_longest__match___rarg___lambda__2___boxed), 9, 8);
x_14 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_parser_monad__parsec_longest__match___rarg___lambda__2), 8, 7);
lean::closure_set(x_14, 0, x_0);
lean::closure_set(x_14, 1, x_1);
lean::closure_set(x_14, 2, x_3);
lean::closure_set(x_14, 3, x_5);
lean::closure_set(x_14, 4, x_7);
lean::closure_set(x_14, 5, x_9);
lean::closure_set(x_14, 6, x_11);
lean::closure_set(x_14, 7, x_4);
lean::closure_set(x_14, 4, x_11);
lean::closure_set(x_14, 5, x_4);
lean::closure_set(x_14, 6, x_7);
x_15 = lean::apply_4(x_5, lean::box(0), lean::box(0), x_11, x_14);
return x_15;
}
@ -11177,16 +11175,13 @@ lean::dec(x_2);
return x_4;
}
}
obj* l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8, obj* x_9, obj* x_10) {
obj* l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7) {
_start:
{
obj* x_11;
x_11 = l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
obj* x_8;
x_8 = l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___rarg(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean::dec(x_2);
lean::dec(x_4);
lean::dec(x_6);
lean::dec(x_7);
return x_11;
return x_8;
}
}
obj* l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__2___boxed(obj* x_0, obj* x_1) {
@ -11199,15 +11194,6 @@ lean::dec(x_1);
return x_2;
}
}
obj* l_lean_parser_monad__parsec_longest__match___rarg___lambda__2___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8) {
_start:
{
obj* x_9;
x_9 = l_lean_parser_monad__parsec_longest__match___rarg___lambda__2(x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean::dec(x_5);
return x_9;
}
}
obj* l_lean_parser_monad__parsec_longest__match___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
_start:
{

914
src/boot/init/lean/parser/term.cpp
View file

File diff suppressed because it is too large Load diff

2750
src/boot/init/lean/parser/token.cpp
View file

File diff suppressed because it is too large Load diff

42
src/boot/init/lean/parser/trie.cpp
View file

@ -19,7 +19,7 @@ obj* l_rbnode_find___main___at___private_init_lean_parser_trie_1__insert__aux___
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4___rarg___boxed(obj*, obj*, obj*);
obj* l_lean_parser_trie_has__to__string(obj*);
obj* l_lean_format_join__sep___main___at___private_init_lean_parser_trie_4__to__string__aux___main___spec__1(obj*, obj*);
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4(obj*, obj*);
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4(obj*);
obj* l___private_init_lean_parser_trie_1__insert__aux___main(obj*);
obj* l_lean_parser_trie_match__prefix___rarg(obj*, obj*);
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__3___rarg___boxed(obj*, obj*, obj*);
@ -77,7 +77,7 @@ obj* l_lean_format_pretty(obj*, obj*);
obj* l___private_init_lean_parser_trie_4__to__string__aux___boxed(obj*);
obj* l_rbnode_insert___at___private_init_lean_parser_trie_1__insert__aux___main___spec__2___rarg(obj*, uint32, obj*);
obj* l_rbnode_find___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__1(obj*);
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4___boxed(obj*, obj*);
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4___boxed(obj*);
obj* l_string_mk__iterator(obj*);
obj* l_rbnode_balance1___main___rarg(obj*, obj*);
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4___rarg(obj*, uint32, obj*);
@ -85,7 +85,7 @@ obj* l___private_init_lean_parser_trie_1__insert__aux___main___boxed(obj*);
uint32 l_string_iterator_curr___main(obj*);
obj* l___private_init_lean_parser_trie_2__find__aux___boxed(obj*);
obj* l_lean_parser_trie_mk___boxed(obj*);
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__3___boxed(obj*, obj*);
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__3___boxed(obj*);
obj* l_lean_to__fmt___at___private_init_lean_parser_trie_4__to__string__aux___main___spec__2(obj*);
obj* l___private_init_lean_parser_trie_3__match__prefix__aux___main___boxed(obj*);
namespace lean {
@ -96,7 +96,7 @@ obj* l___private_init_lean_parser_trie_3__match__prefix__aux___main(obj*);
uint8 l_rbnode_is__red___main___rarg(obj*);
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__3___rarg(obj*, uint32, obj*);
obj* l_rbnode_fold___main___at___private_init_lean_parser_trie_4__to__string__aux___main___spec__3___rarg___boxed(obj*, obj*);
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__3(obj*, obj*);
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__3(obj*);
obj* l_string_iterator_next___main(obj*);
obj* l_rbnode_insert___at___private_init_lean_parser_trie_1__insert__aux___main___spec__2___boxed(obj*);
obj* l_rbnode_fold___main___at___private_init_lean_parser_trie_4__to__string__aux___main___spec__3___rarg(obj*, obj*);
@ -431,12 +431,12 @@ return x_63;
}
}
}
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__3(obj* x_0, obj* x_1) {
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__3(obj* x_0) {
_start:
{
obj* x_2;
x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__3___rarg___boxed), 3, 0);
return x_2;
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__3___rarg___boxed), 3, 0);
return x_1;
}
}
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4___rarg(obj* x_0, uint32 x_1, obj* x_2) {
@ -673,12 +673,12 @@ return x_63;
}
}
}
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4(obj* x_0, obj* x_1) {
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4(obj* x_0) {
_start:
{
obj* x_2;
x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4___rarg___boxed), 3, 0);
return x_2;
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4___rarg___boxed), 3, 0);
return x_1;
}
}
obj* l_rbnode_insert___at___private_init_lean_parser_trie_1__insert__aux___main___spec__2___rarg(obj* x_0, uint32 x_1, obj* x_2) {
@ -810,14 +810,13 @@ x_4 = l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___
return x_4;
}
}
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__3___boxed(obj* x_0, obj* x_1) {
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__3___boxed(obj* x_0) {
_start:
{
obj* x_2;
x_2 = l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__3(x_0, x_1);
obj* x_1;
x_1 = l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__3(x_0);
lean::dec(x_0);
lean::dec(x_1);
return x_2;
return x_1;
}
}
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4___rarg___boxed(obj* x_0, obj* x_1, obj* x_2) {
@ -829,14 +828,13 @@ x_4 = l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___
return x_4;
}
}
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4___boxed(obj* x_0, obj* x_1) {
obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4___boxed(obj* x_0) {
_start:
{
obj* x_2;
x_2 = l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4(x_0, x_1);
obj* x_1;
x_1 = l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__4(x_0);
lean::dec(x_0);
lean::dec(x_1);
return x_2;
return x_1;
}
}
obj* l_rbnode_insert___at___private_init_lean_parser_trie_1__insert__aux___main___spec__2___rarg___boxed(obj* x_0, obj* x_1, obj* x_2) {

371
src/boot/init/lean/position.cpp
View file

@ -16,7 +16,6 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
#endif
obj* l___private_init_lean_position_1__from__string__aux(obj*, obj*, obj*);
uint8 l_prod__has__decidable__lt___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_rbnode_ins___main___at_lean_file__map_from__string___spec__4___boxed(obj*);
namespace lean {
obj* nat_add(obj*, obj*);
}
@ -24,37 +23,28 @@ obj* l_lean_position_lean_has__to__format___closed__1;
obj* l_rbmap_of__list___main___at_lean_file__map_from__string___spec__1(obj*);
obj* l___private_init_lean_position_1__from__string__aux___main(obj*, obj*, obj*);
obj* l_lean_position_lean_has__to__format(obj*);
obj* l_rbmap_insert___main___at_lean_file__map_from__string___spec__2___boxed(obj*);
namespace lean {
obj* string_length(obj*);
}
obj* l_lean_position_has__lt;
obj* l_lean_position_decidable__lt___boxed(obj*, obj*);
obj* l_rbnode_ins___main___at_lean_file__map_from__string___spec__5(obj*);
obj* l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2___boxed(obj*);
obj* l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2___boxed(obj*, obj*, obj*);
obj* l_lean_position_lean_has__to__format___closed__2;
obj* l_rbnode_insert___at_lean_file__map_from__string___spec__3___boxed(obj*);
uint8 l_lean_position_decidable__lt(obj*, obj*);
obj* l_lean_position_decidable__lt___main___boxed(obj*, obj*);
obj* l_rbmap_insert___main___at_lean_file__map_from__string___spec__2(obj*);
obj* l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2___rarg(obj*, obj*, obj*);
obj* l_rbmap_insert___main___at_lean_file__map_from__string___spec__2(obj*, obj*, obj*);
namespace lean {
uint8 nat_dec_eq(obj*, obj*);
}
obj* l_lean_position_decidable__lt___main___closed__2;
obj* l_nat_dec__eq___boxed(obj*, obj*);
obj* l_rbnode_balance2___main___rarg(obj*, obj*);
obj* l_rbmap_insert___main___at_lean_file__map_from__string___spec__2___rarg(obj*, obj*, obj*);
obj* l_rbnode_ins___main___at_lean_file__map_from__string___spec__5___boxed(obj*);
obj* l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2___rarg___boxed(obj*, obj*, obj*);
obj* l_lean_file__map_from__string(obj*);
obj* l_rbnode_ins___main___at_lean_file__map_from__string___spec__4___rarg(obj*, obj*, obj*);
obj* l_lean_to__fmt___at_lean_position_lean_has__to__format___spec__1(obj*);
obj* l_rbnode_ins___main___at_lean_file__map_from__string___spec__4(obj*);
obj* l_rbnode_insert___at_lean_file__map_from__string___spec__3___rarg(obj*, obj*, obj*);
obj* l_rbnode_ins___main___at_lean_file__map_from__string___spec__4(obj*, obj*, obj*);
obj* l_lean_position_lean_has__to__format___closed__3;
obj* l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2(obj*);
obj* l_rbnode_insert___at_lean_file__map_from__string___spec__3(obj*);
obj* l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2(obj*, obj*, obj*);
obj* l_rbnode_insert___at_lean_file__map_from__string___spec__3(obj*, obj*, obj*);
obj* l_string_mk__iterator(obj*);
obj* l_rbnode_balance1___main___rarg(obj*, obj*);
uint32 l_string_iterator_curr___main(obj*);
@ -66,7 +56,6 @@ namespace lean {
uint32 uint32_of_nat(obj*);
}
uint8 l_lean_position_decidable__lt___main(obj*, obj*);
obj* l_rbnode_ins___main___at_lean_file__map_from__string___spec__5___rarg(obj*, obj*, obj*);
namespace lean {
obj* nat_sub(obj*, obj*);
}
@ -386,7 +375,7 @@ lean::dec(x_2);
return x_3;
}
}
obj* l_rbnode_ins___main___at_lean_file__map_from__string___spec__4___rarg(obj* x_0, obj* x_1, obj* x_2) {
obj* l_rbnode_ins___main___at_lean_file__map_from__string___spec__4(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
if (lean::obj_tag(x_0) == 0)
@ -453,7 +442,7 @@ return x_21;
else
{
obj* x_22; obj* x_23; obj* x_24;
x_22 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4___rarg(x_13, x_1, x_2);
x_22 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4(x_13, x_1, x_2);
if (lean::is_scalar(x_15)) {
x_23 = lean::alloc_cnstr(1, 4, 1);
} else {
@ -471,7 +460,7 @@ return x_24;
else
{
obj* x_25; obj* x_26; obj* x_27;
x_25 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4___rarg(x_7, x_1, x_2);
x_25 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4(x_7, x_1, x_2);
if (lean::is_scalar(x_15)) {
x_26 = lean::alloc_cnstr(1, 4, 1);
} else {
@ -537,7 +526,7 @@ x_43 = l_rbnode_is__red___main___rarg(x_34);
if (x_43 == 0)
{
obj* x_44; obj* x_45; obj* x_46;
x_44 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4___rarg(x_34, x_1, x_2);
x_44 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4(x_34, x_1, x_2);
if (lean::is_scalar(x_36)) {
x_45 = lean::alloc_cnstr(1, 4, 1);
} else {
@ -566,7 +555,7 @@ lean::cnstr_set(x_48, 2, x_32);
lean::cnstr_set(x_48, 3, x_47);
lean::cnstr_set_scalar(x_48, sizeof(void*)*4, x_6);
x_49 = x_48;
x_50 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4___rarg(x_34, x_1, x_2);
x_50 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4(x_34, x_1, x_2);
x_51 = l_rbnode_balance2___main___rarg(x_49, x_50);
return x_51;
}
@ -579,7 +568,7 @@ x_52 = l_rbnode_is__red___main___rarg(x_28);
if (x_52 == 0)
{
obj* x_53; obj* x_54; obj* x_55;
x_53 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4___rarg(x_28, x_1, x_2);
x_53 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4(x_28, x_1, x_2);
if (lean::is_scalar(x_36)) {
x_54 = lean::alloc_cnstr(1, 4, 1);
} else {
@ -608,7 +597,7 @@ lean::cnstr_set(x_57, 2, x_32);
lean::cnstr_set(x_57, 3, x_34);
lean::cnstr_set_scalar(x_57, sizeof(void*)*4, x_6);
x_58 = x_57;
x_59 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4___rarg(x_28, x_1, x_2);
x_59 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4(x_28, x_1, x_2);
x_60 = l_rbnode_balance1___main___rarg(x_58, x_59);
return x_60;
}
@ -617,254 +606,7 @@ return x_60;
}
}
}
obj* l_rbnode_ins___main___at_lean_file__map_from__string___spec__4(obj* x_0) {
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_rbnode_ins___main___at_lean_file__map_from__string___spec__4___rarg), 3, 0);
return x_1;
}
}
obj* l_rbnode_ins___main___at_lean_file__map_from__string___spec__5___rarg(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
if (lean::obj_tag(x_0) == 0)
{
uint8 x_3; obj* x_4; obj* x_5;
x_3 = 0;
x_4 = lean::alloc_cnstr(1, 4, 1);
lean::cnstr_set(x_4, 0, x_0);
lean::cnstr_set(x_4, 1, x_1);
lean::cnstr_set(x_4, 2, x_2);
lean::cnstr_set(x_4, 3, x_0);
lean::cnstr_set_scalar(x_4, sizeof(void*)*4, x_3);
x_5 = x_4;
return x_5;
}
else
{
uint8 x_6;
x_6 = lean::cnstr_get_scalar<uint8>(x_0, sizeof(void*)*4);
if (x_6 == 0)
{
obj* x_7; obj* x_9; obj* x_11; obj* x_13; obj* x_15; uint8 x_16;
x_7 = lean::cnstr_get(x_0, 0);
x_9 = lean::cnstr_get(x_0, 1);
x_11 = lean::cnstr_get(x_0, 2);
x_13 = lean::cnstr_get(x_0, 3);
if (lean::is_exclusive(x_0)) {
lean::cnstr_set(x_0, 0, lean::box(0));
lean::cnstr_set(x_0, 1, lean::box(0));
lean::cnstr_set(x_0, 2, lean::box(0));
lean::cnstr_set(x_0, 3, lean::box(0));
x_15 = x_0;
} else {
lean::inc(x_7);
lean::inc(x_9);
lean::inc(x_11);
lean::inc(x_13);
lean::dec(x_0);
x_15 = lean::box(0);
}
x_16 = lean::nat_dec_lt(x_1, x_9);
if (x_16 == 0)
{
uint8 x_17;
x_17 = lean::nat_dec_lt(x_9, x_1);
if (x_17 == 0)
{
obj* x_20; obj* x_21;
lean::dec(x_9);
lean::dec(x_11);
if (lean::is_scalar(x_15)) {
x_20 = lean::alloc_cnstr(1, 4, 1);
} else {
x_20 = x_15;
}
lean::cnstr_set(x_20, 0, x_7);
lean::cnstr_set(x_20, 1, x_1);
lean::cnstr_set(x_20, 2, x_2);
lean::cnstr_set(x_20, 3, x_13);
lean::cnstr_set_scalar(x_20, sizeof(void*)*4, x_6);
x_21 = x_20;
return x_21;
}
else
{
obj* x_22; obj* x_23; obj* x_24;
x_22 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__5___rarg(x_13, x_1, x_2);
if (lean::is_scalar(x_15)) {
x_23 = lean::alloc_cnstr(1, 4, 1);
} else {
x_23 = x_15;
}
lean::cnstr_set(x_23, 0, x_7);
lean::cnstr_set(x_23, 1, x_9);
lean::cnstr_set(x_23, 2, x_11);
lean::cnstr_set(x_23, 3, x_22);
lean::cnstr_set_scalar(x_23, sizeof(void*)*4, x_6);
x_24 = x_23;
return x_24;
}
}
else
{
obj* x_25; obj* x_26; obj* x_27;
x_25 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__5___rarg(x_7, x_1, x_2);
if (lean::is_scalar(x_15)) {
x_26 = lean::alloc_cnstr(1, 4, 1);
} else {
x_26 = x_15;
}
lean::cnstr_set(x_26, 0, x_25);
lean::cnstr_set(x_26, 1, x_9);
lean::cnstr_set(x_26, 2, x_11);
lean::cnstr_set(x_26, 3, x_13);
lean::cnstr_set_scalar(x_26, sizeof(void*)*4, x_6);
x_27 = x_26;
return x_27;
}
}
else
{
obj* x_28; obj* x_30; obj* x_32; obj* x_34; obj* x_36; uint8 x_37;
x_28 = lean::cnstr_get(x_0, 0);
x_30 = lean::cnstr_get(x_0, 1);
x_32 = lean::cnstr_get(x_0, 2);
x_34 = lean::cnstr_get(x_0, 3);
if (lean::is_exclusive(x_0)) {
lean::cnstr_set(x_0, 0, lean::box(0));
lean::cnstr_set(x_0, 1, lean::box(0));
lean::cnstr_set(x_0, 2, lean::box(0));
lean::cnstr_set(x_0, 3, lean::box(0));
x_36 = x_0;
} else {
lean::inc(x_28);
lean::inc(x_30);
lean::inc(x_32);
lean::inc(x_34);
lean::dec(x_0);
x_36 = lean::box(0);
}
x_37 = lean::nat_dec_lt(x_1, x_30);
if (x_37 == 0)
{
uint8 x_38;
x_38 = lean::nat_dec_lt(x_30, x_1);
if (x_38 == 0)
{
obj* x_41; obj* x_42;
lean::dec(x_30);
lean::dec(x_32);
if (lean::is_scalar(x_36)) {
x_41 = lean::alloc_cnstr(1, 4, 1);
} else {
x_41 = x_36;
}
lean::cnstr_set(x_41, 0, x_28);
lean::cnstr_set(x_41, 1, x_1);
lean::cnstr_set(x_41, 2, x_2);
lean::cnstr_set(x_41, 3, x_34);
lean::cnstr_set_scalar(x_41, sizeof(void*)*4, x_6);
x_42 = x_41;
return x_42;
}
else
{
uint8 x_43;
x_43 = l_rbnode_is__red___main___rarg(x_34);
if (x_43 == 0)
{
obj* x_44; obj* x_45; obj* x_46;
x_44 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__5___rarg(x_34, x_1, x_2);
if (lean::is_scalar(x_36)) {
x_45 = lean::alloc_cnstr(1, 4, 1);
} else {
x_45 = x_36;
}
lean::cnstr_set(x_45, 0, x_28);
lean::cnstr_set(x_45, 1, x_30);
lean::cnstr_set(x_45, 2, x_32);
lean::cnstr_set(x_45, 3, x_44);
lean::cnstr_set_scalar(x_45, sizeof(void*)*4, x_6);
x_46 = x_45;
return x_46;
}
else
{
obj* x_47; obj* x_48; obj* x_49; obj* x_50; obj* x_51;
x_47 = lean::box(0);
if (lean::is_scalar(x_36)) {
x_48 = lean::alloc_cnstr(1, 4, 1);
} else {
x_48 = x_36;
}
lean::cnstr_set(x_48, 0, x_28);
lean::cnstr_set(x_48, 1, x_30);
lean::cnstr_set(x_48, 2, x_32);
lean::cnstr_set(x_48, 3, x_47);
lean::cnstr_set_scalar(x_48, sizeof(void*)*4, x_6);
x_49 = x_48;
x_50 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__5___rarg(x_34, x_1, x_2);
x_51 = l_rbnode_balance2___main___rarg(x_49, x_50);
return x_51;
}
}
}
else
{
uint8 x_52;
x_52 = l_rbnode_is__red___main___rarg(x_28);
if (x_52 == 0)
{
obj* x_53; obj* x_54; obj* x_55;
x_53 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__5___rarg(x_28, x_1, x_2);
if (lean::is_scalar(x_36)) {
x_54 = lean::alloc_cnstr(1, 4, 1);
} else {
x_54 = x_36;
}
lean::cnstr_set(x_54, 0, x_53);
lean::cnstr_set(x_54, 1, x_30);
lean::cnstr_set(x_54, 2, x_32);
lean::cnstr_set(x_54, 3, x_34);
lean::cnstr_set_scalar(x_54, sizeof(void*)*4, x_6);
x_55 = x_54;
return x_55;
}
else
{
obj* x_56; obj* x_57; obj* x_58; obj* x_59; obj* x_60;
x_56 = lean::box(0);
if (lean::is_scalar(x_36)) {
x_57 = lean::alloc_cnstr(1, 4, 1);
} else {
x_57 = x_36;
}
lean::cnstr_set(x_57, 0, x_56);
lean::cnstr_set(x_57, 1, x_30);
lean::cnstr_set(x_57, 2, x_32);
lean::cnstr_set(x_57, 3, x_34);
lean::cnstr_set_scalar(x_57, sizeof(void*)*4, x_6);
x_58 = x_57;
x_59 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__5___rarg(x_28, x_1, x_2);
x_60 = l_rbnode_balance1___main___rarg(x_58, x_59);
return x_60;
}
}
}
}
}
}
obj* l_rbnode_ins___main___at_lean_file__map_from__string___spec__5(obj* x_0) {
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_rbnode_ins___main___at_lean_file__map_from__string___spec__5___rarg), 3, 0);
return x_1;
}
}
obj* l_rbnode_insert___at_lean_file__map_from__string___spec__3___rarg(obj* x_0, obj* x_1, obj* x_2) {
obj* l_rbnode_insert___at_lean_file__map_from__string___spec__3(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
uint8 x_3;
@ -872,42 +614,26 @@ x_3 = l_rbnode_is__red___main___rarg(x_0);
if (x_3 == 0)
{
obj* x_4;
x_4 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4___rarg(x_0, x_1, x_2);
x_4 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4(x_0, x_1, x_2);
return x_4;
}
else
{
obj* x_5; obj* x_6;
x_5 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__5___rarg(x_0, x_1, x_2);
x_5 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4(x_0, x_1, x_2);
x_6 = l_rbnode_set__black___main___rarg(x_5);
return x_6;
}
}
}
obj* l_rbnode_insert___at_lean_file__map_from__string___spec__3(obj* x_0) {
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_rbnode_insert___at_lean_file__map_from__string___spec__3___rarg), 3, 0);
return x_1;
}
}
obj* l_rbmap_insert___main___at_lean_file__map_from__string___spec__2___rarg(obj* x_0, obj* x_1, obj* x_2) {
obj* l_rbmap_insert___main___at_lean_file__map_from__string___spec__2(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
obj* x_3;
x_3 = l_rbnode_insert___at_lean_file__map_from__string___spec__3___rarg(x_0, x_1, x_2);
x_3 = l_rbnode_insert___at_lean_file__map_from__string___spec__3(x_0, x_1, x_2);
return x_3;
}
}
obj* l_rbmap_insert___main___at_lean_file__map_from__string___spec__2(obj* x_0) {
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_rbmap_insert___main___at_lean_file__map_from__string___spec__2___rarg), 3, 0);
return x_1;
}
}
obj* l_rbmap_of__list___main___at_lean_file__map_from__string___spec__1(obj* x_0) {
_start:
{
@ -931,7 +657,7 @@ x_9 = lean::cnstr_get(x_2, 1);
lean::inc(x_9);
lean::dec(x_2);
x_12 = l_rbmap_of__list___main___at_lean_file__map_from__string___spec__1(x_4);
x_13 = l_rbnode_insert___at_lean_file__map_from__string___spec__3___rarg(x_12, x_7, x_9);
x_13 = l_rbnode_insert___at_lean_file__map_from__string___spec__3(x_12, x_7, x_9);
return x_13;
}
}
@ -948,43 +674,7 @@ x_5 = l_rbmap_of__list___main___at_lean_file__map_from__string___spec__1(x_4);
return x_5;
}
}
obj* l_rbnode_ins___main___at_lean_file__map_from__string___spec__4___boxed(obj* x_0) {
_start:
{
obj* x_1;
x_1 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__4(x_0);
lean::dec(x_0);
return x_1;
}
}
obj* l_rbnode_ins___main___at_lean_file__map_from__string___spec__5___boxed(obj* x_0) {
_start:
{
obj* x_1;
x_1 = l_rbnode_ins___main___at_lean_file__map_from__string___spec__5(x_0);
lean::dec(x_0);
return x_1;
}
}
obj* l_rbnode_insert___at_lean_file__map_from__string___spec__3___boxed(obj* x_0) {
_start:
{
obj* x_1;
x_1 = l_rbnode_insert___at_lean_file__map_from__string___spec__3(x_0);
lean::dec(x_0);
return x_1;
}
}
obj* l_rbmap_insert___main___at_lean_file__map_from__string___spec__2___boxed(obj* x_0) {
_start:
{
obj* x_1;
x_1 = l_rbmap_insert___main___at_lean_file__map_from__string___spec__2(x_0);
lean::dec(x_0);
return x_1;
}
}
obj* l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2___rarg(obj* x_0, obj* x_1, obj* x_2) {
obj* l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
if (lean::obj_tag(x_0) == 0)
@ -1045,20 +735,12 @@ goto _start;
}
}
}
obj* l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2(obj* x_0) {
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2___rarg___boxed), 3, 0);
return x_1;
}
}
obj* l_rbmap_lower__bound___main___at_lean_file__map_to__position___spec__1(obj* x_0, obj* x_1) {
_start:
{
obj* x_2; obj* x_3;
x_2 = lean::box(0);
x_3 = l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2___rarg(x_0, x_1, x_2);
x_3 = l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2(x_0, x_1, x_2);
return x_3;
}
}
@ -1097,24 +779,15 @@ return x_16;
}
}
}
obj* l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2___rarg___boxed(obj* x_0, obj* x_1, obj* x_2) {
obj* l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2___boxed(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
obj* x_3;
x_3 = l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2___rarg(x_0, x_1, x_2);
x_3 = l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2(x_0, x_1, x_2);
lean::dec(x_1);
return x_3;
}
}
obj* l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2___boxed(obj* x_0) {
_start:
{
obj* x_1;
x_1 = l_rbnode_lower__bound___main___at_lean_file__map_to__position___spec__2(x_0);
lean::dec(x_0);
return x_1;
}
}
obj* l_rbmap_lower__bound___main___at_lean_file__map_to__position___spec__1___boxed(obj* x_0, obj* x_1) {
_start:
{

355
src/boot/init/lean/trace.cpp
View file

@ -14,17 +14,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_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__5___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___boxed(obj*);
obj* l_lean_trace_trace___rarg___lambda__1(obj*, obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__7(obj*, obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__5___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__4(obj*);
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__5(obj*);
obj* l_lean_trace_pp___main(obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__9(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
extern obj* l_lean_format_join___closed__1;
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__5___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2___boxed(obj*);
obj* l_lean_trace_trace___rarg___lambda__1___boxed(obj*, obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__1(obj*, obj*, obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__3___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
@ -34,25 +30,25 @@ obj* l_lean_trace_trace__t_run(obj*, obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__12___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_kvmap_get__bool(obj*, obj*);
obj* l_lean_trace_lean_trace_monad__tracer(obj*);
obj* l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3(obj*);
obj* l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3(obj*, obj*, obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__10(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__5___rarg___lambda__1(obj*, obj*, obj*);
obj* l_lean_trace_trace__t_run___boxed(obj*, obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__11(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg(obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__12(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_trace_trace___boxed(obj*);
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_trace_trace__t_run___rarg___lambda__1(obj*, obj*);
obj* l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3___rarg(obj*, obj*, obj*);
obj* l_rbmap_insert___main___at_lean_trace_lean_trace_monad__tracer___spec__1(obj*, obj*, obj*);
obj* l_rbnode_balance2___main___rarg(obj*, obj*);
obj* l_lean_trace_monad(obj*);
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg___lambda__1(obj*, obj*, obj*);
obj* l_lean_trace_trace___rarg(obj*, obj*, obj*, obj*);
obj* l_lean_has__coe(obj*);
obj* l_state__t_monad___rarg(obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__4___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(obj*, obj*, obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__5(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_trace_trace(obj*);
obj* l_list_foldl___main___at_lean_format_join___spec__1(obj*, obj*);
@ -61,23 +57,20 @@ obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__3(obj*, obj*, obj*,
obj* l_rbnode_balance1___main___rarg(obj*, obj*);
obj* l_lean_trace_trace__t_run___rarg(obj*, obj*, obj*);
obj* l_lean_trace_monad___rarg(obj*);
obj* l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__4___boxed(obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__9___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3___boxed(obj*);
obj* l_lean_has__coe___boxed(obj*);
uint8 l_lean_position_decidable__lt___main(obj*, obj*);
obj* l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2___rarg(obj*, obj*, obj*);
obj* l_lean_trace_monad___boxed(obj*);
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4(obj*);
uint8 l_rbnode_is__red___main___rarg(obj*);
obj* l_lean_trace_pp(obj*);
obj* l_list_append___rarg(obj*, obj*);
obj* l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2(obj*);
obj* l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2(obj*, obj*, obj*);
obj* l_list_map___main___at_lean_trace_pp___main___spec__1(obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__10___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_lean_trace_lean_trace_monad__tracer___boxed(obj*);
obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__6(obj*, obj*, obj*);
obj* l_rbnode_set__black___main___rarg(obj*);
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__5___boxed(obj*);
obj* l_lean_has__coe(obj* x_0) {
_start:
{
@ -249,7 +242,7 @@ lean::dec(x_0);
return x_1;
}
}
obj* l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3___rarg(obj* x_0, obj* x_1, obj* x_2) {
obj* l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
if (lean::obj_tag(x_0) == 0)
@ -320,7 +313,7 @@ return x_25;
else
{
obj* x_26; obj* x_27; obj* x_28;
x_26 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3___rarg(x_13, x_1, x_2);
x_26 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3(x_13, x_1, x_2);
if (lean::is_scalar(x_15)) {
x_27 = lean::alloc_cnstr(1, 4, 1);
} else {
@ -338,7 +331,7 @@ return x_28;
else
{
obj* x_29; obj* x_30; obj* x_31;
x_29 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3___rarg(x_7, x_1, x_2);
x_29 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3(x_7, x_1, x_2);
if (lean::is_scalar(x_15)) {
x_30 = lean::alloc_cnstr(1, 4, 1);
} else {
@ -408,7 +401,7 @@ x_51 = l_rbnode_is__red___main___rarg(x_38);
if (x_51 == 0)
{
obj* x_52; obj* x_53; obj* x_54;
x_52 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3___rarg(x_38, x_1, x_2);
x_52 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3(x_38, x_1, x_2);
if (lean::is_scalar(x_40)) {
x_53 = lean::alloc_cnstr(1, 4, 1);
} else {
@ -437,7 +430,7 @@ lean::cnstr_set(x_56, 2, x_36);
lean::cnstr_set(x_56, 3, x_55);
lean::cnstr_set_scalar(x_56, sizeof(void*)*4, x_6);
x_57 = x_56;
x_58 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3___rarg(x_38, x_1, x_2);
x_58 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3(x_38, x_1, x_2);
x_59 = l_rbnode_balance2___main___rarg(x_57, x_58);
return x_59;
}
@ -450,7 +443,7 @@ x_60 = l_rbnode_is__red___main___rarg(x_32);
if (x_60 == 0)
{
obj* x_61; obj* x_62; obj* x_63;
x_61 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3___rarg(x_32, x_1, x_2);
x_61 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3(x_32, x_1, x_2);
if (lean::is_scalar(x_40)) {
x_62 = lean::alloc_cnstr(1, 4, 1);
} else {
@ -479,7 +472,7 @@ lean::cnstr_set(x_65, 2, x_36);
lean::cnstr_set(x_65, 3, x_38);
lean::cnstr_set_scalar(x_65, sizeof(void*)*4, x_6);
x_66 = x_65;
x_67 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3___rarg(x_32, x_1, x_2);
x_67 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3(x_32, x_1, x_2);
x_68 = l_rbnode_balance1___main___rarg(x_66, x_67);
return x_68;
}
@ -488,262 +481,7 @@ return x_68;
}
}
}
obj* l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3(obj* x_0) {
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3___rarg), 3, 0);
return x_1;
}
}
obj* l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
if (lean::obj_tag(x_0) == 0)
{
uint8 x_3; obj* x_4; obj* x_5;
x_3 = 0;
x_4 = lean::alloc_cnstr(1, 4, 1);
lean::cnstr_set(x_4, 0, x_0);
lean::cnstr_set(x_4, 1, x_1);
lean::cnstr_set(x_4, 2, x_2);
lean::cnstr_set(x_4, 3, x_0);
lean::cnstr_set_scalar(x_4, sizeof(void*)*4, x_3);
x_5 = x_4;
return x_5;
}
else
{
uint8 x_6;
x_6 = lean::cnstr_get_scalar<uint8>(x_0, sizeof(void*)*4);
if (x_6 == 0)
{
obj* x_7; obj* x_9; obj* x_11; obj* x_13; obj* x_15; uint8 x_18;
x_7 = lean::cnstr_get(x_0, 0);
x_9 = lean::cnstr_get(x_0, 1);
x_11 = lean::cnstr_get(x_0, 2);
x_13 = lean::cnstr_get(x_0, 3);
if (lean::is_exclusive(x_0)) {
lean::cnstr_set(x_0, 0, lean::box(0));
lean::cnstr_set(x_0, 1, lean::box(0));
lean::cnstr_set(x_0, 2, lean::box(0));
lean::cnstr_set(x_0, 3, lean::box(0));
x_15 = x_0;
} else {
lean::inc(x_7);
lean::inc(x_9);
lean::inc(x_11);
lean::inc(x_13);
lean::dec(x_0);
x_15 = lean::box(0);
}
lean::inc(x_9);
lean::inc(x_1);
x_18 = l_lean_position_decidable__lt___main(x_1, x_9);
if (x_18 == 0)
{
uint8 x_21;
lean::inc(x_1);
lean::inc(x_9);
x_21 = l_lean_position_decidable__lt___main(x_9, x_1);
if (x_21 == 0)
{
obj* x_24; obj* x_25;
lean::dec(x_9);
lean::dec(x_11);
if (lean::is_scalar(x_15)) {
x_24 = lean::alloc_cnstr(1, 4, 1);
} else {
x_24 = x_15;
}
lean::cnstr_set(x_24, 0, x_7);
lean::cnstr_set(x_24, 1, x_1);
lean::cnstr_set(x_24, 2, x_2);
lean::cnstr_set(x_24, 3, x_13);
lean::cnstr_set_scalar(x_24, sizeof(void*)*4, x_6);
x_25 = x_24;
return x_25;
}
else
{
obj* x_26; obj* x_27; obj* x_28;
x_26 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(x_13, x_1, x_2);
if (lean::is_scalar(x_15)) {
x_27 = lean::alloc_cnstr(1, 4, 1);
} else {
x_27 = x_15;
}
lean::cnstr_set(x_27, 0, x_7);
lean::cnstr_set(x_27, 1, x_9);
lean::cnstr_set(x_27, 2, x_11);
lean::cnstr_set(x_27, 3, x_26);
lean::cnstr_set_scalar(x_27, sizeof(void*)*4, x_6);
x_28 = x_27;
return x_28;
}
}
else
{
obj* x_29; obj* x_30; obj* x_31;
x_29 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(x_7, x_1, x_2);
if (lean::is_scalar(x_15)) {
x_30 = lean::alloc_cnstr(1, 4, 1);
} else {
x_30 = x_15;
}
lean::cnstr_set(x_30, 0, x_29);
lean::cnstr_set(x_30, 1, x_9);
lean::cnstr_set(x_30, 2, x_11);
lean::cnstr_set(x_30, 3, x_13);
lean::cnstr_set_scalar(x_30, sizeof(void*)*4, x_6);
x_31 = x_30;
return x_31;
}
}
else
{
obj* x_32; obj* x_34; obj* x_36; obj* x_38; obj* x_40; uint8 x_43;
x_32 = lean::cnstr_get(x_0, 0);
x_34 = lean::cnstr_get(x_0, 1);
x_36 = lean::cnstr_get(x_0, 2);
x_38 = lean::cnstr_get(x_0, 3);
if (lean::is_exclusive(x_0)) {
lean::cnstr_set(x_0, 0, lean::box(0));
lean::cnstr_set(x_0, 1, lean::box(0));
lean::cnstr_set(x_0, 2, lean::box(0));
lean::cnstr_set(x_0, 3, lean::box(0));
x_40 = x_0;
} else {
lean::inc(x_32);
lean::inc(x_34);
lean::inc(x_36);
lean::inc(x_38);
lean::dec(x_0);
x_40 = lean::box(0);
}
lean::inc(x_34);
lean::inc(x_1);
x_43 = l_lean_position_decidable__lt___main(x_1, x_34);
if (x_43 == 0)
{
uint8 x_46;
lean::inc(x_1);
lean::inc(x_34);
x_46 = l_lean_position_decidable__lt___main(x_34, x_1);
if (x_46 == 0)
{
obj* x_49; obj* x_50;
lean::dec(x_34);
lean::dec(x_36);
if (lean::is_scalar(x_40)) {
x_49 = lean::alloc_cnstr(1, 4, 1);
} else {
x_49 = x_40;
}
lean::cnstr_set(x_49, 0, x_32);
lean::cnstr_set(x_49, 1, x_1);
lean::cnstr_set(x_49, 2, x_2);
lean::cnstr_set(x_49, 3, x_38);
lean::cnstr_set_scalar(x_49, sizeof(void*)*4, x_6);
x_50 = x_49;
return x_50;
}
else
{
uint8 x_51;
x_51 = l_rbnode_is__red___main___rarg(x_38);
if (x_51 == 0)
{
obj* x_52; obj* x_53; obj* x_54;
x_52 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(x_38, x_1, x_2);
if (lean::is_scalar(x_40)) {
x_53 = lean::alloc_cnstr(1, 4, 1);
} else {
x_53 = x_40;
}
lean::cnstr_set(x_53, 0, x_32);
lean::cnstr_set(x_53, 1, x_34);
lean::cnstr_set(x_53, 2, x_36);
lean::cnstr_set(x_53, 3, x_52);
lean::cnstr_set_scalar(x_53, sizeof(void*)*4, x_6);
x_54 = x_53;
return x_54;
}
else
{
obj* x_55; obj* x_56; obj* x_57; obj* x_58; obj* x_59;
x_55 = lean::box(0);
if (lean::is_scalar(x_40)) {
x_56 = lean::alloc_cnstr(1, 4, 1);
} else {
x_56 = x_40;
}
lean::cnstr_set(x_56, 0, x_32);
lean::cnstr_set(x_56, 1, x_34);
lean::cnstr_set(x_56, 2, x_36);
lean::cnstr_set(x_56, 3, x_55);
lean::cnstr_set_scalar(x_56, sizeof(void*)*4, x_6);
x_57 = x_56;
x_58 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(x_38, x_1, x_2);
x_59 = l_rbnode_balance2___main___rarg(x_57, x_58);
return x_59;
}
}
}
else
{
uint8 x_60;
x_60 = l_rbnode_is__red___main___rarg(x_32);
if (x_60 == 0)
{
obj* x_61; obj* x_62; obj* x_63;
x_61 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(x_32, x_1, x_2);
if (lean::is_scalar(x_40)) {
x_62 = lean::alloc_cnstr(1, 4, 1);
} else {
x_62 = x_40;
}
lean::cnstr_set(x_62, 0, x_61);
lean::cnstr_set(x_62, 1, x_34);
lean::cnstr_set(x_62, 2, x_36);
lean::cnstr_set(x_62, 3, x_38);
lean::cnstr_set_scalar(x_62, sizeof(void*)*4, x_6);
x_63 = x_62;
return x_63;
}
else
{
obj* x_64; obj* x_65; obj* x_66; obj* x_67; obj* x_68;
x_64 = lean::box(0);
if (lean::is_scalar(x_40)) {
x_65 = lean::alloc_cnstr(1, 4, 1);
} else {
x_65 = x_40;
}
lean::cnstr_set(x_65, 0, x_64);
lean::cnstr_set(x_65, 1, x_34);
lean::cnstr_set(x_65, 2, x_36);
lean::cnstr_set(x_65, 3, x_38);
lean::cnstr_set_scalar(x_65, sizeof(void*)*4, x_6);
x_66 = x_65;
x_67 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(x_32, x_1, x_2);
x_68 = l_rbnode_balance1___main___rarg(x_66, x_67);
return x_68;
}
}
}
}
}
}
obj* l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__4(obj* x_0) {
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg), 3, 0);
return x_1;
}
}
obj* l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2___rarg(obj* x_0, obj* x_1, obj* x_2) {
obj* l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
uint8 x_3;
@ -751,35 +489,27 @@ x_3 = l_rbnode_is__red___main___rarg(x_0);
if (x_3 == 0)
{
obj* x_4;
x_4 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3___rarg(x_0, x_1, x_2);
x_4 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3(x_0, x_1, x_2);
return x_4;
}
else
{
obj* x_5; obj* x_6;
x_5 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(x_0, x_1, x_2);
x_5 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3(x_0, x_1, x_2);
x_6 = l_rbnode_set__black___main___rarg(x_5);
return x_6;
}
}
}
obj* l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2(obj* x_0) {
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2___rarg), 3, 0);
return x_1;
}
}
obj* l_rbmap_insert___main___at_lean_trace_lean_trace_monad__tracer___spec__1(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
obj* x_3;
x_3 = l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2___rarg(x_0, x_1, x_2);
x_3 = l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2(x_0, x_1, x_2);
return x_3;
}
}
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__5___rarg___lambda__1(obj* x_0, obj* x_1, obj* x_2) {
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg___lambda__1(obj* x_0, obj* x_1, obj* x_2) {
_start:
{
obj* x_3; obj* x_5; obj* x_7; obj* x_8; obj* x_11; obj* x_14; obj* x_15; obj* x_16;
@ -811,7 +541,7 @@ x_16 = lean::apply_2(x_11, lean::box(0), x_15);
return x_16;
}
}
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__5___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
_start:
{
obj* x_6; obj* x_7; obj* x_9; obj* x_10; obj* x_11;
@ -819,18 +549,18 @@ x_6 = lean::apply_1(x_2, x_5);
x_7 = lean::cnstr_get(x_0, 1);
lean::inc(x_7);
x_9 = lean::apply_1(x_4, x_6);
x_10 = lean::alloc_closure(reinterpret_cast<void*>(l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__5___rarg___lambda__1), 3, 2);
x_10 = lean::alloc_closure(reinterpret_cast<void*>(l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg___lambda__1), 3, 2);
lean::closure_set(x_10, 0, x_0);
lean::closure_set(x_10, 1, x_3);
x_11 = lean::apply_4(x_7, lean::box(0), lean::box(0), x_9, x_10);
return x_11;
}
}
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__5(obj* x_0) {
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4(obj* x_0) {
_start:
{
obj* x_1;
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__5___rarg___boxed), 6, 0);
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg___boxed), 6, 0);
return x_1;
}
}
@ -882,7 +612,7 @@ lean::inc(x_14);
x_17 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_17, 0, x_0);
lean::cnstr_set(x_17, 1, x_14);
x_18 = l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2___rarg(x_12, x_1, x_17);
x_18 = l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2(x_12, x_1, x_17);
x_19 = lean::cnstr_get(x_7, 2);
lean::inc(x_19);
lean::dec(x_7);
@ -1261,7 +991,7 @@ x_54 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad
lean::closure_set(x_54, 0, x_2);
x_55 = lean::thunk_get(x_0);
lean::dec(x_0);
x_57 = l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__5___rarg(x_3, lean::box(0), x_53, x_54, x_55, x_24);
x_57 = l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(x_3, lean::box(0), x_53, x_54, x_55, x_24);
return x_57;
}
lbl_32:
@ -1392,47 +1122,20 @@ x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad_
return x_1;
}
}
obj* l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3___boxed(obj* x_0) {
_start:
{
obj* x_1;
x_1 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__3(x_0);
lean::dec(x_0);
return x_1;
}
}
obj* l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__4___boxed(obj* x_0) {
_start:
{
obj* x_1;
x_1 = l_rbnode_ins___main___at_lean_trace_lean_trace_monad__tracer___spec__4(x_0);
lean::dec(x_0);
return x_1;
}
}
obj* l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2___boxed(obj* x_0) {
_start:
{
obj* x_1;
x_1 = l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2(x_0);
lean::dec(x_0);
return x_1;
}
}
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__5___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
_start:
{
obj* x_6;
x_6 = l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__5___rarg(x_0, x_1, x_2, x_3, x_4, x_5);
x_6 = l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(x_0, x_1, x_2, x_3, x_4, x_5);
lean::dec(x_1);
return x_6;
}
}
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__5___boxed(obj* x_0) {
obj* l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___boxed(obj* x_0) {
_start:
{
obj* x_1;
x_1 = l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__5(x_0);
x_1 = l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4(x_0);
lean::dec(x_0);
return x_1;
}