    {-# LANGUAGE FlexibleContexts, TypeOperators #-}
    -- | A pure specification of mutable variables.
    module Test.IOSpec.IORef
       (
        -- * The 'IORefS' spec
         IORefS
        -- * Manipulation and creation of IORefs
       , IORef
       , newIORef
       , readIORef
       , writeIORef
       , modifyIORef
       )
       where

    import Data.Dynamic
    import Data.Maybe (fromJust)
    import Test.IOSpec.Types
    import Test.IOSpec.VirtualMachine

    -- The 'IORefS' spec.
    -- | 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  =
         NewIORef Data (Loc -> a)
      |  ReadIORef Loc (Data -> a)
      |  WriteIORef Loc Data a

    instance Functor IORefS where
      fmap :: forall a b. (a -> b) -> IORefS a -> IORefS b
    fmap a -> b
    f (NewIORef Data
    d Loc -> a
    io)     = Data -> (Loc -> b) -> IORefS b
    forall a. Data -> (Loc -> a) -> IORefS a
    NewIORef Data
    d (a -> b
    f (a -> b) -> (Loc -> a) -> Loc -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Loc -> a
    io)
      fmap a -> b
    f (ReadIORef Loc
    l Data -> a
    io)    = Loc -> (Data -> b) -> IORefS b
    forall a. Loc -> (Data -> a) -> IORefS a
    ReadIORef Loc
    l (a -> b
    f (a -> b) -> (Data -> a) -> Data -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Data -> a
    io)
      fmap a -> b
    f (WriteIORef Loc
    l Data
    d a
    io) = Loc -> Data -> b -> IORefS b
    forall a. Loc -> Data -> a -> IORefS a
    WriteIORef Loc
    l Data
    d (a -> b
    f a
    io)

    -- | A mutable variable storing a value of type a. Note that the
    -- types stored by an 'IORef' are assumed to be @Typeable@.
    newtype IORef a = IORef Loc

    -- | The 'newIORef' function creates a new mutable variable.
    newIORef :: (Typeable a, IORefS :<: f) => a -> IOSpec f (IORef a)
    newIORef :: forall a (f :: * -> *).
    (Typeable a, IORefS :<: f) =>
    a -> IOSpec f (IORef a)
    newIORef a
    d = IORefS (IOSpec f (IORef a)) -> IOSpec f (IORef a)
    forall (g :: * -> *) (f :: * -> *) a.
    (g :<: f) =>
    g (IOSpec f a) -> IOSpec f a
    inject (IORefS (IOSpec f (IORef a)) -> IOSpec f (IORef a))
    -> IORefS (IOSpec f (IORef a)) -> IOSpec f (IORef a)
    forall a b. (a -> b) -> a -> b
    $ Data -> (Loc -> IOSpec f (IORef a)) -> IORefS (IOSpec f (IORef a))
    forall a. Data -> (Loc -> a) -> IORefS a
    NewIORef (a -> Data
    forall a. Typeable a => a -> Data
    toDyn a
    d) (IORef a -> IOSpec f (IORef a)
    forall a. a -> IOSpec f a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (IORef a -> IOSpec f (IORef a))
    -> (Loc -> IORef a) -> Loc -> IOSpec f (IORef a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Loc -> IORef a
    forall a. Loc -> IORef a
    IORef)

    -- | The 'readIORef' function reads the value stored in a mutable variable.
    readIORef :: (Typeable a, IORefS :<:f ) => IORef a -> IOSpec f a
    readIORef :: forall a (f :: * -> *).
    (Typeable a, IORefS :<: f) =>
    IORef a -> IOSpec f a
    readIORef (IORef Loc
    l) = IORefS (IOSpec f a) -> IOSpec f a
    forall (g :: * -> *) (f :: * -> *) a.
    (g :<: f) =>
    g (IOSpec f a) -> IOSpec f a
    inject (IORefS (IOSpec f a) -> IOSpec f a)
    -> IORefS (IOSpec f a) -> IOSpec f a
    forall a b. (a -> b) -> a -> b
    $ Loc -> (Data -> IOSpec f a) -> IORefS (IOSpec f a)
    forall a. Loc -> (Data -> a) -> IORefS a
    ReadIORef Loc
    l (a -> IOSpec f a
    forall a. a -> IOSpec f a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> IOSpec f a) -> (Data -> a) -> Data -> IOSpec f a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .  Maybe a -> a
    forall a. HasCallStack => Maybe a -> a
    fromJust (Maybe a -> a) -> (Data -> Maybe a) -> Data -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Data -> Maybe a
    forall a. Typeable a => Data -> Maybe a
    fromDynamic)

    -- | The 'writeIORef' function overwrites the value stored in a
    -- mutable variable.
    writeIORef :: (Typeable a, IORefS :<: f) => IORef a -> a -> IOSpec f ()
    writeIORef :: forall a (f :: * -> *).
    (Typeable a, IORefS :<: f) =>
    IORef a -> a -> IOSpec f ()
    writeIORef (IORef Loc
    l) a
    d = IORefS (IOSpec f ()) -> IOSpec f ()
    forall (g :: * -> *) (f :: * -> *) a.
    (g :<: f) =>
    g (IOSpec f a) -> IOSpec f a
    inject (IORefS (IOSpec f ()) -> IOSpec f ())
    -> IORefS (IOSpec f ()) -> IOSpec f ()
    forall a b. (a -> b) -> a -> b
    $ Loc -> Data -> IOSpec f () -> IORefS (IOSpec f ())
    forall a. Loc -> Data -> a -> IORefS a
    WriteIORef Loc
    l (a -> Data
    forall a. Typeable a => a -> Data
    toDyn a
    d) (() -> IOSpec f ()
    forall a. a -> IOSpec f a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ())

    -- | The 'modifyIORef' function applies a function to the value stored in
    -- and 'IORef'.
    modifyIORef :: (Typeable a, IORefS :<: f)
      => IORef a -> (a -> a) -> IOSpec f ()
    modifyIORef :: forall a (f :: * -> *).
    (Typeable a, IORefS :<: f) =>
    IORef a -> (a -> a) -> IOSpec f ()
    modifyIORef IORef a
    ref a -> a
    f = IORef a -> IOSpec f a
    forall a (f :: * -> *).
    (Typeable a, IORefS :<: f) =>
    IORef a -> IOSpec f a
    readIORef IORef a
    ref IOSpec f a -> (a -> IOSpec f ()) -> IOSpec f ()
    forall a b. IOSpec f a -> (a -> IOSpec f b) -> IOSpec f b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \a
    x -> IORef a -> a -> IOSpec f ()
    forall a (f :: * -> *).
    (Typeable a, IORefS :<: f) =>
    IORef a -> a -> IOSpec f ()
    writeIORef IORef a
    ref (a -> a
    f a
    x)

    -- | The 'Executable' instance for the `IORefS' monad.
    instance Executable IORefS where
      step :: forall a. IORefS a -> VM (Step a)
    step (NewIORef Data
    d Loc -> a
    t)     = do loc <- VM Loc
    alloc
                                   updateHeap loc d
                                   return (Step (t loc))
      step (ReadIORef Loc
    l Data -> a
    t)    = do Loc -> VM (Maybe Data)
    lookupHeap Loc
    l VM (Maybe Data)
    -> (Maybe Data -> StateT Store Effect (Step a))
    -> StateT Store Effect (Step a)
    forall a b.
    StateT Store Effect a
    -> (a -> StateT Store Effect b) -> StateT Store Effect b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \(Just Data
    d) -> do
                                   Step a -> StateT Store Effect (Step a)
    forall a. a -> StateT Store Effect a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> Step a
    forall a. a -> Step a
    Step (Data -> a
    t Data
    d))
      step (WriteIORef Loc
    l Data
    d a
    t) = do Loc -> Data -> VM ()
    updateHeap Loc
    l Data
    d
                                   Step a -> StateT Store Effect (Step a)
    forall a. a -> StateT Store Effect a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> Step a
    forall a. a -> Step a
    Step a
    t)