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


-- | A library for unit-testing concurrent programs.
--   
--   <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
--   
--   This package builds on the
--   [concurrency](https:/<i>hackage.haskell.org</i>package/concurrency)
--   package by enabling you to deterministically test your concurrent
--   programs.
--   
--   See the <a>website</a> or README for more.
@package dejafu
@version 1.11.0.2


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

-- | Every thread has a unique identitifer.
newtype ThreadId
ThreadId :: Id -> ThreadId

-- | Every <tt>IORef</tt> has a unique identifier.
newtype IORefId
IORefId :: Id -> IORefId

-- | Every <tt>MVar</tt> has a unique identifier.
newtype MVarId
MVarId :: Id -> MVarId

-- | Every <tt>TVar</tt> has a unique identifier.
newtype TVarId
TVarId :: Id -> TVarId

-- | An identifier for a thread, <tt>MVar</tt>, <tt>IORef</tt>, or
--   <tt>TVar</tt>.
--   
--   The number is the important bit. The string is to make execution
--   traces easier to read, but is meaningless.
data Id
Id :: (Maybe String) -> {-# UNPACK #-} !Int -> Id

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

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

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

-- | Start a new bound thread.
ForkOS :: ThreadId -> ThreadAction

-- | Check if the current thread is bound.
IsCurrentThreadBound :: Bool -> 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

-- | Yield/delay the current thread.
ThreadDelay :: Int -> 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>IORef</tt>.
NewIORef :: IORefId -> ThreadAction

-- | Read from a <tt>IORef</tt>.
ReadIORef :: IORefId -> ThreadAction

-- | Read from a <tt>IORef</tt> for a future compare-and-swap.
ReadIORefCas :: IORefId -> ThreadAction

-- | Modify a <tt>IORef</tt>.
ModIORef :: IORefId -> ThreadAction

-- | Modify a <tt>IORef</tt> using a compare-and-swap.
ModIORefCas :: IORefId -> ThreadAction

-- | Write to a <tt>IORef</tt> without synchronising.
WriteIORef :: IORefId -> ThreadAction

-- | Attempt to to a <tt>IORef</tt> using a compare-and-swap, synchronising
--   it.
CasIORef :: IORefId -> Bool -> ThreadAction

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

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

-- | Got blocked in an STM transaction.
BlockedSTM :: [TAction] -> ThreadAction

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

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

-- | Throw an exception. If the <a>Bool</a> is <tt>True</tt>, then this
--   killed the thread.
Throw :: Bool -> ThreadAction

-- | Throw an exception to a thread. If the <a>Bool</a> is <tt>True</tt>,
--   then this killed the thread.
ThrowTo :: ThreadId -> Bool -> ThreadAction

-- | Get blocked on a <tt>throwTo</tt>.
BlockedThrowTo :: ThreadId -> 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

-- | Execute an action with <tt>dontCheck</tt>.
DontCheck :: Trace -> ThreadAction

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

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

-- | Will start a new bound thread.
WillForkOS :: Lookahead

-- | Will check if the current thread is bound.
WillIsCurrentThreadBound :: 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 yield/delay the current thread.
WillThreadDelay :: Int -> 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>IORef</tt>.
WillNewIORef :: Lookahead

-- | Will read from a <tt>IORef</tt>.
WillReadIORef :: IORefId -> Lookahead

-- | Will read from a <tt>IORef</tt> for a future compare-and-swap.
WillReadIORefCas :: IORefId -> Lookahead

-- | Will modify a <tt>IORef</tt>.
WillModIORef :: IORefId -> Lookahead

-- | Will modify a <tt>IORef</tt> using a compare-and-swap.
WillModIORefCas :: IORefId -> Lookahead

-- | Will write to a <tt>IORef</tt> without synchronising.
WillWriteIORef :: IORefId -> Lookahead

-- | Will attempt to to a <tt>IORef</tt> using a compare-and-swap,
--   synchronising it.
WillCasIORef :: IORefId -> Lookahead

-- | Will commit the last write by the given thread to the <tt>IORef</tt>.
WillCommitIORef :: ThreadId -> IORefId -> 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

-- | Will execute an action with <tt>dontCheck</tt>.
WillDontCheck :: Lookahead

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

-- | Create a new <tt>TVar</tt>
TNew :: TVarId -> 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. If the transaction aborts by calling
--   <tt>retry</tt>, execute the other transaction.
TOrElse :: [TAction] -> (Maybe [TAction]) -> TAction

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

-- | Execute a transaction. If the transaction aborts by throwing an
--   exception of the appropriate type, it is handled and execution
--   continues; otherwise aborts, propagating the exception upwards.
TCatch :: [TAction] -> (Maybe [TAction]) -> 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 alternative unblocked threads and what they
--   would do, and the action a thread took in its step.
type Trace = [(Decision, [(ThreadId, 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

-- | An indication of how a concurrent computation failed.
--   
--   The <tt>Eq</tt>, <tt>Ord</tt>, and <tt>NFData</tt> instances
--   compare/evaluate the exception with <tt>show</tt> in the
--   <tt>UncaughtException</tt> case.
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

-- | Every thread is blocked, and the main thread is <i>not</i> blocked in
--   an STM transaction.
Deadlock :: Failure

-- | Every thread is blocked, and the main thread is blocked in an STM
--   transaction.
STMDeadlock :: Failure

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

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

-- | A call to <tt>dontCheck</tt> was attempted after the first action of
--   the initial thread.
IllegalDontCheck :: Failure

-- | Check if a failure is an <tt>InternalError</tt>.
isInternalError :: Failure -> Bool

-- | Check if a failure is an <tt>Abort</tt>.
isAbort :: Failure -> Bool

-- | Check if a failure is a <tt>Deadlock</tt> or an <tt>STMDeadlock</tt>.
isDeadlock :: Failure -> Bool

-- | Check if a failure is an <tt>UncaughtException</tt>
isUncaughtException :: Failure -> Bool

-- | Check if a failure is an <tt>IllegalSubconcurrency</tt>
isIllegalSubconcurrency :: Failure -> Bool

-- | Check if a failure is an <tt>IllegalDontCheck</tt>
isIllegalDontCheck :: Failure -> Bool

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

-- | Restrict the number of pre-emptive context switches allowed in an
--   execution.
--   
--   A pre-emption bound of zero disables pre-emptions entirely.
newtype PreemptionBound
PreemptionBound :: Int -> PreemptionBound

-- | Restrict the maximum difference between the number of yield or delay
--   operations different threads have performed.
--   
--   A fair bound of zero disables yields and delays entirely.
newtype FairBound
FairBound :: Int -> FairBound

-- | Restrict the maximum length (in terms of primitive actions) of an
--   execution.
--   
--   A length bound of zero immediately aborts the execution.
newtype LengthBound
LengthBound :: Int -> LengthBound

-- | An <tt>Either Failure a -&gt; Maybe Discard</tt> value can be used to
--   selectively discard results.
data Discard

-- | Discard the trace but keep the result. The result will appear to have
--   an empty trace.
DiscardTrace :: Discard

-- | Discard the result and the trace. It will simply not be reported as a
--   possible behaviour of the program.
DiscardResultAndTrace :: Discard

-- | A monoid for discard functions: combines two functions, keeping the
--   weaker.
--   
--   <tt>Nothing</tt> is weaker than <tt>Just DiscardTrace</tt>, which is
--   weaker than <tt>Just DiscardResultAndTrace</tt>. This forms a
--   commutative monoid where the unit is <tt>const (Just
--   DiscardResultAndTrace)</tt>.
newtype Weaken a
Weaken :: Either Failure a -> Maybe Discard -> Weaken a
[getWeakDiscarder] :: Weaken a -> Either Failure a -> Maybe Discard

-- | Combine two discard functions, keeping the weaker.
weakenDiscard :: (Either Failure a -> Maybe Discard) -> (Either Failure a -> Maybe Discard) -> Either Failure a -> Maybe Discard

-- | A monoid for discard functions: combines two functions, keeping the
--   stronger.
--   
--   <tt>Just DiscardResultAndTrace</tt> is stronger than <tt>Just
--   DiscardTrace</tt>, which is stronger than <tt>Nothing</tt>. This forms
--   a commutative monoid where the unit is <tt>const Nothing</tt>.
newtype Strengthen a
Strengthen :: Either Failure a -> Maybe Discard -> Strengthen a
[getStrongDiscarder] :: Strengthen a -> Either Failure a -> Maybe Discard

-- | Combine two discard functions, keeping the stronger.
strengthenDiscard :: (Either Failure a -> Maybe Discard) -> (Either Failure a -> Maybe Discard) -> Either Failure a -> Maybe Discard

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

-- | The most intuitive model: a program behaves as a simple interleaving
--   of the actions in different threads. When a <tt>IORef</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>IORef</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>IORef</tt>s
--   are not necessarily committed in the same order that they are created.
PartialStoreOrder :: MemType

-- | An exception for errors in testing caused by use of <a>fail</a>.
newtype MonadFailException
MonadFailException :: String -> MonadFailException
instance GHC.Show.Show Test.DejaFu.Types.MonadFailException
instance GHC.Enum.Bounded Test.DejaFu.Types.MemType
instance GHC.Enum.Enum Test.DejaFu.Types.MemType
instance GHC.Classes.Ord Test.DejaFu.Types.MemType
instance GHC.Read.Read Test.DejaFu.Types.MemType
instance GHC.Show.Show Test.DejaFu.Types.MemType
instance GHC.Classes.Eq Test.DejaFu.Types.MemType
instance GHC.Enum.Bounded Test.DejaFu.Types.Discard
instance GHC.Enum.Enum Test.DejaFu.Types.Discard
instance GHC.Classes.Ord Test.DejaFu.Types.Discard
instance GHC.Read.Read Test.DejaFu.Types.Discard
instance GHC.Show.Show Test.DejaFu.Types.Discard
instance GHC.Classes.Eq Test.DejaFu.Types.Discard
instance GHC.Show.Show Test.DejaFu.Types.Bounds
instance GHC.Read.Read Test.DejaFu.Types.Bounds
instance GHC.Classes.Ord Test.DejaFu.Types.Bounds
instance GHC.Classes.Eq Test.DejaFu.Types.Bounds
instance GHC.Show.Show Test.DejaFu.Types.LengthBound
instance GHC.Read.Read Test.DejaFu.Types.LengthBound
instance GHC.Real.Integral Test.DejaFu.Types.LengthBound
instance GHC.Real.Real Test.DejaFu.Types.LengthBound
instance GHC.Num.Num Test.DejaFu.Types.LengthBound
instance GHC.Classes.Ord Test.DejaFu.Types.LengthBound
instance GHC.Classes.Eq Test.DejaFu.Types.LengthBound
instance GHC.Enum.Enum Test.DejaFu.Types.LengthBound
instance GHC.Show.Show Test.DejaFu.Types.FairBound
instance GHC.Read.Read Test.DejaFu.Types.FairBound
instance GHC.Real.Integral Test.DejaFu.Types.FairBound
instance GHC.Real.Real Test.DejaFu.Types.FairBound
instance GHC.Num.Num Test.DejaFu.Types.FairBound
instance GHC.Classes.Ord Test.DejaFu.Types.FairBound
instance GHC.Classes.Eq Test.DejaFu.Types.FairBound
instance GHC.Enum.Enum Test.DejaFu.Types.FairBound
instance GHC.Show.Show Test.DejaFu.Types.PreemptionBound
instance GHC.Read.Read Test.DejaFu.Types.PreemptionBound
instance GHC.Real.Integral Test.DejaFu.Types.PreemptionBound
instance GHC.Real.Real Test.DejaFu.Types.PreemptionBound
instance GHC.Num.Num Test.DejaFu.Types.PreemptionBound
instance GHC.Classes.Ord Test.DejaFu.Types.PreemptionBound
instance GHC.Classes.Eq Test.DejaFu.Types.PreemptionBound
instance GHC.Enum.Enum Test.DejaFu.Types.PreemptionBound
instance GHC.Show.Show Test.DejaFu.Types.Failure
instance GHC.Show.Show Test.DejaFu.Types.ThreadAction
instance GHC.Generics.Generic Test.DejaFu.Types.ThreadAction
instance GHC.Classes.Eq Test.DejaFu.Types.ThreadAction
instance GHC.Show.Show Test.DejaFu.Types.Decision
instance GHC.Classes.Eq Test.DejaFu.Types.Decision
instance GHC.Show.Show Test.DejaFu.Types.TAction
instance GHC.Classes.Eq Test.DejaFu.Types.TAction
instance GHC.Show.Show Test.DejaFu.Types.Lookahead
instance GHC.Generics.Generic Test.DejaFu.Types.Lookahead
instance GHC.Classes.Eq Test.DejaFu.Types.Lookahead
instance Control.DeepSeq.NFData Test.DejaFu.Types.ThreadId
instance GHC.Classes.Ord Test.DejaFu.Types.ThreadId
instance GHC.Classes.Eq Test.DejaFu.Types.ThreadId
instance GHC.Generics.Generic Test.DejaFu.Types.IORefId
instance Control.DeepSeq.NFData Test.DejaFu.Types.IORefId
instance GHC.Classes.Ord Test.DejaFu.Types.IORefId
instance GHC.Classes.Eq Test.DejaFu.Types.IORefId
instance Control.DeepSeq.NFData Test.DejaFu.Types.MVarId
instance GHC.Classes.Ord Test.DejaFu.Types.MVarId
instance GHC.Classes.Eq Test.DejaFu.Types.MVarId
instance Control.DeepSeq.NFData Test.DejaFu.Types.TVarId
instance GHC.Classes.Ord Test.DejaFu.Types.TVarId
instance GHC.Classes.Eq Test.DejaFu.Types.TVarId
instance GHC.Generics.Generic Test.DejaFu.Types.ThreadId
instance GHC.Generics.Generic Test.DejaFu.Types.MVarId
instance GHC.Generics.Generic Test.DejaFu.Types.TVarId
instance GHC.Generics.Generic Test.DejaFu.Types.Id
instance GHC.Generics.Generic Test.DejaFu.Types.TAction
instance GHC.Generics.Generic Test.DejaFu.Types.Decision
instance GHC.Generics.Generic Test.DejaFu.Types.Failure
instance GHC.Generics.Generic Test.DejaFu.Types.Bounds
instance GHC.Generics.Generic Test.DejaFu.Types.PreemptionBound
instance GHC.Generics.Generic Test.DejaFu.Types.FairBound
instance GHC.Generics.Generic Test.DejaFu.Types.LengthBound
instance GHC.Generics.Generic Test.DejaFu.Types.Discard
instance GHC.Generics.Generic Test.DejaFu.Types.MemType
instance GHC.Generics.Generic Test.DejaFu.Types.MonadFailException
instance GHC.Exception.Exception Test.DejaFu.Types.MonadFailException
instance Control.DeepSeq.NFData Test.DejaFu.Types.MonadFailException
instance Control.DeepSeq.NFData Test.DejaFu.Types.MemType
instance GHC.Base.Semigroup (Test.DejaFu.Types.Strengthen a)
instance GHC.Base.Monoid (Test.DejaFu.Types.Strengthen a)
instance Data.Functor.Contravariant.Contravariant Test.DejaFu.Types.Strengthen
instance Data.Functor.Contravariant.Divisible.Divisible Test.DejaFu.Types.Strengthen
instance GHC.Base.Semigroup (Test.DejaFu.Types.Weaken a)
instance GHC.Base.Monoid (Test.DejaFu.Types.Weaken a)
instance Data.Functor.Contravariant.Contravariant Test.DejaFu.Types.Weaken
instance Data.Functor.Contravariant.Divisible.Divisible Test.DejaFu.Types.Weaken
instance Control.DeepSeq.NFData Test.DejaFu.Types.Discard
instance Control.DeepSeq.NFData Test.DejaFu.Types.Bounds
instance Control.DeepSeq.NFData Test.DejaFu.Types.LengthBound
instance Control.DeepSeq.NFData Test.DejaFu.Types.FairBound
instance Control.DeepSeq.NFData Test.DejaFu.Types.PreemptionBound
instance GHC.Classes.Eq Test.DejaFu.Types.Failure
instance GHC.Classes.Ord Test.DejaFu.Types.Failure
instance Control.DeepSeq.NFData Test.DejaFu.Types.Failure
instance Control.DeepSeq.NFData Test.DejaFu.Types.ThreadAction
instance Control.DeepSeq.NFData Test.DejaFu.Types.Decision
instance Control.DeepSeq.NFData Test.DejaFu.Types.TAction
instance Control.DeepSeq.NFData Test.DejaFu.Types.Lookahead
instance GHC.Show.Show Test.DejaFu.Types.ThreadId
instance GHC.Show.Show Test.DejaFu.Types.IORefId
instance GHC.Show.Show Test.DejaFu.Types.MVarId
instance GHC.Show.Show Test.DejaFu.Types.TVarId
instance GHC.Classes.Eq Test.DejaFu.Types.Id
instance GHC.Classes.Ord Test.DejaFu.Types.Id
instance GHC.Show.Show Test.DejaFu.Types.Id
instance Control.DeepSeq.NFData Test.DejaFu.Types.Id


-- | Internal types and functions used throughout DejaFu. This module is
--   NOT considered to form part of the public interface of this library.
module Test.DejaFu.Internal

-- | SCT configuration record.
data Settings n a
Settings :: Way -> MemType -> Maybe (Either Failure a -> Maybe Discard) -> Maybe (a -> String) -> Maybe (String -> n ()) -> Bool -> Maybe (Either Failure a -> Bool) -> Maybe (a -> a -> Bool) -> Bool -> Bool -> Settings n a
[_way] :: Settings n a -> Way
[_memtype] :: Settings n a -> MemType
[_discard] :: Settings n a -> Maybe (Either Failure a -> Maybe Discard)
[_debugShow] :: Settings n a -> Maybe (a -> String)
[_debugPrint] :: Settings n a -> Maybe (String -> n ())
[_debugFatal] :: Settings n a -> Bool
[_earlyExit] :: Settings n a -> Maybe (Either Failure a -> Bool)
[_equality] :: Settings n a -> Maybe (a -> a -> Bool)
[_simplify] :: Settings n a -> Bool
[_safeIO] :: Settings n a -> Bool

-- | How to explore the possible executions of a concurrent program.
data Way
[Systematic] :: Bounds -> Way
[Randomly] :: RandomGen g => (g -> (Int, g)) -> g -> Int -> Way

-- | The number of ID parameters was getting a bit unwieldy, so this hides
--   them all away.
data IdSource
IdSource :: (Int, [String]) -> (Int, [String]) -> (Int, [String]) -> (Int, [String]) -> IdSource
[_iorids] :: IdSource -> (Int, [String])
[_mvids] :: IdSource -> (Int, [String])
[_tvids] :: IdSource -> (Int, [String])
[_tids] :: IdSource -> (Int, [String])

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

-- | 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)

-- | Helper for <tt>next*</tt>
nextId :: String -> (Int, [String]) -> (Id, (Int, [String]))

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

-- | 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

-- | Get the <tt>TVar</tt>s a transaction wrote to (or would have, if it
--   didn't <tt>retry</tt>).
tvarsWritten :: ThreadAction -> Set TVarId

-- | Get the <tt>TVar</tt>s a transaction read from.
tvarsRead :: ThreadAction -> Set TVarId

-- | Convert a <a>ThreadAction</a> into a <a>Lookahead</a>: "rewind" what
--   has happened.
rewind :: ThreadAction -> 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>readIORef</tt> or a <tt>readForCAS</tt>.
UnsynchronisedRead :: IORefId -> ActionType

-- | A <tt>writeIORef</tt>.
UnsynchronisedWrite :: IORefId -> ActionType

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

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

-- | A <tt>casIORef</tt>
PartiallySynchronisedWrite :: IORefId -> ActionType

-- | A <tt>modifyIORefCAS</tt>
PartiallySynchronisedModify :: IORefId -> ActionType

-- | An <tt>atomicModifyIORef</tt>.
SynchronisedModify :: IORefId -> 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>IORef</tt>.
isCommit :: ActionType -> IORefId -> Bool

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

-- | Get the <tt>IORef</tt> affected.
iorefOf :: ActionType -> Maybe IORefId

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

-- | Get the <tt>ThreadId</tt>s involved in a <tt>ThreadAction</tt>.
tidsOf :: ThreadAction -> Set ThreadId

-- | 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>tail</a> but with a better error message if it fails. Use this only
--   where it shouldn't fail!
etail :: HasCallStack => [a] -> [a]

-- | '(!!)' but with a better error message if it fails. Use this only
--   where it shouldn't fail!
eidx :: HasCallStack => [a] -> Int -> a

-- | <tt>fromJust</tt> but with a better error message if it fails. Use
--   this only where it shouldn't fail!
efromJust :: HasCallStack => Maybe a -> a

-- | <tt>fromList</tt> but with a better error message if it fails. Use
--   this only where it shouldn't fail!
efromList :: HasCallStack => [a] -> NonEmpty a

-- | <tt>fromRight</tt> but with a better error message if it fails. Use
--   this only where it shouldn't fail!
efromRight :: HasCallStack => Either a b -> b

-- | <a>adjust</a> but which errors if the key is not present. Use this
--   only where it shouldn't fail!
eadjust :: (Ord k, Show k, HasCallStack) => (v -> v) -> k -> Map k v -> Map k v

-- | <a>insert</a> but which errors if the key is already present. Use this
--   only where it shouldn't fail!
einsert :: (Ord k, Show k, HasCallStack) => k -> v -> Map k v -> Map k v

-- | <a>lookup</a> but which errors if the key is not present. Use this
--   only where it shouldn't fail!
elookup :: (Ord k, Show k, HasCallStack) => k -> Map k v -> v

-- | <a>error</a> but saying where it came from
fatal :: HasCallStack => String -> a

-- | Run with a continuation that writes its value into a reference,
--   returning the computation and the reference. Using the reference is
--   non-blocking, it is up to you to ensure you wait sufficiently.
runRefCont :: MonadConc n => (n () -> x) -> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, IORef n (Maybe b))
instance Control.DeepSeq.NFData Test.DejaFu.Internal.ActionType
instance GHC.Generics.Generic Test.DejaFu.Internal.ActionType
instance GHC.Show.Show Test.DejaFu.Internal.ActionType
instance GHC.Classes.Eq Test.DejaFu.Internal.ActionType
instance Control.DeepSeq.NFData Test.DejaFu.Internal.IdSource
instance GHC.Generics.Generic Test.DejaFu.Internal.IdSource
instance GHC.Show.Show Test.DejaFu.Internal.IdSource
instance GHC.Classes.Ord Test.DejaFu.Internal.IdSource
instance GHC.Classes.Eq Test.DejaFu.Internal.IdSource
instance GHC.Show.Show Test.DejaFu.Internal.Way


-- | Configuration for the SCT functions.
module Test.DejaFu.Settings

-- | SCT configuration record.
data Settings n a

-- | Default SCT settings: just combine all the other defaults.
defaultSettings :: Applicative n => Settings n a

-- | Construct a <a>Settings</a> record from a <a>Way</a> and a
--   <a>MemType</a>.
--   
--   All other settings take on their default values.
fromWayAndMemType :: Applicative n => Way -> MemType -> Settings n a

-- | 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

-- | A lens into the <a>Way</a>.
lway :: Lens' (Settings n a) Way

-- | Systematically execute a program, trying all distinct executions
--   within the bounds.
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 is not guaranteed to find all distinct results (unlike
--   <a>systematically</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 is not guaranteed to find all distinct results (unlike
--   <a>systematically</a>).
uniformly :: RandomGen g => g -> Int -> Way

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

-- | Restrict the number of pre-emptive context switches allowed in an
--   execution.
--   
--   A pre-emption bound of zero disables pre-emptions entirely.
newtype PreemptionBound
PreemptionBound :: Int -> PreemptionBound

-- | Restrict the maximum difference between the number of yield or delay
--   operations different threads have performed.
--   
--   A fair bound of zero disables yields and delays entirely.
newtype FairBound
FairBound :: Int -> FairBound

-- | Restrict the maximum length (in terms of primitive actions) of an
--   execution.
--   
--   A length bound of zero immediately aborts the execution.
newtype LengthBound
LengthBound :: Int -> LengthBound

-- | All bounds enabled, using their default values.
--   
--   There is no default length bound, so set one if your computation may
--   not terminate!
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

-- | There is no default length bound.
--   
--   This is only suitable if your computation will always terminate!
defaultLengthBound :: 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

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

-- | The most intuitive model: a program behaves as a simple interleaving
--   of the actions in different threads. When a <tt>IORef</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>IORef</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>IORef</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

-- | A lens into the <a>MemType</a>.
lmemtype :: Lens' (Settings n a) MemType

-- | An <tt>Either Failure a -&gt; Maybe Discard</tt> value can be used to
--   selectively discard results.
data Discard

-- | Discard the trace but keep the result. The result will appear to have
--   an empty trace.
DiscardTrace :: Discard

-- | Discard the result and the trace. It will simply not be reported as a
--   possible behaviour of the program.
DiscardResultAndTrace :: Discard

-- | A lens into the discard function.
ldiscard :: Lens' (Settings n a) (Maybe (Either Failure a -> Maybe Discard))

-- | A lens into the early-exit predicate.
learlyExit :: Lens' (Settings n a) (Maybe (Either Failure a -> Bool))

-- | A lens into the equality predicate.
lequality :: Lens' (Settings n a) (Maybe (a -> a -> Bool))

-- | A lens into the simplify flag.
lsimplify :: Lens' (Settings n a) Bool

-- | A lens into the safe IO flag.
lsafeIO :: Lens' (Settings n a) Bool

-- | A lens into the debug <a>show</a> function.
ldebugShow :: Lens' (Settings n a) (Maybe (a -> String))

-- | A lens into the debug <a>print</a> function.
ldebugPrint :: Lens' (Settings n a) (Maybe (String -> n ()))

-- | A lens into the make-recoverable-errors-fatal flag.
ldebugFatal :: Lens' (Settings n a) Bool

-- | Get a value from a lens.
get :: Lens' s a -> s -> a

-- | Set a value in a lens.
set :: Lens' s a -> a -> s -> s


-- | 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 last thread executed (if this is the first invocation, this is
--   <tt>Nothing</tt>).</li>
--   <li>The unblocked threads.</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.
newtype Scheduler state
Scheduler :: Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> state -> (Maybe ThreadId, state) -> Scheduler state
[scheduleThread] :: Scheduler state -> Maybe (ThreadId, ThreadAction) -> NonEmpty (ThreadId, Lookahead) -> state -> (Maybe ThreadId, state)

-- | 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 previously scheduled thread is not blocked, it is picked again,
--   otherwise schedule randomly.
randomSchedNP :: RandomGen g => Scheduler g

-- | A round-robin scheduler which doesn't preempt the running thread. That
--   is, if the previously scheduled thread is not blocked, it is picked
--   again, otherwise schedule the thread with the next <a>ThreadId</a>.
roundRobinSchedNP :: Scheduler ()

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


-- | Internal types and functions for SCT via weighted random scheduling.
--   This module is NOT considered to form part of the public interface of
--   this library.
module Test.DejaFu.SCT.Internal.Weighted

-- | 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 :: 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)
instance Control.DeepSeq.NFData g => Control.DeepSeq.NFData (Test.DejaFu.SCT.Internal.Weighted.RandSchedState g)
instance GHC.Generics.Generic (Test.DejaFu.SCT.Internal.Weighted.RandSchedState g)
instance GHC.Show.Show g => GHC.Show.Show (Test.DejaFu.SCT.Internal.Weighted.RandSchedState g)
instance GHC.Classes.Eq g => GHC.Classes.Eq (Test.DejaFu.SCT.Internal.Weighted.RandSchedState g)


-- | <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.Conc.Internal.STM

-- | The underlying monad is based on continuations over primitive actions.
--   
--   This is not <tt>Cont</tt> because we want to give it a custom
--   <tt>MonadFail</tt> instance.
newtype ModelSTM n a
ModelSTM :: (a -> STMAction n) -> STMAction n -> ModelSTM n a
[runModelSTM] :: ModelSTM n a -> (a -> STMAction n) -> STMAction n

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

-- | A <tt>TVar</tt> is modelled as a unique ID and a reference holding a
--   value.
data ModelTVar n a
ModelTVar :: TVarId -> IORef n a -> ModelTVar n a
[tvarId] :: ModelTVar n a -> TVarId
[tvarRef] :: ModelTVar n a -> IORef n a

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

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

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

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

-- | Run a transaction, returning the result and new initial <a>TVarId</a>.
--   If the transaction failed, any effects are undone.
runTransaction :: MonadConc n => ModelSTM n a -> IdSource -> n (Result a, IdSource, [TAction])

-- | Run a STM transaction, returning an action to undo its effects.
--   
--   If the transaction fails, its effects will automatically be undone, so
--   the undo action returned will be <tt>pure ()</tt>.
doTransaction :: MonadConc n => ModelSTM n a -> IdSource -> n (Result a, n (), IdSource, [TAction])

-- | Run a transaction for one step.
stepTrans :: MonadConc n => STMAction n -> IdSource -> n (STMAction n, n (), IdSource, [TVarId], [TVarId], TAction)
instance GHC.Show.Show a => GHC.Show.Show (Test.DejaFu.Conc.Internal.STM.Result a)
instance GHC.Base.Functor (Test.DejaFu.Conc.Internal.STM.ModelSTM n)
instance GHC.Base.Applicative (Test.DejaFu.Conc.Internal.STM.ModelSTM n)
instance GHC.Base.Monad (Test.DejaFu.Conc.Internal.STM.ModelSTM n)
instance Control.Monad.Fail.MonadFail (Test.DejaFu.Conc.Internal.STM.ModelSTM n)
instance Control.Monad.Catch.MonadThrow (Test.DejaFu.Conc.Internal.STM.ModelSTM n)
instance Control.Monad.Catch.MonadCatch (Test.DejaFu.Conc.Internal.STM.ModelSTM n)
instance GHC.Base.Alternative (Test.DejaFu.Conc.Internal.STM.ModelSTM n)
instance GHC.Base.MonadPlus (Test.DejaFu.Conc.Internal.STM.ModelSTM n)
instance Control.Monad.STM.Class.MonadSTM (Test.DejaFu.Conc.Internal.STM.ModelSTM n)


-- | Common types and utility functions for deterministic execution of
--   <tt>MonadConc</tt> implementations. This module is NOT considered to
--   form part of the public interface of this library.
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 ModelConc n a
ModelConc :: (a -> Action n) -> Action n -> ModelConc n a
[runModelConc] :: ModelConc n a -> (a -> Action n) -> Action n

-- | An <tt>MVar</tt> is modelled as a unique ID and a reference holding a
--   <tt>Maybe</tt> value.
data ModelMVar n a
ModelMVar :: MVarId -> IORef n (Maybe a) -> ModelMVar n a
[mvarId] :: ModelMVar n a -> MVarId
[mvarRef] :: ModelMVar n a -> IORef n (Maybe a)

-- | A <tt>IORef</tt> is modelled as a unique ID and a reference holding
--   thread-local values, the number of commits, and the most recent
--   committed value.
data ModelIORef n a
ModelIORef :: IORefId -> IORef n (Map ThreadId a, Integer, a) -> ModelIORef n a
[iorefId] :: ModelIORef n a -> IORefId
[iorefRef] :: ModelIORef n a -> IORef n (Map ThreadId a, Integer, a)

-- | A <tt>Ticket</tt> is modelled as the ID of the <tt>ModelIORef</tt> it
--   came from, the commits to the <tt>ModelIORef</tt> at the time it was
--   produced, and the value observed.
data ModelTicket a
ModelTicket :: IORefId -> Integer -> a -> ModelTicket a
[ticketIORef] :: ModelTicket a -> IORefId
[ticketWrites] :: ModelTicket a -> Integer
[ticketVal] :: ModelTicket a -> a

-- | 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
AFork :: String -> ((forall b. ModelConc n b -> ModelConc n b) -> Action n) -> (ThreadId -> Action n) -> Action n
AForkOS :: String -> ((forall b. ModelConc n b -> ModelConc n b) -> Action n) -> (ThreadId -> Action n) -> Action n
AIsBound :: (Bool -> Action n) -> Action n
AMyTId :: (ThreadId -> Action n) -> Action n
AGetNumCapabilities :: (Int -> Action n) -> Action n
ASetNumCapabilities :: Int -> (Action n) -> Action n
ANewMVar :: String -> (ModelMVar n a -> Action n) -> Action n
APutMVar :: (ModelMVar n a) -> a -> (Action n) -> Action n
ATryPutMVar :: (ModelMVar n a) -> a -> (Bool -> Action n) -> Action n
AReadMVar :: (ModelMVar n a) -> (a -> Action n) -> Action n
ATryReadMVar :: (ModelMVar n a) -> (Maybe a -> Action n) -> Action n
ATakeMVar :: (ModelMVar n a) -> (a -> Action n) -> Action n
ATryTakeMVar :: (ModelMVar n a) -> (Maybe a -> Action n) -> Action n
ANewIORef :: String -> a -> (ModelIORef n a -> Action n) -> Action n
AReadIORef :: (ModelIORef n a) -> (a -> Action n) -> Action n
AReadIORefCas :: (ModelIORef n a) -> (ModelTicket a -> Action n) -> Action n
AModIORef :: (ModelIORef n a) -> (a -> (a, b)) -> (b -> Action n) -> Action n
AModIORefCas :: (ModelIORef n a) -> (a -> (a, b)) -> (b -> Action n) -> Action n
AWriteIORef :: (ModelIORef n a) -> a -> (Action n) -> Action n
ACasIORef :: (ModelIORef n a) -> (ModelTicket a) -> a -> ((Bool, ModelTicket a) -> Action n) -> Action n
AThrow :: e -> Action n
AThrowTo :: ThreadId -> e -> (Action n) -> Action n
ACatching :: (e -> ModelConc n a) -> (ModelConc n a) -> (a -> Action n) -> Action n
APopCatching :: (Action n) -> Action n
AMasking :: MaskingState -> ((forall b. ModelConc n b -> ModelConc n b) -> ModelConc n a) -> (a -> Action n) -> Action n
AResetMask :: Bool -> Bool -> MaskingState -> (Action n) -> Action n
AAtom :: (ModelSTM n a) -> (a -> Action n) -> Action n
ALift :: (n (Action n)) -> Action n
AYield :: (Action n) -> Action n
ADelay :: Int -> (Action n) -> Action n
AReturn :: (Action n) -> Action n
ACommit :: ThreadId -> IORefId -> Action n
AStop :: (n ()) -> Action n
ASub :: (ModelConc n a) -> (Either Failure a -> Action n) -> Action n
AStopSub :: (Action n) -> Action n
ADontCheck :: (Maybe Int) -> (ModelConc n a) -> (a -> Action n) -> Action n

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


-- | 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 = Map ThreadId (Thread n)

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

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

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

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

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

-- | State for the associated bound thread, if it exists.
[_bound] :: Thread n -> Maybe (BoundThread n)

-- | The state of a bound thread.
data BoundThread n
BoundThread :: MVar n (n (Action n)) -> MVar n (Action n) -> ThreadId n -> BoundThread n

-- | Run an <tt>IO</tt> action in the bound thread by writing to this.
[_runboundIO] :: BoundThread n -> MVar n (n (Action n))

-- | Get the result of the above by reading from this.
[_getboundIO] :: BoundThread n -> MVar n (Action n)

-- | Thread ID
[_boundTId] :: BoundThread n -> ThreadId n

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

-- | 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 -> BlockedOn -> Bool

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

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

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

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

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

-- | Raise an exception in a thread.
except :: HasCallStack => (MaskingState -> Action n) -> [Handler n] -> ThreadId -> Threads n -> Threads n

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

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

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

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

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

-- | 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 -> (Threads n, [ThreadId])

-- | Turn a thread into a bound thread.
makeBound :: (MonadConc n, HasCallStack) => ThreadId -> Threads n -> n (Threads n)

-- | Kill a thread and remove it from the thread map.
--   
--   If the thread is bound, the worker thread is cleaned up.
kill :: (MonadConc n, HasCallStack) => ThreadId -> Threads n -> n (Threads n)

-- | Run an action.
--   
--   If the thread is bound, the action is run in the worker thread.
runLiftedAct :: MonadConc n => ThreadId -> Threads n -> n (Action n) -> n (Action n)
instance GHC.Classes.Eq Test.DejaFu.Conc.Internal.Threading.BlockedOn


-- | Operations over <tt>IORef</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>IORef</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>IORef</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>IORefId</tt> parameter is only used under PSO. Under TSO each
--   thread has a single buffer.
newtype WriteBuffer n
WriteBuffer :: Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n)) -> WriteBuffer n
[buffer] :: WriteBuffer n -> Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n))

