{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}

-- |
-- Module      : Test.DejaFu.Internal
-- Copyright   : (c) 2017--2020 Michael Walker
-- License     : MIT
-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
-- Stability   : experimental
-- Portability : DeriveAnyClass, DeriveGeneric, FlexibleContexts, GADTs, LambdaCase
--
-- Internal types and functions used throughout DejaFu.  This module
-- is NOT considered to form part of the public interface of this
-- library.
module Test.DejaFu.Internal where

import           Control.DeepSeq    (NFData(..))
import           Control.Exception  (MaskingState(..))
import           Data.List.NonEmpty (NonEmpty(..))
import           Data.Map.Strict    (Map)
import qualified Data.Map.Strict    as M
import           Data.Maybe         (fromMaybe)
import           Data.Set           (Set)
import qualified Data.Set           as S
import           GHC.Generics       (Generic)
import           GHC.Stack          (HasCallStack, withFrozenCallStack)
import           System.Random      (RandomGen)

import           Test.DejaFu.Types

-------------------------------------------------------------------------------
-- * SCT settings

-- | SCT configuration record.
--
-- @since 1.2.0.0
data Settings n a = Settings
  { forall (n :: * -> *) a. Settings n a -> Way
_way :: Way
  , forall (n :: * -> *) a. Settings n a -> Maybe LengthBound
_lengthBound :: Maybe LengthBound
  , forall (n :: * -> *) a. Settings n a -> MemType
_memtype :: MemType
  , forall (n :: * -> *) a.
Settings n a -> Maybe (Either Condition a -> Maybe Discard)
_discard :: Maybe (Either Condition a -> Maybe Discard)
  , forall (n :: * -> *) a. Settings n a -> Maybe (a -> String)
_debugShow :: Maybe (a -> String)
  , forall (n :: * -> *) a. Settings n a -> Maybe (String -> n ())
_debugPrint :: Maybe (String -> n ())
  , forall (n :: * -> *) a. Settings n a -> Bool
_debugFatal :: Bool
  , forall (n :: * -> *) a.
Settings n a -> Maybe (Either Condition a -> Bool)
_earlyExit :: Maybe (Either Condition a -> Bool)
  , forall (n :: * -> *) a. Settings n a -> Maybe (a -> a -> Bool)
_equality :: Maybe (a -> a -> Bool)
  , forall (n :: * -> *) a. Settings n a -> Bool
_simplify  :: Bool
  , forall (n :: * -> *) a. Settings n a -> Bool
_safeIO :: Bool
  , forall (n :: * -> *) a. Settings n a -> Bool
_showAborts :: Bool
  }

-- | How to explore the possible executions of a concurrent program.
--
-- @since 0.7.0.0
data Way where
  Systematic :: Bounds -> Way
  Randomly   :: RandomGen g => (g -> (Int, g)) -> g -> Int -> Way

instance Show Way where
  show :: Way -> String
show (Systematic Bounds
bs) = String
"Systematic (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bounds -> String
forall a. Show a => a -> String
show Bounds
bs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show (Randomly g -> (Int, g)
_ g
_ Int
n) = String
"Randomly <f> <gen> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n

-------------------------------------------------------------------------------
-- * Identifiers

-- | The number of ID parameters was getting a bit unwieldy, so this
-- hides them all away.
data IdSource = IdSource
  { IdSource -> (Int, [String])
_iorids :: (Int, [String])
  , IdSource -> (Int, [String])
_mvids  :: (Int, [String])
  , IdSource -> (Int, [String])
_tvids  :: (Int, [String])
  , IdSource -> (Int, [String])
_tids   :: (Int, [String])
  } deriving (IdSource -> IdSource -> Bool
(IdSource -> IdSource -> Bool)
-> (IdSource -> IdSource -> Bool) -> Eq IdSource
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IdSource -> IdSource -> Bool
== :: IdSource -> IdSource -> Bool
$c/= :: IdSource -> IdSource -> Bool
/= :: IdSource -> IdSource -> Bool
Eq, Eq IdSource
Eq IdSource =>
(IdSource -> IdSource -> Ordering)
-> (IdSource -> IdSource -> Bool)
-> (IdSource -> IdSource -> Bool)
-> (IdSource -> IdSource -> Bool)
-> (IdSource -> IdSource -> Bool)
-> (IdSource -> IdSource -> IdSource)
-> (IdSource -> IdSource -> IdSource)
-> Ord IdSource
IdSource -> IdSource -> Bool
IdSource -> IdSource -> Ordering
IdSource -> IdSource -> IdSource
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: IdSource -> IdSource -> Ordering
compare :: IdSource -> IdSource -> Ordering
$c< :: IdSource -> IdSource -> Bool
< :: IdSource -> IdSource -> Bool
$c<= :: IdSource -> IdSource -> Bool
<= :: IdSource -> IdSource -> Bool
$c> :: IdSource -> IdSource -> Bool
> :: IdSource -> IdSource -> Bool
$c>= :: IdSource -> IdSource -> Bool
>= :: IdSource -> IdSource -> Bool
$cmax :: IdSource -> IdSource -> IdSource
max :: IdSource -> IdSource -> IdSource
$cmin :: IdSource -> IdSource -> IdSource
min :: IdSource -> IdSource -> IdSource
Ord, Int -> IdSource -> ShowS
[IdSource] -> ShowS
IdSource -> String
(Int -> IdSource -> ShowS)
-> (IdSource -> String) -> ([IdSource] -> ShowS) -> Show IdSource
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IdSource -> ShowS
showsPrec :: Int -> IdSource -> ShowS
$cshow :: IdSource -> String
show :: IdSource -> String
$cshowList :: [IdSource] -> ShowS
showList :: [IdSource] -> ShowS
Show, (forall x. IdSource -> Rep IdSource x)
-> (forall x. Rep IdSource x -> IdSource) -> Generic IdSource
forall x. Rep IdSource x -> IdSource
forall x. IdSource -> Rep IdSource x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. IdSource -> Rep IdSource x
from :: forall x. IdSource -> Rep IdSource x
$cto :: forall x. Rep IdSource x -> IdSource
to :: forall x. Rep IdSource x -> IdSource
Generic, IdSource -> ()
(IdSource -> ()) -> NFData IdSource
forall a. (a -> ()) -> NFData a
$crnf :: IdSource -> ()
rnf :: IdSource -> ()
NFData)

