diff --git a/examples/Div0.hs b/examples/Div0.hs
deleted file mode 100644
--- a/examples/Div0.hs
+++ /dev/null
@@ -1,95 +0,0 @@
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveGeneric #-}
-
--- | Divide by 0 example in a simple arithmetic language.
-
-module Div0 where
-
-import Test.QuickCheck
-import Test.SmartCheck
-import Control.Monad
-
-import GHC.Generics
-import Data.Typeable
-
------------------------------------------------------------------
-
-data Exp = C Int
-         | Add Exp Exp
-         | Div Exp Exp
-  deriving (Read, Show, Typeable, Generic)
-
-instance SubTypes Exp
-
-eval :: Exp -> Maybe Int
-eval (C i) = Just i
-eval (Add e0 e1) =
-  liftM2 (+) (eval e0) (eval e1)
-eval (Div e0 e1) =
-  let e = eval e1 in
-  if e == Just 0 then Nothing
-    else liftM2 div (eval e0) e
-
-instance Arbitrary Exp where
-  arbitrary = sized mkM
-    where
-    mkM 0 = liftM C arbitrary
-    mkM n = oneof [ liftM2 Add mkM' mkM'
-                  , liftM2 Div mkM' mkM' ]
-      where mkM' = mkM =<< choose (0,n-1)
-
-  -- shrink (C i)       = map C (shrink i)
-  -- shrink (Add e0 e1) = [e0, e1]
-  -- shrink (Div e0 e1) = [e0, e1]
-
--- property: so long as 0 isn't in the divisor, we won't try to divide by 0.
--- It's false: something might evaluate to 0 still.
-prop_div :: Exp -> ScProperty
-prop_div e = divSubTerms e --> eval e /= Nothing
--- prop_div e = property $ case x of
---                           Nothing -> True
---                           Just True -> True
---                           _       -> False
---   where x = fmap (< 1) (eval e)
-
-  -- precondition: no dividand in a subterm can be 0.
-divSubTerms :: Exp -> Bool
-divSubTerms (C _)         = True
-divSubTerms (Div _ (C 0)) = False
-divSubTerms (Add e0 e1)   = divSubTerms e0 && divSubTerms e1
-divSubTerms (Div e0 e1)   = divSubTerms e0 && divSubTerms e1
-
--- div0 (A _ _) = property False
--- div0 _       = property True
-
--- prop_test m = case eval m of
---                 Nothing -> True
---                 Just i -> i < 5
-
-divTest :: IO ()
-divTest = smartCheck args prop_div
-  where
-  args = scStdArgs { qcArgs  = stdArgs
-                                -- { maxSuccess = 1000
-                                -- , maxSize    = 20  }
-                   , format  = PrintString
-                   , runForall  = True
-                   }
-
--- Get the minimal offending sub-value.
-findVal :: Exp -> (Exp,Exp)
-findVal (Div e0 e1)
-  | eval e1 == Just 0     = (e0,e1)
-  | eval e1 == Nothing    = findVal e1
-  | otherwise             = findVal e0
-findVal a@(Add e0 e1)
-  | eval e0 == Nothing    = findVal e0
-  | eval e1 == Nothing    = findVal e1
-  | eval a == Just 0      = (a,a)
-findVal _                 = error "not possible"
-
-divSubValue :: Exp
-divSubValue =
-  Add (Div (C 5) (C (-12))) (Add (Add (C 2) (C 4)) (Add (C 7) (Div (C 3) (Add (C (-5)) (C 5)))))
-
---------------------------------------------------------------------------------
diff --git a/examples/Heap_Program.hs b/examples/Heap_Program.hs
deleted file mode 100644
--- a/examples/Heap_Program.hs
+++ /dev/null
@@ -1,227 +0,0 @@
-{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, DeriveDataTypeable, StandaloneDeriving #-}
-{-# LANGUAGE DeriveGeneric #-}
-
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-
--- Copied from QuickCheck2's examples.
-
-module Heap_Program where
-
---------------------------------------------------------------------------
--- imports
-
-import Test.QuickCheck
-import Test.QuickCheck.Poly
-
-import Data.List
-  ( sort
-  , (\\)
-  )
-import Data.Typeable
-
-import GHC.Generics
-
-import qualified Test.SmartCheck as SC
-
---------------------------------------------------------------------------
--- SmartCheck Testing.  Comment out shrink instance if you want to be more
--- impressed. :)
---------------------------------------------------------------------------
-
-instance Read OrdA where
-  readsPrec _ i = [ (OrdA j, str) | (j, str) <- reads i ]
-
-deriving instance Typeable OrdA
-deriving instance Generic OrdA
-
-heapProgramTest :: IO ()
-heapProgramTest = SC.smartCheck SC.scStdArgs (\h -> (prop_ToSortedList h))
-
-instance SC.SubTypes OrdA
-instance (SC.SubTypes a, Ord a, Arbitrary a, Generic a)
-         => SC.SubTypes (Heap a)
-instance (SC.SubTypes a, Arbitrary a, Generic a)
-         => SC.SubTypes (HeapP a)
-instance (SC.SubTypes a, Ord a, Arbitrary a, Generic a)
-         => SC.SubTypes (HeapPP a)
-
-instance (Ord a, Arbitrary a) => Arbitrary (Heap a) where
-  arbitrary = do p <- arbitrary :: Gen (HeapP a)
-                 return $ heap p
-
---------------------------------------------------------------------------
--- skew heaps
--- Smallest values on top.
-
-data Heap a
-  = Node a (Heap a) (Heap a)
-  | Nil
- deriving ( Eq, Ord, Show, Read, Typeable, Generic )
-
-empty :: Heap a
-empty = Nil
-
-isEmpty :: Heap a -> Bool
-isEmpty Nil = True
-isEmpty _   = False
-
-unit :: a -> Heap a
-unit x = Node x empty empty
-
-size :: Heap a -> Int
-size Nil            = 0
-size (Node _ h1 h2) = 1 + size h1 + size h2
-
-insert :: Ord a => a -> Heap a -> Heap a
-insert x h = unit x `merge` h
-
-removeMin :: Ord a => Heap a -> Maybe (a, Heap a)
-removeMin Nil            = Nothing
-removeMin (Node x h1 h2) = Just (x, h1 `merge` h2)
-
-merge :: Ord a => Heap a -> Heap a -> Heap a
-h1  `merge` Nil = h1
-Nil `merge` h2  = h2
-h1@(Node x h11 h12) `merge` h2@(Node y h21 h22)
-  | x <= y    = Node x (h12 `merge` h2) h11
-  | otherwise = Node y (h22 `merge` h1) h21
-
-fromList :: Ord a => [a] -> Heap a
-fromList xs = merging [ unit x | x <- xs ]
- where
-  merging []  = empty
-  merging [h] = h
-  merging hs  = merging (sweep hs)
-
-  sweep []         = []
-  sweep [h]        = [h]
-  sweep (h1:h2:hs) = (h1 `merge` h2) : sweep hs
-
-toList :: Heap a -> [a]
-toList h = toList' [h]
- where
-  toList' []                  = []
-  toList' (Nil          : hs) = toList' hs
-  toList' (Node x h1 h2 : hs) = x : toList' (h1:h2:hs)
-
-toSortedList :: Ord a => Heap a -> [a]
-toSortedList Nil            = []
-toSortedList (Node x h1 h2) = x : toList (h1 `merge` h2)
-
---------------------------------------------------------------------------
--- heap programs
-
-data HeapP a
-  = Empty
-  | Unit a
-  | Insert a (HeapP a)
-  | SafeRemoveMin (HeapP a)
-  | Merge (HeapP a) (HeapP a)
-  | FromList [a]
- deriving ( Show, Read, Typeable, Generic )
-
-heap :: Ord a => HeapP a -> Heap a
-heap Empty             = empty
-heap (Unit x)          = unit x
-heap (Insert x p)      = insert x (heap p)
-heap (SafeRemoveMin p) = case removeMin (heap p) of
-                           Nothing    -> empty -- arbitrary choice
-                           Just (_,h) -> h
-heap (Merge p q)       = heap p `merge` heap q
-heap (FromList xs)     = fromList xs
-
-instance Arbitrary a => Arbitrary (HeapP a) where
-  arbitrary = sized arbHeapP
-   where
-    arbHeapP s =
-      frequency
-      [ (1, do return Empty)
-      , (1, do x <- arbitrary
-               return (Unit x))
-      , (s, do x <- arbitrary
-               p <- arbHeapP s1
-               return (Insert x p))
-      , (s, do p <- arbHeapP s1
-               return (SafeRemoveMin p))
-      , (s, do p <- arbHeapP s2
-               q <- arbHeapP s2
-               return (Merge p q))
-      , (1, do xs <- arbitrary
-               return (FromList xs))
-      ]
-     where
-      s1 = s-1
-      s2 = s`div`2
-
-
-  -- shrink (Unit x)          = [ Unit x' | x' <- shrink x ]
-  -- shrink (FromList xs)     = [ Unit x | x <- xs ]
-  --                         ++ [ FromList xs' | xs' <- shrink xs ]
-  -- shrink (Insert x p)      = [ p ]
-  --                         ++ [ Insert x p' | p' <- shrink p ]
-  --                         ++ [ Insert x' p | x' <- shrink x ]
-  -- shrink (SafeRemoveMin p) = [ p ]
-  --                         ++ [ SafeRemoveMin p' | p' <- shrink p ]
-  -- shrink (Merge p q)       = [ p, q ]
-  --                         ++ [ Merge p' q | p' <- shrink p ]
-  --                         ++ [ Merge p q' | q' <- shrink q ]
-  -- shrink _                 = []
-
-data HeapPP a = HeapPP (HeapP a) (Heap a)
- deriving ( Show, Read, Typeable, Generic )
-
-instance (Ord a, Arbitrary a) => Arbitrary (HeapPP a) where
-  arbitrary =
-    do p <- arbitrary
-       return (HeapPP p (heap p))
-
-  -- shrink (HeapPP p _) =
-  --   [ HeapPP p' (heap p') | p' <- shrink p ]
-
---------------------------------------------------------------------------
--- properties
-
-(==?) :: Heap OrdA -> [OrdA] -> Bool
-h ==? xs = sort (toList h) == sort xs
-
-prop_Empty =
-  empty ==? []
-
-prop_IsEmpty (HeapPP _ h) =
-  isEmpty h == null (toList h)
-
-prop_Unit x =
-  unit x ==? [x]
-
-prop_Size (HeapPP _ h) =
-  size h == length (toList h)
-
-prop_Insert x (HeapPP _ h) =
-  insert x h ==? (x : toList h)
-
-prop_RemoveMin (HeapPP _ h) =
-  cover (size h > 1) 80 "non-trivial" $
-  case removeMin h of
-    Nothing     -> h ==? []
-    Just (x,h') -> x == minimum (toList h) && h' ==? (toList h \\ [x])
-
-prop_Merge (HeapPP _ h1) (HeapPP _ h2) =
-  (h1 `merge` h2) ==? (toList h1 ++ toList h2)
-
-prop_FromList xs =
-  fromList xs ==? xs
-
-prop_ToSortedList :: HeapPP OrdA -> Bool
-prop_ToSortedList (HeapPP _ h) =
-  h ==? xs && xs == sort xs
- where
-  xs = toSortedList h
-
---------------------------------------------------------------------------
--- main
-
--- main = $(quickCheckAll)
-
---------------------------------------------------------------------------
--- the end.
diff --git a/examples/LambdaCalc.hs b/examples/LambdaCalc.hs
deleted file mode 100644
--- a/examples/LambdaCalc.hs
+++ /dev/null
@@ -1,141 +0,0 @@
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveGeneric #-}
-
--- Copied from <http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html>
-
-module LambdaCalc where
-
-import Data.List
-import Data.Typeable
-
-import Control.Monad
-import GHC.Generics
-
-import Test.QuickCheck
-
-import Test.SmartCheck
-
-type Sym = String
-
-data Expr
-        = Var Sym
-        | App Expr Expr
-        | Lam Sym Expr
-        deriving (Eq, Read, Show, Typeable, Generic)
-
-freeVars :: Expr -> [Sym]
-freeVars (Var v) = [v]
-freeVars (App f a) = freeVars f `union` freeVars a
-freeVars (Lam i e) = freeVars e \\ [i]
-
-subst :: Sym -> Expr -> Expr -> Expr
-subst v x b = sub b
-  where sub e@(Var i) = if i == v then x else e
-        sub (App f a) = App (sub f) (sub a)
-        sub (Lam i e) =
-            if v == i then
-                Lam i e
-            else if i `elem` fvx then
-                let i' = cloneSym e i
-                    e' = substVar i i' e
-                in  Lam i' (sub e')
-            else
-                Lam i (sub e)
-        fvx = freeVars x
-        cloneSym e i = loop i
-           where loop i' = if i' `elem` vs then loop (i ++ "'") else i'
-                 vs = fvx ++ freeVars e
-
-substVar :: Sym -> Sym -> Expr -> Expr
-substVar v v' e = subst v (Var v') e
-
-alphaEq :: Expr -> Expr -> Bool
-alphaEq (Var v)   (Var v')    = v == v'
-alphaEq (App f a) (App f' a') = alphaEq f f' && alphaEq a a'
-alphaEq (Lam v e) (Lam v' e') = alphaEq e (substVar v' v e')
-alphaEq _ _ = False
-
-nf :: Expr -> Expr
-nf ee = spine ee []
-  where spine (App f a) as = spine f (a:as)
-        spine (Lam v e) [] = Lam v (nf e)
-        spine (Lam v e) (a:as) = spine (subst v a e) as
-        spine f as = app f as
-        app f as = foldl App f (map nf as)
-
-betaEq :: Expr -> Expr -> Bool
-betaEq e1 e2 = alphaEq (nf e1) (nf e2)
-
-z,s,m,n :: Expr
-[z,s,m,n] = map (Var . (:[])) "zsmn"
-app2 :: Expr -> Expr -> Expr -> Expr
-app2 f x y = App (App f x) y
-zero, one, two, three, plus :: Expr
-zero  = Lam "s" $ Lam "z" z
-one   = Lam "s" $ Lam "z" $ App s z
-two   = Lam "s" $ Lam "z" $ App s $ App s z
-three = Lam "s" $ Lam "z" $ App s $ App s $ App s z
-plus  = Lam "m" $ Lam "n" $ Lam "s" $ Lam "z" $ app2 m s (app2 n s z)
-
-test0 :: Bool
-test0 = betaEq (app2 plus one two) three
-
----------------------------------------------------------------------------------
-
-instance SubTypes Expr
-instance SubTypes Pr
-
----------------------------------------------------------------------------------
-
-data Pr = Pr Expr Expr
-  deriving (Read, Show, Typeable, Generic)
-
-instance Arbitrary Expr where
-  arbitrary = sized mkE
-    where
-    mkE 0 = liftM Var vars
-    mkE x = oneof [ liftM2 App (liftM2 Lam vars mkE') mkE'
-                  , liftM2 Lam vars mkE'
-                  ]
-      where
-      mkE' = mkE =<< choose (0, x-1)
-
-vars :: Gen [Char]
-vars = oneof $ map return ["x", "y", "z"]
-
-instance Arbitrary Pr where
-  arbitrary = do expr  <- arbitrary
-                 return $ Pr expr expr
-
----------------------------------------------------------------------------------
-
--- prop0 :: Pr -> Property
--- prop0 (Pr (e0, e1)) = alphaEq e0 e1 ==> betaEq e0 e1
-
--- if you do a beta reduction to nf
--- prop1 :: Pr -> ScProperty
--- prop1 (Pr e0 e1) = -- Timeout due to possible non-termination
---   within 1000 $ alphaEq e0 e1 --> betaEq e0 (substVar "x" "y" e1)
-
--- lambdaTest :: IO ()
--- lambdaTest = smartCheck args prop1
---   where args = scStdArgs { qcArgs = stdArgs { maxSuccess = 100
---                                             , maxSize    = 100
---                                             }
---                          }
-
----------------------------------------------------------------------------------
--- Cruft
-
-{-
-nonDet = App x x
-  where
-  x = Lam "x" (App (Var "x") (Var "x"))
-
-
-xx = (App (Lam "`" (App (Lam "\SI" (Var "f")) 
-                        (App (Lam "" (Var "O\172")) 
-                             (Var "3UC")))))
-
-aa (Pr a b) = alphaEq a b
--}
diff --git a/examples/MutualRecData.hs b/examples/MutualRecData.hs
deleted file mode 100644
--- a/examples/MutualRecData.hs
+++ /dev/null
@@ -1,60 +0,0 @@
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveGeneric #-}
-
-module MutualRecData where
-
-import Test.SmartCheck
-import Test.QuickCheck hiding (Result)
-
-import Data.Tree
-import Control.Monad.State
-import Data.Typeable
-
-import GHC.Generics
-
---------------------------------------------------------------------------------
-
-data M = M N N Int | P
-  deriving (Typeable, Show, Eq, Read, Generic)
-
-instance SubTypes M
-
-data N = N M Int String
-  deriving (Typeable, Show, Eq, Read, Generic)
-
-instance SubTypes N
-
---------------------------------------------------------------------------------
-
-instance Arbitrary M where
-  arbitrary =
-    sized $ \n -> if n == 0 then return P
-                    else oneof [ return P
-                               , liftM3 M (resize (n-1) arbitrary)
-                                          (resize (n-1) arbitrary)
-                                          arbitrary
-                               ]
-
-instance Arbitrary N where
-  arbitrary = liftM3 N arbitrary arbitrary arbitrary
-
---------------------------------------------------------------------------------
-
-prop0 :: M -> Bool
-prop0 (M _ _ a) = a < 100
-prop0 _         = True
-
-mutRecTest :: IO ()
-mutRecTest = smartCheck args prop0
-  where
-  args = scStdArgs { qcArgs = stdArgs {maxSuccess = 1000} }
-
---------------------------------------------------------------------------------
-
-xx :: M
-xx = M (N (M (N P 1 "goo") (N P 7 "foo") 8) 3 "hi") (N P 4 "bye") 6
-yy :: Forest Int
-yy = [Node 0 [Node 1 [], Node 2 []], Node 3 [Node 4 [], Node 5 [Node 6 []]]]
-
---------------------------------------------------------------------------------
diff --git a/examples/Tests.hs b/examples/Tests.hs
deleted file mode 100644
--- a/examples/Tests.hs
+++ /dev/null
@@ -1,15 +0,0 @@
-module Main where
-
-import Div0
-import MutualRecData
-import Heap_Program
---import LambdaCalc
---import Protocol
-
-main :: IO ()
-main = do
-  divTest
-  mutRecTest
-  heapProgramTest
---  lambdaTest
---  protocolTest
diff --git a/qc-tests/Tests.hs b/qc-tests/Tests.hs
new file mode 100644
--- /dev/null
+++ b/qc-tests/Tests.hs
@@ -0,0 +1,95 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE StandaloneDeriving #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+-- QuickCheck tests for the implementation of SmartCheck.
+
+module Main where
+
+import qualified Test.QuickCheck as Q
+
+import Data.Maybe
+import Data.Tree
+import Control.Monad
+import GHC.Generics
+import Test.SmartCheck.DataToTree
+import Test.SmartCheck.Types
+
+--------------------------------------------------------------------------------
+
+deriving instance Generic a =>  Generic (Tree a)
+instance (SubTypes a, Generic a) => SubTypes (Tree a)
+
+instance Q.Arbitrary a => Q.Arbitrary (Tree a) where
+  arbitrary = Q.sized mkT
+    where
+    mkT 0 = Q.arbitrary >>= \a -> return (Node a [])
+    mkT n = do len <- Q.choose (0, 4)
+               a <- Q.arbitrary
+               ls <- replicateM len mkT'
+               return $ Node a ls
+      where mkT' = mkT =<< Q.choose (0, n-1)
+
+instance Q.Arbitrary Idx where
+  arbitrary = liftM2 Idx Q.arbitrary Q.arbitrary
+
+--------------------------------------------------------------------------------
+
+-- Just to prevent us from getting too many Nothings from indexing too deeply.
+dep :: Maybe Int
+dep = Just 5
+
+--------------------------------------------------------------------------------
+
+-- If you take from v a sub-value v' at index i, then replace v' at index i, you
+-- get v back.
+prop_getReplaceIdem ::
+  Tree Int -> Q.NonNegative Int -> Q.NonNegative Int -> Bool
+prop_getReplaceIdem v (Q.NonNegative i) (Q.NonNegative j) =
+  let x = getAtIdx v idx dep in
+  case x of
+    Nothing -> True
+    Just st -> rep st
+  where
+  idx = Idx i j
+  rep (SubT v') = replaceAtIdx v idx v' == Just v
+
+--------------------------------------------------------------------------------
+
+-- Morally, getAtIdx v idx Nothing == rootLabel $ getIdxForest (subTypes v) idx
+--
+-- That is, they return the same value, except getIdxForest returns the whole
+-- tree.
+prop_forestTreeEq :: Tree Int -> Q.Positive Int -> Q.NonNegative Int -> Bool
+prop_forestTreeEq v (Q.Positive i) (Q.NonNegative j) =
+  let mx = getAtIdx v idx Nothing :: Maybe SubT in
+  let my = getIdxForest (subTypes v) idx :: Maybe (Tree SubT) in
+  (isNothing mx && isNothing my) || go mx my == Just True
+  where
+  -- XXX Hack! Since SubTypes doesn't derive Eq.
+  exEq (SubT x) (SubT y) = show x == show y
+  idx = Idx i j
+  go a b = do
+   x <- a
+   y <- b
+   return $ exEq x (rootLabel y)
+
+--------------------------------------------------------------------------------
+-- Prop:
+-- null (subTypes v) iff null (showForest v)
+--------------------------------------------------------------------------------
+
+
+-- Some random values.
+vals :: IO ()
+vals = Q.sample (Q.resize 5 Q.arbitrary :: Q.Gen (Tree Int))
+
+main :: IO ()
+main = do
+  Q.quickCheck prop_getReplaceIdem
+  Q.quickCheck prop_forestTreeEq
+
+--------------------------------------------------------------------------------
diff --git a/smartcheck.cabal b/smartcheck.cabal
--- a/smartcheck.cabal
+++ b/smartcheck.cabal
@@ -1,5 +1,5 @@
 Name:                smartcheck
-Version:             0.1
+Version:             0.2
 Synopsis:            A smarter QuickCheck.
 Homepage:            https://github.com/leepike/SmartCheck
 Description:         See the README.md.
@@ -18,6 +18,10 @@
   type:     git
   location: https://github.com/leepike/SmartCheck.git
 
+flag regression-flag
+  default:              False
+  description:          add libraries for regression testing
+
 Library
   Exposed-modules:   Test.SmartCheck,
                      Test.SmartCheck.Args,
@@ -28,15 +32,27 @@
                      Test.SmartCheck.Reduce,
                      Test.SmartCheck.Render,
                      Test.SmartCheck.SmartGen,
+                     Test.SmartCheck.Test,
                      Test.SmartCheck.Types
 
-  Build-depends:     base >= 4.0 && < 5,
-                     QuickCheck >= 2.6,
-                     mtl,
-                     random >= 1.0.1.1,
-                     containers >= 0.4,
-                     generic-deriving >= 1.2.1,
-                     ghc-prim
+  if flag(regression-flag)
+    Build-depends:     base >= 4.0 && < 5,
+                       QuickCheck >= 2.7,
+                       mtl,
+                       random >= 1.0.1.1,
+                       containers >= 0.4,
+                       generic-deriving >= 1.2.1,
+                       ghc-prim,
+                       testing-feat,
+                       lazysmallcheck
+  else
+    Build-depends:     base >= 4.0 && < 5,
+                       QuickCheck >= 2.7,
+                       mtl,
+                       random >= 1.0.1.1,
+                       containers >= 0.4,
+                       generic-deriving >= 1.2.1,
+                       ghc-prim
 
   default-language:  Haskell2010
 
@@ -49,16 +65,33 @@
     -caf-all
     -fno-warn-orphans
 
-executable sc-regression
+-- Tries some SmartCheck on small examples in a REPL.
+-- DEPRECATED in favor of the regression suite.
+-- executable sc-examples
+--   Hs-source-dirs:    examples
+--   Main-is:           Tests.hs
+--   Other-modules:     Div0,
+--                      MutualRecData,
+--                      Heap_Program,
+--                      LambdaCalc
+--   Build-depends:     base >= 4.0 && < 5,
+--                      smartcheck >= 0.2,
+--                      QuickCheck >= 2.7,
+--                      mtl,
+--                      random >= 1.0.1.1,
+--                      containers >= 0.4,
+--                      generic-deriving >= 1.2.1,
+--                      ghc-prim
+--   Default-language:  Haskell2010
+--   Ghc-options:       -Wall
+
+-- QuickCheck some basic properties about SmartCheck.
+executable sc-qc
+  Hs-source-dirs:    qc-tests
   Main-is:           Tests.hs
-  Other-modules:     Div0,
-                     MutualRecData,
-                     Heap_Program,
-                     LambdaCalc
-  Hs-source-dirs:    examples
   Build-depends:     base >= 4.0 && < 5,
-                     smartcheck,
-                     QuickCheck >= 2.4.2,
+                     smartcheck >= 0.2,
+                     QuickCheck >= 2.7,
                      mtl,
                      random >= 1.0.1.1,
                      containers >= 0.4,
diff --git a/src/Test/SmartCheck.hs b/src/Test/SmartCheck.hs
--- a/src/Test/SmartCheck.hs
+++ b/src/Test/SmartCheck.hs
@@ -5,16 +5,14 @@
 -- | Interface module.
 
 module Test.SmartCheck
-  ( -- ** Main interface function.
+  ( -- ** Main SmartCheck interface.
     smartCheck
 
-  -- ** Type of SmartCheck properties.
-  , ScProperty()
-  -- ** Implication for SmartCheck properties.
-  , (-->)
+    -- ** User-suppplied counterexample interface.
+  , smartCheckInput
 
   -- ** Run QuickCheck and get a result.
-  , runQCInit
+  , runQC
 
   -- ** Arguments
   , module Test.SmartCheck.Args
@@ -31,75 +29,83 @@
   ) where
 
 import Test.SmartCheck.Args
-import Test.SmartCheck.Types
+import Test.SmartCheck.ConstructorGen
+import Test.SmartCheck.Extrapolate
 import Test.SmartCheck.Matches
 import Test.SmartCheck.Reduce
-import Test.SmartCheck.Extrapolate
 import Test.SmartCheck.Render
-import Test.SmartCheck.ConstructorGen
+import Test.SmartCheck.Test
+import Test.SmartCheck.Types
 
 import qualified Test.QuickCheck as Q
 
 import Generics.Deriving
+import Control.Monad (when)
 
 --------------------------------------------------------------------------------
 
 -- | Main interface function.
-smartCheck :: forall a prop.
-  ( Read a, Q.Arbitrary a, SubTypes a
+smartCheck ::
+  ( SubTypes a
   , Generic a, ConNames (Rep a)
-  , ScProp prop, Q.Testable prop
+  , Q.Testable prop
   ) => ScArgs -> (a -> prop) -> IO ()
-smartCheck args scProp = do
-  -- Run standard QuickCheck or read in value.
-  (mcex, prop) <-
-    if qc args then runQCInit (qcArgs args) scProp
-      else do smartPrtLn "Input value to SmartCheck:"
-              mcex <- fmap Just (readLn :: IO a)
-              return (mcex, propify scProp)
+smartCheck args scProp =
+  smartCheckRun args =<< runQC (qcArgs args) scProp
 
+smartCheckInput :: forall a prop.
+  ( SubTypes a
+  , Generic a, ConNames (Rep a)
+  , Q.Testable prop
+  , Read a
+  ) => ScArgs -> (a -> prop) -> IO ()
+smartCheckInput args scProp = do
+  smartPrtLn "Input value to SmartCheck:"
+  mcex <- fmap Just (readLn :: IO a)
+  smartCheckRun args (mcex, Q.property . scProp)
+
+smartCheckRun :: forall a.
+  ( SubTypes a
+  , Generic a, ConNames (Rep a)
+  ) => ScArgs -> (Maybe a, a -> Q.Property) -> IO ()
+smartCheckRun args (origMcex, origProp) = do
   smartPrtLn $
-    "(If any stage takes too long, try modifying the standard "
+    "(If any stage takes too long, try modifying SmartCheck's standard "
       ++ "arguments (see Args.hs).)"
-  runSmartCheck prop mcex
-
+  smartCheck' [] origMcex origProp
   where
-  runSmartCheck :: (a -> Q.Property) -> Maybe a -> IO ()
-  runSmartCheck origProp = smartCheck' [] origProp
+  smartCheck' :: [(a, Replace Idx)]
+              -> Maybe a
+              -> (a -> Q.Property)
+              -> IO ()
+  smartCheck' ds mcex prop =
+    maybe (maybeDoneMsg >> return ()) go mcex
     where
-    smartCheck' :: [(a, Replace Idx)]
-                -> (a -> Q.Property)
-                -> Maybe a
-                -> IO ()
-    smartCheck' ds prop mcex = do
-      maybe (maybeDoneMsg >> return ()) go mcex
-      where
-      go cex = do
-          -- Run the smart reduction algorithm.
-        d <- smartRun args cex prop
-        -- If we asked to extrapolate values, do so.
-        valIdxs <- forallExtrap args d origProp
-        -- If we asked to extrapolate constructors, do so, again with the
-        -- original property.
-        csIdxs <- existsExtrap args d valIdxs origProp
-
-        let replIdxs = Replace valIdxs csIdxs
-        -- If either kind of extrapolation pass yielded fruit, prettyprint it.
-        showExtrapOutput args valIdxs csIdxs replIdxs d
+    go cex = do
+        -- Run the smart reduction algorithm.
+      d <- smartRun args cex prop
+      -- If we asked to extrapolate values, do so.
+      valIdxs <- forallExtrap args d origProp
+      -- If we asked to extrapolate constructors, do so, again with the
+      -- original property.
+      csIdxs <- existsExtrap args d valIdxs origProp
 
-        -- Ask the user if she wants to try again.
-        runAgainMsg
-        s <- getLine
+      let replIdxs = Replace valIdxs csIdxs
+      -- If either kind of extrapolation pass yielded fruit, prettyprint it.
+      showExtrapOutput args valIdxs csIdxs replIdxs d
+      -- Try again?
+      runAgainMsg
 
-        if s == ""
-          -- If so, then loop, with the new prop.
-          then do let oldVals  = (d,replIdxs):ds
-                  let matchesProp a =
-                              not (matchesShapes a oldVals)
-                        Q.==> prop a
-                  mcex' <- runQC (qcArgs args) matchesProp
-                  smartCheck' oldVals matchesProp mcex'
-          else smartPrtLn "Done."
+      s <- getLine
+      if s == ""
+        -- If so, then loop, with the new prop.
+        then do let oldVals  = (d,replIdxs):ds
+                let matchesProp a =
+                            not (matchesShapes a oldVals)
+                      Q.==> prop a
+                (mcex', _) <- runQC (qcArgs args) (Q.noShrinking . matchesProp)
+                smartCheck' oldVals mcex' matchesProp
+        else smartPrtLn "Done."
 
   maybeDoneMsg = smartPrtLn "No value to smart-shrink; done."
 
@@ -127,9 +133,10 @@
 showExtrapOutput :: SubTypes a1
                  => ScArgs -> [a] -> [a] -> Replace Idx -> a1 -> IO ()
 showExtrapOutput args valIdxs csIdxs replIdxs d =
-  if (runForall args || runExists args) && (not $ null (valIdxs ++ csIdxs))
-    then output
-    else smartPrtLn "Could not extrapolate a new value."
+  when (runForall args || runExists args) $ do
+    if null (valIdxs ++ csIdxs)
+      then smartPrtLn "Could not extrapolate a new value."
+      else output
   where
   output = do
     putStrLn ""
@@ -146,103 +153,26 @@
 
 --------------------------------------------------------------------------------
 
--- XXX I have to parse a string from QC to get the counterexamples.
-
--- | Run QuickCheck initially, to get counterexamples for each argument,
--- includding the one we want to focus on for SmartCheck, plus a `Property`.
-runQCInit :: (Show a, Read a, Q.Arbitrary a, ScProp prop, Q.Testable prop)
+-- | Run QuickCheck, to get a counterexamples for each argument, including the
+-- one we want to focus on for SmartCheck, which is the first argument.  That
+-- argument is never shrunk by QuickCheck, but others may be shrunk by
+-- QuickCheck.  Returns the value (if it exists) and a 'Property' (by applying
+-- the 'property' method to the 'Testable' value).  In each iteration of
+-- 'runQC', non-SmartCheck arguments are not necessarily held constant
+runQC :: forall a prop . (Show a, Q.Arbitrary a, Q.Testable prop)
           => Q.Args -> (a -> prop) -> IO (Maybe a, a -> Q.Property)
-runQCInit args scProp = do
-  res <- Q.quickCheckWithResult args (genProp $ propify scProp)
-  return $ maybe
-    -- 2nd arg should never be evaluated if the first arg is Nothing.
-    (Nothing, errorMsg "Bug in runQCInit")
-    ((\(cex, p) -> (Just cex, p)) . parse)
-    (getOut res)
-  where
-  parse outs = (read $ head cexs, prop')
-    where cexs = lenChk ((< 2) . length) outs
-          prop' = propifyWithArgs (tail cexs) scProp
-
--- | Run QuickCheck only analyzing the SmartCheck value, holding the other
--- values constant.
-runQC :: (Show a, Read a, Q.Arbitrary a)
-      => Q.Args -> (a -> Q.Property) -> IO (Maybe a)
-runQC args prop = do
-  res <- Q.quickCheckWithResult args (genProp prop)
-  return $ fmap parse (getOut res)
-  where
-  parse outs = read $ head cexs
-    where cexs = lenChk ((/= 2) . length) outs
-
-lenChk :: ([String] -> Bool) -> [String] -> [String]
-lenChk chk ls = if chk ls then errorMsg "No value to SmartCheck!"
-                   else tail ls
+runQC args scProp = do
+  (mCex, res) <- scQuickCheckWithResult args scProp
+  return $ if failureRes res
+             then (mCex,    Q.property . scProp)
+             else (Nothing, Q.property . scProp)
 
-getOut :: Q.Result -> Maybe [String]
-getOut res =
+-- | Returns 'True' if a counterexample is returned and 'False' otherwise.
+failureRes :: Q.Result -> Bool
+failureRes res =
   case res of
-    Q.Failure _ _ _ _ _ _ _ out -> Just $ lines out
-    _                           -> Nothing
-
-genProp :: (Show a, Q.Testable prop, Q.Arbitrary a)
-        => (a -> prop) -> Q.Property
-genProp prop = Q.forAllShrink Q.arbitrary Q.shrink prop
+    Q.Failure _ _ _ _ _ _ _ _ _ _ -> True
+    _                             -> False
 
 --------------------------------------------------------------------------------
 
--- | Type for SmartCheck properties.  Moral equivalent of QuickCheck's
--- `Property` type.
-data ScProperty = Implies (Bool, Bool)
-                | Simple  Bool
-  deriving (Show, Read, Eq)
-
-instance Q.Testable ScProperty where
-  property (Simple prop)         = Q.property prop
-  property (Implies prop)        = Q.property (toQCImp prop)
-  exhaustive (Simple prop)       = Q.exhaustive prop
-  exhaustive (Implies prop)      = Q.exhaustive (toQCImp prop)
-
--- same as ==>
-infixr 0 -->
--- | Moral equivalent of QuickCheck's `==>` operator.
-(-->) :: Bool -> Bool -> ScProperty
-pre --> post = Implies (pre, post)
-
--- Helper function.
-toQCImp :: (Bool, Bool) -> Q.Property
-toQCImp (pre, post) = pre Q.==> post
-
--- | Turn a function that returns a `Bool` into a QuickCheck `Property`.
-class ScProp prop where
-  scProperty :: [String] -> prop -> Q.Property
-  qcProperty :: prop -> Q.Property
-
--- | Instance without preconditions.
-instance ScProp Bool where
-  scProperty _ res = Q.property res
-  qcProperty       = Q.property
-
--- | Wrapped properties.
-instance ScProp ScProperty where
-  scProperty _ (Simple res)     = Q.property res
-  scProperty _ (Implies prop)   = Q.property $ toQCImp prop
-
-  qcProperty   (Simple res)     = Q.property res
-  qcProperty   (Implies prop)   = Q.property $ toQCImp prop
-
--- | Beta-reduction.
-instance (Q.Arbitrary a, Q.Testable prop, Show a, Read a, ScProp prop)
-  => ScProp (a -> prop) where
-  scProperty (str:strs) f = Q.property $ scProperty strs (f (read str))
-  scProperty _          _ = errorMsg "Insufficient values applied to property!"
-  qcProperty              = Q.property
-
-propifyWithArgs :: (Read a, ScProp prop)
-  => [String] -> (a -> prop) -> (a -> Q.Property)
-propifyWithArgs strs prop = \a -> scProperty strs (prop a)
-
-propify :: ScProp prop => (a -> prop) -> (a -> Q.Property)
-propify prop = \a -> qcProperty (prop a)
-
---------------------------------------------------------------------------------
diff --git a/src/Test/SmartCheck/Args.hs b/src/Test/SmartCheck/Args.hs
--- a/src/Test/SmartCheck/Args.hs
+++ b/src/Test/SmartCheck/Args.hs
@@ -18,10 +18,6 @@
                                      --------------
          , qcArgs       :: Q.Args    -- ^ QuickCheck arguments
                                      --------------
-         , qc           :: Bool      -- ^ Should we run QuickCheck?  (If not,
-                                     --   you are expected to pass in data to
-                                     --   analyze.)
-                                     --------------
          , scMaxSize    :: Int       -- ^ Maximum size of data to generate, in
                                      --   terms of the size parameter of
                                      --   QuickCheck's Arbitrary instance for
@@ -64,7 +60,6 @@
 scStdArgs :: ScArgs
 scStdArgs = ScArgs { format       = PrintTree
                    , qcArgs       = Q.stdArgs
-                   , qc           = True
                    , scMaxSize    = 10
                    , scMaxDepth   = Nothing
                    ---------------------
diff --git a/src/Test/SmartCheck/Reduce.hs b/src/Test/SmartCheck/Reduce.hs
--- a/src/Test/SmartCheck/Reduce.hs
+++ b/src/Test/SmartCheck/Reduce.hs
@@ -106,11 +106,11 @@
 -- | Get the maximum depth of d's subforest at idx.  Intuitively, it's the
 -- maximum number of constructors you have *below* the constructor at idx.  So
 -- for a unary constructor C, the value [C, C, C]
-
+--
 -- (:) C
 --   (:) C
 --     (:) C []
-
+--
 -- At (Idx 0 0) in v, we're at C, so subValSize v (Idx 0 0) == 0.
 -- At (Idx 0 1) in v, we're at (C : C : []), so subValSize v (Idx 0 1) == 2, since
 -- we have the constructors :, C (or :, []) in the longest path underneath.
diff --git a/src/Test/SmartCheck/Render.hs b/src/Test/SmartCheck/Render.hs
--- a/src/Test/SmartCheck/Render.hs
+++ b/src/Test/SmartCheck/Render.hs
@@ -83,7 +83,7 @@
   f :: Tree VarRepl -> (String, Idx) -> Tree VarRepl
   f tree (var, idx) = Node (rootLabel tree) $
     case getIdxForest sf idx of
-      Nothing                 -> errorMsg "replaceWithVars"
+      Nothing                 -> errorMsg "replaceWithVars1"
       Just (Node (Right _) _) -> sf -- Don't replace anything
       Just (Node (Left  _) _) -> forestReplaceChildren sf idx (Right var)
 
@@ -94,7 +94,7 @@
   -- data.  showForest is one of our generic methods.
   t :: Tree VarRepl
   t = let forest = showForest d in
-      if null forest then errorMsg "replaceWithVars"
+      if null forest then errorMsg "replaceWithVars2"
          else fmap Left (head forest) -- Should be a singleton
 
   -- Note: we put value idxs before constrs, since they take precedence.
diff --git a/src/Test/SmartCheck/SmartGen.hs b/src/Test/SmartCheck/SmartGen.hs
--- a/src/Test/SmartCheck/SmartGen.hs
+++ b/src/Test/SmartCheck/SmartGen.hs
@@ -11,8 +11,9 @@
 import Test.SmartCheck.Types
 import Test.SmartCheck.DataToTree
 
-import qualified Test.QuickCheck.Gen as Q
-import qualified Test.QuickCheck as Q hiding (Result)
+import qualified Test.QuickCheck.Gen      as Q
+import qualified Test.QuickCheck.Random   as Q
+import qualified Test.QuickCheck          as Q hiding (Result)
 import qualified Test.QuickCheck.Property as P
 
 import Prelude hiding (max)
@@ -24,7 +25,7 @@
 -- | Driver for iterateArb.
 iterateArbIdx :: SubTypes a
               => a -> (Idx, Maybe Int) -> Int -> Int
-              -> (a -> Q.Property) -> IO (Int, Result a)
+              -> (a -> P.Property) -> IO (Int, Result a)
 iterateArbIdx d (idx, max) tries sz prop =
   maybe (errorMsg "iterateArb 0")
         (\ext -> iterateArb d ext idx tries sz prop)
@@ -45,18 +46,18 @@
   -> Idx                -- ^ Index of sub-value.
   -> Int                -- ^ Maximum number of iterations.
   -> Int                -- ^ Maximum size of value to generate.
-  -> (a -> Q.Property)  -- ^ Property.
+  -> (a -> P.Property)      -- ^ Property.
   -> IO (Int, Result a) -- ^ Number of times precondition is passed and returned
                         -- result.
 iterateArb d ext idx tries max prop = do
-  g <- newStdGen
+  g <- Q.newQCGen
   iterateArb' (0, FailedPreCond) g 0 0
   where
   newMax SubT { unSubT = v } = valDepth v
 
   -- Main loop.  We break out if we ever satisfy the property.  Otherwise, we
   -- return the latest value.
-  iterateArb' :: (Int, Result a) -> StdGen -> Int -> Int -> IO (Int, Result a)
+  iterateArb' :: (Int, Result a) -> Q.QCGen -> Int -> Int -> IO (Int, Result a)
   iterateArb' (i, res) g try currMax
     -- We've exhausted the number of iterations.
     | try >= tries = return (i, res)
@@ -74,8 +75,8 @@
               Result x      -> return (i+1, Result x)
     where
     (size, g0) = randomR (0, currMax) g
-    s = sample ext g size
     sample SubT { unSubT = v } = newVal v
+    s = sample ext g size
     rec res' =
       iterateArb' res' g0 (try + 1)
         -- XXX what ratio is right to increase size of values?  This gives us
@@ -90,11 +91,10 @@
 -- | Make a new random value given a generator and a max size.  Based on the
 -- value's type's arbitrary instance.
 newVal :: forall a. (SubTypes a, Q.Arbitrary a)
-       => a -> StdGen -> Int -> SubT
+       => a -> Q.QCGen -> Int -> SubT
 newVal _ g size =
   let Q.MkGen m = Q.resize size (Q.arbitrary :: Q.Gen a) in
-  let v = m g size in
-  subT v
+  subT (m g size)
 
 --------------------------------------------------------------------------------
 
@@ -107,7 +107,7 @@
 
 -- | Make a QuickCheck Result by applying a property function to a value and
 -- then get out the Result using our result type.
-resultify :: (a -> Q.Property) -> a -> IO (Result a)
+resultify :: (a -> P.Property) -> a -> IO (Result a)
 resultify prop a = do
   P.MkRose r _ <- res fs
   return $ maybe FailedPreCond -- Failed precondition (discard)
@@ -120,8 +120,9 @@
     | not b && not (P.expect r) = Result a -- expected failure and got it
     | otherwise                 = FailedProp -- We'll just discard it.
 
-  Q.MkGen { Q.unGen = f } = prop a :: Q.Gen P.Prop
-  fs  = P.unProp $ f err err       :: P.Rose P.Result
+  P.MkProperty { P.unProperty = Q.MkGen { Q.unGen = f } }
+      = prop a :: P.Property
+  fs  = P.unProp $ f err err            :: P.Rose P.Result
   res = P.protectRose . P.reduceRose
 
   -- XXX A hack!  Means we failed the property because it failed, not because of
diff --git a/src/Test/SmartCheck/Test.hs b/src/Test/SmartCheck/Test.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/SmartCheck/Test.hs
@@ -0,0 +1,392 @@
+{-
+
+The following is modified by Lee Pike (2014) and still retains the following
+license:
+
+Copyright (c) 2000-2012, Koen Claessen
+Copyright (c) 2006-2008, Björn Bringert
+Copyright (c) 2009-2012, Nick Smallbone
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+- Redistributions of source code must retain the above copyright notice,
+  this list of conditions and the following disclaimer.
+- Redistributions in binary form must reproduce the above copyright
+  notice, this list of conditions and the following disclaimer in the
+  documentation and/or other materials provided with the distribution.
+- Neither the names of the copyright owners nor the names of the
+  contributors may be used to endorse or promote products derived
+  from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+-}
+
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+-- | SmartCheck's interface to QuickCheck.
+
+module Test.SmartCheck.Test
+  ( scQuickCheckWithResult
+  , stdArgs
+  ) where
+
+--------------------------------------------------------------------------
+-- imports
+
+import Prelude hiding (break)
+
+import Test.QuickCheck
+import Test.QuickCheck.Gen
+import Test.QuickCheck.Property hiding ( Result( reason, theException) )
+import qualified Test.QuickCheck.Property as P
+import Test.QuickCheck.Text
+import Test.QuickCheck.State
+import Test.QuickCheck.Exception
+import Test.QuickCheck.Random
+import System.Random(split)
+
+import Data.Char
+  ( isSpace
+  )
+
+import Data.List
+  ( sort
+  , group
+  , groupBy
+  , intersperse
+  )
+
+--------------------------------------------------------------------------
+-- quickCheck
+
+-- | Our SmartCheck reimplementation of the main QuickCheck driver.  We want to
+-- distinguish the first argument to a 'Testable' property to be SmartChecked.
+-- In particular: the first argument will not be shrunk (even if there are
+-- default shrink instances for the type).  However, the argument will be grown
+-- according to the the 'maxSize' argument to QuickCheck, in accordance with its
+-- generator.  Other arguments will be shrunk, if they have shrinking instances.
+scQuickCheckWithResult :: forall a prop. (Show a, Arbitrary a, Testable prop)
+  => Args -> (a -> prop) -> IO (Maybe a, Result)
+scQuickCheckWithResult a p = (if chatty a then withStdioTerminal else withNullTerminal) $ \tm -> do
+     rnd <- case replay a of
+              Nothing      -> newQCGen
+              Just (rnd,_) -> return rnd
+     test MkState{ terminal                  = tm
+                 , maxSuccessTests           = maxSuccess a
+                 , maxDiscardedTests         = maxDiscardRatio a * maxSuccess a
+                 , computeSize               = case replay a of
+                                                 Nothing    -> computeSize'
+                                                 Just (_,s) -> computeSize' `at0` s
+                 , numSuccessTests           = 0
+                 , numDiscardedTests         = 0
+                 , numRecentlyDiscardedTests = 0
+                 , collected                 = []
+                 , expectedFailure           = False
+                 , randomSeed                = rnd
+                 , numSuccessShrinks         = 0
+                 , numTryShrinks             = 0
+                 , numTotTryShrinks          = 0
+                 } flipProp
+  where computeSize' n d
+          -- e.g. with maxSuccess = 250, maxSize = 100, goes like this:
+          -- 0, 1, 2, ..., 99, 0, 1, 2, ..., 99, 0, 2, 4, ..., 98.
+          | n `roundTo` maxSize a + maxSize a <= maxSuccess a ||
+            n >= maxSuccess a ||
+            maxSuccess a `mod` maxSize a == 0 = (n `mod` maxSize a + d `div` 10) `min` maxSize a
+          | otherwise =
+            ((n `mod` maxSize a) * maxSize a `div` (maxSuccess a `mod` maxSize a) + d `div` 10) `min` maxSize a
+        n `roundTo` m = (n `div` m) * m
+        at0 _f s 0 0  = s
+        at0 f _s n d  = f n d
+
+        flipProp :: QCGen -> Int -> (a -> Prop)
+        flipProp q i = \a' ->
+          let p' = p a' in
+          let g = unGen (unProperty (property p')) in
+          g q i
+
+--------------------------------------------------------------------------
+-- main test loop
+
+test :: Arbitrary a => State -> (QCGen -> Int -> (a -> Prop)) -> IO (Maybe a, Result)
+test st f
+  | numSuccessTests st   >= maxSuccessTests st   = doneTesting st f
+  | numDiscardedTests st >= maxDiscardedTests st = giveUp st f
+  | otherwise                                    = runATest st f
+
+doneTesting :: State -> (QCGen -> Int -> (a -> Prop)) -> IO (Maybe a, Result)
+doneTesting st _f =
+  do -- CALLBACK done_testing?
+     if expectedFailure st then
+       putPart (terminal st)
+         ( "+++ OK, passed "
+        ++ show (numSuccessTests st)
+        ++ " tests"
+         )
+      else
+       putPart (terminal st)
+         ( bold ("*** Failed!")
+        ++ " Passed "
+        ++ show (numSuccessTests st)
+        ++ " tests (expected failure)"
+         )
+     success st
+     theOutput <- terminalOutput (terminal st)
+     return $ (Nothing, if expectedFailure st then
+                          Success{ labels = summary st,
+                                   numTests = numSuccessTests st,
+                                   output = theOutput }
+                        else NoExpectedFailure{ labels = summary st,
+                                                numTests = numSuccessTests st,
+                                                output = theOutput })
+
+giveUp :: State -> (QCGen -> Int -> (a -> Prop)) -> IO (Maybe a, Result)
+giveUp st _f =
+  do -- CALLBACK gave_up?
+     putPart (terminal st)
+       ( bold ("*** Gave up!")
+      ++ " Passed only "
+      ++ show (numSuccessTests st)
+      ++ " tests"
+       )
+     success st
+     theOutput <- terminalOutput (terminal st)
+     return ( Nothing
+            , GaveUp{ numTests = numSuccessTests st
+                    , labels   = summary st
+                    , output   = theOutput
+                    }
+            )
+
+runATest :: forall a. (Arbitrary a)
+         => State
+         -> (QCGen -> Int -> (a -> Prop))
+         -> IO (Maybe a, Result)
+runATest st f =
+  do -- CALLBACK before_test
+     putTemp (terminal st)
+        ( "("
+       ++ number (numSuccessTests st) "test"
+       ++ concat [ "; " ++ show (numDiscardedTests st) ++ " discarded"
+                 | numDiscardedTests st > 0
+                 ]
+       ++ ")"
+        )
+     let size = computeSize st (numSuccessTests st) (numRecentlyDiscardedTests st)
+
+     let p :: a -> Prop
+         p = f rnd1 size
+
+     let genA :: QCGen -> Int -> a
+         genA = unGen arbitrary
+     let rndA = genA rnd1 size
+
+     let mkRes res = return (Just rndA, res)
+
+     MkRose res ts <- protectRose (reduceRose (unProp (p rndA)))
+     callbackPostTest st res
+
+     let continue break st' | abort res = break st'
+                            | otherwise = test st'
+
+     case res of
+       MkResult{ok = Just True, stamp, expect} -> -- successful test
+         do continue doneTesting
+              st{ numSuccessTests           = numSuccessTests st + 1
+                , numRecentlyDiscardedTests = 0
+                , randomSeed                = rnd2
+                , collected                 = stamp : collected st
+                , expectedFailure           = expect
+                } f
+
+       MkResult{ok = Nothing, expect = expect} -> -- discarded test
+         do continue giveUp
+              st{ numDiscardedTests         = numDiscardedTests st + 1
+                , numRecentlyDiscardedTests = numRecentlyDiscardedTests st + 1
+                , randomSeed                = rnd2
+                , expectedFailure           = expect
+                } f
+
+       MkResult{ok = Just False} -> -- failed test
+         do if expect res
+              then putPart (terminal st) (bold "*** Failed! ")
+              else putPart (terminal st) "+++ OK, failed as expected. "
+            (numShrinks, totFailed, lastFailed) <- foundFailure st res ts
+            theOutput <- terminalOutput (terminal st)
+            if not (expect res) then
+              mkRes  Success{ labels = summary st,
+                              numTests = numSuccessTests st+1,
+                              output = theOutput }
+             else
+              mkRes  Failure{ -- correct! (this will be split first)
+                              usedSeed       = randomSeed st
+                            , usedSize       = size
+                            , numTests       = numSuccessTests st+1
+                            , numShrinks     = numShrinks
+                            , numShrinkTries = totFailed
+                            , numShrinkFinal = lastFailed
+                            , output         = theOutput
+                            , reason         = P.reason res
+                            , theException   = P.theException res
+                            , labels         = summary st
+                            }
+ where
+  (rnd1,rnd2) = split (randomSeed st)
+
+summary :: State -> [(String,Int)]
+summary st = reverse
+           . sort
+           . map (\ss -> (head ss, (length ss * 100) `div` numSuccessTests st))
+           . group
+           . sort
+           $ [ concat (intersperse ", " s')
+             | s <- collected st
+             , let s' = [ t | (t,_) <- s ]
+             , not (null s')
+             ]
+
+success :: State -> IO ()
+success st =
+  case allLabels ++ covers of
+    []    -> do putLine (terminal st) "."
+    [pt]  -> do putLine (terminal st)
+                  ( " ("
+                 ++ dropWhile isSpace pt
+                 ++ ")."
+                  )
+    cases -> do putLine (terminal st) ":"
+                sequence_ [ putLine (terminal st) pt | pt <- cases ]
+ where
+  allLabels = reverse
+            . sort
+            . map (\ss -> (showP ((length ss * 100) `div` numSuccessTests st) ++ head ss))
+            . group
+            . sort
+            $ [ concat (intersperse ", " s')
+              | s <- collected st
+              , let s' = [ t | (t,0) <- s ]
+              , not (null s')
+              ]
+
+  covers = [ ("only " ++ show occurP ++ "% " ++ fst (head lps) ++ "; not " ++ show reqP ++ "%")
+           | lps <- groupBy first
+                  . sort
+                  $ [ lp
+                    | lps <- collected st
+                    , lp <- maxi lps
+                    , snd lp > 0
+                    ]
+           , let occurP = (100 * length lps) `div` maxSuccessTests st
+                 reqP   = maximum (map snd lps)
+           , occurP < reqP
+           ]
+
+  (x,_) `first` (y,_) = x == y
+
+  maxi = map (\lps -> (fst (head lps), maximum (map snd lps)))
+       . groupBy first
+       . sort
+
+  showP p = (if p < 10 then " " else "") ++ show p ++ "% "
+
+--------------------------------------------------------------------------
+-- main shrinking loop
+
+foundFailure :: State -> P.Result -> [Rose P.Result] -> IO (Int, Int, Int)
+foundFailure st res ts =
+  do localMin st{ numTryShrinks = 0 } res res ts
+
+localMin :: State -> P.Result -> P.Result -> [Rose P.Result] -> IO (Int, Int, Int)
+localMin st MkResult{P.theException = Just e} lastRes _
+  | isInterrupt e = localMinFound st lastRes
+localMin st res _ ts = do
+  putTemp (terminal st)
+    ( short 26 (oneLine (P.reason res))
+   ++ " (after " ++ number (numSuccessTests st+1) "test"
+   ++ concat [ " and "
+            ++ show (numSuccessShrinks st)
+            ++ concat [ "." ++ show (numTryShrinks st) | numTryShrinks st > 0 ]
+            ++ " shrink"
+            ++ (if numSuccessShrinks st == 1
+                && numTryShrinks st == 0
+                then "" else "s")
+             | numSuccessShrinks st > 0 || numTryShrinks st > 0
+             ]
+   ++ ")..."
+    )
+  r <- tryEvaluate ts
+  case r of
+    Left err ->
+      localMinFound st
+         (exception "Exception while generating shrink-list" err) { callbacks = callbacks res }
+    Right ts' -> localMin' st res ts'
+
+localMin' :: State -> P.Result -> [Rose P.Result] -> IO (Int, Int, Int)
+localMin' st res [] = localMinFound st res
+localMin' st res (t:ts) =
+  do -- CALLBACK before_test
+    MkRose res' ts' <- protectRose (reduceRose t)
+    callbackPostTest st res'
+    if ok res' == Just False
+      then localMin st{ numSuccessShrinks = numSuccessShrinks st + 1,
+                        numTryShrinks     = 0 } res' res ts'
+      else localMin st{ numTryShrinks    = numTryShrinks st + 1,
+                        numTotTryShrinks = numTotTryShrinks st + 1 } res res ts
+
+localMinFound :: State -> P.Result -> IO (Int, Int, Int)
+localMinFound st res =
+  do let report = concat [
+           "(after " ++ number (numSuccessTests st+1) "test",
+           concat [ " and " ++ number (numSuccessShrinks st) "shrink"
+                  | numSuccessShrinks st > 0
+                  ],
+           "): "
+           ]
+     if isOneLine (P.reason res)
+       then putLine (terminal st) (P.reason res ++ " " ++ report)
+       else do
+         putLine (terminal st) report
+         sequence_
+           [ putLine (terminal st) msg
+           | msg <- lines (P.reason res)
+           ]
+     callbackPostFinalFailure st res
+     return (numSuccessShrinks st, numTotTryShrinks st - numTryShrinks st, numTryShrinks st)
+
+--------------------------------------------------------------------------
+-- callbacks
+
+callbackPostTest :: State -> P.Result -> IO ()
+callbackPostTest st res =
+  sequence_ [ safely st (f st res) | PostTest _ f <- callbacks res ]
+
+callbackPostFinalFailure :: State -> P.Result -> IO ()
+callbackPostFinalFailure st res =
+  sequence_ [ safely st (f st res) | PostFinalFailure _ f <- callbacks res ]
+
+safely :: State -> IO () -> IO ()
+safely st x = do
+  r <- tryEvaluateIO x
+  case r of
+    Left e ->
+      putLine (terminal st)
+        ("*** Exception in callback: " ++ show e)
+    Right x' ->
+      return x'
+
+--------------------------------------------------------------------------
+-- the end.
diff --git a/src/Test/SmartCheck/Types.hs b/src/Test/SmartCheck/Types.hs
--- a/src/Test/SmartCheck/Types.hs
+++ b/src/Test/SmartCheck/Types.hs
@@ -26,6 +26,8 @@
 import GHC.Generics
 import Data.Tree
 import Data.Typeable
+import Control.Applicative
+import Control.Monad (ap)
 
 -- For instances
 import Data.Word
@@ -60,6 +62,10 @@
   fmap _ FailedProp    = FailedProp
   fmap f (Result a)    = Result (f a)
 
+instance Applicative Result where
+ pure  = return
+ (<*>) = ap
+
 instance Monad Result where
   return a            = Result a
   FailedPreCond >>= _ = FailedPreCond
@@ -109,10 +115,7 @@
   show (SubT t) = show t
 
 -- | This class covers algebraic datatypes that can be transformed into Trees.
--- subTypes is the main method, placing values into trees.  For types that can't
--- be put into a *structural* order (e.g., Int), we don't want SmartCheck to
--- touch them, so that aren't placed in the tree (the baseType method tells
--- subTypes which types have this property).
+-- subTypes is the main method, placing values into trees.
 --
 -- for a datatype with constructors A and C,
 --
@@ -243,7 +246,9 @@
   gsz (M1 a) = gsz a
 
 instance (Show a, Q.Arbitrary a, SubTypes a, Typeable a) => GST (K1 i a) where
-  gst (K1 a) = if baseType a then [] else [ Node (subT a) (subTypes a) ]
+  gst (K1 a) = if baseType a
+                 then []
+                 else [ Node (subT a) (subTypes a) ]
 
   grc (K1 a) forest c =
     case forest of
@@ -340,23 +345,26 @@
 -- --  toConstrAndBase = toConstrAndBase'
 --  showForest    = showForest'
 
--- For container types like list, if it's over a baseType, we don't want to
--- evaluate the container either.  The intuition is that, e.g., for [Int], it'll
--- be shrunk enough by QuickCheck and doesn't really have "interesting
--- structure".
+-- For example, this makes String a baseType automatically.
+-- instance (Q.Arbitrary a, SubTypes a, Typeable a) => SubTypes [a] where
+--   subTypes      = if baseType (undefined :: a) then \_ -> []
+--                     else gst . from
+--   baseType _    = baseType (undefined :: a)
+--   replaceChild x forest y = if baseType (undefined :: a)
+--                               then replaceChild' x forest y
+--                               else fmap to $ grc (from x) forest y
+--   toConstr      = if baseType (undefined :: a) then toConstr'
+--                     else gtc . from
+--   showForest    = if baseType (undefined :: a) then showForest'
+--                     else gsf . from
 
 -- For example, this makes String a baseType automatically.
 instance (Q.Arbitrary a, SubTypes a, Typeable a) => SubTypes [a] where
-  subTypes      = if baseType (undefined :: a) then \_ -> []
-                    else gst . from
-  baseType _    = baseType (undefined :: a)
-  replaceChild x forest y = if baseType (undefined :: a)
-                              then replaceChild' x forest y
-                              else fmap to $ grc (from x) forest y
-  toConstr      = if baseType (undefined :: a) then toConstr'
-                    else gtc . from
-  showForest    = if baseType (undefined :: a) then showForest'
-                    else gsf . from
+  subTypes      = gst . from
+  baseType _    = False
+  replaceChild x forest y = fmap to $ grc (from x) forest y
+  toConstr      = gtc . from
+  showForest    = gsf . from
 
 instance (Integral a, Q.Arbitrary a, SubTypes a, Typeable a)
   => SubTypes (Ratio a) where