Skip to content

perf: back Text by an array instead of List.Vector - #2

Open
jonaprieto wants to merge 4 commits into
mainfrom
perf/text-array-input
Open

perf: back Text by an array instead of List.Vector#2
jonaprieto wants to merge 4 commits into
mainfrom
perf/text-array-input

Conversation

@jonaprieto

@jonaprieto jonaprieto commented Jul 5, 2026

Copy link
Copy Markdown
Owner

This is just an experiment to run the benchs. For example on could rework the Text to see what's the impact. Say input from List.Vector Char n to an array-backed structure with a single-pass decoder, so parsing no longer pays for O(n) list construction on large inputs. Comment /bench to see the impact vs base.

Comment /bench on a PR to build and run the prim-parser and lean4-parser
benchmarks and post a results table back as a sticky comment. Restricted to
commenters with push access.
Replace the `List.Vector Char n` input with an array-backed `Text` (array +
offset + length invariant), decoded from a String in a single pass via
`@[implemented_by]`. `anyChar` now indexes the array instead of matching a cons
cell, avoiding the O(n) list construction that dominated large inputs.
@jonaprieto

Copy link
Copy Markdown
Owner Author

/bench

@github-actions

github-actions Bot commented Jul 5, 2026

Copy link
Copy Markdown

Benchmark results

PR 281926a04fa04f90f34ebe936c0428e1173ef6c9 vs base 45e652102a7833b13c2f52bbbff0f85760436ce4 — min ms over the repetitions. Δ = PR vs base, lower is better. lean4-parser is an external reference.

grammar prim PR ms prim base ms Δ lean4-parser ms
integers 26.29 25.63 +2.5% 6.36
sexp 19.41 18.98 +2.3% 3.18
csv 17.59 17.53 +0.3% 4.61
json 90.13 89.53 +0.7% 6.39
lambda 5.52 5.55 -0.6% 0.94

@jonaprieto

Copy link
Copy Markdown
Owner Author

/bench

1 similar comment
@jonaprieto

Copy link
Copy Markdown
Owner Author

/bench

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant