diff --git a/app/Intro.hs b/app/Intro.hs
--- a/app/Intro.hs
+++ b/app/Intro.hs
@@ -4,31 +4,31 @@
 module Intro where
 
 import Control.Monad
-import System.Environment (getArgs)
-import Test.QuickCheck
-
 import Control.Monad.Credit
+import Test.Credit
+import Test.QuickCheck
+import Data.Tree
 
-data Batched a = Batched [a] [a]
+data Batched a m = Batched [a] [a]
   deriving (Eq, Ord, Show)
 
 rev :: MonadCount m => [a] -> [a] -> m [a]
 rev [] acc = pure acc
 rev (x : xs) acc = tick >> rev xs (x : acc)
 
-batched :: MonadCount m => [a] -> [a] -> m (Batched a)
+batched :: MonadCount m => [a] -> [a] -> m (Batched a m)
 batched [] rear = do
   front <- rev rear []
   pure $ Batched front []
 batched front rear = pure $ Batched front rear
 
-empty :: MonadCount m => m (Batched a)
+empty :: MonadCount m => m (Batched a m)
 empty = pure $ Batched [] []
 
-snoc :: MonadCount m => Batched a -> a -> m (Batched a)
+snoc :: MonadCount m => Batched a m -> a -> m (Batched a m)
 snoc   (Batched front rear) x = batched front (x : rear)
 
-uncons :: MonadCount m => Batched a -> m (Maybe (a, Batched a))
+uncons :: MonadCount m => Batched a m -> m (Maybe (a, Batched a m))
 uncons (Batched [] []) = pure Nothing
 uncons (Batched (x:front) rear) = do
   q' <- batched front rear
@@ -45,3 +45,35 @@
 testBatched =
   runCounterM $ empty >>= flip (foldM snoc) [1..10]
                       >>= unfoldM uncons
+
+data QueueOp a = Snoc a | Uncons
+  deriving (Eq, Ord, Show)
+
+instance Arbitrary a => Arbitrary (QueueOp a) where
+  arbitrary = frequency
+    [ (7, Snoc <$> arbitrary), (3, pure Uncons) ]
+
+instance (Arbitrary a, Show a)
+      => DataStructure (Batched a) (QueueOp a) where
+  create = pure $ Batched [] []
+
+  perform sz q (Snoc x) = (sz + 1,) <$> snoc q x
+  perform sz q Uncons = do
+    m <- uncons q
+    case m of
+      Nothing -> pure (sz, Batched [] [])
+      Just (_, q') -> pure (sz - 1, q')
+
+  cost n (Snoc _) = 1
+  cost n Uncons   = 0
+
+testSeq :: IO ()
+testSeq = quickCheck $ checkCredits @(Batched Int) Path
+
+genTree :: Strategy -> IO ()
+genTree s = 
+  putStrLn . drawTree . fmap show
+    =<< generate (genExecutionTrace @(QueueOp Int) s)
+
+testPar :: IO ()
+testPar = quickCheck $ checkCredits @(Batched Int) Random
diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -35,7 +35,7 @@
 import Test.Credit.RandomAccess.Zeroless
 
 run :: forall t op. (MemoryStructure t, DataStructure t op) => Args -> Strategy -> IO Result
-run args strat = quickCheckWithResult args $ checkCreditsMemory @t strat
+run args strat = quickCheckWithResult args $ checkCreditsTrace @t strat
 
 newtype Alpha = Alpha Char
   deriving (Eq, Ord)
