{-# OPTIONS_GHC -cpp -fglasgow-exts #-} {- 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.UsePos as UsePos import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Ssrbool as Ssrbool import qualified LinearScan.Ssrnat as Ssrnat --unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base unsafeCoerce = GHC.Base.unsafeCoerce# #else -- HUGS import qualified LinearScan.IOExts as IOExts 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 -> (Blocks.BlockInfo a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> IntMap.IntMap BlockLiveSets computeLocalLiveSets maxReg binfo oinfo blocks = Prelude.snd (Lib.forFold ((,) ((Prelude.succ) 0) IntMap.emptyIntMap) blocks (\acc b -> case acc of { (,) idx m -> case Blocks.blockOps 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 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 -> (,) lastIdx' (IntMap.coq_IntMap_insert (Blocks.blockId binfo b) liveSet3 m)}}}})) computeGlobalLiveSets :: (Blocks.BlockInfo a1 a2 a3 a4) -> ([] a1) -> (IntMap.IntMap BlockLiveSets) -> IntMap.IntMap BlockLiveSets computeGlobalLiveSets binfo blocks liveSets = Lib.forFoldr liveSets blocks (\b liveSets1 -> let {bid = Blocks.blockId binfo b} in case IntMap.coq_IntMap_lookup bid liveSets1 of { Prelude.Just liveSet -> let { liveSet2 = Lib.forFold liveSet (Blocks.blockSuccessors binfo b) (\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 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; Prelude.Nothing -> liveSets1}) computeGlobalLiveSetsRecursively :: (Blocks.BlockInfo a1 a2 a3 a4) -> ([] a1) -> (IntMap.IntMap BlockLiveSets) -> IntMap.IntMap BlockLiveSets computeGlobalLiveSetsRecursively binfo blocks liveSets = let { go n previous = (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1)) (\_ -> previous) (\n0 -> let {computed = computeGlobalLiveSets binfo blocks previous} in case Eqtype.eq_op (IntMap.coq_IntMap_eqType coq_BlockLiveSets_eqType) (unsafeCoerce previous) (unsafeCoerce computed) of { Prelude.True -> computed; Prelude.False -> go n0 computed}) n} in go (Data.List.length blocks) liveSets