feat: add lean_float_of_decimal using GMP

src/Init/Data/Float.lean

@@ -97,3 +97,5 @@ abbrev Nat.toFloat (n : Nat) : Float :=
 @[extern "cbrt"] constant Float.cbrt : Float → Float
 
 instance : Pow Float := ⟨Float.pow⟩
+
+@[extern "lean_float_of_decimal"] constant Float.ofDecimal (m : Nat) (e : Nat) : Float

src/Init/Data/OfDecimal.lean

@@ -12,14 +12,6 @@ import Init.Data.Nat
 class OfDecimal (α : Type u) where
   ofDecimal : Nat → Nat → α
 
-def Float.fromDecimal (m : Nat) (e : Nat) : Float :=
-  fromDec (Float.ofNat m) e
-where
-  fromDec (m : Float) (e : Nat) : Float :=
-    match e with
-    | 0 => m
-    | e+1 => fromDec (m/10) e
-
 @[defaultInstance]
 instance : OfDecimal Float where
-  ofDecimal m e := Float.fromDecimal m e
+  ofDecimal m e := Float.ofDecimal m e

src/include/lean/mpq.h

@@ -33,6 +33,7 @@ public:
     mpq & operator=(double v) { mpq_set_d(m_val, v); return *this; }
 
     mpq() { mpq_init(m_val); }
+    mpq(mpz const & v):mpq() { operator=(v); }
     mpq(mpq const & v):mpq() { operator=(v); }
     mpq(mpq && s):mpq() { mpq_swap(m_val, s.m_val); }
     template<typename T> explicit mpq(T const & v):mpq() { operator=(v); }

src/runtime/object.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include <deque>
 #include <cmath>
 #include <lean/object.h>
+#include <lean/mpq.h>
 #include <lean/thread.h>
 #include <lean/utf8.h>
 #include <lean/alloc.h>
@@ -1463,6 +1464,19 @@ extern "C" lean_obj_res lean_float_to_string(double a) {
     return mk_string(std::to_string(a));
 }
 
+static double of_decimal(mpz const & m, size_t e) {
+    return (mpq(m)/mpz(10).pow(e)).get_double();
+}
+
+extern "C" double lean_float_of_decimal(b_lean_obj_arg m, b_lean_obj_arg e) {
+    if (!lean_is_scalar(e))
+        return 0.0;
+    if (lean_is_scalar(m)) {
+        return of_decimal(mpz::of_size_t(lean_unbox(m)), lean_unbox(e));
+    } else {
+        return of_decimal(mpz_value(m), lean_unbox(e));
+    }
+}
 
 // =======================================
 // Strings