fix(language): a cases block with one case may compare expressions in its when:

CHANGELOG.md

@@ -12,6 +12,7 @@ it releases that version ([RELEASING.md](https://github.com/energy-models/mathsp
 
 ## Upcoming version
 
+- fix(language): a cases block with one case may compare expressions in its when: ([#795](https://github.com/energy-models/mathspec/pull/795))
 - feat(language): a parameter value that is null or NaN is refused when the data is attached ([#788](https://github.com/energy-models/mathspec/pull/788))
 - fix(language): a where string names several columns in at's over= and into=, as an expression does ([#782](https://github.com/energy-models/mathspec/pull/782))
 - fix(language): a file whose terms read each other's sums is refused at load ([#780](https://github.com/energy-models/mathspec/pull/780))

docs/reference/language/expressions.md

@@ -293,8 +293,8 @@ constraints:
     expression: shed >= load - ramp
 ```
 
-A [case `when:`](named.md#the-rules-that-keep-the-cases-apart) may not compare
-expressions. A comparison with a number on both sides, such as `2 < 1`, is
+A [case `when:`](named.md#the-rules-that-keep-the-cases-apart) may compare
+expressions only in a block with one case. A comparison with a number on both sides, such as `2 < 1`, is
 refused everywhere.
 
 ### `position()`

docs/reference/language/named.md

@@ -121,8 +121,11 @@ is an [empty sum](#expressions), `empty: true`.
   against `position(snapshot) == -1` pick the same row on an axis with one
   member. Count from one end only.
 
-- **A `when:` may not compare expressions**, such as `c > 2 * k`, even in a
-  block with one case. Precompute the test as a boolean parameter.
+- **In a block of two or more cases, a `when:` may not compare expressions**,
+  such as `c > 2 * k`. Nothing proves such a case apart from the others before
+  the data arrives. Precompute the test as a boolean parameter. A block with one
+  case may compare expressions: its `otherwise:` claims only what the case
+  leaves.
 
 - **Each `when:` and each value sits inside the frame.** A narrower case
   broadcasts as a parameter with fewer dimensions does.

src/mathspec/exclusivity.py

@@ -76,16 +76,7 @@ def overlapping(cases: Mapping[str, Predicate], dtypes: Mapping[str, DeclaredDty
         both claim or what stopped the pair being decided. Empty where every
         pair is proved apart.
     """
-    undecided = {name: reason for name, mask in cases.items() if (reason := _undecided(mask)) is not None}
-    for name, reason in undecided.items():
-        yield (
-            f"case '{name}' cannot be told apart before the data arrives: {reason}. "
-            f'The `otherwise` is its negation, and only the data says where that falls, so this is refused '
-            f'the way a proven overlap is.'
-        )
     for (first, left), (second, right) in itertools.combinations(cases.items(), 2):
-        if first in undecided or second in undecided:
-            continue
         try:
             witness = _witness(left, right, dtypes)
         except Undecidable as exc:
@@ -215,19 +206,6 @@ def witness(self, cell: dict[Subject, Cell]) -> str:
 }
 
 
-def _undecided(mask: Predicate) -> str | None:
-    """The rewrite for a comparison of expressions under *mask*, or ``None`` where every atom is decidable alone.
-
-    A case is refused on its own rather than as a pair, because a block of one
-    case has no pair and the rule is the same: nothing proves where a
-    comparison of expressions falls before the numbers arrive.
-    """
-    for atom in Mask(mask).atoms:
-        if isinstance(atom, ExpressionComparison):
-            return _expression_rewrite(atom)
-    return None
-
-
 def _expression_rewrite(node: ExpressionComparison) -> str:
     """Why a comparison of expressions is not decided, and what to write instead.
 

tests/test_exclusivity.py

@@ -201,8 +201,8 @@ def test_a_literal_written_first_is_named_as_the_order_it_is(self, schema: Spec)
         the general refusal for a comparison of expressions — which told the
         author to compare one parameter against a literal.
         """
-        [refusal, other] = refusals(schema, {'big': '2 < capacity', 'small': '2 >= capacity'})
-        assert "case 'big'" in refusal and "case 'small'" in other, 'each case is refused on its own, not as a pair'
+        [refusal] = refusals(schema, {'big': '2 < capacity', 'small': '2 >= capacity'})
+        assert "cases 'big' and 'small'" in refusal, 'the pair is refused once, not each case on its own'
         assert 'the literal is on the left' in refusal
         assert 'capacity > 2.0' not in refusal, 'the rewrite quotes the number as the file wrote it'
         assert 'capacity > 2' in refusal, 'the rewrite is the same test written the other way round'
@@ -223,7 +223,7 @@ def test_the_rewrite_is_the_same_test_with_the_sides_swapped(self, schema: Spec,
 
     def test_a_comparison_of_real_expressions_keeps_the_general_refusal(self, schema: Spec):
         """Only the plain shape is named; anything else is still the data's to decide."""
-        [refusal, _] = refusals(schema, {'over': 'capacity > soc_initial', 'under': 'capacity <= soc_initial'})
+        [refusal] = refusals(schema, {'over': 'capacity > soc_initial', 'under': 'capacity <= soc_initial'})
         assert 'it compares expressions, whose values only the data decides' in refusal
 
     def test_a_pair_with_more_regions_than_the_budget(self):

tests/test_validation.py

@@ -16,12 +16,13 @@
 from mathspec.errors import DimensionError, LanguageError, SchemaError
 from mathspec.program import DimensionPosition
 from mathspec.resolution import Namespace
-from mathspec.typesetting import to_markdown, typeset_declaration
+from mathspec.typesetting import FORMATS, to_markdown, typeset_declaration
 from mathspec.validation import to_spec
 from tests.fixtures import DISPATCH_MODEL, OPERATOR_PROBES, SMALL_MODEL, varied, where_of
 
 if TYPE_CHECKING:
     from mathspec.spec import Spec
+    from mathspec.typesetting import FormatName
 
 
 def _schema(**patch) -> Spec:
@@ -774,16 +775,23 @@ def test_a_case_comparing_expressions_is_refused_as_undecidable(self):
         assert 'cannot be told apart before the data arrives: it compares expressions' in message
         assert 'precompute the test as a boolean parameter' in message
 
-    def test_a_lone_case_comparing_expressions_is_refused_too(self):
-        """One case has no pair to be proved apart from, and it loaded: the pairwise
-        check never observed it. The rule is on the case, not on the pair — the
-        `otherwise` is its negation, and only the data decides where that falls."""
-        message = _refusal(
-            expressions={
-                'e': {'dims': ['g'], 'cases': {'wide': {'when': 'c > 2 * k', 'expression': 'c'}}, 'otherwise': 0}
-            }
+    @pytest.mark.parametrize('fmt', sorted(FORMATS))
+    def test_a_lone_case_comparing_expressions_loads(self, fmt: FormatName):
+        """A block of one case that compared expressions was refused as if it
+        could overlap its `otherwise`. The `otherwise` is built as the complement
+        of the cases, so one case overlaps nothing, and the same comparison
+        loaded inside `shift(..., offset=0)` (#794)."""
+        spec = to_spec(
+            varied(
+                SMALL_MODEL,
+                expressions={
+                    'e': {'dims': ['g'], 'cases': {'wide': {'when': 'c > 2 * k', 'expression': 'c'}}, 'otherwise': 0}
+                },
+            )
         )
-        assert "case 'wide' cannot be told apart before the data arrives: it compares expressions" in message
+        assert to_spec(spec.to_yaml()).program == spec.program, 'the when string reads back to the same mask'
+        printed = typeset_declaration(spec, 'e', fmt).replace('\\_', '_')
+        assert '> 2' in printed and 'otherwise' in printed, f'{fmt} prints the comparison and its otherwise'
 
 
 class TestAPredicateIsAnOperand: