{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}

module LinearScan.Loops where


import Debug.Trace (trace, traceShow)
import qualified Prelude
import qualified Data.IntMap
import qualified Data.IntSet
import qualified Data.List
import qualified Data.Ord
import qualified Data.Functor.Identity
import qualified LinearScan.Utils

import qualified LinearScan.Blocks as Blocks
import qualified LinearScan.IntMap as IntMap
import qualified LinearScan.Lib as Lib
import qualified LinearScan.Monad as Monad
import qualified LinearScan.Yoneda as Yoneda
import qualified LinearScan.Eqtype as Eqtype
import qualified LinearScan.Seq as Seq
import qualified LinearScan.Ssrbool as Ssrbool
import qualified LinearScan.Ssrnat as Ssrnat



#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base as GHC.Base
import qualified GHC.Prim as GHC.Prim
#else
-- HUGS
import qualified LinearScan.IOExts as IOExts
#endif


#ifdef __GLASGOW_HASKELL__
--unsafeCoerce :: a -> b
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
--unsafeCoerce :: a -> b
unsafeCoerce = IOExts.unsafeCoerce
#endif

data LoopState =
   Build_LoopState IntMap.IntSet IntMap.IntSet ([] Blocks.BlockId) IntMap.IntSet 
 (IntMap.IntMap IntMap.IntSet) (IntMap.IntMap IntMap.IntSet) (IntMap.IntMap
                                                             IntMap.IntSet) 
 (IntMap.IntMap ((,) Prelude.Int Prelude.Int))

activeBlocks :: LoopState -> IntMap.IntSet
activeBlocks l =
  case l of {
   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
    loopDepths0 -> activeBlocks0}

visitedBlocks :: LoopState -> IntMap.IntSet
visitedBlocks l =
  case l of {
   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
    loopDepths0 -> visitedBlocks0}

loopHeaderBlocks :: LoopState -> [] Blocks.BlockId
loopHeaderBlocks l =
  case l of {
   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
    loopDepths0 -> loopHeaderBlocks0}

loopEndBlocks :: LoopState -> IntMap.IntSet
loopEndBlocks l =
  case l of {
   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
    loopDepths0 -> loopEndBlocks0}

forwardBranches :: LoopState -> IntMap.IntMap IntMap.IntSet
forwardBranches l =
  case l of {
   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
    loopDepths0 -> forwardBranches0}

backwardBranches :: LoopState -> IntMap.IntMap IntMap.IntSet
backwardBranches l =
  case l of {
   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
    loopDepths0 -> backwardBranches0}

loopIndices :: LoopState -> IntMap.IntMap IntMap.IntSet
loopIndices l =
  case l of {
   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
    loopDepths0 -> loopIndices0}

loopDepths :: LoopState -> IntMap.IntMap ((,) Prelude.Int Prelude.Int)
loopDepths l =
  case l of {
   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
    loopDepths0 -> loopDepths0}

emptyLoopState :: LoopState
emptyLoopState =
  Build_LoopState IntMap.emptyIntSet IntMap.emptyIntSet [] IntMap.emptyIntSet
    IntMap.emptyIntMap IntMap.emptyIntMap IntMap.emptyIntMap
    IntMap.emptyIntMap

modifyActiveBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> Monad.State
                      LoopState ()
modifyActiveBlocks f =
  Monad.modify (\st -> Build_LoopState (f (activeBlocks st))
    (visitedBlocks st) (loopHeaderBlocks st) (loopEndBlocks st)
    (forwardBranches st) (backwardBranches st) (loopIndices st)
    (loopDepths st))

modifyVisitedBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> Monad.State
                       LoopState ()
modifyVisitedBlocks f =
  Monad.modify (\st -> Build_LoopState (activeBlocks st)
    (f (visitedBlocks st)) (loopHeaderBlocks st) (loopEndBlocks st)
    (forwardBranches st) (backwardBranches st) (loopIndices st)
    (loopDepths st))

modifyLoopHeaderBlocks :: (([] Blocks.BlockId) -> [] Blocks.BlockId) ->
                          Monad.State LoopState ()
modifyLoopHeaderBlocks f =
  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
    (f (loopHeaderBlocks st)) (loopEndBlocks st) (forwardBranches st)
    (backwardBranches st) (loopIndices st) (loopDepths st))

modifyLoopEndBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> Monad.State
                       LoopState ()
modifyLoopEndBlocks f =
  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
    (loopHeaderBlocks st) (f (loopEndBlocks st)) (forwardBranches st)
    (backwardBranches st) (loopIndices st) (loopDepths st))

modifyForwardBranches :: ((IntMap.IntMap IntMap.IntSet) -> IntMap.IntMap
                         IntMap.IntSet) -> Monad.State LoopState ()
modifyForwardBranches f =
  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
    (loopHeaderBlocks st) (loopEndBlocks st) (f (forwardBranches st))
    (backwardBranches st) (loopIndices st) (loopDepths st))

modifyBackwardBranches :: ((IntMap.IntMap IntMap.IntSet) -> IntMap.IntMap
                          IntMap.IntSet) -> Monad.State LoopState ()
modifyBackwardBranches f =
  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
    (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st)
    (f (backwardBranches st)) (loopIndices st) (loopDepths st))

setLoopIndices :: (IntMap.IntMap IntMap.IntSet) -> Monad.State LoopState ()
setLoopIndices indices =
  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
    (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st)
    (backwardBranches st) indices (loopDepths st))

setLoopDepths :: (IntMap.IntMap ((,) Prelude.Int Prelude.Int)) -> Monad.State
                 LoopState ()
setLoopDepths depths =
  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
    (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st)
    (backwardBranches st) (loopIndices st) depths)

addReference :: Prelude.Int -> Prelude.Int -> (IntMap.IntMap IntMap.IntSet)
                -> IntMap.IntMap IntMap.IntSet
addReference i x =
  IntMap.coq_IntMap_alter (\macc ->
    case macc of {
     Prelude.Just acc -> Prelude.Just (IntMap.coq_IntSet_insert x acc);
     Prelude.Nothing -> Prelude.Just (IntMap.coq_IntSet_singleton x)}) i

pathToLoopHeader :: Blocks.BlockId -> Prelude.Int -> LoopState ->
                    Prelude.Maybe IntMap.IntSet
pathToLoopHeader blk header st =
  let {
   go = let {
         go fuel visited b =
           (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
             (\_ -> (,) visited
             Prelude.Nothing)
             (\n ->
             let {visited' = IntMap.coq_IntSet_insert b visited} in
             let {
              forwardPreds = case IntMap.coq_IntMap_lookup b
                                    (forwardBranches st) of {
                              Prelude.Just preds ->
                               IntMap.coq_IntSet_toList preds;
                              Prelude.Nothing -> []}}
             in
             let {
              backwardPreds = case IntMap.coq_IntMap_lookup b
                                     (backwardBranches st) of {
                               Prelude.Just preds ->
                                IntMap.coq_IntSet_toList preds;
                               Prelude.Nothing -> []}}
             in
             let {preds = (Prelude.++) forwardPreds backwardPreds} in
             Lib.forFold ((,) visited' (Prelude.Just
               (IntMap.coq_IntSet_singleton b))) (unsafeCoerce preds)
               (\mxs pred ->
               case mxs of {
                (,) vis o ->
                 case o of {
                  Prelude.Just xs ->
                   case Eqtype.eq_op Ssrnat.nat_eqType pred
                          (unsafeCoerce header) of {
                    Prelude.True -> (,) vis (Prelude.Just
                     (IntMap.coq_IntSet_union xs
                       (IntMap.coq_IntSet_singleton (unsafeCoerce pred))));
                    Prelude.False ->
                     case IntMap.coq_IntSet_member (unsafeCoerce pred) vis of {
                      Prelude.True -> (,) vis (Prelude.Just xs);
                      Prelude.False ->
                       case unsafeCoerce go n vis pred of {
                        (,) vis' o0 ->
                         case o0 of {
                          Prelude.Just ys -> (,) vis' (Prelude.Just
                           (IntMap.coq_IntSet_union xs ys));
                          Prelude.Nothing -> (,) vis Prelude.Nothing}}}};
                  Prelude.Nothing -> mxs}}))
             fuel}
        in go}
  in
  Prelude.snd
    (go (IntMap.coq_IntSet_size (visitedBlocks st)) IntMap.emptyIntSet blk)

liftStateT :: (Monad.Monad a1) -> (Monad.State a2 a3) -> Monad.StateT 
              a2 a1 a3
