feat: cases on a named expression, and referencing one

[FBumann]

The feature from #2, stacked on #33 (which is stacked on #31) — base is claude/constraint-cases. Retarget down the stack as each lands. #37 has been folded back in: it fixed a defect this PR introduced and rewrote nine of the files this PR writes, so the two are one change.

Implements @FabianHofmann's proposal, with the decisions taken in #2.

What this adds

expressions: takes cases:, with foreach: naming the frame they partition:

expressions:
  previous_status:
    description: the commitment state a unit carries into a snapshot
    foreach: [snapshot, generator]
    cases:
      always_on: { when: "not committable", expression: 1 }
      boundary:
        when: "committable and position(snapshot) == 0"
        expression: status_initial
      interior:
        when: "committable and position(snapshot) > 0"
        expression: shift(status, over=snapshot, offset=1)
constraints:
  no_restart:
    foreach: [snapshot, generator]
    expression: status - previous_status <= 1

Three independent regimes multiply into eight constraint cases and add into seven expression cases — and the inequality using them is written once instead of eight times, so changing it is one edit rather than eight that nothing checks agree.

The rules it enforces

The cases must partition the frame, and it is a load error when they do not — decided before any data binds by #33's procedure, with the overlap or the gap named and a witness for it:

Named expression 'x': the cases do not partition ['generator', 'snapshot'] — no case claims the value where committable is true, the position of snapshot is 1

Disjoint, because two values at one coordinate is not a quantity. Total, because a gap would leave the expression undefined there and absence spreads — every constraint referencing it would lose rows it never masked, which is what diagnostics().omissions exists to catch. Totality is what keeps a constraint's row set readable at the constraint.

Being total is not free, and the tests show the price: with no mask to narrow the frame, the cases have to say what an absent parameter or an unnamed label gets.

when:, not where:. A case selects which value a coordinate takes; it creates no absence and deletes no row, which is what where means on every other block (rule 6). A cased expression has no where of its own, so the word would be free to mislead.

foreach: required with cases, refused without. An uncased expression's dims fall out of its body; a cased one's cannot, since a case may be a scalar where its when is not — always_on above is exactly that. Each when is held to the frame by _check_where_dims, the same check in the same words that holds a variable's or a constraint's mask to its; each case's value must sit inside the frame too.

The two forms do not mix. One expression: or a set of cases:, never both and never neither — with the near-miss named in each direction.

What a reference expands to

A name reaching a cased expression expands to CasesNode, a core arithmetic node carrying every arm. The partition proved on the declaration is what makes that a value rather than a choice: exactly one arm applies at each coordinate, decided without data, so a consumer selects per row the way a where already filters — nothing about the shape of the plan depends on data.

Every dispatcher gains the arm (expansion, resolution, dims, degree, boundedness, the typeset walk), which pyrefly's assert_never exhaustiveness is what enforces. The dims of a reference are the declared foreach, not the union of the arms: an arm narrower than the frame broadcasts, exactly as a parameter with fewer dims does. Arms are substituted through, so a case body may name another expression, and a macro template may name a cased expression.

How it prints — the half that was #37

A cased expression is the one named expression that does not inline. Rendered as an atom, the block printed where the name stood, and a three-arm block is three rows tall, so whatever follows it in the equation sits beside the middle arm:

\text{ramp\_up} && p_{t,g} - p_{t \boxminus_{0} 1,g} & \le \mathit{ramp\_limit}_{g} \cdot \begin{cases} 1 & \text{if } \neg \mathit{committable}_{g} \\ \mathit{status}^{\mathrm{initial}}_{g} & \text{if } \mathit{committable}_{g} \wedge \mathrm{pos}(t) = 0 \\ \mathit{status}_{t - 1,g} & \text{if } \mathit{committable}_{g} \wedge \mathrm{pos}(t) > 0 \end{cases} + \mathit{start\_up\_limit}_{g} \cdot \left( 1 - \begin{cases} \ldots \end{cases} \right) &&& \forall\, t \in \mathcal{T},\ g \in \mathcal{G}

That is one row of examples/commitment.yaml, not a contrived model: the reader's eye lands on \wedge \mathrm{pos}(t) = 0 \cdot \mathit{start\_up\_limit}_g, and the same three arms print twice because ramp_up names the quantity twice. A quantity written once in the file was written once per use on the page, which is the opposite of what naming it was for.

So a use prints the symbol:

$$p_{t,g} - p_{t \boxminus_{0} 1,g} \le \mathit{ramp_limit}_{g} \cdot \mathit{previous_status}_{t,g} + \mathit{start_up_limit}_{g} \cdot \left( 1 - \mathit{previous_status}_{t,g} \right) \qquad \forall\thinspace t \in \mathcal{T},\enspace g \in \mathcal{G}$$

