-- 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:
--   
--   
--   
- Test.IOSpec.Fork: a pure specification of
--   forkIO.
--   
- Test.IOSpec.IORef: a pure specification of most functions
--   that create and manipulate on IORefs.
--   
- Test.IOSpec.MVar: a pure specification of most functions
--   that create and manipulate and MVars.
--   
- Test.IOSpec.STM: a pure specification of atomically
--   and the STM monad.
--   
- Test.IOSpec.Teletype: a pure specification of
--   getChar, putChar, and several related Prelude
--   functions.
--   
--   
--   Besides these modules containing the specifications, there are a few
--   other important modules:
--   
--   
--   
- Test.IOSpec.Types: defines the IOSpec type and
--   several amenities.
--   
- Test.IOSpec.VirtualMachine: defines a virtual machine on
--   which to execute pure specifications.
--   
- Test.IOSpec.Surrogate: a drop-in replacement for the other
--   modules. Import this and recompile your code once you've finished
--   testing and debugging.
--   
--   
--   There are several well-documented examples included with the source
--   distribution.
@package IOSpec
@version 0.3.1.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
--   https://webspace.science.uu.nl/~swier004//publications/2008-jfp.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 :: Type -> Type) a
Pure :: a -> IOSpec (f :: Type -> Type) a
Impure :: f (IOSpec f a) -> IOSpec (f :: Type -> Type) a

-- | The fold over IOSpec values.
foldIOSpec :: Functor f => (a -> b) -> (f b -> b) -> IOSpec f a -> b

-- | The coproduct of functors
data ( (f :: Type -> Type) :+: (g :: Type -> Type) ) x
Inl :: f x -> (:+:) (f :: Type -> Type) (g :: Type -> Type) x
Inr :: g x -> (:+:) (f :: Type -> Type) (g :: Type -> Type) x
infixr 5 :+:

-- | The (:<:) class
class (Functor sub, Functor sup) => (sub :: Type -> Type) :<: (sup :: Type -> Type)
inject :: forall g (f :: Type -> Type) a. g :<: f => g (IOSpec f a) -> IOSpec f a
instance (GHC.Internal.Base.Functor f, GHC.Internal.Base.Functor g) => f Test.IOSpec.Types.:<: (f Test.IOSpec.Types.:+: g)
instance (f Test.IOSpec.Types.:<: g, GHC.Internal.Base.Functor f, GHC.Internal.Base.Functor g, GHC.Internal.Base.Functor h) => f Test.IOSpec.Types.:<: (h Test.IOSpec.Types.:+: g)
instance GHC.Internal.Base.Functor f => f Test.IOSpec.Types.:<: f
instance GHC.Internal.Base.Functor f => GHC.Internal.Base.Applicative (Test.IOSpec.Types.IOSpec f)
instance (GHC.Internal.Base.Functor f, GHC.Internal.Base.Functor g) => GHC.Internal.Base.Functor (f Test.IOSpec.Types.:+: g)
instance GHC.Internal.Base.Functor f => GHC.Internal.Base.Functor (Test.IOSpec.Types.IOSpec f)
instance GHC.Internal.Base.Functor f => GHC.Internal.Base.Monad (Test.IOSpec.Types.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 :: forall (f :: Type -> Type) a. 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 :: Type -> Type)
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 :: forall (f :: Type -> Type) a. 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 :: forall (f :: Type -> Type) a. 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 :: forall (f :: Type -> Type) a. Executable f => IOSpec f a -> Scheduler -> Store
instance GHC.Internal.Base.Applicative Test.IOSpec.VirtualMachine.Effect
instance Test.QuickCheck.Arbitrary.Arbitrary Test.IOSpec.VirtualMachine.Scheduler
instance Test.QuickCheck.Arbitrary.Arbitrary Test.IOSpec.VirtualMachine.ThreadId
instance Test.QuickCheck.Arbitrary.CoArbitrary Test.IOSpec.VirtualMachine.ThreadId
instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.IOSpec.VirtualMachine.Effect a)
instance GHC.Classes.Eq Test.IOSpec.VirtualMachine.ThreadId
instance (Test.IOSpec.VirtualMachine.Executable f, Test.IOSpec.VirtualMachine.Executable g) => Test.IOSpec.VirtualMachine.Executable (f Test.IOSpec.Types.:+: g)
instance GHC.Internal.Base.Functor Test.IOSpec.VirtualMachine.Effect
instance GHC.Internal.Base.Monad Test.IOSpec.VirtualMachine.Effect
instance GHC.Internal.Show.Show Test.IOSpec.VirtualMachine.Scheduler
instance GHC.Internal.Show.Show Test.IOSpec.VirtualMachine.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 :: forall (f :: Type -> Type). Teletype :<: f => IOSpec f Char

