diff options
author | Sebastian Graf <sebastian.graf@kit.edu> | 2019-05-16 18:49:02 +0200 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2019-09-16 13:33:05 -0400 |
commit | 7915afc6bb9539a4534db99aeb6616a6d145918a (patch) | |
tree | 41b7c731d20754b2ce9f73488b7aaeff7ec80565 /docs | |
parent | b5ae3868db62228e7a75a9f1f66a9b05a4cf3277 (diff) | |
download | haskell-7915afc6bb9539a4534db99aeb6616a6d145918a.tar.gz |
Encode shape information in `PmOracle`
Previously, we had an elaborate mechanism for selecting the warnings to
generate in the presence of different `COMPLETE` matching groups that,
albeit finely-tuned, produced wrong results from an end user's
perspective in some cases (#13363).
The underlying issue is that at the point where the `ConVar` case has to
commit to a particular `COMPLETE` group, there's not enough information
to do so and the status quo was to just enumerate all possible complete
sets nondeterministically. The `getResult` function would then pick the
outcome according to metrics defined in accordance to the user's guide.
But crucially, it lacked knowledge about the order in which affected
clauses appear, leading to the surprising behavior in #13363.
In !1010 we taught the term oracle to reason about literal values a
variable can certainly not take on. This MR extends that idea to
`ConLike`s and thereby fixes #13363: Instead of committing to a
particular `COMPLETE` group in the `ConVar` case, we now split off the
matching constructor incrementally and record the newly covered case as
a refutable shape in the oracle. Whenever the set of refutable shapes
covers any `COMPLETE` set, the oracle recognises vacuosity of the
uncovered set.
This patch goes a step further: Since at this point the information
in value abstractions is merely a cut down representation of what the
oracle knows, value abstractions degenerate to a single `Id`, the
semantics of which is determined by the oracle state `Delta`.
Value vectors become lists of `[Id]` given meaning to by a single
`Delta`, value set abstractions (of which the uncovered set is an
instance) correspond to a union of `Delta`s which instantiate the
same `[Id]` (akin to models of formula).
Fixes #11528 #13021, #13363, #13965, #14059, #14253, #14851, #15753, #17096, #17149
-------------------------
Metric Decrease:
ManyAlternatives
T11195
-------------------------
Diffstat (limited to 'docs')
-rw-r--r-- | docs/users_guide/glasgow_exts.rst | 43 |
1 files changed, 0 insertions, 43 deletions
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index 3c951466c9..5cf3c4b9cc 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -15541,49 +15541,6 @@ the user must provide a type signature. :: foo :: [a] -> Int foo T = 5 -.. _multiple-complete-pragmas: - -Disambiguating between multiple ``COMPLETE`` pragmas ----------------------------------------------------- - -What should happen if there are multiple ``COMPLETE`` sets that apply to a -single set of patterns? Consider this example: :: - - data T = MkT1 | MkT2 | MkT2Internal - {-# COMPLETE MkT1, MkT2 #-} - {-# COMPLETE MkT1, MkT2Internal #-} - - f :: T -> Bool - f MkT1 = True - f MkT2 = False - -Which ``COMPLETE`` pragma should be used when checking the coverage of the -patterns in ``f``? If we pick the ``COMPLETE`` set that covers ``MkT1`` and -``MkT2``, then ``f`` is exhaustive, but if we pick the other ``COMPLETE`` set -that covers ``MkT1`` and ``MkT2Internal``, then ``f`` is *not* exhaustive, -since it fails to match ``MkT2Internal``. An intuitive way to solve this -dilemma is to recognize that picking the former ``COMPLETE`` set produces the -fewest number of uncovered pattern clauses, and thus is the better choice. - -GHC disambiguates between multiple ``COMPLETE`` sets based on this rationale. -To make things more formal, when the pattern-match checker requests a set of -constructors for some data type constructor ``T``, the checker returns: - -* The original set of data constructors for ``T`` -* Any ``COMPLETE`` sets of type ``T`` - -GHC then checks for pattern coverage using each of these sets. If any of these -sets passes the pattern coverage checker with no warnings, then we are done. If -each set produces at least one warning, then GHC must pick one of the sets of -warnings depending on how good the results are. The results are prioritized in -this order: - -1. Fewest uncovered clauses -2. Fewest redundant clauses -3. Fewest inaccessible clauses -4. Whether the match comes from the original set of data constructors or from a - ``COMPLETE`` pragma (prioritizing the former over the latter) - .. _overlap-pragma: ``OVERLAPPING``, ``OVERLAPPABLE``, ``OVERLAPS``, and ``INCOHERENT`` pragmas |