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


-- | Test monadic programs using state machine based models
--   
--   See README at
--   <a>https://github.com/advancedtelematic/quickcheck-state-machine#readme</a>
@package quickcheck-state-machine
@version 0.0.0


-- | This module exports some QuickCheck utility functions. Some of these
--   should perhaps be upstreamed.
module Test.StateMachine.Internal.Utils

-- | The type of a shrinker function.
type Shrinker a = a -> [a]

-- | Keep generating until we actually get a value.
genFromMaybe :: StateT s (StateT t Gen) (Maybe a) -> StateT s (StateT t Gen) a

-- | Lifts <a>any</a> to properties.
anyP :: (a -> Property) -> [a] -> Property

-- | Lifts a plain property into a monadic property.
liftProperty :: Monad m => Property -> PropertyM m ()

-- | Write a metaproperty on the output of QuickChecking a property using a
--   boolean predicate on the output.
shrinkPropertyHelper :: Property -> (String -> Bool) -> Property

-- | Same as above, but using a property predicate.
shrinkPropertyHelper' :: Property -> (String -> Property) -> Property

-- | Given shrinkers for the components of a pair we can shrink the pair.
shrinkPair :: Shrinker a -> Shrinker b -> Shrinker (a, b)


-- | This module provides internal refereces.
module Test.StateMachine.Internal.Types.IntRef

-- | An internal (or integer) reference consists of a reference and a
--   process id.
data IntRef
IntRef :: Ref -> Pid -> IntRef

-- | A process id is merely a natural number that keeps track of which
--   thread the reference comes from. In the sequential case the process id
--   is always <tt>0</tt>. Likewise the sequential prefix of a parallel
--   program also has process id <tt>0</tt>, while the left suffix has
--   process id <tt>1</tt>, and then right suffix has process id
--   <tt>2</tt>.
newtype Pid
Pid :: Int -> Pid

-- | A reference is natural number.
newtype Ref
Ref :: Int -> Ref

-- | Type-level function that constantly returns an internal reference.
type ConstIntRef = ConstSym1 IntRef
showRef :: IntRef -> String
instance GHC.Read.Read Test.StateMachine.Internal.Types.IntRef.IntRef
instance GHC.Show.Show Test.StateMachine.Internal.Types.IntRef.IntRef
instance GHC.Classes.Ord Test.StateMachine.Internal.Types.IntRef.IntRef
instance GHC.Classes.Eq Test.StateMachine.Internal.Types.IntRef.IntRef
instance GHC.Num.Num Test.StateMachine.Internal.Types.IntRef.Ref
instance GHC.Read.Read Test.StateMachine.Internal.Types.IntRef.Ref
instance GHC.Show.Show Test.StateMachine.Internal.Types.IntRef.Ref
instance GHC.Classes.Ord Test.StateMachine.Internal.Types.IntRef.Ref
instance GHC.Classes.Eq Test.StateMachine.Internal.Types.IntRef.Ref
instance GHC.Num.Num Test.StateMachine.Internal.Types.IntRef.Pid
instance GHC.Read.Read Test.StateMachine.Internal.Types.IntRef.Pid
instance GHC.Show.Show Test.StateMachine.Internal.Types.IntRef.Pid
instance GHC.Classes.Ord Test.StateMachine.Internal.Types.IntRef.Pid
instance GHC.Classes.Eq Test.StateMachine.Internal.Types.IntRef.Pid


-- | This module contains the main types exposed to the user. The module is
--   perhaps best read indirectly, on a per need basis, via the main module
--   <a>Test.StateMachine</a>.
module Test.StateMachine.Types