-- | The getChar function can be used to print a character to the
--   teletype.
putChar :: forall (f :: Type -> Type). Teletype :<: f => Char -> IOSpec f ()
putStr :: forall (f :: Type -> Type). Teletype :<: f => String -> IOSpec f ()
putStrLn :: forall (f :: Type -> Type). Teletype :<: f => String -> IOSpec f ()
getLine :: forall (f :: Type -> Type). Teletype :<: f => IOSpec f String
instance Test.IOSpec.VirtualMachine.Executable Test.IOSpec.Teletype.Teletype
instance GHC.Internal.Base.Functor Test.IOSpec.Teletype.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 :: forall (f :: Type -> Type) a. 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 GHC.Internal.Base.Applicative Test.IOSpec.STM.STM
instance Test.IOSpec.VirtualMachine.Executable Test.IOSpec.STM.STMS
instance GHC.Internal.Base.Functor Test.IOSpec.STM.STM
instance GHC.Internal.Base.Functor Test.IOSpec.STM.STMS
instance GHC.Internal.Base.Monad Test.IOSpec.STM.STM

-- | 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 :: forall a (f :: Type -> Type). (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 :: forall a (f :: Type -> Type). (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 :: forall a (f :: Type -> Type). (Typeable a, MVarS :<: f) => MVar a -> a -> IOSpec f ()
instance Test.IOSpec.VirtualMachine.Executable Test.IOSpec.MVar.MVarS
instance GHC.Internal.Base.Functor Test.IOSpec.MVar.MVarS

-- | 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 :: forall a (f :: Type -> Type). (Typeable a, IORefS :<: f) => a -> IOSpec f (IORef a)

-- | The readIORef function reads the value stored in a mutable
--   variable.
readIORef :: forall a (f :: Type -> Type). (Typeable a, IORefS :<: f) => IORef a -> IOSpec f a

-- | The writeIORef function overwrites the value stored in a
--   mutable variable.
writeIORef :: forall a (f :: Type -> Type). (Typeable a, IORefS :<: f) => IORef a -> a -> IOSpec f ()

-- | The modifyIORef function applies a function to the value stored
--   in and IORef.
modifyIORef :: forall a (f :: Type -> Type). (Typeable a, IORefS :<: f) => IORef a -> (a -> a) -> IOSpec f ()
instance Test.IOSpec.VirtualMachine.Executable Test.IOSpec.IORef.IORefS
instance GHC.Internal.Base.Functor Test.IOSpec.IORef.IORefS

-- | 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 :: forall (f :: Type -> Type) (g :: Type -> Type) a. (Executable f, ForkS :<: g) => IOSpec f a -> IOSpec g ThreadId
instance Test.IOSpec.VirtualMachine.Executable Test.IOSpec.Fork.ForkS
instance GHC.Internal.Base.Functor Test.IOSpec.Fork.ForkS

module Test.IOSpec

-- | The coproduct of functors
data ( (f :: Type -> Type) :+: (g :: Type -> Type) ) x
Inl :: f x -> (:+:) (f :: Type -> Type) (g :: Type -> Type) x
Inr :: g x -> (:+:) (f :: Type -> Type) (g :: Type -> Type) x
infixr 5 :+:

-- | 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 :: Type -> Type) a
inject :: forall g (f :: Type -> Type) a. g :<: f => g (IOSpec f a) -> IOSpec f a

-- | The (:<:) class
class (Functor sub, Functor sup) => (sub :: Type -> Type) :<: (sup :: Type -> Type)
