This PR changes the counter-example accumulator in the match compiler
from
a `List` (built with cons, producing reverse order) to an `Array` (built
with push, preserving declaration order). Missing cases are now reported
in
the order constructors appear in the inductive type definition.
For example, given `inductive Enum | a | b | c | d`, missing cases `c`
and
`d` were previously shown as `d, c` and are now shown as `c, d`.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `match.maxCounterExamples` option (default 5) to bound
the
number of "missing cases" counter-examples the match compiler generates.
When the match compiler runs out of alternatives for a variable, it
case-splits to explore missing cases. Previously, this would recursively
split all inductive-typed fields of each constructor, leading to
O(K^fields)
counter-examples for types with K constructors per field. For nested
incomplete matches on types like `Op w` (20 constructors with `Operand
w`
fields having 8 constructors each), this produced thousands of
counter-examples and took several seconds.
The fix checks the counter-example count in `isConstructorTransition`:
once
the limit is reached and there are no remaining alternatives, the match
compiler stops exploring further case splits. The error message notes
when
output has been truncated and names the option. The existing protection
against infinite recursion on recursive types is preserved.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
