Repository navigation
perf(parse): a name finds its binder through an index, not a scan of every local - #2064
Open
nicolas-abril wants to merge 4 commits into
Open
nicolas-abril wants to merge 4 commits into
nicolas-abril wants to merge 4 commits into
Conversation
…every local Parse keeps idx, each name's binders on stk, newest last. parse_push adds to both, parse_close pops both back to the mark, and parse_var reads the newest binder of its name directly instead of walking stk (bendlang#2046). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ads its last Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…sses 4096 names 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.
The parser part of #2046.
parse_varlooked up a name by walking the scope stackstkfrom the newest binder down. Every use of an outer variable passed all the locals bound after it, and every global name (Unit,U32.add, …), which is never on the stack, passed all of them. n locals and n uses cost O(n²).Parsenow also keepsidx: each name's binders onstk, newest last.parse_pushadds to both (parse_openand the rewrite binder's hidden_go through it),parse_closepops both back to the mark, andparse_varreads the newest binder of its name directly.stkand its length marks stay as they were. The parser has no try/catch backtracking: every binder it opens is closed byparse_closebefore its scope's mark is reused, soidxalways matchesstk.The conversion part of #2046 (
term_higher'slist_get) and its match-lowering part (in #2062) are not in this PR.Load times (in-process
book_load, best of 12)On the checker benches the scope lookup (
parse_var,parse_open,parse_close) falls from about 8.4 ms to 6.4 ms of parse time per run (CPU profile, 9 runs over generics_3200, defs_12800 and proofs_3200): their defs bind few locals, so the gain there is small.Checks
.bendfile undertests/(1851 files) prints the same output with--check-onlyas on main, error messages included.bend.ts45508 → 45593 ttok (cap 48000)._run.ts): repo 56/56, ping 83/83, perf 122/124 (the same cluster cells main fails today: merkle and nbody, compile and GPU time). Test gave 1830/1838 under_run, failing the io/gfx tests that stale/tmp/bend_io_*files on some cluster nodes break, and 1838/1838 in a separate run of the test gate.🤖 Generated with Claude Code