module LinearScan.Morph 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.IState as IState
import qualified LinearScan.Interval as Interval
import qualified LinearScan.Lib as Lib
import qualified LinearScan.Logic as Logic
import qualified LinearScan.ScanState as ScanState
import qualified LinearScan.Specif as Specif
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
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 SplitReason =
AvailableForPart Prelude.Int
| IntersectsWithFixed Prelude.Int
| SplittingActive Prelude.Int
| SplittingInactive Prelude.Int
data SplitPosition =
BeforePos Lib.Coq_oddnum SplitReason
| EndOfLifetimeHole Lib.Coq_oddnum
data SpillDetails =
SD_NewToHandled
| SD_UnhandledToHandled Prelude.Int
| SD_ActiveToHandled Prelude.Int Prelude.Int
| SD_InactiveToHandled Prelude.Int Prelude.Int
data SSError =
ECannotInsertUnhAtPos SpillDetails Prelude.Int
| EIntervalBeginsBeforeUnhandled Prelude.Int
| ENoValidSplitPositionUnh SplitPosition Prelude.Int
| ENoValidSplitPosition SplitPosition Prelude.Int
| ECannotSplitSingleton SplitPosition Prelude.Int
| ERegisterAlreadyAssigned Prelude.Int
| ERegisterAssignmentsOverlap Prelude.Int
| EUnexpectedNoMoreUnhandled
| ECannotSpillIfRegisterRequired Prelude.Int
| EFuelExhausted
| ENotYetImplemented Prelude.Int
stbind :: (a4 -> IState.IState SSError a2 a3 a5) -> (IState.IState SSError
a1 a2 a4) -> IState.IState SSError a1 a3 a5
stbind f x =
IState.ijoin (IState.imap f x)
error_ :: SSError -> IState.IState SSError a1 a2 a3
error_ err x =
Prelude.Left err
return_ :: a3 -> IState.IState a1 a2 a2 a3
return_ =
IState.ipure
data SSInfo p =
Build_SSInfo ScanState.ScanStateDesc p
thisDesc :: Prelude.Int -> ScanState.ScanStateDesc -> (SSInfo a1) ->
ScanState.ScanStateDesc
thisDesc maxReg startDesc s =
case s of {
Build_SSInfo thisDesc0 thisHolds -> thisDesc0}
type SState p q a = IState.IState SSError (SSInfo p) (SSInfo q) a
withScanStatePO :: Prelude.Int -> ScanState.ScanStateDesc ->
(ScanState.ScanStateDesc -> () -> SState () () a1) ->
SState () () a1
withScanStatePO maxReg pre f i =
case i of {
Build_SSInfo thisDesc0 _ ->
let {f0 = f thisDesc0 __} in
let {x = Build_SSInfo thisDesc0 __} in
let {x0 = f0 x} in
case x0 of {
Prelude.Left s -> Prelude.Left s;
Prelude.Right p -> Prelude.Right
(case p of {
(,) a0 s -> (,) a0
(case s of {
Build_SSInfo thisDesc1 _ -> Build_SSInfo thisDesc1 __})})}}
liftLen :: Prelude.Int -> ScanState.ScanStateDesc -> (ScanState.ScanStateDesc
-> SState () () a1) -> SState () () a1
liftLen maxReg pre f _top_assumption_ =
let {
_evar_0_ = \sd ->
let {ss = Build_SSInfo sd __} in
let {_evar_0_ = \err -> Prelude.Left err} in
let {
_evar_0_0 = \_top_assumption_0 ->
let {
_evar_0_0 = \x _top_assumption_1 ->
let {_evar_0_0 = \sd' -> Prelude.Right ((,) x (Build_SSInfo sd' __))}
in
case _top_assumption_1 of {
Build_SSInfo x0 x1 -> _evar_0_0 x0}}
in
case _top_assumption_0 of {
(,) x x0 -> _evar_0_0 x x0}}
in
case f sd ss of {
Prelude.Left x -> _evar_0_ x;
Prelude.Right x -> _evar_0_0 x}}
in
case _top_assumption_ of {
Build_SSInfo x x0 -> _evar_0_ x}
strengthenHasLen :: Prelude.Int -> ScanState.ScanStateDesc ->
ScanState.ScanStateDesc -> Prelude.Maybe ()
strengthenHasLen maxReg pre sd =
let {_evar_0_ = \_ -> Prelude.Nothing} in
let {_evar_0_0 = \_a_ _l_ -> Prelude.Just __} in
case ScanState.unhandled maxReg sd of {
[] -> _evar_0_ __;
(:) x x0 -> _evar_0_0 x x0}
moveUnhandledToHandled :: Prelude.Int -> ScanState.ScanStateDesc -> SState
() () ()
moveUnhandledToHandled maxReg pre x =
case x of {
Build_SSInfo thisDesc0 _ ->
case thisDesc0 of {
ScanState.Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
unhandled0 active0 inactive0 handled0 ->
case unhandled0 of {
[] -> Logic.coq_False_rect;
(:) p unhandled1 ->
case p of {
(,) i n ->
let {
_evar_0_ = \_ -> Prelude.Right ((,) () (Build_SSInfo
(ScanState.Build_ScanStateDesc nextInterval0 intervals0
fixedIntervals0 unhandled1 active0 inactive0 ((:) ((,)
(Prelude.fst ((,) i n)) Prelude.Nothing) handled0)) __))}
in
let {
_evar_0_0 = \_ -> Prelude.Left (ECannotSpillIfRegisterRequired
( i))}
in
case Eqtype.eq_op
(Eqtype.option_eqType
(Eqtype.sig_eqType
(Eqtype.sig_eqType Ssrnat.nat_eqType
(unsafeCoerce Ssrnat.odd)) (\u ->
(Prelude.&&)
((Prelude.<=)
(Interval.ibeg
(
(LinearScan.Utils.nth nextInterval0 intervals0
i))) ( (unsafeCoerce u)))
((Prelude.<=) ( (unsafeCoerce u))
(Interval.iend
(
(LinearScan.Utils.nth nextInterval0 intervals0
i)))))))
(unsafeCoerce
(Interval.firstUseReqReg
( (LinearScan.Utils.nth nextInterval0 intervals0 i))))
(unsafeCoerce Prelude.Nothing) of {
Prelude.True -> _evar_0_ __;
Prelude.False -> _evar_0_0 __}}}}}
moveUnhandledToActive :: Prelude.Int -> ScanState.ScanStateDesc -> PhysReg ->
SState () () ()
moveUnhandledToActive maxReg pre reg x =
case x of {
Build_SSInfo thisDesc0 _ ->
case thisDesc0 of {
ScanState.Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
unhandled0 active0 inactive0 handled0 ->
case unhandled0 of {
[] -> Logic.coq_False_rect;
(:) p unhandled1 ->
let {
_evar_0_ = \_ -> Prelude.Right ((,) () (Build_SSInfo
(ScanState.Build_ScanStateDesc nextInterval0 intervals0
fixedIntervals0 unhandled1 ((:) ((,) (Prelude.fst p) reg) active0)
inactive0 handled0) __))}
in
let {
_evar_0_0 = \_ -> Prelude.Left (ERegisterAlreadyAssigned ( reg))}
in
case Prelude.not
(Ssrbool.in_mem (unsafeCoerce reg)
(Ssrbool.mem
(Seq.seq_predType (Fintype.ordinal_eqType maxReg))
(unsafeCoerce (Prelude.map (\i -> Prelude.snd i) active0)))) of {
Prelude.True -> _evar_0_ __;
Prelude.False -> _evar_0_0 __}}}}
moveActiveToHandled :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Bool
-> Eqtype.Equality__Coq_sort -> Specif.Coq_sig2
ScanState.ScanStateDesc
moveActiveToHandled maxReg sd spilled x =
ScanState.Build_ScanStateDesc (ScanState.nextInterval maxReg sd)
(ScanState.intervals maxReg sd) (ScanState.fixedIntervals maxReg sd)
(ScanState.unhandled maxReg sd)
(unsafeCoerce
(Seq.rem
(Eqtype.prod_eqType
(Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd))
(Fintype.ordinal_eqType maxReg)) x
(unsafeCoerce (ScanState.active maxReg sd))))
(ScanState.inactive maxReg sd) ((:) ((,) (Prelude.fst (unsafeCoerce x))
(case spilled of {
Prelude.True -> Prelude.Nothing;
Prelude.False -> Prelude.Just (Prelude.snd (unsafeCoerce x))}))
(ScanState.handled maxReg sd))
moveActiveToInactive :: Prelude.Int -> ScanState.ScanStateDesc ->
Eqtype.Equality__Coq_sort -> Specif.Coq_sig2
ScanState.ScanStateDesc
moveActiveToInactive maxReg sd x =
ScanState.Build_ScanStateDesc (ScanState.nextInterval maxReg sd)
(ScanState.intervals maxReg sd) (ScanState.fixedIntervals maxReg sd)
(ScanState.unhandled maxReg sd)
(unsafeCoerce
(Seq.rem
(Eqtype.prod_eqType
(Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd))
(Fintype.ordinal_eqType maxReg)) x
(unsafeCoerce (ScanState.active maxReg sd)))) ((:) (unsafeCoerce x)
(ScanState.inactive maxReg sd)) (ScanState.handled maxReg sd)
moveInactiveToActive :: Prelude.Int -> ScanState.ScanStateDesc ->
Eqtype.Equality__Coq_sort -> Specif.Coq_sig2
ScanState.ScanStateDesc
moveInactiveToActive maxReg sd x =
ScanState.Build_ScanStateDesc (ScanState.nextInterval maxReg sd)
(ScanState.intervals maxReg sd) (ScanState.fixedIntervals maxReg sd)
(ScanState.unhandled maxReg sd) ((:) (unsafeCoerce x)
(ScanState.active maxReg sd))
(unsafeCoerce
(Seq.rem
(Eqtype.prod_eqType
(Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd))
(Fintype.ordinal_eqType maxReg)) x
(unsafeCoerce (ScanState.inactive maxReg sd))))
(ScanState.handled maxReg sd)
moveInactiveToHandled :: Prelude.Int -> ScanState.ScanStateDesc ->
Prelude.Bool -> Eqtype.Equality__Coq_sort ->
Specif.Coq_sig2 ScanState.ScanStateDesc
moveInactiveToHandled maxReg sd spilled x =
ScanState.Build_ScanStateDesc (ScanState.nextInterval maxReg sd)
(ScanState.intervals maxReg sd) (ScanState.fixedIntervals maxReg sd)
(ScanState.unhandled maxReg sd) (ScanState.active maxReg sd)
(unsafeCoerce
(Seq.rem
(Eqtype.prod_eqType
(Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd))
(Fintype.ordinal_eqType maxReg)) x
(unsafeCoerce (ScanState.inactive maxReg sd)))) ((:) ((,)
(Prelude.fst (unsafeCoerce x))
(case spilled of {
Prelude.True -> Prelude.Nothing;
Prelude.False -> Prelude.Just (Prelude.snd (unsafeCoerce x))}))
(ScanState.handled maxReg sd))