{-# OPTIONS_GHC -cpp -fglasgow-exts #-}
{- 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.Morph as Morph
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.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



--unsafeCoerce :: a -> b
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base as GHC.Base
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
import qualified LinearScan.IOExts as IOExts
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 -> (Blocks.OpInfo a4 a2 a3) -> Prelude.Int ->
            Prelude.Int -> Prelude.Int -> a1 -> a2 -> (IntMap.IntMap
            PendingRanges) -> IntMap.IntMap PendingRanges
reduceOp maxReg oinfo b pos e block op ranges =
  let {refs = Blocks.opRefs maxReg oinfo op} in
  let {
   refs' = case Blocks.opKind maxReg oinfo op of {
            Blocks.IsCall ->
             (Prelude.++)
               (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 -> (Blocks.BlockInfo 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 binfo oinfo pos bid block loops varUses =
  let {sz = Blocks.blockSize binfo block} in
  let {e = (Prelude.+) pos sz} in
  let {ops = Blocks.allBlockOps binfo block} in
  (Prelude.flip (Prelude.$)) __ (\_ ->
    (Prelude.flip (Prelude.$)) __ (\_ ->
      let {_evar_0_ = \h0 -> h0} in
      let {
       _evar_0_0 = \os o iHos ranges ->
        (Prelude.flip (Prelude.$)) __ (\_ ->
          (Prelude.flip (Prelude.$)) __ iHos
            (reduceOp maxReg oinfo pos
              ((Prelude.+) pos (Data.List.length os)) e block o ranges))}
      in
      Seq.last_ind (\_ h0 -> _evar_0_ h0) (\os o iHos _ ranges ->
        _evar_0_0 os o iHos ranges) ops __))

reduceBlocks :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->
                (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> Loops.LoopState ->
                (IntMap.IntMap IntMap.IntSet) -> (IntMap.IntMap
                LiveSets.BlockLiveSets) -> Prelude.Int -> BuildState
reduceBlocks maxReg binfo oinfo blocks loops varUses liveSets pos =
  let {_evar_0_ = \pos0 -> newBuildState pos0} in
  let {
   _evar_0_0 = \b blocks0 iHbs pos0 ->
    (Prelude.flip (Prelude.$)) (Blocks.blockId binfo b) (\bid ->
      (Prelude.flip (Prelude.$))
        (case IntMap.coq_IntMap_lookup bid liveSets of {
          Prelude.Just ls -> LiveSets.blockLiveOut ls;
          Prelude.Nothing -> IntMap.emptyIntSet}) (\outs ->
        let {sz = Blocks.blockSize binfo b} in
        let {
         _evar_0_0 = \_ ->
          (Prelude.flip (Prelude.$)) __ (\_ ->
            (Prelude.flip (Prelude.$))
              (reduceBlock maxReg binfo oinfo pos0 bid b loops varUses
                (emptyPendingRanges maxReg pos0 ((Prelude.+) pos0 sz) outs))
              (\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 = \_ -> (,)
          (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 -> (Blocks.BlockInfo a1 a2 a3 a4) ->
                  (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> Loops.LoopState ->
                  (IntMap.IntMap LiveSets.BlockLiveSets) -> Prelude.Either
                  Morph.SSError ScanState.ScanStateSig
buildIntervals maxReg 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 {
   [] -> Prelude.Right
    (ScanState.packScanState maxReg ScanState.InUse
      (ScanState.Build_ScanStateDesc 0 []
      (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []));
   (:) b bs ->
    let {
     varUses = Loops.computeVarReferences maxReg binfo oinfo ((:) b bs) loops}
    in
    let {
     reduced = reduceBlocks maxReg 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
                [] (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
      Prelude.Right (ScanState.packScanState maxReg ScanState.InUse ( s3))}}