{-# LANGUAGE TupleSections #-}

{- |
Module      : Test.DejaFu
Copyright   : (c) 2015--2019 Michael Walker
License     : MIT
Maintainer  : Michael Walker <mike@barrucadu.co.uk>
Stability   : experimental
Portability : TupleSections

dejafu is a library for unit-testing concurrent Haskell programs which
are written using the <https://hackage.haskell.org/package/concurrency
concurrency> package's 'MonadConc' typeclass.

For more in-depth documentation, including migration guides from
earlier versions of dejafu, see the <https://dejafu.readthedocs.io
website>.

__A first test:__ This is a simple concurrent program which forks two
threads and each races to write to the same @MVar@:

>>> :{
let example = do
      var <- newEmptyMVar
      fork (putMVar var "hello")
      fork (putMVar var "world")
      readMVar var
:}

We can test it with dejafu like so:

>>> autocheck example
[pass] Successful
[fail] Deterministic
    "hello" S0----S1--S0--
<BLANKLINE>
    "world" S0----S2--S0--
False

The 'autocheck' function takes a concurrent program to test and looks
for concurrency errors and nondeterminism.  Here we see the program is
nondeterministic, dejafu gives us all the distinct results it found
and, for each, a summarised execution trace leading to that result:

 * \"Sn\" means that thread \"n\" started executing after the previous
   thread terminated or blocked.

 * \"Pn\" means that thread \"n\" started executing, even though the
   previous thread could have continued running.

 * Each \"-\" represents one \"step\" of the computation.

__Memory models:__ dejafu supports three different memory models,
which affect how one thread's 'IORef' updates become visible to other
threads.

 * Sequential consistency: a program behaves as a simple interleaving
   of the actions in different threads. When an 'IORef' is written to,
   that write is immediately visible to all threads.

  * Total store order (TSO): each thread has a write buffer.  A thread
    sees its writes immediately, but other threads will only see
    writes when they are committed, which may happen later.  Writes
    are committed in the same order that they are created.

  * Partial store order (PSO): each 'IORef' has a write buffer.  A
    thread sees its writes immediately, but other threads will only
    see writes when they are committed, which may happen later.
    Writes to different 'IORef's are not necessarily committed in the
    same order that they are created.

This small example shows the difference between sequential consistency
and TSO:

>>> :{
let relaxed = do
      r1 <- newIORef False
      r2 <- newIORef False
      x <- spawn $ writeIORef r1 True >> readIORef r2
      y <- spawn $ writeIORef r2 True >> readIORef r1
      (,) <$> readMVar x <*> readMVar y
:}

The 'autocheckWay' function will let us specify the memory model:

>>> autocheckWay defaultWay SequentialConsistency relaxed
[pass] Successful
[fail] Deterministic
    (False,True) S0---------S1----S0--S2----S0--
<BLANKLINE>
    (True,True) S0---------S1-P2----S1---S0---
<BLANKLINE>
    (True,False) S0---------S2----S1----S0---
False

>>> autocheckWay defaultWay TotalStoreOrder relaxed
[pass] Successful
[fail] Deterministic
    (False,True) S0---------S1----S0--S2----S0--
<BLANKLINE>
    (False,False) S0---------S1--P2----S1--S0---
<BLANKLINE>
    (True,False) S0---------S2----S1----S0---
<BLANKLINE>
    (True,True) S0---------S1-C-S2----S1---S0---
False

The result @(False,False)@ is possible using TSO and PSO, but not
sequential consistency.  The \"C\" in the trace shows where a /commit/
action occurred, which makes a write to an 'IORef' visible to all
threads.

__Beware of 'liftIO':__ dejafu works by running your test case lots of
times with different schedules.  If you use 'liftIO' at all, make sure
that any @IO@ you perform is deterministic when executed in the same
order.

If you need to test things with /nondeterministc/ @IO@, see the
'autocheckWay', 'dejafuWay', and 'dejafusWay' functions: the
'randomly' and 'uniformly' testing modes can cope with nondeterminism.
-}
module Test.DejaFu
  ( -- * Unit testing

    autocheck
  , dejafu
  , dejafus

  -- ** Configuration

  {- |

There are a few knobs to tweak to control the behaviour of dejafu.
The defaults should generally be good enough, but if not you have a
few tricks available.  The main two are: the 'Way', which controls how
schedules are explored; and the 'MemType', which controls how reads
and writes to @IORef@s behave; see "Test.DejaFu.Settings" for a
complete listing.

-}

  , autocheckWay
  , dejafuWay
  , dejafusWay
  , autocheckWithSettings
  , dejafuWithSettings
  , dejafusWithSettings

  , module Test.DejaFu.Settings

  -- ** Manual testing

  {- |

The standard testing functions print their result to stdout, and throw
away some information.  The traces are pretty-printed, and if there
are many failures, only the first few are shown.

If you need more information, use these functions.

-}

  , Result(..)
  , runTest
  , runTestWay
  , runTestWithSettings

  -- ** Predicates

  {- |

A dejafu test has two parts: the concurrent program to test, and a
predicate to determine if the test passes, based on the results of the
schedule exploration.

All of these predicates discard results and traces as eagerly as
possible, to reduce memory usage.

-}

  , Predicate
  , ProPredicate(..)
  , successful
  , alwaysSame
  , notAlwaysSame
  , abortsNever
  , abortsAlways
  , abortsSometimes
  , deadlocksNever
  , deadlocksAlways
  , deadlocksSometimes
  , exceptionsNever
  , exceptionsAlways
  , exceptionsSometimes

  -- *** Helpers

  {- |

Helper functions to produce your own predicates.  Such predicates
discard results and traces as eagerly as possible, to reduce memory
usage.

-}

  , representative
  , alwaysSameOn
  , alwaysSameBy
  , notAlwaysSameOn
  , notAlwaysSameBy
  , alwaysTrue
  , somewhereTrue
  , alwaysNothing
  , somewhereNothing
  , gives
  , gives'

  -- *** Conditions

  {- |

Helper functions to identify conditions.

-}

  , Condition(..)
  , isAbort
  , isDeadlock
  , isUncaughtException
  , isInvariantFailure

  -- * Property-based testing

  {- |

dejafu can also use a property-based testing style to test stateful
operations for a variety of inputs.  Inputs are generated using the
<https://hackage.haskell.org/package/leancheck leancheck> library for
enumerative testing.

__Testing @MVar@ operations with multiple producers__: These are a
little different to the property tests you may be familiar with from
libraries like QuickCheck (and leancheck).  As we're testing
properties of /stateful/ and /concurrent/ things, we need to provide
some extra information.

A property consists of two /signatures/ and a relation between them.
A signature contains:

 * An initialisation function, to construct the initial state.

 * An observation function, to take a snapshot of the state at the
   end.

 * An interference function, to mess with the state in some way.

 * The expression to evaluate, as a function over the state.

>>> import Control.Monad (void)
>>> :{
let sig e = Sig
      { initialise = maybe newEmptyMVar newMVar
      , observe    = \v _ -> tryReadMVar v
      , interfere  = \v _ -> putMVar v 42
      , expression = void . e
      }
:}

This is a signature for operations over @Num n => MVar n@ values where
there are multiple producers.  The initialisation function takes a
@Maybe n@ and constructs an @MVar n@, empty if it gets @Nothing@; the
observation function reads the @MVar@; and the interference function
puts a new value in.

Given this signature, we can check if @readMVar@ is the same as a
@takeMVar@ followed by a @putMVar@:

>>> check $ sig readMVar === sig (\v -> takeMVar v >>= putMVar v)
*** Failure: (seed Just 0)
    left:  [(Nothing,Just 0)]
    right: [(Nothing,Just 0),(Just Deadlock,Just 42)]
False

The two expressions are not equivalent, and we get a counterexample:
if the @MVar@ is nonempty, then the left expression (@readMVar@) will
preserve the value, but the right expression (@\v -> takeMVar v >>=
putMVar v@) may cause it to change.  This is because of the concurrent
interference we have provided: the left term never empties a full
@MVar@, but the Right term does.

-}

  , module Test.DejaFu.Refinement

  -- * Expressing concurrent programs
  , Program
  , Basic
  , ConcT
  , ConcIO

  -- ** Setup and teardown
  , WithSetup
  , WithSetupAndTeardown
  , withSetup
  , withTeardown
  , withSetupAndTeardown

  -- ** Invariants
  , Invariant
  , registerInvariant
  , inspectIORef
  , inspectMVar
  , inspectTVar
) where

import           Control.Arrow          (first)
import           Control.DeepSeq        (NFData(..))
import           Control.Monad          (unless, when)
import           Control.Monad.IO.Class (MonadIO(..))
import           Data.Either            (isLeft)
import           Data.Function          (on)
import           Data.List              (intercalate, intersperse, partition)
import           Data.Maybe             (catMaybes, isJust, isNothing, mapMaybe)
import           Data.Profunctor        (Profunctor(..))
import           System.Environment     (lookupEnv)

import           Test.DejaFu.Conc
import           Test.DejaFu.Internal
import           Test.DejaFu.Refinement
import           Test.DejaFu.SCT
import           Test.DejaFu.Settings
import           Test.DejaFu.Types
import           Test.DejaFu.Utils

{- $setup

>>> import Control.Concurrent.Classy hiding (check)

>>> :{
let example = do
      var <- newEmptyMVar
      fork (putMVar var "hello")
      fork (putMVar var "world")
      readMVar var
:}

>>> :{
let relaxed = do
      r1 <- newIORef False
      r2 <- newIORef False
      x <- spawn $ writeIORef r1 True >> readIORef r2
      y <- spawn $ writeIORef r2 True >> readIORef r1
      (,) <$> readMVar x <*> readMVar y
:}

-}

-------------------------------------------------------------------------------
-- DejaFu

-- | Automatically test a computation.
--
-- In particular, concurrency errors and nondeterminism.  Returns
-- @True@ if all tests pass
--
-- >>> autocheck example
-- [pass] Successful
-- [fail] Deterministic
--     "hello" S0----S1--S0--
-- <BLANKLINE>
--     "world" S0----S2--S0--
-- False
--
-- @since 2.1.0.0
autocheck :: (MonadDejaFu n, MonadIO n, Eq a, Show a)
  => Program pty n a
  -- ^ The computation to test.
  -> n Bool
autocheck :: forall (n :: * -> *) a pty.
(MonadDejaFu n, MonadIO n, Eq a, Show a) =>
Program pty n a -> n Bool
autocheck = forall (n :: * -> *) a pty.
(MonadDejaFu n, MonadIO n, Eq a, Show a) =>
Settings n a -> Program pty n a -> n Bool
autocheckWithSettings forall (n :: * -> *) a. Applicative n => Settings n a
defaultSettings

-- | Variant of 'autocheck' which takes a way to run the program and a
-- memory model.
--
-- >>> autocheckWay defaultWay defaultMemType relaxed
-- [pass] Successful
-- [fail] Deterministic
--     (False,True) S0---------S1----S0--S2----S0--
-- <BLANKLINE>
--     (False,False) S0---------S1--P2----S1--S0---
-- <BLANKLINE>
--     (True,False) S0---------S2----S1----S0---
-- <BLANKLINE>
--     (True,True) S0---------S1-C-S2----S1---S0---
-- False
--
-- >>> autocheckWay defaultWay SequentialConsistency relaxed
-- [pass] Successful
-- [fail] Deterministic
--     (False,True) S0---------S1----S0--S2----S0--
-- <BLANKLINE>
--     (True,True) S0---------S1-P2----S1---S0---
-- <BLANKLINE>
--     (True,False) S0---------S2----S1----S0---
-- False
--
-- @since 2.1.0.0
autocheckWay :: (MonadDejaFu n, MonadIO n, Eq a, Show a)
  => Way
  -- ^ How to run the concurrent program.
  -> MemType
  -- ^ The memory model to use for non-synchronised @IORef@ operations.
  -> Program pty n a
  -- ^ The computation to test.
  -> n Bool
autocheckWay :: forall (n :: * -> *) a pty.
(MonadDejaFu n, MonadIO n, Eq a, Show a) =>
Way -> MemType -> Program pty n a -> n Bool
autocheckWay Way
way = forall (n :: * -> *) a pty.
(MonadDejaFu n, MonadIO n, Eq a, Show a) =>
Settings n a -> Program pty n a -> n Bool
autocheckWithSettings forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way

-- | Variant of 'autocheck' which takes a settings record.
--
-- >>> autocheckWithSettings (fromWayAndMemType defaultWay defaultMemType) relaxed
-- [pass] Successful
-- [fail] Deterministic
--     (False,True) S0---------S1----S0--S2----S0--
-- <BLANKLINE>
--     (False,False) S0---------S1--P2----S1--S0---
-- <BLANKLINE>
--     (True,False) S0---------S2----S1----S0---
-- <BLANKLINE>
--     (True,True) S0---------S1-C-S2----S1---S0---
-- False
--
-- >>> autocheckWithSettings (fromWayAndMemType defaultWay SequentialConsistency) relaxed
-- [pass] Successful
-- [fail] Deterministic
--     (False,True) S0---------S1----S0--S2----S0--
-- <BLANKLINE>
--     (True,True) S0---------S1-P2----S1---S0---
-- <BLANKLINE>
--     (True,False) S0---------S2----S1----S0---
-- False
--
-- @since 2.1.0.0
autocheckWithSettings :: (MonadDejaFu n, MonadIO n, Eq a, Show a)
  => Settings n a
  -- ^ The SCT settings.
  -> Program pty n a
  -- ^ The computation to test.
  -> n Bool
autocheckWithSettings :: forall (n :: * -> *) a pty.
(MonadDejaFu n, MonadIO n, Eq a, Show a) =>
Settings n a -> Program pty n a -> n Bool
autocheckWithSettings Settings n a
settings = forall (n :: * -> *) b a pty.
(MonadDejaFu n, MonadIO n, Show b) =>
Settings n a
-> [(String, ProPredicate a b)] -> Program pty n a -> n Bool
dejafusWithSettings Settings n a
settings
  [ (String
"Successful", forall b a. Eq b => ProPredicate a b -> ProPredicate a b
representative forall a. Predicate a
successful)
  , (String
"Deterministic", forall b a. Eq b => ProPredicate a b -> ProPredicate a b
representative forall a. Eq a => Predicate a
alwaysSame)
  ]

-- | Check a predicate and print the result to stdout, return 'True'
-- if it passes.
--
-- A dejafu test has two parts: the program you are testing, and a
-- predicate to determine if the test passes.  Predicates can look for
-- anything, including checking for some expected nondeterminism.
--
-- >>> dejafu "Test Name" alwaysSame example
-- [fail] Test Name
--     "hello" S0----S1--S0--
-- <BLANKLINE>
--     "world" S0----S2--S0--
-- False
--
-- @since 2.1.0.0
dejafu :: (MonadDejaFu n, MonadIO n, Show b)
  => String
  -- ^ The name of the test.
  -> ProPredicate a b
  -- ^ The predicate to check.
  -> Program pty n a
  -- ^ The computation to test.
  -> n Bool
dejafu :: forall (n :: * -> *) b a pty.
(MonadDejaFu n, MonadIO n, Show b) =>
String -> ProPredicate a b -> Program pty n a -> n Bool
dejafu = forall (n :: * -> *) b a pty.
(MonadDejaFu n, MonadIO n, Show b) =>
Settings n a
-> String -> ProPredicate a b -> Program pty n a -> n Bool
dejafuWithSettings forall (n :: * -> *) a. Applicative n => Settings n a
defaultSettings

-- | Variant of 'dejafu' which takes a way to run the program and a
-- memory model.
--
-- >>> import System.Random
--
-- >>> dejafuWay (randomly (mkStdGen 0) 100) defaultMemType "Randomly!" alwaysSame example
-- [fail] Randomly!
--     "hello" S0----S1--S0--
-- <BLANKLINE>
--     "world" S0----S2--S0--
-- False
--
-- >>> dejafuWay (randomly (mkStdGen 1) 100) defaultMemType "Randomly!" alwaysSame example
-- [fail] Randomly!
--     "hello" S0----S1--S0--
-- <BLANKLINE>
--     "world" S0---P2--S0--
-- False
--
-- @since 2.1.0.0
dejafuWay :: (MonadDejaFu n, MonadIO n, Show b)
  => Way
  -- ^ How to run the concurrent program.
  -> MemType
  -- ^ The memory model to use for non-synchronised @IORef@ operations.
  -> String
  -- ^ The name of the test.
  -> ProPredicate a b
  -- ^ The predicate to check.
  -> Program pty n a
  -- ^ The computation to test.
  -> n Bool
dejafuWay :: forall (n :: * -> *) b a pty.
(MonadDejaFu n, MonadIO n, Show b) =>
Way
-> MemType
-> String
-> ProPredicate a b
-> Program pty n a
-> n Bool
dejafuWay Way
way = forall (n :: * -> *) b a pty.
(MonadDejaFu n, MonadIO n, Show b) =>
Settings n a
-> String -> ProPredicate a b -> Program pty n a -> n Bool
dejafuWithSettings forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way

-- | Variant of 'dejafu' which takes a settings record.
--
-- >>> import System.Random
--
-- >>> dejafuWithSettings (fromWayAndMemType (randomly (mkStdGen 1) 100) defaultMemType) "Randomly!" alwaysSame example
-- [fail] Randomly!
--     "hello" S0----S1--S0--
-- <BLANKLINE>
--     "world" S0---P2--S0--
-- False
--
-- @since 2.1.0.0
dejafuWithSettings :: (MonadDejaFu n, MonadIO n, Show b)
  => Settings n a
  -- ^ The SCT settings.
  -> String
  -- ^ The name of the test.
  -> ProPredicate a b
  -- ^ The predicate to check.
  -> Program pty n a
  -- ^ The computation to test.
  -> n Bool
dejafuWithSettings :: forall (n :: * -> *) b a pty.
(MonadDejaFu n, MonadIO n, Show b) =>
Settings n a
-> String -> ProPredicate a b -> Program pty n a -> n Bool
dejafuWithSettings Settings n a
settings String
name ProPredicate a b
test =
  forall (n :: * -> *) b a pty.
(MonadDejaFu n, MonadIO n, Show b) =>
Settings n a
-> [(String, ProPredicate a b)] -> Program pty n a -> n Bool
dejafusWithSettings Settings n a
settings [(String
name, ProPredicate a b
test)]

-- | Variant of 'dejafu' which takes a collection of predicates to
-- test, returning 'True' if all pass.
--
-- >>> dejafus [("A", alwaysSame), ("B", deadlocksNever)] example
-- [fail] A
--     "hello" S0----S1--S0--
-- <BLANKLINE>
--     "world" S0----S2--S0--
-- [pass] B
-- False
--
-- @since 2.1.0.0
dejafus :: (MonadDejaFu n, MonadIO n, Show b)
  => [(String, ProPredicate a b)]
  -- ^ The list of predicates (with names) to check.
  -> Program pty n a
  -- ^ The computation to test.
  -> n Bool
dejafus :: forall (n :: * -> *) b a pty.
(MonadDejaFu n, MonadIO n, Show b) =>
[(String, ProPredicate a b)] -> Program pty n a -> n Bool
dejafus = forall (n :: * -> *) b a pty.
(MonadDejaFu n, MonadIO n, Show b) =>
Settings n a
-> [(String, ProPredicate a b)] -> Program pty n a -> n Bool
dejafusWithSettings forall (n :: * -> *) a. Applicative n => Settings n a
defaultSettings

-- | Variant of 'dejafus' which takes a way to run the program and a
-- memory model.
--
-- >>> dejafusWay defaultWay SequentialConsistency [("A", alwaysSame), ("B", exceptionsNever)] relaxed
-- [fail] A
--     (False,True) S0---------S1----S0--S2----S0--
-- <BLANKLINE>
--     (True,True) S0---------S1-P2----S1---S0---
-- <BLANKLINE>
--     (True,False) S0---------S2----S1----S0---
-- [pass] B
-- False
--
-- @since 2.1.0.0
dejafusWay :: (MonadDejaFu n, MonadIO n, Show b)
  => Way
  -- ^ How to run the concurrent program.
  -> MemType
  -- ^ The memory model to use for non-synchronised @IORef@ operations.
  -> [(String, ProPredicate a b)]
  -- ^ The list of predicates (with names) to check.
  -> Program pty n a
  -- ^ The computation to test.
  -> n Bool
dejafusWay :: forall (n :: * -> *) b a pty.
(MonadDejaFu n, MonadIO n, Show b) =>
Way
-> MemType
-> [(String, ProPredicate a b)]
-> Program pty n a
-> n Bool
dejafusWay Way
way = forall (n :: * -> *) b a pty.
(MonadDejaFu n, MonadIO n, Show b) =>
Settings n a
-> [(String, ProPredicate a b)] -> Program pty n a -> n Bool
dejafusWithSettings forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way

-- | Variant of 'dejafus' which takes a settings record.
--
-- >>> dejafusWithSettings (fromWayAndMemType defaultWay SequentialConsistency) [("A", alwaysSame), ("B", exceptionsNever)] relaxed
-- [fail] A
--     (False,True) S0---------S1----S0--S2----S0--
-- <BLANKLINE>
--     (True,True) S0---------S1-P2----S1---S0---
-- <BLANKLINE>
--     (True,False) S0---------S2----S1----S0---
-- [pass] B
-- False
--
-- @since 2.1.0.0
dejafusWithSettings :: (MonadDejaFu n, MonadIO n, Show b)
  => Settings n a
  -- ^ The SCT settings.
  -> [(String, ProPredicate a b)]
  -- ^ The list of predicates (with names) to check.
  -> Program pty n a
  -- ^ The computation to test.
  -> n Bool
dejafusWithSettings :: forall (n :: * -> *) b a pty.
(MonadDejaFu n, MonadIO n, Show b) =>
Settings n a
-> [(String, ProPredicate a b)] -> Program pty n a -> n Bool
dejafusWithSettings Settings n a
settings [(String, ProPredicate a b)]
tests Program pty n a
conc = do
    [(Either Condition a, Trace)]
traces  <- forall (n :: * -> *) a pty.
MonadDejaFu n =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
runSCTWithSettings (forall s a. Lens' s a -> a -> s -> s
set forall (n :: * -> *) a.
Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
ldiscard (forall a. a -> Maybe a
Just Either Condition a -> Maybe Discard
discarder) Settings n a
settings) Program pty n a
conc
    [Bool]
results <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(String
name, ProPredicate a b
test) -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => String -> Result a -> IO Bool
doTest String
name forall a b. (a -> b) -> a -> b
$ forall {a} {b}.
ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
chk ProPredicate a b
test [(Either Condition a, Trace)]
traces) [(String, ProPredicate a b)]
tests
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
results)
  where
    discarder :: Either Condition a -> Maybe Discard