-- | 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 n
[BufferedWrite] :: ThreadId -> ModelIORef n a -> a -> BufferedWrite n

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

-- | Add a new write to the end of a buffer.
bufferWrite :: MonadConc n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> ModelIORef n a -> a -> n (WriteBuffer n)

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

-- | Read from a <tt>IORef</tt>, returning a newer thread-local
--   non-committed write if there is one.
readIORef :: MonadConc n => ModelIORef n a -> ThreadId -> n a

-- | Read from a <tt>IORef</tt>, returning a <tt>Ticket</tt> representing
--   the current view of the thread.
readForTicket :: MonadConc n => ModelIORef n a -> ThreadId -> n (ModelTicket a)

-- | Perform a compare-and-swap on a <tt>IORef</tt> if the ticket is still
--   valid. This is strict in the "new" value argument.
casIORef :: MonadConc n => ModelIORef n a -> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ())

-- | Read the local state of a <tt>IORef</tt>.
readIORefPrim :: MonadConc n => ModelIORef n a -> ThreadId -> n (a, Integer)

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

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

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

-- | The ID of a commit thread.
commitThreadId :: ThreadId -> Maybe IORefId -> ThreadId

-- | Remove phantom threads.
delCommitThreads :: Threads n -> Threads n
data Blocking
Blocking :: Blocking
NonBlocking :: Blocking
data Emptying
Emptying :: Emptying
NonEmptying :: Emptying

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

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

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

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

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

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

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

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


