-- | Run lockstep tests
--
-- Intended for qualified import.
--
-- > import Test.QuickCheck.StateModel.Lockstep.Run qualified as Lockstep
module Test.QuickCheck.StateModel.Lockstep.Run (
    -- * Finding labelled examples
    tagActions
  , labelActions
    -- * Run tests
  , runActions
  , runActionsBracket
  ) where

import Prelude hiding (init)

import Control.Exception
import Control.Monad.Reader
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Typeable
import Test.QuickCheck.Monadic

import Test.QuickCheck (Property, Testable)
import Test.QuickCheck qualified as QC
import Test.QuickCheck.StateModel hiding (runActions)
import Test.QuickCheck.StateModel qualified as StateModel

import Test.QuickCheck.StateModel.Lockstep.API
import Test.QuickCheck.StateModel.Lockstep.EnvF qualified as EnvF
import Test.QuickCheck.StateModel.Lockstep.GVar

{-------------------------------------------------------------------------------
  Finding labelled examples

  Implementation note: the 'monitoring' hook from 'StateModel' cannot be used
  for finding labelled examples. This hook is called many times during test
  execution (once per action); this means that we cannot call 'label' inside
  'monitoring', but must instead use 'tabulate'. However, 'tabulate' is not
  supported by 'labelledExamples'. In 'tagActions' we therefore run over all
  actions, collecting tags as we go, and then do a /single/ call to 'label'
  at the end.
-------------------------------------------------------------------------------}

-- | Tag a list of actions
--
-- This can be used together with QuickCheck's 'labelledExamples' to test your
-- tagging code as well as your shrinker (QuickCheck will try to produce
-- /minimal/ labelled examples).
--
-- Unlike 'runActions', this does not require a 'RunModel' instance; this is
-- executed against the model /only/.
tagActions :: forall state.
     InLockstep state
  => Proxy state -> Actions (Lockstep state) -> Property
tagActions :: forall state.
InLockstep state =>
Proxy state -> Actions (Lockstep state) -> Property
tagActions Proxy state
_p Actions (Lockstep state)
actions = forall prop. Testable prop => String -> prop -> Property
QC.label (String
"Tags: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall state.
InLockstep state =>
Actions (Lockstep state) -> [String]
labelActions Actions (Lockstep state)
actions)) Bool
True

labelActions :: forall state.
     InLockstep state
  => Actions (Lockstep state) -> [String]
labelActions :: forall state.
InLockstep state =>
Actions (Lockstep state) -> [String]
labelActions (Actions [Step (Lockstep state)]
steps) =
    Set String -> Lockstep state -> [Step (Lockstep state)] -> [String]
go forall a. Set a
Set.empty forall state. StateModel state => state
Test.QuickCheck.StateModel.initialState [Step (Lockstep state)]
steps
  where
    go :: Set String -> Lockstep state -> [Step (Lockstep state)] -> [String]
    go :: Set String -> Lockstep state -> [Step (Lockstep state)] -> [String]
go Set String
tags Lockstep state
_st []            = forall a. Set a -> [a]
Set.toList Set String
tags
    go Set String
tags  Lockstep state
st ((Var a
v:=Action (Lockstep state) a
a) : [Step (Lockstep state)]
ss) = forall a.
Typeable a =>
Set String
-> Lockstep state
-> Var a
-> Action (Lockstep state) a
-> [Step (Lockstep state)]
-> [String]
go' Set String
tags Lockstep state
st Var a
v Action (Lockstep state) a
a [Step (Lockstep state)]
ss

    go' :: forall a.
         Typeable a
      => Set String                 -- accumulated set of tags
      -> Lockstep state             -- current state
      -> Var a                      -- variable for the result of this action
      -> Action (Lockstep state) a  -- action to execute
      -> [Step (Lockstep state)]    -- remaining steps to execute
      -> [String]
    go' :: forall a.
Typeable a =>
Set String
-> Lockstep state
-> Var a
-> Action (Lockstep state) a
-> [Step (Lockstep state)]
-> [String]
go' Set String
tags (Lockstep state
before EnvF (ModelValue state)
env) Var a
var Action (Lockstep state) a
action [Step (Lockstep state)]
ss =
        Set String -> Lockstep state -> [Step (Lockstep state)] -> [String]
go (forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall a. Ord a => [a] -> Set a
Set.fromList [String]
tags') Set String
tags) Lockstep state
st' [Step (Lockstep state)]
ss
      where
        st' :: Lockstep state
        st' :: Lockstep state
st' = forall state. state -> EnvF (ModelValue state) -> Lockstep state
Lockstep state
after (forall a (f :: * -> *).
Typeable a =>
Var a -> f a -> EnvF f -> EnvF f
EnvF.insert Var a
var ModelValue state a
modelResp EnvF (ModelValue state)
env)

        modelResp :: ModelValue state a
        after     :: state
        (ModelValue state a
modelResp, state
after) = forall state a.
InLockstep state =>
LockstepAction state a
-> ModelLookUp state -> state -> (ModelValue state a, state)
modelNextState Action (Lockstep state) a
action (forall (f :: * -> *) (op :: * -> * -> *) a.
(Typeable f, InterpretOp op f) =>
EnvF f -> GVar op a -> f a
lookUpEnvF EnvF (ModelValue state)
env) state
before

        tags' :: [String]
        tags' :: [String]
