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

module LinearScan.Verify 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.Allocate as Allocate
import qualified LinearScan.Applicative as Applicative
import qualified LinearScan.Blocks as Blocks
import qualified LinearScan.Contravariant as Contravariant
import qualified LinearScan.Functor as Functor
import qualified LinearScan.IntMap as IntMap
import qualified LinearScan.IntSet as IntSet
import qualified LinearScan.Interval as Interval
import qualified LinearScan.Lens as Lens
import qualified LinearScan.List1 as List1
import qualified LinearScan.Loops as Loops
import qualified LinearScan.Maybe as Maybe
import qualified LinearScan.Monad as Monad
import qualified LinearScan.Prelude0 as Prelude0
import qualified LinearScan.Resolve as Resolve
import qualified LinearScan.Ssr as Ssr
import qualified LinearScan.State0 as State0
import qualified LinearScan.UsePos as UsePos
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.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 UseVerifier =
   VerifyDisabled
 | VerifyEnabled
 | VerifyEnabledStrict

type RegAllocations =
  Vector0.Vec ((,) (Prelude.Maybe Blocks.VarId) (Prelude.Maybe Blocks.VarId))

data RegStateDesc =
   Build_RegStateDesc RegAllocations IntSet.IntSet

rsAllocs :: Prelude.Int -> RegStateDesc -> RegAllocations
rsAllocs maxReg r =
  case r of {
   Build_RegStateDesc rsAllocs0 rsStack0 -> rsAllocs0}

rsStack :: Prelude.Int -> RegStateDesc -> IntSet.IntSet
rsStack maxReg r =
  case r of {
   Build_RegStateDesc rsAllocs0 rsStack0 -> rsStack0}

data RegStateDescSet =
   Build_RegStateDescSet ([]
                         ((,) (Prelude.Maybe Blocks.VarId)
                         (Prelude.Maybe Blocks.VarId))) IntSet.IntSet

fromRegStateDesc :: Prelude.Int -> RegStateDesc -> RegStateDescSet
fromRegStateDesc maxReg x =
  Build_RegStateDescSet (Vector0.vec_to_seq maxReg (rsAllocs maxReg x))
    (rsStack maxReg x)

residency :: (Functor.Functor a1) -> ((Prelude.Maybe Blocks.VarId) -> a1) ->
             ((,) (Prelude.Maybe Blocks.VarId) (Prelude.Maybe Blocks.VarId))
             -> a1
residency h x x0 =
  Lens._1 h x x0

reservation :: (Functor.Functor a1) -> ((Prelude.Maybe Blocks.VarId) -> a1)
               -> ((,) (Prelude.Maybe Blocks.VarId)
               (Prelude.Maybe Blocks.VarId)) -> a1
reservation h x x0 =
  Lens._2 h x x0

newRegStateDesc :: Prelude.Int -> RegStateDesc
newRegStateDesc maxReg =
  Build_RegStateDesc
    (Vector0.vconst maxReg ((,) Prelude.Nothing Prelude.Nothing))
    IntSet.emptyIntSet

data AllocError =
   VarNotAllocated Blocks.VarId
 | VarNotResident Blocks.VarId
 | VarNotResidentForReg Blocks.VarId Prelude.Int (Prelude.Maybe Blocks.VarId) 
 Prelude.Int
 | VarNotReservedForReg Blocks.VarId Prelude.Int (Prelude.Maybe Blocks.VarId) 
 Prelude.Int
 | StackNotAllocatedForVar Blocks.VarId
 | StackAlreadyAllocatedForVar Blocks.VarId
 | PhysRegAlreadyReservedForVar Prelude.Int Blocks.VarId
 | RegAlreadyReservedToVar Prelude.Int Blocks.VarId Blocks.VarId
 | BlockWithoutPredecessors Blocks.BlockId
 | AllocationDoesNotMatch Blocks.VarId (Prelude.Maybe
                                       (Prelude.Maybe Prelude.Int)) (Prelude.Maybe
                                                                    (Prelude.Maybe
                                                                    Prelude.Int)) 
 Prelude.Int Prelude.Int
 | UnknownPredecessorBlock Blocks.BlockId Blocks.BlockId
 | LoopInResolvingMoves Resolve.ResolvingMoveSet

type RegStateSig = RegStateDesc

packRegState :: Prelude.Int -> RegStateDesc -> RegStateDesc
packRegState maxReg rd =
  rd

data VerifiedSig a =
   Build_VerifiedSig RegStateDesc (IntMap.IntMap RegStateSig) (IntMap.IntMap
                                                              RegStateSig) 
 (IntMap.IntMap ([] Resolve.ResolvingMoveSet)) (IntMap.IntMap
                                               ((,) RegStateDescSet
                                               ([] AllocError))) a

verDesc :: Prelude.Int -> (VerifiedSig a1) -> RegStateDesc
verDesc maxReg v =
  case v of {
   Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0
    verExt0 -> verDesc0}

