From ab28a179c8d6696d5a287af9594af67659ccf65a Mon Sep 17 00:00:00 2001 From: Maximilian Algehed Date: Thu, 21 Mar 2024 15:56:29 +0100 Subject: [PATCH] Add `withCounterexample` to get a re-useable handle on counterexamples + add recheck to quickly re-test a property --- src/Test/QuickCheck.hs | 11 +++++++++ src/Test/QuickCheck/Property.hs | 42 +++++++++++++++++++++++++++++++-- src/Test/QuickCheck/Test.hs | 29 +++++++++++++++++++++++ 3 files changed, 80 insertions(+), 2 deletions(-) diff --git a/src/Test/QuickCheck.hs b/src/Test/QuickCheck.hs index 12fb6822..d9fb61ae 100644 --- a/src/Test/QuickCheck.hs +++ b/src/Test/QuickCheck.hs @@ -78,6 +78,11 @@ module Test.QuickCheck , quickCheckWith , quickCheckWithResult , quickCheckResult +#ifndef NO_TYPEABLE + , quickCheckCounterexample + , quickCheckWithCounterexample +#endif + , recheck , isSuccess -- ** Running tests verbosely , verboseCheck @@ -317,6 +322,12 @@ module Test.QuickCheck , (.||.) , disjoin -- ** What to do on failure +#ifndef NO_TYPEABLE + , Counterexample(..) + , withCounterexample + , coerceCounterexample + , castCounterexample +#endif , counterexample , printTestCase , whenFail diff --git a/src/Test/QuickCheck/Property.hs b/src/Test/QuickCheck/Property.hs index a9fc9e31..21817678 100644 --- a/src/Test/QuickCheck/Property.hs +++ b/src/Test/QuickCheck/Property.hs @@ -3,6 +3,7 @@ {-# LANGUAGE CPP #-} #ifndef NO_TYPEABLE {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE ExistentialQuantification #-} #endif #ifndef NO_SAFE_HASKELL {-# LANGUAGE Safe #-} @@ -33,7 +34,7 @@ import Data.Set(Set) import Control.DeepSeq #endif #ifndef NO_TYPEABLE -import Data.Typeable (Typeable) +import Data.Typeable (Typeable, cast) #endif import Data.Maybe @@ -254,6 +255,32 @@ data Callback data CallbackKind = Counterexample -- ^ Affected by the 'verbose' combinator | NotCounterexample -- ^ Not affected by the 'verbose' combinator +#ifndef NO_TYPEABLE +data Counterexample = forall a. (Typeable a, Show a) => Cex a + +instance Show Counterexample where + show (Cex a) = show a + +coerceCounterexample :: Typeable a => Counterexample -> a +coerceCounterexample (Cex a) = case cast a of + Nothing -> error $ "Can't coerceCounterexample " ++ show a + Just a -> a + +castCounterexample :: Typeable a => Counterexample -> Maybe a +castCounterexample (Cex a) = cast a + +data Counterexamples = NoCounterexamples + | forall a. (Typeable a, Show a) => a :! Counterexamples + +toCounterexamples :: [Counterexample] -> Counterexamples +toCounterexamples [] = NoCounterexamples +toCounterexamples (Cex a : ces) = a :! toCounterexamples ces + +#define COUNTEREXAMPLES(a) , theCounterexamples a +#else +#define COUNTEREXAMPLES(a) +#endif + -- | The result of a single test. data Result = MkResult @@ -289,6 +316,7 @@ data Result -- ^ the callbacks for this test case , testCase :: [String] -- ^ the generated test case + COUNTEREXAMPLES(:: [Counterexample]) } exception :: String -> AnException -> Result @@ -329,6 +357,7 @@ succeeded, failed, rejected :: Result , requiredCoverage = [] , callbacks = [] , testCase = [] + COUNTEREXAMPLES(= []) } -------------------------------------------------------------------------- @@ -502,6 +531,13 @@ withMaxShrinks n = n `seq` mapTotalResult (\res -> res{ maybeMaxShrinks = Just n withMaxSize :: Testable prop => Int -> prop -> Property withMaxSize n = n `seq` mapTotalResult (\res -> res{ maybeMaxTestSize = Just n }) +#ifndef NO_TYPEABLE +-- | Return a value in the 'counterexamples' field of the 'Result' returned by 'quickCheckResult'. Counterexamples +-- are returned outer-most first. +withCounterexample :: (Typeable a, Show a, Testable prop) => a -> prop -> Property +withCounterexample a = a `seq` mapTotalResult (\res -> res{ theCounterexamples = Cex a : theCounterexamples res }) +#endif + -- | Check that all coverage requirements defined by 'cover' and 'coverTable' -- are met, using a statistically sound test, and fail if they are not met. -- @@ -964,7 +1000,9 @@ disjoin ps = callbacks result2, testCase = testCase result1 ++ - testCase result2 } + testCase result2 + COUNTEREXAMPLES(= theCounterexamples result1 ++ theCounterexamples result2) + } Nothing -> result2 -- The "obvious" semantics of .||. has: -- discard .||. true = true diff --git a/src/Test/QuickCheck/Test.hs b/src/Test/QuickCheck/Test.hs index 64000a55..1034eb65 100644 --- a/src/Test/QuickCheck/Test.hs +++ b/src/Test/QuickCheck/Test.hs @@ -144,6 +144,10 @@ data Result -- ^ The test case's labels (see 'label') , failingClasses :: Set String -- ^ The test case's classes (see 'classify') +#ifndef NO_TYPEABLE + , counterexamples :: [Counterexample] + -- ^ The existentially quantified counterexamples provided by 'withCounterexample' +#endif } -- | A property that should have failed did not | NoExpectedFailure @@ -199,6 +203,28 @@ quickCheckWithResult :: Testable prop => Args -> prop -> IO Result quickCheckWithResult a p = withState a (\s -> test s (property p)) +#ifndef NO_TYPEABLE +-- | Test a property and get counterexamples as a result. Can be used like: +-- +-- @ +-- $> x :! _ <- quickCheckCounterexample $ \ x -> withCounterexample (x :: Int) (x > 0) +-- *** Failed! Falsified (after 1 test): +-- 0 +-- $> x +-- 0 +quickCheckCounterexample :: Testable prop => prop -> IO Counterexamples +quickCheckCounterexample = quickCheckWithCounterexample stdArgs + +-- | Test a property, using test arguments, and get counterexamples as a result. +quickCheckWithCounterexample :: Testable prop => Args -> prop -> IO Counterexamples +quickCheckWithCounterexample args p = toCounterexamples . counterexamples <$> quickCheckWithResult args p +#endif + +-- | Re-run a property with the seed and size that failed in a run of 'quickCheckResult'. +recheck :: Testable prop => Result -> prop -> IO () +recheck res@Failure{} = quickCheckWith stdArgs{ replay = Just (usedSeed res, usedSize res)} . once +recheck _ = error "Can only recheck tests that failed with a counterexample." + withState :: Args -> (State -> IO a) -> IO a withState a test = (if chatty a then withStdioTerminal else withNullTerminal) $ \tm -> do rnd <- case replay a of @@ -481,6 +507,9 @@ runATest st prop = , failingTestCase = testCase , failingLabels = P.labels res , failingClasses = Set.fromList (map fst $ filter snd $ P.classes res) +#ifndef NO_TYPEABLE + , counterexamples = theCounterexamples res +#endif } where (rnd1,rnd2) = split (randomSeed st)