{-# LANGUAGE TypeOperators #-}
module Test.QuickCheck.StateModel.Lockstep.Run (
tagActions
, labelActions
, 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
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
-> Lockstep state
-> Var a
-> Action (Lockstep state) a
-> [Step (Lockstep state)]
-> [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
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
runActionsBracket ::
( 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 :: 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
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
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)