diff --git a/LinearScan.hs b/LinearScan.hs
--- a/LinearScan.hs
+++ b/LinearScan.hs
@@ -1,5 +1,7 @@
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE ViewPatterns #-}
 
 {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}
 
@@ -8,23 +10,18 @@
       allocate
       -- * Blocks
     , BlockInfo(..)
-    , defaultBlockInfo
       -- * Operations
     , OpInfo(..)
     , OpKind(..)
-    , defaultOpInfo
       -- * Variables
     , VarInfo(..)
     , VarKind(..)
-    , Allocation(..)
     , PhysReg
-    , defaultVarInfo
     ) where
 
 import qualified LinearScan.Main as LS
 import LinearScan.Main
     ( VarKind(..)
-    , Allocation(..)
     , OpKind(..)
     , PhysReg
     )
@@ -35,30 +32,17 @@
 --   scope of their lifetime.  For example, output variables are not needed in a
 --   basic block until the first point of use, while the lifetime of input
 --   variables extends until their final use.
-data VarInfo = VarInfo
-    { varId       :: Int
-    , varKind     :: VarKind
-    , varAlloc    :: Allocation
-    , regRequired :: Bool
+data VarInfo v = VarInfo
+    { varId       :: v -> Int
+    , varKind     :: v -> VarKind
+    , regRequired :: v -> Bool
     }
-    deriving (Eq, Show)
 
 deriving instance Eq VarKind
 deriving instance Show VarKind
 
-defaultVarInfo :: VarInfo
-defaultVarInfo = VarInfo
-    { varId       = 0
-    , varKind     = Temp
-    , varAlloc    = Unallocated
-    , regRequired = False
-    }
-
-toVarInfo :: LS.VarInfo -> VarInfo
-toVarInfo (LS.Build_VarInfo a b c d) = VarInfo a b c d
-
-fromVarInfo :: VarInfo -> LS.VarInfo
-fromVarInfo (VarInfo a b c d) = LS.Build_VarInfo a b c d
+fromVarInfo :: VarInfo v -> LS.VarInfo v
+fromVarInfo (VarInfo a b c) = LS.Build_VarInfo a b c
 
 -- | Every operation may reference multiple variables and/or specific physical
 --   registers.  If a physical register is referenced, then that register is
@@ -71,70 +55,49 @@
 --   and restore all registers around a call, but indication of loops is
 --   optional, as it's merely avoids reloading of spilled variables inside
 --   loop bodies.
-data OpInfo = OpInfo
-    { opId    :: Int
-    , opMeta  :: Int
-    , opKind  :: OpKind
-    , varRefs :: [VarInfo]
-    , regRefs :: [PhysReg]
+data OpInfo accType o v a b = OpInfo
+    { opKind      :: o a -> OpKind
+    , opRefs      :: o a -> ([v], [PhysReg])
+    , saveOp      :: Int -> PhysReg -> accType -> (o b, accType)
+    , restoreOp   :: Int -> PhysReg -> accType -> (o b, accType)
+    , applyAllocs :: o a -> [(Int, PhysReg)] -> o b
     }
-    deriving (Eq, Show)
 
 deriving instance Eq OpKind
 deriving instance Show OpKind
 
-defaultOpInfo :: OpInfo
-defaultOpInfo = OpInfo
-    { opId    = 0
-    , opMeta  = 0
-    , opKind  = Normal
-    , varRefs = []
-    , regRefs = []
-    }
-
-toOpInfo :: LS.OpInfo -> OpInfo
-toOpInfo (LS.Build_OpInfo a b c d e) = OpInfo a b c (map toVarInfo d) e
-
-fromOpInfo :: OpInfo -> LS.OpInfo
-fromOpInfo (OpInfo a b c d e) = LS.Build_OpInfo a b c (map fromVarInfo d) e
+fromOpInfo :: OpInfo accType o v a b -> LS.OpInfo accType (o a) (o b) v
+fromOpInfo (OpInfo a b c d e) = LS.Build_OpInfo a b c d e
 
 -- | From the point of view of this library, a basic block is nothing more
 --   than an ordered sequence of operations.
-data BlockInfo = BlockInfo
-    { blockId  :: Int
-    , blockOps :: [OpInfo]
-    }
-    deriving (Eq, Show)
-
-defaultBlockInfo :: BlockInfo
-defaultBlockInfo = BlockInfo
-    { blockId  = 0
-    , blockOps = []
+data BlockInfo blk o a b = BlockInfo
+    { blockId         :: blk a -> Int
+    , blockSuccessors :: blk a -> [Int]
+    , blockOps        :: blk a -> [o a]
+    , setBlockOps     :: blk a -> [o b] -> blk b
     }
 
-toBlockInfo :: LS.BlockInfo -> BlockInfo
-toBlockInfo (LS.Build_BlockInfo a b) = BlockInfo a (map toOpInfo b)
-
-fromBlockInfo :: BlockInfo -> LS.BlockInfo
-fromBlockInfo (BlockInfo a b) = LS.Build_BlockInfo a (map fromOpInfo b)
+fromBlockInfo :: BlockInfo blk o a b -> LS.BlockInfo (blk a) (blk b) (o a) (o b)
+fromBlockInfo (BlockInfo a b c d) = LS.Build_BlockInfo a b c d
 
 -- | Transform a list of basic blocks containing variable references, into an
 --   equivalent list where each reference is associated with a register
 --   allocation.  Artificial save and restore instructions may also be
 --   inserted into blocks to indicate spilling and reloading of variables.
 --
---   In order to call this function, the caller must transform their own basic
---   block representation into a linear series of 'BlockInfo' structures.
---   Each of these structures may be associated with a unique identifier, to
---   assist with processing allocation info afterward.
+--   In order to call this function, the caller must provide records that
+--   allow viewing and mutating of the original program graph.
 --
 --   If allocation is found to be impossible -- for example if there are
 --   simply not enough registers -- a 'Left' value is returned, with a string
 --   describing the error.
-allocate :: [BlockInfo] -> Either String [BlockInfo]
-allocate [] = Left "No basic blocks were provided"
-allocate blocks =
-    case LS.linearScan (map fromBlockInfo blocks) of
+allocate :: BlockInfo blk o a b -> OpInfo accType o v a b -> VarInfo v
+         -> [blk a] -> accType -> Either String ([blk b], accType)
+allocate _ _ _ [] _ = Left "No basic blocks were provided"
+allocate (fromBlockInfo -> binfo) (fromOpInfo -> oinfo)
+         (fromVarInfo -> vinfo) blocks acc =
+    case LS.linearScan binfo oinfo vinfo blocks acc of
         Left x -> Left $ case x of
             LS.ECannotSplitSingleton n ->
                 "Current interval is a singleton (" ++ show n ++ ")"
@@ -146,4 +109,7 @@
                 "Register is already assigned (" ++ show n ++ ")"
             LS.ERegisterAssignmentsOverlap n ->
                 "Register assignments overlap (" ++ show n ++ ")"
-        Right z -> Right (map toBlockInfo z)
+            LS.EFuelExhausted -> "Fuel was exhausted"
+            LS.EUnexpectedNoMoreUnhandled ->
+                "The unexpected happened: no more unhandled intervals"
+        Right z -> Right z
diff --git a/LinearScan/Datatypes.hs b/LinearScan/Datatypes.hs
--- a/LinearScan/Datatypes.hs
+++ b/LinearScan/Datatypes.hs
@@ -2,6 +2,7 @@
 
 
 import qualified Prelude
+import qualified Data.IntMap
 import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Functor.Identity
diff --git a/LinearScan/Eqtype.hs b/LinearScan/Eqtype.hs
--- a/LinearScan/Eqtype.hs
+++ b/LinearScan/Eqtype.hs
@@ -5,6 +5,7 @@
 
 
 import qualified Prelude
+import qualified Data.IntMap
 import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Functor.Identity
diff --git a/LinearScan/Fintype.hs b/LinearScan/Fintype.hs
--- a/LinearScan/Fintype.hs
+++ b/LinearScan/Fintype.hs
@@ -5,6 +5,7 @@
 
 
 import qualified Prelude
+import qualified Data.IntMap
 import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Functor.Identity
diff --git a/LinearScan/IApplicative.hs b/LinearScan/IApplicative.hs
deleted file mode 100644
--- a/LinearScan/IApplicative.hs
+++ /dev/null
@@ -1,40 +0,0 @@
-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}
-{- For Hugs, use the option -F"cpp -P -traditional" -}
-
-module LinearScan.IApplicative where
-
-
-import qualified Prelude
-import qualified Data.List
-import qualified Data.Ord
-import qualified Data.Functor.Identity
-import qualified LinearScan.Utils
-
-import qualified LinearScan.IEndo as IEndo
-
-
-
---unsafeCoerce :: a -> b
-#ifdef __GLASGOW_HASKELL__
-import qualified GHC.Base as GHC.Base
-unsafeCoerce = GHC.Base.unsafeCoerce#
-#else
--- HUGS
-import qualified LinearScan.IOExts as IOExts
-unsafeCoerce = IOExts.unsafeCoerce
-#endif
-
-__ :: any
-__ = Prelude.error "Logical or arity value used"
-
-data IApplicative f =
-   Build_IApplicative (IEndo.IFunctor f) (() -> () -> () -> f) (() -> () ->
-                                                               () -> () -> ()
-                                                               -> f -> f ->
-                                                               f)
-
-ipure :: (IApplicative a1) -> a3 -> a1
-ipure iApplicative x =
-  case iApplicative of {
-   Build_IApplicative is_ifunctor ipure0 iap -> unsafeCoerce ipure0 __ __ x}
-
diff --git a/LinearScan/IEndo.hs b/LinearScan/IEndo.hs
deleted file mode 100644
--- a/LinearScan/IEndo.hs
+++ /dev/null
@@ -1,35 +0,0 @@
-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}
-{- For Hugs, use the option -F"cpp -P -traditional" -}
-
-module LinearScan.IEndo where
-
-
-import qualified Prelude
-import qualified Data.List
-import qualified Data.Ord
-import qualified Data.Functor.Identity
-import qualified LinearScan.Utils
-
-
-
---unsafeCoerce :: a -> b
-#ifdef __GLASGOW_HASKELL__
-import qualified GHC.Base as GHC.Base
-unsafeCoerce = GHC.Base.unsafeCoerce#
-#else
--- HUGS
-import qualified LinearScan.IOExts as IOExts
-unsafeCoerce = IOExts.unsafeCoerce
-#endif
-
-__ :: any
-__ = Prelude.error "Logical or arity value used"
-
-type IFunctor f =
-  () -> () -> () -> () -> (() -> ()) -> f -> f
-  -- singleton inductive, whose constructor was Build_IFunctor
-  
-imap :: (IFunctor a1) -> (a4 -> a5) -> a1 -> a1
-imap iFunctor x x0 =
-  unsafeCoerce iFunctor __ __ __ __ x x0
-
diff --git a/LinearScan/IMonad.hs b/LinearScan/IMonad.hs
deleted file mode 100644
--- a/LinearScan/IMonad.hs
+++ /dev/null
@@ -1,24 +0,0 @@
-module LinearScan.IMonad where
-
-
-import qualified Prelude
-import qualified Data.List
-import qualified Data.Ord
-import qualified Data.Functor.Identity
-import qualified LinearScan.Utils
-
-import qualified LinearScan.IApplicative as IApplicative
-
-
-__ :: any
-__ = Prelude.error "Logical or arity value used"
-
-data IMonad m =
-   Build_IMonad (IApplicative.IApplicative m) (() -> () -> () -> () -> m ->
-                                              m)
-
-ijoin :: (IMonad a1) -> a1 -> a1
-ijoin iMonad x =
-  case iMonad of {
-   Build_IMonad is_iapplicative ijoin0 -> ijoin0 __ __ __ __ x}
-
diff --git a/LinearScan/IState.hs b/LinearScan/IState.hs
--- a/LinearScan/IState.hs
+++ b/LinearScan/IState.hs
@@ -1,53 +1,18 @@
-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}
-{- For Hugs, use the option -F"cpp -P -traditional" -}
-
 module LinearScan.IState where
 
 
 import qualified Prelude
+import qualified Data.IntMap
 import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
-import qualified LinearScan.IApplicative as IApplicative
-import qualified LinearScan.IEndo as IEndo
-import qualified LinearScan.IMonad as IMonad
 
-
-
---unsafeCoerce :: a -> b
-#ifdef __GLASGOW_HASKELL__
-import qualified GHC.Base as GHC.Base
-unsafeCoerce = GHC.Base.unsafeCoerce#
-#else
--- HUGS
-import qualified LinearScan.IOExts as IOExts
-unsafeCoerce = IOExts.unsafeCoerce
-#endif
-
-__ :: any
-__ = Prelude.error "Logical or arity value used"
-
-type IState errType i o a =
-  i -> Prelude.Either errType ((,) a o)
-  -- singleton inductive, whose constructor was mkIState
-  
-runIState :: (IState a1 a2 a3 a4) -> a2 -> Prelude.Either a1 ((,) a4 a3)
-runIState x =
-  x
-
-coq_IState_IFunctor :: IEndo.IFunctor (IState a1 () () ())
-coq_IState_IFunctor _ _ _ _ f x st =
-  let {filtered_var = runIState x st} in
-  case filtered_var of {
-   Prelude.Left err -> Prelude.Left err;
-   Prelude.Right p ->
-    case p of {
-     (,) a st' -> Prelude.Right ((,) (f a) st')}}
+type IState errType i o a = i -> Prelude.Either errType ((,) a o)
 
-ierr :: a1 -> IState a1 a2 a2 ()
-ierr err i =
+ierr :: a1 -> IState a1 a2 a3 a4
+ierr err x =
   Prelude.Left err
 
 iget :: IState a1 a2 a2 a2
@@ -55,45 +20,26 @@
   Prelude.Right ((,) i i)
 
 iput :: a3 -> IState a1 a2 a3 ()
-iput x s =
+iput x x0 =
   Prelude.Right ((,) () x)
 
-imodify :: (a2 -> a3) -> IState a1 a2 a3 ()
-imodify f i =
-  Prelude.Right ((,) () (f i))
+imap :: (a4 -> a5) -> (IState a1 a2 a3 a4) -> IState a1 a2 a3 a5
+imap f x st =
+  case x st of {
+   Prelude.Left err -> Prelude.Left err;
+   Prelude.Right p ->
+    case p of {
+     (,) a st' -> Prelude.Right ((,) (f a) st')}}
 
-coq_IState_IApplicative :: IApplicative.IApplicative (IState a1 () () ())
-coq_IState_IApplicative =
-  IApplicative.Build_IApplicative coq_IState_IFunctor (\_ _ x st ->
-    Prelude.Right ((,) x st)) (\_ _ _ _ _ f x st ->
-    let {filtered_var = runIState f st} in
-    case filtered_var of {
-     Prelude.Left err -> Prelude.Left err;
-     Prelude.Right p ->
-      case p of {
-       (,) f' st' ->
-        unsafeCoerce (\f'0 st'0 _ ->
-          let {filtered_var0 = runIState x st'0} in
-          case filtered_var0 of {
-           Prelude.Left err -> Prelude.Left err;
-           Prelude.Right p0 ->
-            case p0 of {
-             (,) x' st'' -> Prelude.Right ((,) (f'0 x') st'')}}) f' st' __}})
+ipure :: a3 -> IState a1 a2 a2 a3
+ipure x st =
+  Prelude.Right ((,) x st)
 
-coq_IState_IMonad :: IMonad.IMonad (IState a1 () () ())
-coq_IState_IMonad =
-  IMonad.Build_IMonad coq_IState_IApplicative (\_ _ _ _ x st ->
-    let {filtered_var = runIState x st} in
-    case filtered_var of {
-     Prelude.Left err -> Prelude.Left err;
-     Prelude.Right p ->
-      case p of {
-       (,) y st' ->
-        unsafeCoerce (\y0 st'0 _ ->
-          let {filtered_var0 = runIState y0 st'0} in
-          case filtered_var0 of {
-           Prelude.Left err -> Prelude.Left err;
-           Prelude.Right p0 ->
-            case p0 of {
-             (,) a st'' -> Prelude.Right ((,) a st'')}}) y st' __}})
+ijoin :: (IState a1 a2 a3 (IState a1 a3 a4 a5)) -> IState a1 a2 a4 a5
+ijoin x st =
+  case x st of {
+   Prelude.Left err -> Prelude.Left err;
+   Prelude.Right p ->
+    case p of {
+     (,) y st' -> y st'}}
 
diff --git a/LinearScan/Interval.hs b/LinearScan/Interval.hs
--- a/LinearScan/Interval.hs
+++ b/LinearScan/Interval.hs
@@ -1,10 +1,8 @@
-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}
-{- For Hugs, use the option -F"cpp -P -traditional" -}
-
 module LinearScan.Interval where
 
 
 import qualified Prelude
+import qualified Data.IntMap
 import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Functor.Identity
@@ -13,47 +11,53 @@
 import qualified LinearScan.Lib as Lib
 import qualified LinearScan.Logic as Logic
 import qualified LinearScan.Range as Range
-import qualified LinearScan.Eqtype as Eqtype
-import qualified LinearScan.Ssrnat as Ssrnat
 
 
-
---unsafeCoerce :: a -> b
-#ifdef __GLASGOW_HASKELL__
-import qualified GHC.Base as GHC.Base
-unsafeCoerce = GHC.Base.unsafeCoerce#
-#else
--- HUGS
-import qualified LinearScan.IOExts as IOExts
-unsafeCoerce = IOExts.unsafeCoerce
-#endif
-
 __ :: any
 __ = Prelude.error "Logical or arity value used"
 
+data IntervalKind =
+   Whole
+ | LeftMost
+ | Middle
+ | RightMost
+
+splitKind :: IntervalKind -> (,) IntervalKind IntervalKind
+splitKind k =
+  case k of {
+   Whole -> (,) LeftMost RightMost;
+   LeftMost -> (,) LeftMost Middle;
+   Middle -> (,) Middle Middle;
+   RightMost -> (,) Middle RightMost}
+
 data IntervalDesc =
-   Build_IntervalDesc Prelude.Int Prelude.Int Prelude.Int ([]
-                                                          Range.RangeDesc)
+   Build_IntervalDesc Prelude.Int Prelude.Int Prelude.Int IntervalKind 
+ ([] Range.RangeDesc)
 
 ivar :: IntervalDesc -> Prelude.Int
 ivar i =
   case i of {
-   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> ivar0}
+   Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> ivar0}
 
 ibeg :: IntervalDesc -> Prelude.Int
 ibeg i =
   case i of {
-   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> ibeg0}
+   Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> ibeg0}
 
 iend :: IntervalDesc -> Prelude.Int
 iend i =
   case i of {
-   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> iend0}
+   Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> iend0}
 
+iknd :: IntervalDesc -> IntervalKind
+iknd i =
+  case i of {
+   Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> iknd0}
+
 rds :: IntervalDesc -> [] Range.RangeDesc
 rds i =
   case i of {
-   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> rds0}
+   Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> rds0}
 
 getIntervalDesc :: IntervalDesc -> IntervalDesc
 getIntervalDesc d =
@@ -76,19 +80,6 @@
   (Prelude.&&) ((Prelude.<=) (intervalStart d) pos)
     ((Prelude.<=) ((Prelude.succ) pos) (intervalEnd d))
 
-intervalExtent :: IntervalDesc -> Prelude.Int
-intervalExtent d =
-  (Prelude.-) (intervalEnd d) (intervalStart d)
-
-coq_Interval_is_singleton :: IntervalDesc -> Prelude.Bool
-coq_Interval_is_singleton d =
-  (Prelude.&&)
-    (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Prelude.length (rds d)))
-      (unsafeCoerce ((Prelude.succ) 0)))
-    (Eqtype.eq_op Ssrnat.nat_eqType
-      (unsafeCoerce (Prelude.length (Range.ups ( (Prelude.head (rds d))))))
-      (unsafeCoerce ((Prelude.succ) 0)))
-
 intervalsIntersect :: IntervalDesc -> IntervalDesc -> Prelude.Bool
 intervalsIntersect i j =
   let {f = \x y -> Range.rangesIntersect ( x) ( y)} in
@@ -109,7 +100,7 @@
 
 findIntervalUsePos :: IntervalDesc -> (Range.UsePos -> Prelude.Bool) ->
                       Prelude.Maybe ((,) Range.RangeDesc Range.UsePos)
-findIntervalUsePos i f =
+findIntervalUsePos d f =
   let {
    f0 = \r ->
     case Range.findRangeUsePos r f of {
@@ -124,7 +115,7 @@
        (\r rs' ->
        Lib.option_choose (f0 r) (go rs'))
        rs}
-  in go (rds i)
+  in go (rds d)
 
 nextUseAfter :: IntervalDesc -> Prelude.Int -> Prelude.Maybe Prelude.Int
 nextUseAfter d pos =
@@ -141,103 +132,109 @@
   Lib.option_map ((Prelude..) Range.uloc Prelude.snd)
     (findIntervalUsePos d Range.regReq)
 
-lastUsePos :: IntervalDesc -> Prelude.Int
-lastUsePos d =
-  Range.uloc (Prelude.last (Range.ups ( (Prelude.last (rds d)))))
+data SplitPosition =
+   BeforePos Prelude.Int
+ | BeforeFirstUsePosReqReg
+ | EndOfLifetimeHole
 
-splitPosition :: IntervalDesc -> (Prelude.Maybe Prelude.Int) -> Prelude.Bool
-                 -> Prelude.Int
-splitPosition d before splitBeforeLifetimeHole =
-  let {initial = firstUsePos d} in
-  let {final = lastUsePos d} in
-  Prelude.max ((Prelude.succ) initial)
-    (Prelude.min final
-      (Lib.fromMaybe final (Lib.option_choose before (firstUseReqReg d))))
+splitPosition :: IntervalDesc -> SplitPosition -> Prelude.Maybe Prelude.Int
+splitPosition d pos =
+  case pos of {
+   BeforePos x -> Prelude.Just x;
+   BeforeFirstUsePosReqReg -> firstUseReqReg (getIntervalDesc d);
+   EndOfLifetimeHole -> Prelude.Nothing}
 
 intervalSpan :: ([] Range.RangeDesc) -> Prelude.Int -> Prelude.Int ->
-                Prelude.Int -> Prelude.Int ->
+                Prelude.Int -> Prelude.Int -> IntervalKind ->
                 ((,) (Prelude.Maybe IntervalDesc)
                 (Prelude.Maybe IntervalDesc))
-intervalSpan rs before iv ib ie =
-  let {f = \u -> (Prelude.<=) ((Prelude.succ) (Range.uloc u)) before} in
-  (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
-    (\r ->
-    let {_top_assumption_ = Range.rangeSpan f ( r)} in
-    let {
-     _evar_0_ = \_top_assumption_0 ->
+intervalSpan rs before iv ib ie knd =
+  let {
+   _evar_0_ = \lknd rknd ->
+    (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
+      (\r ->
+      let {_top_assumption_ = Range.rangeSpan before ( r)} in
       let {
-       _evar_0_ = \r0 _top_assumption_1 ->
+       _evar_0_ = \_top_assumption_0 ->
         let {
-         _evar_0_ = \r1 ->
+         _evar_0_ = \r0 _top_assumption_1 ->
           let {
-           _evar_0_ = let {
-                       _evar_0_ = \_ _ -> (,) (Prelude.Just
-                        (Build_IntervalDesc iv (Range.rbeg ( r0))
-                        (Range.rend ( r0)) ((:[]) ( r0)))) (Prelude.Just
-                        (Build_IntervalDesc iv (Range.rbeg ( r1))
-                        (Range.rend ( r1)) ((:[]) ( r1))))}
-                      in
-                       _evar_0_}
+           _evar_0_ = \r1 ->
+            let {
+             _evar_0_ = let {
+                         _evar_0_ = \_ _ -> (,) (Prelude.Just
+                          (Build_IntervalDesc iv (Range.rbeg ( r0))
+                          (Range.rend ( r0)) lknd ((:[]) ( r0))))
+                          (Prelude.Just (Build_IntervalDesc iv
+                          (Range.rbeg ( r1)) (Range.rend ( r1)) rknd ((:[])
+                          ( r1))))}
+                        in
+                         _evar_0_}
+            in
+             _evar_0_ __ __}
           in
-           _evar_0_ __ __}
-        in
-        let {
-         _evar_0_0 = \_ ->
           let {
-           _evar_0_0 = \_ -> (,) (Prelude.Just (Build_IntervalDesc iv ib ie
-            ((:[]) r))) Prelude.Nothing}
+           _evar_0_0 = let {
+                        _evar_0_0 = let {
+                                     _evar_0_0 = \_ -> (,) (Prelude.Just
+                                      (Build_IntervalDesc iv
+                                      (Range.rbeg ( r0)) (Range.rend ( r0))
+                                      knd ((:[]) ( r0)))) Prelude.Nothing}
+                                    in
+                                     _evar_0_0}
+                       in
+                        _evar_0_0}
           in
-           _evar_0_0 __}
+          case _top_assumption_1 of {
+           Prelude.Just x -> (\_ -> _evar_0_ x);
+           Prelude.Nothing -> _evar_0_0}}
         in
-        case _top_assumption_1 of {
-         Prelude.Just x -> (\_ -> _evar_0_ x);
-         Prelude.Nothing -> _evar_0_0}}
-      in
-      let {
-       _evar_0_0 = \_top_assumption_1 ->
         let {
-         _evar_0_0 = \r1 ->
+         _evar_0_0 = \_top_assumption_1 ->
           let {
-           _evar_0_0 = \_ -> (,) Prelude.Nothing (Prelude.Just
-            (Build_IntervalDesc iv ib ie ((:[]) r)))}
+           _evar_0_0 = \r1 ->
+            let {
+             _evar_0_0 = let {
+                          _evar_0_0 = \_ -> (,) Prelude.Nothing (Prelude.Just
+                           (Build_IntervalDesc iv (Range.rbeg ( r1))
+                           (Range.rend ( r1)) knd ((:[]) ( r1))))}
+                         in
+                          _evar_0_0}
+            in
+             _evar_0_0}
           in
-           _evar_0_0 __}
+          let {_evar_0_1 = \_ -> Logic.coq_False_rec} in
+          case _top_assumption_1 of {
+           Prelude.Just x -> _evar_0_0 x;
+           Prelude.Nothing -> _evar_0_1}}
         in
-        let {_evar_0_1 = \_ -> Logic.coq_False_rec} in
-        case _top_assumption_1 of {
-         Prelude.Just x -> (\_ -> _evar_0_0 x);
-         Prelude.Nothing -> _evar_0_1}}
+        case _top_assumption_0 of {
+         Prelude.Just x -> _evar_0_ x;
+         Prelude.Nothing -> _evar_0_0}}
       in
-      case _top_assumption_0 of {
-       Prelude.Just x -> _evar_0_ x;
-       Prelude.Nothing -> _evar_0_0}}
-    in
-    case _top_assumption_ of {
-     (,) x x0 -> _evar_0_ x x0 __})
-    (\r rs0 ->
-    let {_top_assumption_ = Range.rangeSpan f ( r)} in
-    let {
-     _evar_0_ = \_top_assumption_0 ->
+      case _top_assumption_ of {
+       (,) x x0 -> _evar_0_ x x0 __})
+      (\r rs0 ->
+      let {_top_assumption_ = Range.rangeSpan before ( r)} in
       let {
-       _evar_0_ = \r0 _top_assumption_1 ->
+       _evar_0_ = \_top_assumption_0 ->
         let {
-         _evar_0_ = \r1 ->
+         _evar_0_ = \r0 _top_assumption_1 ->
           let {
-           _evar_0_ = \_ ->
+           _evar_0_ = \r1 ->
             let {
-             _evar_0_ = \_ _ ->
-              (Prelude.flip (Prelude.$)) __ (\_ -> (,) (Prelude.Just
-                (Build_IntervalDesc iv (Range.rbeg ( r0)) (Range.rend ( r0))
-                ((:[]) ( r0)))) (Prelude.Just (Build_IntervalDesc iv
-                (Range.rbeg ( r1)) (Range.rend ( (Prelude.last rs0))) ((:) r1
-                rs0))))}
+             _evar_0_ = \_ ->
+              (Prelude.flip (Prelude.$)) __ (\_ ->
+                let {
+                 _evar_0_ = \_ -> (,) (Prelude.Just (Build_IntervalDesc iv
+                  (Range.rbeg ( r0)) (Range.rend ( r0)) lknd ((:[]) ( r0))))
+                  (Prelude.Just (Build_IntervalDesc iv (Range.rbeg ( r1))
+                  (Range.rend ( (Prelude.last rs0))) knd ((:) r1 rs0)))}
+                in
+                 _evar_0_ __)}
             in
-             _evar_0_ __ __}
+             _evar_0_ __}
           in
-           _evar_0_ __}
-        in
-        let {
-         _evar_0_0 = \_ ->
           let {
            _evar_0_0 = \_ ->
             let {
@@ -245,7 +242,7 @@
               let {
                _top_assumption_2 = intervalSpan rs0 before iv
                                      (Range.rbeg ( (Prelude.head rs0)))
-                                     (Range.rend ( (Prelude.last rs0)))}
+                                     (Range.rend ( (Prelude.last rs0))) knd}
               in
               let {
                _evar_0_0 = \_top_assumption_3 ->
@@ -254,31 +251,30 @@
                   let {
                    _evar_0_0 = \i1_2 ->
                     case i1_1 of {
-                     Build_IntervalDesc ivar0 ibeg0 iend0 rds0 ->
+                     Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 ->
                       let {
                        _evar_0_0 = let {
-                                    _evar_0_0 = \_ _ ->
+                                    _evar_0_0 = \_ ->
                                      let {
                                       _evar_0_0 = \_ ->
                                        let {
                                         _evar_0_0 = \_ ->
-                                         let {
-                                          _evar_0_0 = (Prelude.flip (Prelude.$))
-                                                        __ (\_ ->
-                                                        let {
-                                                         _evar_0_0 = \_ _ ->
+                                         (Prelude.flip (Prelude.$)) __ (\_ ->
+                                           let {
+                                            _evar_0_0 = let {
+                                                         _evar_0_0 = \_ _ _ ->
                                                           (,) (Prelude.Just
                                                           (Build_IntervalDesc
                                                           ivar0
                                                           (Range.rbeg ( r))
-                                                          iend0 ((:) r
+                                                          iend0 iknd0 ((:) r
                                                           rds0)))
                                                           (Prelude.Just
                                                           i1_2)}
                                                         in
-                                                         _evar_0_0 __)}
-                                         in
-                                          _evar_0_0}
+                                                         _evar_0_0 __}
+                                           in
+                                            _evar_0_0)}
                                        in
                                         _evar_0_0 __}
                                      in
@@ -286,38 +282,83 @@
                                    in
                                     _evar_0_0}
                       in
-                       _evar_0_0 __ __}}
+                       _evar_0_0 __}}
                   in
                   let {
-                   _evar_0_1 = \_ ->
-                    let {
-                     _evar_0_1 = \_ _ _ -> (,) (Prelude.Just
-                      (Build_IntervalDesc iv (Range.rbeg ( r))
-                      (Range.rend ( (Prelude.last rs0))) ((:) r rs0)))
-                      Prelude.Nothing}
-                    in
-                     _evar_0_1 __}
+                   _evar_0_1 = \_ _ _ ->
+                    case i1_1 of {
+                     Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 ->
+                      let {
+                       _evar_0_1 = let {
+                                    _evar_0_1 = \_ ->
+                                     (Prelude.flip (Prelude.$)) __ (\_ ->
+                                       (Prelude.flip (Prelude.$)) __ (\_ ->
+                                         let {
+                                          _evar_0_1 = \_ ->
+                                           let {
+                                            _evar_0_1 = \_ -> (,)
+                                             (Prelude.Just
+                                             (Build_IntervalDesc ivar0
+                                             (Range.rbeg ( r)) iend0 iknd0
+                                             ((:) r rds0))) Prelude.Nothing}
+                                           in
+                                            _evar_0_1 __}
+                                         in
+                                          _evar_0_1 __))}
+                                   in
+                                    _evar_0_1}
+                      in
+                       _evar_0_1 __}}
                   in
                   case _top_assumption_4 of {
-                   Prelude.Just x -> (\_ _ -> _evar_0_0 x);
+                   Prelude.Just x -> (\_ -> _evar_0_0 x);
                    Prelude.Nothing -> _evar_0_1}}
                 in
                 let {
                  _evar_0_1 = \_top_assumption_4 ->
                   let {
                    _evar_0_1 = \i1_2 ->
-                    let {
-                     _evar_0_1 = \_ _ _ -> (,) (Prelude.Just
-                      (Build_IntervalDesc iv ib (Range.rend ( r)) ((:[]) r)))
-                      (Prelude.Just (Build_IntervalDesc iv
-                      (Range.rbeg ( (Prelude.head rs0)))
-                      (Range.rend ( (Prelude.last rs0))) rs0))}
-                    in
-                     _evar_0_1 __}
+                    case i1_2 of {
+                     Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 ->
+                      let {
+                       _evar_0_1 = let {
+                                    _evar_0_1 = \_ ->
+                                     let {
+                                      _evar_0_1 = \_ _ ->
+                                       let {
+                                        _evar_0_1 = \_ ->
+                                         let {
+                                          _evar_0_1 = \_ ->
+                                           let {
+                                            _evar_0_1 = \_ ->
+                                             (Prelude.flip (Prelude.$)) __
+                                               (\_ -> (,) (Prelude.Just
+                                               (Build_IntervalDesc iv
+                                               (Range.rbeg ( r0))
+                                               (Range.rend ( r0)) lknd ((:[])
+                                               ( r0)))) (Prelude.Just
+                                               (Build_IntervalDesc ivar0
+                                               (Range.rbeg
+                                                 ( (Prelude.head rds0)))
+                                               (Range.rend
+                                                 ( (Prelude.last rds0)))
+                                               iknd0 rds0)))}
+                                           in
+                                            _evar_0_1 __}
+                                         in
+                                          _evar_0_1 __}
+                                       in
+                                        _evar_0_1 __}
+                                     in
+                                      _evar_0_1 __ __}
+                                   in
+                                    _evar_0_1}
+                      in
+                       _evar_0_1 __}}
                   in
                   let {_evar_0_2 = \_ _ _ -> Logic.coq_False_rec} in
                   case _top_assumption_4 of {
-                   Prelude.Just x -> (\_ -> _evar_0_1 x);
+                   Prelude.Just x -> (\_ _ _ -> _evar_0_1 x);
                    Prelude.Nothing -> _evar_0_2}}
                 in
                 case _top_assumption_3 of {
@@ -329,72 +370,42 @@
             in
              _evar_0_0 __}
           in
-           _evar_0_0 __}
+          case _top_assumption_1 of {
+           Prelude.Just x -> (\_ -> _evar_0_ x);
+           Prelude.Nothing -> _evar_0_0}}
         in
-        case _top_assumption_1 of {
-         Prelude.Just x -> (\_ -> _evar_0_ x);
-         Prelude.Nothing -> _evar_0_0}}
-      in
-      let {
-       _evar_0_0 = \_top_assumption_1 ->
         let {
-         _evar_0_0 = \r1 ->
+         _evar_0_0 = \_top_assumption_1 ->
           let {
-           _evar_0_0 = \_ -> (,) Prelude.Nothing (Prelude.Just
-            (Build_IntervalDesc iv ib ie ((:) r rs0)))}
+           _evar_0_0 = \r1 ->
+            let {
+             _evar_0_0 = \_ ->
+              let {
+               _evar_0_0 = \_ ->
+                let {
+                 _evar_0_0 = \_ -> (,) Prelude.Nothing (Prelude.Just
+                  (Build_IntervalDesc iv (Range.rbeg ( r1))
+                  (Range.rend ( (Prelude.last rs0))) knd ((:) r1 rs0)))}
+                in
+                 _evar_0_0 __}
+              in
+               _evar_0_0 __}
+            in
+             _evar_0_0 __}
           in
-           _evar_0_0 __}
-        in
-        let {_evar_0_1 = \_ -> Logic.coq_False_rec} in
-        case _top_assumption_1 of {
-         Prelude.Just x -> (\_ -> _evar_0_0 x);
-         Prelude.Nothing -> _evar_0_1}}
-      in
-      case _top_assumption_0 of {
-       Prelude.Just x -> _evar_0_ x;
-       Prelude.Nothing -> _evar_0_0}}
-    in
-    case _top_assumption_ of {
-     (,) x x0 -> _evar_0_ x x0 __})
-    rs
-
-splitInterval :: Prelude.Int -> IntervalDesc ->
-                 ((,) IntervalDesc IntervalDesc)
-splitInterval before d =
-  let {
-   _evar_0_ = \iv ib ie rds0 ->
-    let {_top_assumption_ = intervalSpan rds0 before iv ib ie} in
-    let {
-     _evar_0_ = \_top_assumption_0 ->
-      let {
-       _evar_0_ = \i0 _top_assumption_1 ->
-        let {_evar_0_ = \i1 -> (,) i0 i1} in
-        let {
-         _evar_0_0 = \_ ->
-          let {_evar_0_0 = \_ -> Logic.coq_False_rec} in  _evar_0_0 __}
+          let {_evar_0_1 = \_ -> Logic.coq_False_rec} in
+          case _top_assumption_1 of {
+           Prelude.Just x -> (\_ -> _evar_0_0 x);
+           Prelude.Nothing -> _evar_0_1}}
         in
-        case _top_assumption_1 of {
-         Prelude.Just x -> (\_ -> _evar_0_ x);
+        case _top_assumption_0 of {
+         Prelude.Just x -> _evar_0_ x;
          Prelude.Nothing -> _evar_0_0}}
       in
-      let {
-       _evar_0_0 = \_top_assumption_1 ->
-        let {
-         _evar_0_0 = \i1 ->
-          let {_evar_0_0 = \_ -> Logic.coq_False_rec} in  _evar_0_0 __}
-        in
-        let {_evar_0_1 = \_ -> Logic.coq_False_rec} in
-        case _top_assumption_1 of {
-         Prelude.Just x -> (\_ -> _evar_0_0 x);
-         Prelude.Nothing -> _evar_0_1}}
-      in
-      case _top_assumption_0 of {
-       Prelude.Just x -> _evar_0_ x;
-       Prelude.Nothing -> _evar_0_0}}
-    in
-    case _top_assumption_ of {
-     (,) x x0 -> _evar_0_ x x0 __}}
+      case _top_assumption_ of {
+       (,) x x0 -> _evar_0_ x x0 __})
+      rs}
   in
