{-# 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.docs.barrucadu.co.uk/
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 = Settings n a -> Program pty n a -> n Bool
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
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 = Settings n a -> Program pty n a -> n Bool
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 -> Program pty n a -> n Bool)
-> (MemType -> Settings n a)
-> MemType
-> Program pty n a
-> n Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Way -> MemType -> Settings n a
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 = Settings n a
-> [(String, ProPredicate a a)] -> Program pty n a -> n Bool
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", ProPredicate a a -> ProPredicate a a
forall b a. Eq b => ProPredicate a b -> ProPredicate a b
representative ProPredicate a a
forall a. Predicate a
successful)
  , (String
"Deterministic", ProPredicate a a -> ProPredicate a a
forall b a. Eq b => ProPredicate a b -> ProPredicate a b
representative ProPredicate a a
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 = Settings n a
-> String -> ProPredicate a b -> Program pty n a -> n Bool
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
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 = Settings n a
-> String -> ProPredicate a b -> Program pty n a -> n Bool
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
 -> String -> ProPredicate a b -> Program pty n a -> n Bool)
-> (MemType -> Settings n a)
-> MemType
-> String
-> ProPredicate a b
-> Program pty n a
-> n Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Way -> MemType -> Settings n a
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 =
  Settings n a
-> [(String, ProPredicate a b)] -> Program pty n a -> n Bool
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 = Settings n a
-> [(String, ProPredicate a b)] -> Program pty n a -> n Bool
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
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 = Settings n a
-> [(String, ProPredicate a b)] -> Program pty n a -> n Bool
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
 -> [(String, ProPredicate a b)] -> Program pty n a -> n Bool)
-> (MemType -> Settings n a)
-> MemType
-> [(String, ProPredicate a b)]
-> Program pty n a
-> n Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Way -> MemType -> Settings n a
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  <- Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
forall (n :: * -> *) a pty.
MonadDejaFu n =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
runSCTWithSettings (Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
-> Maybe (Either Condition a -> Maybe Discard)
-> Settings n a
-> Settings n a
forall s a. Lens' s a -> a -> s -> s
set (Maybe (Either Condition a -> Maybe Discard)
 -> f (Maybe (Either Condition a -> Maybe Discard)))
-> Settings n a -> f (Settings n a)
Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
forall (n :: * -> *) a (f :: * -> *).
Functor f =>
(Maybe (Either Condition a -> Maybe Discard)
 -> f (Maybe (Either Condition a -> Maybe Discard)))
-> Settings n a -> f (Settings n a)
ldiscard ((Either Condition a -> Maybe Discard)
-> Maybe (Either Condition a -> Maybe Discard)
forall a. a -> Maybe a
Just Either Condition a -> Maybe Discard
discarder) Settings n a
settings) Program pty n a
conc
    [Bool]
results <- ((String, ProPredicate a b) -> n Bool)
-> [(String, ProPredicate a b)] -> n [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(String
name, ProPredicate a b
test) -> IO Bool -> n Bool
forall a. IO a -> n a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> n Bool) -> (Result b -> IO Bool) -> Result b -> n Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Result b -> IO Bool
forall a. Show a => String -> Result a -> IO Bool
doTest String
name (Result b -> n Bool) -> Result b -> n Bool
forall a b. (a -> b) -> a -> b
$ ProPredicate a b -> [(Either Condition a, Trace)] -> Result 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
    Bool -> n Bool
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
results)
  where
    discarder :: Either Condition a -> Maybe Discard
discarder = ((Either Condition a -> Maybe Discard)
 -> Either Condition a -> Maybe Discard)
-> ((Either Condition a -> Maybe Discard)
    -> (Either Condition a -> Maybe Discard)
    -> Either Condition a
    -> Maybe Discard)
-> Maybe (Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Either Condition a -> Maybe Discard)
-> Either Condition a -> Maybe Discard
forall a. a -> a
id (Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
forall a.
(Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
strengthenDiscard (Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
-> Settings n a -> Maybe (Either Condition a -> Maybe Discard)
forall s a. Lens' s a -> s -> a
get (Maybe (Either Condition a -> Maybe Discard)
 -> f (Maybe (Either Condition a -> Maybe Discard)))
-> Settings n a -> f (Settings n a)
Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
forall (n :: * -> *) a (f :: * -> *).
Functor f =>
(Maybe (Either Condition a -> Maybe Discard)
 -> f (Maybe (Either Condition a -> Maybe Discard)))
-> Settings n a -> f (Settings n a)
ldiscard Settings n a
settings) ((Either Condition a -> Maybe Discard)
 -> Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
forall a b. (a -> b) -> a -> b
$ ((String, ProPredicate a b)
 -> (Either Condition a -> Maybe Discard)
 -> Either Condition a
 -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> [(String, ProPredicate a b)]
-> Either Condition a
-> Maybe Discard
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
      ((Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
forall a.
(Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
weakenDiscard ((Either Condition a -> Maybe Discard)
 -> (Either Condition a -> Maybe Discard)
 -> Either Condition a
 -> Maybe Discard)
-> ((String, ProPredicate a b)
    -> Either Condition a -> Maybe Discard)
-> (String, ProPredicate a b)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProPredicate a b -> Either Condition a -> Maybe Discard
forall a b. ProPredicate a b -> Either Condition a -> Maybe Discard
pdiscard (ProPredicate a b -> Either Condition a -> Maybe Discard)
-> ((String, ProPredicate a b) -> ProPredicate a b)
-> (String, ProPredicate a b)
-> Either Condition a
-> Maybe Discard
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, ProPredicate a b) -> ProPredicate a b
forall a b. (a, b) -> b
snd)
      (Maybe Discard -> Either Condition a -> Maybe Discard
forall a b. a -> b -> a
const (Discard -> Maybe Discard
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
      | Int -> [(Either Condition a, Trace)] -> Bool
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 ProPredicate a b -> Either Condition a -> Maybe Discard
forall a b. ProPredicate a b -> Either Condition a -> Maybe Discard
pdiscard ProPredicate a b
p Either Condition a
efa of
              Just Discard
DiscardResultAndTrace -> Maybe (Either Condition a, [a])
forall a. Maybe a
Nothing
              Just Discard
DiscardTrace -> (Either Condition a, [a]) -> Maybe (Either Condition a, [a])
forall a. a -> Maybe a
Just (Either Condition a
efa, [])
              Maybe Discard
Nothing -> (Either Condition a, [a]) -> Maybe (Either Condition a, [a])
forall a. a -> Maybe a
Just (Either Condition a, [a])
r
        in ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
forall {a} {b}.
ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
peval ProPredicate a b
p (((Either Condition a, Trace) -> Maybe (Either Condition a, Trace))
-> [(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Either Condition a, Trace) -> Maybe (Either Condition a, Trace)
forall {a}.
(Either Condition a, [a]) -> Maybe (Either Condition a, [a])
go [(Either Condition a, Trace)]
rs)
      | Bool
otherwise = ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
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
(Result a -> Result a -> Bool)
-> (Result a -> Result a -> Bool) -> Eq (Result a)
forall a. Eq a => Result a -> Result a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Result a -> Result a -> Bool
Eq, Int -> Result a -> ShowS
[Result a] -> ShowS
Result a -> String
(Int -> Result a -> ShowS)
-> (Result a -> String) -> ([Result a] -> ShowS) -> Show (Result a)
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
$cshowsPrec :: forall a. Show a => Int -> Result a -> ShowS
showsPrec :: Int -> Result a -> ShowS
$cshow :: forall a. Show a => Result a -> String
show :: Result a -> String
$cshowList :: forall a. Show a => [Result a] -> ShowS
showList :: [Result a] -> ShowS
Show)

instance NFData a => NFData (Result a) where
  rnf :: Result a -> ()
rnf Result a
r = (Bool, [(Either Condition a, Trace)], String) -> ()
forall a. NFData a => a -> ()
rnf ( Result a -> Bool
forall a. Result a -> Bool
_pass Result a
r
              , Result a -> [(Either Condition a, Trace)]
forall a. Result a -> [(Either Condition a, Trace)]
_failures Result a
r
              , Result a -> String
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 = Bool -> [(Either Condition a, Trace)] -> String -> Result a
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 = Bool -> [(Either Condition a, Trace)] -> String -> Result a
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 = map (first $ fmap f) $ _failures r }

instance Foldable Result where
  foldMap :: forall m a. Monoid m => (a -> m) -> Result a -> m
foldMap a -> m
f Result a
r = (a -> m) -> [a] -> m
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f [a
a | (Right a
a, Trace
_) <- Result a -> [(Either Condition 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 = Settings n a -> ProPredicate a b -> Program pty n a -> n (Result b)
forall (n :: * -> *) a b pty.
MonadDejaFu n =>
Settings n a -> ProPredicate a b -> Program pty n a -> n (Result b)
runTestWithSettings Settings n a
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 = Settings n a -> ProPredicate a b -> Program pty n a -> n (Result b)
forall (n :: * -> *) a b pty.
MonadDejaFu n =>
Settings n a -> ProPredicate a b -> Program pty n a -> n (Result b)
runTestWithSettings (Settings n a
 -> ProPredicate a b -> Program pty n a -> n (Result b))
-> (MemType -> Settings n a)
-> MemType
-> ProPredicate a b
-> Program pty n a
-> n (Result b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Way -> MemType -> Settings n a
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 = ((Either Condition a -> Maybe Discard)
 -> Either Condition a -> Maybe Discard)
-> ((Either Condition a -> Maybe Discard)
    -> (Either Condition a -> Maybe Discard)
    -> Either Condition a
    -> Maybe Discard)
-> Maybe (Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Either Condition a -> Maybe Discard)
-> Either Condition a -> Maybe Discard
forall a. a -> a
id (Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
forall a.
(Either Condition a -> Maybe Discard)
-> (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
strengthenDiscard (Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
-> Settings n a -> Maybe (Either Condition a -> Maybe Discard)
forall s a. Lens' s a -> s -> a
get (Maybe (Either Condition a -> Maybe Discard)
 -> f (Maybe (Either Condition a -> Maybe Discard)))
-> Settings n a -> f (Settings n a)
Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
forall (n :: * -> *) a (f :: * -> *).
Functor f =>
(Maybe (Either Condition a -> Maybe Discard)
 -> f (Maybe (Either Condition a -> Maybe Discard)))
-> Settings n a -> f (Settings n a)
ldiscard Settings n a
settings) (ProPredicate a b -> Either Condition a -> Maybe Discard
forall a b. ProPredicate a b -> Either Condition a -> Maybe Discard
pdiscard ProPredicate a b
p)
  in ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
forall {a} {b}.
ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
peval ProPredicate a b
p ([(Either Condition a, Trace)] -> Result b)
-> n [(Either Condition a, Trace)] -> n (Result b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
forall (n :: * -> *) a pty.
MonadDejaFu n =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
runSCTWithSettings (Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
-> Maybe (Either Condition a -> Maybe Discard)
-> Settings n a
-> Settings n a
forall s a. Lens' s a -> a -> s -> s
set (Maybe (Either Condition a -> Maybe Discard)
 -> f (Maybe (Either Condition a -> Maybe Discard)))
-> Settings n a -> f (Settings n a)
Lens' (Settings n a) (Maybe (Either Condition a -> Maybe Discard))
forall (n :: * -> *) a (f :: * -> *).
Functor f =>
(Maybe (Either Condition a -> Maybe Discard)
 -> f (Maybe (Either Condition a -> Maybe Discard)))
-> Settings n a -> f (Settings n a)
ldiscard ((Either Condition a -> Maybe Discard)
-> Maybe (Either Condition a -> Maybe Discard)
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 = ProPredicate b c -> Either Condition b -> Maybe Discard
forall a b. ProPredicate a b -> Either Condition a -> Maybe Discard
pdiscard ProPredicate b c
p (Either Condition b -> Maybe Discard)
-> (Either Condition a -> Either Condition b)
-> Either Condition a
-> Maybe Discard
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> Either Condition a -> Either Condition b
forall a b. (a -> b) -> Either Condition a -> Either Condition b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f
    , peval :: [(Either Condition a, Trace)] -> Result d
peval = (c -> d) -> Result c -> Result d
forall a b. (a -> b) -> Result a -> Result b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> d
g (Result c -> Result d)
-> ([(Either Condition a, Trace)] -> Result c)
-> [(Either Condition a, Trace)]
-> Result d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProPredicate b c -> [(Either Condition b, Trace)] -> Result c
forall {a} {b}.
ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
peval ProPredicate b c
p ([(Either Condition b, Trace)] -> Result c)
-> ([(Either Condition a, Trace)] -> [(Either Condition b, Trace)])
-> [(Either Condition a, Trace)]
-> Result c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Either Condition a, Trace) -> (Either Condition b, Trace))
-> [(Either Condition a, Trace)] -> [(Either Condition b, Trace)]
forall a b. (a -> b) -> [a] -> [b]
map ((Either Condition a -> Either Condition b)
-> (Either Condition a, Trace) -> (Either Condition b, Trace)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((a -> b) -> Either Condition a -> Either Condition b
forall a b. (a -> b) -> Either Condition a -> Either Condition b
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 = (x -> x) -> (a -> b) -> ProPredicate x a -> ProPredicate x b
forall a b c d.
(a -> b) -> (c -> d) -> ProPredicate b c -> ProPredicate a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap x -> x
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)]
xs ->
      let result :: Result b
result = ProPredicate a b -> [(Either Condition a, Trace)] -> Result b
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 = simplestsBy (==) (_failures result) }
  }

-- | Check that a computation never produces a @Left@ value.
--
-- @since 1.9.1.0
successful :: Predicate a
successful :: forall a. Predicate a
successful = (Either Condition a -> Bool) -> Predicate a
forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue ((Condition -> Bool) -> (a -> Bool) -> Either Condition a -> Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Bool -> Condition -> Bool
forall a b. a -> b -> a
const Bool
False) (Bool -> a -> Bool
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 = (Either Condition a -> Bool) -> Predicate a
forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue (Bool -> Bool
not (Bool -> Bool)
-> (Either Condition a -> Bool) -> Either Condition a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Condition -> Bool) -> (a -> Bool) -> Either Condition a -> Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Condition -> Condition -> Bool
forall a. Eq a => a -> a -> Bool
==Condition
Abort) (Bool -> a -> Bool
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 = (Either Condition a -> Bool) -> Predicate a
forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue ((Either Condition a -> Bool) -> Predicate a)
-> (Either Condition a -> Bool) -> Predicate a
forall a b. (a -> b) -> a -> b
$ (Condition -> Bool) -> (a -> Bool) -> Either Condition a -> Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Condition -> Condition -> Bool
forall a. Eq a => a -> a -> Bool
==Condition
Abort) (Bool -> a -> Bool
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 = (Either Condition a -> Bool) -> Predicate a
forall a. (Either Condition a -> Bool) -> Predicate a
somewhereTrue ((Either Condition a -> Bool) -> Predicate a)
-> (Either Condition a -> Bool) -> Predicate a
forall a b. (a -> b) -> a -> b
$ (Condition -> Bool) -> (a -> Bool) -> Either Condition a -> Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Condition -> Condition -> Bool
forall a. Eq a => a -> a -> Bool
==Condition
Abort) (Bool -> a -> Bool
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 = (Either Condition a -> Bool) -> Predicate a
forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue (Bool -> Bool
not (Bool -> Bool)
-> (Either Condition a -> Bool) -> Either Condition a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Condition -> Bool) -> (a -> Bool) -> Either Condition a -> Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> Bool
isDeadlock (Bool -> a -> Bool
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 = (Either Condition a -> Bool) -> Predicate a
forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue ((Either Condition a -> Bool) -> Predicate a)
-> (Either Condition a -> Bool) -> Predicate a
forall a b. (a -> b) -> a -> b
$ (Condition -> Bool) -> (a -> Bool) -> Either Condition a -> Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> Bool
isDeadlock (Bool -> a -> Bool
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 = (Either Condition a -> Bool) -> Predicate a
forall a. (Either Condition a -> Bool) -> Predicate a
somewhereTrue ((Either Condition a -> Bool) -> Predicate a)
-> (Either Condition a -> Bool) -> Predicate a
forall a b. (a -> b) -> a -> b
$ (Condition -> Bool) -> (a -> Bool) -> Either Condition a -> Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> Bool
isDeadlock (Bool -> a -> Bool
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 = (Either Condition a -> Bool) -> Predicate a
forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue (Bool -> Bool
not (Bool -> Bool)
-> (Either Condition a -> Bool) -> Either Condition a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Condition -> Bool) -> (a -> Bool) -> Either Condition a -> Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> Bool
isUncaughtException (Bool -> a -> Bool
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 = (Either Condition a -> Bool) -> Predicate a
forall a. (Either Condition a -> Bool) -> Predicate a
alwaysTrue ((Either Condition a -> Bool) -> Predicate a)
-> (Either Condition a -> Bool) -> Predicate a
forall a b. (a -> b) -> a -> b
$ (Condition -> Bool) -> (a -> Bool) -> Either Condition a -> Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> Bool
isUncaughtException (Bool -> a -> Bool
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 = (Either Condition a -> Bool) -> Predicate a
forall a. (Either Condition a -> Bool) -> Predicate a
somewhereTrue ((Either Condition a -> Bool) -> Predicate a)
-> (Either Condition a -> Bool) -> Predicate a
forall a b. (a -> b) -> a -> b
$ (Condition -> Bool) -> (a -> Bool) -> Either Condition a -> Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> Bool
isUncaughtException (Bool -> a -> Bool
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 = (a -> a -> Bool) -> Predicate a
forall a. (a -> a -> Bool) -> Predicate a
alwaysSameBy a -> a -> Bool
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 = (a -> a -> Bool) -> Predicate a
forall a. (a -> a -> Bool) -> Predicate a
alwaysSameBy (b -> b -> Bool
forall a. Eq a => a -> a -> Bool
(==) (b -> b -> Bool) -> (a -> b) -> 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 = Maybe Discard -> Either Condition a -> Maybe Discard
forall a b. a -> b -> a
const Maybe Discard
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) = ((Either Condition a, Trace) -> Bool)
-> [(Either Condition a, Trace)]
-> ([(Either Condition a, Trace)], [(Either Condition a, Trace)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Either Condition a -> Bool
forall a b. Either a b -> Bool
isLeft (Either Condition a -> Bool)
-> ((Either Condition a, Trace) -> Either Condition a)
-> (Either Condition a, Trace)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either Condition a, Trace) -> Either Condition a
forall a b. (a, b) -> a
fst) [(Either Condition a, Trace)]
xs
          simpleSuccesses :: [(Either Condition a, Trace)]
simpleSuccesses = (Either Condition a -> Either Condition a -> Bool)
-> [(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
forall x. (x -> x -> Bool) -> [(x, Trace)] -> [(x, Trace)]
simplestsBy (a -> a -> Bool
f (a -> a -> Bool)
-> (Either Condition a -> a)
-> Either Condition a
-> Either Condition a
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Either Condition a -> a
forall a b. HasCallStack => Either a b -> b
efromRight) [(Either Condition a, Trace)]
successes
          simpleFailures :: [(Either Condition a, Trace)]
simpleFailures  = (Either Condition a -> Either Condition a -> Bool)
-> [(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
forall x. (x -> x -> Bool) -> [(x, Trace)] -> [(x, Trace)]
simplestsBy (Condition -> Condition -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Condition -> Condition -> Bool)
-> (Either Condition a -> Condition)
-> Either Condition a
-> Either Condition a
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Either Condition a -> Condition
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
        ([], []) -> Result a
forall a. Result a
defaultPass
        ([], [(Either Condition a, Trace)
_]) -> Result a
forall a. Result a
defaultPass
        ([(Either Condition a, Trace)]
_, [(Either Condition a, Trace)]
_) -> [(Either Condition a, Trace)] -> Result a
forall a. [(Either Condition a, Trace)] -> Result a
defaultFail ([(Either Condition a, Trace)]
simpleFailures [(Either Condition a, Trace)]
-> [(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
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 = (a -> a -> Bool) -> Predicate a
forall a. (a -> a -> Bool) -> Predicate a
notAlwaysSameBy a -> a -> Bool
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 = (a -> a -> Bool) -> Predicate a
forall a. (a -> a -> Bool) -> Predicate a
notAlwaysSameBy (b -> b -> Bool
forall a. Eq a => a -> a -> Bool
(==) (b -> b -> Bool) -> (a -> b) -> 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 = Maybe Discard -> Either Condition a -> Maybe Discard
forall a b. a -> b -> a
const Maybe Discard
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) = ((Either Condition a, Trace) -> Bool)
-> [(Either Condition a, Trace)]
-> ([(Either Condition a, Trace)], [(Either Condition a, Trace)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Either Condition a -> Bool
forall a b. Either a b -> Bool
isLeft (Either Condition a -> Bool)
-> ((Either Condition a, Trace) -> Either Condition a)
-> (Either Condition a, Trace)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either Condition a, Trace) -> Either Condition a
forall a b. (a, b) -> a
fst) [(Either Condition a, Trace)]
xs
            simpleFailures :: [(Either Condition a, Trace)]
simpleFailures = (Either Condition a -> Either Condition a -> Bool)
-> [(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
forall x. (x -> x -> Bool) -> [(x, Trace)] -> [(x, Trace)]
simplestsBy (Condition -> Condition -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Condition -> Condition -> Bool)
-> (Either Condition a -> Condition)
-> Either Condition a
-> Either Condition a
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Either Condition a -> Condition
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] -> [(Either Condition a, Trace)] -> Result a
forall a. [(Either Condition a, Trace)] -> Result a
defaultFail ((Either Condition a, Trace)
x (Either Condition a, Trace)
-> [(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
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 ([(Either Condition a, Trace)] -> Result a
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 = simpleFailures ++ _failures res, _pass = False }
    }
  where
    (Either a a, b)
y1 .*. :: (Either a a, b) -> (Either a a, b) -> Bool
.*. (Either a a, b)
y2 = Bool -> Bool
not ((a -> a -> Bool)
-> ((Either a a, b) -> a)
-> (Either a a, b)
-> (Either a a, b)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on a -> a -> Bool
f (Either a a -> a
forall a b. HasCallStack => Either a b -> b
efromRight (Either a a -> a)
-> ((Either a a, b) -> Either a a) -> (Either a a, b) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either a a, b) -> Either a a
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 (Either Condition a, Trace) -> (Either Condition a, Trace) -> Bool
forall {a} {b}. (Either a a, b) -> (Either a a, b) -> Bool
.*. (Either Condition a, Trace)
y2 = Result a
res { _pass = True }
      | Bool
otherwise = Result a
res { _failures = y1 : y2 : _failures 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 (Either Condition a, Trace) -> (Either Condition a, Trace) -> Bool
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)
y2(Either Condition a, Trace)
-> [(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
forall a. a -> [a] -> [a]
:[(Either Condition a, Trace)]
ys) Result a
res { _pass = True }
      | Bool
otherwise = [(Either Condition a, Trace)] -> Result a -> Result a
go ((Either Condition a, Trace)
y2(Either Condition a, Trace)
-> [(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
forall a. a -> [a] -> [a]
:[(Either Condition a, Trace)]
ys) Result a
res { _failures = y1 : y2 : _failures 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 = Maybe Discard
-> (Either Condition b -> Maybe Discard)
-> Maybe (Either Condition b)
-> Maybe Discard
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Discard -> Maybe Discard
forall a. a -> Maybe a
Just Discard
DiscardResultAndTrace) (Maybe Discard -> Either Condition b -> Maybe Discard
forall a b. a -> b -> a
const Maybe Discard
forall a. Maybe a
Nothing) (Maybe (Either Condition b) -> Maybe Discard)
-> (Either Condition a -> Maybe (Either Condition b))
-> Either Condition a
-> Maybe Discard
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 = ((Either Condition a, Trace) -> Maybe (Either Condition b, Trace))
-> [(Either Condition a, Trace)] -> [(Either Condition b, Trace)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(Either Condition a
efa,Trace
trc) -> (,Trace
trc) (Either Condition b -> (Either Condition b, Trace))
-> Maybe (Either Condition b) -> Maybe (Either Condition b, Trace)
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 Bool -> [(Either Condition b, Trace)] -> String -> Result b
forall a.
Bool -> [(Either Condition a, Trace)] -> String -> Result a
Result ([(Either Condition b, Trace)] -> Bool
forall a. [a] -> Bool
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 = (Either Condition a -> Maybe (Either Condition a))
-> ProPredicate a a
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 Maybe (Either Condition a)
forall a. Maybe a
Nothing else Either Condition a -> Maybe (Either Condition a)
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 = Maybe Discard
-> (Either Condition b -> Maybe Discard)
-> Maybe (Either Condition b)
-> Maybe Discard
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Discard -> Maybe Discard
forall a. a -> Maybe a
Just Discard
DiscardTrace) (Maybe Discard -> Either Condition b -> Maybe Discard
forall a b. a -> b -> a
const Maybe Discard
forall a. Maybe a
Nothing) (Maybe (Either Condition b) -> Maybe Discard)
-> (Either Condition a -> Maybe (Either Condition b))
-> Either Condition a
-> Maybe Discard
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 = ((Either Condition a, Trace) -> Maybe (Either Condition b, Trace))
-> [(Either Condition a, Trace)]
-> [Maybe (Either Condition b, Trace)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Either Condition a
efa,Trace
trc) -> (,Trace
trc) (Either Condition b -> (Either Condition b, Trace))
-> Maybe (Either Condition b) -> Maybe (Either Condition b, Trace)
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 Bool -> [(Either Condition b, Trace)] -> String -> Result b
forall a.
Bool -> [(Either Condition a, Trace)] -> String -> Result a
Result ((Maybe (Either Condition b, Trace) -> Bool)
-> [Maybe (Either Condition b, Trace)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe (Either Condition b, Trace) -> Bool
forall a. Maybe a -> Bool
isNothing [Maybe (Either Condition b, Trace)]
failures) ([Maybe (Either Condition b, Trace)]
-> [(Either Condition b, Trace)]
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 = (Either Condition a -> Maybe (Either Condition a))
-> ProPredicate a a
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 Maybe (Either Condition a)
forall a. Maybe a
Nothing else Either Condition a -> Maybe (Either Condition a)
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 Either Condition a -> [Either Condition a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Either Condition a]
expected then Discard -> Maybe Discard
forall a. a -> Maybe a
Just Discard
DiscardTrace else Maybe Discard
forall a. Maybe a
Nothing
    , peval :: [(Either Condition a, Trace)] -> Result a
peval = \[(Either Condition a, Trace)]
xs -> [Either Condition a]
-> [Either Condition a]
-> [(Either Condition a, Trace)]
-> Result a
-> Result a
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 (Result a -> Result a) -> Result a -> Result a
forall a b. (a -> b) -> a -> b
$ [(Either Condition a, Trace)] -> Result a
forall a. [(Either Condition a, Trace)] -> Result a
defaultFail ([(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
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 a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
waitingFor  = [a] -> [a] -> [(a, b)] -> Result a -> Result a
go ((a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/=a
x) [a]
waitingFor) (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
alreadySeen) [(a, b)]
xs Result a
res
      -- If it's a result we've already seen, continue.
      | a
x a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
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 = True }
    go [a]
es [a]
_ [] Result a
res = Result a
res { _failureMsg = unlines $ map (\a
e -> String
"Expected: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
e) es }

    failures :: [(Either Condition a, b)] -> [(Either Condition a, b)]
failures = ((Either Condition a, b) -> Bool)
-> [(Either Condition a, b)] -> [(Either Condition a, b)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Either Condition a
r, b
_) -> Either Condition a
r Either Condition a -> [Either Condition a] -> Bool
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' = [Either Condition a] -> Predicate a
forall a. (Eq a, Show a) => [Either Condition a] -> Predicate a
gives ([Either Condition a] -> Predicate a)
-> ([a] -> [Either Condition a]) -> [a] -> Predicate a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Either Condition a) -> [a] -> [Either Condition a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Either Condition a
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 <- Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (Maybe String -> Bool) -> IO (Maybe String) -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO (Maybe String)
lookupEnv String
"DEJAFU_DOCTEST"
    if Result a -> Bool
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)

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

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

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

    failmsg :: Bool -> String
failmsg Bool
True = String
"[fail] " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name
    failmsg Bool
False = String
"\27[31m[fail]\27[0m " String -> ShowS
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
moreThan Int
0 [a]
_ = Bool
True
moreThan Int
n (a
_:[a]
rest) = Int -> [a] -> Bool
forall a. Int -> [a] -> Bool
moreThan (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [a]
rest

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