linearscan-0.8.0: LinearScan/Resolve.hs

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

module LinearScan.Resolve where


import Debug.Trace (trace, traceShow, traceShowId)
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 Hask.Utils

import qualified LinearScan.Allocate as Allocate
import qualified LinearScan.Applicative as Applicative
import qualified LinearScan.Blocks as Blocks
import qualified LinearScan.Functor as Functor
import qualified LinearScan.Graph as Graph
import qualified LinearScan.IntMap as IntMap
import qualified LinearScan.IntSet as IntSet
import qualified LinearScan.Interval as Interval
import qualified LinearScan.List1 as List1
import qualified LinearScan.LiveSets as LiveSets
import qualified LinearScan.Monad as Monad
import qualified LinearScan.Prelude0 as Prelude0
import qualified LinearScan.Range as Range
import qualified LinearScan.UsePos as UsePos
import qualified LinearScan.Eqtype as Eqtype
import qualified LinearScan.Fintype as Fintype
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

__ :: any
__ = Prelude.error "Logical or arity value used"

type PhysReg = Prelude.Int

data ResolvingMove =
   Move PhysReg Blocks.VarId PhysReg
 | Transfer PhysReg Blocks.VarId PhysReg
 | Spill PhysReg Blocks.VarId
 | Restore Blocks.VarId PhysReg
 | AllocReg Blocks.VarId PhysReg
 | FreeReg PhysReg Blocks.VarId
 | Looped ResolvingMove

coq_ResolvingMove_rect :: Prelude.Int -> (PhysReg -> Blocks.VarId -> PhysReg
                          -> a1) -> (PhysReg -> Blocks.VarId -> PhysReg ->
                          a1) -> (PhysReg -> Blocks.VarId -> a1) ->
                          (Blocks.VarId -> PhysReg -> a1) -> (Blocks.VarId ->
                          PhysReg -> a1) -> (PhysReg -> Blocks.VarId -> a1)
                          -> (ResolvingMove -> a1 -> a1) -> ResolvingMove ->
                          a1
coq_ResolvingMove_rect maxReg f f0 f1 f2 f3 f4 f5 r =
  case r of {
   Move p v p0 -> f p v p0;
   Transfer p v p0 -> f0 p v p0;
   Spill p v -> f1 p v;
   Restore v p -> f2 v p;
   AllocReg v p -> f3 v p;
   FreeReg p v -> f4 p v;
   Looped r0 -> f5 r0 (coq_ResolvingMove_rect maxReg f f0 f1 f2 f3 f4 f5 r0)}

data ResolvingMoveSet =
   RSMove Prelude.Int Blocks.VarId Prelude.Int
 | RSTransfer Prelude.Int Blocks.VarId Prelude.Int
 | RSSpill Prelude.Int Blocks.VarId
 | RSRestore Blocks.VarId Prelude.Int
 | RSAllocReg Blocks.VarId Prelude.Int
 | RSFreeReg Prelude.Int Blocks.VarId
 | RSAssignReg Blocks.VarId Prelude.Int
 | RSClearReg Prelude.Int Blocks.VarId
 | RSLooped ResolvingMoveSet

weakenResolvingMove :: Prelude.Int -> ResolvingMove -> ResolvingMoveSet
weakenResolvingMove maxReg x =
  case x of {
   Move fr fv tr -> RSMove ( fr) fv ( tr);
   Transfer fr fv tr -> RSTransfer ( fr) fv ( tr);
   Spill fr tv -> RSSpill ( fr) tv;
   Restore fv tr -> RSRestore fv ( tr);
   AllocReg fv tr -> RSAllocReg fv ( tr);
   FreeReg fr tv -> RSFreeReg ( fr) tv;
   Looped x0 -> RSLooped (weakenResolvingMove maxReg x0)}

eqResolvingMove :: Prelude.Int -> ResolvingMove -> ResolvingMove ->
                   Prelude.Bool
eqResolvingMove maxReg s1 s2 =
  case s1 of {
   Move fr1 fv1 tr1 ->
    case s2 of {
     Move fr2 fv2 tr2 ->
      (Prelude.&&)
        (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1)
          (unsafeCoerce fr2))
        ((Prelude.&&)
          (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1)
            (unsafeCoerce fv2))
          (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)
            (unsafeCoerce tr2)));
     _ -> Prelude.False};
   Transfer fr1 fv1 tr1 ->
    case s2 of {
     Transfer fr2 fv2 tr2 ->
      (Prelude.&&)
        (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1)
          (unsafeCoerce fr2))
        ((Prelude.&&)
          (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1)
            (unsafeCoerce fv2))
          (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)
            (unsafeCoerce tr2)));
     _ -> Prelude.False};
   Spill fr1 fv1 ->
    case s2 of {
     Spill fr2 fv2 ->
      (Prelude.&&)
        (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1)
          (unsafeCoerce fr2))
        (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1)
          (unsafeCoerce fv2));
     _ -> Prelude.False};
   Restore tv1 tr1 ->
    case s2 of {
     Restore tv2 tr2 ->
      (Prelude.&&)
        (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1)
          (unsafeCoerce tv2))
        (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)
          (unsafeCoerce tr2));
     _ -> Prelude.False};
   AllocReg fv1 tr1 ->
    case s2 of {
     AllocReg fv2 tr2 ->
      (Prelude.&&)
        (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1)
          (unsafeCoerce fv2))
        (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)
          (unsafeCoerce tr2));
     _ -> Prelude.False};
   FreeReg fr1 tv1 ->
    case s2 of {
     FreeReg fr2 tv2 ->
      (Prelude.&&)
        (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1)
          (unsafeCoerce fr2))
        (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1)
          (unsafeCoerce tv2));
     _ -> Prelude.False};
   Looped x ->
    case s2 of {
     Looped y -> eqResolvingMove maxReg x y;
     _ -> Prelude.False}}

