smallcheck 0.6.2 → 1.0

raw patch · 33 files changed

+970/−1820 lines, 33 filesdep +logictdep +mtldep +prettydep −dlistdep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: logict, mtl, pretty

Dependencies removed: dlist

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGES.md +9/−0
• README.md +0/−2
• Test/SmallCheck.hs +55/−29
• Test/SmallCheck/Drivers.hs +48/−85
• Test/SmallCheck/Property.hs +284/−133
• Test/SmallCheck/Property/Result.hs +78/−0
• Test/SmallCheck/Series.hs +441/−307
• Test/SmallCheck/SeriesMonad.hs +46/−0
• examples/binarytries/BinaryTries.hs +0/−79
• examples/binarytries/README +0/−10
• examples/circuits/BitAdd.hs +0/−23
• examples/circuits/Mux.hs +0/−114
• examples/circuits/README +0/−30
• examples/circuits/Sad.hs +0/−96
• examples/imperative/Behaviour.hs +0/−23
• examples/imperative/Compiler.hs +0/−59
• examples/imperative/Interpreter.hs +0/−41
• examples/imperative/Machine.hs +0/−50
• examples/imperative/Properties.hs +0/−178
• examples/imperative/README +0/−10
• examples/imperative/StackMap.hs +0/−35
• examples/imperative/Syntax.hs +0/−21
• examples/imperative/Value.hs +0/−44
• examples/listy/ListProps.hs +0/−92
• examples/listy/README +0/−8
• examples/logical/LogicProps.hs +0/−129
• examples/logical/README +0/−7
• examples/numeric/NumProps.hs +0/−64
• examples/numeric/README +0/−14
• examples/regular/README +0/−8
• examples/regular/Regular.hs +0/−104
• examples/run-examples.sh +0/−3
• smallcheck.cabal +9/−22

@@ -1,6 +1,15 @@ Changes ======= +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

