chore: update stage0

This commit is contained in:
Lean stage0 autoupdater 2025-04-25 21:29:05 +00:00
parent 62c6edffef
commit 882d1ab812
21 changed files with 16959 additions and 11223 deletions

View file

@ -227,7 +227,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t
// Locking early prevents potential parallelism issues setting the byte_array.
event_loop_lock(&global_ev);
if (tcp_socket->m_byte_array != nullptr) {
if (tcp_socket->m_promise_read != nullptr) {
event_loop_unlock(&global_ev);
return lean_io_result_mk_error(lean_decode_uv_error(UV_EALREADY, nullptr));
}
@ -295,6 +295,102 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t
return lean_io_result_mk_ok(promise);
}
/* Std.Internal.UV.TCP.Socket.waitReadable (socket : @& Socket) : IO (IO.Promise (Except IO.Error Bool)) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_wait_readable(b_obj_arg socket, obj_arg /* w */) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
event_loop_lock(&global_ev);
if (tcp_socket->m_promise_read != nullptr) {
event_loop_unlock(&global_ev);
return lean_io_result_mk_error(lean_decode_uv_error(UV_EALREADY, nullptr));
}
lean_object* promise = lean_promise_new();
mark_mt(promise);
tcp_socket->m_promise_read = promise;
// The event loop owns the socket.
lean_inc(socket);
lean_inc(promise);
int result = uv_read_start((uv_stream_t*)tcp_socket->m_uv_tcp, [](uv_handle_t* handle, size_t suggested_size, uv_buf_t* buf) {
// According to libuv documentation if we do this we do not lose data and a UV_ENOBUFS will
// be triggered in the read cb.
buf->base = NULL;
buf->len = 0;
}, [](uv_stream_t* stream, ssize_t nread, const uv_buf_t* buf) {
uv_read_stop(stream);
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket((lean_object*)stream->data);
lean_object* promise = tcp_socket->m_promise_read;
tcp_socket->m_promise_read = nullptr;
if (nread == UV_ENOBUFS) {
lean_promise_resolve(mk_except_ok(lean_box(1)), promise);
} else if (nread == UV_EOF) {
lean_promise_resolve(mk_except_ok(lean_box(0)), promise);
} else if (nread < 0) {
lean_promise_resolve(mk_except_err(lean_decode_uv_error(nread, nullptr)), promise);
} else {
// This branch should be dead, we cannot receive a value >= 0 according to docs.
lean_always_assert(false);
}
lean_dec(promise);
// The event loop does not own the object anymore.
lean_dec((lean_object*)stream->data);
});
if (result < 0) {
tcp_socket->m_promise_read = nullptr;
event_loop_unlock(&global_ev);
lean_dec(promise); // The structure does not own it.
lean_dec(promise); // We are not going to return it.
lean_dec(socket);
return lean_io_result_mk_error(lean_decode_uv_error(result, nullptr));
}
event_loop_unlock(&global_ev);
return lean_io_result_mk_ok(promise);
}
/* Std.Internal.UV.TCP.Socket.cancelRecv (socket : @& Socket) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket, obj_arg /* w */) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
event_loop_lock(&global_ev);
if (tcp_socket->m_promise_read == nullptr) {
event_loop_unlock(&global_ev);
return lean_io_result_mk_ok(lean_box(0));
}
uv_read_stop((uv_stream_t*)tcp_socket->m_uv_tcp);
lean_object* promise = tcp_socket->m_promise_read;
lean_dec(promise);
tcp_socket->m_promise_read = nullptr;
lean_object* byte_array = tcp_socket->m_byte_array;
if (byte_array != nullptr) {
lean_dec(byte_array);
tcp_socket->m_byte_array = nullptr;
}
lean_dec((lean_object*)tcp_socket);
event_loop_unlock(&global_ev);
return lean_io_result_mk_ok(lean_box(0));
}
/* Std.Internal.UV.TCP.Socket.bind (socket : @& Socket) (addr : @& SocketAddress) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);

View file

@ -42,6 +42,8 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t buffer_size, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_wait_readable(b_obj_arg socket, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_listen(b_obj_arg socket, int32_t backlog, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket, obj_arg /* w */);

View file