-- | 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, Lookahead)], ThreadAction)

-- | The result of running a concurrent program.
data CResult n g a
CResult :: Context n g -> IORef n (Maybe (Either Failure a)) -> Maybe (Threads n -> n ()) -> SeqTrace -> Maybe (ThreadId, ThreadAction) -> CResult n g a
[finalContext] :: CResult n g a -> Context n g
[finalRef] :: CResult n g a -> IORef n (Maybe (Either Failure a))

-- | Meaningless if this result doesn't come from a snapshotting execution.
[finalRestore] :: CResult n g a -> Maybe (Threads n -> n ())
[finalTrace] :: CResult n g a -> SeqTrace
[finalDecision] :: CResult n g a -> Maybe (ThreadId, ThreadAction)

-- | A snapshot of the concurrency state immediately after
--   <tt>dontCheck</tt> finishes.
data DCSnapshot n a
DCSnapshot :: Context n () -> Threads n -> n () -> IORef n (Maybe (Either Failure a)) -> DCSnapshot n a

-- | The execution context. The scheduler state is ignored when restoring.
[dcsContext] :: DCSnapshot n a -> Context n ()

-- | Action to restore IORef, MVar, and TVar values.
[dcsRestore] :: DCSnapshot n a -> Threads n -> n ()

-- | Reference where the result will be written.
[dcsRef] :: DCSnapshot n a -> IORef n (Maybe (Either Failure a))

