module LinearScan.LiveSets 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.Applicative as Applicative
import qualified LinearScan.Blocks as Blocks
import qualified LinearScan.Functor as Functor
import qualified LinearScan.Identity as Identity
import qualified LinearScan.IntMap as IntMap
import qualified LinearScan.IntSet as IntSet
import qualified LinearScan.Lens as Lens
import qualified LinearScan.List1 as List1
import qualified LinearScan.Monad as Monad
import qualified LinearScan.Prelude0 as Prelude0
import qualified LinearScan.State as State
import qualified LinearScan.State0 as State0
import qualified LinearScan.UsePos as UsePos
import qualified LinearScan.Eqtype as Eqtype
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"
data BlockLiveSets =
Build_BlockLiveSets IntSet.IntSet IntSet.IntSet IntSet.IntSet IntSet.IntSet
Blocks.OpId Blocks.OpId
blockLiveGen :: BlockLiveSets -> IntSet.IntSet
blockLiveGen b =
case b of {
Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveGen0}
blockLiveKill :: BlockLiveSets -> IntSet.IntSet
blockLiveKill b =
case b of {
Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveKill0}
blockLiveIn :: BlockLiveSets -> IntSet.IntSet
blockLiveIn b =
case b of {
Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveIn0}
blockLiveOut :: BlockLiveSets -> IntSet.IntSet
blockLiveOut b =
case b of {
Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveOut0}
blockFirstOpId :: BlockLiveSets -> Blocks.OpId
blockFirstOpId b =
case b of {
Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockFirstOpId0}
blockLastOpId :: BlockLiveSets -> Blocks.OpId
blockLastOpId b =
case b of {
Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLastOpId0}
emptyBlockLiveSets :: BlockLiveSets
emptyBlockLiveSets =
Build_BlockLiveSets IntSet.emptyIntSet IntSet.emptyIntSet
IntSet.emptyIntSet IntSet.emptyIntSet ((Prelude.succ) 0) ((Prelude.succ)
0)
eqBlockLiveSets :: BlockLiveSets -> BlockLiveSets -> Prelude.Bool
eqBlockLiveSets s1 s2 =
case s1 of {
Build_BlockLiveSets lg1 lk1 li1 lo1 fi1 la1 ->
case s2 of {
Build_BlockLiveSets lg2 lk2 li2 lo2 fi2 la2 ->
(Prelude.&&)
(Eqtype.eq_op IntSet.coq_IntSet_eqType (unsafeCoerce lg1)
(unsafeCoerce lg2))
((Prelude.&&)
(Eqtype.eq_op IntSet.coq_IntSet_eqType (unsafeCoerce lk1)
(unsafeCoerce lk2))
((Prelude.&&)
(Eqtype.eq_op IntSet.coq_IntSet_eqType (unsafeCoerce li1)
(unsafeCoerce li2))
((Prelude.&&)
(Eqtype.eq_op IntSet.coq_IntSet_eqType (unsafeCoerce lo1)
(unsafeCoerce lo2))
((Prelude.&&)
(Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fi1)
(unsafeCoerce fi2))
(Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce la1)
(unsafeCoerce la2))))))}}
eqBlockLiveSetsP :: Eqtype.Equality__Coq_axiom BlockLiveSets
eqBlockLiveSetsP _top_assumption_ =
let {
_evar_0_ = \lg1 lk1 li1 lo1 fi1 la1 _top_assumption_0 ->
let {
_evar_0_ = \lg2 lk2 li2 lo2 fi2 la2 ->
let {
_evar_0_ = \_ ->
let {
_evar_0_ = let {
_evar_0_ = \_ ->
let {
_evar_0_ = let {
_evar_0_ = \_ ->
let {
_evar_0_ = let {
_evar_0_ = \_ ->
let {
_evar_0_ = let {
_evar_0_ = \_ ->
let {
_evar_0_ =
let {
_evar_0_ = \_ ->
let {
_evar_0_ = Ssrbool.ReflectT}
in
_evar_0_}
in
let {
_evar_0_0 = \_ ->
Ssrbool.ReflectF}
in
case
Eqtype.eqP
Ssrnat.nat_eqType
la1 la2 of {
Ssrbool.ReflectT ->
_evar_0_
__;
Ssrbool.ReflectF ->
_evar_0_0
__}}
in
_evar_0_}
in
let {
_evar_0_0 = \_ ->
Ssrbool.ReflectF}
in
case Eqtype.eqP
Ssrnat.nat_eqType
fi1 fi2 of {
Ssrbool.ReflectT ->
_evar_0_ __;
Ssrbool.ReflectF ->
_evar_0_0 __}}
in
_evar_0_}
in
let {
_evar_0_0 = \_ ->
Ssrbool.ReflectF}
in
case Eqtype.eqP
IntSet.coq_IntSet_eqType
lo1 lo2 of {
Ssrbool.ReflectT ->
_evar_0_ __;
Ssrbool.ReflectF ->
_evar_0_0 __}}
in
_evar_0_}
in
let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
case Eqtype.eqP IntSet.coq_IntSet_eqType
li1 li2 of {
Ssrbool.ReflectT -> _evar_0_ __;
Ssrbool.ReflectF -> _evar_0_0 __}}
in
_evar_0_}
in
let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
case Eqtype.eqP IntSet.coq_IntSet_eqType lk1 lk2 of {
Ssrbool.ReflectT -> _evar_0_ __;
Ssrbool.ReflectF -> _evar_0_0 __}}
in
_evar_0_}
in
let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
case Eqtype.eqP IntSet.coq_IntSet_eqType lg1 lg2 of {
Ssrbool.ReflectT -> _evar_0_ __;
Ssrbool.ReflectF -> _evar_0_0 __}}
in
case _top_assumption_0 of {
Build_BlockLiveSets x x0 x1 x2 x3 x4 ->
unsafeCoerce _evar_0_ x x0 x1 x2 x3 x4}}
in
case _top_assumption_ of {
Build_BlockLiveSets x x0 x1 x2 x3 x4 ->
unsafeCoerce _evar_0_ x x0 x1 x2 x3 x4}
coq_BlockLiveSets_eqMixin :: Eqtype.Equality__Coq_mixin_of BlockLiveSets
coq_BlockLiveSets_eqMixin =
Eqtype.Equality__Mixin eqBlockLiveSets eqBlockLiveSetsP
coq_BlockLiveSets_eqType :: Eqtype.Equality__Coq_type
coq_BlockLiveSets_eqType =
unsafeCoerce coq_BlockLiveSets_eqMixin
_blockLiveGen :: (Functor.Functor a1) -> (IntSet.IntSet -> a1) ->
BlockLiveSets -> a1
_blockLiveGen h f s =
Functor.fmap h (\x -> Build_BlockLiveSets x (blockLiveKill s)
(blockLiveIn s) (blockLiveOut s) (blockFirstOpId s) (blockLastOpId s))
(f (blockLiveGen s))
_blockLiveKill :: (Functor.Functor a1) -> (IntSet.IntSet -> a1) ->
BlockLiveSets -> a1
_blockLiveKill h f s =
Functor.fmap h (\x -> Build_BlockLiveSets (blockLiveGen s) x
(blockLiveIn s) (blockLiveOut s) (blockFirstOpId s) (blockLastOpId s))
(f (blockLiveKill s))
_blockLiveIn :: (Functor.Functor a1) -> (IntSet.IntSet -> a1) ->
BlockLiveSets -> a1
_blockLiveIn h f s =
Functor.fmap h (\x -> Build_BlockLiveSets (blockLiveGen s)
(blockLiveKill s) x (blockLiveOut s) (blockFirstOpId s)
(blockLastOpId s)) (f (blockLiveIn s))
_blockLiveOut :: (Functor.Functor a1) -> (IntSet.IntSet -> a1) ->
BlockLiveSets -> a1
_blockLiveOut h f s =
Functor.fmap h (\x -> Build_BlockLiveSets (blockLiveGen s)
(blockLiveKill s) (blockLiveIn s) x (blockFirstOpId s) (blockLastOpId s))
(f (blockLiveOut s))
_blockFirstOpId :: (Functor.Functor a1) -> (Blocks.OpId -> a1) ->
BlockLiveSets -> a1
_blockFirstOpId h f s =
Functor.fmap h (\x -> Build_BlockLiveSets (blockLiveGen s)
(blockLiveKill s) (blockLiveIn s) (blockLiveOut s) x (blockLastOpId s))
(f (blockFirstOpId s))
_blockLastOpId :: (Functor.Functor a1) -> (Blocks.OpId -> a1) ->
BlockLiveSets -> a1
_blockLastOpId h f s =
Functor.fmap h (\x -> Build_BlockLiveSets (blockLiveGen s)
(blockLiveKill s) (blockLiveIn s) (blockLiveOut s) (blockFirstOpId s) x)
(f (blockLastOpId s))
computeLiveSets :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo
a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> a1 ->
Prelude.Int -> State.State BlockLiveSets Prelude.Int
computeLiveSets maxReg mDict binfo oinfo b idx =
case Blocks.blockOps mDict binfo b of {
(,) p opse ->
case p of {
(,) opsb opsm ->
Monad.bind
(State0.coq_StateT_Monad (unsafeCoerce Identity.coq_Identity_Monad))
(\x ->
Monad.bind (unsafeCoerce State.coq_State_Monad) (\x0 ->
Monad.forFoldM (unsafeCoerce State.coq_State_Monad) idx
((Prelude.++) opsb ((Prelude.++) opsm opse)) (\next o ->
case List1.partition (\v ->
Eqtype.eq_op UsePos.coq_VarKind_eqType
(unsafeCoerce (Blocks.varKind maxReg v))
(unsafeCoerce UsePos.Input))
(Blocks.opRefs maxReg mDict oinfo o) of {
(,) inputs others ->
Monad.bind (unsafeCoerce State.coq_State_Monad) (\x1 ->
Monad.bind (unsafeCoerce State.coq_State_Monad) (\x2 ->
Monad.bind (unsafeCoerce State.coq_State_Monad) (\x3 ->
Applicative.pure
(unsafeCoerce State.coq_State_Applicative)
((Prelude.succ) ((Prelude.succ) next)))
(Lens.modifyStateT (\_ -> _blockLastOpId) next
(unsafeCoerce Identity.coq_Identity_Monad)))
(Monad.forM_ (unsafeCoerce State.coq_State_Monad) others
(\v ->
case Blocks.varId maxReg v of {
Prelude.Left p0 ->
Applicative.pure
(unsafeCoerce State.coq_State_Applicative) ();
Prelude.Right vid ->
Lens.applyStateT (\_ -> _blockLiveKill)
(IntSet.coq_IntSet_insert vid)
(unsafeCoerce Identity.coq_Identity_Monad)})))
(Monad.forM_ (unsafeCoerce State.coq_State_Monad) inputs
(\v ->
case Blocks.varId maxReg v of {
Prelude.Left p0 ->
Applicative.pure
(unsafeCoerce State.coq_State_Applicative) ();
Prelude.Right vid ->
Monad.bind (unsafeCoerce State.coq_State_Monad)
(\liveKill ->
Monad.unless (unsafeCoerce State.coq_State_Monad)
(IntSet.coq_IntSet_member vid liveKill)
(Lens.applyStateT (\_ -> _blockLiveGen)
(IntSet.coq_IntSet_insert vid)
(unsafeCoerce Identity.coq_Identity_Monad)))
(Lens.use (Lens.stepdownl' (\_ -> _blockLiveKill))
(unsafeCoerce Identity.coq_Identity_Monad))}))}))
(Lens.modifyStateT (\_ -> _blockLastOpId) idx
(unsafeCoerce Identity.coq_Identity_Monad)))
(Lens.modifyStateT (\_ -> _blockFirstOpId)
((Prelude.+) idx (Ssrnat.double (Data.List.length opsb)))
(unsafeCoerce Identity.coq_Identity_Monad))}}
computeLocalLiveSets :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo
a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([]
a1) -> IntMap.IntMap BlockLiveSets
computeLocalLiveSets maxReg mDict binfo oinfo blocks =
Prelude.snd
(List1.forFold ((,) ((Prelude.succ) 0) IntMap.emptyIntMap) blocks
(\acc b ->
case acc of {
(,) idx m ->
case computeLiveSets maxReg mDict binfo oinfo b idx
emptyBlockLiveSets of {
(,) idx' liveSets ->
let {k = Blocks.blockId mDict binfo b} in
(,) idx' (IntMap.coq_IntMap_insert k liveSets m)}}))
updateLiveSets :: (IntMap.IntMap BlockLiveSets) -> ([] Blocks.BlockId) ->
State.State BlockLiveSets ()
updateLiveSets blockLiveSets suxs =
Monad.bind
(State0.coq_StateT_Monad (unsafeCoerce Identity.coq_Identity_Monad))
(\x ->
Monad.bind (unsafeCoerce State.coq_State_Monad) (\x0 ->
Monad.bind (unsafeCoerce State.coq_State_Monad) (\ls ->
Lens.modifyStateT (\_ -> _blockLiveIn)
(IntSet.coq_IntSet_union
(IntSet.coq_IntSet_difference (blockLiveOut ls)
(blockLiveKill ls)) (blockLiveGen ls))
(unsafeCoerce Identity.coq_Identity_Monad))
(unsafeCoerce State.get))
(Monad.forM_ (unsafeCoerce State.coq_State_Monad) suxs (\s_bid ->
case IntMap.coq_IntMap_lookup s_bid blockLiveSets of {
Prelude.Just sux ->
Lens.applyStateT (\_ -> _blockLiveOut)
(Prelude0.flip IntSet.coq_IntSet_union (blockLiveIn sux))
(unsafeCoerce Identity.coq_Identity_Monad);
Prelude.Nothing ->
Applicative.pure (unsafeCoerce State.coq_State_Applicative) ()})))
(Lens.modifyStateT (\_ -> _blockLiveOut) IntSet.emptyIntSet
(unsafeCoerce Identity.coq_Identity_Monad))
computeGlobalLiveSets :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1
a2 a3 a4) -> ([] a1) -> (IntMap.IntMap
BlockLiveSets) -> IntMap.IntMap BlockLiveSets
computeGlobalLiveSets mDict binfo blocks liveSets =
List1.forFoldr liveSets blocks (\b liveSets1 ->
let {bid = Blocks.blockId mDict binfo b} in
case IntMap.coq_IntMap_lookup bid liveSets1 of {
Prelude.Just liveSet ->
let {suxs = Blocks.blockSuccessors mDict binfo b} in
case updateLiveSets liveSets suxs liveSet of {
(,) x liveSet' -> IntMap.coq_IntMap_insert bid liveSet' liveSets1};
Prelude.Nothing -> liveSets1})
computeGlobalLiveSetsRecursively :: (Monad.Monad a5) -> (Blocks.BlockInfo
a5 a1 a2 a3 a4) -> ([] a1) ->
(IntMap.IntMap BlockLiveSets) ->
IntMap.IntMap BlockLiveSets
computeGlobalLiveSetsRecursively mDict binfo blocks liveSets =
let {
go = let {
go n previous =
(\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
(\_ ->
Applicative.pure Identity.coq_Identity_Applicative previous)
(\n0 ->
let {
computed = computeGlobalLiveSets mDict binfo blocks previous}
in
case Eqtype.eq_op
(IntMap.coq_IntMap_eqType coq_BlockLiveSets_eqType)
(unsafeCoerce previous) (unsafeCoerce computed) of {
Prelude.True -> unsafeCoerce computed;
Prelude.False -> go n0 computed})
n}
in go}
in
unsafeCoerce go (Data.List.length blocks) liveSets