module LinearScan.Spill 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.Interval as Interval
import qualified LinearScan.List1 as List1
import qualified LinearScan.Logic as Logic
import qualified LinearScan.Morph as Morph
import qualified LinearScan.Prelude0 as Prelude0
import qualified LinearScan.ScanState as ScanState
import qualified LinearScan.Trace as Trace
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
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base as GHC.Base
import qualified GHC.Prim as GHC.Prim
#else
import qualified LinearScan.IOExts as IOExts
#endif
#ifdef __GLASGOW_HASKELL__
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
unsafeCoerce = IOExts.unsafeCoerce
#endif
__ :: any
__ = Prelude.error "Logical or arity value used"
data SpillCondition =
NewToHandled
| UnhandledToHandled
| ActiveToHandled Prelude.Int Eqtype.Equality__Coq_sort
| InactiveToHandled Prelude.Int Eqtype.Equality__Coq_sort
coq_SpillConditionToT :: Prelude.Int -> ScanState.ScanStateDesc ->
ScanState.IntervalId -> Interval.IntervalDesc ->
SpillCondition -> Trace.SpillConditionT
coq_SpillConditionToT maxReg sd uid i x =
case x of {
NewToHandled -> Trace.NewToHandledT (Prelude.id uid);
UnhandledToHandled -> Trace.UnhandledToHandledT (Prelude.id uid);
ActiveToHandled xid reg -> Trace.ActiveToHandledT (Prelude.id xid)
(Prelude.id (unsafeCoerce reg));
InactiveToHandled xid reg -> Trace.InactiveToHandledT (Prelude.id xid)
(Prelude.id (unsafeCoerce reg))}
optimalSplitPosition :: Interval.IntervalDesc -> Prelude.Int -> Prelude.Int
-> Prelude.Int
optimalSplitPosition d lb ub =
ub
spillInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
Interval.IntervalDesc -> ScanState.IntervalId -> Prelude.Int
-> ([] ((,) ScanState.IntervalId Prelude.Int)) ->
SpillCondition -> ([] Trace.SSTrace) -> Prelude.Either
([] Trace.SSTrace) ScanState.ScanStateSig
spillInterval maxReg sd i1 uid beg us spill e =
(Prelude.flip (Prelude.$)) ((:) (Trace.ESpillInterval
(coq_SpillConditionToT maxReg sd uid i1 spill)) e) (\e2 ->
let {
_evar_0_ = \_top_assumption_ ->
(Prelude.flip (Prelude.$)) ((:) (Trace.EIntervalHasUsePosReqReg
_top_assumption_) e2) (\e3 ->
let {optSplitPos2 = optimalSplitPosition ( i1) beg _top_assumption_}
in
let {
_evar_0_ = \_ ->
let {
_evar_0_ = \_ ->
(Prelude.flip (Prelude.$)) __
(let {
_evar_0_ = \_ -> Prelude.Right
(ScanState.packScanState maxReg ScanState.InUse
(ScanState.Build_ScanStateDesc ((Prelude.succ)
(ScanState.nextInterval maxReg sd))
(unsafeCoerce
(Vector0.vshiftin (ScanState.nextInterval maxReg sd)
(ScanState.intervals maxReg sd) ( i1)))
(ScanState.fixedIntervals maxReg sd)
(List1.insert (Prelude0.lebf Prelude.snd) ((,)
( (ScanState.nextInterval maxReg sd))
(Interval.ibeg ( i1))) ((:) (Prelude.id ((,) uid beg))
(Prelude.map Prelude.id us)))
(Prelude.map Prelude.id (ScanState.active maxReg sd))
(Prelude.map Prelude.id (ScanState.inactive maxReg sd))
(Prelude.map Prelude.id (ScanState.handled maxReg sd))))}
in
_evar_0_)}
in
let {
_evar_0_0 = \_ -> Prelude.Left ((:) (Trace.ECannotInsertUnhandled
beg (Interval.ibeg ( i1)) optSplitPos2 (Interval.iend ( i1)))
((:) Trace.EIntervalBeginsAtSplitPosition e3))}
in
case (Prelude.<=) ((Prelude.succ) beg) (Interval.ibeg ( i1)) of {
Prelude.True -> _evar_0_ __;
Prelude.False -> _evar_0_0 __}}
in
let {
_evar_0_0 = \_ ->
(Prelude.flip (Prelude.$)) __ (\_ ->
let {
_top_assumption_0 = Interval.splitInterval ( i1) optSplitPos2}
in
let {
_evar_0_0 = \i1_0 i1_1 ->
let {
_evar_0_0 = \_top_assumption_1 -> Prelude.Left ((:)
(Trace.ECannotSpillIfRegisterRequiredBefore optSplitPos2
_top_assumption_1) e3)}
in
let {
_evar_0_1 = \_ ->
let {
_evar_0_1 = \_ ->
(Prelude.flip (Prelude.$)) __
(let {
_evar_0_1 = (Prelude.flip (Prelude.$)) __ (\_ _ ->
let {
unh' = List1.insert
(Prelude0.lebf Prelude.snd)
((,)
(
(ScanState.nextInterval
maxReg sd))
(Interval.ibeg ( i1_1))) ((:)
(Prelude.id ((,) uid beg))
(Prelude.map Prelude.id us))}
in
let {
sd' = ScanState.Build_ScanStateDesc
((Prelude.succ)
(ScanState.nextInterval maxReg sd))
(unsafeCoerce
(Vector0.vshiftin
(ScanState.nextInterval maxReg sd)
(ScanState.intervals maxReg sd)
( i1_1)))
(ScanState.fixedIntervals maxReg sd)
unh'
(Prelude.map Prelude.id
(ScanState.active maxReg sd))
(Prelude.map Prelude.id
(ScanState.inactive maxReg sd))
(Prelude.map Prelude.id
(ScanState.handled maxReg sd))}
in
(Prelude.flip (Prelude.$)) __ (\_ ->
let {
_evar_0_1 = let {
_evar_0_1 = \_ ->
Prelude.Right
(ScanState.Build_ScanStateDesc
((Prelude.succ)
(ScanState.nextInterval
maxReg sd'))
(unsafeCoerce
(Vector0.vshiftin
(ScanState.nextInterval
maxReg sd')
(ScanState.intervals
maxReg sd')
( i1_0)))
(ScanState.fixedIntervals
maxReg sd')
(Prelude.map Prelude.id
(ScanState.unhandled
maxReg sd'))
(Prelude.map Prelude.id
(ScanState.active
maxReg sd'))
(Prelude.map Prelude.id
(ScanState.inactive
maxReg sd')) ((:)
((,)
(
(ScanState.nextInterval
maxReg sd'))
Prelude.Nothing)
(Prelude.map Prelude.id
(ScanState.handled
maxReg sd'))))}
in
_evar_0_1 __}
in
let {
_evar_0_2 = \_ ->
(Prelude.flip (Prelude.$)) __ (\_ ->
(Prelude.flip (Prelude.$)) __
(\_ ->
let {
_evar_0_2 = \_ _ ->
let {
_evar_0_2 = \_ _ _ ->
let {
b = Prelude0.lebf
Prelude.snd
(Prelude.id ((,) uid
beg)) ((,)
(
(ScanState.nextInterval
maxReg sd))
(Interval.ibeg
( i1_1)))}
in
let {
_evar_0_2 = \_ ->
Logic.coq_False_rect}
in
let {
_evar_0_3 = \_ ->
Logic.coq_False_rect}
in
case b of {
Prelude.True -> _evar_0_2 __;
Prelude.False ->
_evar_0_3 __}}
in
let {
_evar_0_3 = \u' us' ->
(Prelude.flip (Prelude.$)) __
(\_ -> Prelude.Right
(ScanState.Build_ScanStateDesc
((Prelude.succ)
(ScanState.nextInterval
maxReg sd))
(Vector0.vreplace
((Prelude.succ)
(ScanState.nextInterval
maxReg sd))
(unsafeCoerce
(Vector0.vshiftin
(ScanState.nextInterval
maxReg sd)
(ScanState.intervals
maxReg sd)
( i1_1)))
(Prelude.id uid)
( i1_0))
(ScanState.fixedIntervals
maxReg sd) us'
(Prelude.map Prelude.id
(ScanState.active maxReg
sd))
(Prelude.map Prelude.id
(ScanState.inactive
maxReg sd)) ((:) ((,)
(Prelude.fst u')
Prelude.Nothing)
(Prelude.map Prelude.id
(ScanState.handled maxReg
sd)))))}
in
case unh' of {
[] -> _evar_0_2 __ __ __;
(:) x x0 -> _evar_0_3 x x0}}
in
let {
_evar_0_3 = \_ _ -> Prelude.Left
((:)
(Trace.ECannotModifyHandledInterval
(Prelude.id uid)) e3)}
in
case Prelude.not
(Ssrbool.in_mem
(unsafeCoerce
(Prelude.id uid))
(Ssrbool.mem
(Seq.seq_predType
(Fintype.ordinal_eqType
(ScanState.nextInterval
maxReg sd')))
(unsafeCoerce
(ScanState.handledIds
maxReg sd')))) of {
Prelude.True -> _evar_0_2 __;
Prelude.False -> _evar_0_3 __}))
__}
in
let {
_evar_0_3 = \xid reg ->
(Prelude.flip (Prelude.$)) __ (\_ ->
(Prelude.flip (Prelude.$)) __
(\_ ->
let {
_evar_0_3 = \_ _ ->
let {
sd'' = ScanState.Build_ScanStateDesc
((Prelude.succ)
(ScanState.nextInterval
maxReg sd))
(Vector0.vreplace
((Prelude.succ)
(ScanState.nextInterval
maxReg sd))
(unsafeCoerce
(Vector0.vshiftin
(ScanState.nextInterval
maxReg sd)
(ScanState.intervals
maxReg sd) ( i1_1)))
(Prelude.id xid) ( i1_0))
(ScanState.fixedIntervals
maxReg sd) unh'
(Prelude.map Prelude.id
(ScanState.active maxReg
sd))
(Prelude.map Prelude.id
(ScanState.inactive maxReg
sd))
(Prelude.map Prelude.id
(ScanState.handled maxReg
sd))}
in
let {
elem = Prelude.id ((,) xid
reg)}
in
(Prelude.flip (Prelude.$)) __
(\_ ->
let {
_evar_0_3 = \a b ->
(Prelude.flip (Prelude.$))
__ (\_ ->
let {
_top_assumption_1 =
Morph.moveActiveToHandled
maxReg sd''
Prelude.True
(unsafeCoerce ((,) a
b))}
in
Prelude.Right
_top_assumption_1)}
in
case elem of {
(,) x x0 -> _evar_0_3 x x0})}
in
let {
_evar_0_4 = \_ _ -> Prelude.Left
((:)
(Trace.ECannotModifyHandledInterval
(Prelude.id xid)) e3)}
in
case Prelude.not
(Ssrbool.in_mem
(unsafeCoerce
(Prelude.id xid))
(Ssrbool.mem
(Seq.seq_predType
(Fintype.ordinal_eqType
(ScanState.nextInterval
maxReg sd')))
(unsafeCoerce
(ScanState.handledIds
maxReg sd')))) of {
Prelude.True -> _evar_0_3 __;
Prelude.False -> _evar_0_4 __}))
__}
in
let {
_evar_0_4 = \xid reg ->
(Prelude.flip (Prelude.$)) __ (\_ ->
(Prelude.flip (Prelude.$)) __
(\_ ->
let {
_evar_0_4 = \_ _ ->
let {
sd'' = ScanState.Build_ScanStateDesc
((Prelude.succ)
(ScanState.nextInterval
maxReg sd))
(Vector0.vreplace
((Prelude.succ)
(ScanState.nextInterval
maxReg sd))
(unsafeCoerce
(Vector0.vshiftin
(ScanState.nextInterval
maxReg sd)
(ScanState.intervals
maxReg sd) ( i1_1)))
(Prelude.id xid) ( i1_0))
(ScanState.fixedIntervals
maxReg sd) unh'
(Prelude.map Prelude.id
(ScanState.active maxReg
sd))
(Prelude.map Prelude.id
(ScanState.inactive maxReg
sd))
(Prelude.map Prelude.id
(ScanState.handled maxReg
sd))}
in
let {
elem = Prelude.id ((,) xid
reg)}
in
(Prelude.flip (Prelude.$)) __
(\_ ->
let {
_evar_0_4 = \a b ->
(Prelude.flip (Prelude.$))
__ (\_ ->
let {
_top_assumption_1 =
Morph.moveInactiveToHandled
maxReg sd''
Prelude.True
(unsafeCoerce ((,) a
b))}
in
Prelude.Right
_top_assumption_1)}
in
case elem of {
(,) x x0 -> _evar_0_4 x x0})}
in
let {
_evar_0_5 = \_ _ -> Prelude.Left
((:)
(Trace.ECannotModifyHandledInterval
(Prelude.id xid)) e3)}
in
case Prelude.not
(Ssrbool.in_mem
(unsafeCoerce
(Prelude.id xid))
(Ssrbool.mem
(Seq.seq_predType
(Fintype.ordinal_eqType
(ScanState.nextInterval
maxReg sd')))
(unsafeCoerce
(ScanState.handledIds
maxReg sd')))) of {
Prelude.True -> _evar_0_4 __;
Prelude.False -> _evar_0_5 __}))
__}
in
case spill of {
NewToHandled -> _evar_0_1;
UnhandledToHandled -> _evar_0_2 __;
ActiveToHandled x x0 -> _evar_0_3 x x0;
InactiveToHandled x x0 ->
_evar_0_4 x x0}))}
in
_evar_0_1)}
in
_evar_0_1 __}
in
case Interval.firstUseReqReg ( i1_0) of {
Prelude.Just x -> _evar_0_0 x;
Prelude.Nothing -> _evar_0_1 __}}
in
case _top_assumption_0 of {
(,) x x0 -> _evar_0_0 x x0})}
in
case (Prelude.<=) optSplitPos2 (Interval.ibeg ( i1)) of {
Prelude.True -> _evar_0_ __;
Prelude.False -> _evar_0_0 __})}
in
let {
_evar_0_0 = \_ ->
let {
_evar_0_0 = Prelude.Right (ScanState.Build_ScanStateDesc
((Prelude.succ) (ScanState.nextInterval maxReg sd))
(unsafeCoerce
(Vector0.vshiftin (ScanState.nextInterval maxReg sd)
(ScanState.intervals maxReg sd) ( i1)))
(ScanState.fixedIntervals maxReg sd)
(Prelude.map Prelude.id (ScanState.unhandled maxReg sd))
(Prelude.map Prelude.id (ScanState.active maxReg sd))
(Prelude.map Prelude.id (ScanState.inactive maxReg sd)) ((:) ((,)
( (ScanState.nextInterval maxReg sd)) Prelude.Nothing)
(Prelude.map Prelude.id (ScanState.handled maxReg sd))))}
in
let {
_evar_0_1 = \_ ->
let {
_evar_0_1 = \_ ->
case sd of {
ScanState.Build_ScanStateDesc nextInterval0 intervals0
fixedIntervals0 unhandled0 active0 inactive0 handled0 ->
let {
_evar_0_1 = \_ ->
(Prelude.flip (Prelude.$)) __ (\_ -> Prelude.Right
(ScanState.Build_ScanStateDesc nextInterval0 intervals0
fixedIntervals0 us active0 inactive0 ((:) ((,)
(Prelude.fst ((,) uid beg)) Prelude.Nothing) handled0)))}
in
_evar_0_1 __}}
in
_evar_0_1 __}
in
let {
_evar_0_2 = \xid reg ->
(Prelude.flip (Prelude.$)) __ (\_ ->
let {
_top_assumption_ = Morph.moveActiveToHandled maxReg sd
Prelude.True (unsafeCoerce ((,) xid reg))}
in
Prelude.Right _top_assumption_)}
in
let {
_evar_0_3 = \xid reg ->
(Prelude.flip (Prelude.$)) __ (\_ ->
let {
_top_assumption_ = Morph.moveInactiveToHandled maxReg sd
Prelude.True (unsafeCoerce ((,) xid reg))}
in
Prelude.Right _top_assumption_)}
in
case spill of {
NewToHandled -> _evar_0_0;
UnhandledToHandled -> _evar_0_1 __;
ActiveToHandled x x0 -> _evar_0_2 x x0;
InactiveToHandled x x0 -> _evar_0_3 x x0}}
in
case Interval.firstUseReqReg ( i1) of {
Prelude.Just x -> _evar_0_ x;
Prelude.Nothing -> _evar_0_0 __})
spillCurrentInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
Morph.SState () () ()
spillCurrentInterval maxReg pre e ssi =
(Prelude.flip (Prelude.$)) ((:) Trace.ESpillCurrentInterval e) (\e2 ->
let {
_evar_0_ = \sd ->
let {_evar_0_ = \_ _ _ _ _ -> Logic.coq_False_rect} in
let {
_evar_0_0 = \_top_assumption_ ->
let {
_evar_0_0 = \uid beg us ->
(Prelude.flip (Prelude.$)) __
(let {
d =
(Vector0.vnth (ScanState.nextInterval maxReg sd)
(ScanState.intervals maxReg sd) uid)}
in
\_ _ ->
let {
_evar_0_0 = \_ ->
let {_evar_0_0 = \err -> Prelude.Left err} in
let {
_evar_0_1 = \_top_assumption_0 -> Prelude.Right ((,) ()
(Morph.Build_SSInfo _top_assumption_0 __))}
in
case spillInterval maxReg sd
(Vector0.vnth (ScanState.nextInterval maxReg sd)
(ScanState.intervals maxReg sd) uid) uid beg us
UnhandledToHandled e of {
Prelude.Left x -> _evar_0_0 x;
Prelude.Right x -> _evar_0_1 x}}
in
let {
_evar_0_1 = \_ -> Prelude.Left ((:)
(Trace.EIntervalBeginsBeforeUnhandled (Prelude.id uid)) e)}
in
case (Prelude.<=) beg (Interval.ibeg d) of {
Prelude.True -> _evar_0_0 __;
Prelude.False -> _evar_0_1 __})}
in
(\us _ _ _ _ ->
case _top_assumption_ of {
(,) x x0 -> _evar_0_0 x x0 us})}
in
case ScanState.unhandled maxReg sd of {
[] -> _evar_0_ __ __ __ __;
(:) x x0 -> _evar_0_0 x x0 __ __ __ __}}
in
case ssi of {
Morph.Build_SSInfo x x0 -> _evar_0_ x __})