liftStateT h x =
  Monad.bind (Monad.coq_StateT_Monad h) (\st ->
    case x st of {
     (,) a st' ->
      Monad.bind (Monad.coq_StateT_Monad h) (\x0 ->
        Monad.pure (Monad.coq_StateT_Applicative h) a)
        (Monad.putT (Monad.is_applicative h) st')})
    (Monad.getT (Monad.is_applicative h))

computeLoopDepths :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 
                     a4) -> (IntMap.IntMap a1) -> Monad.StateT LoopState 
                     a5 ()
computeLoopDepths mDict binfo bs =
  Monad.bind (Monad.coq_StateT_Monad mDict) (\st ->
    Monad.bind (Monad.coq_StateT_Monad mDict) (\m ->
      let {
       f = \acc loopIndex refs ->
        IntMap.coq_IntSet_forFold acc refs (\m' blk ->
          let {
           f = \mx ->
            case mx of {
             Prelude.Just y ->
              case y of {
               (,) idx depth -> Prelude.Just ((,) (Prelude.min idx loopIndex)
                ((Prelude.succ) depth))};
             Prelude.Nothing -> Prelude.Just ((,) loopIndex ((Prelude.succ)
              0))}}
          in
          IntMap.coq_IntMap_alter f blk m')}
      in
      liftStateT mDict
        (Monad.bind (unsafeCoerce Monad.coq_State_Monad) (\x ->
          setLoopDepths
            (IntMap.coq_IntMap_foldlWithKey f IntMap.emptyIntMap m))
          (setLoopIndices m)))
      (Monad.lift mDict
        (Yoneda.iso_to
          (Yoneda.coq_Yoneda_lemma
            (Monad.is_functor (Monad.is_applicative mDict)))
          (Monad.forFoldM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict))
            IntMap.emptyIntMap (IntMap.coq_IntSet_toList (loopEndBlocks st))
            (\m endBlock ->
            case IntMap.coq_IntMap_lookup endBlock bs of {
             Prelude.Just b ->
              Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict))
                (\suxs ->
                Monad.pure
                  (unsafeCoerce
                    (Yoneda.coq_Yoneda_Applicative
                      (Monad.is_applicative mDict)))
                  (Lib.forFold m suxs (\m' sux ->
                    let {headers = loopHeaderBlocks st} in
                    let {
                     loopIndex = Seq.find (\x ->
                                   Eqtype.eq_op Ssrnat.nat_eqType
                                     (unsafeCoerce x) sux) headers}
                    in
                    case Eqtype.eq_op Ssrnat.nat_eqType
                           (unsafeCoerce loopIndex)
                           (unsafeCoerce (Data.List.length headers)) of {
                     Prelude.True -> m';
                     Prelude.False ->
                      let {
                       mres = pathToLoopHeader endBlock (unsafeCoerce sux) st}
                      in
                      case mres of {
                       Prelude.Just path ->
                        Lib.forFold m' (IntMap.coq_IntSet_toList path)
                          (\m'' blk -> addReference loopIndex blk m'');
                       Prelude.Nothing -> m'}}))) (\_ ->
                Blocks.blockSuccessors mDict binfo b);
             Prelude.Nothing ->
              Monad.pure
                (unsafeCoerce
                  (Yoneda.coq_Yoneda_Applicative
                    (Monad.is_applicative mDict))) m})))))
    (Monad.getT (Monad.is_applicative mDict))

computeVarReferences :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo
                        a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([]
                        a1) -> LoopState -> a5
computeVarReferences maxReg mDict binfo oinfo bs st =
  Yoneda.iso_to
    (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict)))
    (Monad.forFoldM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict))
      IntMap.emptyIntMap bs (\acc b ->
      Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\bid ->
        let {
         g = \acc1 loopIndex blks ->
          case Prelude.not (IntMap.coq_IntSet_member bid blks) of {
           Prelude.True -> acc1;
           Prelude.False ->
            case Blocks.blockOps mDict binfo b of {
             (,) p zs ->
              case p of {
               (,) xs ys ->
                Lib.forFold acc1 ((Prelude.++) xs ((Prelude.++) ys zs))
                  (\acc2 op ->
                  Lib.forFold acc2 (Blocks.opRefs maxReg mDict oinfo op)
                    (\acc3 v ->
                    case Blocks.varId maxReg v of {
                     Prelude.Left p0 -> acc3;
                     Prelude.Right vid -> addReference loopIndex vid acc3}))}}}}
        in
        Monad.pure
          (unsafeCoerce
            (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))
          (IntMap.coq_IntMap_foldlWithKey g acc (loopIndices st))) (\_ ->
        Blocks.blockId mDict binfo b)))

