module LinearScan.Spill 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.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.Eqtype as Eqtype
import qualified LinearScan.Ssrnat as Ssrnat
#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 ( uid);
UnhandledToHandled -> Trace.UnhandledToHandledT ( uid);
ActiveToHandled xid reg -> Trace.ActiveToHandledT ( xid)
( (unsafeCoerce reg));
InactiveToHandled xid reg -> Trace.InactiveToHandledT ( xid)
( (unsafeCoerce reg))}
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 {
_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))
(LinearScan.Utils.snoc (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
((:) 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)
_top_assumption_}
in
let {
_evar_0_0 = \i1_0 i1_1 ->
let {
_evar_0_0 = \_top_assumption_1 -> Prelude.Left ((:)
(Trace.ECannotSpillIfRegisterRequired ( _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))
(LinearScan.Utils.snoc
(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'))
(LinearScan.Utils.snoc
(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 {
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))
(LinearScan.Utils.set_nth
((Prelude.succ)
(ScanState.nextInterval
maxReg sd))
(LinearScan.Utils.snoc
(ScanState.nextInterval
maxReg sd)
(ScanState.intervals
maxReg sd) ( i1_1))
( 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 = \xid reg ->
(Prelude.flip (Prelude.$)) __ (\_ ->
(Prelude.flip (Prelude.$)) __
(\_ _ ->
let {
sd'' = ScanState.Build_ScanStateDesc
((Prelude.succ)
(ScanState.nextInterval maxReg
sd))
(LinearScan.Utils.set_nth
((Prelude.succ)
(ScanState.nextInterval
maxReg sd))
(LinearScan.Utils.snoc
(ScanState.nextInterval
maxReg sd)
(ScanState.intervals maxReg
sd) ( i1_1)) ( 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 = \xid reg ->
(Prelude.flip (Prelude.$)) __ (\_ ->
(Prelude.flip (Prelude.$)) __
(\_ _ ->
let {
sd'' = ScanState.Build_ScanStateDesc
((Prelude.succ)
(ScanState.nextInterval maxReg
sd))
(LinearScan.Utils.set_nth
((Prelude.succ)
(ScanState.nextInterval
maxReg sd))
(LinearScan.Utils.snoc
(ScanState.nextInterval
maxReg sd)
(ScanState.intervals maxReg
sd) ( i1_1)) ( 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
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 Eqtype.eq_op Ssrnat.nat_eqType
(unsafeCoerce (Interval.ibeg ( i1)))
(unsafeCoerce _top_assumption_) 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))
(LinearScan.Utils.snoc (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 =
(LinearScan.Utils.nth (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
(LinearScan.Utils.nth
(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 ( 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 __})