Test.StateMachine.Types

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

Documentation

data StateMachineModel model cmd

A state machine based model.

Constructors

StateMachineModel

Fields

• precondition :: forall refs resp. IxForallF Ord refs => model refs -> cmd refs resp -> Bool
• postcondition :: forall refs resp. IxForallF Ord refs => model refs -> cmd refs resp -> Response_ refs resp -> Property
• transition :: forall refs resp. IxForallF Ord refs => model refs -> cmd refs resp -> Response_ refs resp -> model refs
• initialModel :: forall refs. model refs

class ShowCmd cmd where

Given a command, how can we show it?

Minimal complete definition

showCmd

Methods

showCmd :: forall resp. cmd (ConstSym1 String) resp -> String

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.

type Signature ix = (TyFun ix Type -> Type) -> Response ix -> Type

Signatures of commands contain a family of references and a response type.

data Response ix

A response of a command is either of some type or a referece at some index.

Constructors

Response Type

Reference ix

data SResponse ix :: Response ix -> Type where

The singleton type of responses.

Constructors

SResponse :: SResponse ix (Response t)

SReference :: Sing (i :: ix) -> SResponse ix (Reference i)

type family Response_ (refs :: TyFun ix Type -> Type) (resp :: Response ix) :: Type where ...

Type-level function that returns a response type.

Equations

Response_ refs (Response t) = t

Response_ refs (Reference i) = refs @@ i

type family GetResponse_ (resp :: Response ix) :: k where ...

Type-level function that maybe returns a response.

Equations

GetResponse_ (Response t) = t

GetResponse_ (Reference i) = ()

class HasResponse cmd where

Given a command, what kind of response does it have?

Minimal complete definition

response

Methods

response :: cmd refs resp -> SResponse ix resp

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.

type CommandConstraint ix cmd = (Ord ix, SDecide ix, SingKind ix, DemoteRep ix ~ ix, ShowCmd cmd, IxTraversable cmd, HasResponse cmd)

The constraints on commands (and their indices) that the sequentialProperty and parallelProperty helpers require.

data Untyped f refs where

Untyped commands are command where we hide the response type. This is used in generation of commands.

Constructors

Untyped :: (Show (GetResponse_ resp), Typeable (Response_ ConstIntRef resp), Typeable resp) => f refs resp -> Untyped f refs

data RefPlaceholder ix :: TyFun ix k -> Type

When generating commands it is enough to provide a reference placeholder.

Instances

type Apply _ * (RefPlaceholder * _) i

type Apply _ * (RefPlaceholder * _) i = Sing _ i

Indexed variant of Functor, Foldable and Traversable.

data Ex p

Dependent pairs.

Constructors

Ex (Sing x) (p @@ x)

class IxFunctor f where

Predicate transformers.

Minimal complete definition

ifmap

Methods

ifmap :: forall p q j. (forall i. Sing (i :: ix) -> (p @@ i) -> q @@ i) -> f p j -> f q j

Indexed fmap.

ifmap :: forall p q j. IxFunctor f => (forall i. Sing (i :: ix) -> (p @@ i) -> q @@ i) -> f p j -> f q j

Indexed fmap.

class IxFoldable t where

Foldable for predicate transformers.

Minimal complete definition

ifoldMap

Methods

ifoldMap :: Monoid m => (forall i. Sing (i :: ix) -> (p @@ i) -> m) -> t p j -> m

Indexed foldMap.

itoList :: t p j -> [Ex p]

Indexed toList.

iany :: (forall i. Sing (i :: ix) -> (p @@ i) -> Bool) -> t p j -> Bool

Indexed any.

ifoldMap :: (IxFoldable t, Monoid m) => (forall i. Sing (i :: ix) -> (p @@ i) -> m) -> t p j -> m

Indexed foldMap.

itoList :: IxFoldable t => t p j -> [Ex p]

Indexed toList.

iany :: IxFoldable t => (forall i. Sing (i :: ix) -> (p @@ i) -> Bool) -> t p j -> Bool

Indexed any.

class (IxFunctor t, IxFoldable t) => IxTraversable t where

Tranversable for predicate transformers.