discarder = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall a.
(Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
strengthenDiscard (forall s a. Lens' s a -> s -> a
get forall (n :: * -> *) a.
Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
ldiscard Settings n a
settings) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
      (forall a.
(Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
weakenDiscard forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. ProPredicate a b -> Either Condition a -> Maybe Discard
pdiscard forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)
      (forall a b. a -> b -> a
const (forall a. a -> Maybe a
Just Discard
DiscardResultAndTrace))
      [(String, ProPredicate a b)]
tests

    -- for evaluating each individual predicate, we only want the
    -- results/traces it would not discard, but the traces set may
    -- include more than this if the different predicates have
    -- different discard functions, so we do another pass of
    -- discarding.
    chk :: ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
chk ProPredicate a b
p [(Either Condition a, Trace)]
rs
      | forall a. Int -> [a] -> Bool
moreThan Int
1 [(Either Condition a, Trace)]
rs =
        let go :: (Either Condition a, [a]) -> Maybe (Either Condition a, [a])
go r :: (Either Condition a, [a])
r@(Either Condition a
efa, [a]
_) = case forall a b. ProPredicate a b -> Either Condition a -> Maybe Discard
pdiscard ProPredicate a b
p Either Condition a
efa of
              Just Discard
DiscardResultAndTrace -> forall a. Maybe a
Nothing
              Just Discard
DiscardTrace -> forall a. a -> Maybe a
Just (Either Condition a
efa, [])
              Maybe Discard
Nothing -> forall a. a -> Maybe a
Just (Either Condition a, [a])
r
        in forall {a} {b}.
ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
peval ProPredicate a b
p (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {a}.
(Either Condition a, [a]) -> Maybe (Either Condition a, [a])
go [(Either Condition a, Trace)]
rs)
      | Bool
otherwise = forall {a} {b}.
ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
peval ProPredicate a b
p [(Either Condition a, Trace)]
rs

-------------------------------------------------------------------------------
-- Test cases

-- | The results of a test, including the number of cases checked to
-- determine the final boolean outcome.
--
-- @since 1.0.0.0
data Result a = Result
  { forall a. Result a -> Bool
_pass :: Bool
  -- ^ Whether the test passed or not.
  , forall a. Result a -> [(Either Condition a, Trace)]
_failures :: [(Either Condition a, Trace)]
  -- ^ The failing cases, if any.
  , forall a. Result a -> String
_failureMsg :: String
  -- ^ A message to display on failure, if nonempty
  } deriving (Result a -> Result a -> Bool
forall a. Eq a => Result a -> Result a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Result a -> Result a -> Bool
$c/= :: forall a. Eq a => Result a -> Result a -> Bool
== :: Result a -> Result a -> Bool
$c== :: forall a. Eq a => Result a -> Result a -> Bool
Eq, Int -> Result a -> ShowS
forall a. Show a => Int -> Result a -> ShowS
forall a. Show a => [Result a] -> ShowS
forall a. Show a => Result a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Result a] -> ShowS
$cshowList :: forall a. Show a => [Result a] -> ShowS
show :: Result a -> String
$cshow :: forall a. Show a => Result a -> String
showsPrec :: Int -> Result a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Result a -> ShowS
Show)

instance NFData a => NFData (Result a) where
  rnf :: Result a -> ()
rnf Result a
r = forall a. NFData a => a -> ()
rnf ( forall a. Result a -> Bool
_pass Result a
r
              , forall a. Result a -> [(Either Condition a, Trace)]
_failures Result a
r
              , forall a. Result a -> String
_failureMsg Result a
r
              )

-- | A failed result, taking the given list of failures.
defaultFail :: [(Either Condition a, Trace)] -> Result a
defaultFail :: forall a. [(Either Condition a, Trace)] -> Result a
defaultFail [(Either Condition a, Trace)]
failures = forall a.
Bool -> [(Either Condition a, Trace)] -> String -> Result a
Result Bool
False [(Either Condition a, Trace)]
failures String
""

-- | A passed result.
defaultPass :: Result a
defaultPass :: forall a. Result a
defaultPass = forall a.
Bool -> [(Either Condition a, Trace)] -> String -> Result a
Result Bool
True [] String
""

instance Functor Result where
  fmap :: forall a b. (a -> b) -> Result a -> Result b
fmap a -> b
f Result a
r = Result a
r { _failures :: [(Either Condition b, Trace)]
_failures = forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) forall a b. (a -> b) -> a -> b
$ forall a. Result a -> [(Either Condition a, Trace)]
_failures Result a
r }