eqResolvingMoveP :: Prelude.Int -> Eqtype.Equality__Coq_axiom ResolvingMove
eqResolvingMoveP maxReg _top_assumption_ =
  let {
   _evar_0_ = \fr1 fv1 tr1 _top_assumption_0 ->
    let {
     _evar_0_ = \fr2 fv2 tr2 ->
      let {
       _evar_0_ = \_ ->
        let {
         _evar_0_ = let {
                     _evar_0_ = \_ ->
                      let {
                       _evar_0_ = let {
                                   _evar_0_ = \_ ->
                                    let {_evar_0_ = Ssrbool.ReflectT} in
                                     _evar_0_}
                                  in
                                  let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
                                  case Eqtype.eqP
                                         (Fintype.ordinal_eqType maxReg) tr1
                                         tr2 of {
                                   Ssrbool.ReflectT -> _evar_0_ __;
                                   Ssrbool.ReflectF -> _evar_0_0 __}}
                      in
                       _evar_0_}
                    in
                    let {
                     _evar_0_0 = \_ ->
                      let {
                       _evar_0_0 = \_ ->
                        let {_evar_0_0 = Ssrbool.ReflectF} in  _evar_0_0}
                      in
                      let {_evar_0_1 = \_ -> Ssrbool.ReflectF} in
                      case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of {
                       Ssrbool.ReflectT -> _evar_0_0 __;
                       Ssrbool.ReflectF -> _evar_0_1 __}}
                    in
                    case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {
                     Ssrbool.ReflectT -> _evar_0_ __;
                     Ssrbool.ReflectF -> _evar_0_0 __}}
        in
         _evar_0_}
      in
      let {
       _evar_0_0 = \_ ->
        let {
         _evar_0_0 = \_ ->
          let {
           _evar_0_0 = let {
                        _evar_0_0 = \_ ->
                         let {_evar_0_0 = Ssrbool.ReflectF} in  _evar_0_0}
                       in
                       let {_evar_0_1 = \_ -> Ssrbool.ReflectF} in
                       case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1
                              tr2 of {
                        Ssrbool.ReflectT -> _evar_0_0 __;
                        Ssrbool.ReflectF -> _evar_0_1 __}}
          in
           _evar_0_0}
        in
        let {
         _evar_0_1 = \_ ->
          let {
           _evar_0_1 = \_ ->
            let {_evar_0_1 = Ssrbool.ReflectF} in  _evar_0_1}
          in
          let {_evar_0_2 = \_ -> Ssrbool.ReflectF} in
          case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of {
           Ssrbool.ReflectT -> _evar_0_1 __;
           Ssrbool.ReflectF -> _evar_0_2 __}}
        in
        case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {
         Ssrbool.ReflectT -> _evar_0_0 __;
         Ssrbool.ReflectF -> _evar_0_1 __}}
      in
      case Eqtype.eqP (Fintype.ordinal_eqType maxReg) fr1 fr2 of {
       Ssrbool.ReflectT -> _evar_0_ __;
       Ssrbool.ReflectF -> _evar_0_0 __}}
    in
    let {_evar_0_0 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_1 = \fr2 fv2 -> Ssrbool.ReflectF} in
    let {_evar_0_2 = \tv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_3 = \fv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_4 = \fr2 tv2 -> Ssrbool.ReflectF} in
    let {_evar_0_5 = \y -> Ssrbool.ReflectF} in
    case _top_assumption_0 of {
     Move x x0 x1 -> unsafeCoerce _evar_0_ x x0 x1;
     Transfer x x0 x1 -> _evar_0_0 x x0 x1;
     Spill x x0 -> _evar_0_1 x x0;
     Restore x x0 -> _evar_0_2 x x0;
     AllocReg x x0 -> _evar_0_3 x x0;
     FreeReg x x0 -> _evar_0_4 x x0;
     Looped x -> _evar_0_5 x}}
  in
  let {
   _evar_0_0 = \fr1 fv1 tr1 _top_assumption_0 ->
    let {_evar_0_0 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
    let {
     _evar_0_1 = \fr2 fv2 tr2 ->
      let {
       _evar_0_1 = \_ ->
        let {
         _evar_0_1 = let {
                      _evar_0_1 = \_ ->
                       let {
                        _evar_0_1 = let {
                                     _evar_0_1 = \_ ->
                                      let {_evar_0_1 = Ssrbool.ReflectT} in
                                       _evar_0_1}
                                    in
                                    let {_evar_0_2 = \_ -> Ssrbool.ReflectF}
                                    in
                                    case Eqtype.eqP
                                           (Fintype.ordinal_eqType maxReg)
                                           tr1 tr2 of {
                                     Ssrbool.ReflectT -> _evar_0_1 __;
                                     Ssrbool.ReflectF -> _evar_0_2 __}}
                       in
                        _evar_0_1}
                     in
                     let {
                      _evar_0_2 = \_ ->
                       let {
                        _evar_0_2 = \_ ->
                         let {_evar_0_2 = Ssrbool.ReflectF} in  _evar_0_2}
                       in
                       let {_evar_0_3 = \_ -> Ssrbool.ReflectF} in
                       case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1
                              tr2 of {
                        Ssrbool.ReflectT -> _evar_0_2 __;
                        Ssrbool.ReflectF -> _evar_0_3 __}}
                     in
                     case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {
                      Ssrbool.ReflectT -> _evar_0_1 __;
                      Ssrbool.ReflectF -> _evar_0_2 __}}
        in
         _evar_0_1}
      in
      let {
       _evar_0_2 = \_ ->
        let {
         _evar_0_2 = \_ ->
          let {
           _evar_0_2 = let {
                        _evar_0_2 = \_ ->
                         let {_evar_0_2 = Ssrbool.ReflectF} in  _evar_0_2}
                       in
                       let {_evar_0_3 = \_ -> Ssrbool.ReflectF} in
                       case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1
                              tr2 of {
                        Ssrbool.ReflectT -> _evar_0_2 __;
                        Ssrbool.ReflectF -> _evar_0_3 __}}
          in
           _evar_0_2}
        in
        let {
         _evar_0_3 = \_ ->
          let {
           _evar_0_3 = \_ ->
            let {_evar_0_3 = Ssrbool.ReflectF} in  _evar_0_3}
          in
          let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in
          case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of {
           Ssrbool.ReflectT -> _evar_0_3 __;
           Ssrbool.ReflectF -> _evar_0_4 __}}
        in
        case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {
         Ssrbool.ReflectT -> _evar_0_2 __;
         Ssrbool.ReflectF -> _evar_0_3 __}}
      in
      case Eqtype.eqP (Fintype.ordinal_eqType maxReg) fr1 fr2 of {
       Ssrbool.ReflectT -> _evar_0_1 __;
       Ssrbool.ReflectF -> _evar_0_2 __}}
    in
    let {_evar_0_2 = \fr2 fv2 -> Ssrbool.ReflectF} in
    let {_evar_0_3 = \tv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_4 = \fv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_5 = \fr2 tv2 -> Ssrbool.ReflectF} in
    let {_evar_0_6 = \y -> Ssrbool.ReflectF} in
    case _top_assumption_0 of {
     Move x x0 x1 -> _evar_0_0 x x0 x1;
     Transfer x x0 x1 -> unsafeCoerce _evar_0_1 x x0 x1;
     Spill x x0 -> _evar_0_2 x x0;
     Restore x x0 -> _evar_0_3 x x0;
     AllocReg x x0 -> _evar_0_4 x x0;
     FreeReg x x0 -> _evar_0_5 x x0;
     Looped x -> _evar_0_6 x}}
  in
  let {
   _evar_0_1 = \fr1 fv1 _top_assumption_0 ->
    let {_evar_0_1 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_2 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
    let {
     _evar_0_3 = \fr2 fv2 ->
      let {
       _evar_0_3 = \_ ->
        let {
         _evar_0_3 = let {
                      _evar_0_3 = \_ ->
                       let {_evar_0_3 = Ssrbool.ReflectT} in  _evar_0_3}
                     in
                     let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in
                     case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {
                      Ssrbool.ReflectT -> _evar_0_3 __;
                      Ssrbool.ReflectF -> _evar_0_4 __}}
        in
         _evar_0_3}
      in
      let {
       _evar_0_4 = \_ ->
        let {
         _evar_0_4 = \_ -> let {_evar_0_4 = Ssrbool.ReflectF} in  _evar_0_4}
        in
        let {_evar_0_5 = \_ -> Ssrbool.ReflectF} in
        case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {
         Ssrbool.ReflectT -> _evar_0_4 __;
         Ssrbool.ReflectF -> _evar_0_5 __}}
      in
      case Eqtype.eqP (Fintype.ordinal_eqType maxReg) fr1 fr2 of {
       Ssrbool.ReflectT -> _evar_0_3 __;
       Ssrbool.ReflectF -> _evar_0_4 __}}
    in
    let {_evar_0_4 = \tv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_5 = \fv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_6 = \fr2 tv2 -> Ssrbool.ReflectF} in
    let {_evar_0_7 = \y -> Ssrbool.ReflectF} in
    case _top_assumption_0 of {
     Move x x0 x1 -> _evar_0_1 x x0 x1;
     Transfer x x0 x1 -> _evar_0_2 x x0 x1;
     Spill x x0 -> unsafeCoerce _evar_0_3 x x0;
     Restore x x0 -> _evar_0_4 x x0;
     AllocReg x x0 -> _evar_0_5 x x0;
     FreeReg x x0 -> _evar_0_6 x x0;
     Looped x -> _evar_0_7 x}}
  in
  let {
   _evar_0_2 = \tv1 tr1 _top_assumption_0 ->
    let {_evar_0_2 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_3 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_4 = \fr2 fv2 -> Ssrbool.ReflectF} in
    let {
     _evar_0_5 = \tv2 tr2 ->
      let {
       _evar_0_5 = \_ ->
        let {
         _evar_0_5 = let {
                      _evar_0_5 = \_ ->
                       let {_evar_0_5 = Ssrbool.ReflectT} in  _evar_0_5}
                     in
                     let {_evar_0_6 = \_ -> Ssrbool.ReflectF} in
                     case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of {
                      Ssrbool.ReflectT -> _evar_0_5 __;
                      Ssrbool.ReflectF -> _evar_0_6 __}}
        in
         _evar_0_5}
      in
      let {
       _evar_0_6 = \_ ->
        let {
         _evar_0_6 = \_ -> let {_evar_0_6 = Ssrbool.ReflectF} in  _evar_0_6}
        in
        let {_evar_0_7 = \_ -> Ssrbool.ReflectF} in
        case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of {
         Ssrbool.ReflectT -> _evar_0_6 __;
         Ssrbool.ReflectF -> _evar_0_7 __}}
      in
      case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of {
       Ssrbool.ReflectT -> _evar_0_5 __;
       Ssrbool.ReflectF -> _evar_0_6 __}}
    in
    let {_evar_0_6 = \fv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_7 = \fr2 tv2 -> Ssrbool.ReflectF} in
    let {_evar_0_8 = \y -> Ssrbool.ReflectF} in
    case _top_assumption_0 of {
     Move x x0 x1 -> _evar_0_2 x x0 x1;
     Transfer x x0 x1 -> _evar_0_3 x x0 x1;
     Spill x x0 -> _evar_0_4 x x0;
     Restore x x0 -> unsafeCoerce _evar_0_5 x x0;
     AllocReg x x0 -> _evar_0_6 x x0;
     FreeReg x x0 -> _evar_0_7 x x0;
     Looped x -> _evar_0_8 x}}
  in
  let {
   _evar_0_3 = \fv1 tr1 _top_assumption_0 ->
    let {_evar_0_3 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_4 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_5 = \fr2 fv2 -> Ssrbool.ReflectF} in
    let {_evar_0_6 = \tv2 tr2 -> Ssrbool.ReflectF} in
    let {
     _evar_0_7 = \fv2 tr2 ->
      let {
       _evar_0_7 = \_ ->
        let {
         _evar_0_7 = let {
                      _evar_0_7 = \_ ->
                       let {_evar_0_7 = Ssrbool.ReflectT} in  _evar_0_7}
                     in
                     let {_evar_0_8 = \_ -> Ssrbool.ReflectF} in
                     case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of {
                      Ssrbool.ReflectT -> _evar_0_7 __;
                      Ssrbool.ReflectF -> _evar_0_8 __}}
        in
         _evar_0_7}
      in
      let {
       _evar_0_8 = \_ ->
        let {
         _evar_0_8 = \_ -> let {_evar_0_8 = Ssrbool.ReflectF} in  _evar_0_8}
        in
        let {_evar_0_9 = \_ -> Ssrbool.ReflectF} in
        case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of {
         Ssrbool.ReflectT -> _evar_0_8 __;
         Ssrbool.ReflectF -> _evar_0_9 __}}
      in
      case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {
       Ssrbool.ReflectT -> _evar_0_7 __;
       Ssrbool.ReflectF -> _evar_0_8 __}}
    in
    let {_evar_0_8 = \fr2 tv2 -> Ssrbool.ReflectF} in
    let {_evar_0_9 = \y -> Ssrbool.ReflectF} in
    case _top_assumption_0 of {
     Move x x0 x1 -> _evar_0_3 x x0 x1;
     Transfer x x0 x1 -> _evar_0_4 x x0 x1;
     Spill x x0 -> _evar_0_5 x x0;
     Restore x x0 -> _evar_0_6 x x0;
     AllocReg x x0 -> unsafeCoerce _evar_0_7 x x0;
     FreeReg x x0 -> _evar_0_8 x x0;
     Looped x -> _evar_0_9 x}}
  in
  let {
   _evar_0_4 = \fr1 tv1 _top_assumption_0 ->
    let {_evar_0_4 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_5 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_6 = \fr2 fv2 -> Ssrbool.ReflectF} in
    let {_evar_0_7 = \tv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_8 = \fv2 tr2 -> Ssrbool.ReflectF} in
    let {
     _evar_0_9 = \fr2 tv2 ->
      let {
       _evar_0_9 = \_ ->
        let {
         _evar_0_9 = let {
                      _evar_0_9 = \_ ->
                       let {_evar_0_9 = Ssrbool.ReflectT} in  _evar_0_9}
                     in
                     let {_evar_0_10 = \_ -> Ssrbool.ReflectF} in
                     case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of {
                      Ssrbool.ReflectT -> _evar_0_9 __;
                      Ssrbool.ReflectF -> _evar_0_10 __}}
        in
         _evar_0_9}
      in
      let {
       _evar_0_10 = \_ ->
        let {
         _evar_0_10 = \_ ->
          let {_evar_0_10 = Ssrbool.ReflectF} in  _evar_0_10}
        in
        let {_evar_0_11 = \_ -> Ssrbool.ReflectF} in
        case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of {
         Ssrbool.ReflectT -> _evar_0_10 __;
         Ssrbool.ReflectF -> _evar_0_11 __}}
      in
      case Eqtype.eqP (Fintype.ordinal_eqType maxReg) fr1 fr2 of {
       Ssrbool.ReflectT -> _evar_0_9 __;
       Ssrbool.ReflectF -> _evar_0_10 __}}
    in
    let {_evar_0_10 = \y -> Ssrbool.ReflectF} in
    case _top_assumption_0 of {
     Move x x0 x1 -> _evar_0_4 x x0 x1;
     Transfer x x0 x1 -> _evar_0_5 x x0 x1;
     Spill x x0 -> _evar_0_6 x x0;
     Restore x x0 -> _evar_0_7 x x0;
     AllocReg x x0 -> _evar_0_8 x x0;
     FreeReg x x0 -> unsafeCoerce _evar_0_9 x x0;
     Looped x -> _evar_0_10 x}}
  in
  let {
   _evar_0_5 = \x iHx _top_assumption_0 ->
    let {_evar_0_5 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_6 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_7 = \fr2 fv2 -> Ssrbool.ReflectF} in
    let {_evar_0_8 = \tv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_9 = \fv2 tr2 -> Ssrbool.ReflectF} in
    let {_evar_0_10 = \fr2 tv2 -> Ssrbool.ReflectF} in
    let {
     _evar_0_11 = \y ->
      let {iHx0 = iHx y} in
      let {_evar_0_11 = \_ -> Ssrbool.ReflectT} in
      let {_evar_0_12 = \_ -> Ssrbool.ReflectF} in
      case iHx0 of {
       Ssrbool.ReflectT -> _evar_0_11 __;
       Ssrbool.ReflectF -> _evar_0_12 __}}
    in
    case _top_assumption_0 of {
     Move x0 x1 x2 -> _evar_0_5 x0 x1 x2;
     Transfer x0 x1 x2 -> _evar_0_6 x0 x1 x2;
     Spill x0 x1 -> _evar_0_7 x0 x1;
     Restore x0 x1 -> _evar_0_8 x0 x1;
     AllocReg x0 x1 -> _evar_0_9 x0 x1;
     FreeReg x0 x1 -> _evar_0_10 x0 x1;
     Looped x0 -> _evar_0_11 x0}}
  in
  coq_ResolvingMove_rect maxReg (unsafeCoerce _evar_0_)
    (unsafeCoerce _evar_0_0) (unsafeCoerce _evar_0_1)
    (unsafeCoerce _evar_0_2) (unsafeCoerce _evar_0_3)
    (unsafeCoerce _evar_0_4) _evar_0_5 _top_assumption_

coq_ResolvingMove_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of
                             ResolvingMove
coq_ResolvingMove_eqMixin maxReg =
  Eqtype.Equality__Mixin (eqResolvingMove maxReg) (eqResolvingMoveP maxReg)

coq_ResolvingMove_eqType :: Prelude.Int -> Eqtype.Equality__Coq_type
coq_ResolvingMove_eqType maxReg =
  unsafeCoerce (coq_ResolvingMove_eqMixin maxReg)

data ResGraphNode =
   RegNode PhysReg
 | VarNode Blocks.VarId
 | VirtNode ResGraphNode

coq_ResGraphNode_rect :: Prelude.Int -> (PhysReg -> a1) -> (Blocks.VarId ->
                         a1) -> (ResGraphNode -> a1 -> a1) -> ResGraphNode ->
                         a1
coq_ResGraphNode_rect maxReg f f0 f1 r =
  case r of {
   RegNode p -> f p;
   VarNode v -> f0 v;
   VirtNode r0 -> f1 r0 (coq_ResGraphNode_rect maxReg f f0 f1 r0)}

eqResGraphNode :: Prelude.Int -> ResGraphNode -> ResGraphNode -> Prelude.Bool
eqResGraphNode maxReg s1 s2 =
  case s1 of {
   RegNode r1 ->
    case s2 of {
     RegNode r2 ->
      Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce r1)
        (unsafeCoerce r2);
     _ -> Prelude.False};
   VarNode v1 ->
    case s2 of {
     VarNode v2 ->
      Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce v1) (unsafeCoerce v2);
     _ -> Prelude.False};
   VirtNode n1 ->
    case s2 of {
     VirtNode n2 -> eqResGraphNode maxReg n1 n2;
     _ -> Prelude.False}}

