diff --git a/Control/Monad/TagShare.hs b/Control/Monad/TagShare.hs
deleted file mode 100644
--- a/Control/Monad/TagShare.hs
+++ /dev/null
@@ -1,62 +0,0 @@
-
--- | A monad for binding values to tags to ensure sharing, 
--- with the added twist that the value can be polymorphic
--- and each monomorphic instance is bound separately.
-module Control.Monad.TagShare(
-  -- ** Dynamic map
-  DynMap,
-  dynEmpty,
-  dynInsert,
-  dynLookup,
-  -- ** Sharing monad
-  Sharing,
-  runSharing,
-  share
-  ) where
-import Control.Monad.State
-import Data.Typeable
-import Data.Dynamic(Dynamic, fromDynamic, toDyn)
-import Data.Map as M
-
--- |  A dynamic map with type safe
--- insertion and lookup.
-newtype DynMap tag = 
-  DynMap (M.Map (tag, TypeRep) Dynamic) 
-  deriving Show
-
-dynEmpty :: DynMap tag
-dynEmpty = DynMap M.empty  
-  
-dynInsert :: (Typeable a, Ord tag) => 
-                tag -> a -> DynMap tag -> DynMap tag
-dynInsert u a (DynMap m) = 
-          DynMap (M.insert (u,typeOf a) (toDyn a) m)
-
-dynLookup :: (Typeable a, Ord tag) => 
-                tag -> DynMap tag -> Maybe a
-dynLookup u (DynMap m) = hlp fun undefined where 
-    hlp :: Typeable a => 
-      (TypeRep -> Maybe a) -> a -> Maybe a
-    hlp f a = f (typeOf a)
-    fun tr = M.lookup (u,tr) m >>= fromDynamic
-
- 
--- | A sharing monad
--- with a function that binds a tag to a value.
-type Sharing tag a = State (DynMap tag) a
-
-runSharing :: Sharing tag a -> a
-runSharing m = evalState m dynEmpty
-
-share :: (Typeable a, Ord tag) => 
-  tag -> Sharing tag a -> Sharing tag a
-share t m = do
-    mx <- gets $ (dynLookup t)
-    case mx of
-      Just e      ->  return e
-      Nothing     ->  mfix $ \e -> do
-        modify (dynInsert t e)
-        m
-
-
-
diff --git a/Test/Feat.hs b/Test/Feat.hs
--- a/Test/Feat.hs
+++ b/Test/Feat.hs
@@ -1,24 +1,30 @@
 -- | This module contains a (hopefully) manageable subset of the functionality
 -- of Feat. The rest resides only in the Test.Feat.* modules.
 module Test.Feat(
-  Enumerate(..),
+  Enumerate(),
   -- * The type class
   Enumerable(..),
+  shared,
   nullary,
   unary,
+  FreePair(..),
   funcurry,
   consts,
+  -- ** Automatic derivation
   deriveEnumerable,
-  FreePair(..),
   -- * Accessing data
-  optimised,
+  optimal,
   index,
   values,
   bounded,
   uniform,
+  -- ** Testing drivers
+  featCheck,
   ioFeat,
   ioAll,
-  ioBounded  
+  ioBounded,
+  Report,
+  inputRep
   ) where
 
 import Test.Feat.Access
diff --git a/Test/Feat/Access.hs b/Test/Feat/Access.hs
--- a/Test/Feat/Access.hs
+++ b/Test/Feat/Access.hs
@@ -9,10 +9,16 @@
   bounded,
   
   -- ** A simple property tester
+  featCheck,
+
   ioFeat,
   ioAll,
   ioBounded,
   
+  Report,
+  inputRep,
+  prePostRep,
+  
   -- ** Compatibility
   -- *** QuickCheck
   uniform,
@@ -32,53 +38,56 @@
 import Test.Feat.Class
 -- base
 import Data.List
+import Data.Ratio((%))
 -- quickcheck
 import Test.QuickCheck
 -- smallcheck
 -- import Test.SmallCheck.Series -- Not needed
 
-group :: Enumerate a -> Part -> Index -> Integer
-group e p i = sum (map (card e) [0..p-1]) + i
 
-split :: Enumerate a -> Integer -> (Part, Index)
-split e i0 = go i0 0 where
-  go i p = let crd = card e p in 
-     if i < crd then (p,i)
-     else go (i-crd) (p+1)
-
--- | Mainly as a proof of concept we can use the isomorphism between 
--- natural numbers and @(Part,Index)@ pairs to index into a type.
--- May not terminate for finite types.
--- Might be slow the first time it is used with a specific enumeration 
--- because cardinalities need to be calculated.
--- The computational complexity (after cardinalities are computed) is a polynomial
--- in the size of the resulting value.
-index :: Enumerate a -> Integer -> a 
-index e = uncurry (select e) . split e
+-- | Mainly as a proof of concept (if this is repeated multiple times it might 
+-- be very inefficient, depending on whether the dictionary for the Enumerable 
+-- is shared or not) we define a function to index into an enumeration.
+index :: Enumerable a => Integer -> a 
+index i0 = go (parts optimal) i0 where
+  go (Finite crd ix : ps)  i  = if i < crd then ix i else go ps (i-crd)
+  go []                    _  = error $ "index out of bounds: "++show i0
 
 -- | All values of the enumeration by increasing cost (which is the number
 -- of constructors for most types). Also contains the cardinality of each list.
 values :: Enumerable a => [(Integer,[a])]
