This PR is a collection of patches that, when taken together, fix #60, #61, and #76:
Use Maybe (instead of an arbitrary MonadPlus) in decode and solveWith
As noted in https://github.com/ekmett/ersatz/issues/61, it's not clear what the intended behavior of decode/solveWith should be for MonadPlus instances like []. Moreover, the internals of ersatz more-or-less already assume that we are working in Maybe, and nearly all uses of solveWith in the wild pick Maybe to begin with. To avoid potential confusion, let's just concretize decode/solveWith to always work over Maybe.
Return consistent results for unconstrained literals
Previously, ersatz would always decode every unconstrained Literal to False, which could produce inconsistent results for things like do { b <- exists; pure [b, not b] }, which would decode to [False, False]. We now adopt the convention that unconstrained non-negative Literals always decode to False, and that unconstrained negative Literals always decode to True, so the example above now decodes to [False, True].
The exact meaning of what solveWith returns is not obvious at a first glance. This patch provides some Haddocks for solveWith that better explains this and provides a complete example of how to use solveWith.
This PR is a collection of patches that, when taken together, fix #60, #61, and #76:
Use
Maybe(instead of an arbitraryMonadPlus) indecodeandsolveWithAs noted in https://github.com/ekmett/ersatz/issues/61, it's not clear what the intended behavior of
decode/solveWithshould be forMonadPlusinstances like[]. Moreover, the internals ofersatzmore-or-less already assume that we are working inMaybe, and nearly all uses ofsolveWithin the wild pickMaybeto begin with. To avoid potential confusion, let's just concretizedecode/solveWithto always work overMaybe.Fixes https://github.com/ekmett/ersatz/issues/61.
Return consistent results for unconstrained literals
Previously,
ersatzwould always decode every unconstrainedLiteraltoFalse, which could produce inconsistent results for things likedo { b <- exists; pure [b, not b] }, which would decode to[False, False]. We now adopt the convention that unconstrained non-negativeLiterals always decode toFalse, and that unconstrained negativeLiterals always decode toTrue, so the example above now decodes to[False, True].Fixes https://github.com/ekmett/ersatz/issues/60. Fixes https://github.com/ekmett/ersatz/issues/76.
Provide Haddocks for
solveWithThe exact meaning of what
solveWithreturns is not obvious at a first glance. This patch provides some Haddocks forsolveWiththat better explains this and provides a complete example of how to usesolveWith.