-- | 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 :: (MonadConc n, HasCallStack) => Bool -> Scheduler g -> MemType -> g -> IdSource -> Int -> ModelConc n a -> n (CResult n g a)

-- | Run a concurrent program using the given context, and without killing
--   threads which remain at the end. The context must have no main thread.
--   
--   Only a separate function because <tt>ADontCheck</tt> needs it.
runConcurrency' :: (MonadConc n, HasCallStack) => Bool -> Scheduler g -> MemType -> Context n g -> ModelConc n a -> n (CResult n g a)

-- | Like <a>runConcurrency</a> but starts from a snapshot.
runConcurrencyWithSnapshot :: (MonadConc n, HasCallStack) => Scheduler g -> MemType -> Context n g -> (Threads n -> n ()) -> IORef n (Maybe (Either Failure a)) -> n (CResult n g a)

-- | Kill the remaining threads
killAllThreads :: (MonadConc n, HasCallStack) => Context n g -> n ()

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

-- | Run a collection of threads, until there are no threads left.
runThreads :: (MonadConc n, HasCallStack) => Bool -> Scheduler g -> MemType -> IORef n (Maybe (Either Failure a)) -> Context n g -> n (CResult n g a)

-- | Apply the context update from stepping an action.
fixContext :: ThreadId -> What n g -> Context n g -> Context n g

-- | <tt>unblockWaitingOn tid</tt> unblocks every thread blocked in a
--   <tt>throwTo tid</tt>.
unblockWaitingOn :: ThreadId -> Threads n -> Threads n

-- | What a thread did, for trace purposes.
data Act

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

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

-- | What a thread did, for execution purposes.
data What n g

-- | Action succeeded: continue execution.
Succeeded :: (Context n g) -> What n g

-- | Action caused computation to fail: stop.
Failed :: Failure -> What n g

-- | Action was a snapshot point and we're in snapshot mode: stop.
Snap :: (Context n g) -> What n g

-- | Run a single thread one step, by dispatching on the type of
--   <a>Action</a>.
--   
--   Each case looks very similar. This is deliberate, so that the
--   essential differences between actions are more apparent, and not
--   hidden by accidental differences in how things are expressed.
--   
--   Note: the returned snapshot action will definitely not do the right
--   thing with relaxed memory.
stepThread :: (MonadConc n, HasCallStack) => Bool -> Bool -> Scheduler g -> MemType -> ThreadId -> Action n -> Context n g -> n (What n g, Act, Threads n -> n ())

