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


-- | This module exports a higher-order version of functors, foldable
--   functors, and traversable functors.
module Test.StateMachine.Types.HFunctor

-- | Higher-order functors.
class HFunctor (f :: (* -> *) -> * -> *) where hfmap f = runIdentity . htraverse (Identity . f)

-- | Higher-order version of <a>fmap</a>.
hfmap :: HFunctor f => (forall a. g a -> h a) -> f g b -> f h b

-- | Higher-order version of <a>fmap</a>.
hfmap :: (HFunctor f, HTraversable f) => (forall a. g a -> h a) -> f g b -> f h b

-- | Higher-order version of <a>fmap</a>.
hfmap :: HFunctor f => (forall a. g a -> h a) -> f g b -> f h b

-- | Higher-order foldable functors.
class HFunctor t => HFoldable (t :: (* -> *) -> * -> *) where hfoldMap f = getConst . htraverse (Const . f)

-- | Higher-order version of <a>foldMap</a>.
hfoldMap :: (HFoldable t, Monoid m) => (forall a. v a -> m) -> t v b -> m

-- | Higher-order version of <a>foldMap</a>.
hfoldMap :: (HFoldable t, HTraversable t, Monoid m) => (forall a. v a -> m) -> t v b -> m

-- | Higher-order version of <a>foldMap</a>.
hfoldMap :: (HFoldable t, Monoid m) => (forall a. v a -> m) -> t v b -> m

-- | Higher-order traversable functors.
class (HFunctor t, HFoldable t) => HTraversable (t :: (* -> *) -> * -> *)

-- | Higher-order version of <a>traverse</a>.
htraverse :: (HTraversable t, Applicative f) => (forall a. g a -> f (h a)) -> t g b -> f (t h b)

-- | Higher-order version of <a>traverse</a>.
htraverse :: (HTraversable t, Applicative f) => (forall a. g a -> f (h a)) -> t g b -> f (t h b)


-- | This module contains reference related types. It's taken almost
--   verbatim from the Hedgehog <a>library</a>.
module Test.StateMachine.Types.References

-- | References are the potential or actual result of executing an action.
--   They are parameterised by either <a>Symbolic</a> or <a>Concrete</a>
--   depending on the phase of the test.
--   
--   <a>Symbolic</a> variables are the potential results of actions. These
--   are used when generating the sequence of actions to execute. They
--   allow actions which occur later in the sequence to make use of the
--   result of an action which came earlier in the sequence.
--   
--   <a>Concrete</a> variables are the actual results of actions. These are
--   used during test execution. They provide access to the actual runtime
--   value of a variable.
data Reference v a
Reference :: (v a) -> Reference v a

-- | Take the value from a concrete variable.
concrete :: Reference Concrete a -> a

-- | Take the value from an opaque concrete variable.
opaque :: Reference Concrete (Opaque a) -> a

-- | Opaque values.
--   
--   Useful if you want to put something without a <a>Show</a> instance
--   inside something which you'd like to be able to display.
newtype Opaque a
Opaque :: a -> Opaque a
[unOpaque] :: Opaque a -> a

-- | Symbolic values.
data Symbolic a
[Symbolic] :: Typeable a => Var -> Symbolic a

-- | Concrete values.
newtype Concrete a
[Concrete] :: a -> Concrete a