diff --git a/app/Stack.hs b/app/Stack.hs
deleted file mode 100644
--- a/app/Stack.hs
+++ /dev/null
@@ -1,61 +0,0 @@
-module Stack where
-
-fn :: Int -> (a -> a) -> a -> a
-fn 0 f x = x
-fn n f x = fn (n - 1) f (f x)
-
-suc :: Int -> Int
-suc n = n + 1
-
-exp1 :: Int -> Int -> Int
-exp1 m n = fn m (fn n) suc 0
-
---
-
-data Fun b = Unit (b -> b) | Rec (Fun b) (Fun b -> b -> b)
-
-call :: Fun b -> b -> b
-call (Unit f) x = f x
-call (Rec env f) x = f env x
-
-fn' :: Int -> Fun b -> b -> b
-fn' 0 f x = x
-fn' n f x = fn' (n - 1) f (call f x)
-
-fn1 :: Int -> Fun b -> Fun b
-fn1 n f = Rec f (fn' n)
-
-exp2 :: Int -> Int -> Int
-exp2 m n = call (fn' m (Unit (fn1 n)) (Unit suc)) 0
-
---
-
-data Closure b where
-  Exists :: a -> (a -> b -> b) -> Closure b
-
-callC :: Closure b -> b -> b
-callC (Exists x f) y = f x y
-
-fnC :: Int -> Closure b -> b -> b
-fnC 0 c x = x
-fnC n c x = fnC (n - 1) c (callC c x)
-
-fnC1 :: Int -> Closure b -> Closure b
-fnC1 n c = Exists c (fnC n)
-
-fnC1' :: Int -> () -> Closure b -> Closure b
-fnC1' n () c = fnC1 n c
-
-sucC :: () -> Int -> Int
-sucC () n = n + 1
-
-exp3 :: Int -> Int -> Int
-exp3 m n = callC (fnC m (Exists () (fnC1' n)) (Exists () sucC)) 0
-
---
-
--- type Closure b c = ... | Fn (type of env) (type of env -> b -> c) | ...
--- [[\x.^n e]] = (fn, env) where
---   fn env x = [[e]]
---   env = "free vars in [[e]]"
-
diff --git a/creditmonad.cabal b/creditmonad.cabal
--- a/creditmonad.cabal
+++ b/creditmonad.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           creditmonad
-version:        1.0.0
+version:        1.1.0
 synopsis:       Reasoning about amortized time complexity
 description:    Persistent data structures are ubiquitous in functional
                 programming languages and their designers frequently have to
@@ -72,7 +72,7 @@
       Control.Monad.Credit.CounterM
   hs-source-dirs:
       src
-  ghc-options: -Wall -Wno-name-shadowing
+  ghc-options: -Wall -Wno-name-shadowing -Wno-unused-matches
   build-depends:
       QuickCheck >=2.14 && <3
     , STMonadTrans ==0.4.*
@@ -87,10 +87,9 @@
   other-modules:
       Implicit
       Intro
-      Stack
   hs-source-dirs:
       app
-  ghc-options: -Wall -Wno-name-shadowing -O2 -fworker-wrapper-cbv -threaded -rtsopts
+  ghc-options: -Wall -Wno-name-shadowing -Wno-unused-matches -O2 -fworker-wrapper-cbv -threaded -rtsopts
   build-depends:
       QuickCheck >=2.14 && <3
     , STMonadTrans ==0.4.*
diff --git a/src/Control/Monad/Credit.hs b/src/Control/Monad/Credit.hs
--- a/src/Control/Monad/Credit.hs
+++ b/src/Control/Monad/Credit.hs
@@ -2,15 +2,15 @@
 
 module Control.Monad.Credit 
   (
-  -- * Computations with credits
+  -- * Computations with Credits
     Control.Monad.Credit.Base.MonadCount(..), Control.Monad.Credit.Base.MonadLazy (..), Control.Monad.Credit.Base.HasStep(..), Control.Monad.Credit.Base.Lazy(..)
-  , Control.Monad.Credit.Base.Ticks, Control.Monad.Credit.Base.Credit, Control.Monad.Credit.Base.MonadCredit(..), Control.Monad.Credit.Base.MonadInherit(..)
+  , Control.Monad.Credit.Base.Credit, Control.Monad.Credit.Base.MonadCredit(..), Control.Monad.Credit.Base.MonadInherit(..)
   -- * Counter Monad
-  , Control.Monad.Credit.CounterM.CounterM, Control.Monad.Credit.CounterM.runCounterM, Control.Monad.Credit.CounterM.CounterT, Control.Monad.Credit.CounterM.runCounterT
+  , Control.Monad.Credit.Base.Ticks, Control.Monad.Credit.CounterM.CounterM, Control.Monad.Credit.CounterM.runCounterM, Control.Monad.Credit.CounterM.CounterT, Control.Monad.Credit.CounterM.runCounterT
   -- * Credit Monad
   , Control.Monad.Credit.CreditM.CreditM, Control.Monad.Credit.CreditM.runCreditM, Control.Monad.Credit.CreditM.CreditT, Control.Monad.Credit.CreditM.runCreditT
   , Control.Monad.Credit.CreditM.Error(..), Control.Monad.Credit.Base.Cell
-  -- * Pretty-printing memory cells
+  -- * Pretty-Printing Memory Cells
   , Control.Monad.Credit.Base.Memory, Control.Monad.Credit.Base.mkMCell, Control.Monad.Credit.Base.mkMList, linearize
   , Control.Monad.Credit.Base.MemoryCell(..), Control.Monad.Credit.Base.MonadMemory(..), Control.Monad.Credit.Base.PrettyCell(..), Control.Monad.Credit.Base.MemoryStructure(..)
   ) where
diff --git a/src/Control/Monad/Credit/Base.hs b/src/Control/Monad/Credit/Base.hs
--- a/src/Control/Monad/Credit/Base.hs
+++ b/src/Control/Monad/Credit/Base.hs
@@ -39,6 +39,8 @@
   data Thunk m :: (Type -> Type) -> Type -> Type
   delay :: t a -> m (Thunk m t a)
   -- ^ delay creates a new cell with the given thunk
+  value :: a -> m (Thunk m t a)
+  -- ^ value creates a new cell with the given value
   force :: HasStep t m => Thunk m t a -> m a
   -- ^ force retrieves and evaluates the thunk of a cell
   lazymatch :: Thunk m t a -> (a -> m b) -> (t a -> m b) -> m b
@@ -51,7 +53,7 @@
 
 -- | A basic thunk that contains the computation to be evaluated.
 -- This type can be used to express any thunk but its disadvantage is that
--- it will be printed merely as "<lazy>".
+-- its content cannot be inspected.
 newtype Lazy m a = Lazy (m a)
 
 instance HasStep (Lazy m) m where
@@ -108,7 +110,7 @@
 instance Monad m => MemoryCell m (Lazy m a) where
   prettyCell (Lazy _) = pure $ mkMCell "<lazy>" []
 
-class Monad m => MonadMemory m where
+class MonadLazy m => MonadMemory m where
   prettyThunk :: (MemoryCell m a, MemoryCell m (t a)) => Thunk m t a -> m Memory
 
 instance (MonadMemory m, MemoryCell m a, MemoryCell m (t a)) => MemoryCell m (Thunk m t a) where
diff --git a/src/Control/Monad/Credit/CounterM.hs b/src/Control/Monad/Credit/CounterM.hs
--- a/src/Control/Monad/Credit/CounterM.hs
+++ b/src/Control/Monad/Credit/CounterM.hs
@@ -66,6 +66,9 @@
   delay a = do
     s <- liftST $ newSTRef (Left a)
     pure (Thunk s)
+  value b = do
+    s <- liftST $ newSTRef (Right b)
+    pure (Thunk s)
   force (Thunk t) = do
     t' <- liftST $ readSTRef t
     case t' of
diff --git a/src/Control/Monad/Credit/CreditM.hs b/src/Control/Monad/Credit/CreditM.hs
--- a/src/Control/Monad/Credit/CreditM.hs
+++ b/src/Control/Monad/Credit/CreditM.hs
@@ -3,10 +3,12 @@
 module Control.Monad.Credit.CreditM (CreditM, Error(..), runCreditM, CreditT, runCreditT, resetCurrentThunk) where
 
 import Prelude hiding (lookup)
+import Control.Monad
 import Control.Monad.Except
 import Control.Monad.Identity
 import Control.Monad.State.Lazy
 import Control.Monad.ST.Trans
+import Data.Either
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.IntMap (IntMap)
@@ -172,6 +174,11 @@
     withCredits $ pure . open i
     s <- liftST $ newSTRef (Left a)
     pure (Thunk i s)
+  value b = do
+    i <- getNext
+    withCredits $ pure . open i
+    s <- liftST $ newSTRef (Right b)
+    pure (Thunk i s)
   force (Thunk i t) = do
     t' <- liftST $ readSTRef t
     case t' of
@@ -212,8 +219,10 @@
       me <- getMe
       withCredits $ subCredit me n . addCredit i n
     else pure ()
-  hasAtLeast (Thunk i _) n =
-    assertAtLeast i n
+  hasAtLeast (Thunk i t) n = do
+    t' <- liftST $ readSTRef t
+    when (isLeft t') $ do
+      assertAtLeast i n
 
 instance Monad m => MonadInherit (CreditT s m) where
   {-# SPECIALIZE instance MonadInherit (CreditT s Identity) #-}
@@ -265,7 +274,7 @@
   pretty (OutOfCredits i) = "Out of credits for" <+> pretty i
   pretty (InvalidAccount i) = "Invalid account for" <+> pretty i
   pretty (InvalidTick i) = "Invalid tick for" <+> pretty i
-  pretty (ClosedCurrent (Cell 0)) = "Closed maint thread account. Never invoke creditAllTo on main thread."
+  pretty (ClosedCurrent (Cell 0)) = "Closed main thread account. Never invoke creditAllTo on main thread."
   pretty (ClosedCurrent i) = "Closed current account" <+> pretty i
   pretty (UserError e) = "User error:" <+> pretty e
   pretty (AssertionFailed i n m) = pretty i <+> "should have" <+> pretty n <+> "credits but only has" <+> pretty m
diff --git a/src/Test/Credit.hs b/src/Test/Credit.hs
--- a/src/Test/Credit.hs
+++ b/src/Test/Credit.hs
@@ -2,12 +2,14 @@
 
 module Test.Credit
   (
-  -- * Common time-complexity functions
+  -- * Common Time-Complexity Functions
     Size, logstar, log2, linear
-  -- * Tree shapes for testing
-  , Strategy(..), genTree
-  -- * Testing data structures on trees of operations
-  , DataStructure(..), runTree, checkCredits, runTreeMemory, checkCreditsMemory
+  -- * Execution Traces for Testing
+  , Strategy(..), genExecutionTrace
+  -- * Running Data Structures on Execution Traces
+  , DataStructure(..), runTree, runTreeTrace
+  -- * Testing Data Structures on Execution Traces
+  , checkCredits, checkCreditsTrace
   ) where
 
 import Data.Either
@@ -70,11 +72,11 @@
 data Strategy = Path | Bloom | Pennant | Random
   deriving (Eq, Ord, Show)
 
-genTree :: Arbitrary op => Strategy -> Gen (Tree op)
-genTree Path = fromSeqTree <$> arbitrary
-genTree Bloom = fromBloomTree <$> arbitrary
-genTree Pennant = fromPennantTree <$> arbitrary
-genTree Random = fromPrsTree <$> arbitrary
+genExecutionTrace :: Arbitrary op => Strategy -> Gen (Tree op)
+genExecutionTrace Path = fromSeqTree <$> arbitrary
+genExecutionTrace Bloom = fromBloomTree <$> arbitrary
+genExecutionTrace Pennant = fromPennantTree <$> arbitrary
+genExecutionTrace Random = fromPrsTree <$> arbitrary
 
 newtype Size = Size Int
   deriving (Eq, Ord, Show)
@@ -102,27 +104,41 @@
 linear (Size n) = fromInteger $ toInteger n
 
 class (Arbitrary op, Show op) => DataStructure t op | t -> op where
-  create :: forall m. MonadInherit m => t m
-  action :: forall m. MonadInherit m => t m -> op -> (Credit, m (t m))
+  cost :: Size -> op -> Credit
+  -- ^ Given a size and an operation, return the cost of the operation.
+  -- This function can not inspect the internal state of the data structure.
+  create :: MonadLazy m => m (t m)
+  -- ^ create a new instance of the data structure.
+  -- We allow the computation to be lazy, since lazy data structures
+  -- often contain thunks even if they contain no elements.
+  -- The create data structure is assumed to have size zero.
+  perform :: MonadInherit m => Size -> t m -> op -> m (Size, t m)
+  -- ^ Given a data structure, its size, and an operation,
+  -- return the updated size and data structure.
+  -- We allow the size to depend on the internal state of the data structure,
+  -- since some operations, like insertions into a binary search tree, might
+  -- return different sizes depending on whether a new element is already present.
 
+-- | Evaluate an execution trace of operations on the given data structure
+-- using the credit monad. Returns either an error or unit if the evaluation succeeded.
 runTree :: forall t op. DataStructure t op => Tree op -> Either Error ()
-runTree tree = runCreditM 0 (go (create @t) tree)
+runTree tree = runCreditM 0 (create @t >>= flip (go 0) tree)
   where
-    go :: forall s t op. DataStructure t op => t (CreditM s) -> Tree op -> CreditM s ()
-    go a (Node op ts) = do
-      let (cr, f) = action a op
+    go :: forall s t op. DataStructure t op => Size -> t (CreditM s) -> Tree op -> CreditM s ()
+    go sz a (Node op ts) = do
+      let cr = cost @t sz op
       resetCurrentThunk cr
-      a' <- f
-      mapM_ (go a') ts
+      (sz, a) <- perform sz a op
+      mapM_ (go sz a) ts
 
 isPersistent :: Tree a -> Bool
 isPersistent (Node _ ts) = length ts > 1 || any isPersistent ts
 
--- | Evaluate the queue operations using the given strategy on the given queue
--- Reports only if evaluation succeeded.
+-- | Test the given data structure in the credit monad using the given strategy.
+-- This property only reports if evaluation succeeded or not.
 checkCredits :: forall t op. DataStructure t op => Strategy -> Property
 checkCredits strat =
-  forAllShrink (genTree strat) shrink $ \t ->
+  forAllShrink (genExecutionTrace strat) shrink $ \t ->
     classify (isPersistent t) "persistent" $
       isRight $ runTree @t t
 
@@ -141,6 +157,10 @@
 extract (Branch x ls Root) = Node x (reverse ls)
 extract z = extract (up z)
 
+-- | If each node has only a single child, flatten the tree
+-- by making all elements children of the root.
+-- This improves the readability of the tree when printed.
+-- Otherwise, return the original tree.
 flattenTree :: Tree a -> Tree a
 flattenTree t = case go t of
   Just (x:xs) -> Node x (map (\x -> Node x []) xs)
@@ -156,25 +176,29 @@
 
 type M s = CreditT s (State (RoseZipper String))
 
-runTreeMemory :: forall t op. (MemoryStructure t, DataStructure t op) => Tree op -> String
-runTreeMemory tree = showState $ runState (runCreditT 0 (go (create @t) tree)) Root
+-- | Evaluate an execution trace of operations on the given data structure
+-- using the credit monad. Returns a pretty-printed string of the execution trace
+-- annotated with the internal state of the data structure at each step.
+runTreeTrace :: forall t op. (MemoryStructure t, DataStructure t op) => Tree op -> String
+runTreeTrace tree = showState $ runState (runCreditT 0 (create @t >>= flip (go 0) tree)) Root
   where
-    go :: forall s t op. (MemoryStructure t, DataStructure t op) => t (M s) -> Tree op -> M s ()
-    go a (Node op ts) = do
-      let (cr, f) = action a op
+    go :: forall s t op. (MemoryStructure t, DataStructure t op) => Size -> t (M s) -> Tree op -> M s ()
+    go sz a (Node op ts) = do
+      let cr = cost @t sz op
       resetCurrentThunk cr
       lift $ modify' (Branch (show op ++ ": ") []) 
-      a' <- f
-      mem <- prettyStructure a'
+      (sz, a) <- perform sz a op
+      mem <- prettyStructure a
       let s = renderString $ layoutSmart (defaultLayoutOptions { layoutPageWidth = Unbounded }) $ nest 2 $ pretty $ mem
       lift $ modify' (extend s)
-      mapM_ (go a') ts
+      mapM_ (go sz a) ts
       lift $ modify' up
 
--- | Evaluate the queue operations using the given strategy on the given queue
--- Reports only if evaluation succeeded.
-checkCreditsMemory :: forall t op. (MemoryStructure t, DataStructure t op) => Strategy -> Property
-checkCreditsMemory strat =
-  forAllShrinkShow (genTree strat) shrink (\t -> runTreeMemory @t t) $ \t ->
+-- | Test the given data structure in the credit monad using the given strategy.
+-- If evaluation fails, this property prints the execution trace
+-- annotated with the internal state of the data structure at each step.
+checkCreditsTrace :: forall t op. (MemoryStructure t, DataStructure t op) => Strategy -> Property
+checkCreditsTrace strat =
+  forAllShrinkShow (genExecutionTrace strat) shrink (\t -> runTreeTrace @t t) $ \t ->
     classify (isPersistent t) "persistent" $
       isRight $ runTree @t t
diff --git a/src/Test/Credit/Deque/Base.hs b/src/Test/Credit/Deque/Base.hs
--- a/src/Test/Credit/Deque/Base.hs
+++ b/src/Test/Credit/Deque/Base.hs
@@ -20,7 +20,7 @@
     ]
 
 class Deque q where
-  empty :: MonadInherit m => m (q a m)
+  empty :: MonadLazy m => m (q a m)
   cons :: MonadInherit m => a -> q a m -> m (q a m)
   snoc :: MonadInherit m => q a m -> a -> m (q a m)
   uncons :: MonadInherit m => q a m -> m (Maybe (a, q a m))
@@ -30,39 +30,32 @@
 class Deque q => BoundedDeque q where
   qcost :: Size -> DequeOp a -> Credit
 
-data D q a m = E | D Size (q (PrettyCell a) m)
+data D q a m = D (q (PrettyCell a) m)
 
 instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (D q a m) where
-  prettyCell E = pure $ mkMCell "" []
-  prettyCell (D _ q) = prettyCell q
+  prettyCell (D q) = prettyCell q
 
 instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (D q a) where
-  prettyStructure E = pure $ mkMCell "" []
-  prettyStructure (D _ q) = prettyStructure q
+  prettyStructure (D q) = prettyStructure q
 
-act :: (MonadInherit m, Deque q) => Size -> q (PrettyCell a) m -> DequeOp a -> m (D q a m)
-act sz q (Cons x) = D (sz + 1) <$> cons (PrettyCell x) q
-act sz q (Snoc x) = D (sz + 1) <$> snoc q (PrettyCell x)
-act sz q Uncons = do
-  m <- uncons q
-  case m of
-    Nothing -> pure E
-    Just (_, q') -> pure $ D (max 0 (sz - 1)) q'
-act sz q Unsnoc = do
-  m <- unsnoc q
-  case m of
-    Nothing -> pure E
-    Just (q', _) -> pure $ D (max 0 (sz - 1)) q'
-act sz q Concat = pure $ D sz q
 
 instance (Arbitrary a, BoundedDeque q, Show a) => DataStructure (D q a) (DequeOp a) where
-  create = E
-  action E op = (qcost @q 0 op, empty >>= flip (act 0) op)
-  action (D sz q) op = (qcost @q sz op, act sz q op)
-
-size :: D q a m -> Size
-size E = 0
-size (D sz _) = sz
+  cost _ Concat = 0
+  cost sz op = qcost @q sz op
+  create = D <$> empty
+  perform sz (D q) (Cons x) = (sz + 1,) <$> D <$> cons (PrettyCell x) q
+  perform sz (D q) (Snoc x) = (sz + 1,) <$> D <$> snoc q (PrettyCell x)
+  perform sz (D q) Uncons = do
+    m <- uncons q
+    case m of
+      Nothing -> (sz,) <$> D <$> empty
+      Just (_, q') -> pure (sz - 1, D q')
+  perform sz (D q) Unsnoc = do
+    m <- unsnoc q
+    case m of
+      Nothing -> (sz,) <$> D <$> empty
+      Just (q', _) -> pure (sz - 1, D q')
+  perform sz (D q) Concat = pure $ (sz, D q) -- no op
 
 data BD q a m = BD (D q a m) (D q a m)
 
@@ -78,33 +71,25 @@
     q2' <- prettyStructure q2
     pure $ mkMCell "Concat" [q1', q2']
 
-act1 :: (MonadInherit m, Deque q) => DequeOp a -> BD q a m -> m (BD q a m)
-act1 op (BD q1 q2) = do
-  q1' <- case q1 of
-    E -> empty
-    D _ q -> pure q
-  q1'' <- act (size q1) q1' op 
-  pure $ BD q1'' q2
-
-act2 :: (MonadInherit m, Deque q) => DequeOp a -> BD q a m -> m (BD q a m)
-act2 op (BD q1 q2) = do
-  let sz = size q2
-  q2' <- case q2 of
-    E -> empty
-    D _ q -> pure q
-  q2'' <- act (size q2) q2' op 
-  pure $ BD q1 q2''
-
-concatenate :: (MonadInherit m, Deque q) => D q a m -> D q a m -> m (D q a m)
-concatenate E E = pure E
-concatenate (D sz1 q1) E = pure $ D sz1 q1
-concatenate E (D sz2 q2) = pure $ D sz2 q2
-concatenate (D sz1 q1) (D sz2 q2) = D (sz1 + sz2) <$> concat q1 q2
-
 instance (Arbitrary a, BoundedDeque q, Show a) => DataStructure (BD q a) (DequeOp a) where
-  create = BD E E
-  action (BD q1 q2) (Cons x) = (qcost @q (size q1) (Cons x), act1 (Cons x) (BD q1 q2))
-  action (BD q1 q2) (Snoc x) = (qcost @q (size q2) (Snoc x), act2 (Snoc x) (BD q1 q2))
-  action (BD q1 q2) Uncons = (qcost @q (size q1) Uncons, act1 Uncons (BD q1 q2))
-  action (BD q1 q2) Unsnoc = (qcost @q (size q2) Unsnoc, act2 Unsnoc (BD q1 q2))
-  action (BD q1 q2) Concat = (qcost @q (size q1 + size q2) Concat, BD E <$> concatenate q1 q2)
+  cost = qcost @q
+  create = do
+    q1 <- empty
+    q2 <- empty
+    pure $ BD (D q1) (D q2)
+  perform sz (BD q1 q2) (Cons x) = do
+    (sz, q1) <- perform sz q1 (Cons x)
+    pure (sz, BD q1 q2)
+  perform sz (BD q1 q2) (Snoc x) = do
+    (sz, q2) <- perform sz q2 (Snoc x)
+    pure (sz, BD q1 q2)
+  perform sz (BD q1 q2) Uncons = do
+    (sz, q1) <- perform sz q1 Uncons
+    pure (sz, BD q1 q2)
+  perform sz (BD q1 q2) Unsnoc = do
+    (sz, q2) <- perform sz q2 Unsnoc
+    pure (sz, BD q1 q2)
+  perform sz (BD (D q1) (D q2)) Concat = do
+    e <- empty
+    q <- concat q1 q2
+    pure (sz, BD (D e) (D q))
diff --git a/src/Test/Credit/Deque/Catenable.hs b/src/Test/Credit/Deque/Catenable.hs
--- a/src/Test/Credit/Deque/Catenable.hs
+++ b/src/Test/Credit/Deque/Catenable.hs
@@ -16,11 +16,9 @@
       (Q.BQueue (Thunk m (CLazyCon m) (CatDeque a m)) m) -- ^ tail
 
 data CLazyCon m a where
-  Pure :: a -> CLazyCon m a
   LinkAll :: Q.BQueue (Thunk m (CLazyCon m) (CatDeque a m)) m -> CLazyCon m (CatDeque a m)
 
 instance MonadInherit m => HasStep (CLazyCon m) m where
-  step (Pure xs) = pure xs
   step (LinkAll q) = linkAll q
 
 costSnoc :: Credit
@@ -49,7 +47,7 @@
 concat' E xs = pure xs
 concat' xs E = pure xs
 concat' xs ys = do
-  ys <- delay $ Pure ys
+  ys <- value ys
   link xs ys
 
 -- | Assign credits to the thunk and force it
@@ -59,14 +57,12 @@
 dischargeThunk s = do
   let assign = creditWith s (costSnoc + costUncons) >> force s >> pure ()
   lazymatch s (\_ -> assign) $ \case
-    Pure _ -> assign
     LinkAll q -> do
       q' <- Q.lazyqueue q
       case q' of
         [] -> assign
         t' : _ -> do
           lazymatch t' (\_ -> assign) $ \case
-            Pure _ -> assign
             LinkAll _ -> dischargeThunk t'
 
 findFirstThunk :: MonadInherit m => CatDeque a m -> m (Maybe (Thunk m (CLazyCon m) (CatDeque a m)))
@@ -79,7 +75,6 @@
 seekFirstThunk [] = pure Nothing
 seekFirstThunk (t : q) = do
   mt <- lazymatch t findFirstThunk $ \case
-    Pure q' -> findFirstThunk q'
     LinkAll _ -> pure $ Just t
   case mt of
     Nothing -> seekFirstThunk q
@@ -114,12 +109,9 @@
   qcost _ (Snoc _) = costSnoc
   qcost _ Uncons = 4 * costUncons + 3 * costSnoc
   qcost _ Unsnoc = 0
-  qcost _ Concat = 0
+  qcost _ Concat = costSnoc
 
 instance (MonadMemory m, MemoryCell m a) => MemoryCell m (CLazyCon m a) where
-  prettyCell (Pure x) = do
-    x' <- prettyCell x
-    pure $ mkMCell "Pure" [x']
   prettyCell (LinkAll q) = do
     q' <- prettyCell q
     pure $ mkMCell "LinkAll" [q']
diff --git a/src/Test/Credit/Deque/ImplicitCat.hs b/src/Test/Credit/Deque/ImplicitCat.hs
--- a/src/Test/Credit/Deque/ImplicitCat.hs
+++ b/src/Test/Credit/Deque/ImplicitCat.hs
@@ -4,7 +4,6 @@
 import Control.Monad (join, when)
 import Prettyprinter (Pretty)
 import Control.Monad.Credit
-import Test.Credit
 import Test.Credit.Deque.Base
 import qualified Test.Credit.Deque.Base as D
 import qualified Test.Credit.Deque.Bankers as D
diff --git a/src/Test/Credit/Deque/SimpleCat.hs b/src/Test/Credit/Deque/SimpleCat.hs
--- a/src/Test/Credit/Deque/SimpleCat.hs
+++ b/src/Test/Credit/Deque/SimpleCat.hs
@@ -4,7 +4,7 @@
 import Prettyprinter (Pretty)
 import Control.Monad
 import Control.Monad.Credit
-import Test.Credit
+import Test.Credit (log2)
 import Test.Credit.Deque.Base
 import qualified Test.Credit.Deque.Base as D
 import qualified Test.Credit.Deque.Bankers as D
@@ -184,7 +184,7 @@
   qcost n (Snoc x) = qcost @(D.BDeque) n (Snoc x)
   qcost n Uncons = 1 + qcost @(D.BDeque) n Uncons + 2 * cost
   qcost n Unsnoc = 1 + qcost @(D.BDeque) n Unsnoc + 2 * cost
-  qcost n Concat = (1 + 6 * cost) * log2 n
+  qcost n Concat = cost + (1 + 6 * cost) * log2 n
 
 instance (MonadMemory m, MemoryCell m a) => MemoryCell m (SimpleCat a m) where
   prettyCell (Shallow d) = do
diff --git a/src/Test/Credit/Finger.hs b/src/Test/Credit/Finger.hs
--- a/src/Test/Credit/Finger.hs
+++ b/src/Test/Credit/Finger.hs
@@ -1,10 +1,8 @@
-{-# LANGUAGE GADTs, OverloadedLists, LambdaCase #-}
+{-# LANGUAGE GADTs, LambdaCase #-}
 
 module Test.Credit.Finger where
 
 import Prelude hiding (head, tail, last, init)
-import Data.List.NonEmpty (NonEmpty(..), (<|))
-import qualified Data.List.NonEmpty as NE
 import Control.Monad (when, unless)
 import Data.Foldable (foldlM, foldrM)
 import Prettyprinter (Pretty)
@@ -25,17 +23,15 @@
 data FingerTree v a m
   = Empty
   | Single a
-  | Deep (Thunk m (Lazy m) v) (Digit a) (Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m)) (Digit a)
+  | Deep v (Digit a) (Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m)) (Digit a)
 
 data FLazyCon m a where
-  FPure :: a -> FLazyCon m a
   FCons :: Measured a v => a -> Thunk m (FLazyCon m) (FingerTree v a m) -> FLazyCon m (FingerTree v a m)
   FSnoc :: Measured a v => Thunk m (FLazyCon m) (FingerTree v a m) -> a -> FLazyCon m (FingerTree v a m)
   FTail :: Measured a v => FingerTree v a m -> FLazyCon m (FingerTree v a m)
   FInit :: Measured a v => FingerTree v a m -> FLazyCon m (FingerTree v a m)
 
 instance MonadCredit m => HasStep (FLazyCon m) m where
-  step (FPure xs) = pure xs
   step (FCons x m) = cons x =<< force m
   step (FSnoc m x) = flip snoc x =<< force m
   step (FTail q) = tail q
@@ -49,39 +45,44 @@
 --  - snoc and tail spend their second credit on either the old m to be able to force it,
 --    or on the new m to maintain the invariant.
 
-class Monoid v => Measured a v where
+class (Eq v, Monoid v) => Measured a v where
   measure :: a -> v
 
-instance Measured a v => Measured [a] v where
-  measure = mconcat . map measure
+instance (Eq v, Monoid v) => Measured (Tuple v a) v where
+  measure (Pair v _ _) = v
+  measure (Triple v _ _ _) = v
 
 instance Measured a v => Measured (Digit a) v where
   measure = measure . toList
 
-instance Monoid v => Measured (Tuple v a) v where
-  measure (Pair v _ _) = v
-  measure (Triple v _ _ _) = v
+instance Measured a v => Measured [a] v where
+  measure = mconcat . map measure
 
-measurement :: (MonadCredit m, Measured a v) => FingerTree v a m -> m v
-measurement Empty = pure $ mempty
-measurement (Single x) = pure $ measure x
-measurement (Deep vm f m r) = do
-  vm' <- force vm
-  pure $ measure f <> vm' <> measure r
+instance (Measured a v, Measured b v) => Measured (a, b) v where
+  measure (x, y) = measure x <> measure y
 
-forceAll :: (MonadCredit m, Measured a v) => FingerTree v a m -> m ()
-forceAll Empty = pure ()
-forceAll (Single _) = pure ()
-forceAll (Deep _ _ m _) = do
-  creditWith m 2
-  forceAll =<< force m
+instance (Measured a v, Measured b v, Measured c v) => Measured (a, b, c) v where
+  measure (x, y, z) = measure x <> measure y <> measure z
 
+instance (Measured a v, Measured b v) => Measured (Either a b) v where
+  measure (Left x) = measure x
+  measure (Right y) = measure y
+
+instance Measured a v => Measured (Maybe a) v where
+  measure Nothing = mempty
+  measure (Just a) = measure a
+
+instance Measured a v => Measured (FingerTree v a m) v where
+  measure Empty = mempty
+  measure (Single x) = measure x
+  measure (Deep vm f m r) = measure f <> vm <> measure r
+
 isTwo :: Digit a -> Bool
 isTwo (Two _ _) = True
 isTwo _ = False
 
 empty :: MonadCredit m => m (Thunk m (FLazyCon m) (FingerTree v a m))
-empty = delay $ FPure Empty
+empty = value $ Empty
 
 pair :: Measured a v => a -> a -> Tuple v a
 pair x y = Pair (measure x <> measure y) x y
@@ -89,20 +90,16 @@
 triple :: Measured a v => a -> a -> a -> Tuple v a
 triple x y z = Triple (measure x <> measure y <> measure z) x y z
 
-deep :: (MonadCredit m, Measured a v) => Thunk m (Lazy m) v -> Digit a -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> Digit a -> m (FingerTree v a m)
+deep :: (MonadCredit m, Measured a v) => v -> Digit a -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> Digit a -> m (FingerTree v a m)
 deep v f m r = do
-  let oneIfDangerous d = if isTwo d then 0 else 1
-  mIsPure <- lazymatch m (\_ -> pure True) $ \case
-    FPure _ -> pure True
-    _ -> pure False
-  unless mIsPure $
-    m `hasAtLeast` (oneIfDangerous f + oneIfDangerous r)
+  let dang d = if isTwo d then 0 else 1
+  m `hasAtLeast` (dang f + dang r)
+  lazymatch m (\m -> when (v /= measure m) $ error "invalid measure") (\_ -> pure ())
   pure $ Deep v f m r
 
-deep' :: (MonadCredit m, Measured a v) => Digit a -> m (Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m)) -> Digit a -> m (FingerTree v a m)
-deep' f mkM r = do
+deep' :: (MonadCredit m, Measured a v) => v -> Digit a -> m (Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m)) -> Digit a -> m (FingerTree v a m)
+deep' vm f mkM r = do
   m <- mkM
-  vm <- delay $ Lazy $ measurement =<< force m
   deep vm f m r
 
 isEmpty :: FingerTree v a m -> Bool
@@ -117,68 +114,90 @@
 toTree :: (MonadCredit m, Measured a v) => [a] -> m (FingerTree v a m)
 toTree [] = pure Empty
 toTree [x] = pure $ Single x
-toTree [x,y] = deep' (One x) empty (One y)
-toTree [x,y,z] = deep' (Two x y) empty (One z)
+toTree [x,y] = deep' mempty (One x) empty (One y)
+toTree [x,y,z] = deep' mempty (Two x y) empty (One z)
 
 toDigit :: Tuple v a -> Digit a
 toDigit (Pair _ x y) = Two x y
 toDigit (Triple _ x y z) = Three x y z
 
 cons :: (MonadCredit m, Measured a v) => a -> FingerTree v a m -> m (FingerTree v a m)
-cons x q = tick >> cons' x q
-
-cons' :: (MonadCredit m, Measured a v) => a -> FingerTree v a m -> m (FingerTree v a m)
-cons' x Empty = pure $ Single x
-cons' x (Single y) = do
-  deep' (One x) empty (One y)
-cons' x (Deep vq pr q u) = case pr of
-  One y       -> deep vq (Two x y) q u
-  Two y z     -> creditWith q 1 >> pure (Deep vq (Three x y z) q u)
-  Three y z w -> do
-    q' <- delay $ FCons (pair z w) q
-    if isTwo u
-      then creditWith q 1
-      else creditWith q' 1
-    vq' <- delay $ Lazy $ measurement =<< force q'
-    deep vq' (Two x y) q' u
+cons x q = do
+  tick
+  case q of
+    Empty -> pure $ Single x
+    Single y -> do
+      deep' mempty (One x) empty (One y)
+    Deep vq (One y) q u -> do
+      deep vq (Two x y) q u
+    Deep vq (Two y z) q u -> do
+      q `creditWith` 1
+      deep vq (Three x y z) q u
+    Deep vq (Three y z w) q u -> do
+      q' <- delay $ FCons (pair z w) q
+      if isTwo u
+        then q  `creditWith` 1
+        else q' `creditWith` 1
+      deep (measure (z, w) <> vq) (Two x y) q' u
 
 head :: MonadCredit m => FingerTree v a m -> m a
 head Empty = fail "head: empty queue"
 head (Single x) = pure x
 head (Deep _ s _ _) = pure $ let (h:_) = toList s in h
 
-tail :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (FingerTree v a m)
-tail Empty = tick >> pure Empty
-tail (Single _) = tick >> pure Empty
-tail (Deep vq (Three _ x y) q u) = tick >> pure (Deep vq (Two x y) q u)
-tail (Deep vq (Two _ x) q u) = tick >> creditWith q 1 >> pure (Deep vq (One x) q u)
-tail (Deep _ (One _) q u) = tick >> do
-  when (isTwo u) $ creditWith q 1
-  q' <- force q
-  deep0 q' u
+tail :: (MonadCredit m, Measured a v)
+     => FingerTree v a m -> m (FingerTree v a m)
+tail q = do
+  tick
+  case q of
+    Empty -> pure Empty
+    Single _ -> pure Empty
+    Deep vq (Three _ x y) q u -> do
+      deep vq (Two x y) q u
+    Deep vq (Two _ x) q u -> do
+      q `creditWith` 1
+      deep vq (One x) q u
+    Deep _ (One _) q u -> do
+      when (isTwo u) $ q `creditWith` 1
+      force q >>= (`deep0` u)
 
-deep0 :: (MonadCredit m, Measured a v) => FingerTree v (Tuple v a) m -> Digit a -> m (FingerTree v a m)
-deep0 Empty s = toTree $ toList s
+deep0 :: (MonadCredit m, Measured a v)
+      => FingerTree v (Tuple v a) m -> Digit a
+      -> m (FingerTree v a m)
+deep0 Empty u = toTree $ toList u
 deep0 q u = do
-  h <- head q
-  case h of
+  hd <- head q
+  case hd of
     Pair _ x y -> do
       t <- delay $ FTail q
-      unless (isTwo u) $ creditWith t 1
-      vt <- delay $ Lazy $ measurement =<< force t
-      deep vt (Two x y) t u
+      unless (isTwo u) $ t `creditWith` 1
+      let v = measureTail q
+      deep v (Two x y) t u
     Triple _ x _ _ -> do
-      q' <- map1 chop q
-      deep' (One x) (delay $ FPure q') u
-      where chop (Triple _ _ y z) = pair y z
+      let q' = map1 chop q
+      q'' <- value q'
+      deep (measure q') (One x) q'' u
+  where chop (Triple _ _ y z) = pair y z
 
-map1 :: (MonadCredit m, Measured a v) => (a -> a) -> FingerTree v a m -> m (FingerTree v a m)
-map1 _ Empty = pure Empty
-map1 f (Single x) = pure $ Single (f x)
-map1 f (Deep vq (One x) q u) = deep vq (One (f x)) q u
-map1 f (Deep vq (Two x y) q u) = deep vq (Two (f x) y) q u
-map1 f (Deep vq (Three x y z) q u) = deep vq (Three (f x) y z) q u
+map1 :: (Measured a v) => (a -> a)
+     -> FingerTree v a m -> FingerTree v a m
+map1 f q = case q of
+  Empty -> Empty
+  Single x -> Single (f x)
+  Deep v (One x)       m sf -> Deep v (One (f x))       m sf
+  Deep v (Two x y)     m sf -> Deep v (Two (f x) y)     m sf
+  Deep v (Three x y z) m sf -> Deep v (Three (f x) y z) m sf
 
+measureTail :: Measured a v
+            => FingerTree v (Tuple v a) m -> v
+measureTail q = case q of
+  Empty -> mempty
+  Single _ -> mempty
+  Deep v pr _ sf -> case pr of
+    One _       ->                   v <> measure sf
+    Two _ y     -> measure y      <> v <> measure sf
+    Three _ y z -> measure (y, z) <> v <> measure sf
+
 uncons :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (Maybe (a, FingerTree v a m))
 uncons q =
   if isEmpty q
@@ -188,15 +207,15 @@
       t <- tail q
       pure $ Just (h, t)
 
-deepL :: (MonadCredit m, Measured a v) => [a] -> Thunk m (Lazy m) v -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> Digit a -> m (FingerTree v a m)
+deepL :: (MonadCredit m, Measured a v) => [a] -> v -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> Digit a -> m (FingerTree v a m)
 deepL [] _ m sf = do
   m' <- uncons =<< force m
   case m' of
     Nothing -> toTree $ toList sf
     Just (Pair _ x y, m'') -> do
-      deep' (Two x y) (delay $ FPure m'') sf
+      deep' (measure m'') (Two x y) (value m'') sf
     Just (Triple _ x y z, m'') -> do
-      deep' (Three x y z) (delay $ FPure m'') sf
+      deep' (measure m'') (Three x y z) (value m'') sf
 deepL [x] vm m sf = deep vm (One x) m sf
 deepL [x,y] vm m sf = deep vm (Two x y) m sf
 deepL [x,y,z] vm m sf = deep vm (Three x y z) m sf
@@ -206,50 +225,65 @@
 last (Single x) = pure x
 last (Deep _ _ _ s) = pure $ let (h:_) = reverse $ toList s in h
 
-snoc :: (MonadCredit m, Measured a v) => FingerTree v a m -> a -> m (FingerTree v a m)
-snoc q y = tick >> snoc' q y
-
-snoc' :: (MonadCredit m, Measured a v) => FingerTree v a m -> a -> m (FingerTree v a m)
-snoc' Empty y = pure $ Single y
-snoc' (Single x) y = deep' (One x) empty (One y)
-snoc' (Deep vq u q (One x)) y = deep vq u q (Two x y)
-snoc' (Deep vq u q (Two x y)) z = creditWith q 1 >> pure (Deep vq u q (Three x y z))
-snoc' (Deep _ u q (Three x y z)) w = do
-  q' <- delay $ FSnoc q (pair x y)
-  if isTwo u
-    then creditWith q 1
-    else creditWith q' 1
-  vq' <- delay $ Lazy $ measurement =<< force q'
-  deep vq' u q' (Two z w)
+snoc :: (MonadCredit m, Measured a v)
+     => FingerTree v a m -> a -> m (FingerTree v a m)
+snoc q w = do
+  tick
+  case q of
+    Empty -> pure $ Single w
+    Single x -> do
+      em <- value Empty
+      deep mempty (One x) em (One w)
+    Deep v front middle (One x) ->
+      deep v front middle (Two x w)
+    Deep v front middle (Two x y) -> do
+      middle `creditWith` 1
+      deep v front middle (Three x y w)
+    Deep v front middle (Three x y z) -> do
+      t <- delay $ FSnoc middle (pair x y)
+      if isTwo front
+        then middle `creditWith` 1
+        else t      `creditWith` 1
+      deep (v <> measure (x, y)) front t (Two z w)
 
 init :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (FingerTree v a m)
-init Empty = tick >> pure Empty
-init (Single _) = tick >> pure Empty
-init (Deep vq u q (Three x y _)) = tick >> pure (Deep vq u q (Two x y))
-init (Deep vq u q (Two x _)) = tick >> creditWith q 1 >> pure (Deep vq u q (One x))
-init (Deep _ u q (One _)) = tick >> when (isTwo u) (creditWith q 1) >> force q >>= deepN u
+init q = do
+  tick
+  case q of
+    Empty -> pure Empty
+    Single _ -> pure Empty
+    Deep vq f q (Three x y _) -> do
+      deep vq f q (Two x y)
+    Deep vq f q (Two x _) -> do
+      q `creditWith` 1
+      deep vq f q (One x)
+    Deep _ f q (One _) -> do
+      when (isTwo f) $
+        q `creditWith` 1
+      deepN f =<< force q
 
 deepN :: (MonadCredit m, Measured a v) => Digit a -> FingerTree v (Tuple v a) m -> m (FingerTree v a m)
 deepN s Empty = toTree $ toList s
-deepN u q = do
-  l <- last q
-  case l of
-    Pair _ x y -> do
-      t <- delay $ FInit q
+deepN s (Single (Pair _ x y)) = do
+  deep' mempty s empty (Two x y)
+deepN s (Single (Triple _ x y z)) = do
+  deep' (measure x <> measure y) s (value (Single (pair x y))) (One z)
+deepN u (Deep vq pr q sf) = do
+  case chopN sf of
+    Left (vsf', x, y) -> do
+      t <- delay $ FInit (Deep vq pr q sf)
       unless (isTwo u) $ creditWith t 1
-      vt <- delay $ Lazy $ measurement =<< force t
-      deep vt u t (Two x y)
-    Triple _ _ _ z -> do
-      q' <- mapN chop q
-      deep' u (delay $ FPure q') (One z)
-      where chop (Triple _ x y _) = pair x y
+      deep (measure pr <> vq <> vsf') u t (Two x y)
+    Right (sf', x) -> do
+      deep' (measure pr <> vq <> measure sf') u (value (Deep vq pr q sf')) (One x)
 
-mapN :: (MonadCredit m, Measured a v) => (a -> a) -> FingerTree v a m -> m (FingerTree v a m)
-mapN _ Empty = pure $ Empty
-mapN f (Single x) = pure $ Single (f x)
-mapN f (Deep vq u q (One x)) = deep vq u q (One (f x))
-mapN f (Deep vq u q (Two x y)) = deep vq u q (Two x (f y))
-mapN f (Deep vq u q (Three x y z)) = deep vq u q (Three x y (f z))
+chopN :: (Measured a v) => Digit (Tuple v a) -> Either (v, a, a) (Digit (Tuple v a), a)
+chopN (One (Pair _ x y)) = Left (mempty, x, y)
+chopN (Two x (Pair _ y z)) = Left (measure x, y, z)
+chopN (Three x y (Pair _ z w)) = Left (measure x <> measure y, z, w)
+chopN (One (Triple _ x y z)) = Right (One (pair x y), z)
+chopN (Two x (Triple _ y z w)) = Right (Two x (pair y z), w)
+chopN (Three x y (Triple _ z w u)) = Right (Three x y (pair z w), u)
 
 unsnoc :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (Maybe (FingerTree v a m, a))
 unsnoc q =
@@ -260,15 +294,15 @@
       t <- init q
       pure $ Just (t, h)
 
-deepR :: (MonadCredit m, Measured a v) => Digit a -> Thunk m (Lazy m) v -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> [a] -> m (FingerTree v a m)
+deepR :: (MonadCredit m, Measured a v) => Digit a -> v -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> [a] -> m (FingerTree v a m)
 deepR s _ m [] = do
   m' <- unsnoc =<< force m
   case m' of
     Nothing -> toTree $ toList s
     Just (m'', Pair _ x y) -> do
-      deep' s (delay $ FPure m'') (Two x y)
+      deep' (measure m'') s (value m'') (Two x y)
     Just (m'', Triple _ x y z) -> do
-      deep' s (delay $ FPure m'') (Three x y z)
+      deep' (measure m'') s (value m'') (Three x y z)
 deepR s vm m [x] = deep vm s m (One x)
 deepR s vm m [x, y] = deep vm s m (Two x y)
 deepR s vm m [x, y, z] = deep vm s m (Three x y z)
@@ -290,14 +324,13 @@
   creditWith q2 2
   q2 <- force q2
   q <- glue q1 (toTuples (toList v1 ++ as ++ toList u2)) q2
-  deep' u1 (delay $ FPure q) v2
+  deep' (measure q) u1 (value q) v2
 
 concat' :: (MonadCredit m, Measured a v) => FingerTree v a m -> FingerTree v a m -> m (FingerTree v a m)
 concat' q1 q2 = glue q1 [] q2
 
 data Split v a m = Split
-  { measureOfSmaller :: v
-  , smaller :: FingerTree v a m
+  { smaller :: FingerTree v a m
   , found   :: a
   , bigger  :: FingerTree v a m
   }
@@ -312,38 +345,32 @@
   | p (i <> measure x <> measure y) = ([x], y, [z])
   | otherwise = ([x, y], z, [])
 
--- For '(Split vml ml xs mr) <- splitTree p i m', we have 'vml = measurement ml'.
 splitTree :: (MonadCredit m, Measured a v) => (v -> Bool) -> v -> FingerTree v a m -> m (Split v a m)
 splitTree p i Empty = fail "splitTree: empty tree"
-splitTree p i (Single x) = pure $ Split mempty Empty x Empty
-splitTree p i (Deep vm pr m sf) = tick >> do
-  vm' <- force vm
+splitTree p i (Single x) = pure $ Split Empty x Empty
+splitTree p i (Deep vm pr m sf) = do
+  tick
+  m `creditWith` 2
   let vpr = i <> measure pr
-  let vprm = vpr <> vm'
+  let vprm = vpr <> vm
   if p vpr then do
     let (l, x, r) = splitDigit p i pr
-    Split (measure l) <$> toTree l <*> pure x <*> deepL r vm m sf
+    Split <$> toTree l <*> pure x <*> deepL r vm m sf
   else if p vprm then do
-    Split vml ml xs mr <- splitTree p vpr =<< force m
+    Split ml xs mr <- splitTree p vpr =<< force m
+    let vml = measure ml
     let (l, x, r) = splitDigit p (vpr <> vml) (toDigit xs)
-    -- [ml', mr', vmr', vml'] <- mapM (delay . Lazy)
-      -- [pure ml, pure mr, measurement mr, pure vml]
-    ml' <- delay $ FPure ml
-    mr' <- delay $ FPure mr
-    vmr' <- delay $ Lazy $ measurement mr
-    vml' <- delay $ Lazy $ pure vml
-    Split (measure pr <> vml <> measure l) <$> deepR pr vml' ml' l <*> pure x <*> deepL r vmr' mr' sf
+    [ml', mr'] <- mapM value [ml, mr]
+    Split <$> deepR pr vml ml' l <*> pure x <*> deepL r (measure mr) mr' sf
   else do
     let (l, x, r) = splitDigit p vprm sf
-    Split (measure pr <> vm' <> measure l) <$> deepR pr vm m l <*> pure x <*> toTree r
+    Split <$> deepR pr vm m l <*> pure x <*> toTree r
 
 split :: (MonadCredit m, Measured a v) => (v -> Bool) -> FingerTree v a m -> m (FingerTree v a m, FingerTree v a m)
 split p Empty = pure (Empty, Empty)
 split p xs = do
-  forceAll xs
-  mxs <- measurement xs
-  if p mxs
-    then do (Split _ l x r) <- splitTree p mempty xs
+  if p (measure xs)
+    then do (Split l x r) <- splitTree p mempty xs
             (l,) <$> cons x r
     else pure (xs, Empty)
 
@@ -356,8 +383,8 @@
 lookupTree :: (MonadCredit m, Measured a v) => (v -> Bool) -> v -> FingerTree v a m -> m (Maybe (v, a))
 lookupTree p i Empty = pure Nothing
 lookupTree p i t = do
-  forceAll t
-  (Split ml _ x _) <- splitTree p i t
+  (Split l x _) <- splitTree p i t
+  let ml = measure l
   pure $ Just (i <> ml, x)
 
 instance MemoryCell m a => MemoryCell m (Digit a) where
@@ -386,9 +413,6 @@
     pure $ mkMCell "Triple" [a', b', c']
 
 instance (MonadMemory m, MemoryCell m a) => MemoryCell m (FLazyCon m a) where
-  prettyCell (FPure x) = do
-    x' <- prettyCell x
-    pure $ mkMCell "FPure" [x']
   prettyCell (FCons x m) = do
     -- x' <- prettyCell x
     m' <- prettyCell m
@@ -476,10 +500,8 @@
 
 newtype FingerRA a m = FingerRA (FingerTree Size (Elem a) m)
 
--- Contrary to Hinze and Paterson, this is not O(1) but O(log n)
--- because we need to force all thunks in the tree to get the size.
-length :: MonadCredit m => FingerRA a m -> m Size
-length (FingerRA t) = measurement t
+len :: MonadCredit m => FingerRA a m -> Size
+len (FingerRA t) = measure t
 
 splitAt :: MonadCredit m => Int -> FingerRA a m -> m (FingerRA a m, FingerRA a m)
 splitAt i (FingerRA xs) = do
@@ -497,14 +519,12 @@
         pure $ Just (x, FingerRA m')
   lookup i (FingerRA Empty) = pure Nothing
   lookup i (FingerRA xs) = do
-    forceAll xs
-    (Split _ _ (Elem x) _) <- splitTree (fromIntegral i <) 0 xs
+    Split _ (Elem x) _ <- splitTree (fromIntegral i <) 0 xs
     pure $ Just x
   update i a (FingerRA Empty) = pure $ FingerRA Empty
   update i a (FingerRA xs) = do
-    forceAll xs
-    (Split ml l (Elem x) r) <- splitTree (fromIntegral i <) 0 xs
-    if fromIntegral i > ml
+    Split l (Elem x) r <- splitTree (fromIntegral i <) 0 xs
+    if fromIntegral i > len (FingerRA l)
       then FingerRA <$> snoc l (Elem x)
       else FingerRA <$> (concat' l =<< cons (Elem a) r)
 
@@ -544,9 +564,7 @@
   merge (FingerHeap a) (FingerHeap b) = FingerHeap <$> concat' a b
   splitMin (FingerHeap Empty) = pure Nothing
   splitMin (FingerHeap xs) = do
-    forceAll xs -- 2 * log n
-    k <- measurement xs
-    (Split _ l (Elem x) r) <- splitTree (k >=) mempty xs -- 3 * log n
+    (Split l (Elem x) r) <- splitTree (measure xs >=) mempty xs -- 3 * log n
     lr <- concat' l r -- 5 log n
     pure $ Just (x, FingerHeap lr)
 
@@ -573,7 +591,7 @@
 instance Monoid (Key a) where
   mempty = NoKey
 
-instance Measured (Elem a) (Key a) where
+instance Eq a => Measured (Elem a) (Key a) where
   measure (Elem x) = Key x
 
 newtype FingerSort a m = FingerSort (FingerTree (Key a) (Elem a) m)
diff --git a/src/Test/Credit/Heap/Base.hs b/src/Test/Credit/Heap/Base.hs
--- a/src/Test/Credit/Heap/Base.hs
+++ b/src/Test/Credit/Heap/Base.hs
@@ -17,7 +17,7 @@
     ]
 
 class Heap h where
-  empty :: MonadCredit m => m (h a m)
+  empty :: MonadLazy m => m (h a m)
   insert :: MonadCredit m => Ord a => a -> h a m -> m (h a m)
   merge :: MonadCredit m => Ord a => h a m -> h a m -> m (h a m)
   splitMin :: MonadCredit m => Ord a => h a m -> m (Maybe (a, h a m))
@@ -25,33 +25,25 @@
 class Heap h => BoundedHeap h where
   hcost :: Size -> HeapOp a -> Credit
 
-data H h a m = E | H Size (h (PrettyCell a) m)
+data H h a m = H (h (PrettyCell a) m)
 
 instance (MemoryCell m (h (PrettyCell a) m)) => MemoryCell m (H h a m) where
-  prettyCell E = pure $ mkMCell "" []
-  prettyCell (H _ h) = prettyCell h
+  prettyCell (H h) = prettyCell h
 
 instance (MemoryStructure (h (PrettyCell a))) => MemoryStructure (H h a) where
-  prettyStructure E = pure $ mkMCell "" []
-  prettyStructure (H _ h) = prettyStructure h
-
-act :: (MonadCredit m, Heap h, Ord a) => Size -> h (PrettyCell a) m -> HeapOp a -> m (H h a m)
-act sz h (Insert x) = H (sz + 1) <$> insert (PrettyCell x) h
-act sz h Merge = pure $ H sz h
-act sz h SplitMin = do
-  m <- splitMin h
-  case m of
-    Nothing -> pure E
-    Just (_, h') -> pure $ H (max 0 (sz - 1)) h'
+  prettyStructure (H h) = prettyStructure h
 
 instance (Arbitrary a, Ord a, BoundedHeap h, Show a) => DataStructure (H h a) (HeapOp a) where
-  create = E
-  action E op = (hcost @h 0 op, empty >>= flip (act 0) op)
-  action (H sz h) op = (hcost @h sz op, act sz h op)
-
-size :: H h a m -> Size
-size E = 0
-size (H sz _) = sz
+  cost sz Merge = 0
+  cost sz op = hcost @h sz op
+  create = H <$> empty
+  perform sz (H h) (Insert x) = (sz + 1,) <$> H <$> insert (PrettyCell x) h
+  perform sz (H h) Merge = pure (sz, H h) -- no op
+  perform sz (H h) SplitMin = do
+    m <- splitMin h
+    case m of
+      Nothing -> (sz,) <$> H <$> empty
+      Just (_, h') -> pure (sz - 1, H h')
 
 data BH h a m = BH (H h a m) (H h a m)
 
@@ -67,30 +59,19 @@
     h2' <- prettyStructure h2
     pure $ mkMCell "Merge" [h1', h2']
 
-act1 :: (MonadInherit m, Heap h, Ord a) => HeapOp a -> BH h a m -> m (BH h a m)
-act1 op (BH h1 h2) = do
-  h1' <- case h1 of
-    E -> empty
-    H _ h -> pure h
-  h1'' <- act (size h1) h1' op 
-  pure $ BH h1'' h2
-
-act2 :: (MonadInherit m, Heap h, Ord a) => HeapOp a -> BH h a m -> m (BH h a m)
-act2 op (BH h1 h2) = do
-  h2' <- case h2 of
-    E -> empty
-    H _ h -> pure h
-  h2'' <- act (size h2) h2' op 
-  pure $ BH h1 h2''
-
-mergeH :: (MonadInherit m, Heap h, Ord a) => H h a m -> H h a m -> m (H h a m)
-mergeH E E = pure E
-mergeH (H sz1 h1) E = pure $ H sz1 h1
-mergeH E (H sz2 h2) = pure $ H sz2 h2
-mergeH (H sz1 h1) (H sz2 h2) = H (sz1 + sz2) <$> merge h1 h2
-
 instance (Arbitrary a, Ord a, BoundedHeap h, Show a) => DataStructure (BH h a) (HeapOp a) where
-  create = BH E E
-  action (BH h1 h2) (Insert a) = (hcost @h (size h1) (Insert a),      act1 (Insert a) (BH h1 h2))
-  action (BH h1 h2) SplitMin   = (hcost @h (size h2) SplitMin,        act2 SplitMin (BH h1 h2))
-  action (BH h1 h2) Merge      = (hcost @h (size h1 + size h2) Merge, BH E <$> mergeH h1 h2)
+  cost = hcost @h
+  create = do
+    h1 <- empty
+    h2 <- empty
+    pure $ BH (H h1) (H h2)
+  perform sz (BH h1 h2) (Insert a) = do
+    (sz, h1) <- perform sz h1 (Insert a)
+    pure (sz, BH h1 h2)
+  perform sz (BH h1 h2) SplitMin = do
+    (sz, h2) <- perform sz h2 SplitMin
+    pure (sz, BH h1 h2)
+  perform sz (BH (H h1) (H h2)) Merge = do
+    h <- merge h1 h2
+    e <- empty
+    pure (sz, BH (H e) (H h))
diff --git a/src/Test/Credit/Heap/Scheduled.hs b/src/Test/Credit/Heap/Scheduled.hs
--- a/src/Test/Credit/Heap/Scheduled.hs
+++ b/src/Test/Credit/Heap/Scheduled.hs
@@ -3,7 +3,7 @@
 module Test.Credit.Heap.Scheduled where
 
 import Prettyprinter (Pretty)
-import Control.Monad.Credit hiding (exec)
+import Control.Monad.Credit
 import Test.Credit
 import Test.Credit.Heap.Base
 
@@ -64,10 +64,10 @@
       (_, Zero) -> SCons d1 <$> mrg ds1 ds2
       (One t1, One t2) -> SCons Zero <$> (insTree (link t1 t2) =<< mrg ds1 ds2)))
 
-normalize :: MonadCredit m => Ord a => Stream m (Digit a) -> m (Stream m (Digit a))
+normalize :: MonadCredit m => Ord a => Stream m (Digit a) -> m ()
 normalize ds = credit 1 ds >> smatch ds
-    (pure SNil)
-    (\d ds -> SCons d <$> normalize ds)
+    (pure ())
+    (\_ ds -> normalize ds)
 
 exec :: MonadCredit m => Schedule m a -> m (Schedule m a)
 exec [] = pure []
@@ -119,7 +119,7 @@
 
 instance BoundedHeap Scheduled where
   hcost _ (Insert _) = 5
-  hcost n Merge = 4 + 8 * log2 n
+  hcost n Merge = 8 * (1 + log2 n)
   hcost n SplitMin = 1 + 5 * log2 n + 6 * log2 (2 * n)
 
 instance MemoryCell m a => MemoryCell m (Tree a) where
diff --git a/src/Test/Credit/Queue/Bankers.hs b/src/Test/Credit/Queue/Bankers.hs
--- a/src/Test/Credit/Queue/Bankers.hs
+++ b/src/Test/Credit/Queue/Bankers.hs
@@ -1,47 +1,76 @@
+{-# LANGUAGE LambdaCase, GADTs #-}
+
 module Test.Credit.Queue.Bankers where
 
-import Prettyprinter (Pretty)
 import Control.Monad.Credit
+import Data.Maybe (fromMaybe)
+import Prettyprinter (Pretty)
 import Test.Credit
 import Test.Credit.Queue.Base
 import Test.Credit.Queue.Streams
 
 data BQueue a m = BQueue
-  { front :: Stream m a
-  , flen :: !Int
-  , rear :: Stream m a
+  { flen :: !Int
   , rlen :: !Int
+  , front :: Stream m a
+  , rear  :: Stream m a
   }
 
-bqueue :: MonadInherit m => BQueue a m -> m (BQueue a m)
-bqueue (BQueue f fl r rl) = do
-  ifIndirect f (`hasAtLeast` fromIntegral rl)
+allEvaluated :: MonadInherit m => StreamCell m a -> m ()
+allEvaluated SNil = pure ()
+allEvaluated (SCons _ xs) = isEvaluated xs
+
+isEvaluated :: MonadInherit m => Stream m a -> m ()
+isEvaluated s = lazymatch s allEvaluated (error "Stream should be pure")
+
+allInvariant :: MonadInherit m => Maybe Int -> StreamCell m a -> m ()
+allInvariant _ SNil = pure ()
+allInvariant rlen (SCons x xs) = invariant xs (fmap (subtract 2) rlen)
+
+invariant :: MonadInherit m => Stream m a -> Maybe Int -> m ()
+invariant front rlen = 
+  lazymatch front (allInvariant rlen) $ \case
+    SAppend xs ys -> do
+      lxs <- slength xs
+      lys <- slength ys
+      front `hasAtLeast` (fromIntegral $ fromMaybe (2 * lxs) rlen)
+      invariant xs Nothing
+      ys `hasAtLeast` (fromIntegral $ lys - lxs)
+    SReverse xs ys -> do
+      lxs <- slength xs
+      front `hasAtLeast` (fromIntegral lxs)
+      isEvaluated xs
+      isEvaluated ys
+
+bqueue :: MonadInherit m => Int -> Int -> Stream m a -> Stream m a -> m (BQueue a m)
+bqueue fl rl f r = do
+  isEvaluated r
+  invariant f (Just rl)
   if fl >= rl 
-    then pure $ BQueue f fl r rl
+    then pure $ BQueue fl rl f r
     else do
-      r' <- delay (SReverse r SNil)
+      r' <- delay . SReverse r =<< nil
       r' `creditWith` 1
-      f' <- delay (SAppend f (SIndirect r'))
-      pure $ BQueue (SIndirect f') (fl + rl) SNil 0
+      BQueue (fl + rl) 0 <$> (delay $ SAppend f r') <*> nil
 
 instance Queue BQueue where
-  empty = pure $ BQueue SNil 0 SNil 0
-  snoc (BQueue f fl r rl) x = do
-    credit f
-    bqueue (BQueue f fl (SCons x r) (rl + 1))
-  uncons (BQueue f fl r rl) = do
-    credit f >> credit f
-    smatch f
-      (\x f -> do
-        q <- bqueue (BQueue f (fl - 1) r rl)
-        pure $ Just (x, q))
-      (pure Nothing)
+  empty = BQueue 0 0 <$> nil <*> nil
+  snoc (BQueue fl rl f r) x = do
+    f `creditWith` 1
+    bqueue fl (rl + 1) f =<< cons x r
+  uncons (BQueue fl rl f r) = do
+    f `creditWith` 2
+    force f >>= \case
+      SCons x f' -> do
+        q <- bqueue (fl - 1) rl f' r
+        pure $ Just (x, q)
+      SNil -> pure Nothing
 
 isEmpty :: BQueue a m -> Bool
-isEmpty (BQueue _ flen _ rlen) = flen == 0 && rlen == 0
+isEmpty (BQueue flen rlen _ _) = flen == 0 && rlen == 0
 
 lazyqueue :: MonadInherit m => BQueue a m -> m [a]
-lazyqueue (BQueue f fl r rl) = do
+lazyqueue (BQueue fl rl f r) = do
   f' <- toList f
   r' <- toList r
   pure $ f' ++ reverse r'
@@ -51,12 +80,12 @@
   qcost _ Uncons = 4
 
 instance (MonadMemory m, MemoryCell m a) => MemoryCell m (BQueue a m) where
-  prettyCell (BQueue f fl r rl) = do
-    f' <- prettyCell f
+  prettyCell (BQueue fl rl f r) = do
     fl' <- prettyCell fl
-    r' <- prettyCell r
     rl' <- prettyCell rl
-    pure $ mkMCell "Queue" [f', fl', r', rl']
+    f' <- prettyCell f
+    r' <- prettyCell r
+    pure $ mkMCell "Queue" [fl', rl', f', r']
 
 instance Pretty a => MemoryStructure (BQueue (PrettyCell a)) where
   prettyStructure = prettyCell
diff --git a/src/Test/Credit/Queue/Base.hs b/src/Test/Credit/Queue/Base.hs
--- a/src/Test/Credit/Queue/Base.hs
+++ b/src/Test/Credit/Queue/Base.hs
@@ -3,7 +3,6 @@
 module Test.Credit.Queue.Base where
 
 import Control.Monad.Credit
-import Prettyprinter
 import Test.Credit
 import Test.QuickCheck
 
@@ -17,28 +16,25 @@
     ]
 
 class Queue q where
-  empty :: MonadInherit m => m (q a m)
+  empty :: MonadLazy m => m (q a m)
   snoc :: MonadInherit m => q a m -> a -> m (q a m)
   uncons :: MonadInherit m => q a m -> m (Maybe (a, q a m))
 
 class Queue q => BoundedQueue q where
   qcost :: Size -> QueueOp a -> Credit
 
-data Q q a m = E | Q Size (q (PrettyCell a) m)
+data Q q a m = Q (q (PrettyCell a) m)
 
 instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (Q q a) where
-  prettyStructure E = pure $ mkMCell "" []
-  prettyStructure (Q _ q) = prettyStructure q
-
-act :: (MonadInherit m, Queue q) => Size -> q (PrettyCell a) m -> QueueOp a -> m (Q q a m)
-act sz q (Snoc x) = Q (sz + 1) <$> snoc q (PrettyCell x)
-act sz q Uncons = do
-  m <- uncons q
-  case m of
-    Nothing -> pure E
-    Just (_, q') -> pure $ Q (max 0 (sz - 1)) q'
+  prettyStructure (Q q) = prettyStructure q
 
 instance (Arbitrary a, BoundedQueue q, Show a) => DataStructure (Q q a) (QueueOp a) where
-  create = E
-  action E op = (qcost @q 0 op, empty >>= flip (act 0) op)
-  action (Q sz q) op = (qcost @q sz op, act sz q op)
+  cost = qcost @q
+  create = Q <$> empty
+  perform sz (Q q) (Snoc x) = (sz + 1,) <$> Q <$> snoc q (PrettyCell x)
+  perform sz (Q q) Uncons = do
+    m <- uncons q
+    q' <- case m of
+      Nothing -> empty
+      Just (_, q') -> pure q'
+    pure (max 0 (sz - 1), Q q')
diff --git a/src/Test/Credit/Queue/Implicit.hs b/src/Test/Credit/Queue/Implicit.hs
--- a/src/Test/Credit/Queue/Implicit.hs
+++ b/src/Test/Credit/Queue/Implicit.hs
@@ -24,12 +24,10 @@
   | Deep (Digit a) (Thunk m (ILazyCon m) (Implicit (a, a) m)) (Digit a)
 
 data ILazyCon m a where
-  IPure :: a -> ILazyCon m a
   ISnoc :: Thunk m (ILazyCon m) (Implicit a m) -> a -> ILazyCon m (Implicit a m)
   ITail :: Implicit a m -> ILazyCon m (Implicit a m)
 
 instance MonadCredit m => HasStep (ILazyCon m) m where
-  step (IPure x) = pure x
   step (ISnoc t p) = do
     q <- force t
     snoc' q p
@@ -60,7 +58,7 @@
   case q of
     Shallow Zero -> pure $ Shallow (One y)
     Shallow (One x) -> do
-      middle <- delay $ IPure $ Shallow Zero
+      middle <- value $ Shallow Zero
       deep (Two x y) middle Zero
     Deep front middle Zero -> do
       middle `creditWith` 1
@@ -100,7 +98,6 @@
 showThunk :: (MonadLazy m, Show a)
           => Thunk m (ILazyCon m) (Implicit a m) -> m String
 showThunk t = lazymatch t showImplicit $ \case
-    IPure a -> showImplicit a
     ISnoc middle xy -> do
       m <- showThunk middle
       pure $ "(snoc " ++ m ++ " " ++ show xy ++ ")"
@@ -143,9 +140,6 @@
     pure $ mkMCell "Two" [a', b']
 
 instance (MonadMemory m, MemoryCell m a) => MemoryCell m (ILazyCon m a) where
-  prettyCell (IPure x) = do
-    x' <- prettyCell x
-    pure $ mkMCell "IPure" [x']
   prettyCell (ISnoc t _) = do
     t' <- prettyCell t
     pure $ mkMCell "ISnoc" [t']
diff --git a/src/Test/Credit/Queue/Realtime.hs b/src/Test/Credit/Queue/Realtime.hs
--- a/src/Test/Credit/Queue/Realtime.hs
+++ b/src/Test/Credit/Queue/Realtime.hs
@@ -1,16 +1,12 @@
-module Test.Credit.Queue.Realtime where
+{-# LANGUAGE LambdaCase #-}
 
-import Prelude hiding (lookup, reverse)
+module Test.Credit.Queue.Realtime where
 
 import Prettyprinter (Pretty)
 import Control.Monad.Credit
 import Test.Credit.Queue.Base
 import Test.Credit.Queue.Streams
 
--- | Delay a computation, but do not consume any credits
-indirect :: MonadInherit m => SLazyCon m (Stream m a) -> m (Stream m a)
-indirect t = delay t >>= pure . SIndirect
-
 data RQueue a m = RQueue
   { front :: Stream m a
   , rear :: Stream m a
@@ -18,20 +14,31 @@
   }
 
 rqueue :: MonadInherit m => RQueue a m -> m (RQueue a m)
-rqueue (RQueue f r s) = credit s >> credit s >> smatch s
-  (\x s -> pure $ RQueue f r s)
-  (do
-    r' <- indirect (SReverse r SNil)
-    f' <- indirect (SAppend f r')
-    credit r' >> evalone r'
-    pure $ RQueue f' SNil f')
+rqueue (RQueue f r s) = do
+  s `creditWith` 2
+  force s >>= \case
+    SCons _ s -> pure $ RQueue f r s
+    SNil -> do
+      r' <- delay . SReverse r =<< nil
+      f' <- delay $ SAppend f r'
+      r' `creditWith` 1
+      n <- nil
+      pure $ RQueue f' n f'
 
 instance Queue RQueue where
-  empty = pure $ RQueue SNil SNil SNil
-  snoc (RQueue f r s) x = rqueue (RQueue f (SCons x r) s)
-  uncons (RQueue f r s) = credit f >> credit f >> smatch f
-    (\x f -> rqueue (RQueue f r s) >>= \q -> pure $ Just (x, q))
-    (pure Nothing)
+  empty = do
+    n <- nil
+    pure $ RQueue n n n
+  snoc (RQueue f r s) x = do
+    r' <- cons x r
+    rqueue $ RQueue f r' s
+  uncons (RQueue f r s) = do
+    f `creditWith` 2
+    force f >>= \case
+      SCons x f -> do
+        q <- rqueue $ RQueue f r s
+        pure $ Just (x, q)
+      SNil -> pure Nothing
 
 instance BoundedQueue RQueue where
   qcost _ (Snoc _) = 4
diff --git a/src/Test/Credit/Queue/Streams.hs b/src/Test/Credit/Queue/Streams.hs
--- a/src/Test/Credit/Queue/Streams.hs
+++ b/src/Test/Credit/Queue/Streams.hs
@@ -1,84 +1,55 @@
 {-# LANGUAGE GADTs, LambdaCase #-}
 
-module Test.Credit.Queue.Streams (Stream(..), SThunk, SLazyCon(..), smatch, credit, evalone, toList, ifIndirect, test) where
+module Test.Credit.Queue.Streams (Stream, StreamCell(..), SLazyCon(..), cons, nil, slength, toList, test) where
 
 import Control.Monad
 import Control.Monad.Credit
 
-data Stream m a
+type Stream m a = Thunk m (SLazyCon m) (StreamCell m a)
+
+data StreamCell m a
   = SCons a (Stream m a)
   | SNil
-  | SIndirect (SThunk m (Stream m a))
 
-type SThunk m = Thunk m (SLazyCon m)
-
 data SLazyCon m a where
-  SAppend :: Stream m a -> Stream m a -> SLazyCon m (Stream m a)
-  SReverse :: Stream m a -> Stream m a -> SLazyCon m (Stream m a)
+  SAppend  :: Stream m a -> Stream m a -> SLazyCon m (StreamCell m a)
+  SReverse :: Stream m a -> Stream m a -> SLazyCon m (StreamCell m a)
 
 instance MonadInherit m => HasStep (SLazyCon m) m where
-  step (SAppend xs ys) = sappend xs ys
-  step (SReverse xs ys) = sreverse xs ys
-
--- | Smart destructor for streams, consuming one credit
-smatch :: MonadInherit m => Stream m a -- ^ Scrutinee
-       -> (a -> Stream m a -> m b) -- ^ Cons case
-       -> m b -- ^ Nil case
-       -> m b
-smatch x cons nil = tick >> eval x
-  where
-    eval x = case x of
-      SCons a as -> cons a as
-      SNil -> nil
-      SIndirect i -> force i >>= eval
-
--- | delay a computation, consuming all credits
-taildelay :: MonadInherit m => SLazyCon m (Stream m a) -> m (Stream m a)
-taildelay t = do
-  x <- delay t
-  creditAllTo x
-  pure (SIndirect x)
-
-sreverse :: MonadInherit m => Stream m a -> Stream m a -> m (Stream m a)
-sreverse xs ys = smatch xs
-  (\x xs -> taildelay (SReverse xs (SCons x ys)))
-  (pure ys)
-
-ifIndirect :: Monad m => Stream m a -> (SThunk m (Stream m a) -> m ()) -> m ()
-ifIndirect (SIndirect i) f = f i
-ifIndirect _ _ = pure ()
-
-credit :: MonadInherit m => Stream m a -> m ()
-credit s = ifIndirect s (`creditWith` 1)
+  step (SAppend  xs ys) = force =<< sappend  xs ys 
+  step (SReverse xs ys) = force =<< sreverse xs ys
 
-evalone :: MonadInherit m => Stream m a -> m ()
-evalone s = ifIndirect s (void . force)
+cons :: MonadLazy m => a -> Stream m a -> m (Stream m a)
+cons x xs = value $ SCons x xs
 
-sappend :: MonadInherit m => Stream m a -> Stream m a -> m (Stream m a)
-sappend xs ys = credit ys >> evalone ys >> smatch xs
-  (\x xs -> SCons x <$> taildelay (SAppend xs ys))
-  (pure ys)
+nil :: MonadLazy m => m (Stream m a)
+nil = value SNil
 
-walk s = smatch s (\_ xs -> walk xs) (pure ())
+sreverse :: MonadInherit m
+          => Stream m a -> Stream m a -> m (Stream m a)
+sreverse xs ys = tick >> force xs >>= \case
+  SCons x xs -> sreverse xs =<< cons x ys
+  SNil -> pure ys
 
-foo :: MonadInherit m => Stream m a -> m ()
-foo s = smatch s (\_ _ -> pure ()) (pure ())
+sappend :: MonadInherit m
+         => Stream m a -> Stream m a -> m (Stream m a)
+sappend xs ys = do
+  tick
+  ys `creditWith` 1
+  force xs >>= \case
+    SCons x xs' -> do
+      xs'ys <- delay $ SAppend xs' ys
+      creditAllTo xs'ys
+      cons x xs'ys
+    SNil -> creditAllTo ys >> pure ys
 
-test :: MonadInherit m => m ()
-test = do
-  s <- sappend (SCons 1 SNil) (SCons 2 SNil)
-  credit s >> credit s
-  foo s
-  credit s
-  walk s
+cellToList :: MonadLazy m => StreamCell m a -> m [a]
+cellToList SNil = pure []
+cellToList (SCons x xs) = (x :) <$> toList xs
 
 toList :: MonadLazy m => Stream m a -> m [a]
-toList SNil = pure []
-toList (SCons x xs) = do
-  xs' <- toList xs
-  pure $ x : xs'
-toList (SIndirect t) = do
-  lazymatch t toList $ \case
+toList t = do
+  lazymatch t cellToList $ \case
       SAppend xs ys -> do
         xs' <- toList xs
         ys' <- toList ys
@@ -88,6 +59,28 @@
         ys' <- toList ys
         pure $ reverse xs' ++ ys'
 
+slength :: MonadLazy m => Stream m a -> m Int
+slength s = length <$> toList s
+
+walk :: MonadInherit m => Stream m a -> m ()
+walk s = force s >>= \case
+  SCons _ xs -> walk xs
+  SNil -> pure ()
+
+foo :: MonadInherit m => Stream m a -> m ()
+foo s = void $ force s
+
+test :: MonadInherit m => m ()
+test = do
+  nil <- value SNil
+  one <- value (SCons 1 nil)
+  two <- value (SCons 2 nil)
+  s <- sappend one two
+  creditWith s 2
+  foo s
+  creditWith s 1
+  walk s
+
 instance (MonadMemory m, MemoryCell m a) => MemoryCell m (SLazyCon m a) where
   prettyCell (SAppend xs ys) = do
     xs' <- prettyCell xs
@@ -98,13 +91,11 @@
     ys' <- prettyCell ys
     pure $ mkMCell "SReverse" [xs', ys']
 
-instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Stream m a) where
+instance (MonadMemory m, MemoryCell m a) => MemoryCell m (StreamCell m a) where
   prettyCell xs = mkMList <$> toList xs <*> toHole xs
     where
       toList SNil = pure $ []
-      toList (SCons x xs) = (:) <$> prettyCell x <*> toList xs
-      toList (SIndirect t) = pure $ []
+      toList (SCons x xs) = (:) <$> prettyCell x <*> lazymatch xs toList (\_ -> pure [])
 
       toHole SNil = pure $ Nothing
-      toHole (SCons x xs) = toHole xs
-      toHole (SIndirect t) = Just <$> prettyCell t
+      toHole (SCons x xs) = lazymatch xs toHole (\_ -> Just <$> prettyCell xs)
diff --git a/src/Test/Credit/RandomAccess/Base.hs b/src/Test/Credit/RandomAccess/Base.hs
--- a/src/Test/Credit/RandomAccess/Base.hs
+++ b/src/Test/Credit/RandomAccess/Base.hs
@@ -19,7 +19,7 @@
     ]
 
 class RandomAccess q where
-  empty :: MonadCredit m => m (q a m)
+  empty :: MonadLazy m => m (q a m)
   cons :: MonadCredit m => a -> q a m  -> m (q a m)
   uncons :: MonadCredit m => q a m -> m (Maybe (a, q a m))
   lookup :: MonadCredit m => Int -> q a m -> m (Maybe a)
@@ -28,15 +28,13 @@
 class RandomAccess q => BoundedRandomAccess q where
   qcost :: Size -> RandomAccessOp a -> Credit
 
-data RA q a m = E | RA Size (q (PrettyCell a) m)
+data RA q a m = RA (q (PrettyCell a) m)
 
 instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (RA q a m) where
-  prettyCell E = pure $ mkMCell "" []
-  prettyCell (RA _ q) = prettyCell q
+  prettyCell (RA q) = prettyCell q
 
 instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (RA q a) where
-  prettyStructure E = pure $ mkMCell "" []
-  prettyStructure (RA _ q) = prettyStructure q
+  prettyStructure (RA q) = prettyStructure q
 
 idx :: Int -> Size -> Int
 idx i sz = if sz <= 0 then 0 else abs (i `mod` fromIntegral sz)
@@ -46,19 +44,17 @@
 norm sz (Update i a) = Update (idx i sz) a
 norm _ op = op
 
-act :: (MonadCredit m, RandomAccess q) => Size -> q (PrettyCell a) m -> RandomAccessOp a -> m (RA q a m)
-act sz q (Cons x) = RA (sz + 1) <$> cons (PrettyCell x) q
-act sz q Uncons = do
-  m <- uncons q
-  case m of
-    Nothing -> pure E
-    Just (_, q') -> pure $ RA (max 0 (sz - 1)) q'
-act sz q (Lookup i) = do
-  _ <- lookup i q
-  pure $ RA sz q
-act sz q (Update i a) = RA sz <$> update i (PrettyCell a) q
-
 instance (Arbitrary a, BoundedRandomAccess q, Show a) => DataStructure (RA q a) (RandomAccessOp a) where
-  create = E
-  action E op = (qcost @q 0 (norm 0 op), empty >>= flip (act 0) (norm 0 op))
-  action (RA sz q) op = (qcost @q sz (norm sz op), act sz q (norm sz op))
+  cost sz op = qcost @q sz (norm sz op)
+  create = RA <$> empty
+  perform sz (RA q) (Cons x) = (sz + 1,) <$> RA <$> cons (PrettyCell x) q
+  perform sz (RA q) Uncons = do
+    m <- uncons q
+    m' <- case m of
+      Nothing -> empty
+      Just (_, q') -> pure q'
+    pure (max 0 (sz - 1), RA m')
+  perform sz (RA q) (Lookup i) = do
+    _ <- lookup (idx i sz) q
+    pure $ (sz, RA q)
+  perform sz (RA q) (Update i a) = (sz,) <$> RA <$> update (idx i sz) (PrettyCell a) q
diff --git a/src/Test/Credit/RandomAccess/Binary.hs b/src/Test/Credit/RandomAccess/Binary.hs
--- a/src/Test/Credit/RandomAccess/Binary.hs
+++ b/src/Test/Credit/RandomAccess/Binary.hs
@@ -4,7 +4,7 @@
 
 import Prelude hiding (lookup)
 import Prettyprinter (Pretty)
-import Control.Monad.Credit hiding (exec)
+import Control.Monad.Credit
 import Test.Credit
 import Test.Credit.RandomAccess.Base
 
diff --git a/src/Test/Credit/RandomAccess/Zeroless.hs b/src/Test/Credit/RandomAccess/Zeroless.hs
--- a/src/Test/Credit/RandomAccess/Zeroless.hs
+++ b/src/Test/Credit/RandomAccess/Zeroless.hs
@@ -4,7 +4,7 @@
 
 import Prelude hiding (lookup)
 import Prettyprinter (Pretty)
-import Control.Monad.Credit hiding (exec)
+import Control.Monad.Credit
 import Test.Credit
 import Test.Credit.RandomAccess.Base
 
diff --git a/src/Test/Credit/Sortable/Base.hs b/src/Test/Credit/Sortable/Base.hs
--- a/src/Test/Credit/Sortable/Base.hs
+++ b/src/Test/Credit/Sortable/Base.hs
@@ -16,30 +16,25 @@
     ]
 
 class Sortable q where
-  empty :: MonadCredit m => m (q a m)
+  empty :: MonadLazy m => m (q a m)
   add :: MonadCredit m => Ord a => a -> q a m -> m (q a m)
   sort :: MonadCredit m => Ord a => q a m -> m [a] 
 
 class Sortable q => BoundedSortable q where
   scost :: Size -> SortableOp a -> Credit
 
-data S q a m = E | S Size (q (PrettyCell a) m)
+data S q a m = S (q (PrettyCell a) m)
 
 instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (S q a m) where
-  prettyCell E = pure $ mkMCell "" []
-  prettyCell (S _ q) = prettyCell q
+  prettyCell (S q) = prettyCell q
 
 instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (S q a) where
-  prettyStructure E = pure $ mkMCell "" []
-  prettyStructure (S sz q) = prettyStructure q
-
-act :: (MonadCredit m, Sortable q, Ord a) => Size -> q (PrettyCell a) m -> SortableOp a -> m (S q a m)
-act sz q (Add x) = S (sz + 1) <$> add (PrettyCell x) q
-act sz q Sort = do
-  xs <- sort q
-  pure $ S sz q
+  prettyStructure (S q) = prettyStructure q
 
 instance (Arbitrary a, Ord a, BoundedSortable q, Show a) => DataStructure (S q a) (SortableOp a) where
-  create = E
-  action E op = (scost @q 0 op, empty >>= flip (act 0) op)
-  action (S sz q) op = (scost @q sz op, act sz q op)
+  cost = scost @q
+  create = S <$> empty
+  perform sz (S q) (Add x) = (sz + 1,) <$> S <$> add (PrettyCell x) q
+  perform sz (S q) Sort = do
+    _ <- sort q
+    pure (sz, S q)