feat(program): a where leaf carries the dims it is read through, so any predicate answers its own questions

[FBumann]

Prompt: the consumer's review, relayed with "Do it" — "resolve dims onto the leaves, not onto the mask … the vocabulary already has the precedent: LookupComparisonNode.over is copied off the declaration at resolution."

Note

The following content was generated by AI.

The three leaf classes that name a parameter or variable — ParameterComparisonNode, ParameterDefinedNode, VariableDefinedNode — carry dims: tuple[str, ...], stamped by resolution off the declaration, exactly as a lookup leaf carries over. Everything downstream of the old name→dims mapping then falls:

• Mask is root-only again — dims becomes a derived property like conjuncts, the one denormalized field in the vocabulary is gone, and a hand-built Mask(root, wrong_dims) stops being expressible.
• A synthetic predicate answers its own questions. Mask(NotNode(root)) and Mask(a) & Mask(b) answer dims correctly with no mapping — the consumer's region complements and conjunctions stay in-language. Mask.negated() carries the double-negation fold (previously private in lowering._negated, re-derived without the fold downstream — one rule, two homes, one wrong) and & the conjunction.
• NameDims, dims_read, dimensions._name_dims, _Lowering.name_dims all die, and free atoms/names_read follow conjuncts into privacy — Mask is now actually the one public door, closing the asymmetry the review named.
• Namespace gains the name→dims map resolution stamps from — the fact's one home, beside the dtypes it already carries.

What lpspec removes or changes

PolarsCompiler.name_dims and every dims_read(root, mapping) call site collapse to Mask(root).dims; NotNode(r.when) for complements becomes r.when.negated() and gains the fold it was missing; both_regions' AndNode(a, b) can stay or become Mask &. Nothing keeps a name→dims copy anywhere.

Verified

pixi run ci exit 0: lint clean, 938 passed (931 + synthetic-predicate dims, the fold and algebra tests, the unresolved-refusal pin, the load-refusal cases, and a double-negation case on the load path), mkdocs build --strict builds, 27 TeX documents compile. schema/ and golden outputs byte-identical.

The literal invariant, after the consolidated review — one fold, applied at the door, with the crashing shape refused at load:

• A case arm whose mask folds to a literal is refused at load — True makes every other arm unreachable, False never applies, and the typesetter has no region to draw for either (its assert not node.value crashed on the shape before). The refusal names the rewrite; the crash class predates the stack.
• _fold has one home (program, beside the vocabulary), now cancels a double negation, and is applied in Mask.__post_init__ — so Mask(OrNode(True, x)), the composition the docs invite, folds at the door, negated/& shrink to one-liners, and __or__ completes the algebra. Resolution imports the same fold for where_of and case arms (via an _arm_mask helper whose docstring carries the kept-literal reason).
• The unresolved-tree refusal is a whole door: Mask.__post_init__ exhausts _atoms, so Mask(parse_where(...)) raises at construction — conjuncts, negated and & can never see an unresolved leaf a raising atoms would have caught later.
• The typesetter reads each where-leaf's dims off the leaf (node.dims), retiring its three schema re-derivations — the second home this PR exists to delete.

Mutation table

Each guard deleted in turn on the committed tree, restored with git checkout --:

Mutation	Result
resolution stamps () on parameter comparisons	11 failed
_atoms' unresolved arm deleted	1 failed
the literal-arm refusal dropped	2 failed
_fold's double-negation cancel dropped	2 failed
the constructor's fold dropped	1 failed
the constructor's unresolved refusal dropped	1 failed
restored	938 passed

Trade named: resolved trees are now spec-bound — a leaf embeds its declaration's dims — which they already were in substance, being typed against the namespace. A hand-built leaf with wrong dims is still expressible; the trust boundary moves to resolution, where it already lives for over.

Stack: fifth, on #323 → #321 → #319. Supersedes the stored-dims design #319 introduced and retracts #321's "free question functions stay public" line — with the resolution the same reviewer proposed in its place.

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34335246 | 📁 Comparing e803063 against latest (18644cd)

  🔍 Preview build  

7 files changed · ± 6 modified · - 1 deleted

± Modified

• reference/language/reading/index.html
• reference/math_spec/dimensions/index.html
• reference/math_spec/program/index.html
• reference/math_spec/resolution/index.html
• reference/math_spec/validation/index.html
• reference/math_spec/typesetting/walk/index.html

- Deleted

• reference/math_spec/where_parser/index.html

[FBumann]

Note

The following content was generated by AI.

Superseded by #327, which combines the reviewed stack into a single diff on the maintainer's call. The review history — two consumer reviews and one consolidated agent review, with mutation tables — lives in this stack's bodies; the tree at #327 is byte-identical to the stack's top.