-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Systematic testing for Haskell concurrency.
--   
--   <i>[Déjà Fu is] A martial art in which the user's limbs move in time
--   as well as space, […] It is best described as "the feeling that you
--   have been kicked in the head this way before"</i> -- Terry Pratchett,
--   Thief of Time
--   
--   Concurrency is nice, deadlocks and race conditions not so much. The
--   <tt>Par</tt> monad family, as defined in <a>abstract-par</a> provides
--   deterministic parallelism, but sometimes we can tolerate a bit of
--   nondeterminism.
--   
--   This package builds on the <a>concurrency</a> package by enabling you
--   to systematically and deterministically test your concurrent programs.
@package dejafu
@version 0.7.0.2


-- | Common types and functions used throughout DejaFu.
module Test.DejaFu.Common

-- | Every live thread has a unique identitifer.
data ThreadId
ThreadId :: (Maybe String) -> Int -> ThreadId

-- | Every <tt>CRef</tt> has a unique identifier.
data CRefId
CRefId :: (Maybe String) -> Int -> CRefId

-- | Every <tt>MVar</tt> has a unique identifier.
data MVarId
MVarId :: (Maybe String) -> Int -> MVarId

-- | Every <tt>TVar</tt> has a unique identifier.
data TVarId
TVarId :: (Maybe String) -> Int -> TVarId

-- | The ID of the initial thread.
initialThread :: ThreadId

-- | The number of ID parameters was getting a bit unwieldy, so this hides
--   them all away.
data IdSource
Id :: Int -> Int -> Int -> Int -> [String] -> [String] -> [String] -> [String] -> IdSource
[_nextCRId] :: IdSource -> Int
[_nextMVId] :: IdSource -> Int
[_nextTVId] :: IdSource -> Int
[_nextTId] :: IdSource -> Int
[_usedCRNames] :: IdSource -> [String]
[_usedMVNames] :: IdSource -> [String]
[_usedTVNames] :: IdSource -> [String]
[_usedTNames] :: IdSource -> [String]

-- | Get the next free <a>CRefId</a>.
nextCRId :: String -> IdSource -> (IdSource, CRefId)

-- | Get the next free <a>MVarId</a>.
nextMVId :: String -> IdSource -> (IdSource, MVarId)

-- | Get the next free <a>TVarId</a>.
nextTVId :: String -> IdSource -> (IdSource, TVarId)

-- | Get the next free <a>ThreadId</a>.
nextTId :: String -> IdSource -> (IdSource, ThreadId)

-- | The initial ID source.
initialIdSource :: IdSource

-- | All the actions that a thread can perform.
data ThreadAction

-- | Start a new thread.
Fork :: ThreadId -> ThreadAction

-- | Get the <a>ThreadId</a> of the current thread.
MyThreadId :: ThreadAction

-- | Get the number of Haskell threads that can run simultaneously.
GetNumCapabilities :: Int -> ThreadAction

-- | Set the number of Haskell threads that can run simultaneously.
SetNumCapabilities :: Int -> ThreadAction

-- | Yield the current thread.
Yield :: ThreadAction

-- | Create a new <tt>MVar</tt>.
NewMVar :: MVarId -> ThreadAction

-- | Put into a <tt>MVar</tt>, possibly waking up some threads.
PutMVar :: MVarId -> [ThreadId] -> ThreadAction

-- | Get blocked on a put.
BlockedPutMVar :: MVarId -> ThreadAction

-- | Try to put into a <tt>MVar</tt>, possibly waking up some threads.
TryPutMVar :: MVarId -> Bool -> [ThreadId] -> ThreadAction

-- | Read from a <tt>MVar</tt>.
ReadMVar :: MVarId -> ThreadAction

-- | Try to read from a <tt>MVar</tt>.
TryReadMVar :: MVarId -> Bool -> ThreadAction

-- | Get blocked on a read.
BlockedReadMVar :: MVarId -> ThreadAction

-- | Take from a <tt>MVar</tt>, possibly waking up some threads.
TakeMVar :: MVarId -> [ThreadId] -> ThreadAction

-- | Get blocked on a take.
BlockedTakeMVar :: MVarId -> ThreadAction

-- | Try to take from a <tt>MVar</tt>, possibly waking up some threads.
TryTakeMVar :: MVarId -> Bool -> [ThreadId] -> ThreadAction

-- | Create a new <tt>CRef</tt>.
NewCRef :: CRefId -> ThreadAction

-- | Read from a <tt>CRef</tt>.
ReadCRef :: CRefId -> ThreadAction

-- | Read from a <tt>CRef</tt> for a future compare-and-swap.
ReadCRefCas :: CRefId -> ThreadAction

-- | Modify a <tt>CRef</tt>.
ModCRef :: CRefId -> ThreadAction

-- | Modify a <tt>CRef</tt> using a compare-and-swap.
ModCRefCas :: CRefId -> ThreadAction

-- | Write to a <tt>CRef</tt> without synchronising.
WriteCRef :: CRefId -> ThreadAction

-- | Attempt to to a <tt>CRef</tt> using a compare-and-swap, synchronising
--   it.
CasCRef :: CRefId -> Bool -> ThreadAction

-- | Commit the last write to the given <tt>CRef</tt> by the given thread,
--   so that all threads can see the updated value.
CommitCRef :: ThreadId -> CRefId -> ThreadAction

-- | An STM transaction was executed, possibly waking up some threads.
STM :: TTrace -> [ThreadId] -> ThreadAction

-- | Got blocked in an STM transaction.
BlockedSTM :: TTrace -> ThreadAction

-- | Register a new exception handler
Catching :: ThreadAction

-- | Pop the innermost exception handler from the stack.
PopCatching :: ThreadAction

-- | Throw an exception.
Throw :: ThreadAction

-- | Throw an exception to a thread.
ThrowTo :: ThreadId -> ThreadAction

-- | Get blocked on a <tt>throwTo</tt>.
BlockedThrowTo :: ThreadId -> ThreadAction

-- | Killed by an uncaught exception.
Killed :: ThreadAction

-- | Set the masking state. If <a>True</a>, this is being used to set the
--   masking state to the original state in the argument passed to a
--   <tt>mask</tt>ed function.
SetMasking :: Bool -> MaskingState -> ThreadAction

-- | Return to an earlier masking state. If <a>True</a>, this is being used
--   to return to the state of the masked block in the argument passed to a
--   <tt>mask</tt>ed function.
ResetMasking :: Bool -> MaskingState -> ThreadAction

-- | Lift an IO action. Note that this can only happen with
--   <tt>ConcIO</tt>.
LiftIO :: ThreadAction

-- | A <a>return</a> or <a>pure</a> action was executed.
Return :: ThreadAction

-- | Cease execution and terminate.
Stop :: ThreadAction

-- | Start executing an action with <tt>subconcurrency</tt>.
Subconcurrency :: ThreadAction

-- | Stop executing an action with <tt>subconcurrency</tt>.
StopSubconcurrency :: ThreadAction

-- | Check if a <tt>ThreadAction</tt> immediately blocks.
isBlock :: ThreadAction -> Bool

-- | Get the <tt>TVar</tt>s affected by a <tt>ThreadAction</tt>.
tvarsOf :: ThreadAction -> Set TVarId

-- | A one-step look-ahead at what a thread will do next.
data Lookahead

-- | Will start a new thread.
WillFork :: Lookahead

-- | Will get the <a>ThreadId</a>.
WillMyThreadId :: Lookahead

-- | Will get the number of Haskell threads that can run simultaneously.
WillGetNumCapabilities :: Lookahead

-- | Will set the number of Haskell threads that can run simultaneously.
WillSetNumCapabilities :: Int -> Lookahead

-- | Will yield the current thread.
WillYield :: Lookahead

-- | Will create a new <tt>MVar</tt>.
WillNewMVar :: Lookahead

-- | Will put into a <tt>MVar</tt>, possibly waking up some threads.
WillPutMVar :: MVarId -> Lookahead

-- | Will try to put into a <tt>MVar</tt>, possibly waking up some threads.
WillTryPutMVar :: MVarId -> Lookahead

-- | Will read from a <tt>MVar</tt>.
WillReadMVar :: MVarId -> Lookahead

-- | Will try to read from a <tt>MVar</tt>.
WillTryReadMVar :: MVarId -> Lookahead

-- | Will take from a <tt>MVar</tt>, possibly waking up some threads.
WillTakeMVar :: MVarId -> Lookahead

-- | Will try to take from a <tt>MVar</tt>, possibly waking up some
--   threads.
WillTryTakeMVar :: MVarId -> Lookahead

-- | Will create a new <tt>CRef</tt>.
WillNewCRef :: Lookahead

-- | Will read from a <tt>CRef</tt>.
WillReadCRef :: CRefId -> Lookahead

-- | Will read from a <tt>CRef</tt> for a future compare-and-swap.
WillReadCRefCas :: CRefId -> Lookahead

-- | Will modify a <tt>CRef</tt>.
WillModCRef :: CRefId -> Lookahead

-- | Will modify a <tt>CRef</tt> using a compare-and-swap.
WillModCRefCas :: CRefId -> Lookahead

-- | Will write to a <tt>CRef</tt> without synchronising.
WillWriteCRef :: CRefId -> Lookahead

-- | Will attempt to to a <tt>CRef</tt> using a compare-and-swap,
--   synchronising it.
WillCasCRef :: CRefId -> Lookahead

-- | Will commit the last write by the given thread to the <tt>CRef</tt>.
WillCommitCRef :: ThreadId -> CRefId -> Lookahead

-- | Will execute an STM transaction, possibly waking up some threads.
WillSTM :: Lookahead

-- | Will register a new exception handler
WillCatching :: Lookahead

-- | Will pop the innermost exception handler from the stack.
WillPopCatching :: Lookahead

-- | Will throw an exception.
WillThrow :: Lookahead

-- | Will throw an exception to a thread.
WillThrowTo :: ThreadId -> Lookahead

-- | Will set the masking state. If <a>True</a>, this is being used to set
--   the masking state to the original state in the argument passed to a
--   <tt>mask</tt>ed function.
WillSetMasking :: Bool -> MaskingState -> Lookahead

-- | Will return to an earlier masking state. If <a>True</a>, this is being
--   used to return to the state of the masked block in the argument passed
--   to a <tt>mask</tt>ed function.
WillResetMasking :: Bool -> MaskingState -> Lookahead

-- | Will lift an IO action. Note that this can only happen with
--   <tt>ConcIO</tt>.
WillLiftIO :: Lookahead

-- | Will execute a <a>return</a> or <a>pure</a> action.
WillReturn :: Lookahead

-- | Will cease execution and terminate.
WillStop :: Lookahead

-- | Will execute an action with <tt>subconcurrency</tt>.
WillSubconcurrency :: Lookahead

-- | Will stop executing an extion with <tt>subconcurrency</tt>.
WillStopSubconcurrency :: Lookahead

-- | Convert a <a>ThreadAction</a> into a <a>Lookahead</a>: "rewind" what
--   has happened. <a>Killed</a> has no <a>Lookahead</a> counterpart.
rewind :: ThreadAction -> Maybe Lookahead

-- | Check if an operation could enable another thread.
willRelease :: Lookahead -> Bool

-- | A simplified view of the possible actions a thread can perform.
data ActionType

-- | A <tt>readCRef</tt> or a <tt>readForCAS</tt>.
UnsynchronisedRead :: CRefId -> ActionType

-- | A <tt>writeCRef</tt>.
UnsynchronisedWrite :: CRefId -> ActionType

-- | Some other action which doesn't require cross-thread communication.
UnsynchronisedOther :: ActionType

-- | A commit.
PartiallySynchronisedCommit :: CRefId -> ActionType

-- | A <tt>casCRef</tt>
PartiallySynchronisedWrite :: CRefId -> ActionType

-- | A <tt>modifyCRefCAS</tt>
PartiallySynchronisedModify :: CRefId -> ActionType

-- | An <tt>atomicModifyCRef</tt>.
SynchronisedModify :: CRefId -> ActionType

-- | A <tt>readMVar</tt> or <tt>takeMVar</tt> (or
--   <tt>try</tt>/<tt>blocked</tt> variants).
SynchronisedRead :: MVarId -> ActionType

-- | A <tt>putMVar</tt> (or <tt>try</tt>/<tt>blocked</tt> variant).
SynchronisedWrite :: MVarId -> ActionType

-- | Some other action which does require cross-thread communication.
SynchronisedOther :: ActionType

-- | Check if an action imposes a write barrier.
isBarrier :: ActionType -> Bool

-- | Check if an action commits a given <tt>CRef</tt>.
isCommit :: ActionType -> CRefId -> Bool

-- | Check if an action synchronises a given <tt>CRef</tt>.
synchronises :: ActionType -> CRefId -> Bool

-- | Get the <tt>CRef</tt> affected.
crefOf :: ActionType -> Maybe CRefId

