PmCheck: Formulate as translation between Clause Trees
We used to check GrdVec
s arising from multiple clauses and guards in
isolation. That resulted in a split between pmCheck
and
pmCheckGuards
, the implementations of which were similar, but subtly
different in detail. Also the throttling mechanism described in
Note [Countering exponential blowup]
ultimately got quite complicated
because it had to cater for both checking functions.
This patch realises that pattern match checking doesn't just consider
single guarded RHSs, but that it's always a whole set of clauses, each
of which can have multiple guarded RHSs in turn. We do so by
translating a list of Match
es to a GrdTree
:
data GrdTree
= Rhs !RhsInfo
| Sequence !GrdTree !GrdTree -- captures top-to-bottom match semantics
| Guard !PmGrd !GrdTree -- captures lef-to-right match semantics
| Empty -- For -XEmptyCase, neutral element of Sequence
Then we have a function checkGrdTree
that matches a given GrdTree
against an incoming set of values, represented by Deltas
:
checkGrdTree :: GrdTree -> Deltas -> CheckResult
...
Throttling is isolated to the Sequence
case and becomes as easy as one
would expect: When the union of uncovered values becomes too big, just
return the original incoming Deltas
instead (which is always a
superset of the union, thus a sound approximation).
The returned CheckResult
contains two things:
- The set of values that were not covered by any of the clauses, for exhaustivity warnings.
- The
AnnotatedTree
that enriches the syntactic structure of the input program with divergence and inaccessibility information.
This is AnnotatedTree
:
data AnnotatedTree
= AccessibleRhs !RhsInfo
| InaccessibleRhs !RhsInfo
| MayDiverge !AnnotatedTree
| SequenceAnn !AnnotatedTree !AnnotatedTree
| EmptyAnn
Crucially, MayDiverge
asserts that the tree may force diverging
values, so not all of its wrapped clauses can be redundant.
While the set of uncovered values can be used to generate the missing
equations for warning messages, redundant and proper inaccessible
equations can be extracted from AnnotatedTree
by
redundantAndInaccessibleRhss
.
For this to work properly, the interface to the Oracle had to change.
There's only addPmCts
now, which takes a bag of PmCt
s. There's a
whole bunch of PmCt
variants to replace the different oracle functions
from before.
The new AnnotatedTree
structure allows for more accurate warning
reporting (as evidenced by a number of changes spread throughout GHC's
code base), thus we fix #17465 (closed).
Fixes #17646 (closed) on the go.