{-# language TypeApplications, ExplicitForAll, RankNTypes, GADTs #-}
module Test.LeanCheck.Extras
(Instances(..),Prop(..),Test(..),And(..))
where
import Test.LeanCheck
import Test.LeanCheck.Core (resultiers)
import qualified Data.List as L
{- | Extra combinators for leancheck, a property-based testing library.
example usage:
> > prop :: forall a . Eq a => [a] -> Bool
> > prop xs = xs == reverse xs
> > p = And
> > [ Test $ Prop "reverse @Unit" $ Instances 20 $ prop @())
> > , Test $ Prop "reverse @Bool" $ Instances 30 $ prop @Bool)
> > ]
> > check p
> *** Failed! Falsifiable (after 27 tests):
> reverse @Bool [False,True]
-}
prop :: forall a . Eq a => [a] -> Bool
prop xs = xs == reverse xs
p = And
[ Test $ Prop "reverse @Unit" $ Instances 20 $ prop @()
, Test $ Prop "reverse @Bool" $ Instances 30 $ prop @Bool
]
-- | restrict number of tests
data Instances a = Instances Int a
instance Testable a => Testable (Instances a) where
resultiers (Instances r p) = takeTotal r (resultiers p)
takeTotal :: Int -> [[a]] -> [[a]]
takeTotal k xss | k <= 0 || null xss = []
takeTotal k (xs : xss) =
let prefix = take k xs
in prefix : takeTotal (k - length prefix) xss
-- | give a name for the property (will be pre-pended in failure messages)
data Prop a = Prop String a
instance Testable a => Testable (Prop a) where
resultiers (Prop n p) = map (map (\ (args, f) -> (n : args, f))) $ resultiers p
-- | Hide the type argument existentially
data Test = forall a . Testable a => Test (a)
instance Testable Test where
resultiers (Test p) = resultiers p
-- | combine properties (each must be true)
-- use `Test` (on each element of argument list for And)
-- to combine properties of different types,
newtype And p = And [p]
instance Testable p => Testable (And p) where
resultiers (And ps) = map concat $ map L.transpose $ map resultiers ps