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

module LinearScan.Build 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.Blocks as Blocks
import qualified LinearScan.Datatypes as Datatypes
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.Logic as Logic
import qualified LinearScan.Loops as Loops
import qualified LinearScan.Monad as Monad
import qualified LinearScan.NonEmpty as NonEmpty
import qualified LinearScan.Prelude0 as Prelude0
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.Vector0 as Vector0
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 ->
                      IntSet.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 -> IntSet.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')))
              (List1.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
                            (List1.insert (coq_BoundedRange_leq b e) r
                              (List1.sortBy (coq_BoundedRange_leq b e)
                                (Prelude.id 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 List1.insert (coq_BoundedRange_leq b e) r
             (List1.sortBy (coq_BoundedRange_leq b e) (Prelude.id 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
                          (List1.sortBy (coq_BoundedRange_leq b e)
                            (Prelude.id 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
        (List1.sortBy (coq_BoundedRange_leq b e) (Prelude.id 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 {
   [] -> (Prelude.<=) ((Prelude.succ) (UsePos.uloc upos)) (Range.rend rd);
   (:) u l -> (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 (Prelude.||)
            (Eqtype.eq_op UsePos.coq_VarKind_eqType
              (unsafeCoerce (UsePos.uvar upos)) (unsafeCoerce UsePos.Input))
            (Eqtype.eq_op UsePos.coq_VarKind_eqType
              (unsafeCoerce (UsePos.uvar upos))
              (unsafeCoerce UsePos.InputOutput)) of {
      Prelude.True -> (Prelude.succ) (Ssrnat.double b);
      Prelude.False -> (Prelude.succ) ((Prelude.succ) (Ssrnat.double pos))})
    (case UsePos.uvar upos of {
      UsePos.Input -> (Prelude.succ) ((Prelude.succ) (Ssrnat.double pos));
      UsePos.Temp -> (Prelude.succ) ((Prelude.succ) ((Prelude.succ)
       (Ssrnat.double pos)));
      _ -> (Prelude.succ) (Ssrnat.double e)}) ((:) upos [])

makeUsePos :: Prelude.Int -> Prelude.Int -> Blocks.VarInfo -> UsePos.UsePos
makeUsePos maxReg pos var =
  UsePos.Build_UsePos
    (case Blocks.varKind maxReg var of {
      UsePos.Input -> (Prelude.succ) (Ssrnat.double pos);
      _ -> (Prelude.succ) ((Prelude.succ) (Ssrnat.double pos))})
    (Blocks.regRequired maxReg var) (Blocks.varKind maxReg var)

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 {
          _evar_0_ = (,) Prelude.True
           (let {
             r1 = Range.coq_Range_shift ( _top_assumption_0)
                    (UsePos.uloc _top_assumption_)}
            in
            (Prelude.flip (Prelude.$)) __ (\_ -> r1))}
         in
         let {
          _evar_0_0 = \_top_assumption_1 ->
           let {
            _evar_0_0 = \loc req kind us ->
             let {
              _evar_0_0 = (,) Prelude.False
               ((Prelude.flip (Prelude.$)) __ (\_ ->
                 let {
                  nR = makeNewRange b pos ((Prelude.succ) pos)
                         _top_assumption_}
                 in
                  nR))}
             in
             let {
              _evar_0_1 = (,) Prelude.True
               (let {
                 r1 = Range.coq_Range_shift ( _top_assumption_0)
                        (UsePos.uloc _top_assumption_)}
                in
                (Prelude.flip (Prelude.$)) __ (\_ -> r1))}
             in
             case Eqtype.eq_op UsePos.coq_VarKind_eqType kind
                    (unsafeCoerce UsePos.Output) of {
              Prelude.True -> _evar_0_0;
              Prelude.False -> _evar_0_1}}
           in
           case _top_assumption_1 of {
            UsePos.Build_UsePos x x0 x1 -> unsafeCoerce _evar_0_0 x x0 x1}}
         in
         case Range.ups ( _top_assumption_0) of {
          [] -> _evar_0_;
          (:) x x0 -> _evar_0_0 x x0}}
       in
       let {
        _evar_0_0 = \_ -> (,) Prelude.True
         (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_ = \replaceFirst _top_assumption_0 ->
        let {
         _evar_0_ = \_ ->
          let {
           _evar_0_ = (Prelude.flip (Prelude.$))
                        (Range.coq_Range_cons _top_assumption_
                          ( _top_assumption_0)) (\br ->
                        let {
                         _evar_0_ = \_the_1st_wildcard_ -> Prelude.Just
                          ((:[]) br)}
                        in
                        let {
                         _evar_0_0 = \_the_2nd_wildcard_ rs -> Prelude.Just
                          (NonEmpty.coq_NE_from_list br (Prelude.id 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.flip (Prelude.$)) _top_assumption_0 (\br ->
                         Prelude.Just
                         (NonEmpty.coq_NE_from_list br (Prelude.id range0)))}
          in
          case replaceFirst of {
           Prelude.True -> _evar_0_;
           Prelude.False -> _evar_0_0}}
        in
        let {
         _evar_0_0 = \_ -> Prelude.Just
          (NonEmpty.coq_NE_from_list (makeNewRange b pos e _top_assumption_)
            (Prelude.id range0))}
        in
        case upos_before_rend ( _top_assumption_0) _top_assumption_ of {
         Prelude.True -> _evar_0_ __;
         Prelude.False -> _evar_0_0 __}}
      in
      case res of {
       (,) x x0 -> _evar_0_ x x0})}
  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
    (NonEmpty.coq_NE_from_list (makeNewRange b pos e _top_assumption_)
      (Prelude.id 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

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 Prelude.id
            (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 ->
             let {
              regsNeeded = Seq.count (\r ->
                             case Blocks.varId maxReg r of {
                              Prelude.Left p -> Prelude.False;
                              Prelude.Right v -> Prelude.True}) refs}
             in
             (Prelude.++)
               (Seq.drop regsNeeded
                 (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
               IntSet.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
              (IntSet.coq_IntSet_member bid (Loops.loopEndBlocks loops)) of {
        Prelude.True -> ranges;
        Prelude.False ->
         let {
          f = \acc loopIndex blks ->
           case Prelude.not (IntSet.coq_IntSet_member bid blks) of {
            Prelude.True -> acc;
            Prelude.False ->
             case IntMap.coq_IntMap_lookup loopIndex varUses of {
              Prelude.Just uses -> IntSet.coq_IntSet_union acc uses;
              Prelude.Nothing -> acc}}}
         in
         let {
          uses = IntMap.coq_IntMap_foldlWithKey f IntSet.emptyIntSet
                   (Loops.loopIndices loops)}
         in
         handleVars maxReg
           (Prelude.map (\u -> Blocks.Build_VarInfo (Prelude.Right u)
             UsePos.Input Prelude.False) (IntSet.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 IntSet.IntSet) ->
                (IntMap.IntMap LiveSets.BlockLiveSets) -> Prelude.Int ->
                BuildState
reduceBlocks maxReg mDict binfo oinfo blocks loops varUses liveSets pos =
  let {_evar_0_ = \pos0 -> 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.$)) __ (\_ ->
        (Prelude.flip (Prelude.$)) (Blocks.blockId mDict binfo b) (\bid ->
          (Prelude.flip (Prelude.$))
            (case IntMap.coq_IntMap_lookup bid liveSets of {
              Prelude.Just ls -> LiveSets.blockLiveOut ls;
              Prelude.Nothing -> IntSet.emptyIntSet}) (\outs ->
            (Prelude.flip (Prelude.$))
              (emptyPendingRanges maxReg pos0 ((Prelude.+) pos0 sz) outs)
              (\ranges ->
              (Prelude.flip (Prelude.$))
                (reduceBlock maxReg mDict binfo oinfo pos0 bid b loops
                  varUses ranges) (\pending ->
                mergeIntoSortedRanges pos0 ((Prelude.+) pos0 sz) pending
                  (iHbs ((Prelude.+) pos0 sz)))))))}
    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_rec _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 = \_ -> (,)
          (Vector0.vreplace maxReg regs ( vid) (Prelude.Just
            (Interval.packInterval (Interval.Build_IntervalDesc vid
              (Range.rbeg
                ( (Prelude.head (NonEmpty.coq_NE_from_list _a_ _l_))))
              (Range.rend
                ( (Prelude.last (NonEmpty.coq_NE_from_list _a_ _l_))))
              (NonEmpty.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 (NonEmpty.coq_NE_from_list _a_ _l_))))
                (Range.rend
                  ( (Prelude.last (NonEmpty.coq_NE_from_list _a_ _l_))))
                (NonEmpty.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}) ((,) (Vector0.vconst 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) -> ScanState.ScanStateSig
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)))
      (unsafeCoerce
        (Vector0.vshiftin (ScanState.nextInterval maxReg ( ss))
          (ScanState.intervals maxReg ( ss)) ( i)))
      (ScanState.fixedIntervals maxReg ( ss))
      (List1.insert (Prelude0.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 {
   [] ->
    ScanState.packScanState maxReg ScanState.InUse
      (ScanState.Build_ScanStateDesc 0 (unsafeCoerce Vector0.vnil)
      (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []);
   (:) b bs ->
    let {
     varUses = Loops.computeVarReferences maxReg mDict binfo oinfo ((:) b bs)
                 loops}
    in
    let {
     reduced = reduceBlocks maxReg mDict binfo oinfo ((:) b bs) loops varUses
                 liveSets 0}
    in
    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
                (unsafeCoerce Vector0.vnil)
                (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []))
              (ScanState.intervals maxReg (ScanState.Build_ScanStateDesc 0
                (unsafeCoerce Vector0.vnil)
                (Vector0.vconst maxReg Prelude.Nothing) [] [] [] [])) regs
              (ScanState.unhandled maxReg (ScanState.Build_ScanStateDesc 0
                (unsafeCoerce Vector0.vnil)
                (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []))
              (ScanState.active maxReg (ScanState.Build_ScanStateDesc 0
                (unsafeCoerce Vector0.vnil)
                (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []))
              (ScanState.inactive maxReg (ScanState.Build_ScanStateDesc 0
                (unsafeCoerce Vector0.vnil)
                (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []))
              (ScanState.handled maxReg (ScanState.Build_ScanStateDesc 0
                (unsafeCoerce Vector0.vnil)
                (Vector0.vconst maxReg Prelude.Nothing) [] [] [] [])))}
      in
      let {s3 = IntMap.coq_IntMap_foldl add_unhandled_interval s2 vars} in
      ScanState.packScanState maxReg ScanState.InUse ( s3)}}