-values = valuesWith optimised
+values = valuesWith optimal
 
 -- | A generalisation of @values@ that enumerates every nth value of the 
 -- enumeration from a given starting point.
--- As a special case @values = striped 0 0 1@.
-striped ::  Enumerable a => Part -> Index -> Integer -> [(Integer,[a])]
-striped = stripedWith optimised 
+-- As a special case @values = striped 0 1@.
+--
+-- Useful for running enumerations in parallel since e.g. @striped 0 2@ is 
+-- disjoint from @striped 0 1 2@ and the union of the two cover all values.
+striped ::  Enumerable a => Index -> Integer -> [(Integer,[a])]
+striped = stripedWith optimal 
 
--- | A version of vales that has a limited number of values in each inner list.
+-- | A version of values with a limited number of values in each inner list.
 -- If the list corresponds to a Part which is larger than the bound it evenly
--- intersperses the values across the enumeration of the Part.
+-- distributes the values across the enumeration of the Part.
 bounded :: Enumerable a => Integer -> [(Integer,[a])]
-bounded = boundedWith optimised
+bounded = boundedWith optimal
 
+
+-- | Check a property for all values up to a given size.
+-- @ featCheck p prop = 'ioAll' p ('inputRep' prop) @
+featCheck :: (Enumerable a, Show a) => Int -> (a -> Bool) -> IO ()
+featCheck p prop = ioAll p (inputRep prop)
+
+-- | Functions that test a property and reports the result.
+type Report a = a -> IO ()
+
 -- | A rather simple but general property testing driver.
 -- The property is an (funcurried) IO function that both tests and reports the 
 -- error. The driver goes on forever or until the list is exhausted, 
--- reporting the coverage and the number of
+-- reporting its progress and the number of 
 -- tests before each new part.
-ioFeat :: [(Integer,[a])] -> (a -> IO ()) -> IO ()
+ioFeat :: [(Integer,[a])] -> Report a -> IO ()
 ioFeat vs f = go vs 0 0 where
   go ((c,xs):xss) s tot = do
     putStrLn $ "--- Testing "++show c++" values at size " ++ show s
@@ -86,70 +95,90 @@
     go xss (s+1) (tot + c)
   go []           s tot = putStrLn $ "--- Done. Tested "++ show tot++" values"
 
--- | Defined as @ioAll = 'ioFeat' 'values' @
-ioAll :: Enumerable a => (a -> IO ()) -> IO ()
-ioAll = ioFeat values
+-- | Defined as @ioAll p = 'ioFeat' (take p 'values') @
+ioAll :: Enumerable a => Int -> Report a -> IO ()
+ioAll p = ioFeat (take p values)
 
--- | Defined as @ioBounded n = 'ioFeat' ('bounded' n)@
-ioBounded :: Enumerable a => Integer -> (a -> IO ()) -> IO ()
-ioBounded n = ioFeat (bounded n)
+-- | Defined as @ioBounded n p = 'ioFeat' (take p $ 'bounded' n)@
+ioBounded :: Enumerable a => Integer -> Int -> Report a -> IO ()
+ioBounded n p = ioFeat (take p $ bounded n)
 
+-- | Reports counterexamples to the given predicate by printing them
+inputRep :: Show a => (a -> Bool) -> Report a
+inputRep pred a = if pred a
+  then return ()
+  else do
+    putStrLn "Counterexample found:"
+    print a
+    putStrLn ""
 
+-- | Takes a function and a predicate on its input/output pairs. 
+-- Reports counterexamples by printing the failing input/output pair.
+prePostRep :: (Show a, Show b) => (a -> b) -> (a -> b -> Bool) -> Report a
+prePostRep f pred a = let fa = f a in if pred a fa
+  then return ()
+  else do
+    putStrLn "Counterexample found. Input:"
+    print a
+    putStrLn "Output:"
+    print fa
+    putStrLn ""
 
+
 -- | Compatibility with QuickCheck. Distribution is uniform generator over 
 -- values bounded by the given size. Typical use: @sized uniform@.
 uniform :: Enumerable a => Int -> Gen a
-uniform = uniformWith optimised
+uniform = uniformWith optimal
 
 -- | Compatibility with SmallCheck. 
 toSeries :: Enumerable a => Int -> [a] 
-toSeries = toSeriesWith optimised
+toSeries = toSeriesWith optimal
 
 -- | Non class version of 'values'.
 valuesWith :: Enumerate a -> [(Integer,[a])]
-valuesWith e = 
-  [(crd,[select e p i|i <- [0..crd - 1]]) 
-    |p <- [0..], let crd = card e p]
+valuesWith = map fromFinite . parts
 
 -- | Non class version of 'striped'.