eqResGraphNodeP :: Prelude.Int -> Eqtype.Equality__Coq_axiom ResGraphNode
eqResGraphNodeP maxReg _top_assumption_ =
  let {
   _evar_0_ = \r1 _top_assumption_0 ->
    let {
     _evar_0_ = \r2 ->
      let {_evar_0_ = \_ -> let {_evar_0_ = Ssrbool.ReflectT} in  _evar_0_}
      in
      let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
      case Eqtype.eqP (Fintype.ordinal_eqType maxReg) r1 r2 of {
       Ssrbool.ReflectT -> _evar_0_ __;
       Ssrbool.ReflectF -> _evar_0_0 __}}
    in
    let {_evar_0_0 = \v2 -> Ssrbool.ReflectF} in
    let {_evar_0_1 = \n2 -> Ssrbool.ReflectF} in
    case _top_assumption_0 of {
     RegNode x -> unsafeCoerce _evar_0_ x;
     VarNode x -> _evar_0_0 x;
     VirtNode x -> _evar_0_1 x}}
  in
  let {
   _evar_0_0 = \v1 _top_assumption_0 ->
    let {_evar_0_0 = \r2 -> Ssrbool.ReflectF} in
    let {
     _evar_0_1 = \v2 ->
      let {
       _evar_0_1 = \_ -> let {_evar_0_1 = Ssrbool.ReflectT} in  _evar_0_1}
      in
      let {_evar_0_2 = \_ -> Ssrbool.ReflectF} in
      case Eqtype.eqP Ssrnat.nat_eqType v1 v2 of {
       Ssrbool.ReflectT -> _evar_0_1 __;
       Ssrbool.ReflectF -> _evar_0_2 __}}
    in
    let {_evar_0_2 = \n2 -> Ssrbool.ReflectF} in
    case _top_assumption_0 of {
     RegNode x -> _evar_0_0 x;
     VarNode x -> unsafeCoerce _evar_0_1 x;
     VirtNode x -> _evar_0_2 x}}
  in
  let {
   _evar_0_1 = \n1 iHn _top_assumption_0 ->
    let {_evar_0_1 = \r2 -> Ssrbool.ReflectF} in
    let {_evar_0_2 = \v2 -> Ssrbool.ReflectF} in
    let {
     _evar_0_3 = \n2 ->
      let {iHn0 = iHn n2} in
      let {_evar_0_3 = \_ -> Ssrbool.ReflectT} in
      let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in
      case iHn0 of {
       Ssrbool.ReflectT -> _evar_0_3 __;
       Ssrbool.ReflectF -> _evar_0_4 __}}
    in
    case _top_assumption_0 of {
     RegNode x -> _evar_0_1 x;
     VarNode x -> _evar_0_2 x;
     VirtNode x -> _evar_0_3 x}}
  in
  coq_ResGraphNode_rect maxReg (unsafeCoerce _evar_0_)
    (unsafeCoerce _evar_0_0) _evar_0_1 _top_assumption_