-- | A state machine based model.
data StateMachineModel model cmd
StateMachineModel :: (forall refs resp. IxForallF Ord refs => model refs -> cmd refs resp -> Bool) -> (forall refs resp. IxForallF Ord refs => model refs -> cmd refs resp -> Response_ refs resp -> Property) -> (forall refs resp. IxForallF Ord refs => model refs -> cmd refs resp -> Response_ refs resp -> model refs) -> (forall refs. model refs) -> StateMachineModel model cmd
[precondition] :: StateMachineModel model cmd -> forall refs resp. IxForallF Ord refs => model refs -> cmd refs resp -> Bool
[postcondition] :: StateMachineModel model cmd -> forall refs resp. IxForallF Ord refs => model refs -> cmd refs resp -> Response_ refs resp -> Property
[transition] :: StateMachineModel model cmd -> forall refs resp. IxForallF Ord refs => model refs -> cmd refs resp -> Response_ refs resp -> model refs
[initialModel] :: StateMachineModel model cmd -> forall refs. model refs

-- | Given a command, how can we show it?
class ShowCmd (cmd :: Signature ix)

-- | How to show a typed command with internal refereces.
showCmd :: forall resp. ShowCmd cmd => cmd (ConstSym1 String) resp -> String

-- | How to show a typed command with internal refereces.
showCmd :: forall resp. ShowCmd cmd => cmd (ConstSym1 String) resp -> String

-- | Signatures of commands contain a family of references and a response
--   type.
type Signature ix = (TyFun ix Type -> Type) -> Response ix -> Type

-- | A response of a command is either of some type or a referece at some
--   index.
data Response ix
Response :: Type -> Response ix
Reference :: ix -> Response ix

-- | The singleton type of responses.
data SResponse ix :: Response ix -> Type
[SResponse] :: SResponse ix (Response t)
[SReference] :: Sing (i :: ix) -> SResponse ix (Reference i)

-- | Type-level function that returns a response type.

-- | Type-level function that maybe returns a response.

-- | Given a command, what kind of response does it have?
class HasResponse cmd

-- | What type of response a typed command has.
response :: HasResponse cmd => cmd refs resp -> SResponse ix resp

-- | What type of response a typed command has.
response :: HasResponse cmd => cmd refs resp -> SResponse ix resp

-- | The constraints on commands (and their indices) that the
--   <a>sequentialProperty</a> and <a>parallelProperty</a> helpers require.
type CommandConstraint ix cmd = (Ord ix, SDecide ix, SingKind ix, DemoteRep ix ~ ix, ShowCmd cmd, IxTraversable cmd, HasResponse cmd)

-- | Untyped commands are command where we hide the response type. This is
--   used in generation of commands.
data Untyped (f :: Signature ix) refs
[Untyped] :: (Show (GetResponse_ resp), Typeable (Response_ ConstIntRef resp), Typeable resp) => f refs resp -> Untyped f refs

-- | When generating commands it is enough to provide a reference
--   placeholder.
data RefPlaceholder ix :: (TyFun ix k) -> Type

-- | Dependent pairs.
data Ex (p :: TyFun a Type -> Type)
Ex :: (Sing x) -> (p @@ x) -> Ex

-- | Predicate transformers.
class IxFunctor (f :: (TyFun ix Type -> Type) -> jx -> Type)

-- | Indexed <a>fmap</a>.
ifmap :: forall p q j. IxFunctor f => (forall i. Sing (i :: ix) -> p @@ i -> q @@ i) -> f p j -> f q j

-- | Indexed <a>fmap</a>.
ifmap :: forall p q j. IxFunctor f => (forall i. Sing (i :: ix) -> p @@ i -> q @@ i) -> f p j -> f q j

-- | Foldable for predicate transformers.
class IxFoldable (t :: (TyFun ix Type -> Type) -> jx -> Type) where itoList = ifoldMap (\ s px -> [Ex s px]) ifoldr f z = foldr (\ (Ex i x) -> f i x) z . itoList iany p = ifoldr (\ i x ih -> p i x || ih) False

-- | Indexed <a>foldMap</a>.
ifoldMap :: (IxFoldable t, Monoid m) => (forall i. Sing (i :: ix) -> p @@ i -> m) -> t p j -> m

-- | Indexed <tt>toList</tt>.
itoList :: IxFoldable t => t p j -> [Ex p]