-- | Get the <tt>MVar</tt> affected.
mvarOf :: ActionType -> Maybe MVarId

-- | Throw away information from a <a>ThreadAction</a> and give a
--   simplified view of what is happening.
--   
--   This is used in the SCT code to help determine interesting alternative
--   scheduling decisions.
simplifyAction :: ThreadAction -> ActionType

-- | Variant of <a>simplifyAction</a> that takes a <a>Lookahead</a>.
simplifyLookahead :: Lookahead -> ActionType

-- | A trace of an STM transaction is just a list of actions that occurred,
--   as there are no scheduling decisions to make.
type TTrace = [TAction]

-- | All the actions that an STM transaction can perform.
data TAction

-- | Create a new <tt>TVar</tt>
TNew :: TAction

-- | Read from a <tt>TVar</tt>.
TRead :: TVarId -> TAction

-- | Write to a <tt>TVar</tt>.
TWrite :: TVarId -> TAction

-- | Abort and discard effects.
TRetry :: TAction

-- | Execute a transaction until it succeeds (<tt>STMStop</tt>) or aborts
--   (<tt>STMRetry</tt>) and, if it aborts, execute the other transaction.
TOrElse :: TTrace -> (Maybe TTrace) -> TAction

-- | Throw an exception, abort, and discard effects.
TThrow :: TAction

-- | Execute a transaction until it succeeds (<tt>STMStop</tt>) or aborts
--   (<tt>STMThrow</tt>). If the exception is of the appropriate type, it
--   is handled and execution continues; otherwise aborts, propagating the
--   exception upwards.
TCatch :: TTrace -> (Maybe TTrace) -> TAction

-- | Terminate successfully and commit effects.
TStop :: TAction

-- | One of the outputs of the runner is a <tt>Trace</tt>, which is a log
--   of decisions made, all the runnable threads and what they would do,
--   and the action a thread took in its step.
type Trace = [(Decision, [(ThreadId, NonEmpty Lookahead)], ThreadAction)]

-- | Scheduling decisions are based on the state of the running program,
--   and so we can capture some of that state in recording what specific
--   decision we made.
data Decision

-- | Start a new thread, because the last was blocked (or it's the start of
--   computation).
Start :: ThreadId -> Decision

-- | Continue running the last thread for another step.
Continue :: Decision

-- | Pre-empt the running thread, and switch to another.
SwitchTo :: ThreadId -> Decision

-- | Pretty-print a trace, including a key of the thread IDs (not including
--   thread 0). Each line of the key is indented by two spaces.
showTrace :: Trace -> String

-- | Count the number of pre-emptions in a schedule prefix.
--   
--   Commit threads complicate this a bit. Conceptually, commits are
--   happening truly in parallel, nondeterministically. The commit thread
--   implementation is just there to unify the two sources of
--   nondeterminism: commit timing and thread scheduling.
--   
--   SO, we don't count a switch TO a commit thread as a preemption.
--   HOWEVER, the switch FROM a commit thread counts as a preemption if it
--   is not to the thread that the commit interrupted.
preEmpCount :: [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Int

-- | An indication of how a concurrent computation failed.
data Failure

-- | Will be raised if the scheduler does something bad. This should never
--   arise unless you write your own, faulty, scheduler! If it does, please
--   file a bug report.
InternalError :: Failure

-- | The scheduler chose to abort execution. This will be produced if, for
--   example, all possible decisions exceed the specified bounds (there
--   have been too many pre-emptions, the computation has executed for too
--   long, or there have been too many yields).
Abort :: Failure

-- | The computation became blocked indefinitely on <tt>MVar</tt>s.
Deadlock :: Failure

-- | The computation became blocked indefinitely on <tt>TVar</tt>s.
STMDeadlock :: Failure

-- | An uncaught exception bubbled to the top of the computation.
UncaughtException :: Failure

-- | Calls to <tt>subconcurrency</tt> were nested, or attempted when
--   multiple threads existed.
IllegalSubconcurrency :: Failure

-- | Pretty-print a failure
showFail :: Failure -> String

-- | The memory model to use for non-synchronised <tt>CRef</tt> operations.
data MemType

-- | The most intuitive model: a program behaves as a simple interleaving
--   of the actions in different threads. When a <tt>CRef</tt> is written
--   to, that write is immediately visible to all threads.
SequentialConsistency :: MemType

-- | 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.
TotalStoreOrder :: MemType

-- | Each <tt>CRef</tt> 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 <tt>CRef</tt>s
--   are not necessarily committed in the same order that they are created.
PartialStoreOrder :: MemType
instance GHC.Enum.Bounded Test.DejaFu.Common.MemType
instance GHC.Enum.Enum Test.DejaFu.Common.MemType
instance GHC.Classes.Ord Test.DejaFu.Common.MemType
instance GHC.Read.Read Test.DejaFu.Common.MemType
instance GHC.Show.Show Test.DejaFu.Common.MemType
instance GHC.Classes.Eq Test.DejaFu.Common.MemType
instance GHC.Enum.Bounded Test.DejaFu.Common.Failure
instance GHC.Enum.Enum Test.DejaFu.Common.Failure
instance GHC.Classes.Ord Test.DejaFu.Common.Failure
instance GHC.Read.Read Test.DejaFu.Common.Failure
instance GHC.Show.Show Test.DejaFu.Common.Failure
instance GHC.Classes.Eq Test.DejaFu.Common.Failure
instance GHC.Show.Show Test.DejaFu.Common.Decision
instance GHC.Classes.Eq Test.DejaFu.Common.Decision
instance GHC.Show.Show Test.DejaFu.Common.ThreadAction
instance GHC.Classes.Eq Test.DejaFu.Common.ThreadAction
instance GHC.Show.Show Test.DejaFu.Common.TAction
instance GHC.Classes.Eq Test.DejaFu.Common.TAction
instance GHC.Show.Show Test.DejaFu.Common.ActionType
instance GHC.Classes.Eq Test.DejaFu.Common.ActionType
instance GHC.Show.Show Test.DejaFu.Common.Lookahead
instance GHC.Classes.Eq Test.DejaFu.Common.Lookahead
instance GHC.Show.Show Test.DejaFu.Common.IdSource
instance GHC.Classes.Ord Test.DejaFu.Common.IdSource
instance GHC.Classes.Eq Test.DejaFu.Common.IdSource
instance GHC.Classes.Eq Test.DejaFu.Common.TVarId
instance GHC.Classes.Eq Test.DejaFu.Common.MVarId
instance GHC.Classes.Eq Test.DejaFu.Common.CRefId
instance GHC.Classes.Eq Test.DejaFu.Common.ThreadId
instance GHC.Classes.Ord Test.DejaFu.Common.ThreadId
instance GHC.Show.Show Test.DejaFu.Common.ThreadId
instance Control.DeepSeq.NFData Test.DejaFu.Common.ThreadId
instance GHC.Classes.Ord Test.DejaFu.Common.CRefId
instance GHC.Show.Show Test.DejaFu.Common.CRefId
instance Control.DeepSeq.NFData Test.DejaFu.Common.CRefId
instance GHC.Classes.Ord Test.DejaFu.Common.MVarId
instance GHC.Show.Show Test.DejaFu.Common.MVarId
instance Control.DeepSeq.NFData Test.DejaFu.Common.MVarId
instance GHC.Classes.Ord Test.DejaFu.Common.TVarId
instance GHC.Show.Show Test.DejaFu.Common.TVarId
instance Control.DeepSeq.NFData Test.DejaFu.Common.TVarId
instance Control.DeepSeq.NFData Test.DejaFu.Common.IdSource
instance Control.DeepSeq.NFData Test.DejaFu.Common.ThreadAction
instance Control.DeepSeq.NFData Test.DejaFu.Common.Lookahead
instance Control.DeepSeq.NFData Test.DejaFu.Common.ActionType
instance Control.DeepSeq.NFData Test.DejaFu.Common.TAction
instance Control.DeepSeq.NFData Test.DejaFu.Common.Decision
instance Control.DeepSeq.NFData Test.DejaFu.Common.Failure
instance Control.DeepSeq.NFData Test.DejaFu.Common.MemType


-- | <tt>MonadSTM</tt> testing implementation, internal types and
--   definitions. This module is NOT considered to form part of the public
--   interface of this library.
module Test.DejaFu.STM.Internal

-- | The underlying monad is based on continuations over primitive actions.
type M n r a = Cont (STMAction n r) a

-- | STM transactions are represented as a sequence of primitive actions.
data STMAction n r
SCatch :: (e -> M n r a) -> (M n r a) -> (a -> STMAction n r) -> STMAction n r
SRead :: (TVar r a) -> (a -> STMAction n r) -> STMAction n r
SWrite :: (TVar r a) -> a -> (STMAction n r) -> STMAction n r
SOrElse :: (M n r a) -> (M n r a) -> (a -> STMAction n r) -> STMAction n r
SNew :: String -> a -> (TVar r a -> STMAction n r) -> STMAction n r
SThrow :: e -> STMAction n r
SRetry :: STMAction n r
SStop :: (n ()) -> STMAction n r

-- | A <a>TVar</a> is a tuple of a unique ID and the value contained. The
--   ID is so that blocked transactions can be re-run when a <a>TVar</a>
--   they depend on has changed.
newtype TVar r a
TVar :: (TVarId, r a) -> TVar r a

-- | The result of an STM transaction, along with which <a>TVar</a>s it
--   touched whilst executing.
data Result a

-- | The transaction completed successfully, reading the first list
--   <a>TVar</a>s and writing to the second.
Success :: [TVarId] -> [TVarId] -> a -> Result a

-- | The transaction aborted by calling <tt>retry</tt>, and read the
--   returned <a>TVar</a>s. It should be retried when at least one of the
--   <a>TVar</a>s has been mutated.
Retry :: [TVarId] -> Result a

-- | The transaction aborted by throwing an exception.
Exception :: SomeException -> Result a

-- | This only reduces a <a>SomeException</a> to WHNF.

-- | Check if a <a>Result</a> is a <tt>Success</tt>.
isSTMSuccess :: Result a -> Bool

-- | Run a STM transaction, returning an action to undo its effects.
doTransaction :: MonadRef r n => M n r a -> IdSource -> n (Result a, n (), IdSource, TTrace)

-- | Run a transaction for one step.
stepTrans :: MonadRef r n => STMAction n r -> IdSource -> n (STMAction n r, n (), IdSource, [TVarId], [TVarId], TAction)
instance GHC.Show.Show a => GHC.Show.Show (Test.DejaFu.STM.Internal.Result a)
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Test.DejaFu.STM.Internal.Result a)
instance GHC.Base.Functor Test.DejaFu.STM.Internal.Result
instance Data.Foldable.Foldable Test.DejaFu.STM.Internal.Result


-- | A <tt>MonadSTM</tt> implementation, which can be run on top of
--   <a>IO</a> or <a>ST</a>.
module Test.DejaFu.STM

data STMLike n r a

-- | A <tt>MonadSTM</tt> implementation using <tt>ST</tt>, it encapsulates
--   a single atomic transaction. The environment, that is, the collection
--   of defined <a>TVar</a>s is implicit, there is no list of them, they
--   exist purely as references. This makes the types simpler, but means
--   you can't really get an aggregate of them (if you ever wanted to for
--   some reason).
type STMST t = STMLike (ST t) (STRef t)

-- | A <tt>MonadSTM</tt> implementation using <tt>ST</tt>, it encapsulates
--   a single atomic transaction. The environment, that is, the collection
--   of defined <a>TVar</a>s is implicit, there is no list of them, they
--   exist purely as references. This makes the types simpler, but means
--   you can't really get an aggregate of them (if you ever wanted to for
--   some reason).
type STMIO = STMLike IO IORef

-- | The result of an STM transaction, along with which <a>TVar</a>s it
--   touched whilst executing.
data Result a

-- | The transaction completed successfully, reading the first list
--   <a>TVar</a>s and writing to the second.
Success :: [TVarId] -> [TVarId] -> a -> Result a

-- | The transaction aborted by calling <tt>retry</tt>, and read the
--   returned <a>TVar</a>s. It should be retried when at least one of the
--   <a>TVar</a>s has been mutated.
Retry :: [TVarId] -> Result a

-- | The transaction aborted by throwing an exception.
Exception :: SomeException -> Result a

-- | A trace of an STM transaction is just a list of actions that occurred,
--   as there are no scheduling decisions to make.
type TTrace = [TAction]

-- | All the actions that an STM transaction can perform.
data TAction

-- | Create a new <tt>TVar</tt>
TNew :: TAction

-- | Read from a <tt>TVar</tt>.
TRead :: TVarId -> TAction

-- | Write to a <tt>TVar</tt>.
TWrite :: TVarId -> TAction

-- | Abort and discard effects.
TRetry :: TAction

