{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -} 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 import qualified LinearScan.Ssrnat as Ssrnat #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" type PhysReg = Prelude.Int splitPosition :: Interval.IntervalDesc -> Morph.SplitPosition -> Lib.Coq_oddnum splitPosition d pos = case pos of { Morph.BeforePos n wildcard' -> n; Morph.EndOfLifetimeHole n -> Interval.afterLifetimeHole (Interval.getIntervalDesc d) n} data SpillCondition = NewToHandled | UnhandledToHandled | ActiveToHandled Prelude.Int Eqtype.Equality__Coq_sort | InactiveToHandled Prelude.Int Eqtype.Equality__Coq_sort spillConditionToDetails :: Prelude.Int -> ScanState.ScanStateDesc -> ScanState.IntervalId -> Interval.IntervalDesc -> SpillCondition -> Morph.SpillDetails spillConditionToDetails maxReg sd uid i spill = case spill of { NewToHandled -> Morph.SD_NewToHandled; UnhandledToHandled -> Morph.SD_UnhandledToHandled ( uid); ActiveToHandled xid reg -> Morph.SD_ActiveToHandled ( xid) ( (unsafeCoerce reg)); InactiveToHandled xid reg -> Morph.SD_InactiveToHandled ( xid) ( (unsafeCoerce reg))} spillInterval :: Prelude.Int -> ScanState.ScanStateDesc -> Interval.IntervalDesc -> ScanState.IntervalId -> Prelude.Int -> ([] ((,) ScanState.IntervalId Prelude.Int)) -> SpillCondition -> Prelude.Either Morph.SSError ScanState.ScanStateSig spillInterval maxReg sd i1 uid beg us spill = let { _evar_0_ = \_top_assumption_ -> 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) (Lib.insert (Lib.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 = \_ -> let {det = spillConditionToDetails maxReg sd uid i1 spill} in Prelude.Left (Morph.ECannotInsertUnhAtPos det beg)} 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 (Morph.ECannotSpillIfRegisterRequired ( _top_assumption_1))} in let { _evar_0_1 = \_ -> let { _evar_0_1 = \_ -> (Prelude.flip (Prelude.$)) __ (let { _evar_0_1 = (Prelude.flip (Prelude.$)) __ (\_ _ -> let { unh' = Lib.insert (Lib.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.$)) __ (\_ _ -> let { _evar_0_2 = \_ _ _ -> let { b = Lib.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.$)) __ (\_ _ -> 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.$)) __ (\_ _ -> 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 ssi = 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 of { Prelude.Left x -> _evar_0_0 x; Prelude.Right x -> _evar_0_1 x}} in let { _evar_0_1 = \_ -> Prelude.Left (Morph.EIntervalBeginsBeforeUnhandled ( uid))} 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 __} splitUnhandledInterval :: Prelude.Int -> ScanState.ScanStateDesc -> ScanState.IntervalId -> Prelude.Int -> ([] ((,) ScanState.IntervalId Prelude.Int)) -> Morph.SplitPosition -> Prelude.Either Morph.SSError ScanState.ScanStateSig splitUnhandledInterval maxReg sd uid beg us pos = let { _evar_0_ = \_nextInterval_ ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 us0 -> let {int = LinearScan.Utils.nth _nextInterval_ ints uid0} in let {splitPos = splitPosition ( int) pos} in let { _evar_0_ = \_ -> let { _evar_0_ = \iv ib ie rds -> let { _top_assumption_ = Interval.splitInterval (Interval.Build_IntervalDesc iv ib ie rds) splitPos} in let { _evar_0_ = \i0 i1 -> let { _evar_0_ = 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_) (LinearScan.Utils.snoc _nextInterval_ (LinearScan.Utils.set_nth _nextInterval_ ints uid1 ( i0)) ( i1)) _fixedIntervals_ (Lib.insert (Lib.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 _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 = \_ -> Prelude.Left (Morph.ENoValidSplitPositionUnh pos ( uid0))} in case (Prelude.&&) ((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int))) splitPos) ((Prelude.<=) splitPos (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 -> Morph.SplitPosition -> Morph.SState () () () splitCurrentInterval maxReg pre pos 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 -> let { _evar_0_0 = \_nextInterval_ intervals0 _fixedIntervals_ 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)}} 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 -> Morph.SplitPosition -> PhysReg -> (Prelude.Either () ()) -> Prelude.Either Morph.SSError ScanState.ScanStateSig splitActiveOrInactiveInterval maxReg sd uid beg us xid pos reg hin = let { _evar_0_ = \ni ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 us0 xid0 hin0 -> let {int = LinearScan.Utils.nth ni ints xid0} in let {splitPos = splitPosition ( int) pos} 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) splitPos} in let { _evar_0_ = \i0 i1 -> let { _evar_0_ = let { _evar_0_ = \_ _ -> let { sd1 = ScanState.Build_ScanStateDesc ni (LinearScan.Utils.set_nth 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 spillInterval maxReg sd1 i1 uid0 beg us0 NewToHandled of { Prelude.Left x -> _evar_0_ x; Prelude.Right x -> _evar_0_0 x})))} 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 spillInterval maxReg sd0 int uid0 beg us0 (ActiveToHandled xid0 (unsafeCoerce reg)) 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 spillInterval maxReg sd0 int uid0 beg us0 (InactiveToHandled xid0 (unsafeCoerce reg)) 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 (Morph.ENoValidSplitPosition pos ( xid0))} 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))) splitPos) ((Prelude.<=) splitPos (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 -> Morph.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_ = \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 _fixedIntervals_ _unhandled_ active0 inactive0 _handled_ uid0 us0 intlist0 intids0 -> let { _evar_0_0 = \_ -> Prelude.Right ((,) () (Morph.Build_SSInfo (ScanState.Build_ScanStateDesc _nextInterval_ intervals0 _fixedIntervals_ _unhandled_ active0 inactive0 _handled_) __))} in let { _evar_0_1 = \aid aids iHaids -> let { _evar_0_1 = \_ -> let { _top_assumption_0 = \x x0 x1 x2 x3 x4 -> splitActiveOrInactiveInterval maxReg (ScanState.Build_ScanStateDesc _nextInterval_ intervals0 _fixedIntervals_ _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'} 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 ((,) ( aid) reg)) (unsafeCoerce (ScanState.active maxReg _top_assumption_3)))) ((:) ((,) ( 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 ((,) ( 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 (Morph.ECannotSplitSingleton pos ( aid))} in case (Prelude.<=) beg ( (splitPosition ( (LinearScan.Utils.nth (ScanState.nextInterval maxReg (ScanState.Build_ScanStateDesc _nextInterval_ intervals0 _fixedIntervals_ _unhandled_ active0 inactive0 _handled_)) (ScanState.intervals maxReg (ScanState.Build_ScanStateDesc _nextInterval_ intervals0 _fixedIntervals_ _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 -> Lib.Coq_oddnum -> Morph.SState () () () splitActiveIntervalForReg maxReg pre reg pos = splitAssignedIntervalForReg maxReg pre reg (Morph.BeforePos pos (Morph.SplittingActive ( reg))) Prelude.True splitAnyInactiveIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc -> PhysReg -> Lib.Coq_oddnum -> Morph.SState () () () splitAnyInactiveIntervalForReg maxReg pre reg pos ss = (Prelude.flip (Prelude.$)) (\s -> splitAssignedIntervalForReg maxReg s reg (Morph.EndOfLifetimeHole pos) 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})