-- | Symbolic variable names.
newtype Var
Var :: Int -> Var
instance Data.Traversable.Traversable Test.StateMachine.Types.References.Concrete
instance Data.Foldable.Foldable Test.StateMachine.Types.References.Concrete
instance GHC.Base.Functor Test.StateMachine.Types.References.Concrete
instance GHC.Classes.Ord a => GHC.Classes.Ord (Test.StateMachine.Types.References.Concrete a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.StateMachine.Types.References.Concrete a)
instance GHC.Read.Read Test.StateMachine.Types.References.Var
instance GHC.Num.Num Test.StateMachine.Types.References.Var
instance GHC.Show.Show Test.StateMachine.Types.References.Var
instance GHC.Classes.Ord Test.StateMachine.Types.References.Var
instance GHC.Classes.Eq Test.StateMachine.Types.References.Var
instance GHC.Classes.Ord a => GHC.Classes.Ord (Test.StateMachine.Types.References.Opaque a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.StateMachine.Types.References.Opaque a)
instance GHC.Classes.Eq (Test.StateMachine.Types.References.Symbolic a)
instance GHC.Classes.Ord (Test.StateMachine.Types.References.Symbolic a)
instance (Data.Functor.Classes.Eq1 v, GHC.Classes.Eq a) => GHC.Classes.Eq (Test.StateMachine.Types.References.Reference v a)
instance (Data.Functor.Classes.Ord1 v, GHC.Classes.Ord a) => GHC.Classes.Ord (Test.StateMachine.Types.References.Reference v a)
instance (GHC.Show.Show a, Data.Functor.Classes.Show1 v) => GHC.Show.Show (Test.StateMachine.Types.References.Reference v a)
instance Test.StateMachine.Types.HFunctor.HTraversable Test.StateMachine.Types.References.Reference
instance Test.StateMachine.Types.HFunctor.HFunctor Test.StateMachine.Types.References.Reference
instance Test.StateMachine.Types.HFunctor.HFoldable Test.StateMachine.Types.References.Reference
instance GHC.Show.Show (Test.StateMachine.Types.References.Opaque a)
instance GHC.Show.Show (Test.StateMachine.Types.References.Symbolic a)
instance Data.Functor.Classes.Show1 Test.StateMachine.Types.References.Symbolic
instance Data.Typeable.Internal.Typeable a => GHC.Read.Read (Test.StateMachine.Types.References.Symbolic a)
instance Data.Functor.Classes.Eq1 Test.StateMachine.Types.References.Symbolic
instance Data.Functor.Classes.Ord1 Test.StateMachine.Types.References.Symbolic
instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.Types.References.Concrete a)
instance Data.Functor.Classes.Show1 Test.StateMachine.Types.References.Concrete
instance Data.Functor.Classes.Eq1 Test.StateMachine.Types.References.Concrete
instance Data.Functor.Classes.Ord1 Test.StateMachine.Types.References.Concrete


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

-- | An untyped action is an action where the response type is hidden away
--   using an existential type.
--   
--   We need to hide the response type when generating actions, because in
--   general the actions we want to generate will have different response
--   types; and thus we can only type the generating function if we hide
--   the response type.
data Untyped (act :: (* -> *) -> * -> *)
[Untyped] :: (Show resp, Typeable resp) => act Symbolic resp -> Untyped act

-- | When generating actions we have access to a model containing symbolic
--   references.
type Generator model act = model Symbolic -> Gen (Untyped act)

-- | Shrinking should preserve the response type of the action.
type Shrinker act = forall (v :: * -> *) resp. act v resp -> [act v resp]

-- | Pre-conditions are checked while generating, at this stage we do not
--   yet have access to concrete references.
type Precondition model act = forall resp. model Symbolic -> act Symbolic resp -> Bool

-- | The transition function must be polymorphic in the type of variables
--   used, as it is used both while generating and executing.
type Transition model act = forall resp v. Ord1 v => model v -> act v resp -> v resp -> model v

-- | When we execute our actions we have access to concrete references.
type Semantics act m = forall resp. act Concrete resp -> m resp

-- | Post-conditions are checked after the actions have been executed and
--   we got a response.
type Postcondition model act = forall resp. model Concrete -> act Concrete resp -> resp -> Property

-- | The initial model is polymorphic in the type of references it uses, so
--   that it can be used both in the pre- and the post-condition check.
type InitialModel m = forall (v :: * -> *). m v


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

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

-- | Same above, but for homogeneous pairs.
shrinkPair :: (a -> [a]) -> ((a, a) -> [(a, a)])

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


-- | This module contains environments that are used to translate between
--   symbolic and concrete references. It's taken verbatim from the
--   Hedgehog <a>library</a>.
module Test.StateMachine.Internal.Types.Environment

-- | A mapping of symbolic values to concrete values.
newtype Environment
Environment :: Map Var Dynamic -> Environment
[unEnvironment] :: Environment -> Map Var Dynamic

-- | Environment errors.
data EnvironmentError
EnvironmentValueNotFound :: !Var -> EnvironmentError
EnvironmentTypeError :: !TypeRep -> !TypeRep -> EnvironmentError

-- | Create an empty environment.
emptyEnvironment :: Environment

-- | Insert a symbolic / concrete pairing in to the environment.
insertConcrete :: Symbolic a -> Concrete a -> Environment -> Environment

-- | Cast a <a>Dynamic</a> in to a concrete value.
reifyDynamic :: forall a. Typeable a => Dynamic -> Either EnvironmentError (Concrete a)

-- | Turns an environment in to a function for looking up a concrete value
--   from a symbolic one.
reifyEnvironment :: Environment -> (forall a. Symbolic a -> Either EnvironmentError (Concrete a))

