math_spec.exclusivity

Can two of a named expression's cases claim one coordinate? 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 only if no coordinate is claimed twice, and nothing about the data decides that — so it is decided at load, and a file leaving two cases free to collide does not load.

The other half of being a quantity — a value everywhere — is the block's shape rather than anything proved: the otherwise: beside the cases takes whatever they leave. Only the when strings are checked, and only against each other, pair by pair: when_i AND when_j unsatisfiable.

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 the pair's subjects are multiplied out and both masks evaluated on each. A cell where both are true is a witness. Because the cells cover every value a 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.

A pair the procedure will not reason about is refused exactly as an overlapping one is, and the refusal names the rewrite: a checker that guesses where it cannot decide buys nothing over no checker.

CELL_BUDGET = 8192 module-attribute

Cell = float | str | bool | int | datetime.date | Special module-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

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

A pair this procedure will not reason about. Carries the rewrite.

overlapping(cases, schema)

One refusal per pair of cases that could both claim a coordinate.

PARAMETER	DESCRIPTION
cases	The when of every case, keyed by the case's name. The block's otherwise is not among them: it claims what the rest leave, so it overlaps nothing by construction. TYPE: Mapping[str, WhereNode]
schema	Read for the dtype of every name a mask compares against. TYPE: Spec

YIELDS	DESCRIPTION
str	A sentence per pair, naming both cases and either a coordinate they
str	both claim or what stopped the pair being decided. Empty where every
str	pair is proved apart.

Source code in src/math_spec/exclusivity.py

def overlapping(cases: Mapping[str, WhereNode], schema: Spec) -> Iterator[str]:
    """One refusal per pair of cases that could both claim a coordinate.

    Args:
        cases: The ``when`` of every case, keyed by the case's name. The
            block's ``otherwise`` is not among them: it claims what the rest
            leave, so it overlaps nothing by construction.
        schema: Read for the dtype of every name a mask compares against.

    Yields:
        A sentence per pair, naming both cases and either a coordinate they
        both claim or what stopped the pair being decided. Empty where every
        pair is proved apart.
    """
    dtypes = Namespace.of(schema).dtypes
    for (first, left), (second, right) in itertools.combinations(cases.items(), 2):
        try:
            witness = _witness(left, right, dtypes)
        except Undecidable as exc:
            yield (
                f"cases '{first}' and '{second}' cannot be told apart before the data arrives: {exc}. "
                f'Two cases claiming one coordinate would give it two values, so this is refused '
                f'the way a proven overlap is.'
            )
            continue
        if witness is not None:
            yield (
                f"cases '{first}' and '{second}' both claim the value where {witness}. "
                f'A coordinate two cases claim has two values, so it has none — narrow one of the '
                f'two `when:` strings by the negation of the other, or drop the wider one and let '
                f'`otherwise:` carry that region.'
            )