verInit :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap RegStateSig
verInit maxReg v =
  case v of {
   Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0
    verExt0 -> verInit0}

verFinal :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap RegStateSig
verFinal maxReg v =
  case v of {
   Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0
    verExt0 -> verFinal0}

verMoves :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap
            ([] Resolve.ResolvingMoveSet)
verMoves maxReg v =
  case v of {
   Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0
    verExt0 -> verMoves0}

verErrors :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap
             ((,) RegStateDescSet ([] AllocError))
verErrors maxReg v =
  case v of {
   Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0
    verExt0 -> verErrors0}

verExt :: Prelude.Int -> (VerifiedSig a1) -> a1
verExt maxReg v =
  case v of {
   Build_VerifiedSig verDesc0 verInit0 verFinal0 verMoves0 verErrors0
    verExt0 -> verExt0}

newVerifiedSig :: Prelude.Int -> a1 -> VerifiedSig a1
newVerifiedSig maxReg i =
  Build_VerifiedSig (newRegStateDesc maxReg) IntMap.emptyIntMap
    IntMap.emptyIntMap IntMap.emptyIntMap IntMap.emptyIntMap i

_verDesc :: Prelude.Int -> (Functor.Functor a2) ->
            (Contravariant.Contravariant a2) -> (RegStateDesc -> a2) ->
            (VerifiedSig a1) -> a2
_verDesc maxReg h h0 f s =
  Functor.fmap h (Prelude0.const s) (f (verDesc maxReg s))

_verState :: Prelude.Int -> (Functor.Functor a2) -> (RegStateDesc -> a2) ->
             (VerifiedSig a1) -> a2
_verState maxReg h f s =
  Functor.fmap h (\x -> Build_VerifiedSig ( x) (verInit maxReg s)
    (verFinal maxReg s) (verMoves maxReg s) (verErrors maxReg s)
    (verExt maxReg s)) (f (verDesc maxReg s))

_verInit :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap
            RegStateSig) -> a2) -> (VerifiedSig a1) -> a2
_verInit maxReg h f s =
  Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s) x
    (verFinal maxReg s) (verMoves maxReg s) (verErrors maxReg s)
    (verExt maxReg s)) (f (verInit maxReg s))

_verFinal :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap
             RegStateSig) -> a2) -> (VerifiedSig a1) -> a2
_verFinal maxReg h f s =
  Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s)
    (verInit maxReg s) x (verMoves maxReg s) (verErrors maxReg s)
    (verExt maxReg s)) (f (verFinal maxReg s))

_verMoves :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap
             ([] Resolve.ResolvingMoveSet)) -> a2) -> (VerifiedSig a1) -> a2
_verMoves maxReg h f s =
  Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s)
    (verInit maxReg s) (verFinal maxReg s) x (verErrors maxReg s)
    (verExt maxReg s)) (f (verMoves maxReg s))

_verErrors :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap
              ((,) RegStateDescSet ([] AllocError))) -> a2) -> (VerifiedSig
              a1) -> a2
_verErrors maxReg h f s =
  Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s)
    (verInit maxReg s) (verFinal maxReg s) (verMoves maxReg s) x
    (verExt maxReg s)) (f (verErrors maxReg s))

_verExt :: Prelude.Int -> (Functor.Functor a2) -> (a1 -> a2) -> (VerifiedSig
           a1) -> a2
_verExt maxReg h f s =
  Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s)
    (verInit maxReg s) (verFinal maxReg s) (verMoves maxReg s)
    (verErrors maxReg s) x) (f (verExt maxReg s))

type Verified mType a a0 = State0.StateT (VerifiedSig a) mType a0

errorsT :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> ([] AllocError)
           -> Verified a1 a2 ()
errorsT maxReg mDict pc errs =
  Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
    Lens.applyStateT (\_ -> _verErrors maxReg) (\m ->
      Prelude0.flip (IntMap.coq_IntMap_insert pc) m
        (case IntMap.coq_IntMap_lookup pc m of {
          Prelude.Just p ->
           case p of {
            (,) d prevErrs -> (,) d ((Prelude.++) prevErrs errs)};
          Prelude.Nothing -> (,) (fromRegStateDesc maxReg st) errs})) mDict)
    (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)

errorT :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> AllocError ->
          Verified a1 a2 ()
errorT maxReg mDict pc err =
  errorsT maxReg mDict pc ((:) err [])

addMove :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->
           Resolve.ResolvingMoveSet -> Verified a1 a2 ()
addMove maxReg mDict pc mv =
  Lens.applyStateT (\_ -> _verMoves maxReg)
    (IntMap.coq_IntMap_alter (\mxs -> Prelude.Just
      (case mxs of {
        Prelude.Just xs -> Seq.rcons xs mv;
        Prelude.Nothing -> (:) mv []})) pc) mDict

allocationsAt :: Prelude.Int -> ([] Allocate.Allocation) -> Prelude.Int -> []
                 Allocate.Allocation
