{-# LANGUAGE DeriveAnyClass             #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE DerivingVia                #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables        #-}

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

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

import           NoThunks.Class

import           Data.List (intercalate, intersperse)
import           Data.Map (Map)
import qualified Data.Map as Map
import           Data.STRef.Lazy
import           Data.Set (Set)
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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IOSimThreadId -> IOSimThreadId -> Bool
$c/= :: IOSimThreadId -> IOSimThreadId -> Bool
== :: IOSimThreadId -> IOSimThreadId -> Bool
$c== :: IOSimThreadId -> IOSimThreadId -> Bool
Eq, Eq 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
min :: IOSimThreadId -> IOSimThreadId -> IOSimThreadId
$cmin :: IOSimThreadId -> IOSimThreadId -> IOSimThreadId
max :: IOSimThreadId -> IOSimThreadId -> IOSimThreadId
$cmax :: IOSimThreadId -> IOSimThreadId -> IOSimThreadId
>= :: IOSimThreadId -> IOSimThreadId -> Bool
$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
compare :: IOSimThreadId -> IOSimThreadId -> Ordering
$ccompare :: IOSimThreadId -> IOSimThreadId -> Ordering
Ord, Int -> IOSimThreadId -> ShowS
[IOSimThreadId] -> ShowS
IOSimThreadId -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IOSimThreadId] -> ShowS
$cshowList :: [IOSimThreadId] -> ShowS
show :: IOSimThreadId -> String
$cshow :: IOSimThreadId -> String
showsPrec :: Int -> IOSimThreadId -> ShowS
$cshowsPrec :: Int -> IOSimThreadId -> ShowS
Show, 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
$cto :: forall x. Rep IOSimThreadId x -> IOSimThreadId
$cfrom :: forall x. IOSimThreadId -> Rep IOSimThreadId x
Generic)
  deriving anyclass IOSimThreadId -> ()
forall a. (a -> ()) -> NFData a
rnf :: IOSimThreadId -> ()
$crnf :: IOSimThreadId -> ()
NFData
  deriving anyclass Context -> IOSimThreadId -> IO (Maybe ThunkInfo)
Proxy IOSimThreadId -> String
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
showTypeOf :: Proxy IOSimThreadId -> String
$cshowTypeOf :: Proxy IOSimThreadId -> String
wNoThunks :: Context -> IOSimThreadId -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> IOSimThreadId -> IO (Maybe ThunkInfo)
noThunks :: Context -> IOSimThreadId -> IO (Maybe ThunkInfo)
$cnoThunks :: Context -> IOSimThreadId -> IO (Maybe ThunkInfo)
NoThunks