-- | Execute a transaction until it succeeds (<tt>STMStop</tt>) or aborts
--   (<tt>STMRetry</tt>) and, if it aborts, execute the other transaction.
TOrElse :: TTrace -> (Maybe TTrace) -> TAction

-- | Throw an exception, abort, and discard effects.
TThrow :: TAction

-- | Execute a transaction until it succeeds (<tt>STMStop</tt>) or aborts
--   (<tt>STMThrow</tt>). If the exception is of the appropriate type, it
--   is handled and execution continues; otherwise aborts, propagating the
--   exception upwards.
TCatch :: TTrace -> (Maybe TTrace) -> TAction

-- | Terminate successfully and commit effects.
TStop :: TAction

-- | Every <tt>TVar</tt> has a unique identifier.
data TVarId

-- | Run a transaction, returning the result and new initial <a>TVarId</a>.
--   If the transaction ended by calling <tt>retry</tt>, any <a>TVar</a>
--   modifications are undone.
runTransaction :: MonadRef r n => STMLike n r a -> IdSource -> n (Result a, IdSource, TTrace)
instance GHC.Base.Monad (Test.DejaFu.STM.STMLike n r)
instance GHC.Base.Applicative (Test.DejaFu.STM.STMLike n r)
instance GHC.Base.Functor (Test.DejaFu.STM.STMLike n r)
instance Control.Monad.Catch.MonadThrow (Test.DejaFu.STM.STMLike n r)
instance Control.Monad.Catch.MonadCatch (Test.DejaFu.STM.STMLike n r)
instance GHC.Base.Monad n => Control.Monad.STM.Class.MonadSTM (Test.DejaFu.STM.STMLike n r)


-- | Common types and utility functions for deterministic execution of
--   <tt>MonadConc</tt> implementations. This module is NOT considered to
--   form
module Test.DejaFu.Conc.Internal.Common

-- | The underlying monad is based on continuations over <a>Action</a>s.
--   
--   One might wonder why the return type isn't reflected in <a>Action</a>,
--   and a free monad formulation used. This would remove the need for a
--   <tt>AStop</tt> actions having their parameter. However, this makes the
--   current expression of threads and exception handlers very difficult
--   (perhaps even not possible without significant reworking), so I
--   abandoned the attempt.
newtype M n r a
M :: ((a -> Action n r) -> Action n r) -> M n r a
[runM] :: M n r a -> (a -> Action n r) -> Action n r

-- | The concurrent variable type used with the <tt>Conc</tt> monad. One
--   notable difference between these and <a>MVar</a>s is that <a>MVar</a>s
--   are single-wakeup, and wake up in a FIFO order. Writing to a
--   <tt>MVar</tt> wakes up all threads blocked on reading it, and it is up
--   to the scheduler which one runs next. Taking from a <tt>MVar</tt>
--   behaves analogously.
data MVar r a
MVar :: MVarId -> r (Maybe a) -> MVar r a
[_cvarId] :: MVar r a -> MVarId
[_cvarVal] :: MVar r a -> r (Maybe a)

-- | The mutable non-blocking reference type. These are like
--   <tt>IORef</tt>s.
--   
--   <tt>CRef</tt>s are represented as a unique numeric identifier and a
--   reference containing (a) any thread-local non-synchronised writes (so
--   each thread sees its latest write), (b) a commit count (used in
--   compare-and-swaps), and (c) the current value visible to all threads.
data CRef r a
CRef :: CRefId -> r (Map ThreadId a, Integer, a) -> CRef r a
[_crefId] :: CRef r a -> CRefId
[_crefVal] :: CRef r a -> r (Map ThreadId a, Integer, a)

-- | The compare-and-swap proof type.
--   
--   <tt>Ticket</tt>s are represented as just a wrapper around the
--   identifier of the <a>CRef</a> it came from, the commit count at the
--   time it was produced, and an <tt>a</tt> value. This doesn't work in
--   the source package (atomic-primops) because of the need to use pointer
--   equality. Here we can just pack extra information into <a>CRef</a> to
--   avoid that need.
data Ticket a
Ticket :: CRefId -> Integer -> a -> Ticket a
[_ticketCRef] :: Ticket a -> CRefId
[_ticketWrites] :: Ticket a -> Integer
[_ticketVal] :: Ticket a -> a

-- | Construct a continuation-passing operation from a function.
cont :: ((a -> Action n r) -> Action n r) -> M n r a

-- | Run a CPS computation with the given final computation.
runCont :: M n r a -> (a -> Action n r) -> Action n r

-- | Scheduling is done in terms of a trace of <a>Action</a>s. Blocking can
--   only occur as a result of an action, and they cover (most of) the
--   primitives of the concurrency. <tt>spawn</tt> is absent as it is
--   implemented in terms of <tt>newEmptyMVar</tt>, <tt>fork</tt>, and
--   <tt>putMVar</tt>.
data Action n r
AFork :: String -> ((forall b. M n r b -> M n r b) -> Action n r) -> (ThreadId -> Action n r) -> Action n r
AMyTId :: (ThreadId -> Action n r) -> Action n r
AGetNumCapabilities :: (Int -> Action n r) -> Action n r
ASetNumCapabilities :: Int -> (Action n r) -> Action n r
ANewMVar :: String -> (MVar r a -> Action n r) -> Action n r
APutMVar :: (MVar r a) -> a -> (Action n r) -> Action n r
ATryPutMVar :: (MVar r a) -> a -> (Bool -> Action n r) -> Action n r
AReadMVar :: (MVar r a) -> (a -> Action n r) -> Action n r
ATryReadMVar :: (MVar r a) -> (Maybe a -> Action n r) -> Action n r
ATakeMVar :: (MVar r a) -> (a -> Action n r) -> Action n r
ATryTakeMVar :: (MVar r a) -> (Maybe a -> Action n r) -> Action n r
ANewCRef :: String -> a -> (CRef r a -> Action n r) -> Action n r
AReadCRef :: (CRef r a) -> (a -> Action n r) -> Action n r
AReadCRefCas :: (CRef r a) -> (Ticket a -> Action n r) -> Action n r
AModCRef :: (CRef r a) -> (a -> (a, b)) -> (b -> Action n r) -> Action n r
AModCRefCas :: (CRef r a) -> (a -> (a, b)) -> (b -> Action n r) -> Action n r
AWriteCRef :: (CRef r a) -> a -> (Action n r) -> Action n r
ACasCRef :: (CRef r a) -> (Ticket a) -> a -> ((Bool, Ticket a) -> Action n r) -> Action n r
AThrow :: e -> Action n r
AThrowTo :: ThreadId -> e -> (Action n r) -> Action n r
ACatching :: (e -> M n r a) -> (M n r a) -> (a -> Action n r) -> Action n r
APopCatching :: (Action n r) -> Action n r
AMasking :: MaskingState -> ((forall b. M n r b -> M n r b) -> M n r a) -> (a -> Action n r) -> Action n r
AResetMask :: Bool -> Bool -> MaskingState -> (Action n r) -> Action n r
AAtom :: (STMLike n r a) -> (a -> Action n r) -> Action n r
ALift :: (n (Action n r)) -> Action n r
AYield :: (Action n r) -> Action n r
AReturn :: (Action n r) -> Action n r
ACommit :: ThreadId -> CRefId -> Action n r
AStop :: (n ()) -> Action n r
ASub :: (M n r a) -> (Either Failure a -> Action n r) -> Action n r
AStopSub :: (Action n r) -> Action n r

-- | Look as far ahead in the given continuation as possible.
lookahead :: Action n r -> NonEmpty Lookahead
instance GHC.Base.Functor (Test.DejaFu.Conc.Internal.Common.M n r)
instance GHC.Base.Applicative (Test.DejaFu.Conc.Internal.Common.M n r)
instance GHC.Base.Monad (Test.DejaFu.Conc.Internal.Common.M n r)


-- | Operations and types for threads. This module is NOT considered to
--   form part of the public interface of this library.
module Test.DejaFu.Conc.Internal.Threading

-- | Threads are stored in a map index by <a>ThreadId</a>.
type Threads n r = Map ThreadId (Thread n r)

-- | All the state of a thread.
data Thread n r
Thread :: Action n r -> Maybe BlockedOn -> [Handler n r] -> MaskingState -> Thread n r

-- | The next action to execute.
[_continuation] :: Thread n r -> Action n r

-- | The state of any blocks.
[_blocking] :: Thread n r -> Maybe BlockedOn

-- | Stack of exception handlers
[_handlers] :: Thread n r -> [Handler n r]

-- | The exception masking state.
[_masking] :: Thread n r -> MaskingState

-- | Construct a thread with just one action
mkthread :: Action n r -> Thread n r

-- | A <tt>BlockedOn</tt> is used to determine what sort of variable a
--   thread is blocked on.
data BlockedOn
OnMVarFull :: MVarId -> BlockedOn
OnMVarEmpty :: MVarId -> BlockedOn
OnTVar :: [TVarId] -> BlockedOn
OnMask :: ThreadId -> BlockedOn

-- | Determine if a thread is blocked in a certain way.
(~=) :: Thread n r -> BlockedOn -> Bool

-- | An exception handler.
data Handler n r
Handler :: (e -> Action n r) -> Handler n r

-- | Propagate an exception upwards, finding the closest handler which can
--   deal with it.
propagate :: SomeException -> ThreadId -> Threads n r -> Maybe (Threads n r)

-- | Check if a thread can be interrupted by an exception.
interruptible :: Thread n r -> Bool

-- | Register a new exception handler.
catching :: Exception e => (e -> Action n r) -> ThreadId -> Threads n r -> Threads n r

-- | Remove the most recent exception handler.
uncatching :: ThreadId -> Threads n r -> Threads n r

-- | Raise an exception in a thread.
except :: Action n r -> [Handler n r] -> ThreadId -> Threads n r -> Threads n r

-- | Set the masking state of a thread.
mask :: MaskingState -> ThreadId -> Threads n r -> Threads n r

-- | Replace the <tt>Action</tt> of a thread.
goto :: Action n r -> ThreadId -> Threads n r -> Threads n r

-- | Start a thread with the given ID, inheriting the masking state from
--   the parent thread. This ID must not already be in use!
launch :: ThreadId -> ThreadId -> ((forall b. M n r b -> M n r b) -> Action n r) -> Threads n r -> Threads n r

-- | Start a thread with the given ID and masking state. This must not
--   already be in use!
launch' :: MaskingState -> ThreadId -> ((forall b. M n r b -> M n r b) -> Action n r) -> Threads n r -> Threads n r

-- | Kill a thread.
kill :: ThreadId -> Threads n r -> Threads n r

-- | Block a thread.
block :: BlockedOn -> ThreadId -> Threads n r -> Threads n r

-- | Unblock all threads waiting on the appropriate block. For
--   <tt>TVar</tt> blocks, this will wake all threads waiting on at least
--   one of the given <tt>TVar</tt>s.
wake :: BlockedOn -> Threads n r -> (Threads n r, [ThreadId])
instance GHC.Classes.Eq Test.DejaFu.Conc.Internal.Threading.BlockedOn


-- | Operations over <tt>CRef</tt>s and <tt>MVar</tt>s. This module is NOT
--   considered to form part of the public interface of this library.
--   
--   Relaxed memory operations over <tt>CRef</tt>s are implemented with an
--   explicit write buffer: one per thread for TSO, and one per
--   thread/variable combination for PSO. Unsynchronised writes append to
--   this buffer, and periodically separate threads commit from these
--   buffers to the "actual" <tt>CRef</tt>.
--   
--   This model comes from /Dynamic Partial Order Reduction for Relaxed
--   Memory Models/, N. Zhang, M. Kusano, and C. Wang (2015).
module Test.DejaFu.Conc.Internal.Memory

-- | In non-sequentially-consistent memory models, non-synchronised writes
--   get buffered.
--   
--   The <tt>CRefId</tt> parameter is only used under PSO. Under TSO each
--   thread has a single buffer.
newtype WriteBuffer r
WriteBuffer :: Map (ThreadId, Maybe CRefId) (Seq (BufferedWrite r)) -> WriteBuffer r
[buffer] :: WriteBuffer r -> Map (ThreadId, Maybe CRefId) (Seq (BufferedWrite r))

-- | A buffered write is a reference to the variable, and the value to
--   write. Universally quantified over the value type so that the only
--   thing which can be done with it is to write it to the reference.
data BufferedWrite r
[BufferedWrite] :: ThreadId -> CRef r a -> a -> BufferedWrite r

-- | An empty write buffer.
emptyBuffer :: WriteBuffer r

-- | Add a new write to the end of a buffer.
bufferWrite :: MonadRef r n => WriteBuffer r -> (ThreadId, Maybe CRefId) -> CRef r a -> a -> n (WriteBuffer r)

