As mapM in IO is strict, composing listToMaybe with counterExamples
necessitates finding ALL counterexamples first, even though only the
first is returned. So an improvement is gained by manually making it
"lazy".
New coverage report, as there have been a bunch of new tests since the
one in the CONTRIBUTING file was generated:
54% expressions used (4311/7948)
51% boolean coverage (67/131)
47% guards (50/106), 31 always True, 6 always False, 19 unevaluated
57% 'if' conditions (11/19), 2 always True, 1 always False, 5 unevaluated
100% qualifiers (6/6)
61% alternatives used (413/671)
83% local declarations used (212/254)
28% top-level declarations used (313/1099)
This lets dejafu test CoCo-style properties, and introduces a
dependency on [leancheck][].
For example, consider this statement about MVars: "using readMVar is
better than a takeMVar followed by a putMVar because the former is
atomic but the latter is not."
This module can test properties like that:
```
sig e = Sig
{ initialise = maybe newEmptyMVar newMVar
, observe = \v _ -> tryReadMVar v
, interfere = \v s -> tryTakeMVar v >>
maybe (pure ()) (void . tryPutMVar v) s
, expr = e
}
> check $ sig (void . readMVar) `equivalentTo`
sig (\v -> takeMVar v >>= putMVar v)
*** Failure: (seed Just ())
left: [(Nothing,Just ())]
right: [(Nothing,Just ()),(Just Deadlock,Just ())]
```
The two expressions are not equivalent, and we get given the
counterexample!
In addition to "equivalentTo", there is also "refines" and
"strictlyRefines" (and negated variants)
[leancheck]: https://hackage.haskell.org/package/leancheck
- `lint.sh` runs HLint, returning 1 if HLint is NOT version 1 (as the
.hlint.yaml configuration file is only supported in version 2 and
later) AND issues are found.
- `style.sh` runs stylish-haskell. I would like it to return 1 if it
reformatted anything, but the tool doesn't appear to support
reporting that :(
