Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Utils.TestHelpers

Contents

- Algebraic properties
- Generators
- Test driver.

Description

Some functions and generators suitable for writing QuickCheck properties.

Synopsis

- associative :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> a -> a -> a -> Bool
- commutative :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> a -> a -> Bool
- isZero :: (Arbitrary a, Eq a, Show a) => a -> (a -> a -> a) -> a -> Bool
- identity :: (Arbitrary a, Eq a, Show a) => a -> (a -> a -> a) -> a -> Bool
- leftDistributive :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool
- rightDistributive :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool
- natural :: Integral i => Gen i
- positive :: Integral i => Gen i
- maybeGen :: Gen a -> Gen (Maybe a)
- maybeCoGen :: (a -> Gen b -> Gen b) -> Maybe a -> Gen b -> Gen b
- listOfElements :: [a] -> Gen [a]
- elementsUnlessEmpty :: Arbitrary a => [a] -> Gen a
- two :: Gen a -> Gen (a, a)
- three :: Gen a -> Gen (a, a, a)
- runTests :: String -> [IO Bool] -> IO Bool

# Algebraic properties

associative :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> a -> a -> a -> Bool

Is the operator associative?

commutative :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> a -> a -> Bool

Is the operator commutative?

isZero :: (Arbitrary a, Eq a, Show a) => a -> (a -> a -> a) -> a -> Bool

Is the element a zero for the operator?

identity :: (Arbitrary a, Eq a, Show a) => a -> (a -> a -> a) -> a -> Bool

Is the element a unit for the operator?

leftDistributive :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool

Does the first operator distribute (from the left) over the second one?

rightDistributive :: (Arbitrary a, Eq a, Show a) => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool

Does the first operator distribute (from the right) over the second one?

# Generators

natural :: Integral i => Gen i

Generates natural numbers.

positive :: Integral i => Gen i

Generates positive numbers.

maybeGen :: Gen a -> Gen (Maybe a)

Generates values of `Maybe` type, using the given generator to generate the contents of the `Just` constructor.

maybeCoGen :: (a -> Gen b -> Gen b) -> Maybe a -> Gen b -> Gen b

`Coarbitrary` "generator" for `Maybe`.

listOfElements :: [a] -> Gen [a]

Generates a list of elements picked from a given list.

elementsUnlessEmpty :: Arbitrary a => [a] -> Gen a

If the given list is non-empty, then an element from the list is generated, and otherwise an arbitrary element is generated.

two :: Gen a -> Gen (a, a)

Generates two elements.

three :: Gen a -> Gen (a, a, a)

Generates three elements.

# Test driver.

runTests

Arguments

:: String | A label for the tests. Used for informational purposes.
-> [IO Bool] |
-> IO Bool |

Runs the tests, and returns `True` if all tests were successful.