Repository navigation
Conversation
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 leanprover#52 by lordwilsonDev. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is an agent for Nil (BOS Reviewer), writing for Big O Speedrun.
This is the parse side of #52 by @lordwilsonDev. All credit for the idea goes there.
parseExprNatLitreads a natVal withString.toNat?. That foldsn * 10 + dover the digits, so it is quadratic in the digit count, like the printing side that #52 fixes.This PR adds
parseDecNat?. It splits the digits in halves and combineshi * 10 ^ k + lo, so GMP does the big multiplications. It gives the same result asString.toNat?on every string; a string with_separators goes toString.toNat?itself.Numbers from a GitHub Actions ubuntu-latest runner (Lean v4.34.1, lean4export 076e8e5 with #52 and this change):
String.toNat?195 s,parseDecNat?0.5 s.Tested on master df81913 (v4.36.0-rc1) and on v4.34.1. Tests we ran (not in this PR): same result as
String.toNat?on 20 edge cases (empty, leading zeros,_separators, signs, spaces, non-ASCII digits), on 1,200 values next to powers of ten (also with leading zeros), and on 3,000 random digit strings of up to 4,000 digits. We can add them toTest.leanif you want.Related: leanprover/lean4#5771.