instance Foldable Result where
  foldMap :: forall m a. Monoid m => (a -> m) -> Result a -> m
foldMap a -> m
f Result a
r = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f [a
a | (Right a
a, Trace
_) <- forall a. Result a -> [(Either Condition a, Trace)]
_failures Result a
r]

-- | Run a predicate over all executions within the default schedule
-- bounds.
--
-- The exact executions tried, and the order in which results are
-- found, is unspecified and may change between releases.  This may
-- affect which failing traces are reported, when there is a failure.
--
-- @since 2.1.0.0
runTest :: MonadDejaFu n
  => ProPredicate a b
  -- ^ The predicate to check
  -> Program pty n a
  -- ^ The computation to test
  -> n (Result b)
runTest :: forall (n :: * -> *) a b pty.
MonadDejaFu n =>
ProPredicate a b -> Program pty n a -> n (Result b)
runTest = forall (n :: * -> *) a b pty.
MonadDejaFu n =>
Settings n a -> ProPredicate a b -> Program pty n a -> n (Result b)
runTestWithSettings forall (n :: * -> *) a. Applicative n => Settings n a
defaultSettings

-- | Variant of 'runTest' which takes a way to run the program and a
-- memory model.
--
-- The exact executions tried, and the order in which results are
-- found, is unspecified and may change between releases.  This may
-- affect which failing traces are reported, when there is a failure.
--
-- @since 2.1.0.0
runTestWay :: MonadDejaFu n
  => Way
  -- ^ How to run the concurrent program.
  -> MemType
  -- ^ The memory model to use for non-synchronised @IORef@ operations.
  -> ProPredicate a b
  -- ^ The predicate to check
  -> Program pty n a
  -- ^ The computation to test
  -> n (Result b)
