-- | Some functions and generators suitable for writing QuickCheck -- properties. module Agda.Utils.TestHelpers ( -- * Algebraic properties associative , commutative , isZero , identity , leftDistributive , rightDistributive -- * Generators , natural , positive , maybeGen , maybeCoGen , listOfElements -- * Test driver. , runTests ) where import Agda.Utils.QuickCheck import Data.List import qualified Agda.Utils.IO.Locale as LocIO ------------------------------------------------------------------------ -- Algebraic properties -- | Is the operator associative? associative :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> a -> a -> a -> Bool associative (+) = \x y z -> x + (y + z) == (x + y) + z -- | Is the operator commutative? commutative :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> a -> a -> Bool commutative (+) = \x y -> x + y == y + x -- | Is the element a zero for the operator? isZero :: (Arbitrary a, Eq a, Show 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 :: (Arbitrary a, Eq a, Show 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 :: (Arbitrary a, Eq a, Show 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 :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool rightDistributive (*) (+) = \x y z -> (x + y) * z == (x * z) + (y * z) ------------------------------------------------------------------------ -- Generators -- | Generates natural numbers. natural :: (Integral i) => Gen i natural = fmap (fromInteger . abs) arbitrary -- | Generates positive numbers. positive :: (Integral i) => Gen i positive = fmap ((+ 1) . abs . fromInteger) arbitrary -- | Generates a list of elements picked from a given list. listOfElements :: [a] -> Gen [a] listOfElements [] = return [] listOfElements xs = listOf $ 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, fmap 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 ------------------------------------------------------------------------ -- 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 LocIO.putStrLn name fmap and $ sequence tests