-- | Get the next free 'IORefId'.
nextIORId :: String -> IdSource -> (IdSource, IORefId)
nextIORId :: String -> IdSource -> (IdSource, IORefId)
nextIORId String
name IdSource
idsource =
  let (Id
iorid, (Int, [String])
iorids') = String -> (Int, [String]) -> (Id, (Int, [String]))
nextId String
name (IdSource -> (Int, [String])
_iorids IdSource
idsource)
  in (IdSource
idsource { _iorids = iorids' }, Id -> IORefId
IORefId Id
iorid)

-- | Get the next free 'MVarId'.
nextMVId :: String -> IdSource -> (IdSource, MVarId)
nextMVId :: String -> IdSource -> (IdSource, MVarId)
nextMVId String
name IdSource
idsource =
  let (Id
mvid, (Int, [String])
mvids') = String -> (Int, [String]) -> (Id, (Int, [String]))
nextId String
name (IdSource -> (Int, [String])
_mvids IdSource
idsource)
  in (IdSource
idsource { _mvids = mvids' }, Id -> MVarId
MVarId Id
mvid)

-- | Get the next free 'TVarId'.
nextTVId :: String -> IdSource -> (IdSource, TVarId)
nextTVId :: String -> IdSource -> (IdSource, TVarId)
nextTVId String
name IdSource
idsource =
  let (Id
tvid, (Int, [String])
tvids') = String -> (Int, [String]) -> (Id, (Int, [String]))
nextId String
name (IdSource -> (Int, [String])
_tvids IdSource
idsource)
  in (IdSource
idsource { _tvids = tvids' }, Id -> TVarId
TVarId Id
tvid)

-- | Get the next free 'ThreadId'.
nextTId :: String -> IdSource -> (IdSource, ThreadId)
nextTId :: String -> IdSource -> (IdSource, ThreadId)
nextTId String
name IdSource
idsource =
  let (Id
tid, (Int, [String])
tids') = String -> (Int, [String]) -> (Id, (Int, [String]))
nextId String
name (IdSource -> (Int, [String])
_tids IdSource
idsource)
  in (IdSource
idsource { _tids = tids' }, Id -> ThreadId
ThreadId Id
tid)

-- | Helper for @next*@
nextId :: String -> (Int, [String]) -> (Id, (Int, [String]))
nextId :: String -> (Int, [String]) -> (Id, (Int, [String]))
nextId String
name (Int
num, [String]
used) = (Maybe String -> Int -> Id
Id Maybe String
newName (Int
numInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1), (Int
numInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, [String]
newUsed)) where
  newName :: Maybe String
newName
    | String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
name = Maybe String
forall a. Maybe a
Nothing
    | Int
occurrences Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = String -> Maybe String
forall a. a -> Maybe a
Just (String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"-" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
occurrences)
    | Bool
otherwise = String -> Maybe String
forall a. a -> Maybe a
Just String
name
  newUsed :: [String]
newUsed
    | String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
name = [String]
used
    | Bool
otherwise = String
name String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
used
  occurrences :: Int
occurrences = [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==String
name) [String]
used)

-- | The initial ID source.
initialIdSource :: IdSource
initialIdSource :: IdSource
initialIdSource = (Int, [String])
-> (Int, [String])
-> (Int, [String])
-> (Int, [String])
-> IdSource
IdSource (Int
0, []) (Int
0, []) (Int
0, []) (Int
0, [])

-------------------------------------------------------------------------------
-- * Actions

-- | Check if a @ThreadAction@ immediately blocks.
isBlock :: ThreadAction -> Bool
isBlock :: ThreadAction -> Bool
isBlock (BlockedThrowTo  ThreadId
_) = Bool
True
isBlock (BlockedTakeMVar MVarId
_) = Bool
True
isBlock (BlockedReadMVar MVarId
_) = Bool
True
isBlock (BlockedPutMVar  MVarId
_) = Bool
True
isBlock (BlockedSTM [TAction]
_) = Bool
True
isBlock ThreadAction
_ = Bool
False

-- | Get the @TVar@s affected by a @ThreadAction@.
tvarsOf :: ThreadAction -> Set TVarId
tvarsOf :: ThreadAction -> Set TVarId
tvarsOf ThreadAction
act = ThreadAction -> Set TVarId
tvarsRead ThreadAction
act Set TVarId -> Set TVarId -> Set TVarId
forall a. Ord a => Set a -> Set a -> Set a
`S.union` ThreadAction -> Set TVarId
tvarsWritten ThreadAction
act

-- | Get the @TVar@s a transaction wrote to (or would have, if it
-- didn't @retry@).
tvarsWritten :: ThreadAction -> Set TVarId
tvarsWritten :: ThreadAction -> Set TVarId
tvarsWritten ThreadAction
act = [TVarId] -> Set TVarId
forall a. Ord a => [a] -> Set a
S.fromList ([TVarId] -> Set TVarId) -> [TVarId] -> Set TVarId
forall a b. (a -> b) -> a -> b
$ case ThreadAction
act of
  STM [TAction]
trc [ThreadId]
_ -> (TAction -> [TVarId]) -> [TAction] -> [TVarId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TAction -> [TVarId]
tvarsOf' [TAction]
trc
  ThrownSTM [TAction]
trc Maybe MaskingState
_ -> (TAction -> [TVarId]) -> [TAction] -> [TVarId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TAction -> [TVarId]
tvarsOf' [TAction]
trc
  BlockedSTM [TAction]
trc -> (TAction -> [TVarId]) -> [TAction] -> [TVarId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TAction -> [TVarId]
tvarsOf' [TAction]
trc
  ThreadAction
_ -> []

  where
    tvarsOf' :: TAction -> [TVarId]
tvarsOf' (TNew TVarId
tv) = [TVarId
tv]
    tvarsOf' (TWrite TVarId
tv) = [TVarId
tv]
    tvarsOf' (TOrElse [TAction]
ta Maybe [TAction]
tb) = (TAction -> [TVarId]) -> [TAction] -> [TVarId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TAction -> [TVarId]
tvarsOf' ([TAction]
ta [TAction] -> [TAction] -> [TAction]
forall a. [a] -> [a] -> [a]
++ [TAction] -> Maybe [TAction] -> [TAction]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [TAction]
tb)
    tvarsOf' (TCatch  [TAction]
ta Maybe [TAction]
tb) = (TAction -> [TVarId]) -> [TAction] -> [TVarId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TAction -> [TVarId]
tvarsOf' ([TAction]
ta [TAction] -> [TAction] -> [TAction]
forall a. [a] -> [a] -> [a]
++ [TAction] -> Maybe [TAction] -> [TAction]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [TAction]
tb)
    tvarsOf' TAction
_ = []

-- | Get the @TVar@s a transaction read from.
tvarsRead :: ThreadAction -> Set TVarId
tvarsRead :: ThreadAction -> Set TVarId
tvarsRead ThreadAction
act = [TVarId] -> Set TVarId
forall a. Ord a => [a] -> Set a
S.fromList ([TVarId] -> Set TVarId) -> [TVarId] -> Set TVarId
forall a b. (a -> b) -> a -> b
$ case ThreadAction
act of
  STM [TAction]
trc [ThreadId]
_ -> (TAction -> [TVarId]) -> [TAction] -> [TVarId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TAction -> [TVarId]
tvarsOf' [TAction]
trc
  ThrownSTM [TAction]
trc Maybe MaskingState
_ -> (TAction -> [TVarId]) -> [TAction] -> [TVarId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TAction -> [TVarId]
tvarsOf' [TAction]
trc
  BlockedSTM [TAction]
trc -> (TAction -> [TVarId]) -> [TAction] -> [TVarId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TAction -> [TVarId]
tvarsOf' [TAction]
trc
  ThreadAction
_ -> []

  where
    tvarsOf' :: TAction -> [TVarId]
tvarsOf' (TRead TVarId
tv) = [TVarId
tv]
    tvarsOf' (TOrElse [TAction]
ta Maybe [TAction]
tb) = (TAction -> [TVarId]) -> [TAction] -> [TVarId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TAction -> [TVarId]
tvarsOf' ([TAction]
ta [TAction] -> [TAction] -> [TAction]
forall a. [a] -> [a] -> [a]
++ [TAction] -> Maybe [TAction] -> [TAction]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [TAction]
tb)
    tvarsOf' (TCatch  [TAction]
ta Maybe [TAction]
tb) = (TAction -> [TVarId]) -> [TAction] -> [TVarId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TAction -> [TVarId]
tvarsOf' ([TAction]
ta [TAction] -> [TAction] -> [TAction]
forall a. [a] -> [a] -> [a]
++ [TAction] -> Maybe [TAction] -> [TAction]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [TAction]
tb)
    tvarsOf' TAction
_ = []

-- | Convert a 'ThreadAction' into a 'Lookahead': \"rewind\" what has
-- happened.
rewind :: ThreadAction -> Lookahead
rewind :: ThreadAction -> Lookahead
rewind (Fork ThreadId
_) = Lookahead
WillFork
rewind (ForkOS ThreadId
_) = Lookahead
WillForkOS
rewind (SupportsBoundThreads Bool
_) = Lookahead
WillSupportsBoundThreads
rewind (IsCurrentThreadBound Bool
_) = Lookahead
WillIsCurrentThreadBound
rewind ThreadAction
MyThreadId = Lookahead
WillMyThreadId
rewind (GetNumCapabilities Int
_) = Lookahead
WillGetNumCapabilities
rewind (SetNumCapabilities Int
i) = Int -> Lookahead
WillSetNumCapabilities Int
i
rewind ThreadAction
Yield = Lookahead
WillYield
rewind (ThreadDelay Int
n) = Int -> Lookahead
WillThreadDelay Int
n
rewind (NewMVar MVarId
_) = Lookahead
WillNewMVar
rewind (PutMVar MVarId
c [ThreadId]
_) = MVarId -> Lookahead
WillPutMVar MVarId
c
rewind (BlockedPutMVar MVarId
c) = MVarId -> Lookahead
WillPutMVar MVarId
c
rewind (TryPutMVar MVarId
c Bool
_ [ThreadId]
_) = MVarId -> Lookahead
WillTryPutMVar MVarId
c
rewind (ReadMVar MVarId
c) = MVarId -> Lookahead
WillReadMVar MVarId
c
rewind (BlockedReadMVar MVarId
c) = MVarId -> Lookahead
WillReadMVar MVarId
c
rewind (TryReadMVar MVarId
c Bool
_) = MVarId -> Lookahead
WillTryReadMVar MVarId
c
rewind (TakeMVar MVarId
c [ThreadId]
_) = MVarId -> Lookahead
WillTakeMVar MVarId
c
rewind (BlockedTakeMVar MVarId
c) = MVarId -> Lookahead
WillTakeMVar MVarId
c
rewind (TryTakeMVar MVarId
c Bool
_ [ThreadId]
_) = MVarId -> Lookahead
WillTryTakeMVar MVarId
c
rewind (NewIORef IORefId
_) = Lookahead
WillNewIORef
rewind (ReadIORef IORefId
c) = IORefId -> Lookahead
WillReadIORef IORefId
c
rewind (ReadIORefCas IORefId
c) = IORefId -> Lookahead
WillReadIORefCas IORefId
c
rewind (ModIORef IORefId
c) = IORefId -> Lookahead
WillModIORef IORefId
c
rewind (ModIORefCas IORefId
c) = IORefId -> Lookahead
WillModIORefCas IORefId
c
rewind (WriteIORef IORefId
c) = IORefId -> Lookahead
WillWriteIORef IORefId
c
rewind (CasIORef IORefId
c Bool
_) = IORefId -> Lookahead
WillCasIORef IORefId
c
rewind (CommitIORef ThreadId
t IORefId
c) = ThreadId -> IORefId -> Lookahead
WillCommitIORef ThreadId
t IORefId
c
rewind (STM [TAction]
_ [ThreadId]
_) = Lookahead
WillSTM
rewind (ThrownSTM [TAction]
_ Maybe MaskingState
_) = Lookahead
WillSTM
rewind (BlockedSTM [TAction]
_) = Lookahead
WillSTM
rewind ThreadAction
Catching = Lookahead
WillCatching
rewind ThreadAction
PopCatching = Lookahead
WillPopCatching
rewind (Throw Maybe MaskingState
_) = Lookahead
WillThrow
rewind (ThrowTo ThreadId
t Maybe MaskingState
_) = ThreadId -> Lookahead
WillThrowTo ThreadId
t
rewind (BlockedThrowTo ThreadId
t) = ThreadId -> Lookahead
WillThrowTo ThreadId
t
rewind (SetMasking Bool
b MaskingState
m) = Bool -> MaskingState -> Lookahead
WillSetMasking Bool
b MaskingState
m
rewind (ResetMasking Bool
b MaskingState
m) = Bool -> MaskingState -> Lookahead
WillResetMasking Bool
b MaskingState
m
rewind (GetMaskingState MaskingState
_) = Lookahead
WillGetMaskingState
rewind ThreadAction
LiftIO = Lookahead
WillLiftIO
rewind ThreadAction
Return = Lookahead
WillReturn
rewind ThreadAction
Stop = Lookahead
WillStop
rewind ThreadAction
RegisterInvariant = Lookahead
WillRegisterInvariant

-- | Check if an operation could enable another thread.
willRelease :: Lookahead -> Bool
willRelease :: Lookahead -> Bool
willRelease Lookahead
WillFork = Bool
True
willRelease Lookahead
WillForkOS = Bool
True
willRelease Lookahead
WillYield = Bool
True
willRelease (WillThreadDelay Int
_) = Bool
True
willRelease (WillPutMVar MVarId
_) = Bool
True
willRelease (WillTryPutMVar MVarId
_) = Bool
True
willRelease (WillReadMVar MVarId
_) = Bool
True
willRelease (WillTakeMVar MVarId
_) = Bool
True
willRelease (WillTryTakeMVar MVarId
_) = Bool
True
willRelease Lookahead
WillSTM = Bool
True
willRelease Lookahead
WillThrow = Bool
True
willRelease (WillSetMasking Bool
_ MaskingState
_) = Bool
True
willRelease (WillResetMasking Bool
_ MaskingState
_) = Bool
True
willRelease Lookahead
WillStop = Bool
True
willRelease Lookahead
_ = Bool
False

-------------------------------------------------------------------------------
-- * Simplified actions

-- | A simplified view of the possible actions a thread can perform.
data ActionType =
    UnsynchronisedRead  IORefId
  -- ^ A 'readIORef' or a 'readForCAS'.
  | UnsynchronisedWrite IORefId
  -- ^ A 'writeIORef'.
  | UnsynchronisedOther
  -- ^ Some other action which doesn't require cross-thread
  -- communication.
  | PartiallySynchronisedCommit IORefId
  -- ^ A commit.
  | PartiallySynchronisedWrite  IORefId
  -- ^ A 'casIORef'
  | PartiallySynchronisedModify IORefId
  -- ^ A 'modifyIORefCAS'
  | SynchronisedModify  IORefId
  -- ^ An 'atomicModifyIORef'.
  | SynchronisedRead    MVarId
  -- ^ A 'readMVar' or 'takeMVar' (or @try@/@blocked@ variants).
  | SynchronisedWrite   MVarId
  -- ^ A 'putMVar' (or @try@/@blocked@ variant).
  | SynchronisedOther
  -- ^ Some other action which does require cross-thread
  -- communication.
  deriving (ActionType -> ActionType -> Bool
(ActionType -> ActionType -> Bool)
-> (ActionType -> ActionType -> Bool) -> Eq ActionType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ActionType -> ActionType -> Bool
== :: ActionType -> ActionType -> Bool
$c/= :: ActionType -> ActionType -> Bool
/= :: ActionType -> ActionType -> Bool
Eq, Int -> ActionType -> ShowS
[ActionType] -> ShowS
ActionType -> String
(Int -> ActionType -> ShowS)
-> (ActionType -> String)
-> ([ActionType] -> ShowS)
-> Show ActionType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ActionType -> ShowS
showsPrec :: Int -> ActionType -> ShowS
$cshow :: ActionType -> String
show :: ActionType -> String
$cshowList :: [ActionType] -> ShowS
showList :: [ActionType] -> ShowS
Show, (forall x. ActionType -> Rep ActionType x)
-> (forall x. Rep ActionType x -> ActionType) -> Generic ActionType
forall x. Rep ActionType x -> ActionType
forall x. ActionType -> Rep ActionType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ActionType -> Rep ActionType x
from :: forall x. ActionType -> Rep ActionType x
$cto :: forall x. Rep ActionType x -> ActionType
to :: forall x. Rep ActionType x -> ActionType
Generic, ActionType -> ()
(ActionType -> ()) -> NFData ActionType
forall a. (a -> ()) -> NFData a
$crnf :: ActionType -> ()
rnf :: ActionType -> ()
NFData)

-- | Check if an action imposes a write barrier.
isBarrier :: ActionType -> Bool
isBarrier :: ActionType -> Bool
isBarrier (SynchronisedModify IORefId
_) = Bool
True
isBarrier (SynchronisedRead   MVarId
_) = Bool
True
isBarrier (SynchronisedWrite  MVarId
_) = Bool
True
isBarrier ActionType
SynchronisedOther = Bool
True
isBarrier ActionType
_ = Bool
False

-- | Check if an action commits a given 'IORef'.
isCommit :: ActionType -> IORefId -> Bool
isCommit :: ActionType -> IORefId -> Bool
isCommit (PartiallySynchronisedCommit IORefId
c) IORefId
r = IORefId
c IORefId -> IORefId -> Bool
forall a. Eq a => a -> a -> Bool
== IORefId
r
isCommit (PartiallySynchronisedWrite  IORefId
c) IORefId
r = IORefId
c IORefId -> IORefId -> Bool
forall a. Eq a => a -> a -> Bool
== IORefId
r
isCommit (PartiallySynchronisedModify IORefId
c) IORefId
r = IORefId
c IORefId -> IORefId -> Bool
forall a. Eq a => a -> a -> Bool
== IORefId
r
isCommit ActionType
_ IORefId
_ = Bool
False

-- | Check if an action synchronises a given 'IORef'.
synchronises :: ActionType -> IORefId -> Bool
synchronises :: ActionType -> IORefId -> Bool
synchronises ActionType
a IORefId
r = ActionType -> IORefId -> Bool
isCommit ActionType
a IORefId
r Bool -> Bool -> Bool
|| ActionType -> Bool
isBarrier ActionType
a

-- | Get the 'IORef' affected.
iorefOf :: ActionType -> Maybe IORefId
iorefOf :: ActionType -> Maybe IORefId
iorefOf (UnsynchronisedRead  IORefId
r) = IORefId -> Maybe IORefId
forall a. a -> Maybe a
Just IORefId
r
iorefOf (UnsynchronisedWrite IORefId
r) = IORefId -> Maybe IORefId
forall a. a -> Maybe a
Just IORefId
r
iorefOf (SynchronisedModify  IORefId
r) = IORefId -> Maybe IORefId
forall a. a -> Maybe a
Just IORefId
r
iorefOf (PartiallySynchronisedCommit IORefId
r) = IORefId -> Maybe IORefId
forall a. a -> Maybe a
Just IORefId
r
iorefOf (PartiallySynchronisedWrite  IORefId
r) = IORefId -> Maybe IORefId
forall a. a -> Maybe a
Just IORefId
r
iorefOf (PartiallySynchronisedModify IORefId
r) = IORefId -> Maybe IORefId
forall a. a -> Maybe a
Just IORefId
r
iorefOf ActionType
_ = Maybe IORefId
forall a. Maybe a
Nothing

-- | Get the 'MVar' affected.
mvarOf :: ActionType -> Maybe MVarId
mvarOf :: ActionType -> Maybe MVarId
mvarOf (SynchronisedRead  MVarId
c) = MVarId -> Maybe MVarId
forall a. a -> Maybe a
Just MVarId
c
mvarOf (SynchronisedWrite MVarId
c) = MVarId -> Maybe MVarId
forall a. a -> Maybe a
Just MVarId
c
mvarOf ActionType
_ = Maybe MVarId
forall a. Maybe a
Nothing

-- | Get the @ThreadId@s involved in a @ThreadAction@.
tidsOf :: ThreadAction -> Set ThreadId
tidsOf :: ThreadAction -> Set ThreadId
tidsOf (Fork ThreadId
tid) = ThreadId -> Set ThreadId
forall a. a -> Set a
S.singleton ThreadId
tid
tidsOf (ForkOS ThreadId
tid) = ThreadId -> Set ThreadId
forall a. a -> Set a
S.singleton ThreadId
tid
tidsOf (PutMVar MVarId
_ [ThreadId]
tids) = [ThreadId] -> Set ThreadId
forall a. Ord a => [a] -> Set a
S.fromList [ThreadId]
tids
tidsOf (TryPutMVar MVarId
_ Bool
_ [ThreadId]
tids) = [ThreadId] -> Set ThreadId
forall a. Ord a => [a] -> Set a
S.fromList [ThreadId]
tids
tidsOf (TakeMVar MVarId
_ [ThreadId]
tids) = [ThreadId] -> Set ThreadId
forall a. Ord a => [a] -> Set a
S.fromList [ThreadId]
tids
tidsOf (TryTakeMVar MVarId
_ Bool
_ [ThreadId]
tids) = [ThreadId] -> Set ThreadId
forall a. Ord a => [a] -> Set a
S.fromList [ThreadId]
tids
tidsOf (CommitIORef ThreadId
tid IORefId
_) = ThreadId -> Set ThreadId
forall a. a -> Set a
S.singleton ThreadId
tid
tidsOf (STM [TAction]
_ [ThreadId]
tids) = [ThreadId] -> Set ThreadId
forall a. Ord a => [a] -> Set a
S.fromList [ThreadId]
tids
tidsOf (ThrowTo ThreadId
tid Maybe MaskingState
_) = ThreadId -> Set ThreadId
forall a. a -> Set a
S.singleton ThreadId
tid
tidsOf (BlockedThrowTo ThreadId
tid) = ThreadId -> Set ThreadId
forall a. a -> Set a
S.singleton ThreadId
tid
tidsOf ThreadAction
_ = Set ThreadId
forall a. Set a
S.empty

-- | Throw away information from a 'ThreadAction' and give a
-- simplified view of what is happening.
--
-- This is used in the SCT code to help determine interesting
-- alternative scheduling decisions.
simplifyAction :: ThreadAction -> ActionType
simplifyAction :: ThreadAction -> ActionType
simplifyAction = Lookahead -> ActionType
simplifyLookahead (Lookahead -> ActionType)
-> (ThreadAction -> Lookahead) -> ThreadAction -> ActionType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreadAction -> Lookahead
rewind

-- | Variant of 'simplifyAction' that takes a 'Lookahead'.
simplifyLookahead :: Lookahead -> ActionType
simplifyLookahead :: Lookahead -> ActionType
simplifyLookahead (WillPutMVar MVarId
c)     = MVarId -> ActionType
SynchronisedWrite MVarId
c
simplifyLookahead (WillTryPutMVar MVarId
c)  = MVarId -> ActionType
SynchronisedWrite MVarId
c
simplifyLookahead (WillReadMVar MVarId
c)    = MVarId -> ActionType
SynchronisedRead MVarId
c
simplifyLookahead (WillTryReadMVar MVarId
c) = MVarId -> ActionType
SynchronisedRead MVarId
c
simplifyLookahead (WillTakeMVar MVarId
c)    = MVarId -> ActionType
SynchronisedRead MVarId
c
simplifyLookahead (WillTryTakeMVar MVarId
c)  = MVarId -> ActionType
SynchronisedRead MVarId
c
simplifyLookahead (WillReadIORef IORefId
r)     = IORefId -> ActionType
UnsynchronisedRead IORefId
r
simplifyLookahead (WillReadIORefCas IORefId
r)  = IORefId -> ActionType
UnsynchronisedRead IORefId
r
simplifyLookahead (WillModIORef IORefId
r)      = IORefId -> ActionType
SynchronisedModify IORefId
r
simplifyLookahead (WillModIORefCas IORefId
r)   = IORefId -> ActionType
PartiallySynchronisedModify IORefId
r
simplifyLookahead (WillWriteIORef IORefId
r)    = IORefId -> ActionType
UnsynchronisedWrite IORefId
r
simplifyLookahead (WillCasIORef IORefId
r)      = IORefId -> ActionType
PartiallySynchronisedWrite IORefId
r
simplifyLookahead (WillCommitIORef ThreadId
_ IORefId
r) = IORefId -> ActionType
PartiallySynchronisedCommit IORefId
r
simplifyLookahead Lookahead
WillSTM         = ActionType
SynchronisedOther
simplifyLookahead (WillThrowTo ThreadId
_) = ActionType
SynchronisedOther
simplifyLookahead Lookahead
_ = ActionType
UnsynchronisedOther

-------------------------------------------------------------------------------
-- * Concurrency state

-- | Initial concurrency state.
initialCState :: ConcurrencyState
initialCState :: ConcurrencyState
initialCState = Map IORefId Int
-> Set MVarId -> Map ThreadId MaskingState -> ConcurrencyState
ConcurrencyState Map IORefId Int
forall k a. Map k a
M.empty Set MVarId
forall a. Set a
S.empty Map ThreadId MaskingState
forall k a. Map k a
M.empty

-- | Update the concurrency state with the action that has just
-- happened.
updateCState :: MemType -> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState :: MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
cstate ThreadId
tid ThreadAction
act = ConcurrencyState
  { concIOState :: Map IORefId Int
concIOState   = MemType -> ThreadAction -> Map IORefId Int -> Map IORefId Int
updateIOState MemType
memtype ThreadAction
act (Map IORefId Int -> Map IORefId Int)
-> Map IORefId Int -> Map IORefId Int
forall a b. (a -> b) -> a -> b
$ ConcurrencyState -> Map IORefId Int
concIOState   ConcurrencyState
cstate
  , concMVState :: Set MVarId
concMVState   = ThreadAction -> Set MVarId -> Set MVarId
updateMVState         ThreadAction
act (Set MVarId -> Set MVarId) -> Set MVarId -> Set MVarId
forall a b. (a -> b) -> a -> b
$ ConcurrencyState -> Set MVarId
concMVState   ConcurrencyState
cstate
  , concMaskState :: Map ThreadId MaskingState
concMaskState = ThreadId
-> ThreadAction
-> Map ThreadId MaskingState
-> Map ThreadId MaskingState
updateMaskState ThreadId
tid   ThreadAction
act (Map ThreadId MaskingState -> Map ThreadId MaskingState)
-> Map ThreadId MaskingState -> Map ThreadId MaskingState
forall a b. (a -> b) -> a -> b
$ ConcurrencyState -> Map ThreadId MaskingState
concMaskState ConcurrencyState
cstate
  }

-- | Update the @IORef@ buffer state with the action that has just
-- happened.
updateIOState :: MemType -> ThreadAction -> Map IORefId Int -> Map IORefId Int
updateIOState :: MemType -> ThreadAction -> Map IORefId Int -> Map IORefId Int
updateIOState MemType
SequentialConsistency ThreadAction
_ = Map IORefId Int -> Map IORefId Int -> Map IORefId Int
forall a b. a -> b -> a
const Map IORefId Int
forall k a. Map k a
M.empty
updateIOState MemType
_ (CommitIORef ThreadId
_ IORefId
r) = ((Maybe Int -> Maybe Int)
-> IORefId -> Map IORefId Int -> Map IORefId Int
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
`M.alter` IORefId
r) ((Maybe Int -> Maybe Int) -> Map IORefId Int -> Map IORefId Int)
-> (Maybe Int -> Maybe Int) -> Map IORefId Int -> Map IORefId Int
forall a b. (a -> b) -> a -> b
$ \case
  Just Int
1  -> Maybe Int
forall a. Maybe a
Nothing
  Just Int
n  -> Int -> Maybe Int
forall a. a -> Maybe a
Just (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
  Maybe Int
Nothing -> Maybe Int
forall a. Maybe a
Nothing
updateIOState MemType
_ (WriteIORef    IORefId
r) = (Int -> Int -> Int)
-> IORefId -> Int -> Map IORefId Int -> Map IORefId Int
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) IORefId
r Int
1
updateIOState MemType
_ ThreadAction
ta
  | ActionType -> Bool
isBarrier (ActionType -> Bool) -> ActionType -> Bool
forall a b. (a -> b) -> a -> b
$ ThreadAction -> ActionType
simplifyAction ThreadAction
ta = Map IORefId Int -> Map IORefId Int -> Map IORefId Int
forall a b. a -> b -> a
const Map IORefId Int
forall k a. Map k a
M.empty
  | Bool
otherwise = Map IORefId Int -> Map IORefId Int
forall a. a -> a
id

-- | Update the @MVar@ full/empty state with the action that has just
-- happened.
updateMVState :: ThreadAction -> Set MVarId -> Set MVarId
updateMVState :: ThreadAction -> Set MVarId -> Set MVarId
updateMVState (PutMVar MVarId
mvid [ThreadId]
_) = MVarId -> Set MVarId -> Set MVarId
forall a. Ord a => a -> Set a -> Set a
S.insert MVarId
mvid
updateMVState (TryPutMVar MVarId
mvid Bool
True [ThreadId]
_) = MVarId -> Set MVarId -> Set MVarId
forall a. Ord a => a -> Set a -> Set a
S.insert MVarId
mvid
updateMVState (TakeMVar MVarId
mvid [ThreadId]
_) = MVarId -> Set MVarId -> Set MVarId
forall a. Ord a => a -> Set a -> Set a
S.delete MVarId
mvid
updateMVState (TryTakeMVar MVarId
mvid Bool
True [ThreadId]
_) = MVarId -> Set MVarId -> Set MVarId
forall a. Ord a => a -> Set a -> Set a
S.delete MVarId
mvid
updateMVState ThreadAction
_ = Set MVarId -> Set MVarId
forall a. a -> a
id

-- | Update the thread masking state with the action that has just
-- happened.
updateMaskState :: ThreadId -> ThreadAction -> Map ThreadId MaskingState -> Map ThreadId MaskingState
updateMaskState :: ThreadId
-> ThreadAction
-> Map ThreadId MaskingState
-> Map ThreadId MaskingState
updateMaskState ThreadId
tid (Fork ThreadId
tid2) = \Map ThreadId MaskingState
masks -> case ThreadId -> Map ThreadId MaskingState -> Maybe MaskingState
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ThreadId
tid Map ThreadId MaskingState
masks of
  -- A thread inherits the masking state of its parent.
  Just MaskingState
ms -> ThreadId
-> MaskingState
-> Map ThreadId MaskingState
-> Map ThreadId MaskingState
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ThreadId
tid2 MaskingState
ms Map ThreadId MaskingState
masks
  Maybe MaskingState
Nothing -> Map ThreadId MaskingState
masks
updateMaskState ThreadId
tid (SetMasking   Bool
_ MaskingState
ms) = ThreadId
-> MaskingState
-> Map ThreadId MaskingState
-> Map ThreadId MaskingState
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ThreadId
tid MaskingState
ms
updateMaskState ThreadId
tid (ResetMasking Bool
_ MaskingState
ms) = ThreadId
-> MaskingState
-> Map ThreadId MaskingState
-> Map ThreadId MaskingState
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ThreadId
tid MaskingState
ms
updateMaskState ThreadId
tid (Throw Maybe MaskingState
Nothing) = ThreadId -> Map ThreadId MaskingState -> Map ThreadId MaskingState
forall k a. Ord k => k -> Map k a -> Map k a
M.delete ThreadId
tid
updateMaskState ThreadId
tid (Throw (Just MaskingState
ms)) = ThreadId
-> MaskingState
-> Map ThreadId MaskingState
-> Map ThreadId MaskingState
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ThreadId
tid MaskingState
ms
updateMaskState ThreadId
tid (ThrownSTM [TAction]
_ Maybe MaskingState
Nothing) = ThreadId -> Map ThreadId MaskingState -> Map ThreadId MaskingState
forall k a. Ord k => k -> Map k a -> Map k a
M.delete ThreadId
tid
updateMaskState ThreadId
tid (ThrownSTM [TAction]
_ (Just MaskingState
ms)) = ThreadId
-> MaskingState
-> Map ThreadId MaskingState
-> Map ThreadId MaskingState
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ThreadId
tid MaskingState
ms
updateMaskState ThreadId
_ (ThrowTo ThreadId
tid Maybe MaskingState
Nothing) = ThreadId -> Map ThreadId MaskingState -> Map ThreadId MaskingState
forall k a. Ord k => k -> Map k a -> Map k a
M.delete ThreadId
tid
updateMaskState ThreadId
_ (ThrowTo ThreadId
tid (Just MaskingState
ms)) = ThreadId
-> MaskingState
-> Map ThreadId MaskingState
-> Map ThreadId MaskingState
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ThreadId
tid MaskingState
ms
updateMaskState ThreadId
tid ThreadAction
Stop = ThreadId -> Map ThreadId MaskingState -> Map ThreadId MaskingState
forall k a. Ord k => k -> Map k a -> Map k a
M.delete ThreadId
tid
updateMaskState ThreadId
_ ThreadAction
_ = Map ThreadId MaskingState -> Map ThreadId MaskingState
forall a. a -> a
id

-------------------------------------------------------------------------------
-- * Error reporting

-- | 'tail' but with a better error message if it fails.  Use this
-- only where it shouldn't fail!
etail :: HasCallStack => [a] -> [a]
etail :: forall a. HasCallStack => [a] -> [a]
etail (a
_:[a]
xs) = [a]
xs
etail [a]
_ = (HasCallStack => [a]) -> [a]
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => [a]) -> [a]) -> (HasCallStack => [a]) -> [a]
forall a b. (a -> b) -> a -> b
$ String -> [a]
forall a. HasCallStack => String -> a
fatal String
"tail: empty list"

-- | '(!!)' but with a better error message if it fails.  Use this
-- only where it shouldn't fail!
eidx :: HasCallStack => [a] -> Int -> a
eidx :: forall a. HasCallStack => [a] -> Int -> a
eidx [a]
xs Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs = [a]
xs [a] -> Int -> a
forall a. HasCallStack => [a] -> Int -> a
!! Int
i
  | Bool
otherwise = (HasCallStack => a) -> a
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => a) -> a) -> (HasCallStack => a) -> a
forall a b. (a -> b) -> a -> b
$ String -> a
forall a. HasCallStack => String -> a
fatal String
"(!!): index too large"

-- | 'fromJust' but with a better error message if it fails.  Use this
-- only where it shouldn't fail!
efromJust :: HasCallStack => Maybe a -> a
efromJust :: forall a. HasCallStack => Maybe a -> a
efromJust (Just a
x) = a
x
efromJust Maybe a
_ = (HasCallStack => a) -> a
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => a) -> a) -> (HasCallStack => a) -> a
forall a b. (a -> b) -> a -> b
$ String -> a
forall a. HasCallStack => String -> a
fatal String
"fromJust: Nothing"

-- | 'fromList' but with a better error message if it fails.  Use this
-- only where it shouldn't fail!
efromList :: HasCallStack => [a] -> NonEmpty a
efromList :: forall a. HasCallStack => [a] -> NonEmpty a
efromList (a
x:[a]
xs) = a
xa -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:|[a]
xs
efromList [a]
_ = (HasCallStack => NonEmpty a) -> NonEmpty a
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => NonEmpty a) -> NonEmpty a)
-> (HasCallStack => NonEmpty a) -> NonEmpty a
forall a b. (a -> b) -> a -> b
$ String -> NonEmpty a
forall a. HasCallStack => String -> a
fatal String
"fromList: empty list"

