diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,28 @@
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. 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.
+
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``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 AUTHORS 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.
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,257 @@
+---------------------------------------------------------------
+SmallCheck: another lightweight testing library in Haskell.
+Version 0.2, November 2006
+Colin Runciman, University of York UK
+
+After QuickCheck, by Koen Claessen and John Hughes (2000-2004).
+---------------------------------------------------------------
+
+If you are a Haskell programmer and a QuickCheck user do you ever wish
+you could:
+
+* write test generators for your own types more easily?
+* be sure that any counter-examples found are minimal?
+* write properties using existentials as well as universals?
+* establish complete coverage of a defined test-space?
+* display counter-examples of functional type?
+* guarantee repeatable test results?
+
+If so, try SmallCheck! This note should be enough to  get you started,
+assuming some prior experience with QuickCheck.
+
+Similarities and Differences
+----------------------------
+
+In many ways SmallCheck is very similar to QuickCheck.  It uses the
+idea of type-based generators for test data, and the way testable
+properties are expressed is closely based on the QuickCheck approach. Like
+QuickCheck, SmallCheck tests whether properties hold for finite completely
+defined values at specific types, and reports counter-examples.
+
+The big difference is that instead of using a sample of randomly generated
+values, SmallCheck tests properties for all the finitely many values
+up to some depth, progressively increasing the depth used.  For data
+values, depth means depth of construction.  For functional values, it
+is a measure combining the depth to which arguments may be evaluated
+and the depth of possible results.
+
+Generators
+----------
+
+Writing SmallCheck generators for application-specific types is
+straightforward.  Just as the QuickCheck user defines 'arbitrary'
+generators, so a SmallCheck user defines 'series' generators -- but
+it is a more straightforward task, using SmallCheck's cons<N> family
+of generic combinators where N is constructor arity.  For example:
+
+data Tree a = Null | Fork Tree a Tree
+
+instance Serial a => Serial (Tree a) where
+  series = cons0 Null \/ cons3 Fork
+
+The default interpretation of depth for datatypes is the depth of nested
+construction: constructor functions, including those for newtypes, build
+results with depth one greater than their deepest argument.  But this
+default can be over-ridden by composing a cons<N> application with an
+application of 'depth', like this:
+
+newtype Light a = Light a
+
+instance Serial a => Serial (Light a) where
+  series = cons1 Light . depth 0
+
+The depth of Light x is just the depth of x.
+
+To generate functions of an application-specific argument type requires a
+second method 'coseries' -- cf. 'coarbitrary' in QuickCheck.  Again there
+is a standard pattern, this time using the alts<N> combinators where
+again N is constructor arity.  Here are Tree and Light instances:
+
+  coseries d = [ \t -> case t of
+                       Null         -> z
+                       Fork t1 x t2 -> f t1 x t2
+               |  z <- alts0 d ,
+                  f <- alts3 d ]
+
+  coseries d = [ \l -> case l of
+                       Light x -> f x
+               |  f <- (alts1 . depth 0) d ]
+
+Properties
+----------
+
+SmallCheck's testable properties are closely based on those of QuickCheck
+but with the introduction of existential quantifiers.  Suppose we have
+defined a function
+
+isPrefix :: Eq a => [a] -> [a] -> Bool
+
+and wish to specify it by some suitable property.  Using QuickCheck we
+might define
+
+prop_isPrefix1 :: String -> String -> Bool
+prop_isPrefix1 xs ys = isPrefix xs (xs++ys)
+
+where xs and ys are universally quantified.  This property is necessary
+but not sufficient for a correct isPrefix.  For example, it is satisfied
+by the function that always returns True!  We can test the same property
+using SmallCheck.  But we can also test the following property, which
+involves an existentially quantified variable:
+
+prop_isPrefix2 :: String -> String -> Bool
+prop_isPrefix2 xs ys = isPrefix xs ys ==>
+                         exists $ \xs' -> ys == xs++xs'
+
+The default testing of existentials is bounded by the same depth as their
+context, here the depth-bound for xs and ys.  This rule has important
+consequences.  Just as a universal property may be satisfied when the
+depth bound is shallow but fail when it is deeper, so the reverse may be
+true for an existential property.  So when testing properties involving
+existentials it may be appropriate to try deeper testing after a shallow
+failure. However, sometimes the default same-depth-bound interpretation
+of existential properties can make testing of a valid property fail at
+all depths.  Here is a contrived but illustrative example:
+
+prop_append1 :: [Bool] -> [Bool] -> Property
+prop_append1 xs ys = exists $ \zs -> zs == xs++ys
+
+Customised variants of 'exists' are handy in such circumstances.
+For example, 'existsDeeperBy' transforms the depth bound by a given
+Int->Int function:
+
+prop_append2 :: [Bool] -> [Bool] -> Property
+prop_append2 xs ys = existsDeeperBy (*2) $ \zs -> zs == xs++ys
+
+QuickCheck's statistics-gathering operators have been omitted from
+SmallCheck's property language, as they seem more relevant to the
+random-testing approach.
+
+Pragmatics of ==>
+-----------------
+
+As in QuickCheck, the ==> operator can be used to express a restricting
+condition under which a property should hold.  For example, testing a
+propositional-logic module (see examples/logical), we might define:
+
+prop_tautEval :: Proposition -> Environment -> Property
+prop_tautEval p e =
+  tautology p ==> eval p e
+
+But here is an alternative definition:
+
+prop_tautEval :: Proposition -> Property
+prop_taut p =
+  tautology p ==> \e -> eval p e
+
+The first definition generates p and e for each test, whereas the second
+only generates e if the tautology p holds.  This difference is not great
+in QuickCheck where single random values are generated, but in SmallCheck
+the second definition is far better as the test-space is reduced from
+P*E to T'+T*E where P, T, T' and E are the numbers of propositions,
+tautologies, non-tautologies and environments.
+
+Testing
+-------
+
+Just as QuickCheck has a top-level function 'quickCheck' so SmallCheck
+has 'smallCheck d'.
+
+smallCheck  :: Testable a => Int -> a -> IO ()
+
+It runs series of tests using depth bounds 0..d, stopping if any test
+fails, and prints a summary report or a counter-example. The variant:
+
+smallCheckI :: Testable a =>        a -> IO ()
+ 
+is interactive. Instead of requiring a maximum-depth argument, it invites
+the user to decide whether to do deeper tests and whether to continue
+after a failure.  The interface is low-tech: y<return> (or just <return>)
+means "yes", anything else means "no".  For example:
+
+haskell> smallCheckI prop_append1
+Depth 0:
+  Completed 1 test(s) without failure.
+  Deeper? y
+Depth 1:
+  Failed test no. 5. Test values follow.
+  [True]
+  [True]
+  Continue? n
+  Deeper? n
+haskell>
+
+Having methods to generate series of all (depth-bounded) values of
+an argument type, SmallCheck can give at least partial information
+about the extension of a function.  For example, if we test the
+property
+
+prop_assoc op =
+  \x y z -> (x `op` y) `op` z == x `op` (y `op` z)
+  where
+  typeInfo = op :: Bool -> Bool -> Bool
+
+the result is shown as follows.
+
+haskell> smallCheckI prop_assoc
+Depth 0:
+  Failed test no. 22. Test values follow.
+  {True->{True->True;False->True};False->{True->False;False->True}}
+  False
+  True
+  False
+
+Large Test Spaces
+-----------------
+
+Using the standard generic scheme to define series of test value, it
+often turns out that at some small depth d the 10,000-100,000 tests
+are quickly checked, but at depth d+1 it is infeasible to complete
+the billions of tests.  There are ways to reduce some dimensions of
+the search space so that other dimensions can be tested more deeply:
+for example, cut the scope of quantifiers to a small fixed domain
+(forAllElem, thereExistsElem), use newtypes to define restricted series
+for some data types (see the 'examples' directory) or assign depth >1
+to some constructors.
+
+Function spaces grow exponentially in relation to their result and
+argument spaces.  Even with a depth bound, testing all functional
+arguments is a challenge.  Keep base-types as small as possible.
+For example, try testing higher-order polymorphic functions over their
+() or Bool instances.
+
+Version 0.1
+-----------
+
+The differences from 0.0 are two fixes (space-fault, output buffering),
+an 'unsafe' but sometimes useful Testable (IO a) instance and additional
+examples.
+
+Version 0.2
+-----------
+
+The 'smallCheck' driver now takes an argument d and runs test series
+at depths 0..d without interaction, stopping if any test fails.
+The interactive variant is still available as 'smallCheckI'.  All
+Prelude numeric types now have Serial instances, including floating-point
+types. Serial types Nat and Natural are also defined.  Examples extended.
+
+Final Notes
+-----------
+
+The name is intended to acknowledge QuickCheck, not to suggest that
+SmallCheck is a tool of equal refinement.
+
+SmallCheck is a Haskell 98 module aside from the import of unsafePerformIO
+for use in a single instance -- the import and instance can be commented
+out if there is no need to test IO computations.  I am not aware of any
+other portability issues.  SmallCheck can be obtained from:
+
+http://www.cs.york.ac.uk/fp/smallcheck0.2.tar
+
+Comments and suggestions are welcome.
+
+Thanks to Galois Connections, my hosts when I first wrote SmallCheck, and
+to users who have mailed me with feedback.
+
+Colin.Runciman@cs.york.ac.uk
+6 November 2006
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/Test/SmallCheck.hs b/Test/SmallCheck.hs
new file mode 100644
--- /dev/null
+++ b/Test/SmallCheck.hs
@@ -0,0 +1,398 @@
+---------------------------------------------------------------------
+-- SmallCheck: another lightweight testing library.
+-- Colin Runciman, August 2006
+-- Version 0.2 (November 2006)
+--
+-- After QuickCheck, by Koen Claessen and John Hughes (2000-2004).
+---------------------------------------------------------------------
+
+module Test.SmallCheck (
+  smallCheck, smallCheckI, depthCheck, test,
+  Property, Testable,
+  forAll, forAllElem,
+  exists, existsDeeperBy, thereExists, thereExistsElem,
+  (==>),
+  Series, Serial(..),
+  (\/), (><), two, three, four,
+  cons0, cons1, cons2, cons3, cons4,
+  alts0, alts1, alts2, alts3, alts4,
+  N(..), Nat, Natural,
+  depth, inc, dec
+  ) where
+
+import Data.List (intersperse)
+import Control.Monad (when)
+import System.IO (stdout, hFlush)
+import System.IO.Unsafe (unsafePerformIO)  -- used only for Testable (IO a)
+
+------------------ <Series of depth-bounded values> -----------------
+
+-- Series arguments should be interpreted as a depth bound (>=0)
+-- Series results should have finite length
+
+type Series a = Int -> [a]
+
+-- sum
+infixr 7 \/
+(\/) :: Series a -> Series a -> Series a
+s1 \/ s2 = \d -> s1 d ++ s2 d
+
+-- product
+infixr 8 ><
+(><) :: Series a -> Series b -> Series (a,b)
+s1 >< s2 = \d -> [(x,y) | x <- s1 d, y <- s2 d]
+
+------------------- <methods for type enumeration> ------------------
+
+-- enumerated data values should be finite and fully defined
+-- enumerated functional values should be total and strict
+
+-- bounds:
+-- for data values, the depth of nested constructor applications
+-- for functional values, both the depth of nested case analysis
+-- and the depth of results
+
+class Serial a where
+  series   :: Series a
+  coseries :: Serial b => Series (a->b)
+
+instance Serial () where
+  series   _ = [()]
+  coseries d = [ \() -> b
+               | b <- series d ]
+
+instance Serial Int where
+  series   d = [(-d)..d]
+  coseries d = [ \i -> if i > 0 then f (N (i - 1))
+                       else if i < 0 then g (N (abs i - 1))
+                       else z
+               | z <- alts0 d, f <- alts1 d, g <- alts1 d ]
+
+instance Serial Integer where
+  series   d = [ toInteger (i :: Int)
+               | i <- series d ]
+  coseries d = [ f . (fromInteger :: Integer->Int)
+               | f <- series d ]
+
+newtype N a = N a
+
+instance Show a => Show (N a) where
+  show (N i) = show i
+
+instance (Integral a, Serial a) => Serial (N a) where
+  series   d = map N [0..d']
+               where
+               d' = fromInteger (toInteger d)
+  coseries d = [ \(N i) -> if i > 0 then f (N (i - 1))
+                           else z
+               | z <- alts0 d, f <- alts1 d ]
+
+type Nat = N Int
+type Natural = N Integer
+
+instance Serial Float where
+  series d   = [ encodeFloat sig exp
+               | (sig,exp) <- series d,
+                 odd sig || sig==0 && exp==0 ]
+  coseries d = [ f . decodeFloat
+               | f <- series d ]
+
+instance Serial Double where
+  series   d = [ frac (x :: Float)
+               | x <- series d ]
+  coseries d = [ f . (frac :: Double->Float)
+               | f <- series d ]
+
+frac :: (Real a, Fractional a, Real b, Fractional b) => a -> b
+frac = fromRational . toRational
+
+instance Serial Char where
+  series d   = take (d+1) ['a'..'z']
+  coseries d = [ \c -> f (N (fromEnum c - fromEnum 'a'))
+               | f <- series d ]
+
+instance (Serial a, Serial b) =>
+         Serial (a,b) where
+  series   = series >< series
+  coseries = map uncurry . coseries
+
+instance (Serial a, Serial b, Serial c) =>
+         Serial (a,b,c) where
+  series   = \d -> [(a,b,c) | (a,(b,c)) <- series d]
+  coseries = map uncurry3 . coseries
+
+instance (Serial a, Serial b, Serial c, Serial d) =>
+         Serial (a,b,c,d) where
+  series   = \d -> [(a,b,c,d) | (a,(b,(c,d))) <- series d]
+  coseries = map uncurry4 . coseries
+
+uncurry3 :: (a->b->c->d) -> ((a,b,c)->d)
+uncurry3 f (x,y,z) = f x y z
+
+uncurry4 :: (a->b->c->d->e) -> ((a,b,c,d)->e)
+uncurry4 f (w,x,y,z) = f w x y z
+
+two   :: Series a -> Series (a,a)
+two   s = s >< s
+
+three :: Series a -> Series (a,a,a)
+three s = \d -> [(x,y,z) | (x,(y,z)) <- (s >< s >< s) d]
+
+four  :: Series a -> Series (a,a,a,a)
+four  s = \d -> [(w,x,y,z) | (w,(x,(y,z))) <- (s >< s >< s >< s) d]
+
+cons0 ::
+         a -> Series a
+cons0 c _ = [c]
+
+cons1 :: Serial a =>
+         (a->b) -> Series b
+cons1 c d = [c z | d > 0, z <- series (d-1)]
+
+cons2 :: (Serial a, Serial b) =>
+         (a->b->c) -> Series c
+cons2 c d = [c y z | d > 0, (y,z) <- series (d-1)]
+
+cons3 :: (Serial a, Serial b, Serial c) =>
+         (a->b->c->d) -> Series d
+cons3 c d = [c x y z | d > 0, (x,y,z) <- series (d-1)]
+
+cons4 :: (Serial a, Serial b, Serial c, Serial d) =>
+         (a->b->c->d->e) -> Series e
+cons4 c d = [c w x y z | d > 0, (w,x,y,z) <- series (d-1)]
+
+alts0 ::  Serial a =>
+            Series a
+alts0 d = series d
+
+alts1 ::  (Serial a, Serial b) =>
+            Series (a->b)
+alts1 d = if d > 0 then series (dec d)
+          else [\_ -> x | x <- series d]
+
+alts2 ::  (Serial a, Serial b, Serial c) =>
+            Series (a->b->c)
+alts2 d = if d > 0 then series (dec d)
+          else [\_ _ -> x | x <- series d]
+
+alts3 ::  (Serial a, Serial b, Serial c, Serial d) =>
+            Series (a->b->c->d)
+alts3 d = if d > 0 then series (dec d)
+          else [\_ _ _ -> x | x <- series d]
+
+alts4 ::  (Serial a, Serial b, Serial c, Serial d, Serial e) =>
+            Series (a->b->c->d->e)
+alts4 d = if d > 0 then series (dec d)
+          else [\_ _ _ _ -> x | x <- series d]
+
+instance Serial Bool where
+  series     = cons0 True \/ cons0 False
+  coseries d = [ \x -> if x then b1 else b2
+               | (b1,b2) <- series d ]
+
+instance Serial a => Serial (Maybe a) where
+  series     = cons0 Nothing \/ cons1 Just
+  coseries d = [ \m -> case m of
+                       Nothing -> z
+                       Just x  -> f x
+               |  z <- alts0 d ,
+                  f <- alts1 d ]
+
+instance (Serial a, Serial b) => Serial (Either a b) where
+  series     = cons1 Left \/ cons1 Right
+  coseries d = [ \e -> case e of
+                       Left x  -> f x
+                       Right y -> g y
+               |  f <- alts1 d ,
+                  g <- alts1 d ]
+
+instance Serial a => Serial [a] where
+  series     = cons0 [] \/ cons2 (:)
+  coseries d = [ \xs -> case xs of
+                        []      -> y
+                        (x:xs') -> f x xs'
+               |   y <- alts0 d ,
+                   f <- alts2 d ]
+
+-- Warning: the coseries instance here may generate duplicates.
+instance (Serial a, Serial b) => Serial (a->b) where
+  series = coseries
+  coseries d = [ \f -> g [f x | x <- series d]
+               | g <- series d ]
+
+-- For customising the depth measure.  Use with care!
+
+depth :: Int -> Int -> Int
+depth d d' | d >= 0    = d'+1-d
+           | otherwise = error "SmallCheck.depth: argument < 0"
+
+dec :: Int -> Int
+dec d | d > 0     = d-1
+      | otherwise = error "SmallCheck.dec: argument <= 0"
+
+inc :: Int -> Int
+inc d = d+1
+
+-- show the extension of a function (in part, bounded both by
+-- the number and depth of arguments)
+instance (Serial a, Show a, Show b) => Show (a->b) where
+  show f =
+    if maxarheight == 1
+    && sumarwidth + length ars * length "->;" < widthLimit then
+      "{"++(
+      concat $ intersperse ";" $ [a++"->"++r | (a,r) <- ars]
+      )++"}"
+    else
+      concat $ [a++"->\n"++indent r | (a,r) <- ars]
+    where
+    ars = take lengthLimit [ (show x, show (f x))
+                           | x <- series depthLimit ]
+    maxarheight = maximum  [ max (height a) (height r)
+                           | (a,r) <- ars ]
+    sumarwidth = sum       [ length a + length r
+                           | (a,r) <- ars]
+    indent = unlines . map ("  "++) . lines
+    height = length . lines
+    (widthLimit,lengthLimit,depthLimit) = (80,20,3)::(Int,Int,Int)
+
+---------------- <properties and their evaluation> ------------------
+
+-- adapted from QuickCheck originals: here results come in lists,
+-- properties have depth arguments, stamps (for classifying random
+-- tests) are omitted, existentials are introduced
+
+newtype PR = Prop [Result]
+
+data Result = Result {ok :: Maybe Bool, arguments :: [String]}
+
+nothing :: Result
+nothing = Result {ok = Nothing, arguments = []}
+
+result :: Result -> PR
+result res = Prop [res]
+
+newtype Property = Property (Int -> PR)
+
+class Testable a where
+  property :: a -> Int -> PR
+
+instance Testable Bool where
+  property b _ = Prop [Result (Just b) []]
+
+instance Testable PR where
+  property prop _ = prop
+
+instance (Serial a, Show a, Testable b) => Testable (a->b) where
+  property f = f' where Property f' = forAll series f
+
+instance Testable Property where
+  property (Property f) d = f d
+
+-- For testing properties involving IO.  Unsafe, so use with care!
+instance Testable a => Testable (IO a) where
+  property = property . unsafePerformIO
+
+evaluate :: Testable a => a -> Series Result
+evaluate x d = rs where Prop rs = property x d
+
+forAll :: (Show a, Testable b) => Series a -> (a->b) -> Property
+forAll xs f = Property $ \d -> Prop $
+  [ r{arguments = show x : arguments r}
+  | x <- xs d, r <- evaluate (f x) d ]
+
+forAllElem :: (Show a, Testable b) => [a] -> (a->b) -> Property
+forAllElem xs = forAll (const xs)
+
+thereExists :: Testable b => Series a -> (a->b) -> Property
+thereExists xs f = Property $ \d -> Prop $
+  [ Result
+      ( Just $ or [ all pass (evaluate (f x) d)
+                  | x <- xs d ] )
+      [] ]
+  where
+  pass (Result Nothing _)  = True
+  pass (Result (Just b) _) = b
+
+thereExistsElem :: Testable b => [a] -> (a->b) -> Property
+thereExistsElem xs = thereExists (const xs)
+
+exists :: (Serial a, Testable b) =>
+            (a->b) -> Property
+exists = thereExists series
+
+existsDeeperBy :: (Serial a, Testable b) =>
+                    (Int->Int) -> (a->b) -> Property
+existsDeeperBy f = thereExists (series . f)
+
+infixr 0 ==>
+
+(==>) :: Testable a => Bool -> a -> Property
+True ==>  x = Property (property x)
+False ==> x = Property (const (result nothing))
+
+--------------------- <top-level test drivers> ----------------------
+
+-- similar in spirit to QuickCheck but with iterative deepening
+
+test :: Testable a => a -> IO ()
+test = smallCheckI
+
+-- test for values of depths 0..d stopping when a property
+-- fails or when it has been checked for all these values
+smallCheck :: Testable a => Int -> a -> IO ()
+smallCheck d = iterCheck 0 (Just d)
+
+-- interactive variant, asking the user whether testing should
+-- continue/go deeper after a failure/completed iteration
+smallCheckI :: Testable a => a -> IO ()
+smallCheckI = iterCheck 0 Nothing
+
+depthCheck :: Testable a => Int -> a -> IO ()
+depthCheck d = iterCheck d (Just d)
+
+iterCheck :: Testable a => Int -> Maybe Int -> a -> IO ()
+iterCheck dFrom mdTo t = iter dFrom
+  where
+  iter d = do
+    putStrLn ("Depth "++show d++":")
+    let Prop results = property t d
+    ok <- check (mdTo==Nothing) 0 0 True results
+    maybe (whenUserWishes "  Deeper" () $ iter (d+1))
+          (\dTo -> when (ok && d < dTo) $ iter (d+1))
+          mdTo
+
+check :: Bool -> Int -> Int -> Bool -> [Result] -> IO Bool
+check i n x ok rs | null rs = do
+  putStr ("  Completed "++show n++" test(s)")
+  putStrLn (if ok then " without failure." else ".")
+  when (x > 0) $
+    putStrLn ("  But "++show x++" did not meet ==> condition.")
+  return ok
+check i n x ok (Result Nothing _ : rs) = do
+  progressReport i n x
+  check i (n+1) (x+1) ok rs
+check i n x f (Result (Just True) _ : rs) = do
+  progressReport i n x
+  check i (n+1) x f rs
+check i n x f (Result (Just False) args : rs) = do
+  putStrLn ("  Failed test no. "++show (n+1)++". Test values follow.")
+  mapM_ (putStrLn . ("  "++)) args
+  ( if i then
+      whenUserWishes "  Continue" False $ check i (n+1) x False rs
+    else
+      return False )
+
+whenUserWishes :: String -> a -> IO a -> IO a
+whenUserWishes wish x action = do
+  putStr (wish++"? ")
+  hFlush stdout
+  reply <- getLine
+  ( if (null reply || reply=="y") then action
+    else return x )
+
+progressReport :: Bool -> Int -> Int -> IO ()
+progressReport i n x | n >= x = do
+  when i $ ( putStr (n' ++ replicate (length n') '\b') >>
+             hFlush stdout )
+  where
+  n' = show n
diff --git a/examples/imperative/Behaviour.hs b/examples/imperative/Behaviour.hs
new file mode 100644
--- /dev/null
+++ b/examples/imperative/Behaviour.hs
@@ -0,0 +1,23 @@
+module Behaviour(Trace(..),(+++),approx) where
+
+data Trace a
+  = Step (Trace a)
+  | a :> Trace a
+  | End
+  | Crash
+  deriving (Eq, Show)
+
+(+++) :: Trace a -> Trace a -> Trace a
+Step s   +++ t = Step (s +++ t)
+(x :> s) +++ t = x :> (s +++ t)
+End      +++ t = t
+Crash    +++ t = Crash
+
+approx :: Eq a => Int -> Trace a -> Trace a -> Bool
+approx 0 _        _        = True
+approx n (a :> s) (b :> t) = a == b && approx (n-1) s t
+approx n (Step s) (Step t) = approx (n-1) s t
+approx n End    End        = True
+approx n Crash  Crash      = True
+approx n _        _        = False
+
diff --git a/examples/imperative/Compiler.hs b/examples/imperative/Compiler.hs
new file mode 100644
--- /dev/null
+++ b/examples/imperative/Compiler.hs
@@ -0,0 +1,59 @@
+module Compiler(compile) where
+
+import Machine
+import Syntax
+import StackMap
+import Value
+
+compile :: Command -> [Instruction]
+compile c =
+  replicate (depth sm) (Push Wrong) ++
+  compObey sm c ++
+  [Halt]
+  where
+  sm = stackMap c
+
+compObey :: StackMap -> Command -> [Instruction]
+compObey sm Skip = 
+  []
+compObey sm (v := e) =
+  compEval sm e ++
+  [Store (location sm v + 1)]
+compObey sm (c1 :-> c2) =
+  compObey sm c1 ++
+  compObey sm c2
+compObey sm (If e c1 c2) =
+  compEval sm e ++
+  [JumpUnless (length isc1 + 1)] ++
+  isc1 ++
+  [Jump (length isc2)] ++
+  isc2
+  where
+  isc1 = compObey sm c1
+  isc2 = compObey sm c2
+compObey sm (While e c) =
+  ise ++
+  [JumpUnless (length isc + 1)] ++
+  isc ++
+  [Jump (negate (length isc + 1 + length ise + 1))]
+  where
+  ise = compEval sm e
+  isc = compObey sm c
+compObey sm (Print e) =
+  compEval sm e ++
+  [Display]
+
+compEval :: StackMap -> Expr -> [Instruction]
+compEval sm (Val v) =
+  [Push v]
+compEval sm (Var v) =
+  [Fetch (location sm v)]
+compEval sm (Uno op1 e) =
+  -- was op before arg eval  
+  compEval sm e ++
+  [Instr1 op1]
+compEval sm (Duo op2 e1 e2) =
+  -- was op before arg evals  
+  compEval sm        e1 ++
+  compEval (push sm) e2 ++
+  [Instr2 op2]
diff --git a/examples/imperative/Interpreter.hs b/examples/imperative/Interpreter.hs
new file mode 100644
--- /dev/null
+++ b/examples/imperative/Interpreter.hs
@@ -0,0 +1,41 @@
+module Interpreter(obey) where
+
+import Syntax
+import Behaviour
+import Value
+
+type Env = [(Name,Value)]
+
+obey :: Command -> Trace Value
+obey p = fst (run p [])
+
+look :: Name -> Env -> Value
+look x s = maybe Wrong id (lookup x s)
+
+update :: Name -> Value -> Env -> Env
+update x a s = (x,a) : filter (\(y,_) -> y/=x) s
+
+run :: Command -> Env -> (Trace Value, Env)
+run Skip        s = (End, s)
+run (x := e)    s = (End, update x (eval e s) s)
+run (p :-> q)   s = let (outp, sp) = run p s
+                        (outq, sq) = run q sp
+                    in (outp +++ outq, sq)
+run (If e p q)  s = case eval e s of
+                    -- was True -> q, False -> p
+                    Log True  -> run p s
+                    Log False -> run q s
+                    _         -> (Crash, s)
+run (While e p) s = case eval e s of
+                    Log True  -> let (outp,sp) = run p s
+                                     (outw,sw) = run (While e p) sp
+                                 in (outp +++ Step outw, sw)
+                    Log False -> (End, s)
+                    _         -> (Crash, s)
+run (Print e)   s = (eval e s :> End, s)
+
+eval :: Expr -> Env -> Value
+eval (Var x)      s = look x s
+eval (Val v)      s = v
+eval (Uno op a)   s = uno op (eval a s)
+eval (Duo op a b) s = duo op (eval a s) (eval b s)
diff --git a/examples/imperative/Machine.hs b/examples/imperative/Machine.hs
new file mode 100644
--- /dev/null
+++ b/examples/imperative/Machine.hs
@@ -0,0 +1,50 @@
+module Machine(Instruction(..), exec) where
+
+import Array
+import Behaviour
+import Value
+
+data Instruction
+  = Push Value
+  | Pop
+  | Fetch Int
+  | Store Int
+  | Instr1 Op1
+  | Instr2 Op2
+  | Display
+  | Jump Int
+  | JumpUnless Int
+  | Halt
+ deriving (Eq, Show)
+ 
+exec :: [Instruction] -> Trace Value
+exec instrs = run 1 []
+  where
+  size   = length instrs
+  memory = array (1,size) ([1..] `zip` instrs)
+  run pc stack =
+    if pc < 1 || size < pc then Crash
+    else
+      case (memory ! pc, stack) of
+      (Push x	    , stack)          -> run pc' (x : stack)
+      (Pop	    , _ : stack)      -> run pc' stack
+      (Fetch n      , stack)	 
+        | length stack >  n           -> run pc' (stack !! n : stack)
+      (Store n      , x : stack)
+        | length stack >= n           -> run pc' (take (n-1) stack ++
+                                                  x : drop n stack)
+      (Instr1 op1   , i : stack)      -> run pc' (uno op1 i : stack)
+      (Instr2 op2   , i : j : stack)  -> run pc' (duo op2 j i : stack)
+      (Display      , i : stack)      -> i :> run pc' stack
+      (Jump n	    , stack)	      -> step n (run (pc' + n) stack)
+      (JumpUnless n , Log b : stack)
+        | b	                      -> run pc' stack
+        | otherwise                   -> step n (run (pc' + n) stack)
+      (Halt	    , stack)	      -> End
+      _ 			      -> Crash
+     where
+      pc' = pc + 1
+
+step :: Int -> Trace Value -> Trace Value    
+step n t | n < 0     = Step t
+         | otherwise = t
diff --git a/examples/imperative/Properties.hs b/examples/imperative/Properties.hs
new file mode 100644
--- /dev/null
+++ b/examples/imperative/Properties.hs
@@ -0,0 +1,178 @@
+import Behaviour
+import Interpreter
+import Compiler
+import Machine
+import Syntax
+import Value
+
+import Test.SmallCheck
+
+------------- <series of expressions and commands> -------------
+
+-- In the abstract syntax variables are just strings,
+-- but we do not want to enumerate all lists of characters.
+-- Just a couple of distinct names.
+
+newtype VarName = VarName Name
+
+instance Serial VarName where
+  series = const [VarName [c] | c <- ['a'..'b']]
+
+var :: VarName -> Expr
+var (VarName v) = Var v
+
+assign :: VarName -> Expr -> Command
+assign (VarName v) e = (v := e)
+
+-- Uses of depth 0 ensure that all occurrences of variables
+-- or literals are treated as zero-depth atoms.
+-- The rest is completely standard, but for the use of
+-- 'var' for Var and 'assign' for Assign.
+
+instance Serial Value where
+  series = cons0 Wrong
+        \/ cons1 Log . depth 0
+        \/ cons1 Num . depth 0
+
+instance Serial Op1 where
+  series = const [Not, Minus]
+
+instance Serial Op2 where
+  series = const [And, Or, Eq, Less, LessEq,
+                  Add, Sub, Mul, Div, Mod]
+
+instance Serial Expr where
+  series = cons1 var . depth 0
+        \/ cons1 Val . depth 0
+        \/ cons2 Uno
+        \/ cons3 Duo
+
+instance Serial Command where
+  series = cons0 Skip
+        \/ cons1 Print
+        \/ cons2 assign
+        \/ cons2 (:->)
+        \/ cons3 If
+        \/ cons2 While
+
+----------------- <Closed Expressions> -------------------
+
+-- If we want a series for a subset of the values in
+-- a given type, one way to define it is via a newtype.
+-- Here, expressions without variables.
+
+newtype ClosedExpr = Closed Expr deriving Show
+
+instance Serial ClosedExpr where
+  series = cons1 val . depth 0
+        \/ cons2 uno
+        \/ cons3 duo
+    where
+    val v = Closed (Val v)
+    uno op (Closed e) = Closed (Uno op e)
+    duo op (Closed e1) (Closed e2) = Closed (Duo op e1 e2)
+
+----------------- <Customised Programs> -----------------
+
+-- The space of all commands grows very quickly with depth,
+-- and many syntactically legal commands are bound to fail.
+-- Here we define a restricted subset of commands in a
+-- 'standard form':
+-- -- Skip only occurs as an else-alternative
+-- -- Print is only applied to simple variables
+-- -- Only integer values are assigned to variables.
+-- -- If and While conditions are compound comparisons.
+
+newtype StdCommand = Std Command deriving Show
+
+instance Serial StdCommand where
+  series = cons1 print'
+        \/ cons2 assign'
+        \/ cons2 seq'
+        \/ cons3 if'
+        \/ cons2 while'
+    where
+    print'  (VarName v)                   = Std (Print (Var v))
+    assign' (VarName v) (I e)             = Std (v := e)
+    seq'    (Std c0) (Std c1)             = Std (c0 :-> c1)
+    if'     (B e) (Std c0) (SkipOrStd c1) = Std (If e c0 c1)
+    while'  (B e) (Std c)                 = Std (While e c)
+
+newtype SkipOrStdCommand = SkipOrStd Command
+
+instance Serial SkipOrStdCommand where
+  series = cons0 skip
+        \/ cons1 std . depth 0
+    where
+    skip        = SkipOrStd Skip
+    std (Std c) = SkipOrStd c
+
+newtype IExpr = I Expr
+
+instance Serial IExpr where
+  series = cons1 var' . depth 0
+        \/ cons1 val' . depth 0
+        \/ cons1 uno'
+        \/ cons3 duo'
+    where
+    var' (VarName v)          = I (Var v)
+    val' i                    = I (Val (Num i))
+    uno' (I e)                = I (Uno Minus e)
+    duo' (I2 d) (I e0) (I e1) = I (Duo d e0 e1)
+
+newtype IOp2 = I2 Op2
+
+instance Serial IOp2 where
+  series = const [I2 op | op <- [Add, Sub, Mul, Div, Mod]]
+
+newtype BExpr = B Expr
+
+instance Serial BExpr where
+  series = cons1 uno'
+        \/ cons3 duo'
+        \/ cons3 cmp'
+    where
+    uno' (B e)                = B (Uno Not e)
+    duo' (B2 d) (B e0) (B e1) = B (Duo d e0 e1)
+    cmp' (C2 c) (I e0) (I e1) = B (Duo c e0 e1)
+
+newtype BOp2 = B2 Op2
+
+instance Serial BOp2 where
+  series = const [B2 op | op <- [And,Or]]
+
+newtype COp2 = C2 Op2
+
+instance Serial COp2 where
+  series = const [C2 op | op <- [Eq,Less,LessEq]]
+
+-------- <depth-bounded equivalence of program traces> --------
+
+newtype Approx = Approx Int deriving Show
+
+instance Serial Approx where
+  series d = [Approx d]
+
+(=~=) :: Eq a => Trace a -> Trace a -> Approx -> Bool
+s =~= t = \(Approx d) -> approx d s t
+
+----------------- <congruence properties> ------------------
+
+prop_Congruence :: Command -> Property
+prop_Congruence p =
+  t1 /= Crash || t2 /= Crash ==>
+    (t1 =~= t2)
+  where
+  t1 = obey p
+  t2 = exec (compile p)
+
+prop_StdCongruence :: StdCommand -> Property
+prop_StdCongruence (Std p) =
+  prop_Congruence p
+
+main :: IO ()
+main = do
+  putStrLn "-- congruence for all programs:"
+  smallCheck 2 prop_Congruence
+  putStrLn "-- congruence for standard-form programs:"
+  smallCheck 2 prop_StdCongruence
diff --git a/examples/imperative/README b/examples/imperative/README
new file mode 100644
--- /dev/null
+++ b/examples/imperative/README
@@ -0,0 +1,10 @@
+First see ../../README.
+
+This directory gives the largest illustrative example.  We test for
+congruence between an interpreter and compiler for a small imperative
+language.  The example is adapted from an original using QuickCheck,
+as described in the lecture notes for AFP'02 (LNCS 2638).  Compared
+with the simpler example in ../logic, here specialised instances
+are used to restrict the input space to programs in a standard form.
+Run Properties.main and compare the rate of growth for the last two
+properties tested.
diff --git a/examples/imperative/StackMap.hs b/examples/imperative/StackMap.hs
new file mode 100644
--- /dev/null
+++ b/examples/imperative/StackMap.hs
@@ -0,0 +1,35 @@
+module StackMap where
+
+import Syntax
+import List( union )
+
+type StackMap = (Int,[Name])
+
+stackMap :: Command -> StackMap
+stackMap c = (0, comVars c)
+
+push :: StackMap -> StackMap
+push (n, vars) = (n+1, vars)
+
+pop :: StackMap -> StackMap
+pop (n, vars) = (n-1, vars)
+
+location :: StackMap -> Name -> Int
+location (n, vars) v = n + length (takeWhile (/=v) vars)
+
+depth :: StackMap -> Int
+depth (n, vars) = n + length vars
+
+expVars :: Expr -> [Name]
+expVars (Var v)     = [v]
+expVars (Val _)     = []
+expVars (Uno _ a)   = expVars a
+expVars (Duo _ a b) = expVars a `union` expVars b
+
+comVars :: Command -> [Name]
+comVars Skip         = []
+comVars (x := e)     = [x] `union` expVars e
+comVars (c1 :-> c2)  = comVars c1 `union` comVars c2
+comVars (If e c1 c2) = expVars e `union` comVars c1 `union` comVars c2
+comVars (While e c)  = expVars e `union` comVars c
+comVars (Print e)    = expVars e
diff --git a/examples/imperative/Syntax.hs b/examples/imperative/Syntax.hs
new file mode 100644
--- /dev/null
+++ b/examples/imperative/Syntax.hs
@@ -0,0 +1,21 @@
+module Syntax(Name, Expr(..), Command(..)) where
+
+import Value
+
+type Name = String
+
+data Expr
+  = Var Name
+  | Val Value
+  | Uno Op1 Expr
+  | Duo Op2 Expr Expr
+  deriving (Eq, Show)
+
+data Command
+  = Skip
+  | Name := Expr
+  | Command :-> Command
+  | If Expr Command Command
+  | While Expr Command
+  | Print Expr
+  deriving (Eq, Show)
diff --git a/examples/imperative/Value.hs b/examples/imperative/Value.hs
new file mode 100644
--- /dev/null
+++ b/examples/imperative/Value.hs
@@ -0,0 +1,44 @@
+module Value(Value(..), Op1(..), Op2(..), uno, duo) where
+
+data Value
+  = Num Int
+  | Log Bool
+  | Wrong
+  deriving (Eq, Show)
+
+data Op1
+  = Not
+  | Minus
+  deriving (Eq, Show)
+
+data Op2
+  = And
+  | Or
+  | Mul
+  | Add
+  | Sub
+  | Div
+  | Mod
+  | Less
+  | LessEq 
+  | Eq
+  deriving (Eq, Show)
+
+uno :: Op1 -> Value -> Value
+uno Not   (Log b) = Log (not b)
+uno Minus (Num n) = Num (negate n)
+uno _     _       = Wrong
+
+duo :: Op2 -> Value -> Value -> Value
+duo And     (Log a) (Log b)          = Log (a && b)
+duo Or      (Log a) (Log b)          = Log (a || b)
+duo Eq      (Log a) (Log b)          = Log (a == b)
+duo Mul     (Num m) (Num n)          = Num (m * n)
+duo Add     (Num m) (Num n)          = Num (m + n)
+duo Sub     (Num m) (Num n)          = Num (m - n)
+duo Div     (Num m) (Num n) | n /= 0 = Num (m `div` n)
+duo Mod     (Num m) (Num n) | n /= 0 = Num (m `mod` n)
+duo Less    (Num m) (Num n)          = Log (m < n)
+duo LessEq  (Num m) (Num n)          = Log (m <= n)
+duo Eq      (Num m) (Num n)          = Log (m == n)
+duo _       _       _                = Wrong
diff --git a/examples/listy/ListProps.hs b/examples/listy/ListProps.hs
new file mode 100644
--- /dev/null
+++ b/examples/listy/ListProps.hs
@@ -0,0 +1,92 @@
+------------------------------------------------
+-- Properties (some valid some invalid) of a few
+-- standard list-processing functions.
+-- A test module for SmallCheck.
+-- Colin Runciman, August 2006.
+-- Revised for 0.2, November 2006.
+------------------------------------------------
+
+module ListProps where
+
+import Test.SmallCheck
+
+-- properties about higher-order functions
+-- plausible-looking but invalid laws about folds
+
+prop_fold1 :: [Bool] -> Property
+prop_fold1 xs =
+  not (null xs) ==>
+    \f -> foldl1 f xs == foldr1 f xs
+
+prop_fold2 :: [Bool] -> [Bool] -> Property
+prop_fold2 xs ys =
+  not (null xs) && not (null ys) ==>
+    \f -> foldr1 f xs `f` foldr1 f ys == foldr1 f (xs++ys)
+
+-- properties using 'exists' with data and functional arguments
+
+-- invalid because depth-bound for zs same as for xs ys
+prop_union1 :: [Bool] -> [Bool] -> Property
+prop_union1 xs ys =
+  exists $ \zs ->
+    \b -> (b `elem` zs) == (b `elem` xs || b `elem` ys)
+
+-- valid variant: depth-bound doubled in existential
+prop_union2 :: [Bool] -> [Bool] -> Property
+prop_union2 xs ys =
+  existsDeeperBy (*2) $ \zs ->
+    \b -> (b `elem` zs) == (b `elem` xs || b `elem` ys)
+
+-- do magical span arguments exist?
+prop_span1 :: [Bool] -> [Bool] -> [Bool] -> Property
+prop_span1 xs ys zs =
+  xs++ys == zs ==> exists $ \t -> (xs,ys) == span t zs
+
+-- deliberate mistake in final isPrefix equation
+isPrefix :: Ord a => [a] -> [a] -> Bool
+isPrefix [] ys = True
+isPrefix (x:xs) [] = False
+isPrefix (x:xs) (y:ys) = x==y || isPrefix xs ys
+
+-- this completeness property still holds
+isPrefixComplete :: String -> String -> Bool
+isPrefixComplete xs ys =
+  isPrefix xs (xs ++ ys)
+
+-- but this existential soundness property fails
+isPrefixSound :: String -> String -> Property
+isPrefixSound xs ys = isPrefix xs ys ==>
+  exists $ \xs' -> ys == (xs ++ xs')
+
+main :: IO ()
+main = do
+  test1 "\\xs -> not (null xs) ==>\n\
+        \  \\f -> foldl1 f xs == foldr1 f xs ?"
+        prop_fold1
+  test1 "\\xs ys -> not (null xs) && not (null ys) ==>\n \
+        \  \\f -> foldr1 f xs `f` foldr1 f ys == foldr1 f (xs++ys) ?"
+        prop_fold2
+  test1 "\\xs ys -> exists $ \\zs ->\n\
+        \  \\b -> (b `elem` zs) == (b `elem` xs || b `elem` ys) ?"
+        prop_union1
+  test1 "\\xs ys -> existsDeeperBy (*2) $ \\zs ->\n\
+        \  \\b -> (b `elem` zs) == (b `elem` xs || b `elem` ys) ?"
+        prop_union2
+  test1 "\\xs ys zs -> xs++ys==zs ==>\n\
+        \  exists $ \\t -> (xs,ys) == span t zs ?"
+        prop_span1
+  test1 "\\xs ys -> isPrefix xs (xs++ys) ?"
+        isPrefixComplete
+  test1 "\\xs ys zs -> isPrefix xs ys ==>\n\
+        \  exists $ \\xs' -> ys == xs ++ xs' ?"
+        isPrefixSound
+
+test1 :: Testable a => String -> a -> IO ()
+test1 s t = do
+  rule
+  putStrLn s
+  rule
+  smallCheck 4 t
+  where
+  rule = putStrLn "----------------------------------------------------"
+
diff --git a/examples/listy/README b/examples/listy/README
new file mode 100644
--- /dev/null
+++ b/examples/listy/README
@@ -0,0 +1,5 @@
+First see ../../README.
+
+In this directory, compile or interpret ListProps.main (SmallCheck
+is the only other module required) for a small selection of
+self-introducing tests of list-processing functions.
diff --git a/examples/logical/LogicProps.hs b/examples/logical/LogicProps.hs
new file mode 100644
--- /dev/null
+++ b/examples/logical/LogicProps.hs
@@ -0,0 +1,128 @@
+----------------------------------------------------
+-- Propositional formulae, satisfiable, tautologous.
+-- A test module for SmallCheck.
+-- Colin Runciman, August 2006.
+----------------------------------------------------
+
+module PropLogic where
+
+import Test.SmallCheck
+
+import Data.List (nub)
+
+data Prop = Var Name
+          | Not Prop
+          | And Prop Prop
+          | Or  Prop Prop
+          | Imp Prop Prop
+
+instance Show Prop where
+  show p = case p of
+           Var n   -> show n
+           Not q   -> "~"++show' q
+           And q r -> show' q++"&"++show' r
+           Or  q r -> show' q++"|"++show' r
+           Imp q r -> show' q++"=>"++show' r
+    where
+    show' x = if priority p > priority x then "("++show x++")"
+              else show x
+    priority (Var _)   = 5
+    priority (Not _)   = 4
+    priority (And _ _) = 3
+    priority (Or  _ _) = 2
+    priority (Imp _ _) = 1
+
+data Name = P | Q | R deriving (Eq,Show)
+
+type Env = Name -> Bool
+
+eval :: Prop -> Env -> Bool
+eval (Var v)   env = env v
+eval (Not p)   env = not (eval p env)
+eval (And p q) env = eval p env && eval q env
+eval (Or  p q) env = eval p env || eval q env
+eval (Imp p q) env = eval p env <= eval q env
+
+envsFor :: Prop -> [Env]
+envsFor p = foldr bind [const False] (nub (varsOf p))
+  where
+  bind v es = concat [ [\x -> x==v || e x, e]
+                     | e <- es ]
+
+varsOf :: Prop -> [Name]
+varsOf (Var v)   = [v]
+varsOf (Not p)   = varsOf p
+varsOf (And p q) = varsOf p ++ varsOf q
+varsOf (Or  p q) = varsOf p ++ varsOf q
+varsOf (Imp p q) = varsOf p ++ varsOf q
+
+tautologous :: Prop -> Bool
+tautologous p = all (eval p) (envsFor p)
+
+satisfiable :: Prop -> Bool
+satisfiable p = any (eval p) (envsFor p)
+
+instance Serial Name where
+  series     = cons0 P \/ cons0 Q \/ cons0 R
+  coseries d = [ \n -> case n of
+                       P -> x ; Q -> y ; R -> z
+               |  x <- alts0 d, y <- alts0 d, z <- alts0 d ]
+
+instance Serial Prop where
+  series = cons1 Var
+        \/ cons1 Not
+        \/ cons2 And
+        \/ cons2 Or
+        \/ cons2 Imp
+
+---------------------- <properties for testing> ---------------------
+
+prop_taut1 :: Prop -> Property
+prop_taut1 p =
+  tautologous p ==> \e -> eval p e
+
+prop_taut2 :: Prop -> Property
+prop_taut2 p =
+  not (tautologous p) ==> exists (\e -> not $ eval p e)
+
+prop_sat1 :: Prop -> Env -> Property
+prop_sat1 p e =
+  eval p e ==> satisfiable p
+
+prop_sat2 :: Prop -> Property
+prop_sat2 p =
+  satisfiable p ==> exists (\e -> eval p e)
+
+prop_tautSat1 :: Prop -> Property
+prop_tautSat1 p =
+  not (tautologous p) ==> satisfiable (Not p)
+
+prop_tautSat2 :: Prop -> Property
+prop_tautSat2 p =
+  not (satisfiable p) ==> tautologous (Not p)
+
+main :: IO ()
+main = do
+  test1 "\\p -> tautologous p ==> \\e -> eval p e ?"
+        prop_taut1
+  test1 "\\p -> not (tautologous p) ==>\n\
+        \  exists (\\e -> not $ eval p e) ?"
+        prop_taut2
+  test1 "\\p e -> eval p e ==> satisfiable p ?"
+        prop_sat1
+  test1 "\\p -> satisfiable p ==> exists (\\e -> eval p e) ?"
+        prop_sat2
+  test1 "\\p -> not (tautologous p) ==> satisfiable (Not p) ?"
+        prop_tautSat1
+  test1 "\\p -> not (satisfiable p) ==> tautologous (Not p) ?"
+        prop_tautSat2
+
+test1 :: Testable a => String -> a -> IO ()
+test1 s t = do
+  rule
+  putStrLn s
+  rule
+  smallCheck 3 t
+  where
+  rule = putStrLn "----------------------------------------------------"
+
diff --git a/examples/logical/README b/examples/logical/README
new file mode 100644
--- /dev/null
+++ b/examples/logical/README
@@ -0,0 +1,7 @@
+First see ../../README.
+
+In this directory, LogicProps.hs illustrates the basic way to define
+Serial instances of your own types, and hence Testable properties of
+functions over them. Compile or interpret LogicProps.main (SmallCheck is
+the only other module required) for a small selection of self-introducing
+tests.
diff --git a/examples/numeric/NumProps.hs b/examples/numeric/NumProps.hs
new file mode 100644
--- /dev/null
+++ b/examples/numeric/NumProps.hs
@@ -0,0 +1,61 @@
+------------------------------------------
+-- Illustrating numerics in SmallCheck 0.2
+-- Colin Runciman, November 2006.
+------------------------------------------
+
+module NumProps where
+
+import Test.SmallCheck
+
+primes :: [Int]
+primes = sieve [2..]
+  where
+  sieve (p:xs) =
+    p : filter (noFactorIn primes) xs
+  noFactorIn (p:ps) x =
+    p*p > x || x `mod` p > 0 && noFactorIn ps x
+
+-- using natural numbers
+
+prop_primes1 :: Nat -> Property
+prop_primes1 (N n) =
+  n > 1 ==> forAll (`take` primes) $ \p ->
+    p `mod` n > 0 || n == p
+
+prop_primes2 :: Nat -> Property
+prop_primes2 (N n) =
+  n > 0 ==> exists $ \exponents ->
+    n == product (zipWith power primes exponents)
+  where
+  power p (N e) = product (replicate e p)
+
+-- using floating point numbers
+
+prop_logExp :: Float -> Bool
+prop_logExp x = exp (log x) == x
+
+prop_recipRecip :: Float -> Bool
+prop_recipRecip x = 1.0 / (1.0 / x) == x
+
+main :: IO ()
+main = do
+  test1 "\\(N n) -> n > 1 ==> forAll (`take` primes) $ \\p ->\n\
+        \  p `mod` n > 0 || n == p"
+        prop_primes1
+  test1 "\\(N n) -> n > 0 ==> exists $ \\exponents ->\n\
+        \  n == product (zipWith power primes exponents)"
+        prop_primes2
+  test1 "\\x -> exp (log x) == x"
+        prop_logExp
+  test1 "\\x -> 1.0 / (1.0 / x) == x"
+        prop_recipRecip
+
+test1 :: Testable a => String -> a -> IO ()
+test1 s t = do
+  rule
+  putStrLn s
+  rule
+  smallCheck 8 t
+  where
+  rule = putStrLn "----------------------------------------------------"
+
diff --git a/examples/numeric/README b/examples/numeric/README
new file mode 100644
--- /dev/null
+++ b/examples/numeric/README
@@ -0,0 +1,9 @@
+First see ../../README.
+
+In this directory, NumProps.hs illustrates the use of test series
+for natural numbers, either by explicit signatures including Nat (or
+Natural) or by use of the N constructor.  It also illustrates use of
+floating-point series. Compile or interpret NumProps (SmallCheck is
+the only other module required) and run main for a small selection of
+self-introducing tests -- a couple about natural numbers and primes,
+and a couple about floating point numbers.
diff --git a/examples/regular/README b/examples/regular/README
new file mode 100644
--- /dev/null
+++ b/examples/regular/README
@@ -0,0 +1,8 @@
+First see ../../README.
+
+In this directory, Regular.hs illustrates a test involving IO -- writing
+and reading expressions to/from a file.  The use of 'smart constructors'
+in the series definition is necessary for the property to hold, but does
+*not* reduce the number of tests -- rather, there are duplicated tests for
+the same expressions generated in different ways. Compile or interpret
+Regular.main for a self-introducing test.
diff --git a/examples/regular/Regular.hs b/examples/regular/Regular.hs
new file mode 100644
--- /dev/null
+++ b/examples/regular/Regular.hs
@@ -0,0 +1,116 @@
+module Regular where
+
+import Data.Char (isAlpha)
+import Data.List (intersperse)
+import Control.Monad (liftM)
+import Test.SmallCheck
+
+-- A data type of regular expressions.
+
+data RE = Emp
+        | Lam
+        | Sym Char
+	| Alt [RE]
+        | Cat [RE]
+	| Rep RE
+	deriving Eq
+
+isEmp, isLam, isSym, isCat, isAlt, isRep :: RE -> Bool
+isEmp Emp     = True
+isEmp _       = False
+isLam Lam     = True
+isLam _       = False
+isSym (Sym _) = True
+isSym _       = False
+isAlt (Alt _) = True
+isAlt _       = False
+isCat (Cat _) = True
+isCat _       = False
+isRep (Rep _) = True
+isRep _       = False
+
+-- Syms may be used to represent terminals or variables.
+-- Using cat and alt instead of Cat and Alt ensures that:
+-- (1) Cat and Alt arguments are multi-item lists;
+-- (2) items in Cat arguments are not Cats;
+-- (3) items in Alt arguments are not Alts.
+
+cat :: [RE] -> RE
+cat []  = Lam
+cat [x] = x
+cat xs  = Cat (concatMap catList xs)
+  where
+  catList (Cat ys) = ys
+  catList z        = [z]
+
+alt :: [RE] -> RE
+alt []  = Emp
+alt [x] = x
+alt xs  = Alt (concatMap altList xs)
+  where
+  altList (Alt ys) = ys
+  altList z        = [z]
+
+instance Read RE where
+  readsPrec _ s  = [rest s [[[]]]]
+
+rest :: String -> [[[RE]]] -> (RE,String)
+rest ""      (    a:as) = if null as then (a2re a,"")
+                          else wrong
+rest ('+':s) ((c:a):as) = if null c then wrong
+			  else rest s (([]:c:a):as)
+rest ('*':s) ((c:a):as) = case c of
+                          []     -> wrong
+                          (x:xs) -> rest s (((Rep x:xs):a):as)
+rest ('0':s) ((c:a):as) = rest s (((Emp:c):a):as)
+rest ('1':s) ((c:a):as) = rest s (((Lam:c):a):as)
+rest ('(':s) as         = rest s ([[]]:as)
+rest (')':s) (a:as)     = case as of
+                          [] -> wrong
+			  ((c:a'):as') -> rest s (((a2re a:c):a'):as')
+rest (' ':s) as         = rest s as
+rest (v  :s) ((c:a):as) = if isAlpha v then rest s (((Sym v:c):a):as)
+                          else if null as then (a2re (c:a),v:s)
+			  else wrong
+
+a2re :: [[RE]] -> RE
+a2re = alt . reverse . map (cat . reverse)
+
+wrong = error "unreadable RE"
+
+instance Show RE where
+  show Emp      = "0"
+  show Lam      = "1"
+  show (Sym c)  = [c]
+  show (Alt xs) = concat (intersperse "+" (map show xs))
+  show (Cat xs) = concatMap (showBrackIf isAlt) xs
+  show (Rep x)  = showBrackIf (\x -> isCat x || isAlt x) x ++ "*"
+
+showBrackIf p x = ['(' | q] ++ show x ++ [')' | q] where q = p x
+
+instance Serial RE where
+  series = cons0 Emp
+        \/ cons0 Lam
+        \/ cons1 Sym . depth 0
+        \/ cons1 alt
+        \/ cons1 cat
+        \/ cons1 Rep
+
+prop_readShow :: RE -> IO Bool
+prop_readShow re = do
+  writeFile "tmp" (show re)
+  re' <- liftM read (readFile "tmp")
+  return (re'==re)
+
+main = do
+  rule
+  putStrLn "Testing property involving IO.  Always returns True?"
+  putStrLn "do\n\
+           \  writeFile \"tmp\" (show re)\n\
+           \  re' <- liftM read (readFile \"tmp\")\n\
+           \  return (re'==re)"
+  rule
+  smallCheck 4 prop_readShow
+  where
+  rule = putStrLn
+           "----------------------------------------------------"
diff --git a/smallcheck.cabal b/smallcheck.cabal
new file mode 100644
--- /dev/null
+++ b/smallcheck.cabal
@@ -0,0 +1,48 @@
+Name:          smallcheck
+Version:       0.2.1
+License:       BSD3
+License-File:  LICENSE
+Author:        Colin Runciman
+Maintainer:    Colin Runciman <Colin.Runciman@cs.york.ac.uk>
+
+Stability:     Beta
+Category:      Testing
+Synopsis:      Another lightweight testing library in Haskell.
+Description:   SmallCheck is similar to QuickCheck (Claessen and Hughes 2000-) but
+               instead of testing for a sample of randomly generated values, SmallCheck
+               tests properties for all the finitely many values up to some depth,
+               progressively increasing the depth used.
+               .
+               Folk-law: if there is any case in which a program
+               fails, there is almost always a simple one.
+               .
+               Corollary: if a program does not fail in any
+               simple case, it almost never fails.
+               .
+               Other possible sales pitches:
+               .
+               * write test generators for your own types more easily
+               .
+               * be sure any counter-examples found are minimal
+               .
+               * write properties using existentials as well as universals
+               .
+               * establish complete coverage of a defined test-space
+               .
+               * display counter-examples of functional type
+Homepage:      http://www.cs.york.ac.uk/fp/smallcheck0.2.tar
+
+Build-Depends: base
+Build-Type:    Simple
+
+Extra-source-files: examples/numeric/NumProps.hs, examples/logical/LogicProps.hs,
+                    examples/imperative/Interpreter.hs, examples/imperative/Syntax.hs,
+                    examples/imperative/Machine.hs, examples/imperative/Behaviour.hs,
+                    examples/imperative/Properties.hs, examples/imperative/Value.hs,
+                    examples/imperative/StackMap.hs, examples/imperative/Compiler.hs,
+                    examples/listy/ListProps.hs, examples/regular/Regular.hs
+
+Data-files:         examples/numeric/README, examples/logical/README, examples/imperative/README,
+                    examples/listy/README, examples/regular/README, README
+
+Exposed-modules:    Test.SmallCheck