ppIOSimThreadId :: IOSimThreadId -> String
ppIOSimThreadId :: IOSimThreadId -> String
ppIOSimThreadId (RacyThreadId [Int]
as) = String
"Thread {"forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"," (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Int]
as) forall a. [a] -> [a] -> [a]
++String
"}"
ppIOSimThreadId     (ThreadId [Int]
as) = String
"Thread " forall a. [a] -> [a] -> [a]
++ 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 forall a. [a] -> [a] -> [a]
++ [Int
i])
childThreadId (ThreadId     [Int]
is) Int
i = [Int] -> IOSimThreadId
ThreadId     ([Int]
is 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 forall a. Ord a => a -> a -> Bool
< Int
0
                     = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [IOSimThreadId -> String
ppIOSimThreadId IOSimThreadId
tid, String
".-"]
ppStepId (IOSimThreadId
tid, Int
step) = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [IOSimThreadId -> String
ppIOSimThreadId IOSimThreadId
tid, String
".", forall a. Show a => a -> String
show Int
step]


newtype TVarId      = TVarId    Int   deriving (TVarId -> TVarId -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TVarId -> TVarId -> Bool
$c/= :: TVarId -> TVarId -> Bool
== :: TVarId -> TVarId -> Bool
$c== :: TVarId -> TVarId -> Bool
Eq, Eq 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
min :: TVarId -> TVarId -> TVarId
$cmin :: TVarId -> TVarId -> TVarId
max :: TVarId -> TVarId -> TVarId
$cmax :: TVarId -> TVarId -> TVarId
>= :: TVarId -> TVarId -> Bool
$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
compare :: TVarId -> TVarId -> Ordering
$ccompare :: TVarId -> TVarId -> Ordering
Ord, Int -> TVarId
TVarId -> Int
TVarId -> [TVarId]
TVarId -> TVarId
TVarId -> TVarId -> [TVarId]
TVarId -> TVarId -> TVarId -> [TVarId]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: TVarId -> TVarId -> TVarId -> [TVarId]
$cenumFromThenTo :: TVarId -> TVarId -> TVarId -> [TVarId]
enumFromTo :: TVarId -> TVarId -> [TVarId]
$cenumFromTo :: TVarId -> TVarId -> [TVarId]
enumFromThen :: TVarId -> TVarId -> [TVarId]
$cenumFromThen :: TVarId -> TVarId -> [TVarId]
enumFrom :: TVarId -> [TVarId]
$cenumFrom :: TVarId -> [TVarId]
fromEnum :: TVarId -> Int
$cfromEnum :: TVarId -> Int
toEnum :: Int -> TVarId
$ctoEnum :: Int -> TVarId
pred :: TVarId -> TVarId
$cpred :: TVarId -> TVarId
succ :: TVarId -> TVarId
$csucc :: TVarId -> TVarId
Enum, Int -> TVarId -> ShowS
[TVarId] -> ShowS
TVarId -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TVarId] -> ShowS
$cshowList :: [TVarId] -> ShowS
show :: TVarId -> String
$cshow :: TVarId -> String
showsPrec :: Int -> TVarId -> ShowS
$cshowsPrec :: Int -> TVarId -> ShowS
Show)
newtype TimeoutId   = TimeoutId Int   deriving (TimeoutId -> TimeoutId -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TimeoutId -> TimeoutId -> Bool
$c/= :: TimeoutId -> TimeoutId -> Bool
== :: TimeoutId -> TimeoutId -> Bool
$c== :: TimeoutId -> TimeoutId -> Bool
Eq, Eq 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
min :: TimeoutId -> TimeoutId -> TimeoutId
$cmin :: TimeoutId -> TimeoutId -> TimeoutId
max :: TimeoutId -> TimeoutId -> TimeoutId
$cmax :: TimeoutId -> TimeoutId -> TimeoutId
>= :: TimeoutId -> TimeoutId -> Bool
$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
compare :: TimeoutId -> TimeoutId -> Ordering
$ccompare :: TimeoutId -> TimeoutId -> Ordering
Ord, Int -> TimeoutId
TimeoutId -> Int
TimeoutId -> [TimeoutId]
TimeoutId -> TimeoutId
TimeoutId -> TimeoutId -> [TimeoutId]
TimeoutId -> TimeoutId -> TimeoutId -> [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
enumFromThenTo :: TimeoutId -> TimeoutId -> TimeoutId -> [TimeoutId]
$cenumFromThenTo :: TimeoutId -> TimeoutId -> TimeoutId -> [TimeoutId]
enumFromTo :: TimeoutId -> TimeoutId -> [TimeoutId]
$cenumFromTo :: TimeoutId -> TimeoutId -> [TimeoutId]
enumFromThen :: TimeoutId -> TimeoutId -> [TimeoutId]
$cenumFromThen :: TimeoutId -> TimeoutId -> [TimeoutId]
enumFrom :: TimeoutId -> [TimeoutId]
$cenumFrom :: TimeoutId -> [TimeoutId]
fromEnum :: TimeoutId -> Int
$cfromEnum :: TimeoutId -> Int
toEnum :: Int -> TimeoutId
$ctoEnum :: Int -> TimeoutId
pred :: TimeoutId -> TimeoutId
$cpred :: TimeoutId -> TimeoutId
succ :: TimeoutId -> TimeoutId
$csucc :: TimeoutId -> TimeoutId
Enum, Int -> TimeoutId -> ShowS
[TimeoutId] -> ShowS
TimeoutId -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TimeoutId] -> ShowS
$cshowList :: [TimeoutId] -> ShowS
show :: TimeoutId -> String
$cshow :: TimeoutId -> String
showsPrec :: Int -> TimeoutId -> ShowS
$cshowsPrec :: Int -> TimeoutId -> ShowS
Show)
newtype ClockId     = ClockId   [Int] deriving (ClockId -> ClockId -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ClockId -> ClockId -> Bool
$c/= :: ClockId -> ClockId -> Bool
== :: ClockId -> ClockId -> Bool
$c== :: ClockId -> ClockId -> Bool
Eq, Eq 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
min :: ClockId -> ClockId -> ClockId
$cmin :: ClockId -> ClockId -> ClockId
max :: ClockId -> ClockId -> ClockId
$cmax :: ClockId -> ClockId -> ClockId
>= :: ClockId -> ClockId -> Bool
$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
compare :: ClockId -> ClockId -> Ordering
$ccompare :: ClockId -> ClockId -> Ordering
Ord, Int -> ClockId -> ShowS
[ClockId] -> ShowS
ClockId -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ClockId] -> ShowS
$cshowList :: [ClockId] -> ShowS
show :: ClockId -> String
$cshow :: ClockId -> String
showsPrec :: Int -> ClockId -> ShowS
$cshowsPrec :: Int -> ClockId -> ShowS
Show)
newtype VectorClock = VectorClock { VectorClock -> Map IOSimThreadId Int
getVectorClock :: Map IOSimThreadId Int }
  deriving 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
$cto :: forall x. Rep VectorClock x -> VectorClock
$cfrom :: forall x. VectorClock -> Rep VectorClock x
Generic
  deriving Int -> VectorClock -> ShowS
[VectorClock] -> ShowS
VectorClock -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VectorClock] -> ShowS
$cshowList :: [VectorClock] -> ShowS
show :: VectorClock -> String
$cshow :: VectorClock -> String
showsPrec :: Int -> VectorClock -> ShowS
$cshowsPrec :: Int -> VectorClock -> ShowS
Show via Quiet VectorClock

ppVectorClock :: VectorClock -> String
ppVectorClock :: VectorClock -> String
ppVectorClock (VectorClock Map IOSimThreadId Int
m) = String
"VectorClock " forall a. [a] -> [a] -> [a]
++ String
"[" forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a. a -> [a] -> [a]
intersperse String
", " ((IOSimThreadId, Int) -> String
ppStepId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Map k a -> [(k, a)]
Map.toList Map IOSimThreadId Int
m)) 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.
       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 forall a. Eq a => a -> a -> Bool
== TVarId
b

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

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

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

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

--
-- Utils
--

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