-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | generalize counter-examples of test properties
--
-- Extrapolate is a tool able to provide generalized counter-examples of
-- test properties where irrelevant sub-expressions are replaces with
-- variables.
--
-- For the incorrect property \xs -> nub xs == (xs::[Int]):
--
--
-- - [0,0] is a counter-example;
-- - x:x:_ is a generalized counter-example.
--
@package extrapolate
@version 0.4.4
-- | This module is part of Extrapolate, a library for generalization of
-- counter-examples.
--
-- This module re-exports functionality from Data.Express and
-- Test.Speculate.Expr along with some extra utilities.
module Test.Extrapolate.Expr
-- | Like canonicalize but uses holes for unrepeated variables.
canonicalizeUsingHoles :: Expr -> Expr
-- | Like canonicalizeWith but uses holes for unrepeated variables.
canonicalizeUsingHolesWith :: (Expr -> [String]) -> Expr -> Expr
unand :: Expr -> (Expr, Expr)
-- | O(n). Replaces the function in the given Expr.
--
--
-- replaceFun timesE (plusE :$ one :$ two) = timesE :$ one :$ two
-- replaceFun absE (idE :$ one) = absE :$ one
-- replaceFun two (one) = two
--
replaceFun :: Expr -> Expr -> Expr
-- | The function && lifted over the Expr type.
--
--
-- > pp -&&- qq
-- p && q :: Bool
--
--
--
-- > false -&&- true
-- False && True :: Bool
--
--
--
-- > evalBool $ false -&&- true
-- False
--
(-&&-) :: Expr -> Expr -> Expr
infixr 3 -&&-
-- | False encoded as an Expr.
--
--
-- > false
-- False :: Bool
--
false :: Expr
-- | This module is part of Extrapolate, a library for generalization of
-- counter-examples.
--
-- This defines utilities for unconditional generalization.
--
-- You are probably better off importing Test.Extrapolate.
module Test.Extrapolate.Generalization
-- | Given boolean expression representing a counter-example, returns all
-- possible unconditional generalizations.
--
-- If more than one generalization is returned, they are _not_ instances
-- of one another. (cf. isInstanceOf) All according to a given
-- function that lists ground expressions.
--
--
-- > counterExampleGeneralizations (groundsFor not) false
-- []
--
--
--
-- > counterExampleGeneralizations (groundsFor not) (false -&&- true)
-- [False && p :: Bool]
--
--
--
-- > counterExampleGeneralizations (groundsFor not) (false -||- true)
-- []
--
--
--
-- > counterExampleGeneralizations (groundsFor not) (false -/=- false)
-- [p /= p :: Bool]
--
--
--
-- > counterExampleGeneralizations (groundsFor not) (false -&&- true -&&- false)
-- [ (False && _) && _ :: Bool
-- , p && False :: Bool
-- ]
--
counterExampleGeneralizations :: (Expr -> [Expr]) -> Expr -> [Expr]
-- | Returns candidate generalizations for an expression. (cf.
-- candidateHoleGeneralizations)
--
-- This takes a function that returns whether to generalize a given
-- subexpression.
--
--
-- > import Data.Express.Fixtures
--
--
--
-- > candidateGeneralizations (\e -> typ e == typ one) (one -+- two)
-- [ _ :: Int
-- , _ + _ :: Int
-- , x + x :: Int
-- , _ + 2 :: Int
-- , 1 + _ :: Int
-- ]
--
--
--
-- > candidateGeneralizations (const True) (one -+- two)
-- [ _ :: Int
-- , _ _ :: Int
-- , _ _ _ :: Int
-- , _ x x :: Int
-- , _ 1 _ :: Int
-- , _ + _ :: Int
-- , x + x :: Int
-- , _ 2 :: Int
-- , _ _ 2 :: Int
-- , _ 1 2 :: Int
-- , _ + 2 :: Int
-- , 1 + _ :: Int
-- ]
--
candidateGeneralizations :: (Expr -> Bool) -> Expr -> [Expr]
-- | Like candidateGeneralizations but faster because result is not
-- canonicalized. Variable names will be repeated across different types.
fastCandidateGeneralizations :: (Expr -> Bool) -> Expr -> [Expr]
-- | Returns candidate generalizations for an expression by replacing
-- values with holes. (cf. candidateGeneralizations)
--
--
-- > import Data.Express.Fixtures
--
--
--
-- > candidateHoleGeneralizations (\e -> typ e == typ one) (one -+- two)
-- [ _ :: Int
-- , _ + _ :: Int
-- , _ + 2 :: Int
-- , 1 + _ :: Int
-- ]
--
--
--
-- > candidateHoleGeneralizations (const True) (one -+- two)
-- [ _ :: Int
-- , _ _ :: Int
-- , _ _ _ :: Int
-- , _ 1 _ :: Int
-- , _ + _ :: Int
-- , _ 2 :: Int
-- , _ _ 2 :: Int
-- , _ 1 2 :: Int
-- , _ + 2 :: Int
-- , 1 + _ :: Int
-- ]
--
candidateHoleGeneralizations :: (Expr -> Bool) -> Expr -> [Expr]
-- | This module is part of Extrapolate, a library for generalization of
-- counter-examples.
--
-- Some type binding operators that are useful when defining
-- Generalizable instances.
module Test.Extrapolate.TypeBinding
arg1 :: (a -> b) -> a
arg2 :: (a -> b -> c) -> b
arg3 :: (a -> b -> c -> d) -> c
arg4 :: (a -> b -> c -> d -> e) -> d
arg5 :: (a -> b -> c -> d -> e -> f) -> e
arg6 :: (a -> b -> c -> d -> e -> f -> g) -> f
(==:) :: (a -> b -> c -> d) -> a -> b
argTy1of1 :: con a -> a
argTy1of2 :: con a b -> a
argTy2of2 :: con a b -> b
argTy1of3 :: con a b c -> a
argTy2of3 :: con a b c -> b
argTy3of3 :: con a b c -> c
argTy1of4 :: con a b c d -> a
argTy2of4 :: con a b c d -> b
argTy3of4 :: con a b c d -> c
argTy4of4 :: con a b c d -> d
argTy1of5 :: con a b c d e -> a
argTy2of5 :: con a b c d e -> b
argTy3of5 :: con a b c d e -> c
argTy4of5 :: con a b c d e -> d
argTy5of5 :: con a b c d e -> e
argTy1of6 :: con a b c d e f -> a
argTy2of6 :: con a b c d e f -> b
argTy3of6 :: con a b c d e f -> c
argTy4of6 :: con a b c d e f -> d
argTy5of6 :: con a b c d e f -> e
argTy6of6 :: con a b c d e f -> f
-- | This module is part of Extrapolate, a library for generalization of
-- counter-examples.
--
-- Miscellaneous utility functions.
--
-- This is not intended to be used by users of Extrapolate, only by
-- modules of Extrapolate itself. Expect symbols exported here to come
-- and go with every minor version.
module Test.Extrapolate.Utils
(+++) :: Ord a => [a] -> [a] -> [a]
infixr 5 +++
nubMerge :: Ord a => [a] -> [a] -> [a]
nubMergeOn :: Ord b => (a -> b) -> [a] -> [a] -> [a]
nubMergeBy :: (a -> a -> Ordering) -> [a] -> [a] -> [a]
foldr0 :: (a -> a -> a) -> a -> [a] -> a
fromLeft :: Either a b -> a
fromRight :: Either a b -> b
elemBy :: (a -> a -> Bool) -> a -> [a] -> Bool
listEq :: (a -> a -> Bool) -> [a] -> [a] -> Bool
listOrd :: (a -> a -> Bool) -> [a] -> [a] -> Bool
maybeEq :: (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
maybeOrd :: (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool
eitherEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> Either a b -> Either a b -> Bool
eitherOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> Either a b -> Either a b -> Bool
pairEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> (a, b) -> (a, b) -> Bool
pairOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> (a, b) -> (a, b) -> Bool
tripleEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool) -> (a, b, c) -> (a, b, c) -> Bool
tripleOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool) -> (a, b, c) -> (a, b, c) -> Bool
quadrupleEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> (a, b, c, d) -> (a, b, c, d) -> Bool
quadrupleOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> (a, b, c, d) -> (a, b, c, d) -> Bool
minimumOn :: Ord b => (a -> b) -> [a] -> a
maximumOn :: Ord b => (a -> b) -> [a] -> a
takeBound :: Maybe Int -> [a] -> [a]
nubMergeMap :: Ord b => (a -> [b]) -> [a] -> [b]
compareIndex :: Eq a => [a] -> a -> a -> Ordering
-- | This module is part of Extrapolate, a library for generalization of
-- counter-examples.
--
-- This defines utilities for speculation about side conditions.
--
-- You are probably better off importing Test.Extrapolate.
module Test.Extrapolate.Speculation
theoryAndReprConds :: (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> (Thy, [Expr])
data Thy
-- | Values of type Expr represent objects or applications between
-- objects. Each object is encapsulated together with its type and string
-- representation. Values encoded in Exprs are always monomorphic.
--
-- An Expr can be constructed using:
--
--
-- - val, for values that are Show instances;
-- - value, for values that are not Show instances, like
-- functions;
-- - :$, for applications between Exprs.
--
--
--
-- > val False
-- False :: Bool
--
--
--
-- > value "not" not :$ val False
-- not False :: Bool
--
--
-- An Expr can be evaluated using evaluate, eval or
-- evl.
--
--
-- > evl $ val (1 :: Int) :: Int
-- 1
--
--
--
-- > evaluate $ val (1 :: Int) :: Maybe Bool
-- Nothing
--
--
--
-- > eval 'a' (val 'b')
-- 'b'
--
--
-- Showing a value of type Expr will return a
-- pretty-printed representation of the expression together with its
-- type.
--
--
-- > show (value "not" not :$ val False)
-- "not False :: Bool"
--
--
-- Expr is like Dynamic but has support for applications
-- and variables (:$, var).
--
-- The var underscore convention: Functions that manipulate
-- Exprs usually follow the convention where a value whose
-- String representation starts with '_' represents a
-- variable.
data Expr
classesFromSchemasAndVariables :: Thy -> [Expr] -> [Expr] -> [Class Expr]
-- | This module is part of Extrapolate, a library for generalization of
-- counter-examples.
--
-- This defines the Generalizable typeclass and utilities
-- involving it.
--
-- You are probably better off importing Test.Extrapolate.
module Test.Extrapolate.Generalizable
-- | Extrapolate can generalize counter-examples of any types that are
-- Generalizable.
--
-- Generalizable types must first be instances of
--
--
-- - Listable, so Extrapolate knows how to enumerate
-- values;
-- - Express, so Extrapolate can represent then manipulate
-- values;
-- - Name, so Extrapolate knows how to name variables.
--
--
-- There are no required functions, so we can define instances with:
--
--
-- instance Generalizable OurType
--
--
-- However, it is desirable to define both background and
-- subInstances.
--
-- The following example shows a datatype and its instance:
--
--
-- data Stack a = Stack a (Stack a) | Empty
--
--
--
-- instance Generalizable a => Generalizable (Stack a) where
-- subInstances s = instances (argTy1of1 s)
--
--
-- To declare instances it may be useful to use type binding
-- operators such as: argTy1of1, argTy1of2 and
-- argTy2of2.
--
-- Instances can be automatically derived using
-- deriveGeneralizable which will also automatically derivate
-- Listable, Express and Name when needed.
class (Listable a, Express a, Name a, Show a) => Generalizable a
-- | List of symbols allowed to appear in side-conditions. Defaults to
-- []. See value.
background :: Generalizable a => a -> [Expr]
-- | Computes a list of reified subtype instances. Defaults to id.
-- See instances.
subInstances :: Generalizable a => a -> Instances -> Instances
-- | Used in the definition of subInstances in Generalizable
-- typeclass instances.
instances :: Generalizable a => a -> Instances -> Instances
mkEq1 :: (Generalizable a, Generalizable b) => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
mkEq2 :: (Generalizable a, Generalizable b, Generalizable c) => ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
mkEq3 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool) -> [Expr]
mkEq4 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d, Generalizable e) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> (e -> e -> Bool) -> a -> a -> Bool) -> [Expr]
mkOrd1 :: (Generalizable a, Generalizable b) => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]
mkOrd2 :: (Generalizable a, Generalizable b, Generalizable c) => ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]
mkOrd3 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> a -> a -> Bool) -> [Expr]
mkOrd4 :: (Generalizable a, Generalizable b, Generalizable c, Generalizable d, Generalizable e) => ((b -> b -> Bool) -> (c -> c -> Bool) -> (d -> d -> Bool) -> (e -> e -> Bool) -> a -> a -> Bool) -> [Expr]
(*==*) :: Generalizable a => a -> a -> Bool
(*/=*) :: Generalizable a => a -> a -> Bool
(*<=*) :: Generalizable a => a -> a -> Bool
(*<*) :: Generalizable a => a -> a -> Bool
-- | 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.
class Listable a
tiers :: Listable a => [[a]]
list :: Listable a => [a]
instance Test.Extrapolate.Generalizable.Generalizable ()
instance Test.Extrapolate.Generalizable.Generalizable GHC.Types.Bool
instance Test.Extrapolate.Generalizable.Generalizable GHC.Types.Int
instance Test.Extrapolate.Generalizable.Generalizable GHC.Integer.Type.Integer
instance Test.Extrapolate.Generalizable.Generalizable GHC.Types.Char
instance Test.Extrapolate.Generalizable.Generalizable a => Test.Extrapolate.Generalizable.Generalizable (GHC.Maybe.Maybe a)
instance (Test.Extrapolate.Generalizable.Generalizable a, Test.Extrapolate.Generalizable.Generalizable b) => Test.Extrapolate.Generalizable.Generalizable (Data.Either.Either a b)
instance (Test.Extrapolate.Generalizable.Generalizable a, Test.Extrapolate.Generalizable.Generalizable b) => Test.Extrapolate.Generalizable.Generalizable (a, b)
instance (Test.Extrapolate.Generalizable.Generalizable a, Test.Extrapolate.Generalizable.Generalizable b, Test.Extrapolate.Generalizable.Generalizable c) => Test.Extrapolate.Generalizable.Generalizable (a, b, c)
instance (Test.Extrapolate.Generalizable.Generalizable a, Test.Extrapolate.Generalizable.Generalizable b, Test.Extrapolate.Generalizable.Generalizable c, Test.Extrapolate.Generalizable.Generalizable d) => Test.Extrapolate.Generalizable.Generalizable (a, b, c, d)
instance Test.Extrapolate.Generalizable.Generalizable a => Test.Extrapolate.Generalizable.Generalizable [a]
instance Test.Extrapolate.Generalizable.Generalizable GHC.Types.Ordering
instance (GHC.Real.Integral a, Test.Extrapolate.Generalizable.Generalizable a) => Test.Extrapolate.Generalizable.Generalizable (GHC.Real.Ratio a)
instance (Test.Extrapolate.Generalizable.Generalizable a, Test.Extrapolate.Generalizable.Generalizable b, Test.Extrapolate.Generalizable.Generalizable c, Test.Extrapolate.Generalizable.Generalizable d, Test.Extrapolate.Generalizable.Generalizable e) => Test.Extrapolate.Generalizable.Generalizable (a, b, c, d, e)
instance (Test.Extrapolate.Generalizable.Generalizable a, Test.Extrapolate.Generalizable.Generalizable b, Test.Extrapolate.Generalizable.Generalizable c, Test.Extrapolate.Generalizable.Generalizable d, Test.Extrapolate.Generalizable.Generalizable e, Test.Extrapolate.Generalizable.Generalizable f) => Test.Extrapolate.Generalizable.Generalizable (a, b, c, d, e, f)
instance (Test.Extrapolate.Generalizable.Generalizable a, Test.Extrapolate.Generalizable.Generalizable b, Test.Extrapolate.Generalizable.Generalizable c, Test.Extrapolate.Generalizable.Generalizable d, Test.Extrapolate.Generalizable.Generalizable e, Test.Extrapolate.Generalizable.Generalizable f, Test.Extrapolate.Generalizable.Generalizable g) => Test.Extrapolate.Generalizable.Generalizable (a, b, c, d, e, f, g)
instance (Test.Extrapolate.Generalizable.Generalizable a, Test.Extrapolate.Generalizable.Generalizable b, Test.Extrapolate.Generalizable.Generalizable c, Test.Extrapolate.Generalizable.Generalizable d, Test.Extrapolate.Generalizable.Generalizable e, Test.Extrapolate.Generalizable.Generalizable f, Test.Extrapolate.Generalizable.Generalizable g, Test.Extrapolate.Generalizable.Generalizable h) => Test.Extrapolate.Generalizable.Generalizable (a, b, c, d, e, f, g, h)
-- | This module is part of Extrapolate, a library for generalization of
-- counter-examples.
--
-- This defines the Testable typeclass and utilities involving it.
--
-- You are probably better off importing Test.Extrapolate.
module Test.Extrapolate.Testable
class Typeable a => Testable a
resultiers :: Testable a => a -> [[(Expr, Bool)]]
tinstances :: Testable a => a -> Instances
options :: Testable a => a -> Options
results :: Testable a => a -> [(Expr, Bool)]
limitedResults :: Testable a => a -> [(Expr, Bool)]
counterExample :: Testable a => a -> Maybe Expr
counterExamples :: Testable a => a -> [Expr]
data Option
MaxTests :: Int -> Option
ExtraInstances :: Instances -> Option
MaxConditionSize :: Int -> Option
data WithOption a
With :: a -> Option -> WithOption a
[property] :: WithOption a -> a
[option] :: WithOption a -> Option
testableMaxTests :: Testable a => a -> Int
testableMaxConditionSize :: Testable a => a -> Int
testableExtraInstances :: Testable a => a -> Instances
testableGrounds :: Testable a => a -> Expr -> [Expr]
testableNames :: Testable a => a -> Expr -> [String]
testableBackground :: Testable a => a -> [Expr]
testableMkEquation :: Testable a => a -> Expr -> Expr -> Expr
testableAtoms :: Testable a => a -> [[Expr]]
instance Test.Extrapolate.Testable.Testable a => Test.Extrapolate.Testable.Testable (Test.Extrapolate.Testable.WithOption a)
instance Test.Extrapolate.Testable.Testable GHC.Types.Bool
instance (Test.Extrapolate.Testable.Testable b, Test.Extrapolate.Generalizable.Generalizable a, Test.LeanCheck.Core.Listable a) => Test.Extrapolate.Testable.Testable (a -> b)
-- | This module is part of Extrapolate, a library for generalization of
-- counter-examples.
--
-- This is a module for deriving Generalizable instances.
--
-- Needs GHC and Template Haskell (tested on GHC 8.0).
--
-- If Extrapolate does not compile under later GHCs, this module is the
-- probable culprit.
module Test.Extrapolate.Generalizable.Derive
-- | Derives a Generalizable instance for a given type Name.
--
-- If needed, this function also automatically derivates Listable,
-- Express and Name instances using respectively
-- deriveListable, deriveExpress and deriveName.
--
-- Consider the following Stack datatype:
--
--
-- data Stack a = Stack a (Stack a) | Empty
--
--
-- Writing
--
--
-- deriveGeneralizable ''Stack
--
--
-- will automatically derive the following Generalizable instance:
--
--
-- instance Generalizable a => Generalizable (Stack a) where
-- instances s = this "s" s
-- $ let Stack x y = Stack undefined undefined `asTypeOf` s
-- in instances x
-- . instances y
--
--
-- This function needs the TemplateHaskell extension.
deriveGeneralizable :: Name -> DecsQ
-- | Same as deriveGeneralizable but does not warn when instance
-- already exists (deriveGeneralizable is preferable).
deriveGeneralizableIfNeeded :: Name -> DecsQ
-- | Derives a Generalizable instance for a given type Name
-- cascading derivation of type arguments as well.
deriveGeneralizableCascading :: Name -> DecsQ
-- | This module is part of Extrapolate, a library for generalization of
-- counter-examples.
--
-- This defines utilities for conditional generalization.
--
-- You are probably better off importing Test.Extrapolate.
module Test.Extrapolate.ConditionalGeneralization
conditionalCounterExampleGeneralizations :: Int -> [[Expr]] -> (Expr -> [Expr]) -> (Expr -> Expr -> Expr) -> Expr -> [Expr]
validConditions :: (Thy, [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
candidateConditions :: (Expr -> [Expr]) -> (Thy, [Expr]) -> Expr -> [Expr]
-- | This module is part of Extrapolate, a library for generalization of
-- counter-examples.
--
-- This is the core of extrapolate.
module Test.Extrapolate.Core
-- | 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]]
-- , ...
-- ]
--
listsOfLength :: Int -> [[a]] -> [[[a]]]
-- | 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
--
setsOf :: [[a]] -> [[[a]]]
-- | 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]]
-- , ...
-- ]
--
bagsOf :: [[a]] -> [[[a]]]
-- | 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]]
-- , ...
-- ]
--
noDupListsOf :: [[a]] -> [[[a]]]
-- | Normalizes tiers by removing up to 12 empty tiers from the end of a
-- list of tiers.
--
--
-- normalizeT [xs0,xs1,...,xsN,[]] = [xs0,xs1,...,xsN]
-- normalizeT [xs0,xs1,...,xsN,[],[]] = [xs0,xs1,...,xsN]
--
--
-- The arbitrary limit of 12 tiers is necessary as this function would
-- loop if there is an infinite trail of empty tiers.
normalizeT :: [[a]] -> [[a]]
-- | Delete the first occurence of an element in a tier.
--
-- For normalized lists-of-tiers without repetitions, the following
-- holds:
--
--
-- deleteT x = normalizeT . (`suchThat` (/= x))
--
deleteT :: Eq a => a -> [[a]] -> [[a]]
-- | 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
--
products :: [[[a]]] -> [[[a]]]
-- | 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]]
-- , ...
-- ]
--
listsOf :: [[a]] -> [[[a]]]
-- | Take the product of lists of tiers by a function returning a
-- Maybe value discarding Nothing values.
productMaybeWith :: (a -> b -> Maybe c) -> [[a]] -> [[b]] -> [[c]]
-- | Like productWith, but over 3 lists of tiers.
product3With :: (a -> b -> c -> d) -> [[a]] -> [[b]] -> [[c]] -> [[d]]
-- | Given a constructor that takes a list with no duplicate elements,
-- return tiers of applications of this constructor.
noDupListCons :: Listable a => ([a] -> b) -> [[b]]
-- | Given a constructor that takes a map of elements (encoded as a list),
-- lists tiers of applications of this constructor
--
-- So long as the underlying Listable enumerations have no
-- repetitions, this will generate no repetitions.
--
-- This allows defining an efficient implementation of tiers that
-- does not repeat maps given by:
--
--
-- tiers = mapCons fromList
--
mapCons :: (Listable a, Listable b) => ([(a, b)] -> c) -> [[c]]
-- | 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.
setCons :: Listable a => ([a] -> b) -> [[b]]
-- | 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
--
bagCons :: Listable a => ([a] -> b) -> [[b]]
-- | Derives a Listable instance for a given type Name
-- cascading derivation of type arguments as well.
--
-- Consider the following series of datatypes:
--
--
-- data Position = CEO | Manager | Programmer
--
-- data Person = Person
-- { name :: String
-- , age :: Int
-- , position :: Position
-- }
--
-- data Company = Company
-- { name :: String
-- , employees :: [Person]
-- }
--
--
-- Writing
--
--
-- deriveListableCascading ''Company
--
--
-- will automatically derive the following three Listable
-- instances:
--
--
-- instance Listable Position where
-- tiers = cons0 CEO \/ cons0 Manager \/ cons0 Programmer
--
-- instance Listable Person where
-- tiers = cons3 Person
--
-- instance Listable Company where
-- tiers = cons2 Company
--
deriveListableCascading :: Name -> DecsQ
-- | 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
--
--
-- Warning: if the values in your type need to follow a data
-- invariant, the derived instance won't respect it. Use this only on
-- "free" datatypes.
--
-- Needs the TemplateHaskell extension.
deriveListable :: Name -> DecsQ
-- | Adds to the weight of a constructor or tiers.
--
--
-- instance Listable <Type> where
-- tiers = ...
-- \/ cons<N> <Cons> `addWeight` <W>
-- \/ ...
--
--
-- Typically used as an infix operator when defining Listable
-- instances:
--
--
-- > [ xs, ys, zs, ... ] `addWeight` 1
-- [ [], xs, ys, zs, ... ]
--
--
--
-- > [ xs, ys, zs, ... ] `addWeight` 2
-- [ [], [], xs, ys, zs, ... ]
--
--
--
-- > [ [], xs, ys, zs, ... ] `addWeight` 3
-- [ [], [], [], [], xs, ys, zs, ... ]
--
--
-- `addWeight` n is equivalent to n
-- applications of delay.
addWeight :: [[a]] -> Int -> [[a]]
-- | Resets the weight of a constructor or tiers.
--
--
-- > [ [], [], ..., xs, ys, zs, ... ] `ofWeight` 1
-- [ [], xs, ys, zs, ... ]
--
--
--
-- > [ xs, ys, zs, ... ] `ofWeight` 2
-- [ [], [], xs, ys, zs, ... ]
--
--
--
-- > [ [], xs, ys, zs, ... ] `ofWeight` 3
-- [ [], [], [], xs, ys, zs, ... ]
--
--
-- Typically used as an infix operator when defining Listable
-- instances:
--
--
-- instance Listable <Type> where
-- tiers = ...
-- \/ cons<N> <Cons> `ofWeight` <W>
-- \/ ...
--
--
-- Warning: do not apply `ofWeight` 0 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` n is equivalent to reset followed
-- by n applications of delay.
ofWeight :: [[a]] -> Int -> [[a]]
-- | Returns tiers of applications of a 12-argument constructor.
cons12 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g, Listable h, Listable i, Listable j, Listable k, Listable l) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> [[m]]
-- | Returns tiers of applications of a 11-argument constructor.
cons11 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g, Listable h, Listable i, Listable j, Listable k) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> [[l]]
-- | Returns tiers of applications of a 10-argument constructor.
cons10 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g, Listable h, Listable i, Listable j) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> [[k]]
-- | Returns tiers of applications of a 9-argument constructor.
cons9 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g, Listable h, Listable i) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> [[j]]
-- | Returns tiers of applications of a 8-argument constructor.
cons8 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g, Listable h) => (a -> b -> c -> d -> e -> f -> g -> h -> i) -> [[i]]
-- | Returns tiers of applications of a 7-argument constructor.
cons7 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g) => (a -> b -> c -> d -> e -> f -> g -> h) -> [[h]]
-- | Returns tiers of applications of a 6-argument constructor.
cons6 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f) => (a -> b -> c -> d -> e -> f -> g) -> [[g]]
-- | 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
infixr 0 ==>
-- | 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
-- | 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
-- | 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
-- | 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]
-- | 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]]
-- | 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)]]
infixr 8 ><
-- | 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]]
infixr 7 \\//
-- | Append tiers --- sum of two tiers enumerations.
--
--
-- [xs,ys,zs,...] \/ [as,bs,cs,...] = [xs++as, ys++bs, zs++cs, ...]
--
(\/) :: [[a]] -> [[a]] -> [[a]]
infixr 7 \/
-- | 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]
infixr 5 +|
-- | 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 flipped version of filterT.
suchThat :: [[a]] -> (a -> Bool) -> [[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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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: 10 and -10.
--
--
-- 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.
tiersFloating :: Fractional a => [[a]]
-- | 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]
-- , ...
-- ]
--
tiersFractional :: Fractional a => [[a]]
-- | 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.
listIntegral :: (Ord a, Num a) => [a]
-- | 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]]
-- | 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.
class Listable a
tiers :: Listable a => [[a]]
list :: Listable a => [a]
counterExampleWithGeneralizations :: Testable a => a -> Maybe (Expr, [Expr])
-- | This module is part of Extrapolate, a library for generalization of
-- counter-examples.
--
-- QuickCheck-like interface.
module Test.Extrapolate.IO
-- | Checks a property printing results on stdout
--
--
-- > check $ \xs -> sort (sort xs) == sort (xs::[Int])
-- +++ OK, passed 360 tests.
--
-- > check $ \xs ys -> xs `union` ys == ys `union` (xs::[Int])
-- *** Failed! Falsifiable (after 4 tests):
-- [] [0,0]
--
-- Generalization:
-- [] (x:x:_)
--
check :: Testable a => a -> IO ()
-- | Check a property printing results on stdout and returning
-- True on success.
--
-- There is no option to silence this function: for silence, you should
-- use holds.
checkResult :: Testable a => a -> IO Bool
-- | Use for to configure the number of tests performed by
-- check.
--
--
-- > check `for` 10080 $ \xs -> sort (sort xs) == sort (xs :: [Int])
-- +++ OK, passed 10080 tests.
--
--
-- Don't forget the dollar ($)!
for :: Testable a => (WithOption a -> b) -> Int -> a -> b
-- | Allows the user to customize instance information available when
-- generalized. (For advanced users.)
withInstances :: Testable a => (WithOption a -> b) -> Instances -> a -> b
-- | Use withBackground to provide additional functions to
-- appear in side-conditions.
--
--
-- check `withBackground` [value "isSpace" isSpace] $ \xs -> unwords (words xs) == xs
-- *** Failed! Falsifiable (after 4 tests):
-- " "
--
-- Generalization:
-- ' ':_
--
-- Conditional Generalization:
-- c:_ when isSpace c
--
withBackground :: Testable a => (WithOption a -> b) -> [Expr] -> a -> b
-- | Use withConditionSize to configure the maximum
-- condition size allowed.
withConditionSize :: Testable a => (WithOption a -> b) -> Int -> a -> b
instance GHC.Show.Show Test.Extrapolate.IO.Result
instance GHC.Classes.Eq Test.Extrapolate.IO.Result
-- | Extrapolate is a property-based testing library capable of reporting
-- generalized counter-examples.
--
-- Consider the following faulty implementation of sort:
--
--
-- sort :: Ord a => [a] -> [a]
-- sort [] = []
-- sort (x:xs) = sort (filter (< x) xs)
-- ++ [x]
-- ++ sort (filter (> x) xs)
--
--
-- When tests pass, Extrapolate works like a regular property-based
-- testing library. See:
--
--
-- > check $ \xs -> sort (sort xs :: [Int]) == sort xs
-- +++ OK, passed 500 tests.
--
--
-- When tests fail, Extrapolate reports a fully defined counter-example
-- and a generalization of failing inputs. See:
--
--
-- > check $ \xs -> length (sort xs :: [Int]) == length xs
-- *** Failed! Falsifiable (after 3 tests):
-- [0,0]
--
-- Generalization:
-- x:x:_
--
-- Conditional Generalization:
-- x:xs when elem x xs
--
--
-- Generalization: the property fails for any integer x
-- and for any list _ at the tail.
--
-- Conditional Generalization: the property fails for a list
-- x:xs whenever x is an element of xs
--
-- This hints at the actual source of the fault: our sort above
-- discards repeated elements!
module Test.Extrapolate
-- | Checks a property printing results on stdout
--
--
-- > check $ \xs -> sort (sort xs) == sort (xs::[Int])
-- +++ OK, passed 360 tests.
--
-- > check $ \xs ys -> xs `union` ys == ys `union` (xs::[Int])
-- *** Failed! Falsifiable (after 4 tests):
-- [] [0,0]
--
-- Generalization:
-- [] (x:x:_)
--
check :: Testable a => a -> IO ()
-- | Check a property printing results on stdout and returning
-- True on success.
--
-- There is no option to silence this function: for silence, you should
-- use holds.
checkResult :: Testable a => a -> IO Bool
-- | Use for to configure the number of tests performed by
-- check.
--
--
-- > check `for` 10080 $ \xs -> sort (sort xs) == sort (xs :: [Int])
-- +++ OK, passed 10080 tests.
--
--
-- Don't forget the dollar ($)!
for :: Testable a => (WithOption a -> b) -> Int -> a -> b
-- | Use withBackground to provide additional functions to
-- appear in side-conditions.
--
--
-- check `withBackground` [value "isSpace" isSpace] $ \xs -> unwords (words xs) == xs
-- *** Failed! Falsifiable (after 4 tests):
-- " "
--
-- Generalization:
-- ' ':_
--
-- Conditional Generalization:
-- c:_ when isSpace c
--
withBackground :: Testable a => (WithOption a -> b) -> [Expr] -> a -> b
-- | Use withConditionSize to configure the maximum
-- condition size allowed.
withConditionSize :: Testable a => (WithOption a -> b) -> Int -> a -> b
-- | Extrapolate can generalize counter-examples of any types that are
-- Generalizable.
--
-- Generalizable types must first be instances of
--
--
-- - Listable, so Extrapolate knows how to enumerate
-- values;
-- - Express, so Extrapolate can represent then manipulate
-- values;
-- - Name, so Extrapolate knows how to name variables.
--
--
-- There are no required functions, so we can define instances with:
--
--
-- instance Generalizable OurType
--
--
-- However, it is desirable to define both background and
-- subInstances.
--
-- The following example shows a datatype and its instance:
--
--
-- data Stack a = Stack a (Stack a) | Empty
--
--
--
-- instance Generalizable a => Generalizable (Stack a) where
-- subInstances s = instances (argTy1of1 s)
--
--
-- To declare instances it may be useful to use type binding
-- operators such as: argTy1of1, argTy1of2 and
-- argTy2of2.
--
-- Instances can be automatically derived using
-- deriveGeneralizable which will also automatically derivate
-- Listable, Express and Name when needed.
class (Listable a, Express a, Name a, Show a) => Generalizable a
-- | List of symbols allowed to appear in side-conditions. Defaults to
-- []. See value.
background :: Generalizable a => a -> [Expr]
-- | Computes a list of reified subtype instances. Defaults to id.
-- See instances.
subInstances :: Generalizable a => a -> Instances -> Instances
-- | Used in the definition of subInstances in Generalizable
-- typeclass instances.
instances :: Generalizable a => a -> Instances -> Instances
-- | Values of type Expr represent objects or applications between
-- objects. Each object is encapsulated together with its type and string
-- representation. Values encoded in Exprs are always monomorphic.
--
-- An Expr can be constructed using:
--
--
-- - val, for values that are Show instances;
-- - value, for values that are not Show instances, like
-- functions;
-- - :$, for applications between Exprs.
--
--
--
-- > val False
-- False :: Bool
--
--
--
-- > value "not" not :$ val False
-- not False :: Bool
--
--
-- An Expr can be evaluated using evaluate, eval or
-- evl.
--
--
-- > evl $ val (1 :: Int) :: Int
-- 1
--
--
--
-- > evaluate $ val (1 :: Int) :: Maybe Bool
-- Nothing
--
--
--
-- > eval 'a' (val 'b')
-- 'b'
--
--
-- Showing a value of type Expr will return a
-- pretty-printed representation of the expression together with its
-- type.
--
--
-- > show (value "not" not :$ val False)
-- "not False :: Bool"
--
--
-- Expr is like Dynamic but has support for applications
-- and variables (:$, var).
--
-- The var underscore convention: Functions that manipulate
-- Exprs usually follow the convention where a value whose
-- String representation starts with '_' represents a
-- variable.
data Expr
-- | a value enconded as String and Dynamic
Value :: String -> Dynamic -> Expr
-- | function application between expressions
(:$) :: Expr -> Expr -> Expr
-- | O(1). It takes a string representation of a value and a value,
-- returning an Expr with that terminal value. For instances of
-- Show, it is preferable to use val.
--
--
-- > value "0" (0 :: Integer)
-- 0 :: Integer
--
--
--
-- > value "'a'" 'a'
-- 'a' :: Char
--
--
--
-- > value "True" True
-- True :: Bool
--
--
--
-- > value "id" (id :: Int -> Int)
-- id :: Int -> Int
--
--
--
-- > value "(+)" ((+) :: Int -> Int -> Int)
-- (+) :: Int -> Int -> Int
--
--
--
-- > value "sort" (sort :: [Bool] -> [Bool])
-- sort :: [Bool] -> [Bool]
--
value :: Typeable a => String -> a -> Expr
-- | O(1). A shorthand for value for values that are
-- Show instances.
--
--
-- > val (0 :: Int)
-- 0 :: Int
--
--
--
-- > val 'a'
-- 'a' :: Char
--
--
--
-- > val True
-- True :: Bool
--
--
-- Example equivalences to value:
--
--
-- val 0 = value "0" 0
-- val 'a' = value "'a'" 'a'
-- val True = value "True" True
--
val :: (Typeable a, Show a) => a -> Expr
-- | O(1). Reifies an Eq instance into a list of
-- Exprs. The list will contain == and /= for the
-- given type. (cf. mkEq, mkEquation)
--
--
-- > reifyEq (undefined :: Int)
-- [ (==) :: Int -> Int -> Bool
-- , (/=) :: Int -> Int -> Bool ]
--
--
--
-- > reifyEq (undefined :: Bool)
-- [ (==) :: Bool -> Bool -> Bool
-- , (/=) :: Bool -> Bool -> Bool ]
--
--
--
-- > reifyEq (undefined :: String)
-- [ (==) :: [Char] -> [Char] -> Bool
-- , (/=) :: [Char] -> [Char] -> Bool ]
--
reifyEq :: (Typeable a, Eq a) => a -> [Expr]
-- | O(1). Reifies an Ord instance into a list of
-- Exprs. The list will contain compare, <= and
-- < for the given type. (cf. mkOrd,
-- mkOrdLessEqual, mkComparisonLE, mkComparisonLT)
--
--
-- > reifyOrd (undefined :: Int)
-- [ (<=) :: Int -> Int -> Bool
-- , (<) :: Int -> Int -> Bool ]
--
--
--
-- > reifyOrd (undefined :: Bool)
-- [ (<=) :: Bool -> Bool -> Bool
-- , (<) :: Bool -> Bool -> Bool ]
--
--
--
-- > reifyOrd (undefined :: [Bool])
-- [ (<=) :: [Bool] -> [Bool] -> Bool
-- , (<) :: [Bool] -> [Bool] -> Bool ]
--
reifyOrd :: (Typeable a, Ord a) => a -> [Expr]
-- | O(1). Reifies Eq and Ord instances into a list of
-- Expr.
reifyEqOrd :: (Typeable a, Ord a) => a -> [Expr]
class Typeable a => Testable a
-- | Derives a Generalizable instance for a given type Name.
--
-- If needed, this function also automatically derivates Listable,
-- Express and Name instances using respectively
-- deriveListable, deriveExpress and deriveName.
--
-- Consider the following Stack datatype:
--
--
-- data Stack a = Stack a (Stack a) | Empty
--
--
-- Writing
--
--
-- deriveGeneralizable ''Stack
--
--
-- will automatically derive the following Generalizable instance:
--
--
-- instance Generalizable a => Generalizable (Stack a) where
-- instances s = this "s" s
-- $ let Stack x y = Stack undefined undefined `asTypeOf` s
-- in instances x
-- . instances y
--
--
-- This function needs the TemplateHaskell extension.
deriveGeneralizable :: Name -> DecsQ
-- | Same as deriveGeneralizable but does not warn when instance
-- already exists (deriveGeneralizable is preferable).
deriveGeneralizableIfNeeded :: Name -> DecsQ
-- | Derives a Generalizable instance for a given type Name
-- cascading derivation of type arguments as well.
deriveGeneralizableCascading :: Name -> DecsQ
-- | If we were to come up with a variable name for the given type what
-- name would it be?
--
-- An instance for a given type Ty is simply given by:
--
--
-- instance Name Ty where name _ = "x"
--
--
-- Examples:
--
--
-- > name (undefined :: Int)
-- "x"
--
--
--
-- > name (undefined :: Bool)
-- "p"
--
--
--
-- > name (undefined :: [Int])
-- "xs"
--
--
-- This is then used to generate an infinite list of variable
-- names:
--
--
-- > names (undefined :: Int)
-- ["x", "y", "z", "x'", "y'", "z'", "x''", "y''", "z''", ...]
--
--
--
-- > names (undefined :: Bool)
-- ["p", "q", "r", "p'", "q'", "r'", "p''", "q''", "r''", ...]
--
--
--
-- > names (undefined :: [Int])
-- ["xs", "ys", "zs", "xs'", "ys'", "zs'", "xs''", "ys''", ...]
--
class Name a
-- | O(1).
--
-- Returns a name for a variable of the given argument's type.
--
--
-- > name (undefined :: Int)
-- "x"
--
--
--
-- > name (undefined :: [Bool])
-- "ps"
--
--
--
-- > name (undefined :: [Maybe Integer])
-- "mxs"
--
--
-- The default definition is:
--
--
-- name _ = "x"
--
name :: Name a => a -> String
-- | Express typeclass instances provide an expr function
-- that allows values to be deeply encoded as applications of
-- Exprs.
--
--
-- expr False = val False
-- expr (Just True) = value "Just" (Just :: Bool -> Maybe Bool) :$ val True
--
--
-- The function expr can be contrasted with the function
-- val:
--
--
-- - val always encodes values as atomic Value
-- Exprs -- shallow encoding.
-- - expr ideally encodes expressions as applications
-- (:$) between Value Exprs -- deep encoding.
--
--
-- Depending on the situation, one or the other may be desirable.
--
-- Instances can be automatically derived using the TH function
-- deriveExpress.
--
-- The following example shows a datatype and its instance:
--
--
-- data Stack a = Stack a (Stack a) | Empty
--
--
--
-- instance Express a => Express (Stack a) where
-- expr s@(Stack x y) = value "Stack" (Stack ->>: s) :$ expr x :$ expr y
-- expr s@Empty = value "Empty" (Empty -: s)
--
--
-- To declare expr it may be useful to use auxiliary type binding
-- operators: -:, ->:, ->>:,
-- ->>>:, ->>>>:,
-- ->>>>>:, ...
--
-- For types with atomic values, just declare expr = val
class Typeable a => Express a
expr :: Express a => a -> Expr
-- | 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]]
-- , ...
-- ]
--
listsOfLength :: Int -> [[a]] -> [[[a]]]
-- | 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
--
setsOf :: [[a]] -> [[[a]]]
-- | 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]]
-- , ...
-- ]
--
bagsOf :: [[a]] -> [[[a]]]
-- | 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]]
-- , ...
-- ]
--
noDupListsOf :: [[a]] -> [[[a]]]
-- | Normalizes tiers by removing up to 12 empty tiers from the end of a
-- list of tiers.
--
--
-- normalizeT [xs0,xs1,...,xsN,[]] = [xs0,xs1,...,xsN]
-- normalizeT [xs0,xs1,...,xsN,[],[]] = [xs0,xs1,...,xsN]
--
--
-- The arbitrary limit of 12 tiers is necessary as this function would
-- loop if there is an infinite trail of empty tiers.
normalizeT :: [[a]] -> [[a]]
-- | Delete the first occurence of an element in a tier.
--
-- For normalized lists-of-tiers without repetitions, the following
-- holds:
--
--
-- deleteT x = normalizeT . (`suchThat` (/= x))
--
deleteT :: Eq a => a -> [[a]] -> [[a]]
-- | 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
--
products :: [[[a]]] -> [[[a]]]
-- | 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]]
-- , ...
-- ]
--
listsOf :: [[a]] -> [[[a]]]
-- | Take the product of lists of tiers by a function returning a
-- Maybe value discarding Nothing values.
productMaybeWith :: (a -> b -> Maybe c) -> [[a]] -> [[b]] -> [[c]]
-- | Like productWith, but over 3 lists of tiers.
product3With :: (a -> b -> c -> d) -> [[a]] -> [[b]] -> [[c]] -> [[d]]
-- | Given a constructor that takes a list with no duplicate elements,
-- return tiers of applications of this constructor.
noDupListCons :: Listable a => ([a] -> b) -> [[b]]
-- | Given a constructor that takes a map of elements (encoded as a list),
-- lists tiers of applications of this constructor
--
-- So long as the underlying Listable enumerations have no
-- repetitions, this will generate no repetitions.
--
-- This allows defining an efficient implementation of tiers that
-- does not repeat maps given by:
--
--
-- tiers = mapCons fromList
--
mapCons :: (Listable a, Listable b) => ([(a, b)] -> c) -> [[c]]
-- | 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.
setCons :: Listable a => ([a] -> b) -> [[b]]
-- | 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
--
bagCons :: Listable a => ([a] -> b) -> [[b]]
-- | Derives a Listable instance for a given type Name
-- cascading derivation of type arguments as well.
--
-- Consider the following series of datatypes:
--
--
-- data Position = CEO | Manager | Programmer
--
-- data Person = Person
-- { name :: String
-- , age :: Int
-- , position :: Position
-- }
--
-- data Company = Company
-- { name :: String
-- , employees :: [Person]
-- }
--
--
-- Writing
--
--
-- deriveListableCascading ''Company
--
--
-- will automatically derive the following three Listable
-- instances:
--
--
-- instance Listable Position where
-- tiers = cons0 CEO \/ cons0 Manager \/ cons0 Programmer
--
-- instance Listable Person where
-- tiers = cons3 Person
--
-- instance Listable Company where
-- tiers = cons2 Company
--
deriveListableCascading :: Name -> DecsQ
-- | 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
--
--
-- Warning: if the values in your type need to follow a data
-- invariant, the derived instance won't respect it. Use this only on
-- "free" datatypes.
--
-- Needs the TemplateHaskell extension.
deriveListable :: Name -> DecsQ
-- | Adds to the weight of a constructor or tiers.
--
--
-- instance Listable <Type> where
-- tiers = ...
-- \/ cons<N> <Cons> `addWeight` <W>
-- \/ ...
--
--
-- Typically used as an infix operator when defining Listable
-- instances:
--
--
-- > [ xs, ys, zs, ... ] `addWeight` 1
-- [ [], xs, ys, zs, ... ]
--
--
--
-- > [ xs, ys, zs, ... ] `addWeight` 2
-- [ [], [], xs, ys, zs, ... ]
--
--
--
-- > [ [], xs, ys, zs, ... ] `addWeight` 3
-- [ [], [], [], [], xs, ys, zs, ... ]
--
--
-- `addWeight` n is equivalent to n
-- applications of delay.
addWeight :: [[a]] -> Int -> [[a]]
-- | Resets the weight of a constructor or tiers.
--
--
-- > [ [], [], ..., xs, ys, zs, ... ] `ofWeight` 1
-- [ [], xs, ys, zs, ... ]
--
--
--
-- > [ xs, ys, zs, ... ] `ofWeight` 2
-- [ [], [], xs, ys, zs, ... ]
--
--
--
-- > [ [], xs, ys, zs, ... ] `ofWeight` 3
-- [ [], [], [], xs, ys, zs, ... ]
--
--
-- Typically used as an infix operator when defining Listable
-- instances:
--
--
-- instance Listable <Type> where
-- tiers = ...
-- \/ cons<N> <Cons> `ofWeight` <W>
-- \/ ...
--
--
-- Warning: do not apply `ofWeight` 0 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` n is equivalent to reset followed
-- by n applications of delay.
ofWeight :: [[a]] -> Int -> [[a]]
-- | Returns tiers of applications of a 12-argument constructor.
cons12 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g, Listable h, Listable i, Listable j, Listable k, Listable l) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> [[m]]
-- | Returns tiers of applications of a 11-argument constructor.
cons11 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g, Listable h, Listable i, Listable j, Listable k) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> [[l]]
-- | Returns tiers of applications of a 10-argument constructor.
cons10 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g, Listable h, Listable i, Listable j) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> [[k]]
-- | Returns tiers of applications of a 9-argument constructor.
cons9 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g, Listable h, Listable i) => (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> [[j]]
-- | Returns tiers of applications of a 8-argument constructor.
cons8 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g, Listable h) => (a -> b -> c -> d -> e -> f -> g -> h -> i) -> [[i]]
-- | Returns tiers of applications of a 7-argument constructor.
cons7 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g) => (a -> b -> c -> d -> e -> f -> g -> h) -> [[h]]
-- | Returns tiers of applications of a 6-argument constructor.
cons6 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f) => (a -> b -> c -> d -> e -> f -> g) -> [[g]]
-- | 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
infixr 0 ==>
-- | 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
-- | 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
-- | 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
-- | 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]
-- | 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]]
-- | 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)]]
infixr 8 ><
-- | 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]]
infixr 7 \\//
-- | Append tiers --- sum of two tiers enumerations.
--
--
-- [xs,ys,zs,...] \/ [as,bs,cs,...] = [xs++as, ys++bs, zs++cs, ...]
--
(\/) :: [[a]] -> [[a]] -> [[a]]
infixr 7 \/
-- | 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]
infixr 5 +|
-- | 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 flipped version of filterT.
suchThat :: [[a]] -> (a -> Bool) -> [[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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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]]
-- | 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: 10 and -10.
--
--
-- 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.
tiersFloating :: Fractional a => [[a]]
-- | 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]
-- , ...
-- ]
--
tiersFractional :: Fractional a => [[a]]
-- | 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.
listIntegral :: (Ord a, Num a) => [a]
-- | 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]]
-- | 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.
class Listable a
tiers :: Listable a => [[a]]
list :: Listable a => [a]