runTestWay :: forall (n :: * -> *) a b pty.
MonadDejaFu n =>
Way
-> MemType -> ProPredicate a b -> Program pty n a -> n (Result b)
runTestWay Way
way = forall (n :: * -> *) a b pty.
MonadDejaFu n =>
Settings n a -> ProPredicate a b -> Program pty n a -> n (Result b)
runTestWithSettings forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way

-- | Variant of 'runTest' which takes a settings record.
--
-- The exact executions tried, and the order in which results are
-- found, is unspecified and may change between releases.  This may
-- affect which failing traces are reported, when there is a failure.
--
-- @since 2.1.0.0
runTestWithSettings :: MonadDejaFu n
  => Settings n a
  -- ^ The SCT settings.
  -> ProPredicate a b
  -- ^ The predicate to check
  -> Program pty n a
  -- ^ The computation to test
  -> n (Result b)
runTestWithSettings :: forall (n :: * -> *) a b pty.
MonadDejaFu n =>
Settings n a -> ProPredicate a b -> Program pty n a -> n (Result b)
runTestWithSettings Settings n a
settings ProPredicate a b
p Program pty n a
conc =
  let discarder :: Either Condition a -> Maybe Discard
discarder = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall a.
(Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
strengthenDiscard (forall s a. Lens' s a -> s -> a
get forall (n :: * -> *) a.
Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
ldiscard Settings n a
settings) (forall a b. ProPredicate a b -> Either Condition a -> Maybe Discard
pdiscard ProPredicate a b
p)
  in forall {a} {b}.
ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
peval ProPredicate a b
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (n :: * -> *) a pty.
MonadDejaFu n =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
runSCTWithSettings (forall s a. Lens' s a -> a -> s -> s
set forall (n :: * -> *) a.
Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
ldiscard (forall a. a -> Maybe a
Just Either Condition a -> Maybe Discard
discarder) Settings n a
settings) Program pty n a
conc


-------------------------------------------------------------------------------
-- Predicates

-- | A @Predicate@ is a function which collapses a list of results
-- into a 'Result', possibly discarding some on the way.
--
-- @Predicate@ cannot be a functor as the type parameter is used both
-- co- and contravariantly.
--
-- @since 1.0.0.0
type Predicate a = ProPredicate a a

-- | A @ProPredicate@ is a function which collapses a list of results
-- into a 'Result', possibly discarding some on the way.
--
-- @since 1.0.0.0
data ProPredicate a b = ProPredicate
  { forall a b. ProPredicate a b -> Either Condition a -> Maybe Discard
pdiscard :: Either Condition a -> Maybe Discard
  -- ^ Selectively discard results before computing the result.
  , forall {a} {b}.
ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
peval :: [(Either Condition a, Trace)] -> Result b
  -- ^ Compute the result with the un-discarded results.
  }

instance Profunctor ProPredicate where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> ProPredicate b c -> ProPredicate a d
dimap a -> b
f c -> d
g ProPredicate b c
p = ProPredicate
    { pdiscard :: Either Condition a -> Maybe Discard
pdiscard = forall a b. ProPredicate a b -> Either Condition a -> Maybe Discard
pdiscard ProPredicate b c
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f
    , peval :: [(Either Condition a, Trace)] -> Result d
peval = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> d
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a} {b}.
ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
peval ProPredicate b c
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f))
    }

