feat(language): a where counts the coordinates a predicate admits

[FBumann]

Prompt: "Let's build both issues in a Pr stacked onto 566" — "If it helps the code, take the time to refactor or rethink the architecture. Also tell me if some larger refactoring might be reasonable to do" — "Why don't we do sum(predicate) instead of count?"

Prompt: "Id like to merge it in the following order: * more capable where_parser to enable proper assumptions * Implement the assumptions: block * a dedicated count() operator for Predicates (how many are true?), and shift() for Predicates […] Can we arrange them like this?" — "Lets do that"

Prompt: "Review the stack of 602 and below" — "Do 1-3"

Note

The following content was generated by AI.

Closes #590 and #591. Two calls read a predicate where every other operator reads arithmetic: count(<predicate>, over=<dim>) answers a number, shift(<predicate>, along=, offset=) answers a predicate. Together they say what #582 needs a curve to state as language.

Stacked on #589, which is stacked on #566. The chain is 566 → 589 → 592.

What this changes

where: "count(points, over=bp) >= 2"
where: "count(points AND NOT shift(points, along=bp, offset=1), over=bp) == 1"

$$\lvert \{ b \in \mathcal{B} \thinspace : \thinspace \mathrm{points}_{g,b} \wedge \neg \mathrm{points}_{g,b - 1} \} \rvert = 1$$

count reduces the counted dimension away, as sum(over=) does, so the count is one number per remaining coordinate and a claim about each group needs no word for the group. It is compared against a whole number: a count is a number of coordinates, so a fraction and a parameter are both refused, and so is a comparison the count settles on its own — >= 0, < 0, or any negative number — because a count is never negative.

shift over a predicate is false where the translation vacates, and takes no edge=. The arithmetic form needs one because no number is neutral and inventing one changes the answer; false is what a missing row already means in a mask. by=, within= and edge='wrap' are refused rather than ignored, per #591's conservative landing. A keyword written twice is refused as the arithmetic grammar refuses it, rather than the last one winning.

Both are where-only atoms, not BUILTINS rows — the shape position() already has. A row in that table would also put them in BUILTIN_NAMES, which the expression resolver, the unknown-operator message and the golden operator census read, and neither is an operator arithmetic may call. So a count that is not on the left of a comparison — bare, or on the right — gets a where refusal naming count(<predicate>, over=<dimension>) <op> <integer>, not the arithmetic grammar's unknown operator.

A count comparison aligns on its relation. #589 folds the comparisons that are one relation between two sides into Walk.sides behind AlignedComparison. CountComparison is one of them, so an assumption or a constraint whose whole predicate is a count prints with the relation leading the right-hand side, as every other comparison does.

Why this shape

Why count and not sum or len

Not sum(<predicate>), though it would add no name. Summing a predicate means summing its 0/1 values, and that is precisely the coercion the language already refuses:

'flag' is declared dtype: bool, and an expression is arithmetic — only dtype: float and dtype: int bind a column it can be done to. A flag masks rather than scales: name it in a where ("flag", "NOT flag"), which is what a mask is — or declare it dtype: int where the 0/1 is meant to arrive as data and be multiplied by.

Adopting it would make sum mean one thing over a float column and another over a bool one, and that refusal would have to be rewritten to say when a flag does scale. The escape hatch it names — declare the column dtype: int — already serves anyone who wants the arithmetic reading.

There is a conceptual reason under the practical one. shift and at over a predicate are vocabulary-preserving: predicate in, predicate out. Counting is vocabulary-crossing: predicate in, number out. "Any operator takes either vocabulary" is therefore not one rule but two, and naming the crossing operator separately is what makes that visible rather than buried in the argument's dtype. The parser agrees: sum(c > 0, over=g) fails arithmetic at the parse, but sum(points, over=bp) parses as arithmetic on a bare name and never reaches the predicate reading, so the common case would need resolution to re-interpret it by dtype — more special-casing than a keyword, not less.

Not len(). len(x) names the size of a container, and there is no container here: the set being sized is the one the predicate admits, which the file never names. Worse, len(points, over=bp) reads as the size of the axis — a different and also-useful question, and len(snapshot) is the obvious spelling for it. Spending len here would block that.

