diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2009-2012, Nick Smallbone
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Nick Smallbone nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,1 @@
+cabal install and look at the examples directory.
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/QuickSpec.hs b/Test/QuickSpec.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec.hs
@@ -0,0 +1,87 @@
+-- | The main QuickSpec module.
+--
+-- This will not make sense if you haven't seen some examples!
+-- Look at <http://github.com/nick8325/quickspec/tree/master/examples>,
+-- or read the paper at <http://www.cse.chalmers.se/~nicsma/quickspec.pdf>.
+
+module Test.QuickSpec
+  (-- * Running QuickSpec
+   quickSpec,
+   sampleTerms,
+
+   -- * The Signature class
+   Sig,
+   Signature(..),
+   -- * Adding functions to a signature
+   --
+   -- | You can add @f@ to the signature by using @\"f\" \`funN\` f@,
+   -- where @N@ is the arity of the function. For example,
+   -- 
+   -- > "&&" `fun2` (&&)
+   --
+   -- will add the binary function @(`&&`)@ to the signature.
+   --
+   -- If f is polymorphic, you must explicitly give it a monomorphic type.
+   -- This module exports types `A`, `B` and `C` for that purpose.
+   -- 
+   -- For example:
+   --
+   -- > "++" `fun2` ((++) :: [A] -> [A] -> [A])
+   --
+   -- The result type of the function must be a member of `Ord`.
+   -- If it isn't, use the `blindN` family of functions (below) instead.
+   -- If you want to get equations over a type that isn't in `Ord`,
+   -- you must use the `observerN` family of functions (below)
+   -- to define an observation function for that type.
+   con, fun0, fun1, fun2, fun3, fun4,
+   -- * Adding functions whose results are not in `Ord`
+   --
+   -- | These functions work the same as `funN` (above),
+   --   but don't use `Ord` to compare the results of the functions.
+   --   Instead you can use the `observerN` family of functions (below)
+   --   to define an observation function.
+   blind0, blind1, blind2, blind3, blind4,
+   -- * Adding variables to a signature
+   vars,
+   gvars,
+   -- * Observational equality
+   --
+   -- | Use this to define comparison operators for types that have
+   --   no `Ord` instance.
+   --
+   -- For example, suppose we have a type @Regex@ of regular expressions,
+   -- and a matching function @match :: String -> Regex -> Bool@.
+   -- We want our equations to talk about semantic equality of regular
+   -- expressions, but we probably won't have an `Ord` instance that does that.
+   -- Instead, we can use @blindN@ to add the regular expression operators
+   -- to the signature, and then write
+   --
+   -- > observer2 match
+   --
+   -- (the @2@ is because @match@ has arity two).
+   -- Then, when QuickSpec wants to compare two @Regex@es, @r1@ and @r2@, it will generate a random
+   -- `String` @xs@, and compare @match xs r1@ with @match xs r2@.
+   --
+   -- Thus you can use `observerN` to get laws about things that can't
+   -- be directly compared for equality but can be tested.
+   observer1, observer2, observer3, observer4,
+   -- * Modifying a signature
+   background,
+   withDepth,
+   withTests,
+   without,
+
+   -- * The standard QuickSpec prelude, to include in your own signatures
+   A, B, C,
+   Two,
+   prelude,
+   bools,
+   arith,
+   lists,
+   funs)
+
+where
+
+import Test.QuickSpec.Main
+import Test.QuickSpec.Signature
+import Test.QuickSpec.Prelude
diff --git a/Test/QuickSpec/Approximate.hs b/Test/QuickSpec/Approximate.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Approximate.hs
@@ -0,0 +1,63 @@
+-- Utilities for testing functions that return partial results.
+{-# LANGUAGE Rank2Types #-}
+module Test.QuickSpec.Approximate where
+
+import Test.QuickCheck
+import Test.QuickCheck.Gen
+import Test.QuickSpec.Signature
+import Test.QuickSpec.Utils
+import Test.QuickSpec.Utils.Typeable
+import Control.Monad
+import Control.Monad.Reader
+import Control.Spoon
+import System.Random
+import Data.Monoid
+
+newtype Plug = Plug { unPlug :: forall a. Partial a => Gen a -> Gen a }
+type GP = ReaderT Plug Gen
+
+plug :: Partial a => GP a -> GP a
+plug x = ReaderT (\plug -> unPlug plug (runReaderT x plug))
+
+class (Typeable a, Arbitrary a, Eq a) => Partial a where
+  unlifted :: a -> GP a
+  unlifted x = return x
+
+lifted :: Partial a => a -> GP a
+lifted x = plug (unlifted x)
+
+instance Partial ()
+instance Partial Int
+instance Partial Integer
+instance Partial Bool
+
+instance Partial a => Partial [a] where
+  unlifted [] = return []
+  unlifted (x:xs) = liftM2 (:) (lifted x) (lifted xs)
+
+approximate :: Partial a => (StdGen, Int) -> a -> a
+approximate (g, n) x = unGen (runReaderT (lifted x) (Plug plug)) g n
+  where
+    plug :: forall a. Partial a => Gen a -> Gen a
+    plug x =
+      sized $ \m ->
+        if m == 0 then return (unGen arbitrary g n)
+        else resize (m-1) $ do
+          y <- x
+          case spoony y of
+            Just z -> return z
+            Nothing -> return (unGen arbitrary g n)
+
+pobserver :: (Ord a, Partial a) => a -> Sig
+pobserver x = observerSig (Observer (MkGen f))
+  where f g n y = approximate (g, n `max` 50) (y `asTypeOf` x)
+
+genPartial :: Partial a => a -> Gen a
+genPartial x = runReaderT (lifted x) (Plug plug)
+  where
+    plug x = frequency [(1, undefined), (3, x)]
+
+pvars :: (Ord a, Partial a) => [String] -> a -> Sig
+pvars xs w = 
+  pobserver w
+  `mappend` gvars xs ((arbitrary `asTypeOf` return w) >>= genPartial)
diff --git a/Test/QuickSpec/Equation.hs b/Test/QuickSpec/Equation.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Equation.hs
@@ -0,0 +1,23 @@
+-- | Equations.
+
+module Test.QuickSpec.Equation where
+
+import Test.QuickSpec.Term
+import Test.QuickSpec.Signature hiding (vars)
+import Test.QuickSpec.Utils.Typed
+import Data.Monoid
+import Data.List
+
+data Equation = Term :=: Term deriving (Eq, Ord)
+
+showEquation :: Sig -> Equation -> String
+showEquation sig (t :=: u) =
+  show (f t) ++ " == " ++ show (f u)
+  where f = disambiguate sig (vars t ++ vars u)
+
+instance Show Equation where
+  show = showEquation mempty
+
+equations :: [[Tagged Term]] -> [Equation]
+equations = sort . concatMap (toEquations . map erase)
+  where toEquations (x:xs) = [y :=: x | y <- xs]
diff --git a/Test/QuickSpec/Generate.hs b/Test/QuickSpec/Generate.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Generate.hs
@@ -0,0 +1,88 @@
+-- | The testing loop and term generation of QuickSpec.
+
+{-# LANGUAGE Rank2Types, TypeOperators, ScopedTypeVariables #-}
+module Test.QuickSpec.Generate where
+
+import Test.QuickSpec.Signature hiding (con)
+import qualified Test.QuickSpec.TestTree as T
+import Test.QuickSpec.TestTree(TestResults, reps, classes, numTests, cutOff, discrete)
+import Test.QuickSpec.Utils.Typed
+import Test.QuickSpec.Utils.TypeRel(TypeRel)
+import qualified Test.QuickSpec.Utils.TypeRel as TypeRel
+import Test.QuickSpec.Utils.TypeMap(TypeMap)
+import qualified Test.QuickSpec.Utils.TypeMap as TypeMap
+import Test.QuickSpec.Term
+import Text.Printf
+import Test.QuickSpec.Utils.Typeable
+import Test.QuickSpec.Utils
+import Test.QuickCheck.Gen
+import System.Random
+import Control.Spoon
+import Test.QuickSpec.Utils.MemoValuation
+
+terms :: Sig -> TypeRel Expr -> TypeRel Expr
+terms sig base =
+  TypeMap.fromList
+    [ Some (O (terms' sig base w))
+    | Some (Witness w) <- usort (saturatedTypes sig ++ variableTypes sig) ]
+
+terms' :: Typeable a => Sig -> TypeRel Expr -> a -> [Expr a]
+terms' sig base w =
+  map var (TypeRel.lookup w (variables sig)) ++
+  map con (TypeRel.lookup w (constants sig)) ++
+  [ app f x
+  | Some (Witness w') <- lhsWitnesses sig w,
+    x <- TypeRel.lookup w' base,
+    not (isUndefined (term x)),
+    f <- terms' sig base (const w),
+    arity f > 0,
+    not (isUndefined (term f)) ]
+
+test :: [(StdGen, Int)] -> Sig ->
+        TypeMap (List `O` Expr) -> TypeMap (TestResults `O` Expr)
+test seeds sig ts = fmap (mapSome2 (test' seeds sig)) ts
+
+test' :: forall a. Typeable a => [(StdGen, Int)] -> Sig -> [Expr a] -> TestResults (Expr a)
+test' seeds sig ts
+  | not (testable sig (undefined :: a)) = discrete ts
+  | otherwise =
+    case observe undefined sig of
+      Observer obs ->
+        let testCase (g, n) =
+              let (g1, g2) = split g
+                  val = memoValuation sig (unGen valuation g1 n) in
+              \x -> spoony . unGen obs g2 n $ eval x val
+        in cutOff base increment (T.test (map testCase seeds) ts)
+  where
+    base = minTests sig `div` 2
+    increment = minTests sig - base
+
+genSeeds :: IO [(StdGen, Int)]
+genSeeds = do
+  rnd <- newStdGen
+  let rnds rnd = rnd1 : rnds rnd2 where (rnd1, rnd2) = split rnd
+  return (zip (rnds rnd) (concat (repeat [0,2..100])))
+
+generate :: Sig -> IO (TypeMap (TestResults `O` Expr))
+generate sig | maxDepth sig < 0 =
+  error "Test.QuickSpec.Generate.generate: maxDepth must be positive"
+generate sig | maxDepth sig == 0 = return TypeMap.empty
+generate sig = unbuffered $ do
+  let d = maxDepth sig
+  rs <- fmap (TypeMap.mapValues2 reps) (generate (updateDepth (d-1) sig))
+  printf "Depth %d: " d
+  let count :: ([a] -> a) -> (forall b. f (g b) -> a) ->
+               TypeMap (f `O` g) -> a
+      count op f = op . map (some2 f) . TypeMap.toList
+      ts = terms sig rs
+  printf "%d terms, " (count sum length ts)
+  seeds <- genSeeds
+  let cs = test seeds sig ts
+  printf "%d tests, %d classes, %d raw equations.\n"
+      (count (maximum . (0:)) numTests cs)
+      (count sum (length . classes) cs)
+      (count sum (sum . map (subtract 1 . length) . classes) cs)
+  return cs
+
+eraseClasses :: TypeMap (TestResults `O` Expr) -> [[Tagged Term]]
+eraseClasses = concatMap (some (map (map (tagged term)) . classes . unO)) . TypeMap.toList
diff --git a/Test/QuickSpec/Main.hs b/Test/QuickSpec/Main.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Main.hs
@@ -0,0 +1,138 @@
+-- | The main implementation of QuickSpec.
+
+{-# LANGUAGE TypeOperators #-}
+module Test.QuickSpec.Main where
+
+import Test.QuickSpec.Generate
+import Test.QuickSpec.Reasoning.NaiveEquationalReasoning hiding (universe, maxDepth)
+import Test.QuickSpec.Utils.Typed
+import qualified Test.QuickSpec.Utils.TypeMap as TypeMap
+import Test.QuickSpec.Signature hiding (vars)
+import Test.QuickSpec.Term
+import Control.Monad
+import Text.Printf
+import Data.Monoid
+import Test.QuickSpec.TestTree(TestResults, classes, reps)
+import Data.List
+import System.Random
+import Data.Monoid
+import Data.Maybe
+import Test.QuickSpec.Utils
+import Test.QuickSpec.Equation
+
+undefinedsSig :: Sig -> Sig
+undefinedsSig sig =
+  background
+    [ undefinedSig "undefined" (undefined `asTypeOf` witness x)
+    | Some x <- saturatedTypes sig ]
+
+universe :: [[Tagged Term]] -> [Tagged Term]
+universe css = filter (not . isUndefined . erase) (concat css)
+
+prune :: Int -> [Tagged Term] -> [Term] -> [Equation] -> [Equation]
+prune d univ reps eqs = evalEQ (initial d univ) (filterM (fmap not . provable) eqs)
+  where
+    provable (t :=: u) = do
+      res <- t =?= u
+      if res then return True else do
+        state <- get
+        -- Check that we won't unify two representatives---if we do
+        -- the equation is false
+        t =:= u
+        reps' <- mapM rep reps
+        if sort reps' == usort reps' then return False else do
+          put state
+          return True
+
+defines :: Equation -> Maybe Symbol
+defines (t :=: u) = do
+  let isVar Var{} = True
+      isVar _ = False
+
+      acyclic t =
+        all acyclic (args t) &&
+        case functor t == functor u of
+          True -> usort (map Var (vars t)) `isProperSubsetOf` args u
+          False -> True
+      xs `isProperSubsetOf` ys = xs `isSubsetOf` ys && sort xs /= sort ys
+      xs `isSubsetOf` ys = sort xs `isSublistOf` sort ys
+      [] `isSublistOf` _ = True
+      (x:xs) `isSublistOf` [] = False
+      (x:xs) `isSublistOf` (y:ys)
+        | x == y = xs `isSublistOf` ys
+        | otherwise = (x:xs) `isSublistOf` ys
+
+  guard (all isVar (args u) && usort (args u) == args u &&
+         acyclic t && vars t `isSubsetOf` vars u)
+
+  return (functor u)
+
+definitions :: [Equation] -> [Equation]
+definitions es = [ e | e <- es, defines e /= Nothing ]
+
+runTool :: Signature a => (Sig -> IO ()) -> a -> IO ()
+runTool tool sig_ = do
+  putStrLn "== API =="
+  putStr (show (signature sig_))
+  let sig = signature sig_ `mappend` undefinedsSig (signature sig_)
+
+  tool sig
+
+-- | Run QuickSpec on a signature.
+quickSpec :: Signature a => a -> IO ()
+quickSpec = runTool $ \sig -> do
+  putStrLn "== Testing =="
+  r <- generate sig
+  let clss = eraseClasses r
+      reps = map (erase . head) clss
+      eqs = equations clss
+      univ = universe clss
+  printf "%d raw equations; %d terms in universe.\n\n"
+    (length eqs)
+    (length univ)
+
+  let pruned = filter (not . all silent . eqnFuns)
+                 (prune (maxDepth sig) univ reps eqs)
+      eqnFuns (t :=: u) = funs t ++ funs u
+      isGround (t :=: u) = null (vars t) && null (vars u)
+      (ground, nonground) = partition isGround pruned
+  putStrLn "== Ground equations =="
+  forM_ (zip [1 :: Int ..] ground) $ \(i, eq) ->
+    printf "%3d: %s\n" i (showEquation sig eq)
+  putStrLn ""
+
+  putStrLn "== Non-ground equations =="
+  forM_ (zip [length ground + 1 ..] nonground) $ \(i, eq) ->
+    printf "%3d: %s\n" i (showEquation sig eq)
+  putStrLn ""
+
+sampleList :: StdGen -> Int -> [a] -> [a]
+sampleList g n xs | n >= length xs = xs
+                  | otherwise = aux g n (length xs) xs
+  where
+    aux g 0 _ _ = []
+    aux g _ _ [] =
+      error "Test.QuickSpec.Main.sampleList: bug in sampling"
+    aux g size len (x:xs)
+      | i <= size = x:aux g' (size-1) (len-1) xs
+      | otherwise = aux g' size (len-1) xs
+      where (i, g') = randomR (1, len) g
+
+-- | Generate random terms from a signature. Useful when QuickSpec is
+--   generating too many terms and you want to know what they look like.
+sampleTerms :: Signature a => a -> IO ()
+sampleTerms = runTool $ \sig -> do
+  putStrLn "== Testing =="
+  r <- generate (updateDepth (maxDepth sig - 1) sig)
+  let univ = sort . concatMap (some2 (map term)) . TypeMap.toList . terms sig .
+             TypeMap.mapValues2 reps $ r
+  printf "Universe contains %d terms.\n\n" (length univ)
+
+  let numTerms = 100
+
+  printf "== Here are %d terms out of a total of %d ==\n" numTerms (length univ)
+  g <- newStdGen
+  forM_ (zip [1 :: Int ..] (sampleList g numTerms univ)) $ \(i, t) ->
+    printf "%d: %s\n" i (show (disambiguate sig (vars t) t))
+
+  putStrLn ""
diff --git a/Test/QuickSpec/Prelude.hs b/Test/QuickSpec/Prelude.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Prelude.hs
@@ -0,0 +1,89 @@
+-- | The \"prelude\": a standard signature containing useful functions
+--   like '++', which can be used as background theory.
+
+{-# LANGUAGE ScopedTypeVariables, DeriveDataTypeable, GeneralizedNewtypeDeriving #-}
+module Test.QuickSpec.Prelude where
+
+import Test.QuickSpec.Signature
+import Test.QuickCheck
+import Data.Typeable
+
+-- | Just a type.
+--   You can instantiate your polymorphic functions at this type
+--   to include them in a signature.
+newtype A = A Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary)
+newtype B = B Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary)
+newtype C = C Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary)
+
+-- | A type with two elements.
+--   Use this instead of @A@ if testing doesn't work well because
+--   the domain of @A@ is too large.
+data Two = One | Two deriving (Eq, Ord, Typeable)
+
+instance Arbitrary Two where
+  arbitrary = elements [One, Two]
+
+instance CoArbitrary Two where
+  coarbitrary One = variant 0
+  coarbitrary Two = variant (-1)
+
+-- | A signature containing boolean functions:
+-- @(`||`)@, @(`&&`)@, `not`, `True`, `False`.
+bools :: Sig
+bools = background [
+  ["x", "y", "z"] `vars` (undefined :: Bool),
+
+  "||"    `fun2` (||),
+  "&&"    `fun2` (&&),
+  "not"   `fun1` not,
+  "True"  `fun0` True,
+  "False" `fun0` False]
+
+-- | A signature containing arithmetic operations:
+-- @0@, @1@, @(`+`)@, @(`*`)@.
+-- Instantiate it with e.g. @arith (undefined :: `Int`)@.
+arith :: forall a. (Typeable a, Ord a, Num a, Arbitrary a) => a -> Sig
+arith _ = background [
+  ["x", "y", "z"] `vars` (undefined :: a),
+
+  "0" `fun0` (0   :: a),
+  "1" `fun0` (1   :: a),
+  "+" `fun2` ((+) :: a -> a -> a),
+  "*" `fun2` ((*) :: a -> a -> a)]
+
+-- | A signature containing list operations:
+-- @[]@, @(:)@, `head`, `tail`, @(`++`)@.
+-- Instantiate it with e.g. @lists (undefined :: `A`)@.
+lists :: forall a. (Typeable a, Ord a, Arbitrary a) => a -> Sig
+lists _ = background [
+  ["xs", "ys", "zs"] `vars` (undefined :: [a]),
+
+  "[]"      `fun0` ([]      :: [a]),
+  ":"       `fun2` ((:)     :: a -> [a] -> [a]),
+  "head"    `fun1` (head    :: [a] -> a),
+  "tail"    `fun1` (tail    :: [a] -> [a]),
+  "++"      `fun2` ((++)    :: [a] -> [a] -> [a])]
+
+-- | A signature containing higher-order functions:
+-- @(`.`)@, `id`, and some function variables.
+-- Useful for testing `map`.
+funs :: forall a. (Typeable a, Ord a, Arbitrary a, CoArbitrary a) => a -> Sig
+funs _ = background [
+  ["f", "g", "h"] `vars` (undefined :: a -> a),
+
+  "."  `blind2` ((.) :: (a -> a) -> (a -> a) -> (a -> a)),
+  "id" `blind0` (id  :: a -> a),
+
+  observer2 (\(x :: a) (f :: a -> a) -> f x)
+  ]
+
+-- | The QuickSpec prelude.
+-- Contains boolean, arithmetic and list functions,
+-- and some variables.
+-- Instantiate it as e.g. @prelude (undefined :: `A`)@.
+prelude :: (Typeable a, Ord a, Arbitrary a) => a -> Sig
+prelude a = background [
+  ["x", "y", "z"] `vars` a,
+  bools,
+  arith (undefined :: Int),
+  lists a ]
diff --git a/Test/QuickSpec/Reasoning/CongruenceClosure.hs b/Test/QuickSpec/Reasoning/CongruenceClosure.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Reasoning/CongruenceClosure.hs
@@ -0,0 +1,167 @@
+-- | A decision procedure for ground equality,
+--   based on the paper "Proof-producing Congruence Closure".
+
+module Test.QuickSpec.Reasoning.CongruenceClosure(CC, newSym, (=:=), (=?=), rep, evalCC, execCC, runCC, ($$), S, funUse, argUse, lookup, initial, frozen) where
+
+import Prelude hiding (lookup)
+import Control.Monad
+import Control.Monad.Trans.State.Strict
+import Data.IntMap(IntMap)
+import qualified Data.IntMap as IntMap
+import Test.QuickSpec.Reasoning.UnionFind(UF, Replacement((:>)))
+import qualified Test.QuickSpec.Reasoning.UnionFind as UF
+import Data.Maybe
+import Data.List(foldl')
+-- import Test.QuickCheck
+-- import Test.QuickCheck.Arbitrary
+-- import Test.QuickCheck.Monadic
+import Text.Printf
+
+lookup2 :: Int -> Int -> IntMap (IntMap a) -> Maybe a
+lookup2 k1 k2 m = IntMap.lookup k2 (IntMap.findWithDefault IntMap.empty k1 m)
+
+insert2 :: Int -> Int -> a -> IntMap (IntMap a) -> IntMap (IntMap a)
+insert2 k1 k2 v m = IntMap.insertWith IntMap.union k1 (IntMap.singleton k2 v) m
+
+delete2 :: Int -> Int -> IntMap (IntMap a) -> IntMap (IntMap a)
+delete2 k1 k2 m = IntMap.adjust (IntMap.delete k2) k1 m
+
+data FlatEqn = (Int, Int) := Int deriving (Eq, Ord)
+
+data S = S {
+      -- in all these maps, the keys are representatives, the values may not be
+      funUse :: !(IntMap [(Int, Int)]),
+      argUse :: !(IntMap [(Int, Int)]),
+      lookup :: IntMap (IntMap Int),
+      uf :: UF.S
+    }
+
+type CC = State S
+
+liftUF :: UF a -> CC a
+liftUF m = do
+  s <- get
+  let (x, uf') = UF.runUF (uf s) m
+  put s { uf = uf' }
+  return x
+
+invariant :: String -> CC ()
+invariant _ = return ()
+-- invariant str = do
+--   S funUse argUse lookup <- get
+--   -- keys of all maps are representatives
+--   let check phase x = do
+--        b <- liftUF (UF.isRep x)
+--        if b then return () else error (printf "%s, %s appears as a key in %s but is not a rep in:\nfunUse=%s\nargUse=%s\nlookup=%s" str (show x) phase (show funUse) (show argUse) (show lookup))
+--   mapM_ (check "funUse") (IntMap.keys funUse)
+--   mapM_ (check "argUse") (IntMap.keys argUse)
+--   mapM_ (check "lookup") (IntMap.keys lookup)
+--   mapM_ (mapM_ (check "inner lookup") . IntMap.keys) (IntMap.elems lookup)
+
+modifyFunUse f = modify (\s -> s { funUse = f (funUse s) })
+modifyArgUse f = modify (\s -> s { argUse = f (argUse s) })
+addFunUses xs s = modifyFunUse (IntMap.insertWith (++) s xs)
+addArgUses xs s = modifyArgUse (IntMap.insertWith (++) s xs)
+modifyLookup f = modify (\s -> s { lookup = f (lookup s) })
+putLookup l = modifyLookup (const l)
+
+newSym :: CC Int
+newSym = liftUF UF.newSym
+
+($$) :: Int -> Int -> CC Int
+f $$ x = do
+  invariant (printf "before %s$$%s" (show f) (show x))
+  m <- gets lookup
+  f' <- rep f
+  x' <- rep x
+  invariant (printf "at %s$$%s:1" (show f) (show x))
+  case lookup2 x' f' m of
+    Nothing -> do
+      c <- newSym
+      invariant (printf "at %s$$%s:2" (show f) (show x))
+      putLookup (insert2 x' f' c m)
+      addFunUses [(x', c)] f'
+      addArgUses [(f', c)] x'
+      invariant (printf "after %s$$%s" (show f) (show x))
+      return c
+    Just k -> return k
+
+(=:=) :: Int -> Int -> CC Bool
+a =:= b = propagate (a, b)
+
+(=?=) :: Int -> Int -> CC Bool
+t =?= u = liftM2 (==) (rep t) (rep u)
+
+propagate (a, b) = do
+  (unified, pending) <- propagate1 (a, b)
+  mapM_ propagate pending
+  return unified
+
+propagate1 (a, b) = do
+  invariant (printf "before propagate (%s, %s)" (show a) (show b))
+  res <- liftUF (a UF.=:= b)
+  case res of
+    Nothing -> return (False, [])
+    Just (r :> r') -> do
+      funUses <- gets (IntMap.lookup r . funUse)
+      argUses <- gets (IntMap.lookup r . argUse)
+      case (funUses, argUses) of
+        (Nothing, Nothing) -> return (True, [])
+        _ -> fmap (\x -> (True, x)) (updateUses r r' (fromMaybe [] funUses) (fromMaybe [] argUses))
+
+updateUses r r' funUses argUses = do
+  modifyFunUse (IntMap.delete r)
+  modifyArgUse (IntMap.delete r)
+  modifyLookup (IntMap.delete r)
+  forM_ funUses $ \(x, _) -> do
+    x' <- rep x
+    modifyLookup (delete2 x' r)
+  invariant (printf "after deleting %s" (show r))
+  let repPair (x, c) = do
+        x' <- rep x
+        return (x', c)
+  funUses' <- mapM repPair funUses
+  argUses' <- mapM repPair argUses
+
+  m <- gets lookup
+
+  let foldUses insert lookup pending m uses = foldl' op e uses
+        where op (pending, newUses, m) (x', c) =
+                case lookup x' m of
+                  Just k -> ((c, k):pending, newUses, m)
+                  Nothing -> (pending, (x', c):newUses, insert x' c m)
+              e = (pending, [], m)
+
+      (funPending, funNewUses, m') = foldUses (\x' c m -> insert2 x' r' c m)
+                                              (\x' m -> lookup2 x' r' m)
+                                              [] m funUses'
+
+      (pending, argNewUses, argM) = foldUses IntMap.insert IntMap.lookup funPending
+                                             (IntMap.findWithDefault IntMap.empty r' m')
+                                             argUses'
+
+  addFunUses funNewUses r'
+  addArgUses argNewUses r'
+
+  putLookup (if IntMap.null argM then m' else IntMap.insert r' argM m')
+  invariant (printf "after updateUses (%s, %s)" (show r) (show r'))
+
+  return pending
+
+rep :: Int -> CC Int
+rep s = liftUF (UF.rep s)
+
+runCC :: S -> CC a -> (a, S)
+runCC s m = runState m s
+
+evalCC :: S -> CC a -> a
+evalCC s m = fst (runCC s m)
+
+execCC :: S -> CC a -> S
+execCC s m = snd (runCC s m)
+
+initial :: Int -> S
+initial n = S IntMap.empty IntMap.empty IntMap.empty (UF.initial n)
+
+frozen :: CC a -> CC a
+frozen x = fmap (evalState x) get
diff --git a/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs b/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Reasoning/NaiveEquationalReasoning.hs
@@ -0,0 +1,123 @@
+-- | Equational reasoning built on top of congruence closure.
+
+{-# LANGUAGE TupleSections #-}
+module Test.QuickSpec.Reasoning.NaiveEquationalReasoning where
+
+import Test.QuickSpec.Term
+import Test.QuickSpec.Equation
+import Test.QuickSpec.Reasoning.CongruenceClosure(CC)
+import qualified Test.QuickSpec.Reasoning.CongruenceClosure as CC
+import Data.Map(Map)
+import qualified Data.Map as Map
+import Data.IntMap(IntMap)
+import qualified Data.IntMap as IntMap
+import Control.Monad
+import Control.Monad.Trans.Reader
+import Control.Monad.Trans.State.Strict
+import qualified Control.Monad.Trans.State.Strict as S
+import Test.QuickSpec.Utils
+import Test.QuickSpec.Utils.Typed
+import Test.QuickSpec.Utils.Typeable
+import Data.Ord
+import Data.List
+
+data Context = Context {
+  rel :: CC.S,
+  universe :: Map TypeRep Universe,
+  maxDepth :: Int
+  }
+
+type Universe = IntMap [Int]
+
+type EQ = ReaderT (Map TypeRep Universe, Int) CC
+
+initial :: Int -> [Tagged Term] -> Context
+initial d ts =
+  let n = 1+maximum (0:concatMap (map index . symbols . erase) ts)
+      (universe, rel) =
+        CC.runCC (CC.initial n) $
+          forM (partitionBy (witnessType . tag) ts) $ \xs@(x:_) ->
+            fmap (witnessType (tag x),) (createUniverse (map erase xs))
+
+  in Context rel (Map.fromList universe) d
+
+createUniverse :: [Term] -> CC Universe
+createUniverse ts = fmap IntMap.fromList (mapM createTerms tss)
+  where tss = partitionBy depth ts
+        createTerms ts@(t:_) = fmap (depth t,) (mapM flatten ts)
+
+runEQ :: Context -> EQ a -> (a, Context)
+runEQ ctx x = (y, ctx { rel = rel' })
+  where (y, rel') = runState (runReaderT x (universe ctx, maxDepth ctx)) (rel ctx)
+
+evalEQ :: Context -> EQ a -> a
+evalEQ ctx x = fst (runEQ ctx x)
+
+execEQ :: Context -> EQ a -> Context
+execEQ ctx x = snd (runEQ ctx x)
+
+liftCC :: CC a -> EQ a
+liftCC x = ReaderT (const x)
+
+(=?=) :: Term -> Term -> EQ Bool
+t =?= u = liftCC $ do
+  x <- flatten t
+  y <- flatten u
+  x CC.=?= y
+
+unifiable :: Equation -> EQ Bool
+unifiable (t :=: u) = t =?= u
+
+(=:=) :: Term -> Term -> EQ Bool
+t =:= u = do
+  (ctx, d) <- ask
+  b <- t =?= u
+  unless b $
+    forM_ (substs t ctx d ++ substs u ctx d) $ \s -> liftCC $ do
+      t' <- subst s t
+      u' <- subst s u
+      t' CC.=:= u'
+  return b
+
+unify :: Equation -> EQ Bool
+unify (t :=: u) = t =:= u
+
+type Subst = Symbol -> Int
+
+substs :: Term -> Map TypeRep Universe -> Int -> [Subst]
+substs t univ d = map lookup (sequence (map choose vars))
+  where vars = map (maximumBy (comparing snd)) .
+               partitionBy fst .
+               holes $ t
+
+        choose (x, n) =
+          let m = Map.findWithDefault
+                  (error "Test.QuickSpec.Reasoning.NaiveEquationalReasoning.substs: empty universe")
+                  (symbolType x) univ in
+          [ (x, t)
+          | d' <- [0..d-n],
+            t <- IntMap.findWithDefault [] d' m ]
+
+        lookup ss =
+          let m = IntMap.fromList [ (index x, y) | (x, y) <- ss ]
+          in \x -> IntMap.findWithDefault (index x) (index x) m
+
+subst :: Subst -> Term -> CC Int
+subst s (Var x) = return (s x)
+subst s (Const x) = return (index x)
+subst s (App f x) = do
+  f' <- subst s f
+  x' <- subst s x
+  f' CC.$$ x'
+
+flatten :: Term -> CC Int
+flatten = subst index
+
+get :: EQ CC.S
+get = liftCC S.get
+
+put :: CC.S -> EQ ()
+put x = liftCC (S.put x)
+
+rep :: Term -> EQ Int
+rep x = liftCC (flatten x >>= CC.rep)
diff --git a/Test/QuickSpec/Reasoning/UnionFind.hs b/Test/QuickSpec/Reasoning/UnionFind.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Reasoning/UnionFind.hs
@@ -0,0 +1,64 @@
+-- | A union-find data structure.
+
+module Test.QuickSpec.Reasoning.UnionFind(UF, Replacement((:>)), newSym, (=:=), rep, evalUF, execUF, runUF, S, isRep, initial) where
+
+import Prelude hiding (min)
+import Control.Monad
+import Control.Monad.Trans.State.Strict
+import Data.IntMap(IntMap)
+import qualified Data.IntMap as IntMap
+
+data S = S {
+      links :: IntMap Int,
+      sym :: Int
+    }
+
+type UF = State S
+data Replacement = Int :> Int
+
+runUF :: S -> UF a -> (a, S)
+runUF s m = runState m s
+
+evalUF :: S -> UF a -> a
+evalUF s m = fst (runUF s m)
+
+execUF :: S -> UF a -> S
+execUF s m = snd (runUF s m)
+
+initial :: Int -> S
+initial n = S IntMap.empty n
+
+modifyLinks f = modify (\s -> s { links = f (links s) })
+modifySym f = modify (\s -> s { sym = f (sym s) })
+putLinks l = modifyLinks (const l)
+
+newSym :: UF Int
+newSym = do
+  s <- get
+  modifySym (+1)
+  return (sym s)
+
+(=:=) :: Int -> Int -> UF (Maybe Replacement)
+s =:= t | s == t = return Nothing
+s =:= t = do
+  rs <- rep s
+  rt <- rep t
+  if (rs /= rt) then do
+    modifyLinks (IntMap.insert rs rt)
+    return (Just (rs :> rt))
+   else return Nothing
+
+rep :: Int -> UF Int
+rep t = do
+  m <- fmap links get
+  case IntMap.lookup t m of
+    Nothing -> return t
+    Just t' -> do
+      r <- rep t'
+      when (t' /= r) $ modifyLinks (IntMap.insert t r)
+      return r
+
+isRep :: Int -> UF Bool
+isRep t = do
+  t' <- rep t
+  return (t == t')
diff --git a/Test/QuickSpec/Signature.hs b/Test/QuickSpec/Signature.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Signature.hs
@@ -0,0 +1,453 @@
+-- | Functions for constructing and analysing signatures.
+
+{-# LANGUAGE Rank2Types, ExistentialQuantification, ScopedTypeVariables #-}
+module Test.QuickSpec.Signature where
+
+import Control.Applicative hiding (some)
+import Test.QuickSpec.Utils.Typeable
+import Data.Monoid
+import Test.QuickCheck
+import Test.QuickSpec.Term hiding (var)
+import Test.QuickSpec.Utils.Typed
+import qualified Test.QuickSpec.Utils.TypeMap as TypeMap
+import Test.QuickSpec.Utils.TypeMap(TypeMap)
+import qualified Test.QuickSpec.Utils.TypeRel as TypeRel
+import Test.QuickSpec.Utils.TypeRel(TypeRel)
+import Data.List
+import qualified Data.Map as Map
+import Test.QuickSpec.Utils
+import Data.Maybe
+import Control.Monad
+
+-- | The class of things that can be used as a signature.
+class Signature a where
+  signature :: a -> Sig
+
+instance Signature Sig where
+  signature = id
+
+instance Signature a => Signature [a] where
+  signature = mconcat . map signature
+
+-- | A signature.
+data Sig = Sig {
+  -- Constants, variables and observation functions.
+  constants :: TypeRel Constant,
+  variables :: TypeRel Variable,
+  observers :: TypeMap Observer,
+
+  -- Ord instances, added whenever the 'fun' family of functions is used.
+  ords :: TypeMap Observer,
+
+  -- Witnesses for Typeable. The following types must have witnesses:
+  --  * Any function argument.
+  --  * Any function result.
+  --  * Any partially-applied function type.
+  --  * Any variable type.
+  witnesses :: TypeMap Witnessed,
+
+  -- Depth of terms in the universe.
+  maxDepth_ :: First Int,
+
+  -- Minimum number of tests to run.
+  minTests_ :: First Int
+  }
+
+maxDepth :: Sig -> Int
+maxDepth = fromMaybe 3 . getFirst . maxDepth_
+
+updateDepth :: Int -> Sig -> Sig
+updateDepth n sig = sig { maxDepth_ = First (Just n) }
+
+minTests :: Sig -> Int
+minTests = fromMaybe 500 . getFirst . minTests_
+
+updateMinTests :: Int -> Sig -> Sig
+updateMinTests n sig = sig { minTests_ = First (Just n) }
+
+instance Show Sig where show = unlines . summarise
+
+data Used = Used Witness [Symbol]
+instance Show Used where
+  show (Used w ks) =
+    show w ++ " (used in " ++ intercalate ", " (map show ks) ++ ")"
+
+uses :: Sig -> Witness -> Used
+uses sig w =
+  Used w
+    [ sym (unConstant k)
+    | Some k <- TypeRel.toList (constants sig),
+      w' <- constantArgs sig k,
+      w == w' ]
+
+summarise :: Sig -> [String]
+summarise sig =
+  section ["-- functions --"]
+    (decls (filter (not . silent) allConstants)) ++
+  section ["-- background functions --"]
+    (decls (filter silent allConstants)) ++
+  section ["-- variables --"]
+    (decls allVariables) ++
+  section ["-- the following types are using non-standard equality --"]
+    (map show (Map.keys (observers sig))) ++
+
+  section ["-- WARNING: the following types are uninhabited --"]
+    (usort
+     [ show (uses sig ty)
+     | ty <- argumentTypes sig,
+       ty `notElem` inhabitedTypes sig,
+       ty `notElem` variableTypes sig ]) ++
+
+  section ["-- WARNING: there are no variables of the following types; consider adding some --"]
+    (usort
+     [ show ty
+     | ty <- argumentTypes sig,
+       -- There is a non-variable term of this type and it appears as the
+       -- argument to some function
+       ty `elem` inhabitedTypes sig,
+       ty `notElem` variableTypes sig ]) ++
+  section ["-- WARNING: cannot test the following types; ",
+        "            consider using 'fun' instead of 'blind' or using 'observe' --"]
+    (usort
+     [ show ty
+     | ty@(Some (Witness w)) <- saturatedTypes sig,
+       -- The type is untestable and is the result type of a constant
+       not (testable sig w) ])
+
+  where
+    symbols :: (Sig -> TypeRel f) -> (forall a. f a -> Symbol) -> [Symbol]
+    symbols f erase = map (some erase) (TypeRel.toList (f sig))
+
+    allConstants = symbols constants (sym . unConstant)
+    allVariables = symbols variables (sym . unVariable)
+
+    section _ [] = []
+    section msg xs = msg ++ xs ++ [""]
+
+    decls xs = map decl (partitionBy symbolType xs)
+
+    decl xs@(x:_) =
+      intercalate ", " (map show xs) ++ " :: " ++ show (symbolType x)
+
+data Observer a = forall b. Ord b => Observer (Gen (a -> b))
+
+observe x sig =
+  TypeMap.lookup (TypeMap.lookup (error msg) x (ords sig))
+               x (observers sig)
+  where msg = "Test.QuickSpec.Signature.observe: no observers found for type " ++ show (typeOf x)
+
+emptySig :: Sig
+emptySig = Sig TypeRel.empty TypeRel.empty TypeMap.empty TypeMap.empty TypeMap.empty mempty mempty
+
+instance Monoid Sig where
+  mempty = emptySig
+  s1 `mappend` s2 =
+    Sig {
+      constants = renumber (mapConstant . alter) 0 constants',
+      variables = renumber (mapVariable . alter) (length constants') variables',
+      observers = observers s1 `mappend` observers s2,
+      ords = ords s1 `mappend` ords s2,
+      witnesses = witnesses s1 `mappend` witnesses s2,
+      maxDepth_ = maxDepth_ s1 `mappend` maxDepth_ s2,
+      minTests_ = minTests_ s1 `mappend` minTests_ s2 }
+    where constants' = TypeRel.toList (constants s1) ++
+                       TypeRel.toList (constants s2)
+          -- Overwrite variables if they're declared twice!
+          variables' = TypeRel.toList (variables s1 `combine` variables s2)
+
+          renumber :: (forall a. Int -> f a -> f a) ->
+                      Int -> [Some f] -> TypeRel f
+          renumber alter n =
+            TypeRel.fromList .
+            zipWith (\x -> mapSome (alter x)) [n..]
+
+          alter :: Int -> Symbol -> Symbol
+          alter n x = x { index = n }
+
+          combine :: TypeRel Variable -> TypeRel Variable -> TypeRel Variable
+          -- If a signature uses vars several times at the same type,
+          -- the declaration with the highest number of variables "wins"
+          -- and all others are discarded
+          combine = Map.unionWith max_
+            where max_ vs1 vs2
+                    | some2 length vs1 > some2 length vs2 = vs1
+                    | otherwise = vs2
+
+constantSig :: Typeable a => Constant a -> Sig
+constantSig x = emptySig { constants = TypeRel.singleton x }
+
+variableSig :: forall a. Typeable a => [Variable a] -> Sig
+variableSig x = emptySig { variables = TypeRel.fromList (map Some x) }
+
+observerSig :: forall a. Typeable a => Observer a -> Sig
+observerSig x = emptySig { observers = TypeMap.singleton x }
+
+typeSig :: Typeable a => a -> Sig
+typeSig x = emptySig { witnesses = TypeMap.singleton (Witness x) }
+
+ordSig :: Typeable a => Observer a -> Sig
+ordSig x = emptySig { ords = TypeMap.singleton x }
+
+-- | If @withDepth n@ is in your signature,
+--   QuickSpec will consider terms of up to depth @n@
+--   (the default is 3).
+withDepth :: Int -> Sig
+withDepth n = updateDepth n emptySig
+
+-- | If @withTests n@ is in your signature,
+--   QuickSpec will run at least @n@ tests
+--   (the default is 500).
+withTests :: Int -> Sig
+withTests n = updateMinTests n emptySig
+
+-- | @sig \`without\` xs@ will remove the functions
+--   in @xs@ from the signature @sig@.
+--   Useful when you want to use `Test.QuickSpec.prelude`
+--   but exclude some functions.
+--   Example: @`prelude` (undefined :: A) \`without\` [\"head\", \"tail\"]@.
+without :: Signature a => a -> [String] -> Sig
+without sig xs = sig' { constants = f p (constants sig'), variables = f q (variables sig') }
+  where
+    sig' = signature sig
+    f p = TypeRel.fromList . filter p . TypeRel.toList
+    p (Some (Constant k)) = name (sym k) `notElem` xs
+    q (Some (Variable v)) = name (sym v) `notElem` xs
+
+undefinedSig :: forall a. Typeable a => String -> a -> Sig
+undefinedSig x u = constantSig (Constant (Atom ((symbol x 0 u) { undef = True }) u))
+
+primCon0 :: forall a. Typeable a => Int -> String -> a -> Sig
+primCon0 n x f = constantSig (Constant (Atom (symbol x n f) f))
+                 `mappend` typeSig (undefined :: a)
+
+primCon1 :: forall a b. (Typeable a, Typeable b) =>
+          Int -> String -> (a -> b) -> Sig
+primCon1 n x f = primCon0 n x f
+                 `mappend` typeSig (undefined :: a)
+                 `mappend` typeSig (undefined :: b)
+
+primCon2 :: forall a b c. (Typeable a, Typeable b, Typeable c) =>
+          Int -> String -> (a -> b -> c) -> Sig
+primCon2 n x f = primCon1 n x f
+                 `mappend` typeSig (undefined :: b)
+                 `mappend` typeSig (undefined :: c)
+
+primCon3 :: forall a b c d. (Typeable a, Typeable b, Typeable c, Typeable d) =>
+          Int -> String -> (a -> b -> c -> d) -> Sig
+primCon3 n x f = primCon2 n x f
+                 `mappend` typeSig (undefined :: c)
+                 `mappend` typeSig (undefined :: d)
+
+primCon4 :: forall a b c d e. (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) =>
+          Int -> String -> (a -> b -> c -> d -> e) -> Sig
+primCon4 n x f = primCon3 n x f
+                 `mappend` typeSig (undefined :: d)
+                 `mappend` typeSig (undefined :: e)
+
+-- | A constant.
+blind0 :: forall a. Typeable a => String -> a -> Sig
+blind0 = primCon0 0
+-- | A unary function.
+blind1 :: forall a b. (Typeable a, Typeable b) =>
+          String -> (a -> b) -> Sig
+blind1 = primCon1 1
+-- | A binary function.
+blind2 :: forall a b c. (Typeable a, Typeable b, Typeable c) =>
+          String -> (a -> b -> c) -> Sig
+blind2 = primCon2 2
+-- | A ternary function.
+blind3 :: forall a b c d. (Typeable a, Typeable b, Typeable c, Typeable d) =>
+          String -> (a -> b -> c -> d) -> Sig
+blind3 = primCon3 3
+-- | A function of arity 4.
+blind4 :: forall a b c d e. (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) =>
+          String -> (a -> b -> c -> d -> e) -> Sig
+blind4 = primCon4 4
+
+ord :: (Ord a, Typeable a) => a -> Sig
+ord x = ordSig (Observer (return id) `observing` x)
+
+observing :: Observer a -> a -> Observer a
+observing x _ = x
+
+-- | Mark all the functions in a signature as background functions.
+--
+-- QuickSpec will only print a law if it contains at least one non-background function.
+--
+-- The functions in e.g. `Test.QuickSpec.prelude` are declared as background functions.
+background :: Signature a => a -> Sig
+background sig =
+  sig' { constants = TypeRel.mapValues (mapConstant silence1) (constants sig'),
+         variables = TypeRel.mapValues (mapVariable silence1) (variables sig') }
+  where sig' = signature sig
+        silence1 x = x { silent = True }
+
+-- | Similar to `vars`, but takes a generator as a parameter.
+--
+-- @gvars xs (arbitrary :: Gen a)@ is the same as
+-- @vars xs (undefined :: a)@.
+gvars :: forall a. Typeable a => [String] -> Gen a -> Sig
+gvars xs g = variableSig [ Variable (Atom (symbol x 0 (undefined :: a)) g) | x <- xs ]
+            `mappend` typeSig (undefined :: a)
+
+-- | Declare a set of variables of a particular type.
+--
+-- For example, @vars [\"x\",\"y\",\"z\"] (undefined :: Int)@
+-- defines three variables, @x@, @y@ and @z@, of type `Int`.
+vars :: forall a. (Arbitrary a, Typeable a) => [String] -> a -> Sig
+vars xs _ = gvars xs (arbitrary :: Gen a)
+
+con, fun0 :: (Ord a, Typeable a) => String -> a -> Sig
+-- | A constant. The same as `fun0`.
+con = fun0
+-- | A constant. The same as `con`.
+fun0 x f = blind0 x f
+           `mappend` ord f
+
+-- | A unary function.
+fun1 :: (Typeable a,
+         Typeable b, Ord b) =>
+        String -> (a -> b) -> Sig
+fun1 x f = blind1 x f
+           `mappend` ord (f undefined)
+
+-- | A binary function.
+fun2 :: (Typeable a, Typeable b,
+         Typeable c, Ord c) =>
+        String -> (a -> b -> c) -> Sig
+fun2 x f = blind2 x f
+           `mappend` ord (f undefined undefined)
+
+-- | A ternary function.
+fun3 :: (Typeable a, Typeable b, Typeable c,
+         Typeable d, Ord d) =>
+        String -> (a -> b -> c -> d) -> Sig
+fun3 x f = blind3 x f
+           `mappend` ord (f undefined undefined undefined)
+
+-- | A function of four arguments.
+fun4 :: (Typeable a, Typeable b, Typeable c, Typeable d,
+         Typeable e, Ord e) =>
+        String -> (a -> b -> c -> d -> e) -> Sig
+fun4 x f = blind4 x f
+           `mappend` ord (f undefined undefined undefined undefined)
+
+-- | An observation function of arity 1.
+observer1 :: (Typeable a, Typeable b, Ord b) => (a -> b) -> Sig
+observer1 f = observerSig (Observer (return f))
+
+-- | An observation function of arity 2.
+observer2 :: (Arbitrary a, Typeable a, Typeable b, Typeable c, Ord c) =>
+             (a -> b -> c) -> Sig
+observer2 f = observerSig (Observer (f <$> arbitrary))
+
+-- | An observation function of arity 3.
+observer3 :: (Arbitrary a, Arbitrary b,
+              Typeable a, Typeable b, Typeable c, Typeable d,
+              Ord d) =>
+             (a -> b -> c -> d) -> Sig
+observer3 f = observerSig (Observer (f <$> arbitrary <*> arbitrary))
+
+-- | An observation function of arity 4.
+observer4 :: (Arbitrary a, Arbitrary b, Arbitrary c,
+              Typeable a, Typeable b, Typeable c, Typeable d, Typeable e,
+              Ord e) =>
+             (a -> b -> c -> d -> e) -> Sig
+observer4 f = observerSig (Observer (f <$> arbitrary <*> arbitrary <*> arbitrary))
+
+testable :: Typeable a => Sig -> a -> Bool
+testable sig x =
+  typeOf x `Map.member` observers sig ||
+  typeOf x `Map.member` ords sig
+
+-- Given a constant, find the types of its partial applications.
+constantApplications :: forall a. Typeable a => Sig -> Constant a -> [Witness]
+constantApplications sig (Constant (Atom {sym = sym })) =
+  map (findWitness sig)
+    (take (symbolArity sym + 1)
+     (iterate rightArrow (typeOf (undefined :: a))))
+
+-- Find the argument types of a constant.
+constantArgs :: forall a. Typeable a => Sig -> Constant a -> [Witness]
+constantArgs sig (Constant (Atom { sym = sym })) =
+  map (findWitness sig)
+    (take (symbolArity sym)
+     (unfoldr splitArrow (typeOf (undefined :: a))))
+
+-- Find the type of a saturated constant.
+constantRes :: forall a. Typeable a => Sig -> Constant a -> Witness
+constantRes sig (Constant (Atom { sym = sym })) =
+  findWitness sig
+    (iterate (snd . fromMaybe (error msg) . splitArrow)
+       (typeOf (undefined :: a)) !! symbolArity sym)
+  where msg = "Test.QuickSpec.Signature.constantRes: type oversaturated"
+
+-- The set of types returned by saturated constants.
+saturatedTypes :: Sig -> [Witness]
+saturatedTypes sig =
+  usort
+    [ constantRes sig k
+    | Some k <- TypeRel.toList (constants sig) ]
+
+-- The set of types of which there is a non-variable term.
+inhabitedTypes :: Sig -> [Witness]
+inhabitedTypes sig =
+  usort . concat $
+    [ constantApplications sig k
+    | Some k <- TypeRel.toList (constants sig) ]
+
+-- The set of types that appear as arguments to functions.
+argumentTypes :: Sig -> [Witness]
+argumentTypes sig =
+  usort . concat $
+    [ constantArgs sig k
+    | Some k <- TypeRel.toList (constants sig) ]
+
+-- The set of types inhabited by variables.
+variableTypes :: Sig -> [Witness]
+variableTypes sig =
+  usort (map someWitness (TypeRel.toList (variables sig)))
+
+-- Given a type, find a witness that it's a function.
+witnessArrow :: Typeable a => Sig -> a -> Maybe (Witness, Witness)
+witnessArrow sig x = do
+  (lhs, rhs) <- splitArrow (typeOf x)
+  liftM2 (,) (lookupWitness sig lhs) (lookupWitness sig rhs)
+
+-- lhsWitnesses sig x is the set of witnessed function types that
+-- might accept x as a parameter. There is no guarantee that
+-- any particular type is inhabited.
+lhsWitnesses :: Typeable a => Sig -> a -> [Witness]
+lhsWitnesses sig x =
+  [ lhs
+  | Some (Witness w) <- TypeMap.toList (witnesses sig),
+    Just (lhs, rhs) <- [witnessArrow sig w],
+    witnessType rhs == typeOf x ]
+
+findWitness :: Sig -> TypeRep -> Witness
+findWitness sig ty =
+  fromMaybe (error "Test.QuickSpec.Signature.findWitness: missing type")
+    (lookupWitness sig ty)
+
+lookupWitness :: Sig -> TypeRep -> Maybe Witness
+lookupWitness sig ty = Map.lookup ty (witnesses sig)
+
+disambiguate :: Sig -> [Symbol] -> Term -> Term
+disambiguate sig ss =
+  mapVars (\x ->
+    fromMaybe (error "Test.QuickSpec.Term.disambiguate: variable not found")
+      (find (\y -> index x == index y)
+        (aux [] (nub ss))))
+  where
+    aux used [] = []
+    aux used (x:xs) = x { name = next }:aux (next:used) xs
+      where next = head (filter (`notElem` used) candidates)
+            candidates
+              | null wellTypedNames = error "Test.QuickSpec.Term.disambiguate: null allVars"
+              | otherwise = wellTypedNames ++ concat [ map (++ show i) wellTypedNames | i <- [1.. ] ]
+            allVars =
+              map (some (sym . unVariable))
+                (TypeRel.toList (variables sig)) ++
+              ss
+            wellTypedNames =
+              [ name v | v <- allVars, symbolType v == symbolType x ]
diff --git a/Test/QuickSpec/Term.hs b/Test/QuickSpec/Term.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Term.hs
@@ -0,0 +1,173 @@
+-- | Terms and evaluation.
+
+{-# LANGUAGE RankNTypes, ExistentialQuantification, DeriveFunctor #-}
+module Test.QuickSpec.Term where
+
+import Test.QuickSpec.Utils.Typeable
+import Test.QuickCheck
+import Data.Function
+import Data.Ord
+import Data.Char
+import Test.QuickSpec.Utils
+
+data Symbol = Symbol {
+  index :: Int,
+  name :: String,
+  symbolArity :: Int,
+  silent :: Bool,
+  undef :: Bool,
+  symbolType :: TypeRep }
+
+symbol :: Typeable a => String -> Int -> a -> Symbol
+symbol x arity v = Symbol 0 x arity False False (typeOf v)
+
+instance Show Symbol where
+  show = showOp . name
+
+instance Eq Symbol where
+  (==) = (==) `on` index
+
+instance Ord Symbol where
+  compare = comparing index
+
+data Term =
+    Var Symbol
+  | Const Symbol
+  | App Term Term deriving Eq
+
+infixl 5 `App`
+
+instance Ord Term where
+  compare = comparing stamp
+    where
+      stamp t = (depth t, size t, -occur t, body t)
+
+      occur t = length (usort (vars t))
+
+      body (Var x) = Left (Left x)
+      body (Const x) = Left (Right x)
+      body (App f x) = Right (f, x)
+
+instance Show Term where
+  showsPrec p t = showString (showTerm p t)
+   where
+     brack s = "(" ++ s ++ ")"
+     parenFun p s | p < 2 = s
+                  | otherwise = brack s
+     parenOp p s | p < 1 = s
+                 | otherwise = brack s
+
+     showTerm p (Var v) = show v
+     showTerm p (Const x) = show x
+     showTerm p (Const op `App` x) | isOp (name op) =
+       brack (showTerm 1 x ++ name op)
+     showTerm p (Const op `App` x `App` y) | isOp (name op) =
+       parenOp p (showTerm 1 x ++ name op ++ showTerm 1 y)
+
+     showTerm p (f `App` x) =
+       parenFun p (showTerm 1 f ++ " " ++ showTerm 2 x)
+
+showOp :: String -> String
+showOp op | isOp op = "(" ++ op ++ ")"
+          | otherwise = op
+
+isOp :: String -> Bool
+isOp "[]" = False
+isOp xs = not (all isIdent xs)
+  where isIdent x = isAlphaNum x || x == '\''
+
+isUndefined :: Term -> Bool
+isUndefined (Const Symbol { undef = True }) = True
+isUndefined _ = False
+
+symbols :: Term -> [Symbol]
+symbols t = symbols' t []
+  where symbols' (Var x) = (x:)
+        symbols' (Const x) = (x:)
+        symbols' (App f x) = symbols' f . symbols' x
+
+depth, size :: Term -> Int
+depth (App f x) = depth f `max` (1 + depth x)
+depth _ = 1
+size (App f x) = size f + size x
+size (Var _) = 0
+size (Const _) = 1
+
+holes :: Term -> [(Symbol, Int)]
+holes t = holes' 0 t []
+  where holes' d (Var x) = ((x, d):)
+        holes' d Const{} = id
+        holes' d (App f x) = holes' d f . holes' (d+1) x
+
+functor :: Term -> Symbol
+functor (Var x) = x
+functor (Const x) = x
+functor (App f x) = functor f
+
+args :: Term -> [Term]
+args = reverse . args'
+  where args' Var{} = []
+        args' Const{} = []
+        args' (App f x) = x:args' f
+
+funs :: Term -> [Symbol]
+funs t = aux t []
+  where aux (Const x) = (x:)
+        aux Var{} = id
+        aux (App f x) = aux f . aux x
+
+vars :: Term -> [Symbol]
+vars t = aux t []
+  where aux (Var x) = (x:)
+        aux (App f x) = aux f . aux x
+        aux Const{} = id
+
+mapVars :: (Symbol -> Symbol) -> Term -> Term
+mapVars f (Var x) = Var (f x)
+mapVars f (Const x) = Const x
+mapVars f (App t u) = App (mapVars f t) (mapVars f u)
+
+data Expr a = Expr {
+  term :: Term,
+  arity :: {-# UNPACK #-} !Int,
+  eval :: (forall b. Variable b -> b) -> a }
+
+instance Eq (Expr a) where
+  (==) = (==) `on` term
+
+instance Ord (Expr a) where
+  compare = comparing term
+
+instance Show (Expr a) where
+  show = show . term
+
+data Atom a = Atom {
+  sym :: Symbol,
+  value :: a } deriving Functor
+
+newtype Variable a = Variable { unVariable :: Atom (Gen a) } deriving Functor
+newtype Constant a = Constant { unConstant :: Atom a } deriving Functor
+
+mapVariable :: (Symbol -> Symbol) -> Variable a -> Variable a
+mapVariable f (Variable v) = Variable v { sym = f (sym v) }
+
+mapConstant :: (Symbol -> Symbol) -> Constant a -> Constant a
+mapConstant f (Constant v) = Constant v { sym = f (sym v) }
+
+-- Generate a random variable valuation
+valuation :: Gen (Variable a -> a)
+valuation = promote (\(Variable x) -> index (sym x) `variant'` value x)
+  where -- work around the fact that split doesn't work
+        variant' 0 = variant (0 :: Int)
+        variant' n = variant (-1 :: Int) . variant' (n-1)
+
+var :: Variable a -> Expr a
+var v@(Variable (Atom x _)) = Expr (Var x) 0 (\env -> env v)
+
+con :: Constant a -> Expr a
+con (Constant (Atom x v)) = Expr (Const x) (symbolArity x) (const v)
+
+app :: Expr (a -> b) -> Expr a -> Expr b
+app (Expr t a f) (Expr u _ x)
+  | a == 0 = error "Test.QuickSpec.Term.app: oversaturated function"
+  | otherwise = Expr (App t u) (a - 1) (\env -> f env (x env))
diff --git a/Test/QuickSpec/TestTree.hs b/Test/QuickSpec/TestTree.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/TestTree.hs
@@ -0,0 +1,98 @@
+-- | A data structure to represent refining a set of terms into
+--   equivalence classes by testing.
+
+module Test.QuickSpec.TestTree(TestTree, terms, union, test,
+               TestResults, cutOff, numTests, classes, reps, discrete) where
+
+import Data.List(sort)
+import Test.QuickSpec.Utils
+import Control.Exception(assert)
+
+-- Invariant: the children of a TestTree are sorted according to the
+-- parent's test. We exploit this in defining merge.
+--
+-- A TestTree is always infinite, and branches t is always a
+-- refinement of t (it may be trivial, so that length (branches t) == 1).
+-- As a special case, a TestTree may be Nil, but Nil may not appear in
+-- the branches of a TestTree.
+data TestTree a = Nil | NonNil (TestTree' a)
+data TestTree' a = Tree { rep :: a, rest :: [a], branches :: [TestTree' a] }
+
+-- Precondition: bs must be sorted according to the TestCase.
+tree :: Ord r => [a] -> (a -> r) -> [TestTree' a] -> TestTree' a
+tree [] _ _ =
+  error "Test.QuickSpec.TestTree.tree: bug: empty equivalence class"
+tree (x:xs) eval bs =
+  assert (isSortedBy (eval . rep) bs) $
+    Tree { rep = x, rest = xs, branches = bs }
+
+terms :: TestTree a -> [a]
+terms Nil = []
+terms (NonNil t) = terms' t
+
+terms' :: TestTree' a -> [a]
+terms' Tree{rep = x, rest = xs} = x:xs
+
+-- Precondition: the sequence of test cases given must be
+-- that used to generate the two TestTrees.
+union :: Ord r => [a -> r] -> TestTree a -> TestTree a -> TestTree a
+union _ Nil t = t
+union _ t Nil = t
+union evals (NonNil t1) (NonNil t2) = NonNil (union' evals t1 t2)
+
+union' :: Ord r => [a -> r] -> TestTree' a -> TestTree' a -> TestTree' a
+union' (eval:evals) t1 t2 =
+  tree (terms' t1 ++ terms' t2) eval
+         (merge (union' evals) (eval . rep) (branches t1) (branches t2))
+
+test :: Ord r => [a -> r] -> [a] -> TestTree a
+test _ [] = Nil
+test tcs xs = NonNil (test' tcs xs)
+
+test' :: Ord r => [a -> r] -> [a] -> TestTree' a
+test' [] _ =
+  error "Test.QuickSpec.TestTree.test': ran out of test cases"
+test' (tc:tcs) xs = tree xs tc (map (test' tcs) bs)
+  where bs = partitionBy tc xs
+
+-- A TestTree with finite depth, represented as a TestTree where some
+-- nodes have no branches. Since this breaks one of the TestTree
+-- invariants we use a different type.
+newtype TestResults a = Results (TestTree a)
+
+discrete :: Ord a => [a] -> TestResults a
+discrete xs =
+  case sort xs of
+    [] -> Results Nil
+    (y:ys) ->
+      Results (NonNil (Tree y ys (map singleton (y:ys))))
+      where singleton x = Tree x [] []
+
+cutOff :: Int -> Int -> TestTree a -> TestResults a
+cutOff _ _ Nil = Results Nil
+cutOff m n (NonNil t) = Results (NonNil (aux m t))
+  where aux 0 t = aux' False n n t
+        aux m t = t { branches = map (aux (m-1)) (branches t) }
+        -- Exponential backoff if we carry on refining a class
+        aux' True 0 n t = t { branches = map (aux' False (n*2-1) (n*2)) (branches t) }
+        aux' False 0 n t = t { branches = [] }
+        aux' x m n t@Tree{branches = [t']} = t { branches = [aux' x (m-1) n t'] }
+        aux' _ m n t = t { branches = map (aux' True (m-1) n) (branches t) }
+
+numTests :: TestResults a -> Int
+numTests (Results Nil) = 0
+numTests (Results (NonNil t)) = aux t
+  where aux Tree{branches = []} = 0
+        aux Tree{branches = bs} = 1 + maximum (map aux bs)
+
+classes :: Ord a => TestResults a -> [[a]]
+classes = sort . map sort . unsortedClasses
+
+unsortedClasses :: TestResults a -> [[a]]
+unsortedClasses (Results Nil) = []
+unsortedClasses (Results (NonNil t)) = aux t
+  where aux Tree{rep = x, rest = xs, branches = []} = [x:xs]
+        aux Tree{branches = bs} = concatMap aux bs
+
+reps :: Ord a => TestResults a -> [a]
+reps = map head . classes
diff --git a/Test/QuickSpec/Utils.hs b/Test/QuickSpec/Utils.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Utils.hs
@@ -0,0 +1,50 @@
+-- | Miscellaneous utility functions.
+
+module Test.QuickSpec.Utils where
+
+import Control.Arrow((&&&))
+import Data.List(groupBy, sortBy, group, sort)
+import Data.Ord(comparing)
+import System.IO
+import Control.Exception
+import Control.Spoon
+
+repeatM :: Monad m => m a -> m [a]
+repeatM = sequence . repeat
+
+partitionBy :: Ord b => (a -> b) -> [a] -> [[a]]
+partitionBy value = map (map fst) . groupBy (\x y -> snd x == snd y) . sortBy (comparing snd) . map (id &&& value)
+
+isSorted :: Ord a => [a] -> Bool
+isSorted xs = and (zipWith (<=) xs (tail xs))
+
+isSortedBy :: Ord b => (a -> b) -> [a] -> Bool
+isSortedBy f xs = isSorted (map f xs)
+
+usort :: Ord a => [a] -> [a]
+usort = map head . group . sort
+
+merge :: Ord b => (a -> a -> a) -> (a -> b) -> [a] -> [a] -> [a]
+merge f c = aux
+  where aux [] ys = ys
+        aux xs [] = xs
+        aux (x:xs) (y:ys) =
+          case comparing c x y of
+            LT -> x:aux xs (y:ys)
+            GT -> y:aux (x:xs) ys
+            EQ -> f x y:aux xs ys
+
+orElse :: Ordering -> Ordering -> Ordering
+EQ `orElse` x = x
+x `orElse` _ = x
+
+unbuffered :: IO a -> IO a
+unbuffered x = do
+  buf <- hGetBuffering stdout
+  bracket_
+    (hSetBuffering stdout NoBuffering)
+    (hSetBuffering stdout buf)
+    x
+
+spoony :: Eq a => a -> Maybe a
+spoony x = teaspoon ((x == x) `seq` x)
diff --git a/Test/QuickSpec/Utils/MemoValuation.hs b/Test/QuickSpec/Utils/MemoValuation.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Utils/MemoValuation.hs
@@ -0,0 +1,22 @@
+-- | Memoise the variable valuation function for terms.
+--   In its own module because it's packed full of dangerous features!
+
+{-# LANGUAGE Rank2Types #-}
+module Test.QuickSpec.Utils.MemoValuation where
+
+import Test.QuickSpec.Term
+import Test.QuickSpec.Signature
+import Data.Array hiding (index)
+import Data.Array.Base(unsafeAt)
+import Unsafe.Coerce
+import GHC.Prim
+import Test.QuickSpec.Utils.Typed
+import Test.QuickSpec.Utils.TypeRel
+
+memoValuation :: Sig -> (forall a. Variable a -> a) -> (forall a. Variable a -> a)
+memoValuation sig f = unsafeCoerce . unsafeAt arr . index . sym . unVariable
+  where arr :: Array Int Any
+        arr = array (0, maximum (0:map (some (index . sym . unVariable)) vars))
+                [(index (sym (unVariable v)), unsafeCoerce (f v))
+                | Some v <- vars ]
+        vars = toList (variables sig)
diff --git a/Test/QuickSpec/Utils/TypeMap.hs b/Test/QuickSpec/Utils/TypeMap.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Utils/TypeMap.hs
@@ -0,0 +1,40 @@
+-- | A map from types to values.
+--   @'TypeMap' f@ maps each type @a@ to a value of type @f a@.
+
+{-# LANGUAGE Rank2Types, TypeOperators #-}
+module Test.QuickSpec.Utils.TypeMap where
+
+import qualified Data.Map as Map
+import Data.Map(Map)
+import Test.QuickSpec.Utils.Typed
+import Test.QuickSpec.Utils.Typeable
+
+type TypeMap f = Map TypeRep (Some f)
+
+empty :: TypeMap f
+empty = fromList []
+
+singleton :: Typeable a => f a -> TypeMap f
+singleton x = fromList [Some x]
+
+fromList :: [Some f] -> TypeMap f
+fromList xs = Map.fromList [ (someType x, x) | x <- xs ]
+
+toList :: TypeMap f -> [Some f]
+toList = Map.elems
+
+lookup :: Typeable a => f a -> a -> TypeMap f -> f a
+lookup def x m =
+  case Map.lookup (typeOf x) m of
+    Nothing -> def
+    Just (Some y) ->
+      case gcast y of
+        Nothing ->
+          error "Test.QuickSpec.Utils.TypeMap.lookup: type error"
+        Just z -> z
+
+mapValues :: (forall a. Typeable a => f a -> g a) -> TypeMap f -> TypeMap g
+mapValues f = fmap (mapSome f)
+
+mapValues2 :: (forall a. Typeable a => f (g a) -> h (i a)) -> TypeMap (f `O` g) -> TypeMap (h `O` i)
+mapValues2 f = fmap (mapSome (O . f . unO))
diff --git a/Test/QuickSpec/Utils/TypeRel.hs b/Test/QuickSpec/Utils/TypeRel.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Utils/TypeRel.hs
@@ -0,0 +1,46 @@
+-- | A relation between types and values.
+--   @'TypeRel' f@ relates each type @a@ to a set of values
+--   of type @f a@.
+
+{-# LANGUAGE Rank2Types, TypeOperators #-}
+module Test.QuickSpec.Utils.TypeRel where
+
+import qualified Test.QuickSpec.Utils.TypeMap as TypeMap
+import Test.QuickSpec.Utils.TypeMap(TypeMap)
+import Test.QuickSpec.Utils.Typed
+import Test.QuickSpec.Utils.Typeable
+import Data.Maybe
+import Test.QuickSpec.Utils
+
+type TypeRel f = TypeMap (List `O` f)
+
+empty :: TypeRel f
+empty = TypeMap.empty
+
+singleton :: Typeable a => f a -> TypeRel f
+singleton x = TypeMap.singleton (O [x])
+
+fromList :: [Some f] -> TypeRel f
+fromList = TypeMap.fromList . classify
+
+toList :: TypeRel f -> [Some f]
+toList = concatMap disperse . TypeMap.toList
+
+lookup :: Typeable a => a -> TypeRel f -> [f a]
+lookup x m = unO (TypeMap.lookup (O []) x m)
+
+mapValues :: (forall a. Typeable a => f a -> g a) -> TypeRel f -> TypeRel g
+mapValues f = TypeMap.mapValues2 (map f)
+
+gather :: [Some f] -> Some (List `O` f)
+gather [] =
+  error "Test.QuickSpec.Utils.TypeRep.sequence: empty list"
+gather (Some x:xs) = Some (O (x:map gcast' xs))
+  where gcast' (Some y) = fromMaybe (error msg) (gcast y)
+        msg = "Test.QuickSpec.Utils.TypeRep.gather: heterogeneous list"
+
+disperse :: Some (List `O` f) -> [Some f]
+disperse (Some (O xs)) = map Some xs
+
+classify :: [Some f] -> [Some (List `O` f)]
+classify xs = map gather (partitionBy someType xs)
diff --git a/Test/QuickSpec/Utils/Typeable.hs b/Test/QuickSpec/Utils/Typeable.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Utils/Typeable.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE NoMonomorphismRestriction, CPP #-}
+
+-- | A wrapper around 'Data.Typeable', to work around:
+--
+--   (1) The lack of an 'Ord' instance in older GHCs,
+--
+--   (2) bug #5962 in new GHCs.
+
+module Test.QuickSpec.Utils.Typeable(TypeRep, T.Typeable, T.Typeable1, T.Typeable2,
+                typeOf, typeOf1, cast, gcast,
+                mkTyConApp, typeRepTyCon, splitTyConApp,
+                mkFunTy, unTypeRep) where
+
+#if __GLASGOW_HASKELL__ >= 702
+#define NEW_TYPEABLE
+#endif
+
+import qualified Data.Typeable as T
+import Data.Ord
+#ifndef NEW_TYPEABLE
+import System.IO.Unsafe
+#endif
+
+newtype TypeRep = TypeRep { unTypeRep :: T.TypeRep }
+
+instance Eq TypeRep where
+  ty == ty' =
+    unTypeRep ty == unTypeRep ty' ||
+    ty `compare` ty' == EQ
+
+#ifdef NEW_TYPEABLE
+instance Ord TypeRep where
+  compare = comparing splitTyConApp
+#else
+instance Ord TypeRep where
+  compare = comparing (unsafePerformIO . T.typeRepKey . unTypeRep)
+#endif
+
+instance Show TypeRep where
+  showsPrec p = showsPrec p . unTypeRep
+
+typeOf = TypeRep . T.typeOf
+typeOf1 = TypeRep . T.typeOf1
+cast = T.cast
+gcast = T.gcast
+
+mkTyConApp f xs = TypeRep (T.mkTyConApp f (map unTypeRep xs))
+typeRepTyCon = T.typeRepTyCon . unTypeRep
+splitTyConApp ty = (c, map TypeRep tys)
+  where (c, tys) = T.splitTyConApp (unTypeRep ty)
+mkFunTy lhs rhs = TypeRep (T.mkFunTy (unTypeRep lhs) (unTypeRep rhs))
diff --git a/Test/QuickSpec/Utils/Typed.hs b/Test/QuickSpec/Utils/Typed.hs
new file mode 100644
--- /dev/null
+++ b/Test/QuickSpec/Utils/Typed.hs
@@ -0,0 +1,76 @@
+-- | Functions for working with existentially-quantified types
+--   and similar.
+
+{-# LANGUAGE Rank2Types, ExistentialQuantification, TypeOperators, TypeSynonymInstances, FlexibleInstances #-}
+module Test.QuickSpec.Utils.Typed where
+
+import Control.Monad
+import Test.QuickSpec.Utils.Typeable
+import Data.Ord
+import Data.Function
+import Data.Maybe
+
+data Some f = forall a. Typeable a => Some (f a)
+
+newtype O f g a = O { unO :: f (g a) }
+type List = []
+
+newtype Witnessed a = Witness { witness :: a }
+type Witness = Some Witnessed
+
+-- No Typeable (Witnessed a) instance to save accidentally looking up
+-- Witnessed a instead of a in a TypeMap
+
+instance Eq Witness where
+  (==) = (==) `on` witnessType
+
+instance Ord Witness where
+  compare = comparing witnessType
+
+instance Show Witness where
+  show = show . witnessType
+
+witnessType :: Witness -> TypeRep
+witnessType = some (typeOf . witness)
+
+data Tagged a = Tagged { tag :: Witness, erase :: a }
+
+tagged :: Typeable a => (f a -> b) -> f a -> Tagged b
+tagged f x = Tagged (Some (Witness (witness x))) (f x)
+  where witness :: f a -> a
+        witness = undefined
+
+some :: (forall a. Typeable a => f a -> b) -> Some f -> b
+some f (Some x) = f x
+
+some2 :: (forall a. Typeable a => f (g a) -> b) -> Some (f `O` g) -> b
+some2 f = some (f . unO)
+
+mapSome :: (forall a. Typeable a => f a -> g a) -> Some f -> Some g
+mapSome f (Some x) = Some (f x)
+
+mapSome2 :: (forall a. Typeable a => f (g a) -> h (i a)) -> Some (f `O` g) -> Some (h `O` i)
+mapSome2 f = mapSome (O . f . unO)
+
+mapSomeM :: Monad m => (forall a. Typeable a => f a -> m (g a)) -> Some f -> m (Some g)
+mapSomeM f (Some x) = liftM Some (f x)
+
+someType :: Some f -> TypeRep
+someType (Some x) = typeOf (witness x)
+  where witness :: f a -> a
+        witness = undefined
+
+someWitness :: Some f -> Witness
+someWitness = mapSome (const undefined)
+
+splitArrow :: TypeRep -> Maybe (TypeRep, TypeRep)
+splitArrow ty =
+  case splitTyConApp ty of
+    (c, [lhs, rhs]) | c == arr -> Just (lhs, rhs)
+    _ -> Nothing
+  where (arr, _) = splitTyConApp (typeOf (undefined :: Int -> Int))
+
+rightArrow :: TypeRep -> TypeRep
+rightArrow ty = snd (fromMaybe (error msg) (splitArrow ty))
+  where
+    msg = "Test.QuickSpec.Utils.Typed.rightArrow: type oversaturated"
diff --git a/examples/Arith.hs b/examples/Arith.hs
new file mode 100644
--- /dev/null
+++ b/examples/Arith.hs
@@ -0,0 +1,18 @@
+-- Natural number functions.
+
+{-# LANGUAGE ScopedTypeVariables #-}
+
+import Test.QuickSpec hiding (arith)
+import Test.QuickCheck
+import Data.Typeable
+
+arith :: forall a. (Typeable a, Ord a, Num a, Arbitrary a) => a -> [Sig]
+arith _ = [
+  ["x", "y", "z"] `vars` (undefined :: a),
+
+  "0" `fun0` (0   :: a),
+  "1" `fun0` (1   :: a),
+  "+" `fun2` ((+) :: a -> a -> a),
+  "*" `fun2` ((*) :: a -> a -> a)]
+
+main = quickSpec (arith (undefined :: Int))
diff --git a/examples/Bools.hs b/examples/Bools.hs
new file mode 100644
--- /dev/null
+++ b/examples/Bools.hs
@@ -0,0 +1,14 @@
+-- A simple booleans example.
+
+import Test.QuickSpec hiding (bools)
+
+bools = [
+  ["x", "y", "z"] `vars` (undefined :: Bool),
+
+  "||"    `fun2` (||),
+  "&&"    `fun2` (&&),
+  "not"   `fun1` not,
+  "True"  `fun0` True,
+  "False" `fun0` False]
+
+main = quickSpec bools
diff --git a/examples/Composition.hs b/examples/Composition.hs
new file mode 100644
--- /dev/null
+++ b/examples/Composition.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+import Test.QuickSpec
+import Test.QuickCheck
+import Data.Typeable
+
+composition :: forall a. (Typeable a, Ord a, Arbitrary a, CoArbitrary a) =>
+               a -> [Sig]
+composition _ = [
+  vars ["f", "g", "h"] (undefined :: a -> a),
+
+  -- We treat . as a function of two arguments here (blind2)---i.e.,
+  -- we do not generate terms of the form (f . g) x.
+  blind2 "."   ((.) :: (a -> a) -> (a -> a) -> (a -> a)),
+
+  -- Similarly, id is not treated as a function.
+  blind0 "id"  (id  :: a -> a),
+
+  -- Tell QuickSpec how to compare values of function type:
+  -- i.e., generate a random argument and apply the function to it.
+  observer2 $ \x (f :: a -> a) -> f x
+  ]
+
+main = quickSpec (composition (undefined :: A))
diff --git a/examples/Heaps.hs b/examples/Heaps.hs
new file mode 100644
--- /dev/null
+++ b/examples/Heaps.hs
@@ -0,0 +1,89 @@
+{-# LANGUAGE ScopedTypeVariables,DeriveDataTypeable #-}
+
+import Prelude hiding (null)
+import Test.QuickSpec
+import Test.QuickCheck
+import Data.Typeable
+import Data.Ord
+import qualified Data.List as L
+
+data Heap a = Nil | Branch Int a (Heap a) (Heap a) deriving Typeable
+
+instance Ord a => Eq (Heap a) where
+  h1 == h2 = toList h1 == toList h2
+
+instance Ord a => Ord (Heap a) where
+  compare = comparing toList
+
+instance (Ord a, Arbitrary a) => Arbitrary (Heap a) where
+  arbitrary = fmap fromList arbitrary
+
+toList :: Ord a => Heap a -> [a]
+toList h | null h = []
+         | otherwise = findMin h:toList (deleteMin h)
+
+fromList :: Ord a => [a] -> Heap a
+fromList = foldr insert Nil
+
+null :: Heap a -> Bool
+null Nil = True
+null _ = False
+
+findMin :: Heap a -> a
+findMin (Branch _ x _ _) = x
+
+insert :: Ord a => a -> Heap a -> Heap a
+insert x h = merge h (branch x Nil Nil)
+
+deleteMin :: Ord a => Heap a -> Heap a
+deleteMin (Branch _ _ l r) = merge l r
+
+branch :: Ord a => a -> Heap a -> Heap a -> Heap a
+branch x l r | npl l <= npl r = Branch (npl l + 1) x l r
+             | otherwise = Branch (npl r + 1) x r l
+
+merge :: Ord a => Heap a -> Heap a -> Heap a
+merge Nil h = h
+merge h Nil = h
+merge h1@(Branch _ x1 l1 r1) h2@(Branch _ x2 l2 r2)
+ | x1 <= x2 = branch x1 (merge l1 h2) r1
+ | otherwise = merge h2 h1
+
+npl :: Heap a -> Int
+npl Nil = 0
+npl (Branch n _ _ _) = n
+
+mergeLists :: Ord a => [a] -> [a] -> [a]
+mergeLists [] xs = xs
+mergeLists xs [] = xs
+mergeLists (x:xs) (y:ys)
+  | x < y = x:mergeLists xs (y:ys)
+  | otherwise = y:mergeLists (x:xs) ys
+
+heaps :: forall a. (Ord a, Typeable a, Arbitrary a) => a -> [Sig]
+heaps a = [
+  prelude a,
+
+  ["h", "h1", "h2"] `vars` (undefined :: Heap a),
+
+  "nil"        `fun0` (Nil        :: Heap a),
+  "insert"     `fun2` (insert     :: a -> Heap a -> Heap a),
+  "findMin"    `fun1` (findMin    :: Heap a -> a),
+  "deleteMin"  `fun1` (deleteMin  :: Heap a -> Heap a),
+  "merge"      `fun2` (merge      :: Heap a -> Heap a -> Heap a),
+  "null"       `fun1` (null       :: Heap a -> Bool),
+  "toList"     `fun1` (toList     :: Heap a -> [a]),
+  "fromList"   `fun1` (fromList   :: [a] -> Heap a),
+
+  -- A few more list functions that are helpful for getting
+  -- laws about toList/fromList.
+  -- We use "background" to mark the functions as background theory,
+  -- so that we only get laws that involve one of the heap functions.
+  background [
+  "sort"       `fun1` (L.sort     :: [a] -> [a]),
+  "insertList" `fun2` (L.insert   :: a -> [a] -> [a]),
+  "nullList"   `fun1` (L.null     :: [a] -> Bool),
+  "deleteList" `fun2` (L.delete   :: a -> [a] -> [a]),
+  "mergeLists" `fun2` (mergeLists :: [a] -> [a] -> [a])]]
+
+main = quickSpec (heaps (undefined :: A))
diff --git a/examples/Lists.hs b/examples/Lists.hs
new file mode 100644
--- /dev/null
+++ b/examples/Lists.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+import Test.QuickSpec hiding (lists)
+import Test.QuickCheck
+import Data.Typeable
+
+lists :: forall a. (Typeable a, Ord a, Arbitrary a, CoArbitrary a) =>
+         a -> [Sig]
+lists a = [
+  arith (undefined :: Int),
+  funs (undefined :: a),
+
+  ["x", "y", "z"] `vars` (undefined :: a),
+  ["xs", "ys", "zs"] `vars` (undefined :: [a]),
+
+  "[]"      `fun0` ([]      :: [a]),
+  ":"       `fun2` ((:)     :: a -> [a] -> [a]),
+  "head"    `fun1` (head    :: [a] -> a),
+  "tail"    `fun1` (tail    :: [a] -> [a]),
+  "unit"    `fun1` (return  :: a -> [a]),
+  "++"      `fun2` ((++)    :: [a] -> [a] -> [a]),
+  "length"  `fun1` (length  :: [a] -> Int),
+  "reverse" `fun1` (reverse :: [a] -> [a]),
+  "map"     `fun2` (map     :: (a -> a) -> [a] -> [a])
+  ]
+
+main = quickSpec (lists (undefined :: A))
diff --git a/examples/TinyWM.hs b/examples/TinyWM.hs
new file mode 100644
--- /dev/null
+++ b/examples/TinyWM.hs
@@ -0,0 +1,194 @@
+-- This example requires QuickCheck >= 2.5. For older versions, you will
+-- have to define an Arbitrary Ordering instance, like so:
+--   instance Arbitrary Ordering where
+--     arbitrary = elements [LT, EQ, GT]
+
+-- A window manager example,
+-- taken from http://donsbot.wordpress.com/2007/05/01/roll-your-own-window-manager-part-1-defining-and-testing-a-model
+
+{-# OPTIONS -fglasgow-exts #-}
+
+import Data.Maybe
+import Data.Map (Map)
+import Data.Typeable
+import qualified Data.Map as M
+import qualified Data.List as L
+import Test.QuickCheck
+import Test.QuickSpec
+
+-- ---------------------------------------------------------------------
+-- A data structure for multiple workspaces containing stacks of screens
+--
+
+data StackSet a = StackSet
+    { current :: Int           -- the current workspace
+    , stacks  :: Map Int [a] } -- map workspaces to window stacks
+    deriving (Eq, Ord, Show, Read, Typeable)
+
+-- | /O(n)/. Create a new empty stackset of 'n' workspaces
+empty :: Ord a => Int -> StackSet a
+empty n = StackSet { current = 0, stacks  = ws }
+  where
+    ws = M.fromList (zip [0..n-1] (repeat []))
+
+-- | /O(log n)/. Set the given stack as being visible. If the index is out of
+-- bounds, the stack is returned unmodified.
+view :: Int -> StackSet a -> StackSet a
+view n w | M.member n (stacks w) = w { current = n }
+         | otherwise             = w
+
+-- | /O(log s)/. Extract the element on the top of the current stack.
+-- If no such element exists, Nothing is returned.
+peek :: Ord a => StackSet a -> Maybe a
+peek w | Just (x:_) <- M.lookup (current w) (stacks w) = Just x
+       | otherwise                                     = Nothing
+
+-- | /O(log n)/. rotate. cycle the current window list up or down.
+-- Has the effect of rotating focus. In fullscreen mode this will cause
+-- a new window to be visible.
+--
+--  rotate EQ   -->  [5,6,7,8,1,2,3,4]
+--  rotate GT   -->  [6,7,8,1,2,3,4,5]
+--  rotate LT   -->  [4,5,6,7,8,1,2,3]
+--
+--  where xs = [5..8] ++ [1..4]
+--
+rotate :: Ordering -> StackSet a -> StackSet a
+rotate o w = w { stacks = M.adjust rot (current w) (stacks w) }
+  where
+    rot [] = []
+    rot xs = case o of
+        GT -> tail xs ++ [head xs]
+        LT -> last xs : init xs
+        _  -> xs
+
+-- ---------------------------------------------------------------------
+-- operations that affect multiple workspaces
+
+-- | /O(log n)/. Push. Insert an element onto the top of the current stack.
+-- If the element is already in the current stack, it is moved to the top.
+-- If the element is managed on another stack, it is removed from that stack.
+--
+push :: Ord a => a -> StackSet a -> StackSet a
+push k w = insert k (current w) w
+
+-- | /O(log n)/. shift. move the client on top of the current stack to
+-- the top of stack 'n'. If the stack to move to is not valid, and
+-- exception is thrown. If there's no client on the current stack, the
+-- stack set is returned unchanged.
+shift :: (Ord a) => Int -> StackSet a -> StackSet a
+shift n w = maybe w (\k -> insert k n w) (peek w)
+
+-- | /O(log n)/. Insert an element onto the top of stack 'n'.
+-- If the element is already in the stack 'n', it is moved to the top.
+-- If the element exists on another stack, it is removed from that stack.
+-- If the index is wrong an exception is thrown.
+insert :: Ord a => a -> Int -> StackSet a -> StackSet a
+insert k n old = new { stacks = M.adjust (k:) n (stacks new) }
+    where new = delete k old
+
+-- | /O(n)/. Delete an element entirely from from the StackSet.
+-- If the element doesn't exist, the original StackSet is returned unmodified.
+-- If the current element is focused, focus will change.
+delete :: Ord a => a -> StackSet a -> StackSet a
+delete k w = maybe w del $ L.find ((k `elem`) . snd) (M.assocs (stacks w))
+  where
+    del (i,_) = w { stacks = M.adjust (L.delete k) i (stacks w) }
+
+-- | /O(log n)/. Index. Extract the stack at workspace 'n'.
+-- If the index is invalid, an exception is thrown.
+index :: Int -> StackSet a -> [a]
+index k w = fromJust (M.lookup k (stacks w))
+
+--
+-- Arbitrary instances and helper functions.
+--
+
+------------------------------------------------------------------------
+--
+-- Building StackSets from lists
+--
+
+fromList :: Ord a => (Int, [[a]]) -> StackSet a
+fromList (_,[]) = error "Cannot build a StackSet from an empty list"
+fromList (n,xs) | n < 0 || n >= length xs
+                = error $ "Cursor index is out of range: " ++ show (n, length xs)
+fromList (o,xs) = view o $
+    foldr (\(i,ys) s ->
+        foldr (\a t -> insert a i t) s ys)
+            (empty (length xs)) (zip [0..] xs)
+
+-- flatten a stackset to a list
+toList  :: StackSet a -> (Int,[[a]])
+toList x = (current x, map snd $ M.toList (stacks x))
+
+-- ---------------------------------------------------------------------
+--
+-- Some useful predicates and helpers
+--
+
+-- a window is a member
+member :: Ord a => a -> StackSet a -> Bool
+member k w =
+    case L.find ((k `elem`) . snd) (M.assocs (stacks w)) of
+        Nothing -> False
+        _       -> True
+
+-- | /O(n)/. Number of stacks
+size :: T -> Int
+size = M.size . stacks
+
+-- | Height of stack 'n'
+height :: Int -> T -> Int
+height i w = length (index i w)
+
+--
+-- Generate arbitrary stacksets
+--
+instance (Ord a, Arbitrary a) => Arbitrary (StackSet a) where
+    arbitrary = do
+        sz <- choose (1,5)
+        n  <- choose (0,sz-1)
+        ls <- vector sz
+        let s = fromList (fromIntegral n,ls)
+        return s
+
+instance (Ord a, CoArbitrary a) => CoArbitrary (StackSet a) where
+    coarbitrary s = coarbitrary (toList s)
+
+--
+-- QuickSpec stuff.
+--
+
+ordering :: Sig
+ordering = signature [
+  con "LT" LT,
+  con "GT" GT,
+  con "EQ" EQ,
+  vars ["o", "o'"] (undefined :: Ordering)]
+
+--
+-- constrain it to a simple element type
+--
+type T = StackSet A
+
+tinywm :: [Sig]
+tinywm = [
+  prelude (undefined :: A) `without` ["+", "*"],
+  gvars ["x", "y", "q"] (choose (0, 3) :: Gen Int),
+  ordering,
+
+  ["s"] `vars` (undefined :: T),
+
+  "empty"   `fun1` (empty           :: Int -> T),
+  "view"    `fun2` (view            :: Int -> T -> T),
+  "peek"    `fun1` (fromJust . peek :: T -> A),
+  "rotate"  `fun2` (rotate          :: Ordering -> T -> T),
+  "push"    `fun2` (push            :: A -> T -> T),
+  "shift"   `fun2` (shift           :: Int -> T -> T),
+  "insert"  `fun3` (insert          :: A -> Int -> T -> T),
+  "delete"  `fun2` (delete          :: A -> T -> T),
+  "current" `fun1` (current         :: T -> Int),
+  "index"   `fun2` (index           :: Int -> T -> [A])]
+
+main = quickSpec tinywm
diff --git a/quickspec.cabal b/quickspec.cabal
new file mode 100644
--- /dev/null
+++ b/quickspec.cabal
@@ -0,0 +1,89 @@
+Name:                quickspec
+Version:             0.9
+Cabal-version:       >=1.6
+Build-type:          Simple
+
+Homepage:            https://github.com/nick8325/quickspec
+Author:              Nick Smallbone
+Maintainer:          nicsma@chalmers.se
+
+License:             BSD3
+License-file:        LICENSE
+Copyright:           2009-2013 Nick Smallbone
+
+Category:            Testing
+
+Synopsis:            Equational laws for free
+Description:
+  QuickSpec automatically finds equational properties of your program.
+  .
+  Give it an API, i.e. a collection of functions, and it will spit out
+  equations about those functions. For example, given @reverse@, @++@
+  and @[]@, QuickSpec finds six laws:
+  .
+  > xs++[] == xs
+  > []++xs == xs
+  > reverse [] == []
+  > (xs++ys)++zs == xs++(ys++zs)
+  > reverse (reverse xs) == xs
+  > reverse xs++reverse ys == reverse (ys++xs)
+  .
+  All you have to provide is:
+  .
+  * Some functions and constants to test. These are the /only/
+    functions that will appear in the equations.
+  .
+  * A collection of variables that can appear in the equations
+    (@xs@, @ys@ and @zs@ in the example above).
+  .
+  * 'Test.QuickCheck.Arbitrary' and 'Data.Typeable.Typeable' instances for the types you want to test.
+  .
+  Consider this a pre-release. Everything is complete but undocumented
+  :) The best place to start is the examples at
+  <http://github.com/nick8325/quickspec/tree/master/examples>. There
+  is also a paper at
+  <http://www.cse.chalmers.se/~nicsma/quickspec.pdf>.
+  Everything you need should be in the module "Test.QuickSpec".
+  .
+  If you want help, email me!
+
+Extra-source-files:
+  README
+  examples/Arith.hs
+  examples/Bools.hs
+  examples/Composition.hs
+  examples/Heaps.hs
+  examples/Lists.hs
+  examples/TinyWM.hs
+
+source-repository head
+  type:     git
+  location: git://github.com/nick8325/quickspec.git
+  branch:   master
+
+library
+  Exposed-modules:
+    Test.QuickSpec,
+    Test.QuickSpec.Main,
+    Test.QuickSpec.Signature,
+    Test.QuickSpec.Prelude,
+    Test.QuickSpec.Term,
+    Test.QuickSpec.Equation,
+    Test.QuickSpec.Generate,
+    Test.QuickSpec.TestTree,
+    Test.QuickSpec.Reasoning.UnionFind,
+    Test.QuickSpec.Reasoning.CongruenceClosure,
+    Test.QuickSpec.Reasoning.NaiveEquationalReasoning,
+    Test.QuickSpec.Utils,
+    Test.QuickSpec.Utils.Typeable,
+    Test.QuickSpec.Utils.Typed,
+    Test.QuickSpec.Utils.TypeMap,
+    Test.QuickSpec.Utils.TypeRel,
+    Test.QuickSpec.Approximate
+  Other-modules:
+    -- Dangerous!
+    Test.QuickSpec.Utils.MemoValuation
+
+  Build-depends:
+    base < 5, containers, transformers, QuickCheck,
+    random, spoon >= 0.2, array, ghc-prim, mtl