{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}

module LinearScan.Assign 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.Lens as Lens
import qualified LinearScan.Lib as Lib
import qualified LinearScan.LiveSets as LiveSets
import qualified LinearScan.Monad as Monad
import qualified LinearScan.Resolve as Resolve
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.Seq as Seq
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

data AllocState =
   Build_AllocState ([] (Prelude.Maybe Prelude.Int)) (IntMap.IntMap
                                                     (Prelude.Maybe PhysReg))

newAllocState :: Prelude.Int -> AllocState
newAllocState maxReg =
  Build_AllocState (Data.List.replicate maxReg Prelude.Nothing)
    IntMap.emptyIntMap

data AllocError =
   Build_AllocError Prelude.Int (Prelude.Maybe PhysReg) (Prelude.Maybe
                                                        PhysReg) Blocks.BlockId

data AssnStateInfo =
   Build_AssnStateInfo Blocks.OpId Blocks.OpId Blocks.OpId AllocState 
 (IntMap.IntMap AllocState) (IntMap.IntMap AllocState) ([] AllocError)

assnOpId :: Prelude.Int -> AssnStateInfo -> Blocks.OpId
assnOpId maxReg a =
  case a of {
   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0
    assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 -> assnOpId0}

assnBlockBeg :: Prelude.Int -> AssnStateInfo -> Blocks.OpId
assnBlockBeg maxReg a =
  case a of {
   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0
    assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 -> assnBlockBeg0}

assnBlockEnd :: Prelude.Int -> AssnStateInfo -> Blocks.OpId
assnBlockEnd maxReg a =
  case a of {
   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0
    assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 -> assnBlockEnd0}

assnAllocState :: Prelude.Int -> AssnStateInfo -> AllocState
assnAllocState maxReg a =
  case a of {
   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0
    assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 -> assnAllocState0}

assnBlockEntryAllocs :: Prelude.Int -> AssnStateInfo -> IntMap.IntMap
                        AllocState
assnBlockEntryAllocs maxReg a =
  case a of {
   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0
    assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 ->
    assnBlockEntryAllocs0}

assnBlockExitAllocs :: Prelude.Int -> AssnStateInfo -> IntMap.IntMap
                       AllocState
assnBlockExitAllocs maxReg a =
  case a of {
   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0
    assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 ->
    assnBlockExitAllocs0}

assnErrors :: Prelude.Int -> AssnStateInfo -> [] AllocError
assnErrors maxReg a =
  case a of {
   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0
    assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 -> assnErrors0}

newAssnStateInfo :: Prelude.Int -> AssnStateInfo
newAssnStateInfo maxReg =
  Build_AssnStateInfo ((Prelude.succ) 0) ((Prelude.succ) 0) ((Prelude.succ)
    0) (newAllocState maxReg) IntMap.emptyIntMap IntMap.emptyIntMap []

_assnOpId :: Prelude.Int -> (Monad.Functor a1) -> (Blocks.OpId -> a1) ->
             AssnStateInfo -> a1
_assnOpId maxReg h f s =
  Monad.fmap h (\x -> Build_AssnStateInfo x (assnBlockBeg maxReg s)
    (assnBlockEnd maxReg s) (assnAllocState maxReg s)
    (assnBlockEntryAllocs maxReg s) (assnBlockExitAllocs maxReg s)
    (assnErrors maxReg s)) (f (assnOpId maxReg s))

_assnBlockBeg :: Prelude.Int -> (Monad.Functor a1) -> (Blocks.OpId -> a1) ->
                 AssnStateInfo -> a1
_assnBlockBeg maxReg h f s =
  Monad.fmap h (\x -> Build_AssnStateInfo (assnOpId maxReg s) x
    (assnBlockEnd maxReg s) (assnAllocState maxReg s)
    (assnBlockEntryAllocs maxReg s) (assnBlockExitAllocs maxReg s)
    (assnErrors maxReg s)) (f (assnBlockBeg maxReg s))

_assnBlockEnd :: Prelude.Int -> (Monad.Functor a1) -> (Blocks.OpId -> a1) ->
                 AssnStateInfo -> a1
_assnBlockEnd maxReg h f s =
  Monad.fmap h (\x -> Build_AssnStateInfo (assnOpId maxReg s)
    (assnBlockBeg maxReg s) x (assnAllocState maxReg s)
    (assnBlockEntryAllocs maxReg s) (assnBlockExitAllocs maxReg s)
    (assnErrors maxReg s)) (f (assnBlockEnd maxReg s))

type AssnState mType a = Monad.StateT AssnStateInfo mType a

generateMoves :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo a3 
                 a1 a2) -> ([] Resolve.ResolvingMove) -> a3