@ -208,7 +208,9 @@ LEAN_EXPORT uint8_t l_BitVec_instGetElemNatBoolLt___rarg(lean_object*, lean_obje
static lean_object* l_BitVec_term_____x23_______closed__4;
LEAN_EXPORT lean_object* l_BitVec_sshiftRight(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_BitVec_unexpandBitVecOfNatLt___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_BitVec_sdivOverflow(lean_object*, lean_object*, lean_object*);
static lean_object* l_BitVec_term_____x23_______closed__17;
LEAN_EXPORT lean_object* l_BitVec_sdivOverflow___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_BitVec_term_____x23_______closed__18;
LEAN_EXPORT lean_object* l_BitVec_instHShiftRight___boxed(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_BitVec_slt(lean_object*, lean_object*, lean_object*);
@ -329,6 +331,7 @@ LEAN_EXPORT lean_object* l_BitVec_term_____x23____;
LEAN_EXPORT lean_object* l_BitVec_cast___rarg(lean_object*);
LEAN_EXPORT lean_object* l_BitVec_instMul(lean_object*);
static lean_object* l_BitVec_term_____x23_______closed__8;
lean_object* lean_int_ediv(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_BitVec_instMod(lean_object*);
LEAN_EXPORT lean_object* l_BitVec_instHashable(lean_object*);
lean_object* lean_int_neg(lean_object*);
@ -3861,6 +3864,51 @@ x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT uint8_t l_BitVec_sdivOverflow(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_4 = lean_unsigned_to_nat(1u);
x_5 = lean_nat_sub(x_1, x_4);
x_6 = l_BitVec_saddOverflow___closed__1;
x_7 = l_Int_pow(x_6, x_5);
lean_dec(x_5);
x_8 = l_BitVec_toInt(x_1, x_2);
x_9 = l_BitVec_toInt(x_1, x_3);
x_10 = lean_int_ediv(x_8, x_9);
lean_dec(x_9);
lean_dec(x_8);
x_11 = lean_int_dec_le(x_7, x_10);
if (x_11 == 0)
{
lean_object* x_12; uint8_t x_13;
x_12 = lean_int_neg(x_7);
lean_dec(x_7);
x_13 = lean_int_dec_lt(x_10, x_12);
lean_dec(x_12);
lean_dec(x_10);
return x_13;
}
else
{
uint8_t x_14;
lean_dec(x_10);
lean_dec(x_7);
x_14 = 1;
return x_14;
}
}
}
LEAN_EXPORT lean_object* l_BitVec_sdivOverflow___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = l_BitVec_sdivOverflow(x_1, x_2, x_3);
lean_dec(x_1);
x_5 = lean_box(x_4);
return x_5;
}
}
LEAN_EXPORT lean_object* l_BitVec_reverse(lean_object* x_1, lean_object* x_2) {
_start:
{

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

View file

@ -5317,7 +5317,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Declaration_definitionVal_x21___closed__1;
x_2 = l_Lean_ConstantInfo_inductiveVal_x21___closed__1;
x_3 = lean_unsigned_to_nat(513u);
x_3 = lean_unsigned_to_nat(514u);
x_4 = lean_unsigned_to_nat(9u);
x_5 = l_Lean_ConstantInfo_inductiveVal_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

View file

@ -606,6 +606,7 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Elab_BuiltinComma
static lean_object* l_Lean_Elab_OpenDecl_elabOpenDecl___at_Lean_Elab_Command_elabOpen___spec__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabOpen___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Command_elabVariable_declRange__1___closed__6;
uint8_t l_List_beq___at___private_Lean_Declaration_0__Lean_beqConstantVal____x40_Lean_Declaration___hyg_431____spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Command_elabNonComputableSection_declRange__1___closed__6;
static lean_object* l___regBuiltin_Lean_Elab_Command_elabChoice__1___closed__4;
@ -1109,7 +1110,6 @@ LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Command_elabOpen__1(lean_objec
LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___spec__4___lambda__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_replaceBinderAnnotation___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_List_beq___at___private_Lean_Data_OpenDecl_0__Lean_beqOpenDecl____x40_Lean_Data_OpenDecl___hyg_41____spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Command_elabReduce_declRange__1(lean_object*);
static lean_object* l_Lean_Elab_Command_elabVersion___rarg___lambda__1___closed__37;
static lean_object* l___regBuiltin_Lean_Elab_Command_elabEoi_declRange__1___closed__6;
@ -1164,7 +1164,6 @@ LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_B
LEAN_EXPORT lean_object* l_Lean_Elab_Command_elabWhere_describeOpenDecls___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_filterTR_loop___at_Lean_Elab_Command_elabOmit___spec__15___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_checkAnonymousScope___closed__1;
lean_object* l_List_toString___at_Lean_OpenDecl_instToString___spec__1(lean_object*);
static lean_object* l_Lean_Elab_Command_elabReduce___closed__2;
static lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_typelessBinder_x3f___closed__8;
LEAN_EXPORT lean_object* l_Lean_Elab_Command_elabSetOption(lean_object*, lean_object*, lean_object*, lean_object*);
@ -1212,6 +1211,7 @@ LEAN_EXPORT lean_object* l_Lean_RBNode_forIn_visit___at_Lean_Elab_Command_elabOm
static lean_object* l___private_Lean_Elab_BuiltinCommand_0__Lean_Elab_Command_typelessBinder_x3f___closed__6;
LEAN_EXPORT lean_object* l___private_Lean_ResolveName_0__Lean_resolveGlobalConstCore___at_Lean_Elab_Command_elabExport___spec__9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addDecl(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_toString___at_Lean_Environment_AddConstAsyncResult_commitConst___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_elabSetOption___lambda__1(lean_object*, lean_object*);
size_t lean_usize_land(size_t, size_t);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_OpenDecl_elabOpenDecl___spec__52(size_t, size_t, lean_object*);
@ -9335,7 +9335,7 @@ lean_inc(x_20);
lean_ctor_set_tag(x_16, 1);
lean_ctor_set(x_16, 1, x_21);
lean_ctor_set(x_16, 0, x_20);
x_22 = l_List_beq___at___private_Lean_Data_OpenDecl_0__Lean_beqOpenDecl____x40_Lean_Data_OpenDecl___hyg_41____spec__1(x_14, x_16);
x_22 = l_List_beq___at___private_Lean_Declaration_0__Lean_beqConstantVal____x40_Lean_Declaration___hyg_431____spec__1(x_14, x_16);
lean_dec(x_16);
if (x_22 == 0)
{
@ -9389,7 +9389,7 @@ lean_inc(x_33);
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_33);
lean_ctor_set(x_35, 1, x_34);
x_36 = l_List_beq___at___private_Lean_Data_OpenDecl_0__Lean_beqOpenDecl____x40_Lean_Data_OpenDecl___hyg_41____spec__1(x_14, x_35);
x_36 = l_List_beq___at___private_Lean_Declaration_0__Lean_beqConstantVal____x40_Lean_Declaration___hyg_431____spec__1(x_14, x_35);
lean_dec(x_35);
if (x_36 == 0)
{
@ -10589,7 +10589,7 @@ x_14 = lean_string_append(x_13, x_12);
lean_dec(x_12);
x_15 = l_Lean_resolveUniqueNamespace___at_Lean_Elab_Command_elabOpen___spec__3___closed__2;
x_16 = lean_string_append(x_14, x_15);
x_17 = l_List_toString___at_Lean_OpenDecl_instToString___spec__1(x_7);
x_17 = l_List_toString___at_Lean_Environment_AddConstAsyncResult_commitConst___spec__1(x_7);
x_18 = lean_string_append(x_16, x_17);
lean_dec(x_17);
x_19 = l_Lean_resolveNamespaceCore___at_Lean_Elab_Command_elabExport___spec__4___closed__3;
@ -10655,7 +10655,7 @@ x_37 = lean_string_append(x_36, x_35);
lean_dec(x_35);
x_38 = l_Lean_resolveUniqueNamespace___at_Lean_Elab_Command_elabOpen___spec__3___closed__2;
x_39 = lean_string_append(x_37, x_38);
x_40 = l_List_toString___at_Lean_OpenDecl_instToString___spec__1(x_7);
x_40 = l_List_toString___at_Lean_Environment_AddConstAsyncResult_commitConst___spec__1(x_7);
x_41 = lean_string_append(x_39, x_40);
lean_dec(x_40);
x_42 = l_Lean_resolveNamespaceCore___at_Lean_Elab_Command_elabExport___spec__4___closed__3;
@ -34903,7 +34903,7 @@ if (lean_is_exclusive(x_13)) {
lean_dec_ref(x_13);
x_20 = lean_box(0);
}
x_110 = l_List_beq___at___private_Lean_Data_OpenDecl_0__Lean_beqOpenDecl____x40_Lean_Data_OpenDecl___hyg_41____spec__1(x_19, x_2);
x_110 = l_List_beq___at___private_Lean_Declaration_0__Lean_beqConstantVal____x40_Lean_Declaration___hyg_431____spec__1(x_19, x_2);
if (x_110 == 0)
{
uint8_t x_111; uint8_t x_112;

View file

@ -63,7 +63,6 @@ lean_object* l_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, l
lean_object* lean_get_set_stdout(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Command_elabRunCmd__1(lean_object*);
static lean_object* l_Lean_Elab_Command_elabEvalCoreUnsafe___lambda__17___closed__1;
lean_object* l_Lean_CollectAxioms_collect(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_BuiltinEvalCommand_0__Lean_Elab_Command_mkToExpr___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_Command_elabEvalCoreUnsafe(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_BuiltinEvalCommand___hyg_7____closed__6;
@ -262,6 +261,7 @@ static lean_object* l___private_Lean_Elab_BuiltinEvalCommand_0__Lean_Elab_Comman
static lean_object* l___regBuiltin_Lean_Elab_Command_elabEval_declRange__1___closed__6;
lean_object* l_Lean_Meta_mkDecide(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Command_elabEval__1___closed__1;
lean_object* l___private_Lean_Util_CollectAxioms_0__Lean_CollectAxioms_collect(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Command_elabEvalBang(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Command_elabRunCmd___lambda__1___closed__13;
@ -2749,7 +2749,7 @@ x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
lean_dec(x_11);
x_13 = l_Lean_collectAxioms___at___private_Lean_Elab_BuiltinEvalCommand_0__Lean_Elab_Command_addAndCompileExprForEval___spec__1___closed__2;
x_14 = l_Lean_CollectAxioms_collect(x_1, x_12, x_13);
x_14 = l___private_Lean_Util_CollectAxioms_0__Lean_CollectAxioms_collect(x_1, x_12, x_13);
x_15 = lean_ctor_get(x_14, 1);
lean_inc(x_15);
lean_dec(x_14);
@ -2771,7 +2771,7 @@ x_19 = lean_ctor_get(x_17, 0);
lean_inc(x_19);
lean_dec(x_17);
x_20 = l_Lean_collectAxioms___at___private_Lean_Elab_BuiltinEvalCommand_0__Lean_Elab_Command_addAndCompileExprForEval___spec__1___closed__2;
x_21 = l_Lean_CollectAxioms_collect(x_1, x_19, x_20);
x_21 = l___private_Lean_Util_CollectAxioms_0__Lean_CollectAxioms_collect(x_1, x_19, x_20);
x_22 = lean_ctor_get(x_21, 1);
lean_inc(x_22);
lean_dec(x_21);

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

View file

@ -55,7 +55,6 @@ static lean_object* l___regBuiltin_Lean_Elab_Command_elabPrint_declRange__1___cl
lean_object* l_Lean_indentD(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_CollectAxioms_collect(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_TSyntax_getString(lean_object*);
lean_object* l_Lean_MessageData_joinSep(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_instantiateStructDefaultValueFn_x3f___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printStructure___spec__34(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -257,10 +256,13 @@ LEAN_EXPORT lean_object* l_Std_Range_forIn_x27_loop___at___private_Lean_Elab_Pri
lean_object* l_Lean_RBNode_insert___at_Lean_NameMap_insert___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__11(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printStructure___spec__32___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__3;
lean_object* l_panic___at_Lean_Expr_appFn_x21___spec__1(lean_object*);
static lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__2;
static lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__2;
lean_object* l_List_lengthTRAux___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printStructure___spec__42___boxed(lean_object**);
lean_object* l___private_Lean_Util_CollectAxioms_0__Lean_CollectAxioms_collect(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_printInduct___closed__4;
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
@ -336,6 +338,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Command_elabPrintEqns_declRange__1_
static lean_object* l___regBuiltin_Lean_Elab_Command_elabPrintEqns_declRange__1___closed__5;
static lean_object* l_Lean_Elab_Command_elabPrint___closed__11;
lean_object* l_Lean_getFieldInfo_x3f(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getOriginalConstKind_x3f(lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader___closed__17;
static lean_object* l___regBuiltin_Lean_Elab_Command_elabPrintAxioms_declRange__1___closed__5;
static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_elabPrintAxioms___spec__1___rarg___closed__1;
@ -365,6 +368,7 @@ extern lean_object* l_Lean_pp_proofs;
static lean_object* l___regBuiltin_Lean_Elab_Command_elabPrintAxioms_declRange__1___closed__2;
lean_object* l_Lean_indentExpr(lean_object*);
static lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_levelParamsToMessageData___closed__7;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_printEqnsOf___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printStructure___spec__19(lean_object*, lean_object*, size_t, size_t);
LEAN_EXPORT lean_object* l_Lean_getStructureResolutionOrder___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printStructure___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -435,6 +439,7 @@ lean_object* l_Lean_getStructureCtor(lean_object*, lean_object*);
lean_object* l_Lean_Level_param___override(lean_object*);
size_t lean_usize_add(size_t, size_t);
lean_object* l___private_Lean_Elab_Util_0__Lean_Elab_evalSyntaxConstantUnsafe(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__1;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Command_elabPrintEqns__1(lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printStructure___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_List_forIn_x27_loop___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printInduct___spec__3___closed__1;
@ -1372,6 +1377,53 @@ lean_dec(x_1);
return x_12;
}
}
static lean_object* _init_l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("<not imported>", 14, 14);
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__1;
x_2 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__2;
x_2 = l_Lean_MessageData_ofFormat(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_2;
x_2 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__3;
return x_2;
}
else
{
lean_object* x_3; lean_object* x_4;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
lean_dec(x_1);
x_4 = l_Lean_MessageData_ofExpr(x_3);
return x_4;
}
}
}
static lean_object* _init_l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike___closed__1() {
_start:
{
@ -1426,7 +1478,7 @@ x_15 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike___closed__4
x_16 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_16, 0, x_11);
lean_ctor_set(x_16, 1, x_15);
x_17 = l_Lean_MessageData_ofExpr(x_5);
x_17 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg(x_5);
x_18 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_18, 0, x_16);
lean_ctor_set(x_18, 1, x_17);
@ -1450,7 +1502,7 @@ x_25 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike___closed__4
x_26 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_26, 0, x_24);
lean_ctor_set(x_26, 1, x_25);
x_27 = l_Lean_MessageData_ofExpr(x_5);
x_27 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg(x_5);
x_28 = lean_alloc_ctor(7, 2, 0);
lean_ctor_set(x_28, 0, x_26);
lean_ctor_set(x_28, 1, x_27);
@ -8942,7 +8994,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printStructure___spec__40___closed__1;
x_2 = l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printStructure___spec__40___closed__2;
x_3 = lean_unsigned_to_nat(127u);
x_3 = lean_unsigned_to_nat(131u);
x_4 = lean_unsigned_to_nat(55u);
x_5 = l_Array_forIn_x27Unsafe_loop___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printStructure___spec__40___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12248,191 +12300,524 @@ return x_11;
}
else
{
lean_object* x_12;
x_12 = lean_ctor_get(x_10, 0);
lean_inc(x_12);
lean_dec(x_10);
switch (lean_obj_tag(x_12)) {
uint8_t x_12;
x_12 = !lean_is_exclusive(x_10);
if (x_12 == 0)
{
lean_object* x_13;
x_13 = lean_ctor_get(x_10, 0);
switch (lean_obj_tag(x_13)) {
case 0:
{
lean_object* x_13; lean_object* x_14; uint8_t x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
lean_dec(x_8);
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
lean_dec(x_12);
lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
lean_free_object(x_10);
x_14 = lean_ctor_get(x_13, 0);
lean_inc(x_14);
x_15 = lean_ctor_get_uint8(x_13, sizeof(void*)*1);
lean_dec(x_13);
x_16 = lean_ctor_get(x_14, 1);
lean_inc(x_16);
x_17 = lean_ctor_get(x_14, 2);
lean_inc(x_17);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_ctor_get_uint8(x_14, sizeof(void*)*1);
lean_dec(x_14);
x_18 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__1;
x_19 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_18, x_1, x_16, x_17, x_15, x_2, x_3, x_7);
return x_19;
}
case 1:
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
lean_dec(x_8);
x_20 = lean_ctor_get(x_12, 0);
lean_inc(x_20);
lean_dec(x_12);
x_21 = lean_ctor_get(x_20, 0);
lean_inc(x_21);
x_22 = lean_ctor_get(x_20, 1);
lean_inc(x_22);
x_23 = lean_ctor_get_uint8(x_20, sizeof(void*)*4);
lean_dec(x_20);
x_24 = lean_ctor_get(x_21, 1);
lean_inc(x_24);
x_25 = lean_ctor_get(x_21, 2);
lean_inc(x_25);
lean_dec(x_21);
x_26 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__2;
x_27 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike(x_26, x_1, x_24, x_25, x_22, x_23, x_2, x_3, x_7);
return x_27;
}
case 2:
{
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; uint8_t x_34; lean_object* x_35;
lean_dec(x_8);
x_28 = lean_ctor_get(x_12, 0);
lean_inc(x_28);
lean_dec(x_12);
x_29 = lean_ctor_get(x_28, 0);
lean_inc(x_29);
x_30 = lean_ctor_get(x_28, 1);
lean_inc(x_30);
lean_dec(x_28);
x_31 = lean_ctor_get(x_29, 1);
lean_inc(x_31);
x_32 = lean_ctor_get(x_29, 2);
lean_inc(x_32);
lean_dec(x_29);
x_33 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__3;
x_34 = 1;
x_35 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike(x_33, x_1, x_31, x_32, x_30, x_34, x_2, x_3, x_7);
return x_35;
}
case 3:
{
lean_object* x_36; lean_object* x_37; uint8_t x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42;
lean_dec(x_8);
x_36 = lean_ctor_get(x_12, 0);
lean_inc(x_36);
lean_dec(x_12);
x_37 = lean_ctor_get(x_36, 0);
lean_inc(x_37);
x_38 = lean_ctor_get_uint8(x_36, sizeof(void*)*3);
lean_dec(x_36);
x_39 = lean_ctor_get(x_37, 1);
lean_inc(x_39);
x_40 = lean_ctor_get(x_37, 2);
lean_inc(x_40);
lean_dec(x_37);
x_41 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__4;
x_42 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_41, x_1, x_39, x_40, x_38, x_2, x_3, x_7);
return x_42;
}
case 4:
{
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48;
lean_dec(x_8);
x_43 = lean_ctor_get(x_12, 0);
lean_inc(x_43);
lean_dec(x_12);
x_44 = lean_ctor_get(x_43, 0);
lean_inc(x_44);
lean_dec(x_43);
x_45 = lean_ctor_get(x_44, 1);
lean_inc(x_45);
x_46 = lean_ctor_get(x_44, 2);
lean_inc(x_46);
lean_dec(x_44);
x_47 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printQuot___closed__1;
x_48 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_47, x_1, x_45, x_46, x_9, x_2, x_3, x_7);
return x_48;
}
case 5:
{
lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; uint8_t x_53; lean_object* x_54; lean_object* x_55; uint8_t x_56;
x_49 = lean_ctor_get(x_12, 0);
lean_inc(x_49);
lean_dec(x_12);
x_50 = lean_ctor_get(x_49, 0);
lean_inc(x_50);
x_51 = lean_ctor_get(x_49, 1);
lean_inc(x_51);
x_52 = lean_ctor_get(x_49, 4);
lean_inc(x_52);
x_53 = lean_ctor_get_uint8(x_49, sizeof(void*)*6 + 1);
lean_dec(x_49);
x_54 = lean_ctor_get(x_50, 1);
lean_inc(x_54);
x_55 = lean_ctor_get(x_50, 2);
lean_inc(x_55);
lean_dec(x_50);
x_17 = lean_ctor_get(x_15, 1);
lean_inc(x_17);
x_18 = lean_ctor_get(x_15, 2);
lean_inc(x_18);
lean_dec(x_15);
lean_inc(x_1);
x_56 = l_Lean_isStructure(x_8, x_1);
if (x_56 == 0)
x_19 = l_Lean_getOriginalConstKind_x3f(x_8, x_1);
if (lean_obj_tag(x_19) == 0)
{
lean_object* x_57;
x_57 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printInduct(x_1, x_54, x_51, x_55, x_52, x_53, x_2, x_3, x_7);
return x_57;
lean_object* x_20; lean_object* x_21;
x_20 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__1;
x_21 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_20, x_1, x_17, x_18, x_16, x_2, x_3, x_7);
return x_21;
}
else
{
lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61;
x_58 = l_Lean_instInhabitedName;
x_59 = lean_unsigned_to_nat(0u);
x_60 = l___private_Init_GetElem_0__List_get_x21Internal___rarg(x_58, x_52, x_59);
lean_dec(x_52);
x_61 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printStructure(x_1, x_54, x_51, x_55, x_60, x_53, x_2, x_3, x_7);
lean_object* x_22;
x_22 = lean_ctor_get(x_19, 0);
lean_inc(x_22);
lean_dec(x_19);
switch (lean_obj_tag(x_22)) {
case 0:
{
lean_object* x_23;
x_23 = lean_box(0);
if (x_16 == 0)
{
lean_object* x_24; uint8_t x_25; lean_object* x_26;
x_24 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__2;
x_25 = 1;
x_26 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike(x_24, x_1, x_17, x_18, x_23, x_25, x_2, x_3, x_7);
return x_26;
}
else
{
lean_object* x_27; uint8_t x_28; lean_object* x_29;
x_27 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__2;
x_28 = 0;
x_29 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike(x_27, x_1, x_17, x_18, x_23, x_28, x_2, x_3, x_7);
return x_29;
}
}
case 1:
{
lean_object* x_30;
x_30 = lean_box(0);
if (x_16 == 0)
{
lean_object* x_31; uint8_t x_32; lean_object* x_33;
x_31 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__3;
x_32 = 1;
x_33 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike(x_31, x_1, x_17, x_18, x_30, x_32, x_2, x_3, x_7);
return x_33;
}
else
{
lean_object* x_34; uint8_t x_35; lean_object* x_36;
x_34 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__3;
x_35 = 0;
x_36 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike(x_34, x_1, x_17, x_18, x_30, x_35, x_2, x_3, x_7);
return x_36;
}
}
default:
{
lean_object* x_37; lean_object* x_38;
lean_dec(x_22);
x_37 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__1;
x_38 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_37, x_1, x_17, x_18, x_16, x_2, x_3, x_7);
return x_38;
}
}
}
}
case 1:
{
lean_object* x_39; lean_object* x_40; lean_object* x_41; uint8_t x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46;
lean_dec(x_8);
x_39 = lean_ctor_get(x_13, 0);
lean_inc(x_39);
lean_dec(x_13);
x_40 = lean_ctor_get(x_39, 0);
lean_inc(x_40);
x_41 = lean_ctor_get(x_39, 1);
lean_inc(x_41);
x_42 = lean_ctor_get_uint8(x_39, sizeof(void*)*4);
lean_dec(x_39);
x_43 = lean_ctor_get(x_40, 1);
lean_inc(x_43);
x_44 = lean_ctor_get(x_40, 2);
lean_inc(x_44);
lean_dec(x_40);
lean_ctor_set(x_10, 0, x_41);
x_45 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__2;
x_46 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike(x_45, x_1, x_43, x_44, x_10, x_42, x_2, x_3, x_7);
return x_46;
}
case 2:
{
lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; uint8_t x_53; lean_object* x_54;
lean_dec(x_8);
x_47 = lean_ctor_get(x_13, 0);
lean_inc(x_47);
lean_dec(x_13);
x_48 = lean_ctor_get(x_47, 0);
lean_inc(x_48);
x_49 = lean_ctor_get(x_47, 1);
lean_inc(x_49);
lean_dec(x_47);
x_50 = lean_ctor_get(x_48, 1);
lean_inc(x_50);
x_51 = lean_ctor_get(x_48, 2);
lean_inc(x_51);
lean_dec(x_48);
lean_ctor_set(x_10, 0, x_49);
x_52 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__3;
x_53 = 1;
x_54 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike(x_52, x_1, x_50, x_51, x_10, x_53, x_2, x_3, x_7);
return x_54;
}
case 3:
{
lean_object* x_55; lean_object* x_56; uint8_t x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61;
lean_free_object(x_10);
lean_dec(x_8);
x_55 = lean_ctor_get(x_13, 0);
lean_inc(x_55);
lean_dec(x_13);
x_56 = lean_ctor_get(x_55, 0);
lean_inc(x_56);
x_57 = lean_ctor_get_uint8(x_55, sizeof(void*)*3);
lean_dec(x_55);
x_58 = lean_ctor_get(x_56, 1);
lean_inc(x_58);
x_59 = lean_ctor_get(x_56, 2);
lean_inc(x_59);
lean_dec(x_56);
x_60 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__4;
x_61 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_60, x_1, x_58, x_59, x_57, x_2, x_3, x_7);
return x_61;
}
case 4:
{
lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67;
lean_free_object(x_10);
lean_dec(x_8);
x_62 = lean_ctor_get(x_13, 0);
lean_inc(x_62);
lean_dec(x_13);
x_63 = lean_ctor_get(x_62, 0);
lean_inc(x_63);
lean_dec(x_62);
x_64 = lean_ctor_get(x_63, 1);
lean_inc(x_64);
x_65 = lean_ctor_get(x_63, 2);
lean_inc(x_65);
lean_dec(x_63);
x_66 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printQuot___closed__1;
x_67 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_66, x_1, x_64, x_65, x_9, x_2, x_3, x_7);
return x_67;
}
case 5:
{
lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; uint8_t x_72; lean_object* x_73; lean_object* x_74; uint8_t x_75;
lean_free_object(x_10);
x_68 = lean_ctor_get(x_13, 0);
lean_inc(x_68);
lean_dec(x_13);
x_69 = lean_ctor_get(x_68, 0);
lean_inc(x_69);
x_70 = lean_ctor_get(x_68, 1);
lean_inc(x_70);
x_71 = lean_ctor_get(x_68, 4);
lean_inc(x_71);
x_72 = lean_ctor_get_uint8(x_68, sizeof(void*)*6 + 1);
lean_dec(x_68);
x_73 = lean_ctor_get(x_69, 1);
lean_inc(x_73);
x_74 = lean_ctor_get(x_69, 2);
lean_inc(x_74);
lean_dec(x_69);
lean_inc(x_1);
x_75 = l_Lean_isStructure(x_8, x_1);
if (x_75 == 0)
{
lean_object* x_76;
x_76 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printInduct(x_1, x_73, x_70, x_74, x_71, x_72, x_2, x_3, x_7);
return x_76;
}
else
{
lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80;
x_77 = l_Lean_instInhabitedName;
x_78 = lean_unsigned_to_nat(0u);
x_79 = l___private_Init_GetElem_0__List_get_x21Internal___rarg(x_77, x_71, x_78);
lean_dec(x_71);
x_80 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printStructure(x_1, x_73, x_70, x_74, x_79, x_72, x_2, x_3, x_7);
return x_80;
}
}
case 6:
{
lean_object* x_62; lean_object* x_63; uint8_t x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68;
lean_object* x_81; lean_object* x_82; uint8_t x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87;
lean_free_object(x_10);
lean_dec(x_8);
x_62 = lean_ctor_get(x_12, 0);
lean_inc(x_62);
lean_dec(x_12);
x_63 = lean_ctor_get(x_62, 0);
lean_inc(x_63);
x_64 = lean_ctor_get_uint8(x_62, sizeof(void*)*5);
lean_dec(x_62);
x_65 = lean_ctor_get(x_63, 1);
lean_inc(x_65);
x_66 = lean_ctor_get(x_63, 2);
lean_inc(x_66);
lean_dec(x_63);
x_67 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__5;
x_68 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_67, x_1, x_65, x_66, x_64, x_2, x_3, x_7);
return x_68;
x_81 = lean_ctor_get(x_13, 0);
lean_inc(x_81);
lean_dec(x_13);
x_82 = lean_ctor_get(x_81, 0);
lean_inc(x_82);
x_83 = lean_ctor_get_uint8(x_81, sizeof(void*)*5);
lean_dec(x_81);
x_84 = lean_ctor_get(x_82, 1);
lean_inc(x_84);
x_85 = lean_ctor_get(x_82, 2);
lean_inc(x_85);
lean_dec(x_82);
x_86 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__5;
x_87 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_86, x_1, x_84, x_85, x_83, x_2, x_3, x_7);
return x_87;
}
default:
{
lean_object* x_69; lean_object* x_70; uint8_t x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75;
lean_object* x_88; lean_object* x_89; uint8_t x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94;
lean_free_object(x_10);
lean_dec(x_8);
x_69 = lean_ctor_get(x_12, 0);
lean_inc(x_69);
lean_dec(x_12);
x_70 = lean_ctor_get(x_69, 0);
lean_inc(x_70);
x_71 = lean_ctor_get_uint8(x_69, sizeof(void*)*7 + 1);
lean_dec(x_69);
x_72 = lean_ctor_get(x_70, 1);
lean_inc(x_72);
x_73 = lean_ctor_get(x_70, 2);
lean_inc(x_73);
lean_dec(x_70);
x_74 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__6;
x_75 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_74, x_1, x_72, x_73, x_71, x_2, x_3, x_7);
return x_75;
x_88 = lean_ctor_get(x_13, 0);
lean_inc(x_88);
lean_dec(x_13);
x_89 = lean_ctor_get(x_88, 0);
lean_inc(x_89);
x_90 = lean_ctor_get_uint8(x_88, sizeof(void*)*7 + 1);
lean_dec(x_88);
x_91 = lean_ctor_get(x_89, 1);
lean_inc(x_91);
x_92 = lean_ctor_get(x_89, 2);
lean_inc(x_92);
lean_dec(x_89);
x_93 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__6;
x_94 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_93, x_1, x_91, x_92, x_90, x_2, x_3, x_7);
return x_94;
}
}
}
else
{
lean_object* x_95;
x_95 = lean_ctor_get(x_10, 0);
lean_inc(x_95);
lean_dec(x_10);
switch (lean_obj_tag(x_95)) {
case 0:
{
lean_object* x_96; lean_object* x_97; uint8_t x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101;
x_96 = lean_ctor_get(x_95, 0);
lean_inc(x_96);
lean_dec(x_95);
x_97 = lean_ctor_get(x_96, 0);
lean_inc(x_97);
x_98 = lean_ctor_get_uint8(x_96, sizeof(void*)*1);
lean_dec(x_96);
x_99 = lean_ctor_get(x_97, 1);
lean_inc(x_99);
x_100 = lean_ctor_get(x_97, 2);
lean_inc(x_100);
lean_dec(x_97);
lean_inc(x_1);
x_101 = l_Lean_getOriginalConstKind_x3f(x_8, x_1);
if (lean_obj_tag(x_101) == 0)
{
lean_object* x_102; lean_object* x_103;
x_102 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__1;
x_103 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_102, x_1, x_99, x_100, x_98, x_2, x_3, x_7);
return x_103;
}
else
{
lean_object* x_104;
x_104 = lean_ctor_get(x_101, 0);
lean_inc(x_104);
lean_dec(x_101);
switch (lean_obj_tag(x_104)) {
case 0:
{
lean_object* x_105;
x_105 = lean_box(0);
if (x_98 == 0)
{
lean_object* x_106; uint8_t x_107; lean_object* x_108;
x_106 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__2;
x_107 = 1;
x_108 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike(x_106, x_1, x_99, x_100, x_105, x_107, x_2, x_3, x_7);
return x_108;
}
else
{
lean_object* x_109; uint8_t x_110; lean_object* x_111;
x_109 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__2;
x_110 = 0;
x_111 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike(x_109, x_1, x_99, x_100, x_105, x_110, x_2, x_3, x_7);
return x_111;
}
}
case 1:
{
lean_object* x_112;
x_112 = lean_box(0);
if (x_98 == 0)
{
lean_object* x_113; uint8_t x_114; lean_object* x_115;
x_113 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__3;
x_114 = 1;
x_115 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike(x_113, x_1, x_99, x_100, x_112, x_114, x_2, x_3, x_7);
return x_115;
}
else
{
lean_object* x_116; uint8_t x_117; lean_object* x_118;
x_116 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__3;
x_117 = 0;
x_118 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike(x_116, x_1, x_99, x_100, x_112, x_117, x_2, x_3, x_7);
return x_118;
}
}
default:
{
lean_object* x_119; lean_object* x_120;
lean_dec(x_104);
x_119 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__1;
x_120 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_119, x_1, x_99, x_100, x_98, x_2, x_3, x_7);
return x_120;
}
}
}
}
case 1:
{
lean_object* x_121; lean_object* x_122; lean_object* x_123; uint8_t x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129;
lean_dec(x_8);
x_121 = lean_ctor_get(x_95, 0);
lean_inc(x_121);
lean_dec(x_95);
x_122 = lean_ctor_get(x_121, 0);
lean_inc(x_122);
x_123 = lean_ctor_get(x_121, 1);
lean_inc(x_123);
x_124 = lean_ctor_get_uint8(x_121, sizeof(void*)*4);
lean_dec(x_121);
x_125 = lean_ctor_get(x_122, 1);
lean_inc(x_125);
x_126 = lean_ctor_get(x_122, 2);
lean_inc(x_126);
lean_dec(x_122);
x_127 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_127, 0, x_123);
x_128 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__2;
x_129 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike(x_128, x_1, x_125, x_126, x_127, x_124, x_2, x_3, x_7);
return x_129;
}
case 2:
{
lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; uint8_t x_137; lean_object* x_138;
lean_dec(x_8);
x_130 = lean_ctor_get(x_95, 0);
lean_inc(x_130);
lean_dec(x_95);
x_131 = lean_ctor_get(x_130, 0);
lean_inc(x_131);
x_132 = lean_ctor_get(x_130, 1);
lean_inc(x_132);
lean_dec(x_130);
x_133 = lean_ctor_get(x_131, 1);
lean_inc(x_133);
x_134 = lean_ctor_get(x_131, 2);
lean_inc(x_134);
lean_dec(x_131);
x_135 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_135, 0, x_132);
x_136 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__3;
x_137 = 1;
x_138 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike(x_136, x_1, x_133, x_134, x_135, x_137, x_2, x_3, x_7);
return x_138;
}
case 3:
{
lean_object* x_139; lean_object* x_140; uint8_t x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144; lean_object* x_145;
lean_dec(x_8);
x_139 = lean_ctor_get(x_95, 0);
lean_inc(x_139);
lean_dec(x_95);
x_140 = lean_ctor_get(x_139, 0);
lean_inc(x_140);
x_141 = lean_ctor_get_uint8(x_139, sizeof(void*)*3);
lean_dec(x_139);
x_142 = lean_ctor_get(x_140, 1);
lean_inc(x_142);
x_143 = lean_ctor_get(x_140, 2);
lean_inc(x_143);
lean_dec(x_140);
x_144 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__4;
x_145 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_144, x_1, x_142, x_143, x_141, x_2, x_3, x_7);
return x_145;
}
case 4:
{
lean_object* x_146; lean_object* x_147; lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151;
lean_dec(x_8);
x_146 = lean_ctor_get(x_95, 0);
lean_inc(x_146);
lean_dec(x_95);
x_147 = lean_ctor_get(x_146, 0);
lean_inc(x_147);
lean_dec(x_146);
x_148 = lean_ctor_get(x_147, 1);
lean_inc(x_148);
x_149 = lean_ctor_get(x_147, 2);
lean_inc(x_149);
lean_dec(x_147);
x_150 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printQuot___closed__1;
x_151 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_150, x_1, x_148, x_149, x_9, x_2, x_3, x_7);
return x_151;
}
case 5:
{
lean_object* x_152; lean_object* x_153; lean_object* x_154; lean_object* x_155; uint8_t x_156; lean_object* x_157; lean_object* x_158; uint8_t x_159;
x_152 = lean_ctor_get(x_95, 0);
lean_inc(x_152);
lean_dec(x_95);
x_153 = lean_ctor_get(x_152, 0);
lean_inc(x_153);
x_154 = lean_ctor_get(x_152, 1);
lean_inc(x_154);
x_155 = lean_ctor_get(x_152, 4);
lean_inc(x_155);
x_156 = lean_ctor_get_uint8(x_152, sizeof(void*)*6 + 1);
lean_dec(x_152);
x_157 = lean_ctor_get(x_153, 1);
lean_inc(x_157);
x_158 = lean_ctor_get(x_153, 2);
lean_inc(x_158);
lean_dec(x_153);
lean_inc(x_1);
x_159 = l_Lean_isStructure(x_8, x_1);
if (x_159 == 0)
{
lean_object* x_160;
x_160 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printInduct(x_1, x_157, x_154, x_158, x_155, x_156, x_2, x_3, x_7);
return x_160;
}
else
{
lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164;
x_161 = l_Lean_instInhabitedName;
x_162 = lean_unsigned_to_nat(0u);
x_163 = l___private_Init_GetElem_0__List_get_x21Internal___rarg(x_161, x_155, x_162);
lean_dec(x_155);
x_164 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printStructure(x_1, x_157, x_154, x_158, x_163, x_156, x_2, x_3, x_7);
return x_164;
}
}
case 6:
{
lean_object* x_165; lean_object* x_166; uint8_t x_167; lean_object* x_168; lean_object* x_169; lean_object* x_170; lean_object* x_171;
lean_dec(x_8);
x_165 = lean_ctor_get(x_95, 0);
lean_inc(x_165);
lean_dec(x_95);
x_166 = lean_ctor_get(x_165, 0);
lean_inc(x_166);
x_167 = lean_ctor_get_uint8(x_165, sizeof(void*)*5);
lean_dec(x_165);
x_168 = lean_ctor_get(x_166, 1);
lean_inc(x_168);
x_169 = lean_ctor_get(x_166, 2);
lean_inc(x_169);
lean_dec(x_166);
x_170 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__5;
x_171 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_170, x_1, x_168, x_169, x_167, x_2, x_3, x_7);
return x_171;
}
default:
{
lean_object* x_172; lean_object* x_173; uint8_t x_174; lean_object* x_175; lean_object* x_176; lean_object* x_177; lean_object* x_178;
lean_dec(x_8);
x_172 = lean_ctor_get(x_95, 0);
lean_inc(x_172);
lean_dec(x_95);
x_173 = lean_ctor_get(x_172, 0);
lean_inc(x_173);
x_174 = lean_ctor_get_uint8(x_172, sizeof(void*)*7 + 1);
lean_dec(x_172);
x_175 = lean_ctor_get(x_173, 1);
lean_inc(x_175);
x_176 = lean_ctor_get(x_173, 2);
lean_inc(x_176);
lean_dec(x_173);
x_177 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__6;
x_178 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomLike(x_177, x_1, x_175, x_176, x_174, x_2, x_3, x_7);
return x_178;
}
}
}
}
@ -13041,7 +13426,7 @@ x_8 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
lean_dec(x_7);
x_9 = l_Lean_collectAxioms___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomsOf___spec__1___closed__1;
x_10 = l_Lean_CollectAxioms_collect(x_1, x_8, x_9);
x_10 = l___private_Lean_Util_CollectAxioms_0__Lean_CollectAxioms_collect(x_1, x_8, x_9);
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
@ -13063,7 +13448,7 @@ x_15 = lean_ctor_get(x_13, 0);
lean_inc(x_15);
lean_dec(x_13);
x_16 = l_Lean_collectAxioms___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printAxiomsOf___spec__1___closed__1;
x_17 = l_Lean_CollectAxioms_collect(x_1, x_15, x_16);
x_17 = l___private_Lean_Util_CollectAxioms_0__Lean_CollectAxioms_collect(x_1, x_15, x_16);
x_18 = lean_ctor_get(x_17, 1);
lean_inc(x_18);
lean_dec(x_17);
@ -14416,6 +14801,12 @@ l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader___closed__22 = _init_l
lean_mark_persistent(l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader___closed__22);
l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader___closed__23 = _init_l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader___closed__23();
lean_mark_persistent(l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader___closed__23);
l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__1 = _init_l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__1);
l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__2 = _init_l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__2();
lean_mark_persistent(l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__2);
l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__3 = _init_l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__3();
lean_mark_persistent(l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkOmittedMsg___closed__3);
l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike___closed__1 = _init_l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike___closed__1();
lean_mark_persistent(l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike___closed__1);
l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike___closed__2 = _init_l___private_Lean_Elab_Print_0__Lean_Elab_Command_printDefLike___closed__2();

