module LinearScan.Split 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.Context as Context
import qualified LinearScan.Datatypes as Datatypes
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.Spill as Spill
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"
type PhysReg = Prelude.Int
data SplitPosition =
BeforePos Prelude.Int
| EndOfLifetimeHole Prelude.Int
coq_SplitPositionToT :: SplitPosition -> Trace.SplitPositionT
coq_SplitPositionToT x =
case x of {
BeforePos n -> Trace.BeforePosT n;
EndOfLifetimeHole n -> Trace.EndOfLifetimeHoleT n}
splitPosition :: Interval.IntervalDesc -> SplitPosition -> Prelude.Int
splitPosition d pos =
case pos of {
BeforePos n -> n;
EndOfLifetimeHole n ->
Interval.afterLifetimeHole (Interval.getIntervalDesc d) n}
splitUnhandledInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
ScanState.IntervalId -> Prelude.Int -> ([]
((,) ScanState.IntervalId Prelude.Int)) ->
SplitPosition -> ([] Trace.SSTrace) ->
Prelude.Either ([] Trace.SSTrace)
ScanState.ScanStateSig
splitUnhandledInterval maxReg sd uid beg us pos e =
(Prelude.flip (Prelude.$)) ((:) (Trace.ESplitUnhandledInterval
(Prelude.id uid) (coq_SplitPositionToT pos)) e) (\e2 ->
let {
_evar_0_ = \_nextInterval_ ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 us0 ->
let {int = Vector0.vnth _nextInterval_ ints uid0} in
let {splitPos = splitPosition ( int) pos} in
let {optSplitPos = Spill.optimalSplitPosition ( int) beg splitPos} in
let {
_evar_0_ = \_ ->
let {
_evar_0_ = \iv ib ie rds ->
let {
_top_assumption_ = Interval.splitInterval
(Interval.Build_IntervalDesc iv ib ie rds)
optSplitPos}
in
let {
_evar_0_ = \i0 i1 ->
let {
_evar_0_ = let {
_evar_0_ = \_ _ ->
(Prelude.flip (Prelude.$)) __ (\_ ->
let {
sd' = ScanState.Build_ScanStateDesc
_nextInterval_ ints _fixedIntervals_ unh
_active_ _inactive_ _handled_}
in
let {
_evar_0_ = \_ _ ->
let {
_evar_0_ = \_discharged_uid_ _discharged_us_ ->
Logic.coq_False_rect}
in
let {
_evar_0_0 = \x xs uid1 us1 ->
(Prelude.flip (Prelude.$)) __ (\_ ->
let {
_evar_0_0 = \_ ->
(Prelude.flip (Prelude.$)) __
(let {
_evar_0_0 = let {
_evar_0_0 = (Prelude.flip (Prelude.$))
__
(\_ _ ->
Prelude.Right
(ScanState.packScanState
maxReg
ScanState.InUse
(ScanState.Build_ScanStateDesc
((Prelude.succ)
_nextInterval_)
(unsafeCoerce
(Vector0.vshiftin
_nextInterval_
(Vector0.vreplace
_nextInterval_
ints uid1
( i0))
( i1)))
_fixedIntervals_
(List1.insert
(Prelude0.lebf
Prelude.snd)
((,)
(
_nextInterval_)
(Interval.ibeg
( i1)))
((:)
(Prelude.id
((,) uid1
beg))
(Prelude.map
Prelude.id
us1)))
(Prelude.map
Prelude.id
_active_)
(Prelude.map
Prelude.id
_inactive_)
(Prelude.map
Prelude.id
_handled_))))}
in
_evar_0_0}
in
_evar_0_0)}
in
_evar_0_0 __)}
in
case unh of {
[] -> _evar_0_ uid0 us0;
(:) x x0 -> _evar_0_0 x x0 uid0 us0}}
in
let {
_evar_0_0 = \_ _ -> Prelude.Left ((:)
(Trace.ECannotModifyHandledInterval
(Prelude.id uid0)) e2)}
in
case Prelude.not
(Ssrbool.in_mem (unsafeCoerce uid0)
(Ssrbool.mem
(Seq.seq_predType
(Fintype.ordinal_eqType
(ScanState.nextInterval maxReg
sd')))
(unsafeCoerce
(ScanState.handledIds maxReg sd')))) of {
Prelude.True -> _evar_0_ __;
Prelude.False -> _evar_0_0 __}) __}
in
_evar_0_ __}
in
_evar_0_ __}
in
case _top_assumption_ of {
(,) x x0 -> _evar_0_ x x0}}
in
case int of {
Interval.Build_IntervalDesc x x0 x1 x2 -> _evar_0_ x x0 x1 x2}}
in
let {
_evar_0_0 = \_ ->
let {
_evar_0_0 = \_ ->
let {
sd0 = ScanState.Build_ScanStateDesc _nextInterval_ ints
_fixedIntervals_ unh _active_ _inactive_ _handled_}
in
let {_evar_0_0 = \err -> Prelude.Left err} in
let {
_evar_0_1 = \_top_assumption_ ->
let {
_evar_0_1 = \_top_assumption_0 -> Prelude.Right
_top_assumption_}
in
let {
_evar_0_2 = \_ ->
let {_evar_0_2 = \_ -> Prelude.Right _top_assumption_} in
let {
_evar_0_3 = \_ -> Prelude.Left ((:)
(Trace.ENoValidSplitPosition (Prelude.id uid0)) e)}
in
case (Prelude.<=) ((Prelude.succ) 0)
(Data.List.length
(ScanState.unhandled maxReg ( _top_assumption_))) of {
Prelude.True -> _evar_0_2 __;
Prelude.False -> _evar_0_3 __}}
in
case Interval.firstUseReqReg ( int) of {
Prelude.Just x -> _evar_0_1 x;
Prelude.Nothing -> _evar_0_2 __}}
in
case Spill.spillInterval maxReg sd0 int uid0 beg us0
Spill.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.ENoValidSplitPosition
(Prelude.id uid0)) e)}
in
case (Prelude.<=) beg (Interval.ibeg ( int)) of {
Prelude.True -> _evar_0_0 __;
Prelude.False -> _evar_0_1 __}}
in
case (Prelude.&&)
((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int)))
optSplitPos)
((Prelude.<=) ((Prelude.succ) optSplitPos)
(Interval.iend ( int))) of {
Prelude.True -> _evar_0_ __;
Prelude.False -> _evar_0_0 __}}
in
case sd of {
ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
_evar_0_ x x0 x1 x2 x3 x4 x5 uid us})
splitCurrentInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
SplitPosition -> Morph.SState () () ()
splitCurrentInterval maxReg pre pos e ssi =
let {
_evar_0_ = \desc ->
let {_evar_0_ = \_ _ _ _ _ -> Logic.coq_False_rect} in
let {
_evar_0_0 = \_top_assumption_ ->
let {
_evar_0_0 = \uid beg us ->
(Prelude.flip (Prelude.$)) ((:) (Trace.ESplitCurrentInterval
(Prelude.id uid) (coq_SplitPositionToT pos)) e) (\e2 _ _ _ _ ->
let {
_evar_0_0 = \_nextInterval_ intervals0 fints unhandled0 _active_ _inactive_ _handled_ uid0 us0 _top_assumption_0 ->
let {_evar_0_0 = \err -> Prelude.Left err} in
let {
_evar_0_1 = \_top_assumption_1 -> Prelude.Right ((,) ()
(Morph.Build_SSInfo _top_assumption_1 __))}
in
case _top_assumption_0 of {
Prelude.Left x -> _evar_0_0 x;
Prelude.Right x -> _evar_0_1 x}}
in
case desc of {
ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
_evar_0_0 x x0 x1 x2 x3 x4 x5 uid us
(splitUnhandledInterval maxReg desc uid beg us pos e2)})}
in
(\us _ ->
case _top_assumption_ of {
(,) x x0 -> _evar_0_0 x x0 us})}
in
case ScanState.unhandled maxReg desc of {
[] -> _evar_0_ __ __ __ __;
(:) x x0 -> _evar_0_0 x x0 __ __ __ __}}
in
case ssi of {
Morph.Build_SSInfo x x0 -> _evar_0_ x __}
splitActiveOrInactiveInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
ScanState.IntervalId -> Prelude.Int -> ([]
((,) ScanState.IntervalId Prelude.Int)) ->
ScanState.IntervalId -> SplitPosition ->
PhysReg -> (Prelude.Either () ()) -> ([]
Trace.SSTrace) -> Prelude.Either
([] Trace.SSTrace) ScanState.ScanStateSig
splitActiveOrInactiveInterval maxReg sd uid beg us xid pos reg hin e =
(Prelude.flip (Prelude.$)) ((:) (Trace.ESplitActiveOrInactiveInterval
(Prelude.id xid)
(case hin of {
Prelude.Left _ -> Prelude.True;
Prelude.Right _ -> Prelude.False}) (coq_SplitPositionToT pos)) e)
(\e2 ->
let {
_evar_0_ = \ni ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 us0 xid0 hin0 ->
let {int = Vector0.vnth ni ints xid0} in
let {splitPos = splitPosition ( int) pos} in
let {optSplitPos = Spill.optimalSplitPosition ( int) beg splitPos} in
let {
sd0 = ScanState.Build_ScanStateDesc ni ints _fixedIntervals_ unh
_active_ _inactive_ _handled_}
in
(Prelude.flip (Prelude.$)) __ (\_ ->
let {
_evar_0_ = \_ ->
let {
_evar_0_ = \iv ib ie rds ->
let {
_top_assumption_ = Interval.splitInterval
(Interval.Build_IntervalDesc iv ib ie rds)
optSplitPos}
in
let {
_evar_0_ = \i0 i1 ->
let {
_evar_0_ = let {
_evar_0_ = \_ _ ->
(Prelude.flip (Prelude.$)) __ (\_ ->
let {
_evar_0_ = \_ _ ->
let {
sd1 = ScanState.Build_ScanStateDesc ni
(Vector0.vreplace ni ints xid0 ( i0))
_fixedIntervals_ unh _active_ _inactive_
_handled_}
in
(Prelude.flip (Prelude.$)) __ (\_ ->
(Prelude.flip (Prelude.$)) __ (\_ ->
(Prelude.flip (Prelude.$)) __ (\_ ->
let {
_evar_0_ = \err -> Prelude.Left err}
in
let {
_evar_0_0 = \_top_assumption_0 ->
Prelude.Right _top_assumption_0}
in
case Spill.spillInterval maxReg sd1 i1
uid0 beg us0 Spill.NewToHandled
e2 of {
Prelude.Left x -> _evar_0_ x;
Prelude.Right x -> _evar_0_0 x})))}
in
let {
_evar_0_0 = \_ _ -> Prelude.Left ((:)
(Trace.ECannotModifyHandledInterval
(Prelude.id xid0)) e2)}
in
case Prelude.not
(Ssrbool.in_mem (unsafeCoerce xid0)
(Ssrbool.mem
(Seq.seq_predType
(Fintype.ordinal_eqType
(ScanState.nextInterval maxReg
sd0)))
(unsafeCoerce
(ScanState.handledIds maxReg sd0)))) of {
Prelude.True -> _evar_0_ __;
Prelude.False -> _evar_0_0 __}) __}
in
_evar_0_ __}
in
_evar_0_ __}
in
case _top_assumption_ of {
(,) x x0 -> _evar_0_ x x0}}
in
case int of {
Interval.Build_IntervalDesc x x0 x1 x2 -> _evar_0_ x x0 x1 x2}}
in
let {
_evar_0_0 = \_ ->
let {
_evar_0_0 = \_ ->
let {
_evar_0_0 = \_ ->
let {_evar_0_0 = \err -> Prelude.Left err} in
let {
_evar_0_1 = \_top_assumption_ -> Prelude.Right
_top_assumption_}
in
case Spill.spillInterval maxReg sd0 int uid0 beg us0
(Spill.ActiveToHandled xid0 (unsafeCoerce reg)) e2 of {
Prelude.Left x -> _evar_0_0 x;
Prelude.Right x -> _evar_0_1 x}}
in
let {
_evar_0_1 = \_ ->
let {_evar_0_1 = \err -> Prelude.Left err} in
let {
_evar_0_2 = \_top_assumption_ -> Prelude.Right
_top_assumption_}
in
case Spill.spillInterval maxReg sd0 int uid0 beg us0
(Spill.InactiveToHandled xid0 (unsafeCoerce reg)) e2 of {
Prelude.Left x -> _evar_0_1 x;
Prelude.Right x -> _evar_0_2 x}}
in
case hin0 of {
Prelude.Left x -> _evar_0_0 x;
Prelude.Right x -> _evar_0_1 x}}
in
let {
_evar_0_1 = \_ -> Prelude.Left ((:) (Trace.ENoValidSplitPosition
(Prelude.id xid0)) e2)}
in
case (Prelude.<=) beg (Interval.ibeg ( int)) of {
Prelude.True -> _evar_0_0 __;
Prelude.False -> _evar_0_1 __}}
in
case (Prelude.&&)
((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int)))
optSplitPos)
((Prelude.<=) ((Prelude.succ) optSplitPos)
(Interval.iend ( int))) of {
Prelude.True -> _evar_0_ __;
Prelude.False -> _evar_0_0 __})}
in
case sd of {
ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
_evar_0_ x x0 x1 x2 x3 x4 x5 uid us xid hin})
splitAssignedIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->
PhysReg -> SplitPosition -> Prelude.Bool ->
Morph.SState () () ()
splitAssignedIntervalForReg maxReg pre reg pos trueForActives e ssi =
let {
_evar_0_ = \desc ->
let {
intlist = case trueForActives of {
Prelude.True -> ScanState.active maxReg desc;
Prelude.False -> ScanState.inactive maxReg desc}}
in
(Prelude.flip (Prelude.$)) __ (\_ ->
let {
intids = Prelude.map (\i -> Prelude.fst i)
(Prelude.filter (\i ->
Eqtype.eq_op (Fintype.ordinal_eqType maxReg)
(Prelude.snd (unsafeCoerce i)) (unsafeCoerce reg))
intlist)}
in
(Prelude.flip (Prelude.$)) __ (\_ ->
let {_evar_0_ = \intlist0 intids0 -> Logic.coq_False_rect} in
let {
_evar_0_0 = \_top_assumption_ ->
let {
_evar_0_0 = \uid beg us ->
let {
_evar_0_0 = \_nextInterval_ intervals0 fints _unhandled_ active0 inactive0 _handled_ uid0 us0 intlist0 intids0 ->
let {
_evar_0_0 = \_ -> Prelude.Right ((,) () (Morph.Build_SSInfo
(ScanState.Build_ScanStateDesc _nextInterval_ intervals0
fints _unhandled_ active0 inactive0 _handled_) __))}
in
let {
_evar_0_1 = \aid aids iHaids ->
(Prelude.flip (Prelude.$)) ((:)
(Trace.ESplitAssignedIntervalForReg (Prelude.id aid)
(Prelude.id reg) (coq_SplitPositionToT pos)) e) (\e2 ->
let {
_evar_0_1 = \_ ->
let {
_top_assumption_0 = \x x0 x1 x2 x3 x4 ->
splitActiveOrInactiveInterval maxReg
(ScanState.Build_ScanStateDesc _nextInterval_
intervals0 fints _unhandled_ active0 inactive0
_handled_) x x0 x1 x2 x3 x4}
in
(Prelude.flip (Prelude.$))
(let {
_evar_0_1 = \_ ->
let {_evar_0_1 = \_ -> Prelude.Left __} in
_evar_0_1 __}
in
let {
_evar_0_2 = \_ ->
let {_evar_0_2 = \_ -> Prelude.Right __} in
_evar_0_2 __}
in
case trueForActives of {
Prelude.True -> _evar_0_1 __;
Prelude.False -> _evar_0_2 __})
(\hin' _top_assumption_1 ->
let {_top_assumption_2 = _top_assumption_1 hin' e2} in
let {_evar_0_1 = \err -> Prelude.Left err} in
let {
_evar_0_2 = \_top_assumption_3 -> Prelude.Right ((,)
()
(let {
_evar_0_2 = \_ ->
(Prelude.flip (Prelude.$)) __
(let {
act_to_inact = ScanState.Build_ScanStateDesc
(ScanState.nextInterval maxReg
_top_assumption_3)
(ScanState.intervals maxReg
_top_assumption_3)
(ScanState.fixedIntervals maxReg
_top_assumption_3)
(ScanState.unhandled maxReg
_top_assumption_3)
(unsafeCoerce
(Seq.rem
(Eqtype.prod_eqType
(Fintype.ordinal_eqType
(ScanState.nextInterval maxReg
_top_assumption_3))
(Fintype.ordinal_eqType maxReg))
(unsafeCoerce ((,) (Prelude.id aid) reg))
(unsafeCoerce
(ScanState.active maxReg
_top_assumption_3)))) ((:) ((,)
(Prelude.id aid) reg)
(ScanState.inactive maxReg _top_assumption_3))
(ScanState.handled maxReg _top_assumption_3)}
in
\_ ->
let {
_evar_0_2 = \_ -> Morph.Build_SSInfo
act_to_inact __}
in
_evar_0_2 __)}
in
let {
_evar_0_3 = \_ ->
let {
_evar_0_3 = \_ -> Morph.Build_SSInfo
_top_assumption_3 __}
in
_evar_0_3 __}
in
case Ssrbool.in_mem
(unsafeCoerce ((,) (Prelude.id aid) reg))
(Ssrbool.mem
(Seq.seq_predType
(Eqtype.prod_eqType
(Fintype.ordinal_eqType
(ScanState.nextInterval maxReg
_top_assumption_3))
(Fintype.ordinal_eqType maxReg)))
(unsafeCoerce
(ScanState.active maxReg
_top_assumption_3))) of {
Prelude.True -> _evar_0_2 __;
Prelude.False -> _evar_0_3 __}))}
in
case _top_assumption_2 of {
Prelude.Left x -> _evar_0_1 x;
Prelude.Right x -> _evar_0_2 x})
(_top_assumption_0 uid0 beg us0 aid pos reg)}
in
let {
_evar_0_2 = \_ -> Prelude.Left ((:)
(Trace.ECannotSplitSingleton (Prelude.id aid)) e2)}
in
case (Prelude.<=) beg
(splitPosition
(
(Vector0.vnth
(ScanState.nextInterval maxReg
(ScanState.Build_ScanStateDesc
_nextInterval_ intervals0 fints _unhandled_
active0 inactive0 _handled_))
(ScanState.intervals maxReg
(ScanState.Build_ScanStateDesc
_nextInterval_ intervals0 fints _unhandled_
active0 inactive0 _handled_)) aid)) pos) of {
Prelude.True -> _evar_0_1 __;
Prelude.False -> _evar_0_2 __})}
in
Datatypes.list_rect _evar_0_0 (\aid aids iHaids _ ->
_evar_0_1 aid aids iHaids) intids0 __}
in
(\intlist0 _ intids0 _ _ _ _ _ ->
case desc of {
ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
_evar_0_0 x x0 x1 x2 x3 x4 x5 uid us intlist0 intids0})}
in
(\us _ ->
case _top_assumption_ of {
(,) x x0 -> _evar_0_0 x x0 us})}
in
case ScanState.unhandled maxReg desc of {
[] -> (\_ _ _ _ -> _evar_0_ intlist intids);
(:) x x0 -> _evar_0_0 x x0 __ intlist __ intids __})) __ __ __}
in
case ssi of {
Morph.Build_SSInfo x x0 -> _evar_0_ x __}
splitActiveIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->
PhysReg -> Prelude.Int -> Morph.SState ()
() ()
splitActiveIntervalForReg maxReg pre reg pos =
Context.context (Trace.ESplitActiveIntervalForReg (Prelude.id reg)
(coq_SplitPositionToT (BeforePos pos)))
(splitAssignedIntervalForReg maxReg pre reg (BeforePos pos) Prelude.True)
splitAnyInactiveIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->
PhysReg -> Prelude.Int -> Morph.SState
() () ()
splitAnyInactiveIntervalForReg maxReg pre reg pos e ss =
(Prelude.flip (Prelude.$)) ((:) (Trace.ESplitAnyInactiveIntervalForReg
(Prelude.id reg) (coq_SplitPositionToT (EndOfLifetimeHole pos))) e)
(\e2 ->
(Prelude.flip (Prelude.$)) (\s ->
splitAssignedIntervalForReg maxReg s reg (EndOfLifetimeHole pos)
Prelude.False) (\_top_assumption_ ->
let {_top_assumption_0 = _top_assumption_ pre e2 ss} in
let {_evar_0_ = \err -> Prelude.Right ((,) () ss)} in
let {
_evar_0_0 = \_top_assumption_1 ->
let {
_evar_0_0 = \_the_1st_wildcard_ ss' -> Prelude.Right ((,) () ss')}
in
case _top_assumption_1 of {
(,) x x0 -> _evar_0_0 x x0}}
in
case _top_assumption_0 of {
Prelude.Left x -> _evar_0_ x;
Prelude.Right x -> _evar_0_0 x}))