diff options
author | Sebastian Graf <sgraf1337@gmail.com> | 2019-09-26 08:46:22 +0000 |
---|---|---|
committer | Sebastian Graf <sgraf1337@gmail.com> | 2019-09-27 08:42:44 +0000 |
commit | c9c190e595ec540916daa9489719f78bfe278d9e (patch) | |
tree | 90083ea2bafed24f52093bf04bbee8ba92a7ddb4 | |
parent | 795986aaf33e2ffc233836b86a92a77366c91db2 (diff) | |
download | haskell-wip/MR1752-leftovers.tar.gz |
PmCheck: Elaborate what 'model' means in the user guide [skip ci]wip/MR1752-leftovers
-rw-r--r-- | docs/users_guide/using-warnings.rst | 22 |
1 files changed, 14 insertions, 8 deletions
diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst index fa44b1a370..0bc7d0a946 100644 --- a/docs/users_guide/using-warnings.rst +++ b/docs/users_guide/using-warnings.rst @@ -839,14 +839,20 @@ of ``-W(no-)*``. :default: 100 - Pattern match checking can be exponential in some cases. This limit makes - sure we scale polynomially in the number of patterns, by forgetting refined - information gained from a partially successful match. For example, when - matching ``x`` against ``Just 4``, we split each incoming matching model - into two sub-models: One where ``x`` is not ``Nothing`` and one where ``x`` - is ``Just y`` but ``y`` is not ``4``. When the number of incoming models - exceeds the limit, we continue checking the next clause with the original, - unrefined model. + The pattern match checker works by assigning symbolic values to each + pattern. We call each such assignment a 'model'. Now, each pattern match + clause leads to potentially multiple splits of that model, encoding + different ways for the pattern match to fail. For example, when matching + ``x`` against ``Just 4``, we split each incoming matching model into two + uncovered sub-models: One where ``x`` is ``Nothing`` and one where ``x`` is + ``Just y`` but ``y`` is not ``4``. + + This can be exponential in the arity of the pattern and in the number of + guards in some cases. The :ghc-flag:`-fmax-pmcheck-models` limit makes sure + we scale polynomially in the number of patterns, by forgetting refined + information gained from a partially successful match. For the above example, + if we had a limit of 1, we would continue checking the next clause with the + original, unrefined model. .. ghc-flag:: -Wincomplete-record-updates :shortdesc: warn when a record update could fail |