{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -} module LinearScan.Resolve 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.Allocate as Allocate import qualified LinearScan.Blocks as Blocks import qualified LinearScan.Graph as Graph import qualified LinearScan.IntMap as IntMap import qualified LinearScan.Interval as Interval import qualified LinearScan.Lib as Lib import qualified LinearScan.LiveSets as LiveSets 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.Fintype as Fintype 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 type PhysReg = Prelude.Int type RawResolvingMove = (,) (Prelude.Maybe PhysReg) (Prelude.Maybe PhysReg) data ResolvingMove = Move PhysReg PhysReg | Swap PhysReg PhysReg | Spill PhysReg Blocks.VarId | Restore Blocks.VarId PhysReg | Nop prepareForGraph :: Prelude.Int -> Eqtype.Equality__Coq_sort -> RawResolvingMove -> (,) (Prelude.Maybe Eqtype.Equality__Coq_sort) (Prelude.Maybe Eqtype.Equality__Coq_sort) prepareForGraph maxReg vid x = case x of { (,) o o0 -> case o of { Prelude.Just x0 -> case o0 of { Prelude.Just y -> (,) (Prelude.Just (unsafeCoerce (Prelude.Left x0))) (Prelude.Just (unsafeCoerce (Prelude.Left y))); Prelude.Nothing -> (,) (Prelude.Just (unsafeCoerce (Prelude.Left x0))) (Prelude.Just (unsafeCoerce (Prelude.Right vid)))}; Prelude.Nothing -> case o0 of { Prelude.Just y -> (,) (Prelude.Just (unsafeCoerce (Prelude.Right vid))) (Prelude.Just (unsafeCoerce (Prelude.Left y))); Prelude.Nothing -> (,) (Prelude.Just (unsafeCoerce (Prelude.Right vid))) (Prelude.Just (unsafeCoerce (Prelude.Right vid)))}}} moveFromGraph :: Prelude.Int -> ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort) (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> ResolvingMove moveFromGraph maxReg mv = case mv of { (,) o o0 -> case o of { Prelude.Just s -> case unsafeCoerce s of { Prelude.Left x -> case o0 of { Prelude.Just s0 -> case unsafeCoerce s0 of { Prelude.Left y -> Move x y; Prelude.Right y -> Spill x y}; Prelude.Nothing -> Nop}; Prelude.Right x -> case o0 of { Prelude.Just s0 -> case unsafeCoerce s0 of { Prelude.Left y -> Restore x y; Prelude.Right s1 -> Nop}; Prelude.Nothing -> Nop}}; Prelude.Nothing -> Nop}} determineMoves :: Prelude.Int -> (IntMap.IntMap RawResolvingMove) -> [] ResolvingMove determineMoves maxReg moves = let { graph = Lib.forFold (Graph.emptyGraph (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType)) (unsafeCoerce (IntMap.coq_IntMap_toList moves)) (\g mv -> Graph.addEdge (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType) (unsafeCoerce (prepareForGraph maxReg (Prelude.fst mv) (Prelude.snd mv))) g)} in Prelude.map (moveFromGraph maxReg) (Graph.topsort (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType) graph) resolvingMoves :: Prelude.Int -> ([] Allocate.Allocation) -> Prelude.Int -> Prelude.Int -> IntMap.IntMap RawResolvingMove resolvingMoves maxReg allocs from to = let { liveAtFrom = IntMap.coq_IntMap_fromList (Prelude.map (\i -> (,) (Interval.ivar (Allocate.intVal maxReg i)) i) (Prelude.filter (\i -> (Prelude.&&) ((Prelude.<=) (Interval.ibeg (Allocate.intVal maxReg i)) from) ((Prelude.<=) ((Prelude.succ) from) (Interval.iend (Allocate.intVal maxReg i)))) allocs))} in let { liveAtTo = IntMap.coq_IntMap_fromList (Prelude.map (\i -> (,) (Interval.ivar (Allocate.intVal maxReg i)) i) (Prelude.filter (\i -> let {int = Allocate.intVal maxReg i} in (Prelude.&&) ((Prelude.<=) (Interval.ibeg int) to) (case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce to) (unsafeCoerce (Interval.iend int)) of { Prelude.True -> case Interval.lastUsePos int of { Prelude.Just u -> (Prelude.<=) to (UsePos.uloc u); Prelude.Nothing -> Prelude.False}; Prelude.False -> (Prelude.<=) ((Prelude.succ) to) (Interval.iend int)})) allocs))} in IntMap.coq_IntMap_mergeWithKey (\vid x y -> case Eqtype.eq_op (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg)) (unsafeCoerce (Allocate.intReg maxReg x)) (unsafeCoerce (Allocate.intReg maxReg y)) of { Prelude.True -> Prelude.Nothing; Prelude.False -> Prelude.Just ((,) (Allocate.intReg maxReg x) (Allocate.intReg maxReg y))}) (\x -> IntMap.emptyIntMap) (\x -> IntMap.emptyIntMap) liveAtFrom liveAtTo checkBlockBoundary :: Prelude.Int -> ([] Allocate.Allocation) -> Prelude.Int -> Prelude.Bool -> LiveSets.BlockLiveSets -> LiveSets.BlockLiveSets -> IntMap.IntSet -> (IntMap.IntMap ((,) Graph.Graph Graph.Graph)) -> IntMap.IntMap ((,) Graph.Graph Graph.Graph) checkBlockBoundary maxReg allocs bid in_from from to liveIn mappings = let { select = \acc vid x -> case IntMap.coq_IntSet_member vid liveIn of { Prelude.True -> (:) ((,) vid x) acc; Prelude.False -> acc}} in let { moves = IntMap.coq_IntMap_foldlWithKey select [] (resolvingMoves maxReg allocs (LiveSets.blockLastOpId from) (LiveSets.blockFirstOpId to))} in Lib.forFold mappings (unsafeCoerce moves) (\ms mv -> let { addToGraphs = \e xs -> case xs of { (,) gbeg gend -> case in_from of { Prelude.True -> (,) gbeg (Graph.addEdge (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType) e gend); Prelude.False -> (,) (Graph.addEdge (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType) e gbeg) gend}}} in let { f = \mxs -> unsafeCoerce addToGraphs (prepareForGraph maxReg (Prelude.fst mv) (Prelude.snd mv)) (case mxs of { Prelude.Just xs -> xs; Prelude.Nothing -> (,) (Graph.emptyGraph (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType)) (Graph.emptyGraph (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType))})} in IntMap.coq_IntMap_alter ((Prelude..) (\x -> Prelude.Just x) f) bid ms) type BlockMoves = (,) Graph.Graph Graph.Graph resolveDataFlow :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> ([] Allocate.Allocation) -> ([] a1) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> a5 resolveDataFlow maxReg mDict binfo allocs blocks liveSets = Yoneda.iso_to (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict))) (Monad.forFoldM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) IntMap.emptyIntMap blocks (\mappings b -> Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\bid -> case IntMap.coq_IntMap_lookup bid liveSets of { Prelude.Just from -> Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\suxs -> let { in_from = (Prelude.<=) (Data.List.length suxs) ((Prelude.succ) 0)} in Monad.pure (unsafeCoerce (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict))) (Lib.forFold mappings suxs (\ms s_bid -> case IntMap.coq_IntMap_lookup s_bid liveSets of { Prelude.Just to -> let { key = case in_from of { Prelude.True -> bid; Prelude.False -> s_bid}} in checkBlockBoundary maxReg allocs key in_from from to (LiveSets.blockLiveIn to) ms; Prelude.Nothing -> ms}))) (unsafeCoerce (\_ -> Blocks.blockSuccessors mDict binfo b)); Prelude.Nothing -> Monad.pure (unsafeCoerce (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict))) mappings}) (\_ -> Blocks.blockId mDict binfo b)))