{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia        #-}
{-# LANGUAGE RoleAnnotations    #-}

-- | Common types shared between `IOSim` and `IOSimPOR`.
--
module Control.Monad.IOSim.CommonTypes
  ( IOSimThreadId (..)
  , ppIOSimThreadId
  , StepId
  , ppStepId
  , childThreadId
  , setRacyThread
  , TVarId (..)
  , VarId
  , TimeoutId (..)
  , ClockId (..)
  , VectorClock (..)
  , ppVectorClock
  , unTimeoutId
  , ThreadLabel
  , TVarLabel
  , TVar (..)
  , SomeTVar (..)
  , someTVarToLabelled
  , Deschedule (..)
  , ThreadStatus (..)
  , BlockedReason (..)
  , Labelled (..)
  , ppLabelled
  , Unique (..)
    -- * Utils
  , ppList
  ) where

import Control.DeepSeq (NFData (..))
import Control.Monad.Class.MonadSTM (TraceValue)
import Control.Monad.ST.Lazy

import NoThunks.Class

import Data.Hashable
import Data.List (intercalate, intersperse)
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set (Set)
import Data.STRef.Lazy
import GHC.Generics
import Quiet


-- | A thread id.
--
-- /IOSimPOR/: 'RacyThreadId' indicates that this thread is taken into account
-- when discovering races.  A thread is marked as racy iff
-- `Control.Monad.Class.MonadTest.exploreRaces` was
-- executed in it or it's a thread forked by a racy thread.
--
data IOSimThreadId =
    -- | A racy thread (`IOSimPOR` only), shown in the trace with curly braces,
    -- e.g. `Thread {2,3}`.
    RacyThreadId [Int]
    -- | A non racy thread.  They have higher priority than racy threads in
    -- `IOSimPOR` scheduler.
  | ThreadId     [Int]
  deriving stock    (IOSimThreadId -> IOSimThreadId -> Bool
(IOSimThreadId -> IOSimThreadId -> Bool)
-> (IOSimThreadId -> IOSimThreadId -> Bool) -> Eq IOSimThreadId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IOSimThreadId -> IOSimThreadId -> Bool
== :: IOSimThreadId -> IOSimThreadId -> Bool
$c/= :: IOSimThreadId -> IOSimThreadId -> Bool
/= :: IOSimThreadId -> IOSimThreadId -> Bool
Eq, Eq IOSimThreadId
Eq IOSimThreadId =>
(IOSimThreadId -> IOSimThreadId -> Ordering)
-> (IOSimThreadId -> IOSimThreadId -> Bool)
-> (IOSimThreadId -> IOSimThreadId -> Bool)
-> (IOSimThreadId -> IOSimThreadId -> Bool)
-> (IOSimThreadId -> IOSimThreadId -> Bool)
-> (IOSimThreadId -> IOSimThreadId -> IOSimThreadId)
-> (IOSimThreadId -> IOSimThreadId -> IOSimThreadId)
-> Ord IOSimThreadId
IOSimThreadId -> IOSimThreadId -> Bool
IOSimThreadId -> IOSimThreadId -> Ordering
IOSimThreadId -> IOSimThreadId -> IOSimThreadId
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: IOSimThreadId -> IOSimThreadId -> Ordering
compare :: IOSimThreadId -> IOSimThreadId -> Ordering
$c< :: IOSimThreadId -> IOSimThreadId -> Bool
< :: IOSimThreadId -> IOSimThreadId -> Bool
$c<= :: IOSimThreadId -> IOSimThreadId -> Bool
<= :: IOSimThreadId -> IOSimThreadId -> Bool
$c> :: IOSimThreadId -> IOSimThreadId -> Bool
> :: IOSimThreadId -> IOSimThreadId -> Bool
$c>= :: IOSimThreadId -> IOSimThreadId -> Bool
>= :: IOSimThreadId -> IOSimThreadId -> Bool
$cmax :: IOSimThreadId -> IOSimThreadId -> IOSimThreadId
max :: IOSimThreadId -> IOSimThreadId -> IOSimThreadId
$cmin :: IOSimThreadId -> IOSimThreadId -> IOSimThreadId
min :: IOSimThreadId -> IOSimThreadId -> IOSimThreadId
Ord, Int -> IOSimThreadId -> ShowS
[IOSimThreadId] -> ShowS
IOSimThreadId -> String
(Int -> IOSimThreadId -> ShowS)
-> (IOSimThreadId -> String)
-> ([IOSimThreadId] -> ShowS)
-> Show IOSimThreadId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IOSimThreadId -> ShowS
showsPrec :: Int -> IOSimThreadId -> ShowS
$cshow :: IOSimThreadId -> String
show :: IOSimThreadId -> String
$cshowList :: [IOSimThreadId] -> ShowS
showList :: [IOSimThreadId] -> ShowS
Show, (forall x. IOSimThreadId -> Rep IOSimThreadId x)
-> (forall x. Rep IOSimThreadId x -> IOSimThreadId)
-> Generic IOSimThreadId
forall x. Rep IOSimThreadId x -> IOSimThreadId
forall x. IOSimThreadId -> Rep IOSimThreadId x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. IOSimThreadId -> Rep IOSimThreadId x
from :: forall x. IOSimThreadId -> Rep IOSimThreadId x
$cto :: forall x. Rep IOSimThreadId x -> IOSimThreadId
to :: forall x. Rep IOSimThreadId x -> IOSimThreadId
Generic)
  deriving anyclass IOSimThreadId -> ()
(IOSimThreadId -> ()) -> NFData IOSimThreadId
forall a. (a -> ()) -> NFData a
$crnf :: IOSimThreadId -> ()
rnf :: IOSimThreadId -> ()
NFData
  deriving anyclass Context -> IOSimThreadId -> IO (Maybe ThunkInfo)
Proxy IOSimThreadId -> String
(Context -> IOSimThreadId -> IO (Maybe ThunkInfo))
-> (Context -> IOSimThreadId -> IO (Maybe ThunkInfo))
-> (Proxy IOSimThreadId -> String)
-> NoThunks IOSimThreadId
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> IOSimThreadId -> IO (Maybe ThunkInfo)
noThunks :: Context -> IOSimThreadId -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> IOSimThreadId -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> IOSimThreadId -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy IOSimThreadId -> String
showTypeOf :: Proxy IOSimThreadId -> String
NoThunks

instance Hashable IOSimThreadId

ppIOSimThreadId :: IOSimThreadId -> String
ppIOSimThreadId :: IOSimThreadId -> String
ppIOSimThreadId (RacyThreadId [Int]
as) = String
"Thread {"String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> Context -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Int -> String) -> [Int] -> Context
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show [Int]
as) String -> ShowS
forall a. [a] -> [a] -> [a]
++String
"}"
ppIOSimThreadId     (ThreadId [Int]
as) = String
"Thread " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Int] -> String
forall a. Show a => a -> String
show [Int]
as

