    {-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables, KindSignatures,
                 FlexibleContexts #-}

    module ZipDataflow
        ( DebugNodes(), RewritingDepth(..), LastOutFacts(..)
        , zdfSolveFrom, zdfRewriteFrom
        , zdfSolveFromL
        , ForwardTransfers(..), BackwardTransfers(..)
        , ForwardRewrites(..),  BackwardRewrites(..)
        , ForwardFixedPoint, BackwardFixedPoint
        , zdfFpFacts
        , zdfFpOutputFact
        , zdfGraphChanged
        , zdfDecoratedGraph -- not yet implemented
        , zdfFpContents
        , zdfFpLastOuts
        , zdfBRewriteFromL, zdfFRewriteFromL
        )
    where

    import BlockId
    import CmmTx
    import DFMonad
    import OptimizationFuel as F
    import MkZipCfg
    import ZipCfg
    import qualified ZipCfg as G

    import Maybes
    import Outputable

    import Control.Monad

    {-

    This module implements two useful tools:

      1. An iterative solver for dataflow problems

      2. The combined dataflow-analysis-and-transformation framework
         described by Lerner, Grove, and Chambers in their excellent
         2002 POPL paper (http://tinyurl.com/3zycbr or
         http://tinyurl.com/3pnscd).

    Each tool comes in two flavors: one for forward dataflow problems
    and one for backward dataflow problems.

    We quote the paper above:

      Dataflow analyses can have mutually beneficial interactions.
      Previous efforts to exploit these interactions have either
      (1) iteratively performed each individual analysis until no
      further improvements are discovered or (2) developed "super-
      analyses" that manually combine conceptually separate anal-
      yses. We have devised a new approach that allows anal-
      yses to be defined independently while still enabling them
      to be combined automatically and profitably. Our approach
      avoids the loss of precision associated with iterating indi-
      vidual analyses and the implementation difficulties of man-
      ually writing a super-analysis.

    The key idea is to provide at each CFG node not only a dataflow
    transfer function but also a rewriting function that has the option to
    replace the node with a new (possibly empty) graph.  The rewriting
    function takes a dataflow fact as input, and the fact is used to
    justify any rewriting.  For example, in a backward problem, the fact
    that variable x is dead can be used to justify rewriting node
      x := e
    to the empty graph.  In a forward problem, the fact that x == 7 can
    be used to justify rewriting node
      y := x + 1
    to
      y := 8
    which in turn will be analyzed and produce a new fact:
    x == 7 and y == 8.

    In its most general form, this module takes as input graph, transfer
    equations, rewrites, and an initial set of dataflow facts, and
    iteratively computes a new graph and a new set of dataflow facts such
    that
      * The set of facts is a fixed point of the transfer equations
      * The graph has been rewritten as much as is consistent with
        the given facts and requested rewriting depth (see below)
    N.B. 'A set of facts' is shorthand for 'A finite map from CFG label to fact'.

    The types of transfer equations, rewrites, and fixed points are
    different for forward and backward problems.  To avoid cluttering the
    name space with two versions of every name, other names such as
    zdfSolveFrom are overloaded to work in both forward or backward
    directions.  This design decision is based on experience with the
    predecessor module, which has been mercifully deleted.

    This module is deliberately very abstract.  It is a completely general
    framework and well-nigh impossible to understand in isolation.  The
    cautious reader will begin with some concrete examples in the form of
    clients.  NR recommends

      CmmLiveZ             A simple liveness analysis

      CmmSpillReload.removeDeadAssignmentsAndReloads
                           A piece of spaghetti to pull on, which leads to
                             - a two-part liveness analysis that tracks
                               variables live in registers and live on the stack
                             - elimination of assignments to dead variables
                             - elimination of redundant reloads

    Even hearty souls should avoid the CmmProcPointZ client, at least for
    the time being.

    -}

    {- ============ TRANSFER FUNCTIONS AND REWRITES =========== -}

    -- | For a backward transfer, you're given the fact on a node's
    -- outedge and you compute the fact on the inedge.  Facts have type 'a'.
    -- A last node may have multiple outedges, each pointing to a labelled
    -- block, so instead of a fact it is given a mapping from BlockId to fact.

    data BackwardTransfers middle last a = BackwardTransfers
        { bt_first_in  :: BlockId -> a              -> a
        , bt_middle_in :: middle  -> a              -> a
        , bt_last_in   :: last    -> (BlockId -> a) -> a
        }

    -- | For a forward transfer, you're given the fact on a node's
    -- inedge and you compute the fact on the outedge. Because a last node
    -- may have multiple outedges, each pointing to a labelled
    -- block, so instead of a fact it produces a list of (BlockId, fact) pairs.

    data ForwardTransfers middle last a = ForwardTransfers
        { ft_first_out  :: BlockId -> a -> a
        , ft_middle_out :: middle  -> a -> a
        , ft_last_outs  :: last    -> a -> LastOutFacts a
        , ft_exit_out   ::            a -> a
        }

    newtype LastOutFacts a = LastOutFacts [(BlockId, a)]
      -- ^ These are facts flowing out of a last node to the node's successors.
      -- They are either to be set (if they pertain to the graph currently
      -- under analysis) or propagated out of a sub-analysis

    -- | A backward rewrite takes the same inputs as a backward transfer,
    -- but instead of producing a fact, it produces a replacement graph or Nothing.

    data BackwardRewrites middle last a = BackwardRewrites
        { br_first  :: BlockId -> a              -> Maybe (AGraph middle last)
        , br_middle :: middle  -> a              -> Maybe (AGraph middle last)
        , br_last   :: last    -> (BlockId -> a) -> Maybe (AGraph middle last)
        , br_exit   ::                              Maybe (AGraph middle last)
        }

    -- | A forward rewrite takes the same inputs as a forward transfer,
    -- but instead of producing a fact, it produces a replacement graph or Nothing.

    data ForwardRewrites middle last a = ForwardRewrites
        { fr_first  :: BlockId -> a -> Maybe (AGraph middle last)
        , fr_middle :: middle  -> a -> Maybe (AGraph middle last)
        , fr_last   :: last    -> a -> Maybe (AGraph middle last)
        , fr_exit   ::            a -> Maybe (AGraph middle last)
        }

    {- ===================== FIXED POINTS =================== -}

    -- | The result of combined analysis and transformation is a
    -- solution to the set of dataflow equations together with a 'contained value'.
    -- This solution is a member of type class 'FixedPoint', which is parameterized by
    --   * middle and last nodes 'm' and 'l'
    --   * data flow fact 'fact'
    --   * the type 'a' of the contained value
    --
    -- In practice, the contained value 'zdfFpContents' is either a
    -- rewritten graph, when rewriting, or (), when solving without
    -- rewriting.  A function 'zdfFpMap' allows a client to change
    -- the contents without changing other values.
    --
    -- To save space, we provide the solution 'zdfFpFacts' as a mapping
    -- from BlockId to fact; if necessary, facts on edges can be
    -- reconstructed using the transfer functions; this functionality is
    -- intended to be included as the 'zdfDecoratedGraph', but the code
    -- has not yet been implemented.
    --
    -- The solution may also includes a fact 'zdfFpOuputFact', which is
    -- not associated with any label:
    --   * for a backward problem, this is the fact at entry
    --   * for a forward problem, this is the fact at the distinguished exit node,
    --     if such a node is present
    --
    -- For a forward problem only, the solution includes 'zdfFpLastOuts',
    -- which is the set of facts on edges leaving the graph.
    --
    -- The flag 'zdfGraphChanged' tells whether the engine did any rewriting.

    class FixedPoint fp where
        zdfFpContents     :: fp m l fact a -> a
        zdfFpFacts        :: fp m l fact a -> BlockEnv fact
        zdfFpOutputFact   :: fp m l fact a -> fact  -- entry for backward; exit for forward
        zdfDecoratedGraph :: fp m l fact a -> Graph (fact, m) (fact, l)
        zdfGraphChanged   :: fp m l fact a -> ChangeFlag
        zdfFpMap          :: (a -> b) -> (fp m l fact a -> fp m l fact b)

    -- | The class 'FixedPoint' has two instances: one for forward problems and
    -- one for backward problems.  The 'CommonFixedPoint' defines all fields
    -- common to both.  (The instance declarations are uninteresting and appear below.)

    data CommonFixedPoint m l fact a = FP
        { fp_facts     :: BlockEnv fact
        , fp_out       :: fact  -- entry for backward; exit for forward
        , fp_changed   :: ChangeFlag
        , fp_dec_graph :: Graph (fact, m) (fact, l)
        , fp_contents  :: a
        }

    -- | The common fixed point is sufficient for a backward problem.
    type BackwardFixedPoint = CommonFixedPoint

    -- | A forward problem needs the common fields, plus the facts on the outedges.
    data ForwardFixedPoint m l fact a = FFP
        { ffp_common    :: CommonFixedPoint m l fact a
        , zdfFpLastOuts :: LastOutFacts fact
        }

    {- ============== SOLVING AND REWRITING ============== -}

    type PassName = String

    -- | 'zdfSolveFrom' is an overloaded name that resolves to a pure
    -- analysis with no rewriting.  It has only two instances: forward and
    -- backward.  Since it needs no rewrites, the type parameters of the
    -- class are transfer functions and the fixed point.
    --
    --
    -- An iterative solver normally starts with the bottom fact at every
    -- node, but it can be useful in other contexts as well.  For this
    -- reason the initial set of facts (at labelled blocks only) is a
    -- parameter to the solver.
    --
    -- The constraints on the type signature exist purely for debugging;
    -- they make it possible to prettyprint nodes and facts.  The parameter of
    -- type 'PassName' is also used just for debugging.
    --
    -- Note that the result is a fixed point with no contents, that is,
    -- the contents have type ().
    --
    -- The intent of the rest of the type signature should be obvious.
    -- If not, place a skype call to norman-ramsey or complain bitterly
    -- to <norman-ramsey@acm.org>.

    class DataflowSolverDirection transfers fixedpt where
      zdfSolveFrom   :: (DebugNodes m l, Outputable a)
                     => BlockEnv a        -- ^ Initial facts (unbound == bottom)
                     -> PassName
                     -> DataflowLattice a -- ^ Lattice
                     -> transfers m l a   -- ^ Dataflow transfer functions
                     -> a                 -- ^ Fact flowing in (at entry or exit)
                     -> Graph m l         -- ^ Graph to be analyzed
                     -> FuelMonad (fixedpt m l a ())  -- ^ Answers
      zdfSolveFromL  :: (DebugNodes m l, Outputable a)
                     => BlockEnv a        -- Initial facts (unbound == bottom)
                     -> PassName
                     -> DataflowLattice a -- Lattice
                     -> transfers m l a   -- Dataflow transfer functions
                     -> a                 -- Fact flowing in (at entry or exit)
                     -> LGraph m l         -- Graph to be analyzed
                     -> FuelMonad (fixedpt m l a ())  -- Answers
      zdfSolveFromL b p l t a g = zdfSolveFrom b p l t a $ quickGraph g

    -- There are exactly two instances: forward and backward
    instance DataflowSolverDirection ForwardTransfers ForwardFixedPoint
      where zdfSolveFrom = solve_f

    instance DataflowSolverDirection BackwardTransfers BackwardFixedPoint
      where zdfSolveFrom = solve_b

    -- | zdfRewriteFrom is an overloaded name that resolves to an
    -- interleaved analysis and transformation.  It too is instantiated in
    -- forward and backward directions.
    --
    -- The type parameters of the class include not only transfer
    -- functions and the fixed point but also rewrites.
    --
    -- The type signature of 'zdfRewriteFrom' is that of 'zdfSolveFrom'
    -- with the rewrites and a rewriting depth as additional parameters,
    -- as well as a different result, which contains a rewritten graph.

    class DataflowSolverDirection transfers fixedpt =>
          DataflowDirection transfers fixedpt rewrites where
      zdfRewriteFrom :: (DebugNodes m l, Outputable a)
                     => RewritingDepth      -- whether to rewrite a rewritten graph
                     -> BlockEnv a          -- initial facts (unbound == bottom)
                     -> PassName
                     -> DataflowLattice a
                     -> transfers m l a
                     -> rewrites m l a
                     -> a                   -- fact flowing in (at entry or exit)
                     -> Graph m l
                     -> FuelMonad (fixedpt m l a (Graph m l))

    -- Temporarily lifting from Graph to LGraph -- an experiment to see how we
    -- can eliminate some hysteresis between Graph and LGraph.
    -- Perhaps Graph should be confined to dataflow code.
    -- Trading space for time
    quickGraph :: LastNode l => LGraph m l -> Graph m l
    quickGraph g = Graph (ZLast $ mkBranchNode $ lg_entry g) $ lg_blocks g

    quickLGraph :: LastNode l => Graph m l -> FuelMonad (LGraph m l)
    quickLGraph (Graph (ZLast (LastOther l)) blockenv)
        | isBranchNode l = return $ LGraph (branchNodeTarget l) blockenv
    quickLGraph g = F.lGraphOfGraph g

    fixptWithLGraph :: LastNode l => CommonFixedPoint m l fact (Graph m l) ->
                                     FuelMonad (CommonFixedPoint m l fact (LGraph m l))
    fixptWithLGraph cfp =
      do fp_c <- quickLGraph $ fp_contents cfp
         return $ cfp {fp_contents = fp_c}

    ffixptWithLGraph :: LastNode l => ForwardFixedPoint m l fact (Graph m l) ->
                                      FuelMonad (ForwardFixedPoint m l fact (LGraph m l))
    ffixptWithLGraph fp =
      do common <- fixptWithLGraph $ ffp_common fp
         return $ fp {ffp_common = common}

    zdfFRewriteFromL :: (DebugNodes m l, Outputable a)
                   => RewritingDepth      -- whether to rewrite a rewritten graph
                   -> BlockEnv a          -- initial facts (unbound == bottom)
                   -> PassName
                   -> DataflowLattice a
                   -> ForwardTransfers m l a
                   -> ForwardRewrites m l a
                   -> a                   -- fact flowing in (at entry or exit)
                   -> LGraph m l
                   -> FuelMonad (ForwardFixedPoint m l a (LGraph m l))
    zdfFRewriteFromL d b p l t r a g@(LGraph _ _) =
      do fp <- zdfRewriteFrom d b p l t r a $ quickGraph g
         ffixptWithLGraph fp

    zdfBRewriteFromL :: (DebugNodes m l, Outputable a)
                   => RewritingDepth      -- whether to rewrite a rewritten graph
                   -> BlockEnv a          -- initial facts (unbound == bottom)
                   -> PassName
                   -> DataflowLattice a
                   -> BackwardTransfers m l a
                   -> BackwardRewrites m l a
                   -> a                   -- fact flowing in (at entry or exit)
                   -> LGraph m l
                   -> FuelMonad (BackwardFixedPoint m l a (LGraph m l))
    zdfBRewriteFromL d b p l t r a g@(LGraph _ _) =
      do fp <- zdfRewriteFrom d b p l t r a $ quickGraph g
         fixptWithLGraph fp

    data RewritingDepth = RewriteShallow | RewriteDeep
    -- When a transformation proposes to rewrite a node,
    -- you can either ask the system to
    --  * "shallow": accept the new graph, analyse it without further rewriting
    --  * "deep": recursively analyse-and-rewrite the new graph

    -- There are currently four instances, but there could be more
    --	forward, backward (instantiates transfers, fixedpt, rewrites)
    --	Graph, AGraph     (instantiates graph)

    instance DataflowDirection ForwardTransfers ForwardFixedPoint ForwardRewrites
      where zdfRewriteFrom = rewrite_f_agraph

    instance DataflowDirection BackwardTransfers BackwardFixedPoint BackwardRewrites
      where zdfRewriteFrom = rewrite_b_agraph

    {- =================== IMPLEMENTATIONS ===================== -}

    -----------------------------------------------------------
    --	solve_f: forward, pure

    solve_f         :: (DebugNodes m l, Outputable a)
                    => BlockEnv a        -- initial facts (unbound == bottom)
                    -> PassName
                    -> DataflowLattice a -- lattice
                    -> ForwardTransfers m l a   -- dataflow transfer functions
                    -> a
                    -> Graph m l         -- graph to be analyzed
                    -> FuelMonad (ForwardFixedPoint m l a ())  -- answers
    solve_f env name lattice transfers in_fact g =
       runDFM lattice $ fwd_pure_anal name env transfers in_fact g

    rewrite_f_agraph :: (DebugNodes m l, Outputable a)
                     => RewritingDepth
                     -> BlockEnv a
                     -> PassName
                     -> DataflowLattice a
                     -> ForwardTransfers m l a
                     -> ForwardRewrites  m l a
                     -> a                 -- fact flowing in (at entry or exit)
                     -> Graph m l
                     -> FuelMonad (ForwardFixedPoint m l a (Graph m l))
    rewrite_f_agraph depth start_facts name lattice transfers rewrites in_fact g =
        runDFM lattice $
        do fuel <- fuelRemaining
           (fp, fuel') <- forward_rew maybeRewriteWithFuel depth start_facts name
                          transfers rewrites in_fact g fuel
           fuelDecrement name fuel fuel'
           return fp

    areturn :: AGraph m l -> DFM a (Graph m l)
    areturn g = liftToDFM $ liftUniq $ graphOfAGraph g

    -- | Here we prefer not simply to slap on 'goto eid' because this
    -- introduces an unnecessary basic block at each rewrite, and we don't
    -- want to stress out the finite map more than necessary
    lgraphToGraph :: LastNode l => LGraph m l -> Graph m l
    lgraphToGraph (LGraph eid blocks) =
        if flip any (eltsBlockEnv blocks) $ \block -> any (== eid) (succs block) then
            Graph (ZLast (mkBranchNode eid)) blocks
        else -- common case: entry is not a branch target
            let Block _ entry = lookupBlockEnv blocks eid `orElse` panic "missing entry!"
            in  Graph entry (delFromBlockEnv blocks eid)

    class (Outputable m, Outputable l, LastNode l, Outputable (LGraph m l)) => DebugNodes m l

    fwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
                 => PassName
                 -> BlockEnv a
                 -> ForwardTransfers m l a
                 -> a
                 -> Graph m l
                 -> DFM a (ForwardFixedPoint m l a ())

    fwd_pure_anal name env transfers in_fact g =
        do (fp, _) <- anal_f name env transfers panic_rewrites in_fact g panic_fuel
           return fp
      where -- definitely a case of "I love lazy evaluation"
        anal_f = forward_sol (\_ _ -> Nothing) panic_depth
        panic_rewrites = panic "pure analysis asked for a rewrite function"
        panic_fuel     = panic "pure analysis asked for fuel"
        panic_depth    = panic "pure analysis asked for a rewrite depth"

    -----------------------------------------------------------------------
    --
    --	Here beginneth the super-general functions
    --
    --  Think of them as (typechecked) macros
    --   *  They are not exported
    --
    --   *  They are called by the specialised wrappers
    --	above, and always inlined into their callers
    --
    -- There are four functions, one for each combination of:
    --	Forward, Backward
    --	Solver, Rewriter
    --
    -- A "solver" produces a (DFM f (f, Fuel)),
    --	where f is the fact at entry(Bwd)/exit(Fwd)
    --	and from the DFM you can extract
    --		the BlockId->f
    --		the change-flag
    --		and more besides
    --
    -- A "rewriter" produces a rewritten *Graph* as well
    --
    -- Both constrain their rewrites by
    --	a) Fuel
    --	b) RewritingDepth: shallow/deep

    -----------------------------------------------------------------------

    type Fuel = OptimizationFuel

    forward_sol
            :: forall m l a .
               (DebugNodes m l, LastNode l, Outputable a)
            => (forall a . Fuel -> Maybe a -> Maybe a)
    		-- Squashes proposed rewrites if there is
    		-- no more fuel; OR if we are doing a pure
    		-- analysis, so totally ignore the rewrite
    		-- ie. For pure-analysis the fn is (\_ _ -> Nothing)
            -> RewritingDepth	-- Shallow/deep
            -> PassName
            -> BlockEnv a		-- Initial set of facts
            -> ForwardTransfers m l a
            -> ForwardRewrites m l a
            -> a			-- Entry fact
            -> Graph m l
            -> Fuel
            -> DFM a (ForwardFixedPoint m l a (), Fuel)
    forward_sol check_maybe = forw
     where
      forw :: RewritingDepth
           -> PassName
           -> BlockEnv a
           -> ForwardTransfers m l a
           -> ForwardRewrites m l a
           -> a
           -> Graph m l
           -> Fuel
           -> DFM a (ForwardFixedPoint m l a (), Fuel)
      forw rewrite name start_facts transfers rewrites =
       let anal_f :: DFM a b -> a -> Graph m l -> DFM a b
           anal_f finish in' g =
               do { _ <- fwd_pure_anal name emptyBlockEnv transfers in' g; finish }

           solve :: DFM a b -> a -> Graph m l -> Fuel -> DFM a (b, Fuel)
           solve finish in_fact (Graph entry blockenv) fuel =
             let blocks = G.postorder_dfs_from blockenv entry
                 set_or_save = mk_set_or_save (isJust . lookupBlockEnv blockenv)
                 set_successor_facts (Block id tail) fuel =
                   do { idfact <- getFact id
                      ; (last_outs, fuel) <- rec_rewrite (fr_first rewrites id idfact)
                                                    (ft_first_out transfers id idfact)
                                                    getExitFact (solve_tail tail)
                                                    (solve_tail tail) idfact fuel
                      ; set_or_save last_outs
                      ; return fuel }
             in do { (last_outs, fuel) <- solve_tail entry in_fact fuel
                       -- last_outs contains a mix of internal facts, which
                       -- are inputs to 'run', and external facts, which
                       -- are going to be forgotten by 'run'
                   ; set_or_save last_outs
                   ; fuel <- run "forward" name set_successor_facts blocks fuel
                   ; set_or_save last_outs
                       -- Re-set facts that may have been forgotten by run
                   ; b <-  finish
                   ; return (b, fuel)
                   }

           -- The need for both k1 and k2 suggests that maybe there's an opportunity
           -- for improvement here -- in most cases, they're the same...
           rec_rewrite :: forall t bI bW.
                          Maybe (AGraph m l) -> t -> DFM a bW
                       -> (t -> Fuel -> DFM a bI)
                       -> (bW -> Fuel -> DFM a bI)
                       -> a -> Fuel -> DFM a bI
           rec_rewrite rewritten analyzed finish k1 k2 in' fuel =
             case check_maybe fuel rewritten of -- fr_first rewrites id idfact of
               Nothing -> k1 analyzed fuel
               Just g -> do g <- areturn g
                            (a, fuel) <- subAnalysis' $
                              case rewrite of
                                RewriteDeep -> solve finish in' g (oneLessFuel fuel)
                                RewriteShallow -> do { a <- anal_f finish in' g
                                                     ; return (a, oneLessFuel fuel) }
                            k2 a fuel
           solve_tail (G.ZTail m t) in' fuel =
             rec_rewrite (fr_middle rewrites m in') (ft_middle_out transfers m in')
                         getExitFact (solve_tail t) (solve_tail t) in' fuel
           solve_tail (G.ZLast (LastOther l)) in' fuel =
             rec_rewrite (fr_last rewrites l in') (ft_last_outs transfers l in')
                         lastOutFacts k k in' fuel
               where k a b = return (a, b)
           solve_tail (G.ZLast LastExit) in' fuel =
             rec_rewrite (fr_exit rewrites in') (ft_exit_out transfers in')
                         lastOutFacts k (\a b -> return (a, b)) in' fuel
               where k a fuel = do { setExitFact a ; return (LastOutFacts [], fuel) }

           fixed_point in_fact g fuel =
             do { setAllFacts start_facts
                ; (a, fuel) <- solve getExitFact in_fact g fuel
                ; facts <- getAllFacts
                ; last_outs <- lastOutFacts
                ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
                ; let fp = FFP cfp last_outs
                ; return (fp, fuel)
                }
       in fixed_point

    mk_set_or_save :: (DataflowAnalysis df, Monad (df a), Outputable a) =>
                      (BlockId -> Bool) -> LastOutFacts a -> df a ()
    mk_set_or_save is_local (LastOutFacts l) = mapM_ set_or_save_one l
        where set_or_save_one (id, a) =
                  if is_local id then setFact id a else addLastOutFact (id, a)

    forward_rew
            :: forall m l a .
               (DebugNodes m l, LastNode l, Outputable a)
            => (forall a . Fuel -> Maybe a -> Maybe a)
            -> RewritingDepth
            -> BlockEnv a
            -> PassName
            -> ForwardTransfers m l a
            -> ForwardRewrites m l a
            -> a
            -> Graph m l
            -> Fuel
            -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
    forward_rew check_maybe = forw
      where
        forw :: RewritingDepth
             -> BlockEnv a
             -> PassName
             -> ForwardTransfers m l a
             -> ForwardRewrites m l a
             -> a
             -> Graph m l
             -> Fuel
             -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
        forw depth xstart_facts name transfers rewrites in_factx gx fuelx =
          let rewrite :: BlockEnv a -> DFM a b
                      -> a -> Graph m l -> Fuel
                      -> DFM a (b, Graph m l, Fuel)
              rewrite start finish in_fact g fuel =
               in_fact `seq` g `seq`
                let Graph entry blockenv = g
                    blocks = G.postorder_dfs_from blockenv entry
                in do { _ <- forward_sol check_maybe depth name start
                                         transfers rewrites in_fact g fuel
                      ; eid <- freshBlockId "temporary entry id"
                      ; (rewritten, fuel) <-
                          rew_tail (ZFirst eid) in_fact entry emptyBlockEnv fuel
                      ; (rewritten, fuel) <- rewrite_blocks blocks rewritten fuel
                      ; a <- finish
                      ; return (a, lgraphToGraph (LGraph eid rewritten), fuel)
                      }

              don't_rewrite :: forall t.
                               BlockEnv a -> DFM a t -> a
                            -> Graph m l -> Fuel
                            -> DFM a (t, Graph m l, Fuel)
              don't_rewrite facts finish in_fact g fuel =
                  do  { _ <- forward_sol check_maybe depth name facts
                                         transfers rewrites in_fact g fuel
                      ; a <- finish
                      ; return (a, g, fuel)
                      }

              inner_rew :: DFM a f -> a -> Graph m l -> Fuel -> DFM a (f, Graph m l, Fuel)
              inner_rew f i g fu = getAllFacts >>= \facts -> inner_rew' facts f i g fu
                  where inner_rew' = case depth of RewriteShallow -> don't_rewrite
                                                   RewriteDeep    -> rewrite
              fixed_pt_and_fuel =
                  do { (a, g, fuel) <- rewrite xstart_facts getExitFact in_factx gx fuelx
                     ; facts <- getAllFacts
                     ; changed <- graphWasRewritten
                     ; last_outs <- lastOutFacts
                     ; let cfp = FP facts a changed (panic "no decoration?!") g
                     ; let fp = FFP cfp last_outs
                     ; return (fp, fuel)
                     }

    -- JD: WHY AREN'T WE TAKING ANY FUEL HERE?
              rewrite_blocks :: [Block m l] -> (BlockEnv (Block m l))
                             -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
              rewrite_blocks [] rewritten fuel = return (rewritten, fuel)
              rewrite_blocks (G.Block id t : bs) rewritten fuel =
                do let h = ZFirst id
                   a <- getFact id
                   case check_maybe fuel $ fr_first rewrites id a of
                     Nothing -> do { (rewritten, fuel) <-
                                        rew_tail h (ft_first_out transfers id a)
                                                 t rewritten fuel
                                   ; rewrite_blocks bs rewritten fuel }
                     Just g  -> do { markGraphRewritten
                                   ; g <- areturn g
                                   ; (outfact, g, fuel) <- inner_rew getExitFact a g fuel
                                   ; let (blocks, h) = splice_head' h g
                                   ; (rewritten, fuel) <-
                                     rew_tail h outfact t (blocks `plusBlockEnv` rewritten) fuel
                                   ; rewrite_blocks bs rewritten fuel }

              rew_tail head in' (G.ZTail m t) rewritten fuel =
               in' `seq` rewritten `seq`
                my_trace "Rewriting middle node" (ppr m) $
                case check_maybe fuel $ fr_middle rewrites m in' of
                  Nothing -> rew_tail (G.ZHead head m) (ft_middle_out transfers m in') t
                                      rewritten fuel
                  Just g -> do { markGraphRewritten
                               ; g <- areturn g
                               ; (a, g, fuel) <- inner_rew getExitFact in' g fuel
                               ; let (blocks, h) = G.splice_head' head g
                               ; rew_tail h a t (blocks `plusBlockEnv` rewritten) fuel
                               }
              rew_tail h in' (G.ZLast l) rewritten fuel =
               in' `seq` rewritten `seq`
                my_trace "Rewriting last node" (ppr l) $
                case check_maybe fuel $ either_last rewrites in' l of
                  Nothing -> do check_facts in' l
                                return (insertBlock (zipht h (G.ZLast l)) rewritten, fuel)
                  Just g ->  do { markGraphRewritten
                               ; g <- areturn g
                               ; ((), g, fuel) <-
                                   my_trace "Just" (ppr g) $ inner_rew (return ()) in' g fuel
                               ; let g' = G.splice_head_only' h g
                               ; return (G.lg_blocks g' `plusBlockEnv` rewritten, fuel)
                               }
              either_last rewrites in' (LastExit) = fr_exit rewrites in'
              either_last rewrites in' (LastOther l) = fr_last rewrites l in'
              check_facts in' (LastOther l) =
                let LastOutFacts last_outs = ft_last_outs transfers l in'
                in mapM_ (uncurry checkFactMatch) last_outs
              check_facts _ LastExit = return ()
          in  fixed_pt_and_fuel

    lastOutFacts :: DFM f (LastOutFacts f)
    lastOutFacts = bareLastOutFacts >>= return . LastOutFacts

    {- ================================================================ -}

    solve_b         :: (DebugNodes m l, Outputable a)
                    => BlockEnv a        -- initial facts (unbound == bottom)
                    -> PassName
                    -> DataflowLattice a -- lattice
                    -> BackwardTransfers m l a   -- dataflow transfer functions
                    -> a                 -- exit fact
                    -> Graph m l         -- graph to be analyzed
                    -> FuelMonad (BackwardFixedPoint m l a ())  -- answers
    solve_b env name lattice transfers exit_fact g =
       runDFM lattice $ bwd_pure_anal name env transfers g exit_fact

    rewrite_b_agraph :: (DebugNodes m l, Outputable a)
                     => RewritingDepth
                     -> BlockEnv a
                     -> PassName
                     -> DataflowLattice a
                     -> BackwardTransfers m l a
                     -> BackwardRewrites m l a
                     -> a                 -- fact flowing in at exit
                     -> Graph m l
                     -> FuelMonad (BackwardFixedPoint m l a (Graph m l))
    rewrite_b_agraph depth start_facts name lattice transfers rewrites exit_fact g =
        runDFM lattice $
        do fuel <- fuelRemaining
           (fp, fuel') <- backward_rew maybeRewriteWithFuel depth start_facts name
                          transfers rewrites g exit_fact fuel
           fuelDecrement name fuel fuel'
           return fp

    backward_sol
            :: forall m l a .
               (DebugNodes m l, LastNode l, Outputable a)
            => (forall a . Fuel -> Maybe a -> Maybe a)
            -> RewritingDepth
            -> PassName
            -> BlockEnv a
            -> BackwardTransfers m l a
            -> BackwardRewrites m l a
            -> Graph m l
            -> a
            -> Fuel
            -> DFM a (BackwardFixedPoint m l a (), Fuel)
    backward_sol check_maybe = back
     where
      back :: RewritingDepth
           -> PassName
           -> BlockEnv a
           -> BackwardTransfers m l a
           -> BackwardRewrites m l a
           -> Graph m l
           -> a
           -> Fuel
           -> DFM a (BackwardFixedPoint m l a (), Fuel)
      back rewrite name start_facts transfers rewrites =
       let anal_b :: Graph m l -> a -> DFM a a
           anal_b g out =
               do { fp <- bwd_pure_anal name emptyBlockEnv transfers g out
                  ; return $ zdfFpOutputFact fp }

           subsolve :: AGraph m l -> a -> Fuel -> DFM a (a, Fuel)
           subsolve =
             case rewrite of
               RewriteDeep    -> \g a fuel ->
                   subAnalysis' $ do { g <- areturn g; solve g a (oneLessFuel fuel) }
               RewriteShallow -> \g a fuel ->
                   subAnalysis' $ do { g <- areturn g; a <- anal_b g a
                                     ; return (a, oneLessFuel fuel) }

           solve :: Graph m l -> a -> Fuel -> DFM a (a, Fuel)
           solve (Graph entry blockenv) exit_fact fuel =
             let blocks = reverse $ G.postorder_dfs_from blockenv entry
                 last_in  _env (LastExit)    = exit_fact
                 last_in   env (LastOther l) = bt_last_in transfers l env
                 last_rew _env (LastExit)    = br_exit rewrites
                 last_rew  env (LastOther l) = br_last rewrites l env
                 set_block_fact block fuel =
                     let (h, l) = G.goto_end (G.unzip block) in
                     do { env <- factsEnv
                        ; (a, fuel) <-
                          case check_maybe fuel $ last_rew env l of
                            Nothing -> return (last_in env l, fuel)
                            Just g -> do g' <- areturn g
                                         my_trace "analysis rewrites last node"
                                          (ppr l <+> pprGraph g') $
                                          subsolve g exit_fact fuel
                        ; _ <- set_head_fact h a fuel
                        ; return fuel }

             in do { fuel <- run "backward" name set_block_fact blocks fuel
                   ; eid <- freshBlockId "temporary entry id"
                   ; fuel <- set_block_fact (Block eid entry) fuel
                   ; a <- getFact eid
                   ; forgetFact eid
                   ; return (a, fuel)
                   }

           set_head_fact (G.ZFirst id) a fuel =
             case check_maybe fuel $ br_first rewrites id a of
               Nothing -> do { my_trace "set_head_fact" (ppr id <+> text "=" <+>
                                                         ppr (bt_first_in transfers id a)) $
                               setFact id $ bt_first_in transfers id a
                             ; return fuel }
               Just g  -> do { g' <- areturn g
                             ; (a, fuel) <- my_trace "analysis rewrites first node"
                                          (ppr id <+> pprGraph g') $
                                          subsolve g a fuel
                             ; setFact id $ bt_first_in transfers id a
                             ; return fuel
                             }
           set_head_fact (G.ZHead h m) a fuel =
             case check_maybe fuel $ br_middle rewrites m a of
               Nothing -> set_head_fact h (bt_middle_in transfers m a) fuel
               Just g -> do { g' <- areturn g
                            ; (a, fuel) <- my_trace "analysis rewrites middle node"
                                          (ppr m <+> pprGraph g') $
                                          subsolve g a fuel
                            ; set_head_fact h a fuel }

           fixed_point g exit_fact fuel =
             do { setAllFacts start_facts
                ; (a, fuel) <- solve g exit_fact fuel
                ; facts <- getAllFacts
                ; let cfp = FP facts a NoChange (panic "no decoration?!") ()
                ; return (cfp, fuel)
                }
       in fixed_point

    bwd_pure_anal :: (DebugNodes m l, LastNode l, Outputable a)
                 => PassName
                 -> BlockEnv a
                 -> BackwardTransfers m l a
                 -> Graph m l
                 -> a
                 -> DFM a (BackwardFixedPoint m l a ())

    bwd_pure_anal name env transfers g exit_fact =
        do (fp, _) <- anal_b name env transfers panic_rewrites g exit_fact panic_fuel
           return fp
      where -- another case of "I love lazy evaluation"
        anal_b = backward_sol (\_ _ -> Nothing) panic_depth
        panic_rewrites = panic "pure analysis asked for a rewrite function"
        panic_fuel     = panic "pure analysis asked for fuel"
        panic_depth    = panic "pure analysis asked for a rewrite depth"

    {- ================================================================ -}

    backward_rew
            :: forall m l a .
               (DebugNodes m l, LastNode l, Outputable a)
            => (forall a . Fuel -> Maybe a -> Maybe a)
            -> RewritingDepth
            -> BlockEnv a
            -> PassName
            -> BackwardTransfers m l a
            -> BackwardRewrites m l a
            -> Graph m l
            -> a
            -> Fuel
            -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
    backward_rew check_maybe = back
      where
        solve = backward_sol check_maybe
        back :: RewritingDepth
             -> BlockEnv a
             -> PassName
             -> BackwardTransfers m l a
             -> BackwardRewrites m l a
             -> Graph m l
             -> a
             -> Fuel
             -> DFM a (BackwardFixedPoint m l a (Graph m l), Fuel)
        back depth xstart_facts name transfers rewrites gx exit_fact fuelx =
          let rewrite :: BlockEnv a
                      -> Graph m l -> a -> Fuel
                      -> DFM a (a, Graph m l, Fuel)
              rewrite start g exit_fact fuel =
               let Graph entry blockenv = g
                   blocks = reverse $ G.postorder_dfs_from blockenv entry
               in do { (FP _ in_fact _ _ _, _) <-    -- don't drop the entry fact!
                         solve depth name start transfers rewrites g exit_fact fuel
                     --; env <- getAllFacts
                     -- ; my_trace "facts after solving" (ppr env) $ return ()
                     ; eid <- freshBlockId "temporary entry id"
                     ; (rewritten, fuel) <- rewrite_blocks True blocks emptyBlockEnv fuel
                     -- We can't have the fact check fail on the bogus entry, which _may_ change
                     ; (rewritten, fuel) <-
                         rewrite_blocks False [Block eid entry] rewritten fuel
                     ; my_trace "eid" (ppr eid) $ return ()
                     ; my_trace "exit_fact" (ppr exit_fact) $ return ()
                     ; my_trace "in_fact" (ppr in_fact) $ return ()
                     ; return (in_fact, lgraphToGraph (LGraph eid rewritten), fuel)
                     } -- Remember: the entry fact computed by @solve@ accounts for rewriting
              don't_rewrite facts g exit_fact fuel =
                do { (fp, _) <-
                         solve depth name facts transfers rewrites g exit_fact fuel
                   ; return (zdfFpOutputFact fp, g, fuel) }
              inner_rew :: Graph m l -> a -> Fuel -> DFM a (a, Graph m l, Fuel)
              inner_rew g a f = getAllFacts >>= \facts -> inner_rew' facts g a f
                  where inner_rew' = case depth of RewriteShallow -> don't_rewrite
                                                   RewriteDeep    -> rewrite
              fixed_pt_and_fuel =
                  do { (a, g, fuel) <- rewrite xstart_facts gx exit_fact fuelx
                     ; facts <- getAllFacts
                     ; changed <- graphWasRewritten
                     ; let fp = FP facts a changed (panic "no decoration?!") g
                     ; return (fp, fuel)
                     }
              rewrite_blocks :: Bool -> [Block m l] -> (BlockEnv (Block m l))
                             -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
              rewrite_blocks check bs rewritten fuel =
                  do { env <- factsEnv
                     ; let rew [] r f = return (r, f)
                           rew (b : bs) r f =
                               do { (r, f) <- rewrite_block check env b r f; rew bs r f }
                     ; rew bs rewritten fuel }
              rewrite_block check env b rewritten fuel =
                let (h, l) = G.goto_end (G.unzip b) in
                case maybeRewriteWithFuel fuel $ either_last env l of
                  Nothing -> propagate check fuel h (last_in env l) (ZLast l) rewritten
                  Just g ->
                    do { markGraphRewritten
                       ; g <- areturn g
                       ; (a, g, fuel) <- inner_rew g exit_fact fuel
                       ; let G.Graph t new_blocks = g
                       ; let rewritten' = new_blocks `plusBlockEnv` rewritten
                       ; propagate check fuel h a t rewritten' -- continue at entry of g
                       }
              either_last _env (LastExit)    = br_exit rewrites
              either_last  env (LastOther l) = br_last rewrites l env
              last_in _env (LastExit)    = exit_fact
              last_in  env (LastOther l) = bt_last_in transfers l env
              propagate check fuel (ZHead h m) a tail rewritten =
                case maybeRewriteWithFuel fuel $ br_middle rewrites m a of
                  Nothing ->
                    propagate check fuel h (bt_middle_in transfers m a) (ZTail m tail) rewritten
                  Just g  ->
                    do { markGraphRewritten
                       ; g <- areturn g
                       ; my_trace "With Facts" (ppr a) $ return ()
                       ; my_trace "  Rewrote middle node"
                                                 (f4sep [ppr m, text "to", pprGraph g]) $
                         return ()
                       ; (a, g, fuel) <- inner_rew g a fuel
                       ; let Graph t newblocks = G.splice_tail g tail
                       ; my_trace "propagating facts" (ppr a) $
                         propagate check fuel h a t (newblocks `plusBlockEnv` rewritten) }
              propagate check fuel (ZFirst id) a tail rewritten =
                case maybeRewriteWithFuel fuel $ br_first rewrites id a of
                  Nothing -> do { if check then
                                    checkFactMatch id $ bt_first_in transfers id a
                                  else return ()
                                ; return (insertBlock (Block id tail) rewritten, fuel) }
                  Just g ->
                    do { markGraphRewritten
                       ; g <- areturn g
                       ; my_trace "Rewrote first node"
                         (f4sep [ppr id <> colon, text "to", pprGraph g]) $ return ()
                       ; (a, g, fuel) <- inner_rew g a fuel
                       ; if check then checkFactMatch id (bt_first_in transfers id a)
                         else return ()
                       ; let Graph t newblocks = G.splice_tail g tail
                       ; let r = insertBlock (Block id t) (newblocks `plusBlockEnv` rewritten)
                       ; return (r, fuel) }
          in  fixed_pt_and_fuel

    {- ================================================================ -}

    instance FixedPoint CommonFixedPoint where
        zdfFpFacts        = fp_facts
        zdfFpOutputFact   = fp_out
        zdfGraphChanged   = fp_changed
        zdfDecoratedGraph = fp_dec_graph
        zdfFpContents     = fp_contents
        zdfFpMap f (FP fs out ch dg a) = FP fs out ch dg (f a)

    instance FixedPoint ForwardFixedPoint where
        zdfFpFacts        = fp_facts     . ffp_common
        zdfFpOutputFact   = fp_out       . ffp_common
        zdfGraphChanged   = fp_changed   . ffp_common
        zdfDecoratedGraph = fp_dec_graph . ffp_common
        zdfFpContents     = fp_contents  . ffp_common
        zdfFpMap f (FFP fp los) = FFP (zdfFpMap f fp) los

    dump_things :: Bool
    dump_things = False

    my_trace :: String -> SDoc -> a -> a
    my_trace = if dump_things then pprTrace else \_ _ a -> a

    -- | Here's a function to run an action on blocks until we reach a fixed point.
    run :: (Outputable a, DebugNodes m l) =>
           String -> String -> (Block m l -> b -> DFM a b) -> [Block m l] -> b -> DFM a b
    run dir name do_block blocks b =
       do { show_blocks $ iterate (1::Int) }
       where
         -- N.B. Each iteration starts with the same transaction limit;
         -- only the rewrites in the final iteration actually count
         trace_block (b, cnt) block =
             do b' <- my_trace "about to do" (text name <+> text "on" <+>
                         ppr (blockId block) <+> ppr cnt) $
                        do_block block b
                return (b', cnt + 1)
         iterate n =
             do { forgetLastOutFacts
                ; markFactsUnchanged
                ; (b, _) <- foldM trace_block (b, 0 :: Int) blocks
                ; changed <- factsStatus
                ; facts <- getAllFacts
                ; let depth = 0 -- was nesting depth
                ; ppIter depth n $
                  case changed of
                    NoChange -> unchanged depth $ return b
                    SomeChange ->
                        pprFacts depth n facts $
                        if n < 1000 then iterate (n+1)
                        else panic $ msg n
                }
         msg n = concat [name, " didn't converge in ", show n, " " , dir,
                         " iterations"]
         my_nest depth sdoc = my_trace "" $ nest (3*depth) sdoc
         ppIter depth n = my_nest depth (empty $$ text "*************** iteration" <+> pp_i n)
         pp_i n = int n <+> text "of" <+> text name <+> text "on" <+> graphId
         unchanged depth =
           my_nest depth (text "facts for" <+> graphId <+> text "are unchanged")

         graphId = case blocks of { Block id _ : _ -> ppr id ; [] -> text "<empty>" }
         show_blocks = my_trace "Blocks:" (vcat (map pprBlock blocks))
         pprBlock (Block id t) = nest 2 (pprFact (id, t))
         pprFacts depth n env =
             my_nest depth (text "facts for iteration" <+> pp_i n <+> text "are:" $$
                            (nest 2 $ vcat $ map pprFact $ blockEnvToList env))

    pprFact :: (Outputable a, Outputable b) => (a,b) -> SDoc
    pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)

    f4sep :: [SDoc] -> SDoc
    f4sep [] = fsep []
    f4sep (d:ds) = fsep (d : map (nest 4) ds)

    subAnalysis' :: (Monad (m f), DataflowAnalysis m, Outputable f) =>
                    m f a -> m f a
    subAnalysis' m =
        do { a <- subAnalysis $
                   do { a <- m; -- facts <- getAllFacts
                      ; -- my_trace "after sub-analysis facts are" (pprFacts facts) $
                        return a }
           -- ; facts <- getAllFacts
           ; -- my_trace "in parent analysis facts are" (pprFacts facts) $
             return a }
      -- where pprFacts env = nest 2 $ vcat $ map pprFact $ blockEnvToList env
            -- pprFact (id, a) = hang (ppr id <> colon) 4 (ppr a)