|
sourcecode:
|
module Test.EasyCheck (
-- test specification:
PropIO, returns, sameReturns, toError, toIOError,
Test, Prop, (==>), for, forAll,
test, is, isAlways, isEventually, uniquely, always, eventually,
failing, successful, deterministic, (-=-), (<~>), (~>), (<~), (<~~>),
(#), (#<), (#>), (<=>),
solutionOf,
-- test annotations
label, trivial, classify, collect, collectAs,
-- enumerating values
valuesOfSearchTree, valuesOf,
-- for EasyCheckExec
Result(..), result, args, updArgs, stamp, testsOf, ioTestOf, forAllValues
) where
import Control.Monad ( unless )
import Data.List ( (\\), delete, diagonal, nub )
import Control.Search.AllValues ( getAllValues )
import Control.Search.SearchTree ( SearchTree, someSearchTree )
import Control.Search.SearchTree.Traversal
import Test.Prop.Types
infix 1 `is`, `isAlways`, `isEventually`
infix 1 -=-, <~>, ~>, <~, <~~>, `trivial`, #, #<, #>, <=>
infix 1 `returns`, `sameReturns`
infixr 0 ==>
-------------------------------------------------------------------------
-- Properties involving I/O actions:
--- The property `returns a x` is satisfied if the execution of the
--- I/O action `a` returns the value `x`.
returns :: (Eq a, Show a) => IO a -> a -> PropIO
returns act r = PropIO (testIO act (return r))
--- The property `sameReturns a1 a2` is satisfied if the execution of the
--- I/O actions `a1` and `a2` return identical values.
sameReturns :: (Eq a, Show a) => IO a -> IO a -> PropIO
sameReturns a1 a2 = PropIO (testIO a1 a2)
--- The property `toError a` is satisfied if the evaluation of the argument
--- to normal form yields an exception.
toError :: a -> PropIO
toError x = toIOError (getAllValues x >>= \rs -> (id $!! rs) `seq` return ())
--- The property `toIOError a` is satisfied if the execution of the
--- I/O action `a` causes an exception.
toIOError :: IO a -> PropIO
toIOError act = PropIO (hasIOError act)
--- Extracts the tests of an I/O property (used by the test runner).
ioTestOf :: PropIO -> (Bool -> String -> IO (Maybe String))
ioTestOf (PropIO t) = t
-- Test an IO property, i.e., compare the results of two IO actions.
testIO :: (Eq a, Show a) => IO a -> IO a -> Bool -> String -> IO (Maybe String)
testIO act1 act2 quiet msg =
catch (do r1 <- act1
r2 <- act2
if r1 == r2
then unless quiet (putStr (msg++": OK\n")) >> return Nothing
else do putStrLn $ msg ++ ": FAILED!\nResults: " ++ show (r1,r2)
return (Just msg)
)
(\err -> do putStrLn $ msg ++ ": EXECUTION FAILURE:\n" ++ show err
return (Just msg)
)
-- Test whether an IO action produces an error.
hasIOError :: IO a -> Bool -> String -> IO (Maybe String)
hasIOError act quiet msg =
catch (act >> return (Just msg))
(\_ -> unless quiet (putStr (msg++": OK\n")) >> return Nothing)
-------------------------------------------------------------------------
-- Some auxiliaries:
--- Extracts the tests of a property (used by the test runner).
testsOf :: Prop -> [Test]
testsOf (Prop ts) = ts
--- An empty test.
notest :: Test
notest = Test Undef [] []
--- Extracts the result of a test.
result :: Test -> Result
result (Test r _ _) = r
--- Set the result of a test.
setResult :: Result -> Test -> Test
setResult res (Test _ s a) = Test res a s
--- Extracts the arguments of a test.
args :: Test -> [String]
args (Test _ a _) = a
--- Extracts the labels of a test.
stamp :: Test -> [String]
stamp (Test _ _ s) = s
--- Updates the arguments of a test.
updArgs :: ([String] -> [String]) -> Test -> Test
updArgs upd (Test r a s) = Test r (upd a) s
--- Updates the labels of a test.
updStamp :: ([String] -> [String]) -> Test -> Test
updStamp upd (Test r a s) = Test r a (upd s)
-- Test Specification
--- Constructs a property to be tested from an arbitrary expression
--- (first argument) and a predicate that is applied to the list of
--- non-deterministic values. The given predicate determines whether
--- the constructed property is satisfied or falsified for the given
--- expression.
test :: Show a => a -> ([a] -> Bool) -> Prop
test x f = Prop [setResult res notest]
where
xs = valuesOf x
res = case valuesOf (f xs) of
[True] -> Ok
[False] -> Falsified (map show xs)
bs -> Ambigious bs (map show xs)
--- The property `x -=- y` is satisfied if `x` and `y` have deterministic
--- values that are equal.
(-=-) :: (Eq a, Show a) => a -> a -> Prop
x -=- y = (x,y) `is` uncurry (==)
--- The property `x <~> y` is satisfied if the sets of the values of
--- `x` and `y` are equal.
(<~>) :: (Eq a, Show a) => a -> a -> Prop
x <~> y = test x (isSameSet (valuesOf y))
--- The property `x ~> y` is satisfied if `x` evaluates to every value of `y`.
--- Thus, the set of values of `y` must be a subset of the set of values of `x`.
(~>) :: (Eq a, Show a) => a -> a -> Prop
x ~> y = test x (isSubsetOf (valuesOf y))
--- The property `x <~ y` is satisfied if `y` evaluates to every value of `x`.
--- Thus, the set of values of `x` must be a subset of the set of values of `y`.
(<~) :: (Eq a, Show a) => a -> a -> Prop
x <~ y = test x (`isSubsetOf` (valuesOf y))
--- The property `x <~~> y` is satisfied if the multisets of the values of
--- `x` and `y` are equal.
(<~~>) :: (Eq a, Show a) => a -> a -> Prop
x <~~> y = test x (isSameMSet (valuesOf y))
isSameSet :: Eq a => [a] -> [a] -> Bool
isSameSet xs ys = xs' `subset` ys' && ys' `subset` xs'
where xs' = nub xs
ys' = nub ys
isSubsetOf :: Eq a => [a] -> [a] -> Bool
xs `isSubsetOf` ys = nub xs `subset` ys
subset :: Eq a => [a] -> [a] -> Bool
xs `subset` ys = null (xs\\ys)
-- compare to lists if they represent the same multi-set
isSameMSet :: Eq a => [a] -> [a] -> Bool
isSameMSet [] ys = ys == []
isSameMSet (x:xs) ys
| x `elem` ys = isSameMSet xs (delete x ys)
| otherwise = False
--- A conditional property is tested if the condition evaluates to `True`.
(==>) :: Bool -> Prop -> Prop
cond ==> p =
if True `elem` valuesOf cond
then p
else Prop [notest]
--- `solutionOf p` returns (non-deterministically) a solution
--- of predicate `p`. This operation is useful to test solutions
--- of predicates.
solutionOf :: Data a => (a -> Bool) -> a
solutionOf pred = pred x &> x where x free
--- The property `is x p` is satisfied if `x` has a deterministic value
--- which satisfies `p`.
is :: Show a => a -> (a -> Bool) -> Prop
is x f = test x (\xs -> case xs of [y] -> f y
_ -> False)
--- The property `isAlways x p` is satisfied if all values of `x` satisfy `p`.
isAlways :: Show a => a -> (a -> Bool) -> Prop
isAlways x = test x . all
--- The property `isEventually x p` is satisfied if some value of `x`
--- satisfies `p`.
isEventually :: Show a => a -> (a -> Bool) -> Prop
isEventually x = test x . any
--- The property `uniquely x` is satisfied if `x` has a deterministic value
--- which is true.
uniquely :: Bool -> Prop
uniquely = (`is` id)
--- The property `always x` is satisfied if all values of `x` are true.
always :: Bool -> Prop
always = (`isAlways` id)
--- The property `eventually x` is satisfied if some value of `x` is true.
eventually :: Bool -> Prop
eventually = (`isEventually` id)
--- The property `failing x` is satisfied if `x` has no value.
failing :: Show a => a -> Prop
failing x = test x null
--- The property `successful x` is satisfied if `x` has at least one value.
successful :: Show a => a -> Prop
successful x = test x (not . null)
--- The property `deterministic x` is satisfied if `x` has exactly one value.
deterministic :: Show a => a -> Prop
deterministic x = x `is` const True
--- The property `x # n` is satisfied if `x` has `n` values.
(#) :: (Eq a, Show a) => a -> Int -> Prop
x # n = test x ((n==) . length . nub)
--- The property `x #< n` is satisfied if `x` has less than `n` values.
(#<) :: (Eq a, Show a) => a -> Int -> Prop
x #< n = test x ((<n) . length . nub)
--- The property `x #> n` is satisfied if `x` has more than `n` values.
(#>) :: (Eq a, Show a) => a -> Int -> Prop
x #> n = test x ((>n) . length . nub)
--- The property `for x p` is satisfied if all values `y` of `x`
--- satisfy property `p y`.
for :: Show a => a -> (a -> Prop) -> Prop
for x p = forAll (valuesOf x) p
--- The property `forAll xs p` is satisfied if all values `x` of the list `xs`
--- satisfy property `p x`.
forAll :: Show a => [a] -> (a -> Prop) -> Prop
forAll xs p = forAllValues id xs p
--- Only for internal use by the test runner.
forAllValues :: Show a => (b -> Prop) -> [a] -> (a -> b) -> Prop
forAllValues c vals f =
Prop $
diagonal
[[ updArgs (show y:) t | let Prop ts = c (f y), t <- ts ] | y <- vals ]
--- The property `f <=> g` is satisfied if `f` and `g` are equivalent
--- operations, i.e., they can be replaced in any context without changing
--- the computed results.
(<=>) :: a -> a -> Prop
_ <=> _ = error $
"Test.Prop.<=> not executable. Use CurryCheck to test this property!"
-------------------------------------------------------------------------
-- Test Annotations
--- Assign a label to a property.
--- All labeled tests are counted and shown at the end.
label :: String -> Prop -> Prop
label l (Prop ts) = Prop (map (updStamp (l:)) ts)
--- Assign a label to a property if the first argument is `True`.
--- All labeled tests are counted and shown at the end.
--- Hence, this combinator can be used to classify tests:
---
--- multIsComm x y = classify (x<0 || y<0) "Negative" $ x*y -=- y*x
---
classify :: Bool -> String -> Prop -> Prop
classify True name = label name
classify False _ = id
--- Assign the label "trivial" to a property if the first argument is `True`.
--- All labeled tests are counted and shown at the end.
trivial :: Bool -> Prop -> Prop
trivial = (`classify` "trivial")
--- Assign a label showing the given argument to a property.
--- All labeled tests are counted and shown at the end.
collect :: Show a => a -> Prop -> Prop
collect = label . show
--- Assign a label showing a given name and the given argument to a property.
--- All labeled tests are counted and shown at the end.
collectAs :: Show a => String -> a -> Prop -> Prop
collectAs name = label . ((name++": ")++) . show
-------------------------------------------------------------------------
-- Value generation
--- Extracts values of a search tree according to a given strategy
--- (here: randomized diagonalization of levels with flattening).
valuesOfSearchTree :: SearchTree a -> [a]
valuesOfSearchTree
-- = depthDiag
-- = rndDepthDiag 0
-- = levelDiag
-- = rndLevelDiag 0
= rndLevelDiagFlat 5 0
-- = allValuesB
--- Computes the list of all values of the given argument
--- according to a given strategy (here:
--- randomized diagonalization of levels with flattening).
valuesOf :: a -> [a]
valuesOf = valuesOfSearchTree . someSearchTree . (id $##)
-------------------------------------------------------------------------
|