-- | Handle an exception being thrown from an <tt>AAtom</tt>,
--   <tt>AThrow</tt>, or <tt>AThrowTo</tt>.
stepThrow :: (MonadConc n, Exception e) => (Bool -> ThreadAction) -> ThreadId -> e -> Context n g -> n (What n g, Act, Threads n -> n ())

-- | Helper for actions impose a write barrier.
synchronised :: MonadConc n => (Context n g -> n (What n g, Act, Threads n -> n ())) -> Context n g -> n (What n g, Act, Threads n -> n ())

-- | scheduler for <tt>ADontCheck</tt>
dcSched :: Scheduler (Maybe Int)
instance GHC.Show.Show Test.DejaFu.Conc.Internal.Act
instance GHC.Classes.Eq Test.DejaFu.Conc.Internal.Act


-- | Utility functions for users of dejafu.
module Test.DejaFu.Utils

-- | Turn a <a>Trace</a> into an abbreviated form.
toTIdTrace :: Trace -> [(ThreadId, ThreadAction)]

-- | 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

-- | Get all named threads in the trace.
threadNames :: Trace -> [(Int, String)]

-- | Find the "simplest" trace leading to each result.
simplestsBy :: (x -> x -> Bool) -> [(x, Trace)] -> [(x, Trace)]

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

-- | 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 collection of threads
--   which are unblocked at this point.
decisionOf :: Foldable f => Maybe ThreadId -> f ThreadId -> ThreadId -> Decision


-- | Internal types and functions for SCT via 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

-- | 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 -> Maybe (ThreadId, DPOR) -> Set ThreadId -> Map ThreadId ThreadAction -> Map ThreadId 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

-- | The next decision made. Executions are explored in a depth-first
--   fashion, so this changes as old subtrees are exhausted and new ones
--   explored.
[dporNext] :: DPOR -> Maybe (ThreadId, DPOR)

-- | All transitions which have been taken from this point, including
--   conservatively-added ones.
[dporDone] :: DPOR -> Set ThreadId

-- | 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

-- | Check the DPOR data invariants and raise an error if any are broken.
--   
--   This is a reasonable thing to do, because if the state is corrupted
--   then nothing sensible can happen anyway.
validateDPOR :: HasCallStack => DPOR -> DPOR

-- | 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.
--   
--   The main thread must be in the list of initially runnable threads.
initialState :: [ThreadId] -> 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 stack. This won't work if to-dos aren't
--   explored depth-first.
incorporateTrace :: HasCallStack => Bool -> 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 :: Bool -> MemType -> BacktrackFunc -> Bool -> Seq ([(ThreadId, Lookahead)], [ThreadId]) -> Trace -> [BacktrackStep]

-- | Add new backtracking points, if they have not already been visited and
--   aren't in the sleep set.
incorporateBacktrackSteps :: HasCallStack => [BacktrackStep] -> DPOR -> DPOR

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

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

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

