feat: add Float32 support (#6366)

This PR adds support for `Float32` and fixes a bug in the runtime.

src/Init/Data/Float32.lean

@@ -9,9 +9,6 @@ import Init.Data.Int.Basic
 import Init.Data.ToString.Basic
 import Init.Data.Float
 
-/-
-#exit -- TODO: Remove after update stage0
-
 -- Just show FloatSpec is inhabited.
 opaque float32Spec : FloatSpec := {
   float := Unit,
@@ -130,7 +127,7 @@ Returns an undefined value if `x` is not finite.
 instance : ToString Float32 where
   toString := Float32.toString
 
-@[extern "lean_uint64_to_float"] opaque UInt64.toFloat32 (n : UInt64) : Float32
+@[extern "lean_uint64_to_float32"] opaque UInt64.toFloat32 (n : UInt64) : Float32
 
 instance : Inhabited Float32 where
   default := UInt64.toFloat32 0
@@ -177,4 +174,6 @@ Efficiently computes `x * 2^i`.
 -/
 @[extern "lean_float32_scaleb"]
 opaque Float32.scaleB (x : Float32) (i : @& Int) : Float32
--/
+
+@[extern "lean_float32_to_float"] opaque Float32.toFloat : Float32 → Float
+@[extern "lean_float_to_float32"] opaque Float.toFloat32 : Float → Float32

src/Init/Data/OfScientific.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Meta
 import Init.Data.Float
+import Init.Data.Float32
 import Init.Data.Nat.Log2
 
 /-- For decimal and scientific numbers (e.g., `1.23`, `3.12e10`).
@@ -56,3 +57,34 @@ instance : OfNat Float n   := ⟨Float.ofNat n⟩
 
 abbrev Nat.toFloat (n : Nat) : Float :=
   Float.ofNat n
+
+/-- Computes `m * 2^e`. -/
+def Float32.ofBinaryScientific (m : Nat) (e : Int) : Float32 :=
+  let s := m.log2 - 63
+  let m := (m >>> s).toUInt64
+  let e := e + s
+  m.toFloat32.scaleB e
+
+protected opaque Float32.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float32 :=
+  if s then
+    let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division
+    let m := (m <<< (3 * e + s)) / 5^e
+    Float32.ofBinaryScientific m (-4 * e - s)
+  else
+    Float32.ofBinaryScientific (m * 5^e) e
+
+instance : OfScientific Float32 where
+  ofScientific := Float32.ofScientific
+
+@[export lean_float32_of_nat]
+def Float32.ofNat (n : Nat) : Float32 :=
+  OfScientific.ofScientific n false 0
+
+def Float32.ofInt : Int → Float
+  | Int.ofNat n => Float.ofNat n
+  | Int.negSucc n => Float.neg (Float.ofNat (Nat.succ n))
+
+instance : OfNat Float32 n   := ⟨Float32.ofNat n⟩
+
+abbrev Nat.toFloat32 (n : Nat) : Float32 :=
+  Float32.ofNat n

src/library/compiler/ir_interpreter.cpp

@@ -187,11 +187,7 @@ option_ref<decl> find_ir_decl(environment const & env, name const & n) {
 }
 
 extern "C" double lean_float_of_nat(lean_obj_arg a);
-
-// TODO: define in Lean like `lean_float_of_nat`
-float lean_float32_of_nat(lean_obj_arg a) {
-    return lean_float_of_nat(a);
-}
+extern "C" float lean_float32_of_nat(lean_obj_arg a);
 
 static string_ref * g_mangle_prefix = nullptr;
 static string_ref * g_boxed_suffix = nullptr;
@@ -257,7 +253,7 @@ union value {
 object * box_t(value v, type t) {
     switch (t) {
     case type::Float:   return box_float(v.m_float);
-    case type::Float32: return box_float(v.m_float32);
+    case type::Float32: return box_float32(v.m_float32);
     case type::UInt8:   return box(v.m_num);
     case type::UInt16:  return box(v.m_num);
     case type::UInt32:  return box_uint32(v.m_num);

src/runtime/object.h

@@ -373,6 +373,7 @@ inline unsigned unbox_uint32(b_obj_arg o) { return lean_unbox_uint32(o); }
 inline obj_res box_uint64(unsigned long long v) { return lean_box_uint64(v); }
 inline unsigned long long unbox_uint64(b_obj_arg o) { return lean_unbox_uint64(o); }
 inline obj_res box_float(double v) { return lean_box_float(v); }
+inline obj_res box_float32(float v) { return lean_box_float32(v); }
 inline double unbox_float(b_obj_arg o) { return lean_unbox_float(o); }
 inline float unbox_float32(b_obj_arg o) { return lean_unbox_float32(o); }
 inline obj_res box_size_t(size_t v) { return lean_box_usize(v); }

tests/lean/run/float32.lean

@@ -0,0 +1,38 @@
+/-- info: 2.100000 -/
+#guard_msgs in
+#eval (2.1 : Float32)
+
+/-- info: 3.200000 -/
+#guard_msgs in
+#eval (2.1 : Float32) + 1.1
+
+/-- info: 0.900000 -/
+#guard_msgs in
+#eval (2.1 : Float32) - 1.2
+
+def test1 : IO Unit := do
+  IO.println ((2 : Float32).sin);
+  IO.println ((2 : Float32).cos);
+  IO.println ((2 : Float32).sqrt);
+  IO.println ((2 : Float32) ^ (100 : Float32));
+
+/--
+info: 0.909297
+-0.416147
+1.414214
+1267650600228229401496703205376.000000
+-/
+#guard_msgs in
+#eval test1
+
+/-- info: 0.909297 -/
+#guard_msgs in
+#eval (2 : Float32).sin.toFloat
+
+/-- info: 0.909297 -/
+#guard_msgs in
+#eval (2 : Float).sin.toFloat32
+
+/-- info: 1606938044258990275541962092341162602522202993782792835301376.000000 -/
+#guard_msgs in
+#eval (2 : Float32).toFloat ^ (200 : Float32).toFloat