{-# LANGUAGE ExistentialQuantification, TypeOperators #-}

-- | The virtual machine on which the specifications execute.
module Test.IOSpec.VirtualMachine
  (
  -- * The Virtual Machine
   VM
  , Data
  , Loc
  , Scheduler
  , Store
  , ThreadId
  , initialStore
  -- * Primitive operations on the VM
  , alloc
  , emptyLoc
  , freshThreadId
  , finishThread
  , lookupHeap
  , mainTid
  , printChar
  , readChar
  , updateHeap
  , updateSoup
  -- * The observable effects on the VM
  , Effect (..)
  -- * Sample schedulers
  -- $schedulerDoc
  , roundRobin
  , singleThreaded
  -- * Executing code on the VM
  , Executable(..)
  , Step(..)
  , runIOSpec
  , evalIOSpec
  , execIOSpec
  )
  where

import Control.Monad.State
import Data.Dynamic
import Data.List
import qualified Data.Stream as Stream
import Test.IOSpec.Types
import Test.QuickCheck
import Control.Monad (liftM, ap)

type Data         = Dynamic
type Loc          = Int
type Heap         = Loc -> Maybe Data

newtype ThreadId  = ThreadId Int deriving (ThreadId -> ThreadId -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ThreadId -> ThreadId -> Bool
$c/= :: ThreadId -> ThreadId -> Bool
== :: ThreadId -> ThreadId -> Bool
$c== :: ThreadId -> ThreadId -> Bool
Eq, Int -> ThreadId -> ShowS
[ThreadId] -> ShowS
ThreadId -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ThreadId] -> ShowS
$cshowList :: [ThreadId] -> ShowS
show :: ThreadId -> String
$cshow :: ThreadId -> String
showsPrec :: Int -> ThreadId -> ShowS
$cshowsPrec :: Int -> ThreadId -> ShowS
Show)

instance Arbitrary ThreadId where
  arbitrary :: Gen ThreadId
arbitrary                = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> ThreadId
ThreadId forall a. Arbitrary a => Gen a
arbitrary

instance CoArbitrary ThreadId where
  coarbitrary :: forall b. ThreadId -> Gen b -> Gen b
coarbitrary (ThreadId Int
k) = forall a b. CoArbitrary a => a -> Gen b -> Gen b
coarbitrary Int
k

newtype Scheduler =
  Scheduler (Int -> (Int, Scheduler))

instance Arbitrary Scheduler where
  arbitrary :: Gen Scheduler
arbitrary   = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Stream Int -> Scheduler
streamSched forall a. Arbitrary a => Gen a
arbitrary

instance Show Scheduler where
  show :: Scheduler -> String
show Scheduler
_ = String
"Test.IOSpec.Scheduler"


data ThreadStatus =
     forall f b . Executable f => Running (IOSpec f b)
  |  Finished

type ThreadSoup = ThreadId -> ThreadStatus

data Store =
  Store { Store -> Int
fresh :: Loc
        ,  Store -> Heap
heap :: Heap
        ,  Store -> ThreadId
nextTid :: ThreadId
        ,  Store -> [ThreadId]
blockedThreads :: [ThreadId]
        ,  Store -> [ThreadId]
finishedThreads :: [ThreadId]
        ,  Store -> Scheduler
scheduler :: Scheduler
        ,  Store -> ThreadSoup
threadSoup :: ThreadSoup
        }

initialStore :: Scheduler -> Store
initialStore :: Scheduler -> Store
initialStore Scheduler
sch =
  Store { fresh :: Int
fresh = Int
0
        , heap :: Heap
heap = forall a. String -> a
internalError String
"Access of unallocated memory "
        , nextTid :: ThreadId
nextTid = Int -> ThreadId
ThreadId Int
1
        , blockedThreads :: [ThreadId]
blockedThreads = []
        , finishedThreads :: [ThreadId]
finishedThreads = []
        , scheduler :: Scheduler
scheduler = Scheduler
sch
        , threadSoup :: ThreadSoup
threadSoup = forall a. String -> a
internalError String
"Unknown thread scheduled"
        }