-- | Which threads are runnable and in-bound at each step, and the
--   alternative decisions still to make.
[schedBPoints] :: DPORSchedState k -> Seq ([(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 k -> Bool

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

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

-- | State used by the incremental bounding function.
[schedBState] :: DPORSchedState k -> Maybe k

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

-- | An incremental bounding function is a stateful function that takes the
--   last and next decisions, and returns a new state only if the next
--   decision is within the bound.
type IncrementalBoundFunc k = Maybe k -> Maybe (ThreadId, ThreadAction) -> (Decision, Lookahead) -> Maybe k

-- | 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 :: HasCallStack => (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 :: HasCallStack => Bool -> MemType -> IncrementalBoundFunc k -> Scheduler (DPORSchedState k)

-- | Check if two actions commute.
--   
--   This implements a stronger check that <tt>not (dependent ...)</tt>, as
--   it handles some cases which <a>dependent</a> doesn't need to care
--   about.
--   
--   This should not be used to re-order traces which contain
--   subconcurrency.
independent :: Bool -> DepState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool

-- | Check if an action is dependent on another.
--   
--   This is basically the same as <a>dependent'</a>, but can make use of
--   the additional information in a <a>ThreadAction</a> to make better
--   decisions in a few cases.
dependent :: Bool -> 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' :: Bool -> 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 :: DepState -> ActionType -> ActionType -> Bool
data DepState
DepState :: Map IORefId Bool -> Set MVarId -> Map ThreadId MaskingState -> DepState

-- | Keep track of which <tt>IORef</tt>s have buffered writes.
[depIOState] :: DepState -> Map IORefId Bool

-- | Keep track of which <tt>MVar</tt>s are full.
[depMVState] :: DepState -> Set MVarId

-- | 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 dependency state with the action that has just happened.
updateDepState :: MemType -> DepState -> ThreadId -> ThreadAction -> DepState

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

-- | Update the <tt>MVar</tt> full/empty state with the action that has
--   just happened.
updateMVState :: ThreadAction -> Set MVarId -> Set MVarId

-- | 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>IORef</tt> has a buffered write pending.
isBuffered :: DepState -> IORefId -> Bool

-- | Check if an <tt>MVar</tt> is full.
isFull :: DepState -> MVarId -> 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
instance Control.DeepSeq.NFData Test.DejaFu.SCT.Internal.DPOR.BacktrackStep
instance GHC.Generics.Generic Test.DejaFu.SCT.Internal.DPOR.BacktrackStep
instance GHC.Show.Show Test.DejaFu.SCT.Internal.DPOR.BacktrackStep
instance GHC.Classes.Eq Test.DejaFu.SCT.Internal.DPOR.BacktrackStep
instance Control.DeepSeq.NFData k => Control.DeepSeq.NFData (Test.DejaFu.SCT.Internal.DPOR.DPORSchedState k)
instance GHC.Generics.Generic (Test.DejaFu.SCT.Internal.DPOR.DPORSchedState k)
instance GHC.Show.Show k => GHC.Show.Show (Test.DejaFu.SCT.Internal.DPOR.DPORSchedState k)
instance GHC.Classes.Eq k => GHC.Classes.Eq (Test.DejaFu.SCT.Internal.DPOR.DPORSchedState k)
instance GHC.Show.Show Test.DejaFu.SCT.Internal.DPOR.DepState
instance GHC.Classes.Eq Test.DejaFu.SCT.Internal.DPOR.DepState
instance Control.DeepSeq.NFData Test.DejaFu.SCT.Internal.DPOR.DPOR
instance GHC.Generics.Generic Test.DejaFu.SCT.Internal.DPOR.DPOR
instance GHC.Show.Show Test.DejaFu.SCT.Internal.DPOR.DPOR
instance GHC.Classes.Eq Test.DejaFu.SCT.Internal.DPOR.DPOR
instance Control.DeepSeq.NFData Test.DejaFu.SCT.Internal.DPOR.DepState


-- | 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 n a

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

-- | An indication of how a concurrent computation failed.
--   
--   The <tt>Eq</tt>, <tt>Ord</tt>, and <tt>NFData</tt> instances
--   compare/evaluate the exception with <tt>show</tt> in the
--   <tt>UncaughtException</tt> case.
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

-- | Every thread is blocked, and the main thread is <i>not</i> blocked in
--   an STM transaction.
Deadlock :: Failure

-- | Every thread is blocked, and the main thread is blocked in an STM
--   transaction.
STMDeadlock :: Failure

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

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

-- | A call to <tt>dontCheck</tt> was attempted after the first action of
--   the initial thread.
IllegalDontCheck :: Failure

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

-- | The most intuitive model: a program behaves as a simple interleaving
--   of the actions in different threads. When a <tt>IORef</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>IORef</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>IORef</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.
--   
--   If the RTS supports bound threads (ghc -threaded when linking) then
--   the main thread of the concurrent computation will be bound, and
--   <tt>forkOS</tt> / <tt>forkOSN</tt> will work during execution. If not,
--   then the main thread will not be found, and attempting to fork a bound
--   thread will raise an error.
--   
--   <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 :: MonadConc n => Scheduler s -> MemType -> s -> ConcT 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, or placed
--   inside a call to <a>dontCheck</a>. Violating either of these
--   conditions will result in the computation failing with
--   <tt>IllegalSubconcurrency</tt>. The overall test-case can still
--   succeed if the predicate allows for a failing computation.
subconcurrency :: ConcT n a -> ConcT n (Either Failure a)

-- | Run an arbitrary action which gets some special treatment:
--   
--   <ul>
--   <li>For systematic testing, <a>dontCheck</a> is not dependent with
--   anything, even if the action has dependencies.</li>
--   <li>For pre-emption bounding, <a>dontCheck</a> counts for zero
--   pre-emptions, even if the action performs pre-emptive context
--   switches.</li>
--   <li>For fair bounding, <a>dontCheck</a> counts for zero yields/delays,
--   even if the action performs yields or delays.</li>
--   <li>For length bounding, <a>dontCheck</a> counts for one step, even if
--   the action has many.</li>
--   <li>All SCT functions use <a>runForDCSnapshot</a> /
--   <a>runWithDCSnapshot</a> to ensure that the action is only executed
--   once, although you should be careful with <tt>IO</tt> (see note on
--   snapshotting <tt>IO</tt>).</li>
--   </ul>
--   
--   The action is executed atomically with a deterministic scheduler under
--   sequential consistency. Any threads created inside the action continue
--   to exist in the main computation.
--   
--   This must be the first thing done in the main thread. Violating this
--   condition will result in the computation failing with
--   <tt>IllegalDontCheck</tt>. The overall test-case can still succeed if
--   the predicate allows for a failing computation.
--   
--   If the action fails (deadlock, length bound exceeded, etc), the whole
--   computation fails.
dontCheck :: Maybe Int -> ConcT n a -> ConcT n a

-- | A snapshot of the concurrency state immediately after
--   <tt>dontCheck</tt> finishes.
data DCSnapshot n a

-- | Like <a>runConcurrent</a>, but terminates immediately after running
--   the <a>dontCheck</a> action with a <a>DCSnapshot</a> which can be used
--   in <a>runWithDCSnapshot</a> to avoid doing that work again.
--   
--   If this program does not contain a legal use of <a>dontCheck</a>, then
--   the result will be <tt>Nothing</tt>.
--   
--   If you are using the SCT functions on an action which contains a
--   <a>dontCheck</a>, snapshotting will be handled for you, without you
--   needing to call this function yourself.
runForDCSnapshot :: MonadConc n => ConcT n a -> n (Maybe (Either Failure (DCSnapshot n a), Trace))

-- | Like <a>runConcurrent</a>, but uses a <a>DCSnapshot</a> produced by
--   <a>runForDCSnapshot</a> to skip the <a>dontCheck</a> work.
--   
--   If you are using the SCT functions on an action which contains a
--   <a>dontCheck</a>, snapshotting will be handled for you, without you
--   needing to call this function yourself.
runWithDCSnapshot :: MonadConc n => Scheduler s -> MemType -> s -> DCSnapshot n a -> n (Either Failure a, s, Trace)

-- | Check if a <a>DCSnapshot</a> can be taken from this computation.
canDCSnapshot :: ConcT n a -> Bool

-- | Get the threads which exist in a snapshot, partitioned into runnable
--   and not runnable.
threadsFromDCSnapshot :: DCSnapshot n a -> ([ThreadId], [ThreadId])

-- | One of the outputs of the runner is a <tt>Trace</tt>, which is a log
--   of decisions made, all the alternative unblocked threads and what they
--   would do, and the action a thread took in its step.
type Trace = [(Decision, [(ThreadId, 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 thread has a unique identitifer.
newtype ThreadId
ThreadId :: Id -> ThreadId

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

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

-- | Start a new bound thread.
ForkOS :: ThreadId -> ThreadAction

-- | Check if the current thread is bound.
IsCurrentThreadBound :: Bool -> 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

-- | Yield/delay the current thread.
ThreadDelay :: Int -> 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>IORef</tt>.
NewIORef :: IORefId -> ThreadAction

-- | Read from a <tt>IORef</tt>.
ReadIORef :: IORefId -> ThreadAction

-- | Read from a <tt>IORef</tt> for a future compare-and-swap.
ReadIORefCas :: IORefId -> ThreadAction

-- | Modify a <tt>IORef</tt>.
ModIORef :: IORefId -> ThreadAction

-- | Modify a <tt>IORef</tt> using a compare-and-swap.
ModIORefCas :: IORefId -> ThreadAction

-- | Write to a <tt>IORef</tt> without synchronising.
WriteIORef :: IORefId -> ThreadAction

-- | Attempt to to a <tt>IORef</tt> using a compare-and-swap, synchronising
--   it.
CasIORef :: IORefId -> Bool -> ThreadAction

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

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

-- | Got blocked in an STM transaction.
BlockedSTM :: [TAction] -> ThreadAction

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

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

-- | Throw an exception. If the <a>Bool</a> is <tt>True</tt>, then this
--   killed the thread.
Throw :: Bool -> ThreadAction

-- | Throw an exception to a thread. If the <a>Bool</a> is <tt>True</tt>,
--   then this killed the thread.
ThrowTo :: ThreadId -> Bool -> ThreadAction

-- | Get blocked on a <tt>throwTo</tt>.
BlockedThrowTo :: ThreadId -> 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

-- | Execute an action with <tt>dontCheck</tt>.
DontCheck :: Trace -> ThreadAction

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

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

-- | Will start a new bound thread.
WillForkOS :: Lookahead

-- | Will check if the current thread is bound.
WillIsCurrentThreadBound :: 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 yield/delay the current thread.
WillThreadDelay :: Int -> 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>IORef</tt>.
WillNewIORef :: Lookahead

-- | Will read from a <tt>IORef</tt>.
WillReadIORef :: IORefId -> Lookahead

-- | Will read from a <tt>IORef</tt> for a future compare-and-swap.
WillReadIORefCas :: IORefId -> Lookahead

-- | Will modify a <tt>IORef</tt>.
WillModIORef :: IORefId -> Lookahead

-- | Will modify a <tt>IORef</tt> using a compare-and-swap.
WillModIORefCas :: IORefId -> Lookahead

-- | Will write to a <tt>IORef</tt> without synchronising.
WillWriteIORef :: IORefId -> Lookahead

-- | Will attempt to to a <tt>IORef</tt> using a compare-and-swap,
--   synchronising it.
WillCasIORef :: IORefId -> Lookahead

-- | Will commit the last write by the given thread to the <tt>IORef</tt>.
WillCommitIORef :: ThreadId -> IORefId -> 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

-- | Will execute an action with <tt>dontCheck</tt>.
WillDontCheck :: Lookahead

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

-- | Every <tt>IORef</tt> has a unique identifier.
data IORefId

-- | 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 Control.Monad.Fail.MonadFail (Test.DejaFu.Conc.ConcT n)
instance GHC.Base.Monad (Test.DejaFu.Conc.ConcT n)
instance GHC.Base.Applicative (Test.DejaFu.Conc.ConcT n)
instance GHC.Base.Functor (Test.DejaFu.Conc.ConcT n)
instance Control.Monad.IO.Class.MonadIO n => Control.Monad.IO.Class.MonadIO (Test.DejaFu.Conc.ConcT n)
instance Control.Monad.Trans.Class.MonadTrans Test.DejaFu.Conc.ConcT
instance Control.Monad.Catch.MonadCatch (Test.DejaFu.Conc.ConcT n)
instance Control.Monad.Catch.MonadThrow (Test.DejaFu.Conc.ConcT n)
instance Control.Monad.Catch.MonadMask (Test.DejaFu.Conc.ConcT n)
instance GHC.Base.Monad n => Control.Monad.Conc.Class.MonadConc (Test.DejaFu.Conc.ConcT n)


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

-- | General-purpose SCT function.
sct :: (MonadConc n, HasCallStack) => Settings n a -> ([ThreadId] -> s) -> (s -> Maybe t) -> ((Scheduler g -> g -> n (Either Failure a, g, Trace)) -> s -> t -> n (s, Maybe (Either Failure a, Trace))) -> ConcT n a -> n [(Either Failure a, Trace)]

-- | Like <a>sct</a> but given a function to run the computation.
sct' :: (MonadConc n, HasCallStack) => Settings n a -> s -> (s -> Maybe t) -> (s -> t -> n (s, Maybe (Either Failure a, Trace))) -> (forall x. Scheduler x -> x -> n (Either Failure a, x, Trace)) -> ThreadId -> IORefId -> n [(Either Failure a, Trace)]

-- | Given a result and a trace, produce a more minimal trace.
--   
--   In principle, simplification is semantics preserving and can be done
--   without needing to execute the computation again. However, there are
--   two good reasons to do so:
--   
--   <ul>
--   <li>It's a sanity check that there are no bugs.</li>
--   <li>It's easier to generate a reduced sequence of scheduling decisions
--   and let dejafu generate the full trace, than to generate a reduced
--   trace directly</li>
--   </ul>
--   
--   Unlike shrinking in randomised property-testing tools like QuickCheck
--   or Hedgehog, we only run the test case <i>once</i>, at the end, rather
--   than after every simplification step.
simplifyExecution :: (MonadConc n, HasCallStack) => Settings n a -> (forall x. Scheduler x -> x -> n (Either Failure a, x, Trace)) -> ThreadId -> IORefId -> Either Failure a -> Trace -> n (Either Failure a, Trace)

-- | Replay an execution.
replay :: MonadConc n => (forall x. Scheduler x -> x -> n (Either Failure a, x, Trace)) -> [(ThreadId, ThreadAction)] -> n (Either Failure a, [(ThreadId, ThreadAction)], Trace)

-- | Simplify a trace by permuting adjacent independent actions to reduce
--   context switching.
simplify :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]

-- | Put a trace into lexicographic (by thread ID) normal form.
lexicoNormalForm :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]

-- | Swap adjacent independent actions in the trace if a predicate holds.
permuteBy :: Bool -> MemType -> [ThreadId -> ThreadId -> Bool] -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]

-- | Throw away commit actions which are followed by a memory barrier.
dropCommits :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]

-- | Attempt to reduce context switches by "pulling" thread actions back to
--   a prior execution of that thread.
--   
--   Simple example, say we have <tt>[(tidA, act1), (tidB, act2), (tidA,
--   act3)]</tt>, where <tt>act2</tt> and <tt>act3</tt> are independent. In
--   this case <a>pullBack</a> will swap them, giving the sequence
--   <tt>[(tidA, act1), (tidA, act3), (tidB, act2)]</tt>. It works for
--   arbitrary separations.
pullBack :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]

-- | Attempt to reduce context switches by "pushing" thread actions forward
--   to a future execution of that thread.
--   
--   This is kind of the opposite of <a>pullBack</a>, but there are cases
--   where one applies but not the other.
--   
--   Simple example, say we have <tt>[(tidA, act1), (tidB, act2), (tidA,
--   act3)]</tt>, where <tt>act1</tt> and <tt>act2</tt> are independent. In
--   this case <a>pushForward</a> will swap them, giving the sequence
--   <tt>[(tidB, act2), (tidA, act1), (tidA, act3)]</tt>. It works for
--   arbitrary separations.
pushForward :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]

-- | Re-number threads and IORefs.
--   
--   Permuting forks or newIORefs makes the existing numbering invalid,
--   which then causes problems for scheduling. Just re-numbering threads
--   isn't enough, as IORef IDs are used to determine commit thread IDs.
--   
--   Renumbered things will not fix their names, so don't rely on those at
--   all.
renumber :: MemType -> Int -> Int -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]

-- | Helper function for constructing IDs of any sort.
toId :: Coercible Id a => Int -> a

-- | Helper function for deconstructing IDs of any sort.
fromId :: Coercible a Id => a -> Int


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

-- | Explore possible executions of a concurrent program according to the
--   given <a>Way</a>.
--   
--   The exact executions tried, and the order in which results are found,
--   is unspecified and may change between releases.
runSCT :: MonadConc n => Way -> MemType -> ConcT 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.
--   
--   The exact executions tried, and the order in which results are found,
--   is unspecified and may change between releases.
runSCT' :: (MonadConc n, NFData a) => Way -> MemType -> ConcT n a -> n [(Either Failure a, Trace)]

-- | Return the set of results of a concurrent program.
resultsSet :: (MonadConc n, Ord a) => Way -> MemType -> ConcT 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' :: (MonadConc n, Ord a, NFData a) => Way -> MemType -> ConcT n a -> n (Set (Either Failure a))

-- | A variant of <a>runSCT</a> which takes a <a>Settings</a> record.
--   
--   The exact executions tried, and the order in which results are found,
--   is unspecified and may change between releases.
runSCTWithSettings :: MonadConc n => Settings n a -> ConcT n a -> n [(Either Failure a, Trace)]

-- | A strict variant of <a>runSCTWithSettings</a>.
--   
--   Demanding the result of this will force it to normal form, which may
--   be more efficient in some situations.
--   
--   The exact executions tried, and the order in which results are found,
--   is unspecified and may change between releases.
runSCTWithSettings' :: (MonadConc n, NFData a) => Settings n a -> ConcT n a -> n [(Either Failure a, Trace)]

-- | A variant of <a>resultsSet</a> which takes a <a>Settings</a> record.
resultsSetWithSettings :: (MonadConc n, Ord a) => Settings n a -> ConcT n a -> n (Set (Either Failure a))

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

-- | A variant of <a>runSCT</a> which can selectively discard results.
--   
--   The exact executions tried, and the order in which results are found,
--   is unspecified and may change between releases.

-- | <i>Deprecated: Use runSCTWithSettings instead</i>
runSCTDiscard :: MonadConc n => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n [(Either Failure a, Trace)]

-- | A strict variant of <a>runSCTDiscard</a>.
--   
--   Demanding the result of this will force it to normal form, which may
--   be more efficient in some situations.
--   
--   The exact executions tried, and the order in which results are found,
--   is unspecified and may change between releases.

-- | <i>Deprecated: Use runSCTWithSettings' instead</i>
runSCTDiscard' :: (MonadConc n, NFData a) => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n [(Either Failure a, Trace)]

-- | A variant of <a>resultsSet</a> which can selectively discard results.

-- | <i>Deprecated: Use resultsSetWithSettings instead</i>
resultsSetDiscard :: (MonadConc n, Ord a) => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n (Set (Either Failure a))

-- | A strict variant of <a>resultsSetDiscard</a>.
--   
--   Demanding the result of this will force it to normal form, which may
--   be more efficient in some situations.

-- | <i>Deprecated: Use resultsSetWithSettings' instead</i>
resultsSetDiscard' :: (MonadConc n, Ord a, NFData a) => (Either Failure a -> Maybe Discard) -> Way -> MemType -> ConcT n a -> n (Set (Either Failure a))

-- | 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.
--   
--   The exact executions tried, and the order in which results are found,
--   is unspecified and may change between releases.

-- | <i>Deprecated: Use runSCT instead</i>
sctBound :: MonadConc n => MemType -> Bounds -> ConcT n a -> n [(Either Failure a, Trace)]

-- | A variant of <a>sctBound</a> which can selectively discard results.
--   
--   The exact executions tried, and the order in which results are found,
--   is unspecified and may change between releases.

-- | <i>Deprecated: Use runSCTWithSettings instead</i>
sctBoundDiscard :: MonadConc n => (Either Failure a -> Maybe Discard) -> MemType -> Bounds -> ConcT n a -> n [(Either Failure a, Trace)]

-- | 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.

-- | <i>Deprecated: Use runSCT instead</i>
sctUniformRandom :: (MonadConc n, RandomGen g) => MemType -> g -> Int -> ConcT n a -> n [(Either Failure a, Trace)]

-- | A variant of <a>sctUniformRandom</a> which can selectively discard
--   results.
--   
--   This is not guaranteed to find all distinct results.

-- | <i>Deprecated: Use runSCTWithSettings instead</i>
sctUniformRandomDiscard :: (MonadConc n, RandomGen g) => (Either Failure a -> Maybe Discard) -> MemType -> g -> Int -> ConcT 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.

-- | <i>Deprecated: Use runSCT instead</i>
sctWeightedRandom :: (MonadConc n, RandomGen g) => MemType -> g -> Int -> ConcT n a -> n [(Either Failure a, Trace)]

-- | A variant of <a>sctWeightedRandom</a> which can selectively discard
--   results.
--   
--   This is not guaranteed to find all distinct results.

-- | <i>Deprecated: Use runSCTWithSettings instead</i>
sctWeightedRandomDiscard :: (MonadConc n, RandomGen g) => (Either Failure a -> Maybe Discard) -> MemType -> g -> Int -> ConcT n a -> n [(Either Failure a, Trace)]


-- | 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>
--   &gt;&gt;&gt; import Control.Monad (void)
--   
--   &gt;&gt;&gt; :{
--   let sig e = Sig
--         { initialise = maybe newEmptyMVar newMVar
--         , observe    = \v _ -&gt; tryReadMVar v
--         , interfere  = \v _ -&gt; putMVar v 42
--         , expression = void . e
--         }
--   :}
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; check $ sig readMVar === sig (\v -&gt; takeMVar v &gt;&gt;= putMVar v)
--   *** Failure: (seed Just 0)
--       left:  [(Nothing,Just 0)]
--       right: [(Nothing,Just 0),(Just Deadlock,Just 42)]
--   False
--   </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 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 x, GHC.Show.Show o) => 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)


