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

module LinearScan.Morph 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.Context as Context
import qualified LinearScan.Interval as Interval
import qualified LinearScan.Logic as Logic
import qualified LinearScan.ScanState as ScanState
import qualified LinearScan.Specif as Specif
import qualified LinearScan.Trace as Trace
import qualified LinearScan.Vector0 as Vector0
import qualified LinearScan.Eqtype as Eqtype
import qualified LinearScan.Fintype as Fintype
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

__ :: any
__ = Prelude.error "Logical or arity value used"

type PhysReg = Prelude.Int

data SSInfo p =
   Build_SSInfo ScanState.ScanStateDesc p

thisDesc :: Prelude.Int -> (SSInfo a1) -> ScanState.ScanStateDesc
thisDesc maxReg s =
  case s of {
   Build_SSInfo thisDesc0 thisHolds -> thisDesc0}

type SState p q a = Context.Context Trace.SSTrace (SSInfo p) (SSInfo q) a

error_ :: Prelude.Int -> ScanState.ScanStateDesc -> ([] Trace.SSTrace) ->
          SState a1 a2 a3
error_ maxReg sd err x x0 =
  Prelude.Left err

withScanStatePO :: Prelude.Int -> ScanState.ScanStateDesc ->
                   (ScanState.ScanStateDesc -> () -> SState () () a1) ->
                   SState () () a1
withScanStatePO maxReg pre f e i =
  case i of {
   Build_SSInfo thisDesc0 _ ->
    let {f0 = f thisDesc0 __} in
    let {x = Build_SSInfo thisDesc0 __} in
    let {x0 = f0 e x} in
    case x0 of {
     Prelude.Left err -> Prelude.Left err;
     Prelude.Right p -> Prelude.Right
      (case p of {
        (,) a0 s -> (,) a0
         (case s of {
           Build_SSInfo thisDesc1 _ -> Build_SSInfo thisDesc1 __})})}}

liftLen :: Prelude.Int -> ScanState.ScanStateDesc -> (ScanState.ScanStateDesc
           -> SState () () a1) -> SState () () a1
liftLen maxReg pre f e _top_assumption_ =
  let {
   _evar_0_ = \sd ->
    let {ss = Build_SSInfo sd __} in
    let {_evar_0_ = \err -> Prelude.Left err} in
    let {
     _evar_0_0 = \_top_assumption_0 ->
      let {
       _evar_0_0 = \x _top_assumption_1 ->
        let {_evar_0_0 = \sd' -> Prelude.Right ((,) x (Build_SSInfo sd' __))}
        in
        case _top_assumption_1 of {
         Build_SSInfo x0 x1 -> _evar_0_0 x0}}
      in
      case _top_assumption_0 of {
       (,) x x0 -> _evar_0_0 x x0}}
    in
    case f sd e ss of {
     Prelude.Left x -> _evar_0_ x;
     Prelude.Right x -> _evar_0_0 x}}
  in
  case _top_assumption_ of {
   Build_SSInfo x x0 -> _evar_0_ x}

strengthenHasLen :: Prelude.Int -> ScanState.ScanStateDesc ->
                    ScanState.ScanStateDesc -> Prelude.Maybe ()
strengthenHasLen maxReg pre sd =
  let {_evar_0_ = \_ -> Prelude.Nothing} in
  let {_evar_0_0 = \_a_ _l_ -> Prelude.Just __} in
  case ScanState.unhandled maxReg sd of {
   [] -> _evar_0_ __;
   (:) x x0 -> _evar_0_0 x x0}

moveUnhandledToHandled :: Prelude.Int -> ScanState.ScanStateDesc -> SState 
                          () () ()
moveUnhandledToHandled maxReg pre e x =
  case x of {
   Build_SSInfo thisDesc0 _ ->
    case thisDesc0 of {
     ScanState.Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
      unhandled0 active0 inactive0 handled0 ->
      case unhandled0 of {
       [] -> Logic.coq_False_rect;
       (:) p unhandled1 ->
        case p of {
         (,) i n ->
          let {
           _evar_0_ = \_ -> Prelude.Right ((,) () (Build_SSInfo
            (ScanState.Build_ScanStateDesc nextInterval0 intervals0
            fixedIntervals0 unhandled1 active0 inactive0 ((:) ((,)
            (Prelude.fst ((,) i n)) Prelude.Nothing) handled0)) __))}
          in
          let {
           _evar_0_0 = \_ -> Prelude.Left ((:)
            (Trace.ECannotSpillIfRegisterRequired (Prelude.id i)) e)}
          in
          case Eqtype.eq_op
                 (Eqtype.option_eqType
                   (Eqtype.sig_eqType Ssrnat.nat_eqType (\u ->
                     (Prelude.&&)
                       ((Prelude.<=)
                         (Interval.ibeg
                           ( (Vector0.vnth nextInterval0 intervals0 i)))
                         (unsafeCoerce u))
                       ((Prelude.<=) ((Prelude.succ) (unsafeCoerce u))
                         (Interval.iend
                           ( (Vector0.vnth nextInterval0 intervals0 i)))))))
                 (unsafeCoerce
                   (Interval.firstUseReqReg
                     ( (Vector0.vnth nextInterval0 intervals0 i))))
                 (unsafeCoerce Prelude.Nothing) of {
           Prelude.True -> _evar_0_ __;
           Prelude.False -> _evar_0_0 __}}}}}

