{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes #-}
module Test.DejaFu.Conc.Internal.Common where
import Control.Exception (Exception, MaskingState(..))
import qualified Control.Monad.Conc.Class as C
import qualified Control.Monad.Fail as Fail
import Data.Map.Strict (Map)
import Test.DejaFu.Conc.Internal.STM (ModelSTM)
import Test.DejaFu.Types
newtype ModelConc n a = ModelConc { runModelConc :: (a -> Action n) -> Action n }
instance Functor (ModelConc n) where
fmap f m = ModelConc $ \c -> runModelConc m (c . f)
instance Applicative (ModelConc n) where
pure x = ModelConc $ \c -> AReturn $ c x
f <*> v = ModelConc $ \c -> runModelConc f (\g -> runModelConc v (c . g))
instance Monad (ModelConc n) where
return = pure
m >>= k = ModelConc $ \c -> runModelConc m (\x -> runModelConc (k x) c)
fail = Fail.fail
instance Fail.MonadFail (ModelConc n) where
fail e = ModelConc $ \_ -> AThrow (MonadFailException e)
data ModelMVar n a = ModelMVar
{ mvarId :: MVarId
, mvarRef :: C.IORef n (Maybe a)
}
data ModelIORef n a = ModelIORef
{ iorefId :: IORefId
, iorefRef :: C.IORef n (Map ThreadId a, Integer, a)
}
data ModelTicket a = ModelTicket
{ ticketIORef :: IORefId
, ticketWrites :: Integer
, ticketVal :: a
}
data Action n =
AFork String ((forall b. ModelConc n b -> ModelConc n b) -> Action n) (ThreadId -> Action n)
| AForkOS String ((forall b. ModelConc n b -> ModelConc n b) -> Action n) (ThreadId -> Action n)
| AIsBound (Bool -> Action n)
| AMyTId (ThreadId -> Action n)
| AGetNumCapabilities (Int -> Action n)
| ASetNumCapabilities Int (Action n)
| forall a. ANewMVar String (ModelMVar n a -> Action n)
| forall a. APutMVar (ModelMVar n a) a (Action n)
| forall a. ATryPutMVar (ModelMVar n a) a (Bool -> Action n)
| forall a. AReadMVar (ModelMVar n a) (a -> Action n)
| forall a. ATryReadMVar (ModelMVar n a) (Maybe a -> Action n)
| forall a. ATakeMVar (ModelMVar n a) (a -> Action n)
| forall a. ATryTakeMVar (ModelMVar n a) (Maybe a -> Action n)
| forall a. ANewIORef String a (ModelIORef n a -> Action n)
| forall a. AReadIORef (ModelIORef n a) (a -> Action n)
| forall a. AReadIORefCas (ModelIORef n a) (ModelTicket a -> Action n)
| forall a b. AModIORef (ModelIORef n a) (a -> (a, b)) (b -> Action n)
| forall a b. AModIORefCas (ModelIORef n a) (a -> (a, b)) (b -> Action n)
| forall a. AWriteIORef (ModelIORef n a) a (Action n)
| forall a. ACasIORef (ModelIORef n a) (ModelTicket a) a ((Bool, ModelTicket a) -> Action n)
| forall e. Exception e => AThrow e
| forall e. Exception e => AThrowTo ThreadId e (Action n)
| forall a e. Exception e => ACatching (e -> ModelConc n a) (ModelConc n a) (a -> Action n)
| APopCatching (Action n)
| forall a. AMasking MaskingState ((forall b. ModelConc n b -> ModelConc n b) -> ModelConc n a) (a -> Action n)
| AResetMask Bool Bool MaskingState (Action n)
| forall a. AAtom (ModelSTM n a) (a -> Action n)
| ALift (n (Action n))
| AYield (Action n)
| ADelay Int (Action n)
| AReturn (Action n)
| ACommit ThreadId IORefId
| AStop (n ())
| forall a. ASub (ModelConc n a) (Either Failure a -> Action n)
| AStopSub (Action n)
| forall a. ADontCheck (Maybe Int) (ModelConc n a) (a -> Action n)
lookahead :: Action n -> Lookahead
lookahead (AFork _ _ _) = WillFork
lookahead (AForkOS _ _ _) = WillForkOS
lookahead (AIsBound _) = WillIsCurrentThreadBound
lookahead (AMyTId _) = WillMyThreadId
lookahead (AGetNumCapabilities _) = WillGetNumCapabilities
lookahead (ASetNumCapabilities i _) = WillSetNumCapabilities i
lookahead (ANewMVar _ _) = WillNewMVar
lookahead (APutMVar (ModelMVar m _) _ _) = WillPutMVar m
lookahead (ATryPutMVar (ModelMVar m _) _ _) = WillTryPutMVar m
lookahead (AReadMVar (ModelMVar m _) _) = WillReadMVar m
lookahead (ATryReadMVar (ModelMVar m _) _) = WillTryReadMVar m
lookahead (ATakeMVar (ModelMVar m _) _) = WillTakeMVar m
lookahead (ATryTakeMVar (ModelMVar m _) _) = WillTryTakeMVar m
lookahead (ANewIORef _ _ _) = WillNewIORef
lookahead (AReadIORef (ModelIORef r _) _) = WillReadIORef r
lookahead (AReadIORefCas (ModelIORef r _) _) = WillReadIORefCas r
lookahead (AModIORef (ModelIORef r _) _ _) = WillModIORef r
lookahead (AModIORefCas (ModelIORef r _) _ _) = WillModIORefCas r
lookahead (AWriteIORef (ModelIORef r _) _ _) = WillWriteIORef r
lookahead (ACasIORef (ModelIORef r _) _ _ _) = WillCasIORef r
lookahead (ACommit t c) = WillCommitIORef t c
lookahead (AAtom _ _) = WillSTM
lookahead (AThrow _) = WillThrow
lookahead (AThrowTo tid _ _) = WillThrowTo tid
lookahead (ACatching _ _ _) = WillCatching
lookahead (APopCatching _) = WillPopCatching
lookahead (AMasking ms _ _) = WillSetMasking False ms
lookahead (AResetMask b1 b2 ms _) = (if b1 then WillSetMasking else WillResetMasking) b2 ms
lookahead (ALift _) = WillLiftIO
lookahead (AYield _) = WillYield
lookahead (ADelay n _) = WillThreadDelay n
lookahead (AReturn _) = WillReturn
lookahead (AStop _) = WillStop
lookahead (ASub _ _) = WillSubconcurrency
lookahead (AStopSub _) = WillStopSubconcurrency
lookahead (ADontCheck _ _ _) = WillDontCheck