{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -} module LinearScan.Morph 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.Interval as Interval import qualified LinearScan.Logic as Logic import qualified LinearScan.ScanState as ScanState import qualified LinearScan.Specif as Specif 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 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 data SSInfo p = Build_SSInfo ScanState.ScanStateDesc p thisDesc :: Prelude.Int -> (SSInfo a1) -> ScanState.ScanStateDesc thisDesc maxReg s = case s of { Build_SSInfo thisDesc0 thisHolds -> thisDesc0} type SState p q a = Context.Context Trace.SSTrace (SSInfo p) (SSInfo q) a error_ :: Prelude.Int -> ScanState.ScanStateDesc -> ([] Trace.SSTrace) -> SState a1 a2 a3 error_ maxReg sd err x x0 = Prelude.Left err withScanStatePO :: Prelude.Int -> ScanState.ScanStateDesc -> (ScanState.ScanStateDesc -> () -> SState () () a1) -> SState () () a1 withScanStatePO maxReg pre f e i = case i of { Build_SSInfo thisDesc0 _ -> let {f0 = f thisDesc0 __} in let {x = Build_SSInfo thisDesc0 __} in let {x0 = f0 e x} in case x0 of { Prelude.Left err -> Prelude.Left err; 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 e _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 e 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 e 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 ((:) (Trace.ECannotSpillIfRegisterRequired (Prelude.id i)) e)} in case Eqtype.eq_op (Eqtype.option_eqType (Eqtype.sig_eqType Ssrnat.nat_eqType (\u -> (Prelude.&&) ((Prelude.<=) (Interval.ibeg ( (Vector0.vnth nextInterval0 intervals0 i))) (unsafeCoerce u)) ((Prelude.<=) ((Prelude.succ) (unsafeCoerce u)) (Interval.iend ( (Vector0.vnth nextInterval0 intervals0 i))))))) (unsafeCoerce (Interval.firstUseReqReg ( (Vector0.vnth 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 e 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 ((:) (Trace.ERegisterAlreadyAssigned (Prelude.id reg)) e)} 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))