-- | dejafu is a library for unit-testing concurrent Haskell programs,
--   written using the <a>concurrency</a> package's <a>MonadConc</a>
--   typeclass.
--   
--   <b>A first test:</b> This is a simple concurrent program which forks
--   two threads and each races to write to the same <tt>MVar</tt>:
--   
--   <pre>
--   &gt;&gt;&gt; :{
--   let example = do
--         var &lt;- newEmptyMVar
--         fork (putMVar var "hello")
--         fork (putMVar var "world")
--         readMVar var
--   :}
--   </pre>
--   
--   We can test it with dejafu like so:
--   
--   <pre>
--   &gt;&gt;&gt; autocheck example
--   [pass] Successful
--   [fail] Deterministic
--       "hello" S0----S1--S0--
--   
--       "world" S0----S2--S0--
--   False
--   </pre>
--   
--   The <a>autocheck</a> function takes a concurrent program to test and
--   looks for concurrency errors and nondeterminism. Here we see the
--   program is nondeterministic, dejafu gives us all the distinct results
--   it found and, for each, a summarised execution trace leading to that
--   result:
--   
--   <ul>
--   <li>"Sn" means that thread "n" started executing after the previous
--   thread terminated or blocked.</li>
--   <li>"Pn" means that thread "n" started executing, even though the
--   previous thread could have continued running.</li>
--   <li>Each "-" represents one "step" of the computation.</li>
--   </ul>
--   
--   <b>Failures:</b> If a program doesn't terminate successfully, we say
--   it has <i>failed</i>. dejafu can detect a few different types of
--   failure:
--   
--   <ul>
--   <li><a>Deadlock</a>, if every thread is blocked.</li>
--   <li><a>STMDeadlock</a>, if every thread is blocked <i>and</i> the main
--   thread is blocked in an STM transaction.</li>
--   <li><a>UncaughtException</a>, if the main thread is killed by an
--   exception.</li>
--   </ul>
--   
--   There are two types of failure which dejafu itself may raise:
--   
--   <ul>
--   <li><a>Abort</a>, used in systematic testing (the default) if there
--   are no allowed decisions remaining. For example, by default any test
--   case which takes more than 250 scheduling points to finish will be
--   aborted. You can use the <a>systematically</a> function to supply (or
--   disable) your own bounds.</li>
--   <li><a>InternalError</a>, used if something goes wrong. If you get
--   this and aren't using a scheduler you wrote yourself, please <a>file a
--   bug</a>.</li>
--   </ul>
--   
--   Finally, there are two failures which can arise through improper use
--   of dejafu:
--   
--   <ul>
--   <li><a>IllegalDontCheck</a>, the "Test.DejaFu.Conc.dontCheck" function
--   is used as anything other than the fist action in the main
--   thread.</li>
--   <li><a>IllegalSubconcurrency</a>, the
--   "Test.DejaFu.Conc.subconcurrency" function is used when multiple
--   threads exist, or is used inside another <tt>subconcurrency</tt>
--   call.</li>
--   </ul>
--   
--   <b>Beware of <a>liftIO</a>:</b> dejafu works by running your test case
--   lots of times with different schedules. If you use <a>liftIO</a> at
--   all, make sure that any <tt>IO</tt> you perform is deterministic when
--   executed in the same order.
--   
--   If you need to test things with <i>nondeterministc</i> <tt>IO</tt>,
--   see the <a>autocheckWay</a>, <a>dejafuWay</a>, and <a>dejafusWay</a>
--   functions: the <a>randomly</a> and <a>uniformly</a> testing modes can
--   cope with nondeterminism.
module Test.DejaFu

-- | Automatically test a computation.
--   
--   In particular, concurrency errors and nondeterminism. Returns
--   <tt>True</tt> if all tests pass
--   
--   <pre>
--   &gt;&gt;&gt; autocheck example
--   [pass] Successful
--   [fail] Deterministic
--       "hello" S0----S1--S0--
--   
--       "world" S0----S2--S0--
--   False
--   </pre>
autocheck :: (MonadConc n, MonadIO n, Eq a, Show a) => ConcT n a -> n Bool

-- | Check a predicate and print the result to stdout, return <a>True</a>
--   if it passes.
--   
--   A dejafu test has two parts: the program you are testing, and a
--   predicate to determine if the test passes. Predicates can look for
--   anything, including checking for some expected nondeterminism.
--   
--   <pre>
--   &gt;&gt;&gt; dejafu "Test Name" alwaysSame example
--   [fail] Test Name
--       "hello" S0----S1--S0--
--   
--       "world" S0----S2--S0--
--   False
--   </pre>
dejafu :: (MonadConc n, MonadIO n, Show b) => String -> ProPredicate a b -> ConcT n a -> n Bool

-- | Variant of <a>dejafu</a> which takes a collection of predicates to
--   test, returning <a>True</a> if all pass.
--   
--   <pre>
--   &gt;&gt;&gt; dejafus [("A", alwaysSame), ("B", deadlocksNever)] example
--   [fail] A
--       "hello" S0----S1--S0--
--   
--       "world" S0----S2--S0--
--   [pass] B
--   False
--   </pre>
dejafus :: (MonadConc n, MonadIO n, Show b) => [(String, ProPredicate a b)] -> ConcT n a -> n Bool

-- | Variant of <a>autocheck</a> which takes a way to run the program and a
--   memory model.
--   
--   <pre>
--   &gt;&gt;&gt; autocheckWay defaultWay defaultMemType relaxed
--   [pass] Successful
--   [fail] Deterministic
--       (False,True) S0---------S1----S0--S2----S0--
--   
--       (False,False) S0---------S1--P2----S1--S0---
--   
--       (True,False) S0---------S2----S1----S0---
--   
--       (True,True) S0---------S1-C-S2----S1---S0---
--   False
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; autocheckWay defaultWay SequentialConsistency relaxed
--   [pass] Successful
--   [fail] Deterministic
--       (False,True) S0---------S1----S0--S2----S0--
--   
--       (True,True) S0---------S1-P2----S1---S0---
--   
--       (True,False) S0---------S2----S1----S0---
--   False
--   </pre>
autocheckWay :: (MonadConc n, MonadIO n, Eq a, Show a) => Way -> MemType -> ConcT n a -> n Bool