Minimal complete definition

itraverse | ifor

Methods

itraverse :: Applicative f => Proxy q -> (forall x. Sing x -> (p @@ x) -> f (q @@ x)) -> t p j -> f (t q j)

Indexed traverse function.

ifor :: Applicative f => Proxy q -> t p j -> (forall x. Sing x -> (p @@ x) -> f (q @@ x)) -> f (t q j)

Same as above, with arguments flipped.

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

Indexed traverse function.

ifor :: (IxTraversable t, Applicative f) => Proxy q -> t p j -> (forall x. Sing x -> (p @@ x) -> f (q @@ x)) -> f (t q j)

Same as above, with arguments flipped.

Indexed variants of some constraints package combinators.

class Forall (IxComposeC p f) => IxForallF p f

Indexed variant of ForallF.

Instances

Forall k1 (IxComposeC k1 k2 p f) => IxForallF k1 k2 p f

type Ords refs = IxForallF Ord refs :- Ord (refs @@ ())

Type alias that is helpful when defining state machine models.

type Ords' refs i = IxForallF Ord refs :- Ord (refs @@ i)

Same as the above.

iinstF :: forall a p f. Proxy a -> IxForallF p f :- p (f @@ a)

Indexed variant of instF.

Re-export

(\\) :: a => (b -> r) -> (:-) a b -> r infixl 1

Given that a :- b, derive something that needs a context b, using the context a

type (@@) k1 k2 a b = Apply k1 k2 a b infixl 9

An infix synonym for Apply

data Property :: *

The type of properties.

Instances

Testable Property

Methods

property :: Property -> Property

property :: Testable prop => prop -> Property

Convert the thing to a property.

data Proxy k t :: forall k. k -> *

A concrete, poly-kinded proxy type

Constructors

Proxy

Instances

Monad (Proxy *)

Methods

(>>=) :: Proxy * a -> (a -> Proxy * b) -> Proxy * b

(>>) :: Proxy * a -> Proxy * b -> Proxy * b

return :: a -> Proxy * a

fail :: String -> Proxy * a

Functor (Proxy *)

Methods

fmap :: (a -> b) -> Proxy * a -> Proxy * b

(<$) :: a -> Proxy * b -> Proxy * a

Applicative (Proxy *)

Methods

pure :: a -> Proxy * a

(<*>) :: Proxy * (a -> b) -> Proxy * a -> Proxy * b

(*>) :: Proxy * a -> Proxy * b -> Proxy * b

(<*) :: Proxy * a -> Proxy * b -> Proxy * a

Foldable (Proxy *)

Methods

fold :: Monoid m => Proxy * m -> m

foldMap :: Monoid m => (a -> m) -> Proxy * a -> m

foldr :: (a -> b -> b) -> b -> Proxy * a -> b

foldr' :: (a -> b -> b) -> b -> Proxy * a -> b

foldl :: (b -> a -> b) -> b -> Proxy * a -> b

foldl' :: (b -> a -> b) -> b -> Proxy * a -> b

foldr1 :: (a -> a -> a) -> Proxy * a -> a

foldl1 :: (a -> a -> a) -> Proxy * a -> a

toList :: Proxy * a -> [a]

null :: Proxy * a -> Bool

length :: Proxy * a -> Int

elem :: Eq a => a -> Proxy * a -> Bool

maximum :: Ord a => Proxy * a -> a

minimum :: Ord a => Proxy * a -> a

sum :: Num a => Proxy * a -> a

product :: Num a => Proxy * a -> a

Traversable (Proxy *)

Methods

traverse :: Applicative f => (a -> f b) -> Proxy * a -> f (Proxy * b)

sequenceA :: Applicative f => Proxy * (f a) -> f (Proxy * a)

mapM :: Monad m => (a -> m b) -> Proxy * a -> m (Proxy * b)

sequence :: Monad m => Proxy * (m a) -> m (Proxy * a)

Generic1 (Proxy *)

Associated Types

type Rep1 (Proxy * :: * -> *) :: * -> *

Methods

from1 :: Proxy * a -> Rep1 (Proxy *) a

