diff --git a/Compiler/Hoopl.hs b/Compiler/Hoopl.hs
--- a/Compiler/Hoopl.hs
+++ b/Compiler/Hoopl.hs
@@ -3,6 +3,7 @@
   , module Compiler.Hoopl.MkGraph
   , module Compiler.Hoopl.XUtil
   , module Compiler.Hoopl.Collections
+  , module Compiler.Hoopl.Checkpoint
   , module Compiler.Hoopl.Dataflow
   , module Compiler.Hoopl.Label
   , module Compiler.Hoopl.Pointed
@@ -15,9 +16,11 @@
   )
 where
 
+import Compiler.Hoopl.Checkpoint
 import Compiler.Hoopl.Collections
 import Compiler.Hoopl.Combinators
-import Compiler.Hoopl.Dataflow
+import Compiler.Hoopl.Dataflow hiding ( wrapFR, wrapFR2, wrapBR, wrapBR2
+                                      )
 import Compiler.Hoopl.Debug
 import Compiler.Hoopl.Fuel hiding (withFuel, getFuel, setFuel, FuelMonadT)
 import Compiler.Hoopl.Graph hiding 
diff --git a/Compiler/Hoopl/Checkpoint.hs b/Compiler/Hoopl/Checkpoint.hs
new file mode 100644
--- /dev/null
+++ b/Compiler/Hoopl/Checkpoint.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Compiler.Hoopl.Checkpoint
+  ( CheckpointMonad(..)
+  )
+where
+
+-- | Obeys the following law:
+-- for all @m@ 
+-- @
+--    do { s <- checkpoint; m; restart s } == return ()
+-- @
+class Monad m => CheckpointMonad m where
+  type Checkpoint m
+  checkpoint :: m (Checkpoint m)
+  restart    :: Checkpoint m -> m () 
+
diff --git a/Compiler/Hoopl/Combinators.hs b/Compiler/Hoopl/Combinators.hs
--- a/Compiler/Hoopl/Combinators.hs
+++ b/Compiler/Hoopl/Combinators.hs
@@ -1,93 +1,35 @@
-{-# LANGUAGE RankNTypes, LiberalTypeSynonyms, ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes, LiberalTypeSynonyms, ScopedTypeVariables, GADTs #-}
 
 module Compiler.Hoopl.Combinators
-  ( SimpleFwdRewrite, SimpleFwdRewrite3, noFwdRewrite, thenFwdRw
-  , shallowFwdRw3, shallowFwdRw, deepFwdRw3, deepFwdRw, iterFwdRw
-  , SimpleBwdRewrite, SimpleBwdRewrite3, noBwdRewrite, thenBwdRw
-  , shallowBwdRw3, shallowBwdRw, deepBwdRw3, deepBwdRw, iterBwdRw
+  ( thenFwdRw
+  , deepFwdRw3, deepFwdRw, iterFwdRw
+  , thenBwdRw
+  , deepBwdRw3, deepBwdRw, iterBwdRw
   , pairFwd, pairBwd, pairLattice
   )
 
 where
 
 import Control.Monad
-import Data.Function
 import Data.Maybe
 
 import Compiler.Hoopl.Collections
 import Compiler.Hoopl.Dataflow
-import Compiler.Hoopl.Graph (Graph, C, O)
+import Compiler.Hoopl.Fuel
+import Compiler.Hoopl.Graph (Graph, C, O, Shape(..))
 import Compiler.Hoopl.Label
 
-type FR m n f = FwdRewrite m n f
-type BR m n f = BwdRewrite m n f
-
-type FwdRes m n f e x = Maybe (FwdRew m n f e x)
-
-type SFRW m n f e x = n e x -> f -> m (Maybe (Graph n e x))
-type FRW  m n f e x = n e x -> f -> m (FwdRes m n f e x)
-type SimpleFwdRewrite3 m n f = ExTriple (SFRW m n f)
-type ExTriple a = (a C O, a O O, a O C) -- ^ entry/exit triple
-type SimpleFwdRewrite m n f = forall e x . SFRW m n f e x
-type LiftFRW m n f e x = SFRW m n f e x -> FRW m n f e x
-type MapFRW  m n f e x = FRW  m n f e x -> FRW m n f e x
-type MapFRW2 m n f e x = FRW  m n f e x -> FRW m n f e x -> FRW m n f e x
-
 ----------------------------------------------------------------
--- common operations on triples
 
-uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d
-uncurry3 f (a, b, c) = f a b c
-
-apply :: (a -> b, d -> e, g -> h) -> (a, d, g) -> (b, e, h)
-apply (f1, f2, f3) (x1, x2, x3) = (f1 x1, f2 x2, f3 x3)
-
-applyBinary :: (a -> b -> c, d -> e -> f, g -> h -> i)
-            -> (a, d, g) -> (b, e, h) -> (c, f, i)
-applyBinary (f1, f2, f3) (x1, x2, x3) (y1, y2, y3) = (f1 x1 y1, f2 x2 y2, f3 x3 y3)
-
-
-----------------------------------------------------------------
-
-wrapSFRewrite3 :: ExTriple (LiftFRW m n f) -> SimpleFwdRewrite3 m n f -> FR m n f
-wrapSFRewrite3 lift rw = uncurry3 mkFRewrite3 $ apply lift rw
-
-wrapFRewrite3 :: ExTriple (MapFRW m n f) -> FR m n f -> FR m n f
-wrapFRewrite3 map frw = uncurry3 mkFRewrite3 $ apply map $ getFRewrite3 frw
-
-wrapFRewrites23 :: ExTriple (MapFRW2 m n f) -> FR m n f -> FR m n f -> FR m n f
-wrapFRewrites23 map frw1 frw2 =
-  uncurry3 mkFRewrite3 $ (applyBinary map `on` getFRewrite3) frw1 frw2
-
-
--- Combinators for higher-rank rewriting functions:
-wrapSFRewrites' :: (forall e x . LiftFRW m n f e x) -> SimpleFwdRewrite3 m n f -> FR m n f
-wrapSFRewrites' lift = wrapSFRewrite3 (lift, lift, lift)
-
-wrapFRewrites :: (forall e x . MapFRW m n f e x) -> FR m n f -> FR m n f
-wrapFRewrites map = wrapFRewrite3 (map, map, map)
--- It's ugly that we can't use
---    wrapFRewrites' = mkFRewrite'
--- Would be nice to refactor here XXX  ---NR
-
-
-wrapFRewrites2 :: (forall e x . MapFRW2 m n f e x) -> FR m n f -> FR m n f -> FR m n f
-wrapFRewrites2 map = wrapFRewrites23 (map, map, map)
-
-----------------------------------------------------------------
-
-
-shallowFwdRw3 :: forall m n f . Monad m => SimpleFwdRewrite3 m n f -> FwdRewrite m n f
-shallowFwdRw3 rw = wrapSFRewrites' lift rw
-  where lift rw n f = liftM (liftM (flip FwdRew noFwdRewrite)) (rw n f) 
-
-shallowFwdRw :: Monad m => SimpleFwdRewrite m n f -> FwdRewrite m n f
-shallowFwdRw f = shallowFwdRw3 (f, f, f)
-
-deepFwdRw3    :: Monad m => SimpleFwdRewrite3 m n f -> FwdRewrite m n f
-deepFwdRw :: Monad m => SimpleFwdRewrite m n f -> FwdRewrite m n f
-deepFwdRw3    r = iterFwdRw (shallowFwdRw3 r)
-deepFwdRw f = deepFwdRw3 (f, f, f)
+deepFwdRw3 :: FuelMonad m
+           => (n C O -> f -> m (Maybe (Graph n C O)))
+           -> (n O O -> f -> m (Maybe (Graph n O O)))
+           -> (n O C -> f -> m (Maybe (Graph n O C)))
+           -> (FwdRewrite m n f)
+deepFwdRw :: FuelMonad m
+          => (forall e x . n e x -> f -> m (Maybe (Graph n e x))) -> FwdRewrite m n f
+deepFwdRw3 f m l = iterFwdRw $ mkFRewrite3 f m l
+deepFwdRw f = deepFwdRw3 f f f
 
 -- N.B. rw3, rw3', and rw3a are triples of functions.
 -- But rw and rw' are single functions.
@@ -97,91 +39,77 @@
           -> FwdRewrite m n f 
           -> FwdRewrite m n f
 -- @ end comb1.tex
-thenFwdRw rw3 rw3' = wrapFRewrites2 thenrw rw3 rw3'
+thenFwdRw rw3 rw3' = wrapFR2 thenrw rw3 rw3'
  where
   thenrw rw rw' n f = rw n f >>= fwdRes
-     where fwdRes Nothing = rw' n f
-           fwdRes (Just (FwdRew g rw3a))
-            = return $ Just $ FwdRew g (rw3a `thenFwdRw` rw3')
-
-noFwdRewrite :: Monad m => FwdRewrite m n f
-noFwdRewrite = mkFRewrite $ \ _ _ -> return Nothing
+     where fwdRes Nothing   = rw' n f
+           fwdRes (Just gr) = return $ Just $ fadd_rw rw3' gr
 
 -- @ start iterf.tex
 iterFwdRw :: Monad m 
           => FwdRewrite m n f 
           -> FwdRewrite m n f
 -- @ end iterf.tex
-iterFwdRw rw3 = wrapFRewrites iter rw3
- where
-    iter rw n f = liftM (liftM fwdRes) (rw n f)
-    fwdRes (FwdRew g rw3a) = 
-      FwdRew g (rw3a `thenFwdRw` iterFwdRw rw3)
+iterFwdRw rw3 = wrapFR iter rw3
+ where iter rw n = (liftM $ liftM $ fadd_rw (iterFwdRw rw3)) . rw n
+       _iter = frewrite_cps (return . Just . fadd_rw (iterFwdRw rw3)) (return Nothing)
 
-----------------------------------------------------------------
-type BwdRes m n f e x = Maybe (BwdRew m n f e x)
+-- | Function inspired by 'rew' in the paper
+frewrite_cps :: Monad m
+             => ((Graph n e x, FwdRewrite m n f) -> m a)
+             -> m a
+             -> (forall e x . n e x -> f -> m (Maybe (Graph n e x, FwdRewrite m n f)))
+             -> n e x
+             -> f
+             -> m a
+frewrite_cps j n rw node f =
+    do mg <- rw node f
+       case mg of Nothing -> n
+                  Just gr -> j gr
 
-type SBRW m n f e x = n e x -> Fact x f -> m (Maybe (Graph n e x))
-type BRW  m n f e x = n e x -> Fact x f -> m (BwdRes m n f e x)
-type SimpleBwdRewrite3 m n f = ExTriple ( SBRW m n f)
-type SimpleBwdRewrite m n f = forall e x . SBRW m n f e x
-type LiftBRW m n f e x = SBRW m n f e x -> BRW m n f e x
-type MapBRW  m n f e x = BRW  m n f e x -> BRW m n f e x
-type MapBRW2 m n f e x = BRW  m n f e x -> BRW m n f e x -> BRW m n f e x
 
-----------------------------------------------------------------
 
-wrapSBRewrite3 :: ExTriple (LiftBRW m n f) -> SimpleBwdRewrite3 m n f -> BwdRewrite m n f
-wrapSBRewrite3 lift rw = uncurry3 mkBRewrite3 $ apply lift rw
-
-wrapBRewrite3 :: ExTriple (MapBRW m n f) -> BwdRewrite m n f -> BwdRewrite m n f
-wrapBRewrite3 map rw = uncurry3 mkBRewrite3 $ apply map $ getBRewrite3 rw
-
-wrapBRewrites2 :: ExTriple (MapBRW2 m n f) -> BR m n f -> BR m n f -> BR m n f
-wrapBRewrites2 map rw1 rw2 =
-  uncurry3 mkBRewrite3 $ (applyBinary map `on` getBRewrite3) rw1 rw2
-
--- Combinators for higher-rank rewriting functions:
-wrapSBRewrites' :: (forall e x . LiftBRW m n f e x) -> SimpleBwdRewrite3 m n f -> BR m n f
-wrapSBRewrites' lift = wrapSBRewrite3 (lift, lift, lift)
-
-wrapBRewrites' :: (forall e x . MapBRW m n f e x) -> BwdRewrite m n f -> BwdRewrite m n f
-wrapBRewrites' map = wrapBRewrite3 (map, map, map)
-
-wrapBRewrites2' :: (forall e x . MapBRW2 m n f e x) -> BR m n f -> BR m n f -> BR m n f
-wrapBRewrites2' map = wrapBRewrites2 (map, map, map)
+-- | Function inspired by 'add' in the paper
+fadd_rw :: Monad m
+       => FwdRewrite m n f
+       -> (Graph n e x, FwdRewrite m n f)
+       -> (Graph n e x, FwdRewrite m n f)
+fadd_rw rw2 (g, rw1) = (g, rw1 `thenFwdRw` rw2)
 
 ----------------------------------------------------------------
 
-noBwdRewrite :: Monad m => BwdRewrite m n f
-noBwdRewrite = mkBRewrite $ \ _ _ -> return Nothing
-
-shallowBwdRw3 :: Monad m => SimpleBwdRewrite3 m n f -> BwdRewrite m n f
-shallowBwdRw3 rw = wrapSBRewrites' lift rw
-  where lift rw n f = liftM (liftM (flip BwdRew noBwdRewrite)) (rw n f)
-
-shallowBwdRw :: Monad m => SimpleBwdRewrite m n f -> BwdRewrite m n f
-shallowBwdRw f = shallowBwdRw3 (f, f, f)
-
-deepBwdRw3 :: Monad m => SimpleBwdRewrite3 m n f -> BwdRewrite m n f
-deepBwdRw  :: Monad m => SimpleBwdRewrite  m n f -> BwdRewrite m n f
-deepBwdRw3 r = iterBwdRw (shallowBwdRw3 r)
-deepBwdRw  f = deepBwdRw3 (f, f, f)
+deepBwdRw3 :: FuelMonad m
+           => (n C O -> f          -> m (Maybe (Graph n C O)))
+           -> (n O O -> f          -> m (Maybe (Graph n O O)))
+           -> (n O C -> FactBase f -> m (Maybe (Graph n O C)))
+           -> (BwdRewrite m n f)
+deepBwdRw  :: FuelMonad m
+           => (forall e x . n e x -> Fact x f -> m (Maybe (Graph n e x)))
+           -> BwdRewrite m n f
+deepBwdRw3 f m l = iterBwdRw $ mkBRewrite3 f m l
+deepBwdRw  f = deepBwdRw3 f f f
 
 
 thenBwdRw :: Monad m => BwdRewrite m n f -> BwdRewrite m n f -> BwdRewrite m n f
-thenBwdRw rw1 rw2 = wrapBRewrites2' f rw1 rw2
-  where f rw1 rw2' n f = do
+thenBwdRw rw1 rw2 = wrapBR2 f rw1 rw2
+  where f _ rw1 rw2' n f = do
           res1 <- rw1 n f
           case res1 of
-            Nothing              -> rw2' n f
-            Just (BwdRew g rw1a) -> return $ Just $ BwdRew g (rw1a `thenBwdRw` rw2)
+            Nothing -> rw2' n f
+            Just gr -> return $ Just $ badd_rw rw2 gr
 
 iterBwdRw :: Monad m => BwdRewrite m n f -> BwdRewrite m n f
-iterBwdRw rw = wrapBRewrites' f rw
-  where f rw' n f = liftM (liftM iterRewrite) (rw' n f)
-        iterRewrite (BwdRew g rw2) = BwdRew g (rw2 `thenBwdRw` iterBwdRw rw)
+iterBwdRw rw = wrapBR f rw
+  where f _ rw' n f = liftM (liftM (badd_rw (iterBwdRw rw))) (rw' n f)
 
+-- | Function inspired by 'add' in the paper
+badd_rw :: Monad m
+       => BwdRewrite m n f
+       -> (Graph n e x, BwdRewrite m n f)
+       -> (Graph n e x, BwdRewrite m n f)
+badd_rw rw2 (g, rw1) = (g, rw1 `thenBwdRw` rw2)
+
+
 -- @ start pairf.tex
 pairFwd :: Monad m
         => FwdPass m n f
@@ -201,14 +129,14 @@
                 bot2 = fact_bot (fp_lattice pass2)
         (tf1, tm1, tl1) = getFTransfer3 (fp_transfer pass1)
         (tf2, tm2, tl2) = getFTransfer3 (fp_transfer pass2)
-    rewrite = liftRW (fp_rewrite pass1) fst `thenFwdRw` liftRW (fp_rewrite pass2) snd
+    rewrite = lift fst (fp_rewrite pass1) `thenFwdRw` lift snd (fp_rewrite pass2) 
       where
-        liftRW rws proj = mkFRewrite3 (lift f) (lift m) (lift l)
-          where lift rw n f = liftM (liftM projRewrite) $ rw n (proj f)
-                projRewrite (FwdRew g rws') = FwdRew g $ liftRW rws' proj
-                (f, m, l) = getFRewrite3 rws
+        lift proj = wrapFR project
+          where project rw = \n pair -> liftM (liftM repair) $ rw n (proj pair)
+                repair (g, rw') = (g, lift proj rw')
 
-pairBwd :: forall m n f f' . Monad m => BwdPass m n f -> BwdPass m n f' -> BwdPass m n (f, f')
+pairBwd :: forall m n f f' . 
+           Monad m => BwdPass m n f -> BwdPass m n f' -> BwdPass m n (f, f')
 pairBwd pass1 pass2 = BwdPass lattice transfer rewrite
   where
     lattice = pairLattice (bp_lattice pass1) (bp_lattice pass2)
@@ -218,15 +146,27 @@
         tfb t1 t2 n fb = (t1 n $ mapMap fst fb, t2 n $ mapMap snd fb)
         (tf1, tm1, tl1) = getBTransfer3 (bp_transfer pass1)
         (tf2, tm2, tl2) = getBTransfer3 (bp_transfer pass2)
-    rewrite = liftRW (bp_rewrite pass1) fst `thenBwdRw` liftRW (bp_rewrite pass2) snd
+    rewrite = lift fst (bp_rewrite pass1) `thenBwdRw` lift snd (bp_rewrite pass2) 
       where
-        liftRW :: forall f1 . BwdRewrite m n f1 -> ((f, f') -> f1) -> BwdRewrite m n (f, f')
-        liftRW rws proj = mkBRewrite3 (lift proj f) (lift proj m) (lift (mapMap proj) l)
-          where lift proj' rw n f = liftM (liftM projRewrite) $ rw n (proj' f)
-                projRewrite (BwdRew g rws') = BwdRew g $ liftRW rws' proj
-                (f, m, l) = getBRewrite3 rws
+       lift :: forall f1 .
+                ((f, f') -> f1) -> BwdRewrite m n f1 -> BwdRewrite m n (f, f')
+       lift proj = wrapBR project
+        where project :: forall e x . Shape x 
+               -> (n e x ->
+                       Fact x f1     -> m (Maybe (Graph n e x, BwdRewrite m n f1)))
+               -> (n e x ->
+                       Fact x (f,f') -> m (Maybe (Graph n e x, BwdRewrite m n (f,f'))))
+              project Open = 
+                 \rw n pair -> liftM (liftM repair) $ rw n (       proj pair)
+              project Closed = 
+                 \rw n pair -> liftM (liftM repair) $ rw n (mapMap proj pair)
+              repair (g, rw') = (g, lift proj rw')
+                -- XXX specialize repair so that the cost
+                -- of discriminating is one per combinator not one
+                -- per rewrite
 
-pairLattice :: forall f f' . DataflowLattice f -> DataflowLattice f' -> DataflowLattice (f, f')
+pairLattice :: forall f f' .
+               DataflowLattice f -> DataflowLattice f' -> DataflowLattice (f, f')
 pairLattice l1 l2 =
   DataflowLattice
     { fact_name = fact_name l1 ++ " x " ++ fact_name l2
diff --git a/Compiler/Hoopl/Dataflow.hs b/Compiler/Hoopl/Dataflow.hs
--- a/Compiler/Hoopl/Dataflow.hs
+++ b/Compiler/Hoopl/Dataflow.hs
@@ -1,18 +1,25 @@
 {-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs, EmptyDataDecls, PatternGuards, TypeFamilies, MultiParamTypeClasses #-}
 
 module Compiler.Hoopl.Dataflow
-  ( DataflowLattice(..), JoinFun, OldFact(..), NewFact(..), Fact
+  ( DataflowLattice(..), JoinFun, OldFact(..), NewFact(..), Fact, mkFactBase
   , ChangeFlag(..), changeIf
   , FwdPass(..), FwdTransfer, mkFTransfer, mkFTransfer3, getFTransfer3
-  , FwdRew(..),  FwdRewrite,  mkFRewrite,  mkFRewrite3,  getFRewrite3
+  -- * Respecting Fuel
+
+  -- $fuel
+  , FwdRewrite,  mkFRewrite,  mkFRewrite3,  getFRewrite3, noFwdRewrite
+  , wrapFR, wrapFR2
   , BwdPass(..), BwdTransfer, mkBTransfer, mkBTransfer3, getBTransfer3
-  , BwdRew(..),  BwdRewrite,  mkBRewrite,  mkBRewrite3,  getBRewrite3
+  , wrapBR, wrapBR2
+  , BwdRewrite,  mkBRewrite,  mkBRewrite3,  getBRewrite3, noBwdRewrite
   , analyzeAndRewriteFwd,  analyzeAndRewriteBwd
   )
 where
 
+import Control.Monad
 import Data.Maybe
 
+import Compiler.Hoopl.Checkpoint
 import Compiler.Hoopl.Collections
 import Compiler.Hoopl.Fuel
 import Compiler.Hoopl.Graph hiding (Graph) -- hiding so we can redefine
@@ -22,7 +29,7 @@
 import Compiler.Hoopl.Util
 
 -----------------------------------------------------------------------------
---		DataflowLattice
+--              DataflowLattice
 -----------------------------------------------------------------------------
 
 data DataflowLattice a = DataflowLattice  
@@ -45,8 +52,22 @@
 changeIf :: Bool -> ChangeFlag
 changeIf changed = if changed then SomeChange else NoChange
 
+
+-- | 'mkFactBase' creates a 'FactBase' from a list of ('Label', fact)
+-- pairs.  If the same label appears more than once, the relevant facts
+-- are joined.
+
+mkFactBase :: DataflowLattice f -> [(Label, f)] -> FactBase f
+mkFactBase lattice = foldl add mapEmpty
+  where add map (lbl, f) = mapInsert lbl newFact map
+          where newFact = case mapLookup lbl map of
+                            Nothing -> f
+                            Just f' -> snd $ join lbl (OldFact f') (NewFact f)
+                join = fact_join lattice
+
+
 -----------------------------------------------------------------------------
---		Analyze and rewrite forward: the interface
+--              Analyze and rewrite forward: the interface
 -----------------------------------------------------------------------------
 
 data FwdPass m n f
@@ -61,16 +82,35 @@
                      , n O C -> f -> FactBase f
                      ) }
 
-newtype FwdRewrite m n f 
+newtype FwdRewrite m n f   -- see Note [Respects Fuel]
   = FwdRewrite3 { getFRewrite3 ::
-                    ( n C O -> f -> m (Maybe (FwdRew m n f C O))
-                    , n O O -> f -> m (Maybe (FwdRew m n f O O))
-                    , n O C -> f -> m (Maybe (FwdRew m n f O C))
+                    ( n C O -> f -> m (Maybe (Graph n C O, FwdRewrite m n f))
+                    , n O O -> f -> m (Maybe (Graph n O O, FwdRewrite m n f))
+                    , n O C -> f -> m (Maybe (Graph n O C, FwdRewrite m n f))
                     ) }
-data FwdRew m n f e x = FwdRew (Graph n e x) (FwdRewrite m n f)
 
-  -- result of a rewrite is a new graph and a (possibly) new rewrite function
+wrapFR :: (forall e x. (n  e x -> f  -> m  (Maybe (Graph n  e x, FwdRewrite m  n  f )))
+                    -> (n' e x -> f' -> m' (Maybe (Graph n' e x, FwdRewrite m' n' f')))
+          )
+            -- ^ This argument may assume that any function passed to it
+            -- respects fuel, and it must return a result that respects fuel.
+       -> FwdRewrite m  n  f 
+       -> FwdRewrite m' n' f'      -- see Note [Respects Fuel]
+wrapFR wrap (FwdRewrite3 (f, m, l)) = FwdRewrite3 (wrap f, wrap m, wrap l)
+wrapFR2 
+  :: (forall e x . (n1 e x -> f1 -> m1 (Maybe (Graph n1 e x, FwdRewrite m1 n1 f1))) ->
+                   (n2 e x -> f2 -> m2 (Maybe (Graph n2 e x, FwdRewrite m2 n2 f2))) ->
+                   (n3 e x -> f3 -> m3 (Maybe (Graph n3 e x, FwdRewrite m3 n3 f3)))
+     )
+            -- ^ This argument may assume that any function passed to it
+            -- respects fuel, and it must return a result that respects fuel.
+  -> FwdRewrite m1 n1 f1
+  -> FwdRewrite m2 n2 f2
+  -> FwdRewrite m3 n3 f3      -- see Note [Respects Fuel]
+wrapFR2 wrap2 (FwdRewrite3 (f1, m1, l1)) (FwdRewrite3 (f2, m2, l2)) =
+    FwdRewrite3 (wrap2 f1 f2, wrap2 m1 m2, wrap2 l1 l2)
 
+
 mkFTransfer3 :: (n C O -> f -> f)
              -> (n O O -> f -> f)
              -> (n O C -> f -> FactBase f)
@@ -80,15 +120,30 @@
 mkFTransfer :: (forall e x . n e x -> f -> Fact x f) -> FwdTransfer n f
 mkFTransfer f = FwdTransfer3 (f, f, f)
 
-mkFRewrite3 :: (n C O -> f -> m (Maybe (FwdRew m n f C O)))
-            -> (n O O -> f -> m (Maybe (FwdRew m n f O O)))
-            -> (n O C -> f -> m (Maybe (FwdRew m n f O C)))
+-- | Functions passed to 'mkFRewrite3' should not be aware of the fuel supply.
+-- The result returned by 'mkFRewrite3' respects fuel.
+mkFRewrite3 :: FuelMonad m
+            => (n C O -> f -> m (Maybe (Graph n C O)))
+            -> (n O O -> f -> m (Maybe (Graph n O O)))
+            -> (n O C -> f -> m (Maybe (Graph n O C)))
             -> FwdRewrite m n f
-mkFRewrite3 f m l = FwdRewrite3 (f, m, l)
+mkFRewrite3 f m l = FwdRewrite3 (lift f, lift m, lift l)
+  where lift rw node fact = liftM (liftM asRew) (withFuel =<< rw node fact)
+        asRew g = (g, noFwdRewrite)
 
-mkFRewrite :: (forall e x . n e x -> f -> m (Maybe (FwdRew m n f e x)))
+noFwdRewrite :: Monad m => FwdRewrite m n f
+noFwdRewrite = FwdRewrite3 (noRewrite, noRewrite, noRewrite)
+
+noRewrite :: Monad m => a -> b -> m (Maybe c)
+noRewrite _ _ = return Nothing
+
+                               
+
+-- | Functions passed to 'mkFRewrite' should not be aware of the fuel supply.
+-- The result returned by 'mkFRewrite' respects fuel.
+mkFRewrite :: FuelMonad m => (forall e x . n e x -> f -> m (Maybe (Graph n e x)))
            -> FwdRewrite m n f
-mkFRewrite f = FwdRewrite3 (f, f, f)
+mkFRewrite f = mkFRewrite3 f f f
 
 
 type family   Fact x f :: *
@@ -98,7 +153,7 @@
 -- | if the graph being analyzed is open at the entry, there must
 --   be no other entry point, or all goes horribly wrong...
 analyzeAndRewriteFwd
-   :: forall m n f e x entries. (FuelMonad m, NonLocal n, LabelsPtr entries)
+   :: forall m n f e x entries. (CheckpointMonad m, NonLocal n, LabelsPtr entries)
    => FwdPass m n f
    -> MaybeC e entries
    -> Graph n e x -> Fact e f
@@ -123,7 +178,7 @@
 type Entries e = MaybeC e [Label]
 
 arfGraph :: forall m n f e x .
-            (NonLocal n, FuelMonad m) => FwdPass m n f -> 
+            (NonLocal n, CheckpointMonad m) => FwdPass m n f -> 
             Entries e -> Graph n e x -> Fact e f -> m (DG f n e x, Fact x f)
 arfGraph pass entries = graph
   where
@@ -132,9 +187,14 @@
     type ARFX thing = forall e x . thing e x -> Fact e f -> m (DG f n e x, Fact x f)
     -}
     graph ::              Graph n e x -> Fact e f -> m (DG f n e x, Fact x f)
-    block :: forall e x . Block n e x -> f        -> m (DG f n e x, Fact x f)
-    node  :: forall e x . (ShapeLifter e x) 
-                       => n e x       -> f        -> m (DG f n e x, Fact x f)
+-- @ start block.tex -2
+    block :: forall e x . 
+             Block n e x -> f -> m (DG f n e x, Fact x f)
+-- @ end block.tex
+-- @ start node.tex -4
+    node :: forall e x . (ShapeLifter e x) 
+         => n e x -> f -> m (DG f n e x, Fact x f)
+-- @ end node.tex
 -- @ start bodyfun.tex
     body  :: [Label] -> LabelMap (Block n C C)
           -> Fact C f -> m (DG f n C C, Fact C f)
@@ -142,10 +202,12 @@
                     -- Outgoing factbase is restricted to Labels *not* in
                     -- in the Body; the facts for Labels *in*
                     -- the Body are in the 'DG f n C C'
-    cat :: forall m e a x info info' info''. Monad m =>
-           (info  -> m (DG f n e a, info'))
-        -> (info' -> m (DG f n a x, info''))
-        -> (info  -> m (DG f n e x, info''))
+-- @ start cat.tex -2
+    cat :: forall e a x f1 f2 f3. 
+           (f1 -> m (DG f n e a, f2))
+        -> (f2 -> m (DG f n a x, f3))
+        -> (f1 -> m (DG f n e x, f3))
+-- @ end cat.tex
 
     graph GNil            = \f -> return (dgnil, f)
     graph (GUnit blk)     = block blk
@@ -163,30 +225,37 @@
              c _ _ = error "bogus GADT pattern match failure"
 
     -- Lift from nodes to blocks
+-- @ start block.tex -2
     block (BFirst  n)  = node n
     block (BMiddle n)  = node n
     block (BLast   n)  = node n
     block (BCat b1 b2) = block b1 `cat` block b2
+-- @ end block.tex
     block (BHead h n)  = block h  `cat` node n
     block (BTail n t)  = node  n  `cat` block t
     block (BClosed h t)= block h  `cat` block t
 
+-- @ start node.tex -4
     node n f
-      = do { fwdres <- withFuel =<< frewrite pass n f
-           ; case fwdres of
-               Nothing -> return (toDg f (toBlock n),
-                                  ftransfer pass n f)
-               Just (FwdRew g rw) ->
-                   let pass' = pass { fp_rewrite = rw }
-                   in  arfGraph pass' (maybeEntry n) g (fwdEntryFact n f) }
+     = do { grw <- frewrite pass n f
+          ; case grw of
+              Nothing -> return ( singletonDG f n
+                                , ftransfer pass n f )
+              Just (g, rw) ->
+                  let pass' = pass { fp_rewrite = rw }
+                      f'    = fwdEntryFact n f
+                  in  arfGraph pass' (fwdEntryLabel n) g f' }
 
+-- @ end node.tex
+
     -- | Compose fact transformers and concatenate the resulting
     -- rewritten graphs.
     {-# INLINE cat #-} 
+-- @ start cat.tex -2
     cat ft1 ft2 f = do { (g1,f1) <- ft1 f
                        ; (g2,f2) <- ft2 f1
                        ; return (g1 `dgSplice` g2, f2) }
-
+-- @ end cat.tex
     arfx :: forall thing x .
             NonLocal thing
          => (thing C x ->        f -> m (DG f n C x, Fact x f))
@@ -198,7 +267,7 @@
 
 
                     -- Outgoing factbase is restricted to Labels *not* in
-    		    -- in the Body; the facts for Labels *in*
+                    -- in the Body; the facts for Labels *in*
                     -- the Body are in the 'DG f n C C'
 -- @ start bodyfun.tex
     body entries blockmap init_fbase
@@ -215,8 +284,8 @@
 -- We know the results _shouldn't change_, but the transfer
 -- functions might, for example, generate some debugging traces.
 joinInFacts :: DataflowLattice f -> FactBase f -> FactBase f
-joinInFacts (DataflowLattice {fact_bot = bot, fact_join = fj}) fb =
-  mkFactBase $ map botJoin $ mapToList fb
+joinInFacts (lattice @ DataflowLattice {fact_bot = bot, fact_join = fj}) fb =
+  mkFactBase lattice $ map botJoin $ mapToList fb
     where botJoin (l, f) = (l, snd $ fj l (OldFact bot) (NewFact f))
 
 forwardBlockList :: (NonLocal n, LabelsPtr entry)
@@ -226,7 +295,7 @@
 forwardBlockList entries blks = postorder_dfs_from blks entries
 
 -----------------------------------------------------------------------------
---		Backward analysis and rewriting: the interface
+--              Backward analysis and rewriting: the interface
 -----------------------------------------------------------------------------
 
 data BwdPass m n f
@@ -242,13 +311,37 @@
                      ) }
 newtype BwdRewrite m n f 
   = BwdRewrite3 { getBRewrite3 ::
-                    ( n C O -> f          -> m (Maybe (BwdRew m n f C O))
-                    , n O O -> f          -> m (Maybe (BwdRew m n f O O))
-                    , n O C -> FactBase f -> m (Maybe (BwdRew m n f O C))
+                    ( n C O -> f          -> m (Maybe (Graph n C O, BwdRewrite m n f))
+                    , n O O -> f          -> m (Maybe (Graph n O O, BwdRewrite m n f))
+                    , n O C -> FactBase f -> m (Maybe (Graph n O C, BwdRewrite m n f))
                     ) }
-data BwdRew m n f e x = BwdRew (Graph n e x) (BwdRewrite m n f)
 
+wrapBR :: (forall e x .
+                Shape x 
+             -> (n  e x -> Fact x f  -> m  (Maybe (Graph n  e x, BwdRewrite m  n  f )))
+             -> (n' e x -> Fact x f' -> m' (Maybe (Graph n' e x, BwdRewrite m' n' f')))
+          )
+            -- ^ This argument may assume that any function passed to it
+            -- respects fuel, and it must return a result that respects fuel.
+       -> BwdRewrite m  n  f 
+       -> BwdRewrite m' n' f'      -- see Note [Respects Fuel]
+wrapBR wrap (BwdRewrite3 (f, m, l)) = 
+  BwdRewrite3 (wrap Open f, wrap Open m, wrap Closed l)
 
+wrapBR2 :: (forall e x . Shape x
+            -> (n1 e x -> Fact x f1 -> m1 (Maybe (Graph n1 e x, BwdRewrite m1 n1 f1)))
+            -> (n2 e x -> Fact x f2 -> m2 (Maybe (Graph n2 e x, BwdRewrite m2 n2 f2)))
+            -> (n3 e x -> Fact x f3 -> m3 (Maybe (Graph n3 e x, BwdRewrite m3 n3 f3))))
+            -- ^ This argument may assume that any function passed to it
+            -- respects fuel, and it must return a result that respects fuel.
+        -> BwdRewrite m1 n1 f1
+        -> BwdRewrite m2 n2 f2
+        -> BwdRewrite m3 n3 f3      -- see Note [Respects Fuel]
+wrapBR2 wrap2 (BwdRewrite3 (f1, m1, l1)) (BwdRewrite3 (f2, m2, l2)) =
+    BwdRewrite3 (wrap2 Open f1 f2, wrap2 Open m1 m2, wrap2 Closed l1 l2)
+
+
+
 mkBTransfer3 :: (n C O -> f -> f) -> (n O O -> f -> f) ->
                 (n O C -> FactBase f -> f) -> BwdTransfer n f
 mkBTransfer3 f m l = BwdTransfer3 (f, m, l)
@@ -256,23 +349,34 @@
 mkBTransfer :: (forall e x . n e x -> Fact x f -> f) -> BwdTransfer n f
 mkBTransfer f = BwdTransfer3 (f, f, f)
 
-mkBRewrite3 :: (n C O -> f          -> m (Maybe (BwdRew m n f C O)))
-            -> (n O O -> f          -> m (Maybe (BwdRew m n f O O)))
-            -> (n O C -> FactBase f -> m (Maybe (BwdRew m n f O C)))
+-- | Functions passed to 'mkBRewrite3' should not be aware of the fuel supply.
+-- The result returned by 'mkBRewrite3' respects fuel.
+mkBRewrite3 :: FuelMonad m
+            => (n C O -> f          -> m (Maybe (Graph n C O)))
+            -> (n O O -> f          -> m (Maybe (Graph n O O)))
+            -> (n O C -> FactBase f -> m (Maybe (Graph n O C)))
             -> BwdRewrite m n f
-mkBRewrite3 f m l = BwdRewrite3 (f, m, l)
+mkBRewrite3 f m l = BwdRewrite3 (lift f, lift m, lift l)
+  where lift rw node fact = liftM (liftM asRew) (withFuel =<< rw node fact)
+        asRew g = (g, noBwdRewrite)
 
-mkBRewrite :: (forall e x . n e x -> Fact x f -> m (Maybe (BwdRew m n f e x)))
+noBwdRewrite :: Monad m => BwdRewrite m n f
+noBwdRewrite = BwdRewrite3 (noRewrite, noRewrite, noRewrite)
+
+-- | Functions passed to 'mkBRewrite' should not be aware of the fuel supply.
+-- The result returned by 'mkBRewrite' respects fuel.
+mkBRewrite :: FuelMonad m 
+           => (forall e x . n e x -> Fact x f -> m (Maybe (Graph n e x)))
            -> BwdRewrite m n f
-mkBRewrite f = BwdRewrite3 (f, f, f)
+mkBRewrite f = mkBRewrite3 f f f
 
 
 -----------------------------------------------------------------------------
---		Backward implementation
+--              Backward implementation
 -----------------------------------------------------------------------------
 
 arbGraph :: forall m n f e x .
-            (NonLocal n, FuelMonad m) => BwdPass m n f -> 
+            (NonLocal n, CheckpointMonad m) => BwdPass m n f -> 
             Entries e -> Graph n e x -> Fact x f -> m (DG f n e x, Fact e f)
 arbGraph pass entries = graph
   where
@@ -315,13 +419,13 @@
     block (BClosed h t)= block h  `cat` block t
 
     node n f
-      = do { bwdres <- withFuel =<< brewrite pass n f
+      = do { bwdres <- brewrite pass n f
            ; case bwdres of
-               Nothing -> return (toDg entry_f (toBlock n), entry_f)
+               Nothing -> return (singletonDG entry_f n, entry_f)
                             where entry_f = btransfer pass n f
-               Just (BwdRew g rw) ->
+               Just (g, rw) ->
                           do { let pass' = pass { bp_rewrite = rw }
-                             ; (g, f) <- arbGraph pass' (maybeEntry n) g f
+                             ; (g, f) <- arbGraph pass' (fwdEntryLabel n) g f
                              ; return (g, bwdEntryFact (bp_lattice pass) n f)} }
 
     -- | Compose fact transformers and concatenate the resulting
@@ -343,7 +447,7 @@
      -- joinInFacts adds debugging information
 
                     -- Outgoing factbase is restricted to Labels *not* in
-    		    -- in the Body; the facts for Labels *in*
+                    -- in the Body; the facts for Labels *in*
                     -- the Body are in the 'DG f n C C'
     body entries blockmap init_fbase
       = fixpoint Bwd (bp_lattice pass) do_block blocks init_fbase
@@ -376,7 +480,7 @@
 -- | if the graph being analyzed is open at the exit, I don't
 --   quite understand the implications of possible other exits
 analyzeAndRewriteBwd
-   :: (FuelMonad m, NonLocal n, LabelsPtr entries)
+   :: (CheckpointMonad m, NonLocal n, LabelsPtr entries)
    => BwdPass m n f
    -> MaybeC e entries -> Graph n e x -> Fact x f
    -> m (Graph n e x, FactBase f, MaybeO e f)
@@ -396,13 +500,15 @@
 -----------------------------------------------------------------------------
 --      fixpoint: finding fixed points
 -----------------------------------------------------------------------------
+-- @ start txfb.tex
 data TxFactBase n f
   = TxFB { tfb_fbase :: FactBase f
          , tfb_rg    :: DG f n C C -- Transformed blocks
          , tfb_cha   :: ChangeFlag
          , tfb_lbls  :: LabelSet }
+-- @ end txfb.tex
      -- See Note [TxFactBase invariants]
-
+-- @ start update.tex
 updateFact :: DataflowLattice f -> LabelSet
            -> Label -> f -> (ChangeFlag, FactBase f)
            -> (ChangeFlag, FactBase f)
@@ -421,35 +527,33 @@
                    (OldFact old_fact) (NewFact new_fact)
                (_, new_fact_debug) = join (fact_bot lat)
     new_fbase = mapInsert lbl res_fact fbase
+-- @ end update.tex
 
-{-  this type is too general for the paper :-( 
-fixpoint :: forall m block n f. 
-            (FuelMonad m, NonLocal n, NonLocal (block n))
-         => Direction
-         -> DataflowLattice f
-         -> (block n C C -> FactBase f
-             -> m (DG f n C C, [(Label, f)]))
-         -> [block n C C]
-         -> FactBase f 
-         -> m (DG f n C C, FactBase f)
+
+{-
+-- this doesn't work because it can't be implemented
+class Monad m => FixpointMonad m where
+  observeChangedFactBase :: m (Maybe (FactBase f)) -> Maybe (FactBase f)
 -}
+
 -- @ start fptype.tex
 data Direction = Fwd | Bwd
-fixpoint :: forall m n f. (FuelMonad m, NonLocal n)
+fixpoint :: forall m n f. (CheckpointMonad m, NonLocal n)
  => Direction
  -> DataflowLattice f
  -> (Block n C C -> Fact C f -> m (DG f n C C, Fact C f))
  -> [Block n C C]
  -> (Fact C f -> m (DG f n C C, Fact C f))
 -- @ end fptype.tex
+-- @ start fpimp.tex
 fixpoint direction lat do_block blocks init_fbase
-  = do { fuel <- getFuel  
-       ; tx_fb <- loop fuel init_fbase
+  = do { tx_fb <- loop init_fbase
        ; return (tfb_rg tx_fb, 
                  map (fst . fst) tagged_blocks 
                     `mapDeleteList` tfb_fbase tx_fb ) }
-	     -- The successors of the Graph are the the Labels for which
-	     -- we have facts, that are *not* in the blocks of the graph
+    -- The successors of the Graph are the the Labels 
+    -- for which we have facts and which are *not* in
+    -- the blocks of the graph
   where
     tagged_blocks = map tag blocks
     is_fwd = case direction of { Fwd -> True; 
@@ -474,23 +578,25 @@
         tx_fb@(TxFB { tfb_fbase = fbase, tfb_lbls = lbls
                     , tfb_rg = blks, tfb_cha = cha })
       | is_fwd && not (lbl `mapMember` fbase)
-      = return (tx_fb {tfb_lbls = lbls'})	-- Note [Unreachable blocks]
+      = return (tx_fb {tfb_lbls = lbls'})       -- Note [Unreachable blocks]
       | otherwise
       = do { (rg, out_facts) <- do_block blk fbase
-           ; let (cha',fbase') 
-                   = mapFoldWithKey (updateFact lat lbls) 
-                          (cha,fbase) out_facts
-           ; return (TxFB { tfb_lbls  = lbls'
-                          , tfb_rg    = rg `dgSplice` blks
-                          , tfb_fbase = fbase'
-                          , tfb_cha = cha' }) }
+           ; let (cha', fbase') = mapFoldWithKey
+                                  (updateFact lat lbls) 
+                                  (cha,fbase) out_facts
+           ; return $
+               TxFB { tfb_lbls  = lbls'
+                    , tfb_rg    = rg `dgSplice` blks
+                    , tfb_fbase = fbase'
+                    , tfb_cha = cha' } }
       where
         lbls' = lbls `setUnion` setFromList in_lbls
         
 
-    loop :: Fuel -> FactBase f -> m (TxFactBase n f)
-    loop fuel fbase 
-      = do { let init_tx = TxFB { tfb_fbase = fbase
+    loop :: FactBase f -> m (TxFactBase n f)
+    loop fbase 
+      = do { s <- checkpoint
+           ; let init_tx = TxFB { tfb_fbase = fbase
                                 , tfb_cha   = NoChange
                                 , tfb_rg    = dgnilC
                                 , tfb_lbls  = setEmpty }
@@ -498,9 +604,11 @@
            ; case tfb_cha tx_fb of
                NoChange   -> return tx_fb
                SomeChange 
-                 -> do { setFuel fuel
-                       ; loop fuel (tfb_fbase tx_fb) } }
+                 -> do { restart s
+                       ; loop (tfb_fbase tx_fb) } }
+-- @ end fpimp.tex           
 
+
 {-  Note [TxFactBase invariants]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The TxFactBase is used only during a fixpoint iteration (or "sweep"),
@@ -571,7 +679,7 @@
 -}
 
 -----------------------------------------------------------------------------
---	DG: an internal data type for 'decorated graphs'
+--      DG: an internal data type for 'decorated graphs'
 --          TOTALLY internal to Hoopl; each block is decorated with a fact
 -----------------------------------------------------------------------------
 
@@ -579,7 +687,6 @@
 type Graph = Graph' Block
 type DG f  = Graph' (DBlock f)
 data DBlock f n e x = DBlock f (Block n e x) -- ^ block decorated with fact
-toDg :: NonLocal n => f -> Block n e x -> DG f n e x
 -- @ end dg.tex
 instance NonLocal n => NonLocal (DBlock f n) where
   entryLabel (DBlock _ b) = entryLabel b
@@ -618,14 +725,6 @@
 dgnil  = GNil
 dgnilC = GMany NothingO emptyBody NothingO
 
-toDg f b@(BFirst  {}) = gUnitCO (DBlock f b)
-toDg f b@(BMiddle {}) = gUnitOO (DBlock f b)
-toDg f b@(BLast   {}) = gUnitOC (DBlock f b)
-toDg f b@(BCat {})    = gUnitOO (DBlock f b)
-toDg f b@(BHead {})   = gUnitCO (DBlock f b)
-toDg f b@(BTail {})   = gUnitOC (DBlock f b)
-toDg f b@(BClosed {}) = gUnitCC (DBlock f b)
-
 dgSplice = U.splice fzCat
   where fzCat (DBlock f b1) (DBlock _ b2) = DBlock f (b1 `U.cat` b2)
 
@@ -639,47 +738,72 @@
 -- Lowering back:
 --  - from fact-like things to facts
 -- Note that the latter two functions depend only on the entry shape.
+-- @ start node.tex
 class ShapeLifter e x where
-  toBlock      :: n e x -> Block n e x
-  fwdEntryFact :: NonLocal n =>                      n e x -> f -> Fact e f
-  bwdEntryFact :: NonLocal n => DataflowLattice f -> n e x -> Fact e f -> f
-  ftransfer    :: FwdPass m n f -> n e x -> f        -> Fact x f
-  btransfer    :: BwdPass m n f -> n e x -> Fact x f -> f
-  frewrite     :: FwdPass m n f -> n e x -> f        -> m (Maybe (FwdRew m n f e x))
-  brewrite     :: BwdPass m n f -> n e x -> Fact x f -> m (Maybe (BwdRew m n f e x))
-  maybeEntry   :: NonLocal n => n e x -> Entries e
+ singletonDG   :: f -> n e x -> DG f n e x
+ fwdEntryFact  :: NonLocal n => n e x -> f -> Fact e f
+ fwdEntryLabel :: NonLocal n => n e x -> MaybeC e [Label]
+ ftransfer :: FwdPass m n f -> n e x -> f -> Fact x f
+ frewrite  :: FwdPass m n f -> n e x 
+           -> f -> m (Maybe (Graph n e x, FwdRewrite m n f))
+-- @ end node.tex
+ bwdEntryFact :: NonLocal n => DataflowLattice f -> n e x -> Fact e f -> f
+ btransfer    :: BwdPass m n f -> n e x -> Fact x f -> f
+ brewrite     :: BwdPass m n f -> n e x
+              -> Fact x f -> m (Maybe (Graph n e x, BwdRewrite m n f))
 
 instance ShapeLifter C O where
-  toBlock         = BFirst
-  fwdEntryFact     n f  = mkFactBase [(entryLabel n, f)]
+  singletonDG f = gUnitCO . DBlock f . BFirst
+  fwdEntryFact     n f  = mapSingleton (entryLabel n) f
   bwdEntryFact lat n fb = getFact lat (entryLabel n) fb
   ftransfer (FwdPass {fp_transfer = FwdTransfer3 (ft, _, _)}) n f = ft n f
   btransfer (BwdPass {bp_transfer = BwdTransfer3 (bt, _, _)}) n f = bt n f
   frewrite  (FwdPass {fp_rewrite  = FwdRewrite3  (fr, _, _)}) n f = fr n f
   brewrite  (BwdPass {bp_rewrite  = BwdRewrite3  (br, _, _)}) n f = br n f
-  maybeEntry n = JustC [entryLabel n]
+  fwdEntryLabel n = JustC [entryLabel n]
 
 instance ShapeLifter O O where
-  toBlock      = BMiddle
+  singletonDG f = gUnitOO . DBlock f . BMiddle
   fwdEntryFact   _ f = f
   bwdEntryFact _ _ f = f
   ftransfer (FwdPass {fp_transfer = FwdTransfer3 (_, ft, _)}) n f = ft n f
   btransfer (BwdPass {bp_transfer = BwdTransfer3 (_, bt, _)}) n f = bt n f
   frewrite  (FwdPass {fp_rewrite  = FwdRewrite3  (_, fr, _)}) n f = fr n f
   brewrite  (BwdPass {bp_rewrite  = BwdRewrite3  (_, br, _)}) n f = br n f
-  maybeEntry _ = NothingC
+  fwdEntryLabel _ = NothingC
 
 instance ShapeLifter O C where
-  toBlock      = BLast
+  singletonDG f = gUnitOC . DBlock f . BLast
   fwdEntryFact   _ f = f
   bwdEntryFact _ _ f = f
   ftransfer (FwdPass {fp_transfer = FwdTransfer3 (_, _, ft)}) n f = ft n f
   btransfer (BwdPass {bp_transfer = BwdTransfer3 (_, _, bt)}) n f = bt n f
   frewrite  (FwdPass {fp_rewrite  = FwdRewrite3  (_, _, fr)}) n f = fr n f
   brewrite  (BwdPass {bp_rewrite  = BwdRewrite3  (_, _, br)}) n f = br n f
-  maybeEntry _ = NothingC
+  fwdEntryLabel _ = NothingC
 
 -- Fact lookup: the fact `orelse` bottom
 getFact  :: DataflowLattice f -> Label -> FactBase f -> f
 getFact lat l fb = case lookupFact l fb of Just  f -> f
                                            Nothing -> fact_bot lat
+
+
+
+{-  Note [Respects fuel]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-}
+-- $fuel
+-- A value of type 'FwdRewrite' or 'BwdRewrite' /respects fuel/ if 
+-- any function contained within the value satisfies the following properties:
+--
+--   * When fuel is exhausted, it always returns 'Nothing'.
+--
+--   * When it returns @Just g rw@, it consumes /exactly/ one unit
+--     of fuel, and new rewrite 'rw' also respects fuel.
+--
+-- Provided that functions passed to 'mkFRewrite', 'mkFRewrite3', 
+-- 'mkBRewrite', and 'mkBRewrite3' are not aware of the fuel supply,
+-- the results respect fuel.
+--
+-- It is an /unchecked/ run-time error for the argument passed to 'wrapFR',
+-- 'wrapFR2', 'wrapBR', or 'warpBR2' to return a function that does not respect fuel.
diff --git a/Compiler/Hoopl/Fuel.hs b/Compiler/Hoopl/Fuel.hs
--- a/Compiler/Hoopl/Fuel.hs
+++ b/Compiler/Hoopl/Fuel.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE TypeFamilies #-}
+
 -----------------------------------------------------------------------------
 --		The fuel monad
 -----------------------------------------------------------------------------
@@ -13,6 +15,7 @@
   )
 where
 
+import Compiler.Hoopl.Checkpoint
 import Compiler.Hoopl.Unique
 
 class Monad m => FuelMonad m where
@@ -46,6 +49,12 @@
   return a = FM (\f -> return (a, f))
   fm >>= k = FM (\f -> do { (a, f') <- unFM fm f; unFM (k a) f' })
 
+instance CheckpointMonad m => CheckpointMonad (CheckingFuelMonad m) where
+  type Checkpoint (CheckingFuelMonad m) = (Fuel, Checkpoint m)
+  checkpoint = FM $ \fuel -> do { s <- checkpoint
+                                ; return ((fuel, s), fuel) }
+  restart (fuel, s) = FM $ \_ -> do { restart s; return ((), fuel) }
+
 instance UniqueMonad m => UniqueMonad (CheckingFuelMonad m) where
   freshUnique = FM (\f -> do { l <- freshUnique; return (l, f) })
 
@@ -69,6 +78,13 @@
 instance Monad m => FuelMonad (InfiniteFuelMonad m) where
   getFuel   = return infiniteFuel
   setFuel _ = return ()
+
+instance CheckpointMonad m => CheckpointMonad (InfiniteFuelMonad m) where
+  type Checkpoint (InfiniteFuelMonad m) = Checkpoint m
+  checkpoint = IFM checkpoint
+  restart s  = IFM $ restart s
+
+
 
 instance FuelMonadT InfiniteFuelMonad where
   runWithFuel _ = unIFM
diff --git a/Compiler/Hoopl/Graph.hs b/Compiler/Hoopl/Graph.hs
--- a/Compiler/Hoopl/Graph.hs
+++ b/Compiler/Hoopl/Graph.hs
@@ -2,7 +2,7 @@
 
 module Compiler.Hoopl.Graph 
   ( O, C, Block(..), Body, Body'(..), Graph, Graph'(..)
-  , MaybeO(..), MaybeC(..), EitherCO
+  , MaybeO(..), MaybeC(..), Shape(..), IndexedCO
   , NonLocal(entryLabel, successors)
   , emptyBody, addBlock, bodyList
   )
@@ -71,10 +71,15 @@
   JustC    :: t -> MaybeC C t
   NothingC ::      MaybeC O t
 
+-- | Dynamic shape value
+data Shape ex where
+  Closed :: Shape C
+  Open   :: Shape O
+
 -- | Either type indexed by closed/open using type families
-type family   EitherCO e a b :: *
-type instance EitherCO C a b = a
-type instance EitherCO O a b = b
+type family IndexedCO ex a b :: *
+type instance IndexedCO C a b = a
+type instance IndexedCO O a b = b
 
 instance Functor (MaybeO ex) where
   fmap _ NothingO = NothingO
diff --git a/Compiler/Hoopl/Label.hs b/Compiler/Hoopl/Label.hs
--- a/Compiler/Hoopl/Label.hs
+++ b/Compiler/Hoopl/Label.hs
@@ -3,7 +3,7 @@
   ( Label
   , freshLabel
   , LabelSet, LabelMap
-  , FactBase, noFacts, mkFactBase, lookupFact
+  , FactBase, noFacts, lookupFact
 
   , uniqueToLbl -- MkGraph and GHC use only
   , lblToUnique -- GHC use only
@@ -99,9 +99,6 @@
 
 noFacts :: FactBase f
 noFacts = mapEmpty
-
-mkFactBase :: [(Label, f)] -> FactBase f
-mkFactBase = mapFromList
 
 lookupFact :: Label -> FactBase f -> Maybe f
 lookupFact = mapLookup
diff --git a/Compiler/Hoopl/Shape.hs b/Compiler/Hoopl/Shape.hs
new file mode 100644
--- /dev/null
+++ b/Compiler/Hoopl/Shape.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE GADTs, EmptyDataDecls #-}
+
+module Compiler.Hoopl.Shape {-# DEPRECATED "not ready to migrate to this yet" #-}
+where
+
+-- | Used at the type level to indicate an "open" structure with    
+-- a unique, unnamed control-flow edge flowing in or out.         
+-- "Fallthrough" and concatenation are permitted at an open point.
+data O 
+       
+       
+-- | Used at the type level to indicate a "closed" structure which
+-- supports control transfer only through the use of named
+-- labels---no "fallthrough" is permitted.  The number of control-flow
+-- edges is unconstrained.
+data C
+
+
+data HalfShape s where
+  ShapeO :: HalfShape O
+  ShapeC :: HalfShape C
+
+data Shape e x where
+  ShapeOO :: Shape O O
+  ShapeCO :: Shape C O
+  ShapeOC :: Shape O C
+  ShapeCC :: Shape C C
+
+class Shapely n where
+  shape        :: n e x -> Shape e x
+  shapeAtEntry :: n e x -> HalfShape e
+  shapeAtExit  :: n e x -> HalfShape x
+
+  shapeAtEntry = entryHalfShape . shape
+  shapeAtExit  = exitHalfShape  . shape
+  
+
+entryHalfShape :: Shape e x -> HalfShape e
+exitHalfShape  :: Shape e x -> HalfShape x
+
+entryHalfShape ShapeOO = ShapeO
+entryHalfShape ShapeOC = ShapeO
+entryHalfShape ShapeCO = ShapeC
+entryHalfShape ShapeCC = ShapeC
+
+exitHalfShape ShapeOO = ShapeO
+exitHalfShape ShapeOC = ShapeC
+exitHalfShape ShapeCO = ShapeO
+exitHalfShape ShapeCC = ShapeC
+
diff --git a/Compiler/Hoopl/Unique.hs b/Compiler/Hoopl/Unique.hs
--- a/Compiler/Hoopl/Unique.hs
+++ b/Compiler/Hoopl/Unique.hs
@@ -11,6 +11,7 @@
 
 where
 
+import Compiler.Hoopl.Checkpoint
 import Compiler.Hoopl.Collections
 
 import qualified Data.IntMap as M
@@ -106,6 +107,11 @@
 
 instance UniqueMonad SimpleUniqueMonad where
   freshUnique = SUM $ \(u:us) -> (u, us)
+
+instance CheckpointMonad SimpleUniqueMonad where
+  type Checkpoint SimpleUniqueMonad = [Unique]
+  checkpoint = SUM $ \us -> (us, us)
+  restart us = SUM $ \_  -> ((), us)
 
 runSimpleUniqueMonad :: SimpleUniqueMonad a -> a
 runSimpleUniqueMonad m = fst (unSUM m allUniques)
diff --git a/Compiler/Hoopl/Wrappers.hs b/Compiler/Hoopl/Wrappers.hs
new file mode 100644
--- /dev/null
+++ b/Compiler/Hoopl/Wrappers.hs
@@ -0,0 +1,7 @@
+module Compiler.Hoopl.Wrappers {-# DEPRECATED "Use only if you know what you are doing and can preserve the 'respects fuel' invariant" #-}
+  ( wrapFR, wrapFR2, wrapBR, wrapBR2
+  )
+where
+
+import Compiler.Hoopl.Dataflow
+
diff --git a/Compiler/Hoopl/XUtil.hs b/Compiler/Hoopl/XUtil.hs
--- a/Compiler/Hoopl/XUtil.hs
+++ b/Compiler/Hoopl/XUtil.hs
@@ -8,6 +8,7 @@
   , successorFacts
   , joinFacts
   , joinOutFacts -- deprecated
+  , joinMaps
   , foldGraphNodes
   , foldBlockNodesF, foldBlockNodesB, foldBlockNodesF3, foldBlockNodesB3
   , tfFoldBlock
@@ -24,11 +25,12 @@
   )
 where
 
+import qualified Data.Map as M
 import Data.Maybe
 
+import Compiler.Hoopl.Checkpoint
 import Compiler.Hoopl.Collections
 import Compiler.Hoopl.Dataflow
-import Compiler.Hoopl.Fuel
 import Compiler.Hoopl.Graph
 import Compiler.Hoopl.Label
 import Compiler.Hoopl.Util
@@ -38,7 +40,7 @@
 -- A set of entry points must be supplied; blocks not reachable from
 -- the set are thrown away.
 analyzeAndRewriteFwdBody
-   :: forall m n f entries. (FuelMonad m, NonLocal n, LabelsPtr entries)
+   :: forall m n f entries. (CheckpointMonad m, NonLocal n, LabelsPtr entries)
    => FwdPass m n f
    -> entries -> Body n -> FactBase f
    -> m (Body n, FactBase f)
@@ -47,7 +49,7 @@
 -- A set of entry points must be supplied; blocks not reachable from
 -- the set are thrown away.
 analyzeAndRewriteBwdBody
-   :: forall m n f entries. (FuelMonad m, NonLocal n, LabelsPtr entries)
+   :: forall m n f entries. (CheckpointMonad m, NonLocal n, LabelsPtr entries)
    => BwdPass m n f 
    -> entries -> Body n -> FactBase f 
    -> m (Body n, FactBase f)
@@ -82,7 +84,7 @@
 -- from having to specify a type signature for 'NothingO', which beginners
 -- might find confusing and experts might find annoying.
 analyzeAndRewriteFwdOx
-   :: forall m n f x. (FuelMonad m, NonLocal n)
+   :: forall m n f x. (CheckpointMonad m, NonLocal n)
    => FwdPass m n f -> Graph n O x -> f -> m (Graph n O x, FactBase f, MaybeO x f)
 
 -- | Backward dataflow analysis and rewriting for the special case of a 
@@ -90,7 +92,7 @@
 -- from having to specify a type signature for 'NothingO', which beginners
 -- might find confusing and experts might find annoying.
 analyzeAndRewriteBwdOx
-   :: forall m n f x. (FuelMonad m, NonLocal n)
+   :: forall m n f x. (CheckpointMonad m, NonLocal n)
    => BwdPass m n f -> Graph n O x -> Fact x f -> m (Graph n O x, FactBase f, f)
 
 -- | A value that can be used for the entry point of a graph open at the entry.
@@ -117,19 +119,23 @@
 -- | This utility function handles a common case in which a transfer function
 -- produces a single fact out of a last node, which is then distributed
 -- over the outgoing edges.
-distributeXfer :: NonLocal n => (n O C -> f -> f) -> (n O C -> f -> FactBase f)
-distributeXfer xfer n f = mkFactBase [ (l, xfer n f) | l <- successors n ]
+distributeXfer :: NonLocal n
+               => DataflowLattice f -> (n O C -> f -> f) -> (n O C -> f -> FactBase f)
+distributeXfer lattice xfer n f =
+    mkFactBase lattice [ (l, xfer n f) | l <- successors n ]
 
 -- | This utility function handles a common case in which a transfer function
 -- for a last node takes the incoming fact unchanged and simply distributes
 -- that fact over the outgoing edges.
 distributeFact :: NonLocal n => n O C -> f -> FactBase f
-distributeFact n f = mkFactBase [ (l, f) | l <- successors n ]
+distributeFact n f = mapFromList [ (l, f) | l <- successors n ]
+   -- because the same fact goes out on every edge,
+   -- there's no need for 'mkFactBase' here.
 
 -- | This utility function handles a common case in which a backward transfer
 -- function takes the incoming fact unchanged and tags it with the node's label.
 distributeFactBwd :: NonLocal n => n C O -> f -> FactBase f
-distributeFactBwd n f = mkFactBase [ (entryLabel n, f) ]
+distributeFactBwd n f = mapSingleton (entryLabel n) f
 
 -- | List of (unlabelled) facts from the successors of a last node
 successorFacts :: NonLocal n => n O C -> FactBase f -> [f]
@@ -148,16 +154,33 @@
   where join (lbl, new) old = snd $ fact_join lat lbl (OldFact old) (NewFact new)
         facts = [(s, fromJust fact) | s <- successors n, let fact = lookupFact s f, isJust fact]
 
--- | A fold function that relies on the EitherCO type function.
+
+-- | It's common to represent dataflow facts as a map from variables
+-- to some fact about the locations. For these maps, the join
+-- operation on the map can be expressed in terms of the join on each
+-- element of the codomain:
+joinMaps :: Ord k => JoinFun v -> JoinFun (M.Map k v)
+joinMaps eltJoin l (OldFact old) (NewFact new) = M.foldWithKey add (NoChange, old) new
+  where 
+    add k new_v (ch, joinmap) =
+      case M.lookup k joinmap of
+        Nothing    -> (SomeChange, M.insert k new_v joinmap)
+        Just old_v -> case eltJoin l (OldFact old_v) (NewFact new_v) of
+                        (SomeChange, v') -> (SomeChange, M.insert k v' joinmap)
+                        (NoChange,   _)  -> (ch, joinmap)
+
+
+
+-- | A fold function that relies on the IndexedCO type function.
 --   Note that the type parameter e is available to the functions
 --   that are applied to the middle and last nodes.
 tfFoldBlock :: forall n bc bo c e x .
                ( n C O -> bc
-               , n O O -> EitherCO e bc bo -> EitherCO e bc bo
-               , n O C -> EitherCO e bc bo -> c)
-            -> (Block n e x -> bo -> EitherCO x c (EitherCO e bc bo))
+               , n O O -> IndexedCO e bc bo -> IndexedCO e bc bo
+               , n O C -> IndexedCO e bc bo -> c)
+            -> (Block n e x -> bo -> IndexedCO x c (IndexedCO e bc bo))
 tfFoldBlock (f, m, l) bl bo = block bl
-  where block :: forall x . Block n e x -> EitherCO x c (EitherCO e bc bo)
+  where block :: forall x . Block n e x -> IndexedCO x c (IndexedCO e bc bo)
         block (BFirst  n)       = f n
         block (BMiddle n)       = m n bo
         block (BLast   n)       = l n bo
@@ -165,7 +188,7 @@
         block (b1 `BClosed` b2) = oblock b2 $ block b1
         block (b1 `BHead` n)    = m n $ block b1
         block (n `BTail` b2)    = oblock b2 $ m n bo
-        oblock :: forall x . Block n O x -> EitherCO e bc bo -> EitherCO x c (EitherCO e bc bo)
+        oblock :: forall x . Block n O x -> IndexedCO e bc bo -> IndexedCO x c (IndexedCO e bc bo)
         oblock (BMiddle n)       = m n
         oblock (BLast   n)       = l n
         oblock (b1 `BCat`    b2) = oblock b1 `cat` oblock b2
@@ -175,8 +198,8 @@
 
 type NodeList' e x n = (MaybeC e (n C O), [n O O], MaybeC x (n O C))
 blockToNodeList''' ::
-  forall n e x. ( EitherCO e (NodeList' C O n) (NodeList' O O n) ~ NodeList' e O n
-                , EitherCO x (NodeList' e C n) (NodeList' e O n) ~ NodeList' e x n) =>
+  forall n e x. ( IndexedCO e (NodeList' C O n) (NodeList' O O n) ~ NodeList' e O n
+                , IndexedCO x (NodeList' e C n) (NodeList' e O n) ~ NodeList' e x n) =>
     Block n e x -> NodeList' e x n
 blockToNodeList''' b = (h, reverse ms', t)
   where
@@ -259,14 +282,14 @@
          ( n C O       -> a -> b
          , n O O       -> b -> b
          , n O C       -> b -> c)
-      -> (forall e x . Block n e x -> EitherCO e a b -> EitherCO x c b)
+      -> (forall e x . Block n e x -> IndexedCO e a b -> IndexedCO x c b)
 fbnf3 (ff, fm, fl) block = unFF3 $ scottFoldBlock (ScottBlock f m l cat) block
     where f n = FF3 $ ff n
           m n = FF3 $ fm n
           l n = FF3 $ fl n
           FF3 f `cat` FF3 f' = FF3 $ f' . f
 
-newtype FF3 a b c e x = FF3 { unFF3 :: EitherCO e a b -> EitherCO x c b }
+newtype FF3 a b c e x = FF3 { unFF3 :: IndexedCO e a b -> IndexedCO x c b }
 
 blockToNodeList'' :: Block n e x -> (MaybeC e (n C O), [n O O], MaybeC x (n O C))
 blockToNodeList'' = finish . unList . scottFoldBlock (ScottBlock f m l cat)
@@ -349,18 +372,18 @@
                    ( n C O       -> a -> b
                    , n O O       -> b -> b
                    , n O C       -> b -> c)
-                 -> (forall e x . Block n e x -> EitherCO e a b -> EitherCO x c b)
+                 -> (forall e x . Block n e x -> IndexedCO e a b -> IndexedCO x c b)
 foldBlockNodesF  :: forall n a .
                     (forall e x . n e x       -> a -> a)
-                 -> (forall e x . Block n e x -> EitherCO e a a -> EitherCO x a a)
+                 -> (forall e x . Block n e x -> IndexedCO e a a -> IndexedCO x a a)
 foldBlockNodesB3 :: forall n a b c .
                    ( n C O       -> b -> c
                    , n O O       -> b -> b
                    , n O C       -> a -> b)
-                 -> (forall e x . Block n e x -> EitherCO x a b -> EitherCO e c b)
+                 -> (forall e x . Block n e x -> IndexedCO x a b -> IndexedCO e c b)
 foldBlockNodesB  :: forall n a .
                     (forall e x . n e x       -> a -> a)
-                 -> (forall e x . Block n e x -> EitherCO x a a -> EitherCO e a a)
+                 -> (forall e x . Block n e x -> IndexedCO x a a -> IndexedCO e a a)
 -- | Fold a function over every node in a graph.
 -- The fold function must be polymorphic in the shape of the nodes.
 
@@ -370,7 +393,7 @@
 
 
 foldBlockNodesF3 (ff, fm, fl) = block
-  where block :: forall e x . Block n e x -> EitherCO e a b -> EitherCO x c b
+  where block :: forall e x . Block n e x -> IndexedCO e a b -> IndexedCO x c b
         block (BFirst  node)    = ff node
         block (BMiddle node)    = fm node
         block (BLast   node)    = fl node
@@ -382,7 +405,7 @@
 foldBlockNodesF f = foldBlockNodesF3 (f, f, f)
 
 foldBlockNodesB3 (ff, fm, fl) = block
-  where block :: forall e x . Block n e x -> EitherCO x a b -> EitherCO e c b
+  where block :: forall e x . Block n e x -> IndexedCO x a b -> IndexedCO e c b
         block (BFirst  node)    = ff node
         block (BMiddle node)    = fm node
         block (BLast   node)    = fl node
@@ -417,7 +440,7 @@
 -- is or is not present depending on the shape of the block.
 --
 -- The blockToNodeList function cannot be currently expressed using
--- foldBlockNodesB, because it returns EitherCO e a b, which means
+-- foldBlockNodesB, because it returns IndexedCO e a b, which means
 -- two different types depending on the shape of the block entry.
 -- But blockToNodeList returns one of four possible types, depending
 -- on the shape of the block entry *and* exit.
diff --git a/hoopl.cabal b/hoopl.cabal
--- a/hoopl.cabal
+++ b/hoopl.cabal
@@ -1,5 +1,6 @@
 Name:                hoopl
-Version:             3.8.3.0
+Version:             3.8.6.0
+-- version 3.8.6.0 is the version that goes with the camera-ready Haskell'10 paper
 Description:         Higher-order optimization library
 License:             BSD3
 License-file:        LICENSE
@@ -16,6 +17,7 @@
 Library
   Build-Depends:     base >= 3 && < 5, containers
   Exposed-modules:   Compiler.Hoopl,
+                     Compiler.Hoopl.Wrappers,
                      Compiler.Hoopl.Passes.Dominator,
                      Compiler.Hoopl.Passes.DList,
 --                       Compiler.Hoopl.DataflowFold,
@@ -24,16 +26,20 @@
   Other-modules:     Compiler.Hoopl.GraphUtil,
                      -- GraphUtil should *never* be seen by clients.
                      -- The remaining modules are hidden *provisionally*
+                       Compiler.Hoopl.Checkpoint,
                        Compiler.Hoopl.Collections,
                        Compiler.Hoopl.Combinators,
                        Compiler.Hoopl.Dataflow,
                        Compiler.Hoopl.Debug,
                        Compiler.Hoopl.Graph, 
+                       Compiler.Hoopl.Label,
                        Compiler.Hoopl.MkGraph,
                        Compiler.Hoopl.Fuel,
                        Compiler.Hoopl.Pointed,
-                       Compiler.Hoopl.Unique, Compiler.Hoopl.Label,
-                       Compiler.Hoopl.Show, Compiler.Hoopl.Util
+                       Compiler.Hoopl.Shape,
+                       Compiler.Hoopl.Show, 
+                       Compiler.Hoopl.Unique, 
+                       Compiler.Hoopl.Util
                        Compiler.Hoopl.XUtil
   ghc-options:       -Wall -fno-warn-name-shadowing
 
diff --git a/hoopl.pdf b/hoopl.pdf
Binary files a/hoopl.pdf and b/hoopl.pdf differ