{-# LANGUAGE CPP #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeFamilies #-}

-- Must come after TypeFamilies
{-# LANGUAGE NoMonoLocalBinds #-}

-- |
-- Module      : Test.DejaFu.Conc.Internal.STM
-- Copyright   : (c) 2017--2019 Michael Walker
-- License     : MIT
-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
-- Stability   : experimental
-- Portability : CPP, ExistentialQuantification, NoMonoLocalBinds, RecordWildCards, TypeFamilies
--
-- 'MonadSTM' testing implementation, internal types and definitions.
-- This module is NOT considered to form part of the public interface
-- of this library.
module Test.DejaFu.Conc.Internal.STM where

import           Control.Applicative     (Alternative(..))
import           Control.Exception       (Exception, SomeException,
                                          fromException, toException)
import           Control.Monad           (MonadPlus(..))
import           Control.Monad.Catch     (MonadCatch(..), MonadThrow(..))
import qualified Control.Monad.Fail      as Fail
import qualified Control.Monad.STM.Class as S
import           Data.List               (nub)

import           Test.DejaFu.Internal
import           Test.DejaFu.Types

--------------------------------------------------------------------------------
-- * The @ModelSTM@ monad

-- | The underlying monad is based on continuations over primitive
-- actions.
--
-- This is not @Cont@ because we want to give it a custom @MonadFail@
-- instance.
newtype ModelSTM n a = ModelSTM { forall (n :: * -> *) a.
ModelSTM n a -> (a -> STMAction n) -> STMAction n
runModelSTM :: (a -> STMAction n) -> STMAction n }

instance Functor (ModelSTM n) where
    fmap :: forall a b. (a -> b) -> ModelSTM n a -> ModelSTM n b
fmap a -> b
f ModelSTM n a
m = forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM forall a b. (a -> b) -> a -> b
$ \b -> STMAction n
c -> forall (n :: * -> *) a.
ModelSTM n a -> (a -> STMAction n) -> STMAction n
runModelSTM ModelSTM n a
m (b -> STMAction n
c forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f)

instance Applicative (ModelSTM n) where
    pure :: forall a. a -> ModelSTM n a
pure a
x  = forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM forall a b. (a -> b) -> a -> b
$ \a -> STMAction n
c -> a -> STMAction n
c a
x
    ModelSTM n (a -> b)
f <*> :: forall a b. ModelSTM n (a -> b) -> ModelSTM n a -> ModelSTM n b
<*> ModelSTM n a
v = forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM forall a b. (a -> b) -> a -> b
$ \b -> STMAction n
c -> forall (n :: * -> *) a.
ModelSTM n a -> (a -> STMAction n) -> STMAction n
runModelSTM ModelSTM n (a -> b)
f (\a -> b
g -> forall (n :: * -> *) a.
ModelSTM n a -> (a -> STMAction n) -> STMAction n
runModelSTM ModelSTM n a
v (b -> STMAction n
c forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
g))

instance Monad (ModelSTM n) where
    return :: forall a. a -> ModelSTM n a
return  = forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ModelSTM n a
m >>= :: forall a b. ModelSTM n a -> (a -> ModelSTM n b) -> ModelSTM n b
>>= a -> ModelSTM n b
k = forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM forall a b. (a -> b) -> a -> b
$ \b -> STMAction n
c -> forall (n :: * -> *) a.
ModelSTM n a -> (a -> STMAction n) -> STMAction n
runModelSTM ModelSTM n a
m (\a
x -> forall (n :: * -> *) a.
ModelSTM n a -> (a -> STMAction n) -> STMAction n
runModelSTM (a -> ModelSTM n b
k a
x) b -> STMAction n
c)

#if MIN_VERSION_base(4,13,0)
#else
    fail = Fail.fail
#endif

instance Fail.MonadFail (ModelSTM n) where
    fail :: forall a. String -> ModelSTM n a
fail String
e = forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM forall a b. (a -> b) -> a -> b
$ \a -> STMAction n
_ -> forall (n :: * -> *) e. Exception e => e -> STMAction n
SThrow (String -> MonadFailException
MonadFailException String
e)

instance MonadThrow (ModelSTM n) where
  throwM :: forall e a. Exception e => e -> ModelSTM n a
throwM e
e = forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM forall a b. (a -> b) -> a -> b
$ \a -> STMAction n
_ -> forall (n :: * -> *) e. Exception e => e -> STMAction n
SThrow e
e

instance MonadCatch (ModelSTM n) where
  catch :: forall e a.
Exception e =>
ModelSTM n a -> (e -> ModelSTM n a) -> ModelSTM n a
catch ModelSTM n a
stm e -> ModelSTM n a
handler = forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM forall a b. (a -> b) -> a -> b
$ forall (n :: * -> *) a e.
Exception e =>
(e -> ModelSTM n a)
-> ModelSTM n a -> (a -> STMAction n) -> STMAction n
SCatch e -> ModelSTM n a
handler ModelSTM n a
stm

instance Alternative (ModelSTM n) where
  ModelSTM n a
a <|> :: forall a. ModelSTM n a -> ModelSTM n a -> ModelSTM n a
<|> ModelSTM n a
b = forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM forall a b. (a -> b) -> a -> b
$ forall (n :: * -> *) a.
ModelSTM n a -> ModelSTM n a -> (a -> STMAction n) -> STMAction n
SOrElse ModelSTM n a
a ModelSTM n a
b
  empty :: forall a. ModelSTM n a
empty = forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall (n :: * -> *). STMAction n
SRetry

instance MonadPlus (ModelSTM n)

instance S.MonadSTM (ModelSTM n) where
  type TVar (ModelSTM n) = ModelTVar n

  newTVarN :: forall a. String -> a -> ModelSTM n (TVar (ModelSTM n) a)
newTVarN String
n = forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *) a.
String -> a -> (ModelTVar n a -> STMAction n) -> STMAction n
SNew String
n

  readTVar :: forall a. TVar (ModelSTM n) a -> ModelSTM n a
readTVar = forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *) a.
ModelTVar n a -> (a -> STMAction n) -> STMAction n
SRead

  writeTVar :: forall a. TVar (ModelSTM n) a -> a -> ModelSTM n ()
