-- 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]): -- --
-- typesIn (typeOf (undefined :: (Int -> Int) -> Int -> Bool)) -- == [Bool,Int] --typesIn :: TypeRep -> [TypeRep] argumentTy :: TypeRep -> TypeRep resultTy :: TypeRep -> TypeRep discard :: (a -> Bool) -> [a] -> [a] compareIndex :: Eq a => [a] -> a -> a -> Ordering (.:) :: (c -> d) -> (a -> b -> c) -> (a -> b -> d) -- | 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. 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 ---- -- Needs the TemplateHaskell extension. deriveListable :: Name -> DecsQ -- | Adds to the weight of tiers of a constructor -- -- addWeight is closely related to delay. addWeight :: () => [[a]] -> Int -> [[a]] -- | Resets the weight of a constructor (or tiers) Typically used as an -- infix constructor when defining Listable instances: -- --
-- cons<N> `ofWeight` <W> ---- -- Be careful: do not apply 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 is closely related to reset. ofWeight :: () => [[a]] -> Int -> [[a]] 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]] 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]] 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]] 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]] 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]] cons7 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g) => a -> b -> c -> d -> e -> f -> g -> h -> [[h]] 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 --(==>) :: 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 --exists :: Testable a => Int -> a -> Bool -- | Does a property fail for a number of test values? -- --
-- fails 1000 $ \xs -> xs ++ ys == ys ++ xs --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 --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 :: Testable a => Int -> a -> Maybe [String] -- | Lists all witnesses up to a number of tests to a property, 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)] -- ... -- ] --(><) :: () => [[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 -- --
-- cons<N> `suchThat` condition --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. Typically used when defining Listable instances: -- --
-- reset (cons<N> <Constr>) ---- -- 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. Typically used when defining -- Listable instances: -- --
-- delay (cons<N> <Constr>) --delay :: () => [[a]] -> [[a]] -- | Returns tiers of applications of a 5-argument constructor. -- -- Test.LeanCheck.Basic defines cons6 up to cons12. -- Those are exported by default from Test.LeanCheck, but are -- hidden from the Haddock documentation. 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. cons4 :: (Listable a, Listable b, Listable c, Listable d) => a -> b -> c -> d -> e -> [[e]] -- | Returns tiers of applications of a 3-argument 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. 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. 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. cons0 :: () => a -> [[a]] -- | concatMap over tiers concatMapT :: () => a -> [[b]] -> [[a]] -> [[b]] -- | concat tiers of tiers concatT :: () => [[[[a]]]] -> [[a]] -- | filter tiers filterT :: () => a -> Bool -> [[a]] -> [[a]] -- | map over tiers mapT :: () => a -> b -> [[a]] -> [[b]] -- | Tiers of Fractional values. This can be used as the -- implementation of tiers for Fractional types. tiersFractional :: Fractional a => [[a]] -- | Tiers of Integral values. Can be used as a default -- implementation of list for Integral types. listIntegral :: (Enum 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. -- -- 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. -- -- 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] -- | Extrapolate can generalize counter-examples of any types that are -- Generalizable. -- -- The core (and only required functions) of the generalizable typeclass -- are the expr and instances functions. -- -- The following example shows a datatype and its instance: -- --
-- data Stack a = Stack a (Stack a) | Empty ---- --
-- instance Generalizable a => Generalizable (Stack a) where -- name _ = "s" -- expr s@(Stack x y) = constant "Stack" (Stack ->>: s) :$ expr x :$ expr y -- expr s@Empty = constant "Empty" (Empty -: s) -- instances s = this s $ instances (argTy1of1 s) ---- -- To declare instances and expr it may be useful to use: -- --
-- [0,1] `matchList` [x,y] = Just [x=0, y=1] -- [0,1+2] `matchList` [x,y+y] = Nothing --matchList :: [Expr] -> [Expr] -> Maybe Binds newMatches :: [Expr] -> [Expr] -> Maybe Binds class Testable a resultiers :: Testable a => a -> [[([Expr], Bool)]] ($-|) :: Testable a => a -> [Expr] -> Bool tinstances :: Testable a => a -> Instances options :: Testable a => a -> Options results :: Testable a => a -> [([Expr], Bool)] areInstancesOf :: [Expr] -> [Expr] -> Bool instance GHC.Show.Show Test.Extrapolate.Core.Option instance Test.Extrapolate.Core.Testable a => Test.Extrapolate.Core.Testable (Test.Extrapolate.Core.WithOption a) instance Test.Extrapolate.Core.Testable GHC.Types.Bool instance (Test.Extrapolate.Core.Testable b, Test.Extrapolate.Core.Generalizable a, Test.LeanCheck.Core.Listable a) => Test.Extrapolate.Core.Testable (a -> b) instance Test.Extrapolate.Core.Generalizable () instance Test.Extrapolate.Core.Generalizable GHC.Types.Bool instance Test.Extrapolate.Core.Generalizable GHC.Types.Int instance Test.Extrapolate.Core.Generalizable GHC.Integer.Type.Integer instance Test.Extrapolate.Core.Generalizable GHC.Types.Char instance Test.Extrapolate.Core.Generalizable a => Test.Extrapolate.Core.Generalizable (GHC.Base.Maybe a) instance (Test.Extrapolate.Core.Generalizable a, Test.Extrapolate.Core.Generalizable b) => Test.Extrapolate.Core.Generalizable (Data.Either.Either a b) instance (Test.Extrapolate.Core.Generalizable a, Test.Extrapolate.Core.Generalizable b) => Test.Extrapolate.Core.Generalizable (a, b) instance (Test.Extrapolate.Core.Generalizable a, Test.Extrapolate.Core.Generalizable b, Test.Extrapolate.Core.Generalizable c) => Test.Extrapolate.Core.Generalizable (a, b, c) instance (Test.Extrapolate.Core.Generalizable a, Test.Extrapolate.Core.Generalizable b, Test.Extrapolate.Core.Generalizable c, Test.Extrapolate.Core.Generalizable d) => Test.Extrapolate.Core.Generalizable (a, b, c, d) instance Test.Extrapolate.Core.Generalizable a => Test.Extrapolate.Core.Generalizable [a] instance Test.Extrapolate.Core.Generalizable GHC.Types.Ordering -- | This module is otherwise unused in the code. -- -- This is a stub of a new algorithm that is smarter and generalizes from -- several initial counter-examples rather than just one. -- -- When this gets finished, it should be moved into -- Test.Extrapolate.Core. module Test.Extrapolate.New generalizedCounterExamples :: Testable a => Int -> a -> [Exprs] lgg :: Exprs -> Exprs -> Exprs -- | Computes the least general generalization of two expressions -- --
-- lgg1 (expr [0,0]) (expr [1,1]) ---- --
-- > 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` [constant "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 -- | Use minFailures to configure the minimum number of -- failures for a conditional generalization in function of the maximum -- number of tests. -- -- To set that conditional generalizations should fail for 10% of cases: -- > check minFailures (div 10) $ prop -- -- To set that conditional generalizations should fail for 5% of cases: -- > check minFailures (div 20) $ prop minFailures :: Testable a => (WithOption a -> b) -> Ratio Int -> a -> b maxSpeculateSize :: Testable a => (WithOption a -> b) -> Maybe Int -> a -> b conditionBound :: Testable a => (WithOption a -> b) -> Maybe Int -> a -> b -- | Configures a bound on the number of constants allowed in expressions -- that are considered when testing for equality in Speculate. -- -- Defaults to 2. constantBound :: Testable a => (WithOption a -> b) -> Maybe Int -> a -> b -- | Configures a bound on the depth of expressions that are considered -- when testing for equality in Speculate. -- -- Default to 3. depthBound :: Testable a => (WithOption a -> b) -> Maybe Int -> a -> b instance GHC.Show.Show Test.Extrapolate.IO.Result instance GHC.Classes.Eq Test.Extrapolate.IO.Result -- | 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.Derive -- | Derives a Generalizable instance for a given type Name. -- -- 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 -- expr s@(Stack x y) = constant "Stack" (Stack ->>: s) :$ expr x :$ expr y -- expr s@Empty = constant "Empty" (Empty -: s) -- 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 instance GHC.Show.Show Test.Extrapolate.Derive.Bla instance GHC.Classes.Ord Test.Extrapolate.Derive.Bla instance GHC.Classes.Eq Test.Extrapolate.Derive.Bla -- | This module is part of Extrapolate, a library for generalization of -- counter-examples. -- -- This provides the basic functionality of extrapolate. You will have -- better luck importing Test.Extrapolate directly. module Test.Extrapolate.Basic instance (GHC.Real.Integral a, Test.Extrapolate.Core.Generalizable a) => Test.Extrapolate.Core.Generalizable (GHC.Real.Ratio a) instance (Test.Extrapolate.Core.Generalizable a, Test.Extrapolate.Core.Generalizable b, Test.Extrapolate.Core.Generalizable c, Test.Extrapolate.Core.Generalizable d, Test.Extrapolate.Core.Generalizable e) => Test.Extrapolate.Core.Generalizable (a, b, c, d, e) instance (Test.Extrapolate.Core.Generalizable a, Test.Extrapolate.Core.Generalizable b, Test.Extrapolate.Core.Generalizable c, Test.Extrapolate.Core.Generalizable d, Test.Extrapolate.Core.Generalizable e, Test.Extrapolate.Core.Generalizable f) => Test.Extrapolate.Core.Generalizable (a, b, c, d, e, f) instance (Test.Extrapolate.Core.Generalizable a, Test.Extrapolate.Core.Generalizable b, Test.Extrapolate.Core.Generalizable c, Test.Extrapolate.Core.Generalizable d, Test.Extrapolate.Core.Generalizable e, Test.Extrapolate.Core.Generalizable f, Test.Extrapolate.Core.Generalizable g) => Test.Extrapolate.Core.Generalizable (a, b, c, d, e, f, g) instance (Test.Extrapolate.Core.Generalizable a, Test.Extrapolate.Core.Generalizable b, Test.Extrapolate.Core.Generalizable c, Test.Extrapolate.Core.Generalizable d, Test.Extrapolate.Core.Generalizable e, Test.Extrapolate.Core.Generalizable f, Test.Extrapolate.Core.Generalizable g, Test.Extrapolate.Core.Generalizable h) => Test.Extrapolate.Core.Generalizable (a, b, c, d, e, f, g, h) -- | 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 360 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:_ ---- -- The property fails for any integer x and for any list -- _ at the tail. 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` [constant "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 -- | Use minFailures to configure the minimum number of -- failures for a conditional generalization in function of the maximum -- number of tests. -- -- To set that conditional generalizations should fail for 10% of cases: -- > check minFailures (div 10) $ prop -- -- To set that conditional generalizations should fail for 5% of cases: -- > check minFailures (div 20) $ prop minFailures :: Testable a => (WithOption a -> b) -> Ratio Int -> a -> b -- | Extrapolate can generalize counter-examples of any types that are -- Generalizable. -- -- The core (and only required functions) of the generalizable typeclass -- are the expr and instances functions. -- -- The following example shows a datatype and its instance: -- --
-- data Stack a = Stack a (Stack a) | Empty ---- --
-- instance Generalizable a => Generalizable (Stack a) where -- name _ = "s" -- expr s@(Stack x y) = constant "Stack" (Stack ->>: s) :$ expr x :$ expr y -- expr s@Empty = constant "Empty" (Empty -: s) -- instances s = this s $ instances (argTy1of1 s) ---- -- To declare instances and expr it may be useful to use: -- --
-- 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 -- expr s@(Stack x y) = constant "Stack" (Stack ->>: s) :$ expr x :$ expr y -- expr s@Empty = constant "Empty" (Empty -: s) -- 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 -- | 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. 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 ---- -- Needs the TemplateHaskell extension. deriveListable :: Name -> DecsQ -- | Adds to the weight of tiers of a constructor -- -- addWeight is closely related to delay. addWeight :: () => [[a]] -> Int -> [[a]] -- | Resets the weight of a constructor (or tiers) Typically used as an -- infix constructor when defining Listable instances: -- --
-- cons<N> `ofWeight` <W> ---- -- Be careful: do not apply 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 is closely related to reset. ofWeight :: () => [[a]] -> Int -> [[a]] 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]] 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]] 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]] 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]] 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]] cons7 :: (Listable a, Listable b, Listable c, Listable d, Listable e, Listable f, Listable g) => a -> b -> c -> d -> e -> f -> g -> h -> [[h]] 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 --(==>) :: 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 --exists :: Testable a => Int -> a -> Bool -- | Does a property fail for a number of test values? -- --
-- fails 1000 $ \xs -> xs ++ ys == ys ++ xs --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 --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 :: Testable a => Int -> a -> Maybe [String] -- | Lists all witnesses up to a number of tests to a property, 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)] -- ... -- ] --(><) :: () => [[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 -- --
-- cons<N> `suchThat` condition --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. Typically used when defining Listable instances: -- --
-- reset (cons<N> <Constr>) ---- -- 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. Typically used when defining -- Listable instances: -- --
-- delay (cons<N> <Constr>) --delay :: () => [[a]] -> [[a]] -- | Returns tiers of applications of a 5-argument constructor. -- -- Test.LeanCheck.Basic defines cons6 up to cons12. -- Those are exported by default from Test.LeanCheck, but are -- hidden from the Haddock documentation. 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. cons4 :: (Listable a, Listable b, Listable c, Listable d) => a -> b -> c -> d -> e -> [[e]] -- | Returns tiers of applications of a 3-argument 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. 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. 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. cons0 :: () => a -> [[a]] -- | concatMap over tiers concatMapT :: () => a -> [[b]] -> [[a]] -> [[b]] -- | concat tiers of tiers concatT :: () => [[[[a]]]] -> [[a]] -- | filter tiers filterT :: () => a -> Bool -> [[a]] -> [[a]] -- | map over tiers mapT :: () => a -> b -> [[a]] -> [[b]] -- | Tiers of Fractional values. This can be used as the -- implementation of tiers for Fractional types. tiersFractional :: Fractional a => [[a]] -- | Tiers of Integral values. Can be used as a default -- implementation of list for Integral types. listIntegral :: (Enum 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. -- -- 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. -- -- 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]