Copyright	(c) 2017--2019 Michael Walker
License	MIT
Maintainer	Michael Walker <mike@barrucadu.co.uk>
Stability	experimental
Portability	CPP, ExistentialQuantification, NoMonoLocalBinds, RecordWildCards, TypeFamilies
Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.DejaFu.Conc.Internal.STM

Contents

The ModelSTM monad
Primitive actions
TVars
Output
Execution

Description

MonadSTM testing implementation, internal types and definitions. This module is NOT considered to form part of the public interface of this library.

Synopsis

newtype ModelSTM n a = ModelSTM {
- runModelSTM :: (a -> STMAction n) -> STMAction n
}
data STMAction n
- = forall a e.Exception e => SCatch (e -> ModelSTM n a) (ModelSTM n a) (a -> STMAction n)
- | forall a. SRead (ModelTVar n a) (a -> STMAction n)
- | forall a. SWrite (ModelTVar n a) a (STMAction n)
- | forall a. SOrElse (ModelSTM n a) (ModelSTM n a) (a -> STMAction n)
- | forall a. SNew String a (ModelTVar n a -> STMAction n)
- | forall e.Exception e => SThrow e
- | SRetry
- | SStop (n ())
data ModelTVar n a = ModelTVar {
- tvarId :: TVarId
- tvarRef :: Ref n a
}
data Result a
- = Success [TVarId] [TVarId] a
- | Retry [TVarId]
- | Exception SomeException
runTransaction :: MonadDejaFu n => ModelSTM n a -> IdSource -> n (Result a, n (), IdSource, [TAction])
doTransaction :: MonadDejaFu n => ModelSTM n a -> IdSource -> n (Result a, n (), n (), IdSource, [TAction])
stepTrans :: MonadDejaFu n => STMAction n -> IdSource -> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], TAction)

The `ModelSTM` monad

newtype ModelSTM n a Source #

The underlying monad is based on continuations over primitive actions.

This is not Cont because we want to give it a custom MonadFail instance.

Constructors

ModelSTM
Fields runModelSTM :: (a -> STMAction n) -> STMAction n

Instances

Instances details

MonadFail (ModelSTM n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.STM Methods fail :: String -> ModelSTM n a #
Alternative (ModelSTM n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.STM Methods empty :: ModelSTM n a # (<\|>) :: ModelSTM n a -> ModelSTM n a -> ModelSTM n a # some :: ModelSTM n a -> ModelSTM n [a] # many :: ModelSTM n a -> ModelSTM n [a] #
Applicative (ModelSTM n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.STM Methods pure :: a -> ModelSTM n a # (<>) :: ModelSTM n (a -> b) -> ModelSTM n a -> ModelSTM n b # liftA2 :: (a -> b -> c) -> ModelSTM n a -> ModelSTM n b -> ModelSTM n c # (>) :: ModelSTM n a -> ModelSTM n b -> ModelSTM n b # (<*) :: ModelSTM n a -> ModelSTM n b -> ModelSTM n a #
Functor (ModelSTM n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.STM Methods fmap :: (a -> b) -> ModelSTM n a -> ModelSTM n b # (<$) :: a -> ModelSTM n b -> ModelSTM n a #
Monad (ModelSTM n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.STM Methods (>>=) :: ModelSTM n a -> (a -> ModelSTM n b) -> ModelSTM n b # (>>) :: ModelSTM n a -> ModelSTM n b -> ModelSTM n b # return :: a -> ModelSTM n a #
MonadPlus (ModelSTM n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.STM Methods mzero :: ModelSTM n a # mplus :: ModelSTM n a -> ModelSTM n a -> ModelSTM n a #
MonadSTM (ModelSTM n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.STM Associated Types type TVar (ModelSTM n) :: Type -> Type # Methods newTVar :: a -> ModelSTM n (TVar (ModelSTM n) a) # newTVarN :: String -> a -> ModelSTM n (TVar (ModelSTM n) a) # readTVar :: TVar (ModelSTM n) a -> ModelSTM n a # writeTVar :: TVar (ModelSTM n) a -> a -> ModelSTM n () #
MonadCatch (ModelSTM n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.STM Methods catch :: Exception e => ModelSTM n a -> (e -> ModelSTM n a) -> ModelSTM n a #
MonadThrow (ModelSTM n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.STM Methods throwM :: Exception e => e -> ModelSTM n a #
type TVar (ModelSTM n) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.STM type TVar (ModelSTM n) = ModelTVar n

Primitive actions

data STMAction n Source #

STM transactions are represented as a sequence of primitive actions.

Constructors

forall a e.Exception e => SCatch (e -> ModelSTM n a) (ModelSTM n a) (a -> STMAction n)
forall a. SRead (ModelTVar n a) (a -> STMAction n)
forall a. SWrite (ModelTVar n a) a (STMAction n)
forall a. SOrElse (ModelSTM n a) (ModelSTM n a) (a -> STMAction n)
forall a. SNew String a (ModelTVar n a -> STMAction n)
forall e.Exception e => SThrow e
SRetry
SStop (n ())

`TVar`s

data ModelTVar n a Source #

A TVar is modelled as a unique ID and a reference holding a value.

Constructors

ModelTVar
Fields tvarId :: TVarId tvarRef :: Ref n a

Output

data Result a Source #

The result of an STM transaction, along with which TVars it touched whilst executing.

Constructors

Success [TVarId] [TVarId] a	The transaction completed successfully, reading the first list `TVar`s and writing to the second.
Retry [TVarId]	The transaction aborted by calling `retry`, and read the returned `TVar`s. It should be retried when at least one of the `TVar`s has been mutated.
Exception SomeException	The transaction aborted by throwing an exception.

Instances

Instances details

Show a => Show (Result a) Source #
Instance details Defined in Test.DejaFu.Conc.Internal.STM Methods showsPrec :: Int -> Result a -> ShowS # show :: Result a -> String # showList :: [Result a] -> ShowS #

Execution

runTransaction :: MonadDejaFu n => ModelSTM n a -> IdSource -> n (Result a, n (), IdSource, [TAction]) Source #

Run a transaction, returning the result and new initial TVarId. If the transaction failed, any effects are undone.

doTransaction :: MonadDejaFu n => ModelSTM n a -> IdSource -> n (Result a, n (), n (), IdSource, [TAction]) Source #

Run a STM transaction, returning an action to undo its effects.

If the transaction fails, its effects will automatically be undone, so the undo action returned will be pure ().

stepTrans :: MonadDejaFu n => STMAction n -> IdSource -> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], TAction) Source #

Run a transaction for one step.

The ModelSTM monad

Instances

Primitive actions

TVars

Output

Instances

Execution

The `ModelSTM` monad

`TVar`s