childThreadId :: IOSimThreadId -> Int -> IOSimThreadId
childThreadId :: IOSimThreadId -> Int -> IOSimThreadId
childThreadId (RacyThreadId [Int]
is) Int
i = [Int] -> IOSimThreadId
RacyThreadId ([Int]
is [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
i])
childThreadId (ThreadId     [Int]
is) Int
i = [Int] -> IOSimThreadId
ThreadId     ([Int]
is [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
i])

setRacyThread :: IOSimThreadId -> IOSimThreadId
setRacyThread :: IOSimThreadId -> IOSimThreadId
setRacyThread (ThreadId [Int]
is)      = [Int] -> IOSimThreadId
RacyThreadId [Int]
is
setRacyThread tid :: IOSimThreadId
tid@RacyThreadId{} = IOSimThreadId
tid

-- | Execution step in `IOSimPOR` is identified by the thread id and
-- a monotonically increasing number (thread specific).
--
type StepId = (IOSimThreadId, Int)

ppStepId :: (IOSimThreadId, Int) -> String
ppStepId :: (IOSimThreadId, Int) -> String
ppStepId (IOSimThreadId
tid, Int
step) | Int
step Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
                     = Context -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [IOSimThreadId -> String
ppIOSimThreadId IOSimThreadId
tid, String
".-"]
ppStepId (IOSimThreadId
tid, Int
step) = Context -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [IOSimThreadId -> String
ppIOSimThreadId IOSimThreadId
tid, String
".", Int -> String
forall a. Show a => a -> String
show Int
step]


