{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -} module LinearScan.Loops 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.List1 as List1 import qualified LinearScan.Monad as Monad import qualified LinearScan.State as State import qualified LinearScan.State0 as State0 import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Seq as Seq 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 data LoopState = Build_LoopState IntSet.IntSet IntSet.IntSet ([] Blocks.BlockId) IntSet.IntSet (IntMap.IntMap IntSet.IntSet) (IntMap.IntMap IntSet.IntSet) (IntMap.IntMap IntSet.IntSet) (IntMap.IntMap ((,) Prelude.Int Prelude.Int)) activeBlocks :: LoopState -> IntSet.IntSet activeBlocks l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> activeBlocks0} visitedBlocks :: LoopState -> IntSet.IntSet visitedBlocks l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> visitedBlocks0} loopHeaderBlocks :: LoopState -> [] Blocks.BlockId loopHeaderBlocks l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> loopHeaderBlocks0} loopEndBlocks :: LoopState -> IntSet.IntSet loopEndBlocks l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> loopEndBlocks0} forwardBranches :: LoopState -> IntMap.IntMap IntSet.IntSet forwardBranches l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> forwardBranches0} backwardBranches :: LoopState -> IntMap.IntMap IntSet.IntSet backwardBranches l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> backwardBranches0} loopIndices :: LoopState -> IntMap.IntMap IntSet.IntSet loopIndices l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> loopIndices0} loopDepths :: LoopState -> IntMap.IntMap ((,) Prelude.Int Prelude.Int) loopDepths l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> loopDepths0} emptyLoopState :: LoopState emptyLoopState = Build_LoopState IntSet.emptyIntSet IntSet.emptyIntSet [] IntSet.emptyIntSet IntMap.emptyIntMap IntMap.emptyIntMap IntMap.emptyIntMap IntMap.emptyIntMap modifyActiveBlocks :: (IntSet.IntSet -> IntSet.IntSet) -> State.State LoopState () modifyActiveBlocks f = State.modify (\st -> Build_LoopState (f (activeBlocks st)) (visitedBlocks st) (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st) (backwardBranches st) (loopIndices st) (loopDepths st)) modifyVisitedBlocks :: (IntSet.IntSet -> IntSet.IntSet) -> State.State LoopState () modifyVisitedBlocks f = State.modify (\st -> Build_LoopState (activeBlocks st) (f (visitedBlocks st)) (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st) (backwardBranches st) (loopIndices st) (loopDepths st)) modifyLoopHeaderBlocks :: (([] Blocks.BlockId) -> [] Blocks.BlockId) -> State.State LoopState () modifyLoopHeaderBlocks f = State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st) (f (loopHeaderBlocks st)) (loopEndBlocks st) (forwardBranches st) (backwardBranches st) (loopIndices st) (loopDepths st)) modifyLoopEndBlocks :: (IntSet.IntSet -> IntSet.IntSet) -> State.State LoopState () modifyLoopEndBlocks f = State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st) (loopHeaderBlocks st) (f (loopEndBlocks st)) (forwardBranches st) (backwardBranches st) (loopIndices st) (loopDepths st)) modifyForwardBranches :: ((IntMap.IntMap IntSet.IntSet) -> IntMap.IntMap IntSet.IntSet) -> State.State LoopState () modifyForwardBranches f = State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st) (loopHeaderBlocks st) (loopEndBlocks st) (f (forwardBranches st)) (backwardBranches st) (loopIndices st) (loopDepths st)) modifyBackwardBranches :: ((IntMap.IntMap IntSet.IntSet) -> IntMap.IntMap IntSet.IntSet) -> State.State LoopState () modifyBackwardBranches f = State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st) (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st) (f (backwardBranches st)) (loopIndices st) (loopDepths st)) setLoopIndices :: (IntMap.IntMap IntSet.IntSet) -> State.State LoopState () setLoopIndices indices = State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st) (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st) (backwardBranches st) indices (loopDepths st)) setLoopDepths :: (IntMap.IntMap ((,) Prelude.Int Prelude.Int)) -> State.State LoopState () setLoopDepths depths = State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st) (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st) (backwardBranches st) (loopIndices st) depths) addReference :: Prelude.Int -> Prelude.Int -> (IntMap.IntMap IntSet.IntSet) -> IntMap.IntMap IntSet.IntSet addReference i x = IntMap.coq_IntMap_alter (\macc -> case macc of { Prelude.Just acc -> Prelude.Just (IntSet.coq_IntSet_insert x acc); Prelude.Nothing -> Prelude.Just (IntSet.coq_IntSet_singleton x)}) i pathToLoopHeader :: Blocks.BlockId -> Prelude.Int -> LoopState -> Prelude.Maybe IntSet.IntSet pathToLoopHeader blk header st = let { go = let { go fuel visited b = (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1)) (\_ -> (,) visited Prelude.Nothing) (\n -> let {visited' = IntSet.coq_IntSet_insert b visited} in let { forwardPreds = case IntMap.coq_IntMap_lookup b (forwardBranches st) of { Prelude.Just preds -> IntSet.coq_IntSet_toList preds; Prelude.Nothing -> []}} in let { backwardPreds = case IntMap.coq_IntMap_lookup b (backwardBranches st) of { Prelude.Just preds -> IntSet.coq_IntSet_toList preds; Prelude.Nothing -> []}} in let {preds = (Prelude.++) forwardPreds backwardPreds} in List1.forFold ((,) visited' (Prelude.Just (IntSet.coq_IntSet_singleton b))) (unsafeCoerce preds) (\mxs pred -> case mxs of { (,) vis o -> case o of { Prelude.Just xs -> case Eqtype.eq_op Ssrnat.nat_eqType pred (unsafeCoerce header) of { Prelude.True -> (,) vis (Prelude.Just (IntSet.coq_IntSet_union xs (IntSet.coq_IntSet_singleton (unsafeCoerce pred)))); Prelude.False -> case IntSet.coq_IntSet_member (unsafeCoerce pred) vis of { Prelude.True -> (,) vis (Prelude.Just xs); Prelude.False -> case unsafeCoerce go n vis pred of { (,) vis' o0 -> case o0 of { Prelude.Just ys -> (,) vis' (Prelude.Just (IntSet.coq_IntSet_union xs ys)); Prelude.Nothing -> (,) vis Prelude.Nothing}}}}; Prelude.Nothing -> mxs}})) fuel} in go} in Prelude.snd (go (IntSet.coq_IntSet_size (visitedBlocks st)) IntSet.emptyIntSet blk) computeLoopDepths :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> (IntMap.IntMap a1) -> State.State LoopState () computeLoopDepths mDict binfo bs = Monad.bind (State0.coq_StateT_Monad (unsafeCoerce Identity.coq_Identity_Monad)) (\st -> let { m = List1.forFold IntMap.emptyIntMap (IntSet.coq_IntSet_toList (loopEndBlocks st)) (\m endBlock -> case IntMap.coq_IntMap_lookup endBlock bs of { Prelude.Just b -> let {suxs = Blocks.blockSuccessors mDict binfo b} in List1.forFold m (unsafeCoerce suxs) (\m' sux -> let {headers = loopHeaderBlocks st} in let { loopIndex = Seq.find (\x -> Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce x) sux) headers} in case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce loopIndex) (unsafeCoerce (Data.List.length headers)) of { Prelude.True -> m'; Prelude.False -> let {mres = pathToLoopHeader endBlock (unsafeCoerce sux) st} in case mres of { Prelude.Just path -> List1.forFold m' (IntSet.coq_IntSet_toList path) (\m'' blk -> addReference loopIndex blk m''); Prelude.Nothing -> m'}}); Prelude.Nothing -> m})} in let { f = \acc loopIndex refs -> IntSet.coq_IntSet_forFold acc refs (\m' blk -> let { f = \mx -> case mx of { Prelude.Just y -> case y of { (,) idx depth -> Prelude.Just ((,) (Prelude.min idx loopIndex) ((Prelude.succ) depth))}; Prelude.Nothing -> Prelude.Just ((,) loopIndex ((Prelude.succ) 0))}} in IntMap.coq_IntMap_alter f blk m')} in State0.liftStateT (unsafeCoerce Identity.coq_Identity_Monad) (Monad.bind (unsafeCoerce State.coq_State_Monad) (\x -> setLoopDepths (IntMap.coq_IntMap_foldlWithKey f IntMap.emptyIntMap m)) (setLoopIndices m))) (unsafeCoerce State.get) computeVarReferences :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> LoopState -> IntMap.IntMap IntSet.IntSet computeVarReferences maxReg mDict binfo oinfo bs st = List1.forFold IntMap.emptyIntMap bs (\acc b -> let {bid = Blocks.blockId mDict binfo b} in let { g = \acc1 loopIndex blks -> case Prelude.not (IntSet.coq_IntSet_member bid blks) of { Prelude.True -> acc1; Prelude.False -> case Blocks.blockOps mDict binfo b of { (,) p zs -> case p of { (,) xs ys -> List1.forFold acc1 ((Prelude.++) xs ((Prelude.++) ys zs)) (\acc2 op -> List1.forFold acc2 (Blocks.opRefs maxReg mDict oinfo op) (\acc3 v -> case Blocks.varId maxReg v of { Prelude.Left p0 -> acc3; Prelude.Right vid -> addReference loopIndex vid acc3}))}}}} in IntMap.coq_IntMap_foldlWithKey g acc (loopIndices st)) findLoopEnds :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> (IntMap.IntMap a1) -> State.State LoopState () findLoopEnds mDict binfo bs = let { go = let { go n b = (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1)) (\_ -> Applicative.pure State.coq_State_Applicative ()) (\n0 -> let {bid = Blocks.blockId mDict binfo b} in Monad.bind State.coq_State_Monad (\x -> Monad.bind State.coq_State_Monad (\x0 -> let {suxs = Blocks.blockSuccessors mDict binfo b} in Monad.bind State.coq_State_Monad (\x1 -> unsafeCoerce (modifyActiveBlocks (IntSet.coq_IntSet_delete bid))) (Monad.forM_ State.coq_State_Monad suxs (\sux -> Monad.bind State.coq_State_Monad (\active -> Monad.bind State.coq_State_Monad (\x1 -> Monad.bind State.coq_State_Monad (\visited -> case IntSet.coq_IntSet_member sux visited of { Prelude.True -> Applicative.pure State.coq_State_Applicative (); Prelude.False -> case IntMap.coq_IntMap_lookup sux bs of { Prelude.Just x2 -> go n0 x2; Prelude.Nothing -> Applicative.pure State.coq_State_Applicative ()}}) (State.gets (unsafeCoerce visitedBlocks))) (case IntSet.coq_IntSet_member sux active of { Prelude.True -> Monad.bind State.coq_State_Monad (\x1 -> Monad.bind State.coq_State_Monad (\x2 -> unsafeCoerce (modifyBackwardBranches (addReference sux bid))) (unsafeCoerce (modifyLoopEndBlocks (IntSet.coq_IntSet_insert bid)))) (unsafeCoerce (modifyLoopHeaderBlocks (\l -> case Prelude.not (Ssrbool.in_mem (unsafeCoerce sux) (Ssrbool.mem (Seq.seq_predType Ssrnat.nat_eqType) (unsafeCoerce l))) of { Prelude.True -> (:) sux l; Prelude.False -> l}))); Prelude.False -> unsafeCoerce (modifyForwardBranches (addReference sux bid))})) (State.gets (unsafeCoerce activeBlocks))))) (unsafeCoerce (modifyActiveBlocks (IntSet.coq_IntSet_insert bid)))) (unsafeCoerce (modifyVisitedBlocks (IntSet.coq_IntSet_insert bid)))) n} in go} in case IntMap.coq_IntMap_toList bs of { [] -> Applicative.pure (unsafeCoerce State.coq_State_Applicative) (); (:) p l -> case p of { (,) n b -> unsafeCoerce go (IntMap.coq_IntMap_size bs) b}} computeBlockOrder :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> ([] a1) -> a5 computeBlockOrder mDict binfo blocks = case blocks of { [] -> Applicative.pure (Monad.is_applicative mDict) ((,) emptyLoopState []); (:) b bs -> let { keys = Prelude.map (\x -> (,) (Blocks.blockId mDict binfo x) x) blocks} in let {blockMap = IntMap.coq_IntMap_fromList keys} in case findLoopEnds mDict binfo blockMap emptyLoopState of { (,) u st0 -> Monad.bind mDict (\blocks' -> let { keys' = Prelude.map (\x -> (,) (Blocks.blockId mDict binfo x) x) blocks'} in let {blockMap' = IntMap.coq_IntMap_fromList keys'} in let {z' = findLoopEnds mDict binfo blockMap' emptyLoopState} in case z' of { (,) u0 st1 -> case blocks' of { [] -> Applicative.pure (Monad.is_applicative mDict) ((,) emptyLoopState []); (:) b' bs' -> let {w = computeLoopDepths mDict binfo blockMap st1} in case w of { (,) u1 st2 -> let { isHeavier = \x y -> let {x_id = Blocks.blockId mDict binfo x} in let {y_id = Blocks.blockId mDict binfo y} in let { x_depth = case IntMap.coq_IntMap_lookup x_id (loopDepths st2) of { Prelude.Just p -> case p of { (,) idx depth -> depth}; Prelude.Nothing -> 0}} in let { y_depth = case IntMap.coq_IntMap_lookup y_id (loopDepths st2) of { Prelude.Just p -> case p of { (,) idx depth -> depth}; Prelude.Nothing -> 0}} in (Prelude.<=) ((Prelude.succ) y_depth) x_depth} in let { go = let { go n branches work_list = (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1)) (\_ -> []) (\n0 -> case work_list of { [] -> []; (:) w0 ws -> let {bid = Blocks.blockId mDict binfo w0} in let {suxs = Blocks.blockSuccessors mDict binfo w0} in let { x = List1.forFold ((,) branches ws) suxs (\acc sux -> case acc of { (,) branches' ws' -> let { insertion = case IntMap.coq_IntMap_lookup sux blockMap' of { Prelude.Just s -> List1.insert isHeavier s ws'; Prelude.Nothing -> ws'}} in case IntMap.coq_IntMap_lookup sux branches' of { Prelude.Just incs -> (,) (IntMap.coq_IntMap_insert sux (IntSet.coq_IntSet_delete bid incs) branches') (case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (IntSet.coq_IntSet_size incs)) (unsafeCoerce ((Prelude.succ) 0)) of { Prelude.True -> insertion; Prelude.False -> ws'}); Prelude.Nothing -> (,) branches' insertion}})} in case x of { (,) branches' ws' -> (:) w0 (go n0 branches' ws')}}) n} in go} in let { res = go (Data.List.length blocks') (forwardBranches st2) ((:) b' [])} in Applicative.pure (Monad.is_applicative mDict) ((,) st2 res)}}}) (Monad.forFoldrM mDict [] blocks (\b0 rest -> let {suxs = Blocks.blockSuccessors mDict binfo b0} in case (Prelude.<=) (Data.List.length suxs) ((Prelude.succ) 0) of { Prelude.True -> Applicative.pure (Monad.is_applicative mDict) ((:) b0 rest); Prelude.False -> Functor.fmap (Applicative.is_functor (Monad.is_applicative mDict)) (\x -> case x of { (,) b' rest' -> (:) b' rest'}) (Monad.forFoldrM mDict ((,) b0 rest) suxs (\sux x -> case x of { (,) b' rest' -> let { fsz = case IntMap.coq_IntMap_lookup sux (forwardBranches st0) of { Prelude.Just fwds -> IntSet.coq_IntSet_size fwds; Prelude.Nothing -> 0}} in let { bsz = case IntMap.coq_IntMap_lookup sux (backwardBranches st0) of { Prelude.Just bwds -> IntSet.coq_IntSet_size bwds; Prelude.Nothing -> 0}} in case (Prelude.<=) ((Prelude.+) fsz bsz) ((Prelude.succ) 0) of { Prelude.True -> Applicative.pure (Monad.is_applicative mDict) ((,) b' rest'); Prelude.False -> case IntMap.coq_IntMap_lookup sux blockMap of { Prelude.Just sux' -> Monad.bind mDict (\z -> case z of { (,) b'' sux'' -> Applicative.pure (Monad.is_applicative mDict) ((,) b'' ((:) sux'' rest'))}) (Blocks.splitCriticalEdge mDict binfo b' sux'); Prelude.Nothing -> Applicative.pure (Monad.is_applicative mDict) ((,) b' rest')}}}))}))}}