-- | Commit the write at the head of a buffer.
commitWrite :: MonadRef r n => WriteBuffer r -> (ThreadId, Maybe CRefId) -> n (WriteBuffer r)

-- | Read from a <tt>CRef</tt>, returning a newer thread-local
--   non-committed write if there is one.
readCRef :: MonadRef r n => CRef r a -> ThreadId -> n a

-- | Read from a <tt>CRef</tt>, returning a <tt>Ticket</tt> representing
--   the current view of the thread.
readForTicket :: MonadRef r n => CRef r a -> ThreadId -> n (Ticket a)

-- | Perform a compare-and-swap on a <tt>CRef</tt> if the ticket is still
--   valid. This is strict in the "new" value argument.
casCRef :: MonadRef r n => CRef r a -> ThreadId -> Ticket a -> a -> n (Bool, Ticket a)

-- | Read the local state of a <tt>CRef</tt>.
readCRefPrim :: MonadRef r n => CRef r a -> ThreadId -> n (a, Integer)

-- | Write and commit to a <tt>CRef</tt> immediately, clearing the update
--   map and incrementing the write count.
writeImmediate :: MonadRef r n => CRef r a -> a -> n ()

-- | Flush all writes in the buffer.
writeBarrier :: MonadRef r n => WriteBuffer r -> n ()

-- | Add phantom threads to the thread list to commit pending writes.
addCommitThreads :: WriteBuffer r -> Threads n r -> Threads n r

-- | Remove phantom threads.
delCommitThreads :: Threads n r -> Threads n r

-- | Put into a <tt>MVar</tt>, blocking if full.
putIntoMVar :: MonadRef r n => MVar r a -> a -> Action n r -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])

-- | Try to put into a <tt>MVar</tt>, not blocking if full.
tryPutIntoMVar :: MonadRef r n => MVar r a -> a -> (Bool -> Action n r) -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])

-- | Read from a <tt>MVar</tt>, blocking if empty.
readFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r) -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])

-- | Try to read from a <tt>MVar</tt>, not blocking if empty.
tryReadFromMVar :: MonadRef r n => MVar r a -> (Maybe a -> Action n r) -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])

-- | Take from a <tt>MVar</tt>, blocking if empty.
takeFromMVar :: MonadRef r n => MVar r a -> (a -> Action n r) -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])

-- | Try to take from a <tt>MVar</tt>, not blocking if empty.
tryTakeFromMVar :: MonadRef r n => MVar r a -> (Maybe a -> Action n r) -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])

-- | Mutate a <tt>MVar</tt>, in either a blocking or nonblocking way.
mutMVar :: MonadRef r n => Bool -> MVar r a -> a -> (Bool -> Action n r) -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])

-- | Read a <tt>MVar</tt>, in either a blocking or nonblocking way.
seeMVar :: MonadRef r n => Bool -> Bool -> MVar r a -> (Maybe a -> Action n r) -> ThreadId -> Threads n r -> n (Bool, Threads n r, [ThreadId])


-- | Scheduling for concurrent computations.
module Test.DejaFu.Schedule

-- | A <tt>Scheduler</tt> drives the execution of a concurrent program. The
--   parameters it takes are:
--   
--   <ol>
--   <li>The trace so far.</li>
--   <li>The last thread executed (if this is the first invocation, this is
--   <tt>Nothing</tt>).</li>
--   <li>The runnable threads at this point.</li>
--   <li>The state.</li>
--   </ol>
--   
--   It returns a thread to execute, or <tt>Nothing</tt> if execution
--   should abort here, and also a new state.
type Scheduler state = [(Decision, ThreadAction)] -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> state -> (Maybe ThreadId, state)

-- | Scheduling decisions are based on the state of the running program,
--   and so we can capture some of that state in recording what specific
--   decision we made.
data Decision

-- | Start a new thread, because the last was blocked (or it's the start of
--   computation).
Start :: ThreadId -> Decision

-- | Continue running the last thread for another step.
Continue :: Decision

-- | Pre-empt the running thread, and switch to another.
SwitchTo :: ThreadId -> Decision

-- | Get the resultant thread identifier of a <a>Decision</a>, with a
--   default case for <a>Continue</a>.
tidOf :: ThreadId -> Decision -> ThreadId

-- | Get the <a>Decision</a> that would have resulted in this thread
--   identifier, given a prior thread (if any) and list of runnable
--   threads.
decisionOf :: Foldable f => Maybe ThreadId -> f ThreadId -> ThreadId -> Decision

-- | Non-empty (and non-strict) list type.
data NonEmpty a :: * -> *
(:|) :: a -> [a] -> NonEmpty a

-- | A simple random scheduler which, at every step, picks a random thread
--   to run.
randomSched :: RandomGen g => Scheduler g

-- | A round-robin scheduler which, at every step, schedules the thread
--   with the next <a>ThreadId</a>.
roundRobinSched :: Scheduler ()

-- | A random scheduler which doesn't preempt the running thread. That is,
--   if the last thread scheduled is still runnable, run that, otherwise
--   schedule randomly.
randomSchedNP :: RandomGen g => Scheduler g

-- | A round-robin scheduler which doesn't preempt the running thread.
roundRobinSchedNP :: Scheduler ()

-- | Turn a potentially preemptive scheduler into a non-preemptive one.
makeNonPreemptive :: Scheduler s -> Scheduler s


-- | Concurrent monads with a fixed scheduler: internal types and
--   functions. This module is NOT considered to form part of the public
--   interface of this library.
module Test.DejaFu.Conc.Internal

-- | <a>Trace</a> but as a sequence.
type SeqTrace = Seq (Decision, [(ThreadId, NonEmpty Lookahead)], ThreadAction)

-- | Run a concurrent computation with a given <a>Scheduler</a> and initial
--   state, returning a failure reason on error. Also returned is the final
--   state of the scheduler, and an execution trace.
runConcurrency :: MonadRef r n => Scheduler g -> MemType -> g -> IdSource -> Int -> M n r a -> n (Either Failure a, Context n r g, SeqTrace, Maybe (ThreadId, ThreadAction))

-- | The context a collection of threads are running in.
data Context n r g
Context :: g -> IdSource -> Threads n r -> WriteBuffer r -> Int -> Context n r g
[cSchedState] :: Context n r g -> g
[cIdSource] :: Context n r g -> IdSource
[cThreads] :: Context n r g -> Threads n r
[cWriteBuf] :: Context n r g -> WriteBuffer r
[cCaps] :: Context n r g -> Int

-- | Run a collection of threads, until there are no threads left.
runThreads :: MonadRef r n => Scheduler g -> MemType -> r (Maybe (Either Failure a)) -> Context n r g -> n (Context n r g, SeqTrace, Maybe (ThreadId, ThreadAction))

-- | What a thread did.
data Act

-- | Just one action.
Single :: ThreadAction -> Act

-- | Subconcurrency, with the given trace and final action.
SubC :: SeqTrace -> (Maybe (ThreadId, ThreadAction)) -> Act

-- | Run a single thread one step, by dispatching on the type of
--   <a>Action</a>.
stepThread :: forall n r g. MonadRef r n => Scheduler g -> MemType -> ThreadId -> Action n r -> Context n r g -> n (Either Failure (Context n r g), Act)
instance GHC.Show.Show Test.DejaFu.Conc.Internal.Act
instance GHC.Classes.Eq Test.DejaFu.Conc.Internal.Act


-- | Deterministic traced execution of concurrent computations.
--   
--   This works by executing the computation on a single thread, calling
--   out to the supplied scheduler after each step to determine which
--   thread runs next.
module Test.DejaFu.Conc

data ConcT r n a

-- | A <tt>MonadConc</tt> implementation using <tt>ST</tt>, this should be
--   preferred if you do not need <tt>liftIO</tt>.
type ConcST t = ConcT (STRef t) (ST t)

-- | A <tt>MonadConc</tt> implementation using <tt>IO</tt>.
type ConcIO = ConcT IORef IO

-- | An indication of how a concurrent computation failed.
data Failure

-- | Will be raised if the scheduler does something bad. This should never
--   arise unless you write your own, faulty, scheduler! If it does, please
--   file a bug report.
InternalError :: Failure

-- | The scheduler chose to abort execution. This will be produced if, for
--   example, all possible decisions exceed the specified bounds (there
--   have been too many pre-emptions, the computation has executed for too
--   long, or there have been too many yields).
Abort :: Failure

-- | The computation became blocked indefinitely on <tt>MVar</tt>s.
Deadlock :: Failure

-- | The computation became blocked indefinitely on <tt>TVar</tt>s.
STMDeadlock :: Failure

-- | An uncaught exception bubbled to the top of the computation.
UncaughtException :: Failure

-- | Calls to <tt>subconcurrency</tt> were nested, or attempted when
--   multiple threads existed.
IllegalSubconcurrency :: Failure

-- | The memory model to use for non-synchronised <tt>CRef</tt> operations.
data MemType

-- | The most intuitive model: a program behaves as a simple interleaving
--   of the actions in different threads. When a <tt>CRef</tt> is written
--   to, that write is immediately visible to all threads.
SequentialConsistency :: MemType

-- | 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.
TotalStoreOrder :: MemType

-- | Each <tt>CRef</tt> 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 <tt>CRef</tt>s
--   are not necessarily committed in the same order that they are created.
PartialStoreOrder :: MemType

-- | Run a concurrent computation with a given <a>Scheduler</a> and initial
--   state, returning a failure reason on error. Also returned is the final
--   state of the scheduler, and an execution trace.
--   
--   <b>Warning:</b> Blocking on the action of another thread in
--   <tt>liftIO</tt> cannot be detected! So if you perform some potentially
--   blocking action in a <tt>liftIO</tt> the entire collection of threads
--   may deadlock! You should therefore keep <tt>IO</tt> blocks small, and
--   only perform blocking operations with the supplied primitives, insofar
--   as possible.
--   
--   <b>Note:</b> In order to prevent computation from hanging, the runtime
--   will assume that a deadlock situation has arisen if the scheduler
--   attempts to (a) schedule a blocked thread, or (b) schedule a
--   nonexistent thread. In either of those cases, the computation will be
--   halted.
runConcurrent :: MonadRef r n => Scheduler s -> MemType -> s -> ConcT r n a -> n (Either Failure a, s, Trace)

-- | Run a concurrent computation and return its result.
--   
--   This can only be called in the main thread, when no other threads
--   exist. Calls to <a>subconcurrency</a> cannot be nested. Violating
--   either of these conditions will result in the computation failing with
--   <tt>IllegalSubconcurrency</tt>.
subconcurrency :: ConcT r n a -> ConcT r n (Either Failure a)

-- | One of the outputs of the runner is a <tt>Trace</tt>, which is a log
--   of decisions made, all the runnable threads and what they would do,
--   and the action a thread took in its step.
type Trace = [(Decision, [(ThreadId, NonEmpty Lookahead)], ThreadAction)]

-- | Scheduling decisions are based on the state of the running program,
--   and so we can capture some of that state in recording what specific
--   decision we made.
data Decision

-- | Start a new thread, because the last was blocked (or it's the start of
--   computation).
Start :: ThreadId -> Decision

-- | Continue running the last thread for another step.
Continue :: Decision

-- | Pre-empt the running thread, and switch to another.
SwitchTo :: ThreadId -> Decision

-- | Every live thread has a unique identitifer.
data ThreadId
ThreadId :: (Maybe String) -> Int -> ThreadId

-- | All the actions that a thread can perform.
data ThreadAction

-- | Start a new thread.
Fork :: ThreadId -> ThreadAction

-- | Get the <a>ThreadId</a> of the current thread.
MyThreadId :: ThreadAction

-- | Get the number of Haskell threads that can run simultaneously.
GetNumCapabilities :: Int -> ThreadAction

-- | Set the number of Haskell threads that can run simultaneously.
SetNumCapabilities :: Int -> ThreadAction

-- | Yield the current thread.
Yield :: ThreadAction

-- | Create a new <tt>MVar</tt>.
NewMVar :: MVarId -> ThreadAction

-- | Put into a <tt>MVar</tt>, possibly waking up some threads.
PutMVar :: MVarId -> [ThreadId] -> ThreadAction

-- | Get blocked on a put.
BlockedPutMVar :: MVarId -> ThreadAction

-- | Try to put into a <tt>MVar</tt>, possibly waking up some threads.
TryPutMVar :: MVarId -> Bool -> [ThreadId] -> ThreadAction

-- | Read from a <tt>MVar</tt>.
ReadMVar :: MVarId -> ThreadAction

-- | Try to read from a <tt>MVar</tt>.
TryReadMVar :: MVarId -> Bool -> ThreadAction

-- | Get blocked on a read.
BlockedReadMVar :: MVarId -> ThreadAction

-- | Take from a <tt>MVar</tt>, possibly waking up some threads.
TakeMVar :: MVarId -> [ThreadId] -> ThreadAction