-- | Indexed <a>any</a>.
iany :: IxFoldable t => (forall i. Sing (i :: ix) -> p @@ i -> Bool) -> t p j -> Bool

-- | Indexed <a>foldMap</a>.
ifoldMap :: (IxFoldable t, Monoid m) => (forall i. Sing (i :: ix) -> p @@ i -> m) -> t p j -> m

-- | Indexed <tt>toList</tt>.
itoList :: IxFoldable t => t p j -> [Ex p]

-- | Indexed <a>any</a>.
iany :: IxFoldable t => (forall i. Sing (i :: ix) -> p @@ i -> Bool) -> t p j -> Bool

-- | Tranversable for predicate transformers.
class (IxFunctor t, IxFoldable t) => IxTraversable (t :: (TyFun ix Type -> Type) -> jx -> Type) where itraverse pq f tp = ifor pq tp f ifor pq tp f = itraverse pq f tp

-- | Indexed traverse function.
itraverse :: (IxTraversable t, Applicative f) => Proxy q -> (forall x. Sing x -> p @@ x -> f (q @@ x)) -> t p j -> f (t q j)

-- | Same as above, with arguments flipped.
ifor :: (IxTraversable t, Applicative f) => Proxy q -> t p j -> (forall x. Sing x -> p @@ x -> f (q @@ x)) -> f (t q j)

-- | Indexed traverse function.
itraverse :: (IxTraversable t, Applicative f) => Proxy q -> (forall x. Sing x -> p @@ x -> f (q @@ x)) -> t p j -> f (t q j)

-- | Same as above, with arguments flipped.
ifor :: (IxTraversable t, Applicative f) => Proxy q -> t p j -> (forall x. Sing x -> p @@ x -> f (q @@ x)) -> f (t q j)

-- | Indexed variant of <a>ForallF</a>.
class Forall (IxComposeC p f) => IxForallF (p :: k2 -> Constraint) (f :: TyFun k1 k2 -> Type)

-- | Type alias that is helpful when defining state machine models.
type Ords refs = IxForallF Ord refs :- Ord (refs @@ ())

-- | Same as the above.
type Ords' refs i = IxForallF Ord refs :- Ord (refs @@ i)

-- | Indexed variant of <a>instF</a>.
iinstF :: forall a p f. Proxy a -> IxForallF p f :- p (f @@ a)

-- | Given that <tt>a :- b</tt>, derive something that needs a context
--   <tt>b</tt>, using the context <tt>a</tt>
(\\) :: a => (b -> r) -> (:-) a b -> r
infixl 1 \\

-- | An infix synonym for <a>Apply</a>
type (@@) k1 k2 (a :: (~>) k1 k2) (b :: k1) = Apply k1 k2 a b

-- | The type of properties.
data Property :: *

-- | Convert the thing to a property.
property :: Testable prop => prop -> Property

-- | A concrete, poly-kinded proxy type
data Proxy k (t :: k) :: forall k. k -> *
Proxy :: Proxy k
instance forall k1 k2 (p :: k2 -> GHC.Types.Constraint) (f :: k1 Data.Singletons.~> k2) (a :: k1). p (f Data.Singletons.@@ a) => Test.StateMachine.Types.IxComposeC p f a
instance forall k1 k2 (p :: k2 -> GHC.Types.Constraint) (f :: Data.Singletons.TyFun k1 k2 -> GHC.Types.Type). Data.Constraint.Forall.Forall (Test.StateMachine.Types.IxComposeC p f) => Test.StateMachine.Types.IxForallF p f


-- | This module exports some types that are used internally by the
--   library.
module Test.StateMachine.Internal.Types

-- | An internal (or integer) reference consists of a reference and a
--   process id.
data IntRef
IntRef :: Ref -> Pid -> IntRef

