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

module LinearScan.Allocate 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.Context as Context
import qualified LinearScan.Cursor as Cursor
import qualified LinearScan.Interval as Interval
import qualified LinearScan.Lib as Lib
import qualified LinearScan.Morph as Morph
import qualified LinearScan.Prelude0 as Prelude0
import qualified LinearScan.ScanState as ScanState
import qualified LinearScan.Specif as Specif
import qualified LinearScan.Spill as Spill
import qualified LinearScan.Split as Split
import qualified LinearScan.Trace as Trace
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.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

intersectsWithFixedInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
                               PhysReg -> Morph.SState () ()
                               (Prelude.Maybe Prelude0.Coq_oddnum)
intersectsWithFixedInterval maxReg pre reg =
  Cursor.withCursor maxReg pre (\sd _ ->
    let {int = Cursor.curIntDetails maxReg sd} in
    Context.ipure
      (case LinearScan.Utils.nth maxReg (ScanState.fixedIntervals maxReg sd)
              reg of {
        Prelude.Just i -> Interval.intervalIntersectionPoint ( int) ( i);
        Prelude.Nothing -> Prelude.Nothing}))

updateRegisterPos :: Prelude.Int -> ([] (Prelude.Maybe Prelude0.Coq_oddnum))
                     -> Prelude.Int -> (Prelude.Maybe Prelude0.Coq_oddnum) ->
                     [] (Prelude.Maybe Prelude0.Coq_oddnum)
updateRegisterPos n v r p =
  case p of {
   Prelude.Just x ->
    LinearScan.Utils.set_nth n v r (Prelude.Just
      (case LinearScan.Utils.nth n v r of {
        Prelude.Just n0 ->
         case (Prelude.<=) ((Prelude.succ) ( n0)) ( x) of {
          Prelude.True -> n0;
          Prelude.False -> x};
        Prelude.Nothing -> x}));
   Prelude.Nothing -> v}

convert_oddnum :: (Prelude.Maybe Prelude0.Coq_oddnum) -> Prelude.Maybe
                  Prelude.Int
convert_oddnum x =
  case x of {
   Prelude.Just x0 -> Prelude.Just ( x0);
   Prelude.Nothing -> Prelude.Nothing}

findEligibleRegister :: Prelude.Int -> ScanState.ScanStateDesc ->
                        Interval.IntervalDesc -> ([]
                        (Prelude.Maybe Prelude0.Coq_oddnum)) -> (,) PhysReg
                        (Prelude.Maybe Prelude0.Coq_oddnum)
findEligibleRegister maxReg sd d xs =
  case (LinearScan.Utils.vfoldl'_with_index) maxReg (\reg acc mint ->
         case acc of {
          (,) fup fai ->
           case mint of {
            Prelude.Just int ->
             let {ip = Interval.intervalIntersectionPoint ( int) d} in
             let {
              intersects = case ip of {
                            Prelude.Just o -> Prelude.True;
                            Prelude.Nothing -> Prelude.False}}
             in
             (,)
             (updateRegisterPos maxReg fup reg
               (Interval.intervalIntersectionPoint ( int) d))
             (LinearScan.Utils.set_nth maxReg fai reg intersects);
            Prelude.Nothing -> acc}}) ((,) xs
         (Data.List.replicate maxReg Prelude.False))
         (ScanState.fixedIntervals maxReg sd) of {
   (,) xs0 fixedAndIntersects ->
    ScanState.registerWithHighestPos maxReg fixedAndIntersects xs0}

tryAllocateFreeReg :: Prelude.Int -> ScanState.ScanStateDesc -> Morph.SState
                      () () (Prelude.Maybe (Morph.SState () () PhysReg))