-- | Get blocked on a take.
BlockedTakeMVar :: MVarId -> ThreadAction

-- | Try to take from a <tt>MVar</tt>, possibly waking up some threads.
TryTakeMVar :: MVarId -> Bool -> [ThreadId] -> ThreadAction

-- | Create a new <tt>CRef</tt>.
NewCRef :: CRefId -> ThreadAction

-- | Read from a <tt>CRef</tt>.
ReadCRef :: CRefId -> ThreadAction

-- | Read from a <tt>CRef</tt> for a future compare-and-swap.
ReadCRefCas :: CRefId -> ThreadAction

-- | Modify a <tt>CRef</tt>.
ModCRef :: CRefId -> ThreadAction

-- | Modify a <tt>CRef</tt> using a compare-and-swap.
ModCRefCas :: CRefId -> ThreadAction

-- | Write to a <tt>CRef</tt> without synchronising.
WriteCRef :: CRefId -> ThreadAction

-- | Attempt to to a <tt>CRef</tt> using a compare-and-swap, synchronising
--   it.
CasCRef :: CRefId -> Bool -> ThreadAction

-- | Commit the last write to the given <tt>CRef</tt> by the given thread,
--   so that all threads can see the updated value.
CommitCRef :: ThreadId -> CRefId -> ThreadAction

-- | An STM transaction was executed, possibly waking up some threads.
STM :: TTrace -> [ThreadId] -> ThreadAction

-- | Got blocked in an STM transaction.
BlockedSTM :: TTrace -> ThreadAction

-- | Register a new exception handler
Catching :: ThreadAction

-- | Pop the innermost exception handler from the stack.
PopCatching :: ThreadAction

-- | Throw an exception.
Throw :: ThreadAction

-- | Throw an exception to a thread.
ThrowTo :: ThreadId -> ThreadAction

-- | Get blocked on a <tt>throwTo</tt>.
BlockedThrowTo :: ThreadId -> ThreadAction

-- | Killed by an uncaught exception.
Killed :: ThreadAction

-- | Set the masking state. If <a>True</a>, this is being used to set the
--   masking state to the original state in the argument passed to a
--   <tt>mask</tt>ed function.
SetMasking :: Bool -> MaskingState -> ThreadAction

-- | Return to an earlier masking state. If <a>True</a>, this is being used
--   to return to the state of the masked block in the argument passed to a
--   <tt>mask</tt>ed function.
ResetMasking :: Bool -> MaskingState -> ThreadAction

-- | Lift an IO action. Note that this can only happen with
--   <tt>ConcIO</tt>.
LiftIO :: ThreadAction

-- | A <a>return</a> or <a>pure</a> action was executed.
Return :: ThreadAction

-- | Cease execution and terminate.
Stop :: ThreadAction

-- | Start executing an action with <tt>subconcurrency</tt>.
Subconcurrency :: ThreadAction

-- | Stop executing an action with <tt>subconcurrency</tt>.
StopSubconcurrency :: ThreadAction

-- | A one-step look-ahead at what a thread will do next.
data Lookahead

-- | Will start a new thread.
WillFork :: Lookahead

-- | Will get the <a>ThreadId</a>.
WillMyThreadId :: Lookahead

-- | Will get the number of Haskell threads that can run simultaneously.
WillGetNumCapabilities :: Lookahead

-- | Will set the number of Haskell threads that can run simultaneously.
WillSetNumCapabilities :: Int -> Lookahead

-- | Will yield the current thread.
WillYield :: Lookahead

-- | Will create a new <tt>MVar</tt>.
WillNewMVar :: Lookahead

-- | Will put into a <tt>MVar</tt>, possibly waking up some threads.
WillPutMVar :: MVarId -> Lookahead

-- | Will try to put into a <tt>MVar</tt>, possibly waking up some threads.
WillTryPutMVar :: MVarId -> Lookahead

-- | Will read from a <tt>MVar</tt>.
WillReadMVar :: MVarId -> Lookahead

-- | Will try to read from a <tt>MVar</tt>.
WillTryReadMVar :: MVarId -> Lookahead

-- | Will take from a <tt>MVar</tt>, possibly waking up some threads.
WillTakeMVar :: MVarId -> Lookahead

-- | Will try to take from a <tt>MVar</tt>, possibly waking up some
--   threads.
WillTryTakeMVar :: MVarId -> Lookahead

-- | Will create a new <tt>CRef</tt>.
WillNewCRef :: Lookahead

-- | Will read from a <tt>CRef</tt>.
WillReadCRef :: CRefId -> Lookahead

-- | Will read from a <tt>CRef</tt> for a future compare-and-swap.
WillReadCRefCas :: CRefId -> Lookahead

-- | Will modify a <tt>CRef</tt>.
WillModCRef :: CRefId -> Lookahead

-- | Will modify a <tt>CRef</tt> using a compare-and-swap.
WillModCRefCas :: CRefId -> Lookahead

-- | Will write to a <tt>CRef</tt> without synchronising.
WillWriteCRef :: CRefId -> Lookahead

-- | Will attempt to to a <tt>CRef</tt> using a compare-and-swap,
--   synchronising it.
WillCasCRef :: CRefId -> Lookahead

-- | Will commit the last write by the given thread to the <tt>CRef</tt>.
WillCommitCRef :: ThreadId -> CRefId -> Lookahead

-- | Will execute an STM transaction, possibly waking up some threads.
WillSTM :: Lookahead

-- | Will register a new exception handler
WillCatching :: Lookahead

-- | Will pop the innermost exception handler from the stack.
WillPopCatching :: Lookahead

-- | Will throw an exception.
WillThrow :: Lookahead

-- | Will throw an exception to a thread.
WillThrowTo :: ThreadId -> Lookahead

-- | Will set the masking state. If <a>True</a>, this is being used to set
--   the masking state to the original state in the argument passed to a
--   <tt>mask</tt>ed function.
WillSetMasking :: Bool -> MaskingState -> Lookahead

-- | Will return to an earlier masking state. If <a>True</a>, this is being
--   used to return to the state of the masked block in the argument passed
--   to a <tt>mask</tt>ed function.
WillResetMasking :: Bool -> MaskingState -> Lookahead

-- | Will lift an IO action. Note that this can only happen with
--   <tt>ConcIO</tt>.
WillLiftIO :: Lookahead

-- | Will execute a <a>return</a> or <a>pure</a> action.
WillReturn :: Lookahead

-- | Will cease execution and terminate.
WillStop :: Lookahead

-- | Will execute an action with <tt>subconcurrency</tt>.
WillSubconcurrency :: Lookahead

-- | Will stop executing an extion with <tt>subconcurrency</tt>.
WillStopSubconcurrency :: Lookahead

-- | Every <tt>MVar</tt> has a unique identifier.
data MVarId

-- | Every <tt>CRef</tt> has a unique identifier.
data CRefId

-- | Describes the behaviour of a thread when an asynchronous exception is
--   received.
data MaskingState :: *

-- | asynchronous exceptions are unmasked (the normal state)
Unmasked :: MaskingState

-- | the state during <a>mask</a>: asynchronous exceptions are masked, but
--   blocking operations may still be interrupted
MaskedInterruptible :: MaskingState

-- | the state during <a>uninterruptibleMask</a>: asynchronous exceptions
--   are masked, and blocking operations may not be interrupted
MaskedUninterruptible :: MaskingState

-- | Pretty-print a trace, including a key of the thread IDs (not including
--   thread 0). Each line of the key is indented by two spaces.
showTrace :: Trace -> String

-- | Pretty-print a failure
showFail :: Failure -> String
instance GHC.Base.Monad (Test.DejaFu.Conc.ConcT r n)
instance GHC.Base.Applicative (Test.DejaFu.Conc.ConcT r n)
instance GHC.Base.Functor (Test.DejaFu.Conc.ConcT r n)
instance Control.Monad.IO.Class.MonadIO Test.DejaFu.Conc.ConcIO
instance Control.Monad.Base.MonadBase GHC.Types.IO Test.DejaFu.Conc.ConcIO
instance Control.Monad.Ref.MonadRef (Test.DejaFu.Conc.Internal.Common.CRef r) (Test.DejaFu.Conc.ConcT r n)
instance Control.Monad.Ref.MonadAtomicRef (Test.DejaFu.Conc.Internal.Common.CRef r) (Test.DejaFu.Conc.ConcT r n)
instance Control.Monad.Trans.Class.MonadTrans (Test.DejaFu.Conc.ConcT r)
instance Control.Monad.Catch.MonadCatch (Test.DejaFu.Conc.ConcT r n)
instance Control.Monad.Catch.MonadThrow (Test.DejaFu.Conc.ConcT r n)
instance Control.Monad.Catch.MonadMask (Test.DejaFu.Conc.ConcT r n)
instance GHC.Base.Monad n => Control.Monad.Conc.Class.MonadConc (Test.DejaFu.Conc.ConcT r n)


-- | Internal types and functions for dynamic partial-order reduction. This
--   module is NOT considered to form part of the public interface of this
--   library.
module Test.DejaFu.SCT.Internal

-- | DPOR execution is represented as a tree of states, characterised by
--   the decisions that lead to that state.
data DPOR
DPOR :: Set ThreadId -> Map ThreadId Bool -> Map ThreadId DPOR -> Map ThreadId ThreadAction -> Map ThreadId ThreadAction -> Maybe ThreadAction -> DPOR

-- | What threads are runnable at this step.
[dporRunnable] :: DPOR -> Set ThreadId

-- | Follow-on decisions still to make, and whether that decision was added
--   conservatively due to the bound.
[dporTodo] :: DPOR -> Map ThreadId Bool

-- | Follow-on decisions that have been made.
[dporDone] :: DPOR -> Map ThreadId DPOR

-- | Transitions to ignore (in this node and children) until a dependent
--   transition happens.
[dporSleep] :: DPOR -> Map ThreadId ThreadAction

-- | Transitions which have been taken, excluding conservatively-added
--   ones. This is used in implementing sleep sets.
[dporTaken] :: DPOR -> Map ThreadId ThreadAction

-- | What happened at this step. This will be <a>Nothing</a> at the root,
--   <a>Just</a> everywhere else.
[dporAction] :: DPOR -> Maybe ThreadAction

-- | One step of the execution, including information for backtracking
--   purposes. This backtracking information is used to generate new
--   schedules.
data BacktrackStep
BacktrackStep :: ThreadId -> Decision -> ThreadAction -> Map ThreadId Lookahead -> Map ThreadId Bool -> DepState -> BacktrackStep

-- | The thread running at this step
[bcktThreadid] :: BacktrackStep -> ThreadId

-- | What was decided at this step.
[bcktDecision] :: BacktrackStep -> Decision

-- | What happened at this step.
[bcktAction] :: BacktrackStep -> ThreadAction

-- | The threads runnable at this step
[bcktRunnable] :: BacktrackStep -> Map ThreadId Lookahead

-- | The list of alternative threads to run, and whether those alternatives
--   were added conservatively due to the bound.
[bcktBacktracks] :: BacktrackStep -> Map ThreadId Bool

-- | Some domain-specific state at this point.
[bcktState] :: BacktrackStep -> DepState

-- | Initial DPOR state, given an initial thread ID. This initial thread
--   should exist and be runnable at the start of execution.
initialState :: DPOR

-- | Produce a new schedule prefix from a <tt>DPOR</tt> tree. If there are
--   no new prefixes remaining, return <a>Nothing</a>. Also returns whether
--   the decision was added conservatively, and the sleep set at the point
--   where divergence happens.
--   
--   A schedule prefix is a possibly empty sequence of decisions that have
--   already been made, terminated by a single decision from the to-do set.
--   The intent is to put the system into a new state when executed with
--   this initial sequence of scheduling decisions.
findSchedulePrefix :: DPOR -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)

-- | Add a new trace to the tree, creating a new subtree branching off at
--   the point where the "to-do" decision was made.
incorporateTrace :: MemType -> Bool -> Trace -> DPOR -> DPOR

-- | Produce a list of new backtracking points from an execution trace.
--   These are then used to inform new "to-do" points in the <tt>DPOR</tt>
--   tree.
--   
--   Two traces are passed in to this function: the first is generated from
--   the special DPOR scheduler, the other from the execution of the
--   concurrent program.
--   
--   If the trace ends with any threads other than the initial one still
--   runnable, a dependency is imposed between this final action and
--   everything else.
findBacktrackSteps :: MemType -> BacktrackFunc -> Bool -> Seq (NonEmpty (ThreadId, Lookahead), [ThreadId]) -> Trace -> [BacktrackStep]

