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


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


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

-- | Automatically test a computation. In particular, look for deadlocks,
--   uncaught exceptions, and multiple return values.
testAuto :: (Eq a, Show a) => ConcIO a -> Test

-- | Check that a predicate holds.
testDejafu :: Show b => String -> ProPredicate a b -> ConcIO a -> Test

-- | 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 b => [(String, ProPredicate a b)] -> ConcIO a -> Test

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

-- | Variant of <a>testDejafu</a> which takes a way to execute the program
--   and a memory model.
testDejafuWay :: Show b => Way -> MemType -> String -> ProPredicate a b -> ConcIO a -> Test

-- | Variant of <a>testDejafus</a> which takes a way to execute the program
--   and a memory model.
testDejafusWay :: Show b => Way -> MemType -> [(String, ProPredicate a b)] -> ConcIO a -> Test

-- | Variant of <a>testAuto</a> which takes a settings record.
testAutoWithSettings :: (Eq a, Show a) => Settings IO a -> ConcIO a -> Test

-- | Variant of <a>testDejafu</a> which takes a settings record.
testDejafuWithSettings :: Show b => Settings IO a -> String -> ProPredicate a b -> ConcIO a -> Test

-- | Variant of <a>testDejafus</a> which takes a settings record.
testDejafusWithSettings :: Show b => Settings IO a -> [(String, ProPredicate a b)] -> ConcIO a -> Test

-- | 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 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)) => String -> p -> Test

-- | Like <a>testProperty</a>, but takes a number of cases to check.
--   
--   The maximum number of cases tried by <tt>testPropertyFor n m</tt> will
--   be <tt>n * m</tt>.
testPropertyFor :: (Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) => Int -> Int -> String -> p -> Test

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

-- | Variant of <a>testDejafuWay</a> which can selectively discard results.

-- | <i>Deprecated: Use testDejafuWithSettings instead</i>
testDejafuDiscard :: Show b => (Either Failure a -> Maybe Discard) -> Way -> MemType -> String -> ProPredicate a b -> ConcIO a -> Test

-- | Variant of <a>testDejafusWay</a> which can selectively discard
--   results, beyond what each predicate already discards.

-- | <i>Deprecated: Use testDejafusWithSettings instead</i>
testDejafusDiscard :: Show b => (Either Failure a -> Maybe Discard) -> Way -> MemType -> [(String, ProPredicate a b)] -> ConcIO a -> Test
instance Test.HUnit.Base.Testable (Test.DejaFu.Conc.ConcIO ())
instance Test.HUnit.Base.Assertable (Test.DejaFu.Conc.ConcIO ())