tags' = forall state a.
InLockstep state =>
(state, state)
-> LockstepAction state a -> ModelValue state a -> [String]
tagStep (state
before, state
after) Action (Lockstep state) a
action ModelValue state a
modelResp

{-------------------------------------------------------------------------------
  Run tests
-------------------------------------------------------------------------------}

runActions ::
     RunLockstep state IO
  => Proxy state
  -> Actions (Lockstep state) -> Property
runActions :: forall state.
RunLockstep state IO =>
Proxy state -> Actions (Lockstep state) -> Property
runActions Proxy state
_ Actions (Lockstep state)
actions = forall a. Testable a => PropertyM IO a -> Property
monadicIO forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall state (m :: * -> *).
(StateModel state, RunModel state m) =>
Actions state -> PropertyM m (state, Env m)
StateModel.runActions Actions (Lockstep state)
actions

-- | Convenience runner with support for state initialization
--
-- This is less general than 'Test.QuickCheck.StateModel.runActions', but will
-- be useful in many scenarios.
--
-- For most lockstep-style tests, a suitable monad to run the tests in is
-- @'ReaderT' r 'IO'@. In this case, using @'runReaderT'@ as the runner argument
-- is a reasonable choice.
runActionsBracket ::
     RunLockstep state m
  => Proxy state
  -> IO st         -- ^ Initialisation
  -> (st -> IO ()) -- ^ Cleanup
  -> (m Property -> st -> IO Property) -- ^ Runner
  -> Actions (Lockstep state) -> Property
runActionsBracket :: forall state (m :: * -> *) st.
RunLockstep state m =>
Proxy state
-> IO st
-> (st -> IO ())
-> (m Property -> st -> IO Property)
-> Actions (Lockstep state)
-> Property
runActionsBracket Proxy state
_ IO st
init st -> IO ()
cleanup m Property -> st -> IO Property
runner Actions (Lockstep state)
actions =
    forall st a (m :: * -> *).
(Monad m, Testable a) =>
IO st
-> (st -> IO ())
-> (m Property -> st -> IO Property)
-> PropertyM m a
-> Property
monadicBracketIO IO st
init st -> IO ()
cleanup m Property -> st -> IO Property
runner forall a b. (a -> b) -> a -> b
$
      forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall state (m :: * -> *).
(StateModel state, RunModel state m) =>
Actions state -> PropertyM m (state, Env m)
StateModel.runActions Actions (Lockstep state)
actions

{-------------------------------------------------------------------------------
  Internal auxiliary
-------------------------------------------------------------------------------}

ioPropertyBracket ::
     Testable a
  => IO st
  -> (st -> IO ())
  -> (m a -> st -> IO a)
  -> m a
  -> Property
ioPropertyBracket :: forall a st (m :: * -> *).
Testable a =>
IO st -> (st -> IO ()) -> (m a -> st -> IO a) -> m a -> Property
ioPropertyBracket IO st
init st -> IO ()
cleanup m a -> st -> IO a
runner m a
prop =
    forall prop. Testable prop => IO prop -> Property
QC.ioProperty forall a b. (a -> b) -> a -> b
$ forall b. ((forall a. IO a -> IO a) -> IO b) -> IO b
mask forall a b. (a -> b) -> a -> b
$ \forall a. IO a -> IO a
restore -> do
      st
st <- IO st
init
      a
a <- forall a. IO a -> IO a
restore (m a -> st -> IO a
runner m a
prop st
st) forall a b. IO a -> IO b -> IO a
`onException` st -> IO ()
cleanup st
st
      st -> IO ()
cleanup st
st
      forall (m :: * -> *) a. Monad m => a -> m a
return a
a

-- | Variation on 'monadicIO' that allows for state initialisation/cleanup
monadicBracketIO :: forall st a m.
     (Monad m, Testable a)
  => IO st
  -> (st -> IO ())
  -> (m Property -> st -> IO Property)
  -> PropertyM m a
  -> Property
monadicBracketIO :: forall st a (m :: * -> *).
(Monad m, Testable a) =>
IO st
-> (st -> IO ())
-> (m Property -> st -> IO Property)
-> PropertyM m a
-> Property
monadicBracketIO IO st
init st -> IO ()
cleanup m Property -> st -> IO Property
runner =
    forall a (m :: * -> *).
(Testable a, Monad m) =>
(m Property -> Property) -> PropertyM m a -> Property
monadic (forall a st (m :: * -> *).
Testable a =>
IO st -> (st -> IO ()) -> (m a -> st -> IO a) -> m a -> Property
ioPropertyBracket IO st
init st -> IO ()
cleanup m Property -> st -> IO Property
runner)