1
-- | Some functions and generators suitable for writing QuickCheck
4
module Agda.Utils.TestHelpers
5
( -- * Algebraic properties
23
import Agda.Utils.QuickCheck
25
import qualified System.IO.UTF8 as UTF8
27
------------------------------------------------------------------------
28
-- Algebraic properties
30
-- | Is the operator associative?
32
associative :: (Arbitrary a, Eq a, Show a)
34
-> a -> a -> a -> Bool
35
associative (+) = \x y z ->
36
x + (y + z) == (x + y) + z
38
-- | Is the operator commutative?
40
commutative :: (Arbitrary a, Eq a, Show a)
43
commutative (+) = \x y ->
46
-- | Is the element a zero for the operator?
48
isZero :: (Arbitrary a, Eq a, Show a)
51
isZero zer (*) = \x ->
56
-- | Is the element a unit for the operator?
58
identity :: (Arbitrary a, Eq a, Show a)
61
identity one (*) = \x ->
66
-- | Does the first operator distribute (from the left) over the
70
:: (Arbitrary a, Eq a, Show a)
71
=> (a -> a -> a) -> (a -> a -> a)
72
-> a -> a -> a -> Bool
73
leftDistributive (*) (+) = \x y z ->
74
x * (y + z) == (x * y) + (x * z)
76
-- | Does the first operator distribute (from the right) over the
80
:: (Arbitrary a, Eq a, Show a)
81
=> (a -> a -> a) -> (a -> a -> a)
82
-> a -> a -> a -> Bool
83
rightDistributive (*) (+) = \x y z ->
84
(x + y) * z == (x * z) + (y * z)
86
------------------------------------------------------------------------
89
-- | Generates natural numbers.
91
natural :: (Integral i) => Gen i
92
natural = fmap (fromInteger . abs) arbitrary
94
-- | Generates positive numbers.
96
positive :: (Integral i) => Gen i
97
positive = fmap ((+ 1) . abs . fromInteger) arbitrary
99
-- | Generates a list of elements picked from a given list.
100
listOfElements :: [a] -> Gen [a]
101
listOfElements [] = return []
102
listOfElements xs = listOf $ elements xs
104
-- | Generates values of 'Maybe' type, using the given generator to
105
-- generate the contents of the 'Just' constructor.
107
maybeGen :: Gen a -> Gen (Maybe a)
108
maybeGen gen = frequency [ (1, return Nothing)
112
-- | 'Coarbitrary' \"generator\" for 'Maybe'.
114
maybeCoGen :: (a -> Gen b -> Gen b) -> (Maybe a -> Gen b -> Gen b)
115
maybeCoGen f Nothing = variant 0
116
maybeCoGen f (Just x) = variant 1 . f x
118
------------------------------------------------------------------------
121
-- | Runs the tests, and returns 'True' if all tests were successful.
123
runTests :: String -- ^ A label for the tests. Used for
124
-- informational purposes.
127
runTests name tests = do
129
fmap and $ sequence tests
added
removed
src/full/Agda/Utils/TestHelpers.hs
