-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | A pure specification of the IO monad.
--
-- This package consists of several modules, that give a pure
-- specification of functions in the IO monad:
--
--
--
-- Besides these modules containing the specifications, there are a few
-- other important modules:
--
--
--
-- There are several well-documented examples included with the source
-- distribution.
@package IOSpec
@version 0.2.2
-- | This module contains a few type signatures to help replace pure
-- specifications by their effectful counterparts.
module Test.IOSpec.Surrogate
-- | The IOSpec f a is merely type synonym for IO a. Once
-- you've tested a module, you can use these definitions to avoid having
-- to change your type signatures.
--
-- Note that because this definition of IOSpec ignores its
-- f argument, each of ForkS, MVarS, etc., is
-- simply an empty data type.
type IOSpec f a = IO a
data ForkS
data MVarS
data IORefS
data STMS
data Teletype
data (:+:) f g
-- | This module contains the basic data types underlying the IOSpec
-- library. Most of the types and classes in this module are described in
-- http://www.cs.nott.ac.uk/~wss/Publications/DataTypesALaCarte.pdf.
module Test.IOSpec.Types
-- | A value of type IOSpec f a is either a pure
-- value of type a or some effect, determined by f.
-- Crucially, IOSpec f is a monad, provided f is
-- a functor.
data IOSpec f a
Pure :: a -> IOSpec f a
Impure :: (f (IOSpec f a)) -> IOSpec f a
-- | The fold over IOSpec values.
foldIOSpec :: Functor f => (a -> b) -> (f b -> b) -> IOSpec f a -> b
-- | The coproduct of functors
data (:+:) f g x
Inl :: (f x) -> :+: f g x
Inr :: (g x) -> :+: f g x
-- | The (:<:) class
class (Functor sub, Functor sup) => :<: sub sup
inject :: :<: g f => g (IOSpec f a) -> IOSpec f a
instance [overlap ok] (f :<: g, Functor f, Functor g, Functor h) => f :<: (h :+: g)
instance [overlap ok] (Functor f, Functor g) => f :<: (f :+: g)
instance [overlap ok] Functor f => f :<: f
instance [overlap ok] (Functor f, Functor g) => Functor (f :+: g)
instance [overlap ok] Functor f => Monad (IOSpec f)
instance [overlap ok] Functor f => Functor (IOSpec f)
-- | The virtual machine on which the specifications execute.
module Test.IOSpec.VirtualMachine
-- | 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 VM a = StateT Store Effect a
type Data = Dynamic
type Loc = Int
data Scheduler
data Store
data ThreadId
initialStore :: Scheduler -> Store
-- | The alloc function allocate a fresh location on the heap.
alloc :: VM Loc
-- | The emptyLoc function removes the data stored at a given
-- location. This corresponds, for instance, to emptying an
-- MVar.
emptyLoc :: Loc -> VM ()
-- | The freshThreadId function returns a previously unallocated
-- ThreadId.
freshThreadId :: VM ThreadId
-- | The finishThread function kills the thread with the specified
-- ThreadId.
finishThread :: ThreadId -> VM ()
-- | The lookupHeap function returns the data stored at a given heap
-- location, if there is any.
lookupHeap :: Loc -> VM (Maybe Data)
-- | The mainTid constant is the ThreadId of the main
-- process.
mainTid :: ThreadId
printChar :: Char -> VM ()
-- | The readChar and printChar functions are the primitive
-- counterparts of getChar and putChar in the VM
-- monad.
readChar :: VM Char
-- | The updateHeap function overwrites a given location with new
-- data.
updateHeap :: Loc -> Data -> VM ()
-- | The updateSoup function updates the process associated with a
-- given ThreadId.
updateSoup :: Executable f => ThreadId -> IOSpec f a -> VM ()
-- | The Effect type contains all the primitive effects that are
-- observable on the virtual machine.
data Effect a
Done :: a -> Effect a
ReadChar :: (Char -> Effect a) -> Effect a
Print :: Char -> (Effect a) -> Effect a
Fail :: String -> Effect a
-- | The roundRobin scheduler provides a simple round-robin
-- scheduler.
roundRobin :: Scheduler
-- | The singleThreaded scheduler will never schedule forked
-- threads, always scheduling the main thread. Only use this scheduler if
-- your code is not concurrent.
singleThreaded :: Scheduler
-- | The Executable type class captures all the different types of
-- operations that can be executed in the VM monad.
class Functor f => Executable f
step :: Executable f => f a -> VM (Step a)
data Step a
Step :: a -> Step a
Block :: Step a
-- | 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.
runIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect (a, Store)
-- | The evalIOSpec function returns the effects a computation
-- yields, but discards the final state of the virtual machine.
evalIOSpec :: Executable f => IOSpec f a -> Scheduler -> Effect a
-- | 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.
execIOSpec :: Executable f => IOSpec f a -> Scheduler -> Store
instance [overlap ok] Eq ThreadId
instance [overlap ok] Show ThreadId
instance [overlap ok] (Executable f, Executable g) => Executable (f :+: g)
instance [overlap ok] Eq a => Eq (Effect a)
instance [overlap ok] Monad Effect
instance [overlap ok] Functor Effect
instance [overlap ok] Show Scheduler
instance [overlap ok] Arbitrary Scheduler
instance [overlap ok] CoArbitrary ThreadId
instance [overlap ok] Arbitrary ThreadId
-- | A pure specification of getChar and putChar.
module Test.IOSpec.Teletype
-- | An expression of type IOSpec Teletype a
-- corresponds to an IO computation that may print to or read
-- from stdout and stdin respectively.
--
-- There is a minor caveat here. I assume that stdin and stdout are not
-- buffered. This is not the standard behaviour in many Haskell
-- compilers.
data Teletype a
-- | The getChar function can be used to read a character from the
-- teletype.
getChar :: :<: Teletype f => IOSpec f Char
-- | The getChar function can be used to print a character to the
-- teletype.
putChar :: :<: Teletype f => Char -> IOSpec f ()
putStr :: :<: Teletype f => String -> IOSpec f ()
putStrLn :: :<: Teletype f => String -> IOSpec f ()
getLine :: :<: Teletype f => IOSpec f String
instance [overlap ok] Executable Teletype
instance [overlap ok] Functor Teletype
module Test.IOSpec.STM
-- | An expression of type IOSpec STMS a corresponds to an
-- IO computation that may use atomically and returns a
-- value of type a.
--
-- By itself, STMS is not terribly useful. You will probably want
-- to use IOSpec (ForkS :+: STMS).
data STMS a
-- | The atomically function atomically executes an STM
-- action.
atomically :: :<: STMS f => STM a -> IOSpec f a
data STM a
-- | A TVar is a shared, mutable variable used by STM.
data TVar a
-- | The newTVar function creates a new transactional variable.
newTVar :: Typeable a => a -> STM (TVar a)
-- | The readTVar function reads the value stored in a transactional
-- variable.
readTVar :: Typeable a => TVar a -> STM a
-- | The writeTVar function overwrites the value stored in a
-- transactional variable.
writeTVar :: Typeable a => TVar a -> a -> STM ()
-- | The retry function abandons a transaction and retries at some
-- later time.
retry :: STM a
-- | The orElse function takes two STM actions stm1
-- and stm2 and performs stm1. If stm1 calls
-- retry it performs stm2. If stm1 succeeds, on
-- the other hand, stm2 is not executed.
orElse :: STM a -> STM a -> STM a
-- | The check function checks if its boolean argument holds. If the
-- boolean is true, it returns (); otherwise it calls retry.
check :: Bool -> STM ()
instance [overlap ok] Monad STM
instance [overlap ok] Functor STM
instance [overlap ok] Executable STMS
instance [overlap ok] Functor STMS
-- | A pure specification of mutable variables.
module Test.IOSpec.IORef
-- | An expression of type IOSpec IORefS a corresponds to an
-- IO computation that uses mutable references and returns a
-- value of type a.
data IORefS a
-- | A mutable variable storing a value of type a. Note that the types
-- stored by an IORef are assumed to be Typeable.
data IORef a
-- | The newIORef function creates a new mutable variable.
newIORef :: (Typeable a, :<: IORefS f) => a -> IOSpec f (IORef a)
-- | The readIORef function reads the value stored in a mutable
-- variable.
readIORef :: (Typeable a, :<: IORefS f) => IORef a -> IOSpec f a
-- | The writeIORef function overwrites the value stored in a
-- mutable variable.
writeIORef :: (Typeable a, :<: IORefS f) => IORef a -> a -> IOSpec f ()
-- | The modifyIORef function applies a function to the value stored
-- in and IORef.
modifyIORef :: (Typeable a, :<: IORefS f) => IORef a -> (a -> a) -> IOSpec f ()
instance [overlap ok] Executable IORefS
instance [overlap ok] Functor IORefS
-- | A pure specification of basic operations on MVars.
module Test.IOSpec.MVar
-- | An expression of type IOSpec MVarS a corresponds to an
-- IO computation that uses shared, mutable variables and
-- returns a value of type a.
--
-- By itself, MVarS is not terribly useful. You will probably want
-- to use IOSpec (ForkS :+: MVarS).
data MVarS a
-- | An MVar is a shared, mutable variable.
data MVar a
-- | The newEmptyMVar function creates a new MVar that is
-- initially empty.
newEmptyMVar :: (Typeable a, :<: MVarS f) => IOSpec f (MVar a)
-- | The takeMVar function removes the value stored in an
-- MVar. If the MVar is empty, the thread is blocked.
takeMVar :: (Typeable a, :<: MVarS f) => MVar a -> IOSpec f a
-- | The putMVar function fills an MVar with a new value. If
-- the MVar is not empty, the thread is blocked.
putMVar :: (Typeable a, :<: MVarS f) => MVar a -> a -> IOSpec f ()
instance [overlap ok] Typeable1 MVar
instance [overlap ok] Executable MVarS
instance [overlap ok] Functor MVarS
-- | A pure specification of forkIO.
module Test.IOSpec.Fork
-- | An expression of type IOSpec ForkS a corresponds to an
-- IO computation that uses forkIO and returns a value of
-- type a.
--
-- By itself, ForkS is not terribly useful. You will probably want
-- to use IOSpec (ForkS :+: MVarS) or IOSpec (ForkS :+:
-- STMS).
data ForkS a
-- | The forkIO function forks off a new thread.
forkIO :: (Executable f, :<: ForkS g) => IOSpec f a -> IOSpec g ThreadId
instance [overlap ok] Executable ForkS
instance [overlap ok] Functor ForkS
module Test.IOSpec