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

Agda.Utils.TestHelpers

Description

Some functions and generators suitable for writing QuickCheck properties.

Synopsis

# Algebraic properties

associative :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool Source #

Is the operator associative?

commutative :: Eq a => (a -> a -> a) -> a -> a -> Bool Source #

Is the operator commutative?

idempotent :: Eq a => (a -> a -> a) -> a -> Bool Source #

Is the operator idempotent?

isZero :: Eq a => a -> (a -> a -> a) -> a -> Bool Source #

Is the element a zero for the operator?

identity :: Eq a => a -> (a -> a -> a) -> a -> Bool Source #

Is the element a unit for the operator?

leftDistributive :: Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool Source #

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

rightDistributive :: Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool Source #

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

distributive :: Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool Source #

Does the first operator distribute over the second one?

# Generators

natural :: Integral i => Gen i Source #

Generates natural numbers.

positive :: Integral i => Gen i Source #

Generates positive numbers.

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

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 Source #

Coarbitrary "generator" for Maybe.

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

Generates a list of elements picked from a given list.

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

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) Source #

Generates two elements.

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

Generates three elements.

# Test driver.

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.