summaryrefslogtreecommitdiff
path: root/docs
diff options
context:
space:
mode:
authorSebastian Graf <sebastian.graf@kit.edu>2019-10-28 13:32:41 +0100
committerMarge Bot <ben+marge-bot@smart-cactus.org>2020-01-25 05:21:05 -0500
commit8038cbd96f444fdba18e8c9fb292c565738b774d (patch)
treeed9643488e63acafe3ffca4537cde87290fac04a /docs
parent0e57d8a106a61cac11bacb43633b8b4af12d7fdb (diff)
downloadhaskell-8038cbd96f444fdba18e8c9fb292c565738b774d.tar.gz
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`: ```haskell data GrdTree = Rhs !RhsInfo | Guard !PmGrd !GrdTree -- captures lef-to-right match semantics | Sequence !GrdTree !GrdTree -- captures top-to-bottom 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`: ```haskell 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: 1. The set of values that were not covered by any of the clauses, for exhaustivity warnings. 2. The `AnnotatedTree` that enriches the syntactic structure of the input program with divergence and inaccessibility information. This is `AnnotatedTree`: ```haskell 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. Fixes #17646 on the go. Metric Decrease: T11822 T9233 PmSeriesS haddock.compiler
Diffstat (limited to 'docs')
-rw-r--r--docs/users_guide/using-warnings.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst
index 137ca9c637..586af57136 100644
--- a/docs/users_guide/using-warnings.rst
+++ b/docs/users_guide/using-warnings.rst
@@ -857,7 +857,7 @@ of ``-W(no-)*``.
:type: dynamic
:category:
- :default: 100
+ :default: 30
The pattern match checker works by assigning symbolic values to each
pattern. We call each such assignment a 'model'. Now, each pattern match