feat: cases on a named expression, read in order with a fallback

[FBumann]

Implements the feature from #2. Supersedes #36 and #33, which took the same feature through a proved static partition; this takes it through the shape of the block instead.

Note

The following content was generated by AI.

expressions: takes cases: — an ordered set of arms over a declared foreach:, the last of them the fallback. The value at a coordinate is the first arm whose when holds there; the last arm carries no when. So the quantity has exactly one value at every coordinate, and a value at every coordinate — both by the shape of the block rather than by anything a checker establishes, which is why #33's 945-line decision procedure is not needed at all.

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: "position(snapshot) == 0", expression: status_initial }
      interior: { expression: shift(status, over=snapshot, offset=1) }
constraints:
  no_restart:
    foreach: [snapshot, generator]
    expression: status - previous_status <= 1

Three regimes, one quantity, and the inequality using it written once instead of three times that nothing checks agree.

Three commits, each green on its own:

1. feat(language): a named expression may write a constant as a number — the bug writing the example found, separable from cases:.
2. feat(language): a named expression may give a value per region — the construct and its printing. The two halves do not separate: CasesNode joins ArithmeticNode, and test_the_golden_model_carries_every_node_kind_the_walk_renders holds the walk to get_args(ArithmeticNode).
3. docs: unit commitment, the model cases exists for — the example, its gallery page, the nav entry. Cherry-picks cleanly if it should be its own PR.

Checks. pixi run ci clean on 9a215da: lint (ruff, pyrefly 0 errors, reuse, typos, prettier), 745 passed, mkdocs build --strict, and 27 TeX documents compiled — the new example among them. Every equation quoted below is the renderer's own output.

The rule that makes it a quantity

The arms are read in order, and the last one carries no when:.

The value at a coordinate is the first arm whose when holds there; the last arm has no condition and covers everything the arms above it leave. So the arms cannot disagree — only the first to match is read — and the quantity has a value everywhere, because the fallback has no condition to fail. Nothing has to decide what a predicate could be true of, and there is no case set that loads and later turns out to have a hole in it.

Totality is not a nicety. A gap would leave the quantity undefined there, and absence spreads — every constraint referencing it would lose rows it never masked, which is what diagnostics().omissions exists to catch. A cased expression being total is what keeps a constraint's row set readable at the constraint. It is not free, and the example shows the price: with no mask to narrow the frame, the fallback has to say what an absent parameter or an unnamed label gets.

The near-miss is named in each direction: a fallback that is not last, no fallback at all, one case, both forms, neither form, a foreach: without cases, and — the typo this design invites — where: inside a case:

expressions.x.cases.a: unknown key 'where' in an expression case. Did you mean 'when'?

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 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.

Why this is not #36

#36 required the cases to be a proved partition — pairwise disjoint and jointly exhaustive, decided before any data binds by #33's 945-line decision procedure, with the overlap or the gap named and a witness for it. The error messages were genuinely good.

Ordered arms with a mandatory fallback give the same two guarantees by making the bad states unrepresentable rather than diagnosed. What that buys:

• 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.
• The wiring here shrinks to two 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, the arms no longer restate each other's negations: boundary and interior above drop the committable and … that feat: cases on a named expression, and referencing one #36's version needed, and the printed block loses a conjunction per row.
• It prints the way papers write it — \text{otherwise} on the last row, which feat: cases on a named expression, and referencing one #36's format.cases docstring 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 must be read top-down instead of as an unordered set. \begin{cases} rows are read top-down anyway.

What a reference expands to