allocationsAt maxReg intervals pos =
  Prelude.map (\i -> i)
    (Prelude.filter (\i ->
      let {int = Allocate.intVal maxReg i} in
      (Prelude.&&) ((Prelude.<=) (Interval.ibeg int) pos)
        ((Prelude.<=) ((Prelude.succ) pos) (Interval.iend int))) intervals)

allocationFor :: Prelude.Int -> ([] Allocate.Allocation) -> Blocks.VarId ->
                 Prelude.Int -> Prelude.Maybe (Prelude.Maybe PhysReg)
allocationFor maxReg intervals var pos =
  case Prelude.filter (\i ->
         Eqtype.eq_op Ssrnat.nat_eqType
           (unsafeCoerce (Interval.ivar (Allocate.intVal maxReg i)))
           (unsafeCoerce var)) (allocationsAt maxReg intervals pos) of {
   [] -> Prelude.Nothing;
   (:) a l ->
    case l of {
     [] -> Prelude.Just (Allocate.intReg maxReg a);
     (:) a0 l0 -> Prelude.Nothing}}

checkAllocation :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> ([]
                   Allocate.Allocation) -> (Prelude.Maybe
                   (Prelude.Maybe PhysReg)) -> Blocks.VarId -> Prelude.Int ->
                   Prelude.Int -> Verified a1 a2 ()
checkAllocation maxReg mDict pc intervals reg var pos idx =
  let {alloc = allocationFor maxReg intervals var pos} in
  case Prelude.not
         (Eqtype.eq_op
           (Eqtype.option_eqType
             (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg)))
           (unsafeCoerce alloc) (unsafeCoerce reg)) of {
   Prelude.True ->
    errorT maxReg mDict pc (AllocationDoesNotMatch var
      (Maybe.option_map (Maybe.option_map Prelude.id) reg)
      (Maybe.option_map (Maybe.option_map Prelude.id) alloc) pos idx);
   Prelude.False -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}

reserveReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg ->
              Blocks.VarId -> Verified a1 a2 ()