generateMoves maxReg mDict oinfo moves =
  Monad.forFoldrM mDict [] moves (\mv acc ->
    let {
     k = (Prelude..)
           (Monad.fmap (Monad.is_functor (Monad.is_applicative mDict)) (\x ->
             Prelude.Just x))
           (Yoneda.iso_to
             (Yoneda.coq_Yoneda_lemma
               (Monad.is_functor (Monad.is_applicative mDict))))}
    in
    Monad.bind mDict (\mops ->
      Monad.pure (Monad.is_applicative mDict)
        (case mops of {
          Prelude.Just ops -> (Prelude.++) ops acc;
          Prelude.Nothing -> acc}))
      (case mv of {
        Resolve.Move sreg dreg ->
         k (\_ -> Blocks.moveOp maxReg mDict oinfo sreg dreg);
        Resolve.Swap sreg dreg ->
         k (\_ -> Blocks.swapOp maxReg mDict oinfo sreg dreg);
        Resolve.Spill sreg vid ->
         k (\_ -> Blocks.saveOp maxReg mDict oinfo sreg (Prelude.Just vid));
        Resolve.Restore vid dreg ->
         k (\_ ->
           Blocks.restoreOp maxReg mDict oinfo (Prelude.Just vid) dreg);
        Resolve.Nop ->
         Monad.pure (Monad.is_applicative mDict) Prelude.Nothing}))

varAllocs :: Prelude.Int -> Prelude.Int -> ([] Allocate.Allocation) ->
             Blocks.VarInfo -> [] ((,) Blocks.VarId PhysReg)
varAllocs maxReg opid allocs v =
  case Blocks.varId maxReg v of {
   Prelude.Left p -> [];
   Prelude.Right vid ->
    Prelude.map (\x -> (,) vid x)
      (Lib.catMaybes
        (Prelude.map (\i -> Allocate.intReg maxReg i)
          (Prelude.filter (\i ->
            let {int = Allocate.intVal maxReg i} in
            (Prelude.&&)
              (Eqtype.eq_op Ssrnat.nat_eqType
                (unsafeCoerce (Interval.ivar int)) (unsafeCoerce vid))
              ((Prelude.&&) ((Prelude.<=) (Interval.ibeg int) opid)
                (case Blocks.varKind maxReg v of {
                  UsePos.Input -> (Prelude.<=) opid (Interval.iend int);
                  _ -> (Prelude.<=) ((Prelude.succ) opid) (Interval.iend int)})))
            allocs)))}

setAllocations :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo a3 
                  a1 a2) -> ([] Allocate.Allocation) -> a1 -> AssnState 
                  a3 ([] a2)
setAllocations maxReg mDict oinfo allocs op =
  Monad.bind (Monad.coq_StateT_Monad mDict) (\assn ->
    let {opid = assnOpId maxReg assn} in
    let {vars = Blocks.opRefs maxReg mDict oinfo op} in
    let {
     regs = Monad.concat (Prelude.map (varAllocs maxReg opid allocs) vars)}
    in
    Monad.bind (Monad.coq_StateT_Monad mDict) (\ops ->
      Monad.bind (Monad.coq_StateT_Monad mDict) (\transitions ->
        Monad.bind (Monad.coq_StateT_Monad mDict) (\x ->
          Monad.pure (Monad.coq_StateT_Applicative mDict)
            ((Prelude.++) ops transitions))
          (Monad.modifyT (Monad.is_applicative mDict)
            (Lens.set (\_ -> _assnOpId maxReg) ((Prelude.succ)
              ((Prelude.succ) opid)))))
        (case (Prelude.&&) ((Prelude.<=) (assnBlockBeg maxReg assn) opid)
                ((Prelude.<=) ((Prelude.succ) opid)
                  (assnBlockEnd maxReg assn)) of {
          Prelude.True ->
           Monad.lift mDict
             (generateMoves maxReg mDict oinfo
               (Resolve.determineMoves maxReg
                 (Resolve.resolvingMoves maxReg allocs opid ((Prelude.succ)
                   ((Prelude.succ) opid)))));
          Prelude.False -> Monad.pure (Monad.coq_StateT_Applicative mDict) []}))
      (Monad.lift mDict
        (Yoneda.iso_to
          (Yoneda.coq_Yoneda_lemma
            (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->
          Blocks.applyAllocs maxReg mDict oinfo op regs))))
    (Monad.getT (Monad.is_applicative mDict))

resolveMappings :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo 
                   a3 a1 a2) -> Prelude.Int -> ([] a2) -> (IntMap.IntMap
                   ((,) Graph.Graph Graph.Graph)) -> a3