instance Functor (ProPredicate x) where
  fmap :: forall a b. (a -> b) -> ProPredicate x a -> ProPredicate x b
fmap = forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap forall a. a -> a
id

-- | Reduce the list of failures in a @ProPredicate@ to one
-- representative trace for each unique result.
--
-- This may throw away \"duplicate\" failures which have a unique
-- cause but happen to manifest in the same way. However, it is
-- convenient for filtering out true duplicates.
--
-- @since 1.0.0.0
representative :: Eq b => ProPredicate a b -> ProPredicate a b
representative :: forall b a. Eq b => ProPredicate a b -> ProPredicate a b
representative ProPredicate a b
p = ProPredicate a b
p
  { peval :: [(Either Condition a, Trace)] -> Result b
peval = \[(Either Condition a, Trace)]
xs ->
      let result :: Result b
result = forall {a} {b}.
ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
peval ProPredicate a b
p [(Either Condition a, Trace)]
xs
      in Result b
result { _failures :: [(Either Condition b, Trace)]
_failures = forall x. (x -> x -> Bool) -> [(x, Trace)] -> [(x, Trace)]
simplestsBy forall a. Eq a => a -> a -> Bool
(==) (forall a. Result a -> [(Either Condition a, Trace)]
_failures Result b
result) }
  }

-- | Check that a computation never produces a @Left@ value.
--
-- @since 1.9.1.0
successful :: Predicate a
successful :: forall a. Predicate a
successful = forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const Bool
False) (forall a b. a -> b -> a
const Bool
True))

-- | Check that a computation never aborts.
--
-- Any result other than an abort, including other 'Condition's, is
-- allowed.
--
-- @since 1.0.0.0
abortsNever :: Predicate a
abortsNever :: forall a. Predicate a
abortsNever = forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a. Eq a => a -> a -> Bool
==Condition
Abort) (forall a b. a -> b -> a
const Bool
False))

-- | Check that a computation always aborts.
--
-- @since 1.0.0.0
abortsAlways :: Predicate a
abortsAlways :: forall a. Predicate a
abortsAlways = forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a. Eq a => a -> a -> Bool
==Condition
Abort) (forall a b. a -> b -> a
const Bool
False)

-- | Check that a computation aborts at least once.
--
-- Any result other than an abort, including other 'Condition's, is
-- allowed.
--
-- @since 1.0.0.0
abortsSometimes :: Predicate a
abortsSometimes :: forall a. Predicate a
abortsSometimes = forall a. (Either Condition a -> Bool) -> Predicate a
somewhereTrue forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a. Eq a => a -> a -> Bool
==Condition
Abort) (forall a b. a -> b -> a
const Bool
False)

-- | Check that a computation never deadlocks.
--
-- Any result other than a deadlock, including other 'Condition's, is
-- allowed.
--
-- @since 1.0.0.0
deadlocksNever :: Predicate a
deadlocksNever :: forall a. Predicate a
deadlocksNever = forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> Bool
isDeadlock (forall a b. a -> b -> a
const Bool
False))

-- | Check that a computation always deadlocks.
--
-- @since 1.0.0.0
deadlocksAlways :: Predicate a
deadlocksAlways :: forall a. Predicate a
deadlocksAlways = forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> Bool
isDeadlock (forall a b. a -> b -> a
const Bool
False)

-- | Check that a computation deadlocks at least once.
--
-- Any result other than a deadlock, including other 'Condition's, is
-- allowed.
--
-- @since 1.0.0.0
deadlocksSometimes :: Predicate a
deadlocksSometimes :: forall a. Predicate a
deadlocksSometimes = forall a. (Either Condition a -> Bool) -> Predicate a
somewhereTrue forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> Bool
isDeadlock (forall a b. a -> b -> a
const Bool
False)

-- | Check that a computation never fails with an uncaught exception.
--
-- Any result other than an uncaught exception, including other
-- 'Condition's, is allowed.
--
-- @since 1.0.0.0
exceptionsNever :: Predicate a
exceptionsNever :: forall a. Predicate a
exceptionsNever = forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> Bool
isUncaughtException (forall a b. a -> b -> a
const Bool
False))

-- | Check that a computation always fails with an uncaught exception.
--
-- @since 1.0.0.0
exceptionsAlways :: Predicate a
exceptionsAlways :: forall a. Predicate a
exceptionsAlways = forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> Bool
isUncaughtException (forall a b. a -> b -> a
const Bool
False)

-- | Check that a computation fails with an uncaught exception at least once.
--
-- Any result other than an uncaught exception, including other
-- 'Condition's, is allowed.
--
-- @since 1.0.0.0
exceptionsSometimes :: Predicate a
exceptionsSometimes :: forall a. Predicate a
exceptionsSometimes = forall a. (Either Condition a -> Bool) -> Predicate a
somewhereTrue forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> Bool
isUncaughtException (forall a b. a -> b -> a
const Bool
False)

-- | Check that a computation always gives the same, @Right@, result.
--
-- > alwaysSame = alwaysSameBy (==)
--
-- @since 1.10.0.0
alwaysSame :: Eq a => Predicate a
alwaysSame :: forall a. Eq a => Predicate a
alwaysSame = forall a. (a -> a -> Bool) -> Predicate a
alwaysSameBy forall a. Eq a => a -> a -> Bool
(==)

-- | Check that a computation always gives the same (according to the
-- provided function), @Right@, result.
--
-- > alwaysSameOn = alwaysSameBy ((==) `on` f)
--
-- @since 1.10.0.0
alwaysSameOn :: Eq b => (a -> b) -> Predicate a
alwaysSameOn :: forall b a. Eq b => (a -> b) -> Predicate a
alwaysSameOn a -> b
f = forall a. (a -> a -> Bool) -> Predicate a
alwaysSameBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f)

-- | Check that the result of a computation is always the same, using
-- some transformation on results.
--
-- @since 1.10.0.0
alwaysSameBy :: (a -> a -> Bool) -> Predicate a
alwaysSameBy :: forall a. (a -> a -> Bool) -> Predicate a
alwaysSameBy a -> a -> Bool
f = ProPredicate
  { pdiscard :: Either Condition a -> Maybe Discard
pdiscard = forall a b. a -> b -> a
const forall a. Maybe a
Nothing
  , peval :: [(Either Condition a, Trace)] -> Result a
peval = \[(Either Condition a, Trace)]
xs ->
      let ([(Either Condition a, Trace)]
failures, [(Either Condition a, Trace)]
successes) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (forall a b. Either a b -> Bool
isLeft forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Either Condition a, Trace)]
xs
          simpleSuccesses :: [(Either Condition a, Trace)]
simpleSuccesses = forall x. (x -> x -> Bool) -> [(x, Trace)] -> [(x, Trace)]
simplestsBy (a -> a -> Bool
f forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. HasCallStack => Either a b -> b
efromRight) [(Either Condition a, Trace)]
successes
          simpleFailures :: [(Either Condition a, Trace)]
simpleFailures  = forall x. (x -> x -> Bool) -> [(x, Trace)] -> [(x, Trace)]
simplestsBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. HasCallStack => Either a b -> a
efromLeft) [(Either Condition a, Trace)]
failures
      in case ([(Either Condition a, Trace)]
simpleFailures, [(Either Condition a, Trace)]
simpleSuccesses) of
        ([], []) -> forall a. Result a
defaultPass
        ([], [(Either Condition a, Trace)
_]) -> forall a. Result a
defaultPass
        ([(Either Condition a, Trace)]
_, [(Either Condition a, Trace)]
_) -> forall a. [(Either Condition a, Trace)] -> Result a
defaultFail ([(Either Condition a, Trace)]
simpleFailures forall a. [a] -> [a] -> [a]
++ [(Either Condition a, Trace)]
simpleSuccesses)
  }

-- | Check that a computation never fails, and gives multiple distinct
-- @Right@ results.
--
-- > notAlwaysSame = notAlwaysSameBy (==)
--
-- @since 1.10.0.0
notAlwaysSame :: Eq a => Predicate a
notAlwaysSame :: forall a. Eq a => Predicate a
notAlwaysSame = forall a. (a -> a -> Bool) -> Predicate a
notAlwaysSameBy forall a. Eq a => a -> a -> Bool
(==)

-- | Check that a computation never fails, and gives multiple distinct
-- (according to the provided function) @Right@ results.
--
-- > notAlwaysSameOn = notAlwaysSameBy ((==) `on` f)
--
-- @since 1.10.0.0
notAlwaysSameOn :: Eq b => (a -> b) -> Predicate a
notAlwaysSameOn :: forall b a. Eq b => (a -> b) -> Predicate a
notAlwaysSameOn a -> b
f = forall a. (a -> a -> Bool) -> Predicate a
notAlwaysSameBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f)

