Skip to content

Commit

Permalink
Add withCounterexample to get a re-useable handle on counterexamples +
Browse files Browse the repository at this point in the history
add recheck to quickly re-test a property
  • Loading branch information
MaximilianAlgehed committed Apr 18, 2024
1 parent 5111763 commit ab28a17
Show file tree
Hide file tree
Showing 3 changed files with 80 additions and 2 deletions.
11 changes: 11 additions & 0 deletions src/Test/QuickCheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -78,6 +78,11 @@ module Test.QuickCheck
, quickCheckWith
, quickCheckWithResult
, quickCheckResult
#ifndef NO_TYPEABLE
, quickCheckCounterexample
, quickCheckWithCounterexample
#endif
, recheck
, isSuccess
-- ** Running tests verbosely
, verboseCheck
Expand Down Expand Up @@ -317,6 +322,12 @@ module Test.QuickCheck
, (.||.)
, disjoin
-- ** What to do on failure
#ifndef NO_TYPEABLE
, Counterexample(..)
, withCounterexample
, coerceCounterexample
, castCounterexample
#endif
, counterexample
, printTestCase
, whenFail
Expand Down
42 changes: 40 additions & 2 deletions src/Test/QuickCheck/Property.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
{-# LANGUAGE CPP #-}
#ifndef NO_TYPEABLE
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ExistentialQuantification #-}
#endif
#ifndef NO_SAFE_HASKELL
{-# LANGUAGE Safe #-}
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -289,6 +316,7 @@ data Result
-- ^ the callbacks for this test case
, testCase :: [String]
-- ^ the generated test case
COUNTEREXAMPLES(:: [Counterexample])
}

exception :: String -> AnException -> Result
Expand Down Expand Up @@ -329,6 +357,7 @@ succeeded, failed, rejected :: Result
, requiredCoverage = []
, callbacks = []
, testCase = []
COUNTEREXAMPLES(= [])
}

--------------------------------------------------------------------------
Expand Down Expand Up @@ -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.
--
Expand Down Expand Up @@ -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
Expand Down
29 changes: 29 additions & 0 deletions src/Test/QuickCheck/Test.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit ab28a17

Please sign in to comment.