resolveMappings maxReg mDict oinfo bid opsm mappings =
  case IntMap.coq_IntMap_lookup bid mappings of {
   Prelude.Just graphs ->
    case graphs of {
     (,) gbeg gend ->
      Monad.bind mDict (\bmoves ->
        Monad.bind mDict (\emoves ->
          Monad.pure (Monad.is_applicative mDict)
            ((Prelude.++) bmoves ((Prelude.++) opsm emoves)))
          (generateMoves maxReg mDict oinfo
            (Prelude.map (Resolve.moveFromGraph maxReg)
              (Graph.topsort
                (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
                  Ssrnat.nat_eqType) gend))))
        (generateMoves maxReg mDict oinfo
          (Prelude.map (Resolve.moveFromGraph maxReg)
            (Graph.topsort
              (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
                Ssrnat.nat_eqType) gbeg)))};
   Prelude.Nothing -> Monad.pure (Monad.is_applicative mDict) opsm}

considerOps :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 
               a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([]
               Allocate.Allocation) -> (IntMap.IntMap LiveSets.BlockLiveSets)
               -> (IntMap.IntMap Resolve.BlockMoves) -> ([] a1) -> AssnState
               a5 ([] a2)
considerOps maxReg mDict binfo oinfo allocs liveSets mappings =
  Monad.mapM (Monad.coq_StateT_Applicative mDict) (\blk ->
    case Blocks.blockOps mDict binfo blk of {
     (,) p opse ->
      case p of {
       (,) opsb opsm ->
        Monad.bind (Monad.coq_StateT_Monad mDict) (\x ->
          let {k = setAllocations maxReg mDict oinfo allocs} in
          Monad.bind (Monad.coq_StateT_Monad mDict) (\opsb' ->
            Monad.bind (Monad.coq_StateT_Monad mDict) (\opsm' ->
              Monad.bind (Monad.coq_StateT_Monad mDict) (\opse' ->
                Monad.bind (Monad.coq_StateT_Monad mDict) (\bid ->
                  Monad.bind (Monad.coq_StateT_Monad mDict) (\opsm'' ->
                    case opsb' of {
                     [] ->
                      case opse' of {
                       [] ->
                        Monad.pure (Monad.coq_StateT_Applicative mDict)
                          (Blocks.setBlockOps mDict binfo blk [] opsm'' []);
                       (:) e es ->
                        Monad.pure (Monad.coq_StateT_Applicative mDict)
                          (Blocks.setBlockOps mDict binfo blk []
                            ((Prelude.++) opsm'' (Seq.belast e es)) ((:)
                            (Seq.last e es) []))};
                     (:) b bs ->
                      case opse' of {
                       [] ->
                        Monad.pure (Monad.coq_StateT_Applicative mDict)
                          (Blocks.setBlockOps mDict binfo blk ((:) b [])
                            ((Prelude.++) bs opsm'') []);
                       (:) e es ->
                        Monad.pure (Monad.coq_StateT_Applicative mDict)
                          (Blocks.setBlockOps mDict binfo blk ((:) b [])
                            ((Prelude.++) bs
                              ((Prelude.++) opsm'' (Seq.belast e es))) ((:)
                            (Seq.last e es) []))}})
                    (Monad.lift mDict
                      (resolveMappings maxReg mDict oinfo bid opsm' mappings)))
                  (Monad.lift mDict
                    (Yoneda.iso_to
                      (Yoneda.coq_Yoneda_lemma
                        (Monad.is_functor (Monad.is_applicative mDict)))
                      (\_ -> Blocks.blockId mDict binfo blk))))
                (Monad.concatMapM (Monad.coq_StateT_Applicative mDict) k
                  opse))
              (Monad.concatMapM (Monad.coq_StateT_Applicative mDict) k opsm))
            (Monad.concatMapM (Monad.coq_StateT_Applicative mDict) k opsb))
          (Monad.modifyT (Monad.is_applicative mDict) (\assn ->
            let {opid = Lens.view (\_ -> _assnOpId maxReg) assn} in
            Lens.set (\_ -> _assnBlockEnd maxReg)
              ((Prelude.+) opid
                (Ssrnat.double
                  ((Prelude.+) (Data.List.length opsb)
                    (Data.List.length opsm))))
              (Lens.set (\_ -> _assnBlockBeg maxReg)
                ((Prelude.+) opid (Ssrnat.double (Data.List.length opsb)))
                assn)))}})

assignRegNum :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo 
                a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([]
                Allocate.Allocation) -> (IntMap.IntMap
                LiveSets.BlockLiveSets) -> (IntMap.IntMap Resolve.BlockMoves)
                -> ([] a1) -> a5
assignRegNum maxReg mDict binfo oinfo allocs liveSets mappings blocks =
  Monad.fmap (Monad.is_functor (Monad.is_applicative mDict)) Prelude.fst
    (considerOps maxReg mDict binfo oinfo allocs liveSets mappings blocks
      (newAssnStateInfo maxReg))