-- | Convert a symbolic structure to a concrete one, using the provided
--   environment.
reify :: HTraversable t => Environment -> t Symbolic b -> Either EnvironmentError (t Concrete b)
instance GHC.Show.Show Test.StateMachine.Internal.Types.Environment.EnvironmentError
instance GHC.Classes.Ord Test.StateMachine.Internal.Types.Environment.EnvironmentError
instance GHC.Classes.Eq Test.StateMachine.Internal.Types.Environment.EnvironmentError
instance GHC.Show.Show Test.StateMachine.Internal.Types.Environment.Environment


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

-- | A (sequential) program is an abstract datatype representing a list of
--   actions.
--   
--   The idea is that the user shows how to generate, shrink, execute and
--   modelcheck individual actions, and then the below combinators lift
--   those things to whole programs.
newtype Program act
Program :: [Internal act] -> Program act
[unProgram] :: Program act -> [Internal act]

-- | A parallel program is an abstract datatype that represents three
--   sequences of actions; a sequential prefix and two parallel suffixes.
--   Analogous to the sequential case, the user shows how to generate,
--   shrink, execute and modelcheck individual actions, and then the below
--   combinators lift those things to whole parallel programs.
newtype ParallelProgram act
ParallelProgram :: Fork (Program act) -> ParallelProgram act
[unParallelProgram] :: ParallelProgram act -> Fork (Program act)

-- | A process id.
newtype Pid
Pid :: Int -> Pid

-- | Forks are used to represent parallel programs.
data Fork a
Fork :: a -> a -> a -> Fork a

-- | An internal action is an action together with the symbolic variable
--   that will hold its result.
data Internal (act :: (* -> *) -> * -> *)
[Internal] :: (Show resp, Typeable resp) => act Symbolic resp -> Symbolic resp -> Internal act
instance GHC.Show.Show Test.StateMachine.Internal.Types.Pid
instance GHC.Classes.Eq Test.StateMachine.Internal.Types.Pid
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 GHC.Classes.Eq (Test.StateMachine.Internal.Types.Internal act) => GHC.Classes.Eq (Test.StateMachine.Internal.Types.Program act)
instance GHC.Base.Monoid (Test.StateMachine.Internal.Types.Program act)
instance (GHC.Show.Show (Test.StateMachine.Types.Untyped act), Test.StateMachine.Types.HFunctor.HFoldable act) => GHC.Show.Show (Test.StateMachine.Internal.Types.Program act)
instance GHC.Read.Read (Test.StateMachine.Internal.Types.Internal act) => GHC.Read.Read (Test.StateMachine.Internal.Types.Program act)
instance (GHC.Show.Show (Test.StateMachine.Types.Untyped act), Test.StateMachine.Types.HFunctor.HFoldable act) => GHC.Show.Show (Test.StateMachine.Internal.Types.ParallelProgram act)


-- | This module contains functions for visualing a history of a parallel
--   execution.
module Test.StateMachine.Internal.Utils.BoxDrawer

-- | Event invocation or response.
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 contains helpers for generating, shrinking, and checking
--   sequential programs.
module Test.StateMachine.Internal.Sequential

-- | Generate programs whose actions all respect their pre-conditions.
generateProgram :: forall model act. Generator model act -> Precondition model act -> Transition model act -> Int -> StateT (model Symbolic) Gen (Program act)

-- | Filter out invalid actions from a program. An action is invalid if
--   either its pre-condition doesn't hold, or it uses references that are
--   not in scope.
filterInvalid :: HFoldable act => Precondition model act -> Transition model act -> Program act -> State (model Symbolic, Set Var) (Program act)

-- | Returns the set of references an action uses.
getUsedVars :: HFoldable act => act Symbolic a -> Set Var

-- | Given a shrinker of typed actions we can lift it to a shrinker of
--   internal actions.
liftShrinkInternal :: Shrinker act -> (Internal act -> [Internal act])

-- | Shrink a program in a pre-condition and scope respecting way.
shrinkProgram :: HFoldable act => Shrinker act -> Precondition model act -> Transition model act -> model Symbolic -> Program act -> [Program act]

-- | For each action in a program, check that if the pre-condition holds
--   for the action, then so does the post-condition.
checkProgram :: Monad m => HFunctor act => Precondition model act -> Transition model act -> Postcondition model act -> model Symbolic -> model Concrete -> Semantics act m -> Program act -> PropertyM (StateT Environment m) ()


-- | This module provides scope-checking for internal actions. 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 program, i.e. make sure that no action uses a reference
--   that doesn't exist.
scopeCheck :: forall act. HFoldable act => Program act -> Bool

