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

module LinearScan.Build 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.Datatypes as Datatypes
import qualified LinearScan.IntMap as IntMap
import qualified LinearScan.Interval as Interval
import qualified LinearScan.Lib as Lib
import qualified LinearScan.LiveSets as LiveSets
import qualified LinearScan.Logic as Logic
import qualified LinearScan.Loops as Loops
import qualified LinearScan.Monad as Monad
import qualified LinearScan.NonEmpty0 as NonEmpty0
import qualified LinearScan.Range as Range
import qualified LinearScan.ScanState as ScanState
import qualified LinearScan.Specif as Specif
import qualified LinearScan.UsePos as UsePos
import qualified LinearScan.Yoneda as Yoneda
import qualified LinearScan.Eqtype as Eqtype
import qualified LinearScan.Fintype as Fintype
import qualified LinearScan.Seq as Seq
import qualified LinearScan.Ssrbool as Ssrbool
import qualified LinearScan.Ssrfun as Ssrfun
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 BuildState = IntMap.IntMap Range.SortedRanges

newBuildState :: Prelude.Int -> BuildState
newBuildState n =
  IntMap.emptyIntMap

type PendingRanges = [] Range.BoundedRange

emptyPendingRanges :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
                      IntMap.IntSet -> IntMap.IntMap PendingRanges
emptyPendingRanges maxReg b e liveOuts =
  (Prelude.flip (Prelude.$)) __ (\_ ->
    (Prelude.flip (Prelude.$))
      (Range.emptyBoundedRange ((Prelude.succ) (Ssrnat.double b))
        ((Prelude.succ) (Ssrnat.double e))) (\empty ->
      (Prelude.flip (Prelude.$)) (\xs vid ->
        IntMap.coq_IntMap_insert ((Prelude.+) vid maxReg) ((:[]) empty) xs)
        (\f -> IntMap.coq_IntSet_foldl f IntMap.emptyIntMap liveOuts)))

coq_BoundedRange_leq :: Prelude.Int -> Prelude.Int -> Range.BoundedRange ->
                        Range.BoundedRange -> Prelude.Bool
coq_BoundedRange_leq b e x y =
  let {_evar_0_ = (Prelude.<=) (Range.rbeg x) (Range.rbeg y)} in
  let {_evar_0_0 = (Prelude.<=) (Range.rend x) (Range.rend y)} in
  case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Range.rend x))
         (unsafeCoerce (Range.rend y)) of {
   Prelude.True -> _evar_0_;
   Prelude.False -> _evar_0_0}

compilePendingRanges :: Prelude.Int -> Prelude.Int -> ([] Range.BoundedRange)
                        -> Specif.Coq_sig2 Range.SortedRanges
