{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -} 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 -- 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" 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 __})