-- | A process id is merely a natural number that keeps track of which
--   thread the reference comes from. In the sequential case the process id
--   is always <tt>0</tt>. Likewise the sequential prefix of a parallel
--   program also has process id <tt>0</tt>, while the left suffix has
--   process id <tt>1</tt>, and then right suffix has process id
--   <tt>2</tt>.
newtype Pid
Pid :: Int -> Pid

-- | A reference is natural number.
newtype Ref
Ref :: Int -> Ref

-- | Type-level function that constantly returns an internal reference.
type ConstIntRef = ConstSym1 IntRef

-- | Internal untyped commands.
data IntRefed (f :: Signature ix)
[IntRefed] :: (Show (GetResponse_ resp), Typeable (Response_ ConstIntRef resp), Typeable resp) => f ConstIntRef resp -> MayResponse_ ConstIntRef resp -> IntRefed f

-- | Forks are used to represent parallel programs. They have a sequential
--   prefix (the middle argument of the constructor), and two parallel
--   suffixes (the left- and right-most argument of the constructor).
data Fork a
Fork :: a -> a -> a -> Fork a

-- | Show function for <a>Response_</a>.
showResponse_ :: Show (GetResponse_ resp) => SResponse ix resp -> Response_ ConstIntRef resp -> String

-- | Type-level function that maybe returns a reference.
instance GHC.Read.Read a => GHC.Read.Read (Test.StateMachine.Internal.Types.Fork a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Test.StateMachine.Internal.Types.Fork a)
instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.Internal.Types.Fork a)
instance GHC.Base.Functor Test.StateMachine.Internal.Types.Fork
instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.StateMachine.Internal.Types.Fork a)
instance forall ix (cmd :: (Data.Singletons.TyFun ix GHC.Types.Type -> GHC.Types.Type) -> Test.StateMachine.Types.Response ix -> GHC.Types.Type). (Test.StateMachine.Types.IxFunctor cmd, Test.StateMachine.Types.ShowCmd cmd, Test.StateMachine.Types.HasResponse cmd) => GHC.Show.Show (Test.StateMachine.Internal.Types.IntRefed cmd)
instance Text.PrettyPrint.ANSI.Leijen.Pretty a => Text.PrettyPrint.ANSI.Leijen.Pretty (Test.StateMachine.Internal.Types.Fork a)


-- | This module contains functions for drawing the history for the
--   <a>parallelProperty</a>.
module Test.StateMachine.Internal.Utils.BoxDrawer
data EventType
Open :: EventType
Close :: EventType

-- | Given a history, and output from processes generate Doc with boxes
exec :: [(EventType, Pid)] -> Fork [String] -> Doc
instance GHC.Show.Show Test.StateMachine.Internal.Utils.BoxDrawer.EventType


-- | This module provides scope-checking for internal commands. This
--   functionality isn't used anywhere in the library, but can be useful
--   for writing <a>metaproperties</a>.
module Test.StateMachine.Internal.ScopeCheck

-- | Scope-check a list of untyped internal commands, i.e. make sure that
--   no command uses a reference that doesn't exist.
scopeCheck :: forall cmd. (IxFoldable cmd, HasResponse cmd) => [IntRefed cmd] -> Bool

-- | Same as above, but for forks rather than lists.
scopeCheckFork :: (IxFoldable cmd, HasResponse cmd) => Fork [IntRefed cmd] -> Bool


-- | This module provides indexed maps. These are used to implement support
--   for multiple references.
module Test.StateMachine.Internal.IxMap

-- | An <tt>ix</tt>-indexed family of maps.
data IxMap (ix :: Type) (k :: Type) (vs :: TyFun ix Type -> Type)

-- | The empty map.
empty :: IxMap i k vs

-- | Partial lookup function.
(!) :: Ord k => IxMap ix k vs -> (Sing i, k) -> vs @@ i

-- | Total version of the above.
lookup :: Ord k => Sing i -> k -> IxMap ix k vs -> Maybe (vs @@ i)

-- | Key membership check.
member :: Ord k => Sing (i :: ix) -> k -> IxMap ix k vs -> Bool