-  case d of {
-   Build_IntervalDesc x x0 x1 x2 -> _evar_0_ x x0 x1 x2}
+  case splitKind knd of {
+   (,) x x0 -> _evar_0_ x x0}
 
diff --git a/LinearScan/Lib.hs b/LinearScan/Lib.hs
--- a/LinearScan/Lib.hs
+++ b/LinearScan/Lib.hs
@@ -2,12 +2,12 @@
 
 
 import qualified Prelude
+import qualified Data.IntMap
 import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
-import qualified LinearScan.Logic as Logic
 import qualified LinearScan.Specif as Specif
 import qualified LinearScan.Eqtype as Eqtype
 
@@ -15,16 +15,6 @@
 __ :: any
 __ = Prelude.error "Logical or arity value used"
 
-ex_falso_quodlibet :: a1
-ex_falso_quodlibet =
-  Logic.coq_False_rect
-
-fromMaybe :: a1 -> (Prelude.Maybe a1) -> a1
-fromMaybe d mx =
-  case mx of {
-   Prelude.Just x -> x;
-   Prelude.Nothing -> d}
-
 option_map :: (a1 -> a2) -> (Prelude.Maybe a1) -> Prelude.Maybe a2
 option_map f x =
   case x of {
@@ -37,6 +27,10 @@
    Prelude.Just a -> x;
    Prelude.Nothing -> y}
 
+forFold :: a2 -> ([] a1) -> (a2 -> a1 -> a2) -> a2
+forFold b v f =
+  Data.List.foldl' f b v
+
 foldl_with_index :: (Prelude.Int -> a2 -> a1 -> a2) -> a2 -> ([] a1) -> a2
 foldl_with_index f b v =
   let {
@@ -46,16 +40,6 @@
       (:) y ys -> go ((Prelude.succ) n) ys (f n z y)}}
   in go 0 v b
 
