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

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

data ThreadId = RacyThreadId [Int]
              | ThreadId     [Int]    -- non racy threads have higher priority
  deriving (ThreadId -> ThreadId -> Bool
(ThreadId -> ThreadId -> Bool)
-> (ThreadId -> ThreadId -> Bool) -> Eq ThreadId
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
Eq ThreadId
-> (ThreadId -> ThreadId -> Ordering)
-> (ThreadId -> ThreadId -> Bool)
-> (ThreadId -> ThreadId -> Bool)
-> (ThreadId -> ThreadId -> Bool)
-> (ThreadId -> ThreadId -> Bool)
-> (ThreadId -> ThreadId -> ThreadId)
-> (ThreadId -> ThreadId -> ThreadId)
-> Ord 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
$cp1Ord :: Eq ThreadId
Ord, Int -> ThreadId -> ShowS
[ThreadId] -> ShowS
ThreadId -> String
(Int -> ThreadId -> ShowS)
-> (ThreadId -> String) -> ([ThreadId] -> ShowS) -> Show ThreadId
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 [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
i])
childThreadId (ThreadId     [Int]
is) Int
i = [Int] -> ThreadId
ThreadId     ([Int]
is [Int] -> [Int] -> [Int]
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
(TVarId -> TVarId -> Bool)
-> (TVarId -> TVarId -> Bool) -> Eq TVarId
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
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
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
$cp1Ord :: Eq TVarId
Ord, Int -> TVarId
TVarId -> Int
TVarId -> [TVarId]
TVarId -> TVarId
TVarId -> TVarId -> [TVarId]
TVarId -> TVarId -> TVarId -> [TVarId]
(TVarId -> TVarId)
-> (TVarId -> TVarId)
-> (Int -> TVarId)
-> (TVarId -> Int)
-> (TVarId -> [TVarId])
-> (TVarId -> TVarId -> [TVarId])
-> (TVarId -> TVarId -> [TVarId])
-> (TVarId -> TVarId -> TVarId -> [TVarId])
-> Enum 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
(Int -> TVarId -> ShowS)
-> (TVarId -> String) -> ([TVarId] -> ShowS) -> Show TVarId
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
(TimeoutId -> TimeoutId -> Bool)
-> (TimeoutId -> TimeoutId -> Bool) -> Eq TimeoutId
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
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
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
$cp1Ord :: Eq 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
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
(Int -> TimeoutId -> ShowS)
-> (TimeoutId -> String)
-> ([TimeoutId] -> ShowS)
-> Show TimeoutId
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
(ClockId -> ClockId -> Bool)
-> (ClockId -> ClockId -> Bool) -> Eq ClockId
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
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
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
$cp1Ord :: Eq 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
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
(Int -> VectorClock -> ShowS)
-> (VectorClock -> String)
-> ([VectorClock] -> ShowS)
-> Show VectorClock
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.
       --
       TVar s a -> TVarId
tvarId      :: !TVarId,

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

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

       -- | A stack of undo values. This is only used while executing a
       -- transaction.
       --
       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.
       --
       TVar s a -> STRef s ([ThreadId], Set ThreadId)
tvarBlocked :: !(STRef s ([ThreadId], Set ThreadId)),

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

       -- | Callback to construct a trace which will be attached to the dynamic
       -- trace.
       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

data Deschedule = Yield | Interruptable | Blocked | 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
showList :: [Deschedule] -> ShowS
$cshowList :: [Deschedule] -> ShowS
show :: Deschedule -> String
$cshow :: Deschedule -> String
showsPrec :: Int -> Deschedule -> ShowS
$cshowsPrec :: Int -> Deschedule -> ShowS
Show