writeTVar TVar (ModelSTM n) a
tvar a
a = forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM forall a b. (a -> b) -> a -> b
$ \() -> STMAction n
c -> forall (n :: * -> *) a.
ModelTVar n a -> a -> STMAction n -> STMAction n
SWrite TVar (ModelSTM n) a
tvar a
a (() -> STMAction n
c ())

--------------------------------------------------------------------------------
-- * Primitive actions

-- | STM transactions are represented as a sequence of primitive
-- actions.
data STMAction n
  = forall a e. Exception e => SCatch (e -> ModelSTM n a) (ModelSTM n a) (a -> STMAction n)
  | forall a. SRead  (ModelTVar n a) (a -> STMAction n)
  | forall a. SWrite (ModelTVar n a) a (STMAction n)
  | forall a. SOrElse (ModelSTM n a) (ModelSTM n a) (a -> STMAction n)
  | forall a. SNew String a (ModelTVar n a -> STMAction n)
  | forall e. Exception e => SThrow e
  | SRetry
  | SStop (n ())

--------------------------------------------------------------------------------
-- * @TVar@s

-- | A @TVar@ is modelled as a unique ID and a reference holding a
-- value.
data ModelTVar n a = ModelTVar
  { forall (n :: * -> *) a. ModelTVar n a -> TVarId
tvarId  :: TVarId
  , forall (n :: * -> *) a. ModelTVar n a -> Ref n a
tvarRef :: Ref n a
  }

--------------------------------------------------------------------------------
-- * Output

-- | The result of an STM transaction, along with which 'TVar's it
-- touched whilst executing.
data Result a =
    Success [TVarId] [TVarId] a
  -- ^ The transaction completed successfully, reading the first list
  -- 'TVar's and writing to the second.
  | Retry [TVarId]
  -- ^ The transaction aborted by calling 'retry', and read the
  -- returned 'TVar's. It should be retried when at least one of the
  -- 'TVar's has been mutated.
  | Exception SomeException
  -- ^ The transaction aborted by throwing an exception.
  deriving Int -> Result a -> ShowS
