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


-- | Deja Fu support for the Tasty test framework.
--   
--   Integration between the <a>dejafu</a> library for concurrency testing
--   and <a>tasty</a>. This lets you easily incorporate concurrency testing
--   into your existing test suites.
@package tasty-dejafu
@version 0.6.0.0


-- | This module allows using Deja Fu predicates with Tasty to test the
--   behaviour of concurrent systems.
module Test.Tasty.DejaFu

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

-- | Check that a predicate holds.
testDejafu :: Show a => (forall t. ConcST t a) -> TestName -> Predicate a -> TestTree

-- | Variant of <a>testDejafu</a> which takes a collection of predicates to
--   test. This will share work between the predicates, rather than running
--   the concurrent computation many times for each predicate.
testDejafus :: Show a => (forall t. ConcST t a) -> [(TestName, Predicate a)] -> TestTree

-- | Variant of <a>testAuto</a> which tests a computation under a given
--   execution way and memory model.
testAutoWay :: (Eq a, Show a) => Way -> MemType -> (forall t. ConcST t a) -> TestTree

-- | Variant of <a>testDejafu</a> which takes a way to execute the program
--   and a memory model.
testDejafuWay :: Show a => Way -> MemType -> (forall t. ConcST t a) -> TestName -> Predicate a -> TestTree

-- | Variant of <a>testDejafus</a> which takes a way to execute the program
--   and a memory model.
testDejafusWay :: Show a => Way -> MemType -> (forall t. ConcST t a) -> [(TestName, Predicate a)] -> TestTree

-- | Variant of <a>testAuto</a> for computations which do <a>IO</a>.
testAutoIO :: (Eq a, Show a) => ConcIO a -> TestTree

-- | Variant of <a>testDejafu</a> for computations which do <a>IO</a>.
testDejafuIO :: Show a => ConcIO a -> TestName -> Predicate a -> TestTree

-- | Variant of <a>testDejafus</a> for computations which do <a>IO</a>.
testDejafusIO :: Show a => ConcIO a -> [(TestName, Predicate a)] -> TestTree

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

-- | Variant of <a>testDejafuWay</a> for computations which do <a>IO</a>.
testDejafuWayIO :: Show a => Way -> MemType -> ConcIO a -> TestName -> Predicate a -> TestTree

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

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

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

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

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

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

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

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

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

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

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

-- | Each thread has a write buffer. A thread sees its writes immediately,
--   but other threads will only see writes when they are committed, which
--   may happen later. Writes are committed in the same order that they are
--   created.
TotalStoreOrder :: MemType

-- | Each <tt>CRef</tt> has a write buffer. A thread sees its writes
--   immediately, but other threads will only see writes when they are
--   committed, which may happen later. Writes to different <tt>CRef</tt>s
--   are not necessarily committed in the same order that they are created.
PartialStoreOrder :: MemType

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

-- | Check a refinement property with a variety of seed values and variable
--   assignments.
testProperty :: (Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) => TestName -> p -> TestTree

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

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

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

-- | 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
instance Data.Typeable.Internal.Typeable t => Test.Tasty.Core.IsTest (Test.DejaFu.Conc.ConcST t (GHC.Base.Maybe GHC.Base.String))
instance Test.Tasty.Core.IsTest (Test.DejaFu.Conc.ConcIO (GHC.Base.Maybe GHC.Base.String))
instance Test.Tasty.Options.IsOption Test.DejaFu.Common.MemType
instance Test.Tasty.Options.IsOption Test.DejaFu.SCT.Way
instance Test.Tasty.Core.IsTest Test.Tasty.DejaFu.ConcTest
instance Test.Tasty.Core.IsTest Test.Tasty.DejaFu.ConcIOTest
instance Test.Tasty.Core.IsTest Test.Tasty.DejaFu.PropTest