coq_ResGraphNode_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of
                            ResGraphNode
coq_ResGraphNode_eqMixin maxReg =
  Eqtype.Equality__Mixin (eqResGraphNode maxReg) (eqResGraphNodeP maxReg)

coq_ResGraphNode_eqType :: Prelude.Int -> Eqtype.Equality__Coq_type
coq_ResGraphNode_eqType maxReg =
  unsafeCoerce (coq_ResGraphNode_eqMixin maxReg)

data ResGraphEdge =
   Build_ResGraphEdge ResolvingMove Prelude.Bool

resMove :: Prelude.Int -> ResGraphEdge -> ResolvingMove
resMove maxReg r =
  case r of {
   Build_ResGraphEdge resMove0 resGhost0 -> resMove0}

resGhost :: Prelude.Int -> ResGraphEdge -> Prelude.Bool
resGhost maxReg r =
  case r of {
   Build_ResGraphEdge resMove0 resGhost0 -> resGhost0}

eqResGraphEdge :: Prelude.Int -> ResGraphEdge -> ResGraphEdge -> Prelude.Bool
eqResGraphEdge maxReg s1 s2 =
  case s1 of {
   Build_ResGraphEdge a1 b1 ->
    case s2 of {
     Build_ResGraphEdge a2 b2 ->
      (Prelude.&&)
        (Eqtype.eq_op (coq_ResolvingMove_eqType maxReg) (unsafeCoerce a1)
          (unsafeCoerce a2))
        (Eqtype.eq_op Eqtype.bool_eqType (unsafeCoerce b1) (unsafeCoerce b2))}}