-- | Map insertion.
insert :: (Ord k, SDecide ix) => Sing i -> k -> vs @@ i -> IxMap ix k vs -> IxMap ix k vs

-- | Size of the key set.
size :: Sing (i :: ix) -> IxMap ix k vs -> Int


-- | This module contains the building blocks needed to implement the
--   <a>sequentialProperty</a> helper.
module Test.StateMachine.Internal.Sequential

-- | Lift a generator of untyped commands with reference placeholders into
--   a generator of lists of untyped internal commands.
liftGen :: forall ix cmd. Ord ix => SingKind ix => DemoteRep ix ~ ix => IxTraversable cmd => HasResponse cmd => Gen (Untyped cmd (RefPlaceholder ix)) -> Pid -> Map ix Int -> Gen ([IntRefed cmd], Map ix Int)

-- | Same as the above, but for stateful generators.
liftGen' :: forall ix cmd genState. Ord ix => SingKind ix => DemoteRep ix ~ ix => IxTraversable cmd => HasResponse cmd => StateT genState Gen (Untyped cmd (RefPlaceholder ix)) -> genState -> Pid -> Map ix Int -> Gen (([IntRefed cmd], genState), Map ix Int)

-- | A shrinker of typed commands can be lifted to a shrinker of untyped
--   commands.
liftShrinker :: (forall resp. Shrinker (cmd ConstIntRef resp)) -> Shrinker (IntRefed cmd)

-- | Lift a shrinker of internal commands into a shrinker of lists of
--   untyped internal commands.
liftShrink :: IxFoldable cmd => HasResponse cmd => (forall resp. Shrinker (cmd ConstIntRef resp)) -> Shrinker [IntRefed cmd]

-- | Lift semantics of typed commands with external references, into
--   semantics for typed commands with internal references.
liftSem :: forall ix cmd refs resp m. SDecide ix => Monad m => IxFunctor cmd => HasResponse cmd => (cmd refs resp -> m (Response_ refs resp)) -> cmd ConstIntRef resp -> MayResponse_ ConstIntRef resp -> StateT (IxMap ix IntRef refs) m (Response_ ConstIntRef resp)

-- | Remove commands that uses a reference.
removeCommands :: forall cmd. IxFoldable cmd => HasResponse cmd => IntRefed cmd -> [IntRefed cmd] -> [IntRefed cmd]

-- | Collects length statistics about the input list.
collectStats :: [a] -> Property -> Property

-- | Check that the pre- and post-conditions hold in a sequential way.
checkSequentialInvariant :: ShowCmd cmd => Monad m => SDecide ix => IxFunctor cmd => Show (model ConstIntRef) => HasResponse cmd => StateMachineModel model cmd -> model ConstIntRef -> (forall resp. model ConstIntRef -> MayResponse_ ConstIntRef resp -> cmd refs resp -> m (Response_ refs resp)) -> [IntRefed cmd] -> PropertyM (StateT (IxMap ix IntRef refs) m) ()


-- | This module contains the building blocks needed to implement the
--   <a>parallelProperty</a> helper.
module Test.StateMachine.Internal.Parallel

-- | Lift a generator of untyped commands with reference placeholders into
--   a generator of forks of untyped internal commands.
liftGenFork :: Ord ix => SingKind ix => DemoteRep ix ~ ix => IxTraversable cmd => HasResponse cmd => Gen (Untyped cmd (RefPlaceholder ix)) -> Gen (Fork [IntRefed cmd])
liftGenFork' :: Ord ix => SingKind ix => DemoteRep ix ~ ix => IxTraversable cmd => HasResponse cmd => StateT genState Gen (Untyped cmd (RefPlaceholder ix)) -> genState -> Gen (Fork [IntRefed cmd])

-- | Lift a shrinker of internal commands into a shrinker of forks of
--   untyped internal commands.
liftShrinkFork :: forall cmd. IxFoldable cmd => HasResponse cmd => (forall resp. Shrinker (cmd ConstIntRef resp)) -> Shrinker (Fork [IntRefed cmd])