forall a. Show a => Int -> Result a -> ShowS
forall a. Show a => [Result a] -> ShowS
forall a. Show a => Result a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Result a] -> ShowS
$cshowList :: forall a. Show a => [Result a] -> ShowS
show :: Result a -> String
$cshow :: forall a. Show a => Result a -> String
showsPrec :: Int -> Result a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Result a -> ShowS
Show


--------------------------------------------------------------------------------
-- * Execution

-- | Run a transaction, returning the result and new initial 'TVarId'.
-- If the transaction failed, any effects are undone.
runTransaction :: MonadDejaFu n
  => ModelSTM n a
  -> IdSource
  -> n (Result a, n (), IdSource, [TAction])
runTransaction :: forall (n :: * -> *) a.
MonadDejaFu n =>
ModelSTM n a -> IdSource -> n (Result a, n (), IdSource, [TAction])
runTransaction ModelSTM n a
ma IdSource
tvid = do
  (Result a
res, n ()
effect, n ()
_, IdSource
tvid', [TAction]
trace) <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelSTM n a
-> IdSource -> n (Result a, n (), n (), IdSource, [TAction])
doTransaction ModelSTM n a
ma IdSource
tvid
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Result a
res, n ()
effect, IdSource
tvid', [TAction]
trace)

-- | Run a STM transaction, returning an action to undo its effects.
--
-- If the transaction fails, its effects will automatically be undone,
-- so the undo action returned will be @pure ()@.
doTransaction :: MonadDejaFu n
  => ModelSTM n a
  -> IdSource
  -> n (Result a, n (), n (), IdSource, [TAction])
doTransaction :: forall (n :: * -> *) a.
MonadDejaFu n =>
ModelSTM n a
-> IdSource -> n (Result a, n (), n (), IdSource, [TAction])
doTransaction ModelSTM n a
ma IdSource
idsource = do
  (STMAction n
c, Ref n (Maybe (Either SomeException a))
ref) <- forall (n :: * -> *) x a b.
MonadDejaFu n =>
(n () -> x)
-> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, Ref n (Maybe b))
runRefCont forall (n :: * -> *). n () -> STMAction n
SStop (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right) (forall (n :: * -> *) a.
ModelSTM n a -> (a -> STMAction n) -> STMAction n
runModelSTM ModelSTM n a
ma)
  (IdSource
idsource', n ()
effect, n ()
undo, [TVarId]
readen, [TVarId]
written, [TAction]
trace) <- forall {m :: * -> *} {b} {b}.
MonadDejaFu m =>
Ref m (Maybe (Either SomeException b))
-> STMAction m
-> m ()
-> m b
-> IdSource
-> [TVarId]
-> [TVarId]
-> [TAction]
-> m (IdSource, m (), m b, [TVarId], [TVarId], [TAction])
go Ref n (Maybe (Either SomeException a))
ref STMAction n
c (forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) IdSource
idsource [] [] []
  Maybe (Either SomeException a)
res <- forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n (Maybe (Either SomeException a))
ref

  case Maybe (Either SomeException a)
res of
    Just (Right a
val) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. [TVarId] -> [TVarId] -> a -> Result a
Success (forall a. Eq a => [a] -> [a]
nub [TVarId]
readen) (forall a. Eq a => [a] -> [a]
nub [TVarId]
written) a
val, n ()
effect, n ()
undo, IdSource
idsource', forall a. [a] -> [a]
reverse [TAction]
trace)
    Just (Left  SomeException
exc) -> n ()
undo forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. SomeException -> Result a
Exception SomeException
exc,      forall (f :: * -> *) a. Applicative f => a -> f a
pure (), forall (f :: * -> *) a. Applicative f => a -> f a
pure (), IdSource
idsource, forall a. [a] -> [a]
reverse [TAction]
trace)
    Maybe (Either SomeException a)