-- | 'fromRight' but with a better error message if it fails.  Use
-- this only where it shouldn't fail!
efromRight :: HasCallStack => Either a b -> b
efromRight :: forall a b. HasCallStack => Either a b -> b
efromRight (Right b
b) = b
b
efromRight Either a b
_ = (HasCallStack => b) -> b
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => b) -> b) -> (HasCallStack => b) -> b
forall a b. (a -> b) -> a -> b
$ String -> b
forall a. HasCallStack => String -> a
fatal String
"fromRight: Left"

-- | 'fromLeft' but with a better error message if it fails.  Use
-- this only where it shouldn't fail!
efromLeft :: HasCallStack => Either a b -> a
efromLeft :: forall a b. HasCallStack => Either a b -> a
efromLeft (Left a
a) = a
a
efromLeft Either a b
_ = (HasCallStack => a) -> a
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => a) -> a) -> (HasCallStack => a) -> a
forall a b. (a -> b) -> a -> b
$ String -> a
forall a. HasCallStack => String -> a
fatal String
"fromLeft: Right"

-- | 'M.adjust' but which errors if the key is not present.  Use this
-- only where it shouldn't fail!
eadjust :: (Ord k, Show k, HasCallStack) => (v -> v) -> k -> M.Map k v -> M.Map k v
eadjust :: forall k v.
(Ord k, Show k, HasCallStack) =>
(v -> v) -> k -> Map k v -> Map k v
eadjust v -> v
f k
k Map k v
m = case k -> Map k v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup k
k Map k v
m of
  Just v