eqResGraphEdgeP :: Prelude.Int -> Eqtype.Equality__Coq_axiom ResGraphEdge
eqResGraphEdgeP maxReg _top_assumption_ =
  let {
   _evar_0_ = \a1 b1 _top_assumption_0 ->
    let {
     _evar_0_ = \a2 b2 ->
      let {
       _evar_0_ = \_ ->
        let {
         _evar_0_ = let {
                     _evar_0_ = \_ ->
                      let {_evar_0_ = Ssrbool.ReflectT} in  _evar_0_}
                    in
                    let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
                    case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {
                     Ssrbool.ReflectT -> _evar_0_ __;
                     Ssrbool.ReflectF -> _evar_0_0 __}}
        in
         _evar_0_}
      in
      let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
      case Eqtype.eqP (coq_ResolvingMove_eqType maxReg) a1 a2 of {
       Ssrbool.ReflectT -> _evar_0_ __;
       Ssrbool.ReflectF -> _evar_0_0 __}}
    in
    case _top_assumption_0 of {
     Build_ResGraphEdge x x0 -> unsafeCoerce _evar_0_ x x0}}
  in
  case _top_assumption_ of {
   Build_ResGraphEdge x x0 -> unsafeCoerce _evar_0_ x x0}

coq_ResGraphEdge_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of
                            ResGraphEdge
