A first stab at a C implementation, leaveing as much to std::to_strin…

…g as possible
leanprover · Apr 11, 2024 · 3e32e35 · 3e32e35
1 parent 99cbe00
commit 3e32e35
Show file tree

Hide file tree

Showing 3 changed files with 39 additions and 1 deletion.
diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
@@ -120,7 +120,8 @@ def toDigitsCore (base : Nat) : Nat → Nat → List Char → List Char
 def toDigits (base : Nat) (n : Nat) : List Char :=
   toDigitsCore base (n+1) n []
 
-protected def repr (n : Nat) : String :=
+@[extern "lean_string_of_nat"]
+protected def repr (n : @& Nat) : String :=
   (toDigits 10 n).asString
 
 def superDigitChar (n : Nat) : Char :=

diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
@@ -1044,6 +1044,7 @@ LEAN_EXPORT bool lean_string_lt(b_lean_obj_arg s1, b_lean_obj_arg s2);
 static inline uint8_t lean_string_dec_eq(b_lean_obj_arg s1, b_lean_obj_arg s2) { return lean_string_eq(s1, s2); }
 static inline uint8_t lean_string_dec_lt(b_lean_obj_arg s1, b_lean_obj_arg s2) { return lean_string_lt(s1, s2); }
 LEAN_EXPORT uint64_t lean_string_hash(b_lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_string_of_nat(b_lean_obj_arg n);
 
 /* Thunks */
 

diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
@@ -1629,6 +1629,10 @@ object * mk_string(std::string const & s) {
     return lean_mk_string_from_bytes(s.data(), s.size());
 }
 
+object * mk_ascii_string(std::string const & s) {
+    return lean_mk_string_core(s.data(), s.size(), s.size());
+}
+
 std::string string_to_std(b_obj_arg o) {
     lean_assert(string_size(o) > 0);
     return std::string(w_string_cstr(o), lean_string_size(o) - 1);
@@ -1999,6 +2003,38 @@ extern "C" LEAN_EXPORT uint64 lean_string_hash(b_obj_arg s) {
     return hash_str(sz, (unsigned char const *) str, 11);
 }
 
+#if 1000000000000000000 < LEAN_MAX_SMALL_NAT
+#define LEAN_MAX_SMALL_POWER_OF_10 1000000000000000000
+#define LEAN_MAX_SMALL_POWER_OF_10_DIGITS 18
+#elif 1000000000 < LEAN_MAX_SMALL_NAT
+#define LEAN_MAX_SMALL_POWER_OF_10 1000000000
+#define LEAN_MAX_SMALL_POWER_OF_10_DIGITS 9
+#else
+#error "Cannot find suitable LEAN_MAX_SMALL_POWER_OF_10"
+#endif
+
+extern "C" LEAN_EXPORT obj_res lean_string_of_nat(b_obj_arg n) {
+    if (lean_is_scalar(n)) {
+        return mk_ascii_string(std::to_string(lean_unbox(n)));
+    } else {
+        object * s = lean_mk_string("");
+        while (true) {
+            lean_inc(n);
+            object * d = lean_nat_mod(n, lean_box(LEAN_MAX_SMALL_POWER_OF_10));
+            lean_assert(lean_is_scalar(d));
+            n = lean_nat_div(n, lean_box(LEAN_MAX_SMALL_POWER_OF_10));
+            if (lean_unbox(n) == 0) {
+                return lean_string_append(mk_ascii_string(std::to_string(lean_unbox(d))), s);
+            } else {
+                std::string ss = std::to_string(lean_unbox(d));
+                // pad to LEAN_MAX_SMALL_POWER_OF_10_DIGITS digits
+                ss.insert(0, LEAN_MAX_SMALL_POWER_OF_10_DIGITS - ss.length(), '0');
+                s = lean_string_append(mk_ascii_string(ss), s);
+            }
+        }
+    }
+}
+
 // =======================================
 // ByteArray & FloatArray