math_spec.partition

Do a named expression's cases partition its frame? Decided without data.

A named expression with cases: is one quantity whose value varies by region — the regime a unit is in, which end of the horizon a row sits at. It is one quantity, with one value per coordinate, only if the cases claim each coordinate exactly once. That claim is decidable here, before any data binds, which is rule 2 in a new position.

Three obligations, all the same unsatisfiability question:

• disjoint — case_i AND case_j is unsatisfiable, for every pair. Two values at one coordinate is not a quantity.
• exhaustive — NOT (case_1 OR ... OR case_n) is unsatisfiable. An expression is total over its foreach: a gap would leave it undefined, and rule 7 would spread that to every constraint referencing it, silently deleting rows the constraint never masked.
• no dead case — case_i alone is satisfiable. A case that claims nothing is a mistake rather than a no-op.

Nothing is conditioned on a mask, because an expression carries none: it is total or it is refused. That is what keeps a constraint's row set readable at the constraint, which is the whole reason the cases sit here rather than there.

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. Atoms with different subjects are independent; atoms sharing one are not, and that is where a propositional reading goes wrong: on kind == 'battery' and kind == 'h2' it invents a world where both hold and reports an overlap that no data can produce.

So each subject is split into cells — finitely many regions its value can sit in, chosen so that every atom over that subject is constant on each cell. The cells of all subjects are multiplied out and each mask is evaluated on each cell. A cell where two cases are true is a witness for overlap; a cell where none is, a witness for a gap. Because the cells cover every value the subject can take, "no witness" is a proof and not a sample.

Independence between subjects is an over-approximation: the product of cells contains worlds the data may never produce, so a spurious world can only manufacture a witness, never hide one. Every outcome here is therefore conservative — this refuses case sets that would have been fine, and admits none that would not.

Run at load by :func:math_spec.validation.validate_expressions, once per cased expression, so a case set that is not a partition is a load error rather than a build-time surprise.

CELL_BUDGET = 8192 module-attribute

Cell = float | str | bool | int | datetime.date | Special module-attribute

Witness = dict[str, str] module-attribute

Case(name, when) dataclass

One case of an expression: its when, and the name the LaTeX prints.

Every case carries a when; NOT (x) is how the complement is written. The key is not where because a case selects which value a coordinate takes — it creates no absence and deletes no row, which is what where means everywhere else (rule 6).

name instance-attribute

when instance-attribute

Overlap(cases, witness) dataclass

Two cases that can both claim one coordinate.

cases instance-attribute

witness instance-attribute

Special

Bases: Enum

Values a cell can hold that are not values of the subject's own type.

NEG_INF = '-inf' class-attribute instance-attribute

NULL = 'null' class-attribute instance-attribute

OTHER = 'other' class-attribute instance-attribute

POS_INF = '+inf' class-attribute instance-attribute

Status

Bases: Enum

What the check established.

:attr:UNDECIDED is refused by the caller exactly as :attr:VIOLATED is: a checker that guesses where it cannot decide buys nothing over no checker.

PARTITION = 'partition' class-attribute instance-attribute

UNDECIDED = 'undecided' class-attribute instance-attribute

VIOLATED = 'violated' class-attribute instance-attribute

Subject(kind, name, qualifier=None) dataclass

What an atom talks about — the key its cells are built for.

kind separates the namespaces that could otherwise collide: a dimension's coordinates and its rank are two subjects over one name, and a rank is further split by the by= lookup it is counted within.

kind instance-attribute

name instance-attribute

qualifier = None class-attribute instance-attribute

Undecidable

Bases: Exception

An atom this procedure will not reason about. Carries the rewrite.

Verdict(status, overlaps=(), gaps=(), dead=(), reason=None) dataclass

dead = () class-attribute instance-attribute

gaps = () class-attribute instance-attribute

ok property

overlaps = () class-attribute instance-attribute

reason = None class-attribute instance-attribute

status instance-attribute

message()

What a load error would print. Empty for a proven partition.

Source code in src/math_spec/partition.py

def message(self) -> str:
    """What a load error would print. Empty for a proven partition."""
    if self.status is Status.PARTITION:
        return ''
    if self.status is Status.UNDECIDED:
        return f'cannot decide statically: {self.reason}'
    parts = []
    for overlap in self.overlaps:
        first, second = overlap.cases
        parts.append(f"cases '{first}' and '{second}' both claim the value where {_render(overlap.witness)}")
    parts.extend(f'no case claims the value where {_render(gap)}' for gap in self.gaps)
    parts.extend(f"case '{name}' claims nothing" for name in self.dead)
    return '; '.join(parts)

check_partition(cases, schema)

Decide whether cases partition the expression's frame.

PARAMETER	DESCRIPTION
cases	The cases, in declaration order, each with its own when. TYPE: Iterable[Case]
schema	Read for dtypes, and for the declared values: that give a dimension a statically known extent. TYPE: Model

RETURNS	DESCRIPTION
Verdict	The verdict. :attr:Status.UNDECIDED is a refusal — see the module
Verdict	docstring.

Source code in src/math_spec/partition.py

def check_partition(cases: Iterable[Case], schema: Model) -> Verdict:
    """Decide whether *cases* partition the expression's frame.

    Args:
        cases: The cases, in declaration order, each with its own ``when``.
        schema: Read for dtypes, and for the declared ``values:`` that give a
            dimension a statically known extent.

    Returns:
        The verdict. :attr:`Status.UNDECIDED` is a refusal — see the module
        docstring.
    """
    try:
        return _decide(list(cases), schema)
    except Undecidable as exc:
        return Verdict(Status.UNDECIDED, reason=str(exc))