{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
module Test.DejaFu.SCT.Internal where
import Data.Coerce (Coercible, coerce)
import qualified Data.IntMap.Strict as I
import Data.List (find, mapAccumL)
import Data.Maybe (fromMaybe)
import GHC.Stack (HasCallStack)
import Test.DejaFu.Conc
import Test.DejaFu.Conc.Internal (Context(..))
import Test.DejaFu.Conc.Internal.Memory (commitThreadId)
import Test.DejaFu.Conc.Internal.Program
import Test.DejaFu.Internal
import Test.DejaFu.Schedule (Scheduler(..))
import Test.DejaFu.SCT.Internal.DPOR
import Test.DejaFu.Types
import Test.DejaFu.Utils
sct :: (MonadDejaFu n, HasCallStack)
=> Settings n a
-> ([ThreadId] -> s)
-> (s -> Maybe t)
-> (ConcurrencyState -> (Scheduler g -> g -> n (Either Condition a, g, Trace)) -> s -> t -> n (s, Maybe (Either Condition a, Trace)))
-> Program pty n a
-> n [(Either Condition a, Trace)]
sct :: forall (n :: * -> *) a s t g pty.
(MonadDejaFu n, HasCallStack) =>
Settings n a
-> ([ThreadId] -> s)
-> (s -> Maybe t)
-> (ConcurrencyState
-> (Scheduler g -> g -> n (Either Condition a, g, Trace))
-> s
-> t
-> n (s, Maybe (Either Condition a, Trace)))
-> Program pty n a
-> n [(Either Condition a, Trace)]
sct Settings n a
settings [ThreadId] -> s
s0 s -> Maybe t
sfun ConcurrencyState
-> (Scheduler g -> g -> n (Either Condition a, g, Trace))
-> s
-> t
-> n (s, Maybe (Either Condition a, Trace))
srun Program pty n a
conc = Program pty n a
-> n (Maybe (Either Condition (Snapshot pty n a), Trace))
forall (n :: * -> *) pty a.
MonadDejaFu n =>
Program pty n a
-> n (Maybe (Either Condition (Snapshot pty n a), Trace))
recordSnapshot Program pty n a
conc n (Maybe (Either Condition (Snapshot pty n a), Trace))
-> (Maybe (Either Condition (Snapshot pty n a), Trace)
-> n [(Either Condition a, Trace)])
-> n [(Either Condition a, Trace)]
forall a b. n a -> (a -> n b) -> n b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just (Right Snapshot pty n a
snap, Trace
_) -> Snapshot pty n a -> n [(Either Condition a, Trace)]
forall {pty}. Snapshot pty n a -> n [(Either Condition a, Trace)]
sct'Snap Snapshot pty n a
snap
Just (Left Condition
f, Trace
trace) -> [(Either Condition a, Trace)] -> n [(Either Condition a, Trace)]
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Condition -> Either Condition a
forall a b. a -> Either a b
Left Condition
f, Trace
trace)]
Maybe (Either Condition (Snapshot pty n a), Trace)
Nothing -> n [(Either Condition a, Trace)]
sct'Full
where
sct'Full :: n [(Either Condition a, Trace)]
sct'Full = Settings n a
-> ConcurrencyState
-> s
-> (s -> Maybe t)
-> (s -> t -> n (s, Maybe (Either Condition a, Trace)))
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> n [(Either Condition a, Trace)]
forall (n :: * -> *) a s t.
(MonadDejaFu n, HasCallStack) =>
Settings n a
-> ConcurrencyState
-> s
-> (s -> Maybe t)
-> (s -> t -> n (s, Maybe (Either Condition a, Trace)))
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> n [(Either Condition a, Trace)]
sct'
Settings n a
settings
ConcurrencyState
initialCState
([ThreadId] -> s
s0 [ThreadId
initialThread])
s -> Maybe t
sfun
(ConcurrencyState
-> (Scheduler g -> g -> n (Either Condition a, g, Trace))
-> s
-> t
-> n (s, Maybe (Either Condition a, Trace))
srun ConcurrencyState
initialCState Scheduler g -> g -> n (Either Condition a, g, Trace)
forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
runFull)
Scheduler x -> x -> n (Either Condition a, x, Trace)
forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
runFull
(Int -> ThreadId
forall a. Coercible Id a => Int -> a
toId Int
1)
(Int -> IORefId
forall a. Coercible Id a => Int -> a
toId Int
1)
sct'Snap :: Snapshot pty n a -> n [(Either Condition a, Trace)]
sct'Snap Snapshot pty n a
snap =
let idsrc :: IdSource
idsrc = Context n () -> IdSource
forall (n :: * -> *) g. Context n g -> IdSource
cIdSource (Snapshot pty n a -> Context n ()
forall p (n :: * -> *) a. Snapshot p n a -> Context n ()
contextFromSnapshot Snapshot pty n a
snap)
cstate :: ConcurrencyState
cstate = Context n () -> ConcurrencyState
forall (n :: * -> *) g. Context n g -> ConcurrencyState
cCState (Snapshot pty n a -> Context n ()
forall p (n :: * -> *) a. Snapshot p n a -> Context n ()
contextFromSnapshot Snapshot pty n a
snap)
in Settings n a
-> ConcurrencyState
-> s
-> (s -> Maybe t)
-> (s -> t -> n (s, Maybe (Either Condition a, Trace)))
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> n [(Either Condition a, Trace)]
forall (n :: * -> *) a s t.
(MonadDejaFu n, HasCallStack) =>
Settings n a
-> ConcurrencyState
-> s
-> (s -> Maybe t)
-> (s -> t -> n (s, Maybe (Either Condition a, Trace)))
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> n [(Either Condition a, Trace)]
sct'
Settings n a
settings
ConcurrencyState
cstate
([ThreadId] -> s
s0 (([ThreadId], [ThreadId]) -> [ThreadId]
forall a b. (a, b) -> a
fst (Snapshot pty n a -> ([ThreadId], [ThreadId])
forall p (n :: * -> *) a.
Snapshot p n a -> ([ThreadId], [ThreadId])
threadsFromSnapshot Snapshot pty n a
snap)))
s -> Maybe t
sfun
(ConcurrencyState
-> (Scheduler g -> g -> n (Either Condition a, g, Trace))
-> s
-> t
-> n (s, Maybe (Either Condition a, Trace))
srun ConcurrencyState
cstate (Snapshot pty n a
-> Scheduler g -> g -> n (Either Condition a, g, Trace)
forall {n :: * -> *} {pty} {a} {s}.
MonadDejaFu n =>
Snapshot pty n a
-> Scheduler s -> s -> n (Either Condition a, s, Trace)
runSnap Snapshot pty n a
snap))
(Snapshot pty n a
-> Scheduler x -> x -> n (Either Condition a, x, Trace)
forall {n :: * -> *} {pty} {a} {s}.
MonadDejaFu n =>
Snapshot pty n a
-> Scheduler s -> s -> n (Either Condition a, s, Trace)
runSnap Snapshot pty n a
snap)
(Int -> ThreadId
forall a. Coercible Id a => Int -> a
toId (Int -> ThreadId) -> Int -> ThreadId
forall a b. (a -> b) -> a -> b
$ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int, [String]) -> Int
forall a b. (a, b) -> a
fst (IdSource -> (Int, [String])
_tids IdSource
idsrc))
(Int -> IORefId
forall a. Coercible Id a => Int -> a
toId (Int -> IORefId) -> Int -> IORefId
forall a b. (a -> b) -> a -> b
$ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int, [String]) -> Int
forall a b. (a, b) -> a
fst (IdSource -> (Int, [String])
_iorids IdSource
idsrc))
runFull :: Scheduler s -> s -> n (Either Condition a, s, Trace)
runFull Scheduler s
sched s
s = Scheduler s
-> MemType
-> s
-> Program pty n a
-> n (Either Condition a, s, Trace)
forall (n :: * -> *) s pty a.
MonadDejaFu n =>
Scheduler s
-> MemType
-> s
-> Program pty n a
-> n (Either Condition a, s, Trace)
runConcurrent Scheduler s
sched (Settings n a -> MemType
forall (n :: * -> *) a. Settings n a -> MemType
_memtype Settings n a
settings) s
s Program pty n a
conc
runSnap :: Snapshot pty n a
-> Scheduler s -> s -> n (Either Condition a, s, Trace)
runSnap Snapshot pty n a
snap Scheduler s
sched s
s = Scheduler s
-> MemType
-> s
-> Snapshot pty n a
-> n (Either Condition a, s, Trace)
forall (n :: * -> *) s pty a.
MonadDejaFu n =>
Scheduler s
-> MemType
-> s
-> Snapshot pty n a
-> n (Either Condition a, s, Trace)
runSnapshot Scheduler s
sched (Settings n a -> MemType
forall (n :: * -> *) a. Settings n a -> MemType
_memtype Settings n a
settings) s
s Snapshot pty n a
snap
sct' :: (MonadDejaFu n, HasCallStack)
=> Settings n a
-> ConcurrencyState
-> s
-> (s -> Maybe t)
-> (s -> t -> n (s, Maybe (Either Condition a, Trace)))
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> n [(Either Condition a, Trace)]
sct' :: forall (n :: * -> *) a s t.
(MonadDejaFu n, HasCallStack) =>
Settings n a
-> ConcurrencyState
-> s
-> (s -> Maybe t)
-> (s -> t -> n (s, Maybe (Either Condition a, Trace)))
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> n [(Either Condition a, Trace)]
sct' Settings n a
settings ConcurrencyState
cstate0 s
s0 s -> Maybe t
sfun s -> t -> n (s, Maybe (Either Condition a, Trace))
srun forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
run ThreadId
nTId IORefId
nCRId = Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go Maybe (Either Condition a)
forall a. Maybe a
Nothing [] s
s0 where
go :: Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go (Just Either Condition a
res) [Either Condition a]
_ s
_ | Either Condition a -> Bool
earlyExit Either Condition a
res = [(Either Condition a, Trace)] -> n [(Either Condition a, Trace)]
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
go Maybe (Either Condition a)
res0 [Either Condition a]
seen !s
s = case s -> Maybe t
sfun s
s of
Just t
t -> s -> t -> n (s, Maybe (Either Condition a, Trace))
srun s
s t
t n (s, Maybe (Either Condition a, Trace))
-> ((s, Maybe (Either Condition a, Trace))
-> n [(Either Condition a, Trace)])
-> n [(Either Condition a, Trace)]
forall a b. n a -> (a -> n b) -> n b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
(s
s', Just (Left Condition
Abort, Trace
_)) | Bool
hideAborts -> Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go Maybe (Either Condition a)
res0 [Either Condition a]
seen s
s'
(s
s', Just (Either Condition a
res, Trace
trace)) -> case Either Condition a -> Maybe Discard
discard Either Condition a
res of
Just Discard
DiscardResultAndTrace -> Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go (Either Condition a -> Maybe (Either Condition a)
forall a. a -> Maybe a
Just Either Condition a
res) [Either Condition a]
seen s
s'
Just Discard
DiscardTrace -> Either Condition a
-> Trace
-> [Either Condition a]
-> s
-> n [(Either Condition a, Trace)]
result Either Condition a
res [] [Either Condition a]
seen s
s'
Maybe Discard
Nothing -> Either Condition a
-> Trace
-> [Either Condition a]
-> s
-> n [(Either Condition a, Trace)]
result Either Condition a
res Trace
trace [Either Condition a]
seen s
s'
(s
s', Maybe (Either Condition a, Trace)
Nothing) -> Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go Maybe (Either Condition a)
forall a. Maybe a
Nothing [Either Condition a]
seen s
s'
Maybe t
Nothing -> [(Either Condition a, Trace)] -> n [(Either Condition a, Trace)]
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
result :: Either Condition a
-> Trace
-> [Either Condition a]
-> s
-> n [(Either Condition a, Trace)]
result = case Settings n a -> Maybe (a -> a -> Bool)
forall (n :: * -> *) a. Settings n a -> Maybe (a -> a -> Bool)
_equality Settings n a
settings of
Just a -> a -> Bool
f -> \Either Condition a
res Trace
trace [Either Condition a]
seen s
s ->
let eq :: (t -> t -> Bool) -> Either a t -> Either a t -> Bool
eq t -> t -> Bool
cmp (Right t
a1) (Right t
a2) = t -> t -> Bool
cmp t
a1 t
a2
eq t -> t -> Bool
_ (Left a
e1) (Left a
e2) = a
e1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
e2
eq t -> t -> Bool
_ Either a t
_ Either a t
_ = Bool
False
in if (Either Condition a -> Bool) -> [Either Condition a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((a -> a -> Bool)
-> Either Condition a -> Either Condition a -> Bool
forall {a} {t} {t}.
Eq a =>
(t -> t -> Bool) -> Either a t -> Either a t -> Bool
eq a -> a -> Bool
f Either Condition a
res) [Either Condition a]
seen
then Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go (Either Condition a -> Maybe (Either Condition a)
forall a. a -> Maybe a
Just Either Condition a
res) [Either Condition a]
seen s
s
else Either Condition a
-> Trace
-> [Either Condition a]
-> s
-> n [(Either Condition a, Trace)]
dosimplify Either Condition a
res Trace
trace (Either Condition a
resEither Condition a -> [Either Condition a] -> [Either Condition a]
forall a. a -> [a] -> [a]
:[Either Condition a]
seen) s
s
Maybe (a -> a -> Bool)
Nothing -> Either Condition a
-> Trace
-> [Either Condition a]
-> s
-> n [(Either Condition a, Trace)]
dosimplify
dosimplify :: Either Condition a
-> Trace
-> [Either Condition a]
-> s
-> n [(Either Condition a, Trace)]
dosimplify Either Condition a
res [] [Either Condition a]
seen s
s = ((Either Condition a
res, []) (Either Condition a, Trace)
-> [(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
forall a. a -> [a] -> [a]
:) ([(Either Condition a, Trace)] -> [(Either Condition a, Trace)])
-> n [(Either Condition a, Trace)]
-> n [(Either Condition a, Trace)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go (Either Condition a -> Maybe (Either Condition a)
forall a. a -> Maybe a
Just Either Condition a
res) [Either Condition a]
seen s
s
dosimplify Either Condition a
res Trace
trace [Either Condition a]
seen s
s
| Bool -> Bool
not (Settings n a -> Bool
forall (n :: * -> *) a. Settings n a -> Bool
_simplify Settings n a
settings) = ((Either Condition a
res, Trace
trace) (Either Condition a, Trace)
-> [(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
forall a. a -> [a] -> [a]
:) ([(Either Condition a, Trace)] -> [(Either Condition a, Trace)])
-> n [(Either Condition a, Trace)]
-> n [(Either Condition a, Trace)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go (Either Condition a -> Maybe (Either Condition a)
forall a. a -> Maybe a
Just Either Condition a
res) [Either Condition a]
seen s
s
| Bool
otherwise = do
(Either Condition a, Trace)
shrunk <- Settings n a
-> ConcurrencyState
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> Either Condition a
-> Trace
-> n (Either Condition a, Trace)
forall (n :: * -> *) a.
(MonadDejaFu n, HasCallStack) =>
Settings n a
-> ConcurrencyState
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> Either Condition a
-> Trace
-> n (Either Condition a, Trace)
simplifyExecution Settings n a
settings ConcurrencyState
cstate0 Scheduler x -> x -> n (Either Condition a, x, Trace)
forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
run ThreadId
nTId IORefId
nCRId Either Condition a
res Trace
trace
((Either Condition a, Trace)
shrunk (Either Condition a, Trace)
-> [(Either Condition a, Trace)] -> [(Either Condition a, Trace)]
forall a. a -> [a] -> [a]
:) ([(Either Condition a, Trace)] -> [(Either Condition a, Trace)])
-> n [(Either Condition a, Trace)]
-> n [(Either Condition a, Trace)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Either Condition a)
-> [Either Condition a] -> s -> n [(Either Condition a, Trace)]
go (Either Condition a -> Maybe (Either Condition a)
forall a. a -> Maybe a
Just Either Condition a
res) [Either Condition a]
seen s
s
earlyExit :: Either Condition a -> Bool
earlyExit = (Either Condition a -> Bool)
-> Maybe (Either Condition a -> Bool) -> Either Condition a -> Bool
forall a. a -> Maybe a -> a
fromMaybe (Bool -> Either Condition a -> Bool
forall a b. a -> b -> a
const Bool
False) (Settings n a -> Maybe (Either Condition a -> Bool)
forall (n :: * -> *) a.
Settings n a -> Maybe (Either Condition a -> Bool)
_earlyExit Settings n a
settings)
discard :: Either Condition a -> Maybe Discard
discard = (Either Condition a -> Maybe Discard)
-> Maybe (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
forall a. a -> Maybe a -> a
fromMaybe (Maybe Discard -> Either Condition a -> Maybe Discard
forall a b. a -> b -> a
const Maybe Discard
forall a. Maybe a
Nothing) (Settings n a -> Maybe (Either Condition a -> Maybe Discard)
forall (n :: * -> *) a.
Settings n a -> Maybe (Either Condition a -> Maybe Discard)
_discard Settings n a
settings)
hideAborts :: Bool
hideAborts = Bool -> Bool
not (Settings n a -> Bool
forall (n :: * -> *) a. Settings n a -> Bool
_showAborts Settings n a
settings)
simplifyExecution :: (MonadDejaFu n, HasCallStack)
=> Settings n a
-> ConcurrencyState
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> Either Condition a
-> Trace
-> n (Either Condition a, Trace)
simplifyExecution :: forall (n :: * -> *) a.
(MonadDejaFu n, HasCallStack) =>
Settings n a
-> ConcurrencyState
-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> ThreadId
-> IORefId
-> Either Condition a
-> Trace
-> n (Either Condition a, Trace)
simplifyExecution Settings n a
settings ConcurrencyState
cstate0 forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
run ThreadId
nTId IORefId
nCRId Either Condition a
res Trace
trace
| [(ThreadId, ThreadAction)]
tidTrace [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] -> Bool
forall a. Eq a => a -> a -> Bool
== [(ThreadId, ThreadAction)]
simplifiedTrace = do
String -> n ()
debugPrint (String
"Simplifying new result '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Either Condition a -> String
p Either Condition a
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"': no simplification possible!")
(Either Condition a, Trace) -> n (Either Condition a, Trace)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Condition a
res, Trace
trace)
| Bool
otherwise = do
String -> n ()
debugPrint (String
"Simplifying new result '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Either Condition a -> String
p Either Condition a
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"': OK!")
(Either Condition a
res', [(ThreadId, ThreadAction)]
_, Trace
trace') <- (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> [(ThreadId, ThreadAction)]
-> n (Either Condition a, [(ThreadId, ThreadAction)], Trace)
forall (n :: * -> *) a.
MonadDejaFu n =>
(forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> [(ThreadId, ThreadAction)]
-> n (Either Condition a, [(ThreadId, ThreadAction)], Trace)
replay Scheduler x -> x -> n (Either Condition a, x, Trace)
forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
run ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
fixup [(ThreadId, ThreadAction)]
simplifiedTrace)
case (Settings n a -> Maybe (a -> a -> Bool)
forall (n :: * -> *) a. Settings n a -> Maybe (a -> a -> Bool)
_equality Settings n a
settings, Either Condition a
res, Either Condition a
res') of
(Just a -> a -> Bool
f, Right a
a1, Right a
a2) | a -> a -> Bool
f a
a1 a
a2 -> (Either Condition a, Trace) -> n (Either Condition a, Trace)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Condition a
res', Trace
trace')
(Maybe (a -> a -> Bool)
_, Left Condition
e1, Left Condition
e2) | Condition
e1 Condition -> Condition -> Bool
forall a. Eq a => a -> a -> Bool
== Condition
e2 -> (Either Condition a, Trace) -> n (Either Condition a, Trace)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Condition a
res', Trace
trace')
(Maybe (a -> a -> Bool)
Nothing, Right a
_, Right a
_) -> (Either Condition a, Trace) -> n (Either Condition a, Trace)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Condition a
res', Trace
trace')
(Maybe (a -> a -> Bool), Either Condition a, Either Condition a)
_ -> do
String -> n ()
debugFatal (String
"Got a different result after simplifying: '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Either Condition a -> String
p Either Condition a
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' /= '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Either Condition a -> String
p Either Condition a
res' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'")
(Either Condition a, Trace) -> n (Either Condition a, Trace)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Condition a
res, Trace
trace)
where
tidTrace :: [(ThreadId, ThreadAction)]
tidTrace = Trace -> [(ThreadId, ThreadAction)]
toTIdTrace Trace
trace
simplifiedTrace :: [(ThreadId, ThreadAction)]
simplifiedTrace = Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
simplify (Settings n a -> Bool
forall (n :: * -> *) a. Settings n a -> Bool
_safeIO Settings n a
settings) (Settings n a -> MemType
forall (n :: * -> *) a. Settings n a -> MemType
_memtype Settings n a
settings) ConcurrencyState
cstate0 [(ThreadId, ThreadAction)]
tidTrace
fixup :: [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
fixup = MemType
-> Int
-> Int
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
renumber (Settings n a -> MemType
forall (n :: * -> *) a. Settings n a -> MemType
_memtype Settings n a
settings) (ThreadId -> Int
forall a. Coercible a Id => a -> Int
fromId ThreadId
nTId) (IORefId -> Int
forall a. Coercible a Id => a -> Int
fromId IORefId
nCRId)
debugFatal :: String -> n ()
debugFatal = if Settings n a -> Bool
forall (n :: * -> *) a. Settings n a -> Bool
_debugFatal Settings n a
settings then String -> n ()
forall a. HasCallStack => String -> a
fatal else String -> n ()
debugPrint
debugPrint :: String -> n ()
debugPrint = (String -> n ()) -> Maybe (String -> n ()) -> String -> n ()
forall a. a -> Maybe a -> a
fromMaybe (n () -> String -> n ()
forall a b. a -> b -> a
const (() -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())) (Settings n a -> Maybe (String -> n ())
forall (n :: * -> *) a. Settings n a -> Maybe (String -> n ())
_debugPrint Settings n a
settings)
debugShow :: a -> String
debugShow = (a -> String) -> Maybe (a -> String) -> a -> String
forall a. a -> Maybe a -> a
fromMaybe (String -> a -> String
forall a b. a -> b -> a
const String
"_") (Settings n a -> Maybe (a -> String)
forall (n :: * -> *) a. Settings n a -> Maybe (a -> String)
_debugShow Settings n a
settings)
p :: Either Condition a -> String
p = (Condition -> String)
-> (a -> String) -> Either Condition a -> String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Condition -> String
forall a. Show a => a -> String
show a -> String
debugShow
replay :: MonadDejaFu n
=> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> [(ThreadId, ThreadAction)]
-> n (Either Condition a, [(ThreadId, ThreadAction)], Trace)
replay :: forall (n :: * -> *) a.
MonadDejaFu n =>
(forall x. Scheduler x -> x -> n (Either Condition a, x, Trace))
-> [(ThreadId, ThreadAction)]
-> n (Either Condition a, [(ThreadId, ThreadAction)], Trace)
replay forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
run = Scheduler [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
-> n (Either Condition a, [(ThreadId, ThreadAction)], Trace)
forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)
run ((Maybe (ThreadId, ThreadAction)
-> NonEmpty (ThreadId, Lookahead)
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> (Maybe ThreadId, [(ThreadId, ThreadAction)]))
-> Scheduler [(ThreadId, ThreadAction)]
forall state.
(Maybe (ThreadId, ThreadAction)
-> NonEmpty (ThreadId, Lookahead)
-> ConcurrencyState
-> state
-> (Maybe ThreadId, state))
-> Scheduler state
Scheduler ((NonEmpty (ThreadId, Lookahead)
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> (Maybe ThreadId, [(ThreadId, ThreadAction)]))
-> Maybe (ThreadId, ThreadAction)
-> NonEmpty (ThreadId, Lookahead)
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> (Maybe ThreadId, [(ThreadId, ThreadAction)])
forall a b. a -> b -> a
const NonEmpty (ThreadId, Lookahead)
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> (Maybe ThreadId, [(ThreadId, ThreadAction)])
forall {a} {a} {t :: * -> *} {b} {t}.
(Coercible a Id, Coercible a Id, Foldable t) =>
t (a, b)
-> t -> [(a, ThreadAction)] -> (Maybe a, [(a, ThreadAction)])
sched)) where
sched :: t (a, b)
-> t -> [(a, ThreadAction)] -> (Maybe a, [(a, ThreadAction)])
sched t (a, b)
runnable t
cs ((a
t, ThreadAction
Stop):[(a, ThreadAction)]
ts) = case a -> t (a, b) -> Maybe a
forall {a} {a} {t :: * -> *} {b}.
(Coercible a Id, Coercible a Id, Foldable t) =>
a -> t (a, b) -> Maybe a
findThread a
t t (a, b)
runnable of
Just a
t' -> (a -> Maybe a
forall a. a -> Maybe a
Just a
t', [(a, ThreadAction)]
ts)
Maybe a
Nothing -> t (a, b)
-> t -> [(a, ThreadAction)] -> (Maybe a, [(a, ThreadAction)])
sched t (a, b)
runnable t
cs [(a, ThreadAction)]
ts
sched t (a, b)
runnable t
_ ((a
t, ThreadAction
_):[(a, ThreadAction)]
ts) = (a -> t (a, b) -> Maybe a
forall {a} {a} {t :: * -> *} {b}.
(Coercible a Id, Coercible a Id, Foldable t) =>
a -> t (a, b) -> Maybe a
findThread a
t t (a, b)
runnable, [(a, ThreadAction)]
ts)
sched t (a, b)
_ t
_ [(a, ThreadAction)]
_ = (Maybe a
forall a. Maybe a
Nothing, [])
findThread :: a -> t (a, b) -> Maybe a
findThread a
tid0 =
((a, b) -> a) -> Maybe (a, b) -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, b) -> a
forall a b. (a, b) -> a
fst (Maybe (a, b) -> Maybe a)
-> (t (a, b) -> Maybe (a, b)) -> t (a, b) -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, b) -> Bool) -> t (a, b) -> Maybe (a, b)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\(a
tid,b
_) -> a -> Int
forall a. Coercible a Id => a -> Int
fromId a
tid Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Int
forall a. Coercible a Id => a -> Int
fromId a
tid0)
simplify
:: Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
simplify :: Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
simplify Bool
safeIO MemType
memtype ConcurrencyState
cstate0 [(ThreadId, ThreadAction)]
trc0 = Int -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall {t}.
(Eq t, Num t) =>
t -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
loop ([(ThreadId, ThreadAction)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(ThreadId, ThreadAction)]
trc0) ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
prepare [(ThreadId, ThreadAction)]
trc0) where
prepare :: [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
prepare = Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
dropCommits Bool
safeIO MemType
memtype ConcurrencyState
cstate0 ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
lexicoNormalForm Bool
safeIO MemType
memtype ConcurrencyState
cstate0
step :: [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
step = Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
pushForward Bool
safeIO MemType
memtype ConcurrencyState
cstate0 ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
pullBack Bool
safeIO MemType
memtype ConcurrencyState
cstate0
loop :: t -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
loop t
0 [(ThreadId, ThreadAction)]
trc = [(ThreadId, ThreadAction)]
trc
loop t
n [(ThreadId, ThreadAction)]
trc =
let trc' :: [(ThreadId, ThreadAction)]
trc' = [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
step [(ThreadId, ThreadAction)]
trc
in if [(ThreadId, ThreadAction)]
trc' [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] -> Bool
forall a. Eq a => a -> a -> Bool
/= [(ThreadId, ThreadAction)]
trc then t -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
loop (t
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1) [(ThreadId, ThreadAction)]
trc' else [(ThreadId, ThreadAction)]
trc
lexicoNormalForm
:: Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
lexicoNormalForm :: Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
lexicoNormalForm Bool
safeIO MemType
memtype ConcurrencyState
cstate0 = [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go where
go :: [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go [(ThreadId, ThreadAction)]
trc =
let trc' :: [(ThreadId, ThreadAction)]
trc' = Bool
-> MemType
-> ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
permuteBy Bool
safeIO MemType
memtype ConcurrencyState
cstate0 ((ThreadId -> ThreadId -> Bool) -> [ThreadId -> ThreadId -> Bool]
forall a. a -> [a]
repeat ThreadId -> ThreadId -> Bool
forall a. Ord a => a -> a -> Bool
(>)) [(ThreadId, ThreadAction)]
trc
in if [(ThreadId, ThreadAction)]
trc [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] -> Bool
forall a. Eq a => a -> a -> Bool
== [(ThreadId, ThreadAction)]
trc' then [(ThreadId, ThreadAction)]
trc else [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go [(ThreadId, ThreadAction)]
trc'
permuteBy
:: Bool
-> MemType
-> ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
permuteBy :: Bool
-> MemType
-> ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
permuteBy Bool
safeIO MemType
memtype = ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
go where
go :: ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds (ThreadId -> ThreadId -> Bool
p:[ThreadId -> ThreadId -> Bool]
ps) (t1 :: (ThreadId, ThreadAction)
t1@(ThreadId
tid1, ThreadAction
ta1):t2 :: (ThreadId, ThreadAction)
t2@(ThreadId
tid2, ThreadAction
ta2):[(ThreadId, ThreadAction)]
trc)
| Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> ThreadAction
-> Bool
independent Bool
safeIO ConcurrencyState
ds ThreadId
tid1 ThreadAction
ta1 ThreadId
tid2 ThreadAction
ta2 Bool -> Bool -> Bool
&& ThreadId -> ThreadId -> Bool
p ThreadId
tid1 ThreadId
tid2 = ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
go' ConcurrencyState
ds [ThreadId -> ThreadId -> Bool]
ps (ThreadId, ThreadAction)
t2 ((ThreadId, ThreadAction)
t1 (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: [(ThreadId, ThreadAction)]
trc)
| Bool
otherwise = ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
go' ConcurrencyState
ds [ThreadId -> ThreadId -> Bool]
ps (ThreadId, ThreadAction)
t1 ((ThreadId, ThreadAction)
t2 (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: [(ThreadId, ThreadAction)]
trc)
go ConcurrencyState
_ [ThreadId -> ThreadId -> Bool]
_ [(ThreadId, ThreadAction)]
trc = [(ThreadId, ThreadAction)]
trc
go' :: ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
go' ConcurrencyState
ds [ThreadId -> ThreadId -> Bool]
ps t :: (ThreadId, ThreadAction)
t@(ThreadId
tid, ThreadAction
ta) [(ThreadId, ThreadAction)]
trc = (ThreadId, ThreadAction)
t (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: ConcurrencyState
-> [ThreadId -> ThreadId -> Bool]
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
go (MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
ds ThreadId
tid ThreadAction
ta) [ThreadId -> ThreadId -> Bool]
ps [(ThreadId, ThreadAction)]
trc
dropCommits
:: Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
dropCommits :: Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
dropCommits Bool
_ MemType
SequentialConsistency = ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
forall a b. a -> b -> a
const [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> a
id
dropCommits Bool
safeIO MemType
memtype = ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go where
go :: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds (t1 :: (ThreadId, ThreadAction)
t1@(ThreadId
tid1, ta1 :: ThreadAction
ta1@(CommitIORef ThreadId
_ IORefId
iorefid)):t2 :: (ThreadId, ThreadAction)
t2@(ThreadId
tid2, ThreadAction
ta2):[(ThreadId, ThreadAction)]
trc)
| ActionType -> Bool
isBarrier (ThreadAction -> ActionType
simplifyAction ThreadAction
ta2) Bool -> Bool -> Bool
&& ConcurrencyState -> IORefId -> Int
numBuffered ConcurrencyState
ds IORefId
iorefid Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds ((ThreadId, ThreadAction)
t2(ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
:[(ThreadId, ThreadAction)]
trc)
| Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> ThreadAction
-> Bool
independent Bool
safeIO ConcurrencyState
ds ThreadId
tid1 ThreadAction
ta1 ThreadId
tid2 ThreadAction
ta2 = (ThreadId, ThreadAction)
t2 (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go (MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
ds ThreadId
tid2 ThreadAction
ta2) ((ThreadId, ThreadAction)
t1(ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
:[(ThreadId, ThreadAction)]
trc)
go ConcurrencyState
ds (t :: (ThreadId, ThreadAction)
t@(ThreadId
tid,ThreadAction
ta):[(ThreadId, ThreadAction)]
trc) = (ThreadId, ThreadAction)
t (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go (MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
ds ThreadId
tid ThreadAction
ta) [(ThreadId, ThreadAction)]
trc
go ConcurrencyState
_ [] = []
pullBack
:: Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
pullBack :: Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
pullBack Bool
safeIO MemType
memtype = ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go where
go :: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds (t1 :: (ThreadId, ThreadAction)
t1@(ThreadId
tid1, ThreadAction
ta1):trc :: [(ThreadId, ThreadAction)]
trc@((ThreadId
tid2, ThreadAction
_):[(ThreadId, ThreadAction)]
_)) =
let ds' :: ConcurrencyState
ds' = MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
ds ThreadId
tid1 ThreadAction
ta1
trc' :: [(ThreadId, ThreadAction)]
trc' = if ThreadId
tid1 ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
/= ThreadId
tid2
then [(ThreadId, ThreadAction)]
-> (((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
-> [(ThreadId, ThreadAction)])
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
-> [(ThreadId, ThreadAction)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [(ThreadId, ThreadAction)]
trc (((ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
-> [(ThreadId, ThreadAction)]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (:)) (ThreadId
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
findAction ThreadId
tid1 ConcurrencyState
ds' [(ThreadId, ThreadAction)]
trc)
else [(ThreadId, ThreadAction)]
trc
in (ThreadId, ThreadAction)
t1 (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds' [(ThreadId, ThreadAction)]
trc'
go ConcurrencyState
_ [(ThreadId, ThreadAction)]
trc = [(ThreadId, ThreadAction)]
trc
findAction :: ThreadId
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
findAction ThreadId
tid0 = ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
fgo where
fgo :: ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
fgo ConcurrencyState
ds (t :: (ThreadId, ThreadAction)
t@(ThreadId
tid, ThreadAction
ta):[(ThreadId, ThreadAction)]
trc)
| ThreadId
tid ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
tid0 = ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
forall a. a -> Maybe a
Just ((ThreadId, ThreadAction)
t, [(ThreadId, ThreadAction)]
trc)
| Bool
otherwise = case ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
fgo (MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
ds ThreadId
tid ThreadAction
ta) [(ThreadId, ThreadAction)]
trc of
Just (ft :: (ThreadId, ThreadAction)
ft@(ThreadId
ftid, ThreadAction
fa), [(ThreadId, ThreadAction)]
trc')
| Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> ThreadAction
-> Bool
independent Bool
safeIO ConcurrencyState
ds ThreadId
tid ThreadAction
ta ThreadId
ftid ThreadAction
fa -> ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
-> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
forall a. a -> Maybe a
Just ((ThreadId, ThreadAction)
ft, (ThreadId, ThreadAction)
t(ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
:[(ThreadId, ThreadAction)]
trc')
Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
_ -> Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
forall a. Maybe a
Nothing
fgo ConcurrencyState
_ [(ThreadId, ThreadAction)]
_ = Maybe ((ThreadId, ThreadAction), [(ThreadId, ThreadAction)])
forall a. Maybe a
Nothing
pushForward
:: Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
pushForward :: Bool
-> MemType
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
pushForward Bool
safeIO MemType
memtype = ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go where
go :: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds (t1 :: (ThreadId, ThreadAction)
t1@(ThreadId
tid1, ThreadAction
ta1):trc :: [(ThreadId, ThreadAction)]
trc@((ThreadId
tid2, ThreadAction
_):[(ThreadId, ThreadAction)]
_)) =
let ds' :: ConcurrencyState
ds' = MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
ds ThreadId
tid1 ThreadAction
ta1
in if ThreadId
tid1 ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
/= ThreadId
tid2
then [(ThreadId, ThreadAction)]
-> ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> Maybe [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((ThreadId, ThreadAction)
t1 (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds' [(ThreadId, ThreadAction)]
trc) (ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds) (ThreadId
-> ThreadAction
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> Maybe [(ThreadId, ThreadAction)]
findAction ThreadId
tid1 ThreadAction
ta1 ConcurrencyState
ds [(ThreadId, ThreadAction)]
trc)
else (ThreadId, ThreadAction)
t1 (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
go ConcurrencyState
ds' [(ThreadId, ThreadAction)]
trc
go ConcurrencyState
_ [(ThreadId, ThreadAction)]
trc = [(ThreadId, ThreadAction)]
trc
findAction :: ThreadId
-> ThreadAction
-> ConcurrencyState
-> [(ThreadId, ThreadAction)]
-> Maybe [(ThreadId, ThreadAction)]
findAction ThreadId
tid0 ThreadAction
ta0 = ConcurrencyState
-> [(ThreadId, ThreadAction)] -> Maybe [(ThreadId, ThreadAction)]
fgo where
fgo :: ConcurrencyState
-> [(ThreadId, ThreadAction)] -> Maybe [(ThreadId, ThreadAction)]
fgo ConcurrencyState
ds (t :: (ThreadId, ThreadAction)
t@(ThreadId
tid, ThreadAction
ta):[(ThreadId, ThreadAction)]
trc)
| ThreadId
tid ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
tid0 = [(ThreadId, ThreadAction)] -> Maybe [(ThreadId, ThreadAction)]
forall a. a -> Maybe a
Just ((ThreadId
tid0, ThreadAction
ta0) (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: (ThreadId, ThreadAction)
t (ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
: [(ThreadId, ThreadAction)]
trc)
| Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> ThreadAction
-> Bool
independent Bool
safeIO ConcurrencyState
ds ThreadId
tid0 ThreadAction
ta0 ThreadId
tid ThreadAction
ta = ((ThreadId, ThreadAction)
t(ThreadId, ThreadAction)
-> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
forall a. a -> [a] -> [a]
:) ([(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)])
-> Maybe [(ThreadId, ThreadAction)]
-> Maybe [(ThreadId, ThreadAction)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConcurrencyState
-> [(ThreadId, ThreadAction)] -> Maybe [(ThreadId, ThreadAction)]
fgo (MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
ds ThreadId
tid ThreadAction
ta) [(ThreadId, ThreadAction)]
trc
| Bool
otherwise = Maybe [(ThreadId, ThreadAction)]
forall a. Maybe a
Nothing
fgo ConcurrencyState
_ [(ThreadId, ThreadAction)]
_ = Maybe [(ThreadId, ThreadAction)]
forall a. Maybe a
Nothing
renumber
:: MemType
-> Int
-> Int
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
renumber :: MemType
-> Int
-> Int
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
renumber MemType
memtype Int
tid0 Int
crid0 = ((IntMap Int, Int, IntMap Int, Int), [(ThreadId, ThreadAction)])
-> [(ThreadId, ThreadAction)]
forall a b. (a, b) -> b
snd (((IntMap Int, Int, IntMap Int, Int), [(ThreadId, ThreadAction)])
-> [(ThreadId, ThreadAction)])
-> ([(ThreadId, ThreadAction)]
-> ((IntMap Int, Int, IntMap Int, Int),
[(ThreadId, ThreadAction)]))
-> [(ThreadId, ThreadAction)]
-> [(ThreadId, ThreadAction)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((IntMap Int, Int, IntMap Int, Int)
-> (ThreadId, ThreadAction)
-> ((IntMap Int, Int, IntMap Int, Int), (ThreadId, ThreadAction)))
-> (IntMap Int, Int, IntMap Int, Int)
-> [(ThreadId, ThreadAction)]
-> ((IntMap Int, Int, IntMap Int, Int), [(ThreadId, ThreadAction)])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL (IntMap Int, Int, IntMap Int, Int)
-> (ThreadId, ThreadAction)
-> ((IntMap Int, Int, IntMap Int, Int), (ThreadId, ThreadAction))
go (IntMap Int
forall a. IntMap a
I.empty, Int
tid0, IntMap Int
forall a. IntMap a
I.empty, Int
crid0) where
go :: (IntMap Int, Int, IntMap Int, Int)
-> (ThreadId, ThreadAction)
-> ((IntMap Int, Int, IntMap Int, Int), (ThreadId, ThreadAction))
go s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
cridmap, Int
_) (ThreadId
_, CommitIORef ThreadId
tid IORefId
crid) =
let tid' :: ThreadId
tid' = IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap ThreadId
tid
crid' :: IORefId
crid' = IntMap Int -> IORefId -> IORefId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
cridmap IORefId
crid
act' :: ThreadAction
act' = ThreadId -> IORefId -> ThreadAction
CommitIORef ThreadId
tid' IORefId
crid'
in case MemType
memtype of
MemType
PartialStoreOrder -> ((IntMap Int, Int, IntMap Int, Int)
s, (ThreadId -> Maybe IORefId -> ThreadId
commitThreadId ThreadId
tid' (IORefId -> Maybe IORefId
forall a. a -> Maybe a
Just IORefId
crid'), ThreadAction
act'))
MemType
_ -> ((IntMap Int, Int, IntMap Int, Int)
s, (ThreadId -> Maybe IORefId -> ThreadId
commitThreadId ThreadId
tid' Maybe IORefId
forall a. Maybe a
Nothing, ThreadAction
act'))
go s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (ThreadId
tid, ThreadAction
act) =
let ((IntMap Int, Int, IntMap Int, Int)
s', ThreadAction
act') = (IntMap Int, Int, IntMap Int, Int)
-> ThreadAction
-> ((IntMap Int, Int, IntMap Int, Int), ThreadAction)
updateAction (IntMap Int, Int, IntMap Int, Int)
s ThreadAction
act
in ((IntMap Int, Int, IntMap Int, Int)
s', (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap ThreadId
tid, ThreadAction
act'))
updateAction :: (IntMap Int, Int, IntMap Int, Int)
-> ThreadAction
-> ((IntMap Int, Int, IntMap Int, Int), ThreadAction)
updateAction (IntMap Int
tidmap, Int
nTId, IntMap Int
cridmap, Int
nCRId) (Fork ThreadId
old) =
let tidmap' :: IntMap Int
tidmap' = Int -> Int -> IntMap Int -> IntMap Int
forall a. Int -> a -> IntMap a -> IntMap a
I.insert (ThreadId -> Int
forall a. Coercible a Id => a -> Int
fromId ThreadId
old) Int
nTId IntMap Int
tidmap
nTId' :: Int
nTId' = Int
nTId Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
in ((IntMap Int
tidmap', Int
nTId', IntMap Int
cridmap, Int
nCRId), ThreadId -> ThreadAction
Fork (Int -> ThreadId
forall a. Coercible Id a => Int -> a
toId Int
nTId))
updateAction (IntMap Int
tidmap, Int
nTId, IntMap Int
cridmap, Int
nCRId) (ForkOS ThreadId
old) =
let tidmap' :: IntMap Int
tidmap' = Int -> Int -> IntMap Int -> IntMap Int
forall a. Int -> a -> IntMap a -> IntMap a
I.insert (ThreadId -> Int
forall a. Coercible a Id => a -> Int
fromId ThreadId
old) Int
nTId IntMap Int
tidmap
nTId' :: Int
nTId' = Int
nTId Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
in ((IntMap Int
tidmap', Int
nTId', IntMap Int
cridmap, Int
nCRId), ThreadId -> ThreadAction
ForkOS (Int -> ThreadId
forall a. Coercible Id a => Int -> a
toId Int
nTId))
updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (PutMVar MVarId
mvid [ThreadId]
olds) =
((IntMap Int, Int, IntMap Int, Int)
s, MVarId -> [ThreadId] -> ThreadAction
PutMVar MVarId
mvid ((ThreadId -> ThreadId) -> [ThreadId] -> [ThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap) [ThreadId]
olds))
updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (TryPutMVar MVarId
mvid Bool
b [ThreadId]
olds) =
((IntMap Int, Int, IntMap Int, Int)
s, MVarId -> Bool -> [ThreadId] -> ThreadAction
TryPutMVar MVarId
mvid Bool
b ((ThreadId -> ThreadId) -> [ThreadId] -> [ThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap) [ThreadId]
olds))
updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (TakeMVar MVarId
mvid [ThreadId]
olds) =
((IntMap Int, Int, IntMap Int, Int)
s, MVarId -> [ThreadId] -> ThreadAction
TakeMVar MVarId
mvid ((ThreadId -> ThreadId) -> [ThreadId] -> [ThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap) [ThreadId]
olds))
updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (TryTakeMVar MVarId
mvid Bool
b [ThreadId]
olds) =
((IntMap Int, Int, IntMap Int, Int)
s, MVarId -> Bool -> [ThreadId] -> ThreadAction
TryTakeMVar MVarId
mvid Bool
b ((ThreadId -> ThreadId) -> [ThreadId] -> [ThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap) [ThreadId]
olds))
updateAction (IntMap Int
tidmap, Int
nTId, IntMap Int
cridmap, Int
nCRId) (NewIORef IORefId
old) =
let cridmap' :: IntMap Int
cridmap' = Int -> Int -> IntMap Int -> IntMap Int
forall a. Int -> a -> IntMap a -> IntMap a
I.insert (IORefId -> Int
forall a. Coercible a Id => a -> Int
fromId IORefId
old) Int
nCRId IntMap Int
cridmap
nCRId' :: Int
nCRId' = Int
nCRId Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
in ((IntMap Int
tidmap, Int
nTId, IntMap Int
cridmap', Int
nCRId'), IORefId -> ThreadAction
NewIORef (Int -> IORefId
forall a. Coercible Id a => Int -> a
toId Int
nCRId))
updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
_, Int
_, IntMap Int
cridmap, Int
_) (ReadIORef IORefId
old) =
((IntMap Int, Int, IntMap Int, Int)
s, IORefId -> ThreadAction
ReadIORef (IntMap Int -> IORefId -> IORefId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
cridmap IORefId
old))
updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
_, Int
_, IntMap Int
cridmap, Int
_) (ReadIORefCas IORefId
old) =
((IntMap Int, Int, IntMap Int, Int)
s, IORefId -> ThreadAction
ReadIORefCas (IntMap Int -> IORefId -> IORefId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
cridmap IORefId
old))
updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
_, Int
_, IntMap Int
cridmap, Int
_) (ModIORef IORefId
old) =
((IntMap Int, Int, IntMap Int, Int)
s, IORefId -> ThreadAction
ModIORef (IntMap Int -> IORefId -> IORefId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
cridmap IORefId
old))
updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
_, Int
_, IntMap Int
cridmap, Int
_) (ModIORefCas IORefId
old) =
((IntMap Int, Int, IntMap Int, Int)
s, IORefId -> ThreadAction
ModIORefCas (IntMap Int -> IORefId -> IORefId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
cridmap IORefId
old))
updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
_, Int
_, IntMap Int
cridmap, Int
_) (WriteIORef IORefId
old) =
((IntMap Int, Int, IntMap Int, Int)
s, IORefId -> ThreadAction
WriteIORef (IntMap Int -> IORefId -> IORefId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
cridmap IORefId
old))
updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
_, Int
_, IntMap Int
cridmap, Int
_) (CasIORef IORefId
old Bool
b) =
((IntMap Int, Int, IntMap Int, Int)
s, IORefId -> Bool -> ThreadAction
CasIORef (IntMap Int -> IORefId -> IORefId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
cridmap IORefId
old) Bool
b)
updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (STM [TAction]
tas [ThreadId]
olds) =
((IntMap Int, Int, IntMap Int, Int)
s, [TAction] -> [ThreadId] -> ThreadAction
STM [TAction]
tas ((ThreadId -> ThreadId) -> [ThreadId] -> [ThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap) [ThreadId]
olds))
updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (ThrowTo ThreadId
old Maybe MaskingState
ms) =
((IntMap Int, Int, IntMap Int, Int)
s, ThreadId -> Maybe MaskingState -> ThreadAction
ThrowTo (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap ThreadId
old) Maybe MaskingState
ms)
updateAction s :: (IntMap Int, Int, IntMap Int, Int)
s@(IntMap Int
tidmap, Int
_, IntMap Int
_, Int
_) (BlockedThrowTo ThreadId
old) =
((IntMap Int, Int, IntMap Int, Int)
s, ThreadId -> ThreadAction
BlockedThrowTo (IntMap Int -> ThreadId -> ThreadId
forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
tidmap ThreadId
old))
updateAction (IntMap Int, Int, IntMap Int, Int)
s ThreadAction
act = ((IntMap Int, Int, IntMap Int, Int)
s, ThreadAction
act)
renumbered :: (Coercible a Id, Coercible Id a) => I.IntMap Int -> a -> a
renumbered :: forall a. (Coercible a Id, Coercible Id a) => IntMap Int -> a -> a
renumbered IntMap Int
idmap a
id_ = Int -> a
forall a. Coercible Id a => Int -> a
toId (Int -> a) -> Int -> a
forall a b. (a -> b) -> a -> b
$ Int -> Int -> IntMap Int -> Int
forall a. a -> Int -> IntMap a -> a
I.findWithDefault (a -> Int
forall a. Coercible a Id => a -> Int
fromId a
id_) (a -> Int
forall a. Coercible a Id => a -> Int
fromId a
id_) IntMap Int
idmap
toId :: Coercible Id a => Int -> a
toId :: forall a. Coercible Id a => Int -> a
toId = Id -> a
forall a b. Coercible a b => a -> b
coerce (Id -> a) -> (Int -> Id) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe String -> Int -> Id
Id Maybe String
forall a. Maybe a
Nothing
fromId :: Coercible a Id => a -> Int
fromId :: forall a. Coercible a Id => a -> Int
fromId a
a = let (Id Maybe String
_ Int
id_) = a -> Id
forall a b. Coercible a b => a -> b
coerce a
a in Int
id_