feat: add more float functions

src/Init/Data/Float.lean

@@ -31,33 +31,33 @@ structure Float where
 
 instance : Inhabited Float := ⟨{ val := floatSpec.val }⟩
 
-@[extern "lean_float_add"]  opaque Float.add : Float → Float → Float
-@[extern "lean_float_sub"]  opaque Float.sub : Float → Float → Float
-@[extern "lean_float_mul"]  opaque Float.mul : Float → Float → Float
-@[extern "lean_float_div"]  opaque Float.div : Float → Float → Float
-@[extern "lean_float_negate"]   opaque Float.neg : Float → Float
+@[extern "lean_float_add"] opaque Float.add : Float → Float → Float
+@[extern "lean_float_sub"] opaque Float.sub : Float → Float → Float
+@[extern "lean_float_mul"] opaque Float.mul : Float → Float → Float
+@[extern "lean_float_div"] opaque Float.div : Float → Float → Float
+@[extern "lean_float_negate"] opaque Float.neg : Float → Float
 
 set_option bootstrap.genMatcherCode false
-def Float.lt  : Float → Float → Prop := fun a b =>
+def Float.lt : Float → Float → Prop := fun a b =>
   match a, b with
   | ⟨a⟩, ⟨b⟩ => floatSpec.lt a b
 
-def Float.le  : Float → Float → Prop := fun a b =>
+def Float.le : Float → Float → Prop := fun a b =>
   floatSpec.le a.val b.val
 
-instance : Add Float       := ⟨Float.add⟩
-instance : Sub Float       := ⟨Float.sub⟩
-instance : Mul Float       := ⟨Float.mul⟩
-instance : Div Float       := ⟨Float.div⟩
-instance : Neg Float       := ⟨Float.neg⟩
-instance : LT Float        := ⟨Float.lt⟩
-instance : LE Float        := ⟨Float.le⟩
+instance : Add Float := ⟨Float.add⟩
+instance : Sub Float := ⟨Float.sub⟩
+instance : Mul Float := ⟨Float.mul⟩
+instance : Div Float := ⟨Float.div⟩
+instance : Neg Float := ⟨Float.neg⟩
+instance : LT Float  := ⟨Float.lt⟩
+instance : LE Float  := ⟨Float.le⟩
 
 @[extern "lean_float_beq"] opaque Float.beq (a b : Float) : Bool
 
 instance : BEq Float := ⟨Float.beq⟩
 
-@[extern "lean_float_decLt"]   opaque Float.decLt (a b : Float) : Decidable (a < b) :=
+@[extern "lean_float_decLt"] opaque Float.decLt (a b : Float) : Decidable (a < b) :=
   match a, b with
   | ⟨a⟩, ⟨b⟩ => floatSpec.decLt a b
 
@@ -76,6 +76,11 @@ instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
 @[extern "lean_float_to_uint64"] opaque Float.toUInt64 : Float → UInt64
 @[extern "lean_float_to_usize"] opaque Float.toUSize : Float → USize
 
+@[extern "lean_float_isnan"] opaque Float.isNaN : Float → Bool
+@[extern "lean_float_isfinite"] opaque Float.isFinite : Float → Bool
+@[extern "lean_float_isinf"] opaque Float.isInf : Float → Bool
+@[extern "lean_float_frexp"] opaque Float.frExp : Float → Float × Int
+
 instance : ToString Float where
   toString := Float.toString
 

src/include/lean/lean.h

@@ -1688,6 +1688,10 @@ static inline uint64_t lean_usize_to_uint64(size_t a) { return ((uint64_t)a); }
 
 LEAN_SHARED lean_obj_res lean_float_to_string(double a);
 LEAN_SHARED double lean_float_scaleb(double a, b_lean_obj_arg b);
+LEAN_SHARED uint8_t lean_float_isnan(double a);
+LEAN_SHARED uint8_t lean_float_isfinite(double a);
+LEAN_SHARED uint8_t lean_float_isinf(double a);
+LEAN_SHARED lean_obj_res lean_float_frexp(double a);
 
 /* Boxing primitives */
 

src/runtime/object.cpp

@@ -32,6 +32,12 @@ Author: Leonardo de Moura
 #ifndef isnan
 #define isnan(x) std::isnan(x)
 #endif
+#ifndef isfinite
+#define isfinite(x) std::isfinite(x)
+#endif
+#ifndef isinf
+#define isinf(x) std::isinf(x)
+#endif
 
 // see `Task.Priority.max`
 #define LEAN_MAX_PRIO 8
@@ -1480,6 +1486,17 @@ extern "C" LEAN_EXPORT double lean_float_scaleb(double a, b_lean_obj_arg b) {
    }
 }
 
+extern "C" LEAN_EXPORT uint8_t lean_float_isnan(double a) { return (bool) isnan(a); }
+extern "C" LEAN_EXPORT uint8_t lean_float_isfinite(double a) { return (bool) isfinite(a); }
+extern "C" LEAN_EXPORT uint8_t lean_float_isinf(double a) { return (bool) isinf(a); }
+extern "C" LEAN_EXPORT obj_res lean_float_frexp(double a) {
+    object* r = lean_alloc_ctor(0, 2, 0);
+    int exp;
+    lean_ctor_set(r, 0, lean_box_float(frexp(a, &exp)));
+    lean_ctor_set(r, 1, isfinite(a) ? lean_int_to_int(exp) : lean_box(0));
+    return r;
+}
+
 // =======================================
 // Strings
 

tests/compiler/float.lean

@@ -25,8 +25,11 @@ def tst1 : IO Unit := do
   IO.println (-1 : Float).toUInt64
   IO.println (2^64 : Float).toUInt64
   IO.println (1 / 0 : Float).toUInt64
-  IO.println (0 / 0 : Float)
-  IO.println (-(0 / 0) : Float)
+  IO.println (let x : Float := 1.4; (x, x.isNaN, x.isInf, x.isFinite, x.frExp))
+  IO.println (let x : Float := 0 / 0; (x, x.isNaN, x.isInf, x.isFinite, x.frExp))
+  IO.println (let x : Float := -0 / 0; (x, x.isNaN, x.isInf, x.isFinite, x.frExp))
+  IO.println (let x : Float := 1 / 0; (x, x.isNaN, x.isInf, x.isFinite, x.frExp))
+  IO.println (let x : Float := -1 / 0; (x, x.isNaN, x.isInf, x.isFinite, x.frExp))
 
 structure Foo where
   x : Nat

tests/compiler/float.lean.expected.out

@@ -23,8 +23,11 @@ true
 0
 18446744073709551615
 18446744073709551615
-NaN
-NaN
+(1.400000, (false, (false, (true, (0.700000, 1)))))
+(NaN, (true, (false, (false, (NaN, 0)))))
+(NaN, (true, (false, (false, (NaN, 0)))))
+(inf, (false, (true, (false, (inf, 0)))))
+(-inf, (false, (true, (false, (-inf, 0)))))
 -----
 2.333333
 3.500000