fix(typesetting): a cased expression whose otherwise holds a variable is set as one the solver decides

docs/examples/commitment.md

@@ -145,13 +145,13 @@ $$p_{t,g} \ge \mathit{status}_{t,g} \cdot \mathrm{p}^{\mathrm{min}}_{g} \qquad \
 
 **`ramp_up`**
 
-$$p_{t,g} - p_{t \boxminus_{0} 1,g} \le \mathrm{ramp\_limit}_{g} \cdot \mathrm{previous\_status}_{t,g} + \mathrm{start\_up\_limit}_{g} \cdot \left( 1 - \mathrm{previous\_status}_{t,g} \right) \qquad \forall\thinspace t \in \mathcal{T},\enspace g \in \mathcal{G}$$
+$$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) \qquad \forall\thinspace t \in \mathcal{T},\enspace g \in \mathcal{G}$$
 
 #### Definitions
 
 **`previous_status`**
 
-$$\mathrm{previous\_status}_{t,g} = \begin{cases} 1 & \text{if } \neg \mathrm{committable}_{g} \cr \mathrm{status}^{\mathrm{initial}}_{g} & \text{if } \mathrm{committable}_{g} \wedge \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}$$
+$$\mathit{previous\_status}_{t,g} = \begin{cases} 1 & \text{if } \neg \mathrm{committable}_{g} \cr \mathrm{status}^{\mathrm{initial}}_{g} & \text{if } \mathrm{committable}_{g} \wedge \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}$$
 
 #### Variable domains
 

src/math_spec/exclusivity.py

@@ -296,7 +296,10 @@ def _cells_for(subject: Subject, values: set[Any], dtypes: Mapping[str, str]) ->
             raise Undecidable(msg)
         return [True, False, Special.NULL]
     numeric = _numeric(dtype, values)
-    cells: list[Cell] = list(_ordered_cells(values) if numeric or _dated(values) else _label_cells(values))
+    dated = _dated(values)
+    cells: list[Cell] = list(
+        _ordered_cells(values, discrete=dated or dtype == 'int') if numeric or dated else _label_cells(values)
+    )
     # A dimension's coordinates are its own index, so there is no null among
     # them; everything else may be absent, and absence is a region of its own
     # because a null compares false and is not `defined`.
@@ -320,7 +323,7 @@ def _dated(literals: set[Any]) -> bool:
     return bool(literals) and all(isinstance(value, datetime.date) for value in literals)
 
 
-def _ordered_cells(literals: set[Any]) -> list[Cell]:
+def _ordered_cells(literals: set[Any], *, discrete: bool) -> list[Cell]:
     """Each literal, and one representative of the gap on either side of it."""
     if not literals:
         return [0.0]
@@ -332,7 +335,7 @@ def _ordered_cells(literals: set[Any]) -> list[Cell]:
         following = values[index + 1] if index + 1 < len(values) else None
         if following is None:
             continue
-        between = _between(value, following, step)
+        between = _between(value, following, step, discrete=discrete)
         if between is not None:
             cells.append(between)
     cells.append(values[-1] + step)
@@ -348,13 +351,18 @@ def _step(value: Any) -> Any:
     return 1.0
 
 
-def _between(value: Any, following: Any, step: Any) -> Any | None:
+def _between(value: Any, following: Any, step: Any, *, discrete: bool) -> Any | None:
     """A value strictly between two literals, where the type admits one.
 
-    A magnitude always does — the midpoint. A date is discrete, so the gap has
-    to be wider than one unit before there is anything in it to stand for.
+    A continuous magnitude always admits one — the midpoint. A **discrete**
+    subject, an ``int`` or a date, need not: between 0 and 1 there is no
+    integer and between two adjacent days no date, so the gap has to be wider
+    than one unit before there is anything in it to stand for. A midpoint
+    invented there is a coordinate the subject cannot take, and the only thing
+    it can do is manufacture a witness — refusing ``n < 1`` against ``n > 0``,
+    which no integer claims twice, at a coordinate named ``0.5``.
     """
-    if isinstance(value, datetime.date):
+    if discrete:
         return value + step if following - value > step else None
     return (value + following) / 2.0
 

src/math_spec/lowering.py

@@ -33,7 +33,7 @@
 
 import math_spec.program as program
 from math_spec.dimensions import dims_of