@@ -13,7 +13,6 @@ To get started with SmallCheck:  * 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`@@ -24,7 +23,6 @@  [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

@@ -7,6 +7,9 @@ -- -- 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 -- <https://github.com/feuerbach/smallcheck/blob/master/README.md>@@ -15,57 +18,80 @@   -- * Constructing tests    -- | The simplest kind of test is a function (possibly of many-  -- arguments) returning 'Bool'.+  -- arguments) returning '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:+  --+  -- * ∀ x, y. p x y ('forAll')+  --+  -- * ∃ x, y: p x y ('exists')+  --+  -- * ∃! x, y: 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 ∀ x, y. p x y   ---  -- >isPrefix :: Eq a => [a] -> [a] -> Bool+  -- * @'exists' $ \\x y -> p x y@ means ∃ x, y: p x y   ---  -- and wish to specify it by some suitable property. We might define+  -- * @'exists' $ \\x -> 'forAll' $ \\y -> p x y@ means ∃ x: ∀ y. p x y   ---  -- >prop_isPrefix1 :: String -> String -> Bool-  -- >prop_isPrefix1 xs ys = isPrefix xs (xs++ys)+  -- * @'existsUnique' $ \\x y -> p x y@ means ∃! (x, y): 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 ∃! (x, y): y ∈ s && p x y   ---  -- We can also test the following property, which involves an existentially-  -- quantified variable:+  -- * @'existsUnique' $ \\x -> 'monadic' $ \\y -> p x y@ means ∃! x: ∀ y. [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 ∃! x: ∃! y: p x y+  --+  -- * @'exists' $ \\x -> (\\y -> p y) '==>' (\\z -> q z)@ means ∃ x: (∀ y. p y) => (∀ z. p 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 the @test-framework@ package:+  -- <http://hackage.haskell.org/package/test-framework>   --   -- It allows to organize SmallCheck properties into a test suite (possibly   -- together with HUnit or QuickCheck tests), apply timeouts, get nice   -- statistics etc.   --   -- To use SmallCheck properties with test-framework, install-  -- @test-framework-smallcheck@ package.-  smallCheck, depthCheck, smallCheckI,-  Depth+  -- the @test-framework-smallcheck@ package: <http://hackage.haskell.org/package/test-framework>+  --+  -- For more ways to run the tests, see "Test.SmallCheck.Drivers".+  Depth,+  smallCheck,++  -- * Main types and classes+  Testable,+  Property,+   ) where  import Test.SmallCheck.Property

@@ -5,103 +5,66 @@ -- License   : BSD3 -- Maintainer: Roman Cheplyaka <roma@ro-che.info> ----- Functions to run SmallCheck tests.+-- You should only need this module if you wish to create your own way to+-- run SmallCheck tests --------------------------------------------------------------------+{-# LANGUAGE FlexibleContexts #-} module Test.SmallCheck.Drivers (-  smallCheck, smallCheckI, depthCheck, smallCheckPure+  smallCheck, smallCheckM, smallCheckWithHook,+  test,+  ppFailure,+  PropertyFailure(..), PropertySuccess(..), Argument, TestQuality(..)   ) where -import System.IO (stdout, hFlush) import Control.Monad (when) import Test.SmallCheck.Property---- | 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)+import Test.SmallCheck.Property.Result+import Text.Printf+import Data.IORef --- | Same as 'smallCheck', but test for values of depth d only-depthCheck :: Testable a => Depth -> a -> IO ()-depthCheck d = iterCheck d (Just d)+-- | A simple driver that runs the test in the 'IO' monad and prints the+-- results.+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 --- | 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+runTestWithStats :: Testable IO a => Depth -> a -> IO ((Integer, Integer), Maybe PropertyFailure)+runTestWithStats d prop = do+  good <- newIORef 0+  bad <- newIORef 0 -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+  let+    hook GoodTest = modifyIORef' good (+1)+    hook BadTest  = modifyIORef' bad  (+1) -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 )+  r <- smallCheckWithHook d hook prop -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 )+  goodN <- readIORef good+  badN  <- readIORef bad -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+  return ((goodN, badN), r) --- | 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+smallCheckM :: Testable m a => Depth -> a -> m (Maybe PropertyFailure)+smallCheckM d a = smallCheckWithHook d (const $ return ()) a++-- | 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.+smallCheckWithHook :: Testable m a => Depth -> (TestQuality -> m ()) -> a -> m (Maybe PropertyFailure)+smallCheckWithHook d hook a = runProperty d hook $ test a

@@ -1,3 +1,5 @@+-- vim:fdm=marker:foldtext=foldtext()+ -------------------------------------------------------------------- -- | -- Module    : Test.SmallCheck.Property@@ -7,173 +9,322 @@ -- -- Properties and tools to construct them. ---------------------------------------------------------------------{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TypeFamilies,+             ScopedTypeVariables #-} 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, Depth, Testable(..),   ) where  import Test.SmallCheck.Series+import Test.SmallCheck.SeriesMonad+import Test.SmallCheck.Property.Result+import Control.Monad+import Control.Monad.Logic+import Control.Monad.Reader+import Control.Applicative import Data.Typeable -data TestResult-    = Pass-    | Fail-    | Inappropriate-        -- ^ 'Inappropriate' means that the precondition of '==>'-        -- was not satisfied-data TestCase = TestCase { result :: TestResult, arguments :: [String] }+------------------------------+-- Property-related types+------------------------------+--{{{ --- | Wrapper type for 'Testable's-newtype Property = Property (Depth -> [TestCase])-  deriving Typeable+-- | The type of properties over the monad @m@+newtype Property m = Property { unProperty :: Reader (Env m) (PropertySeries m) } --- | Wrap a 'Testable' into a 'Property'-property :: Testable a => a -> Property-property = Property . test+data PropertySeries m =+  PropertySeries+    { searchExamples        :: Series m PropertySuccess+    , searchCounterExamples :: Series m PropertyFailure+    , searchClosest         :: Series m (Property m, [Argument])+    } --- | A lower-level way to create properties. Use 'property' if possible.+data Env m =+  Env+    { quantification :: Quantification+    , testHook :: TestQuality -> m ()+    }++data Quantification+  = Forall+  | Exists+  | ExistsUnique++data TestQuality+  = GoodTest+  | BadTest+  deriving (Eq, Ord, Enum, Show)++instance Typeable1 m => Typeable (Property m)+  where+    typeOf _ =+      mkTyConApp+        (mkTyCon3 "smallcheck" "Test.SmallCheck.Property" "Property")+        [typeOf (undefined :: m ())]++-- }}}++------------------------------------+-- Property runners and constructors+------------------------------------+--{{{++unProp :: Env t -> Property t -> PropertySeries t+unProp q (Property p) = runReader p q++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++atomicProperty :: Series m PropertySuccess -> Series m PropertyFailure -> PropertySeries m+atomicProperty s f =+  let prop = PropertySeries s f (pure (Property $ pure prop, []))+  in prop++makeAtomic :: Property m -> Property m+makeAtomic (Property prop) =+  Property $ flip fmap prop $ \ps ->+    atomicProperty (searchExamples ps) (searchCounterExamples ps)++-- | @'over' s $ \\x -> p x@ makes @x@ range over the 'Series' @s@ (by+-- default, all variables range over the 'series' for their types). ----- The argument is a function that produces the list of results given the depth--- of testing.-mkProperty :: (Depth -> [TestCase]) -> Property-mkProperty = Property+-- 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.+over+  :: (Monad m, Show a, Testable m b)+  => Series m a -> (a -> b) -> Property m+over = testFunction --- | Anything of a 'Testable' type can be regarded as a \"test\"-class Testable a where-  test :: a -> Depth -> [TestCase]+-- | Execute a monadic test+monadic :: Testable m a => m a -> Property m+monadic a =+  Property $ reader $ \env -> -instance Testable Bool where-  test b _ = [TestCase (boolToResult b) []]+    let pair = unProp env . freshContext <$> lift a in -instance (Serial a, Show a, Testable b) => Testable (a->b) where-  test f = f' where Property f' = forAll series f+    atomicProperty+      (searchExamples =<< pair)+      (searchCounterExamples =<< pair) -instance Testable Property where-  test (Property f) d = f d+-- }}} -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 ]+-------------------------------+-- Testable class and instances+-------------------------------+-- {{{ -forAllElem :: (Show a, Testable b) => [a] -> (a->b) -> Property-forAllElem xs = forAll (const xs)+-- | 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 'Identity'.+class Monad m => Testable m a where+  test :: a -> Property m -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+instance Monad m => Testable m Bool where+  test b = Property $ reader $ \env ->+    let+      success = do+        lift $ testHook env GoodTest+        if b then return PropertyTrue else mzero+      failure = PropertyFalse <$ lnot success+    in atomicProperty success failure -unique :: [a] -> Bool-unique [_] = True-unique  _  = False+instance (Serial m a, Show a, Testable m b) => Testable m (a->b) where+  test = testFunction series --- | Return 'False' iff the result is 'Fail'-resultIsOk :: TestResult -> Bool-resultIsOk r =-    case r of-        Fail -> False-        Pass -> True-        Inappropriate -> True+instance (Monad m, m ~ n) => Testable n (Property m) where+  test = id -boolToResult :: Bool -> TestResult-boolToResult b = if b then Pass else Fail+testFunction+  :: (Monad m, 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 -thereExists :: (Show a, Testable b) => Series a -> (a->b) -> Property-thereExists = existence False+  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 -thereExists1 :: (Show a, Testable b) => Series a -> (a->b) -> Property-thereExists1 = existence True+        success = PropertyTrue <$ lnot failure+      -- }}} -thereExistsElem :: (Show a, Testable b) => [a] -> (a->b) -> Property-thereExistsElem xs = thereExists (const xs)+    Exists -> PropertySeries success failure closest+      -- {{{+      where+        success = do+          x <- s+          s <- searchExamples $ unProp env $ test $ f x+          let arg = show x -thereExists1Elem :: (Show a, Testable b) => [a] -> (a->b) -> Property-thereExists1Elem xs = thereExists1 (const xs)+          return $+            case s of+              Exist args etc -> Exist (arg:args) etc+              _ -> Exist [arg] s --- | @'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+        failure = NotExist <$ lnot success+      -- }}} --- | 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+    ExistsUnique -> PropertySeries success failure closest+      -- {{{+      where+        search = atMost 2 $ do+          (prop, args) <- closest+          ex <- once $ searchExamples $ unProp env $ test prop+          return (args, ex) --- | 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:------ >prop_append1 :: [Bool] -> [Bool] -> Property--- >prop_append1 xs ys = exists $ \zs -> zs == xs++ys------ 'existsDeeperBy' transforms the depth bound by a given @'Depth' -> 'Depth'@ function:------ >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)+        success =+          search >>=+            \examples ->+              case examples of+                [(x,s)] -> return $ ExistUnique x s+                _ -> mzero --- | 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)+        failure =+          search >>=+            \examples ->+              case examples of+                [] -> return NotExist+                (x1,s1):(x2,s2):_ -> return $ AtLeastTwo x1 s1 x2 s2+                _ -> mzero+      -- }}} -infixr 0 ==>+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 --- | 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:+-- }}}++------------------------------+-- 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+forAll :: Testable m a => a -> Property m+forAll = quantify Forall . test++-- | Set the existential quantification context+exists :: Testable m a => a -> Property m+exists = quantify Exists . test++-- | Set the uniqueness quantification context. ----- >prop_tautEval :: Proposition -> Environment -> Property--- >prop_tautEval p e =--- >  tautology p ==> eval p e+-- Bear in mind that ∃! (x, y): p x y is not the same as ∃! x: ∃! y: p x y. ----- But here is an alternative definition:+-- For example, ∃! x: ∃! y: |x| = |y| is true (it holds only when x=0), but ∃! (x,y): |x| = |y| is false (there are many such pairs). ----- >prop_tautEval :: Proposition -> Property--- >prop_taut p =--- >  tautology p ==> \e -> eval p e+-- 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). ----- The first definition generates p and e for each test, whereas the--- second only generates e if the tautology p holds.+-- That is, all the variables affected by the same uniqueness context are+-- quantified simultaneously as a tuple.+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. ----- 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 = [] }+-- Note that '==>' resets the quantification context for its operands to+-- the default (universal).+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.+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)+        ((\(prop, args) -> (changeDepth modifyDepth prop, args)) <$>+          localDepth modifyDepth sc)++-- | Quantify the function's argument over its 'series', but adjust the+-- depth. This doesn't affect any subsequent variables.+changeDepth1 :: (Show a, Serial m a, Testable m b) => (Depth -> Depth) -> (a -> b) -> Property m+changeDepth1 modifyDepth = over $ localDepth modifyDepth series++-- }}}

@@ -0,0 +1,78 @@+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, DefaultSignatures #-}+module Test.SmallCheck.Property.Result+  ( PropertySuccess(..)+  , PropertyFailure(..)+  , ppFailure+  , Argument+  ) where++import Text.PrettyPrint++type Argument = String++data PropertySuccess+  = Exist [Argument] PropertySuccess+  | ExistUnique [Argument] PropertySuccess+  | PropertyTrue+  | Vacuously PropertyFailure+  deriving (Eq, Show)++data PropertyFailure+  = NotExist+  | AtLeastTwo [Argument] PropertySuccess [Argument] PropertySuccess+  | CounterExample [Argument] PropertyFailure+  | PropertyFalse+  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 = text "condition is false"++instance Pretty PropertySuccess where+  pretty PropertyTrue = text "condition is true"+  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++ppFailure :: PropertyFailure -> String+ppFailure = render . pretty

@@ -1,3 +1,5 @@+-- vim:fdm=marker:foldtext=foldtext()+ -------------------------------------------------------------------- -- | -- Module    : Test.SmallCheck.Series@@ -5,28 +7,58 @@ -- License   : BSD3 -- Maintainer: Roman Cheplyaka <roma@ro-che.info> ----- Generation of test data.+-- 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 #-} -#ifdef GENERICS-{-# LANGUAGE DefaultSignatures-           , FlexibleContexts-           , TypeOperators-           , TypeSynonymInstances-           , FlexibleInstances-  #-}-#endif+{-# LANGUAGE CPP, RankNTypes, MultiParamTypeClasses, FlexibleInstances,+             GeneralizedNewtypeDeriving, FlexibleContexts #-}+-- The following is needed for generic instances+{-# LANGUAGE DefaultSignatures, FlexibleContexts, TypeOperators,+             TypeSynonymInstances, FlexibleInstances #-}  module Test.SmallCheck.Series (-  -- * Basic definitions-  Depth, Series, Serial(..),+  -- {{{+  -- * 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-  -- | SmallCheck itself defines data generators for all the data types used-  -- by the Prelude.-  ---  -- Writing SmallCheck generators for application-specific types is+  -- | 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.   --@@ -34,21 +66,17 @@   --   -- >data Tree a = Null | Fork (Tree a) a (Tree a)   -- >-  -- >instance Serial a => Serial (Tree a) where+  -- >instance Serial m a => Serial m (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:+  -- 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 a => Serial (Light a) where-  -- >  series = cons1 Light . depth 0-  ---  -- The depth of @Light x@ is just the depth of @x@.+  -- >instance Serial m a => Serial m (Light a) where+  -- >  series = newtypeCons Light    -- ** What does consN do, exactly? @@ -63,25 +91,38 @@   -- 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@).   --+  -- @consN@ functions also ensure that x_i are enumerated in the+  -- breadth-first order. Thus, combinations of smaller depth come first+  -- (assuming the same is true for @t_i@).+  --   -- If @d <= 0@, no values are produced. -  cons0, cons1, cons2, cons3, cons4,+  cons0, cons1, cons2, cons3, cons4, newtypeCons,   -- * 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:+  -- | To generate functions of an application-specific argument type,+  -- make the type an instance of 'CoSerial'.   ---  -- >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 ]+  -- 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    -- ** What does altsN do, exactly? @@ -93,342 +134,405 @@   --   -- >t_1 -> ... -> t_N -> t   ---  -- If @d <= 0@, these are constant functions, one for each value of @s 0@.+  -- If @d <= 0@, these are constant functions, one for each value produced+  -- by @s@.   ---  -- If @d > 0@, these functions inspect each of their arguments up to depth+  -- 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 given by @s d@.--  alts0, alts1, alts2, alts3, alts4,+  -- types) and return values produced by @s@. -  -- * Automated Derivation of Generators+  alts0, alts1, alts2, alts3, alts4, newtypeAlts, -  -- | 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+  -- * Basic definitions+  Depth, Series, Serial(..), CoSerial(..), -  -- ** 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.+  -- * Convenient wrappers+  Positive(..), NonNegative(..),    -- * Other useful definitions-  (\/), (><),-  N(..), Nat, Natural,-  depth+  (\/), (><), (<~>), (>>-),+  localDepth,+  decDepth,+  getDepth,+  generate,+  list+  -- }}}   ) where -import Data.List (intersperse)--#ifdef GENERICS+import Control.Monad.Logic+import Control.Monad.Reader+import Control.Applicative+import Control.Monad.Identity+import Data.List+import Test.SmallCheck.SeriesMonad 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+------------------------------+-- Main types and classes+------------------------------+--{{{ --- | '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]+class Monad m => Serial m a where+  series   :: Series m a +  default series :: (Generic a, GSerial m (Rep a)) => Series m a+  series = to <$> gSeries++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)++  default coseries :: (Generic a, GCoSerial m (Rep a)) => Series m b -> Series m (a->b)+  coseries rs = (. from) <$> gCoseries rs++-- }}}++------------------------------+-- Helper functions+------------------------------+-- {{{++-- | A simple series specified by a function from depth to the list of+-- values up to that depth.+generate :: (Depth -> [a]) -> Series m a+generate f = do+  d <- getDepth+  msum $ map return $ f d++suchThat :: Series m a -> (a -> Bool) -> Series m a+suchThat s p = s >>= \x -> if p x then pure x else empty++-- | Return the list of values generated by a 'Series'. Useful for+-- debugging 'Serial' instances.+list :: Depth -> Series Identity a -> [a]+list d s = runIdentity $ observeAllT $ runSeries d s+ -- | Sum (union) of series infixr 7 \/-(\/) :: Series a -> Series a -> Series a-s1 \/ s2 = \d -> s1 d ++ s2 d+(\/) :: Monad m => Series m a -> Series m a -> Series m a+(\/) = interleave  -- | Product of series infixr 8 ><-(><) :: Series a -> Series b -> Series (a,b)-s1 >< s2 = \d -> [(x,y) | x <- s1 d, y <- s2 d]+(><) :: Monad m => Series m a -> Series m b -> Series m (a,b)+a >< b = (,) <$> a <~> b -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)+-- | Fair version of 'ap' and '<*>'+infixl 4 <~>+(<~>) :: Monad m => Series m (a -> b) -> Series m a -> Series m b+a <~> b = a >>- (<$> b) -#ifdef GENERICS-  default series :: (Generic a, GSerial (Rep a)) => Series a-  series = map to . gSeries+uncurry3 :: (a->b->c->d) -> ((a,b,c)->d)+uncurry3 f (x,y,z) = f x y z -  default coseries :: (Generic a, GSerial (Rep a)) => Series b -> Series (a->b)-  coseries rs = map (. from) . gCoseries rs+uncurry4 :: (a->b->c->d->e) -> ((a,b,c,d)->e)+uncurry4 f (w,x,y,z) = f w x y z -class GSerial f where-  gSeries   :: Series (f a)-  gCoseries :: Series b -> Series (f a -> b)+-- | Query the current depth+getDepth :: Series m Depth+getDepth = Series ask -instance GSerial f => GSerial (M1 i c f) where-  gSeries      = map M1 . gSeries-  gCoseries rs = map (. unM1) . gCoseries rs-  {-# INLINE gSeries #-}-  {-# INLINE gCoseries #-}+-- | Run a series with a modified depth+localDepth :: (Depth -> Depth) -> Series m a -> Series m a+localDepth f (Series a) = Series $ local f a -instance Serial c => GSerial (K1 i c) where-  gSeries      = map K1 . series-  gCoseries rs = map (. unK1) . coseries rs-  {-# INLINE gSeries #-}-  {-# INLINE gCoseries #-}+-- | Run a 'Series' with the depth decreased by 1.+--+-- If the current depth is less or equal to 0, the result is 'mzero'.+decDepth :: Series m a -> Series m a+decDepth a = do+  checkDepth+  localDepth (subtract 1) a -instance GSerial U1 where-  gSeries        = cons0 U1-  gCoseries rs d = [\U1 -> b | b <- rs d]-  {-# INLINE gSeries #-}-  {-# INLINE gCoseries #-}+checkDepth :: Series m ()+checkDepth = do+  d <- getDepth+  guard $ d > 0 -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 #-}+constM :: Monad m => m b -> m (a -> b)+constM = liftM const -instance (GSerialSum a, GSerialSum b) => GSerial (a :+: b) where-  gSeries   = toList . gSeriesSum-  gCoseries = gCoseriesSum-  {-# INLINE gSeries #-}-  {-# INLINE gCoseries #-}+-- | If the current depth is 0, evaluate the first argument. Otherwise,+-- evaluate the second argument with decremented depth.+decDepthChecked :: Series m a -> Series m a -> Series m a+decDepthChecked b r = do+  d <- getDepth+  if d == 0+    then b+    else decDepth r -class GSerialSum f where-  gSeriesSum   :: DSeries (f a)-  gCoseriesSum :: Series b -> Series (f a -> b)+unwind :: MonadLogic m => m a -> m [a]+unwind a =+  msplit a >>=+  maybe (return []) (\(x,a') -> (x:) `liftM` unwind a') -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 #-}+------------------------------+-- cons* and alts* functions+------------------------------+-- {{{ -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+cons0 :: a -> Series m a+cons0 x = decDepth $ pure x -instance Serial () where-  series      _ = [()]-  coseries rs d = [ \() -> b-                  | b <- rs d ]+cons1 :: Serial m a => (a->b) -> Series m b+cons1 f = decDepth $ f <$> series -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 ]+-- | Same as 'cons1', but preserves the depth.+newtypeCons :: Serial m a => (a->b) -> Series m b+newtypeCons f = f <$> series -instance Serial Integer where-  series      d = [ toInteger (i :: Int)-                  | i <- series d ]-  coseries rs d = [ f . (fromInteger :: Integer->Int)-                  | f <- coseries rs d ]+cons2 :: (Serial m a, Serial m b) => (a->b->c) -> Series m c+cons2 f = decDepth $ f <$> series <~> series --- | '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)+cons3 :: (Serial m a, Serial m b, Serial m c) =>+         (a->b->c->d) -> Series m d+cons3 f = decDepth $+  f <$> series+    <~> series+    <~> series -instance Show a => Show (N a) where-  show (N i) = show i+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 -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 ]+alts0 :: Series m a -> Series m a+alts0 s = s -type Nat = N Int-type Natural = N Integer+alts1 :: (Monad m, CoSerial m a) => Series m b -> Series m (a->b)+alts1 rs =+  decDepthChecked (constM rs) (coseries rs) -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 ]+alts2+  :: (CoSerial m a, CoSerial m b)+  => Series m c -> Series m (a->b->c)+alts2 rs =+  decDepthChecked+    (constM $ constM rs)+    (coseries $ coseries rs) -instance Serial Double where-  series      d = [ frac (x :: Float)-                  | x <- series d ]-  coseries rs d = [ f . (frac :: Double->Float)-                  | f <- coseries rs d ]+alts3 ::  (CoSerial m a, CoSerial m b, CoSerial m c) =>+            Series m d -> Series m (a->b->c->d)+alts3 rs =+  decDepthChecked+    (constM $ constM $ constM rs)+    (coseries $ coseries $ coseries rs) -frac :: (Real a, Fractional a, Real b, Fractional b) => a -> b-frac = fromRational . toRational+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 =+  decDepthChecked+    (constM $ constM $ constM $ constM rs)+    (coseries $ coseries $ coseries $ coseries rs) -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 ]+-- | Same as 'alts1', but preserves the depth.+newtypeAlts :: (Monad m, CoSerial m a) => Series m b -> Series m (a->b)+newtypeAlts = coseries -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)+------------------------------+-- Generic instances+------------------------------+-- {{{ -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)+class GSerial m f where+  gSeries :: Series m (f a)+class GCoSerial m f where+  gCoseries :: Series m b -> Series m (f a -> b) -uncurry3 :: (a->b->c->d) -> ((a,b,c)->d)-uncurry3 f (x,y,z) = f x y z+instance 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 #-} -uncurry4 :: (a->b->c->d->e) -> ((a,b,c,d)->e)-uncurry4 f (w,x,y,z) = f w x y z+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 #-} -cons0 ::-         a -> Series a-cons0 c _ = [c]+instance GSerial m U1 where+  gSeries = cons0 U1+  {-# INLINE gSeries #-}+instance GCoSerial m U1 where+  gCoseries rs = constM rs+  {-# INLINE gCoseries #-} -cons1 :: Serial a =>-         (a->b) -> Series b-cons1 c d = [c z | d > 0, z <- series (d-1)]+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 #-} -cons2 :: (Serial a, Serial b) =>-         (a->b->c) -> Series c-cons2 c d = [c y z | d > 0, (y,z) <- series (d-1)]+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 #-} -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)]+------------------------------+-- Instances for basic types+------------------------------+-- {{{+instance Monad m => Serial m () where+  series = return ()+instance Monad m => CoSerial m () where+  coseries rs = constM rs -alts0 ::  Series a ->-            Series a-alts0 as d = as d+instance Monad m => Serial m Int where+  series =+    generate (\d -> if d >= 0 then pure 0 else empty) <|>+      nats `interleave` (fmap negate nats)+    where+      nats = generate $ \d -> [1..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]+instance Monad m => CoSerial m Int where+  coseries rs =+    alts0 rs >>- \z ->+    alts1 rs >>- \f ->+    alts1 rs >>- \g ->+    return $ \i -> case () of { _+      | i > 0 -> f (N (i - 1))+      | i < 0 -> g (N (abs i - 1))+      | otherwise -> z+    } -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]+instance Monad m => Serial m Integer where+  series = (toInteger :: Int -> Integer) <$> series+instance Monad m => CoSerial m Integer where+  coseries rs = (. (fromInteger :: Integer->Int)) <$> coseries rs -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]+-- | '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 a deriving (Eq, Ord, Real, Enum, Num, Integral) -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 (Integral a, Serial m a) => Serial m (N a) where+  series = generate $ \d -> map (N . fromIntegral) [0..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 (Integral a, Serial m a) => CoSerial m (N a) where+  coseries rs =+    alts0 rs >>- \z ->+    alts1 rs >>- \f ->+    return $ \(N i) ->+      if i > 0+        then f (N $ i-1)+        else z -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 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 (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 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 -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 ]+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 (Monad m, Serial m a, Serial m b) => Serial m (a,b) where+  series = cons2 (,)+instance (Monad m, CoSerial m a, CoSerial m b) => CoSerial m (a,b) where+  coseries rs = uncurry <$> alts2 rs++instance (Monad m, Serial m a, Serial m b, Serial m c) => Serial m (a,b,c) where+  series = cons3 (,,)+instance (Monad m, CoSerial m a, CoSerial m b, CoSerial m c) => CoSerial m (a,b,c) where+  coseries rs = uncurry3 <$> alts3 rs++instance (Monad m, Serial m a, Serial m b, Serial m c, Serial m d) => Serial m (a,b,c,d) where+  series = cons4 (,,,)+instance (Monad m, CoSerial m a, CoSerial m b, CoSerial m c, CoSerial m d) => CoSerial m (a,b,c,d) where+  coseries rs = uncurry4 <$> alts4 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++instance (Monad m, Serial m a) => Serial m (Maybe a) where+  series = cons0 Nothing \/ cons1 Just+instance (Monad m, CoSerial m a) => CoSerial m (Maybe a) where+  coseries rs =+    maybe <$> alts0 rs <~> alts1 rs++instance (Monad m, Serial m a, Serial m b) => Serial m (Either a b) where+  series = cons1 Left \/ cons1 Right+instance (Monad m, 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'++instance (CoSerial m a, Serial m b, Monad m) => Serial m (a->b) where+  series = coseries series -- 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 ]+instance (Serial m a, CoSerial m a, Serial m b, CoSerial m b, Monad m) => CoSerial m (a->b) where+  coseries r = do+    args <- unwind series --- | 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"+    g <- nest r args+    return $ \f -> g $ map f args -dec :: Depth -> Depth-dec d | d > 0     = d-1-      | otherwise = error "SmallCheck.dec: argument <= 0"+    where -inc :: Depth -> Depth-inc d = d+1+    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 a, Show a, Show b) => Show (a->b) where+instance (Serial Identity a, Show a, Show b) => Show (a->b) where   show f =     if maxarheight == 1     && sumarwidth + length ars * length "->;" < widthLimit then@@ -439,7 +543,7 @@       concat $ [a++"->\n"++indent r | (a,r) <- ars]     where     ars = take lengthLimit [ (show x, show (f x))-                           | x <- series depthLimit ]+                           | x <- list depthLimit series ]     maxarheight = maximum  [ max (height a) (height r)                            | (a,r) <- ars ]     sumarwidth = sum       [ length a + length r@@ -447,3 +551,33 @@     indent = unlines . map ("  "++) . lines     height = length . lines     (widthLimit,lengthLimit,depthLimit) = (80,20,3)::(Int,Int,Depth)++-- }}}++------------------------------+-- Convenient wrappers+------------------------------+-- {{{++--------------------------------------------------------------------------+-- | @Positive x@: guarantees that @x \> 0@.+newtype Positive a = Positive { getPositive :: a }+ deriving (Eq, Ord, Num, Integral, Real, Enum)++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 \>= 0@.+newtype NonNegative a = NonNegative { getNonNegative :: a }+ deriving (Eq, Ord, Num, Integral, Real, Enum)++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++-- }}}

@@ -0,0 +1,46 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+module Test.SmallCheck.SeriesMonad where++import Control.Applicative+import Control.Monad+import Control.Monad.Logic+import Control.Monad.Reader++-- | 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 `MonadLogic` action that enumerates values of a certain+-- type, up to some depth.+--+-- The depth bound is tracked in the 'SC' monad and can be extracted using+-- 'getDepth' and changed using '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.+-- @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.+newtype Series m a = Series (ReaderT Depth (LogicT m) a)+  deriving+    ( Functor+    , Monad+    , Applicative+    , MonadPlus+    , Alternative+    , MonadLogic)++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

@@ -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 "----------------------------------------------------------"-

@@ -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.

@@ -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

@@ -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

@@ -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.

@@ -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

@@ -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-

@@ -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]

@@ -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)

@@ -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

@@ -1,178 +0,0 @@-import Behaviour-import Interpreter-import Compiler-import Machine-import Syntax-import Value--import Test.SmallCheck--------------- <series of expressions and commands> ----------------- 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------------------- <Closed Expressions> ----------------------- 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)------------------- <Customised Programs> --------------------- 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]]---------- <depth-bounded equivalence of program traces> ----------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------------------- <congruence properties> --------------------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

@@ -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.

@@ -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

@@ -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)

@@ -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

@@ -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 "----------------------------------------------------"-

@@ -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.

@@ -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------------------------ <properties for testing> -----------------------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 "----------------------------------------------------"-

@@ -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.

@@ -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 "----------------------------------------------------"-

@@ -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.

@@ -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.

@@ -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

@@ -1,3 +0,0 @@-find -iname '*.hs' \-     -exec grep -q ^main {} \; \-     -exec runghc {} \;

@@ -1,9 +1,9 @@ Name:          smallcheck-Version:       0.6.2+Version:       1.0 Cabal-Version: >= 1.6 License:       BSD3 License-File:  LICENSE-Author:        Colin Runciman+Author:        Colin Runciman, Roman Cheplyaka Maintainer:    Roman Cheplyaka <roma@ro-che.info> Homepage:      https://github.com/feuerbach/smallcheck Bug-reports:   https://github.com/feuerbach/smallcheck/issues@@ -16,19 +16,7 @@                automatically by SmallCheck. Build-Type:    Simple -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+Extra-source-files: README.md, CREDITS.md, CHANGES.md   @@ -39,18 +27,17 @@ Source-repository this   type:     git   location: git://github.com/feuerbach/smallcheck.git-  tag:      v0.6.2+  tag:      v1.0  Library -    Build-Depends: base == 4.*+    Build-Depends: base == 4.*, mtl, logict, ghc-prim >= 0.2, pretty      Exposed-modules:         Test.SmallCheck         Test.SmallCheck.Drivers-        Test.SmallCheck.Property         Test.SmallCheck.Series--    if impl(ghc >= 7.2.1)-      cpp-options: -DGENERICS-      build-depends: ghc-prim >= 0.2, dlist >= 0.2 && < 0.6+    Other-modules:+        Test.SmallCheck.Property+        Test.SmallCheck.SeriesMonad+        Test.SmallCheck.Property.Result