StructsAndArith.lean => C

StructsAndArith.c

// Lean compiler output
// Module: StructsAndArith
// 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
double sin(double);
lean_object *l_main___closed__2;
double lean_float_of_nat(lean_object *);
lean_object *_lean_main(lean_object *);
double l_Polar_distance(lean_object *, lean_object *);
double l_HasPowFloatNat(double, lean_object *);
lean_object *l_main___closed__6;
lean_object *l_main___closed__3;
uint8_t l_Float_beq(double, double);
lean_object *lean_string_append(lean_object *, lean_object *);
double sqrt(double);
lean_object *l_main___closed__5;
lean_object *l_Polar_toCartesian(lean_object *);
lean_object *l_main___closed__4;
double l_Cartesian_toPolar___closed__7;
extern double l_Float_HasZero___closed__1;
lean_object *l_main___closed__9;
double l_Cartesian_distance___closed__1;
lean_object *l_Cartesian_distance___boxed(lean_object *, lean_object *);
lean_object *l_main___closed__8;
lean_object *l_IO_println___at___private_Init_System_IO_1__printlnAux___spec__1(
    lean_object *, lean_object *);
double l_Cartesian_toPolar___closed__5;
double l_main___closed__1;
lean_object *lean_float_to_string(double);
lean_object *l_Polar_toCartesian___boxed(lean_object *);
double l_Float_div(double, double);
extern lean_object *l_List_reprAux___main___rarg___closed__1;
double l_Cartesian_toPolar___closed__3;
double l_Float_sub(double, double);
double l_Float_add(double, double);
extern double l_Float_HasOne___closed__1;
lean_object *l_HasPowFloatNat___boxed(lean_object *, lean_object *);
double l_Cartesian_toPolar___closed__6;
lean_object *l_main___closed__10;
double atan(double);
double cos(double);
double pow(double, double);
lean_object *l_Polar_distance___boxed(lean_object *, lean_object *);
lean_object *l_main___closed__11;
double l_Cartesian_toPolar___closed__8;
double l_Cartesian_toPolar___closed__4;
double l_Cartesian_distance(lean_object *, lean_object *);
double l_Cartesian_toPolar___closed__9;
double l_Cartesian_toPolar___closed__2;
lean_object *l_Cartesian_toPolar___boxed(lean_object *);
lean_object *l_Cartesian_toPolar(lean_object *);
double l_Cartesian_toPolar___closed__1;
lean_object *l_main___closed__7;
double l_Float_mul(double, double);
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;
}
}
double _init_l_Cartesian_distance___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 l_Cartesian_distance(lean_object *x_1, lean_object *x_2) {
_start : {
  double x_3;
  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;
  x_3 = lean_ctor_get_float(x_1, 0);
  x_4 = lean_ctor_get_float(x_2, 0);
  x_5 = x_3 - x_4;
  x_6 = l_Cartesian_distance___closed__1;
  x_7 = pow(x_5, x_6);
  x_8 = lean_ctor_get_float(x_1, 8);
  x_9 = lean_ctor_get_float(x_2, 8);
  x_10 = x_8 - x_9;
  x_11 = pow(x_10, x_6);
  x_12 = x_7 + x_11;
  x_13 = sqrt(x_12);
  return x_13;
}
}
lean_object *l_Cartesian_distance___boxed(lean_object *x_1, lean_object *x_2) {
_start : {
  double x_3;
  lean_object *x_4;
  x_3 = l_Cartesian_distance(x_1, x_2);
  lean_dec(x_2);
  lean_dec(x_1);
  x_4 = lean_box_float(x_3);
  return x_4;
}
}
double _init_l_Cartesian_toPolar___closed__1() {
_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_Cartesian_toPolar___closed__2() {
_start : {
  double x_1;
  double x_2;
  x_1 = l_Cartesian_toPolar___closed__1;
  x_2 = x_1 + x_1;
  return x_2;
}
}
double _init_l_Cartesian_toPolar___closed__3() {
_start : {
  double x_1;
  double x_2;
  double x_3;
  x_1 = l_Cartesian_toPolar___closed__2;
  x_2 = l_Float_HasOne___closed__1;
  x_3 = x_1 + x_2;
  return x_3;
}
}
double _init_l_Cartesian_toPolar___closed__4() {
_start : {
  double x_1;
  double x_2;
  x_1 = l_Cartesian_toPolar___closed__3;
  x_2 = x_1 + x_1;
  return x_2;
}
}
double _init_l_Cartesian_toPolar___closed__5() {
_start : {
  double x_1;
  double x_2;
  double x_3;
  x_1 = l_Cartesian_toPolar___closed__4;
  x_2 = l_Float_HasOne___closed__1;
  x_3 = x_1 + x_2;
  return x_3;
}
}
double _init_l_Cartesian_toPolar___closed__6() {
_start : {
  double x_1;
  double x_2;
  x_1 = l_Cartesian_toPolar___closed__5;
  x_2 = x_1 + x_1;
  return x_2;
}
}
double _init_l_Cartesian_toPolar___closed__7() {
_start : {
  double x_1;
  double x_2;
  x_1 = l_Cartesian_toPolar___closed__6;
  x_2 = x_1 + x_1;
  return x_2;
}
}
double _init_l_Cartesian_toPolar___closed__8() {
_start : {
  double x_1;
  double x_2;
  double x_3;
  x_1 = l_Cartesian_toPolar___closed__7;
  x_2 = l_Float_HasOne___closed__1;
  x_3 = x_1 + x_2;
  return x_3;
}
}
double _init_l_Cartesian_toPolar___closed__9() {
_start : {
  double x_1;
  double x_2;
  x_1 = l_Cartesian_toPolar___closed__8;
  x_2 = x_1 + x_1;
  return x_2;
}
}
lean_object *l_Cartesian_toPolar(lean_object *x_1) {
_start : {
  double x_2;
  double x_3;
  double x_4;
  double x_5;
  double x_6;
  double x_7;
  double x_8;
  double x_9;
  uint8_t x_10;
  x_2 = lean_ctor_get_float(x_1, 0);
  x_3 = l_Cartesian_distance___closed__1;
  x_4 = pow(x_2, x_3);
  x_5 = lean_ctor_get_float(x_1, 8);
  x_6 = pow(x_5, x_3);
  x_7 = x_4 + x_6;
  x_8 = sqrt(x_7);
  x_9 = l_Float_HasZero___closed__1;
  x_10 = x_2 == x_9;
  if (x_10 == 0) {
    double x_11;
    double x_12;
    lean_object *x_13;
    x_11 = x_5 / x_2;
    x_12 = atan(x_11);
    x_13 = lean_alloc_ctor(0, 0, 16);
    lean_ctor_set_float(x_13, 0, x_8);
    lean_ctor_set_float(x_13, 8, x_12);
    return x_13;
  } else {
    double x_14;
    lean_object *x_15;
    x_14 = l_Cartesian_toPolar___closed__9;
    x_15 = lean_alloc_ctor(0, 0, 16);
    lean_ctor_set_float(x_15, 0, x_8);
    lean_ctor_set_float(x_15, 8, x_14);
    return x_15;
  }
}
}
lean_object *l_Cartesian_toPolar___boxed(lean_object *x_1) {
_start : {
  lean_object *x_2;
  x_2 = l_Cartesian_toPolar(x_1);
  lean_dec(x_1);
  return x_2;
}
}
double l_Polar_distance(lean_object *x_1, lean_object *x_2) {
_start : {
  double x_3;
  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;
  x_3 = lean_ctor_get_float(x_1, 0);
  x_4 = l_Cartesian_distance___closed__1;
  x_5 = pow(x_3, x_4);
  x_6 = lean_ctor_get_float(x_2, 0);
  x_7 = pow(x_6, x_4);
  x_8 = x_5 + x_7;
  x_9 = l_Cartesian_toPolar___closed__1;
  x_10 = x_9 * x_3;
  x_11 = x_10 * x_6;
  x_12 = lean_ctor_get_float(x_2, 8);
  x_13 = lean_ctor_get_float(x_1, 8);
  x_14 = x_12 - x_13;
  x_15 = cos(x_14);
  x_16 = x_11 * x_15;
  x_17 = x_8 - x_16;
  x_18 = sqrt(x_17);
  return x_18;
}
}
lean_object *l_Polar_distance___boxed(lean_object *x_1, lean_object *x_2) {
_start : {
  double x_3;
  lean_object *x_4;
  x_3 = l_Polar_distance(x_1, x_2);
  lean_dec(x_2);
  lean_dec(x_1);
  x_4 = lean_box_float(x_3);
  return x_4;
}
}
lean_object *l_Polar_toCartesian(lean_object *x_1) {
_start : {
  double x_2;
  double x_3;
  double x_4;
  double x_5;
  double x_6;
  double x_7;
  lean_object *x_8;
  x_2 = lean_ctor_get_float(x_1, 0);
  x_3 = lean_ctor_get_float(x_1, 8);
  x_4 = cos(x_3);
  x_5 = x_2 * x_4;
  x_6 = sin(x_3);
  x_7 = x_2 * x_6;
  x_8 = lean_alloc_ctor(0, 0, 16);
  lean_ctor_set_float(x_8, 0, x_5);
  lean_ctor_set_float(x_8, 8, x_7);
  return x_8;
}
}
lean_object *l_Polar_toCartesian___boxed(lean_object *x_1) {
_start : {
  lean_object *x_2;
  x_2 = l_Polar_toCartesian(x_1);
  lean_dec(x_1);
  return x_2;
}
}
double _init_l_main___closed__1() {
_start : {
  double x_1;
  double x_2;
  double x_3;
  x_1 = l_Cartesian_toPolar___closed__1;
  x_2 = l_Float_HasOne___closed__1;
  x_3 = x_1 + x_2;
  return x_3;
}
}
lean_object *_init_l_main___closed__2() {
_start : {
  double x_1;
  double x_2;
  lean_object *x_3;
  x_1 = l_main___closed__1;
  x_2 = l_Cartesian_toPolar___closed__2;
  x_3 = lean_alloc_ctor(0, 0, 16);
  lean_ctor_set_float(x_3, 0, x_1);
  lean_ctor_set_float(x_3, 8, x_2);
  return x_3;
}
}
lean_object *_init_l_main___closed__3() {
_start : {
  lean_object *x_1;
  lean_object *x_2;
  x_1 = l_main___closed__2;
  x_2 = l_Cartesian_toPolar(x_1);
  return x_2;
}
}
lean_object *_init_l_main___closed__4() {
_start : {
  lean_object *x_1;
  double x_2;
  lean_object *x_3;
  x_1 = l_main___closed__3;
  x_2 = lean_ctor_get_float(x_1, 0);
  x_3 = lean_float_to_string(x_2);
  return x_3;
}
}
lean_object *_init_l_main___closed__5() {
_start : {
  lean_object *x_1;
  x_1 = lean_mk_string("(3,4) in cartesian is (");
  return x_1;
}
}
lean_object *_init_l_main___closed__6() {
_start : {
  lean_object *x_1;
  lean_object *x_2;
  lean_object *x_3;
  x_1 = l_main___closed__5;
  x_2 = l_main___closed__4;
  x_3 = lean_string_append(x_1, x_2);
  return x_3;
}
}
lean_object *_init_l_main___closed__7() {
_start : {
  lean_object *x_1;
  lean_object *x_2;
  lean_object *x_3;
  x_1 = l_main___closed__6;
  x_2 = l_List_reprAux___main___rarg___closed__1;
  x_3 = lean_string_append(x_1, x_2);
  return x_3;
}
}
lean_object *_init_l_main___closed__8() {
_start : {
  lean_object *x_1;
  double x_2;
  lean_object *x_3;
  x_1 = l_main___closed__3;
  x_2 = lean_ctor_get_float(x_1, 8);
  x_3 = lean_float_to_string(x_2);
  return x_3;
}
}
lean_object *_init_l_main___closed__9() {
_start : {
  lean_object *x_1;
  lean_object *x_2;
  lean_object *x_3;
  x_1 = l_main___closed__7;
  x_2 = l_main___closed__8;
  x_3 = lean_string_append(x_1, x_2);
  return x_3;
}
}
lean_object *_init_l_main___closed__10() {
_start : {
  lean_object *x_1;
  x_1 = lean_mk_string(") in polar");
  return x_1;
}
}
lean_object *_init_l_main___closed__11() {
_start : {
  lean_object *x_1;
  lean_object *x_2;
  lean_object *x_3;
  x_1 = l_main___closed__9;
  x_2 = l_main___closed__10;
  x_3 = lean_string_append(x_1, x_2);
  return x_3;
}
}
lean_object *_lean_main(lean_object *x_1) {
_start : {
  lean_object *x_2;
  lean_object *x_3;
  x_2 = l_main___closed__11;
  x_3 = l_IO_println___at___private_Init_System_IO_1__printlnAux___spec__1(x_2,
                                                                           x_1);
  if (lean_obj_tag(x_3) == 0) {
    uint8_t x_4;
    x_4 = !lean_is_exclusive(x_3);
    if (x_4 == 0) {
      lean_object *x_5;
      lean_object *x_6;
      x_5 = lean_ctor_get(x_3, 0);
      lean_dec(x_5);
      x_6 = lean_box(0);
      lean_ctor_set(x_3, 0, x_6);
      return x_3;
    } else {
      lean_object *x_7;
      lean_object *x_8;
      lean_object *x_9;
      x_7 = lean_ctor_get(x_3, 1);
      lean_inc(x_7);
      lean_dec(x_3);
      x_8 = lean_box(0);
      x_9 = lean_alloc_ctor(0, 2, 0);
      lean_ctor_set(x_9, 0, x_8);
      lean_ctor_set(x_9, 1, x_7);
      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 *initialize_Init(lean_object *);
static bool _G_initialized = false;
lean_object *initialize_StructsAndArith(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_Cartesian_distance___closed__1 = _init_l_Cartesian_distance___closed__1();
  l_Cartesian_toPolar___closed__1 = _init_l_Cartesian_toPolar___closed__1();
  l_Cartesian_toPolar___closed__2 = _init_l_Cartesian_toPolar___closed__2();
  l_Cartesian_toPolar___closed__3 = _init_l_Cartesian_toPolar___closed__3();
  l_Cartesian_toPolar___closed__4 = _init_l_Cartesian_toPolar___closed__4();
  l_Cartesian_toPolar___closed__5 = _init_l_Cartesian_toPolar___closed__5();
  l_Cartesian_toPolar___closed__6 = _init_l_Cartesian_toPolar___closed__6();
  l_Cartesian_toPolar___closed__7 = _init_l_Cartesian_toPolar___closed__7();
  l_Cartesian_toPolar___closed__8 = _init_l_Cartesian_toPolar___closed__8();
  l_Cartesian_toPolar___closed__9 = _init_l_Cartesian_toPolar___closed__9();
  l_main___closed__1 = _init_l_main___closed__1();
  l_main___closed__2 = _init_l_main___closed__2();
  lean_mark_persistent(l_main___closed__2);
  l_main___closed__3 = _init_l_main___closed__3();
  lean_mark_persistent(l_main___closed__3);
  l_main___closed__4 = _init_l_main___closed__4();
  lean_mark_persistent(l_main___closed__4);
  l_main___closed__5 = _init_l_main___closed__5();
  lean_mark_persistent(l_main___closed__5);
  l_main___closed__6 = _init_l_main___closed__6();
  lean_mark_persistent(l_main___closed__6);
  l_main___closed__7 = _init_l_main___closed__7();
  lean_mark_persistent(l_main___closed__7);
  l_main___closed__8 = _init_l_main___closed__8();
  lean_mark_persistent(l_main___closed__8);
  l_main___closed__9 = _init_l_main___closed__9();
  lean_mark_persistent(l_main___closed__9);
  l_main___closed__10 = _init_l_main___closed__10();
  lean_mark_persistent(l_main___closed__10);
  l_main___closed__11 = _init_l_main___closed__11();
  lean_mark_persistent(l_main___closed__11);
  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_StructsAndArith(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