module Agda.Utils.TestHelpers
(
associative
, commutative
, isZero
, identity
, leftDistributive
, rightDistributive
, natural
, positive
, maybeGen
, maybeCoGen
, listOfElements
, runTests
)
where
import Agda.Utils.QuickCheck
import Data.List
import qualified Agda.Utils.IO.Locale as LocIO
associative :: (Arbitrary a, Eq a, Show a)
=> (a -> a -> a)
-> a -> a -> a -> Bool
associative (+) = \x y z ->
x + (y + z) == (x + y) + z
commutative :: (Arbitrary a, Eq a, Show a)
=> (a -> a -> a)
-> a -> a -> Bool
commutative (+) = \x y ->
x + y == y + x
isZero :: (Arbitrary a, Eq a, Show a)
=> a -> (a -> a -> a)
-> a -> Bool
isZero zer (*) = \x ->
(zer * x == zer)
&&
(x * zer == zer)
identity :: (Arbitrary a, Eq a, Show a)
=> a -> (a -> a -> a)
-> a -> Bool
identity one (*) = \x ->
(one * x == x)
&&
(x * one == x)
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)
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)
natural :: (Integral i) => Gen i
natural = fmap (fromInteger . abs) arbitrary
positive :: (Integral i) => Gen i
positive = fmap ((+ 1) . abs . fromInteger) arbitrary
listOfElements :: [a] -> Gen [a]
listOfElements [] = return []
listOfElements xs = listOf $ elements xs
maybeGen :: Gen a -> Gen (Maybe a)
maybeGen gen = frequency [ (1, return Nothing)
, (9, fmap Just gen)
]
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
runTests :: String
-> [IO Bool]
-> IO Bool
runTests name tests = do
LocIO.putStrLn name
fmap and $ sequence tests