{-# 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)))