feat: a named expression may give a value per region, and no two regions may claim one coordinate

[FBumann]

Implements the feature from #2. Supersedes #70, #36 and #33 — #70 took it through the shape of the block alone, #36 through a proved partition; this is the middle ground decided in #70's thread.

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, in #70, agreeing with @FabianHofmann

Note

The following content was generated by AI. Rewritten after #251 and #252 landed — the earlier body described a version where the fallback was a reserved case named default.

expressions: takes cases: — one case per region over a declared foreach: — and an otherwise: beside them. Exactly one applies at every coordinate, by two different means: no two when masks can hold at once, proved at load before any data binds, and otherwise: carries whatever the cases leave. So the cases have no order and no reserved name among them: each says where it applies on its own terms, and a file a key-sorting formatter rewrote says what it said before.

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 }
    otherwise: 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.

It is a Program node

@dataclass(frozen=True)
class Region:
    when: WhereNode
    value: ExpressionNode

@dataclass(frozen=True)
class Cases(Expression):
    regions: tuple[Region, ...]

The fallback arrives carrying its own mask. The file writes none; lowering fills in the negation of every other region's, cancelling a negation rather than stacking one. So a consumer adds regions rather than working out which is left, and the remainder is resolved once here instead of once per consumer:

not committable                                                # always_on
committable and position(snapshot) == 0                        # boundary
committable and not (committable and position(snapshot) == 0)  # otherwise, built

It could not lower away instead. The program's nodes have no predicate-in-a-value-position, and the obvious alternative — mask each region and add — fails on the absence rules: absence spreads through +, so every region outside its own would take the row with it. Cases is the one node carrying a mask in a value position, and its docstring says so, that being why it exists.

The two rules that make it a quantity

No two cases may claim one coordinate, and it is a load error when they can — decided before any data binds, with the pair named and a coordinate they both claim:

Named expression 'previous_status': cases 'always_on' and 'boundary' both claim the value where
committable is false, the position of snapshot is 0. A coordinate two cases claim has two values,
so it has none — narrow one of the two `when:` strings by the negation of the other, or drop the
wider one and let `otherwise:` carry that region.

That is why boundary above says committable and. Two values at one coordinate is not a quantity, so the regimes are spelled apart rather than ranked.

otherwise: is the value wherever no when holds. It takes every coordinate the cases leave — which is what makes the quantity whole without a second proof, there being no condition on it to fail. Totality is not a nicety: a gap would leave the quantity undefined, and absence spreads, so every constraint referencing it would lose rows it never masked. 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, otherwise: has to say what an absent parameter or an unnamed label gets.

It is written beside cases: rather than inside them because it is not a region like they are — it is what is left. Having nothing but a value to carry, it is written as one, the shorthand expressions: itself takes, and it prints as the last row, the one that reads "otherwise".

Covering a coordinate is not having a value at it. The otherwise: above carries no edge=, so it is empty at the first snapshot; previous_status is whole only because every unit there is claimed by boundary or by always_on. The docs say so, and name the three ways to close such a hole. Nothing catches one left open at load, because whether a case has a value there depends on the data.

The near-miss is named in each direction — no otherwise:, an otherwise: with no cases:, 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'?

A case with no when: and an empty cases: are the closed schema's own errors, when being required and cases: carrying minProperties: 1.

The exclusivity check, and why it is not a SAT call

Every atom in the where-grammar talks about exactly one subject — a parameter, a dimension's coordinates, a dimension's rank, a lookup, a pair of lookups. A propositional reading invents a storage that is both a battery and hydrogen, and refuses the split the feature exists for. So each subject is split into cells — finitely many regions its value can sit in, chosen so every atom over that subject is constant on each — the pair's cells are multiplied out, and a cell where both masks hold is a witness. Because the cells cover every value a subject can take, "no witness" is a proof rather than a sample.

Independence between subjects over-approximates, so a spurious world can only manufacture a witness, never hide one: this refuses case sets that would have been fine and admits none that would not. A pair it will not reason about — both ends of one axis, an ordering on a dtype that has none, a product past CELL_BUDGET — is refused exactly as an overlap is, and the refusal names the rewrite.

