Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

LeanCheck is a simple enumerative property-based testing library.

This is the core module of the library, with the most basic definitions. If you are looking just to use the library, import and see Test.LeanCheck.

If you want to understand how the code works, this is the place to start reading.

Other important modules:

- Test.LeanCheck.Basic exports:
Test.LeanCheck.Core,
additional
`tiers`

constructors (`cons6`

...`cons12`

) and`Listable`

tuple instances. - Test.LeanCheck.Tiers exports: functions for advanced Listable definitions.
- Test.LeanCheck exports:
Test.LeanCheck.Basic,
most of Test.LeanCheck.Tiers and
`deriveListable`

.

- holds :: Testable a => Int -> a -> Bool
- fails :: Testable a => Int -> a -> Bool
- exists :: Testable a => Int -> a -> Bool
- counterExample :: Testable a => Int -> a -> Maybe [String]
- counterExamples :: Testable a => Int -> a -> [[String]]
- witness :: Testable a => Int -> a -> Maybe [String]
- witnesses :: Testable a => Int -> a -> [[String]]
- class Testable a where
- results :: Testable a => a -> [([String], Bool)]
- class Listable a where
- cons0 :: a -> [[a]]
- cons1 :: Listable a => (a -> b) -> [[b]]
- cons2 :: (Listable a, Listable b) => (a -> b -> c) -> [[c]]
- cons3 :: (Listable a, Listable b, Listable c) => (a -> b -> c -> d) -> [[d]]
- cons4 :: (Listable a, Listable b, Listable c, Listable d) => (a -> b -> c -> d -> e) -> [[e]]
- cons5 :: (Listable a, Listable b, Listable c, Listable d, Listable e) => (a -> b -> c -> d -> e -> f) -> [[f]]
- ofWeight :: [[a]] -> Int -> [[a]]
- addWeight :: [[a]] -> Int -> [[a]]
- suchThat :: [[a]] -> (a -> Bool) -> [[a]]
- (\/) :: [[a]] -> [[a]] -> [[a]]
- (\\//) :: [[a]] -> [[a]] -> [[a]]
- (><) :: [[a]] -> [[b]] -> [[(a, b)]]
- productWith :: (a -> b -> c) -> [[a]] -> [[b]] -> [[c]]
- mapT :: (a -> b) -> [[a]] -> [[b]]
- filterT :: (a -> Bool) -> [[a]] -> [[a]]
- concatT :: [[[[a]]]] -> [[a]]
- concatMapT :: (a -> [[b]]) -> [[a]] -> [[b]]
- toTiers :: [a] -> [[a]]
- (==>) :: Bool -> Bool -> Bool
- (+|) :: [a] -> [a] -> [a]
- listIntegral :: (Enum a, Num a) => [a]
- tiersFractional :: Fractional a => [[a]]

# Checking and testing

holds :: Testable a => Int -> a -> Bool Source #

Does a property **hold** up to a number of test values?

holds 1000 $ \xs -> length (sort xs) == length xs

fails :: Testable a => Int -> a -> Bool Source #

Does a property **fail** for a number of test values?

fails 1000 $ \xs -> xs ++ ys == ys ++ xs

exists :: Testable a => Int -> a -> Bool Source #

There **exists** an assignment of values that satisfies a property
up to a number of test values?

exists 1000 $ \x -> x > 10

counterExamples :: Testable a => Int -> a -> [[String]] Source #

Lists all counter-examples for a number of tests to a property,

witnesses :: Testable a => Int -> a -> [[String]] Source #

Lists all witnesses up to a number of tests to a property,

class Testable a where Source #

`Testable`

values are functions
of `Listable`

arguments that return boolean values,
e.g.:

Bool

Listable a => a -> Bool

Listable a => a -> a -> Bool

Int -> Bool

String -> [Int] -> Bool

resultiers :: a -> [[([String], Bool)]] Source #

results :: Testable a => a -> [([String], Bool)] Source #

List all results of a `Testable`

property.
Each result is a pair of a list of strings and a boolean.
The list of strings is a printable representation of one possible choice of
argument values for the property. Each boolean paired with such a list
indicates whether the property holds for this choice. The outer list is
potentially infinite and lazily evaluated.

# Listing test values

class Listable a where Source #

A type is `Listable`

when there exists a function that
is able to list (ideally all of) its values.

Ideally, instances should be defined by a `tiers`

function that
returns a (potentially infinite) list of finite sub-lists (tiers):
the first sub-list contains elements of size 0,
the second sub-list contains elements of size 1
and so on.
Size here is defined by the implementor of the type-class instance.

For algebraic data types, the general form for `tiers`

is

tiers = cons<N> ConstructorA \/ cons<N> ConstructorB \/ ... \/ cons<N> ConstructorZ

where `N`

is the number of arguments of each constructor `A...Z`

.

Instances can be alternatively defined by `list`

.
In this case, each sub-list in `tiers`

is a singleton list
(each succeeding element of `list`

has +1 size).

The function `deriveListable`

from Test.LeanCheck.Derive
can automatically derive instances of this typeclass.

A `Listable`

instance for functions is also available but is not exported by
default. Import Test.LeanCheck.Function if you need to test higher-order
properties.

## Constructing lists of tiers

Given a constructor with no arguments,
returns `tiers`

of all possible applications of this constructor.
Since in this case there is only one possible application (to no
arguments), only a single value, of size/weight 0, will be present in the
resulting list of tiers.

cons3 :: (Listable a, Listable b, Listable c) => (a -> b -> c -> d) -> [[d]] Source #

Returns tiers of applications of a 3-argument constructor.

cons4 :: (Listable a, Listable b, Listable c, Listable d) => (a -> b -> c -> d -> e) -> [[e]] Source #

Returns tiers of applications of a 4-argument constructor.

cons5 :: (Listable a, Listable b, Listable c, Listable d, Listable e) => (a -> b -> c -> d -> e -> f) -> [[f]] Source #

Returns tiers of applications of a 5-argument constructor.

Test.LeanCheck.Basic defines
`cons6`

up to `cons12`

.
Those are exported by default from Test.LeanCheck,
but are hidden from the Haddock documentation.

ofWeight :: [[a]] -> Int -> [[a]] Source #

Resets the weight of a constructor (or tiers) Typically used as an infix constructor when defining Listable instances:

cons<N> `ofWeight` <W>

Be careful: do not apply

to recursive data structure
constructors. In general this will make the list of size 0 infinite,
breaking the tier invariant (each tier must be finite).`ofWeight`

0

suchThat :: [[a]] -> (a -> Bool) -> [[a]] Source #

Tiers of values that follow a property

cons<N> `suchThat` condition

## Combining lists of tiers

(\/) :: [[a]] -> [[a]] -> [[a]] infixr 7 Source #

Append tiers --- sum of two tiers enumerations.

[xs,ys,zs,...] \/ [as,bs,cs,...] = [xs++as,ys++bs,zs++cs,...]

(\\//) :: [[a]] -> [[a]] -> [[a]] infixr 7 Source #

Interleave tiers --- sum of two tiers enumerations.
When in doubt, use `\/`

instead.

[xs,ys,zs,...] \/ [as,bs,cs,...] = [xs+|as,ys+|bs,zs+|cs,...]

(><) :: [[a]] -> [[b]] -> [[(a, b)]] infixr 8 Source #

Take a tiered product of lists of tiers.

[t0,t1,t2,...] >< [u0,u1,u2,...] = [ t0**u0 , t0**u1 ++ t1**u0 , t0**u2 ++ t1**u1 ++ t2**u0 , ... ... ... ... ] where xs ** ys = [(x,y) | x <- xs, y <- ys]

Example:

[[0],[1],[2],...] >< [[0],[1],[2],...] == [ [(0,0)] , [(1,0),(0,1)] , [(2,0),(1,1),(0,2)] , [(3,0),(2,1),(1,2),(0,3)] ... ]

productWith :: (a -> b -> c) -> [[a]] -> [[b]] -> [[c]] Source #

Take a tiered product of lists of tiers.
`productWith`

can be defined by `><`

, as:

productWith f xss yss = map (uncurry f) $ xss >< yss

## Manipulating lists of tiers

concatMapT :: (a -> [[b]]) -> [[a]] -> [[b]] Source #

`concatMap`

over tiers

toTiers :: [a] -> [[a]] Source #

Takes a list of values `xs`

and transform it into tiers on which each
tier is occupied by a single element from `xs`

.

To convert back to a list, just `concat`

.

## Boolean (property) operators

(==>) :: Bool -> Bool -> Bool infixr 0 Source #

Boolean implication operator. Useful for defining conditional properties:

prop_something x y = condition x y ==> something x y

## Misc utilities

(+|) :: [a] -> [a] -> [a] infixr 5 Source #

Lazily interleaves two lists, switching between elements of the two. Union/sum of the elements in the lists.

[x,y,z] +| [a,b,c] == [x,a,y,b,z,c]

listIntegral :: (Enum a, Num a) => [a] Source #

tiersFractional :: Fractional a => [[a]] Source #

Tiers of `Fractional`

values.
This can be used as the implementation of `tiers`

for `Fractional`

types.