findLoopEnds :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) ->
                (IntMap.IntMap a1) -> Monad.StateT LoopState a5 ()
findLoopEnds mDict binfo bs =
  let {
   go = let {
         go n b =
           (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
             (\_ ->
             Monad.pure (Monad.coq_StateT_Applicative mDict) ())
             (\n0 ->
             Monad.bind (Monad.coq_StateT_Monad mDict) (\bid ->
               Monad.bind (Monad.coq_StateT_Monad mDict) (\x ->
                 Monad.bind (Monad.coq_StateT_Monad mDict) (\suxs ->
                   Monad.bind (Monad.coq_StateT_Monad mDict) (\x0 ->
                     liftStateT mDict
                       (modifyActiveBlocks (IntMap.coq_IntSet_delete bid)))
                     (Monad.forM_ (Monad.coq_StateT_Monad mDict) suxs
                       (\sux ->
                       Monad.bind (Monad.coq_StateT_Monad mDict) (\active ->
                         Monad.bind (Monad.coq_StateT_Monad mDict) (\x0 ->
                           Monad.bind (Monad.coq_StateT_Monad mDict)
                             (\visited ->
                             case IntMap.coq_IntSet_member sux visited of {
                              Prelude.True ->
                               Monad.pure
                                 (Monad.coq_StateT_Applicative mDict) ();
                              Prelude.False ->
                               case IntMap.coq_IntMap_lookup sux bs of {
                                Prelude.Just x1 -> go n0 x1;
                                Prelude.Nothing ->
                                 Monad.pure
                                   (Monad.coq_StateT_Applicative mDict) ()}})
                             (Monad.getsT (Monad.is_applicative mDict)
                               visitedBlocks))
                           (liftStateT mDict
                             (case IntMap.coq_IntSet_member sux active of {
                               Prelude.True ->
                                Monad.bind
                                  (unsafeCoerce Monad.coq_State_Monad)
                                  (\x0 ->
                                  Monad.bind
                                    (unsafeCoerce Monad.coq_State_Monad)
                                    (\x1 ->
                                    modifyBackwardBranches
                                      (addReference sux bid))
                                    (modifyLoopEndBlocks
                                      (IntMap.coq_IntSet_insert bid)))
                                  (modifyLoopHeaderBlocks (\l ->
                                    case Prelude.not
                                           (Ssrbool.in_mem (unsafeCoerce sux)
                                             (Ssrbool.mem
                                               (Seq.seq_predType
                                                 Ssrnat.nat_eqType)
                                               (unsafeCoerce l))) of {
                                     Prelude.True -> (:) sux l;
                                     Prelude.False -> l}));
                               Prelude.False ->
                                modifyForwardBranches (addReference sux bid)})))
                         (Monad.getsT (Monad.is_applicative mDict)
                           activeBlocks))))
                   (Monad.lift mDict
                     (Yoneda.iso_to
                       (Yoneda.coq_Yoneda_lemma
                         (Monad.is_functor (Monad.is_applicative mDict)))
                       (\_ -> Blocks.blockSuccessors mDict binfo b))))
                 (liftStateT mDict
                   (Monad.bind (unsafeCoerce Monad.coq_State_Monad) (\x ->
                     modifyActiveBlocks (IntMap.coq_IntSet_insert bid))
                     (modifyVisitedBlocks (IntMap.coq_IntSet_insert bid)))))
               (Monad.lift mDict
                 (Yoneda.iso_to
                   (Yoneda.coq_Yoneda_lemma
                     (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->
                   Blocks.blockId mDict binfo b))))
             n}
        in go}
  in
  case IntMap.coq_IntMap_toList bs of {
   [] -> Monad.pure (Monad.coq_StateT_Applicative mDict) ();
   (:) p l ->
    case p of {
     (,) n b -> go (IntMap.coq_IntMap_size bs) b}}

computeBlockOrder :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 
                     a4) -> ([] a1) -> a5
computeBlockOrder mDict binfo blocks =
  case blocks of {
   [] -> Monad.pure (Monad.is_applicative mDict) ((,) emptyLoopState []);
   (:) b bs ->
    Monad.bind mDict (\keys ->
      let {blockMap = IntMap.coq_IntMap_fromList keys} in
      Monad.bind mDict (\z ->
        case z of {
         (,) y st0 ->
          Monad.bind mDict (\blocks' ->
            Monad.bind mDict (\keys' ->
              let {blockMap' = IntMap.coq_IntMap_fromList keys'} in
              Monad.bind mDict (\z' ->
                case z' of {
                 (,) y0 st1 ->
                  case blocks' of {
                   [] ->
                    Monad.pure (Monad.is_applicative mDict) ((,)
                      emptyLoopState []);
                   (:) b' bs' ->
                    Monad.bind mDict (\w ->
                      case w of {
                       (,) y1 st2 ->
                        let {
                         isHeavier = \x y2 ->
                          Monad.bind mDict (\x_id ->
                            Monad.bind mDict (\y_id ->
                              let {
                               x_depth = case IntMap.coq_IntMap_lookup x_id
                                                (loopDepths st2) of {
                                          Prelude.Just p ->
                                           case p of {
                                            (,) idx depth -> depth};
                                          Prelude.Nothing -> 0}}
                              in
                              let {
                               y_depth = case IntMap.coq_IntMap_lookup y_id
                                                (loopDepths st2) of {
                                          Prelude.Just p ->
                                           case p of {
                                            (,) idx depth -> depth};
                                          Prelude.Nothing -> 0}}
                              in
                              Monad.pure (Monad.is_applicative mDict)
                                ((Prelude.<=) ((Prelude.succ) y_depth)
                                  x_depth))
                              (Yoneda.iso_to
                                (Yoneda.coq_Yoneda_lemma
                                  (Monad.is_functor
                                    (Monad.is_applicative mDict))) (\_ ->
                                Blocks.blockId mDict binfo y2)))
                            (Yoneda.iso_to
                              (Yoneda.coq_Yoneda_lemma
                                (Monad.is_functor
                                  (Monad.is_applicative mDict))) (\_ ->
                              Blocks.blockId mDict binfo x))}
                        in
                        let {
                         go = let {
                               go n branches work_list =
                                 (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
                                   (\_ ->
                                   Monad.pure (Monad.is_applicative mDict) [])
                                   (\n0 ->
                                   case work_list of {
                                    [] ->
                                     Monad.pure (Monad.is_applicative mDict)
                                       [];
                                    (:) w0 ws ->
                                     Monad.bind mDict (\bid ->
                                       Monad.bind mDict (\suxs ->
                                         Monad.bind mDict (\x ->
                                           case x of {
                                            (,) branches' ws' ->
                                             Monad.fmap
                                               (Monad.is_functor
                                                 (Monad.is_applicative mDict))
                                               (\x0 -> (:) w0 x0)
                                               (go n0 branches' ws')})
                                           (Monad.forFoldM mDict ((,)
                                             branches ws) suxs (\acc sux ->
                                             case acc of {
                                              (,) branches' ws' ->
                                               Monad.bind mDict
                                                 (\insertion ->
                                                 Monad.pure
                                                   (Monad.is_applicative
                                                     mDict)
                                                   (case IntMap.coq_IntMap_lookup
                                                           sux branches' of {
                                                     Prelude.Just incs -> (,)
                                                      (IntMap.coq_IntMap_insert
                                                        sux
                                                        (IntMap.coq_IntSet_delete
                                                          bid incs)
                                                        branches')
                                                      (case Eqtype.eq_op
                                                              Ssrnat.nat_eqType
                                                              (unsafeCoerce
                                                                (IntMap.coq_IntSet_size
                                                                  incs))
                                                              (unsafeCoerce
                                                                ((Prelude.succ)
                                                                0)) of {
                                                        Prelude.True ->
                                                         insertion;
                                                        Prelude.False -> ws'});
                                                     Prelude.Nothing -> (,)
                                                      branches' insertion}))
                                                 (case IntMap.coq_IntMap_lookup
                                                         sux blockMap' of {
                                                   Prelude.Just s ->
                                                    Monad.insertM mDict
                                                      isHeavier s ws';
                                                   Prelude.Nothing ->
                                                    Monad.pure
                                                      (Monad.is_applicative
                                                        mDict) ws'})})))
                                         (Yoneda.iso_to
                                           (Yoneda.coq_Yoneda_lemma
                                             (Monad.is_functor
                                               (Monad.is_applicative mDict)))
                                           (\_ ->
                                           Blocks.blockSuccessors mDict binfo
                                             w0)))
                                       (Yoneda.iso_to
                                         (Yoneda.coq_Yoneda_lemma
                                           (Monad.is_functor
                                             (Monad.is_applicative mDict)))
                                         (\_ ->
                                         Blocks.blockId mDict binfo w0))})
                                   n}
                              in go}
                        in
                        Monad.bind mDict (\res ->
                          Monad.pure (Monad.is_applicative mDict) ((,) st2
                            res))
                          (go (Data.List.length blocks')
                            (forwardBranches st2) ((:) b' []))})
                      (computeLoopDepths mDict binfo blockMap st1)}})
                (findLoopEnds mDict binfo blockMap' emptyLoopState))
              (Monad.mapM (Monad.is_applicative mDict) (\x ->
                Monad.bind mDict (\bid ->
                  Monad.pure (Monad.is_applicative mDict) ((,) bid x))
                  (Yoneda.iso_to
                    (Yoneda.coq_Yoneda_lemma
                      (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->
                    Blocks.blockId mDict binfo x))) blocks'))
            (Monad.forFoldrM mDict [] blocks (\b0 rest ->
              Monad.bind mDict (\suxs ->
                case (Prelude.<=) (Data.List.length suxs) ((Prelude.succ) 0) of {
                 Prelude.True ->
                  Monad.pure (Monad.is_applicative mDict) ((:) b0 rest);
                 Prelude.False ->
                  Monad.fmap (Monad.is_functor (Monad.is_applicative mDict))
                    (\x ->
                    case x of {
                     (,) b' rest' -> (:) b' rest'})
                    (Monad.forFoldrM mDict ((,) b0 rest) suxs (\sux x ->
                      case x of {
                       (,) b' rest' ->
                        let {
                         fsz = case IntMap.coq_IntMap_lookup sux
                                      (forwardBranches st0) of {
                                Prelude.Just fwds ->
                                 IntMap.coq_IntSet_size fwds;
                                Prelude.Nothing -> 0}}
                        in
                        let {
                         bsz = case IntMap.coq_IntMap_lookup sux
                                      (backwardBranches st0) of {
                                Prelude.Just bwds ->
                                 IntMap.coq_IntSet_size bwds;
                                Prelude.Nothing -> 0}}
                        in
                        case (Prelude.<=) ((Prelude.+) fsz bsz)
                               ((Prelude.succ) 0) of {
                         Prelude.True ->
                          Monad.pure (Monad.is_applicative mDict) ((,) b'
                            rest');
                         Prelude.False ->
                          case IntMap.coq_IntMap_lookup sux blockMap of {
                           Prelude.Just sux' ->
                            Monad.bind mDict (\z0 ->
                              case z0 of {
                               (,) b'' sux'' ->
                                Monad.pure (Monad.is_applicative mDict) ((,)
                                  b'' ((:) sux'' rest'))})
                              (Yoneda.iso_to
                                (Yoneda.coq_Yoneda_lemma
                                  (Monad.is_functor
                                    (Monad.is_applicative mDict))) (\_ ->
                                Blocks.splitCriticalEdge mDict binfo b' sux'));
                           Prelude.Nothing ->
                            Monad.pure (Monad.is_applicative mDict) ((,) b'
                              rest')}}}))})
                (Yoneda.iso_to
                  (Yoneda.coq_Yoneda_lemma
                    (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->
                  Blocks.blockSuccessors mDict binfo b0))))})
        (findLoopEnds mDict binfo blockMap emptyLoopState))
      (Monad.mapM (Monad.is_applicative mDict) (\x ->
        Monad.bind mDict (\bid ->
          Monad.pure (Monad.is_applicative mDict) ((,) bid x))
          (Yoneda.iso_to
            (Yoneda.coq_Yoneda_lemma
              (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->
            Blocks.blockId mDict binfo x))) blocks)}