-stripedWith :: Enumerate a -> Part -> Index -> Integer -> [(Integer,[a])]
-stripedWith e p o step = if space <= 0 
-  then (0,[]) : stripedWith e (p+1) (o - crd) step
-  else (d,thisP) : stripedWith e (p+1) (step-m-1) step
-  where
-    thisP = 
-      [select e p x|x <- genericTake d $ iterate (+step) o]
-    space = crd - o
-    (d,m) = divMod space step
-    crd = card e p
+stripedWith :: Enumerate a -> Index -> Integer -> [(Integer,[a])]
+stripedWith e o0 step = stripedWith' (parts e) o0 where
+  stripedWith' []                   o = []
+  stripedWith' (Finite crd ix : ps) o = 
+    (max 0 d,thisP) : stripedWith' ps o'
+    where
+      o'     = if space <= 0 then o-crd else step-m-1
+      thisP  = map ix (genericTake d $ iterate (+step) o)
+      space  = crd - o
+      (d,m)  = divMod space step
 
 -- | Non class version of 'bounded'.
 boundedWith :: Enumerate a -> Integer -> [(Integer,[a])]
-boundedWith e n = map (samplePart e n) [0..]
+boundedWith e n = map (samplePart n) $ parts e
 
-samplePart :: Enumerate a -> Index -> Part -> (Integer,[a])
-samplePart e m p = 
-  let
-    top   =  toRational $ (card e p) - 1
-    step  =  top / toRational (m-1) 
-    crd = card e p
-  in if toRational m >= top 
-       then (crd, map (select e p) [0..crd - 1])
-       else let d = floor ((toRational crd)/ step) in 
-         (d+1,[select e p (round (k * step))|k <- map toRational [0..d]])
+-- Specification: pick at most @m@ evenly distributed values from part @p@ of @e@
+-- Return the list length together with the list of the selected values.
+samplePart :: Index -> Finite a -> (Integer,[a])
+samplePart m (Finite crd ix) = 
+  let  step  =  crd % m
+  in if crd <= m
+       then (crd,  map ix [0..crd - 1])
+       else (m,    map ix [ round (k * step)
+                                    | k <- map toRational [0..m-1]])
+-- The first value is at index 0 and the last value is at index ~= crd - step
+-- This is "fair" if we consider using samplePart on the next part as well.
+-- An alternative would be to make the last index used |crd-1|.
 
+
 -- | Non class version of 'uniform'.
-uniformWith :: Enumerate a -> Part -> Gen a
-uniformWith e maxp = let
-  cards  = [(card e x, x) | x <- [maxp, maxp-1 .. 0]]
-  tot    = sum $ fst $ unzip cards
-  in if tot == 0 then uniformWith e (maxp+1) else do
-    i <- choose (0,tot-1)
-    return $ uncurry (select e) (lu i cards)
-  where
-    lu i ((crd,p):xs)  = if i<crd 
-      then (p,i) 
-      else lu (i-crd) xs
+uniformWith :: Enumerate a -> Int -> Gen a
+uniformWith = uni . parts where
+  uni :: [Finite a] -> Int -> Gen a 
+  uni  []  _     =  error "uniform: empty enumeration"
+  uni  ps  maxp  =  let  (incl, rest)  = splitAt maxp ps
+                         fin           = mconcat incl   
+    in  case fCard fin of
+          0  -> uni rest 1
+          _  -> do  i <- choose (0,fCard fin-1)
+                    return (fIndex fin i)   
       
 -- | Non class version of 'toSeries'.
 toSeriesWith :: Enumerate a -> Int -> [a]
diff --git a/Test/Feat/Class.hs b/Test/Feat/Class.hs
--- a/Test/Feat/Class.hs
+++ b/Test/Feat/Class.hs
@@ -24,7 +24,8 @@
   consts,
   
   -- ** Accessing the enumerator of an instance
-  optimised,
+  shared,
+  optimal,
   
   -- *** Free pairs
   FreePair(..),
@@ -60,24 +61,24 @@
 
 -- | A class of functionally enumerable types
 class Typeable a => Enumerable a where
-  -- | This is the interface for defining an instance. Memoisation needs to 
-  -- be ensured e.g. using 'mempay' but sharing is handled automatically by 
-  -- the default implementation of 'shared'.
+  -- | This is the interface for defining an instance. When combining 
+  -- enumerations use 'shared' instead and when accessing the data of 
+  -- enumerations use 'optimal'.
   enumerate  :: Enumerate a
-  
-  -- | Version of enumerate that ensures it is shared between
-  -- all accessing functions. Should always be used when 
-  -- combining enumerations.
-  -- Should typically be left to default behaviour.
-  shared     :: Enumerate a
-  shared  = tagShare Class enumerate
 
--- | An optimised version of enumerate. Used by all
+
+-- | Version of 'enumerate' that ensures that the enumeration is shared 
+-- between all accesses. Should always be used when 
+-- combining enumerations.
+shared :: Enumerable a => Enumerate a
+shared  = eShare Class enumerate
+  
+-- | An optimal version of enumerate. Used by all
 -- library functions that access enumerated values (but not 
 -- by combining functions). Library functions should ensure that 
