{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables        #-}

-- | Common types shared between `IOSim` and `IOSimPOR`.
--
module Control.Monad.IOSim.CommonTypes where

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

import           Data.Map (Map)
import           Data.STRef.Lazy
import           Data.Set (Set)


-- | 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 ThreadId = RacyThreadId [Int]
              | ThreadId     [Int]    -- non racy threads have higher priority
  deriving (ThreadId -> ThreadId -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ThreadId -> ThreadId -> Bool
$c/= :: ThreadId -> ThreadId -> Bool
== :: ThreadId -> ThreadId -> Bool
$c== :: ThreadId -> ThreadId -> Bool
Eq, Eq ThreadId
ThreadId -> ThreadId -> Bool
ThreadId -> ThreadId -> Ordering
ThreadId -> ThreadId -> ThreadId
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 :: ThreadId -> ThreadId -> ThreadId
$cmin :: ThreadId -> ThreadId -> ThreadId
max :: ThreadId -> ThreadId -> ThreadId
$cmax :: ThreadId -> ThreadId -> ThreadId
>= :: ThreadId -> ThreadId -> Bool
$c>= :: ThreadId -> ThreadId -> Bool
> :: ThreadId -> ThreadId -> Bool
$c> :: ThreadId -> ThreadId -> Bool
<= :: ThreadId -> ThreadId -> Bool
$c<= :: ThreadId -> ThreadId -> Bool
< :: ThreadId -> ThreadId -> Bool
$c< :: ThreadId -> ThreadId -> Bool
compare :: ThreadId -> ThreadId -> Ordering
$ccompare :: ThreadId -> ThreadId -> Ordering
Ord, Int -> ThreadId -> ShowS
[ThreadId] -> ShowS
ThreadId -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ThreadId] -> ShowS
$cshowList :: [ThreadId] -> ShowS
show :: ThreadId -> String
$cshow :: ThreadId -> String
showsPrec :: Int -> ThreadId -> ShowS
$cshowsPrec :: Int -> ThreadId -> ShowS
Show)

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

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


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 ThreadId Int
getVectorClock :: Map ThreadId Int }
  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

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 ([ThreadId], Set ThreadId)
tvarBlocked :: !(STRef s ([ThreadId], Set ThreadId)),

       -- | 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
                   | BlockedOnOther
  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)