-- Auxiliary functions
modifyFresh :: (Loc -> Loc) -> VM ()
modifyFresh :: (Int -> Int) -> VM ()
modifyFresh Int -> Int
f           = do Store
s <- forall s (m :: * -> *). MonadState s m => m s
get
                             forall s (m :: * -> *). MonadState s m => s -> m ()
put (Store
s {fresh :: Int
fresh = Int -> Int
f (Store -> Int
fresh Store
s)})

modifyHeap :: (Heap -> Heap) -> VM ()
modifyHeap :: (Heap -> Heap) -> VM ()
modifyHeap Heap -> Heap
f            = do Store
s <- forall s (m :: * -> *). MonadState s m => m s
get
                             forall s (m :: * -> *). MonadState s m => s -> m ()
put (Store
s {heap :: Heap
heap = Heap -> Heap
f (Store -> Heap
heap Store
s)})

modifyNextTid :: (ThreadId -> ThreadId) -> VM ()
modifyNextTid :: (ThreadId -> ThreadId) -> VM ()
modifyNextTid ThreadId -> ThreadId
f         = do Store
s <- forall s (m :: * -> *). MonadState s m => m s
get
                             forall s (m :: * -> *). MonadState s m => s -> m ()
put (Store
s {nextTid :: ThreadId
nextTid = ThreadId -> ThreadId
f (Store -> ThreadId
nextTid Store
s)})

modifyBlockedThreads :: ([ThreadId] -> [ThreadId]) -> VM ()
modifyBlockedThreads :: ([ThreadId] -> [ThreadId]) -> VM ()
modifyBlockedThreads [ThreadId] -> [ThreadId]
f  = do Store
s <- forall s (m :: * -> *). MonadState s m => m s
get
                             forall s (m :: * -> *). MonadState s m => s -> m ()
put (Store
s {blockedThreads :: [ThreadId]
blockedThreads = [ThreadId] -> [ThreadId]
f (Store -> [ThreadId]
blockedThreads Store
s)})

modifyFinishedThreads :: ([ThreadId] -> [ThreadId]) -> VM ()
modifyFinishedThreads :: ([ThreadId] -> [ThreadId]) -> VM ()
modifyFinishedThreads [ThreadId] -> [ThreadId]
f  = do Store
s <- forall s (m :: * -> *). MonadState s m => m s
get
                              forall s (m :: * -> *). MonadState s m => s -> m ()
put (Store
s {finishedThreads :: [ThreadId]
finishedThreads = [ThreadId] -> [ThreadId]
f (Store -> [ThreadId]
finishedThreads Store
s)})

modifyScheduler :: (Scheduler -> Scheduler) -> VM ()
modifyScheduler :: (Scheduler -> Scheduler) -> VM ()
modifyScheduler Scheduler -> Scheduler
f       = do Store
s <- forall s (m :: * -> *). MonadState s m => m s
get
                             forall s (m :: * -> *). MonadState s m => s -> m ()
put (Store
s {scheduler :: Scheduler
scheduler = Scheduler -> Scheduler
f (Store -> Scheduler
scheduler Store
s)})

modifyThreadSoup :: (ThreadSoup -> ThreadSoup) -> VM ()
modifyThreadSoup :: (ThreadSoup -> ThreadSoup) -> VM ()
modifyThreadSoup ThreadSoup -> ThreadSoup
f = do Store
s <- forall s (m :: * -> *). MonadState s m => m s
get
                        forall s (m :: * -> *). MonadState s m => s -> m ()
put (Store
s {threadSoup :: ThreadSoup
threadSoup = ThreadSoup -> ThreadSoup
f (Store -> ThreadSoup
threadSoup Store
s)})


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

-- | The 'alloc' function allocate a fresh location on the heap.
alloc :: VM Loc
alloc :: VM Int
alloc = do  Int
loc <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> Int
fresh
            (Int -> Int) -> VM ()
modifyFresh (forall a. Num a => a -> a -> a
(+) Int
1)
            forall (m :: * -> *) a. Monad m => a -> m a
