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

[FabianHofmann]

Prompt: "1" (the option: "Open the R1 PR from a new worktree, with the failing test first.")

Note

The following content was generated by AI.

A cases: block with one case may now compare expressions in its when:. The otherwise: is the complement of the cases, so one case overlaps nothing. Two or more such cases are still refused.

Closes #794

Method, gate output, alternatives

Why the refusal can go

• otherwise is built as the complement of the cases (remainder in src/mathspec/resolution.py:263-273). A single case cannot overlap it, so the message "the otherwise is its negation" gave no reason to refuse.
• A variable or a dual in a mask is refused earlier (src/mathspec/_where_resolver.py:364-373). A when: comparison only compares parameters.
• where: has accepted comparisons of expressions since feat(language): a where may compare arithmetic over parameters #566.
• The refusal was already bypassed by shift(<cmp>, along=period, offset=0), which loaded.

The change

• src/mathspec/exclusivity.py: _undecided and the per-case refusal in overlapping are deleted. The pair check did not need them: _observe already raises Undecidable with _expression_rewrite for an ExpressionComparison, so a pair that compares expressions is refused as before, now once per pair instead of once per case. The message "The otherwise is its negation" is gone with it.
• docs/reference/language/named.md and docs/reference/language/expressions.md: the rule now applies to a block of two or more cases.

Failing test first

tests/test_validation.py::TestAWhereSideIsReadInResolution::test_a_lone_case_comparing_expressions_loads replaces test_a_lone_case_comparing_expressions_is_refused_too. It loads a block with one case c > 2 * k, reads the YAML back to the same program, and prints it in latex, markdown and typst. On the unfixed tree:

E           mathspec.errors.SchemaError: Named expression 'e': case 'wide' cannot be told apart before the data arrives: it compares expressions, whose values only the data decides — compare one parameter against a literal, or precompute the test as a boolean parameter and test that. The `otherwise` is its negation, and only the data says where that falls, so this is refused the way a proven overlap is.
FAILED tests/test_validation.py::TestAWhereSideIsReadInResolution::test_a_lone_case_comparing_expressions_loads[latex]
FAILED tests/test_validation.py::TestAWhereSideIsReadInResolution::test_a_lone_case_comparing_expressions_loads[markdown]
FAILED tests/test_validation.py::TestAWhereSideIsReadInResolution::test_a_lone_case_comparing_expressions_loads[typst]
3 failed, 405 deselected

After the fix: 3 passed.

Where the coverage of the old tests moved

The fix with the old tests gave 3 failed, 2596 passed:

• test_validation.py::test_a_lone_case_comparing_expressions_is_refused_too: replaced by the test above, which asserts the opposite.
• test_exclusivity.py::test_a_literal_written_first_is_named_as_the_order_it_is and test_a_comparison_of_real_expressions_keeps_the_general_refusal: they unpacked two refusals, one per case. They now unpack one refusal for the pair. The first asserts it names cases 'big' and 'small'. The rewrite text they check is unchanged.
• The pair refusal stays covered by test_validation.py::test_a_case_comparing_expressions_is_refused_as_undecidable, unchanged and passing.

Gates

• pixi run lint: all hooks pass.
• pixi run ci: 2601 passed; docs-build --strict no issues; render-tex and compile-tex 55 documents.

Deliberately not done

• R2: two cases that each compare expressions are still refused. Letting the pair check treat a comparison as an opaque atom is a separate change.
• Masks are unchanged. examples/ is unchanged; no test forced a change.

[read-the-docs-community]

Documentation build overview

📚 mathspec | 🛠️ Build #34850348 | 📁 Comparing 813e81d against latest (abe9967)

  🔍 Preview build  

3 files changed

± changelog/index.html
± reference/language/expressions/index.html
± reference/language/named/index.html

[FBumann]

@FabianHofmann Feel free to merge