Copyright | (c) 2015-2020 Rudy Matela |
---|---|

License | 3-Clause BSD (see the file LICENSE) |

Maintainer | Rudy Matela <rudy@matela.com.br> |

Safe Haskell | Safe-Inferred |

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`

.

## Synopsis

- 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
- resultiers :: a -> [[([String], Bool)]]

- 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]]
- delay :: [[a]] -> [[a]]
- reset :: [[a]] -> [[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 :: (Ord a, Num a) => [a]
- listFractional :: (Ord a, Fractional a) => [a]
- listFloating :: (Ord a, 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 True

> holds 1000 $ \x -> x == x + 1 False

The suggested number of test values are 500, 1 000 or 10 000.
With more than that you may or may not run out of memory
depending on the types being tested.
This also applies to `fails`

, `exists`

, etc.

(cf. `fails`

, `counterExample`

)

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

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

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

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

This is the negation of `holds`

.

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 True

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

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

> counterExamples 12 $ \xs -> xs == nub (xs :: [Int]) [["[0,0]"],["[0,0,0]"],["[0,0,0,0]"],["[0,0,1]"],["[0,1,0]"]]

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

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

> witnesses 1000 (\x -> x > 1 && x < 77 && 77 `rem` x == 0) [["7"],["11"]]

class Testable a where Source #

`Testable`

values are functions
of `Listable`

arguments that return boolean values.

Bool

Listable a => a -> Bool

(Listable a, Listable b) => a -> b -> Bool

(Listable a, Listable b, Listable c) => a -> b -> c -> Bool

(Listable a, Listable b, Listable c, ...) => a -> b -> c -> ... -> Bool

For example:

Int -> Bool

String -> [Int] -> Bool

(cf. `results`

)

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.

> results (<) [ (["0","0"], False) , (["0","1"], True) , (["1","0"], False) , (["0","(-1)"], False) , (["1","1"], False) , (["(-1)","0"], True) , (["0","2"], True) , (["1","(-1)"], False) , ... ]

> take 10 $ results (\xs -> xs == nub (xs :: [Int])) [ (["[]"], True) , (["[0]"], True) , (["[0,0]"], False) , (["[1]"], True) , (["[0,0,0]"], False) , ... ]

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

.

Here is a datatype with 4 constructors and its listable instance:

data MyType = MyConsA | MyConsB Int | MyConsC Int Char | MyConsD String instance Listable MyType where tiers = cons0 MyConsA \/ cons1 MyConsB \/ cons2 MyConsC \/ cons1 MyConsD

The instance for Hutton's Razor is given by:

data Expr = Val Int | Add Expr Expr instance Listable Expr where tiers = cons1 Val \/ cons2 Add

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.

#### Instances

Listable CBool Source # | |

Listable CChar Source # | |

Listable CClock Source # | |

Listable CDouble Source # | |

Listable CFloat Source # | |

Listable CInt Source # | |

Listable CIntMax Source # | |

Listable CIntPtr Source # | |

Listable CLLong Source # | |

Listable CLong Source # | |

Listable CPtrdiff Source # | |

Listable CSChar Source # | |

Listable CSUSeconds Source # | |

Defined in Test.LeanCheck.Basic tiers :: [[CSUSeconds]] Source # list :: [CSUSeconds] Source # | |

Listable CShort Source # | |

Listable CSigAtomic Source # | |

Defined in Test.LeanCheck.Basic tiers :: [[CSigAtomic]] Source # list :: [CSigAtomic] Source # | |

Listable CSize Source # | |

Listable CTime Source # | |

Listable CUChar Source # | |

Listable CUInt Source # | |

Listable CUIntMax Source # | |

Listable CUIntPtr Source # | |

Listable CULLong Source # | |

Listable CULong Source # | |

Listable CUSeconds Source # | |

Listable CUShort Source # | |

Listable CWchar Source # | |

Listable SeekMode Source # | |

Listable ExitCode Source # | Only includes valid POSIX exit codes > list :: [ExitCode] [ExitSuccess, ExitFailure 1, ExitFailure 2, ..., ExitFailure 255] |

Listable BufferMode Source # | |

Defined in Test.LeanCheck.Basic tiers :: [[BufferMode]] Source # list :: [BufferMode] Source # | |

Listable IOMode Source # | |

Listable Int16 Source # | list :: [Int16] = [0, 1, -1, 2, -2, ..., 32767, -32767, -32768] |

Listable Int32 Source # | list :: [Int32] = [0, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5, 6, ...] |

Listable Int64 Source # | list :: [Int64] = [0, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5, 6, ...] |

Listable Int8 Source # | list :: [Int8] = [0, 1, -1, 2, -2, 3, -3, ..., 127, -127, -128] |

Listable GeneralCategory Source # | |

Defined in Test.LeanCheck.Basic tiers :: [[GeneralCategory]] Source # list :: [GeneralCategory] Source # | |

Listable Word16 Source # | list :: [Word16] = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, ..., 65535] |

Listable Word32 Source # | list :: [Word32] = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, ...] |

Listable Word64 Source # | list :: [Word64] = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, ...] |

Listable Word8 Source # | list :: [Word8] = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, ..., 255] |

Listable Ordering Source # | list :: [Ordering] = [LT, EQ, GT] |

Listable A Source # | |

Listable Alpha Source # | |

Listable AlphaNum Source # | |

Listable AlphaNums Source # | |

Listable Alphas Source # | |

Listable B Source # | |

Listable C Source # | |

Listable D Source # | |

Listable Digit Source # | |

Listable Digits Source # | |

Listable E Source # | |

Listable F Source # | |

Listable Int1 Source # | |

Listable Int2 Source # | |

Listable Int3 Source # | |

Listable Int4 Source # | |

Listable Letter Source # | |

Listable Letters Source # | |

Listable Lower Source # | |

Listable Lowers Source # | |

Listable Nat Source # | |

Listable Nat1 Source # | |

Listable Nat2 Source # | |

Listable Nat3 Source # | |

Listable Nat4 Source # | |

Listable Nat5 Source # | |

Listable Nat6 Source # | |

Listable Nat7 Source # | |

Listable Natural Source # | |

Listable Space Source # | |

Listable Spaces Source # | |

Listable Upper Source # | |

Listable Uppers Source # | |

Listable Word1 Source # | |

Listable Word2 Source # | |

Listable Word3 Source # | |

Listable Word4 Source # | |

Listable Integer Source # | list :: [Int] = [0, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5, 6, ...] |

Listable () Source # | list :: [()] = [()] tiers :: [[()]] = [[()]] |

Listable Bool Source # | tiers :: [[Bool]] = [[False,True]] list :: [[Bool]] = [False,True] |

Listable Char Source # | list :: [Char] = ['a', ' ', 'b', 'A', 'c', '\', 'n', 'd', ...] |

Listable Double Source # |
list :: [Double] = [0.0, 1.0, -1.0, Infinity, 0.5, 2.0, ...] |

Listable Float Source # |
list :: [Float] = [ 0.0 , 1.0, -1.0, Infinity , 0.5, 2.0, -Infinity, -0.5, -2.0 , 0.33333334, 3.0, -0.33333334, -3.0 , 0.25, 0.6666667, 1.5, 4.0, -0.25, -0.6666667, -1.5, -4.0 , ... ] |

Listable Int Source # | tiers :: [[Int]] = [[0], [1], [-1], [2], [-2], [3], [-3], ...] list :: [Int] = [0, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5, 6, ...] |

Listable Word Source # | list :: [Word] = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, ...] |

(RealFloat a, Listable a) => Listable (Complex a) Source # | |

(Integral a, Listable a) => Listable (Ratio a) Source # | list :: [Rational] = [ 0 % 1 , 1 % 1 , (-1) % 1 , 1 % 2, 2 % 1 , (-1) % 2, (-2) % 1 , 1 % 3, 3 % 1 , (-1) % 3, (-3) % 1 , 1 % 4, 2 % 3, 3 % 2, 4 % 1 , (-1) % 4, (-2) % 3, (-3) % 2, (-4) % 1 , 1 % 5, 5 % 1 , (-1) % 5, (-5) % 1 , ... ] |

Listable a => Listable (Bag a) Source # | |

Listable a => Listable (NoDup a) Source # | |

Listable a => Listable (Set a) Source # | |

(Integral a, Bounded a) => Listable (X a) Source # | Extremily large integers are intercalated with small integers. list :: [X Int] = map X [ 0, 1, -1, maxBound, minBound , 2, -2, maxBound-1, minBound+1 , 3, -3, maxBound-2, minBound+2 , ... ] |

(Integral a, Bounded a) => Listable (Xs a) Source # | Lists with elements of the |

Listable a => Listable (Maybe a) Source # | tiers :: [[Maybe Int]] = [[Nothing], [Just 0], [Just 1], ...] tiers :: [[Maybe Bool]] = [[Nothing], [Just False, Just True]] |

Listable a => Listable [a] Source # | tiers :: [[ [Int] ]] = [ [ [] ] , [ [0] ] , [ [0,0], [1] ] , [ [0,0,0], [0,1], [1,0], [-1] ] , ... ] list :: [ [Int] ] = [ [], [0], [0,0], [1], [0,0,0], ... ] |

(Listable a, Listable b) => Listable (Either a b) Source # | tiers :: [[Either Bool Bool]] = [[Left False, Right False, Left True, Right True]] tiers :: [[Either Int Int]] = [ [Left 0, Right 0] , [Left 1, Right 1] , [Left (-1), Right (-1)] , [Left 2, Right 2] , ... ] |

(Listable a, Listable b) => Listable (Map a b) Source # | |

(Eq a, Listable a, Listable b) => Listable (a -> b) Source # | |

(Listable a, Listable b) => Listable (a, b) Source # | tiers :: [[(Int,Int)]] = [ [(0,0)] , [(0,1),(1,0)] , [(0,-1),(1,1),(-1,0)] , ...] list :: [(Int,Int)] = [ (0,0), (0,1), (1,0), (0,-1), (1,1), ...] |

(Listable a, Listable b, Listable c) => Listable (a, b, c) Source # | list :: [(Int,Int,Int)] = [ (0,0,0), (0,0,1), (0,1,0), ...] |

(Listable a, Listable b, Listable c, Listable d) => Listable (a, b, c, d) Source # | |

(Listable a, Listable b, Listable c, Listable d, Listable e) => Listable (a, b, c, d, e) Source # | |

(Listable a, Listable b, Listable c, Listable d, Listable e, Listable f) => Listable (a, b, c, d, e, f) Source # | |

(Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g) => Listable (a, b, c, d, e, f, g) Source # | |

(Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g, Listable h) => Listable (a, b, c, d, e, f, g, h) Source # | |

(Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g, Listable h, Listable i) => Listable (a, b, c, d, e, f, g, h, i) Source # | |

(Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g, Listable h, Listable i, Listable j) => Listable (a, b, c, d, e, f, g, h, i, j) Source # | |

(Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g, Listable h, Listable i, Listable j, Listable k) => Listable (a, b, c, d, e, f, g, h, i, j, k) Source # | |

(Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g, Listable h, Listable i, Listable j, Listable k, Listable l) => Listable (a, b, c, d, e, f, g, h, i, j, k, l) Source # | |

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

To be used in the declaration of `tiers`

in `Listable`

instances.

instance Listable <Type> where tiers = ... \/ cons0 <Constructor> \/ ...

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

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

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

Delays the enumeration of `tiers`

.
Conceptually this function adds to the weight of a constructor.

delay [xs, ys, zs, ... ] = [[], xs, ys, zs, ...]

delay [[x,...], [y,...], ...] = [[], [x,...], [y,...], ...]

Typically used when defining `Listable`

instances:

instance Listable <Type> where tiers = ... \/ delay (cons<N> <Constructor>) \/ ...

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

Resets any delays in a list-of `tiers`

.
Conceptually this function makes a constructor "weightless",
assuring the first tier is non-empty.

reset [[], [], ..., xs, ys, zs, ...] = [xs, ys, zs, ...]

reset [[], xs, ys, zs, ...] = [xs, ys, zs, ...]

reset [[], [], ..., [x], [y], [z], ...] = [[x], [y], [z], ...]

Typically used when defining `Listable`

instances:

instance Listable <Type> where tiers = ... \/ reset (cons<N> <Constructor>) \/ ...

Be careful: do not apply `reset`

to recursive data structure
constructors. In general this will make the list of size 0 infinite,
breaking the `tiers`

invariant (each tier must be finite).

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

Tiers of values that follow a property.

Typically used in the definition of `Listable`

tiers:

instance Listable <Type> where tiers = ... \/ cons<N> `suchThat` <condition> \/ ...

Examples:

> tiers `suchThat` odd [[], [1], [-1], [], [], [3], [-3], [], [], [5], ...]

> tiers `suchThat` even [[0], [], [], [2], [-2], [], [], [4], [-4], [], ...]

## 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)] , ... ]

(cf. `productWith`

)

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

(cf. `><`

)

## Manipulating lists of tiers

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

`map`

over tiers

mapT f [[x], [y,z], [w,...], ...] = [[f x], [f y, f z], [f w, ...], ...]

mapT f [xs, ys, zs, ...] = [map f xs, map f ys, map f zs]

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

`filter`

tiers

filterT p [xs, yz, zs, ...] = [filter p xs, filter p ys, filter p zs]

filterT odd tiers = [[], [1], [-1], [], [], [3], [-3], [], [], [5], ...]

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

`concat`

tiers of tiers

concatT [ [xss0, yss0, zss0, ...] , [xss1, yss1, zss1, ...] , [xss2, yss2, zss2, ...] , ... ] = xss0 \/ yss0 \/ zss0 \/ ... \/ delay (xss1 \/ yss1 \/ zss1 \/ ... \/ delay (xss2 \/ yss2 \/ zss2 \/ ... \/ (delay ...)))

(cf. `concatMapT`

)

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

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`

