From 8e84a8c9ec28d7331f8eb7d3042c19ac82bf450d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 Apr 2020 14:05:17 -0700 Subject: [PATCH] feat: `Float` from big numbers --- src/runtime/mpz.h | 1 + src/runtime/object.cpp | 2 +- tests/lean/run/float_from_bignum.lean | 11 +++++++++++ 3 files changed, 13 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/float_from_bignum.lean diff --git a/src/runtime/mpz.h b/src/runtime/mpz.h index 8b0272bb8e..a05a211cb2 100644 --- a/src/runtime/mpz.h +++ b/src/runtime/mpz.h @@ -77,6 +77,7 @@ public: unsigned long int get_unsigned_long_int() const { lean_assert(is_unsigned_long_int()); return mpz_get_ui(m_val); } unsigned int get_unsigned_int() const { lean_assert(is_unsigned_int()); return static_cast(get_unsigned_long_int()); } size_t get_size_t() const; + double get_double() const { return mpz_get_d(m_val); } mpz & operator=(mpz const & v) { mpz_set(m_val, v.m_val); return *this; } mpz & operator=(mpz && v) { swap(*this, v); return *this; } diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index b7aee568a5..cff29d996a 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -1453,7 +1453,7 @@ extern "C" double lean_float_of_nat(b_lean_obj_arg a) { if (lean_is_scalar(a)) { return static_cast(lean_unbox(a)); } else { - return std::nan(""); // TODO(Leo): improve + return mpz_value(a).get_double(); } } diff --git a/tests/lean/run/float_from_bignum.lean b/tests/lean/run/float_from_bignum.lean new file mode 100644 index 0000000000..8936ffad4a --- /dev/null +++ b/tests/lean/run/float_from_bignum.lean @@ -0,0 +1,11 @@ +def check (b : Bool) : IO Unit := +unless b $ throw $ IO.userError "check failed" + +def tst1 : IO Unit := do +check (Nat.toFloat (10^40) > Nat.toFloat (10^30)); +check (Nat.toFloat (10^40) >= Nat.toFloat (10^30)); +check (Nat.toFloat (10^40) == Nat.toFloat (10^40)); +check (Nat.toFloat (10^80) > Nat.toFloat (10^40)); +pure () + +#eval tst1