Copyright	(C) 2017 ATS Advanced Telematic Systems GmbH
License	BSD-style (see the file LICENSE)
Maintainer	Stevan Andjelkovic <stevan@advancedtelematic.com>
Stability	provisional
Portability	non-portable (GHC extensions)
Safe Haskell	None
Language	Haskell2010

Test.StateMachine.Types

Contents

Indexed variant of Functor, Foldable and Traversable.
Indexed variants of some constraints package combinators.
Re-export

Description

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.

Synopsis

Documentation

data StateMachineModel model cmd Source #

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

Given a command, how can we show it?

Minimal complete definition

showCmd

Methods

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

How to show a typed command with internal refereces.

showCmd :: forall resp. ShowCmd cmd => cmd (ConstSym1 String) resp -> String Source #

How to show a typed command with internal refereces.

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

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

data Response ix Source #

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

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 ... Source #

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 ... Source #

Type-level function that maybe returns a response.

Equations

GetResponse_ (Response t) = t
GetResponse_ (Reference i) = ()

class HasResponse cmd where Source #

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

Minimal complete definition

response

Methods

response :: cmd refs resp -> SResponse ix resp Source #

What type of response a typed command has.

response :: HasResponse cmd => cmd refs resp -> SResponse ix resp Source #

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) Source #

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

data Untyped f refs where Source #

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

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

Instances

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

Indexed variant of `Functor`, `Foldable` and `Traversable`.

data Ex p Source #

Dependent pairs.

Constructors

Ex (Sing x) (p @@ x)

class IxFunctor f where Source #

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

Indexed fmap.

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

Indexed fmap.

class IxFoldable t where Source #

Foldable for predicate transformers.

Minimal complete definition

ifoldMap

Methods

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

Indexed foldMap.

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

Indexed toList.

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

Indexed any.

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

Indexed foldMap.

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

Indexed toList.

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

Indexed any.

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

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) Source #

Indexed traverse function.

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

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) Source #

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) Source #

Same as above, with arguments flipped.

Indexed variants of some `constraints` package combinators.

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

Indexed variant of ForallF.

Instances

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

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

Type alias that is helpful when defining state machine models.

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

Same as the above.

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

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)

Documentation

Indexed variant of Functor, Foldable and Traversable.

Indexed variants of some constraints package combinators.

Re-export

Indexed variant of `Functor`, `Foldable` and `Traversable`.

Indexed variants of some `constraints` package combinators.