--- @optimised@ is not reevaluated.
-optimised :: Enumerable a => Enumerate a
-optimised = optimise shared   
+-- @optimal@ is not reevaluated.
+optimal :: Enumerable a => Enumerate a
+optimal = optimise shared   
 
 -- | A free pair constructor. The cost of constructing a free pair
 -- is equal to the sum of the costs of its components. 
@@ -90,7 +91,7 @@
 
 instance (Enumerable a, Enumerable b) => 
          Enumerable (FreePair a b) where
-  enumerate = mem $ curry Free <$> shared <*> shared
+  enumerate = curry Free <$> shared <*> shared
 
 type Constructor = Enumerate
   
@@ -109,17 +110,24 @@
 -- directly in an instance even if it only has one constructor. So you 
 -- should apply consts even in that case. 
 consts :: [Constructor a] -> Enumerate a
-consts xs = mempay $ mconcat xs 
+consts xs = pay $ mconcat xs 
 
 
 --------------------------------------------------------------------
 -- Automatic derivation
 
--- | Derive an instance of Enumberable with Template Haskell.
+-- | Derive an instance of Enumberable with Template Haskell. To derive
+-- an instance for @Enumerable A@, just put this as a top level declaration 
+-- in your module (with the TemplateHaskell extension enabled):
+-- 
+-- @
+--   deriveEnumerable ''A
+-- @
+
 deriveEnumerable :: Name -> Q [Dec]
 deriveEnumerable = deriveEnumerable' . dAll
-  -- fmap return . instanceFor ''Enumerable [enumDef]
 
+
 type ConstructorDeriv = (Name, [(Name, ExpQ)])
 dAll :: Name -> ConstructorDeriv
 dAll n = (n,[])
@@ -150,20 +158,8 @@
           [] -> return ()
           xs -> error $ "Invalid constructors for "++show n++": "++show xs
         
--- do
---          (_,ns,_) <- extractData n
---          if all (map snd nse) (`elem` ns) 
---            then return () 
---            else error $ "Invalid constructors for "++show n++": "++
---                        show (filter (`notElem` ns) (map fst nse)) 
 
 
-
-
-
-
-
-
 ---------------------------------------------------------------------
 -- Instances
 
@@ -195,19 +191,23 @@
   in it)
   
 
+simpleEnum car sel = 
+  let e = Enumerate 
+           (toRev$ map (\p -> Finite (car p) (sel p)) [0..])
+           (return e)
+  in e
 
+
 -- This instance is quite important. It needs to be exponential for 
 -- the other instances to work.
 instance Infinite a => Enumerable (Nat a) where 
-  enumerate = let e = Enumerate{
-    card = crd,
-    select = sel,
-    optimal = return e} in e where
+  enumerate = simpleEnum crd sel 
+    where
       crd p
         | p <= 0     = 0
         | p == 1     = 1
         | otherwise  = 2^(p-2)
-      sel :: Num a => Part -> Index -> Nat a
+      sel :: Num a => Int -> Index -> Nat a
       sel 1 0 = Nat 0
       sel p i = Nat $ 2^(p-2) + fromInteger i
 