return Int
loc

-- | The 'emptyLoc' function removes the data stored at a given
-- location. This corresponds, for instance, to emptying an @MVar@.
emptyLoc :: Loc -> VM ()
emptyLoc :: Int -> VM ()
emptyLoc Int
l = (Heap -> Heap) -> VM ()
modifyHeap (forall a b. Eq a => a -> b -> (a -> b) -> a -> b
update Int
l forall a. Maybe a
Nothing)

-- | The 'freshThreadId' function returns a previously unallocated 'ThreadId'.
freshThreadId :: VM ThreadId
freshThreadId :: VM ThreadId
freshThreadId = do
  ThreadId
t <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> ThreadId
nextTid
  (ThreadId -> ThreadId) -> VM ()
modifyNextTid (\(ThreadId Int
n) -> Int -> ThreadId
ThreadId (Int
nforall a. Num a => a -> a -> a
+Int
1))
  forall (m :: * -> *) a. Monad m => a -> m a
return ThreadId
t

-- | The 'finishThread' function kills the thread with the specified
-- 'ThreadId'.
finishThread :: ThreadId -> VM ()
finishThread :: ThreadId -> VM ()
finishThread ThreadId
tid = do
  ([ThreadId] -> [ThreadId]) -> VM ()
modifyFinishedThreads (ThreadId
tidforall a. a -> [a] -> [a]
:)
  (ThreadSoup -> ThreadSoup) -> VM ()
modifyThreadSoup (forall a b. Eq a => a -> b -> (a -> b) -> a -> b
update ThreadId
tid ThreadStatus
Finished)

-- | The 'blockThread' method is used to record when a thread cannot
-- make progress.
blockThread :: ThreadId -> VM ()
blockThread :: ThreadId -> VM ()
blockThread ThreadId
tid = ([ThreadId] -> [ThreadId]) -> VM ()
modifyBlockedThreads (ThreadId
tidforall a. a -> [a] -> [a]
:)

-- | When progress is made, the 'resetBlockedThreads' function
-- | ensures that any thread can be scheduled.
resetBlockedThreads :: VM ()
resetBlockedThreads :: VM ()
resetBlockedThreads = ([ThreadId] -> [ThreadId]) -> VM ()
modifyBlockedThreads (forall a b. a -> b -> a
const [])

-- | The 'lookupHeap' function returns the data stored at a given
-- heap location, if there is any.
lookupHeap :: Loc -> VM (Maybe Data)
lookupHeap :: Int -> VM (Maybe Data)
lookupHeap Int
l = do  Heap
h <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> Heap
heap
                   forall (m :: * -> *) a. Monad m => a -> m a
return (Heap
h Int
l)

-- | The 'mainTid' constant is the 'ThreadId' of the main process.
mainTid :: ThreadId
mainTid :: ThreadId
mainTid = Int -> ThreadId
ThreadId Int
0

-- | The 'readChar' and 'printChar' functions are the primitive
-- counterparts of 'getChar' and 'putChar' in the 'VM' monad.
readChar :: VM Char
readChar :: VM Char
readChar = forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT (\Store
s -> (forall a. (Char -> Effect a) -> Effect a
ReadChar (\Char
c -> (forall a. a -> Effect a
Done (Char
c,Store
s)))))

printChar :: Char -> VM ()
printChar :: Char -> VM ()
printChar Char
c = forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT (\Store
s -> (forall a. Char -> Effect a -> Effect a
Print Char
c (forall a. a -> Effect a
Done ((),Store
s))))

-- | The 'updateHeap' function overwrites a given location with
-- new data.
updateHeap :: Loc -> Data -> VM ()
updateHeap :: Int -> Data -> VM ()
updateHeap Int
l Data
d  = (Heap -> Heap) -> VM ()
modifyHeap (forall a b. Eq a => a -> b -> (a -> b) -> a -> b
update Int
l (forall a. a -> Maybe a
Just Data
d))