Nothing          -> n ()
undo forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. [TVarId] -> Result a
Retry forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a]
nub [TVarId]
readen, forall (f :: * -> *) a. Applicative f => a -> f a
pure (), forall (f :: * -> *) a. Applicative f => a -> f a
pure (), IdSource
idsource, forall a. [a] -> [a]
reverse [TAction]
trace)

  where
    go :: Ref m (Maybe (Either SomeException b))
-> STMAction m
-> m ()
-> m b
-> IdSource
-> [TVarId]
-> [TVarId]
-> [TAction]
-> m (IdSource, m (), m b, [TVarId], [TVarId], [TAction])
go Ref m (Maybe (Either SomeException b))
ref STMAction m
act m ()
effect m b
undo IdSource
nidsrc [TVarId]
readen [TVarId]
written [TAction]
sofar = do
      (STMAction m
act', m ()
effect', m ()
undo', IdSource
nidsrc', [TVarId]
readen', [TVarId]
written', TAction
tact) <- forall (n :: * -> *).
MonadDejaFu n =>
STMAction n
-> IdSource
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
stepTrans STMAction m
act IdSource
nidsrc

      let newIDSource :: IdSource
newIDSource = IdSource
nidsrc'
          newAct :: STMAction m
newAct = STMAction m
act'
          newEffect :: m ()
newEffect = m ()
effect forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m ()
effect'
          newUndo :: m b
newUndo = m ()
undo' forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m b
undo
          newReaden :: [TVarId]
newReaden = [TVarId]
readen' forall a. [a] -> [a] -> [a]
++ [TVarId]
readen
          newWritten :: [TVarId]
newWritten = [TVarId]
written' forall a. [a] -> [a] -> [a]
++ [TVarId]
written
          newSofar :: [TAction]
newSofar = TAction
tact forall a. a -> [a] -> [a]
: [TAction]
sofar

      case TAction
tact of
        TAction
TStop  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (IdSource
newIDSource, m ()
newEffect, m b
newUndo, [TVarId]
newReaden, [TVarId]
newWritten, TAction
TStopforall a. a -> [a] -> [a]
:[TAction]
newSofar)
        TAction
TRetry -> do
          forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref m (Maybe (Either SomeException b))
ref forall a. Maybe a
Nothing
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (IdSource
newIDSource, m ()
newEffect, m b
newUndo, [TVarId]
newReaden, [TVarId]
newWritten, TAction
TRetryforall a. a -> [a] -> [a]
:[TAction]
newSofar)
        TAction
TThrow -> do
          forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref m (Maybe (Either SomeException b))
ref (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ case STMAction m
act of SThrow e
e -> forall e. Exception e => e -> SomeException
toException e
e; STMAction m
_ -> forall a. HasCallStack => a
undefined)
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (IdSource
newIDSource, m ()
newEffect, m b
newUndo, [TVarId]
newReaden, [TVarId]
newWritten, TAction
TThrowforall a. a -> [a] -> [a]
:[TAction]
newSofar)
        TAction
_ -> Ref m (Maybe (Either SomeException b))
-> STMAction m
-> m ()
-> m b
-> IdSource
-> [TVarId]
-> [TVarId]
-> [TAction]
-> m (IdSource, m (), m b, [TVarId], [TVarId], [TAction])
go Ref m (Maybe (Either SomeException b))
ref STMAction m
newAct m ()
newEffect m b
newUndo IdSource
newIDSource [TVarId]
newReaden [TVarId]
newWritten [TAction]
newSofar

-- | Run a transaction for one step.
stepTrans :: MonadDejaFu n
  => STMAction n
  -> IdSource
  -> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], TAction)
stepTrans :: forall (n :: * -> *).
MonadDejaFu n =>
STMAction n
-> IdSource
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
stepTrans STMAction n
act IdSource
idsource = case STMAction n
act of
  SCatch  e -> ModelSTM n a
h ModelSTM n a
stm a -> STMAction n
c -> forall {t} {t} {n :: * -> *}.
Exception t =>
(t -> ModelSTM n t)
-> ModelSTM n t
-> (t -> STMAction n)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
stepCatch e -> ModelSTM n a
h ModelSTM n a
stm a -> STMAction n
c
  SRead   ModelTVar n a