-from math_spec.errors import LanguageError, did_you_mean
+from math_spec.errors import LanguageError
 from math_spec.expression_parser import (
     ArithmeticNode,
     BinaryOperatorNode,
@@ -228,16 +228,12 @@ def _lower_expression(schema: _ExpandedSpec, ns: Namespace, name: str) -> progra
     """Compile the named expression *name* into a program expression.
 
     Raises:
-        KeyError: No named expression called *name*.
         LanguageError: A construct outside the streaming language.
     """
-    expanded = schema
     context = f"named expression '{name}'"
-    if name not in expanded.expressions:
-        raise KeyError(f"unknown named expression '{name}'. " + did_you_mean(name, expanded.expressions))
-    ast = expression_of(name, expanded, ns, context)
+    ast = expression_of(name, schema, ns, context)
     assert not isinstance(ast, ComparisonNode), 'load-time validation refuses a comparison in a named expression'
-    return _Lowering(expanded, context).expr(ast)
+    return _Lowering(schema, context).expr(ast)
 
 
 # ---------------------------------------------------------------------------

src/math_spec/program.py

@@ -407,10 +407,11 @@ class Window(Expression):
 class Region:
     """One region of a :class:`Cases`: where it applies, and the value there.
 
-    ``when`` is stated on every region, the file's ``default`` included — its
-    mask is the negation of the others, resolved once here rather than by each
-    consumer in turn. A consumer builds a region without holding the rest in
-    mind, and both facts it needs are on the region it is reading.
+    ``when`` is stated on every region, the one the file wrote as
+    ``otherwise:`` included — its mask is the negation of the others, resolved
+    once here rather than by each consumer in turn. A consumer builds a region
+    without holding the rest in mind, and both facts it needs are on the region
+    it is reading.
     """
 
     when: WhereNode
@@ -422,8 +423,8 @@ class Cases(Expression):
     """A value defined by region — exactly one region applies at each coordinate.
 
     The language proves the regions apart before any data binds, and the
-    file's ``default`` covers whatever the rest leave, so they are disjoint and
-    total by construction: a consumer adds the regions rather than ranking
+    file's ``otherwise:`` covers whatever the rest leave, so they are disjoint
+    and total by construction: a consumer adds the regions rather than ranking
     them, and needs neither an order nor a tie-break.
 
     Not a shape operator — every region spans the dims the expression does, and

src/math_spec/resolution.py

@@ -270,6 +270,18 @@ def resolve_expression(
     return None if len(errors) > before else resolved
 
 
+def _arm_context(name: str, arm: CaseArm) -> str:
+    """Where an error inside one arm is reported: the declaration, not the use site.
+
+    A cased expression is expanded where its name stood, so the context in hand
+    at that point is the constraint's — and naming it would report a case on a
+    constraint that has none. The arm without a ``when`` is the block's
+    ``otherwise:``, which is not a case and is not named as one.
+    """
+    where = 'otherwise' if arm.when is None else f"case '{arm.label}'"
+    return f"Named expression '{name}', {where}"
+
+
 def _resolve_arith(
     node: ArithmeticNode,
     ns: Namespace,
@@ -372,7 +384,7 @@ def _resolve_arith(
     if isinstance(node, CasesNode):
         arms = []
         for arm in node.arms:
-            arm_context = f"{context}, case '{arm.label}'"
+            arm_context = _arm_context(node.name, arm)
             when = None if arm.when is None else _resolve_where(arm.when, ns, arm_context, errors)
             arms.append(CaseArm(arm.label, when, _resolve_arith(arm.value, ns, arm_context, errors)))
         return CasesNode(node.name, tuple(arms))

src/math_spec/typesetting/format.py

@@ -171,7 +171,7 @@ def summation(self, domain: str, body: str) -> str: ...
     def cases(self, arms: list[tuple[str, str]]) -> str:
         """A value defined by region: ``(value, condition)`` per arm, in order.
 
-        Both halves arrive rendered — which arm is the ``default`` is the walk's
+        Both halves arrive rendered — which arm is the fallback is the walk's
         to decide, and this only stacks the rows.
         """
         ...

src/math_spec/typesetting/symbols.py

@@ -25,7 +25,9 @@
 from math_spec.resolution import Namespace, expression_of
 
 if TYPE_CHECKING:
-    from math_spec.model import _ExpandedSpec
+    from collections.abc import Iterator
+
+    from math_spec.model import ExpressionBlock, _ExpandedSpec
     from math_spec.typesetting.format import Format
 
 __all__ = ['SymbolTable', 'Symbols']
@@ -100,12 +102,25 @@ def chosen_expressions(schema: _ExpandedSpec) -> frozenset[str]:
         name
         for name in printed_expressions(schema)
         if any(
-            carries_variable(expression_of(case.expression, schema, namespace, f"expression '{name}', case '{label}'"))
-            for label, case in schema.expressions[name].cases.items()
+            carries_variable(expression_of(text, schema, namespace, f"expression '{name}', {where}"))
+            for text, where in _values_of(schema.expressions[name])
         )
     )
 
 
+def _values_of(block: ExpressionBlock) -> Iterator[tuple[str, str]]:
+    """Every value a cased block holds, the ``otherwise:`` included, and where it sits.
+
+    The fallback is a value of the quantity like any case's, so it decides what
+    the block *is* alongside them: a block whose only variable is there is one
+    the solver returns, and printing it upright would call it data.
+    """
+    for label, case in block.cases.items():
+        yield case.expression, f"case '{label}'"
+    assert block.otherwise is not None
+    yield block.otherwise, 'otherwise'
+
+
 class Symbols:
     r"""How every declared name prints: overrides first, derivation for the rest.
 

src/math_spec/validation.py

@@ -60,6 +60,17 @@ def to_spec(model: str | Path | dict[str, Any] | Spec) -> Spec:
     return Spec.model_validate(model if isinstance(model, dict) else read_yaml(Path(model)))
 
 
+def _once(errors: list[str]) -> str:
+    """The errors as one message, an identical sentence kept only the first time.
+
+    A cased expression is expanded at every use, so a fault in one of its arms
+    is found again at each constraint naming it. Every error carries the
+    context it was found in, so two that differ at all are two faults and an
+    exact repeat is one seen twice.
+    """
+    return '\n'.join(dict.fromkeys(errors))
+
+
 def validate_expressions(schema: Spec) -> None:
     """Validate and resolve every expression and where string in *schema*.
 
@@ -127,7 +138,7 @@ def validate_expressions(schema: Spec) -> None:
         _check_expression(schema.objective.expression, schema, ns, 'The objective', errors, comparison=False, ceiling=2)
 
     if errors:
-        raise SchemaError('\n'.join(errors))
+        raise SchemaError(_once(errors))
 
     check_schema(schema)
 

tests/test_exclusivity.py

@@ -41,6 +41,7 @@
         'kind': {'dims': ['storage'], 'dtype': 'str'},
         'soc_initial': {'dims': ['storage']},
         'capacity': {'dims': ['storage']},
+        'age': {'dims': ['storage'], 'dtype': 'int'},
     },
     'variables': {'soc': {'foreach': ['snapshot', 'storage']}},
     'constraints': {'balance': {'foreach': ['snapshot', 'storage'], 'expression': 'soc == 1'}},
@@ -90,7 +91,7 @@ def test_a_category_split(self, schema: Spec):
         assert refusals(schema, cases) == [], 'a storage carries one kind, so the two labels are apart'
 
     def test_the_ramp_regimes_from_the_issue(self, schema: Spec):
-        """The three quantities #2 factors a PyPSA ramp limit into, less each one's `default`.
+        """The three quantities #2 factors a PyPSA ramp limit into, less each one's `otherwise`.
 
         The point of putting cases on an expression rather than on the
         constraint: three independent axes multiply into eight constraint cases
@@ -119,8 +120,23 @@ def test_numeric_bands(self, schema: Spec):
         cases = {'small': 'capacity and capacity <= 10', 'large': 'capacity and capacity > 10'}
         assert refusals(schema, cases) == [], 'a capacity is at most 10 or above it'
 
-    def test_a_when_of_true_is_not_a_default(self, schema: Spec):
-        """`default` is the case *without* a `when`, and nothing here stands in for it.
+    def test_an_integer_admits_no_value_between_its_bands(self, schema: Spec):
+        """`age` is declared `int`, and the two bands are complements over the integers.
+
+        A midpoint invented in the gap is a coordinate the subject cannot take,
+        and the refusal it manufactures names `0.5` — a value no data produces,
+        with a rewrite the file has already followed.
+        """
+        cases = {'new': 'age < 1', 'old': 'age > 0'}
+        assert refusals(schema, cases) == [], 'an integer is below 1 or above 0, never between'
+
+    def test_a_magnitude_still_admits_one(self, schema: Spec):
+        """The mirror: `capacity` is a float, so 0.5 is a coordinate it can take."""
+        cases = {'small': 'capacity < 1', 'large': 'capacity > 0'}
+        assert refusals(schema, cases), 'a float between the two bands is claimed by both'
+
+    def test_a_when_of_true_is_not_a_fallback(self, schema: Spec):
+        """The fallback is the block's `otherwise:`, and nothing inside `cases:` stands in for it.
 
         A mask that happens to be true everywhere is read as any other mask is,
         so it collides with every case beside it.
@@ -197,6 +213,12 @@ class TestSoundness:
     infinities, an absent value, labels the masks never name — and asserts that
     nothing it proved apart has a point claimed by both.
 
+    **The two masks are drawn independently**, and only the pairs the check
+    proves apart are walked. A pair built as a complement — `m` against
+    `not m` — makes the assertion `X and not X`, false at every point under
+    every implementation, so a fuzz over those shapes cannot fail and certifies
+    nothing.
+
     What it does not test is the reading of an individual atom: ground truth
     here evaluates through the same `_evaluate` the checker uses, so a misread
     atom would agree with itself. That is what `TestProvesApart` and
@@ -254,12 +276,8 @@ def test_a_pair_proved_apart_stays_apart_on_a_finer_grid(self, schema: Spec, see
         rng = random.Random(seed)
         dtypes = namespace.dtypes
         proved = 0
-        for _ in range(300):
-            split = self._mask(rng, atoms)
-            first, second = split, NotNode(split)
-            if rng.random() < 0.5:
-                inner = self._mask(rng, atoms)
-                first, second = AndNode(split, inner), AndNode(split, NotNode(inner))
+        for _ in range(2000):
+            first, second = self._mask(rng, atoms), self._mask(rng, atoms)
             if list(overlapping({'a': first, 'b': second}, schema)):
                 continue
             proved += 1
@@ -269,4 +287,4 @@ def test_a_pair_proved_apart_stays_apart_on_a_finer_grid(self, schema: Spec, see
             for point in grid:
                 both = _evaluate(first, point, frame) and _evaluate(second, point, frame)
                 assert not both, f'both cases claim {point} — the cells hid a witness'
-        assert proved > 50, f'only {proved} pairs proved apart; the fuzz is not exercising the check'
+        assert proved > 150, f'only {proved} pairs proved apart; the fuzz is not exercising the check'

tests/test_validation.py

@@ -761,6 +761,41 @@ def test_a_constraint_naming_it_carries_the_declared_frame(self):
         with pytest.raises(DimensionError, match='snapshot'):
             to_spec(model)
 
+    def test_a_fault_in_an_arm_names_the_declaration_and_is_reported_once(self):
+        """The block is expanded at every use, and the fault is in one place.
+
+        Naming the use site would report a case on a constraint that has none,
+        and one sentence per constraint reading the expression is the same
+        fault as many.
+        """
+        model = _cased({'opening': {'when': 'position(snapshot) == 0', 'expression': 'nope'}})
+        model['constraints'] = {
+            name: {'foreach': ['snapshot', 'generator'], 'expression': f'p <= headroom + {n}'}
+            for n, name in enumerate(('cap', 'floor'))
+        }
+        with pytest.raises(SchemaError) as caught:
+            to_spec(model)
+
+        message = str(caught.value)
+        assert message.count("'nope' not found") == 1, 'two constraints read it; the fault is reported once'
+        assert "Named expression 'headroom', case 'opening'" in message
+        assert 'Constraint' not in message, "the arm is the declaration's, not the use site's"
+
+    def test_the_fallback_is_not_named_as_a_case(self):
+        """`otherwise:` is what is left, not a region like the cases are.
+
+        Reached through a constraint, which is where the arms are walked a
+        second time and where the label was read off the arm.
+        """
+        model = _cased(otherwise='nope')
+        model['constraints'] = {'cap': {'foreach': ['snapshot', 'generator'], 'expression': 'p <= headroom'}}
+        with pytest.raises(SchemaError) as caught:
+            to_spec(model)
+
+        message = str(caught.value)
+        assert "Named expression 'headroom', otherwise: 'nope' not found" in message
+        assert "case 'otherwise'" not in message, 'the fallback is not one of the cases'
+
     def test_a_case_may_name_another_expression(self):
         model = _cased({'opening': {'when': 'position(snapshot) == 0', 'expression': 'spare'}})
         model['expressions']['spare'] = 'p_max * 2'

tests/typesetting/test_cases.py

@@ -100,6 +100,19 @@ def test_a_case_reaching_a_variable_is_chosen(fmt: Format):
     assert fmt.italic('headroom') in typeset(decided, fmt, legend=False)
 
 
+@EVERY_FORMAT
+def test_the_fallback_reaching_a_variable_is_chosen(fmt: Format):
+    """The `otherwise:` is a value of the quantity like any case's.
+
+    `previous_status` in the commitment example is this shape and no other: its
+    two cases are a constant and a parameter, and the variable is in the
+    fallback alone. Read only the cases and the block prints upright, which
+    says the model was handed a quantity it in fact solves for.
+    """
+    decided = override(CASED, **{'expressions.headroom.otherwise': 'p'})
+    assert fmt.italic('headroom') in typeset(decided, fmt, legend=False)
+
+
 @EVERY_FORMAT
 def test_a_definition_naming_another_one_prints_both(fmt: Format):
     """The cases are walked too, so the collection runs to a fixpoint."""