Repository navigation
remove specialization masks in safe.ts - #1353
Merged
Lorenzobattistela merged 2 commits intoOct 6, 2026
Merged
Conversation
toprameen
marked this pull request as ready for review
October 5, 2026 19:39
Lorenzobattistela
requested changes
Oct 6, 2026
Lorenzobattistela
left a comment
Collaborator
There was a problem hiding this comment.
Thanks, this is a clean follow-up to #1203. Since #1203, spec_of was always a leading prefix of tld.x trues, so storing the count instead of the array is exact. It relies on two things the parser guarantees: a ~ only comes on leading clauses or binders, and a def that fills a law has tele.length >= law.x, so x <= n always holds.
I checked it merged onto main 53fc961, using main's own gate files:
- repo 50/50, ping 47/47, test 1577/1577
- perf 123/124, the same as main (a first run showed 120/124 from node contention; the rerun matches)
gates/safe.ts tests: the table is byte-identical to main's (1018 agree, 0 timeouts; the one false reject, agree_32, is already on main)-o: everytests/*/*.bendemitted on both trees; all 1577 exit codes match and all 1090.bendttfiles are byte-identical
So the change has no effect on output. Two small nits, neither blocking:
spis aboolean[]on main and a count after this PR (inargsand ingroup_emit'srest). Code that still doessp[j]on a number getsundefinedwith no type error, and every parameter silently counts as unspecialized. A name likenxwould make- The comment on the deleted
spec_ofwas the only placesafe.tssaid which parameters get specialized. The new code also depends on those parameters one-line comment atroot_colsorargs(e.g. "a def's first x parameters, its ~ ones, are specialized") would keep that rule written down.
toprameen
force-pushed
the
simplify-specialization-prefix
branch
from
October 6, 2026 17:52
b3da467 to
4649752
Compare
Lorenzobattistela
approved these changes
Oct 6, 2026
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.
Replace
spec_of’s boolean arrays with declaration arity and the template prefix count. Checked templates have a contiguous leading prefix; datatypes and term heads keep prefix zero.Local checks: repository gate and whitespace check pass. Exact BendTT text and out-of-scope results match on 331 checked books, including a focused fixture, with four repeated-call comparisons and 15 direct boundary checks. All 14 local BendTT verdict comparisons match the baseline; 13 CLI verdicts pass and five parser diagnostic pins match.