coq_ResGraphEdge_eqMixin maxReg =
  Eqtype.Equality__Mixin (eqResGraphEdge maxReg) (eqResGraphEdgeP maxReg)

coq_ResGraphEdge_eqType :: Prelude.Int -> Eqtype.Equality__Coq_type
coq_ResGraphEdge_eqType maxReg =
  unsafeCoerce (coq_ResGraphEdge_eqMixin maxReg)

determineEdge :: Prelude.Int -> ResGraphEdge -> (,) ResGraphNode ResGraphNode
determineEdge maxReg x =
  let {
   go m =
     case m of {
      Move fr fv tr -> (,) (RegNode tr) (RegNode fr);
      Transfer fr fv tr -> (,) (RegNode tr) (RegNode fr);
      Spill fr tv -> (,) (VirtNode (VarNode tv)) (RegNode fr);
      Restore fv tr -> (,) (RegNode tr) (VarNode fv);
      AllocReg fv tr -> (,) (RegNode tr) (VarNode fv);
      FreeReg fr tv -> (,) (VirtNode (VarNode tv)) (RegNode fr);
      Looped x0 -> go x0}}
  in go (resMove maxReg x)

compareEdges :: Prelude.Int -> ((,) Prelude.Int ResGraphEdge) -> ((,)
                Prelude.Int ResGraphEdge) -> Prelude.Bool
compareEdges maxReg x y =
  let {xe = determineEdge maxReg (Prelude.snd x)} in
  let {ye = determineEdge maxReg (Prelude.snd y)} in
  case (Prelude.&&)
         (Eqtype.eq_op Ssrnat.nat_eqType (Prelude.fst (unsafeCoerce x))
           (Prelude.fst (unsafeCoerce y)))
         (Eqtype.eq_op (coq_ResGraphNode_eqType maxReg)
           (Prelude.fst (unsafeCoerce xe)) (Prelude.fst (unsafeCoerce ye))) of {
   Prelude.True ->
    (Prelude.&&) (resGhost maxReg (Prelude.snd x))
      (Prelude.not (resGhost maxReg (Prelude.snd y)));
   Prelude.False -> Prelude.False}

isEdgeSplittable :: Prelude.Int -> ResGraphEdge -> Prelude.Bool
isEdgeSplittable maxReg x =
  case resMove maxReg x of {
   Move p v p0 -> Prelude.True;
   Transfer p v p0 -> Prelude.True;
   _ -> Prelude.False}

splitEdge :: Prelude.Int -> ResGraphEdge -> [] ResGraphEdge
splitEdge maxReg x =
  case resMove maxReg x of {
   Move fr fv tr -> (:) (Build_ResGraphEdge (Spill fr fv) Prelude.False) ((:)
    (Build_ResGraphEdge (Restore fv tr) (resGhost maxReg x)) []);
   Transfer fr fv tr -> (:) (Build_ResGraphEdge (FreeReg fr fv)
    Prelude.False) ((:) (Build_ResGraphEdge (AllocReg fv tr)
    (resGhost maxReg x)) []);
   Looped r -> (:) x [];
   _ -> (:) (Build_ResGraphEdge (Looped (resMove maxReg x))
    (resGhost maxReg x)) []}

sortMoves :: Prelude.Int -> Graph.Graph -> [] ResGraphEdge
sortMoves maxReg x =
  Prelude.map (\i -> Prelude.snd (unsafeCoerce i))
    (List1.sortBy (unsafeCoerce (compareEdges maxReg))
      (Prelude.snd
        (Graph.topsort (coq_ResGraphNode_eqType maxReg)
          (coq_ResGraphEdge_eqType maxReg) x
          (unsafeCoerce (isEdgeSplittable maxReg))
          (unsafeCoerce (splitEdge maxReg)))))

determineMoves :: Prelude.Int -> (IntMap.IntMap ([] ResGraphEdge)) -> []
                  ResGraphEdge
determineMoves maxReg moves =
  sortMoves maxReg
    (IntMap.coq_IntMap_foldr
      (Prelude0.flip
        (Prelude.foldr
          (unsafeCoerce
            (Graph.addEdge (coq_ResGraphNode_eqType maxReg)
              (coq_ResGraphEdge_eqType maxReg)))))
      (Graph.emptyGraph (coq_ResGraphNode_eqType maxReg)
        (coq_ResGraphEdge_eqType maxReg)
        (unsafeCoerce (determineEdge maxReg))) moves)

resolvingMoves :: Prelude.Int -> ([] Allocate.Allocation) -> (Prelude.Maybe
                  IntSet.IntSet) -> Prelude.Int -> Prelude.Int ->
                  IntMap.IntMap ([] ResGraphEdge)
