{-# 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.CRef n (Maybe a)
}
data ModelCRef n a = ModelCRef
{ crefId :: CRefId
, crefRef :: C.CRef n (Map ThreadId a, Integer, a)
}
data ModelTicket a = ModelTicket
{ ticketCRef :: CRefId
, 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. ANewCRef String a (ModelCRef n a -> Action n)
| forall a. AReadCRef (ModelCRef n a) (a -> Action n)
| forall a. AReadCRefCas (ModelCRef n a) (ModelTicket a -> Action n)
| forall a b. AModCRef (ModelCRef n a) (a -> (a, b)) (b -> Action n)
| forall a b. AModCRefCas (ModelCRef n a) (a -> (a, b)) (b -> Action n)
| forall a. AWriteCRef (ModelCRef n a) a (Action n)
| forall a. ACasCRef (ModelCRef 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 CRefId
| 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 (ANewCRef _ _ _) = WillNewCRef
lookahead (AReadCRef (ModelCRef r _) _) = WillReadCRef r
lookahead (AReadCRefCas (ModelCRef r _) _) = WillReadCRefCas r
lookahead (AModCRef (ModelCRef r _) _ _) = WillModCRef r
lookahead (AModCRefCas (ModelCRef r _) _ _) = WillModCRefCas r
lookahead (AWriteCRef (ModelCRef r _) _ _) = WillWriteCRef r
lookahead (ACasCRef (ModelCRef r _) _ _ _) = WillCasCRef r
lookahead (ACommit t c) = WillCommitCRef 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