tryAllocateFreeReg maxReg pre =
  Cursor.withCursor maxReg pre (\sd _ ->
    let {pos = Cursor.curPosition maxReg sd} in
    let {
     go = \f v p ->
      case p of {
       (,) i r -> updateRegisterPos maxReg v r (f i)}}
    in
    let {
     freeUntilPos' = Data.List.foldl' (go (\x -> Prelude.Just Prelude0.odd1))
                       (Data.List.replicate maxReg Prelude.Nothing)
                       (ScanState.active maxReg sd)}
    in
    let {
     intersectingIntervals = Prelude.filter (\x ->
                               Interval.intervalsIntersect
                                 ( (Cursor.curIntDetails maxReg sd))
                                 (
                                   (LinearScan.Utils.nth
                                     (ScanState.nextInterval maxReg sd)
                                     (ScanState.intervals maxReg sd)
                                     (Prelude.fst x))))
                               (ScanState.inactive maxReg sd)}
    in
    let {
     freeUntilPos'' = Data.List.foldl'
                        (go (\i ->
                          Interval.intervalIntersectionPoint
                            (
                              (LinearScan.Utils.nth
                                (ScanState.nextInterval maxReg sd)
                                (ScanState.intervals maxReg sd) i))
                            ( (Cursor.curIntDetails maxReg sd))))
                        freeUntilPos' intersectingIntervals}
    in
    case findEligibleRegister maxReg sd ( (Cursor.curIntDetails maxReg sd))
           freeUntilPos'' of {
     (,) reg mres ->
      let {
       success = Context.ibind (\x -> Context.ipure reg)
                   (Morph.moveUnhandledToActive maxReg pre reg)}
      in
      let {cid = Cursor.curId maxReg sd} in
      Context.context (Trace.ETryAllocateFreeReg ( reg) (convert_oddnum mres)
        ( (Prelude.fst cid)))
        (Context.ipure
          (case mres of {
            Prelude.Just n ->
             case (Prelude.<=) ( n) pos of {
              Prelude.True -> Prelude.Nothing;
              Prelude.False -> Prelude.Just
               (case (Prelude.<=) ((Prelude.succ)
                       (Interval.intervalEnd
                         ( (Cursor.curIntDetails maxReg sd)))) ( n) of {
                 Prelude.True -> success;
                 Prelude.False ->
                  Context.ibind (\x -> success)
                    (Split.splitCurrentInterval maxReg pre (Split.BeforePos
                      n))})};
            Prelude.Nothing -> Prelude.Just success}))})

allocateBlockedReg :: Prelude.Int -> ScanState.ScanStateDesc -> Morph.SState
                      () () (Prelude.Maybe PhysReg)
allocateBlockedReg maxReg pre =
  Cursor.withCursor maxReg pre (\sd _ ->
    let {start = Interval.intervalStart ( (Cursor.curIntDetails maxReg sd))}
    in
    let {pos = Cursor.curPosition maxReg sd} in
    let {
     go = \n v p ->
      case p of {
       (,) int r ->
        let {
         atPos = \u ->
          (Prelude.&&)
            (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos)
              (unsafeCoerce (UsePos.uloc u))) (UsePos.regReq u)}
        in
        let {
         pos' = case Interval.findIntervalUsePos ( int) atPos of {
                 Prelude.Just s -> Prelude.Just Prelude0.odd1;
                 Prelude.Nothing -> Interval.nextUseAfter ( int) start}}
        in
        updateRegisterPos n v r pos'}}
    in
    let {
     resolve = \xs ->
      Prelude.map (\i -> (,)
        (Interval.packInterval
          (
            (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)
              (ScanState.intervals maxReg sd) (Prelude.fst i))))
        (Prelude.snd i)) xs}
    in
    let {
     nextUsePos' = Data.List.foldl' (go maxReg)
                     (Data.List.replicate maxReg Prelude.Nothing)
                     (resolve (ScanState.active maxReg sd))}
    in
    let {
     intersectingIntervals = Prelude.filter (\x ->
                               Interval.intervalsIntersect
                                 ( (Cursor.curIntDetails maxReg sd))
                                 ( (Prelude.fst x)))
                               (resolve (ScanState.inactive maxReg sd))}
    in
    let {
     nextUsePos'' = Data.List.foldl' (go maxReg) nextUsePos'
                      intersectingIntervals}
    in
    case findEligibleRegister maxReg sd ( (Cursor.curIntDetails maxReg sd))
           nextUsePos'' of {
     (,) reg mres ->
      let {cid = Cursor.curId maxReg sd} in
      Context.context (Trace.EAllocateBlockedReg ( reg) (convert_oddnum mres)
        ( (Prelude.fst cid)))
        (case case mres of {
               Prelude.Just n ->
                (Prelude.<=) ((Prelude.succ) ( n))
                  (case Interval.lookupUsePos
                          ( (Cursor.curIntDetails maxReg sd)) (\u ->
                          (Prelude.<=) pos (UsePos.uloc u)) of {
                    Prelude.Just s ->  s;
                    Prelude.Nothing ->
                     Interval.intervalEnd ( (Cursor.curIntDetails maxReg sd))});
               Prelude.Nothing -> Prelude.False} of {
          Prelude.True ->
           Context.ibind (\x -> Context.ipure Prelude.Nothing)
             (Spill.spillCurrentInterval maxReg pre);
          Prelude.False ->
           Context.ibind (\x ->
             Context.ibind (\x0 ->
               Context.ibind (\mloc ->
                 Context.ibind (\x1 ->
                   Context.ibind (\x2 -> Context.ipure (Prelude.Just reg))
                     (Morph.moveUnhandledToActive maxReg pre reg))
                   (case mloc of {
                     Prelude.Just n ->
                      Context.context (Trace.EIntersectsWithFixedInterval
                        ( n) ( reg))
                        (Split.splitCurrentInterval maxReg pre
                          (Split.BeforePos n));
                     Prelude.Nothing -> Context.ipure ()}))
                 (intersectsWithFixedInterval maxReg pre reg))
               (Split.splitActiveIntervalForReg maxReg pre reg pos))
             (Split.splitAnyInactiveIntervalForReg maxReg pre reg pos)})})

