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

Language | Haskell2010 |

LeanCheck is a simple enumerative property-based testing library.

A **property** is a function returning a `Bool`

that should be `True`

for
all possible choices of arguments. Properties can be viewed as a
parameterized unit tests.

To check if a property `holds`

by testing up to a thousand values,
we evaluate:

holds 1000 property

`True`

indicates success. `False`

indicates a bug.

For example:

holds $ \xs -> length (sort xs) == length (xs::[Int])

To get the smallest `counterExample`

by testing up to a thousand values,
we evaluate:

counterExample 1000 property

Arguments of properties should be instances of the `Listable`

typeclass.
`Listable`

instances are provided for the most common Haskell types.
New instances are easily defined
(see `Listable`

for more info).

- holds :: Testable a => Int -> a -> Bool
- fails :: Testable a => Int -> a -> Bool
- exists :: Testable a => Int -> a -> Bool
- (==>) :: Bool -> Bool -> 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]]
- check :: Testable a => a -> IO ()
- checkFor :: Testable a => Int -> a -> IO ()
- checkResult :: Testable a => a -> IO Bool
- checkResultFor :: Testable a => Int -> a -> IO 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]]
- deleteT :: Eq a => a -> [[a]] -> [[a]]
- normalizeT :: [[a]] -> [[a]]
- toTiers :: [a] -> [[a]]
- deriveListable :: Name -> DecsQ
- setCons :: Listable a => ([a] -> b) -> [[b]]
- bagCons :: Listable a => ([a] -> b) -> [[b]]
- noDupListCons :: Listable a => ([a] -> b) -> [[b]]
- product3With :: (a -> b -> c -> d) -> [[a]] -> [[b]] -> [[c]] -> [[d]]
- productMaybeWith :: (a -> b -> Maybe c) -> [[a]] -> [[b]] -> [[c]]
- listsOf :: [[a]] -> [[[a]]]
- setsOf :: [[a]] -> [[[a]]]
- bagsOf :: [[a]] -> [[[a]]]
- noDupListsOf :: [[a]] -> [[[a]]]
- products :: [[[a]]] -> [[[a]]]
- listsOfLength :: Int -> [[a]] -> [[[a]]]
- tiersFractional :: Fractional a => [[a]]
- listIntegral :: (Enum a, Num a) => [a]
- (+|) :: [a] -> [a] -> [a]
- class Testable a
- results :: Testable a => a -> [([String], Bool)]

# 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

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

## Counterexamples and witnesses

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,

## Reporting

check :: Testable a => a -> IO () Source #

Checks a property printing results on `stdout`

> check $ \xs -> sort (sort xs) == sort (xs::[Int]) +++ OK, passed 200 tests. > check $ \xs ys -> xs `union` ys == ys `union` (xs::[Int]) *** Failed! Falsifiable (after 4 tests): [] [0,0]

checkFor :: Testable a => Int -> a -> IO () Source #

Check a property for a given number of tests
printing results on `stdout`

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

## Listing constructors

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 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 tiers

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

`concatMap`

over tiers

deleteT :: Eq a => a -> [[a]] -> [[a]] Source #

Delete the first occurence of an element in a tier.

For tiers without repetitions, the following holds:

deleteT x = normalizeT . (`suchThat` (/= x))

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

Normalizes tiers by removing an empty tier from the end of a list of tiers.

normalizeT [xs0,xs1,...,xsN,[]] = [xs0,xs1,...,xsN]

Note this will only remove a single empty tier:

normalizeT [xs0,xs1,...,xsN,[],[]] = [xs0,xs1,...,xsN,[]]

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`

.

## Automatically deriving Listable instances

deriveListable :: Name -> DecsQ Source #

Derives a `Listable`

instance for a given type `Name`

.

Consider the following `Stack`

datatype:

data Stack a = Stack a (Stack a) | Empty

Writing

deriveListable ''Stack

will automatically derive the following `Listable`

instance:

instance Listable a => Listable (Stack a) where tiers = cons2 Stack \/ cons0 Empty

Needs the `TemplateHaskell`

extension.

## Specialized constructors of tiers

setCons :: Listable a => ([a] -> b) -> [[b]] Source #

Given a constructor that takes a set of elements (as a list), lists tiers of applications of this constructor.

A naive `Listable`

instance for the `Set`

(of Data.Set)
would read:

instance Listable a => Listable (Set a) where tiers = cons0 empty \/ cons2 insert

The above instance has a problem: it generates repeated sets. A more efficient implementation that does not repeat sets is given by:

tiers = setCons fromList

Alternatively, you can use `setsOf`

direclty.

bagCons :: Listable a => ([a] -> b) -> [[b]] Source #

Given a constructor that takes a bag of elements (as a list), lists tiers of applications of this constructor.

For example, a `Bag`

represented as a list.

bagCons Bag

noDupListCons :: Listable a => ([a] -> b) -> [[b]] Source #

Given a constructor that takes a list with no duplicate elements, return tiers of applications of this constructor.

## Products of tiers

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

Like `productWith`

, but over 3 lists of tiers.

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

# Listing lists

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

Takes as argument tiers of element values; returns tiers of lists of elements.

listsOf [[]] == [[[]]]

listsOf [[x]] == [ [[]] , [[x]] , [[x,x]] , [[x,x,x]] , ... ]

listsOf [[x],[y]] == [ [[]] , [[x]] , [[x,x],[y]] , [[x,x,x],[x,y],[y,x]] , ... ]

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

Takes as argument tiers of element values; returns tiers of size-ordered lists of elements without repetition.

setsOf [[0],[1],[2],...] = [ [[]] , [[0]] , [[1]] , [[0,1],[2]] , [[0,2],[3]] , [[0,3],[1,2],[4]] , [[0,1,2],[0,4],[1,3],[5]] , ... ]

Can be used in the constructor of specialized `Listable`

instances.
For `Set`

(from Data.Set), we would have:

instance Listable a => Listable (Set a) where tiers = mapT fromList $ setsOf tiers

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

Takes as argument tiers of element values; returns tiers of size-ordered lists of elements possibly with repetition.

bagsOf [[0],[1],[2],...] = [ [[]] , [[0]] , [[0,0],[1]] , [[0,0,0],[0,1],[2]] , [[0,0,0,0],[0,0,1],[0,2],[1,1],[3]] , [[0,0,0,0,0],[0,0,0,1],[0,0,2],[0,1,1],[0,3],[1,2],[4]] , ... ]

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

Takes as argument tiers of element values; returns tiers of lists with no repeated elements.

noDupListsOf [[0],[1],[2],...] == [ [[]] , [[0]] , [[1]] , [[0,1],[1,0],[2]] , [[0,2],[2,0],[3]] , ... ]

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

Takes the product of N lists of tiers, producing lists of length N.

Alternatively, takes as argument a list of lists of tiers of elements; returns lists combining elements of each list of tiers.

products [xss] = mapT (:[]) xss products [xss,yss] = mapT (\(x,y) -> [x,y]) (xss >< yss) products [xss,yss,zss] = product3With (\x y z -> [x,y,z]) xss yss zss

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

Takes as argument an integer length and tiers of element values; returns tiers of lists of element values of the given length.

listsOfLength 3 [[0],[1],[2],[3],[4]...] = [ [[0,0,0]] , [[0,0,1],[0,1,0],[1,0,0]] , [[0,0,2],[0,1,1],[0,2,0],[1,0,1],[1,1,0],[2,0,0]] , ... ]

## Listing values

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

Tiers of `Fractional`

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

for `Fractional`

types.

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

(+|) :: [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]

# Test results

`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

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.