This does not foreclose porting the others. The grammar production is <name>(<predicate>, kwargs…) for any name; only resolution gates it, which is why sum_back(flag, along=g, window=2) gets a language refusal rather than a parse error today. Adding at over a predicate later is one resolution arm and one program node — no new name, no grammar change.

The architecture, and the two forks taken

count is spelled in the grammar; shift is not. position() needs no grammar rule because it parses as an ordinary call and resolution routes it. count cannot: its argument is a predicate, and the arithmetic call rule takes arithmetic arguments. So the where grammar reads count(<where_expr>, …) itself. Every other predicate-reading call stands where arithmetic cannot — as a bare atom, after the comparison above it has been tried — so one generic production covers it and the name stays free. A single generic production for both was the first attempt and was wrong: it shadowed sum(p_max, over=generator) >= budget, whose operand also parses as a predicate.

A count comparison is its own parse node. Hanging the call off UnresolvedComparisonNode.left widened that field to carry a predicate, and the widening then reached expansion.expand, _side_name and every other reader of a comparison side — nine type errors for one feature. UnresolvedCountNode keeps the widening where the feature is.

A leaf carries its predicate as a Mask, a connective as a bare Predicate. That is the rule the two new nodes follow: a walk recurses through a connective and stops at a leaf, so a leaf's predicate is a field it reads rather than a child. Mask joins CARRIERS in the golden census for the same reason.

A larger refactoring that is now reasonable — not done here

Predicate has sixteen members, and eight of them are one relation between two things: ParameterComparison, RelationComparison, RelationPairComparison, DimensionComparison, DimensionPosition, ExpressionComparison, ArithmeticComparison, and now CountComparison. Each of _atom_dims, _atom_names, _subject_of, _observe, _atom and _check_where_dims carries an eight-way match over them, and adding a ninth meant touching all six. The typesetter's is now one union and one sides helper, which #589 landed.

It is a real cleanup and it is not this PR. It also has a prerequisite and a risk, both now written down: #593 has to land first, because ParameterComparison is the only comparison over parameters the exclusivity check can reason about, and folding it away without the peel would silently stop models loading. And a flat Comparison(left: Term, op, right: Term) makes roughly forty illegal side-pairs representable that the current split makes unconstructable, which matters because reading.md tells consumers they may build predicates themselves.

What this does not do

Contiguous and the curvature conditions are now expressible, which is what #582's checklist asked for, but this PR emits nothing: no piecewise: block writes an assumptions: entry here. That work lands in #582 on top of this branch, which now carries both assumptions: and the two operators.

Stacked on #589, and what the merge took

The base was #566's branch and is now #589's, so the three land as one chain rather than a fan. #589 was merged in, not rebased onto: the hard rule here is never to force-push.

Five files conflicted. Resolved by hand:

• src/math_spec/typesetting/walk.py. feat(language): a model declares what it assumes of its data #589 folds six comparison arms of _where into Walk.sides behind AlignedComparison; this branch had added CountComparison to the old shape. CountComparison joins that union and becomes one elif in sides. TranslatedPredicate stays a branch of _where, because it recurses rather than comparing.
• tests/test_lowering.py, tests/typesetting/test_walk.py. Both sides append cases at the same point. Both kept; feat(language): a model declares what it assumes of its data #589's first rendering case takes back the @EVERY_FORMAT the two blocks shared.
• tests/typesetting/golden/latex.out, typst.out. Regenerated, not resolved.

Format.set_of, which both PRs add with the same body, merged clean, as did the golden fixture and markdown.out. Every generated page was re-run and none moved.

The review round merged #589's review commit in as its own commit (1f5c01c), with one conflict in src/math_spec/resolution.py resolved by keeping both sides' helpers.

Gates

pixi is not installed in this environment, so the gates ran from a uv environment on Python 3.12 with the pinned ruff==0.16.1 and pyrefly==1.2.0. That is a departure from the "prefix every command with pixi run" default.

Run on the head:

gate	result
pytest -q -n 4	1467 passed, 1 skipped (#589's head: 1426 passed, 1 skipped)
ruff check	clean
ruff format --check	137 files already formatted
pyrefly check	0 errors, 10 suppressed
mkdocs build --strict	clean, with the docs.python.org inventory dropped for the run, which the proxy refuses with 403
the schema and the five page generators	no diff
render-tex	30 models rendered before the review commit; not run for it
compile-tex	not run, for want of a TeX distribution
typos, reuse lint	not run, for want of the tools
prettier --check	not run at the pinned version. An unpinned prettier@3 reports mkdocs.yml, and reports it identically on main, so it is the version and not this change. Clean over docs, examples and tools.

The three golden files were regenerated and read: both this branch's counts and #589's Assumptions section print into them.

The review commit (2199a95) was written as eight failing cases first in test_a_shape_the_language_refuses: a keyword given twice for count and for shift, a bare count, a count on the right, a negative literal, >= 0 and < 0, and the by= message no longer speaking of an edge. It removes the one pyrefly suppression the parse-action lambda needed.

Mutation table

Each guard deleted in turn, the suite run, the file restored and the tree
checked clean.

Guard	Caught by
the keyword check on a predicate-reading call	4 × TestAPredicateIsAnOperand::test_a_shape_the_language_refuses
the lowering recursion into a leaf's own mask	test_a_predicate_a_leaf_carries_is_lowered_like_any_other_mask
names_read seeing through both carriers	that test and test_a_count_reduces_the_dim_it_counts_along_away
the undecidable verdict in a case when	test_a_count_is_undecidable_in_a_case_when — and without it the _atom assertion fires, so the two layers agree
the bail-out on an unresolved operand	test_a_name_the_operand_does_not_declare_is_reported_rather_than_walked (both cases)

The last one is a bug this PR found in itself. Resolution collects problems rather than raising, so a failed operand comes back unresolved — and asking it for its dims asserted instead of refusing. count(nope, over=g) >= 2 raised AssertionError: UnresolvedNameNode reached a predicate walk unresolved. The test was written against that failure first.

This table was measured before the merge with #589; the review re-measured the first, fourth and fifth rows after it, and they hold.

Coverage, and what the fixture gained

• TestAPredicateIsAnOperand holds every shape: seven the language admits, nineteen it refuses, the undecidable case, the unresolved operand, and the dim rule.
• Two lowering tests: a comparison of expressions inside a count is rebuilt like any other mask, and a translated predicate keeps what it reads in names_read.
• Three rendering tests, two of them in every format, including the primed dummy a count takes when the counted dimension is already quantified.
• The golden fixture gains counted, counted_here and run_start, so both new arms of the walk print into a committed file and the line census reaches them. Mask joins CARRIERS in the node census: it is a wrapper the walk steps through, like Direction and Partition.
• Not done, on purpose: no test asserts a count inside an assumptions: entry, though the merge makes one expressible and sides prints it. That pairing is feat(language): a model writes its formulations out on request, and a curve prints as the curve it states #582's, which is the PR that writes such an entry. shift(<predicate>, offset=0) loads as the identity, as the arithmetic shift does. 2.0 is admitted as a whole number where the grammar page writes INTEGER.

🤖 Generated with Claude Code

https://claude.ai/code/session_01DBU3ocfqkHe99mWmxijw64

https://claude.ai/code/session_01EQHKbwGtpVBm6yKHzrjMx9

https://claude.ai/code/session_019tCWoetBmjF1LpbTbjQY29

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34692302 | 📁 Comparing 2199a95 against latest (11a8a2e)

  🔍 Preview build  

25 files changed · + 1 added · ± 24 modified

+ Added

• reference/language/assumptions/index.html

± Modified

• CHANGELOG/index.html
• about/limits/index.html
• examples/commitment/index.html
• reference/language/index.html
• reference/notation/index.html
• reference/reading/index.html
• reference/typeset/index.html
• reference/language/expressions/index.html
• reference/language/file/index.html
• reference/language/piecewise/index.html
• and 14 more...