compilePendingRanges b e ranges =
  let {_evar_0_ = \_ -> []} in
  let {
   _evar_0_0 = \r1 rs iHrs ->
    case rs of {
     [] -> (:) ( r1) [];
     (:) r2 rs2 ->
      (Prelude.flip (Prelude.$)) __ (\_ ->
        let {iHrs0 = iHrs __} in
        let {_evar_0_0 = \_ _ _ _ _ -> Logic.coq_False_rec} in
        let {
         _evar_0_1 = \r2' rs2' ->
          let {_evar_0_1 = \_ -> (:) ( r1) ((:) r2' rs2')} in
          let {
           _evar_0_2 = \_ -> (:)
            (Range.packRange (Range.Build_RangeDesc
              (Prelude.min (Range.rbeg (Range.getRangeDesc r1))
                (Range.rbeg (Range.getRangeDesc r2')))
              (Prelude.max (Range.rend (Range.getRangeDesc r1))
                (Range.rend (Range.getRangeDesc r2')))
              (Lib.sortBy UsePos.upos_le
                ((Prelude.++) (Range.ups (Range.getRangeDesc r1))
                  (Range.ups (Range.getRangeDesc r2')))))) rs2'}
          in
          case Range.range_ltn ( r1) r2' of {
           Prelude.True -> _evar_0_1 __;
           Prelude.False -> _evar_0_2 __}}
        in
        case iHrs0 of {
         [] -> _evar_0_0 __ __ __ __ __;
         (:) x x0 -> _evar_0_1 x x0})}}
  in
  Datatypes.list_rec _evar_0_ (\r1 rs iHrs _ -> _evar_0_0 r1 rs iHrs) ranges
    __

rangesToBoundedRanges :: Prelude.Int -> Prelude.Int -> Range.RangeDesc -> ([]
                         Range.RangeDesc) -> [] Range.BoundedRange
rangesToBoundedRanges b e y ys =
  case ys of {
   [] -> (:[]) ( y);
   (:) z zs -> (:) ( y) (rangesToBoundedRanges b e z zs)}

compressPendingRanges :: Prelude.Int -> Prelude.Int -> PendingRanges ->
                         PendingRanges
compressPendingRanges b e ranges =
  let {_evar_0_ = \r -> (:[]) r} in
  let {
   _evar_0_0 = \r rs ->
    let {
     _evar_0_0 = \_ ->
      let {
       _top_assumption_ = compilePendingRanges b e
                            (Lib.insert (coq_BoundedRange_leq b e) r
                              (Lib.sortBy (coq_BoundedRange_leq b e) ( rs)))}
      in
      let {
       _evar_0_0 = \_ _ ->
        (Prelude.flip (Prelude.$)) __ (\_ ->
          let {_evar_0_0 = \_ -> rs} in  _evar_0_0 __)}
      in
      let {
       _evar_0_1 = \x xs ->
        case _top_assumption_ of {
         [] -> Logic.coq_False_rec;
         (:) y ys -> rangesToBoundedRanges b e y ys}}
      in
      case Lib.insert (coq_BoundedRange_leq b e) r
             (Lib.sortBy (coq_BoundedRange_leq b e) ( rs)) of {
       [] -> _evar_0_0 __ __;
       (:) x x0 -> _evar_0_1 x x0}}
    in
     _evar_0_0 __}
  in
  (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
    (\x ->
    _evar_0_ x)
    (\x x0 ->
    _evar_0_0 x x0)
    ranges

mergeIntoSortedRanges :: Prelude.Int -> Prelude.Int -> (IntMap.IntMap
                         PendingRanges) -> (IntMap.IntMap Range.SortedRanges)
                         -> IntMap.IntMap Range.SortedRanges
mergeIntoSortedRanges b e pmap rmap =
  IntMap.coq_IntMap_mergeWithKey (\_the_1st_wildcard_ brs srs2 ->
    let {
     _top_assumption_ = compilePendingRanges b e
                          (Lib.sortBy (coq_BoundedRange_leq b e) ( brs))}
    in
    Prelude.Just
    (Range.coq_SortedRanges_cat ((Prelude.succ) (Ssrnat.double b))
      _top_assumption_ ((Prelude.succ) (Ssrnat.double e)) srs2))
    (IntMap.coq_IntMap_map (\brs ->
      compilePendingRanges b e (Lib.sortBy (coq_BoundedRange_leq b e) ( brs))))
    (\sr ->
    (Prelude.flip (Prelude.$)) __ (\_ ->
      IntMap.coq_IntMap_map
        (Range.transportSortedRanges ((Prelude.succ) (Ssrnat.double b))
          ((Prelude.succ) (Ssrnat.double e))) sr)) pmap rmap

upos_before_rend :: Range.RangeDesc -> UsePos.UsePos -> Prelude.Bool
upos_before_rend rd upos =
  case Range.ups rd of {
   [] ->
    case UsePos.uvar upos of {
     UsePos.Input -> (Prelude.<=) (UsePos.uloc upos) (Range.rend rd);
     _ -> (Prelude.<=) ((Prelude.succ) (UsePos.uloc upos)) (Range.rend rd)};
   (:) u l ->
    case (Prelude.&&)
           (Prelude.not
             (Eqtype.eq_op UsePos.coq_VarKind_eqType
               (unsafeCoerce (UsePos.uvar upos)) (unsafeCoerce UsePos.Input)))
           (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (UsePos.uloc u))
             (unsafeCoerce (Range.rend rd))) of {
     Prelude.True ->
      (Prelude.<=) ((Prelude.succ) (UsePos.uloc upos)) (UsePos.uloc u);
     Prelude.False -> (Prelude.<=) (UsePos.uloc upos) (UsePos.uloc u)}}

makeNewRange :: Prelude.Int -> Prelude.Int -> Prelude.Int -> UsePos.UsePos ->
                Range.BoundedRange
makeNewRange b pos e upos =
  Range.Build_RangeDesc
    (case UsePos.uvar upos of {
      UsePos.Input -> (Prelude.succ) (Ssrnat.double b);
      _ -> (Prelude.succ) (Ssrnat.double pos)})
    (case UsePos.uvar upos of {
      UsePos.Input -> (Prelude.succ) (Ssrnat.double pos);
      UsePos.Temp -> (Prelude.succ) ((Prelude.succ) (Ssrnat.double pos));
      UsePos.Output -> (Prelude.succ) (Ssrnat.double e)}) ((:) upos [])

makeUsePos :: Prelude.Int -> Prelude.Int -> Blocks.VarInfo -> Specif.Coq_sig2
              UsePos.UsePos
makeUsePos maxReg pos var =
  let {
   upos = UsePos.Build_UsePos ((Prelude.succ) (Ssrnat.double pos))
    (Blocks.regRequired maxReg var) (Blocks.varKind maxReg var)}
  in
  (Prelude.flip (Prelude.$)) __ (\_ -> upos)

handleOutputVar :: Prelude.Int -> Prelude.Int -> Prelude.Int -> Prelude.Int
                   -> (Prelude.Maybe PendingRanges) -> Blocks.VarInfo ->
                   Prelude.Maybe PendingRanges
handleOutputVar maxReg b pos e range var =
  let {_top_assumption_ = makeUsePos maxReg pos var} in
  let {
   _evar_0_ = \range0 ->
    (Prelude.flip (Prelude.$))
      (let {_top_assumption_0 = Prelude.head range0} in
       let {
        _evar_0_ = \_ ->
         let {
          r1 = Range.coq_Range_shift ( _top_assumption_0)
                 (UsePos.uloc _top_assumption_)}
         in
         (Prelude.flip (Prelude.$)) __ (\_ -> r1)}
       in
       let {
        _evar_0_0 = \_ ->
         let {_evar_0_0 = \_ -> _top_assumption_0} in  _evar_0_0 __}
       in
       case (Prelude.<=) ((Prelude.succ) (UsePos.uloc _top_assumption_))
              (Range.head_or_end ( _top_assumption_0)) of {
        Prelude.True -> _evar_0_ __;
        Prelude.False -> _evar_0_0 __}) (\res ->
      let {
       _evar_0_ = \_ ->
        (Prelude.flip (Prelude.$))
          (Range.coq_Range_cons _top_assumption_ ( res)) (\br ->
          let {_evar_0_ = \_the_1st_wildcard_ -> Prelude.Just ((:[]) br)} in
          let {
           _evar_0_0 = \_the_2nd_wildcard_ rs -> Prelude.Just
            (NonEmpty0.coq_NE_from_list br ( rs))}
          in
          (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
            (\x ->
            _evar_0_ x)
            (\x x0 ->
            _evar_0_0 x x0)
            range0)}
      in
      let {
       _evar_0_0 = \_ -> Prelude.Just
        (NonEmpty0.coq_NE_from_list (makeNewRange b pos e _top_assumption_)
          ( range0))}
      in
      case upos_before_rend ( res) _top_assumption_ of {
       Prelude.True -> _evar_0_ __;
       Prelude.False -> _evar_0_0 __})}
  in
  let {
   _evar_0_0 = Prelude.Just ((:[]) (makeNewRange b pos e _top_assumption_))}
  in
  case range of {
   Prelude.Just x -> _evar_0_ x;
   Prelude.Nothing -> _evar_0_0}

handleVar :: Prelude.Int -> Prelude.Int -> Prelude.Int -> Prelude.Int ->
             (Prelude.Maybe PendingRanges) -> Blocks.VarInfo -> Prelude.Maybe
             PendingRanges
handleVar maxReg b pos e range var =
  let {_top_assumption_ = makeUsePos maxReg pos var} in
  let {
   _evar_0_ = \range0 -> Prelude.Just
    (NonEmpty0.coq_NE_from_list (makeNewRange b pos e _top_assumption_)
      ( range0))}
  in
  let {
   _evar_0_0 = Prelude.Just ((:[]) (makeNewRange b pos e _top_assumption_))}
  in
  case range of {
   Prelude.Just x -> _evar_0_ x;
   Prelude.Nothing -> _evar_0_0}

handleVars_combine :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
                      Prelude.Int -> Prelude.Int -> ([] Blocks.VarInfo) ->
                      PendingRanges -> Prelude.Maybe PendingRanges
handleVars_combine maxReg b pos e vid vars c1 =
  (Prelude.flip (Prelude.$)) __ (\_ ->
    (Prelude.flip (Prelude.$)) (compressPendingRanges b e c1) (\c2 ->
      (Prelude.flip (Prelude.$))
        (Data.List.foldl' (handleOutputVar maxReg b pos e) (Prelude.Just c2)
          (Prelude.filter (\k ->
            Eqtype.eq_op UsePos.coq_VarKind_eqType
              (unsafeCoerce (Blocks.varKind maxReg k))
              (unsafeCoerce UsePos.Output)) vars)) (\c3 ->
        (Prelude.flip (Prelude.$))
          (Data.List.foldl' (handleVar maxReg b pos e) c3
            (Prelude.filter (\k ->
              Prelude.not
                (Eqtype.eq_op UsePos.coq_VarKind_eqType
                  (unsafeCoerce (Blocks.varKind maxReg k))
                  (unsafeCoerce UsePos.Output))) vars)) (\c4 -> c4))))

handleVars_onlyRanges :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
                         (IntMap.IntMap PendingRanges) -> IntMap.IntMap
                         PendingRanges
handleVars_onlyRanges b pos e h0 =
  h0

handleVars_onlyVars :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
                       Prelude.Int -> (IntMap.IntMap ([] Blocks.VarInfo)) ->
                       IntMap.IntMap PendingRanges
handleVars_onlyVars maxReg b pos e =
  IntMap.coq_IntMap_foldlWithKey (\m vid vars ->
    (Prelude.flip (Prelude.$))
      (Data.List.foldl' (handleOutputVar maxReg b pos e) Prelude.Nothing
        (Prelude.filter (\k ->
          Eqtype.eq_op UsePos.coq_VarKind_eqType
            (unsafeCoerce (Blocks.varKind maxReg k))
            (unsafeCoerce UsePos.Output)) vars)) (\c2 ->
      (Prelude.flip (Prelude.$))
        (Data.List.foldl' (handleVar maxReg b pos e) c2
          (Prelude.filter (\k ->
            Prelude.not
              (Eqtype.eq_op UsePos.coq_VarKind_eqType
                (unsafeCoerce (Blocks.varKind maxReg k))
                (unsafeCoerce UsePos.Output))) vars)) (\c3 ->
        let {_evar_0_ = \c4 -> IntMap.coq_IntMap_insert vid c4 m} in
        case c3 of {
         Prelude.Just x -> _evar_0_ x;
         Prelude.Nothing -> m}))) IntMap.emptyIntMap

extractVarInfo :: Prelude.Int -> ([] Blocks.VarInfo) -> [] Blocks.VarInfo
extractVarInfo maxReg xs =
  let {_evar_0_ = \x -> (:) x []} in
  let {_evar_0_0 = \x xs0 -> (:) x ( xs0)} in
  (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
    (\x ->
    _evar_0_ x)
    (\x x0 ->
    _evar_0_0 x x0)
    xs

handleVars :: Prelude.Int -> ([] Blocks.VarInfo) -> Prelude.Int ->
              Prelude.Int -> Prelude.Int -> (IntMap.IntMap PendingRanges) ->
              IntMap.IntMap PendingRanges
handleVars maxReg varRefs b pos e ranges =
  let {
   vars = IntMap.coq_IntMap_map (extractVarInfo maxReg)
            (IntMap.coq_IntMap_groupOn (Blocks.nat_of_varId maxReg) varRefs)}
  in
  IntMap.coq_IntMap_mergeWithKey (handleVars_combine maxReg b pos e)
    (handleVars_onlyVars maxReg b pos e) (handleVars_onlyRanges b pos e) vars
    ranges

reduceOp :: Prelude.Int -> (Monad.Monad a4) -> (Blocks.OpInfo a4 a2 a3) ->
            Prelude.Int -> Prelude.Int -> Prelude.Int -> a1 -> a2 ->
            (IntMap.IntMap PendingRanges) -> IntMap.IntMap PendingRanges
reduceOp maxReg mDict oinfo b pos e block op ranges =
  let {refs = Blocks.opRefs maxReg mDict oinfo op} in
  let {
   refs' = case Blocks.opKind maxReg mDict oinfo op of {
            Blocks.IsCall ->
             (Prelude.++)
               (Prelude.filter (\x ->
                 Prelude.not
                   (Ssrbool.in_mem (unsafeCoerce (Blocks.varId maxReg x))
                     (Ssrbool.mem
                       (Seq.seq_predType
                         (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
                           Ssrnat.nat_eqType))
                       (unsafeCoerce
                         (Prelude.map (Blocks.varId maxReg) refs)))))
                 (Fintype.image_mem (Fintype.ordinal_finType maxReg) (\n ->
                   Blocks.Build_VarInfo (Prelude.Left (unsafeCoerce n))
                   UsePos.Temp Prelude.True)
                   (Ssrbool.mem
                     (Seq.seq_predType (Fintype.ordinal_eqType maxReg))
                     (unsafeCoerce (Fintype.ord_enum maxReg))))) refs;
            _ -> refs}}
  in
  handleVars maxReg refs' b pos e ranges

reduceBlock :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 
               a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> Prelude.Int ->
               Blocks.BlockId -> a1 -> Loops.LoopState -> (IntMap.IntMap
               IntMap.IntSet) -> (IntMap.IntMap PendingRanges) ->
               IntMap.IntMap PendingRanges
reduceBlock maxReg mDict binfo oinfo pos bid block loops varUses =
  let {sz = Blocks.blockSize mDict binfo block} in
  let {e = (Prelude.+) pos sz} in
  let {ops = Blocks.allBlockOps mDict binfo block} in
  (Prelude.flip (Prelude.$)) __ (\_ ranges ->
    (Prelude.flip (Prelude.$))
      (case Prelude.not
              (IntMap.coq_IntSet_member bid (Loops.loopEndBlocks loops)) of {
        Prelude.True -> ranges;
        Prelude.False ->
         let {
          f = \acc loopIndex blks ->
           case Prelude.not (IntMap.coq_IntSet_member bid blks) of {
            Prelude.True -> acc;
            Prelude.False ->
             case IntMap.coq_IntMap_lookup loopIndex varUses of {
              Prelude.Just uses -> IntMap.coq_IntSet_union acc uses;
              Prelude.Nothing -> acc}}}
         in
         let {
          uses = IntMap.coq_IntMap_foldlWithKey f IntMap.emptyIntSet
                   (Loops.loopIndices loops)}
         in
         handleVars maxReg
           (Prelude.map (\u -> Blocks.Build_VarInfo (Prelude.Right u)
             UsePos.Input Prelude.False) (IntMap.coq_IntSet_toList uses)) pos
           (Prelude.pred ((Prelude.+) pos sz)) ((Prelude.+) pos sz) ranges})
      ((Prelude.flip (Prelude.$)) __ (\_ ->
        let {_evar_0_ = \x -> x} in
        let {
         _evar_0_0 = \os o iHos ranges0 ->
          (Prelude.flip (Prelude.$)) __ (\_ ->
            (Prelude.flip (Prelude.$)) __ iHos
              (reduceOp maxReg mDict oinfo pos
                ((Prelude.+) pos (Data.List.length os)) e block o ranges0))}
        in
        Seq.last_ind (\_ x -> _evar_0_ x) (\os o iHos _ ranges0 ->
          _evar_0_0 os o iHos ranges0) ops __)))

reduceBlocks :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo 
                a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([] a1) ->
                Loops.LoopState -> (IntMap.IntMap IntMap.IntSet) ->
                (IntMap.IntMap LiveSets.BlockLiveSets) -> Prelude.Int -> a5
reduceBlocks maxReg mDict binfo oinfo blocks loops varUses liveSets pos =
  let {
   _evar_0_ = \pos0 ->
    Monad.pure (Monad.is_applicative mDict) (newBuildState pos0)}
  in
  let {
   _evar_0_0 = \b blocks0 iHbs pos0 ->
    let {sz = Blocks.blockSize mDict binfo b} in
    let {
     _evar_0_0 = \_ ->
      (Prelude.flip (Prelude.$)) __ (\_ ->
        Monad.bind mDict (\bid ->
          let {
           outs = case IntMap.coq_IntMap_lookup bid liveSets of {
                   Prelude.Just ls -> LiveSets.blockLiveOut ls;
                   Prelude.Nothing -> IntMap.emptyIntSet}}
          in
          let {
           ranges = emptyPendingRanges maxReg pos0 ((Prelude.+) pos0 sz) outs}
          in
          let {
           pending = reduceBlock maxReg mDict binfo oinfo pos0 bid b loops
                       varUses ranges}
          in
          Monad.fmap (Monad.is_functor (Monad.is_applicative mDict))
            (mergeIntoSortedRanges pos0 ((Prelude.+) pos0 sz) pending)
            (iHbs ((Prelude.+) pos0 sz)))
          (Yoneda.iso_to
            (Yoneda.coq_Yoneda_lemma
              (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->
            Blocks.blockId mDict binfo b)))}
    in
    let {_evar_0_1 = \_ -> iHbs pos0} in
    case (Prelude.<=) ((Prelude.succ) 0) sz of {
     Prelude.True -> _evar_0_0 __;
     Prelude.False -> _evar_0_1 __}}
  in
  Datatypes.list_rect _evar_0_ _evar_0_0 blocks pos

compileIntervals :: Prelude.Int -> Prelude.Int -> BuildState -> (,)
                    ScanState.FixedIntervalsType
                    (IntMap.IntMap Interval.IntervalDesc)
compileIntervals maxReg pos bs =
  IntMap.coq_IntMap_foldlWithKey (\_top_assumption_ ->
    let {
     _evar_0_ = \regs vars vid rs ->
      let {_evar_0_ = \_ -> (,) regs vars} in
      let {
       _evar_0_0 = \_a_ _l_ ->
        let {
         _evar_0_0 = \_ -> (,)
          (LinearScan.Utils.set_nth maxReg regs ( vid) (Prelude.Just
            (Interval.packInterval (Interval.Build_IntervalDesc vid
              (Range.rbeg
                ( (Prelude.head (NonEmpty0.coq_NE_from_list _a_ _l_))))
              (Range.rend
                ( (Prelude.last (NonEmpty0.coq_NE_from_list _a_ _l_))))
              (NonEmpty0.coq_NE_from_list _a_ _l_))))) vars}
        in
        let {
         _evar_0_1 = \_ ->
          (Prelude.flip (Prelude.$)) ((Prelude.-) vid maxReg) (\vid' -> (,)
            regs
            (IntMap.coq_IntMap_insert vid'
              (Interval.packInterval (Interval.Build_IntervalDesc vid'
                (Range.rbeg
                  ( (Prelude.head (NonEmpty0.coq_NE_from_list _a_ _l_))))
                (Range.rend
                  ( (Prelude.last (NonEmpty0.coq_NE_from_list _a_ _l_))))
                (NonEmpty0.coq_NE_from_list _a_ _l_))) vars))}
        in
        case (Prelude.<=) ((Prelude.succ) vid) maxReg of {
         Prelude.True -> _evar_0_0 __;
         Prelude.False -> _evar_0_1 __}}
      in
      case  (Ssrfun.sig_of_sig2 rs) of {
       [] -> _evar_0_ __;
       (:) x x0 -> _evar_0_0 x x0}}
    in
    case _top_assumption_ of {
     (,) x x0 -> _evar_0_ x x0}) ((,)
    (Data.List.replicate maxReg Prelude.Nothing) IntMap.emptyIntMap) bs

buildIntervals :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo 
                  a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([] 
                  a1) -> Loops.LoopState -> (IntMap.IntMap
                  LiveSets.BlockLiveSets) -> a5
buildIntervals maxReg mDict binfo oinfo blocks loops liveSets =
  let {
   add_unhandled_interval = \ss i ->
    ScanState.packScanState maxReg ScanState.Pending
      (ScanState.Build_ScanStateDesc ((Prelude.succ)
      (ScanState.nextInterval maxReg ( ss)))
      (LinearScan.Utils.snoc (ScanState.nextInterval maxReg ( ss))
        (ScanState.intervals maxReg ( ss)) ( i))
      (ScanState.fixedIntervals maxReg ( ss))
      (Lib.insert (Lib.lebf Prelude.snd) ((,)
        ( (ScanState.nextInterval maxReg ( ss))) (Interval.ibeg ( i)))
        (Prelude.map Prelude.id (ScanState.unhandled maxReg ( ss))))
      (Prelude.map Prelude.id (ScanState.active maxReg ( ss)))
      (Prelude.map Prelude.id (ScanState.inactive maxReg ( ss)))
      (Prelude.map Prelude.id (ScanState.handled maxReg ( ss))))}
  in
  case blocks of {
   [] ->
    Monad.pure (Monad.is_applicative mDict) (Prelude.Right
      (ScanState.packScanState maxReg ScanState.InUse
        (ScanState.Build_ScanStateDesc 0 []
        (Data.List.replicate maxReg Prelude.Nothing) [] [] [] [])));
   (:) b bs ->
    Monad.bind mDict (\varUses ->
      Monad.bind mDict (\reduced ->
        case compileIntervals maxReg 0 reduced of {
         (,) regs vars ->
          let {
           s2 = ScanState.packScanState maxReg ScanState.Pending
                  (ScanState.Build_ScanStateDesc
                  (ScanState.nextInterval maxReg
                    (ScanState.Build_ScanStateDesc 0 []
                    (Data.List.replicate maxReg Prelude.Nothing) [] [] []
                    []))
                  (ScanState.intervals maxReg (ScanState.Build_ScanStateDesc
                    0 [] (Data.List.replicate maxReg Prelude.Nothing) [] []
                    [] [])) regs
                  (ScanState.unhandled maxReg (ScanState.Build_ScanStateDesc
                    0 [] (Data.List.replicate maxReg Prelude.Nothing) [] []
                    [] []))
                  (ScanState.active maxReg (ScanState.Build_ScanStateDesc 0
                    [] (Data.List.replicate maxReg Prelude.Nothing) [] [] []
                    []))
                  (ScanState.inactive maxReg (ScanState.Build_ScanStateDesc 0
                    [] (Data.List.replicate maxReg Prelude.Nothing) [] [] []
                    []))
                  (ScanState.handled maxReg (ScanState.Build_ScanStateDesc 0
                    [] (Data.List.replicate maxReg Prelude.Nothing) [] [] []
                    [])))}
          in
          let {s3 = IntMap.coq_IntMap_foldl add_unhandled_interval s2 vars}
          in
          Monad.pure (Monad.is_applicative mDict) (Prelude.Right
            (ScanState.packScanState maxReg ScanState.InUse ( s3)))})
        (reduceBlocks maxReg mDict binfo oinfo ((:) b bs) loops varUses
          liveSets 0))
      (Loops.computeVarReferences maxReg mDict binfo oinfo ((:) b bs) loops)}