Skip to content

math_spec.exclusivity

Can two of a named expression's cases claim one coordinate? Decided without data.

Each when is read over cells: regions of one subject's value on which every atom is constant. The cells of the pair's subjects are multiplied out, both masks are evaluated on each, and a cell where both hold is a witness. Independence between subjects over-approximates, so it can manufacture a witness but never hide one. The rule itself is stated in docs/reference/language/expressions.md.

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, dtypes) #

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]

dtypes

The declared dtype of every name a mask compares against.

TYPE: Mapping[str, DeclaredDtype]

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], dtypes: Mapping[str, DeclaredDtype]) -> 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.
        dtypes: The declared 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.
    """
    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.'
            )