module LinearScan.Split 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.Datatypes as Datatypes
import qualified LinearScan.Interval as Interval
import qualified LinearScan.Lib as Lib
import qualified LinearScan.Logic as Logic
import qualified LinearScan.Morph as Morph
import qualified LinearScan.ScanState as ScanState
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
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
import qualified LinearScan.IOExts as IOExts
unsafeCoerce = IOExts.unsafeCoerce
#endif
__ :: any
__ = Prelude.error "Logical or arity value used"
type PhysReg = Prelude.Int
data SplitPosition =
BeforePos Lib.Coq_oddnum
| BeforeFirstUsePosReqReg
| EndOfLifetimeHole
splitPosition :: Interval.IntervalDesc -> SplitPosition -> Prelude.Maybe
Lib.Coq_oddnum
splitPosition d pos =
case pos of {
BeforePos x -> Prelude.Just x;
BeforeFirstUsePosReqReg ->
Interval.firstUseReqReg (Interval.getIntervalDesc d);
EndOfLifetimeHole -> Prelude.Nothing}
splitInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
ScanState.IntervalId -> SplitPosition -> Prelude.Bool ->
Prelude.Either Morph.SSError
(Prelude.Maybe ScanState.ScanStateSig)
splitInterval maxReg sd uid pos forCurrent =
let {
_evar_0_ = \_nextInterval_ ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 ->
let {
_evar_0_ = \uid1 -> Prelude.Left (Morph.ECannotSplitSingleton1 ( uid1))}
in
let {
_evar_0_0 = \_top_assumption_ ->
let {
_evar_0_0 = \u beg us uid1 ->
let {int = LinearScan.Utils.nth _nextInterval_ ints uid1} in
let {
_evar_0_0 = \_top_assumption_0 ->
let {
_evar_0_0 = \_ ->
(Prelude.flip (Prelude.$)) __ (\_ ->
let {
_evar_0_0 = \iv ib ie _iknd_ rds ->
let {
_top_assumption_1 = Interval.intervalSpan rds
_top_assumption_0 iv ib ie _iknd_}
in
let {
_evar_0_0 = \_top_assumption_2 ->
let {
_evar_0_0 = \_top_assumption_3 _top_assumption_4 ->
let {
_evar_0_0 = \_top_assumption_5 ->
let {
_evar_0_0 = \_ ->
let {
_evar_0_0 = \_ ->
let {
set_int_desc = ScanState.Build_ScanStateDesc
_nextInterval_
(LinearScan.Utils.set_nth _nextInterval_ ints
uid1 _top_assumption_3) _fixedIntervals_ ((:)
((,) u beg) us) _active_ _inactive_ _handled_}
in
let {
_evar_0_0 = \_ ->
(Prelude.flip (Prelude.$)) __
(let {
new_unhandled = ScanState.Build_ScanStateDesc
((Prelude.succ) _nextInterval_)
(LinearScan.Utils.snoc _nextInterval_
(LinearScan.Utils.set_nth _nextInterval_
ints uid1 _top_assumption_3)
_top_assumption_5) _fixedIntervals_
(Lib.insert (Lib.lebf Prelude.snd) ((,)
( _nextInterval_)
(Interval.ibeg _top_assumption_5)) ((:)
(Prelude.id ((,) u beg))
(Prelude.map Prelude.id us)))
(Prelude.map Prelude.id _active_)
(Prelude.map Prelude.id _inactive_)
(Prelude.map Prelude.id _handled_)}
in
\_ -> Prelude.Right (Prelude.Just
(ScanState.packScanState maxReg
ScanState.InUse new_unhandled)))}
in
let {
_evar_0_1 = \_ ->
let {
_evar_0_1 = \_top_assumption_6 ->
let {
_evar_0_1 = \_ ->
let {
_evar_0_1 = \iv1 ib1 ie1 _iknd1_ rds1 ->
let {
_top_assumption_7 = Interval.intervalSpan
rds1
_top_assumption_6
iv1 ib1 ie1 _iknd1_}
in
let {
_evar_0_1 = \_top_assumption_8 ->
let {
_evar_0_1 = \_top_assumption_9 _top_assumption_10 ->
let {
_evar_0_1 = \_top_assumption_11 ->
(Prelude.flip (Prelude.$)) __
(let {
new_unhandled = ScanState.Build_ScanStateDesc
((Prelude.succ) _nextInterval_)
(LinearScan.Utils.snoc
_nextInterval_
(LinearScan.Utils.set_nth
_nextInterval_ ints uid1
_top_assumption_3)
_top_assumption_11)
_fixedIntervals_
(Lib.insert
(Lib.lebf Prelude.snd) ((,)
( _nextInterval_)
(Interval.ibeg
_top_assumption_11)) ((:)
(Prelude.id ((,) u beg))
(Prelude.map Prelude.id us)))
(Prelude.map Prelude.id
_active_)
(Prelude.map Prelude.id
_inactive_)
(Prelude.map Prelude.id
_handled_)}
in
let {
_evar_0_1 = \_ _ -> Prelude.Right
(Prelude.Just
(ScanState.packScanState maxReg
ScanState.InUse new_unhandled))}
in
let {
_evar_0_2 = \_ _ -> Prelude.Left
(Morph.ECannotSplitSingleton3
( uid1))}
in
case (Prelude.<=) ((Prelude.succ)
beg)
(Interval.ibeg
_top_assumption_11) of {
Prelude.True -> _evar_0_1 __;
Prelude.False -> _evar_0_2 __})}
in
let {
_evar_0_2 = \_ -> Prelude.Right
(Prelude.Just
(ScanState.packScanState maxReg
ScanState.InUse set_int_desc))}
in
case _top_assumption_10 of {
Prelude.Just x -> (\_ -> _evar_0_1 x);
Prelude.Nothing -> _evar_0_2}}
in
let {
_evar_0_2 = \_top_assumption_9 ->
let {
_evar_0_2 = \_top_assumption_10 ->
(Prelude.flip (Prelude.$)) __
(let {
new_unhandled = ScanState.Build_ScanStateDesc
((Prelude.succ) _nextInterval_)
(LinearScan.Utils.snoc
_nextInterval_
(LinearScan.Utils.set_nth
_nextInterval_ ints uid1
_top_assumption_3)
_top_assumption_10)
_fixedIntervals_
(Lib.insert
(Lib.lebf Prelude.snd) ((,)
( _nextInterval_)
(Interval.ibeg
_top_assumption_10)) ((:)
(Prelude.id ((,) u beg))
(Prelude.map Prelude.id us)))
(Prelude.map Prelude.id
_active_)
(Prelude.map Prelude.id
_inactive_)
(Prelude.map Prelude.id
_handled_)}
in
let {
_evar_0_2 = \_ _ -> Prelude.Right
(Prelude.Just
(ScanState.packScanState maxReg
ScanState.InUse new_unhandled))}
in
let {
_evar_0_3 = \_ _ -> Prelude.Left
(Morph.ECannotSplitSingleton3
( uid1))}
in
case (Prelude.<=) ((Prelude.succ)
beg)
(Interval.ibeg
_top_assumption_10) of {
Prelude.True -> _evar_0_2 __;
Prelude.False -> _evar_0_3 __})}
in
let {
_evar_0_3 = \_ ->
Logic.coq_False_rect}
in
case _top_assumption_9 of {
Prelude.Just x -> (\_ -> _evar_0_2 x);
Prelude.Nothing -> _evar_0_3}}
in
case _top_assumption_8 of {
Prelude.Just x -> _evar_0_1 x;
Prelude.Nothing -> _evar_0_2}}
in
case _top_assumption_7 of {
(,) x x0 -> _evar_0_1 x x0 __}}
in
case _top_assumption_5 of {
Interval.Build_IntervalDesc x x0 x1 x2 x3 ->
_evar_0_1 x x0 x1 x2 x3}}
in
let {
_evar_0_2 = \_ -> Prelude.Left
(Morph.ECannotSplitSingleton2 ( uid1))}
in
case (Prelude.&&)
((Prelude.<=) ((Prelude.succ)
(Interval.ibeg _top_assumption_5))
_top_assumption_6)
((Prelude.<=) ((Prelude.succ)
_top_assumption_6)
(Interval.iend _top_assumption_5)) of {
Prelude.True -> _evar_0_1 __;
Prelude.False -> _evar_0_2 __}}
in
let {
_evar_0_2 = Prelude.Right (Prelude.Just
(ScanState.packScanState maxReg ScanState.InUse
set_int_desc))}
in
case splitPosition _top_assumption_5
BeforeFirstUsePosReqReg of {
Prelude.Just x -> _evar_0_1 x;
Prelude.Nothing -> _evar_0_2}}
in
case (Prelude.<=) ((Prelude.succ) beg)
(Interval.ibeg _top_assumption_5) of {
Prelude.True -> _evar_0_0 __;
Prelude.False -> _evar_0_1 __}}
in
_evar_0_0 __}
in
_evar_0_0 __}
in
let {
_evar_0_1 = \_ ->
let {
_evar_0_1 = Prelude.Left (Morph.ECannotSplitSingleton4
( uid1))}
in
let {
_evar_0_2 = let {
_evar_0_2 = \_ ->
let {
_evar_0_2 = \_ ->
let {
set_int_desc = ScanState.Build_ScanStateDesc
_nextInterval_
(LinearScan.Utils.set_nth
_nextInterval_ ints uid1
_top_assumption_3)
_fixedIntervals_ ((:) ((,) u beg)
us) _active_ _inactive_ _handled_}
in
Prelude.Right (Prelude.Just
(ScanState.packScanState maxReg
ScanState.InUse set_int_desc))}
in
_evar_0_2 __}
in
_evar_0_2 __}
in
case forCurrent of {
Prelude.True -> _evar_0_1;
Prelude.False -> _evar_0_2}}
in
case _top_assumption_4 of {
Prelude.Just x -> (\_ -> _evar_0_0 x);
Prelude.Nothing -> _evar_0_1}}
in
let {
_evar_0_1 = \_top_assumption_3 ->
let {
_evar_0_1 = \_top_assumption_4 ->
let {
_evar_0_1 = \_ ->
(Prelude.flip (Prelude.$)) __
(let {
new_unhandled = ScanState.Build_ScanStateDesc
((Prelude.succ) _nextInterval_)
(LinearScan.Utils.snoc _nextInterval_ ints
_top_assumption_4) _fixedIntervals_
(Lib.insert (Lib.lebf Prelude.snd) ((,)
( _nextInterval_)
(Interval.ibeg _top_assumption_4)) ((:)
(Prelude.id ((,) u beg))
(Prelude.map Prelude.id us)))
(Prelude.map Prelude.id _active_)
(Prelude.map Prelude.id _inactive_)
(Prelude.map Prelude.id _handled_)}
in
\_ -> Prelude.Right (Prelude.Just
(ScanState.packScanState maxReg ScanState.InUse
new_unhandled)))}
in
let {
_evar_0_2 = \_ -> Prelude.Left
(Morph.ECannotSplitSingleton5 ( uid1))}
in
case (Prelude.<=) ((Prelude.succ) beg)
(Interval.ibeg _top_assumption_4) of {
Prelude.True -> _evar_0_1 __;
Prelude.False -> _evar_0_2 __}}
in
let {_evar_0_2 = \_ -> Logic.coq_False_rect} in
case _top_assumption_3 of {
Prelude.Just x -> (\_ -> _evar_0_1 x);
Prelude.Nothing -> _evar_0_2}}
in
case _top_assumption_2 of {
Prelude.Just x -> _evar_0_0 x;
Prelude.Nothing -> _evar_0_1}}
in
case _top_assumption_1 of {
(,) x x0 -> _evar_0_0 x x0 __}}
in
case int of {
Interval.Build_IntervalDesc x x0 x1 x2 x3 ->
_evar_0_0 x x0 x1 x2 x3})}
in
let {
_evar_0_1 = \_ -> Prelude.Left (Morph.ECannotSplitSingleton2
( uid1))}
in
case (Prelude.&&)
((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int)))
_top_assumption_0)
((Prelude.<=) ((Prelude.succ) _top_assumption_0)
(Interval.iend ( int))) of {
Prelude.True -> _evar_0_0 __;
Prelude.False -> _evar_0_1 __}}
in
let {_evar_0_1 = Prelude.Right Prelude.Nothing} in
case splitPosition ( int) pos of {
Prelude.Just x -> _evar_0_0 x;
Prelude.Nothing -> _evar_0_1}}
in
(\us _ uid1 ->
case _top_assumption_ of {
(,) x x0 -> _evar_0_0 x x0 us uid1})}
in
case unh of {
[] -> _evar_0_ uid0;
(:) x x0 -> _evar_0_0 x x0 __ uid0}}
in
case sd of {
ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
_evar_0_ x x0 x1 x2 x3 x4 x5 uid}
splitCurrentInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
SplitPosition -> Morph.SState () () ()
splitCurrentInterval maxReg pre pos ssi =
let {
_evar_0_ = \desc ->
let {
_evar_0_ = \_nextInterval_ intervals0 _fixedIntervals_ unhandled0 _active_ _inactive_ _handled_ ->
let {_evar_0_ = \_ _ _ _ _ -> Logic.coq_False_rect} in
let {
_evar_0_0 = \_top_assumption_ ->
let {
_evar_0_0 = \uid beg us ->
let {
desc0 = ScanState.Build_ScanStateDesc _nextInterval_ intervals0
_fixedIntervals_ ((:) ((,) uid beg) us) _active_ _inactive_
_handled_}
in
(\_ _ _ _ ->
let {
_top_assumption_0 = splitInterval maxReg desc0 uid pos
Prelude.True}
in
let {_evar_0_0 = \err -> Prelude.Left err} in
let {
_evar_0_1 = \_top_assumption_1 ->
let {
_evar_0_1 = \_top_assumption_2 -> Prelude.Right ((,) ()
(Morph.Build_SSInfo _top_assumption_2 __))}
in
let {
_evar_0_2 = Prelude.Left (Morph.ECannotSplitSingleton6 ( uid))}
in
case _top_assumption_1 of {
Prelude.Just x -> _evar_0_1 x;
Prelude.Nothing -> _evar_0_2}}
in
case _top_assumption_0 of {
Prelude.Left x -> _evar_0_0 x;
Prelude.Right x -> _evar_0_1 x})}
in
(\us _ ->
case _top_assumption_ of {
(,) x x0 -> _evar_0_0 x x0 us})}
in
case unhandled0 of {
[] -> _evar_0_ __;
(:) x x0 -> _evar_0_0 x x0 __}}
in
case desc of {
ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
_evar_0_ x x0 x1 x2 x3 x4 x5 __ __ __}}
in
case ssi of {
Morph.Build_SSInfo x x0 -> _evar_0_ x __}
splitAssignedIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->
PhysReg -> SplitPosition -> Prelude.Bool ->
Morph.SState () () ()
splitAssignedIntervalForReg maxReg pre reg pos trueForActives 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_ = \_nextInterval_ intervals0 _fixedIntervals_ _unhandled_ active0 inactive0 _handled_ intlist0 intids0 ->
let {
desc0 = ScanState.Build_ScanStateDesc _nextInterval_ intervals0
_fixedIntervals_ _unhandled_ active0 inactive0 _handled_}
in
(\_ _ _ _ ->
let {_evar_0_ = \_ -> Prelude.Left Morph.ENoIntervalsToSplit} in
let {
_evar_0_0 = \aid aids iHaids ->
let {
_top_assumption_ = splitInterval maxReg desc0 aid pos
Prelude.False}
in
let {_evar_0_0 = \err -> Prelude.Left err} in
let {
_evar_0_1 = \_top_assumption_0 ->
let {
_evar_0_1 = \_top_assumption_1 -> Prelude.Right ((,) ()
(let {
_evar_0_1 = \_ ->
(Prelude.flip (Prelude.$)) __
(let {
act_to_inact = ScanState.Build_ScanStateDesc
(ScanState.nextInterval maxReg _top_assumption_1)
(ScanState.intervals maxReg _top_assumption_1)
(ScanState.fixedIntervals maxReg _top_assumption_1)
(ScanState.unhandled maxReg _top_assumption_1)
(unsafeCoerce
(Seq.rem
(Eqtype.prod_eqType
(Fintype.ordinal_eqType
(ScanState.nextInterval maxReg
_top_assumption_1))
(Fintype.ordinal_eqType maxReg))
(unsafeCoerce ((,) ( aid) reg))
(unsafeCoerce
(ScanState.active maxReg _top_assumption_1))))
((:) ((,) ( aid) reg)
(ScanState.inactive maxReg _top_assumption_1))
(ScanState.handled maxReg _top_assumption_1)}
in
\_ -> Morph.Build_SSInfo act_to_inact __)}
in
let {
_evar_0_2 = \_ -> Morph.Build_SSInfo _top_assumption_1 __}
in
case Ssrbool.in_mem (unsafeCoerce ((,) ( aid) reg))
(Ssrbool.mem
(Seq.seq_predType
(Eqtype.prod_eqType
(Fintype.ordinal_eqType
(ScanState.nextInterval maxReg
_top_assumption_1))
(Fintype.ordinal_eqType maxReg)))
(unsafeCoerce
(ScanState.active maxReg _top_assumption_1))) of {
Prelude.True -> _evar_0_1 __;
Prelude.False -> _evar_0_2 __}))}
in
let {
_evar_0_2 = Prelude.Left (Morph.ECannotSplitSingleton7
( aid))}
in
case _top_assumption_0 of {
Prelude.Just x -> _evar_0_1 x;
Prelude.Nothing -> _evar_0_2}}
in
case _top_assumption_ of {
Prelude.Left x -> _evar_0_0 x;
Prelude.Right x -> _evar_0_1 x}}
in
Datatypes.list_rect _evar_0_ (\aid aids iHaids _ ->
_evar_0_0 aid aids iHaids) intids0 __)}
in
case desc of {
ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
_evar_0_ x x0 x1 x2 x3 x4 x5 intlist intids})) __ __ __}
in
case ssi of {
Morph.Build_SSInfo x x0 -> _evar_0_ x __}
splitActiveIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->
PhysReg -> Lib.Coq_oddnum -> Morph.SState
() () ()
splitActiveIntervalForReg maxReg pre reg pos =
splitAssignedIntervalForReg maxReg pre reg (BeforePos pos) Prelude.True
splitAnyInactiveIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->
PhysReg -> Morph.SState () () ()
splitAnyInactiveIntervalForReg maxReg pre reg ss =
(Prelude.flip (Prelude.$)) (\s ->
splitAssignedIntervalForReg maxReg s reg EndOfLifetimeHole Prelude.False)
(\_top_assumption_ ->
let {_top_assumption_0 = _top_assumption_ pre 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})