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

Safe Haskell | Safe-Inferred
Language | Haskell98

Test.IOSpec.VirtualMachine

Contents

- The Virtual Machine
- Primitive operations on the VM
- The observable effects on the VM
- Sample schedulers
- Executing code on the VM

Description

The virtual machine on which the specifications execute.

Synopsis

- type VM a = StateT Store Effect a
- type Data = Dynamic
- type Loc = Int
- data Scheduler
- data Store
- data ThreadId
- initialStore :: Scheduler -> Store
- alloc :: VM Loc
- emptyLoc :: Loc -> VM ()
- freshThreadId :: VM ThreadId
- finishThread :: ThreadId -> VM ()
- lookupHeap :: Loc -> VM (Maybe Data)
- mainTid :: ThreadId
- printChar :: Char -> VM ()
- readChar :: VM Char
- updateHeap :: Loc -> Data -> VM ()
- updateSoup :: forall (f :: Type -> Type) a. Executable f => ThreadId -> IOSpec f a -> VM ()
- data Effect a
  - = Done a
  - | ReadChar (Char -> Effect a)
  - | Print Char (Effect a)
  - | Fail String
- roundRobin :: Scheduler
- singleThreaded :: Scheduler
- class Functor f => Executable (f :: Type -> Type) where
  - step :: f a -> VM (Step a)
- data Step a
  - = Step a
  - | Block
- runIOSpec :: forall (f :: Type -> Type) a. Executable f => IOSpec f a -> Scheduler -> Effect (a, Store)
- evalIOSpec :: forall (f :: Type -> Type) a. Executable f => IOSpec f a -> Scheduler -> Effect a
- execIOSpec :: forall (f :: Type -> Type) a. Executable f => IOSpec f a -> Scheduler -> Store

# The Virtual Machine

type VM a = StateT Store Effect a Source #

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

type Loc = Int Source #

data Scheduler Source #

#### Instances

Instances details

Arbitrary Scheduler Source # |
Instance details Defined in Test.IOSpec.VirtualMachine Methods arbitrary :: Gen Scheduler Source # shrink :: Scheduler -> [Scheduler] Source #
Show Scheduler Source # |
Instance details Defined in Test.IOSpec.VirtualMachine Methods showsPrec :: Int -> Scheduler -> ShowS Source # show :: Scheduler -> String Source # showList :: [Scheduler] -> ShowS Source #

data Store Source #

data ThreadId Source #

#### Instances

Instances details

Arbitrary ThreadId Source # |
Instance details Defined in Test.IOSpec.VirtualMachine Methods arbitrary :: Gen ThreadId Source # shrink :: ThreadId -> [ThreadId] Source #
CoArbitrary ThreadId Source # |
Instance details Defined in Test.IOSpec.VirtualMachine Methods coarbitrary :: ThreadId -> Gen b -> Gen b Source #
Show ThreadId Source # |
Instance details Defined in Test.IOSpec.VirtualMachine Methods showsPrec :: Int -> ThreadId -> ShowS Source # show :: ThreadId -> String Source # showList :: [ThreadId] -> ShowS Source #
Eq ThreadId Source # |
Instance details Defined in Test.IOSpec.VirtualMachine Methods (==) :: ThreadId -> ThreadId -> Bool Source # (/=) :: ThreadId -> ThreadId -> Bool Source #

initialStore :: Scheduler -> Store Source #

# Primitive operations on the VM

alloc :: VM Loc Source #

The `alloc` function allocate a fresh location on the heap.

emptyLoc :: Loc -> VM () Source #

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

freshThreadId :: VM ThreadId Source #

The `freshThreadId` function returns a previously unallocated `ThreadId`.

finishThread :: ThreadId -> VM () Source #

The `finishThread` function kills the thread with the specified `ThreadId`.

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

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

mainTid :: ThreadId Source #

The `mainTid` constant is the `ThreadId` of the main process.

printChar :: Char -> VM () Source #

readChar :: VM Char Source #

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

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

The `updateHeap` function overwrites a given location with new data.

updateSoup :: forall (f :: Type -> Type) a. Executable f => ThreadId -> IOSpec f a -> VM () Source #

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

# The observable effects on the VM

data Effect a Source #

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

Instances details

Applicative Effect Source # |
Instance details Defined in Test.IOSpec.VirtualMachine Methods pure :: a -> Effect a Source # (<*>) :: Effect (a -> b) -> Effect a -> Effect b Source # liftA2 :: (a -> b -> c) -> Effect a -> Effect b -> Effect c Source # (*>) :: Effect a -> Effect b -> Effect b Source # (<*) :: Effect a -> Effect b -> Effect a Source #
Functor Effect Source # |
Instance details Defined in Test.IOSpec.VirtualMachine Methods fmap :: (a -> b) -> Effect a -> Effect b Source # (<$) :: a -> Effect b -> Effect a Source #
Monad Effect Source # |
Instance details Defined in Test.IOSpec.VirtualMachine Methods (>>=) :: Effect a -> (a -> Effect b) -> Effect b Source # (>>) :: Effect a -> Effect b -> Effect b Source # return :: a -> Effect a Source #
Eq a => Eq (Effect a) Source # |
Instance details Defined in Test.IOSpec.VirtualMachine Methods (==) :: Effect a -> Effect a -> Bool Source # (/=) :: Effect a -> Effect a -> Bool Source #

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

The `roundRobin` scheduler provides a simple round-robin scheduler.

singleThreaded :: Scheduler Source #

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 :: Type -> Type) where Source #

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

Methods

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

#### Instances

Instances details

Executable ForkS Source # |
Instance details Defined in Test.IOSpec.Fork Methods step :: ForkS a -> VM (Step a) Source #
Executable IORefS Source # | The `Executable` instance for the `IORefS` monad.
Instance details Defined in Test.IOSpec.IORef Methods step :: IORefS a -> VM (Step a) Source #
Executable MVarS Source # |
Instance details Defined in Test.IOSpec.MVar Methods step :: MVarS a -> VM (Step a) Source #
Executable STMS Source # |
Instance details Defined in Test.IOSpec.STM Methods step :: STMS a -> VM (Step a) Source #
Executable Teletype Source # |
Instance details Defined in Test.IOSpec.Teletype Methods step :: Teletype a -> VM (Step a) Source #
(Executable f, Executable g) => Executable (f :+: g) Source # |
Instance details Defined in Test.IOSpec.VirtualMachine Methods step :: (f :+: g) a -> VM (Step a) Source #

data Step a Source #

Constructors

Step a |
Block |

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

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 :: forall (f :: Type -> Type) a. Executable f => IOSpec f a -> Scheduler -> Effect a Source #

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

execIOSpec :: forall (f :: Type -> Type) a. Executable f => IOSpec f a -> Scheduler -> Store Source #

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.