-- | Lift the semantics of a single typed command into a semantics for
--   forks of untyped internal commands. The prefix of the fork is executed
--   sequentially, while the two suffixes are executed in parallel, and the
--   result (or trace) is collected in a so called history.
liftSemFork :: forall (ix :: Type) (cmd :: Signature ix) (refs :: TyFun ix Type -> Type). SDecide ix => IxFunctor cmd => HasResponse cmd => (forall resp. cmd refs resp -> IO (Response_ refs resp)) -> Fork [IntRefed cmd] -> IO (History cmd)

-- | Check if a history can be linearised.
checkParallelInvariant :: (ShowCmd cmd, IxFunctor cmd, HasResponse cmd) => StateMachineModel model cmd -> History cmd -> PropertyM IO ()
instance forall ix (cmd :: Test.StateMachine.Types.Signature ix). (Test.StateMachine.Types.ShowCmd cmd, Test.StateMachine.Types.IxFunctor cmd) => Text.PrettyPrint.ANSI.Leijen.Pretty (Test.StateMachine.Internal.Parallel.Operation cmd)


-- | This module provides &lt;math&gt;-equality for internal commands. This
--   functionality isn't used anywhere in the library, but can be useful
--   for writing <a>metaproperties</a>.
module Test.StateMachine.Internal.AlphaEquality

-- | Check if two lists of commands are equal modulo
--   &lt;math&gt;-conversion.
alphaEq :: forall ix (cmd :: Signature ix). SDecide ix => IxTraversable cmd => HasResponse cmd => Eq (IntRefed cmd) => [IntRefed cmd] -> [IntRefed cmd] -> Bool

-- | Check if two forks of commands are equal modulo
--   &lt;math&gt;-conversion.
alphaEqFork :: forall ix (cmd :: Signature ix). SDecide ix => IxTraversable cmd => HasResponse cmd => Eq (IntRefed cmd) => Fork [IntRefed cmd] -> Fork [IntRefed cmd] -> Bool


-- | The main module for state machine based testing.
module Test.StateMachine

-- | This function builds a property that tests if your model is agrees
--   with your semantics when running commands sequentially.
sequentialProperty :: CommandConstraint ix cmd => Monad m => Show (model ConstIntRef) => StateMachineModel model cmd -> Gen (Untyped cmd (RefPlaceholder ix)) -> (forall resp refs'. Shrinker (cmd refs' resp)) -> (forall resp. cmd refs resp -> m (Response_ refs resp)) -> (m Property -> Property) -> Property

-- | Same as above, except it provides more flexibility.
sequentialProperty' :: CommandConstraint ix cmd => Show (model ConstIntRef) => Monad m => StateMachineModel model cmd -> StateT s Gen (Untyped cmd (RefPlaceholder ix)) -> s -> (forall resp refs'. Shrinker (cmd refs' resp)) -> (forall resp. model ConstIntRef -> MayResponse_ ConstIntRef resp -> cmd refs resp -> m (Response_ refs resp)) -> (m Property -> Property) -> Property

-- | This function builds a property that tests your semantics for race
--   conditions, by runnings commands in parallel and then trying to
--   linearise the resulting history.
--   
--   <i>Note:</i> Make sure that your model passes the sequential property
--   first.
parallelProperty :: CommandConstraint ix cmd => StateMachineModel model cmd -> Gen (Untyped cmd (RefPlaceholder ix)) -> (forall resp refs'. Shrinker (cmd refs' resp)) -> (forall resp. cmd refs resp -> IO (Response_ refs resp)) -> Property
parallelProperty' :: CommandConstraint ix cmd => StateMachineModel model cmd -> StateT genState Gen (Untyped cmd (RefPlaceholder ix)) -> genState -> (forall resp refs'. Shrinker (cmd refs' resp)) -> (forall resp. cmd refs resp -> IO (Response_ refs resp)) -> IO () -> Property