morphlen_transport :: Prelude.Int -> ScanState.ScanStateDesc ->
                      ScanState.ScanStateDesc -> ScanState.IntervalId ->
                      ScanState.IntervalId
morphlen_transport maxReg b b' = GHC.Base.id
  

mt_fst :: Prelude.Int -> ScanState.ScanStateDesc -> ScanState.ScanStateDesc
          -> ((,) ScanState.IntervalId PhysReg) -> (,) ScanState.IntervalId
          PhysReg
mt_fst maxReg b b' x =
  case x of {
   (,) xid reg -> (,) (morphlen_transport maxReg b b' xid) reg}

type Coq_int_reg_seq = [] ((,) ScanState.IntervalId PhysReg)

type Coq_intermediate_result = Specif.Coq_sig2 ScanState.ScanStateDesc

goActive :: Prelude.Int -> Prelude.Int -> ScanState.ScanStateDesc ->
            ScanState.ScanStateDesc -> ((,) ScanState.IntervalId PhysReg) ->
            Coq_int_reg_seq -> Coq_intermediate_result
goActive maxReg pos sd z x xs =
  case (Prelude.<=) ((Prelude.succ)
         (Interval.intervalEnd
           (
             (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)
               (ScanState.intervals maxReg z) (Prelude.fst x))))) pos of {
   Prelude.True ->
    Morph.moveActiveToHandled maxReg z Prelude.False (unsafeCoerce x);
   Prelude.False ->
    case Prelude.not
           (Interval.posWithinInterval
             (
               (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)
                 (ScanState.intervals maxReg z) (Prelude.fst x))) pos) of {
     Prelude.True -> Morph.moveActiveToInactive maxReg z (unsafeCoerce x);
     Prelude.False -> z}}

checkActiveIntervals :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int
                        -> Morph.SState () () ()
checkActiveIntervals maxReg pre pos =
  Morph.withScanStatePO maxReg pre (\sd _ ->
    let {
     res = Lib.dep_foldl_inv (\s ->
             Eqtype.prod_eqType
               (Fintype.ordinal_eqType (ScanState.nextInterval maxReg s))
               (Fintype.ordinal_eqType maxReg)) sd
             (unsafeCoerce (ScanState.active maxReg sd))
             (Data.List.length (ScanState.active maxReg sd))
             (unsafeCoerce (ScanState.active maxReg))
             (unsafeCoerce (\x x0 _ -> mt_fst maxReg x x0))
             (unsafeCoerce (\x _ x0 x1 _ -> goActive maxReg pos sd x x0 x1))}
    in
    Context.iput (Morph.Build_SSInfo res __))

