Skip to content

Instantly share code, notes, and snippets.

@pnwamk

pnwamk/Arith.c

Last active September 11, 2020 21:00
Show Gist options
  • Save pnwamk/3a82034a9d00223dcab59558798d3c4d to your computer and use it in GitHub Desktop.
Save pnwamk/3a82034a9d00223dcab59558798d3c4d to your computer and use it in GitHub Desktop.
Download ZIP
Arith.lean => C
Raw
Arith.c
// Lean compiler output
// Module: Arith
// Imports: Init
#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_object *l_IO_println___at_main___spec__1(lean_object *, lean_object *);
double l_main___closed__2;
lean_object *l_IO_println___at_main___spec__5(uint64_t, lean_object *);
lean_object *l_IO_println___at_main___spec__3___boxed(lean_object *,
lean_object *);
uint64_t l_UInt64_add(uint64_t, uint64_t);
double lean_float_of_nat(lean_object *);
lean_object *_lean_main(lean_object *);
extern lean_object *l_Prod_HasRepr___rarg___closed__1;
double l_HasPowFloatNat(double, lean_object *);
lean_object *l_main___closed__6;
lean_object *l_addInts(lean_object *, lean_object *);
double l_main___closed__3;
lean_object *l_IO_println___at_main___spec__3(lean_object *, lean_object *);
lean_object *lean_string_append(lean_object *, lean_object *);
double sqrt(double);
lean_object *l_quadraticFormula(double, double, double);
double l_main___closed__5;
lean_object *l_addFloats___boxed(lean_object *, lean_object *);
extern lean_object *l_Int_zero;
lean_object *lean_nat_add(lean_object *, lean_object *);
double l_FloatHasNeg(double);
double l_main___closed__4;
lean_object *l_Int_repr(lean_object *);
lean_object *l_addUInt64s___boxed(lean_object *, lean_object *);
extern lean_object *l_IO_FS_Handle_putStrLn___rarg___closed__1;
lean_object *l_IO_println___at_main___spec__5___boxed(lean_object *,
lean_object *);
lean_object *l_IO_print___at_main___spec__4(lean_object *, lean_object *);
extern double l_Float_HasZero___closed__1;
lean_object *l_IO_println___at_main___spec__7(double, lean_object *);
lean_object *l_main___closed__1;
lean_object *lean_float_to_string(double);
lean_object *l_IO_print___at_main___spec__2(lean_object *, lean_object *);
lean_object *l_Nat_repr(lean_object *);
double l_Float_div(double, double);
extern lean_object *l_List_reprAux___main___rarg___closed__1;
lean_object *l_IO_print___at_main___spec__6___boxed(lean_object *,
lean_object *);
double l_Float_sub(double, double);
lean_object *l_FloatHasNeg___boxed(lean_object *);
double l_Float_add(double, double);
extern double l_Float_HasOne___closed__1;
lean_object *l_HasPowFloatNat___boxed(lean_object *, lean_object *);
lean_object *l_IO_print___at_main___spec__4___boxed(lean_object *,
lean_object *);
extern lean_object *l_Option_HasRepr___rarg___closed__3;
lean_object *l_addInts___boxed(lean_object *, lean_object *);
lean_object *l_IO_print___at_main___spec__8___boxed(lean_object *,
lean_object *);
extern lean_object *l_Int_one;
double pow(double, double);
lean_object *l_IO_println___at_main___spec__7___boxed(lean_object *,
lean_object *);
double l_addFloats(double, double);
lean_object *lean_get_stdout(lean_object *);
lean_object *l_IO_print___at_main___spec__6(uint64_t, lean_object *);
double l_quadraticFormula___closed__2;
lean_object *l_IO_println___at_main___spec__9(lean_object *, lean_object *);
lean_object *lean_uint64_to_nat(uint64_t);
lean_object *l_IO_print___at_main___spec__10(lean_object *, lean_object *);
lean_object *
l_IO_print___at___private_Init_System_IO_1__printlnAux___spec__2(lean_object *,
lean_object *);
lean_object *l_addNats(lean_object *, lean_object *);
lean_object *lean_int_add(lean_object *, lean_object *);
lean_object *l_quadraticFormula___boxed(lean_object *, lean_object *,
lean_object *);
uint64_t l_addUInt64s(uint64_t, uint64_t);
double l_quadraticFormula___closed__1;
lean_object *l_addNats___boxed(lean_object *, lean_object *);
lean_object *l_IO_print___at_main___spec__8(double, lean_object *);
double l_quadraticFormula___closed__3;
double l_Float_mul(double, double);
double l_FloatHasNeg(double x_1) {
_start : {
double x_2;
double x_3;
x_2 = l_Float_HasZero___closed__1;
x_3 = x_2 - x_1;
return x_3;
}
}
lean_object *l_FloatHasNeg___boxed(lean_object *x_1) {
_start : {
double x_2;
double x_3;
lean_object *x_4;
x_2 = lean_unbox_float(x_1);
lean_dec(x_1);
x_3 = l_FloatHasNeg(x_2);
x_4 = lean_box_float(x_3);
return x_4;
}
}
double l_HasPowFloatNat(double x_1, lean_object *x_2) {
_start : {
double x_3;
double x_4;
x_3 = lean_float_of_nat(x_2);
x_4 = pow(x_1, x_3);
return x_4;
}
}
lean_object *l_HasPowFloatNat___boxed(lean_object *x_1, lean_object *x_2) {
_start : {
double x_3;
double x_4;
lean_object *x_5;
x_3 = lean_unbox_float(x_1);
lean_dec(x_1);
x_4 = l_HasPowFloatNat(x_3, x_2);
lean_dec(x_2);
x_5 = lean_box_float(x_4);
return x_5;
}
}
lean_object *l_addNats(lean_object *x_1, lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = lean_nat_add(x_1, x_2);
return x_3;
}
}
lean_object *l_addNats___boxed(lean_object *x_1, lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = l_addNats(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object *l_addInts(lean_object *x_1, lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = lean_int_add(x_1, x_2);
return x_3;
}
}
lean_object *l_addInts___boxed(lean_object *x_1, lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = l_addInts(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
uint64_t l_addUInt64s(uint64_t x_1, uint64_t x_2) {
_start : {
uint64_t x_3;
x_3 = x_1 + x_2;
return x_3;
}
}
lean_object *l_addUInt64s___boxed(lean_object *x_1, lean_object *x_2) {
_start : {
uint64_t x_3;
uint64_t x_4;
uint64_t x_5;
lean_object *x_6;
x_3 = lean_unbox_uint64(x_1);
lean_dec(x_1);
x_4 = lean_unbox_uint64(x_2);
lean_dec(x_2);
x_5 = l_addUInt64s(x_3, x_4);
x_6 = lean_box_uint64(x_5);
return x_6;
}
}
double l_addFloats(double x_1, double x_2) {
_start : {
double x_3;
x_3 = x_1 + x_2;
return x_3;
}
}
lean_object *l_addFloats___boxed(lean_object *x_1, lean_object *x_2) {
_start : {
double x_3;
double x_4;
double x_5;
lean_object *x_6;
x_3 = lean_unbox_float(x_1);
lean_dec(x_1);
x_4 = lean_unbox_float(x_2);
lean_dec(x_2);
x_5 = l_addFloats(x_3, x_4);
x_6 = lean_box_float(x_5);
return x_6;
}
}
double _init_l_quadraticFormula___closed__1() {
_start : {
lean_object *x_1;
double x_2;
x_1 = lean_unsigned_to_nat(2u);
x_2 = lean_float_of_nat(x_1);
return x_2;
}
}
double _init_l_quadraticFormula___closed__2() {
_start : {
double x_1;
double x_2;
x_1 = l_Float_HasOne___closed__1;
x_2 = x_1 + x_1;
return x_2;
}
}
double _init_l_quadraticFormula___closed__3() {
_start : {
double x_1;
double x_2;
x_1 = l_quadraticFormula___closed__2;
x_2 = x_1 + x_1;
return x_2;
}
}
lean_object *l_quadraticFormula(double x_1, double x_2, double x_3) {
_start : {
double x_4;
double x_5;
double x_6;
double x_7;
double x_8;
double x_9;
double x_10;
double x_11;
double x_12;
double x_13;
double x_14;
double x_15;
double x_16;
double x_17;
double x_18;
lean_object *x_19;
lean_object *x_20;
lean_object *x_21;
x_4 = l_Float_HasZero___closed__1;
x_5 = x_4 - x_2;
x_6 = l_quadraticFormula___closed__1;
x_7 = pow(x_2, x_6);
x_8 = l_quadraticFormula___closed__3;
x_9 = x_8 * x_1;
x_10 = x_9 * x_3;
x_11 = x_7 - x_10;
x_12 = sqrt(x_11);
x_13 = x_5 + x_12;
x_14 = l_quadraticFormula___closed__2;
x_15 = x_14 * x_1;
x_16 = x_13 / x_15;
x_17 = x_5 - x_12;
x_18 = x_17 / x_15;
x_19 = lean_box_float(x_16);
x_20 = lean_box_float(x_18);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
return x_21;
}
}
lean_object *l_quadraticFormula___boxed(lean_object *x_1, lean_object *x_2,
lean_object *x_3) {
_start : {
double x_4;
double x_5;
double x_6;
lean_object *x_7;
x_4 = lean_unbox_float(x_1);
lean_dec(x_1);
x_5 = lean_unbox_float(x_2);
lean_dec(x_2);
x_6 = lean_unbox_float(x_3);
lean_dec(x_3);
x_7 = l_quadraticFormula(x_4, x_5, x_6);
return x_7;
}
}
lean_object *l_IO_print___at_main___spec__2(lean_object *x_1,
lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = lean_get_stdout(x_2);
if (lean_obj_tag(x_3) == 0) {
lean_object *x_4;
lean_object *x_5;
lean_object *x_6;
lean_object *x_7;
lean_object *x_8;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_ctor_get(x_3, 1);
lean_inc(x_5);
lean_dec(x_3);
x_6 = lean_ctor_get(x_4, 5);
lean_inc(x_6);
lean_dec(x_4);
x_7 = l_Nat_repr(x_1);
x_8 = lean_apply_2(x_6, x_7, x_5);
return x_8;
} else {
uint8_t x_9;
lean_dec(x_1);
x_9 = !lean_is_exclusive(x_3);
if (x_9 == 0) {
return x_3;
} else {
lean_object *x_10;
lean_object *x_11;
lean_object *x_12;
x_10 = lean_ctor_get(x_3, 0);
x_11 = lean_ctor_get(x_3, 1);
lean_inc(x_11);
lean_inc(x_10);
lean_dec(x_3);
x_12 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
return x_12;
}
}
}
}
lean_object *l_IO_println___at_main___spec__1(lean_object *x_1,
lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = l_IO_print___at_main___spec__2(x_1, x_2);
if (lean_obj_tag(x_3) == 0) {
lean_object *x_4;
lean_object *x_5;
lean_object *x_6;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = l_IO_FS_Handle_putStrLn___rarg___closed__1;
x_6 = l_IO_print___at___private_Init_System_IO_1__printlnAux___spec__2(x_5,
x_4);
return x_6;
} else {
uint8_t x_7;
x_7 = !lean_is_exclusive(x_3);
if (x_7 == 0) {
return x_3;
} else {
lean_object *x_8;
lean_object *x_9;
lean_object *x_10;
x_8 = lean_ctor_get(x_3, 0);
x_9 = lean_ctor_get(x_3, 1);
lean_inc(x_9);
lean_inc(x_8);
lean_dec(x_3);
x_10 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_10, 0, x_8);
lean_ctor_set(x_10, 1, x_9);
return x_10;
}
}
}
}
lean_object *l_IO_print___at_main___spec__4(lean_object *x_1,
lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = lean_get_stdout(x_2);
if (lean_obj_tag(x_3) == 0) {
lean_object *x_4;
lean_object *x_5;
lean_object *x_6;
lean_object *x_7;
lean_object *x_8;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_ctor_get(x_3, 1);
lean_inc(x_5);
lean_dec(x_3);
x_6 = lean_ctor_get(x_4, 5);
lean_inc(x_6);
lean_dec(x_4);
x_7 = l_Int_repr(x_1);
x_8 = lean_apply_2(x_6, x_7, x_5);
return x_8;
} else {
uint8_t x_9;
x_9 = !lean_is_exclusive(x_3);
if (x_9 == 0) {
return x_3;
} else {
lean_object *x_10;
lean_object *x_11;
lean_object *x_12;
x_10 = lean_ctor_get(x_3, 0);
x_11 = lean_ctor_get(x_3, 1);
lean_inc(x_11);
lean_inc(x_10);
lean_dec(x_3);
x_12 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
return x_12;
}
}
}
}
lean_object *l_IO_println___at_main___spec__3(lean_object *x_1,
lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = l_IO_print___at_main___spec__4(x_1, x_2);
if (lean_obj_tag(x_3) == 0) {
lean_object *x_4;
lean_object *x_5;
lean_object *x_6;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = l_IO_FS_Handle_putStrLn___rarg___closed__1;
x_6 = l_IO_print___at___private_Init_System_IO_1__printlnAux___spec__2(x_5,
x_4);
return x_6;
} else {
uint8_t x_7;
x_7 = !lean_is_exclusive(x_3);
if (x_7 == 0) {
return x_3;
} else {
lean_object *x_8;
lean_object *x_9;
lean_object *x_10;
x_8 = lean_ctor_get(x_3, 0);
x_9 = lean_ctor_get(x_3, 1);
lean_inc(x_9);
lean_inc(x_8);
lean_dec(x_3);
x_10 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_10, 0, x_8);
lean_ctor_set(x_10, 1, x_9);
return x_10;
}
}
}
}
lean_object *l_IO_print___at_main___spec__6(uint64_t x_1, lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = lean_get_stdout(x_2);
if (lean_obj_tag(x_3) == 0) {
lean_object *x_4;
lean_object *x_5;
lean_object *x_6;
lean_object *x_7;
lean_object *x_8;
lean_object *x_9;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_ctor_get(x_3, 1);
lean_inc(x_5);
lean_dec(x_3);
x_6 = lean_ctor_get(x_4, 5);
lean_inc(x_6);
lean_dec(x_4);
x_7 = lean_uint64_to_nat(x_1);
x_8 = l_Nat_repr(x_7);
x_9 = lean_apply_2(x_6, x_8, x_5);
return x_9;
} else {
uint8_t x_10;
x_10 = !lean_is_exclusive(x_3);
if (x_10 == 0) {
return x_3;
} else {
lean_object *x_11;
lean_object *x_12;
lean_object *x_13;
x_11 = lean_ctor_get(x_3, 0);
x_12 = lean_ctor_get(x_3, 1);
lean_inc(x_12);
lean_inc(x_11);
lean_dec(x_3);
x_13 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
return x_13;
}
}
}
}
lean_object *l_IO_println___at_main___spec__5(uint64_t x_1, lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = l_IO_print___at_main___spec__6(x_1, x_2);
if (lean_obj_tag(x_3) == 0) {
lean_object *x_4;
lean_object *x_5;
lean_object *x_6;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = l_IO_FS_Handle_putStrLn___rarg___closed__1;
x_6 = l_IO_print___at___private_Init_System_IO_1__printlnAux___spec__2(x_5,
x_4);
return x_6;
} else {
uint8_t x_7;
x_7 = !lean_is_exclusive(x_3);
if (x_7 == 0) {
return x_3;
} else {
lean_object *x_8;
lean_object *x_9;
lean_object *x_10;
x_8 = lean_ctor_get(x_3, 0);
x_9 = lean_ctor_get(x_3, 1);
lean_inc(x_9);
lean_inc(x_8);
lean_dec(x_3);
x_10 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_10, 0, x_8);
lean_ctor_set(x_10, 1, x_9);
return x_10;
}
}
}
}
lean_object *l_IO_print___at_main___spec__8(double x_1, lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = lean_get_stdout(x_2);
if (lean_obj_tag(x_3) == 0) {
lean_object *x_4;
lean_object *x_5;
lean_object *x_6;
lean_object *x_7;
lean_object *x_8;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_ctor_get(x_3, 1);
lean_inc(x_5);
lean_dec(x_3);
x_6 = lean_ctor_get(x_4, 5);
lean_inc(x_6);
lean_dec(x_4);
x_7 = lean_float_to_string(x_1);
x_8 = lean_apply_2(x_6, x_7, x_5);
return x_8;
} else {
uint8_t x_9;
x_9 = !lean_is_exclusive(x_3);
if (x_9 == 0) {
return x_3;
} else {
lean_object *x_10;
lean_object *x_11;
lean_object *x_12;
x_10 = lean_ctor_get(x_3, 0);
x_11 = lean_ctor_get(x_3, 1);
lean_inc(x_11);
lean_inc(x_10);
lean_dec(x_3);
x_12 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
return x_12;
}
}
}
}
lean_object *l_IO_println___at_main___spec__7(double x_1, lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = l_IO_print___at_main___spec__8(x_1, x_2);
if (lean_obj_tag(x_3) == 0) {
lean_object *x_4;
lean_object *x_5;
lean_object *x_6;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = l_IO_FS_Handle_putStrLn___rarg___closed__1;
x_6 = l_IO_print___at___private_Init_System_IO_1__printlnAux___spec__2(x_5,
x_4);
return x_6;
} else {
uint8_t x_7;
x_7 = !lean_is_exclusive(x_3);
if (x_7 == 0) {
return x_3;
} else {
lean_object *x_8;
lean_object *x_9;
lean_object *x_10;
x_8 = lean_ctor_get(x_3, 0);
x_9 = lean_ctor_get(x_3, 1);
lean_inc(x_9);
lean_inc(x_8);
lean_dec(x_3);
x_10 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_10, 0, x_8);
lean_ctor_set(x_10, 1, x_9);
return x_10;
}
}
}
}
lean_object *l_IO_print___at_main___spec__10(lean_object *x_1,
lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = lean_get_stdout(x_2);
if (lean_obj_tag(x_3) == 0) {
lean_object *x_4;
lean_object *x_5;
lean_object *x_6;
lean_object *x_7;
lean_object *x_8;
double x_9;
lean_object *x_10;
lean_object *x_11;
lean_object *x_12;
lean_object *x_13;
lean_object *x_14;
double x_15;
lean_object *x_16;
lean_object *x_17;
lean_object *x_18;
lean_object *x_19;
lean_object *x_20;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_ctor_get(x_3, 1);
lean_inc(x_5);
lean_dec(x_3);
x_6 = lean_ctor_get(x_4, 5);
lean_inc(x_6);
lean_dec(x_4);
x_7 = lean_ctor_get(x_1, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_1, 1);
lean_inc(x_8);
lean_dec(x_1);
x_9 = lean_unbox_float(x_7);
lean_dec(x_7);
x_10 = lean_float_to_string(x_9);
x_11 = l_Prod_HasRepr___rarg___closed__1;
x_12 = lean_string_append(x_11, x_10);
lean_dec(x_10);
x_13 = l_List_reprAux___main___rarg___closed__1;
x_14 = lean_string_append(x_12, x_13);
x_15 = lean_unbox_float(x_8);
lean_dec(x_8);
x_16 = lean_float_to_string(x_15);
x_17 = lean_string_append(x_14, x_16);
lean_dec(x_16);
x_18 = l_Option_HasRepr___rarg___closed__3;
x_19 = lean_string_append(x_17, x_18);
x_20 = lean_apply_2(x_6, x_19, x_5);
return x_20;
} else {
uint8_t x_21;
lean_dec(x_1);
x_21 = !lean_is_exclusive(x_3);
if (x_21 == 0) {
return x_3;
} else {
lean_object *x_22;
lean_object *x_23;
lean_object *x_24;
x_22 = lean_ctor_get(x_3, 0);
x_23 = lean_ctor_get(x_3, 1);
lean_inc(x_23);
lean_inc(x_22);
lean_dec(x_3);
x_24 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_24, 0, x_22);
lean_ctor_set(x_24, 1, x_23);
return x_24;
}
}
}
}
lean_object *l_IO_println___at_main___spec__9(lean_object *x_1,
lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = l_IO_print___at_main___spec__10(x_1, x_2);
if (lean_obj_tag(x_3) == 0) {
lean_object *x_4;
lean_object *x_5;
lean_object *x_6;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = l_IO_FS_Handle_putStrLn___rarg___closed__1;
x_6 = l_IO_print___at___private_Init_System_IO_1__printlnAux___spec__2(x_5,
x_4);
return x_6;
} else {
uint8_t x_7;
x_7 = !lean_is_exclusive(x_3);
if (x_7 == 0) {
return x_3;
} else {
lean_object *x_8;
lean_object *x_9;
lean_object *x_10;
x_8 = lean_ctor_get(x_3, 0);
x_9 = lean_ctor_get(x_3, 1);
lean_inc(x_9);
lean_inc(x_8);
lean_dec(x_3);
x_10 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_10, 0, x_8);
lean_ctor_set(x_10, 1, x_9);
return x_10;
}
}
}
}
lean_object *_init_l_main___closed__1() {
_start : {
lean_object *x_1;
lean_object *x_2;
lean_object *x_3;
x_1 = l_Int_zero;
x_2 = l_Int_one;
x_3 = lean_int_add(x_1, x_2);
return x_3;
}
}
double _init_l_main___closed__2() {
_start : {
double x_1;
double x_2;
double x_3;
x_1 = l_Float_HasZero___closed__1;
x_2 = l_Float_HasOne___closed__1;
x_3 = x_1 + x_2;
return x_3;
}
}
double _init_l_main___closed__3() {
_start : {
double x_1;
double x_2;
double x_3;
x_1 = l_Float_HasZero___closed__1;
x_2 = l_quadraticFormula___closed__2;
x_3 = x_1 - x_2;
return x_3;
}
}
double _init_l_main___closed__4() {
_start : {
double x_1;
double x_2;
double x_3;
x_1 = l_quadraticFormula___closed__2;
x_2 = l_Float_HasOne___closed__1;
x_3 = x_1 + x_2;
return x_3;
}
}
double _init_l_main___closed__5() {
_start : {
double x_1;
double x_2;
double x_3;
x_1 = l_Float_HasZero___closed__1;
x_2 = l_main___closed__4;
x_3 = x_1 - x_2;
return x_3;
}
}
lean_object *_init_l_main___closed__6() {
_start : {
double x_1;
double x_2;
double x_3;
lean_object *x_4;
x_1 = l_Float_HasOne___closed__1;
x_2 = l_main___closed__3;
x_3 = l_main___closed__5;
x_4 = l_quadraticFormula(x_1, x_2, x_3);
return x_4;
}
}
lean_object *_lean_main(lean_object *x_1) {
_start : {
lean_object *x_2;
lean_object *x_3;
x_2 = lean_unsigned_to_nat(1u);
x_3 = l_IO_println___at_main___spec__1(x_2, x_1);
if (lean_obj_tag(x_3) == 0) {
lean_object *x_4;
lean_object *x_5;
lean_object *x_6;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = l_main___closed__1;
x_6 = l_IO_println___at_main___spec__3(x_5, x_4);
if (lean_obj_tag(x_6) == 0) {
lean_object *x_7;
uint64_t x_8;
lean_object *x_9;
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
lean_dec(x_6);
x_8 = 1;
x_9 = l_IO_println___at_main___spec__5(x_8, x_7);
if (lean_obj_tag(x_9) == 0) {
lean_object *x_10;
double x_11;
lean_object *x_12;
x_10 = lean_ctor_get(x_9, 1);
lean_inc(x_10);
lean_dec(x_9);
x_11 = l_main___closed__2;
x_12 = l_IO_println___at_main___spec__7(x_11, x_10);
if (lean_obj_tag(x_12) == 0) {
lean_object *x_13;
lean_object *x_14;
lean_object *x_15;
x_13 = lean_ctor_get(x_12, 1);
lean_inc(x_13);
lean_dec(x_12);
x_14 = l_main___closed__6;
x_15 = l_IO_println___at_main___spec__9(x_14, x_13);
if (lean_obj_tag(x_15) == 0) {
uint8_t x_16;
x_16 = !lean_is_exclusive(x_15);
if (x_16 == 0) {
lean_object *x_17;
lean_object *x_18;
x_17 = lean_ctor_get(x_15, 0);
lean_dec(x_17);
x_18 = lean_box(0);
lean_ctor_set(x_15, 0, x_18);
return x_15;
} else {
lean_object *x_19;
lean_object *x_20;
lean_object *x_21;
x_19 = lean_ctor_get(x_15, 1);
lean_inc(x_19);
lean_dec(x_15);
x_20 = lean_box(0);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
return x_21;
}
} else {
uint8_t x_22;
x_22 = !lean_is_exclusive(x_15);
if (x_22 == 0) {
return x_15;
} else {
lean_object *x_23;
lean_object *x_24;
lean_object *x_25;
x_23 = lean_ctor_get(x_15, 0);
x_24 = lean_ctor_get(x_15, 1);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_15);
x_25 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
return x_25;
}
}
} else {
uint8_t x_26;
x_26 = !lean_is_exclusive(x_12);
if (x_26 == 0) {
return x_12;
} else {
lean_object *x_27;
lean_object *x_28;
lean_object *x_29;
x_27 = lean_ctor_get(x_12, 0);
x_28 = lean_ctor_get(x_12, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_dec(x_12);
x_29 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
return x_29;
}
}
} else {
uint8_t x_30;
x_30 = !lean_is_exclusive(x_9);
if (x_30 == 0) {
return x_9;
} else {
lean_object *x_31;
lean_object *x_32;
lean_object *x_33;
x_31 = lean_ctor_get(x_9, 0);
x_32 = lean_ctor_get(x_9, 1);
lean_inc(x_32);
lean_inc(x_31);
lean_dec(x_9);
x_33 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_33, 0, x_31);
lean_ctor_set(x_33, 1, x_32);
return x_33;
}
}
} else {
uint8_t x_34;
x_34 = !lean_is_exclusive(x_6);
if (x_34 == 0) {
return x_6;
} else {
lean_object *x_35;
lean_object *x_36;
lean_object *x_37;
x_35 = lean_ctor_get(x_6, 0);
x_36 = lean_ctor_get(x_6, 1);
lean_inc(x_36);
lean_inc(x_35);
lean_dec(x_6);
x_37 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_37, 0, x_35);
lean_ctor_set(x_37, 1, x_36);
return x_37;
}
}
} else {
uint8_t x_38;
x_38 = !lean_is_exclusive(x_3);
if (x_38 == 0) {
return x_3;
} else {
lean_object *x_39;
lean_object *x_40;
lean_object *x_41;
x_39 = lean_ctor_get(x_3, 0);
x_40 = lean_ctor_get(x_3, 1);
lean_inc(x_40);
lean_inc(x_39);
lean_dec(x_3);
x_41 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_41, 0, x_39);
lean_ctor_set(x_41, 1, x_40);
return x_41;
}
}
}
}
lean_object *l_IO_print___at_main___spec__4___boxed(lean_object *x_1,
lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = l_IO_print___at_main___spec__4(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object *l_IO_println___at_main___spec__3___boxed(lean_object *x_1,
lean_object *x_2) {
_start : {
lean_object *x_3;
x_3 = l_IO_println___at_main___spec__3(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object *l_IO_print___at_main___spec__6___boxed(lean_object *x_1,
lean_object *x_2) {
_start : {
uint64_t x_3;
lean_object *x_4;
x_3 = lean_unbox_uint64(x_1);
lean_dec(x_1);
x_4 = l_IO_print___at_main___spec__6(x_3, x_2);
return x_4;
}
}
lean_object *l_IO_println___at_main___spec__5___boxed(lean_object *x_1,
lean_object *x_2) {
_start : {
uint64_t x_3;
lean_object *x_4;
x_3 = lean_unbox_uint64(x_1);
lean_dec(x_1);
x_4 = l_IO_println___at_main___spec__5(x_3, x_2);
return x_4;
}
}
lean_object *l_IO_print___at_main___spec__8___boxed(lean_object *x_1,
lean_object *x_2) {
_start : {
double x_3;
lean_object *x_4;
x_3 = lean_unbox_float(x_1);
lean_dec(x_1);
x_4 = l_IO_print___at_main___spec__8(x_3, x_2);
return x_4;
}
}
lean_object *l_IO_println___at_main___spec__7___boxed(lean_object *x_1,
lean_object *x_2) {
_start : {
double x_3;
lean_object *x_4;
x_3 = lean_unbox_float(x_1);
lean_dec(x_1);
x_4 = l_IO_println___at_main___spec__7(x_3, x_2);
return x_4;
}
}
lean_object *initialize_Init(lean_object *);
static bool _G_initialized = false;
lean_object *initialize_Arith(lean_object *w) {
lean_object *res;
if (_G_initialized)
return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res))
return res;
lean_dec_ref(res);
l_quadraticFormula___closed__1 = _init_l_quadraticFormula___closed__1();
l_quadraticFormula___closed__2 = _init_l_quadraticFormula___closed__2();
l_quadraticFormula___closed__3 = _init_l_quadraticFormula___closed__3();
l_main___closed__1 = _init_l_main___closed__1();
lean_mark_persistent(l_main___closed__1);
l_main___closed__2 = _init_l_main___closed__2();
l_main___closed__3 = _init_l_main___closed__3();
l_main___closed__4 = _init_l_main___closed__4();
l_main___closed__5 = _init_l_main___closed__5();
l_main___closed__6 = _init_l_main___closed__6();
lean_mark_persistent(l_main___closed__6);
return lean_io_result_mk_ok(lean_box(0));
}
void lean_initialize_runtime_module();
#if defined(WIN32) || defined(_WIN32)
#include <windows.h>
#endif
int main(int argc, char **argv) {
#if defined(WIN32) || defined(_WIN32)
SetErrorMode(SEM_FAILCRITICALERRORS);
#endif
lean_object *in;
lean_object *res;
lean_initialize_runtime_module();
res = initialize_Arith(lean_io_mk_world());
lean_io_mark_end_initialization();
if (lean_io_result_is_ok(res)) {
lean_dec_ref(res);
lean_init_task_manager();
res = _lean_main(lean_io_mk_world());
}
if (lean_io_result_is_ok(res)) {
int ret = lean_unbox(lean_io_result_get_value(res));
lean_dec_ref(res);
return ret;
} else {
lean_io_result_show_error(res);
lean_dec_ref(res);
return 1;
}
}
#ifdef __cplusplus
}
#endif
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment