diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,171 @@ +Changes +======= + +Version 1.2.1.1 +------------- + +* Annotate everything with `@since` pragmas. + +Version 1.2.1 +------------- + +* Add `Serial` and `CoSerial` instances for `Ordering`. + +Version 1.2.0 +------------- + +* Add `Serial` and `CoSerial` instances for + `(,,,,)`, `(,,,,,)`, + `Compose`, + `Foreign.C.Types`, + `Data.List.NonEmpty`, + `Void`, + `Complex`. +* Add `Bounded`, `Functor`, `Foldable` and `Traversable` instances + for `Positive` and `NonNegative` wrappers. +* Add `NonZero` wrapper for non-zero integers. +* Add `cons5`, `cons6`, `alts5`, `alts6`. + +Version 1.1.7 +------------- + +* Fix overlapping instances of `GSerial`. + +Version 1.1.6 +------------- + +* Mark modules as `Safe`, not just `Trustworthy`. + +Version 1.1.5 +------------- + +* Add `limit :: Monad m => Int -> Series m a -> Series m a` +* Add `genericSeries` and `genericCoseries`, so that you can use the generic + implementations more flexibly. Previously, the generic implementation was + only available as the default method for `series`/`coseries` but not as + standalone functions. + +Version 1.1.4 +------------- + +* Add instances for fixed-width Int and Word types (Int8, Word8 etc.) + +Version 1.1.3.1 +--------------- + +* Fix compatibility with GHC 7.8 and older + +Version 1.1.3 +------------- + +* Add `Serial` and `CoSerial` instances for `Word` and `Natural` + +Version 1.1.2 +------------- + +* Export the `test` function +* Add a `listSeries` function + +Version 1.1.1 +------------- + +Export some auxiliary functions from `T.S.Series`, and document how to express +`consN` and `altsN` for `N > 4`. + +Version 1.1.0.1 +--------------- + +Documentation fixes + +Version 1.1 +----------- + +* Add a `Serial` instance for `Ratio` +* Add the `NonEmpty` wrapper for lists +* Add `listM` (the monadic version of `list`) +* Add optional explanation for test outcomes + +Version 1.0.4 +------------- + +Fix compatibility with GHC 7.4.1 + +Version 1.0.3 +------------- + +Fix a bug where no test cases were generated for some functional types (#19). + +Version 1.0.2 +------------- + +Fix a bug in the generic instance + +Version 1.0.1 +------------- + +Make SmallCheck build with GHC 7.4 + +Version 1.0 +----------- + +This is a major incompatible release of SmallCheck. Virtually every function has +changed its name, type, semantics or module. So please carefully read the docs +when upgrading. + +For some highlights, see [this blog post](http://ro-che.info/articles/2013-02-19-smallcheck.html). + +Version 0.6.2 +----------- +* Derive Typeable Property instance +* Add smallCheckPure + +Version 0.6.1 +----------- + +* Documentation improvements +* Make the package build with GHC 7.4.1 + +Version 0.6 +----------- + +* Default Generic implementation of Serial instance (by Bas van Dijk) +* The code is split into modules +* Convert much of README into haddock documentation +* Many small API changes +* Remove impure Testable (IO a) instance + +Version 0.5 +----------- + +Make the package build with GHC 7.2. Some cosmetic changes. + +Version 0.4 +----------- + +The module SmallCheck is now Test.SmallCheck. Packaged with Cabal. + +Version 0.3 +----------- + +Existential quantifiers now have unique variants for which two witnesses +are reported when uniqueness fails. The over-generating coseries method +for functions of functional arguments has been replaced; now 'coseries' +and the 'alts' family take a series argument. Test counters are +now Integers, not Ints. Ord and Eq are now derived for the N types. +Examples extended. + +Version 0.2 +----------- + +The 'smallCheck' driver now takes an argument d and runs test series +at depths 0..d without interaction, stopping if any test fails. +The interactive variant is still available as 'smallCheckI'. All +Prelude numeric types now have Serial instances, including floating-point +types. Serial types Nat and Natural are also defined. Examples extended. + +Version 0.1 +----------- + +The differences from 0.0 are two fixes (space-fault, output buffering), +an 'unsafe' but sometimes useful Testable (IO a) instance and additional +examples. diff --git a/CHANGES.md b/CHANGES.md deleted file mode 100644 --- a/CHANGES.md +++ /dev/null @@ -1,58 +0,0 @@ -Changes -======= - -Version 0.6.2 ------------ -* Derive Typeable Property instance -* Add smallCheckPure - -Version 0.6.1 ------------ - -* Documentation improvements -* Make the package build with GHC 7.4.1 - -Version 0.6 ------------ - -* Default Generic implementation of Serial instance (by Bas van Dijk) -* The code is split into modules -* Convert much of README into haddock documentation -* Many small API changes -* Remove impure Testable (IO a) instance - -Version 0.5 ------------ - -Make the package build with GHC 7.2. Some cosmetic changes. - -Version 0.4 ------------ - -The module SmallCheck is now Test.SmallCheck. Packaged with Cabal. - -Version 0.3 ------------ - -Existential quantifiers now have unique variants for which two witnesses -are reported when uniqueness fails. The over-generating coseries method -for functions of functional arguments has been replaced; now 'coseries' -and the 'alts' family take a series argument. Test counters are -now Integers, not Ints. Ord and Eq are now derived for the N types. -Examples extended. - -Version 0.2 ------------ - -The 'smallCheck' driver now takes an argument d and runs test series -at depths 0..d without interaction, stopping if any test fails. -The interactive variant is still available as 'smallCheckI'. All -Prelude numeric types now have Serial instances, including floating-point -types. Serial types Nat and Natural are also defined. Examples extended. - -Version 0.1 ------------ - -The differences from 0.0 are two fixes (space-fault, output buffering), -an 'unsafe' but sometimes useful Testable (IO a) instance and additional -examples. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,6 +1,10 @@ SmallCheck: a property-based testing library for Haskell ======================================================== +**As of 2023, this library is largely obsolete: arbitrary test generators +with shrinking such as [`falsify`](https://hackage.haskell.org/package/falsify) +offer much better user experience.** + SmallCheck is a testing library that allows to verify properties for all test cases up to some depth. The test cases are generated automatically by SmallCheck. @@ -10,23 +14,9 @@ > If a program fails to meet its specification in some cases, it almost always > fails in some simple case. -To get started with SmallCheck: +In many ways SmallCheck is very similar to QuickCheck. It uses the idea of type-based generators for test data, and the way testable properties are expressed is closely based on the QuickCheck approach. Like QuickCheck, SmallCheck tests whether properties hold for finite completely defined values at specific types, and reports counter-examples. -* Read the [documentation][haddock] -* Look at some [examples][examples] -* If you have experience with QuickCheck, [read the comparison of QuickCheck and SmallCheck][comparison] -* Install it and give it a try! - `cabal update; cabal install smallcheck` -* Read the [paper][paper] or [other materials][oldpage] from the original - authors of SmallCheck (note that that information might be somewhat outdated) -* If you see something that can be improved, please [submit an issue][issues] -* Check out [the source code][github] at GitHub +The big difference is that instead of using a sample of randomly generated values, SmallCheck tests properties for all the finitely many values up to some depth, progressively increasing the depth used. For data values, depth means depth of construction. For functional values, it is a measure combining the depth to which arguments may be evaluated and the depth of possible results. -[haddock]: http://hackage.haskell.org/packages/archive/smallcheck/latest/doc/html/Test-SmallCheck.html -[hackage]: http://hackage.haskell.org/package/smallcheck -[examples]: https://github.com/feuerbach/smallcheck/tree/master/examples -[paper]: http://www.cs.york.ac.uk/fp/smallcheck/smallcheck.pdf -[oldpage]: http://www.cs.york.ac.uk/fp/smallcheck/ -[comparison]: https://github.com/feuerbach/smallcheck/wiki/Comparison-with-QuickCheck -[github]: https://github.com/feuerbach/smallcheck -[issues]: https://github.com/feuerbach/smallcheck/issues +The package is based on the [paper](http://www.cs.york.ac.uk/fp/smallcheck/smallcheck.pdf) +by Colin Runciman, Matthew Naylor and Fredrik Lindblad. diff --git a/Test/SmallCheck.hs b/Test/SmallCheck.hs --- a/Test/SmallCheck.hs +++ b/Test/SmallCheck.hs @@ -7,65 +7,109 @@ -- -- This module exports the main pieces of SmallCheck functionality. -- +-- To generate test cases for your own types, refer to +-- "Test.SmallCheck.Series". +-- -- For pointers to other sources of information about SmallCheck, please refer -- to the README at --- +-- -------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} +{-# LANGUAGE NoImplicitPrelude #-} +#if __GLASGOW_HASKELL__ >= 704 +{-# LANGUAGE Safe #-} +#endif + module Test.SmallCheck ( -- * Constructing tests -- | The simplest kind of test is a function (possibly of many - -- arguments) returning 'Bool'. + -- arguments) returning 'Data.Bool.Bool'. The function arguments are interpreted + -- as being universally, existentially or uniquely quantified, depending + -- on the quantification context. -- - -- In addition, you can use the combinators shown below. For more - -- advanced combinators, see "Test.SmallCheck.Property". - - Testable, - Property, - property, + -- The default quantification context is universal ('forAll'). + -- + -- 'forAll', 'exists' and 'existsUnique' functions set the quantification + -- context for function arguments. Depending on the quantification + -- context, the test @\\x y -> p x y@ may be equivalent to: + -- + -- * \( \forall x, y\colon p\, x \, y \) ('forAll'), + -- + -- * \( \exists x, y\colon p\, x \, y \) ('exists'), + -- + -- * \( \exists! x, y\colon p\, x \, y \) ('existsUnique'). + -- + -- The quantification context affects all the variables immediately + -- following the quantification operator, also extending past 'over', + -- 'changeDepth' and 'changeDepth1' functions. + -- + -- However, it doesn't extend past other functions, like 'monadic', and + -- doesn't affect the operands of '==>'. Such functions start a fresh + -- default quantification context. - -- ** Existential quantification + -- ** Examples - -- | Suppose we have defined a function + -- | + -- * @\\x y -> p x y@ means + -- \( \forall x, y\colon p\, x \, y \). -- - -- >isPrefix :: Eq a => [a] -> [a] -> Bool + -- * @'exists' $ \\x y -> p x y@ means + -- \( \exists x, y\colon p\, x \, y \). -- - -- and wish to specify it by some suitable property. We might define + -- * @'exists' $ \\x -> 'forAll' $ \\y -> p x y@ means + -- \( \exists x\colon \forall y\colon p \, x \, y \). -- - -- >prop_isPrefix1 :: String -> String -> Bool - -- >prop_isPrefix1 xs ys = isPrefix xs (xs++ys) + -- * @'existsUnique' $ \\x y -> p x y@ means + -- \( \exists! x, y\colon p\, x \, y \). -- - -- where @xs@ and @ys@ are universally quantified. This property is necessary - -- but not sufficient for a correct @isPrefix@. For example, it is satisfied - -- by the function that always returns @True@! + -- * @'existsUnique' $ \\x -> 'over' s $ \\y -> p x y@ means + -- \( \exists! x, y \colon y \in s \wedge p \, x \, y \). -- - -- We can also test the following property, which involves an existentially - -- quantified variable: + -- * @'existsUnique' $ \\x -> 'monadic' $ \\y -> p x y@ means + -- \( \exists! x \colon \forall y \colon [p \, x \, y] \). -- - -- >prop_isPrefix2 :: String -> String -> Property - -- >prop_isPrefix2 xs ys = isPrefix xs ys ==> exists $ \xs' -> ys == xs++xs' + -- * @'existsUnique' $ \\x -> 'existsUnique' $ \\y -> p x y@ means + -- \( \exists! x \colon \exists! y \colon p \, x \, y \). + -- + -- * @'exists' $ \\x -> (\\y -> p y) '==>' (\\z -> q z)@ means + -- \( \exists x \colon (\forall y\colon p\, y) \implies (\forall z\colon q\, z) \). + forAll, exists, - exists1, - existsDeeperBy, - exists1DeeperBy, + existsUnique, + over, + monadic, - -- ** Conditioning (==>), + changeDepth, + changeDepth1, -- * Running tests - -- | The functions below can be used to run SmallCheck tests. + -- | 'smallCheck' is a simple way to run a test. -- - -- As an alternative, consider using @test-framework@ package. + -- As an alternative, consider using a testing framework. -- - -- It allows to organize SmallCheck properties into a test suite (possibly - -- together with HUnit or QuickCheck tests), apply timeouts, get nice - -- statistics etc. + -- The packages + -- and + -- + -- provide integration with Tasty and HSpec, two popular testing + -- frameworks. -- - -- To use SmallCheck properties with test-framework, install - -- @test-framework-smallcheck@ package. - smallCheck, depthCheck, smallCheckI, - Depth + -- They allow to organize SmallCheck properties into a test suite (possibly + -- together with HUnit or QuickCheck tests) and provide other useful + -- features. + -- + -- For more ways to run the tests, see "Test.SmallCheck.Drivers". + Depth, + smallCheck, + + -- * Main types and classes + Testable(..), + Property, + Reason + ) where import Test.SmallCheck.Property diff --git a/Test/SmallCheck/Drivers.hs b/Test/SmallCheck/Drivers.hs --- a/Test/SmallCheck/Drivers.hs +++ b/Test/SmallCheck/Drivers.hs @@ -5,103 +5,93 @@ -- License : BSD3 -- Maintainer: Roman Cheplyaka -- --- Functions to run SmallCheck tests. +-- You should only need this module if you wish to create your own way to +-- run SmallCheck tests -------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NoImplicitPrelude #-} +#if __GLASGOW_HASKELL__ >= 704 +{-# LANGUAGE Safe #-} +#endif + module Test.SmallCheck.Drivers ( - smallCheck, smallCheckI, depthCheck, smallCheckPure + smallCheck, smallCheckM, smallCheckWithHook, + test, + ppFailure, + PropertyFailure(..), PropertySuccess(..), Argument, Reason, TestQuality(..) ) where -import System.IO (stdout, hFlush) -import Control.Monad (when) +import Control.Monad (when, return) +import Data.Function (($), (.), const) +import Data.IORef (readIORef, writeIORef, IORef, newIORef) -- NB: explicit import list to avoid name clash with modifyIORef' +import Data.Maybe (Maybe(Nothing, Just)) +import Data.Ord ((>)) +import Prelude (Integer, (+), seq) +import System.IO (IO, putStrLn) import Test.SmallCheck.Property +import Test.SmallCheck.Property.Result +import Text.Printf (printf) --- | Run series of tests using depth bounds 0..d, stopping if any test fails, --- and print a summary report or a counter-example. -smallCheck :: Testable a => Depth -> a -> IO () -smallCheck d = iterCheck 0 (Just d) +-- | A simple driver that runs the test in the 'IO' monad and prints the +-- results. +-- +-- @since 1.0 +smallCheck :: Testable IO a => Depth -> a -> IO () +smallCheck d a = do + ((good, bad), mbEx) <- runTestWithStats d a + let testsRun = good + bad + case mbEx of + Nothing -> do + printf "Completed %d tests without failure.\n" testsRun + when (bad > 0) $ + printf "But %d did not meet ==> condition.\n" bad + Just x -> do + printf "Failed test no. %d.\n" testsRun + putStrLn $ ppFailure x --- | Same as 'smallCheck', but test for values of depth d only -depthCheck :: Testable a => Depth -> a -> IO () -depthCheck d = iterCheck d (Just d) +runTestWithStats :: Testable IO a => Depth -> a -> IO ((Integer, Integer), Maybe PropertyFailure) +runTestWithStats d prop = do + good <- newIORef 0 + bad <- newIORef 0 --- | Interactive variant, asking the user whether testing should --- continue\/go deeper after a failure\/completed iteration. --- --- Example session: --- --- >haskell> smallCheckI prop_append1 --- >Depth 0: --- > Completed 1 test(s) without failure. --- > Deeper? y --- >Depth 1: --- > Failed test no. 5. Test values follow. --- > [True] --- > [True] --- > Continue? n --- > Deeper? n --- >haskell> -smallCheckI :: Testable a => a -> IO () -smallCheckI = iterCheck 0 Nothing + let + hook GoodTest = modifyIORef' good (+1) + hook BadTest = modifyIORef' bad (+1) -iterCheck :: Testable a => Depth -> Maybe Depth -> a -> IO () -iterCheck dFrom mdTo t = iter dFrom - where - iter d = do - putStrLn ("Depth "++show d++":") - let results = test t d - ok <- check (mdTo==Nothing) 0 0 True results - maybe (whenUserWishes " Deeper" () $ iter (d+1)) - (\dTo -> when (ok && d < dTo) $ iter (d+1)) - mdTo + r <- smallCheckWithHook d hook prop -check :: Bool -> Integer -> Integer -> Bool -> [TestCase] -> IO Bool -check i n x ok rs | null rs = do - putStr (" Completed "++show n++" test(s)") - putStrLn (if ok then " without failure." else ".") - when (x > 0) $ - putStrLn (" But "++show x++" did not meet ==> condition.") - return ok -check i n x ok (TestCase Inappropriate _ : rs) = do - progressReport i n x - check i (n+1) (x+1) ok rs -check i n x f (TestCase Pass _ : rs) = do - progressReport i n x - check i (n+1) x f rs -check i n x f (TestCase Fail args : rs) = do - putStrLn (" Failed test no. "++show (n+1)++". Test values follow.") - mapM_ (putStrLn . (" "++)) args - ( if i then - whenUserWishes " Continue" False $ check i (n+1) x False rs - else - return False ) + goodN <- readIORef good + badN <- readIORef bad -whenUserWishes :: String -> a -> IO a -> IO a -whenUserWishes wish x action = do - putStr (wish++"? ") - hFlush stdout - reply <- getLine - ( if (null reply || reply=="y") then action - else return x ) + return ((goodN, badN), r) -progressReport :: Bool -> Integer -> Integer -> IO () -progressReport i n x | n >= x = do - when i $ ( putStr (n' ++ replicate (length n') '\b') >> - hFlush stdout ) - where - n' = show n +-- NB: modifyIORef' is in base starting at least from GHC 7.6.1. +-- +-- So get rid of this once 7.6.1 becomes widely adopted. +modifyIORef' :: IORef a -> (a -> a) -> IO () +modifyIORef' ref f = do + x <- readIORef ref + let x' = f x + x' `seq` writeIORef ref x' --- | A pure analog of 'smallCheck'. +-- | Use this if: -- --- If a counterexample is found, it is returned. +-- * You need to run a test in a monad different from 'IO' -- --- Otherwise, a tuple of two numbers is returned, where the first number is the --- number of all test cases, and the second number is the number of test cases --- that did not satisfy the precondition. -smallCheckPure :: Testable a => Depth -> a -> Either [String] (Integer, Integer) -smallCheckPure d a = (foldr step Right $ concatMap (test a) [0..d]) (0,0) - where - step testRes rest (n, x) = n `seq` x `seq` - case result testRes of - Fail -> Left $ arguments testRes - Pass -> rest (n+1, x) - Inappropriate -> rest (n+1, x+1) +-- * You need to analyse the results rather than just print them +-- +-- @since 1.0 +smallCheckM :: Testable m a => Depth -> a -> m (Maybe PropertyFailure) +smallCheckM d = smallCheckWithHook d (const $ return ()) + +-- | Like `smallCheckM`, but allows to specify a monadic hook that gets +-- executed after each test is run. +-- +-- Useful for applications that want to report progress information to the +-- user. +-- +-- @since 1.0 +smallCheckWithHook :: Testable m a => Depth -> (TestQuality -> m ()) -> a -> m (Maybe PropertyFailure) +smallCheckWithHook d hook a = runProperty d hook $ test a diff --git a/Test/SmallCheck/Property.hs b/Test/SmallCheck/Property.hs --- a/Test/SmallCheck/Property.hs +++ b/Test/SmallCheck/Property.hs @@ -1,3 +1,5 @@ +-- vim:fdm=marker:foldtext=foldtext() + -------------------------------------------------------------------- -- | -- Module : Test.SmallCheck.Property @@ -7,173 +9,421 @@ -- -- Properties and tools to construct them. -------------------------------------------------------------------- -{-# LANGUAGE DeriveDataTypeable #-} + +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +-- Are we using new, polykinded and derivable Typeable yet? +#define NEWTYPEABLE MIN_VERSION_base(4,7,0) + +#if NEWTYPEABLE +{-# LANGUAGE Safe #-} +#else +-- Trustworthy is needed because of the hand-written Typeable instance +#if __GLASGOW_HASKELL__ >= 704 +{-# LANGUAGE Trustworthy #-} +#endif +#endif + module Test.SmallCheck.Property ( - -- * Basic definitions - TestCase(..), - TestResult(..), - resultIsOk, + -- * Constructors + forAll, exists, existsUnique, over, (==>), monadic, changeDepth, changeDepth1, - Property, Depth, Testable(..), - property, mkProperty, + -- * Property's entrails + Property, - -- * Constructing tests - (==>), exists, existsDeeperBy, exists1, exists1DeeperBy, - -- ** Series- and list-based constructors - -- | Combinators below can be used to explicitly specify the domain of - -- quantification (as 'Series' or lists). - -- - -- Hopefully, their meaning is evident from their names and types. - forAll, forAllElem, - thereExists, thereExistsElem, - thereExists1, thereExists1Elem + PropertySuccess(..), PropertyFailure(..), runProperty, TestQuality(..), Argument, Reason, Depth, Testable(..), ) where +import Control.Applicative (pure, (<$>), (<$)) +import Control.Arrow (first) +import Control.Monad (Monad, liftM, mzero, return, (=<<), (>>=)) +import Control.Monad.Logic (MonadLogic, runLogicT, ifte, once, msplit, lnot) +import Control.Monad.Reader (Reader, runReader, lift, ask, local, reader) +import Data.Bool (Bool, otherwise) +import Data.Either (Either, either) +import Data.Eq (Eq) +import Data.Function (($), flip, (.), const, id) +import Data.Functor (fmap) +import Data.Int (Int) +import Data.Maybe (Maybe (Nothing, Just)) +import Data.Ord (Ord, (<=)) +import Data.Typeable (Typeable) +import Prelude (Enum, (-)) +import Test.SmallCheck.Property.Result import Test.SmallCheck.Series -import Data.Typeable +import Test.SmallCheck.SeriesMonad +import Text.Show (Show, show) -data TestResult - = Pass - | Fail - | Inappropriate - -- ^ 'Inappropriate' means that the precondition of '==>' - -- was not satisfied -data TestCase = TestCase { result :: TestResult, arguments :: [String] } +#if MIN_VERSION_base(4,17,0) +import Data.Type.Equality (type (~)) +#endif --- | Wrapper type for 'Testable's -newtype Property = Property (Depth -> [TestCase]) - deriving Typeable +#if !NEWTYPEABLE +import Data.Typeable (Typeable1, mkTyConApp, typeOf) +import Prelude (undefined) +#if MIN_VERSION_base(4,4,0) +import Data.Typeable (mkTyCon3) +#else +import Data.Typeable (mkTyCon) +#endif +#endif --- | Wrap a 'Testable' into a 'Property' -property :: Testable a => a -> Property -property = Property . test +------------------------------ +-- Property-related types +------------------------------ +--{{{ --- | A lower-level way to create properties. Use 'property' if possible. +-- | The type of properties over the monad @m@. -- --- The argument is a function that produces the list of results given the depth --- of testing. -mkProperty :: (Depth -> [TestCase]) -> Property -mkProperty = Property +-- @since 1.0 +newtype Property m = Property { unProperty :: Reader (Env m) (PropertySeries m) } +#if NEWTYPEABLE + deriving Typeable +#endif --- | Anything of a 'Testable' type can be regarded as a \"test\" -class Testable a where - test :: a -> Depth -> [TestCase] +data PropertySeries m = + PropertySeries + { searchExamples :: Series m PropertySuccess + , searchCounterExamples :: Series m PropertyFailure + , searchClosest :: Series m (Property m, [Argument]) + } -instance Testable Bool where - test b _ = [TestCase (boolToResult b) []] +data Env m = + Env + { quantification :: Quantification + , testHook :: TestQuality -> m () + } -instance (Serial a, Show a, Testable b) => Testable (a->b) where - test f = f' where Property f' = forAll series f +data Quantification + = Forall + | Exists + | ExistsUnique -instance Testable Property where - test (Property f) d = f d +-- | @since 1.0 +data TestQuality + = GoodTest + | BadTest + deriving (Eq, Ord, Enum, Show) -forAll :: (Show a, Testable b) => Series a -> (a->b) -> Property -forAll xs f = Property $ \d -> - [ r{arguments = show x : arguments r} - | x <- xs d, r <- test (f x) d ] +#if !NEWTYPEABLE +-- Typeable here is not polykinded yet, and also GHC doesn't know how to +-- derive this. +instance Typeable1 m => Typeable (Property m) + where + typeOf _ = + mkTyConApp +#if MIN_VERSION_base(4,4,0) + (mkTyCon3 "smallcheck" "Test.SmallCheck.Property" "Property") +#else + (mkTyCon "smallcheck Test.SmallCheck.Property Property") +#endif + [typeOf (undefined :: m ())] +#endif -forAllElem :: (Show a, Testable b) => [a] -> (a->b) -> Property -forAllElem xs = forAll (const xs) +-- }}} -existence :: (Show a, Testable b) => Bool -> Series a -> (a->b) -> Property -existence u xs f = Property existenceDepth - where - existenceDepth d = [ TestCase (boolToResult valid) arguments ] - where - witnesses = [ show x | x <- xs d, all (resultIsOk . result) (test (f x) d) ] - valid = enough witnesses - enough = if u then unique else (not . null) - arguments = if valid then [] - else if null witnesses then ["non-existence"] - else "non-uniqueness" : take 2 witnesses +------------------------------------ +-- Property runners and constructors +------------------------------------ +--{{{ -unique :: [a] -> Bool -unique [_] = True -unique _ = False +unProp :: Env t -> Property t -> PropertySeries t +unProp q (Property p) = runReader p q --- | Return 'False' iff the result is 'Fail' -resultIsOk :: TestResult -> Bool -resultIsOk r = - case r of - Fail -> False - Pass -> True - Inappropriate -> True +runProperty + :: Monad m + => Depth + -> (TestQuality -> m ()) + -> Property m + -> m (Maybe PropertyFailure) +runProperty depth hook prop = + (\l -> runLogicT l (\x _ -> return $ Just x) (return Nothing)) $ + runSeries depth $ + searchCounterExamples $ + flip runReader (Env Forall hook) $ + unProperty prop -boolToResult :: Bool -> TestResult -boolToResult b = if b then Pass else Fail +atomicProperty :: Series m PropertySuccess -> Series m PropertyFailure -> PropertySeries m +atomicProperty s f = + let prop = PropertySeries s f (pure (Property $ pure prop, [])) + in prop -thereExists :: (Show a, Testable b) => Series a -> (a->b) -> Property -thereExists = existence False +makeAtomic :: Property m -> Property m +makeAtomic (Property prop) = + Property $ flip fmap prop $ \ps -> + atomicProperty (searchExamples ps) (searchCounterExamples ps) -thereExists1 :: (Show a, Testable b) => Series a -> (a->b) -> Property -thereExists1 = existence True +-- | @'over' s $ \\x -> p x@ makes @x@ range over the 'Series' @s@ (by +-- default, all variables range over the 'series' for their types). +-- +-- Note that, unlike the quantification operators, this affects only the +-- variable following the operator and not subsequent variables. +-- +-- 'over' does not affect the quantification context. +-- +-- @since 1.0 +over + :: (Show a, Testable m b) + => Series m a -> (a -> b) -> Property m +over = testFunction -thereExistsElem :: (Show a, Testable b) => [a] -> (a->b) -> Property -thereExistsElem xs = thereExists (const xs) +-- | Execute a monadic test. +-- +-- @since 1.0 +monadic :: Testable m a => m a -> Property m +monadic a = + Property $ reader $ \env -> -thereExists1Elem :: (Show a, Testable b) => [a] -> (a->b) -> Property -thereExists1Elem xs = thereExists1 (const xs) + let pair = unProp env . freshContext <$> lift a in --- | @'exists' p@ holds iff it is possible to find an argument @a@ (within the --- depth constraints!) satisfying the predicate @p@ -exists :: (Show a, Serial a, Testable b) => (a->b) -> Property -exists = thereExists series + atomicProperty + (searchExamples =<< pair) + (searchCounterExamples =<< pair) --- | Like 'exists', but additionally require the uniqueness of the --- argument satisfying the predicate -exists1 :: (Show a, Serial a, Testable b) => (a->b) -> Property -exists1 = thereExists1 series +-- }}} --- | The default testing of existentials is bounded by the same depth as their --- context. This rule has important consequences. Just as a universal property --- may be satisfied when the depth bound is shallow but fail when it is deeper, --- so the reverse may be true for an existential property. So when testing --- properties involving existentials it may be appropriate to try deeper testing --- after a shallow failure. However, sometimes the default same-depth-bound --- interpretation of existential properties can make testing of a valid property --- fail at all depths. Here is a contrived but illustrative example: +------------------------------- +-- Testable class and instances +------------------------------- +-- {{{ + +-- | Class of tests that can be run in a monad. For pure tests, it is +-- recommended to keep their types polymorphic in @m@ rather than +-- specialising it to 'Data.Functor.Identity'. -- --- >prop_append1 :: [Bool] -> [Bool] -> Property --- >prop_append1 xs ys = exists $ \zs -> zs == xs++ys +-- @since 1.0 +class Monad m => Testable m a where + -- | @since 1.0 + test :: a -> Property m + +instance Monad m => Testable m Bool where + test b = Property $ reader $ \env -> + let + success = do + lift $ testHook env GoodTest + if b then return $ PropertyTrue Nothing else mzero + failure = PropertyFalse Nothing <$ lnot success + in atomicProperty success failure + +-- | Works like the 'Data.Bool.Bool' instance, but includes an explanation of the result. -- --- 'existsDeeperBy' transforms the depth bound by a given @'Depth' -> 'Depth'@ function: +-- 'Data.Either.Left' and 'Data.Either.Right' correspond to test failure and success +-- respectively. -- --- >prop_append2 :: [Bool] -> [Bool] -> Property --- >prop_append2 xs ys = existsDeeperBy (*2) $ \zs -> zs == xs++ys -existsDeeperBy :: (Show a, Serial a, Testable b) => (Depth->Depth) -> (a->b) -> Property -existsDeeperBy f = thereExists (series . f) +-- @since 1.1 +instance Monad m => Testable m (Either Reason Reason) where + test r = Property $ reader $ \env -> + let + success = do + lift $ testHook env GoodTest + either (const mzero) (pure . PropertyTrue . Just) r + failure = do + lift $ testHook env GoodTest + either (pure . PropertyFalse . Just) (const mzero) r + in atomicProperty success failure --- | Like 'existsDeeperBy', but additionally require the uniqueness of the --- argument satisfying the predicate -exists1DeeperBy :: (Show a, Serial a, Testable b) => (Depth->Depth) -> (a->b) -> Property -exists1DeeperBy f = thereExists1 (series . f) +instance (Serial m a, Show a, Testable m b) => Testable m (a->b) where + test = testFunction series -infixr 0 ==> +instance (Monad m, m ~ n) => Testable n (Property m) where + test = id --- | The '==>' operator can be used to express a --- restricting condition under which a property should hold. For example, --- testing a propositional-logic module (see examples/logical), we might --- define: +testFunction + :: (Show a, Testable m b) + => Series m a -> (a -> b) -> Property m +testFunction s f = Property $ reader $ \env -> + let + closest = do + x <- s + (p, args) <- searchClosest $ unProp env $ test $ f x + return (p, show x : args) + in + + case quantification env of + Forall -> PropertySeries success failure closest + -- {{{ + where + failure = do + x <- s + failure <- searchCounterExamples $ unProp env $ test $ f x + let arg = show x + return $ + case failure of + CounterExample args etc -> CounterExample (arg:args) etc + _ -> CounterExample [arg] failure + + success = PropertyTrue Nothing <$ lnot failure + -- }}} + + Exists -> PropertySeries success failure closest + -- {{{ + where + success = do + x <- s + s <- searchExamples $ unProp env $ test $ f x + let arg = show x + + return $ + case s of + Exist args etc -> Exist (arg:args) etc + _ -> Exist [arg] s + + failure = NotExist <$ lnot success + -- }}} + + ExistsUnique -> PropertySeries success failure closest + -- {{{ + where + search = atMost 2 $ do + (prop, args) <- closest + ex <- once $ searchExamples $ unProp env $ test prop + return (args, ex) + + success = + search >>= + \examples -> + case examples of + [(x,s)] -> return $ ExistUnique x s + _ -> mzero + + failure = + search >>= + \examples -> + case examples of + [] -> return NotExist + (x1,s1):(x2,s2):_ -> return $ AtLeastTwo x1 s1 x2 s2 + _ -> mzero + -- }}} + +atMost :: MonadLogic m => Int -> m a -> m [a] +atMost n m + | n <= 0 = return [] + | otherwise = do + m' <- msplit m + case m' of + Nothing -> return [] + Just (x,rest) -> + (x:) `liftM` atMost (n-1) rest + +-- }}} + +------------------------------ +-- Test constructors +------------------------------ +-- {{{ + +quantify :: Quantification -> Property m -> Property m +quantify q (Property a) = + makeAtomic $ Property $ local (\env -> env { quantification = q }) a + +freshContext :: Testable m a => a -> Property m +freshContext = forAll + +-- | Set the universal quantification context. -- --- >prop_tautEval :: Proposition -> Environment -> Property --- >prop_tautEval p e = --- > tautology p ==> eval p e +-- @since 1.0 +forAll :: Testable m a => a -> Property m +forAll = quantify Forall . test + +-- | Set the existential quantification context. -- --- But here is an alternative definition: +-- @since 1.0 +exists :: Testable m a => a -> Property m +exists = quantify Exists . test + +-- | Set the uniqueness quantification context. -- --- >prop_tautEval :: Proposition -> Property --- >prop_taut p = --- > tautology p ==> \e -> eval p e +-- Bear in mind that \( \exists! x, y\colon p\, x \, y \) +-- is not the same as \( \exists! x \colon \exists! y \colon p \, x \, y \). -- --- The first definition generates p and e for each test, whereas the --- second only generates e if the tautology p holds. +-- For example, \( \exists! x \colon \exists! y \colon |x| = |y| \) +-- is true (it holds only when \(x=y=0\)), +-- but \( \exists! x, y \colon |x| = |y| \) is false +-- (there are many such pairs). -- --- The second definition is far better as the test-space is --- reduced from PE to T'+TE where P, T, T' and E are the numbers of --- propositions, tautologies, non-tautologies and environments. -(==>) :: Testable a => Bool -> a -> Property -True ==> x = Property (test x) -False ==> x = Property (const [nothing]) - where - nothing = TestCase { result = Inappropriate, arguments = [] } +-- As is customary in mathematics, +-- @'existsUnique' $ \\x y -> p x y@ is equivalent to +-- @'existsUnique' $ \\(x, y) -> p x y@ and not to +-- @'existsUnique' $ \\x -> 'existsUnique' $ \\y -> p x y@ +-- (the latter, of course, may be explicitly written when desired). +-- +-- That is, all the variables affected by the same uniqueness context are +-- quantified simultaneously as a tuple. +-- +-- @since 1.0 +existsUnique :: Testable m a => a -> Property m +existsUnique = quantify ExistsUnique . test + +-- | The '==>' operator can be used to express a restricting condition +-- under which a property should hold. It corresponds to implication in the +-- classical logic. +-- +-- Note that '==>' resets the quantification context for its operands to +-- the default (universal). +-- +-- @since 1.0 +infixr 0 ==> +(==>) :: (Testable m c, Testable m a) => c -> a -> Property m +cond ==> prop = Property $ do + env <- ask + + let + counterExample = once $ searchCounterExamples $ unProp env' $ freshContext cond + -- NB: we do not invoke the test hook in the antecedent + where env' = env { testHook = const $ return () } + + consequent = unProp env $ freshContext prop + + badTestHook = lift $ testHook env BadTest + + success = + ifte counterExample + -- then + (\ex -> do + badTestHook + return $ Vacuously ex + ) + -- else + (searchExamples consequent) + + failure = + ifte counterExample + -- then + (const $ do + lift $ testHook env BadTest + mzero + ) + -- else + (searchCounterExamples consequent) + + return $ atomicProperty success failure + +-- | Run property with a modified depth. Affects all quantified variables +-- in the property. +-- +-- @since 1.0 +changeDepth :: Testable m a => (Depth -> Depth) -> a -> Property m +changeDepth modifyDepth a = Property (changeDepthPS <$> unProperty (test a)) + where + changeDepthPS (PropertySeries ss sf sc) = + PropertySeries + (localDepth modifyDepth ss) + (localDepth modifyDepth sf) + (first (changeDepth modifyDepth) <$> + localDepth modifyDepth sc) + +-- | Quantify the function's argument over its 'series', but adjust the +-- depth. This doesn't affect any subsequent variables. +-- +-- @since 1.0 +changeDepth1 :: (Show a, Serial m a, Testable m b) => (Depth -> Depth) -> (a -> b) -> Property m +changeDepth1 modifyDepth = over $ localDepth modifyDepth series + +-- }}} diff --git a/Test/SmallCheck/Property/Result.hs b/Test/SmallCheck/Property/Result.hs new file mode 100644 --- /dev/null +++ b/Test/SmallCheck/Property/Result.hs @@ -0,0 +1,104 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE NoImplicitPrelude #-} +#if __GLASGOW_HASKELL__ >= 704 +{-# LANGUAGE Safe #-} +#endif + +module Test.SmallCheck.Property.Result + ( PropertySuccess(..) + , PropertyFailure(..) + , ppFailure + , Reason + , Argument + ) where + +import Data.Bool (Bool (False, True)) +import Data.Eq (Eq) +import Data.Function (($), (.)) +import Data.Int (Int) +import Data.List (map) +import Data.Maybe (Maybe (Nothing, Just)) +import Prelude (String) +import Text.PrettyPrint (Doc, empty, hsep, nest, render, text, (<+>), ($+$), ($$)) +import Text.Show (Show) + +-- | @since 1.0 +type Argument = String + +-- | An explanation for the test outcome. +-- +-- @since 1.1 +type Reason = String + +-- | @since 1.0 +data PropertySuccess + = Exist [Argument] PropertySuccess + | ExistUnique [Argument] PropertySuccess + | PropertyTrue (Maybe Reason) -- ^ @since 1.1 + | Vacuously PropertyFailure + deriving (Eq, Show) + +-- | @since 1.0 +data PropertyFailure + = NotExist + | AtLeastTwo [Argument] PropertySuccess [Argument] PropertySuccess + | CounterExample [Argument] PropertyFailure + | PropertyFalse (Maybe Reason) -- ^ @since 1.1 + deriving (Eq, Show) + +class Pretty a where + pretty :: a -> Doc + +instance Pretty PropertyFailure where + pretty NotExist = text "argument does not exist" + pretty (AtLeastTwo args1 s1 args2 s2) = + text "there are at least two" <+> + plural args1 empty (text "sets of") <+> + text "arguments satisfying the property:" $$ + formatExample args1 s1 $$ formatExample args2 s2 + where + formatExample args s = nest ind $ text "for" <+> prettyArgs args pretty s + pretty (CounterExample args f) = + text "there" <+> + text (plural args "exists" "exist") <+> + prettyArgs args <+> + text "such that" + pretty f + pretty (PropertyFalse Nothing) = text "condition is false" + pretty (PropertyFalse (Just s)) = text s + +instance Pretty PropertySuccess where + pretty (PropertyTrue Nothing) = text "condition is true" + pretty (PropertyTrue (Just s)) = text s + pretty (Exist args s) = existsMsg False args s + pretty (ExistUnique args s) = existsMsg True args s + pretty (Vacuously s) = text "property is vacuously true because" pretty s + +ind :: Int +ind = 2 + +infixl 5 +() :: Doc -> Doc -> Doc +a b = a $+$ nest ind b + +prettyArgs :: [Argument] -> Doc +prettyArgs = hsep . map text + +existsMsg :: Pretty a => Bool -> [Argument] -> a -> Doc +existsMsg unique args s = + text "there" <+> text (plural args "exists" "exist") <+> + (if unique then text "unique" else empty) <+> + prettyArgs args <+> + text "such that" + pretty s + +plural :: [a] -> b -> b -> b +plural lst sing pl = + case lst of + _:_:_ -> pl + _ -> sing + +-- | @since 1.0 +ppFailure :: PropertyFailure -> String +ppFailure = render . pretty diff --git a/Test/SmallCheck/Series.hs b/Test/SmallCheck/Series.hs --- a/Test/SmallCheck/Series.hs +++ b/Test/SmallCheck/Series.hs @@ -1,449 +1,1322 @@ --------------------------------------------------------------------- --- | --- Module : Test.SmallCheck.Series --- Copyright : (c) Colin Runciman et al. --- License : BSD3 --- Maintainer: Roman Cheplyaka --- --- Generation of test data. --------------------------------------------------------------------- -{-# LANGUAGE CPP #-} - -#ifdef GENERICS -{-# LANGUAGE DefaultSignatures - , FlexibleContexts - , TypeOperators - , TypeSynonymInstances - , FlexibleInstances - #-} -#endif - -module Test.SmallCheck.Series ( - -- * Basic definitions - Depth, Series, Serial(..), - - -- * Data Generators - -- | SmallCheck itself defines data generators for all the data types used - -- by the Prelude. - -- - -- Writing SmallCheck generators for application-specific types is - -- straightforward. You need to define a 'series' generator, typically using - -- @consN@ family of generic combinators where N is constructor arity. - -- - -- For example: - -- - -- >data Tree a = Null | Fork (Tree a) a (Tree a) - -- > - -- >instance Serial a => Serial (Tree a) where - -- > series = cons0 Null \/ cons3 Fork - -- - -- The default interpretation of depth for datatypes is the depth of nested - -- construction: constructor functions, including those for newtypes, build - -- results with depth one greater than their deepest argument. But this - -- default can be over-ridden by composing a @consN@ application with an - -- application of 'depth', like this: - -- - -- >newtype Light a = Light a - -- > - -- >instance Serial a => Serial (Light a) where - -- > series = cons1 Light . depth 0 - -- - -- The depth of @Light x@ is just the depth of @x@. - - -- ** What does consN do, exactly? - - -- | @consN@ has type - -- @(Serial t_1, ..., Serial t_N) => (t_1 -> ... -> t_N -> t) -> Series t@. - -- - -- @consN f@ is a series which, for a given depth @d > 0@, produces values of the - -- form - -- - -- >f x_1 ... x_N - -- - -- where @x_i@ ranges over all values of type @t_i@ of depth up to @d-1@ - -- (as defined by the 'series' functions for @t_i@). - -- - -- If @d <= 0@, no values are produced. - - cons0, cons1, cons2, cons3, cons4, - -- * Function Generators - - -- | To generate functions of an application-specific argument type - -- requires a second method 'coseries'. Again there is a standard - -- pattern, this time using the altsN combinators where again N is - -- constructor arity. Here are Tree and Light instances: - -- - -- >coseries rs d = [ \t -> case t of - -- > Null -> z - -- > Fork t1 x t2 -> f t1 x t2 - -- > | z <- alts0 rs d , - -- > f <- alts3 rs d ] - -- > - -- >coseries rs d = [ \l -> case l of - -- > Light x -> f x - -- > | f <- (alts1 rs . depth 0) d ] - - -- ** What does altsN do, exactly? - - -- | @altsN@ has type - -- @(Serial t_1, ..., Serial t_N) => Series t -> Series (t_1 -> ... -> t_N -> t)@. - -- - -- @altsN s@ is a series which, for a given depth @d@, produces functions of - -- type - -- - -- >t_1 -> ... -> t_N -> t - -- - -- If @d <= 0@, these are constant functions, one for each value of @s 0@. - -- - -- If @d > 0@, these functions inspect each of their arguments up to depth - -- @d-1@ (as defined by the 'coseries' functions for the corresponding - -- types) and return values given by @s d@. - - alts0, alts1, alts2, alts3, alts4, - - -- * Automated Derivation of Generators - - -- | For small examples, Series instances are easy enough to define by hand, - -- following the above patterns. But for programs with many or large data - -- type definitions, automatic derivation using a tool such as \"derive\" - -- is a better option. For example, the following command-line appends to - -- Prog.hs the Series instances for all data types defined there. - -- - -- >$ derive Prog.hs -d Serial --append - - -- ** Using GHC Generics - -- | For GHC users starting from GHC 7.2.1 there's also an option to use GHC's - -- Generics to get 'Serial' instance for free. - -- - -- Example: - -- - -- >{-# LANGUAGE DeriveGeneric #-} - -- >import Test.SmallCheck - -- >import GHC.Generics - -- > - -- >data Tree a = Null | Fork (Tree a) a (Tree a) - -- > deriving Generic - -- >instance Serial a => Serial (Tree a) - -- - -- Here we enable the @DeriveGeneric@ extension which allows to derive 'Generic' - -- instance for our data type. Then we declare that @Tree a@ is an instance of - -- 'Serial', but do not provide any definitions. This causes GHC to use the - -- default definitions that use the 'Generic' instance. - - -- * Other useful definitions - (\/), (><), - N(..), Nat, Natural, - depth - ) where - -import Data.List (intersperse) - -#ifdef GENERICS -import GHC.Generics -import Data.DList (DList, toList, fromList) -import Data.Monoid (mempty, mappend) -#endif - --- | Maximum depth of generated test values --- --- For data values, it is the depth of nested constructor applications. --- --- For functional values, it is both the depth of nested case analysis --- and the depth of results. -type Depth = Int - --- | 'Series' is a function from the depth to a finite list of values. --- --- If @s@ is a 'Series', @s n@ is expected to yield values of depth up to @n@. --- --- (In particular, @series d@ is expected to be a subset of @series (d+1)@.) -type Series a = Depth -> [a] - --- | Sum (union) of series -infixr 7 \/ -(\/) :: Series a -> Series a -> Series a -s1 \/ s2 = \d -> s1 d ++ s2 d - --- | Product of series -infixr 8 >< -(><) :: Series a -> Series b -> Series (a,b) -s1 >< s2 = \d -> [(x,y) | x <- s1 d, y <- s2 d] - -class Serial a where - series :: Series a - -- | A proper 'coseries' implementation should pass the depth unchanged to - -- its first argument. Doing otherwise will make enumeration of curried - -- functions non-uniform in their arguments. - coseries :: Series b -> Series (a->b) - -#ifdef GENERICS - default series :: (Generic a, GSerial (Rep a)) => Series a - series = map to . gSeries - - default coseries :: (Generic a, GSerial (Rep a)) => Series b -> Series (a->b) - coseries rs = map (. from) . gCoseries rs - -class GSerial f where - gSeries :: Series (f a) - gCoseries :: Series b -> Series (f a -> b) - -instance GSerial f => GSerial (M1 i c f) where - gSeries = map M1 . gSeries - gCoseries rs = map (. unM1) . gCoseries rs - {-# INLINE gSeries #-} - {-# INLINE gCoseries #-} - -instance Serial c => GSerial (K1 i c) where - gSeries = map K1 . series - gCoseries rs = map (. unK1) . coseries rs - {-# INLINE gSeries #-} - {-# INLINE gCoseries #-} - -instance GSerial U1 where - gSeries = cons0 U1 - gCoseries rs d = [\U1 -> b | b <- rs d] - {-# INLINE gSeries #-} - {-# INLINE gCoseries #-} - -instance (GSerial a, GSerial b) => GSerial (a :*: b) where - gSeries d = [x :*: y | x <- gSeries d, y <- gSeries d] - gCoseries rs = map uncur . gCoseries (gCoseries rs) - where - uncur f (x :*: y) = f x y - {-# INLINE gSeries #-} - {-# INLINE gCoseries #-} - -instance (GSerialSum a, GSerialSum b) => GSerial (a :+: b) where - gSeries = toList . gSeriesSum - gCoseries = gCoseriesSum - {-# INLINE gSeries #-} - {-# INLINE gCoseries #-} - -class GSerialSum f where - gSeriesSum :: DSeries (f a) - gCoseriesSum :: Series b -> Series (f a -> b) - -type DSeries a = Depth -> DList a - -instance (GSerialSum a, GSerialSum b) => GSerialSum (a :+: b) where - gSeriesSum d = fmap L1 (gSeriesSum d) `mappend` fmap R1 (gSeriesSum d) - gCoseriesSum rs d = [ \e -> case e of - L1 x -> f x - R1 y -> g y - | f <- gCoseriesSum rs d - , g <- gCoseriesSum rs d - ] - {-# INLINE gSeriesSum #-} - {-# INLINE gCoseriesSum #-} - -instance GSerial f => GSerialSum (C1 c f) where - gSeriesSum d | d > 0 = fromList $ gSeries (d-1) - | otherwise = mempty - gCoseriesSum rs d | d > 0 = gCoseries rs (d-1) - | otherwise = [\_ -> x | x <- rs d] - {-# INLINE gSeriesSum #-} - {-# INLINE gCoseriesSum #-} -#endif - -instance Serial () where - series _ = [()] - coseries rs d = [ \() -> b - | b <- rs d ] - -instance Serial Int where - series d = [(-d)..d] - coseries rs d = [ \i -> if i > 0 then f (N (i - 1)) - else if i < 0 then g (N (abs i - 1)) - else z - | z <- alts0 rs d, f <- alts1 rs d, g <- alts1 rs d ] - -instance Serial Integer where - series d = [ toInteger (i :: Int) - | i <- series d ] - coseries rs d = [ f . (fromInteger :: Integer->Int) - | f <- coseries rs d ] - --- | 'N' is a wrapper for 'Integral' types that causes only non-negative values --- to be generated. Generated functions of type @N a -> b@ do not distinguish --- different negative values of @a@. --- --- See also 'Nat' and 'Natural'. -newtype N a = N a - deriving (Eq, Ord) - -instance Show a => Show (N a) where - show (N i) = show i - -instance (Integral a, Serial a) => Serial (N a) where - series d = map N [0..d'] - where - d' = fromInteger (toInteger d) - coseries rs d = [ \(N i) -> if i > 0 then f (N (i - 1)) - else z - | z <- alts0 rs d, f <- alts1 rs d ] - -type Nat = N Int -type Natural = N Integer - -instance Serial Float where - series d = [ encodeFloat sig exp - | (sig,exp) <- series d, - odd sig || sig==0 && exp==0 ] - coseries rs d = [ f . decodeFloat - | f <- coseries rs d ] - -instance Serial Double where - series d = [ frac (x :: Float) - | x <- series d ] - coseries rs d = [ f . (frac :: Double->Float) - | f <- coseries rs d ] - -frac :: (Real a, Fractional a, Real b, Fractional b) => a -> b -frac = fromRational . toRational - -instance Serial Char where - series d = take (d+1) ['a'..'z'] - coseries rs d = [ \c -> f (N (fromEnum c - fromEnum 'a')) - | f <- coseries rs d ] - -instance (Serial a, Serial b) => - Serial (a,b) where - series = series >< series - coseries rs = map uncurry . (coseries $ coseries rs) - -instance (Serial a, Serial b, Serial c) => - Serial (a,b,c) where - series = \d -> [(a,b,c) | (a,(b,c)) <- series d] - coseries rs = map uncurry3 . (coseries $ coseries $ coseries rs) - -instance (Serial a, Serial b, Serial c, Serial d) => - Serial (a,b,c,d) where - series = \d -> [(a,b,c,d) | (a,(b,(c,d))) <- series d] - coseries rs = map uncurry4 . (coseries $ coseries $ coseries $ coseries rs) - -uncurry3 :: (a->b->c->d) -> ((a,b,c)->d) -uncurry3 f (x,y,z) = f x y z - -uncurry4 :: (a->b->c->d->e) -> ((a,b,c,d)->e) -uncurry4 f (w,x,y,z) = f w x y z - -cons0 :: - a -> Series a -cons0 c _ = [c] - -cons1 :: Serial a => - (a->b) -> Series b -cons1 c d = [c z | d > 0, z <- series (d-1)] - -cons2 :: (Serial a, Serial b) => - (a->b->c) -> Series c -cons2 c d = [c y z | d > 0, (y,z) <- series (d-1)] - -cons3 :: (Serial a, Serial b, Serial c) => - (a->b->c->d) -> Series d -cons3 c d = [c x y z | d > 0, (x,y,z) <- series (d-1)] - -cons4 :: (Serial a, Serial b, Serial c, Serial d) => - (a->b->c->d->e) -> Series e -cons4 c d = [c w x y z | d > 0, (w,x,y,z) <- series (d-1)] - -alts0 :: Series a -> - Series a -alts0 as d = as d - -alts1 :: Serial a => - Series b -> Series (a->b) -alts1 bs d = if d > 0 then coseries bs (dec d) - else [\_ -> x | x <- bs d] - -alts2 :: (Serial a, Serial b) => - Series c -> Series (a->b->c) -alts2 cs d = if d > 0 then coseries (coseries cs) (dec d) - else [\_ _ -> x | x <- cs d] - -alts3 :: (Serial a, Serial b, Serial c) => - Series d -> Series (a->b->c->d) -alts3 ds d = if d > 0 then coseries (coseries (coseries ds)) (dec d) - else [\_ _ _ -> x | x <- ds d] - -alts4 :: (Serial a, Serial b, Serial c, Serial d) => - Series e -> Series (a->b->c->d->e) -alts4 es d = if d > 0 then coseries (coseries (coseries (coseries es))) (dec d) - else [\_ _ _ _ -> x | x <- es d] - -instance Serial Bool where - series = cons0 True \/ cons0 False - coseries rs d = [ \x -> if x then r1 else r2 - | r1 <- rs d, r2 <- rs d ] - -instance Serial a => Serial (Maybe a) where - series = cons0 Nothing \/ cons1 Just - coseries rs d = [ \m -> case m of - Nothing -> z - Just x -> f x - | z <- alts0 rs d , - f <- alts1 rs d ] - -instance (Serial a, Serial b) => Serial (Either a b) where - series = cons1 Left \/ cons1 Right - coseries rs d = [ \e -> case e of - Left x -> f x - Right y -> g y - | f <- alts1 rs d , - g <- alts1 rs d ] - -instance Serial a => Serial [a] where - series = cons0 [] \/ cons2 (:) - coseries rs d = [ \xs -> case xs of - [] -> y - (x:xs') -> f x xs' - | y <- alts0 rs d , - f <- alts2 rs d ] - --- Thanks to Ralf Hinze for the definition of coseries --- using the nest auxiliary. -instance (Serial a, Serial b) => Serial (a->b) where - series = coseries series - coseries rs d = - [ \ f -> g [ f a | a <- args ] - | g <- nest args d ] - where - args = series d - nest [] _ = [ \[] -> c - | c <- rs d ] - nest (a:as) _ = [ \(b:bs) -> f b bs - | f <- coseries (nest as) d ] - --- | For customising the depth measure. Use with care! -depth :: Depth -> Depth -> Depth -depth d d' | d >= 0 = d'+1-d - | otherwise = error "SmallCheck.depth: argument < 0" - -dec :: Depth -> Depth -dec d | d > 0 = d-1 - | otherwise = error "SmallCheck.dec: argument <= 0" - -inc :: Depth -> Depth -inc d = d+1 - --- show the extension of a function (in part, bounded both by --- the number and depth of arguments) -instance (Serial a, Show a, Show b) => Show (a->b) where - show f = - if maxarheight == 1 - && sumarwidth + length ars * length "->;" < widthLimit then - "{"++( - concat $ intersperse ";" $ [a++"->"++r | (a,r) <- ars] - )++"}" - else - concat $ [a++"->\n"++indent r | (a,r) <- ars] - where - ars = take lengthLimit [ (show x, show (f x)) - | x <- series depthLimit ] - maxarheight = maximum [ max (height a) (height r) - | (a,r) <- ars ] - sumarwidth = sum [ length a + length r - | (a,r) <- ars] - indent = unlines . map (" "++) . lines - height = length . lines - (widthLimit,lengthLimit,depthLimit) = (80,20,3)::(Int,Int,Depth) +-- vim:fdm=marker:foldtext=foldtext() + +-------------------------------------------------------------------- +-- | +-- Module : Test.SmallCheck.Series +-- Copyright : (c) Colin Runciman et al. +-- License : BSD3 +-- Maintainer: Roman Cheplyaka +-- +-- You need this module if you want to generate test values of your own +-- types. +-- +-- You'll typically need the following extensions: +-- +-- >{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-} +-- +-- SmallCheck itself defines data generators for all the data types used +-- by the "Prelude". +-- +-- In order to generate values and functions of your own types, you need +-- to make them instances of 'Serial' (for values) and 'CoSerial' (for +-- functions). There are two main ways to do so: using Generics or writing +-- the instances by hand. +-------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} +#if __GLASGOW_HASKELL__ >= 702 +{-# LANGUAGE DefaultSignatures #-} +#endif +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + +#if MIN_VERSION_base(4,8,0) +{-# LANGUAGE Safe #-} +#else +{-# LANGUAGE OverlappingInstances #-} +#if __GLASGOW_HASKELL__ >= 704 +{-# LANGUAGE Trustworthy #-} +#endif +#endif + +#define HASCBOOL MIN_VERSION_base(4,10,0) + +module Test.SmallCheck.Series ( + -- {{{ + -- * Generic instances + -- | The easiest way to create the necessary instances is to use GHC + -- generics (available starting with GHC 7.2.1). + -- + -- Here's a complete example: + -- + -- >{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-} + -- >{-# LANGUAGE DeriveGeneric #-} + -- > + -- >import Test.SmallCheck.Series + -- >import GHC.Generics + -- > + -- >data Tree a = Null | Fork (Tree a) a (Tree a) + -- > deriving Generic + -- > + -- >instance Serial m a => Serial m (Tree a) + -- + -- Here we enable the @DeriveGeneric@ extension which allows to derive 'Generic' + -- instance for our data type. Then we declare that @Tree@ @a@ is an instance of + -- 'Serial', but do not provide any definitions. This causes GHC to use the + -- default definitions that use the 'Generic' instance. + -- + -- One minor limitation of generic instances is that there's currently no + -- way to distinguish newtypes and datatypes. Thus, newtype constructors + -- will also count as one level of depth. + + -- * Data Generators + -- | Writing 'Serial' instances for application-specific types is + -- straightforward. You need to define a 'series' generator, typically using + -- @consN@ family of generic combinators where N is constructor arity. + -- + -- For example: + -- + -- >data Tree a = Null | Fork (Tree a) a (Tree a) + -- > + -- >instance Serial m a => Serial m (Tree a) where + -- > series = cons0 Null \/ cons3 Fork + -- + -- For newtypes use 'newtypeCons' instead of 'cons1'. + -- The difference is that 'cons1' is counts as one level of depth, while + -- 'newtypeCons' doesn't affect the depth. + -- + -- >newtype Light a = Light a + -- > + -- >instance Serial m a => Serial m (Light a) where + -- > series = newtypeCons Light + -- + -- For data types with more than 6 fields define @consN@ as + -- + -- >consN f = decDepth $ + -- > f <$> series + -- > <~> series + -- > <~> series + -- > <~> ... {- series repeated N times in total -} + + -- ** What does @consN@ do, exactly? + + -- | @consN@ has type + -- @(Serial t₁, ..., Serial tₙ) => (t₁ -> ... -> tₙ -> t) -> Series t@. + -- + -- @consN@ @f@ is a series which, for a given depth \(d > 0\), produces values of the + -- form + -- + -- >f x₁ ... xₙ + -- + -- where @xₖ@ ranges over all values of type @tₖ@ of depth up to \(d-1\) + -- (as defined by the 'series' functions for @tₖ@). + -- + -- @consN@ functions also ensure that xₖ are enumerated in the + -- breadth-first order. Thus, combinations of smaller depth come first + -- (assuming the same is true for @tₖ@). + -- + -- If \(d \le 0\), no values are produced. + + cons0, cons1, cons2, cons3, cons4, cons5, cons6, newtypeCons, + -- * Function Generators + + -- | To generate functions of an application-specific argument type, + -- make the type an instance of 'CoSerial'. + -- + -- Again there is a standard pattern, this time using the @altsN@ + -- combinators where again N is constructor arity. Here are @Tree@ and + -- @Light@ instances: + -- + -- + -- >instance CoSerial m a => CoSerial m (Tree a) where + -- > coseries rs = + -- > alts0 rs >>- \z -> + -- > alts3 rs >>- \f -> + -- > return $ \t -> + -- > case t of + -- > Null -> z + -- > Fork t1 x t2 -> f t1 x t2 + -- + -- >instance CoSerial m a => CoSerial m (Light a) where + -- > coseries rs = + -- > newtypeAlts rs >>- \f -> + -- > return $ \l -> + -- > case l of + -- > Light x -> f x + -- + -- For data types with more than 6 fields define @altsN@ as + -- + -- >altsN rs = do + -- > rs <- fixDepth rs + -- > decDepthChecked + -- > (constM $ constM $ ... $ constM rs) + -- > (coseries $ coseries $ ... $ coseries rs) + -- > {- constM and coseries are repeated N times each -} + + -- ** What does altsN do, exactly? + + -- | @altsN@ has type + -- @(Serial t₁, ..., Serial tₙ) => Series t -> Series (t₁ -> ... -> tₙ -> t)@. + -- + -- @altsN@ @s@ is a series which, for a given depth \( d \), produces functions of + -- type + -- + -- >t₁ -> ... -> tₙ -> t + -- + -- If \( d \le 0 \), these are constant functions, one for each value produced + -- by @s@. + -- + -- If \( d > 0 \), these functions inspect each of their arguments up to the depth + -- \( d-1 \) (as defined by the 'coseries' functions for the corresponding + -- types) and return values produced by @s@. The depth to which the + -- values are enumerated does not depend on the depth of inspection. + + alts0, alts1, alts2, alts3, alts4, alts5, alts6, newtypeAlts, + + -- * Basic definitions + Depth, Series, Serial(..), CoSerial(..), + +#if __GLASGOW_HASKELL__ >= 702 + -- * Generic implementations + genericSeries, + genericCoseries, +#endif + + -- * Convenient wrappers + Positive(..), NonNegative(..), NonZero(..), NonEmpty(..), + + -- * Other useful definitions + (\/), (><), (<~>), (>>-), + localDepth, + decDepth, + getDepth, + generate, + limit, + listSeries, + list, + listM, + fixDepth, + decDepthChecked, + constM + -- }}} + ) where + +import Control.Applicative (empty, pure, (<$>), (<|>)) +import Control.Monad (Monad, liftM, guard, mzero, mplus, msum, return, (>>), (>>=)) +import Control.Monad.Identity (Identity(Identity), runIdentity) +import Control.Monad.Logic (MonadLogic, (>>-), interleave, msplit, observeAllT) +import Control.Monad.Reader (ask, local) +import Data.Bool (Bool (True, False), (&&), (||)) +import Data.Char (Char) +import Data.Complex (Complex((:+))) +import Data.Either (Either (Left, Right), either) +import Data.Eq (Eq, (==), (/=)) +import Data.Foldable (Foldable) +import Data.Function (($), (.), const) +import Data.Functor (Functor, fmap) +import Data.Functor.Compose (Compose(Compose), getCompose) +import Data.Int (Int, Int8, Int16, Int32, Int64) +import Data.List (intercalate, take, map, length, (++), maximum, sum, unlines, lines, concat) +import qualified Data.List.NonEmpty as NE +import Data.Maybe (Maybe (Just, Nothing), maybe) +import Data.Ord (Ord, Ordering (LT, EQ, GT), max, (<), (>), (>=), compare, (<=)) +import Data.Ratio (Ratio, numerator, denominator, (%)) +import Data.Traversable (Traversable) +import Data.Tuple (uncurry) +import Data.Void (Void, absurd) +import Data.Word (Word, Word8, Word16, Word32, Word64) +import Numeric.Natural (Natural) +import Prelude (Integer, Real, toRational, Enum, toEnum, fromEnum, Num, (+), (*), Integral, quotRem, toInteger, negate, abs, signum, fromInteger, Bounded, minBound, maxBound, Float, Double, (-), odd, encodeFloat, decodeFloat, realToFrac, seq, subtract) +import Test.SmallCheck.SeriesMonad +import Text.Show (Show, showsPrec, show) + +#if MIN_VERSION_base(4,5,0) +import Foreign.C.Types (CFloat(CFloat), CDouble(CDouble), CChar(CChar), CSChar(CSChar), CUChar(CUChar), CShort(CShort), CUShort(CUShort), CInt(CInt), CUInt(CUInt), CLong(CLong), CULong(CULong), CPtrdiff(CPtrdiff), CSize(CSize), CWchar(CWchar), CSigAtomic(CSigAtomic), CLLong(CLLong), CULLong(CULLong), CIntPtr(CIntPtr), CUIntPtr(CUIntPtr), CIntMax(CIntMax), CUIntMax(CUIntMax), CClock(CClock), CTime(CTime), CUSeconds(CUSeconds), CSUSeconds(CSUSeconds)) +#endif + +#if __GLASGOW_HASKELL__ >= 702 +import GHC.Generics (Generic, (:+:)(L1, R1), (:*:)((:*:)), C1, K1(K1), unK1, M1(M1), unM1, U1(U1), V1, Rep, to, from) +#else +import Prelude (RealFloat) +#endif +#if HASCBOOL +import Foreign.C.Types (CBool(CBool)) +#endif + +------------------------------ +-- Main types and classes +------------------------------ +--{{{ + +-- | @since 1.0 +class Monad m => Serial m a where + series :: Series m a + +#if __GLASGOW_HASKELL__ >= 704 + default series :: (Generic a, GSerial m (Rep a)) => Series m a + series = genericSeries +#endif + +#if __GLASGOW_HASKELL__ >= 702 +-- | @since 1.1.5 +genericSeries + :: (Monad m, Generic a, GSerial m (Rep a)) + => Series m a +genericSeries = to <$> gSeries +#endif + +-- | @since 1.0 +class Monad m => CoSerial m a where + -- | A proper 'coseries' implementation should pass the depth unchanged to + -- its first argument. Doing otherwise will make enumeration of curried + -- functions non-uniform in their arguments. + coseries :: Series m b -> Series m (a->b) + +#if __GLASGOW_HASKELL__ >= 704 + default coseries :: (Generic a, GCoSerial m (Rep a)) => Series m b -> Series m (a->b) + coseries = genericCoseries +#endif + +#if __GLASGOW_HASKELL__ >= 702 +-- | @since 1.1.5 +genericCoseries + :: (Monad m, Generic a, GCoSerial m (Rep a)) + => Series m b -> Series m (a->b) +genericCoseries rs = (. from) <$> gCoseries rs +#endif + +-- }}} + +------------------------------ +-- Helper functions +------------------------------ +-- {{{ + +-- | A simple series specified by a function from depth to the list of +-- values up to that depth. +-- +-- @since 1.0 +generate :: (Depth -> [a]) -> Series m a +generate f = do + d <- getDepth + msum $ map return $ f d + +-- | Limit a 'Series' to its first @n@ elements. +-- +-- @since 1.1.5 +limit :: forall m a . Monad m => Int -> Series m a -> Series m a +limit n0 (Series s) = Series $ go n0 s + where + go 0 _ = empty + go n mb1 = do + cons :: Maybe (b, ml b) <- msplit mb1 + case cons of + Nothing -> empty + Just (b, mb2) -> return b <|> go (n-1) mb2 + +suchThat :: Series m a -> (a -> Bool) -> Series m a +suchThat s p = s >>= \x -> if p x then pure x else empty + +-- | Given a depth, return the list of values generated by a 'Serial' instance. +-- +-- For example, list all integers up to depth 1: +-- +-- * @listSeries 1 :: [Int] -- returns [0,1,-1]@ +-- +-- @since 1.1.2 +listSeries :: Serial Identity a => Depth -> [a] +listSeries d = list d series + +-- | Return the list of values generated by a 'Series'. Useful for +-- debugging 'Serial' instances. +-- +-- Examples: +-- +-- * @'list' 3 'series' :: ['Int'] -- returns [0,1,-1,2,-2,3,-3]@ +-- +-- * @'list' 3 ('series' :: 'Series' 'Data.Functor.Identity' 'Int') -- returns [0,1,-1,2,-2,3,-3]@ +-- +-- * @'list' 2 'series' :: [['Bool']] -- returns [[],['True'],['False']]@ +-- +-- The first two are equivalent. The second has a more explicit type binding. +-- +-- @since 1.0 +list :: Depth -> Series Identity a -> [a] +list d s = runIdentity $ observeAllT $ runSeries d s + +-- | Monadic version of 'list'. +-- +-- @since 1.1 +listM d s = observeAllT $ runSeries d s + +-- | Sum (union) of series. +-- +-- @since 1.0 +infixr 7 \/ +(\/) :: Monad m => Series m a -> Series m a -> Series m a +(\/) = interleave + +-- | Product of series +-- +-- @since 1.0 +infixr 8 >< +(><) :: Monad m => Series m a -> Series m b -> Series m (a,b) +a >< b = (,) <$> a <~> b + +-- | Fair version of 'Control.Applicative.ap' and 'Control.Applicative.<*>'. +-- +-- @since 1.0 +infixl 4 <~> +(<~>) :: Monad m => Series m (a -> b) -> Series m a -> Series m b +a <~> b = a >>- (<$> b) + +uncurry3 :: (a->b->c->d) -> ((a,b,c)->d) +uncurry3 f (x,y,z) = f x y z + +uncurry4 :: (a->b->c->d->e) -> ((a,b,c,d)->e) +uncurry4 f (w,x,y,z) = f w x y z + +uncurry5 :: (a->b->c->d->e->f) -> ((a,b,c,d,e)->f) +uncurry5 f (v,w,x,y,z) = f v w x y z + +uncurry6 :: (a->b->c->d->e->f->g) -> ((a,b,c,d,e,f)->g) +uncurry6 f (u,v,w,x,y,z) = f u v w x y z + +-- | Query the current depth. +-- +-- @since 1.0 +getDepth :: Series m Depth +getDepth = Series ask + +-- | Run a series with a modified depth. +-- +-- @since 1.0 +localDepth :: (Depth -> Depth) -> Series m a -> Series m a +localDepth f (Series a) = Series $ local f a + +-- | Run a 'Series' with the depth decreased by 1. +-- +-- If the current depth is less or equal to 0, the result is 'empty'. +-- +-- @since 1.0 +decDepth :: Series m a -> Series m a +decDepth a = do + checkDepth + localDepth (subtract 1) a + +checkDepth :: Series m () +checkDepth = do + d <- getDepth + guard $ d > 0 + +-- | @'constM' = 'liftM' 'const'@ +-- +-- @since 1.1.1 +constM :: Monad m => m b -> m (a -> b) +constM = liftM const + +-- | Fix the depth of a series at the current level. The resulting series +-- will no longer depend on the \"ambient\" depth. +-- +-- @since 1.1.1 +fixDepth :: Series m a -> Series m (Series m a) +fixDepth s = getDepth >>= \d -> return $ localDepth (const d) s + +-- | If the current depth is 0, evaluate the first argument. Otherwise, +-- evaluate the second argument with decremented depth. +-- +-- @since 1.1.1 +decDepthChecked :: Series m a -> Series m a -> Series m a +decDepthChecked b r = do + d <- getDepth + if d <= 0 + then b + else decDepth r + +unwind :: MonadLogic m => m a -> m [a] +unwind a = + msplit a >>= + maybe (return []) (\(x,a') -> (x:) `liftM` unwind a') + +-- }}} + +------------------------------ +-- cons* and alts* functions +------------------------------ +-- {{{ + +-- | @since 1.0 +cons0 :: a -> Series m a +cons0 x = decDepth $ pure x + +-- | @since 1.0 +cons1 :: Serial m a => (a->b) -> Series m b +cons1 f = decDepth $ f <$> series + +-- | Same as 'cons1', but preserves the depth. +-- +-- @since 1.0 +newtypeCons :: Serial m a => (a->b) -> Series m b +newtypeCons f = f <$> series + +-- | @since 1.0 +cons2 :: (Serial m a, Serial m b) => (a->b->c) -> Series m c +cons2 f = decDepth $ f <$> series <~> series + +-- | @since 1.0 +cons3 :: (Serial m a, Serial m b, Serial m c) => + (a->b->c->d) -> Series m d +cons3 f = decDepth $ + f <$> series + <~> series + <~> series + +-- | @since 1.0 +cons4 :: (Serial m a, Serial m b, Serial m c, Serial m d) => + (a->b->c->d->e) -> Series m e +cons4 f = decDepth $ + f <$> series + <~> series + <~> series + <~> series + +-- | @since 1.2.0 +cons5 :: (Serial m a, Serial m b, Serial m c, Serial m d, Serial m e) => + (a->b->c->d->e->f) -> Series m f +cons5 f = decDepth $ + f <$> series + <~> series + <~> series + <~> series + <~> series + +-- | @since 1.2.0 +cons6 :: (Serial m a, Serial m b, Serial m c, Serial m d, Serial m e, Serial m f) => + (a->b->c->d->e->f->g) -> Series m g +cons6 f = decDepth $ + f <$> series + <~> series + <~> series + <~> series + <~> series + <~> series + +-- | @since 1.0 +alts0 :: Series m a -> Series m a +alts0 s = s + +-- | @since 1.0 +alts1 :: CoSerial m a => Series m b -> Series m (a->b) +alts1 rs = do + rs <- fixDepth rs + decDepthChecked (constM rs) (coseries rs) + +-- | @since 1.0 +alts2 + :: (CoSerial m a, CoSerial m b) + => Series m c -> Series m (a->b->c) +alts2 rs = do + rs <- fixDepth rs + decDepthChecked + (constM $ constM rs) + (coseries $ coseries rs) + +-- | @since 1.0 +alts3 :: (CoSerial m a, CoSerial m b, CoSerial m c) => + Series m d -> Series m (a->b->c->d) +alts3 rs = do + rs <- fixDepth rs + decDepthChecked + (constM $ constM $ constM rs) + (coseries $ coseries $ coseries rs) + +-- | @since 1.0 +alts4 :: (CoSerial m a, CoSerial m b, CoSerial m c, CoSerial m d) => + Series m e -> Series m (a->b->c->d->e) +alts4 rs = do + rs <- fixDepth rs + decDepthChecked + (constM $ constM $ constM $ constM rs) + (coseries $ coseries $ coseries $ coseries rs) + +-- | @since 1.2.0 +alts5 :: (CoSerial m a, CoSerial m b, CoSerial m c, CoSerial m d, CoSerial m e) => + Series m f -> Series m (a->b->c->d->e->f) +alts5 rs = do + rs <- fixDepth rs + decDepthChecked + (constM $ constM $ constM $ constM $ constM rs) + (coseries $ coseries $ coseries $ coseries $ coseries rs) + +-- | @since 1.2.0 +alts6 :: (CoSerial m a, CoSerial m b, CoSerial m c, CoSerial m d, CoSerial m e, CoSerial m f) => + Series m g -> Series m (a->b->c->d->e->f->g) +alts6 rs = do + rs <- fixDepth rs + decDepthChecked + (constM $ constM $ constM $ constM $ constM $ constM rs) + (coseries $ coseries $ coseries $ coseries $ coseries $ coseries rs) + +-- | Same as 'alts1', but preserves the depth. +-- +-- @since 1.0 +newtypeAlts :: CoSerial m a => Series m b -> Series m (a->b) +newtypeAlts = coseries + +-- }}} + +------------------------------ +-- Generic instances +------------------------------ +-- {{{ + +class GSerial m f where + gSeries :: Series m (f a) +class GCoSerial m f where + gCoseries :: Series m b -> Series m (f a -> b) + +#if __GLASGOW_HASKELL__ >= 702 +instance {-# OVERLAPPABLE #-} GSerial m f => GSerial m (M1 i c f) where + gSeries = M1 <$> gSeries + {-# INLINE gSeries #-} +instance GCoSerial m f => GCoSerial m (M1 i c f) where + gCoseries rs = (. unM1) <$> gCoseries rs + {-# INLINE gCoseries #-} + +instance Serial m c => GSerial m (K1 i c) where + gSeries = K1 <$> series + {-# INLINE gSeries #-} +instance CoSerial m c => GCoSerial m (K1 i c) where + gCoseries rs = (. unK1) <$> coseries rs + {-# INLINE gCoseries #-} + +instance GSerial m U1 where + gSeries = pure U1 + {-# INLINE gSeries #-} +instance GCoSerial m U1 where + gCoseries rs = constM rs + {-# INLINE gCoseries #-} + +instance GSerial m V1 where + gSeries = mzero + {-# INLINE gSeries #-} +instance GCoSerial m V1 where + gCoseries = const $ return (\a -> a `seq` let x = x in x) + {-# INLINE gCoseries #-} + +instance (Monad m, GSerial m a, GSerial m b) => GSerial m (a :*: b) where + gSeries = (:*:) <$> gSeries <~> gSeries + {-# INLINE gSeries #-} +instance (Monad m, GCoSerial m a, GCoSerial m b) => GCoSerial m (a :*: b) where + gCoseries rs = uncur <$> gCoseries (gCoseries rs) + where + uncur f (x :*: y) = f x y + {-# INLINE gCoseries #-} + +instance (Monad m, GSerial m a, GSerial m b) => GSerial m (a :+: b) where + gSeries = (L1 <$> gSeries) `interleave` (R1 <$> gSeries) + {-# INLINE gSeries #-} +instance (Monad m, GCoSerial m a, GCoSerial m b) => GCoSerial m (a :+: b) where + gCoseries rs = + gCoseries rs >>- \f -> + gCoseries rs >>- \g -> + return $ + \e -> case e of + L1 x -> f x + R1 y -> g y + {-# INLINE gCoseries #-} + +instance {-# OVERLAPPING #-} GSerial m f => GSerial m (C1 c f) where + gSeries = M1 <$> decDepth gSeries + {-# INLINE gSeries #-} +#endif + +-- }}} + +------------------------------ +-- Instances for basic types +------------------------------ +-- {{{ +instance Monad m => Serial m () where + series = return () +instance Monad m => CoSerial m () where + coseries rs = constM rs + +instance Monad m => Serial m Integer where series = unM <$> series +instance Monad m => CoSerial m Integer where coseries = fmap (. M) . coseries + +-- | @since 1.1.3 +instance Monad m => Serial m Natural where series = unN <$> series +-- | @since 1.1.3 +instance Monad m => CoSerial m Natural where coseries = fmap (. N) . coseries + +instance Monad m => Serial m Int where series = unM <$> series +instance Monad m => CoSerial m Int where coseries = fmap (. M) . coseries + +-- | @since 1.1.3 +instance Monad m => Serial m Word where series = unN <$> series +-- | @since 1.1.3 +instance Monad m => CoSerial m Word where coseries = fmap (. N) . coseries + +-- | @since 1.1.4 +instance Monad m => Serial m Int8 where series = unM <$> series +-- | @since 1.1.4 +instance Monad m => CoSerial m Int8 where coseries = fmap (. M) . coseries + +-- | @since 1.1.4 +instance Monad m => Serial m Word8 where series = unN <$> series +-- | @since 1.1.4 +instance Monad m => CoSerial m Word8 where coseries = fmap (. N) . coseries + +-- | @since 1.1.4 +instance Monad m => Serial m Int16 where series = unM <$> series +-- | @since 1.1.4 +instance Monad m => CoSerial m Int16 where coseries = fmap (. M) . coseries + +-- | @since 1.1.4 +instance Monad m => Serial m Word16 where series = unN <$> series +-- | @since 1.1.4 +instance Monad m => CoSerial m Word16 where coseries = fmap (. N) . coseries + +-- | @since 1.1.4 +instance Monad m => Serial m Int32 where series = unM <$> series +-- | @since 1.1.4 +instance Monad m => CoSerial m Int32 where coseries = fmap (. M) . coseries + +-- | @since 1.1.4 +instance Monad m => Serial m Word32 where series = unN <$> series +-- | @since 1.1.4 +instance Monad m => CoSerial m Word32 where coseries = fmap (. N) . coseries + +-- | @since 1.1.4 +instance Monad m => Serial m Int64 where series = unM <$> series +-- | @since 1.1.4 +instance Monad m => CoSerial m Int64 where coseries = fmap (. M) . coseries + +-- | @since 1.1.4 +instance Monad m => Serial m Word64 where series = unN <$> series +-- | @since 1.1.4 +instance Monad m => CoSerial m Word64 where coseries = fmap (. N) . coseries + +-- | 'N' is a wrapper for 'Integral' types that causes only non-negative values +-- to be generated. Generated functions of type @N a -> b@ do not distinguish +-- different negative values of @a@. +newtype N a = N { unN :: a } deriving (Eq, Ord, Show) + +instance Real a => Real (N a) where + toRational (N x) = toRational x + +instance Enum a => Enum (N a) where + toEnum x = N (toEnum x) + fromEnum (N x) = fromEnum x + +instance Num a => Num (N a) where + N x + N y = N (x + y) + N x * N y = N (x * y) + negate (N x) = N (negate x) + abs (N x) = N (abs x) + signum (N x) = N (signum x) + fromInteger x = N (fromInteger x) + +instance Integral a => Integral (N a) where + quotRem (N x) (N y) = (N q, N r) + where + (q, r) = x `quotRem` y + toInteger (N x) = toInteger x + +instance (Num a, Enum a, Serial m a) => Serial m (N a) where + series = generate $ \d -> take (d+1) [0..] + +instance (Integral a, Monad m) => CoSerial m (N a) where + coseries rs = + -- This is a recursive function, because @alts1 rs@ typically calls + -- back to 'coseries' (but with lower depth). + -- + -- The recursion stops when depth == 0. Then alts1 produces a constant + -- function, and doesn't call back to 'coseries'. + alts0 rs >>- \z -> + alts1 rs >>- \f -> + return $ \(N i) -> + if i > 0 + then f (N $ i-1) + else z + +-- | 'M' is a helper type to generate values of a signed type of increasing magnitude. +newtype M a = M { unM :: a } deriving (Eq, Ord, Show) + +instance Real a => Real (M a) where + toRational (M x) = toRational x + +instance Enum a => Enum (M a) where + toEnum x = M (toEnum x) + fromEnum (M x) = fromEnum x + +instance Num a => Num (M a) where + M x + M y = M (x + y) + M x * M y = M (x * y) + negate (M x) = M (negate x) + abs (M x) = M (abs x) + signum (M x) = M (signum x) + fromInteger x = M (fromInteger x) + +instance Integral a => Integral (M a) where + quotRem (M x) (M y) = (M q, M r) + where + (q, r) = x `quotRem` y + toInteger (M x) = toInteger x + +instance (Num a, Enum a, Monad m) => Serial m (M a) where + series = others `interleave` positives + where positives = generate $ \d -> take d [1..] + others = generate $ \d -> take (d+1) [0,-1..] + +instance (Ord a, Num a, Monad m) => CoSerial m (M a) where + coseries rs = + alts0 rs >>- \z -> + alts1 rs >>- \f -> + alts1 rs >>- \g -> + pure $ \ i -> case compare i 0 of + GT -> f (M (i - 1)) + LT -> g (M (abs i - 1)) + EQ -> z + +instance Monad m => Serial m Float where + series = + series >>- \(sig, exp) -> + guard (odd sig || sig==0 && exp==0) >> + return (encodeFloat sig exp) +instance Monad m => CoSerial m Float where + coseries rs = + coseries rs >>- \f -> + return $ f . decodeFloat + +instance Monad m => Serial m Double where + series = (realToFrac :: Float -> Double) <$> series +instance Monad m => CoSerial m Double where + coseries rs = + (. (realToFrac :: Double -> Float)) <$> coseries rs + +-- | @since 1.1 +instance (Integral i, Serial m i) => Serial m (Ratio i) where + series = pairToRatio <$> series + where + pairToRatio (n, Positive d) = n % d +-- | @since 1.1 +instance (Integral i, CoSerial m i) => CoSerial m (Ratio i) where + coseries rs = (. ratioToPair) <$> coseries rs + where + ratioToPair r = (numerator r, denominator r) + +instance Monad m => Serial m Char where + series = generate $ \d -> take (d+1) ['a'..'z'] +instance Monad m => CoSerial m Char where + coseries rs = + coseries rs >>- \f -> + return $ \c -> f (N (fromEnum c - fromEnum 'a')) + +instance (Serial m a, Serial m b) => Serial m (a,b) where + series = cons2 (,) +instance (CoSerial m a, CoSerial m b) => CoSerial m (a,b) where + coseries rs = uncurry <$> alts2 rs + +instance (Serial m a, Serial m b, Serial m c) => Serial m (a,b,c) where + series = cons3 (,,) +instance (CoSerial m a, CoSerial m b, CoSerial m c) => CoSerial m (a,b,c) where + coseries rs = uncurry3 <$> alts3 rs + +instance (Serial m a, Serial m b, Serial m c, Serial m d) => Serial m (a,b,c,d) where + series = cons4 (,,,) +instance (CoSerial m a, CoSerial m b, CoSerial m c, CoSerial m d) => CoSerial m (a,b,c,d) where + coseries rs = uncurry4 <$> alts4 rs + +-- | @since 1.2.0 +instance (Serial m a, Serial m b, Serial m c, Serial m d, Serial m e) => Serial m (a,b,c,d,e) where + series = cons5 (,,,,) +-- | @since 1.2.0 +instance (CoSerial m a, CoSerial m b, CoSerial m c, CoSerial m d, CoSerial m e) => CoSerial m (a,b,c,d,e) where + coseries rs = uncurry5 <$> alts5 rs + +-- | @since 1.2.0 +instance (Serial m a, Serial m b, Serial m c, Serial m d, Serial m e, Serial m f) => Serial m (a,b,c,d,e,f) where + series = cons6 (,,,,,) +-- | @since 1.2.0 +instance (CoSerial m a, CoSerial m b, CoSerial m c, CoSerial m d, CoSerial m e, CoSerial m f) => CoSerial m (a,b,c,d,e,f) where + coseries rs = uncurry6 <$> alts6 rs + +instance Monad m => Serial m Bool where + series = cons0 True \/ cons0 False +instance Monad m => CoSerial m Bool where + coseries rs = + rs >>- \r1 -> + rs >>- \r2 -> + return $ \x -> if x then r1 else r2 + +-- | @since 1.2.1 +instance Monad m => Serial m Ordering where + series = cons0 LT \/ cons0 EQ \/ cons0 GT +-- | @since 1.2.1 +instance Monad m => CoSerial m Ordering where + coseries rs = + rs >>- \r1 -> + rs >>- \r2 -> + rs >>- \r3 -> + pure $ \x -> case x of + LT -> r1 + EQ -> r2 + GT -> r3 + +instance (Serial m a) => Serial m (Maybe a) where + series = cons0 Nothing \/ cons1 Just +instance (CoSerial m a) => CoSerial m (Maybe a) where + coseries rs = + maybe <$> alts0 rs <~> alts1 rs + +instance (Serial m a, Serial m b) => Serial m (Either a b) where + series = cons1 Left \/ cons1 Right +instance (CoSerial m a, CoSerial m b) => CoSerial m (Either a b) where + coseries rs = + either <$> alts1 rs <~> alts1 rs + +instance Serial m a => Serial m [a] where + series = cons0 [] \/ cons2 (:) +instance CoSerial m a => CoSerial m [a] where + coseries rs = + alts0 rs >>- \y -> + alts2 rs >>- \f -> + return $ \xs -> case xs of [] -> y; x:xs' -> f x xs' + +-- | @since 1.2.0 +instance Serial m a => Serial m (NE.NonEmpty a) where + series = cons2 (NE.:|) + +-- | @since 1.2.0 +instance CoSerial m a => CoSerial m (NE.NonEmpty a) where + coseries rs = + alts2 rs >>- \f -> + return $ \(x NE.:| xs') -> f x xs' + +#if MIN_VERSION_base(4,4,0) +-- | @since 1.2.0 +instance Serial m a => Serial m (Complex a) where +#else +-- | @since 1.2.0 +instance (RealFloat a, Serial m a) => Serial m (Complex a) where +#endif + series = cons2 (:+) + +#if MIN_VERSION_base(4,4,0) +-- | @since 1.2.0 +instance CoSerial m a => CoSerial m (Complex a) where +#else +-- | @since 1.2.0 +instance (RealFloat a, CoSerial m a) => CoSerial m (Complex a) where +#endif + coseries rs = + alts2 rs >>- \f -> + return $ \(x :+ xs') -> f x xs' + +-- | @since 1.2.0 +instance Monad m => Serial m Void where + series = mzero + +-- | @since 1.2.0 +instance Monad m => CoSerial m Void where + coseries = const $ return absurd + +instance (CoSerial m a, Serial m b) => Serial m (a->b) where + series = coseries series +-- Thanks to Ralf Hinze for the definition of coseries +-- using the nest auxiliary. +instance (Serial m a, CoSerial m a, Serial m b, CoSerial m b) => CoSerial m (a->b) where + coseries r = do + args <- unwind series + + g <- nest r args + return $ \f -> g $ map f args + + where + + nest :: forall a b m c . (Serial m b, CoSerial m b) => Series m c -> [a] -> Series m ([b] -> c) + nest rs args = do + case args of + [] -> const `liftM` rs + _:rest -> do + let sf = coseries $ nest rs rest + f <- sf + return $ \(b:bs) -> f b bs + +-- show the extension of a function (in part, bounded both by +-- the number and depth of arguments) +instance (Serial Identity a, Show a, Show b) => Show (a -> b) where + show f = + if maxarheight == 1 + && sumarwidth + length ars * length "->;" < widthLimit then + "{"++ + intercalate ";" [a++"->"++r | (a,r) <- ars] + ++"}" + else + concat $ [a++"->\n"++indent r | (a,r) <- ars] + where + ars = take lengthLimit [ (show x, show (f x)) + | x <- list depthLimit series ] + maxarheight = maximum [ max (height a) (height r) + | (a,r) <- ars ] + sumarwidth = sum [ length a + length r + | (a,r) <- ars] + indent = unlines . map (" "++) . lines + height = length . lines + (widthLimit,lengthLimit,depthLimit) = (80,20,3)::(Int,Int,Depth) + +-- | @since 1.2.0 +instance (Monad m, Serial m (f (g a))) => Serial m (Compose f g a) where + series = Compose <$> series +-- | @since 1.2.0 +instance (Monad m, CoSerial m (f (g a))) => CoSerial m (Compose f g a) where + coseries = fmap (. getCompose) . coseries + +-- }}} + +------------------------------ +-- Convenient wrappers +------------------------------ +-- {{{ + +-------------------------------------------------------------------------- +-- | 'Positive' @x@ guarantees that \( x > 0 \). +-- +-- @since 1.0 +newtype Positive a = Positive { getPositive :: a } + deriving + ( Eq + , Ord + , Functor -- ^ @since 1.2.0 + , Foldable -- ^ @since 1.2.0 + , Traversable -- ^ @since 1.2.0 + ) + +instance Real a => Real (Positive a) where + toRational (Positive x) = toRational x + +-- | @since 1.2.0 +instance (Num a, Bounded a) => Bounded (Positive a) where + minBound = Positive 1 + maxBound = Positive (maxBound :: a) + +instance Enum a => Enum (Positive a) where + toEnum x = Positive (toEnum x) + fromEnum (Positive x) = fromEnum x + +instance Num a => Num (Positive a) where + Positive x + Positive y = Positive (x + y) + Positive x * Positive y = Positive (x * y) + negate (Positive x) = Positive (negate x) + abs (Positive x) = Positive (abs x) + signum (Positive x) = Positive (signum x) + fromInteger x = Positive (fromInteger x) + +instance Integral a => Integral (Positive a) where + quotRem (Positive x) (Positive y) = (Positive q, Positive r) + where + (q, r) = x `quotRem` y + toInteger (Positive x) = toInteger x + +instance (Num a, Ord a, Serial m a) => Serial m (Positive a) where + series = Positive <$> series `suchThat` (> 0) + +instance Show a => Show (Positive a) where + showsPrec n (Positive x) = showsPrec n x + +-- | 'NonNegative' @x@ guarantees that \( x \ge 0 \). +-- +-- @since 1.0 +newtype NonNegative a = NonNegative { getNonNegative :: a } + deriving + ( Eq + , Ord + , Functor -- ^ @since 1.2.0 + , Foldable -- ^ @since 1.2.0 + , Traversable -- ^ @since 1.2.0 + ) + +instance Real a => Real (NonNegative a) where + toRational (NonNegative x) = toRational x + +-- | @since 1.2.0 +instance (Num a, Bounded a) => Bounded (NonNegative a) where + minBound = NonNegative 0 + maxBound = NonNegative (maxBound :: a) + +instance Enum a => Enum (NonNegative a) where + toEnum x = NonNegative (toEnum x) + fromEnum (NonNegative x) = fromEnum x + +instance Num a => Num (NonNegative a) where + NonNegative x + NonNegative y = NonNegative (x + y) + NonNegative x * NonNegative y = NonNegative (x * y) + negate (NonNegative x) = NonNegative (negate x) + abs (NonNegative x) = NonNegative (abs x) + signum (NonNegative x) = NonNegative (signum x) + fromInteger x = NonNegative (fromInteger x) + +instance Integral a => Integral (NonNegative a) where + quotRem (NonNegative x) (NonNegative y) = (NonNegative q, NonNegative r) + where + (q, r) = x `quotRem` y + toInteger (NonNegative x) = toInteger x + +instance (Num a, Ord a, Serial m a) => Serial m (NonNegative a) where + series = NonNegative <$> series `suchThat` (>= 0) + +instance Show a => Show (NonNegative a) where + showsPrec n (NonNegative x) = showsPrec n x + +-- | 'NonZero' @x@ guarantees that \( x \ne 0 \). +-- +-- @since 1.2.0 +newtype NonZero a = NonZero { getNonZero :: a } + deriving (Eq, Ord, Functor, Foldable, Traversable) + +instance Real a => Real (NonZero a) where + toRational (NonZero x) = toRational x + +instance (Eq a, Num a, Bounded a) => Bounded (NonZero a) where + minBound = let x = minBound in NonZero (if x == 0 then 1 else x) + maxBound = let x = maxBound in NonZero (if x == 0 then -1 else x) + +instance Enum a => Enum (NonZero a) where + toEnum x = NonZero (toEnum x) + fromEnum (NonZero x) = fromEnum x + +instance Num a => Num (NonZero a) where + NonZero x + NonZero y = NonZero (x + y) + NonZero x * NonZero y = NonZero (x * y) + negate (NonZero x) = NonZero (negate x) + abs (NonZero x) = NonZero (abs x) + signum (NonZero x) = NonZero (signum x) + fromInteger x = NonZero (fromInteger x) + +instance Integral a => Integral (NonZero a) where + quotRem (NonZero x) (NonZero y) = (NonZero q, NonZero r) + where + (q, r) = x `quotRem` y + toInteger (NonZero x) = toInteger x + +instance (Num a, Ord a, Serial m a) => Serial m (NonZero a) where + series = NonZero <$> series `suchThat` (/= 0) + +instance Show a => Show (NonZero a) where + showsPrec n (NonZero x) = showsPrec n x + +-- | 'NonEmpty' @xs@ guarantees that @xs@ is not null. +-- +-- @since 1.1 +newtype NonEmpty a = NonEmpty { getNonEmpty :: [a] } + +instance (Serial m a) => Serial m (NonEmpty a) where + series = NonEmpty <$> cons2 (:) + +instance Show a => Show (NonEmpty a) where + showsPrec n (NonEmpty x) = showsPrec n x + +-- }}} + +------------------------------ +-- Foreign.C.Types +------------------------------ +-- {{{ + +#if MIN_VERSION_base(4,5,0) +-- | @since 1.2.0 +instance Monad m => Serial m CFloat where + series = newtypeCons CFloat +-- | @since 1.2.0 +instance Monad m => CoSerial m CFloat where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CFloat x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CDouble where + series = newtypeCons CDouble +-- | @since 1.2.0 +instance Monad m => CoSerial m CDouble where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CDouble x -> f x + +#if HASCBOOL +-- | @since 1.2.0 +instance Monad m => Serial m CBool where + series = newtypeCons CBool +-- | @since 1.2.0 +instance Monad m => CoSerial m CBool where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CBool x -> f x +#endif + +-- | @since 1.2.0 +instance Monad m => Serial m CChar where + series = newtypeCons CChar +-- | @since 1.2.0 +instance Monad m => CoSerial m CChar where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CChar x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CSChar where + series = newtypeCons CSChar +-- | @since 1.2.0 +instance Monad m => CoSerial m CSChar where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CSChar x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CUChar where + series = newtypeCons CUChar +-- | @since 1.2.0 +instance Monad m => CoSerial m CUChar where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CUChar x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CShort where + series = newtypeCons CShort +-- | @since 1.2.0 +instance Monad m => CoSerial m CShort where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CShort x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CUShort where + series = newtypeCons CUShort +-- | @since 1.2.0 +instance Monad m => CoSerial m CUShort where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CUShort x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CInt where + series = newtypeCons CInt +-- | @since 1.2.0 +instance Monad m => CoSerial m CInt where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CInt x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CUInt where + series = newtypeCons CUInt +-- | @since 1.2.0 +instance Monad m => CoSerial m CUInt where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CUInt x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CLong where + series = newtypeCons CLong +-- | @since 1.2.0 +instance Monad m => CoSerial m CLong where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CLong x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CULong where + series = newtypeCons CULong +-- | @since 1.2.0 +instance Monad m => CoSerial m CULong where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CULong x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CPtrdiff where + series = newtypeCons CPtrdiff +-- | @since 1.2.0 +instance Monad m => CoSerial m CPtrdiff where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CPtrdiff x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CSize where + series = newtypeCons CSize +-- | @since 1.2.0 +instance Monad m => CoSerial m CSize where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CSize x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CWchar where + series = newtypeCons CWchar +-- | @since 1.2.0 +instance Monad m => CoSerial m CWchar where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CWchar x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CSigAtomic where + series = newtypeCons CSigAtomic +-- | @since 1.2.0 +instance Monad m => CoSerial m CSigAtomic where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CSigAtomic x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CLLong where + series = newtypeCons CLLong +-- | @since 1.2.0 +instance Monad m => CoSerial m CLLong where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CLLong x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CULLong where + series = newtypeCons CULLong +-- | @since 1.2.0 +instance Monad m => CoSerial m CULLong where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CULLong x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CIntPtr where + series = newtypeCons CIntPtr +-- | @since 1.2.0 +instance Monad m => CoSerial m CIntPtr where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CIntPtr x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CUIntPtr where + series = newtypeCons CUIntPtr +-- | @since 1.2.0 +instance Monad m => CoSerial m CUIntPtr where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CUIntPtr x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CIntMax where + series = newtypeCons CIntMax +-- | @since 1.2.0 +instance Monad m => CoSerial m CIntMax where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CIntMax x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CUIntMax where + series = newtypeCons CUIntMax +-- | @since 1.2.0 +instance Monad m => CoSerial m CUIntMax where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CUIntMax x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CClock where + series = newtypeCons CClock +-- | @since 1.2.0 +instance Monad m => CoSerial m CClock where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CClock x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CTime where + series = newtypeCons CTime +-- | @since 1.2.0 +instance Monad m => CoSerial m CTime where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CTime x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CUSeconds where + series = newtypeCons CUSeconds +-- | @since 1.2.0 +instance Monad m => CoSerial m CUSeconds where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CUSeconds x -> f x + +-- | @since 1.2.0 +instance Monad m => Serial m CSUSeconds where + series = newtypeCons CSUSeconds +-- | @since 1.2.0 +instance Monad m => CoSerial m CSUSeconds where + coseries rs = newtypeAlts rs >>- \f -> return $ \l -> case l of CSUSeconds x -> f x +#endif + +-- }}} diff --git a/Test/SmallCheck/SeriesMonad.hs b/Test/SmallCheck/SeriesMonad.hs new file mode 100644 --- /dev/null +++ b/Test/SmallCheck/SeriesMonad.hs @@ -0,0 +1,77 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE NoImplicitPrelude #-} +#if __GLASGOW_HASKELL__ >= 704 +{-# LANGUAGE Safe #-} +#endif + +module Test.SmallCheck.SeriesMonad where + +import Control.Applicative (Applicative, Alternative, (<$>), pure, (<*>), empty, (<|>)) +import Control.Arrow (second) +import Control.Monad (Monad, (>>=), return, MonadPlus, mzero, mplus) +import Control.Monad.Logic (MonadLogic, LogicT, msplit) +import Control.Monad.Reader (MonadTrans, ReaderT, runReaderT, lift) +import Data.Function ((.), ($)) +import Data.Functor (Functor, fmap) +import Data.Int (Int) + +-- | Maximum depth of generated test values. +-- +-- For data values, it is the depth of nested constructor applications. +-- +-- For functional values, it is both the depth of nested case analysis +-- and the depth of results. +-- +-- @since 0.6 +type Depth = Int + +-- | 'Series' is a `MonadLogic` action that enumerates values of a certain +-- type, up to some depth. +-- +-- The depth bound is tracked in the 'Series' monad and can be extracted using +-- 'Test.SmallCheck.Series.getDepth' and changed using 'Test.SmallCheck.Series.localDepth'. +-- +-- To manipulate series at the lowest level you can use its 'Monad', +-- 'MonadPlus' and 'MonadLogic' instances. This module provides some +-- higher-level combinators which simplify creating series. +-- +-- A proper 'Series' should be monotonic with respect to the depth — i.e. +-- 'Test.SmallCheck.Series.localDepth' @(+1)@ @s@ should emit all the values that @s@ emits (and +-- possibly some more). +-- +-- It is also desirable that values of smaller depth come before the values +-- of greater depth. +-- +-- @since 1.0 +newtype Series m a = Series (ReaderT Depth (LogicT m) a) + +instance Functor (Series m) where + fmap f (Series x) = Series (fmap f x) + +instance Monad (Series m) where + Series x >>= f = Series (x >>= unSeries . f) + where + unSeries (Series y) = y + return = pure + +instance Applicative (Series m) where + pure = Series . pure + Series x <*> Series y = Series (x <*> y) + +instance MonadPlus (Series m) where + mzero = empty + mplus = (<|>) + +instance Alternative (Series m) where + empty = Series empty + Series x <|> Series y = Series (x <|> y) + +-- This instance is written manually. Using the GND for it is not safe. +instance Monad m => MonadLogic (Series m) where + msplit (Series a) = Series (fmap (second Series) <$> msplit a) + +instance MonadTrans Series where + lift a = Series $ lift . lift $ a + +runSeries :: Depth -> Series m a -> LogicT m a +runSeries d (Series a) = runReaderT a d diff --git a/examples/binarytries/BinaryTries.hs b/examples/binarytries/BinaryTries.hs deleted file mode 100644 --- a/examples/binarytries/BinaryTries.hs +++ /dev/null @@ -1,79 +0,0 @@ -------------------------------------------------- --- Binary tries representing sets of bitstrings. --- A test module for SmallCheck. --- Colin Runciman, May 2008. -------------------------------------------------- - -module BinaryTries where - -import Test.SmallCheck -import Test.SmallCheck.Series - --- first representation - -data BT1 = E | B Bool BT1 BT1 deriving Show - -instance Serial BT1 where - series = cons0 E \/ cons3 B - - -contains1 :: BT1 -> [Bool] -> Bool -contains1 E _ = False -contains1 (B b _ _) [] = b -contains1 (B _ z _) (False:s) = contains1 z s -contains1 (B _ _ o) (True :s) = contains1 o s - -prop_uniqueBT1 :: ([Bool]->Bool) -> Property -prop_uniqueBT1 f = - exists1DeeperBy (+1) $ \bt -> contains1 bt === f - --- second representation - -data BT2 = E2 | NE BT2' - deriving Show - -data BT2' = T | O Bool BT2' | I Bool BT2' | OI Bool BT2' BT2' - deriving Show - -instance Serial BT2 where - series = cons0 E2 \/ cons1 NE - -instance Serial BT2' where - series = cons0 T \/ cons2 O \/ cons2 I \/ cons3 OI - -contains2 :: BT2 -> [Bool] -> Bool -contains2 = contains1 . convert - -convert :: BT2 -> BT1 -convert E2 = E -convert (NE bt') = convert' bt' - -convert' :: BT2' -> BT1 -convert' T = B True E E -convert' (O b z') = B b (convert' z') E -convert' (I b o' ) = B b E (convert' o') -convert' (OI b o' z') = B b (convert' z') (convert' o') - -prop_uniqueBT2 :: ([Bool]->Bool) -> Property -prop_uniqueBT2 f = - exists1DeeperBy (+1) $ \bt -> contains2 bt === f - -(===) :: Eq b => (a->b) -> (a->b) -> a -> Bool -f === g = \x -> f x == g x - -main :: IO () -main = do - test1 "\\f -> exists1DeeperBy (+1) $ \\bt1 -> contains1 bt1 === f ?" - prop_uniqueBT1 - test1 "\\f -> exists1DeeperBy (+1) $ \\bt1 -> contains2 bt2 === f ?" - prop_uniqueBT2 - -test1 :: Testable a => String -> a -> IO () -test1 s t = do - rule - putStrLn s - rule - smallCheck 2 t - where - rule = putStrLn "----------------------------------------------------------" - diff --git a/examples/binarytries/README b/examples/binarytries/README deleted file mode 100644 --- a/examples/binarytries/README +++ /dev/null @@ -1,10 +0,0 @@ -First see ../../README. - -In this directory, BinaryTries.hs illustrates properties quantified -over functions and requiring the unique existence of a data-structure. -Two different trie representations are defined for sets of bitstrings. -The properties state that each set has a unique representation as a -trie -- true for the second representation, but not for the first. -The properties are specified using functions with boolean results -as a pure representation of sets, independent of any data structure. -Compile or interpret BinaryTries.main for the self-introducing tests. diff --git a/examples/circuits/BitAdd.hs b/examples/circuits/BitAdd.hs deleted file mode 100644 --- a/examples/circuits/BitAdd.hs +++ /dev/null @@ -1,23 +0,0 @@ -import Test.SmallCheck - -and2 (a,b) = a && b - -xor2 (a,b) = a /= b - -halfAdd (a,b) = (sum,carry) - where sum = xor2 (a,b) - carry = and2 (a,b) - -bit False = 0 -bit True = 1 - -num [] = 0 -num (a:as) = bit a + 2 * num as - -bitAdd a [] = [a] -bitAdd a (b:bs) = s : bitAdd c bs - where (s,c) = halfAdd (a,b) - -prop_bitAdd a as = num (bitAdd a as) == bit a + num as - -main = smallCheck 8 prop_bitAdd diff --git a/examples/circuits/Mux.hs b/examples/circuits/Mux.hs deleted file mode 100644 --- a/examples/circuits/Mux.hs +++ /dev/null @@ -1,114 +0,0 @@ -import List -import Test.SmallCheck -import Test.SmallCheck.Series - -type Bit = Bool - -unaryMux :: [Bit] -> [[Bit]] -> [Bit] -unaryMux sel xs = map (tree (||)) - $ transpose - $ zipWith (\s x -> map (s &&) x) sel xs - -tree :: (a -> a -> a) -> [a] -> a -tree f [x] = x -tree f (x:y:ys) = tree f (ys ++ [f x y]) - -decode :: [Bit] -> [Bit] -decode [] = [True] -decode [x] = [not x,x] -decode (x:xs) = concatMap (\y -> [not x && y,x && y]) rest - where - rest = decode xs - -binaryMux :: [Bit] -> [[Bit]] -> [Bit] -binaryMux sel xs = unaryMux (decode sel) xs - -bitMux2 :: Bit -> Bit -> Bit -> Bit -bitMux2 sel x y = (sel && y) || (not sel && x) - -muxf5 = bitMux2 - -muxf6 = bitMux2 - -busMux2 :: Bit -> [Bit] -> [Bit] -> [Bit] -busMux2 sel xs ys = zipWith (bitMux2 sel) xs ys - -bitMux8 :: [Bit] -> [Bit] -> Bit -bitMux8 _ [x] = x -bitMux8 (s0:_) [x0,x1] - = bitMux2 s0 x0 x1 -bitMux8 (s0:s1:_) [x0,x1,x2,x3] - = muxf5 s1 (bitMux8 [s0] [x0,x1]) (bitMux8 [s0] [x2,x3]) -bitMux8 (s0:s1:s2:_) [x0,x1,x2,x3,x4,x5,x6,x7] - = muxf6 s2 (bitMux8 [s0,s1] [x0,x1,x2,x3]) - (bitMux8 [s0,s1] [x4,x5,x6,x7]) -bitMux8 sels xs = bitMux8 (take n sels) (pad m xs) - where - n = log2 (length xs) - m = 2 ^ n - -log2 :: Int -> Int -log2 n = length (takeWhile (< n) (iterate (*2) 1)) - -pad :: Int -> [Bit] -> [Bit] -pad n xs | m > n = xs - | otherwise = xs ++ replicate (n-m) False - where - m = length xs - -bitMux :: [Bit] -> [Bit] -> Bit -bitMux sels [x] = x -bitMux sels xs = bitMux (drop 3 sels) ys - where - ys = zipWith bitMux8 (repeat (take 3 sels)) (groupn 8 xs) - - -groupn :: Int -> [a] -> [[a]] -groupn n [] = [] -groupn n xs = take n xs : groupn n (drop n xs) - -binaryMux' :: [Bit] -> [[Bit]] -> [Bit] -binaryMux' sel = map (bitMux sel) . transpose - -num :: [Bit] -> Int -num [] = 0 -num (a:as) = fromEnum a + 2 * num as - --- Property 0: binaryMux is correct - -prop_mux0 sel xs = length xs == 2 ^ length sel - && all ((== length (head xs)) . length) xs - ==> binaryMux sel xs == xs !! num sel - --- But this is inefficient as most of the test cases do not meet the --- antecedent. Instead, we can define a custom generator in which --- the number of inputs grows exponentially (i.e. 2^) with respect to --- the width of the address word. - -newtype Word = Word { bits :: [Bit] } - deriving Show - -newtype File = File { wrds :: [Word] } - deriving Show - -instance Serial Word where - series n = map Word $ sequence (replicate n [False,True]) - -instance Serial File where - series n = map File $ sequence $ replicate (2^n) ws - where - ws = series n :: [Word] - -prop_mux0' sel xs = xs' !! num sel' == binaryMux sel' xs' - where - sel' = bits sel - xs' = map bits (wrds xs) - --- Property 1: binaryMux' is correct - -prop_mux1 sel xs = xs' !! num sel' == binaryMux' sel' xs' - where - sel' = bits sel - xs' = map bits (wrds xs) - -main = smallCheck 2 prop_mux1 diff --git a/examples/circuits/README b/examples/circuits/README deleted file mode 100644 --- a/examples/circuits/README +++ /dev/null @@ -1,30 +0,0 @@ -First see ../../README. - -The programs in this directory define a number of different circuits. -Some of these were originally written in Lava and were used to generate -circuit netlists for external synthesis tools and propositional logic for -external theorem provers. They have been slightly adapted as examples -for SmallCheck, so that they do not depend on Lava. - -BitAdd.hs defines a trivial circuit that takes two inputs, a bit and a -bit-vector (i.e. a list of bits), and returns a bit-vector containing -the sum of the two. Using SmallCheck, it is straightforward to verify -that the circuit behaves correctly for all bit-vector inputs up to the -given size. - -Sad.hs defines a more complicated circuit that works over two lists of -lists of bits, but verification with SmallCheck is just as simple and -useful as before. - -Mux.hs defines a simple multiplexor and a more complicated variant that -is optimised for Xilinx FPGAs. Originally, the correctness of the more -complicated version was argued by verifying its equivalence with the -simpler version using an external SAT solver. However, using SmallCheck, -more general properties can be expressed, and so each circuit can be -verified independently in terms of Haskell's list indexing operator (!!). -The correctness properties are again easy to express in SmallCheck, -but their antecedents filter out so many test cases as to make them -inefficient. This problem is resolved by writing a custom test-case -generator using SmallCheck's "Serial" class. - -Matthew Naylor, University of York, 22nd Jan 2007. diff --git a/examples/circuits/Sad.hs b/examples/circuits/Sad.hs deleted file mode 100644 --- a/examples/circuits/Sad.hs +++ /dev/null @@ -1,96 +0,0 @@ -import Test.SmallCheck - --- We take the following specification for the sum of absolute --- differences, and develop a circuit generator that has the same --- behaviour. - -sad :: [Int] -> [Int] -> Int -sad xs ys = sum (map abs (zipWith (-) xs ys)) - -type Bit = Bool - -low :: Bit -low = False - -high :: Bit -high = True - -inv :: Bit -> Bit -inv a = not a - -and2 :: Bit -> Bit -> Bit -and2 a b = a && b -or2 a b = a || b -xor2 a b = a /= b -xnor2 a b = a == b - -mux2 :: Bit -> Bit -> Bit -> Bit -mux2 sel a b = (sel && b) || (not sel && a) - -bitAdd :: Bit -> [Bit] -> [Bit] -bitAdd x [] = [x] -bitAdd x (y:ys) = let (sum,carry) = halfAdd x y - in sum:bitAdd carry ys - -halfAdd x y = (xor2 x y,and2 x y) - -binAdd :: [Bit] -> [Bit] -> [Bit] -binAdd xs ys = binAdd' low xs ys - -binAdd' cin [] [] = [cin] -binAdd' cin (x:xs) [] = bitAdd cin (x:xs) -binAdd' cin [] (y:ys) = bitAdd cin (y:ys) -binAdd' cin (x:xs) (y:ys) = let (sum,cout) = fullAdd cin x y - in sum:binAdd' cout xs ys - -fullAdd cin a b = let (s0,c0) = halfAdd a b - (s1,c1) = halfAdd cin s0 - in (s1,xor2 c0 c1) - -binGte :: [Bit] -> [Bit] -> Bit -binGte xs ys = binGte' high xs ys - -binGte' gin [] [] = gin -binGte' gin (x:xs) [] = orl (gin:x:xs) -binGte' gin [] (y:ys) = and2 gin (orl (y:ys)) -binGte' gin (x:xs) (y:ys) = let gout = gteCell gin x y - in binGte' gout xs ys - -gteCell gin x y = mux2 (xnor2 x y) x gin - -orl :: [Bit] -> Bit -orl xs = tree or2 low xs - -binDiff :: [Bit] -> [Bit] -> [Bit] -binDiff xs ys = let xs' = pad (length ys) xs - ys' = pad (length xs) ys - gte = binGte xs' ys' - xs'' = map (xor2 (inv gte)) xs' - ys'' = map (xor2 gte) ys' - in init (binAdd' high xs'' ys'') - -pad :: Int -> [Bit] -> [Bit] -pad n xs | m > n = xs - | otherwise = xs ++ replicate (n-m) False - where - m = length xs - -tree :: (a -> a -> a) -> a -> [a] -> a -tree f z [] = z -tree f z [x] = x -tree f z (x:y:ys) = tree f z (ys ++ [f x y]) - -binSum :: [[Bit]] -> [Bit] -binSum xs = tree binAdd [] xs - -binSad :: [[Bit]] -> [[Bit]] -> [Bit] -binSad xs ys = binSum (zipWith binDiff xs ys) - -num :: [Bit] -> Int -num [] = 0 -num (a:as) = fromEnum a + 2 * num as - -prop_binSad xs ys = sad (map num xs) (map num ys) - == num (binSad xs ys) - -main = smallCheck 3 prop_binSad diff --git a/examples/imperative/Behaviour.hs b/examples/imperative/Behaviour.hs deleted file mode 100644 --- a/examples/imperative/Behaviour.hs +++ /dev/null @@ -1,23 +0,0 @@ -module Behaviour(Trace(..),(+++),approx) where - -data Trace a - = Step (Trace a) - | a :> Trace a - | End - | Crash - deriving (Eq, Show) - -(+++) :: Trace a -> Trace a -> Trace a -Step s +++ t = Step (s +++ t) -(x :> s) +++ t = x :> (s +++ t) -End +++ t = t -Crash +++ t = Crash - -approx :: Eq a => Int -> Trace a -> Trace a -> Bool -approx 0 _ _ = True -approx n (a :> s) (b :> t) = a == b && approx (n-1) s t -approx n (Step s) (Step t) = approx (n-1) s t -approx n End End = True -approx n Crash Crash = True -approx n _ _ = False - diff --git a/examples/imperative/Compiler.hs b/examples/imperative/Compiler.hs deleted file mode 100644 --- a/examples/imperative/Compiler.hs +++ /dev/null @@ -1,59 +0,0 @@ -module Compiler(compile) where - -import Machine -import Syntax -import StackMap -import Value - -compile :: Command -> [Instruction] -compile c = - replicate (depth sm) (Push Wrong) ++ - compObey sm c ++ - [Halt] - where - sm = stackMap c - -compObey :: StackMap -> Command -> [Instruction] -compObey sm Skip = - [] -compObey sm (v := e) = - compEval sm e ++ - [Store (location sm v + 1)] -compObey sm (c1 :-> c2) = - compObey sm c1 ++ - compObey sm c2 -compObey sm (If e c1 c2) = - compEval sm e ++ - [JumpUnless (length isc1 + 1)] ++ - isc1 ++ - [Jump (length isc2)] ++ - isc2 - where - isc1 = compObey sm c1 - isc2 = compObey sm c2 -compObey sm (While e c) = - ise ++ - [JumpUnless (length isc + 1)] ++ - isc ++ - [Jump (negate (length isc + 1 + length ise + 1))] - where - ise = compEval sm e - isc = compObey sm c -compObey sm (Print e) = - compEval sm e ++ - [Display] - -compEval :: StackMap -> Expr -> [Instruction] -compEval sm (Val v) = - [Push v] -compEval sm (Var v) = - [Fetch (location sm v)] -compEval sm (Uno op1 e) = - -- was op before arg eval - compEval sm e ++ - [Instr1 op1] -compEval sm (Duo op2 e1 e2) = - -- was op before arg evals - compEval sm e1 ++ - compEval (push sm) e2 ++ - [Instr2 op2] diff --git a/examples/imperative/Interpreter.hs b/examples/imperative/Interpreter.hs deleted file mode 100644 --- a/examples/imperative/Interpreter.hs +++ /dev/null @@ -1,41 +0,0 @@ -module Interpreter(obey) where - -import Syntax -import Behaviour -import Value - -type Env = [(Name,Value)] - -obey :: Command -> Trace Value -obey p = fst (run p []) - -look :: Name -> Env -> Value -look x s = maybe Wrong id (lookup x s) - -update :: Name -> Value -> Env -> Env -update x a s = (x,a) : filter (\(y,_) -> y/=x) s - -run :: Command -> Env -> (Trace Value, Env) -run Skip s = (End, s) -run (x := e) s = (End, update x (eval e s) s) -run (p :-> q) s = let (outp, sp) = run p s - (outq, sq) = run q sp - in (outp +++ outq, sq) -run (If e p q) s = case eval e s of - -- was True -> q, False -> p - Log True -> run p s - Log False -> run q s - _ -> (Crash, s) -run (While e p) s = case eval e s of - Log True -> let (outp,sp) = run p s - (outw,sw) = run (While e p) sp - in (outp +++ Step outw, sw) - Log False -> (End, s) - _ -> (Crash, s) -run (Print e) s = (eval e s :> End, s) - -eval :: Expr -> Env -> Value -eval (Var x) s = look x s -eval (Val v) s = v -eval (Uno op a) s = uno op (eval a s) -eval (Duo op a b) s = duo op (eval a s) (eval b s) diff --git a/examples/imperative/Machine.hs b/examples/imperative/Machine.hs deleted file mode 100644 --- a/examples/imperative/Machine.hs +++ /dev/null @@ -1,50 +0,0 @@ -module Machine(Instruction(..), exec) where - -import Array -import Behaviour -import Value - -data Instruction - = Push Value - | Pop - | Fetch Int - | Store Int - | Instr1 Op1 - | Instr2 Op2 - | Display - | Jump Int - | JumpUnless Int - | Halt - deriving (Eq, Show) - -exec :: [Instruction] -> Trace Value -exec instrs = run 1 [] - where - size = length instrs - memory = array (1,size) ([1..] `zip` instrs) - run pc stack = - if pc < 1 || size < pc then Crash - else - case (memory ! pc, stack) of - (Push x , stack) -> run pc' (x : stack) - (Pop , _ : stack) -> run pc' stack - (Fetch n , stack) - | length stack > n -> run pc' (stack !! n : stack) - (Store n , x : stack) - | length stack >= n -> run pc' (take (n-1) stack ++ - x : drop n stack) - (Instr1 op1 , i : stack) -> run pc' (uno op1 i : stack) - (Instr2 op2 , i : j : stack) -> run pc' (duo op2 j i : stack) - (Display , i : stack) -> i :> run pc' stack - (Jump n , stack) -> step n (run (pc' + n) stack) - (JumpUnless n , Log b : stack) - | b -> run pc' stack - | otherwise -> step n (run (pc' + n) stack) - (Halt , stack) -> End - _ -> Crash - where - pc' = pc + 1 - -step :: Int -> Trace Value -> Trace Value -step n t | n < 0 = Step t - | otherwise = t diff --git a/examples/imperative/Properties.hs b/examples/imperative/Properties.hs deleted file mode 100644 --- a/examples/imperative/Properties.hs +++ /dev/null @@ -1,178 +0,0 @@ -import Behaviour -import Interpreter -import Compiler -import Machine -import Syntax -import Value - -import Test.SmallCheck - -------------- ------------- - --- In the abstract syntax variables are just strings, --- but we do not want to enumerate all lists of characters. --- Just a couple of distinct names. - -newtype VarName = VarName Name - -instance Serial VarName where - series = const [VarName [c] | c <- ['a'..'b']] - -var :: VarName -> Expr -var (VarName v) = Var v - -assign :: VarName -> Expr -> Command -assign (VarName v) e = (v := e) - --- Uses of depth 0 ensure that all occurrences of variables --- or literals are treated as zero-depth atoms. --- The rest is completely standard, but for the use of --- 'var' for Var and 'assign' for Assign. - -instance Serial Value where - series = cons0 Wrong - \/ cons1 Log . depth 0 - \/ cons1 Num . depth 0 - -instance Serial Op1 where - series = const [Not, Minus] - -instance Serial Op2 where - series = const [And, Or, Eq, Less, LessEq, - Add, Sub, Mul, Div, Mod] - -instance Serial Expr where - series = cons1 var . depth 0 - \/ cons1 Val . depth 0 - \/ cons2 Uno - \/ cons3 Duo - -instance Serial Command where - series = cons0 Skip - \/ cons1 Print - \/ cons2 assign - \/ cons2 (:->) - \/ cons3 If - \/ cons2 While - ------------------ ------------------- - --- If we want a series for a subset of the values in --- a given type, one way to define it is via a newtype. --- Here, expressions without variables. - -newtype ClosedExpr = Closed Expr deriving Show - -instance Serial ClosedExpr where - series = cons1 val . depth 0 - \/ cons2 uno - \/ cons3 duo - where - val v = Closed (Val v) - uno op (Closed e) = Closed (Uno op e) - duo op (Closed e1) (Closed e2) = Closed (Duo op e1 e2) - ------------------ ----------------- - --- The space of all commands grows very quickly with depth, --- and many syntactically legal commands are bound to fail. --- Here we define a restricted subset of commands in a --- 'standard form': --- -- Skip only occurs as an else-alternative --- -- Print is only applied to simple variables --- -- Only integer values are assigned to variables. --- -- If and While conditions are compound comparisons. - -newtype StdCommand = Std Command deriving Show - -instance Serial StdCommand where - series = cons1 print' - \/ cons2 assign' - \/ cons2 seq' - \/ cons3 if' - \/ cons2 while' - where - print' (VarName v) = Std (Print (Var v)) - assign' (VarName v) (I e) = Std (v := e) - seq' (Std c0) (Std c1) = Std (c0 :-> c1) - if' (B e) (Std c0) (SkipOrStd c1) = Std (If e c0 c1) - while' (B e) (Std c) = Std (While e c) - -newtype SkipOrStdCommand = SkipOrStd Command - -instance Serial SkipOrStdCommand where - series = cons0 skip - \/ cons1 std . depth 0 - where - skip = SkipOrStd Skip - std (Std c) = SkipOrStd c - -newtype IExpr = I Expr - -instance Serial IExpr where - series = cons1 var' . depth 0 - \/ cons1 val' . depth 0 - \/ cons1 uno' - \/ cons3 duo' - where - var' (VarName v) = I (Var v) - val' i = I (Val (Num i)) - uno' (I e) = I (Uno Minus e) - duo' (I2 d) (I e0) (I e1) = I (Duo d e0 e1) - -newtype IOp2 = I2 Op2 - -instance Serial IOp2 where - series = const [I2 op | op <- [Add, Sub, Mul, Div, Mod]] - -newtype BExpr = B Expr - -instance Serial BExpr where - series = cons1 uno' - \/ cons3 duo' - \/ cons3 cmp' - where - uno' (B e) = B (Uno Not e) - duo' (B2 d) (B e0) (B e1) = B (Duo d e0 e1) - cmp' (C2 c) (I e0) (I e1) = B (Duo c e0 e1) - -newtype BOp2 = B2 Op2 - -instance Serial BOp2 where - series = const [B2 op | op <- [And,Or]] - -newtype COp2 = C2 Op2 - -instance Serial COp2 where - series = const [C2 op | op <- [Eq,Less,LessEq]] - --------- -------- - -newtype Approx = Approx Int deriving Show - -instance Serial Approx where - series d = [Approx d] - -(=~=) :: Eq a => Trace a -> Trace a -> Approx -> Bool -s =~= t = \(Approx d) -> approx d s t - ------------------ ------------------ - -prop_Congruence :: Command -> Property -prop_Congruence p = - t1 /= Crash || t2 /= Crash ==> - (t1 =~= t2) - where - t1 = obey p - t2 = exec (compile p) - -prop_StdCongruence :: StdCommand -> Property -prop_StdCongruence (Std p) = - prop_Congruence p - -main :: IO () -main = do - putStrLn "-- congruence for all programs:" - smallCheck 2 prop_Congruence - putStrLn "-- congruence for standard-form programs:" - smallCheck 2 prop_StdCongruence diff --git a/examples/imperative/README b/examples/imperative/README deleted file mode 100644 --- a/examples/imperative/README +++ /dev/null @@ -1,10 +0,0 @@ -First see ../../README. - -This directory gives the largest illustrative example. We test for -congruence between an interpreter and compiler for a small imperative -language. The example is adapted from an original using QuickCheck, -as described in the lecture notes for AFP'02 (LNCS 2638). Compared -with the simpler example in ../logic, here specialised instances -are used to restrict the input space to programs in a standard form. -Run Properties.main and compare the rate of growth for the last two -properties tested. diff --git a/examples/imperative/StackMap.hs b/examples/imperative/StackMap.hs deleted file mode 100644 --- a/examples/imperative/StackMap.hs +++ /dev/null @@ -1,35 +0,0 @@ -module StackMap where - -import Syntax -import List( union ) - -type StackMap = (Int,[Name]) - -stackMap :: Command -> StackMap -stackMap c = (0, comVars c) - -push :: StackMap -> StackMap -push (n, vars) = (n+1, vars) - -pop :: StackMap -> StackMap -pop (n, vars) = (n-1, vars) - -location :: StackMap -> Name -> Int -location (n, vars) v = n + length (takeWhile (/=v) vars) - -depth :: StackMap -> Int -depth (n, vars) = n + length vars - -expVars :: Expr -> [Name] -expVars (Var v) = [v] -expVars (Val _) = [] -expVars (Uno _ a) = expVars a -expVars (Duo _ a b) = expVars a `union` expVars b - -comVars :: Command -> [Name] -comVars Skip = [] -comVars (x := e) = [x] `union` expVars e -comVars (c1 :-> c2) = comVars c1 `union` comVars c2 -comVars (If e c1 c2) = expVars e `union` comVars c1 `union` comVars c2 -comVars (While e c) = expVars e `union` comVars c -comVars (Print e) = expVars e diff --git a/examples/imperative/Syntax.hs b/examples/imperative/Syntax.hs deleted file mode 100644 --- a/examples/imperative/Syntax.hs +++ /dev/null @@ -1,21 +0,0 @@ -module Syntax(Name, Expr(..), Command(..)) where - -import Value - -type Name = String - -data Expr - = Var Name - | Val Value - | Uno Op1 Expr - | Duo Op2 Expr Expr - deriving (Eq, Show) - -data Command - = Skip - | Name := Expr - | Command :-> Command - | If Expr Command Command - | While Expr Command - | Print Expr - deriving (Eq, Show) diff --git a/examples/imperative/Value.hs b/examples/imperative/Value.hs deleted file mode 100644 --- a/examples/imperative/Value.hs +++ /dev/null @@ -1,44 +0,0 @@ -module Value(Value(..), Op1(..), Op2(..), uno, duo) where - -data Value - = Num Int - | Log Bool - | Wrong - deriving (Eq, Show) - -data Op1 - = Not - | Minus - deriving (Eq, Show) - -data Op2 - = And - | Or - | Mul - | Add - | Sub - | Div - | Mod - | Less - | LessEq - | Eq - deriving (Eq, Show) - -uno :: Op1 -> Value -> Value -uno Not (Log b) = Log (not b) -uno Minus (Num n) = Num (negate n) -uno _ _ = Wrong - -duo :: Op2 -> Value -> Value -> Value -duo And (Log a) (Log b) = Log (a && b) -duo Or (Log a) (Log b) = Log (a || b) -duo Eq (Log a) (Log b) = Log (a == b) -duo Mul (Num m) (Num n) = Num (m * n) -duo Add (Num m) (Num n) = Num (m + n) -duo Sub (Num m) (Num n) = Num (m - n) -duo Div (Num m) (Num n) | n /= 0 = Num (m `div` n) -duo Mod (Num m) (Num n) | n /= 0 = Num (m `mod` n) -duo Less (Num m) (Num n) = Log (m < n) -duo LessEq (Num m) (Num n) = Log (m <= n) -duo Eq (Num m) (Num n) = Log (m == n) -duo _ _ _ = Wrong diff --git a/examples/listy/ListProps.hs b/examples/listy/ListProps.hs deleted file mode 100644 --- a/examples/listy/ListProps.hs +++ /dev/null @@ -1,92 +0,0 @@ ------------------------------------------------- --- Properties (some valid some invalid) of a few --- standard list-processing functions. --- A test module for SmallCheck. --- Colin Runciman, August 2006. --- Revised for 0.2, November 2006. ------------------------------------------------- - -module ListProps where - -import Test.SmallCheck - --- properties about higher-order functions --- plausible-looking but invalid laws about folds - -prop_fold1 :: [Bool] -> Property -prop_fold1 xs = - not (null xs) ==> - \f -> foldl1 f xs == foldr1 f xs - -prop_fold2 :: [Bool] -> [Bool] -> Property -prop_fold2 xs ys = - not (null xs) && not (null ys) ==> - \f -> foldr1 f xs `f` foldr1 f ys == foldr1 f (xs++ys) - --- properties using 'exists' with data and functional arguments - --- invalid because depth-bound for zs same as for xs ys -prop_union1 :: [Bool] -> [Bool] -> Property -prop_union1 xs ys = - exists $ \zs -> - \b -> (b `elem` zs) == (b `elem` xs || b `elem` ys) - --- valid variant: depth-bound doubled in existential -prop_union2 :: [Bool] -> [Bool] -> Property -prop_union2 xs ys = - existsDeeperBy (*2) $ \zs -> - \b -> (b `elem` zs) == (b `elem` xs || b `elem` ys) - --- do magical span arguments exist? -prop_span1 :: [Bool] -> [Bool] -> [Bool] -> Property -prop_span1 xs ys zs = - xs++ys == zs ==> exists $ \t -> (xs,ys) == span t zs - --- deliberate mistake in final isPrefix equation -isPrefix :: Ord a => [a] -> [a] -> Bool -isPrefix [] ys = True -isPrefix (x:xs) [] = False -isPrefix (x:xs) (y:ys) = x==y || isPrefix xs ys - --- this completeness property still holds -isPrefixComplete :: String -> String -> Bool -isPrefixComplete xs ys = - isPrefix xs (xs ++ ys) - --- but this existential soundness property fails -isPrefixSound :: String -> String -> Property -isPrefixSound xs ys = isPrefix xs ys ==> - exists $ \xs' -> ys == (xs ++ xs') - -main :: IO () -main = do - test1 "\\xs -> not (null xs) ==>\n\ - \ \\f -> foldl1 f xs == foldr1 f xs ?" - prop_fold1 - test1 "\\xs ys -> not (null xs) && not (null ys) ==>\n \ - \ \\f -> foldr1 f xs `f` foldr1 f ys == foldr1 f (xs++ys) ?" - prop_fold2 - test1 "\\xs ys -> exists $ \\zs ->\n\ - \ \\b -> (b `elem` zs) == (b `elem` xs || b `elem` ys) ?" - prop_union1 - test1 "\\xs ys -> existsDeeperBy (*2) $ \\zs ->\n\ - \ \\b -> (b `elem` zs) == (b `elem` xs || b `elem` ys) ?" - prop_union2 - test1 "\\xs ys zs -> xs++ys==zs ==>\n\ - \ exists $ \\t -> (xs,ys) == span t zs ?" - prop_span1 - test1 "\\xs ys -> isPrefix xs (xs++ys) ?" - isPrefixComplete - test1 "\\xs ys zs -> isPrefix xs ys ==>\n\ - \ exists $ \\xs' -> ys == xs ++ xs' ?" - isPrefixSound - -test1 :: Testable a => String -> a -> IO () -test1 s t = do - rule - putStrLn s - rule - smallCheck 4 t - where - rule = putStrLn "----------------------------------------------------" - diff --git a/examples/listy/README b/examples/listy/README deleted file mode 100644 --- a/examples/listy/README +++ /dev/null @@ -1,8 +0,0 @@ -First see ../../README. - -In this directory, compile or interpret ListProps.main (SmallCheck is -the only other module required) for a small selection of self-introducing -tests of list-processing functions. - -The definition of isPrefix is deliberately incorrect: the completeness -property still holds, but the existential soundness property fails. diff --git a/examples/logical/LogicProps.hs b/examples/logical/LogicProps.hs deleted file mode 100644 --- a/examples/logical/LogicProps.hs +++ /dev/null @@ -1,129 +0,0 @@ ----------------------------------------------------- --- Propositional formulae, satisfiable, tautologous. --- A test module for SmallCheck. --- Colin Runciman, August 2006. ----------------------------------------------------- - -module PropLogic where - -import Test.SmallCheck -import Test.SmallCheck.Series - -import List (nub) - -data Prop = Var Name - | Not Prop - | And Prop Prop - | Or Prop Prop - | Imp Prop Prop - -instance Show Prop where - show p = case p of - Var n -> show n - Not q -> "~"++show' q - And q r -> show' q++"&"++show' r - Or q r -> show' q++"|"++show' r - Imp q r -> show' q++"=>"++show' r - where - show' x = if priority p > priority x then "("++show x++")" - else show x - priority (Var _) = 5 - priority (Not _) = 4 - priority (And _ _) = 3 - priority (Or _ _) = 2 - priority (Imp _ _) = 1 - -data Name = P | Q | R deriving (Eq,Show) - -type Env = Name -> Bool - -eval :: Prop -> Env -> Bool -eval (Var v) env = env v -eval (Not p) env = not (eval p env) -eval (And p q) env = eval p env && eval q env -eval (Or p q) env = eval p env || eval q env -eval (Imp p q) env = eval p env <= eval q env - -envsFor :: Prop -> [Env] -envsFor p = foldr bind [const False] (nub (varsOf p)) - where - bind v es = concat [ [\x -> x==v || e x, e] - | e <- es ] - -varsOf :: Prop -> [Name] -varsOf (Var v) = [v] -varsOf (Not p) = varsOf p -varsOf (And p q) = varsOf p ++ varsOf q -varsOf (Or p q) = varsOf p ++ varsOf q -varsOf (Imp p q) = varsOf p ++ varsOf q - -tautologous :: Prop -> Bool -tautologous p = all (eval p) (envsFor p) - -satisfiable :: Prop -> Bool -satisfiable p = any (eval p) (envsFor p) - -instance Serial Name where - series = cons0 P \/ cons0 Q \/ cons0 R - coseries rs d = [ \n -> case n of - P -> x ; Q -> y ; R -> z - | x <- alts0 rs d, y <- alts0 rs d, z <- alts0 rs d ] - -instance Serial Prop where - series = cons1 Var - \/ cons1 Not - \/ cons2 And - \/ cons2 Or - \/ cons2 Imp - ----------------------- --------------------- - -prop_taut1 :: Prop -> Property -prop_taut1 p = - tautologous p ==> \e -> eval p e - -prop_taut2 :: Prop -> Property -prop_taut2 p = - not (tautologous p) ==> exists (\e -> not $ eval p e) - -prop_sat1 :: Prop -> Env -> Property -prop_sat1 p e = - eval p e ==> satisfiable p - -prop_sat2 :: Prop -> Property -prop_sat2 p = - satisfiable p ==> exists (\e -> eval p e) - -prop_tautSat1 :: Prop -> Property -prop_tautSat1 p = - not (tautologous p) ==> satisfiable (Not p) - -prop_tautSat2 :: Prop -> Property -prop_tautSat2 p = - not (satisfiable p) ==> tautologous (Not p) - -main :: IO () -main = do - test1 "\\p -> tautologous p ==> \\e -> eval p e ?" - prop_taut1 - test1 "\\p -> not (tautologous p) ==>\n\ - \ exists (\\e -> not $ eval p e) ?" - prop_taut2 - test1 "\\p e -> eval p e ==> satisfiable p ?" - prop_sat1 - test1 "\\p -> satisfiable p ==> exists (\\e -> eval p e) ?" - prop_sat2 - test1 "\\p -> not (tautologous p) ==> satisfiable (Not p) ?" - prop_tautSat1 - test1 "\\p -> not (satisfiable p) ==> tautologous (Not p) ?" - prop_tautSat2 - -test1 :: Testable a => String -> a -> IO () -test1 s t = do - rule - putStrLn s - rule - smallCheck 3 t - where - rule = putStrLn "----------------------------------------------------" - diff --git a/examples/logical/README b/examples/logical/README deleted file mode 100644 --- a/examples/logical/README +++ /dev/null @@ -1,7 +0,0 @@ -First see ../../README. - -In this directory, LogicProps.hs illustrates the basic way to define -Serial instances of your own types, and hence Testable properties of -functions over them. Compile or interpret LogicProps.main (SmallCheck is -the only other module required) for a small selection of self-introducing -tests. diff --git a/examples/numeric/NumProps.hs b/examples/numeric/NumProps.hs deleted file mode 100644 --- a/examples/numeric/NumProps.hs +++ /dev/null @@ -1,64 +0,0 @@ ----------------------------------------- --- Illustrating numerics in SmallCheck --- Colin Runciman, November 2006. --- Modified for SmallCheck 0.3, May 2008 ----------------------------------------- - -import Test.SmallCheck -import Test.SmallCheck.Series -import Test.SmallCheck.Property - -primes :: [Int] -primes = sieve [2..] - where - sieve (p:xs) = - p : filter (noFactorIn primes) xs - noFactorIn (p:ps) x = - p*p > x || x `mod` p > 0 && noFactorIn ps x - --- using natural numbers - -prop_primes1 :: Nat -> Property -prop_primes1 (N n) = - n > 1 ==> forAll (`take` primes) $ \p -> - p `mod` n > 0 || n == p - -prop_primes2 :: Nat -> Property -prop_primes2 (N n) = - n > 0 ==> exists1 $ \exponents -> - (null exponents || last exponents /= N 0) && - n == product (zipWith power primes exponents) - where - power p (N e) = product (replicate e p) - --- using floating point numbers - -prop_logExp :: Float -> Bool -prop_logExp x = exp (log x) == x - -prop_recipRecip :: Float -> Bool -prop_recipRecip x = 1.0 / (1.0 / x) == x - -main :: IO () -main = do - test1 "\\(N n) -> n > 1 ==> forAll (`take` primes) $ \\p ->\n\ - \ p `mod` n > 0 || n == p" - prop_primes1 - test1 "\\(N n) -> n > 0 ==> exists1 $ \\exponents ->\n\ - \ (null exponents || last exponents /= N 0) &&\n\ - \ n == product (zipWith power primes exponents)" - prop_primes2 - test1 "\\x -> exp (log x) == x" - prop_logExp - test1 "\\x -> 1.0 / (1.0 / x) == x" - prop_recipRecip - -test1 :: Testable a => String -> a -> IO () -test1 s t = do - rule - putStrLn s - rule - smallCheck 8 t - where - rule = putStrLn "----------------------------------------------------" - diff --git a/examples/numeric/README b/examples/numeric/README deleted file mode 100644 --- a/examples/numeric/README +++ /dev/null @@ -1,14 +0,0 @@ -First see ../../README. - -In this directory, NumProps.hs illustrates the use of test series -for natural numbers, either by explicit signatures including Nat (or -Natural) or by use of the N constructor. It also illustrates use of -floating-point series. Compile or interpret NumProps (SmallCheck is -the only other module required) and run main for a small selection of -self-introducing tests -- a couple about natural numbers and primes, -and a couple about floating point numbers. - -For version 0.3 the second property about primes has been strengthened -by making the existence unique. The restriction on the exponent list -was prompted by reports of non-uniqueness when the 'exists1' version -was first tested. diff --git a/examples/regular/README b/examples/regular/README deleted file mode 100644 --- a/examples/regular/README +++ /dev/null @@ -1,8 +0,0 @@ -First see ../../README. - -In this directory, Regular.hs illustrates a test involving IO -- writing -and reading expressions to/from a file. The use of 'smart constructors' -in the series definition is necessary for the property to hold, but does -*not* reduce the number of tests -- rather, there are duplicated tests for -the same expressions generated in different ways. Compile or interpret -Regular.main for a self-introducing test. diff --git a/examples/regular/Regular.hs b/examples/regular/Regular.hs deleted file mode 100644 --- a/examples/regular/Regular.hs +++ /dev/null @@ -1,104 +0,0 @@ -module Regular where - -import Char (isAlpha) -import List (intersperse) -import Monad (liftM) - -import Test.SmallCheck -import Test.SmallCheck.Series - --- A data type of regular expressions. - -data RE = Emp - | Lam - | Sym Char - | Alt [RE] - | Cat [RE] - | Rep RE - deriving Eq - -isEmp, isLam, isSym, isCat, isAlt, isRep :: RE -> Bool -isEmp Emp = True -isEmp _ = False -isLam Lam = True -isLam _ = False -isSym (Sym _) = True -isSym _ = False -isAlt (Alt _) = True -isAlt _ = False -isCat (Cat _) = True -isCat _ = False -isRep (Rep _) = True -isRep _ = False - --- Syms may be used to represent terminals or variables. --- Using cat and alt instead of Cat and Alt ensures that: --- (1) Cat and Alt arguments are multi-item lists; --- (2) items in Cat arguments are not Cats; --- (3) items in Alt arguments are not Alts. - -cat :: [RE] -> RE -cat [] = Lam -cat [x] = x -cat xs = Cat (concatMap catList xs) - where - catList (Cat ys) = ys - catList z = [z] - -alt :: [RE] -> RE -alt [] = Emp -alt [x] = x -alt xs = Alt (concatMap altList xs) - where - altList (Alt ys) = ys - altList z = [z] - -instance Read RE where - readsPrec _ s = [rest s [[[]]]] - -rest :: String -> [[[RE]]] -> (RE,String) -rest "" ( a:as) = if null as then (a2re a,"") - else wrong -rest ('+':s) ((c:a):as) = if null c then wrong - else rest s (([]:c:a):as) -rest ('*':s) ((c:a):as) = case c of - [] -> wrong - (x:xs) -> rest s (((Rep x:xs):a):as) -rest ('0':s) ((c:a):as) = rest s (((Emp:c):a):as) -rest ('1':s) ((c:a):as) = rest s (((Lam:c):a):as) -rest ('(':s) as = rest s ([[]]:as) -rest (')':s) (a:as) = case as of - [] -> wrong - ((c:a'):as') -> rest s (((a2re a:c):a'):as') -rest (' ':s) as = rest s as -rest (v :s) ((c:a):as) = if isAlpha v then rest s (((Sym v:c):a):as) - else if null as then (a2re (c:a),v:s) - else wrong - -a2re :: [[RE]] -> RE -a2re = alt . reverse . map (cat . reverse) - -wrong = error "unreadable RE" - -instance Show RE where - show Emp = "0" - show Lam = "1" - show (Sym c) = [c] - show (Alt xs) = concat (intersperse "+" (map show xs)) - show (Cat xs) = concatMap (showBrackIf isAlt) xs - show (Rep x) = showBrackIf (\x -> isCat x || isAlt x) x ++ "*" - -showBrackIf p x = ['(' | q] ++ show x ++ [')' | q] where q = p x - -instance Serial RE where - series = cons0 Emp - \/ cons0 Lam - \/ cons1 Sym . depth 0 - \/ cons1 alt - \/ cons1 cat - \/ cons1 Rep - -prop_readShow :: RE -> Bool -prop_readShow re = read (show re) == re - -main = smallCheck 4 prop_readShow diff --git a/examples/run-examples.sh b/examples/run-examples.sh deleted file mode 100644 --- a/examples/run-examples.sh +++ /dev/null @@ -1,3 +0,0 @@ -find -iname '*.hs' \ - -exec grep -q ^main {} \; \ - -exec runghc {} \; diff --git a/smallcheck.cabal b/smallcheck.cabal --- a/smallcheck.cabal +++ b/smallcheck.cabal @@ -1,56 +1,70 @@ -Name: smallcheck -Version: 0.6.2 -Cabal-Version: >= 1.6 -License: BSD3 -License-File: LICENSE -Author: Colin Runciman -Maintainer: Roman Cheplyaka -Homepage: https://github.com/feuerbach/smallcheck -Bug-reports: https://github.com/feuerbach/smallcheck/issues +name: smallcheck +version: 1.2.1.1 +license: BSD3 +license-file: LICENSE +maintainer: Andrew Lelechenko +author: Colin Runciman, Roman Cheplyaka +cabal-version: >=1.10 +tested-with: + ghc ==9.6.1 ghc ==9.4.5 + ghc ==9.2.7 ghc ==9.0.2 ghc ==8.10.7 ghc ==8.8.4 ghc ==8.6.5 ghc ==8.4.4 ghc ==8.2.2 + ghc ==8.0.2 ghc ==7.10.3 ghc ==7.8.4 ghc ==7.6.3 ghc ==7.4.2 ghc ==7.2.2 ghc ==7.0.4 -Stability: Beta -Category: Testing -Synopsis: A property-based testing library -Description: SmallCheck is a testing library that allows to verify properties - for all test cases up to some depth. The test cases are generated - automatically by SmallCheck. -Build-Type: Simple +homepage: https://github.com/Bodigrim/smallcheck +bug-reports: https://github.com/Bodigrim/smallcheck/issues +synopsis: A property-based testing library +description: + As of 2023, this library is largely obsolete: arbitrary test generators + with shrinking such as [falsify](https://hackage.haskell.org/package/falsify) + offer much better user experience. + . + SmallCheck is a testing library that allows to verify properties + for all test cases up to some depth. The test cases are generated + automatically by SmallCheck. -Extra-source-files: examples/numeric/NumProps.hs, examples/logical/LogicProps.hs, - examples/imperative/Interpreter.hs, examples/imperative/Syntax.hs, - examples/imperative/Machine.hs, examples/imperative/Behaviour.hs, - examples/imperative/Properties.hs, examples/imperative/Value.hs, - examples/imperative/StackMap.hs, examples/imperative/Compiler.hs, - examples/listy/ListProps.hs, examples/regular/Regular.hs, - examples/circuits/BitAdd.hs, examples/circuits/Mux.hs, examples/circuits/Sad.hs, - examples/binarytries/BinaryTries.hs, - examples/numeric/README, examples/logical/README, examples/imperative/README, - examples/listy/README, examples/regular/README, examples/circuits/README, - examples/binarytries/README, - README.md, CREDITS.md, CHANGES.md, - examples/run-examples.sh +category: Testing +build-type: Simple +extra-source-files: + README.md + CREDITS.md + CHANGELOG.md +source-repository head + type: git + location: git://github.com/Bodigrim/smallcheck.git +library + default-language: Haskell2010 -Source-repository head - type: git - location: git://github.com/feuerbach/smallcheck.git + exposed-modules: + Test.SmallCheck + Test.SmallCheck.Drivers + Test.SmallCheck.Series -Source-repository this - type: git - location: git://github.com/feuerbach/smallcheck.git - tag: v0.6.2 + other-modules: + Test.SmallCheck.Property + Test.SmallCheck.SeriesMonad + Test.SmallCheck.Property.Result -Library + build-depends: + base >=4.3 && <5, + mtl <2.4, + logict >=0.5 && <0.9, + pretty <1.2 - Build-Depends: base == 4.* + if impl(ghc <8.0) + build-depends: + semigroups <0.21, + transformers <0.7 - Exposed-modules: - Test.SmallCheck - Test.SmallCheck.Drivers - Test.SmallCheck.Property - Test.SmallCheck.Series + if impl(ghc <7.10) + build-depends: + nats <1.2, + void <0.8 - if impl(ghc >= 7.2.1) - cpp-options: -DGENERICS - build-depends: ghc-prim >= 0.2, dlist >= 0.2 && < 0.6 + if impl(ghc <7.6) + build-depends: + ghc-prim >=0.2 && <1 + + if impl(ghc >= 8.0) + ghc-options: -Wcompat