-mapAccumL :: (a1 -> a2 -> (,) a1 a3) -> a1 -> ([] a2) -> (,) a1 ([] a3)
-mapAccumL f s v =
-  case v of {
-   [] -> (,) s [];
-   (:) x xs ->
-    case f s x of {
-     (,) s' y ->
-      case mapAccumL f s' xs of {
-       (,) s'' ys -> (,) s'' ((:) y ys)}}}
-
 dep_foldl_inv :: (a1 -> Eqtype.Equality__Coq_type) -> a1 -> ([]
                  Eqtype.Equality__Coq_sort) -> Prelude.Int -> (a1 -> []
                  Eqtype.Equality__Coq_sort) -> (a1 -> a1 -> () ->
@@ -70,7 +54,7 @@
     case l of {
      [] -> b;
      (:) y ys ->
-      (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
+      (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
         (\_ ->
         b)
         (\n' ->
@@ -93,7 +77,7 @@
     case l of {
      [] -> Prelude.Right b;
      (:) y ys ->
-      (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
+      (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
         (\_ -> Prelude.Right
         b)
         (\n' ->
diff --git a/LinearScan/Logic.hs b/LinearScan/Logic.hs
--- a/LinearScan/Logic.hs
+++ b/LinearScan/Logic.hs
@@ -2,6 +2,7 @@
 
 
 import qualified Prelude
+import qualified Data.IntMap
 import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Functor.Identity
diff --git a/LinearScan/Main.hs b/LinearScan/Main.hs
--- a/LinearScan/Main.hs
+++ b/LinearScan/Main.hs
@@ -5,1696 +5,2394 @@
 
 
 import qualified Prelude
-import qualified Data.List
-import qualified Data.Ord
-import qualified Data.Functor.Identity
-import qualified LinearScan.Utils
-
-import qualified LinearScan.Datatypes as Datatypes
-import qualified LinearScan.IApplicative as IApplicative
-import qualified LinearScan.IEndo as IEndo
-import qualified LinearScan.IMonad as IMonad
-import qualified LinearScan.IState as IState
-import qualified LinearScan.Interval as Interval
-import qualified LinearScan.Lib as Lib
-import qualified LinearScan.Logic as Logic
-import qualified LinearScan.NonEmpty0 as NonEmpty0
-import qualified LinearScan.Range as Range
-import qualified LinearScan.Specif as Specif
-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
-
-
-
---unsafeCoerce :: a -> b
-#ifdef __GLASGOW_HASKELL__
-import qualified GHC.Base as GHC.Base
-unsafeCoerce = GHC.Base.unsafeCoerce#
-#else
--- HUGS
-import qualified LinearScan.IOExts as IOExts
-unsafeCoerce = IOExts.unsafeCoerce
-#endif
-
-__ :: any
-__ = Prelude.error "Logical or arity value used"
-
-_MyMachine__maxReg :: Prelude.Int
-_MyMachine__maxReg = 32
-
-type MyMachine__PhysReg = Prelude.Int
-
-maxReg :: Prelude.Int
-maxReg =
-  _MyMachine__maxReg
-
-type PhysReg = Prelude.Int
-
-data SSError =
-   ECannotSplitSingleton Prelude.Int
- | ECannotSplitAssignedSingleton Prelude.Int
- | ENoIntervalsToSplit
- | ERegisterAlreadyAssigned Prelude.Int
- | ERegisterAssignmentsOverlap Prelude.Int
-
-coq_SSError_rect :: (Prelude.Int -> a1) -> (Prelude.Int -> a1) ->
-                               a1 -> (Prelude.Int -> a1) -> (Prelude.Int ->
-                               a1) -> SSError -> a1
-coq_SSError_rect f f0 f1 f2 f3 s =
-  case s of {
-   ECannotSplitSingleton x -> f x;
-   ECannotSplitAssignedSingleton x -> f0 x;
-   ENoIntervalsToSplit -> f1;
-   ERegisterAlreadyAssigned x -> f2 x;
-   ERegisterAssignmentsOverlap x -> f3 x}
-
-coq_SSError_rec :: (Prelude.Int -> a1) -> (Prelude.Int -> a1) ->
-                              a1 -> (Prelude.Int -> a1) -> (Prelude.Int ->
-                              a1) -> SSError -> a1
-coq_SSError_rec =
-  coq_SSError_rect
-
-stbind :: (a4 -> IState.IState SSError a2 a3 a5) ->
-                     (IState.IState SSError a1 a2 a4) ->
-                     IState.IState SSError a1 a3 a5
-stbind f x =
-  IMonad.ijoin (unsafeCoerce IState.coq_IState_IMonad)
-    (IEndo.imap (unsafeCoerce IState.coq_IState_IFunctor) f (unsafeCoerce x))
-
-error_ :: SSError -> IState.IState SSError 
-                     a1 a1 a2
-error_ err x =
-  Prelude.Left err
-
-return_ :: a2 -> IState.IState SSError a1 a1 a2
-return_ =
-  IApplicative.ipure (unsafeCoerce IState.coq_IState_IApplicative)
-
-type Coq_fixedIntervalsType =
-  [] (Prelude.Maybe Interval.IntervalDesc)
-
-data ScanStateDesc =
-   Build_ScanStateDesc Prelude.Int ([] Interval.IntervalDesc) 
- Coq_fixedIntervalsType ([] ((,) Prelude.Int Prelude.Int)) 
- ([] ((,) Prelude.Int PhysReg)) ([]
-                                          ((,) Prelude.Int PhysReg)) 
- ([] ((,) Prelude.Int PhysReg))
-
-coq_ScanStateDesc_rect :: (Prelude.Int -> ([]
-                                     Interval.IntervalDesc) ->
-                                     Coq_fixedIntervalsType -> ([]
-                                     ((,) Prelude.Int Prelude.Int)) -> ([]
-                                     ((,) Prelude.Int PhysReg)) ->
-                                     ([] ((,) Prelude.Int PhysReg))
-                                     -> ([]
-                                     ((,) Prelude.Int PhysReg)) ->
-                                     a1) -> ScanStateDesc -> a1
-coq_ScanStateDesc_rect f s =
-  case s of {
-   Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 -> f x x0 x1 x2 x3 x4 x5}
-
-coq_ScanStateDesc_rec :: (Prelude.Int -> ([]
-                                    Interval.IntervalDesc) ->
-                                    Coq_fixedIntervalsType -> ([]
-                                    ((,) Prelude.Int Prelude.Int)) -> ([]
-                                    ((,) Prelude.Int PhysReg)) ->
-                                    ([] ((,) Prelude.Int PhysReg))
-                                    -> ([]
-                                    ((,) Prelude.Int PhysReg)) ->
-                                    a1) -> ScanStateDesc -> a1
-coq_ScanStateDesc_rec =
-  coq_ScanStateDesc_rect
-
-nextInterval :: ScanStateDesc -> Prelude.Int
-nextInterval s =
-  case s of {
-   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
-    unhandled0 active0 inactive0 handled0 -> nextInterval0}
-
-type IntervalId = Prelude.Int
-
-intervals :: ScanStateDesc -> [] Interval.IntervalDesc
-intervals s =
-  case s of {
-   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
-    unhandled0 active0 inactive0 handled0 -> intervals0}
-
-fixedIntervals :: ScanStateDesc ->
-                             Coq_fixedIntervalsType
-fixedIntervals s =
-  case s of {
-   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
-    unhandled0 active0 inactive0 handled0 -> fixedIntervals0}
-
-unhandled :: ScanStateDesc -> []
-                        ((,) IntervalId Prelude.Int)
-unhandled s =
-  case s of {
-   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
-    unhandled0 active0 inactive0 handled0 -> unhandled0}
-
-active :: ScanStateDesc -> []
-                     ((,) IntervalId PhysReg)
-active s =
-  case s of {
-   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
-    unhandled0 active0 inactive0 handled0 -> active0}
-
-inactive :: ScanStateDesc -> []
-                       ((,) IntervalId PhysReg)
-inactive s =
-  case s of {
-   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
-    unhandled0 active0 inactive0 handled0 -> inactive0}
-
-handled :: ScanStateDesc -> []
-                      ((,) IntervalId PhysReg)
-handled s =
-  case s of {
-   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
-    unhandled0 active0 inactive0 handled0 -> handled0}
-
-unhandledIds :: ScanStateDesc -> [] IntervalId
-unhandledIds s =
-  Prelude.map (\i -> Prelude.fst i) (unhandled s)
-
-activeIds :: ScanStateDesc -> [] IntervalId
-activeIds s =
-  Prelude.map (\i -> Prelude.fst i) (active s)
-
-inactiveIds :: ScanStateDesc -> [] IntervalId
-inactiveIds s =
-  Prelude.map (\i -> Prelude.fst i) (inactive s)
-
-handledIds :: ScanStateDesc -> [] IntervalId
-handledIds s =
-  Prelude.map (\i -> Prelude.fst i) (handled s)
-
-all_state_lists :: ScanStateDesc -> []
-                              IntervalId
-all_state_lists s =
-  (Prelude.++) (unhandledIds s)
-    ((Prelude.++) (activeIds s)
-      ((Prelude.++) (inactiveIds s) (handledIds s)))
-
-totalExtent :: ScanStateDesc -> ([]
-                          IntervalId) -> Prelude.Int
-totalExtent sd xs =
-  Data.List.sum
-    (Prelude.map (\i ->
-      Interval.intervalExtent
-        (
-          (LinearScan.Utils.nth (nextInterval sd)
-            (intervals sd) i))) xs)
-
-unhandledExtent :: ScanStateDesc -> Prelude.Int
-unhandledExtent sd =
-  totalExtent sd
-    (Prelude.map (\i -> Prelude.fst i) (unhandled sd))
-
-registerWithHighestPos :: ([] (Prelude.Maybe Prelude.Int)) -> (,)
-                                     Prelude.Int (Prelude.Maybe Prelude.Int)
-registerWithHighestPos =
-  (LinearScan.Utils.vfoldl'_with_index) maxReg (\reg res x ->
-    case res of {
-     (,) r o ->
-      case o of {
-       Prelude.Just n ->
-        case x of {
-         Prelude.Just m ->
-          case (Prelude.<=) ((Prelude.succ) n) m of {
-           Prelude.True -> (,) reg (Prelude.Just m);
-           Prelude.False -> (,) r (Prelude.Just n)};
-         Prelude.Nothing -> (,) reg Prelude.Nothing};
-       Prelude.Nothing -> (,) r Prelude.Nothing}}) ((,) ( 0) (Prelude.Just
-    0))
-
-getScanStateDesc :: ScanStateDesc ->
-                               ScanStateDesc
-getScanStateDesc sd =
-  sd
-
-packScanState :: ScanStateDesc ->
-                            ScanStateDesc
-packScanState sd =
-  sd
-
-coq_ScanStateCursor_rect :: ScanStateDesc -> (() -> ()
-                                       -> a1) -> a1
-coq_ScanStateCursor_rect sd f =
-  f __ __
-
-coq_ScanStateCursor_rec :: ScanStateDesc -> (() -> () ->
-                                      a1) -> a1
-coq_ScanStateCursor_rec sd f =
-  coq_ScanStateCursor_rect sd f
-
-curId :: ScanStateDesc -> (,) IntervalId
-                    Prelude.Int
-curId sd =
-  Prelude.head (unhandled sd)
-
-curIntDetails :: ScanStateDesc -> Interval.IntervalDesc
-curIntDetails sd =
-  LinearScan.Utils.nth (nextInterval sd) (intervals sd)
-    (Prelude.fst (curId sd))
-
-curPosition :: ScanStateDesc -> Prelude.Int
-curPosition sd =
-  Interval.intervalStart ( (curIntDetails sd))
-
-data VarKind =
-   Input
- | Temp
- | Output
-
-coq_VarKind_rect :: a1 -> a1 -> a1 -> VarKind -> a1
-coq_VarKind_rect f f0 f1 v =
-  case v of {
-   Input -> f;
-   Temp -> f0;
-   Output -> f1}
-
-coq_VarKind_rec :: a1 -> a1 -> a1 -> VarKind -> a1
-coq_VarKind_rec =
-  coq_VarKind_rect
-
-data Allocation =
-   Unallocated
- | Register PhysReg
- | Spill deriving (Prelude.Show, Prelude.Eq)
-
-coq_Allocation_rect :: a1 -> (PhysReg -> a1) -> a1 ->
-                                  Allocation -> a1
-coq_Allocation_rect f f0 f1 a =
-  case a of {
-   Unallocated -> f;
-   Register x -> f0 x;
-   Spill -> f1}
-
-coq_Allocation_rec :: a1 -> (PhysReg -> a1) -> a1 ->
-                                 Allocation -> a1
-coq_Allocation_rec =
-  coq_Allocation_rect
-
-data VarInfo =
-   Build_VarInfo Prelude.Int VarKind Allocation 
- Prelude.Bool
-
-coq_VarInfo_rect :: (Prelude.Int -> VarKind ->
-                               Allocation -> Prelude.Bool -> a1) ->
-                               VarInfo -> a1
-coq_VarInfo_rect f v =
-  case v of {
-   Build_VarInfo x x0 x1 x2 -> f x x0 x1 x2}
-
-coq_VarInfo_rec :: (Prelude.Int -> VarKind ->
-                              Allocation -> Prelude.Bool -> a1) ->
-                              VarInfo -> a1
-coq_VarInfo_rec =
-  coq_VarInfo_rect
-
-varId :: VarInfo -> Prelude.Int
-varId v =
-  case v of {
-   Build_VarInfo varId0 varKind0 varAlloc0 regRequired0 -> varId0}
-
-varKind :: VarInfo -> VarKind
-varKind v =
-  case v of {
-   Build_VarInfo varId0 varKind0 varAlloc0 regRequired0 -> varKind0}
-
-varAlloc :: VarInfo -> Allocation
-varAlloc v =
-  case v of {
-   Build_VarInfo varId0 varKind0 varAlloc0 regRequired0 ->
-    varAlloc0}
-
-regRequired :: VarInfo -> Prelude.Bool
-regRequired v =
-  case v of {
-   Build_VarInfo varId0 varKind0 varAlloc0 regRequired0 ->
-    regRequired0}
-
-data OpKind =
-   Normal
- | LoopBegin
- | LoopEnd
- | Call
-
-coq_OpKind_rect :: a1 -> a1 -> a1 -> a1 -> OpKind -> a1
-coq_OpKind_rect f f0 f1 f2 o =
-  case o of {
-   Normal -> f;
-   LoopBegin -> f0;
-   LoopEnd -> f1;
-   Call -> f2}
-
-coq_OpKind_rec :: a1 -> a1 -> a1 -> a1 -> OpKind -> a1
-coq_OpKind_rec =
-  coq_OpKind_rect
-
-data OpInfo =
-   Build_OpInfo Prelude.Int Prelude.Int OpKind ([]
-                                                                   VarInfo) 
- ([] PhysReg)
-
-coq_OpInfo_rect :: (Prelude.Int -> Prelude.Int -> OpKind
-                              -> ([] VarInfo) -> ([]
-                              PhysReg) -> a1) -> OpInfo
-                              -> a1
-coq_OpInfo_rect f o =
-  case o of {
-   Build_OpInfo x x0 x1 x2 x3 -> f x x0 x1 x2 x3}
-
-coq_OpInfo_rec :: (Prelude.Int -> Prelude.Int -> OpKind
-                             -> ([] VarInfo) -> ([]
-                             PhysReg) -> a1) -> OpInfo ->
-                             a1
-coq_OpInfo_rec =
-  coq_OpInfo_rect
-
-opId :: OpInfo -> Prelude.Int
-opId o =
-  case o of {
-   Build_OpInfo opId0 opMeta0 opKind0 varRefs0 regRefs0 -> opId0}
-
-opMeta :: OpInfo -> Prelude.Int
-opMeta o =
-  case o of {
-   Build_OpInfo opId0 opMeta0 opKind0 varRefs0 regRefs0 -> opMeta0}
-
-opKind :: OpInfo -> OpKind
-opKind o =
-  case o of {
-   Build_OpInfo opId0 opMeta0 opKind0 varRefs0 regRefs0 -> opKind0}
-
-varRefs :: OpInfo -> [] VarInfo
-varRefs o =
-  case o of {
-   Build_OpInfo opId0 opMeta0 opKind0 varRefs0 regRefs0 -> varRefs0}
-
-regRefs :: OpInfo -> [] PhysReg
-regRefs o =
-  case o of {
-   Build_OpInfo opId0 opMeta0 opKind0 varRefs0 regRefs0 -> regRefs0}
-
-data BlockInfo =
-   Build_BlockInfo Prelude.Int ([] OpInfo)
-
-coq_BlockInfo_rect :: (Prelude.Int -> ([] OpInfo) -> a1)
-                                 -> BlockInfo -> a1
-coq_BlockInfo_rect f b =
-  case b of {
-   Build_BlockInfo x x0 -> f x x0}
-
-coq_BlockInfo_rec :: (Prelude.Int -> ([] OpInfo) -> a1)
-                                -> BlockInfo -> a1
-coq_BlockInfo_rec =
-  coq_BlockInfo_rect
-
-blockId :: BlockInfo -> Prelude.Int
-blockId b =
-  case b of {
-   Build_BlockInfo blockId0 blockOps0 -> blockId0}
-
-blockOps :: BlockInfo -> [] OpInfo
-blockOps b =
-  case b of {
-   Build_BlockInfo blockId0 blockOps0 -> blockOps0}
-
-type BlockList = [] BlockInfo
-
-type BoundedRange = Range.RangeDesc
-
-transportBoundedRange :: Prelude.Int -> Prelude.Int ->
-                                    BoundedRange ->
-                                    BoundedRange
-transportBoundedRange base prev x =
-  x
-
-data BuildState =
-   Build_BuildState Prelude.Int ([]
-                                          (Prelude.Maybe
-                                          BoundedRange)) ([]
-                                                                   (Prelude.Maybe
-                                                                   BoundedRange))
-
-coq_BuildState_rect :: (Prelude.Int -> ([]
-                                  (Prelude.Maybe BoundedRange)) ->
-                                  ([] (Prelude.Maybe BoundedRange))
-                                  -> a1) -> BuildState -> a1
-coq_BuildState_rect f b =
-  case b of {
-   Build_BuildState x x0 x1 -> f x x0 x1}
-
-coq_BuildState_rec :: (Prelude.Int -> ([]
-                                 (Prelude.Maybe BoundedRange)) ->
-                                 ([] (Prelude.Maybe BoundedRange))
-                                 -> a1) -> BuildState -> a1
-coq_BuildState_rec =
-  coq_BuildState_rect
-
-bsPos :: BuildState -> Prelude.Int
-bsPos b =
-  case b of {
-   Build_BuildState bsPos0 bsVars0 bsRegs0 -> bsPos0}
-
-bsVars :: BuildState -> []
-                     (Prelude.Maybe BoundedRange)
-bsVars b =
-  case b of {
-   Build_BuildState bsPos0 bsVars0 bsRegs0 -> bsVars0}
-
-bsRegs :: BuildState -> []
-                     (Prelude.Maybe BoundedRange)
-bsRegs b =
-  case b of {
-   Build_BuildState bsPos0 bsVars0 bsRegs0 -> bsRegs0}
-
-foldOps :: (a1 -> OpInfo -> a1) -> a1 ->
-                      BlockList -> a1
-foldOps f z =
-  Data.List.foldl' (\bacc blk ->
-    Data.List.foldl' f bacc (blockOps blk)) z
-
-foldOpsRev :: (a1 -> OpInfo -> a1) -> a1 ->
-                         BlockList -> a1
-foldOpsRev f z blocks =
-  Data.List.foldl' (\bacc blk ->
-    Data.List.foldl' f bacc (Seq.rev (blockOps blk))) z
-    (Seq.rev ( blocks))
-
-mapAccumLOps :: (a1 -> OpInfo -> (,) a1
-                           OpInfo) -> a1 -> BlockList ->
-                           (,) a1 BlockList
-mapAccumLOps f =
-  NonEmpty0.coq_NE_mapAccumL (\z blk ->
-    case Lib.mapAccumL f z (blockOps blk) of {
-     (,) z' ops -> (,) z' (Build_BlockInfo (blockId blk)
-      ops)})
-
-processOperations :: BlockList -> BuildState
-processOperations blocks =
-  (Prelude.flip (Prelude.$))
-    (foldOps (\x op ->
-      case x of {
-       (,) n m -> (,) ((Prelude.succ) n)
-        (Data.List.foldl' (\m0 v -> Prelude.max m0 (varId v)) m
-          (varRefs op))}) ((,) 0 0) blocks) (\_top_assumption_ ->
-    let {
-     _evar_0_ = \opCount highestVar ->
-      let {
-       z = Build_BuildState opCount
-        (Seq.nseq ((Prelude.succ) highestVar) Prelude.Nothing)
-        (Data.List.replicate maxReg Prelude.Nothing)}
-      in
-      foldOpsRev (\_top_assumption_0 ->
-        let {
-         _evar_0_ = \pos vars regs op ->
-          (Prelude.flip (Prelude.$)) __ (\_ ->
-            let {
-             _evar_0_ = \vars0 regs0 -> Build_BuildState 0 vars0
-              regs0}
-            in
-            let {
-             _evar_0_0 = \pos0 vars0 regs0 -> Build_BuildState pos0
-              ((Prelude.flip (Prelude.$))
-                ((Prelude.flip (Prelude.$)) vars0 (\vars' ->
-                  let {
-                   vars'0 = Prelude.map
-                              (Lib.option_map
-                                (transportBoundedRange
-                                  ((Prelude.succ) (Ssrnat.double pos0))
-                                  ((Prelude.succ)
-                                  (Ssrnat.double ((Prelude.succ) pos0)))))
-                              vars'}
-                  in
-                  Data.List.foldl' (\vars'1 v ->
-                    let {
-                     upos = Range.Build_UsePos ((Prelude.succ)
-                      (Ssrnat.double pos0)) (regRequired v)}
-                    in
-                    (Prelude.flip (Prelude.$)) __ (\_ ->
-                      Seq.set_nth Prelude.Nothing vars'1 (varId v)
-                        (Prelude.Just
-                        (let {
-                          _evar_0_0 = \_top_assumption_1 ->
-                           Range.Build_RangeDesc (Range.uloc upos)
-                           (Range.rend ( _top_assumption_1)) ((:) upos
-                           (Range.ups ( _top_assumption_1)))}
-                         in
-                         let {
-                          _evar_0_1 = Range.Build_RangeDesc (Range.uloc upos)
-                           ((Prelude.succ) (Range.uloc upos)) ((:[]) upos)}
-                         in
-                         case Seq.nth Prelude.Nothing vars0
-                                (varId v) of {
-                          Prelude.Just x -> _evar_0_0 x;
-                          Prelude.Nothing -> _evar_0_1})))) vars'0
-                    (varRefs op))) (\x -> x))
-              ((Prelude.flip (Prelude.$))
-                ((Prelude.flip (Prelude.$)) regs0 (\regs' ->
-                  let {
-                   regs'0 = LinearScan.Utils.vmap maxReg
-                              (Lib.option_map
-                                (transportBoundedRange
-                                  ((Prelude.succ) (Ssrnat.double pos0))
-                                  ((Prelude.succ)
-                                  (Ssrnat.double ((Prelude.succ) pos0)))))
-                              regs'}
-                  in
-                  Data.List.foldl' (\regs'1 reg ->
-                    let {
-                     upos = Range.Build_UsePos ((Prelude.succ)
-                      (Ssrnat.double pos0)) Prelude.True}
-                    in
-                    (Prelude.flip (Prelude.$)) __ (\_ ->
-                      LinearScan.Utils.set_nth maxReg regs'1 reg
-                        (Prelude.Just
-                        (let {
-                          _evar_0_0 = \_top_assumption_1 ->
-                           Range.Build_RangeDesc (Range.uloc upos)
-                           (Range.rend ( _top_assumption_1)) ((:) upos
-                           (Range.ups ( _top_assumption_1)))}
-                         in
-                         let {
-                          _evar_0_1 = Range.Build_RangeDesc (Range.uloc upos)
-                           ((Prelude.succ) (Range.uloc upos)) ((:[]) upos)}
-                         in
-                         case LinearScan.Utils.nth maxReg regs0
-                                reg of {
-                          Prelude.Just x -> _evar_0_0 x;
-                          Prelude.Nothing -> _evar_0_1})))) regs'0
-                    (regRefs op))) (\x -> x))}
-            in
-            (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
-              (\_ ->
-              _evar_0_ vars regs)
-              (\x ->
-              _evar_0_0 x vars regs)
-              pos)}
-        in
-        case _top_assumption_0 of {
-         Build_BuildState x x0 x1 -> _evar_0_ x x0 x1}) z blocks}
-    in
-    case _top_assumption_ of {
-     (,) x x0 -> _evar_0_ x x0})
-
-computeBlockOrder :: IState.IState SSError
-                                BlockList BlockList 
-                                ()
-computeBlockOrder =
-  return_ ()
-
-numberOperations :: IState.IState SSError
-                               BlockList BlockList 
-                               ()
-numberOperations =
-  let {
-   f = \n op -> (,) ((Prelude.succ) ((Prelude.succ) n))
-    (Build_OpInfo n (opMeta op) (opKind op)
-    (varRefs op) (regRefs op))}
-  in
-  IState.imodify
-    ((Prelude..) Prelude.snd (mapAccumLOps f ((Prelude.succ) 0)))
-
-type BlockState a =
-  IState.IState SSError BlockList BlockList a
-
-computeLocalLiveSets :: BlockState ()
-computeLocalLiveSets =
-  return_ ()
-
-computeGlobalLiveSets :: BlockState ()
-computeGlobalLiveSets =
-  return_ ()
-
-buildIntervals :: IState.IState SSError
-                             BlockList BlockList
-                             ScanStateDesc
-buildIntervals =
-  let {
-   mkint = \vid ss pos mx f ->
-    case mx of {
-     Prelude.Just b ->
-      f ss __ (Interval.Build_IntervalDesc vid (Range.rbeg ( b))
-        (Range.rend ( b)) ((:[]) ( b))) __;
-     Prelude.Nothing -> ss}}
-  in
-  let {
-   handleVar = \pos vid ss mx ->
-    (Prelude.$) (mkint vid ss pos mx) (\sd _ d _ ->
-      packScanState (Build_ScanStateDesc ((Prelude.succ)
-        (nextInterval sd))
-        (LinearScan.Utils.snoc (nextInterval sd)
-          (intervals sd) d) (fixedIntervals sd)
-        (Data.List.insertBy (Data.Ord.comparing Prelude.snd) ((,)
-          ( (nextInterval sd)) (Interval.ibeg d))
-          (Prelude.map Prelude.id (unhandled sd)))
-        (Prelude.map Prelude.id (active sd))
-        (Prelude.map Prelude.id (inactive sd))
-        (Prelude.map Prelude.id (handled sd))))}
-  in
-  stbind (\blocks ->
-    let {bs = processOperations blocks} in
-    let {
-     regs = LinearScan.Utils.vmap maxReg (\mr ->
-              case mr of {
-               Prelude.Just y -> Prelude.Just
-                (Interval.packInterval (Interval.Build_IntervalDesc 0
-                  (Range.rbeg ( y)) (Range.rend ( y)) ((:[]) ( y))));
-               Prelude.Nothing -> Prelude.Nothing}) (bsRegs bs)}
-    in
-    let {
-     s2 = packScanState (Build_ScanStateDesc
-            (nextInterval (Build_ScanStateDesc 0 []
-              (Data.List.replicate maxReg Prelude.Nothing) [] []
-              [] []))
-            (intervals (Build_ScanStateDesc 0 []
-              (Data.List.replicate maxReg Prelude.Nothing) [] []
-              [] [])) regs
-            (unhandled (Build_ScanStateDesc 0 []
-              (Data.List.replicate maxReg Prelude.Nothing) [] []
-              [] []))
-            (active (Build_ScanStateDesc 0 []
-              (Data.List.replicate maxReg Prelude.Nothing) [] []
-              [] []))
-            (inactive (Build_ScanStateDesc 0 []
-              (Data.List.replicate maxReg Prelude.Nothing) [] []
-              [] []))
-            (handled (Build_ScanStateDesc 0 []
-              (Data.List.replicate maxReg Prelude.Nothing) [] []
-              [] [])))}
-    in
-    (Prelude.$) return_
-      (Lib.foldl_with_index (handleVar (bsPos bs)) s2
-        (bsVars bs))) IState.iget
-
-resolveDataFlow :: BlockState ()
-resolveDataFlow =
-  return_ ()
-
-mapOps :: (OpInfo -> OpInfo) ->
-                     BlockList -> BlockList
-mapOps f =
-  Prelude.map (\blk -> Build_BlockInfo (blockId blk)
-    (Prelude.map f (blockOps blk)))
-
-assignRegNum :: ScanStateDesc -> IState.IState
-                           SSError BlockList
-                           BlockList ()
-assignRegNum sd =
-  let {
-   ints = (Prelude.++) (handled sd)
-            ((Prelude.++) (active sd) (inactive sd))}
-  in
-  let {
-   f = \op ->
-    let {
-     k = \v ->
-      let {vid = varId v} in
-      let {
-       h = \acc x ->
-        case x of {
-         (,) xid reg ->
-          let {
-           int = Interval.getIntervalDesc
-                   (
-                     (LinearScan.Utils.nth (nextInterval sd)
-                       (intervals sd) xid))}
-          in
-          case (Prelude.&&)
-                 (Eqtype.eq_op Ssrnat.nat_eqType
-                   (unsafeCoerce (Interval.ivar int)) (unsafeCoerce vid))
-                 ((Prelude.&&)
-                   ((Prelude.<=) (Interval.ibeg int) (opId op))
-                   ((Prelude.<=) ((Prelude.succ) (opId op))
-                     (Interval.iend int))) of {
-           Prelude.True -> Build_VarInfo (varId v)
-            (varKind v) (Register reg)
-            (regRequired v);
-           Prelude.False -> acc}}}
-      in
-      Data.List.foldl' h v ints}
-    in
-    Build_OpInfo (opId op) (opMeta op)
-    (opKind op) (Prelude.map k (varRefs op))
-    (regRefs op)}
-  in
-  IState.imodify (mapOps f)
-
-coq_SSMorph_rect :: ScanStateDesc ->
-                               ScanStateDesc -> (() -> () -> () ->
-                               a1) -> a1
-coq_SSMorph_rect sd1 sd2 f =
-  f __ __ __
-
-coq_SSMorph_rec :: ScanStateDesc ->
-                              ScanStateDesc -> (() -> () -> () ->
-                              a1) -> a1
-coq_SSMorph_rec sd1 sd2 f =
-  coq_SSMorph_rect sd1 sd2 f
-
-coq_SSMorphSt_rect :: ScanStateDesc ->
-                                 ScanStateDesc -> (() -> () -> a1)
-                                 -> a1
-coq_SSMorphSt_rect sd1 sd2 f =
-  f __ __
-
-coq_SSMorphSt_rec :: ScanStateDesc ->
-                                ScanStateDesc -> (() -> () -> a1)
-                                -> a1
-coq_SSMorphSt_rec sd1 sd2 f =
-  coq_SSMorphSt_rect sd1 sd2 f
-
-coq_SSMorphLen_rect :: ScanStateDesc ->
-                                  ScanStateDesc -> (() -> () -> a1)
-                                  -> a1
-coq_SSMorphLen_rect sd1 sd2 f =
-  f __ __
-
-coq_SSMorphLen_rec :: ScanStateDesc ->
-                                 ScanStateDesc -> (() -> () -> a1)
-                                 -> a1
-coq_SSMorphLen_rec sd1 sd2 f =
-  coq_SSMorphLen_rect sd1 sd2 f
-
-transportation :: ScanStateDesc ->
-                             ScanStateDesc -> IntervalId
-                             -> IntervalId
-transportation sd1 sd2 x =
-   x
-
-data HasBase p =
-   Build_HasBase
-
-coq_HasBase_rect :: (() -> a2) -> a2
-coq_HasBase_rect f =
-  f __
-
-coq_HasBase_rec :: (() -> a2) -> a2
-coq_HasBase_rec f =
-  coq_HasBase_rect f
-
-coq_SSMorphStLen_rect :: ScanStateDesc ->
-                                    ScanStateDesc -> (() -> () ->
-                                    a1) -> a1
-coq_SSMorphStLen_rect sd1 sd2 f =
-  f __ __
-
-coq_SSMorphStLen_rec :: ScanStateDesc ->
-                                   ScanStateDesc -> (() -> () ->
-                                   a1) -> a1
-coq_SSMorphStLen_rec sd1 sd2 f =
-  coq_SSMorphStLen_rect sd1 sd2 f
-
-coq_SSMorphHasLen_rect :: ScanStateDesc ->
-                                     ScanStateDesc -> (() -> () ->
-                                     a1) -> a1
-coq_SSMorphHasLen_rect sd1 sd2 f =
-  f __ __
-
-coq_SSMorphHasLen_rec :: ScanStateDesc ->
-                                    ScanStateDesc -> (() -> () ->
-                                    a1) -> a1
-coq_SSMorphHasLen_rec sd1 sd2 f =
-  coq_SSMorphHasLen_rect sd1 sd2 f
-
-data HasWork p =
-   Build_HasWork
-
-coq_HasWork_rect :: (() -> a2) -> a2
-coq_HasWork_rect f =
-  f __
-
-coq_HasWork_rec :: (() -> a2) -> a2
-coq_HasWork_rec f =
-  coq_HasWork_rect f
-
-coq_SSMorphStHasLen_rect :: ScanStateDesc ->
-                                       ScanStateDesc -> (() -> ()
-                                       -> a1) -> a1
-coq_SSMorphStHasLen_rect sd1 sd2 f =
-  f __ __
-
-coq_SSMorphStHasLen_rec :: ScanStateDesc ->
-                                      ScanStateDesc -> (() -> () ->
-                                      a1) -> a1
-coq_SSMorphStHasLen_rec sd1 sd2 f =
-  coq_SSMorphStHasLen_rect sd1 sd2 f
-
-coq_SSMorphSplit_rect :: ScanStateDesc ->
-                                    ScanStateDesc -> (() -> () ->
-                                    a1) -> a1
-coq_SSMorphSplit_rect sd1 sd2 f =
-  f __ __
-
-coq_SSMorphSplit_rec :: ScanStateDesc ->
-                                   ScanStateDesc -> (() -> () ->
-                                   a1) -> a1
-coq_SSMorphSplit_rec sd1 sd2 f =
-  coq_SSMorphSplit_rect sd1 sd2 f
-
-data IsSplittable p =
-   Build_IsSplittable
-
-coq_IsSplittable_rect :: (() -> a2) -> a2
-coq_IsSplittable_rect f =
-  f __
-
-coq_IsSplittable_rec :: (() -> a2) -> a2
-coq_IsSplittable_rec f =
-  coq_IsSplittable_rect f
-
-coq_SSMorphStSplit_rect :: ScanStateDesc ->
-                                      ScanStateDesc -> (() -> () ->
-                                      a1) -> a1
-coq_SSMorphStSplit_rect sd1 sd2 f =
-  f __ __
-
-coq_SSMorphStSplit_rec :: ScanStateDesc ->
-                                     ScanStateDesc -> (() -> () ->
-                                     a1) -> a1
-coq_SSMorphStSplit_rec sd1 sd2 f =
-  coq_SSMorphStSplit_rect sd1 sd2 f
-
-data SSInfo p =
-   Build_SSInfo ScanStateDesc p
-
-coq_SSInfo_rect :: ScanStateDesc ->
-                              (ScanStateDesc -> a1 -> () -> a2) ->
-                              (SSInfo a1) -> a2
-coq_SSInfo_rect startDesc f s =
-  case s of {
-   Build_SSInfo x x0 -> f x x0 __}
-
-coq_SSInfo_rec :: ScanStateDesc ->
-                             (ScanStateDesc -> a1 -> () -> a2) ->
-                             (SSInfo a1) -> a2
-coq_SSInfo_rec startDesc =
-  coq_SSInfo_rect startDesc
-
-thisDesc :: ScanStateDesc -> (SSInfo a1) ->
-                       ScanStateDesc
-thisDesc startDesc s =
-  case s of {
-   Build_SSInfo thisDesc0 thisHolds0 -> thisDesc0}
-
-thisHolds :: ScanStateDesc -> (SSInfo 
-                        a1) -> a1
-thisHolds startDesc s =
-  case s of {
-   Build_SSInfo thisDesc0 thisHolds0 -> thisHolds0}
-
-type SState p q a =
-  IState.IState SSError (SSInfo p) (SSInfo q) a
-
-withScanState :: ScanStateDesc ->
-                            (ScanStateDesc -> () ->
-                            SState a2 a3 a1) -> SState 
-                            a2 a3 a1
-withScanState pre f =
-  stbind (\i -> f (thisDesc pre i) __) IState.iget
-
-withScanStatePO :: ScanStateDesc ->
-                              (ScanStateDesc -> () ->
-                              SState () () a1) -> SState
-                              () () a1
-withScanStatePO pre f i =
-  case i of {
-   Build_SSInfo thisDesc0 _ ->
-    let {f0 = f thisDesc0 __} in
-    let {x = Build_SSInfo thisDesc0 __} in
-    let {x0 = f0 x} in
-    case x0 of {
-     Prelude.Left s0 -> Prelude.Left s0;
-     Prelude.Right p -> Prelude.Right
-      (case p of {
-        (,) a0 s0 -> (,) a0
-         (case s0 of {
-           Build_SSInfo thisDesc1 _ -> Build_SSInfo
-            thisDesc1 __})})}}
-
-liftLen :: ScanStateDesc -> (ScanStateDesc ->
-                      SState () () a1) -> SState 
-                      () () a1
-liftLen pre f _top_assumption_ =
-  let {
-   _evar_0_ = \sd ->
-    let {ss = Build_SSInfo sd __} in
-    let {_top_assumption_0 = f sd} in
-    let {_top_assumption_1 = _top_assumption_0 ss} in
-    let {_evar_0_ = \err -> Prelude.Left err} in
-    let {
-     _evar_0_0 = \_top_assumption_2 ->
-      let {
-       _evar_0_0 = \x _top_assumption_3 ->
-        let {
-         _evar_0_0 = \sd' -> Prelude.Right ((,) x (Build_SSInfo sd'
-          __))}
-        in
-        case _top_assumption_3 of {
-         Build_SSInfo x0 x1 -> _evar_0_0 x0}}
-      in
-      case _top_assumption_2 of {
-       (,) x x0 -> _evar_0_0 x x0}}
-    in
-    case _top_assumption_1 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}
-
-weakenStHasLenToSt :: ScanStateDesc -> SState
-                                 () () ()
-weakenStHasLenToSt pre hS =
-  Prelude.Right ((,) ()
-    (case hS of {
-      Build_SSInfo thisDesc0 _ -> Build_SSInfo thisDesc0
-       __}))
-
-withCursor :: ScanStateDesc -> (ScanStateDesc
-                         -> () -> SState a1 a2 a3) ->
-                         SState a1 a2 a3
-withCursor pre f x =
-  case x of {
-   Build_SSInfo thisDesc0 thisHolds0 ->
-    f thisDesc0 __ (Build_SSInfo thisDesc0 thisHolds0)}
-
-moveUnhandledToActive :: ScanStateDesc ->
-                                    PhysReg -> SState 
-                                    a1 () ()
-moveUnhandledToActive pre reg x =
-  case x of {
-   Build_SSInfo thisDesc0 thisHolds0 ->
-    case thisDesc0 of {
-     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
-          (Build_ScanStateDesc nextInterval0 intervals0
-          fixedIntervals0 unhandled1 ((:) ((,) (Prelude.fst p) reg) active0)
-          inactive0 handled0) __))}
-        in
-        let {
-         _evar_0_0 = \_ -> Prelude.Left (ERegisterAlreadyAssigned
-          ( reg))}
-        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 :: ScanStateDesc ->
-                                  Eqtype.Equality__Coq_sort ->
-                                  Specif.Coq_sig2 ScanStateDesc
-moveActiveToHandled sd x =
-  Build_ScanStateDesc (nextInterval sd)
-    (intervals sd) (fixedIntervals sd)
-    (unhandled sd)
-    (unsafeCoerce
-      (Seq.rem
-        (Eqtype.prod_eqType
-          (Fintype.ordinal_eqType (nextInterval sd))
-          (Fintype.ordinal_eqType maxReg)) x
-        (unsafeCoerce (active sd)))) (inactive sd) ((:)
-    (unsafeCoerce x) (handled sd))
-
-moveActiveToInactive :: ScanStateDesc ->
-                                   Eqtype.Equality__Coq_sort ->
-                                   Specif.Coq_sig2 ScanStateDesc
-moveActiveToInactive sd x =
-  Build_ScanStateDesc (nextInterval sd)
-    (intervals sd) (fixedIntervals sd)
-    (unhandled sd)
-    (unsafeCoerce
-      (Seq.rem
-        (Eqtype.prod_eqType
-          (Fintype.ordinal_eqType (nextInterval sd))
-          (Fintype.ordinal_eqType maxReg)) x
-        (unsafeCoerce (active sd)))) ((:) (unsafeCoerce x)
-    (inactive sd)) (handled sd)
-
-moveInactiveToActive :: ScanStateDesc ->
-                                   Eqtype.Equality__Coq_sort ->
-                                   Specif.Coq_sig2 ScanStateDesc
-moveInactiveToActive sd x =
-  Build_ScanStateDesc (nextInterval sd)
-    (intervals sd) (fixedIntervals sd)
-    (unhandled sd) ((:) (unsafeCoerce x) (active sd))
-    (unsafeCoerce
-      (Seq.rem
-        (Eqtype.prod_eqType
-          (Fintype.ordinal_eqType (nextInterval sd))
-          (Fintype.ordinal_eqType maxReg)) x
-        (unsafeCoerce (inactive sd)))) (handled sd)
-
-moveInactiveToHandled :: ScanStateDesc ->
-                                    Eqtype.Equality__Coq_sort ->
-                                    Specif.Coq_sig2 ScanStateDesc
-moveInactiveToHandled sd x =
-  Build_ScanStateDesc (nextInterval sd)
-    (intervals sd) (fixedIntervals sd)
-    (unhandled sd) (active sd)
-    (unsafeCoerce
-      (Seq.rem
-        (Eqtype.prod_eqType
-          (Fintype.ordinal_eqType (nextInterval sd))
-          (Fintype.ordinal_eqType maxReg)) x
-        (unsafeCoerce (inactive sd)))) ((:) (unsafeCoerce x)
-    (handled sd))
-
-distance :: Prelude.Int -> Prelude.Int -> Prelude.Int
-distance n m =
-  case (Prelude.<=) ((Prelude.succ) n) m of {
-   Prelude.True -> (Prelude.-) m n;
-   Prelude.False -> (Prelude.-) n m}
-
-splitCurrentInterval :: ScanStateDesc -> (Prelude.Maybe
-                                   Prelude.Int) -> SState a1 
-                                   () ()
-splitCurrentInterval pre before ssi =
-  let {
-   _evar_0_ = \desc holds ->
-    let {
-     _evar_0_ = \_nextInterval_ intervals0 _fixedIntervals_ unhandled0 _active_ _inactive_ _handled_ ->
-      let {_evar_0_ = \holds0 -> Logic.coq_False_rect} in
-      let {
-       _evar_0_0 = \_top_assumption_ ->
-        let {
-         _evar_0_0 = \uid beg us holds0 ->
-          let {int = LinearScan.Utils.nth _nextInterval_ intervals0 uid} in
-          let {
-           _evar_0_0 = \_ -> Prelude.Left (ECannotSplitSingleton
-            ( uid))}
-          in
-          let {
-           _evar_0_1 = \_ -> Prelude.Right ((,) ()
-            ((Prelude.flip (Prelude.$)) __ (\_ ->
-              let {
-               _top_assumption_0 = Interval.splitPosition ( int) before
-                                     Prelude.True}
-              in
-              let {
-               _top_assumption_1 = Interval.splitInterval _top_assumption_0
-                                     ( int)}
-              in
-              let {
-               _evar_0_1 = \_top_assumption_2 _top_assumption_3 ->
-                let {
-                 _evar_0_1 = \_ ->
-                  (Prelude.flip (Prelude.$)) __ (\_ ->
-                    (Prelude.flip (Prelude.$)) __
-                      ((Prelude.flip (Prelude.$)) __
-                        ((Prelude.flip (Prelude.$)) __ (\_ _ _ ->
-                          (Prelude.flip (Prelude.$)) __
-                            ((Prelude.flip (Prelude.$)) __
-                              (let {
-                                new_unhandled_added = Build_ScanStateDesc
-                                 ((Prelude.succ) _nextInterval_)
-                                 (LinearScan.Utils.snoc _nextInterval_
-                                   (LinearScan.Utils.set_nth _nextInterval_
-                                     intervals0 uid _top_assumption_2)
-                                   _top_assumption_3) _fixedIntervals_
-                                 (Data.List.insertBy
-                                   (Data.Ord.comparing Prelude.snd) ((,)
-                                   ( _nextInterval_)
-                                   (Interval.ibeg _top_assumption_3)) ((:)
-                                   (Prelude.id ((,) uid beg))
-                                   (Prelude.map Prelude.id us)))
-                                 (Prelude.map Prelude.id _active_)
-                                 (Prelude.map Prelude.id _inactive_)
-                                 (Prelude.map Prelude.id _handled_)}
-                               in
-                               \_ _ -> Build_SSInfo
-                               new_unhandled_added __))))))}
-                in
-                 _evar_0_1 __}
-              in
-              case _top_assumption_1 of {
-               (,) x x0 -> _evar_0_1 x x0})))}
-          in
-          case Interval.coq_Interval_is_singleton ( int) of {
-           Prelude.True -> _evar_0_0 __;
-           Prelude.False -> _evar_0_1 __}}
-        in
-        (\us _ _ _ _ _ holds0 _ _ ->
-        case _top_assumption_ of {
-         (,) x x0 -> _evar_0_0 x x0 us holds0})}
-      in
-      case unhandled0 of {
-       [] -> (\_ _ _ _ holds0 _ _ -> _evar_0_ holds0);
-       (:) x x0 -> _evar_0_0 x x0 __}}
-    in
-    case desc of {
-     Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
-      _evar_0_ x x0 x1 x2 x3 x4 x5 __ __ __ __ holds __}}
-  in
-  case ssi of {
-   Build_SSInfo x x0 -> _evar_0_ x x0 __}
-
-create_ssinfo :: Prelude.Int -> ([] Interval.IntervalDesc) ->
-                            Coq_fixedIntervalsType -> ([]
-                            ((,) Prelude.Int Prelude.Int)) -> ([]
-                            ((,) Prelude.Int PhysReg)) -> ([]
-                            ((,) Prelude.Int PhysReg)) -> ([]
-                            ((,) Prelude.Int PhysReg)) ->
-                            ScanStateDesc -> Prelude.Int ->
-                            Prelude.Int -> Interval.IntervalDesc ->
-                            Interval.IntervalDesc -> ([]
-                            ((,) Prelude.Int PhysReg)) -> ([]
-                            ((,) Prelude.Int PhysReg)) ->
-                            SSInfo ()
-create_ssinfo ni intervals0 fixedIntervals0 unh active0 inactive0 handled0 pre aid pos' id0 id1 active1 inactive1 =
-  let {
-   new_inactive_added = Build_ScanStateDesc ((Prelude.succ) ni)
-    (LinearScan.Utils.snoc ni
-      (LinearScan.Utils.set_nth ni intervals0 aid id0) id1) fixedIntervals0
-    (Prelude.map (\i -> Prelude.id i) unh) active1 inactive1
-    (Prelude.map (\i -> Prelude.id i) handled0)}
-  in
-  Build_SSInfo new_inactive_added __
-
-splitAssignedIntervalForReg :: ScanStateDesc ->
-                                          PhysReg -> (Prelude.Maybe
-                                          Prelude.Int) -> Prelude.Bool ->
-                                          SState a1 () ()
-splitAssignedIntervalForReg pre reg pos trueForActives ssi =
-  let {
-   _evar_0_ = \desc holds ->
-    let {
-     intlist = case trueForActives of {
-                Prelude.True -> active desc;
-                Prelude.False -> inactive desc}}
-    in
-    (Prelude.flip (Prelude.$)) __ (\_ ->
-      let {
-       intids = Prelude.map (\i -> Prelude.fst i)
-                  (Prelude.filter (\i ->
-                    Eqtype.eq_op (Fintype.ordinal_eqType maxReg)
-                      (Prelude.snd (unsafeCoerce i)) (unsafeCoerce reg))
-                    intlist)}
-      in
-      (Prelude.flip (Prelude.$)) __ (\_ ->
-        let {
-         _evar_0_ = \_ ->
-          let {
-           _evar_0_ = \ni intervals0 _fixedIntervals_ unh active0 _inactive_ _handled_ holds0 intlist0 intids0 ->
-            let {_evar_0_ = \_ -> Prelude.Left ENoIntervalsToSplit}
-            in
-            let {
-             _evar_0_0 = \aid aids iHaids ->
-              let {int = LinearScan.Utils.nth ni intervals0 aid} in
-              let {_evar_0_0 = \_ -> iHaids __} in
-              let {
-               _evar_0_1 = \_ ->
-                (Prelude.flip (Prelude.$)) __ (\_ ->
-                  let {
-                   _top_assumption_ = Interval.splitPosition ( int) pos
-                                        Prelude.False}
-                  in
-                  let {_evar_0_1 = iHaids __} in
-                  let {
-                   _evar_0_2 = Prelude.Right ((,) ()
-                    (let {
-                      _top_assumption_0 = Interval.splitInterval
-                                            _top_assumption_ ( int)}
-                     in
-                     let {
-                      _evar_0_2 = \_top_assumption_1 _top_assumption_2 ->
-                       let {
-                        _evar_0_2 = \_ ->
-                         (Prelude.flip (Prelude.$)) __ (\_ ->
-                           let {
-                            _evar_0_2 = \_ _ ->
-                             (Prelude.flip (Prelude.$)) __
-                               (let {
-                                 _evar_0_2 = \_ ->
-                                  (Prelude.flip (Prelude.$)) __ (\_ ->
-                                    create_ssinfo ni intervals0
-                                      _fixedIntervals_ unh active0 _inactive_
-                                      _handled_ pre aid _top_assumption_
-                                      _top_assumption_1 _top_assumption_2
-                                      (Prelude.map (unsafeCoerce Prelude.id)
-                                        (Seq.rem
-                                          (Eqtype.prod_eqType
-                                            (Fintype.ordinal_eqType ni)
-                                            (Fintype.ordinal_eqType
-                                              maxReg))
-                                          (unsafeCoerce ((,) aid reg))
-                                          intlist0)) ((:) ((,) ( ni) reg)
-                                      ((:) (Prelude.id ((,) aid reg))
-                                      (Prelude.map Prelude.id _inactive_))))}
-                                in
-                                 _evar_0_2)}
-                           in
-                           let {
-                            _evar_0_3 = \_ _ ->
-                             (Prelude.flip (Prelude.$)) __ (\_ ->
-                               create_ssinfo ni intervals0
-                                 _fixedIntervals_ unh active0 _inactive_
-                                 _handled_ pre aid _top_assumption_
-                                 _top_assumption_1 _top_assumption_2
-                                 (Prelude.map Prelude.id active0) ((:) ((,)
-                                 ( ni) reg)
-                                 (Prelude.map Prelude.id _inactive_)))}
-                           in
-                           case trueForActives of {
-                            Prelude.True -> _evar_0_2 __ __;
-                            Prelude.False -> _evar_0_3 __ __})}
-                       in
-                        _evar_0_2 __}
-                     in
-                     case _top_assumption_0 of {
-                      (,) x x0 -> _evar_0_2 x x0}))}
-                  in
-                  case Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)
-                         (unsafeCoerce pos)
-                         (unsafeCoerce (Prelude.Just
-                           (Prelude.pred _top_assumption_))) of {
-                   Prelude.True -> _evar_0_1;
-                   Prelude.False -> _evar_0_2})}
-              in
-              case Interval.coq_Interval_is_singleton ( int) of {
-               Prelude.True -> _evar_0_0 __;
-               Prelude.False -> _evar_0_1 __}}
-            in
-            Datatypes.list_rect _evar_0_ (\aid aids iHaids _ ->
-              _evar_0_0 aid aids iHaids) intids0 __}
-          in
-          (\intlist0 _ intids0 _ ->
-          case desc of {
-           Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
-            _evar_0_ x x0 x1 x2 x3 x4 x5 holds intlist0 intids0})}
-        in
-        unsafeCoerce _evar_0_ __ intlist __ intids __))}
-  in
-  case ssi of {
-   Build_SSInfo x x0 -> _evar_0_ x x0}
-
-splitActiveIntervalForReg :: ScanStateDesc ->
-                                        PhysReg -> Prelude.Int ->
-                                        SState a1 () ()
-splitActiveIntervalForReg pre reg pos =
-  splitAssignedIntervalForReg pre reg (Prelude.Just pos)
-    Prelude.True
-
-splitAnyInactiveIntervalForReg :: ScanStateDesc ->
-                                             PhysReg ->
-                                             SState a1 () ()
-splitAnyInactiveIntervalForReg pre reg ss =
-  (Prelude.flip (Prelude.$)) (\s _ _ ->
-    splitAssignedIntervalForReg s reg Prelude.Nothing
-      Prelude.False) (\_top_assumption_ ->
-    let {_top_assumption_0 = _top_assumption_ pre __ __} in
-    let {_top_assumption_1 = _top_assumption_0 ss} in
-    let {
-     _evar_0_ = \err -> Prelude.Right ((,) () (Build_SSInfo
-      (thisDesc pre ss) __))}
-    in
-    let {
-     _evar_0_0 = \_top_assumption_2 ->
-      let {_evar_0_0 = \_the_1st_wildcard_ ss' -> Prelude.Right ((,) () ss')}
-      in
-      case _top_assumption_2 of {
-       (,) x x0 -> _evar_0_0 x x0}}
-    in
-    case _top_assumption_1 of {
-     Prelude.Left x -> _evar_0_ x;
-     Prelude.Right x -> _evar_0_0 x})
-
-intersectsWithFixedInterval :: ScanStateDesc ->
-                                          PhysReg ->
-                                          SState a1 a1
-                                          (Prelude.Maybe Prelude.Int)
-intersectsWithFixedInterval pre reg =
-  (Prelude.$) (withCursor pre) (\sd _ ->
-    let {int = curIntDetails sd} in
-    (Prelude.$) return_
-      (LinearScan.Utils.vfoldl' maxReg (\mx v ->
-        Lib.option_choose mx
-          (case v of {
-            Prelude.Just i -> Interval.intervalIntersectionPoint ( int) ( i);
-            Prelude.Nothing -> Prelude.Nothing})) Prelude.Nothing
-        (fixedIntervals sd)))
-
-tryAllocateFreeReg :: ScanStateDesc -> SState
-                                 a1 a1
-                                 (Prelude.Maybe
-                                 (SState a1 () PhysReg))
-tryAllocateFreeReg pre =
-  (Prelude.$) (withCursor pre) (\sd _ ->
-    let {
-     go = \n ->
-      Data.List.foldl' (\v p ->
-        case p of {
-         (,) i r -> LinearScan.Utils.set_nth maxReg v r (n i)})}
-    in
-    let {
-     freeUntilPos' = go (\x -> Prelude.Just 0)
-                       (Data.List.replicate maxReg
-                         Prelude.Nothing) (active sd)}
-    in
-    let {
-     intersectingIntervals = Prelude.filter (\x ->
-                               Interval.intervalsIntersect
-                                 ( (curIntDetails sd))
-                                 (
-                                   (LinearScan.Utils.nth
-                                     (nextInterval sd)
-                                     (intervals sd)
-                                     (Prelude.fst x))))
-                               (inactive sd)}
-    in
-    let {
-     freeUntilPos = go (\i ->
-                      Interval.intervalIntersectionPoint
-                        (
-                          (LinearScan.Utils.nth (nextInterval sd)
-                            (intervals sd) i))
-                        ( (curIntDetails sd))) freeUntilPos'
-                      intersectingIntervals}
-    in
-    case registerWithHighestPos freeUntilPos of {
-     (,) reg mres ->
-      let {
-       success = stbind (\x -> return_ reg)
-                   (moveUnhandledToActive pre reg)}
-      in
-      let {
-       maction = case mres of {
-                  Prelude.Just n ->
-                   case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce n)
-                          (unsafeCoerce 0) of {
-                    Prelude.True -> Prelude.Nothing;
-                    Prelude.False -> Prelude.Just
-                     (case (Prelude.<=) ((Prelude.succ)
-                             (Interval.intervalEnd
-                               ( (curIntDetails sd)))) n of {
-                       Prelude.True -> success;
-                       Prelude.False ->
-                        stbind (\x ->
-                          stbind (\x0 -> return_ reg)
-                            (moveUnhandledToActive pre reg))
-                          (splitCurrentInterval pre (Prelude.Just
-                            n))})};
-                  Prelude.Nothing -> Prelude.Just success}}
-      in
-      return_ maction})
-
-allocateBlockedReg :: ScanStateDesc -> SState
-                                 a1 () (Prelude.Maybe PhysReg)
-allocateBlockedReg pre =
-  (Prelude.$) (withCursor pre) (\sd _ ->
-    let {start = Interval.intervalStart ( (curIntDetails sd))} in
-    let {pos = curPosition sd} in
-    let {
-     go = \v p ->
-      case p of {
-       (,) i r ->
-        let {
-         atPos = \u ->
-          Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos)
-            (unsafeCoerce (Range.uloc u))}
-        in
-        let {
-         pos' = case Interval.findIntervalUsePos
-                       (
-                         (LinearScan.Utils.nth (nextInterval sd)
-                           (intervals sd) i)) atPos of {
-                 Prelude.Just p0 -> Prelude.Just 0;
-                 Prelude.Nothing ->
-                  Interval.nextUseAfter
-                    (
-                      (LinearScan.Utils.nth (nextInterval sd)
-                        (intervals sd) i)) start}}
-        in
-        LinearScan.Utils.set_nth maxReg v r pos'}}
-    in
-    let {
-     nextUsePos' = Data.List.foldl' go
-                     (Data.List.replicate maxReg Prelude.Nothing)
-                     (active sd)}
-    in
-    let {
-     intersectingIntervals = Prelude.filter (\x ->
-                               Interval.intervalsIntersect
-                                 ( (curIntDetails sd))
-                                 (
-                                   (LinearScan.Utils.nth
-                                     (nextInterval sd)
-                                     (intervals sd)
-                                     (Prelude.fst x))))
-                               (inactive sd)}
-    in
-    let {nextUsePos = Data.List.foldl' go nextUsePos' intersectingIntervals}
-    in
-    case registerWithHighestPos nextUsePos of {
-     (,) reg mres ->
-      case case mres of {
-            Prelude.Just n -> (Prelude.<=) ((Prelude.succ) n) start;
-            Prelude.Nothing -> Prelude.False} of {
-       Prelude.True ->
-        stbind (\x ->
-          stbind (\mloc ->
-            stbind (\x0 ->
-              stbind (\x1 -> return_ Prelude.Nothing)
-                (weakenStHasLenToSt pre))
-              (case mloc of {
-                Prelude.Just n ->
-                 splitCurrentInterval pre (Prelude.Just n);
-                Prelude.Nothing -> return_ ()}))
-            (intersectsWithFixedInterval pre reg))
-          (splitCurrentInterval pre
-            (Interval.firstUseReqReg ( (curIntDetails sd))));
-       Prelude.False ->
-        stbind (\x ->
-          stbind (\x0 ->
-            stbind (\mloc ->
-              stbind (\x1 ->
-                return_ (Prelude.Just reg))
-                (case mloc of {
-                  Prelude.Just n ->
-                   stbind (\x1 ->
-                     moveUnhandledToActive pre reg)
-                     (splitCurrentInterval pre (Prelude.Just n));
-                  Prelude.Nothing -> moveUnhandledToActive pre reg}))
-              (intersectsWithFixedInterval pre reg))
-            (splitActiveIntervalForReg pre reg pos))
-          (splitAnyInactiveIntervalForReg pre reg)}})
-
-morphlen_transport :: ScanStateDesc ->
-                                 ScanStateDesc ->
-                                 IntervalId -> IntervalId
-morphlen_transport b b' = GHC.Base.id
-  
-
-mt_fst :: ScanStateDesc -> ScanStateDesc ->
-                     ((,) IntervalId PhysReg) -> (,)
-                     IntervalId PhysReg
-mt_fst b b' x =
-  case x of {
-   (,) xid reg -> (,) (morphlen_transport b b' xid) reg}
-
-type Coq_int_reg_seq =
-  [] ((,) IntervalId PhysReg)
-
-type Coq_intermediate_result =
-  Specif.Coq_sig2 ScanStateDesc
-
-goActive :: Prelude.Int -> ScanStateDesc ->
-                       ScanStateDesc -> ((,) IntervalId
-                       PhysReg) -> Coq_int_reg_seq ->
-                       Coq_intermediate_result
-goActive pos sd z x xs =
-  case (Prelude.<=) ((Prelude.succ)
-         (Interval.intervalEnd
-           (
-             (LinearScan.Utils.nth (nextInterval z)
-               (intervals z) (Prelude.fst x))))) pos of {
-   Prelude.True -> moveActiveToHandled z (unsafeCoerce x);
-   Prelude.False ->
-    case Prelude.not
-           (Interval.intervalCoversPos
-             (
-               (LinearScan.Utils.nth (nextInterval z)
-                 (intervals z) (Prelude.fst x))) pos) of {
-     Prelude.True -> moveActiveToInactive z (unsafeCoerce x);
-     Prelude.False -> z}}
-
-checkActiveIntervals :: ScanStateDesc -> Prelude.Int ->
-                                   SState () () ()
-checkActiveIntervals pre pos =
-  (Prelude.$) (withScanStatePO pre) (\sd _ ->
-    let {
-     res = Lib.dep_foldl_inv (\s ->
-             Eqtype.prod_eqType
-               (Fintype.ordinal_eqType (nextInterval s))
-               (Fintype.ordinal_eqType maxReg)) sd
-             (unsafeCoerce (active sd))
-             (Data.List.length (active sd))
-             (unsafeCoerce active)
-             (unsafeCoerce (\x x0 _ -> mt_fst x x0))
-             (unsafeCoerce (\x _ x0 x1 _ ->
-               goActive pos sd x x0 x1))}
-    in
-    IState.iput (Build_SSInfo res __))
-
-moveInactiveToActive' :: ScanStateDesc -> ((,)
-                                    IntervalId PhysReg)
-                                    -> Coq_int_reg_seq ->
-                                    Prelude.Either SSError
-                                    (Specif.Coq_sig2 ScanStateDesc)
-moveInactiveToActive' z x xs =
-  let {
-   filtered_var = Prelude.not
-                    (Ssrbool.in_mem (Prelude.snd (unsafeCoerce x))
-                      (Ssrbool.mem
-                        (Seq.seq_predType
-                          (Fintype.ordinal_eqType maxReg))
-                        (unsafeCoerce
-                          (Prelude.map (\i -> Prelude.snd i)
-                            (active z)))))}
-  in
-  case filtered_var of {
-   Prelude.True ->
-    let {filtered_var0 = moveInactiveToActive z (unsafeCoerce x)}
-    in
-    Prelude.Right filtered_var0;
-   Prelude.False -> Prelude.Left (ERegisterAssignmentsOverlap
-    ( (Prelude.snd x)))}
-
-goInactive :: Prelude.Int -> ScanStateDesc ->
-                         ScanStateDesc -> ((,) IntervalId
-                         PhysReg) -> Coq_int_reg_seq ->
-                         Prelude.Either SSError
-                         Coq_intermediate_result
-goInactive pos sd z x xs =
-  let {f = \sd' -> Prelude.Right sd'} in
-  case (Prelude.<=) ((Prelude.succ)
-         (Interval.intervalEnd
-           (
-             (LinearScan.Utils.nth (nextInterval z)
-               (intervals z) (Prelude.fst x))))) pos of {
-   Prelude.True ->
-    let {filtered_var = moveInactiveToHandled z (unsafeCoerce x)}
-    in
-    f filtered_var;
-   Prelude.False ->
-    case Interval.intervalCoversPos
-           (
-             (LinearScan.Utils.nth (nextInterval z)
-               (intervals z) (Prelude.fst x))) pos of {
-     Prelude.True ->
-      let {filtered_var = moveInactiveToActive' z x xs} in
-      case filtered_var of {
-       Prelude.Left err -> Prelude.Left err;
-       Prelude.Right s -> f s};
-     Prelude.False -> f z}}
-
-checkInactiveIntervals :: ScanStateDesc -> Prelude.Int
-                                     -> SState () () ()
-checkInactiveIntervals pre pos =
-  (Prelude.$) (withScanStatePO pre) (\sd _ ->
-    let {
-     eres = Lib.dep_foldl_invE (\s ->
-              Eqtype.prod_eqType
-                (Fintype.ordinal_eqType (nextInterval s))
-                (Fintype.ordinal_eqType maxReg)) sd
-              (unsafeCoerce (inactive sd))
-              (Data.List.length (inactive sd))
-              (unsafeCoerce inactive)
-              (unsafeCoerce (\x x0 _ -> mt_fst x x0))
-              (unsafeCoerce (\x _ x0 x1 _ ->
-                goInactive pos sd x x0 x1))}
-    in
-    case eres of {
-     Prelude.Left err -> IState.ierr err;
-     Prelude.Right s -> IState.iput (Build_SSInfo s __)})
-
-handleInterval :: ScanStateDesc -> SState 
-                             () () (Prelude.Maybe PhysReg)
-handleInterval pre =
-  (Prelude.$) (unsafeCoerce (withCursor pre)) (\sd _ ->
-    let {position = curPosition sd} in
-    stbind (\x ->
-      stbind (\x0 ->
-        stbind (\mres ->
-          case mres of {
-           Prelude.Just x1 ->
-            IEndo.imap (unsafeCoerce IState.coq_IState_IFunctor) (\x2 ->
-              Prelude.Just x2) x1;
-           Prelude.Nothing ->
-            unsafeCoerce (allocateBlockedReg pre)})
-          (tryAllocateFreeReg pre))
-        (liftLen pre (\sd0 ->
-          checkInactiveIntervals sd0 position)))
-      (liftLen pre (\sd0 ->
-        checkActiveIntervals sd0 position)))
-
-walkIntervals_func :: ((,) ScanStateDesc ()) ->
-                                 Prelude.Either SSError
-                                 ScanStateDesc
-walkIntervals_func x =
-  let {sd = Prelude.fst x} in
-  let {
-   walkIntervals0 = \sd0 ->
-    let {y = (,) sd0 __} in walkIntervals_func ( y)}
-  in
-  let {filtered_var = LinearScan.Utils.uncons (unhandled sd)} in
-  case filtered_var of {
-   Prelude.Just s ->
-    let {ssinfo = Build_SSInfo sd __} in
-    let {
-     filtered_var0 = IState.runIState (handleInterval sd) ssinfo}
-    in
-    case filtered_var0 of {
-     Prelude.Left err -> Prelude.Left err;
-     Prelude.Right p ->
-      case p of {
-       (,) wildcard' ssinfo' ->
-        walkIntervals0 (thisDesc sd ssinfo')}};
-   Prelude.Nothing -> Prelude.Right (packScanState sd)}
-
-walkIntervals :: ScanStateDesc -> Prelude.Either
-                            SSError ScanStateDesc
-walkIntervals sd =
-  walkIntervals_func ((,) sd __)
-
-mainAlgorithm :: IState.IState SSError BlockList
-                 BlockList ()
-mainAlgorithm =
-  stbind (\x ->
-    stbind (\x0 ->
-      stbind (\x1 ->
-        stbind (\x2 ->
-          stbind (\ssig ->
-            case walkIntervals ( ssig) of {
-             Prelude.Left err -> error_ err;
-             Prelude.Right ssig' ->
-              stbind (\x3 -> assignRegNum ( ssig'))
-                resolveDataFlow}) buildIntervals)
-          computeGlobalLiveSets) computeLocalLiveSets)
-      numberOperations) computeBlockOrder
-
-linearScan :: BlockList -> Prelude.Either SSError
-              BlockList
-linearScan blocks =
-  case IState.runIState mainAlgorithm blocks of {
-   Prelude.Left err -> Prelude.Left err;
-   Prelude.Right p ->
-    case p of {
-     (,) u res -> Prelude.Right res}}
+import qualified Data.IntMap
+import qualified Data.List
+import qualified Data.Ord
+import qualified Data.Functor.Identity
+import qualified LinearScan.Utils
+
+import qualified LinearScan.Datatypes as Datatypes
+import qualified LinearScan.IState as IState
+import qualified LinearScan.Interval as Interval
+import qualified LinearScan.Lib as Lib
+import qualified LinearScan.Logic as Logic
+import qualified LinearScan.Range as Range
+import qualified LinearScan.Specif as Specif
+import qualified LinearScan.State as State
+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
+
+
+
+--unsafeCoerce :: a -> b
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base as GHC.Base
+unsafeCoerce = GHC.Base.unsafeCoerce#
+#else
+-- HUGS
+import qualified LinearScan.IOExts as IOExts
+unsafeCoerce = IOExts.unsafeCoerce
+#endif
+
+__ :: any
+__ = Prelude.error "Logical or arity value used"
+
+_MyMachine__maxReg :: Prelude.Int
+_MyMachine__maxReg = 32
+
+_MyMachine__regSize :: Prelude.Int
+_MyMachine__regSize = 8
+
+type MyMachine__PhysReg = Prelude.Int
+
+maxReg :: Prelude.Int
+maxReg =
+  _MyMachine__maxReg
+
+regSize :: Prelude.Int
+regSize =
+  _MyMachine__regSize
+
+type PhysReg = Prelude.Int
+
+data SSError =
+   ECannotSplitSingleton Prelude.Int
+ | ECannotSplitAssignedSingleton Prelude.Int
+ | ENoIntervalsToSplit
+ | ERegisterAlreadyAssigned Prelude.Int
+ | ERegisterAssignmentsOverlap Prelude.Int
+ | EFuelExhausted
+ | EUnexpectedNoMoreUnhandled
+
+coq_SSError_rect :: (Prelude.Int -> a1) -> (Prelude.Int -> a1) ->
+                               a1 -> (Prelude.Int -> a1) -> (Prelude.Int ->
+                               a1) -> a1 -> a1 -> SSError -> a1
+coq_SSError_rect f f0 f1 f2 f3 f4 f5 s =
+  case s of {
+   ECannotSplitSingleton x -> f x;
+   ECannotSplitAssignedSingleton x -> f0 x;
+   ENoIntervalsToSplit -> f1;
+   ERegisterAlreadyAssigned x -> f2 x;
+   ERegisterAssignmentsOverlap x -> f3 x;
+   EFuelExhausted -> f4;
+   EUnexpectedNoMoreUnhandled -> f5}
+
+coq_SSError_rec :: (Prelude.Int -> a1) -> (Prelude.Int -> a1) ->
+                              a1 -> (Prelude.Int -> a1) -> (Prelude.Int ->
+                              a1) -> a1 -> a1 -> SSError -> a1
+coq_SSError_rec =
+  coq_SSError_rect
+
+stbind :: (a4 -> IState.IState SSError a2 a3 a5) ->
+                     (IState.IState SSError a1 a2 a4) ->
+                     IState.IState SSError a1 a3 a5
+stbind f x =
+  IState.ijoin (IState.imap f x)
+
+error_ :: SSError -> IState.IState SSError 
+                     a1 a2 a3
+error_ err x =
+  Prelude.Left err
+
+return_ :: a3 -> IState.IState a1 a2 a2 a3
+return_ =
+  IState.ipure
+
+type Coq_fixedIntervalsType =
+  [] (Prelude.Maybe Interval.IntervalDesc)
+
+data ScanStateDesc =
+   Build_ScanStateDesc Prelude.Int ([] Interval.IntervalDesc) 
+ Coq_fixedIntervalsType ([] ((,) Prelude.Int Prelude.Int)) 
+ ([] ((,) Prelude.Int PhysReg)) ([]
+                                          ((,) Prelude.Int PhysReg)) 
+ ([] ((,) Prelude.Int PhysReg))
+
+coq_ScanStateDesc_rect :: (Prelude.Int -> ([]
+                                     Interval.IntervalDesc) ->
+                                     Coq_fixedIntervalsType -> ([]
+                                     ((,) Prelude.Int Prelude.Int)) -> ([]
+                                     ((,) Prelude.Int PhysReg)) ->
+                                     ([] ((,) Prelude.Int PhysReg))
+                                     -> ([]
+                                     ((,) Prelude.Int PhysReg)) ->
+                                     a1) -> ScanStateDesc -> a1
+coq_ScanStateDesc_rect f s =
+  case s of {
+   Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 -> f x x0 x1 x2 x3 x4 x5}
+
+coq_ScanStateDesc_rec :: (Prelude.Int -> ([]
+                                    Interval.IntervalDesc) ->
+                                    Coq_fixedIntervalsType -> ([]
+                                    ((,) Prelude.Int Prelude.Int)) -> ([]
+                                    ((,) Prelude.Int PhysReg)) ->
+                                    ([] ((,) Prelude.Int PhysReg))
+                                    -> ([]
+                                    ((,) Prelude.Int PhysReg)) ->
+                                    a1) -> ScanStateDesc -> a1
+coq_ScanStateDesc_rec =
+  coq_ScanStateDesc_rect
+
+nextInterval :: ScanStateDesc -> Prelude.Int
+nextInterval s =
+  case s of {
+   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
+    unhandled0 active0 inactive0 handled0 -> nextInterval0}
+
+type IntervalId = Prelude.Int
+
+intervals :: ScanStateDesc -> [] Interval.IntervalDesc
+intervals s =
+  case s of {
+   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
+    unhandled0 active0 inactive0 handled0 -> intervals0}
+
+fixedIntervals :: ScanStateDesc ->
+                             Coq_fixedIntervalsType
+fixedIntervals s =
+  case s of {
+   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
+    unhandled0 active0 inactive0 handled0 -> fixedIntervals0}
+
+unhandled :: ScanStateDesc -> []
+                        ((,) IntervalId Prelude.Int)
+unhandled s =
+  case s of {
+   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
+    unhandled0 active0 inactive0 handled0 -> unhandled0}
+
+active :: ScanStateDesc -> []
+                     ((,) IntervalId PhysReg)
+active s =
+  case s of {
+   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
+    unhandled0 active0 inactive0 handled0 -> active0}
+
+inactive :: ScanStateDesc -> []
+                       ((,) IntervalId PhysReg)
+inactive s =
+  case s of {
+   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
+    unhandled0 active0 inactive0 handled0 -> inactive0}
+
+handled :: ScanStateDesc -> []
+                      ((,) IntervalId PhysReg)
+handled s =
+  case s of {
+   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
+    unhandled0 active0 inactive0 handled0 -> handled0}
+
+unhandledIds :: ScanStateDesc -> [] IntervalId
+unhandledIds s =
+  Prelude.map (\i -> Prelude.fst i) (unhandled s)
+
+activeIds :: ScanStateDesc -> [] IntervalId
+activeIds s =
+  Prelude.map (\i -> Prelude.fst i) (active s)
+
+inactiveIds :: ScanStateDesc -> [] IntervalId
+inactiveIds s =
+  Prelude.map (\i -> Prelude.fst i) (inactive s)
+
+handledIds :: ScanStateDesc -> [] IntervalId
+handledIds s =
+  Prelude.map (\i -> Prelude.fst i) (handled s)
+
+all_state_lists :: ScanStateDesc -> []
+                              IntervalId
+all_state_lists s =
+  (Prelude.++) (unhandledIds s)
+    ((Prelude.++) (activeIds s)
+      ((Prelude.++) (inactiveIds s) (handledIds s)))
+
+registerWithHighestPos :: ([] (Prelude.Maybe Prelude.Int)) -> (,)
+                                     Prelude.Int (Prelude.Maybe Prelude.Int)
+registerWithHighestPos =
+  (LinearScan.Utils.vfoldl'_with_index) maxReg (\reg res x ->
+    case res of {
+     (,) r o ->
+      case o of {
+       Prelude.Just n ->
+        case x of {
+         Prelude.Just m ->
+          case (Prelude.<=) ((Prelude.succ) n) m of {
+           Prelude.True -> (,) reg (Prelude.Just m);
+           Prelude.False -> (,) r (Prelude.Just n)};
+         Prelude.Nothing -> (,) reg Prelude.Nothing};
+       Prelude.Nothing -> (,) r Prelude.Nothing}}) ((,) ( 0) (Prelude.Just
+    0))
+
+isWithin :: Interval.IntervalDesc -> Prelude.Int -> Prelude.Int ->
+                       Prelude.Bool
+isWithin int vid opid =
+  (Prelude.&&)
+    (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Interval.ivar int))
+      (unsafeCoerce vid))
+    ((Prelude.&&) ((Prelude.<=) (Interval.ibeg int) opid)
+      ((Prelude.<=) ((Prelude.succ) opid) (Interval.iend int)))
+
+lookupInterval :: ScanStateDesc -> a1 -> Prelude.Int ->
+                             Prelude.Int -> Prelude.Maybe
+                             IntervalId
+lookupInterval sd st vid opid =
+  let {
+   f = \idx acc int ->
+    case acc of {
+     Prelude.Just x -> Prelude.Just x;
+     Prelude.Nothing ->
+      case isWithin ( int) vid opid of {
+       Prelude.True -> Prelude.Just idx;
+       Prelude.False -> Prelude.Nothing}}}
+  in
+  (LinearScan.Utils.vfoldl'_with_index) (nextInterval sd) f
+    Prelude.Nothing (intervals sd)
+
+lookupRegister :: ScanStateDesc -> a1 ->
+                             Eqtype.Equality__Coq_sort -> Prelude.Maybe
+                             PhysReg
+lookupRegister sd st intid =
+  Lib.forFold Prelude.Nothing
+    ((Prelude.++) (unsafeCoerce (handled sd))
+      ((Prelude.++) (unsafeCoerce (active sd))
+        (unsafeCoerce (inactive sd)))) (\acc x ->
+    case x of {
+     (,) xid reg ->
+      case acc of {
+       Prelude.Just r -> Prelude.Just r;
+       Prelude.Nothing ->
+        case Eqtype.eq_op
+               (Fintype.ordinal_eqType (nextInterval sd)) xid
+               intid of {
+         Prelude.True -> Prelude.Just reg;
+         Prelude.False -> Prelude.Nothing}}})
+
+data ScanStateStatus =
+   Pending
+ | InUse
+
+coq_ScanStateStatus_rect :: a1 -> a1 -> ScanStateStatus
+                                       -> a1
+coq_ScanStateStatus_rect f f0 s =
+  case s of {
+   Pending -> f;
+   InUse -> f0}
+
+coq_ScanStateStatus_rec :: a1 -> a1 -> ScanStateStatus
+                                      -> a1
+coq_ScanStateStatus_rec =
+  coq_ScanStateStatus_rect
+
+type ScanStateSig = ScanStateDesc
+
+getScanStateDesc :: ScanStateDesc ->
+                               ScanStateDesc
+getScanStateDesc sd =
+  sd
+
+packScanState :: ScanStateStatus ->
+                            ScanStateDesc ->
+                            ScanStateDesc
+packScanState b sd =
+  sd
+
+coq_ScanStateCursor_rect :: ScanStateDesc -> (() -> ()
+                                       -> a1) -> a1
+coq_ScanStateCursor_rect sd f =
+  f __ __
+
+coq_ScanStateCursor_rec :: ScanStateDesc -> (() -> () ->
+                                      a1) -> a1
+coq_ScanStateCursor_rec sd f =
+  coq_ScanStateCursor_rect sd f
+
+curId :: ScanStateDesc -> (,) IntervalId
+                    Prelude.Int
+curId sd =
+  Prelude.head (unhandled sd)
+
+curIntDetails :: ScanStateDesc -> Interval.IntervalDesc
+curIntDetails sd =
+  LinearScan.Utils.nth (nextInterval sd) (intervals sd)
+    (Prelude.fst (curId sd))
+
+curPosition :: ScanStateDesc -> Prelude.Int
+curPosition sd =
+  Interval.intervalStart ( (curIntDetails sd))
+
+data VarKind =
+   Input
+ | Temp
+ | Output
+
+coq_VarKind_rect :: a1 -> a1 -> a1 -> VarKind -> a1
+coq_VarKind_rect f f0 f1 v =
+  case v of {
+   Input -> f;
+   Temp -> f0;
+   Output -> f1}
+
+coq_VarKind_rec :: a1 -> a1 -> a1 -> VarKind -> a1
+coq_VarKind_rec =
+  coq_VarKind_rect
+
+type VarId = Prelude.Int
+
+data VarInfo varType =
+   Build_VarInfo (varType -> VarId) (varType ->
+                                                        VarKind) 
+ (varType -> Prelude.Bool)
+
+coq_VarInfo_rect :: ((a1 -> VarId) -> (a1 ->
+                               VarKind) -> (a1 -> Prelude.Bool) ->
+                               a2) -> (VarInfo a1) -> a2
+coq_VarInfo_rect f v =
+  case v of {
+   Build_VarInfo x x0 x1 -> f x x0 x1}
+
+coq_VarInfo_rec :: ((a1 -> VarId) -> (a1 ->
+                              VarKind) -> (a1 -> Prelude.Bool) ->
+                              a2) -> (VarInfo a1) -> a2
+coq_VarInfo_rec =
+  coq_VarInfo_rect
+
+varId :: (VarInfo a1) -> a1 -> VarId
+varId v =
+  case v of {
+   Build_VarInfo varId0 varKind0 regRequired0 -> varId0}
+
+varKind :: (VarInfo a1) -> a1 -> VarKind
+varKind v =
+  case v of {
+   Build_VarInfo varId0 varKind0 regRequired0 -> varKind0}
+
+regRequired :: (VarInfo a1) -> a1 -> Prelude.Bool
+regRequired v =
+  case v of {
+   Build_VarInfo varId0 varKind0 regRequired0 -> regRequired0}
+
+data OpKind =
+   IsNormal
+ | IsCall
+ | IsBranch
+ | IsLoopBegin
+ | IsLoopEnd
+
+coq_OpKind_rect :: a1 -> a1 -> a1 -> a1 -> a1 -> OpKind
+                              -> a1
+coq_OpKind_rect f f0 f1 f2 f3 o =
+  case o of {
+   IsNormal -> f;
+   IsCall -> f0;
+   IsBranch -> f1;
+   IsLoopBegin -> f2;
+   IsLoopEnd -> f3}
+
+coq_OpKind_rec :: a1 -> a1 -> a1 -> a1 -> a1 -> OpKind
+                             -> a1
+coq_OpKind_rec =
+  coq_OpKind_rect
+
+data OpInfo accType opType1 opType2 varType =
+   Build_OpInfo (opType1 -> OpKind) (opType1 -> (,)
+                                                        ([] varType)
+                                                        ([]
+                                                        PhysReg)) 
+ (VarId -> PhysReg -> accType -> (,) opType2 accType) 
+ (VarId -> PhysReg -> accType -> (,) opType2 accType) 
+ (opType1 -> ([] ((,) VarId PhysReg)) -> opType2)
+
+coq_OpInfo_rect :: ((a2 -> OpKind) -> (a2 -> (,) 
+                              ([] a4) ([] PhysReg)) ->
+                              (VarId -> PhysReg -> a1 ->
+                              (,) a3 a1) -> (VarId ->
+                              PhysReg -> a1 -> (,) a3 a1) -> (a2 ->
+                              ([] ((,) VarId PhysReg)) ->
+                              a3) -> a5) -> (OpInfo a1 a2 a3 
+                              a4) -> a5
+coq_OpInfo_rect f o =
+  case o of {
+   Build_OpInfo x x0 x1 x2 x3 -> f x x0 x1 x2 x3}
+
+coq_OpInfo_rec :: ((a2 -> OpKind) -> (a2 -> (,) 
+                             ([] a4) ([] PhysReg)) ->
+                             (VarId -> PhysReg -> a1 ->
+                             (,) a3 a1) -> (VarId ->
+                             PhysReg -> a1 -> (,) a3 a1) -> (a2 ->
+                             ([] ((,) VarId PhysReg)) ->
+                             a3) -> a5) -> (OpInfo a1 a2 a3 
+                             a4) -> a5
+coq_OpInfo_rec =
+  coq_OpInfo_rect
+
+opKind :: (OpInfo a1 a2 a3 a4) -> a2 -> OpKind
+opKind o =
+  case o of {
+   Build_OpInfo opKind0 opRefs0 saveOp0 restoreOp0 applyAllocs0 ->
+    opKind0}
+
+opRefs :: (OpInfo a1 a2 a3 a4) -> a2 -> (,) ([] a4)
+                     ([] PhysReg)
+opRefs o =
+  case o of {
+   Build_OpInfo opKind0 opRefs0 saveOp0 restoreOp0 applyAllocs0 ->
+    opRefs0}
+
+saveOp :: (OpInfo a1 a2 a3 a4) -> VarId ->
+                     PhysReg -> a1 -> (,) a3 a1
+saveOp o =
+  case o of {
+   Build_OpInfo opKind0 opRefs0 saveOp0 restoreOp0 applyAllocs0 ->
+    saveOp0}
+
+restoreOp :: (OpInfo a1 a2 a3 a4) -> VarId ->
+                        PhysReg -> a1 -> (,) a3 a1
+restoreOp o =
+  case o of {
+   Build_OpInfo opKind0 opRefs0 saveOp0 restoreOp0 applyAllocs0 ->
+    restoreOp0}
+
+applyAllocs :: (OpInfo a1 a2 a3 a4) -> a2 -> ([]
+                          ((,) VarId PhysReg)) -> a3
+applyAllocs o =
+  case o of {
+   Build_OpInfo opKind0 opRefs0 saveOp0 restoreOp0 applyAllocs0 ->
+    applyAllocs0}
+
+type BlockId = Prelude.Int
+
+data BlockInfo blockType1 blockType2 opType1 opType2 =
+   Build_BlockInfo (blockType1 -> BlockId) (blockType1 ->
+                                                               []
+                                                               BlockId) 
+ (blockType1 -> [] opType1) (blockType1 -> ([] opType2) -> blockType2)
+
+coq_BlockInfo_rect :: ((a1 -> BlockId) -> (a1 -> []
+                                 BlockId) -> (a1 -> [] a3) -> (a1
+                                 -> ([] a4) -> a2) -> a5) ->
+                                 (BlockInfo a1 a2 a3 a4) -> a5
+coq_BlockInfo_rect f b =
+  case b of {
+   Build_BlockInfo x x0 x1 x2 -> f x x0 x1 x2}
+
+coq_BlockInfo_rec :: ((a1 -> BlockId) -> (a1 -> []
+                                BlockId) -> (a1 -> [] a3) -> (a1 ->
+                                ([] a4) -> a2) -> a5) -> (BlockInfo
+                                a1 a2 a3 a4) -> a5
+coq_BlockInfo_rec =
+  coq_BlockInfo_rect
+
+blockId :: (BlockInfo a1 a2 a3 a4) -> a1 ->
+                      BlockId
+blockId b =
+  case b of {
+   Build_BlockInfo blockId0 blockSuccessors0 blockOps0
+    setBlockOps0 -> blockId0}
+
+blockSuccessors :: (BlockInfo a1 a2 a3 a4) -> a1 -> []
+                              BlockId
+blockSuccessors b =
+  case b of {
+   Build_BlockInfo blockId0 blockSuccessors0 blockOps0
+    setBlockOps0 -> blockSuccessors0}
+
+blockOps :: (BlockInfo a1 a2 a3 a4) -> a1 -> [] a3
+blockOps b =
+  case b of {
+   Build_BlockInfo blockId0 blockSuccessors0 blockOps0
+    setBlockOps0 -> blockOps0}
+
+setBlockOps :: (BlockInfo a1 a2 a3 a4) -> a1 -> ([] 
+                          a4) -> a2
+setBlockOps b =
+  case b of {
+   Build_BlockInfo blockId0 blockSuccessors0 blockOps0
+    setBlockOps0 -> setBlockOps0}
+
+type BoundedRange = Range.RangeDesc
+
+transportBoundedRange :: Prelude.Int -> Prelude.Int ->
+                                    BoundedRange ->
+                                    BoundedRange
+transportBoundedRange base prev x =
+  x
+
+data BuildState =
+   Build_BuildState Prelude.Int ([]
+                                          (Prelude.Maybe
+                                          BoundedRange)) ([]
+                                                                   (Prelude.Maybe
+                                                                   BoundedRange))
+
+coq_BuildState_rect :: (Prelude.Int -> ([]
+                                  (Prelude.Maybe BoundedRange)) ->
+                                  ([] (Prelude.Maybe BoundedRange))
+                                  -> a1) -> BuildState -> a1
+coq_BuildState_rect f b =
+  case b of {
+   Build_BuildState x x0 x1 -> f x x0 x1}
+
+coq_BuildState_rec :: (Prelude.Int -> ([]
+                                 (Prelude.Maybe BoundedRange)) ->
+                                 ([] (Prelude.Maybe BoundedRange))
+                                 -> a1) -> BuildState -> a1
+coq_BuildState_rec =
+  coq_BuildState_rect
+
+bsPos :: BuildState -> Prelude.Int
+bsPos b =
+  case b of {
+   Build_BuildState bsPos0 bsVars0 bsRegs0 -> bsPos0}
+
+bsVars :: BuildState -> []
+                     (Prelude.Maybe BoundedRange)
+bsVars b =
+  case b of {
+   Build_BuildState bsPos0 bsVars0 bsRegs0 -> bsVars0}
+
+bsRegs :: BuildState -> []
+                     (Prelude.Maybe BoundedRange)
+bsRegs b =
+  case b of {
+   Build_BuildState bsPos0 bsVars0 bsRegs0 -> bsRegs0}
+
+foldOps :: (BlockInfo a1 a2 a3 a4) -> (a5 -> a3 -> a5)
+                      -> a5 -> ([] a1) -> a5
+foldOps binfo f z =
+  Data.List.foldl' (\bacc blk ->
+    Data.List.foldl' f bacc (blockOps binfo blk)) z
+
+countOps :: (BlockInfo a1 a2 a3 a4) -> ([] a1) ->
+                       Prelude.Int
+countOps binfo =
+  foldOps binfo (\acc x -> (Prelude.succ) acc) 0
+
+foldOpsRev :: (BlockInfo a1 a2 a3 a4) -> (a5 -> a3 ->
+                         a5) -> a5 -> ([] a1) -> a5
+foldOpsRev binfo f z blocks =
+  Data.List.foldl' (\bacc blk ->
+    Data.List.foldl' f bacc (Seq.rev (blockOps binfo blk))) z
+    (Seq.rev blocks)
+
+processOperations :: (VarInfo a6) -> (OpInfo
+                                a1 a4 a5 a6) -> (BlockInfo 
+                                a2 a3 a4 a5) -> ([] a2) ->
+                                BuildState
+processOperations vinfo oinfo binfo blocks =
+  (Prelude.flip (Prelude.$))
+    (foldOps binfo (\x op ->
+      case x of {
+       (,) n m -> (,) ((Prelude.succ) n)
+        (Data.List.foldl' (\m0 v ->
+          Prelude.max m0 (varId vinfo v)) m
+          (Prelude.fst (opRefs oinfo op)))}) ((,) 0 0) blocks)
+    (\_top_assumption_ ->
+    let {
+     _evar_0_ = \opCount highestVar ->
+      let {
+       z = Build_BuildState opCount
+        (Seq.nseq ((Prelude.succ) highestVar) Prelude.Nothing)
+        (Data.List.replicate maxReg Prelude.Nothing)}
+      in
+      foldOpsRev binfo (\_top_assumption_0 ->
+        let {
+         _evar_0_ = \pos vars regs op ->
+          (Prelude.flip (Prelude.$)) __ (\_ ->
+            let {
+             _evar_0_ = \vars0 regs0 -> Build_BuildState 0 vars0
+              regs0}
+            in
+            let {
+             _evar_0_0 = \pos0 vars0 regs0 ->
+              let {_top_assumption_1 = opRefs oinfo op} in
+              let {
+               _evar_0_0 = \varRefs regRefs -> Build_BuildState
+                pos0
+                ((Prelude.flip (Prelude.$))
+                  ((Prelude.flip (Prelude.$)) vars0 (\vars' ->
+                    let {
+                     vars'0 = Prelude.map
+                                (Lib.option_map
+                                  (transportBoundedRange
+                                    ((Prelude.succ) (Ssrnat.double pos0))
+                                    ((Prelude.succ)
+                                    (Ssrnat.double ((Prelude.succ) pos0)))))
+                                vars'}
+                    in
+                    Data.List.foldl' (\vars'1 v ->
+                      let {
+                       upos = Range.Build_UsePos ((Prelude.succ)
+                        (Ssrnat.double pos0))
+                        (regRequired vinfo v)}
+                      in
+                      (Prelude.flip (Prelude.$)) __ (\_ ->
+                        Seq.set_nth Prelude.Nothing vars'1
+                          (varId vinfo v) (Prelude.Just
+                          (let {
+                            _evar_0_0 = \_top_assumption_2 ->
+                             Range.Build_RangeDesc (Range.uloc upos)
+                             (Range.rend ( _top_assumption_2)) ((:) upos
+                             (Range.ups ( _top_assumption_2)))}
+                           in
+                           let {
+                            _evar_0_1 = Range.Build_RangeDesc
+                             (Range.uloc upos) ((Prelude.succ)
+                             (Range.uloc upos)) ((:[]) upos)}
+                           in
+                           case Seq.nth Prelude.Nothing vars0
+                                  (varId vinfo v) of {
+                            Prelude.Just x -> _evar_0_0 x;
+                            Prelude.Nothing -> _evar_0_1})))) vars'0 varRefs))
+                  (\x -> x))
+                ((Prelude.flip (Prelude.$))
+                  ((Prelude.flip (Prelude.$)) regs0 (\regs' ->
+                    let {
+                     regs'0 = LinearScan.Utils.vmap maxReg
+                                (Lib.option_map
+                                  (transportBoundedRange
+                                    ((Prelude.succ) (Ssrnat.double pos0))
+                                    ((Prelude.succ)
+                                    (Ssrnat.double ((Prelude.succ) pos0)))))
+                                regs'}
+                    in
+                    Data.List.foldl' (\regs'1 reg ->
+                      let {
+                       upos = Range.Build_UsePos ((Prelude.succ)
+                        (Ssrnat.double pos0)) Prelude.True}
+                      in
+                      (Prelude.flip (Prelude.$)) __ (\_ ->
+                        LinearScan.Utils.set_nth maxReg regs'1 reg
+                          (Prelude.Just
+                          (let {
+                            _evar_0_0 = \_top_assumption_2 ->
+                             Range.Build_RangeDesc (Range.uloc upos)
+                             (Range.rend ( _top_assumption_2)) ((:) upos
+                             (Range.ups ( _top_assumption_2)))}
+                           in
+                           let {
+                            _evar_0_1 = Range.Build_RangeDesc
+                             (Range.uloc upos) ((Prelude.succ)
+                             (Range.uloc upos)) ((:[]) upos)}
+                           in
+                           case LinearScan.Utils.nth maxReg regs0
+                                  reg of {
+                            Prelude.Just x -> _evar_0_0 x;
+                            Prelude.Nothing -> _evar_0_1})))) regs'0 regRefs))
+                  (\x -> x))}
+              in
+              case _top_assumption_1 of {
+               (,) x x0 -> _evar_0_0 x x0}}
+            in
+            (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
+              (\_ ->
+              _evar_0_ vars regs)
+              (\x ->
+              _evar_0_0 x vars regs)
+              pos)}
+        in
+        case _top_assumption_0 of {
+         Build_BuildState x x0 x1 -> _evar_0_ x x0 x1}) z blocks}
+    in
+    case _top_assumption_ of {
+     (,) x x0 -> _evar_0_ x x0})
+
+computeBlockOrder :: ([] a1) -> [] a1
+computeBlockOrder blocks =
+  blocks
+
+numberOperations :: ([] a1) -> [] a1
+numberOperations blocks =
+  blocks
+
+type OpId = Prelude.Int
+
+data BlockLiveSets =
+   Build_BlockLiveSets ([] VarId) ([] VarId) 
+ ([] VarId) ([] VarId) OpId OpId
+
+coq_BlockLiveSets_rect :: (([] VarId) -> ([]
+                                     VarId) -> ([] VarId)
+                                     -> ([] VarId) ->
+                                     OpId -> OpId -> a1)
+                                     -> BlockLiveSets -> a1
+coq_BlockLiveSets_rect f b =
+  case b of {
+   Build_BlockLiveSets x x0 x1 x2 x3 x4 -> f x x0 x1 x2 x3 x4}
+
+coq_BlockLiveSets_rec :: (([] VarId) -> ([]
+                                    VarId) -> ([] VarId)
+                                    -> ([] VarId) -> OpId
+                                    -> OpId -> a1) ->
+                                    BlockLiveSets -> a1
+coq_BlockLiveSets_rec =
+  coq_BlockLiveSets_rect
+
+blockLiveGen :: BlockLiveSets -> [] VarId
+blockLiveGen b =
+  case b of {
+   Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
+    blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveGen0}
+
+blockLiveKill :: BlockLiveSets -> [] VarId
+blockLiveKill b =
+  case b of {
+   Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
+    blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveKill0}
+
+blockLiveIn :: BlockLiveSets -> [] VarId
+blockLiveIn b =
+  case b of {
+   Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
+    blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveIn0}
+
+blockLiveOut :: BlockLiveSets -> [] VarId
+blockLiveOut b =
+  case b of {
+   Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
+    blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveOut0}
+
+blockFirstOpId :: BlockLiveSets -> OpId
+blockFirstOpId b =
+  case b of {
+   Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
+    blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockFirstOpId0}
+
+blockLastOpId :: BlockLiveSets -> OpId
+blockLastOpId b =
+  case b of {
+   Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
+    blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLastOpId0}
+
+coq_IntMap_rect :: a2 -> (([] ((,) Prelude.Int a1)) -> a2) ->
+                              (Data.IntMap.IntMap a1) -> a2
+coq_IntMap_rect f f0 i =
+  (\fO fS _ -> fO ())
+    (\_ ->
+    f)
+    (\x ->
+    f0 x)
+    i
+
+coq_IntMap_rec :: a2 -> (([] ((,) Prelude.Int a1)) -> a2) ->
+                             (Data.IntMap.IntMap a1) -> a2
+coq_IntMap_rec =
+  coq_IntMap_rect
+
+union :: Eqtype.Equality__Coq_type -> ([]
+                    Eqtype.Equality__Coq_sort) -> ([]
+                    Eqtype.Equality__Coq_sort) -> []
+                    Eqtype.Equality__Coq_sort
+union a m1 m2 =
+  Seq.undup a ((Prelude.++) m1 m2)
+
+relative_complement :: Eqtype.Equality__Coq_type -> ([]
+                                  Eqtype.Equality__Coq_sort) -> ([]
+                                  Eqtype.Equality__Coq_sort) -> []
+                                  Eqtype.Equality__Coq_sort
+relative_complement a m1 m2 =
+  Prelude.filter (\i ->
+    Prelude.not
+      (Ssrbool.in_mem i (Ssrbool.mem (Seq.seq_predType a) (unsafeCoerce m2))))
+    m1
+
+computeLocalLiveSets :: (VarInfo a6) ->
+                                   (OpInfo a1 a4 a5 a6) ->
+                                   (BlockInfo a2 a3 a4 a5) -> ([]
+                                   a2) -> Data.IntMap.IntMap
+                                   BlockLiveSets
+computeLocalLiveSets vinfo oinfo binfo blocks =
+  Prelude.snd
+    (Lib.forFold ((,) ((Prelude.succ) 0) Data.IntMap.empty) blocks (\acc b ->
+      case acc of {
+       (,) idx m ->
+        let {liveSet = Build_BlockLiveSets [] [] [] [] idx idx} in
+        case Lib.forFold ((,) idx liveSet) (blockOps binfo b)
+               (\acc0 o ->
+               case acc0 of {
+                (,) lastIdx liveSet1 -> (,) ((Prelude.succ) ((Prelude.succ)
+                 lastIdx))
+                 (Lib.forFold liveSet1
+                   (Prelude.fst (opRefs oinfo o)) (\liveSet2 v ->
+                   let {vid = varId vinfo v} in
+                   case varKind vinfo v of {
+                    Input ->
+                     case Prelude.not
+                            (Ssrbool.in_mem (unsafeCoerce vid)
+                              (Ssrbool.mem
+                                (Seq.seq_predType Ssrnat.nat_eqType)
+                                (unsafeCoerce
+                                  (blockLiveKill liveSet2)))) of {
+                      Prelude.True -> Build_BlockLiveSets ((:) vid
+                       (blockLiveGen liveSet2))
+                       (blockLiveKill liveSet2)
+                       (blockLiveIn liveSet2)
+                       (blockLiveOut liveSet2)
+                       (blockFirstOpId liveSet2) lastIdx;
+                      Prelude.False -> liveSet2};
+                    _ -> Build_BlockLiveSets
+                     (blockLiveGen liveSet2) ((:) vid
+                     (blockLiveKill liveSet2))
+                     (blockLiveIn liveSet2)
+                     (blockLiveOut liveSet2)
+                     (blockFirstOpId liveSet2) lastIdx}))}) of {
+         (,) lastIdx' liveSet3 -> (,) lastIdx'
+          (Data.IntMap.insert (blockId binfo b) liveSet3 m)}}))
+
+computeGlobalLiveSets :: (BlockInfo a1 a2 a3 a4) -> ([]
+                                    a1) -> (Data.IntMap.IntMap
+                                    BlockLiveSets) ->
+                                    Data.IntMap.IntMap
+                                    BlockLiveSets
+computeGlobalLiveSets binfo blocks liveSets =
+  Lib.forFold liveSets (Seq.rev blocks) (\liveSets1 b ->
+    let {bid = blockId binfo b} in
+    case Data.IntMap.lookup bid liveSets1 of {
+     Prelude.Just liveSet ->
+      let {
+       liveSet2 = Lib.forFold liveSet (blockSuccessors binfo b)
+                    (\liveSet1 s_bid ->
+                    case Data.IntMap.lookup s_bid liveSets1 of {
+                     Prelude.Just sux -> Build_BlockLiveSets
+                      (blockLiveGen liveSet1)
+                      (blockLiveKill liveSet1)
+                      (blockLiveIn liveSet1)
+                      (unsafeCoerce
+                        (union Ssrnat.nat_eqType
+                          (unsafeCoerce (blockLiveOut liveSet1))
+                          (unsafeCoerce (blockLiveIn sux))))
+                      (blockFirstOpId liveSet1)
+                      (blockLastOpId liveSet1);
+                     Prelude.Nothing -> liveSet1})}
+      in
+      Data.IntMap.insert bid (Build_BlockLiveSets
+        (blockLiveGen liveSet2)
+        (blockLiveKill liveSet2)
+        (unsafeCoerce
+          (union Ssrnat.nat_eqType
+            (relative_complement Ssrnat.nat_eqType
+              (unsafeCoerce (blockLiveOut liveSet2))
+              (unsafeCoerce (blockLiveKill liveSet2)))
+            (unsafeCoerce (blockLiveGen liveSet2))))
+        (blockLiveOut liveSet2)
+        (blockFirstOpId liveSet2)
+        (blockLastOpId liveSet2)) liveSets1;
+     Prelude.Nothing -> liveSets1})
+
+buildIntervals :: (VarInfo a6) -> (OpInfo 
+                             a1 a4 a5 a6) -> (BlockInfo a2 
+                             a3 a4 a5) -> ([] a2) -> ScanStateSig
+buildIntervals vinfo oinfo binfo blocks =
+  let {
+   mkint = \vid ss pos mx f ->
+    case mx of {
+     Prelude.Just b ->
+      f ss __ (Interval.Build_IntervalDesc vid (Range.rbeg ( b))
+        (Range.rend ( b)) Interval.Whole ((:[]) ( b))) __;
+     Prelude.Nothing -> ss}}
+  in
+  let {
+   handleVar = \pos vid ss mx ->
+    mkint vid ss pos mx (\sd _ d _ ->
+      packScanState Pending
+        (Build_ScanStateDesc ((Prelude.succ)
+        (nextInterval sd))
+        (LinearScan.Utils.snoc (nextInterval sd)
+          (intervals sd) d) (fixedIntervals sd)
+        (Data.List.insertBy (Data.Ord.comparing Prelude.snd) ((,)
+          ( (nextInterval sd)) (Interval.ibeg d))
+          (Prelude.map Prelude.id (unhandled sd)))
+        (Prelude.map Prelude.id (active sd))
+        (Prelude.map Prelude.id (inactive sd))
+        (Prelude.map Prelude.id (handled sd))))}
+  in
+  let {bs = processOperations vinfo oinfo binfo blocks} in
+  let {
+   regs = LinearScan.Utils.vmap maxReg (\mr ->
+            case mr of {
+             Prelude.Just y -> Prelude.Just
+              (Interval.packInterval (Interval.Build_IntervalDesc 0
+                (Range.rbeg ( y)) (Range.rend ( y)) Interval.Whole ((:[])
+                ( y))));
+             Prelude.Nothing -> Prelude.Nothing}) (bsRegs bs)}
+  in
+  let {
+   s2 = packScanState Pending
+          (Build_ScanStateDesc
+          (nextInterval (Build_ScanStateDesc 0 []
+            (Data.List.replicate maxReg Prelude.Nothing) [] [] []
+            []))
+          (intervals (Build_ScanStateDesc 0 []
+            (Data.List.replicate maxReg Prelude.Nothing) [] [] []
+            [])) regs
+          (unhandled (Build_ScanStateDesc 0 []
+            (Data.List.replicate maxReg Prelude.Nothing) [] [] []
+            []))
+          (active (Build_ScanStateDesc 0 []
+            (Data.List.replicate maxReg Prelude.Nothing) [] [] []
+            []))
+          (inactive (Build_ScanStateDesc 0 []
+            (Data.List.replicate maxReg Prelude.Nothing) [] [] []
+            []))
+          (handled (Build_ScanStateDesc 0 []
+            (Data.List.replicate maxReg Prelude.Nothing) [] [] []
+            [])))}
+  in
+  let {
+   s3 = Lib.foldl_with_index (handleVar (bsPos bs)) s2
+          (bsVars bs)}
+  in
+  packScanState InUse ( s3)
+
+data InsertPos =
+   AtBegin VarId PhysReg
+ | AtEnd VarId PhysReg
+
+coq_InsertPos_rect :: (VarId -> PhysReg -> a1)
+                                 -> (VarId -> PhysReg ->
+                                 a1) -> InsertPos -> a1
+coq_InsertPos_rect f f0 i =
+  case i of {
+   AtBegin x x0 -> f x x0;
+   AtEnd x x0 -> f0 x x0}
+
+coq_InsertPos_rec :: (VarId -> PhysReg -> a1)
+                                -> (VarId -> PhysReg ->
+                                a1) -> InsertPos -> a1
+coq_InsertPos_rec =
+  coq_InsertPos_rect
+
+eqact :: InsertPos -> InsertPos ->
+                    Prelude.Bool
+eqact v1 v2 =
+  case v1 of {
+   AtBegin v3 r1 ->
+    case v2 of {
+     AtBegin v4 r2 ->
+      (Prelude.&&)
+        (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce v3) (unsafeCoerce v4))
+        (Eqtype.eq_op (Fintype.ordinal_eqType maxReg)
+          (unsafeCoerce r1) (unsafeCoerce r2));
+     AtEnd v p -> Prelude.False};
+   AtEnd v3 r1 ->
+    case v2 of {
+     AtBegin v p -> Prelude.False;
+     AtEnd v4 r2 ->
+      (Prelude.&&)
+        (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce v3) (unsafeCoerce v4))
+        (Eqtype.eq_op (Fintype.ordinal_eqType maxReg)
+          (unsafeCoerce r1) (unsafeCoerce r2))}}
+
+eqactP :: Eqtype.Equality__Coq_axiom InsertPos
+eqactP _top_assumption_ =
+  let {
+   _evar_0_ = \v1 r1 _top_assumption_0 ->
+    let {
+     _evar_0_ = \v2 r2 ->
+      let {
+       _evar_0_ = \_ ->
+        let {
+         _evar_0_ = let {
+                     _evar_0_ = \_ ->
+                      let {
+                       _evar_0_ = let {_evar_0_ = Ssrbool.ReflectT} in
+                                   _evar_0_}
+                      in
+                       _evar_0_}
+                    in
+                    let {
+                     _evar_0_0 = \_ ->
+                      let {_evar_0_0 = Ssrbool.ReflectF} in  _evar_0_0}
+                    in
+                    case Eqtype.eqP
+                           (Fintype.ordinal_eqType maxReg) r1 r2 of {
+                     Ssrbool.ReflectT -> _evar_0_ __;
+                     Ssrbool.ReflectF -> _evar_0_0 __}}
+        in
+         _evar_0_}
+      in
+      let {
+       _evar_0_0 = \_ -> let {_evar_0_0 = Ssrbool.ReflectF} in  _evar_0_0}
+      in
+      case Eqtype.eqP Ssrnat.nat_eqType v1 v2 of {
+       Ssrbool.ReflectT -> _evar_0_ __;
+       Ssrbool.ReflectF -> _evar_0_0 __}}
+    in
+    let {
+     _evar_0_0 = \v2 r2 ->
+      let {
+       _evar_0_0 = \_ -> let {_evar_0_0 = Ssrbool.ReflectF} in  _evar_0_0}
+      in
+      let {_evar_0_1 = \_ -> Ssrbool.ReflectF} in
+      case Eqtype.eqP Ssrnat.nat_eqType v1 v2 of {
+       Ssrbool.ReflectT -> _evar_0_0 __;
+       Ssrbool.ReflectF -> _evar_0_1 __}}
+    in
+    case _top_assumption_0 of {
+     AtBegin x x0 -> unsafeCoerce _evar_0_ x x0;
+     AtEnd x x0 -> unsafeCoerce _evar_0_0 x x0}}
+  in
+  let {
+   _evar_0_0 = \v1 r1 _top_assumption_0 ->
+    let {
+     _evar_0_0 = \v2 r2 ->
+      let {
+       _evar_0_0 = \_ -> let {_evar_0_0 = Ssrbool.ReflectF} in  _evar_0_0}
+      in
+      let {_evar_0_1 = \_ -> Ssrbool.ReflectF} in
+      case Eqtype.eqP Ssrnat.nat_eqType v1 v2 of {
+       Ssrbool.ReflectT -> _evar_0_0 __;
+       Ssrbool.ReflectF -> _evar_0_1 __}}
+    in
+    let {
+     _evar_0_1 = \v2 r2 ->
+      let {
+       _evar_0_1 = \_ ->
+        let {
+         _evar_0_1 = let {
+                      _evar_0_1 = \_ ->
+                       let {
+                        _evar_0_1 = let {_evar_0_1 = Ssrbool.ReflectT} in
+                                     _evar_0_1}
+                       in
+                        _evar_0_1}
+                     in
+                     let {
+                      _evar_0_2 = \_ ->
+                       let {_evar_0_2 = Ssrbool.ReflectF} in  _evar_0_2}
+                     in
+                     case Eqtype.eqP
+                            (Fintype.ordinal_eqType maxReg) r1 r2 of {
+                      Ssrbool.ReflectT -> _evar_0_1 __;
+                      Ssrbool.ReflectF -> _evar_0_2 __}}
+        in
+         _evar_0_1}
+      in
+      let {
+       _evar_0_2 = \_ -> let {_evar_0_2 = Ssrbool.ReflectF} in  _evar_0_2}
+      in
+      case Eqtype.eqP Ssrnat.nat_eqType v1 v2 of {
+       Ssrbool.ReflectT -> _evar_0_1 __;
+       Ssrbool.ReflectF -> _evar_0_2 __}}
+    in
+    case _top_assumption_0 of {
+     AtBegin x x0 -> unsafeCoerce _evar_0_0 x x0;
+     AtEnd x x0 -> unsafeCoerce _evar_0_1 x x0}}
+  in
+  case _top_assumption_ of {
+   AtBegin x x0 -> unsafeCoerce _evar_0_ x x0;
+   AtEnd x x0 -> unsafeCoerce _evar_0_0 x x0}
+
+act_eqMixin :: Eqtype.Equality__Coq_mixin_of InsertPos
+act_eqMixin =
+  Eqtype.Equality__Mixin eqact eqactP
+
+act_eqType :: Eqtype.Equality__Coq_type
+act_eqType =
+  unsafeCoerce act_eqMixin
+
+coq_InsertPos_eqType :: Eqtype.Equality__Coq_type ->
+                                   Eqtype.Equality__Coq_type
+coq_InsertPos_eqType a =
+  unsafeCoerce act_eqMixin
+
+resolveDataFlow :: (BlockInfo a1 a2 a3 a4) ->
+                              ScanStateDesc -> ([] a1) ->
+                              (Data.IntMap.IntMap BlockLiveSets) ->
+                              Data.IntMap.IntMap ([] InsertPos)
+resolveDataFlow binfo sd blocks liveSets =
+  Lib.forFold Data.IntMap.empty blocks (\mappings b ->
+    let {bid = blockId binfo b} in
+    case Data.IntMap.lookup bid liveSets of {
+     Prelude.Just from ->
+      let {successors = blockSuccessors binfo b} in
+      Lib.forFold mappings successors (\ms s_bid ->
+        case Data.IntMap.lookup s_bid liveSets of {
+         Prelude.Just to ->
+          Lib.forFold ms (blockLiveIn to) (\ms' vid ->
+            case lookupInterval sd __ vid
+                   (blockLastOpId from) of {
+             Prelude.Just from_interval ->
+              case lookupInterval sd __ vid
+                     (blockFirstOpId to) of {
+               Prelude.Just to_interval ->
+                case Prelude.not
+                       (Eqtype.eq_op
+                         (Fintype.ordinal_eqType
+                           (nextInterval sd))
+                         (unsafeCoerce from_interval)
+                         (unsafeCoerce to_interval)) of {
+                 Prelude.True ->
+                  let {
+                   in_from = (Prelude.<=) (Data.List.length successors)
+                               ((Prelude.succ) 0)}
+                  in
+                  let {
+                   mreg = lookupRegister sd __
+                            (case in_from of {
+                              Prelude.True -> unsafeCoerce from_interval;
+                              Prelude.False -> unsafeCoerce to_interval})}
+                  in
+                  case mreg of {
+                   Prelude.Just reg ->
+                    let {
+                     ins = case in_from of {
+                            Prelude.True -> AtEnd vid reg;
+                            Prelude.False -> AtBegin vid reg}}
+                    in
+                    let {
+                     f = \mxs ->
+                      case mxs of {
+                       Prelude.Just xs ->
+                        case Prelude.not
+                               (Ssrbool.in_mem (unsafeCoerce ins)
+                                 (Ssrbool.mem
+                                   (Seq.seq_predType act_eqType)
+                                   xs)) of {
+                         Prelude.True -> Prelude.Just ((:) ins
+                          (unsafeCoerce xs));
+                         Prelude.False -> Prelude.Just (unsafeCoerce xs)};
+                       Prelude.Nothing -> Prelude.Just ((:) ins [])}}
+                    in
+                    let {
+                     key = case in_from of {
+                            Prelude.True -> bid;
+                            Prelude.False -> s_bid}}
+                    in
+                    Data.IntMap.alter (unsafeCoerce f) key ms';
+                   Prelude.Nothing -> ms'};
+                 Prelude.False -> ms'};
+               Prelude.Nothing -> ms'};
+             Prelude.Nothing -> ms'});
+         Prelude.Nothing -> ms});
+     Prelude.Nothing -> mappings})
+
+data AssnStateInfo accType =
+   Build_AssnStateInfo OpId accType
+
+coq_AssnStateInfo_rect :: (OpId -> a1 -> a2) ->
+                                     (AssnStateInfo a1) -> a2
+coq_AssnStateInfo_rect f a =
+  case a of {
+   Build_AssnStateInfo x x0 -> f x x0}
+
+coq_AssnStateInfo_rec :: (OpId -> a1 -> a2) ->
+                                    (AssnStateInfo a1) -> a2
+coq_AssnStateInfo_rec =
+  coq_AssnStateInfo_rect
+
+assnOpId :: (AssnStateInfo a1) -> OpId
+assnOpId a =
+  case a of {
+   Build_AssnStateInfo assnOpId0 assnAcc0 -> assnOpId0}
+
+assnAcc :: (AssnStateInfo a1) -> a1
+assnAcc a =
+  case a of {
+   Build_AssnStateInfo assnOpId0 assnAcc0 -> assnAcc0}
+
+type AssnState accType a =
+  State.State (AssnStateInfo accType) a
+
+saveOpM :: (OpInfo a1 a2 a3 a4) -> VarId ->
+                      PhysReg -> AssnState a1 a3
+saveOpM oinfo vid reg =
+  State.bind (\assn ->
+    case saveOp oinfo vid reg (assnAcc assn) of {
+     (,) sop acc' ->
+      State.bind (\x -> State.pure sop)
+        (State.put (Build_AssnStateInfo (assnOpId assn)
+          acc'))}) State.get
+
+restoreOpM :: (OpInfo a1 a2 a3 a4) -> VarId ->
+                         PhysReg -> AssnState a1 
+                         a3
+restoreOpM oinfo vid reg =
+  State.bind (\assn ->
+    case restoreOp oinfo vid reg (assnAcc assn) of {
+     (,) rop acc' ->
+      State.bind (\x -> State.pure rop)
+        (State.put (Build_AssnStateInfo (assnOpId assn)
+          acc'))}) State.get
+
+pairM :: (AssnState a1 a2) -> (AssnState 
+                    a1 a3) -> AssnState a1 ((,) a2 a3)
+pairM x y =
+  State.bind (\x' -> State.bind (\y' -> State.pure ((,) x' y')) y) x
+
+savesAndRestores :: (OpInfo a1 a2 a3 a4) ->
+                               Eqtype.Equality__Coq_sort -> VarId
+                               -> PhysReg -> Interval.IntervalDesc
+                               -> AssnState a1
+                               ((,) ([] a3) ([] a3))
+savesAndRestores oinfo opid vid reg int =
+  let {
+   isFirst = Eqtype.eq_op Ssrnat.nat_eqType
+               (unsafeCoerce (Interval.firstUsePos int)) opid}
+  in
+  let {
+   isLast = Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)
+              (unsafeCoerce (Interval.nextUseAfter int (unsafeCoerce opid)))
+              (unsafeCoerce Prelude.Nothing)}
+  in
+  let {
+   save = State.bind (\sop -> State.pure ((:) sop []))
+            (saveOpM oinfo vid reg)}
+  in
+  let {
+   restore = State.bind (\rop -> State.pure ((:) rop []))
+               (restoreOpM oinfo vid reg)}
+  in
+  case Interval.iknd int of {
+   Interval.Whole -> State.pure ((,) [] []);
+   Interval.LeftMost ->
+    case isLast of {
+     Prelude.True -> pairM (State.pure []) save;
+     Prelude.False -> State.pure ((,) [] [])};
+   Interval.Middle ->
+    case isFirst of {
+     Prelude.True ->
+      case isLast of {
+       Prelude.True -> pairM restore save;
+       Prelude.False -> pairM restore (State.pure [])};
+     Prelude.False ->
+      case isLast of {
+       Prelude.True -> pairM (State.pure []) save;
+       Prelude.False -> State.pure ((,) [] [])}};
+   Interval.RightMost ->
+    case isFirst of {
+     Prelude.True -> pairM restore (State.pure []);
+     Prelude.False -> State.pure ((,) [] [])}}
+
+collectAllocs :: (VarInfo a4) -> (OpInfo 
+                            a1 a2 a3 a4) -> Prelude.Int -> ([]
+                            ((,) Interval.IntervalDesc PhysReg)) ->
+                            ((,)
+                            ((,) ([] ((,) VarId PhysReg))
+                            ([] a3)) ([] a3)) -> a4 -> AssnState 
+                            a1
+                            ((,)
+                            ((,) ([] ((,) VarId PhysReg))
+                            ([] a3)) ([] a3))
+collectAllocs vinfo oinfo opid ints acc v =
+  let {vid = varId vinfo v} in
+  let {
+   v_ints = Prelude.filter (\x ->
+              isWithin (Prelude.fst x) vid opid) ints}
+  in
+  case v_ints of {
+   [] -> State.pure acc;
+   (:) p l ->
+    case p of {
+     (,) int reg ->
+      case acc of {
+       (,) p0 saves' ->
+        case p0 of {
+         (,) allocs' restores' ->
+          State.bind (\res ->
+            case res of {
+             (,) rs ss ->
+              State.pure ((,) ((,) ((:) ((,) vid reg) allocs')
+                ((Prelude.++) rs restores')) ((Prelude.++) ss saves'))})
+            (savesAndRestores oinfo (unsafeCoerce opid) vid reg
+              int)}}}}
+
+doAllocations :: (VarInfo a4) -> (OpInfo 
+                            a1 a2 a3 a4) -> ([]
+                            ((,) Interval.IntervalDesc PhysReg)) ->
+                            a2 -> AssnState a1 ([] a3)
+doAllocations vinfo oinfo ints op =
+  State.bind (\assn ->
+    let {opid = assnOpId assn} in
+    let {vars = Prelude.fst (opRefs oinfo op)} in
+    State.bind (\res ->
+      case res of {
+       (,) y saves ->
+        case y of {
+         (,) allocs restores ->
+          let {op' = applyAllocs oinfo op allocs} in
+          State.bind (\x ->
+            State.pure ((Prelude.++) restores ((:) op' saves)))
+            (State.modify (\assn' -> Build_AssnStateInfo
+              ((Prelude.succ) ((Prelude.succ) opid))
+              (assnAcc assn')))}})
+      (State.forFoldM ((,) ((,) [] []) []) vars
+        (collectAllocs vinfo oinfo opid ints))) State.get
+
+resolveMappings :: (OpInfo a1 a2 a3 a4) -> Prelude.Int
+                              -> ([] a2) -> ([] a3) -> (Data.IntMap.IntMap
+                              ([] InsertPos)) -> State.State
+                              (AssnStateInfo a1) ([] a3)
+resolveMappings oinfo bid ops ops' mappings =
+  case Data.IntMap.lookup bid mappings of {
+   Prelude.Just inss ->
+    State.forFoldM ops' inss (\ops'' ins ->
+      case ins of {
+       AtBegin vid reg ->
+        State.bind (\rop -> State.pure ((:) rop ops''))
+          (restoreOpM oinfo vid reg);
+       AtEnd vid reg ->
+        State.bind (\sop ->
+          State.pure
+            (case ops of {
+              [] -> (:) sop [];
+              (:) o os ->
+               case ops'' of {
+                [] -> (:) sop [];
+                (:) o'' os'' ->
+                 case opKind oinfo (Seq.last o os) of {
+                  IsBranch ->
+                   (Prelude.++) (Seq.belast o'' os'') ((:) sop ((:)
+                     (Seq.last o'' os'') []));
+                  _ -> (Prelude.++) ops' ((:) sop [])}}}))
+          (saveOpM oinfo vid reg)});
+   Prelude.Nothing -> State.pure ops'}
+
+considerOps :: (OpInfo a1 a4 a5 a6) ->
+                          (BlockInfo a2 a3 a4 a5) -> (a4 ->
+                          AssnState a1 ([] a5)) ->
+                          (Data.IntMap.IntMap ([] InsertPos)) ->
+                          ([] a2) -> State.State (AssnStateInfo a1)
+                          ([] a3)
+considerOps oinfo binfo f mappings =
+  State.mapM (\blk ->
+    let {ops = blockOps binfo blk} in
+    State.bind (\ops' ->
+      let {bid = blockId binfo blk} in
+      State.bind (\ops'' ->
+        State.pure (setBlockOps binfo blk ops''))
+        (resolveMappings oinfo bid ops ops' mappings))
+      (State.concatMapM f ops))
+
+assignRegNum :: (VarInfo a6) -> (OpInfo 
+                           a1 a4 a5 a6) -> (BlockInfo a2 a3 
+                           a4 a5) -> ScanStateDesc ->
+                           (Data.IntMap.IntMap ([] InsertPos)) ->
+                           ([] a2) -> a1 -> (,) ([] a3) a1
+assignRegNum vinfo oinfo binfo sd mappings blocks acc =
+  case considerOps oinfo binfo
+         (doAllocations vinfo oinfo
+           (Prelude.map (\x -> (,)
+             (Interval.getIntervalDesc
+               (
+                 (LinearScan.Utils.nth (nextInterval sd)
+                   (intervals sd) (Prelude.fst x))))
+             (Prelude.snd x))
+             ((Prelude.++) (handled sd)
+               ((Prelude.++) (active sd) (inactive sd)))))
+         mappings blocks (Build_AssnStateInfo ((Prelude.succ) 0)
+         acc) of {
+   (,) blocks' assn -> (,) blocks' (assnAcc assn)}
+
+coq_SSMorph_rect :: ScanStateDesc ->
+                               ScanStateDesc -> (() -> a1) -> a1
+coq_SSMorph_rect sd1 sd2 f =
+  f __
+
+coq_SSMorph_rec :: ScanStateDesc ->
+                              ScanStateDesc -> (() -> a1) -> a1
+coq_SSMorph_rec sd1 sd2 f =
+  coq_SSMorph_rect sd1 sd2 f
+
+coq_SSMorphLen_rect :: ScanStateDesc ->
+                                  ScanStateDesc -> (() -> () -> a1)
+                                  -> a1
+coq_SSMorphLen_rect sd1 sd2 f =
+  f __ __
+
+coq_SSMorphLen_rec :: ScanStateDesc ->
+                                 ScanStateDesc -> (() -> () -> a1)
+                                 -> a1
+coq_SSMorphLen_rec sd1 sd2 f =
+  coq_SSMorphLen_rect sd1 sd2 f
+
+coq_SSMorphHasLen_rect :: ScanStateDesc ->
+                                     ScanStateDesc -> (() -> () ->
+                                     a1) -> a1
+coq_SSMorphHasLen_rect sd1 sd2 f =
+  f __ __
+
+coq_SSMorphHasLen_rec :: ScanStateDesc ->
+                                    ScanStateDesc -> (() -> () ->
+                                    a1) -> a1
+coq_SSMorphHasLen_rec sd1 sd2 f =
+  coq_SSMorphHasLen_rect sd1 sd2 f
+
+data SSInfo p =
+   Build_SSInfo ScanStateDesc p
+
+coq_SSInfo_rect :: ScanStateDesc ->
+                              (ScanStateDesc -> a1 -> () -> a2) ->
+                              (SSInfo a1) -> a2
+coq_SSInfo_rect startDesc f s =
+  case s of {
+   Build_SSInfo x x0 -> f x x0 __}
+
+coq_SSInfo_rec :: ScanStateDesc ->
+                             (ScanStateDesc -> a1 -> () -> a2) ->
+                             (SSInfo a1) -> a2
+coq_SSInfo_rec startDesc =
+  coq_SSInfo_rect startDesc
+
+thisDesc :: ScanStateDesc -> (SSInfo a1) ->
+                       ScanStateDesc
+thisDesc startDesc s =
+  case s of {
+   Build_SSInfo thisDesc0 thisHolds0 -> thisDesc0}
+
+thisHolds :: ScanStateDesc -> (SSInfo 
+                        a1) -> a1
+thisHolds startDesc s =
+  case s of {
+   Build_SSInfo thisDesc0 thisHolds0 -> thisHolds0}
+
+type SState p q a =
+  IState.IState SSError (SSInfo p) (SSInfo q) a
+
+withScanState :: ScanStateDesc ->
+                            (ScanStateDesc -> () ->
+                            SState a2 a3 a1) -> SState 
+                            a2 a3 a1
+withScanState pre f =
+  stbind (\i -> f (thisDesc pre i) __) IState.iget
+
+withScanStatePO :: ScanStateDesc ->
+                              (ScanStateDesc -> () ->
+                              SState () () a1) -> SState
+                              () () a1
+withScanStatePO pre f i =
+  case i of {
+   Build_SSInfo thisDesc0 _ ->
+    let {f0 = f thisDesc0 __} in
+    let {x = Build_SSInfo thisDesc0 __} in
+    let {x0 = f0 x} in
+    case x0 of {
+     Prelude.Left s -> Prelude.Left s;
+     Prelude.Right p -> Prelude.Right
+      (case p of {
+        (,) a0 s -> (,) a0
+         (case s of {
+           Build_SSInfo thisDesc1 _ -> Build_SSInfo
+            thisDesc1 __})})}}
+
+liftLen :: ScanStateDesc -> (ScanStateDesc ->
+                      SState () () a1) -> SState 
+                      () () a1
+liftLen pre f _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 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}
+
+weakenHasLen_ :: ScanStateDesc -> SState 
+                            () () ()
+weakenHasLen_ pre hS =
+  Prelude.Right ((,) ()
+    (case hS of {
+      Build_SSInfo thisDesc0 _ -> Build_SSInfo thisDesc0
+       __}))
+
+strengthenHasLen :: ScanStateDesc ->
+                               ScanStateDesc -> Prelude.Maybe 
+                               ()
+strengthenHasLen pre sd =
+  let {_evar_0_ = \_ -> Prelude.Nothing} in
+  let {_evar_0_0 = \_a_ _l_ -> Prelude.Just __} in
+  case unhandled sd of {
+   [] -> _evar_0_ __;
+   (:) x x0 -> _evar_0_0 x x0}
+
+withCursor :: ScanStateDesc -> (ScanStateDesc
+                         -> () -> SState () a1 a2) ->
+                         SState () a1 a2
+withCursor pre f x =
+  case x of {
+   Build_SSInfo thisDesc0 _ ->
+    f thisDesc0 __ (Build_SSInfo thisDesc0 __)}
+
+moveUnhandledToActive :: ScanStateDesc ->
+                                    PhysReg -> SState 
+                                    () () ()
+moveUnhandledToActive pre reg x =
+  case x of {
+   Build_SSInfo thisDesc0 _ ->
+    case thisDesc0 of {
+     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
+          (Build_ScanStateDesc nextInterval0 intervals0
+          fixedIntervals0 unhandled1 ((:) ((,) (Prelude.fst p) reg) active0)
+          inactive0 handled0) __))}
+        in
+        let {
+         _evar_0_0 = \_ -> Prelude.Left (ERegisterAlreadyAssigned
+          ( reg))}
+        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 :: ScanStateDesc ->
+                                  Eqtype.Equality__Coq_sort ->
+                                  Specif.Coq_sig2 ScanStateDesc
+moveActiveToHandled sd x =
+  Build_ScanStateDesc (nextInterval sd)
+    (intervals sd) (fixedIntervals sd)
+    (unhandled sd)
+    (unsafeCoerce
+      (Seq.rem
+        (Eqtype.prod_eqType
+          (Fintype.ordinal_eqType (nextInterval sd))
+          (Fintype.ordinal_eqType maxReg)) x
+        (unsafeCoerce (active sd)))) (inactive sd) ((:)
+    (unsafeCoerce x) (handled sd))
+
+moveActiveToInactive :: ScanStateDesc ->
+                                   Eqtype.Equality__Coq_sort ->
+                                   Specif.Coq_sig2 ScanStateDesc
+moveActiveToInactive sd x =
+  Build_ScanStateDesc (nextInterval sd)
+    (intervals sd) (fixedIntervals sd)
+    (unhandled sd)
+    (unsafeCoerce
+      (Seq.rem
+        (Eqtype.prod_eqType
+          (Fintype.ordinal_eqType (nextInterval sd))
+          (Fintype.ordinal_eqType maxReg)) x
+        (unsafeCoerce (active sd)))) ((:) (unsafeCoerce x)
+    (inactive sd)) (handled sd)
+
+moveInactiveToActive :: ScanStateDesc ->
+                                   Eqtype.Equality__Coq_sort ->
+                                   Specif.Coq_sig2 ScanStateDesc
+moveInactiveToActive sd x =
+  Build_ScanStateDesc (nextInterval sd)
+    (intervals sd) (fixedIntervals sd)
+    (unhandled sd) ((:) (unsafeCoerce x) (active sd))
+    (unsafeCoerce
+      (Seq.rem
+        (Eqtype.prod_eqType
+          (Fintype.ordinal_eqType (nextInterval sd))
+          (Fintype.ordinal_eqType maxReg)) x
+        (unsafeCoerce (inactive sd)))) (handled sd)
+
+moveInactiveToHandled :: ScanStateDesc ->
+                                    Eqtype.Equality__Coq_sort ->
+                                    Specif.Coq_sig2 ScanStateDesc
+moveInactiveToHandled sd x =
+  Build_ScanStateDesc (nextInterval sd)
+    (intervals sd) (fixedIntervals sd)
+    (unhandled sd) (active sd)
+    (unsafeCoerce
+      (Seq.rem
+        (Eqtype.prod_eqType
+          (Fintype.ordinal_eqType (nextInterval sd))
+          (Fintype.ordinal_eqType maxReg)) x
+        (unsafeCoerce (inactive sd)))) ((:) (unsafeCoerce x)
+    (handled sd))
+
+splitInterval :: ScanStateDesc -> IntervalId
+                            -> Interval.SplitPosition -> Prelude.Bool ->
+                            Prelude.Either SSError
+                            (Prelude.Maybe ScanStateSig)
+splitInterval sd uid pos forCurrent =
+  let {
+   _evar_0_ = \_nextInterval_ ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 ->
+    let {int = LinearScan.Utils.nth _nextInterval_ ints uid0} in
+    let {
+     _evar_0_ = \_ -> Prelude.Left (ECannotSplitSingleton ( uid0))}
+    in
+    let {
+     _evar_0_0 = \_top_assumption_ ->
+      let {
+       _evar_0_0 = \u beg us ->
+        let {
+         _evar_0_0 = \splitPos ->
+          let {
+           _evar_0_0 = \_ ->
+            (Prelude.flip (Prelude.$)) __ (\_ ->
+              let {
+               _evar_0_0 = \iv ib ie _iknd_ rds ->
+                let {
+                 _top_assumption_0 = Interval.intervalSpan rds splitPos iv ib
+                                       ie _iknd_}
+                in
+                let {
+                 _evar_0_0 = \_top_assumption_1 ->
+                  let {
+                   _evar_0_0 = \_top_assumption_2 _top_assumption_3 ->
+                    let {
+                     _evar_0_0 = \_top_assumption_4 ->
+                      let {
+                       _evar_0_0 = \_ ->
+                        let {
+                         _evar_0_0 = \_ ->
+                          let {
+                           _evar_0_0 = \_ ->
+                            (Prelude.flip (Prelude.$)) __
+                              (let {
+                                new_unhandled = Build_ScanStateDesc
+                                 ((Prelude.succ) _nextInterval_)
+                                 (LinearScan.Utils.snoc _nextInterval_
+                                   (LinearScan.Utils.set_nth _nextInterval_
+                                     ints uid0 _top_assumption_2)
+                                   _top_assumption_4) _fixedIntervals_
+                                 (Data.List.insertBy
+                                   (Data.Ord.comparing Prelude.snd) ((,)
+                                   ( _nextInterval_)
+                                   (Interval.ibeg _top_assumption_4)) ((:)
+                                   (Prelude.id ((,) u beg))
+                                   (Prelude.map Prelude.id us)))
+                                 (Prelude.map Prelude.id _active_)
+                                 (Prelude.map Prelude.id _inactive_)
+                                 (Prelude.map Prelude.id _handled_)}
+                               in
+                               \_ -> Prelude.Right (Prelude.Just
+                               (packScanState InUse
+                                 new_unhandled)))}
+                          in
+                           _evar_0_0 __}
+                        in
+                         _evar_0_0 __}
+                      in
+                      let {
+                       _evar_0_1 = \_ -> Prelude.Left
+                        (ECannotSplitSingleton ( uid0))}
+                      in
+                      case (Prelude.<=) ((Prelude.succ) beg)
+                             (Interval.ibeg _top_assumption_4) of {
+                       Prelude.True -> _evar_0_0 __;
+                       Prelude.False -> _evar_0_1 __}}
+                    in
+                    let {
+                     _evar_0_1 = \_ ->
+                      let {
+                       _evar_0_1 = Prelude.Left
+                        (ECannotSplitSingleton ( uid0))}
+                      in
+                      let {
+                       _evar_0_2 = let {
+                                    _evar_0_2 = \_ ->
+                                     let {
+                                      _evar_0_2 = \_ ->
+                                       let {
+                                        set_int_desc = Build_ScanStateDesc
+                                         _nextInterval_
+                                         (LinearScan.Utils.set_nth
+                                           _nextInterval_ ints uid0
+                                           _top_assumption_2)
+                                         _fixedIntervals_ ((:) ((,) u beg)
+                                         us) _active_ _inactive_ _handled_}
+                                       in
+                                       Prelude.Right (Prelude.Just
+                                       (packScanState
+                                         InUse set_int_desc))}
+                                     in
+                                      _evar_0_2 __}
+                                   in
+                                    _evar_0_2 __}
+                      in
+                      case forCurrent of {
+                       Prelude.True -> _evar_0_1;
+                       Prelude.False -> _evar_0_2}}
+                    in
+                    case _top_assumption_3 of {
+                     Prelude.Just x -> (\_ -> _evar_0_0 x);
+                     Prelude.Nothing -> _evar_0_1}}
+                  in
+                  let {
+                   _evar_0_1 = \_top_assumption_2 ->
+                    let {
+                     _evar_0_1 = \_top_assumption_3 ->
+                      let {
+                       _evar_0_1 = \_ ->
+                        (Prelude.flip (Prelude.$)) __
+                          (let {
+                            new_unhandled = Build_ScanStateDesc
+                             ((Prelude.succ) _nextInterval_)
+                             (LinearScan.Utils.snoc _nextInterval_ ints
+                               _top_assumption_3) _fixedIntervals_
+                             (Data.List.insertBy
+                               (Data.Ord.comparing Prelude.snd) ((,)
+                               ( _nextInterval_)
+                               (Interval.ibeg _top_assumption_3)) ((:)
+                               (Prelude.id ((,) u beg))
+                               (Prelude.map Prelude.id us)))
+                             (Prelude.map Prelude.id _active_)
+                             (Prelude.map Prelude.id _inactive_)
+                             (Prelude.map Prelude.id _handled_)}
+                           in
+                           \_ -> Prelude.Right (Prelude.Just
+                           (packScanState InUse
+                             new_unhandled)))}
+                      in
+                      let {
+                       _evar_0_2 = \_ -> Prelude.Left
+                        (ECannotSplitSingleton ( uid0))}
+                      in
+                      case (Prelude.<=) ((Prelude.succ) beg)
+                             (Interval.ibeg _top_assumption_3) of {
+                       Prelude.True -> _evar_0_1 __;
+                       Prelude.False -> _evar_0_2 __}}
+                    in
+                    let {_evar_0_2 = \_ -> Logic.coq_False_rect} in
+                    case _top_assumption_2 of {
+                     Prelude.Just x -> (\_ -> _evar_0_1 x);
+                     Prelude.Nothing -> _evar_0_2}}
+                  in
+                  case _top_assumption_1 of {
+                   Prelude.Just x -> _evar_0_0 x;
+                   Prelude.Nothing -> _evar_0_1}}
+                in
+                case _top_assumption_0 of {
+                 (,) x x0 -> _evar_0_0 x x0 __}}
+              in
+              case int of {
+               Interval.Build_IntervalDesc x x0 x1 x2 x3 ->
+                _evar_0_0 x x0 x1 x2 x3})}
+          in
+          let {
+           _evar_0_1 = \_ -> Prelude.Left (ECannotSplitSingleton
+            ( uid0))}
+          in
+          case (Prelude.&&)
+                 ((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int)))
+                   splitPos)
+                 ((Prelude.<=) ((Prelude.succ) splitPos)
+                   (Interval.iend ( int))) of {
+           Prelude.True -> _evar_0_0 __;
+           Prelude.False -> _evar_0_1 __}}
+        in
+        let {_evar_0_1 = Prelude.Right Prelude.Nothing} in
+        case Interval.splitPosition ( int) pos of {
+         Prelude.Just x -> _evar_0_0 x;
+         Prelude.Nothing -> _evar_0_1}}
+      in
+      (\us _ ->
+      case _top_assumption_ of {
+       (,) x x0 -> _evar_0_0 x x0 us})}
+    in
+    case unh of {
+     [] -> _evar_0_ __;
+     (:) x x0 -> _evar_0_0 x x0 __}}
+  in
+  case sd of {
+   Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
+    _evar_0_ x x0 x1 x2 x3 x4 x5 uid}
+
+splitCurrentInterval :: ScanStateDesc ->
+                                   Interval.SplitPosition -> SState
+                                   () () ()
+splitCurrentInterval pre pos ssi =
+  let {
+   _evar_0_ = \desc ->
+    let {
+     _evar_0_ = \_nextInterval_ intervals0 _fixedIntervals_ unhandled0 _active_ _inactive_ _handled_ ->
+      let {_evar_0_ = \_ _ _ _ _ -> Logic.coq_False_rect} in
+      let {
+       _evar_0_0 = \_top_assumption_ ->
+        let {
+         _evar_0_0 = \uid beg us ->
+          let {
+           desc0 = Build_ScanStateDesc _nextInterval_ intervals0
+            _fixedIntervals_ ((:) ((,) uid beg) us) _active_ _inactive_
+            _handled_}
+          in
+          (\_ _ _ _ ->
+          let {
+           _top_assumption_0 = splitInterval desc0 uid pos
+                                 Prelude.True}
+          in
+          let {_evar_0_0 = \err -> Prelude.Left err} in
+          let {
+           _evar_0_1 = \_top_assumption_1 ->
+            let {
+             _evar_0_1 = \_top_assumption_2 -> Prelude.Right ((,) ()
+              (Build_SSInfo _top_assumption_2 __))}
+            in
+            let {
+             _evar_0_2 = Prelude.Left (ECannotSplitSingleton
+              ( uid))}
+            in
+            case _top_assumption_1 of {
+             Prelude.Just x -> _evar_0_1 x;
+             Prelude.Nothing -> _evar_0_2}}
+          in
+          case _top_assumption_0 of {
+           Prelude.Left x -> _evar_0_0 x;
+           Prelude.Right x -> _evar_0_1 x})}
+        in
+        (\us _ ->
+        case _top_assumption_ of {
+         (,) x x0 -> _evar_0_0 x x0 us})}
+      in
+      case unhandled0 of {
+       [] -> _evar_0_ __;
+       (:) x x0 -> _evar_0_0 x x0 __}}
+    in
+    case desc of {
+     Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
+      _evar_0_ x x0 x1 x2 x3 x4 x5 __ __ __}}
+  in
+  case ssi of {
+   Build_SSInfo x x0 -> _evar_0_ x __}
+
+splitAssignedIntervalForReg :: ScanStateDesc ->
+                                          PhysReg ->
+                                          Interval.SplitPosition ->
+                                          Prelude.Bool -> SState 
+                                          () () ()
+splitAssignedIntervalForReg pre reg pos trueForActives ssi =
+  let {
+   _evar_0_ = \desc ->
+    let {
+     intlist = case trueForActives of {
+                Prelude.True -> active desc;
+                Prelude.False -> inactive desc}}
+    in
+    (Prelude.flip (Prelude.$)) __ (\_ ->
+      let {
+       intids = Prelude.map (\i -> Prelude.fst i)
+                  (Prelude.filter (\i ->
+                    Eqtype.eq_op (Fintype.ordinal_eqType maxReg)
+                      (Prelude.snd (unsafeCoerce i)) (unsafeCoerce reg))
+                    intlist)}
+      in
+      (Prelude.flip (Prelude.$)) __ (\_ ->
+        let {
+         _evar_0_ = \_nextInterval_ intervals0 _fixedIntervals_ _unhandled_ active0 inactive0 _handled_ intlist0 intids0 ->
+          let {
+           desc0 = Build_ScanStateDesc _nextInterval_ intervals0
+            _fixedIntervals_ _unhandled_ active0 inactive0 _handled_}
+          in
+          (\_ _ _ _ ->
+          let {_evar_0_ = \_ -> Prelude.Left ENoIntervalsToSplit}
+          in
+          let {
+           _evar_0_0 = \aid aids iHaids ->
+            let {
+             _top_assumption_ = splitInterval desc0 aid pos
+                                  Prelude.False}
+            in
+            let {_evar_0_0 = \err -> Prelude.Left err} in
+            let {
+             _evar_0_1 = \_top_assumption_0 ->
+              let {
+               _evar_0_1 = \_top_assumption_1 -> Prelude.Right ((,) ()
+                (let {
+                  _evar_0_1 = \_ ->
+                   (Prelude.flip (Prelude.$)) __
+                     (let {
+                       act_to_inact = Build_ScanStateDesc
+                        (nextInterval _top_assumption_1)
+                        (intervals _top_assumption_1)
+                        (fixedIntervals _top_assumption_1)
+                        (unhandled _top_assumption_1)
+                        (unsafeCoerce
+                          (Seq.rem
+                            (Eqtype.prod_eqType
+                              (Fintype.ordinal_eqType
+                                (nextInterval _top_assumption_1))
+                              (Fintype.ordinal_eqType maxReg))
+                            (unsafeCoerce ((,) ( aid) reg))
+                            (unsafeCoerce
+                              (active _top_assumption_1)))) ((:)
+                        ((,) ( aid) reg)
+                        (inactive _top_assumption_1))
+                        (handled _top_assumption_1)}
+                      in
+                      \_ -> Build_SSInfo act_to_inact __)}
+                 in
+                 let {
+                  _evar_0_2 = \_ -> Build_SSInfo _top_assumption_1
+                   __}
+                 in
+                 case Ssrbool.in_mem (unsafeCoerce ((,) ( aid) reg))
+                        (Ssrbool.mem
+                          (Seq.seq_predType
+                            (Eqtype.prod_eqType
+                              (Fintype.ordinal_eqType
+                                (nextInterval _top_assumption_1))
+                              (Fintype.ordinal_eqType maxReg)))
+                          (unsafeCoerce
+                            (active _top_assumption_1))) of {
+                  Prelude.True -> _evar_0_1 __;
+                  Prelude.False -> _evar_0_2 __}))}
+              in
+              let {
+               _evar_0_2 = Prelude.Left (ECannotSplitSingleton
+                ( aid))}
+              in
+              case _top_assumption_0 of {
+               Prelude.Just x -> _evar_0_1 x;
+               Prelude.Nothing -> _evar_0_2}}
+            in
+            case _top_assumption_ of {
+             Prelude.Left x -> _evar_0_0 x;
+             Prelude.Right x -> _evar_0_1 x}}
+          in
+          Datatypes.list_rect _evar_0_ (\aid aids iHaids _ ->
+            _evar_0_0 aid aids iHaids) intids0 __)}
+        in
+        case desc of {
+         Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
+          _evar_0_ x x0 x1 x2 x3 x4 x5 intlist intids})) __ __ __}
+  in
+  case ssi of {
+   Build_SSInfo x x0 -> _evar_0_ x __}
+
+splitActiveIntervalForReg :: ScanStateDesc ->
+                                        PhysReg -> Prelude.Int ->
+                                        SState () () ()
+splitActiveIntervalForReg pre reg pos =
+  splitAssignedIntervalForReg pre reg (Interval.BeforePos pos)
+    Prelude.True
+
+splitAnyInactiveIntervalForReg :: ScanStateDesc ->
+                                             PhysReg ->
+                                             SState () () ()
+splitAnyInactiveIntervalForReg pre reg ss =
+  (Prelude.flip (Prelude.$)) (\s ->
+    splitAssignedIntervalForReg s reg Interval.EndOfLifetimeHole
+      Prelude.False) (\_top_assumption_ ->
+    let {_top_assumption_0 = _top_assumption_ pre ss} in
+    let {_evar_0_ = \err -> Prelude.Right ((,) () ss)} in
+    let {
+     _evar_0_0 = \_top_assumption_1 ->
+      let {_evar_0_0 = \_the_1st_wildcard_ ss' -> Prelude.Right ((,) () ss')}
+      in
+      case _top_assumption_1 of {
+       (,) x x0 -> _evar_0_0 x x0}}
+    in
+    case _top_assumption_0 of {
+     Prelude.Left x -> _evar_0_ x;
+     Prelude.Right x -> _evar_0_0 x})
+
+intersectsWithFixedInterval :: ScanStateDesc ->
+                                          PhysReg ->
+                                          SState () ()
+                                          (Prelude.Maybe Prelude.Int)
+intersectsWithFixedInterval pre reg =
+  withCursor pre (\sd _ ->
+    let {int = curIntDetails sd} in
+    return_
+      (LinearScan.Utils.vfoldl' maxReg (\mx v ->
+        Lib.option_choose mx
+          (case v of {
+            Prelude.Just i -> Interval.intervalIntersectionPoint ( int) ( i);
+            Prelude.Nothing -> Prelude.Nothing})) Prelude.Nothing
+        (fixedIntervals sd)))
+
+updateRegisterPos :: Prelude.Int -> ([]
+                                (Prelude.Maybe Prelude.Int)) -> Prelude.Int
+                                -> (Prelude.Maybe Prelude.Int) -> []
+                                (Prelude.Maybe Prelude.Int)
+updateRegisterPos n v r p =
+  case p of {
+   Prelude.Just x ->
+    LinearScan.Utils.set_nth n v r (Prelude.Just
+      (case LinearScan.Utils.nth n v r of {
+        Prelude.Just n0 -> Prelude.min n0 x;
+        Prelude.Nothing -> x}));
+   Prelude.Nothing -> v}
+
+tryAllocateFreeReg :: ScanStateDesc -> SState
+                                 () ()
+                                 (Prelude.Maybe
+                                 (SState () () PhysReg))
+tryAllocateFreeReg pre =
+  withCursor pre (\sd _ ->
+    let {
+     go = \f v p ->
+      case p of {
+       (,) i r -> updateRegisterPos maxReg v r (f i)}}
+    in
+    let {
+     freeUntilPos' = Data.List.foldl' (go (\x -> Prelude.Just 0))
+                       (Data.List.replicate maxReg
+                         Prelude.Nothing) (active sd)}
+    in
+    let {
+     intersectingIntervals = Prelude.filter (\x ->
+                               Interval.intervalsIntersect
+                                 ( (curIntDetails sd))
+                                 (
+                                   (LinearScan.Utils.nth
+                                     (nextInterval sd)
+                                     (intervals sd)
+                                     (Prelude.fst x))))
+                               (inactive sd)}
+    in
+    let {
+     freeUntilPos = Data.List.foldl'
+                      (go (\i ->
+                        Interval.intervalIntersectionPoint
+                          (
+                            (LinearScan.Utils.nth
+                              (nextInterval sd)
+                              (intervals sd) i))
+                          ( (curIntDetails sd)))) freeUntilPos'
+                      intersectingIntervals}
+    in
+    case registerWithHighestPos freeUntilPos of {
+     (,) reg mres ->
+      let {
+       success = stbind (\x -> return_ reg)
+                   (moveUnhandledToActive pre reg)}
+      in
+      let {
+       maction = case mres of {
+                  Prelude.Just n ->
+                   case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce n)
+                          (unsafeCoerce 0) of {
+                    Prelude.True -> Prelude.Nothing;
+                    Prelude.False -> Prelude.Just
+                     (case (Prelude.<=) ((Prelude.succ)
+                             (Interval.intervalEnd
+                               ( (curIntDetails sd)))) n of {
+                       Prelude.True -> success;
+                       Prelude.False ->
+                        stbind (\x ->
+                          stbind (\x0 -> return_ reg)
+                            (moveUnhandledToActive pre reg))
+                          (splitCurrentInterval pre
+                            (Interval.BeforePos n))})};
+                  Prelude.Nothing -> Prelude.Just success}}
+      in
+      return_ maction})
+
+allocateBlockedReg :: ScanStateDesc -> SState
+                                 () () (Prelude.Maybe PhysReg)
+allocateBlockedReg pre =
+  withCursor pre (\sd _ ->
+    let {start = Interval.intervalStart ( (curIntDetails sd))} in
+    let {pos = curPosition sd} in
+    let {
+     go = \v p ->
+      case p of {
+       (,) i r ->
+        let {
+         atPos = \u ->
+          Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos)
+            (unsafeCoerce (Range.uloc u))}
+        in
+        let {
+         pos' = case Interval.findIntervalUsePos
+                       (Interval.getIntervalDesc
+                         (
+                           (LinearScan.Utils.nth (nextInterval sd)
+                             (intervals sd) i))) atPos of {
+                 Prelude.Just p0 -> Prelude.Just 0;
+                 Prelude.Nothing ->
+                  Interval.nextUseAfter
+                    (Interval.getIntervalDesc
+                      (
+                        (LinearScan.Utils.nth (nextInterval sd)
+                          (intervals sd) i))) start}}
+        in
+        updateRegisterPos maxReg v r pos'}}
+    in
+    let {
+     nextUsePos' = Data.List.foldl' go
+                     (Data.List.replicate maxReg Prelude.Nothing)
+                     (active sd)}
+    in
+    let {
+     intersectingIntervals = Prelude.filter (\x ->
+                               Interval.intervalsIntersect
+                                 ( (curIntDetails sd))
+                                 (
+                                   (LinearScan.Utils.nth
+                                     (nextInterval sd)
+                                     (intervals sd)
+                                     (Prelude.fst x))))
+                               (inactive sd)}
+    in
+    let {nextUsePos = Data.List.foldl' go nextUsePos' intersectingIntervals}
+    in
+    case registerWithHighestPos nextUsePos of {
+     (,) reg mres ->
+      case case mres of {
+            Prelude.Just n -> (Prelude.<=) ((Prelude.succ) n) start;
+            Prelude.Nothing -> Prelude.False} of {
+       Prelude.True ->
+        stbind (\x ->
+          stbind (\mloc ->
+            stbind (\x0 ->
+              stbind (\x1 -> return_ Prelude.Nothing)
+                (weakenHasLen_ pre))
+              (case mloc of {
+                Prelude.Just n ->
+                 splitCurrentInterval pre (Interval.BeforePos n);
+                Prelude.Nothing -> return_ ()}))
+            (intersectsWithFixedInterval pre reg))
+          (splitCurrentInterval pre
+            Interval.BeforeFirstUsePosReqReg);
+       Prelude.False ->
+        stbind (\x ->
+          stbind (\x0 ->
+            stbind (\mloc ->
+              stbind (\x1 ->
+                return_ (Prelude.Just reg))
+                (case mloc of {
+                  Prelude.Just n ->
+                   stbind (\x1 ->
+                     moveUnhandledToActive pre reg)
+                     (splitCurrentInterval pre (Interval.BeforePos
+                       n));
+                  Prelude.Nothing -> moveUnhandledToActive pre reg}))
+              (intersectsWithFixedInterval pre reg))
+            (splitActiveIntervalForReg pre reg pos))
+          (splitAnyInactiveIntervalForReg pre reg)}})
+
+morphlen_transport :: ScanStateDesc ->
+                                 ScanStateDesc ->
+                                 IntervalId -> IntervalId
+morphlen_transport b b' = GHC.Base.id
+  
+
+mt_fst :: ScanStateDesc -> ScanStateDesc ->
+                     ((,) IntervalId PhysReg) -> (,)
+                     IntervalId PhysReg
+mt_fst b b' x =
+  case x of {
+   (,) xid reg -> (,) (morphlen_transport b b' xid) reg}
+
+type Coq_int_reg_seq =
+  [] ((,) IntervalId PhysReg)
+
+type Coq_intermediate_result =
+  Specif.Coq_sig2 ScanStateDesc
+
+goActive :: Prelude.Int -> ScanStateDesc ->
+                       ScanStateDesc -> ((,) IntervalId
+                       PhysReg) -> Coq_int_reg_seq ->
+                       Coq_intermediate_result
+goActive pos sd z x xs =
+  case (Prelude.<=) ((Prelude.succ)
+         (Interval.intervalEnd
+           (
+             (LinearScan.Utils.nth (nextInterval z)
+               (intervals z) (Prelude.fst x))))) pos of {
+   Prelude.True -> moveActiveToHandled z (unsafeCoerce x);
+   Prelude.False ->
+    case Prelude.not
+           (Interval.intervalCoversPos
+             (
+               (LinearScan.Utils.nth (nextInterval z)
+                 (intervals z) (Prelude.fst x))) pos) of {
+     Prelude.True -> moveActiveToInactive z (unsafeCoerce x);
+     Prelude.False -> z}}
+
+checkActiveIntervals :: ScanStateDesc -> Prelude.Int ->
+                                   SState () () ()
+checkActiveIntervals pre pos =
+  withScanStatePO pre (\sd _ ->
+    let {
+     res = Lib.dep_foldl_inv (\s ->
+             Eqtype.prod_eqType
+               (Fintype.ordinal_eqType (nextInterval s))
+               (Fintype.ordinal_eqType maxReg)) sd
+             (unsafeCoerce (active sd))
+             (Data.List.length (active sd))
+             (unsafeCoerce active)
+             (unsafeCoerce (\x x0 _ -> mt_fst x x0))
+             (unsafeCoerce (\x _ x0 x1 _ ->
+               goActive pos sd x x0 x1))}
+    in
+    IState.iput (Build_SSInfo res __))
+
+moveInactiveToActive' :: ScanStateDesc -> ((,)
+                                    IntervalId PhysReg)
+                                    -> Coq_int_reg_seq ->
+                                    Prelude.Either SSError
+                                    (Specif.Coq_sig2 ScanStateDesc)
+moveInactiveToActive' z x xs =
+  let {
+   filtered_var = Prelude.not
+                    (Ssrbool.in_mem (Prelude.snd (unsafeCoerce x))
+                      (Ssrbool.mem
+                        (Seq.seq_predType
+                          (Fintype.ordinal_eqType maxReg))
+                        (unsafeCoerce
+                          (Prelude.map (\i -> Prelude.snd i)
+                            (active z)))))}
+  in
+  case filtered_var of {
+   Prelude.True ->
+    let {filtered_var0 = moveInactiveToActive z (unsafeCoerce x)}
+    in
+    Prelude.Right filtered_var0;
+   Prelude.False -> Prelude.Left (ERegisterAssignmentsOverlap
+    ( (Prelude.snd x)))}
+
+goInactive :: Prelude.Int -> ScanStateDesc ->
+                         ScanStateDesc -> ((,) IntervalId
+                         PhysReg) -> Coq_int_reg_seq ->
+                         Prelude.Either SSError
+                         Coq_intermediate_result
+goInactive pos sd z x xs =
+  let {f = \sd' -> Prelude.Right sd'} in
+  case (Prelude.<=) ((Prelude.succ)
+         (Interval.intervalEnd
+           (
+             (LinearScan.Utils.nth (nextInterval z)
+               (intervals z) (Prelude.fst x))))) pos of {
+   Prelude.True ->
+    let {filtered_var = moveInactiveToHandled z (unsafeCoerce x)}
+    in
+    f filtered_var;
+   Prelude.False ->
+    case Interval.intervalCoversPos
+           (
+             (LinearScan.Utils.nth (nextInterval z)
+               (intervals z) (Prelude.fst x))) pos of {
+     Prelude.True ->
+      let {filtered_var = moveInactiveToActive' z x xs} in
+      case filtered_var of {
+       Prelude.Left err -> Prelude.Left err;
+       Prelude.Right s -> f s};
+     Prelude.False -> f z}}
+
+checkInactiveIntervals :: ScanStateDesc -> Prelude.Int
+                                     -> SState () () ()
+checkInactiveIntervals pre pos =
+  withScanStatePO pre (\sd _ ->
+    let {
+     eres = Lib.dep_foldl_invE (\s ->
+              Eqtype.prod_eqType
+                (Fintype.ordinal_eqType (nextInterval s))
+                (Fintype.ordinal_eqType maxReg)) sd
+              (unsafeCoerce (inactive sd))
+              (Data.List.length (inactive sd))
+              (unsafeCoerce inactive)
+              (unsafeCoerce (\x x0 _ -> mt_fst x x0))
+              (unsafeCoerce (\x _ x0 x1 _ ->
+                goInactive pos sd x x0 x1))}
+    in
+    case eres of {
+     Prelude.Left err -> IState.ierr err;
+     Prelude.Right s -> IState.iput (Build_SSInfo s __)})
+
+handleInterval :: ScanStateDesc -> SState 
+                             () () (Prelude.Maybe PhysReg)
+handleInterval pre =
+  withCursor pre (\sd _ ->
+    let {position = curPosition sd} in
+    stbind (\x ->
+      stbind (\x0 ->
+        stbind (\mres ->
+          case mres of {
+           Prelude.Just x1 -> IState.imap (\x2 -> Prelude.Just x2) x1;
+           Prelude.Nothing -> allocateBlockedReg pre})
+          (tryAllocateFreeReg pre))
+        (liftLen pre (\sd0 ->
+          checkInactiveIntervals sd0 position)))
+      (liftLen pre (\sd0 ->
+        checkActiveIntervals sd0 position)))
+
+walkIntervals :: ScanStateDesc -> Prelude.Int ->
+                            Prelude.Either SSError
+                            ScanStateSig
+walkIntervals sd positions =
+  (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
+    (\_ -> Prelude.Left
+    EFuelExhausted)
+    (\n ->
+    let {
+     go = let {
+           go count0 ss =
+             (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
+               (\_ -> Prelude.Right (Build_SSInfo
+               (thisDesc sd ss)
+               __))
+               (\cnt ->
+               case handleInterval sd ss of {
+                Prelude.Left err -> Prelude.Left err;
+                Prelude.Right p ->
+                 case p of {
+                  (,) o ss' ->
+                   case strengthenHasLen sd
+                          (thisDesc sd ss') of {
+                    Prelude.Just _ ->
+                     go cnt (Build_SSInfo
+                       (thisDesc sd ss') __);
+                    Prelude.Nothing ->
+                     (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
+                       (\_ -> Prelude.Right
+                       ss')
+                       (\n0 -> Prelude.Left
+                       EUnexpectedNoMoreUnhandled)
+                       cnt}}})
+               count0}
+          in go}
+    in
+    case LinearScan.Utils.uncons (unhandled sd) of {
+     Prelude.Just s ->
+      case s of {
+       (,) x s0 ->
+        case x of {
+         (,) i pos ->
+          case go
+                 (Seq.count (\x0 ->
+                   Eqtype.eq_op Ssrnat.nat_eqType
+                     (Prelude.snd (unsafeCoerce x0)) (unsafeCoerce pos))
+                   (unhandled sd)) (Build_SSInfo sd __) of {
+           Prelude.Left err -> Prelude.Left err;
+           Prelude.Right ss ->
+            walkIntervals (thisDesc sd ss) n}}};
+     Prelude.Nothing -> Prelude.Right
+      (packScanState InUse sd)})
+    positions
+
+linearScan :: (BlockInfo a2 a3 a4 a5) -> (OpInfo 
+              a1 a4 a5 a6) -> (VarInfo a6) -> ([] a2) -> a1 ->
+              Prelude.Either SSError ((,) ([] a3) a1)
+linearScan binfo oinfo vinfo blocks accum =
+  let {blocks' = computeBlockOrder blocks} in
+  let {liveSets = computeLocalLiveSets vinfo oinfo binfo blocks'}
+  in
+  let {liveSets' = computeGlobalLiveSets binfo blocks' liveSets}
+  in
+  let {ssig = buildIntervals vinfo oinfo binfo blocks} in
+  case walkIntervals ( ssig) ((Prelude.succ)
+         (countOps binfo blocks)) of {
+   Prelude.Left err -> Prelude.Left err;
+   Prelude.Right ssig' ->
+    let {
+     mappings = resolveDataFlow binfo ( ssig') blocks liveSets'}
+    in
+    Prelude.Right
+    (assignRegNum vinfo oinfo binfo ( ssig') mappings blocks
+      accum)}
 
diff --git a/LinearScan/NonEmpty0.hs b/LinearScan/NonEmpty0.hs
--- a/LinearScan/NonEmpty0.hs
+++ b/LinearScan/NonEmpty0.hs
@@ -2,23 +2,10 @@
 
 
 import qualified Prelude
+import qualified Data.IntMap
 import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
-
-coq_NE_mapAccumL :: (a1 -> a2 -> (,) a1 a3) -> a1 -> ([] a2) -> (,) a1
-                    ([] a3)
-coq_NE_mapAccumL f s v =
-  (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
-    (\x ->
-    case f s x of {
-     (,) s' y -> (,) s' ((:[]) y)})
-    (\x xs ->
-    case f s x of {
-     (,) s' y ->
-      case coq_NE_mapAccumL f s' xs of {
-       (,) s'' ys -> (,) s'' ((:) y ys)}})
-    v
 
diff --git a/LinearScan/Range.hs b/LinearScan/Range.hs
--- a/LinearScan/Range.hs
+++ b/LinearScan/Range.hs
@@ -2,14 +2,13 @@
 
 
 import qualified Prelude
+import qualified Data.IntMap
 import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
-import qualified LinearScan.Lib as Lib
 
-
 __ :: any
 __ = Prelude.error "Logical or arity value used"
 
@@ -29,20 +28,20 @@
 type UsePosSublistsOf =
   ((,) (Prelude.Maybe ([] UsePos)) (Prelude.Maybe ([] UsePos)))
 
-usePosSpan :: (UsePos -> Prelude.Bool) -> ([] UsePos) -> UsePosSublistsOf
-usePosSpan f l =
+usePosSpan :: Prelude.Int -> ([] UsePos) -> UsePosSublistsOf
+usePosSpan before l =
   (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
     (\x ->
-    let {b = f x} in
+    let {b = (Prelude.<=) ((Prelude.succ) (uloc x)) before} in
     case b of {
      Prelude.True -> (,) (Prelude.Just ((:[]) x)) Prelude.Nothing;
      Prelude.False -> (,) Prelude.Nothing (Prelude.Just ((:[]) x))})
     (\x xs ->
-    let {b = f x} in
+    let {b = (Prelude.<=) ((Prelude.succ) (uloc x)) before} in
     case b of {
      Prelude.True ->
-      let {u = usePosSpan f xs} in
-      case u of {
+      let {u = \_ -> usePosSpan before xs} in
+      case u __ of {
        (,) o x0 ->
         case o of {
          Prelude.Just l1 ->
@@ -103,28 +102,54 @@
        xs}
   in go (ups r)
 
-makeDividedRange :: (UsePos -> Prelude.Bool) -> RangeDesc -> ([] UsePos) ->
-                    ([] UsePos) ->
+makeDividedRange :: RangeDesc -> Prelude.Int -> ([] UsePos) -> ([] UsePos) ->
                     ((,) (Prelude.Maybe RangeDesc) (Prelude.Maybe RangeDesc))
-makeDividedRange f rd l1 l2 =
+makeDividedRange rd before l1 l2 =
   case rd of {
    Build_RangeDesc rbeg0 rend0 ups0 ->
-     (\_ -> (,) (Prelude.Just (Build_RangeDesc rbeg0 ((Prelude.succ)
-      (uloc (Prelude.last l1))) l1)) (Prelude.Just (Build_RangeDesc
-      (uloc (Prelude.head l2)) rend0 l2))) __}
+     (\_ -> (,) (Prelude.Just (Build_RangeDesc rbeg0 before l1))
+      (Prelude.Just (Build_RangeDesc (uloc (Prelude.head l2)) rend0 l2))) __}
 
-rangeSpan :: (UsePos -> Prelude.Bool) -> RangeDesc ->
+rangeSpan :: Prelude.Int -> RangeDesc ->
              ((,) (Prelude.Maybe RangeDesc) (Prelude.Maybe RangeDesc))
-rangeSpan f rd =
-  case usePosSpan f (ups rd) of {
-   (,) o o0 ->
-    case o of {
-     Prelude.Just l1 ->
-      case o0 of {
-       Prelude.Just l2 -> makeDividedRange f rd l1 l2;
-       Prelude.Nothing -> (,) (Prelude.Just rd) Prelude.Nothing};
-     Prelude.Nothing ->
-      case o0 of {
-       Prelude.Just n -> (,) Prelude.Nothing (Prelude.Just rd);
-       Prelude.Nothing -> Lib.ex_falso_quodlibet}}}
+rangeSpan before rd =
+  let {_top_assumption_ = usePosSpan before (ups rd)} in
+  let {
+   _evar_0_ = \_top_assumption_0 ->
+    let {
+     _evar_0_ = \o1 _top_assumption_1 ->
+      let {_evar_0_ = \o2 -> makeDividedRange rd before o1 o2} in
+      let {
+       _evar_0_0 = \_ ->
+        let {
+         rd' = Build_RangeDesc (rbeg rd) (Prelude.min before (rend rd))
+          (ups rd)}
+        in
+        (,) (Prelude.Just rd') Prelude.Nothing}
+      in
+      case _top_assumption_1 of {
+       Prelude.Just x -> (\_ -> _evar_0_ x);
+       Prelude.Nothing -> _evar_0_0}}
+    in
+    let {
+     _evar_0_0 = \_top_assumption_1 ->
+      let {
+       _evar_0_0 = \o2 ->
+        let {
+         rd' = Build_RangeDesc (Prelude.max before (rbeg rd)) (rend rd)
+          (ups rd)}
+        in
+        (,) Prelude.Nothing (Prelude.Just rd')}
+      in
+      let {_evar_0_1 = \_ -> Prelude.error "absurd case"} in
+      case _top_assumption_1 of {
+       Prelude.Just x -> (\_ -> _evar_0_0 x);
+       Prelude.Nothing -> _evar_0_1}}
+    in
+    case _top_assumption_0 of {
+     Prelude.Just x -> _evar_0_ x;
+     Prelude.Nothing -> _evar_0_0}}
+  in
+  case _top_assumption_ of {
+   (,) x x0 -> _evar_0_ x x0 __}
 
diff --git a/LinearScan/Seq.hs b/LinearScan/Seq.hs
--- a/LinearScan/Seq.hs
+++ b/LinearScan/Seq.hs
@@ -5,6 +5,7 @@
 
 
 import qualified Prelude
+import qualified Data.IntMap
 import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Functor.Identity
@@ -34,12 +35,24 @@
 nseq n x =
   ncons n x []
 
+last :: a1 -> ([] a1) -> a1
+last x s =
+  case s of {
+   [] -> x;
+   (:) x' s' -> last x' s'}
+
+belast :: a1 -> ([] a1) -> [] a1
+belast x s =
+  case s of {
+   [] -> [];
+   (:) x' s' -> (:) x (belast x' s')}
+
 nth :: a1 -> ([] a1) -> Prelude.Int -> a1
 nth x0 s n =
   case s of {
    [] -> x0;
    (:) x s' ->
-    (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
+    (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
       (\_ ->
       x)
       (\n' ->
@@ -51,13 +64,19 @@
   case s of {
    [] -> ncons n x0 ((:) y []);
    (:) x s' ->
-    (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
+    (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
       (\_ -> (:) y
       s')
       (\n' -> (:) x
       (set_nth x0 s' n' y))
       n}
 
+count :: (Ssrbool.Coq_pred a1) -> ([] a1) -> Prelude.Int
+count a s =
+  case s of {
+   [] -> 0;
+   (:) x s' -> (Prelude.+) (Ssrnat.nat_of_bool (a x)) (count a s')}
+
 catrev :: ([] a1) -> ([] a1) -> [] a1
 catrev s1 s2 =
   case s1 of {
@@ -87,6 +106,16 @@
                 Eqtype.Equality__Coq_sort
 seq_predType t =
   Ssrbool.mkPredType (unsafeCoerce (pred_of_eq_seq t))
+
+undup :: Eqtype.Equality__Coq_type -> ([] Eqtype.Equality__Coq_sort) -> []
+         Eqtype.Equality__Coq_sort
+undup t s =
+  case s of {
+   [] -> [];
+   (:) x s' ->
+    case Ssrbool.in_mem x (Ssrbool.mem (seq_predType t) (unsafeCoerce s')) of {
+     Prelude.True -> undup t s';
+     Prelude.False -> (:) x (undup t s')}}
 
 rem :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> ([]
        Eqtype.Equality__Coq_sort) -> [] Eqtype.Equality__Coq_sort
diff --git a/LinearScan/Specif.hs b/LinearScan/Specif.hs
--- a/LinearScan/Specif.hs
+++ b/LinearScan/Specif.hs
@@ -2,6 +2,7 @@
 
 
 import qualified Prelude
+import qualified Data.IntMap
 import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Functor.Identity
diff --git a/LinearScan/Ssrbool.hs b/LinearScan/Ssrbool.hs
--- a/LinearScan/Ssrbool.hs
+++ b/LinearScan/Ssrbool.hs
@@ -5,6 +5,7 @@
 
 
 import qualified Prelude
+import qualified Data.IntMap
 import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Functor.Identity
diff --git a/LinearScan/Ssrfun.hs b/LinearScan/Ssrfun.hs
--- a/LinearScan/Ssrfun.hs
+++ b/LinearScan/Ssrfun.hs
@@ -2,6 +2,7 @@
 
 
 import qualified Prelude
+import qualified Data.IntMap
 import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Functor.Identity
diff --git a/LinearScan/Ssrnat.hs b/LinearScan/Ssrnat.hs
--- a/LinearScan/Ssrnat.hs
+++ b/LinearScan/Ssrnat.hs
@@ -5,6 +5,7 @@
 
 
 import qualified Prelude
+import qualified Data.IntMap
 import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Functor.Identity
@@ -39,16 +40,22 @@
 
 iter :: Prelude.Int -> (a1 -> a1) -> a1 -> a1
 iter n f x =
-  (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
+  (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
     (\_ ->
     x)
     (\i ->
     f (iter i f x))
     n
 
+nat_of_bool :: Prelude.Bool -> Prelude.Int
+nat_of_bool b =
+  case b of {
+   Prelude.True -> (Prelude.succ) 0;
+   Prelude.False -> 0}
+
 double_rec :: Prelude.Int -> Prelude.Int
 double_rec n =
-  (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
+  (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
     (\_ ->
     0)
     (\n' -> (Prelude.succ) ((Prelude.succ)
diff --git a/LinearScan/State.hs b/LinearScan/State.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/State.hs
@@ -0,0 +1,80 @@
+module LinearScan.State where
+
+
+import qualified Prelude
+import qualified Data.IntMap
+import qualified Data.List
+import qualified Data.Ord
+import qualified Data.Functor.Identity
+import qualified LinearScan.Utils
+
+
+type State s a = s -> (,) a s
+
+get :: State a1 a1
+get i =
+  (,) i i
+
+put :: a1 -> State a1 ()
+put x x0 =
+  (,) () x
+
+modify :: (a1 -> a1) -> State a1 ()
+modify f i =
+  (,) () (f i)
+
+join :: (State a1 (State a1 a2)) -> State a1 a2
+join x st =
+  case x st of {
+   (,) y st' -> y st'}
+
+fmap :: (a2 -> a3) -> (State a1 a2) -> State a1 a3
+fmap f x st =
+  case x st of {
+   (,) a st' -> (,) (f a) st'}
+
+bind :: (a2 -> State a1 a3) -> (State a1 a2) -> State a1 a3
+bind f x =
+  join (fmap f x)
+
+pure :: a2 -> State a1 a2
+pure x st =
+  (,) x st
+
+ap :: (State a1 (a2 -> a3)) -> (State a1 a2) -> State a1 a3
+ap f x st =
+  case f st of {
+   (,) f' st' ->
+    case x st' of {
+     (,) x' st'' -> (,) (f' x') st''}}
+
+liftA2 :: (a2 -> a3 -> a4) -> (State a1 a2) -> (State a1 a3) -> State a1 a4
+liftA2 f x y =
+  ap (fmap f x) y
+
+mapM :: (a2 -> State a1 a3) -> ([] a2) -> State a1 ([] a3)
+mapM f l =
+  case l of {
+   [] -> pure [];
+   (:) x xs -> liftA2 (\x0 x1 -> (:) x0 x1) (f x) (mapM f xs)}
+
+foldM :: (a2 -> a3 -> State a1 a2) -> a2 -> ([] a3) -> State a1 a2
+foldM f s l =
+  case l of {
+   [] -> pure s;
+   (:) y ys -> bind (\x -> foldM f x ys) (f s y)}
+
+forFoldM :: a2 -> ([] a3) -> (a2 -> a3 -> State a1 a2) -> State a1 a2
+forFoldM s l f =
+  foldM f s l
+
+concat :: ([] ([] a1)) -> [] a1
+concat l =
+  case l of {
+   [] -> [];
+   (:) x xs -> (Prelude.++) x (concat xs)}
+
+concatMapM :: (a2 -> State a1 ([] a3)) -> ([] a2) -> State a1 ([] a3)
+concatMapM f l =
+  fmap concat (mapM f l)
+
diff --git a/LinearScan/Utils.hs b/LinearScan/Utils.hs
--- a/LinearScan/Utils.hs
+++ b/LinearScan/Utils.hs
@@ -1,6 +1,10 @@
 module LinearScan.Utils where
 
+import Data.Char
 import Data.List
+import Debug.Trace
+
+trace = Debug.Trace.trace . map chr
 
 boundedTransport' pos n _top_assumption_ = _top_assumption_
 
diff --git a/LinearScan/Vector0.hs b/LinearScan/Vector0.hs
--- a/LinearScan/Vector0.hs
+++ b/LinearScan/Vector0.hs
@@ -5,6 +5,7 @@
 
 
 import qualified Prelude
+import qualified Data.IntMap
 import qualified Data.List
 import qualified Data.Ord
 import qualified Data.Functor.Identity
diff --git a/linearscan.cabal b/linearscan.cabal
--- a/linearscan.cabal
+++ b/linearscan.cabal
@@ -1,5 +1,5 @@
 name:          linearscan
-version:       0.1.0.0
+version:       0.2.0.0
 synopsis:      Linear scan register allocator, formally verified in Coq
 homepage:      http://github.com/jwiegley/linearscan
 license:       BSD3
@@ -41,11 +41,7 @@
   .
   This library's sole entry point is the 'LinearScan.allocate' function, which
   takes a list of information about basic blocks to an equivalent list, with
-  annotations indicating allocation choices.  In order to use this function
-  you must first convert from your own basic block representation to that of
-  the @BlockInfo@, @OpInfo@ and @VarInfo@ structures used by this library.
-  For example of such a transformation from a Hoopl Graph, see the file
-  @Tempest.hs@ in the tests directory.
+  annotations indicating allocation choices.
 
 library
   default-language: Haskell2010
@@ -53,10 +49,8 @@
     LinearScan
   other-modules:
     LinearScan.Datatypes
-    LinearScan.IApplicative
-    LinearScan.IEndo
-    LinearScan.IMonad
     LinearScan.IState
+    LinearScan.State
     LinearScan.Interval
     LinearScan.Lib
     -- LinearScan.List0
@@ -75,8 +69,10 @@
     -- LinearScan.Ssreflect
     LinearScan.Ssrfun
     LinearScan.Ssrnat
+  cpp-options:      -DMAX_REG=4 -DREG_SIZE=8
   ghc-options:      -fno-warn-deprecated-flags
   build-depends:    base >=4.7 && <4.8
+                  , containers
                   , transformers
 
 test-suite test
@@ -91,7 +87,8 @@
       , HUnit              >= 1.2.5
       , hspec              >= 1.4.4
       , hspec-expectations >= 0.3
-      , hoopl              >= 3.10
       , containers         >= 0.5.5
       , transformers       >= 0.3.0.0
+      , hoopl              >= 3.10.0.1
+      , lens               >= 4.2
       , free
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -16,203 +16,242 @@
 
 main :: IO ()
 main = hspec $ do
-  let basicAlloc = op $ alloc 0 2 >> alloc 1 1 >> alloc 2 0
-
   describe "Sanity tests" $ do
     it "Single instruction" $ asmTest
-        (add v0 v1 v2)
+        (label "entry"
+            (add v0 v1 v2)
+            return_) $
 
-        (block basicAlloc)
+        label "entry"
+            (add r2 r1 r0)
+            return_
 
     it "Single, repeated instruction" $ asmTest
-        (do add v0 v1 v2
-            add v0 v1 v2
-            add v0 v1 v2) $
+        (label "entry"
+            (do add v0 v1 v2
+                add v0 v1 v2
+                add v0 v1 v2)
+            return_) $
 
-        block $ do
-            basicAlloc
-            basicAlloc
-            basicAlloc
+        label "entry"
+            (do add r2 r1 r0
+                add r2 r1 r0
+                add r2 r1 r0)
+            return_
 
     it "Multiple instructions" $ asmTest
-        (do add v0 v1 v2
-            add v0 v1 v3
-            add v0 v1 v2) $
+        (label "entry"
+            (do add v0 v1 v2
+                add v0 v1 v3
+                add v0 v1 v2)
+            return_) $
 
-        block $ do
-            basicAlloc
-            op $ alloc 0 2 >> alloc 1 1 >> alloc 3 3
-            basicAlloc
+        label "entry"
+            (do add r2 r1 r0
+                add r2 r1 r3
+                add r2 r1 r0)
+            return_
 
     it "More variables used than registers" $ asmTest
-        (do add v0 v1 v2
-            add v3 v4 v5
-            add v6 v7 v8
-            add v9 v10 v11
-            add v12 v13 v14
-            add v15 v16 v17
-            add v18 v19 v20
-            add v21 v22 v23
-            add v24 v25 v26
-            add v27 v28 v29
-            add v30 v31 v32
-            add v33 v34 v35) $
+        (label "entry"
+            (do add v0 v1 v2
+                add v3 v4 v5
+                add v6 v7 v8
+                add v9 v10 v11
+                add v12 v13 v14
+                add v15 v16 v17
+                add v18 v19 v20
+                add v21 v22 v23
+                add v24 v25 v26
+                add v27 v28 v29
+                add v30 v31 v32
+                add v33 v34 v35)
+            return_) $
 
-        block $ do
-            op $ alloc  0 2 >> alloc  1 1 >> alloc  2 0
-            op $ alloc  3 2 >> alloc  4 1 >> alloc  5 0
-            op $ alloc  6 2 >> alloc  7 1 >> alloc  8 0
-            op $ alloc  9 2 >> alloc 10 1 >> alloc 11 0
-            op $ alloc 12 2 >> alloc 13 1 >> alloc 14 0
-            op $ alloc 15 2 >> alloc 16 1 >> alloc 17 0
-            op $ alloc 18 2 >> alloc 19 1 >> alloc 20 0
-            op $ alloc 21 2 >> alloc 22 1 >> alloc 23 0
-            op $ alloc 24 2 >> alloc 25 1 >> alloc 26 0
-            op $ alloc 27 2 >> alloc 28 1 >> alloc 29 0
-            op $ alloc 30 2 >> alloc 31 1 >> alloc 32 0
-            op $ alloc 33 2 >> alloc 34 1 >> alloc 35 0
+        label "entry"
+            (do add r2 r1 r0
+                add r2 r1 r0
+                add r2 r1 r0
+                add r2 r1 r0
+                add r2 r1 r0
+                add r2 r1 r0
+                add r2 r1 r0
+                add r2 r1 r0
+                add r2 r1 r0
+                add r2 r1 r0
+                add r2 r1 r0
+                add r2 r1 r0)
+            return_
 
-    it "Single long-lived variable" $ asmTest
-        (do add v0 v1 v2
-            add v0 v4 v5
-            add v0 v7 v8
-            add v0 v10 v11) $
+    it "Single rong-lived variable" $ asmTest
+        (label "entry"
+            (do add v0 v1 v2
+                add v0 v4 v5
+                add v0 v7 v8
+                add v0 v10 v11)
+            return_) $
 
-        block $ do
-            op $ alloc  0 2 >> alloc  1 1 >> alloc  2 0
-            op $ alloc  0 2 >> alloc  4 1 >> alloc  5 0
-            op $ alloc  0 2 >> alloc  7 1 >> alloc  8 0
-            op $ alloc  0 2 >> alloc 10 1 >> alloc 11 0
+        label "entry"
+            (do add r2 r1 r0
+                add r2 r1 r0
+                add r2 r1 r0
+                add r2 r1 r0)
+            return_
 
-    it "Two long-lived variables" $ asmTest
-        (do add v0 v1 v2
-            add v0 v4 v5
-            add v0 v4 v8
-            add v0 v4 v11) $
+    it "Two rong-lived variables" $ asmTest
+        (label "entry"
+            (do add v0 v1 v2
+                add v0 v4 v5
+                add v0 v4 v8
+                add v0 v4 v11)
+            return_) $
 
-        block $ do
-            op $ alloc  0 2 >> alloc  1 1 >> alloc  2 0
-            op $ alloc  0 2 >> alloc  4 1 >> alloc  5 0
-            op $ alloc  0 2 >> alloc  4 1 >> alloc  8 0
-            op $ alloc  0 2 >> alloc  4 1 >> alloc 11 0
+        label "entry"
+            (do add r2 r1 r0
+                add r2 r1 r0
+                add r2 r1 r0
+                add r2 r1 r0)
+            return_
 
-    it "One variable with a long interval" $ asmTest
-        (do add v0   v1  v2
-            add v3   v4  v5
-            add v6   v7  v8
-            add v9  v10 v11
-            add v12 v13 v14
-            add v15 v16 v17
-            add v18 v19 v20
-            add v21 v22 v23
-            add v24 v25 v26
-            add v27 v28 v29
-            add v30 v31 v32
-            add v0  v34 v35) $
+    it "One variable with a rong interval" $ asmTest
+        (label "entry"
+            (do add v0   v1  v2
+                add v3   v4  v5
+                add v6   v7  v8
+                add v9  v10 v11
+                add v12 v13 v14
+                add v15 v16 v17
+                add v18 v19 v20
+                add v21 v22 v23
+                add v24 v25 v26
+                add v27 v28 v29
+                add v30 v31 v32
+                add v0  v34 v35)
+            return_) $
 
-        block $ do
-            op $ alloc  0 2 >> alloc  1 1 >> alloc  2 0
-            op $ alloc  3 3 >> alloc  4 1 >> alloc  5 0
-            op $ alloc  6 3 >> alloc  7 1 >> alloc  8 0
-            op $ alloc  9 3 >> alloc 10 1 >> alloc 11 0
-            op $ alloc 12 3 >> alloc 13 1 >> alloc 14 0
-            op $ alloc 15 3 >> alloc 16 1 >> alloc 17 0
-            op $ alloc 18 3 >> alloc 19 1 >> alloc 20 0
-            op $ alloc 21 3 >> alloc 22 1 >> alloc 23 0
-            op $ alloc 24 3 >> alloc 25 1 >> alloc 26 0
-            op $ alloc 27 3 >> alloc 28 1 >> alloc 29 0
-            op $ alloc 30 3 >> alloc 31 1 >> alloc 32 0
-            op $ alloc  0 2 >> alloc 34 1 >> alloc 35 0
+        label "entry"
+            (do add r2 r1 r0
+                add r3 r1 r0
+                add r3 r1 r0
+                add r3 r1 r0
+                add r3 r1 r0
+                add r3 r1 r0
+                add r3 r1 r0
+                add r3 r1 r0
+                add r3 r1 r0
+                add r3 r1 r0
+                add r3 r1 r0
+                add r2 r1 r0)
+            return_
 
-    it "Many variables with long intervals" $ asmTest
-        (do add v0   v1  v2
-            add v3   v4  v5
-            add v6   v7  v8
-            add v9  v10 v11
-            add v12 v13 v14
-            add v15 v16 v17
-            add v18 v19 v20
-            add v21 v22 v23
-            add v24 v25 v26
-            add v27 v28 v29
-            add v0   v1  v2
-            add v3   v4  v5
-            add v6   v7  v8
-            add v9  v10 v11
-            add v12 v13 v14
-            add v15 v16 v17
-            add v18 v19 v20
-            add v21 v22 v23
-            add v24 v25 v26
-            add v27 v28 v29
-        ) $
+    it "Many variables with rong intervals" $ asmTest
+        (label "entry"
+            (do add v0   v1  v2
+                add v3   v4  v5
+                add v6   v7  v8
+                add v9  v10 v11
+                add v12 v13 v14
+                add v15 v16 v17
+                add v18 v19 v20
+                add v21 v22 v23
+                add v24 v25 v26
+                add v27 v28 v29
+                add v0   v1  v2
+                add v3   v4  v5
+                add v6   v7  v8
+                add v9  v10 v11
+                add v12 v13 v14
+                add v15 v16 v17
+                add v18 v19 v20
+                add v21 v22 v23
+                add v24 v25 v26
+                add v27 v28 v29)
+            return_) $
 
-        block $ do
-            op $ alloc  0  2 >> alloc  1  1 >> alloc  2  0
-            op $ alloc  3  5 >> alloc  4  4 >> alloc  5  3
-            op $ alloc  6  8 >> alloc  7  7 >> alloc  8  6
-            op $ alloc  9 11 >> alloc 10 10 >> alloc 11  9
-            op $ alloc 12 14 >> alloc 13 13 >> alloc 14 12
-            op $ alloc 15 17 >> alloc 16 16 >> alloc 17 15
-            op $ alloc 18 20 >> alloc 19 19 >> alloc 20 18
-            op $ alloc 21 23 >> alloc 22 22 >> alloc 23 21
-            op $ alloc 24 26 >> alloc 25 25 >> alloc 26 24
-            op $ alloc 27 29 >> alloc 28 28 >> alloc 29 27
-            op $ alloc  0  2 >> alloc  1  1 >> alloc  2  0
-            op $ alloc  3  5 >> alloc  4  4 >> alloc  5  3
-            op $ alloc  6  8 >> alloc  7  7 >> alloc  8  6
-            op $ alloc  9 11 >> alloc 10 10 >> alloc 11  9
-            op $ alloc 12 14 >> alloc 13 13 >> alloc 14 12
-            op $ alloc 15 17 >> alloc 16 16 >> alloc 17 15
-            op $ alloc 18 20 >> alloc 19 19 >> alloc 20 18
-            op $ alloc 21 23 >> alloc 22 22 >> alloc 23 21
-            op $ alloc 24 26 >> alloc 25 25 >> alloc 26 24
-            op $ alloc 27 29 >> alloc 28 28 >> alloc 29 27
+        label "entry"
+            (do add r2 r1 r0
+                add r5 r4 r3
+                add r8 r7 r6
+                add r11 r10 r9
+                add r14 r13 r12
+                add r17 r16 r15
+                add r20 r19 r18
+                add r23 r22 r21
+                add r26 r25 r24
+                add r29 r28 r27
+                add r2 r1 r0
+                add r5 r4 r3
+                add r8 r7 r6
+                add r11 r10 r9
+                add r14 r13 r12
+                add r17 r16 r15
+                add r20 r19 r18
+                add r23 r22 r21
+                add r26 r25 r24
+                add r29 r28 r27)
+            return_
 
     it "Spilling one variable" $ asmTest
-        (do {-  1 -} add v0   v1  v2
-            {-  3 -} add v3   v4  v5
-            {-  5 -} add v6   v7  v8
-            {-  7 -} add v9  v10 v11
-            {-  9 -} add v12 v13 v14
-            {- 11 -} add v15 v16 v17
-            {- 13 -} add v18 v19 v20
-            {- 15 -} add v21 v22 v23
-            {- 17 -} add v24 v25 v26
-            {- 19 -} add v27 v28 v29
-            {- 21 -} add v30 v31 v32
-            {- 23 -} add v0   v1  v2
-            {- 25 -} add v3   v4  v5
-            {- 27 -} add v6   v7  v8
-            {- 29 -} add v9  v10 v11
-            {- 31 -} add v12 v13 v14
-            {- 33 -} add v15 v16 v17
-            {- 35 -} add v18 v19 v20
-            {- 37 -} add v21 v22 v23
-            {- 39 -} add v24 v25 v26
-            {- 41 -} add v27 v28 v29
-            {- 43 -} add v30 v31 v32) $
+        (label "entry"
+            (do {-  1 -} add v0   v1  v2
+                {-  3 -} add v3   v4  v5
+                {-  5 -} add v6   v7  v8
+                {-  7 -} add v9  v10 v11
+                {-  9 -} add v12 v13 v14
+                {- 11 -} add v15 v16 v17
+                {- 13 -} add v18 v19 v20
+                {- 15 -} add v21 v22 v23
+                {- 17 -} add v24 v25 v26
+                {- 19 -} add v27 v28 v29
+                {- 21 -} add v30 v31 v32
+                {- 23 -} add v0   v1  v2
+                {- 25 -} add v3   v4  v5
+                {- 27 -} add v6   v7  v8
+                {- 29 -} add v9  v10 v11
+                {- 31 -} add v12 v13 v14
+                {- 33 -} add v15 v16 v17
+                {- 35 -} add v18 v19 v20
+                {- 37 -} add v21 v22 v23
+                {- 39 -} add v24 v25 v26
+                {- 41 -} add v27 v28 v29
+                {- 43 -} add v30 v31 v32)
+            return_) $
 
-        block $ do
-            op $ alloc  0  2 >> alloc  1  1 >> alloc  2  0
-            op $ alloc  3  5 >> alloc  4  4 >> alloc  5  3
-            op $ alloc  6  8 >> alloc  7  7 >> alloc  8  6
-            op $ alloc  9 11 >> alloc 10 10 >> alloc 11  9
-            op $ alloc 12 14 >> alloc 13 13 >> alloc 14 12
-            op $ alloc 15 17 >> alloc 16 16 >> alloc 17 15
-            op $ alloc 18 20 >> alloc 19 19 >> alloc 20 18
-            op $ alloc 21 23 >> alloc 22 22 >> alloc 23 21
-            op $ alloc 24 26 >> alloc 25 25 >> alloc 26 24
-            op $ alloc 27 29 >> alloc 28 28 >> alloc 29 27
-            op $ alloc 30 27 >> alloc 31 31 >> alloc 32 30
-            op $ alloc  0  2 >> alloc  1  1 >> alloc  2  0
-            op $ alloc  3  5 >> alloc  4  4 >> alloc  5  3
-            op $ alloc  6  8 >> alloc  7  7 >> alloc  8  6
-            op $ alloc  9 11 >> alloc 10 10 >> alloc 11  9
-            op $ alloc 12 14 >> alloc 13 13 >> alloc 14 12
-            op $ alloc 15 17 >> alloc 16 16 >> alloc 17 15
-            op $ alloc 18 20 >> alloc 19 19 >> alloc 20 18
-            op $ alloc 21 23 >> alloc 22 22 >> alloc 23 21
-            op $ alloc 24 26 >> alloc 25 25 >> alloc 26 24
-            op $ alloc 27 29 >> alloc 28 28 >> alloc 29 27
-            op $ alloc 30 27 >> alloc 31 31 >> alloc 32 30
+        label "entry"
+            (do {-  1 -} add r2 r1 r0
+                {-  3 -} add r5 r4 r3
+                {-  5 -} add r8 r7 r6
+                {-  7 -} add r11 r10 r9
+                {-  9 -} add r14 r13 r12
+                {- 11 -} add r17 r16 r15
+                {- 13 -} add r20 r19 r18
+                {- 15 -} add r23 r22 r21
+                {- 17 -} add r26 r25 r24
+                {- 19 -} add r29 r28 r27
+
+                -- When we reach the 32nd variable considered (which happens
+                -- to be v30), we must spill a register because there are not 32
+                -- registers.  So we pick the first register, counting from 0,
+                -- whose next use position is the furthest from this position.
+                -- That happens to be r27, which is next used at position 41.
+                         save 27 0
+                {- 21 -} add r27 r31 r30
+
+                {- 23 -} add r2 r1 r0
+                {- 25 -} add r5 r4 r3
+                {- 27 -} add r8 r7 r6
+                {- 29 -} add r11 r10 r9
+                {- 31 -} add r14 r13 r12
+                {- 33 -} add r17 r16 r15
+                {- 35 -} add r20 r19 r18
+                {- 37 -} add r23 r22 r21
+                {- 39 -} add r26 r25 r24
+
+                -- When it comes time to reload v29 (which had been allocated
+                -- to r27), we pick the first available register which happens
+                -- to be r0 in this case.
+                         restore 0 0
+                {- 41 -} add r29 r28 r0
+
+                {- 43 -} add r27 r31 r30)
+            return_