moveInactiveToActive' :: Prelude.Int -> ScanState.ScanStateDesc -> ((,)
                         ScanState.IntervalId PhysReg) -> Coq_int_reg_seq ->
                         ([] Trace.SSTrace) -> Prelude.Either
                         ([] Trace.SSTrace)
                         (Specif.Coq_sig2 ScanState.ScanStateDesc)
moveInactiveToActive' maxReg z x xs e =
  let {
   filtered_var = Prelude.not
                    (Ssrbool.in_mem (Prelude.snd (unsafeCoerce x))
                      (Ssrbool.mem
                        (Seq.seq_predType (Fintype.ordinal_eqType maxReg))
                        (unsafeCoerce
                          (Prelude.map (\i -> Prelude.snd i)
                            (ScanState.active maxReg z)))))}
  in
  case filtered_var of {
   Prelude.True ->
    let {
     filtered_var0 = Morph.moveInactiveToActive maxReg z (unsafeCoerce x)}
    in
    Prelude.Right filtered_var0;
   Prelude.False -> Prelude.Left ((:) (Trace.ERegisterAssignmentsOverlap
    ( (Prelude.snd x))) e)}

goInactive :: Prelude.Int -> Prelude.Int -> ScanState.ScanStateDesc -> ([]
              Trace.SSTrace) -> ScanState.ScanStateDesc -> ((,)
              ScanState.IntervalId PhysReg) -> Coq_int_reg_seq ->
              Prelude.Either ([] Trace.SSTrace) Coq_intermediate_result
goInactive maxReg pos sd e z x xs =
  let {f = \sd' -> Prelude.Right sd'} in
  case (Prelude.<=) ((Prelude.succ)
         (Interval.intervalEnd
           (
             (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)
               (ScanState.intervals maxReg z) (Prelude.fst x))))) pos of {
   Prelude.True ->
    let {
     filtered_var = Morph.moveInactiveToHandled maxReg z Prelude.False
                      (unsafeCoerce x)}
    in
    f filtered_var;
   Prelude.False ->
    case Interval.posWithinInterval
           (
             (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)
               (ScanState.intervals maxReg z) (Prelude.fst x))) pos of {
     Prelude.True ->
      let {filtered_var = moveInactiveToActive' maxReg z x xs e} in
      case filtered_var of {
       Prelude.Left err -> Prelude.Left err;
       Prelude.Right s -> f s};
     Prelude.False -> f z}}

checkInactiveIntervals :: Prelude.Int -> ScanState.ScanStateDesc ->
                          Prelude.Int -> Morph.SState () () ()
checkInactiveIntervals maxReg pre pos =
  Morph.withScanStatePO maxReg pre (\sd _ ->
    Context.ibind (\e ->
      let {
       eres = Lib.dep_foldl_invE (\s ->
                Eqtype.prod_eqType
                  (Fintype.ordinal_eqType (ScanState.nextInterval maxReg s))
                  (Fintype.ordinal_eqType maxReg)) sd
                (unsafeCoerce (ScanState.inactive maxReg sd))
                (Data.List.length (ScanState.inactive maxReg sd))
                (unsafeCoerce (ScanState.inactive maxReg))
                (unsafeCoerce (\x x0 _ -> mt_fst maxReg x x0))
                (unsafeCoerce (\x _ x0 x1 _ ->
                  goInactive maxReg pos sd e x x0 x1))}
      in
      case eres of {
       Prelude.Left err -> Morph.error_ maxReg sd err;
       Prelude.Right s -> Context.iput (Morph.Build_SSInfo s __)})
      Context.iask)

handleInterval :: Prelude.Int -> ScanState.ScanStateDesc -> Morph.SState 
                  () () (Prelude.Maybe PhysReg)
handleInterval maxReg pre =
  Cursor.withCursor maxReg pre (\sd _ ->
    let {position = Cursor.curPosition maxReg sd} in
    case Interval.firstUsePos
           (Interval.getIntervalDesc ( (Cursor.curIntDetails maxReg sd))) of {
     Prelude.Just u ->
      Context.ibind (\x ->
        Context.ibind (\x0 ->
          Context.ibind (\mres ->
            case mres of {
             Prelude.Just x1 -> Context.imap (\x2 -> Prelude.Just x2) x1;
             Prelude.Nothing -> allocateBlockedReg maxReg pre})
            (tryAllocateFreeReg maxReg pre))
          (Morph.liftLen maxReg pre (\sd0 ->
            checkInactiveIntervals maxReg sd0 position)))
        (Morph.liftLen maxReg pre (\sd0 ->
          checkActiveIntervals maxReg sd0 position));
     Prelude.Nothing ->
      Context.ibind (\x -> Context.ipure Prelude.Nothing)
        (Morph.moveUnhandledToHandled maxReg pre)})