to1 :: Rep1 (Proxy *) a -> Proxy * a

Eq1 (Proxy *)

Since: 4.9.0.0

Methods

liftEq :: (a -> b -> Bool) -> Proxy * a -> Proxy * b -> Bool

Ord1 (Proxy *)

Since: 4.9.0.0

Methods

liftCompare :: (a -> b -> Ordering) -> Proxy * a -> Proxy * b -> Ordering

Read1 (Proxy *)

Since: 4.9.0.0

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Proxy * a)

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Proxy * a]

Show1 (Proxy *)

Since: 4.9.0.0

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Proxy * a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Proxy * a] -> ShowS

Alternative (Proxy *)

Methods

empty :: Proxy * a

(<|>) :: Proxy * a -> Proxy * a -> Proxy * a

some :: Proxy * a -> Proxy * [a]

many :: Proxy * a -> Proxy * [a]

MonadPlus (Proxy *)

Methods

mzero :: Proxy * a

mplus :: Proxy * a -> Proxy * a -> Proxy * a

Bounded (Proxy k s)

Methods

minBound :: Proxy k s

maxBound :: Proxy k s

Enum (Proxy k s)

Methods

succ :: Proxy k s -> Proxy k s

pred :: Proxy k s -> Proxy k s

toEnum :: Int -> Proxy k s

fromEnum :: Proxy k s -> Int

enumFrom :: Proxy k s -> [Proxy k s]

enumFromThen :: Proxy k s -> Proxy k s -> [Proxy k s]

enumFromTo :: Proxy k s -> Proxy k s -> [Proxy k s]

enumFromThenTo :: Proxy k s -> Proxy k s -> Proxy k s -> [Proxy k s]

Eq (Proxy k s)

Methods

(==) :: Proxy k s -> Proxy k s -> Bool

(/=) :: Proxy k s -> Proxy k s -> Bool

Ord (Proxy k s)

Methods

compare :: Proxy k s -> Proxy k s -> Ordering

(<) :: Proxy k s -> Proxy k s -> Bool

(<=) :: Proxy k s -> Proxy k s -> Bool

(>) :: Proxy k s -> Proxy k s -> Bool

(>=) :: Proxy k s -> Proxy k s -> Bool

max :: Proxy k s -> Proxy k s -> Proxy k s

min :: Proxy k s -> Proxy k s -> Proxy k s

Read (Proxy k s)

Methods

readsPrec :: Int -> ReadS (Proxy k s)

readList :: ReadS [Proxy k s]

readPrec :: ReadPrec (Proxy k s)

readListPrec :: ReadPrec [Proxy k s]

Show (Proxy k s)

Methods

showsPrec :: Int -> Proxy k s -> ShowS

show :: Proxy k s -> String

showList :: [Proxy k s] -> ShowS

Ix (Proxy k s)

Methods

range :: (Proxy k s, Proxy k s) -> [Proxy k s]

index :: (Proxy k s, Proxy k s) -> Proxy k s -> Int

unsafeIndex :: (Proxy k s, Proxy k s) -> Proxy k s -> Int

inRange :: (Proxy k s, Proxy k s) -> Proxy k s -> Bool

rangeSize :: (Proxy k s, Proxy k s) -> Int

unsafeRangeSize :: (Proxy k s, Proxy k s) -> Int

Generic (Proxy k t)

Associated Types

type Rep (Proxy k t) :: * -> *

Methods

from :: Proxy k t -> Rep (Proxy k t) x

to :: Rep (Proxy k t) x -> Proxy k t

Semigroup (Proxy k s)

Methods

(<>) :: Proxy k s -> Proxy k s -> Proxy k s

sconcat :: NonEmpty (Proxy k s) -> Proxy k s

stimes :: Integral b => b -> Proxy k s -> Proxy k s

Monoid (Proxy k s)

Methods

mempty :: Proxy k s

mappend :: Proxy k s -> Proxy k s -> Proxy k s

mconcat :: [Proxy k s] -> Proxy k s

type Rep1 (Proxy *)

type Rep1 (Proxy *) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) U1)

type Rep (Proxy k t)

type Rep (Proxy k t) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) U1)