-- | The 'updateSoup' function updates the process associated with a
-- given 'ThreadId'.
updateSoup :: Executable f => ThreadId -> IOSpec f a -> VM ()
updateSoup :: forall (f :: * -> *) a.
Executable f =>
ThreadId -> IOSpec f a -> VM ()
updateSoup ThreadId
tid IOSpec f a
p = (ThreadSoup -> ThreadSoup) -> VM ()
modifyThreadSoup (forall a b. Eq a => a -> b -> (a -> b) -> a -> b
update ThreadId
tid (forall (f :: * -> *) b. Executable f => IOSpec f b -> ThreadStatus
Running IOSpec f a
p))

update :: Eq a => a -> b -> (a -> b) -> (a -> b)
update :: forall a b. Eq a => a -> b -> (a -> b) -> a -> b
update a
l b
d a -> b
h a
k
  | a
l forall a. Eq a => a -> a -> Bool
== a
k       = b
d
  | Bool
otherwise    = a -> b
h a
k

-- | The 'Effect' type contains all the primitive effects that are
-- observable on the virtual machine.
data Effect a =
    Done a
  | ReadChar (Char -> Effect a)
  | Print Char (Effect a)
  | Fail String

instance Functor Effect where
  fmap :: forall a b. (a -> b) -> Effect a -> Effect b
fmap a -> b
f (Done a
x) = forall a. a -> Effect a
Done (a -> b
f a
x)
  fmap a -> b
f (ReadChar Char -> Effect a
t) = forall a. (Char -> Effect a) -> Effect a
ReadChar (\Char
c -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (Char -> Effect a
t Char
c))
  fmap a -> b
f (Print Char
c Effect a
t) = forall a. Char -> Effect a -> Effect a
Print Char
c (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Effect a
t)
  fmap a -> b
_ (Fail String
msg) = forall a. String -> Effect a
Fail String
msg

instance Applicative Effect where
  pure :: forall a. a -> Effect a
pure = forall a. a -> Effect a
Done
  <*> :: forall a b. Effect (a -> b) -> Effect a -> Effect b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad Effect where
  return :: forall a. a -> Effect a
return = forall a. a -> Effect a
Done
  (Done a
x) >>= :: forall a b. Effect a -> (a -> Effect b) -> Effect b
>>= a -> Effect b
f = a -> Effect b
f a
x
  (ReadChar Char -> Effect a
t) >>= a -> Effect b
f = forall a. (Char -> Effect a) -> Effect a
ReadChar (\Char
c -> Char -> Effect a
t Char
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Effect b
f)
  (Print Char
c Effect a
t) >>= a -> Effect b
f = forall a. Char -> Effect a -> Effect a
Print Char
c (Effect a
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Effect b
f)
  (Fail String
msg) >>= a -> Effect b
_ = forall a. String -> Effect a
Fail String
msg

instance Eq a => Eq (Effect a) where
  (Done a
x) == :: Effect a -> Effect a -> Bool
== (Done a
y) = a
x forall a. Eq a => a -> a -> Bool
== a
y
  (ReadChar Char -> Effect a
f) == (ReadChar Char -> Effect a
g) =
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Char
x -> Char -> Effect a
f Char
x forall a. Eq a => a -> a -> Bool
== Char -> Effect a
g Char
x) [forall a. Bounded a => a
minBound .. forall a. Bounded a => a
maxBound]
  (Print Char
c Effect a
t) == (Print Char
d Effect a
u) = Char
c forall a. Eq a => a -> a -> Bool
== Char
d Bool -> Bool -> Bool
&& Effect a
t forall a. Eq a => a -> a -> Bool
== Effect a
u
  (Fail String
s) == (Fail String
t) = String
s forall a. Eq a => a -> a -> Bool
== String
t
  Effect a
_ == Effect a
_ = Bool
False

-- $schedulerDoc
--
-- 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.

-- | The 'roundRobin' scheduler provides a simple round-robin scheduler.
roundRobin :: Scheduler
roundRobin :: Scheduler
roundRobin = Stream Int -> Scheduler
streamSched (forall c a. (c -> (a, c)) -> c -> Stream a
Stream.unfold (\Int
k -> (Int
k, Int
kforall a. Num a => a -> a -> a
+Int
1)) Int
0)

