-
Notifications
You must be signed in to change notification settings - Fork 18
Open
Description
Extend predicate inversion (introduced in #217) to handle case expressions with multiple arms, enabling queries like:
from x where (case x of 1 => true | 3 => true | _ => false);
> val it = [1, 3] : int bagCurrently this fails because the case expression cannot be inverted.
A more advanced example uses constructor patterns with predicates on the payloads.
from e where (case e of
INL 0 => true
| INL 6 => false
| INR b => not b
| INL 7 => true
| INL 100 => true
| INL n => n >= 5 andalso n <= 8);
> val it = [INL 0, INL 5, INL 7, INL 8, INR false, INL 100] : (int, bool) either bagNote:
INL 7appears only once even though two arms match it;INL 6does not appear, because it is excluded byINL 6 => falsebefore reaching the branchINL n => n >= 5 andalso n <= 8that would include it;- the
INL narm uses range inversion; INR b => not binverts tob = false(or just iterates overboolean, which is a practically finite type);- constant patterns like
INL 0use point inversion.
Proposed approach
Transform the multi-arm case into an orelse of singleton cases:
case x of p1 => e1 | p2 => e2 | _ => falsebecomes:
(case x of p1 => e1 | _ => false) orelse (case x of p2 => e2 | _ => false)The existing maybeUnion rule in Generators handles orelse by recursively inverting each branch and combining them via generateUnion. This avoids duplicating the upstream query.
Each singleton case then requires its own inversion:
- Constant patterns (
1 => true) reduce to equality (x = 1), handled bymaybePoint - Constructor patterns (
SOME n => e) generate the constructor shape and pusheas a constraint on payload variables
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels