{-# 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 = ((b -> STMAction n) -> STMAction n) -> ModelSTM n b
forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM (((b -> STMAction n) -> STMAction n) -> ModelSTM n b)
-> ((b -> STMAction n) -> STMAction n) -> ModelSTM n b
forall a b. (a -> b) -> a -> b
$ \b -> STMAction n
c -> ModelSTM n a -> (a -> STMAction n) -> STMAction n
forall (n :: * -> *) a.
ModelSTM n a -> (a -> STMAction n) -> STMAction n
runModelSTM ModelSTM n a
m (b -> STMAction n
c (b -> STMAction n) -> (a -> b) -> a -> STMAction n
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  = ((a -> STMAction n) -> STMAction n) -> ModelSTM n a
forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM (((a -> STMAction n) -> STMAction n) -> ModelSTM n a)
-> ((a -> STMAction n) -> STMAction n) -> ModelSTM n a
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 = ((b -> STMAction n) -> STMAction n) -> ModelSTM n b
forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM (((b -> STMAction n) -> STMAction n) -> ModelSTM n b)
-> ((b -> STMAction n) -> STMAction n) -> ModelSTM n b
forall a b. (a -> b) -> a -> b
$ \b -> STMAction n
c -> ModelSTM n (a -> b) -> ((a -> b) -> STMAction n) -> STMAction n
forall (n :: * -> *) a.
ModelSTM n a -> (a -> STMAction n) -> STMAction n
runModelSTM ModelSTM n (a -> b)
f (\a -> b
g -> ModelSTM n a -> (a -> STMAction n) -> STMAction n
forall (n :: * -> *) a.
ModelSTM n a -> (a -> STMAction n) -> STMAction n
runModelSTM ModelSTM n a
v (b -> STMAction n
c (b -> STMAction n) -> (a -> b) -> a -> STMAction n
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  = a -> ModelSTM n a
forall a. a -> ModelSTM n a
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 = ((b -> STMAction n) -> STMAction n) -> ModelSTM n b
forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM (((b -> STMAction n) -> STMAction n) -> ModelSTM n b)
-> ((b -> STMAction n) -> STMAction n) -> ModelSTM n b
forall a b. (a -> b) -> a -> b
$ \b -> STMAction n
c -> ModelSTM n a -> (a -> STMAction n) -> STMAction n
forall (n :: * -> *) a.
ModelSTM n a -> (a -> STMAction n) -> STMAction n
runModelSTM ModelSTM n a
m (\a
x -> ModelSTM n b -> (b -> STMAction n) -> STMAction n
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 = ((a -> STMAction n) -> STMAction n) -> ModelSTM n a
forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM (((a -> STMAction n) -> STMAction n) -> ModelSTM n a)
-> ((a -> STMAction n) -> STMAction n) -> ModelSTM n a
forall a b. (a -> b) -> a -> b
$ \a -> STMAction n
_ -> MonadFailException -> 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. (HasCallStack, Exception e) => e -> ModelSTM n a
throwM e
e = ((a -> STMAction n) -> STMAction n) -> ModelSTM n a
forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM (((a -> STMAction n) -> STMAction n) -> ModelSTM n a)
-> ((a -> STMAction n) -> STMAction n) -> ModelSTM n a
forall a b. (a -> b) -> a -> b
$ \a -> STMAction n
_ -> e -> STMAction n
forall (n :: * -> *) e. Exception e => e -> STMAction n
SThrow e
e

instance MonadCatch (ModelSTM n) where
  catch :: forall e a.
(HasCallStack, Exception e) =>
ModelSTM n a -> (e -> ModelSTM n a) -> ModelSTM n a
catch ModelSTM n a
stm e -> ModelSTM n a
handler = ((a -> STMAction n) -> STMAction n) -> ModelSTM n a
forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM (((a -> STMAction n) -> STMAction n) -> ModelSTM n a)
-> ((a -> STMAction n) -> STMAction n) -> ModelSTM n a
forall a b. (a -> b) -> a -> b
$ (e -> ModelSTM n a)
-> ModelSTM n a -> (a -> STMAction n) -> STMAction n
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 = ((a -> STMAction n) -> STMAction n) -> ModelSTM n a
forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM (((a -> STMAction n) -> STMAction n) -> ModelSTM n a)
-> ((a -> STMAction n) -> STMAction n) -> ModelSTM n a
forall a b. (a -> b) -> a -> b
$ ModelSTM n a -> ModelSTM n a -> (a -> STMAction n) -> STMAction n
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 = ((a -> STMAction n) -> STMAction n) -> ModelSTM n a
forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM (((a -> STMAction n) -> STMAction n) -> ModelSTM n a)
-> ((a -> STMAction n) -> STMAction n) -> ModelSTM n a
forall a b. (a -> b) -> a -> b
$ STMAction n -> (a -> STMAction n) -> STMAction n
forall a b. a -> b -> a
const STMAction n
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 = ((ModelTVar n a -> STMAction n) -> STMAction n)
-> ModelSTM n (ModelTVar n a)
forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM (((ModelTVar n a -> STMAction n) -> STMAction n)
 -> ModelSTM n (ModelTVar n a))
-> (a -> (ModelTVar n a -> STMAction n) -> STMAction n)
-> a
-> ModelSTM n (ModelTVar n a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> a -> (ModelTVar n a -> STMAction n) -> STMAction n
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 = ((a -> STMAction n) -> STMAction n) -> ModelSTM n a
forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM (((a -> STMAction n) -> STMAction n) -> ModelSTM n a)
-> (ModelTVar n a -> (a -> STMAction n) -> STMAction n)
-> ModelTVar n a
-> ModelSTM n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelTVar n a -> (a -> STMAction n) -> STMAction n
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 = ((() -> STMAction n) -> STMAction n) -> ModelSTM n ()
forall (n :: * -> *) a.
((a -> STMAction n) -> STMAction n) -> ModelSTM n a
ModelSTM (((() -> STMAction n) -> STMAction n) -> ModelSTM n ())
-> ((() -> STMAction n) -> STMAction n) -> ModelSTM n ()
forall a b. (a -> b) -> a -> b
$ \() -> STMAction n
c -> ModelTVar n a -> a -> STMAction n -> STMAction n
forall (n :: * -> *) a.
ModelTVar n a -> a -> STMAction n -> STMAction n
SWrite TVar (ModelSTM n) a
ModelTVar 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
[Result a] -> ShowS
Result a -> String
(Int -> Result a -> ShowS)
-> (Result a -> String) -> ([Result a] -> ShowS) -> Show (Result a)
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
$cshowsPrec :: forall a. Show a => Int -> Result a -> ShowS
showsPrec :: Int -> Result a -> ShowS
$cshow :: forall a. Show a => Result a -> String
show :: Result a -> String
$cshowList :: forall a. Show a => [Result a] -> ShowS
showList :: [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) <- ModelSTM n a
-> IdSource -> n (Result a, n (), n (), IdSource, [TAction])
forall (n :: * -> *) a.
MonadDejaFu n =>
ModelSTM n a
-> IdSource -> n (Result a, n (), n (), IdSource, [TAction])
doTransaction ModelSTM n a
ma IdSource
tvid
  (Result a, n (), IdSource, [TAction])
-> n (Result a, n (), IdSource, [TAction])
forall a. a -> n a
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) <- (n () -> STMAction n)
-> (a -> Maybe (Either SomeException a))
-> ((a -> STMAction n) -> STMAction n)
-> n (STMAction n, Ref n (Maybe (Either SomeException a)))
forall (n :: * -> *) x a b.
MonadDejaFu n =>
(n () -> x)
-> (a -> Maybe b) -> ((a -> x) -> x) -> n (x, Ref n (Maybe b))
runRefCont n () -> STMAction n
forall (n :: * -> *). n () -> STMAction n
SStop (Either SomeException a -> Maybe (Either SomeException a)
forall a. a -> Maybe a
Just (Either SomeException a -> Maybe (Either SomeException a))
-> (a -> Either SomeException a)
-> a
-> Maybe (Either SomeException a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either SomeException a
forall a b. b -> Either a b
Right) (ModelSTM n a -> (a -> STMAction n) -> STMAction n
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) <- Ref n (Maybe (Either SomeException a))
-> STMAction n
-> n ()
-> n ()
-> IdSource
-> [TVarId]
-> [TVarId]
-> [TAction]
-> n (IdSource, n (), n (), [TVarId], [TVarId], [TAction])
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 (() -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (() -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) IdSource
idsource [] [] []
  Maybe (Either SomeException a)
res <- Ref n (Maybe (Either SomeException a))
-> n (Maybe (Either SomeException a))
forall a. Ref n a -> n a
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) -> (Result a, n (), n (), IdSource, [TAction])
-> n (Result a, n (), n (), IdSource, [TAction])
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TVarId] -> [TVarId] -> a -> Result a
forall a. [TVarId] -> [TVarId] -> a -> Result a
Success ([TVarId] -> [TVarId]
forall a. Eq a => [a] -> [a]
nub [TVarId]
readen) ([TVarId] -> [TVarId]
forall a. Eq a => [a] -> [a]
nub [TVarId]
written) a
val, n ()
effect, n ()
undo, IdSource
idsource', [TAction] -> [TAction]
forall a. [a] -> [a]
reverse [TAction]
trace)
    Just (Left  SomeException
exc) -> n ()
undo n ()
-> n (Result a, n (), n (), IdSource, [TAction])
-> n (Result a, n (), n (), IdSource, [TAction])
forall a b. n a -> n b -> n b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Result a, n (), n (), IdSource, [TAction])
-> n (Result a, n (), n (), IdSource, [TAction])
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeException -> Result a
forall a. SomeException -> Result a
Exception SomeException
exc,      () -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), () -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), IdSource
idsource, [TAction] -> [TAction]
forall a. [a] -> [a]
reverse [TAction]
trace)
    Maybe (Either SomeException a)
Nothing          -> n ()
undo n ()
-> n (Result a, n (), n (), IdSource, [TAction])
-> n (Result a, n (), n (), IdSource, [TAction])
forall a b. n a -> n b -> n b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Result a, n (), n (), IdSource, [TAction])
-> n (Result a, n (), n (), IdSource, [TAction])
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TVarId] -> Result a
forall a. [TVarId] -> Result a
Retry ([TVarId] -> Result a) -> [TVarId] -> Result a
forall a b. (a -> b) -> a -> b
$ [TVarId] -> [TVarId]
forall a. Eq a => [a] -> [a]
nub [TVarId]
readen, () -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), () -> n ()
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (), IdSource
idsource, [TAction] -> [TAction]
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) <- STMAction m
-> IdSource
-> m (STMAction m, m (), m (), IdSource, [TVarId], [TVarId],
      TAction)
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 m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m ()
effect'
          newUndo :: m b
newUndo = m ()
undo' m () -> m b -> m b
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m b
undo
          newReaden :: [TVarId]
newReaden = [TVarId]
readen' [TVarId] -> [TVarId] -> [TVarId]
forall a. [a] -> [a] -> [a]
++ [TVarId]
readen
          newWritten :: [TVarId]
newWritten = [TVarId]
written' [TVarId] -> [TVarId] -> [TVarId]
forall a. [a] -> [a] -> [a]
++ [TVarId]
written
          newSofar :: [TAction]
newSofar = TAction
tact TAction -> [TAction] -> [TAction]
forall a. a -> [a] -> [a]
: [TAction]
sofar

      case TAction
tact of
        TAction
TStop  -> (IdSource, m (), m b, [TVarId], [TVarId], [TAction])
-> m (IdSource, m (), m b, [TVarId], [TVarId], [TAction])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IdSource
newIDSource, m ()
newEffect, m b
newUndo, [TVarId]
newReaden, [TVarId]
newWritten, TAction
TStopTAction -> [TAction] -> [TAction]
forall a. a -> [a] -> [a]
:[TAction]
newSofar)
        TAction
TRetry -> do
          Ref m (Maybe (Either SomeException b))
-> Maybe (Either SomeException b) -> m ()
forall a. Ref m a -> a -> m ()
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref m (Maybe (Either SomeException b))
ref Maybe (Either SomeException b)
forall a. Maybe a
Nothing
          (IdSource, m (), m b, [TVarId], [TVarId], [TAction])
-> m (IdSource, m (), m b, [TVarId], [TVarId], [TAction])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IdSource
newIDSource, m ()
newEffect, m b
newUndo, [TVarId]
newReaden, [TVarId]
newWritten, TAction
TRetryTAction -> [TAction] -> [TAction]
forall a. a -> [a] -> [a]
:[TAction]
newSofar)
        TAction
TThrow -> do
          Ref m (Maybe (Either SomeException b))
-> Maybe (Either SomeException b) -> m ()
forall a. Ref m a -> a -> m ()
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref m (Maybe (Either SomeException b))
ref (Either SomeException b -> Maybe (Either SomeException b)
forall a. a -> Maybe a
Just (Either SomeException b -> Maybe (Either SomeException b))
-> (SomeException -> Either SomeException b)
-> SomeException
-> Maybe (Either SomeException b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeException -> Either SomeException b
forall a b. a -> Either a b
Left (SomeException -> Maybe (Either SomeException b))
-> SomeException -> Maybe (Either SomeException b)
forall a b. (a -> b) -> a -> b
$ case STMAction m
act of SThrow e
e -> e -> SomeException
forall e. Exception e => e -> SomeException
toException e
e; STMAction m
_ -> SomeException
forall a. HasCallStack => a
undefined)
          (IdSource, m (), m b, [TVarId], [TVarId], [TAction])
-> m (IdSource, m (), m b, [TVarId], [TVarId], [TAction])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IdSource
newIDSource, m ()
newEffect, m b
newUndo, [TVarId]
newReaden, [TVarId]
newWritten, TAction
TThrowTAction -> [TAction] -> [TAction]
forall 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 -> (e -> ModelSTM n a)
-> ModelSTM n a
-> (a -> STMAction n)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
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   -> ModelTVar n a
-> (a -> STMAction n)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
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 -> ModelTVar n a
-> a
-> STMAction n
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
forall {m :: * -> *} {m :: * -> *} {m :: * -> *} {n :: * -> *} {a}
       {a} {a}.
(Ref m ~ Ref m, Ref m ~ 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   -> String
-> a
-> (ModelTVar n a -> STMAction n)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
forall {n :: * -> *} {m :: * -> *} {m :: * -> *} {a} {a} {a}.
(Ref n ~ Ref m, Ref m ~ Ref m, 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   -> ModelSTM n a
-> ModelSTM n a
-> (a -> STMAction n)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
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      -> n ()
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
forall {n :: * -> *} {a} {a}.
Monad n =>
n () -> n (STMAction n, n (), n (), IdSource, [a], [a], TAction)
stepStop n ()
na

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

  where
    nothing :: n ()
nothing = () -> n ()
forall a. a -> n a
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 = ([TAction] -> Maybe [TAction] -> TAction)
-> ModelSTM n t
-> (t -> STMAction n)
-> ([TAction]
    -> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
          TAction))
-> ([TAction]
    -> SomeException
    -> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
          TAction))
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
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 -> (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], TAction)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (STMAction n
forall (n :: * -> *). STMAction n
SRetry, n ()
nothing, n ()
nothing, IdSource
idsource, [], [], [TAction] -> Maybe [TAction] -> TAction
TCatch [TAction]
trace Maybe [TAction]
forall a. Maybe a
Nothing))
      (\[TAction]
trace SomeException
exc    -> case SomeException -> Maybe t
forall e. Exception e => SomeException -> Maybe e
fromException SomeException
exc of
        Just t
exc' -> ([TAction] -> TAction)
-> ModelSTM n t
-> (t -> STMAction n)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
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 (Maybe [TAction] -> TAction)
-> ([TAction] -> Maybe [TAction]) -> [TAction] -> TAction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TAction] -> Maybe [TAction]
forall a. a -> Maybe a
Just) (t -> ModelSTM n t
h t
exc') t -> STMAction n
c
        Maybe t
Nothing   -> (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], TAction)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeException -> STMAction n
forall (n :: * -> *) e. Exception e => e -> STMAction n
SThrow SomeException
exc, n ()
nothing, n ()
nothing, IdSource
idsource, [], [], [TAction] -> Maybe [TAction] -> TAction
TCatch [TAction]
trace Maybe [TAction]
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
tvarId :: forall (n :: * -> *) a. ModelTVar n a -> TVarId
tvarRef :: forall (n :: * -> *) a. ModelTVar n a -> Ref n a
tvarId :: TVarId
tvarRef :: Ref n t
..} t -> a
c = do
      t
val <- Ref m t -> m t
forall a. Ref m a -> m a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n t
Ref m t
tvarRef
      (a, n (), n (), IdSource, [TVarId], [a], TAction)
-> m (a, n (), n (), IdSource, [TVarId], [a], TAction)
forall a. a -> m a
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
tvarId :: forall (n :: * -> *) a. ModelTVar n a -> TVarId
tvarRef :: forall (n :: * -> *) a. ModelTVar n a -> Ref n a
tvarId :: TVarId
tvarRef :: Ref n a
..} a
a a
c = do
      a
old <- Ref m a -> m a
forall a. Ref m a -> m a
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> m a
readRef Ref n a
Ref m a
tvarRef
      Ref m a -> a -> m ()
forall a. Ref m a -> a -> m ()
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n a
Ref m a
tvarRef a
a
      (a, m (), m (), IdSource, [a], [TVarId], TAction)
-> m (a, m (), m (), IdSource, [a], [TVarId], TAction)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
c, Ref m a -> a -> m ()
forall a. Ref m a -> a -> m ()
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n a
Ref m a
tvarRef a
a, Ref m a -> a -> m ()
forall a. Ref m a -> a -> m ()
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n a
Ref m 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 <- a -> m (Ref m a)
forall a. a -> m (Ref m a)
forall (m :: * -> *) a. MonadDejaFu m => a -> m (Ref m a)
newRef a
a
      let tvar :: ModelTVar n a
tvar = TVarId -> Ref n a -> ModelTVar n a
forall (n :: * -> *) a. TVarId -> Ref n a -> ModelTVar n a
ModelTVar TVarId
tvid Ref n a
ref
      (a, m (), n (), IdSource, [a], [TVarId], TAction)
-> m (a, m (), n (), IdSource, [a], [TVarId], TAction)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ModelTVar n a -> a
c ModelTVar n a
tvar, Ref m a -> a -> m ()
forall a. Ref m a -> a -> m ()
forall (m :: * -> *) a. MonadDejaFu m => Ref m a -> a -> m ()
writeRef Ref n a
Ref m 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 = ([TAction] -> Maybe [TAction] -> TAction)
-> ModelSTM n t
-> (t -> STMAction n)
-> ([TAction]
    -> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
          TAction))
-> ([TAction]
    -> SomeException
    -> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
          TAction))
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
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   -> ([TAction] -> TAction)
-> ModelSTM n t
-> (t -> STMAction n)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
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 (Maybe [TAction] -> TAction)
-> ([TAction] -> Maybe [TAction]) -> [TAction] -> TAction
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TAction] -> Maybe [TAction]
forall a. a -> Maybe a
Just) ModelSTM n t
b t -> STMAction n
c)
      (\[TAction]
trace SomeException
exc -> (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], TAction)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId],
      TAction)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeException -> STMAction n
forall (n :: * -> *) e. Exception e => e -> STMAction n
SThrow SomeException
exc, n ()
nothing, n ()
nothing, IdSource
idsource, [], [], [TAction] -> Maybe [TAction] -> TAction
TOrElse [TAction]
trace Maybe [TAction]
forall a. Maybe a
Nothing))

    stepStop :: n () -> n (STMAction n, n (), n (), IdSource, [a], [a], TAction)
stepStop n ()
na = do
      n ()
na
      (STMAction n, n (), n (), IdSource, [a], [a], TAction)
-> n (STMAction n, n (), n (), IdSource, [a], [a], TAction)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (n () -> STMAction n
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) <- ModelSTM m t
-> IdSource -> m (Result t, m (), m (), IdSource, [TAction])
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 -> (a, m (), m (), IdSource, [TVarId], [TVarId], g)
-> m (a, m (), m (), IdSource, [TVarId], [TVarId], g)
forall a. a -> m a
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 Maybe a
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
          (a, m (), m (), IdSource, [TVarId], [TVarId], g)
-> m (a, m (), m (), IdSource, [TVarId], [TVarId], g)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
res', m ()
effect', m ()
undo', IdSource
idsource'', [TVarId]
readen [TVarId] -> [TVarId] -> [TVarId]
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 = ([TAction] -> Maybe Any -> g)
-> ModelSTM n t
-> (t -> STMAction n)
-> ([TAction]
    -> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], g))
-> ([TAction]
    -> SomeException
    -> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], g))
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], g)
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     -> (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], g)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], g)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (STMAction n
forall (n :: * -> *). STMAction n
SRetry, n ()
nothing, n ()
nothing, IdSource
idsource, [], [], [TAction] -> g
tact [TAction]
trace))
      (\[TAction]
trace SomeException
exc -> (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], g)
-> n (STMAction n, n (), n (), IdSource, [TVarId], [TVarId], g)
forall a. a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeException -> STMAction n
forall (n :: * -> *) e. Exception e => e -> STMAction n
SThrow SomeException
exc, n ()
nothing, n ()
nothing, IdSource
idsource, [], [], [TAction] -> g
tact [TAction]
trace))