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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2024-03-01 19:33:29 -08:00 • committed by Leonardo de Moura
parent 70d9106644
commit ea9a417371
12 changed files with 5461 additions and 2307 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
stage0/src/CMakeLists.txt generated
View file

@ -501,24 +501,18 @@ string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
# (also looks nicer in the build log)
file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a")
else()
string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,--whole-archive -lInit ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive")
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
endif()
# set up libInit_shared only on Windows; see also stdlib.make.in
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
endif()
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a")
set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
else()
string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive")
if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
endif()
set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
endif()
string(APPEND LEANSHARED_LINKER_FLAGS " -lInit_shared")
if (${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
# We do not use dynamic linking via leanshared for Emscripten to keep things

10
stage0/src/stdlib.make.in generated
View file

@ -42,14 +42,22 @@ Init:
Lean: Init
+"${LEAN_BIN}/leanmake" lib PKG=Lean $(LEANMAKE_OPTS) LEANC_OPTS+=-DLEAN_EXPORTING
${LIB}/temp/empty.c:
touch $@
# the following targets are all invoked by separate `make` calls; see src/CMakeLists.txt
# we specify the precise file names here to avoid rebuilds
${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/lean/libInit.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a
${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/lean/libInit.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LIB}/temp/empty.c
ifeq "${INIT_SHARED_LINKER_FLAGS}" ""
# create empty library on platforms without restrictive symbol limits; avoids costly indirections and troubles with cross-library exceptions
"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ ${LIB}/temp/empty.c ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
else
@echo "[ ] Building $@"
# on Windows, must remove file before writing a new one (since the old one may be in use)
@rm -f $@
"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ ${INIT_SHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
endif
Init_shared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}

95
stage0/stdlib/Init/Data/BitVec/Basic.c generated
View file

@ -50,7 +50,6 @@ LEAN_EXPORT lean_object* l_BitVec_or(lean_object*);
LEAN_EXPORT lean_object* l_BitVec_udiv(lean_object*);
LEAN_EXPORT lean_object* l_BitVec_instHShiftRightBitVec___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_BitVec_xor___rarg(lean_object*, lean_object*);
static lean_object* l_BitVec_ofInt___closed__1;
static lean_object* l_BitVec_term_____x23_______closed__12;
LEAN_EXPORT lean_object* l_BitVec___aux__Init__Data__BitVec__Basic______macroRules__BitVec__term_____x23_x27______1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_instDecidableEqBitVec___boxed(lean_object*);
@ -59,6 +58,7 @@ LEAN_EXPORT lean_object* l_BitVec_zeroExtend_x27(lean_object*, lean_object*, lea
LEAN_EXPORT lean_object* l_BitVec_getMsb___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_BitVec_toNat___rarg(lean_object*);
LEAN_EXPORT lean_object* l_BitVec_append(lean_object*);
lean_object* lean_int_emod(lean_object*, lean_object*);
static lean_object* l_BitVec_term_____x23_x27_______closed__1;
static lean_object* l_BitVec_instReprBitVec___closed__1;
LEAN_EXPORT lean_object* l_BitVec_instModBitVec___boxed(lean_object*);
@ -206,7 +206,6 @@ static lean_object* l_BitVec_term_____x23_______closed__9;
static lean_object* l_BitVec___aux__Init__Data__BitVec__Basic______macroRules__BitVec__term_____x23______1___closed__11;
LEAN_EXPORT lean_object* l_BitVec_abs___boxed(lean_object*, lean_object*);
lean_object* lean_nat_lxor(lean_object*, lean_object*);
lean_object* lean_nat_abs(lean_object*);
uint8_t l_Nat_testBit(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_BitVec_zeroExtend___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_BitVec_truncate___boxed(lean_object*, lean_object*, lean_object*);
@ -238,6 +237,7 @@ static lean_object* l_BitVec___aux__Init__Data__BitVec__Basic______macroRules__B
LEAN_EXPORT lean_object* l_BitVec_instHShiftRightBitVec___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_BitVec_instDecidableLtBitVecInstLTBitVec(lean_object*);
LEAN_EXPORT lean_object* l_BitVec_toInt(lean_object*, lean_object*);
lean_object* l_Int_toNat(lean_object*);
LEAN_EXPORT uint8_t l_BitVec_msb(lean_object*, lean_object*);
lean_object* lean_nat_shiftl(lean_object*, lean_object*);
uint8_t lean_int_dec_lt(lean_object*, lean_object*);
@ -683,43 +683,29 @@ return x_4;
LEAN_EXPORT lean_object* l_BitVec_toInt(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
x_3 = lean_unsigned_to_nat(0u);
x_4 = lean_nat_dec_lt(x_3, x_1);
if (x_4 == 0)
lean_object* x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6;
x_3 = lean_unsigned_to_nat(2u);
x_4 = lean_nat_mul(x_3, x_2);
x_5 = lean_nat_pow(x_3, x_1);
x_6 = lean_nat_dec_lt(x_4, x_5);
lean_dec(x_4);
if (x_6 == 0)
{
lean_object* x_5;
x_5 = lean_nat_to_int(x_2);
return x_5;
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_nat_to_int(x_2);
x_8 = lean_nat_to_int(x_5);
x_9 = lean_int_sub(x_7, x_8);
lean_dec(x_8);
lean_dec(x_7);
return x_9;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_6 = lean_unsigned_to_nat(1u);
x_7 = lean_nat_sub(x_1, x_6);
x_8 = lean_nat_sub(x_7, x_3);
lean_dec(x_7);
x_9 = l_Nat_testBit(x_2, x_8);
lean_dec(x_8);
if (x_9 == 0)
{
lean_object* x_10;
lean_dec(x_5);
x_10 = lean_nat_to_int(x_2);
return x_10;
}
else
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_11 = lean_nat_to_int(x_2);
x_12 = lean_unsigned_to_nat(2u);
x_13 = lean_nat_pow(x_12, x_1);
x_14 = lean_nat_to_int(x_13);
x_15 = lean_int_sub(x_11, x_14);
lean_dec(x_14);
lean_dec(x_11);
return x_15;
}
}
}
}
LEAN_EXPORT lean_object* l_BitVec_toInt___boxed(lean_object* x_1, lean_object* x_2) {
@ -731,47 +717,18 @@ lean_dec(x_1);
return x_3;
}
}
static lean_object* _init_l_BitVec_ofInt___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_BitVec_ofInt(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
x_3 = l_BitVec_ofInt___closed__1;
x_4 = lean_int_dec_lt(x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_nat_abs(x_2);
x_6 = l_BitVec_ofNat(x_1, x_5);
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = lean_unsigned_to_nat(2u);
x_4 = lean_nat_pow(x_3, x_1);
x_5 = lean_nat_to_int(x_4);
x_6 = lean_int_emod(x_2, x_5);
lean_dec(x_5);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_7 = lean_nat_abs(x_2);
x_8 = lean_unsigned_to_nat(1u);
x_9 = lean_nat_sub(x_7, x_8);
lean_dec(x_7);
x_10 = lean_unsigned_to_nat(2u);
x_11 = lean_nat_pow(x_10, x_1);
x_12 = lean_nat_mod(x_9, x_11);
lean_dec(x_9);
x_13 = lean_nat_sub(x_11, x_12);
lean_dec(x_12);
lean_dec(x_11);
x_14 = lean_nat_sub(x_13, x_8);
lean_dec(x_13);
return x_14;
}
x_7 = l_Int_toNat(x_6);
lean_dec(x_6);
return x_7;
}
}
LEAN_EXPORT lean_object* l_BitVec_ofInt___boxed(lean_object* x_1, lean_object* x_2) {
@ -3490,8 +3447,6 @@ l_BitVec_nil___closed__1 = _init_l_BitVec_nil___closed__1();
lean_mark_persistent(l_BitVec_nil___closed__1);
l_BitVec_nil = _init_l_BitVec_nil();
lean_mark_persistent(l_BitVec_nil);
l_BitVec_ofInt___closed__1 = _init_l_BitVec_ofInt___closed__1();
lean_mark_persistent(l_BitVec_ofInt___closed__1);
l_BitVec_term_____x23_______closed__1 = _init_l_BitVec_term_____x23_______closed__1();
lean_mark_persistent(l_BitVec_term_____x23_______closed__1);
l_BitVec_term_____x23_______closed__2 = _init_l_BitVec_term_____x23_______closed__2();

127
stage0/stdlib/Init/Data/Int/DivMod.c generated
View file

@ -14,15 +14,21 @@
extern "C" {
#endif
static lean_object* l_Int_fdiv___closed__1;
LEAN_EXPORT lean_object* l_Nat_cast___at_Int_bmod___spec__1(lean_object*);
static lean_object* l_Int_bmod___closed__1;
LEAN_EXPORT lean_object* l_Int_mod___boxed(lean_object*, lean_object*);
lean_object* lean_int_emod(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_ediv___boxed(lean_object*, lean_object*);
static lean_object* l_Int_bmod___closed__2;
LEAN_EXPORT lean_object* l_Int_fdiv(lean_object*, lean_object*);
lean_object* lean_nat_to_int(lean_object*);
lean_object* lean_nat_div(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_fmod(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_fdiv___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_bmod___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_div___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_bmod(lean_object*, lean_object*);
lean_object* lean_int_sub(lean_object*, lean_object*);
lean_object* l_Int_subNatNat(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_instDivInt;
lean_object* lean_int_div(lean_object*, lean_object*);
@ -33,14 +39,17 @@ lean_object* lean_nat_mod(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_fmod___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_emod___boxed(lean_object*, lean_object*);
uint8_t lean_int_dec_lt(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_bdiv(lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* lean_int_mod(lean_object*, lean_object*);
lean_object* lean_int_neg_succ_of_nat(lean_object*);
LEAN_EXPORT lean_object* l_Int_instModInt;
lean_object* lean_int_add(lean_object*, lean_object*);
lean_object* lean_int_ediv(lean_object*, lean_object*);
lean_object* lean_int_neg(lean_object*);
static lean_object* l_Int_instModInt___closed__1;
lean_object* lean_nat_add(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_bdiv___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_div___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -346,6 +355,120 @@ x_1 = l_Int_instModInt___closed__1;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Nat_cast___at_Int_bmod___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
static lean_object* _init_l_Int_bmod___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(1u);
x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
static lean_object* _init_l_Int_bmod___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(2u);
x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Int_bmod(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; lean_object* x_8; uint8_t x_9;
x_3 = lean_nat_to_int(x_2);
x_4 = lean_int_emod(x_1, x_3);
x_5 = l_Int_bmod___closed__1;
x_6 = lean_int_add(x_3, x_5);
x_7 = l_Int_bmod___closed__2;
x_8 = lean_int_ediv(x_6, x_7);
lean_dec(x_6);
x_9 = lean_int_dec_lt(x_4, x_8);
lean_dec(x_8);
if (x_9 == 0)
{
lean_object* x_10;
x_10 = lean_int_sub(x_4, x_3);
lean_dec(x_3);
lean_dec(x_4);
return x_10;
}
else
{
lean_dec(x_3);
return x_4;
}
}
}
LEAN_EXPORT lean_object* l_Int_bmod___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Int_bmod(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Int_bdiv(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
x_3 = lean_unsigned_to_nat(0u);
x_4 = lean_nat_dec_eq(x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12;
x_5 = lean_nat_to_int(x_2);
x_6 = lean_int_ediv(x_1, x_5);
x_7 = lean_int_emod(x_1, x_5);
x_8 = l_Int_bmod___closed__1;
x_9 = lean_int_add(x_5, x_8);
lean_dec(x_5);
x_10 = l_Int_bmod___closed__2;
x_11 = lean_int_ediv(x_9, x_10);
lean_dec(x_9);
x_12 = lean_int_dec_lt(x_7, x_11);
lean_dec(x_11);
lean_dec(x_7);
if (x_12 == 0)
{
lean_object* x_13;
x_13 = lean_int_add(x_6, x_8);
lean_dec(x_6);
return x_13;
}
else
{
return x_6;
}
}
else
{
lean_object* x_14;
lean_dec(x_2);
x_14 = l_Int_fdiv___closed__1;
return x_14;
}
}
}
LEAN_EXPORT lean_object* l_Int_bdiv___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Int_bdiv(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* initialize_Init_Data_Int_Basic(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data_Int_DivMod(uint8_t builtin, lean_object* w) {
@ -365,6 +488,10 @@ l_Int_instModInt___closed__1 = _init_l_Int_instModInt___closed__1();
lean_mark_persistent(l_Int_instModInt___closed__1);
l_Int_instModInt = _init_l_Int_instModInt();
lean_mark_persistent(l_Int_instModInt);
l_Int_bmod___closed__1 = _init_l_Int_bmod___closed__1();
lean_mark_persistent(l_Int_bmod___closed__1);
l_Int_bmod___closed__2 = _init_l_Int_bmod___closed__2();
lean_mark_persistent(l_Int_bmod___closed__2);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

67
stage0/stdlib/Init/Data/Int/DivModLemmas.c generated
View file

@ -15,18 +15,10 @@ extern "C" {
#endif
LEAN_EXPORT uint8_t l_Int_decidableDvd(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_decidableDvd___boxed(lean_object*, lean_object*);
static lean_object* l_Int_bmod___closed__1;
lean_object* lean_int_emod(lean_object*, lean_object*);
static lean_object* l_Int_bmod___closed__2;
lean_object* lean_nat_to_int(lean_object*);
LEAN_EXPORT lean_object* l_Int_bmod___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_bmod(lean_object*, lean_object*);
static lean_object* l_Int_decidableDvd___closed__1;
lean_object* lean_int_sub(lean_object*, lean_object*);
uint8_t lean_int_dec_lt(lean_object*, lean_object*);
lean_object* lean_int_add(lean_object*, lean_object*);
uint8_t lean_int_dec_eq(lean_object*, lean_object*);
lean_object* lean_int_ediv(lean_object*, lean_object*);
static lean_object* _init_l_Int_decidableDvd___closed__1() {
_start:
{
@ -58,61 +50,6 @@ x_4 = lean_box(x_3);
return x_4;
}
}
static lean_object* _init_l_Int_bmod___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(1u);
x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
static lean_object* _init_l_Int_bmod___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(2u);
x_2 = lean_nat_to_int(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Int_bmod(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; lean_object* x_8; uint8_t x_9;
x_3 = lean_nat_to_int(x_2);
x_4 = lean_int_emod(x_1, x_3);
x_5 = l_Int_bmod___closed__1;
x_6 = lean_int_add(x_3, x_5);
x_7 = l_Int_bmod___closed__2;
x_8 = lean_int_ediv(x_6, x_7);
lean_dec(x_6);
x_9 = lean_int_dec_lt(x_4, x_8);
lean_dec(x_8);
if (x_9 == 0)
{
lean_object* x_10;
x_10 = lean_int_sub(x_4, x_3);
lean_dec(x_3);
lean_dec(x_4);
return x_10;
}
else
{
lean_dec(x_3);
return x_4;
}
}
}
LEAN_EXPORT lean_object* l_Int_bmod___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Int_bmod(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* initialize_Init_Data_Int_DivMod(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Int_Order(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Nat_Dvd(uint8_t builtin, lean_object*);
@ -140,10 +77,6 @@ if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Int_decidableDvd___closed__1 = _init_l_Int_decidableDvd___closed__1();
lean_mark_persistent(l_Int_decidableDvd___closed__1);
l_Int_bmod___closed__1 = _init_l_Int_bmod___closed__1();
lean_mark_persistent(l_Int_bmod___closed__1);
l_Int_bmod___closed__2 = _init_l_Int_bmod___closed__2();
lean_mark_persistent(l_Int_bmod___closed__2);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

102
stage0/stdlib/Init/Tactics.c generated
View file

@ -21712,27 +21712,28 @@ static lean_object* _init_l_Lean_Parser_Tactic___aux__Init__Tactics______macroRu
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("show_term_elab", 14);
x_1 = lean_mk_string_from_bytes("showTermElabImpl", 16);
return x_1;
}
}
static lean_object* _init_l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__showTermElab__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__showTermElab__1___closed__2;
x_2 = l_String_toSubstring_x27(x_1);
return x_2;
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_Tactic_withAnnotateState___closed__1;
x_2 = l_Lean_Parser_Tactic_withAnnotateState___closed__2;
x_3 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticExfalso__1___closed__1;
x_4 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__showTermElab__1___closed__2;
x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__showTermElab__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__showTermElab__1___closed__2;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("show_term_elab", 14);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__showTermElab__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@ -21755,59 +21756,50 @@ return x_7;
}
else
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34;
x_8 = lean_unsigned_to_nat(1u);
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_8 = lean_unsigned_to_nat(0u);
x_9 = l_Lean_Syntax_getArg(x_1, x_8);
x_10 = lean_unsigned_to_nat(1u);
x_11 = l_Lean_Syntax_getArg(x_1, x_10);
lean_dec(x_1);
x_10 = lean_ctor_get(x_2, 5);
lean_inc(x_10);
x_11 = 0;
x_12 = l_Lean_SourceInfo_fromRef(x_10, x_11);
x_13 = lean_ctor_get(x_2, 2);
lean_inc(x_13);
x_14 = lean_ctor_get(x_2, 1);
lean_inc(x_14);
lean_dec(x_2);
x_15 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticRefine__lift____1___closed__3;
x_12 = lean_ctor_get(x_2, 5);
lean_inc(x_12);
lean_dec(x_2);
x_13 = 0;
x_14 = l_Lean_SourceInfo_fromRef(x_12, x_13);
x_15 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticRefine__lift____1___closed__3;
lean_inc(x_14);
x_16 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_16, 0, x_12);
lean_ctor_set(x_16, 0, x_14);
lean_ctor_set(x_16, 1, x_15);
x_17 = l_Lean_Parser_Tactic_paren___closed__3;
lean_inc(x_12);
lean_inc(x_14);
x_18 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_18, 0, x_12);
lean_ctor_set(x_18, 0, x_14);
lean_ctor_set(x_18, 1, x_17);
x_19 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__showTermElab__1___closed__4;
x_20 = l_Lean_addMacroScope(x_14, x_19, x_13);
x_21 = lean_box(0);
x_22 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__showTermElab__1___closed__3;
lean_inc(x_12);
x_23 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_23, 0, x_12);
lean_ctor_set(x_23, 1, x_22);
lean_ctor_set(x_23, 2, x_20);
lean_ctor_set(x_23, 3, x_21);
x_24 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticExfalso__1___closed__14;
lean_inc(x_12);
x_25 = l_Lean_Syntax_node1(x_12, x_24, x_9);
x_26 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticExfalso__1___closed__3;
lean_inc(x_12);
x_27 = l_Lean_Syntax_node2(x_12, x_26, x_23, x_25);
x_28 = l_Lean_Parser_Tactic_paren___closed__9;
lean_inc(x_12);
x_29 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_29, 0, x_12);
lean_ctor_set(x_29, 1, x_28);
x_30 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__showTermElab__1___closed__1;
lean_inc(x_12);
x_31 = l_Lean_Syntax_node3(x_12, x_30, x_18, x_27, x_29);
x_32 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticRefine__lift____1___closed__2;
x_33 = l_Lean_Syntax_node2(x_12, x_32, x_16, x_31);
x_34 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_34, 0, x_33);
lean_ctor_set(x_34, 1, x_3);
return x_34;
x_19 = 1;
x_20 = l_Lean_SourceInfo_fromRef(x_9, x_19);
x_21 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__showTermElab__1___closed__4;
x_22 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
x_23 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__showTermElab__1___closed__3;
lean_inc(x_14);
x_24 = l_Lean_Syntax_node2(x_14, x_23, x_22, x_11);
x_25 = l_Lean_Parser_Tactic_paren___closed__9;
lean_inc(x_14);
x_26 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_26, 0, x_14);
lean_ctor_set(x_26, 1, x_25);
x_27 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__showTermElab__1___closed__1;
lean_inc(x_14);
x_28 = l_Lean_Syntax_node3(x_14, x_27, x_18, x_24, x_26);
x_29 = l_Lean_Parser_Tactic___aux__Init__Tactics______macroRules__Lean__Parser__Tactic__tacticRefine__lift____1___closed__2;
x_30 = l_Lean_Syntax_node2(x_14, x_29, x_16, x_28);
x_31 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_3);
return x_31;
}
}
}

12
stage0/stdlib/Lean/Elab/Tactic/Omega/OmegaM.c generated
View file

@ -3404,13 +3404,11 @@ return x_3;
static lean_object* _init_l_Lean_Elab_Tactic_Omega_analyzeAtom___closed__71() {
_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_Elab_Tactic_Omega_atomsCoeffs___rarg___closed__1;
x_2 = l_Lean_Elab_Tactic_Omega_atomsCoeffs___rarg___closed__2;
x_3 = l_Lean_Elab_Tactic_Omega_atomsList___rarg___closed__1;
x_4 = l_Lean_Elab_Tactic_Omega_analyzeAtom___closed__37;
x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
return x_5;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Tactic_Omega_atomsList___rarg___closed__1;
x_2 = l_Lean_Elab_Tactic_Omega_analyzeAtom___closed__37;
x_3 = l_Lean_Name_mkStr2(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_Omega_analyzeAtom___closed__72() {

470
stage0/stdlib/Lean/Elab/Tactic/ShowTerm.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Elab.Tactic.ShowTerm
// Imports: Init Lean.Elab.ElabRules Lean.Meta.Tactic.TryThis
// Imports: Lean.Elab.ElabRules Lean.Meta.Tactic.TryThis
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -17,14 +17,12 @@ static lean_object* l___regBuiltin_Std_Tactic_elabShowTerm_declRange___closed__7
lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Std_Tactic_evalShowTerm___closed__3;
lean_object* l_Lean_addBuiltinDocString(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_matchesIdent(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Std_Tactic_evalShowTerm___closed__5;
LEAN_EXPORT lean_object* l___regBuiltin_Std_Tactic_evalShowTerm_declRange(lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Std_Tactic_elabShowTerm_declRange(lean_object*);
static lean_object* l_Std_Tactic_elabShowTerm___closed__3;
lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Std_Tactic_evalShowTerm_declRange___closed__1;
static lean_object* l___regBuiltin_Std_Tactic_elabShowTerm___closed__5;
LEAN_EXPORT lean_object* l___regBuiltin_Std_Tactic_elabShowTerm(lean_object*);
static lean_object* l___regBuiltin_Std_Tactic_evalShowTerm___closed__4;
lean_object* l_Lean_Meta_Tactic_TryThis_addTermSuggestion(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -40,8 +38,6 @@ static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Std_Tactic_evalShowT
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
lean_object* l_Lean_Expr_mvar___override(lean_object*);
LEAN_EXPORT lean_object* l_Std_Tactic_elabShowTerm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Std_Tactic_elabShowTerm___closed__6;
static lean_object* l_Std_Tactic_elabShowTerm___closed__6;
static lean_object* l___regBuiltin_Std_Tactic_elabShowTerm_declRange___closed__5;
LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Std_Tactic_evalShowTerm___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Tactic_evalShowTerm___closed__4;
@ -54,22 +50,17 @@ static lean_object* l___regBuiltin_Std_Tactic_elabShowTerm_declRange___closed__3
extern lean_object* l_Lean_Elab_Term_termElabAttribute;
static lean_object* l___regBuiltin_Std_Tactic_evalShowTerm_declRange___closed__3;
LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Std_Tactic_evalShowTerm___spec__1___rarg(lean_object*);
static lean_object* l_Std_Tactic_elabShowTerm___closed__7;
lean_object* l_Lean_Meta_Tactic_TryThis_addExactSuggestion(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Std_Tactic_evalShowTerm_declRange___closed__4;
static lean_object* l___regBuiltin_Std_Tactic_evalShowTerm___closed__1;
static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Std_Tactic_evalShowTerm___spec__1___rarg___closed__2;
static lean_object* l___regBuiltin_Std_Tactic_evalShowTerm_declRange___closed__7;
lean_object* l_Lean_instantiateMVars___at_Lean_Elab_Tactic_getMainTarget___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
static lean_object* l_Std_Tactic_elabShowTerm___closed__8;
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
uint8_t l_Lean_Syntax_matchesNull(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Tactic_evalShowTerm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Std_Tactic_evalShowTerm_declRange___closed__6;
static lean_object* l_Std_Tactic_evalShowTerm___closed__5;
static lean_object* l_Std_Tactic_elabShowTerm___closed__2;
static lean_object* l_Std_Tactic_elabShowTerm___closed__5;
static lean_object* l_Std_Tactic_elabShowTerm___closed__4;
static lean_object* l___regBuiltin_Std_Tactic_elabShowTerm_declRange___closed__4;
static lean_object* l___regBuiltin_Std_Tactic_evalShowTerm_declRange___closed__2;
@ -410,7 +401,7 @@ static lean_object* _init_l___regBuiltin_Std_Tactic_evalShowTerm_declRange___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(12u);
x_1 = lean_unsigned_to_nat(13u);
x_2 = lean_unsigned_to_nat(27u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -422,7 +413,7 @@ static lean_object* _init_l___regBuiltin_Std_Tactic_evalShowTerm_declRange___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(18u);
x_1 = lean_unsigned_to_nat(19u);
x_2 = lean_unsigned_to_nat(31u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -450,7 +441,7 @@ static lean_object* _init_l___regBuiltin_Std_Tactic_evalShowTerm_declRange___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(12u);
x_1 = lean_unsigned_to_nat(13u);
x_2 = lean_unsigned_to_nat(31u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -462,7 +453,7 @@ static lean_object* _init_l___regBuiltin_Std_Tactic_evalShowTerm_declRange___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(12u);
x_1 = lean_unsigned_to_nat(13u);
x_2 = lean_unsigned_to_nat(43u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -512,67 +503,31 @@ static lean_object* _init_l_Std_Tactic_elabShowTerm___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("term_%_", 7);
x_1 = lean_mk_string_from_bytes("Term", 4);
return x_1;
}
}
static lean_object* _init_l_Std_Tactic_elabShowTerm___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Std_Tactic_elabShowTerm___closed__1;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("showTermElabImpl", 16);
return x_1;
}
}
static lean_object* _init_l_Std_Tactic_elabShowTerm___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("show_term_elab", 14);
return x_1;
}
}
static lean_object* _init_l_Std_Tactic_elabShowTerm___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Std_Tactic_elabShowTerm___closed__3;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Std_Tactic_elabShowTerm___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("Term", 4);
return x_1;
}
}
static lean_object* _init_l_Std_Tactic_elabShowTerm___closed__6() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("app", 3);
return x_1;
}
}
static lean_object* _init_l_Std_Tactic_elabShowTerm___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Std_Tactic_evalShowTerm___closed__1;
x_2 = l_Std_Tactic_evalShowTerm___closed__2;
x_3 = l_Std_Tactic_elabShowTerm___closed__5;
x_4 = l_Std_Tactic_elabShowTerm___closed__6;
x_3 = l_Std_Tactic_elabShowTerm___closed__1;
x_4 = l_Std_Tactic_elabShowTerm___closed__2;
x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
return x_5;
}
}
static lean_object* _init_l_Std_Tactic_elabShowTerm___closed__8() {
static lean_object* _init_l_Std_Tactic_elabShowTerm___closed__4() {
_start:
{
lean_object* x_1;
@ -584,7 +539,7 @@ LEAN_EXPORT lean_object* l_Std_Tactic_elabShowTerm(lean_object* x_1, lean_object
_start:
{
lean_object* x_10; uint8_t x_11;
x_10 = l_Std_Tactic_elabShowTerm___closed__2;
x_10 = l_Std_Tactic_elabShowTerm___closed__3;
lean_inc(x_1);
x_11 = l_Lean_Syntax_isOfKind(x_1, x_10);
if (x_11 == 0)
@ -603,236 +558,167 @@ return x_12;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16;
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19;
x_13 = lean_unsigned_to_nat(0u);
x_14 = l_Lean_Syntax_getArg(x_1, x_13);
x_15 = l_Std_Tactic_elabShowTerm___closed__4;
x_16 = l_Lean_Syntax_matchesIdent(x_14, x_15);
lean_dec(x_14);
if (x_16 == 0)
{
lean_object* x_17;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_15 = lean_unsigned_to_nat(1u);
x_16 = l_Lean_Syntax_getArg(x_1, x_15);
lean_dec(x_1);
x_17 = l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_elabLetMVar___spec__1___rarg(x_9);
return x_17;
}
else
x_17 = lean_box(0);
x_18 = 1;
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_19 = l_Lean_Elab_Term_elabTermEnsuringType(x_16, x_2, x_18, x_18, x_17, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_19) == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21;
x_18 = lean_unsigned_to_nat(2u);
x_19 = l_Lean_Syntax_getArg(x_1, x_18);
lean_dec(x_1);
x_20 = l_Std_Tactic_elabShowTerm___closed__7;
lean_inc(x_19);
x_21 = l_Lean_Syntax_isOfKind(x_19, x_20);
if (x_21 == 0)
{
lean_object* x_22;
lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23;
x_20 = lean_ctor_get(x_19, 0);
lean_inc(x_20);
x_21 = lean_ctor_get(x_19, 1);
lean_inc(x_21);
lean_dec(x_19);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_22 = l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_elabLetMVar___spec__1___rarg(x_9);
return x_22;
}
else
x_22 = 0;
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_23 = l_Lean_Elab_Term_synthesizeSyntheticMVars(x_22, x_22, x_3, x_4, x_5, x_6, x_7, x_8, x_21);
if (lean_obj_tag(x_23) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26;
x_23 = l_Lean_Syntax_getArg(x_19, x_13);
x_24 = lean_unsigned_to_nat(1u);
x_25 = l_Lean_Syntax_getArg(x_19, x_24);
lean_dec(x_19);
lean_inc(x_25);
x_26 = l_Lean_Syntax_matchesNull(x_25, x_24);
if (x_26 == 0)
{
lean_object* x_27;
lean_dec(x_25);
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_24 = lean_ctor_get(x_23, 1);
lean_inc(x_24);
lean_dec(x_23);
lean_inc(x_20);
x_25 = l_Lean_instantiateMVars___at_Lean_Elab_Term_MVarErrorInfo_logError___spec__1(x_20, x_3, x_4, x_5, x_6, x_7, x_8, x_24);
lean_dec(x_4);
lean_dec(x_3);
x_26 = lean_ctor_get(x_25, 0);
lean_inc(x_26);
x_27 = lean_ctor_get(x_25, 1);
lean_inc(x_27);
lean_dec(x_25);
x_28 = lean_ctor_get(x_7, 5);
lean_inc(x_28);
x_29 = l_Lean_Expr_headBeta(x_26);
x_30 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_30, 0, x_28);
x_31 = l_Std_Tactic_elabShowTerm___closed__4;
x_32 = l_Lean_Meta_Tactic_TryThis_addTermSuggestion(x_14, x_29, x_30, x_31, x_17, x_5, x_6, x_7, x_8, x_27);
if (lean_obj_tag(x_32) == 0)
{
uint8_t x_33;
x_33 = !lean_is_exclusive(x_32);
if (x_33 == 0)
{
lean_object* x_34;
x_34 = lean_ctor_get(x_32, 0);
lean_dec(x_34);
lean_ctor_set(x_32, 0, x_20);
return x_32;
}
else
{
lean_object* x_35; lean_object* x_36;
x_35 = lean_ctor_get(x_32, 1);
lean_inc(x_35);
lean_dec(x_32);
x_36 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_36, 0, x_20);
lean_ctor_set(x_36, 1, x_35);
return x_36;
}
}
else
{
uint8_t x_37;
lean_dec(x_20);
x_37 = !lean_is_exclusive(x_32);
if (x_37 == 0)
{
return x_32;
}
else
{
lean_object* x_38; lean_object* x_39; lean_object* x_40;
x_38 = lean_ctor_get(x_32, 0);
x_39 = lean_ctor_get(x_32, 1);
lean_inc(x_39);
lean_inc(x_38);
lean_dec(x_32);
x_40 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_40, 0, x_38);
lean_ctor_set(x_40, 1, x_39);
return x_40;
}
}
}
else
{
uint8_t x_41;
lean_dec(x_20);
lean_dec(x_14);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_27 = l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_elabLetMVar___spec__1___rarg(x_9);
return x_27;
x_41 = !lean_is_exclusive(x_23);
if (x_41 == 0)
{
return x_23;
}
else
{
lean_object* x_28; lean_object* x_29; uint8_t x_30; lean_object* x_31;
x_28 = l_Lean_Syntax_getArg(x_25, x_13);
lean_dec(x_25);
x_29 = lean_box(0);
x_30 = 1;
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_31 = l_Lean_Elab_Term_elabTermEnsuringType(x_28, x_2, x_30, x_30, x_29, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_31) == 0)
{
lean_object* x_32; lean_object* x_33; uint8_t x_34; lean_object* x_35;
x_32 = lean_ctor_get(x_31, 0);
lean_inc(x_32);
x_33 = lean_ctor_get(x_31, 1);
lean_inc(x_33);
lean_dec(x_31);
x_34 = 0;
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_35 = l_Lean_Elab_Term_synthesizeSyntheticMVars(x_34, x_34, x_3, x_4, x_5, x_6, x_7, x_8, x_33);
if (lean_obj_tag(x_35) == 0)
{
lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44;
x_36 = lean_ctor_get(x_35, 1);
lean_inc(x_36);
lean_dec(x_35);
lean_inc(x_32);
x_37 = l_Lean_instantiateMVars___at_Lean_Elab_Term_MVarErrorInfo_logError___spec__1(x_32, x_3, x_4, x_5, x_6, x_7, x_8, x_36);
lean_dec(x_4);
lean_dec(x_3);
x_38 = lean_ctor_get(x_37, 0);
lean_inc(x_38);
x_39 = lean_ctor_get(x_37, 1);
lean_inc(x_39);
lean_dec(x_37);
x_40 = lean_ctor_get(x_7, 5);
lean_inc(x_40);
x_41 = l_Lean_Expr_headBeta(x_38);
x_42 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_42, 0, x_40);
x_43 = l_Std_Tactic_elabShowTerm___closed__8;
x_44 = l_Lean_Meta_Tactic_TryThis_addTermSuggestion(x_23, x_41, x_42, x_43, x_29, x_5, x_6, x_7, x_8, x_39);
if (lean_obj_tag(x_44) == 0)
lean_object* x_42; lean_object* x_43; lean_object* x_44;
x_42 = lean_ctor_get(x_23, 0);
x_43 = lean_ctor_get(x_23, 1);
lean_inc(x_43);
lean_inc(x_42);
lean_dec(x_23);
x_44 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_44, 0, x_42);
lean_ctor_set(x_44, 1, x_43);
return x_44;
}
}
}
else
{
uint8_t x_45;
x_45 = !lean_is_exclusive(x_44);
lean_dec(x_14);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_45 = !lean_is_exclusive(x_19);
if (x_45 == 0)
{
lean_object* x_46;
x_46 = lean_ctor_get(x_44, 0);
lean_dec(x_46);
lean_ctor_set(x_44, 0, x_32);
return x_44;
return x_19;
}
else
{
lean_object* x_47; lean_object* x_48;
x_47 = lean_ctor_get(x_44, 1);
lean_object* x_46; lean_object* x_47; lean_object* x_48;
x_46 = lean_ctor_get(x_19, 0);
x_47 = lean_ctor_get(x_19, 1);
lean_inc(x_47);
lean_dec(x_44);
x_48 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_48, 0, x_32);
lean_inc(x_46);
lean_dec(x_19);
x_48 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_48, 0, x_46);
lean_ctor_set(x_48, 1, x_47);
return x_48;
}
}
else
{
uint8_t x_49;
lean_dec(x_32);
x_49 = !lean_is_exclusive(x_44);
if (x_49 == 0)
{
return x_44;
}
else
{
lean_object* x_50; lean_object* x_51; lean_object* x_52;
x_50 = lean_ctor_get(x_44, 0);
x_51 = lean_ctor_get(x_44, 1);
lean_inc(x_51);
lean_inc(x_50);
lean_dec(x_44);
x_52 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_52, 0, x_50);
lean_ctor_set(x_52, 1, x_51);
return x_52;
}
}
}
else
{
uint8_t x_53;
lean_dec(x_32);
lean_dec(x_23);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_53 = !lean_is_exclusive(x_35);
if (x_53 == 0)
{
return x_35;
}
else
{
lean_object* x_54; lean_object* x_55; lean_object* x_56;
x_54 = lean_ctor_get(x_35, 0);
x_55 = lean_ctor_get(x_35, 1);
lean_inc(x_55);
lean_inc(x_54);
lean_dec(x_35);
x_56 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_56, 0, x_54);
lean_ctor_set(x_56, 1, x_55);
return x_56;
}
}
}
else
{
uint8_t x_57;
lean_dec(x_23);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_57 = !lean_is_exclusive(x_31);
if (x_57 == 0)
{
return x_31;
}
else
{
lean_object* x_58; lean_object* x_59; lean_object* x_60;
x_58 = lean_ctor_get(x_31, 0);
x_59 = lean_ctor_get(x_31, 1);
lean_inc(x_59);
lean_inc(x_58);
lean_dec(x_31);
x_60 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_60, 0, x_58);
lean_ctor_set(x_60, 1, x_59);
return x_60;
}
}
}
}
}
}
}
}
@ -840,42 +726,22 @@ static lean_object* _init_l___regBuiltin_Std_Tactic_elabShowTerm___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("showTermElabImpl", 16);
x_1 = lean_mk_string_from_bytes("elabShowTerm", 12);
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Std_Tactic_elabShowTerm___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Std_Tactic_evalShowTerm___closed__1;
x_2 = l_Std_Tactic_evalShowTerm___closed__2;
x_3 = l_Std_Tactic_elabShowTerm___closed__5;
x_4 = l___regBuiltin_Std_Tactic_elabShowTerm___closed__1;
x_5 = l_Lean_Name_mkStr4(x_1, x_2, x_3, x_4);
return x_5;
}
}
static lean_object* _init_l___regBuiltin_Std_Tactic_elabShowTerm___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("elabShowTerm", 12);
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Std_Tactic_elabShowTerm___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___regBuiltin_Std_Tactic_evalShowTerm___closed__1;
x_2 = l_Std_Tactic_evalShowTerm___closed__3;
x_3 = l___regBuiltin_Std_Tactic_elabShowTerm___closed__3;
x_3 = l___regBuiltin_Std_Tactic_elabShowTerm___closed__1;
x_4 = l_Lean_Name_mkStr3(x_1, x_2, x_3);
return x_4;
}
}
static lean_object* _init_l___regBuiltin_Std_Tactic_elabShowTerm___closed__5() {
static lean_object* _init_l___regBuiltin_Std_Tactic_elabShowTerm___closed__3() {
_start:
{
lean_object* x_1;
@ -883,7 +749,7 @@ x_1 = l_Lean_Elab_Term_termElabAttribute;
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Std_Tactic_elabShowTerm___closed__6() {
static lean_object* _init_l___regBuiltin_Std_Tactic_elabShowTerm___closed__4() {
_start:
{
lean_object* x_1;
@ -895,10 +761,10 @@ LEAN_EXPORT lean_object* l___regBuiltin_Std_Tactic_elabShowTerm(lean_object* x_1
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = l___regBuiltin_Std_Tactic_elabShowTerm___closed__5;
x_3 = l___regBuiltin_Std_Tactic_elabShowTerm___closed__2;
x_4 = l___regBuiltin_Std_Tactic_elabShowTerm___closed__4;
x_5 = l___regBuiltin_Std_Tactic_elabShowTerm___closed__6;
x_2 = l___regBuiltin_Std_Tactic_elabShowTerm___closed__3;
x_3 = l_Std_Tactic_elabShowTerm___closed__3;
x_4 = l___regBuiltin_Std_Tactic_elabShowTerm___closed__2;
x_5 = l___regBuiltin_Std_Tactic_elabShowTerm___closed__4;
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
@ -915,7 +781,7 @@ LEAN_EXPORT lean_object* l___regBuiltin_Std_Tactic_elabShowTerm_docString(lean_o
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l___regBuiltin_Std_Tactic_elabShowTerm___closed__4;
x_2 = l___regBuiltin_Std_Tactic_elabShowTerm___closed__2;
x_3 = l___regBuiltin_Std_Tactic_elabShowTerm_docString___closed__1;
x_4 = l_Lean_addBuiltinDocString(x_2, x_3, x_1);
return x_4;
@ -925,7 +791,7 @@ static lean_object* _init_l___regBuiltin_Std_Tactic_elabShowTerm_declRange___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(21u);
x_1 = lean_unsigned_to_nat(22u);
x_2 = lean_unsigned_to_nat(38u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -937,7 +803,7 @@ static lean_object* _init_l___regBuiltin_Std_Tactic_elabShowTerm_declRange___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(27u);
x_1 = lean_unsigned_to_nat(28u);
x_2 = lean_unsigned_to_nat(34u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -965,7 +831,7 @@ static lean_object* _init_l___regBuiltin_Std_Tactic_elabShowTerm_declRange___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(21u);
x_1 = lean_unsigned_to_nat(22u);
x_2 = lean_unsigned_to_nat(42u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -977,7 +843,7 @@ static lean_object* _init_l___regBuiltin_Std_Tactic_elabShowTerm_declRange___clo
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(21u);
x_1 = lean_unsigned_to_nat(22u);
x_2 = lean_unsigned_to_nat(54u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1017,13 +883,12 @@ LEAN_EXPORT lean_object* l___regBuiltin_Std_Tactic_elabShowTerm_declRange(lean_o
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l___regBuiltin_Std_Tactic_elabShowTerm___closed__4;
x_2 = l___regBuiltin_Std_Tactic_elabShowTerm___closed__2;
x_3 = l___regBuiltin_Std_Tactic_elabShowTerm_declRange___closed__7;
x_4 = l_Lean_addBuiltinDeclarationRanges(x_2, x_3, x_1);
return x_4;
}
}
lean_object* initialize_Init(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Elab_ElabRules(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_TryThis(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
@ -1031,9 +896,6 @@ LEAN_EXPORT lean_object* initialize_Lean_Elab_Tactic_ShowTerm(uint8_t builtin, l
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_ElabRules(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
@ -1092,14 +954,6 @@ l_Std_Tactic_elabShowTerm___closed__3 = _init_l_Std_Tactic_elabShowTerm___closed
lean_mark_persistent(l_Std_Tactic_elabShowTerm___closed__3);
l_Std_Tactic_elabShowTerm___closed__4 = _init_l_Std_Tactic_elabShowTerm___closed__4();
lean_mark_persistent(l_Std_Tactic_elabShowTerm___closed__4);
l_Std_Tactic_elabShowTerm___closed__5 = _init_l_Std_Tactic_elabShowTerm___closed__5();
lean_mark_persistent(l_Std_Tactic_elabShowTerm___closed__5);
l_Std_Tactic_elabShowTerm___closed__6 = _init_l_Std_Tactic_elabShowTerm___closed__6();
lean_mark_persistent(l_Std_Tactic_elabShowTerm___closed__6);
l_Std_Tactic_elabShowTerm___closed__7 = _init_l_Std_Tactic_elabShowTerm___closed__7();
lean_mark_persistent(l_Std_Tactic_elabShowTerm___closed__7);
l_Std_Tactic_elabShowTerm___closed__8 = _init_l_Std_Tactic_elabShowTerm___closed__8();
lean_mark_persistent(l_Std_Tactic_elabShowTerm___closed__8);
l___regBuiltin_Std_Tactic_elabShowTerm___closed__1 = _init_l___regBuiltin_Std_Tactic_elabShowTerm___closed__1();
lean_mark_persistent(l___regBuiltin_Std_Tactic_elabShowTerm___closed__1);
l___regBuiltin_Std_Tactic_elabShowTerm___closed__2 = _init_l___regBuiltin_Std_Tactic_elabShowTerm___closed__2();
@ -1108,10 +962,6 @@ l___regBuiltin_Std_Tactic_elabShowTerm___closed__3 = _init_l___regBuiltin_Std_Ta
lean_mark_persistent(l___regBuiltin_Std_Tactic_elabShowTerm___closed__3);
l___regBuiltin_Std_Tactic_elabShowTerm___closed__4 = _init_l___regBuiltin_Std_Tactic_elabShowTerm___closed__4();
lean_mark_persistent(l___regBuiltin_Std_Tactic_elabShowTerm___closed__4);
l___regBuiltin_Std_Tactic_elabShowTerm___closed__5 = _init_l___regBuiltin_Std_Tactic_elabShowTerm___closed__5();
lean_mark_persistent(l___regBuiltin_Std_Tactic_elabShowTerm___closed__5);
l___regBuiltin_Std_Tactic_elabShowTerm___closed__6 = _init_l___regBuiltin_Std_Tactic_elabShowTerm___closed__6();
lean_mark_persistent(l___regBuiltin_Std_Tactic_elabShowTerm___closed__6);
if (builtin) {res = l___regBuiltin_Std_Tactic_elabShowTerm(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

2442
stage0/stdlib/Lean/Meta/Tactic/LibrarySearch.c generated
View file

File diff suppressed because it is too large Load diff

1438
stage0/stdlib/Lean/Parser/Do.c generated
View file

File diff suppressed because it is too large Load diff

2586
stage0/stdlib/Lean/Parser/Term.c generated
View file

File diff suppressed because it is too large Load diff

399
stage0/stdlib/Lean/Server/Watchdog.c generated
View file

@ -170,6 +170,7 @@ static lean_object* l_Lean_Server_Watchdog_mkLeanServerCapabilities___closed__18
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Server_Watchdog_handleCallHierarchyOutgoingCalls___spec__7___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_HashMapImp_find_x3f___at_Lean_Server_Watchdog_handleCallHierarchyOutgoingCalls_collapseSameOutgoingCalls___spec__3(lean_object*, lean_object*);
static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__31;
static lean_object* l_Lean_Server_Watchdog_startLoadingReferences___closed__1;
static lean_object* l_IO_FS_Stream_readNotificationAs___at_Lean_Server_Watchdog_initAndRunWatchdogAux___spec__2___closed__1;
static lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_startFileWorker___spec__2___closed__1;
static lean_object* l_Lean_Server_Watchdog_startFileWorker___closed__4;
@ -287,6 +288,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handle
lean_object* l_IO_FS_Stream_readLspMessage(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_RBNode_erase___at_Lean_Server_Watchdog_FileWorker_erasePendingRequest___spec__1(lean_object*, lean_object*);
static lean_object* l_Lean_Server_Watchdog_mainLoop___closed__5;
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_startLoadingReferences___lambda__2(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_Watchdog_forwardRequestToWorker___closed__1;
static lean_object* l_Lean_Server_Watchdog_parseParams___rarg___closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_fromJsonCallHierarchyItemData____x40_Lean_Server_Watchdog___hyg_3453_(lean_object*);
@ -308,7 +310,6 @@ lean_object* lean_io_wait_any(lean_object*, lean_object*);
static lean_object* l_Lean_Server_Watchdog_initAndRunWatchdogAux___closed__2;
static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__44;
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Server_Watchdog_handleCallHierarchyOutgoingCalls___spec__7___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_loadReferences___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handleCallHierarchyIncomingCalls_collapseSameIncomingCalls___spec__18(size_t, size_t, lean_object*);
static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__64;
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_findWorkerPath___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
@ -366,7 +367,6 @@ static lean_object* l_Lean_Server_Watchdog_findWorkerPath___lambda__2___closed__
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handleRequest___spec__11___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_get_stdin(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_handleCallHierarchyIncomingCalls_collapseSameIncomingCalls___lambda__1(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_loadReferences(lean_object*);
lean_object* l___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonDidChangeTextDocumentParams____x40_Lean_Data_Lsp_TextSync___hyg_547_(lean_object*);
lean_object* l_System_FilePath_addExtension(lean_object*, lean_object*);
lean_object* lean_get_stderr(lean_object*);
@ -414,6 +414,7 @@ static lean_object* l_Lean_Server_Watchdog_handleRequest___lambda__1___closed__5
lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonCancelParams____x40_Lean_Data_Lsp_Basic___hyg_87_(lean_object*);
lean_object* l_Lean_Server_RequestError_toLspResponseError(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_workerCfg;
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_startLoadingReferences___lambda__1(lean_object*);
static lean_object* l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_fromJsonCallHierarchyItemData____x40_Lean_Server_Watchdog___hyg_3453____closed__8;
lean_object* l_Lean_Server_Ilean_load(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handleCallHierarchyOutgoingCalls___spec__1(size_t, size_t, lean_object*);
@ -511,7 +512,6 @@ LEAN_EXPORT lean_object* l_Array_filterMapM___at_Lean_Server_Watchdog_handlePrep
lean_object* l_IO_FS_Stream_readMessage(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handleCallHierarchyOutgoingCalls_collapseSameOutgoingCalls___spec__18___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__36;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_loadReferences___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_RBNode_forIn_visit___at_Lean_Server_Watchdog_shutdown___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_FileWorker_erasePendingRequest(lean_object*, lean_object*, lean_object*);
lean_object* l_IO_FS_Stream_writeLspMessage(lean_object*, lean_object*, lean_object*);
@ -675,6 +675,7 @@ lean_object* l_List_redLength___rarg(lean_object*);
lean_object* l_IO_FS_Stream_putStrLn(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_handleCallHierarchyOutgoingCalls_collapseSameOutgoingCalls___spec__13___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_handleDidClose(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_startLoadingReferences(lean_object*, lean_object*);
static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__51;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonWorkspaceSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3337_(lean_object*);
static lean_object* l_Lean_Server_Watchdog_handleRename___closed__2;
@ -698,6 +699,7 @@ extern lean_object* l_Lean_Lsp_instInhabitedCallHierarchyOutgoingCall;
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_handleCancelRequest(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
static lean_object* l_Lean_Server_Watchdog_handleRequest___lambda__1___closed__6;
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_startLoadingReferences___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_AssocList_foldlM___at_Lean_Server_Watchdog_handleCallHierarchyOutgoingCalls_collapseSameOutgoingCalls___spec__11(lean_object*, lean_object*);
extern lean_object* l_Lean_Lsp_instInhabitedCallHierarchyIncomingCall;
lean_object* lean_int_neg(lean_object*);
@ -707,6 +709,7 @@ uint8_t lean_nat_dec_le(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_Server_Watchdog_handleWorkspaceSymbol___spec__1___lambda__1___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__7;
uint8_t lean_usize_dec_lt(size_t, size_t);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_startLoadingReferences___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_Watchdog_mkLeanServerCapabilities___closed__10;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_handleDidChangeWatchedFiles___spec__3(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_filterMapM___at_Lean_Server_Watchdog_handlePrepareCallHierarchy___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -745,6 +748,7 @@ lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Server_Watchdog_handleCallHierarchyOutgoingCalls___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_Watchdog_handleRename___lambda__1___closed__3;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_tryWriteMessage___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_startLoadingReferences___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*);
static lean_object* l_Lean_Server_Watchdog_tryWriteMessage___closed__26;
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_handleIleanInfoUpdate(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonPrepareRenameParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_9752_(lean_object*);
@ -29894,138 +29898,229 @@ lean_dec(x_2);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_loadReferences___spec__1(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4, lean_object* x_5) {
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_startLoadingReferences___spec__1(lean_object* x_1, lean_object* x_2, size_t x_3, size_t x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
uint8_t x_6;
x_6 = lean_usize_dec_lt(x_3, x_2);
if (x_6 == 0)
uint8_t x_7;
x_7 = lean_usize_dec_lt(x_4, x_3);
if (x_7 == 0)
{
lean_object* x_7;
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_4);
lean_ctor_set(x_7, 1, x_5);
return x_7;
lean_object* x_8;
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_5);
lean_ctor_set(x_8, 1, x_6);
return x_8;
}
else
{
lean_object* x_8; lean_object* x_9;
x_8 = lean_array_uget(x_1, x_3);
x_9 = l_Lean_Server_Ilean_load(x_8, x_5);
if (lean_obj_tag(x_9) == 0)
lean_object* x_9; lean_object* x_10;
lean_dec(x_5);
x_9 = lean_array_uget(x_2, x_4);
x_10 = l_Lean_Server_Ilean_load(x_9, x_6);
if (lean_obj_tag(x_10) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; size_t x_13; size_t x_14;
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; size_t x_19; size_t x_20; lean_object* x_21;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
lean_dec(x_9);
x_12 = l_Lean_Server_References_addIlean(x_4, x_8, x_10);
x_13 = 1;
x_14 = lean_usize_add(x_3, x_13);
x_3 = x_14;
x_4 = x_12;
x_5 = x_11;
x_12 = lean_ctor_get(x_10, 1);
lean_inc(x_12);
lean_dec(x_10);
x_13 = lean_st_ref_take(x_1, x_12);
x_14 = lean_ctor_get(x_13, 0);
lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 1);
lean_inc(x_15);
lean_dec(x_13);
x_16 = l_Lean_Server_References_addIlean(x_14, x_9, x_11);
x_17 = lean_st_ref_set(x_1, x_16, x_15);
x_18 = lean_ctor_get(x_17, 1);
lean_inc(x_18);
lean_dec(x_17);
x_19 = 1;
x_20 = lean_usize_add(x_4, x_19);
x_21 = lean_box(0);
x_4 = x_20;
x_5 = x_21;
x_6 = x_18;
goto _start;
}
else
{
lean_object* x_16; size_t x_17; size_t x_18;
lean_dec(x_8);
x_16 = lean_ctor_get(x_9, 1);
lean_inc(x_16);
lean_object* x_23; size_t x_24; size_t x_25; lean_object* x_26;
lean_dec(x_9);
x_17 = 1;
x_18 = lean_usize_add(x_3, x_17);
x_3 = x_18;
x_5 = x_16;
x_23 = lean_ctor_get(x_10, 1);
lean_inc(x_23);
lean_dec(x_10);
x_24 = 1;
x_25 = lean_usize_add(x_4, x_24);
x_26 = lean_box(0);
x_4 = x_25;
x_5 = x_26;
x_6 = x_23;
goto _start;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_loadReferences(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_startLoadingReferences___lambda__1(lean_object* x_1) {
_start:
{
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_2; lean_object* x_3; uint8_t x_4;
x_2 = l_Lean_Server_Watchdog_handleDidChangeWatchedFiles___closed__1;
x_3 = lean_st_ref_get(x_2, x_1);
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_ctor_get(x_3, 1);
x_4 = !lean_is_exclusive(x_3);
if (x_4 == 0)
{
return x_3;
}
else
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = lean_ctor_get(x_3, 0);
x_6 = lean_ctor_get(x_3, 1);
lean_inc(x_6);
lean_inc(x_5);
lean_dec(x_3);
x_6 = l_Lean_Server_Watchdog_handleDidChangeWatchedFiles___closed__2;
x_7 = l_Lean_SearchPath_findAllWithExt(x_4, x_6, x_5);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; size_t x_11; size_t x_12; lean_object* x_13; lean_object* x_14; uint8_t x_15;
x_8 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
x_9 = lean_ctor_get(x_7, 1);
lean_inc(x_9);
lean_dec(x_7);
x_10 = lean_array_get_size(x_8);
x_11 = lean_usize_of_nat(x_10);
lean_dec(x_10);
x_12 = 0;
x_13 = l_Lean_Server_References_empty;
x_14 = l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_loadReferences___spec__1(x_8, x_11, x_12, x_13, x_9);
lean_dec(x_8);
x_15 = !lean_is_exclusive(x_14);
if (x_15 == 0)
{
return x_14;
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_16 = lean_ctor_get(x_14, 0);
x_17 = lean_ctor_get(x_14, 1);
lean_inc(x_17);
lean_inc(x_16);
lean_dec(x_14);
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_16);
lean_ctor_set(x_18, 1, x_17);
return x_18;
}
}
else
{
uint8_t x_19;
x_19 = !lean_is_exclusive(x_7);
if (x_19 == 0)
{
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_5);
lean_ctor_set(x_7, 1, x_6);
return x_7;
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_20 = lean_ctor_get(x_7, 0);
x_21 = lean_ctor_get(x_7, 1);
lean_inc(x_21);
lean_inc(x_20);
lean_dec(x_7);
x_22 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
return x_22;
}
}
}
}
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_loadReferences___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_startLoadingReferences___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
size_t x_6; size_t x_7; lean_object* x_8;
x_6 = lean_unbox_usize(x_2);
lean_dec(x_2);
lean_object* x_4; lean_object* x_5;
x_4 = l_Lean_Server_Watchdog_handleDidChangeWatchedFiles___closed__2;
x_5 = l_Lean_SearchPath_findAllWithExt(x_2, x_4, x_3);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; size_t x_9; size_t x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_6 = lean_ctor_get(x_5, 0);
lean_inc(x_6);
x_7 = lean_ctor_get(x_5, 1);
lean_inc(x_7);
lean_dec(x_5);
x_8 = lean_array_get_size(x_6);
x_9 = lean_usize_of_nat(x_8);
lean_dec(x_8);
x_10 = 0;
x_11 = lean_box(0);
x_12 = l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_startLoadingReferences___spec__1(x_1, x_6, x_9, x_10, x_11, x_7);
lean_dec(x_6);
x_13 = !lean_is_exclusive(x_12);
if (x_13 == 0)
{
lean_object* x_14;
x_14 = lean_ctor_get(x_12, 0);
lean_dec(x_14);
lean_ctor_set(x_12, 0, x_11);
return x_12;
}
else
{
lean_object* x_15; lean_object* x_16;
x_15 = lean_ctor_get(x_12, 1);
lean_inc(x_15);
lean_dec(x_12);
x_16 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_16, 0, x_11);
lean_ctor_set(x_16, 1, x_15);
return x_16;
}
}
else
{
uint8_t x_17;
x_17 = !lean_is_exclusive(x_5);
if (x_17 == 0)
{
return x_5;
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_18 = lean_ctor_get(x_5, 0);
x_19 = lean_ctor_get(x_5, 1);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_5);
x_20 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_20, 0, x_18);
lean_ctor_set(x_20, 1, x_19);
return x_20;
}
}
}
}
static lean_object* _init_l_Lean_Server_Watchdog_startLoadingReferences___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Server_Watchdog_startLoadingReferences___lambda__1), 1, 0);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_startLoadingReferences(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; lean_object* x_8; uint8_t x_9;
x_3 = lean_alloc_closure((void*)(l_Lean_Server_Watchdog_startLoadingReferences___lambda__2___boxed), 3, 1);
lean_closure_set(x_3, 0, x_1);
x_4 = l_Lean_Server_Watchdog_startLoadingReferences___closed__1;
x_5 = lean_alloc_closure((void*)(l_EStateM_bind___rarg), 3, 2);
lean_closure_set(x_5, 0, x_4);
lean_closure_set(x_5, 1, x_3);
x_6 = lean_alloc_closure((void*)(l_EIO_toBaseIO___rarg), 2, 1);
lean_closure_set(x_6, 0, x_5);
x_7 = l_Task_Priority_default;
x_8 = lean_io_as_task(x_6, x_7, x_2);
x_9 = !lean_is_exclusive(x_8);
if (x_9 == 0)
{
lean_object* x_10; lean_object* x_11;
x_10 = lean_ctor_get(x_8, 0);
lean_dec(x_10);
x_11 = lean_box(0);
lean_ctor_set(x_8, 0, x_11);
return x_8;
}
else
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = lean_ctor_get(x_8, 1);
lean_inc(x_12);
lean_dec(x_8);
x_13 = lean_box(0);
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_12);
return x_14;
}
}
}
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_startLoadingReferences___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
size_t x_7; size_t x_8; lean_object* x_9;
x_7 = lean_unbox_usize(x_3);
lean_dec(x_3);
x_8 = l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_loadReferences___spec__1(x_1, x_6, x_7, x_4, x_5);
x_8 = lean_unbox_usize(x_4);
lean_dec(x_4);
x_9 = l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_startLoadingReferences___spec__1(x_1, x_2, x_7, x_8, x_5, x_6);
lean_dec(x_2);
lean_dec(x_1);
return x_8;
return x_9;
}
}
LEAN_EXPORT lean_object* l_Lean_Server_Watchdog_startLoadingReferences___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Server_Watchdog_startLoadingReferences___lambda__2(x_1, x_2, x_3);
lean_dec(x_1);
return x_4;
}
}
static lean_object* _init_l_IO_FS_Stream_readRequestAs___at_Lean_Server_Watchdog_initAndRunWatchdog___spec__2___closed__1() {
@ -32389,27 +32484,24 @@ x_9 = lean_box(0);
x_10 = l_Lean_initSrcSearchPath(x_9, x_8);
if (lean_obj_tag(x_10) == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24; lean_object* x_25;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_10, 1);
lean_inc(x_12);
lean_dec(x_10);
x_13 = l_Lean_Server_Watchdog_loadReferences(x_12);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24; lean_object* x_25;
x_14 = lean_ctor_get(x_13, 0);
lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 1);
x_13 = l_Lean_Server_References_empty;
x_14 = lean_st_mk_ref(x_13, x_12);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
lean_dec(x_13);
x_16 = lean_st_mk_ref(x_14, x_15);
x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
x_18 = lean_ctor_get(x_16, 1);
x_16 = lean_ctor_get(x_14, 1);
lean_inc(x_16);
lean_dec(x_14);
lean_inc(x_15);
x_17 = l_Lean_Server_Watchdog_startLoadingReferences(x_15, x_16);
x_18 = lean_ctor_get(x_17, 1);
lean_inc(x_18);
lean_dec(x_16);
lean_dec(x_17);
x_19 = lean_box(0);
x_20 = lean_st_mk_ref(x_19, x_18);
x_21 = lean_ctor_get(x_20, 0);
@ -32495,7 +32587,7 @@ lean_ctor_set(x_50, 4, x_21);
lean_ctor_set(x_50, 5, x_42);
lean_ctor_set(x_50, 6, x_7);
lean_ctor_set(x_50, 7, x_11);
lean_ctor_set(x_50, 8, x_17);
lean_ctor_set(x_50, 8, x_15);
x_51 = l_Lean_Server_Watchdog_initAndRunWatchdogAux(x_50, x_49);
return x_51;
}
@ -32507,7 +32599,7 @@ lean_dec(x_35);
lean_dec(x_31);
lean_dec(x_26);
lean_dec(x_21);
lean_dec(x_17);
lean_dec(x_15);
lean_dec(x_11);
lean_dec(x_7);
lean_dec(x_1);
@ -32539,7 +32631,7 @@ lean_dec(x_35);
lean_dec(x_31);
lean_dec(x_26);
lean_dec(x_21);
lean_dec(x_17);
lean_dec(x_15);
lean_dec(x_11);
lean_dec(x_7);
lean_dec(x_1);
@ -32570,7 +32662,7 @@ lean_dec(x_35);
lean_dec(x_31);
lean_dec(x_26);
lean_dec(x_21);
lean_dec(x_17);
lean_dec(x_15);
lean_dec(x_11);
lean_dec(x_7);
lean_dec(x_1);
@ -32600,7 +32692,7 @@ uint8_t x_64;
lean_dec(x_31);
lean_dec(x_26);
lean_dec(x_21);
lean_dec(x_17);
lean_dec(x_15);
lean_dec(x_11);
lean_dec(x_7);
lean_dec(x_1);
@ -32629,7 +32721,7 @@ else
uint8_t x_68;
lean_dec(x_26);
lean_dec(x_21);
lean_dec(x_17);
lean_dec(x_15);
lean_dec(x_11);
lean_dec(x_7);
lean_dec(x_4);
@ -32658,7 +32750,7 @@ else
{
uint8_t x_72;
lean_dec(x_21);
lean_dec(x_17);
lean_dec(x_15);
lean_dec(x_11);
lean_dec(x_7);
lean_dec(x_4);
@ -32687,25 +32779,24 @@ return x_75;
else
{
uint8_t x_76;
lean_dec(x_11);
lean_dec(x_7);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_76 = !lean_is_exclusive(x_13);
x_76 = !lean_is_exclusive(x_10);
if (x_76 == 0)
{
return x_13;
return x_10;
}
else
{
lean_object* x_77; lean_object* x_78; lean_object* x_79;
x_77 = lean_ctor_get(x_13, 0);
x_78 = lean_ctor_get(x_13, 1);
x_77 = lean_ctor_get(x_10, 0);
x_78 = lean_ctor_get(x_10, 1);
lean_inc(x_78);
lean_inc(x_77);
lean_dec(x_13);
lean_dec(x_10);
x_79 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_79, 0, x_77);
lean_ctor_set(x_79, 1, x_78);
@ -32716,55 +32807,27 @@ return x_79;
else
{
uint8_t x_80;
lean_dec(x_7);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_80 = !lean_is_exclusive(x_10);
x_80 = !lean_is_exclusive(x_6);
if (x_80 == 0)
{
return x_10;
}
else
{
lean_object* x_81; lean_object* x_82; lean_object* x_83;
x_81 = lean_ctor_get(x_10, 0);
x_82 = lean_ctor_get(x_10, 1);
lean_inc(x_82);
lean_inc(x_81);
lean_dec(x_10);
x_83 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_83, 0, x_81);
lean_ctor_set(x_83, 1, x_82);
return x_83;
}
}
}
else
{
uint8_t x_84;
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_84 = !lean_is_exclusive(x_6);
if (x_84 == 0)
{
return x_6;
}
else
{
lean_object* x_85; lean_object* x_86; lean_object* x_87;
x_85 = lean_ctor_get(x_6, 0);
x_86 = lean_ctor_get(x_6, 1);
lean_inc(x_86);
lean_inc(x_85);
lean_object* x_81; lean_object* x_82; lean_object* x_83;
x_81 = lean_ctor_get(x_6, 0);
x_82 = lean_ctor_get(x_6, 1);
lean_inc(x_82);
lean_inc(x_81);
lean_dec(x_6);
x_87 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_87, 0, x_85);
lean_ctor_set(x_87, 1, x_86);
return x_87;
x_83 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_83, 0, x_81);
lean_ctor_set(x_83, 1, x_82);
return x_83;
}
}
}
@ -33362,6 +33425,8 @@ l_Lean_Server_Watchdog_findWorkerPath___closed__2 = _init_l_Lean_Server_Watchdog
lean_mark_persistent(l_Lean_Server_Watchdog_findWorkerPath___closed__2);
l_Lean_Server_Watchdog_findWorkerPath___closed__3 = _init_l_Lean_Server_Watchdog_findWorkerPath___closed__3();
lean_mark_persistent(l_Lean_Server_Watchdog_findWorkerPath___closed__3);
l_Lean_Server_Watchdog_startLoadingReferences___closed__1 = _init_l_Lean_Server_Watchdog_startLoadingReferences___closed__1();
lean_mark_persistent(l_Lean_Server_Watchdog_startLoadingReferences___closed__1);
l_IO_FS_Stream_readRequestAs___at_Lean_Server_Watchdog_initAndRunWatchdog___spec__2___closed__1 = _init_l_IO_FS_Stream_readRequestAs___at_Lean_Server_Watchdog_initAndRunWatchdog___spec__2___closed__1();
lean_mark_persistent(l_IO_FS_Stream_readRequestAs___at_Lean_Server_Watchdog_initAndRunWatchdog___spec__2___closed__1);
l_IO_FS_Stream_readRequestAs___at_Lean_Server_Watchdog_initAndRunWatchdog___spec__2___closed__2 = _init_l_IO_FS_Stream_readRequestAs___at_Lean_Server_Watchdog_initAndRunWatchdog___spec__2___closed__2();