chore: naming convention and NaN normalization

src/Init/Data/Float.lean

@@ -53,7 +53,7 @@ Raw transmutation from `UInt64`.
 Floats and UInts have the same endianness on all supported platforms.
 IEEE 754 very precisely specifies the bit layout of floats.
 -/
-@[extern "lean_float_from_bits"] opaque Float.fromBits : UInt64 → Float
+@[extern "lean_float_of_bits"] opaque Float.ofBits : UInt64 → Float
 
 /--
 Raw transmutation to `UInt64`.

src/include/lean/lean.h

@@ -2691,7 +2691,7 @@ static inline size_t lean_float_to_usize(double a) {
     else
         return (size_t) lean_float_to_uint32(a); // NOLINT
 }
-LEAN_EXPORT double lean_float_from_bits(uint64_t u);
+LEAN_EXPORT double lean_float_of_bits(uint64_t u);
 LEAN_EXPORT uint64_t lean_float_to_bits(double d);
 static inline double lean_float_add(double a, double b) { return a + b; }
 static inline double lean_float_sub(double a, double b) { return a - b; }

src/runtime/object.cpp

@@ -1620,17 +1620,21 @@ extern "C" LEAN_EXPORT obj_res lean_float_frexp(double a) {
     return r;
 }
 
-extern "C" LEAN_EXPORT double lean_float_from_bits(uint64_t u)
+extern "C" LEAN_EXPORT double lean_float_of_bits(uint64_t u)
 {
     static_assert(sizeof(double) == sizeof(u), "`double` unexpected size.");
     double ret;
     std::memcpy(&ret, &u, sizeof(double));
+    if (isnan(ret))
+        ret = std::numeric_limits<double>::quiet_NaN();
     return ret;
 }
 
 extern "C" LEAN_EXPORT uint64_t lean_float_to_bits(double d)
 {
     uint64_t ret;
+    if (isnan(d))
+        d = std::numeric_limits<double>::quiet_NaN();
     std::memcpy(&ret, &d, sizeof(double));
     return ret;
 }

tests/lean/run/floatBits.lean

@@ -10,4 +10,40 @@ info: 4608285800708723180
 info: true
 -/
 #guard_msgs in
-#eval Float.fromBits d.toBits == d
+#eval Float.ofBits d.toBits == d
+
+/--
+info: NaN
+-/
+#guard_msgs in
+#eval Float.ofBits 9221120237041090560
+/--
+info: NaN
+-/
+#guard_msgs in
+#eval Float.ofBits 18444492273895866368
+
+/--
+info: 9221120237041090560
+-/
+#guard_msgs in
+#eval (Float.ofBits 9221120237041090560).toBits
+
+/--
+info: 9221120237041090560
+-/
+#guard_msgs in
+#eval (Float.ofBits 18444492273895866368).toBits
+
+/--
+info: 9221120237041090560
+-/
+#guard_msgs in
+#eval (1.0/0.0 - 1.0/0.0).toBits
+
+/--
+info: 9221120237041090560
+-/
+-- Should also produce quiet_NaN
+#guard_msgs in
+#eval (-(1.0/0.0 - 1.0/0.0)).toBits