module LinearScan.LiveSets 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.Applicative as Applicative
import qualified LinearScan.Blocks as Blocks
import qualified LinearScan.Functor as Functor
import qualified LinearScan.IntMap as IntMap
import qualified LinearScan.IntSet as IntSet
import qualified LinearScan.Iso as Iso
import qualified LinearScan.List1 as List1
import qualified LinearScan.Monad as Monad
import qualified LinearScan.UsePos as UsePos
import qualified LinearScan.Yoneda as Yoneda
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}
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
computeLocalLiveSets :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo
a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([]
a1) -> a5
computeLocalLiveSets maxReg mDict binfo oinfo blocks =
Iso.iso_to
(Yoneda.coq_Yoneda_lemma
(Applicative.is_functor (Monad.is_applicative mDict)))
(Functor.fmap (unsafeCoerce Yoneda.coq_Yoneda_Functor) Prelude.snd
(Monad.forFoldM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) ((,)
((Prelude.succ) 0) IntMap.emptyIntMap) blocks (\acc b ->
case acc of {
(,) idx m ->
case Blocks.blockOps mDict binfo b of {
(,) p opse ->
case p of {
(,) opsb opsm ->
let {
liveSet = Build_BlockLiveSets IntSet.emptyIntSet
IntSet.emptyIntSet IntSet.emptyIntSet IntSet.emptyIntSet
((Prelude.+) idx (Ssrnat.double (Data.List.length opsb)))
idx}
in
case List1.forFold ((,) idx liveSet)
((Prelude.++) opsb ((Prelude.++) opsm opse)) (\acc0 o ->
case acc0 of {
(,) lastIdx liveSet1 -> (,) ((Prelude.succ)
((Prelude.succ) lastIdx))
(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 ->
let {
liveSet2 = List1.forFold liveSet1 inputs
(\liveSet2 v ->
case Blocks.varId maxReg v of {
Prelude.Left p0 -> liveSet2;
Prelude.Right vid ->
case Prelude.not
(IntSet.coq_IntSet_member
vid
(blockLiveKill liveSet2)) of {
Prelude.True ->
Build_BlockLiveSets
(IntSet.coq_IntSet_insert vid
(blockLiveGen liveSet2))
(blockLiveKill liveSet2)
(blockLiveIn liveSet2)
(blockLiveOut liveSet2)
(blockFirstOpId liveSet2) lastIdx;
Prelude.False -> liveSet2}})}
in
let {
liveSet3 = List1.forFold liveSet2 others
(\liveSet3 v ->
case Blocks.varId maxReg v of {
Prelude.Left p0 -> liveSet3;
Prelude.Right vid ->
Build_BlockLiveSets
(blockLiveGen liveSet3)
(IntSet.coq_IntSet_insert vid
(blockLiveKill liveSet3))
(blockLiveIn liveSet3)
(blockLiveOut liveSet3)
(blockFirstOpId liveSet3) lastIdx})}
in
Build_BlockLiveSets (blockLiveGen liveSet3)
(blockLiveKill liveSet3) (blockLiveIn liveSet3)
(blockLiveOut liveSet3) (blockFirstOpId liveSet3)
lastIdx})}) of {
(,) lastIdx' liveSet3 ->
Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict))
(\k ->
Applicative.pure
(unsafeCoerce
(Yoneda.coq_Yoneda_Applicative
(Monad.is_applicative mDict))) ((,) lastIdx'
(IntMap.coq_IntMap_insert k liveSet3 m))) (\_ ->
Blocks.blockId mDict binfo b)}}}})))
computeGlobalLiveSets :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1
a2 a3 a4) -> ([] a1) -> (IntMap.IntMap
BlockLiveSets) -> a5
computeGlobalLiveSets mDict binfo blocks liveSets =
Iso.iso_to
(Yoneda.coq_Yoneda_lemma
(Applicative.is_functor (Monad.is_applicative mDict)))
(Monad.forFoldrM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) liveSets
blocks (\b liveSets1 ->
Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\bid ->
case IntMap.coq_IntMap_lookup bid liveSets1 of {
Prelude.Just liveSet ->
Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\suxs ->
let {
liveSet2 = List1.forFold liveSet suxs (\liveSet2 s_bid ->
case IntMap.coq_IntMap_lookup s_bid liveSets1 of {
Prelude.Just sux -> Build_BlockLiveSets
(blockLiveGen liveSet2) (blockLiveKill liveSet2)
(blockLiveIn liveSet2)
(IntSet.coq_IntSet_union (blockLiveOut liveSet2)
(blockLiveIn sux)) (blockFirstOpId liveSet2)
(blockLastOpId liveSet2);
Prelude.Nothing -> liveSet2})}
in
Applicative.pure
(unsafeCoerce
(Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))
(IntMap.coq_IntMap_insert bid (Build_BlockLiveSets
(blockLiveGen liveSet2) (blockLiveKill liveSet2)
(IntSet.coq_IntSet_union
(IntSet.coq_IntSet_difference (blockLiveOut liveSet2)
(blockLiveKill liveSet2)) (blockLiveGen liveSet2))
(blockLiveOut liveSet2) (blockFirstOpId liveSet2)
(blockLastOpId liveSet2)) liveSets1))
(unsafeCoerce (\_ -> Blocks.blockSuccessors mDict binfo b));
Prelude.Nothing ->
Applicative.pure
(unsafeCoerce
(Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))
liveSets1}) (\_ -> Blocks.blockId mDict binfo b)))
computeGlobalLiveSetsRecursively :: (Monad.Monad a5) -> (Blocks.BlockInfo
a5 a1 a2 a3 a4) -> ([] a1) ->
(IntMap.IntMap BlockLiveSets) -> a5
computeGlobalLiveSetsRecursively mDict binfo blocks liveSets =
let {
go n previous =
(\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
(\_ ->
Applicative.pure (Monad.is_applicative mDict) previous)
(\n0 ->
Monad.bind mDict (\computed ->
case Eqtype.eq_op
(IntMap.coq_IntMap_eqType coq_BlockLiveSets_eqType)
(unsafeCoerce previous) computed of {
Prelude.True ->
Applicative.pure (Monad.is_applicative mDict) computed;
Prelude.False -> unsafeCoerce go n0 computed})
(computeGlobalLiveSets mDict binfo blocks previous))
n}
in go (Data.List.length blocks) liveSets