v -> k -> v -> Map k v -> Map k v
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert k
k (v -> v
f v
v) Map k v
m
  Maybe v
Nothing -> (HasCallStack => Map k v) -> Map k v
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => Map k v) -> Map k v)
-> (HasCallStack => Map k v) -> Map k v
forall a b. (a -> b) -> a -> b
$ String -> Map k v
forall a. HasCallStack => String -> a
fatal (String
"adjust: key '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ k -> String
forall a. Show a => a -> String
show k
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"' not found")

-- | 'M.insert' but which errors if the key is already present.  Use
-- this only where it shouldn't fail!
einsert :: (Ord k, Show k, HasCallStack) => k -> v -> M.Map k v -> M.Map k v
einsert :: forall k v.
(Ord k, Show k, HasCallStack) =>
k -> v -> Map k v -> Map k v
einsert k
k v
v Map k v
m
  | k -> Map k v -> Bool
forall k a. Ord k => k -> Map k a -> Bool
M.member k
k Map k v
m = (HasCallStack => Map k v) -> Map k v
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => Map k v) -> Map k v)
-> (HasCallStack => Map k v) -> Map k v
forall a b. (a -> b) -> a -> b
$ String -> Map k v
forall a. HasCallStack => String -> a
fatal (String
"insert: key '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ k -> String
forall a. Show a => a -> String
show k
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"' already present")
  | Bool