-- | Add new backtracking points, if they have not already been visited,
--   fit into the bound, and aren't in the sleep set.
incorporateBacktrackSteps :: ([(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool) -> [BacktrackStep] -> DPOR -> DPOR

-- | The scheduler state
data DPORSchedState
DPORSchedState :: Map ThreadId ThreadAction -> [ThreadId] -> Seq (NonEmpty (ThreadId, Lookahead), [ThreadId]) -> Bool -> Bool -> DepState -> DPORSchedState

-- | The sleep set: decisions not to make until something dependent with
--   them happens.
[schedSleep] :: DPORSchedState -> Map ThreadId ThreadAction

-- | Decisions still to make
[schedPrefix] :: DPORSchedState -> [ThreadId]

-- | Which threads are runnable at each step, and the alternative decisions
--   still to make.
[schedBPoints] :: DPORSchedState -> Seq (NonEmpty (ThreadId, Lookahead), [ThreadId])

-- | Whether to ignore this execution or not: <tt>True</tt> if the
--   execution is aborted due to all possible decisions being in the sleep
--   set, as then everything in this execution is covered by another.
[schedIgnore] :: DPORSchedState -> Bool

-- | Whether the execution was terminated due to all decisions being out of
--   bounds.
[schedBoundKill] :: DPORSchedState -> Bool

-- | State used by the dependency function to determine when to remove
--   decisions from the sleep set.
[schedDepState] :: DPORSchedState -> DepState

-- | Initial DPOR scheduler state for a given prefix
initialDPORSchedState :: Map ThreadId ThreadAction -> [ThreadId] -> DPORSchedState

-- | A bounding function takes the scheduling decisions so far and a
--   decision chosen to come next, and returns if that decision is within
--   the bound.
type BoundFunc = [(Decision, ThreadAction)] -> (Decision, Lookahead) -> Bool

-- | A backtracking step is a point in the execution where another decision
--   needs to be made, in order to explore interesting new schedules. A
--   backtracking <i>function</i> takes the steps identified so far and a
--   list of points and thread at that point to backtrack to. More points
--   be added to compensate for the effects of the bounding function. For
--   example, under pre-emption bounding a conservative backtracking point
--   is added at the prior context switch. The bool is whether the point is
--   conservative. Conservative points are always explored, whereas
--   non-conservative ones might be skipped based on future information.
--   
--   In general, a backtracking function should identify one or more
--   backtracking points, and then use <tt>backtrackAt</tt> to do the
--   actual work.
type BacktrackFunc = [BacktrackStep] -> [(Int, Bool, ThreadId)] -> [BacktrackStep]

-- | Add a backtracking point. If the thread isn't runnable, add all
--   runnable threads. If the backtracking point is already present, don't
--   re-add it UNLESS this would make it conservative.
backtrackAt :: (ThreadId -> BacktrackStep -> Bool) -> BacktrackFunc

-- | DPOR scheduler: takes a list of decisions, and maintains a trace
--   including the runnable threads, and the alternative choices allowed by
--   the bound-specific initialise function.
--   
--   After the initial decisions are exhausted, this prefers choosing the
--   prior thread if it's (1) still runnable and (2) hasn't just yielded.
--   Furthermore, threads which <i>will</i> yield are ignored in preference
--   of those which will not.
dporSched :: MemType -> BoundFunc -> Scheduler DPORSchedState

-- | The scheduler state
data RandSchedState g
RandSchedState :: Map ThreadId Int -> g -> RandSchedState g

-- | The thread weights: used in determining which to run.
[schedWeights] :: RandSchedState g -> Map ThreadId Int

-- | The random number generator.
[schedGen] :: RandSchedState g -> g

-- | Initial weighted random scheduler state.
initialRandSchedState :: Maybe (Map ThreadId Int) -> g -> RandSchedState g

-- | Weighted random scheduler: assigns to each new thread a weight, and
--   makes a weighted random choice out of the runnable threads at every
--   step.
randSched :: RandomGen g => (g -> (Int, g)) -> Scheduler (RandSchedState g)

-- | Check if an action is dependent on another.
dependent :: MemType -> DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool

-- | Variant of <a>dependent</a> to handle <a>Lookahead</a>.
--   
--   Termination of the initial thread is handled specially in the DPOR
--   implementation.
dependent' :: MemType -> DepState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool

-- | Check if two <a>ActionType</a>s are dependent. Note that this is not
--   sufficient to know if two <a>ThreadAction</a>s are dependent, without
--   being so great an over-approximation as to be useless!
dependentActions :: MemType -> DepState -> ActionType -> ActionType -> Bool
data DepState
DepState :: Map CRefId Bool -> Map ThreadId MaskingState -> DepState

-- | Keep track of which <tt>CRef</tt>s have buffered writes.
[depCRState] :: DepState -> Map CRefId Bool

-- | Keep track of thread masking states. If a thread isn't present, the
--   masking state is assumed to be <tt>Unmasked</tt>. This nicely provides
--   compatibility with dpor-0.1, where the thread IDs are not available.
[depMaskState] :: DepState -> Map ThreadId MaskingState

-- | Initial dependency state.
initialDepState :: DepState

-- | Update the <tt>CRef</tt> buffer state with the action that has just
--   happened.
updateDepState :: DepState -> ThreadId -> ThreadAction -> DepState

-- | Update the <tt>CRef</tt> buffer state with the action that has just
--   happened.
updateCRState :: ThreadAction -> Map CRefId Bool -> Map CRefId Bool

-- | Update the thread masking state with the action that has just
--   happened.
updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState

-- | Check if a <tt>CRef</tt> has a buffered write pending.
isBuffered :: DepState -> CRefId -> Bool

-- | Check if an exception can interrupt a thread (action).
canInterrupt :: DepState -> ThreadId -> ThreadAction -> Bool

-- | Check if an exception can interrupt a thread (lookahead).
canInterruptL :: DepState -> ThreadId -> Lookahead -> Bool

-- | Check if a thread is masked interruptible.
isMaskedInterruptible :: DepState -> ThreadId -> Bool

-- | Check if a thread is masked uninterruptible.
isMaskedUninterruptible :: DepState -> ThreadId -> Bool
initialDPORThread :: DPOR -> ThreadId

-- | Check if a thread yielded.
didYield :: ThreadAction -> Bool

-- | Check if a thread will yield.
willYield :: Lookahead -> Bool

-- | Check if an action will kill daemon threads.
killsDaemons :: ThreadId -> Lookahead -> Bool

-- | Internal errors.
err :: String -> String -> a

-- | A combination of <a>partition</a> and <a>concat</a>.
concatPartition :: (a -> Bool) -> [[a]] -> ([a], [a])
instance GHC.Show.Show Test.DejaFu.SCT.Internal.BacktrackStep
instance GHC.Classes.Eq Test.DejaFu.SCT.Internal.BacktrackStep
instance GHC.Show.Show Test.DejaFu.SCT.Internal.DPORSchedState
instance GHC.Classes.Eq Test.DejaFu.SCT.Internal.DPORSchedState
instance GHC.Show.Show Test.DejaFu.SCT.Internal.DepState
instance GHC.Classes.Eq Test.DejaFu.SCT.Internal.DepState
instance GHC.Show.Show g => GHC.Show.Show (Test.DejaFu.SCT.Internal.RandSchedState g)
instance GHC.Classes.Eq g => GHC.Classes.Eq (Test.DejaFu.SCT.Internal.RandSchedState g)
instance GHC.Show.Show Test.DejaFu.SCT.Internal.DPOR
instance GHC.Classes.Eq Test.DejaFu.SCT.Internal.DPOR
instance Control.DeepSeq.NFData Test.DejaFu.SCT.Internal.DPOR
instance Control.DeepSeq.NFData Test.DejaFu.SCT.Internal.BacktrackStep
instance Control.DeepSeq.NFData Test.DejaFu.SCT.Internal.DPORSchedState
instance Control.DeepSeq.NFData g => Control.DeepSeq.NFData (Test.DejaFu.SCT.Internal.RandSchedState g)
instance Control.DeepSeq.NFData Test.DejaFu.SCT.Internal.DepState


-- | Systematic testing for concurrent computations.
module Test.DejaFu.SCT

-- | How to explore the possible executions of a concurrent program.
data Way

-- | Systematically execute a program, trying all distinct executions
--   within the bounds.
--   
--   This corresponds to <a>sctBound</a>.
systematically :: Bounds -> Way

-- | Randomly execute a program, exploring a fixed number of executions.
--   
--   Threads are scheduled by a weighted random selection, where weights
--   are assigned randomly on thread creation.
--   
--   This corresponds to <a>sctWeightedRandom</a> with weight re-use
--   disabled, and is not guaranteed to find all distinct results (unlike
--   <a>systematically</a> / <a>sctBound</a>).
randomly :: RandomGen g => g -> Int -> Way

-- | Randomly execute a program, exploring a fixed number of executions.
--   
--   Threads are scheduled by a uniform random selection.
--   
--   This corresponds to <a>sctUniformRandom</a>, and is not guaranteed to
--   find all distinct results (unlike <a>systematically</a> /
--   <a>sctBound</a>).
uniformly :: RandomGen g => g -> Int -> Way

-- | Randomly execute a program, exploring a fixed number of executions.
--   
--   Threads are scheduled by a weighted random selection, where weights
--   are assigned randomly on thread creation.
--   
--   This corresponds to <a>sctWeightedRandom</a>, and is not guaranteed to
--   find all distinct results (unlike <a>systematically</a> /
--   <a>sctBound</a>).
swarmy :: RandomGen g => g -> Int -> Int -> Way

-- | Explore possible executions of a concurrent program according to the
--   given <a>Way</a>.
runSCT :: MonadRef r n => Way -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)]

-- | A strict variant of <a>runSCT</a>.
--   
--   Demanding the result of this will force it to normal form, which may
--   be more efficient in some situations.
runSCT' :: (MonadRef r n, NFData a) => Way -> MemType -> ConcT r n a -> n [(Either Failure a, Trace)]

-- | Return the set of results of a concurrent program.
resultsSet :: (MonadRef r n, Ord a) => Way -> MemType -> ConcT r n a -> n (Set (Either Failure a))

-- | A strict variant of <a>resultsSet</a>.
--   
--   Demanding the result of this will force it to normal form, which may
--   be more efficient in some situations.
resultsSet' :: (MonadRef r n, Ord a, NFData a) => Way -> MemType -> ConcT r n a -> n (Set (Either Failure a))

data Bounds
Bounds :: Maybe PreemptionBound -> Maybe FairBound -> Maybe LengthBound -> Bounds
[boundPreemp] :: Bounds -> Maybe PreemptionBound
[boundFair] :: Bounds -> Maybe FairBound
[boundLength] :: Bounds -> Maybe LengthBound

-- | No bounds enabled. This forces the scheduler to just use partial-order
--   reduction and sleep sets to prune the search space. This will
--   <i>ONLY</i> work if your computation always terminates!
noBounds :: Bounds

-- | SCT via BPOR.
--   
--   Schedules are generated by running the computation with a
--   deterministic scheduler with some initial list of decisions. At each
--   step of execution, possible-conflicting actions are looked for, if any
--   are found, "backtracking points" are added, to cause the events to
--   happen in a different order in a future execution.
--   
--   Note that unlike with non-bounded partial-order reduction, this may do
--   some redundant work as the introduction of a bound can make previously
--   non-interfering events interfere with each other.
sctBound :: MonadRef r n => MemType -> Bounds -> ConcT r n a -> n [(Either Failure a, Trace)]

newtype PreemptionBound
PreemptionBound :: Int -> PreemptionBound

newtype FairBound
FairBound :: Int -> FairBound

newtype LengthBound
LengthBound :: Int -> LengthBound

-- | SCT via uniform random scheduling.
--   
--   Schedules are generated by assigning to each new thread a random
--   weight. Threads are then scheduled by a weighted random selection.
--   
--   This is not guaranteed to find all distinct results.
sctUniformRandom :: (MonadRef r n, RandomGen g) => MemType -> g -> Int -> ConcT r n a -> n [(Either Failure a, Trace)]