resolvingMoves maxReg allocs liveIn from to =
  let {
   collect = \p q i rest ->
    let {int = Allocate.intVal maxReg i} in
    case p int of {
     Prelude.True -> IntMap.coq_IntMap_alter (q i) (Interval.ivar int) rest;
     Prelude.False -> rest}}
  in
  let {
   liveAtFrom = Prelude.foldr
                  (collect (\i ->
                    (Prelude.&&) ((Prelude.<=) (Interval.ibeg i) from)
                      ((Prelude.<=) ((Prelude.succ) from) (Interval.iend i)))
                    (\a x -> Prelude.Just a)) IntMap.emptyIntMap allocs}
  in
  let {
   shouldKeep = \int pos ->
    case (Prelude.<=) (Interval.ibeg int) pos of {
     Prelude.True ->
      case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos)
             (unsafeCoerce (Interval.iend int)) of {
       Prelude.True -> (,)
        (case Interval.lastUsePos int of {
          Prelude.Just u -> (Prelude.<=) to (UsePos.uloc u);
          Prelude.Nothing -> Prelude.False}) Prelude.True;
       Prelude.False -> (,)
        ((Prelude.<=) ((Prelude.succ) to) (Interval.iend int)) Prelude.False};
     Prelude.False -> (,) Prelude.False Prelude.False}}
  in
  let {
   outputBegin = \int pos ->
    Range.hasOnlyOutputsAt ( (Prelude.head (Interval.rds int))) pos}
  in
  let {
   liveAtTo = Prelude.foldr
                (collect (\i -> Prelude.fst (shouldKeep i to)) (\a rest ->
                  Prelude.Just ((:) ((,) ((,) a
                  (Prelude.snd (shouldKeep (Allocate.intVal maxReg a) to)))
                  (outputBegin (Allocate.intVal maxReg a) to))
                  (case rest of {
                    Prelude.Just xs -> xs;
                    Prelude.Nothing -> []})))) IntMap.emptyIntMap allocs}
  in
  let {
   varNotLive = \vid ->
    case liveIn of {
     Prelude.Just ins -> Prelude.not (IntSet.coq_IntSet_member vid ins);
     Prelude.Nothing -> Prelude.False}}
  in
  let {
   regsReferenced = IntMap.coq_IntMap_mergeWithKey (\vid x yps ->
                      let {
                       go = \acc yp ->
                        case yp of {
                         (,) y0 y1 ->
                          case y0 of {
                           (,) y y2 ->
                            case Prelude.not
                                   (Eqtype.eq_op
                                     (Eqtype.option_eqType
                                       (Fintype.ordinal_eqType maxReg))
                                     (unsafeCoerce
                                       (Allocate.intReg maxReg x))
                                     (unsafeCoerce
                                       (Allocate.intReg maxReg y))) of {
                             Prelude.True ->
                              let {
                               next = case Allocate.intReg maxReg y of {
                                       Prelude.Just yreg -> (:) yreg acc;
                                       Prelude.Nothing -> acc}}
                              in
                              case Allocate.intReg maxReg x of {
                               Prelude.Just xreg -> (:) xreg next;
                               Prelude.Nothing -> next};
                             Prelude.False -> acc}}}}
                      in
                      Prelude.Just (Data.List.foldl' go [] yps))
                      (IntMap.coq_IntMap_foldlWithKey (\acc vid x ->
                        case Allocate.intReg maxReg x of {
                         Prelude.Just xreg ->
                          IntMap.coq_IntMap_addToList vid xreg acc;
                         Prelude.Nothing -> acc}) IntMap.emptyIntMap)
                      (IntMap.coq_IntMap_foldlWithKey (\acc vid yps ->
                        let {
                         go = \acc0 yp ->
                          case yp of {
                           (,) y0 y1 ->
                            case y0 of {
                             (,) y y2 ->
                              case Allocate.intReg maxReg y of {
                               Prelude.Just yreg ->
                                IntMap.coq_IntMap_addToList vid yreg acc0;
                               Prelude.Nothing -> acc0}}}}
                        in
                        Data.List.foldl' go acc yps) IntMap.emptyIntMap)
                      liveAtFrom liveAtTo}
  in
  let {
   otherRegs = List1.concat
                 (Prelude.map (\x ->
                   (Prelude..) (Prelude.map Prelude.id) Prelude.snd x)
                   (IntMap.coq_IntMap_toList regsReferenced))}
  in
  IntMap.coq_IntMap_mergeWithKey (\vid x yps ->
    let {
     go = \yp ->
      case yp of {
       (,) y0 outb ->
        case y0 of {
         (,) y ghost ->
          case Eqtype.eq_op
                 (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))
                 (unsafeCoerce (Allocate.intReg maxReg x))
                 (unsafeCoerce (Allocate.intReg maxReg y)) of {
           Prelude.True ->
            case Allocate.intReg maxReg y of {
             Prelude.Just reg ->
              case ghost of {
               Prelude.True -> (:) (Build_ResGraphEdge (FreeReg reg vid)
                Prelude.True) [];
               Prelude.False ->
                case IntSet.coq_IntSet_member ( reg) otherRegs of {
                 Prelude.True -> (:) (Build_ResGraphEdge (FreeReg reg vid)
                  Prelude.False) ((:) (Build_ResGraphEdge (AllocReg vid reg)
                  Prelude.False) []);
                 Prelude.False -> []}};
             Prelude.Nothing -> []};
           Prelude.False ->
            let {
             mmv = case Allocate.intReg maxReg x of {
                    Prelude.Just xr ->
                     case Allocate.intReg maxReg y of {
                      Prelude.Just yr -> Prelude.Just
                       (case (Prelude.||) outb (varNotLive vid) of {
                         Prelude.True -> Transfer xr vid yr;
                         Prelude.False -> Move xr vid yr});
                      Prelude.Nothing -> Prelude.Just (Spill xr vid)};
                    Prelude.Nothing ->
                     case Allocate.intReg maxReg y of {
                      Prelude.Just yr -> Prelude.Just
                       (case (Prelude.||) outb (varNotLive vid) of {
                         Prelude.True -> AllocReg vid yr;
                         Prelude.False -> Restore vid yr});
                      Prelude.Nothing -> Prelude.Nothing}}}
            in
            case mmv of {
             Prelude.Just mv -> (:) (Build_ResGraphEdge mv ghost) [];
             Prelude.Nothing -> []}}}}}
    in
    List1.listToMaybe
      (Data.List.foldl' (\acc x0 -> (Prelude.++) acc (go x0)) [] yps))
    (IntMap.coq_IntMap_foldlWithKey (\acc vid x ->
      case Allocate.intReg maxReg x of {
       Prelude.Just r ->
        IntMap.coq_IntMap_addToList vid (Build_ResGraphEdge (FreeReg r vid)
          Prelude.False) acc;
       Prelude.Nothing -> acc}) IntMap.emptyIntMap)
    (IntMap.coq_IntMap_foldlWithKey (\acc vid yps ->
      let {
       go = \acc0 yp ->
        case yp of {
         (,) y0 outb ->
          case y0 of {
           (,) y ghost ->
            case Allocate.intReg maxReg y of {
             Prelude.Just r ->
              IntMap.coq_IntMap_addToList vid (Build_ResGraphEdge (AllocReg
                vid r) ghost) acc0;
             Prelude.Nothing -> acc0}}}}
      in
      Data.List.foldl' go acc yps) IntMap.emptyIntMap) liveAtFrom liveAtTo

type BlockMoves = (,) Graph.Graph Graph.Graph

applyMappings :: Prelude.Int -> Blocks.BlockId -> (IntMap.IntMap BlockMoves)
                 -> Prelude.Bool -> (IntMap.IntMap ([] ResGraphEdge)) ->
                 IntMap.IntMap BlockMoves
applyMappings maxReg bid mappings in_from moves =
  let {
   go = \ms mv ->
    let {
     addToGraphs = \e xs ->
      case xs of {
       (,) gbeg gend ->
        case in_from of {
         Prelude.True -> (,) gbeg
          (Graph.addEdge (coq_ResGraphNode_eqType maxReg)
            (coq_ResGraphEdge_eqType maxReg) e gend);
         Prelude.False -> (,)
          (Graph.addEdge (coq_ResGraphNode_eqType maxReg)
            (coq_ResGraphEdge_eqType maxReg) e gbeg) gend}}}
    in
    let {
     eg = Graph.emptyGraph (coq_ResGraphNode_eqType maxReg)
            (coq_ResGraphEdge_eqType maxReg)
            (unsafeCoerce (determineEdge maxReg))}
    in
    let {
     f = \mxs ->
      addToGraphs mv
        (case mxs of {
          Prelude.Just xs -> xs;
          Prelude.Nothing -> (,) eg eg})}
    in
    IntMap.coq_IntMap_alter ((Prelude..) (\x -> Prelude.Just x) f) bid ms}
  in
  IntMap.coq_IntMap_foldl (Data.List.foldl' (unsafeCoerce go)) mappings moves

checkBlockBoundary :: Prelude.Int -> ([] Allocate.Allocation) ->
                      Blocks.BlockId -> Prelude.Bool ->
                      LiveSets.BlockLiveSets -> LiveSets.BlockLiveSets ->
                      IntSet.IntSet -> (IntMap.IntMap BlockMoves) ->
                      IntMap.IntMap BlockMoves
checkBlockBoundary maxReg allocs bid in_from from to liveIn mappings =
  applyMappings maxReg bid mappings in_from
    (resolvingMoves maxReg allocs (Prelude.Just liveIn)
      (LiveSets.blockLastOpId from) (LiveSets.blockFirstOpId to))

resolveDataFlow :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo 
                   a5 a1 a2 a3 a4) -> ([] Allocate.Allocation) -> ([] 
                   a1) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> a5
resolveDataFlow maxReg mDict binfo allocs blocks liveSets =
  Functor.fmap (Applicative.is_functor (Monad.is_applicative mDict))
    Prelude.fst
    (Monad.forFoldM mDict ((,) IntMap.emptyIntMap Prelude.True) blocks
      (\z b ->
      case z of {
       (,) mappings isFirst ->
        Monad.bind mDict (\bid ->
          case IntMap.coq_IntMap_lookup bid liveSets of {
           Prelude.Just from ->
            let {
             mappings' = case isFirst of {
                          Prelude.True ->
                           applyMappings maxReg bid mappings Prelude.False
                             (resolvingMoves maxReg allocs Prelude.Nothing
                               ((Prelude.succ) 0)
                               (LiveSets.blockFirstOpId from));
                          Prelude.False -> mappings}}
            in
            Monad.bind mDict (\suxs ->
              let {
               in_from = (Prelude.<=) (Data.List.length suxs) ((Prelude.succ)
                           0)}
              in
              let {
               mappings'' = case Eqtype.eq_op Ssrnat.nat_eqType
                                   (unsafeCoerce (Data.List.length suxs))
                                   (unsafeCoerce 0) of {
                             Prelude.True -> mappings';
                             Prelude.False ->
                              List1.forFold mappings' suxs (\ms s_bid ->
                                case IntMap.coq_IntMap_lookup s_bid liveSets of {
                                 Prelude.Just to ->
                                  let {
                                   key = case in_from of {
                                          Prelude.True -> bid;
                                          Prelude.False -> s_bid}}
                                  in
                                  checkBlockBoundary maxReg allocs key
                                    in_from from to (LiveSets.blockLiveIn to)
                                    ms;
                                 Prelude.Nothing -> ms})}}
              in
              Applicative.pure (Monad.is_applicative mDict) ((,) mappings''
                Prelude.False)) (Blocks.blockSuccessors mDict binfo b);
           Prelude.Nothing ->
            Applicative.pure (Monad.is_applicative mDict) ((,) mappings
              Prelude.False)}) (Blocks.blockId mDict binfo b)}))