and the block prints once, under a new Definitions section between Subject to and Variable domains — where a paper states a quantity defined by region:

$$\mathit{previous_status}_{t,g} = \begin{cases} 1 & \text{if } \neg \mathit{committable}_{g} \cr \mathit{status}^{\mathrm{initial}}_{g} & \text{if } \mathit{committable}_{g} \wedge \mathrm{pos}(t) = 0 \cr \mathit{status}_{t - 1,g} & \text{if } \mathit{committable}_{g} \wedge \mathrm{pos}(t) > 0 \end{cases} \qquad \forall\thinspace t \in \mathcal{T},\enspace g \in \mathcal{G}$$

The section is named Definitions rather than the conventional where, which in this repo is a keyword and would read as the wrong thing.

CasesNode already carries name and foreach, so the walk needs nothing new from the AST: rendering one records it and returns the indexed symbol. definitions() then prints what the other sections reached — so it runs after them, and to a fixpoint, since an arm may name another cased expression. An expression nobody names prints nothing.

Symbols. Cased expressions join the symbol pool, deriving a symbol like any other name, and --symbols can rename one. Uncased expressions stay out: they print nothing under their own name, so a table entry for one would never apply — the silent-typo failure the table is strict about.

The asymmetry is deliberate and is the one thing worth arguing with. test_macros_and_named_expressions_are_expanded_away still holds for every other named expression; a cased one is the exception. The defence: it is the only kind that cannot inline legibly, and the only kind whose declaration a reader has to see to check the regions.

The format seam gains cases() — \begin{cases} in LaTeX, cases() in Typst, and \cr rather than \\ in Markdown, whose escape pass eats one of the two backslashes before MathJax sees them. The golden model carries a cased expression and a constraint naming it, so the three .out files and the walk's line-coverage guard cover the new arm.

An example, and the bug writing it found

examples/commitment.yaml is the formulation #2 factors: ramp_up holds a running unit to ramp_limit and a starting one to start_up_limit in one inequality instead of three. tools/render_tex.py picks it up like every other model, so the LaTeX gate compiles it, and it gets a page in the example gallery #38 added.

Writing it turned up a bug in the documented example: expression: 1 is how a constant case is spelled, YAML reads it as an int, and the annotation took only a string — so the block in expressions.md did not load. Nothing caught it because no test loads the page's snippets. A number is now accepted wherever an expression string is declared, and the checked-in JSON schema says so, since a mode='before' rewrite is otherwise invisible to it. Booleans still fail: true is not arithmetic, and an error naming the type reads better than one naming 'True'.

What is deliberately not here

Macros are a follow-up. Cases there are safe only under a stronger obligation — provable with the names uninterpreted, since a macro has no frame until it is called.

Scope

