Simplify, leave the > USize.size case to pure lean code

leanprover · Apr 12, 2024 · ffec048 · ffec048
1 parent 32adde5
commit ffec048
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 25 deletions.
diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
@@ -120,15 +120,17 @@ def toDigitsCore (base : Nat) : Nat → Nat → List Char → List Char
 def toDigits (base : Nat) (n : Nat) : List Char :=
   toDigitsCore base (n+1) n []
 
-@[extern "lean_string_of_nat"]
-private opaque reprFastAux (n : @& Nat) : String
+@[extern "lean_string_of_usize"]
+protected def _root_.USize.repr (n : @& USize) : String :=
+  (toDigits 10 n.toNat).asString
 
 private def reprArray : Array String := Id.run do
-  List.range 128 |>.map Nat.reprFastAux |> Array.mk
+  List.range 128 |>.map (·.toUSize.repr) |> Array.mk
 
 private def reprFast (n : Nat) : String :=
   if h : n < 128 then Nat.reprArray.get ⟨n, h⟩ else
-  Nat.reprFastAux n
+  if h : n < USize.size then (USize.ofNatCore n h).repr
+  else (toDigits 10 n).asString
 
 @[implemented_by reprFast]
 protected def repr (n : Nat) : String :=

diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
@@ -1044,7 +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);
+LEAN_EXPORT lean_obj_res lean_string_of_usize(size_t);
 
 /* Thunks */
 

diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
@@ -2013,26 +2013,8 @@ extern "C" LEAN_EXPORT uint64 lean_string_hash(b_obj_arg s) {
 #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);
-            }
-        }
-    }
+extern "C" LEAN_EXPORT obj_res lean_string_of_nat(size_t n) {
+    return mk_ascii_string(std::to_string(n));
 }
 
 // =======================================