finalizeScanState :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int ->
                     ScanState.ScanStateDesc
finalizeScanState maxReg sd finalPos =
  case Context.ibind (\x -> checkInactiveIntervals maxReg sd finalPos)
         (checkActiveIntervals maxReg sd finalPos) [] (Morph.Build_SSInfo sd
         __) of {
   Prelude.Left l -> sd;
   Prelude.Right p ->
    case p of {
     (,) u ss -> Morph.thisDesc maxReg sd ss}}

walkIntervals :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int ->
                 Prelude.Either
                 ((,) ([] Trace.SSTrace) ScanState.ScanStateSig)
                 ScanState.ScanStateSig
walkIntervals maxReg sd positions =
  (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
    (\_ -> Prelude.Left ((,) ((:) Trace.EFuelExhausted [])
    (ScanState.packScanState maxReg ScanState.InUse sd)))
    (\n ->
    let {
     go = let {
           go count0 ss =
             (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
               (\_ -> Prelude.Right (Morph.Build_SSInfo
               (Morph.thisDesc maxReg sd ss)
               __))
               (\cnt ->
               case handleInterval maxReg sd [] ss of {
                Prelude.Left err -> Prelude.Left ((,) err
                 (ScanState.packScanState maxReg ScanState.InUse
                   (Morph.thisDesc maxReg sd ss)));
                Prelude.Right p ->
                 case p of {
                  (,) o ss' ->
                   case Morph.strengthenHasLen maxReg sd
                          (Morph.thisDesc maxReg sd ss') of {
                    Prelude.Just _ ->
                     go cnt (Morph.Build_SSInfo
                       (Morph.thisDesc maxReg sd ss') __);
                    Prelude.Nothing ->
                     (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
                       (\_ -> Prelude.Right
                       ss')
                       (\n0 -> Prelude.Left ((,) ((:)
                       Trace.EUnexpectedNoMoreUnhandled [])
                       (ScanState.packScanState maxReg ScanState.InUse
                         (Morph.thisDesc maxReg sd ss'))))
                       cnt}}})
               count0}
          in go}
    in
    case LinearScan.Utils.uncons (ScanState.unhandled maxReg sd) of {
     Prelude.Just s ->
      case s of {
       (,) x s0 ->
        case x of {
         (,) i pos ->
          case go
                 (Seq.count (\x0 ->
                   Eqtype.eq_op Ssrnat.nat_eqType
                     (Prelude.snd (unsafeCoerce x0)) (unsafeCoerce pos))
                   (ScanState.unhandled maxReg sd)) (Morph.Build_SSInfo sd
                 __) of {
           Prelude.Left err -> Prelude.Left err;
           Prelude.Right ss ->
            walkIntervals maxReg (Morph.thisDesc maxReg sd ss) n}}};
     Prelude.Nothing -> Prelude.Right
      (ScanState.packScanState maxReg ScanState.InUse sd)})
    positions

data Allocation =
   Build_Allocation Prelude.Int Interval.IntervalDesc (Prelude.Maybe PhysReg)

intVal :: Prelude.Int -> Allocation -> Interval.IntervalDesc
intVal maxReg a =
  case a of {
   Build_Allocation intId intVal0 intReg0 -> intVal0}

intReg :: Prelude.Int -> Allocation -> Prelude.Maybe PhysReg
intReg maxReg a =
  case a of {
   Build_Allocation intId intVal0 intReg0 -> intReg0}

determineAllocations :: Prelude.Int -> ScanState.ScanStateDesc -> []
                        Allocation
determineAllocations maxReg sd =
  Prelude.map (\x -> Build_Allocation ( (Prelude.fst x))
    (Interval.getIntervalDesc
      (
        (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)
          (ScanState.intervals maxReg sd) (Prelude.fst x)))) (Prelude.snd x))
    (ScanState.handled maxReg sd)