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

…g as possible

src/Init/Data/Repr.lean

@@ -103,37 +103,25 @@ instance {p : α → Prop} [Repr α] : Repr (Subtype p) where
 
 namespace Nat
 
-def digitChar (n : Nat) : Char :=
-  if n = 0 then '0' else
-  if n = 1 then '1' else
-  if n = 2 then '2' else
-  if n = 3 then '3' else
-  if n = 4 then '4' else
-  if n = 5 then '5' else
-  if n = 6 then '6' else
-  if n = 7 then '7' else
-  if n = 8 then '8' else
-  if n = 9 then '9' else
-  if n = 0xa then 'a' else
-  if n = 0xb then 'b' else
-  if n = 0xc then 'c' else
-  if n = 0xd then 'd' else
-  if n = 0xe then 'e' else
-  if n = 0xf then 'f' else
-  '*'
+def digitChars : Array Char :=
+  -- Array syntax not available yet
+  Array.mk ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f']
+
+def digitChar (n : Nat) : Char := digitChars.getD n '*'
 
 def toDigitsCore (base : Nat) : Nat → Nat → List Char → List Char
   | 0,      _, ds => ds
   | fuel+1, n, ds =>
-    let d  := digitChar <| n % base;
+    let d  := digitChar (n % base)
     let n' := n / base;
     if n' = 0 then d::ds
     else toDigitsCore base fuel n' (d::ds)
 
 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 :=

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 */
 

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