-- | SCT via weighted random scheduling.
--   
--   Schedules are generated by assigning to each new thread a random
--   weight. Threads are then scheduled by a weighted random selection.
--   
--   This is not guaranteed to find all distinct results.
sctWeightedRandom :: (MonadRef r n, RandomGen g) => MemType -> g -> Int -> Int -> ConcT r n a -> n [(Either Failure a, Trace)]
instance GHC.Show.Show Test.DejaFu.SCT.Bounds
instance GHC.Read.Read Test.DejaFu.SCT.Bounds
instance GHC.Classes.Ord Test.DejaFu.SCT.Bounds
instance GHC.Classes.Eq Test.DejaFu.SCT.Bounds
instance GHC.Show.Show Test.DejaFu.SCT.LengthBound
instance GHC.Read.Read Test.DejaFu.SCT.LengthBound
instance GHC.Real.Integral Test.DejaFu.SCT.LengthBound
instance GHC.Real.Real Test.DejaFu.SCT.LengthBound
instance GHC.Num.Num Test.DejaFu.SCT.LengthBound
instance GHC.Classes.Ord Test.DejaFu.SCT.LengthBound
instance GHC.Classes.Eq Test.DejaFu.SCT.LengthBound
instance GHC.Enum.Enum Test.DejaFu.SCT.LengthBound
instance GHC.Show.Show Test.DejaFu.SCT.FairBound
instance GHC.Read.Read Test.DejaFu.SCT.FairBound
instance GHC.Real.Integral Test.DejaFu.SCT.FairBound
instance GHC.Real.Real Test.DejaFu.SCT.FairBound
instance GHC.Num.Num Test.DejaFu.SCT.FairBound
instance GHC.Classes.Ord Test.DejaFu.SCT.FairBound
instance GHC.Classes.Eq Test.DejaFu.SCT.FairBound
instance GHC.Enum.Enum Test.DejaFu.SCT.FairBound
instance GHC.Show.Show Test.DejaFu.SCT.PreemptionBound
instance GHC.Read.Read Test.DejaFu.SCT.PreemptionBound
instance GHC.Real.Integral Test.DejaFu.SCT.PreemptionBound
instance GHC.Real.Real Test.DejaFu.SCT.PreemptionBound
instance GHC.Num.Num Test.DejaFu.SCT.PreemptionBound
instance GHC.Classes.Ord Test.DejaFu.SCT.PreemptionBound
instance GHC.Classes.Eq Test.DejaFu.SCT.PreemptionBound
instance GHC.Enum.Enum Test.DejaFu.SCT.PreemptionBound
instance GHC.Show.Show Test.DejaFu.SCT.Way
instance Control.DeepSeq.NFData Test.DejaFu.SCT.Bounds
instance Control.DeepSeq.NFData Test.DejaFu.SCT.PreemptionBound
instance Control.DeepSeq.NFData Test.DejaFu.SCT.FairBound
instance Control.DeepSeq.NFData Test.DejaFu.SCT.LengthBound


-- | Default parameters for test execution.
module Test.DejaFu.Defaults

-- | A default way to execute concurrent programs: systematically using
--   <a>defaultBounds</a>.
defaultWay :: Way

-- | The default memory model: <tt>TotalStoreOrder</tt>
defaultMemType :: MemType

-- | All bounds enabled, using their default values.
defaultBounds :: Bounds

-- | A sensible default preemption bound: 2.
--   
--   See <i>Concurrency Testing Using Schedule Bounding: an Empirical
--   Study</i>, P. Thomson, A. F. Donaldson, A. Betts for justification.
defaultPreemptionBound :: PreemptionBound

-- | A sensible default fair bound: 5.
--   
--   This comes from playing around myself, but there is probably a better
--   default.
defaultFairBound :: FairBound

-- | A sensible default length bound: 250.
--   
--   Based on the assumption that anything which executes for much longer
--   (or even this long) will take ages to test.
defaultLengthBound :: LengthBound


-- | Properties about the side-effects of concurrent functions on some
--   shared state.
--   
--   Consider this statement about <tt>MVar</tt>s: "using <tt>readMVar</tt>
--   is better than <tt>takeMVar</tt> followed by <tt>putMVar</tt> because
--   the former is atomic but the latter is not."
--   
--   This module can test properties like that:
--   
--   <pre>
--   sig e = Sig
--     { initialise = maybe newEmptyMVar newMVar
--     , observe    = \v _ -&gt; tryReadMVar v
--     , interfere  = \v s -&gt; tryTakeMVar v &gt;&gt; maybe (pure ()) (void . tryPutMVar v) s
--     , expression = e
--     }
--   
--   &gt; check $ sig (void . readMVar) `equivalentTo` sig (\v -&gt; takeMVar v &gt;&gt;= putMVar v)
--   *** Failure: (seed Just ())
--       left:  [(Nothing,Just ())]
--       right: [(Nothing,Just ()),(Just Deadlock,Just ())]
--   </pre>
--   
--   The two expressions are not equivalent, and we get given the
--   counterexample!
--   
--   There are quite a few things going on here, so let's unpack this:
--   
--   <ol>
--   <li>Properties are specified in terms of an <b>initialisation</b>
--   function, an <b>observation</b> function, an <b>interference</b>
--   function, and the expression of interest.</li>
--   <li>The initialisation function (<a>initialise</a>) says how to
--   construct some <b>state</b> value from a <b>seed</b> value, which is
--   supplied by <a>check</a>. In this case the seed is of type <tt>Maybe
--   a</tt> and the state <tt>MVar ConcIO a</tt>.</li>
--   <li>The observation (<a>observe</a>) function says how to take the
--   state and the seed, and produce some value which will be used to
--   compare the expressions. In this case the observation value is of type
--   <tt>Maybe a</tt>.</li>
--   <li>The interference (<a>interfere</a>) function says what sort of
--   concurrent interference can happen. In this case we just try to set
--   the <tt>MVar</tt> to its original value.</li>
--   </ol>
--   
--   The <a>check</a> function takes a property, consisting of two
--   signatures and a way to compare them, evaluates all the results of
--   each signature, and then compares them in the appropriate way.
--   
--   See the sections later in the documentation for what "refinement",
--   "strict refinement", and "equivalence" mean exactly.
module Test.DejaFu.Refinement

-- | A concurrent function and some information about how to execute it and
--   observe its effect.
--   
--   <ul>
--   <li><tt>s</tt> is the state type (<tt>MVar ConcIO a</tt> in the
--   example)</li>
--   <li><tt>o</tt> is the observation type (<tt>Maybe a</tt> in the
--   example)</li>
--   <li><tt>x</tt> is the seed type (<tt>Maybe a</tt> in the example)</li>
--   </ul>
data Sig s o x
Sig :: (x -> ConcIO s) -> (s -> x -> ConcIO o) -> (s -> x -> ConcIO ()) -> (s -> ConcIO ()) -> Sig s o x

-- | Create a new instance of the state variable.
[initialise] :: Sig s o x -> x -> ConcIO s

-- | The observation to make.
[observe] :: Sig s o x -> s -> x -> ConcIO o

-- | Set the state value. This doesn't need to be atomic, or even
--   guaranteed to work, its purpose is to cause interference.
[interfere] :: Sig s o x -> s -> x -> ConcIO ()

-- | The expression to evaluate.
[expression] :: Sig s o x -> s -> ConcIO ()

-- | A property which can be given to <a>check</a>.
data RefinementProperty o x

-- | Indicates that the property is supposed to fail.
expectFailure :: RefinementProperty o x -> RefinementProperty o x

-- | Observational refinement.
--   
--   True iff the result-set of the left expression is a subset (not
--   necessarily proper) of the result-set of the right expression.
--   
--   The two signatures can have different state types, this lets you
--   compare the behaviour of different data structures. The observation
--   and seed types must match, however.
refines :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x

-- | Infix synonym for <a>refines</a>.
--   
--   You might think this should be <tt>=&lt;=</tt>, so it looks kind of
--   like a funny subset operator, with <tt>A =&lt;= B</tt> meaning "the
--   result-set of A is a subset of the result-set of B". Unfortunately you
--   would be wrong. The operator used in the literature for refinement has
--   the open end pointing at the LESS general term and the closed end at
--   the MORE general term. It is read as "is refined by", not "refines".
--   So for consistency with the literature, the open end of
--   <tt>=&gt;=</tt> points at the less general term, and the closed end at
--   the more general term, to give the same argument order as
--   <a>refines</a>.
(=>=) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x

-- | Strict observational refinement.
--   
--   True iff the result-set of the left expression is a proper subset of
--   the result-set of the right expression.
--   
--   The two signatures can have different state types, this lets you
--   compare the behaviour of different data structures. The observation
--   and seed types must match, however.
strictlyRefines :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x

-- | Infix synonym for <a>strictlyRefines</a>
(->-) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x

-- | Observational equivalence.
--   
--   True iff the result-set of the left expression is equal to the
--   result-set of the right expression.
--   
--   The two signatures can have different state types, this lets you
--   compare the behaviour of different data structures. The observation
--   and seed types must match, however.
equivalentTo :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x

-- | Infix synonym for <a>equivalentTo</a>.
(===) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x

-- | A counter example is a seed value and a list of variable assignments.
data FailedProperty o x
CounterExample :: x -> [String] -> Set (Maybe Failure, o) -> Set (Maybe Failure, o) -> FailedProperty o x

-- | The seed for this set of executions.
[failingSeed] :: FailedProperty o x -> x

-- | The values of free variables, as strings.
[failingArgs] :: FailedProperty o x -> [String]

-- | The set of results of the left signature.
[leftResults] :: FailedProperty o x -> Set (Maybe Failure, o)

-- | The set of results of the right signature.
[rightResults] :: FailedProperty o x -> Set (Maybe Failure, o)
NoExpectedFailure :: FailedProperty o x

-- | Things which can be tested.
class Testable a where type O a :: * type X a :: * where {
    type family O a :: *;
    type family X a :: *;
}

-- | Check a refinement property with a variety of seed values and variable
--   assignments.
check :: (Testable p, Listable (X p), Show (X p), Show (O p)) => p -> IO Bool

-- | A version of <a>check</a> that doesn't print, and returns the
--   counterexample.
check' :: (Testable p, Listable (X p)) => p -> IO (Maybe (FailedProperty (O p) (X p)))

-- | Like <a>check</a>, but take a number of cases to try, also returns the
--   counter example found rather than printing it.
--   
--   If multiple counterexamples exist, this will be faster than
--   <tt>listToMaybe</tt> composed with <tt>counterExamples</tt>.
checkFor :: (Testable p, Listable (X p)) => Int -> Int -> p -> IO (Maybe (FailedProperty (O p) (X p)))

-- | Find all counterexamples up to a limit.
counterExamples :: (Testable p, Listable (X p)) => Int -> Int -> p -> IO [FailedProperty (O p) (X p)]

-- | A type is <a>Listable</a> when there exists a function that is able to
--   list (ideally all of) its values.
--   
--   Ideally, instances should be defined by a <a>tiers</a> function that
--   returns a (potentially infinite) list of finite sub-lists (tiers): the
--   first sub-list contains elements of size 0, the second sub-list
--   contains elements of size 1 and so on. Size here is defined by the
--   implementor of the type-class instance.
--   
--   For algebraic data types, the general form for <a>tiers</a> is
--   
--   <pre>
--   tiers = cons&lt;N&gt; ConstructorA
--        \/ cons&lt;N&gt; ConstructorB
--        \/ ...
--        \/ cons&lt;N&gt; ConstructorZ
--   </pre>
--   
--   where <tt>N</tt> is the number of arguments of each constructor
--   <tt>A...Z</tt>.
--   
--   Instances can be alternatively defined by <a>list</a>. In this case,
--   each sub-list in <a>tiers</a> is a singleton list (each succeeding
--   element of <a>list</a> has +1 size).
--   
--   The function <a>deriveListable</a> from <a>Test.LeanCheck.Derive</a>
--   can automatically derive instances of this typeclass.
--   
--   A <a>Listable</a> instance for functions is also available but is not
--   exported by default. Import <a>Test.LeanCheck.Function</a> if you need
--   to test higher-order properties.
class Listable a
tiers :: Listable a => [[a]]
list :: Listable a => [a]
instance (GHC.Show.Show o, GHC.Show.Show x) => GHC.Show.Show (Test.DejaFu.Refinement.FailedProperty o x)
instance GHC.Classes.Eq Test.DejaFu.Refinement.How
instance Test.DejaFu.Refinement.Testable (Test.DejaFu.Refinement.RefinementProperty o x)
instance (Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Test.DejaFu.Refinement.Testable b) => Test.DejaFu.Refinement.Testable (a -> b)