otherwise = k -> v -> Map k v -> Map k v
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert k
k v
v Map k v
m

-- | 'M.lookup' but which errors if the key is not present.  Use this
-- only where it shouldn't fail!
elookup :: (Ord k, Show k, HasCallStack) => k -> M.Map k v -> v
elookup :: forall k v. (Ord k, Show k, HasCallStack) => k -> Map k v -> v
elookup k
k =
  v -> Maybe v -> v
forall a. a -> Maybe a -> a
fromMaybe ((HasCallStack => v) -> v
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => v) -> v) -> (HasCallStack => v) -> v
forall a b. (a -> b) -> a -> b
$ String -> v
forall a. HasCallStack => String -> a
fatal (String
"lookup: key '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ k -> String
forall a. Show a => a -> String
show k
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"' not found")) (Maybe v -> v) -> (Map k v -> Maybe v) -> Map k v -> v
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  k -> Map k v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup k
k

-- | 'error' but saying where it came from
fatal :: HasCallStack => String -> a
fatal :: forall a. HasCallStack => String -> a
fatal String
msg = (HasCallStack => a) -> a
forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack ((HasCallStack => a) -> a) -> (HasCallStack => a) -> a
forall a b. (a -> b) -> a -> b
$ String -> a
forall a. HasCallStack => String -> a
error (String
"(dejafu) " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg)

