diff --git a/Test/LazySmallCheck.hs b/Test/LazySmallCheck.hs
new file mode 100644
--- /dev/null
+++ b/Test/LazySmallCheck.hs
@@ -0,0 +1,275 @@
+-- Lazy SmallCheck (type-class variant, largely a SmallCheck subset)
+-- Lindblad, Naylor and Runciman
+
+module Test.LazySmallCheck
+  ( Serial(series) -- :: class
+  , Series         -- :: type Series a = Int -> Cons a
+  , Cons           -- :: *
+  , cons           -- :: a -> Series a
+  , (><)           -- :: Series (a -> b) -> Series a -> Series b
+  , (\/)           -- :: Series a -> Series a -> Series a
+  , drawnFrom      -- :: [a] -> Cons a
+  , cons0          -- :: a -> Series a
+  , cons1          -- :: Serial a => (a -> b) -> Series b
+  , cons2          -- :: (Serial a, Serial b) => (a -> b -> c) -> Series c
+  , cons3          -- :: ...
+  , cons4          -- :: ...
+  , cons5          -- :: ...
+  , Testable       -- :: class
+  , depthCheck     -- :: Testable a => Int -> a -> IO ()
+  , test           -- :: Testable a => a -> IO ()
+  , (==>)          -- :: Bool -> Bool -> Bool
+  , Prop           -- :: *
+  , lift           -- :: Bool -> Prop
+  , neg            -- :: Prop -> Prop
+  , (*&*)          -- :: Prop -> Prop -> Prop
+  , (*|*)          -- :: Prop -> Prop -> Prop
+  , (*=>*)         -- :: Prop -> Prop -> Prop
+  )
+  where
+
+import Monad
+import Control.Exception
+import System.Exit
+
+infixr 0 ==>, *=>*
+infixr 3 \/, *|*
+infixl 4 ><, *&*
+
+type Pos = [Int]
+
+data Term = Var Pos Type | Ctr Int [Term]
+
+data Type = SumOfProd [[Type]]
+
+type Series a = Int -> Cons a
+
+data Cons a = C Type ([[Term] -> a])
+
+class Serial a where
+  series :: Series a
+
+-- Series constructors
+
+cons :: a -> Series a
+cons a d = C (SumOfProd [[]]) [const a]
+
+(><) :: Series (a -> b) -> Series a -> Series b
+(f >< a) d = C (SumOfProd [ta:p | d > 0, p <- ps]) cs
+  where
+    C (SumOfProd ps) cfs = f d
+    C ta cas = a (d-1)
+    cs = [\(x:xs) -> cf xs (conv cas x) | d > 0, cf <- cfs]
+
+(\/) :: Series a -> Series a -> Series a
+(a \/ b) d = C (SumOfProd (ssa ++ ssb)) (ca ++ cb)
+  where
+    C (SumOfProd ssa) ca = a d
+    C (SumOfProd ssb) cb = b d
+
+conv :: [[Term] -> a] -> Term -> a
+conv cs (Var p _) = error ('\0':map toEnum p)
+conv cs (Ctr i xs) = (cs !! i) xs
+
+drawnFrom :: [a] -> Cons a
+drawnFrom xs = C (SumOfProd (map (const []) xs)) (map const xs)
+
+-- Helpers, a la SmallCheck
+
+cons0 :: a -> Series a
+cons0 f = cons f
+
+cons1 :: Serial a => (a -> b) -> Series b
+cons1 f = cons f >< series
+
+cons2 :: (Serial a, Serial b) => (a -> b -> c) -> Series c
+cons2 f = cons f >< series >< series
+
+cons3 :: (Serial a, Serial b, Serial c) => (a -> b -> c -> d) -> Series d
+cons3 f = cons f >< series >< series >< series
+
+cons4 :: (Serial a, Serial b, Serial c, Serial d) =>
+  (a -> b -> c -> d -> e) -> Series e
+cons4 f = cons f >< series >< series >< series >< series
+
+cons5 :: (Serial a, Serial b, Serial c, Serial d, Serial e) =>
+  (a -> b -> c -> d -> e -> f) -> Series f
+cons5 f = cons f >< series >< series >< series >< series >< series
+
+-- Standard instances
+
+instance Serial () where
+  series = cons0 ()
+
+instance Serial Bool where
+  series = cons0 False \/ cons0 True
+
+instance Serial a => Serial (Maybe a) where
+  series = cons0 Nothing \/ cons1 Just
+
+instance (Serial a, Serial b) => Serial (Either a b) where
+  series = cons1 Left \/ cons1 Right
+
+instance Serial a => Serial [a] where
+  series = cons0 [] \/ cons2 (:)
+
+instance (Serial a, Serial b) => Serial (a, b) where
+  series = cons2 (,) . (+1)
+
+instance (Serial a, Serial b, Serial c) => Serial (a, b, c) where
+  series = cons3 (,,) . (+1)
+
+instance (Serial a, Serial b, Serial c, Serial d) =>
+    Serial (a, b, c, d) where
+  series = cons4 (,,,) . (+1)
+
+instance (Serial a, Serial b, Serial c, Serial d, Serial e) =>
+    Serial (a, b, c, d, e) where
+  series = cons5 (,,,,) . (+1)
+
+instance Serial Int where
+  series d = drawnFrom [-d..d]
+
+instance Serial Integer where
+  series d = drawnFrom (map toInteger [-d..d])
+
+instance Serial Char where
+  series d = drawnFrom (take (d+1) ['a'..])
+
+instance Serial Float where
+  series d = drawnFrom (floats d)
+
+instance Serial Double where
+  series d = drawnFrom (floats d)
+
+floats :: RealFloat a => Int -> [a]
+floats d = [ encodeFloat sig exp
+           | sig <- map toInteger [-d..d]
+           , exp <- [-d..d]
+           , odd sig || sig == 0 && exp == 0
+           ]
+
+-- Term refinement
+
+refine :: Term -> Pos -> [Term]
+refine (Var p (SumOfProd ss)) [] = new p ss
+refine (Ctr c xs) p = map (Ctr c) (refineList xs p)
+
+refineList :: [Term] -> Pos -> [[Term]]
+refineList xs (i:is) = [ls ++ y:rs | y <- refine x is]
+  where (ls, x:rs) = splitAt i xs
+
+new :: Pos -> [[Type]] -> [Term]
+new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
+           | (c, ts) <- zip [0..] ps ]
+
+-- Find total instantiations of a partial value
+
+total :: Term -> [Term] 
+total val = tot val
+  where
+    tot (Ctr c xs) = [Ctr c ys | ys <- mapM tot xs] 
+    tot (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- tot x]
+
+-- Answers
+
+answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b
+answer a known unknown =
+  do res <- try (evaluate a)
+     case res of
+       Right b -> known b
+       Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
+       Left e -> throw e
+
+-- Refute
+
+refute :: Result -> IO Int
+refute r = ref (args r)
+  where
+    ref xs = eval (apply r xs) known unknown
+      where
+        known True = return 1
+        known False = report
+        unknown p = sumMapM ref 1 (refineList xs p)
+
+        report =
+          do putStr "Counter example found"
+             case [ys | ys <- mapM total xs] of
+               [] -> putStrLn ", but too deep to fully instantiate"
+               as:_ -> do putStrLn ":"
+                          mapM_ putStrLn $ zipWith ($) (showArgs r) as
+             exitWith ExitSuccess
+
+sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int
+sumMapM f n [] = return n
+sumMapM f n (a:as) = seq n (do m <- f a ; sumMapM f (n+m) as)
+
+-- Properties with parallel conjunction (Lindblad TFP'07)
+
+data Prop = Bool Bool | Neg Prop | And Prop Prop | ParAnd Prop Prop
+
+eval :: Prop -> (Bool -> IO a) -> (Pos -> IO a) -> IO a
+eval p k u = answer p (\p -> eval' p k u) u
+
+eval' (Bool b) k u = answer b k u
+eval' (Neg p) k u = eval p (k . not) u
+eval' (And p q) k u = eval p (\b -> if b then eval q k u else k b) u
+eval' (ParAnd p q) k u = eval p (\b -> if b then eval q k u else k b) unknown
+  where
+    unknown pos = eval q (\b -> if b then u pos else k b) (\_ -> u pos)
+
+lift :: Bool -> Prop
+lift b = Bool b
+
+neg :: Prop -> Prop
+neg p = Neg p
+
+(*&*), (*|*), (*=>*) :: Prop -> Prop -> Prop
+p *&* q = ParAnd p q
+p *|* q = neg (neg p *&* neg q)
+p *=>* q = neg (p *&* neg q)
+
+-- Boolean implication
+
+(==>) :: Bool -> Bool -> Bool
+False ==> _ = True
+True ==> x = x
+
+-- Testable
+
+data Result =
+  Result { args     :: [Term]
+         , showArgs :: [Term -> String]
+         , apply    :: [Term] -> Prop
+         }
+
+data Property = P (Int -> Int -> Result)
+
+run :: Testable a => ([Term] -> a) -> Int -> Int -> Result
+run a = f where P f = property a
+
+class Testable a where
+  property :: ([Term] -> a) -> Property
+
+instance Testable Bool where
+  property apply = P $ \n d -> Result [] [] (Bool . apply . reverse)
+
+instance Testable Prop where
+  property apply = P $ \n d -> Result [] [] (apply . reverse)
+
+instance (Show a, Serial a, Testable b) => Testable (a -> b) where
+  property f = P $ \n d ->
+    let C t c = series d
+        c' = conv c
+        r = run (\(x:xs) -> f xs (c' x)) (n+1) d
+    in  r { args = Var [n] t : args r, showArgs = (show . c') : showArgs r }
+
+-- Top-level interface
+
+depthCheck :: Testable a => Int -> a -> IO ()
+depthCheck d p =
+  do n <- refute $ run (const p) 0 d
+     putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d
+
+test :: Testable a => a -> IO ()
+test p = mapM_ (`depthCheck` p) [0..]
diff --git a/Test/LazySmallCheck/Generic.hs b/Test/LazySmallCheck/Generic.hs
new file mode 100644
--- /dev/null
+++ b/Test/LazySmallCheck/Generic.hs
@@ -0,0 +1,143 @@
+{-# OPTIONS -fglasgow-exts #-}
+
+module Test.LazySmallCheck.Generic
+  ( depthCheck  -- :: (Data a, Show a) => Int -> (a -> Bool) -> IO [a]
+  , (==>)       -- :: Bool -> Bool -> Bool
+  ) where
+
+import Data.Maybe
+import Data.Generics
+import Control.Exception
+import Control.Monad
+import System.Exit
+
+uniquePrefix = "UP:"
+
+lenUniquePrefix = length uniquePrefix
+
+type Position = String
+
+initPData :: a
+initPData = error uniquePrefix
+
+data HLP a = HLP Int (Either a [a])
+
+refinePData :: Data a => String -> Int -> Position -> a -> [a]
+refinePData s d = r
+ where
+  depleft = d - (length s - lenUniquePrefix)
+  r :: Data a => Position -> a -> [a]
+  r [] x =
+    let dt = dataTypeOf x
+    in case dataTypeRep dt of
+         AlgRep cons ->
+           let cons = dataTypeConstrs dt
+               z x = (0, x)
+               k (i, g) = (i + 1, g (error $ s ++ [toEnum i]))
+               xs' = map (gunfold k z) cons
+           in  if   depleft > 0
+               then map snd xs'
+               else mapMaybe (\(ncon, x') ->
+                                 if   ncon == 0
+                                 then Just x'
+                                 else Nothing) xs'
+         IntRep -> mkPrim dt (mkIntConstr dt . toInteger)
+                             [-depleft .. depleft]
+         StringRep -> mkPrim dt (mkStringConstr dt . (:[]))
+                                (take (depleft+1) ['a' .. 'z'])
+         _ -> error $ "LazySmallCheck.Generic: Can't generate type "
+                   ++ dataTypeName dt
+  r (c:ps) x =
+   let p = fromEnum c
+       z y = HLP 0 (Left y)
+       k (HLP i (Left xs)) y | i == p = HLP (i + 1) (Right $ map xs (r ps y))
+       k (HLP i (Left xs)) y = HLP (i + 1) (Left $ xs y)
+       k (HLP i (Right xss)) y = HLP (i + 1) (Right $ map (\xs -> xs y) xss)
+       HLP _ (Right x') = gfoldl k z x
+   in  x'
+
+mkPrim dt mk vs = map (\i -> fromJust $ gunfold undefined Just $ mk i) vs
+
+--
+
+mapVars :: Data a => (forall b . Data b => b -> IO b) -> a -> IO a
+mapVars f = gmapM (\x -> Control.Exception.catch
+  (mapVars f x)
+  (\exc -> case exc of
+    ErrorCall s | take (length uniquePrefix) s == uniquePrefix ->
+     f x
+    _ -> throw exc
+  )
+ )
+
+-- Taken from Ralf Laemmel, SYB website
+-- Generate all terms of a given depth
+enumerate :: Data a => Int -> [a]
+enumerate 0 = []
+enumerate d = result
+   where
+     -- Getting hold of the result (type)
+     result = concat (map recurse cons')
+
+     -- Find all terms headed by a specific Constr
+     recurse :: Data a => Constr -> [a]
+     recurse con = gmapM (\_ -> enumerate (d-1)) 
+                         (fromConstr con)
+
+     -- We could also deal with primitive types easily.
+     -- Then we had to use cons' instead of cons.
+     --
+     cons' :: [Constr]
+     cons' = case dataTypeRep ty of
+              AlgRep cons -> cons
+              IntRep      -> map (mkIntConstr ty . toInteger) [-d .. d]
+              StringRep   -> map (mkStringConstr ty . (:[])) (take d ['a'..'z'])
+              --FloatRep  ->
+      where
+        ty = dataTypeOf (head result)     
+
+smallValue :: Data a => a
+smallValue = f 1
+ where
+  f d = case enumerate d of
+   [] -> f (d + 1)
+   (x:_) -> x
+
+smallInstance :: Data a => a -> IO a
+smallInstance = mapVars (\_ -> return smallValue)
+
+--
+
+refute :: (Show a, Data a) => Int -> (a -> Bool) -> IO Int
+refute d p = r initPData
+  where
+    r x = do res <- try (evaluate (p x))
+             case res of
+               Right True -> return 1
+               Right False -> stop x "Counter example found:"
+               Left (ErrorCall s)
+                 | take (lenUniquePrefix) s == uniquePrefix ->
+                     let pos = drop lenUniquePrefix s
+                     in  do ns <- mapM r (refinePData s d pos x)
+                            return (1 + sum ns)
+               Left e -> stop x "Property crashed on input:"
+
+    stop x s = do putStrLn s
+                  x' <- smallInstance x
+                  putStrLn (show x')
+                  exitWith ExitSuccess
+                     
+--
+
+depthCheck :: (Show a, Data a) => Int -> (a -> Bool) -> IO ()
+depthCheck d f = do count <- refute d f
+                    putStrLn $ "Completed " ++ show count
+                            ++  " tests without finding a counter example."
+
+--
+
+infixr 0 ==>
+
+(==>) :: Bool -> Bool -> Bool
+False ==> a = True
+True ==> a = a
diff --git a/benchmarks/Benchmark.hs b/benchmarks/Benchmark.hs
deleted file mode 100644
--- a/benchmarks/Benchmark.hs
+++ /dev/null
@@ -1,35 +0,0 @@
-import System
-import Data.List
-
-main :: IO ()
-main = do args <- getArgs
-          case args of
-            [checker, file] -> benchmark checker file
-            _ -> error usage
-
-usage = "Usage: runhugs Benchmark.hs "
-        ++ "[SmallCheck|LazySmallCheck|LazySmallCheck.Generic] FILE"
-
-benchmark checker file =
-  do extra <-
-      case checker of
-       "SmallCheck" -> return ""
-       "LazySmallCheck" -> return ""
-       "LazySmallCheck.Generic" -> return "import Data.Generics\n"
-       _ -> error usage
-     if '.' `elem` file then error "Filename should not contain '.'"
-                        else return ()
-     contents <- readFile (file ++ ".hs")
-     let props = nub $ filter ("prop_" `isPrefixOf`) (words contents)
-     writeFile (file ++ "2.hs") $  extra
-                                ++ "import System\n"
-                                ++ "import " ++ checker ++ "\n\n"
-                                ++ contents ++ "\n\n"
-                                ++ "main = do { [p, d] <- getArgs"
-                                ++ "          ; case p of { "
-                                ++ concatMap propAlt props
-                                ++ "_ -> error \"Unknown property\"}}"
-     system $ "ghc -fglasgow-exts -O2 --make " ++ file ++ "2.hs -o " ++ file
-     return ()
-
-propAlt p = "\"" ++ p ++ "\" -> " ++ "depthCheck (read d) " ++ p ++ ";"
diff --git a/benchmarks/Countdown.hs b/benchmarks/Countdown.hs
deleted file mode 100644
--- a/benchmarks/Countdown.hs
+++ /dev/null
@@ -1,187 +0,0 @@
------------------------------------------------------------------------------
---
---                           The Countdown Problem
---
---                               Graham Hutton
---                         University of Nottingham
---
---                               November 2001
---
------------------------------------------------------------------------------
-
------------------------------------------------------------------------------
--- Formally specifying the problem
------------------------------------------------------------------------------
-
-data Op               = Add | Sub | Mul | Div
-  deriving Eq
-
-valid                :: Op -> Int -> Int -> Bool
-valid Add _ _         = True
-valid Sub x y         = x > y
-valid Mul _ _         = True
-valid Div x y         = x `mod` y == 0
- 
-apply                :: Op -> Int -> Int -> Int
-apply Add x y         = x + y
-apply Sub x y         = x - y
-apply Mul x y         = x * y
-apply Div x y         = x `div` y
-
-data Expr             = Val Int | App Op Expr Expr
-  deriving Eq
-
-values               :: Expr -> [Int]
-values (Val n)        = [n]
-values (App _ l r)    = values l ++ values r
-
-eval                 :: Expr -> [Int]
-eval (Val n)          = [n | n > 0]
-eval (App o l r)      = [apply o x y | x <- eval l, y <- eval r, valid o x y]
-
-subbags              :: [a] -> [[a]]
-subbags xs            = [zs | ys <- subs xs, zs <- perms ys]
-
-subs                 :: [a] -> [[a]]
-subs []               = [[]]
-subs (x:xs)           = ys ++ map (x:) ys
-                        where
-                           ys = subs xs
-
-perms                :: [a] -> [[a]]
-perms []              = [[]]
-perms (x:xs)          = concat (map (interleave x) (perms xs))
-
-interleave           :: a -> [a] -> [[a]]
-interleave x []       = [[x]]
-interleave x (y:ys)   = (x:y:ys) : map (y:) (interleave x ys)
-
-solution             :: Expr -> [Int] -> Int -> Bool
-solution e ns n       = elem (values e) (subbags ns) && eval e == [n]
-
------------------------------------------------------------------------------
--- Brute force implementation
------------------------------------------------------------------------------
-
-split                :: [a] -> [([a],[a])]
-split []              = [([],[])]
-split (x:xs)          = ([],x:xs) : [(x:ls,rs) | (ls,rs) <- split xs]
-
-nesplit              :: [a] -> [([a],[a])]
-nesplit               = filter ne . split
-
-ne                   :: ([a],[b]) -> Bool
-ne (xs,ys)            = not (null xs || null ys)
-
-exprs                :: [Int] -> [Expr]
-exprs []              = []
-exprs [n]             = [Val n]
-exprs ns              = [e | (ls,rs) <- nesplit ns
-                           , l       <- exprs ls
-                           , r       <- exprs rs
-                           , e       <- combine l r]
-
-combine              :: Expr -> Expr -> [Expr]
-combine l r           = [App o l r | o <- ops]
- 
-ops                  :: [Op]
-ops                   = [Add,Sub,Mul,Div]
-
-solutions            :: [Int] -> Int -> [Expr]
-solutions ns n        = [e | ns' <- subbags ns, e <- exprs ns', eval e == [n]]
-
------------------------------------------------------------------------------
--- Fusing generation and evaluation
------------------------------------------------------------------------------
-
-type Result           = (Expr,Int)
-
-results              :: [Int] -> [Result]
-results []            = []
-results [n]           = [(Val n,n) | n > 0]
-results ns            = [res | (ls,rs) <- nesplit ns
-                             , lx      <- results ls
-                             , ry      <- results rs
-                             , res     <- combine' lx ry]
-
-combine'             :: Result -> Result -> [Result]
-combine' (l,x) (r,y)  = [(App o l r, apply o x y) | o <- ops, valid o x y]
-
-solutions'           :: [Int] -> Int -> [Expr]
-solutions' ns n       = [e | ns' <- subbags ns, (e,m) <- results ns', m == n]
-
------------------------------------------------------------------------------
--- Exploiting arithmetic properties
------------------------------------------------------------------------------
-
-valid'               :: Op -> Int -> Int -> Bool
-valid' Add x y        = x <= y
-valid' Sub x y        = x > y
-valid' Mul x y        = x /= 1 && y /= 1 && x <= y
-valid' Div x y        = y /= 1 && x `mod` y == 0
-
-eval'                :: Expr -> [Int]
-eval' (Val n)         = [n | n > 0]
-eval' (App o l r)     = [apply o x y | x <- eval' l, y <- eval' r, valid' o x y]
-
-solution'            :: Expr -> [Int] -> Int -> Bool
-solution' e ns n      = elem (values e) (subbags ns) && eval' e == [n]
-
-results'             :: [Int] -> [Result]
-results' []           = []
-results' [n]          = [(Val n,n) | n > 0]
-results' ns           = [res | (ls,rs) <- nesplit ns
-                             , lx      <- results' ls
-                             , ry      <- results' rs
-                             , res     <- combine'' lx ry]
-
-combine''            :: Result -> Result -> [Result]
-combine'' (l,x) (r,y) = [(App o l r, apply o x y) | o <- ops, valid' o x y]
-
-solutions''          :: [Int] -> Int -> [Expr]
-solutions'' ns n      = [e | ns' <- subbags ns, (e,m) <- results' ns', m == n]
-
------------------------------------------------------------------------------
--- Interactive version for testing
------------------------------------------------------------------------------
-
-instance Show Op where
-   show Add           = "+"
-   show Sub           = "-"
-   show Mul           = "*"
-   show Div           = "/"
-
-instance Show Expr where
-   show (Val n)       = show n
-   show (App o l r)   = bracket l ++ show o ++ bracket r
-                        where
-                           bracket (Val n) = show n
-                           bracket e       = "(" ++ show e ++ ")"
-
-display              :: [Expr] -> IO ()
-display []            = putStr "\nThere are no solutions.\n\n"
-display (e:es)        = do putStr "\nOne possible solution is "
-                           putStr (show e)
-	                   putStr ".\n\nPress return to continue searching..."
-                           getLine
-                           putStr "\n"
-                           if null es then
-                               putStr "There are no more solutions.\n\n"
-                            else
-                               do sequence [print e | e <- es]
-                                  putStr "\nThere were "
-                                  putStr (show (length (e:es)))
-                                  putStr " solutions in total.\n\n"
-
-prop_lemma1 :: ([Int], [Int], [Int]) -> Bool
-prop_lemma1 (xs, ys, zs) = ((xs,ys) `elem` split zs) == (xs ++ ys == zs)
-
-prop_lemma3 :: ([Int], [Int], [Int]) -> Bool
-prop_lemma3 (xs, ys, zs) = ((xs, ys) `elem` nesplit zs)
-                             == (xs ++ ys == zs && ne (xs, ys))
-
-prop_lemma4 :: ([Int], [Int], [Int]) -> Bool
-prop_lemma4 (xs, ys, zs) = ((xs, ys) `elem` nesplit zs) ==>
-                             (length xs < length zs && length ys < length zs)
-
-prop_solutions (ns, m) = solutions ns m == solutions' ns m
diff --git a/benchmarks/List.hs b/benchmarks/List.hs
deleted file mode 100644
--- a/benchmarks/List.hs
+++ /dev/null
@@ -1,20 +0,0 @@
-ord [] = True
-ord [x] = True
-ord (x:y:ys) = x <= y && ord (y:ys)
-
-insert x [] = [x]
-insert x (y:ys)
-  | x <= y = x:y:ys
-  | otherwise = y:insert x ys
-
-merge [] ys = ys
-merge xs [] = xs
-merge (x:xs) (y:ys)
-  | x <= y = x : merge xs (y:ys)
-  | otherwise = y : merge (x:xs) ys
-
-prop_ordInsert :: (Char, [Char]) -> Bool
-prop_ordInsert (x, xs) = ord xs ==> ord (insert x xs)
-
-prop_ordMerge :: ([Char], [Char]) -> Bool
-prop_ordMerge (xs, ys) = ord xs && ord ys ==> ord (merge xs ys)
diff --git a/benchmarks/Mux.hs b/benchmarks/Mux.hs
deleted file mode 100644
--- a/benchmarks/Mux.hs
+++ /dev/null
@@ -1,33 +0,0 @@
-import Data.List
-
--- Binary multiplexor
-
-tree              :: (a -> a -> a) -> [a] -> a
-tree f [x]        =  x
-tree f (x:y:ys)   =  tree f (ys ++ [f x y])
-
-unaryMux          :: [Bool] -> [[Bool]] -> [Bool]
-unaryMux sel xs   =  map (tree (||))
-                  $  transpose
-                  $  zipWith (\s x -> map (s &&) x) sel xs
-
-decode []         =  [True]
-decode [x]        =  [not x,x]
-decode (x:xs)     =  concatMap (\y -> [not x && y,x && y]) rest
-  where
-    rest          =  decode xs
-
-binaryMux         :: [Bool] -> [[Bool]] -> [Bool]
-binaryMux sel xs  =  unaryMux (decode sel) xs
-
-num               :: [Bool] -> Int
-num []            =  0
-num (a:as)        =  (if a then 1 else 0) + 2 * num as
-
--- Property
-
-prop_binMux :: ([Bool], [[Bool]]) -> Bool
-prop_binMux (sel, xs) =
-     ((length xs == 2 ^ length sel)
-  && all ((== length (head xs)) . length) xs)
-  ==> (binaryMux sel xs == xs !! num sel)
diff --git a/benchmarks/RegExp.hs b/benchmarks/RegExp.hs
deleted file mode 100644
--- a/benchmarks/RegExp.hs
+++ /dev/null
@@ -1,124 +0,0 @@
-(<==>) :: Bool -> Bool -> Bool
-a <==> b = (a ==> b) && (b ==> a)
-
--- ---------------------
-
-data Nat = Zer
-         | Suc Nat
-  deriving Show
---  deriving (Show,Data, Typeable)
-
-
-instance Serial Nat where
-  series = cons0 Zer \/ cons1 Suc
-
-sub :: Nat -> Nat -> Nat
-sub x y =
- case y of
-  Zer -> x
-  Suc y' -> case x of
-   Zer -> Zer
-   Suc x' -> sub x' y'
-
-data Sym = N0
-         | N1 Sym
- deriving (Eq, Show)
--- deriving (Eq, Show, Data, Typeable)
-
-instance Serial Sym where
-  series = cons0 N0 \/ cons1 N1
-
--- deriving Eq
-
-data RE = Sym Sym
-        | Or RE RE
-        | Seq RE RE
-        | And RE RE
-        | Star RE
-        | Empty
-  deriving Show
---  deriving (Data, Typeable, Show)
-
-{-
-instance Serial RE where
-  series =  cons0 Empty
-         \/ cons1 Star
-         \/ cons2 And
-         \/ cons2 Seq
-         \/ cons2 Or
-         \/ cons1 Sym
--}
-
-instance Serial RE where
-  series = cons1 Sym
-        \/ cons2 Or
-        \/ cons2 Seq
-        \/ cons2 And
-        \/ cons1 Star
-        \/ cons0 Empty
-
-
-
-accepts :: RE -> [Sym] -> Bool
-accepts re ss =
- case re of
-  Sym n -> case ss of
-   [] -> False
-   (n':ss') -> n == n' && null ss'
-  Or re1 re2 -> accepts re1 ss || accepts re2 ss
-  Seq re1 re2 -> seqSplit re1 re2 [] ss
-  And re1 re2 -> accepts re1 ss && accepts re2 ss
-  Star re' -> case ss of
-   [] -> True
-   (s:ss') -> seqSplit re' re (s:[]) ss'
-    -- accepts Empty ss || accepts (Seq re' re) ss
-  Empty -> null ss
-
-seqSplit :: RE -> RE -> [Sym] -> [Sym] -> Bool
-seqSplit re1 re2 ss2 ss =
- seqSplit'' re1 re2 ss2 ss || seqSplit' re1 re2 ss2 ss
-
-seqSplit'' :: RE -> RE -> [Sym] -> [Sym] -> Bool
-seqSplit'' re1 re2 ss2 ss = accepts re1 ss2 && accepts re2 ss
-
-seqSplit' :: RE -> RE -> [Sym] -> [Sym] -> Bool
-seqSplit' re1 re2 ss2 ss =
- case ss of
-  [] -> False
-  (n:ss') ->
-   seqSplit re1 re2 (ss2 ++ [n]) ss'
-
-rep :: Nat -> RE -> RE
-rep n re =
- case n of
-  Zer -> Empty
-  Suc n' -> Seq re (rep n' re)
-
-repMax :: Nat -> RE -> RE
-repMax n re =
- case n of
-  Zer -> Empty
-  Suc n' -> Or (rep n re) (repMax n' re)
-
-repInt' :: Nat -> Nat -> RE -> RE
-repInt' n k re =
- case k of
-  Zer -> rep n re
-  Suc k' -> Or (rep n re) (repInt' (Suc n) k' re)
-
-repInt :: Nat -> Nat -> RE -> RE
-repInt n k re = repInt' n (sub k n) re
-
--- ---------------------
-
-
--- main_1
-prop_regex :: (Nat, Nat, RE, RE, [Sym]) -> Bool
-prop_regex (n, k, p, q, s) =  r -- if r then True else True
-  where
-    r = (accepts (repInt n k (And p q)) s)
-          <==> (accepts (And (repInt n k p) (repInt n k q)) s)
---(accepts (And (repInt n k p) (repInt n k q)) s) <==> (accepts (repInt n k (And p q)) s)
-
-a_sol = (Zer, Suc (Suc Zer), Sym N0, Seq (Sym N0) (Sym N0), [N0, N0])
-
diff --git a/benchmarks/Sad.hs b/benchmarks/Sad.hs
deleted file mode 100644
--- a/benchmarks/Sad.hs
+++ /dev/null
@@ -1,92 +0,0 @@
--- We take the following specification for the sum of absolute
--- differences, and develop a program that generates circuits that
--- have 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)
diff --git a/benchmarks/SumPuz.hs b/benchmarks/SumPuz.hs
deleted file mode 100644
--- a/benchmarks/SumPuz.hs
+++ /dev/null
@@ -1,68 +0,0 @@
-import Data.List((\\))
-import Char(isAlpha, chr, ord)
-import Maybe(fromJust)
-
-type Soln = [(Char, Int)]
-
-solve :: String -> String
-solve p =
-  display p (solutions xs ys zs 0 [])
-  where
-  [xs,ys,zs] = map reverse (words (filter (`notElem` "+=") p))
-
-display :: String -> [Soln] -> String
-display p []    = "No solution!"
-display p (s:_) =
-  map soln p
-  where
-  soln c = if isAlpha c then chr (ord '0' + img s c) else c
-
-rng :: Soln -> [Int]
-rng = map snd
-
-img :: Soln -> Char -> Int
-img lds l = fromJust (lookup l lds)
-
-bindings :: Char -> [Int] -> Soln -> [Soln]
-bindings l ds lds =
-  case lookup l lds of
-  Nothing  -> map (:lds) (zip (repeat l) (ds \\ rng lds))
-  Just d -> if d `elem` ds then [lds] else []
-
-solutions :: String -> String -> String -> Int -> Soln -> [Soln]
-solutions [] [] []  c lds = if c==0 then [lds] else []
-solutions [] [] [z] c lds = if c==1 then bindings z [1] lds else []
-solutions (x:xs) (y:ys) (z:zs) c lds =
-  solns `ofAll`
-  bindings y [(if null ys then 1 else 0)..9] `ofAll`
-  bindings x [(if null xs then 1 else 0)..9] lds
-  where  
-  solns s = 
-    solutions xs ys zs (xy `div` 10) `ofAll` bindings z [xy `mod` 10] s
-    where    
-    xy = img s x + img s y + c
-
-infixr 5 `ofAll`
-ofAll :: (a -> [b]) -> [a] -> [b]
-ofAll = concatMap
-
--- Property
-
-find :: String -> String -> String -> [Soln]
-find xs ys zs = solutions (reverse xs) (reverse ys) (reverse zs) 0 []
-
-val :: Soln -> String -> Int
-val s "" = 0
-val s xs = read (concatMap (show . img s) xs)
-
-prop_Sound :: (String, String, String) -> Bool
-prop_Sound (xs, ys, zs) =
-      length xs == length ys
-   && (diff == 0 || diff == 1)
-   && not (null sols)
-  ==> and [ val s xs + val s ys == val s zs
-          | s <- sols
-          ]
-  where
-    sols = find xs ys zs
-    diff = length zs - length xs
diff --git a/benchmarks/clean.sh b/benchmarks/clean.sh
deleted file mode 100644
--- a/benchmarks/clean.sh
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/bin/sh
-
-rm -f *.hi *.o List Countdown *2.hs RegExp Mux SumPuz Sad
-cd LazySmallCheck
-rm -f *.hi *.o
diff --git a/examples/Catch.hs b/examples/Catch.hs
new file mode 100644
--- /dev/null
+++ b/examples/Catch.hs
@@ -0,0 +1,112 @@
+module Catch where
+
+-- A property of Catch by Neil Mitchell
+
+import Data.List
+import Data.Maybe
+
+
+-- Property
+
+data Prop a = Or [Prop a] | And [Prop a] | Lit a
+
+andP = And
+orP = Or
+lit = Lit
+true = And []
+
+
+-- Constraints
+
+data Sat a = Sat a Constraint
+
+substP ::  Eq alpha => [(alpha,beta)] -> Prop (Sat alpha) -> Prop (Sat beta)
+substP xs (Lit (Sat i k)) = Lit $ Sat (fromJust $ lookup i xs) k
+substP xs (And p) = And $ map (substP xs) p
+substP xs (Or p) = Or $ map (substP xs) p
+
+
+-- MP constraints
+
+type Constraint  =  [Val]
+data Val         =  [Pattern] :* [Pattern] |  Any deriving (Show,Eq)
+data Pattern     =  Pattern CtorName [Val] deriving (Show,Eq)
+
+
+(<|) :: CtorName -> Constraint -> Prop (Sat Int)
+c <| vs = orP (map f vs)
+    where
+    (rec,non) = partition (isRec . (,) c) [0..arity c-1]
+
+    f Any = true
+    f (ms_1 :* ms_2) = orP  [ andP $ map lit $ g vs_1
+                            | Pattern c_1 vs_1 <- ms_1, c_1 == c]
+        where g vs =  zipWith Sat non (map (:[]) vs) ++
+                      map (`Sat` [ms_2 :* ms_2]) rec
+
+mergeVal :: Val -> Val -> Val
+(a_1 :* b_1)  `mergeVal`  (a_2 :* b_2)  = merge a_1 a_2 :* merge b_1 b_2
+x             `mergeVal`  y             = if x == Any then y else x
+
+merge :: [Pattern] -> [Pattern] -> [Pattern]
+merge  ms_1 ms_2 = [Pattern c_1 (zipWith mergeVal vs_1 vs_2) |
+       Pattern c_1 vs_1 <- ms_1, Pattern c_2 vs_2 <- ms_2, c_1 == c_2]
+
+validConstraint = all validVal
+validVal Any = True
+validVal (ms1 :* ms2) = validPatterns ms1 && validPatterns ms2
+validPatterns = all validPattern
+validPattern (Pattern c xs) = (fields c == length xs) && all validVal xs
+
+
+-- Evaluator
+
+data Value  =  Value CtorName [Value]
+            |  Bottom
+               deriving (Eq,Show)
+
+sat :: Sat Value -> Bool
+sat (Sat Bottom        k) = True
+sat (Sat (Value c xs)  k) = sat' $ substP (zip [0..] xs) (c <| k)
+
+sat' :: Prop (Sat Value) -> Bool
+sat' (And xs) = all sat' xs
+sat' (Or xs) = any sat' xs
+sat' (Lit x) = sat x
+
+
+-- Core language
+
+data CtorName = Ctor | CtorN | CtorR | CtorNR
+                deriving (Show,Eq)
+
+arity Ctor = 0
+arity CtorN = 1
+arity CtorR = 1
+arity CtorNR = 2
+
+fields Ctor = 0
+fields CtorN = 1
+fields CtorR = 0
+fields CtorNR = 1
+
+isRec (CtorR,  0) = True
+isRec (CtorNR, 1) = True
+isRec _ = False
+
+validValue :: Value -> Bool
+validValue Bottom = True
+validValue (Value c xs) = (arity c == length xs) && all validValue xs
+
+
+-- Properties
+
+infixr 0 -->
+False --> _ = True
+True --> x = x
+
+prop :: (Value, [Pattern], [Pattern]) -> Bool
+prop (v,ms1,ms2) = (validValue v && validPatterns ms1 && validPatterns ms2 &&
+                   sat (Sat v [ms :* ms])) --> sat (Sat v [ms1 :* ms2])
+    where
+        ms = merge ms1 ms2
diff --git a/examples/Countdown.hs b/examples/Countdown.hs
new file mode 100644
--- /dev/null
+++ b/examples/Countdown.hs
@@ -0,0 +1,195 @@
+module Countdown where
+
+-----------------------------------------------------------------------------
+--
+--                           The Countdown Problem
+--
+--                               Graham Hutton
+--                         University of Nottingham
+--
+--                               November 2001
+--
+-----------------------------------------------------------------------------
+
+-----------------------------------------------------------------------------
+-- Formally specifying the problem
+-----------------------------------------------------------------------------
+
+data Op               = Add | Sub | Mul | Div
+  deriving Eq
+
+valid                :: Op -> Int -> Int -> Bool
+valid Add _ _         = True
+valid Sub x y         = x > y
+valid Mul _ _         = True
+valid Div x y         = x `mod` y == 0
+
+apply                :: Op -> Int -> Int -> Int
+apply Add x y         = x + y
+apply Sub x y         = x - y
+apply Mul x y         = x * y
+apply Div x y         = x `div` y
+
+data Expr             = Val Int | App Op Expr Expr
+  deriving Eq
+
+values               :: Expr -> [Int]
+values (Val n)        = [n]
+values (App _ l r)    = values l ++ values r
+
+eval                 :: Expr -> [Int]
+eval (Val n)          = [n | n > 0]
+eval (App o l r)      = [apply o x y | x <- eval l, y <- eval r, valid o x y]
+
+subbags              :: [a] -> [[a]]
+subbags xs            = [zs | ys <- subs xs, zs <- perms ys]
+
+subs                 :: [a] -> [[a]]
+subs []               = [[]]
+subs (x:xs)           = ys ++ map (x:) ys
+                        where
+                           ys = subs xs
+
+perms                :: [a] -> [[a]]
+perms []              = [[]]
+perms (x:xs)          = concat (map (interleave x) (perms xs))
+
+interleave           :: a -> [a] -> [[a]]
+interleave x []       = [[x]]
+interleave x (y:ys)   = (x:y:ys) : map (y:) (interleave x ys)
+
+solution             :: Expr -> [Int] -> Int -> Bool
+solution e ns n       = elem (values e) (subbags ns) && eval e == [n]
+
+-----------------------------------------------------------------------------
+-- Brute force implementation
+-----------------------------------------------------------------------------
+
+split                :: [a] -> [([a],[a])]
+split []              = [([],[])]
+split (x:xs)          = ([],x:xs) : [(x:ls,rs) | (ls,rs) <- split xs]
+
+nesplit              :: [a] -> [([a],[a])]
+nesplit               = filter ne . split
+
+ne                   :: ([a],[b]) -> Bool
+ne (xs,ys)            = not (null xs || null ys)
+
+exprs                :: [Int] -> [Expr]
+exprs []              = []
+exprs [n]             = [Val n]
+exprs ns              = [e | (ls,rs) <- nesplit ns
+                           , l       <- exprs ls
+                           , r       <- exprs rs
+                           , e       <- combine l r]
+
+combine              :: Expr -> Expr -> [Expr]
+combine l r           = [App o l r | o <- ops]
+
+ops                  :: [Op]
+ops                   = [Add,Sub,Mul,Div]
+
+solutions            :: [Int] -> Int -> [Expr]
+solutions ns n        = [e | ns' <- subbags ns, e <- exprs ns', eval e == [n]]
+
+-----------------------------------------------------------------------------
+-- Fusing generation and evaluation
+-----------------------------------------------------------------------------
+
+type Result           = (Expr,Int)
+
+results              :: [Int] -> [Result]
+results []            = []
+results [n]           = [(Val n,n) | n > 0]
+results ns            = [res | (ls,rs) <- nesplit ns
+                             , lx      <- results ls
+                             , ry      <- results rs
+                             , res     <- combine' lx ry]
+
+combine'             :: Result -> Result -> [Result]
+combine' (l,x) (r,y)  = [(App o l r, apply o x y) | o <- ops, valid o x y]
+
+solutions'           :: [Int] -> Int -> [Expr]
+solutions' ns n       = [e | ns' <- subbags ns, (e,m) <- results ns', m == n]
+
+-----------------------------------------------------------------------------
+-- Exploiting arithmetic properties
+-----------------------------------------------------------------------------
+
+valid'               :: Op -> Int -> Int -> Bool
+valid' Add x y        = x <= y
+valid' Sub x y        = x > y
+valid' Mul x y        = x /= 1 && y /= 1 && x <= y
+valid' Div x y        = y /= 1 && x `mod` y == 0
+
+eval'                :: Expr -> [Int]
+eval' (Val n)         = [n | n > 0]
+eval' (App o l r)     = [apply o x y | x <- eval' l, y <- eval' r, valid' o x y]
+
+solution'            :: Expr -> [Int] -> Int -> Bool
+solution' e ns n      = elem (values e) (subbags ns) && eval' e == [n]
+
+results'             :: [Int] -> [Result]
+results' []           = []
+results' [n]          = [(Val n,n) | n > 0]
+results' ns           = [res | (ls,rs) <- nesplit ns
+                             , lx      <- results' ls
+                             , ry      <- results' rs
+                             , res     <- combine'' lx ry]
+
+combine''            :: Result -> Result -> [Result]
+combine'' (l,x) (r,y) = [(App o l r, apply o x y) | o <- ops, valid' o x y]
+
+solutions''          :: [Int] -> Int -> [Expr]
+solutions'' ns n      = [e | ns' <- subbags ns, (e,m) <- results' ns', m == n]
+
+-----------------------------------------------------------------------------
+-- Interactive version for testing
+-----------------------------------------------------------------------------
+
+instance Show Op where
+   show Add           = "+"
+   show Sub           = "-"
+   show Mul           = "*"
+   show Div           = "/"
+
+instance Show Expr where
+   show (Val n)       = show n
+   show (App o l r)   = bracket l ++ show o ++ bracket r
+                        where
+                           bracket (Val n) = show n
+                           bracket e       = "(" ++ show e ++ ")"
+
+display              :: [Expr] -> IO ()
+display []            = putStr "\nThere are no solutions.\n\n"
+display (e:es)        = do putStr "\nOne possible solution is "
+                           putStr (show e)
+	                   putStr ".\n\nPress return to continue searching..."
+                           getLine
+                           putStr "\n"
+                           if null es then
+                               putStr "There are no more solutions.\n\n"
+                            else
+                               do sequence [print e | e <- es]
+                                  putStr "\nThere were "
+                                  putStr (show (length (e:es)))
+                                  putStr " solutions in total.\n\n"
+
+-- Properties
+
+infixr 0 -->
+False --> _ = True
+True --> x = x
+
+prop_lemma1 :: ([Int], [Int], [Int]) -> Bool
+prop_lemma1 (xs, ys, zs) = ((xs,ys) `elem` split zs) == (xs ++ ys == zs)
+
+prop_lemma3 :: ([Int], [Int], [Int]) -> Bool
+prop_lemma3 (xs, ys, zs) = ((xs, ys) `elem` nesplit zs)
+                             == (xs ++ ys == zs && ne (xs, ys))
+
+prop_lemma4 :: ([Int], [Int], [Int]) -> Bool
+prop_lemma4 (xs, ys, zs) = ((xs, ys) `elem` nesplit zs) -->
+                             (length xs < length zs && length ys < length zs)
+
+prop_solutions (ns, m) = solutions ns m == solutions' ns m
diff --git a/examples/Huffman.hs b/examples/Huffman.hs
new file mode 100644
--- /dev/null
+++ b/examples/Huffman.hs
@@ -0,0 +1,86 @@
+module Huffman where
+
+-- A Huffman codec, slightly adapted from Bird
+-- (with properties added)
+
+data BTree a = Leaf a | Fork (BTree a) (BTree a)
+  deriving Show
+
+decode t bs = if null bs then [] else dec t t bs
+
+dec (Leaf x) t bs = x : decode t bs
+dec (Fork xt yt) t (b:bs) = dec (if b then yt else xt) t bs
+
+encode t cs = enc (codetable t) cs
+
+enc table [] = []
+enc table (c:cs) = (table ! c) ++ enc table cs
+
+((x, bs) : xbs) ! y = if x == y then bs else xbs ! y
+
+codetable t = tab [] t
+
+tab p (Leaf x) = [(x,p)]
+tab p (Fork xt yt) = tab (p++[False]) xt ++ tab (p++[True]) yt
+
+collate [] = []
+collate (c:cs) = insert (1+n, Leaf c) (collate ds)
+  where (n, ds) = count c cs
+
+count x [] = (0, [])
+count x (y:ys) = if x == y then (1+n, zs) else (n, y:zs)
+  where (n, zs) = count x ys
+
+insert (w, x) [] = [(w, x)]
+insert (w0, x) ((w1, y):wys)
+  | w0 <= w1 = (w0, x) : (w1, y) : wys
+  | otherwise = (w1, y) : insert (w0, x) wys
+
+hufftree cs = mkHuff (collate cs)
+
+mkHuff [(w, t)] = t
+mkHuff ((w0, t0):(w1, t1):wts) =
+  mkHuff (insert (w0+w1, Fork t0 t1) wts)
+
+-- Properties
+
+infixr 0 -->
+False --> _ = True
+True --> x = x
+
+prop_decEnc cs = length h > 1 --> (decode t (encode t cs) == cs)
+  where
+    h = collate cs
+    t = mkHuff h
+    types = cs :: String
+
+prop_optimal (cs, t) =
+    t `treeOf` h --> cost h t >= cost h (mkHuff h)
+  where
+    h = collate cs
+    types = cs :: String
+
+-- Cost
+
+cost h t = cost' h (codetable t)
+
+cost' h [] = 0
+cost' h ((c, bs):cbs) = (n * length bs) + cost' h cbs
+  where
+    n = head [n | (n, Leaf sym) <- h, sym == c]
+
+leaves (Leaf c) = [c]
+leaves (Fork xt yt) = leaves xt ++ leaves yt
+
+treeOf t h = leaves t === [c | (_, Leaf c) <- h]
+
+[] === [] = True
+(x:xs) === ys = case del x ys of
+                  Nothing -> False
+                  Just zs -> xs === zs
+_ === _ = False
+
+del x [] = Nothing
+del x (y:ys) = if x == y then Just ys else case del x ys of
+                                             Nothing -> Nothing
+                                             Just zs -> Just (y:zs)
diff --git a/examples/ListSet.hs b/examples/ListSet.hs
new file mode 100644
--- /dev/null
+++ b/examples/ListSet.hs
@@ -0,0 +1,34 @@
+module ListSet where
+
+type Set a = [a]
+
+empty :: Set a
+empty = []
+
+insert :: Ord a => a -> Set a -> Set a
+insert a [] = [a]
+insert a (x:xs)
+  | a < x = a:x:xs
+  | a > x = x:insert a xs
+  | a == x = x:xs
+
+set :: Ord a => [a] -> Set a
+set = foldr insert empty
+
+ordered [] = True
+ordered [x] = True
+ordered (x:y:zs) = x <= y && ordered (y:zs)
+
+allDiff [] = True
+allDiff (x:xs) = x `notElem` xs && allDiff xs
+
+isSet s = ordered s && allDiff s
+
+-- Properties
+
+infixr 0 -->
+False --> _ = True
+True --> x = x
+
+prop_insertSet :: (Char, Set Char) -> Bool
+prop_insertSet (c, s) = ordered s --> ordered (insert c s)
diff --git a/examples/Mate.hs b/examples/Mate.hs
new file mode 100644
--- /dev/null
+++ b/examples/Mate.hs
@@ -0,0 +1,256 @@
+module Mate where
+
+import LazySmallCheck
+import List
+
+data Kind = King | Queen | Rook | Bishop | Knight | Pawn
+  deriving (Eq, Show)
+
+data Colour = Black | White
+  deriving (Eq, Show)
+
+type Piece = (Colour,Kind)
+type Square = (Int,Int)
+
+data Board = Board
+		[(Kind,Square)] -- white
+		[(Kind,Square)] -- black
+  deriving Show
+
+pieceAt :: Board -> Square -> Maybe Piece
+pieceAt (Board wkss bkss) sq =
+        pieceAtWith White (pieceAtWith Black Nothing bkss) wkss
+	where
+	pieceAtWith c n [] = n
+	pieceAtWith c n ((k,s):xs) = if s==sq then Just (c,k) else pieceAtWith c n xs
+
+emptyAtAll :: Board -> (Square->Bool) -> Bool
+emptyAtAll (Board wkss bkss) e =
+	emptyAtAllAnd (emptyAtAllAnd True bkss) wkss
+	where
+	emptyAtAllAnd b []         = b
+	emptyAtAllAnd b ((_,s):xs) = not (e s) && emptyAtAllAnd b xs
+
+rmPieceAt White sq (Board wkss bkss) = Board (rPa sq wkss) bkss
+rmPieceAt Black sq (Board wkss bkss) = Board wkss (rPa sq bkss)
+
+rPa sq (ks@(k,s):kss) = if s==sq then kss else ks : rPa sq kss
+
+putPieceAt sq (White,k) (Board wkss bkss) = Board ((k,sq):wkss) bkss
+putPieceAt sq (Black,k) (Board wkss bkss) = Board wkss ((k,sq):bkss)
+
+kingSquare :: Colour -> Board -> Square
+kingSquare White (Board kss _) = kSq kss
+kingSquare Black (Board _ kss) = kSq kss
+
+kSq ((King,s):_)   = s
+kSq (       _:kss) = kSq kss 
+
+opponent Black = White
+opponent White = Black
+
+colourOf :: Piece -> Colour
+colourOf (c,_) = c
+
+kindOf :: Piece -> Kind
+kindOf (_,k) = k
+
+onboard :: Square -> Bool
+onboard (p,q) = 1<=p && p<=8 && 1<=q && q<=8
+
+forcesColoured White (Board kss _) = kss
+forcesColoured Black (Board _ kss) = kss
+
+emptyBoard = Board [] []
+
+data Move = Move 
+    Square    -- to here
+    (Maybe Piece) -- capturing this
+    (Maybe Piece) -- gaining promotion to this
+    
+data MoveInFull = MoveInFull Piece Square Move
+
+tryMove :: Colour -> (Kind,Square) -> Move -> Board -> Maybe (MoveInFull,Board)
+tryMove c ksq@(k,sq) m@(Move sq' mcp mpp) bd =
+  if not (kingincheck c bd2) then Just (MoveInFull p sq m, bd2)
+  else Nothing 
+  where
+  p   =   (c,k)
+  bd1 = rmPieceAt c sq bd
+  p'  = maybe p id mpp
+  bd2 = maybe (putPieceAt sq' p' bd1)
+          (const (putPieceAt sq' p' (rmPieceAt (opponent c) sq' bd1)))
+          mcp
+
+moveDetailsFor :: Colour -> Board -> [(MoveInFull,Board)]
+moveDetailsFor c bd =
+  foldr ( \ksq ms ->
+    foldr (\rm ms' -> maybe id (:) (tryMove c ksq rm bd) ms')
+                   ms
+                   (rawmoves c ksq bd) )
+        []
+              (forcesColoured c bd)
+
+
+-- NB raw move = might illegally leave the king in check.
+rawmoves :: Colour -> (Kind,Square) -> Board -> [Move]
+rawmoves c (k,sq) bd = m c sq bd
+	where
+        m = case k of
+	    King   -> kingmoves
+	    Queen  -> queenmoves
+	    Rook   -> rookmoves
+	    Bishop -> bishopmoves
+	    Knight -> knightmoves
+	    Pawn   -> pawnmoves
+
+bishopmoves :: Colour -> Square -> Board -> [Move]
+bishopmoves c sq bd =
+	( moveLine bd c sq (\(x,y) -> (x-1,y+1)) $
+	  moveLine bd c sq (\(x,y) -> (x+1,y+1)) $
+	  moveLine bd c sq (\(x,y) -> (x-1,y-1)) $
+	  moveLine bd c sq (\(x,y) -> (x+1,y-1)) id
+        ) []
+
+rookmoves :: Colour -> Square -> Board -> [Move]
+rookmoves c sq bd =
+	( moveLine bd c sq (\(x,y) -> (x-1,y)) $
+	  moveLine bd c sq (\(x,y) -> (x+1,y)) $
+	  moveLine bd c sq (\(x,y) -> (x,y-1)) $
+	  moveLine bd c sq (\(x,y) -> (x,y+1)) id
+        ) []
+
+moveLine :: Board -> Colour -> Square -> (Square->Square) -> ([Move]->a) -> [Move] -> a
+moveLine bd c sq inc cont = ml sq
+	where
+	ml sq ms =
+		let sq' = inc sq in
+		if onboard sq' then
+			case pieceAt bd sq' of
+			Nothing -> ml sq' (Move sq' Nothing Nothing : ms)
+			Just p' -> if colourOf p' /= c then
+					cont (Move sq' (Just p') Nothing : ms)
+                                   else cont ms
+		else cont ms
+
+kingmoves :: Colour -> Square -> Board -> [Move]
+kingmoves c (p,q) bd =
+	sift c bd []     [(p-1,q+1), (p,q+1), (p+1,q+1),
+	  	 	  (p-1,q),            (p+1,q),
+		 	  (p-1,q-1), (p,q-1), (p+1,q-1)]
+
+knightmoves :: Colour -> Square -> Board -> [Move]
+knightmoves c (p,q) bd =
+	sift c bd [] [	  	 (p-1,q+2),(p+1,q+2),
+			  (p-2,q+1),		  (p+2,q+1),
+                          (p-2,q-1),		  (p+2,q-1),
+		  		 (p-1,q-2),(p+1,q-2) ]
+
+sift :: Colour -> Board -> [Move] -> [Square] -> [Move]
+sift _ _  ms [] = ms
+sift c bd ms (sq:sqs) =
+	if onboard sq then
+		case pieceAt bd sq of
+                Nothing -> sift c bd (Move sq Nothing Nothing : ms) sqs
+		Just p' -> if colourOf p' == c then sift c bd ms sqs
+                           else sift c bd (Move sq (Just p') Nothing : ms) sqs
+	else sift c bd ms sqs
+
+pawnmoves :: Colour -> Square -> Board -> [Move]
+pawnmoves c (p,q) bd = movs ++ caps
+	where
+	movs =	let on1 = (p,q+fwd)
+		    on2 = (p,q+2*fwd) in
+		if pieceAt bd on1 == Nothing then
+			promote on1 Nothing ++
+			if (q==2 && c==White || q==7 && c==Black) &&
+			 	pieceAt bd on2 == Nothing then [Move on2 Nothing Nothing] 
+			else []
+		else []
+	caps =	concat [ promote sq mcp
+                       | sq <- [(p+1,q+fwd), (p-1,q+fwd)],
+                         mcp@(Just p') <- [pieceAt bd sq], colourOf p'/=c ]
+	fwd  =	case c of
+       		White -> 1
+		Black -> -1
+	promote sq@(x,y) mcp =  
+		if (c==Black && y==1 || c==White && y==8) then
+			map (Move sq mcp . Just)
+			    [(c,Queen), (c,Rook), (c,Bishop), (c,Knight)]
+		else [Move sq mcp Nothing]
+
+queenmoves :: Colour -> Square -> Board -> [Move]
+queenmoves c sq bd = bishopmoves c sq bd ++ rookmoves c sq bd
+
+kingincheck :: Colour -> Board -> Bool
+kingincheck c bd =
+	any givesCheck (forcesColoured (opponent c) bd)
+	where
+	givesCheck (k,(x,y)) = kthreat k
+		where
+		kthreat King =
+			abs (x-xk) <= 1 && abs (y-yk) <= 1
+		kthreat Queen =
+			kthreat Rook || kthreat Bishop
+		kthreat Rook =
+			x==xk &&
+                        emptyAtAll bd (\(xe,ye) -> xe==xk && min y yk < ye && ye < max y yk) ||
+			y==yk &&
+                        emptyAtAll bd (\(xe,ye) -> ye==yk && min x xk < xe && xe < max x xk)
+		kthreat	Bishop =
+			x+y==xk+yk &&
+			emptyAtAll bd (\(xe,ye) -> xe+ye==xk+yk && min x xk < xe && xe < max x xk) ||
+			x-y==xk-yk &&
+			emptyAtAll bd (\(xe,ye) -> xe-ye==xk-yk && min x xk < xe && xe < max x xk)
+		kthreat	Knight =
+			abs (x-xk) == 2 && abs (y-yk) == 1 ||
+			abs (x-xk) == 1 && abs (y-yk) == 2
+		kthreat Pawn =
+			abs (x-xk) == 1 &&
+			case c of
+			Black -> yk == y+1
+			White -> yk == y-1
+	(xk,yk) = kingSquare c bd
+
+checkmate :: Colour -> Board -> Bool
+checkmate col b = null (moveDetailsFor col b) && kingincheck col b
+
+-- Board generator
+
+allDiff [] = True
+allDiff (x:xs) = x `notElem` xs && allDiff xs
+
+onBoard (p, q) = 1 <= p && p <= 8 && 1 <= q && q <= 8
+
+one p [] = False
+one p (x:xs) = if p x then all (not . p) xs else one p xs
+
+kingsDontTouch ws bs =
+     (bx > succ wx || wx > succ bx || by > succ wy || wy > succ by)
+  where
+    (wx, wy) = kSq ws
+    (bx, by) = kSq bs
+
+validBoard (Board ws bs) =
+     one ((== King) . fst) ws
+  && one ((== King) . fst) bs
+  && all onBoard sqs
+  && kingsDontTouch ws bs
+  && allDiff sqs
+  where
+    sqs = map snd (ws ++ bs)
+
+-- Property
+
+infixr 0 -->
+False --> _ = True
+True --> x = x
+
+prop_checkmate b = 
+      (  length ws == 2
+      && Pawn `elem` (map fst ws)
+      && validBoard b
+      )
+  ==> not (checkmate Black b)
+  where
+    ws = forcesColoured White b
diff --git a/examples/Mux.hs b/examples/Mux.hs
new file mode 100644
--- /dev/null
+++ b/examples/Mux.hs
@@ -0,0 +1,64 @@
+module Mux where
+
+import Data.List
+
+type Bit             =  Bool
+  
+mux                  :: [Bit] -> [[Bit]] -> [Bit]
+mux 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     =  mux (decode sel) xs
+
+num                  :: [Bool] -> Int
+num []               =  0
+num (a:as)           =  (if a then 1 else 0) + 2 * num as
+
+encode as            =  enc (as ++ replicate n False)
+  where
+    n                =  2 ^ ulog2 (length as) - length as
+
+enc [_]              =  []
+enc as               =  zipWith (||) (enc ls) (enc rs) ++ [tree (||) rs]
+  where
+    (ls, rs)         =  splitAt (length as `div` 2) as
+
+oneHot []            =  False
+oneHot (a:as)        =  if a then not (or as) else oneHot as
+
+log2 n               =  if n == 1 then 0 else 1 + log2 (n `div` 2)
+
+ulog2 n              =  log2 (2*n - 1)
+
+-- Properties
+
+infixr 0 -->
+False --> _ = True
+True --> x = x
+
+prop_encode as = oneHot as --> (num (encode as) == n)
+  where
+    n = length (takeWhile not as)
+
+prop_mux (sel, xs) =
+      oneHot sel
+  &&  length sel == length xs
+  &&  all ((== length (head xs)) . length) xs
+  --> mux sel xs == xs !! n
+  where
+    n = length (takeWhile not sel)
+
+prop_encDec as = encode (decode as) == as
diff --git a/examples/RedBlack.hs b/examples/RedBlack.hs
new file mode 100644
--- /dev/null
+++ b/examples/RedBlack.hs
@@ -0,0 +1,80 @@
+module RedBlack where
+
+-- Red-Black trees in a functional setting, by Okasaki.
+-- (With invariants coded, and a fault injected.)
+
+data Colour = R | B
+  deriving Show
+
+data Tree a = E | T Colour (Tree a) a (Tree a)
+  deriving Show
+
+-- Methods
+
+member x E = False
+member x (T _ a y b)
+  | x < y = member x a
+  | x > y = member x b
+  | otherwise = True
+
+makeBlack (T _ a y b) = T B a y b
+
+insert x s = makeBlack (ins x s)
+
+ins x E = T R E x E
+ins x (T col a y b)
+  | x < y = balance col (ins x a) y b
+  | x > y = balance col a y (ins x b)
+  | otherwise = T col a y b
+
+-- Mistake on 4th line, 3rd line is correct
+balance B (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)
+balance B (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)
+--balance B a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)
+balance B a x (T R (T R c y b) z d) = T R (T B a x b) y (T B c z d)
+balance B a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)
+balance col a x b = T col a x b
+
+-- Helpers
+
+isRed R = True
+isRed B = False
+
+blackRoot E = True
+blackRoot (T col a x b) = not (isRed col)
+
+-- INVARIANT 1. No red node has a red parent.
+
+red E = True
+red (T col a x b) =
+  (if isRed col then blackRoot a && blackRoot b else True) && red a && red b
+
+-- INVARIANT 2. Every path from the root to an empty node contains the
+-- same number of black nodes.
+
+black t = fst (black' t)
+
+black' E = (True, 1)
+black' (T col a x b) = (b0 && b1 && n == m, n + if isRed col then 0 else 1)
+  where (b0, n) = black' a
+        (b1, m) = black' b
+
+-- INVARIANT 3. Trees are ordered.
+
+every p E = True
+every p (T _ a x b) = p x && every p a && every p b
+
+ord E = True
+ord (T _ a x b) = every (<= x) a && every (>= x) b && ord a && ord b
+
+-- Properties
+
+infixr 0 -->
+False --> _ = True
+True --> x = x
+
+redBlack t = red t && black t && ord t
+
+prop_insertRB (x, t) = redBlack t --> redBlack (insert x t)
+  where
+    types = x :: Int
diff --git a/examples/RegExp.hs b/examples/RegExp.hs
new file mode 100644
--- /dev/null
+++ b/examples/RegExp.hs
@@ -0,0 +1,91 @@
+module RegExp where
+
+(<==>) :: Bool -> Bool -> Bool
+a <==> b = a == b
+
+-- ---------------------
+
+data Nat = Zer
+         | Suc Nat
+  deriving (Eq, Show)
+
+sub :: Nat -> Nat -> Nat
+sub x y =
+ case y of
+  Zer -> x
+  Suc y' -> case x of
+   Zer -> Zer
+   Suc x' -> sub x' y'
+
+data Sym = N0
+         | N1 Sym
+ deriving (Eq, Show)
+
+data RE = Sym Sym
+        | Or RE RE
+        | Seq RE RE
+        | And RE RE
+        | Star RE
+        | Empty
+  deriving (Eq, Show)
+
+accepts :: RE -> [Sym] -> Bool
+accepts re ss =
+ case re of
+  Sym n -> case ss of
+   [] -> False
+   (n':ss') -> n == n' && null ss'
+  Or re1 re2 -> accepts re1 ss || accepts re2 ss
+  Seq re1 re2 -> seqSplit re1 re2 [] ss
+  And re1 re2 -> accepts re1 ss && accepts re2 ss
+  Star re' -> case ss of
+   [] -> True
+   (s:ss') -> seqSplit re' re (s:[]) ss'
+    -- accepts Empty ss || accepts (Seq re' re) ss
+  Empty -> null ss
+
+seqSplit :: RE -> RE -> [Sym] -> [Sym] -> Bool
+seqSplit re1 re2 ss2 ss =
+ seqSplit'' re1 re2 ss2 ss || seqSplit' re1 re2 ss2 ss
+
+seqSplit'' :: RE -> RE -> [Sym] -> [Sym] -> Bool
+seqSplit'' re1 re2 ss2 ss = accepts re1 ss2 && accepts re2 ss
+
+seqSplit' :: RE -> RE -> [Sym] -> [Sym] -> Bool
+seqSplit' re1 re2 ss2 ss =
+ case ss of
+  [] -> False
+  (n:ss') ->
+   seqSplit re1 re2 (ss2 ++ [n]) ss'
+
+rep :: Nat -> RE -> RE
+rep n re =
+ case n of
+  Zer -> Empty
+  Suc n' -> Seq re (rep n' re)
+
+repMax :: Nat -> RE -> RE
+repMax n re =
+ case n of
+  Zer -> Empty
+  Suc n' -> Or (rep n re) (repMax n' re)
+
+repInt' :: Nat -> Nat -> RE -> RE
+repInt' n k re =
+ case k of
+  Zer -> rep n re
+  Suc k' -> Or (rep n re) (repInt' (Suc n) k' re)
+
+repInt :: Nat -> Nat -> RE -> RE
+repInt n k re = repInt' n (sub k n) re
+
+-- Properties
+
+prop_regex :: (Nat, Nat, RE, RE, [Sym]) -> Bool
+prop_regex (n, k, p, q, s) = r
+  where
+    r = (accepts (repInt n k (And p q)) s)
+          <==> (accepts (And (repInt n k p) (repInt n k q)) s)
+  --(accepts (And (repInt n k p) (repInt n k q)) s) <==> (accepts (repInt n k (And p q)) s)^M
+
+a_sol = (Zer, Suc (Suc Zer), Sym N0, Seq (Sym N0) (Sym N0), [N0, N0])
diff --git a/examples/Sad.hs b/examples/Sad.hs
new file mode 100644
--- /dev/null
+++ b/examples/Sad.hs
@@ -0,0 +1,96 @@
+module Sad where
+
+-- We take the following specification for the sum of absolute
+-- differences, and develop a program that generates circuits that
+-- have 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
+
+-- Properties
+
+prop_binSad (xs, ys)           =   sad (map num xs) (map num ys)
+                                     == num (binSad xs ys)
diff --git a/examples/SumPuz.hs b/examples/SumPuz.hs
new file mode 100644
--- /dev/null
+++ b/examples/SumPuz.hs
@@ -0,0 +1,76 @@
+module SumPuz where
+
+-- Cryptarithmetic solver from AFP 2003
+
+import Data.List((\\))
+import Char(isAlpha, chr, ord)
+import Maybe(fromJust)
+
+type Soln = [(Char, Int)]
+
+solve :: String -> String
+solve p =
+  display p (solutions xs ys zs 0 [])
+  where
+  [xs,ys,zs] = map reverse (words (filter (`notElem` "+=") p))
+
+display :: String -> [Soln] -> String
+display p []    = "No solution!"
+display p (s:_) =
+  map soln p
+  where
+  soln c = if isAlpha c then chr (ord '0' + img s c) else c
+
+rng :: Soln -> [Int]
+rng = map snd
+
+img :: Soln -> Char -> Int
+img lds l = fromJust (lookup l lds)
+
+bindings :: Char -> [Int] -> Soln -> [Soln]
+bindings l ds lds =
+  case lookup l lds of
+  Nothing  -> map (:lds) (zip (repeat l) (ds \\ rng lds))
+  Just d -> if d `elem` ds then [lds] else []
+
+solutions :: String -> String -> String -> Int -> Soln -> [Soln]
+solutions [] [] []  c lds = if c==0 then [lds] else []
+solutions [] [] [z] c lds = if c==1 then bindings z [1] lds else []
+solutions (x:xs) (y:ys) (z:zs) c lds =
+  solns `ofAll`
+  bindings y [(if null ys then 1 else 0)..9] `ofAll`
+  bindings x [(if null xs then 1 else 0)..9] lds
+  where  
+  solns s = 
+    solutions xs ys zs (xy `div` 10) `ofAll` bindings z [xy `mod` 10] s
+    where    
+    xy = img s x + img s y + c
+
+infixr 5 `ofAll`
+ofAll :: (a -> [b]) -> [a] -> [b]
+ofAll = concatMap
+
+-- Properties
+
+infixr 0 -->
+False --> _ = True
+True --> x = x
+
+find :: String -> String -> String -> [Soln]
+find xs ys zs = solutions (reverse xs) (reverse ys) (reverse zs) 0 []
+
+val :: Soln -> String -> Int
+val s "" = 0
+val s xs = read (concatMap (show . img s) xs)
+
+prop_Sound :: (String, String, String) -> Bool
+prop_Sound (xs, ys, zs) =
+      length xs == length ys
+   && (diff == 0 || diff == 1)
+   && not (null sols)
+  --> and [ val s xs + val s ys == val s zs
+          | s <- sols
+          ]
+  where
+    sols = find xs ys zs
+    diff = length zs - length xs
diff --git a/examples/Turner.hs b/examples/Turner.hs
new file mode 100644
--- /dev/null
+++ b/examples/Turner.hs
@@ -0,0 +1,59 @@
+module Turner where
+
+-- Turner's abstraction algorithm as defined by Simon PJ
+-- (with properties added)
+
+infixl 9 :@
+
+data Var = V0 | V1
+  deriving (Show, Eq)
+
+data Exp = Exp :@ Exp | L Var Exp | V Var | F Comb
+  deriving (Show, Eq)
+
+data Comb = I | K | B | C | S | C' | B' | S'
+  deriving (Show, Eq)
+
+compile (f :@ x) = compile f :@ compile x
+compile (L v e) = abstr v (compile e)
+compile e = e
+
+abstr v (f :@ x) = opt (F S :@ abstr v f :@ abstr v x)
+abstr v (V w) | v == w = F I
+abstr v e = F K :@ e
+
+opt (F S :@ (F K :@ p) :@ (F K :@ q)) = F K :@ (p :@ q)
+opt (F S :@ (F K :@ p) :@ F I) = p
+opt (F S :@ (F K :@ p) :@ (F B :@ q :@ r)) = F B' :@ p :@ q :@ r
+opt (F S :@ (F K :@ p) :@ q) = F B :@ p :@ q
+opt (F S :@ (F B :@ p :@ q) :@ (F K :@ r)) = F C' :@ p :@ q :@ r
+opt (F S :@ p :@ (F K :@ q)) = F C :@ p :@ q
+opt (F S :@ (F B :@ p :@ q) :@ r) = F S' :@ p :@ q :@ r
+opt e = e
+
+-- Combinator reduction
+
+simp (F I :@ a) = Just a
+simp (F K :@ a :@ b) = Just a
+simp (F S :@ f :@ g :@ x) = Just $ f :@ x :@ (g :@ x)
+simp (F B :@ f :@ g :@ x) = Just $ f :@ (g :@ x)
+simp (F C :@ f :@ g :@ x) = Just $ f :@ x :@ g
+simp (F B' :@ k :@ f :@ g :@ x) = Just $ k :@ (f :@ (g :@ x))
+simp (F C' :@ k :@ f :@ g :@ x) = Just $ k :@ (f :@ x) :@ g
+simp (F S' :@ k :@ f :@ g :@ x) = Just $ k :@ (f :@ x) :@ (g :@ x)
+simp e = Nothing
+
+simplify e =
+  case simp e of
+    Nothing -> case e of
+                 f :@ g -> simplify f :@ simplify g
+                 _ -> e
+    Just e' -> simplify e'
+
+-- Properties
+
+infixr 0 -->
+False --> _ = True
+True --> x = x
+
+prop_abstr (v, e) = simplify (abstr v e :@ V v) == e
diff --git a/examples/test/TestCatch.hs b/examples/test/TestCatch.hs
new file mode 100644
--- /dev/null
+++ b/examples/test/TestCatch.hs
@@ -0,0 +1,17 @@
+import Test.LazySmallCheck
+import Catch
+import System
+
+instance Serial Value where
+  series = cons0 Bottom \/ cons2 Value
+
+instance Serial CtorName where
+  series = cons0 Ctor \/ cons0 CtorN \/ cons0 CtorR \/ cons0 CtorNR
+
+instance Serial Val where
+  series = cons2 (:*) \/ cons0 Any
+
+instance Serial Pattern where
+  series = cons2 Pattern
+
+main = do [d] <- getArgs ; depthCheck (read d) prop
diff --git a/examples/test/TestCountdown1.hs b/examples/test/TestCountdown1.hs
new file mode 100644
--- /dev/null
+++ b/examples/test/TestCountdown1.hs
@@ -0,0 +1,5 @@
+import Test.LazySmallCheck
+import Countdown
+import System
+
+main = do [d] <- getArgs ; depthCheck (read d) prop_lemma3
diff --git a/examples/test/TestCountdown2.hs b/examples/test/TestCountdown2.hs
new file mode 100644
--- /dev/null
+++ b/examples/test/TestCountdown2.hs
@@ -0,0 +1,5 @@
+import Test.LazySmallCheck
+import Countdown
+import System
+
+main = do [d] <- getArgs ; depthCheck (read d) prop_solutions
diff --git a/examples/test/TestHuffman1.hs b/examples/test/TestHuffman1.hs
new file mode 100644
--- /dev/null
+++ b/examples/test/TestHuffman1.hs
@@ -0,0 +1,8 @@
+import Test.LazySmallCheck
+import Huffman
+import System
+
+instance Serial a => Serial (BTree a) where
+  series = cons1 Leaf \/ cons2 Fork
+
+main = do [d] <- getArgs ; depthCheck (read d) prop_decEnc
diff --git a/examples/test/TestHuffman2.hs b/examples/test/TestHuffman2.hs
new file mode 100644
--- /dev/null
+++ b/examples/test/TestHuffman2.hs
@@ -0,0 +1,8 @@
+import Test.LazySmallCheck
+import Huffman
+import System
+
+instance Serial a => Serial (BTree a) where
+  series = cons1 Leaf \/ cons2 Fork
+
+main = do [d] <- getArgs ; depthCheck (read d) prop_optimal
diff --git a/examples/test/TestListSet1.hs b/examples/test/TestListSet1.hs
new file mode 100644
--- /dev/null
+++ b/examples/test/TestListSet1.hs
@@ -0,0 +1,5 @@
+import Test.LazySmallCheck
+import ListSet
+import System
+
+main = do [d] <- getArgs ; depthCheck (read d) prop_insertSet
diff --git a/examples/test/TestMate.hs b/examples/test/TestMate.hs
new file mode 100644
--- /dev/null
+++ b/examples/test/TestMate.hs
@@ -0,0 +1,19 @@
+import Test.LazySmallCheck
+import Mate
+import System
+
+instance Serial Kind where
+  series = cons0 King
+      \/ cons0 Queen
+      \/ cons0 Rook
+      \/ cons0 Bishop
+      \/ cons0 Knight
+      \/ cons0 Pawn
+
+instance Serial Colour where
+  series = cons0 Black \/ cons0 White
+
+instance Serial Board where
+  series = cons2 Board
+
+main = do [d] <- getArgs ; depthCheck (read d) prop_checkmate
diff --git a/examples/test/TestMux1.hs b/examples/test/TestMux1.hs
new file mode 100644
--- /dev/null
+++ b/examples/test/TestMux1.hs
@@ -0,0 +1,5 @@
+import Test.LazySmallCheck
+import Mux
+import System
+
+main = do [d] <- getArgs ; depthCheck (read d) prop_mux
diff --git a/examples/test/TestMux2.hs b/examples/test/TestMux2.hs
new file mode 100644
--- /dev/null
+++ b/examples/test/TestMux2.hs
@@ -0,0 +1,5 @@
+import Test.LazySmallCheck
+import Mux
+import System
+
+main = do [d] <- getArgs ; depthCheck (read d) prop_encode
diff --git a/examples/test/TestMux3.hs b/examples/test/TestMux3.hs
new file mode 100644
--- /dev/null
+++ b/examples/test/TestMux3.hs
@@ -0,0 +1,5 @@
+import Test.LazySmallCheck
+import Mux
+import System
+
+main = do [d] <- getArgs ; depthCheck (read d) prop_encDec
diff --git a/examples/test/TestRedBlack.hs b/examples/test/TestRedBlack.hs
new file mode 100644
--- /dev/null
+++ b/examples/test/TestRedBlack.hs
@@ -0,0 +1,11 @@
+import Test.LazySmallCheck
+import RedBlack
+import System
+
+instance Serial Colour where
+  series = cons0 R \/ cons0 B
+
+instance Serial a => Serial (Tree a) where
+  series = cons0 E \/ cons4 T
+
+main = do [d] <- getArgs ; depthCheck (read d) prop_insertRB
diff --git a/examples/test/TestRegExp.hs b/examples/test/TestRegExp.hs
new file mode 100644
--- /dev/null
+++ b/examples/test/TestRegExp.hs
@@ -0,0 +1,19 @@
+import Test.LazySmallCheck
+import RegExp
+import System
+
+instance Serial Nat where
+  series = cons0 Zer \/ cons1 Suc
+
+instance Serial Sym where
+  series = cons0 N0 \/ cons1 N1
+
+instance Serial RE where
+  series = cons1 Sym
+        \/ cons2 Or
+        \/ cons2 Seq
+        \/ cons2 And
+        \/ cons1 Star
+        \/ cons0 Empty
+
+main = do [d] <- getArgs ; depthCheck (read d) prop_regex
diff --git a/examples/test/TestSad.hs b/examples/test/TestSad.hs
new file mode 100644
--- /dev/null
+++ b/examples/test/TestSad.hs
@@ -0,0 +1,5 @@
+import Test.LazySmallCheck
+import Sad
+import System
+
+main = do [d] <- getArgs ; depthCheck (read d) prop_binSad
diff --git a/examples/test/TestSumPuz.hs b/examples/test/TestSumPuz.hs
new file mode 100644
--- /dev/null
+++ b/examples/test/TestSumPuz.hs
@@ -0,0 +1,5 @@
+import Test.LazySmallCheck
+import SumPuz
+import System
+
+main = do [d] <- getArgs ; depthCheck (read d) prop_Sound
diff --git a/examples/test/TestTurner.hs b/examples/test/TestTurner.hs
new file mode 100644
--- /dev/null
+++ b/examples/test/TestTurner.hs
@@ -0,0 +1,11 @@
+import Test.LazySmallCheck
+import Turner
+import System
+
+instance Serial Var where
+  series = cons0 V0 \/ cons0 V1
+
+instance Serial Exp where
+  series = cons2 (:@) \/ cons2 L \/ (cons1 V . (+1))
+
+main = do [d] <- getArgs ; depthCheck (read d) prop_abstr
diff --git a/lazysmallcheck.cabal b/lazysmallcheck.cabal
--- a/lazysmallcheck.cabal
+++ b/lazysmallcheck.cabal
@@ -1,34 +1,51 @@
 Name:               lazysmallcheck
-Version:            0.1
-Copyright:          2007, Matthew Naylor
-Maintainer:         mfn@cs.york.ac.uk
+Version:            0.2
+Maintainer:         Matthew Naylor <mfn@cs.york.ac.uk>
 Homepage:           http://www.cs.york.ac.uk/~mfn/lazysmallcheck/
-Build-Depends:      base, haskell98, random
-Build-Type:         Simple
+Build-Depends:      base, haskell98
 License:            BSD3
 License-File:       LICENSE
 Author:             Matthew Naylor and Fredrik Lindblad
 Synopsis:           A library for demand-driven testing of Haskell programs
 Description:
-    Lazy SmallCheck is a library for exhaustive, demand-driven testing of
-    Haskell programs.  It is based on the idea that if a property holds
-    for a partially-defined input then it must also hold for all
-    fully-defined instantiations of the that input.  Compared to ``eager''
-    input generation as in SmallCheck, Lazy SmallCheck may require
-    significantly fewer test-cases to verify a property for all inputs up
-    to a given depth.
+  Lazy SmallCheck is a library for exhaustive, demand-driven testing of
+  Haskell programs.  It is based on the idea that if a property holds
+  for a partially-defined input then it must also hold for all
+  fully-defined refinements of the that input.  Compared to ``eager'' 
+  input generation as in SmallCheck, Lazy SmallCheck may require
+  significantly fewer test-cases to verify a property for all inputs up 
+  to a given depth.
 Category:           Testing
-Hs-Source-dirs:
-    source
+Build-Depends:      base, haskell98
+Build-Type:         Simple
 Extra-Source-Files:
-    benchmarks/Benchmark.hs
-    benchmarks/Countdown.hs
-    benchmarks/List.hs
-    benchmarks/Mux.hs
-    benchmarks/RegExp.hs
-    benchmarks/Sad.hs
-    benchmarks/SumPuz.hs
-    benchmarks/clean.sh
+  examples/Catch.hs
+  examples/Mate.hs
+  examples/Sad.hs
+  examples/Countdown.hs
+  examples/Mux.hs
+  examples/SumPuz.hs
+  examples/Huffman.hs
+  examples/RedBlack.hs
+  examples/Turner.hs
+  examples/ListSet.hs
+  examples/RegExp.hs
+  examples/test/TestCatch.hs
+  examples/test/TestMux2.hs
+  examples/test/TestCountdown1.hs
+  examples/test/TestMux3.hs
+  examples/test/TestCountdown2.hs
+  examples/test/TestRedBlack.hs
+  examples/test/TestHuffman1.hs
+  examples/test/TestRegExp.hs
+  examples/test/TestHuffman2.hs
+  examples/test/TestSad.hs
+  examples/test/TestListSet1.hs
+  examples/test/TestSumPuz.hs
+  examples/test/TestMate.hs
+  examples/test/TestTurner.hs
+  examples/test/TestMux1.hs
+
 Exposed-modules:
-    LazySmallCheck
-    LazySmallCheck.Generic
+  Test.LazySmallCheck
+  Test.LazySmallCheck.Generic
diff --git a/source/LazySmallCheck.hs b/source/LazySmallCheck.hs
deleted file mode 100644
--- a/source/LazySmallCheck.hs
+++ /dev/null
@@ -1,262 +0,0 @@
-module LazySmallCheck
-  ( Serial(series) -- class Serial
-  , (\/)           -- :: Series a -> Series a -> Series a
-  , cons0          -- :: a -> Series a
-  , cons1          -- :: Serial a => (a -> b) -> Series b
-  , cons2          -- :: (Serial a, Serial b) =>
-                   --    (a -> b -> c) -> Series c
-  , cons3          -- :: (Serial a, Serial b, Serial c) =>
-                   --    (a -> b -> c -> d) -> Series d
-  , cons4          -- :: (Serial a, Serial b, Serial c, Serial d) =>
-                   --    (a -> b -> c -> d -> e) -> Series e
-  , cons5          -- :: (Serial a, Serial b, Serial c, Serial d, Serial e) =>
-                   --    (a -> b -> c -> d -> e -> f) -> Series f
-  , Testable       -- class Testable
-  , depthCheck     -- :: Testable a => Int -> a -> IO ()
-  , (==>)          -- :: Bool -> Bool -> Bool
-  ) where
-
-import Control.Monad
-import Control.Exception
-import System.Exit
-
-infixr 3 \/
-infixr 0 ==>
-
--- Type class and instance helpers
-
-data Family = Algebraic [(Int, [Family])] | Builtin (Int -> [Value])
-
-data Value = Var Family Int String | Ctr Int [Value] | Prim Prim
-
-data Prim = Char Char | Int Int | Integer Integer
-
-type Series a = Int -> (Family, [[Value] -> a])
-
-class Serial a where
-  series :: Series a
-
-genSeries :: Serial a => (Family, [[Value] -> a])
-genSeries = series 0
-
-convert :: [[Value] -> a] -> Value -> a
-convert alts (Var _ _ v) = error v
-convert alts (Prim p) = head alts [Prim p]
-convert alts (Ctr n as) = (alts !! n) as
-
-(\/) :: Series a -> Series a -> Series a
-(c0 \/ c1) n = (Algebraic (cs0 ++ cs1), alts0 ++ alts1)
-  where
-    (Algebraic cs0, alts0) = c0 n
-    (Algebraic cs1, alts1) = c1 (n + 1)
-
-cons0 :: a -> Series a
-cons0 c n = (Algebraic [(n, [])], alts)
-  where
-    alts = [\_ -> c]
-
-cons1 :: Serial a => (a -> b) -> Series b
-cons1 c n = (Algebraic [(n, [fam0])], alts)
-  where
-    alts = [\(a0:_) -> c (convert alts0 a0)]
-    (fam0, alts0) = genSeries
-
-cons2 :: (Serial a, Serial b) => (a -> b -> c) -> Series c
-cons2 c n = (Algebraic [(n, [fam0, fam1])], alts)
-  where
-    alts = [\(a0:a1:_) -> c (convert alts0 a0) (convert alts1 a1)]
-    (fam0, alts0) = genSeries
-    (fam1, alts1) = genSeries
-
-cons3 :: (Serial a, Serial b, Serial c) => (a -> b -> c -> d) -> Series d
-cons3 c n = (Algebraic [(n, [fam0, fam1, fam2])], alts)
-  where
-    alts = [\(a0:a1:a2:_) -> c (convert alts0 a0)
-                               (convert alts1 a1)
-                               (convert alts2 a2)]
-    (fam0, alts0) = genSeries
-    (fam1, alts1) = genSeries
-    (fam2, alts2) = genSeries
-
-cons4 :: (Serial a, Serial b, Serial c, Serial d) =>
-         (a -> b -> c -> d -> e) -> Series e
-cons4 c n = (Algebraic [(n, [fam0, fam1, fam2, fam3])], alts)
-  where
-    alts = [\(a0:a1:a2:a3:_) -> c (convert alts0 a0)
-                                  (convert alts1 a1)
-                                  (convert alts2 a2)
-                                  (convert alts3 a3)]
-    (fam0, alts0) = genSeries
-    (fam1, alts1) = genSeries
-    (fam2, alts2) = genSeries
-    (fam3, alts3) = genSeries
-
-
-cons5 :: (Serial a, Serial b, Serial c, Serial d, Serial e) =>
-         (a -> b -> c -> d -> e -> f) -> Series f
-cons5 c n = (Algebraic [(n, [fam0, fam1, fam2, fam3, fam4])], alts)
-  where
-    alts = [\(a0:a1:a2:a3:a4:_) -> c (convert alts0 a0)
-                                     (convert alts1 a1)
-                                     (convert alts2 a2)
-                                     (convert alts3 a3)
-                                     (convert alts4 a4)]
-    (fam0, alts0) = genSeries
-    (fam1, alts1) = genSeries
-    (fam2, alts2) = genSeries
-    (fam3, alts3) = genSeries
-    (fam4, alts4) = genSeries
-
-
--- Useful Serial instances
-
-instance Serial Bool where
-  series = cons0 False \/ cons0 True
-
-instance Serial a => Serial (Maybe a) where
-  series = cons0 Nothing \/ cons1 Just
-
-instance (Serial a, Serial b) => Serial (Either a b) where
-  series = cons1 Left \/ cons1 Right
-
-instance Serial a => Serial [a] where
-  series = cons0 [] \/ cons2 (:)
-
-instance (Serial a, Serial b) => Serial (a, b) where
-  series = cons2 (,)
-
-instance (Serial a, Serial b, Serial c) => Serial (a, b, c) where
-  series = cons3 (,,)
-
-instance (Serial a, Serial b, Serial c, Serial d) => Serial (a, b, c, d) where
-  series = cons4 (,,,)
-
-instance (Serial a, Serial b, Serial c, Serial d, Serial e) =>
-           Serial (a, b, c, d, e) where
-  series = cons5 (,,,,)
-
--- Primitive Serial instances
-
-instance Serial Int where
-  series _ = (fam, alts)
-    where
-      fam = Builtin (\d -> map (Prim . Int) [-d .. d])
-      alts = [\(Prim (Int i):_) -> i]
-
-instance Serial Integer where
-  series _ = (fam, alts)
-    where
-      fam = Builtin (\d -> map (Prim . Integer . toInteger) [-d .. d])
-      alts = [\(Prim (Integer i):_) -> i]
-
-instance Serial Char where
-  series _ = (fam, alts)
-    where
-      fam = Builtin (\d -> map (Prim . Char) (take (d+1) ['a'..'z']))
-      alts = [\(Prim (Char c):_) -> c]
-
--- Refinement of partial values
-
-uniquePrefix = "UP:"
-
-lenUniquePrefix = length uniquePrefix
-
-type Position = String
-
-inst :: Int -> String -> (Int, [Family]) -> Value
-inst d s (n, fs) = Ctr n (zipWith mkVar fs ['\NUL'..])
-  where
-    mkVar fam c = Var fam d (s++[c])
-
-refine :: Position -> Value -> [Value]
-refine [] (Var (Algebraic cs) d s) = map (inst (d-1) s) cs'
-  where
-    cs' = if d == 0 then filter (null . snd) cs else cs
-refine [] (Var (Builtin f) d s) = f d
-refine (p:ps) (Ctr n as) = map (Ctr n) (refineMany p ps as)
-
-refineMany :: Char -> Position -> [Value] -> [[Value]]
-refineMany p ps as = [(xs ++ a':ys) | a' <- refine ps a]
-  where
-    (xs, a:ys) = splitAt (fromEnum p) as
-
--- Find total instantiations of a partial value, by iterative deepening
-
-total :: Int -> Value -> [Value]
-total d val = tot d val ++ total (d-1) val
-
-tot :: Int -> Value -> [Value]
-tot lim (Prim p) = [Prim p]
-tot lim (Ctr n as) = [Ctr n as' | as' <- mapM (tot lim) as]
-tot lim (Var fam d s)
-  | d < lim = []
-  | otherwise = case fam of
-                  Builtin f -> f (d - lim)
-                  Algebraic cs -> concatMap (tot lim . inst (d-1) s) cs
-
--- General
-
-False ==> _ = True
-True ==> a = a
-
--- Testable class machinery
-
-data Info = Info { arguments :: [Value]
-                 , showFuncs :: [Value -> String]
-                 , apply     :: ([Value] -> Bool)
-                 }
-
-newtype Property = Prop (Int -> Int -> Info)
-
-eval :: Testable a => ([Value] -> a) -> Int -> Int -> Info
-eval a = gen where Prop gen = property a
-
-class Testable a where
-  property :: ([Value] -> a) -> Property
-
-instance Testable Bool where
-  property apply = Prop $ \depth n -> Info [] [] (apply . reverse)
-
-instance (Show a, Serial a, Testable b) => Testable (a -> b) where
-  property f =
-    Prop $ \depth n ->
-      let (fam, alts) = genSeries
-          initial = Var fam depth (uniquePrefix ++ [toEnum n])
-          val = convert alts initial
-          g (x:xs) = f xs (convert alts x)
-          info = eval g depth (n+1)
-      in  info { arguments = initial : arguments info
-               , showFuncs = (show . convert alts) : showFuncs info
-               }
-
--- Refute
-
-refute :: Info -> IO Int
-refute info = r (arguments info)
-  where
-    r args = do res <- try (evaluate (prop args))
-                case res of
-                  Right True -> return 1
-                  Right False -> stop args "Counter example found:"
-                  Left (ErrorCall s)
-                    | take (lenUniquePrefix) s == uniquePrefix ->
-                        let (c:pos) = drop lenUniquePrefix s
-                        in  do ns <- mapM r (refineMany c pos args)
-                               return (1 + sum ns)
-                  Left e -> stop args $ "Property crashed on input:"
-
-    prop = apply info
-    disp as = zipWith ($) (showFuncs info) as
-    stop args s = do putStrLn s
-                     let args' = head [as | as <- mapM (total 0) args]
-                     mapM putStrLn (disp args')
-                     exitWith ExitSuccess
-
-depthCheck :: Testable a => Int -> a -> IO ()
-depthCheck d p =
-  do count <- refute info
-     putStrLn $  "Completed " ++ show count
-              ++ " tests without finding a counter example."
-  where
-    Prop f = property (const p)
-    info = f d 0
diff --git a/source/LazySmallCheck/Generic.hs b/source/LazySmallCheck/Generic.hs
deleted file mode 100644
--- a/source/LazySmallCheck/Generic.hs
+++ /dev/null
@@ -1,144 +0,0 @@
-{-# OPTIONS -fglasgow-exts #-}
-
-module LazySmallCheck.Generic
-  ( depthCheck  -- :: (Data a, Show a) => Int -> (a -> Bool) -> IO [a]
-  , (==>)       -- :: Bool -> Bool -> Bool
-  ) where
-
-import Data.Maybe
-import Data.Generics
-import Control.Exception
-import Control.Monad
-import System.Random
-import System.Exit
-
-uniquePrefix = "UP:"
-
-lenUniquePrefix = length uniquePrefix
-
-type Position = String
-
-initPData :: a
-initPData = error uniquePrefix
-
-data HLP a = HLP Int (Either a [a])
-
-refinePData :: Data a => String -> Int -> Position -> a -> [a]
-refinePData s d = r
- where
-  depleft = d - (length s - lenUniquePrefix)
-  r :: Data a => Position -> a -> [a]
-  r [] x =
-    let dt = dataTypeOf x
-    in case dataTypeRep dt of
-         AlgRep cons ->
-           let cons = dataTypeConstrs dt
-               z x = (0, x)
-               k (i, g) = (i + 1, g (error $ s ++ [toEnum i]))
-               xs' = map (gunfold k z) cons
-           in  if   depleft > 0
-               then map snd xs'
-               else mapMaybe (\(ncon, x') ->
-                                 if   ncon == 0
-                                 then Just x'
-                                 else Nothing) xs'
-         IntRep -> mkPrim dt (mkIntConstr dt . toInteger)
-                             [-depleft .. depleft]
-         StringRep -> mkPrim dt (mkStringConstr dt . (:[]))
-                                (take (depleft+1) ['a' .. 'z'])
-         _ -> error $ "LazySmallCheck.Generic: Can't generate type "
-                   ++ dataTypeName dt
-  r (c:ps) x =
-   let p = fromEnum c
-       z y = HLP 0 (Left y)
-       k (HLP i (Left xs)) y | i == p = HLP (i + 1) (Right $ map xs (r ps y))
-       k (HLP i (Left xs)) y = HLP (i + 1) (Left $ xs y)
-       k (HLP i (Right xss)) y = HLP (i + 1) (Right $ map (\xs -> xs y) xss)
-       HLP _ (Right x') = gfoldl k z x
-   in  x'
-
-mkPrim dt mk vs = map (\i -> fromJust $ gunfold undefined Just $ mk i) vs
-
---
-
-mapVars :: Data a => (forall b . Data b => b -> IO b) -> a -> IO a
-mapVars f = gmapM (\x -> Control.Exception.catch
-  (mapVars f x)
-  (\exc -> case exc of
-    ErrorCall s | take (length uniquePrefix) s == uniquePrefix ->
-     f x
-    _ -> throw exc
-  )
- )
-
--- Taken from Ralf Laemmel, SYB website
--- Generate all terms of a given depth
-enumerate :: Data a => Int -> [a]
-enumerate 0 = []
-enumerate d = result
-   where
-     -- Getting hold of the result (type)
-     result = concat (map recurse cons')
-
-     -- Find all terms headed by a specific Constr
-     recurse :: Data a => Constr -> [a]
-     recurse con = gmapM (\_ -> enumerate (d-1)) 
-                         (fromConstr con)
-
-     -- We could also deal with primitive types easily.
-     -- Then we had to use cons' instead of cons.
-     --
-     cons' :: [Constr]
-     cons' = case dataTypeRep ty of
-              AlgRep cons -> cons
-              IntRep      -> map (mkIntConstr ty . toInteger) [-d .. d]
-              StringRep   -> map (mkStringConstr ty . (:[])) (take d ['a'..'z'])
-              --FloatRep  ->
-      where
-        ty = dataTypeOf (head result)     
-
-smallValue :: Data a => a
-smallValue = f 1
- where
-  f d = case enumerate d of
-   [] -> f (d + 1)
-   (x:_) -> x
-
-smallInstance :: Data a => a -> IO a
-smallInstance = mapVars (\_ -> return smallValue)
-
---
-
-refute :: (Show a, Data a) => Int -> (a -> Bool) -> IO Int
-refute d p = r initPData
-  where
-    r x = do res <- try (evaluate (p x))
-             case res of
-               Right True -> return 1
-               Right False -> stop x "Counter example found:"
-               Left (ErrorCall s)
-                 | take (lenUniquePrefix) s == uniquePrefix ->
-                     let pos = drop lenUniquePrefix s
-                     in  do ns <- mapM r (refinePData s d pos x)
-                            return (1 + sum ns)
-               Left e -> stop x "Property crashed on input:"
-
-    stop x s = do putStrLn s
-                  x' <- smallInstance x
-                  putStrLn (show x')
-                  exitWith ExitSuccess
-                     
---
-
-depthCheck :: (Show a, Data a) => Int -> (a -> Bool) -> IO ()
-depthCheck d f = do count <- refute d f
-                    putStrLn $ "Completed " ++ show count
-                            ++  " tests without finding a counter example."
-
---
-
-infixr 0 ==>
-
-(==>) :: Bool -> Bool -> Bool
-False ==> a = True
-True ==> a = a