Memoize small Nat strings

leanprover · Apr 12, 2024 · 57cf9ae · 57cf9ae
1 parent 71c77ee
commit 57cf9ae
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 2 deletions.
diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
@@ -121,7 +121,17 @@ def toDigits (base : Nat) (n : Nat) : List Char :=
   toDigitsCore base (n+1) n []
 
 @[extern "lean_string_of_nat"]
-protected def repr (n : @& Nat) : String :=
+private opaque reprFastAux (n : @& Nat) : String
+
+private def reprArray : Array String := Id.run do
+  List.range 128 |>.map Nat.reprFastAux |> Array.mk
+
+private def reprFast (n : Nat) : String :=
+  if h : n < 128 then Nat.reprArray.get ⟨n, h⟩ else
+  Nat.reprFastAux n
+
+@[implemented_by reprFast]
+protected def repr (n : Nat) : String :=
   (toDigits 10 n).asString
 
 def superDigitChar (n : Nat) : Char :=

diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
@@ -6,7 +6,7 @@ options get_default_options() {
     // see https://lean-lang.org/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications
 #if LEAN_IS_STAGE0 == 1
     // switch to `true` for ABI-breaking changes affecting meta code
-    opts = opts.update({"interpreter", "prefer_native"}, false);
+    opts = opts.update({"interpreter", "prefer_native"}, true);
     // switch to `true` for changing built-in parsers used in quotations
     opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax