{-# 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 = autocheckWithSettings 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 way = autocheckWithSettings . fromWayAndMemType 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 settings = dejafusWithSettings settings
  [ ("Successful", representative successful)
  , ("Deterministic", representative 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 = dejafuWithSettings 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----S2--S1-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 way = dejafuWithSettings . fromWayAndMemType 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----S2--S1-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 settings name test =
  dejafusWithSettings settings [(name, 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 = dejafusWithSettings 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 way = dejafusWithSettings . fromWayAndMemType 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 settings tests conc = do
    traces  <- runSCTWithSettings (set ldiscard (Just discarder) settings) conc
    results <- mapM (\(name, test) -> liftIO . doTest name $ chk test traces) tests
    pure (and results)
  where
    discarder = maybe id strengthenDiscard (get ldiscard settings) $ foldr
      (weakenDiscard . pdiscard . snd)
      (const (Just DiscardResultAndTrace))
      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 p rs
      | moreThan 1 rs =
        let go r@(efa, _) = case pdiscard p efa of
              Just DiscardResultAndTrace -> Nothing
              Just DiscardTrace -> Just (efa, [])
              Nothing -> Just r
        in peval p (mapMaybe go rs)
      | otherwise = peval p 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
  { _pass :: Bool
  -- ^ Whether the test passed or not.
  , _failures :: [(Either Condition a, Trace)]
  -- ^ The failing cases, if any.
  , _failureMsg :: String
  -- ^ A message to display on failure, if nonempty
  } deriving (Eq, Show)

instance NFData a => NFData (Result a) where
  rnf r = rnf ( _pass r
              , _failures r
              , _failureMsg r
              )

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

-- | A passed result.
defaultPass :: Result a
defaultPass = Result True [] ""

instance Functor Result where
  fmap f r = r { _failures = map (first $ fmap f) $ _failures r }

instance Foldable Result where
  foldMap f r = foldMap f [a | (Right a, _) <- _failures 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 = runTestWithSettings 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 way = runTestWithSettings . fromWayAndMemType 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 settings p conc =
  let discarder = maybe id strengthenDiscard (get ldiscard settings) (pdiscard p)
  in peval p <$> runSCTWithSettings (set ldiscard (Just discarder) settings) 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
  { pdiscard :: Either Condition a -> Maybe Discard
  -- ^ Selectively discard results before computing the result.
  , peval :: [(Either Condition a, Trace)] -> Result b
  -- ^ Compute the result with the un-discarded results.
  }

instance Profunctor ProPredicate where
  dimap f g p = ProPredicate
    { pdiscard = pdiscard p . fmap f
    , peval = fmap g . peval p . map (first (fmap f))
    }

instance Functor (ProPredicate x) where
  fmap = dimap 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 p = p
  { peval = \xs ->
      let result = peval p xs
      in result { _failures = simplestsBy (==) (_failures result) }
  }

-- | Check that a computation never produces a @Left@ value.
--
-- @since 1.9.1.0
successful :: Predicate a
successful = alwaysTrue (either (const False) (const 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 = alwaysTrue (not . either (==Abort) (const False))

-- | Check that a computation always aborts.
--
-- @since 1.0.0.0
abortsAlways :: Predicate a
abortsAlways = alwaysTrue $ either (==Abort) (const 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 = somewhereTrue $ either (==Abort) (const 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 = alwaysTrue (not . either isDeadlock (const False))

-- | Check that a computation always deadlocks.
--
-- @since 1.0.0.0
deadlocksAlways :: Predicate a
deadlocksAlways = alwaysTrue $ either isDeadlock (const 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 = somewhereTrue $ either isDeadlock (const 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 = alwaysTrue (not . either isUncaughtException (const False))

-- | Check that a computation always fails with an uncaught exception.
--
-- @since 1.0.0.0
exceptionsAlways :: Predicate a
exceptionsAlways = alwaysTrue $ either isUncaughtException (const 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 = somewhereTrue $ either isUncaughtException (const False)

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

-- | 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 f = alwaysSameBy ((==) `on` 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 f = ProPredicate
  { pdiscard = const Nothing
  , peval = \xs ->
      let (failures, successes) = partition (isLeft . fst) xs
          simpleSuccesses = simplestsBy (f `on` efromRight) successes
          simpleFailures  = simplestsBy ((==) `on` efromLeft) failures
      in case (simpleFailures, simpleSuccesses) of
        ([], []) -> defaultPass
        ([], [_]) -> defaultPass
        (_, _) -> defaultFail (simpleFailures ++ 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 = notAlwaysSameBy (==)

-- | 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 f = notAlwaysSameBy ((==) `on` 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 f = ProPredicate
    { pdiscard = const Nothing
    , peval = \xs ->
        let (failures, successes) = partition (isLeft . fst) xs
            simpleFailures = simplestsBy ((==) `on` efromLeft) failures
        in case successes of
          [x] -> defaultFail (x : simpleFailures)
          _  ->
            let res = go successes (defaultFail [])
            in case failures of
              [] -> res
              _ -> res { _failures = simpleFailures ++ _failures res, _pass = False }
    }
  where
    y1 .*. y2 = not (on f (efromRight . fst) y1 y2)

    go [y1,y2] res
      | y1 .*. y2 = res { _pass = True }
      | otherwise = res { _failures = y1 : y2 : _failures res }
    go (y1:y2:ys) res
      | y1 .*. y2 = go (y2:ys) res { _pass = True }
      | otherwise = go (y2:ys) res { _failures = y1 : y2 : _failures res }
    go _ res = 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 f = ProPredicate
  { pdiscard = maybe (Just DiscardResultAndTrace) (const Nothing) . f
  , peval = \xs ->
      let failures = mapMaybe (\(efa,trc) -> (,trc) <$> f efa) xs
      in Result (null failures) failures ""
  }

-- | 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 p = alwaysNothing (\efa -> if p efa then Nothing else Just 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 f = ProPredicate
  { pdiscard = maybe (Just DiscardTrace) (const Nothing) . f
  , peval = \xs ->
      let failures = map (\(efa,trc) -> (,trc) <$> f efa) xs
      in Result (any isNothing failures) (catMaybes failures) ""
  }

-- | 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 p = somewhereNothing (\efa -> if p efa then Nothing else Just 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 expected = ProPredicate
    { pdiscard = \efa -> if efa `elem` expected then Just DiscardTrace else Nothing
    , peval = \xs -> go expected [] xs $ defaultFail (failures xs)
    }
  where
    go waitingFor alreadySeen ((x, _):xs) res
      -- If it's a result we're waiting for, move it to the
      -- @alreadySeen@ list and continue.
      | x `elem` waitingFor  = go (filter (/=x) waitingFor) (x:alreadySeen) xs res
      -- If it's a result we've already seen, continue.
      | x `elem` alreadySeen = go waitingFor alreadySeen xs res
      -- If it's not a result we expected, fail.
      | otherwise = res

    go [] _ [] res = res { _pass = True }
    go es _ [] res = res { _failureMsg = unlines $ map (\e -> "Expected: " ++ show e) es }

    failures = filter (\(r, _) -> r `notElem` 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' = gives . map Right


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

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

      unless (null $ _failureMsg result) $
        putStrLn $ _failureMsg result

      let failures = _failures result
      let output = map (\(r, t) -> putStrLn . indent $ either showCondition show r ++ " " ++ showTrace t) $ take 5 failures
      sequence_ $ intersperse (putStrLn "") output
      when (moreThan 5 failures) $
        putStrLn (indent "...")

    pure (_pass result)
  where
    passmsg True = "[pass] " ++ name
    passmsg False = "\27[32m[pass]\27[0m " ++ name

    failmsg True = "[fail] " ++ name
    failmsg False = "\27[31m[fail]\27[0m " ++ name

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

-- | Indent every line of a string.
indent :: String -> String
indent = intercalate "\n" . map ("    "++) . lines