-- | Some functions and generators suitable for writing QuickCheck -- properties. module Agda.Utils.TestHelpers ( -- * Algebraic properties associative , commutative , idempotent , isZero , identity , leftDistributive , rightDistributive , distributive -- * Generators , natural , positive , maybeGen , maybeCoGen , listOfElements , elementsUnlessEmpty , two , three -- * Test driver. , runTests ) where import Control.Monad import Data.Functor import Test.QuickCheck ------------------------------------------------------------------------ -- Algebraic properties -- | Is the operator associative? associative :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool associative (+) = \x y z -> x + (y + z) == (x + y) + z -- | Is the operator commutative? commutative :: Eq a => (a -> a -> a) -> a -> a -> Bool commutative (+) = \x y -> x + y == y + x -- | Is the operator idempotent? idempotent :: Eq a => (a -> a -> a) -> a -> Bool idempotent (/\) = \ x -> (x /\ x) == x -- | Is the element a zero for the operator? isZero :: Eq a => a -> (a -> a -> a) -> a -> Bool isZero zer (*) = \x -> (zer * x == zer) && (x * zer == zer) -- | Is the element a unit for the operator? identity :: Eq a => a -> (a -> a -> a) -> a -> Bool identity one (*) = \x -> (one * x == x) && (x * one == x) -- | Does the first operator distribute (from the left) over the -- second one? leftDistributive :: Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool leftDistributive (*) (+) = \x y z -> x * (y + z) == (x * y) + (x * z) -- | Does the first operator distribute (from the right) over the -- second one? rightDistributive :: Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool rightDistributive (*) (+) = \x y z -> (x + y) * z == (x * z) + (y * z) -- | Does the first operator distribute over the second one? distributive :: Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool distributive (*) (+) = \ x y z -> leftDistributive (*) (+) x y z && rightDistributive (*) (+) x y z ------------------------------------------------------------------------ -- Generators -- | Generates natural numbers. natural :: (Integral i) => Gen i natural = fromInteger . abs <\$> arbitrary -- | Generates positive numbers. positive :: (Integral i) => Gen i positive = succ <\$> natural -- | Generates a list of elements picked from a given list. listOfElements :: [a] -> Gen [a] listOfElements [] = return [] listOfElements xs = listOf \$ elements xs -- | If the given list is non-empty, then an element from the list is -- generated, and otherwise an arbitrary element is generated. elementsUnlessEmpty :: Arbitrary a => [a] -> Gen a elementsUnlessEmpty [] = arbitrary elementsUnlessEmpty xs = elements xs -- | Generates values of 'Maybe' type, using the given generator to -- generate the contents of the 'Just' constructor. maybeGen :: Gen a -> Gen (Maybe a) maybeGen gen = frequency [ (1, return Nothing) , (9, Just <\$> gen) ] -- | 'Coarbitrary' \"generator\" for 'Maybe'. maybeCoGen :: (a -> Gen b -> Gen b) -> (Maybe a -> Gen b -> Gen b) maybeCoGen f Nothing = variant 0 maybeCoGen f (Just x) = variant 1 . f x -- | Generates two elements. two :: Gen a -> Gen (a, a) two gen = liftM2 (,) gen gen -- | Generates three elements. three :: Gen a -> Gen (a, a, a) three gen = liftM3 (,,) gen gen gen ------------------------------------------------------------------------ -- Test driver -- | Runs the tests, and returns 'True' if all tests were successful. runTests :: String -- ^ A label for the tests. Used for -- informational purposes. -> [IO Bool] -> IO Bool runTests name tests = do putStrLn name and <\$> sequence tests