tests/test_exclusivity.py::TestSoundness is the check on that claim: pairs are drawn independently, filtered to the ones the check proves apart, and walked over a grid finer than the cells — several points inside single cells, both infinities, an absent value, labels no mask names.

History

Five commits, then two stacked PRs merged in:

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, the exclusivity proof, the lowering, and the printing.
3. docs: unit commitment, the model cases exists for — the example, its gallery page, the nav entry.
4. feat(language): a cased expression writes its fallback as otherwise, outside the cases #251 — the fallback moves out of cases: and becomes the block's own otherwise:, retiring _default_is_the_last_case and the five hand-written errors that policed a reserved name inside a map of user-chosen ones.
5. fix(typesetting): a cased expression whose otherwise holds a variable is set as one the solver decides #252 — five fixes from a review of this branch: a cased expression whose only variable sits in its otherwise: was printing upright, as data rather than as something solved for; an error inside an arm named the constraint that used it rather than the declaration; an integer partition was refused at a midpoint no integer can be; the exclusivity soundness fuzz built every pair as a complement and so could not fail; and an unreachable guard plus the default spelling the rename left in five docstrings.

The node also answered to three rebases: #201's fence (every_program_node.yaml gains a cased expression, in the same commit as the node), #208's total fan_in (Cases declares one-to-one — its regions are disjoint, so an output row reads exactly one of them, alternatives rather than slots summed together), and #211's move of the edge rules to load time.

Checks

pixi run ci clean: lint (ruff, pyrefly, reuse, typos, prettier, zizmor, taplo), 884 passed against main's 829, mkdocs build --strict, and 27 TeX documents compiled — the new example among them.

