    {-# 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
    (ThreadId -> ThreadId -> Bool)
    -> (ThreadId -> ThreadId -> Bool) -> Eq ThreadId
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ThreadId -> ThreadId -> Bool
    == :: ThreadId -> ThreadId -> Bool
    $c/= :: ThreadId -> ThreadId -> Bool
    /= :: ThreadId -> ThreadId -> Bool
    Eq, Int -> ThreadId -> ShowS
    [ThreadId] -> ShowS
    ThreadId -> String
    (Int -> ThreadId -> ShowS)
    -> (ThreadId -> String) -> ([ThreadId] -> ShowS) -> Show ThreadId
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ThreadId -> ShowS
    showsPrec :: Int -> ThreadId -> ShowS
    $cshow :: ThreadId -> String
    show :: ThreadId -> String
    $cshowList :: [ThreadId] -> ShowS
    showList :: [ThreadId] -> ShowS
    Show)

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

    instance CoArbitrary ThreadId where
      coarbitrary :: forall b. ThreadId -> Gen b -> Gen b
    coarbitrary (ThreadId Int
    k) = Int -> Gen b -> Gen b
    forall b. Int -> Gen b -> Gen b
    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   = (Stream Int -> Scheduler) -> Gen (Stream Int) -> Gen Scheduler
    forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
    liftM Stream Int -> Scheduler
    streamSched Gen (Stream Int)
    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 = String -> 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 = String -> 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 s <- StateT Store Effect Store
    forall s (m :: * -> *). MonadState s m => m s
    get
                                 put (s {fresh = f (fresh s)})

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

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

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

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

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

    modifyThreadSoup :: (ThreadSoup -> ThreadSoup) -> VM ()
    modifyThreadSoup :: (ThreadSoup -> ThreadSoup) -> VM ()
    modifyThreadSoup ThreadSoup -> ThreadSoup
    f = do s <- StateT Store Effect Store
    forall s (m :: * -> *). MonadState s m => m s
    get
                            put (s {threadSoup = f (threadSoup 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  loc <- (Store -> Int) -> VM Int
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets Store -> Int
    fresh
                modifyFresh ((+) 1)
                return 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 (Int -> Maybe Data -> Heap -> Heap
    forall a b. Eq a => a -> b -> (a -> b) -> a -> b
    update Int
    l Maybe Data
    forall a. Maybe a
    Nothing)

    -- | The 'freshThreadId' function returns a previously unallocated 'ThreadId'.
    freshThreadId :: VM ThreadId
    freshThreadId :: VM ThreadId
    freshThreadId = do
      t <- (Store -> ThreadId) -> VM ThreadId
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets Store -> ThreadId
    nextTid
      modifyNextTid (\(ThreadId Int
    n) -> Int -> ThreadId
    ThreadId (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1))
      return 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
    tidThreadId -> [ThreadId] -> [ThreadId]
    forall a. a -> [a] -> [a]
    :)
      (ThreadSoup -> ThreadSoup) -> VM ()
    modifyThreadSoup (ThreadId -> ThreadStatus -> ThreadSoup -> ThreadSoup
    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
    tidThreadId -> [ThreadId] -> [ThreadId]
    forall 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 ([ThreadId] -> [ThreadId] -> [ThreadId]
    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  h <- (Store -> Heap) -> StateT Store Effect Heap
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets Store -> Heap
    heap
                       return (h 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 = (Store -> Effect (Char, Store)) -> VM Char
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    StateT (\Store
    s -> ((Char -> Effect (Char, Store)) -> Effect (Char, Store)
    forall a. (Char -> Effect a) -> Effect a
    ReadChar (\Char
    c -> ((Char, Store) -> Effect (Char, Store)
    forall a. a -> Effect a
    Done (Char
    c,Store
    s)))))

    printChar :: Char -> VM ()
    printChar :: Char -> VM ()
    printChar Char
    c = (Store -> Effect ((), Store)) -> VM ()
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
    StateT (\Store
    s -> (Char -> Effect ((), Store) -> Effect ((), Store)
    forall a. Char -> Effect a -> Effect a
    Print Char
    c (((), Store) -> Effect ((), Store)
    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 (Int -> Maybe Data -> Heap -> Heap
    forall a b. Eq a => a -> b -> (a -> b) -> a -> b
    update Int
    l (Data -> Maybe Data
    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 (ThreadId -> ThreadStatus -> ThreadSoup -> ThreadSoup
    forall a b. Eq a => a -> b -> (a -> b) -> a -> b
    update ThreadId
    tid (IOSpec f a -> ThreadStatus
    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 a -> a -> Bool
    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) = b -> Effect b
    forall a. a -> Effect a
    Done (a -> b
    f a
    x)
      fmap a -> b
    f (ReadChar Char -> Effect a
    t) = (Char -> Effect b) -> Effect b
    forall a. (Char -> Effect a) -> Effect a
    ReadChar (\Char
    c -> (a -> b) -> Effect a -> Effect b
    forall a b. (a -> b) -> Effect a -> Effect b
    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) = Char -> Effect b -> Effect b
    forall a. Char -> Effect a -> Effect a
    Print Char
    c ((a -> b) -> Effect a -> Effect b
    forall a b. (a -> b) -> Effect a -> Effect b
    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) = String -> Effect b
    forall a. String -> Effect a
    Fail String
    msg

    instance Applicative Effect where
      pure :: forall a. a -> Effect a
    pure = a -> Effect a
    forall a. a -> Effect a
    Done
      <*> :: forall a b. Effect (a -> b) -> Effect a -> Effect 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 = a -> Effect a
    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 = (Char -> Effect b) -> Effect b
    forall a. (Char -> Effect a) -> Effect a
    ReadChar (\Char
    c -> Char -> Effect a
    t Char
    c Effect a -> (a -> Effect b) -> Effect b
    forall a b. Effect a -> (a -> Effect b) -> Effect b
    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 = Char -> Effect b -> Effect b
    forall a. Char -> Effect a -> Effect a
    Print Char
    c (Effect a
    t Effect a -> (a -> Effect b) -> Effect b
    forall a b. Effect a -> (a -> Effect b) -> Effect b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= a -> Effect b
    f)
      (Fail String
    msg) >>= a -> Effect b
    _ = String -> 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 a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    y
      (ReadChar Char -> Effect a
    f) == (ReadChar Char -> Effect a
    g) =
        (Char -> Bool) -> String -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (\Char
    x -> Char -> Effect a
    f Char
    x Effect a -> Effect a -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char -> Effect a
    g Char
    x) [Char
    forall a. Bounded a => a
    minBound .. Char
    forall a. Bounded a => a
    maxBound]
      (Print Char
    c Effect a
    t) == (Print Char
    d Effect a
    u) = Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    d Bool -> Bool -> Bool
    && Effect a
    t Effect a -> Effect a -> Bool
    forall a. Eq a => a -> a -> Bool
    == Effect a
    u
      (Fail String
    s) == (Fail String
    t) = String
    s String -> String -> Bool
    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 ((Int -> (Int, Int)) -> Int -> Stream Int
    forall c a. (c -> (a, c)) -> c -> Stream a
    Stream.unfold (\Int
    k -> (Int
    k, Int
    kInt -> Int -> Int
    forall 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 (Int -> Stream Int
    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 Int -> Int -> Int
    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) = f a -> VM (Step a)
    forall a. f a -> VM (Step a)
    forall (f :: * -> *) a. Executable f => f a -> VM (Step a)
    step f a
    x
      step (Inr g a
    y) = g a -> VM (Step a)
    forall a. g a -> VM (Step a)
    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
      (tid,t) <- IOSpec f a -> VM (ThreadId, Process a)
    forall (f :: * -> *) a.
    Executable f =>
    IOSpec f a -> VM (ThreadId, Process a)
    schedule IOSpec f a
    main
      case t of
        (Main (Pure a
    x)) -> VM ()
    resetBlockedThreads VM () -> StateT Store Effect a -> StateT Store Effect a
    forall a b.
    StateT Store Effect a
    -> StateT Store Effect b -> StateT Store Effect b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> a -> StateT Store Effect a
    forall a. a -> StateT Store Effect a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x
        (Main (Impure f (IOSpec f a)
    p)) -> do x <- f (IOSpec f a) -> VM (Step (IOSpec f a))
    forall a. f a -> VM (Step a)
    forall (f :: * -> *) a. Executable f => f a -> VM (Step a)
    step f (IOSpec f a)
    p
                                case x of
                                  Step IOSpec f a
    y -> VM ()
    resetBlockedThreads VM () -> StateT Store Effect a -> StateT Store Effect a
    forall a b.
    StateT Store Effect a
    -> StateT Store Effect b -> StateT Store Effect b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> IOSpec f a -> StateT Store Effect a
    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 VM () -> StateT Store Effect a -> StateT Store Effect a
    forall a b.
    StateT Store Effect a
    -> StateT Store Effect b -> StateT Store Effect b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> IOSpec f a -> StateT Store Effect a
    forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
    execVM IOSpec f a
    main
        (Aux (Pure b
    _)) -> do ThreadId -> VM ()
    finishThread ThreadId
    tid
                             IOSpec f a -> StateT Store Effect a
    forall (f :: * -> *) a. Executable f => IOSpec f a -> VM a
    execVM IOSpec f a
    main
        (Aux (Impure f (IOSpec f b)
    p)) -> do x <- f (IOSpec f b) -> VM (Step (IOSpec f b))
    forall a. f a -> VM (Step a)
    forall (f :: * -> *) a. Executable f => f a -> VM (Step a)
    step f (IOSpec f b)
    p
                               case x of
                                 Step IOSpec f b
    y -> VM ()
    resetBlockedThreads VM () -> VM () -> VM ()
    forall a b.
    StateT Store Effect a
    -> StateT Store Effect b -> StateT Store Effect b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >>
                                           ThreadId -> IOSpec f b -> VM ()
    forall (f :: * -> *) a.
    Executable f =>
    ThreadId -> IOSpec f a -> VM ()
    updateSoup ThreadId
    tid IOSpec f b
    y VM () -> StateT Store Effect a -> StateT Store Effect a
    forall a b.
    StateT Store Effect a
    -> StateT Store Effect b -> StateT Store Effect b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >>
                                           IOSpec f a -> StateT Store Effect a
    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 VM () -> StateT Store Effect a -> StateT Store Effect a
    forall a b.
    StateT Store Effect a
    -> StateT Store Effect b -> StateT Store Effect b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >>
                                          IOSpec f a -> StateT Store Effect a
    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 sch <- (Store -> Scheduler) -> StateT Store Effect Scheduler
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets Store -> Scheduler
    scheduler
      (ThreadId total) <- gets nextTid
      let allTids = [Int -> ThreadId
    ThreadId Int
    i | Int
    i <- [Int
    0 .. Int
    total Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1]]
      blockedTids <- gets blockedThreads
      finishedTids <- gets finishedThreads
      let activeThreads = [ThreadId]
    allTids [ThreadId] -> [ThreadId] -> [ThreadId]
    forall a. Eq a => [a] -> [a] -> [a]
    \\ ([ThreadId]
    blockedTids [ThreadId] -> [ThreadId] -> [ThreadId]
    forall a. Eq a => [a] -> [a] -> [a]
    `union` [ThreadId]
    finishedTids)
      let (i,s) = sch (length activeThreads)
      modifyScheduler (const s)
      return (activeThreads !! 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  tid <- VM ThreadId
    getNextThreadId
                        if tid == mainTid
                          then return (mainTid, Main main)
                          else do
                            tsoup <- gets threadSoup
                            case tsoup tid of
                              ThreadStatus
    Finished ->  String -> StateT Store Effect (ThreadId, Process a)
    forall a. String -> a
    internalError
                                String
    "Scheduled finished thread."
                              Running IOSpec f b
    p -> (ThreadId, Process a) -> StateT Store Effect (ThreadId, Process a)
    forall a. a -> StateT Store Effect a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ThreadId
    tid, IOSpec f b -> Process a
    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 = StateT Store Effect a -> Store -> Effect (a, Store)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT
                           (IOSpec f a -> StateT Store Effect a
    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 IOSpec f a -> Scheduler -> Effect (a, Store)
    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)
    _ -> String -> Store
    forall a. HasCallStack => String -> a
    error (String -> Store) -> String -> Store
    forall a b. (a -> b) -> a -> b
    $ String
    "Failed application of Test.IOSpec.execIOSpec.\n" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
                     String
    "Probable cause: your function uses functions such as " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
                     String
    "putChar and getChar. Check the preconditions for calling " String -> ShowS
    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 = ((a, Store) -> a) -> Effect (a, Store) -> Effect a
    forall a b. (a -> b) -> Effect a -> Effect b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (a, Store) -> a
    forall a b. (a, b) -> a
    fst (IOSpec f a -> Scheduler -> Effect (a, Store)
    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 = String -> a
    forall a. HasCallStack => String -> a
    error (String
    "IOSpec.VirtualMachine: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    msg)