-- | 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
singleThreaded :: Scheduler
singleThreaded = Stream Int -> Scheduler
streamSched (forall a. a -> Stream a
Stream.repeat Int
0)

streamSched :: Stream.Stream Int -> Scheduler
streamSched :: Stream Int -> Scheduler
streamSched (Stream.Cons Int
x Stream Int
xs) =
  (Int -> (Int, Scheduler)) -> Scheduler
Scheduler (\Int
k -> (Int
x forall a. Integral a => a -> a -> a
`mod` Int
k, Stream Int -> Scheduler
streamSched Stream Int
xs))


-- | The 'Executable' type class captures all the different types of
-- operations that can be executed in the 'VM' monad.
class Functor f => Executable f where
  step :: f a -> VM (Step a)

data Step a = Step a | Block

instance (Executable f, Executable g) => Executable (f :+: g) where
  step :: forall a. (:+:) f g a -> VM (Step a)
step (Inl f a
x) = forall (f :: * -> *) a. Executable f => f a -> VM (Step a)
step f a
x
  step (Inr g a
y) = forall (f :: * -> *) a. Executable f => f a -> VM (Step a)
step g a
y

-- The 'execVM' function essentially schedules a thread and allows
-- it to perform a single step. If the main thread is finished, it
-- returns the final result of the comptuation.
execVM :: Executable f => IOSpec f a -> VM a
execVM :: forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
execVM IOSpec f a
main = do
  (ThreadId
tid,Process a
t) <- forall (f :: * -> *) a.
Executable f =>
IOSpec f a -> VM (ThreadId, Process a)
schedule IOSpec f a
main
  case Process a
t of
    (Main (Pure a
x)) -> VM ()
resetBlockedThreads forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return a
x
    (Main (Impure f (IOSpec f a)
p)) -> do Step (IOSpec f a)
x <- forall (f :: * -> *) a. Executable f => f a -> VM (Step a)
step f (IOSpec f a)
p
                            case Step (IOSpec f a)
x of
                              Step IOSpec f a
y -> VM ()
resetBlockedThreads forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
execVM IOSpec f a
y
                              Step (IOSpec f a)
Block -> ThreadId -> VM ()
blockThread ThreadId
mainTid forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
execVM IOSpec f a
main
    (Aux (Pure b
_)) -> do ThreadId -> VM ()
finishThread ThreadId
tid
                         forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
execVM IOSpec f a
main
    (Aux (Impure f (IOSpec f b)
p)) -> do Step (IOSpec f b)
x <- forall (f :: * -> *) a. Executable f => f a -> VM (Step a)
step f (IOSpec f b)
p
                           case Step (IOSpec f b)
x of
                             Step IOSpec f b
y -> VM ()
resetBlockedThreads forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                       forall (f :: * -> *) a.
Executable f =>
ThreadId -> IOSpec f a -> VM ()
updateSoup ThreadId
tid IOSpec f b
y forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                       forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
execVM IOSpec f a
main
                             Step (IOSpec f b)
Block -> ThreadId -> VM ()
blockThread ThreadId
tid forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                      forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
execVM IOSpec f a
main
-- A Process is the result of a call to the scheduler.
data Process a =
     forall f . Executable f => Main (IOSpec f a)
  |  forall f b . Executable f => Aux (IOSpec f b)

-- Gets the ThreadId of the next thread to schedule.
getNextThreadId :: VM ThreadId
getNextThreadId :: VM ThreadId
getNextThreadId = do
  Scheduler Int -> (Int, Scheduler)
sch <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> Scheduler
scheduler
  (ThreadId Int
total) <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> ThreadId
nextTid
  let allTids :: [ThreadId]
allTids = [Int -> ThreadId
ThreadId Int
i | Int
i <- [Int
0 .. Int
total forall a. Num a => a -> a -> a
- Int
1]]
  [ThreadId]