moveUnhandledToActive :: Prelude.Int -> ScanState.ScanStateDesc -> PhysReg ->
                         SState () () ()
moveUnhandledToActive maxReg pre reg e x =
  case x of {
   Build_SSInfo thisDesc0 _ ->
    case thisDesc0 of {
     ScanState.Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
      unhandled0 active0 inactive0 handled0 ->
      case unhandled0 of {
       [] -> Logic.coq_False_rect;
       (:) p unhandled1 ->
        let {
         _evar_0_ = \_ -> Prelude.Right ((,) () (Build_SSInfo
          (ScanState.Build_ScanStateDesc nextInterval0 intervals0
          fixedIntervals0 unhandled1 ((:) ((,) (Prelude.fst p) reg) active0)
          inactive0 handled0) __))}
        in
        let {
         _evar_0_0 = \_ -> Prelude.Left ((:) (Trace.ERegisterAlreadyAssigned
          (Prelude.id reg)) e)}
        in
        case Prelude.not
               (Ssrbool.in_mem (unsafeCoerce reg)
                 (Ssrbool.mem
                   (Seq.seq_predType (Fintype.ordinal_eqType maxReg))
                   (unsafeCoerce (Prelude.map (\i -> Prelude.snd i) active0)))) of {
         Prelude.True -> _evar_0_ __;
         Prelude.False -> _evar_0_0 __}}}}

moveActiveToHandled :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Bool
                       -> Eqtype.Equality__Coq_sort -> Specif.Coq_sig2
                       ScanState.ScanStateDesc
moveActiveToHandled maxReg sd spilled x =
  ScanState.Build_ScanStateDesc (ScanState.nextInterval maxReg sd)
    (ScanState.intervals maxReg sd) (ScanState.fixedIntervals maxReg sd)
    (ScanState.unhandled maxReg sd)
    (unsafeCoerce
      (Seq.rem
        (Eqtype.prod_eqType
          (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd))
          (Fintype.ordinal_eqType maxReg)) x
        (unsafeCoerce (ScanState.active maxReg sd))))
    (ScanState.inactive maxReg sd) ((:) ((,) (Prelude.fst (unsafeCoerce x))
    (case spilled of {
      Prelude.True -> Prelude.Nothing;
      Prelude.False -> Prelude.Just (Prelude.snd (unsafeCoerce x))}))
    (ScanState.handled maxReg sd))

moveActiveToInactive :: Prelude.Int -> ScanState.ScanStateDesc ->
                        Eqtype.Equality__Coq_sort -> Specif.Coq_sig2
                        ScanState.ScanStateDesc
moveActiveToInactive maxReg sd x =
  ScanState.Build_ScanStateDesc (ScanState.nextInterval maxReg sd)
    (ScanState.intervals maxReg sd) (ScanState.fixedIntervals maxReg sd)
    (ScanState.unhandled maxReg sd)
    (unsafeCoerce
      (Seq.rem
        (Eqtype.prod_eqType
          (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd))
          (Fintype.ordinal_eqType maxReg)) x
        (unsafeCoerce (ScanState.active maxReg sd)))) ((:) (unsafeCoerce x)
    (ScanState.inactive maxReg sd)) (ScanState.handled maxReg sd)

moveInactiveToActive :: Prelude.Int -> ScanState.ScanStateDesc ->
                        Eqtype.Equality__Coq_sort -> Specif.Coq_sig2
                        ScanState.ScanStateDesc
moveInactiveToActive maxReg sd x =
  ScanState.Build_ScanStateDesc (ScanState.nextInterval maxReg sd)
    (ScanState.intervals maxReg sd) (ScanState.fixedIntervals maxReg sd)
    (ScanState.unhandled maxReg sd) ((:) (unsafeCoerce x)
    (ScanState.active maxReg sd))
    (unsafeCoerce
      (Seq.rem
        (Eqtype.prod_eqType
          (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd))
          (Fintype.ordinal_eqType maxReg)) x
        (unsafeCoerce (ScanState.inactive maxReg sd))))
    (ScanState.handled maxReg sd)

moveInactiveToHandled :: Prelude.Int -> ScanState.ScanStateDesc ->
                         Prelude.Bool -> Eqtype.Equality__Coq_sort ->
                         Specif.Coq_sig2 ScanState.ScanStateDesc
moveInactiveToHandled maxReg sd spilled x =
  ScanState.Build_ScanStateDesc (ScanState.nextInterval maxReg sd)
    (ScanState.intervals maxReg sd) (ScanState.fixedIntervals maxReg sd)
    (ScanState.unhandled maxReg sd) (ScanState.active maxReg sd)
    (unsafeCoerce
      (Seq.rem
        (Eqtype.prod_eqType
          (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd))
          (Fintype.ordinal_eqType maxReg)) x
        (unsafeCoerce (ScanState.inactive maxReg sd)))) ((:) ((,)
    (Prelude.fst (unsafeCoerce x))
    (case spilled of {
      Prelude.True -> Prelude.Nothing;
      Prelude.False -> Prelude.Just (Prelude.snd (unsafeCoerce x))}))
    (ScanState.handled maxReg sd))