@@ -231,10 +231,8 @@
   e = cutOff (bitSize' e+1) $ unary fromInteger
 
 cutOff :: Int -> Enumerate a -> Enumerate a 
-cutOff n e = e{
-  card = \p -> if p > n then 0 else card e p, 
-  optimal = fmap (cutOff n) $ optimal e
-  }
+cutOff n e = Enumerate prts (fmap (cutOff n) (optimiser e)) where
+  prts = toRev$ take n $ parts e
 
 bitSize' :: Bits a => f a -> Int
 bitSize' f = hlp undefined f where
diff --git a/Test/Feat/Class/Override.hs b/Test/Feat/Class/Override.hs
--- a/Test/Feat/Class/Override.hs
+++ b/Test/Feat/Class/Override.hs
@@ -33,11 +33,12 @@
 -- you from placing lots of 'printable' modifiers in your instances or 
 -- newtypes in your data type definitions.
 --
--- This works for any type (not just characters) as long as the instance does 
--- not override the default definition of 'shared' so it does not use 
--- 'tagShare' (no instance in the library does this).This function should not 
--- be used for defining instances (doing so might increase memory usage).
+-- This works for any type (not just characters). This function should typically 
+-- not be used when combining enumerations (doing so might increase memory 
+-- usage because the resulting enumeration is optimised).
+-- Also this only has effect on enumerations which have not already been 
+-- optimised, so using override again on the result of override has no effect.
 override :: Enumerable a => Override -> Enumerate a
-override = evalState (optimal shared) 
+override = evalState (optimiser shared) 
 
 
diff --git a/Test/Feat/Enumerate.hs b/Test/Feat/Enumerate.hs
--- a/Test/Feat/Enumerate.hs
+++ b/Test/Feat/Enumerate.hs
@@ -4,29 +4,39 @@
 -- most users will want to use the type class 
 -- based combinators in "Test.Feat.Class" instead. 
 
-module Test.Feat.Enumerate(
-  
-  Part,
+module Test.Feat.Enumerate (
+ 
+
   Index,
   Enumerate(..),
+  parts,
+  fromParts,
   
+  -- ** Reversed lists
+  RevList(..),
+  toRev,
+  
+  -- ** Finite ordered sets
+  Finite(..),
+  fromFinite,
+  
+  
   -- ** Combinators for building enumerations
   module Data.Monoid,
   union,
   module Control.Applicative,
+  cartesian,
   singleton,
   pay,
-  
-  -- ** Memoisation
-  mem,
-  mempay,
-    
-  -- *** Polymorphic memoisation
+
+  -- *** Polymorphic sharing
   module Data.Typeable,
   Tag(Source),
   tag,
-  tagShare,
+  eShare,
+  noOptim,
   optimise  
+
   ) where
 
 -- testing-feat
@@ -35,11 +45,11 @@
 -- base
 import Control.Applicative
 import Control.Monad
+import Data.Function
 import Data.Monoid
 import Data.Typeable
 import Language.Haskell.TH
--- data-memocombinators
-import Data.MemoCombinators
+import Data.List(transpose)
 
 
 
@@ -47,81 +57,143 @@
 type Index = Integer
 
 -- | A functional enumeration of type @t@ is a partition of
--- @t@ into finite numbered sets called Parts. The number that
--- identifies each part is called the cost of the values in 
--- that part.
-data Enumerate a = Enumerate
-   {  
-   -- | Computes the cardinality of a given part.
-   card      ::  Part -> Index,
-   -- | Selects a value from the enumeration
-   -- For @select e p i@, the index @i@ should be less than @card e p@
-   select    ::  Part -> Index -> a,
-   -- | A self-optimising function (mainly for internal use). 
-   optimal   ::  Sharing Tag (Enumerate a)
-   } deriving Typeable     
+-- @t@ into finite numbered sets called Parts. Each parts contains values
+-- of a certain cost (typically the size of the value).
+data Enumerate a = Enumerate 
+   { revParts :: RevList (Finite a)
+   , optimiser ::  Sharing Tag (Enumerate a) -- Should be RevList a?
+   } deriving Typeable    
 
+parts :: Enumerate a -> [Finite a]
+parts = fromRev . revParts
+
+fromParts :: [Finite a] -> Enumerate a
+fromParts ps = Enumerate (toRev ps) (return $ fromParts ps)
+
 -- | Only use fmap with bijective functions (e.g. data constructors)
 instance Functor Enumerate where 
-  fmap f cf = cf
-    {select    = \p n -> f (select cf p n)
-    , optimal  = liftM (fmap f) (optimal cf) }
+  fmap f e = Enumerate (fmap (fmap f) $ revParts e) (fmap (noOptim . fmap f) $ optimiser e)
 
+-- | Pure is 'singleton' and '<*>' corresponds to cartesian product (as with lists)
+instance Applicative Enumerate where
+  pure     = singleton
+  f <*> a  = fmap (uncurry ($)) (cartesian f a)
+
 -- | The @'mappend'@ is (disjoint) @'union'@
 instance Monoid (Enumerate a) where
-  mempty      = let e = Enumerate  (\p -> 0) 
-                                   (\p i -> error "select: empty")
-                                   (return e) in e
+  mempty      = Enumerate mempty (return mempty)
   mappend     = union
+  mconcat     = econcat
+  
+-- | Optimal 'mconcat' on enumerations.
+econcat :: [Enumerate a] -> Enumerate a
+econcat []    = mempty
+econcat [a]   = a
+econcat [a,b] = union a b
+econcat xs    = Enumerate 
+  (toRev . map mconcat . transpose $ map parts xs)
+  (fmap (noOptim . econcat) $ mapM optimiser xs)
 
--- | Disjoint union
-union :: Enumerate a -> Enumerate a -> Enumerate a
-union a b  =  infinite part (liftM2 union (optimal a) (optimal b)) where
-  part p   =  finUnion (finite a p) (finite b p)
 
--- | Pure is 'singleton' and '<*>' corresponds to cartesian product (as with lists)
-instance Applicative Enumerate where
-  pure     = singleton
-  f <*> a  = fmap (uncurry ($)) (cartesian f a)
+-- Product of two enumerations
+cartesian (Enumerate xs1 o1) (Enumerate xs2 o2) =
+  Enumerate (xs1 `prod` xs2) (fmap noOptim $ liftM2 cartesian o1 o2)
 
--- | The product of two enumerations
-cartesian :: Enumerate a -> Enumerate b -> Enumerate (a,b)
-cartesian a b = infinite (\p -> foldl1 finUnion
-  [finCart (finite a x) (finite b (p-x))| x <- [0..p]])
-    (liftM2 cartesian (optimal a) (optimal b))
+prod :: RevList (Finite a) -> RevList (Finite b) -> RevList (Finite (a,b))
+prod (RevList [] _)          _                = mempty
+prod (RevList xs0@(_:xst) _) (RevList _ rys0) = toRev$ prod' rys0 where
 
+  -- We need to thread carefully here, making sure that guarded recursion is safe
+  prod' []        = []
+  prod' (ry:rys)  = go ry rys where
+    go ry    rys  = merge xs0 ry : case rys of
+      (ry':rys') -> go ry' rys'
+      []         -> prod'' ry xst
+
+  -- rys0 is exhausted, slide a window over xs0 until it is exhausted
+  prod'' :: [Finite b] -> [Finite a] -> [Finite (a,b)]
+  prod'' ry = go where
+    go []         = []
+    go xs@(_:xs') = merge xs ry : go xs'
+
+  merge :: [Finite a] -> [Finite b] -> Finite (a,b)
+  merge xs ys = Finite 
+    (sum $ zipWith (*) (map fCard xs) (map fCard ys )) 
+    (prodSel xs ys)
+
+  prodSel :: [Finite a] -> [Finite b] -> (Index -> (a,b))
+  prodSel (f1:f1s) (f2:f2s) = \i -> let mul = fCard f1 * fCard f2  in if i < mul 
+    then let (q, r) = (i `quotRem` fCard f2) 
+       in (fIndex f1 q, fIndex f2 r)
+    else prodSel f1s f2s (i-mul)
+  prodSel _ _ = \i -> error "index out of bounds"
+
+
+union :: Enumerate a -> Enumerate a -> Enumerate a
+union (Enumerate xs1 o1) (Enumerate xs2 o2) =
+  Enumerate (xs1 `mappend` xs2) (fmap noOptim $ liftM2 union o1 o2)
+
+
 -- | The definition of @pure@ for the applicative instance. 
 singleton :: a -> Enumerate a
-singleton a = let e = Enumerate car sel (return e) in e 
-  where  car p    = if p == 0 then 1 else 0
-         sel 0 0  = a
-         sel _ _  = 
-           error "select: index out of bounds"
+singleton a = Enumerate (revPure $ finPure a) (return (singleton a))
 
+
 -- | Increases the cost of all values in an enumeration by one.
 pay :: Enumerate a -> Enumerate a
-pay sel = Enumerate
-    {  card      = \p -> if p <= 0 then 0 else card sel (p-1)
-    ,  select    = \p -> select sel (p-1)
-    ,  optimal   = liftM pay (optimal sel)
-    }
+pay e = Enumerate (revCons mempty $ revParts e) (fmap (noOptim . pay) $ optimiser e)
 
--------------------------------------------------------
--- Memoisation
 
-mem :: Enumerate a -> Enumerate a
-mem sel = sel
-    { card      = bits (card sel)
-    , optimal   = fmap mem (optimal sel)
-    }
+------------------------------------------------------------------
+-- Reverse lists
 
--- | A convenient combination of memoisation and guarded recursion.
-mempay :: Enumerate a -> Enumerate a
-mempay = mem . pay
-           
+-- | A data structure that contains a list and the reversals of all initial 
+-- segments of the list. Intuitively 
+--
+-- @reversals xs !! n = reverse (take (n+1) (fromRev xs))@
+--
+-- Any operation on a @RevList@ typically discards the reversals and constructs
+-- new reversals on demand.
+data RevList a = RevList {fromRev :: [a], reversals :: [[a]]} deriving Show
 
+instance Functor RevList where
+  fmap f = toRev. fmap f . fromRev
+
+-- Maybe this should be append instead?
+-- | Padded zip
+instance Monoid a => Monoid (RevList a) where
+  mempty         = toRev[]
+  mappend xs ys  = toRev$ zipMon (fromRev xs) (fromRev ys) where
+    zipMon :: Monoid a => [a] -> [a] -> [a]
+    zipMon (x:xs) (y:ys) = x <> y : zipMon xs ys
+    zipMon xs ys         = xs ++ ys  
+
+-- | Constructs a reversable variant of a given list. In a sensible 
+-- Haskell implementation evaluating any inital segment of 
+-- @reversals (toRevxs)@ uses linear memory in the size of the segment.
+toRev:: [a] -> RevList a
+toRev xs = RevList xs $ go [] xs where
+  go _ []       = []
+  go rev (x:xs) = let rev' = x:rev in rev' : go rev' xs
+  
+-- | Adds an  element to the head of a @RevList@. Constant memory iff the 
+-- the reversals of the resulting list are not evaluated (which is frequently 
+-- the case in @Feat@).
+revCons a = toRev. (a:) . fromRev
+
+revPure a = RevList [a] [[a]]
+
+
+
+
+
 -------------------------------------------------------
--- Polymorphic memoisation
+-- Polymorphic sharing
+
+eShare :: Typeable a => Tag -> Enumerate a -> Enumerate a
+eShare t e = e{optimiser = share t (optimiser e)}
+
+-- Automatically generates a unique tag based on the source position.
 tag :: Q Exp -- :: Tag
 tag = location >>= makeTag where
    makeTag Loc{  loc_package  = p,    
@@ -129,34 +201,63 @@
                  loc_start    = (r,c) }
        = [|Source p m r c|]
 
-tagShare :: Typeable a => Tag -> Enumerate a -> Enumerate a
-tagShare t e = e{optimal = share t (optimal e)}
-
 optimise :: Enumerate a -> Enumerate a
-optimise e = let e' = runSharing (optimal e) in
-  e'{optimal = return e'}   
+optimise e = let e' = runSharing (optimiser e) in
+  e'{optimiser = return e'}   
 
-           
+noOptim :: Enumerate a -> Enumerate a
+noOptim e = e{optimiser = return e}
+
+         
 --------------------------------------------------------
 -- Operations on finite sets
-data Finite a = Finite {fCard :: Index, fSelect :: Index -> a}
-
-finite :: Enumerate a -> Part -> Finite a
-finite e p = Finite (card e p) (select e p) 
+data Finite a = Finite {fCard :: Index, fIndex :: Index -> a}
 
-infinite :: (Part -> Finite a) -> Sharing Tag (Enumerate a) -> Enumerate a
-infinite f m = Enumerate (fCard . f) (fSelect . f) m
+finEmpty = Finite 0 (\i -> error "index: Empty")
 
 finUnion :: Finite a -> Finite a -> Finite a
-finUnion f1 f2 = Finite car sel where
+finUnion f1 f2 
+  | fCard f1 == 0  = f2
+  | fCard f2 == 0  = f1
+  | otherwise      = Finite car sel where
   car = fCard f1 + fCard f2
   sel i = if i < fCard f1
-    then fSelect f1 i
-    else fSelect f2 (i-fCard f1)  
+    then fIndex f1 i
+    else fIndex f2 (i-fCard f1)  
 
+instance Functor Finite where
+  fmap f fin = fin{fIndex = f . fIndex fin}
+
+instance Monoid (Finite a) where 
+  mempty = finEmpty
+  mappend = finUnion
+  mconcat xs = Finite
+    (sum $ map fCard xs)
+    (sumSel $ filter ((>0) . fCard) xs)
+
+sumSel :: [Finite a] -> (Index -> a)
+sumSel (f:rest) = \i -> if i < fCard f
+  then fIndex f i
+  else sumSel rest (i-fCard f)
+sumSel _        = error "Index out of bounds"
+
 finCart :: Finite a -> Finite b -> Finite (a,b)
 finCart f1 f2 = Finite car sel where
   car = fCard f1 * fCard f2
   sel i = let (q, r) = (i `quotRem` fCard f2) 
-    in (fSelect f1 q, fSelect f2 r)
- 
+    in (fIndex f1 q, fIndex f2 r)
+
+finPure :: a -> Finite a
+finPure a = Finite 1 one where
+  one 0 = a
+  one _ = error "index: index out of bounds"
+
+
+fromFinite :: Finite a -> (Index,[a])
+fromFinite (Finite c ix) = (c,map ix [0..c-1])
+
+
+instance Show a => Show (Finite a) where
+  show = show . fromFinite
+
+
diff --git a/Test/Feat/Modifiers.hs b/Test/Feat/Modifiers.hs
--- a/Test/Feat/Modifiers.hs
+++ b/Test/Feat/Modifiers.hs
@@ -59,8 +59,9 @@
 
 
 enumerateBounded :: (Enum a) => Int -> Int -> Enumerate a
-enumerateBounded from to = let e = Enumerate crd sel (return e) in e 
+enumerateBounded from to = let e = Enumerate prts (return e) in e 
   where
+    prts = toRev$ map (\p -> Finite (crd p) (sel p)) [0..]
     crd p
        | p <= 0          = 0
        | p == 1          = 1
@@ -75,7 +76,7 @@
   deriving (Typeable, Show, Eq, Ord)
 
 instance Enumerable Unicode where
-  enumerate = mempay $ fmap Unicode $ enumerateBounded 
+  enumerate = fmap Unicode $ enumerateBounded 
     (fromEnum (minBound :: Char)) 
     (fromEnum (maxBound :: Char))
 
@@ -88,7 +89,7 @@
   deriving (Typeable, Show)
 
 instance Enumerable Printable where
-  enumerate = mempay $ fmap Printable $ enumerateBounded 32 126
+  enumerate = fmap Printable $ enumerateBounded 32 126
 
 -- | Smart constructor for printable ASCII strings
 printables :: [Printable] -> String
diff --git a/examples/lambda-terms/lambdas.hs b/examples/lambda-terms/lambdas.hs
new file mode 100644
--- /dev/null
+++ b/examples/lambda-terms/lambdas.hs
@@ -0,0 +1,37 @@
+-- This module contains an enumeration of well scoped lambda terms
+
+{-#LANGUAGE DeriveDataTypeable#-}
+import Test.Feat
+import Test.Feat.Enumerate
+import Test.Feat.Access
+import Data.MemoCombinators(bits) -- From package data-memocombinators
+
+
+-- De Bruijn style lambda calculus
+data Lam = Lam Lam
+         | App Lam Lam
+         | Var Integer
+         deriving (Show,Eq,Ord, Typeable)
+
+
+enumLamPair :: Integer -> Enumerate (Lam,Lam)
+enumLamPair = bits enumLamPair' where
+  enumLamPair' n = (,) <$> enumLam n <*> enumLam n
+
+enumLam :: Integer -> Enumerate Lam
+enumLam = bits enumLam' where
+  enumLam' n = 
+    let e = consts $
+         [ App <$> e <*> e
+         , fmap Lam $ enumLam (n+1)
+         , fromParts [Finite n Var]
+         ] 
+    in e 
+
+instance Enumerable Lam where
+  enumerate = noOptim $ enumLam 0
+
+
+
+test n = take n $ values :: [(Integer,[Lam])]
+
diff --git a/examples/template-haskell/th.hs b/examples/template-haskell/th.hs
--- a/examples/template-haskell/th.hs
+++ b/examples/template-haskell/th.hs
@@ -32,11 +32,14 @@
 import Test.SmallCheck.Series hiding (Nat)
 import Test.SmallCheck
 
--- Currently both of these spit out a lot of errors. Disabling a few of the
--- buggier constructors might help.
-test_parsesAll = ioAll report_parses
-test_parsesBounded = ioBounded 10000 report_parses
+-- Currently both of these spit out a lot of errors unless we disable a few of the
+-- buggier constructors (which we have done below).
+test_parsesAll = ioAll 15 report_parses
+-- | Test (at most) 10000 values of each size up to size 100. 
+test_parsesBounded = ioBounded 10000 100 report_parses
 
+test_parsesBounded' = ioFeat (boundedWith enumerate 1000) report_parses
+
 report_parses e = case prop_parsesM e of
     Nothing -> return ()
     Just s  -> do
@@ -51,8 +54,8 @@
   E.ParseFailed _ s -> Just s
 
 
-test_cycleAll = ioAll report_cycle
-test_cycleBounded = ioBounded 10000 report_cycle
+test_cycleAll = ioAll 15 report_cycle
+test_cycleBounded = ioBounded 10000 100 report_cycle
 report_cycle e = case prop_cycle e of
     Nothing       -> return ()
     Just (ee,ex)  -> do
@@ -444,7 +447,11 @@
   series = toSerial cNameFlavour
   coseries = undefined
 
--- instance (Enumerable a, Integral a) => Enumerable (Ratio a) where
---   enumerate = consts [c1 $ funcurry (:%)]
+
+main = test_parsesBounded
+-- or test_parsesAll, but that takes much longer to find bugs
+
+eExp :: Enumerate Exp
+eExp = toSel cExp
 
 
diff --git a/testing-feat.cabal b/testing-feat.cabal
--- a/testing-feat.cabal
+++ b/testing-feat.cabal
@@ -1,20 +1,19 @@
 Name:                testing-feat
-Version:             0.2
-Synopsis:            Functional enumeration for systematic and random testing
-Description:         Feat (Functional Enumeration of Abstract Types) 
-                     provides an enumeration as a function from natural 
-                     numbers to values (similar to @toEnum@). This can be used
-                     both for SmallCheck-style systematic testing and QuickCheck 
-                     style random testing, and hybrids of the two.
+Version:             0.3
+Synopsis:            Functional Enumeration of Abstract Types
+Description:         Feat (Functional Enumeration of Abstract Types) provides
+                     enumerations as functions from natural numbers to values 
+                     (similar to @toEnum@ but for any algebraic data type). This 
+                     can be used for SmallCheck-style systematic testing, 
+                     QuickCheck style random testing, and hybrids of the two. 
                      .
                      The enumerators are defined in a very boilerplate manner
                      and there is a Template Haskell script for deriving the 
                      class instance for most types.
                      "Test.Feat" contain a subset of the other modules that 
                      should be sufficient for most test usage. There 
-                     are two (somewhat similar) large scale example in the tar 
-                     ball: testing the Template Haskell pretty printer and 
-                     testing haskell-src-exts.
+                     are some small and large example in the tar 
+                     ball.
                                           
 License:             BSD3
 License-file:        LICENSE
@@ -27,6 +26,7 @@
 Extra-source-files:  
     examples/template-haskell/th.hs
     examples/haskell-src-exts/hse.hs
+    examples/lambda-terms/lambdas.hs
 
 Cabal-version:       >=1.2
 
@@ -39,16 +39,14 @@
     Test.Feat.Class.Override,
     Test.Feat.Enumerate,
     Test.Feat.Modifiers 
-    Control.Monad.TagShare
 
   
   Build-depends: 
     base >= 4.5 && <= 5,
-    template-haskell >= 2.4 && < 2.8,
+    template-haskell >= 2.5 && < 2.8,
     mtl >= 1 && < 3,
     QuickCheck > 2 && < 3,
-    containers < 1,
-    data-memocombinators >= 0.4.2 && < 0.5
+    tagshare<0.1
     
   Other-modules:
     Test.Feat.Internals.Derive