feat(program): a resolved where is a first-class Mask whose leaves carry their dims, and the where grammar is package-private - #327
Merged
Conversation
…rry their dims, and the where grammar is package-private Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01D59sEp5d7CecJAwrzACbRh
This was referenced Sep 1, 2026
Closed
Documentation build overview
7 files changed ·
|
This was referenced Sep 1, 2026
Merged
FBumann
added a commit
that referenced
this pull request
Sep 1, 2026
…sed, and the refusal says what actually breaks (#336) The rule landed in #327 with no home on the reference page a file's author reads, and its wording framed the cases as ordered. Cases are kept apart by proof rather than ranked, so an always-true arm is not one that shadows the arms under it — it is one no other arm can be proved apart from, leaving `otherwise:` nothing. The refusal says that, out of a named helper whose docstring carries the reason. `expressions.md` gains the rule beside the other two the cases are held to, quoting the refusal verbatim, and says why a declaration's `where:` is not held to it. The where-string table's literal row gains the double negation the fold also cancels. Claude-Session: https://claude.ai/code/session_01BJfy8K5XfxLmX5Tq5YW71b Co-authored-by: Claude Opus 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.
Note
The following content was generated by AI.
A resolved
wheretravels as one thing: aMask, built at resolution's single door and answering every question the language owns about it —conjuncts,names_read,atoms, anddims, read off leaves that carry their declarations' dims the way a lookup leaf carriesover. The algebra is total and self-folding (~,&,|; a literal flips or is absorbed, a double negation cancels, construction refuses an unresolved tree), the resolved node vocabulary lives inprogrambeside everything else a consumer dispatches on, and the where grammar is package-private with exactly two internal importers.One acceptance change: a case arm whose mask folds to a literal is refused at load —
Truemakes every other arm unreachable,Falsenever applies, and the typesetter (which previously crashed on the shape) has no region to draw for either. The refusal names the rewrite.Supersedes #317, #318, and the reviewed stack #319 → #321 → #323 → #324, combined into one diff on the maintainer's call — nothing had merged, and the intermediate shapes (a stored
Mask.dims, aNameDimsalias, public free question functions) never reachmain. The four stacked PRs hold the full review history: two external reviews from the consumer and one consolidated agent review, every finding either implemented and mutation-verified or declined with the reason recorded.Verified
pixi run ciexit 0 on this branch (lint incl. pyrefly clean, 938 passed,mkdocs build --strict, 27 TeX documents compiled), and the committed tree is byte-identical to the stack's top (feat/leaf-dimsate803063), whose remote CI — GitHub Actions and Read the Docs — is green.schema/andtests/typesetting/golden/untouched throughout: nothing that renders changed output, only who computes it.Guards land with the tests that fail without them, mutation-verified on the stack (tables in #324's body): wrong leaf dims at resolution → 11 failures; each fold arm, the literal-arm refusal, and the unresolved-tree refusal → 1–2 targeted failures each; full suite green on restore.
What consumers migrate:
dims_read(root, name_dims)call sites and any hand-built name→dims mapping becomeMask(root).dims;NotNode(r.when)complements become~r.when; imports ofwhere_parser's resolved names move toprogram(the old module path now raisesModuleNotFoundError; sweep wholesale).Deliberately not done:
Program.name_dims(no consumer asks now that leaves carry dims); per-leafdims_readproperties (would spread_atom_dims's one rule across eight homes); splittingexpression_parserthe way_where_parserwas split (__init__'s docstring records that its door stays open until something asks); suffix-free node renames (aliases refused on principle, and theNodesuffix disambiguates against the expression vocabulary sharing the module).Breaking throughout, described here rather than in the title per the refused breaking-marker rule.