-- | Same as above, but for parallel programs.
scopeCheckParallel :: HFoldable act => ParallelProgram act -> Bool


-- | This module contains helpers for generating, shrinking, and checking
--   parallel programs.
module Test.StateMachine.Internal.Parallel

-- | Generate a parallel program whose actions all respect their
--   pre-conditions.
generateParallelProgram :: Generator model act -> Precondition model act -> Transition model act -> model Symbolic -> Gen (ParallelProgram act)

-- | Shrink a parallel program in a pre-condition and scope respecting way.
shrinkParallelProgram :: HFoldable act => Shrinker act -> Precondition model act -> Transition model act -> model Symbolic -> (ParallelProgram act -> [ParallelProgram act])

-- | Run a parallel program, by first executing the prefix sequentially and
--   then the suffixes in parallel, and return the history (or trace) of
--   the execution.
executeParallelProgram :: forall act. HTraversable act => Show (Untyped act) => Semantics act IO -> ParallelProgram act -> IO (History act)

-- | Check if a history from a parallel execution can be linearised.
checkParallelProgram :: HFoldable act => Transition model act -> Postcondition model act -> InitialModel model -> ParallelProgram act -> History act -> Property

-- | A history is a trace of invocations and responses from running a
--   parallel program.
newtype History act
History :: History' act -> History act
[unHistory] :: History act -> History' act


-- | This module provides &lt;math&gt;-equality for internal actions. 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 actions are equal modulo
--   &lt;math&gt;-conversion.
alphaEq :: (HFunctor act, Eq (Program act)) => Program act -> Program act -> Bool

-- | Check if two forks of actions are equal modulo
--   &lt;math&gt;-conversion.
alphaEqFork :: (HFunctor act, Eq (Program act)) => Fork (Program act) -> Fork (Program act) -> Bool


-- | The main module for state machine based testing, it contains
--   combinators that help you build sequential and parallel properties.
module Test.StateMachine

-- | A (sequential) program is an abstract datatype representing a list of
--   actions.
--   
--   The idea is that the user shows how to generate, shrink, execute and
--   modelcheck individual actions, and then the below combinators lift
--   those things to whole programs.
data Program act

-- | This function is like a <a>forAllShrink</a> for sequential programs.
forAllProgram :: Show (Untyped act) => HFoldable act => Generator model act -> Shrinker act -> Precondition model act -> Transition model act -> InitialModel model -> (Program act -> Property) -> Property

-- | Run a sequential program and check if your model agrees with your
--   semantics.
runAndCheckProgram :: Monad m => HFunctor act => Precondition model act -> Transition model act -> Postcondition model act -> InitialModel model -> Semantics act m -> (m Property -> Property) -> Program act -> Property

-- | Same as above, except with the possibility to setup some resource for
--   the runner to use. The resource could be a database connection for
--   example.
runAndCheckProgram' :: Monad m => HFunctor act => Precondition model act -> Transition model act -> Postcondition model act -> InitialModel model -> Semantics act m -> IO setup -> (setup -> m Property -> Property) -> (setup -> IO ()) -> Program act -> Property

-- | A parallel program is an abstract datatype that represents three
--   sequences of actions; a sequential prefix and two parallel suffixes.
--   Analogous to the sequential case, the user shows how to generate,
--   shrink, execute and modelcheck individual actions, and then the below
--   combinators lift those things to whole parallel programs.
data ParallelProgram act

-- | This function is like a <a>forAllShrink</a> for parallel programs.
forAllParallelProgram :: Show (Untyped act) => HFoldable act => Generator model act -> Shrinker act -> Precondition model act -> Transition model act -> InitialModel model -> (ParallelProgram act -> Property) -> Property

-- | A history is a trace of invocations and responses from running a
--   parallel program.
data History act

-- | Run a parallel program and collect the history of the execution.
runParallelProgram :: Show (Untyped act) => HTraversable act => Semantics act IO -> ParallelProgram act -> (History act -> Property) -> Property

-- | Same as above, but with the possibility of setting up some resource.
runParallelProgram' :: Show (Untyped act) => HTraversable act => IO setup -> (setup -> Semantics act IO) -> (setup -> IO ()) -> ParallelProgram act -> (History act -> Property) -> Property

-- | Check if a history from a parallel execution can be linearised.
checkParallelProgram :: HFoldable act => Transition model act -> Postcondition model act -> InitialModel model -> ParallelProgram act -> History act -> Property