{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -} 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 -- 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 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