diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -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
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -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
diff --git a/Test/SmallCheck.hs b/Test/SmallCheck.hs
--- a/Test/SmallCheck.hs
+++ b/Test/SmallCheck.hs
@@ -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
diff --git a/Test/SmallCheck/Drivers.hs b/Test/SmallCheck/Drivers.hs
--- a/Test/SmallCheck/Drivers.hs
+++ b/Test/SmallCheck/Drivers.hs
@@ -5,103 +5,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
diff --git a/Test/SmallCheck/Property.hs b/Test/SmallCheck/Property.hs
--- a/Test/SmallCheck/Property.hs
+++ b/Test/SmallCheck/Property.hs
@@ -1,3 +1,5 @@
+-- vim:fdm=marker:foldtext=foldtext()
+
 --------------------------------------------------------------------
 -- |
 -- Module    : Test.SmallCheck.Property
@@ -7,173 +9,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
+
+-- }}}
diff --git a/Test/SmallCheck/Property/Result.hs b/Test/SmallCheck/Property/Result.hs
new file mode 100644
--- /dev/null
+++ b/Test/SmallCheck/Property/Result.hs
@@ -0,0 +1,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
diff --git a/Test/SmallCheck/Series.hs b/Test/SmallCheck/Series.hs
--- a/Test/SmallCheck/Series.hs
+++ b/Test/SmallCheck/Series.hs
@@ -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
+
+-- }}}
diff --git a/Test/SmallCheck/SeriesMonad.hs b/Test/SmallCheck/SeriesMonad.hs
new file mode 100644
--- /dev/null
+++ b/Test/SmallCheck/SeriesMonad.hs
@@ -0,0 +1,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
diff --git a/examples/binarytries/BinaryTries.hs b/examples/binarytries/BinaryTries.hs
deleted file mode 100644
--- a/examples/binarytries/BinaryTries.hs
+++ /dev/null
@@ -1,79 +0,0 @@
--------------------------------------------------
--- Binary tries representing sets of bitstrings.
--- A test module for SmallCheck.
--- Colin Runciman, May 2008.
--------------------------------------------------
-
-module BinaryTries where
-
-import Test.SmallCheck
-import Test.SmallCheck.Series
-
--- first representation
-
-data BT1 = E | B Bool BT1 BT1 deriving Show
-
-instance Serial BT1 where
-  series = cons0 E \/ cons3 B
-
-
-contains1 :: BT1 -> [Bool] -> Bool
-contains1 E         _         = False
-contains1 (B b _ _) []        = b
-contains1 (B _ z _) (False:s) = contains1 z s
-contains1 (B _ _ o) (True :s) = contains1 o s
-
-prop_uniqueBT1 :: ([Bool]->Bool) -> Property
-prop_uniqueBT1 f =
-  exists1DeeperBy (+1) $ \bt -> contains1 bt === f
-
--- second representation
-
-data BT2  = E2 | NE BT2'
-            deriving Show
-
-data BT2' = T | O Bool BT2' | I Bool BT2' | OI Bool BT2' BT2'
-            deriving Show
-
-instance Serial BT2 where
-  series = cons0 E2 \/ cons1 NE
-
-instance Serial BT2' where
-  series = cons0 T \/ cons2 O \/ cons2 I \/ cons3 OI
-
-contains2 :: BT2 -> [Bool] -> Bool
-contains2 = contains1 . convert
-
-convert :: BT2 -> BT1
-convert E2       = E
-convert (NE bt') = convert' bt'
-
-convert' :: BT2' -> BT1
-convert' T            = B True E E
-convert' (O  b    z') = B b (convert' z') E
-convert' (I  b o'   ) = B b E (convert' o')
-convert' (OI b o' z') = B b (convert' z') (convert' o')
-
-prop_uniqueBT2 :: ([Bool]->Bool) -> Property
-prop_uniqueBT2 f =
-  exists1DeeperBy (+1) $ \bt -> contains2 bt === f
-
-(===) :: Eq b => (a->b) -> (a->b) -> a -> Bool
-f === g = \x -> f x == g x
-
-main :: IO ()
-main = do
-  test1 "\\f -> exists1DeeperBy (+1) $ \\bt1 -> contains1 bt1 === f ?"
-        prop_uniqueBT1
-  test1 "\\f -> exists1DeeperBy (+1) $ \\bt1 -> contains2 bt2 === f ?"
-        prop_uniqueBT2
-
-test1 :: Testable a => String -> a -> IO ()
-test1 s t = do
-  rule
-  putStrLn s
-  rule
-  smallCheck 2 t
-  where
-  rule = putStrLn "----------------------------------------------------------"
-
diff --git a/examples/binarytries/README b/examples/binarytries/README
deleted file mode 100644
--- a/examples/binarytries/README
+++ /dev/null
@@ -1,10 +0,0 @@
-First see ../../README.
-
-In this directory, BinaryTries.hs illustrates properties quantified
-over functions and requiring the unique existence of a data-structure.
-Two different trie representations are defined for sets of bitstrings.
-The properties state that each set has a unique representation as a
-trie -- true for the second representation, but not for the first.
-The properties are specified using functions with boolean results
-as a pure representation of sets, independent of any data structure.
-Compile or interpret BinaryTries.main for the self-introducing tests.
diff --git a/examples/circuits/BitAdd.hs b/examples/circuits/BitAdd.hs
deleted file mode 100644
--- a/examples/circuits/BitAdd.hs
+++ /dev/null
@@ -1,23 +0,0 @@
-import Test.SmallCheck
-
-and2 (a,b)       = a && b
-
-xor2 (a,b)       = a /= b
-
-halfAdd (a,b)    = (sum,carry)
-  where sum      = xor2 (a,b)
-        carry    = and2 (a,b)
-
-bit False        = 0
-bit True         = 1
-
-num []           = 0
-num (a:as)       = bit a + 2 * num as
-
-bitAdd a []      = [a]
-bitAdd a (b:bs)  = s : bitAdd c bs
-  where (s,c)    = halfAdd (a,b)
-
-prop_bitAdd a as = num (bitAdd a as) == bit a + num as
-
-main             = smallCheck 8 prop_bitAdd
diff --git a/examples/circuits/Mux.hs b/examples/circuits/Mux.hs
deleted file mode 100644
--- a/examples/circuits/Mux.hs
+++ /dev/null
@@ -1,114 +0,0 @@
-import List
-import Test.SmallCheck
-import Test.SmallCheck.Series
-
-type Bit             =  Bool
-
-unaryMux             :: [Bit] -> [[Bit]] -> [Bit]
-unaryMux sel xs      =  map (tree (||))
-                     $  transpose
-                     $  zipWith (\s x -> map (s &&) x) sel xs
-
-tree                 :: (a -> a -> a) -> [a] -> a
-tree f [x]           =  x
-tree f (x:y:ys)      =  tree f (ys ++ [f x y])
-
-decode               :: [Bit] -> [Bit]
-decode []            =  [True]
-decode [x]           =  [not x,x]
-decode (x:xs)        =  concatMap (\y -> [not x && y,x && y]) rest
-  where
-    rest             =  decode xs
-
-binaryMux            :: [Bit] -> [[Bit]] -> [Bit]
-binaryMux sel xs     =  unaryMux (decode sel) xs
-
-bitMux2              :: Bit -> Bit -> Bit -> Bit
-bitMux2 sel x y      =  (sel && y) || (not sel && x)
-
-muxf5                =  bitMux2
-
-muxf6                =  bitMux2
-
-busMux2              :: Bit -> [Bit] -> [Bit] -> [Bit]
-busMux2 sel xs ys    =  zipWith (bitMux2 sel) xs ys
-
-bitMux8              :: [Bit] -> [Bit] -> Bit
-bitMux8 _ [x]        =  x
-bitMux8 (s0:_) [x0,x1]
-                     =  bitMux2 s0 x0 x1
-bitMux8 (s0:s1:_) [x0,x1,x2,x3]
-                     =  muxf5 s1 (bitMux8 [s0] [x0,x1]) (bitMux8 [s0] [x2,x3])
-bitMux8 (s0:s1:s2:_) [x0,x1,x2,x3,x4,x5,x6,x7]
-                     =  muxf6 s2 (bitMux8 [s0,s1] [x0,x1,x2,x3])
-                                 (bitMux8 [s0,s1] [x4,x5,x6,x7])
-bitMux8 sels xs      =  bitMux8 (take n sels) (pad m xs)
-  where
-    n                =  log2 (length xs)
-    m                =  2 ^ n
-
-log2                 :: Int -> Int
-log2 n               =  length (takeWhile (< n) (iterate (*2) 1))
-
-pad                  :: Int -> [Bit] -> [Bit]
-pad n xs | m > n     =  xs
-         | otherwise =  xs ++ replicate (n-m) False
-  where
-    m                =  length xs
-
-bitMux               :: [Bit] -> [Bit] -> Bit
-bitMux sels [x]      =  x
-bitMux sels xs       =  bitMux (drop 3 sels) ys
-  where
-    ys               =  zipWith bitMux8 (repeat (take 3 sels)) (groupn 8 xs)
-
-
-groupn               :: Int -> [a] -> [[a]]
-groupn n []          =  []
-groupn n xs          =  take n xs : groupn n (drop n xs)
-
-binaryMux'           :: [Bit] -> [[Bit]] -> [Bit]
-binaryMux' sel       =  map (bitMux sel) . transpose
-
-num                  :: [Bit] -> Int
-num []               =  0
-num (a:as)           =  fromEnum a + 2 * num as
-
--- Property 0: binaryMux is correct
-
-prop_mux0 sel xs     =  length xs == 2 ^ length sel
-                     && all ((== length (head xs)) . length) xs
-                    ==> binaryMux sel xs == xs !! num sel
-
--- But this is inefficient as most of the test cases do not meet the
--- antecedent.  Instead, we can define a custom generator in which
--- the number of inputs grows exponentially (i.e. 2^) with respect to
--- the width of the address word.
-
-newtype Word         =  Word { bits :: [Bit] }
-                          deriving Show
-
-newtype File         =  File { wrds :: [Word] }
-                          deriving Show
-
-instance Serial Word where
-  series n  = map Word $ sequence (replicate n [False,True])
-
-instance Serial File where
-  series n  = map File $ sequence $ replicate (2^n) ws
-    where
-      ws    = series n :: [Word]
-
-prop_mux0' sel xs    =  xs' !! num sel' == binaryMux sel' xs'
-  where
-    sel'             =  bits sel
-    xs'              =  map bits (wrds xs)
-
--- Property 1: binaryMux' is correct
-
-prop_mux1 sel xs     =  xs' !! num sel' == binaryMux' sel' xs'
-  where
-    sel'             =  bits sel
-    xs'              =  map bits (wrds xs)
-
-main                 =  smallCheck 2 prop_mux1
diff --git a/examples/circuits/README b/examples/circuits/README
deleted file mode 100644
--- a/examples/circuits/README
+++ /dev/null
@@ -1,30 +0,0 @@
-First see ../../README.
-
-The programs in this directory define a number of different circuits.
-Some of these were originally written in Lava and were used to generate
-circuit netlists for external synthesis tools and propositional logic for
-external theorem provers.  They have been slightly adapted as examples
-for SmallCheck, so that they do not depend on Lava.
-
-BitAdd.hs defines a trivial circuit that takes two inputs, a bit and a
-bit-vector (i.e. a list of bits), and returns a bit-vector containing
-the sum of the two.  Using SmallCheck, it is straightforward to verify
-that the circuit behaves correctly for all bit-vector inputs up to the
-given size.
-
-Sad.hs defines a more complicated circuit that works over two lists of
-lists of bits, but verification with SmallCheck is just as simple and
-useful as before.
-
-Mux.hs defines a simple multiplexor and a more complicated variant that
-is optimised for Xilinx FPGAs.  Originally, the correctness of the more
-complicated version was argued by verifying its equivalence with the
-simpler version using an external SAT solver.  However, using SmallCheck,
-more general properties can be expressed, and so each circuit can be
-verified independently in terms of Haskell's list indexing operator (!!).
-The correctness properties are again easy to express in SmallCheck,
-but their antecedents filter out so many test cases as to make them
-inefficient.  This problem is resolved by writing a custom test-case
-generator using SmallCheck's "Serial" class.
-
-Matthew Naylor, University of York, 22nd Jan 2007.
diff --git a/examples/circuits/Sad.hs b/examples/circuits/Sad.hs
deleted file mode 100644
--- a/examples/circuits/Sad.hs
+++ /dev/null
@@ -1,96 +0,0 @@
-import Test.SmallCheck
-
--- We take the following specification for the sum of absolute
--- differences, and develop a circuit generator that has the same
--- behaviour.
-
-sad                            ::  [Int] -> [Int] -> Int
-sad xs ys                      =   sum (map abs (zipWith (-) xs ys))
-
-type Bit                       =   Bool
-
-low                            ::  Bit
-low                            =   False
-
-high                           ::  Bit
-high                           =   True
-
-inv                            ::  Bit -> Bit
-inv a                          =   not a
-
-and2                           ::  Bit -> Bit -> Bit
-and2 a b                       =   a && b
-or2 a b                        =   a || b
-xor2 a b                       =   a /= b
-xnor2 a b                      =   a == b
-
-mux2                           ::  Bit -> Bit -> Bit -> Bit
-mux2 sel a b                   =   (sel && b) || (not sel && a)
-
-bitAdd                         ::  Bit -> [Bit] -> [Bit]
-bitAdd x []                    =   [x]
-bitAdd x (y:ys)                =   let  (sum,carry) = halfAdd x y
-                                   in   sum:bitAdd carry ys
-
-halfAdd x y                    =   (xor2 x y,and2 x y)
-
-binAdd                         ::  [Bit] -> [Bit] -> [Bit]
-binAdd xs ys                   =   binAdd' low xs ys
-
-binAdd' cin   []       []      =   [cin]
-binAdd' cin   (x:xs)   []      =   bitAdd cin (x:xs)
-binAdd' cin   []       (y:ys)  =   bitAdd cin (y:ys)
-binAdd' cin   (x:xs)   (y:ys)  =   let  (sum,cout) = fullAdd cin x y
-                                   in   sum:binAdd' cout xs ys
-
-fullAdd cin a b                =   let  (s0,c0)  =  halfAdd a b
-                                        (s1,c1)  =  halfAdd cin s0
-                                   in   (s1,xor2 c0 c1)
-
-binGte                         ::  [Bit] -> [Bit] -> Bit
-binGte xs ys                   =   binGte' high xs ys
-
-binGte' gin  []      []        =   gin
-binGte' gin  (x:xs)  []        =   orl (gin:x:xs)
-binGte' gin  []      (y:ys)    =   and2 gin (orl (y:ys))
-binGte' gin  (x:xs)  (y:ys)    =   let  gout = gteCell gin x y
-                                   in   binGte' gout xs ys
-
-gteCell gin x y                =   mux2 (xnor2 x y) x gin
-
-orl                            ::  [Bit] -> Bit
-orl xs                         =   tree or2 low xs
-
-binDiff                        ::  [Bit] -> [Bit] -> [Bit]
-binDiff xs ys                  =   let  xs'   =  pad (length ys) xs
-                                        ys'   =  pad (length xs) ys
-                                        gte   =  binGte xs' ys'
-                                        xs''  =  map (xor2 (inv gte)) xs'
-                                        ys''  =  map (xor2 gte) ys'
-                                   in   init (binAdd' high xs'' ys'')
-  
-pad                            ::  Int -> [Bit] -> [Bit]
-pad n xs | m > n               =   xs
-         | otherwise           =   xs ++ replicate (n-m) False
-  where
-    m                          =   length xs
-
-tree                           ::  (a -> a -> a) -> a -> [a] -> a
-tree f z []                    =   z
-tree f z [x]                   =   x
-tree f z (x:y:ys)              =   tree f z (ys ++ [f x y])
-
-binSum                         ::  [[Bit]] -> [Bit]
-binSum xs                      =   tree binAdd [] xs
-
-binSad                         ::  [[Bit]] -> [[Bit]] -> [Bit]
-binSad xs ys                   =   binSum (zipWith binDiff xs ys)
-
-num                            ::  [Bit] -> Int
-num []                         =   0
-num (a:as)                     =   fromEnum a + 2 * num as
-
-prop_binSad xs ys              =   sad (map num xs) (map num ys)
-                                     == num (binSad xs ys)
-
-main                           =   smallCheck 3 prop_binSad
diff --git a/examples/imperative/Behaviour.hs b/examples/imperative/Behaviour.hs
deleted file mode 100644
--- a/examples/imperative/Behaviour.hs
+++ /dev/null
@@ -1,23 +0,0 @@
-module Behaviour(Trace(..),(+++),approx) where
-
-data Trace a
-  = Step (Trace a)
-  | a :> Trace a
-  | End
-  | Crash
-  deriving (Eq, Show)
-
-(+++) :: Trace a -> Trace a -> Trace a
-Step s   +++ t = Step (s +++ t)
-(x :> s) +++ t = x :> (s +++ t)
-End      +++ t = t
-Crash    +++ t = Crash
-
-approx :: Eq a => Int -> Trace a -> Trace a -> Bool
-approx 0 _        _        = True
-approx n (a :> s) (b :> t) = a == b && approx (n-1) s t
-approx n (Step s) (Step t) = approx (n-1) s t
-approx n End    End        = True
-approx n Crash  Crash      = True
-approx n _        _        = False
-
diff --git a/examples/imperative/Compiler.hs b/examples/imperative/Compiler.hs
deleted file mode 100644
--- a/examples/imperative/Compiler.hs
+++ /dev/null
@@ -1,59 +0,0 @@
-module Compiler(compile) where
-
-import Machine
-import Syntax
-import StackMap
-import Value
-
-compile :: Command -> [Instruction]
-compile c =
-  replicate (depth sm) (Push Wrong) ++
-  compObey sm c ++
-  [Halt]
-  where
-  sm = stackMap c
-
-compObey :: StackMap -> Command -> [Instruction]
-compObey sm Skip = 
-  []
-compObey sm (v := e) =
-  compEval sm e ++
-  [Store (location sm v + 1)]
-compObey sm (c1 :-> c2) =
-  compObey sm c1 ++
-  compObey sm c2
-compObey sm (If e c1 c2) =
-  compEval sm e ++
-  [JumpUnless (length isc1 + 1)] ++
-  isc1 ++
-  [Jump (length isc2)] ++
-  isc2
-  where
-  isc1 = compObey sm c1
-  isc2 = compObey sm c2
-compObey sm (While e c) =
-  ise ++
-  [JumpUnless (length isc + 1)] ++
-  isc ++
-  [Jump (negate (length isc + 1 + length ise + 1))]
-  where
-  ise = compEval sm e
-  isc = compObey sm c
-compObey sm (Print e) =
-  compEval sm e ++
-  [Display]
-
-compEval :: StackMap -> Expr -> [Instruction]
-compEval sm (Val v) =
-  [Push v]
-compEval sm (Var v) =
-  [Fetch (location sm v)]
-compEval sm (Uno op1 e) =
-  -- was op before arg eval  
-  compEval sm e ++
-  [Instr1 op1]
-compEval sm (Duo op2 e1 e2) =
-  -- was op before arg evals  
-  compEval sm        e1 ++
-  compEval (push sm) e2 ++
-  [Instr2 op2]
diff --git a/examples/imperative/Interpreter.hs b/examples/imperative/Interpreter.hs
deleted file mode 100644
--- a/examples/imperative/Interpreter.hs
+++ /dev/null
@@ -1,41 +0,0 @@
-module Interpreter(obey) where
-
-import Syntax
-import Behaviour
-import Value
-
-type Env = [(Name,Value)]
-
-obey :: Command -> Trace Value
-obey p = fst (run p [])
-
-look :: Name -> Env -> Value
-look x s = maybe Wrong id (lookup x s)
-
-update :: Name -> Value -> Env -> Env
-update x a s = (x,a) : filter (\(y,_) -> y/=x) s
-
-run :: Command -> Env -> (Trace Value, Env)
-run Skip        s = (End, s)
-run (x := e)    s = (End, update x (eval e s) s)
-run (p :-> q)   s = let (outp, sp) = run p s
-                        (outq, sq) = run q sp
-                    in (outp +++ outq, sq)
-run (If e p q)  s = case eval e s of
-                    -- was True -> q, False -> p
-                    Log True  -> run p s
-                    Log False -> run q s
-                    _         -> (Crash, s)
-run (While e p) s = case eval e s of
-                    Log True  -> let (outp,sp) = run p s
-                                     (outw,sw) = run (While e p) sp
-                                 in (outp +++ Step outw, sw)
-                    Log False -> (End, s)
-                    _         -> (Crash, s)
-run (Print e)   s = (eval e s :> End, s)
-
-eval :: Expr -> Env -> Value
-eval (Var x)      s = look x s
-eval (Val v)      s = v
-eval (Uno op a)   s = uno op (eval a s)
-eval (Duo op a b) s = duo op (eval a s) (eval b s)
diff --git a/examples/imperative/Machine.hs b/examples/imperative/Machine.hs
deleted file mode 100644
--- a/examples/imperative/Machine.hs
+++ /dev/null
@@ -1,50 +0,0 @@
-module Machine(Instruction(..), exec) where
-
-import Array
-import Behaviour
-import Value
-
-data Instruction
-  = Push Value
-  | Pop
-  | Fetch Int
-  | Store Int
-  | Instr1 Op1
-  | Instr2 Op2
-  | Display
-  | Jump Int
-  | JumpUnless Int
-  | Halt
- deriving (Eq, Show)
- 
-exec :: [Instruction] -> Trace Value
-exec instrs = run 1 []
-  where
-  size   = length instrs
-  memory = array (1,size) ([1..] `zip` instrs)
-  run pc stack =
-    if pc < 1 || size < pc then Crash
-    else
-      case (memory ! pc, stack) of
-      (Push x	    , stack)          -> run pc' (x : stack)
-      (Pop	    , _ : stack)      -> run pc' stack
-      (Fetch n      , stack)	 
-        | length stack >  n           -> run pc' (stack !! n : stack)
-      (Store n      , x : stack)
-        | length stack >= n           -> run pc' (take (n-1) stack ++
-                                                  x : drop n stack)
-      (Instr1 op1   , i : stack)      -> run pc' (uno op1 i : stack)
-      (Instr2 op2   , i : j : stack)  -> run pc' (duo op2 j i : stack)
-      (Display      , i : stack)      -> i :> run pc' stack
-      (Jump n	    , stack)	      -> step n (run (pc' + n) stack)
-      (JumpUnless n , Log b : stack)
-        | b	                      -> run pc' stack
-        | otherwise                   -> step n (run (pc' + n) stack)
-      (Halt	    , stack)	      -> End
-      _ 			      -> Crash
-     where
-      pc' = pc + 1
-
-step :: Int -> Trace Value -> Trace Value    
-step n t | n < 0     = Step t
-         | otherwise = t
diff --git a/examples/imperative/Properties.hs b/examples/imperative/Properties.hs
deleted file mode 100644
--- a/examples/imperative/Properties.hs
+++ /dev/null
@@ -1,178 +0,0 @@
-import Behaviour
-import Interpreter
-import Compiler
-import Machine
-import Syntax
-import Value
-
-import Test.SmallCheck
-
-------------- <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
diff --git a/examples/imperative/README b/examples/imperative/README
deleted file mode 100644
--- a/examples/imperative/README
+++ /dev/null
@@ -1,10 +0,0 @@
-First see ../../README.
-
-This directory gives the largest illustrative example.  We test for
-congruence between an interpreter and compiler for a small imperative
-language.  The example is adapted from an original using QuickCheck,
-as described in the lecture notes for AFP'02 (LNCS 2638).  Compared
-with the simpler example in ../logic, here specialised instances
-are used to restrict the input space to programs in a standard form.
-Run Properties.main and compare the rate of growth for the last two
-properties tested.
diff --git a/examples/imperative/StackMap.hs b/examples/imperative/StackMap.hs
deleted file mode 100644
--- a/examples/imperative/StackMap.hs
+++ /dev/null
@@ -1,35 +0,0 @@
-module StackMap where
-
-import Syntax
-import List( union )
-
-type StackMap = (Int,[Name])
-
-stackMap :: Command -> StackMap
-stackMap c = (0, comVars c)
-
-push :: StackMap -> StackMap
-push (n, vars) = (n+1, vars)
-
-pop :: StackMap -> StackMap
-pop (n, vars) = (n-1, vars)
-
-location :: StackMap -> Name -> Int
-location (n, vars) v = n + length (takeWhile (/=v) vars)
-
-depth :: StackMap -> Int
-depth (n, vars) = n + length vars
-
-expVars :: Expr -> [Name]
-expVars (Var v)     = [v]
-expVars (Val _)     = []
-expVars (Uno _ a)   = expVars a
-expVars (Duo _ a b) = expVars a `union` expVars b
-
-comVars :: Command -> [Name]
-comVars Skip         = []
-comVars (x := e)     = [x] `union` expVars e
-comVars (c1 :-> c2)  = comVars c1 `union` comVars c2
-comVars (If e c1 c2) = expVars e `union` comVars c1 `union` comVars c2
-comVars (While e c)  = expVars e `union` comVars c
-comVars (Print e)    = expVars e
diff --git a/examples/imperative/Syntax.hs b/examples/imperative/Syntax.hs
deleted file mode 100644
--- a/examples/imperative/Syntax.hs
+++ /dev/null
@@ -1,21 +0,0 @@
-module Syntax(Name, Expr(..), Command(..)) where
-
-import Value
-
-type Name = String
-
-data Expr
-  = Var Name
-  | Val Value
-  | Uno Op1 Expr
-  | Duo Op2 Expr Expr
-  deriving (Eq, Show)
-
-data Command
-  = Skip
-  | Name := Expr
-  | Command :-> Command
-  | If Expr Command Command
-  | While Expr Command
-  | Print Expr
-  deriving (Eq, Show)
diff --git a/examples/imperative/Value.hs b/examples/imperative/Value.hs
deleted file mode 100644
--- a/examples/imperative/Value.hs
+++ /dev/null
@@ -1,44 +0,0 @@
-module Value(Value(..), Op1(..), Op2(..), uno, duo) where
-
-data Value
-  = Num Int
-  | Log Bool
-  | Wrong
-  deriving (Eq, Show)
-
-data Op1
-  = Not
-  | Minus
-  deriving (Eq, Show)
-
-data Op2
-  = And
-  | Or
-  | Mul
-  | Add
-  | Sub
-  | Div
-  | Mod
-  | Less
-  | LessEq 
-  | Eq
-  deriving (Eq, Show)
-
-uno :: Op1 -> Value -> Value
-uno Not   (Log b) = Log (not b)
-uno Minus (Num n) = Num (negate n)
-uno _     _       = Wrong
-
-duo :: Op2 -> Value -> Value -> Value
-duo And     (Log a) (Log b)          = Log (a && b)
-duo Or      (Log a) (Log b)          = Log (a || b)
-duo Eq      (Log a) (Log b)          = Log (a == b)
-duo Mul     (Num m) (Num n)          = Num (m * n)
-duo Add     (Num m) (Num n)          = Num (m + n)
-duo Sub     (Num m) (Num n)          = Num (m - n)
-duo Div     (Num m) (Num n) | n /= 0 = Num (m `div` n)
-duo Mod     (Num m) (Num n) | n /= 0 = Num (m `mod` n)
-duo Less    (Num m) (Num n)          = Log (m < n)
-duo LessEq  (Num m) (Num n)          = Log (m <= n)
-duo Eq      (Num m) (Num n)          = Log (m == n)
-duo _       _       _                = Wrong
diff --git a/examples/listy/ListProps.hs b/examples/listy/ListProps.hs
deleted file mode 100644
--- a/examples/listy/ListProps.hs
+++ /dev/null
@@ -1,92 +0,0 @@
-------------------------------------------------
--- Properties (some valid some invalid) of a few
--- standard list-processing functions.
--- A test module for SmallCheck.
--- Colin Runciman, August 2006.
--- Revised for 0.2, November 2006.
-------------------------------------------------
-
-module ListProps where
-
-import Test.SmallCheck
-
--- properties about higher-order functions
--- plausible-looking but invalid laws about folds
-
-prop_fold1 :: [Bool] -> Property
-prop_fold1 xs =
-  not (null xs) ==>
-    \f -> foldl1 f xs == foldr1 f xs
-
-prop_fold2 :: [Bool] -> [Bool] -> Property
-prop_fold2 xs ys =
-  not (null xs) && not (null ys) ==>
-    \f -> foldr1 f xs `f` foldr1 f ys == foldr1 f (xs++ys)
-
--- properties using 'exists' with data and functional arguments
-
--- invalid because depth-bound for zs same as for xs ys
-prop_union1 :: [Bool] -> [Bool] -> Property
-prop_union1 xs ys =
-  exists $ \zs ->
-    \b -> (b `elem` zs) == (b `elem` xs || b `elem` ys)
-
--- valid variant: depth-bound doubled in existential
-prop_union2 :: [Bool] -> [Bool] -> Property
-prop_union2 xs ys =
-  existsDeeperBy (*2) $ \zs ->
-    \b -> (b `elem` zs) == (b `elem` xs || b `elem` ys)
-
--- do magical span arguments exist?
-prop_span1 :: [Bool] -> [Bool] -> [Bool] -> Property
-prop_span1 xs ys zs =
-  xs++ys == zs ==> exists $ \t -> (xs,ys) == span t zs
-
--- deliberate mistake in final isPrefix equation
-isPrefix :: Ord a => [a] -> [a] -> Bool
-isPrefix [] ys = True
-isPrefix (x:xs) [] = False
-isPrefix (x:xs) (y:ys) = x==y || isPrefix xs ys
-
--- this completeness property still holds
-isPrefixComplete :: String -> String -> Bool
-isPrefixComplete xs ys =
-  isPrefix xs (xs ++ ys)
-
--- but this existential soundness property fails
-isPrefixSound :: String -> String -> Property
-isPrefixSound xs ys = isPrefix xs ys ==>
-  exists $ \xs' -> ys == (xs ++ xs')
-
-main :: IO ()
-main = do
-  test1 "\\xs -> not (null xs) ==>\n\
-        \  \\f -> foldl1 f xs == foldr1 f xs ?"
-        prop_fold1
-  test1 "\\xs ys -> not (null xs) && not (null ys) ==>\n \
-        \  \\f -> foldr1 f xs `f` foldr1 f ys == foldr1 f (xs++ys) ?"
-        prop_fold2
-  test1 "\\xs ys -> exists $ \\zs ->\n\
-        \  \\b -> (b `elem` zs) == (b `elem` xs || b `elem` ys) ?"
-        prop_union1
-  test1 "\\xs ys -> existsDeeperBy (*2) $ \\zs ->\n\
-        \  \\b -> (b `elem` zs) == (b `elem` xs || b `elem` ys) ?"
-        prop_union2
-  test1 "\\xs ys zs -> xs++ys==zs ==>\n\
-        \  exists $ \\t -> (xs,ys) == span t zs ?"
-        prop_span1
-  test1 "\\xs ys -> isPrefix xs (xs++ys) ?"
-        isPrefixComplete
-  test1 "\\xs ys zs -> isPrefix xs ys ==>\n\
-        \  exists $ \\xs' -> ys == xs ++ xs' ?"
-        isPrefixSound
-
-test1 :: Testable a => String -> a -> IO ()
-test1 s t = do
-  rule
-  putStrLn s
-  rule
-  smallCheck 4 t
-  where
-  rule = putStrLn "----------------------------------------------------"
-
diff --git a/examples/listy/README b/examples/listy/README
deleted file mode 100644
--- a/examples/listy/README
+++ /dev/null
@@ -1,8 +0,0 @@
-First see ../../README.
-
-In this directory, compile or interpret ListProps.main (SmallCheck is
-the only other module required) for a small selection of self-introducing
-tests of list-processing functions.
-
-The definition of isPrefix is deliberately incorrect: the completeness
-property still holds, but the existential soundness property fails.
diff --git a/examples/logical/LogicProps.hs b/examples/logical/LogicProps.hs
deleted file mode 100644
--- a/examples/logical/LogicProps.hs
+++ /dev/null
@@ -1,129 +0,0 @@
-----------------------------------------------------
--- Propositional formulae, satisfiable, tautologous.
--- A test module for SmallCheck.
--- Colin Runciman, August 2006.
-----------------------------------------------------
-
-module PropLogic where
-
-import Test.SmallCheck
-import Test.SmallCheck.Series
-
-import List (nub)
-
-data Prop = Var Name
-          | Not Prop
-          | And Prop Prop
-          | Or  Prop Prop
-          | Imp Prop Prop
-
-instance Show Prop where
-  show p = case p of
-           Var n   -> show n
-           Not q   -> "~"++show' q
-           And q r -> show' q++"&"++show' r
-           Or  q r -> show' q++"|"++show' r
-           Imp q r -> show' q++"=>"++show' r
-    where
-    show' x = if priority p > priority x then "("++show x++")"
-              else show x
-    priority (Var _)   = 5
-    priority (Not _)   = 4
-    priority (And _ _) = 3
-    priority (Or  _ _) = 2
-    priority (Imp _ _) = 1
-
-data Name = P | Q | R deriving (Eq,Show)
-
-type Env = Name -> Bool
-
-eval :: Prop -> Env -> Bool
-eval (Var v)   env = env v
-eval (Not p)   env = not (eval p env)
-eval (And p q) env = eval p env && eval q env
-eval (Or  p q) env = eval p env || eval q env
-eval (Imp p q) env = eval p env <= eval q env 
-
-envsFor :: Prop -> [Env]
-envsFor p = foldr bind [const False] (nub (varsOf p))
-  where
-  bind v es = concat [ [\x -> x==v || e x, e]
-                     | e <- es ]
-
-varsOf :: Prop -> [Name]
-varsOf (Var v)   = [v]
-varsOf (Not p)   = varsOf p
-varsOf (And p q) = varsOf p ++ varsOf q
-varsOf (Or  p q) = varsOf p ++ varsOf q
-varsOf (Imp p q) = varsOf p ++ varsOf q
-
-tautologous :: Prop -> Bool
-tautologous p = all (eval p) (envsFor p)
-
-satisfiable :: Prop -> Bool
-satisfiable p = any (eval p) (envsFor p)
-
-instance Serial Name where 
-  series        = cons0 P \/ cons0 Q \/ cons0 R 
-  coseries rs d = [ \n -> case n of
-                          P -> x ; Q -> y ; R -> z               
-                  |  x <- alts0 rs d, y <- alts0 rs d, z <- alts0 rs d ]
-
-instance Serial Prop where
-  series = cons1 Var
-        \/ cons1 Not
-        \/ cons2 And
-        \/ cons2 Or
-        \/ cons2 Imp
-
----------------------- <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 "----------------------------------------------------"
-
diff --git a/examples/logical/README b/examples/logical/README
deleted file mode 100644
--- a/examples/logical/README
+++ /dev/null
@@ -1,7 +0,0 @@
-First see ../../README.
-
-In this directory, LogicProps.hs illustrates the basic way to define
-Serial instances of your own types, and hence Testable properties of
-functions over them. Compile or interpret LogicProps.main (SmallCheck is
-the only other module required) for a small selection of self-introducing
-tests.
diff --git a/examples/numeric/NumProps.hs b/examples/numeric/NumProps.hs
deleted file mode 100644
--- a/examples/numeric/NumProps.hs
+++ /dev/null
@@ -1,64 +0,0 @@
-----------------------------------------
--- Illustrating numerics in SmallCheck
--- Colin Runciman, November 2006.
--- Modified for SmallCheck 0.3, May 2008
-----------------------------------------
-
-import Test.SmallCheck
-import Test.SmallCheck.Series
-import Test.SmallCheck.Property
-
-primes :: [Int]
-primes = sieve [2..]
-  where
-  sieve (p:xs) =
-    p : filter (noFactorIn primes) xs
-  noFactorIn (p:ps) x =
-    p*p > x || x `mod` p > 0 && noFactorIn ps x
-
--- using natural numbers
-
-prop_primes1 :: Nat -> Property
-prop_primes1 (N n) =
-  n > 1 ==> forAll (`take` primes) $ \p ->
-    p `mod` n > 0 || n == p
-
-prop_primes2 :: Nat -> Property
-prop_primes2 (N n) =
-  n > 0 ==> exists1 $ \exponents ->
-    (null exponents || last exponents /= N 0) && 
-    n == product (zipWith power primes exponents)
-  where
-  power p (N e) = product (replicate e p)
-
--- using floating point numbers
-
-prop_logExp :: Float -> Bool
-prop_logExp x = exp (log x) == x
-
-prop_recipRecip :: Float -> Bool
-prop_recipRecip x = 1.0 / (1.0 / x) == x
-
-main :: IO ()
-main = do
-  test1 "\\(N n) -> n > 1 ==> forAll (`take` primes) $ \\p ->\n\
-        \  p `mod` n > 0 || n == p"
-        prop_primes1
-  test1 "\\(N n) -> n > 0 ==> exists1 $ \\exponents ->\n\
-        \  (null exponents || last exponents /= N 0) &&\n\
-        \  n == product (zipWith power primes exponents)"
-        prop_primes2
-  test1 "\\x -> exp (log x) == x"
-        prop_logExp
-  test1 "\\x -> 1.0 / (1.0 / x) == x"
-        prop_recipRecip
-
-test1 :: Testable a => String -> a -> IO ()
-test1 s t = do
-  rule
-  putStrLn s
-  rule
-  smallCheck 8 t
-  where
-  rule = putStrLn "----------------------------------------------------"
-
diff --git a/examples/numeric/README b/examples/numeric/README
deleted file mode 100644
--- a/examples/numeric/README
+++ /dev/null
@@ -1,14 +0,0 @@
-First see ../../README.
-
-In this directory, NumProps.hs illustrates the use of test series
-for natural numbers, either by explicit signatures including Nat (or
-Natural) or by use of the N constructor.  It also illustrates use of
-floating-point series. Compile or interpret NumProps (SmallCheck is
-the only other module required) and run main for a small selection of
-self-introducing tests -- a couple about natural numbers and primes,
-and a couple about floating point numbers.
-
-For version 0.3 the second property about primes has been strengthened
-by making the existence unique.  The restriction on the exponent list
-was prompted by reports of non-uniqueness when the 'exists1' version
-was first tested.
diff --git a/examples/regular/README b/examples/regular/README
deleted file mode 100644
--- a/examples/regular/README
+++ /dev/null
@@ -1,8 +0,0 @@
-First see ../../README.
-
-In this directory, Regular.hs illustrates a test involving IO -- writing
-and reading expressions to/from a file.  The use of 'smart constructors'
-in the series definition is necessary for the property to hold, but does
-*not* reduce the number of tests -- rather, there are duplicated tests for
-the same expressions generated in different ways. Compile or interpret
-Regular.main for a self-introducing test.
diff --git a/examples/regular/Regular.hs b/examples/regular/Regular.hs
deleted file mode 100644
--- a/examples/regular/Regular.hs
+++ /dev/null
@@ -1,104 +0,0 @@
-module Regular where
-
-import Char (isAlpha)
-import List (intersperse)
-import Monad (liftM)
-
-import Test.SmallCheck
-import Test.SmallCheck.Series
-
--- A data type of regular expressions.
-
-data RE = Emp
-        | Lam
-        | Sym Char
-        | Alt [RE]
-        | Cat [RE]
-        | Rep RE
-        deriving Eq
-
-isEmp, isLam, isSym, isCat, isAlt, isRep :: RE -> Bool
-isEmp Emp     = True
-isEmp _       = False
-isLam Lam     = True
-isLam _       = False
-isSym (Sym _) = True
-isSym _       = False
-isAlt (Alt _) = True
-isAlt _       = False
-isCat (Cat _) = True
-isCat _       = False
-isRep (Rep _) = True
-isRep _       = False
-
--- Syms may be used to represent terminals or variables.
--- Using cat and alt instead of Cat and Alt ensures that:
--- (1) Cat and Alt arguments are multi-item lists;
--- (2) items in Cat arguments are not Cats;
--- (3) items in Alt arguments are not Alts.
-
-cat :: [RE] -> RE
-cat []  = Lam
-cat [x] = x
-cat xs  = Cat (concatMap catList xs)
-  where
-  catList (Cat ys) = ys
-  catList z        = [z]
-
-alt :: [RE] -> RE
-alt []  = Emp
-alt [x] = x
-alt xs  = Alt (concatMap altList xs)
-  where
-  altList (Alt ys) = ys
-  altList z        = [z]
-
-instance Read RE where
-  readsPrec _ s  = [rest s [[[]]]]
-
-rest :: String -> [[[RE]]] -> (RE,String)
-rest ""      (    a:as) = if null as then (a2re a,"")
-                          else wrong
-rest ('+':s) ((c:a):as) = if null c then wrong
-			  else rest s (([]:c:a):as)
-rest ('*':s) ((c:a):as) = case c of
-                          []     -> wrong
-                          (x:xs) -> rest s (((Rep x:xs):a):as)
-rest ('0':s) ((c:a):as) = rest s (((Emp:c):a):as)
-rest ('1':s) ((c:a):as) = rest s (((Lam:c):a):as)
-rest ('(':s) as         = rest s ([[]]:as)
-rest (')':s) (a:as)     = case as of
-                          [] -> wrong
-			  ((c:a'):as') -> rest s (((a2re a:c):a'):as')
-rest (' ':s) as         = rest s as
-rest (v  :s) ((c:a):as) = if isAlpha v then rest s (((Sym v:c):a):as)
-                          else if null as then (a2re (c:a),v:s)
-			  else wrong
-			      
-a2re :: [[RE]] -> RE
-a2re = alt . reverse . map (cat . reverse)
-
-wrong = error "unreadable RE"
-
-instance Show RE where
-  show Emp      = "0"
-  show Lam      = "1"
-  show (Sym c)  = [c]
-  show (Alt xs) = concat (intersperse "+" (map show xs))
-  show (Cat xs) = concatMap (showBrackIf isAlt) xs
-  show (Rep x)  = showBrackIf (\x -> isCat x || isAlt x) x ++ "*"
-
-showBrackIf p x = ['(' | q] ++ show x ++ [')' | q] where q = p x
-
-instance Serial RE where
-  series = cons0 Emp
-        \/ cons0 Lam
-        \/ cons1 Sym . depth 0
-        \/ cons1 alt
-        \/ cons1 cat
-        \/ cons1 Rep
-
-prop_readShow :: RE -> Bool
-prop_readShow re = read (show re) == re
-
-main = smallCheck 4 prop_readShow
diff --git a/examples/run-examples.sh b/examples/run-examples.sh
deleted file mode 100644
--- a/examples/run-examples.sh
+++ /dev/null
@@ -1,3 +0,0 @@
-find -iname '*.hs' \
-     -exec grep -q ^main {} \; \
-     -exec runghc {} \;
diff --git a/smallcheck.cabal b/smallcheck.cabal
--- a/smallcheck.cabal
+++ b/smallcheck.cabal
@@ -1,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