View file

@ -15342,7 +15342,7 @@ static lean_object* _init_l_Lean_Elab_Tactic_Omega_asLinearComboImpl_handleNatCa
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("ofNat_emod", 10, 10);
x_1 = lean_mk_string_unchecked("natCast_emod", 12, 12);
return x_1;
}
}
@ -15408,7 +15408,7 @@ static lean_object* _init_l_Lean_Elab_Tactic_Omega_asLinearComboImpl_handleNatCa
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("ofNat_ediv", 10, 10);
x_1 = lean_mk_string_unchecked("natCast_ediv", 12, 12);
return x_1;
}
}
@ -15494,7 +15494,7 @@ static lean_object* _init_l_Lean_Elab_Tactic_Omega_asLinearComboImpl_handleNatCa
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("ofNat_add", 9, 9);
x_1 = lean_mk_string_unchecked("natCast_add", 11, 11);
return x_1;
}
}

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

View file

@ -188,7 +188,6 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Completion_tact
LEAN_EXPORT lean_object* l___private_Lean_Server_Completion_CompletionCollectors_0__Lean_Server_Completion_normPrivateName_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_RBNode_forIn_visit___at_Lean_Server_Completion_optionCompletion___spec__1___closed__3;
LEAN_EXPORT lean_object* l_Lean_Server_Completion_dotIdCompletion___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_ConstantInfo_isTheorem(lean_object*);
static lean_object* l_List_forIn_x27_loop___at___private_Lean_Server_Completion_CompletionCollectors_0__Lean_Server_Completion_idCompletionCore___spec__22___closed__1;
lean_object* lean_st_ref_take(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_Completion_forEligibleDeclsM___at___private_Lean_Server_Completion_CompletionCollectors_0__Lean_Server_Completion_forEligibleDeclsWithCancellationM___spec__1___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -494,6 +493,7 @@ lean_object* l_Lean_Expr_consumeMData(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Server_Completion_CompletionCollectors_0__Lean_Server_Completion_forEligibleDeclsWithCancellationM___rarg___lambda__8___boxed(lean_object*, lean_object*);
static lean_object* l___private_Lean_Server_Completion_CompletionCollectors_0__Lean_Server_Completion_forEligibleDeclsWithCancellationM___rarg___lambda__4___closed__1;
uint8_t l_Lean_Name_isInternal(lean_object*);
uint8_t l_Lean_wasOriginallyTheorem(lean_object*, lean_object*);
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_forM___at___private_Lean_Server_Completion_CompletionCollectors_0__Lean_Server_Completion_idCompletionCore___spec__25(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_Completion_dotIdCompletion___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1682,15 +1682,15 @@ uint8_t x_16;
x_16 = l_Lean_ConstantInfo_isInductive(x_1);
if (x_16 == 0)
{
uint8_t x_17;
lean_dec(x_14);
x_17 = l_Lean_ConstantInfo_isTheorem(x_1);
if (x_17 == 0)
lean_object* x_17; uint8_t x_18;
x_17 = l_Lean_ConstantInfo_name(x_1);
lean_inc(x_17);
x_18 = l_Lean_wasOriginallyTheorem(x_14, x_17);
if (x_18 == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22;
lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22;
lean_free_object(x_10);
x_18 = l_Lean_ConstantInfo_name(x_1);
x_19 = l_Lean_isProjectionFn___at___private_Lean_Server_Completion_CompletionCollectors_0__Lean_Server_Completion_getCompletionKindForDecl___spec__1(x_18, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_13);
x_19 = l_Lean_isProjectionFn___at___private_Lean_Server_Completion_CompletionCollectors_0__Lean_Server_Completion_getCompletionKindForDecl___spec__1(x_17, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_13);
x_20 = lean_ctor_get(x_19, 0);
lean_inc(x_20);
x_21 = lean_ctor_get(x_20, 0);
@ -1944,6 +1944,7 @@ return x_79;
else
{
lean_object* x_80;
lean_dec(x_17);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
@ -2099,14 +2100,14 @@ uint8_t x_109;
x_109 = l_Lean_ConstantInfo_isInductive(x_1);
if (x_109 == 0)
{
uint8_t x_110;
lean_dec(x_107);
x_110 = l_Lean_ConstantInfo_isTheorem(x_1);
if (x_110 == 0)
lean_object* x_110; uint8_t x_111;
x_110 = l_Lean_ConstantInfo_name(x_1);
lean_inc(x_110);
x_111 = l_Lean_wasOriginallyTheorem(x_107, x_110);
if (x_111 == 0)
{
lean_object* x_111; lean_object* x_112; lean_object* x_113; lean_object* x_114; uint8_t x_115;
x_111 = l_Lean_ConstantInfo_name(x_1);
x_112 = l_Lean_isProjectionFn___at___private_Lean_Server_Completion_CompletionCollectors_0__Lean_Server_Completion_getCompletionKindForDecl___spec__1(x_111, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_106);
lean_object* x_112; lean_object* x_113; lean_object* x_114; uint8_t x_115;
x_112 = l_Lean_isProjectionFn___at___private_Lean_Server_Completion_CompletionCollectors_0__Lean_Server_Completion_getCompletionKindForDecl___spec__1(x_110, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_106);
x_113 = lean_ctor_get(x_112, 0);
lean_inc(x_113);
x_114 = lean_ctor_get(x_113, 0);
@ -2288,6 +2289,7 @@ return x_151;
else
{
lean_object* x_152; lean_object* x_153;
lean_dec(x_110);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Std.Internal.Async.TCP
// Imports: Std.Time Std.Internal.UV Std.Internal.Async.Basic Std.Net.Addr
// Imports: Std.Time Std.Internal.UV.TCP Std.Internal.Async.Select Std.Net.Addr
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -17,12 +17,16 @@ LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Server_getSockName(l
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__22;
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__3;
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__26;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__1___boxed(lean_object*, lean_object*);
lean_object* lean_uv_tcp_bind(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_mk(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_uv_tcp_getsockname(lean_object*, lean_object*);
lean_object* l_Std_Internal_IO_Async_AsyncTask_block___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Server_noDelay___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_getPeerName(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Server_accept___lambda__1(lean_object*);
static lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___closed__2;
lean_object* lean_uv_tcp_connect(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_noDelay___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_shutdown(lean_object*, lean_object*);
@ -32,18 +36,25 @@ lean_object* lean_array_push(lean_object*, lean_object*);
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__1;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Server_keepAlive___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_uv_tcp_getpeername(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_Waiter_race___at_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___spec__2(uint64_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recv_x3f___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Internal_IO_Async_TCP_Socket_Server_accept___closed__1;
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__16;
lean_object* lean_uv_tcp_send(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Server_listen(lean_object*, uint32_t, lean_object*);
lean_object* l_IO_Promise_isResolved___rarg(lean_object*, lean_object*);
lean_object* lean_uv_tcp_nodelay(lean_object*, lean_object*);
lean_object* lean_uv_tcp_new(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_connect___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__27;
lean_object* lean_io_promise_resolve(lean_object*, lean_object*, lean_object*);
lean_object* lean_io_promise_result_opt(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__5;
lean_object* lean_st_ref_take(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Server_mk(lean_object*);
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__14;
LEAN_EXPORT lean_object* l_IO_ofExcept___at_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___spec__1(lean_object*, lean_object*);
uint32_t lean_uint32_of_nat(lean_object*);
lean_object* lean_uv_tcp_listen(lean_object*, uint32_t, lean_object*);
uint8_t lean_bool_to_int8(uint8_t);
@ -58,22 +69,29 @@ static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__8;
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__9;
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__2;
lean_object* l_EStateM_pure___rarg(lean_object*, lean_object*);
lean_object* lean_uv_tcp_wait_readable(lean_object*, lean_object*);
lean_object* lean_io_map_task(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_bind___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Task_Priority_default;
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__4;
lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
lean_object* lean_uv_tcp_accept(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Server_getSockName___boxed(lean_object*, lean_object*);
static lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___closed__1;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Server_bind(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134_;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Server_bind___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_bind(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_keepAlive___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__25;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector(lean_object*, uint64_t, lean_object*);
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__12;
lean_object* lean_uv_tcp_keepalive(lean_object*, uint8_t, uint32_t, lean_object*);
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__7;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Server_accept___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_uv_tcp_recv(lean_object*, uint64_t, lean_object*);
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__19;
lean_object* l_Int_toNat(lean_object*);
@ -81,20 +99,29 @@ LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Server_noDelay(lean_
lean_object* l_IO_Promise_result_x21___rarg(lean_object*);
lean_object* lean_task_map(lean_object*, lean_object*, lean_object*, uint8_t);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_shutdown___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__2(lean_object*, uint64_t, uint8_t, lean_object*);
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__10;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_keepAlive(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_getSockName___boxed(lean_object*, lean_object*);
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__6;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_Waiter_race___at_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_Internal_UV_TCP_Socket_cancelRecv___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Server_accept(lean_object*, lean_object*);
lean_object* lean_io_error_to_string(lean_object*);
lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_536_;
lean_object* l_Lean_Name_mkStr4(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_noDelay(lean_object*, lean_object*);
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__11;
LEAN_EXPORT lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_269_;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__4(lean_object*, uint64_t, lean_object*, lean_object*, lean_object*);
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__13;
lean_object* lean_uv_tcp_shutdown(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_send___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3(uint64_t, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__20;
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Server_keepAlive(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_getPeerName___boxed(lean_object*, lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_connect(lean_object*, lean_object*, lean_object*);
@ -938,6 +965,754 @@ lean_dec(x_1);
return x_5;
}
}
LEAN_EXPORT lean_object* l_IO_ofExcept___at_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
uint8_t x_3;
x_3 = !lean_is_exclusive(x_1);
if (x_3 == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_1, 0);
x_5 = lean_io_error_to_string(x_4);
lean_ctor_set_tag(x_1, 18);
lean_ctor_set(x_1, 0, x_5);
x_6 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_2);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_7 = lean_ctor_get(x_1, 0);
lean_inc(x_7);
lean_dec(x_1);
x_8 = lean_io_error_to_string(x_7);
x_9 = lean_alloc_ctor(18, 1, 0);
lean_ctor_set(x_9, 0, x_8);
x_10 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_10, 0, x_9);
lean_ctor_set(x_10, 1, x_2);
return x_10;
}
}
else
{
lean_object* x_11; lean_object* x_12;
x_11 = lean_ctor_get(x_1, 0);
lean_inc(x_11);
lean_dec(x_1);
x_12 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_12, 0, x_11);
lean_ctor_set(x_12, 1, x_2);
return x_12;
}
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_Waiter_race___at_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___spec__2(uint64_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
uint8_t x_7; lean_object* x_8; lean_object* x_51; lean_object* x_52; lean_object* x_53; uint8_t x_54;
x_51 = lean_ctor_get(x_4, 0);
x_52 = lean_st_ref_take(x_51, x_6);
x_53 = lean_ctor_get(x_52, 0);
lean_inc(x_53);
x_54 = lean_unbox(x_53);
lean_dec(x_53);
if (x_54 == 0)
{
lean_object* x_55; uint8_t x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59;
x_55 = lean_ctor_get(x_52, 1);
lean_inc(x_55);
lean_dec(x_52);
x_56 = 1;
x_57 = lean_box(x_56);
x_58 = lean_st_ref_set(x_51, x_57, x_55);
x_59 = lean_ctor_get(x_58, 1);
lean_inc(x_59);
lean_dec(x_58);
x_7 = x_56;
x_8 = x_59;
goto block_50;
}
else
{
lean_object* x_60; uint8_t x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; uint8_t x_65;
x_60 = lean_ctor_get(x_52, 1);
lean_inc(x_60);
lean_dec(x_52);
x_61 = 1;
x_62 = lean_box(x_61);
x_63 = lean_st_ref_set(x_51, x_62, x_60);
x_64 = lean_ctor_get(x_63, 1);
lean_inc(x_64);
lean_dec(x_63);
x_65 = 0;
x_7 = x_65;
x_8 = x_64;
goto block_50;
}
block_50:
{
if (x_7 == 0)
{
lean_object* x_9;
lean_dec(x_3);
x_9 = lean_apply_1(x_5, x_8);
return x_9;
}
else
{
lean_object* x_10; lean_object* x_11;
lean_dec(x_5);
x_10 = lean_ctor_get(x_4, 1);
x_11 = l_IO_ofExcept___at_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___spec__1(x_3, x_8);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13;
x_12 = lean_ctor_get(x_11, 1);
lean_inc(x_12);
lean_dec(x_11);
x_13 = lean_uv_tcp_recv(x_2, x_1, x_12);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_14 = lean_ctor_get(x_13, 0);
lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 1);
lean_inc(x_15);
lean_dec(x_13);
x_16 = l_IO_Promise_result_x21___rarg(x_14);
lean_dec(x_14);
x_17 = l_Std_Internal_IO_Async_AsyncTask_block___rarg(x_16, x_15);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22;
x_18 = lean_ctor_get(x_17, 0);
lean_inc(x_18);
x_19 = lean_ctor_get(x_17, 1);
lean_inc(x_19);
lean_dec(x_17);
x_20 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_20, 0, x_18);
x_21 = lean_io_promise_resolve(x_20, x_10, x_19);
x_22 = !lean_is_exclusive(x_21);
if (x_22 == 0)
{
return x_21;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_23 = lean_ctor_get(x_21, 0);
x_24 = lean_ctor_get(x_21, 1);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_21);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
return x_25;
}
}
else
{
lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; uint8_t x_30;
x_26 = lean_ctor_get(x_17, 0);
lean_inc(x_26);
x_27 = lean_ctor_get(x_17, 1);
lean_inc(x_27);
lean_dec(x_17);
x_28 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_28, 0, x_26);
x_29 = lean_io_promise_resolve(x_28, x_10, x_27);
x_30 = !lean_is_exclusive(x_29);
if (x_30 == 0)
{
return x_29;
}
else
{
lean_object* x_31; lean_object* x_32; lean_object* x_33;
x_31 = lean_ctor_get(x_29, 0);
x_32 = lean_ctor_get(x_29, 1);
lean_inc(x_32);
lean_inc(x_31);
lean_dec(x_29);
x_33 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_33, 0, x_31);
lean_ctor_set(x_33, 1, x_32);
return x_33;
}
}
}
else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; uint8_t x_38;
x_34 = lean_ctor_get(x_13, 0);
lean_inc(x_34);
x_35 = lean_ctor_get(x_13, 1);
lean_inc(x_35);
lean_dec(x_13);
x_36 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_36, 0, x_34);
x_37 = lean_io_promise_resolve(x_36, x_10, x_35);
x_38 = !lean_is_exclusive(x_37);
if (x_38 == 0)
{
return x_37;
}
else
{
lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_39 = lean_ctor_get(x_37, 0);
x_40 = lean_ctor_get(x_37, 1);
lean_inc(x_40);
lean_inc(x_39);
lean_dec(x_37);
x_41 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_41, 0, x_39);
lean_ctor_set(x_41, 1, x_40);
return x_41;
}
}
}
else
{
lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; uint8_t x_46;
x_42 = lean_ctor_get(x_11, 0);
lean_inc(x_42);
x_43 = lean_ctor_get(x_11, 1);
lean_inc(x_43);
lean_dec(x_11);
x_44 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_44, 0, x_42);
x_45 = lean_io_promise_resolve(x_44, x_10, x_43);
x_46 = !lean_is_exclusive(x_45);
if (x_46 == 0)
{
return x_45;
}
else
{
lean_object* x_47; lean_object* x_48; lean_object* x_49;
x_47 = lean_ctor_get(x_45, 0);
x_48 = lean_ctor_get(x_45, 1);
lean_inc(x_48);
lean_inc(x_47);
lean_dec(x_45);
x_49 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_49, 0, x_47);
lean_ctor_set(x_49, 1, x_48);
return x_49;
}
}
}
}
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
x_3 = l_IO_Promise_isResolved___rarg(x_1, x_2);
x_4 = !lean_is_exclusive(x_3);
if (x_4 == 0)
{
return x_3;
}
else
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = lean_ctor_get(x_3, 0);
x_6 = lean_ctor_get(x_3, 1);
lean_inc(x_6);
lean_inc(x_5);
lean_dec(x_3);
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_5);
lean_ctor_set(x_7, 1, x_6);
return x_7;
}
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__2(lean_object* x_1, uint64_t x_2, uint8_t x_3, lean_object* x_4) {
_start:
{
if (x_3 == 0)
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_box(0);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_5);
lean_ctor_set(x_6, 1, x_4);
return x_6;
}
else
{
lean_object* x_7;
x_7 = lean_uv_tcp_recv(x_1, x_2, x_4);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_8 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
x_9 = lean_ctor_get(x_7, 1);
lean_inc(x_9);
lean_dec(x_7);
x_10 = l_IO_Promise_result_x21___rarg(x_8);
lean_dec(x_8);
x_11 = l_Std_Internal_IO_Async_AsyncTask_block___rarg(x_10, x_9);
if (lean_obj_tag(x_11) == 0)
{
uint8_t x_12;
x_12 = !lean_is_exclusive(x_11);
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_11, 0);
x_14 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_11, 0, x_14);
return x_11;
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_15 = lean_ctor_get(x_11, 0);
x_16 = lean_ctor_get(x_11, 1);
lean_inc(x_16);
lean_inc(x_15);
lean_dec(x_11);
x_17 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_17, 0, x_15);
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_16);
return x_18;
}
}
else
{
uint8_t x_19;
x_19 = !lean_is_exclusive(x_11);
if (x_19 == 0)
{
return x_11;
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_20 = lean_ctor_get(x_11, 0);
x_21 = lean_ctor_get(x_11, 1);
lean_inc(x_21);
lean_inc(x_20);
lean_dec(x_11);
x_22 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
return x_22;
}
}
}
else
{
uint8_t x_23;
x_23 = !lean_is_exclusive(x_7);
if (x_23 == 0)
{
return x_7;
}
else
{
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = lean_ctor_get(x_7, 0);
x_25 = lean_ctor_get(x_7, 1);
lean_inc(x_25);
lean_inc(x_24);
lean_dec(x_7);
x_26 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_26, 0, x_24);
lean_ctor_set(x_26, 1, x_25);
return x_26;
}
}
}
}
}
static lean_object* _init_l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_box(0);
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_box(0);
x_2 = lean_alloc_closure((void*)(l_EStateM_pure___rarg), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3(uint64_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_6; lean_object* x_7;
x_6 = l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___closed__1;
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_5);
return x_7;
}
else
{
uint8_t x_8;
x_8 = !lean_is_exclusive(x_4);
if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = lean_ctor_get(x_4, 0);
x_10 = l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___closed__2;
x_11 = l_Std_Internal_IO_Async_Waiter_race___at_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___spec__2(x_1, x_2, x_9, x_3, x_10, x_5);
if (lean_obj_tag(x_11) == 0)
{
uint8_t x_12;
x_12 = !lean_is_exclusive(x_11);
if (x_12 == 0)
{
lean_object* x_13;
x_13 = lean_ctor_get(x_11, 0);
lean_ctor_set(x_4, 0, x_13);
lean_ctor_set(x_11, 0, x_4);
return x_11;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_14 = lean_ctor_get(x_11, 0);
x_15 = lean_ctor_get(x_11, 1);
lean_inc(x_15);
lean_inc(x_14);
lean_dec(x_11);
lean_ctor_set(x_4, 0, x_14);
x_16 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_16, 0, x_4);
lean_ctor_set(x_16, 1, x_15);
return x_16;
}
}
else
{
uint8_t x_17;
x_17 = !lean_is_exclusive(x_11);
if (x_17 == 0)
{
lean_object* x_18;
x_18 = lean_ctor_get(x_11, 0);
lean_ctor_set_tag(x_4, 0);
lean_ctor_set(x_4, 0, x_18);
lean_ctor_set_tag(x_11, 0);
lean_ctor_set(x_11, 0, x_4);
return x_11;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_11, 0);
x_20 = lean_ctor_get(x_11, 1);
lean_inc(x_20);
lean_inc(x_19);
lean_dec(x_11);
lean_ctor_set_tag(x_4, 0);
lean_ctor_set(x_4, 0, x_19);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_4);
lean_ctor_set(x_21, 1, x_20);
return x_21;
}
}
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_22 = lean_ctor_get(x_4, 0);
lean_inc(x_22);
lean_dec(x_4);
x_23 = l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___closed__2;
x_24 = l_Std_Internal_IO_Async_Waiter_race___at_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___spec__2(x_1, x_2, x_22, x_3, x_23, x_5);
if (lean_obj_tag(x_24) == 0)
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_25 = lean_ctor_get(x_24, 0);
lean_inc(x_25);
x_26 = lean_ctor_get(x_24, 1);
lean_inc(x_26);
if (lean_is_exclusive(x_24)) {
lean_ctor_release(x_24, 0);
lean_ctor_release(x_24, 1);
x_27 = x_24;
} else {
lean_dec_ref(x_24);
x_27 = lean_box(0);
}
x_28 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_28, 0, x_25);
if (lean_is_scalar(x_27)) {
x_29 = lean_alloc_ctor(0, 2, 0);
} else {
x_29 = x_27;
}
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_26);
return x_29;
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34;
x_30 = lean_ctor_get(x_24, 0);
lean_inc(x_30);
x_31 = lean_ctor_get(x_24, 1);
lean_inc(x_31);
if (lean_is_exclusive(x_24)) {
lean_ctor_release(x_24, 0);
lean_ctor_release(x_24, 1);
x_32 = x_24;
} else {
lean_dec_ref(x_24);
x_32 = lean_box(0);
}
x_33 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_33, 0, x_30);
if (lean_is_scalar(x_32)) {
x_34 = lean_alloc_ctor(0, 2, 0);
} else {
x_34 = x_32;
lean_ctor_set_tag(x_34, 0);
}
lean_ctor_set(x_34, 0, x_33);
lean_ctor_set(x_34, 1, x_31);
return x_34;
}
}
}
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__4(lean_object* x_1, uint64_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; uint8_t x_12;
x_6 = lean_io_promise_result_opt(x_1);
x_7 = lean_box_uint64(x_2);
x_8 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___boxed), 5, 3);
lean_closure_set(x_8, 0, x_7);
lean_closure_set(x_8, 1, x_3);
lean_closure_set(x_8, 2, x_4);
x_9 = l_Task_Priority_default;
x_10 = 0;
x_11 = lean_io_map_task(x_8, x_6, x_9, x_10, x_5);
x_12 = !lean_is_exclusive(x_11);
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_11, 0);
lean_dec(x_13);
x_14 = lean_box(0);
lean_ctor_set(x_11, 0, x_14);
return x_11;
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_ctor_get(x_11, 1);
lean_inc(x_15);
lean_dec(x_11);
x_16 = lean_box(0);
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_15);
return x_17;
}
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector(lean_object* x_1, uint64_t x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_uv_tcp_wait_readable(x_1, x_3);
if (lean_obj_tag(x_4) == 0)
{
uint8_t x_5;
x_5 = !lean_is_exclusive(x_4);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_6 = lean_ctor_get(x_4, 0);
lean_inc(x_6);
x_7 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__1___boxed), 2, 1);
lean_closure_set(x_7, 0, x_6);
x_8 = lean_box_uint64(x_2);
lean_inc(x_1);
x_9 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__2___boxed), 4, 2);
lean_closure_set(x_9, 0, x_1);
lean_closure_set(x_9, 1, x_8);
x_10 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_10, 0, x_7);
lean_closure_set(x_10, 1, x_9);
x_11 = lean_box_uint64(x_2);
lean_inc(x_1);
x_12 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__4___boxed), 5, 3);
lean_closure_set(x_12, 0, x_6);
lean_closure_set(x_12, 1, x_11);
lean_closure_set(x_12, 2, x_1);
x_13 = lean_alloc_closure((void*)(l_Std_Internal_UV_TCP_Socket_cancelRecv___boxed), 2, 1);
lean_closure_set(x_13, 0, x_1);
x_14 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_14, 0, x_10);
lean_ctor_set(x_14, 1, x_12);
lean_ctor_set(x_14, 2, x_13);
lean_ctor_set(x_4, 0, x_14);
return x_4;
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_15 = lean_ctor_get(x_4, 0);
x_16 = lean_ctor_get(x_4, 1);
lean_inc(x_16);
lean_inc(x_15);
lean_dec(x_4);
lean_inc(x_15);
x_17 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__1___boxed), 2, 1);
lean_closure_set(x_17, 0, x_15);
x_18 = lean_box_uint64(x_2);
lean_inc(x_1);
x_19 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__2___boxed), 4, 2);
lean_closure_set(x_19, 0, x_1);
lean_closure_set(x_19, 1, x_18);
x_20 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_20, 0, x_17);
lean_closure_set(x_20, 1, x_19);
x_21 = lean_box_uint64(x_2);
lean_inc(x_1);
x_22 = lean_alloc_closure((void*)(l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__4___boxed), 5, 3);
lean_closure_set(x_22, 0, x_15);
lean_closure_set(x_22, 1, x_21);
lean_closure_set(x_22, 2, x_1);
x_23 = lean_alloc_closure((void*)(l_Std_Internal_UV_TCP_Socket_cancelRecv___boxed), 2, 1);
lean_closure_set(x_23, 0, x_1);
x_24 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_24, 0, x_20);
lean_ctor_set(x_24, 1, x_22);
lean_ctor_set(x_24, 2, x_23);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_16);
return x_25;
}
}
else
{
uint8_t x_26;
lean_dec(x_1);
x_26 = !lean_is_exclusive(x_4);
if (x_26 == 0)
{
return x_4;
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_27 = lean_ctor_get(x_4, 0);
x_28 = lean_ctor_get(x_4, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_dec(x_4);
x_29 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
return x_29;
}
}
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_Waiter_race___at_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
uint64_t x_7; lean_object* x_8;
x_7 = lean_unbox_uint64(x_1);
lean_dec(x_1);
x_8 = l_Std_Internal_IO_Async_Waiter_race___at_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___spec__2(x_7, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_4);
lean_dec(x_2);
return x_8;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__1(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint64_t x_5; uint8_t x_6; lean_object* x_7;
x_5 = lean_unbox_uint64(x_2);
lean_dec(x_2);
x_6 = lean_unbox(x_3);
lean_dec(x_3);
x_7 = l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__2(x_1, x_5, x_6, x_4);
lean_dec(x_1);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
uint64_t x_6; lean_object* x_7;
x_6 = lean_unbox_uint64(x_1);
lean_dec(x_1);
x_7 = l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3(x_6, x_2, x_3, x_4, x_5);
lean_dec(x_3);
lean_dec(x_2);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
uint64_t x_6; lean_object* x_7;
x_6 = lean_unbox_uint64(x_2);
lean_dec(x_2);
x_7 = l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__4(x_1, x_6, x_3, x_4, x_5);
lean_dec(x_1);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint64_t x_4; lean_object* x_5;
x_4 = lean_unbox_uint64(x_2);
lean_dec(x_2);
x_5 = l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector(x_1, x_4, x_3);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_IO_Async_TCP_Socket_Client_shutdown(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -1056,7 +1831,7 @@ lean_dec(x_1);
return x_3;
}
}
static lean_object* _init_l___auto____x40_Std_Internal_Async_TCP___hyg_269_() {
static lean_object* _init_l___auto____x40_Std_Internal_Async_TCP___hyg_536_() {
_start:
{
lean_object* x_1;
@ -1089,8 +1864,8 @@ return x_7;
}
}
lean_object* initialize_Std_Time(uint8_t builtin, lean_object*);
lean_object* initialize_Std_Internal_UV(uint8_t builtin, lean_object*);
lean_object* initialize_Std_Internal_Async_Basic(uint8_t builtin, lean_object*);
lean_object* initialize_Std_Internal_UV_TCP(uint8_t builtin, lean_object*);
lean_object* initialize_Std_Internal_Async_Select(uint8_t builtin, lean_object*);
lean_object* initialize_Std_Net_Addr(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Std_Internal_Async_TCP(uint8_t builtin, lean_object* w) {
@ -1100,10 +1875,10 @@ _G_initialized = true;
res = initialize_Std_Time(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Std_Internal_UV(builtin, lean_io_mk_world());
res = initialize_Std_Internal_UV_TCP(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Std_Internal_Async_Basic(builtin, lean_io_mk_world());
res = initialize_Std_Internal_Async_Select(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Std_Net_Addr(builtin, lean_io_mk_world());
@ -1167,8 +1942,12 @@ l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__27 = _init_l___auto_
lean_mark_persistent(l___auto____x40_Std_Internal_Async_TCP___hyg_134____closed__27);
l___auto____x40_Std_Internal_Async_TCP___hyg_134_ = _init_l___auto____x40_Std_Internal_Async_TCP___hyg_134_();
lean_mark_persistent(l___auto____x40_Std_Internal_Async_TCP___hyg_134_);
l___auto____x40_Std_Internal_Async_TCP___hyg_269_ = _init_l___auto____x40_Std_Internal_Async_TCP___hyg_269_();
lean_mark_persistent(l___auto____x40_Std_Internal_Async_TCP___hyg_269_);
l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___closed__1 = _init_l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___closed__1();
lean_mark_persistent(l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___closed__1);
l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___closed__2 = _init_l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___closed__2();
lean_mark_persistent(l_Std_Internal_IO_Async_TCP_Socket_Client_recvSelector___lambda__3___closed__2);
l___auto____x40_Std_Internal_Async_TCP___hyg_536_ = _init_l___auto____x40_Std_Internal_Async_TCP___hyg_536_();
lean_mark_persistent(l___auto____x40_Std_Internal_Async_TCP___hyg_536_);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

View file

@ -16,6 +16,7 @@ extern "C" {
LEAN_EXPORT lean_object* l_Std_Internal_UV_TCP_Socket_keepAlive___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_uv_tcp_bind(lean_object*, lean_object*, lean_object*);
lean_object* lean_uv_tcp_getsockname(lean_object*, lean_object*);
lean_object* lean_uv_tcp_cancel_recv(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Std_Internal_UV_TCP_0__Std_Internal_UV_TCP_SocketImpl;
lean_object* lean_uv_tcp_connect(lean_object*, lean_object*, lean_object*);
lean_object* lean_uv_tcp_getpeername(lean_object*, lean_object*);
@ -27,15 +28,18 @@ lean_object* lean_uv_tcp_new(lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_UV_TCP_Socket_getPeerName___boxed(lean_object*, lean_object*);
lean_object* lean_uv_tcp_listen(lean_object*, uint32_t, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_UV_TCP_Socket_new___boxed(lean_object*);
lean_object* lean_uv_tcp_wait_readable(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_UV_TCP_Socket_bind___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_uv_tcp_accept(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_UV_TCP_Socket_listen___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_uv_tcp_keepalive(lean_object*, uint8_t, uint32_t, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_UV_TCP_Socket_waitReadable___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_UV_TCP_Socket_getSockName___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_UV_TCP_Socket_accept___boxed(lean_object*, lean_object*);
lean_object* lean_uv_tcp_recv(lean_object*, uint64_t, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_UV_TCP_Socket_send___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_UV_TCP_Socket_noDelay___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_UV_TCP_Socket_cancelRecv___boxed(lean_object*, lean_object*);
lean_object* lean_uv_tcp_shutdown(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Internal_UV_TCP_Socket_shutdown___boxed(lean_object*, lean_object*);
static lean_object* _init_l___private_Std_Internal_UV_TCP_0__Std_Internal_UV_TCP_SocketImpl() {
@ -82,6 +86,24 @@ lean_dec(x_1);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_UV_TCP_Socket_waitReadable___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_uv_tcp_wait_readable(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_UV_TCP_Socket_cancelRecv___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_uv_tcp_cancel_recv(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Std_Internal_UV_TCP_Socket_bind___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{