From c03edae0ccd5d43a8b51e0f11923a837be411bf2 Mon Sep 17 00:00:00 2001
From: nil <3745260+nmamano@users.noreply.github.com>
Date: Thu, 12 Nov 2026 00:18:06 +0100
Subject: [PATCH] Parse huge natVal literals in sub-quadratic time

String.toNat? folds n * 10 + d over the digits, which is quadratic in the digit count.
parseDecNat? splits the digits in halves and combines hi * 10 ^ k + lo, so GMP does the
big multiplications. It gives the same result as String.toNat? on every string.

This is the parse side of #52 by lordwilsonDev.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Export/Parse.lean | 23 ++++++++++++++++++++++-
 1 file changed, 22 insertions(+), 1 deletion(-)

diff --git a/Export/Parse.lean b/Export/Parse.lean
index 1eedbab..f81a6be 100644
--- a/Export/Parse.lean
+++ b/Export/Parse.lean
@@ -210,9 +210,30 @@ def parseExprProj (json : Json) : M Expr := do
 
   return .proj typeName projIdx struct
 
+/-- Decimal digits to `Nat` in sub-quadratic time. `String.toNat?` folds `n * 10 + d` over the
+digits, which is quadratic in the digit count. This splits the digit range in halves and combines
+`hi * 10 ^ k + lo`, so the large multiplications go to GMP. `b` holds ASCII digits only; reads
+`b[lo:hi]`. -/
+partial def natOfDigits (b : ByteArray) (lo hi : Nat) : Nat :=
+  if hi - lo ≤ 64 then Id.run do
+    let mut n := 0
+    for i in [lo:hi] do
+      n := n * 10 + (b[i]!.toNat - 48)
+    return n
+  else
+    let k := (hi - lo) / 2
+    natOfDigits b lo (hi - k) * 10 ^ k + natOfDigits b (hi - k) hi
+
+/-- The same result as `String.toNat?` on every string (a string with `_` separators goes to
+`String.toNat?` itself). -/
+def parseDecNat? (s : String) : Option Nat :=
+  if !s.isNat then none
+  else if s.any (· == '_') then s.toNat?
+  else some (natOfDigits s.toUTF8 0 s.utf8ByteSize)
+
 def parseExprNatLit (json : Json) : M Expr := do
   let .str natValStr := json | fail s!"Expr.lit natVal invalid"
-  let some natVal := String.toNat? natValStr | fail s!"Expr.lit natVal invalid"
+  let some natVal := parseDecNat? natValStr | fail s!"Expr.lit natVal invalid"
 
   return .lit (.natVal natVal)