The nine PRs stacked on this branch (#242 … #250) are rebased onto its current tip.

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34309132 | 📁 Comparing 427ae2f against latest (003b806)

  🔍 Preview build  

40 files changed · + 5 added · ± 35 modified

+ Added

• examples/commitment/index.html
• reference/math_spec/advice/index.html
• reference/math_spec/exclusivity/index.html
• reference/math_spec/lowering/index.html
• reference/math_spec/program/index.html

± Modified

• index.html
• CHANGELOG/index.html
• examples/index.html
• about/ceiling/index.html
• examples/dispatch/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
• and 25 more...

[FBumann]

Note

The following content was generated by AI.

Taking @FabianHofmann's point about the asymmetric layout: the fallback is now the case named default, rather than "the arm that happens to carry no when:".

It stays inside cases:, so the block is still one top-to-bottom list that reads the way \begin{cases} does, and the name says what it is instead of the reader inferring it from a missing key.

cases:
  always_on: { when: "not committable", expression: 1 }
  boundary: { when: "committable and position(snapshot) == 0", expression: status_initial }
  default: { expression: shift(status, over=snapshot, offset=1) }

The name is reserved and the position is fixed — default is written last because that is the row it prints on — and each near-miss gets its own sentence:

a `cases:` block needs a case named `default` — the value wherever no `when` holds, and the row
that prints as "otherwise". Without it the quantity would have no value there, and absence spreads
to every constraint that names it. The cases here are `always_on`, `boundary`.

`default` is written last, and here `always_on` follows it. It is the row that prints as
"otherwise", which is the last row of the block, so the file reads in the order the page does.

`default` carries a `when:`, and it is the one case that must not — it is what covers every
coordinate the others leave. Give the region a name of its own if it is a region like any other.

`opening` carry no `when:`, and `default` is the only case that may omit one — every other case
says where it applies, so that no two of them can claim one coordinate.

a `cases:` block whose only case is `default` is one value everywhere, which is what a plain
`expression:` already says.

pixi run ci clean on ee22929: lint, 790 passed, mkdocs build --strict, 27 TeX documents compiled. Each of the three commits gated on its own.

[FBumann]

@FabianHofmann On hold until I move the lowering + Plan

[FBumann]

Note

The following content was generated by AI.

Rebased onto main (alpha.29). #169 removed values: from a dimension — its members are data now — and that landed on this feature, so the rebase is not just a replay:

• _extent_of, _Frame.extents and the extent-aware half of _rank_cells are gone. Nothing sizes an axis before data, so the rank cells are always one frame and _evaluate no longer folds a negative position into a positive one. _Frame.of drops its schema argument with them.
• position(x) == 0 against position(x) == -1 is now always undecided, where it used to be decidable on an axis that declared values:. Its refusal named a rewrite that no longer exists, and now names the one that does:

cases 'boundary' and 'closing' cannot be told apart before the data arrives: snapshot is split at
positions counted from both ends (-1, 0), and how many members it has is data, so they are the same
row on a one-member axis — count from one end only.

• test_both_ends_where_the_extent_is_declared is deleted rather than moved: the capability it asserted is not in the language any more. test_a_group_never_has_a_declared_extent becomes test_a_group_is_named_as_the_group_it_is — by= never had an extent, so what is left to pin is that the refusal says which group.
• examples/commitment.yaml and the STORAGE / CASED_BASE fixtures drop their values:, and the expressions.md paragraph making the old promise is rewritten.

One textual conflict in tests/test_validation.py, in the import block.

pixi run ci clean on 74b094d: lint, 780 passed, mkdocs build --strict, 27 TeX documents compiled. Each of the three commits gated on its own (716 / 779 / 780).

[FBumann]

Prompt: "Rebase … Rethink it under the new architecture. Easier?" … "But dont they instead need to be in the Program?"

Note

The following content was generated by AI.

Rebased onto main at alpha.36, and your question found a hole. Pushed to feat/cases-proved-apart-rebased — retarget this PR at that branch, or I can open a fresh one.

cases: did not lower

Rebasing and calling to_program on this PR's own example:

to_spec     : ok
to_program  : FAILED
  AssertionError: Expected code to be unreachable, but got: CasesNode(name='previous_status', arms=…)

grep CasesNode in lowering.py and program.py: 0 hits each.

This PR was green on 780 tests when it was written, and correctly so — lowering was lpspec's then, so a construct the language accepted and no lowering built was invisible here. It would have merged, released, and surfaced downstream at the pin bump as a keyword neither lane builds. Owning the pass is what turns that into a red assert_never in the repo that can fix it.

So they are in the Program now

@dataclass(frozen=True)
class Region:
    when: WhereNode
    value: ExpressionNode

@dataclass(frozen=True)
class Cases(Expression):
    regions: tuple[Region, ...]

default arrives carrying its own mask. The file writes no when on it; lowering fills in the negation of every other region's, so a consumer adds regions rather than working out which one is left over. The exclusivity proof already ran on the spec, so that negation is the remainder and the regions stay disjoint and total.

when NotNode  -> value Constant     # always_on
when AndNode  -> value Parameter    # boundary
when AndNode  -> value Translate    # default, its mask built

There was no way to lower this away instead. The program's thirteen nodes have no predicate-in-a-value-position, and the obvious dodge — mask each region and Add — fails on the absence rules: absence spreads through Add, so every region outside its own would take the row with it. The node's docstring says that, since it is the reason it exists.

_lower_expression also had to change: it read block.expression, which a cased block has none of. It now lowers the name, which is the path a reference to it already takes.

Easier, on balance

• CaseArm and CasesNode cost zero public surface. refactor: two public states and a conversion to each, where the surface was seventy-seven names #180 took the AST out of __all__, so the conflict there resolved to "take ours" and nothing is exported.
• Program.check is gone (refactor: a program is trusted by construction, so the language's rules are checked once, on the spec #189), so the node needed no dim or degree arm — the spec is checked once and the program is trusted.
• Against that: the lowering and the differential cost are now in scope rather than downstream. That is the tax, and it is the honest place for it.

Verified: pixi run ci on the rebuilt history — lint, 796 passed (780 on main), docs-build --strict, 27 TeX documents compiled. Three commits as before, with the lowering folded into the feature commit so no commit leaves cases: unbuildable.

What the rebase itself had to resolve

Seven conflicting files, all ones the #177/#180/#181 stack rewrote: __init__.py and test_public_surface.py took ours (the AST additions need no surface); expansion.py, typesetting/symbols.py, walk.py and tests/typesetting/test_walk.py took theirs with Model→Spec, Buildable→_ExpandedSpec, load_model→to_spec re-applied and 31 AST imports repointed at their modules; schema/math-spec.schema.json regenerated.

[FBumann]

Prompt: "Did you successfully lower it?"

Note

The following content was generated by AI.

Not properly, no — the previous comment proved to_program stopped raising, which is not the same claim. Two things were missing, both now on the branch.

The remainder had a double negation

default's mask is built from the negations of the stated cases, and always_on is already not committable, so it came out as not (not committable) — a term every consumer evaluates twice to reach where it started. Cancelled where the regions are built, which is the one place that can:

before                                    after
not committable                           not committable
committable and position(t) == 0          committable and position(t) == 0
not (not committable)                     committable
  and not (committable and position…)       and not (committable and position…)

Which reduces to committable and not position(t) == 0 — disjoint from both, and together with them total.

There were no tests

Four in tests/test_lowering.py, and one of them is the real check rather than a shape assertion:

test_the_lowered_regions_are_still_proved_apart feeds the lowered regions — the invented default mask included — back through exclusivity.overlapping(), the same prover the language runs on the stated cases at load. It asserts no pair can claim a coordinate. The language proves the written masks apart; this proves the one lowering writes does not collide with them.

The other three: one region per case with each value lowered, the default carrying the negation rather than a second not, and the cased expression readable by name off Program.expressions.

Mutation table

Taken by hand — tools/mutate.py cannot express a changed connective — with a clean tree, git checkout -- to restore and __pycache__ dropped on both sides.

Mutation	Caught by
the remainder Ors the negations instead of Anding them	..._are_still_proved_apart, ..._carries_the_mask_the_file_left_unwritten
the double-negation cancel is dropped	..._carries_the_mask_the_file_left_unwritten

The first is the one that matters: an Or of negations is true almost everywhere, so default would overlap both stated cases and the quantity would have two values at once — and the prover says so.

Verified: pixi run ci — lint, 800 passed (780 on main), docs-build --strict, 27 TeX documents. The tests and the peephole are folded into the feature commit, so it is still three commits and none of them leaves cases: unbuildable.

[FabianHofmann]

Note

The following content was generated by AI.

Move the fallback out of cases: and call it otherwise:.

expressions:
  previous_status:
    foreach: [snapshot, generator]
    cases:
      always_on: { when: "not committable", expression: 1 }
      boundary:  { when: "committable and position(snapshot) == 0", expression: status_initial }
    otherwise: shift(status, over=snapshot, offset=1)

A reserved name inside a map of user-chosen names needs five hand-written errors to police it. _default_is_the_last_case (model.py:435) is those five. Taking the name out of the map removes all of them:

today	after
"needs a case named default"	the closed schema's missing-field error on otherwise:
"default is written last"	deleted — nothing depends on order
"only case is default"	min_length=1 on cases:
"default carries a when:"	structurally impossible
"opening carry no when:"	when: is simply required

Two further reasons:

• The ordering rule leans on something YAML does not promise. A mapping is unordered by spec, so the loader currently refuses a valid document that a key-sorting library or a reformatter produced. With otherwise: outside, case order carries no meaning and no error — which is what the exclusivity proof was for.
• otherwise is the honest word. It is the row that prints as \text{otherwise}, and "default" already means the boundz: fall-back elsewhere in the model.

Cost is small and confined to the input spelling. walk.py:654 already finds the fallback by arm.when is None, not by name or position, so CasesNode, expansion, resolution, the dim algebra and boundedness are untouched. Changes land in model.py, the regenerated schema, expressions.md, examples/commitment.yaml, golden/model.yaml, and the tests for the retired messages. The three golden .out files do not change — the rendered maths is identical, which is the check that this is input-only.

Keeping the required fallback; only its spelling moves.

[FabianHofmann]

@FBumann let's pull this is. this looks clean now and fulfills our needs at this stage.

[FabianHofmann]

@FBumann ready to pull in?