reserveReg maxReg mDict pc reg var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
      case Ssr.prop
             (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)
               (Lens.view
                 (Lens.stepdownl' (unsafeCoerce (\_ -> reservation)))
                 (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
               (unsafeCoerce Prelude.Nothing)) of {
       Prelude.Just _ ->
        Lens.modifyStateT (\_ -> _verState maxReg)
          (packRegState maxReg (Build_RegStateDesc
            (Vector0.vmodify maxReg (rsAllocs maxReg st) reg
              (Lens.set (\_ -> reservation) (Prelude.Just var)))
            (rsStack maxReg st))) mDict;
       Prelude.Nothing ->
        case Lens.view (Lens.stepdownl' (\_ -> reservation))
               (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {
         Prelude.Just v ->
          Monad.when (State0.coq_StateT_Monad mDict)
            (Prelude.not
              (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce v)
                (unsafeCoerce var)))
            (errorT maxReg mDict pc (RegAlreadyReservedToVar (Prelude.id reg)
              v var));
         Prelude.Nothing ->
          Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})
      (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))
    (addMove maxReg mDict pc (Resolve.RSAllocReg var (Prelude.id reg)))

isReserved :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Verified 
              a1 a2 (Prelude.Maybe Blocks.VarId)
isReserved maxReg mDict reg =
  Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
    Applicative.pure (State0.coq_StateT_Applicative mDict)
      (Lens.view (Lens.stepdownl' (\_ -> reservation))
        (Vector0.vnth maxReg (rsAllocs maxReg st) reg)))
    (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)

checkReservation :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg
                    -> Blocks.VarId -> Verified a1 a2 ()
checkReservation maxReg mDict pc reg var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
    let {
     err = errorT maxReg mDict pc (VarNotReservedForReg var (Prelude.id reg)
             (Lens.view (Lens.stepdownl' (\_ -> reservation))
               (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
             ((Prelude.succ) 0))}
    in
    Monad.bind (State0.coq_StateT_Monad mDict) (\res ->
      case res of {
       Prelude.Just var' ->
        Monad.unless (State0.coq_StateT_Monad mDict)
          (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce var) var') err;
       Prelude.Nothing -> err}) (isReserved maxReg mDict reg))
    (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)

releaseReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg ->
              Blocks.VarId -> Verified a1 a2 ()
releaseReg maxReg mDict pc reg var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
      case Ssr.prop
             (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)
               (Lens.view
                 (Lens.stepdownl' (unsafeCoerce (\_ -> reservation)))
                 (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
               (unsafeCoerce (Prelude.Just var))) of {
       Prelude.Just _ ->
        Lens.modifyStateT (\_ -> _verState maxReg)
          (packRegState maxReg (Build_RegStateDesc
            (Vector0.vmodify maxReg (rsAllocs maxReg st) reg
              (Lens.set (\_ -> reservation) Prelude.Nothing))
            (rsStack maxReg st))) mDict;
       Prelude.Nothing ->
        errorT maxReg mDict pc (VarNotReservedForReg var (Prelude.id reg)
          (Lens.view (Lens.stepdownl' (\_ -> reservation))
            (Vector0.vnth maxReg (rsAllocs maxReg st) reg)) ((Prelude.succ)
          ((Prelude.succ) 0)))})
      (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))
    (addMove maxReg mDict pc (Resolve.RSFreeReg (Prelude.id reg) var))

clearReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier ->
            PhysReg -> Blocks.VarId -> Verified a1 a2 ()
clearReg maxReg mDict pc useVerifier reg var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
      case Ssr.prop
             (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)
               (Lens.view (Lens.stepdownl' (unsafeCoerce (\_ -> residency)))
                 (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
               (unsafeCoerce (Prelude.Just var))) of {
       Prelude.Just _ ->
        Lens.modifyStateT (\_ -> _verState maxReg)
          (packRegState maxReg (Build_RegStateDesc
            (Vector0.vmodify maxReg (rsAllocs maxReg st) reg
              (Lens.set (\_ -> residency) Prelude.Nothing))
            (rsStack maxReg st))) mDict;
       Prelude.Nothing ->
        let {
         err = errorT maxReg mDict pc (VarNotResidentForReg var
                 (Prelude.id reg)
                 (Lens.view (Lens.stepdownl' (\_ -> residency))
                   (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
                 ((Prelude.succ) ((Prelude.succ) 0)))}
        in
        case useVerifier of {
         VerifyEnabledStrict -> err;
         _ ->
          case Lens.view (Lens.stepdownl' (\_ -> residency))
                 (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {
           Prelude.Just v -> err;
           Prelude.Nothing ->
            Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}})
      (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))
    (addMove maxReg mDict pc (Resolve.RSClearReg (Prelude.id reg) var))

assignReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier ->
             PhysReg -> Blocks.VarId -> Verified a1 a2 ()
assignReg maxReg mDict pc useVerifier reg var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
      case Ssr.prop
             (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)
               (Lens.view
                 (Lens.stepdownl' (unsafeCoerce (\_ -> reservation)))
                 (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
               (unsafeCoerce (Prelude.Just var))) of {
       Prelude.Just _ ->
        Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
          Lens.modifyStateT (\_ -> _verState maxReg)
            (packRegState maxReg (Build_RegStateDesc
              (Vector0.vmodify maxReg (rsAllocs maxReg st) reg
                (Lens.set (\_ -> residency) (Prelude.Just var)))
              (rsStack maxReg st))) mDict)
          (Vector0.vfoldr_with_index maxReg (\reg0 x0 act ->
            case Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)
                   (Prelude.fst x0) (unsafeCoerce (Prelude.Just var)) of {
             Prelude.True ->
              Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> act)
                (clearReg maxReg mDict pc useVerifier reg0 var);
             Prelude.False -> act})
            (Applicative.pure (State0.coq_StateT_Applicative mDict) ())
            (rsAllocs maxReg st));
       Prelude.Nothing ->
        let {
         err = errorT maxReg mDict pc (VarNotReservedForReg var
                 (Prelude.id reg)
                 (Lens.view (Lens.stepdownl' (\_ -> reservation))
                   (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
                 ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0))))}
        in
        case useVerifier of {
         VerifyEnabledStrict -> err;
         _ ->
          case Lens.view (Lens.stepdownl' (\_ -> reservation))
                 (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {
           Prelude.Just v -> err;
           Prelude.Nothing ->
            Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}})
      (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))
    (addMove maxReg mDict pc (Resolve.RSAssignReg var (Prelude.id reg)))

isResident :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Verified 
              a1 a2 (Prelude.Maybe Blocks.VarId)
isResident maxReg mDict reg =
  Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
    Applicative.pure (State0.coq_StateT_Applicative mDict)
      (Lens.view (Lens.stepdownl' (\_ -> residency))
        (Vector0.vnth maxReg (rsAllocs maxReg st) reg)))
    (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)

checkResidency :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->
                  UseVerifier -> PhysReg -> Blocks.VarId -> Verified 
                  a1 a2 ()
checkResidency maxReg mDict pc useVerifier reg var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\res ->
      let {
       err = errorT maxReg mDict pc (VarNotResidentForReg var
               (Prelude.id reg) res ((Prelude.succ) 0))}
      in
      case useVerifier of {
       VerifyEnabledStrict ->
        case res of {
         Prelude.Just var' ->
          Monad.unless (State0.coq_StateT_Monad mDict)
            (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce var)
              (unsafeCoerce var')) err;
         Prelude.Nothing -> err};
       _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()})
      (isResident maxReg mDict reg))
    (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)

isStackAllocated :: Prelude.Int -> (Monad.Monad a1) -> Blocks.VarId ->
                    Verified a1 a2 Prelude.Bool
isStackAllocated maxReg mDict var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
    Applicative.pure (State0.coq_StateT_Applicative mDict)
      (IntSet.coq_IntSet_member var (rsStack maxReg st)))
    (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)

checkStack :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier
              -> Blocks.VarId -> Verified a1 a2 ()
checkStack maxReg mDict pc useVerifier var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\res ->
      let {err = errorT maxReg mDict pc (StackNotAllocatedForVar var)} in
      case useVerifier of {
       VerifyEnabledStrict ->
        Monad.unless (State0.coq_StateT_Monad mDict) res err;
       _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()})
      (isStackAllocated maxReg mDict var))
    (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)

allocStack :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier
              -> Blocks.VarId -> Verified a1 a2 ()
allocStack maxReg mDict pc useVerifier var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
      case Ssr.prop
             (Prelude.not (IntSet.coq_IntSet_member var (rsStack maxReg st))) of {
       Prelude.Just _ ->
        Lens.modifyStateT (\_ -> _verState maxReg)
          (packRegState maxReg (Build_RegStateDesc (rsAllocs maxReg st)
            (IntSet.coq_IntSet_insert var (rsStack maxReg st)))) mDict;
       Prelude.Nothing ->
        let {err = errorT maxReg mDict pc (StackAlreadyAllocatedForVar var)}
        in
        case useVerifier of {
         VerifyEnabledStrict -> err;
         _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})
      (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))
    (addMove maxReg mDict pc (Resolve.RSAllocStack var))

freeStack :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier ->
             Blocks.VarId -> Verified a1 a2 ()
freeStack maxReg mDict pc useVerifier var =
  Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
      case Ssr.prop (IntSet.coq_IntSet_member var (rsStack maxReg st)) of {
       Prelude.Just _ ->
        Lens.modifyStateT (\_ -> _verState maxReg)
          (packRegState maxReg (Build_RegStateDesc (rsAllocs maxReg st)
            (IntSet.coq_IntSet_delete var (rsStack maxReg st)))) mDict;
       Prelude.Nothing ->
        let {err = errorT maxReg mDict pc (StackNotAllocatedForVar var)} in
        case useVerifier of {
         VerifyEnabledStrict -> err;
         _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})
      (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))
    (addMove maxReg mDict pc (Resolve.RSFreeStack var))

verifyBlockBegin :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->
                    UseVerifier -> Prelude.Int -> IntSet.IntSet ->
                    Loops.LoopState -> Verified a1 a2 ()
verifyBlockBegin maxReg mDict pc useVerifier bid liveIns loops =
  case useVerifier of {
   VerifyDisabled ->
    Applicative.pure (State0.coq_StateT_Applicative mDict) ();
   VerifyEnabled ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
      Monad.bind (State0.coq_StateT_Monad mDict) (\allocs ->
        Lens.applyStateT (\_ -> _verInit maxReg)
          (IntMap.coq_IntMap_insert bid allocs) mDict)
        (Lens.use (Lens.stepdownl' (\_ -> _verState maxReg)) mDict))
      (case IntMap.coq_IntMap_lookup bid (Loops.forwardBranches loops) of {
        Prelude.Just fwds ->
         Monad.forM_ (State0.coq_StateT_Monad mDict)
           (IntSet.coq_IntSet_toList fwds) (\pred ->
           Monad.bind (State0.coq_StateT_Monad mDict) (\exits ->
             case IntMap.coq_IntMap_lookup pred exits of {
              Prelude.Just allocs ->
               Lens.modifyStateT (\_ -> _verState maxReg) allocs mDict;
              Prelude.Nothing ->
               errorT maxReg mDict pc (UnknownPredecessorBlock bid pred)})
             (Lens.use (Lens.stepdownl' (\_ -> _verFinal maxReg)) mDict));
        Prelude.Nothing ->
         case useVerifier of {
          VerifyEnabledStrict ->
           Monad.when (State0.coq_StateT_Monad mDict)
             ((Prelude.<=) ((Prelude.succ) 0)
               (IntSet.coq_IntSet_size liveIns))
             (errorT maxReg mDict pc (BlockWithoutPredecessors bid));
          _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}});
   VerifyEnabledStrict ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
      Monad.bind (State0.coq_StateT_Monad mDict) (\allocs ->
        Lens.applyStateT (\_ -> _verInit maxReg)
          (IntMap.coq_IntMap_insert bid allocs) mDict)
        (Lens.use (Lens.stepdownl' (\_ -> _verState maxReg)) mDict))
      (case IntMap.coq_IntMap_lookup bid (Loops.forwardBranches loops) of {
        Prelude.Just fwds ->
         Monad.forM_ (State0.coq_StateT_Monad mDict)
           (IntSet.coq_IntSet_toList fwds) (\pred ->
           Monad.bind (State0.coq_StateT_Monad mDict) (\exits ->
             case IntMap.coq_IntMap_lookup pred exits of {
              Prelude.Just allocs ->
               Lens.modifyStateT (\_ -> _verState maxReg) allocs mDict;
              Prelude.Nothing ->
               errorT maxReg mDict pc (UnknownPredecessorBlock bid pred)})
             (Lens.use (Lens.stepdownl' (\_ -> _verFinal maxReg)) mDict));
        Prelude.Nothing ->
         case useVerifier of {
          VerifyEnabledStrict ->
           Monad.when (State0.coq_StateT_Monad mDict)
             ((Prelude.<=) ((Prelude.succ) 0)
               (IntSet.coq_IntSet_size liveIns))
             (errorT maxReg mDict pc (BlockWithoutPredecessors bid));
          _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})}

verifyBlockEnd :: Prelude.Int -> (Monad.Monad a1) -> UseVerifier ->
                  Prelude.Int -> IntSet.IntSet -> Verified a1 a2 ()
verifyBlockEnd maxReg mDict useVerifier bid liveOuts =
  case useVerifier of {
   VerifyDisabled ->
    Applicative.pure (State0.coq_StateT_Applicative mDict) ();
   _ ->
    Monad.bind (State0.coq_StateT_Monad mDict) (\allocs ->
      Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
        Lens.modifyStateT (\_ -> _verState maxReg)
          (packRegState maxReg (newRegStateDesc maxReg)) mDict)
        (Lens.applyStateT (\_ -> _verFinal maxReg)
          (IntMap.coq_IntMap_insert bid allocs) mDict))
      (Lens.use (Lens.stepdownl' (\_ -> _verState maxReg)) mDict)}

verifyAllocs :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo a3 
                a1 a2) -> Blocks.OpId -> ([] Allocate.Allocation) ->
                UseVerifier -> a1 -> ([]
                ((,) ((,) Blocks.VarId UsePos.VarKind) PhysReg)) -> Verified
                a3 a4 ()
verifyAllocs maxReg mDict oinfo pc intervals useVerifier op allocs =
  case useVerifier of {
   VerifyDisabled ->
    Applicative.pure (State0.coq_StateT_Applicative mDict) ();
   VerifyEnabled ->
    Monad.forM_ (State0.coq_StateT_Monad mDict)
      (Blocks.opRefs maxReg mDict oinfo op) (\ref ->
      case Blocks.varId maxReg ref of {
       Prelude.Left reg ->
        Monad.when (State0.coq_StateT_Monad mDict)
          (Prelude.not
            (Eqtype.eq_op UsePos.coq_VarKind_eqType
              (unsafeCoerce (Blocks.varKind maxReg ref))
              (unsafeCoerce UsePos.Input)))
          (Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
            case Lens.view (Lens.stepdownl' (\_ -> reservation))
                   (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {
             Prelude.Just v ->
              errorT maxReg mDict pc (PhysRegAlreadyReservedForVar
                (Prelude.id reg) v);
             Prelude.Nothing ->
              case Prelude.filter (\i ->
                     Eqtype.eq_op
                       (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))
                       (unsafeCoerce (Allocate.intReg maxReg i))
                       (unsafeCoerce (Prelude.Just reg)))
                     (allocationsAt maxReg intervals (Prelude.pred pc)) of {
               [] ->
                Applicative.pure (State0.coq_StateT_Applicative mDict) ();
               (:) x l ->
                errorT maxReg mDict pc (AllocationDoesNotMatch
                  (Interval.ivar (Allocate.intVal maxReg x)) Prelude.Nothing
                  (Prelude.Just
                  (Maybe.option_map Prelude.id (Allocate.intReg maxReg x)))
                  (Prelude.pred pc) 0)}})
            (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict));
       Prelude.Right var ->
        case List1.maybeLookup
               (Eqtype.prod_eqType Ssrnat.nat_eqType
                 UsePos.coq_VarKind_eqType) (unsafeCoerce allocs)
               (unsafeCoerce ((,) var (Blocks.varKind maxReg ref))) of {
         Prelude.Just reg ->
          case Blocks.varKind maxReg ref of {
           UsePos.Input -> checkResidency maxReg mDict pc useVerifier reg var;
           UsePos.InputOutput ->
            Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
              Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
                assignReg maxReg mDict pc useVerifier reg var)
                (checkAllocation maxReg mDict pc intervals (Prelude.Just
                  (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ)
                  0))) (checkResidency maxReg mDict pc useVerifier reg var);
           UsePos.Temp ->
            Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
              checkReservation maxReg mDict pc reg var)
              (checkAllocation maxReg mDict pc intervals (Prelude.Just
                (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ)
                ((Prelude.succ) 0)));
           UsePos.Output ->
            Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
              assignReg maxReg mDict pc useVerifier reg var)
              (checkAllocation maxReg mDict pc intervals (Prelude.Just
                (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ)
                ((Prelude.succ) ((Prelude.succ) 0))))};
         Prelude.Nothing -> errorT maxReg mDict pc (VarNotAllocated var)}});
   VerifyEnabledStrict ->
    Monad.forM_ (State0.coq_StateT_Monad mDict)
      (Blocks.opRefs maxReg mDict oinfo op) (\ref ->
      case Blocks.varId maxReg ref of {
       Prelude.Left reg ->
        Monad.when (State0.coq_StateT_Monad mDict)
          (Prelude.not
            (Eqtype.eq_op UsePos.coq_VarKind_eqType
              (unsafeCoerce (Blocks.varKind maxReg ref))
              (unsafeCoerce UsePos.Input)))
          (Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
            case Lens.view (Lens.stepdownl' (\_ -> reservation))
                   (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {
             Prelude.Just v ->
              errorT maxReg mDict pc (PhysRegAlreadyReservedForVar
                (Prelude.id reg) v);
             Prelude.Nothing ->
              case Prelude.filter (\i ->
                     Eqtype.eq_op
                       (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))
                       (unsafeCoerce (Allocate.intReg maxReg i))
                       (unsafeCoerce (Prelude.Just reg)))
                     (allocationsAt maxReg intervals (Prelude.pred pc)) of {
               [] ->
                Applicative.pure (State0.coq_StateT_Applicative mDict) ();
               (:) x l ->
                errorT maxReg mDict pc (AllocationDoesNotMatch
                  (Interval.ivar (Allocate.intVal maxReg x)) Prelude.Nothing
                  (Prelude.Just
                  (Maybe.option_map Prelude.id (Allocate.intReg maxReg x)))
                  (Prelude.pred pc) 0)}})
            (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict));
       Prelude.Right var ->
        case List1.maybeLookup
               (Eqtype.prod_eqType Ssrnat.nat_eqType
                 UsePos.coq_VarKind_eqType) (unsafeCoerce allocs)
               (unsafeCoerce ((,) var (Blocks.varKind maxReg ref))) of {
         Prelude.Just reg ->
          case Blocks.varKind maxReg ref of {
           UsePos.Input -> checkResidency maxReg mDict pc useVerifier reg var;
           UsePos.InputOutput ->
            Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
              Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
                assignReg maxReg mDict pc useVerifier reg var)
                (checkAllocation maxReg mDict pc intervals (Prelude.Just
                  (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ)
                  0))) (checkResidency maxReg mDict pc useVerifier reg var);
           UsePos.Temp ->
            Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
              checkReservation maxReg mDict pc reg var)
              (checkAllocation maxReg mDict pc intervals (Prelude.Just
                (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ)
                ((Prelude.succ) 0)));
           UsePos.Output ->
            Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
              assignReg maxReg mDict pc useVerifier reg var)
              (checkAllocation maxReg mDict pc intervals (Prelude.Just
                (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ)
                ((Prelude.succ) ((Prelude.succ) 0))))};
         Prelude.Nothing -> errorT maxReg mDict pc (VarNotAllocated var)}})}

verifyResolutions :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->
                     UseVerifier -> ([] Resolve.ResolvingMove) -> Verified 
                     a1 a2 ([] Resolve.ResolvingMove)
verifyResolutions maxReg mDict pc useVerifier moves =
  case useVerifier of {
   VerifyDisabled ->
    Applicative.pure (State0.coq_StateT_Applicative mDict) moves;
   _ ->
    Monad.forFoldM (State0.coq_StateT_Monad mDict) [] moves (\acc mv ->
      Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
        case mv of {
         Resolve.Move fromReg fromVar toReg ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
              Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->
                Applicative.pure (State0.coq_StateT_Applicative mDict)
                  (Seq.rcons acc mv))
                (addMove maxReg mDict pc
                  (Resolve.weakenResolvingMove maxReg mv)))
              (checkReservation maxReg mDict pc toReg fromVar))
            (checkResidency maxReg mDict pc useVerifier fromReg fromVar);
         Resolve.Spill fromReg toSpillSlot fromSplit ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Monad.bind (State0.coq_StateT_Monad mDict) (\check ->
              case Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)
                     check (unsafeCoerce (Prelude.Just toSpillSlot)) of {
               Prelude.True ->
                Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
                  Applicative.pure (State0.coq_StateT_Applicative mDict)
                    (Seq.rcons acc mv))
                  (addMove maxReg mDict pc
                    (Resolve.weakenResolvingMove maxReg mv));
               Prelude.False ->
                let {mv' = Resolve.FreeStack toSpillSlot} in
                Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
                  Applicative.pure (State0.coq_StateT_Applicative mDict)
                    (Seq.rcons acc mv'))
                  (addMove maxReg mDict pc
                    (Resolve.weakenResolvingMove maxReg mv'))})
              (isResident maxReg mDict fromReg))
            (checkStack maxReg mDict pc useVerifier toSpillSlot);
         Resolve.Restore fromSpillSlot toReg fromSplit ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
              Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->
                Applicative.pure (State0.coq_StateT_Applicative mDict)
                  (Seq.rcons acc mv))
                (addMove maxReg mDict pc
                  (Resolve.weakenResolvingMove maxReg mv)))
              (checkReservation maxReg mDict pc toReg fromSpillSlot))
            (checkStack maxReg mDict pc useVerifier fromSpillSlot);
         Resolve.AllocReg toVar toReg ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Applicative.pure (State0.coq_StateT_Applicative mDict) acc)
            (reserveReg maxReg mDict pc toReg toVar);
         Resolve.FreeReg fromReg fromVar ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Applicative.pure (State0.coq_StateT_Applicative mDict) acc)
            (releaseReg maxReg mDict pc fromReg fromVar);
         Resolve.AssignReg fromVar toReg ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Applicative.pure (State0.coq_StateT_Applicative mDict) acc)
            (assignReg maxReg mDict pc useVerifier toReg fromVar);
         Resolve.ClearReg fromReg toVar ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Applicative.pure (State0.coq_StateT_Applicative mDict) acc)
            (clearReg maxReg mDict pc useVerifier fromReg toVar);
         Resolve.AllocStack toVar ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Applicative.pure (State0.coq_StateT_Applicative mDict) acc)
            (allocStack maxReg mDict pc useVerifier toVar);
         Resolve.FreeStack fromVar ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Applicative.pure (State0.coq_StateT_Applicative mDict) acc)
            (freeStack maxReg mDict pc useVerifier fromVar);
         Resolve.Looped x ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
            Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->
              Applicative.pure (State0.coq_StateT_Applicative mDict)
                (Seq.rcons acc mv))
              (addMove maxReg mDict pc
                (Resolve.weakenResolvingMove maxReg mv)))
            (errorT maxReg mDict pc (LoopInResolvingMoves
              (Resolve.weakenResolvingMove maxReg x)))})
        (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))}