blockedTids <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> [ThreadId]
blockedThreads
  [ThreadId]
finishedTids <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> [ThreadId]
finishedThreads
  let activeThreads :: [ThreadId]
activeThreads = [ThreadId]
allTids forall a. Eq a => [a] -> [a] -> [a]
\\ ([ThreadId]
blockedTids forall a. Eq a => [a] -> [a] -> [a]
`union` [ThreadId]
finishedTids)
  let (Int
i,Scheduler
s) = Int -> (Int, Scheduler)
sch (forall (t :: * -> *) a. Foldable t => t a -> Int
length [ThreadId]
activeThreads)
  (Scheduler -> Scheduler) -> VM ()
modifyScheduler (forall a b. a -> b -> a
const Scheduler
s)
  forall (m :: * -> *) a. Monad m => a -> m a
return ([ThreadId]
activeThreads forall a. [a] -> Int -> a
!! Int
i)

-- The 'schedule' function tries to schedule an active thread,
-- returning the scheduled thread's ThreadId and the process
-- associated with that id.
schedule :: Executable f => IOSpec f a -> VM (ThreadId, Process a)
schedule :: forall (f :: * -> *) a.
Executable f =>
IOSpec f a -> VM (ThreadId, Process a)
schedule IOSpec f a
main = do  ThreadId
tid <- VM ThreadId
getNextThreadId
                    if ThreadId
tid forall a. Eq a => a -> a -> Bool
== ThreadId
mainTid
                      then forall (m :: * -> *) a. Monad m => a -> m a
return (ThreadId
mainTid, forall a (f :: * -> *). Executable f => IOSpec f a -> Process a
Main IOSpec f a
main)
                      else do
                        ThreadSoup
tsoup <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Store -> ThreadSoup
threadSoup
                        case ThreadSoup
tsoup ThreadId
tid of
                          ThreadStatus
Finished ->  forall a. String -> a
internalError
                            String
"Scheduled finished thread."
                          Running IOSpec f b
p -> forall (m :: * -> *) a. Monad m => a -> m a
return (ThreadId
tid, forall a (f :: * -> *) b. Executable f => IOSpec f b -> Process a
Aux IOSpec f b
p)

-- | 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)
runIOSpec :: forall (f :: * -> *) a.
Executable f =>
IOSpec f a -> Scheduler -> Effect (a, Store)
runIOSpec IOSpec f a
io Scheduler
sched = forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
                       (forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
execVM IOSpec f a
io)
                       (Scheduler -> Store
initialStore Scheduler
sched)

-- | 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
execIOSpec :: forall (f :: * -> *) a.
Executable f =>
IOSpec f a -> Scheduler -> Store
execIOSpec IOSpec f a
io Scheduler
sched =
  case forall (f :: * -> *) a.
Executable f =>
IOSpec f a -> Scheduler -> Effect (a, Store)
runIOSpec IOSpec f a
io Scheduler
sched of
    Done (a
_,Store
s) -> Store
s
    Effect (a, Store)
_ -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Failed application of Test.IOSpec.execIOSpec.\n" forall a. [a] -> [a] -> [a]
++
                 String
"Probable cause: your function uses functions such as " forall a. [a] -> [a] -> [a]
++
                 String
"putChar and getChar. Check the preconditions for calling " forall a. [a] -> [a] -> [a]
++
                 String
"this function in the IOSpec documentation."

-- | 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
evalIOSpec :: forall (f :: * -> *) a.
Executable f =>
IOSpec f a -> Scheduler -> Effect a
evalIOSpec IOSpec f a
io Scheduler
sched = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst (forall (f :: * -> *) a.
Executable f =>
IOSpec f a -> Scheduler -> Effect (a, Store)
runIOSpec IOSpec f a
io Scheduler
sched)

internalError :: String -> a
internalError :: forall a. String -> a
internalError String
msg = forall a. HasCallStack => String -> a
error (String
"IOSpec.VirtualMachine: " forall a. [a] -> [a] -> [a]
++ String
msg)