remove the monad from the postcondition and get rid of extra callbacks

Author: MaximilianAlgehed

quickcheck-dynamic/src/Test/QuickCheck/ParallelActions.hs

@@ -12,20 +12,13 @@ import Test.QuickCheck.Monadic
 import Test.QuickCheck.StateModel.Variables
 import Test.QuickCheck.StateModel
 import Control.Concurrent
-import Control.Monad.Identity
 import Control.Arrow (first)
 import Data.Tree
 
-
 class RunModel state m => RunModelPar state m where
   performPar :: Typeable a => Action state a -> LookUp -> m (PerformResult state m a)
   performPar = perform (error "Trying to evaluate state in default implementation of performPar")
 
-  postconditionPar :: (state, state) -> Action state a -> LookUp -> a -> PostconditionM Identity Bool
-
-  postconditionOnFailurePar :: (state, state) -> Action state a -> LookUp -> Either (Error state m) a -> PostconditionM Identity Bool
-  postconditionOnFailurePar _ _ _ _ = pure True
-
   monitoringPar :: Action state a -> LookUp -> Either (Error state m) a -> Property -> Property
   monitoringPar _ _ _ = id
 
@@ -188,13 +181,13 @@ checkTrace s env (Node (TraceStep r v (ActionWithPolarity a _)) trs) =
       s' = computeNextState s act v
       env' | Right val <- r = (v :== val) : env
            | otherwise      = env
-      checkPost | Right val <- r, polarity act == PosPolarity = fst . runWriter . runPost $ postconditionPar @state @m
+      checkPost | Right val <- r, polarity act == PosPolarity = fst . runWriter . runPost $ postcondition @state @m
                                                                 (underlyingState s, underlyingState s')
                                                                 (polarAction act)
                                                                 (lookUpVar env')
                                                                 val
                 | Left{} <- r, polarity act == PosPolarity = False
-                | otherwise = fst . runWriter . runPost $ postconditionOnFailurePar @state @m
+                | otherwise = fst . runWriter . runPost $ postconditionOnFailure @state @m
                                       (underlyingState s, underlyingState s')
                                       (polarAction act)
                                       (lookUpVar env')

quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs

@@ -53,7 +53,6 @@ module Test.QuickCheck.StateModel (
 ) where
 
 import Control.Monad
-import Control.Monad.Reader
 import Control.Monad.Writer
 import Data.Data
 import Data.Kind
@@ -165,27 +164,24 @@ class
 
 deriving instance (forall a. Show (Action state a)) => Show (Any (Action state))
 
-newtype PostconditionM m a = PostconditionM {runPost :: WriterT (Endo Property, Endo Property) m a}
+newtype PostconditionM a = PostconditionM {runPost :: Writer (Endo Property, Endo Property) a}
   deriving (Functor, Applicative, Monad)
 
-instance MonadTrans PostconditionM where
-  lift = PostconditionM . lift
-
-evaluatePostCondition :: Monad m => PostconditionM m Bool -> PropertyM m ()
+evaluatePostCondition :: Monad m => PostconditionM Bool -> PropertyM m ()
 evaluatePostCondition post = do
-  (b, (Endo mon, Endo onFail)) <- run . runWriterT . runPost $ post
+  let (b, (Endo mon, Endo onFail)) = runWriter . runPost $ post
   monitor mon
   unless b $ monitor onFail
   assert b
 
 -- | Apply the property transformation to the property after evaluating
 -- the postcondition. Useful for collecting statistics while avoiding
 -- duplication between `monitoring` and `postcondition`.
-monitorPost :: Monad m => (Property -> Property) -> PostconditionM m ()
+monitorPost :: (Property -> Property) -> PostconditionM ()
 monitorPost m = PostconditionM $ tell (Endo m, mempty)
 
 -- | Acts as `Test.QuickCheck.counterexample` if the postcondition fails.
-counterexamplePost :: Monad m => String -> PostconditionM m ()
+counterexamplePost :: String -> PostconditionM ()
 counterexamplePost c = PostconditionM $ tell (mempty, Endo $ counterexample c)
 
 -- | The result required of `perform` depending on the `Error` type.
@@ -230,14 +226,14 @@ class (forall a. Show (Action state a), Show (Error state m), Monad m) => RunMod
   -- | Postcondition on the `a` value produced at some step.
   -- The result is `assert`ed and will make the property fail should it be `False`. This is useful
   -- to check the implementation produces expected values.
-  postcondition :: (state, state) -> Action state a -> LookUp -> a -> PostconditionM m Bool
+  postcondition :: (state, state) -> Action state a -> LookUp -> a -> PostconditionM Bool
   postcondition _ _ _ _ = pure True
 
   -- | Postcondition on the result of running a _negative_ `Action`.
   -- The result is `assert`ed and will make the property fail should it be `False`. This is useful
   -- to check the implementation produces e.g. the expected errors or to check that the SUT hasn't
   -- been updated during the execution of the negative action.
-  postconditionOnFailure :: (state, state) -> Action state a -> LookUp -> Either (Error state m) a -> PostconditionM m Bool
+  postconditionOnFailure :: (state, state) -> Action state a -> LookUp -> Either (Error state m) a -> PostconditionM Bool
   postconditionOnFailure _ _ _ _ = pure True
 
   -- | Allows the user to attach additional information to the `Property` at each step of the process.
@@ -624,7 +620,7 @@ runSteps s env ((v := act) : as) = do
     positiveActionSucceeded ret val = do
       (s', env', stateTransition) <- computeNewState ret
       evaluatePostCondition $
-        postcondition
+        postcondition @state @m
           stateTransition
           action
           (lookUpVar env)
@@ -634,7 +630,7 @@ runSteps s env ((v := act) : as) = do
     negativeActionResult ret = do
       (s', env', stateTransition) <- computeNewState ret
       evaluatePostCondition $
-        postconditionOnFailure
+        postconditionOnFailure @state @m
           stateTransition
           action
           (lookUpVar env)

quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs

@@ -116,9 +116,6 @@ instance RunModelPar Counter (ReaderT (IORef Int) IO) where
     ref <- ask
     lift $ atomicModifyIORef ref (\ c -> (0, c))
 
-  postconditionPar (Counter n, _) Reset _ res = pure $ n == res
-  postconditionPar _ _ _ _ = pure True
-
 prop_counter_par :: ParallelActions Counter -> Property
 prop_counter_par as = always 10 $ monadicIO $ do
   ref <- lift $ newIORef (0 :: Int)

quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs

@@ -166,18 +166,7 @@ instance GoodMonad m => RunModel (RegState m) (RegM m) where
     counterexample (show res ++ " <- " ++ show act ++ "\n  -- State: " ++ show s')
       . tabulate "Registry size" [show $ Map.size (regs s')]
 
-instance GoodMonad m => RunModelPar (RegState m) (RegM m) where
-  postconditionPar (s, _) (WhereIs name) env mtid =
-    return $ (env <$> Map.lookup name (regs s)) == mtid
-  postconditionPar _ _ _ _ = return True
-
-  postconditionOnFailurePar (s, _) act@Register{} _ res = do
-    monitorPost $
-      tabulate
-        "Reason for -Register"
-        [why s act]
-    pure $ isLeft res
-  postconditionOnFailurePar _ _ _ _ = pure True
+instance GoodMonad m => RunModelPar (RegState m) (RegM m)
 
 data ShowDict a where
   ShowDict :: Show a => ShowDict a