.

toTiers [x, y, z, ...] = [[x], [y], [z], ...]

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

Examples:

> prop_addMonotonic x y = y > 0 ==> x + y > x > check prop_addMonotonic +++ OK, passed 200 tests.

## 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 :: (Ord a, Num a) => [a] Source #

Tiers of `Integral`

values.
Can be used as a default implementation of `list`

for `Integral`

types.

For types with negative values, like `Int`

,
the list starts with 0 then intercalates between positives and negatives.

listIntegral = [0, 1, -1, 2, -2, 3, -3, 4, -4, ...]

For types without negative values, like `Word`

,
the list starts with 0 followed by positives of increasing magnitude.

listIntegral = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, ...]

This function will not work for types that throw errors when the result of
an arithmetic operation is negative such as `Natural`

. For these, use
`[0..]`

as the `list`

implementation.

listFractional :: (Ord a, Fractional a) => [a] Source #

Listing of `Fractional`

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

for `Fractional`

types.

listFractional :: [[Rational]] = [0 % 1, 1 % 1, (-1) % 1, 1 % 2, (-1) % 2, 2 % 1, (-2) % 1, 1 % 3, ...]

All rationals are included without repetition in their most simple form.
This is the Calkin-Wilf sequence
computed with the help of the `fusc`

function (EWD 570).

This also works for unsigned types that wrap around zero, yielding:

listFractional :: [Ratio Word] = [0 % 1, 1 % 1, 1 % 2, 2 % 1, 1 % 3, 3 % 2, 2 % 3, 3 % 1, 1 % 4, ...]

listFloating :: (Ord a, Fractional a) => [a] Source #

Listing of `Floating`

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

for `Floating`

types.

listFloating :: [Double] = [0.0, 1.0, -1.0, 0.5, -0.5, 2.0, Infinity, -Infinity, -2.0, 0.333, ...]

This follow the same Calkin-Wilf sequence of `listFractional`

but positive and negative infinities are artificially included after two.

`NaN`

and `-0`

are excluded from this enumeration.