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

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

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

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`

.

## 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]
- tiersFractional :: Fractional a => [[a]]
- tiersFloating :: 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,

> 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

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 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 Int8 Source # | list :: [Int8] = [0, 1, -1, 2, -2, 3, -3, ..., 127, -127, -128] |

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 Integer Source # | list :: [Int] = [0, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5, 6, ...] |

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

Listable Word Source # | list :: [Word] = [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 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 () Source # | list :: [()] = [()] tiers :: [[()]] = [[()]] |

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

Listable CChar Source # | |

Listable CSChar Source # | |

Listable CUChar Source # | |

Listable CShort Source # | |

Listable CUShort Source # | |

Listable CInt Source # | |

Listable CUInt Source # | |

Listable CLong Source # | |

Listable CULong Source # | |

Listable CLLong Source # | |

Listable CULLong Source # | |

Listable CBool Source # | |

Listable CFloat Source # | |

Listable CDouble Source # | |

Listable CPtrdiff Source # | |

Listable CSize Source # | |

Listable CWchar Source # | |

Listable CSigAtomic Source # | |

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

Listable CClock Source # | |

Listable CTime Source # | |

Listable CUSeconds Source # | |

Listable CSUSeconds Source # | |

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

Listable CIntPtr Source # | |

Listable CUIntPtr Source # | |

Listable CIntMax Source # | |

Listable CUIntMax Source # | |

Listable IOMode Source # | |

Listable GeneralCategory Source # | |

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

Listable Letters Source # | |

Listable AlphaNums Source # | |

Listable Digits Source # | |

Listable Alphas Source # | |

Listable Uppers Source # | |

Listable Lowers Source # | |

Listable Spaces Source # | |

Listable Letter Source # | |

Listable AlphaNum Source # | |

Listable Digit Source # | |

Listable Alpha Source # | |

Listable Upper Source # | |

Listable Lower Source # | |

Listable Space Source # | |

Listable Nat7 Source # | |

Listable Nat6 Source # | |

Listable Nat5 Source # | |

Listable Nat4 Source # | |

Listable Nat3 Source # | |

Listable Nat2 Source # | |

Listable Nat1 Source # | |

Listable Nat Source # | |

Listable Natural Source # | |

Listable Word4 Source # | |

Listable Word3 Source # | |

Listable Word2 Source # | |

Listable Word1 Source # | |

Listable Int4 Source # | |

Listable Int3 Source # | |

Listable Int2 Source # | |

Listable Int1 Source # | |

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 (Maybe a) Source # | tiers :: [[Maybe Int]] = [[Nothing], [Just 0], [Just 1], ...] tiers :: [[Maybe Bool]] = [[Nothing], [Just False, Just True]] |

(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 , ... ] |

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

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

(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 , ... ] |

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

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

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

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

(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 (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 (Map a b) Source # | |

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

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.

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

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

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

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`

.

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

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

Tiers of `Fractional`

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

for `Fractional`

types.

tiersFractional :: [[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] , [ 1 % 6, 2 % 5, 3 % 4, 4 % 3, 5 % 2, 6 % 1] , [(-1) % 6, (-2) % 5, (-3) % 4, (-4) % 3, (-5) % 2, (-6) % 1] , ... ]

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

Tiers of `Floating`

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

for `Floating`

types.

This function is equivalent to `tiersFractional`

with positive and negative infinities included: 1*0 and -1*0.

tiersFloating :: [[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] , [ 0.2, 5.0] , [-0.2, -5.0] , [ 0.16666667, 0.4, 0.75, 1.3333334, 2.5, 6.0] , [-0.16666667, -0.4, -0.75, -1.3333334, -2.5, -6.0] , ... ]

`NaN`

and `-0`

are excluded from this enumeration.