model.py (ExpressionCase, ExpressionBlock gaining foreach/cases with the form validator and round-trip serialiser, and the number coercion), validation.py (resolve each case, run the partition check), dimensions.py (the frame checks, beside the ones for variables and constraints), expansion.py (CasesNode where the name stood), expression_parser.py (the node), resolution.py/degree.py/boundedness.py (the dispatch arms), typeset/ (the format seam, the symbol at the use site, definitions(), the section and the ordering the collection needs, printed_expressions and the table's accepted names), the regenerated JSON schema, tools/notation.py, expressions.md, notation.md, examples/commitment.yaml and its gallery page, the golden fixture and its three outputs, and tests.

The gallery page is regenerated rather than hand-edited, and tests/test_docs.py is what catches it going stale — which is what that test is for.

schema/math-spec.schema.json is regenerated by tools/schema.py and pinned by tests/test_schema.py; it is outside prettier's *.{md,yml,yaml} glob, and main's copy fails prettier --check identically — generator-owned, like CHANGELOG.md.

Checks

Gates reproduced with a 3.13 venv on the versions pixi.toml pins plus prettier@3.9.3: ruff format and check clean, pyrefly 0 errors, reuse lint compliant, typos clean, prettier clean over its own glob, mkdocs build --strict clean, 425 passed — including the Typst compile and the walk's line-coverage guard, which the bare install skips. Every equation quoted above is the renderer's own output, not written by hand.

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34195480 | 📁 Comparing 35d62ac against latest (b97a1df)

  🔍 Preview build  

42 files changed · + 5 added · ± 37 modified

+ Added

• examples/index.html
• examples/commitment/index.html
• examples/dispatch/index.html
• examples/operators/index.html
• reference/math_spec/partition/index.html

± Modified

• 404.html
• index.html
• CHANGELOG/index.html
• contributing/index.html
• installation/index.html
• about/ceiling/index.html
• about/what-counts-as-language/index.html
• reference/language/index.html
• reference/notation/index.html
• reference/typeset/index.html
• and 27 more...

[FBumann]

Heads-up: I pushed a behaviour change to this branch, not just a rebase, and it should be reviewed as one rather than inherited.

Why

This branch is now rebased onto main at 13da65d, which carries the notation convention from #44 — upright is what the model is given, italic is what the solver chooses — and the whole-page guard from #46, which asserts every \mathit on the page names a quantity the solver decides.

The rebase failed that guard immediately: startup_cost printed italic, and both of its arms (cost * p_max, cost) are parameters. A quantity written in two regions is still given when every region is — the number of regions says something about the frame, not about who decides the value.

What changed

typeset now works out which cased expressions reach a variable, which Symbols cannot do for itself because it has no namespace to resolve an arm against. The walk runs over the resolved arm, so an arm naming another cased expression answers for that one's arms too.

	arms	prints
startup_cost	cost * p_max, cost	$\mathrm{startup_cost}$ — given
committed_power	p, 0	$\mathit{committed_power}$ — chosen

committed_power is new in the fixture: with only startup_cost, the page showed the rule holding in one direction and nothing testing the other.

The line it draws, and the one to argue with if you disagree. Only a case's value is scanned, never its when. A variable in a mask asks whether that variable exists at a coordinate — which the model settles when it is built, not something a solver returns — so a cased expression whose every arm is a parameter is data however its regions are cut. That was already true of the implementation; it now has a test, because the obvious "fix" for whoever meets it next is to scan both halves.

Two of this branch's own tests moved to upright with the change — CASED's headroom is a parameter in every arm — and one now counts the indexed symbol, since Typst spells a row label and an upright symbol identically and only the symbol carries the dims.

Checks

461 passed, ruff check and format clean, pyrefly 0 errors, prettier and typos clean, goldens and all four generated pages re-run. CI is green on d8c68bb.

Revert the top commit if you would rather decide this differently — the branch is red against main's guard without some answer to it, but this particular answer is yours to keep or change.

---

Generated by Claude Code

[FBumann]

Superseded by #70, which lands the same feature — cases: on a named expression, the partition rule, the Definitions section — through a different rule about what a case set is.

The difference. Here the arms are an unordered set required to be a proved partition: pairwise disjoint and jointly exhaustive, decided before any data binds by #33's decision procedure, with the overlap or the gap named and a witness for it. In #70 the arms are ordered, first match wins, and the last one carries no when: at all.

That gives the same two guarantees — exactly one value per coordinate, and a value at every one — by making the bad states unrepresentable rather than diagnosed. Two arms cannot disagree, because only the first to match is read; no coordinate is left without a value, because the fallback has no condition to fail. Both are properties of the shape of the block, so nothing has to decide what a predicate could be true of.

What that removes:

• feat: a static partition check for expression cases #33 is not needed at all — 945 lines of cell enumeration over where-atom subjects, and the coupling that came with it: every where atom added later would have had to teach partition.py about its cells, or the procedure would silently get more conservative. Closed alongside this.
• The wiring here shrinks to two form validators. _check_cases, _resolved_when, the witness-bearing message and the "a when did not resolve, so the partition would misreport" bail-out are all gone.
• The math gets shorter. With disjointness enforced rather than proved, arms stop restating each other's negations — boundary and interior in this PR's own example drop the committable and … they needed here, and the printed block loses a conjunction per row.
• It prints the way papers write it. \text{otherwise} on the last row, which format.cases's docstring here specifically defended not having.

What it costs, stated plainly: a fully shadowed arm is now silently dead rather than a load error, and the arms are read top-down instead of as an unordered set. \begin{cases} rows are read top-down anyway.

Two other things carried across, changed. _touches_a_variable — the reflective is_dataclass/vars() walk behind the given/chosen cut — never descended into a CasesNode, because arms is a tuple and the walk only unpacked list and dict. So a cased expression whose only route to a variable ran through another cased expression printed upright, as data the model was handed. #70 uses degree.carries_variable over the typed AST instead, which is the same predicate and stays inside the assert_never exhaustiveness discipline; there is a regression test for the chain. And Symbols takes the namespace positionally rather than a defaulted chosen, so that cut cannot be forgotten into silence — the test file here had a call site that already did forget it.

#70 is also based on current main: typeset/ is typesetting/ since #54, and #52's named node groups mean CasesNode joins BranchNode and reaches degree, boundedness and the dim algebra through children(), so four of the dispatch arms written here are no longer needed.

The number coercion (expression: 0) and the examples/commitment.yaml example came across as they were.