-- | Variant of <a>dejafu</a> which takes a way to run the program and a
--   memory model.
--   
--   <pre>
--   &gt;&gt;&gt; import System.Random
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; dejafuWay (randomly (mkStdGen 0) 100) defaultMemType "Randomly!" alwaysSame example
--   [fail] Randomly!
--       "hello" S0----S1--S0--
--   
--       "world" S0----S2--S0--
--   False
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; dejafuWay (randomly (mkStdGen 1) 100) defaultMemType "Randomly!" alwaysSame example
--   [fail] Randomly!
--       "hello" S0----S1--S0--
--   
--       "world" S0----S2--S1-S0--
--   False
--   </pre>
dejafuWay :: (MonadConc n, MonadIO n, Show b) => Way -> MemType -> String -> ProPredicate a b -> ConcT n a -> n Bool

-- | Variant of <a>dejafus</a> which takes a way to run the program and a
--   memory model.
--   
--   <pre>
--   &gt;&gt;&gt; dejafusWay defaultWay SequentialConsistency [("A", alwaysSame), ("B", exceptionsNever)] relaxed
--   [fail] A
--       (False,True) S0---------S1----S0--S2----S0--
--   
--       (True,True) S0---------S1-P2----S1---S0---
--   
--       (True,False) S0---------S2----S1----S0---
--   [pass] B
--   False
--   </pre>
dejafusWay :: (MonadConc n, MonadIO n, Show b) => Way -> MemType -> [(String, ProPredicate a b)] -> ConcT n a -> n Bool

-- | Variant of <a>autocheck</a> which takes a settings record.
--   
--   <pre>
--   &gt;&gt;&gt; autocheckWithSettings (fromWayAndMemType defaultWay defaultMemType) relaxed
--   [pass] Successful
--   [fail] Deterministic
--       (False,True) S0---------S1----S0--S2----S0--
--   
--       (False,False) S0---------S1--P2----S1--S0---
--   
--       (True,False) S0---------S2----S1----S0---
--   
--       (True,True) S0---------S1-C-S2----S1---S0---
--   False
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; autocheckWithSettings (fromWayAndMemType defaultWay SequentialConsistency) relaxed
--   [pass] Successful
--   [fail] Deterministic
--       (False,True) S0---------S1----S0--S2----S0--
--   
--       (True,True) S0---------S1-P2----S1---S0---
--   
--       (True,False) S0---------S2----S1----S0---
--   False
--   </pre>
autocheckWithSettings :: (MonadConc n, MonadIO n, Eq a, Show a) => Settings n a -> ConcT n a -> n Bool

-- | Variant of <a>dejafu</a> which takes a settings record.
--   
--   <pre>
--   &gt;&gt;&gt; import System.Random
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; dejafuWithSettings (fromWayAndMemType (randomly (mkStdGen 1) 100) defaultMemType) "Randomly!" alwaysSame example
--   [fail] Randomly!
--       "hello" S0----S1--S0--
--   
--       "world" S0----S2--S1-S0--
--   False
--   </pre>
dejafuWithSettings :: (MonadConc n, MonadIO n, Show b) => Settings n a -> String -> ProPredicate a b -> ConcT n a -> n Bool

-- | Variant of <a>dejafus</a> which takes a settings record.
--   
--   <pre>
--   &gt;&gt;&gt; dejafusWithSettings (fromWayAndMemType defaultWay SequentialConsistency) [("A", alwaysSame), ("B", exceptionsNever)] relaxed
--   [fail] A
--       (False,True) S0---------S1----S0--S2----S0--
--   
--       (True,True) S0---------S1-P2----S1---S0---
--   
--       (True,False) S0---------S2----S1----S0---
--   [pass] B
--   False
--   </pre>
dejafusWithSettings :: (MonadConc n, MonadIO n, Show b) => Settings n a -> [(String, ProPredicate a b)] -> ConcT n a -> n Bool

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

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

-- | 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.
--   
--   The <tt>Eq</tt>, <tt>Ord</tt>, and <tt>NFData</tt> instances
--   compare/evaluate the exception with <tt>show</tt> in the
--   <tt>UncaughtException</tt> case.
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

-- | Every thread is blocked, and the main thread is <i>not</i> blocked in
--   an STM transaction.
Deadlock :: Failure

-- | Every thread is blocked, and the main thread is blocked in an STM
--   transaction.
STMDeadlock :: Failure

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

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

-- | A call to <tt>dontCheck</tt> was attempted after the first action of
--   the initial thread.
IllegalDontCheck :: Failure

-- | Run a predicate over all executions within the default schedule
--   bounds.
--   
--   The exact executions tried, and the order in which results are found,
--   is unspecified and may change between releases. This may affect which
--   failing traces are reported, when there is a failure.
runTest :: MonadConc n => ProPredicate a b -> ConcT n a -> n (Result b)

-- | Variant of <a>runTest</a> which takes a way to run the program and a
--   memory model.
--   
--   The exact executions tried, and the order in which results are found,
--   is unspecified and may change between releases. This may affect which
--   failing traces are reported, when there is a failure.
runTestWay :: MonadConc n => Way -> MemType -> ProPredicate a b -> ConcT n a -> n (Result b)

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

-- | A <tt>ProPredicate</tt> is a function which collapses a list of
--   results into a <a>Result</a>, possibly discarding some on the way.
data ProPredicate a b
ProPredicate :: Either Failure a -> Maybe Discard -> [(Either Failure a, Trace)] -> Result b -> ProPredicate a b

-- | Selectively discard results before computing the result.
[pdiscard] :: ProPredicate a b -> Either Failure a -> Maybe Discard

-- | Compute the result with the un-discarded results.
[peval] :: ProPredicate a b -> [(Either Failure a, Trace)] -> Result b

-- | Check that a computation never fails.
successful :: Predicate a

-- | Check that a computation always gives the same, successful, result.
--   
--   <pre>
--   alwaysSame = alwaysSameBy (==)
--   </pre>
alwaysSame :: Eq a => Predicate a

-- | Check that a computation never fails, and gives multiple distinct
--   successful results.
--   
--   <pre>
--   notAlwaysSame = notAlwaysSameBy (==)
--   </pre>
notAlwaysSame :: Eq a => Predicate a

-- | Check that a computation never aborts.
--   
--   Any result other than an abort, including other <a>Failure</a>s, is
--   allowed.
abortsNever :: Predicate a

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

-- | Check that a computation aborts at least once.
--   
--   Any result other than an abort, including other <a>Failure</a>s, is
--   allowed.
abortsSometimes :: Predicate a

-- | Check that a computation never deadlocks.
--   
--   Any result other than a deadlock, including other <a>Failure</a>s, is
--   allowed.
deadlocksNever :: Predicate a

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

-- | Check that a computation deadlocks at least once.
--   
--   Any result other than a deadlock, including other <a>Failure</a>s, is
--   allowed.
deadlocksSometimes :: Predicate a

-- | Check that a computation never fails with an uncaught exception.
--   
--   Any result other than an uncaught exception, including other
--   <a>Failure</a>s, is allowed.
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.
--   
--   Any result other than an uncaught exception, including other
--   <a>Failure</a>s, is allowed.
exceptionsSometimes :: Predicate a

-- | Reduce the list of failures in a <tt>ProPredicate</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 b => ProPredicate a b -> ProPredicate a b

-- | Check that a computation always gives the same (according to the
--   provided function), successful, result.
--   
--   <pre>
--   alwaysSameOn = alwaysSameBy ((==) `on` f)
--   </pre>
alwaysSameOn :: Eq b => (a -> b) -> Predicate a

-- | Check that the result of a computation is always the same, using some
--   transformation on results.
alwaysSameBy :: (a -> a -> Bool) -> Predicate a

-- | Check that a computation never fails, and gives multiple distinct
--   (according to the provided function) successful results.
--   
--   <pre>
--   notAlwaysSameOn = notAlwaysSameBy ((==) `on` f)
--   </pre>
notAlwaysSameOn :: Eq b => (a -> b) -> Predicate a

-- | Check that a computation never fails, and gives multiple distinct
--   successful results, by applying a transformation on results.
--   
--   This inverts the condition, so (eg) <tt>notAlwaysSameBy (==)</tt> will
--   pass if there are unequal results.
notAlwaysSameBy :: (a -> a -> Bool) -> 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 unary boolean predicate is true at least
--   once.
somewhereTrue :: (Either Failure a -> Bool) -> Predicate a

-- | Check that a <tt>Maybe</tt>-producing function always returns
--   <a>Nothing</a>.
alwaysNothing :: (Either Failure a -> Maybe (Either Failure b)) -> ProPredicate a b

-- | Check that a <tt>Maybe</tt>-producing function returns <a>Nothing</a>
--   at least once.
somewhereNothing :: (Either Failure a -> Maybe (Either Failure b)) -> ProPredicate a b

-- | 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

-- | Check if a failure is an <tt>InternalError</tt>.
isInternalError :: Failure -> Bool

-- | Check if a failure is an <tt>Abort</tt>.
isAbort :: Failure -> Bool

-- | Check if a failure is a <tt>Deadlock</tt> or an <tt>STMDeadlock</tt>.
isDeadlock :: Failure -> Bool

-- | Check if a failure is an <tt>UncaughtException</tt>
isUncaughtException :: Failure -> Bool

-- | Check if a failure is an <tt>IllegalSubconcurrency</tt>
isIllegalSubconcurrency :: Failure -> Bool

-- | Check if a failure is an <tt>IllegalDontCheck</tt>
isIllegalDontCheck :: Failure -> Bool

-- | Variant of <a>dejafuWay</a> which can selectively discard results.
--   
--   <pre>
--   &gt;&gt;&gt; dejafuDiscard (\_ -&gt; Just DiscardTrace) defaultWay defaultMemType "Discarding" alwaysSame example
--   [fail] Discarding
--       "hello" &lt;trace discarded&gt;
--   
--       "world" &lt;trace discarded&gt;
--   False
--   </pre>

-- | <i>Deprecated: Use dejafuWithSettings instead</i>
dejafuDiscard :: (MonadConc n, MonadIO n, Show b) => (Either Failure a -> Maybe Discard) -> Way -> MemType -> String -> ProPredicate a b -> ConcT n a -> n Bool
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 Data.Profunctor.Unsafe.Profunctor Test.DejaFu.ProPredicate
instance GHC.Base.Functor (Test.DejaFu.ProPredicate x)
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