A name reaching a cased expression expands to CasesNode, a core arithmetic node carrying the name and every arm in file order — and not the frame, which is on the declaration that every consumer needing it already holds. Because it joins BranchNode (#52's named groups), degree, _adds, is_quadratic, _degree and boundedness' variable walk all reach the arms through children() — only expansion, resolution, the dim algebra and the typeset walk needed an arm of their own, and pyrefly's assert_never is what enforced that. Arms are substituted through, so a case body may name another expression, and a macro template may name a cased expression.

Verified by probe, and unchanged by this PR because the existing walks already cover it: a self- or mutually-referential cased expression is caught by the existing cycle check; _degree takes a max over arms rather than a sum, so p * p * x is still refused at degree 3; a piecewise: link may name a cased expression; a bound still refuses any named expression.

How it prints

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 — and a quantity written once in the file is 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 \mathrm{ramp_limit}_{g} \cdot \mathit{previous_status}_{t,g} + \mathrm{start_up_limit}_{g} \cdot \left( 1 - \mathit{previous_status}_{t,g} \right)$$

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 \mathrm{committable}_{g} \cr \mathrm{status}^{\mathrm{initial}}_{g} & \text{if } \mathrm{pos}(t) = 0 \cr \mathit{status}_{t - 1,g} & \text{otherwise} \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.

Every declared cased expression prints, used or not, in declaration order — the rule a variable's domain already follows. definitions() therefore iterates the declarations and resolves each one the way constraints() resolves a constraint, rather than collecting what the other sections happened to reach: no reached-set on Walk, no fixpoint over arms that name further cased expressions, and no ordering dependency between the sections of the document. printed_expressions returns a tuple rather than a set precisely because the section's row order is the file's; test_the_definitions_print_in_declaration_order declares six of them so a shuffle cannot pass by luck.

Which arm is the fallback is a fact about the math, so the walk chooses between if and otherwise and a Format only stacks the rows — the split typesetting/README.md states. Format.cases takes (value, condition) pairs both already rendered.

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.

Given or chosen. A cased expression is on whichever side its arms put it: one whose every arm is data prints upright, however many regions it is cut into; a when naming a variable does not move it, since that asks whether the variable exists, which the model settles when it is built. The chain is followed all the way — chosen_expressions resolves each arm and asks degree.carries_variable, which walks another cased expression's arms too, so a quantity whose only route to a variable runs through a second cased expression still prints italic.

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. The row separator is a cases_row class attribute, the shape dash and operators already use: Markdown overrides it with \cr rather than \\, 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, the Typst compile and the walk's node-coverage guard all cover the new arm.

The 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.

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 in this repo loads the page's snippets. A number is now accepted where a named expression or one of its cases declares its body, and the checked-in JSON schema says so, since a mode='before' rewrite is otherwise invisible to it. A constraint, an objective and a piecewise: link are untouched: none of them is a bare number. Booleans still fail: true is not arithmetic, and an error naming the type reads better than one naming 'True'.

That fix is the first commit, and stands on its own.

Scope, and what is deliberately not here

Cases in a macro template are a follow-up. The fallback would have to cover a frame the macro does not have until it is called.

model.py (ExpressionCase, ExpressionBlock gaining foreach/cases, the two form validators, the round-trip serialiser and the number coercion), expression_parser.py (CasesNode/CaseArm, joining BranchNode and children()), expansion.py (CasesNode where the name stood), resolution.py and dimensions.py (the dispatch arms and the frame checks, beside the ones for variables and constraints), validation.py (resolve each case), typesetting/ (the format seam, the symbol at the use site, definitions(), the section, and the given/chosen cut), the regenerated JSON schema, tools/notation.py, tools/gallery.py, expressions.md, notation.md, examples/commitment.yaml and its gallery page, the golden fixture and its three outputs, and tests.

The generated pages are regenerated rather than hand-edited, and tests/test_docs.py is what catches one going stale.

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34260549 | 📁 Comparing 51dd7b7 against latest (768fdf2)

  🔍 Preview build  

47 files changed · + 7 added · ± 40 modified

+ Added

• examples/commitment/index.html
• examples/pypsa/index.html
• examples/pypsa_linearized_uc/index.html
• examples/pypsa_losses/index.html
• examples/pypsa_multi_period/index.html
• examples/pypsa_quadratic/index.html
• examples/pypsa_stochastic/index.html

± Modified

• 404.html
• index.html
• CHANGELOG/index.html
• contributing/index.html
• examples/index.html
• installation/index.html
• about/ceiling/index.html
• about/what-counts-as-language/index.html
• examples/dispatch/index.html
• examples/operators/index.html
• and 30 more...

[FBumann]

Rebased onto current main (alpha.24). The typesetter tests it added moved into main's split (tests/typesetting/test_cases.py, plus the chosen line in the page guard in test_walk.py); the walk's ceiling went, since degree is decided at load now; the validation tests sit in TestExpressionCases at the end of test_validation.py. Gate: pytest, strict docs, compile-tex.

[FabianHofmann]

@FBumann I very much like the implementation. The docstring tried to explain to hard why using when instead of where. I removed that, so it stays clean and does not cause confusion. I would say this is ready to go.

There is one undocumented pitfall here which I would mention in the docs. The fallback is not catching cases where the absence is created by the body of a cased expression itself, eg. using the shift function. This is a more general topic related to expressions themselves. pushing something for this

[FBumann]

Id like to chat about wether this simpler implementation is better than the one in #36 / #33, which is much mroe strict about the case definition before merging this.

Do you have time for it?

[FBumann]

Agreement with @FabianHofmann

Land on a middle ground between #70 and #36, enforcing mutual exclusivity between when conditions (no reliance on ordering), but keeping a otherwise as the so to say default, which covers the rest. The remaining when does not need to be stated explicitly, like it was in #36.

[FBumann]

Superseeded by #168

[FabianHofmann]

@FBumann still unsure about the last expression being the fallback. while this sort of aligned with the math nomenclature, I don't like the assymetric layout. wouldn't a default on the same level as cases be better/clearer/stricter?

[FBumann]

Yes it would.
Id argue for it! Ill add it.

EDIT: Not sure about the level. What about

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 }
      default: shift(status, over=snapshot, offset=1)
constraints:
  no_restart:
    foreach: [snapshot, generator]
    expression: status - previous_status <= 1

With the default as a mandatory case name?
@FabianHofmann
Would match the rendering well. And order still doesnt matter.