verifyTransitions :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> ([]
                     Allocate.Allocation) -> UseVerifier -> ([]
                     Resolve.ResolvingMove) -> Prelude.Int -> Prelude.Int ->
                     Verified a1 a2 ()
verifyTransitions maxReg mDict pc intervals useVerifier moves from to =
  case useVerifier of {
   VerifyDisabled ->
    Applicative.pure (State0.coq_StateT_Applicative mDict) ();
   _ ->
    Monad.forM_ (State0.coq_StateT_Monad mDict) moves (\mv ->
      Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
        case mv of {
         Resolve.Move fromReg fromVar toReg ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            checkAllocation maxReg mDict pc intervals (Prelude.Just
              (Prelude.Just toReg)) fromVar to ((Prelude.succ)
              ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
              0))))))
            (checkAllocation maxReg mDict pc intervals (Prelude.Just
              (Prelude.Just fromReg)) fromVar from ((Prelude.succ)
              ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0)))));
         Resolve.Spill fromReg toSpillSlot fromSplit ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            Monad.unless (State0.coq_StateT_Monad mDict) fromSplit
              (checkAllocation maxReg mDict pc intervals (Prelude.Just
                Prelude.Nothing) toSpillSlot to ((Prelude.succ)
                ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
                ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0)))))))))
            (checkAllocation maxReg mDict pc intervals (Prelude.Just
              (Prelude.Just fromReg)) toSpillSlot from ((Prelude.succ)
              ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
              ((Prelude.succ) 0)))))));
         Resolve.Restore fromSpillSlot toReg fromSplit ->
          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
            checkAllocation maxReg mDict pc intervals (Prelude.Just
              (Prelude.Just toReg)) fromSpillSlot to ((Prelude.succ)
              ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
              ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
              0))))))))))
            (Monad.unless (State0.coq_StateT_Monad mDict) fromSplit
              (checkAllocation maxReg mDict pc intervals (Prelude.Just
                Prelude.Nothing) fromSpillSlot from ((Prelude.succ)
                ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
                ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
                ((Prelude.succ) 0))))))))));
         Resolve.AllocReg toVar toReg ->
          checkAllocation maxReg mDict pc intervals (Prelude.Just
            (Prelude.Just toReg)) toVar to ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
            0))))))))));
         Resolve.FreeReg fromReg fromVar ->
          checkAllocation maxReg mDict pc intervals (Prelude.Just
            (Prelude.Just fromReg)) fromVar from ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) 0)))))))))));
         Resolve.AssignReg fromVar toReg ->
          checkAllocation maxReg mDict pc intervals (Prelude.Just
            (Prelude.Just toReg)) fromVar to ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) 0))))))))))));
         Resolve.ClearReg fromReg toVar ->
          checkAllocation maxReg mDict pc intervals (Prelude.Just
            (Prelude.Just fromReg)) toVar from ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
            0)))))))))))));
         Resolve.AllocStack toVar ->
          checkAllocation maxReg mDict pc intervals (Prelude.Just
            Prelude.Nothing) toVar to ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
            0))))))))))))));
         Resolve.FreeStack fromVar ->
          checkAllocation maxReg mDict pc intervals (Prelude.Just
            Prelude.Nothing) fromVar from ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ)
            ((Prelude.succ) 0)))))))))))))));
         Resolve.Looped x ->
          Applicative.pure (State0.coq_StateT_Applicative mDict) ()})
        (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))}