IOSpec-0.3: A pure specification of the IO monad.

Safe HaskellSafe
LanguageHaskell98

Test.IOSpec.VirtualMachine

Contents

Description

The virtual machine on which the specifications execute.

Synopsis

The Virtual Machine

type VM a = StateT Store Effect a #

The VM monad is essentially a state monad, modifying the store. Besides returning pure values, various primitive effects may occur, such as printing characters or failing with an error message.

type Data = Dynamic #

type Loc = Int #

data Scheduler #

Instances

data Store #

data ThreadId #

Instances

Eq ThreadId # 
Show ThreadId # 
CoArbitrary ThreadId # 

Methods

coarbitrary :: ThreadId -> Gen b -> Gen b

Arbitrary ThreadId # 

Primitive operations on the VM

alloc :: VM Loc #

The alloc function allocate a fresh location on the heap.

emptyLoc :: Loc -> VM () #

The emptyLoc function removes the data stored at a given location. This corresponds, for instance, to emptying an MVar.

freshThreadId :: VM ThreadId #

The freshThreadId function returns a previously unallocated ThreadId.

finishThread :: ThreadId -> VM () #

The finishThread function kills the thread with the specified ThreadId.

lookupHeap :: Loc -> VM (Maybe Data) #

The lookupHeap function returns the data stored at a given heap location, if there is any.

mainTid :: ThreadId #

The mainTid constant is the ThreadId of the main process.

printChar :: Char -> VM () #

readChar :: VM Char #

The readChar and printChar functions are the primitive counterparts of getChar and putChar in the VM monad.

updateHeap :: Loc -> Data -> VM () #

The updateHeap function overwrites a given location with new data.

updateSoup :: Executable f => ThreadId -> IOSpec f a -> VM () #

The updateSoup function updates the process associated with a given ThreadId.

The observable effects on the VM

data Effect a #

The Effect type contains all the primitive effects that are observable on the virtual machine.

Constructors

Done a 
ReadChar (Char -> Effect a) 
Print Char (Effect a) 
Fail String 

Instances

Monad Effect # 

Methods

(>>=) :: Effect a -> (a -> Effect b) -> Effect b #

(>>) :: Effect a -> Effect b -> Effect b #

return :: a -> Effect a #

fail :: String -> Effect a #

Functor Effect # 

Methods

fmap :: (a -> b) -> Effect a -> Effect b #

(<$) :: a -> Effect b -> Effect a #

Applicative Effect # 

Methods

pure :: a -> Effect a #

(<*>) :: Effect (a -> b) -> Effect a -> Effect b #

(*>) :: Effect a -> Effect b -> Effect b #

(<*) :: Effect a -> Effect b -> Effect a #

Eq a => Eq (Effect a) # 

Methods

(==) :: Effect a -> Effect a -> Bool #

(/=) :: Effect a -> Effect a -> Bool #

Sample schedulers

There are two example scheduling algorithms roundRobin and singleThreaded. Note that Scheduler is also an instance of Arbitrary. Using QuickCheck to generate random schedulers is a great way to maximise the number of interleavings that your tests cover.

roundRobin :: Scheduler #

The roundRobin scheduler provides a simple round-robin scheduler.

singleThreaded :: Scheduler #

The singleThreaded scheduler will never schedule forked threads, always scheduling the main thread. Only use this scheduler if your code is not concurrent.

Executing code on the VM

class Functor f => Executable f where #

The Executable type class captures all the different types of operations that can be executed in the VM monad.

Minimal complete definition

step

Methods

step :: f a -> VM (Step a) #

Instances

Executable Teletype # 

Methods

step :: Teletype a -> VM (Step a) #

Executable STMS # 

Methods

step :: STMS a -> VM (Step a) #

Executable MVarS # 

Methods

step :: MVarS a -> VM (Step a) #

Executable IORefS #

The Executable instance for the IORefS monad.

Methods

step :: IORefS a -> VM (Step a) #

Executable ForkS # 

Methods

step :: ForkS a -> VM (Step a) #

(Executable f, Executable g) => Executable ((:+:) f g) # 

Methods

step :: (f :+: g) a -> VM (Step a) #

data Step a #

Constructors

Step a 
Block 

runIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect (a, Store) #

The runIOSpec function is the heart of this library. Given the scheduling algorithm you want to use, it will run a value of type IOSpec f a, returning the sequence of observable effects together with the final store.

evalIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect a #

The evalIOSpec function returns the effects a computation yields, but discards the final state of the virtual machine.

execIOSpec :: Executable f => IOSpec f a -> Scheduler -> Store #

The execIOSpec returns the final Store after executing a computation.

Beware: this function assumes that your computation will succeed, without any other visible Effect. If your computation reads a character from the teletype, for instance, it will return an error.