ref a -> STMAction n
c   -> forall {n :: * -> *} {m :: * -> *} {t} {a} {a}.
(Ref n ~ Ref m, MonadDejaFu m) =>
ModelTVar n t
-> (t -> a) -> m (a, n (), n (), IdSource, [TVarId], [a], TAction)
stepRead ModelTVar n a
ref a -> STMAction n
c
  SWrite  ModelTVar n a
ref a
a STMAction n
c -> forall {n :: * -> *} {m :: * -> *} {m :: * -> *} {m :: * -> *} {a}
       {a} {a}.
(Ref n ~ Ref m, Ref n ~ Ref m, Ref n ~ Ref m, MonadDejaFu m,
 MonadDejaFu m, MonadDejaFu m) =>
ModelTVar n a
-> a -> a -> m (a, m (), m (), IdSource, [a], [TVarId], TAction)
stepWrite ModelTVar n a
ref a
a STMAction n
c
  SNew    String
n a
a ModelTVar n a -> STMAction n
c   -> forall {n :: * -> *} {m :: * -> *} {m :: * -> *} {a} {a} {a}.
(Ref n ~ Ref m, Ref m ~ Ref n, MonadDejaFu m, MonadDejaFu m) =>
String
-> a
-> (ModelTVar n a -> a)
-> m (a, m (), n (), IdSource, [a], [TVarId], TAction)
stepNew String
n a
a ModelTVar n a -> STMAction n
c
  SOrElse ModelSTM n a
a ModelSTM n a
b a -> STMAction n
c   -> forall {t} {n :: * -> *}.
ModelSTM n t
-> ModelSTM n t
-> (t -> STMAction n)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
stepOrElse ModelSTM n a
a ModelSTM n a
b a -> STMAction n
c
  SStop   n ()
na      -> forall {n :: * -> *} {a} {a}.
Monad n =>
n () -> n (STMAction n, n (), n (), IdSource, [a], [a], TAction)
stepStop n ()
na

  SThrow e
e -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (n :: * -> *) e. Exception e => e -> STMAction n
SThrow e
e, n ()
nothing, n ()
nothing, IdSource
idsource, [], [], TAction
TThrow)
  STMAction n
SRetry   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (n :: * -> *). STMAction n
SRetry,   n ()
nothing, n ()
nothing, IdSource
idsource, [], [], TAction
TRetry)

  where
    nothing :: n ()
nothing = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

    stepCatch :: (t -> ModelSTM n t)
-> ModelSTM n t
-> (t -> STMAction n)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
stepCatch t -> ModelSTM n t
h ModelSTM n t
stm t -> STMAction n
c = forall {m :: * -> *} {a} {g} {t} {a}.
MonadDejaFu m =>
([TAction] -> Maybe a -> g)
-> ModelSTM m t
-> (t -> a)
-> ([TAction]
    -> m (a, m (), m (), IdSource, [TVarId], [TVarId], g))
-> ([TAction]
    -> SomeException
    -> m (a, m (), m (), IdSource, [TVarId], [TVarId], g))
-> m (a, m (), m (), IdSource, [TVarId], [TVarId], g)
cases [TAction] -> Maybe [TAction] -> TAction
TCatch ModelSTM n t
stm t -> STMAction n
c
      (\[TAction]
trace -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (n :: * -> *). STMAction n
SRetry, n ()
nothing, n ()
nothing, IdSource
idsource, [], [], [TAction] -> Maybe [TAction] -> TAction
TCatch [TAction]
trace forall a. Maybe a
Nothing))
      (\[TAction]
trace SomeException
exc    -> case forall e. Exception e => SomeException -> Maybe e
fromException SomeException
exc of
        Just t
exc' -> forall {g} {t} {n :: * -> *}.
([TAction] -> g)
-> ModelSTM n t
-> (t -> STMAction n)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], g)
transaction ([TAction] -> Maybe [TAction] -> TAction
TCatch [TAction]
trace forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) (t -> ModelSTM n t
h t
exc') t -> STMAction n
c
        Maybe t
Nothing   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (n :: * -> *) e. Exception e => e -> STMAction n
SThrow SomeException
exc, n ()
nothing, n ()
nothing, IdSource
idsource, [], [], [TAction] -> Maybe [TAction] -> TAction
TCatch [TAction]
trace forall a. Maybe a
Nothing))

    stepRead :: ModelTVar n t
-> (t -> a) -> m (a, n (), n (), IdSource, [TVarId], [a], TAction)
stepRead ModelTVar{TVarId
Ref n t
tvarRef :: Ref n t
tvarId :: TVarId
tvarRef :: forall (n :: * -> *) a. ModelTVar n a -> Ref n a
tvarId :: forall (n :: * -> *) a. ModelTVar n a -> TVarId
..} t -> a
c = do
      t
val <- forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n t
tvarRef
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> a
c t
val, n ()
nothing, n ()
nothing, IdSource
idsource, [TVarId
tvarId], [], TVarId -> TAction
TRead TVarId
tvarId)

    stepWrite :: ModelTVar n a
-> a -> a -> m (a, m (), m (), IdSource, [a], [TVarId], TAction)
stepWrite ModelTVar{TVarId
Ref n a
tvarRef :: Ref n a
tvarId :: TVarId
tvarRef :: forall (n :: * -> *) a. ModelTVar n a -> Ref n a
tvarId :: forall (n :: * -> *) a. ModelTVar n a -> TVarId
..} a
a a
c = do
      a
old <- forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n a
tvarRef
      forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n a
tvarRef a
a
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
c, forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n a
tvarRef a
a, forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n a
tvarRef a
old, IdSource
idsource, [], [TVarId
tvarId], TVarId -> TAction
TWrite TVarId
tvarId)

    stepNew :: String
-> a
-> (ModelTVar n a -> a)
-> m (a, m (), n (), IdSource, [a], [TVarId], TAction)
stepNew String
n a
a ModelTVar n a -> a
c = do
      let (IdSource
idsource', TVarId
tvid) = String -> IdSource -> (IdSource, TVarId)
nextTVId String
n IdSource
idsource
      Ref n a
ref <- forall (m :: * -> *) a. MonadDejaFu m => a -> m (Ref m a)
newRef a
a
      let tvar :: ModelTVar n a
tvar = forall (n :: * -> *) a. TVarId -> Ref n a -> ModelTVar n a
ModelTVar TVarId
tvid Ref n a
ref
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (ModelTVar n a -> a
c ModelTVar n a
tvar, forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n a
ref a
a, n ()
nothing, IdSource
idsource', [], [TVarId
tvid], TVarId -> TAction
TNew TVarId
tvid)

    stepOrElse :: ModelSTM n t
-> ModelSTM n t
-> (t -> STMAction n)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
stepOrElse ModelSTM n t
a ModelSTM n t
b t -> STMAction n
c = forall {m :: * -> *} {a} {g} {t} {a}.
MonadDejaFu m =>
([TAction] -> Maybe a -> g)
-> ModelSTM m t
-> (t -> a)
-> ([TAction]
    -> m (a, m (), m (), IdSource, [TVarId], [TVarId], g))
-> ([TAction]
    -> SomeException
    -> m (a, m (), m (), IdSource, [TVarId], [TVarId], g))
-> m (a, m (), m (), IdSource, [TVarId], [TVarId], g)
cases [TAction] -> Maybe [TAction] -> TAction
TOrElse ModelSTM n t
a t -> STMAction n
c
      (\[TAction]
trace   -> forall {g} {t} {n :: * -> *}.
([TAction] -> g)
-> ModelSTM n t
-> (t -> STMAction n)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], g)
transaction ([TAction] -> Maybe [TAction] -> TAction
TOrElse [TAction]
trace forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) ModelSTM n t
b t -> STMAction n
c)
      (\[TAction]
trace SomeException
exc -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (n :: * -> *) e. Exception e => e -> STMAction n
SThrow SomeException
exc, n ()
nothing, n ()
nothing, IdSource
idsource, [], [], [TAction] -> Maybe [TAction] -> TAction
TOrElse [TAction]
trace forall a. Maybe a
Nothing))

    stepStop :: n () -> n (STMAction n, n (), n (), IdSource, [a], [a], TAction)
