diff --git a/src/boot/init/coe.cpp b/src/boot/init/coe.cpp index 3b3bb6bfbf..c25145fcd6 100644 --- a/src/boot/init/coe.cpp +++ b/src/boot/init/coe.cpp @@ -3,8 +3,6 @@ // Imports: init.data.list.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/control/alternative.cpp b/src/boot/init/control/alternative.cpp index 8d2921afb4..c452872b3b 100644 --- a/src/boot/init/control/alternative.cpp +++ b/src/boot/init/control/alternative.cpp @@ -3,8 +3,6 @@ // Imports: init.core init.control.applicative #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/control/applicative.cpp b/src/boot/init/control/applicative.cpp index cd5ec58411..8ae7aec402 100644 --- a/src/boot/init/control/applicative.cpp +++ b/src/boot/init/control/applicative.cpp @@ -3,8 +3,6 @@ // Imports: init.control.functor #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/control/combinators.cpp b/src/boot/init/control/combinators.cpp index 0f1e7bbdef..9a7acbbec1 100644 --- a/src/boot/init/control/combinators.cpp +++ b/src/boot/init/control/combinators.cpp @@ -3,8 +3,6 @@ // Imports: init.control.monad init.control.alternative init.data.list.basic init.coe #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -51,6 +49,7 @@ obj* l_mwhen___rarg___lambda__1(obj*, obj*, uint8); obj* l_list_mexists___main___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*); obj* l_list_mforall___main___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*); obj* l_list_mfoldr___main(obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_list_mmap___main___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*); obj* l_list_mfirst___main(obj*); obj* l_nat_mrepeat___rarg(obj*, obj*, obj*); @@ -76,6 +75,7 @@ obj* l_list_mfoldl___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_list_mexists___main(obj*); obj* l_list_mexists___main___rarg(obj*, obj*, obj*, obj*); obj* l_mcond(obj*); +obj* l_nat_sub(obj*, obj*); obj* l_list_mforall___main___rarg___lambda__1(obj*, obj*, obj*, uint8); obj* l_unless(obj*); obj* l_when(obj*); diff --git a/src/boot/init/control/coroutine.cpp b/src/boot/init/control/coroutine.cpp index 55d7b2d22e..d3b887baf3 100644 --- a/src/boot/init/control/coroutine.cpp +++ b/src/boot/init/control/coroutine.cpp @@ -3,8 +3,6 @@ // Imports: init.control.monad init.wf init.control.reader #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/control/default.cpp b/src/boot/init/control/default.cpp index 114999f563..a7672f7f31 100644 --- a/src/boot/init/control/default.cpp +++ b/src/boot/init/control/default.cpp @@ -3,8 +3,6 @@ // Imports: init.control.applicative init.control.functor init.control.alternative init.control.monad init.control.lift init.control.state init.control.id init.control.except init.control.reader init.control.option init.control.combinators #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/control/except.cpp b/src/boot/init/control/except.cpp index 83b8190628..2df9a01953 100644 --- a/src/boot/init/control/except.cpp +++ b/src/boot/init/control/except.cpp @@ -3,8 +3,6 @@ // Imports: init.control.alternative init.control.lift init.data.to_string init.control.monad_fail #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -51,6 +49,9 @@ obj* l_except_monad___lambda__5(obj*, obj*, obj*, obj*); obj* l_except_map__error___rarg(obj*, obj*); obj* l_except__t_bind__cont___at_except__t_monad___spec__1___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_except__t_monad___rarg___lambda__6(obj*, obj*, obj*); +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_except__t_monad__except___rarg(obj*); obj* l_except_has__to__string(obj*, obj*); obj* l_function_comp___rarg(obj*, obj*, obj*); diff --git a/src/boot/init/control/functor.cpp b/src/boot/init/control/functor.cpp index 3300007ce6..cac19230b0 100644 --- a/src/boot/init/control/functor.cpp +++ b/src/boot/init/control/functor.cpp @@ -3,8 +3,6 @@ // Imports: init.core init.function #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/control/id.cpp b/src/boot/init/control/id.cpp index fa0488a532..f10682ad60 100644 --- a/src/boot/init/control/id.cpp +++ b/src/boot/init/control/id.cpp @@ -3,8 +3,6 @@ // Imports: init.control.lift #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/control/lift.cpp b/src/boot/init/control/lift.cpp index 5969d89530..4f43d60efb 100644 --- a/src/boot/init/control/lift.cpp +++ b/src/boot/init/control/lift.cpp @@ -3,8 +3,6 @@ // Imports: init.function init.coe init.control.monad #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/control/monad.cpp b/src/boot/init/control/monad.cpp index 745660d9e3..6f7883ea81 100644 --- a/src/boot/init/control/monad.cpp +++ b/src/boot/init/control/monad.cpp @@ -3,8 +3,6 @@ // Imports: init.control.applicative #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/control/monad_fail.cpp b/src/boot/init/control/monad_fail.cpp index 4c3ef3f6fa..ef9d7eab61 100644 --- a/src/boot/init/control/monad_fail.cpp +++ b/src/boot/init/control/monad_fail.cpp @@ -3,8 +3,6 @@ // Imports: init.control.lift init.data.string.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/control/option.cpp b/src/boot/init/control/option.cpp index 0b34887e0a..91905bf712 100644 --- a/src/boot/init/control/option.cpp +++ b/src/boot/init/control/option.cpp @@ -3,8 +3,6 @@ // Imports: init.control.alternative init.control.lift init.control.except #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/control/reader.cpp b/src/boot/init/control/reader.cpp index 4720f4739d..58e504bcdd 100644 --- a/src/boot/init/control/reader.cpp +++ b/src/boot/init/control/reader.cpp @@ -3,8 +3,6 @@ // Imports: init.control.lift init.control.id init.control.alternative init.control.except #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/control/state.cpp b/src/boot/init/control/state.cpp index be7194895b..8210f28def 100644 --- a/src/boot/init/control/state.cpp +++ b/src/boot/init/control/state.cpp @@ -3,8 +3,6 @@ // Imports: init.control.alternative init.control.lift init.control.id init.control.except #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/core.cpp b/src/boot/init/core.cpp index 55419ee0b4..9734cdd05a 100644 --- a/src/boot/init/core.cpp +++ b/src/boot/init/core.cpp @@ -3,8 +3,6 @@ // Imports: #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -32,6 +30,7 @@ uint8 l_prod__has__decidable__lt___rarg(obj*, obj*, obj*, obj*, obj*, obj*); uint8 l_band___main(uint8, uint8); uint8 l_sum_decidable__eq___rarg(obj*, obj*, obj*, obj*); uint8 l_xor_decidable___rarg(uint8, uint8); +obj* l_thunk_pure(obj*, obj*); uint8 l_ite_decidable___rarg(uint8, uint8, uint8); uint8 l_true_decidable; obj* l_inline___rarg(obj*); @@ -53,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_nat_add(obj*, obj*); 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*); @@ -161,6 +161,7 @@ obj* l_empty__relation; obj* l_list_has__sizeof(obj*); obj* l_eq_ndrec(obj*, obj*, obj*); obj* l_left__cancelative; +obj* l_thunk_bind(obj*, obj*, obj*, obj*); obj* l_pi_inhabited(obj*, obj*); obj* l_option_has__sizeof(obj*); uint8 l_bnot___main(uint8); @@ -191,6 +192,7 @@ obj* l_quotient_sound; obj* l_option_has__sizeof___rarg(obj*); obj* l_list_sizeof(obj*); obj* l_right__identity; +uint8 l_nat_dec__eq(obj*, obj*); obj* l_std_prec_arrow; uint8 l_decidable__eq__of__bool__pred___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_bit0___rarg(obj*, obj*); @@ -239,6 +241,7 @@ obj* l_psum_sizeof___rarg(obj*, obj*, obj*); obj* l_xor_decidable___rarg___boxed(obj*, obj*); obj* l_psum_has__sizeof___rarg(obj*, obj*); obj* l_classical_by__cases; +obj* l_thunk_map(obj*, obj*, obj*, obj*); obj* l_bool_decidable__eq___boxed(obj*, obj*); obj* l_prod__has__decidable__lt___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_quotient_lift_u_2082___rarg(obj*, obj*, obj*, obj*); @@ -260,6 +263,7 @@ obj* l_ge; obj* l_option_sizeof___main(obj*); obj* l_quot_rec__on___rarg(obj*, obj*, obj*); obj* l_dite___rarg(uint8, obj*, obj*, obj*); +obj* l_thunk_get(obj*, obj*); obj* l_task_map___rarg(obj*, obj*, obj*); obj* l_quotient_rec__on__subsingleton_u_2082___rarg(obj*, obj*, obj*); obj* l_subtype_sizeof___main(obj*); @@ -364,6 +368,7 @@ uint8 l_bnot(uint8); obj* l_std_prec_max__plus; obj* l_absurd(obj*, obj*, obj*, obj*); obj* l_eq_mp___rarg(obj*); +obj* l_nat_sub(obj*, obj*); obj* l___private_init_core_27__extfun__app___rarg(obj*, obj*); obj* l_quotient_lift__on___rarg(obj*, obj*, obj*); uint8 l_subtype_decidable__eq___rarg(obj*, obj*, obj*); diff --git a/src/boot/init/data/array/basic.cpp b/src/boot/init/data/array/basic.cpp index e9f8bd4c60..015b07c1a8 100644 --- a/src/boot/init/data/array/basic.cpp +++ b/src/boot/init/data/array/basic.cpp @@ -3,8 +3,6 @@ // Imports: init.data.nat.basic init.data.fin.basic init.data.usize init.data.repr init.function #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -21,6 +19,7 @@ obj* l_array_rev__iterate(obj*, obj*); obj* l_array_push___rarg___lambda__1(obj*, obj*, obj*, obj*); obj* l_array_rev__foldl(obj*, obj*); obj* l_array_uread___rarg___boxed(obj*, obj*, obj*); +obj* l_nat_add(obj*, obj*); obj* l_array_rev__iterate___rarg(obj*, obj*, obj*); obj* l_array_read___rarg(obj*, obj*); obj* l___private_init_data_array_basic_2__rev__iterate__aux___main___rarg(obj*, obj*, obj*, obj*, obj*); @@ -58,11 +57,13 @@ obj* l_array_foldl(obj*, obj*); obj* l___private_init_data_array_basic_1__iterate__aux___main(obj*, obj*); uint8 l_array_empty___rarg(obj*); obj* l___private_init_data_array_basic_3__foreach__aux(obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_array_pop___rarg(obj*); obj* l_list_repr___rarg(obj*, obj*); obj* l_array_map_u_2082(obj*); obj* l_list_to__array__aux(obj*); obj* l_array_uread_x_27___rarg___boxed(obj*, obj*, obj*); +uint8 l_nat_dec__le(obj*, obj*); obj* l_array_foreach(obj*); obj* l_array_foldl___rarg(obj*, obj*, obj*); obj* l_mk__array___rarg___lambda__1(obj*, obj*); @@ -89,12 +90,17 @@ obj* l___private_init_data_array_basic_2__rev__iterate__aux___main(obj*, obj*); obj* l_array_foldl___rarg___lambda__1(obj*, obj*, obj*, obj*); obj* l_array_map___rarg(obj*, obj*); obj* l_array_map___rarg___lambda__1(obj*, obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l___private_init_data_array_basic_2__rev__iterate__aux___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_array_read_x_27___rarg(obj*, obj*, obj*); obj* l_array_to__list___rarg___closed__1; obj* l_list_to__array___rarg(obj*); obj* l_array_iterate(obj*, obj*); +namespace lean { +obj* usize_to_nat(usize); +} obj* l___private_init_data_array_basic_1__iterate__aux___main___rarg(obj*, obj*, obj*, obj*, obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* l_mk__array___rarg(obj* x_0, obj* x_1) { _start: { diff --git a/src/boot/init/data/array/default.cpp b/src/boot/init/data/array/default.cpp index 372d319860..92b87f5cc5 100644 --- a/src/boot/init/data/array/default.cpp +++ b/src/boot/init/data/array/default.cpp @@ -3,8 +3,6 @@ // Imports: init.data.array.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/basic.cpp b/src/boot/init/data/basic.cpp index 2b3a48e03d..b99659b9ff 100644 --- a/src/boot/init/data/basic.cpp +++ b/src/boot/init/data/basic.cpp @@ -3,8 +3,6 @@ // Imports: init.data.nat.basic init.data.fin.basic init.data.list.basic init.data.char.basic init.data.string.basic init.data.option.basic init.data.uint init.data.ordering.basic init.data.repr init.data.to_string #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/char/basic.cpp b/src/boot/init/data/char/basic.cpp index de9beb7330..e4d70e77a2 100644 --- a/src/boot/init/data/char/basic.cpp +++ b/src/boot/init/data/char/basic.cpp @@ -3,8 +3,6 @@ // Imports: init.data.nat.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -19,6 +17,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; uint8 l_char_is__whitespace(uint32); obj* l_char_is__upper___boxed(obj*); uint8 l_char_is__lower(uint32); +obj* l_nat_add(obj*, obj*); obj* l_char_to__lower(uint32); obj* l_char_is__digit___boxed(obj*); obj* l_char_dec__lt___boxed(obj*, obj*); @@ -32,10 +31,12 @@ obj* l_char_to__lower___boxed(obj*); obj* l_char_is__whitespace___boxed(obj*); obj* l_char_to__nat___boxed(obj*); obj* l_char_dec__le___boxed(obj*, obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_char_has__sizeof___boxed(obj*); obj* l_char_lt; obj* l_char_inhabited; uint32 l_char_has__sizeof(uint32); +uint8 l_nat_dec__le(obj*, obj*); uint8 l_char_dec__lt(uint32, uint32); obj* l_char_is__lower___boxed(obj*); obj* l_char_decidable__eq___boxed(obj*, obj*); @@ -47,6 +48,7 @@ uint8 l_char_decidable__eq(uint32, uint32); uint32 l_char_to__nat(uint32); obj* l_is__valid__char; obj* l_char_is__alpha___boxed(obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* _init_l_is__valid__char() { _start: { diff --git a/src/boot/init/data/char/default.cpp b/src/boot/init/data/char/default.cpp index 6e3aa1c896..32906ef4d3 100644 --- a/src/boot/init/data/char/default.cpp +++ b/src/boot/init/data/char/default.cpp @@ -3,8 +3,6 @@ // Imports: init.data.char.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/default.cpp b/src/boot/init/data/default.cpp index 6167d4379e..b77affa6c8 100644 --- a/src/boot/init/data/default.cpp +++ b/src/boot/init/data/default.cpp @@ -3,8 +3,6 @@ // Imports: init.data.basic init.data.nat.default init.data.char.default init.data.string.default init.data.list.default init.data.int.default init.data.array.default init.data.fin.default init.data.uint init.data.ordering.default init.data.rbtree.default init.data.rbmap.default init.data.option.basic init.data.option.instances #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/dlist.cpp b/src/boot/init/data/dlist.cpp index 27b1e82423..f966015134 100644 --- a/src/boot/init/data/dlist.cpp +++ b/src/boot/init/data/dlist.cpp @@ -3,8 +3,6 @@ // Imports: init.data.list.basic init.function #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/fin/basic.cpp b/src/boot/init/data/fin/basic.cpp index c53ab1dabd..1fc8db10e0 100644 --- a/src/boot/init/data/fin/basic.cpp +++ b/src/boot/init/data/fin/basic.cpp @@ -3,8 +3,6 @@ // Imports: init.data.nat.div #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -22,8 +20,10 @@ obj* l_fin_modn(obj*, obj*, obj*); obj* l_fin_has__one(obj*); obj* l_fin_elim0___main(obj*, obj*); uint8 l_fin_dec__lt___rarg(obj*, obj*); +obj* l_nat_add(obj*, obj*); obj* l_fin_mod(obj*, obj*, obj*); obj* l_fin_le; +obj* l_nat_mod(obj*, obj*); uint8 l_fin_dec__le___rarg(obj*, obj*); obj* l_fin_has__le(obj*); obj* l_fin_sub(obj*, obj*, obj*); @@ -31,9 +31,12 @@ obj* l_fin_decidable__eq(obj*); obj* l_fin_mod___main(obj*, obj*, obj*); obj* l_fin_lt; obj* l_fin_add(obj*, obj*, obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_fin_add___main(obj*, obj*, obj*); obj* l_fin_of__nat(obj*, obj*); +uint8 l_nat_dec__le(obj*, obj*); obj* l_fin_has__sub(obj*); +obj* l_nat_div(obj*, obj*); obj* l_fin_mul___main(obj*, obj*, obj*); obj* l_fin_has__div(obj*); obj* l_fin_dec__le(obj*); @@ -44,13 +47,16 @@ obj* l_fin_mul(obj*, obj*, obj*); obj* l_fin_has__modn(obj*); obj* l_fin_dec__le___rarg___boxed(obj*, obj*); obj* l_fin_dec__lt(obj*); +obj* l_nat_mul(obj*, obj*); obj* l_fin_div___main(obj*, obj*, obj*); obj* l_fin_dec__lt___rarg___boxed(obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l_fin_has__mod(obj*); obj* l_fin_has__mul(obj*); obj* l_fin_modn___main(obj*, obj*, obj*); obj* l_fin_div(obj*, obj*, obj*); obj* l_fin_has__add(obj*); +uint8 l_nat_dec__lt(obj*, obj*); uint8 l_fin_decidable__eq___rarg(obj*, obj*); obj* _init_l_fin_lt() { _start: diff --git a/src/boot/init/data/fin/default.cpp b/src/boot/init/data/fin/default.cpp index d99ff56ca7..09d161168b 100644 --- a/src/boot/init/data/fin/default.cpp +++ b/src/boot/init/data/fin/default.cpp @@ -3,8 +3,6 @@ // Imports: init.data.fin.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/hashable.cpp b/src/boot/init/data/hashable.cpp index e8b23d76e5..797b998aa6 100644 --- a/src/boot/init/data/hashable.cpp +++ b/src/boot/init/data/hashable.cpp @@ -3,8 +3,6 @@ // Imports: init.data.usize init.data.string.default #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -24,6 +22,9 @@ obj* l_nat_hash___boxed(obj*); obj* l_mix__hash___boxed(obj*, obj*); usize l_nat_hash(obj*); usize l_mix__hash(usize, usize); +namespace lean { +usize usize_of_nat(obj*); +} obj* l_string_hash___boxed(obj*); usize l_mix__hash___closed__1; usize _init_l_mix__hash___closed__1() { diff --git a/src/boot/init/data/hashmap/basic.cpp b/src/boot/init/data/hashmap/basic.cpp index c1a8409ef1..344d680338 100644 --- a/src/boot/init/data/hashmap/basic.cpp +++ b/src/boot/init/data/hashmap/basic.cpp @@ -3,8 +3,6 @@ // Imports: init.data.array.basic init.data.list.basic init.data.option.basic init.data.hashable #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -29,6 +27,7 @@ obj* l_hashmap_size___rarg(obj*); obj* l_hashmap__imp_find__aux___main___rarg(obj*, obj*, obj*); obj* l_hashmap_size(obj*, obj*, obj*, obj*); obj* l_d__hashmap_insert___rarg(obj*, obj*, obj*, obj*, obj*); +obj* l_nat_add(obj*, obj*); obj* l_hashmap__imp_replace__aux___main(obj*, obj*); obj* l_hashmap_empty(obj*, obj*, obj*, obj*); obj* l_hashmap__imp_erase___rarg(obj*, obj*, obj*, obj*); @@ -59,10 +58,15 @@ obj* l_mk__hashmap(obj*, obj*, obj*, obj*); obj* l_hashmap__imp_find(obj*, obj*); obj* l_hashmap__imp_find__aux___rarg(obj*, obj*, obj*); obj* l_mk__d__hashmap(obj*, obj*, obj*, obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_hashmap__imp_fold__buckets___rarg___lambda__1(obj*, obj*, obj*); obj* l_hashmap_fold___rarg(obj*, obj*, obj*); obj* l_d__hashmap_find(obj*, obj*); obj* l_d__hashmap_size___rarg(obj*); +uint8 l_nat_dec__le(obj*, obj*); +namespace lean { +usize usize_modn(usize, obj*); +} obj* l_array_foldl___rarg(obj*, obj*, obj*); obj* l_bucket__array_uwrite___rarg(obj*, usize, obj*, obj*); obj* l_hashmap_insert(obj*, obj*); @@ -87,7 +91,9 @@ obj* l_d__hashmap; obj* l_hashmap__imp_replace__aux(obj*, obj*); obj* l_hashmap_contains(obj*, obj*); obj* l_bucket__array; +obj* l_nat_mul(obj*, obj*); obj* l_hashmap; +obj* l_nat_sub(obj*, obj*); obj* l_hashmap_erase___rarg(obj*, obj*, obj*, obj*); obj* l_d__hashmap_contains___rarg___boxed(obj*, obj*, obj*, obj*); obj* l_hashmap__imp_find___rarg(obj*, obj*, obj*, obj*); diff --git a/src/boot/init/data/int/basic.cpp b/src/boot/init/data/int/basic.cpp index d46e153d65..53cd8e35f5 100644 --- a/src/boot/init/data/int/basic.cpp +++ b/src/boot/init/data/int/basic.cpp @@ -3,8 +3,6 @@ // Imports: init.data.nat.basic init.data.list.default init.coe init.data.repr init.data.to_string #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -18,15 +16,39 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #endif obj* l_int_repr(obj*); obj* l_int_has__repr; +namespace lean { +obj* nat_abs(obj*); +} +namespace lean { +obj* nat2int(obj*); +} obj* l_int_neg__of__nat(obj*); +namespace lean { +uint8 int_dec_nonneg(obj*); +} obj* l_int_has__sub; +namespace lean { +obj* int_neg_succ_of_nat(obj*); +} +obj* l_nat_add(obj*, obj*); +obj* l_nat_mod(obj*, obj*); obj* l_int_add___boxed(obj*, obj*); +namespace lean { +uint8 int_dec_le(obj*, obj*); +} obj* l_int_neg___boxed(obj*); obj* l_int_repr___main(obj*); obj* l_int_div___boxed(obj*, obj*); +namespace lean { +obj* int_mod(obj*, obj*); +} obj* l_int_to__nat___main(obj*); +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_int_sub___boxed(obj*, obj*); obj* l_int_has__mul; +uint8 l_nat_dec__eq(obj*, obj*); obj* l_int_lt; obj* l_int_neg__of__nat___main(obj*); obj* l_int_has__lt; @@ -34,10 +56,17 @@ obj* l_int_int_decidable__eq; obj* l_int_nat__abs___boxed(obj*); obj* l_int_sub__nat__nat(obj*, obj*); obj* l_int_dec__lt___boxed(obj*, obj*); +namespace lean { +obj* int_add(obj*, obj*); +} obj* l_int_zero; obj* l_int_has__div; obj* l_int_div___main(obj*, obj*); +namespace lean { +obj* int_sub(obj*, obj*); +} obj* l_int_has__mod; +obj* l_nat_div(obj*, obj*); obj* l_int_sign(obj*); obj* l_int_repr___main___closed__1; obj* l_int_to__nat(obj*); @@ -45,11 +74,17 @@ obj* l_int_dec__eq___boxed(obj*, obj*); obj* l_int_has__coe(obj*); obj* l_int_has__le; obj* l_int_has__one; +namespace lean { +obj* int_div(obj*, obj*); +} obj* l_int_nat__mod(obj*, obj*); obj* l_int_mod___boxed(obj*, obj*); obj* l___private_init_data_int_basic_2__dec__nonneg___boxed(obj*); obj* l_int_has__neg; obj* l___private_init_data_int_basic_1__nonneg; +namespace lean { +obj* int_neg(obj*); +} obj* l_int_repr___main___closed__2; obj* l_int_has__to__string; obj* l_int_mod___main(obj*, obj*); @@ -58,10 +93,20 @@ obj* l_int_mul___boxed(obj*, obj*); obj* l_int_sign___main(obj*); obj* l_int_has__add; obj* l_int_le; +obj* l_nat_sub(obj*, obj*); obj* l_int_has__zero; obj* l_int_dec__le___boxed(obj*, obj*); obj* l_int_sign___main___closed__1; +namespace lean { +obj* int_mul(obj*, obj*); +} +namespace lean { +uint8 int_dec_lt(obj*, obj*); +} obj* l_int_one; +namespace lean { +uint8 int_dec_eq(obj*, obj*); +} obj* l_int_has__coe(obj* x_0) { _start: { diff --git a/src/boot/init/data/int/default.cpp b/src/boot/init/data/int/default.cpp index 642b68ffb1..e4154fd6dd 100644 --- a/src/boot/init/data/int/default.cpp +++ b/src/boot/init/data/int/default.cpp @@ -3,8 +3,6 @@ // Imports: init.data.int.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/list/basic.cpp b/src/boot/init/data/list/basic.cpp index cb39a0493c..a81f8f33b6 100644 --- a/src/boot/init/data/list/basic.cpp +++ b/src/boot/init/data/list/basic.cpp @@ -3,8 +3,6 @@ // Imports: init.core init.data.nat.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -48,6 +46,7 @@ obj* l_list_length__aux___rarg(obj*, obj*); obj* l_list_union(obj*); obj* l_list_bag__inter___rarg(obj*, obj*, obj*); obj* l___private_init_data_list_basic_1__to__list__aux___main(obj*); +obj* l_nat_add(obj*, obj*); obj* l_list_bor(obj*); obj* l_list_has__dec__eq___main___rarg___boxed(obj*, obj*, obj*); obj* l_list_assoc___main(obj*, obj*); @@ -147,6 +146,7 @@ uint8 l_list_has__dec__eq___rarg(obj*, obj*, obj*); obj* l_list_foldr1__opt___rarg(obj*, obj*); obj* l_list_remove__nth___main___rarg(obj*, obj*); uint8 l_list_has__decidable__lt___main___rarg(obj*, obj*, obj*, obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_list_filter(obj*, obj*); obj* l_list_ilast___main___rarg(obj*, obj*); obj* l_list_head___main___rarg(obj*, obj*); @@ -244,6 +244,7 @@ obj* l_list_foldl___rarg(obj*, obj*, obj*); obj* l_list_foldr1___main(obj*); obj* l_list_foldr___main___at_list_union___spec__1___rarg(obj*, obj*, obj*); obj* l_list_length__aux___main(obj*); +obj* l_nat_sub(obj*, obj*); obj* l_list_reverse__core___main___rarg(obj*, obj*); obj* l_list_is__prefix__of___rarg(obj*, obj*, obj*); obj* l_list_take___rarg(obj*, obj*); diff --git a/src/boot/init/data/list/default.cpp b/src/boot/init/data/list/default.cpp index 2b7ab70b22..2dec6c8b2b 100644 --- a/src/boot/init/data/list/default.cpp +++ b/src/boot/init/data/list/default.cpp @@ -3,8 +3,6 @@ // Imports: init.data.list.basic init.data.list.instances #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/list/instances.cpp b/src/boot/init/data/list/instances.cpp index 0e8aaf3afe..42e39cfe08 100644 --- a/src/boot/init/data/list/instances.cpp +++ b/src/boot/init/data/list/instances.cpp @@ -3,8 +3,6 @@ // Imports: init.data.list.basic init.control.alternative init.control.monad #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/nat/basic.cpp b/src/boot/init/data/nat/basic.cpp index 38ff6c5f7b..98f81c355d 100644 --- a/src/boot/init/data/nat/basic.cpp +++ b/src/boot/init/data/nat/basic.cpp @@ -3,8 +3,6 @@ // Imports: init.core #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -18,6 +16,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_add(obj*, obj*); obj* l_nat_mul___boxed(obj*, obj*); obj* l_nat_max(obj*, obj*); obj* l_nat_le__refl; @@ -32,10 +31,12 @@ obj* l_nat_repeat(obj*); obj* l_nat_pred___main(obj*); obj* l_nat_has__pow; obj* l_nat_ble(obj*, obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_nat_repeat__core___main(obj*); obj* l_nat_dec__eq___boxed(obj*, obj*); obj* l_nat_has__lt; obj* l_nat_has__mul; +uint8 l_nat_dec__le(obj*, obj*); obj* l_nat_lt_base; obj* l_nat_lt; obj* l_nat_pow___main(obj*, obj*); @@ -46,11 +47,14 @@ 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_mul(obj*, obj*); obj* l_nat_has__le; +obj* l_nat_sub(obj*, obj*); obj* l_nat_le; obj* l_nat_ble___main(obj*, obj*); obj* l_nat_le__refl___main; obj* l_nat_dec__lt___boxed(obj*, obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* l_nat_beq___main(obj* x_0, obj* x_1) { _start: { diff --git a/src/boot/init/data/nat/default.cpp b/src/boot/init/data/nat/default.cpp index ce019e711e..7ef2b95279 100644 --- a/src/boot/init/data/nat/default.cpp +++ b/src/boot/init/data/nat/default.cpp @@ -3,8 +3,6 @@ // Imports: init.data.nat.basic init.data.nat.div #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/nat/div.cpp b/src/boot/init/data/nat/div.cpp index d46486e184..0c22233692 100644 --- a/src/boot/init/data/nat/div.cpp +++ b/src/boot/init/data/nat/div.cpp @@ -3,8 +3,6 @@ // Imports: init.wf init.data.nat.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -17,12 +15,18 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #pragma GCC diagnostic ignored "-Wunused-but-set-variable" #endif obj* l_nat_mod___boxed(obj*, obj*); +obj* l_nat_add(obj*, obj*); +obj* l_nat_mod(obj*, obj*); obj* l___private_init_data_nat_div_5__mod_F(obj*, obj*, obj*); obj* l_nat_has__div; obj* l___private_init_data_nat_div_2__div_F(obj*, obj*, obj*); obj* l___private_init_data_nat_div_1__div__rec__lemma; +uint8 l_nat_dec__le(obj*, obj*); +obj* l_nat_div(obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l_nat_has__mod; obj* l_nat_div___boxed(obj*, obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* _init_l___private_init_data_nat_div_1__div__rec__lemma() { _start: { diff --git a/src/boot/init/data/option/basic.cpp b/src/boot/init/data/option/basic.cpp index a7841c056d..f6db1da627 100644 --- a/src/boot/init/data/option/basic.cpp +++ b/src/boot/init/data/option/basic.cpp @@ -3,8 +3,6 @@ // Imports: init.core init.control.monad init.control.alternative init.coe #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/option/instances.cpp b/src/boot/init/data/option/instances.cpp index d523028070..8ec843db70 100644 --- a/src/boot/init/data/option/instances.cpp +++ b/src/boot/init/data/option/instances.cpp @@ -3,8 +3,6 @@ // Imports: init.data.option.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/ordering/basic.cpp b/src/boot/init/data/ordering/basic.cpp index 83139702b6..3fc8164423 100644 --- a/src/boot/init/data/ordering/basic.cpp +++ b/src/boot/init/data/ordering/basic.cpp @@ -3,8 +3,6 @@ // Imports: init.data.repr #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/ordering/default.cpp b/src/boot/init/data/ordering/default.cpp index bde2b2d4e4..17f887f1de 100644 --- a/src/boot/init/data/ordering/default.cpp +++ b/src/boot/init/data/ordering/default.cpp @@ -3,8 +3,6 @@ // Imports: init.data.ordering.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/rbmap/basic.cpp b/src/boot/init/data/rbmap/basic.cpp index 9d03faf445..01807a2f7d 100644 --- a/src/boot/init/data/rbmap/basic.cpp +++ b/src/boot/init/data/rbmap/basic.cpp @@ -3,8 +3,6 @@ // Imports: init.data.ordering.basic init.coe init.data.option.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -35,6 +33,7 @@ obj* l_rbnode_ins___main___at_rbmap_of__list___main___spec__3___rarg(obj*, obj*, obj* l_rbmap_mfold___main(obj*, obj*, obj*, obj*, obj*); obj* l_rbmap_max___main___rarg(obj*); obj* l_rbnode_all___rarg(obj*, obj*); +obj* l_nat_add(obj*, obj*); obj* l_rbmap; obj* l_rbmap_insert___main___rarg(obj*, obj*, obj*, obj*); obj* l_list_repr__aux___main___at_rbmap_has__repr___spec__2___rarg(obj*, obj*, uint8, obj*); @@ -86,6 +85,9 @@ obj* l_rbnode_insert___at_rbmap__of___spec__3(obj*, obj*, obj*); obj* l_rbnode_lower__bound___main___rarg(obj*, obj*, obj*, obj*); obj* l_rbmap_empty___main(obj*, obj*, obj*); obj* l_rbnode_find___main___at_rbmap_find___main___spec__1(obj*, obj*); +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_rbnode_balance2__node___rarg(obj*, obj*, obj*, obj*); obj* l_rbmap_contains(obj*, obj*, obj*); obj* l_rbmap_empty___main___rarg___boxed(obj*); diff --git a/src/boot/init/data/rbmap/default.cpp b/src/boot/init/data/rbmap/default.cpp index c026fae0be..5bed4231df 100644 --- a/src/boot/init/data/rbmap/default.cpp +++ b/src/boot/init/data/rbmap/default.cpp @@ -3,8 +3,6 @@ // Imports: init.data.rbtree.default init.data.rbmap.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/rbtree/basic.cpp b/src/boot/init/data/rbtree/basic.cpp index d8cfc5c154..ec5fb700d9 100644 --- a/src/boot/init/data/rbtree/basic.cpp +++ b/src/boot/init/data/rbtree/basic.cpp @@ -3,8 +3,6 @@ // Imports: init.data.rbmap.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -67,6 +65,9 @@ obj* l_rbmap_find__core___main___at_rbtree_contains___spec__2___rarg(obj*, obj*, obj* l_rbnode_all___main___at_rbtree_subset___spec__4(obj*, obj*); obj* l_rbtree_empty___rarg___boxed(obj*); obj* l_rbnode_insert___at_rbtree_of__list___main___spec__2(obj*, obj*); +namespace lean { +obj* string_append(obj*, obj*); +} uint8 l_option_to__bool___main___rarg(obj*); obj* l_rbtree_subset___at_rbtree_seteq___spec__6(obj*, obj*); obj* l_rbtree_find___at_rbtree_seteq___spec__7(obj*, obj*); diff --git a/src/boot/init/data/rbtree/default.cpp b/src/boot/init/data/rbtree/default.cpp index a5b413e895..874124000a 100644 --- a/src/boot/init/data/rbtree/default.cpp +++ b/src/boot/init/data/rbtree/default.cpp @@ -3,8 +3,6 @@ // Imports: init.data.rbtree.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/repr.cpp b/src/boot/init/data/repr.cpp index 818f4f0f18..4a32284d23 100644 --- a/src/boot/init/data/repr.cpp +++ b/src/boot/init/data/repr.cpp @@ -3,8 +3,6 @@ // Imports: init.data.string.basic init.data.uint init.data.usize init.data.nat.div #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -26,9 +24,13 @@ obj* l_string_quote__aux(obj*); obj* l_string_iterator_has__repr___closed__1; obj* l_nat_digit__char___closed__29; obj* l_nat_digit__char___closed__15; +namespace lean { +obj* uint16_to_nat(uint16); +} obj* l_option_has__repr___rarg___closed__2; obj* l_id_has__repr___rarg(obj*); obj* l_string_has__repr; +obj* l_nat_add(obj*, obj*); obj* l_nat_digit__char___closed__5; obj* l_fin_has__repr(obj*); obj* l_nat_digit__char___closed__14; @@ -37,6 +39,7 @@ obj* l_nat_digit__char___closed__30; obj* l_nat_digit__char___closed__16; obj* l_uint32_has__repr(uint32); obj* l_unit_has__repr___closed__1; +obj* l_nat_mod(obj*, obj*); obj* l_nat_digit__char___closed__38; obj* l_list_repr__aux___main(obj*); obj* l_nat_digit__char___closed__1; @@ -59,6 +62,9 @@ obj* l_list_repr___main___rarg___closed__1; obj* l_option_has__repr(obj*); obj* l_nat_digit__char___closed__34; obj* l_hex__digit__repr(obj*); +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_char_quote__core___closed__2; obj* l_usize_has__repr___boxed(obj*); obj* l_string_quote__aux___main(obj*); @@ -72,12 +78,19 @@ obj* l_sum_has__repr(obj*, obj*); obj* l_nat_digit__char___closed__28; obj* l_nat_digit__char___closed__18; obj* l_char_quote__core___closed__4; +namespace lean { +obj* string_data(obj*); +} obj* l_list_repr__aux___main___rarg___closed__1; obj* l_char_has__repr___boxed(obj*); obj* l_char_quote__core___closed__5; obj* l_string_iterator_has__repr(obj*); obj* l_nat_digit__char___closed__8; obj* l_list_repr___main___rarg___closed__3; +uint8 l_nat_dec__eq(obj*, obj*); +namespace lean { +obj* string_iterator_remaining_to_string(obj*); +} obj* l_char_has__repr___closed__1; obj* l_nat_digit__char___closed__7; obj* l_decidable_has__repr(obj*); @@ -86,6 +99,10 @@ obj* l_bool_has__repr(uint8); obj* l_list_repr___rarg(obj*, obj*); obj* l_nat_digit__char___closed__47; extern obj* l_string_join___closed__1; +uint8 l_nat_dec__le(obj*, obj*); +namespace lean { +obj* uint32_to_nat(uint32); +} obj* l_list_has__repr(obj*); obj* l_char__to__hex___boxed(obj*); obj* l_nat_digit__char___closed__12; @@ -95,8 +112,12 @@ obj* l_nat_digit__char___closed__44; obj* l_nat_digit__char___closed__32; obj* l_uint64_has__repr(uint64); obj* l_string_quote___closed__2; +namespace lean { +obj* string_mk(obj*); +} obj* l_nat_digit__char___closed__51; obj* l_list_repr__aux___main___rarg___boxed(obj*, obj*, obj*); +obj* l_nat_div(obj*, obj*); obj* l_char_quote__core___closed__3; obj* l_char_repr___boxed(obj*); obj* l_char_has__repr(uint32); @@ -113,6 +134,9 @@ obj* l_sigma_has__repr___rarg(obj*, obj*, obj*); obj* l_uint32_has__repr___boxed(obj*); obj* l_uint64_has__repr___boxed(obj*); obj* l_subtype_has__repr___rarg(obj*, obj*); +namespace lean { +obj* uint64_to_nat(uint64); +} obj* l_nat_digit__char___closed__49; obj* l_nat_digit__char___closed__46; obj* l_decidable_has__repr___rarg(uint8); @@ -135,20 +159,28 @@ obj* l_nat_digit__char___closed__25; obj* l_nat_digit__char___closed__48; obj* l_nat_digit__char___closed__4; obj* l_char__to__hex(uint32); +obj* l_nat_sub(obj*, obj*); obj* l_nat_digit__char___closed__31; obj* l_option_has__repr___rarg___closed__3; obj* l_nat_digit__char___closed__13; +namespace lean { +obj* string_push(obj*, uint32); +} obj* l_nat_to__digits__core___main(obj*, obj*, obj*, obj*); obj* l_unit_has__repr(obj*); obj* l_nat_digit__char___closed__26; obj* l_nat_digit__char___closed__42; obj* l_nat_digit__char___closed__17; obj* l_nat_digit__char___closed__10; +namespace lean { +obj* usize_to_nat(usize); +} obj* l_char_quote__core(uint32); obj* l_nat_digit__char___closed__20; obj* l_list_repr__aux___main___rarg(obj*, uint8, obj*); obj* l_nat_digit__char___closed__39; obj* l_nat_digit__char___closed__33; +uint8 l_nat_dec__lt(obj*, obj*); obj* l_nat_digit__char___closed__6; obj* l_nat_digit__char___closed__21; obj* l_uint16_has__repr___boxed(obj*); diff --git a/src/boot/init/data/string/basic.cpp b/src/boot/init/data/string/basic.cpp index 911866e229..2e00f50f83 100644 --- a/src/boot/init/data/string/basic.cpp +++ b/src/boot/init/data/string/basic.cpp @@ -3,8 +3,6 @@ // Imports: init.data.list.basic init.data.char.basic init.data.option.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -21,13 +19,20 @@ 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*); +namespace lean { +obj* string_iterator_prev_to_string(obj*); +} uint32 l_string_front(obj*); uint8 l_char_is__whitespace(uint32); obj* l___private_init_data_string_basic_2__trim__right__aux(obj*, obj*); obj* l_string_iterator_prev__to__string___boxed(obj*); obj* l___private_init_data_string_basic_1__trim__left__aux___main(obj*, obj*); obj* l_string_pushn___boxed(obj*, obj*, obj*); +obj* l_nat_add(obj*, obj*); obj* l_string_has__lt; +namespace lean { +obj* string_iterator_fst(obj*); +} obj* l_string_iterator_remaining___boxed(obj*); obj* l_string_iterator_forward(obj*, obj*); obj* l_string_iterator_extract___main___closed__1; @@ -47,26 +52,60 @@ uint8 l_string_iterator_has__prev___main(obj*); obj* l_nat_repeat__core___main___at_string_pushn___spec__1(uint32, obj*, obj*, obj*); obj* l_string_iterator_extract__core(obj*, obj*); obj* l_string_back___boxed(obj*); +namespace lean { +obj* string_iterator_next(obj*); +} obj* l_string_singleton___boxed(obj*); +namespace lean { +obj* string_length(obj*); +} 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*); +namespace lean { +uint32 string_iterator_curr(obj*); +} +namespace lean { +obj* string_iterator_set_curr(obj*, uint32); +} +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_string_iterator_insert___boxed(obj*, obj*); obj* l___private_init_data_string_basic_4__to__nat__core(obj*, obj*, obj*); obj* l_string_pop__back(obj*); obj* l_string_intercalate(obj*, obj*); +namespace lean { +uint8 string_dec_lt(obj*, obj*); +} obj* l_char_to__string___boxed(obj*); +namespace lean { +obj* string_iterator_to_end(obj*); +} obj* l_string_iterator_remaining___main(obj*); obj* l_string_iterator_curr___boxed(obj*); +namespace lean { +obj* string_iterator_extract(obj*, obj*); +} 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*); +namespace lean { +obj* string_data(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*); +namespace lean { +uint8 string_iterator_has_next(obj*); +} +uint8 l_nat_dec__eq(obj*, obj*); +namespace lean { +obj* string_iterator_remaining_to_string(obj*); +} obj* l_string_line__column(obj*, obj*); obj* l_string_iterator_set__curr___main(obj*, uint32); obj* l_string_iterator_nextn___main(obj*, obj*); @@ -84,9 +123,21 @@ obj* l___private_init_data_string_basic_3__line__column__aux(obj*, obj*, obj*); obj* l_string_iterator_insert___main(obj*, obj*); obj* l___private_init_data_string_basic_3__line__column__aux___main(obj*, obj*, obj*); obj* l_string_has__append; +namespace lean { +obj* string_iterator_prev(obj*); +} obj* l_string_iterator_prevn___main(obj*, obj*); +namespace lean { +obj* string_iterator_remove(obj*, obj*); +} obj* l_string_popn__back(obj*, obj*); obj* l_list_intercalate___rarg(obj*, obj*); +namespace lean { +obj* string_iterator_offset(obj*); +} +namespace lean { +obj* string_mk(obj*); +} obj* l_string_inhabited; obj* l_string_join(obj*); uint8 l_string_iterator_decidable__rel(obj*, obj*); @@ -97,11 +148,26 @@ 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*); obj* l_string_iterator_nextn(obj*, obj*); +namespace lean { +uint8 string_dec_eq(obj*, obj*); +} obj* l_string_trim__right(obj*); obj* l_string_iterator_extract__core___main(obj*, obj*); +namespace lean { +obj* string_iterator_insert(obj*, obj*); +} obj* l_string_push___main(obj*, uint32); obj* l_char_to__string(uint32); +namespace lean { +obj* string_iterator_remaining(obj*); +} +namespace lean { +obj* string_mk_iterator(obj*); +} obj* l_list_map___main___at_string_intercalate___spec__1(obj*); +namespace lean { +obj* string_iterator_mk(obj*, obj*); +} obj* l_list_length__aux___main___rarg(obj*, obj*); obj* l_string_has__sizeof; obj* l_string_to__list(obj*); @@ -113,19 +179,34 @@ obj* l_nat_repeat__core___main___at_string_pushn___spec__1___boxed(obj*, obj*, o 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_nat_mul(obj*, obj*); obj* l___private_init_data_string_basic_4__to__nat__core___main(obj*, obj*, obj*); obj* l_string_is__empty___boxed(obj*); +namespace lean { +uint8 string_iterator_has_prev(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_nat_sub(obj*, obj*); obj* l_string_trim__left(obj*); +namespace lean { +obj* string_push(obj*, uint32); +} 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*); +namespace lean { +obj* string_iterator_to_string(obj*); +} obj* l_string_iterator_next___main(obj*); obj* l_string_iterator_has__prev___boxed(obj*); obj* l_string_dec__lt___boxed(obj*, obj*); +namespace lean { +obj* string_iterator_snd(obj*); +} +uint8 l_nat_dec__lt(obj*, obj*); obj* l_string_length___main(obj*); obj* l_string_dec__eq___boxed(obj* x_0, obj* x_1) { _start: diff --git a/src/boot/init/data/string/default.cpp b/src/boot/init/data/string/default.cpp index e23e081ac5..3391dafe24 100644 --- a/src/boot/init/data/string/default.cpp +++ b/src/boot/init/data/string/default.cpp @@ -3,8 +3,6 @@ // Imports: init.data.string.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/data/to_string.cpp b/src/boot/init/data/to_string.cpp index 6f616495d6..a56acaf0f1 100644 --- a/src/boot/init/data/to_string.cpp +++ b/src/boot/init/data/to_string.cpp @@ -3,8 +3,6 @@ // Imports: init.data.string.basic init.data.uint init.data.nat.div init.data.repr #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -18,6 +16,9 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #endif obj* l_list_to__string__aux(obj*); obj* l_list_to__string__aux___main___rarg(obj*, uint8, obj*); +namespace lean { +obj* uint16_to_nat(uint16); +} obj* l_usize_has__to__string___boxed(obj*); obj* l_char_has__to__string(uint32); extern obj* l_option_has__repr___rarg___closed__2; @@ -43,6 +44,9 @@ obj* l_id_has__to__string___rarg(obj*); extern obj* l_list_repr___main___rarg___closed__1; obj* l_option_has__to__string___rarg(obj*, obj*); obj* l_fin_has__to__string(obj*); +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_uint16_has__to__string___boxed(obj*); obj* l_list_has__to__string(obj*); obj* l_list_to__string___main(obj*); @@ -52,11 +56,17 @@ obj* l_option_has__to__string(obj*); extern obj* l_sum_has__repr___rarg___closed__2; extern obj* l_list_repr__aux___main___rarg___closed__1; extern obj* l_list_repr___main___rarg___closed__3; +namespace lean { +obj* string_iterator_remaining_to_string(obj*); +} obj* l_list_to__string___rarg(obj*, obj*); obj* l_list_has__to__string___rarg(obj*); obj* l_uint32_has__to__string(uint32); obj* l_decidable_has__to__string___rarg(uint8); extern obj* l_string_join___closed__1; +namespace lean { +obj* uint32_to_nat(uint32); +} obj* l_uint64_has__to__string(uint64); extern obj* l_sigma_has__repr___rarg___closed__1; obj* l_uint64_has__to__string___boxed(obj*); @@ -66,6 +76,9 @@ extern obj* l_list_repr___main___rarg___closed__2; extern obj* l_bool_has__repr___closed__2; obj* l_usize_has__to__string(usize); extern obj* l_prod_has__repr___rarg___closed__1; +namespace lean { +obj* uint64_to_nat(uint64); +} obj* l_id_has__to__string(obj*); obj* l_bool_has__to__string___boxed(obj*); extern obj* l_bool_has__repr___closed__1; @@ -75,7 +88,13 @@ extern obj* l_sigma_has__repr___rarg___closed__2; obj* l_list_to__string__aux___main(obj*); obj* l_sigma_has__to__string___rarg(obj*, obj*, obj*); extern obj* l_option_has__repr___rarg___closed__3; +namespace lean { +obj* string_push(obj*, uint32); +} obj* l_subtype_has__to__string___rarg(obj*, obj*); +namespace lean { +obj* usize_to_nat(usize); +} obj* l_subtype_has__to__string(obj*, obj*); obj* l_decidable_has__to__string___rarg___boxed(obj*); obj* l_id_has__to__string___rarg(obj* x_0) { diff --git a/src/boot/init/data/uint.cpp b/src/boot/init/data/uint.cpp index 6442e3241b..b8c4031697 100644 --- a/src/boot/init/data/uint.cpp +++ b/src/boot/init/data/uint.cpp @@ -3,8 +3,6 @@ // Imports: init.data.fin.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -18,15 +16,22 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #endif obj* l_uint32_mul___boxed(obj*, obj*); obj* l_uint8_div___boxed(obj*, obj*); +namespace lean { +uint64 uint64_modn(uint64, obj*); +} obj* l_uint8_has__le; obj* l_uint16_inhabited___boxed; obj* l_uint32_has__decidable__le___boxed(obj*, obj*); +uint64 l_uint64_mul(uint64, uint64); uint8 l_uint32_has__decidable__lt(uint32, uint32); uint8 l_uint8_has__decidable__lt(uint8, uint8); obj* l_uint64_has__sub; obj* l_uint8_inhabited___boxed; obj* l_uint8_mod___boxed(obj*, obj*); obj* l_uint32_lt; +namespace lean { +obj* uint16_to_nat(uint16); +} obj* l_uint16_has__decidable__le___boxed(obj*, obj*); obj* l_uint16_sub___boxed(obj*, obj*); obj* l_uint16_has__sub; @@ -37,6 +42,7 @@ obj* l_uint64_add___boxed(obj*, obj*); obj* l_uint16_has__decidable__lt___boxed(obj*, obj*); obj* l_uint8_add___boxed(obj*, obj*); obj* l_uint16_dec__lt___boxed(obj*, obj*); +uint16 l_uint16_sub(uint16, uint16); obj* l_uint64_inhabited___boxed; obj* l_uint16_has__add; uint8 l_uint32_has__decidable__le(uint32, uint32); @@ -44,30 +50,47 @@ uint32 l_uint32_inhabited; obj* l_uint32_decidable__eq; obj* l_uint32_has__mul; obj* l_uint64_div___boxed(obj*, obj*); +uint8 l_uint32_dec__le(uint32, uint32); obj* l_uint64_dec__eq___boxed(obj*, obj*); uint8 l_uint64_has__decidable__lt(uint64, uint64); obj* l_uint32_has__sub; uint8 l_uint8_inhabited; obj* l_uint16_add___boxed(obj*, obj*); +uint16 l_uint16_add(uint16, uint16); +uint8 l_uint16_dec__le(uint16, uint16); +uint64 l_uint64_mod(uint64, uint64); obj* l_uint16_modn___boxed(obj*, obj*); obj* l_uint32_mod___boxed(obj*, obj*); obj* l_uint32_has__lt; obj* l_uint32_has__zero___boxed; obj* l_uint16_has__le; +uint8 l_uint32_dec__lt(uint32, uint32); obj* l_uint32_sub___boxed(obj*, obj*); obj* l_uint32_has__div; obj* l_uint32_has__modn; obj* l_uint64_has__decidable__le___boxed(obj*, obj*); obj* l_uint8__sz; +namespace lean { +uint32 uint32_modn(uint32, obj*); +} obj* l_uint64_has__mul; +namespace lean { +uint8 uint8_modn(uint8, obj*); +} obj* l_uint8_has__decidable__le___boxed(obj*, obj*); uint8 l_uint16_has__decidable__lt(uint16, uint16); uint64 l_uint64_inhabited; +uint8 l_uint8_div(uint8, uint8); uint64 l_uint64_has__zero; obj* l_uint8_has__mod; +uint64 l_uint64_div(uint64, uint64); obj* l_uint16_div___boxed(obj*, obj*); +uint16 l_uint16_mul(uint16, uint16); uint8 l_uint8_has__one; obj* l_uint64_of__nat___boxed(obj*); +namespace lean { +uint16 uint16_of_nat(obj*); +} obj* l_uint16_has__zero___boxed; obj* l_uint8_has__zero___boxed; obj* l_uint8_has__decidable__lt___boxed(obj*, obj*); @@ -77,12 +100,17 @@ obj* l_uint8_has__add; obj* l_uint8_le; obj* l_uint8_lt; obj* l_uint8_has__mul; +uint8 l_uint8_dec__eq(uint8, uint8); obj* l_uint8_has__modn; obj* l_uint8_dec__le___boxed(obj*, obj*); obj* l_uint32_has__mod; obj* l_uint8_to__nat___boxed(obj*); +namespace lean { +uint16 uint16_modn(uint16, obj*); +} obj* l_uint64_mul___boxed(obj*, obj*); obj* l_uint16_to__nat___boxed(obj*); +uint64 l_uint64_add(uint64, uint64); obj* l_uint16_has__lt; obj* l_uint8_has__sub; uint32 l_uint32_has__zero; @@ -94,31 +122,53 @@ uint16 l_uint16_inhabited; obj* l_uint32_le; obj* l_uint16_has__modn; obj* l_uint64__sz; +uint8 l_uint64_dec__lt(uint64, uint64); +namespace lean { +obj* uint32_to_nat(uint32); +} obj* l_uint8_of__nat___boxed(obj*); obj* l_uint8_has__div; uint64 l_uint64_has__one; +uint8 l_uint16_dec__lt(uint16, uint16); obj* l_uint16_decidable__eq; obj* l_uint64_dec__lt___boxed(obj*, obj*); obj* l_uint64_has__lt; obj* l_uint64_has__div; obj* l_uint16_mul___boxed(obj*, obj*); +uint8 l_uint8_mul(uint8, uint8); obj* l_uint16_le; obj* l_uint16_mod___boxed(obj*, obj*); obj* l_uint32_dec__eq___boxed(obj*, obj*); obj* l_uint64_has__one___boxed; +namespace lean { +uint64 uint64_of_nat(obj*); +} obj* l_uint64_lt; uint8 l_uint8_has__zero; obj* l_uint16_of__nat___boxed(obj*); obj* l_uint32_has__decidable__lt___boxed(obj*, obj*); obj* l_uint32_modn___boxed(obj*, obj*); +namespace lean { +obj* uint8_to_nat(uint8); +} obj* l_uint32_add___boxed(obj*, obj*); +uint32 l_uint32_mod(uint32, uint32); obj* l_uint64_has__le; obj* l_uint32_div___boxed(obj*, obj*); +uint32 l_uint32_div(uint32, uint32); +uint8 l_uint32_dec__eq(uint32, uint32); +namespace lean { +obj* uint64_to_nat(uint64); +} obj* l_uint16_has__one___boxed; +uint64 l_uint64_sub(uint64, uint64); obj* l_uint32_has__one___boxed; +uint32 l_uint32_mul(uint32, uint32); obj* l_uint64_has__decidable__lt___boxed(obj*, obj*); +uint8 l_uint8_add(uint8, uint8); obj* l_uint64_mod___boxed(obj*, obj*); obj* l_uint32_dec__lt___boxed(obj*, obj*); +uint16 l_uint16_mod(uint16, uint16); obj* l_uint16_dec__eq___boxed(obj*, obj*); obj* l_uint8_dec__eq___boxed(obj*, obj*); obj* l_uint16_dec__le___boxed(obj*, obj*); @@ -129,9 +179,18 @@ obj* l_uint8_has__lt; obj* l_uint8_dec__lt___boxed(obj*, obj*); obj* l_uint64_to__nat___boxed(obj*); obj* l_uint8_has__one___boxed; +uint8 l_uint64_dec__le(uint64, uint64); obj* l_uint16_has__mod; +uint8 l_uint8_mod(uint8, uint8); +uint8 l_uint8_sub(uint8, uint8); obj* l_uint64_modn___boxed(obj*, obj*); obj* l_uint8_modn___boxed(obj*, obj*); +namespace lean { +uint32 uint32_of_nat(obj*); +} +uint16 l_uint16_div(uint16, uint16); +uint8 l_uint8_dec__le(uint8, uint8); +uint32 l_uint32_sub(uint32, uint32); obj* l_uint32_inhabited___boxed; obj* l_uint64_le; obj* l_uint32_to__nat___boxed(obj*); @@ -142,12 +201,19 @@ obj* l_uint64_has__add; obj* l_uint64_has__zero___boxed; uint16 l_uint16_has__zero; uint8 l_uint8_has__decidable__le(uint8, uint8); +uint8 l_uint8_dec__lt(uint8, uint8); obj* l_uint32_dec__le___boxed(obj*, obj*); obj* l_uint64_dec__le___boxed(obj*, obj*); uint32 l_uint32_has__one; obj* l_uint64_sub___boxed(obj*, obj*); obj* l_uint32_has__add; uint8 l_uint64_has__decidable__le(uint64, uint64); +uint32 l_uint32_add(uint32, uint32); +namespace lean { +uint8 uint8_of_nat(obj*); +} +uint8 l_uint64_dec__eq(uint64, uint64); +uint8 l_uint16_dec__eq(uint16, uint16); obj* _init_l_uint8__sz() { _start: { diff --git a/src/boot/init/data/usize.cpp b/src/boot/init/data/usize.cpp index b5e8a6282f..4ea9f16dea 100644 --- a/src/boot/init/data/usize.cpp +++ b/src/boot/init/data/usize.cpp @@ -3,8 +3,6 @@ // Imports: init.data.uint init.platform init.data.fin.default #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -16,18 +14,23 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; #pragma GCC diagnostic ignored "-Wunused-label" #pragma GCC diagnostic ignored "-Wunused-but-set-variable" #endif +usize l_usize_div(usize, usize); obj* l_usize_has__add; obj* l_usize_has__modn; obj* l_usize_mod___boxed(obj*, obj*); obj* l_usize_has__le; obj* l_usize_dec__lt___boxed(obj*, obj*); +usize l_usize_mul(usize, usize); +uint8 l_usize_dec__lt(usize, usize); extern obj* l_system_platform_nbits; obj* l_usize_has__mod; +uint8 l_usize_dec__eq(usize, usize); uint8 l_usize_has__decidable__le(usize, usize); obj* l_usize_of__nat___boxed(obj*); obj* l_usize_has__div; obj* l_usize_dec__eq___boxed(obj*, obj*); obj* l_usize_dec__le___boxed(obj*, obj*); +usize l_usize_mod(usize, usize); obj* l_usize_has__zero___boxed; obj* l_usize_has__one___boxed; obj* l_usize_div___boxed(obj*, obj*); @@ -37,18 +40,30 @@ usize l_usize_inhabited; obj* l_usize_add___boxed(obj*, obj*); obj* l_usize_has__sub; usize l_usize_has__zero; +namespace lean { +usize usize_modn(usize, obj*); +} obj* l_usize_lt; usize l_usize_has__one; obj* l_usize_has__decidable__lt___boxed(obj*, obj*); +usize l_usize_add(usize, usize); obj* l_usize_has__lt; obj* l_nat_pow___main(obj*, obj*); obj* l_usize_mul___boxed(obj*, obj*); +namespace lean { +usize usize_of_nat(obj*); +} obj* l_usize__sz; obj* l_usize_le; obj* l_usize_has__decidable__le___boxed(obj*, obj*); uint8 l_usize_has__decidable__lt(usize, usize); +uint8 l_usize_dec__le(usize, usize); obj* l_usize_to__nat___boxed(obj*); obj* l_usize_inhabited___boxed; +usize l_usize_sub(usize, usize); +namespace lean { +obj* usize_to_nat(usize); +} obj* l_usize_has__mul; obj* l_usize_modn___boxed(obj*, obj*); obj* _init_l_usize__sz() { diff --git a/src/boot/init/default.cpp b/src/boot/init/default.cpp index c7cf3f596a..604bd43e34 100644 --- a/src/boot/init/default.cpp +++ b/src/boot/init/default.cpp @@ -3,8 +3,6 @@ // Imports: init.core init.control.default init.data.basic init.function init.coe init.wf init.data.default init.io #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/env_ext.cpp b/src/boot/init/env_ext.cpp index cba2ab8e9d..fb28b98a1e 100644 --- a/src/boot/init/env_ext.cpp +++ b/src/boot/init/env_ext.cpp @@ -3,8 +3,6 @@ // Imports: #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/function.cpp b/src/boot/init/function.cpp index 513212a555..714d700341 100644 --- a/src/boot/init/function.cpp +++ b/src/boot/init/function.cpp @@ -3,8 +3,6 @@ // Imports: init.core #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/io.cpp b/src/boot/init/io.cpp index d9f0a3651b..2f38eed8bf 100644 --- a/src/boot/init/io.cpp +++ b/src/boot/init/io.cpp @@ -3,8 +3,6 @@ // Imports: init.control.state init.control.except init.data.string.basic init.control.coroutine #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -29,6 +27,9 @@ 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*); +namespace lean { +obj* io_prim_handle_mk(obj*, uint8, uint8, 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*); @@ -44,6 +45,9 @@ obj* l_coroutine__io_resume___rarg(obj*, obj*, obj*); obj* l_io_prim_iterate___rarg(obj*, obj*, obj*); obj* l_id_monad___lambda__1(obj*, obj*, obj*, obj*); obj* l_io_has__eval___rarg(obj*, obj*, obj*); +namespace lean { +obj* io_prim_put_str(obj*, obj*); +} obj* l_io_prim_lift__eio___at_io_fs_handle_read__to__end___spec__7___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_io_prim_iterate___main___at_io_prim_iterate__eio___spec__1___rarg(obj*, obj*, obj*); obj* l_io_fs_handle_flush(obj*, obj*); @@ -67,6 +71,9 @@ obj* l_coroutine__io_monad___lambda__8(obj*, obj*, obj*, obj*); obj* l_coroutine__io_yield(obj*, obj*); obj* l_coroutine__io_read___rarg(obj*, obj*); obj* l_io_fs_handle_is__eof___rarg(obj*, obj*, obj*, obj*, obj*); +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_eio_has__eval(obj*, obj*); obj* l_io_print___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_coroutine__io_monad___lambda__4(obj*, obj*, obj*, obj*); @@ -84,6 +91,9 @@ obj* l_coroutine__io_monad___lambda__7(obj*, obj*, obj*, obj*); obj* l_coroutine__io_bind(obj*, obj*, obj*, obj*); obj* l_io_error_has__to__string; obj* l_io_prim_lift__eio___at_io_fs_handle_read__to__end___spec__4(obj*, obj*); +namespace lean { +obj* io_prim_handle_close(obj*, obj*); +} obj* l_io_fs_handle_mk___at_io_fs_read__file___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_coroutine__result__io; obj* l_monad__io; @@ -106,6 +116,9 @@ obj* l_io_fs_handle_close___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_coroutine__io_pure___rarg(obj*, obj*, obj*); obj* l_id_monad___lambda__3(obj*, obj*, obj*, obj*); obj* l_coroutine__io_yield___rarg___lambda__1(obj*, obj*); +namespace lean { +obj* io_prim_handle_flush(obj*, obj*); +} obj* l_io_fs_read__file___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_io_monad; obj* l_coroutine__io_read(obj*, obj*); @@ -118,6 +131,9 @@ obj* l_eio; obj* l_io_fs_handle_get__line___at_io_fs_handle_read__to__end___spec__3(obj*, obj*); obj* l_io_prim_lift__eio___at_io_fs_handle_is__eof___spec__1___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_eio_has__eval___rarg(obj*, obj*, obj*, obj*); +namespace lean { +obj* io_prim_get_line(obj*); +} obj* l_io_prim_lift__eio___at_io_fs_read__file___spec__2(obj*, obj*); obj* l_io_fs_handle_get__line___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_io_prim_lift__eio___at_io_fs_handle_read__to__end___spec__2(obj*, obj*); @@ -130,6 +146,9 @@ obj* l_coroutine__io_monad___lambda__5(obj*, obj*, obj*, obj*); obj* l_io_prim_lift__eio___at_io_fs_handle_get__line___spec__1(obj*, obj*); obj* l_coroutine__io_yield___rarg___closed__1; obj* l_io_prim_lift__eio___at_io_fs_handle_close___spec__1(obj*, obj*); +namespace lean { +obj* io_prim_handle_get_line(obj*, obj*); +} obj* l_io_prim_lift__eio___at_io_println___spec__2___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_io_fs_handle_mk(obj*, obj*); obj* l___private_init_io_10__put__str___rarg(obj*, obj*, obj*, obj*, obj*); @@ -151,6 +170,9 @@ obj* l_coroutine__io_pipe___rarg(obj*, obj*); obj* l_io_fs_handle_close(obj*, obj*); obj* l_coroutine__io_monad___lambda__1___closed__1; obj* l_io__unit_has__eval(obj*, obj*); +namespace lean { +obj* io_prim_handle_is_eof(obj*, obj*); +} obj* l_eio_has__eval___rarg___closed__1; obj* l_string_has__lift(obj*); obj* l_io_fs_handle_get__line(obj*, obj*); diff --git a/src/boot/init/lean/config.cpp b/src/boot/init/lean/config.cpp index 375106c1b3..f128d0b610 100644 --- a/src/boot/init/lean/config.cpp +++ b/src/boot/init/lean/config.cpp @@ -3,8 +3,6 @@ // Imports: init.core #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/lean/declaration.cpp b/src/boot/init/lean/declaration.cpp index fb5e290a93..10a752992f 100644 --- a/src/boot/init/lean/declaration.cpp +++ b/src/boot/init/lean/declaration.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.expr #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/lean/disjoint_set.cpp b/src/boot/init/lean/disjoint_set.cpp index 84c8f0bc58..2df9999b60 100644 --- a/src/boot/init/lean/disjoint_set.cpp +++ b/src/boot/init/lean/disjoint_set.cpp @@ -3,8 +3,6 @@ // Imports: init.data.hashmap.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -21,6 +19,7 @@ obj* l_lean_disjoint__set_merge(obj*); obj* l_d__hashmap_insert___at_lean_disjoint__set_merge___main___spec__4___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_hashmap__imp_insert___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_lean_disjoint__set_find___rarg(obj*, obj*, obj*, obj*); +obj* l_nat_add(obj*, obj*); obj* l___private_init_lean_disjoint__set_1__find__aux___main___rarg(obj*, obj*, obj*, obj*, obj*); obj* l___private_init_lean_disjoint__set_1__find__aux___main(obj*); obj* l_lean_disjoint__set_rank___main___rarg(obj*, obj*, obj*, obj*); @@ -29,6 +28,7 @@ obj* l_lean_disjoint__set_rank(obj*); obj* l_lean_disjoint__set_merge___main___rarg(obj*, obj*, obj*, obj*, obj*); obj* l___private_init_lean_disjoint__set_1__find__aux(obj*); obj* l_lean_disjoint__set_merge___main(obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_mk__disjoint__set___rarg(obj*, obj*); obj* l_d__hashmap_insert___at_lean_disjoint__set_merge___main___spec__2(obj*); obj* l_d__hashmap_insert___at_lean_disjoint__set_merge___main___spec__1___rarg(obj*, obj*, obj*, obj*, obj*); @@ -45,8 +45,10 @@ obj* l_lean_disjoint__set_merge___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_lean_disjoint__set_rank___rarg(obj*, obj*, obj*, obj*); obj* l_lean_disjoint__set_find(obj*); obj* l_d__hashmap_insert___at_lean_disjoint__set_merge___main___spec__4(obj*); +obj* l_nat_sub(obj*, obj*); obj* l_hashmap__imp_find___rarg(obj*, obj*, obj*, obj*); obj* l_lean_disjoint__set_find___main(obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* l_d__hashmap_insert___at_lean_disjoint__set_merge___main___spec__3(obj*); obj* l_mk__d__hashmap___at_lean_mk__disjoint__set___spec__1___rarg(obj* x_0) { _start: diff --git a/src/boot/init/lean/elaborator.cpp b/src/boot/init/lean/elaborator.cpp index b464596f24..5adf5c92d2 100644 --- a/src/boot/init/lean/elaborator.cpp +++ b/src/boot/init/lean/elaborator.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.parser.module init.lean.expander init.lean.expr init.lean.options #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -66,6 +64,7 @@ obj* l_lean_elaborator_run___closed__2; obj* l_lean_elaborator_end__scope___lambda__3___closed__1; obj* l_rbmap_insert___main___at_lean_elaborator_ordered__rbmap_insert___spec__1(obj*, obj*, obj*); extern obj* l_lean_parser_command_declaration; +obj* l_nat_add(obj*, obj*); obj* l_lean_elaborator_commands_elaborate___main___lambda__4___boxed(obj*, obj*, obj*, obj*, obj*); obj* l_list_mmap___main___at_lean_elaborator_command__parser__config_register__notation__parser___spec__2___closed__1; obj* l_lean_elaborator_to__level(obj*, obj*, obj*); @@ -115,6 +114,9 @@ obj* l_lean_elaborator_mk__eqns___closed__2; obj* l_lean_elaborator_locally___rarg___lambda__3(obj*, obj*, obj*); obj* l_list_reverse___rarg(obj*); obj* l_lean_elaborator_run___lambda__4(obj*, obj*, obj*, obj*, obj*); +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_lean_elaborator_to__pexpr___main___closed__31; obj* l_lean_elaborator_register__notation__macro(obj*, obj*, obj*); obj* l_lean_elaborator_section_elaborate___lambda__1(obj*, obj*, obj*, obj*); @@ -138,6 +140,8 @@ obj* l_lean_elaborator_mk__notation__kind___rarg(obj*); obj* l_rbnode_ins___main___at_lean_elaborator_ordered__rbmap_insert___spec__3___rarg(obj*, obj*, obj*, obj*); uint8 l_lean_parser_syntax_is__of__kind___main(obj*, obj*); obj* l_lean_elaborator_run___lambda__8(obj*); +obj* lean_expr_local(obj*, obj*, obj*, uint8); + extern obj* l_lean_expander_expand__bracketed__binder___main___closed__4; obj* l_lean_parser_term_simple__binder_view_to__binder__info___main(obj*); extern obj* l_lean_parser_command_set__option; @@ -196,6 +200,9 @@ 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*); +namespace lean { +obj* string_append(obj*, obj*); +} extern obj* l_lean_parser_command_reserve__notation; obj* l_lean_elaborator_commands_elaborate___main___lambda__3___boxed(obj*, obj*, obj*, obj*, obj*); obj* l_except__t_monad__except___rarg(obj*); @@ -307,6 +314,7 @@ extern obj* l_lean_message__log_empty; obj* l_list_mmap___main___at_lean_elaborator_to__pexpr___main___spec__11(obj*, obj*, obj*, obj*); obj* l_lean_elaborator_export_elaborate(obj*, obj*, obj*); obj* l_lean_elaborator_namespace_elaborate___lambda__2(obj*, obj*, obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_rbnode_ins___main___at_lean_elaborator_elaborators___spec__4(obj*, obj*, obj*); obj* l_lean_elaborator_to__pexpr___main___closed__38; obj* l_list_map___main___at_lean_elaborator_to__pexpr___main___spec__21(obj*); @@ -314,6 +322,8 @@ uint8 l_lean_elaborator_is__open__namespace___main(obj*, obj*); obj* l_rbnode_insert___at_lean_elaborator_old__elab__command___spec__17(obj*, obj*, obj*); obj* l_list_mmap___main___at_lean_elaborator_declaration_elaborate___spec__7(obj*, obj*, obj*); extern obj* l_char_has__repr___closed__1; +obj* lean_environment_mk_empty(obj*); + obj* l_list_filter___main___at_lean_elaborator_resolve__context___main___spec__1(obj*, obj*, obj*); obj* l_lean_elaborator_elaborator__t_monad__except(obj*); obj* l_coroutine_bind___main___rarg(obj*, obj*, obj*); @@ -452,11 +462,17 @@ extern obj* l_coroutine_monad___closed__1; obj* l_rbtree_of__list___main___at_lean_elaborator_old__elab__command___spec__15(obj*); obj* l_lean_elaborator_no__kind_elaborate___lambda__2(obj*, obj*, obj*); obj* l_lean_elaborator_module_header_elaborate(obj*, obj*, obj*); +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} obj* l_lean_parser_syntax_kind___main(obj*); obj* l_lean_elaborator_to__pexpr___main___closed__2; obj* l_lean_elaborator_section_elaborate(obj*, obj*, obj*); obj* l_lean_elaborator_namespace_elaborate___lambda__1(obj*, obj*, obj*, obj*); obj* l_lean_elaborator_preresolve(obj*, obj*, obj*); +namespace lean { +uint8 string_dec_eq(obj*, obj*); +} extern obj* l_lean_parser_module_header_has__view; obj* l_rbmap_from__list___at_lean_elaborator_elaborators___spec__1___lambda__26(obj*, obj*, obj*); uint8 l_list_foldr___main___at_lean_elaborator_notation_elaborate___spec__1(obj*); @@ -546,6 +562,9 @@ obj* l_list_map___main___at_lean_elaborator_mk__eqns___spec__1___closed__1; extern obj* l_lean_parser_level_leading_has__view_x_27___lambda__1___closed__5; obj* l_lean_elaborator_run___closed__7; obj* l_lean_kvmap_insert__core___main(obj*, obj*, obj*); +namespace lean { +obj* name_mk_numeral(obj*, obj*); +} obj* l_lean_elaborator_to__pexpr___main___closed__28; obj* l_lean_elaborator_to__level___main___closed__3; obj* l_lean_elaborator_locally___at_lean_elaborator_namespace_elaborate___spec__1___lambda__1(obj*, obj*, obj*); @@ -585,6 +604,7 @@ obj* l_lean_elaborator_elab__def__like___closed__2; extern obj* l_lean_parser_command_include_has__view; extern obj* l_lean_parser_command_namespace; obj* l_rbmap_insert___main___at_lean_elaborator_elaborators___spec__2(obj*, obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l_list_map___main___at_lean_elaborator_elab__def__like___spec__3(obj*); obj* l_lean_elaborator_old__elab__command(obj*, obj*, obj*, obj*); obj* l_list_map___main___at_lean_elaborator_declaration_elaborate___spec__13(obj*); @@ -592,6 +612,8 @@ obj* l_option_to__monad___main___at_lean_elaborator_command__parser__config_regi obj* l_lean_file__map_to__position(obj*, obj*); obj* l_lean_name_quick__lt___main(obj*, obj*); obj* l_state__t_lift___rarg(obj*, obj*, obj*, obj*); +obj* lean_elaborator_elaborate_command(obj*, obj*, obj*); + obj* l_dlist_singleton___rarg(obj*, obj*); obj* l_rbmap_from__list___at_lean_elaborator_elaborators___spec__1___lambda__20(obj*, obj*, obj*); extern obj* l_lean_expander_get__opt__type___main___closed__1; @@ -624,6 +646,8 @@ obj* l_lean_parser_string__lit_view_value(obj*); obj* l_lean_elaborator_commands_elaborate___main___lambda__4(obj*, obj*, uint8, obj*, obj*); obj* l_lean_elaborator_to__pexpr___main___closed__42; obj* l_lean_elaborator_yield__to__outside___rarg___lambda__2___closed__1; +uint8 lean_environment_contains(obj*, obj*); + obj* l_lean_expander_error___at_lean_elaborator_no__kind_elaborate___spec__1___rarg___lambda__1(obj*, obj*, obj*); extern obj* l_lean_parser_command_notation_has__view; extern obj* l_lean_parser_command_check; diff --git a/src/boot/init/lean/expander.cpp b/src/boot/init/lean/expander.cpp index f1a1811dcb..78586a0cde 100644 --- a/src/boot/init/lean/expander.cpp +++ b/src/boot/init/lean/expander.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.parser.module init.lean.expr #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -45,6 +43,7 @@ obj* l_lean_expander_if_transform(obj*, obj*); extern obj* l_lean_parser_command_declaration; obj* l_list_map___main___at_lean_expander_intro__rule_transform___spec__1(obj*); obj* l_lean_expander_universes_transform(obj*, obj*); +obj* l_nat_add(obj*, obj*); obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__20___boxed(obj*, obj*, obj*); obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__20(uint8, obj*, obj*); obj* l_lean_expander_variables_transform(obj*, obj*); @@ -69,6 +68,9 @@ obj* l_lean_parser_syntax_flip__scopes___main(obj*, obj*); obj* l_rbnode_ins___main___at_lean_expander_builtin__transformers___spec__4(obj*, obj*, obj*); obj* l_lean_expander_assume_transform___closed__1; obj* l_list_foldr___main___at_lean_expander_expand__binders___spec__7(obj*, obj*, obj*); +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__6(obj*, obj*); obj* l_lean_expander_binding__annotation__update_has__view; obj* l_coe___at_lean_expander_coe__binders__ext___spec__1(obj*); @@ -156,6 +158,7 @@ obj* l_rbmap_insert___main___at_lean_expander_builtin__transformers___spec__2(ob obj* l_lean_expander_lambda_transform___closed__1; extern obj* l_lean_parser_term_pi; extern obj* l_lean_parser_term_paren_has__view; +uint8 l_nat_dec__eq(obj*, obj*); extern obj* l_lean_parser_term__parser__m_lean_parser_monad__parsec; obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__3___closed__1; obj* l_id(obj*); @@ -225,6 +228,9 @@ obj* l_lean_expander_mixfix__to__notation__spec(obj*, obj*, obj*); obj* l_list_foldr___main___at_lean_expander_expand__binders___spec__1(obj*, obj*, obj*); obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__4___closed__1; obj* l_lean_expander_coe__binder__bracketed__binder___closed__1; +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} obj* l_list_map___main___at_lean_expander_expand__bracketed__binder___main___spec__18(obj*, obj*); obj* l_lean_expander_declaration_transform___closed__1; obj* l_lean_expander_coe__binders__ext__binders(obj*); @@ -284,6 +290,7 @@ obj* l_id_monad___lambda__2(obj*, obj*, obj*, obj*); obj* l_lean_expander_reserve__mixfix_transform(obj*, obj*); obj* l_list_foldr1___main___at_lean_expander_paren_transform___spec__3___closed__1; obj* l_lean_expander_level_leading_transform(obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l_lean_expander_binding__annotation__update_parser_lean_parser_has__view; obj* l_lean_expander_expander__m; obj* l_lean_file__map_to__position(obj*, obj*); diff --git a/src/boot/init/lean/expr.cpp b/src/boot/init/lean/expr.cpp index 4b83967d62..8f22723300 100644 --- a/src/boot/init/lean/expr.cpp +++ b/src/boot/init/lean/expr.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.level init.lean.kvmap #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/lean/extern.cpp b/src/boot/init/lean/extern.cpp index 255d25c9d4..173f77f742 100644 --- a/src/boot/init/lean/extern.cpp +++ b/src/boot/init/lean/extern.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.expr init.data.option.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -22,14 +20,33 @@ obj* l_lean_expand__extern__entry(obj*, obj*); namespace lean { obj* expand_extern_pattern_core(obj*, obj*); } +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_list_foldl___main___at_lean_mk__simple__fn__call___spec__1(obj*, obj*); namespace lean { +obj* string_iterator_next(obj*); +} +namespace lean { obj* mk_adhoc_ext_entry_core(obj*); } +namespace lean { +obj* string_length(obj*); +} +namespace lean { +uint32 string_iterator_curr(obj*); +} +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_lean_get__extern__entry__for__aux___main___closed__1; obj* l_option_get__or__else___main___rarg(obj*, obj*); extern obj* l_list_repr__aux___main___rarg___closed__1; namespace lean { +uint8 string_iterator_has_next(obj*); +} +uint8 l_nat_dec__eq(obj*, obj*); +namespace lean { obj* mk_std_ext_entry_core(obj*, obj*); } extern obj* l_string_join___closed__1; @@ -43,10 +60,16 @@ obj* mk_extern_call_core(obj*, obj*, obj*); } obj* l_list_intersperse___main___rarg(obj*, obj*); obj* l_lean_extern__entry_backend(obj*); +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} obj* l_lean_expand__extern__pattern__aux(obj*, obj*, obj*, obj*); extern obj* l_prod_has__repr___rarg___closed__1; obj* l_lean_extern__entry_backend___main(obj*); namespace lean { +obj* string_mk_iterator(obj*); +} +namespace lean { obj* mk_foreign_ext_entry_core(obj*, obj*); } namespace lean { @@ -54,10 +77,15 @@ obj* mk_extern_attr_data_core(obj*, obj*); } obj* l_lean_expand__extern__entry___main(obj*, obj*); obj* l_lean_mk__simple__fn__call(obj*, obj*); +obj* l_nat_sub(obj*, obj*); extern obj* l_option_has__repr___rarg___closed__3; namespace lean { +obj* string_push(obj*, uint32); +} +namespace lean { obj* get_extern_entry_for_core(obj*, obj*); } +uint8 l_nat_dec__lt(obj*, obj*); namespace lean { obj* mk_adhoc_ext_entry_core(obj* x_0) { _start: diff --git a/src/boot/init/lean/format.cpp b/src/boot/init/lean/format.cpp index c4dc7a7edd..043098fb4d 100644 --- a/src/boot/init/lean/format.cpp +++ b/src/boot/init/lean/format.cpp @@ -3,8 +3,6 @@ // Imports: init.control.except init.control.reader init.control.state #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -22,13 +20,18 @@ obj* l_lean_list_to__format___main___rarg(obj*, obj*); obj* l_lean_format_space__upto__line_x_27___main___lambda__1(obj*, obj*, obj*); obj* l_lean_format_paren___closed__1; obj* l_lean_format_space__upto__line___main(obj*, obj*); +namespace lean { +obj* uint16_to_nat(uint16); +} obj* l_lean_format_prefix__join(obj*); +obj* l_nat_add(obj*, obj*); obj* l_lean_format_flatten___main(obj*); obj* l_lean_format_join___closed__1; obj* l_lean_format_join__sep___main___rarg(obj*, obj*, obj*); obj* l_lean_prod__has__to__format___rarg___closed__1; obj* l_lean_usize__has__to__format___boxed(obj*); obj* l_lean_nat__has__to__format(obj*); +obj* l_thunk_mk(obj*, obj*); obj* l_nat_repeat__core___main___at_string_pushn___spec__1(uint32, obj*, obj*, obj*); obj* l_lean_format_repr___main___closed__5; obj* l_lean_has__repr___lambda__1(obj*); @@ -37,8 +40,14 @@ obj* l_lean_list_to__format___main___rarg___closed__1; obj* l_lean_to__string__to__format___rarg___lambda__1(obj*); obj* l_lean_uint64__has__to__format(uint64); obj* l_lean_format_repr(obj*); +namespace lean { +obj* string_length(obj*); +} obj* l_lean_format_prefix__join___rarg(obj*, obj*, obj*); obj* l_lean_to__fmt(obj*); +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_lean_format_sbracket___closed__2; obj* l_function_comp___rarg(obj*, obj*, obj*); obj* l_lean_format_join__suffix___main(obj*); @@ -67,6 +76,9 @@ extern obj* l_string_join___closed__1; obj* l_id___rarg(obj*); obj* l_lean_format_has__coe(obj*); obj* l_lean_format_prefix__join___main(obj*); +namespace lean { +obj* uint32_to_nat(uint32); +} obj* l_lean_list__has__to__format(obj*); obj* l_lean_format_has__append(obj*, obj*); obj* l_lean_format_group___main(obj*); @@ -74,6 +86,7 @@ obj* l_lean_list__has__to__format___rarg(obj*); obj* l_lean_format_paren___closed__3; obj* l_lean_format_paren(obj*); obj* l_lean_format_repr___main(obj*); +obj* l_thunk_get(obj*, obj*); obj* l_lean_format_join__suffix(obj*); obj* l_lean_format_join__sep___rarg(obj*, obj*, obj*); obj* l_lean_format_pretty(obj*, obj*); @@ -84,6 +97,9 @@ obj* l_lean_format_space__upto__line___main___closed__1; obj* l_lean_format_repr___main___closed__6; obj* l_lean_format_space__upto__line___main___lambda__1(obj*, obj*, obj*); obj* l_list_foldl___main___at_lean_format_join___spec__1(obj*, obj*); +namespace lean { +obj* uint64_to_nat(uint64); +} obj* l_lean_format_flatten___main___closed__1; obj* l_lean_format_flatten(obj*); obj* l_lean_prod__has__to__format(obj*, obj*); @@ -106,7 +122,11 @@ obj* l_lean_format_repr___main___closed__2; obj* l_lean_format_join__suffix___rarg(obj*, obj*, obj*); obj* l_lean_format_bracket(obj*, obj*, obj*); obj* l_lean_to__string__to__format(obj*); +namespace lean { +obj* usize_to_nat(usize); +} obj* l_lean_format_join__sep___main___at_lean_list_to__format___main___spec__1___rarg(obj*, obj*, obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* l_lean_format_has__append(obj* x_0, obj* x_1) { _start: { diff --git a/src/boot/init/lean/frontend.cpp b/src/boot/init/lean/frontend.cpp index b2e2c4ec93..ab8faa4c05 100644 --- a/src/boot/init/lean/frontend.cpp +++ b/src/boot/init/lean/frontend.cpp @@ -3,8 +3,6 @@ // Imports: init.default init.lean.parser.module init.lean.expander init.lean.elaborator init.io #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -41,6 +39,9 @@ obj* l_lean_process__file___lambda__1___closed__8; obj* lean_process_file(obj*, obj*, uint8, obj*); obj* l_lean_run__frontend(obj*, obj*, obj*, obj*); obj* l_lean_parser_module_parser(obj*, obj*, obj*); +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_io_prim_iterate___main___at_lean_run__frontend___spec__15(obj*, obj*, obj*); obj* l_lean_process__file___lambda__1___closed__2; obj* l_lean_process__file___closed__1; @@ -78,6 +79,9 @@ obj* l_lean_run__expander___rarg(obj*, obj*); obj* l_list_mmap_x_27___main___at_lean_run__frontend___spec__10(obj*, obj*, obj*); obj* l_io_prim_iterate__eio___at_lean_run__frontend___spec__14___closed__1; obj* l_lean_parser_parsec__t_run___at_lean_run__frontend___spec__2___rarg___closed__1; +namespace lean { +obj* string_mk_iterator(obj*); +} obj* l_io_print___at_lean_run__frontend___spec__4(obj*, obj*); extern obj* l_lean_parser_command_builtin__command__parsers; obj* l_io_prim_iterate__eio___at_lean_run__frontend___spec__14___lambda__1(obj*, obj*, obj*, obj*); diff --git a/src/boot/init/lean/ir/elim_phi.cpp b/src/boot/init/lean/ir/elim_phi.cpp index 5ddd1a6908..1d4bd8c7dd 100644 --- a/src/boot/init/lean/ir/elim_phi.cpp +++ b/src/boot/init/lean/ir/elim_phi.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.ir.instances init.control.state init.lean.disjoint_set #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -20,12 +18,16 @@ obj* l_mk__hashmap__imp___rarg(obj*); obj* l_hashmap__imp_fold__buckets___rarg(obj*, obj*, obj*); obj* l_lean_ir_elim__phi(obj*); obj* l_lean_ir_header_replace__vars(obj*, obj*); +obj* l_nat_add(obj*, obj*); obj* l_lean_mk__disjoint__set___at_lean_ir_elim__phi__m_run___spec__1; obj* l_lean_ir_elim__phi__m_run___rarg___closed__1; obj* l_lean_ir_arg_replace__vars(obj*, obj*); obj* l_d__hashmap_find___at_lean_ir_merge___spec__4(obj*, obj*); obj* l_list_mmap_x_27___main___at_lean_ir_group__vars___main___spec__1(obj*, obj*, obj*); obj* l_lean_ir_elim__phi__aux(obj*, obj*); +namespace lean { +usize name_hash_usize(obj*); +} obj* l_lean_ir_instr_replace__vars(obj*, obj*); obj* l_list_mmap___main___at_lean_ir_instr_replace__vars___main___spec__1(obj*, obj*); obj* l_list_mmap___main___at_lean_ir_instr_replace__vars___main___spec__2(obj*, obj*); @@ -39,7 +41,12 @@ obj* l_array_uread___rarg(obj*, usize, obj*); obj* l_lean_ir_decl_replace__vars(obj*, obj*); obj* l_lean_ir_find(obj*, obj*); obj* l_lean_ir_elim__phi__m_run___rarg(obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_ir_instr_replace__vars___main(obj*, obj*); +uint8 l_nat_dec__le(obj*, obj*); +namespace lean { +usize usize_modn(usize, obj*); +} obj* l_mk__d__hashmap___at_lean_ir_elim__phi__m_run___spec__2(obj*); obj* l_hashmap__imp_find__aux___main___at_lean_ir_merge___spec__10(obj*, obj*); uint8 l_hashmap__imp_contains__aux___at_lean_ir_merge___spec__9(obj*, obj*); @@ -50,14 +57,19 @@ obj* l_lean_ir_block_replace__vars(obj*, obj*); obj* l_hashmap__imp_insert___at_lean_ir_merge___spec__8___closed__1; obj* l_d__hashmap_insert___at_lean_ir_merge___spec__7(obj*, obj*, obj*); obj* l_lean_disjoint__set_merge___main___at_lean_ir_merge___spec__1(obj*, obj*, obj*); +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} obj* l_lean_ir_merge(obj*, obj*, obj*); obj* l_lean_ir_group__vars(obj*, obj*); obj* l_array_uwrite___rarg(obj*, usize, obj*, obj*); obj* l_list_mmap___main___at_lean_ir_instr_replace__vars___main___spec__3(obj*, obj*); obj* l_lean_ir_elim__phi__m_run(obj*); +obj* l_nat_mul(obj*, obj*); obj* l_lean_disjoint__set_find___main___at_lean_ir_find___spec__1(obj*, obj*); obj* l_lean_ir_group__vars___main(obj*, obj*); obj* l_lean_ir_terminator_replace__vars(obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l_hashmap__imp_replace__aux___main___at_lean_ir_merge___spec__11(obj*, obj*, obj*); obj* l_lean_name_hash___boxed(obj*); obj* l_hashmap__imp_find___at_lean_ir_merge___spec__5(obj*, obj*); @@ -67,6 +79,7 @@ obj* l_hashmap__imp_contains__aux___at_lean_ir_merge___spec__9___boxed(obj*, obj obj* l_lean_ir_decl_replace__vars___main(obj*, obj*); obj* l_list_mmap_x_27___main___at_lean_ir_group__vars___main___spec__3(obj*, obj*); obj* l_hashmap__imp_insert___at_lean_ir_merge___spec__8(obj*, obj*, obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* l_hashmap__imp_reinsert__aux___rarg(obj*, obj*, obj*, obj*); obj* _init_l_lean_ir_elim__phi__m() { _start: diff --git a/src/boot/init/lean/ir/extract_cpp.cpp b/src/boot/init/lean/ir/extract_cpp.cpp index 4ac5fb6645..e42381d4eb 100644 --- a/src/boot/init/lean/ir/extract_cpp.cpp +++ b/src/boot/init/lean/ir/extract_cpp.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.name_mangling init.lean.config init.lean.ir.type_check #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -28,6 +26,9 @@ obj* l_lean_ir_cpp_emit__main__proc___closed__1; obj* l_except__t_monad__run___rarg(obj*, obj*, obj*); obj* l_list_foldr___main___at_lean_ir_cpp_decl__locals___spec__1(obj*, obj*); obj* l_lean_ir_cpp_emit(obj*); +namespace lean { +obj* nat2int(obj*); +} obj* l_lean_ir_cpp_emit__uncurry__header(obj*, obj*, obj*); obj* l_lean_ir_cpp_assign__unop2cpp___boxed(obj*, obj*); obj* l_lean_ir_cpp_emit__cases___main(obj*, obj*, obj*, obj*); @@ -52,6 +53,9 @@ obj* l_lean_ir_cpp_file__header___closed__4; obj* l_lean_ir_cpp_emit__main__proc___closed__4; obj* l_rbnode_balance2__node___main___rarg(obj*, obj*, obj*, obj*); extern obj* l___private_init_lean_name__mangling_1__string_mangle__aux___main___closed__2; +namespace lean { +obj* uint16_to_nat(uint16); +} obj* l_list_foldl___main___at_lean_ir_cpp_collect__used___spec__4(obj*, obj*); obj* l_lean_ir_cpp_emit__infix___closed__1; obj* l_rbnode_insert___at_lean_ir_cpp_collect__used___spec__2(obj*, obj*, obj*); @@ -65,6 +69,7 @@ obj* l_lean_ir_instr_to__format___main(obj*); obj* l_lean_ir_cpp_emit__instr___closed__1; obj* l_lean_ir_cpp_unop2cpp___main___closed__9; extern obj* l_lean_ir_match__type___closed__5; +obj* l_nat_add(obj*, obj*); obj* l_lean_ir_cpp_emit__case___main___closed__7; obj* l_lean_ir_cpp_emit__eos___closed__1; obj* l_lean_ir_cpp_assign__unop2cpp___main___closed__8; @@ -128,6 +133,9 @@ extern obj* l_lean_ir_mk__fnid__set; obj* l_lean_ir_cpp_emit__template__params(obj*, obj*, obj*); obj* l_lean_ir_cpp_emit__template__param___boxed(obj*, obj*, obj*); obj* l_lean_ir_cpp_emit__type__size___closed__1; +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_lean_ir_cpp_emit__main__proc___closed__2; obj* l_except__t_monad__except___rarg(obj*); obj* l_lean_ir_cpp_emit__uncurry___closed__1; @@ -184,6 +192,7 @@ obj* l_lean_ir_cpp_emit__assign__binop___closed__12; obj* l_lean_ir_cpp_emit__main__proc(obj*, obj*); obj* l_rbmap_insert___main___at_lean_ir_cpp_collect__used___spec__1(obj*, obj*, obj*); extern obj* l_list_repr___main___rarg___closed__3; +uint8 l_nat_dec__eq(obj*, obj*); extern obj* l_lean_format_be___main___closed__1; obj* l_lean_ir_cpp_emit__uncurry__header___closed__1; obj* l_lean_ir_cpp_emit__assign__binop___closed__23; @@ -262,6 +271,9 @@ obj* l___private_init_lean_name__mangling_4__name_mangle__aux___main(obj*, obj*) obj* l_lean_ir_cpp_file__header___closed__3; obj* l_lean_ir_cpp_emit__logical__arith___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_ir_cpp_extract__m_monad__state; +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} obj* l_lean_ir_cpp_emit__assign__binop___closed__17; obj* l_lean_ir_cpp_type2cpp___main___closed__4; obj* l_lean_ir_cpp_emit__instr___closed__6; @@ -343,6 +355,7 @@ obj* l_rbnode_balance1__node___main___rarg(obj*, obj*, obj*, obj*); obj* l_id_monad___lambda__2(obj*, obj*, obj*, obj*); obj* l_lean_ir_cpp_emit__num__suffix___main___boxed(obj*, obj*, obj*); extern obj* l_lean_ir_mk__context; +obj* l_nat_sub(obj*, obj*); extern obj* l_option_has__repr___rarg___closed__3; obj* l_lean_ir_cpp_emit__assign__binop___closed__39; obj* l_lean_ir_cpp_emit__big__binop(obj*, obj*, obj*, obj*, obj*, obj*); @@ -365,10 +378,17 @@ obj* l_lean_ir_cpp_file__header(obj*); obj* l_lean_ir_cpp_emit__assign__binop___closed__2; obj* l_rbnode_mfold___main___at_lean_ir_cpp_emit__used__headers___spec__1___closed__1; obj* l_lean_ir_cpp_emit__instr___closed__4; +namespace lean { +obj* usize_to_nat(usize); +} obj* l_lean_ir_cpp_emit__apply___closed__3; +namespace lean { +uint8 int_dec_lt(obj*, obj*); +} obj* l_lean_ir_cpp_emit__assign__binop___closed__32; obj* l_lean_ir_cpp_emit__assign__binop___closed__22; extern obj* l_lean_closure__max__args; +uint8 l_nat_dec__lt(obj*, obj*); obj* l_lean_ir_cpp_emit__assign__binop___closed__6; extern obj* l_lean_ir_is__arith__ty___closed__1; obj* l_lean_ir_cpp_unop2cpp___main___closed__7; diff --git a/src/boot/init/lean/ir/format.cpp b/src/boot/init/lean/ir/format.cpp index bab2f07100..e947731bea 100644 --- a/src/boot/init/lean/ir/format.cpp +++ b/src/boot/init/lean/ir/format.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.format init.lean.parser.identifier init.lean.ir.reserved init.lean.ir.ir #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -33,6 +31,9 @@ obj* l_lean_ir_terminator_to__format(obj*); obj* l_lean_ir_block_to__format___main(obj*); obj* l_lean_ir_unop_has__to__format; obj* l_lean_ir_instr_to__format___main___closed__12; +namespace lean { +obj* uint16_to_nat(uint16); +} obj* l_lean_ir_decl_to__format(obj*); obj* l_lean_ir_assign__unop_to__format___main___closed__17; obj* l_lean_ir_should__escape__aux___main(obj*, uint8, obj*); @@ -91,6 +92,9 @@ extern obj* l_lean_list_to__format___main___rarg___closed__1; obj* l_lean_ir_type_to__format___main(uint8); obj* l_lean_ir_assign__unop_to__format___main___closed__1; obj* l_lean_format_join__sep___main___at_lean_ir_decl_to__format___main___spec__1(obj*, obj*); +namespace lean { +obj* string_iterator_next(obj*); +} obj* l_lean_ir_assign__binop_to__format___main___closed__19; obj* l_lean_ir_arg_has__to__string; obj* l_lean_ir_blockid_has__to__format(obj*); @@ -103,6 +107,9 @@ obj* l_lean_ir_type_to__format___main___closed__9; obj* l_lean_ir_literal_has__to__string; obj* l_lean_ir_block_has__to__format; obj* l_lean_ir_assign__binop_to__format___main___closed__10; +namespace lean { +obj* string_length(obj*); +} obj* l_lean_ir_instr_decorate__error___rarg(obj*, obj*, obj*); obj* l_lean_ir_assign__binop_to__format___main___boxed(obj*); obj* l_lean_ir_assign__binop_to__format___main___closed__5; @@ -111,10 +118,16 @@ obj* l_lean_ir_instr_to__format___main___closed__9; obj* l_lean_ir_assign__binop_to__format___main___closed__22; obj* l_lean_ir_tag_has__to__format; obj* l_lean_ir_assign__unop_to__format___main___closed__12; +namespace lean { +uint32 string_iterator_curr(obj*); +} extern obj* l_lean_name_to__string___closed__1; obj* l_lean_ir_decl_has__to__string; obj* l_lean_to__fmt___at_lean_ir_arg_has__to__string___spec__1(obj*); obj* l_lean_ir_instr_to__format___main___closed__13; +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_uint16_has__to__string___boxed(obj*); obj* l_lean_ir_assign__unop_to__format___main___closed__14; extern obj* l_lean_format_sbracket___closed__2; @@ -157,6 +170,7 @@ obj* l_lean_ir_assign__binop_has__to__format; obj* l_lean_ir_decl_to__format___main___closed__1; obj* l_lean_ir_block_to__format___main___closed__1; obj* l_lean_ir_unop_to__format___main___closed__7; +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_format_join__suffix___main___at_lean_ir_block_to__format___main___spec__2(obj*, obj*); obj* l_lean_to__fmt___at_lean_ir_unop_has__to__string___spec__1(uint8); obj* l_lean_ir_instr_to__format___main___closed__10; @@ -208,6 +222,9 @@ obj* l_lean_ir_type_to__format___main___closed__2; obj* l_lean_ir_assign__binop_to__format___main___closed__16; obj* l_lean_ir_escape__string(obj*); obj* l_lean_to__fmt___at_lean_ir_instr_to__format___main___spec__4(uint16); +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} obj* l_lean_ir_unop_to__format___main___boxed(obj*); obj* l_lean_ir_block_to__format___main___closed__2; obj* l_lean_to__fmt___at_lean_ir_instr_to__format___main___spec__6___boxed(obj*); @@ -224,6 +241,9 @@ obj* l_lean_ir_id_to__string___main___closed__1; extern obj* l_lean_format_flatten___main___closed__1; obj* l_lean_ir_assign__unop_to__format___main___closed__11; obj* l_lean_ir_assign__unop_to__format___main___closed__8; +namespace lean { +obj* string_mk_iterator(obj*); +} obj* l_lean_to__fmt___at_lean_ir_terminator_to__format___main___spec__4(obj*); obj* l_lean_ir_header_has__to__string; extern obj* l_lean_format_paren___closed__2; @@ -255,9 +275,13 @@ obj* l_lean_to__fmt___at_lean_ir_literal_to__format___main___spec__1___boxed(obj obj* l_lean_to__fmt___at_lean_ir_block_has__to__string___spec__1(obj*); obj* l_lean_ir_assign__binop_to__format___main___closed__6; obj* l_lean_ir_instr_to__format___main___closed__5; +obj* l_nat_sub(obj*, obj*); obj* l_lean_to__fmt___at_lean_ir_sizet__entry_to__format___main___spec__1(obj*); obj* l_lean_ir_instr_to__format___main___closed__4; obj* l_lean_ir_terminator_decorate__error(obj*, obj*); +namespace lean { +obj* string_push(obj*, uint32); +} obj* l_lean_ir_header_decorate__error(obj*, obj*); obj* l_lean_ir_assign__unop_to__format___main___closed__7; obj* l_lean_ir_fnid_has__to__string(obj*); @@ -265,6 +289,9 @@ obj* l_lean_ir_assign__binop_to__format___main___closed__3; obj* l_lean_ir_instr_to__format___main___closed__8; obj* l_lean_ir_block_decorate__error___rarg___lambda__1(obj*, obj*, obj*); obj* l_lean_ir_type_to__format___boxed(obj*); +namespace lean { +obj* usize_to_nat(usize); +} obj* l_lean_ir_assign__binop_to__format___main___closed__9; obj* l_lean_ir_terminator_to__format___main___closed__3; obj* l_lean_ir_assign__unop_to__format___main___closed__4; diff --git a/src/boot/init/lean/ir/instances.cpp b/src/boot/init/lean/ir/instances.cpp index 42fe4c7a9a..4696e6fefd 100644 --- a/src/boot/init/lean/ir/instances.cpp +++ b/src/boot/init/lean/ir/instances.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.ir.ir #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -31,6 +29,7 @@ obj* l_lean_ir_mk__fnid__set; obj* l_lean_ir_blockid__set; obj* l_lean_ir_mk__fnid2string; extern obj* l_lean_name_hashable; +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_ir_type2id___boxed(obj*); obj* l_lean_ir_mk__var2blockid; obj* l_lean_ir_inhabited___boxed; diff --git a/src/boot/init/lean/ir/ir.cpp b/src/boot/init/lean/ir/ir.cpp index 648ba4057d..6c7591e567 100644 --- a/src/boot/init/lean/ir/ir.cpp +++ b/src/boot/init/lean/ir/ir.cpp @@ -3,8 +3,6 @@ // Imports: init.data.rbmap.default init.data.int.default init.control.state init.control.except init.control.combinators init.lean.name #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/lean/ir/lirc.cpp b/src/boot/init/lean/ir/lirc.cpp index 3dbf7d3f4a..916df97c3d 100644 --- a/src/boot/init/lean/ir/lirc.cpp +++ b/src/boot/init/lean/ir/lirc.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.ir.parser init.lean.ir.type_check init.lean.ir.ssa_check init.lean.ir.extract_cpp init.lean.ir.format init.lean.ir.elim_phi #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -34,15 +32,27 @@ obj* l_rbmap_insert___main___at_lean_ir_parse__input__aux___main___spec__1(obj*, obj* l___private_init_lean_parser_parsec_6__take__while__aux_x_27___main___at_lean_ir_parse__input___spec__3(obj*, uint8, obj*); extern obj* l_lean_parser_monad__parsec_eoi__error___rarg___closed__1; obj* l_lean_ir_parse__decl(obj*); +namespace lean { +obj* string_iterator_next(obj*); +} obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_parse__input__aux___main___spec__5(uint32, obj*); obj* l_list_foldl___main___at_lean_ir_update__env___spec__4(obj*, obj*); obj* l_lean_parser_parsec__t_run___at_lean_parser_parsec_parse___spec__1___rarg(obj*, obj*, obj*); obj* l_rbmap_insert___main___at_lean_ir_update__env___spec__1(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_eoi___at___private_init_lean_name__mangling_2__parse__mangled__string__aux___main___spec__6(obj*); obj* l_lean_ir_symbol(obj*, obj*); +namespace lean { +obj* string_length(obj*); +} obj* l_option_orelse___main___rarg(obj*, obj*); uint8 l_char_is__alpha(uint32); +namespace lean { +uint32 string_iterator_curr(obj*); +} obj* l_lean_ir_parse__input___lambda__1(obj*, obj*, obj*); +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_function_comp___rarg(obj*, obj*, obj*); obj* l_rbnode_mk__insert__result___main___rarg(uint8, obj*); extern obj* l_lean_ir_mk__fnid2string; @@ -53,8 +63,12 @@ obj* l___private_init_lean_parser_parsec_6__take__while__aux_x_27___main___at_le obj* l_rbnode_insert___at_lean_ir_update__env___spec__2(obj*, obj*, obj*); obj* l_lean_ir_extract__cpp(obj*, obj*); obj* l_lean_parser_parsec_message_to__string___rarg(obj*); +namespace lean { +uint8 string_iterator_has_next(obj*); +} obj* l_lean_ir_check__blockids(obj*); extern obj* l_list_repr___main___rarg___closed__3; +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_parser_monad__parsec_take__while_x_27___at_lean_ir_parse__input___spec__2(obj*); extern obj* l_char_has__repr___closed__1; obj* l_lean_ir_parse__input__aux(obj*, obj*, obj*, obj*); @@ -70,6 +84,9 @@ extern obj* l_list_repr___main___rarg___closed__2; obj* l_lean_ir_parse__input(obj*); obj* l_lean_ir_decl_valid__ssa(obj*); obj* l_lean_ir_parse__input__aux___main(obj*, obj*, obj*, obj*); +namespace lean { +obj* string_iterator_remaining(obj*); +} obj* l_rbnode_find___main___at_lean_ir_update__env___spec__6___rarg(obj*, obj*); obj* l_lean_ir_decl_name(obj*); obj* l_rbmap_find___main___at_lean_ir_update__external__names___spec__1(obj*, obj*); @@ -84,6 +101,10 @@ obj* l___private_init_lean_parser_parsec_3__mk__string__result___rarg(obj*, obj* obj* l_lean_ir_type__check(obj*, obj*); obj* l_rbmap_find___main___at_lean_ir_update__env___spec__5(obj*, obj*); obj* l_rbnode_balance1__node___main___rarg(obj*, obj*, obj*, obj*); +obj* l_nat_sub(obj*, obj*); +namespace lean { +obj* string_push(obj*, uint32); +} obj* l_lean_name_quick__lt___main(obj*, obj*); obj* l_dlist_singleton___rarg(obj*, obj*); obj* l_lean_parser_parsec__t_orelse__mk__res___rarg(obj*, obj*); @@ -92,6 +113,7 @@ obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at_lean_ir obj* l_lean_ir_update__external__names(obj*, obj*, obj*); obj* l_char_quote__core(uint32); obj* l_list_mmap_x_27___main___at_lean_ir_lirc___spec__1___boxed(obj*, obj*, obj*, obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* l_rbnode_ins___main___at_lean_ir_parse__input__aux___main___spec__3(obj* x_0, obj* x_1, obj* x_2) { _start: { diff --git a/src/boot/init/lean/ir/parser.cpp b/src/boot/init/lean/ir/parser.cpp index 8ac2c2a303..0bccc4767e 100644 --- a/src/boot/init/lean/ir/parser.cpp +++ b/src/boot/init/lean/ir/parser.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.ir.ir init.lean.parser.parsec init.lean.parser.identifier init.lean.parser.string_literal init.lean.ir.reserved #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -23,6 +21,9 @@ obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_parse__literal__ obj* l_lean_ir_parse__untyped__assignment(obj*, obj*); obj* l___private_init_lean_parser_parsec_6__take__while__aux_x_27___main___at_lean_ir_symbol___spec__4___boxed(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_foldl___at_lean_ir_identifier___spec__37(obj*, obj*); +namespace lean { +obj* nat2int(obj*); +} obj* l_lean_parser_parsec__t_bind__mk__res___rarg(obj*, obj*); obj* l_lean_ir_parse__arg(obj*); uint8 l_char_is__whitespace(uint32); @@ -42,6 +43,7 @@ obj* l_lean_parser_monad__parsec_curr___at_lean_ir_identifier___spec__3(obj*); obj* l_lean_parser_monad__parsec_error___at_lean_ir_keyword___spec__1___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_lean_ir_parse__unop(obj*); obj* l_lean_ir_parse__type(obj*); +obj* l_nat_add(obj*, obj*); obj* l_lean_parser_monad__parsec_many1__aux___main___at_lean_ir_parse__block___spec__6(obj*, obj*); extern obj* l_lean_parser_parse__quoted__char___rarg___lambda__7___closed__1; obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at_lean_ir_parse__literal___spec__22(obj*, obj*, obj*); @@ -66,6 +68,9 @@ obj* l_lean_parser_monad__parsec_many1__aux___main___at_lean_ir_parse__terminato obj* l_lean_parser_parsec__t_try__mk__res___rarg(obj*); obj* l_lean_parser_monad__parsec_many___at_lean_ir_parse__untyped__assignment___spec__6(obj*); obj* l_lean_parser_monad__parsec_foldl___at_lean_ir_identifier___spec__41(obj*, obj*); +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_lean_ir_parse__defconst___closed__1; obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at_lean_ir_parse__literal___spec__14(obj*, obj*, obj*); obj* l_lean_parser_parse__hex__digit___at_lean_ir_parse__literal___spec__6(obj*); @@ -86,6 +91,9 @@ obj* l_lean_ir_parse__decl(obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_identifier___spec__9(uint32, obj*); obj* l_lean_parser_monad__parsec_foldl__aux___main___at_lean_ir_identifier___spec__42(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_many___at_lean_ir_parse__untyped__assignment___spec__1(obj*); +namespace lean { +obj* string_iterator_next(obj*); +} obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_parse__literal___spec__19(uint32, obj*); obj* l_lean_ir_parse__untyped__assignment___lambda__3(obj*, uint16, uint16, usize); obj* l_lean_ir_parse__fnid___closed__1; @@ -96,13 +104,22 @@ obj* l_lean_parser_monad__parsec_many1___at_lean_ir_parse__untyped__assignment__ obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at_lean_ir_parse__literal___spec__18(obj*, obj*, obj*); obj* l_lean_ir_symbol(obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_parse__literal___spec__13___boxed(obj*, obj*); +namespace lean { +obj* string_length(obj*); +} obj* l_lean_ir_parse__untyped__assignment___closed__1; obj* l_lean_parser_monad__parsec_any___at_lean_ir_parse__literal___spec__4(obj*); obj* l_lean_parser_monad__parsec_many1__aux___main___at_lean_ir_parse__phi___spec__2(obj*, obj*); uint8 l_string_is__empty(obj*); obj* l_lean_ir_keyword___closed__1; +namespace lean { +uint32 string_iterator_curr(obj*); +} obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_parse__literal___spec__11___boxed(obj*, obj*); obj* l_lean_ir_parse__untyped__assignment___lambda__6(obj*, obj*, obj*); +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_lean_parser_monad__parsec_many1___at_lean_ir_parse__def___spec__2(obj*); obj* l_function_comp___rarg(obj*, obj*, obj*); obj* l_lean_ir_parse__untyped__assignment___lambda__1___boxed(obj*, obj*, obj*, obj*); @@ -122,6 +139,9 @@ obj* l_lean_parser_parse__hex__digit___at_lean_ir_parse__literal___spec__6___clo obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_identifier___spec__21___boxed(obj*, obj*); obj* l_lean_ir_parse__untyped__assignment___closed__3; obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_parse__literal___spec__21___boxed(obj*, obj*); +namespace lean { +uint16 uint16_of_nat(obj*); +} obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_identifier___spec__33___boxed(obj*, obj*); obj* l_lean_ir_parse__untyped__assignment___closed__5; obj* l_lean_ir_parse__typed__assignment___closed__3; @@ -138,10 +158,14 @@ obj* l_lean_parser_monad__parsec_take__while1___at_lean_ir_identifier___spec__20 obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_parse__literal___spec__23(obj*, obj*); obj* l_lean_ir_parse__instr___closed__3; obj* l_lean_ir_parse__typed__assignment(obj*, obj*); +namespace lean { +uint8 string_iterator_has_next(obj*); +} obj* l_lean_ir_parse__instr___lambda__2___boxed(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_many1__aux___main___at_lean_ir_parse__untyped__assignment___spec__3(obj*, obj*); obj* l_lean_parser_monad__parsec_many___at_lean_ir_parse__def___spec__1(obj*); extern obj* l_list_repr___main___rarg___closed__3; +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_ir_parse__instr___lambda__4(obj*, obj*, obj*); obj* l_lean_ir_parse__key2val___rarg(obj*, obj*, obj*); extern obj* l_char_has__repr___closed__1; @@ -164,6 +188,7 @@ extern obj* l_string_join___closed__1; obj* l_lean_ir_parse__var(obj*); obj* l_id___rarg(obj*); obj* l_lean_ir_parse__terminator(obj*); +uint8 l_nat_dec__le(obj*, obj*); obj* l_lean_parser_monad__parsec_foldl__aux___main___at_lean_ir_identifier___spec__38(obj*, obj*, obj*); obj* l_lean_ir_parse__terminator___closed__2; obj* l_lean_parser_monad__parsec_take__while1___at_lean_ir_parse__literal___spec__10(obj*); @@ -202,6 +227,15 @@ obj* l_lean_ir_str2aunop; obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_identifier___spec__23___boxed(obj*, obj*); obj* l_lean_parser_id__part___at_lean_ir_identifier___spec__2(obj*); obj* l_lean_ir_parse__untyped__assignment___lambda__1(obj*, uint8, obj*, obj*); +namespace lean { +obj* string_iterator_remaining(obj*); +} +namespace lean { +usize usize_of_nat(obj*); +} +namespace lean { +obj* string_mk_iterator(obj*); +} obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_identifier___spec__15(uint32, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_identifier___spec__13___boxed(obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_identifier___spec__7___boxed(obj*, obj*); @@ -210,6 +244,9 @@ extern obj* l_usize__sz; obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at_lean_ir_identifier___spec__12(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_many1___at_lean_ir_parse__block___spec__5(obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_identifier___spec__25___boxed(obj*, obj*); +namespace lean { +obj* int_neg(obj*); +} obj* l_lean_parser_monad__parsec_many1__aux___main___at_lean_ir_parse__block___spec__3___closed__1; obj* l_lean_parser_monad__parsec_foldl___at_lean_ir_identifier___spec__35(obj*, obj*); obj* l_lean_ir_parse__untyped__assignment___lambda__5(obj*, obj*, uint16); @@ -228,6 +265,7 @@ obj* l_lean_ir_parse__typed__assignment___lambda__2(obj*, uint8, uint8, obj*); uint8 l_lean_is__id__first(uint32); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_identifier___spec__29___boxed(obj*, obj*); obj* l_lean_parser_monad__parsec_unexpected__at___at_lean_ir_parse__literal___spec__8___rarg(obj*, obj*, obj*); +obj* l_nat_mul(obj*, obj*); obj* l_lean_parser_monad__parsec_many___at_lean_ir_parse__defconst___spec__1(obj*); obj* l_lean_ir_parse__literal___closed__1; obj* l_lean_parser_monad__parsec_ch___at_lean_ir_parse__literal___spec__2(uint32, obj*); @@ -242,10 +280,14 @@ obj* l_lean_ir_keyword(obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_parse__literal___spec__11(uint32, obj*); extern obj* l_uint16__sz; obj* l_lean_ir_parse__typed__assignment___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l_lean_ir_parse__blockid(obj*); extern obj* l_option_has__repr___rarg___closed__3; obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_identifier___spec__17(obj*, obj*); obj* l_lean_ir_parse__assign__unop(obj*); +namespace lean { +obj* string_push(obj*, uint32); +} obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at_lean_ir_parse__literal___spec__24(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_identifier___spec__29(uint32, obj*); obj* l_dlist_singleton___rarg(obj*, obj*); @@ -270,6 +312,7 @@ obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at_lean_ir obj* l_lean_parser_monad__parsec_many1___at_lean_ir_parse__untyped__assignment___spec__2(obj*); obj* l_char_quote__core(uint32); obj* l_lean_parser_monad__parsec_error___at_lean_ir_keyword___spec__1(obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_identifier___spec__27(obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_identifier___spec__11___boxed(obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_ir_parse__literal___spec__19___boxed(obj*, obj*); diff --git a/src/boot/init/lean/ir/reserved.cpp b/src/boot/init/lean/ir/reserved.cpp index ae78edb8cf..82b887dc13 100644 --- a/src/boot/init/lean/ir/reserved.cpp +++ b/src/boot/init/lean/ir/reserved.cpp @@ -3,8 +3,6 @@ // Imports: init.data.rbtree.basic init.lean.name #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -28,6 +26,9 @@ uint8 l_lean_ir_is__reserved(obj*); obj* l_lean_ir_is__reserved__name___boxed(obj*); obj* l_rbnode_mk__insert__result___main___rarg(uint8, obj*); uint8 l_option_is__some___main___rarg(obj*); +namespace lean { +uint8 string_dec_lt(obj*, obj*); +} uint8 l_lean_ir_is__reserved__name(obj*); obj* l_rbtree_insert___at_lean_ir_reserved__set___spec__1(obj*, obj*); obj* l_lean_ir_reserved; diff --git a/src/boot/init/lean/ir/ssa_check.cpp b/src/boot/init/lean/ir/ssa_check.cpp index 4e5ccd7634..087ec4618e 100644 --- a/src/boot/init/lean/ir/ssa_check.cpp +++ b/src/boot/init/lean/ir/ssa_check.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.ir.instances init.lean.ir.format #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/lean/ir/type_check.cpp b/src/boot/init/lean/ir/type_check.cpp index e2ef2f79fc..4a51e3b4be 100644 --- a/src/boot/init/lean/ir/type_check.cpp +++ b/src/boot/init/lean/ir/type_check.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.ir.instances init.lean.ir.format init.control.combinators #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -78,6 +76,7 @@ obj* l_lean_ir_check__ne__type___closed__2; obj* l_lean_ir_type__checker__m; obj* l_lean_ir_match__type___boxed(obj*, obj*, obj*, obj*, obj*); obj* l_lean_ir_match__type___closed__2; +uint8 l_nat_dec__eq(obj*, obj*); uint8 l_lean_ir_is__bitshift__ty(uint8); obj* l_lean_ir_type__checker__m_run___rarg(obj*, obj*, obj*); obj* l_lean_ir_infer__types(obj*, obj*); @@ -94,6 +93,7 @@ obj* l_lean_ir_get__decl(obj*, obj*, obj*); uint8 l_lean_ir_valid__assign__binop__types(uint8, uint8, uint8, uint8); obj* l_lean_ir_match__type___closed__3; obj* l_lean_ir_check__arg__types(obj*, obj*, obj*, obj*); +uint8 l_nat_dec__le(obj*, obj*); extern obj* l_int_zero; obj* l_list_mmap_x_27___main___at_lean_ir_phi_check___spec__1(obj*, obj*, obj*, obj*); obj* l_lean_ir_invalid__literal(obj*); @@ -140,6 +140,9 @@ obj* l_lean_ir_check__type___boxed(obj*, obj*, obj*, obj*); obj* l_lean_ir_is__bitwise__ty___boxed(obj*); obj* l_lean_ir_is__nonfloat__arith__ty___closed__1; obj* l_list_mmap_x_27___main___at_lean_ir_block_infer__types___spec__2(obj*, obj*, obj*); +namespace lean { +uint8 int_dec_lt(obj*, obj*); +} obj* l_reader__t_bind___at_lean_ir_type__check___spec__2(obj*, obj*); obj* l_lean_ir_is__arith__ty___closed__1; obj* l_lean_ir_arg_infer__types(obj*, obj*, obj*); diff --git a/src/boot/init/lean/kvmap.cpp b/src/boot/init/lean/kvmap.cpp index a4c2993ba4..9ae4395d62 100644 --- a/src/boot/init/lean/kvmap.cpp +++ b/src/boot/init/lean/kvmap.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.name init.data.option.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -29,6 +27,9 @@ uint8 l_option_is__some___main___rarg(obj*); obj* l_lean_kvmap_contains___boxed(obj*, obj*); obj* l_lean_kvmap_insert(obj*, obj*, obj*); obj* l_lean_kvmap_find___main(obj*, obj*); +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} obj* l_lean_kvmap_find(obj*, obj*); obj* l_lean_kvmap_get__name(obj*, obj*); obj* l_lean_kvmap_insert__core___main(obj*, obj*, obj*); diff --git a/src/boot/init/lean/level.cpp b/src/boot/init/lean/level.cpp index 317dd10c42..2240f189c8 100644 --- a/src/boot/init/lean/level.cpp +++ b/src/boot/init/lean/level.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.name init.data.option.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -24,6 +22,7 @@ extern obj* l_lean_format_paren___closed__1; obj* l_lean_level__to__format_result__list_to__format(obj*); obj* l_lean_level_instantiate___main(obj*, obj*); obj* l_lean_level__to__format_paren__if__false(obj*, uint8); +obj* l_nat_add(obj*, obj*); obj* l_lean_level__to__format_level_to__result___main(obj*); obj* l_lean_level__to__format_result_succ___main(obj*); obj* l_nat_max(obj*, obj*); @@ -46,6 +45,7 @@ obj* l_lean_level__to__format_result_max(obj*, obj*); obj* l_lean_level_instantiate(obj*, obj*); obj* l_lean_level__to__format_result_succ(obj*); obj* l_lean_level_to__nat___main___closed__1; +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_level_to__offset(obj*); obj* l_lean_level__to__format_result_to__format___main___closed__1; obj* l_lean_level_of__nat(obj*); @@ -70,6 +70,7 @@ obj* l_lean_level__to__format_result__list_to__format___main(obj*); obj* l_lean_level_to__nat(obj*); obj* l_nat_repr(obj*); obj* l_lean_level__to__format_result_imax(obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l_lean_level_to__offset___main(obj*); obj* l_option_map___rarg(obj*, obj*); obj* l_lean_level_to__nat___main___closed__3; diff --git a/src/boot/init/lean/message.cpp b/src/boot/init/lean/message.cpp index 371bb290d7..18d484b762 100644 --- a/src/boot/init/lean/message.cpp +++ b/src/boot/init/lean/message.cpp @@ -3,8 +3,6 @@ // Imports: init.data.to_string init.lean.position #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -22,12 +20,18 @@ obj* l_lean_message__log_append(obj*, obj*); uint8 l_list_foldr___main___at_lean_message__log_has__errors___spec__1(obj*); obj* l_list_reverse___rarg(obj*); obj* l_lean_message__log_to__list(obj*); +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_lean_message_has__to__string; obj* l_lean_message__log_has__append; obj* l_lean_message__log_empty; obj* l_lean_message__log_add(obj*, obj*); extern obj* l_string_join___closed__1; obj* l_lean_message_to__string(obj*); +namespace lean { +uint8 string_dec_eq(obj*, obj*); +} obj* l_lean_message_to__string___closed__4; obj* l_lean_message_to__string___closed__3; obj* l_list_foldr___main___at_lean_message__log_has__errors___spec__1___boxed(obj*); diff --git a/src/boot/init/lean/name.cpp b/src/boot/init/lean/name.cpp index 8821e05a6c..86d78843b2 100644 --- a/src/boot/init/lean/name.cpp +++ b/src/boot/init/lean/name.cpp @@ -3,8 +3,6 @@ // Imports: init.data.string.basic init.coe init.data.uint init.data.to_string init.lean.format init.data.hashable #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -24,23 +22,42 @@ obj* l___private_init_lean_name_1__hash__aux___main___boxed(obj*, obj*); obj* l_lean_name_components_x_27(obj*); obj* l_lean_name_to__string(obj*); obj* l_list_reverse___rarg(obj*); +namespace lean { +usize name_hash_usize(obj*); +} +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_lean_name_has__lt__quick; obj* l_lean_name_replace__prefix(obj*, obj*, obj*); uint8 l_lean_name_dec__eq___main(obj*, obj*); obj* l_lean_inhabited; obj* l_lean_name_to__string___closed__1; +namespace lean { +obj* string_append(obj*, obj*); +} uint8 l_lean_name_decidable__rel(obj*, obj*); obj* l_lean_name_append(obj*, obj*); obj* l_lean_name_hashable; obj* l_lean_name_replace__prefix___main(obj*, obj*, obj*); obj* l_lean_name_components(obj*); +namespace lean { +uint8 string_dec_lt(obj*, obj*); +} obj* l_lean_name_to__string__with__sep___main(obj*, obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_name_update__prefix(obj*, obj*); obj* l_lean_name_components_x_27___main(obj*); obj* l_lean_name_append___main(obj*, obj*); obj* l_lean_name_to__string__with__sep(obj*, obj*); obj* l_lean_name_dec__eq___boxed(obj*, obj*); obj* l___private_init_lean_name_1__hash__aux(obj*, usize); +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} +namespace lean { +uint8 string_dec_eq(obj*, obj*); +} obj* l_lean_mk__num__name(obj*, obj*); obj* l_lean_name_quick__lt(obj*, obj*); obj* l_lean_mk__simple__name(obj*); @@ -49,12 +66,16 @@ obj* l___private_init_lean_name_1__hash__aux___boxed(obj*, obj*); obj* l_lean_name_update__prefix___main(obj*, obj*); obj* l_lean_name_get__prefix(obj*); obj* l___private_init_lean_name_1__hash__aux___main(obj*, usize); +namespace lean { +obj* name_mk_numeral(obj*, obj*); +} obj* l_nat_repr(obj*); obj* l_lean_name_get__prefix___main(obj*); obj* l_lean_name_hash___boxed(obj*); obj* l_lean_name_quick__lt___main(obj*, obj*); obj* l_lean_name_to__string__with__sep___main___closed__1; obj* l_lean_name_has__to__string; +uint8 l_nat_dec__lt(obj*, obj*); obj* l_lean_name_dec__eq___main___boxed(obj*, obj*); obj* l_lean_name_decidable__rel___boxed(obj*, obj*); extern usize l_mix__hash___closed__1; diff --git a/src/boot/init/lean/name_mangling.cpp b/src/boot/init/lean/name_mangling.cpp index b865add007..0039e9d29e 100644 --- a/src/boot/init/lean/name_mangling.cpp +++ b/src/boot/init/lean/name_mangling.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.name init.lean.parser.string_literal #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -28,12 +26,17 @@ obj* l___private_init_lean_name__mangling_5__parse__mangled__name__aux(obj*, obj obj* l_lean_parser_parse__hex__digit___at___private_init_lean_name__mangling_2__parse__mangled__string__aux___main___spec__2___closed__1; obj* l_lean_parser_monad__parsec_error___at___private_init_lean_name__mangling_2__parse__mangled__string__aux___main___spec__3___rarg(obj*, obj*, obj*, obj*, obj*); obj* l___private_init_lean_name__mangling_1__string_mangle__aux___main___closed__2; +obj* l_nat_add(obj*, obj*); obj* l___private_init_lean_name__mangling_2__parse__mangled__string__aux___main___closed__1; extern obj* l_mjoin___rarg___closed__1; obj* l___private_init_lean_name__mangling_2__parse__mangled__string__aux___main___closed__3; +obj* l_nat_mod(obj*, obj*); obj* l___private_init_lean_name__mangling_1__string_mangle__aux___main(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_num___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__2(obj*); extern obj* l_lean_parser_monad__parsec_eoi___rarg___lambda__1___closed__1; +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_lean_parser_monad__parsec_take__while__cont___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__16(obj*, obj*); uint8 l_char_is__digit(uint32); obj* l_lean_parser_parsec__t_labels__mk__res___rarg(obj*, obj*); @@ -43,12 +46,24 @@ obj* l_lean_parser_monad__parsec_take__while__cont___at___private_init_lean_name obj* l_string_quote(obj*); extern obj* l_lean_parser_monad__parsec_eoi__error___rarg___closed__1; obj* l_lean_parser_monad__parsec_take__while1___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__3(obj*); +namespace lean { +obj* string_iterator_next(obj*); +} obj* l_lean_parser_parsec__t_run___at_lean_parser_parsec_parse___spec__1___rarg(obj*, obj*, obj*); obj* l___private_init_lean_parser_parsec_2__take__aux___main___rarg(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_eoi___at___private_init_lean_name__mangling_2__parse__mangled__string__aux___main___spec__6(obj*); +namespace lean { +obj* string_length(obj*); +} uint8 l_string_is__empty(obj*); obj* l___private_init_lean_name__mangling_4__name_mangle__aux___main___closed__1; uint8 l_char_is__alpha(uint32); +namespace lean { +uint32 string_iterator_curr(obj*); +} +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_function_comp___rarg(obj*, obj*, obj*); extern obj* l_lean_parser_parsec_result_mk__eps___rarg___closed__1; obj* l_lean_parser_monad__parsec_ch___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__1(uint32, obj*); @@ -62,6 +77,10 @@ obj* l_option_get__or__else___main___rarg(obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__8(uint32, obj*); obj* l_string_to__nat(obj*); obj* l_lean_parser_monad__parsec_str__core___at___private_init_lean_name__mangling_2__parse__mangled__string__aux___main___spec__1(obj*, obj*, obj*); +namespace lean { +uint8 string_iterator_has_next(obj*); +} +uint8 l_nat_dec__eq(obj*, obj*); extern obj* l_char_has__repr___closed__1; obj* l___private_init_lean_name__mangling_5__parse__mangled__name__aux___main(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_digit___at___private_init_lean_name__mangling_2__parse__mangled__string__aux___main___spec__4(obj*); @@ -69,11 +88,13 @@ obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at___priva obj* l___private_init_lean_name__mangling_4__name_mangle__aux(obj*, obj*); extern obj* l_string_join___closed__1; obj* l_id___rarg(obj*); +uint8 l_nat_dec__le(obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__6(uint32, obj*); obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__11(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_alpha___at___private_init_lean_name__mangling_2__parse__mangled__string__aux___main___spec__5(obj*); obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__7(obj*, obj*, obj*); obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__13(obj*, obj*, obj*); +obj* l_nat_div(obj*, obj*); obj* l___private_init_lean_name__mangling_4__name_mangle__aux___main(obj*, obj*); obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__17(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at___private_init_lean_name__mangling_2__parse__mangled__string__aux___main___spec__3(obj*); @@ -82,16 +103,30 @@ obj* l_lean_parser_monad__parsec_take__while__cont___at___private_init_lean_name obj* l_lean_parser_monad__parsec_take__while__cont___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__14(uint32, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__12___boxed(obj*, obj*); obj* l_lean_parser_monad__parsec_eoi___at___private_init_lean_name__mangling_2__parse__mangled__string__aux___main___spec__6___closed__1; +namespace lean { +obj* string_iterator_remaining(obj*); +} +namespace lean { +obj* string_mk_iterator(obj*); +} obj* l___private_init_lean_name__mangling_4__name_mangle__aux___main___closed__2; obj* l___private_init_lean_name__mangling_2__parse__mangled__string__aux___main(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__4(uint32, obj*); +namespace lean { +obj* name_mk_numeral(obj*, obj*); +} obj* l_nat_repr(obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__4___boxed(obj*, obj*); extern obj* l_lean_parser_parsec__t_monad__fail___rarg___closed__1; +obj* l_nat_mul(obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__12(uint32, obj*); obj* l___private_init_lean_parser_parsec_3__mk__string__result___rarg(obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l___private_init_lean_name__mangling_1__string_mangle__aux(obj*, obj*, obj*); obj* l___private_init_lean_name__mangling_2__parse__mangled__string__aux(obj*, obj*, obj*); +namespace lean { +obj* string_push(obj*, uint32); +} obj* l_dlist_singleton___rarg(obj*, obj*); obj* l_lean_parser_parsec__t_orelse__mk__res___rarg(obj*, obj*); obj* l___private_init_lean_name__mangling_1__string_mangle__aux___main___closed__3; @@ -102,6 +137,7 @@ obj* l_lean_parser_monad__parsec_take___at___private_init_lean_name__mangling_5_ obj* l___private_init_lean_name__mangling_1__string_mangle__aux___main___closed__1; obj* l_lean_parser_monad__parsec_take__while__cont___at___private_init_lean_name__mangling_5__parse__mangled__name__aux___main___spec__6___boxed(obj*, obj*); obj* l_char_quote__core(uint32); +uint8 l_nat_dec__lt(obj*, obj*); obj* _init_l___private_init_lean_name__mangling_1__string_mangle__aux___main___closed__1() { _start: { diff --git a/src/boot/init/lean/options.cpp b/src/boot/init/lean/options.cpp index a39b902360..98efb8fa8c 100644 --- a/src/boot/init/lean/options.cpp +++ b/src/boot/init/lean/options.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.kvmap #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/lean/parser/basic.cpp b/src/boot/init/lean/parser/basic.cpp index 87690ac71d..381c93f83a 100644 --- a/src/boot/init/lean/parser/basic.cpp +++ b/src/boot/init/lean/parser/basic.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.parser.parsec init.lean.parser.syntax init.lean.parser.rec init.lean.parser.trie init.lean.parser.identifier init.data.rbmap.default init.lean.message init.control.coroutine #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -68,6 +66,9 @@ obj* l_lean_parser_list_nil_tokens(obj*); obj* l_lean_parser_command__parser__m_monad(obj*); obj* l_lean_parser_has__view_default___rarg(obj*); obj* l_lean_parser_basic__parser__m; +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_lean_parser_command__parser__m_alternative___closed__1; obj* l_lean_parser_parser__core__t_monad__except(obj*); obj* l_lean_parser_command__parser; @@ -95,6 +96,7 @@ obj* l_lean_parser_log__message___rarg(obj*, obj*, obj*, obj*, obj*); extern obj* l_lean_parser_trie_mk___closed__1; obj* l_lean_parser_lean_parser_monad__parsec___rarg(obj*); extern obj* l_lean_message__log_empty; +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_parser_token__map__cons_tokens___rarg(obj*, obj*); obj* l_lean_parser_command__parser__m_basic__parser(obj*); obj* l_lean_parser_term__parser__m_lean_parser_monad__parsec; @@ -124,6 +126,9 @@ obj* l_reader__t_monad__except___rarg(obj*); obj* l_lean_parser_monad__parsec__trans___rarg(obj*, obj*, obj*); obj* l_rbmap_find___main___at_lean_parser_token__map_insert___spec__1(obj*); obj* l_lean_parser_parsec_message_text___rarg(obj*); +namespace lean { +obj* string_iterator_offset(obj*); +} obj* l_lean_parser_token__map_of__list___main(obj*); obj* l_list_mfoldl___main___at_lean_parser_mk__token__trie___spec__1___closed__3; obj* l_state__t_monad___rarg(obj*); @@ -137,6 +142,9 @@ obj* l_lean_parser_rec__t_recurse___rarg(obj*, obj*, obj*); obj* l_reader__t_lift(obj*, obj*, obj*, obj*); obj* l_lean_parser_try__view(obj*); obj* l_lean_parser_trailing__term__parser__m_monad; +namespace lean { +obj* string_mk_iterator(obj*); +} obj* l_lean_parser_basic__parser__m_alternative; obj* l_lean_parser_parser__t_alternative(obj*, obj*); obj* l_lean_parser_command__parser__m_monad__except(obj*); diff --git a/src/boot/init/lean/parser/combinators.cpp b/src/boot/init/lean/parser/combinators.cpp index 0743e8e10c..857616aa5e 100644 --- a/src/boot/init/lean/parser/combinators.cpp +++ b/src/boot/init/lean/parser/combinators.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.parser.basic init.data.list.instances #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -41,6 +39,7 @@ obj* l_lean_parser_combinators_longest__match_tokens(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* 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*); +obj* l_nat_add(obj*, obj*); obj* l_lean_parser_combinators_many1_tokens___rarg(obj*); obj* l_list_map___main___at_lean_parser_combinators_longest__choice___spec__1(obj*); obj* l___private_init_lean_parser_combinators_2__sep__by__aux___main___at_lean_parser_combinators_sep__by1___spec__1___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); @@ -112,6 +111,7 @@ obj* l_lean_parser_combinators_sep__by_view___rarg___lambda__2(obj*, obj*, obj*, obj* l_lean_parser_combinators_choice___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_combinators_many1_view___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_combinators_choice__aux___main___rarg___lambda__1(obj*, obj*, obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_parser_combinators_sep__by_tokens___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_combinators_optional_view___rarg___lambda__1(obj*, obj*); obj* l_list_mfoldl___main___at_lean_parser_combinators_node___spec__1(obj*); @@ -190,6 +190,9 @@ obj* l_lean_parser_combinators_any__of_tokens(obj*, obj*, obj*, obj*, obj*, obj* obj* l_lean_parser_combinators_seq__right_view___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_combinators_longest__match_tokens___rarg(obj*); obj* l_lean_parser_combinators_sep__by_view___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*); +namespace lean { +obj* name_mk_numeral(obj*, obj*); +} obj* l_lean_parser_combinators_sep__by(obj*); obj* l_lean_parser_combinators_any__of(obj*); extern obj* l_lean_parser_choice; @@ -197,6 +200,7 @@ obj* l___private_init_lean_parser_combinators_2__sep__by__aux___main___rarg___la obj* l_lean_parser_combinators_optional___rarg___lambda__2(obj*, obj*); extern obj* l_lean_parser_monad__parsec_try___rarg___closed__1; obj* l_list_map___main___at_lean_parser_combinators_sep__by_view___spec__1(obj*, obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l___private_init_lean_parser_combinators_2__sep__by__aux___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_combinators_many1___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_combinators_choice__aux(obj*); diff --git a/src/boot/init/lean/parser/command.cpp b/src/boot/init/lean/parser/command.cpp index c972238040..4e31a9386f 100644 --- a/src/boot/init/lean/parser/command.cpp +++ b/src/boot/init/lean/parser/command.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.parser.declaration #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -53,6 +51,7 @@ obj* l_lean_parser_command_open__spec_hiding_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_end_parser_lean_parser_has__tokens; obj* l_lean_parser_command_universes; obj* l_lean_parser_command_open_has__view_x_27___lambda__1(obj*); +obj* l_nat_add(obj*, obj*); obj* l_lean_parser_command_open__spec_has__view_x_27___lambda__1___closed__5; obj* l_lean_parser_command_open__spec_has__view_x_27___lambda__1___closed__3; obj* l_lean_parser_command_universe_has__view_x_27___lambda__1(obj*); @@ -81,6 +80,9 @@ obj* l_lean_parser_monad__parsec_error___at___private_init_lean_parser_token_1__ obj* l_lean_parser_command_namespace_parser_lean_parser_has__tokens; obj* l_lean_parser_parsec__t_try__mk__res___rarg(obj*); extern obj* l_lean_parser_command__parser__m_monad__except___closed__1; +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_lean_parser_monad__parsec_error___at_lean_parser_command_doc__comment_parser_lean_parser_has__view___spec__4___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_command_variable_has__view_x_27___lambda__1___closed__3; obj* l_lean_parser_command_open__spec_has__view_x_27___lambda__1___closed__1; @@ -194,6 +196,7 @@ obj* l_lean_parser_command_check_parser___closed__1; obj* l_lean_parser_symbol_tokens___rarg(obj*, obj*); extern obj* l_lean_parser_term_bracketed__binders_has__view; obj* l_list_map___main___at_lean_parser_command_attribute_has__view_x_27___spec__4(obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_parser_command_open__spec_renaming_item; obj* l_lean_parser_command_open__spec_renaming_has__view; extern obj* l_lean_parser_command_notation_has__view_x_27___lambda__1___closed__1; @@ -260,7 +263,13 @@ obj* l_list_map___main___at_lean_parser_command_open__spec_only_has__view_x_27__ obj* l_lean_parser_substring_to__string(obj*); obj* l_lean_parser_try__view___at_lean_parser_string__lit_parser___spec__1(obj*); obj* l_lean_parser_command_namespace_has__view_x_27___lambda__1(obj*); +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} obj* l_lean_parser_command_bool__option__value_has__view_x_27___lambda__2(obj*); +namespace lean { +uint8 string_dec_eq(obj*, obj*); +} obj* l_lean_parser_command_namespace_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_combinators_sep__by1___at_lean_parser_command_decl__attributes_parser_lean_parser_has__view___spec__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_command_section; @@ -273,6 +282,9 @@ obj* l_lean_parser_command_universe; obj* l_lean_parser_combinators_any__of___at_lean_parser_command__parser_run___spec__2(obj*, obj*, obj*, obj*); obj* l_lean_parser_command_section_parser(obj*, obj*, obj*, obj*); obj* l_lean_parser_command_attribute_has__view_x_27___lambda__1___closed__1; +namespace lean { +obj* string_iterator_remaining(obj*); +} 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; diff --git a/src/boot/init/lean/parser/declaration.cpp b/src/boot/init/lean/parser/declaration.cpp index 4224177ae7..3b942719a1 100644 --- a/src/boot/init/lean/parser/declaration.cpp +++ b/src/boot/init/lean/parser/declaration.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.parser.term #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -62,6 +60,7 @@ obj* l_lean_parser_command_structure_parser(obj*, obj*, obj*, obj*); obj* l_lean_parser_command_ident__univ__params_has__view_x_27___lambda__1___closed__3; obj* l_lean_parser_command_declaration; obj* l_lean_parser_command_doc__comment_parser_lean_parser_has__view; +obj* l_nat_add(obj*, obj*); obj* l_lean_parser_monad__parsec_many_x_27___at_lean_parser_command_doc__comment_parser___spec__2(obj*, obj*, obj*, obj*); obj* l_lean_parser_command_decl__sig_has__view_x_27; obj* l_lean_parser_command_structure__field__block_has__view_x_27___lambda__1(obj*); @@ -117,6 +116,9 @@ obj* l_lean_parser_parsec__t_lookahead___at_lean_parser_command_doc__comment_par obj* l_lean_parser_command_infer__modifier_parser___closed__1; obj* l_lean_parser_command_structure__field__block_has__view_x_27___lambda__1___closed__2; obj* l_lean_parser_command_constant__keyword; +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_lean_parser_monad__parsec_error___at_lean_parser_command_doc__comment_parser_lean_parser_has__view___spec__4___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_command_infer__modifier_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_command_structure_parser_lean_parser_has__tokens; @@ -150,6 +152,9 @@ obj* l_lean_parser_command_inst__implicit__binder_has__view_x_27___lambda__1___c obj* l_lean_parser_combinators_optional___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__view___spec__1(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_command_struct__implicit__binder_has__view; obj* l_lean_parser_command_instance; +namespace lean { +obj* string_iterator_next(obj*); +} extern obj* l_lean_parser_command__parser__m_monad___closed__1; obj* l_lean_parser_command_struct__explicit__binder__content; obj* l_lean_parser_ident_parser___at_lean_parser_command_intro__rule_parser_lean_parser_has__view___spec__1(obj*, obj*, obj*, obj*); @@ -168,6 +173,9 @@ obj* l_lean_parser_command_decl__attributes_has__view; obj* l_lean_parser_command_intro__rule_parser_lean_parser_has__view; obj* l_lean_parser_command_struct__explicit__binder__content_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_def__like_kind_has__view_x_27___lambda__1(obj*); +namespace lean { +obj* string_length(obj*); +} obj* l_lean_parser_command_struct__implicit__binder_has__view_x_27___lambda__1___closed__2; obj* l_lean_parser_command_old__univ__params_parser(obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_any___at_lean_parser_command_doc__comment_parser_lean_parser_has__view___spec__5(obj*, obj*, obj*, obj*); @@ -178,9 +186,15 @@ obj* l_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens; obj* l_lean_parser_command_intro__rule_has__view; obj* l_lean_parser_command_structure_has__view_x_27; obj* l_lean_parser_command_structure_has__view_x_27___lambda__2(obj*); +namespace lean { +uint32 string_iterator_curr(obj*); +} obj* l_lean_parser_command_strict__implicit__binder_has__view_x_27; obj* l_lean_parser_command_structure__kw_has__view_x_27___lambda__1___closed__4; obj* l_lean_parser_command_declaration_inner; +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_lean_parser_command_extends_has__view; extern obj* l_lean_parser_term_binder__content_has__view_x_27___lambda__2___closed__2; obj* l_lean_parser_command_visibility_has__view_x_27___lambda__1(obj*); @@ -247,6 +261,9 @@ obj* l_lean_parser_command_relaxed__infer__modifier_has__view; obj* l_lean_parser_command_decl__sig_has__view; obj* l_lean_parser_command_decl__val_has__view; obj* l_lean_parser_command_structure_has__view_x_27___lambda__1___closed__3; +namespace lean { +uint8 string_iterator_has_next(obj*); +} obj* l_lean_parser_command_structure__field__block_has__view_x_27; obj* l_lean_parser_command_struct__binder__content_parser_lean_parser_has__tokens; obj* l_lean_parser_command_strict__infer__modifier_has__view_x_27___lambda__1___closed__1; @@ -255,6 +272,7 @@ obj* l_lean_parser_symbol_tokens___rarg(obj*, obj*); obj* l_lean_parser_command_structure_has__view_x_27___lambda__1___closed__2; extern obj* l_lean_parser_term_bracketed__binders_has__view; obj* l_lean_parser_command_declaration_has__view_x_27___lambda__1(obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_parser_command_decl__attributes_parser(obj*, obj*, obj*, obj*); obj* l_lean_parser_command_inductive_has__view_x_27___lambda__2___closed__1; obj* l_lean_parser_command_instance_has__view; @@ -349,6 +367,9 @@ obj* l_lean_parser_command_structure; obj* l_lean_parser_command_structure__field__block_has__view; extern obj* l_lean_parser_term_binder__content_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_command_struct__implicit__binder_has__view_x_27___lambda__2(obj*); +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} extern obj* l___private_init_lean_parser_token_1__finish__comment__block__aux___main___closed__2; extern obj* l_lean_parser_term_binder__default_parser_lean_parser_has__tokens; obj* l_lean_parser_command_structure__field__block_parser(obj*, obj*, obj*, obj*); @@ -358,6 +379,9 @@ obj* l_lean_parser_command_extends_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_opt__decl__sig_parser_lean_parser_has__view; obj* l_lean_parser_command_constant__keyword_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_command_decl__sig_has__view_x_27___lambda__1___closed__3; +namespace lean { +uint8 string_dec_eq(obj*, obj*); +} obj* l_lean_parser_combinators_sep__by1___at_lean_parser_command_decl__attributes_parser_lean_parser_has__view___spec__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_command_constant_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_attr__instance_has__view; @@ -377,6 +401,12 @@ obj* l_lean_parser_command_extends_has__view_x_27___lambda__1___closed__2; obj* l_lean_parser_command_simple__decl__val_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_command_struct__explicit__binder_has__view_x_27___lambda__1(obj*); obj* l_list_map___main___at_lean_parser_command_attr__instance_has__view_x_27___spec__5(obj*); +namespace lean { +obj* string_iterator_remaining(obj*); +} +namespace lean { +obj* string_mk_iterator(obj*); +} obj* l_lean_parser_command_constant_has__view_x_27; obj* l_lean_parser_command_strict__infer__modifier_has__view_x_27; obj* l_list_map___main___at_lean_parser_command_attr__instance_has__view_x_27___spec__2(obj*); @@ -425,6 +455,9 @@ obj* l_lean_parser_command_struct__binder__content; obj* l_lean_parser_command_univ__params; obj* l_lean_parser_command_declaration_inner_has__view_x_27; obj* l_lean_parser_command_struct__binder__content_has__view_x_27; +namespace lean { +obj* name_mk_numeral(obj*, obj*); +} obj* l_lean_parser_command_structure_parser_lean_parser_has__view; obj* l_lean_parser_monad__parsec_many1__aux_x_27___main___at_lean_parser_command_doc__comment_parser_lean_parser_has__tokens___spec__3(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_command_univ__params_has__view_x_27___lambda__1(obj*); @@ -448,6 +481,7 @@ obj* l_lean_parser_command_infer__modifier_parser_lean_parser_has__view___lambda obj* l_lean_parser_command_notation__like_parser(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_command_decl__val_parser_lean_parser_has__tokens; obj* l_lean_parser_command_decl__sig_parser(obj*, obj*, obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l_lean_parser_command_ident__univ__params_has__view_x_27___lambda__1___closed__5; obj* l_lean_parser_command_declaration_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_command_infer__modifier_has__view_x_27___lambda__1___closed__1; diff --git a/src/boot/init/lean/parser/identifier.cpp b/src/boot/init/lean/parser/identifier.cpp index 38c6697665..c746abec81 100644 --- a/src/boot/init/lean/parser/identifier.cpp +++ b/src/boot/init/lean/parser/identifier.cpp @@ -3,8 +3,6 @@ // Imports: init.data.char.basic init.lean.parser.parsec #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -41,6 +39,9 @@ obj* l_lean_parser_monad__parsec_foldl__aux___main___at_lean_parser_identifier__ obj* l_lean_parser_monad__parsec_labels___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_identifier___spec__11___rarg(obj*, obj*, uint32); obj* l_lean_parser_cpp__identifier___rarg(obj*, obj*, obj*); +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_lean_parser_monad__parsec_error___at_lean_parser_c__identifier___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_identifier___spec__18(obj*, obj*, obj*); obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at_lean_parser_id__part__default___spec__4___rarg(obj*, obj*, obj*); @@ -57,6 +58,9 @@ obj* l_lean_parser_cpp__identifier___rarg___lambda__1(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_identifier___spec__18___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_id__part__escaped___spec__2(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_identifier___spec__16___rarg(obj*, obj*, uint32); +namespace lean { +obj* string_iterator_next(obj*); +} obj* l_lean_parser_monad__parsec_foldl___at_lean_parser_identifier___spec__4(obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_id__part__escaped___spec__3___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_c__identifier(obj*, obj*); @@ -73,7 +77,13 @@ uint8 l_string_is__empty(obj*); obj* l_lean_parser_monad__parsec_foldl___at_lean_parser_identifier___spec__14___rarg(obj*, obj*, obj*, obj*); uint8 l_lean_is__sub__script__alnum(uint32); uint8 l_char_is__alpha(uint32); +namespace lean { +uint32 string_iterator_curr(obj*); +} obj* l_lean_parser_monad__parsec_foldl___at_lean_parser_identifier___spec__4___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*); +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_lean_parser_monad__parsec_ch___at_lean_parser_identifier___spec__6___rarg___boxed(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_id__part__escaped___spec__4___rarg___lambda__1(obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_identifier___spec__16___rarg___lambda__1(obj*, obj*, uint32, obj*, obj*); @@ -99,10 +109,14 @@ obj* l_lean_parser_c__identifier___rarg(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while1___at_lean_parser_id__part__escaped___spec__1___rarg___lambda__1(obj*, obj*, obj*, obj*); obj* l_lean_is__id__first___boxed(obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_identifier___spec__6(obj*, obj*); +namespace lean { +uint8 string_iterator_has_next(obj*); +} obj* l_lean_parser_monad__parsec_foldl__aux___main___at_lean_parser_identifier___spec__15___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_c__identifier___spec__3___rarg(obj*, uint32); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_identifier___spec__1___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_c__identifier___rarg___closed__1; +uint8 l_nat_dec__eq(obj*, obj*); obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at_lean_parser_id__part__escaped___spec__5___rarg(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_c__identifier___spec__2(obj*, obj*, obj*); extern obj* l_char_has__repr___closed__1; @@ -113,6 +127,7 @@ extern obj* l_lean_parser_monad__parsec_left__over___rarg___closed__1; extern obj* l_string_join___closed__1; obj* l_list_foldl___main___at_string_join___spec__1(obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_identifier___spec__12___rarg(obj*, obj*, obj*, obj*, obj*, obj*); +uint8 l_nat_dec__le(obj*, obj*); obj* l_lean_parser_id__part__escaped___rarg(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_foldl__aux___main___at_lean_parser_identifier___spec__20___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_identifier___rarg___lambda__1(obj*, obj*, obj*, obj*); @@ -139,6 +154,9 @@ obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_id__part__de obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_c__identifier___spec__3(obj*, obj*, obj*); obj* l_lean_parser_id__part(obj*, obj*); obj* l_lean_parser_id__part___rarg(obj*, obj*, obj*); +namespace lean { +obj* string_iterator_remaining(obj*); +} obj* l_lean_parser_monad__parsec_error___at_lean_parser_id__part__default___spec__1(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_identifier___spec__6___rarg___lambda__1(obj*, obj*, uint32, obj*, obj*); obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at_lean_parser_id__part__escaped___spec__5(obj*); @@ -159,7 +177,11 @@ uint8 l_lean_is__id__begin__escape(uint32); obj* l_lean_parser_monad__parsec_foldl__aux___main___at_lean_parser_identifier___spec__5(obj*, obj*); extern obj* l_lean_parser_monad__parsec_try___rarg___closed__1; obj* l_lean_parser_monad__parsec_ch___at_lean_parser_identifier___spec__1___rarg___lambda__1(obj*, obj*, uint32, obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_identifier___spec__8(obj*, obj*, obj*); +namespace lean { +obj* string_push(obj*, uint32); +} obj* l_dlist_singleton___rarg(obj*, obj*); obj* l_lean_parser_cpp__identifier___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_foldl__aux___main___at_lean_parser_identifier___spec__15(obj*, obj*); @@ -172,6 +194,7 @@ obj* l_lean_parser_monad__parsec_foldl___at_lean_parser_identifier___spec__9___r obj* l_lean_parser_identifier___rarg___closed__1; obj* l_char_quote__core(uint32); obj* l_lean_parser_cpp__identifier(obj*, obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* l_lean_parser_id__part___rarg___closed__1; obj* l_lean_parser_monad__parsec_error___at_lean_parser_c__identifier___spec__2___rarg(obj*, obj*, obj*, obj*, obj*, obj*); uint8 l_lean_is__greek(uint32 x_0) { diff --git a/src/boot/init/lean/parser/level.cpp b/src/boot/init/lean/parser/level.cpp index 86093168f6..9b1bdbcc54 100644 --- a/src/boot/init/lean/parser/level.cpp +++ b/src/boot/init/lean/parser/level.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.parser.pratt #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -32,6 +30,7 @@ obj* l_lean_parser_level_trailing_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_level_paren_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_level_leading_has__view; obj* l_lean_parser_level__parser; +obj* l_nat_add(obj*, obj*); obj* l_lean_parser_level__parser__m_lean_parser_monad__parsec; extern obj* l_mjoin___rarg___closed__1; extern obj* l_lean_parser_basic__parser__m_monad; @@ -47,6 +46,9 @@ obj* l_lean_parser_level_leading_has__view_x_27___lambda__1___closed__2; obj* l_lean_parser_parsec__t_try__mk__res___rarg(obj*); obj* l_lean_parser_level_add__lit_parser(obj*, obj*, obj*, obj*, obj*); obj* l_list_reverse___rarg(obj*); +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_reader__t_alternative___rarg(obj*, obj*); obj* l_lean_parser_combinators_node___at_lean_parser_level_paren_parser___spec__1(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_level_parser___closed__1; @@ -109,6 +111,7 @@ obj* l_lean_parser_ident_parser___at_lean_parser_level_leading_parser_lean_parse obj* l_lean_parser_symbol_tokens___rarg(obj*, obj*); obj* l_lean_parser_pratt__parser___at_lean_parser_level__parser_run___spec__1(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_level_leading_parser_lean_parser_has__view; +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_parser_ident_parser___at_lean_parser_level_leading_parser_lean_parser_has__view___spec__3___rarg(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_level__parser_run___spec__3___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_level_lean_parser_has__tokens; @@ -154,13 +157,25 @@ obj* l_lean_parser_level__parser_run_lean_parser_has__view___closed__3; obj* l_lean_parser_monad__parsec_error___at_lean_parser_level_trailing_parser_lean_parser_has__view___spec__2___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_level_paren_parser(obj*, obj*, obj*, obj*); obj* l_lean_parser_number_parser___at_lean_parser_level_leading_parser_lean_parser_has__view___spec__2(obj*); +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} obj* l_lean_parser_rec__t_recurse___rarg(obj*, obj*, obj*); +namespace lean { +uint8 string_dec_eq(obj*, obj*); +} obj* l_reader__t_lift(obj*, obj*, obj*, obj*); obj* l_lean_parser_level_paren_has__view; extern obj* l_lean_parser_combinators_choice__aux___main___rarg___closed__1; obj* l_lean_parser_level_leading_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_level__parser_run___spec__3(obj*); obj* l_lean_parser_level__parser_run_lean_parser_has__view___closed__2; +namespace lean { +obj* string_iterator_remaining(obj*); +} +namespace lean { +obj* string_mk_iterator(obj*); +} extern obj* l_lean_parser_basic__parser__m_alternative; obj* l_lean_parser_level_leading_has__view_x_27___lambda__1___closed__4; obj* l_lean_parser_level_leading_has__view_x_27___lambda__1___closed__3; @@ -173,6 +188,9 @@ obj* l_lean_parser_number_parser___at_lean_parser_level_leading_parser_lean_pars extern obj* l_lean_parser_curr__lbp___rarg___lambda__3___closed__1; obj* l_reader__t_monad___rarg(obj*); obj* l_lean_parser_level_leading_has__view_x_27___lambda__1___closed__5; +namespace lean { +obj* name_mk_numeral(obj*, obj*); +} obj* l_has__monad__lift__t__trans___rarg(obj*, obj*, obj*, obj*); obj* l_lean_parser_level_add__lit_has__view; obj* l_lean_parser_level_app_parser(obj*, obj*, obj*, obj*, obj*); @@ -184,6 +202,7 @@ obj* l_lean_parser_pratt__parser_view___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj* l_lean_parser_level_add__lit_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_symbol__core___at_lean_parser_level_paren_parser_lean_parser_has__view___spec__1(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_level_trailing_parser_lean_parser_has__view; +obj* l_nat_sub(obj*, obj*); obj* l_lean_parser_level_app_has__view_x_27; extern obj* l_lean_parser_detail__ident__part_has__view_x_27___lambda__2___closed__2; extern obj* l_lean_parser_basic__parser__m_lean_parser_monad__parsec; @@ -204,6 +223,7 @@ obj* l_lean_parser_combinators_choice__aux___main___at_lean_parser_level_leading obj* l_lean_parser_monad__rec_trans___rarg(obj*, obj*, obj*, obj*); obj* l_lean_parser_level_leading_parser___closed__1; obj* l_lean_parser_substring_of__string(obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* l_lean_parser_level_paren_parser_lean_parser_has__tokens; obj* l_lean_parser_level_trailing_has__view_x_27; obj* l___private_init_lean_parser_rec_1__run__aux___main___rarg(obj*, obj*, obj*, obj*); diff --git a/src/boot/init/lean/parser/module.cpp b/src/boot/init/lean/parser/module.cpp index be18550206..4d5ad123c5 100644 --- a/src/boot/init/lean/parser/module.cpp +++ b/src/boot/init/lean/parser/module.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.parser.command init.control.coroutine #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -39,6 +37,7 @@ obj* l___private_init_lean_parser_module_1__commands__aux___main___lambda__15___ obj* l_lean_parser_module_yield__command___lambda__8(obj*, obj*, obj*, obj*); obj* l___private_init_lean_parser_module_1__commands__aux___main___lambda__11___closed__2; obj* l___private_init_lean_parser_module_1__commands__aux___main___lambda__3___closed__1; +obj* l_nat_add(obj*, obj*); obj* l_lean_parser_module_tokens; obj* l_list_map___main___at_lean_parser_module_commands_parser_has__view___spec__2(obj*); obj* l_lean_parser_module_header_has__view_x_27___lambda__1___closed__2; @@ -64,6 +63,9 @@ obj* l___private_init_lean_parser_module_1__commands__aux___main___boxed(obj*, o extern obj* l_lean_parser_monad__parsec_eoi___rarg___lambda__1___closed__1; obj* l_lean_parser_log__message___at___private_init_lean_parser_module_1__commands__aux___main___spec__5(obj*, obj*, obj*, obj*); obj* l_lean_parser_module_header_has__view_x_27___lambda__2___closed__1; +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_lean_parser_module_import; obj* l_lean_parser_module__parser__m_monad__coroutine; obj* l_lean_parser_parsec__t_labels__mk__res___rarg(obj*, obj*); @@ -75,6 +77,9 @@ obj* l_string_quote(obj*); extern obj* l_lean_parser_monad__parsec_eoi__error___rarg___closed__1; obj* l_lean_parser_module_header_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_log__message___at___private_init_lean_parser_module_1__commands__aux___main___spec__4___lambda__2(obj*, obj*); +namespace lean { +obj* string_iterator_next(obj*); +} obj* l___private_init_lean_parser_module_1__commands__aux___main___lambda__16(obj*, obj*); obj* l_lean_parser_message__of__parsec__message___rarg(obj*, obj*); obj* l___private_init_lean_parser_module_1__commands__aux___main___lambda__10(obj*); @@ -88,6 +93,9 @@ obj* l_state__t_monad__state___rarg(obj*); obj* l___private_init_lean_parser_module_1__commands__aux___main___lambda__2(obj*); obj* l_list_map___main___at_lean_parser_module_commands_parser_has__view___spec__1(obj*); obj* l___private_init_lean_parser_module_1__commands__aux___main___lambda__9___closed__1; +namespace lean { +uint32 string_iterator_curr(obj*); +} obj* l_lean_parser_module__parser__m_monad__reader; obj* l_lean_parser_module_yield__command___lambda__2(obj*, obj*, obj*, obj*); obj* l_lean_parser_module_parser(obj*, obj*, obj*); @@ -96,6 +104,9 @@ obj* l_lean_parser_module__parser__m_lift__parser__t___rarg___lambda__3(obj*, ob obj* l_lean_parser_combinators_optional___at_lean_parser_module_header_parser_lean_parser_has__tokens___spec__1(obj*, obj*, obj*, obj*); extern obj* l_lean_parser_command_parser___rarg___closed__1; obj* l_lean_parser_monad__parsec_any___at___private_init_lean_parser_module_1__commands__aux___main___spec__3___closed__1; +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_lean_parser_module_import_has__view_x_27___lambda__1___closed__2; obj* l_function_comp___rarg(obj*, obj*, obj*); obj* l_lean_parser_module__parser__config__coe(obj*); @@ -112,6 +123,9 @@ obj* l___private_init_lean_parser_module_1__commands__aux___main___lambda__17(ui obj* l_reader__t_bind___at_lean_parser_with__trailing___spec__2___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_module_parser___lambda__10(obj*); obj* l_lean_parser_module_import_has__view_x_27___lambda__1___closed__1; +namespace lean { +obj* string_iterator_to_end(obj*); +} obj* l_lean_parser_module_prelude_has__view; obj* l_lean_parser_combinators_many1___at_lean_parser_ident__univ__spec_parser_lean_parser_has__view___spec__1(obj*, obj*, obj*, obj*); obj* l_lean_parser_tokens___rarg(obj*); @@ -126,10 +140,14 @@ obj* l_lean_parser_module_eoi; obj* l_lean_parser_module_prelude_parser_lean_parser_has__tokens; obj* l_monad__coroutine__trans___rarg(obj*, obj*, obj*); obj* l_lean_parser_module_import_parser_lean_parser_has__view; +namespace lean { +uint8 string_iterator_has_next(obj*); +} obj* l_lean_parser_module__parser__m_monad__state; obj* l_lean_parser_module_prelude_parser(obj*, obj*, obj*); obj* l_lean_parser_symbol_tokens___rarg(obj*, obj*); extern obj* l_lean_message__log_empty; +uint8 l_nat_dec__eq(obj*, obj*); obj* l___private_init_lean_parser_module_1__commands__aux___main___lambda__9(obj*, obj*, obj*); obj* l_lean_parser_mk__raw__res(obj*, obj*); obj* l_lean_parser_module_import__path_parser_lean_parser_has__view; @@ -168,6 +186,9 @@ obj* l_lean_parser_module_commands_parser(obj*, obj*, obj*); obj* l_lean_parser_module_parser___lambda__2(obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec__trans___rarg(obj*, obj*, obj*); obj* l_lean_parser_module_parser___lambda__5___closed__1; +namespace lean { +obj* string_iterator_offset(obj*); +} obj* l_lean_parser_module_import_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_module_parser___lambda__7(obj*, obj*); obj* l_state__t_monad___rarg(obj*); @@ -193,6 +214,9 @@ obj* l_lean_parser_module_import__path_has__view_x_27___lambda__1___closed__2; obj* l_lean_parser_module_commands_parser___closed__2; obj* l_list_map___main___at_lean_parser_module_import__path_has__view_x_27___spec__2(obj*); obj* l_lean_parser_module_import__path_has__view_x_27___lambda__1___closed__1; +namespace lean { +obj* string_iterator_remaining(obj*); +} extern obj* l_lean_parser_basic__parser__m_alternative; obj* l_lean_parser_module_import_parser(obj*, obj*, obj*); obj* l___private_init_lean_parser_module_1__commands__aux___main___lambda__7(obj*); @@ -227,6 +251,7 @@ obj* l_lean_parser_log__message___at___private_init_lean_parser_module_1__comman obj* l_lean_parser_module_header_parser___closed__1; obj* l_lean_parser_module__parser__m_basic__parser__m(obj*, obj*); obj* l_lean_parser_module_import__path_has__view; +obj* l_nat_sub(obj*, obj*); obj* l___private_init_lean_parser_module_1__commands__aux___main___lambda__13___boxed(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_log__message___at___private_init_lean_parser_module_1__commands__aux___main___spec__4(obj*, obj*, obj*, obj*); obj* l_lean_parser_parsec__t_has__monad__lift___rarg(obj*, obj*, obj*, obj*, obj*); diff --git a/src/boot/init/lean/parser/notation.cpp b/src/boot/init/lean/parser/notation.cpp index bf61d79303..ecfe2df7f7 100644 --- a/src/boot/init/lean/parser/notation.cpp +++ b/src/boot/init/lean/parser/notation.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.parser.token #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -45,6 +43,7 @@ obj* l_lean_parser_command_notation__spec_precedence_parser_lean_parser_has__tok obj* l_lean_parser_command_reserve__notation_has__view; obj* l_lean_parser_command_notation__spec_precedence__term_parser_lean_parser_has__view; obj* l_lean_parser_command_notation__spec_mixfix__symbol_has__view_x_27___lambda__1___closed__3; +obj* l_nat_add(obj*, obj*); obj* l_lean_parser_combinators_choice__aux___main___at_lean_parser_command_notation__spec_precedence__lit_parser_lean_parser_has__view___spec__3(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_command_notation__spec_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_notation__spec_symbol__quote_has__view_x_27___lambda__1(obj*); @@ -78,6 +77,9 @@ obj* l_lean_parser_command_notation__spec_precedence_has__view_x_27___lambda__1_ obj* l_lean_parser_command_notation__spec_notation__symbol_parser_lean_parser_has__tokens; obj* l_list_reverse___rarg(obj*); obj* l_lean_parser_command_notation__spec_precedence__offset__op_has__view_x_27___lambda__1(obj*); +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_lean_parser_command_notation__spec_notation__symbol_has__view; obj* l_lean_parser_command_mixfix_has__view; obj* l_lean_parser_command_notation__spec_precedence_parser___closed__1; @@ -99,6 +101,9 @@ obj* l_lean_parser_command_notation_has__view_x_27; obj* l_string_quote(obj*); obj* l_lean_parser_command_notation_parser___closed__1; obj* l_lean_parser_command_notation__spec_fold__action; +namespace lean { +obj* string_iterator_next(obj*); +} obj* l_lean_parser_combinators_optional___at_lean_parser_command_notation__spec_symbol__quote_parser_lean_parser_has__view___spec__7(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_command_notation__spec_precedence__term_view_to__nat___main(obj*); obj* l_lean_parser_command_notation__spec_action__kind; @@ -118,11 +123,17 @@ obj* l_lean_parser_combinators_any__of___at_lean_parser_command_notation__spec_f obj* l_lean_parser_command_notation__spec_action_has__view_x_27___lambda__1___closed__2; obj* l_lean_parser_command_notation__spec; obj* l_lean_parser_command_notation__spec_rule_parser_lean_parser_has__tokens; +namespace lean { +obj* string_length(obj*); +} obj* l_lean_parser_command_notation_parser_lean_parser_has__tokens; uint8 l_string_is__empty(obj*); obj* l_lean_parser_command_notation__like_parser_lean_parser_has__tokens; obj* l_lean_parser_command_notation__spec_action_has__view; obj* l_lean_parser_command_notation__spec_precedence__lit_parser(obj*, obj*, obj*, obj*, obj*); +namespace lean { +uint32 string_iterator_curr(obj*); +} obj* l_lean_parser_command_notation__spec_parser_lean_parser_has__view; obj* l_lean_parser_command_notation__spec_precedence__offset__op_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_mixfix_parser_lean_parser_has__view; @@ -179,6 +190,9 @@ obj* l_lean_parser_command_notation__spec_precedence__offset__op_has__view_x_27_ obj* l_lean_parser_command_notation__spec_fold__action_parser(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_command_mixfix_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_command_notation__spec_unquoted__symbol_parser(obj*, obj*, obj*, obj*, obj*); +namespace lean { +uint8 string_iterator_has_next(obj*); +} obj* l_lean_parser_command_notation__spec_precedence__offset_has__view_x_27; obj* l_lean_parser_command_notation__spec_symbol__quote_parser_lean_parser_has__view___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_list_foldl___main___at_lean_parser_command_notation__spec_fold__action_parser_lean_parser_has__view___spec__3(obj*, obj*, obj*, obj*, obj*, obj*, obj*); @@ -186,6 +200,7 @@ obj* l_lean_parser_command_notation__spec_precedence__term_has__view_x_27___lamb obj* l_lean_parser_symbol_tokens___rarg(obj*, obj*); obj* l_lean_parser_command_mixfix_kind_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_command_notation__spec_transition_has__view_x_27___lambda__2(obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_parser_command_notation__like_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_raw_view___rarg___lambda__1(obj*); extern obj* l_lean_parser_term__parser__m_lean_parser_monad__parsec; @@ -268,6 +283,9 @@ obj* l_lean_parser_command_notation__spec_fold__action__folder; obj* l_lean_parser_substring_to__string(obj*); obj* l_lean_parser_command_notation__like_parser_lean_parser_has__view; obj* l_reader__t_orelse___at_lean_parser_command_notation__spec_fold__action_parser_lean_parser_has__view___spec__2(obj*); +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} obj* l_lean_parser_command_mixfix_has__view_x_27; obj* l_lean_parser_command_notation__spec_symbol__quote_parser_lean_parser_has__view___lambda__1___closed__1; obj* l_lean_parser_command_mixfix_kind_parser(obj*, obj*, obj*, obj*, obj*); @@ -275,6 +293,9 @@ obj* l_lean_parser_command_notation__spec_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_command_notation_parser_lean_parser_has__view; obj* l_lean_parser_command_notation__spec_fold__action_has__view_x_27___lambda__1___closed__2; obj* l_lean_parser_command_notation__spec_precedence_parser(obj*, obj*, obj*, obj*, obj*); +namespace lean { +uint8 string_dec_eq(obj*, obj*); +} obj* l_lean_parser_command_notation__spec_precedence__offset_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_command_notation__spec_action_parser(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_command_notation__spec_precedence__offset; @@ -286,7 +307,13 @@ obj* l_lean_parser_command_notation__spec_rule; obj* l_lean_parser_command_notation__spec_parser___closed__1; obj* l_lean_parser_command_notation__like_has__view_x_27; obj* l_lean_parser_command_notation__spec_mixfix__symbol_parser(obj*, obj*, obj*, obj*, obj*); +namespace lean { +obj* string_iterator_remaining(obj*); +} obj* l_lean_parser_command_mixfix_kind_has__view_x_27___lambda__1___closed__7; +namespace lean { +obj* string_mk_iterator(obj*); +} obj* l_lean_parser_command_notation__spec_notation__symbol; obj* l_lean_parser_command_notation__spec_action_has__view_x_27; obj* l_lean_parser_command_notation__spec_precedence__offset__op_has__view_x_27___lambda__1___closed__4; @@ -332,6 +359,9 @@ obj* l_lean_parser_command_mixfix_kind_has__view; obj* l_lean_parser_command_notation__spec_mixfix__symbol_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_command_reserve__mixfix_parser___closed__1; obj* l_lean_parser_command_notation__spec_mixfix__symbol_has__view; +namespace lean { +obj* name_mk_numeral(obj*, obj*); +} obj* l_lean_parser_command_notation__spec_notation__symbol_has__view_x_27; obj* l_lean_parser_command_notation__spec_parser(obj*, obj*, obj*, obj*, obj*); obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at_lean_parser_command_notation__spec_quoted__symbol_parser_lean_parser_has__tokens___spec__2(obj*, obj*, obj*); @@ -357,10 +387,14 @@ obj* l_lean_parser_command_reserve__notation_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_command_notation__spec_mixfix__symbol_parser___closed__1; obj* l_lean_parser_command_notation__spec_quoted__symbol_parser_lean_parser_has__view; obj* l_lean_parser_command_notation__spec_has__view; +obj* l_nat_sub(obj*, obj*); obj* l_lean_parser_command_notation__spec_precedence__term_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_command_notation__spec_binder; obj* l_lean_parser_command_notation__spec_quoted__symbol_parser(obj*, obj*, obj*, obj*, obj*); extern obj* l_lean_parser_detail__ident__part_has__view_x_27___lambda__2___closed__2; +namespace lean { +obj* string_push(obj*, uint32); +} obj* l_dlist_singleton___rarg(obj*, obj*); obj* l_lean_parser_command_notation__spec_precedence__term_has__view; obj* l_lean_parser_command_notation__spec_has__view_x_27___lambda__1___closed__4; @@ -395,6 +429,7 @@ obj* l_lean_parser_command_notation__spec_argument_has__view_x_27___lambda__2(ob obj* l_lean_parser_command_notation__spec_action_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_command_notation__spec_action_has__view_x_27___lambda__1___closed__3; obj* l_lean_parser_command_notation__spec_transition_parser(obj*, obj*, obj*, obj*, obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* l_lean_parser_command_notation__spec_precedence__offset__op_has__view; obj* l_lean_parser_rec__t_recurse___at_lean_parser_term_parser_lean_parser_has__view___spec__1(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_command_notation__spec_precedence_has__view_x_27___lambda__1___closed__2; diff --git a/src/boot/init/lean/parser/parsec.cpp b/src/boot/init/lean/parser/parsec.cpp index 13c7eb5af2..044cf8f427 100644 --- a/src/boot/init/lean/parser/parsec.cpp +++ b/src/boot/init/lean/parser/parsec.cpp @@ -3,8 +3,6 @@ // Imports: init.data.to_string init.data.string.basic init.data.list.basic init.control.except init.data.repr init.lean.name init.data.dlist init.control.monad_fail init.control.combinators #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -67,6 +65,7 @@ obj* l_lean_parser_parsec__t_monad__except___rarg(obj*, obj*); obj* l_lean_parser_parsec__t_run___at_lean_parser_parsec__t_parse__with__left__over___spec__1(obj*); obj* l_lean_parser_monad__parsec_sep__by1___rarg___closed__1; obj* l_lean_parser_monad__parsec_curr___rarg(obj*, obj*); +obj* l_nat_add(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*); @@ -131,6 +130,9 @@ obj* l_lean_parser_parsec__t_run___at_lean_parser_parsec__t_parse__with__eoi___s obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_ch___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_list_zip___rarg___lambda__1(obj*, obj*); obj* l_lean_parser_monad__parsec_left__over___rarg___lambda__1(obj*); +namespace lean { +obj* string_iterator_next(obj*); +} obj* l_lean_parser_monad__parsec_pos___rarg___closed__1; obj* l_lean_parser_lean_parser_monad__parsec___rarg___lambda__1(obj*, obj*, obj*, obj*); obj* l___private_init_lean_parser_parsec_5__mk__consumed__result(obj*); @@ -147,6 +149,9 @@ obj* l_lean_parser_monad__parsec_take__while__cont___rarg(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while_x_27___rarg(obj*, obj*); obj* l_lean_parser_monad__parsec_eoi___rarg___lambda__1(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_not__followed__by___rarg___lambda__3(obj*, obj*, obj*, obj*, obj*, obj*, obj*); +namespace lean { +obj* string_length(obj*); +} obj* l_lean_parser_monad__parsec_eoi(obj*, obj*); obj* l_lean_parser_monad__parsec_not__followed__by___rarg___lambda__2___boxed(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_many1___rarg(obj*, obj*, obj*, obj*, obj*); @@ -164,10 +169,16 @@ obj* l_list_mfoldr___main___at_lean_parser_monad__parsec_longest__match___spec__ uint8 l_char_is__alpha(uint32); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_monad__parsec_take__until1___spec__4___rarg___lambda__1(obj*, obj*, obj*); obj* l_lean_parser_parsec__t_run(obj*); +namespace lean { +uint32 string_iterator_curr(obj*); +} obj* l_lean_parser_monad__parsec_upper(obj*, obj*); obj* l_lean_parser_monad__parsec_left__over___rarg(obj*); obj* l_lean_parser_monad__parsec_take__until(obj*, obj*); obj* l_lean_parser_monad__parsec_not__followed__by__sat___rarg(obj*, obj*, obj*); +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_lean_parser_parsec__t_monad__except___rarg___lambda__4(obj*, obj*, obj*, obj*, obj*); obj* l_function_comp___rarg(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_not__followed__by__sat(obj*, obj*); @@ -219,6 +230,9 @@ obj* l___private_init_lean_parser_parsec_3__mk__string__result(obj*); obj* l_lean_parser_monad__parsec_lower___rarg(obj*, obj*); obj* l_lean_parser_parsec__t_monad__except___rarg___lambda__1(obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while1___at_lean_parser_monad__parsec_num___spec__1___rarg___lambda__1(obj*, obj*, obj*, obj*); +namespace lean { +uint8 string_iterator_has_next(obj*); +} obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_satisfy___spec__2(obj*, obj*, obj*); obj* l_lean_parser_lean_parser_monad__parsec___rarg(obj*); obj* l_lean_parser_parsec_message_text___rarg___closed__1; @@ -228,6 +242,7 @@ obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_not__follo obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_eoi___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_parsec__t_parse__with__left__over(obj*, obj*); obj* l_lean_parser_monad__parsec_eoi__error___rarg(obj*); +uint8 l_nat_dec__eq(obj*, obj*); extern obj* l_lean_format_be___main___closed__1; obj* l_string_line__column(obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_upper___spec__1(obj*, obj*, obj*); @@ -260,6 +275,7 @@ 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_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_lower___spec__1(obj*, obj*, obj*); obj* l_lean_parser_parsec__t_monad___rarg___lambda__13(obj*, obj*, obj*, obj*, obj*, obj*); +uint8 l_nat_dec__le(obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_parsec__t_parse__with__eoi___spec__2___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_str__core___rarg(obj*, obj*, obj*, obj*); obj* l_lean_parser_parsec__t_pure(obj*); @@ -303,6 +319,9 @@ obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_num___spec obj* l_lean_parser_parsec__t_monad___rarg___lambda__1(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_many1__aux_x_27___main___rarg(obj*, obj*, obj*); obj* l_lean_parser_parsec_message_text___rarg(obj*); +namespace lean { +obj* string_iterator_offset(obj*); +} obj* l_lean_parser_monad__parsec_foldl(obj*, obj*); obj* l_lean_parser_monad__parsec_hidden___rarg___lambda__1(obj*, obj*); obj* l_lean_parser_monad__parsec_lookahead___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*); @@ -345,6 +364,9 @@ obj* l___private_init_lean_parser_parsec_6__take__while__aux_x_27___main___rarg_ obj* l_lean_parser_parsec__t_monad___rarg___lambda__4(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_num___rarg(obj*, obj*); obj* l_lean_parser_monad__parsec__trans___rarg___lambda__3(obj*, obj*, obj*, obj*, obj*); +namespace lean { +uint8 string_dec_eq(obj*, obj*); +} obj* l_lean_parser_parsec__t_orelse___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_eoi___at_lean_parser_parsec__t_parse__with__eoi___spec__1(obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_fix__aux___main___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*); @@ -358,6 +380,12 @@ obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_alpha___sp obj* l_lean_parser_parsec__t_labels___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_parsec__t_try__mk__res(obj*, obj*); obj* l_lean_parser_monad__parsec_many1__aux___main___rarg___lambda__3(obj*, obj*); +namespace lean { +obj* string_iterator_remaining(obj*); +} +namespace lean { +obj* string_mk_iterator(obj*); +} obj* l_lean_parser_monad__parsec_take(obj*, obj*); obj* l___private_init_lean_parser_parsec_6__take__while__aux_x_27___main___rarg(obj*, obj*, uint8, obj*); obj* l_lean_parser_monad__parsec_longest__match___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*, obj*, obj*); @@ -424,6 +452,7 @@ obj* l_lean_parser_monad__parsec_upper___rarg(obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_any___spec__2(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_upper___spec__2(obj*, obj*, obj*); obj* l_lean_parser_parsec__t_parse__with__left__over___rarg___lambda__1(obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l_lean_parser_monad__parsec_take__while(obj*, obj*, obj*); obj* l_lean_parser_parsec__t_has__monad__lift___rarg(obj*, obj*, obj*, obj*, obj*); obj* l___private_init_lean_parser_parsec_2__take__aux___main(obj*); @@ -433,6 +462,9 @@ obj* l_lean_parser_parsec_expected_to__string___main___closed__1; obj* l_lean_parser_monad__parsec_many1__aux_x_27___rarg(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while1___at_lean_parser_monad__parsec_num___spec__1___rarg(obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_monad__parsec_take__while1___spec__2___rarg(obj*, obj*, obj*, obj*, obj*, obj*); +namespace lean { +obj* string_push(obj*, uint32); +} obj* l_lean_parser_parsec_message_to__string___rarg___closed__1; obj* l_lean_parser_monad__parsec_many1_x_27___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_dlist_singleton___rarg(obj*, obj*); @@ -453,6 +485,9 @@ obj* l_lean_parser_parsec__t_parse__with__left__over___rarg(obj*, obj*, obj*, ob obj* l_lean_parser_parsec__t_monad__except___rarg___lambda__3(obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_x_27; obj* l_lean_parser_parsec__t_alternative___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*); +namespace lean { +obj* string_iterator_to_string(obj*); +} obj* l_lean_parser_parsec__t_try___rarg___lambda__1(obj*, obj*); obj* l___private_init_lean_parser_parsec_1__str__aux(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__until1(obj*, obj*); @@ -464,6 +499,7 @@ 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_many_x_27___rarg(obj*, obj*, obj*, obj*, obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* l_lean_parser_monad__parsec_take__while_x_27___at_lean_parser_monad__parsec_whitespace___spec__1___rarg___closed__1; obj* l_lean_parser_parsec__t_monad___rarg___lambda__3(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_not__followed__by___rarg___lambda__1(obj*, obj*); diff --git a/src/boot/init/lean/parser/pratt.cpp b/src/boot/init/lean/parser/pratt.cpp index 6a873237ab..36b85477cf 100644 --- a/src/boot/init/lean/parser/pratt.cpp +++ b/src/boot/init/lean/parser/pratt.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.parser.token #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -21,11 +19,15 @@ obj* l_lean_parser_curr__lbp(obj*); obj* l_lean_parser_trie_match__prefix___rarg(obj*, obj*); obj* l_lean_parser_pratt__parser(obj*); obj* l___private_init_lean_parser_pratt_1__trailing__loop___main___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); +obj* l_nat_add(obj*, obj*); obj* l_lean_parser_monad__parsec_error___at___private_init_lean_parser_pratt_1__trailing__loop___main___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*); extern obj* l_mjoin___rarg___closed__1; obj* l_lean_parser_rec__t_run__parsec___at_lean_parser_pratt__parser___spec__1(obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_curr__lbp___spec__2(obj*, obj*); extern obj* l_lean_parser_rec__t_run__parsec___rarg___lambda__1___closed__1; +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_lean_parser_monad__parsec_error___at_lean_parser_pratt__parser___spec__2___rarg(obj*, obj*, obj*, obj*, obj*, obj*); extern obj* l___private_init_lean_parser_combinators_1__many1__aux___main___rarg___closed__1; obj* l_lean_parser_rec__t_run__parsec___at_lean_parser_pratt__parser___spec__1___rarg(obj*, obj*, obj*, obj*); @@ -39,6 +41,7 @@ obj* l_lean_parser_curr__lbp___rarg___lambda__3(obj*, obj*, obj*, obj*, obj*, ob obj* l_lean_parser_rec__t_run___at_lean_parser_pratt__parser___spec__3(obj*, obj*); obj* l_lean_parser_pratt__parser_view(obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_curr__lbp___spec__3___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_parser_pratt__parser_tokens(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l___private_init_lean_parser_pratt_1__trailing__loop(obj*); extern obj* l_lean_parser_monad__parsec_left__over___rarg___closed__1; @@ -52,7 +55,16 @@ extern obj* l_lean_parser_indexed___rarg___closed__1; obj* l_lean_parser_pratt__parser___rarg___lambda__3(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_curr__lbp___rarg___lambda__3___closed__2; obj* l_lean_parser_curr__lbp___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*); +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} obj* l___private_init_lean_parser_pratt_1__trailing__loop___main___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); +namespace lean { +obj* string_iterator_remaining(obj*); +} +namespace lean { +obj* string_mk_iterator(obj*); +} obj* l_lean_parser_curr__lbp___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_curr__lbp___rarg___lambda__3___closed__1; obj* l___private_init_lean_parser_rec_1__run__aux___rarg(obj*, obj*, obj*, obj*); @@ -62,11 +74,13 @@ obj* l_lean_parser_monad__parsec_error___at_lean_parser_curr__lbp___spec__1(obj* obj* l_lean_parser_pratt__parser_view___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l___private_init_lean_parser_pratt_1__trailing__loop___main___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l___private_init_lean_parser_pratt_1__trailing__loop___main(obj*); +obj* l_nat_sub(obj*, obj*); obj* l_list_append___rarg(obj*, obj*); extern obj* l_lean_parser_number_has__view_x_27___lambda__1___closed__6; obj* l_lean_parser_pratt__parser___rarg___lambda__2(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_pratt__parser___spec__2(obj*, obj*); obj* l_lean_parser_rec__t_run___at_lean_parser_pratt__parser___spec__3___rarg(obj*, obj*, obj*, obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_curr__lbp___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: { diff --git a/src/boot/init/lean/parser/rec.cpp b/src/boot/init/lean/parser/rec.cpp index edb1e7bc96..8f0528ec06 100644 --- a/src/boot/init/lean/parser/rec.cpp +++ b/src/boot/init/lean/parser/rec.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.parser.parsec #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -19,6 +17,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; obj* l_lean_parser_monad__parsec_error___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*); obj* l___private_init_lean_parser_rec_1__run__aux(obj*, obj*, obj*, obj*); obj* l_lean_parser_rec__t_recurse(obj*, obj*, obj*); +obj* l_nat_add(obj*, obj*); obj* l_lean_parser_rec__t_alternative___rarg(obj*, obj*); obj* l_lean_parser_rec__t_run__parsec___rarg___lambda__1(obj*, obj*, obj*); obj* l_lean_parser_rec__t_monad__functor(obj*, obj*, obj*, obj*); @@ -39,6 +38,7 @@ obj* l_lean_parser_rec__t_run__parsec___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_rec__t_monad__except(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_rec__t_run___rarg(obj*, obj*, obj*, obj*); obj* l_lean_parser_rec__t_monad__functor___rarg(obj*); +uint8 l_nat_dec__eq(obj*, obj*); extern obj* l_lean_parser_monad__parsec_left__over___rarg___closed__1; obj* l_lean_parser_rec__t_alternative(obj*, obj*, obj*); obj* l_lean_parser_rec__t_lean_parser_monad__parsec___rarg(obj*, obj*, obj*); @@ -51,6 +51,9 @@ obj* l_lean_parser_rec__t_run__parsec___rarg___lambda__2(obj*, obj*, obj*, obj*, obj* l_lean_parser_rec__t_recurse___rarg(obj*, obj*, obj*); obj* l_reader__t_lift(obj*, obj*, obj*, obj*); obj* l_lean_parser_rec__t_run(obj*, obj*, obj*, obj*, obj*); +namespace lean { +obj* string_iterator_remaining(obj*); +} obj* l_lean_parser_rec__t; obj* l_lean_parser_monad__parsec_error___at_lean_parser_rec__t_run__parsec___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l___private_init_lean_parser_rec_1__run__aux___rarg(obj*, obj*, obj*, obj*); @@ -58,6 +61,7 @@ obj* l_reader__t_monad___rarg(obj*); obj* l_lean_parser_rec__t_has__monad__lift(obj*, obj*, obj*); obj* l___private_init_lean_parser_rec_1__run__aux___main(obj*, obj*, obj*); obj* l_lean_parser_rec__t_run___at_lean_parser_rec__t_run__parsec___spec__2___rarg(obj*, obj*, obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l_lean_parser_monad__rec_trans___rarg(obj*, obj*, obj*, obj*); obj* l___private_init_lean_parser_rec_1__run__aux___main___rarg(obj*, obj*, obj*, obj*); obj* _init_l_lean_parser_rec__t() { diff --git a/src/boot/init/lean/parser/string_literal.cpp b/src/boot/init/lean/parser/string_literal.cpp index e2398842e8..e4006de514 100644 --- a/src/boot/init/lean/parser/string_literal.cpp +++ b/src/boot/init/lean/parser/string_literal.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.parser.parsec #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -22,6 +20,7 @@ obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal___sp obj* l_lean_parser_parse__string__literal__aux___main___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_parse__quoted__char___rarg___lambda__4(obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_unexpected__at___at_lean_parser_parse__quoted__char___spec__3___rarg(obj*, obj*, obj*, obj*, obj*); +obj* l_nat_add(obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal___spec__7(obj*, obj*); obj* l_lean_parser_parse__quoted__char___rarg___lambda__7___closed__1; obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal___spec__10___rarg___lambda__1(obj*, obj*, uint32, obj*, obj*); @@ -59,9 +58,15 @@ obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal___sp obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal___spec__7___rarg(obj*, obj*, uint32); obj* l_lean_parser_parse__hex__digit___rarg___lambda__1(obj*, uint32); obj* l_lean_parser_monad__parsec_error___at_lean_parser_parse__string__literal__aux___main___spec__6(obj*, obj*, obj*); +namespace lean { +uint32 string_iterator_curr(obj*); +} obj* l_lean_parser_monad__parsec_unexpected__at___at_lean_parser_parse__quoted__char___spec__5(obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal___spec__1___rarg___lambda__1(obj*, obj*, uint32, obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal__aux___main___spec__7(obj*, obj*); +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_lean_parser_monad__parsec_error___at_lean_parser_parse__string__literal___spec__12(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal___spec__4___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_parse__string__literal___spec__5___rarg(obj*, obj*, obj*, obj*, obj*, obj*); @@ -84,11 +89,15 @@ obj* l_lean_parser_parse__hex__digit___rarg___lambda__5(obj*, uint32); obj* l_lean_parser_monad__parsec_error___at_lean_parser_parse__quoted__char___spec__4(obj*, obj*, obj*); obj* l_lean_parser_parse__string__literal__aux___main___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*, uint32); obj* l_lean_parser_monad__parsec_error___at_lean_parser_parse__hex__digit___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*); +namespace lean { +uint8 string_iterator_has_next(obj*); +} obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal__aux___main___spec__4(obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_parse__quoted__char___spec__2(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_parse__string__literal__aux___main___spec__11(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal__aux___main___spec__1___rarg___lambda__1(obj*, obj*, uint32, obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal___spec__1(obj*, obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_parse__string__literal__aux___main___spec__2___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_parse__string__literal__aux___main___spec__8___rarg(obj*, obj*, obj*, obj*, obj*, obj*); extern obj* l_char_has__repr___closed__1; @@ -101,6 +110,7 @@ obj* l_lean_parser_monad__parsec_unexpected__at___at_lean_parser_parse__quoted__ obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal__aux___main___spec__1___rarg___boxed(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal___spec__10___rarg(obj*, obj*, uint32); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal___spec__4___rarg___boxed(obj*, obj*, obj*); +uint8 l_nat_dec__le(obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal__aux___main___spec__1(obj*, obj*); obj* l_lean_parser_parse__hex__digit___rarg___lambda__4(obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal__aux___main___spec__7___rarg___boxed(obj*, obj*, obj*); @@ -138,10 +148,15 @@ obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal___sp obj* l_lean_parser_monad__parsec_error___at_lean_parser_parse__hex__digit___spec__1(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal__aux___main___spec__10___rarg___boxed(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal___spec__1___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*); +obj* l_nat_mul(obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_parse__string__literal__aux___main___spec__9___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_parse__quoted__char___rarg___lambda__3(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal__aux___main___spec__7___rarg___lambda__1(obj*, obj*, uint32, obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l_lean_parser_parse__quoted__char___rarg___lambda__8(obj*, obj*, obj*, obj*, obj*); +namespace lean { +obj* string_push(obj*, uint32); +} obj* l_dlist_singleton___rarg(obj*, obj*); obj* l_lean_parser_parse__string__literal__aux___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_parse__string__literal__aux___main___spec__12___rarg(obj*, obj*, obj*, obj*, obj*, obj*); @@ -157,6 +172,7 @@ obj* l_lean_parser_monad__parsec_error___at_lean_parser_parse__string__literal__ obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal___spec__10___rarg___boxed(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_ch___at_lean_parser_parse__string__literal__aux___main___spec__10(obj*, obj*); obj* l_char_quote__core(uint32); +uint8 l_nat_dec__lt(obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_parse__quoted__char___spec__6___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_parse__string__literal___spec__2___rarg(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_parse__quoted__char___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*); diff --git a/src/boot/init/lean/parser/syntax.cpp b/src/boot/init/lean/parser/syntax.cpp index 196db60ce4..30a7abdcce 100644 --- a/src/boot/init/lean/parser/syntax.cpp +++ b/src/boot/init/lean/parser/syntax.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.name init.lean.parser.parsec #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -34,6 +32,9 @@ obj* l_lean_parser_syntax_flip__scopes___main(obj*, obj*); obj* l_lean_parser_syntax_to__format___main___closed__1; obj* l_lean_parser_syntax_get__head__info__lst(obj*); obj* l_list_reverse___rarg(obj*); +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_lean_parser_syntax_reprint__atom___main(obj*); obj* l_lean_nat__has__to__format(obj*); obj* l_lean_parser_syntax_to__format__lst(obj*); @@ -43,9 +44,15 @@ obj* l_string_quote(obj*); obj* l_lean_parser_syntax_update__leading___closed__1; obj* l_lean_parser_macro__scopes; obj* l_lean_parser_syntax_to__format___main___closed__7; +namespace lean { +obj* string_length(obj*); +} obj* l_lean_parser_syntax_mreplace__lst___main(obj*); obj* l_option_orelse___main___rarg(obj*, obj*); extern obj* l_lean_name_to__string___closed__1; +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_lean_parser_syntax_mreplace(obj*); obj* l_lean_parser_syntax_to__format___main___closed__6; obj* l_lean_parser_syntax_reprint__lst(obj*); @@ -57,6 +64,12 @@ obj* l_list_map___main___at_lean_parser_syntax_as__node___main___spec__1(obj*, o obj* l_lean_parser_syntax_to__format___main___closed__5; obj* l_lean_name_replace__prefix___main(obj*, obj*, obj*); obj* l_lean_parser_syntax_get__pos(obj*); +namespace lean { +obj* string_iterator_to_end(obj*); +} +namespace lean { +obj* string_iterator_extract(obj*, obj*); +} obj* l_lean_parser_syntax_to__format___main___closed__9; obj* l_option_get__or__else___main___rarg(obj*, obj*); obj* l_lean_name_to__string__with__sep___main(obj*, obj*); @@ -68,6 +81,7 @@ obj* l_lean_parser_syntax_get__head__info__lst___main(obj*); obj* l_lean_parser_syntax_has__to__string; obj* l_lean_parser_syntax_mreplace__lst___main___at_lean_parser_syntax_update__leading___spec__2(obj*, obj*, obj*); obj* l_lean_parser_syntax_to__format___main___closed__8; +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_parser_syntax_flip__scopes(obj*, obj*); obj* l_string_iterator_nextn___main(obj*, obj*); extern obj* l_lean_format_sbracket___closed__1; @@ -91,10 +105,19 @@ obj* l_lean_parser_syntax_lean_has__to__format; obj* l_lean_format_group___main(obj*); obj* l_lean_parser_syntax_mreplace__lst___main___at_lean_parser_syntax_replace___spec__2(obj*, obj*); extern obj* l_lean_format_paren___closed__3; +namespace lean { +obj* string_iterator_offset(obj*); +} obj* l_string_join(obj*); obj* l_lean_parser_syntax_mreplace__lst___rarg(obj*, obj*, obj*); obj* l_lean_parser_substring_to__string(obj*); +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} obj* l_lean_parser_syntax_kind___main(obj*); +namespace lean { +uint8 string_dec_eq(obj*, obj*); +} obj* l_lean_to__fmt___at_lean_parser_syntax_has__to__string___spec__1(obj*); obj* l_lean_parser_syntax_mreplace___main___rarg___lambda__1(obj*, obj*, obj*); obj* l_lean_parser_syntax_reprint__atom(obj*); @@ -102,6 +125,9 @@ obj* l_lean_format_join__sep___main___at_lean_parser_syntax_to__format___main___ obj* l_lean_parser_syntax_reprint__lst___main___closed__1; obj* l_lean_parser_syntax_to__format___main___closed__2; obj* l_lean_parser_macro__scope_lean_has__to__format; +namespace lean { +obj* string_mk_iterator(obj*); +} extern obj* l_lean_format_paren___closed__2; obj* l_lean_parser_macro__scopes_flip___main(obj*, obj*); obj* l_lean_parser_syntax_list(obj*); @@ -118,6 +144,7 @@ obj* l_nat_repr(obj*); obj* l_lean_parser_choice; obj* l_lean_parser_syntax_reprint___main___closed__1; obj* l___private_init_lean_parser_syntax_1__update__leading__aux(obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l_list_append___rarg(obj*, obj*); obj* l___private_init_lean_parser_syntax_1__update__leading__aux___main(obj*, obj*); obj* l_option_map___rarg(obj*, obj*); diff --git a/src/boot/init/lean/parser/term.cpp b/src/boot/init/lean/parser/term.cpp index c9b6bbaa48..82fa3a5718 100644 --- a/src/boot/init/lean/parser/term.cpp +++ b/src/boot/init/lean/parser/term.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.parser.level init.lean.parser.notation init.lean.expr #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -109,6 +107,7 @@ obj* l_lean_parser_term_simple__binder_has__view_x_27___lambda__1___closed__2; obj* l_lean_parser_term_assume__anonymous; obj* l_lean_parser_term_projection_parser(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_term_binders__ext; +obj* l_nat_add(obj*, obj*); obj* l_lean_parser_combinators_choice__aux___main___at_lean_parser_command_notation__spec_precedence__lit_parser_lean_parser_has__view___spec__3(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_term_explicit__modifier; obj* l_reader__t_lift___at_lean_parser_term_sort__app_parser_lean_parser_has__view___spec__2(obj*); @@ -194,6 +193,9 @@ obj* l_lean_parser_term_sorry_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_term_type__spec_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_term_paren__special_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_term_binders_has__view_x_27; +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_lean_parser_term_subtype_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_term_paren__content_has__view; obj* l_lean_parser_term_strict__implicit__binder_has__view_x_27___lambda__1(obj*); @@ -280,6 +282,9 @@ obj* l_lean_parser_term_explicit__modifier_has__view_x_27___lambda__1___closed__ obj* l_lean_parser_term_inaccessible; obj* l_lean_parser_term_simple__binder_parser___closed__1; obj* l_lean_parser_combinators_choice__aux___main___at_lean_parser_term_projection_parser_lean_parser_has__view___spec__4(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); +namespace lean { +obj* string_length(obj*); +} obj* l_lean_parser_term_projection_parser_lean_parser_has__view___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_term_binder_parser_lean_parser_has__tokens; obj* l_lean_parser_ident__univs; @@ -437,6 +442,7 @@ obj* l_lean_parser_term_have; obj* l_lean_parser_term_match_parser___closed__1; obj* l_lean_parser_term_pi; obj* l_lean_parser_term_paren_has__view; +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_parser_term_binder__content_has__view_x_27___lambda__1___closed__4; obj* l_lean_parser_term_sort_has__view_x_27; obj* l_lean_parser_token__map__cons_tokens___rarg(obj*, obj*); @@ -585,6 +591,9 @@ obj* l_lean_parser_term_binders__ext_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_term_assume_has__view; obj* l_lean_parser_term_mixed__binder_has__view_x_27___lambda__1(obj*); extern obj* l_lean_parser_term_parser_lean_parser_has__tokens___closed__1; +namespace lean { +obj* string_iterator_offset(obj*); +} obj* l_lean_parser_term_get__leading(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_combinators_many1___at_lean_parser_command_notation__spec_parser_lean_parser_has__view___spec__2(obj*, obj*, obj*, obj*, obj*, obj*); extern obj* l_lean_parser_level_leading_parser_lean_parser_has__tokens; @@ -642,6 +651,9 @@ extern obj* l_lean_parser_level__parser_run_lean_parser_has__view___closed__3; obj* l_lean_parser_term_binder__content_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_term_assume__binders_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_parsec__t_lookahead___at___private_init_lean_parser_term_1__trailing___spec__8(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} obj* l_lean_parser_term_projection_parser___closed__1; obj* l_lean_parser_term_struct__inst__with; obj* l_lean_parser_term_inaccessible_parser(obj*, obj*, obj*, obj*, obj*); @@ -690,8 +702,14 @@ obj* l_lean_parser_term_match__equation; obj* l_lean_parser_term_from_parser___closed__1; obj* l_lean_parser_term_have__term_has__view_x_27; obj* l_lean_parser_string__lit_parser___at_lean_parser_term_builtin__leading__parsers_lean_parser_has__tokens___spec__1(obj*); +namespace lean { +obj* string_iterator_remaining(obj*); +} obj* l_rbmap_find___main___at___private_init_lean_parser_term_1__trailing___spec__3(obj*); extern obj* l_lean_parser_trailing__term__parser__m_monad; +namespace lean { +obj* string_mk_iterator(obj*); +} obj* l_lean_parser_term_binder_has__view_x_27; obj* l_lean_parser_term_app_has__view_x_27___lambda__1(obj*); extern obj* l_lean_parser_basic__parser__m_alternative; @@ -770,6 +788,9 @@ extern obj* l_lean_parser_trailing__term__parser__m_alternative; obj* l_lean_parser_term_anonymous__inaccessible_has__view_x_27___lambda__1(obj*); obj* l_lean_parser_term_pi_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_term_let_has__view_x_27; +namespace lean { +obj* name_mk_numeral(obj*, obj*); +} obj* l_lean_parser_term_binder__content_has__view; obj* l_lean_parser_term_binder__default_has__view_x_27___lambda__2(obj*); obj* l_lean_parser_string__lit_parser___at_lean_parser_term_builtin__leading__parsers_lean_parser_has__tokens___spec__1___rarg(obj*, obj*, obj*, obj*); @@ -824,6 +845,7 @@ obj* l_lean_parser_term_hole; obj* l_lean_parser_command_notation__like_parser(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_term_lean_parser_has__tokens; obj* l_lean_parser_ident__univ__spec_has__view_x_27___lambda__1___closed__2; +obj* l_nat_sub(obj*, obj*); obj* l_lean_parser_term_mixed__binder_has__view_x_27___lambda__1___closed__1; obj* l_lean_parser_term_match_parser(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_term_binder__content_has__view_x_27; @@ -897,6 +919,7 @@ obj* l_rbmap_find___main___at___private_init_lean_parser_term_1__trailing___spec obj* l_lean_parser_term_mixed__binder_has__view; obj* l_lean_parser_term_inst__implicit__named__binder_has__view; obj* l_lean_parser_term_explicit__binder__content_has__view_x_27___lambda__2(obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* l_lean_parser_term_simple__strict__implicit__binder_has__view_x_27___lambda__1___closed__1; obj* l___private_init_lean_parser_rec_1__run__aux___main___rarg(obj*, obj*, obj*, obj*); obj* l_lean_parser_term_from_has__view; diff --git a/src/boot/init/lean/parser/token.cpp b/src/boot/init/lean/parser/token.cpp index 90ef8e51a4..ffaee6088e 100644 --- a/src/boot/init/lean/parser/token.cpp +++ b/src/boot/init/lean/parser/token.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.parser.combinators init.lean.parser.string_literal #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -82,6 +80,7 @@ obj* l_lean_parser_ident_parser_view___rarg___lambda__1___closed__2; obj* l_lean_parser_raw_view___rarg___lambda__2(obj*); obj* l_lean_parser_detail__ident_parser___closed__1; obj* l_lean_parser_parsec__t_lookahead___at___private_init_lean_parser_token_2__whitespace__aux___main___spec__4___closed__2; +obj* l_nat_add(obj*, obj*); extern obj* l_lean_parser_parse__quoted__char___rarg___lambda__7___closed__1; obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_detail__ident__part_parser_lean_parser_has__view___spec__4(obj*, obj*, obj*, obj*); obj* l_lean_parser_parse__hex__digit___at_lean_parser_string__lit_x_27___spec__4___closed__1; @@ -138,6 +137,9 @@ obj* l_lean_parser_detail__ident__suffix_has__view_x_27; obj* l_lean_parser_monad__parsec_whitespace___at___private_init_lean_parser_token_2__whitespace__aux___main___spec__1(obj*, obj*, obj*); obj* l_list_reverse___rarg(obj*); obj* l_lean_parser_ident_parser___rarg___closed__1; +namespace lean { +obj* name_mk_string(obj*, obj*); +} obj* l_reader__t_alternative___rarg(obj*, obj*); obj* l_lean_parser_unicode__symbol_view__default___rarg(obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_foldl___at___private_init_lean_parser_token_4__ident_x_27___spec__20(obj*, uint32, obj*, obj*, obj*); @@ -165,6 +167,9 @@ extern obj* l_lean_parser_monad__parsec_eoi__error___rarg___closed__1; obj* l_lean_parser_monad__parsec_take__while__cont___at___private_init_lean_parser_token_4__ident_x_27___spec__4(uint32, obj*, obj*, obj*); obj* l_lean_parser_raw___rarg___lambda__3___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at_lean_parser_detail__ident__part_parser_lean_parser_has__tokens___spec__26(obj*, obj*, obj*); +namespace lean { +obj* string_iterator_next(obj*); +} obj* l_rbmap_find___main___at_lean_parser_indexed___spec__3___rarg(obj*, obj*); obj* l_lean_parser_raw__str_lean_parser_has__tokens(obj*, obj*, obj*, obj*, obj*, uint8); obj* l_lean_parser_ident_parser_view___rarg___closed__1; @@ -186,6 +191,9 @@ obj* l_lean_parser_monad__parsec_foldl__aux___main___at___private_init_lean_pars obj* l___private_init_lean_parser_parsec_6__take__while__aux_x_27___main___at___private_init_lean_parser_token_2__whitespace__aux___main___spec__3(obj*, uint8, obj*); obj* l_lean_parser_raw___rarg___lambda__2___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_raw__ident_parser_tokens(obj*, obj*); +namespace lean { +obj* string_length(obj*); +} obj* l_list_map___main___at_lean_parser_number_x_27___spec__9(obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_detail__ident__part_parser_lean_parser_has__tokens___spec__13(uint32, obj*, obj*, obj*); obj* l_lean_parser_symbol__or__ident(obj*); @@ -203,6 +211,9 @@ obj* l_lean_parser_detail__ident__suffix_parser_lean_parser_has__view___lambda__ obj* l_lean_parser_monad__parsec_take__while_x_27___at___private_init_lean_parser_token_2__whitespace__aux___main___spec__2___rarg(obj*, obj*); uint8 l_char_is__alpha(uint32); obj* l_lean_parser_detail__ident_parser___lambda__1(obj*, obj*, obj*, obj*, obj*); +namespace lean { +uint32 string_iterator_curr(obj*); +} obj* l_lean_parser_parse__string__literal__aux___main___at_lean_parser_string__lit_x_27___spec__2(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while___at_lean_parser_detail__ident__part_parser_lean_parser_has__tokens___spec__17___rarg(obj*, obj*); obj* l___private_init_lean_parser_token_2__whitespace__aux___main___closed__3; @@ -211,6 +222,9 @@ obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_number_x_27_ extern obj* l_lean_name_to__string___closed__1; obj* l_list_mfoldl___main___at_lean_parser_detail__ident__part_parser_lean_parser_has__view___spec__9(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_number_has__view_x_27___lambda__1___closed__5; +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_reader__t_bind___at_lean_parser_detail__ident__suffix_parser_lean_parser_has__view___spec__3(obj*, obj*); obj* l_lean_parser_symbol__or__ident_view___rarg(obj*, obj*); obj* l_function_comp___rarg(obj*, obj*, obj*); @@ -279,12 +293,16 @@ obj* l_lean_parser_symbol_view__default___rarg(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at___private_init_lean_parser_token_4__ident_x_27___spec__17(uint32, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_number_x_27___spec__6(obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_detail__ident__part_parser___spec__2(uint32, obj*, obj*, obj*); +namespace lean { +uint8 string_iterator_has_next(obj*); +} obj* l_lean_parser_raw_tokens___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_symbol_tokens___rarg(obj*, obj*); obj* l_lean_parser_parsec__t_lookahead___at___private_init_lean_parser_token_2__whitespace__aux___main___spec__4(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_error___at_lean_parser_number_x_27___spec__12(obj*); obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at_lean_parser_parse__hex__lit___spec__3(obj*, obj*, obj*); obj* l_lean_parser_raw_view___rarg___boxed(obj*, obj*, obj*, obj*, obj*, obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_parser_combinators_optional___at_lean_parser_detail__ident_x_27___spec__2(obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_raw_view___rarg___lambda__1(obj*); obj* l_lean_parser_detail__ident_parser___closed__2; @@ -331,6 +349,7 @@ obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_detail__iden obj* l_rbmap_find___main___at_lean_parser_indexed___spec__5(obj*); obj* l_lean_parser_token___closed__1; obj* l_lean_parser_monad__parsec_take__while___at_lean_parser_detail__ident__part_parser_lean_parser_has__view___spec__12(obj*); +uint8 l_nat_dec__le(obj*, obj*); obj* l_lean_parser_rec__t_lean_parser_monad__parsec___rarg(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_str__core___rarg(obj*, obj*, obj*, obj*); obj* l_lean_parser_raw__str_lean_parser_has__view___rarg(obj*, obj*, obj*, obj*, uint8); @@ -372,6 +391,9 @@ obj* l_lean_parser_with__trailing___rarg(obj*, obj*, obj*, obj*); extern obj* l_lean_id__begin__escape; obj* l_rbmap_find___main___at_lean_parser_indexed___spec__3(obj*); obj* l_lean_parser_parsec__t_lookahead___at_lean_parser_detail__ident__suffix_parser_lean_parser_has__tokens___spec__1___boxed(obj*, obj*, obj*, obj*, obj*); +namespace lean { +obj* string_iterator_offset(obj*); +} obj* l___private_init_lean_parser_token_7__to__nat__core(obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_curr___at___private_init_lean_parser_token_4__ident_x_27___spec__2___rarg(obj*, obj*); obj* l_lean_parser_with__trailing___rarg___lambda__2(obj*, obj*, obj*, obj*); @@ -398,10 +420,16 @@ obj* l_lean_parser_monad__parsec_observing___at_lean_parser_token___spec__2(obj* obj* l_lean_parser_substring_to__string(obj*); obj* l_lean_parser_try__view___at_lean_parser_string__lit_parser___spec__1(obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_parse__oct__lit___spec__6(uint32, obj*, obj*, obj*, obj*); +namespace lean { +uint8 name_dec_eq(obj*, obj*); +} obj* l___private_init_lean_parser_token_1__finish__comment__block__aux___main___closed__2; obj* l_lean_parser_unicode__symbol_lean_parser_has__view(obj*); obj* l_lean_parser_monad__parsec_unexpected__at___at_lean_parser_string__lit_view_value___spec__9(obj*); obj* l_lean_parser_parsec__t_lookahead___at___private_init_lean_parser_token_2__whitespace__aux___main___spec__4___closed__1; +namespace lean { +uint8 string_dec_eq(obj*, obj*); +} obj* l___private_init_lean_parser_parsec_4__take__while__aux___main___at_lean_parser_detail__ident__part_parser___spec__5(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at___private_init_lean_parser_token_4__ident_x_27___spec__17___boxed(obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while___at_lean_parser_detail__ident__part_parser_lean_parser_has__view___spec__12___rarg(obj*, obj*); @@ -429,6 +457,12 @@ obj* l_lean_parser_detail__ident__part__escaped_has__view_x_27; obj* l_lean_parser_number_has__view_x_27___lambda__1___closed__3; obj* l_lean_parser_monad__parsec_take__while_x_27___at___private_init_lean_parser_token_2__whitespace__aux___main___spec__5___rarg(obj*, obj*); obj* l_lean_parser_as__substring___rarg(obj*, obj*, obj*, obj*); +namespace lean { +obj* string_iterator_remaining(obj*); +} +namespace lean { +obj* string_mk_iterator(obj*); +} extern obj* l_lean_parser_basic__parser__m_alternative; obj* l_lean_parser_with__trailing___rarg___closed__1; obj* l_lean_parser_detail__ident__suffix_parser_lean_parser_has__view; @@ -466,6 +500,9 @@ obj* l___private_init_lean_parser_token_7__to__nat__core___main(obj*, obj*, obj* obj* l_lean_parser_monad__parsec_take__while__cont___at___private_init_lean_parser_token_4__ident_x_27___spec__6___boxed(obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_detail__ident__part_parser___spec__2___boxed(obj*, obj*, obj*, obj*); obj* l_lean_parser_number_x_27___lambda__2(obj*, obj*, obj*, obj*); +namespace lean { +obj* name_mk_numeral(obj*, obj*); +} obj* l_lean_parser_monad__parsec_take__while___at_lean_parser_detail__ident__part_parser___spec__10___rarg(obj*, obj*); obj* l_lean_parser_detail__ident__part__escaped; uint8 l_lean_is__id__first(uint32); @@ -475,6 +512,7 @@ obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_parse__oct__ obj* l_list_mfoldl___main___at_lean_parser_detail__ident__suffix_parser_lean_parser_has__view___spec__6(obj*, obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_parser_parse__string__literal___at_lean_parser_string__lit_x_27___spec__1(obj*, obj*, obj*); obj* l___private_init_lean_parser_token_1__finish__comment__block__aux___main___closed__4; +obj* l_nat_mul(obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_detail__ident__part_parser___spec__4(obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_parse__hex__lit___spec__2___boxed(obj*, obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_take__while___at_lean_parser_detail__ident__part_parser_lean_parser_has__tokens___spec__23(obj*); @@ -492,6 +530,7 @@ obj* l_lean_parser_string__lit_has__view_x_27; obj* l_lean_parser_monad__parsec_take__while__cont___at_lean_parser_detail__ident__part_parser_lean_parser_has__tokens___spec__6(uint32, obj*, obj*, obj*); obj* l_lean_parser_detail__ident__part__escaped_has__view_x_27___lambda__2(obj*); obj* l___private_init_lean_parser_token_1__finish__comment__block__aux(obj*, obj*, obj*, obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l_lean_parser_string__lit_x_27(obj*, obj*, obj*); obj* l_lean_parser_detail__ident__part_parser___closed__1; obj* l_lean_parser_rec__t_recurse___at_lean_parser_detail__ident__suffix_parser_lean_parser_has__view___spec__4(obj*, obj*, obj*, obj*, obj*); @@ -503,6 +542,9 @@ obj* l_lean_parser_parse__bin__lit(obj*, obj*, obj*); extern obj* l_lean_parser_basic__parser__m_lean_parser_monad__parsec; obj* l_reader__t_bind___at_lean_parser_with__trailing___spec__2(obj*, obj*); obj* l_lean_parser_detail__ident_x_27(obj*, obj*, obj*, obj*); +namespace lean { +obj* string_push(obj*, uint32); +} obj* l_lean_parser_parse__oct__lit(obj*, obj*, obj*); obj* l_dlist_singleton___rarg(obj*, obj*); obj* l_lean_parser_symbol__core___rarg___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*); @@ -553,6 +595,7 @@ obj* l_char_quote__core(uint32); obj* l___private_init_lean_parser_token_3__update__trailing__lst___main(obj*, obj*); obj* l_lean_parser_number_x_27(obj*, obj*, obj*); obj* l_lean_parser_monad__parsec_digit___at_lean_parser_string__lit_x_27___spec__5(obj*, obj*, obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* l_lean_parser_detail__ident__part_parser_lean_parser_has__view___lambda__1(obj*, obj*, obj*, obj*, obj*, obj*); obj* l___private_init_lean_parser_rec_1__run__aux___main___rarg(obj*, obj*, obj*, obj*); obj* l_lean_parser_raw_tokens(obj*, obj*, obj*, obj*, obj*, obj*, uint8); diff --git a/src/boot/init/lean/parser/trie.cpp b/src/boot/init/lean/parser/trie.cpp index 20b77a8a38..d75acfb553 100644 --- a/src/boot/init/lean/parser/trie.cpp +++ b/src/boot/init/lean/parser/trie.cpp @@ -3,8 +3,6 @@ // Imports: init.data.rbmap.default init.lean.format #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -30,8 +28,20 @@ obj* l___private_init_lean_parser_trie_2__find__aux___main(obj*); obj* l_rbnode_find___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__1___rarg(obj*, uint32); obj* l_lean_parser_trie_match__prefix(obj*); obj* l_list_zip___rarg___lambda__1(obj*, obj*); +namespace lean { +obj* string_iterator_next(obj*); +} obj* l___private_init_lean_parser_trie_4__to__string__aux(obj*); +namespace lean { +obj* string_length(obj*); +} obj* l_option_orelse___main___rarg(obj*, obj*); +namespace lean { +uint32 string_iterator_curr(obj*); +} +namespace lean { +obj* string_append(obj*, obj*); +} obj* l_lean_parser_trie_insert___rarg(obj*, obj*, obj*); obj* l_rbnode_mk__insert__result___main___rarg(uint8, obj*); obj* l_option_get__or__else___main___rarg(obj*, obj*); @@ -39,6 +49,7 @@ obj* l_rbnode_fold___main___at___private_init_lean_parser_trie_4__to__string__au obj* l___private_init_lean_parser_trie_2__find__aux___rarg(obj*, obj*, obj*); obj* l_lean_parser_trie_mk___closed__1; obj* l___private_init_lean_parser_trie_1__insert__aux___main___rarg(obj*, obj*, obj*, obj*); +uint8 l_nat_dec__eq(obj*, obj*); extern obj* l_char_has__repr___closed__1; obj* l_rbnode_insert___at___private_init_lean_parser_trie_1__insert__aux___main___spec__2___rarg___boxed(obj*, obj*, obj*); obj* l_lean_parser_trie_find(obj*); @@ -54,9 +65,16 @@ obj* l___private_init_lean_parser_trie_1__insert__aux(obj*); obj* l_lean_format_pretty(obj*, 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*); +namespace lean { +obj* string_iterator_remaining(obj*); +} +namespace lean { +obj* string_mk_iterator(obj*); +} uint8 l_rbnode_get__color___main___rarg(obj*); obj* l_lean_to__fmt___at___private_init_lean_parser_trie_4__to__string__aux___main___spec__2(obj*); obj* l_rbnode_balance1__node___main___rarg(obj*, obj*, obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l___private_init_lean_parser_trie_3__match__prefix__aux___main(obj*); obj* l_rbnode_ins___main___at___private_init_lean_parser_trie_1__insert__aux___main___spec__3___rarg(obj*, uint32, obj*); obj* l_option_map___rarg(obj*, obj*); @@ -65,6 +83,7 @@ obj* l_rbnode_fold___main___at___private_init_lean_parser_trie_4__to__string__au obj* l_char_quote__core(uint32); obj* l_lean_parser_trie_insert(obj*); obj* l_lean_parser_trie_has__to__string___rarg(obj*); +uint8 l_nat_dec__lt(obj*, obj*); obj* l___private_init_lean_parser_trie_2__find__aux___main___rarg(obj*, obj*, obj*); obj* l___private_init_lean_parser_trie_2__find__aux(obj*); obj* _init_l_lean_parser_trie_mk___closed__1() { diff --git a/src/boot/init/lean/position.cpp b/src/boot/init/lean/position.cpp index 3253fd200a..87ccd7dfc1 100644 --- a/src/boot/init/lean/position.cpp +++ b/src/boot/init/lean/position.cpp @@ -3,8 +3,6 @@ // Imports: init.data.nat.default init.data.rbmap.default init.lean.format #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -19,38 +17,60 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64; 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_balance2__node___main___rarg(obj*, obj*, obj*, obj*); +obj* l_nat_add(obj*, obj*); 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_lt; obj* l_lean_position_lean_has__to__format(obj*); +namespace lean { +obj* string_iterator_next(obj*); +} +namespace lean { +obj* string_length(obj*); +} obj* l_lean_position_has__lt; obj* l_lean_position_decidable__lt___boxed(obj*, obj*); +namespace lean { +uint32 string_iterator_curr(obj*); +} obj* l_rbnode_mk__insert__result___main___rarg(uint8, obj*); obj* l_lean_position_lean_has__to__format___closed__2; uint8 l_lean_position_decidable__lt(obj*, obj*); obj* l_lean_position_decidable__lt___main___boxed(obj*, obj*); +namespace lean { +uint8 string_iterator_has_next(obj*); +} obj* l_rbmap_insert___main___at_lean_file__map_from__string___spec__2(obj*, obj*, obj*); +uint8 l_nat_dec__eq(obj*, obj*); obj* l_lean_position_decidable__lt___main___closed__2; obj* l_nat_dec__eq___boxed(obj*, obj*); +namespace lean { +obj* string_iterator_offset(obj*); +} obj* l_lean_file__map_from__string(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*, 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*, obj*); obj* l_rbnode_insert___at_lean_file__map_from__string___spec__3(obj*, obj*, obj*); +namespace lean { +obj* string_mk_iterator(obj*); +} uint8 l_rbnode_get__color___main___rarg(obj*); obj* l_lean_position_decidable__lt___main___closed__1; obj* l_rbmap_lower__bound___main___at_lean_file__map_to__position___spec__1(obj*, obj*); obj* l_nat_repr(obj*); uint8 l_lean_position_decidable__lt___main(obj*, obj*); obj* l_rbnode_balance1__node___main___rarg(obj*, obj*, obj*, obj*); +obj* l_nat_sub(obj*, obj*); obj* l_lean_file__map_to__position(obj*, obj*); obj* l_lean_position_lt___main; obj* l_lean_position_inhabited; uint8 l_lean_position_decidable__eq(obj*, obj*); obj* l_nat_dec__lt___boxed(obj*, obj*); obj* l_lean_position_decidable__eq___boxed(obj*, obj*); +uint8 l_nat_dec__lt(obj*, obj*); uint8 l_lean_position_decidable__eq(obj* x_0, obj* x_1) { _start: { diff --git a/src/boot/init/lean/trace.cpp b/src/boot/init/lean/trace.cpp index 423545245b..dbfda67513 100644 --- a/src/boot/init/lean/trace.cpp +++ b/src/boot/init/lean/trace.cpp @@ -3,8 +3,6 @@ // Imports: init.lean.format init.data.rbmap.default init.lean.position init.lean.name init.lean.options #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; @@ -23,6 +21,7 @@ obj* l_lean_trace_pp___main(obj*); obj* l_lean_trace_trace__map; 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_thunk_mk(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__8(obj*, obj*, obj*, obj*, obj*, obj*); obj* l_lean_trace_trace__t_run(obj*, obj*); @@ -42,6 +41,7 @@ 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_thunk_get(obj*, obj*); obj* l_state__t_monad___rarg(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*); diff --git a/src/boot/init/platform.cpp b/src/boot/init/platform.cpp index b731d8fc5b..59c8fb85ff 100644 --- a/src/boot/init/platform.cpp +++ b/src/boot/init/platform.cpp @@ -3,8 +3,6 @@ // Imports: init.core #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64; diff --git a/src/boot/init/wf.cpp b/src/boot/init/wf.cpp index 79839021e6..255cabc418 100644 --- a/src/boot/init/wf.cpp +++ b/src/boot/init/wf.cpp @@ -3,8 +3,6 @@ // Imports: init.data.nat.basic #include "runtime/object.h" #include "runtime/apply.h" -#include "runtime/io.h" -#include "kernel/builtin.h" typedef lean::object obj; typedef lean::usize usize; typedef lean::uint8 uint8; typedef lean::uint16 uint16; typedef lean::uint32 uint32; typedef lean::uint64 uint64;