-------------------------------------------------------------------------------
-- * Miscellaneous

-- | Run with a continuation that writes its value into a reference,
-- returning the computation and the reference.  Using the reference
-- is non-blocking, it is up to you to ensure you wait sufficiently.
runRefCont :: MonadDejaFu n
  => (n () -> x)
  -> (a -> Maybe b)
  -> ((a -> x) -> x)
  -> n (x, Ref n (Maybe b))
runRefCont :: forall (n :: * -> *) x a b.
MonadDejaFu n =>
(n () -> x)
-> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, Ref n (Maybe b))
runRefCont n () -> x
act a -> Maybe b
f (a -> x) -> x
k = do
  Ref n (Maybe b)
ref <- Maybe b -> n (Ref n (Maybe b))
forall a. a -> n (Ref n a)
forall (m :: * -> *) a. MonadDejaFu m => a -> m (Ref m a)
newRef Maybe b
forall a. Maybe a
Nothing
  let c :: x
c = (a -> x) -> x
k (n () -> x
act (n () -> x) -> (a -> n ()) -> a -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ref n (Maybe b) -> Maybe b -> n ()
forall a. Ref n a -> a -> n ()
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n (Maybe b)
ref (Maybe b -> n ()) -> (a -> Maybe b) -> a -> n ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe b
f)
  (x, Ref n (Maybe b)) -> n (x, Ref n (Maybe b))
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (x
c, Ref n (Maybe b)
ref)