type VarId = Int
-- | 'TVar's are used to emulate other shared variables. Each one comes with
-- its own id constructor.
data TVarId =
    TVarId  !VarId
    -- ^ a `TVar`
  | TMVarId !VarId
    -- ^ a `TMVar` simulated by a `TVar`.
  | MVarId  !VarId
    -- ^ an `MVar` simulated by a `TVar`.
  | TQueueId !VarId
    -- ^ a 'TQueue` simulated by a `TVar`.
  | TBQueueId !VarId
    -- ^ a 'TBQueue` simulated by a `TVar`.
  | TSemId !VarId
    -- ^ a 'TSem` simulated by a `TVar`.
  -- TODO: `TChan`
  deriving (TVarId -> TVarId -> Bool
(TVarId -> TVarId -> Bool)
-> (TVarId -> TVarId -> Bool) -> Eq TVarId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TVarId -> TVarId -> Bool
== :: TVarId -> TVarId -> Bool
$c/= :: TVarId -> TVarId -> Bool
/= :: TVarId -> TVarId -> Bool
Eq, Eq TVarId
Eq TVarId =>
(TVarId -> TVarId -> Ordering)
-> (TVarId -> TVarId -> Bool)
-> (TVarId -> TVarId -> Bool)
-> (TVarId -> TVarId -> Bool)
-> (TVarId -> TVarId -> Bool)
-> (TVarId -> TVarId -> TVarId)
-> (TVarId -> TVarId -> TVarId)
-> Ord TVarId
TVarId -> TVarId -> Bool
TVarId -> TVarId -> Ordering
TVarId -> TVarId -> TVarId
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: TVarId -> TVarId -> Ordering
compare :: TVarId -> TVarId -> Ordering
$c< :: TVarId -> TVarId -> Bool
< :: TVarId -> TVarId -> Bool
$c<= :: TVarId -> TVarId -> Bool
<= :: TVarId -> TVarId -> Bool
$c> :: TVarId -> TVarId -> Bool
> :: TVarId -> TVarId -> Bool
$c>= :: TVarId -> TVarId -> Bool
>= :: TVarId -> TVarId -> Bool
$cmax :: TVarId -> TVarId -> TVarId
max :: TVarId -> TVarId -> TVarId
$cmin :: TVarId -> TVarId -> TVarId
min :: TVarId -> TVarId -> TVarId
Ord, Int -> TVarId -> ShowS
[TVarId] -> ShowS
TVarId -> String
(Int -> TVarId -> ShowS)
-> (TVarId -> String) -> ([TVarId] -> ShowS) -> Show TVarId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TVarId -> ShowS
showsPrec :: Int -> TVarId -> ShowS
$cshow :: TVarId -> String
show :: TVarId -> String
$cshowList :: [TVarId] -> ShowS
showList :: [TVarId] -> ShowS
Show)
newtype TimeoutId   = TimeoutId Int   deriving (TimeoutId -> TimeoutId -> Bool
(TimeoutId -> TimeoutId -> Bool)
-> (TimeoutId -> TimeoutId -> Bool) -> Eq TimeoutId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TimeoutId -> TimeoutId -> Bool
== :: TimeoutId -> TimeoutId -> Bool
$c/= :: TimeoutId -> TimeoutId -> Bool
/= :: TimeoutId -> TimeoutId -> Bool
Eq, Eq TimeoutId
Eq TimeoutId =>
(TimeoutId -> TimeoutId -> Ordering)
-> (TimeoutId -> TimeoutId -> Bool)
-> (TimeoutId -> TimeoutId -> Bool)
-> (TimeoutId -> TimeoutId -> Bool)
-> (TimeoutId -> TimeoutId -> Bool)
-> (TimeoutId -> TimeoutId -> TimeoutId)
-> (TimeoutId -> TimeoutId -> TimeoutId)
-> Ord TimeoutId
TimeoutId -> TimeoutId -> Bool
TimeoutId -> TimeoutId -> Ordering
TimeoutId -> TimeoutId -> TimeoutId
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: TimeoutId -> TimeoutId -> Ordering
compare :: TimeoutId -> TimeoutId -> Ordering
$c< :: TimeoutId -> TimeoutId -> Bool
< :: TimeoutId -> TimeoutId -> Bool
$c<= :: TimeoutId -> TimeoutId -> Bool
<= :: TimeoutId -> TimeoutId -> Bool
$c> :: TimeoutId -> TimeoutId -> Bool
> :: TimeoutId -> TimeoutId -> Bool
$c>= :: TimeoutId -> TimeoutId -> Bool
>= :: TimeoutId -> TimeoutId -> Bool
$cmax :: TimeoutId -> TimeoutId -> TimeoutId
max :: TimeoutId -> TimeoutId -> TimeoutId
$cmin :: TimeoutId -> TimeoutId -> TimeoutId
min :: TimeoutId -> TimeoutId -> TimeoutId
Ord, Int -> TimeoutId
TimeoutId -> Int
TimeoutId -> [TimeoutId]
TimeoutId -> TimeoutId
TimeoutId -> TimeoutId -> [TimeoutId]
TimeoutId -> TimeoutId -> TimeoutId -> [TimeoutId]
(TimeoutId -> TimeoutId)
-> (TimeoutId -> TimeoutId)
-> (Int -> TimeoutId)
-> (TimeoutId -> Int)
-> (TimeoutId -> [TimeoutId])
-> (TimeoutId -> TimeoutId -> [TimeoutId])
-> (TimeoutId -> TimeoutId -> [TimeoutId])
-> (TimeoutId -> TimeoutId -> TimeoutId -> [TimeoutId])
-> Enum TimeoutId
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: TimeoutId -> TimeoutId
succ :: TimeoutId -> TimeoutId
$cpred :: TimeoutId -> TimeoutId
pred :: TimeoutId -> TimeoutId
$ctoEnum :: Int -> TimeoutId
toEnum :: Int -> TimeoutId
$cfromEnum :: TimeoutId -> Int
fromEnum :: TimeoutId -> Int
$cenumFrom :: TimeoutId -> [TimeoutId]
enumFrom :: TimeoutId -> [TimeoutId]
$cenumFromThen :: TimeoutId -> TimeoutId -> [TimeoutId]
enumFromThen :: TimeoutId -> TimeoutId -> [TimeoutId]
$cenumFromTo :: TimeoutId -> TimeoutId -> [TimeoutId]
enumFromTo :: TimeoutId -> TimeoutId -> [TimeoutId]
$cenumFromThenTo :: TimeoutId -> TimeoutId -> TimeoutId -> [TimeoutId]
enumFromThenTo :: TimeoutId -> TimeoutId -> TimeoutId -> [TimeoutId]
Enum, Int -> TimeoutId -> ShowS
[TimeoutId] -> ShowS
TimeoutId -> String
(Int -> TimeoutId -> ShowS)
-> (TimeoutId -> String)
-> ([TimeoutId] -> ShowS)
-> Show TimeoutId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TimeoutId -> ShowS
showsPrec :: Int -> TimeoutId -> ShowS
$cshow :: TimeoutId -> String
show :: TimeoutId -> String
$cshowList :: [TimeoutId] -> ShowS
showList :: [TimeoutId] -> ShowS
Show)
newtype ClockId     = ClockId   [Int] deriving (ClockId -> ClockId -> Bool
(ClockId -> ClockId -> Bool)
-> (ClockId -> ClockId -> Bool) -> Eq ClockId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ClockId -> ClockId -> Bool
== :: ClockId -> ClockId -> Bool
$c/= :: ClockId -> ClockId -> Bool
/= :: ClockId -> ClockId -> Bool
Eq, Eq ClockId
Eq ClockId =>
(ClockId -> ClockId -> Ordering)
-> (ClockId -> ClockId -> Bool)
-> (ClockId -> ClockId -> Bool)
-> (ClockId -> ClockId -> Bool)
-> (ClockId -> ClockId -> Bool)
-> (ClockId -> ClockId -> ClockId)
-> (ClockId -> ClockId -> ClockId)
-> Ord ClockId
ClockId -> ClockId -> Bool
ClockId -> ClockId -> Ordering
ClockId -> ClockId -> ClockId
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ClockId -> ClockId -> Ordering
compare :: ClockId -> ClockId -> Ordering
$c< :: ClockId -> ClockId -> Bool
< :: ClockId -> ClockId -> Bool
$c<= :: ClockId -> ClockId -> Bool
<= :: ClockId -> ClockId -> Bool
$c> :: ClockId -> ClockId -> Bool
> :: ClockId -> ClockId -> Bool
$c>= :: ClockId -> ClockId -> Bool
>= :: ClockId -> ClockId -> Bool
$cmax :: ClockId -> ClockId -> ClockId
max :: ClockId -> ClockId -> ClockId
$cmin :: ClockId -> ClockId -> ClockId
min :: ClockId -> ClockId -> ClockId
Ord, Int -> ClockId -> ShowS
[ClockId] -> ShowS
ClockId -> String
(Int -> ClockId -> ShowS)
-> (ClockId -> String) -> ([ClockId] -> ShowS) -> Show ClockId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ClockId -> ShowS
showsPrec :: Int -> ClockId -> ShowS
$cshow :: ClockId -> String
show :: ClockId -> String
$cshowList :: [ClockId] -> ShowS
showList :: [ClockId] -> ShowS
Show)
newtype VectorClock = VectorClock { VectorClock -> Map IOSimThreadId Int
getVectorClock :: Map IOSimThreadId Int }
  deriving (forall x. VectorClock -> Rep VectorClock x)
