{-# LANGUAGE FlexibleContexts, TypeOperators #-}
module Test.IOSpec.IORef
(
IORefS
, IORef
, newIORef
, readIORef
, writeIORef
, modifyIORef
)
where
import Data.Dynamic
import Data.Maybe (fromJust)
import Test.IOSpec.Types
import Test.IOSpec.VirtualMachine
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)
newtype IORef a = IORef Loc
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)
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)
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 ())
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)
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)