{-# LANGUAGE TypeOperators #-}

-- | 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 (void)
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 = String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
QC.label (String
"Tags: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show (Actions (Lockstep state) -> [String]
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 Set String
forall a. Set a
Set.empty Lockstep state
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 []            = Set String -> [String]
forall a. Set a -> [a]
Set.toList Set String
tags
    go Set String
tags  Lockstep state
st ((Var a
v:=ActionWithPolarity (Lockstep state) a
a) : [Step (Lockstep state)]
ss) = Set String
-> Lockstep state
-> Var a
-> Action (Lockstep state) a
-> [Step (Lockstep state)]
-> [String]
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 (ActionWithPolarity (Lockstep state) a -> Action (Lockstep state) a
forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity (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 (Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.union ([String] -> Set String
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' = state -> EnvF (ModelValue state) -> Lockstep state
forall state. state -> EnvF (ModelValue state) -> Lockstep state
Lockstep state
after (Var a
-> ModelValue state a
-> EnvF (ModelValue state)
-> EnvF (ModelValue state)
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) = Action (Lockstep state) a
-> ModelLookUp state -> state -> (ModelValue state a, state)
forall a.
LockstepAction state a
-> ModelLookUp state -> state -> (ModelValue state a, state)
forall state a.
InLockstep state =>
LockstepAction state a
-> ModelLookUp state -> state -> (ModelValue state a, state)
modelNextState Action (Lockstep state) a
action (EnvF (ModelValue state)
-> GVar (ModelOp state) a -> ModelValue state a
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' = (state, state)
-> Action (Lockstep state) a -> ModelValue state a -> [String]
forall a.
(state, state)
-> LockstepAction state a -> ModelValue state a -> [String]
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
     , e ~ Error (Lockstep state)
     , forall a. IsPerformResult e a
     )
  => Proxy state
  -> Actions (Lockstep state) -> Property
runActions :: forall state e.
(RunLockstep state IO, e ~ Error (Lockstep state),
 forall a. IsPerformResult e a) =>
Proxy state -> Actions (Lockstep state) -> Property
runActions Proxy state
_ Actions (Lockstep state)
actions = PropertyM IO () -> Property
forall a. Testable a => PropertyM IO a -> Property
monadicIO (PropertyM IO () -> Property) -> PropertyM IO () -> Property
forall a b. (a -> b) -> a -> b
$ PropertyM IO (Annotated (Lockstep state), Env IO)
-> PropertyM IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (PropertyM IO (Annotated (Lockstep state), Env IO)
 -> PropertyM IO ())
-> PropertyM IO (Annotated (Lockstep state), Env IO)
-> PropertyM IO ()
forall a b. (a -> b) -> a -> b
$ Actions (Lockstep state)
-> PropertyM IO (Annotated (Lockstep state), Env IO)
forall state (m :: * -> *) e.
(StateModel state, RunModel state m, e ~ Error state,
 forall a. IsPerformResult e a) =>
Actions state -> PropertyM m (Annotated 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
     , e ~ Error (Lockstep state)
     , forall a. IsPerformResult e a
     )
  => Proxy state
  -> IO st         -- ^ Initialisation
  -> (st -> IO ()) -- ^ Cleanup
  -> (m Property -> st -> IO Property) -- ^ Runner
  -> Actions (Lockstep state) -> Property
runActionsBracket :: forall state (m :: * -> *) e st.
(RunLockstep state m, e ~ Error (Lockstep state),
 forall a. IsPerformResult e a) =>
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 =
    IO st
-> (st -> IO ())
-> (m Property -> st -> IO Property)
-> PropertyM m ()
-> Property
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 (PropertyM m () -> Property) -> PropertyM m () -> Property
forall a b. (a -> b) -> a -> b
$
      PropertyM m (Annotated (Lockstep state), Env m) -> PropertyM m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (PropertyM m (Annotated (Lockstep state), Env m) -> PropertyM m ())
-> PropertyM m (Annotated (Lockstep state), Env m)
-> PropertyM m ()
forall a b. (a -> b) -> a -> b
$ Actions (Lockstep state)
-> PropertyM m (Annotated (Lockstep state), Env m)
forall state (m :: * -> *) e.
(StateModel state, RunModel state m, e ~ Error state,
 forall a. IsPerformResult e a) =>
Actions state -> PropertyM m (Annotated 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 =
    IO a -> Property
forall prop. Testable prop => IO prop -> Property
QC.ioProperty (IO a -> Property) -> IO a -> Property
forall a b. (a -> b) -> a -> b
$ ((forall a. IO a -> IO a) -> IO a) -> IO a
forall b. ((forall a. IO a -> IO a) -> IO b) -> IO b
mask (((forall a. IO a -> IO a) -> IO a) -> IO a)
-> ((forall a. IO a -> IO a) -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ \forall a. IO a -> IO a
restore -> do
      st
st <- IO st
init
      a
a <- IO a -> IO a
forall a. IO a -> IO a
restore (m a -> st -> IO a
runner m a
prop st
st) IO a -> IO () -> IO a
forall a b. IO a -> IO b -> IO a
`onException` st -> IO ()
cleanup st
st
      st -> IO ()
cleanup st
st
      a -> IO a
forall a. a -> IO a
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 =
    (m Property -> Property) -> PropertyM m a -> Property
forall a (m :: * -> *).
(Testable a, Monad m) =>
(m Property -> Property) -> PropertyM m a -> Property
monadic (IO st
-> (st -> IO ())
-> (m Property -> st -> IO Property)
-> m Property
-> Property
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)