-- | Check that a computation never fails, and gives multiple distinct
-- @Right@ results, by applying a transformation on results.
--
-- This inverts the condition, so (eg) @notAlwaysSameBy (==)@ will
-- pass if there are unequal results.
--
-- @since 1.10.0.0
notAlwaysSameBy :: (a -> a -> Bool) -> Predicate a
notAlwaysSameBy :: forall a. (a -> a -> Bool) -> Predicate a
notAlwaysSameBy a -> a -> Bool
f = ProPredicate
    { pdiscard :: Either Condition a -> Maybe Discard
pdiscard = forall a b. a -> b -> a
const forall a. Maybe a
Nothing
    , peval :: [(Either Condition a, Trace)] -> Result a
peval = \[(Either Condition a, Trace)]
xs ->
        let ([(Either Condition a, Trace)]
failures, [(Either Condition a, Trace)]
successes) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (forall a b. Either a b -> Bool
isLeft forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Either Condition a, Trace)]
xs
            simpleFailures :: [(Either Condition a, Trace)]
simpleFailures = forall x. (x -> x -> Bool) -> [(x, Trace)] -> [(x, Trace)]
simplestsBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. HasCallStack => Either a b -> a
efromLeft) [(Either Condition a, Trace)]
failures
        in case [(Either Condition a, Trace)]
successes of
          [(Either Condition a, Trace)
x] -> forall a. [(Either Condition a, Trace)] -> Result a
defaultFail ((Either Condition a, Trace)
x forall a. a -> [a] -> [a]
: [(Either Condition a, Trace)]
simpleFailures)
          [(Either Condition a, Trace)]
_  ->
            let res :: Result a
res = [(Either Condition a, Trace)] -> Result a -> Result a
go [(Either Condition a, Trace)]
successes (forall a. [(Either Condition a, Trace)] -> Result a
defaultFail [])
            in case [(Either Condition a, Trace)]
failures of
              [] -> Result a
res
              [(Either Condition a, Trace)]
_ -> Result a
res { _failures :: [(Either Condition a, Trace)]
_failures = [(Either Condition a, Trace)]
simpleFailures forall a. [a] -> [a] -> [a]
++ forall a. Result a -> [(Either Condition a, Trace)]
_failures Result a
res, _pass :: Bool
_pass = Bool
False }
    }
  where
    (Either a a, b)
y1 .*. :: (Either a a, b) -> (Either a a, b) -> Bool
.*. (Either a a, b)
y2 = Bool -> Bool
not (forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on a -> a -> Bool
f (forall a b. HasCallStack => Either a b -> b
efromRight forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) (Either a a, b)
y1 (Either a a, b)
y2)

    go :: [(Either Condition a, Trace)] -> Result a -> Result a
go [(Either Condition a, Trace)
y1,(Either Condition a, Trace)
y2] Result a
res
      | (Either Condition a, Trace)
y1 forall {a} {b}. (Either a a, b) -> (Either a a, b) -> Bool
.*. (Either Condition a, Trace)
y2 = Result a
res { _pass :: Bool
_pass = Bool
True }
      | Bool
otherwise = Result a
res { _failures :: [(Either Condition a, Trace)]
_failures = (Either Condition a, Trace)
y1 forall a. a -> [a] -> [a]
: (Either Condition a, Trace)
y2 forall a. a -> [a] -> [a]
: forall a. Result a -> [(Either Condition a, Trace)]
_failures Result a
res }
    go ((Either Condition a, Trace)
y1:(Either Condition a, Trace)
y2:[(Either Condition a, Trace)]
ys) Result a
res
      | (Either Condition a, Trace)
y1 forall {a} {b}. (Either a a, b) -> (Either a a, b) -> Bool
.*. (Either Condition a, Trace)
y2 = [(Either Condition a, Trace)] -> Result a -> Result a
go ((Either Condition a, Trace)
y2forall a. a -> [a] -> [a]
:[(Either Condition a, Trace)]
ys) Result a
res { _pass :: Bool
_pass = Bool
True }
      | Bool
otherwise = [(Either Condition a, Trace)] -> Result a -> Result a
go ((Either Condition a, Trace)
y2forall a. a -> [a] -> [a]
:[(Either Condition a, Trace)]
ys) Result a
res { _failures :: [(Either Condition a, Trace)]
_failures = (Either Condition a, Trace)
y1 forall a. a -> [a] -> [a]
: (Either Condition a, Trace)
y2 forall a. a -> [a] -> [a]
: forall a. Result a -> [(Either Condition a, Trace)]
_failures Result a
res }
    go [(Either Condition a, Trace)]
_ Result a
res = Result a
res

-- | Check that a @Maybe@-producing function always returns 'Nothing'.
--
-- @since 1.0.0.0
alwaysNothing :: (Either Condition a -> Maybe (Either Condition b)) -> ProPredicate a b
alwaysNothing :: forall a b.
(Either Condition a -> Maybe (Either Condition b))
-> ProPredicate a b
alwaysNothing Either Condition a -> Maybe (Either Condition b)
f = ProPredicate
  { pdiscard :: Either Condition a -> Maybe Discard
pdiscard = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. a -> Maybe a
Just Discard
DiscardResultAndTrace) (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Condition a -> Maybe (Either Condition b)
f
  , peval :: [(Either Condition a, Trace)] -> Result b
peval = \[(Either Condition a, Trace)]
xs ->
      let failures :: [(Either Condition b, Trace)]
failures = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(Either Condition a
efa,Trace
trc) -> (,Trace
trc) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either Condition a -> Maybe (Either Condition b)
f Either Condition a
efa) [(Either Condition a, Trace)]
xs
      in forall a.
Bool -> [(Either Condition a, Trace)] -> String -> Result a
Result (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Either Condition b, Trace)]
failures) [(Either Condition b, Trace)]
failures String
""
  }

-- | Check that the result of a unary boolean predicate is always
-- true.
--
-- @since 1.0.0.0
alwaysTrue :: (Either Condition a -> Bool) -> Predicate a
alwaysTrue :: forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue Either Condition a -> Bool
p = forall a b.
(Either Condition a -> Maybe (Either Condition b))
-> ProPredicate a b
alwaysNothing (\Either Condition a
efa -> if Either Condition a -> Bool
p Either Condition a
efa then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just Either Condition a
efa)

-- | Check that a @Maybe@-producing function returns 'Nothing' at
-- least once.
--
-- @since 1.0.0.0
somewhereNothing :: (Either Condition a -> Maybe (Either Condition b)) -> ProPredicate a b
somewhereNothing :: forall a b.
(Either Condition a -> Maybe (Either Condition b))
-> ProPredicate a b
somewhereNothing Either Condition a -> Maybe (Either Condition b)
f = ProPredicate
  { pdiscard :: Either Condition a -> Maybe Discard
pdiscard = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. a -> Maybe a
Just Discard
DiscardTrace) (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Condition a -> Maybe (Either Condition b)
f
  , peval :: [(Either Condition a, Trace)] -> Result b
peval = \[(Either Condition a, Trace)]
xs ->
      let failures :: [Maybe (Either Condition b, Trace)]
failures = forall a b. (a -> b) -> [a] -> [b]
map (\(Either Condition a
efa,Trace
trc) -> (,Trace
trc) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either Condition a -> Maybe (Either Condition b)
f Either Condition a
efa) [(Either Condition a, Trace)]
xs
      in forall a.
Bool -> [(Either Condition a, Trace)] -> String -> Result a
Result (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. Maybe a -> Bool
isNothing [Maybe (Either Condition b, Trace)]
failures) (forall a. [Maybe a] -> [a]
catMaybes [Maybe (Either Condition b, Trace)]
failures) String
""
  }

