{-# 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 :: (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 :: 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 (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 :: 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 (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 :: 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 (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 :: 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 (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 :: IORefS a -> VM (Step a)
step (NewIORef Data
d Loc -> a
t)     = do Loc
loc <- VM Loc
alloc
                               Loc -> Data -> VM ()
updateHeap Loc
loc Data
d
                               Step a -> VM (Step a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Step a
forall a. a -> Step a
Step (Loc -> a
t Loc
loc))
  step (ReadIORef Loc
l Data -> a
t)    = do Loc -> VM (Maybe Data)
lookupHeap Loc
l VM (Maybe Data) -> (Maybe Data -> VM (Step a)) -> VM (Step a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(Just Data
d) -> do
                               Step a -> VM (Step 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 -> VM (Step a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Step a
forall a. a -> Step a
Step a
t)