chore: update stage0
This commit is contained in:
parent
d2d32f13c0
commit
06ba748221
28 changed files with 28995 additions and 9872 deletions
2
stage0/src/runtime/CMakeLists.txt
generated
2
stage0/src/runtime/CMakeLists.txt
generated
|
|
@ -3,7 +3,7 @@ object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
|
|||
stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp byteslice.cpp
|
||||
platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
|
||||
process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp uv/event_loop.cpp
|
||||
uv/timer.cpp uv/tcp.cpp uv/udp.cpp uv/dns.cpp uv/system.cpp)
|
||||
uv/timer.cpp uv/tcp.cpp uv/udp.cpp uv/dns.cpp uv/system.cpp uv/signal.cpp)
|
||||
if (USE_MIMALLOC)
|
||||
list(APPEND RUNTIME_OBJS ${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc/src/static.c)
|
||||
# Lean code includes it as `lean/mimalloc.h` but for compiling `static.c` itself, add original dir
|
||||
|
|
|
|||
1
stage0/src/runtime/libuv.cpp
generated
1
stage0/src/runtime/libuv.cpp
generated
|
|
@ -20,6 +20,7 @@ extern "C" void initialize_libuv() {
|
|||
initialize_libuv_timer();
|
||||
initialize_libuv_tcp_socket();
|
||||
initialize_libuv_udp_socket();
|
||||
initialize_libuv_signal();
|
||||
initialize_libuv_loop();
|
||||
|
||||
lthread([]() { event_loop_run_loop(&global_ev); });
|
||||
|
|
|
|||
1
stage0/src/runtime/libuv.h
generated
1
stage0/src/runtime/libuv.h
generated
|
|
@ -11,6 +11,7 @@ Author: Markus Himmel, Sofia Rodrigues
|
|||
#include "runtime/uv/tcp.h"
|
||||
#include "runtime/uv/dns.h"
|
||||
#include "runtime/uv/udp.h"
|
||||
#include "runtime/uv/signal.h"
|
||||
#include "runtime/alloc.h"
|
||||
#include "runtime/io.h"
|
||||
#include "runtime/utf8.h"
|
||||
|
|
|
|||
240
stage0/src/runtime/uv/signal.cpp
generated
Normal file
240
stage0/src/runtime/uv/signal.cpp
generated
Normal file
|
|
@ -0,0 +1,240 @@
|
|||
/*
|
||||
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sofia Rodrigues
|
||||
*/
|
||||
#include "runtime/uv/signal.h"
|
||||
|
||||
namespace lean {
|
||||
#ifndef LEAN_EMSCRIPTEN
|
||||
|
||||
using namespace std;
|
||||
|
||||
// The finalizer of the `Signal`.
|
||||
void lean_uv_signal_finalizer(void* ptr) {
|
||||
lean_uv_signal_object * signal = (lean_uv_signal_object*) ptr;
|
||||
|
||||
if (signal->m_promise != NULL) {
|
||||
lean_dec(signal->m_promise);
|
||||
}
|
||||
|
||||
event_loop_lock(&global_ev);
|
||||
|
||||
uv_close((uv_handle_t*)signal->m_uv_signal, [](uv_handle_t* handle) {
|
||||
free(handle);
|
||||
});
|
||||
|
||||
event_loop_unlock(&global_ev);
|
||||
|
||||
free(signal);
|
||||
}
|
||||
|
||||
void initialize_libuv_signal() {
|
||||
g_uv_signal_external_class = lean_register_external_class(lean_uv_signal_finalizer, [](void* obj, lean_object* f) {
|
||||
if (((lean_uv_signal_object*)obj)->m_promise != NULL) {
|
||||
lean_inc(f);
|
||||
lean_apply_1(f, ((lean_uv_signal_object*)obj)->m_promise);
|
||||
}
|
||||
});
|
||||
}
|
||||
|
||||
static bool signal_promise_is_finished(lean_uv_signal_object * signal) {
|
||||
return lean_io_get_task_state_core((lean_object *)lean_to_promise(signal->m_promise)->m_result) == 2;
|
||||
}
|
||||
|
||||
void handle_signal_event(uv_signal_t* handle, int signum) {
|
||||
lean_object * obj = (lean_object*)handle->data;
|
||||
lean_uv_signal_object * signal = lean_to_uv_signal(obj);
|
||||
|
||||
lean_assert(signal->m_state == SIGNAL_STATE_RUNNING);
|
||||
lean_assert(signal->m_promise != NULL);
|
||||
|
||||
if (signal->m_repeating) {
|
||||
if (!signal_promise_is_finished(signal)) {
|
||||
lean_object* res = lean_io_promise_resolve(lean_box(signum), signal->m_promise, lean_io_mk_world());
|
||||
lean_dec(res);
|
||||
}
|
||||
} else {
|
||||
lean_assert(!signal_promise_is_finished(signal));
|
||||
uv_signal_stop(signal->m_uv_signal);
|
||||
signal->m_state = SIGNAL_STATE_FINISHED;
|
||||
|
||||
lean_object* res = lean_io_promise_resolve(lean_box(signum), signal->m_promise, lean_io_mk_world());
|
||||
lean_dec(res);
|
||||
|
||||
lean_dec(obj);
|
||||
}
|
||||
}
|
||||
|
||||
/* Std.Internal.UV.Signal.mk (signum : Int32) (repeating : Bool) : IO Signal */
|
||||
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating, obj_arg /* w */) {
|
||||
int signum = (int)(int32_t)signum_obj;
|
||||
|
||||
lean_uv_signal_object * signal = (lean_uv_signal_object*)malloc(sizeof(lean_uv_signal_object));
|
||||
signal->m_signum = signum;
|
||||
signal->m_repeating = repeating;
|
||||
signal->m_state = SIGNAL_STATE_INITIAL;
|
||||
signal->m_promise = NULL;
|
||||
|
||||
uv_signal_t * uv_signal = (uv_signal_t*)malloc(sizeof(uv_signal_t));
|
||||
|
||||
event_loop_lock(&global_ev);
|
||||
int result = uv_signal_init(global_ev.loop, uv_signal);
|
||||
event_loop_unlock(&global_ev);
|
||||
|
||||
if (result != 0) {
|
||||
free(uv_signal);
|
||||
free(signal);
|
||||
return lean_io_result_mk_error(lean_decode_uv_error(result, NULL));
|
||||
}
|
||||
|
||||
signal->m_uv_signal = uv_signal;
|
||||
|
||||
lean_object * obj = lean_uv_signal_new(signal);
|
||||
lean_mark_mt(obj);
|
||||
signal->m_uv_signal->data = obj;
|
||||
|
||||
return lean_io_result_mk_ok(obj);
|
||||
}
|
||||
|
||||
/* Std.Internal.UV.Signal.next (signal : @& Signal) : IO (IO.Promise Int) */
|
||||
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg obj, obj_arg /* w */ ) {
|
||||
lean_uv_signal_object * signal = lean_to_uv_signal(obj);
|
||||
|
||||
auto create_promise = []() {
|
||||
lean_object * prom_res = lean_io_promise_new(lean_io_mk_world());
|
||||
lean_object * promise = lean_ctor_get(prom_res, 0);
|
||||
lean_inc(promise);
|
||||
lean_dec(prom_res);
|
||||
|
||||
return promise;
|
||||
};
|
||||
|
||||
auto setup_signal = [create_promise, obj, signal]() {
|
||||
lean_assert(signal->m_promise == NULL);
|
||||
signal->m_promise = create_promise();
|
||||
signal->m_state = SIGNAL_STATE_RUNNING;
|
||||
|
||||
// The event loop must keep the signal alive for the duration of the run time.
|
||||
lean_inc(obj);
|
||||
|
||||
event_loop_lock(&global_ev);
|
||||
|
||||
int result;
|
||||
if (signal->m_repeating) {
|
||||
result = uv_signal_start(
|
||||
signal->m_uv_signal,
|
||||
handle_signal_event,
|
||||
signal->m_signum
|
||||
);
|
||||
} else {
|
||||
result = uv_signal_start_oneshot(
|
||||
signal->m_uv_signal,
|
||||
handle_signal_event,
|
||||
signal->m_signum
|
||||
);
|
||||
}
|
||||
|
||||
event_loop_unlock(&global_ev);
|
||||
|
||||
if (result != 0) {
|
||||
lean_dec(obj);
|
||||
return lean_io_result_mk_error(lean_decode_uv_error(result, NULL));
|
||||
} else {
|
||||
lean_inc(signal->m_promise);
|
||||
return lean_io_result_mk_ok(signal->m_promise);
|
||||
}
|
||||
};
|
||||
|
||||
if (signal->m_repeating) {
|
||||
switch (signal->m_state) {
|
||||
case SIGNAL_STATE_INITIAL:
|
||||
{
|
||||
return setup_signal();
|
||||
}
|
||||
case SIGNAL_STATE_RUNNING:
|
||||
{
|
||||
lean_assert(signal->m_promise != NULL);
|
||||
// 2 indicates finished
|
||||
if (signal_promise_is_finished(signal)) {
|
||||
lean_dec(signal->m_promise);
|
||||
signal->m_promise = create_promise();
|
||||
lean_inc(signal->m_promise);
|
||||
return lean_io_result_mk_ok(signal->m_promise);
|
||||
} else {
|
||||
lean_inc(signal->m_promise);
|
||||
return lean_io_result_mk_ok(signal->m_promise);
|
||||
}
|
||||
}
|
||||
case SIGNAL_STATE_FINISHED:
|
||||
{
|
||||
lean_assert(signal->m_promise != NULL);
|
||||
lean_inc(signal->m_promise);
|
||||
return lean_io_result_mk_ok(signal->m_promise);
|
||||
}
|
||||
}
|
||||
} else {
|
||||
if (signal->m_state == SIGNAL_STATE_INITIAL) {
|
||||
return setup_signal();
|
||||
} else {
|
||||
lean_assert(signal->m_promise != NULL);
|
||||
|
||||
lean_inc(signal->m_promise);
|
||||
return lean_io_result_mk_ok(signal->m_promise);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/* Std.Internal.UV.Signal.stop (signal : @& Signal) : IO Unit */
|
||||
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg obj, obj_arg /* w */) {
|
||||
lean_uv_signal_object * signal = lean_to_uv_signal(obj);
|
||||
|
||||
if (signal->m_state == SIGNAL_STATE_RUNNING) {
|
||||
lean_assert(signal->m_promise != NULL);
|
||||
|
||||
event_loop_lock(&global_ev);
|
||||
int result = uv_signal_stop(signal->m_uv_signal);
|
||||
event_loop_unlock(&global_ev);
|
||||
|
||||
signal->m_state = SIGNAL_STATE_FINISHED;
|
||||
|
||||
// The loop does not need to keep the signal alive anymore.
|
||||
lean_dec(obj);
|
||||
|
||||
if (result != 0) {
|
||||
return lean_io_result_mk_error(lean_decode_uv_error(result, NULL));
|
||||
} else {
|
||||
return lean_io_result_mk_ok(lean_box(0));
|
||||
}
|
||||
} else {
|
||||
return lean_io_result_mk_ok(lean_box(0));
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
#else
|
||||
|
||||
/* Std.Internal.UV.Signal.mk (signum : Int32) (repeating : Bool) : IO Signal */
|
||||
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating, obj_arg /* w */) {
|
||||
lean_always_assert(
|
||||
false && ("Please build a version of Lean4 with libuv to invoke this.")
|
||||
);
|
||||
}
|
||||
|
||||
/* Std.Internal.UV.Signal.next (signal : @& Signal) : IO (IO.Promise Int) */
|
||||
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg signal, obj_arg /* w */) {
|
||||
lean_always_assert(
|
||||
false && ("Please build a version of Lean4 with libuv to invoke this.")
|
||||
);
|
||||
}
|
||||
|
||||
/* Std.Internal.UV.Signal.stop (signal : @& Signal) : IO Unit */
|
||||
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg signal, obj_arg /* w */) {
|
||||
lean_always_assert(
|
||||
false && ("Please build a version of Lean4 with libuv to invoke this.")
|
||||
);
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
}
|
||||
55
stage0/src/runtime/uv/signal.h
generated
Normal file
55
stage0/src/runtime/uv/signal.h
generated
Normal file
|
|
@ -0,0 +1,55 @@
|
|||
/*
|
||||
Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Sofia Rodrigues
|
||||
*/
|
||||
#pragma once
|
||||
#include <lean/lean.h>
|
||||
#include "runtime/uv/event_loop.h"
|
||||
|
||||
#ifndef LEAN_EMSCRIPTEN
|
||||
#include <uv.h>
|
||||
#endif
|
||||
|
||||
namespace lean {
|
||||
|
||||
static lean_external_class * g_uv_signal_external_class = NULL;
|
||||
void initialize_libuv_signal();
|
||||
|
||||
#ifndef LEAN_EMSCRIPTEN
|
||||
using namespace std;
|
||||
|
||||
enum uv_signal_state {
|
||||
SIGNAL_STATE_INITIAL,
|
||||
SIGNAL_STATE_RUNNING,
|
||||
SIGNAL_STATE_FINISHED,
|
||||
};
|
||||
|
||||
// Structure for managing a single UV signal object, including promise handling, signal number, and
|
||||
// repeating behavior. The repeating behavior exists to "set" a handler and avoid it not getting signals
|
||||
// between the creation of oneshot signal handlers.
|
||||
typedef struct {
|
||||
uv_signal_t * m_uv_signal; // LibUV signal handle.
|
||||
lean_object * m_promise; // The associated promise for asynchronous results.
|
||||
int m_signum; // Signal number to watch for.
|
||||
bool m_repeating; // Flag indicating if the signal handler is repeating.
|
||||
uv_signal_state m_state; // The state of the signal. Beyond the API description on the Lean
|
||||
// side this state has the invariant:
|
||||
// `m_state != SIGNAL_STATE_INITIAL` -> `m_promise != NULL`
|
||||
} lean_uv_signal_object;
|
||||
|
||||
// =======================================
|
||||
// Signal object manipulation functions.
|
||||
static inline lean_object* lean_uv_signal_new(lean_uv_signal_object * s) { return lean_alloc_external(g_uv_signal_external_class, s); }
|
||||
static inline lean_uv_signal_object* lean_to_uv_signal(lean_object * o) { return (lean_uv_signal_object*)(lean_get_external_data(o)); }
|
||||
|
||||
#endif
|
||||
|
||||
// =======================================
|
||||
// Signal manipulation functions
|
||||
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating, obj_arg /* w */);
|
||||
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg signal, obj_arg /* w */);
|
||||
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg signal, obj_arg /* w */);
|
||||
|
||||
}
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
#include "util/options.h"
|
||||
// Please update stage0
|
||||
|
||||
namespace lean {
|
||||
options get_default_options() {
|
||||
options opts;
|
||||
|
|
|
|||
120
stage0/stdlib/Init/Tactics.c
generated
120
stage0/stdlib/Init/Tactics.c
generated
|
|
@ -580,6 +580,7 @@ static lean_object* l_Lean_Parser_Tactic_simpPre___closed__1;
|
|||
static lean_object* l_Lean_Parser_Tactic_locationHyp___closed__4;
|
||||
static lean_object* l_Lean_Parser_Tactic_rwRuleSeq___closed__7;
|
||||
static lean_object* l_Lean_Parser_Tactic_SolveByElim_erase___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Attr_method__specs__simp;
|
||||
static lean_object* l_Lean_Parser_Tactic_tacticNext___x3d_x3e_____closed__6;
|
||||
lean_object* l_Array_mkArray0(lean_object*);
|
||||
static lean_object* l_Lean_Parser_Tactic_tacDepIfThenElse___closed__11;
|
||||
|
|
@ -683,6 +684,7 @@ static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__L
|
|||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_dsimp;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticHaveI____;
|
||||
static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__bvDecideMacro__1___closed__0;
|
||||
static lean_object* l_Lean_Parser_Attr_method__specs__simp___closed__5;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticRefine__lift_x27____1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_Tactic_first___closed__8;
|
||||
static lean_object* l_Lean_Parser_Tactic_dsimp___closed__8;
|
||||
|
|
@ -893,6 +895,7 @@ static lean_object* l_Lean_Parser_Tactic_by_x3f___closed__1;
|
|||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__mexfalsoMacro__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_Tactic_valConfigItem___closed__26;
|
||||
static lean_object* l_Lean_Parser_Tactic_intro___closed__7;
|
||||
static lean_object* l_Lean_Parser_Attr_method__specs__simp___closed__0;
|
||||
static lean_object* l_Lean_Parser_Tactic_substEqs___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticSorry;
|
||||
static lean_object* l_Lean_Parser_Tactic_mleaveMacro___closed__3;
|
||||
|
|
@ -1507,6 +1510,7 @@ static lean_object* l_Lean_Parser_Tactic_SolveByElim_args___closed__4;
|
|||
static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticBv__omega__1___closed__3;
|
||||
static lean_object* l_Lean_Parser_Attr_normCastLabel___closed__1;
|
||||
static lean_object* l_Lean_Parser_Tactic_inductionAltLHS___closed__4;
|
||||
static lean_object* l_Lean_Parser_Attr_method__specs__simp___closed__6;
|
||||
static lean_object* l_Lean_Parser_Tactic_dsimpTraceArgsRest___closed__4;
|
||||
static lean_object* l_Lean_Parser_Tactic_simpAllTrace___closed__3;
|
||||
static lean_object* l_Lean_Parser_Tactic_negConfigItem___closed__3;
|
||||
|
|
@ -1567,6 +1571,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_injections;
|
|||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_tacticAssumption__mod__cast__;
|
||||
static lean_object* l_Lean_Parser_Tactic_case_x27___closed__5;
|
||||
static lean_object* l_Lean_Parser_Tactic_SolveByElim_using_____closed__3;
|
||||
static lean_object* l_Lean_Parser_Attr_method__specs__simp___closed__1;
|
||||
static lean_object* l_Lean_Parser_Tactic_inductionAltLHS___closed__14;
|
||||
static lean_object* l_Lean_Parser_Tactic_mintroMacro___closed__2;
|
||||
static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticAnd__intros__1___closed__4;
|
||||
|
|
@ -1611,6 +1616,7 @@ static lean_object* l_Lean_Parser_Tactic_intro___closed__3;
|
|||
static lean_object* l_Lean_Parser_Tactic_mcasesMacro___closed__2;
|
||||
static lean_object* l_Lean_Parser_Tactic_simpErase___closed__0;
|
||||
static lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticExfalso__1___closed__10;
|
||||
static lean_object* l_Lean_Parser_Attr_method__specs__simp___closed__2;
|
||||
static lean_object* l_Lean_Parser_Tactic_clearValueHyp___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__mrightMacro__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Attr_normCastLabel;
|
||||
|
|
@ -1887,6 +1893,7 @@ static lean_object* l_Lean_Parser_Tactic_intro___closed__9;
|
|||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic_config;
|
||||
static lean_object* l_Lean_Parser_Tactic_mvcgenMacro___closed__1;
|
||||
static lean_object* l_Lean_Parser_Tactic_tacIfThenElse___closed__9;
|
||||
static lean_object* l_Lean_Parser_Attr_method__specs__simp___closed__4;
|
||||
static lean_object* l___aux__Init__Tactics______macroRules__term_u2039___u203a__1___closed__2;
|
||||
static lean_object* l_Lean_Parser_Tactic_clearValue___closed__1;
|
||||
static lean_object* l_Lean_Parser_Tactic_induction___closed__14;
|
||||
|
|
@ -2011,6 +2018,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRul
|
|||
static lean_object* l_Lean_Parser_Tactic_withUnfoldingAll___closed__2;
|
||||
static lean_object* l_Lean_Parser_Tactic_generalize___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__by_x3f__1(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_Attr_method__specs__simp___closed__3;
|
||||
static lean_object* l_Lean_Parser_Tactic_injection___closed__6;
|
||||
static lean_object* l_Lean_Parser_Tactic_tacticSuffices_____closed__1;
|
||||
static lean_object* l_Lean_Parser_Tactic_locationType___closed__10;
|
||||
|
|
@ -30761,6 +30769,102 @@ x_1 = l_Lean_Parser_Attr_wf__preprocess___closed__6;
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Attr_method__specs__simp___closed__0() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string_unchecked("method_specs_simp", 17, 17);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Attr_method__specs__simp___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_1 = l_Lean_Parser_Attr_method__specs__simp___closed__0;
|
||||
x_2 = l_Lean_Parser_Attr_simp___closed__0;
|
||||
x_3 = l_Lean_Parser_Tactic_as__aux__lemma___closed__1;
|
||||
x_4 = l_Lean_Parser_Tactic_as__aux__lemma___closed__0;
|
||||
x_5 = l_Lean_Name_mkStr4(x_4, x_3, x_2, x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Attr_method__specs__simp___closed__2() {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = 0;
|
||||
x_2 = l_Lean_Parser_Attr_method__specs__simp___closed__0;
|
||||
x_3 = lean_alloc_ctor(6, 1, 1);
|
||||
lean_ctor_set(x_3, 0, x_2);
|
||||
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Attr_method__specs__simp___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Parser_Tactic_simpLemma___closed__3;
|
||||
x_2 = l_Lean_Parser_Attr_method__specs__simp___closed__2;
|
||||
x_3 = l_Lean_Parser_Tactic_as__aux__lemma___closed__6;
|
||||
x_4 = lean_alloc_ctor(2, 3, 0);
|
||||
lean_ctor_set(x_4, 0, x_3);
|
||||
lean_ctor_set(x_4, 1, x_2);
|
||||
lean_ctor_set(x_4, 2, x_1);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Attr_method__specs__simp___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Parser_Tactic_rwRule___closed__12;
|
||||
x_2 = l_Lean_Parser_Attr_method__specs__simp___closed__3;
|
||||
x_3 = l_Lean_Parser_Tactic_as__aux__lemma___closed__6;
|
||||
x_4 = lean_alloc_ctor(2, 3, 0);
|
||||
lean_ctor_set(x_4, 0, x_3);
|
||||
lean_ctor_set(x_4, 1, x_2);
|
||||
lean_ctor_set(x_4, 2, x_1);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Attr_method__specs__simp___closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Parser_Attr_simp___closed__8;
|
||||
x_2 = l_Lean_Parser_Attr_method__specs__simp___closed__4;
|
||||
x_3 = l_Lean_Parser_Tactic_as__aux__lemma___closed__6;
|
||||
x_4 = lean_alloc_ctor(2, 3, 0);
|
||||
lean_ctor_set(x_4, 0, x_3);
|
||||
lean_ctor_set(x_4, 1, x_2);
|
||||
lean_ctor_set(x_4, 2, x_1);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Attr_method__specs__simp___closed__6() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_Parser_Attr_method__specs__simp___closed__5;
|
||||
x_2 = lean_unsigned_to_nat(1022u);
|
||||
x_3 = l_Lean_Parser_Attr_method__specs__simp___closed__1;
|
||||
x_4 = lean_alloc_ctor(3, 3, 0);
|
||||
lean_ctor_set(x_4, 0, x_3);
|
||||
lean_ctor_set(x_4, 1, x_2);
|
||||
lean_ctor_set(x_4, 2, x_1);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Attr_method__specs__simp() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = l_Lean_Parser_Attr_method__specs__simp___closed__6;
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_Attr_normCastLabel___closed__0() {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -35708,6 +35812,22 @@ l_Lean_Parser_Attr_wf__preprocess___closed__6 = _init_l_Lean_Parser_Attr_wf__pre
|
|||
lean_mark_persistent(l_Lean_Parser_Attr_wf__preprocess___closed__6);
|
||||
l_Lean_Parser_Attr_wf__preprocess = _init_l_Lean_Parser_Attr_wf__preprocess();
|
||||
lean_mark_persistent(l_Lean_Parser_Attr_wf__preprocess);
|
||||
l_Lean_Parser_Attr_method__specs__simp___closed__0 = _init_l_Lean_Parser_Attr_method__specs__simp___closed__0();
|
||||
lean_mark_persistent(l_Lean_Parser_Attr_method__specs__simp___closed__0);
|
||||
l_Lean_Parser_Attr_method__specs__simp___closed__1 = _init_l_Lean_Parser_Attr_method__specs__simp___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_Attr_method__specs__simp___closed__1);
|
||||
l_Lean_Parser_Attr_method__specs__simp___closed__2 = _init_l_Lean_Parser_Attr_method__specs__simp___closed__2();
|
||||
lean_mark_persistent(l_Lean_Parser_Attr_method__specs__simp___closed__2);
|
||||
l_Lean_Parser_Attr_method__specs__simp___closed__3 = _init_l_Lean_Parser_Attr_method__specs__simp___closed__3();
|
||||
lean_mark_persistent(l_Lean_Parser_Attr_method__specs__simp___closed__3);
|
||||
l_Lean_Parser_Attr_method__specs__simp___closed__4 = _init_l_Lean_Parser_Attr_method__specs__simp___closed__4();
|
||||
lean_mark_persistent(l_Lean_Parser_Attr_method__specs__simp___closed__4);
|
||||
l_Lean_Parser_Attr_method__specs__simp___closed__5 = _init_l_Lean_Parser_Attr_method__specs__simp___closed__5();
|
||||
lean_mark_persistent(l_Lean_Parser_Attr_method__specs__simp___closed__5);
|
||||
l_Lean_Parser_Attr_method__specs__simp___closed__6 = _init_l_Lean_Parser_Attr_method__specs__simp___closed__6();
|
||||
lean_mark_persistent(l_Lean_Parser_Attr_method__specs__simp___closed__6);
|
||||
l_Lean_Parser_Attr_method__specs__simp = _init_l_Lean_Parser_Attr_method__specs__simp();
|
||||
lean_mark_persistent(l_Lean_Parser_Attr_method__specs__simp);
|
||||
l_Lean_Parser_Attr_normCastLabel___closed__0 = _init_l_Lean_Parser_Attr_normCastLabel___closed__0();
|
||||
lean_mark_persistent(l_Lean_Parser_Attr_normCastLabel___closed__0);
|
||||
l_Lean_Parser_Attr_normCastLabel___closed__1 = _init_l_Lean_Parser_Attr_normCastLabel___closed__1();
|
||||
|
|
|
|||
4
stage0/stdlib/Lean/DocString/Parser.c
generated
4
stage0/stdlib/Lean/DocString/Parser.c
generated
|
|
@ -166,7 +166,6 @@ static lean_object* l___private_Lean_DocString_Parser_0__Lean_Doc_Parser_code_no
|
|||
static lean_object* l_Lean_Doc_Parser_emph___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Doc_Parser_para___lam__2(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_String_quote(lean_object*);
|
||||
lean_object* l_Lean_Parser_strLitFnAux___redArg(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_DocString_Parser_0__Lean_Doc_Parser_arg_flag___lam__5___closed__2;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_DocString_Parser_0__Lean_Doc_Parser_arg_mkNamed___boxed(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_DocString_Parser_0__Lean_Doc_Parser_bol___closed__1;
|
||||
|
|
@ -554,6 +553,7 @@ LEAN_EXPORT lean_object* l_Lean_Doc_Parser_OrderedListType_ctorIdx___boxed(lean_
|
|||
lean_object* l_Lean_Parser_SyntaxStack_get_x21(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Doc_Parser_instReprBlockCtxt;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_DocString_Parser_0__Lean_Doc_Parser_blankLine___lam__2(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_strLitFnAux(lean_object*, uint8_t, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Doc_Parser_header___lam__5(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Doc_Parser_para___lam__0(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Doc_Parser_codeBlock___closed__0;
|
||||
|
|
@ -6080,7 +6080,7 @@ else
|
|||
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49;
|
||||
lean_inc(x_4);
|
||||
x_46 = l_Lean_Parser_ParserState_next_x27___redArg(x_2, x_1, x_4);
|
||||
x_47 = l_Lean_Parser_strLitFnAux___redArg(x_4, x_1, x_46);
|
||||
x_47 = l_Lean_Parser_strLitFnAux(x_4, x_5, x_1, x_46);
|
||||
x_48 = l_Lean_Doc_Parser_val___closed__9;
|
||||
x_49 = l_Lean_Parser_ParserState_mkNode(x_47, x_48, x_8);
|
||||
lean_dec(x_8);
|
||||
|
|
|
|||
2930
stage0/stdlib/Lean/Elab/Deriving/BEq.c
generated
2930
stage0/stdlib/Lean/Elab/Deriving/BEq.c
generated
File diff suppressed because it is too large
Load diff
305
stage0/stdlib/Lean/Elab/Deriving/DecEq.c
generated
305
stage0/stdlib/Lean/Elab/Deriving/DecEq.c
generated
|
|
@ -383,7 +383,7 @@ static lean_object* l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_D
|
|||
static lean_object* l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkMatchOld___closed__4;
|
||||
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_initFn___closed__13____x40_Lean_Elab_Deriving_DecEq_2689463041____hygCtx___hyg_2_;
|
||||
lean_object* l_Lean_Elab_Deriving_mkContext(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Deriving_mkContext(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_addMacroStack___at___Lean_throwError___at___Lean_throwErrorAt___at___Lean_throwUnknownIdentifierAt___at___Lean_throwUnknownConstantAt___at___Lean_throwUnknownConstant___at___Lean_getConstInfo___at___Lean_getConstInfoCtor___at_____private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkMatchOld_mkAlts_spec__0_spec__0_spec__0_spec__0_spec__0_spec__1_spec__1_spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_mkUnknownIdentifierMessage___at___Lean_throwUnknownIdentifierAt___at___Lean_throwUnknownConstantAt___at___Lean_throwUnknownConstant___at___Lean_getConstInfo___at___Lean_getConstInfoInduct___at_____private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkEnumOfNat_spec__0_spec__0_spec__0_spec__0_spec__0_spec__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqEnum___lam__0___closed__9;
|
||||
|
|
@ -14735,7 +14735,7 @@ return x_2;
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14;
|
||||
x_9 = lean_ctor_get(x_1, 0);
|
||||
lean_inc_ref(x_9);
|
||||
lean_dec_ref(x_1);
|
||||
|
|
@ -14744,6 +14744,7 @@ lean_inc(x_10);
|
|||
lean_dec_ref(x_9);
|
||||
x_11 = l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqHeader___closed__1;
|
||||
x_12 = l_Lean_Elab_Deriving_DecEq_initFn___closed__1____x40_Lean_Elab_Deriving_DecEq_1775403645____hygCtx___hyg_4_;
|
||||
x_13 = 1;
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
|
|
@ -14751,205 +14752,205 @@ lean_inc_ref(x_4);
|
|||
lean_inc(x_3);
|
||||
lean_inc_ref(x_2);
|
||||
lean_inc(x_10);
|
||||
x_13 = l_Lean_Elab_Deriving_mkContext(x_11, x_12, x_10, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
if (lean_obj_tag(x_13) == 0)
|
||||
x_14 = l_Lean_Elab_Deriving_mkContext(x_11, x_12, x_10, x_13, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
if (lean_obj_tag(x_14) == 0)
|
||||
{
|
||||
lean_object* x_14; lean_object* x_15; lean_object* x_16;
|
||||
x_14 = lean_ctor_get(x_13, 0);
|
||||
lean_inc(x_14);
|
||||
x_15 = lean_ctor_get(x_13, 1);
|
||||
lean_object* x_15; lean_object* x_16; lean_object* x_17;
|
||||
x_15 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_15);
|
||||
lean_dec_ref(x_13);
|
||||
x_16 = lean_ctor_get(x_14, 1);
|
||||
lean_inc(x_16);
|
||||
lean_dec_ref(x_14);
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc_ref(x_4);
|
||||
lean_inc(x_3);
|
||||
lean_inc_ref(x_2);
|
||||
lean_inc(x_14);
|
||||
x_16 = l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkAuxFunctions(x_14, x_2, x_3, x_4, x_5, x_6, x_7, x_15);
|
||||
if (lean_obj_tag(x_16) == 0)
|
||||
lean_inc(x_15);
|
||||
x_17 = l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkAuxFunctions(x_15, x_2, x_3, x_4, x_5, x_6, x_7, x_16);
|
||||
if (lean_obj_tag(x_17) == 0)
|
||||
{
|
||||
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21; lean_object* x_22;
|
||||
x_17 = lean_ctor_get(x_16, 0);
|
||||
lean_inc(x_17);
|
||||
x_18 = lean_ctor_get(x_16, 1);
|
||||
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23;
|
||||
x_18 = lean_ctor_get(x_17, 0);
|
||||
lean_inc(x_18);
|
||||
lean_dec_ref(x_16);
|
||||
x_19 = l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds___closed__0;
|
||||
x_20 = lean_array_push(x_19, x_10);
|
||||
x_21 = 0;
|
||||
x_19 = lean_ctor_get(x_17, 1);
|
||||
lean_inc(x_19);
|
||||
lean_dec_ref(x_17);
|
||||
x_20 = l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds___closed__0;
|
||||
x_21 = lean_array_push(x_20, x_10);
|
||||
x_22 = 0;
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc_ref(x_4);
|
||||
x_22 = l_Lean_Elab_Deriving_mkInstanceCmds(x_14, x_11, x_20, x_21, x_2, x_3, x_4, x_5, x_6, x_7, x_18);
|
||||
lean_dec_ref(x_20);
|
||||
if (lean_obj_tag(x_22) == 0)
|
||||
x_23 = l_Lean_Elab_Deriving_mkInstanceCmds(x_15, x_11, x_21, x_22, x_2, x_3, x_4, x_5, x_6, x_7, x_19);
|
||||
lean_dec_ref(x_21);
|
||||
if (lean_obj_tag(x_23) == 0)
|
||||
{
|
||||
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27;
|
||||
x_23 = lean_ctor_get(x_22, 0);
|
||||
lean_inc(x_23);
|
||||
x_24 = lean_ctor_get(x_22, 1);
|
||||
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; uint8_t x_28;
|
||||
x_24 = lean_ctor_get(x_23, 0);
|
||||
lean_inc(x_24);
|
||||
lean_dec_ref(x_22);
|
||||
x_25 = l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds___closed__1;
|
||||
x_26 = l_Lean_isTracingEnabledFor___at_____private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds_spec__0___redArg(x_25, x_6, x_24);
|
||||
x_27 = !lean_is_exclusive(x_26);
|
||||
if (x_27 == 0)
|
||||
x_25 = lean_ctor_get(x_23, 1);
|
||||
lean_inc(x_25);
|
||||
lean_dec_ref(x_23);
|
||||
x_26 = l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds___closed__1;
|
||||
x_27 = l_Lean_isTracingEnabledFor___at_____private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds_spec__0___redArg(x_26, x_6, x_25);
|
||||
x_28 = !lean_is_exclusive(x_27);
|
||||
if (x_28 == 0)
|
||||
{
|
||||
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; uint8_t x_32;
|
||||
x_28 = lean_ctor_get(x_26, 0);
|
||||
x_29 = lean_ctor_get(x_26, 1);
|
||||
x_30 = lean_array_push(x_19, x_17);
|
||||
x_31 = l_Array_append___redArg(x_30, x_23);
|
||||
lean_dec(x_23);
|
||||
x_32 = lean_unbox(x_28);
|
||||
lean_dec(x_28);
|
||||
if (x_32 == 0)
|
||||
lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33;
|
||||
x_29 = lean_ctor_get(x_27, 0);
|
||||
x_30 = lean_ctor_get(x_27, 1);
|
||||
x_31 = lean_array_push(x_20, x_18);
|
||||
x_32 = l_Array_append___redArg(x_31, x_24);
|
||||
lean_dec(x_24);
|
||||
x_33 = lean_unbox(x_29);
|
||||
lean_dec(x_29);
|
||||
if (x_33 == 0)
|
||||
{
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec_ref(x_4);
|
||||
lean_ctor_set(x_26, 0, x_31);
|
||||
return x_26;
|
||||
lean_ctor_set(x_27, 0, x_32);
|
||||
return x_27;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; uint8_t x_40;
|
||||
lean_free_object(x_26);
|
||||
x_33 = l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds___closed__3;
|
||||
lean_inc_ref(x_31);
|
||||
x_34 = lean_array_to_list(x_31);
|
||||
x_35 = lean_box(0);
|
||||
x_36 = l_List_mapTR_loop___at_____private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds_spec__1(x_34, x_35);
|
||||
x_37 = l_Lean_MessageData_ofList(x_36);
|
||||
x_38 = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(x_38, 0, x_33);
|
||||
lean_ctor_set(x_38, 1, x_37);
|
||||
x_39 = l_Lean_addTrace___at_____private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds_spec__2___redArg(x_25, x_38, x_4, x_5, x_6, x_7, x_29);
|
||||
lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; uint8_t x_41;
|
||||
lean_free_object(x_27);
|
||||
x_34 = l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds___closed__3;
|
||||
lean_inc_ref(x_32);
|
||||
x_35 = lean_array_to_list(x_32);
|
||||
x_36 = lean_box(0);
|
||||
x_37 = l_List_mapTR_loop___at_____private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds_spec__1(x_35, x_36);
|
||||
x_38 = l_Lean_MessageData_ofList(x_37);
|
||||
x_39 = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(x_39, 0, x_34);
|
||||
lean_ctor_set(x_39, 1, x_38);
|
||||
x_40 = l_Lean_addTrace___at_____private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds_spec__2___redArg(x_26, x_39, x_4, x_5, x_6, x_7, x_30);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec_ref(x_4);
|
||||
x_40 = !lean_is_exclusive(x_39);
|
||||
if (x_40 == 0)
|
||||
x_41 = !lean_is_exclusive(x_40);
|
||||
if (x_41 == 0)
|
||||
{
|
||||
lean_object* x_41;
|
||||
x_41 = lean_ctor_get(x_39, 0);
|
||||
lean_dec(x_41);
|
||||
lean_ctor_set(x_39, 0, x_31);
|
||||
return x_39;
|
||||
lean_object* x_42;
|
||||
x_42 = lean_ctor_get(x_40, 0);
|
||||
lean_dec(x_42);
|
||||
lean_ctor_set(x_40, 0, x_32);
|
||||
return x_40;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_42; lean_object* x_43;
|
||||
x_42 = lean_ctor_get(x_39, 1);
|
||||
lean_inc(x_42);
|
||||
lean_dec(x_39);
|
||||
x_43 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_43, 0, x_31);
|
||||
lean_ctor_set(x_43, 1, x_42);
|
||||
return x_43;
|
||||
lean_object* x_43; lean_object* x_44;
|
||||
x_43 = lean_ctor_get(x_40, 1);
|
||||
lean_inc(x_43);
|
||||
lean_dec(x_40);
|
||||
x_44 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_44, 0, x_32);
|
||||
lean_ctor_set(x_44, 1, x_43);
|
||||
return x_44;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; uint8_t x_48;
|
||||
x_44 = lean_ctor_get(x_26, 0);
|
||||
x_45 = lean_ctor_get(x_26, 1);
|
||||
lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; uint8_t x_49;
|
||||
x_45 = lean_ctor_get(x_27, 0);
|
||||
x_46 = lean_ctor_get(x_27, 1);
|
||||
lean_inc(x_46);
|
||||
lean_inc(x_45);
|
||||
lean_inc(x_44);
|
||||
lean_dec(x_26);
|
||||
x_46 = lean_array_push(x_19, x_17);
|
||||
x_47 = l_Array_append___redArg(x_46, x_23);
|
||||
lean_dec(x_23);
|
||||
x_48 = lean_unbox(x_44);
|
||||
lean_dec(x_44);
|
||||
if (x_48 == 0)
|
||||
lean_dec(x_27);
|
||||
x_47 = lean_array_push(x_20, x_18);
|
||||
x_48 = l_Array_append___redArg(x_47, x_24);
|
||||
lean_dec(x_24);
|
||||
x_49 = lean_unbox(x_45);
|
||||
lean_dec(x_45);
|
||||
if (x_49 == 0)
|
||||
{
|
||||
lean_object* x_49;
|
||||
lean_object* x_50;
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec_ref(x_4);
|
||||
x_49 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_49, 0, x_47);
|
||||
lean_ctor_set(x_49, 1, x_45);
|
||||
return x_49;
|
||||
x_50 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_50, 0, x_48);
|
||||
lean_ctor_set(x_50, 1, x_46);
|
||||
return x_50;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59;
|
||||
x_50 = l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds___closed__3;
|
||||
lean_inc_ref(x_47);
|
||||
x_51 = lean_array_to_list(x_47);
|
||||
x_52 = lean_box(0);
|
||||
x_53 = l_List_mapTR_loop___at_____private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds_spec__1(x_51, x_52);
|
||||
x_54 = l_Lean_MessageData_ofList(x_53);
|
||||
x_55 = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(x_55, 0, x_50);
|
||||
lean_ctor_set(x_55, 1, x_54);
|
||||
x_56 = l_Lean_addTrace___at_____private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds_spec__2___redArg(x_25, x_55, x_4, x_5, x_6, x_7, x_45);
|
||||
lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60;
|
||||
x_51 = l___private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds___closed__3;
|
||||
lean_inc_ref(x_48);
|
||||
x_52 = lean_array_to_list(x_48);
|
||||
x_53 = lean_box(0);
|
||||
x_54 = l_List_mapTR_loop___at_____private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds_spec__1(x_52, x_53);
|
||||
x_55 = l_Lean_MessageData_ofList(x_54);
|
||||
x_56 = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(x_56, 0, x_51);
|
||||
lean_ctor_set(x_56, 1, x_55);
|
||||
x_57 = l_Lean_addTrace___at_____private_Lean_Elab_Deriving_DecEq_0__Lean_Elab_Deriving_DecEq_mkDecEqCmds_spec__2___redArg(x_26, x_56, x_4, x_5, x_6, x_7, x_46);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec_ref(x_4);
|
||||
x_57 = lean_ctor_get(x_56, 1);
|
||||
lean_inc(x_57);
|
||||
if (lean_is_exclusive(x_56)) {
|
||||
lean_ctor_release(x_56, 0);
|
||||
lean_ctor_release(x_56, 1);
|
||||
x_58 = x_56;
|
||||
x_58 = lean_ctor_get(x_57, 1);
|
||||
lean_inc(x_58);
|
||||
if (lean_is_exclusive(x_57)) {
|
||||
lean_ctor_release(x_57, 0);
|
||||
lean_ctor_release(x_57, 1);
|
||||
x_59 = x_57;
|
||||
} else {
|
||||
lean_dec_ref(x_56);
|
||||
x_58 = lean_box(0);
|
||||
lean_dec_ref(x_57);
|
||||
x_59 = lean_box(0);
|
||||
}
|
||||
if (lean_is_scalar(x_58)) {
|
||||
x_59 = lean_alloc_ctor(0, 2, 0);
|
||||
if (lean_is_scalar(x_59)) {
|
||||
x_60 = lean_alloc_ctor(0, 2, 0);
|
||||
} else {
|
||||
x_59 = x_58;
|
||||
x_60 = x_59;
|
||||
}
|
||||
lean_ctor_set(x_59, 0, x_47);
|
||||
lean_ctor_set(x_59, 1, x_57);
|
||||
return x_59;
|
||||
lean_ctor_set(x_60, 0, x_48);
|
||||
lean_ctor_set(x_60, 1, x_58);
|
||||
return x_60;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_60;
|
||||
lean_dec(x_17);
|
||||
uint8_t x_61;
|
||||
lean_dec(x_18);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec_ref(x_4);
|
||||
x_60 = !lean_is_exclusive(x_22);
|
||||
if (x_60 == 0)
|
||||
x_61 = !lean_is_exclusive(x_23);
|
||||
if (x_61 == 0)
|
||||
{
|
||||
return x_22;
|
||||
return x_23;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_61; lean_object* x_62; lean_object* x_63;
|
||||
x_61 = lean_ctor_get(x_22, 0);
|
||||
x_62 = lean_ctor_get(x_22, 1);
|
||||
lean_object* x_62; lean_object* x_63; lean_object* x_64;
|
||||
x_62 = lean_ctor_get(x_23, 0);
|
||||
x_63 = lean_ctor_get(x_23, 1);
|
||||
lean_inc(x_63);
|
||||
lean_inc(x_62);
|
||||
lean_inc(x_61);
|
||||
lean_dec(x_22);
|
||||
x_63 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_63, 0, x_61);
|
||||
lean_ctor_set(x_63, 1, x_62);
|
||||
return x_63;
|
||||
lean_dec(x_23);
|
||||
x_64 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_64, 0, x_62);
|
||||
lean_ctor_set(x_64, 1, x_63);
|
||||
return x_64;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_64;
|
||||
lean_dec(x_14);
|
||||
uint8_t x_65;
|
||||
lean_dec(x_15);
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
|
|
@ -14957,29 +14958,29 @@ lean_dec(x_5);
|
|||
lean_dec_ref(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec_ref(x_2);
|
||||
x_64 = !lean_is_exclusive(x_16);
|
||||
if (x_64 == 0)
|
||||
x_65 = !lean_is_exclusive(x_17);
|
||||
if (x_65 == 0)
|
||||
{
|
||||
return x_16;
|
||||
return x_17;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_65; lean_object* x_66; lean_object* x_67;
|
||||
x_65 = lean_ctor_get(x_16, 0);
|
||||
x_66 = lean_ctor_get(x_16, 1);
|
||||
lean_object* x_66; lean_object* x_67; lean_object* x_68;
|
||||
x_66 = lean_ctor_get(x_17, 0);
|
||||
x_67 = lean_ctor_get(x_17, 1);
|
||||
lean_inc(x_67);
|
||||
lean_inc(x_66);
|
||||
lean_inc(x_65);
|
||||
lean_dec(x_16);
|
||||
x_67 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_67, 0, x_65);
|
||||
lean_ctor_set(x_67, 1, x_66);
|
||||
return x_67;
|
||||
lean_dec(x_17);
|
||||
x_68 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_68, 0, x_66);
|
||||
lean_ctor_set(x_68, 1, x_67);
|
||||
return x_68;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_68;
|
||||
uint8_t x_69;
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
|
|
@ -14987,23 +14988,23 @@ lean_dec(x_5);
|
|||
lean_dec_ref(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec_ref(x_2);
|
||||
x_68 = !lean_is_exclusive(x_13);
|
||||
if (x_68 == 0)
|
||||
x_69 = !lean_is_exclusive(x_14);
|
||||
if (x_69 == 0)
|
||||
{
|
||||
return x_13;
|
||||
return x_14;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_69; lean_object* x_70; lean_object* x_71;
|
||||
x_69 = lean_ctor_get(x_13, 0);
|
||||
x_70 = lean_ctor_get(x_13, 1);
|
||||
lean_object* x_70; lean_object* x_71; lean_object* x_72;
|
||||
x_70 = lean_ctor_get(x_14, 0);
|
||||
x_71 = lean_ctor_get(x_14, 1);
|
||||
lean_inc(x_71);
|
||||
lean_inc(x_70);
|
||||
lean_inc(x_69);
|
||||
lean_dec(x_13);
|
||||
x_71 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_71, 0, x_69);
|
||||
lean_ctor_set(x_71, 1, x_70);
|
||||
return x_71;
|
||||
lean_dec(x_14);
|
||||
x_72 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_72, 0, x_70);
|
||||
lean_ctor_set(x_72, 1, x_71);
|
||||
return x_72;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
146
stage0/stdlib/Lean/Elab/Deriving/FromToJson.c
generated
146
stage0/stdlib/Lean/Elab/Deriving/FromToJson.c
generated
|
|
@ -357,7 +357,7 @@ static lean_object* l_Lean_mkUnknownIdentifierMessage___at___Lean_throwUnknownId
|
|||
static lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonAuxFunction___lam__0___closed__10;
|
||||
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_addMacroStack___at___Lean_throwError___at___Lean_throwErrorAt___at___Lean_throwUnknownIdentifierAt___at___Lean_throwUnknownConstantAt___at___Lean_throwUnknownConstant___at___Lean_getConstInfo___at___Lean_getConstInfoCtor___at_____private_Lean_Elab_Deriving_FromToJson_0__Lean_Elab_Deriving_FromToJson_mkToJsonBodyForInduct_mkAlts_spec__0_spec__0_spec__0_spec__0_spec__0_spec__1_spec__1_spec__2___redArg___closed__1;
|
||||
lean_object* l_Lean_Elab_Deriving_mkContext(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Deriving_mkContext(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Deriving_FromToJson_mkJsonField___closed__0;
|
||||
LEAN_EXPORT lean_object* l_Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Elab_Deriving_FromToJson_0__Lean_Elab_Deriving_FromToJson_mkToJsonBodyForInduct_mkAlts_spec__14___boxed(lean_object**);
|
||||
LEAN_EXPORT lean_object* l_Lean_isInductive___at___Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler_spec__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -17731,9 +17731,10 @@ return x_2;
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Deriving_FromToJson_0__Lean_Elab_Deriving_FromToJson_mkToJsonInstance(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11;
|
||||
lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12;
|
||||
x_9 = l_Lean_Elab_Deriving_FromToJson_mkToJsonHeader___closed__2;
|
||||
x_10 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at___Lean_Elab_Deriving_FromToJson_mkToJsonBodyForStruct_spec__0___redArg___closed__32;
|
||||
x_11 = 1;
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
|
|
@ -17741,40 +17742,39 @@ lean_inc_ref(x_4);
|
|||
lean_inc(x_3);
|
||||
lean_inc_ref(x_2);
|
||||
lean_inc(x_1);
|
||||
x_11 = l_Lean_Elab_Deriving_mkContext(x_9, x_10, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
if (lean_obj_tag(x_11) == 0)
|
||||
x_12 = l_Lean_Elab_Deriving_mkContext(x_9, x_10, x_1, x_11, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
if (lean_obj_tag(x_12) == 0)
|
||||
{
|
||||
lean_object* x_12; lean_object* x_13; lean_object* x_14;
|
||||
x_12 = lean_ctor_get(x_11, 0);
|
||||
lean_inc(x_12);
|
||||
x_13 = lean_ctor_get(x_11, 1);
|
||||
lean_object* x_13; lean_object* x_14; lean_object* x_15;
|
||||
x_13 = lean_ctor_get(x_12, 0);
|
||||
lean_inc(x_13);
|
||||
lean_dec_ref(x_11);
|
||||
x_14 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_14);
|
||||
lean_dec_ref(x_12);
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc_ref(x_4);
|
||||
lean_inc(x_3);
|
||||
lean_inc_ref(x_2);
|
||||
lean_inc(x_12);
|
||||
x_14 = l_Lean_Elab_Deriving_FromToJson_mkToJsonMutualBlock(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_13);
|
||||
if (lean_obj_tag(x_14) == 0)
|
||||
lean_inc(x_13);
|
||||
x_15 = l_Lean_Elab_Deriving_FromToJson_mkToJsonMutualBlock(x_13, x_2, x_3, x_4, x_5, x_6, x_7, x_14);
|
||||
if (lean_obj_tag(x_15) == 0)
|
||||
{
|
||||
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19; lean_object* x_20;
|
||||
x_15 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_15);
|
||||
x_16 = lean_ctor_get(x_14, 1);
|
||||
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
|
||||
x_16 = lean_ctor_get(x_15, 0);
|
||||
lean_inc(x_16);
|
||||
lean_dec_ref(x_14);
|
||||
x_17 = l___private_Lean_Elab_Deriving_FromToJson_0__Lean_Elab_Deriving_FromToJson_mkToJsonInstance___closed__0;
|
||||
x_18 = lean_array_push(x_17, x_1);
|
||||
x_19 = 1;
|
||||
x_17 = lean_ctor_get(x_15, 1);
|
||||
lean_inc(x_17);
|
||||
lean_dec_ref(x_15);
|
||||
x_18 = l___private_Lean_Elab_Deriving_FromToJson_0__Lean_Elab_Deriving_FromToJson_mkToJsonInstance___closed__0;
|
||||
x_19 = lean_array_push(x_18, x_1);
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc_ref(x_4);
|
||||
x_20 = l_Lean_Elab_Deriving_mkInstanceCmds(x_12, x_9, x_18, x_19, x_2, x_3, x_4, x_5, x_6, x_7, x_16);
|
||||
lean_dec_ref(x_18);
|
||||
x_20 = l_Lean_Elab_Deriving_mkInstanceCmds(x_13, x_9, x_19, x_11, x_2, x_3, x_4, x_5, x_6, x_7, x_17);
|
||||
lean_dec_ref(x_19);
|
||||
if (lean_obj_tag(x_20) == 0)
|
||||
{
|
||||
uint8_t x_21;
|
||||
|
|
@ -17792,7 +17792,7 @@ if (x_26 == 0)
|
|||
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31;
|
||||
x_27 = lean_ctor_get(x_25, 0);
|
||||
x_28 = lean_ctor_get(x_25, 1);
|
||||
x_29 = lean_array_push(x_17, x_15);
|
||||
x_29 = lean_array_push(x_18, x_16);
|
||||
x_30 = l_Array_append___redArg(x_29, x_22);
|
||||
lean_dec(x_22);
|
||||
x_31 = lean_unbox(x_27);
|
||||
|
|
@ -17855,7 +17855,7 @@ x_43 = lean_ctor_get(x_25, 1);
|
|||
lean_inc(x_43);
|
||||
lean_inc(x_42);
|
||||
lean_dec(x_25);
|
||||
x_44 = lean_array_push(x_17, x_15);
|
||||
x_44 = lean_array_push(x_18, x_16);
|
||||
x_45 = l_Array_append___redArg(x_44, x_22);
|
||||
lean_dec(x_22);
|
||||
x_46 = lean_unbox(x_42);
|
||||
|
|
@ -17933,7 +17933,7 @@ if (lean_is_exclusive(x_60)) {
|
|||
lean_dec_ref(x_60);
|
||||
x_63 = lean_box(0);
|
||||
}
|
||||
x_64 = lean_array_push(x_17, x_15);
|
||||
x_64 = lean_array_push(x_18, x_16);
|
||||
x_65 = l_Array_append___redArg(x_64, x_57);
|
||||
lean_dec(x_57);
|
||||
x_66 = lean_unbox(x_61);
|
||||
|
|
@ -17995,7 +17995,7 @@ return x_77;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_dec(x_15);
|
||||
lean_dec(x_16);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
|
|
@ -18006,7 +18006,7 @@ return x_20;
|
|||
else
|
||||
{
|
||||
uint8_t x_78;
|
||||
lean_dec(x_12);
|
||||
lean_dec(x_13);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
|
|
@ -18014,19 +18014,19 @@ lean_dec_ref(x_4);
|
|||
lean_dec(x_3);
|
||||
lean_dec_ref(x_2);
|
||||
lean_dec(x_1);
|
||||
x_78 = !lean_is_exclusive(x_14);
|
||||
x_78 = !lean_is_exclusive(x_15);
|
||||
if (x_78 == 0)
|
||||
{
|
||||
return x_14;
|
||||
return x_15;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_79; lean_object* x_80; lean_object* x_81;
|
||||
x_79 = lean_ctor_get(x_14, 0);
|
||||
x_80 = lean_ctor_get(x_14, 1);
|
||||
x_79 = lean_ctor_get(x_15, 0);
|
||||
x_80 = lean_ctor_get(x_15, 1);
|
||||
lean_inc(x_80);
|
||||
lean_inc(x_79);
|
||||
lean_dec(x_14);
|
||||
lean_dec(x_15);
|
||||
x_81 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_81, 0, x_79);
|
||||
lean_ctor_set(x_81, 1, x_80);
|
||||
|
|
@ -18044,19 +18044,19 @@ lean_dec_ref(x_4);
|
|||
lean_dec(x_3);
|
||||
lean_dec_ref(x_2);
|
||||
lean_dec(x_1);
|
||||
x_82 = !lean_is_exclusive(x_11);
|
||||
x_82 = !lean_is_exclusive(x_12);
|
||||
if (x_82 == 0)
|
||||
{
|
||||
return x_11;
|
||||
return x_12;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_83; lean_object* x_84; lean_object* x_85;
|
||||
x_83 = lean_ctor_get(x_11, 0);
|
||||
x_84 = lean_ctor_get(x_11, 1);
|
||||
x_83 = lean_ctor_get(x_12, 0);
|
||||
x_84 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_84);
|
||||
lean_inc(x_83);
|
||||
lean_dec(x_11);
|
||||
lean_dec(x_12);
|
||||
x_85 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_85, 0, x_83);
|
||||
lean_ctor_set(x_85, 1, x_84);
|
||||
|
|
@ -18136,9 +18136,10 @@ return x_4;
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Deriving_FromToJson_0__Lean_Elab_Deriving_FromToJson_mkFromJsonInstance(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11;
|
||||
lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12;
|
||||
x_9 = l_Lean_Elab_Deriving_FromToJson_mkFromJsonHeader___closed__1;
|
||||
x_10 = l___private_Lean_Elab_Deriving_FromToJson_0__Lean_Elab_Deriving_FromToJson_mkFromJsonInstance___closed__0;
|
||||
x_11 = 1;
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
|
|
@ -18146,40 +18147,39 @@ lean_inc_ref(x_4);
|
|||
lean_inc(x_3);
|
||||
lean_inc_ref(x_2);
|
||||
lean_inc(x_1);
|
||||
x_11 = l_Lean_Elab_Deriving_mkContext(x_9, x_10, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
if (lean_obj_tag(x_11) == 0)
|
||||
x_12 = l_Lean_Elab_Deriving_mkContext(x_9, x_10, x_1, x_11, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
if (lean_obj_tag(x_12) == 0)
|
||||
{
|
||||
lean_object* x_12; lean_object* x_13; lean_object* x_14;
|
||||
x_12 = lean_ctor_get(x_11, 0);
|
||||
lean_inc(x_12);
|
||||
x_13 = lean_ctor_get(x_11, 1);
|
||||
lean_object* x_13; lean_object* x_14; lean_object* x_15;
|
||||
x_13 = lean_ctor_get(x_12, 0);
|
||||
lean_inc(x_13);
|
||||
lean_dec_ref(x_11);
|
||||
x_14 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_14);
|
||||
lean_dec_ref(x_12);
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc_ref(x_4);
|
||||
lean_inc(x_3);
|
||||
lean_inc_ref(x_2);
|
||||
lean_inc(x_12);
|
||||
x_14 = l_Lean_Elab_Deriving_FromToJson_mkFromJsonMutualBlock(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_13);
|
||||
if (lean_obj_tag(x_14) == 0)
|
||||
lean_inc(x_13);
|
||||
x_15 = l_Lean_Elab_Deriving_FromToJson_mkFromJsonMutualBlock(x_13, x_2, x_3, x_4, x_5, x_6, x_7, x_14);
|
||||
if (lean_obj_tag(x_15) == 0)
|
||||
{
|
||||
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19; lean_object* x_20;
|
||||
x_15 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_15);
|
||||
x_16 = lean_ctor_get(x_14, 1);
|
||||
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
|
||||
x_16 = lean_ctor_get(x_15, 0);
|
||||
lean_inc(x_16);
|
||||
lean_dec_ref(x_14);
|
||||
x_17 = l___private_Lean_Elab_Deriving_FromToJson_0__Lean_Elab_Deriving_FromToJson_mkToJsonInstance___closed__0;
|
||||
x_18 = lean_array_push(x_17, x_1);
|
||||
x_19 = 1;
|
||||
x_17 = lean_ctor_get(x_15, 1);
|
||||
lean_inc(x_17);
|
||||
lean_dec_ref(x_15);
|
||||
x_18 = l___private_Lean_Elab_Deriving_FromToJson_0__Lean_Elab_Deriving_FromToJson_mkToJsonInstance___closed__0;
|
||||
x_19 = lean_array_push(x_18, x_1);
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc_ref(x_4);
|
||||
x_20 = l_Lean_Elab_Deriving_mkInstanceCmds(x_12, x_9, x_18, x_19, x_2, x_3, x_4, x_5, x_6, x_7, x_16);
|
||||
lean_dec_ref(x_18);
|
||||
x_20 = l_Lean_Elab_Deriving_mkInstanceCmds(x_13, x_9, x_19, x_11, x_2, x_3, x_4, x_5, x_6, x_7, x_17);
|
||||
lean_dec_ref(x_19);
|
||||
if (lean_obj_tag(x_20) == 0)
|
||||
{
|
||||
uint8_t x_21;
|
||||
|
|
@ -18197,7 +18197,7 @@ if (x_26 == 0)
|
|||
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31;
|
||||
x_27 = lean_ctor_get(x_25, 0);
|
||||
x_28 = lean_ctor_get(x_25, 1);
|
||||
x_29 = lean_array_push(x_17, x_15);
|
||||
x_29 = lean_array_push(x_18, x_16);
|
||||
x_30 = l_Array_append___redArg(x_29, x_22);
|
||||
lean_dec(x_22);
|
||||
x_31 = lean_unbox(x_27);
|
||||
|
|
@ -18260,7 +18260,7 @@ x_43 = lean_ctor_get(x_25, 1);
|
|||
lean_inc(x_43);
|
||||
lean_inc(x_42);
|
||||
lean_dec(x_25);
|
||||
x_44 = lean_array_push(x_17, x_15);
|
||||
x_44 = lean_array_push(x_18, x_16);
|
||||
x_45 = l_Array_append___redArg(x_44, x_22);
|
||||
lean_dec(x_22);
|
||||
x_46 = lean_unbox(x_42);
|
||||
|
|
@ -18338,7 +18338,7 @@ if (lean_is_exclusive(x_60)) {
|
|||
lean_dec_ref(x_60);
|
||||
x_63 = lean_box(0);
|
||||
}
|
||||
x_64 = lean_array_push(x_17, x_15);
|
||||
x_64 = lean_array_push(x_18, x_16);
|
||||
x_65 = l_Array_append___redArg(x_64, x_57);
|
||||
lean_dec(x_57);
|
||||
x_66 = lean_unbox(x_61);
|
||||
|
|
@ -18400,7 +18400,7 @@ return x_77;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_dec(x_15);
|
||||
lean_dec(x_16);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
|
|
@ -18411,7 +18411,7 @@ return x_20;
|
|||
else
|
||||
{
|
||||
uint8_t x_78;
|
||||
lean_dec(x_12);
|
||||
lean_dec(x_13);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
|
|
@ -18419,19 +18419,19 @@ lean_dec_ref(x_4);
|
|||
lean_dec(x_3);
|
||||
lean_dec_ref(x_2);
|
||||
lean_dec(x_1);
|
||||
x_78 = !lean_is_exclusive(x_14);
|
||||
x_78 = !lean_is_exclusive(x_15);
|
||||
if (x_78 == 0)
|
||||
{
|
||||
return x_14;
|
||||
return x_15;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_79; lean_object* x_80; lean_object* x_81;
|
||||
x_79 = lean_ctor_get(x_14, 0);
|
||||
x_80 = lean_ctor_get(x_14, 1);
|
||||
x_79 = lean_ctor_get(x_15, 0);
|
||||
x_80 = lean_ctor_get(x_15, 1);
|
||||
lean_inc(x_80);
|
||||
lean_inc(x_79);
|
||||
lean_dec(x_14);
|
||||
lean_dec(x_15);
|
||||
x_81 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_81, 0, x_79);
|
||||
lean_ctor_set(x_81, 1, x_80);
|
||||
|
|
@ -18449,19 +18449,19 @@ lean_dec_ref(x_4);
|
|||
lean_dec(x_3);
|
||||
lean_dec_ref(x_2);
|
||||
lean_dec(x_1);
|
||||
x_82 = !lean_is_exclusive(x_11);
|
||||
x_82 = !lean_is_exclusive(x_12);
|
||||
if (x_82 == 0)
|
||||
{
|
||||
return x_11;
|
||||
return x_12;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_83; lean_object* x_84; lean_object* x_85;
|
||||
x_83 = lean_ctor_get(x_11, 0);
|
||||
x_84 = lean_ctor_get(x_11, 1);
|
||||
x_83 = lean_ctor_get(x_12, 0);
|
||||
x_84 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_84);
|
||||
lean_inc(x_83);
|
||||
lean_dec(x_11);
|
||||
lean_dec(x_12);
|
||||
x_85 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_85, 0, x_83);
|
||||
lean_ctor_set(x_85, 1, x_84);
|
||||
|
|
|
|||
72
stage0/stdlib/Lean/Elab/Deriving/Hashable.c
generated
72
stage0/stdlib/Lean/Elab/Deriving/Hashable.c
generated
|
|
@ -204,7 +204,7 @@ lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
|
|||
static lean_object* l_Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Elab_Deriving_Hashable_0__Lean_Elab_Deriving_Hashable_mkMatch_mkAlts_spec__13___redArg___closed__15;
|
||||
LEAN_EXPORT lean_object* l_Lean_withExporting___at___Lean_withoutExporting___at___Lean_Elab_Deriving_Hashable_mkHashableHandler_spec__4_spec__4___redArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Deriving_Hashable_mkAuxFunction___closed__31;
|
||||
lean_object* l_Lean_Elab_Deriving_mkContext(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Deriving_mkContext(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t lean_name_eq(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_withoutExporting___at___Lean_Elab_Deriving_Hashable_mkHashableHandler_spec__4___redArg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
|
||||
|
|
@ -7798,9 +7798,10 @@ return x_2;
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Deriving_Hashable_0__Lean_Elab_Deriving_Hashable_mkHashableInstanceCmds(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11;
|
||||
lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12;
|
||||
x_9 = l_Lean_Elab_Deriving_Hashable_mkHashableHeader___closed__1;
|
||||
x_10 = l_Std_PRange_RangeIterator_instIteratorLoop_loop___at_____private_Lean_Elab_Deriving_Hashable_0__Lean_Elab_Deriving_Hashable_mkMatch_mkAlts_spec__13___redArg___closed__40;
|
||||
x_11 = 1;
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
|
|
@ -7808,40 +7809,39 @@ lean_inc_ref(x_4);
|
|||
lean_inc(x_3);
|
||||
lean_inc_ref(x_2);
|
||||
lean_inc(x_1);
|
||||
x_11 = l_Lean_Elab_Deriving_mkContext(x_9, x_10, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
if (lean_obj_tag(x_11) == 0)
|
||||
x_12 = l_Lean_Elab_Deriving_mkContext(x_9, x_10, x_1, x_11, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
if (lean_obj_tag(x_12) == 0)
|
||||
{
|
||||
lean_object* x_12; lean_object* x_13; lean_object* x_14;
|
||||
x_12 = lean_ctor_get(x_11, 0);
|
||||
lean_inc(x_12);
|
||||
x_13 = lean_ctor_get(x_11, 1);
|
||||
lean_object* x_13; lean_object* x_14; lean_object* x_15;
|
||||
x_13 = lean_ctor_get(x_12, 0);
|
||||
lean_inc(x_13);
|
||||
lean_dec_ref(x_11);
|
||||
x_14 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_14);
|
||||
lean_dec_ref(x_12);
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc_ref(x_4);
|
||||
lean_inc(x_3);
|
||||
lean_inc_ref(x_2);
|
||||
lean_inc(x_12);
|
||||
x_14 = l_Lean_Elab_Deriving_Hashable_mkHashFuncs(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_13);
|
||||
if (lean_obj_tag(x_14) == 0)
|
||||
lean_inc(x_13);
|
||||
x_15 = l_Lean_Elab_Deriving_Hashable_mkHashFuncs(x_13, x_2, x_3, x_4, x_5, x_6, x_7, x_14);
|
||||
if (lean_obj_tag(x_15) == 0)
|
||||
{
|
||||
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19; lean_object* x_20;
|
||||
x_15 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_15);
|
||||
x_16 = lean_ctor_get(x_14, 1);
|
||||
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
|
||||
x_16 = lean_ctor_get(x_15, 0);
|
||||
lean_inc(x_16);
|
||||
lean_dec_ref(x_14);
|
||||
x_17 = l___private_Lean_Elab_Deriving_Hashable_0__Lean_Elab_Deriving_Hashable_mkHashableInstanceCmds___closed__0;
|
||||
x_18 = lean_array_push(x_17, x_1);
|
||||
x_19 = 1;
|
||||
x_17 = lean_ctor_get(x_15, 1);
|
||||
lean_inc(x_17);
|
||||
lean_dec_ref(x_15);
|
||||
x_18 = l___private_Lean_Elab_Deriving_Hashable_0__Lean_Elab_Deriving_Hashable_mkHashableInstanceCmds___closed__0;
|
||||
x_19 = lean_array_push(x_18, x_1);
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc_ref(x_4);
|
||||
x_20 = l_Lean_Elab_Deriving_mkInstanceCmds(x_12, x_9, x_18, x_19, x_2, x_3, x_4, x_5, x_6, x_7, x_16);
|
||||
lean_dec_ref(x_18);
|
||||
x_20 = l_Lean_Elab_Deriving_mkInstanceCmds(x_13, x_9, x_19, x_11, x_2, x_3, x_4, x_5, x_6, x_7, x_17);
|
||||
lean_dec_ref(x_19);
|
||||
if (lean_obj_tag(x_20) == 0)
|
||||
{
|
||||
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25;
|
||||
|
|
@ -7858,7 +7858,7 @@ if (x_25 == 0)
|
|||
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_24, 0);
|
||||
x_27 = lean_ctor_get(x_24, 1);
|
||||
x_28 = lean_array_push(x_17, x_15);
|
||||
x_28 = lean_array_push(x_18, x_16);
|
||||
x_29 = l_Array_append___redArg(x_28, x_21);
|
||||
lean_dec(x_21);
|
||||
x_30 = lean_unbox(x_26);
|
||||
|
|
@ -7920,7 +7920,7 @@ x_43 = lean_ctor_get(x_24, 1);
|
|||
lean_inc(x_43);
|
||||
lean_inc(x_42);
|
||||
lean_dec(x_24);
|
||||
x_44 = lean_array_push(x_17, x_15);
|
||||
x_44 = lean_array_push(x_18, x_16);
|
||||
x_45 = l_Array_append___redArg(x_44, x_21);
|
||||
lean_dec(x_21);
|
||||
x_46 = lean_unbox(x_42);
|
||||
|
|
@ -7978,7 +7978,7 @@ return x_57;
|
|||
else
|
||||
{
|
||||
uint8_t x_58;
|
||||
lean_dec(x_15);
|
||||
lean_dec(x_16);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
|
|
@ -8006,7 +8006,7 @@ return x_61;
|
|||
else
|
||||
{
|
||||
uint8_t x_62;
|
||||
lean_dec(x_12);
|
||||
lean_dec(x_13);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
|
|
@ -8014,19 +8014,19 @@ lean_dec_ref(x_4);
|
|||
lean_dec(x_3);
|
||||
lean_dec_ref(x_2);
|
||||
lean_dec(x_1);
|
||||
x_62 = !lean_is_exclusive(x_14);
|
||||
x_62 = !lean_is_exclusive(x_15);
|
||||
if (x_62 == 0)
|
||||
{
|
||||
return x_14;
|
||||
return x_15;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_63; lean_object* x_64; lean_object* x_65;
|
||||
x_63 = lean_ctor_get(x_14, 0);
|
||||
x_64 = lean_ctor_get(x_14, 1);
|
||||
x_63 = lean_ctor_get(x_15, 0);
|
||||
x_64 = lean_ctor_get(x_15, 1);
|
||||
lean_inc(x_64);
|
||||
lean_inc(x_63);
|
||||
lean_dec(x_14);
|
||||
lean_dec(x_15);
|
||||
x_65 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_65, 0, x_63);
|
||||
lean_ctor_set(x_65, 1, x_64);
|
||||
|
|
@ -8044,19 +8044,19 @@ lean_dec_ref(x_4);
|
|||
lean_dec(x_3);
|
||||
lean_dec_ref(x_2);
|
||||
lean_dec(x_1);
|
||||
x_66 = !lean_is_exclusive(x_11);
|
||||
x_66 = !lean_is_exclusive(x_12);
|
||||
if (x_66 == 0)
|
||||
{
|
||||
return x_11;
|
||||
return x_12;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_67; lean_object* x_68; lean_object* x_69;
|
||||
x_67 = lean_ctor_get(x_11, 0);
|
||||
x_68 = lean_ctor_get(x_11, 1);
|
||||
x_67 = lean_ctor_get(x_12, 0);
|
||||
x_68 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_68);
|
||||
lean_inc(x_67);
|
||||
lean_dec(x_11);
|
||||
lean_dec(x_12);
|
||||
x_69 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_69, 0, x_67);
|
||||
lean_ctor_set(x_69, 1, x_68);
|
||||
|
|
|
|||
1759
stage0/stdlib/Lean/Elab/Deriving/Inhabited.c
generated
1759
stage0/stdlib/Lean/Elab/Deriving/Inhabited.c
generated
File diff suppressed because it is too large
Load diff
1725
stage0/stdlib/Lean/Elab/Deriving/Ord.c
generated
1725
stage0/stdlib/Lean/Elab/Deriving/Ord.c
generated
File diff suppressed because it is too large
Load diff
70
stage0/stdlib/Lean/Elab/Deriving/Repr.c
generated
70
stage0/stdlib/Lean/Elab/Deriving/Repr.c
generated
|
|
@ -294,7 +294,7 @@ lean_object* l_Lean_PersistentArray_push___redArg(lean_object*, lean_object*);
|
|||
static lean_object* l___private_Lean_Elab_Deriving_Repr_0__Lean_Elab_Deriving_Repr_initFn___closed__9____x40_Lean_Elab_Deriving_Repr_1829928117____hygCtx___hyg_2_;
|
||||
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_List_forIn_x27_loop___at___List_forIn_x27_loop___at_____private_Lean_Elab_Deriving_Repr_0__Lean_Elab_Deriving_Repr_mkBodyForInduct_mkAlts_spec__3_spec__3___redArg___lam__1___closed__26;
|
||||
lean_object* l_Lean_Elab_Deriving_mkContext(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Deriving_mkContext(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Deriving_Repr_mkAuxFunction___closed__42;
|
||||
static lean_object* l_Lean_Elab_Deriving_Repr_mkBodyForInduct___closed__0;
|
||||
LEAN_EXPORT lean_object* l_Lean_throwUnknownIdentifierAt___at___Lean_throwUnknownConstantAt___at___Lean_throwUnknownConstant___at___Lean_getConstInfo___at___Lean_getConstInfoCtor___at___Lean_Elab_Deriving_Repr_mkBodyForStruct_spec__0_spec__0_spec__0_spec__0_spec__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -10292,9 +10292,10 @@ return x_2;
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Elab_Deriving_Repr_0__Lean_Elab_Deriving_Repr_mkReprInstanceCmd(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11;
|
||||
lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12;
|
||||
x_9 = l_Lean_Elab_Deriving_Repr_mkReprHeader___closed__1;
|
||||
x_10 = l_Std_PRange_RangeIterator_instIteratorLoop_loop___at___Lean_Elab_Deriving_Repr_mkBodyForStruct_spec__12___redArg___lam__1___closed__51;
|
||||
x_11 = 1;
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
|
|
@ -10302,39 +10303,38 @@ lean_inc_ref(x_4);
|
|||
lean_inc(x_3);
|
||||
lean_inc_ref(x_2);
|
||||
lean_inc(x_1);
|
||||
x_11 = l_Lean_Elab_Deriving_mkContext(x_9, x_10, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
if (lean_obj_tag(x_11) == 0)
|
||||
x_12 = l_Lean_Elab_Deriving_mkContext(x_9, x_10, x_1, x_11, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
if (lean_obj_tag(x_12) == 0)
|
||||
{
|
||||
lean_object* x_12; lean_object* x_13; lean_object* x_14;
|
||||
x_12 = lean_ctor_get(x_11, 0);
|
||||
lean_inc(x_12);
|
||||
x_13 = lean_ctor_get(x_11, 1);
|
||||
lean_object* x_13; lean_object* x_14; lean_object* x_15;
|
||||
x_13 = lean_ctor_get(x_12, 0);
|
||||
lean_inc(x_13);
|
||||
lean_dec_ref(x_11);
|
||||
x_14 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_14);
|
||||
lean_dec_ref(x_12);
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc_ref(x_4);
|
||||
lean_inc(x_3);
|
||||
lean_inc_ref(x_2);
|
||||
x_14 = l_Lean_Elab_Deriving_Repr_mkMutualBlock(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_13);
|
||||
if (lean_obj_tag(x_14) == 0)
|
||||
x_15 = l_Lean_Elab_Deriving_Repr_mkMutualBlock(x_13, x_2, x_3, x_4, x_5, x_6, x_7, x_14);
|
||||
if (lean_obj_tag(x_15) == 0)
|
||||
{
|
||||
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19; lean_object* x_20;
|
||||
x_15 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_15);
|
||||
x_16 = lean_ctor_get(x_14, 1);
|
||||
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
|
||||
x_16 = lean_ctor_get(x_15, 0);
|
||||
lean_inc(x_16);
|
||||
lean_dec_ref(x_14);
|
||||
x_17 = l___private_Lean_Elab_Deriving_Repr_0__Lean_Elab_Deriving_Repr_mkReprInstanceCmd___closed__0;
|
||||
x_18 = lean_array_push(x_17, x_1);
|
||||
x_19 = 1;
|
||||
x_17 = lean_ctor_get(x_15, 1);
|
||||
lean_inc(x_17);
|
||||
lean_dec_ref(x_15);
|
||||
x_18 = l___private_Lean_Elab_Deriving_Repr_0__Lean_Elab_Deriving_Repr_mkReprInstanceCmd___closed__0;
|
||||
x_19 = lean_array_push(x_18, x_1);
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc_ref(x_4);
|
||||
x_20 = l_Lean_Elab_Deriving_mkInstanceCmds(x_12, x_9, x_18, x_19, x_2, x_3, x_4, x_5, x_6, x_7, x_16);
|
||||
lean_dec_ref(x_18);
|
||||
x_20 = l_Lean_Elab_Deriving_mkInstanceCmds(x_13, x_9, x_19, x_11, x_2, x_3, x_4, x_5, x_6, x_7, x_17);
|
||||
lean_dec_ref(x_19);
|
||||
if (lean_obj_tag(x_20) == 0)
|
||||
{
|
||||
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25;
|
||||
|
|
@ -10351,7 +10351,7 @@ if (x_25 == 0)
|
|||
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_24, 0);
|
||||
x_27 = lean_ctor_get(x_24, 1);
|
||||
x_28 = lean_array_push(x_17, x_15);
|
||||
x_28 = lean_array_push(x_18, x_16);
|
||||
x_29 = l_Array_append___redArg(x_28, x_21);
|
||||
lean_dec(x_21);
|
||||
x_30 = lean_unbox(x_26);
|
||||
|
|
@ -10413,7 +10413,7 @@ x_43 = lean_ctor_get(x_24, 1);
|
|||
lean_inc(x_43);
|
||||
lean_inc(x_42);
|
||||
lean_dec(x_24);
|
||||
x_44 = lean_array_push(x_17, x_15);
|
||||
x_44 = lean_array_push(x_18, x_16);
|
||||
x_45 = l_Array_append___redArg(x_44, x_21);
|
||||
lean_dec(x_21);
|
||||
x_46 = lean_unbox(x_42);
|
||||
|
|
@ -10471,7 +10471,7 @@ return x_57;
|
|||
else
|
||||
{
|
||||
uint8_t x_58;
|
||||
lean_dec(x_15);
|
||||
lean_dec(x_16);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
|
|
@ -10499,7 +10499,7 @@ return x_61;
|
|||
else
|
||||
{
|
||||
uint8_t x_62;
|
||||
lean_dec(x_12);
|
||||
lean_dec(x_13);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
|
|
@ -10507,19 +10507,19 @@ lean_dec_ref(x_4);
|
|||
lean_dec(x_3);
|
||||
lean_dec_ref(x_2);
|
||||
lean_dec(x_1);
|
||||
x_62 = !lean_is_exclusive(x_14);
|
||||
x_62 = !lean_is_exclusive(x_15);
|
||||
if (x_62 == 0)
|
||||
{
|
||||
return x_14;
|
||||
return x_15;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_63; lean_object* x_64; lean_object* x_65;
|
||||
x_63 = lean_ctor_get(x_14, 0);
|
||||
x_64 = lean_ctor_get(x_14, 1);
|
||||
x_63 = lean_ctor_get(x_15, 0);
|
||||
x_64 = lean_ctor_get(x_15, 1);
|
||||
lean_inc(x_64);
|
||||
lean_inc(x_63);
|
||||
lean_dec(x_14);
|
||||
lean_dec(x_15);
|
||||
x_65 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_65, 0, x_63);
|
||||
lean_ctor_set(x_65, 1, x_64);
|
||||
|
|
@ -10537,19 +10537,19 @@ lean_dec_ref(x_4);
|
|||
lean_dec(x_3);
|
||||
lean_dec_ref(x_2);
|
||||
lean_dec(x_1);
|
||||
x_66 = !lean_is_exclusive(x_11);
|
||||
x_66 = !lean_is_exclusive(x_12);
|
||||
if (x_66 == 0)
|
||||
{
|
||||
return x_11;
|
||||
return x_12;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_67; lean_object* x_68; lean_object* x_69;
|
||||
x_67 = lean_ctor_get(x_11, 0);
|
||||
x_68 = lean_ctor_get(x_11, 1);
|
||||
x_67 = lean_ctor_get(x_12, 0);
|
||||
x_68 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_68);
|
||||
lean_inc(x_67);
|
||||
lean_dec(x_11);
|
||||
lean_dec(x_12);
|
||||
x_69 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_69, 0, x_67);
|
||||
lean_ctor_set(x_69, 1, x_68);
|
||||
|
|
|
|||
301
stage0/stdlib/Lean/Elab/Deriving/ToExpr.c
generated
301
stage0/stdlib/Lean/Elab/Deriving/ToExpr.c
generated
|
|
@ -276,7 +276,7 @@ static lean_object* l___private_Init_Data_Array_Basic_0__Array_foldlMUnsafe_fold
|
|||
static lean_object* l_Lean_mkUnknownIdentifierMessage___at___Lean_throwUnknownIdentifierAt___at___Lean_throwUnknownConstantAt___at___Lean_throwUnknownConstant___at___Lean_getConstInfo___at___Lean_getConstInfoCtor___at_____private_Lean_Elab_Deriving_ToExpr_0__Lean_Elab_Deriving_ToExpr_mkToExprBody_mkAlts_spec__1_spec__1_spec__1_spec__1_spec__1_spec__1___closed__18;
|
||||
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_Deriving_ToExpr_mkToExprBody___closed__2;
|
||||
lean_object* l_Lean_Elab_Deriving_mkContext(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Deriving_mkContext(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_addTrace___at___Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds_spec__2___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Elab_Deriving_ToExpr_0__Lean_Elab_Deriving_ToExpr_initFn___closed__22____x40_Lean_Elab_Deriving_ToExpr_1932707508____hygCtx___hyg_2_;
|
||||
LEAN_EXPORT lean_object* l_Std_Iterators_IterM_DefaultConsumers_toArrayMapped_go___at___Lean_Elab_Deriving_ToExpr_mkLocalInstanceLetDecls_spec__0___redArg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -20149,12 +20149,13 @@ return x_2;
|
|||
LEAN_EXPORT lean_object* l_Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; lean_object* x_15;
|
||||
x_9 = lean_box(0);
|
||||
x_10 = l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___Lean_Elab_Deriving_ToExpr_mkLocalInstanceLetDecls_spec__1_spec__1___closed__14;
|
||||
x_11 = l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at___Lean_Elab_Deriving_ToExpr_mkToTypeExpr_spec__1___redArg___closed__0;
|
||||
x_12 = lean_unsigned_to_nat(0u);
|
||||
x_13 = lean_array_get_borrowed(x_9, x_1, x_12);
|
||||
x_14 = 1;
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
|
|
@ -20162,255 +20163,255 @@ lean_inc_ref(x_4);
|
|||
lean_inc(x_3);
|
||||
lean_inc_ref(x_2);
|
||||
lean_inc(x_13);
|
||||
x_14 = l_Lean_Elab_Deriving_mkContext(x_10, x_11, x_13, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
if (lean_obj_tag(x_14) == 0)
|
||||
x_15 = l_Lean_Elab_Deriving_mkContext(x_10, x_11, x_13, x_14, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
if (lean_obj_tag(x_15) == 0)
|
||||
{
|
||||
lean_object* x_15; lean_object* x_16; lean_object* x_17;
|
||||
x_15 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_15);
|
||||
x_16 = lean_ctor_get(x_14, 1);
|
||||
lean_object* x_16; lean_object* x_17; lean_object* x_18;
|
||||
x_16 = lean_ctor_get(x_15, 0);
|
||||
lean_inc(x_16);
|
||||
lean_dec_ref(x_14);
|
||||
x_17 = lean_ctor_get(x_15, 1);
|
||||
lean_inc(x_17);
|
||||
lean_dec_ref(x_15);
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc_ref(x_4);
|
||||
lean_inc(x_3);
|
||||
lean_inc_ref(x_2);
|
||||
lean_inc(x_15);
|
||||
x_17 = l_Lean_Elab_Deriving_ToExpr_mkAuxFunctions(x_15, x_2, x_3, x_4, x_5, x_6, x_7, x_16);
|
||||
if (lean_obj_tag(x_17) == 0)
|
||||
lean_inc(x_16);
|
||||
x_18 = l_Lean_Elab_Deriving_ToExpr_mkAuxFunctions(x_16, x_2, x_3, x_4, x_5, x_6, x_7, x_17);
|
||||
if (lean_obj_tag(x_18) == 0)
|
||||
{
|
||||
lean_object* x_18; lean_object* x_19; lean_object* x_20;
|
||||
x_18 = lean_ctor_get(x_17, 0);
|
||||
lean_inc(x_18);
|
||||
x_19 = lean_ctor_get(x_17, 1);
|
||||
lean_object* x_19; lean_object* x_20; lean_object* x_21;
|
||||
x_19 = lean_ctor_get(x_18, 0);
|
||||
lean_inc(x_19);
|
||||
lean_dec_ref(x_17);
|
||||
x_20 = lean_ctor_get(x_18, 1);
|
||||
lean_inc(x_20);
|
||||
lean_dec_ref(x_18);
|
||||
lean_inc(x_7);
|
||||
lean_inc_ref(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc_ref(x_4);
|
||||
x_20 = l_Lean_Elab_Deriving_ToExpr_mkInstanceCmds(x_15, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_19);
|
||||
if (lean_obj_tag(x_20) == 0)
|
||||
x_21 = l_Lean_Elab_Deriving_ToExpr_mkInstanceCmds(x_16, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_20);
|
||||
if (lean_obj_tag(x_21) == 0)
|
||||
{
|
||||
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25;
|
||||
x_21 = lean_ctor_get(x_20, 0);
|
||||
lean_inc(x_21);
|
||||
x_22 = lean_ctor_get(x_20, 1);
|
||||
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26;
|
||||
x_22 = lean_ctor_get(x_21, 0);
|
||||
lean_inc(x_22);
|
||||
lean_dec_ref(x_20);
|
||||
x_23 = l_Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds___closed__0;
|
||||
x_24 = l_Lean_isTracingEnabledFor___at___Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds_spec__0___redArg(x_23, x_6, x_22);
|
||||
x_25 = !lean_is_exclusive(x_24);
|
||||
if (x_25 == 0)
|
||||
x_23 = lean_ctor_get(x_21, 1);
|
||||
lean_inc(x_23);
|
||||
lean_dec_ref(x_21);
|
||||
x_24 = l_Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds___closed__0;
|
||||
x_25 = l_Lean_isTracingEnabledFor___at___Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds_spec__0___redArg(x_24, x_6, x_23);
|
||||
x_26 = !lean_is_exclusive(x_25);
|
||||
if (x_26 == 0)
|
||||
{
|
||||
lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31;
|
||||
x_26 = lean_ctor_get(x_24, 0);
|
||||
x_27 = lean_ctor_get(x_24, 1);
|
||||
x_28 = l_Lean_Elab_Deriving_ToExpr_mkAuxFunction___closed__1;
|
||||
x_29 = lean_array_push(x_28, x_18);
|
||||
x_30 = l_Array_append___redArg(x_29, x_21);
|
||||
lean_dec(x_21);
|
||||
x_31 = lean_unbox(x_26);
|
||||
lean_dec(x_26);
|
||||
if (x_31 == 0)
|
||||
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; uint8_t x_32;
|
||||
x_27 = lean_ctor_get(x_25, 0);
|
||||
x_28 = lean_ctor_get(x_25, 1);
|
||||
x_29 = l_Lean_Elab_Deriving_ToExpr_mkAuxFunction___closed__1;
|
||||
x_30 = lean_array_push(x_29, x_19);
|
||||
x_31 = l_Array_append___redArg(x_30, x_22);
|
||||
lean_dec(x_22);
|
||||
x_32 = lean_unbox(x_27);
|
||||
lean_dec(x_27);
|
||||
if (x_32 == 0)
|
||||
{
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec_ref(x_4);
|
||||
lean_ctor_set(x_24, 0, x_30);
|
||||
return x_24;
|
||||
lean_ctor_set(x_25, 0, x_31);
|
||||
return x_25;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; uint8_t x_39;
|
||||
lean_free_object(x_24);
|
||||
x_32 = l_Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds___closed__2;
|
||||
lean_inc_ref(x_30);
|
||||
x_33 = lean_array_to_list(x_30);
|
||||
x_34 = lean_box(0);
|
||||
x_35 = l_List_mapTR_loop___at___Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds_spec__1(x_33, x_34);
|
||||
x_36 = l_Lean_MessageData_ofList(x_35);
|
||||
x_37 = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(x_37, 0, x_32);
|
||||
lean_ctor_set(x_37, 1, x_36);
|
||||
x_38 = l_Lean_addTrace___at___Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds_spec__2___redArg(x_23, x_37, x_4, x_5, x_6, x_7, x_27);
|
||||
lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; uint8_t x_40;
|
||||
lean_free_object(x_25);
|
||||
x_33 = l_Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds___closed__2;
|
||||
lean_inc_ref(x_31);
|
||||
x_34 = lean_array_to_list(x_31);
|
||||
x_35 = lean_box(0);
|
||||
x_36 = l_List_mapTR_loop___at___Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds_spec__1(x_34, x_35);
|
||||
x_37 = l_Lean_MessageData_ofList(x_36);
|
||||
x_38 = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(x_38, 0, x_33);
|
||||
lean_ctor_set(x_38, 1, x_37);
|
||||
x_39 = l_Lean_addTrace___at___Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds_spec__2___redArg(x_24, x_38, x_4, x_5, x_6, x_7, x_28);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec_ref(x_4);
|
||||
x_39 = !lean_is_exclusive(x_38);
|
||||
if (x_39 == 0)
|
||||
x_40 = !lean_is_exclusive(x_39);
|
||||
if (x_40 == 0)
|
||||
{
|
||||
lean_object* x_40;
|
||||
x_40 = lean_ctor_get(x_38, 0);
|
||||
lean_dec(x_40);
|
||||
lean_ctor_set(x_38, 0, x_30);
|
||||
return x_38;
|
||||
lean_object* x_41;
|
||||
x_41 = lean_ctor_get(x_39, 0);
|
||||
lean_dec(x_41);
|
||||
lean_ctor_set(x_39, 0, x_31);
|
||||
return x_39;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_41; lean_object* x_42;
|
||||
x_41 = lean_ctor_get(x_38, 1);
|
||||
lean_inc(x_41);
|
||||
lean_dec(x_38);
|
||||
x_42 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_42, 0, x_30);
|
||||
lean_ctor_set(x_42, 1, x_41);
|
||||
return x_42;
|
||||
lean_object* x_42; lean_object* x_43;
|
||||
x_42 = lean_ctor_get(x_39, 1);
|
||||
lean_inc(x_42);
|
||||
lean_dec(x_39);
|
||||
x_43 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_43, 0, x_31);
|
||||
lean_ctor_set(x_43, 1, x_42);
|
||||
return x_43;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; uint8_t x_48;
|
||||
x_43 = lean_ctor_get(x_24, 0);
|
||||
x_44 = lean_ctor_get(x_24, 1);
|
||||
lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; uint8_t x_49;
|
||||
x_44 = lean_ctor_get(x_25, 0);
|
||||
x_45 = lean_ctor_get(x_25, 1);
|
||||
lean_inc(x_45);
|
||||
lean_inc(x_44);
|
||||
lean_inc(x_43);
|
||||
lean_dec(x_24);
|
||||
x_45 = l_Lean_Elab_Deriving_ToExpr_mkAuxFunction___closed__1;
|
||||
x_46 = lean_array_push(x_45, x_18);
|
||||
x_47 = l_Array_append___redArg(x_46, x_21);
|
||||
lean_dec(x_21);
|
||||
x_48 = lean_unbox(x_43);
|
||||
lean_dec(x_43);
|
||||
if (x_48 == 0)
|
||||
lean_dec(x_25);
|
||||
x_46 = l_Lean_Elab_Deriving_ToExpr_mkAuxFunction___closed__1;
|
||||
x_47 = lean_array_push(x_46, x_19);
|
||||
x_48 = l_Array_append___redArg(x_47, x_22);
|
||||
lean_dec(x_22);
|
||||
x_49 = lean_unbox(x_44);
|
||||
lean_dec(x_44);
|
||||
if (x_49 == 0)
|
||||
{
|
||||
lean_object* x_49;
|
||||
lean_object* x_50;
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec_ref(x_4);
|
||||
x_49 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_49, 0, x_47);
|
||||
lean_ctor_set(x_49, 1, x_44);
|
||||
return x_49;
|
||||
x_50 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_50, 0, x_48);
|
||||
lean_ctor_set(x_50, 1, x_45);
|
||||
return x_50;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59;
|
||||
x_50 = l_Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds___closed__2;
|
||||
lean_inc_ref(x_47);
|
||||
x_51 = lean_array_to_list(x_47);
|
||||
x_52 = lean_box(0);
|
||||
x_53 = l_List_mapTR_loop___at___Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds_spec__1(x_51, x_52);
|
||||
x_54 = l_Lean_MessageData_ofList(x_53);
|
||||
x_55 = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(x_55, 0, x_50);
|
||||
lean_ctor_set(x_55, 1, x_54);
|
||||
x_56 = l_Lean_addTrace___at___Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds_spec__2___redArg(x_23, x_55, x_4, x_5, x_6, x_7, x_44);
|
||||
lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60;
|
||||
x_51 = l_Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds___closed__2;
|
||||
lean_inc_ref(x_48);
|
||||
x_52 = lean_array_to_list(x_48);
|
||||
x_53 = lean_box(0);
|
||||
x_54 = l_List_mapTR_loop___at___Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds_spec__1(x_52, x_53);
|
||||
x_55 = l_Lean_MessageData_ofList(x_54);
|
||||
x_56 = lean_alloc_ctor(7, 2, 0);
|
||||
lean_ctor_set(x_56, 0, x_51);
|
||||
lean_ctor_set(x_56, 1, x_55);
|
||||
x_57 = l_Lean_addTrace___at___Lean_Elab_Deriving_ToExpr_mkToExprInstanceCmds_spec__2___redArg(x_24, x_56, x_4, x_5, x_6, x_7, x_45);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec_ref(x_4);
|
||||
x_57 = lean_ctor_get(x_56, 1);
|
||||
lean_inc(x_57);
|
||||
if (lean_is_exclusive(x_56)) {
|
||||
lean_ctor_release(x_56, 0);
|
||||
lean_ctor_release(x_56, 1);
|
||||
x_58 = x_56;
|
||||
x_58 = lean_ctor_get(x_57, 1);
|
||||
lean_inc(x_58);
|
||||
if (lean_is_exclusive(x_57)) {
|
||||
lean_ctor_release(x_57, 0);
|
||||
lean_ctor_release(x_57, 1);
|
||||
x_59 = x_57;
|
||||
} else {
|
||||
lean_dec_ref(x_56);
|
||||
x_58 = lean_box(0);
|
||||
lean_dec_ref(x_57);
|
||||
x_59 = lean_box(0);
|
||||
}
|
||||
if (lean_is_scalar(x_58)) {
|
||||
x_59 = lean_alloc_ctor(0, 2, 0);
|
||||
if (lean_is_scalar(x_59)) {
|
||||
x_60 = lean_alloc_ctor(0, 2, 0);
|
||||
} else {
|
||||
x_59 = x_58;
|
||||
x_60 = x_59;
|
||||
}
|
||||
lean_ctor_set(x_59, 0, x_47);
|
||||
lean_ctor_set(x_59, 1, x_57);
|
||||
return x_59;
|
||||
lean_ctor_set(x_60, 0, x_48);
|
||||
lean_ctor_set(x_60, 1, x_58);
|
||||
return x_60;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_60;
|
||||
lean_dec(x_18);
|
||||
uint8_t x_61;
|
||||
lean_dec(x_19);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec_ref(x_4);
|
||||
x_60 = !lean_is_exclusive(x_20);
|
||||
if (x_60 == 0)
|
||||
x_61 = !lean_is_exclusive(x_21);
|
||||
if (x_61 == 0)
|
||||
{
|
||||
return x_20;
|
||||
return x_21;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_61; lean_object* x_62; lean_object* x_63;
|
||||
x_61 = lean_ctor_get(x_20, 0);
|
||||
x_62 = lean_ctor_get(x_20, 1);
|
||||
lean_object* x_62; lean_object* x_63; lean_object* x_64;
|
||||
x_62 = lean_ctor_get(x_21, 0);
|
||||
x_63 = lean_ctor_get(x_21, 1);
|
||||
lean_inc(x_63);
|
||||
lean_inc(x_62);
|
||||
lean_inc(x_61);
|
||||
lean_dec(x_20);
|
||||
x_63 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_63, 0, x_61);
|
||||
lean_ctor_set(x_63, 1, x_62);
|
||||
return x_63;
|
||||
lean_dec(x_21);
|
||||
x_64 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_64, 0, x_62);
|
||||
lean_ctor_set(x_64, 1, x_63);
|
||||
return x_64;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_64;
|
||||
lean_dec(x_15);
|
||||
uint8_t x_65;
|
||||
lean_dec(x_16);
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec_ref(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec_ref(x_2);
|
||||
x_64 = !lean_is_exclusive(x_17);
|
||||
if (x_64 == 0)
|
||||
x_65 = !lean_is_exclusive(x_18);
|
||||
if (x_65 == 0)
|
||||
{
|
||||
return x_17;
|
||||
return x_18;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_65; lean_object* x_66; lean_object* x_67;
|
||||
x_65 = lean_ctor_get(x_17, 0);
|
||||
x_66 = lean_ctor_get(x_17, 1);
|
||||
lean_object* x_66; lean_object* x_67; lean_object* x_68;
|
||||
x_66 = lean_ctor_get(x_18, 0);
|
||||
x_67 = lean_ctor_get(x_18, 1);
|
||||
lean_inc(x_67);
|
||||
lean_inc(x_66);
|
||||
lean_inc(x_65);
|
||||
lean_dec(x_17);
|
||||
x_67 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_67, 0, x_65);
|
||||
lean_ctor_set(x_67, 1, x_66);
|
||||
return x_67;
|
||||
lean_dec(x_18);
|
||||
x_68 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_68, 0, x_66);
|
||||
lean_ctor_set(x_68, 1, x_67);
|
||||
return x_68;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_68;
|
||||
uint8_t x_69;
|
||||
lean_dec(x_7);
|
||||
lean_dec_ref(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec_ref(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec_ref(x_2);
|
||||
x_68 = !lean_is_exclusive(x_14);
|
||||
if (x_68 == 0)
|
||||
x_69 = !lean_is_exclusive(x_15);
|
||||
if (x_69 == 0)
|
||||
{
|
||||
return x_14;
|
||||
return x_15;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_69; lean_object* x_70; lean_object* x_71;
|
||||
x_69 = lean_ctor_get(x_14, 0);
|
||||
x_70 = lean_ctor_get(x_14, 1);
|
||||
lean_object* x_70; lean_object* x_71; lean_object* x_72;
|
||||
x_70 = lean_ctor_get(x_15, 0);
|
||||
x_71 = lean_ctor_get(x_15, 1);
|
||||
lean_inc(x_71);
|
||||
lean_inc(x_70);
|
||||
lean_inc(x_69);
|
||||
lean_dec(x_14);
|
||||
x_71 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_71, 0, x_69);
|
||||
lean_ctor_set(x_71, 1, x_70);
|
||||
return x_71;
|
||||
lean_dec(x_15);
|
||||
x_72 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_72, 0, x_70);
|
||||
lean_ctor_set(x_72, 1, x_71);
|
||||
return x_72;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
930
stage0/stdlib/Lean/Elab/Deriving/Util.c
generated
930
stage0/stdlib/Lean/Elab/Deriving/Util.c
generated
File diff suppressed because it is too large
Load diff
4469
stage0/stdlib/Lean/Elab/MutualDef.c
generated
4469
stage0/stdlib/Lean/Elab/MutualDef.c
generated
File diff suppressed because it is too large
Load diff
6
stage0/stdlib/Lean/Meta.c
generated
6
stage0/stdlib/Lean/Meta.c
generated
|
|
@ -1,6 +1,6 @@
|
|||
// Lean compiler output
|
||||
// Module: Lean.Meta
|
||||
// Imports: Lean.Meta.Basic Lean.Meta.LevelDefEq Lean.Meta.WHNF Lean.Meta.InferType Lean.Meta.FunInfo Lean.Meta.ExprDefEq Lean.Meta.DecLevel Lean.Meta.DiscrTree Lean.Meta.Reduce Lean.Meta.Instances Lean.Meta.AbstractMVars Lean.Meta.SynthInstance Lean.Meta.AppBuilder Lean.Meta.Sorry Lean.Meta.Tactic Lean.Meta.KAbstract Lean.Meta.RecursorInfo Lean.Meta.GeneralizeTelescope Lean.Meta.Match Lean.Meta.ReduceEval Lean.Meta.Closure Lean.Meta.AbstractNestedProofs Lean.Meta.LetToHave Lean.Meta.ForEachExpr Lean.Meta.Transform Lean.Meta.PPGoal Lean.Meta.UnificationHint Lean.Meta.Inductive Lean.Meta.SizeOf Lean.Meta.IndPredBelow Lean.Meta.Coe Lean.Meta.CollectFVars Lean.Meta.GeneralizeVars Lean.Meta.Injective Lean.Meta.Structure Lean.Meta.Constructions Lean.Meta.CongrTheorems Lean.Meta.Eqns Lean.Meta.ExprLens Lean.Meta.ExprTraverse Lean.Meta.Eval Lean.Meta.CoeAttr Lean.Meta.Iterator Lean.Meta.LazyDiscrTree Lean.Meta.LitValues Lean.Meta.CheckTactic Lean.Meta.Canonicalizer Lean.Meta.Diagnostics Lean.Meta.BinderNameHint Lean.Meta.TryThis Lean.Meta.Hint
|
||||
// Imports: Lean.Meta.Basic Lean.Meta.LevelDefEq Lean.Meta.WHNF Lean.Meta.InferType Lean.Meta.FunInfo Lean.Meta.ExprDefEq Lean.Meta.DecLevel Lean.Meta.DiscrTree Lean.Meta.Reduce Lean.Meta.Instances Lean.Meta.AbstractMVars Lean.Meta.SynthInstance Lean.Meta.AppBuilder Lean.Meta.Sorry Lean.Meta.Tactic Lean.Meta.KAbstract Lean.Meta.RecursorInfo Lean.Meta.GeneralizeTelescope Lean.Meta.Match Lean.Meta.ReduceEval Lean.Meta.Closure Lean.Meta.AbstractNestedProofs Lean.Meta.LetToHave Lean.Meta.ForEachExpr Lean.Meta.Transform Lean.Meta.PPGoal Lean.Meta.UnificationHint Lean.Meta.Inductive Lean.Meta.SizeOf Lean.Meta.IndPredBelow Lean.Meta.Coe Lean.Meta.CollectFVars Lean.Meta.GeneralizeVars Lean.Meta.Injective Lean.Meta.Structure Lean.Meta.Constructions Lean.Meta.CongrTheorems Lean.Meta.Eqns Lean.Meta.ExprLens Lean.Meta.ExprTraverse Lean.Meta.Eval Lean.Meta.CoeAttr Lean.Meta.Iterator Lean.Meta.LazyDiscrTree Lean.Meta.LitValues Lean.Meta.CheckTactic Lean.Meta.Canonicalizer Lean.Meta.Diagnostics Lean.Meta.BinderNameHint Lean.Meta.TryThis Lean.Meta.Hint Lean.Meta.MethodSpecs
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
|
|
@ -64,6 +64,7 @@ lean_object* initialize_Lean_Meta_Diagnostics(uint8_t builtin, lean_object*);
|
|||
lean_object* initialize_Lean_Meta_BinderNameHint(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Lean_Meta_TryThis(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Lean_Meta_Hint(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Lean_Meta_MethodSpecs(uint8_t builtin, lean_object*);
|
||||
static bool _G_initialized = false;
|
||||
LEAN_EXPORT lean_object* initialize_Lean_Meta(uint8_t builtin, lean_object* w) {
|
||||
lean_object * res;
|
||||
|
|
@ -222,6 +223,9 @@ lean_dec_ref(res);
|
|||
res = initialize_Lean_Meta_Hint(builtin, lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Lean_Meta_MethodSpecs(builtin, lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
return lean_io_result_mk_ok(lean_box(0));
|
||||
}
|
||||
#ifdef __cplusplus
|
||||
|
|
|
|||
13202
stage0/stdlib/Lean/Meta/MethodSpecs.c
generated
Normal file
13202
stage0/stdlib/Lean/Meta/MethodSpecs.c
generated
Normal file
File diff suppressed because it is too large
Load diff
906
stage0/stdlib/Lean/Meta/Tactic/Grind/EMatchTheorem.c
generated
906
stage0/stdlib/Lean/Meta/Tactic/Grind/EMatchTheorem.c
generated
File diff suppressed because it is too large
Load diff
4926
stage0/stdlib/Lean/Meta/Tactic/Simp/Rewrite.c
generated
4926
stage0/stdlib/Lean/Meta/Tactic/Simp/Rewrite.c
generated
File diff suppressed because it is too large
Load diff
2304
stage0/stdlib/Lean/Meta/Tactic/Simp/SimpTheorems.c
generated
2304
stage0/stdlib/Lean/Meta/Tactic/Simp/SimpTheorems.c
generated
File diff suppressed because it is too large
Load diff
135
stage0/stdlib/Lean/Parser/Basic.c
generated
135
stage0/stdlib/Lean/Parser/Basic.c
generated
|
|
@ -83,6 +83,7 @@ static lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_nameLitAux___cl
|
|||
LEAN_EXPORT uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_identFnAux_parse___lam__0(uint32_t);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_LeadingIdentBehavior_toCtorIdx___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_errorAtSavedPos___regBuiltin_Lean_Parser_errorAtSavedPos_docString__1(lean_object*);
|
||||
static lean_object* l_Lean_Parser_strLitFnAux___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_dbgTraceStateFn___lam__0(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_instReprRecoveryContext_repr___redArg___closed__12;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_LeadingIdentBehavior_default_elim___redArg(lean_object*);
|
||||
|
|
@ -121,7 +122,6 @@ static lean_object* l_Lean_Parser_quotedCharFn___closed__0;
|
|||
lean_object* l_Lean_Parser_Error_toString(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_rawFn(lean_object*, uint8_t, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_antiquotNestedExpr___closed__7;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_strLitFnAux___redArg(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_recover_x27___regBuiltin_Lean_Parser_recover_x27_docString__1___closed__2;
|
||||
lean_object* l_Lean_Parser_adaptCacheableContextFn(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_andthenInfo(lean_object*, lean_object*);
|
||||
|
|
@ -182,6 +182,7 @@ LEAN_EXPORT lean_object* l_Lean_Syntax_forArgsM___redArg___boxed(lean_object*, l
|
|||
LEAN_EXPORT lean_object* l_Lean_Parser_isQuotableCharDefault___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_sepBy1Fn(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_andthenFn(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_strLitFnAux___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_mkAtomicInfo(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_longestMatchStep___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_ParserState_mkUnexpectedError(lean_object*, lean_object*, lean_object*, uint8_t);
|
||||
|
|
@ -207,6 +208,7 @@ static lean_object* l_Lean_Parser_mkAntiquot___closed__2;
|
|||
LEAN_EXPORT uint8_t l_Lean_Parser_instDecidableEqRecoveryContext_decEq(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_instReprRecoveryContext___closed__0;
|
||||
lean_object* l_Lean_Parser_ParserState_next_x27___redArg(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_strLitFnAux___closed__0;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_withAntiquotSuffixSplice___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_orelse(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_sepByInfo(lean_object*, lean_object*);
|
||||
|
|
@ -313,7 +315,6 @@ static lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_mkAntiquot___re
|
|||
LEAN_EXPORT lean_object* l_Lean_Parser_nonReservedSymbolInfo___boxed(lean_object*, lean_object*);
|
||||
size_t lean_usize_of_nat(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_LeadingIdentBehavior_both_elim(lean_object*, uint8_t, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_strLitFnAux___redArg___closed__0;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_instOrElseParserFn___lam__0(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_checkColGe___regBuiltin_Lean_Parser_checkColGe_docString__1___closed__0;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_checkTailWs___boxed(lean_object*);
|
||||
|
|
@ -493,7 +494,6 @@ LEAN_EXPORT lean_object* l_Lean_Parser_numLitFn(lean_object*, lean_object*);
|
|||
LEAN_EXPORT lean_object* l_Lean_Parser_withAntiquot(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_finishCommentBlock(uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_nodeInfo(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_strLitFnAux___redArg___closed__1;
|
||||
static lean_object* l_List_foldl___at___List_toString___at___Lean_Parser_dbgTraceStateFn_spec__0_spec__0___closed__0;
|
||||
static lean_object* l_Lean_Parser_tokenAntiquotFn___closed__7;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_takeWhileFn___lam__0___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -794,7 +794,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_decimalNum
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_identFnAux_parse___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_hygieneInfoFn___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_identEqFn(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Parser_strLitFnAux___redArg___closed__2;
|
||||
static lean_object* l_Lean_Parser_instReprLeadingIdentBehavior_repr___closed__0;
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_lookahead(lean_object*);
|
||||
static lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_errorAtSavedPos___regBuiltin_Lean_Parser_errorAtSavedPos_docString__1___closed__0;
|
||||
|
|
@ -6986,7 +6985,7 @@ return x_32;
|
|||
}
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_strLitFnAux___redArg___closed__0() {
|
||||
static lean_object* _init_l_Lean_Parser_strLitFnAux___closed__0() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -6994,16 +6993,16 @@ x_1 = lean_mk_string_unchecked("str", 3, 3);
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_strLitFnAux___redArg___closed__1() {
|
||||
static lean_object* _init_l_Lean_Parser_strLitFnAux___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Parser_strLitFnAux___redArg___closed__0;
|
||||
x_1 = l_Lean_Parser_strLitFnAux___closed__0;
|
||||
x_2 = l_Lean_Name_mkStr1(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Parser_strLitFnAux___redArg___closed__2() {
|
||||
static lean_object* _init_l_Lean_Parser_strLitFnAux___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -7011,66 +7010,60 @@ x_1 = lean_mk_string_unchecked("unterminated string literal", 27, 27);
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_strLitFnAux___redArg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_strLitFnAux(lean_object* x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5; uint8_t x_6;
|
||||
x_4 = lean_ctor_get(x_3, 2);
|
||||
x_5 = lean_ctor_get(x_2, 0);
|
||||
x_6 = l_Lean_Parser_InputContext_atEnd(x_5, x_4);
|
||||
if (x_6 == 0)
|
||||
lean_object* x_5; lean_object* x_6; uint8_t x_7;
|
||||
x_5 = lean_ctor_get(x_4, 2);
|
||||
x_6 = lean_ctor_get(x_3, 0);
|
||||
x_7 = l_Lean_Parser_InputContext_atEnd(x_6, x_5);
|
||||
if (x_7 == 0)
|
||||
{
|
||||
lean_object* x_7; uint32_t x_8; lean_object* x_9; lean_object* x_10; uint32_t x_11; uint8_t x_12;
|
||||
x_7 = lean_ctor_get(x_5, 0);
|
||||
x_8 = lean_string_utf8_get_fast(x_7, x_4);
|
||||
x_9 = lean_string_utf8_next_fast(x_7, x_4);
|
||||
x_10 = l_Lean_Parser_ParserState_setPos(x_3, x_9);
|
||||
x_11 = 34;
|
||||
x_12 = lean_uint32_dec_eq(x_8, x_11);
|
||||
if (x_12 == 0)
|
||||
lean_object* x_8; uint32_t x_9; lean_object* x_10; lean_object* x_11; uint32_t x_12; uint8_t x_13;
|
||||
x_8 = lean_ctor_get(x_6, 0);
|
||||
x_9 = lean_string_utf8_get_fast(x_8, x_5);
|
||||
x_10 = lean_string_utf8_next_fast(x_8, x_5);
|
||||
x_11 = l_Lean_Parser_ParserState_setPos(x_4, x_10);
|
||||
x_12 = 34;
|
||||
x_13 = lean_uint32_dec_eq(x_9, x_12);
|
||||
if (x_13 == 0)
|
||||
{
|
||||
uint32_t x_13; uint8_t x_14;
|
||||
x_13 = 92;
|
||||
x_14 = lean_uint32_dec_eq(x_8, x_13);
|
||||
if (x_14 == 0)
|
||||
uint32_t x_14; uint8_t x_15;
|
||||
x_14 = 92;
|
||||
x_15 = lean_uint32_dec_eq(x_9, x_14);
|
||||
if (x_15 == 0)
|
||||
{
|
||||
x_3 = x_10;
|
||||
x_4 = x_11;
|
||||
goto _start;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_16; lean_object* x_17; lean_object* x_18;
|
||||
x_16 = lean_alloc_closure((void*)(l_Lean_Parser_quotedStringFn), 2, 0);
|
||||
x_17 = lean_alloc_closure((void*)(l_Lean_Parser_strLitFnAux___redArg), 3, 1);
|
||||
lean_closure_set(x_17, 0, x_1);
|
||||
x_18 = l_Lean_Parser_andthenFn(x_16, x_17, x_2, x_10);
|
||||
return x_18;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_19; lean_object* x_20;
|
||||
x_19 = l_Lean_Parser_strLitFnAux___redArg___closed__1;
|
||||
x_20 = l_Lean_Parser_mkNodeToken(x_19, x_1, x_12, x_2, x_10);
|
||||
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
|
||||
x_17 = lean_alloc_closure((void*)(l_Lean_Parser_quotedStringFn), 2, 0);
|
||||
x_18 = lean_box(x_15);
|
||||
x_19 = lean_alloc_closure((void*)(l_Lean_Parser_strLitFnAux___boxed), 4, 2);
|
||||
lean_closure_set(x_19, 0, x_1);
|
||||
lean_closure_set(x_19, 1, x_18);
|
||||
x_20 = l_Lean_Parser_andthenFn(x_17, x_19, x_3, x_11);
|
||||
return x_20;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_21; lean_object* x_22;
|
||||
lean_dec_ref(x_2);
|
||||
x_21 = l_Lean_Parser_strLitFnAux___redArg___closed__2;
|
||||
x_22 = l_Lean_Parser_ParserState_mkUnexpectedErrorAt(x_3, x_21, x_1);
|
||||
x_21 = l_Lean_Parser_strLitFnAux___closed__1;
|
||||
x_22 = l_Lean_Parser_mkNodeToken(x_21, x_1, x_2, x_3, x_11);
|
||||
return x_22;
|
||||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_strLitFnAux(lean_object* x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
else
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = l_Lean_Parser_strLitFnAux___redArg(x_1, x_3, x_4);
|
||||
return x_5;
|
||||
lean_object* x_23; lean_object* x_24;
|
||||
lean_dec_ref(x_3);
|
||||
x_23 = l_Lean_Parser_strLitFnAux___closed__2;
|
||||
x_24 = l_Lean_Parser_ParserState_mkUnexpectedErrorAt(x_4, x_23, x_1);
|
||||
return x_24;
|
||||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Parser_strLitFnAux___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
|
|
@ -7183,7 +7176,7 @@ return x_17;
|
|||
else
|
||||
{
|
||||
lean_object* x_18; lean_object* x_19;
|
||||
x_18 = l_Lean_Parser_strLitFnAux___redArg___closed__1;
|
||||
x_18 = l_Lean_Parser_strLitFnAux___closed__1;
|
||||
x_19 = l_Lean_Parser_mkNodeToken(x_18, x_1, x_16, x_3, x_11);
|
||||
return x_19;
|
||||
}
|
||||
|
|
@ -7252,7 +7245,7 @@ else
|
|||
{
|
||||
lean_object* x_24; lean_object* x_25;
|
||||
lean_dec(x_21);
|
||||
x_24 = l_Lean_Parser_strLitFnAux___redArg___closed__1;
|
||||
x_24 = l_Lean_Parser_strLitFnAux___closed__1;
|
||||
x_25 = l_Lean_Parser_mkNodeToken(x_24, x_1, x_22, x_4, x_12);
|
||||
return x_25;
|
||||
}
|
||||
|
|
@ -9426,7 +9419,7 @@ return x_23;
|
|||
LEAN_EXPORT lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_tokenFnAux(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint32_t x_8; uint32_t x_9; uint8_t x_10;
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; uint32_t x_8; uint32_t x_9; uint8_t x_10; uint8_t x_11; uint8_t x_12; uint8_t x_19; uint8_t x_26; uint8_t x_34;
|
||||
x_3 = lean_ctor_get(x_1, 0);
|
||||
x_4 = lean_ctor_get(x_2, 2);
|
||||
x_5 = lean_ctor_get(x_1, 3);
|
||||
|
|
@ -9435,10 +9428,10 @@ x_7 = lean_ctor_get(x_3, 3);
|
|||
x_8 = lean_string_utf8_get(x_6, x_4);
|
||||
x_9 = 34;
|
||||
x_10 = lean_uint32_dec_eq(x_8, x_9);
|
||||
x_11 = 1;
|
||||
if (x_10 == 0)
|
||||
{
|
||||
uint8_t x_11; uint8_t x_12; uint8_t x_19; uint8_t x_26; uint8_t x_34; uint32_t x_42; uint8_t x_43;
|
||||
x_11 = 1;
|
||||
uint32_t x_42; uint8_t x_43;
|
||||
x_42 = 39;
|
||||
x_43 = lean_uint32_dec_eq(x_8, x_42);
|
||||
if (x_43 == 0)
|
||||
|
|
@ -9464,6 +9457,15 @@ x_34 = x_10;
|
|||
goto block_41;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_47; lean_object* x_48;
|
||||
lean_inc(x_4);
|
||||
x_47 = l_Lean_Parser_ParserState_next(x_2, x_1, x_4);
|
||||
x_48 = l_Lean_Parser_strLitFnAux(x_4, x_11, x_1, x_47);
|
||||
return x_48;
|
||||
}
|
||||
block_18:
|
||||
{
|
||||
if (x_12 == 0)
|
||||
|
|
@ -9575,15 +9577,6 @@ return x_40;
|
|||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_47; lean_object* x_48;
|
||||
lean_inc(x_4);
|
||||
x_47 = l_Lean_Parser_ParserState_next(x_2, x_1, x_4);
|
||||
x_48 = l_Lean_Parser_strLitFnAux___redArg(x_4, x_1, x_47);
|
||||
return x_48;
|
||||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_updateTokenCache(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
|
|
@ -11458,7 +11451,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_strLitFn(lean_object* x_1, lean_object* x
|
|||
_start:
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_3 = l_Lean_Parser_strLitFnAux___redArg___closed__1;
|
||||
x_3 = l_Lean_Parser_strLitFnAux___closed__1;
|
||||
x_4 = l_Lean_Parser_strLitFn___closed__0;
|
||||
x_5 = l_Lean_Parser_expectTokenFn(x_3, x_4, x_1, x_2);
|
||||
return x_5;
|
||||
|
|
@ -11468,7 +11461,7 @@ static lean_object* _init_l_Lean_Parser_strLitNoAntiquot___closed__0() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Parser_strLitFnAux___redArg___closed__0;
|
||||
x_1 = l_Lean_Parser_strLitFnAux___closed__0;
|
||||
x_2 = l_Lean_Parser_mkAtomicInfo(x_1);
|
||||
return x_2;
|
||||
}
|
||||
|
|
@ -18936,12 +18929,12 @@ l_Lean_Parser_charLitFnAux___closed__1 = _init_l_Lean_Parser_charLitFnAux___clos
|
|||
lean_mark_persistent(l_Lean_Parser_charLitFnAux___closed__1);
|
||||
l_Lean_Parser_charLitFnAux___closed__2 = _init_l_Lean_Parser_charLitFnAux___closed__2();
|
||||
lean_mark_persistent(l_Lean_Parser_charLitFnAux___closed__2);
|
||||
l_Lean_Parser_strLitFnAux___redArg___closed__0 = _init_l_Lean_Parser_strLitFnAux___redArg___closed__0();
|
||||
lean_mark_persistent(l_Lean_Parser_strLitFnAux___redArg___closed__0);
|
||||
l_Lean_Parser_strLitFnAux___redArg___closed__1 = _init_l_Lean_Parser_strLitFnAux___redArg___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_strLitFnAux___redArg___closed__1);
|
||||
l_Lean_Parser_strLitFnAux___redArg___closed__2 = _init_l_Lean_Parser_strLitFnAux___redArg___closed__2();
|
||||
lean_mark_persistent(l_Lean_Parser_strLitFnAux___redArg___closed__2);
|
||||
l_Lean_Parser_strLitFnAux___closed__0 = _init_l_Lean_Parser_strLitFnAux___closed__0();
|
||||
lean_mark_persistent(l_Lean_Parser_strLitFnAux___closed__0);
|
||||
l_Lean_Parser_strLitFnAux___closed__1 = _init_l_Lean_Parser_strLitFnAux___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_strLitFnAux___closed__1);
|
||||
l_Lean_Parser_strLitFnAux___closed__2 = _init_l_Lean_Parser_strLitFnAux___closed__2();
|
||||
lean_mark_persistent(l_Lean_Parser_strLitFnAux___closed__2);
|
||||
l___private_Lean_Parser_Basic_0__Lean_Parser_rawStrLitFnAux_errorUnterminated___closed__0 = _init_l___private_Lean_Parser_Basic_0__Lean_Parser_rawStrLitFnAux_errorUnterminated___closed__0();
|
||||
lean_mark_persistent(l___private_Lean_Parser_Basic_0__Lean_Parser_rawStrLitFnAux_errorUnterminated___closed__0);
|
||||
l_Lean_Parser_takeDigitsFn___closed__0 = _init_l_Lean_Parser_takeDigitsFn___closed__0();
|
||||
|
|
|
|||
6
stage0/stdlib/Std/Internal/Async.c
generated
6
stage0/stdlib/Std/Internal/Async.c
generated
|
|
@ -1,6 +1,6 @@
|
|||
// Lean compiler output
|
||||
// Module: Std.Internal.Async
|
||||
// Imports: Std.Internal.Async.Basic Std.Internal.Async.Timer Std.Internal.Async.TCP Std.Internal.Async.UDP Std.Internal.Async.DNS Std.Internal.Async.Select Std.Internal.Async.Process Std.Internal.Async.System
|
||||
// Imports: Std.Internal.Async.Basic Std.Internal.Async.Timer Std.Internal.Async.TCP Std.Internal.Async.UDP Std.Internal.Async.DNS Std.Internal.Async.Select Std.Internal.Async.Process Std.Internal.Async.System Std.Internal.Async.Signal
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
|
|
@ -21,6 +21,7 @@ lean_object* initialize_Std_Internal_Async_DNS(uint8_t builtin, lean_object*);
|
|||
lean_object* initialize_Std_Internal_Async_Select(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Std_Internal_Async_Process(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Std_Internal_Async_System(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Std_Internal_Async_Signal(uint8_t builtin, lean_object*);
|
||||
static bool _G_initialized = false;
|
||||
LEAN_EXPORT lean_object* initialize_Std_Internal_Async(uint8_t builtin, lean_object* w) {
|
||||
lean_object * res;
|
||||
|
|
@ -50,6 +51,9 @@ lean_dec_ref(res);
|
|||
res = initialize_Std_Internal_Async_System(builtin, lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Std_Internal_Async_Signal(builtin, lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
return lean_io_result_mk_ok(lean_box(0));
|
||||
}
|
||||
#ifdef __cplusplus
|
||||
|
|
|
|||
4160
stage0/stdlib/Std/Internal/Async/Signal.c
generated
Normal file
4160
stage0/stdlib/Std/Internal/Async/Signal.c
generated
Normal file
File diff suppressed because it is too large
Load diff
6
stage0/stdlib/Std/Internal/UV.c
generated
6
stage0/stdlib/Std/Internal/UV.c
generated
|
|
@ -1,6 +1,6 @@
|
|||
// Lean compiler output
|
||||
// Module: Std.Internal.UV
|
||||
// Imports: Init.System.IO Init.System.Promise Std.Internal.UV.Loop Std.Internal.UV.Timer Std.Internal.UV.TCP Std.Internal.UV.UDP Std.Internal.UV.System Std.Internal.UV.DNS
|
||||
// Imports: Init.System.IO Init.System.Promise Std.Internal.UV.Loop Std.Internal.UV.Timer Std.Internal.UV.TCP Std.Internal.UV.UDP Std.Internal.UV.System Std.Internal.UV.DNS Std.Internal.UV.Signal
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
|
|
@ -21,6 +21,7 @@ lean_object* initialize_Std_Internal_UV_TCP(uint8_t builtin, lean_object*);
|
|||
lean_object* initialize_Std_Internal_UV_UDP(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Std_Internal_UV_System(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Std_Internal_UV_DNS(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Std_Internal_UV_Signal(uint8_t builtin, lean_object*);
|
||||
static bool _G_initialized = false;
|
||||
LEAN_EXPORT lean_object* initialize_Std_Internal_UV(uint8_t builtin, lean_object* w) {
|
||||
lean_object * res;
|
||||
|
|
@ -50,6 +51,9 @@ lean_dec_ref(res);
|
|||
res = initialize_Std_Internal_UV_DNS(builtin, lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Std_Internal_UV_Signal(builtin, lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
return lean_io_result_mk_ok(lean_box(0));
|
||||
}
|
||||
#ifdef __cplusplus
|
||||
|
|
|
|||
84
stage0/stdlib/Std/Internal/UV/Signal.c
generated
Normal file
84
stage0/stdlib/Std/Internal/UV/Signal.c
generated
Normal file
|
|
@ -0,0 +1,84 @@
|
|||
// Lean compiler output
|
||||
// Module: Std.Internal.UV.Signal
|
||||
// Imports: Init.System.IO Init.System.Promise Init.Data.SInt Std.Net
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
#elif defined(__GNUC__) && !defined(__CLANG__)
|
||||
#pragma GCC diagnostic ignored "-Wunused-parameter"
|
||||
#pragma GCC diagnostic ignored "-Wunused-label"
|
||||
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
|
||||
#endif
|
||||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif
|
||||
LEAN_EXPORT lean_object* l_Std_Internal_UV_Signal_mk___boxed(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Std_Internal_UV_Signal_0__Std_Internal_UV_SignalImpl;
|
||||
lean_object* lean_uv_signal_mk(uint32_t, uint8_t, lean_object*);
|
||||
lean_object* lean_uv_signal_next(lean_object*, lean_object*);
|
||||
lean_object* lean_uv_signal_stop(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_Internal_UV_Signal_stop___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_Internal_UV_Signal_next___boxed(lean_object*, lean_object*);
|
||||
static lean_object* _init_l___private_Std_Internal_UV_Signal_0__Std_Internal_UV_SignalImpl() {
|
||||
_start:
|
||||
{
|
||||
return lean_box(0);
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Std_Internal_UV_Signal_mk___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
uint32_t x_4; uint8_t x_5; lean_object* x_6;
|
||||
x_4 = lean_unbox_uint32(x_1);
|
||||
lean_dec(x_1);
|
||||
x_5 = lean_unbox(x_2);
|
||||
x_6 = lean_uv_signal_mk(x_4, x_5, x_3);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Std_Internal_UV_Signal_next___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_uv_signal_next(x_1, x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Std_Internal_UV_Signal_stop___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = lean_uv_signal_stop(x_1, x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* initialize_Init_System_IO(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Init_System_Promise(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Init_Data_SInt(uint8_t builtin, lean_object*);
|
||||
lean_object* initialize_Std_Net(uint8_t builtin, lean_object*);
|
||||
static bool _G_initialized = false;
|
||||
LEAN_EXPORT lean_object* initialize_Std_Internal_UV_Signal(uint8_t builtin, lean_object* w) {
|
||||
lean_object * res;
|
||||
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
|
||||
_G_initialized = true;
|
||||
res = initialize_Init_System_IO(builtin, lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Init_System_Promise(builtin, lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Init_Data_SInt(builtin, lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Std_Net(builtin, lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l___private_Std_Internal_UV_Signal_0__Std_Internal_UV_SignalImpl = _init_l___private_Std_Internal_UV_Signal_0__Std_Internal_UV_SignalImpl();
|
||||
return lean_io_result_mk_ok(lean_box(0));
|
||||
}
|
||||
#ifdef __cplusplus
|
||||
}
|
||||
#endif
|
||||
Loading…
Add table
Reference in a new issue