-- | Check that the result of a unary boolean predicate is true at
-- least once.
--
-- @since 1.0.0.0
somewhereTrue :: (Either Condition a -> Bool) -> Predicate a
somewhereTrue :: forall a. (Either Condition a -> Bool) -> Predicate a
somewhereTrue Either Condition a -> Bool
p = forall a b.
(Either Condition a -> Maybe (Either Condition b))
-> ProPredicate a b
somewhereNothing (\Either Condition a
efa -> if Either Condition a -> Bool
p Either Condition a
efa then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just Either Condition a
efa)

-- | Predicate for when there is a known set of results where every
-- result must be exhibited at least once.
--
-- @since 1.0.0.0
gives :: (Eq a, Show a) => [Either Condition a] -> Predicate a
gives :: forall a. (Eq a, Show a) => [Either Condition a] -> Predicate a
gives [Either Condition a]
expected = ProPredicate
    { pdiscard :: Either Condition a -> Maybe Discard
pdiscard = \Either Condition a
efa -> if Either Condition a
efa forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Either Condition a]
expected then forall a. a -> Maybe a
Just Discard
DiscardTrace else forall a. Maybe a
Nothing
    , peval :: [(Either Condition a, Trace)] -> Result a
peval = \[(Either Condition a, Trace)]
xs -> forall {a} {b} {a}.
(Eq a, Show a) =>
[a] -> [a] -> [(a, b)] -> Result a -> Result a
go [Either Condition a]
expected [] [(Either Condition a, Trace)]
xs forall a b. (a -> b) -> a -> b
$ forall a. [(Either Condition a, Trace)] -> Result a
defaultFail (forall {b}. [(Either Condition a, b)] -> [(Either Condition a, b)]
failures [(Either Condition a, Trace)]
xs)
    }
  where
    go :: [a] -> [a] -> [(a, b)] -> Result a -> Result a
go [a]
waitingFor [a]
alreadySeen ((a
x, b
_):[(a, b)]
xs) Result a
res
      -- If it's a result we're waiting for, move it to the
      -- @alreadySeen@ list and continue.
      | a
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
waitingFor  = [a] -> [a] -> [(a, b)] -> Result a -> Result a
go (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/=a
x) [a]
waitingFor) (a
xforall a. a -> [a] -> [a]
:[a]
alreadySeen) [(a, b)]
xs Result a
res
      -- If it's a result we've already seen, continue.
      | a
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
alreadySeen = [a] -> [a] -> [(a, b)] -> Result a -> Result a
go [a]
waitingFor [a]
alreadySeen [(a, b)]
xs Result a
res
      -- If it's not a result we expected, fail.
      | Bool
otherwise = Result a
res

    go [] [a]
_ [] Result a
res = Result a
res { _pass :: Bool
_pass = Bool
True }
    go [a]
es [a]
_ [] Result a
res = Result a
res { _failureMsg :: String
_failureMsg = [String] -> String
unlines forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\a
e -> String
"Expected: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
e) [a]
es }

    failures :: [(Either Condition a, b)] -> [(Either Condition a, b)]
failures = forall a. (a -> Bool) -> [a] -> [a]
filter (\(Either Condition a
r, b
_) -> Either Condition a
r forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Either Condition a]
expected)

-- | Variant of 'gives' that doesn't allow for @Left@ results.
--
-- > gives' = gives . map Right
--
-- @since 1.0.0.0
gives' :: (Eq a, Show a) => [a] -> Predicate a
gives' :: forall a. (Eq a, Show a) => [a] -> Predicate a
gives' = forall a. (Eq a, Show a) => [Either Condition a] -> Predicate a
gives forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. b -> Either a b
Right


-------------------------------------------------------------------------------
-- Utils

-- | Run a test and print to stdout
doTest :: Show a => String -> Result a -> IO Bool
doTest :: forall a. Show a => String -> Result a -> IO Bool
doTest String
name Result a
result = do
    Bool
doctest <- forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO (Maybe String)
lookupEnv String
"DEJAFU_DOCTEST"
    if forall a. Result a -> Bool
_pass Result a
result
    then String -> IO ()
putStrLn (Bool -> String
passmsg Bool
doctest)
    else do
      -- Display a failure message, and the first 5 (simplified) failed traces
      String -> IO ()
putStrLn (Bool -> String
failmsg Bool
doctest)

      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ forall a. Result a -> String
_failureMsg Result a
result) forall a b. (a -> b) -> a -> b
$
        String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall a. Result a -> String
_failureMsg Result a
result

      let failures :: [(Either Condition a, Trace)]
failures = forall a. Result a -> [(Either Condition a, Trace)]
_failures Result a
result
      let output :: [IO ()]
output = forall a b. (a -> b) -> [a] -> [b]
map (\(Either Condition a
r, Trace
t) -> String -> IO ()
putStrLn forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
indent forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> String
showCondition forall a. Show a => a -> String
show Either Condition a
r forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Trace -> String
showTrace Trace
t) forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
5 [(Either Condition a, Trace)]
failures
      forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> [a]
intersperse (String -> IO ()
putStrLn String
"") [IO ()]
output
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Int -> [a] -> Bool
moreThan Int
5 [(Either Condition a, Trace)]
failures) forall a b. (a -> b) -> a -> b
$
        String -> IO ()
putStrLn (ShowS
indent String
"...")

    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Result a -> Bool
_pass Result a
result)
  where
    passmsg :: Bool -> String
passmsg Bool
True = String
"[pass] " forall a. [a] -> [a] -> [a]
++ String
name
    passmsg Bool
False = String
"\27[32m[pass]\27[0m " forall a. [a] -> [a] -> [a]
++ String
name

    failmsg :: Bool -> String
failmsg Bool
True = String
"[fail] " forall a. [a] -> [a] -> [a]
++ String
name
    failmsg Bool
False = String
"\27[31m[fail]\27[0m " forall a. [a] -> [a] -> [a]
++ String
name

-- | Check if a list is longer than some value, without needing to
-- compute the entire length.
moreThan :: Int -> [a] -> Bool
moreThan :: forall a. Int -> [a] -> Bool
moreThan Int
n [] = Int
n forall a. Ord a => a -> a -> Bool
< Int
0
moreThan Int
0 [a]
_ = Bool
True
moreThan Int
n (a
_:[a]
rest) = forall a. Int -> [a] -> Bool
moreThan (Int
nforall a. Num a => a -> a -> a
-Int
1) [a]
rest

-- | Indent every line of a string.
indent :: String -> String
indent :: ShowS
indent = forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (String
"    "forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines