diff options
author | Sebastian Graf <sgraf1337@gmail.com> | 2019-09-26 08:46:22 +0000 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2019-09-27 22:10:17 -0400 |
commit | 289fc8da2a29dab8282538a0ddc5db7617cdca5b (patch) | |
tree | 29b50e58abf8374b286f35b80a7f757e74a4aa39 /docs/users_guide/using-warnings.rst | |
parent | 4f81fab062e521b6b59f3f7b93bc410fd1111166 (diff) | |
download | haskell-289fc8da2a29dab8282538a0ddc5db7617cdca5b.tar.gz |
PmCheck: Elaborate what 'model' means in the user guide [skip ci]
Diffstat (limited to 'docs/users_guide/using-warnings.rst')
-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 |