stepStop n ()
na = do
      n ()
na
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (n :: * -> *). n () -> STMAction n
SStop n ()
na, n ()
nothing, n ()
nothing, IdSource
idsource, [], [], TAction
TStop)

    cases :: ([TAction] -> Maybe a -> g)
-> ModelSTM m t
-> (t -> a)
-> ([TAction]
    -> m (a, m (), m (), IdSource, [TVarId], [TVarId], g))
-> ([TAction]
    -> SomeException
    -> m (a, m (), m (), IdSource, [TVarId], [TVarId], g))
-> m (a, m (), m (), IdSource, [TVarId], [TVarId], g)
cases [TAction] -> Maybe a -> g
tact ModelSTM m t
stm t -> a
onSuccess [TAction] -> m (a, m (), m (), IdSource, [TVarId], [TVarId], g)
onRetry [TAction]
-> SomeException
-> m (a, m (), m (), IdSource, [TVarId], [TVarId], g)
onException = do
      (Result t
res, m ()
effect, m ()
undo, IdSource
idsource', [TAction]
trace) <- forall (n :: * -> *) a.
MonadDejaFu n =>
ModelSTM n a
-> IdSource -> n (Result a, n (), n (), IdSource, [TAction])
doTransaction ModelSTM m t
stm IdSource
idsource
      case Result t
res of
        Success [TVarId]
readen [TVarId]
written t
val -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (t -> a
onSuccess t
val, m ()
effect, m ()
undo, IdSource
idsource', [TVarId]
readen, [TVarId]
written, [TAction] -> Maybe a -> g
tact [TAction]
trace forall a. Maybe a
Nothing)
        Retry [TVarId]
readen -> do
          (a
res', m ()
effect', m ()
undo', IdSource
idsource'', [TVarId]
readen', [TVarId]
written', g
trace') <- [TAction] -> m (a, m (), m (), IdSource, [TVarId], [TVarId], g)
onRetry [TAction]
trace
          forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
res', m ()
effect', m ()
undo', IdSource
idsource'', [TVarId]
readen forall a. [a] -> [a] -> [a]
++ [TVarId]
readen', [TVarId]
written', g
trace')
        Exception SomeException
exc -> [TAction]
-> SomeException
-> m (a, m (), m (), IdSource, [TVarId], [TVarId], g)
onException [TAction]
trace SomeException
exc

    transaction :: ([TAction] -> g)
-> ModelSTM n t
-> (t -> STMAction n)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], g)
transaction [TAction] -> g
tact ModelSTM n t
stm t -> STMAction n
onSuccess = forall {m :: * -> *} {a} {g} {t} {a}.
MonadDejaFu m =>
([TAction] -> Maybe a -> g)
-> ModelSTM m t
-> (t -> a)
-> ([TAction]
    -> m (a, m (), m (), IdSource, [TVarId], [TVarId], g))
-> ([TAction]
    -> SomeException
    -> m (a, m (), m (), IdSource, [TVarId], [TVarId], g))
-> m (a, m (), m (), IdSource, [TVarId], [TVarId], g)
cases (\[TAction]
t Maybe Any
_ -> [TAction] -> g
tact [TAction]
t) ModelSTM n t
stm t -> STMAction n
onSuccess
      (\[TAction]
trace     -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (n :: * -> *). STMAction n
SRetry, n ()
nothing, n ()
nothing, IdSource
idsource, [], [], [TAction] -> g
tact [TAction]
trace))
      (\[TAction]
trace SomeException
exc -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (n :: * -> *) e. Exception e => e -> STMAction n
SThrow SomeException
exc, n ()
nothing, n ()
nothing, IdSource
idsource, [], [], [TAction] -> g
tact [TAction]
trace))