diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for falsify + +## 0.1.0 -- 2023-04-05 + +* First release diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2023, Well-Typed LLP + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Well-Typed LLP nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/falsify.cabal b/falsify.cabal new file mode 100644 --- /dev/null +++ b/falsify.cabal @@ -0,0 +1,170 @@ +cabal-version: 3.0 +name: falsify +version: 0.1.0 +synopsis: Property-based testing with internal integrated shrinking +description: This library provides property based testing with support + for internal integrated shrinking: integrated in the sense + of Hedgehog, meaning that there is no need to write a + separate shrinker and generator; and internal in the sense + of Hypothesis, meaning that this works well even across + monadic bind. However, the actual techniques that power + @falsify@ are quite different from both of these two + libraries. + + Most users will probably want to use the integration with + @@, + and use "Test.Tasty.Falsify" as their main entrypoint + into the library. The "Test.Falsify.Interactive" module + can be used to experiment with the libary in @ghci@. + +license: BSD-3-Clause +license-file: LICENSE +author: Edsko de Vries +maintainer: edsko@well-typed.com +copyright: Well-Typed LLP +category: Testing +build-type: Simple +extra-doc-files: CHANGELOG.md +tested-with: GHC==8.6.5 + , GHC==8.8.4 + , GHC==8.10.7 + , GHC==9.0.2 + , GHC==9.2.5 + , GHC==9.4.4 + , GHC==9.6.1 + +source-repository head + type: git + location: https://github.com/well-typed/falsify + +common lang + ghc-options: + -Wall + -Wredundant-constraints + -Widentities + build-depends: + base >= 4.12 && < 4.19 + default-language: + Haskell2010 + default-extensions: + BangPatterns + DataKinds + DefaultSignatures + DeriveAnyClass + DeriveFoldable + DeriveFunctor + DeriveGeneric + DeriveTraversable + DerivingStrategies + DerivingVia + DisambiguateRecordFields + FlexibleContexts + FlexibleInstances + GADTs + GeneralizedNewtypeDeriving + InstanceSigs + KindSignatures + LambdaCase + MultiParamTypeClasses + MultiWayIf + NamedFieldPuns + NumericUnderscores + PatternSynonyms + QuantifiedConstraints + RankNTypes + ScopedTypeVariables + StandaloneDeriving + TupleSections + TypeApplications + TypeOperators + ViewPatterns + +library + import: + lang + exposed-modules: + Test.Falsify.Generator + Test.Falsify.Interactive + Test.Falsify.Predicate + Test.Falsify.Property + Test.Falsify.Range + + -- For consistency with the other tasty runners, we places these modules + -- in the @Test.Tasty.*@ hiearchy instead of @Test.Falsify.*@. + Test.Tasty.Falsify + other-modules: + Test.Falsify.Internal.Driver + Test.Falsify.Internal.Driver.ReplaySeed + Test.Falsify.Internal.Driver.Tasty + Test.Falsify.Internal.Generator + Test.Falsify.Internal.Generator.Definition + Test.Falsify.Internal.Generator.Shrinking + Test.Falsify.Internal.Property + Test.Falsify.Internal.Range + Test.Falsify.Internal.SampleTree + Test.Falsify.Internal.Search + Test.Falsify.Reexported.Generator.Compound + Test.Falsify.Reexported.Generator.Function + Test.Falsify.Reexported.Generator.Precision + Test.Falsify.Reexported.Generator.Shrinking + Test.Falsify.Reexported.Generator.Simple + + Data.Falsify.Integer + Data.Falsify.List + Data.Falsify.Marked + Data.Falsify.Tree + hs-source-dirs: + src + build-depends: + , base16-bytestring >= 1.0 && < 1.1 + , binary >= 0.8 && < 0.9 + , bytestring >= 0.10 && < 0.12 + , containers >= 0.6 && < 0.7 + , data-default >= 0.7 && < 0.8 + , mtl >= 2.2 && < 2.4 + , optics-core >= 0.3 && < 0.5 + , optparse-applicative >= 0.16 && < 0.18 + , selective >= 0.4 && < 0.8 + , sop-core >= 0.5 && < 0.6 + , splitmix >= 0.1 && < 0.2 + , tagged >= 0.8 && < 0.9 + , tasty >= 1.3 && < 1.5 + , transformers >= 0.5 && < 0.7 + , vector >= 0.12 && < 0.14 + other-extensions: + CPP + +test-suite test-falsify + import: + lang + type: + exitcode-stdio-1.0 + hs-source-dirs: + test + main-is: + Main.hs + other-modules: + TestSuite.Sanity.Predicate + TestSuite.Sanity.Range + TestSuite.Sanity.Selective + TestSuite.Prop.Generator.Compound + TestSuite.Prop.Generator.Function + TestSuite.Prop.Generator.Marking + TestSuite.Prop.Generator.Precision + TestSuite.Prop.Generator.Prim + TestSuite.Prop.Generator.Selective + TestSuite.Prop.Generator.Shrinking + TestSuite.Prop.Generator.Simple + TestSuite.Util.List + TestSuite.Util.Tree + build-depends: + , QuickCheck >= 2.14 && < 2.15 + , tasty-hunit >= 0.10 && < 0.11 + + -- Inherit bounds from the main library + , containers + , data-default + , falsify + , selective + , tasty + diff --git a/src/Data/Falsify/Integer.hs b/src/Data/Falsify/Integer.hs new file mode 100644 --- /dev/null +++ b/src/Data/Falsify/Integer.hs @@ -0,0 +1,59 @@ +module Data.Falsify.Integer ( + -- * Encoding + Bit(..) + , encIntegerEliasG + ) where + +import Data.Bits +import Numeric.Natural + +{------------------------------------------------------------------------------- + Binary encoding +-------------------------------------------------------------------------------} + +data Bit = I | O + deriving (Show, Eq, Ord) + +-- | Binary encoding (most significant bit first) +natToBits :: Natural -> [Bit] +natToBits = \n -> if + | n < 0 -> error "toBits: negative input" + | n == 0 -> [] + | otherwise -> reverse $ go n + where + go :: Natural -> [Bit] + go 0 = [] + go n = (if testBit n 0 then I else O) : go (shiftR n 1) + +{------------------------------------------------------------------------------- + Elias γ code +-------------------------------------------------------------------------------} + +-- | Elias γ code +-- +-- Precondition: input @x >= 1@. +-- +-- See . +encEliasG :: Natural -> [Bit] +encEliasG x + | x == 0 = error "eliasG: zero" + | otherwise = zeroes x + where + zeroes :: Natural -> [Bit] + zeroes n + | n <= 1 = natToBits x + | otherwise = O : zeroes (shiftR n 1) + +-- | Extension of Elias γ coding to signed integers +-- +-- This is adapted from @integerVariant@ in @Test.QuickCheck.Random@. The first +-- bit encs whether @x >= 1@ or not (this will result in @0@ and @1@ having +-- short codes). +encIntegerEliasG :: Integer -> [Bit] +encIntegerEliasG = \x -> + if x >= 1 + then O : encEliasG (fromInteger $ x) + else I : encEliasG (fromInteger . mangle $ x) + where + mangle :: Integer -> Integer + mangle x = 1 - x diff --git a/src/Data/Falsify/List.hs b/src/Data/Falsify/List.hs new file mode 100644 --- /dev/null +++ b/src/Data/Falsify/List.hs @@ -0,0 +1,80 @@ +module Data.Falsify.List ( + -- * Splitting + chunksOfNonEmpty + -- * Permutations + , Permutation + , applyPermutation + -- * Dealing with marks + , keepAtLeast + ) where + +import Control.Monad +import Control.Monad.ST +import Data.Foldable (toList) +import Data.List.NonEmpty (NonEmpty(..)) + +import qualified Data.Vector as V +import qualified Data.Vector.Mutable as VM + +import Data.Falsify.Marked + +{------------------------------------------------------------------------------- + Splitting +-------------------------------------------------------------------------------} + +-- | Take chunks of a non-empty list +-- +-- This is lazy: +-- +-- > NE.take 4 $ chunksOfNonEmpty 3 (0 :| [1..]) +-- > == [ 0 :| [1,2] +-- > , 3 :| [4,5] +-- > , 6 :| [7,8] +-- > , 9 :| [10,11] +-- > ] +chunksOfNonEmpty :: Word -> NonEmpty a -> NonEmpty (NonEmpty a) +chunksOfNonEmpty 0 _ = error "chunksOfNonEmpty: zero chunk size" +chunksOfNonEmpty n (x :| xs) = + let (chunk, rest) = splitAt (fromIntegral n) (x : xs) + in case (chunk, rest) of + ([] , _) -> error "impossible" + (c:cs , []) -> (c :| cs) :| [] + (c:cs , r:rs) -> (c :| cs) :| toList (chunksOfNonEmpty n (r :| rs)) + +{------------------------------------------------------------------------------- + Permutations +-------------------------------------------------------------------------------} + +-- | Permutation is a sequence of swaps +type Permutation = [(Word, Word)] + +applyPermutation :: Permutation -> [a] -> [a] +applyPermutation p xs = + V.toList $ V.modify (forM_ (map conv p) . swap) (V.fromList xs) + where + swap :: V.MVector s a -> (Int, Int) -> ST s () + swap vec (i, j) = do + x <- VM.read vec i + y <- VM.read vec j + VM.write vec i y + VM.write vec j x + + conv :: (Word, Word) -> (Int, Int) + conv (i, j) = (fromIntegral i, fromIntegral j) + +{------------------------------------------------------------------------------- + Dealing with marks +-------------------------------------------------------------------------------} + +keepAtLeast :: Word -> [Marked f a] -> [Marked f a] +keepAtLeast = \n xs -> + let kept = countKept xs + in if kept >= n + then xs + else go (n - kept) xs + where + go :: Word -> [Marked f a] -> [Marked f a] + go _ [] = [] + go 0 xs = xs + go n (Marked Keep x:xs) = Marked Keep x : go n xs + go n (Marked Drop x:xs) = Marked Keep x : go (n - 1) xs diff --git a/src/Data/Falsify/Marked.hs b/src/Data/Falsify/Marked.hs new file mode 100644 --- /dev/null +++ b/src/Data/Falsify/Marked.hs @@ -0,0 +1,57 @@ +-- | Marked elements +-- +-- Intended for unqualified import. +module Data.Falsify.Marked ( + Mark(..) + , Marked(..) + -- * Generation + , selectAllKept + -- * Queries + , countKept + , shouldKeep + ) where + +import Control.Selective +import Data.Foldable (toList) +import Data.Maybe (mapMaybe) + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +data Mark = Keep | Drop + deriving stock (Show, Eq, Ord) + +data Marked f a = Marked { + getMark :: Mark + , unmark :: f a + } + deriving stock (Show, Eq, Ord) + +{------------------------------------------------------------------------------- + Generation +-------------------------------------------------------------------------------} + +selectKept :: Selective f => Marked f a -> f (Maybe a) +selectKept (Marked mark gen) = + ifS (pure $ mark == Keep) + (Just <$> gen) + (pure Nothing) + +-- | Traverse the argument, generating all values marked 'Keep', and replacing +-- all values marked 'Drop' by 'Nothing' +selectAllKept :: + (Traversable t, Selective f) + => t (Marked f a) -> f (t (Maybe a)) +selectAllKept = traverse selectKept + +{------------------------------------------------------------------------------- + Queries +-------------------------------------------------------------------------------} + +countKept :: Foldable t => t (Marked f a) -> Word +countKept = fromIntegral . length . mapMaybe shouldKeep . toList + +shouldKeep :: Marked f a -> Maybe (f a) +shouldKeep (Marked Keep x) = Just x +shouldKeep (Marked Drop _) = Nothing diff --git a/src/Data/Falsify/Tree.hs b/src/Data/Falsify/Tree.hs new file mode 100644 --- /dev/null +++ b/src/Data/Falsify/Tree.hs @@ -0,0 +1,192 @@ +module Data.Falsify.Tree ( + Tree(Leaf, Branch) + -- * Dealing with marks + , propagate + , genKept + , keepAtLeast + -- * Binary search trees + , Interval(..) + , Endpoint(..) + , inclusiveBounds + , lookup + -- * Debugging + , drawTree + ) where + +import Prelude hiding (drop, lookup) + +import Control.Selective (Selective, ifS) +import Control.Monad.State +import GHC.Show + +import qualified Data.Tree as Rose + +import Data.Falsify.Marked + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +data Tree a = + Leaf + + -- 'Branch_' caches the size of the tree + | Branch_ {-# UNPACK #-} !Word a (Tree a) (Tree a) + deriving stock (Eq, Functor, Foldable, Traversable) + +{------------------------------------------------------------------------------- + Tree stats +-------------------------------------------------------------------------------} + +-- | Size of the tree +-- +-- @O(1)@ +size :: Tree a -> Word +size Leaf = 0 +size (Branch_ s _ _ _) = s + +{------------------------------------------------------------------------------- + Pattern synonyms that hide the size argument +-------------------------------------------------------------------------------} + +viewBranch :: Tree a -> Maybe (a, Tree a, Tree a) +viewBranch Leaf = Nothing +viewBranch (Branch_ _ x l r) = Just (x, l, r) + +branch :: a -> Tree a -> Tree a -> Tree a +branch x l r = Branch_ (1 + size l + size r) x l r + +pattern Branch :: a -> Tree a -> Tree a -> Tree a +pattern Branch x l r <- (viewBranch -> Just (x, l, r)) + where + Branch = branch + +{-# COMPLETE Leaf, Branch #-} + +{------------------------------------------------------------------------------- + 'Show' instance that depends on the pattern synonyms +-------------------------------------------------------------------------------} + +instance Show a => Show (Tree a) where + showsPrec _ Leaf = showString "Leaf" + showsPrec a (Branch x l r) = showParen (a > appPrec) $ + showString "Branch " + . showsPrec appPrec1 x + . showSpace + . showsPrec appPrec1 l + . showSpace + . showsPrec appPrec1 r + +{------------------------------------------------------------------------------- + Dealing with marks +-------------------------------------------------------------------------------} + +-- | Propagate 'Drop' marker down the tree +-- +-- This is useful in conjunction with 'genKept', which truncates entire +-- subtrees. +propagate :: Tree (Marked f a) -> Tree (Marked f a) +propagate = keep + where + keep :: Tree (Marked f a) -> Tree (Marked f a) + keep Leaf = Leaf + keep (Branch (Marked Keep x) l r) = Branch (Marked Keep x) (keep l) (keep r) + keep (Branch (Marked Drop x) l r) = Branch (Marked Drop x) (drop l) (drop r) + + drop :: Tree (Marked f a) -> Tree (Marked f a) + drop = fmap $ \(Marked _ x) -> Marked Drop x + +-- | Generate those values we want to keep +-- +-- Whenever we meet an element marked 'Drop', that entire subtree is dropped. +genKept :: forall f a. Selective f => Tree (Marked f a) -> f (Tree a) +genKept = go + where + go :: Tree (Marked f a) -> f (Tree a) + go Leaf = pure Leaf + go (Branch (Marked m g) l r) = ifS (pure $ m == Keep) + (Branch <$> g <*> go l <*> go r) + (pure Leaf) + +-- | Change enough nodes currently marked as 'Drop' to 'Keep' to ensure at +-- least @n@ nodes are marked 'Keep'. +-- +-- Precondition: any 'Drop' marks must have been propagated; see 'propagate'. +-- Postcondition: this property is preserved. +keepAtLeast :: Word -> Tree (Marked f a) -> Tree (Marked f a) +keepAtLeast = \n t -> + let kept = countKept t + in if kept >= n + then t + else evalState (go t) (n - kept) + where + go :: Tree (Marked f a) -> State Word (Tree (Marked f a)) + go Leaf = return Leaf + go (Branch (Marked Keep x) l r) = Branch (Marked Keep x) <$> go l <*> go r + go t@(Branch (Marked Drop x) l r) = get >>= \case + 0 -> + -- Nothing left to drop + return t + n | size t <= n -> do + -- We can keep the entire subtree + put $ n - size t + return $ fmap (Marked Keep . unmark) t + n -> do + -- We cannot delete the entire subtree. In order to preserve the + -- "drop property", we /must/ mark this node as 'Keep' + put $ n - 1 + Branch (Marked Keep x) <$> go l <*> go r + +{------------------------------------------------------------------------------- + BST +-------------------------------------------------------------------------------} + +data Endpoint a = Inclusive a | Exclusive a +data Interval a = Interval (Endpoint a) (Endpoint a) + +-- | Compute interval with inclusive bounds, without exceeding range +-- +-- Returns 'Nothing' if the interval is empty, and @Just@ the inclusive +-- lower and upper bound otherwise. +inclusiveBounds :: forall a. (Ord a, Enum a) => Interval a -> Maybe (a, a) +inclusiveBounds = \(Interval lo hi) -> go lo hi + where + -- The inequality checks in @go@ justify the use of @pred@ or @succ@ + go :: Endpoint a -> Endpoint a -> Maybe (a, a) + go (Inclusive lo) (Inclusive hi) + | lo <= hi = Just (lo, hi) + | otherwise = Nothing + go (Exclusive lo) (Inclusive hi) + | lo < hi = Just (succ lo, hi) + | otherwise = Nothing + go (Inclusive lo) (Exclusive hi) + | lo < hi = Just (lo, pred hi) + | otherwise = Nothing + go (Exclusive lo) (Exclusive hi) + | lo < hi = if succ lo > pred hi + then Nothing + else Just (succ lo, pred hi) + | otherwise = Nothing + + +-- | Look value up in BST +-- +-- NOTE: The 'Tree' datatype itself does /NOT/ guarantee that the tree is in +-- fact a BST. It is the responsibility of the caller to ensure this. +lookup :: Ord a => a -> Tree (a, b) -> Maybe b +lookup a' (Branch (a, b) l r) + | a' < a = lookup a' l + | a' > a = lookup a' r + | otherwise = Just b +lookup _ Leaf = Nothing + +{------------------------------------------------------------------------------- + Debugging +-------------------------------------------------------------------------------} + +drawTree :: Tree String -> String +drawTree = Rose.drawTree . conv + where + conv :: Tree String -> Rose.Tree String + conv Leaf = Rose.Node "*" [] + conv (Branch x l r) = Rose.Node x [conv l, conv r] diff --git a/src/Test/Falsify/Generator.hs b/src/Test/Falsify/Generator.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Generator.hs @@ -0,0 +1,92 @@ +-- | Generator +-- +-- Intended for qualified import. +-- +-- > import Test.Falsify.Generator (Gen) +-- > import qualified Test.Falsify.Generator qualified as Gen +module Test.Falsify.Generator ( + -- * Definition + Gen -- opaque + -- * Simple (non-compound) generators + , bool + , integral + , int + , enum + -- * Compound generators + -- ** Taking advantage of 'Selective' + , choose + -- ** Lists + , list + , elem + , pick + , pickBiased + , shuffle + -- ** Permutations + , Permutation + , applyPermutation + , permutation + -- ** Tweak test data distribution + , frequency + -- ** Trees + , Tree(Leaf, Branch) + , drawTree + -- *** Binary trees + , tree + , bst + -- *** Shrink trees + , ShrinkTree + , IsValidShrink(..) + , path + , pathAny + -- ** Marking + , Marked(..) + , Mark(..) + , selectAllKept + , mark + -- * Functions + -- ** Generation + , Fun + , applyFun + , pattern Fn + , pattern Fn2 + , pattern Fn3 + , fun + -- ** Construction + , Function(..) + , (:->) -- opaque + , functionMap + -- * Reducing precision + , WordN(..) + , wordN + , properFraction + -- * Overriding shrinking + , withoutShrinking + , shrinkToOneOf + , firstThen + , shrinkWith + , shrinkToNothing + -- * Shrink trees + , fromShrinkTree + , toShrinkTree + -- * Generator independence + , bindIntegral + , perturb + -- * Low-level + , prim + , primWith + , exhaustive + , captureLocalTree + , bindWithoutShortcut + ) where + +import Prelude hiding (either, elem, properFraction) + +import Data.Falsify.List +import Data.Falsify.Marked +import Test.Falsify.Internal.Generator +import Test.Falsify.Reexported.Generator.Compound +import Test.Falsify.Reexported.Generator.Function +import Test.Falsify.Reexported.Generator.Precision +import Test.Falsify.Reexported.Generator.Shrinking +import Test.Falsify.Reexported.Generator.Simple +import Data.Falsify.Tree diff --git a/src/Test/Falsify/Interactive.hs b/src/Test/Falsify/Interactive.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Interactive.hs @@ -0,0 +1,81 @@ +-- | Utilities for interaction with falsify in ghci +module Test.Falsify.Interactive ( + falsify + , falsify' + , sample + , shrink + , shrink' + -- * Re-exports + , module Test.Falsify.Property + -- ** Functions + , pattern Gen.Fn + , pattern Gen.Fn2 + , pattern Gen.Fn3 + ) where + +import Data.Bifunctor +import Data.Default +import Data.List.NonEmpty (NonEmpty(..)) +import System.Random.SplitMix + +import qualified Data.List.NonEmpty as NE + +import Test.Falsify.Internal.Driver.ReplaySeed +import Test.Falsify.Internal.Generator +import Test.Falsify.Internal.Generator.Shrinking +import Test.Falsify.Internal.Property +import Test.Falsify.Property + +import qualified Test.Falsify.Generator as Gen +import qualified Test.Falsify.Internal.Driver as Driver +import qualified Test.Falsify.Internal.SampleTree as SampleTree + +-- | Sample generator +sample :: Gen a -> IO a +sample g = do + prng <- initSMGen + let (x, _shrunk) = runGen g (SampleTree.fromPRNG prng) + return x + +-- | Shrink counter-example +-- +-- This will run the generator repeatedly until it finds a counter-example to +-- the given property, and will then shrink it. +-- +-- Returns 'Nothing' if no counter-example could be found. +shrink :: forall a. (a -> Bool) -> Gen a -> IO (Maybe a) +shrink p g = falsify $ testGen' (\x -> aux x $ p x) g + where + aux :: a -> Bool -> Either a () + aux _ True = Right () + aux x False = Left x + +-- | Generalization of 'shrink'. Returns the full shrink history. +shrink' :: forall e a. (a -> Maybe e) -> Gen a -> IO (Maybe (NonEmpty e)) +shrink' p g = falsify' $ testGen' (aux . p) g + where + aux :: Maybe e -> Either e () + aux Nothing = Right () + aux (Just x) = Left x + +-- | Try to falsify the given property +-- +-- Reports the counter-example, if we find any. +falsify :: forall e a. Property' e a -> IO (Maybe e) +falsify = fmap (fmap NE.last) . falsify' + +-- | Generalization of 'falsify' that reports the full shrink history +falsify' :: forall e a. Property' e a -> IO (Maybe (NonEmpty e)) +falsify' = fmap aux . Driver.falsify def + where + aux :: + ( ReplaySeed + , [Driver.Success a] + , Driver.TotalDiscarded + , Maybe (Driver.Failure e) + ) + -> Maybe (NonEmpty e) + aux (_seed, _successes, _discarded, failure) = + case failure of + Nothing -> Nothing + Just f -> Just $ shrinkHistory $ first fst $ Driver.failureRun f diff --git a/src/Test/Falsify/Internal/Driver.hs b/src/Test/Falsify/Internal/Driver.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Internal/Driver.hs @@ -0,0 +1,481 @@ +-- | Test driver +-- +-- Intended for qualified import. +-- +-- > import Test.Falsify.Internal.Driver (Success, Failure, falsify) +-- > import qualified Test.Falsify.Internal.Driver as Driver +module Test.Falsify.Internal.Driver ( + -- * Options + Options(..) + -- * Results + , Success(..) + , Failure(..) + , TotalDiscarded(..) + -- * Test driver + , falsify + -- * Process results + , Verbose(..) + , ExpectFailure(..) + , RenderedTestResult(..) + , renderTestResult + ) where + +import Prelude hiding (log) + +import Data.Bifunctor +import Data.Default +import Data.List (intercalate) +import Data.List.NonEmpty (NonEmpty) +import Data.Map (Map) +import Data.Set (Set) +import GHC.Exception +import System.Random.SplitMix +import Text.Printf + +import qualified Data.List.NonEmpty as NE +import qualified Data.Map as Map +import qualified Data.Set as Set + +import Test.Falsify.Internal.Driver.ReplaySeed +import Test.Falsify.Internal.Generator +import Test.Falsify.Internal.Generator.Shrinking +import Test.Falsify.Internal.Property +import Test.Falsify.Internal.SampleTree (SampleTree) + +import qualified Test.Falsify.Internal.SampleTree as SampleTree + +{------------------------------------------------------------------------------- + Options +-------------------------------------------------------------------------------} + +-- | Options for running a test +data Options = Options { + -- | Number of test cases to generate + tests :: Word + + -- | Number of shrinks allowed before failing a test + , maxShrinks :: Maybe Word + + -- | Random seed to use for replaying a previous test run + , replay :: Maybe ReplaySeed + + -- | Maximum number of discarded test per successful test + , maxRatio :: Word + } + +instance Default Options where + def = Options { + tests = 100 + , maxShrinks = Nothing + , replay = Nothing + , maxRatio = 100 + } + +{------------------------------------------------------------------------------- + Driver +-------------------------------------------------------------------------------} + +data Success a = Success { + successResult :: a + , successSeed :: ReplaySeed + , successRun :: TestRun + } + deriving (Show) + +data Failure e = Failure { + failureSeed :: ReplaySeed + , failureRun :: ShrinkExplanation (e, TestRun) TestRun + } + deriving (Show) + +newtype TotalDiscarded = TotalDiscarded Word + +-- | Run a test: attempt to falsify the given property +-- +-- We return +-- +-- * initial replay seed (each test also records its own seed) +-- * successful tests +-- * how many tests we discarded +-- * the failed test (if any). +falsify :: forall e a. + Options + -> Property' e a + -> IO (ReplaySeed, [Success a], TotalDiscarded, Maybe (Failure e)) +falsify opts prop = do + acc <- initDriverState opts + (successes, discarded, mFailure) <- go acc + return ( + splitmixReplaySeed (prng acc) + , successes + , TotalDiscarded discarded + , mFailure + ) + where + go :: DriverState a -> IO ([Success a], Word, Maybe (Failure e)) + go acc | todo acc == 0 = return (successes acc, discardedTotal acc, Nothing) + go acc = do + let now, later :: SMGen + (now, later) = splitSMGen (prng acc) + + st :: SampleTree + st = SampleTree.fromPRNG now + + result :: TestResult e a + run :: TestRun + shrunk :: [SampleTree] + ((result, run), shrunk) = runGen (runProperty prop) st + + case result of + -- Test passed + TestPassed x -> do + let success :: Success a + success = Success { + successResult = x + , successSeed = splitmixReplaySeed now + , successRun = run + } + if runDeterministic run then + case (successes acc, discardedTotal acc) of + ([], 0) -> return ([success], 0, Nothing) + _otherwise -> error "falsify.go: impossible" + else + go $ withSuccess later success acc + + -- Test failed + -- + -- We ignore the failure message here, because this is the failure + -- message before shrinking, which we are typically not interested in. + TestFailed e -> do + let explanation :: ShrinkExplanation (e, TestRun) TestRun + explanation = + limitShrinkSteps (maxShrinks opts) . second snd $ + shrinkFrom + resultIsValidShrink + (runProperty prop) + ((e, run), shrunk) + + -- We have to be careful here: if the user specifies a seed, we + -- will first /split/ it to run the test (call to splitSMGen, + -- above). This means that the seed we should provide for the + -- test is the seed /before/ splitting. + failure :: Failure e + failure = Failure { + failureSeed = splitmixReplaySeed (prng acc) + , failureRun = explanation + } + + return (successes acc, discardedTotal acc, Just failure) + + -- Test discarded, but reached maximum already + TestDiscarded | discardedForTest acc == maxRatio opts -> + return (successes acc, discardedTotal acc, Nothing) + + -- Test discarded; continue. + TestDiscarded -> + go $ withDiscard later acc + +{------------------------------------------------------------------------------- + Internal: driver state +-------------------------------------------------------------------------------} + +data DriverState a = DriverState { + -- | State of the PRNG after the previously executed test + prng :: SMGen + + -- | Accumulated successful tests + , successes :: [Success a] + + -- | Number of tests still to execute + , todo :: Word + + -- | Number of tests we discarded so far (for this test) + , discardedForTest :: Word + + -- | Number of tests we discarded (in total) + , discardedTotal :: Word + } + deriving (Show) + +initDriverState :: Options -> IO (DriverState a) +initDriverState opts = do + prng <- case replay opts of + Just (ReplaySplitmix seed gamma) -> + return $ seedSMGen seed gamma + Nothing -> + initSMGen + return $ DriverState { + prng + , successes = [] + , todo = tests opts + , discardedForTest = 0 + , discardedTotal = 0 + } + +withSuccess :: SMGen -> Success a -> DriverState a -> DriverState a +withSuccess next success acc = DriverState { + prng = next + , successes = success : successes acc + , todo = pred (todo acc) + , discardedForTest = 0 -- reset for the next test + , discardedTotal = discardedTotal acc + } + +withDiscard :: SMGen -> DriverState a -> DriverState a +withDiscard next acc = DriverState { + prng = next + , successes = successes acc + , todo = todo acc + , discardedForTest = succ $ discardedForTest acc + , discardedTotal = succ $ discardedTotal acc + } + +{------------------------------------------------------------------------------- + Process results +-------------------------------------------------------------------------------} + +-- | Verbose output +-- +-- Note that if a test fails (and we were not expecting failure) we show the +-- logs independent of verbosity. +data Verbose = Verbose | NotVerbose + +-- | Do we expect the property to fail? +-- +-- If 'ExpectFailure', the test will fail if the property does /not/ fail. +-- Note that if we expect failure for a property, then we can stop at the first +-- failed test; the number of tests to run for the property becomes a maximum +-- rather than a goal. +data ExpectFailure = ExpectFailure | DontExpectFailure + +-- | Test result as it should be shown to the user +data RenderedTestResult = RenderedTestResult { + testPassed :: Bool + , testOutput :: String + } + +renderTestResult :: + Verbose + -> ExpectFailure + -> (ReplaySeed, [Success ()], TotalDiscarded, Maybe (Failure String)) + -> RenderedTestResult +renderTestResult + verbose + expectFailure + (initSeed, successes, TotalDiscarded discarded, mFailure) = + case (verbose, expectFailure, mFailure) of + + -- + -- All tests discarded + -- + -- TODO: Verbose mode here does nothing currently (we get no logs for + -- discarded tests). + -- + + (_, DontExpectFailure, Nothing) | null successes -> RenderedTestResult { + testPassed = False + , testOutput = unlines [ + concat [ + "All tests discarded" + , countDiscarded + ] + ] + } + + -- + -- Test succeeded + -- + -- This may still be a failure, if we were expecting the test not to + -- succeed. + -- + + (NotVerbose, DontExpectFailure, Nothing) -> RenderedTestResult { + testPassed = True + , testOutput = unlines [ + concat [ + countSuccess + , countDiscarded + ] + , showLabels + ] + } + + (Verbose, DontExpectFailure, Nothing) -> RenderedTestResult { + testPassed = True + , testOutput = unlines [ + concat [ + countSuccess + , countDiscarded + ] + , "" + , "Logs for each test run below." + , "" + , unlines $ map renderSuccess (zip [1..] successes) + ] + } + + (NotVerbose, ExpectFailure, Nothing) -> RenderedTestResult { + testPassed = False + , testOutput = unlines [ + "Expected failure, but " ++ countAll ++ " passed" + , showSeed initSeed + ] + } + + (Verbose, ExpectFailure, Nothing) -> RenderedTestResult { + testPassed = False + , testOutput = unlines [ + "Expected failure, but " ++ countAll ++ " passed" + , "" + , "Logs for each test run below." + , "" + , intercalate "\n" $ map renderSuccess (zip [1..] successes) + , showSeed initSeed + ] + } + + -- + -- Test failed + -- + -- This might still mean the test passed, if we /expected/ failure. + -- + -- If the test failed and we were not expecting failure, we show the + -- logs independent of verbosity. + -- + + (NotVerbose, ExpectFailure, Just e) -> RenderedTestResult { + testPassed = True + , testOutput = unlines [ + concat [ + "expected failure after " + , countHistory history + , countDiscarded + ] + , fst $ NE.last history + ] + } + where + history = shrinkHistory (failureRun e) + + (Verbose, ExpectFailure, Just e) -> RenderedTestResult { + testPassed = True + , testOutput = unlines [ + concat [ + "expected failure after " + , countHistory history + , countDiscarded + ] + , fst $ NE.last history + , "Logs for failed test run:" + , renderLog . runLog . snd $ NE.last history + ] + } + where + history = shrinkHistory (failureRun e) + + (_, DontExpectFailure, Just e) -> RenderedTestResult { + testPassed = False + , testOutput = unlines [ + "failed after " ++ countHistory history + , fst $ NE.last history + , "Logs for failed test run:" + , renderLog . runLog . snd $ NE.last history + , showSeed $ failureSeed e + ] + } + where + history = shrinkHistory (failureRun e) + where + countSuccess, countDiscarded, countAll :: String + countSuccess + | length successes == 1 = "1 successful test" + | otherwise = show (length successes) ++ " successful tests" + countDiscarded + | discarded == 0 = "" + | otherwise = " (discarded " ++ show discarded ++ ")" + countAll + | length successes == 1 = "the test" + | otherwise = "all " ++ show (length successes) ++ " tests" + + -- The history includes the original value, so the number of shrink steps + -- is the length of the history minus 1. + countHistory :: NonEmpty (String, TestRun) -> [Char] + countHistory history = concat [ + if | length successes == 0 -> "" + | otherwise -> countSuccess ++ " and " + , if | length history == 2 -> "1 shrink" + | otherwise -> show (length history - 1) ++ " shrinks" + ] + + showSeed :: ReplaySeed -> String + showSeed seed = "Use --falsify-replay=" ++ show seed ++ " to replay." + + showLabels :: String + showLabels = intercalate "\n" [ + intercalate "\n" $ ("\nLabel " ++ show l ++ ":") : [ + asPct n ++ " " ++ v + | v <- Set.toList (Map.findWithDefault Set.empty l allValues) + , let n = Map.findWithDefault 0 v + $ Map.findWithDefault Map.empty l + $ perTest + ] + | l <- Set.toList allLabels + ] + where + -- Absolute number of tests as a percentage of total successes + asPct :: Int -> String + asPct n = + printf " %8.4f%%" pct + where + pct :: Double + pct = fromIntegral n / fromIntegral (length successes) * 100 + + -- All labels across all tests + allLabels :: Set String + allLabels = Map.keysSet allValues + + -- For each label, all values reported across all tests + allValues :: Map String (Set String) + allValues = + Map.unionsWith Set.union $ + map (runLabels . successRun) successes + + -- For each label and each value, the corresponding number of tests + perTest :: Map String (Map String Int) + perTest = + Map.fromList [ + (l, Map.fromList [ + (v, length $ filter (labelHasValue l v) successes) + | v <- Set.toList $ + Map.findWithDefault Set.empty l allValues + ]) + | l <- Set.toList allLabels + ] + + -- Check if in particular test run label @l@ has value @v@ + labelHasValue :: String -> String -> Success () -> Bool + labelHasValue l v = + Set.member v + . Map.findWithDefault Set.empty l + . runLabels + . successRun + +renderSuccess :: (Int, Success ()) -> String +renderSuccess (ix, Success{successRun}) = + intercalate "\n" . concat $ [ + ["Test " ++ show ix] + , [renderLog $ runLog successRun] + ] + +renderLog :: Log -> String +renderLog (Log log) = unlines $ map renderLogEntry (reverse log) + +renderLogEntry :: LogEntry -> String +renderLogEntry = \case + Generated stack x -> concat [ + "generated " + , x + , " at " + , prettyCallStack stack + ] + Info x -> x diff --git a/src/Test/Falsify/Internal/Driver/ReplaySeed.hs b/src/Test/Falsify/Internal/Driver/ReplaySeed.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Internal/Driver/ReplaySeed.hs @@ -0,0 +1,73 @@ +{-# LANGUAGE CPP #-} + +-- | Replay seeds +-- +-- We need a seed/gamma pair to initialize a splitmix PRNG. This is however a +-- pretty low level implementation detail that I'd prefer not be be directly +-- visible. We therefore provide a thin layer on top, which provides an +-- "encoded" replay seed. This has the additional benefits that the length of +-- the replay seed is always the same (unlike just writing a 'Word64'), and we +-- could in principle at some point support other kinds of PRNGs. +module Test.Falsify.Internal.Driver.ReplaySeed ( + ReplaySeed(..) + , parseReplaySeed + , safeReadReplaySeed + , splitmixReplaySeed + ) where + +import Data.String +import Data.Word +import Data.Binary +import System.Random.SplitMix + +import qualified Data.ByteString.Base16.Lazy as Lazy.Base16 +import qualified Data.ByteString.Lazy.Char8 as Lazy.Char8 + +data ReplaySeed = + ReplaySplitmix Word64 Word64 + +splitmixReplaySeed :: SMGen -> ReplaySeed +splitmixReplaySeed = uncurry ReplaySplitmix . unseedSMGen + +instance Binary ReplaySeed where + put (ReplaySplitmix seed gamma) = do + putWord8 1 + put seed + put gamma + + get = do + tag <- getWord8 + case tag of + 1 -> do seed <- get + gamma <- get + if odd gamma + then return $ ReplaySplitmix seed gamma + else fail $ "ReplaySeed: expected odd gamma for splitmix" + n -> fail $ "ReplaySeed: invalid tag: " ++ show n + +instance Show ReplaySeed where + show = Lazy.Char8.unpack . Lazy.Base16.encode . encode + +instance IsString ReplaySeed where + fromString = aux . safeReadReplaySeed + where + aux :: Maybe ReplaySeed -> ReplaySeed + aux Nothing = error "ReplaySeed: invalid seed" + aux (Just s) = s + +safeReadReplaySeed :: String -> Maybe ReplaySeed +safeReadReplaySeed = parseReplaySeed + +#if MIN_VERSION_base(4,13,0) +parseReplaySeed :: forall m. MonadFail m => String -> m ReplaySeed +#else +parseReplaySeed :: forall m. Monad m => String -> m ReplaySeed +#endif + +parseReplaySeed str = do + raw <- case Lazy.Base16.decode (Lazy.Char8.pack str) of + Left err -> fail err + Right x -> return x + case decodeOrFail raw of + Left (_, _, err) -> fail err + Right (_, _, x) -> return x diff --git a/src/Test/Falsify/Internal/Driver/Tasty.hs b/src/Test/Falsify/Internal/Driver/Tasty.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Internal/Driver/Tasty.hs @@ -0,0 +1,176 @@ +{-# OPTIONS_GHC -Wno-orphans #-} +-- | Tasty integration +-- +-- This are the internal guts of the integration. Publicly visible API lives in +-- "Test.Tasty.Falsify". +module Test.Falsify.Internal.Driver.Tasty ( + -- * Test property + testProperty + -- * Configure test behaviour + , TestOptions(..) + , Verbose(..) + , ExpectFailure(..) + , testPropertyWith + ) where + +import Prelude hiding (log) + +import Data.Default +import Data.Maybe +import Data.Proxy +import Data.Tagged +import Test.Tasty +import Test.Tasty.Options (IsOption(..), OptionSet) +import Test.Tasty.Providers (IsTest(..)) + +import qualified Test.Tasty.Options as Tasty + +import Test.Falsify.Internal.Driver +import Test.Falsify.Internal.Driver.ReplaySeed +import Test.Falsify.Internal.Property + +import qualified Options.Applicative as Opts +import qualified Test.Tasty.Providers as Tasty + +{------------------------------------------------------------------------------- + Tasty integration +-------------------------------------------------------------------------------} + +data Test = Test TestOptions (Property' String ()) + +data TestOptions = TestOptions { + -- | Do we expect this test to fail? + expectFailure :: ExpectFailure + + -- | Override verbose mode for this test + , overrideVerbose :: Maybe Verbose + + -- | Override the maximum number of shrink steps for this test + , overrideMaxShrinks :: Maybe Word + + -- | Override the number of tests + , overrideNumTests :: Maybe Word + + -- | Override how many tests can be discarded per successful test + , overrideMaxRatio :: Maybe Word + } + +instance Default TestOptions where + def = TestOptions { + expectFailure = DontExpectFailure + , overrideVerbose = Nothing + , overrideMaxShrinks = Nothing + , overrideNumTests = Nothing + , overrideMaxRatio = Nothing + } + +instance IsTest Test where + -- @tasty@ docs (1.4.3) explicitly say to ignore the @reportProgress@ argument + run opts (Test testOpts prop) _reportProgress = + toTastyResult . renderTestResult verbose (expectFailure testOpts) <$> + falsify driverOpts prop + where + verbose :: Verbose + verbose = fromMaybe (Tasty.lookupOption opts) (overrideVerbose testOpts) + + driverOpts :: Options + driverOpts = + maybe id + (\x o -> o{maxShrinks = Just x}) + (overrideMaxShrinks testOpts) + $ maybe id + (\x o -> o{tests = x}) + (overrideNumTests testOpts) + $ maybe id + (\x o -> o{maxRatio = x}) + (overrideMaxRatio testOpts) + $ driverOptions opts + + testOptions = Tagged [ + Tasty.Option $ Proxy @Verbose + , Tasty.Option $ Proxy @Tests + , Tasty.Option $ Proxy @MaxShrinks + , Tasty.Option $ Proxy @Replay + , Tasty.Option $ Proxy @MaxRatio + ] + +toTastyResult :: RenderedTestResult -> Tasty.Result +toTastyResult RenderedTestResult{testPassed, testOutput} + | testPassed = Tasty.testPassed testOutput + | otherwise = Tasty.testFailed testOutput + +{------------------------------------------------------------------------------- + User API +-------------------------------------------------------------------------------} + +-- | Generalization of 'testPropertyWith' using default options +testProperty :: TestName -> Property' String () -> TestTree +testProperty = testPropertyWith def + +testPropertyWith :: TestOptions -> TestName -> Property' String () -> TestTree +testPropertyWith testOpts name = Tasty.singleTest name . Test testOpts + +{------------------------------------------------------------------------------- + Options specific to the tasty test runner + + Not all of these options are command line options; some are set on a + test-by-test basis, such as 'ExpectFailure'. +-------------------------------------------------------------------------------} + +instance IsOption Verbose where + defaultValue = NotVerbose + parseValue = fmap (\b -> if b then Verbose else NotVerbose) + . Tasty.safeReadBool + optionName = Tagged $ "falsify-verbose" + optionHelp = Tagged $ "Show the generated test cases" + optionCLParser = Tasty.mkFlagCLParser mempty Verbose + +{------------------------------------------------------------------------------- + Options + + NOTE: If we add another option here, we must also add it in 'testOptions'. +-------------------------------------------------------------------------------} + +newtype Tests = Tests { getTests :: Word } +newtype MaxShrinks = MaxShrinks { getMaxShrinks :: Maybe Word } +newtype Replay = Replay { getReplay :: Maybe ReplaySeed } +newtype MaxRatio = MaxRatio { getMaxRatio :: Word } + +instance IsOption Tests where + defaultValue = Tests (tests def) + parseValue = fmap Tests . Tasty.safeRead . filter (/= '_') + optionName = Tagged "falsify-tests" + optionHelp = Tagged "Number of test cases to generate" + +instance IsOption MaxShrinks where + defaultValue = MaxShrinks (maxShrinks def) + parseValue = fmap (MaxShrinks . Just) . Tasty.safeRead + optionName = Tagged "falsify-shrinks" + optionHelp = Tagged "Random seed to use for replaying a previous test run" + +instance IsOption Replay where + defaultValue = Replay (replay def) + parseValue = fmap (Replay . Just) . safeReadReplaySeed + optionName = Tagged "falsify-replay" + optionHelp = Tagged "Random seed to use for replaying test" + optionCLParser = Opts.option readReplaySeed $ mconcat [ + Opts.long $ untag $ optionName @Replay + , Opts.help $ untag $ optionHelp @Replay + ] + where + readReplaySeed :: Opts.ReadM Replay + readReplaySeed = Opts.str >>= fmap (Replay . Just) . parseReplaySeed + +instance IsOption MaxRatio where + defaultValue = MaxRatio (maxRatio def) + parseValue = fmap MaxRatio . Tasty.safeRead . filter (/= '_') + optionName = Tagged "falsify-max-ratio" + optionHelp = Tagged "Maximum number of discarded tests per successful test" + +driverOptions :: OptionSet -> Options +driverOptions opts = Options { + tests = getTests $ Tasty.lookupOption opts + , maxShrinks = getMaxShrinks $ Tasty.lookupOption opts + , replay = getReplay $ Tasty.lookupOption opts + , maxRatio = getMaxRatio $ Tasty.lookupOption opts + } diff --git a/src/Test/Falsify/Internal/Generator.hs b/src/Test/Falsify/Internal/Generator.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Internal/Generator.hs @@ -0,0 +1,26 @@ +-- | Export the public API of the generator, hiding implementation details. +-- +-- This is the only module that should import from +-- @Test.Falsify.Internal.Generator.*@. +-- +-- Intended for unqualified import. +module Test.Falsify.Internal.Generator ( + Gen -- opaque + , bindWithoutShortcut + -- * Execution + , runGen + , shrinkFrom + -- * Primitive generators + , prim + , primWith + , exhaustive + , captureLocalTree + -- * Generator independence + , bindIntegral + , perturb + -- * Combinators + , withoutShrinking + ) where + +import Test.Falsify.Internal.Generator.Definition +import Test.Falsify.Internal.Generator.Shrinking diff --git a/src/Test/Falsify/Internal/Generator/Definition.hs b/src/Test/Falsify/Internal/Generator/Definition.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Internal/Generator/Definition.hs @@ -0,0 +1,230 @@ +module Test.Falsify.Internal.Generator.Definition ( + -- * Definition + Gen(..) + , bindWithoutShortcut + -- * Primitive generators + , prim + , primWith + , exhaustive + , captureLocalTree + -- * Generator independence + , bindIntegral + , perturb + -- * Combinators + , withoutShrinking + ) where + +import Control.Monad +import Control.Selective +import Data.List.NonEmpty (NonEmpty((:|))) +import Data.Word +import Optics.Core (Lens', (%)) + +import qualified Optics.Core as Optics + +import Data.Falsify.Integer (Bit(..), encIntegerEliasG) +import Test.Falsify.Internal.SampleTree (SampleTree(..), Sample (..), pattern Inf) +import Test.Falsify.Internal.Search + +import qualified Test.Falsify.Internal.SampleTree as SampleTree + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +-- | Generator of a random value +-- +-- Generators can be combined through their 'Functor', 'Applicative' and 'Monad' +-- interfaces. The primitive generator is 'prim', but most users will probably +-- want to construct their generators using the predefined from +-- "Test.Falsify.Generator" as building blocks. +-- +-- Generators support \"internal integrated shrinking\". Shrinking is +-- /integrated/ in the sense of Hedgehog, meaning that we don't write a separate +-- shrinker at all, but the shrink behaviour is implied by the generator. For +-- example, if you have a generator @genList@ for a list of numbers, then +-- +-- > filter even <$> genList +-- +-- will only generate even numbers, and that property is automatically preserved +-- during shrinking. Shrinking is /internal/ in the sense of Hypothesis, meaning +-- that unlike in Hedgehog, shrinking works correctly even in the context of +-- monadic bind. For example, if you do +-- +-- > do n <- genListLength +-- > replicateM n someOtherGen +-- +-- then we can shrink @n@ and the results from @someOtherGen@ in any order (that +-- said, users may prefer to use the dedicated +-- 'Test.Falsify.Generator.Compound.list' generator for this purpose, which +-- improves on this in a few ways). +-- +-- NOTE: 'Gen' is /NOT/ an instance of 'Alternative'; this would not be +-- compatible with the generation of infinite data structures. For the same +-- reason, we do not have a monad transformer version of Gen either. +newtype Gen a = Gen { runGen :: SampleTree -> (a, [SampleTree]) } + deriving stock (Functor) + +instance Applicative Gen where + pure x = Gen $ \_st -> (x, []) + (<*>) = ap + +instance Monad Gen where + return = pure + x >>= f = Gen $ \(Inf s l r) -> + let (a, ls) = runGen x l + (b, rs) = runGen (f a) r + in (b, combineShrunk s (l :| ls) (r :| rs)) + +instance Selective Gen where + select e f = Gen $ \(Inf s l r) -> do + let (ma, ls) = runGen e l + case ma of + Left a -> + let (f', rs) = runGen f r + in (f' a, combineShrunk s (l :| ls) (r :| rs)) + Right b -> + (b, combineShrunk s (l :| ls) (r :| [])) + +-- | Combine shrunk left and right sample trees +-- +-- This is an internal function only. +combineShrunk :: + Sample + -> NonEmpty SampleTree -- ^ Original and shrunk left trees + -> NonEmpty SampleTree -- ^ Original and shrunk right trees + -> [SampleTree] +combineShrunk s (l :| ls) (r :| rs) = shortcut $ concat [ + [SampleTree s l' r | l' <- unlessMinimal l ls] + , [SampleTree s l r' | r' <- unlessMinimal r rs] + ] + where + -- We must be careful not to force @ls@/@rs@ if the tree is already minimal. + unlessMinimal :: SampleTree -> [a] -> [a] + unlessMinimal Minimal _ = [] + unlessMinimal _ xs = xs + + shortcut :: [SampleTree] -> [SampleTree] + shortcut [] = [] + shortcut ts = Minimal : ts + +-- | Varation on @(>>=)@ that doesn't apply the shortcut to 'Minimal' +-- +-- This function is primarily useful for debugging @falsify@ itself; users +-- will probably never need it. +bindWithoutShortcut :: Gen a -> (a -> Gen b) -> Gen b +bindWithoutShortcut x f = Gen $ \(Inf s l r) -> + let (a, ls) = runGen x l + (b, rs) = runGen (f a) r + in (b, combine s (l :| ls) (r :| rs)) + where + -- Variation on 'combineShrunk' that doesn't apply the shortcut + combine :: + Sample + -> NonEmpty SampleTree -- ^ Original and shrunk left trees + -> NonEmpty SampleTree -- ^ Original and shrunk right trees + -> [SampleTree] + combine s (l :| ls) (r :| rs) = concat [ + [SampleTree s l' r | l' <- ls] + , [SampleTree s l r' | r' <- rs] + ] + +{------------------------------------------------------------------------------- + Generator independence +-------------------------------------------------------------------------------} + +-- | Selective bind +-- +-- Unlike monadic bind, the RHS is generated and shrunk completely independently +-- for each different value of @a@ produced by the LHS. +-- +-- This is a generalization of 'bindS' to arbitrary integral values; it is also +-- much more efficient than 'bindS'. +-- +-- NOTE: This is only one way to make a generator independent. See 'perturb' +-- for more primitive combinator. +bindIntegral :: Integral a => Gen a -> (a -> Gen b) -> Gen b +bindIntegral x f = x >>= \a -> perturb a (f a) + +-- | Run generator on different part of the sample tree depending on @a@ +perturb :: Integral a => a -> Gen b -> Gen b +perturb a g = Gen $ \st -> + let (b, shrunk) = runGen g (Optics.view lens st) + in (b, map (\st' -> Optics.set lens st' st) shrunk) + where + lens :: Lens' SampleTree SampleTree + lens = computeLens (encIntegerEliasG $ fromIntegral a) + + computeLens :: [Bit] -> Lens' SampleTree SampleTree + computeLens [] = Optics.castOptic Optics.simple + computeLens (O : bs) = SampleTree.left % computeLens bs + computeLens (I : bs) = SampleTree.right % computeLens bs + +{------------------------------------------------------------------------------- + Primitive generators +-------------------------------------------------------------------------------} + +-- | Uniform selection of 'Word64', shrinking towards 0, using binary search +-- +-- This is a primitive generator; most users will probably not want to use this +-- generator directly. +prim :: Gen Word64 +prim = + SampleTree.sampleValue <$> + primWith (binarySearch . SampleTree.sampleValue) + +-- | Generalization of 'prim' that allows to override the shrink behaviour +-- +-- This is only required in rare circumstances. Most users will probably never +-- need to use this generator. +primWith :: (Sample -> [Word64]) -> Gen Sample +primWith f = Gen $ \(Inf s l r) -> ( + s + , (\s' -> SampleTree (Shrunk s') l r) <$> f s + ) + +-- | Generate arbitrary value @x <= n@ +-- +-- Unlike 'prim', 'exhaustive' does not execute binary search. Instead, /all/ +-- smaller values are considered. This is potentially very expensive; the +-- primary use case for this generator is testing shrinking behaviour, where +-- binary search can lead to some unpredicatable results. +-- +-- This does /NOT/ do uniform selection: for small @n@, the generator will with +-- overwhelming probability produce @n@ itself as initial value. +-- +-- This is a primitive generator; most users will probably not want to use this +-- generator directly. +exhaustive :: Word64 -> Gen Word64 +exhaustive n = + min n . SampleTree.sampleValue <$> + primWith (completeSearch . SampleTree.sampleValue) + where + completeSearch :: Word64 -> [Word64] + completeSearch 0 = [] + completeSearch x = takeWhile (<= n) [0 .. pred x] + +-- | Capture the local sample tree +-- +-- This generator does not shrink. +captureLocalTree :: Gen SampleTree +captureLocalTree = Gen $ \st -> (st, []) + +{------------------------------------------------------------------------------- + Shrinking combinators +-------------------------------------------------------------------------------} + +-- | Disable shrinking in the given generator +-- +-- Due to the nature of internal shrinking, it is always possible that a +-- generator gets reapplied to samples that were shrunk wrt to a /different/ +-- generator. In this sense, 'withoutShrinking' should be considered to be a +-- hint only. +-- +-- This function is only occassionally necessary; most users will probably not +-- need to use it. +withoutShrinking :: Gen a -> Gen a +withoutShrinking (Gen g) = Gen $ aux . g + where + aux :: (a, [SampleTree]) -> (a, [SampleTree]) + aux (outcome, _) = (outcome, []) diff --git a/src/Test/Falsify/Internal/Generator/Shrinking.hs b/src/Test/Falsify/Internal/Generator/Shrinking.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Internal/Generator/Shrinking.hs @@ -0,0 +1,169 @@ +module Test.Falsify.Internal.Generator.Shrinking ( + -- * Shrinking + shrinkFrom + -- * With full history + , ShrinkExplanation(..) + , ShrinkHistory(..) + , IsValidShrink(..) + , limitShrinkSteps + , shrinkHistory + , shrinkOutcome + ) where + +import Data.Bifunctor +import Data.Either +import Data.List.NonEmpty (NonEmpty((:|))) + +import Test.Falsify.Internal.Generator.Definition +import Test.Falsify.Internal.SampleTree (SampleTree(..)) + +{------------------------------------------------------------------------------- + Explanation +-------------------------------------------------------------------------------} + +-- | Shrink explanation +-- +-- @p@ is the type of \"positive\" elements that satisfied the predicate (i.e., +-- valid shrinks), and @n@ is the type of \"negative\" which didn't. +data ShrinkExplanation p n = ShrinkExplanation { + -- | The value we started, before shrinking + initial :: p + + -- | The full shrink history + , history :: ShrinkHistory p n + } + deriving (Show) + +-- | Shrink explanation +data ShrinkHistory p n = + -- | We successfully executed a single shrink step + ShrunkTo p (ShrinkHistory p n) + + -- | We could no shrink any further + -- + -- We also record all rejected next steps. This is occasionally useful when + -- trying to figure out why a value didn't shrink any further (what did it + -- try to shrink to?) + | ShrinkingDone [n] + + -- | We stopped shrinking early + -- + -- This is used when the number of shrink steps is limited. + | ShrinkingStopped + deriving (Show) + +limitShrinkSteps :: Maybe Word -> ShrinkExplanation p n -> ShrinkExplanation p n +limitShrinkSteps Nothing = id +limitShrinkSteps (Just limit) = \case + ShrinkExplanation{initial, history} -> + ShrinkExplanation{ + initial + , history = go limit history + } + where + go :: Word -> ShrinkHistory p n -> ShrinkHistory p n + go 0 (ShrunkTo _ _) = ShrinkingStopped + go n (ShrunkTo x xs) = ShrunkTo x (go (pred n) xs) + go _ (ShrinkingDone rej) = ShrinkingDone rej + go _ ShrinkingStopped = ShrinkingStopped + +-- | Simplify the shrink explanation to keep only the shrink history +shrinkHistory :: ShrinkExplanation p n -> NonEmpty p +shrinkHistory = \(ShrinkExplanation unshrunk shrunk) -> + unshrunk :| go shrunk + where + go :: ShrinkHistory p n -> [p] + go (ShrunkTo x xs) = x : go xs + go (ShrinkingDone _) = [] + go ShrinkingStopped = [] + +-- | The final shrunk value, as well as all rejected /next/ shrunk steps +-- +-- The list of rejected next steps is +-- +-- * @Nothing@ if shrinking was terminated early ('limitShrinkSteps') +-- * @Just []@ if the final value truly is minimal (typically, it is only +-- minimal wrt to a particular properly, but not the minimal value that a +-- generator can produce). +shrinkOutcome :: forall p n. ShrinkExplanation p n -> (p, Maybe [n]) +shrinkOutcome = \ShrinkExplanation{initial, history} -> + go initial history + where + go :: p -> ShrinkHistory p n -> (p, Maybe [n]) + go _ (ShrunkTo p h) = go p h + go p (ShrinkingDone ns) = (p, Just ns) + go p ShrinkingStopped = (p, Nothing) + +{------------------------------------------------------------------------------- + Mapping +-------------------------------------------------------------------------------} + +instance Functor (ShrinkExplanation p) where + fmap = second + +instance Functor (ShrinkHistory p) where + fmap = second + +instance Bifunctor ShrinkExplanation where + bimap f g ShrinkExplanation{initial, history} = ShrinkExplanation{ + initial = f initial + , history = bimap f g history + } + +instance Bifunctor ShrinkHistory where + bimap f g = \case + ShrunkTo truncated history -> + ShrunkTo (f truncated) (bimap f g history) + ShrinkingDone rejected -> + ShrinkingDone (map g rejected) + ShrinkingStopped -> + ShrinkingStopped + +{------------------------------------------------------------------------------- + Shrinking +-------------------------------------------------------------------------------} + +-- | Does a given shrunk value represent a valid shrink step? +data IsValidShrink p n = + ValidShrink p + | InvalidShrink n + deriving stock (Show) + +-- | Find smallest value that the generator can produce and still satisfies +-- the predicate. +-- +-- Returns the full shrink history. +-- +-- To avoid boolean blindness, we use different types for values that satisfy +-- the property and values that do not. +-- +-- This is lazy in the shrink history; see 'limitShrinkSteps' to limit the +-- number of shrinking steps. +shrinkFrom :: forall a p n. + (a -> IsValidShrink p n) + -> Gen a + -> (p, [SampleTree]) -- ^ Initial result of the generator + -> ShrinkExplanation p n +shrinkFrom prop gen = \(p, shrunk) -> + ShrinkExplanation p $ go shrunk + where + go :: [SampleTree] -> ShrinkHistory p n + go shrunk = + -- Shrinking is a greedy algorithm: we go with the first candidate that + -- works, and discard the others. + -- + -- NOTE: 'partitionEithers' is lazy enough: + -- + -- > head . fst $ partitionEithers [Left True, undefined] == True + case partitionEithers candidates of + ([], rejected) -> ShrinkingDone rejected + ((p, shrunk'):_, _) -> ShrunkTo p $ go shrunk' + where + candidates :: [Either (p, [SampleTree]) n] + candidates = map consider $ map (runGen gen) shrunk + + consider :: (a, [SampleTree]) -> Either (p, [SampleTree]) n + consider (a, shrunk) = + case prop a of + ValidShrink p -> Left (p, shrunk) + InvalidShrink n -> Right n diff --git a/src/Test/Falsify/Internal/Property.hs b/src/Test/Falsify/Internal/Property.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Internal/Property.hs @@ -0,0 +1,470 @@ +{-# LANGUAGE CPP #-} + +-- | Properties +-- +-- Intended for unqualified import. +module Test.Falsify.Internal.Property ( + -- * Property + Property' -- opaque + , runProperty + -- * Test results + , TestResult(..) + , resultIsValidShrink + -- * State + , TestRun(..) + , Log(..) + , LogEntry(..) + -- * Running generators + , gen + , genWith + -- * 'Property' features + , testFailed + , info + , assert + , discard + , label + , collect + -- * Testing shrinking + , testShrinking + , testMinimum + -- * Testing generators + , testGen + , testGen' + , testShrinkingOfGen + ) where + +import Prelude hiding (log) + +import Control.Monad +import Control.Monad.State +import Data.Foldable (toList) +import Data.List.NonEmpty (NonEmpty) +import Data.Map (Map) +import Data.Maybe (fromMaybe) +import Data.Set (Set) +import GHC.Stack + +import qualified Data.Map as Map +import qualified Data.Set as Set + +#if !MIN_VERSION_base(4,13,0) +import Control.Monad.Fail (MonadFail(..)) +#endif + +import Test.Falsify.Generator (Gen) +import Test.Falsify.Internal.Generator.Shrinking +import Test.Falsify.Predicate (Predicate, (.$)) + +import qualified Test.Falsify.Generator as Gen +import qualified Test.Falsify.Internal.Generator as Gen +import qualified Test.Falsify.Predicate as P + +{------------------------------------------------------------------------------- + Information about a test run +-------------------------------------------------------------------------------} + +data TestRun = TestRun { + runLog :: Log + + -- | Did we generate any values in this test run? + -- + -- If not, there is no point running the test more than once (with + -- different seeds), since the test is deterministic. + , runDeterministic :: Bool + + -- | Labels + , runLabels :: Map String (Set String) + } + deriving (Show) + +data LogEntry = + -- | Generated a value + -- + -- We record the value that was generated as well as /where/ we generated it + Generated CallStack String + + -- | Some additional information + | Info String + deriving (Show) + +-- | Log of the events happened during a test run +-- +-- The events are recorded in reverse chronological order +newtype Log = Log [LogEntry] + deriving (Show) + +initTestRun :: TestRun +initTestRun = TestRun { + runLog = Log [] + , runDeterministic = True + , runLabels = Map.empty + } + +-- | Append log from another test run to the current test run +-- +-- This is an internal function, used when testing shrinking to include the runs +-- from an unshrunk test and a shrunk test. +appendLog :: Log -> Property' e () +appendLog (Log log') = mkProperty $ \run@TestRun{runLog = Log log} -> return ( + TestPassed () + , run{runLog = Log $ log' ++ log} + ) + +{------------------------------------------------------------------------------- + Test result +-------------------------------------------------------------------------------} + +-- | Test result +data TestResult e a = + -- | Test was successful + -- + -- Under normal circumstances @a@ will be @()@. + TestPassed a + + -- | Test failed + | TestFailed e + + -- | Test was discarded + -- + -- This is neither a failure nor a success, but instead is a request to + -- discard this PRNG seed and try a new one. + | TestDiscarded + deriving stock (Show, Functor) + +-- | A test result is a valid shrink step if the test still fails +resultIsValidShrink :: + (TestResult e a, TestRun) + -> IsValidShrink (e, TestRun) (Maybe a, TestRun) +resultIsValidShrink (result, run) = + case result of + TestFailed e -> ValidShrink (e , run) + TestDiscarded -> InvalidShrink (Nothing , run) + TestPassed a -> InvalidShrink (Just a , run) + +{------------------------------------------------------------------------------- + Monad-transformer version of 'TestResult' +-------------------------------------------------------------------------------} + +newtype TestResultT e m a = TestResultT { + runTestResultT :: m (TestResult e a) + } + deriving (Functor) + +instance Monad m => Applicative (TestResultT e m) where + pure x = TestResultT $ pure (TestPassed x) + (<*>) = ap + +instance Monad m => Monad (TestResultT e m) where + return = pure + x >>= f = TestResultT $ runTestResultT x >>= \case + TestPassed a -> runTestResultT (f a) + TestFailed e -> pure $ TestFailed e + TestDiscarded -> pure $ TestDiscarded + +{------------------------------------------------------------------------------- + Definition + + The @Property@ type synonym for properties that use strings are errors is + defined in "Test.Falsify.Property". We do not define it here, so that we + cannot by mistake make a function less polymorphic than it should be. +-------------------------------------------------------------------------------} + +-- | Property +-- +-- A 'Property' is a generator that can fail and keeps a track of some +-- information about the test run. +-- +-- In most cases, you will probably want to use 'Test.Falsify.Property.Property' +-- instead, which fixes @e@ at 'String'. +newtype Property' e a = WrapProperty { + unwrapProperty :: TestResultT e (StateT TestRun Gen) a + } + deriving newtype (Functor, Applicative, Monad) + +-- | Construct property +-- +-- This is a low-level function for internal use only. +mkProperty :: (TestRun -> Gen (TestResult e a, TestRun)) -> Property' e a +mkProperty = WrapProperty . TestResultT . StateT + +-- | Run property +runProperty :: Property' e a -> Gen (TestResult e a, TestRun) +runProperty = flip runStateT initTestRun . runTestResultT . unwrapProperty + +{------------------------------------------------------------------------------- + 'Property' features +-------------------------------------------------------------------------------} + +-- | Test failure +testFailed :: e -> Property' e a +testFailed err = mkProperty $ \run -> return (TestFailed err, run) + +-- | Discard this test +discard :: Property' e a +discard = mkProperty $ \run -> return (TestDiscarded, run) + +-- | Log some additional information about the test +-- +-- This will be shown in verbose mode. +info :: String -> Property' e () +info msg = + mkProperty $ \run@TestRun{runLog = Log log} -> return ( + TestPassed () + , run{runLog = Log $ Info msg : log} + ) + +-- | Fail the test if the predicate does not hold +assert :: Predicate '[] -> Property' String () +assert p = + case P.eval p of + Left err -> testFailed err + Right () -> return () + +-- | Variation on 'collect' that does not rely on 'Show' +-- +-- See 'collect' for detailed discussion. +label :: String -> [String] -> Property' e () +label lbl vals = + mkProperty $ \run@TestRun{runLabels} -> return ( + TestPassed () + , run{runLabels = Map.alter addValues lbl runLabels} + ) + where + addValues :: Maybe (Set String) -> Maybe (Set String) + addValues = Just . Set.union (Set.fromList vals) . fromMaybe Set.empty + +-- | Label this test +-- +-- See also 'label', which does not rely on 'Show'. +-- +-- === Motivation +-- +-- Labelling is instrumental in understanding the distribution of test data. For +-- example, consider testing a binary tree type, and we want to test some +-- properties of an @insert@ operation (example from "How to specify it!" by +-- John Hughes): +-- +-- > prop_insert_insert :: Property () +-- > prop_insert_insert = do +-- > tree <- gen $ .. +-- > (k1, v1) <- gen $ .. +-- > (k2, v2) <- gen $ .. +-- > assert $ .. (insert k1 v1 $ insert k2 v2 $ tree) .. +-- +-- We might want to know in what percentage of tests @k1 == k2@: +-- +-- > collect "sameKey" [k1 == k2] +-- +-- When we do, @falsify@ will report in which percentage of tests the key +-- are the same, and in which percentage of tests they are not. +-- +-- === Labels with multiple values +-- +-- In general, a particular label can have multiple values in any given test +-- run. Given a test of @n@ test runs, for each value @v@ reported, @falsify@ +-- will report what percentage of the @n@ runs are labelled with @v@. That means +-- that these percentages /may/ not add up to 100%; indeed, if we had +-- +-- > collect "sameKey" [True] +-- > .. +-- > collect "sameKey" [False] +-- +-- or, equivalently, +-- +-- > collect "sameKey" [True, False] +-- +-- then /every/ test would have been reported as labelled with @True@ (100%@) +-- /as well as/ with @False@ (also 100%). Of course, if we do (like above) +-- +-- > collect "sameKey" [k1 == k2] +-- +-- each test will be labelled with /either/ @True@ /or/ @False@, and the +-- percentages /will/ add up to 100%. +-- +-- === Difference from QuickCheck +-- +-- Since you can call @collect@ anywhere in a property, it is natural that the +-- same label can have /multiple/ values in any given test run. In this regard, +-- @collect@ is closer to QuickCheck's @tabulate@. However, the statistics of +-- @tabulate@ can be difficult to interpret; QuickCheck reports the frequency of +-- a value as a percentage of the /total number of values collected/; the +-- frequency reported by @falsify@ here is always in terms of number of test +-- runs, like @collect@ does in QuickCheck. We therefore opted to use the name +-- @collect@ rather than @tabulate@. +collect :: Show a => String -> [a] -> Property' e () +collect l = label l . map show + +instance MonadFail (Property' String) where + fail = testFailed + +{------------------------------------------------------------------------------- + Running generators +-------------------------------------------------------------------------------} + +-- | Internal auxiliary +genWithCallStack :: forall e a. + CallStack -- ^ Explicit argument to avoid irrelevant entries + -- (users don't care that 'gen' uses 'genWith'). + -> (a -> Maybe String) -- ^ Entry to add to the log (if any) + -> Gen a -> Property' e a +genWithCallStack stack f g = mkProperty $ \run -> aux run <$> g + where + aux :: TestRun -> a -> (TestResult e a, TestRun) + aux run@TestRun{runLog = Log log} x = ( + TestPassed x + , run{ runLog = Log $ case f x of + Just entry -> Generated stack entry : log + Nothing -> log + , runDeterministic = False + } + ) + +-- | Generate value and add it to the log +gen :: (HasCallStack, Show a) => Gen a -> Property' e a +gen = genWithCallStack callStack (Just . show) + +-- | Generalization of 'gen' that doesn't depend on a 'Show' instance +-- +-- No log entry is added if 'Nothing'. +genWith :: HasCallStack => (a -> Maybe String) -> Gen a -> Property' e a +genWith = genWithCallStack callStack + +{------------------------------------------------------------------------------- + Internal auxiliary: testing shrinking +-------------------------------------------------------------------------------} + +-- | Construct random path through the property's shrink tree +genShrinkPath :: Property' e () -> Property' e' [(e, TestRun)] +genShrinkPath prop = do + st <- genWith (const Nothing) $ Gen.toShrinkTree (runProperty prop) + mPath <- genWith (const Nothing) $ Gen.path resultIsValidShrink st + aux mPath + where + aux :: + Either (Maybe (), TestRun) (NonEmpty (e, TestRun)) + -> Property' e' [(e, TestRun)] + aux (Left (Just (), _)) = return [] + aux (Left (Nothing, _)) = discard + aux (Right es) = return $ toList es + +{------------------------------------------------------------------------------- + Test shrinking +-------------------------------------------------------------------------------} + +-- | Test shrinking of a property +-- +-- A property is normally only shrunk when it /fails/. We do the same here: +-- if the property succeeds, we discard the test and try again. +-- +-- If the given property itself discards immediately, then this generator will +-- discard also; otherwise, only shrink steps are considered that do not lead +-- to a discard. +testShrinking :: forall e. + Show e + => Predicate [e, e] -> Property' e () -> Property' String () +testShrinking p prop = do + path <- genShrinkPath prop + case findCounterExample (toList path) of + Nothing -> + return () + Just (err, logBefore, logAfter) -> do + info "Before shrinking:" + appendLog logBefore + info "After shrinking:" + appendLog logAfter + testFailed err + where + findCounterExample :: [(e, TestRun)] -> Maybe (String, Log, Log) + findCounterExample = \case + [] -> Nothing + [_] -> Nothing + ((x, runX) : rest@((y, runY) : _)) -> + case P.eval $ p .$ ("original", x) .$ ("shrunk", y) of + Left err -> Just (err, runLog runX, runLog runY) + Right () -> findCounterExample rest + +-- | Test the minimum error thrown by the property +-- +-- If the given property passes, we will discard this test (in that case, there +-- is nothing to test); this test is also discarded if the given property +-- discards. +-- +-- NOTE: When testing a particular generator, you might still want to test with +-- some particular property in mind. Otherwise, the minimum value will always +-- simply be the value that the generator produces when given the @Minimal@ +-- sample tree. +testMinimum :: forall e. + Show e + => Predicate '[e] + -> Property' e () + -> Property' String () +testMinimum p prop = do + st <- genWith (const Nothing) $ Gen.captureLocalTree + case Gen.runGen (runProperty prop) st of + ((TestPassed (), _run), _shrunk) -> + -- The property passed; nothing to test + discard + ((TestDiscarded, _run), _shrunk) -> + -- The property needs to be discarded; discard this one, too + discard + ((TestFailed initErr, initRun), shrunk) -> do + let explanation :: ShrinkExplanation (e, TestRun) (Maybe (), TestRun) + explanation = shrinkFrom + resultIsValidShrink + (runProperty prop) + ((initErr, initRun), shrunk) + + minErr :: e + minRun :: TestRun + mRejected :: Maybe [(Maybe (), TestRun)] + ((minErr, minRun), mRejected) = shrinkOutcome explanation + + rejected :: [TestRun] + rejected = maybe [] (map snd) mRejected + + case P.eval $ p .$ ("minimum", minErr) of + Right () -> do + -- For a successful test, we add the full shrink history as info + -- This means that users can use verbose mode to see precisely + -- how the minimum value is reached, if they wish. + info "Shrink history:" + forM_ (shrinkHistory explanation) $ \(e, _run) -> + info $ show e + Left err -> do + appendLog (runLog minRun) + unless (null rejected) $ do + info "\nLogs for rejected potential next shrinks:" + forM_ (zip [0 :: Word ..] rejected) $ \(i, rej) -> do + info $ "\n** Rejected run " ++ show i + appendLog $ runLog rej + testFailed err + +{------------------------------------------------------------------------------- + Testing generators +-------------------------------------------------------------------------------} + +-- | Test output of the generator +testGen :: forall a. Show a => Predicate '[a] -> Gen a -> Property' String () +testGen p = testGen' $ \a -> P.eval $ p .$ ("generated", a) + +-- | Generalization of 'testGen' +testGen' :: forall e a b. (a -> Either e b) -> Gen a -> Property' e b +testGen' p g = WrapProperty $ TestResultT $ StateT $ \run -> + -- We do not use bind here to avoid introducing new shrinking shortcuts + aux run <$> g + where + aux :: TestRun -> a -> (TestResult e b, TestRun) + aux run a = ( + case p a of + Left e -> TestFailed e + Right b -> TestPassed b + , run{runDeterministic = False} + ) + +-- | Test shrinking of a generator +-- +-- We check /any/ shrink step that the generator can make (independent of any +-- property). +testShrinkingOfGen :: Show a => Predicate [a, a] -> Gen a -> Property' String () +testShrinkingOfGen p = testShrinking p . testGen' Left + diff --git a/src/Test/Falsify/Internal/Range.hs b/src/Test/Falsify/Internal/Range.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Internal/Range.hs @@ -0,0 +1,58 @@ +-- | Internal 'Range' API +module Test.Falsify.Internal.Range ( + -- * Definition + Range(..) + , ProperFraction(ProperFraction) + , Precision(..) + ) where + +import Data.Word +import GHC.Show +import GHC.Stack + +{------------------------------------------------------------------------------- + Proper frations +-------------------------------------------------------------------------------} + +-- | Value @x@ such that @0 <= x < 1@ +newtype ProperFraction = UnsafeProperFraction { getProperFraction :: Double } + deriving stock (Eq, Ord) + deriving newtype (Num, Fractional) + +-- | Show instance relies on the 'ProperFraction' pattern synonym +instance Show ProperFraction where + showsPrec p (UnsafeProperFraction f) = showParen (p >= appPrec1) $ + showString "ProperFraction " + . showsPrec appPrec1 f + +mkProperFraction :: HasCallStack => Double -> ProperFraction +mkProperFraction f + | 0 <= f && f < 1 = UnsafeProperFraction f + | otherwise = error $ "mkProperFraction: not a proper fraction: " ++ show f + +pattern ProperFraction :: Double -> ProperFraction +pattern ProperFraction f <- (getProperFraction -> f) + where + ProperFraction = mkProperFraction + +{-# COMPLETE ProperFraction #-} + +{------------------------------------------------------------------------------- + Precision +-------------------------------------------------------------------------------} + +-- | Precision (in bits) +newtype Precision = Precision Word8 + deriving stock (Show, Eq, Ord) + deriving newtype (Num, Enum) + +{------------------------------------------------------------------------------- + Range +-------------------------------------------------------------------------------} + +-- | Range of values +data Range a = + Constant a + | FromProperFraction Precision (ProperFraction -> a) + | Towards a [Range a] + deriving stock (Functor) diff --git a/src/Test/Falsify/Internal/SampleTree.hs b/src/Test/Falsify/Internal/SampleTree.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Internal/SampleTree.hs @@ -0,0 +1,196 @@ +-- | Sample tree +-- +-- Intended for qualified import. +-- +-- import Test.Falsify.Internal.SampleTree (SampleTree(..)) +-- import qualified Test.Falsify.Internal.SampleTree as SampleTree +module Test.Falsify.Internal.SampleTree ( + -- * Definition + SampleTree(..) + , Sample(..) + , pattern Inf + , sampleValue + -- * Lenses + , next + , left + , right + -- * Construction + , fromPRNG + , fromSeed + , minimal + , constant + -- * Combinators + , map + , mod + ) where + +import Prelude hiding (map, mod) +import qualified Prelude + +import Data.Word +import Optics.Core (Lens') +import System.Random.SplitMix + +import qualified Optics.Core as Optics + +{------------------------------------------------------------------------------- + Definition +-------------------------------------------------------------------------------} + +-- | Sample tree +-- +-- A sample tree is a (conceptually and sometimes actually) infinite tree +-- representing drawing values from and splitting a PRNG. +data SampleTree = + -- | Default constructor + -- + -- The type of ST is really + -- + -- > ST :: Word64 & (SampleTree * SampleTree) -> SampleTree + -- + -- where `(&)` is the additive conjunction from linear logic. In other + -- words, the intention is that /either/ the @Word64@ is used, /or/ + -- the pair of subtrees; put another way, we /either/ draw a value from the + -- PRNG, /or/ split it into two new PRNGs. See 'next' and 'split'. + SampleTree Sample SampleTree SampleTree + + -- | Minimal tree (0 everywhere) + -- + -- This constructor allows us to represent an infinite tree in a finite way + -- and, importantly, /recognize/ a tree that is minimal everywhere. This is + -- necessary when shrinking in the context of generators that generate + -- infinitely large values. + | Minimal + deriving (Show) + +{------------------------------------------------------------------------------- + Samples +-------------------------------------------------------------------------------} + +-- | Sample +-- +-- The samples in the 'SampleTree' record if they were the originally produced +-- sample, or whether they have been shrunk. +data Sample = + NotShrunk Word64 + | Shrunk Word64 + deriving (Show, Eq, Ord) + +sampleValue :: Sample -> Word64 +sampleValue (NotShrunk s) = s +sampleValue (Shrunk s) = s + +{------------------------------------------------------------------------------- + Views +-------------------------------------------------------------------------------} + +view :: SampleTree -> (Sample, SampleTree, SampleTree) +view Minimal = (Shrunk 0, Minimal, Minimal) +view (SampleTree s l r) = (s, l, r) + +-- | Pattern synonym for treating the sample tree as infinite +pattern Inf :: Sample -> SampleTree -> SampleTree -> SampleTree +pattern Inf s l r <- (view -> (s, l, r)) + +{-# COMPLETE Inf #-} + +{------------------------------------------------------------------------------- + Lenses + + NOTE: The setter part of these lenses leaves 'Minimal' sample tree unchanged. +-------------------------------------------------------------------------------} + +next :: Lens' SampleTree Sample +next = Optics.lens getter setter + where + getter :: SampleTree -> Sample + getter (Inf s _ _) = s + + setter :: SampleTree -> Sample -> SampleTree + setter Minimal _ = Minimal + setter (SampleTree _ l r) s = SampleTree s l r + +left :: Lens' SampleTree SampleTree +left = Optics.lens getter setter + where + getter :: SampleTree -> SampleTree + getter (Inf _ l _) = l + + setter :: SampleTree -> SampleTree -> SampleTree + setter Minimal _ = Minimal + setter (SampleTree s _ r) l = SampleTree s l r + +right :: Lens' SampleTree SampleTree +right = Optics.lens getter setter + where + getter :: SampleTree -> SampleTree + getter (Inf _ _ r) = r + + setter :: SampleTree -> SampleTree -> SampleTree + setter Minimal _ = Minimal + setter (SampleTree s l _) r = SampleTree s l r + +{------------------------------------------------------------------------------- + Construction +-------------------------------------------------------------------------------} + +fromPRNG :: SMGen -> SampleTree +fromPRNG = go + where + go :: SMGen -> SampleTree + go g = + let (n, _) = nextWord64 g + (l, r) = splitSMGen g + in SampleTree (NotShrunk n) (go l) (go r) + +fromSeed :: Word64 -> SampleTree +fromSeed = fromPRNG . mkSMGen + +-- | Minimal sample tree +-- +-- Generators should produce the \"simplest\" value when given this tree, +-- for some suitable application-specific definition of \"simple\". +minimal :: SampleTree +minimal = Minimal + +-- | Sample tree that is the given value everywhere +-- +-- This is primarily useful for debugging. +constant :: Word64 -> SampleTree +constant s = go + where + go :: SampleTree + go = SampleTree (NotShrunk s) go go + +{------------------------------------------------------------------------------- + Combinators +-------------------------------------------------------------------------------} + +-- | Map function over all random samples in the tree +-- +-- Precondition: the function must preserve zeros: +-- +-- > f 0 == 0 +-- +-- This means that we have +-- +-- > map f M == M +-- +-- This is primarily useful for debugging. +map :: (Word64 -> Word64) -> SampleTree -> SampleTree +map f = go + where + go :: SampleTree -> SampleTree + go (SampleTree s l r) = SampleTree (mapSample s) (go l) (go r) + go Minimal = Minimal + + mapSample :: Sample -> Sample + mapSample (NotShrunk s) = NotShrunk (f s) + mapSample (Shrunk s) = Shrunk (f s) + +-- | Apply @mod m@ at every sample in the tree +-- +-- This is primarily useful for debugging. +mod :: Word64 -> SampleTree -> SampleTree +mod m = map (\s -> s `Prelude.mod` m) + diff --git a/src/Test/Falsify/Internal/Search.hs b/src/Test/Falsify/Internal/Search.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Internal/Search.hs @@ -0,0 +1,103 @@ +module Test.Falsify.Internal.Search ( + -- * Binary search + binarySearch + , binarySearchNoParityBias + ) where + +import Data.Bits +import Data.List (nub) +import Data.Word + +{------------------------------------------------------------------------------- + Binary search +-------------------------------------------------------------------------------} + +-- | Binary search +-- +-- Compute one step of a binary search algorithm. +-- +-- Examples: +-- +-- > binarySearch 0 == [] +-- > binarySearch 1 == [0] +-- > binarySearch 2 == [0,1] +-- > binarySearch 3 == [0,2] +-- > binarySearch 4 == [0,2,3] +-- > binarySearch 5 == [0,3,4] +-- > binarySearch 6 == [0,3,5] +-- > binarySearch 7 == [0,4,6] +-- > binarySearch 8 == [0,4,6,7] +-- > binarySearch 9 == [0,5,7,8] +-- > binarySearch 10 == [0,5,8,9] +-- > binarySearch 16 == [0,8,12,14,15] +-- > binarySearch 127 == [0,64,96,112,120,124,126] +-- > binarySearch 128 == [0,64,96,112,120,124,126,127] +-- +-- The gap between each successive number halves at each step. +-- +-- NOTE: 'binarySearch' introduces a bias for even numbers: when shrinking +-- succeeds with the first (non-zero) option, the number is basically halved +-- each at step; since halving an even number results in another even number, +-- and halving an odd number /also/ results in an even number, this results in a +-- strong bias towards even numbers. See also 'binarySearchNoParityBias'. +binarySearch :: Word64 -> [Word64] +binarySearch = go 0 . deltas + where + go :: Word64 -> [Word64] -> [Word64] + go _ [] = [] + go n (d:ds) = n : go (n + d) ds + +-- | Binary search without parity bias +-- +-- For some cases the parity (even or odd) of a number is very important, and +-- unfotunately standard binary search is not very good at allowing search to +-- flip between even and odd. For example, if we start with 'maxBound', +-- /every/ possibly shrink value computed by 'binarySearch' is even. The +-- situation is less extreme for other numbers, but it's nonetheless something +-- we need to take into account. +-- +-- In this function we pair each possible shrunk value with the corresponding +-- value of opposite parity, ordered in such a way that we try to shrink to +-- opposite parity first. +-- +-- Examples: +-- +-- > binarySearchNoParityBias 0 == [] +-- > binarySearchNoParityBias 1 == [0] +-- > binarySearchNoParityBias 2 == [1,0] +-- > binarySearchNoParityBias 3 == [0,1,2] +-- > binarySearchNoParityBias 4 == [1,0,3,2] +-- > binarySearchNoParityBias 5 == [0,1,2,3,4] +-- > binarySearchNoParityBias 6 == [1,0,3,2,5,4] +-- > binarySearchNoParityBias 7 == [0,1,4,5,6] +-- > binarySearchNoParityBias 8 == [1,0,5,4,7,6] +-- > binarySearchNoParityBias 9 == [0,1,4,5,6,7,8] +-- > binarySearchNoParityBias 10 == [1,0,5,4,9,8] +-- > binarySearchNoParityBias 16 == [1,0,9,8,13,12,15,14] +-- > binarySearchNoParityBias 127 == [0,1,64,65,96,97,112,113,120,121,124,125,126] +-- > binarySearchNoParityBias 128 == [1,0,65,64,97,96,113,112,121,120,125,124,127,126] +binarySearchNoParityBias :: Word64 -> [Word64] +binarySearchNoParityBias y = + filter (< y) . nub . concatMap pairWithOpposite $ + binarySearch y + where + pairWithOpposite :: Word64 -> [Word64] + pairWithOpposite x + | even x == even y = [x `xor` 1, x] + | otherwise = [x, x `xor` 1] + +-- | Auxiliary to 'binarySearch' +-- +-- Given a number @n@, compute a set of steps @n1, n2, ..@ such that +-- @sum [n1, n2, ..] == n@, the distance between each subsequent step +-- is halved, and all steps are non-zero. For example: +-- +-- > deltas 200 == [100,50,25,12,6,3,2,1,1] +deltas :: Word64 -> [Word64] +deltas 0 = [] +deltas 1 = [1] +deltas n + | even n = mid : deltas mid + | otherwise = mid + 1 : deltas mid + where + mid = n `div` 2 diff --git a/src/Test/Falsify/Predicate.hs b/src/Test/Falsify/Predicate.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Predicate.hs @@ -0,0 +1,566 @@ +-- | Predicates +-- +-- Intended for qualified import. + +-- > import Test.Falsify.Predicate (Predicate, (.$)) +-- > import qualified Test.Falsify.Predicate as P +module Test.Falsify.Predicate ( + Predicate -- opaque + -- * Expressions + , Expr -- opaque + , prettyExpr + -- * Functions + , Fn -- opaque + , fn + , fnWith + , transparent + -- * Construction + , alwaysPass + , alwaysFail + , unary + , binary + -- * Auxiliary construction + , satisfies + , relatedBy + -- * Combinators + , dot + , on + , flip + , matchEither + , matchBool + -- * Evaluation and partial evaluation + , eval + , (.$) + , at + -- * Specific predicates + , eq + , ne + , lt + , le + , gt + , ge + , towards + , expect + , between + , even + , odd + , elem + ) where + +import Prelude hiding (all, flip, even, odd, pred, elem) +import qualified Prelude + +import Data.Bifunctor +import Data.Kind +import Data.List (intercalate) +import Data.Maybe (catMaybes) +import Data.SOP (NP(..), K(..), I(..), SListI) + +import qualified Data.SOP as SOP + +{------------------------------------------------------------------------------- + Small expression language +-------------------------------------------------------------------------------} + +-- | Variable +type Var = String + +-- | Simple expression language +-- +-- The internal details of this type are (currently) not exposed. +data Expr = + -- | Variable + Var Var + + -- | Application + | App Expr Expr + + -- | Non-associative infix operator + | Infix Var Expr Expr + +prettyExpr :: Expr -> String +prettyExpr = go False + where + go :: + Bool -- Does the context require brackets? + -> Expr -> String + go needsBrackets = \case + Var x -> x + App e1 e2 -> parensIf needsBrackets $ intercalate " " [ + go False e1 -- application is left associative + , go True e2 + ] + Infix op e1 e2 -> parensIf needsBrackets $ intercalate " " [ + go True e1 + , op + , go True e2 + ] + + parensIf :: Bool -> String -> String + parensIf False = id + parensIf True = \s -> "(" ++ s ++ ")" + +{------------------------------------------------------------------------------- + Functions +-------------------------------------------------------------------------------} + +-- | Function (used for composition of a 'Predicate' with a function) +data Fn a b = + -- | Function that is visible in rendered results + Visible Var (b -> String) (a -> b) + + -- | Function that should not be visible in rendered results + -- + -- See 'transparent' for an example. + | Transparent (a -> b) + +-- | Default constructor for a function +fn :: Show b => (Var, a -> b) -> Fn a b +fn (n, f) = fnWith (n, show, f) + +-- | Generalization of 'fn' that does not depend on 'Show' +fnWith :: (Var, b -> String, a -> b) -> Fn a b +fnWith (n, r, f) = Visible n r f + +-- | Function that should not be visible in any rendered failure +-- +-- Consider these two predicates: +-- +-- > p1, p2 :: Predicate '[Char, Char] +-- > p1 = P.eq `P.on` (P.fn "ord" ord) +-- > p2 = P.eq `P.on` (P.transparent ord) +-- +-- Both of these compare two characters on their codepoints (through 'ord'), but +-- they result in different failures. The first would give us something like +-- +-- > (ord x) /= (ord y) +-- > x : 'a' +-- > y : 'b' +-- > ord x: 97 +-- > ord y: 98 +-- +-- whereas the second might give us something like +-- +-- > x /= y +-- > x: 'a' +-- > y: 'b' +-- +-- which of these is more useful is of course application dependent. +transparent :: (a -> b) -> Fn a b +transparent = Transparent + +{------------------------------------------------------------------------------- + Decorated predicate inputs + + This is internal API. +-------------------------------------------------------------------------------} + +-- | Input to a 'Predicate' +data Input x = Input { + -- | Expression describing the input + inputExpr :: Expr + + -- | Rendered value of the input + , inputRendered :: String + + -- | The input proper + , inputValue :: x + } + +-- | Apply function to an argument +-- +-- If the funciton is visible, we also return the /input/ to the function +-- (so that we can render both the input and the output); we return 'Nothing' +-- for transparent functions. +applyFn :: Fn a b -> Input a -> (Input b, Maybe (Expr, String)) +applyFn (Visible n r f) x = ( + Input { + inputExpr = App (Var n) $ inputExpr x + , inputRendered = r $ f (inputValue x) + , inputValue = f $ inputValue x + } + , Just $ renderInput x + ) +applyFn (Transparent f) x = ( + Input { + inputExpr = inputExpr x + , inputRendered = inputRendered x + , inputValue = f $ inputValue x + } + , Nothing + ) + +renderInput :: Input x -> (Expr, String) +renderInput x = (inputExpr x, inputRendered x) + +renderInputs :: SListI xs => NP Input xs -> [(Expr, String)] +renderInputs xs = SOP.hcollapse $ SOP.hmap (K . renderInput) xs + +{------------------------------------------------------------------------------- + Definition + + 'Predicate' is a relatively deep embedding, so that we can provide more + powerful combinators. +-------------------------------------------------------------------------------} + +-- | Error message (when the predicate fails) +type Err = String + +-- | N-ary predicate +-- +-- A predicate of type +-- +-- > Predicate '[Int, Bool, Char, ..] +-- +-- is essentially a function @Int -> Bool -> Char -> .. -> Bool@, along with +-- some metadata about that function that allows us to render it in a human +-- readable way. In particular, we construct an 'Expr' for the values that the +-- predicate has been applied to. +data Predicate :: [Type] -> Type where + -- | Primitive generator + Prim :: (NP I xs -> Bool) -> (NP (K Expr) xs -> Err) -> Predicate xs + + -- | Predicate that always passes + Pass :: Predicate xs + + -- | Predicate that always fails + Fail :: Predicate xs + + -- | Conjunction + Both :: Predicate xs -> Predicate xs -> Predicate xs + + -- | Abstraction + Lam :: (x -> Predicate xs) -> Predicate (x ': xs) + + -- | Partial application + At :: Predicate (x : xs) -> Input x -> Predicate xs + + -- | Function compostion + Dot :: Predicate (x : xs) -> Fn y x -> Predicate (y : xs) + + -- | Analogue of 'Prelude.on' + On :: Predicate (x : x : xs) -> Fn y x -> Predicate (y : y : xs) + + -- | Analogue of 'Prelude.flip' + Flip :: Predicate (x : y : zs) -> Predicate (y : x : zs) + + -- | Choice + Choose :: + Predicate ( a : xs) + -> Predicate ( b : xs) + -> Predicate (Either a b : xs) + + -- | Predicate that ignores its argument + Const :: Predicate xs -> Predicate (x ': xs) + +instance Monoid (Predicate a) where mempty = Pass +instance Semigroup (Predicate a) where (<>) = Both + +-- | Primitive way to construct a predicate +-- +-- This is (currently) not part of the public API. +prim :: + (NP I xs -> Bool) + -- ^ Predicate to check + -> (NP (K Expr) xs -> Err) + -- ^ Produce error message, given the expressions describing the inputs + -> Predicate xs +prim = Prim + +{------------------------------------------------------------------------------- + Construction +-------------------------------------------------------------------------------} + +-- | Constant 'True' +alwaysPass :: Predicate xs +alwaysPass = Pass + +-- | Constant 'False' +alwaysFail :: Predicate xs +alwaysFail = Fail + +-- | Unary predicate +-- +-- This is essentially a function @a -> Bool@; see 'Predicate' for detailed +-- discussion. +unary :: + (a -> Bool) -- ^ The predicate proper + -> (Expr -> Err) -- ^ Error message, given 'Expr' describing the input + -> Predicate '[a] +unary p msg = + prim + (\(I x :* Nil) -> p x) + (\(K l :* Nil) -> msg l) + +-- | Binary predicate +-- +-- This is essentially a function @a -> b -> Bool@; see 'Predicate' for detailed +-- discussion. +binary :: + (a -> b -> Bool) -- ^ The predicate proper + -> (Expr -> Expr -> Err) -- ^ Error message, given 'Expr' describing inputs + -> Predicate [a, b] +binary p msg = + prim + (\(I x :* I y :* Nil) -> p x y) + (\(K lx :* K ly :* Nil) -> msg lx ly) + +{------------------------------------------------------------------------------- + Auxiliary construction +-------------------------------------------------------------------------------} + +-- | Specialization of 'unary' for unary relations +satisfies :: (Var, a -> Bool) -> Predicate '[a] +satisfies (n, p) = + unary p $ \x -> + prettyExpr $ Var "not" `App` (Var n `App` x) + +-- | Specialization of 'binary' for relations +relatedBy :: (Var, a -> b -> Bool) -> Predicate [a, b] +relatedBy (n, p) = + binary p $ \x y -> + prettyExpr $ Var "not" `App` (Var n `App` x `App` y) + +{------------------------------------------------------------------------------- + Combinators +-------------------------------------------------------------------------------} + +-- | Function composition (analogue of '(.)') +dot :: Predicate (x : xs) -> Fn y x -> Predicate (y : xs) +dot = Dot + +-- | Analogue of 'Prelude.on' +on :: Predicate (x : x : xs) -> Fn y x -> Predicate (y : y : xs) +on = On + +-- | Analogue of 'Prelude.flip' +flip :: Predicate (x : y : zs) -> Predicate (y : x : zs) +flip = Flip + +-- | Match on the argument, and apply whichever predicate is applicable. +matchEither :: + Predicate (a : xs) + -> Predicate (b : xs) + -> Predicate (Either a b : xs) +matchEither = Choose + +-- | Conditional +-- +-- This is a variation on 'choose' that provides no evidence for which branch is +-- taken. +matchBool :: + Predicate xs -- ^ Predicate to evaluate if the condition is true + -> Predicate xs -- ^ Predicate to evaluate if the condition is false + -> Predicate (Bool : xs) +matchBool t f = + matchEither (Const t) (Const f) `dot` transparent fromBool + where + fromBool :: Bool -> Either () () + fromBool True = Left () + fromBool False = Right () + +{------------------------------------------------------------------------------- + Failures +-------------------------------------------------------------------------------} + +data Failure = Failure { + failureErr :: Err + , failureInputs :: [(Expr, String)] + } + +addInputs :: [(Expr, String)] -> Failure -> Failure +addInputs new Failure{failureErr, failureInputs} = Failure{ + failureErr + , failureInputs = new ++ failureInputs + } + +prettyFailure :: Failure -> String +prettyFailure Failure{failureErr, failureInputs} = + unlines $ failureErr : map (uncurry padInput) failureInputs + where + maxLabelLen :: Int + maxLabelLen = maximum $ map (length . prettyExpr . fst) failureInputs + + padInput :: Expr -> String -> String + padInput e v = padTo maxLabelLen (prettyExpr e) ++ ": " ++ v + + padTo :: Int -> String -> String + padTo n xs = xs ++ replicate (n - length xs) ' ' + +{------------------------------------------------------------------------------- + Generalized evaluation + + This is internal API. Only the top-level 'eval' is exported. +-------------------------------------------------------------------------------} + +evalPrim :: + SListI xs + => (NP I xs -> Bool) + -> (NP (K Expr) xs -> Err) + -> NP Input xs + -> Either Failure () +evalPrim p err xs + | p (SOP.hmap (I . inputValue) xs) + = Right () + + | otherwise + = Left Failure { + failureErr = err $ SOP.hmap (K . inputExpr) xs + , failureInputs = renderInputs xs + } + +evalLam :: + SListI xs + => (x -> Predicate xs) + -> NP Input (x : xs) + -> Either Failure () +evalLam f (x :* xs) = + first (addInputs [renderInput x]) $ + evalAt (f $ inputValue x) xs + +evalDot :: + SListI xs + => Predicate (x : xs) + -> Fn y x + -> NP Input (y : xs) + -> Either Failure () +evalDot p f (x :* xs) = + first (addInputs $ catMaybes [x']) $ + evalAt p (y :* xs) + where + (y, x') = applyFn f x + +evalOn :: + SListI xs + => Predicate (x : x : xs) + -> Fn y x + -> NP Input (y : y : xs) + -> Either Failure () +evalOn p f (x0 :* x1 :* xs) = + first (addInputs $ catMaybes [x0', x1']) $ + evalAt p (y0 :* y1 :* xs) + where + (y0, x0') = applyFn f x0 + (y1, x1') = applyFn f x1 + +evalChoice :: + SListI xs + => Predicate (a : xs) + -> Predicate (b : xs) + -> NP Input (Either a b : xs) + -> Either Failure () +evalChoice t f (x :* xs) = + first (addInputs [renderInput x]) $ + case inputValue x of + Left a -> evalAt t (x{inputValue = a} :* xs) + Right b -> evalAt f (x{inputValue = b} :* xs) + +evalAt :: SListI xs => Predicate xs -> NP Input xs -> Either Failure () +evalAt (Prim p err) xs = evalPrim p err xs +evalAt Pass _ = return () +evalAt Fail xs = Left $ Failure "Fail" (renderInputs xs) +evalAt (Both p1 p2) xs = evalAt p1 xs >> evalAt p2 xs +evalAt (Lam f) xs = evalLam f xs +evalAt (p `At` x) xs = evalAt p (x :* xs) +evalAt (p `Dot` f) xs = evalDot p f xs +evalAt (p `On` f) xs = evalOn p f xs +evalAt (Flip p) xs = let (x :* y :* zs) = xs in evalAt p (y :* x :* zs) +evalAt (Choose l r) xs = evalChoice l r xs +evalAt (Const p) xs = evalAt p (SOP.tl xs) + +{------------------------------------------------------------------------------- + Evaluation and partial evaluation +-------------------------------------------------------------------------------} + +-- | Evaluate fully applied predicate +eval :: Predicate '[] -> Either Err () +eval p = first prettyFailure $ evalAt p Nil + +-- | Infix version of 'at' +-- +-- Typical usage example: +-- +-- > assert $ +-- > P.relatedBy ("equiv", equiv) +-- > .$ ("x", x) +-- > .$ ("y", y) +(.$) :: Show x => Predicate (x : xs) -> (Var, x) -> Predicate xs +p .$ (n, x) = p `at` (n, show x, x) + +-- | Generation of '(.$)' that does not require a 'Show' instance +at :: + Predicate (x : xs) + -> (Var, String, x) -- ^ Renderded name, name for the input, and input proper + -> Predicate xs +p `at` (n, r, x) = p `At` (Input (Var n) r x) + +{------------------------------------------------------------------------------- + Specific predicates +-------------------------------------------------------------------------------} + +-- | Construct predicate corresponding to some infix operator +-- +-- This is an internal auxiliary. +binaryInfix :: + Var -- ^ Infix operator corresponding to the relation /NOT/ holding + -> (a -> b -> Bool) -> Predicate [a, b] +binaryInfix op f = binary f $ \x y -> prettyExpr (Infix op x y) + +-- | Equal +eq :: Eq a => Predicate [a, a] +eq = binaryInfix "/=" (==) + +-- | Not equal +ne :: Eq a => Predicate [a, a] +ne = binaryInfix "==" (/=) + +-- | (Strictly) less than +lt :: Ord a => Predicate [a, a] +lt = binaryInfix ">=" (<) + +-- | Less than or equal to +le :: Ord a => Predicate [a, a] +le = binaryInfix ">" (<=) + +-- | (Strictly) greater than +gt :: Ord a => Predicate [a, a] +gt = binaryInfix "<=" (>) + +-- | Greater than or equal to +ge :: Ord a => Predicate [a, a] +ge = binaryInfix "<" (>=) + +-- | Check that values get closed to the specified target +towards :: forall a. (Show a, Ord a, Num a) => a -> Predicate [a, a] +towards = \target -> pred .$ ("target", target) + where + pred :: Predicate [a, a, a] + pred = Lam (\target -> ge `on` fn ("distanceToTarget", distanceTo target)) + + distanceTo :: a -> a -> a + distanceTo target x + | x <= target = target - x + | otherwise = x - target + +-- | Specialization of 'eq', useful when expecting a specific value in a test +expect :: (Show a, Eq a) => a -> Predicate '[a] +expect x = eq .$ ("expected", x) + +-- | Check that @lo <= x <= hi@ +between :: (Show a, Ord a) => a -> a -> Predicate '[a] +between lo hi = mconcat [ + le .$ ("lo", lo) + , flip le .$ ("hi", hi) + ] + +-- | Number is even +even :: Integral a => Predicate '[a] +even = satisfies ("even", Prelude.even) + +-- | Number is odd +odd :: Integral a => Predicate '[a] +odd = satisfies ("odd ", Prelude.odd) + +-- | Membership check +elem :: Eq a => Predicate '[[a], a] +elem = flip $ binaryInfix ("`notElem`") Prelude.elem diff --git a/src/Test/Falsify/Property.hs b/src/Test/Falsify/Property.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Property.hs @@ -0,0 +1,30 @@ +-- | Properties +-- +-- Intended for unqualified import. +-- +-- Most users will probably use "Test.Tasty.Falsify" instead of this module. +module Test.Falsify.Property ( + Property' -- opaque + , Property + -- * Run generators + , gen + , genWith + -- * 'Property' features + , testFailed + , assert + , info + , discard + , label + , collect + -- * Testing shrinking + , testShrinking + , testMinimum + -- * Testing generators + , testGen + , testShrinkingOfGen + ) where + +import Test.Falsify.Internal.Property + +-- | Property that uses strings as errors +type Property = Property' String diff --git a/src/Test/Falsify/Range.hs b/src/Test/Falsify/Range.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Range.hs @@ -0,0 +1,290 @@ +-- | Numerical ranges +module Test.Falsify.Range ( + Range -- opaque + -- * Constructors + -- ** Linear + , between + , withOrigin + -- ** Non-linear + , skewedBy + -- * Queries + , origin + -- * Primitive constructors + , ProperFraction(..) + , Precision(..) + , constant + , fromProperFraction + , towards + -- * Evalation + , eval + ) where + +import Data.List (minimumBy) +import Data.Ord + +import Test.Falsify.Internal.Range +import Data.Bits + +{------------------------------------------------------------------------------- + Primitive ranges +-------------------------------------------------------------------------------} + +-- | Range that is @x@ everywhere +constant :: a -> Range a +constant = Constant + +-- | Construct @a@ given a fraction +-- +-- Precondition: @f@ must be monotonically increasing or decreasing; i.e. +-- +-- * for all @x <= y@, @f x <= f y@, /or/ +-- * for all @x <= y@, @f y <= f x@ +fromProperFraction :: Precision -> (ProperFraction -> a) -> Range a +fromProperFraction = FromProperFraction + +-- | Generate value in any of the specified ranges, then choose the one +-- that is closest to the specified origin +-- +-- Precondition: the target must be within the bounds of all ranges. +towards :: a -> [Range a] -> Range a +towards = Towards + +{------------------------------------------------------------------------------- + Constructing ranges +-------------------------------------------------------------------------------} + +-- | Uniform selection between the given bounds, shrinking towards first bound +between :: forall a. (Integral a, FiniteBits a) => (a, a) -> Range a +between = skewedBy 0 + +-- | Selection within the given bounds, shrinking towards the specified origin +withOrigin :: (Integral a, FiniteBits a) => (a, a) -> a -> Range a +withOrigin (x, y) o + | not originInBounds + = error "withOrigin: origin not within bounds" + + -- Since origin must be within bounds, we must have x == o == y here + | x == y + = Constant x + + | o == x + = between (x, y) + + | o == y + = between (y, x) + +-- Split the range into two halves. We are careful to do this only when needed: +-- if we didn't (i.e., if the origin /equals/ one of the endpoints), that would +-- result in a singleton range, and since that singleton range (by definition) +-- would be at the origin, we would only ever produce that one value. + | otherwise = + towards o [ + between (o, x) + , between (o, y) + ] + where + originInBounds :: Bool + originInBounds + | x <= o && o <= y = True + | y <= o && o <= x = True + | otherwise = False + +{------------------------------------------------------------------------------- + Skew + + To introduce skew, we want something that is reasonably simply to implement + but also has some reasonal properties. Suppose a skew of @s@ means that we + generate value from the lower 20% of the range 60% of the time. Then: + + - Symmetry around the antidiagonal: we will generate a value from the + upper 60% of the range 20% of the time. + + - Symmetry around the diagonal: a skew of @-s@ will mean we generate a value + from the /upper/ 20% of the range 60% of the time. + + To derive the formula we use, suppose we start with a circle with radius 1, + centered at the origin: + + > x^2 + y^2 == 1 + > y^2 == 1 - x^2 + > y == (1 - x^2) ^ (1/2) + + In the interval [0, 1] this gives us the upper right quadrant of the circle, + but we want the lower right: + + > y == 1 - ((1 - x^2) ^ (1/2)) + + We can now vary that power. + + > y == 1 - ((1 - x^3) ^ (1/3)) + > y == 1 - ((1 - x^4) ^ (1/4)) + > .. + + If the power is 1, we get no skew: + + > y == 1 - ((1 - x^1) ^ (1/1)) + > == 1 - (1 - x) + > == x + + We want a skew of 0 to mean no skew, so in terms of s: + + > y == 1 - ((1 - x^(s+1)) ^ (1/(s+1))) + + For negative values of @s@, we flip this around the diagonal: + + > y == 1 - (1 - ((1 - (1-x)^(s+1)) ^ (1/(s+1)))) + > == (1 - (1-x)^(s+1)) ^ (1/(s+1)) + + giving us + + > (1 - (1 - x)^2)^(1/2) for s == -1 + > (1 - (1 - x)^3)^(1/3) for s == -2 + > etc. +-------------------------------------------------------------------------------} + +-- | Introduce skew (non-uniform selection) +-- +-- A skew of @s == 0@ means no skew: uniform selection. +-- +-- A positive skew @(s > 0)@ introduces a bias towards smaller values (this is +-- the typical use case). As example, for a skew of @s == 1@: +-- +-- * We will generate a value from the lower 20% of the range 60% of the time. +-- * We will generate a value from the upper 60% of the range 20% of the time. +-- +-- A negative skew @(s < 0)@ introduces a bias towards larger values. For a +-- skew of @s == 1@: +-- +-- * We will generate a value from the upper 20% of the range 60% of the time. +-- * We will generate a value from the lower 60% of the range 20% of the time. +-- +-- The table below lists values for the percentage of the range used, given a +-- percentage of the time (a value of 0 means a single value from the range): +-- +-- > | time% +-- > s | 50% | 90% +-- > -------------- +-- > 0 | 50 | 90 +-- > 1 | 13 | 56 +-- > 2 | 4 | 35 +-- > 3 | 1 | 23 +-- > 4 | 0 | 16 +-- > 5 | 0 | 11 +-- > 6 | 0 | 8 +-- > 7 | 0 | 6 +-- > 8 | 0 | 5 +-- > 9 | 0 | 4 +-- > 10 | 0 | 3 +-- +-- Will shrink towards @x@, independent of skew. +-- +-- NOTE: The implementation currently uses something similar to μ-law encoding. +-- As a consequence, the generator gets increased precision near the end of the +-- range we skew towards, and less precision near the other end. This means that +-- not all values in the range can be produced. +skewedBy :: forall a. (FiniteBits a, Integral a) => Double -> (a, a) -> Range a +skewedBy s (x, y) + | x == y = constant x + | x < y = let p = precisionRequiredToRepresent (y - x) + in fromProperFraction p $ \(ProperFraction f) -> roundDown f + | otherwise = let p = precisionRequiredToRepresent (x - y) + in fromProperFraction p $ \(ProperFraction f) -> roundUp f + where + x', y' :: Double + x' = fromIntegral x + y' = fromIntegral y + + -- We have to be careful here. Perhaps the more obvious way to express this + -- calculation is + -- + -- > round $ x' + skew f * (y' - x') + -- + -- However, this leads to a bad distribution of test data. Suppose we are + -- generating values in the range [0 .. 2]. Then that call to 'round' + -- would result in something like this: + -- + -- > 0..............1..............2 + -- > [ /\ /\ ] + -- > ^^^^^^^^ ^^^^^^^^^^^^ ^^^^^^ + -- > 0 1 2 + -- + -- To avoid this heavy bias, we instead do this: + -- + -- > 0..............1..............2..............3 + -- > [ /\ /\ ] + -- > ^^^^^^^^^^^^^^ ^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^ + -- > 0 1 2 + -- + -- By insisting that the fraction is a /proper/ fraction (i.e., not equal to + -- 1), we avoid generating @3@ (which would be outside the range). + roundDown, roundUp :: Double -> a + roundDown f = floor $ x' + skew f * (y' - x' + 1) + roundUp f = ceiling $ x' - skew f * (x' - y' + 1) + + pos, neg :: Double -> Double + pos f = 1 - ((1 - f ** (s + 1)) ** (1 / ( s + 1))) + neg f = (1 - (1 - f) ** (s + 1)) ** (1 / (abs s + 1)) + + skew :: Double -> Double + skew | s == 0 = id + | s >= 0 = pos + | otherwise = neg + +{------------------------------------------------------------------------------- + Precision +-------------------------------------------------------------------------------} + +-- | Precision required to be able to choose within the given range +-- +-- In order to avoid rounding errors, we set a lower bound on the precision. +-- This lower bound is verified in "TestSuite.Sanity.Range", which verifies that +-- for small ranges, the expected distribution is never off by more than 1% +-- from the actual distribution. +precisionRequiredToRepresent :: forall a. FiniteBits a => a -> Precision +precisionRequiredToRepresent x = fromIntegral $ + 7 `max` (finiteBitSize (undefined :: a) - countLeadingZeros x) + +{------------------------------------------------------------------------------- + Queries +-------------------------------------------------------------------------------} + +-- | Origin of the range (value we shrink towards) +origin :: Range a -> a +origin (Constant x) = x +origin (FromProperFraction _ f) = f (ProperFraction 0) +origin (Towards o _) = o + +{------------------------------------------------------------------------------- + Evaluation +-------------------------------------------------------------------------------} + +-- | Internal auxiliary for 'eval' +evalTowards :: forall f a. + (Applicative f, Ord a, Num a) + => a -> [f a] -> f a +evalTowards o gens = + pick <$> sequenceA gens + where + pick :: [a] -> a + pick [] = o + pick as = minimumBy (comparing distanceToOrigin) as + + distanceToOrigin :: a -> a + distanceToOrigin x + | x >= o = x - o + | otherwise = o - x + +-- | Evaluate a range, given an action to generate fractions +-- +-- Most users will probably never need to call this function. +eval :: forall f a. + (Applicative f, Ord a, Num a) + => (Precision -> f ProperFraction) -> Range a -> f a +eval genFraction = go + where + go :: Range a -> f a + go r = + case r of + Constant x -> pure x + FromProperFraction p f -> f <$> genFraction p + Towards o rs -> evalTowards o (map go rs) diff --git a/src/Test/Falsify/Reexported/Generator/Compound.hs b/src/Test/Falsify/Reexported/Generator/Compound.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Reexported/Generator/Compound.hs @@ -0,0 +1,429 @@ +-- | Compound generators +module Test.Falsify.Reexported.Generator.Compound ( + -- * Taking advantage of 'Selective' + choose + -- * Lists + , list + , elem + , pick + , pickBiased + -- ** Shuffling + , shuffle + , permutation + -- * Tweak test data distribution + , frequency + -- * Trees + -- ** Binary trees + , tree + , bst + -- ** Shrink trees + , IsValidShrink(..) + , ShrinkTree + , path + , pathAny + -- * Auxiliary + , shrinkToNothing + , mark + ) where + +import Prelude hiding (either, elem) + +import Control.Monad +import Control.Selective +import Data.Either (either) +import Data.List.NonEmpty (NonEmpty(..)) +import Data.Maybe (catMaybes) +import Data.Void + +import qualified Data.List.NonEmpty as NE +import qualified Data.Tree as Rose + +import Data.Falsify.List (Permutation) +import Data.Falsify.Marked +import Data.Falsify.Tree (Tree(..), Interval(..), Endpoint(..)) +import Test.Falsify.Internal.Generator +import Test.Falsify.Internal.Generator.Shrinking (IsValidShrink(..)) +import Test.Falsify.Range (Range) +import Test.Falsify.Reexported.Generator.Shrinking +import Test.Falsify.Reexported.Generator.Simple + +import qualified Data.Falsify.List as List +import qualified Data.Falsify.Tree as Tree +import qualified Test.Falsify.Range as Range + +{------------------------------------------------------------------------------- + Taking advantage of 'Selective' +-------------------------------------------------------------------------------} + +-- | Generate a value with one of two generators +-- +-- Shrinks towards the first generator;the two generators can shrink +-- independently from each other. +-- +-- === Background +-- +-- In the remainder of this docstring we give some background to this function, +-- which may be useful for general understanding of the @falsify@ library. +-- +-- The implementation takes advantage of the that 'Gen' is a selective functor +-- to ensure that the two generators can shrink independently: if the initial +-- value of the generator is some @y@ produced by the second generator, later +-- shrunk to some @y'@, then if the generator can shrink to @x@ at some point, +-- produced by the /first/ generator, then shrinking effectively "starts over": +-- the value of @x@ is independent of @y'@. +-- +-- That is different from doing this: +-- +-- > do b <- bool +-- > if b then l else r +-- +-- In this case, @l@ and @r@ will be generated from the /same/ sample tree, +-- and so cannot shrink independently. +-- +-- It is /also/ different from +-- +-- > do x <- l +-- > y <- r +-- > b <- bool +-- > return $ if b then x else y +-- +-- In this case, @l@ and @r@ are run against /different/ sample trees, like we +-- do here, /but/ in this case if the current value produced by the generator is +-- produced by the right generator, then the sample tree used for the left +-- generator will always shrink to 'Minimal' (this /must/ be possible because +-- we're not currently using it); this means that we would then only be able to +-- shrink to a value from the left generator if the /minimal/ value produced by +-- that generator happens to work. +-- +-- To rephrase that last point: generating values that are not actually used +-- will lead to poor shrinking, since those values can always be shrunk to their +-- minimal value, independently from whatever property is being tested: the +-- shrinker does not know that the value is not being used. The correct way to +-- conditionally use a value is to use the selective interface, as we do here. +choose :: Gen a -> Gen a -> Gen a +choose = ifS (bool True) + +{------------------------------------------------------------------------------- + Auxiliary: marking elements +-------------------------------------------------------------------------------} + +-- | Start with @Just x@ for some @x@, then shrink to @Nothing@ +shrinkToNothing :: Gen a -> Gen (Maybe a) +shrinkToNothing g = firstThen Just (const Nothing) <*> g + +-- | Mark an element, shrinking towards 'Drop' +-- +-- This is similar to 'shrinkToNothing', except that 'Marked' still has a value +-- in the 'Drop' case: marks are merely hints, that we may or may not use. +mark :: Gen a -> Gen (Marked Gen a) +mark x = flip Marked x <$> firstThen Keep Drop + +{------------------------------------------------------------------------------- + Lists +-------------------------------------------------------------------------------} + +-- | Generate list of specified length +-- +-- Shrinking behaviour: +-- +-- * The length of the list will shrink as specified by the given range. +-- * We can drop random elements from the list, but prefer to drop them +-- from near the /end/ of the list. +-- +-- Note on shrinking predictability: in the case that the specified 'Range' has +-- an origin which is neither the lower bound nor the upper bound (and only in +-- that case), 'list' can have confusing shrinking behaviour. For example, +-- suppose we have a range @(0, 10)@ with origin 5. Then we could start by +-- generating an intermediate list of length of 10 and then subsequently drop 5 +-- elements from that, resulting in an optimal list length. However, we can now +-- shrink that length from 10 to 2 (which is closer to 5, after all), but now we +-- only have 2 elements to work with, and hence the generated list will now drop +-- from 5 elements to 2. This is not necessarily a problem, because that length +-- 2 can now subsequently shrink further towards closer to the origin (5), but +-- nonetheless it might result in confusing intermediate shrinking steps. +list :: Range Word -> Gen a -> Gen [a] +list len gen = do + -- We do /NOT/ mark this call to 'integral' as 'withoutShrinking': it could + -- shrink towards larger values, in which case we really need to generate + -- more elements. This doesn't really have any downsides: it merely means + -- that we would prefer to shrink towards a prefix of the list first, before + -- we try to drop random other elements from the list. + -- + -- If we have an expression such as @(,) <$> list .. <*> list@, the two + -- lists will be shrunk independently from each other due to the branching + -- point above them. Hence, it doesn't matter if first generator uses "fewer + -- samples" as it shrinks. + n <- integral len + + -- Generate @n@ marks, indicating for each element if we want to keep that + -- element or not, so that we can drop elements from the middle of the list. + -- + -- Due to the left-biased nature of shrinking, this will shrink towards + -- dropped elements (@False@ values) near the start, but we want them near + -- the /end/, so we reverse the list. + marks <- fmap (List.keepAtLeast (Range.origin len) . reverse) $ + replicateM (fromIntegral n) $ mark gen + + -- Finally, generate the elements we want to keep + catMaybes <$> selectAllKept marks + +-- | Choose random element +-- +-- Shrinks towards earlier elements. +-- +-- NOTE: Does not work on infinite lists (it computes the length of the list). +elem :: NonEmpty a -> Gen a +elem = fmap (\(_before, x, _after) -> x) . pick + +-- | Generalization of 'elem' that additionally returns the parts of the list +-- before and after the element +pick :: NonEmpty a -> Gen ([a], a, [a]) +pick = \xs -> + aux [] (NE.toList xs) <$> + integral (Range.between (0, length xs - 1)) + where + aux :: [a] -> [a] -> Int -> ([a], a, [a]) + aux _ [] _ = error "pick: impossible" + aux prev (x:xs) 0 = (reverse prev, x, xs) + aux prev (x:xs) i = aux (x:prev) xs (i - 1) + +-- | Choose random element from a list +-- +-- This is different from 'elem': it avoids first computing the length of the +-- list, and is biased towards elements earlier in the list. The advantage is +-- that this works for infinite lists, too. +-- +-- Also returns the elements from the list before and after the chosen element. +pickBiased :: NonEmpty a -> Gen ([a], a, [a]) +pickBiased = \xs -> pickChunk [] (List.chunksOfNonEmpty chunkSize xs) + where + chunkSize :: Word + chunkSize = 1_000 + + -- We want to avoid computing the length of the list, but equally we don't + -- want to skew /too/ heavily towards the start of the list. Therefore we + -- chunk the list (this is lazy), then flip a coin for each chunk, and once + -- we find a chunk, do an unbiased choice within that chunk. + pickChunk :: [NonEmpty a] -> NonEmpty (NonEmpty a) -> Gen ([a], a, [a]) + pickChunk prev (chunk :| []) = do + -- No choice left: we must generate use this chunk + withChunk prev chunk [] + pickChunk prev (chunk :| next@(n:ns)) = do + useChunk <- bool True + if useChunk + then withChunk prev chunk next + else pickChunk (chunk:prev) (n :| ns) + + withChunk :: [NonEmpty a] -> NonEmpty a -> [NonEmpty a] -> Gen ([a], a, [a]) + withChunk prev chunk next = do + (chunkBefore, chunkElem, chunkAfter) <- pick chunk + return ( + concat $ reverse $ chunkBefore : map NE.toList prev + , chunkElem + , chunkAfter ++ concatMap NE.toList next + ) + +{------------------------------------------------------------------------------- + Tweak test data distribution +-------------------------------------------------------------------------------} + +-- | Choose generator with the given frequency +-- +-- For example, +-- +-- > frequency [ +-- > (1, genA) +-- > , (2, genB) +-- > ] +-- +-- will use @genA@ 1/3rd of the time, and @genB@ 2/3rds. +-- +-- Shrinks towards generators earlier in the list; the generators themselves +-- are independent from each other (shrinking of @genB@ does not affect +-- shrinking of @genA@). +-- +-- Precondition: there should at least one generator with non-zero frequency. +frequency :: forall a. [(Word, Gen a)] -> Gen a +frequency gens = + case filter ((/= 0) . fst) indexedGens of + [] -> error "frequency: no generators with non-zero frequency" + gens' -> do + let r :: Range Word + r = Range.between (0, sum (map fst gens') - 1) + (gen, genIx) <- (\i -> frequencyLookup i gens') <$> integral r + perturb genIx gen + where + -- We need to be careful: we don't want to perturb the generator by the + -- value generated by 'integral', because many different values could + -- correspond to the /same/ generator. Instead, we assign each generator its + -- own index, and use that instead. + indexedGens :: [(Word, (Gen a, Word))] + indexedGens = zipWith (\(f, g) i -> (f, (g, i))) gens [0..] + +-- | Internal auxiliary to 'frequency' +frequencyLookup :: Word -> [(Word, x)] -> x +frequencyLookup = \i xs -> + case go i xs of + Just x -> x + Nothing -> + error $ concat [ + "frequencyLookup: index " + , show i + , " out of range of " + , show (map fst xs) + ] + where + go :: Word -> [(Word, x)] -> Maybe x + go _ [] = Nothing + go i ((n, x):xs) + | i < n = Just x + | otherwise = go (i - n) xs + +{------------------------------------------------------------------------------- + Shuffling +-------------------------------------------------------------------------------} + +-- | Shuffle list (construct a permutation) +-- +-- Shrinking behaviour: 'shuffle' is defined in terms of 'permutation', which +-- provides some guarantees: it shrinks towards making changes near the /start/ +-- of the list, and towards swapping /fewer/ elements of the list. +-- +-- It is difficult to define precisely how this affects the resulting list, but +-- we /can/ say that if for a particular counter-example it suffices if two +-- lists are different in /one/ element, then the shuffled list will in fact +-- only be different in /one/ place from the original, and that one element will +-- have been swapped with an immediate neighbour. +shuffle :: [a] -> Gen [a] +shuffle xs = + flip List.applyPermutation xs <$> + permutation (fromIntegral $ length xs) + +-- | Generate permutation for a list of length @n@ +-- +-- This is essentially an implemention of Fisher-Yates, in that we generate a +-- series of swaps (i, j), with 1 <= i <= n - 1 and @0 <= j <= i@, except that +-- +-- * We can shrink a choice of @i@ (towards 1). +-- * We can drop arbitrary swaps. +-- +-- This ensures that we shrink towards making swaps nearer the /start/ of the +-- list, as well as towards /fewer/ swaps. +-- +-- We make no attempt to make the permutation canonical; doing so makes it +-- extremely difficult to get predicable shrinking behaviour. +permutation :: Word -> Gen Permutation +permutation 0 = return [] +permutation 1 = return [] +permutation n = do + swaps <- mapM (mark . genSwap) [n - 1, n - 2 .. 1] + catMaybes <$> selectAllKept swaps + where + genSwap :: Word -> Gen (Word, Word) + genSwap i = do + i' <- integral $ Range.between (1, i) + j <- integral $ Range.between (i, 0) + return (i', min i' j) + +{------------------------------------------------------------------------------- + Binary trees +-------------------------------------------------------------------------------} + +-- | Generate binary tree +tree :: forall a. Range Word -> Gen a -> Gen (Tree a) +tree size gen = do + n <- integral size + t <- Tree.keepAtLeast (Range.origin size) . Tree.propagate <$> go n + Tree.genKept t + where + go :: Word -> Gen (Tree (Marked Gen a)) + go 0 = return Leaf + go n = do + -- Generate element at the root + x <- mark gen + + -- Choose how many elements to put in the left subtree + -- + -- This ranges from none (right-biased) to all (left-biased), shrinking + -- towards half the number of elements: hence, towards a balanced tree. + inLeft <- integral $ Range.withOrigin (0, n - 1) ((n - 1) `div` 2) + let inRight = (n - 1) - inLeft + Branch x <$> go inLeft <*> go inRight + +-- | Construct binary search tree +-- +-- Shrinks by replacing entire subtrees by the empty tree. +bst :: forall a b. Integral a => (a -> Gen b) -> Interval a -> Gen (Tree (a, b)) +bst gen = go >=> traverse (\a -> (a,) <$> gen a) + where + go :: Interval a -> Gen (Tree a) + go i = + case Tree.inclusiveBounds i of + Nothing -> pure Leaf + Just (lo, hi) -> firstThen id (const Leaf) <*> go' lo hi + + -- inclusive bounds, lo <= hi + go' :: a -> a -> Gen (Tree a) + go' lo hi = Branch mid + <$> go (Interval (Inclusive lo) (Exclusive mid)) + <*> go (Interval (Exclusive mid) (Inclusive hi)) + where + mid :: a + mid = lo + ((hi - lo) `div` 2) + +{------------------------------------------------------------------------------- + Shrink trees +-------------------------------------------------------------------------------} + +type ShrinkTree = Rose.Tree + +-- | Generate semi-random path through the tree +-- +-- Will only construct paths that satisfy the given predicate (typically, a +-- property that is being tested). +-- +-- Shrinks towards shorter paths, and towards paths that use subtrees that +-- appear earlier in the list of subtrees at any node in the tree. +-- +-- See also 'pathAny'. +path :: forall a p n. + (a -> IsValidShrink p n) -- ^ Predicate + -> ShrinkTree a + -> Gen (Either n (NonEmpty p)) +path validShrink = \(Rose.Node a as) -> + case validShrink a of + InvalidShrink n -> pure $ Left n + ValidShrink p -> Right <$> go p as + where + -- We only want to pick a shrunk value that matches the predicate, but we + -- potentially waste a /lot/ of work if we first evaluate the predicate for + -- /all/ potential shrunk values and then choose. So, instead we choose + -- first, evaluate the predicate, and if it fails, choose again. + go :: p -> [Rose.Tree a] -> Gen (NonEmpty p) + go p [] = pure (p :| []) + go p (a:as) = do + (before, a', after) <- pickBiased (a :| as) + + case checkPred a' of + Nothing -> + -- Not a valid shrink step. Pick a different one. + go p (before ++ after) + Just (p', as') -> + -- Found a valid shrink step. + -- + -- We only call @choose@ once we found a valid shrink step, + -- otherwise we would skew very heavily towards shorter paths. + choose + (pure (p :| [])) + (NE.cons p <$> go p' as') + + checkPred :: Rose.Tree a -> Maybe (p, [Rose.Tree a]) + checkPred (Rose.Node a as) = + case validShrink a of + InvalidShrink _ -> Nothing + ValidShrink b -> Just (b, as) + +-- | Variation on 'path' without a predicate. +pathAny :: ShrinkTree a -> Gen (NonEmpty a) +pathAny = fmap (either absurd id) . path ValidShrink + diff --git a/src/Test/Falsify/Reexported/Generator/Function.hs b/src/Test/Falsify/Reexported/Generator/Function.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Reexported/Generator/Function.hs @@ -0,0 +1,393 @@ +module Test.Falsify.Reexported.Generator.Function ( + Fun -- opaque + , applyFun + , pattern Fn + , pattern Fn2 + , pattern Fn3 + -- * Generation + , fun + -- * Construction + , Function(..) + , (:->) -- opaque + , functionMap + ) where + +import Prelude hiding (sum) + +import Control.Monad +import Data.Bifunctor +import Data.Char +import Data.Foldable (toList) +import Data.Int +import Data.Kind +import Data.List (intercalate) +import Data.Maybe (fromMaybe, mapMaybe) +import Data.Ratio (Ratio) +import Data.Word +import GHC.Generics +import Numeric.Natural + +import qualified Data.Ratio as Ratio + +import Data.Falsify.Tree (Tree, Interval(..), Endpoint(..)) +import Test.Falsify.Internal.Generator (Gen) +import Test.Falsify.Reexported.Generator.Shrinking +import Test.Falsify.Reexported.Generator.Compound + +import qualified Data.Falsify.Tree as Tree + +{------------------------------------------------------------------------------- + Functions that can be shrunk and shown +-------------------------------------------------------------------------------} + +-- | Function @a -> b@ which can be shown, generated, and shrunk +data Fun a b = Fun { + concrete :: a :-> b + , defaultValue :: b + + -- Since functions are typically infinite, they can only safely be shown + -- once they are fully shrunk: after all, once a function has been fully + -- shrunk, we /know/ it must be finite, because in any given property, a + -- function will only ever be applied a finite number of times. + , isFullyShrunk :: Bool + } + deriving (Functor) + +-- | Generate function @a -> b@ given a generator for @b@ +fun :: Function a => Gen b -> Gen (Fun a b) +fun gen = do + -- Generate value first, so that we try to shrink that first + defaultValue <- gen + concrete <- function gen + isFullyShrunk <- firstThen False True + return Fun{concrete, defaultValue, isFullyShrunk} + +{------------------------------------------------------------------------------- + Concrete functions + + NOTE: @Nil@ is useful as a separate constructor, since it does not have an + @Eq@ constraint. +-------------------------------------------------------------------------------} + +data (:->) :: Type -> Type -> Type where + Nil :: a :-> b + Unit :: a -> () :-> a + Table :: Ord a => Tree (a, Maybe b) -> a :-> b + Sum :: (a :-> c) -> (b :-> c) -> (Either a b :-> c) + Prod :: (a :-> (b :-> c)) -> (a, b) :-> c + Map :: (b -> a) -> (a -> b) -> (a :-> c) -> (b :-> c) + +instance Functor ((:->) a) where + fmap _ Nil = Nil + fmap f (Unit x) = Unit (f x) + fmap f (Table xs) = Table (fmap (second (fmap f)) xs) + fmap f (Sum x y) = Sum (fmap f x) (fmap f y) + fmap f (Prod x) = Prod (fmap (fmap f) x) + fmap f (Map ab ba x) = Map ab ba (fmap f x) + +-- | The basic building block for 'Function' instances +-- +-- Provides a 'Function' instance by mapping to and from a type that +-- already has a 'Function' instance. +functionMap :: (b -> a) -> (a -> b) -> (a :-> c) -> b :-> c +functionMap = Map + +-- | Apply concrete function +abstract :: (a :-> b) -> b -> (a -> b) +abstract Nil d _ = d +abstract (Unit x) _ _ = x +abstract (Prod p) d (x,y) = abstract (fmap (\q -> abstract q d y) p) d x +abstract (Sum p q) d exy = either (abstract p d) (abstract q d) exy +abstract (Table xys) d x = fromMaybe d . join $ Tree.lookup x xys +abstract (Map g _ p) d x = abstract p d (g x) + +{------------------------------------------------------------------------------- + Patterns + + These are analogue to their counterparts in QuickCheck. +-------------------------------------------------------------------------------} + +-- | Pattern synonym useful when generating functions of one argument +pattern Fn :: (a -> b) -> Fun a b +pattern Fn f <- (applyFun -> f) + +-- | Pattern synonym useful when generating functions of two arguments +pattern Fn2 :: (a -> b -> c) -> Fun (a, b) c +pattern Fn2 f <- (applyFun2 -> f) + +-- | Pattern synonym useful when generating functions of three arguments +pattern Fn3 :: (a -> b -> c -> d) -> Fun (a, b, c) d +pattern Fn3 f <- (applyFun3 -> f) + +-- | Apply function to argument +-- +-- See also the 'Fn', 'Fn2', and 'Fn3' patter synonyms. +applyFun :: Fun a b -> a -> b +applyFun Fun{concrete, defaultValue} = abstract concrete defaultValue + +applyFun2 :: Fun (a, b) c -> (a -> b -> c) +applyFun2 f a b = applyFun f (a, b) + +applyFun3 :: Fun (a, b, c) d -> (a -> b -> c -> d) +applyFun3 f a b c = applyFun f (a, b, c) + +{-# COMPLETE Fn #-} +{-# COMPLETE Fn2 #-} +{-# COMPLETE Fn3 #-} + +{------------------------------------------------------------------------------- + Constructing concrete functions +-------------------------------------------------------------------------------} + +shrinkToNil :: Gen (a :-> b) -> Gen (a :-> b) +shrinkToNil gen = fromMaybe Nil <$> shrinkToNothing gen + +table :: forall a b. (Integral a, Bounded a) => Gen b -> Gen (a :-> b) +table gen = Table <$> bst (\_a -> shrinkToNothing gen) i + where + i :: Interval a + i = Interval (Inclusive minBound) (Inclusive maxBound) + +unit :: Gen c -> Gen (() :-> c) +unit gen = shrinkToNil (Unit <$> gen) + +sum :: + (Gen c -> Gen ( a :-> c)) + -> (Gen c -> Gen ( b :-> c)) + -> (Gen c -> Gen (Either a b :-> c)) +sum f g gen = Sum <$> shrinkToNil (f gen) <*> shrinkToNil (g gen) + +prod :: + (forall c. Gen c -> Gen ( a :-> c)) + -> (forall c. Gen c -> Gen ( b :-> c)) + -> (forall c. Gen c -> Gen ((a, b) :-> c)) +prod f g = fmap Prod . f . g + +{------------------------------------------------------------------------------- + Show functions +-------------------------------------------------------------------------------} + +instance (Show a, Show b) => Show (Fun a b) where + show Fun{concrete, defaultValue, isFullyShrunk} + | isFullyShrunk = showFunction concrete defaultValue + | otherwise = "" + +-- | Show concrete function +-- +-- Only use this on finite functions. +showFunction :: (Show a, Show b) => (a :-> b) -> b -> String +showFunction p d = concat [ + "{" + , intercalate ", " $ concat [ + [ show x ++ "->" ++ show c + | (x,c) <- toTable p + ] + , ["_->" ++ show d] + ] + , "}" + ] + +-- | Generating a table from a concrete function +-- +-- This is only used in the 'Show' instance. +toTable :: (a :-> b) -> [(a, b)] +toTable Nil = [] +toTable (Unit x) = [((), x)] +toTable (Prod p) = [ ((x,y),c) | (x,q) <- toTable p, (y,c) <- toTable q ] +toTable (Sum p q) = [ (Left x, c) | (x,c) <- toTable p ] + ++ [ (Right y,c) | (y,c) <- toTable q ] +toTable (Table xys) = mapMaybe (\(a, b) -> (a,) <$> b) $ toList xys +toTable (Map _ h p) = [ (h x, c) | (x,c) <- toTable p ] + +{------------------------------------------------------------------------------- + Class to construct functions +-------------------------------------------------------------------------------} + +-- | Generating functions +class Function a where + -- | Build reified function + -- + -- '(:->)' is an abstract type; if you need to add additional 'Function' + -- instances, you need to use 'functionMap', or rely on the default + -- implementation in terms of generics. + function :: Gen b -> Gen (a :-> b) + + default function :: (Generic a, GFunction (Rep a)) => Gen b -> Gen (a :-> b) + function gen = functionMap from to <$> gFunction gen + +instance Function Word8 where function = table +instance Function Int8 where function = table + +instance Function Int where function = integral +instance Function Int16 where function = integral +instance Function Int32 where function = integral +instance Function Int64 where function = integral +instance Function Word where function = integral +instance Function Word16 where function = integral +instance Function Word32 where function = integral +instance Function Word64 where function = integral +instance Function Integer where function = integral +instance Function Natural where function = integral + +instance Function Float where function = realFrac +instance Function Double where function = realFrac + +instance (Integral a, Function a) => Function (Ratio a) where + function = fmap (functionMap toPair fromPair) . function + where + toPair :: Ratio a -> (a, a) + toPair r = (Ratio.numerator r, Ratio.denominator r) + + fromPair :: (a, a) -> Ratio a + fromPair (n, d) = n Ratio.% d + +instance Function Char where + function = fmap (functionMap ord chr) . function + +-- instances that depend on generics + +instance Function () +instance Function Bool + +instance (Function a, Function b) => Function (Either a b) + +instance Function a => Function [a] +instance Function a => Function (Maybe a) + +-- Tuples (these are also using generics) + +-- 2 +instance + ( Function a + , Function b + ) + => Function (a, b) + +-- 3 +instance + ( Function a + , Function b + , Function c + ) + => Function (a, b, c) + +-- 4 +instance + ( Function a + , Function b + , Function c + , Function d + ) + => Function (a, b, c, d) + +-- 5 +instance + ( Function a + , Function b + , Function c + , Function d + , Function e + ) + => Function (a, b, c, d, e) + +-- 6 +instance + ( Function a + , Function b + , Function c + , Function d + , Function e + , Function f + ) + => Function (a, b, c, d, e, f) + +-- 7 +instance + ( Function a + , Function b + , Function c + , Function d + , Function e + , Function f + , Function g + ) + => Function (a, b, c, d, e, f, g) + +{------------------------------------------------------------------------------- + Support for numbers +-------------------------------------------------------------------------------} + +integral :: Integral a => Gen b -> Gen (a :-> b) +integral = + fmap (functionMap + (fmap bytes . toSignedNatural . toInteger) + (fromInteger . fromSignedNatural . fmap unbytes) + ) + . function + where + bytes :: Natural -> [Word8] + bytes 0 = [] + bytes n = fromIntegral (n `mod` 256) : bytes (n `div` 256) + + unbytes :: [Word8] -> Natural + unbytes [] = 0 + unbytes (w:ws) = fromIntegral w + 256 * unbytes ws + +realFrac :: RealFrac a => Gen b -> Gen (a :-> b) +realFrac = fmap (functionMap toRational fromRational) . function + +data Signed a = Pos a | Neg a + deriving stock (Show, Functor, Generic) + deriving anyclass (Function) + +toSignedNatural :: Integer -> Signed Natural +toSignedNatural n + | n < 0 = Neg (fromInteger (abs n - 1)) + | otherwise = Pos (fromInteger n) + +fromSignedNatural :: Signed Natural -> Integer +fromSignedNatural (Neg n) = negate (toInteger n + 1) +fromSignedNatural (Pos n) = toInteger n + +{------------------------------------------------------------------------------- + Generic support for 'Function' +-------------------------------------------------------------------------------} + +class GFunction f where + gFunction :: Gen b -> Gen (f p :-> b) + +instance GFunction f => GFunction (M1 i c f) where + gFunction = fmap (functionMap unM1 M1) . gFunction @f + +instance GFunction U1 where + gFunction = fmap (functionMap unwrap wrap) . unit + where + unwrap :: U1 p -> () + unwrap _ = () + + wrap :: () -> U1 p + wrap _ = U1 + +instance (GFunction f, GFunction g) => GFunction (f :*: g) where + gFunction = fmap (functionMap unwrap wrap) . prod (gFunction @f) (gFunction @g) + where + unwrap :: (f :*: g) p -> (f p, g p) + unwrap (x :*: y) = (x, y) + + wrap :: (f p, g p) -> (f :*: g) p + wrap (x, y) = x :*: y + +instance (GFunction f, GFunction g) => GFunction (f :+: g) where + gFunction = + fmap (functionMap unwrap wrap) . sum (gFunction @f) (gFunction @g) + where + unwrap :: (f :+: g) p -> Either (f p) (g p) + unwrap (L1 x) = Left x + unwrap (R1 y) = Right y + + wrap :: Either (f p) (g p) -> (f :+: g) p + wrap (Left x) = L1 x + wrap (Right y) = R1 y + +instance Function a => GFunction (K1 i a) where + gFunction = fmap (functionMap unK1 K1) . function @a diff --git a/src/Test/Falsify/Reexported/Generator/Precision.hs b/src/Test/Falsify/Reexported/Generator/Precision.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Reexported/Generator/Precision.hs @@ -0,0 +1,84 @@ +-- | Fixed precision generators +module Test.Falsify.Reexported.Generator.Precision ( + -- * @n@-bit words + WordN(..) + , wordN + -- ** Fractions + , properFraction + ) where + +import Prelude hiding (properFraction) + +import Data.Bits +import Data.Word +import GHC.Stack + +import Test.Falsify.Internal.Generator +import Test.Falsify.Internal.Range +import Test.Falsify.Internal.SampleTree (sampleValue) +import Test.Falsify.Internal.Search + +{------------------------------------------------------------------------------- + @n@-bit word +-------------------------------------------------------------------------------} + +-- | @n@-bit word +data WordN = WordN Precision Word64 + deriving (Show, Eq, Ord) + +forgetPrecision :: WordN -> Word64 +forgetPrecision (WordN _ x) = x + +-- | Make @n@-bit word (@n <= 64@) +-- +-- Bits outside the requested precision will be zeroed. +-- +-- We use this to generate random @n@-bit words from random 64-bit words. +-- It is important that we /truncate/ rather than /cap/ the value: capping the +-- value (limiting it to a certain maximum) would result in a strong bias +-- towards that maximum value. +-- +-- Of course, /shrinking/ of a Word64 bit does not translate automatically to +-- shrinking of the lower @n@ bits of that word (a decrease in the larger +-- 'Word64' may very well be an /increase/ in the lower @n@ bits), so this must +-- be taken into account. +truncateAt :: Precision -> Word64 -> WordN +truncateAt desiredPrecision x = + WordN actualPrecision (x .&. mask actualPrecision) + where + maximumPrecision, actualPrecision :: Precision + maximumPrecision = Precision 64 + actualPrecision = min desiredPrecision maximumPrecision + + -- Maximum possible value + -- + -- If @n == 64@ then @2 ^ n@ will overflow, but it will overflow to @0@, and + -- @(-1) :: Word64 == maxBound@; so no need to treat this case separately. + mask :: Precision -> Word64 + mask (Precision n) = 2 ^ n - 1 + +-- | Uniform selection of @n@-bit word of given precision, shrinking towards 0 +wordN :: Precision -> Gen WordN +wordN p = + fmap (truncateAt p . sampleValue) . primWith $ + binarySearch + . forgetPrecision + . truncateAt p + . sampleValue + +{------------------------------------------------------------------------------- + Fractions +-------------------------------------------------------------------------------} + +-- | Compute fraction from @n@-bit word +mkFraction :: WordN -> ProperFraction +mkFraction (WordN (Precision p) x) = + ProperFraction $ (fromIntegral x) / (2 ^ p) + +-- | Uniform selection of fraction, shrinking towards 0 +-- +-- Precondition: precision must be at least 1 bit (a zero-bit number is constant +-- 0; it is meaningless to have a fraction in a point range). +properFraction :: HasCallStack => Precision -> Gen ProperFraction +properFraction (Precision 0) = error "fraction: 0 precision" +properFraction p = mkFraction <$> wordN p diff --git a/src/Test/Falsify/Reexported/Generator/Shrinking.hs b/src/Test/Falsify/Reexported/Generator/Shrinking.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Reexported/Generator/Shrinking.hs @@ -0,0 +1,128 @@ +module Test.Falsify.Reexported.Generator.Shrinking ( + -- * User-specified shrinking + shrinkToOneOf + , firstThen + , shrinkWith + -- * Support for shrink trees + , fromShrinkTree + , toShrinkTree + ) where + +import Prelude hiding (properFraction) + +import Data.Word + +import qualified Data.Tree as Rose + +import Test.Falsify.Internal.Generator +import Test.Falsify.Internal.SampleTree (Sample(..), SampleTree) + +{------------------------------------------------------------------------------- + Specialized shrinking behaviour +-------------------------------------------------------------------------------} + +-- | Start with @x@, then shrink to one of the @xs@ +-- +-- Once shrunk, will not shrink again. +-- +-- Minimal value is the first shrunk value, if it exists, and the original +-- otherwise. +shrinkToOneOf :: forall a. a -> [a] -> Gen a +shrinkToOneOf x xs = + aux <$> primWith shrinker + where + aux :: Sample -> a + aux (NotShrunk _) = x + aux (Shrunk i) = index i xs + + -- When we shrink, we will try a bunch of new sample trees; we must ensure + -- that we can try /any/ of the possible shrunk values. + -- + -- We use this to implement 'fromShrinkTree'. Here, we explore a rose tree + -- of possibilities; at every level in the tree, once we make a choice, + -- we should commit to that choice and not consider it over and over again. + -- Thus, once shrunk, we should not shrink any further. + shrinker :: Sample -> [Word64] + shrinker (Shrunk _) = [] + shrinker (NotShrunk _) = zipWith const [0..] xs + + -- Index the list of possible shrunk values. This is a bit like @(!!)@ from + -- the prelude, but with some edge cases. + -- + -- - If the list is empty, we return the unshrunk value. + -- - Otherwise, if the index exceeds the bounds, we return the last element. + -- + -- These two special cases can arise in one of two circumstances: + -- + -- - When we run the generator against the 'Minimal' tree. This will give us + -- a @Shrunk 0@ value, independent of what the specified shrinking + -- function does, and it is important that we produce the right value. + -- - When the generator is run against a sample tree that was shrunk wrt to + -- a /different/ generator. In this case the value could be anything; + -- we return the final ("least preferred") element, and then rely on + -- later shrinking to replace this with a more preferred element. + index :: Word64 -> [a] -> a + index _ [] = x + index _ [y] = y + index 0 (y:_) = y + index n (_:ys) = index (n - 1) ys + +-- | Generator that always produces @x@ as initial value, and shrinks to @y@ +firstThen :: forall a. a -> a -> Gen a +firstThen x y = x `shrinkToOneOf` [y] + +-- | Shrink with provided shrinker +-- +-- This provides compatibility with QuickCheck-style manual shrinking. +-- +-- Defined in terms of 'fromShrinkTree'; see discussion there for some +-- notes on performance. +shrinkWith :: forall a. (a -> [a]) -> Gen a -> Gen a +shrinkWith f gen = do + -- It is critical that we do not apply normal shrinking of the 'SampleTree' + -- here (not even to 'Minimal'). If we did, then the resulting shrink tree + -- would change, and we would be unable to iteratively construct a path + -- through the shrink tree. + -- + -- Of course, it can still happen that the generator gets reapplied in a + -- different context; we must take this case into account in + -- 'shrinkToOneOf'. + x <- withoutShrinking gen + fromShrinkTree $ Rose.unfoldTree (\x' -> (x', f x')) x + +{------------------------------------------------------------------------------- + Shrink trees +-------------------------------------------------------------------------------} + +-- | Construct generator from shrink tree +-- +-- This provides compatibility with Hedgehog-style integrated shrinking. +-- +-- This is O(n^2) in the number of shrink steps: as this shrinks, the generator +-- is growing a path of indices which locates a particular value in the shrink +-- tree (resulting from unfolding the provided shrinking function). At each +-- step during the shrinking process the shrink tree is re-evaluated and the +-- next value in the tree is located; since this path throws linearly, the +-- overall cost is O(n^2). +-- +-- The O(n^2) cost is only incurred on /locating/ the next element to be tested; +-- the property is not reevaluated at already-shrunk values. +fromShrinkTree :: forall a. Rose.Tree a -> Gen a +fromShrinkTree = go + where + go :: Rose.Tree a -> Gen a + go (Rose.Node x xs) = do + next <- Nothing `shrinkToOneOf` map Just xs + case next of + Nothing -> return x + Just x' -> go x' + +-- | Expose the full shrink tree of a generator +-- +-- This generator does not shrink. +toShrinkTree :: forall a. Gen a -> Gen (Rose.Tree a) +toShrinkTree gen = + Rose.unfoldTree aux . runGen gen <$> captureLocalTree + where + aux :: (a, [SampleTree]) -> (a,[(a, [SampleTree])]) + aux (x, shrunk) = (x, map (runGen gen) shrunk) diff --git a/src/Test/Falsify/Reexported/Generator/Simple.hs b/src/Test/Falsify/Reexported/Generator/Simple.hs new file mode 100644 --- /dev/null +++ b/src/Test/Falsify/Reexported/Generator/Simple.hs @@ -0,0 +1,59 @@ +-- | Simple (i.e., non-compound) generators +module Test.Falsify.Reexported.Generator.Simple ( + bool + , integral + , int + , enum + ) where + +import Prelude hiding (properFraction) + +import Data.Bits +import Data.Word + +import Test.Falsify.Internal.Generator +import Test.Falsify.Internal.Range +import Test.Falsify.Internal.SampleTree (Sample(..), sampleValue) +import Test.Falsify.Reexported.Generator.Precision + +import qualified Test.Falsify.Range as Range + +{------------------------------------------------------------------------------- + Simple generators +-------------------------------------------------------------------------------} + +-- | Generate random bool, shrink towards the given value +-- +-- Chooses with equal probability between 'True' and 'False'. +bool :: Bool -> Gen Bool +bool target = aux . sampleValue <$> primWith shrinker + where + aux :: Word64 -> Bool + aux x | msbSet x = not target + | otherwise = target + + msbSet :: forall a. FiniteBits a => a -> Bool + msbSet x = testBit x (finiteBitSize (undefined :: a) - 1) + + shrinker :: Sample -> [Word64] + shrinker (Shrunk 0) = [] + shrinker _ = [0] + +{------------------------------------------------------------------------------- + Integral ranges +-------------------------------------------------------------------------------} + +-- | Generate value of integral type +integral :: Integral a => Range a -> Gen a +integral r = Range.eval properFraction r + +-- | Type-specialization of 'integral' +int :: Range Int -> Gen Int +int = integral + +-- | Generate value of enumerable type +-- +-- For most types 'integral' is preferred; the 'Enum' class goes through 'Int', +-- and is therefore also limited by the range of 'Int'. +enum :: forall a. Enum a => Range a -> Gen a +enum r = toEnum <$> integral (fromEnum <$> r) diff --git a/src/Test/Tasty/Falsify.hs b/src/Test/Tasty/Falsify.hs new file mode 100644 --- /dev/null +++ b/src/Test/Tasty/Falsify.hs @@ -0,0 +1,28 @@ +-- | Support for @falsify@ in the @tasty@ framework +-- +-- As is customary, this also re-exports parts of the @falsify@ API, but not +-- modules such as "Test.Falsify.Range" that are intended to be imported +-- qualified. +module Test.Tasty.Falsify ( + -- * Test property + testProperty + -- * Configure test behaviour + , TestOptions(..) + , Verbose(..) + , ExpectFailure(..) + , testPropertyWith + -- * Re-exports + , module Test.Falsify.Property + -- ** Generators + , Gen + -- ** Functions + , pattern Gen.Fn + , pattern Gen.Fn2 + , pattern Gen.Fn3 + ) where + +import Test.Falsify.Generator (Gen) +import Test.Falsify.Internal.Driver.Tasty +import Test.Falsify.Property + +import qualified Test.Falsify.Reexported.Generator.Function as Gen diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,35 @@ +module Main (main) where + +import Test.Tasty + +import qualified TestSuite.Sanity.Predicate +import qualified TestSuite.Sanity.Range +import qualified TestSuite.Sanity.Selective + +import qualified TestSuite.Prop.Generator.Compound +import qualified TestSuite.Prop.Generator.Function +import qualified TestSuite.Prop.Generator.Marking +import qualified TestSuite.Prop.Generator.Precision +import qualified TestSuite.Prop.Generator.Prim +import qualified TestSuite.Prop.Generator.Selective +import qualified TestSuite.Prop.Generator.Shrinking +import qualified TestSuite.Prop.Generator.Simple + +main :: IO () +main = defaultMain $ testGroup "falsify" [ + testGroup "Sanity" [ + TestSuite.Sanity.Range.tests + , TestSuite.Sanity.Selective.tests + , TestSuite.Sanity.Predicate.tests + ] + , testGroup "Prop" [ + TestSuite.Prop.Generator.Prim.tests + , TestSuite.Prop.Generator.Selective.tests + , TestSuite.Prop.Generator.Marking.tests + , TestSuite.Prop.Generator.Precision.tests + , TestSuite.Prop.Generator.Simple.tests + , TestSuite.Prop.Generator.Shrinking.tests + , TestSuite.Prop.Generator.Compound.tests + , TestSuite.Prop.Generator.Function.tests + ] + ] diff --git a/test/TestSuite/Prop/Generator/Compound.hs b/test/TestSuite/Prop/Generator/Compound.hs new file mode 100644 --- /dev/null +++ b/test/TestSuite/Prop/Generator/Compound.hs @@ -0,0 +1,323 @@ +module TestSuite.Prop.Generator.Compound (tests) where + +import Control.Monad +import Data.Default +import Data.Foldable (toList) +import Data.Word +import Test.Tasty +import Test.Tasty.Falsify + +import qualified Data.Tree as Rose + +import Test.Falsify.Predicate (Predicate, (.$)) +import Test.Falsify.Generator (ShrinkTree, Permutation, Tree(..)) + +import qualified Test.Falsify.Generator as Gen +import qualified Test.Falsify.Predicate as P +import qualified Test.Falsify.Range as Range + +import TestSuite.Util.List + +import qualified TestSuite.Util.Tree as Tree + +tests :: TestTree +tests = testGroup "TestSuite.Prop.Generator.Compound" [ + testGroup "list" [ + testGroup "towardsShorter" [ + testProperty "shrinking" prop_list_towardsShorter_shrinking + , testProperty "minimum" prop_list_towardsShorter_minimum + ] + , testGroup "towardsShorterEven" [ + testPropertyWith expectFailure "shrinking" prop_list_towardsShorterEven_shrinking_wrong + , testProperty "minimum" prop_list_towardsShorterEven_minimum + ] + , testGroup "towardsLonger" [ + testProperty "shrinking" prop_list_towardsLonger_shrinking + , testProperty "minimum" prop_list_towardsLonger_minimum + ] + , testGroup "towardsOrigin" [ + testProperty "minimum" prop_list_towardsOrigin_minimum + ] + ] + , testGroup "perm" [ + testProperty "shrinking" prop_perm_shrinking + , testGroup "minimum" [ + testPropertyWith def{overrideMaxRatio = Just 1000} + (show n) $ prop_perm_minimum n + | n <- [0 .. 9] + ] + ] + , testGroup "tree" [ + testProperty "towardsSmaller1" prop_tree_towardsSmaller1 + , testProperty "towardsSmaller2" prop_tree_towardsSmaller2 + , testProperty "towardsOrigin1" prop_tree_towardsOrigin1 + , testProperty "towardsOrigin2" prop_tree_towardsOrigin2 + ] + , testGroup "shrinkTree" [ + testProperty "pathAny" prop_pathAny + , testProperty "toShrinkTree" prop_toShrinkTree + ] + , testGroup "frequency" [ + testProperty "shrinking" prop_frequency_shrinking + , testPropertyWith expectFailure + "shrinking_wrong" prop_frequency_shrinking_wrong + , testProperty "replicateM" prop_replicateM_shrinking + ] + ] + where + expectFailure :: TestOptions + expectFailure = def { + expectFailure = ExpectFailure + , overrideNumTests = Just 10_000 + } + +{------------------------------------------------------------------------------- + Lists + + Here and elsewhere, for the 'testMinimum' tests, we don't /always/ fail, but + check some property. This ensures that the minimum value isn't just always the + one produced by the @Minimal@ sample tree. +-------------------------------------------------------------------------------} + +prop_list_towardsShorter_shrinking :: Property () +prop_list_towardsShorter_shrinking = + testShrinkingOfGen (P.ge `P.on` P.fn ("length", length)) $ + Gen.list (Range.between (10, 20)) $ + Gen.int $ Range.between (0, 1) + +prop_list_towardsShorter_minimum :: Property () +prop_list_towardsShorter_minimum = + testMinimum (P.satisfies ("expectedLength", (== 10) . length)) $ do + xs <- gen $ Gen.list (Range.between (10, 20)) $ + Gen.int $ Range.between (0, 1) + unless (pairwiseAll (<=) xs) $ testFailed xs + +-- In principle the filtered list can /grow/ in size during shrinking (if +-- a previously odd number is shrunk to be even). +prop_list_towardsShorterEven_shrinking_wrong :: Property () +prop_list_towardsShorterEven_shrinking_wrong = + testShrinkingOfGen (P.ge `P.on` P.fn ("length", length)) $ + fmap (filter even) $ + Gen.list (Range.between (10, 20)) $ + Gen.int $ Range.withOrigin (0, 10) 5 + +-- Although [6,4] is the perfect counter-example here, we don't always get it, +-- due to binary search +prop_list_towardsShorterEven_minimum :: Property () +prop_list_towardsShorterEven_minimum = + testMinimum (P.elem .$ ("expected", [[6,4],[4,2]])) $ do + xs <- gen $ fmap (filter even) $ + Gen.list (Range.between (10, 20)) $ + Gen.int $ Range.withOrigin (0, 10) 5 + unless (pairwiseAll (<=) xs) $ testFailed xs + +prop_list_towardsLonger_shrinking :: Property () +prop_list_towardsLonger_shrinking = + testShrinkingOfGen (P.le `P.on` P.fn ("length", length)) $ + Gen.list (Range.between (10, 0)) $ + Gen.int $ Range.between (0, 1) + +prop_list_towardsLonger_minimum :: Property () +prop_list_towardsLonger_minimum = + testMinimum (P.satisfies ("expectedLength", (== 10) . length)) $ do + xs <- gen $ Gen.list (Range.between (10, 0)) $ + Gen.int $ Range.between (0, 1) + unless (pairwiseAll (<=) xs) $ testFailed xs + +prop_list_towardsOrigin_minimum :: Property () +prop_list_towardsOrigin_minimum = + testMinimum (P.satisfies ("expectedLength", (== 5) . length)) $ do + xs <- gen $ Gen.list (Range.withOrigin (0, 10) 5) $ + Gen.int $ Range.between (0, 1) + unless (pairwiseAll (<=) xs) $ testFailed xs + +{------------------------------------------------------------------------------- + Permutations (and shuffling) +-------------------------------------------------------------------------------} + +validPermShrink :: Predicate [Permutation, Permutation] +validPermShrink = mconcat [ + P.ge `P.on` P.fn ("numSwaps", length ) + , P.ge `P.on` P.fn ("distance", distance) + ] + where + distance :: Permutation -> Word + distance = sum . map weighted + + weighted :: (Word, Word) -> Word + weighted (i, j) + | i < j = error "unexpected swap" + | otherwise = (10 ^ i) * (i - j) + +prop_perm_shrinking :: Property () +prop_perm_shrinking = + testShrinkingOfGen validPermShrink $ + Gen.permutation 10 + +prop_perm_minimum :: Word -> Property () +prop_perm_minimum n = + testMinimum (P.satisfies ("suffixIsUnchanged", suffixIsUnchanged)) $ do + perm <- gen $ Gen.permutation 10 + let shuffled = Gen.applyPermutation perm [0 .. 9] + when (shuffled !! fromIntegral n /= n) $ testFailed perm + where + suffixIsUnchanged :: Permutation -> Bool + suffixIsUnchanged perm = + case perm of + [(i, j)] -> i == j + 1 && (i == n || j == n) + _otherwise -> False + +{------------------------------------------------------------------------------- + Tree + + TODO: We're currently only testing minimums here. + TODO: These are discarding a lot of tests; is it expected that a randomly + generated tree is so often weight or heigh balanced..? +-------------------------------------------------------------------------------} + +prop_tree_towardsSmaller1 :: Property () +prop_tree_towardsSmaller1 = + testMinimum (P.expect expected) $ do + t <- gen $ Gen.tree (Range.between (0, 100)) $ + Gen.int $ Range.between (0, 1) + -- "Every tree is height balanced" + unless (Tree.isHeightBalanced t) $ testFailed t + where + expected :: Tree Int + expected = Branch 0 Leaf (Branch 0 Leaf (Branch 0 Leaf Leaf)) + +prop_tree_towardsSmaller2 :: Property () +prop_tree_towardsSmaller2 = + testMinimum (P.elem .$ ("expected", expected)) $ do + t <- gen $ Gen.tree (Range.between (0, 100)) $ + Gen.int $ Range.between (0, 1) + -- "Every tree is weight balanced" + unless (Tree.isWeightBalanced t) $ testFailed t + where + -- For a minimal tree that is not weight-balanced, we need three elements in + -- one subtree and none in the other: the weight of the empty tree is 1, + -- the weight of the tree with three elements is 4, and 4 > Δ * 1, for Δ=3. + expected :: [Tree Int] + expected = [ + Branch 0 (Branch 0 (Branch 0 Leaf Leaf) (Branch 0 Leaf Leaf)) Leaf + , Branch 0 (Branch 0 Leaf (Branch 0 Leaf (Branch 0 Leaf Leaf))) Leaf + , Branch 0 Leaf (Branch 0 (Branch 0 Leaf Leaf) (Branch 0 Leaf Leaf)) + , Branch 0 Leaf (Branch 0 Leaf (Branch 0 Leaf (Branch 0 Leaf Leaf))) + ] + +prop_tree_towardsOrigin1 :: Property () +prop_tree_towardsOrigin1 = + testMinimum ( P.satisfies ("expected", expected) + `P.dot` P.fn ("size", Tree.size) + ) $ do + t <- gen $ Gen.tree (Range.withOrigin (0, 100) 10) $ pure () + unless (Tree.isHeightBalanced t) $ testFailed t + where + -- We can always find a non-balanced tree of roughly the specified size + -- (The /exact/ size might not always be reachable with single shrink steps) + expected :: Word -> Bool + expected sz = 8 <= sz && sz <= 10 + +prop_tree_towardsOrigin2 :: Property () +prop_tree_towardsOrigin2 = + testMinimum ( P.satisfies ("expected", expected) + `P.dot` P.fn ("size", Tree.size) + ) $ do + t <- gen $ Gen.tree (Range.withOrigin (0, 100) 10) $ pure () + unless (Tree.isWeightBalanced t) $ testFailed t + where + expected :: Word -> Bool + expected sz = 8 <= sz && sz <= 10 + +{------------------------------------------------------------------------------- + Shrink trees +-------------------------------------------------------------------------------} + +prop_pathAny :: Property () +prop_pathAny = + testMinimum (P.expect ["", "a", "aa"]) $ do + xs <- gen $ toList <$> Gen.pathAny st + unless (length xs < 3) $ testFailed xs + where + -- Infinite ShrinkTree containing all strings containing lowercase letters + st :: ShrinkTree String + st = Rose.unfoldTree (\xs -> (xs, map (:xs) ['a' .. 'z'])) "" + +prop_toShrinkTree :: Property () +prop_toShrinkTree = + testMinimum (P.satisfies ("expected", expected)) $ do + xs <- gen $ Gen.toShrinkTree genToTest >>= fmap toList . Gen.pathAny + unless (pairwiseAll (>) xs) $ testFailed xs + where + -- Should be any kind of path in which the last two pairs of numbers are + -- NOT decreasing. + expected :: [Word64] -> Bool + expected xs = + case reverse xs of + x : y : _ -> x >= y + _otherwise -> False + + genToTest :: Gen Word64 + genToTest = (`mod` 100) <$> Gen.prim + + +{------------------------------------------------------------------------------- + Tweak test data distribution +-------------------------------------------------------------------------------} + +propShrinkingList1 :: [Word] -> [Word] -> Bool +propShrinkingList1 = aux + where + aux [_, _, _] [_, _] = True + aux [_, _, _] [_] = True + aux [_, _] [_] = True + aux [x] [x'] = x >= x' + aux [x, y] [x', y'] = x >= x' && y >= y' + aux [x, y, z] [x', y', z'] = x >= x' && y >= y' && z >= z' + aux _ _ = error "impossible" + +propShrinkingList2 :: [Word] -> [Word] -> Bool +propShrinkingList2 = aux + where + aux :: [Word] -> [Word] -> Bool + aux [x, y, _] [x', y'] = x >= x' && y >= y' + aux [x, _, _] [x'] = x >= x' + aux [x, _] [x'] = x >= x' + aux [x] [x'] = x >= x' + aux [x, y] [x', y'] = x >= x' && y >= y' + aux [x, y, z] [x', y', z'] = x >= x' && y >= y' && z >= z' + aux _ _ = error "impossible" + +genListFrequency :: Gen [Word] +genListFrequency = + Gen.frequency [ + (1, replicateM 1 $ Gen.integral $ Range.between (0, 10)) + , (2, replicateM 2 $ Gen.integral $ Range.between (0, 10)) + , (3, replicateM 3 $ Gen.integral $ Range.between (0, 10)) + ] + +genListMonad :: Gen [Word] +genListMonad = do + n <- Gen.integral $ Range.between (1, 3) + replicateM n $ Gen.integral $ Range.between (0, 10) + +prop_frequency_shrinking :: Property () +prop_frequency_shrinking = + testShrinkingOfGen + (P.relatedBy ("propShrinkingList1", propShrinkingList1)) + genListFrequency + +-- 'propShrinkingList2' does /not/ hold for 'genListFrequency' because the +-- generators are independent +prop_frequency_shrinking_wrong :: Property () +prop_frequency_shrinking_wrong = + testShrinkingOfGen + (P.relatedBy ("propShrinkingList2", propShrinkingList2)) + genListFrequency + +-- 'propShrinkingList2' /does/ hold if we simply use 'replicateM'. +prop_replicateM_shrinking :: Property () +prop_replicateM_shrinking = + testShrinkingOfGen + (P.relatedBy ("propShrinkingList2", propShrinkingList2)) + genListMonad diff --git a/test/TestSuite/Prop/Generator/Function.hs b/test/TestSuite/Prop/Generator/Function.hs new file mode 100644 --- /dev/null +++ b/test/TestSuite/Prop/Generator/Function.hs @@ -0,0 +1,153 @@ +module TestSuite.Prop.Generator.Function (tests) where + +import Control.Monad +import Data.Default +import Data.Word +import Test.Tasty +import Test.Tasty.Falsify + +import qualified Data.Set as Set + +import Test.Falsify.Generator (Fun) + +import qualified Test.Falsify.Generator as Gen +import qualified Test.Falsify.Predicate as P +import qualified Test.Falsify.Range as Range + +tests :: TestTree +tests = testGroup "TestSuite.Prop.Generator.Function" [ + testGroup "BoolToBool" [ + testProperty "notConstant" prop_BoolToBool_notConstant + , testProperty "constant" prop_BoolToBool_constant + ] + , testProperty "Word8ToBool" prop_Word8ToBool + , testPropertyWith fewerTests "IntegerToBool" prop_IntegerToBool + , testProperty "IntToInt" prop_IntToInt + , testPropertyWith fewerTests "StringToBool" prop_StringToBool + ] + where + -- These tests are pretty slow + fewerTests :: TestOptions + fewerTests = def { + overrideNumTests = Just 10 + } + +{------------------------------------------------------------------------------- + Functions @Bool -> Bool@ + + TODO: Should we define these in terms of the concrete functions instead? +-------------------------------------------------------------------------------} + +prop_BoolToBool_notConstant :: Property () +prop_BoolToBool_notConstant = + testMinimum (P.satisfies ("isConstant", isConstant)) $ do + fn <- gen $ Gen.fun (Gen.bool False) + let Fn f = fn + -- "No function Bool -> Bool can be constant" + unless (f False /= f True) $ testFailed fn + where + isConstant :: Fun Bool Bool -> Bool + isConstant fn = show fn == "{_->False}" + +prop_BoolToBool_constant :: Property () +prop_BoolToBool_constant = do + testMinimum (P.satisfies ("notConstant", notConstant)) $ do + fn <- gen $ Gen.fun (Gen.bool False) + let Fn f = fn + -- "Every function Bool -> Bool is constant" + unless (f False == f True) $ testFailed fn + where + notConstant :: Fun Bool Bool -> Bool + notConstant fn = or [ + show fn == "{True->True, _->False}" + , show fn == "{False->True, _->False}" + ] + +{------------------------------------------------------------------------------- + Functions @Word8 -> Bool@ +-------------------------------------------------------------------------------} + +prop_Word8ToBool :: Property () +prop_Word8ToBool = do + testMinimum (P.satisfies ("notConstant", notConstant)) $ do + fn <- gen $ Gen.fun (Gen.bool False) + -- "Every function Word8 -> Bool is constant" + unless (isConstant fn) $ testFailed fn + where + notConstant :: Fun Word8 Bool -> Bool + notConstant fn = any aux [0 .. 255] + where + aux :: Word8 -> Bool + aux n = show fn == "{" ++ show n ++ "->True, _->False}" + + isConstant :: Fun Word8 Bool -> Bool + isConstant (Fn f) = + (\s -> Set.size s == 1) $ + Set.fromList (map f [minBound .. maxBound]) + +{------------------------------------------------------------------------------- + Functions @Integer -> Bool@ + + This is the first test where the input domain is infinite. +-------------------------------------------------------------------------------} + +prop_IntegerToBool :: Property () +prop_IntegerToBool = + testMinimum (P.satisfies ("expected", expected)) $ do + fn <- gen $ Gen.fun (Gen.bool False) + let Fn f = fn + -- "Every fn from Integer to Bool must give the same result for π and φ" + unless (f 3142 == f 1618) $ testFailed fn + where + expected :: Fun Integer Bool -> Bool + expected fn = or [ + show fn == "{1618->True, _->False}" + , show fn == "{3142->True, _->False}" + ] + +{------------------------------------------------------------------------------- + Functions @Int -> Int@ +-------------------------------------------------------------------------------} + +prop_IntToInt :: Property () +prop_IntToInt = + testMinimum (P.satisfies ("expected", expected)) $ do + fn <- gen $ Gen.fun (Gen.integral $ Range.between (0, 100)) + let Fn f = fn + unless (f 0 == 0 && f 1 == 0) $ testFailed fn + where + expected :: Fun Int Int -> Bool + expected fn = or [ + show fn == "{1->1, _->0}" + , show fn == "{0->1, _->0}" + ] + +{------------------------------------------------------------------------------- + Functions @String -> Bool@ + + This example (as well as 'test_IntToInt_mapFilter') is adapted from + Koen Claessen's presentation "Shrinking and showing functions" + at Haskell Symposium 2012 . + + TODO: His example uses longer strings, which does work, it's just expensive. + We can definitely use some performance optimization here. +-------------------------------------------------------------------------------} + +prop_StringToBool :: Property () +prop_StringToBool = + testMinimum (P.satisfies ("expected", expected)) $ do + fn <- gen $ Gen.fun (Gen.bool False) + let Fn p = fn + unless (p "abc" `implies` p "def") $ testFailed fn + where + -- TODO: Actually, the second case doesn't seem to get triggered. Not sure + -- why; maybe it's just unlikely..? + expected :: Fun String Bool -> Bool + expected fn = or [ + show fn == "{\"abc\"->True, _->False}" + , show fn == "{\"def\"->True, _->False}" + ] + + implies :: Bool -> Bool -> Bool + implies False _ = True + implies True b = b diff --git a/test/TestSuite/Prop/Generator/Marking.hs b/test/TestSuite/Prop/Generator/Marking.hs new file mode 100644 --- /dev/null +++ b/test/TestSuite/Prop/Generator/Marking.hs @@ -0,0 +1,84 @@ +module TestSuite.Prop.Generator.Marking (tests) where + +import Control.Monad +import Data.Map (Map) +import Data.Maybe (catMaybes) +import Data.Word +import Test.Tasty +import Test.Tasty.Falsify + +import qualified Data.Map as Map +import qualified Data.Set as Set + +import Test.Falsify.Generator (Marked(..), Mark(..)) + +import qualified Test.Falsify.Generator as Gen hiding (mark) +import qualified Test.Falsify.Predicate as P + +import TestSuite.Util.List + +tests :: TestTree +tests = testGroup "TestSuite.Prop.Generator.Marking" [ + testGroup "list" [ + testProperty "shrinking" prop_list_shrinking + , testProperty "minimum" prop_list_minimum + ] + ] + +{------------------------------------------------------------------------------- + Marking +-------------------------------------------------------------------------------} + +-- | Mark an element +-- +-- Marks as 'Drop' with 50% probability. +-- +-- We avoid using 'Gen.mark' here, which depends on @shrinkTo@. This version +-- uses only 'Gen.prim'; the difference in behaviour is that this version of +-- @mark@ can produce elements that are marked as drop from the get-go. +mark :: Gen a -> Gen (Marked Gen a) +mark x = flip Marked x <$> (aux <$> Gen.prim) + where + aux :: Word64 -> Mark + aux n = if n >= maxBound `div` 2 then Keep else Drop + +{------------------------------------------------------------------------------- + List +-------------------------------------------------------------------------------} + +genMarkedList :: Gen [(Word, Word64)] +genMarkedList = do + xs <- forM [0 .. 9] (\i -> mark ((i, ) <$> Gen.prim)) + catMaybes <$> Gen.selectAllKept xs + +prop_list_shrinking :: Property () +prop_list_shrinking = + testShrinkingOfGen + ( mconcat [ + P.flip (P.relatedBy ("isSubsetOf", Set.isSubsetOf)) + `P.on` P.fn ("keysSet", Map.keysSet) + , P.relatedBy ("shrunkCod", shrunkCod) + ] + `P.on` P.transparent Map.fromList + ) + genMarkedList + where + shrunkCod :: Map Word Word64 -> Map Word Word64 -> Bool + shrunkCod orig shrunk = and [ + -- The 'shrunkDom' check justifies the use of @(!)@ here + orig Map.! k >= v + | (k, v) <- Map.toList shrunk + ] + +prop_list_minimum :: Property () +prop_list_minimum = + testMinimum (P.satisfies ("expected", expected)) $ do + xs <- gen $ genMarkedList + case xs of + (0, _):_ -> discard + _otherwise -> return () + unless (pairwiseAll (==) $ map snd xs) $ testFailed xs + where + expected :: [(Word, Word64)] -> Bool + expected [(i, 0), (j, 1)] | i < j = True + expected _otherwise = False diff --git a/test/TestSuite/Prop/Generator/Precision.hs b/test/TestSuite/Prop/Generator/Precision.hs new file mode 100644 --- /dev/null +++ b/test/TestSuite/Prop/Generator/Precision.hs @@ -0,0 +1,69 @@ +module TestSuite.Prop.Generator.Precision (tests) where + +import Control.Monad +import Test.Tasty +import Test.Tasty.Falsify + +import Test.Falsify.Generator (WordN(..)) +import Test.Falsify.Range (Precision(..), ProperFraction(..)) + +import qualified Test.Falsify.Generator as Gen +import qualified Test.Falsify.Predicate as P + +tests :: TestTree +tests = testGroup "TestSuite.Prop.Generator.Precision" [ + testGroup "wordN" [ + testGroup (show p) [ + testProperty "shrinking" $ prop_wordN_shrinking p + , testProperty "minimum" $ prop_wordN_minimum p + ] + | p <- map Precision [0, 1, 2, 3, 63, 64] + ] + , testGroup "fraction" [ + testGroup (show p) [ + testProperty "shrinking" $ prop_fraction_shrinking (Precision p) + , testProperty "minimum" $ prop_fraction_minimum (Precision p) target expected + ] + | (p, target, expected) <- [ + -- The higher the precision, the closer we can get to the target + (2 , 50, 75) + , (3 , 50, 62) + , (4 , 50, 56) + , (5 , 50, 53) + , (63 , 50, 51) + , (64 , 50, 51) + ] + ] + ] + +{------------------------------------------------------------------------------- + wordN +-------------------------------------------------------------------------------} + +prop_wordN_shrinking :: Precision -> Property () +prop_wordN_shrinking p = + testShrinkingOfGen P.ge $ Gen.wordN p + +prop_wordN_minimum :: Precision -> Property () +prop_wordN_minimum p = + testMinimum (P.expect $ WordN p 0) $ do + x <- gen $ Gen.wordN p + testFailed x + +{------------------------------------------------------------------------------- + fraction +-------------------------------------------------------------------------------} + +prop_fraction_shrinking :: Precision -> Property () +prop_fraction_shrinking p = + testShrinkingOfGen P.ge $ Gen.properFraction p + +prop_fraction_minimum :: Precision -> Word -> Word -> Property () +prop_fraction_minimum p target expected = + testMinimum ((P.expect expected) `P.dot` P.fn ("pct", pct)) $ do + x <- gen $ Gen.properFraction p + unless (pct x <= target) $ testFailed x + where + pct :: ProperFraction -> Word + pct (ProperFraction f) = round (f * 100) + diff --git a/test/TestSuite/Prop/Generator/Prim.hs b/test/TestSuite/Prop/Generator/Prim.hs new file mode 100644 --- /dev/null +++ b/test/TestSuite/Prop/Generator/Prim.hs @@ -0,0 +1,383 @@ +module TestSuite.Prop.Generator.Prim (tests) where + +import Prelude hiding (pred) + +import Control.Monad +import Control.Selective +import Data.Default +import Data.Word +import Test.Tasty +import Test.Tasty.Falsify + +import qualified Test.Falsify.Generator as Gen +import qualified Test.Falsify.Predicate as P + +import TestSuite.Util.List + +tests :: TestTree +tests = testGroup "TestSuite.Prop.Generator.Prim" [ + testGroup "prim" [ + testProperty "shrinking" prop_prim_shrinking + , testGroup "minimum" [ + testProperty (show target) $ prop_prim_minimum target + | target <- [0 .. 4] + ] + , testPropertyWith (def { expectFailure = ExpectFailure }) + "prim_minimum_wrong" prop_prim_minimum_wrong + ] + , testGroup "applicative" [ + testGroup "pair" [ + testProperty "shrinking" prop_applicative_pair_shrinking + , testProperty "minimum1" prop_applicative_pair_minimum1 + , testProperty "minimum2" prop_applicative_pair_minimum2 + ] + , testGroup "replicateM" [ + testProperty "shrinking" prop_applicative_replicateM_shrinking + , testProperty "minimum" prop_applicative_replicateM_minimum + ] + ] + , testGroup "monad" [ + testGroup "maybe" [ + testGroup "towardsNothing" [ + testProperty "shrinking" prop_monad_maybe_towardsNothing_shrinking + , testProperty "minimum" prop_monad_maybe_towardsNothing_minimum + , testPropertyWith expectFailure + "shrinking_wrong" prop_monad_maybe_towardsNothing_shrinking_wrong + ] + , testGroup "towardsJust" [ + testProperty "shrinking" prop_monad_maybe_towardsJust_shrinking + , testProperty "minimum" prop_monad_maybe_towardsJust_minimum + , testPropertyWith expectFailure + "minimum_wrong" prop_monad_maybe_towardsJust_minimum_wrong + ] + ] + , testGroup "either" [ + testProperty "shrinking" prop_monad_either_shrinking + ] + ] + , testGroup "selective" [ + testGroup "either" [ + testPropertyWith expectFailure + "shrinking" prop_selective_either_shrinking_wrong + ] + ] + , testGroup "captureLocalTree" [ + testProperty "shrinking1" prop_captureLocalTree_shrinking1 + , testProperty "shrinking2" prop_captureLocalTree_shrinking2 + ] + , testGroup "stream" [ + testProperty "shrinking1" prop_stream_shrinking1 + , testProperty "shrinking2" prop_stream_shrinking2 + , testProperty "minimum" prop_stream_minimum + ] + ] + where + expectFailure :: TestOptions + expectFailure = def { + expectFailure = ExpectFailure + , overrideNumTests = Just 100_000 + } + +{------------------------------------------------------------------------------- + Prim +-------------------------------------------------------------------------------} + +-- Gen.prime is the only generator where we a /strict/ inequality +prop_prim_shrinking :: Property () +prop_prim_shrinking = testShrinkingOfGen P.gt $ Gen.prim + +-- The minimum is always 0, unless 0 is not a counter-example +prop_prim_minimum :: Word64 -> Property () +prop_prim_minimum target = do + testMinimum (P.expect $ if target == 0 then 1 else 0) $ do + x <- gen $ Gen.prim + unless (x == target) $ testFailed x + +-- | Just to verify that we if we specify the /wrong/ minimum, we get a failure +prop_prim_minimum_wrong :: Property () +prop_prim_minimum_wrong = + testMinimum (P.expect 1) $ do + x <- gen $ Gen.prim + testFailed x + +{------------------------------------------------------------------------------- + Applicative: pairs +-------------------------------------------------------------------------------} + +prop_applicative_pair_shrinking :: Property () +prop_applicative_pair_shrinking = + testShrinkingOfGen (P.relatedBy ("validShrink", validShrink)) $ + (,) <$> Gen.prim <*> Gen.prim + where + validShrink :: (Word64, Word64) -> (Word64, Word64) -> Bool + validShrink (x, y) (x', y') = x >= x' && y >= y' + +prop_applicative_pair_minimum1 :: Property () +prop_applicative_pair_minimum1 = + testMinimum (P.expect (1, 0)) $ do + (x, y) <- gen $ (,) <$> Gen.prim <*> Gen.prim + unless (x == 0 || x < y) $ testFailed (x, y) + +prop_applicative_pair_minimum2 :: Property () +prop_applicative_pair_minimum2 = + testMinimum (P.expect (1, 1)) $ do + (x, y) <- gen $ (,) <$> Gen.prim <*> Gen.prim + unless (x == 0 || x > y) $ testFailed (x, y) + +{------------------------------------------------------------------------------- + Applicative: replicateM +-------------------------------------------------------------------------------} + +genList :: Gen [Word64] +genList = do + n <- (`min` 10) <$> Gen.prim + replicateM (fromIntegral n) Gen.prim + +prop_applicative_replicateM_shrinking :: Property () +prop_applicative_replicateM_shrinking = + testShrinkingOfGen (P.relatedBy ("validShrink", validShrink)) genList + where + validShrink :: [Word64] -> [Word64] -> Bool + validShrink [] [] = True + validShrink [] (_:_) = False + validShrink (_:_) [] = True + validShrink (x:xs) (y:ys) = x >= y && validShrink xs ys + +prop_applicative_replicateM_minimum :: Property () +prop_applicative_replicateM_minimum = + testMinimum (P.expect [0,1]) $ do + xs <- gen $ genList + unless (pairwiseAll (==) xs) $ testFailed xs + +{------------------------------------------------------------------------------- + Monad: Maybe (towards 'Nothing') +-------------------------------------------------------------------------------} + +genSmall :: Gen Word64 +genSmall = do + startWithEven <- Gen.prim + if startWithEven >= maxBound `div` 2 + then Gen.exhaustive 100 + else Gen.exhaustive 99 -- smaller bound, to ensure shrinking + +genTowardsNothing :: Gen (Maybe Word64, Word64) +genTowardsNothing = do + genNothing <- (== 0) <$> Gen.prim + if genNothing + then (\ y -> (Nothing, y)) <$> genSmall + else (\x y -> (Just x, y)) <$> genSmall <*> genSmall + +prop_monad_maybe_towardsNothing_shrinking :: Property () +prop_monad_maybe_towardsNothing_shrinking = + testShrinkingOfGen + (P.relatedBy ("validShrink", validShrink)) + genTowardsNothing + where + validShrink :: (Maybe Word64, Word64) -> (Maybe Word64, Word64) -> Bool + validShrink (Nothing , y) (Nothing , y') = y >= y' + validShrink (Just _ , _) (Nothing , _ ) = True -- See @.._wrong@ property + validShrink (Nothing , _) (Just _ , _ ) = False + validShrink (Just x , y) (Just x' , y') = x >= x' && y >= y' + +prop_monad_maybe_towardsNothing_minimum :: Property () +prop_monad_maybe_towardsNothing_minimum = + testMinimum (P.expect expected) $ do + (x, y) <- gen $ genTowardsNothing + unless (even y) $ testFailed (x, y) + where + -- We are using different generators, a switch from 'Just' to 'Nothing' + -- might temporarily because @y@ to increase (see @.._wrong@), but we will + -- then continue to shrink that value. + expected :: (Maybe Word64, Word64) + expected = (Nothing, 1) + +prop_monad_maybe_towardsNothing_shrinking_wrong :: Property () +prop_monad_maybe_towardsNothing_shrinking_wrong = + testShrinkingOfGen + (P.relatedBy ("validShrink", validShrink)) + genTowardsNothing + where + -- This property is wrong: the two generators on the RHS have a different + -- structure, and therefore shrink independently. When we switch the + -- LHS from Just to Nothing, we run a /different/ generator. + validShrink :: (Maybe Word64, Word64) -> (Maybe Word64, Word64) -> Bool + validShrink (Nothing , y) (Nothing , y') = y >= y' + validShrink (Just _ , y) (Nothing , y') = y >= y' + validShrink (Nothing , _) (Just _ , _) = False + validShrink (Just x , y) (Just x' , y') = x >= x' && y >= y' + +{------------------------------------------------------------------------------- + Monad: Maybe (towards 'Just') + + Unlike hypothesis, we are always dealing with infinite sample tree; if a + "simpler" test case needs more samples, then they are available. +-------------------------------------------------------------------------------} + +genTowardsJust :: Gen (Maybe Word64, Word64) +genTowardsJust = do + genJust <- (== 0) <$> Gen.prim + if genJust + then (\x y -> (Just x, y)) <$> genSmall <*> genSmall + else (\ y -> (Nothing, y)) <$> genSmall + +prop_monad_maybe_towardsJust_shrinking :: Property () +prop_monad_maybe_towardsJust_shrinking = + testShrinkingOfGen + (P.relatedBy ("validShrink", validShrink)) + genTowardsJust + where + validShrink :: (Maybe Word64, Word64) -> (Maybe Word64, Word64) -> Bool + validShrink (Nothing , y) (Nothing , y') = y >= y' + validShrink (Just _ , _) (Nothing , _ ) = False + validShrink (Nothing , _) (Just _ , _ ) = True + validShrink (Just x , y) (Just x' , y') = x >= x' && y >= y' + +prop_monad_maybe_towardsJust_minimum :: Property () +prop_monad_maybe_towardsJust_minimum = + testMinimum (P.satisfies ("expected", expected)) $ do + (x, y) <- gen $ genTowardsJust + unless (even y) $ testFailed (x, y) + where + expected :: (Maybe Word64, Word64) -> Bool + expected (Just _ , y) = y == 1 + expected (Nothing , _) = True + +prop_monad_maybe_towardsJust_minimum_wrong :: Property () +prop_monad_maybe_towardsJust_minimum_wrong = + testMinimum (P.expect expected) $ do + (x, y) <- gen $ genTowardsJust + unless (even y) $ testFailed (x, y) + where + -- We might not always be able to shrink from 'Nothing' to 'Just', because + -- the /value/ of that 'Just' might not be a counter-example; we would need + -- to take two shrink steps at once (switch from 'Just' to 'Nothing' /and/ + -- reduce the value of the 'Just'). + -- + -- 'Selective' does not help either (it also would need to take two steps); + -- we /could/ try to solve the problem by generating /both/ values always, + -- and using only one, but as we know, that is not an effective strategy: + -- generated-by-not-used values will always be shrunk to their minimal + -- value, independent of the property. + expected :: (Maybe Word64, Word64) + expected = (Just 0, 1) + +{------------------------------------------------------------------------------- + Monad: Either +-------------------------------------------------------------------------------} + +genMonadEither :: Gen (Either Word64 Word64) +genMonadEither = do + genLeft <- (== 0) <$> Gen.prim -- shrink towards left + if genLeft + then Left <$> Gen.prim + else Right <$> Gen.prim + +prop_monad_either_shrinking :: Property () +prop_monad_either_shrinking = + testShrinkingOfGen + (P.relatedBy ("validShrink", validShrink)) + genMonadEither + where + -- The 'Left' and 'Right' case use the /same/ part of the sample tree, so + -- that if we shrink from one to the other, we /must/ get the same value. + validShrink :: Either Word64 Word64 -> Either Word64 Word64 -> Bool + validShrink _ (Left 0) = True -- We can always shrink to 'Minimal' + validShrink (Left x) (Left x') = x >= x' + validShrink (Left _) (Right _) = False + validShrink (Right x) (Left x') = x == x' + validShrink (Right x) (Right x') = x >= x' + +{------------------------------------------------------------------------------- + Selective: either +-------------------------------------------------------------------------------} + +genSelectiveEither :: Gen (Either Word64 Word64) +genSelectiveEither = + ifS ((== 0) <$> Gen.prim) + (Left <$> Gen.prim) + (Right <$> Gen.prim) + +prop_selective_either_shrinking_wrong :: Property () +prop_selective_either_shrinking_wrong = + testShrinkingOfGen + (P.relatedBy ("validShrink", validShrink)) + genSelectiveEither + where + -- Like in 'prop_monad_either_shrinking', here the two generators are + -- independent, and so it's entirely possible we might shrink from @Right x@ + -- to @Left y@ for @x /= y@. + validShrink :: Either Word64 Word64 -> Either Word64 Word64 -> Bool + validShrink _ (Left 0) = True -- We can always shrink to 'Minimal' + validShrink (Left x) (Left x') = x >= x' + validShrink (Left _) (Right _) = False + validShrink (Right x) (Left x') = x == x' + validShrink (Right x) (Right x') = x >= x' + +{------------------------------------------------------------------------------- + captureLocalTree +-------------------------------------------------------------------------------} + +prop_captureLocalTree_shrinking1 :: Property () +prop_captureLocalTree_shrinking1 = + testShrinkingOfGen P.alwaysFail $ + Gen.captureLocalTree + +-- Check that we /still/ cannot shrink (i.e., monadic bind is not +-- introducing a bug somewhere) +prop_captureLocalTree_shrinking2 :: Property () +prop_captureLocalTree_shrinking2 = + testShrinkingOfGen P.alwaysFail $ do + t1 <- Gen.captureLocalTree + t2 <- Gen.captureLocalTree + return (t1, t2) + +{------------------------------------------------------------------------------- + Stream + + The purpose of this test is to test generation (and shrinking) of infinite + data structures. The function generation tests will verify that also, but they + are much more complicated. +-------------------------------------------------------------------------------} + +-- | Infinite stream of values +-- +-- Intentionally does not have a 'Show' instance! +data Stream a = Stream a (Stream a) + +prefix :: Stream a -> Word64 -> [a] +prefix _ 0 = [] +prefix (Stream x xs) n = x : prefix xs (n - 1) + +genStream :: Gen (Stream Word64) +genStream = Stream <$> Gen.exhaustive 10 <*> genStream + +genStreamPrefix :: Gen [Word64] +genStreamPrefix = prefix <$> genStream <*> Gen.exhaustive 10 + +-- | Check that we can test shrinking of infinite structures /at all/ +prop_stream_shrinking1 :: Property () +prop_stream_shrinking1 = + testShrinkingOfGen P.alwaysPass $ + genStreamPrefix + +-- | Check that we shrink in the way we expect +prop_stream_shrinking2 :: Property () +prop_stream_shrinking2 = + testShrinkingOfGen pred $ + genStreamPrefix + where + pred :: P.Predicate '[[Word64], [Word64]] + pred = mconcat [ + P.ge `P.on` P.fn ("length", length) + , P.relatedBy ("elemsRelated", elemsRelated) + ] + + elemsRelated :: [Word64] -> [Word64] -> Bool + elemsRelated orig shrunk = and $ zipWith (>=) orig shrunk + +prop_stream_minimum :: Property () +prop_stream_minimum = + testMinimum (P.expect [0, 0]) $ do + xs <- gen genStreamPrefix + unless (pairwiseAll (<) xs) $ testFailed xs + diff --git a/test/TestSuite/Prop/Generator/Selective.hs b/test/TestSuite/Prop/Generator/Selective.hs new file mode 100644 --- /dev/null +++ b/test/TestSuite/Prop/Generator/Selective.hs @@ -0,0 +1,99 @@ +module TestSuite.Prop.Generator.Selective (tests) where + +import Control.Monad +import Control.Selective +import Data.Default +import Data.Word +import Test.Tasty +import Test.Tasty.Falsify + +import qualified Test.Falsify.Generator as Gen +import qualified Test.Falsify.Predicate as P + +tests :: TestTree +tests = testGroup "TestSuite.Prop.Generator.Selective" [ + testGroup "pair" [ + testProperty "ifM" $ prop_pair ifM + , testPropertyWith expectFailure "ifS" $ prop_pair ifS + , testProperty "ifThenElse" $ prop_pair_ifThenElse + ] + ] + where + expectFailure :: TestOptions + expectFailure = def { + expectFailure = ExpectFailure + , overrideNumTests = Just 10_000 + } + +{------------------------------------------------------------------------------- + Either + + We only only primitive generators here (avoiding generators like + 'Test.Falsify.Reexported.Generator.Simple.bool') to avoid getting distracted + by specific implementation details of derived generators. +-------------------------------------------------------------------------------} + +-- If we use monadic bind, the seed for the Right value is reused when +-- when we shrink it to Left: they are not independent. +-- +-- Here this is still somewhat reasonable, but in general this means we +-- will reuse a seed reduced in one context in a completely different +-- context, which may not make any sense at all. +propEither :: + (Word64, Either Word64 Word64) + -> (Word64, Either Word64 Word64) + -> Bool +propEither _ (_, Left 0) = True -- Can always shrink to 'Minimal' +propEither (_, Right x) (_, Left y) = x == y +propEither _ _ = True + +genPair :: + (forall a. Gen Bool -> Gen a -> Gen a -> Gen a) + -> Gen (Word64, Either Word64 Word64) +genPair if_ = + (,) <$> Gen.prim + <*> if_ ((== 0) <$> Gen.prim) + (Left <$> Gen.exhaustive 100) + (Right <$> Gen.exhaustive 100) + +prop_pair :: (forall a. Gen Bool -> Gen a -> Gen a -> Gen a) -> Property () +prop_pair if_ = + testShrinkingOfGen (P.relatedBy ("propEither", propEither)) $ + genPair if_ + +prop_pair_ifThenElse :: Property () +prop_pair_ifThenElse = + testShrinking (P.relatedBy ("stayRight", stayRight)) $ do + pair <- gen $ genPair ifBoth + when (prop pair) $ testFailed pair + where + prop :: (Word64, Either Word64 Word64) -> Bool + prop (x, Right y) = x < 10 || y > x + prop (x, Left y) = x < 1 || y < x + + -- Since we are generating the left value before the right value, if we + -- /start/ with a right value, we will then shrink the left value first even + -- though it is not used: indeed, this /must/ always succeed precisely + -- /because/ that left value is not used. At that point we can no longer + -- reduce the Right to a Left, because @Left 0@ is not a counterexample. + stayRight :: + (Word64, Either Word64 Word64) + -> (Word64, Either Word64 Word64) + -> Bool + stayRight _ (_, Left 0) = True -- Can always shrink to 'Minimal' + stayRight (_, Right _) (_, Left _) = False + stayRight _ _ = True + +{------------------------------------------------------------------------------- + Generic auxiliary +-------------------------------------------------------------------------------} + +ifM :: Gen Bool -> Gen a -> Gen a -> Gen a +ifM cond t f = cond `Gen.bindWithoutShortcut` \b -> if b then t else f + +ifBoth :: Gen Bool -> Gen a -> Gen a -> Gen a +ifBoth cond t f = + t `Gen.bindWithoutShortcut` \x -> + f `Gen.bindWithoutShortcut` \y -> + cond `Gen.bindWithoutShortcut` \b -> + return $ if b then x else y diff --git a/test/TestSuite/Prop/Generator/Shrinking.hs b/test/TestSuite/Prop/Generator/Shrinking.hs new file mode 100644 --- /dev/null +++ b/test/TestSuite/Prop/Generator/Shrinking.hs @@ -0,0 +1,132 @@ +module TestSuite.Prop.Generator.Shrinking (tests) where + +import Control.Monad +import Data.Default +import Data.Word +import Test.Tasty +import Test.Tasty.Falsify + +import qualified Test.QuickCheck as QuickCheck + +import qualified Test.Falsify.Generator as Gen +import qualified Test.Falsify.Predicate as P + +import TestSuite.Util.List + +tests :: TestTree +tests = testGroup "TestSuite.Prop.Generator.Shrinking" [ + testGroup "prim" [ + testPropertyWith expectFailure "prim" prop_prim_minimum + ] + , testGroup "shrinkTo" [ + testProperty "shrinking" prop_shrinkTo_shrinking + , testProperty "minimum" prop_shrinkTo_minimum + ] + , testGroup "firstThen" [ + testProperty "shrinking" prop_firstThen_shrinking + , testProperty "minimum" prop_firstThen_minimum + ] + , testGroup "shrinkWith" [ + testGroup "minimum" [ + testProperty "minimum" prop_shrinkWith_minimum_word + , testGroup "list" [ + testProperty (show i) $ prop_shrinkWith_minimum_list i + | i <- [20, 40, 60, 80, 100, 120, 140, 160, 180] + ] + ] + ] + ] + where + expectFailure :: TestOptions + expectFailure = def { + expectFailure = ExpectFailure + , overrideNumTests = Just 10_000 + } + +{------------------------------------------------------------------------------- + prim +-------------------------------------------------------------------------------} + +-- Binary search is not guaranteed to always find the minimum value. For +-- example, if we are looking for counter-examples to the property that "all +-- numbers are even", and we start with 3, then binary search will only try 0 +-- and 2, both of which are even, and hence conclude that 3 is the minimum +-- counter-example. This is true in QuickCheck, also. +prop_prim_minimum :: Property () +prop_prim_minimum = + testMinimum (P.expect 1) $ do + x <- gen Gen.prim + unless (even x) $ testFailed x + +{------------------------------------------------------------------------------- + shrinkTo +-------------------------------------------------------------------------------} + +prop_shrinkTo_shrinking :: Property () +prop_shrinkTo_shrinking = + testShrinkingOfGen (P.relatedBy ("validShrink", validShrink)) $ + Gen.shrinkToOneOf 3 [0 :: Word .. 2] + where + -- 'shrinkToOneOf' only shrinks /once/, so the original (pre-shrink) value + -- /must/ be 3. + validShrink :: Word -> Word -> Bool + validShrink 3 0 = True + validShrink 3 1 = True + validShrink 3 2 = True + validShrink _ _ = False + +prop_shrinkTo_minimum :: Property () +prop_shrinkTo_minimum = + testMinimum (P.expect 1) $ do + x <- gen $ Gen.shrinkToOneOf 3 [0 :: Word .. 2] + unless (even x) $ testFailed x + +{------------------------------------------------------------------------------- + firstThen +-------------------------------------------------------------------------------} + +prop_firstThen_shrinking :: Property () +prop_firstThen_shrinking = + testShrinkingOfGen (P.relatedBy ("validShrink", validShrink)) $ + Gen.firstThen True False + where + validShrink :: Bool -> Bool -> Bool + validShrink True False = True + validShrink _ _ = False + +prop_firstThen_minimum :: Property () +prop_firstThen_minimum = + testMinimum (P.expect False) $ do + x <- gen $ Gen.firstThen True False + testFailed x + +{------------------------------------------------------------------------------- + shrinkWith +-------------------------------------------------------------------------------} + +-- This is obviously not a valid general-purpose shrinking function for +-- 'Word64', but that is not important here. +shrinkWord :: Word64 -> [Word64] +shrinkWord n = takeWhile (< n) [0 .. 100] + +prop_shrinkWith_minimum_word :: Property () +prop_shrinkWith_minimum_word = + testMinimum (P.expect 1) $ do + x <- gen $ Gen.shrinkWith shrinkWord Gen.prim + unless (even x) $ testFailed x + +-- | Test performance of 'shrinkWith' +-- +-- We test this for lists of increasing size, to verify that this is not growing +-- exponentially with the size of the list (and thereby verifying that we are +-- not exploring the full shrink tree of those lists, because they certainly +-- /are/ exponential in size). +prop_shrinkWith_minimum_list :: Int -> Property () +prop_shrinkWith_minimum_list listLength = + testMinimum (P.expect [1,0]) $ do + xs <- gen $ Gen.shrinkWith (QuickCheck.shrinkList shrinkWord) $ + replicateM listLength Gen.prim + unless (pairwiseAll (<=) xs) $ testFailed xs + + + diff --git a/test/TestSuite/Prop/Generator/Simple.hs b/test/TestSuite/Prop/Generator/Simple.hs new file mode 100644 --- /dev/null +++ b/test/TestSuite/Prop/Generator/Simple.hs @@ -0,0 +1,174 @@ +module TestSuite.Prop.Generator.Simple (tests) where + +import Control.Monad (unless) +import Data.List (intercalate) +import Data.Word +import Test.Tasty +import Test.Tasty.Falsify + +import Test.Falsify.Predicate ((.$)) + +import qualified Test.Falsify.Generator as Gen +import qualified Test.Falsify.Predicate as P +import qualified Test.Falsify.Range as Range +import Data.Bits +import Data.Proxy +import Data.Typeable + +tests :: TestTree +tests = testGroup "TestSuite.Prop.Generator.Simple" [ + testGroup "prim" [ + testProperty "shrinking" prop_prim_shrinking + , testGroup "minimum" [ + testProperty (show target) $ prop_prim_minimum target + | target <- [0 .. 4] + ] + ] + , testGroup "bool" [ + testGroup "towardsFalse" [ + testProperty "shrinking" $ prop_bool_shrinking False + , testProperty "minimum" $ prop_bool_minimum False + ] + , testGroup "towardsTrue" [ + testProperty "shrinking" $ prop_bool_shrinking True + , testProperty "minimum" $ prop_bool_minimum True + ] + ] + , testGroup "int" [ + testGroup "between" [ + testGroup (intercalate "_" [show x, show y]) [ + testProperty "shrinking" $ prop_int_between_shrinking (x, y) + , testGroup "minimum" [ + testProperty (show target) $ + prop_int_between_minimum (x, y) target + | target <- [0, 1, 99, 100] + ] + ] + | (x, y) <- [ + ( 0, 0) + , ( 0, 10) + , ( 0, 100) + , ( 10, 0) + , ( 10, 10) + , ( 10, 100) + , (100, 0) + , (100, 10) + , (100, 100) + ] + ] + , let test_int_withOrigin :: forall a. + (Typeable a, Show a, Integral a, FiniteBits a) + => Proxy a -> TestTree + test_int_withOrigin p = testGroup (show $ typeRep p) [ + testGroup (intercalate "_" [show x, show y, show o]) [ + testProperty "shrinking" $ + prop_integral_withOrigin_shrinking @a (x, y) o + , testGroup "minimum" [ + testProperty (show target) $ + prop_integral_withOrigin_minimum (x, y) o target + | target <- [0, 1, 49, 50, 51, 99, 100] + ] + ] + | ((x, y), o) <- [ + ((0, 10), 0) + , ((0, 10), 10) + , ((0, 10), 5) + , ((0, 100), 0) + , ((0, 100), 100) + , ((0, 100), 50) + ] + ] + in testGroup "withOrigin" [ + test_int_withOrigin (Proxy @Int) + , test_int_withOrigin (Proxy @Word) + ] + ] + ] + + +{------------------------------------------------------------------------------- + Prim +-------------------------------------------------------------------------------} + +-- Gen.prime is the only generator where we a /strict/ inequality +prop_prim_shrinking :: Property () +prop_prim_shrinking = testShrinkingOfGen P.gt $ Gen.prim + +-- The minimum is always 0, unless 0 is not a counter-example +prop_prim_minimum :: Word64 -> Property () +prop_prim_minimum target = do + testMinimum (P.expect $ if target == 0 then 1 else 0) $ do + x <- gen $ Gen.prim + unless (x == target) $ testFailed x + +{------------------------------------------------------------------------------- + Bool +-------------------------------------------------------------------------------} + +prop_bool_shrinking :: Bool -> Property () +prop_bool_shrinking False = testShrinkingOfGen P.ge $ Gen.bool False +prop_bool_shrinking True = testShrinkingOfGen P.le $ Gen.bool True + +prop_bool_minimum :: Bool -> Property () +prop_bool_minimum target = + testMinimum (P.expect target) $ do + b <- gen $ Gen.bool target + testFailed b + +{------------------------------------------------------------------------------- + Range: 'between' + + This implicitly tests generation of fractions as well as determining + precision. +-------------------------------------------------------------------------------} + +prop_int_between_shrinking :: (Int, Int) -> Property () +prop_int_between_shrinking (x, y) + | x <= y = testShrinkingOfGen P.ge $ Gen.integral $ Range.between (x, y) + | otherwise = testShrinkingOfGen P.le $ Gen.integral $ Range.between (x, y) + +prop_int_between_minimum :: (Int, Int) -> Int -> Property () +prop_int_between_minimum (x, y) _target | x == y = + testMinimum (P.expect x) $ do + n <- gen $ Gen.integral $ Range.between (x, y) + -- The only value we can produce here is @x@, so no point looking for + -- anything these (that would just result in all tests being discarded) + testFailed n +prop_int_between_minimum (x, y) target = + testMinimum (P.expect expected) $ do + n <- gen $ Gen.integral $ Range.between (x, y) + unless (n == target) $ testFailed n + where + expected :: Int + expected + | x < y = if target == x then x + 1 else x + | otherwise = if target == x then x - 1 else x + +{------------------------------------------------------------------------------- + Range: 'withOrigin' +-------------------------------------------------------------------------------} + +prop_integral_withOrigin_shrinking :: + (Show a, Integral a, FiniteBits a) + => (a, a) -> a -> Property () +prop_integral_withOrigin_shrinking (x, y) o = + testShrinkingOfGen (P.towards o) $ + Gen.integral $ Range.withOrigin (x, y) o + +prop_integral_withOrigin_minimum :: forall a. + (Show a, Integral a, FiniteBits a) + => (a, a) -> a -> a -> Property () +prop_integral_withOrigin_minimum (x, y) o _target | x == y = + testMinimum (P.expect x) $ do + -- See discussion in 'prop_int_between_minimum' + n <- gen $ Gen.integral $ Range.withOrigin (x, y) o + testFailed n +prop_integral_withOrigin_minimum (x, y) o target = + testMinimum (P.elem .$ ("expected", expected)) $ do + n <- gen $ Gen.integral $ Range.withOrigin (x, y) o + unless (n == target) $ testFailed n + where + expected :: [a] + expected + | target == o = [o + 1, o - 1] + | otherwise = [o] diff --git a/test/TestSuite/Sanity/Predicate.hs b/test/TestSuite/Sanity/Predicate.hs new file mode 100644 --- /dev/null +++ b/test/TestSuite/Sanity/Predicate.hs @@ -0,0 +1,36 @@ +module TestSuite.Sanity.Predicate (tests) where + +import Test.Tasty +import Test.Tasty.HUnit +import Test.Falsify.Predicate (Predicate, (.$)) +import qualified Test.Falsify.Predicate as P +import Data.Char + +tests :: TestTree +tests = testGroup "TestSuite.Sanity.Predicate" [ + testCase "on" test_on + ] + +test_on :: Assertion +test_on = do + assertEqual "ok" (Right ()) $ P.eval $ p1 .$ ("x", 'a') .$ ("y", 'a') + assertEqual "err1" (Left err1) $ P.eval $ p1 .$ ("x", 'a') .$ ("y", 'b') + assertEqual "err2" (Left err2) $ P.eval $ p2 .$ ("x", 'a') .$ ("y", 'b') + where + p1, p2 :: Predicate '[Char, Char] + p1 = P.eq `P.on` P.fn ("ord", ord) + p2 = P.eq `P.on` P.transparent ord + + err1, err2 :: String + err1 = unlines [ + "(ord x) /= (ord y)" + , "x : 'a'" + , "y : 'b'" + , "ord x: 97" + , "ord y: 98" + ] + err2 = unlines [ + "x /= y" + , "x: 'a'" + , "y: 'b'" + ] diff --git a/test/TestSuite/Sanity/Range.hs b/test/TestSuite/Sanity/Range.hs new file mode 100644 --- /dev/null +++ b/test/TestSuite/Sanity/Range.hs @@ -0,0 +1,86 @@ +module TestSuite.Sanity.Range (tests) where + +import Control.Monad +import Data.Bifunctor +import Data.Map (Map) +import Data.Maybe (fromMaybe) +import Test.Tasty +import Test.Tasty.HUnit +import Text.Printf + +import qualified Data.Map as Map + +import Test.Falsify.Range (Range, Precision(..), ProperFraction(..)) + +import qualified Test.Falsify.Range as Range + +tests :: TestTree +tests = testGroup "TestSuite.Sanity.Range" [ + testGroup "between" [ + testCase (show size) $ test_between size + | size <- [2, 3, 4, 10, 100, 1000, 10_000] + ] + ] + +test_between :: Word -> Assertion +test_between size = do + assertEqual "domain" [0 .. size - 1] $ + map fst $ stats r + + forM_ (map snd $ stats r) $ \(Percentage pct _) -> + unless (abs (pct - expected) < tolerance) $ + assertFailure $ concat [ + "Percentage " + , show pct + , ". Expected " + , show expected + , " (tolerance " + , show tolerance + , ")" + ] + where + r :: Range Word + r = Range.between (0, size - 1) + + expected, tolerance :: Double + expected = 1 / fromIntegral size + tolerance = 0.01 + +{------------------------------------------------------------------------------- + Auxiliary +-------------------------------------------------------------------------------} + +data Percentage = Percentage Double Bool + +instance Show Percentage where + show (Percentage pct isZero) = + printf "%8.4f%% (%s)" pct (if isZero then "zero" else "non-zero") + +-- | Compute statistics about the given range +-- +-- Whenever the 'Range' asks for a fraction with a certain precision, we give +-- it /all/ possible fractions with that precision. We then count how often +-- each value in the range is produced. +stats :: forall a. (Ord a, Num a) => Range a -> [(a, Percentage)] +stats r = + count Map.empty $ Range.eval genFraction r + where + genFraction :: Precision -> [ProperFraction] + genFraction (Precision p) + | p >= 16 = error $ "stats: precision " ++ show p ++ " too high" + | otherwise = [ + ProperFraction $ fromIntegral x / fromIntegral ((2 :: Word) ^ p) + | x <- [0 .. (2 :: Word) ^ p - 1] + ] + + count :: Map a Word -> [a] -> [(a, Percentage)] + count acc (x:xs) = count (Map.alter (Just . (+1) . fromMaybe 0) x acc) xs + count acc [] = map (second asPct) $ Map.toList acc + where + total :: Word + total = sum $ Map.elems acc + + asPct :: Word -> Percentage + asPct c = Percentage (fromIntegral c / fromIntegral total) (c == 0) + + diff --git a/test/TestSuite/Sanity/Selective.hs b/test/TestSuite/Sanity/Selective.hs new file mode 100644 --- /dev/null +++ b/test/TestSuite/Sanity/Selective.hs @@ -0,0 +1,108 @@ +module TestSuite.Sanity.Selective (tests) where + +import Control.Selective +import Data.Word +import System.Timeout +import Test.Tasty +import Test.Tasty.HUnit + +import Test.Falsify.Generator (Gen, Tree(..)) +import Test.Falsify.Interactive (sample, shrink') + +import qualified Test.Falsify.Generator as Gen + +tests :: TestTree +tests = testGroup "TestSuite.Sanity.Selective" [ + testGroup "tree" [ + testCaseInfo "ifBoth" test_tree_ifBoth + , testGroup "ifS" [ + testCase "10" $ test_tree_ifS 10 + , testCase "20" $ test_tree_ifS 20 + , testCase "30" $ test_tree_ifS 30 + , testCase "40" $ test_tree_ifS 40 + , testCase "50" $ test_tree_ifS 50 + , testCase "60" $ test_tree_ifS 60 + , testCase "70" $ test_tree_ifS 70 + , testCase "80" $ test_tree_ifS 80 + , testCase "90" $ test_tree_ifS 90 + , testCase "100" $ test_tree_ifS 100 + ] + ] + ] + +{------------------------------------------------------------------------------- + Tree + + In this test we construct a "biased tree" (aka list) using a generator for a + /complete/ tree but then only using part of the result. Clearly, if we + /actually/ used the entire complete tree, this would have exponential + complexity, so that's not an option. + + The problem is not in /generation/, which is sufficiently lazy, but in + shrinking. With the monadic interface, there are two non-solutions: + + - With the shrinking shortcut in place (reducing entire prats of the tree + to 'Minimal'), then shrinking isn't all that interesting: the part of the + tree we're not using will be set to all zeroes immediately (this is what + the @either@ examples were demonstrating) + - Without the shrinking shortcut in place, the /generator/ might not look + at the full complete tree, but the /shrinker/ will, and so shrinking will + have abysmal performance. This is demonstrated in 'test_tree_ifBoth'. + + With the selective interface, however, everything works just fine. +-------------------------------------------------------------------------------} + +test_tree_ifBoth :: IO String +test_tree_ifBoth = do + let depth = 15 + -- Verify that we /don't/ get a timeout during generation + sampled <- sample (tree ifBoth depth) + assertBool "initial" $ isBiased sampled + -- But we /do/ get a timeout during shrinking + didTimeout <- timeout 10_000_000 $ do + Just history <- shrink' Just (tree ifBoth depth) + assertBool "shrunk" $ all isBiased history + return history + case didTimeout of + Nothing -> return "Timed out as expected" + Just history -> assertFailure $ unlines [ + "Expected timeout, but did not get it. " + , "Shrink history: " ++ show history + ] + +test_tree_ifS :: Word64 -> Assertion +test_tree_ifS depth = do + sampled <- sample (tree ifS depth) + assertBool "initial" $ isBiased sampled + Just shrunk <- shrink' Just (tree ifS depth) + assertBool "shrunk" $ all isBiased shrunk + +isBiased :: Tree a -> Bool +isBiased Leaf = True +isBiased (Branch _ Leaf t ) = isBiased t +isBiased (Branch _ t Leaf ) = isBiased t +isBiased (Branch _ Branch{} Branch{}) = False + +tree :: + (forall a. Gen Bool -> Gen a -> Gen a -> Gen a) + -> Word64 -> Gen (Tree Word64) +tree if_ = go + where + go :: Word64 -> Gen (Tree Word64) + go 0 = pure Leaf + go d = + Gen.prim `Gen.bindWithoutShortcut` \x -> + if_ ((== 0) <$> Gen.prim) + ((\t -> Branch x t Leaf) <$> go (d - 1)) + ((\t -> Branch x Leaf t) <$> go (d - 1)) + +{------------------------------------------------------------------------------- + Generic auxiliary +-------------------------------------------------------------------------------} + +ifBoth :: Gen Bool -> Gen a -> Gen a -> Gen a +ifBoth cond t f = + t `Gen.bindWithoutShortcut` \x -> + f `Gen.bindWithoutShortcut` \y -> + cond `Gen.bindWithoutShortcut` \b -> + return $ if b then x else y diff --git a/test/TestSuite/Util/List.hs b/test/TestSuite/Util/List.hs new file mode 100644 --- /dev/null +++ b/test/TestSuite/Util/List.hs @@ -0,0 +1,16 @@ +module TestSuite.Util.List ( + -- * Predicates + pairwiseAll + ) where + +{------------------------------------------------------------------------------- + Predicates +-------------------------------------------------------------------------------} + +pairwiseAll :: forall a. (a -> a -> Bool) -> [a] -> Bool +pairwiseAll p = go + where + go :: [a] -> Bool + go [] = True + go [_] = True + go (x:y:zs) = p x y && go (y:zs) diff --git a/test/TestSuite/Util/Tree.hs b/test/TestSuite/Util/Tree.hs new file mode 100644 --- /dev/null +++ b/test/TestSuite/Util/Tree.hs @@ -0,0 +1,83 @@ +module TestSuite.Util.Tree ( + -- * Stats + size + , weight + , height + -- * Balancing + , isWeightBalanced + , isHeightBalanced + ) where + +import Test.Falsify.Generator (Tree(..)) + +{------------------------------------------------------------------------------- + Tree stats +-------------------------------------------------------------------------------} + +-- | Size of the tree +size :: Tree a -> Word +size Leaf = 0 +size (Branch _ l r) = 1 + size l + size r + +-- | Weight of the tree +-- +-- The weight of a tree is simply its size plus one. +-- +-- @O(1)@ +weight :: Tree a -> Word +weight = succ . size + +-- | Height of the tree +-- +-- The height of a tree is the maximum length from the root to any of the leafs. +-- +-- @O(1)@ +height :: Tree a -> Word +height Leaf = 0 +height (Branch _ l r) = 1 + max (height l) (height r) + +{------------------------------------------------------------------------------- + Balancing +-------------------------------------------------------------------------------} + +-- | Check if the tree is weight-balanced +-- +-- A tree is weight-balanced if the weights of the subtrees does not differ +-- by more than a factor 3. +-- +-- See "Balancing weight-balanced trees", Hirai and Yamamoto, JFP 21(3), 2011. +isWeightBalanced :: Tree a -> Bool +isWeightBalanced = checkBalanceCondition isBalanced + where + delta :: Word + delta = 3 + + isBalanced :: Tree a -> Tree a -> Bool + isBalanced a b = and [ + delta * weight a >= weight b + , delta * weight b >= weight a + ] + +-- | Check if a tree is height-balanced +-- +-- A tree is height balanced if the heights of its subtrees do not differ +-- by more than one. +isHeightBalanced :: Tree a -> Bool +isHeightBalanced = checkBalanceCondition isBalanced + where + isBalanced :: Tree a -> Tree a -> Bool + isBalanced a b = or [ + (height a <= height b) && (height b - height a <= 1) + , (height b <= height a) && (height a - height b <= 1) + ] + +-- | Internal auxiliary: check given tree balance condition +-- +-- Property @p l r@ will be checked at every branch in the tree. +checkBalanceCondition :: forall a. (Tree a -> Tree a -> Bool) -> Tree a -> Bool +checkBalanceCondition p = go + where + go :: Tree a -> Bool + go Leaf = True + go (Branch _ l r) = and [p l r, go l, go r] +