-- | Deterministic testing for concurrent computations.
--   
--   As an example, consider this program, which has two locks and a shared
--   variable. Two threads are spawned, which claim the locks, update the
--   shared variable, and release the locks. The main thread waits for them
--   both to terminate, and returns the final result.
--   
--   <pre>
--   example1 :: MonadConc m =&gt; m Int
--   example1 = do
--     a &lt;- newEmptyMVar
--     b &lt;- newEmptyMVar
--   
--     c &lt;- newMVar 0
--   
--     let lock m = putMVar m ()
--     let unlock = takeMVar
--   
--     j1 &lt;- spawn $ lock a &gt;&gt; lock b &gt;&gt; modifyMVar_ c (return . succ) &gt;&gt; unlock b &gt;&gt; unlock a
--     j2 &lt;- spawn $ lock b &gt;&gt; lock a &gt;&gt; modifyMVar_ c (return . pred) &gt;&gt; unlock a &gt;&gt; unlock b
--   
--     takeMVar j1
--     takeMVar j2
--   
--     takeMVar c
--   </pre>
--   
--   The correct result is 0, as it starts out as 0 and is incremented and
--   decremented by threads 1 and 2, respectively. However, note the order
--   of acquisition of the locks in the two threads. If thread 2 pre-empts
--   thread 1 between the acquisition of the locks (or if thread 1
--   pre-empts thread 2), a deadlock situation will arise, as thread 1 will
--   have lock <tt>a</tt> and be waiting on <tt>b</tt>, and thread 2 will
--   have <tt>b</tt> and be waiting on <tt>a</tt>.
--   
--   Here is what Deja Fu has to say about it:
--   
--   <pre>
--   &gt; autocheck example1
--   [fail] Never Deadlocks (checked: 5)
--           [deadlock] S0------------S1-P2--S1-
--   [pass] No Exceptions (checked: 12)
--   [fail] Consistent Result (checked: 11)
--           0 S0------------S2-----------------S1-----------------S0----
--   
--           [deadlock] S0------------S1-P2--S1-
--   False
--   </pre>
--   
--   It identifies the deadlock, and also the possible results the
--   computation can produce, and displays a simplified trace leading to
--   each failing outcome. The trace contains thread numbers, and the names
--   (which can be set by the programmer) are displayed beneath. It also
--   returns <tt>False</tt> as there are test failures. The automatic
--   testing functionality is good enough if you only want to check your
--   computation is deterministic, but if you have more specific
--   requirements (or have some expected and tolerated level of
--   nondeterminism), you can write tests yourself using the
--   <tt>dejafu*</tt> functions.
--   
--   <b>Warning:</b> If your computation under test does <tt>IO</tt>, the
--   <tt>IO</tt> will be executed lots of times! Be sure that it is
--   deterministic enough not to invalidate your test results. Mocking may
--   be useful where possible.
module Test.DejaFu

-- | Automatically test a computation. In particular, look for deadlocks,
--   uncaught exceptions, and multiple return values.
--   
--   This uses the <tt>Conc</tt> monad for testing, which is an instance of
--   <tt>MonadConc</tt>. If you need to test something which also uses
--   <tt>MonadIO</tt>, use <a>autocheckIO</a>.
autocheck :: (Eq a, Show a) => (forall t. ConcST t a) -> IO Bool

-- | Check a predicate and print the result to stdout, return <a>True</a>
--   if it passes.
dejafu :: Show a => (forall t. ConcST t a) -> (String, Predicate a) -> IO Bool

-- | Variant of <a>dejafu</a> which takes a collection of predicates to
--   test, returning <a>True</a> if all pass.
dejafus :: Show a => (forall t. ConcST t a) -> [(String, Predicate a)] -> IO Bool

-- | Variant of <a>autocheck</a> for computations which do <a>IO</a>.
autocheckIO :: (Eq a, Show a) => ConcIO a -> IO Bool

-- | Variant of <a>dejafu</a> for computations which do <a>IO</a>.
dejafuIO :: Show a => ConcIO a -> (String, Predicate a) -> IO Bool

-- | Variant of <a>dejafus</a> for computations which do <a>IO</a>.
dejafusIO :: Show a => ConcIO a -> [(String, Predicate a)] -> IO Bool

-- | How to explore the possible executions of a concurrent program.
data Way

-- | A default way to execute concurrent programs: systematically using
--   <a>defaultBounds</a>.
defaultWay :: Way

-- | Systematically execute a program, trying all distinct executions
--   within the bounds.
--   
--   This corresponds to <a>sctBound</a>.
systematically :: Bounds -> Way

-- | Randomly execute a program, exploring a fixed number of executions.
--   
--   Threads are scheduled by a weighted random selection, where weights
--   are assigned randomly on thread creation.
--   
--   This corresponds to <a>sctWeightedRandom</a> with weight re-use
--   disabled, and is not guaranteed to find all distinct results (unlike
--   <a>systematically</a> / <a>sctBound</a>).
randomly :: RandomGen g => g -> Int -> Way

-- | Randomly execute a program, exploring a fixed number of executions.
--   
--   Threads are scheduled by a uniform random selection.
--   
--   This corresponds to <a>sctUniformRandom</a>, and is not guaranteed to
--   find all distinct results (unlike <a>systematically</a> /
--   <a>sctBound</a>).
uniformly :: RandomGen g => g -> Int -> Way

-- | Randomly execute a program, exploring a fixed number of executions.
--   
--   Threads are scheduled by a weighted random selection, where weights
--   are assigned randomly on thread creation.
--   
--   This corresponds to <a>sctWeightedRandom</a>, and is not guaranteed to
--   find all distinct results (unlike <a>systematically</a> /
--   <a>sctBound</a>).
swarmy :: RandomGen g => g -> Int -> Int -> Way

-- | Variant of <a>autocheck</a> which takes a way to run the program and a
--   memory model.
--   
--   Schedule bounding is used to filter the large number of possible
--   schedules, and can be iteratively increased for further coverage
--   guarantees. Empirical studies (/Concurrency Testing Using Schedule
--   Bounding: an Empirical Study/, P. Thompson, A. Donaldson, and A.
--   Betts) have found that many concurrency bugs can be exhibited with as
--   few as two threads and two pre-emptions, which is part of what
--   <a>dejafus</a> uses.
--   
--   <b>Warning:</b> Using largers bounds will almost certainly
--   significantly increase the time taken to test!
autocheckWay :: (Eq a, Show a) => Way -> MemType -> (forall t. ConcST t a) -> IO Bool

-- | Variant of <a>autocheckWay</a> for computations which do <a>IO</a>.
autocheckWayIO :: (Eq a, Show a) => Way -> MemType -> ConcIO a -> IO Bool

-- | Variant of <a>dejafu</a> which takes a way to run the program and a
--   memory model.
dejafuWay :: Show a => Way -> MemType -> (forall t. ConcST t a) -> (String, Predicate a) -> IO Bool

-- | Variant of <a>dejafuWay</a> for computations which do <a>IO</a>.
dejafuWayIO :: Show a => Way -> MemType -> ConcIO a -> (String, Predicate a) -> IO Bool

-- | Variant of <a>dejafus</a> which takes a way to run the program and a
--   memory model.
dejafusWay :: Show a => Way -> MemType -> (forall t. ConcST t a) -> [(String, Predicate a)] -> IO Bool

-- | Variant of <a>dejafusWay</a> for computations which do <a>IO</a>.
dejafusWayIO :: Show a => Way -> MemType -> ConcIO a -> [(String, Predicate a)] -> IO Bool

-- | The memory model to use for non-synchronised <tt>CRef</tt> operations.
data MemType

-- | The most intuitive model: a program behaves as a simple interleaving
--   of the actions in different threads. When a <tt>CRef</tt> is written
--   to, that write is immediately visible to all threads.
SequentialConsistency :: MemType

-- | 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.
TotalStoreOrder :: MemType

-- | Each <tt>CRef</tt> 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 <tt>CRef</tt>s
--   are not necessarily committed in the same order that they are created.
PartialStoreOrder :: MemType

-- | The default memory model: <tt>TotalStoreOrder</tt>
defaultMemType :: MemType

data Bounds
Bounds :: Maybe PreemptionBound -> Maybe FairBound -> Maybe LengthBound -> Bounds
[boundPreemp] :: Bounds -> Maybe PreemptionBound
[boundFair] :: Bounds -> Maybe FairBound
[boundLength] :: Bounds -> Maybe LengthBound

-- | All bounds enabled, using their default values.
defaultBounds :: Bounds

-- | No bounds enabled. This forces the scheduler to just use partial-order
--   reduction and sleep sets to prune the search space. This will
--   <i>ONLY</i> work if your computation always terminates!
noBounds :: Bounds

newtype PreemptionBound
PreemptionBound :: Int -> PreemptionBound

-- | A sensible default preemption bound: 2.
--   
--   See <i>Concurrency Testing Using Schedule Bounding: an Empirical
--   Study</i>, P. Thomson, A. F. Donaldson, A. Betts for justification.
defaultPreemptionBound :: PreemptionBound

newtype FairBound
FairBound :: Int -> FairBound

-- | A sensible default fair bound: 5.
--   
--   This comes from playing around myself, but there is probably a better
--   default.
defaultFairBound :: FairBound

newtype LengthBound
LengthBound :: Int -> LengthBound

-- | A sensible default length bound: 250.
--   
--   Based on the assumption that anything which executes for much longer
--   (or even this long) will take ages to test.
defaultLengthBound :: LengthBound

-- | The results of a test, including the number of cases checked to
--   determine the final boolean outcome.
data Result a
Result :: Bool -> Int -> [(Either Failure a, Trace)] -> String -> Result a

-- | Whether the test passed or not.
[_pass] :: Result a -> Bool

-- | The number of cases checked.
[_casesChecked] :: Result a -> Int

-- | The failing cases, if any.
[_failures] :: Result a -> [(Either Failure a, Trace)]

-- | A message to display on failure, if nonempty
[_failureMsg] :: Result a -> String

-- | An indication of how a concurrent computation failed.
data Failure

-- | Will be raised if the scheduler does something bad. This should never
--   arise unless you write your own, faulty, scheduler! If it does, please
--   file a bug report.
InternalError :: Failure

-- | The scheduler chose to abort execution. This will be produced if, for
--   example, all possible decisions exceed the specified bounds (there
--   have been too many pre-emptions, the computation has executed for too
--   long, or there have been too many yields).
Abort :: Failure

-- | The computation became blocked indefinitely on <tt>MVar</tt>s.
Deadlock :: Failure

-- | The computation became blocked indefinitely on <tt>TVar</tt>s.
STMDeadlock :: Failure

-- | An uncaught exception bubbled to the top of the computation.
UncaughtException :: Failure

-- | Calls to <tt>subconcurrency</tt> were nested, or attempted when
--   multiple threads existed.
IllegalSubconcurrency :: Failure

-- | Run a predicate over all executions within the default schedule
--   bounds.
runTest :: Predicate a -> (forall t. ConcST t a) -> Result a

-- | Variant of <a>runTest</a> which takes a way to run the program and a
--   memory model.
runTestWay :: Way -> MemType -> Predicate a -> (forall t. ConcST t a) -> Result a

-- | Monad-polymorphic variant of <a>runTest</a>.
runTestM :: MonadRef r n => Predicate a -> ConcT r n a -> n (Result a)

-- | Monad-polymorphic variant of <tt>runTest'</tt>.
runTestWayM :: MonadRef r n => Way -> MemType -> Predicate a -> ConcT r n a -> n (Result a)

-- | A <tt>Predicate</tt> is a function which collapses a list of results
--   into a <a>Result</a>.
type Predicate a = [(Either Failure a, Trace)] -> Result a

-- | Reduce the list of failures in a <tt>Predicate</tt> 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.
representative :: Eq a => Predicate a -> Predicate a

-- | Check that a computation never aborts.
abortsNever :: Predicate a

-- | Check that a computation always aborts.
abortsAlways :: Predicate a

-- | Check that a computation aborts at least once.
abortsSometimes :: Predicate a

-- | Check that a computation never deadlocks.
deadlocksNever :: Predicate a

-- | Check that a computation always deadlocks.
deadlocksAlways :: Predicate a

-- | Check that a computation deadlocks at least once.
deadlocksSometimes :: Predicate a

-- | Check that a computation never fails with an uncaught exception.
exceptionsNever :: Predicate a

-- | Check that a computation always fails with an uncaught exception.
exceptionsAlways :: Predicate a

-- | Check that a computation fails with an uncaught exception at least
--   once.
exceptionsSometimes :: Predicate a

-- | Check that the result of a computation is always the same. In
--   particular this means either: (a) it always fails in the same way, or
--   (b) it never fails and the values returned are all equal.
alwaysSame :: Eq a => Predicate a

-- | Check that the result of a computation is not always the same.
notAlwaysSame :: Eq a => Predicate a

-- | Check that the result of a unary boolean predicate is always true.
alwaysTrue :: (Either Failure a -> Bool) -> Predicate a

-- | Check that the result of a binary boolean predicate is true between
--   all pairs of results. Only properties which are transitive and
--   symmetric should be used here.
--   
--   If the predicate fails, <i>both</i> (result,trace) tuples will be
--   added to the failures list.
alwaysTrue2 :: (Either Failure a -> Either Failure a -> Bool) -> Predicate a

-- | Check that the result of a unary boolean predicate is true at least
--   once.
somewhereTrue :: (Either Failure a -> Bool) -> Predicate a

-- | Predicate for when there is a known set of results where every result
--   must be exhibited at least once.
gives :: (Eq a, Show a) => [Either Failure a] -> Predicate a

-- | Variant of <a>gives</a> that doesn't allow for expected failures.
gives' :: (Eq a, Show a) => [a] -> Predicate a
instance GHC.Show.Show a => GHC.Show.Show (Test.DejaFu.Result a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.DejaFu.Result a)
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Test.DejaFu.Result a)
instance GHC.Base.Functor Test.DejaFu.Result
instance Data.Foldable.Foldable Test.DejaFu.Result
