{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -} 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.Blocks as Blocks import qualified LinearScan.IntMap as IntMap import qualified LinearScan.Lib as Lib 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 -- 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" data BlockLiveSets = Build_BlockLiveSets IntMap.IntSet IntMap.IntSet IntMap.IntSet IntMap.IntSet Blocks.OpId Blocks.OpId blockLiveGen :: BlockLiveSets -> IntMap.IntSet blockLiveGen b = case b of { Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0 blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveGen0} blockLiveKill :: BlockLiveSets -> IntMap.IntSet blockLiveKill b = case b of { Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0 blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveKill0} blockLiveIn :: BlockLiveSets -> IntMap.IntSet blockLiveIn b = case b of { Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0 blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveIn0} blockLiveOut :: BlockLiveSets -> IntMap.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 IntMap.coq_IntSet_eqType (unsafeCoerce lg1) (unsafeCoerce lg2)) ((Prelude.&&) (Eqtype.eq_op IntMap.coq_IntSet_eqType (unsafeCoerce lk1) (unsafeCoerce lk2)) ((Prelude.&&) (Eqtype.eq_op IntMap.coq_IntSet_eqType (unsafeCoerce li1) (unsafeCoerce li2)) ((Prelude.&&) (Eqtype.eq_op IntMap.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 IntMap.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 IntMap.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 IntMap.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 IntMap.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 = Yoneda.iso_to (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict))) (Monad.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 IntMap.emptyIntSet IntMap.emptyIntSet IntMap.emptyIntSet IntMap.emptyIntSet ((Prelude.+) idx (Ssrnat.double (Data.List.length opsb))) idx} in case Lib.forFold ((,) idx liveSet) ((Prelude.++) opsb ((Prelude.++) opsm opse)) (\acc0 o -> case acc0 of { (,) lastIdx liveSet1 -> (,) ((Prelude.succ) ((Prelude.succ) lastIdx)) (case Lib.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 = Lib.forFold liveSet1 inputs (\liveSet2 v -> case Blocks.varId maxReg v of { Prelude.Left p0 -> liveSet2; Prelude.Right vid -> case Prelude.not (IntMap.coq_IntSet_member vid (blockLiveKill liveSet2)) of { Prelude.True -> Build_BlockLiveSets (IntMap.coq_IntSet_insert vid (blockLiveGen liveSet2)) (blockLiveKill liveSet2) (blockLiveIn liveSet2) (blockLiveOut liveSet2) (blockFirstOpId liveSet2) lastIdx; Prelude.False -> liveSet2}})} in let { liveSet3 = Lib.forFold liveSet2 others (\liveSet3 v -> case Blocks.varId maxReg v of { Prelude.Left p0 -> liveSet3; Prelude.Right vid -> Build_BlockLiveSets (blockLiveGen liveSet3) (IntMap.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 -> Monad.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 = Yoneda.iso_to (Yoneda.coq_Yoneda_lemma (Monad.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 = Lib.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) (IntMap.coq_IntSet_union (blockLiveOut liveSet2) (blockLiveIn sux)) (blockFirstOpId liveSet2) (blockLastOpId liveSet2); Prelude.Nothing -> liveSet2})} in Monad.pure (unsafeCoerce (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict))) (IntMap.coq_IntMap_insert bid (Build_BlockLiveSets (blockLiveGen liveSet2) (blockLiveKill liveSet2) (IntMap.coq_IntSet_union (IntMap.coq_IntSet_difference (blockLiveOut liveSet2) (blockLiveKill liveSet2)) (blockLiveGen liveSet2)) (blockLiveOut liveSet2) (blockFirstOpId liveSet2) (blockLastOpId liveSet2)) liveSets1)) (unsafeCoerce (\_ -> Blocks.blockSuccessors mDict binfo b)); Prelude.Nothing -> Monad.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)) (\_ -> Monad.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 -> Monad.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