-> (forall x. Rep VectorClock x -> VectorClock)
-> Generic VectorClock
forall x. Rep VectorClock x -> VectorClock
forall x. VectorClock -> Rep VectorClock x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. VectorClock -> Rep VectorClock x
from :: forall x. VectorClock -> Rep VectorClock x
$cto :: forall x. Rep VectorClock x -> VectorClock
to :: forall x. Rep VectorClock x -> VectorClock
Generic
  deriving Int -> VectorClock -> ShowS
[VectorClock] -> ShowS
VectorClock -> String
(Int -> VectorClock -> ShowS)
-> (VectorClock -> String)
-> ([VectorClock] -> ShowS)
-> Show VectorClock
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> VectorClock -> ShowS
showsPrec :: Int -> VectorClock -> ShowS
$cshow :: VectorClock -> String
show :: VectorClock -> String
$cshowList :: [VectorClock] -> ShowS
showList :: [VectorClock] -> ShowS
Show via Quiet VectorClock

ppVectorClock :: VectorClock -> String
ppVectorClock :: VectorClock -> String
ppVectorClock (VectorClock Map IOSimThreadId Int
m) = String
"VectorClock " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Context -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (String -> Context -> Context
forall a. a -> [a] -> [a]
intersperse String
", " ((IOSimThreadId, Int) -> String
ppStepId ((IOSimThreadId, Int) -> String)
-> [(IOSimThreadId, Int)] -> Context
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map IOSimThreadId Int -> [(IOSimThreadId, Int)]
forall k a. Map k a -> [(k, a)]
Map.toList Map IOSimThreadId Int
m)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"

unTimeoutId :: TimeoutId -> Int
unTimeoutId :: TimeoutId -> Int
unTimeoutId (TimeoutId Int
a) = Int
a

type ThreadLabel = String
type TVarLabel   = String

data TVar s a = TVar {

       -- | The identifier of this var.
       --
       forall s a. TVar s a -> TVarId
tvarId      :: !TVarId,

       -- | Label.
       forall s a. TVar s a -> STRef s (Maybe String)
tvarLabel   :: !(STRef s (Maybe TVarLabel)),

       -- | The var's current value
       --
       forall s a. TVar s a -> STRef s a
tvarCurrent :: !(STRef s a),

       -- | A stack of undo values. This is only used while executing a
       -- transaction.
       --
       forall s a. TVar s a -> STRef s [a]
tvarUndo    :: !(STRef s [a]),

       -- | Thread Ids of threads blocked on a read of this var. It is
       -- represented in reverse order of thread wakeup, without duplicates.
       --
       -- To avoid duplicates efficiently, the operations rely on a copy of the
       -- thread Ids represented as a set.
       --
       forall s a.
TVar s a -> STRef s ([IOSimThreadId], Set IOSimThreadId)
tvarBlocked :: !(STRef s ([IOSimThreadId], Set IOSimThreadId)),

       -- | The vector clock of the current value.
       --
       forall s a. TVar s a -> STRef s VectorClock
tvarVClock  :: !(STRef s VectorClock),

       -- | Callback to construct a trace which will be attached to the dynamic
       -- trace each time the `TVar` is committed.
       forall s a.
TVar s a -> STRef s (Maybe (Maybe a -> a -> ST s TraceValue))
tvarTrace   :: !(STRef s (Maybe (Maybe a -> a -> ST s TraceValue)))
     }

instance Eq (TVar s a) where
    TVar {tvarId :: forall s a. TVar s a -> TVarId
tvarId = TVarId
a} == :: TVar s a -> TVar s a -> Bool
== TVar {tvarId :: forall s a. TVar s a -> TVarId
tvarId = TVarId
b} = TVarId
a TVarId -> TVarId -> Bool
forall a. Eq a => a -> a -> Bool
== TVarId
b

data SomeTVar s where
  SomeTVar :: !(TVar s a) -> SomeTVar s

someTVarToLabelled :: SomeTVar s -> ST s (Labelled (SomeTVar s))
someTVarToLabelled :: forall s. SomeTVar s -> ST s (Labelled (SomeTVar s))
someTVarToLabelled tv :: SomeTVar s
tv@(SomeTVar TVar s a
var) = do
  lbl <- STRef s (Maybe String) -> ST s (Maybe String)
forall s a. STRef s a -> ST s a
readSTRef (TVar s a -> STRef s (Maybe String)
forall s a. TVar s a -> STRef s (Maybe String)
tvarLabel TVar s a
var)
  pure (Labelled tv lbl)

data Deschedule = Yield
                | Interruptable
                | Blocked BlockedReason
                | Terminated
                | Sleep
  deriving Int -> Deschedule -> ShowS
[Deschedule] -> ShowS
Deschedule -> String
(Int -> Deschedule -> ShowS)
-> (Deschedule -> String)
-> ([Deschedule] -> ShowS)
-> Show Deschedule
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Deschedule -> ShowS
showsPrec :: Int -> Deschedule -> ShowS
$cshow :: Deschedule -> String
show :: Deschedule -> String
$cshowList :: [Deschedule] -> ShowS
showList :: [Deschedule] -> ShowS
Show

data ThreadStatus = ThreadRunning
                  | ThreadBlocked BlockedReason
                  | ThreadDone
  deriving (ThreadStatus -> ThreadStatus -> Bool
(ThreadStatus -> ThreadStatus -> Bool)
-> (ThreadStatus -> ThreadStatus -> Bool) -> Eq ThreadStatus
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ThreadStatus -> ThreadStatus -> Bool
== :: ThreadStatus -> ThreadStatus -> Bool
$c/= :: ThreadStatus -> ThreadStatus -> Bool
/= :: ThreadStatus -> ThreadStatus -> Bool
Eq, Int -> ThreadStatus -> ShowS
[ThreadStatus] -> ShowS
ThreadStatus -> String
(Int -> ThreadStatus -> ShowS)
-> (ThreadStatus -> String)
-> ([ThreadStatus] -> ShowS)
-> Show ThreadStatus
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ThreadStatus -> ShowS
showsPrec :: Int -> ThreadStatus -> ShowS
$cshow :: ThreadStatus -> String
show :: ThreadStatus -> String
$cshowList :: [ThreadStatus] -> ShowS
showList :: [ThreadStatus] -> ShowS
Show)

data BlockedReason = BlockedOnSTM
                   | BlockedOnDelay
                   | BlockedOnThrowTo
  deriving (BlockedReason -> BlockedReason -> Bool
(BlockedReason -> BlockedReason -> Bool)
-> (BlockedReason -> BlockedReason -> Bool) -> Eq BlockedReason
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BlockedReason -> BlockedReason -> Bool
== :: BlockedReason -> BlockedReason -> Bool
$c/= :: BlockedReason -> BlockedReason -> Bool
/= :: BlockedReason -> BlockedReason -> Bool
Eq, Int -> BlockedReason -> ShowS
[BlockedReason] -> ShowS
BlockedReason -> String
(Int -> BlockedReason -> ShowS)
-> (BlockedReason -> String)
-> ([BlockedReason] -> ShowS)
-> Show BlockedReason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BlockedReason -> ShowS
showsPrec :: Int -> BlockedReason -> ShowS
$cshow :: BlockedReason -> String
show :: BlockedReason -> String
$cshowList :: [BlockedReason] -> ShowS
showList :: [BlockedReason] -> ShowS
Show)

-- | A labelled value.
--
-- For example 'labelThread' or `labelTVar' will insert a label to `IOSimThreadId`
-- (or `TVarId`).
data Labelled a = Labelled {
    forall a. Labelled a -> a
l_labelled :: !a,
    forall a. Labelled a -> Maybe String
l_label    :: !(Maybe String)
  }
  deriving (Labelled a -> Labelled a -> Bool
(Labelled a -> Labelled a -> Bool)
-> (Labelled a -> Labelled a -> Bool) -> Eq (Labelled a)
forall a. Eq a => Labelled a -> Labelled a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Labelled a -> Labelled a -> Bool
== :: Labelled a -> Labelled a -> Bool
$c/= :: forall a. Eq a => Labelled a -> Labelled a -> Bool
/= :: Labelled a -> Labelled a -> Bool
Eq, Eq (Labelled a)
Eq (Labelled a) =>
(Labelled a -> Labelled a -> Ordering)
-> (Labelled a -> Labelled a -> Bool)
-> (Labelled a -> Labelled a -> Bool)
-> (Labelled a -> Labelled a -> Bool)
-> (Labelled a -> Labelled a -> Bool)
-> (Labelled a -> Labelled a -> Labelled a)
-> (Labelled a -> Labelled a -> Labelled a)
-> Ord (Labelled a)
Labelled a -> Labelled a -> Bool
Labelled a -> Labelled a -> Ordering
Labelled a -> Labelled a -> Labelled a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Labelled a)
forall a. Ord a => Labelled a -> Labelled a -> Bool
forall a. Ord a => Labelled a -> Labelled a -> Ordering
forall a. Ord a => Labelled a -> Labelled a -> Labelled a
$ccompare :: forall a. Ord a => Labelled a -> Labelled a -> Ordering
compare :: Labelled a -> Labelled a -> Ordering
$c< :: forall a. Ord a => Labelled a -> Labelled a -> Bool
< :: Labelled a -> Labelled a -> Bool
$c<= :: forall a. Ord a => Labelled a -> Labelled a -> Bool
<= :: Labelled a -> Labelled a -> Bool
$c> :: forall a. Ord a => Labelled a -> Labelled a -> Bool
> :: Labelled a -> Labelled a -> Bool
$c>= :: forall a. Ord a => Labelled a -> Labelled a -> Bool
>= :: Labelled a -> Labelled a -> Bool
$cmax :: forall a. Ord a => Labelled a -> Labelled a -> Labelled a
max :: Labelled a -> Labelled a -> Labelled a
$cmin :: forall a. Ord a => Labelled a -> Labelled a -> Labelled a
min :: Labelled a -> Labelled a -> Labelled a
Ord, (forall x. Labelled a -> Rep (Labelled a) x)
-> (forall x. Rep (Labelled a) x -> Labelled a)
-> Generic (Labelled a)
forall x. Rep (Labelled a) x -> Labelled a
forall x. Labelled a -> Rep (Labelled a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Labelled a) x -> Labelled a
forall a x. Labelled a -> Rep (Labelled a) x
$cfrom :: forall a x. Labelled a -> Rep (Labelled a) x
from :: forall x. Labelled a -> Rep (Labelled a) x
$cto :: forall a x. Rep (Labelled a) x -> Labelled a
to :: forall x. Rep (Labelled a) x -> Labelled a
Generic, (forall a b. (a -> b) -> Labelled a -> Labelled b)
-> (forall a b. a -> Labelled b -> Labelled a) -> Functor Labelled
forall a b. a -> Labelled b -> Labelled a
forall a b. (a -> b) -> Labelled a -> Labelled b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Labelled a -> Labelled b
fmap :: forall a b. (a -> b) -> Labelled a -> Labelled b
$c<$ :: forall a b. a -> Labelled b -> Labelled a
<$ :: forall a b. a -> Labelled b -> Labelled a
Functor)
  deriving Int -> Labelled a -> ShowS
[Labelled a] -> ShowS
Labelled a -> String
(Int -> Labelled a -> ShowS)
-> (Labelled a -> String)
-> ([Labelled a] -> ShowS)
-> Show (Labelled a)
forall a. Show a => Int -> Labelled a -> ShowS
forall a. Show a => [Labelled a] -> ShowS
forall a. Show a => Labelled a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Labelled a -> ShowS
showsPrec :: Int -> Labelled a -> ShowS
$cshow :: forall a. Show a => Labelled a -> String
show :: Labelled a -> String
$cshowList :: forall a. Show a => [Labelled a] -> ShowS
showList :: [Labelled a] -> ShowS
Show via Quiet (Labelled a)

ppLabelled :: (a -> String) -> Labelled a -> String
ppLabelled :: forall a. (a -> String) -> Labelled a -> String
ppLabelled a -> String
pp Labelled { l_labelled :: forall a. Labelled a -> a
l_labelled = a
a, l_label :: forall a. Labelled a -> Maybe String
l_label = Maybe String
Nothing  } = a -> String
pp a
a
ppLabelled a -> String
pp Labelled { l_labelled :: forall a. Labelled a -> a
l_labelled = a
a, l_label :: forall a. Labelled a -> Maybe String
l_label = Just String
lbl } = Context -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"Labelled ", a -> String
pp a
a, String
" ", String
lbl]

-- | Abstract unique symbols à la "Data.Unique".
newtype Unique s = MkUnique{ forall {k} (s :: k). Unique s -> Integer
unMkUnique :: Integer }
  deriving stock   (Unique s -> Unique s -> Bool
(Unique s -> Unique s -> Bool)
-> (Unique s -> Unique s -> Bool) -> Eq (Unique s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (s :: k). Unique s -> Unique s -> Bool
$c== :: forall k (s :: k). Unique s -> Unique s -> Bool
== :: Unique s -> Unique s -> Bool
$c/= :: forall k (s :: k). Unique s -> Unique s -> Bool
/= :: Unique s -> Unique s -> Bool
Eq, Eq (Unique s)
Eq (Unique s) =>
(Unique s -> Unique s -> Ordering)
-> (Unique s -> Unique s -> Bool)
-> (Unique s -> Unique s -> Bool)
-> (Unique s -> Unique s -> Bool)
-> (Unique s -> Unique s -> Bool)
-> (Unique s -> Unique s -> Unique s)
-> (Unique s -> Unique s -> Unique s)
-> Ord (Unique s)
Unique s -> Unique s -> Bool
Unique s -> Unique s -> Ordering
Unique s -> Unique s -> Unique s
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (s :: k). Eq (Unique s)
forall k (s :: k). Unique s -> Unique s -> Bool
forall k (s :: k). Unique s -> Unique s -> Ordering
forall k (s :: k). Unique s -> Unique s -> Unique s
$ccompare :: forall k (s :: k). Unique s -> Unique s -> Ordering
compare :: Unique s -> Unique s -> Ordering
$c< :: forall k (s :: k). Unique s -> Unique s -> Bool
< :: Unique s -> Unique s -> Bool
$c<= :: forall k (s :: k). Unique s -> Unique s -> Bool
<= :: Unique s -> Unique s -> Bool
$c> :: forall k (s :: k). Unique s -> Unique s -> Bool
> :: Unique s -> Unique s -> Bool
$c>= :: forall k (s :: k). Unique s -> Unique s -> Bool
>= :: Unique s -> Unique s -> Bool
$cmax :: forall k (s :: k). Unique s -> Unique s -> Unique s
max :: Unique s -> Unique s -> Unique s
$cmin :: forall k (s :: k). Unique s -> Unique s -> Unique s
min :: Unique s -> Unique s -> Unique s
Ord)
  deriving newtype Unique s -> ()
(Unique s -> ()) -> NFData (Unique s)
forall a. (a -> ()) -> NFData a
forall k (s :: k). Unique s -> ()
$crnf :: forall k (s :: k). Unique s -> ()
rnf :: Unique s -> ()
NFData
type role Unique nominal

instance Hashable (Unique s) where
  hash :: Unique s -> Int
hash = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> (Unique s -> Integer) -> Unique s -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unique s -> Integer
forall {k} (s :: k). Unique s -> Integer
unMkUnique
  hashWithSalt :: Int -> Unique s -> Int
hashWithSalt = Int -> Unique s -> Int
forall a. Hashable a => Int -> a -> Int
defaultHashWithSalt

--
-- Utils
--

ppList :: (a -> String) -> [a] -> String
ppList :: forall a. (a -> String) -> [a] -> String
ppList a -> String
pp [a]
as = String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Context -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (String -> Context -> Context
forall a. a -> [a] -> [a]
intersperse String
", " ((a -> String) -> [a] -> Context
forall a b. (a -> b) -> [a] -> [b]
map a -> String
pp [a]
as)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"