-- |
-- Module      : Test.LeanCheck.Core
-- Copyright   : (c) 2015-2024 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- 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
--       ('Test.LeanCheck.Basic.cons6' ...
--        'Test.LeanCheck.Basic.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
--      'Test.LeanCheck.Derive.deriveListable'.
module Test.LeanCheck.Core
  (
  -- * Checking and testing
    holds
  , fails
  , exists
  , counterExample
  , counterExamples
  , witness
  , witnesses
  , Testable(..)

  , results

  -- * Listing test values
  , Listable(..)

  -- ** Constructing lists of tiers
  , cons0
  , cons1
  , cons2
  , cons3
  , cons4
  , cons5

  , delay
  , reset
  , suchThat

  -- ** Combining lists of tiers
  , (\/), (\\//)
  , (><)
  , productWith

  -- ** Manipulating lists of tiers
  , mapT
  , filterT
  , concatT
  , concatMapT
  , toTiers

  -- ** Boolean (property) operators
  , (==>)

  -- ** Misc utilities
  , (+|)
  , listIntegral
  , listFractional
  , listFloating
  )
where

import Data.Maybe (listToMaybe)


-- | 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 'Test.LeanCheck.Derive.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.
class Listable a where
  tiers :: [[a]]
  list :: [a]
  tiers  =  [a] -> [[a]]
forall a. [a] -> [[a]]
toTiers [a]
forall a. Listable a => [a]
list
  list  =  [[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[a]]
forall a. Listable a => [[a]]
tiers
  {-# MINIMAL list | tiers #-}

-- | 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'.
toTiers :: [a] -> [[a]]
toTiers :: forall a. [a] -> [[a]]
toTiers  =  (a -> [a]) -> [a] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map (a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[])

-- | > list :: [()]  =  [()]
--   > tiers :: [[()]]  =  [[()]]
instance Listable () where
  list :: [()]
list  =  [()]

-- | 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 'GHC.Natural'.  For these, use
-- @[0..]@ as the 'list' implementation.
listIntegral :: (Ord a, Num a) => [a]
listIntegral :: forall a. (Ord a, Num a) => [a]
listIntegral  =  a
0 a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
positives [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
+| [a]
negatives
  where
  positives :: [a]
positives  =  (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>a
0) ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ (a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (a -> a -> a
forall a. Num a => a -> a -> a
+a
1) a
1  -- stop generating on overflow
  negatives :: [a]
negatives  =  (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<a
0) ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ (a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (a -> a -> a
forall a. Num a => a -> a -> a
subtract a
1) (-a
1)

-- | > tiers :: [[Int]]  =  [[0], [1], [-1], [2], [-2], [3], [-3], ...]
--   > list :: [Int]  =  [0, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5, 6, ...]
instance Listable Int where
  list :: [Int]
list  =  [Int]
forall a. (Ord a, Num a) => [a]
listIntegral

-- | > list :: [Int]  =  [0, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5, 6, ...]
instance Listable Integer where
  list :: [Integer]
list  =  [Integer]
forall a. (Ord a, Num a) => [a]
listIntegral

-- | > list :: [Char]  =  ['a', ' ', 'b', 'A', 'c', '\', 'n', 'd', ...]
instance Listable Char where
  list :: [Char]
list  =  [Char
'a'..Char
'z']
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
+| [Char
' ',Char
'\n']
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
+| [Char
'A'..Char
'Z']
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
+| [Char
'0'..Char
'9']
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
+| [Char
'!'..Char
'/']
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
+| [Char
'\t']
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
+| [Char
':'..Char
'@']
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
+| [Char
'['..Char
'`']
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
+| [Char
'{'..Char
'~']

-- | > tiers :: [[Bool]]  =  [[False,True]]
--   > list :: [[Bool]]  =  [False,True]
instance Listable Bool where
  tiers :: [[Bool]]
tiers  =  Bool -> [[Bool]]
forall a. a -> [[a]]
cons0 Bool
False [[Bool]] -> [[Bool]] -> [[Bool]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ Bool -> [[Bool]]
forall a. a -> [[a]]
cons0 Bool
True

-- | > tiers :: [[Maybe Int]]  =  [[Nothing], [Just 0], [Just 1], ...]
--   > tiers :: [[Maybe Bool]]  =  [[Nothing], [Just False, Just True]]
instance Listable a => Listable (Maybe a) where
  tiers :: [[Maybe a]]
tiers  =  Maybe a -> [[Maybe a]]
forall a. a -> [[a]]
cons0 Maybe a
forall a. Maybe a
Nothing [[Maybe a]] -> [[Maybe a]] -> [[Maybe a]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ (a -> Maybe a) -> [[Maybe a]]
forall a b. Listable a => (a -> b) -> [[b]]
cons1 a -> Maybe a
forall a. a -> Maybe a
Just

-- | > 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]
--   >                                 , ... ]
instance (Listable a, Listable b) => Listable (Either a b) where
  tiers :: [[Either a b]]
tiers  =  [[Either a b]] -> [[Either a b]]
forall a. [[a]] -> [[a]]
reset ((a -> Either a b) -> [[Either a b]]
forall a b. Listable a => (a -> b) -> [[b]]
cons1 a -> Either a b
forall a b. a -> Either a b
Left)
       [[Either a b]] -> [[Either a b]] -> [[Either a b]]
forall a. [[a]] -> [[a]] -> [[a]]
\\// [[Either a b]] -> [[Either a b]]
forall a. [[a]] -> [[a]]
reset ((b -> Either a b) -> [[Either a b]]
forall a b. Listable a => (a -> b) -> [[b]]
cons1 b -> Either a b
forall a b. b -> Either a b
Right)

-- | > 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), ...]
instance (Listable a, Listable b) => Listable (a,b) where
  tiers :: [[(a, b)]]
tiers  =  [[a]]
forall a. Listable a => [[a]]
tiers [[a]] -> [[b]] -> [[(a, b)]]
forall a b. [[a]] -> [[b]] -> [[(a, b)]]
>< [[b]]
forall a. Listable a => [[a]]
tiers

-- | > list :: [(Int,Int,Int)]  =  [ (0,0,0), (0,0,1), (0,1,0), ...]
instance (Listable a, Listable b, Listable c) => Listable (a,b,c) where
  tiers :: [[(a, b, c)]]
tiers  =  (a -> (b, c) -> (a, b, c)) -> [[a]] -> [[(b, c)]] -> [[(a, b, c)]]
forall a b c. (a -> b -> c) -> [[a]] -> [[b]] -> [[c]]
productWith (\a
x (b
y,c
z) -> (a
x,b
y,c
z)) [[a]]
forall a. Listable a => [[a]]
tiers [[(b, c)]]
forall a. Listable a => [[a]]
tiers

instance (Listable a, Listable b, Listable c, Listable d) =>
         Listable (a,b,c,d) where
  tiers :: [[(a, b, c, d)]]
tiers  =  (a -> (b, c, d) -> (a, b, c, d))
-> [[a]] -> [[(b, c, d)]] -> [[(a, b, c, d)]]
forall a b c. (a -> b -> c) -> [[a]] -> [[b]] -> [[c]]
productWith (\a
x (b
y,c
z,d
w) -> (a
x,b
y,c
z,d
w)) [[a]]
forall a. Listable a => [[a]]
tiers [[(b, c, d)]]
forall a. Listable a => [[a]]
tiers

instance (Listable a, Listable b, Listable c, Listable d, Listable e) =>
         Listable (a,b,c,d,e) where
  tiers :: [[(a, b, c, d, e)]]
tiers  =  (a -> (b, c, d, e) -> (a, b, c, d, e))
-> [[a]] -> [[(b, c, d, e)]] -> [[(a, b, c, d, e)]]
forall a b c. (a -> b -> c) -> [[a]] -> [[b]] -> [[c]]
productWith (\a
x (b
y,c
z,d
w,e
v) -> (a
x,b
y,c
z,d
w,e
v)) [[a]]
forall a. Listable a => [[a]]
tiers [[(b, c, d, e)]]
forall a. Listable a => [[a]]
tiers

-- | > tiers :: [[ [Int] ]]  =  [ [ [] ]
--   >                          , [ [0] ]
--   >                          , [ [0,0], [1] ]
--   >                          , [ [0,0,0], [0,1], [1,0], [-1] ]
--   >                          , ... ]
--   > list :: [ [Int] ]  =  [ [], [0], [0,0], [1], [0,0,0], ... ]
instance (Listable a) => Listable [a] where
  tiers :: [[[a]]]
tiers  =  [a] -> [[[a]]]
forall a. a -> [[a]]
cons0 []
         [[[a]]] -> [[[a]]] -> [[[a]]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ (a -> [a] -> [a]) -> [[[a]]]
forall a b c. (Listable a, Listable b) => (a -> b -> c) -> [[c]]
cons2 (:)

-- | 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, ...]
listFractional :: (Ord a, Fractional a) => [a]
listFractional :: forall a. (Ord a, Fractional a) => [a]
listFractional  =  a
0 a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
positives [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
+| [a]
negatives
  where
  stern :: [a]
stern  =  (Integer -> a) -> [Integer] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> a
forall a. Num a => Integer -> a
fromInteger (Integer -> a) -> (Integer -> Integer) -> Integer -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
fusc) [Integer
1..]
  positives :: [a]
positives  =  (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>a
0) ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> [a] -> [a] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> a
forall a. Fractional a => a -> a -> a
(/) [a]
stern (Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
1 [a]
stern)
  negatives :: [a]
negatives  =  (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<a
0) ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map a -> a
forall a. Num a => a -> a
negate [a]
positives
  fusc :: Integer -> Integer
fusc  =  Integer -> Integer -> Integer -> Integer
forall {t} {t}. (Integral t, Num t) => t -> t -> t -> t
fu Integer
1 Integer
0  where  fu :: t -> t -> t -> t
fu t
a t
b t
0               =  t
b
                          fu t
a t
b t
n  | t -> Bool
forall a. Integral a => a -> Bool
even t
n     =  t -> t -> t -> t
fu (t
a t -> t -> t
forall a. Num a => a -> a -> a
+ t
b) t
b (t
n t -> t -> t
forall a. Integral a => a -> a -> a
`div` t
2)
                                    | Bool
otherwise  =  t -> t -> t -> t
fu t
a (t
a t -> t -> t
forall a. Num a => a -> a -> a
+ t
b) ((t
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1) t -> t -> t
forall a. Integral a => a -> a -> a
`div` t
2)

-- | 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.
listFloating :: (Ord a, Fractional a) => [a]
listFloating :: forall a. (Ord a, Fractional a) => [a]
listFloating  =  [a]
heading [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a
two, a
1a -> a -> a
forall a. Fractional a => a -> a -> a
/a
0, -a
1a -> a -> a
forall a. Fractional a => a -> a -> a
/a
0] [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
etc
  where
  ([a]
heading,a
two:[a]
etc)  =  (a -> Bool) -> [a] -> ([a], [a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
2) [a]
forall a. (Ord a, Fractional a) => [a]
listFractional

-- | @NaN@ and @-0@ are not included in the list of 'Float's.
--
-- > 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
-- >   , ...
-- >   ]
instance Listable Float where
  list :: [Float]
list  =  [Float]
forall a. (Ord a, Fractional a) => [a]
listFloating

-- | @NaN@ and @-0@ are not included in the list of 'Double's.
--
-- > list :: [Double]  =  [0.0, 1.0, -1.0, Infinity, 0.5, 2.0, ...]
instance Listable Double where
  list :: [Double]
list  =  [Double]
forall a. (Ord a, Fractional a) => [a]
listFloating

-- | > list :: [Ordering]  =  [LT, EQ, GT]
instance Listable Ordering where
  tiers :: [[Ordering]]
tiers  =  Ordering -> [[Ordering]]
forall a. a -> [[a]]
cons0 Ordering
LT
         [[Ordering]] -> [[Ordering]] -> [[Ordering]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ Ordering -> [[Ordering]]
forall a. a -> [[a]]
cons0 Ordering
EQ
         [[Ordering]] -> [[Ordering]] -> [[Ordering]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ Ordering -> [[Ordering]]
forall a. a -> [[a]]
cons0 Ordering
GT

-- | '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]
mapT :: (a -> b) -> [[a]] -> [[b]]
mapT :: forall a b. (a -> b) -> [[a]] -> [[b]]
mapT  =  ([a] -> [b]) -> [[a]] -> [[b]]
forall a b. (a -> b) -> [a] -> [b]
map (([a] -> [b]) -> [[a]] -> [[b]])
-> ((a -> b) -> [a] -> [b]) -> (a -> b) -> [[a]] -> [[b]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map

-- | 'filter' tiers
--
-- > filterT p [xs, yz, zs, ...]  =  [filter p xs, filter p ys, filter p zs]
--
-- > filterT odd tiers  =  [[], [1], [-1], [], [], [3], [-3], [], [], [5], ...]
filterT :: (a -> Bool) -> [[a]] -> [[a]]
filterT :: forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT a -> Bool
f  =  ([a] -> [a]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
f)

-- | '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')
concatT :: [[ [[a]] ]] -> [[a]]
concatT :: forall a. [[[[a]]]] -> [[a]]
concatT  =  ([[a]] -> [[a]] -> [[a]]) -> [[a]] -> [[[a]]] -> [[a]]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [[a]] -> [[a]] -> [[a]]
forall a. [[a]] -> [[a]] -> [[a]]
(\+:/) [] ([[[a]]] -> [[a]]) -> ([[[[a]]]] -> [[[a]]]) -> [[[[a]]]] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([[[a]]] -> [[a]]) -> [[[[a]]]] -> [[[a]]]
forall a b. (a -> b) -> [a] -> [b]
map (([[a]] -> [[a]] -> [[a]]) -> [[a]] -> [[[a]]] -> [[a]]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [[a]] -> [[a]] -> [[a]]
forall a. [[a]] -> [[a]] -> [[a]]
(\/) [])
  where
  [[a]]
xss \+:/ :: [[a]] -> [[a]] -> [[a]]
\+:/ [[a]]
yss  =  [[a]]
xss [[a]] -> [[a]] -> [[a]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ ([][a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:[[a]]
yss)

-- | 'concatMap' over tiers
--
-- > concatMapT f [ [x0, y0, z0]
-- >              , [x1, y1, z1]
-- >              , [x2, y2, z2]
-- >              , ...
-- >              ]
-- >   =  f x0 \/ f y0 \/ f z0 \/ ...
-- >           \/ delay (f x1 \/ f y1 \/ f z1 \/ ...
-- >                          \/ delay (f x2 \/ f y2 \/ f z2 \/ ...
-- >                                         \/ (delay ...)))
--
-- (cf. 'concatT')
concatMapT :: (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT :: forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT a -> [[b]]
f  =  [[[[b]]]] -> [[b]]
forall a. [[[[a]]]] -> [[a]]
concatT ([[[[b]]]] -> [[b]]) -> ([[a]] -> [[[[b]]]]) -> [[a]] -> [[b]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> [[b]]) -> [[a]] -> [[[[b]]]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT a -> [[b]]
f


-- | 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>
-- >          \/ ...
cons0 :: a -> [[a]]
cons0 :: forall a. a -> [[a]]
cons0 a
x  =  [[a
x]]

-- | Given a constructor with one 'Listable' argument,
--   return 'tiers' of applications of this constructor.
--
-- By default, returned values will have size/weight of 1.
--
-- To be used in the declaration of 'tiers' in 'Listable' instances.
--
-- > instance Listable <Type> where
-- >   tiers  =  ...
-- >          \/ cons1 <Constructor>
-- >          \/ ...
cons1 :: Listable a => (a -> b) -> [[b]]
cons1 :: forall a b. Listable a => (a -> b) -> [[b]]
cons1 a -> b
f  =  [[b]] -> [[b]]
forall a. [[a]] -> [[a]]
delay ([[b]] -> [[b]]) -> [[b]] -> [[b]]
forall a b. (a -> b) -> a -> b
$ (a -> b) -> [[a]] -> [[b]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT a -> b
f [[a]]
forall a. Listable a => [[a]]
tiers

-- | Given a constructor with two 'Listable' arguments,
--   return 'tiers' of applications of this constructor.
--
-- By default, returned values will have size/weight of 1.
--
-- To be used in the declaration of 'tiers' in 'Listable' instances.
--
-- > instance Listable <Type> where
-- >   tiers  =  ...
-- >          \/ cons2 <Constructor>
-- >          \/ ...
cons2 :: (Listable a, Listable b) => (a -> b -> c) -> [[c]]
cons2 :: forall a b c. (Listable a, Listable b) => (a -> b -> c) -> [[c]]
cons2 a -> b -> c
f  =  [[c]] -> [[c]]
forall a. [[a]] -> [[a]]
delay ([[c]] -> [[c]]) -> [[c]] -> [[c]]
forall a b. (a -> b) -> a -> b
$ ((a, b) -> c) -> [[(a, b)]] -> [[c]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT ((a -> b -> c) -> (a, b) -> c
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> b -> c
f) [[(a, b)]]
forall a. Listable a => [[a]]
tiers

-- | Returns tiers of applications of a 3-argument constructor.
--
-- To be used in the declaration of 'tiers' in 'Listable' instances.
--
-- > instance Listable <Type> where
-- >   tiers  =  ...
-- >          \/ cons3 <Constructor>
-- >          \/ ...
cons3 :: (Listable a, Listable b, Listable c) => (a -> b -> c -> d) -> [[d]]
cons3 :: forall a b c d.
(Listable a, Listable b, Listable c) =>
(a -> b -> c -> d) -> [[d]]
cons3 a -> b -> c -> d
f  =  [[d]] -> [[d]]
forall a. [[a]] -> [[a]]
delay ([[d]] -> [[d]]) -> [[d]] -> [[d]]
forall a b. (a -> b) -> a -> b
$ ((a, b, c) -> d) -> [[(a, b, c)]] -> [[d]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT ((a -> b -> c -> d) -> (a, b, c) -> d
forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 a -> b -> c -> d
f) [[(a, b, c)]]
forall a. Listable a => [[a]]
tiers

-- | Returns tiers of applications of a 4-argument constructor.
--
-- To be used in the declaration of 'tiers' in 'Listable' instances.
cons4 :: (Listable a, Listable b, Listable c, Listable d)
      => (a -> b -> c -> d -> e) -> [[e]]
cons4 :: forall a b c d e.
(Listable a, Listable b, Listable c, Listable d) =>
(a -> b -> c -> d -> e) -> [[e]]
cons4 a -> b -> c -> d -> e
f  =  [[e]] -> [[e]]
forall a. [[a]] -> [[a]]
delay ([[e]] -> [[e]]) -> [[e]] -> [[e]]
forall a b. (a -> b) -> a -> b
$ ((a, b, c, d) -> e) -> [[(a, b, c, d)]] -> [[e]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT ((a -> b -> c -> d -> e) -> (a, b, c, d) -> e
forall a b c d e. (a -> b -> c -> d -> e) -> (a, b, c, d) -> e
uncurry4 a -> b -> c -> d -> e
f) [[(a, b, c, d)]]
forall a. Listable a => [[a]]
tiers

-- | Returns tiers of applications of a 5-argument constructor.
--
-- To be used in the declaration of 'tiers' in 'Listable' instances.
cons5 :: (Listable a, Listable b, Listable c, Listable d, Listable e)
      => (a -> b -> c -> d -> e -> f) -> [[f]]
cons5 :: forall a b c d e f.
(Listable a, Listable b, Listable c, Listable d, Listable e) =>
(a -> b -> c -> d -> e -> f) -> [[f]]
cons5 a -> b -> c -> d -> e -> f
f  =  [[f]] -> [[f]]
forall a. [[a]] -> [[a]]
delay ([[f]] -> [[f]]) -> [[f]] -> [[f]]
forall a b. (a -> b) -> a -> b
$ ((a, b, c, d, e) -> f) -> [[(a, b, c, d, e)]] -> [[f]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT ((a -> b -> c -> d -> e -> f) -> (a, b, c, d, e) -> f
forall a b c d e f.
(a -> b -> c -> d -> e -> f) -> (a, b, c, d, e) -> f
uncurry5 a -> b -> c -> d -> e -> f
f) [[(a, b, c, d, e)]]
forall a. Listable a => [[a]]
tiers

-- | 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>)
-- >          \/ ...
delay :: [[a]] -> [[a]]
delay :: forall a. [[a]] -> [[a]]
delay  =  ([][a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:)

-- | 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).
reset :: [[a]] -> [[a]]
reset :: forall a. [[a]] -> [[a]]
reset  =  ([a] -> Bool) -> [[a]] -> [[a]]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null

-- | 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], [], ...]
--
-- This function is just a 'flip'ped version of `filterT`.
suchThat :: [[a]] -> (a->Bool) -> [[a]]
suchThat :: forall a. [[a]] -> (a -> Bool) -> [[a]]
suchThat  =  ((a -> Bool) -> [[a]] -> [[a]]) -> [[a]] -> (a -> Bool) -> [[a]]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> Bool) -> [[a]] -> [[a]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT

-- | 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,...]
(+|) :: [a] -> [a] -> [a]
[]     +| :: forall a. [a] -> [a] -> [a]
+| [a]
ys  =  [a]
ys
(a
x:[a]
xs) +| [a]
ys  =  a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:([a]
ys [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
+| [a]
xs)
infixr 5 +|

-- | Append tiers --- sum of two tiers enumerations.
--
-- > [xs,ys,zs,...] \/ [as,bs,cs,...]  =  [xs++as, ys++bs, zs++cs, ...]
(\/) :: [[a]] -> [[a]] -> [[a]]
[[a]]
xss \/ :: forall a. [[a]] -> [[a]] -> [[a]]
\/ []   =  [[a]]
xss
[]  \/ [[a]]
yss  =  [[a]]
yss
([a]
xs:[[a]]
xss) \/ ([a]
ys:[[a]]
yss)  =  ([a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
ys) [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [[a]]
xss [[a]] -> [[a]] -> [[a]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ [[a]]
yss
infixr 7 \/

-- | 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]] -> [[a]] -> [[a]]
[[a]]
xss \\// :: forall a. [[a]] -> [[a]] -> [[a]]
\\// []   =  [[a]]
xss
[]  \\// [[a]]
yss  =  [[a]]
yss
([a]
xs:[[a]]
xss) \\// ([a]
ys:[[a]]
yss)  =  ([a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
+| [a]
ys) [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [[a]]
xss [[a]] -> [[a]] -> [[a]]
forall a. [[a]] -> [[a]] -> [[a]]
\\// [[a]]
yss
infixr 7 \\//

-- | 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')
(><) :: [[a]] -> [[b]] -> [[(a,b)]]
>< :: forall a b. [[a]] -> [[b]] -> [[(a, b)]]
(><)  =  (a -> b -> (a, b)) -> [[a]] -> [[b]] -> [[(a, b)]]
forall a b c. (a -> b -> c) -> [[a]] -> [[b]] -> [[c]]
productWith (,)
infixr 8 ><

-- | Take a tiered product of lists of tiers.
--   'productWith' can be defined by '><', as:
--
-- > productWith f xss yss  =  map (uncurry f) $ xss >< yss
--
-- (cf. '><')
productWith :: (a->b->c) -> [[a]] -> [[b]] -> [[c]]
productWith :: forall a b c. (a -> b -> c) -> [[a]] -> [[b]] -> [[c]]
productWith a -> b -> c
_ [[a]]
_ []  =  []
productWith a -> b -> c
_ [] [[b]]
_  =  []
productWith a -> b -> c
f ([a]
xs:[[a]]
xss) [[b]]
yss  =  ([b] -> [c]) -> [[b]] -> [[c]]
forall a b. (a -> b) -> [a] -> [b]
map ([a]
xs [a] -> [b] -> [c]
**) [[b]]
yss
                            [[c]] -> [[c]] -> [[c]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ [[c]] -> [[c]]
forall a. [[a]] -> [[a]]
delay ((a -> b -> c) -> [[a]] -> [[b]] -> [[c]]
forall a b c. (a -> b -> c) -> [[a]] -> [[b]] -> [[c]]
productWith a -> b -> c
f [[a]]
xss [[b]]
yss)
  where
  [a]
xs ** :: [a] -> [b] -> [c]
** [b]
ys  =  [a
x a -> b -> c
`f` b
y | a
x <- [a]
xs, b
y <- [b]
ys]

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

instance Testable Bool where
  resultiers :: Bool -> [[([[Char]], Bool)]]
resultiers Bool
p  =  [[([],Bool
p)]]

instance (Testable b, Show a, Listable a) => Testable (a->b) where
  resultiers :: (a -> b) -> [[([[Char]], Bool)]]
resultiers a -> b
p  =  (a -> [[([[Char]], Bool)]]) -> [[a]] -> [[([[Char]], Bool)]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT a -> [[([[Char]], Bool)]]
resultiersFor [[a]]
forall a. Listable a => [[a]]
tiers
    where
    resultiersFor :: a -> [[([[Char]], Bool)]]
resultiersFor a
x  =  ([[Char]] -> [[Char]]) -> ([[Char]], Bool) -> ([[Char]], Bool)
forall {t} {a} {b}. (t -> a) -> (t, b) -> (a, b)
mapFst (Int -> a -> [Char] -> [Char]
forall a. Show a => Int -> a -> [Char] -> [Char]
showsPrec Int
11 a
x [Char]
""[Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:) (([[Char]], Bool) -> ([[Char]], Bool))
-> [[([[Char]], Bool)]] -> [[([[Char]], Bool)]]
forall a b. (a -> b) -> [[a]] -> [[b]]
`mapT` b -> [[([[Char]], Bool)]]
forall a. Testable a => a -> [[([[Char]], Bool)]]
resultiers (a -> b
p a
x)
    mapFst :: (t -> a) -> (t, b) -> (a, b)
mapFst t -> a
f (t
x,b
y)  =  (t -> a
f t
x, b
y)

-- | 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)
-- > , ...
-- > ]
results :: Testable a => a -> [([String],Bool)]
results :: forall a. Testable a => a -> [([[Char]], Bool)]
results  =  [[([[Char]], Bool)]] -> [([[Char]], Bool)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[([[Char]], Bool)]] -> [([[Char]], Bool)])
-> (a -> [[([[Char]], Bool)]]) -> a -> [([[Char]], Bool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [[([[Char]], Bool)]]
forall a. Testable a => a -> [[([[Char]], Bool)]]
resultiers

-- | 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]"]]
counterExamples :: Testable a => Int -> a -> [[String]]
counterExamples :: forall a. Testable a => Int -> a -> [[[Char]]]
counterExamples Int
n a
p  =  [[[Char]]
as | ([[Char]]
as,Bool
False) <- Int -> [([[Char]], Bool)] -> [([[Char]], Bool)]
forall a. Int -> [a] -> [a]
take Int
n (a -> [([[Char]], Bool)]
forall a. Testable a => a -> [([[Char]], Bool)]
results a
p)]

-- | Up to a number of tests to a property,
--   returns 'Just' the first counter-example
--   or 'Nothing' if there is none.
--
-- > > counterExample 100 $ \xs -> [] `union` xs == (xs::[Int])
-- > Just ["[0,0]"]
counterExample :: Testable a => Int -> a -> Maybe [String]
counterExample :: forall a. Testable a => Int -> a -> Maybe [[Char]]
counterExample Int
n  =  [[[Char]]] -> Maybe [[Char]]
forall a. [a] -> Maybe a
listToMaybe ([[[Char]]] -> Maybe [[Char]])
-> (a -> [[[Char]]]) -> a -> Maybe [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> [[[Char]]]
forall a. Testable a => Int -> a -> [[[Char]]]
counterExamples Int
n

-- | 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"]]
witnesses :: Testable a => Int -> a -> [[String]]
witnesses :: forall a. Testable a => Int -> a -> [[[Char]]]
witnesses Int
n a
p  =  [[[Char]]
as | ([[Char]]
as,Bool
True) <- Int -> [([[Char]], Bool)] -> [([[Char]], Bool)]
forall a. Int -> [a] -> [a]
take Int
n (a -> [([[Char]], Bool)]
forall a. Testable a => a -> [([[Char]], Bool)]
results a
p)]

-- | Up to a number of tests to a property,
--   returns 'Just' the first witness
--   or 'Nothing' if there is none.
--
-- > > witness 1000 (\x -> x > 1 && x < 77 && 77 `rem` x == 0)
-- > Just ["7"]
witness :: Testable a => Int -> a -> Maybe [String]
witness :: forall a. Testable a => Int -> a -> Maybe [[Char]]
witness Int
n  =  [[[Char]]] -> Maybe [[Char]]
forall a. [a] -> Maybe a
listToMaybe ([[[Char]]] -> Maybe [[Char]])
-> (a -> [[[Char]]]) -> a -> Maybe [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> [[[Char]]]
forall a. Testable a => Int -> a -> [[[Char]]]
witnesses Int
n

-- | 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')
holds :: Testable a => Int -> a -> Bool
holds :: forall a. Testable a => Int -> a -> Bool
holds Int
n  =  [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> (a -> [Bool]) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Bool] -> [Bool]
forall a. Int -> [a] -> [a]
take Int
n ([Bool] -> [Bool]) -> (a -> [Bool]) -> a -> [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([[Char]], Bool) -> Bool) -> [([[Char]], Bool)] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ([[Char]], Bool) -> Bool
forall a b. (a, b) -> b
snd ([([[Char]], Bool)] -> [Bool])
-> (a -> [([[Char]], Bool)]) -> a -> [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [([[Char]], Bool)]
forall a. Testable a => a -> [([[Char]], Bool)]
results

-- | 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'.
fails :: Testable a => Int -> a -> Bool
fails :: forall a. Testable a => Int -> a -> Bool
fails Int
n  =  Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> Bool
forall a. Testable a => Int -> a -> Bool
holds Int
n

-- | There __exists__ an assignment of values that satisfies a property
--   up to a number of test values?
--
-- > > exists 1000 $ \x -> x > 10
-- > True
exists :: Testable a => Int -> a -> Bool
exists :: forall a. Testable a => Int -> a -> Bool
exists Int
n  =  [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> (a -> [Bool]) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Bool] -> [Bool]
forall a. Int -> [a] -> [a]
take Int
n ([Bool] -> [Bool]) -> (a -> [Bool]) -> a -> [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([[Char]], Bool) -> Bool) -> [([[Char]], Bool)] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ([[Char]], Bool) -> Bool
forall a b. (a, b) -> b
snd ([([[Char]], Bool)] -> [Bool])
-> (a -> [([[Char]], Bool)]) -> a -> [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [([[Char]], Bool)]
forall a. Testable a => a -> [([[Char]], Bool)]
results

uncurry3 :: (a->b->c->d) -> (a,b,c) -> d
uncurry3 :: forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 a -> b -> c -> d
f (a
x,b
y,c
z)  =  a -> b -> c -> d
f a
x b
y c
z

uncurry4 :: (a->b->c->d->e) -> (a,b,c,d) -> e
uncurry4 :: forall a b c d e. (a -> b -> c -> d -> e) -> (a, b, c, d) -> e
uncurry4 a -> b -> c -> d -> e
f (a
x,b
y,c
z,d
w)  =  a -> b -> c -> d -> e
f a
x b
y c
z d
w

uncurry5 :: (a->b->c->d->e->f) -> (a,b,c,d,e) -> f
uncurry5 :: forall a b c d e f.
(a -> b -> c -> d -> e -> f) -> (a, b, c, d, e) -> f
uncurry5 a -> b -> c -> d -> e -> f
f (a
x,b
y,c
z,d
w,e
v)  =  a -> b -> c -> d -> e -> f
f a
x b
y c
z d
w e
v

-- | 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.
(==>) :: Bool -> Bool -> Bool
Bool
False ==> :: Bool -> Bool -> Bool
==> Bool
_  =  Bool
True
Bool
True  ==> Bool
p  =  Bool
p
infixr 0 ==>