diff --git a/LinearScan.hs b/LinearScan.hs
--- a/LinearScan.hs
+++ b/LinearScan.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE ViewPatterns #-}
 
@@ -9,27 +10,37 @@
     ( -- * Main entry point
       allocate
       -- * Blocks
-    , BlockInfo(..)
+    , LinearScan.BlockInfo(..)
       -- * Operations
-    , OpInfo(..)
+    , LinearScan.OpInfo(..)
     , OpKind(..)
       -- * Variables
     , VarId
-    , VarInfo(..)
-    , VarKind(..)
+    , LinearScan.VarInfo(..)
+    , LS.VarKind(..)
     , PhysReg
     ) where
 
-import Control.Monad.Trans.State
+import           Control.Monad.State
+import           Data.Functor.Identity
+import           Data.IntMap (IntMap)
+import qualified Data.IntMap as M
+import           Data.IntSet (IntSet)
+import qualified Data.IntSet as S
+import qualified Data.List as L
+-- import           Debug.Trace
 import qualified LinearScan.Blocks as LS
+import           LinearScan.Blocks as LS
+import qualified LinearScan.IntMap as LS
+import qualified LinearScan.Interval as LS
+import qualified LinearScan.LiveSets as LS
+import qualified LinearScan.Loops as LS
 import qualified LinearScan.Main as LS
 import qualified LinearScan.Morph as LS
-import LinearScan.Blocks
-    ( VarId
-    , VarKind(..)
-    , OpKind(..)
-    , PhysReg
-    )
+import qualified LinearScan.Range as LS
+import qualified LinearScan.ScanState as LS
+import qualified LinearScan.UsePos as LS
+import qualified LinearScan.Utils as LS
 
 -- | Each variable has associated allocation details, and a flag to indicate
 --   whether it must be loaded into a register at its point of use.  Variables
@@ -39,16 +50,19 @@
 --   variables extends until their final use.
 data VarInfo = VarInfo
     { varId       :: Either PhysReg VarId
-    , varKind     :: VarKind
+    , varKind     :: LS.VarKind
     , regRequired :: Bool
     }
 
-deriving instance Eq VarKind
--- deriving instance Show VarKind
+deriving instance Eq LS.VarKind
+deriving instance Show LS.VarKind
 
-fromVarInfo :: VarInfo -> LS.VarInfo
+fromVarInfo :: LinearScan.VarInfo -> LS.VarInfo
 fromVarInfo (VarInfo a b c) = LS.Build_VarInfo a b c
 
+toVarInfo :: LS.VarInfo -> LinearScan.VarInfo
+toVarInfo (LS.Build_VarInfo a b c) = 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
 --   considered unavailable for allocation over the range of such references.
@@ -62,26 +76,55 @@
 --   loop bodies.
 data OpInfo accType op1 op2 = OpInfo
     { opKind      :: op1 -> OpKind
-    , opRefs      :: op1 -> [VarInfo]
+    , opRefs      :: op1 -> [LinearScan.VarInfo]
     , moveOp      :: PhysReg   -> PhysReg   -> State accType [op2]
     , swapOp      :: PhysReg   -> PhysReg   -> State accType [op2]
     , saveOp      :: PhysReg   -> Maybe Int -> State accType [op2]
     , restoreOp   :: Maybe Int -> PhysReg   -> State accType [op2]
     , applyAllocs :: op1 -> [(Int, PhysReg)] -> [op2]
+    , showOp1     :: op1 -> String
     }
 
+showOp1' :: (op1 -> String)
+         -> LS.OpId
+           -- Interval Id, it's identity, and possible assigned reg
+         -> [(Int, Either PhysReg LS.VarId, Maybe PhysReg)]
+         -> [(Int, Either PhysReg LS.VarId, Maybe PhysReg)]
+         -> op1
+         -> String
+showOp1' showop pos ins outs o =
+    let showerv (Left r)  = "r" ++ show r
+        showerv (Right v) = "v" ++ show v in
+    let render Nothing = ""
+        render (Just r) = "=r" ++ show r in
+    let marker label (i, erv, reg) =
+            "<" ++ label ++ " " ++ showerv erv ++
+            (if i == either id id erv
+             then ""
+             else "[" ++ show i ++ "]") ++ render reg ++ ">\n" in
+    concatMap (marker "End") outs ++
+    concatMap (marker "Beg") ins ++
+    show pos ++ ": " ++ showop o ++ "\n"
+
 deriving instance Eq OpKind
 deriving instance Show OpKind
 
-fromOpInfo :: OpInfo accType op1 op2 -> LS.OpInfo accType op1 op2
-fromOpInfo (OpInfo a b c d e f g) =
-    LS.Build_OpInfo a
-        (map fromVarInfo . b)
+fromOpInfo :: LinearScan.OpInfo accType op1 op2 -> LS.OpInfo accType op1 op2
+fromOpInfo (OpInfo a b c d e f g h) =
+    LS.Build_OpInfo a (map fromVarInfo . b)
         ((runState .) . c)
         ((runState .) . d)
         ((runState .) . e)
-        ((runState .) . f) g
+        ((runState .) . f) g h
 
+toOpInfo :: LS.OpInfo accType op1 op2 -> LinearScan.OpInfo accType op1 op2
+toOpInfo (LS.Build_OpInfo a b c d e f g h) =
+    OpInfo a (map toVarInfo . b)
+        ((StateT .) . fmap (fmap (fmap Identity)) c)
+        ((StateT .) . fmap (fmap (fmap Identity)) d)
+        ((StateT .) . fmap (fmap (fmap Identity)) e)
+        ((StateT .) . fmap (fmap (fmap Identity)) f) g h
+
 -- | From the point of view of this library, a basic block is nothing more
 --   than an ordered sequence of operations.
 data BlockInfo blk1 blk2 op1 op2 = BlockInfo
@@ -91,12 +134,225 @@
     , setBlockOps     :: blk1 -> [op2] -> [op2] -> [op2] -> blk2
     }
 
-fromBlockInfo :: BlockInfo blk1 blk2 op1 op2
+type IntervalId = Int
+
+data ScanStateDesc = ScanStateDesc
+    { _nextInterval  :: Int
+    , intervals      :: [LS.IntervalDesc]
+    , fixedIntervals :: [Maybe LS.IntervalDesc]
+    , unhandled      :: [(IntervalId, Int)]
+    , active         :: [(IntervalId, PhysReg)]
+    , inactive       :: [(IntervalId, PhysReg)]
+    , handled        :: [(IntervalId, Maybe PhysReg)]
+    , allocations    :: IntMap PhysReg
+    }
+
+deriving instance Show LS.IntervalDesc
+deriving instance Show LS.RangeDesc
+deriving instance Show LS.UsePos
+
+instance Show ScanStateDesc where
+    show sd =
+        "Unhandled:\n"
+            ++ concatMap (\(i, _) -> "  " ++ showInterval i ++ "\n")
+                         (unhandled sd) ++
+        "Active:\n"
+            ++ concatMap (\(i, r) ->
+                           "  r" ++ show r ++ showInterval i ++ "\n")
+                         (active sd) ++
+        "Inactive:\n"
+            ++ concatMap (\(i, r) ->
+                           "  r" ++ show r ++ showInterval i ++ "\n")
+                         (inactive sd) ++
+        "Handled:\n"
+            ++ concatMap (\(i, r) ->
+                           "  " ++ showReg r ++ showInterval i ++ "\n")
+                         (handled sd)
+      where
+        showInterval i = showIntervalDesc i (intervals sd !! i)
+
+        showReg Nothing = "<stack>"
+        showReg (Just r) = "r" ++ show r
+
+showIntervalDesc :: Int -> LS.IntervalDesc -> String
+showIntervalDesc i (LS.Build_IntervalDesc iv ib ie rs) =
+    "[" ++ show i ++ "]: " ++ " v" ++ show iv ++ " "
+          ++ show ib ++ "-" ++ show ie ++ " =>" ++ showRanges rs
+
+showRanges :: [LS.RangeDesc] -> String
+showRanges [] = ""
+showRanges (LS.Build_RangeDesc rb re us:rs) =
+    " " ++ show rb ++ "-" ++ show re
+      ++ (case us of
+               [] -> ""
+               _  -> " [" ++ showUsePositions us ++ "]")
+      ++ showRanges rs
+
+showUsePositions :: [LS.UsePos] -> String
+showUsePositions [] = ""
+showUsePositions [u] = go u
+  where
+    go (LS.Build_UsePos n req _v) = show n ++ (if req then "" else "?")
+showUsePositions (u:us) = go u ++ " " ++ showUsePositions us
+  where
+    go (LS.Build_UsePos n req _v) = show n ++ (if req then "" else "?")
+
+toScanStateDesc :: LS.ScanStateDesc -> ScanStateDesc
+toScanStateDesc (LS.Build_ScanStateDesc a b c d e f g) =
+    let rs = L.foldl' (\m (k, mx) -> case mx of
+                            Nothing -> m
+                            Just r -> M.insert k r m)
+                 M.empty g in
+    let xs = L.foldl' (\m (k, r) -> M.insert k r m) rs (e ++ f) in
+    ScanStateDesc a b c d e f g xs
+
+data LoopState = LoopState
+    { activeBlocks     :: IntSet
+    , visitedBlocks    :: IntSet
+    , loopHeaderBlocks :: [BlockId]
+    , loopEndBlocks    :: IntSet
+    , forwardBranches  :: IntMap IntSet
+    , backwardBranches :: IntMap IntSet
+    , loopIndices      :: IntMap IntSet
+    , loopDepths       :: IntMap (Int, Int)
+    }
+
+instance Show LoopState where
+  show LoopState {..} = "LoopState = " ++
+      "\n    activeBlocks     = " ++ show (S.toList activeBlocks) ++
+      "\n    visitedBlocks    = " ++ show (S.toList visitedBlocks) ++
+      "\n    loopHeaderBlocks = " ++ show loopHeaderBlocks ++
+      "\n    loopEndBlocks    = " ++ show (S.toList loopEndBlocks) ++
+      "\n    forwardBranches  = " ++ show (map (fmap S.toList) $
+                                           M.toList forwardBranches) ++
+      "\n    backwardBranches = " ++ show (map (fmap S.toList) $
+                                           M.toList backwardBranches) ++
+      "\n    loopIndices      = " ++ show (map (fmap S.toList) $
+                                           M.toList loopIndices) ++
+      "\n    loopDepths       = " ++ show (M.toList loopDepths)
+
+toLoopState :: LS.LoopState -> LinearScan.LoopState
+toLoopState (LS.Build_LoopState a b c d e f g h) =
+    LoopState (S.fromList a) (S.fromList b) c (S.fromList d)
+        (M.fromList (map (fmap S.fromList) e))
+        (M.fromList (map (fmap S.fromList) f))
+        (M.fromList (map (fmap S.fromList) g))
+        (M.fromList h)
+
+-- tracer :: String -> a -> a
+-- tracer x = Debug.Trace.trace ("====================\n" ++ x)
+
+showBlock1 :: (blk1 -> [op1])
+           -> LS.BlockId
+           -> LS.OpId
+           -> [Int]
+           -> [Int]
+           -> (LS.OpId -> [op1] -> String)
+           -> blk1
+           -> String
+showBlock1 getops bid pos liveIns liveOuts showops b =
+    "\nBlock " ++ show bid ++
+    " => IN:" ++ show liveIns ++ " OUT:" ++ show liveOuts ++ "\n" ++
+    showops pos (getops b)
+
+showOps1 :: LinearScan.OpInfo accType op1 op2 -> ScanStateDesc -> Int -> [op1]
+         -> String
+showOps1 _ _ _ [] = ""
+showOps1 oinfo sd pos (o:os) =
+    let here = pos*2+1 in
+    let allocs = allocations sd in
+    let k idx (bacc, eacc) i =
+            let mreg = M.lookup idx allocs in
+            (if LS.ibeg i == here
+             then (idx, Right (LS.ivar i), mreg) : bacc
+             else bacc,
+             if LS.iend i == here
+             then (idx, Right (LS.ivar i), mreg) : eacc
+             else eacc) in
+    let r _idx acc Nothing = acc
+        r idx (bacc, eacc) (Just i) =
+            let mreg = M.lookup idx allocs in
+            (if LS.ibeg i == here
+             then (idx, Left idx, mreg) : bacc
+             else bacc,
+             if LS.iend i == here
+             then (idx, Left idx, mreg) : eacc
+             else eacc) in
+    let (begs, ends) =
+            LS.vfoldl'_with_index (0 :: Int) k ([], []) (intervals sd) in
+    let (begs', ends') =
+            LS.vfoldl'_with_index (0 :: Int) r (begs, ends)
+                                  (fixedIntervals sd) in
+    showOp1' (showOp1 oinfo) (pos*2+1) begs' ends' o
+        ++ showOps1 oinfo sd (pos+1) os
+
+showBlocks1 :: LinearScan.BlockInfo blk1 blk2 op1 op2
+            -> LinearScan.OpInfo accType op1 op2
+            -> ScanStateDesc
+            -> LS.IntMap LS.BlockLiveSets
+            -> [blk1]
+            -> String
+showBlocks1 binfo oinfo sd ls = go 0
+  where
+    go _ [] = ""
+    go pos (b:bs) =
+        let bid = LinearScan.blockId binfo b in
+        let (liveIn, liveOut) =
+                 case LS.coq_IntMap_lookup bid ls of
+                     Nothing -> (LS.emptyIntSet, LS.emptyIntSet)
+                     Just s  -> (LS.blockLiveIn s, LS.blockLiveOut s) in
+        let allops blk = let (x, y, z) = LinearScan.blockOps binfo blk in
+                         x ++ y ++ z in
+        showBlock1 allops bid pos liveIn liveOut (showOps1 oinfo sd) b
+            ++ go (pos + length (allops b)) bs
+
+fromBlockInfo :: LinearScan.BlockInfo blk1 blk2 op1 op2
               -> LS.BlockInfo blk1 blk2 op1 op2
 fromBlockInfo (BlockInfo a b c d) =
-    LS.Build_BlockInfo a b
-        (\blk -> let (x, y, z) = c blk in ((x, y), z)) d
+    LS.Build_BlockInfo a b (\blk -> let (x, y, z) = c blk in ((x, y), z)) d
 
+toBlockInfo :: LS.BlockInfo blk1 blk2 op1 op2
+            -> LinearScan.BlockInfo blk1 blk2 op1 op2
+toBlockInfo (LS.Build_BlockInfo a b c d) =
+    BlockInfo a b (\blk -> let ((x, y), z) = c blk in (x, y, z)) d
+
+data Details blk1 blk2 op1 op2 accType = Details
+    { reason          :: Maybe (LS.SSError, LS.FinalStage)
+    , liveSets        :: [(Int, LS.BlockLiveSets)]
+    , inputBlocks     :: [blk1]
+    , allocatedBlocks :: [blk2]
+    , accumulator     :: accType
+    , scanStatePre    :: Maybe ScanStateDesc
+    , scanStatePost   :: Maybe ScanStateDesc
+    , blockInfo       :: LinearScan.BlockInfo blk1 blk2 op1 op2
+    , opInfo          :: LinearScan.OpInfo accType op1 op2
+    , loopState       :: LoopState
+    }
+
+instance Show (Details blk1 blk2 op1 op2 accType) where
+    show err = "Reason: " ++ show (reason err) ++ "\n\n"
+               ++ ">>> ScanState before allocation:\n"
+               ++ showScanStateDesc (scanStatePre err) ++ "\n"
+               ++ ">>> ScanState after allocation:\n"
+               ++ showScanStateDesc (scanStatePost err) ++ "\n"
+               ++ ">>> " ++ show (loopState err) ++ "\n"
+      where
+        showScanStateDesc Nothing = ""
+        showScanStateDesc (Just sd) =
+            showBlocks1 (blockInfo err) (opInfo err) sd
+                        (liveSets err) (inputBlocks err)
+                ++ "\n" ++ show sd
+
+deriving instance Show LS.SSError
+deriving instance Show LS.FinalStage
+deriving instance Show LS.BlockLiveSets
+
+toDetails :: LS.Details blk1 blk2 op1 op2 accType
+               -> Details blk1 blk2 op1 op2 accType
+toDetails (LS.Build_Details a b c d e f g h i j) =
+    Details a b c d e (fmap toScanStateDesc f) (fmap toScanStateDesc g)
+                 (toBlockInfo h) (toOpInfo i) (toLoopState j)
+
 -- | 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
@@ -109,37 +365,48 @@
 --   simply not enough registers -- a 'Left' value is returned, with a string
 --   describing the error.
 allocate :: Int                  -- ^ Maximum number of registers to use
-         -> BlockInfo blk1 blk2 op1 op2
-         -> OpInfo accType op1 op2
+         -> LinearScan.BlockInfo blk1 blk2 op1 op2
+         -> LinearScan.OpInfo accType op1 op2
          -> [blk1]
          -> State accType (Either String [blk2])
 allocate 0 _ _ _  = return $ Left "Cannot allocate with no registers"
 allocate _ _ _ [] = return $ Left "No basic blocks were provided"
 allocate maxReg (fromBlockInfo -> binfo) (fromOpInfo -> oinfo) blocks = do
-    eres <- gets (LS.linearScan maxReg binfo oinfo blocks)
-    case eres of
-        Left x -> return $ Left $ case x of
-            LS.ECannotSplitSingleton1 n ->
-                "Current interval is a singleton (err#1) (" ++ show n ++ ")"
-            LS.ECannotSplitSingleton2 n ->
-                "Current interval is a singleton (err#2) (" ++ show n ++ ")"
-            LS.ECannotSplitSingleton3 n ->
-                "Current interval is a singleton (err#3) (" ++ show n ++ ")"
-            LS.ECannotSplitSingleton4 n ->
-                "Current interval is a singleton (err#4) (" ++ show n ++ ")"
-            LS.ECannotSplitSingleton5 n ->
-                "Current interval is a singleton (err#5) (" ++ show n ++ ")"
-            LS.ECannotSplitSingleton6 n ->
-                "Current interval is a singleton (err#6) (" ++ show n ++ ")"
-            LS.ECannotSplitSingleton7 n ->
-                "Current interval is a singleton (err#7) (" ++ show n ++ ")"
-            LS.ENoIntervalsToSplit ->
-                "There are no intervals to split"
-            LS.ERegisterAlreadyAssigned n ->
-                "Register is already assigned (" ++ show n ++ ")"
-            LS.ERegisterAssignmentsOverlap n ->
-                "Register assignments overlap (" ++ show n ++ ")"
-            LS.EFuelExhausted -> "Fuel was exhausted"
-            LS.EUnexpectedNoMoreUnhandled ->
-                "The unexpected happened: no more unhandled intervals"
-        Right (z, acc) -> put acc >> return (Right z)
+    res <- gets (LS.linearScan maxReg binfo oinfo blocks)
+    let res' = toDetails res
+    put $ accumulator res'
+    case reason res' of
+        Just (err, _) -> reportError res' err
+        Nothing ->
+            -- tracer (show res') $
+            return $ Right (allocatedBlocks res')
+  where
+    -- reportError res err =
+    --     return $ Left $ tracer (show res) $ reasonToStr err
+    reportError _res err =
+        return $ Left $ reasonToStr err
+
+    reasonToStr r = case r of
+        LS.ERegistersExhausted _ ->
+            "No registers available for allocation"
+        LS.ENoValidSplitPositionUnh xid splitPos ->
+            "No split position could be found for unhandled interval "
+                ++ show xid ++ " @ " ++ show splitPos
+        LS.ENoValidSplitPosition xid splitPos ->
+            "No split position could be found for " ++ show xid
+                ++ " @ " ++ show splitPos
+        LS.ECannotSplitSingleton1 n ->
+            "Current interval is a singleton (err#1) (" ++ show n ++ ")"
+        LS.ECannotSplitSingleton2 n ->
+            "Current interval is a singleton (err#2) (" ++ show n ++ ")"
+        LS.ECannotSplitSingleton3 n ->
+            "Current interval is a singleton (err#3) (" ++ show n ++ ")"
+        LS.ENoIntervalsToSplit ->
+            "There are no intervals to split"
+        LS.ERegisterAlreadyAssigned n ->
+            "Register is already assigned (" ++ show n ++ ")"
+        LS.ERegisterAssignmentsOverlap n ->
+            "Register assignments overlap (" ++ show n ++ ")"
+        LS.EFuelExhausted -> "Fuel was exhausted"
+        LS.EUnexpectedNoMoreUnhandled ->
+            "The unexpected happened: no more unhandled intervals"
diff --git a/LinearScan/Allocate.hs b/LinearScan/Allocate.hs
--- a/LinearScan/Allocate.hs
+++ b/LinearScan/Allocate.hs
@@ -52,12 +52,10 @@
   Cursor.withCursor maxReg pre (\sd _ ->
     let {int = Cursor.curIntDetails maxReg sd} in
     Morph.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
-        (ScanState.fixedIntervals maxReg sd)))
+      (case LinearScan.Utils.nth maxReg (ScanState.fixedIntervals maxReg sd)
+              reg of {
+        Prelude.Just i -> Interval.intervalIntersectionPoint ( int) ( i);
+        Prelude.Nothing -> Prelude.Nothing}))
 
 updateRegisterPos :: Prelude.Int -> ([] (Prelude.Maybe Lib.Coq_oddnum)) ->
                      Prelude.Int -> (Prelude.Maybe Lib.Coq_oddnum) -> []
@@ -78,6 +76,7 @@
                       () () (Prelude.Maybe (Morph.SState () () PhysReg))
 tryAllocateFreeReg maxReg pre =
   Cursor.withCursor maxReg pre (\sd _ ->
+    let {pos = Cursor.curPosition maxReg sd} in
     let {
      go = \f v p ->
       case p of {
@@ -100,43 +99,47 @@
                                (ScanState.inactive maxReg sd)}
     in
     let {
-     freeUntilPos = Data.List.foldl'
-                      (go (\i ->
-                        Interval.intervalIntersectionPoint
-                          (
-                            (LinearScan.Utils.nth
-                              (ScanState.nextInterval maxReg sd)
-                              (ScanState.intervals maxReg sd) i))
-                          ( (Cursor.curIntDetails maxReg sd)))) freeUntilPos'
-                      intersectingIntervals}
+     freeUntilPos'' = Data.List.foldl'
+                        (go (\i ->
+                          Interval.intervalIntersectionPoint
+                            (
+                              (LinearScan.Utils.nth
+                                (ScanState.nextInterval maxReg sd)
+                                (ScanState.intervals maxReg sd) i))
+                            ( (Cursor.curIntDetails maxReg sd))))
+                        freeUntilPos' intersectingIntervals}
     in
+    let {
+     freeUntilPos = (LinearScan.Utils.vfoldl'_with_index) maxReg
+                      (\reg acc mint ->
+                      case mint of {
+                       Prelude.Just int ->
+                        updateRegisterPos maxReg acc reg
+                          (Interval.intervalIntersectionPoint ( int)
+                            ( (Cursor.curIntDetails maxReg sd)));
+                       Prelude.Nothing -> acc}) freeUntilPos''
+                      (ScanState.fixedIntervals maxReg sd)}
+    in
     case ScanState.registerWithHighestPos maxReg freeUntilPos of {
      (,) reg mres ->
       let {
        success = Morph.stbind (\x -> Morph.return_ reg)
                    (Morph.moveUnhandledToActive maxReg pre reg)}
       in
-      let {
-       maction = case mres of {
-                  Prelude.Just n ->
-                   case Eqtype.eq_op Ssrnat.nat_eqType ( (unsafeCoerce n))
-                          (unsafeCoerce ((Prelude.succ) 0)) of {
-                    Prelude.True -> Prelude.Nothing;
-                    Prelude.False -> Prelude.Just
-                     (case (Prelude.<=) ((Prelude.succ)
-                             (Interval.intervalEnd
-                               ( (Cursor.curIntDetails maxReg sd)))) 
-                             ( n) of {
-                       Prelude.True -> success;
-                       Prelude.False ->
-                        Morph.stbind (\x ->
-                          Morph.stbind (\x0 -> Morph.return_ reg)
-                            (Morph.moveUnhandledToActive maxReg pre reg))
-                          (Split.splitCurrentInterval maxReg pre
-                            (Split.BeforePos n))})};
-                  Prelude.Nothing -> Prelude.Just success}}
-      in
-      Morph.return_ maction})
+      Morph.return_
+        (case mres of {
+          Prelude.Just n ->
+           case (Prelude.<=) ( n) pos of {
+            Prelude.True -> Prelude.Nothing;
+            Prelude.False -> Prelude.Just
+             (case (Prelude.<=) ((Prelude.succ)
+                     (Interval.intervalEnd
+                       ( (Cursor.curIntDetails maxReg sd)))) ( n) of {
+               Prelude.True -> success;
+               Prelude.False ->
+                Morph.stbind (\x -> success)
+                  (Split.splitCurrentInterval maxReg pre (Split.BeforePos n))})};
+          Prelude.Nothing -> Prelude.Just success})})
 
 allocateBlockedReg :: Prelude.Int -> ScanState.ScanStateDesc -> Morph.SState
                       () () (Prelude.Maybe PhysReg)
@@ -146,68 +149,78 @@
     in
     let {pos = Cursor.curPosition maxReg sd} in
     let {
-     go = \v p ->
+     go = \n v p ->
       case p of {
-       (,) i r ->
+       (,) int r ->
         let {
          atPos = \u ->
           Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos)
             (unsafeCoerce (UsePos.uloc u))}
         in
         let {
-         pos' = case Interval.findIntervalUsePos
-                       (Interval.getIntervalDesc
-                         (
-                           (LinearScan.Utils.nth
-                             (ScanState.nextInterval maxReg sd)
-                             (ScanState.intervals maxReg sd) i))) atPos of {
+         pos' = case Interval.findIntervalUsePos ( int) atPos of {
                  Prelude.Just s -> Prelude.Just Lib.odd1;
-                 Prelude.Nothing ->
-                  Interval.nextUseAfter
-                    (Interval.getIntervalDesc
-                      (
-                        (LinearScan.Utils.nth
-                          (ScanState.nextInterval maxReg sd)
-                          (ScanState.intervals maxReg sd) i))) start}}
+                 Prelude.Nothing -> Interval.nextUseAfter ( int) start}}
         in
-        updateRegisterPos maxReg v r pos'}}
+        updateRegisterPos n v r pos'}}
     in
     let {
-     nextUsePos' = Data.List.foldl' go
+     resolve = \xs ->
+      Prelude.map (\i -> (,)
+        (Interval.packInterval
+          (
+            (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)
+              (ScanState.intervals maxReg sd) (Prelude.fst i))))
+        (Prelude.snd i)) xs}
+    in
+    let {
+     nextUsePos' = Data.List.foldl' (go maxReg)
                      (Data.List.replicate maxReg Prelude.Nothing)
-                     (ScanState.active maxReg sd)}
+                     (resolve (ScanState.active maxReg sd))}
     in
     let {
-     intersectingIntervals = Prelude.filter (\x ->
-                               Interval.intervalsIntersect
-                                 ( (Cursor.curIntDetails maxReg sd))
-                                 (
-                                   (LinearScan.Utils.nth
-                                     (ScanState.nextInterval maxReg sd)
-                                     (ScanState.intervals maxReg sd)
-                                     (Prelude.fst x))))
-                               (ScanState.inactive maxReg sd)}
+     intersectingIntervals = (Prelude.++)
+                               (Prelude.filter (\x ->
+                                 Interval.intervalsIntersect
+                                   ( (Cursor.curIntDetails maxReg sd))
+                                   ( (Prelude.fst x)))
+                                 (resolve (ScanState.inactive maxReg sd)))
+                               ((LinearScan.Utils.vfoldl'_with_index) maxReg
+                                 (\reg acc mint ->
+                                 case mint of {
+                                  Prelude.Just int ->
+                                   case Interval.intervalsIntersect
+                                          ( (Cursor.curIntDetails maxReg sd))
+                                          ( int) of {
+                                    Prelude.True -> (:) ((,) int reg) acc;
+                                    Prelude.False -> acc};
+                                  Prelude.Nothing -> acc}) []
+                                 (ScanState.fixedIntervals maxReg sd))}
     in
-    let {nextUsePos = Data.List.foldl' go nextUsePos' intersectingIntervals}
+    let {
+     nextUsePos = Data.List.foldl' (go maxReg) nextUsePos'
+                    intersectingIntervals}
     in
     case ScanState.registerWithHighestPos maxReg nextUsePos of {
      (,) reg mres ->
       case case mres of {
-            Prelude.Just n -> (Prelude.<=) ((Prelude.succ) ( n)) start;
+            Prelude.Just n ->
+             (Prelude.<=) ((Prelude.succ) ( n))
+               (case Interval.lookupUsePos
+                       ( (Cursor.curIntDetails maxReg sd)) (\u ->
+                       (Prelude.<=) pos (UsePos.uloc u)) of {
+                 Prelude.Just s ->  s;
+                 Prelude.Nothing ->
+                  Interval.intervalEnd ( (Cursor.curIntDetails maxReg sd))});
             Prelude.Nothing -> Prelude.False} of {
        Prelude.True ->
+        let {
+         p = Interval.firstUseReqRegOrEnd ( (Cursor.curIntDetails maxReg sd))}
+        in
         Morph.stbind (\x ->
-          Morph.stbind (\mloc ->
-            Morph.stbind (\x0 ->
-              Morph.stbind (\x1 -> Morph.return_ Prelude.Nothing)
-                (Morph.weakenHasLen_ maxReg pre))
-              (case mloc of {
-                Prelude.Just n ->
-                 Split.splitCurrentInterval maxReg pre (Split.BeforePos n);
-                Prelude.Nothing -> Morph.return_ ()}))
-            (intersectsWithFixedInterval maxReg pre reg))
-          (Split.splitCurrentInterval maxReg pre
-            Split.BeforeFirstUsePosReqReg);
+          Morph.stbind (\x0 -> Morph.return_ Prelude.Nothing)
+            (Morph.moveUnhandledToHandled maxReg pre))
+          (Split.splitCurrentInterval maxReg pre (Split.BeforePos p));
        Prelude.False ->
         Morph.stbind (\x ->
           Morph.stbind (\x0 ->
@@ -221,7 +234,7 @@
                   Prelude.Nothing -> Morph.return_ ()}))
               (intersectsWithFixedInterval maxReg pre reg))
             (Split.splitActiveIntervalForReg maxReg pre reg pos))
-          (Split.splitAnyInactiveIntervalForReg maxReg pre reg)}})
+          (Split.splitAnyInactiveIntervalForReg maxReg pre reg pos)}})
 
 morphlen_transport :: Prelude.Int -> ScanState.ScanStateDesc ->
                       ScanState.ScanStateDesc -> ScanState.IntervalId ->
@@ -252,7 +265,7 @@
    Prelude.True -> Morph.moveActiveToHandled maxReg z (unsafeCoerce x);
    Prelude.False ->
     case Prelude.not
-           (Interval.intervalCoversPos
+           (Interval.posWithinInterval
              (
                (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)
                  (ScanState.intervals maxReg z) (Prelude.fst x))) pos) of {
@@ -316,7 +329,7 @@
     in
     f filtered_var;
    Prelude.False ->
-    case Interval.intervalCoversPos
+    case Interval.posWithinInterval
            (
              (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)
                (ScanState.intervals maxReg z) (Prelude.fst x))) pos of {
@@ -352,24 +365,41 @@
 handleInterval maxReg pre =
   Cursor.withCursor maxReg pre (\sd _ ->
     let {position = Cursor.curPosition maxReg sd} in
-    Morph.stbind (\x ->
-      Morph.stbind (\x0 ->
-        Morph.stbind (\mres ->
-          case mres of {
-           Prelude.Just x1 -> IState.imap (\x2 -> Prelude.Just x2) x1;
-           Prelude.Nothing -> allocateBlockedReg maxReg pre})
-          (tryAllocateFreeReg maxReg pre))
+    case Interval.firstUsePos
+           (Interval.getIntervalDesc ( (Cursor.curIntDetails maxReg sd))) of {
+     Prelude.Just u ->
+      Morph.stbind (\x ->
+        Morph.stbind (\x0 ->
+          Morph.stbind (\mres ->
+            case mres of {
+             Prelude.Just x1 -> IState.imap (\x2 -> Prelude.Just x2) x1;
+             Prelude.Nothing -> allocateBlockedReg maxReg pre})
+            (tryAllocateFreeReg maxReg pre))
+          (Morph.liftLen maxReg pre (\sd0 ->
+            checkInactiveIntervals maxReg sd0 position)))
         (Morph.liftLen maxReg pre (\sd0 ->
-          checkInactiveIntervals maxReg sd0 position)))
-      (Morph.liftLen maxReg pre (\sd0 ->
-        checkActiveIntervals maxReg sd0 position)))
+          checkActiveIntervals maxReg sd0 position));
+     Prelude.Nothing ->
+      Morph.stbind (\x -> Morph.return_ Prelude.Nothing)
+        (Morph.moveUnhandledToHandled maxReg pre)})
 
+finalizeScanState :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int ->
+                     ScanState.ScanStateDesc
+finalizeScanState maxReg sd finalPos =
+  case Morph.stbind (\x -> checkInactiveIntervals maxReg sd finalPos)
+         (checkActiveIntervals maxReg sd finalPos) (Morph.Build_SSInfo sd __) of {
+   Prelude.Left s -> sd;
+   Prelude.Right p ->
+    case p of {
+     (,) u ss -> Morph.thisDesc maxReg sd ss}}
+
 walkIntervals :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int ->
-                 Prelude.Either Morph.SSError ScanState.ScanStateSig
+                 Prelude.Either ((,) Morph.SSError ScanState.ScanStateSig)
+                 ScanState.ScanStateSig
 walkIntervals maxReg sd positions =
   (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
-    (\_ -> Prelude.Left
-    Morph.EFuelExhausted)
+    (\_ -> Prelude.Left ((,) Morph.EFuelExhausted
+    (ScanState.packScanState maxReg ScanState.InUse sd)))
     (\n ->
     let {
      go = let {
@@ -380,7 +410,9 @@
                __))
                (\cnt ->
                case handleInterval maxReg sd ss of {
-                Prelude.Left err -> Prelude.Left err;
+                Prelude.Left err -> Prelude.Left ((,) err
+                 (ScanState.packScanState maxReg ScanState.InUse
+                   (Morph.thisDesc maxReg sd ss)));
                 Prelude.Right p ->
                  case p of {
                   (,) o ss' ->
@@ -393,8 +425,10 @@
                      (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
                        (\_ -> Prelude.Right
                        ss')
-                       (\n0 -> Prelude.Left
-                       Morph.EUnexpectedNoMoreUnhandled)
+                       (\n0 -> Prelude.Left ((,)
+                       Morph.EUnexpectedNoMoreUnhandled
+                       (ScanState.packScanState maxReg ScanState.InUse
+                         (Morph.thisDesc maxReg sd ss'))))
                        cnt}}})
                count0}
           in go}
diff --git a/LinearScan/Assign.hs b/LinearScan/Assign.hs
--- a/LinearScan/Assign.hs
+++ b/LinearScan/Assign.hs
@@ -17,12 +17,14 @@
 import qualified LinearScan.Graph as Graph
 import qualified LinearScan.IntMap as IntMap
 import qualified LinearScan.Interval as Interval
+import qualified LinearScan.Lib as Lib
 import qualified LinearScan.LiveSets as LiveSets
 import qualified LinearScan.Resolve as Resolve
-import qualified LinearScan.ScanState as ScanState
 import qualified LinearScan.State as State
+import qualified LinearScan.UsePos as UsePos
 import qualified LinearScan.Eqtype as Eqtype
 import qualified LinearScan.Fintype as Fintype
+import qualified LinearScan.Seq as Seq
 import qualified LinearScan.Ssrnat as Ssrnat
 
 
@@ -68,6 +70,16 @@
 
 type AssnState accType a = State.State (AssnStateInfo accType) a
 
+swapOpM :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Blocks.PhysReg ->
+           Blocks.PhysReg -> AssnState a3 ([] a2)
+swapOpM maxReg oinfo sreg dreg =
+  State.bind (\assn ->
+    case Blocks.swapOp maxReg oinfo sreg dreg (assnAcc assn) of {
+     (,) mop acc' ->
+      State.bind (\x -> State.pure mop)
+        (State.put (Build_AssnStateInfo (assnOpId assn) (assnBlockBeg assn)
+          (assnBlockEnd assn) acc'))}) State.get
+
 moveOpM :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Blocks.PhysReg ->
            Blocks.PhysReg -> AssnState a3 ([] a2)
 moveOpM maxReg oinfo sreg dreg =
@@ -98,190 +110,72 @@
         (State.put (Build_AssnStateInfo (assnOpId assn) (assnBlockBeg assn)
           (assnBlockEnd 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 :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Blocks.OpId ->
-                    Blocks.VarInfo -> Blocks.PhysReg -> Interval.IntervalDesc
-                    -> IntMap.IntSet -> AssnState a3 ((,) ([] a2) ([] a2))
-savesAndRestores maxReg oinfo opid v reg int outs =
-  case Blocks.varId maxReg v of {
-   Prelude.Left p -> State.pure ((,) [] []);
-   Prelude.Right vid ->
-    State.bind (\assn ->
-      let {knd = Blocks.varKind maxReg v} in
-      let {
-       atBoundary = (Prelude.||)
-                      ((Prelude.&&)
-                        (Eqtype.eq_op Blocks.coq_VarKind_eqType
-                          (unsafeCoerce knd) (unsafeCoerce Blocks.Input))
-                        (Eqtype.eq_op Ssrnat.nat_eqType
-                          (unsafeCoerce (assnBlockBeg assn))
-                          (unsafeCoerce opid)))
-                      ((Prelude.&&)
-                        (Eqtype.eq_op Blocks.coq_VarKind_eqType
-                          (unsafeCoerce knd) (unsafeCoerce Blocks.Output))
-                        (Eqtype.eq_op Ssrnat.nat_eqType
-                          (unsafeCoerce ((Prelude.succ) ((Prelude.succ)
-                            opid))) (unsafeCoerce (assnBlockEnd assn))))}
-      in
-      let {
-       isFirst = Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)
-                   (unsafeCoerce (Interval.firstUsePos int))
-                   (unsafeCoerce (Prelude.Just opid))}
-      in
-      let {
-       isLast = Eqtype.eq_op
-                  (Eqtype.option_eqType
-                    (Eqtype.sig_eqType Ssrnat.nat_eqType
-                      (unsafeCoerce Ssrnat.odd)))
-                  (unsafeCoerce (Interval.nextUseAfter int opid))
-                  (unsafeCoerce Prelude.Nothing)}
-      in
-      let {save = saveOpM maxReg oinfo reg (Prelude.Just vid)} in
-      let {
-       msave = case atBoundary of {
-                Prelude.True -> State.pure [];
-                Prelude.False -> save}}
-      in
-      let {restore = restoreOpM maxReg oinfo (Prelude.Just vid) reg} in
-      let {
-       mrestore = case atBoundary of {
-                   Prelude.True -> State.pure [];
-                   Prelude.False -> restore}}
-      in
-      case knd of {
-       Blocks.Input ->
-        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 mrestore save;
-             Prelude.False -> pairM mrestore (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 mrestore (State.pure []);
-           Prelude.False -> State.pure ((,) [] [])}};
-       Blocks.Temp -> State.pure ((,) [] []);
-       Blocks.Output ->
-        case Interval.iknd int of {
-         Interval.LeftMost ->
-          case isLast of {
-           Prelude.True -> pairM (State.pure []) msave;
-           Prelude.False -> State.pure ((,) [] [])};
-         Interval.Middle ->
-          case isLast of {
-           Prelude.True -> pairM (State.pure []) msave;
-           Prelude.False -> State.pure ((,) [] [])};
-         _ -> State.pure ((,) [] [])}}) State.get}
-
-collectAllocs :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Prelude.Int ->
-                 IntMap.IntSet -> ([] ((,) Interval.IntervalDesc PhysReg)) ->
-                 ((,) ((,) ([] ((,) Blocks.VarId PhysReg)) ([] a2)) ([] a2))
-                 -> Blocks.VarInfo -> State.State (AssnStateInfo a3)
-                 ((,) ((,) ([] ((,) Blocks.VarId PhysReg)) ([] a2)) ([] a2))
-collectAllocs maxReg oinfo opid outs ints acc v =
+varAllocs :: Prelude.Int -> Prelude.Int -> ([] Resolve.Allocation) ->
+             Blocks.VarInfo -> [] ((,) Blocks.VarId PhysReg)
+varAllocs maxReg opid allocs v =
   case Blocks.varId maxReg v of {
-   Prelude.Left p -> State.pure acc;
+   Prelude.Left p -> [];
    Prelude.Right vid ->
-    let {
-     v_ints = Prelude.filter (\x ->
-                ScanState.isWithin (Prelude.fst x) vid opid) ints}
-    in
-    State.forFoldM acc v_ints (\acc' x ->
-      case x of {
-       (,) int reg ->
-        case acc' of {
-         (,) p saves' ->
-          case p of {
-           (,) allocs' restores' ->
-            State.bind (\res ->
-              case res of {
-               (,) rs ss ->
-                State.pure ((,) ((,) ((:) ((,) vid reg) allocs')
-                  ((Prelude.++) rs restores')) ((Prelude.++) ss saves'))})
-              (savesAndRestores maxReg oinfo opid v reg int outs)}}})}
-
-doAllocations :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> ([]
-                 ((,) Interval.IntervalDesc PhysReg)) -> IntMap.IntSet -> a1
-                 -> AssnState a3 ([] a2)
-doAllocations maxReg oinfo ints outs op =
-  State.bind (\assn ->
-    let {opid = assnOpId assn} in
-    let {vars = Blocks.opRefs maxReg oinfo op} in
-    State.bind (\res ->
-      case res of {
-       (,) y saves ->
-        case y of {
-         (,) allocs restores ->
-          let {op' = Blocks.applyAllocs maxReg oinfo op allocs} in
-          State.bind (\x ->
-            State.pure ((Prelude.++) restores ((Prelude.++) op' saves)))
-            (State.modify (\assn' -> Build_AssnStateInfo ((Prelude.succ)
-              ((Prelude.succ) opid)) (assnBlockBeg assn')
-              (assnBlockEnd assn') (assnAcc assn')))}})
-      (State.forFoldM ((,) ((,) [] []) []) vars
-        (collectAllocs maxReg oinfo opid outs ints))) State.get
+    Prelude.map (\x -> (,) vid x)
+      (Lib.catMaybes
+        (Prelude.map (\i -> Resolve.intReg maxReg i)
+          (Prelude.filter (\i ->
+            let {int = Resolve.intVal maxReg i} in
+            (Prelude.&&)
+              (Eqtype.eq_op Ssrnat.nat_eqType
+                (unsafeCoerce (Interval.ivar int)) (unsafeCoerce vid))
+              ((Prelude.&&) ((Prelude.<=) (Interval.ibeg int) opid)
+                (case Blocks.varKind maxReg v of {
+                  UsePos.Input -> (Prelude.<=) opid (Interval.iend int);
+                  _ -> (Prelude.<=) ((Prelude.succ) opid) (Interval.iend int)})))
+            allocs)))}
 
 generateMoves :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> ([]
-                 ((,) (Prelude.Maybe (Prelude.Either PhysReg Prelude.Int))
-                 (Prelude.Maybe (Prelude.Either PhysReg Prelude.Int)))) ->
-                 AssnState a3 ([] a2)
+                 Resolve.ResolvingMove) -> AssnState a3 ([] a2)
 generateMoves maxReg oinfo moves =
-  State.forFoldM [] moves (\acc mv ->
+  State.forFoldrM [] moves (\mv acc ->
     State.bind (\mops ->
       State.pure
         (case mops of {
           Prelude.Just ops -> (Prelude.++) ops acc;
           Prelude.Nothing -> acc}))
       (case mv of {
-        (,) o o0 ->
-         case o of {
-          Prelude.Just s ->
-           case s of {
-            Prelude.Left sreg ->
-             case o0 of {
-              Prelude.Just s0 ->
-               case s0 of {
-                Prelude.Left dreg ->
-                 State.fmap (\x -> Prelude.Just x)
-                   (moveOpM maxReg oinfo sreg dreg);
-                Prelude.Right vid ->
-                 State.fmap (\x -> Prelude.Just x)
-                   (saveOpM maxReg oinfo sreg (Prelude.Just vid))};
-              Prelude.Nothing ->
-               State.fmap (\x -> Prelude.Just x)
-                 (saveOpM maxReg oinfo sreg Prelude.Nothing)};
-            Prelude.Right vid ->
-             case o0 of {
-              Prelude.Just s0 ->
-               case s0 of {
-                Prelude.Left dreg ->
-                 State.fmap (\x -> Prelude.Just x)
-                   (restoreOpM maxReg oinfo (Prelude.Just vid) dreg);
-                Prelude.Right n -> State.pure Prelude.Nothing};
-              Prelude.Nothing -> State.pure Prelude.Nothing}};
-          Prelude.Nothing ->
-           case o0 of {
-            Prelude.Just s ->
-             case s of {
-              Prelude.Left dreg ->
-               State.fmap (\x -> Prelude.Just x)
-                 (restoreOpM maxReg oinfo Prelude.Nothing dreg);
-              Prelude.Right n -> State.pure Prelude.Nothing};
-            Prelude.Nothing -> State.pure Prelude.Nothing}}}))
+        Resolve.Move sreg dreg ->
+         State.fmap (\x -> Prelude.Just x) (moveOpM maxReg oinfo sreg dreg);
+        Resolve.Swap sreg dreg ->
+         State.fmap (\x -> Prelude.Just x) (swapOpM maxReg oinfo sreg dreg);
+        Resolve.Spill sreg vid ->
+         State.fmap (\x -> Prelude.Just x)
+           (saveOpM maxReg oinfo sreg (Prelude.Just vid));
+        Resolve.Restore vid dreg ->
+         State.fmap (\x -> Prelude.Just x)
+           (restoreOpM maxReg oinfo (Prelude.Just vid) dreg);
+        Resolve.Nop -> State.pure Prelude.Nothing}))
 
+doAllocations :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> ([]
+                 Resolve.Allocation) -> a1 -> AssnState a3 ([] a2)
+doAllocations maxReg oinfo allocs op =
+  State.bind (\assn ->
+    let {opid = assnOpId assn} in
+    let {vars = Blocks.opRefs maxReg oinfo op} in
+    let {
+     regs = State.concat (Prelude.map (varAllocs maxReg opid allocs) vars)}
+    in
+    let {ops = Blocks.applyAllocs maxReg oinfo op regs} in
+    State.bind (\transitions ->
+      State.bind (\x -> State.pure ((Prelude.++) ops transitions))
+        (State.modify (\assn' -> Build_AssnStateInfo ((Prelude.succ)
+          ((Prelude.succ) opid)) (assnBlockBeg assn') (assnBlockEnd assn')
+          (assnAcc assn'))))
+      (case (Prelude.&&) ((Prelude.<=) (assnBlockBeg assn) opid)
+              ((Prelude.<=) ((Prelude.succ) opid) (assnBlockEnd assn)) of {
+        Prelude.True ->
+         generateMoves maxReg oinfo
+           (Resolve.determineMoves maxReg
+             (Resolve.resolvingMoves maxReg allocs opid ((Prelude.succ)
+               ((Prelude.succ) opid))));
+        Prelude.False -> State.pure []})) State.get
+
 resolveMappings :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Prelude.Int ->
                    ([] a2) -> (IntMap.IntMap ((,) Graph.Graph Graph.Graph))
                    -> AssnState a3 ([] a2)
@@ -295,31 +189,26 @@
         State.bind (\emoves ->
           let {opsm'' = (Prelude.++) opsm' emoves} in State.pure opsm'')
           (generateMoves maxReg oinfo
-            (unsafeCoerce
+            (Prelude.map (Resolve.moveFromGraph maxReg)
               (Graph.topsort
                 (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
                   Ssrnat.nat_eqType) gend))))
         (generateMoves maxReg oinfo
-          (unsafeCoerce
+          (Prelude.map (Resolve.moveFromGraph maxReg)
             (Graph.topsort
               (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
                 Ssrnat.nat_eqType) gbeg)))};
    Prelude.Nothing -> State.pure opsm}
 
 considerOps :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->
-               (Blocks.OpInfo a5 a3 a4) -> (IntMap.IntSet -> a3 -> AssnState
-               a5 ([] a4)) -> (IntMap.IntMap LiveSets.BlockLiveSets) ->
-               (IntMap.IntMap ((,) Graph.Graph Graph.Graph)) -> ([] a1) ->
-               State.State (AssnStateInfo a5) ([] a2)
+               (Blocks.OpInfo a5 a3 a4) -> (a3 -> AssnState a5 ([] a4)) ->
+               (IntMap.IntMap LiveSets.BlockLiveSets) -> (IntMap.IntMap
+               ((,) Graph.Graph Graph.Graph)) -> ([] a1) -> State.State
+               (AssnStateInfo a5) ([] a2)
 considerOps maxReg binfo oinfo f liveSets mappings =
   State.mapM (\blk ->
     let {ops = Blocks.blockOps binfo blk} in
     let {bid = Blocks.blockId binfo blk} in
-    let {
-     outs = case IntMap.coq_IntMap_lookup bid liveSets of {
-             Prelude.Just ls -> LiveSets.blockLiveOut ls;
-             Prelude.Nothing -> IntMap.emptyIntSet}}
-    in
     case ops of {
      (,) p opse ->
       case p of {
@@ -329,12 +218,24 @@
             State.bind (\opsm' ->
               State.bind (\opse' ->
                 State.bind (\opsm'' ->
-                  State.pure
-                    (Blocks.setBlockOps binfo blk opsb' opsm'' opse'))
+                  case opsb' of {
+                   [] ->
+                    State.pure
+                      (Blocks.setBlockOps binfo blk opsb' opsm'' opse');
+                   (:) b bs ->
+                    case opse' of {
+                     [] ->
+                      State.pure
+                        (Blocks.setBlockOps binfo blk opsb' opsm'' opse');
+                     (:) e es ->
+                      State.pure
+                        (Blocks.setBlockOps binfo blk ((:) b [])
+                          ((Prelude.++) bs
+                            ((Prelude.++) opsm'' (Seq.belast e es))) ((:)
+                          (Seq.last e es) []))}})
                   (resolveMappings maxReg oinfo bid opsm' mappings))
-                (State.concatMapM (f outs) opse))
-              (State.concatMapM (f outs) opsm))
-            (State.concatMapM (f outs) opsb))
+                (State.concatMapM f opse)) (State.concatMapM f opsm))
+            (State.concatMapM f opsb))
           (State.modify (\assn -> Build_AssnStateInfo (assnOpId assn)
             ((Prelude.+) (assnOpId assn)
               (Ssrnat.double (Data.List.length opsb)))
@@ -344,22 +245,12 @@
             (assnAcc assn)))}})
 
 assignRegNum :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->
-                (Blocks.OpInfo a5 a3 a4) -> ScanState.ScanStateDesc ->
+                (Blocks.OpInfo a5 a3 a4) -> ([] Resolve.Allocation) ->
                 (IntMap.IntMap LiveSets.BlockLiveSets) -> (IntMap.IntMap
                 Resolve.BlockMoves) -> ([] a1) -> a5 -> (,) ([] a2) a5
-assignRegNum maxReg binfo oinfo sd liveSets mappings blocks acc =
-  case considerOps maxReg binfo oinfo
-         (doAllocations maxReg oinfo
-           (Prelude.map (\x -> (,)
-             (Interval.getIntervalDesc
-               (
-                 (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)
-                   (ScanState.intervals maxReg sd) (Prelude.fst x))))
-             (Prelude.snd x))
-             ((Prelude.++) (ScanState.handled maxReg sd)
-               ((Prelude.++) (ScanState.active maxReg sd)
-                 (ScanState.inactive maxReg sd))))) liveSets mappings blocks
-         (Build_AssnStateInfo ((Prelude.succ) 0) ((Prelude.succ) 0)
-         ((Prelude.succ) 0) acc) of {
+assignRegNum maxReg binfo oinfo allocs liveSets mappings blocks acc =
+  case considerOps maxReg binfo oinfo (doAllocations maxReg oinfo allocs)
+         liveSets mappings blocks (Build_AssnStateInfo ((Prelude.succ) 0)
+         ((Prelude.succ) 0) ((Prelude.succ) 0) acc) of {
    (,) blocks' assn -> (,) blocks' (assnAcc assn)}
 
diff --git a/LinearScan/Blocks.hs b/LinearScan/Blocks.hs
--- a/LinearScan/Blocks.hs
+++ b/LinearScan/Blocks.hs
@@ -1,6 +1,3 @@
-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}
-{- For Hugs, use the option -F"cpp -P -traditional" -}
-
 module LinearScan.Blocks where
 
 
@@ -13,97 +10,22 @@
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
-import qualified LinearScan.Eqtype as Eqtype
-import qualified LinearScan.Ssrbool as Ssrbool
-
+import qualified LinearScan.UsePos as UsePos
 
 
---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
-
 type PhysReg = Prelude.Int
 
-data VarKind =
-   Input
- | Temp
- | Output
-
-eqVarKind :: VarKind -> VarKind -> Prelude.Bool
-eqVarKind s1 s2 =
-  case s1 of {
-   Input ->
-    case s2 of {
-     Input -> Prelude.True;
-     _ -> Prelude.False};
-   Temp ->
-    case s2 of {
-     Temp -> Prelude.True;
-     _ -> Prelude.False};
-   Output ->
-    case s2 of {
-     Output -> Prelude.True;
-     _ -> Prelude.False}}
-
-eqVarKindP :: Eqtype.Equality__Coq_axiom VarKind
-eqVarKindP b1 b2 =
-  let {
-   _evar_0_ = let {_evar_0_ = Ssrbool.ReflectT} in
-              let {_evar_0_0 = Ssrbool.ReflectF} in
-              let {_evar_0_1 = Ssrbool.ReflectF} in
-              case b2 of {
-               Input -> _evar_0_;
-               Temp -> _evar_0_0;
-               Output -> _evar_0_1}}
-  in
-  let {
-   _evar_0_0 = let {_evar_0_0 = Ssrbool.ReflectF} in
-               let {_evar_0_1 = Ssrbool.ReflectT} in
-               let {_evar_0_2 = Ssrbool.ReflectF} in
-               case b2 of {
-                Input -> _evar_0_0;
-                Temp -> _evar_0_1;
-                Output -> _evar_0_2}}
-  in
-  let {
-   _evar_0_1 = let {_evar_0_1 = Ssrbool.ReflectF} in
-               let {_evar_0_2 = Ssrbool.ReflectF} in
-               let {_evar_0_3 = Ssrbool.ReflectT} in
-               case b2 of {
-                Input -> _evar_0_1;
-                Temp -> _evar_0_2;
-                Output -> _evar_0_3}}
-  in
-  case b1 of {
-   Input -> _evar_0_;
-   Temp -> _evar_0_0;
-   Output -> _evar_0_1}
-
-coq_VarKind_eqMixin :: Eqtype.Equality__Coq_mixin_of VarKind
-coq_VarKind_eqMixin =
-  Eqtype.Equality__Mixin eqVarKind eqVarKindP
-
-coq_VarKind_eqType :: Eqtype.Equality__Coq_type
-coq_VarKind_eqType =
-  unsafeCoerce coq_VarKind_eqMixin
-
 type VarId = Prelude.Int
 
 data VarInfo =
-   Build_VarInfo (Prelude.Either PhysReg VarId) VarKind Prelude.Bool
+   Build_VarInfo (Prelude.Either PhysReg VarId) UsePos.VarKind Prelude.Bool
 
 varId :: Prelude.Int -> VarInfo -> Prelude.Either PhysReg VarId
 varId maxReg v =
   case v of {
    Build_VarInfo varId0 varKind0 regRequired0 -> varId0}
 
-varKind :: Prelude.Int -> VarInfo -> VarKind
+varKind :: Prelude.Int -> VarInfo -> UsePos.VarKind
 varKind maxReg v =
   case v of {
    Build_VarInfo varId0 varKind0 regRequired0 -> varKind0}
@@ -123,9 +45,9 @@
    IsNormal
  | IsCall
  | IsBranch
- | IsLoopBegin
- | IsLoopEnd
 
+type OpId = Prelude.Int
+
 data OpInfo accType opType1 opType2 =
    Build_OpInfo (opType1 -> OpKind) (opType1 -> [] VarInfo) (PhysReg ->
                                                             PhysReg ->
@@ -139,47 +61,55 @@
                                                              ([] opType2)
                                                              accType) 
  ((Prelude.Maybe VarId) -> PhysReg -> accType -> (,) ([] opType2) accType) 
- (opType1 -> ([] ((,) VarId PhysReg)) -> [] opType2)
+ (opType1 -> ([] ((,) VarId PhysReg)) -> [] opType2) (opType1 ->
+                                                     Prelude.String)
 
 opKind :: Prelude.Int -> (OpInfo a1 a2 a3) -> a2 -> OpKind
 opKind maxReg o =
   case o of {
-   Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0
-    applyAllocs0 -> opKind0}
+   Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0
+    applyAllocs0 showOp -> opKind0}
 
 opRefs :: Prelude.Int -> (OpInfo a1 a2 a3) -> a2 -> [] VarInfo
 opRefs maxReg o =
   case o of {
-   Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0
-    applyAllocs0 -> opRefs0}
+   Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0
+    applyAllocs0 showOp -> opRefs0}
 
 moveOp :: Prelude.Int -> (OpInfo a1 a2 a3) -> PhysReg -> PhysReg -> a1 -> (,)
           ([] a3) a1
 moveOp maxReg o =
   case o of {
-   Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0
-    applyAllocs0 -> moveOp0}
+   Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0
+    applyAllocs0 showOp -> moveOp0}
 
+swapOp :: Prelude.Int -> (OpInfo a1 a2 a3) -> PhysReg -> PhysReg -> a1 -> (,)
+          ([] a3) a1
+swapOp maxReg o =
+  case o of {
+   Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0
+    applyAllocs0 showOp -> swapOp0}
+
 saveOp :: Prelude.Int -> (OpInfo a1 a2 a3) -> PhysReg -> (Prelude.Maybe
           VarId) -> a1 -> (,) ([] a3) a1
 saveOp maxReg o =
   case o of {
-   Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0
-    applyAllocs0 -> saveOp0}
+   Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0
+    applyAllocs0 showOp -> saveOp0}
 
 restoreOp :: Prelude.Int -> (OpInfo a1 a2 a3) -> (Prelude.Maybe VarId) ->
              PhysReg -> a1 -> (,) ([] a3) a1
 restoreOp maxReg o =
   case o of {
-   Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0
-    applyAllocs0 -> restoreOp0}
+   Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0
+    applyAllocs0 showOp -> restoreOp0}
 
 applyAllocs :: Prelude.Int -> (OpInfo a1 a2 a3) -> a2 -> ([]
                ((,) VarId PhysReg)) -> [] a3
 applyAllocs maxReg o =
   case o of {
-   Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0
-    applyAllocs0 -> applyAllocs0}
+   Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0
+    applyAllocs0 showOp -> applyAllocs0}
 
 type BlockId = Prelude.Int
 
@@ -230,8 +160,6 @@
 blockSize :: (BlockInfo a1 a2 a3 a4) -> a1 -> Prelude.Int
 blockSize binfo block =
   Data.List.length (allBlockOps binfo block)
-
-type OpId = Prelude.Int
 
 foldOps :: (BlockInfo a1 a2 a3 a4) -> (a5 -> a3 -> a5) -> a5 -> ([] a1) -> a5
 foldOps binfo f z =
diff --git a/LinearScan/Build.hs b/LinearScan/Build.hs
--- a/LinearScan/Build.hs
+++ b/LinearScan/Build.hs
@@ -19,10 +19,13 @@
 import qualified LinearScan.Interval as Interval
 import qualified LinearScan.Lib as Lib
 import qualified LinearScan.LiveSets as LiveSets
+import qualified LinearScan.Logic as Logic
+import qualified LinearScan.Loops as Loops
 import qualified LinearScan.Morph as Morph
 import qualified LinearScan.NonEmpty0 as NonEmpty0
 import qualified LinearScan.Range as Range
 import qualified LinearScan.ScanState as ScanState
+import qualified LinearScan.Specif as Specif
 import qualified LinearScan.UsePos as UsePos
 import qualified LinearScan.Eqtype as Eqtype
 import qualified LinearScan.Fintype as Fintype
@@ -52,206 +55,319 @@
 newBuildState n =
   IntMap.emptyIntMap
 
-data RangeCursor =
-   Build_RangeCursor Prelude.Int Range.BoundedRange Range.SortedRanges
-
-emptyRangeCursor :: Prelude.Int -> Prelude.Int -> Prelude.Int -> RangeCursor
-emptyRangeCursor b pos e =
-  (Prelude.flip (Prelude.$)) __ (\_ -> Build_RangeCursor pos
-    (Range.emptyBoundedRange ((Prelude.succ) (Ssrnat.double b))
-      ((Prelude.succ) (Ssrnat.double pos)))
-    (Range.emptySortedRanges ((Prelude.succ) (Ssrnat.double pos))))
-
-transportRangeCursor :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
-                        Prelude.Int -> RangeCursor -> RangeCursor
-transportRangeCursor b prev base e c =
-  let {_evar_0_ = \mid r rs -> Build_RangeCursor mid r rs} in
-  case c of {
-   Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1}
-
-type PendingRanges = (IntMap.IntMap RangeCursor)
+type PendingRanges = [] Range.BoundedRange
 
 emptyPendingRanges :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
-                      Prelude.Int -> IntMap.IntSet -> PendingRanges
-emptyPendingRanges maxReg b pos e liveOuts =
-  (Prelude.flip (Prelude.$)) (emptyRangeCursor b pos e) (\empty ->
-    (Prelude.flip (Prelude.$)) (\xs vid ->
-      IntMap.coq_IntMap_insert ((Prelude.+) vid maxReg) empty xs) (\f ->
-      IntMap.coq_IntSet_foldl f IntMap.emptyIntMap liveOuts))
+                      IntMap.IntSet -> IntMap.IntMap PendingRanges
+emptyPendingRanges maxReg b e liveOuts =
+  (Prelude.flip (Prelude.$)) __ (\_ ->
+    (Prelude.flip (Prelude.$))
+      (Range.emptyBoundedRange ((Prelude.succ) (Ssrnat.double b))
+        ((Prelude.succ) (Ssrnat.double e))) (\empty ->
+      (Prelude.flip (Prelude.$)) (\xs vid ->
+        IntMap.coq_IntMap_insert ((Prelude.+) vid maxReg) ((:[]) empty) xs)
+        (\f -> IntMap.coq_IntSet_foldl f IntMap.emptyIntMap liveOuts)))
 
-mergeIntoSortedRanges :: Prelude.Int -> Prelude.Int -> PendingRanges ->
-                         (IntMap.IntMap Range.SortedRanges) -> IntMap.IntMap
-                         Range.SortedRanges
-mergeIntoSortedRanges b pos pmap rmap =
-  IntMap.coq_IntMap_mergeWithKey (\_the_1st_wildcard_ _top_assumption_ ->
-    let {
-     _evar_0_ = \mid br ps rs ->
+coq_BoundedRange_leq :: Prelude.Int -> Prelude.Int -> Range.BoundedRange ->
+                        Range.BoundedRange -> Prelude.Bool
+coq_BoundedRange_leq b e x y =
+  let {_evar_0_ = (Prelude.<=) (Range.rbeg x) (Range.rbeg y)} in
+  let {_evar_0_0 = (Prelude.<=) (Range.rend x) (Range.rend y)} in
+  case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Range.rend x))
+         (unsafeCoerce (Range.rend y)) of {
+   Prelude.True -> _evar_0_;
+   Prelude.False -> _evar_0_0}
+
+compilePendingRanges :: Prelude.Int -> Prelude.Int -> ([] Range.BoundedRange)
+                        -> Specif.Coq_sig2 Range.SortedRanges
+compilePendingRanges b e ranges =
+  let {_evar_0_ = \_ -> []} in
+  let {
+   _evar_0_0 = \r1 rs iHrs ->
+    case rs of {
+     [] -> (:) ( r1) [];
+     (:) r2 rs2 ->
       (Prelude.flip (Prelude.$)) __ (\_ ->
+        let {iHrs0 = iHrs __} in
+        let {_evar_0_0 = \_ _ _ _ _ -> Logic.coq_False_rec} in
         let {
-         ps' = Range.prependRange ((Prelude.succ) (Ssrnat.double b))
-                 ((Prelude.succ) (Ssrnat.double mid)) br ps ((Prelude.succ)
-                 (Ssrnat.double b))}
+         _evar_0_1 = \r2' rs2' ->
+          let {_evar_0_1 = \_ -> (:) ( r1) ((:) r2' rs2')} in
+          let {
+           _evar_0_2 = \_ -> (:)
+            (Range.packRange (Range.Build_RangeDesc
+              (Prelude.min (Range.rbeg (Range.getRangeDesc r1))
+                (Range.rbeg (Range.getRangeDesc r2')))
+              (Prelude.max (Range.rend (Range.getRangeDesc r1))
+                (Range.rend (Range.getRangeDesc r2')))
+              (Lib.sortBy UsePos.upos_le
+                ((Prelude.++) (Range.ups (Range.getRangeDesc r1))
+                  (Range.ups (Range.getRangeDesc r2')))))) rs2'}
+          in
+          case Range.range_ltn ( r1) r2' of {
+           Prelude.True -> _evar_0_1 __;
+           Prelude.False -> _evar_0_2 __}}
         in
-        Prelude.Just
-        (Range.coq_SortedRanges_cat ((Prelude.succ) (Ssrnat.double b)) ps'
-          ((Prelude.succ) (Ssrnat.double pos)) rs))}
-    in
-    (\rs ->
-    case _top_assumption_ of {
-     Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1 rs}))
-    (IntMap.coq_IntMap_map (\_top_assumption_ ->
-      let {
-       _evar_0_ = \_cursorMid_ br rs ->
-        (Prelude.flip (Prelude.$)) __ (\_ ->
-          
-            (Range.prependRange ((Prelude.succ) (Ssrnat.double b))
-              ((Prelude.succ) (Ssrnat.double _cursorMid_)) br rs
-              ((Prelude.succ) (Ssrnat.double b))))}
-      in
-      case _top_assumption_ of {
-       Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1}))
-    (IntMap.coq_IntMap_map
-      (Range.transportSortedRanges ((Prelude.succ) (Ssrnat.double b))
-        ((Prelude.succ) (Ssrnat.double pos)))) ( pmap) rmap
+        case iHrs0 of {
+         [] -> _evar_0_0 __ __ __ __ __;
+         (:) x x0 -> _evar_0_1 x x0})}}
+  in
+  Datatypes.list_rec _evar_0_ (\r1 rs iHrs _ -> _evar_0_0 r1 rs iHrs) ranges
+    __
 
-varKindLtn :: Blocks.VarKind -> Blocks.VarKind -> Prelude.Bool
-varKindLtn x y =
-  case x of {
-   Blocks.Input ->
-    case y of {
-     Blocks.Input -> Prelude.False;
-     _ -> Prelude.True};
-   Blocks.Temp ->
-    case y of {
-     Blocks.Output -> Prelude.True;
-     _ -> Prelude.False};
-   Blocks.Output -> Prelude.False}
+rangesToBoundedRanges :: Prelude.Int -> Prelude.Int -> Range.RangeDesc -> ([]
+                         Range.RangeDesc) -> [] Range.BoundedRange
+rangesToBoundedRanges b e y ys =
+  case ys of {
+   [] -> (:[]) ( y);
+   (:) z zs -> (:) ( y) (rangesToBoundedRanges b e z zs)}
 
-handleVars_combine :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
-                      Prelude.Int -> RangeCursor -> ((,) Prelude.Bool
-                      ([] Blocks.VarKind)) -> Prelude.Maybe RangeCursor
-handleVars_combine b pos e vid range vars =
+compressPendingRanges :: Prelude.Int -> Prelude.Int -> PendingRanges ->
+                         PendingRanges
+compressPendingRanges b e ranges =
+  let {_evar_0_ = \r -> (:[]) r} in
   let {
-   _evar_0_ = \mid br srs ->
+   _evar_0_0 = \r rs ->
     let {
-     _evar_0_ = \req kinds ->
+     _evar_0_0 = \_ ->
       let {
-       upos = UsePos.Build_UsePos ((Prelude.succ) (Ssrnat.double pos)) req}
+       _top_assumption_ = compilePendingRanges b e
+                            (Lib.insert (coq_BoundedRange_leq b e) r
+                              (Lib.sortBy (coq_BoundedRange_leq b e) ( rs)))}
       in
-      (Prelude.flip (Prelude.$)) __ (\_ ->
+      let {
+       _evar_0_0 = \_ _ ->
         (Prelude.flip (Prelude.$)) __ (\_ ->
-          (Prelude.flip (Prelude.$)) __ (\_ ->
-            let {
-             _evar_0_ = \_ ->
-              (Prelude.flip (Prelude.$)) __ (\_ ->
-                let {
-                 r2 = Range.coq_Range_cons upos (Range.Build_RangeDesc
-                        ((Prelude.succ) (Ssrnat.double pos))
-                        (Range.rend ( br)) (Range.ups ( br)))}
-                in
-                Prelude.Just (Build_RangeCursor mid r2 srs))}
-            in
-            let {
-             _evar_0_0 = \_ ->
-              let {
-               _evar_0_0 = \_ ->
-                (Prelude.flip (Prelude.$)) __ (\_ ->
-                  let {r1 = Range.coq_Range_cons upos ( ( br))} in
-                  Prelude.Just (Build_RangeCursor mid r1 srs))}
-              in
-              let {
-               _evar_0_1 = \_ ->
-                let {r1 = Range.newRange upos} in
-                let {
-                 _evar_0_1 = \_ ->
-                  (Prelude.flip (Prelude.$)) __ (\_ -> Prelude.Just
-                    (Build_RangeCursor ((Prelude.succ) pos) r1
-                    (
-                      (Range.prependRange ((Prelude.succ) (Ssrnat.double b))
-                        ((Prelude.succ) (Ssrnat.double mid)) br srs
-                        ((Prelude.succ)
-                        (Ssrnat.double ((Prelude.succ) pos)))))))}
-                in
-                 _evar_0_1 __}
-              in
-              case (Prelude.<=) (Range.rbeg ( ( br))) (UsePos.uloc upos) of {
-               Prelude.True -> _evar_0_0 __;
-               Prelude.False -> _evar_0_1 __}}
-            in
-            case (Prelude.&&)
-                   (Ssrbool.in_mem (unsafeCoerce Blocks.Output)
-                     (Ssrbool.mem
-                       (Seq.seq_predType Blocks.coq_VarKind_eqType) kinds))
-                   (Prelude.not
-                     (Ssrbool.in_mem (unsafeCoerce Blocks.Input)
-                       (Ssrbool.mem
-                         (Seq.seq_predType Blocks.coq_VarKind_eqType) kinds))) of {
-             Prelude.True -> _evar_0_ __;
-             Prelude.False -> _evar_0_0 __})))}
+          let {_evar_0_0 = \_ -> rs} in  _evar_0_0 __)}
+      in
+      let {
+       _evar_0_1 = \x xs ->
+        case _top_assumption_ of {
+         [] -> Logic.coq_False_rec;
+         (:) y ys -> rangesToBoundedRanges b e y ys}}
+      in
+      case Lib.insert (coq_BoundedRange_leq b e) r
+             (Lib.sortBy (coq_BoundedRange_leq b e) ( rs)) of {
+       [] -> _evar_0_0 __ __;
+       (:) x x0 -> _evar_0_1 x x0}}
     in
-    case vars of {
-     (,) x x0 -> unsafeCoerce _evar_0_ x x0}}
+     _evar_0_0 __}
   in
+  (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
+    (\x ->
+    _evar_0_ x)
+    (\x x0 ->
+    _evar_0_0 x x0)
+    ranges
+
+mergeIntoSortedRanges :: Prelude.Int -> Prelude.Int -> (IntMap.IntMap
+                         PendingRanges) -> (IntMap.IntMap Range.SortedRanges)
+                         -> IntMap.IntMap Range.SortedRanges
+mergeIntoSortedRanges b e pmap rmap =
+  IntMap.coq_IntMap_mergeWithKey (\_the_1st_wildcard_ brs srs2 ->
+    let {
+     _top_assumption_ = compilePendingRanges b e
+                          (Lib.sortBy (coq_BoundedRange_leq b e) ( brs))}
+    in
+    Prelude.Just
+    (Range.coq_SortedRanges_cat ((Prelude.succ) (Ssrnat.double b))
+      _top_assumption_ ((Prelude.succ) (Ssrnat.double e)) srs2))
+    (IntMap.coq_IntMap_map (\brs ->
+      compilePendingRanges b e (Lib.sortBy (coq_BoundedRange_leq b e) ( brs))))
+    (\sr ->
+    (Prelude.flip (Prelude.$)) __ (\_ ->
+      IntMap.coq_IntMap_map
+        (Range.transportSortedRanges ((Prelude.succ) (Ssrnat.double b))
+          ((Prelude.succ) (Ssrnat.double e))) sr)) pmap rmap
+
+upos_before_rend :: Range.RangeDesc -> UsePos.UsePos -> Prelude.Bool
+upos_before_rend rd upos =
+  case Range.ups rd of {
+   [] ->
+    case UsePos.uvar upos of {
+     UsePos.Input -> (Prelude.<=) (UsePos.uloc upos) (Range.rend rd);
+     _ -> (Prelude.<=) ((Prelude.succ) (UsePos.uloc upos)) (Range.rend rd)};
+   (:) u l ->
+    case (Prelude.&&)
+           (Prelude.not
+             (Eqtype.eq_op UsePos.coq_VarKind_eqType
+               (unsafeCoerce (UsePos.uvar upos)) (unsafeCoerce UsePos.Input)))
+           (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (UsePos.uloc u))
+             (unsafeCoerce (Range.rend rd))) of {
+     Prelude.True ->
+      (Prelude.<=) ((Prelude.succ) (UsePos.uloc upos)) (UsePos.uloc u);
+     Prelude.False -> (Prelude.<=) (UsePos.uloc upos) (UsePos.uloc u)}}
+
+makeNewRange :: Prelude.Int -> Prelude.Int -> Prelude.Int -> UsePos.UsePos ->
+                Range.BoundedRange
+makeNewRange b pos e upos =
+  Range.Build_RangeDesc
+    (case UsePos.uvar upos of {
+      UsePos.Input -> (Prelude.succ) (Ssrnat.double b);
+      _ -> (Prelude.succ) (Ssrnat.double pos)})
+    (case UsePos.uvar upos of {
+      UsePos.Input -> (Prelude.succ) (Ssrnat.double pos);
+      UsePos.Temp -> (Prelude.succ) ((Prelude.succ) (Ssrnat.double pos));
+      UsePos.Output -> (Prelude.succ) (Ssrnat.double e)}) ((:) upos [])
+
+makeUsePos :: Prelude.Int -> Prelude.Int -> Blocks.VarInfo -> Specif.Coq_sig2
+              UsePos.UsePos
+makeUsePos maxReg pos var =
+  let {
+   upos = UsePos.Build_UsePos ((Prelude.succ) (Ssrnat.double pos))
+    (Blocks.regRequired maxReg var) (Blocks.varKind maxReg var)}
+  in
+  (Prelude.flip (Prelude.$)) __ (\_ -> upos)
+
+handleOutputVar :: Prelude.Int -> Prelude.Int -> Prelude.Int -> Prelude.Int
+                   -> (Prelude.Maybe PendingRanges) -> Blocks.VarInfo ->
+                   Prelude.Maybe PendingRanges
+handleOutputVar maxReg b pos e range var =
+  let {_top_assumption_ = makeUsePos maxReg pos var} in
+  let {
+   _evar_0_ = \range0 ->
+    (Prelude.flip (Prelude.$))
+      (let {_top_assumption_0 = Prelude.head range0} in
+       let {
+        _evar_0_ = \_ ->
+         let {
+          r1 = Range.coq_Range_shift ( _top_assumption_0)
+                 (UsePos.uloc _top_assumption_)}
+         in
+         (Prelude.flip (Prelude.$)) __ (\_ -> r1)}
+       in
+       let {
+        _evar_0_0 = \_ ->
+         let {_evar_0_0 = \_ -> _top_assumption_0} in  _evar_0_0 __}
+       in
+       case (Prelude.<=) ((Prelude.succ) (UsePos.uloc _top_assumption_))
+              (Range.head_or_end ( _top_assumption_0)) of {
+        Prelude.True -> _evar_0_ __;
+        Prelude.False -> _evar_0_0 __}) (\res ->
+      let {
+       _evar_0_ = \_ ->
+        (Prelude.flip (Prelude.$))
+          (Range.coq_Range_cons _top_assumption_ ( res)) (\br ->
+          let {_evar_0_ = \_the_1st_wildcard_ -> Prelude.Just ((:[]) br)} in
+          let {
+           _evar_0_0 = \_the_2nd_wildcard_ rs -> Prelude.Just
+            (NonEmpty0.coq_NE_from_list br ( rs))}
+          in
+          (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
+            (\x ->
+            _evar_0_ x)
+            (\x x0 ->
+            _evar_0_0 x x0)
+            range0)}
+      in
+      let {
+       _evar_0_0 = \_ -> Prelude.Just
+        (NonEmpty0.coq_NE_from_list (makeNewRange b pos e _top_assumption_)
+          ( range0))}
+      in
+      case upos_before_rend ( res) _top_assumption_ of {
+       Prelude.True -> _evar_0_ __;
+       Prelude.False -> _evar_0_0 __})}
+  in
+  let {
+   _evar_0_0 = Prelude.Just ((:[]) (makeNewRange b pos e _top_assumption_))}
+  in
   case range of {
-   Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1}
+   Prelude.Just x -> _evar_0_ x;
+   Prelude.Nothing -> _evar_0_0}
 
+handleVar :: Prelude.Int -> Prelude.Int -> Prelude.Int -> Prelude.Int ->
+             (Prelude.Maybe PendingRanges) -> Blocks.VarInfo -> Prelude.Maybe
+             PendingRanges
+handleVar maxReg b pos e range var =
+  let {_top_assumption_ = makeUsePos maxReg pos var} in
+  let {
+   _evar_0_ = \range0 -> Prelude.Just
+    (NonEmpty0.coq_NE_from_list (makeNewRange b pos e _top_assumption_)
+      ( range0))}
+  in
+  let {
+   _evar_0_0 = Prelude.Just ((:[]) (makeNewRange b pos e _top_assumption_))}
+  in
+  case range of {
+   Prelude.Just x -> _evar_0_ x;
+   Prelude.Nothing -> _evar_0_0}
+
+handleVars_combine :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
+                      Prelude.Int -> Prelude.Int -> ([] Blocks.VarInfo) ->
+                      PendingRanges -> Prelude.Maybe PendingRanges
+handleVars_combine maxReg b pos e vid vars c1 =
+  (Prelude.flip (Prelude.$)) __ (\_ ->
+    (Prelude.flip (Prelude.$)) (compressPendingRanges b e c1) (\c2 ->
+      (Prelude.flip (Prelude.$))
+        (Data.List.foldl' (handleOutputVar maxReg b pos e) (Prelude.Just c2)
+          (Prelude.filter (\k ->
+            Eqtype.eq_op UsePos.coq_VarKind_eqType
+              (unsafeCoerce (Blocks.varKind maxReg k))
+              (unsafeCoerce UsePos.Output)) vars)) (\c3 ->
+        (Prelude.flip (Prelude.$))
+          (Data.List.foldl' (handleVar maxReg b pos e) c3
+            (Prelude.filter (\k ->
+              Prelude.not
+                (Eqtype.eq_op UsePos.coq_VarKind_eqType
+                  (unsafeCoerce (Blocks.varKind maxReg k))
+                  (unsafeCoerce UsePos.Output))) vars)) (\c4 -> c4))))
+
 handleVars_onlyRanges :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
-                         (IntMap.IntMap RangeCursor) -> IntMap.IntMap
-                         RangeCursor
-handleVars_onlyRanges b pos e =
-  IntMap.coq_IntMap_map (transportRangeCursor b ((Prelude.succ) pos) pos e)
+                         (IntMap.IntMap PendingRanges) -> IntMap.IntMap
+                         PendingRanges
+handleVars_onlyRanges b pos e h0 =
+  h0
 
 handleVars_onlyVars :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
-                       (IntMap.IntMap ((,) Prelude.Bool ([] Blocks.VarKind)))
-                       -> IntMap.IntMap RangeCursor
-handleVars_onlyVars b pos e =
-  IntMap.coq_IntMap_map (\_top_assumption_ ->
-    let {
-     _evar_0_ = \req kinds ->
-      let {
-       rd = Range.Build_RangeDesc
-        (case Ssrbool.in_mem (unsafeCoerce Blocks.Input)
-                (Ssrbool.mem (Seq.seq_predType Blocks.coq_VarKind_eqType)
-                  kinds) of {
-          Prelude.True -> (Prelude.succ) (Ssrnat.double b);
-          Prelude.False -> (Prelude.succ) (Ssrnat.double pos)})
-        (case Ssrbool.in_mem (unsafeCoerce Blocks.Output)
-                (Ssrbool.mem (Seq.seq_predType Blocks.coq_VarKind_eqType)
-                  kinds) of {
-          Prelude.True -> (Prelude.succ) (Ssrnat.double e);
-          Prelude.False -> (Prelude.succ) ((Prelude.succ)
-           (Ssrnat.double pos))}) ((:) (UsePos.Build_UsePos ((Prelude.succ)
-        (Ssrnat.double pos)) req) [])}
-      in
-      Build_RangeCursor e rd []}
-    in
-    case _top_assumption_ of {
-     (,) x x0 -> unsafeCoerce _evar_0_ x x0})
+                       Prelude.Int -> (IntMap.IntMap ([] Blocks.VarInfo)) ->
+                       IntMap.IntMap PendingRanges
+handleVars_onlyVars maxReg b pos e =
+  IntMap.coq_IntMap_foldlWithKey (\m vid vars ->
+    (Prelude.flip (Prelude.$))
+      (Data.List.foldl' (handleOutputVar maxReg b pos e) Prelude.Nothing
+        (Prelude.filter (\k ->
+          Eqtype.eq_op UsePos.coq_VarKind_eqType
+            (unsafeCoerce (Blocks.varKind maxReg k))
+            (unsafeCoerce UsePos.Output)) vars)) (\c2 ->
+      (Prelude.flip (Prelude.$))
+        (Data.List.foldl' (handleVar maxReg b pos e) c2
+          (Prelude.filter (\k ->
+            Prelude.not
+              (Eqtype.eq_op UsePos.coq_VarKind_eqType
+                (unsafeCoerce (Blocks.varKind maxReg k))
+                (unsafeCoerce UsePos.Output))) vars)) (\c3 ->
+        let {_evar_0_ = \c4 -> IntMap.coq_IntMap_insert vid c4 m} in
+        case c3 of {
+         Prelude.Just x -> _evar_0_ x;
+         Prelude.Nothing -> m}))) IntMap.emptyIntMap
 
-extractVarInfo :: Prelude.Int -> ([] Blocks.VarInfo) -> (,) Prelude.Bool
-                  ([] Blocks.VarKind)
+extractVarInfo :: Prelude.Int -> ([] Blocks.VarInfo) -> [] Blocks.VarInfo
 extractVarInfo maxReg xs =
-  (,)
-    (Prelude.not
-      (Eqtype.eq_op Ssrnat.nat_eqType
-        (unsafeCoerce (Seq.find (Blocks.regRequired maxReg) xs))
-        (unsafeCoerce (Data.List.length xs))))
-    (Lib.sortBy varKindLtn (Prelude.map (\v -> Blocks.varKind maxReg v) xs))
+  let {_evar_0_ = \x -> (:) x []} in
+  let {_evar_0_0 = \x xs0 -> (:) x ( xs0)} in
+  (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
+    (\x ->
+    _evar_0_ x)
+    (\x x0 ->
+    _evar_0_0 x x0)
+    xs
 
 handleVars :: Prelude.Int -> ([] Blocks.VarInfo) -> Prelude.Int ->
-              Prelude.Int -> Prelude.Int -> PendingRanges -> PendingRanges
+              Prelude.Int -> Prelude.Int -> (IntMap.IntMap PendingRanges) ->
+              IntMap.IntMap PendingRanges
 handleVars maxReg varRefs b pos e ranges =
   let {
    vars = IntMap.coq_IntMap_map (extractVarInfo maxReg)
             (IntMap.coq_IntMap_groupOn (Blocks.nat_of_varId maxReg) varRefs)}
   in
-  IntMap.coq_IntMap_mergeWithKey (handleVars_combine b pos e)
-    (handleVars_onlyRanges b pos e) (handleVars_onlyVars b pos e) ( ranges)
-    vars
+  IntMap.coq_IntMap_mergeWithKey (handleVars_combine maxReg b pos e)
+    (handleVars_onlyVars maxReg b pos e) (handleVars_onlyRanges b pos e) vars
+    ranges
 
 reduceOp :: Prelude.Int -> (Blocks.OpInfo a4 a2 a3) -> Prelude.Int ->
-            Prelude.Int -> Prelude.Int -> a1 -> a2 -> PendingRanges ->
-            PendingRanges
+            Prelude.Int -> Prelude.Int -> a1 -> a2 -> (IntMap.IntMap
+            PendingRanges) -> IntMap.IntMap PendingRanges
 reduceOp maxReg oinfo b pos e block op ranges =
   let {refs = Blocks.opRefs maxReg oinfo op} in
   let {
@@ -260,7 +376,7 @@
              (Prelude.++)
                (Fintype.image_mem (Fintype.ordinal_finType maxReg) (\n ->
                  Blocks.Build_VarInfo (Prelude.Left (unsafeCoerce n))
-                 Blocks.Temp Prelude.True)
+                 UsePos.Temp Prelude.True)
                  (Ssrbool.mem
                    (Seq.seq_predType (Fintype.ordinal_eqType maxReg))
                    (unsafeCoerce (Fintype.ord_enum maxReg)))) refs;
@@ -269,33 +385,31 @@
   handleVars maxReg refs' b pos e ranges
 
 reduceBlock :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->
-               (Blocks.OpInfo a5 a3 a4) -> Prelude.Int -> a1 -> PendingRanges
-               -> PendingRanges
-reduceBlock maxReg binfo oinfo pos block =
+               (Blocks.OpInfo a5 a3 a4) -> Prelude.Int -> Blocks.BlockId ->
+               a1 -> Loops.LoopState -> (IntMap.IntMap IntMap.IntSet) ->
+               (IntMap.IntMap PendingRanges) -> IntMap.IntMap PendingRanges
+reduceBlock maxReg binfo oinfo pos bid block loops varUses =
   let {sz = Blocks.blockSize binfo block} in
   let {e = (Prelude.+) pos sz} in
   let {ops = Blocks.allBlockOps binfo block} in
-  let {
-   _evar_0_ = let {_evar_0_ = let {_evar_0_ = \h -> h} in  _evar_0_} in
-              let {
-               _evar_0_0 = \o os iHos ->
-                let {
-                 _evar_0_0 = \ranges ->
-                  iHos
-                    (reduceOp maxReg oinfo pos
-                      ((Prelude.+) pos (Data.List.length os)) e block o
-                      ranges)}
-                in
-                 _evar_0_0}
-              in
-              Datatypes.list_rec _evar_0_ _evar_0_0 (Seq.rev ops)}
-  in
-   _evar_0_
+  (Prelude.flip (Prelude.$)) __ (\_ ->
+    (Prelude.flip (Prelude.$)) __ (\_ ->
+      let {_evar_0_ = \h0 -> h0} in
+      let {
+       _evar_0_0 = \os o iHos ranges ->
+        (Prelude.flip (Prelude.$)) __ (\_ ->
+          (Prelude.flip (Prelude.$)) __ iHos
+            (reduceOp maxReg oinfo pos
+              ((Prelude.+) pos (Data.List.length os)) e block o ranges))}
+      in
+      Seq.last_ind (\_ h0 -> _evar_0_ h0) (\os o iHos _ ranges ->
+        _evar_0_0 os o iHos ranges) ops __))
 
 reduceBlocks :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->
-                (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> (IntMap.IntMap
+                (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> Loops.LoopState ->
+                (IntMap.IntMap IntMap.IntSet) -> (IntMap.IntMap
                 LiveSets.BlockLiveSets) -> Prelude.Int -> BuildState
-reduceBlocks maxReg binfo oinfo blocks liveSets pos =
+reduceBlocks maxReg binfo oinfo blocks loops varUses liveSets pos =
   let {_evar_0_ = \pos0 -> newBuildState pos0} in
   let {
    _evar_0_0 = \b blocks0 iHbs pos0 ->
@@ -307,14 +421,13 @@
         let {sz = Blocks.blockSize binfo b} in
         let {
          _evar_0_0 = \_ ->
-          let {endpos = (Prelude.+) pos0 sz} in
           (Prelude.flip (Prelude.$)) __ (\_ ->
-            (Prelude.flip (Prelude.$)) __ (\_ ->
-              (Prelude.flip (Prelude.$))
-                (reduceBlock maxReg binfo oinfo pos0 b
-                  (emptyPendingRanges maxReg pos0 endpos endpos outs))
-                (\pending ->
-                mergeIntoSortedRanges pos0 endpos pending (iHbs endpos))))}
+            (Prelude.flip (Prelude.$))
+              (reduceBlock maxReg binfo oinfo pos0 bid b loops varUses
+                (emptyPendingRanges maxReg pos0 ((Prelude.+) pos0 sz) outs))
+              (\pending ->
+              mergeIntoSortedRanges pos0 ((Prelude.+) pos0 sz) pending
+                (iHbs ((Prelude.+) pos0 sz))))}
         in
         let {_evar_0_1 = \_ -> iHbs pos0} in
         case (Prelude.<=) ((Prelude.succ) 0) sz of {
@@ -341,7 +454,7 @@
                 ( (Prelude.head (NonEmpty0.coq_NE_from_list _a_ _l_))))
               (Range.rend
                 ( (Prelude.last (NonEmpty0.coq_NE_from_list _a_ _l_))))
-              Interval.Whole (NonEmpty0.coq_NE_from_list _a_ _l_))))) vars}
+              (NonEmpty0.coq_NE_from_list _a_ _l_))))) vars}
         in
         let {
          _evar_0_1 = \_ ->
@@ -353,7 +466,7 @@
                   ( (Prelude.head (NonEmpty0.coq_NE_from_list _a_ _l_))))
                 (Range.rend
                   ( (Prelude.last (NonEmpty0.coq_NE_from_list _a_ _l_))))
-                Interval.Whole (NonEmpty0.coq_NE_from_list _a_ _l_))) vars))}
+                (NonEmpty0.coq_NE_from_list _a_ _l_))) vars))}
         in
         case (Prelude.<=) ((Prelude.succ) vid) maxReg of {
          Prelude.True -> _evar_0_0 __;
@@ -368,12 +481,12 @@
     (Data.List.replicate maxReg Prelude.Nothing) IntMap.emptyIntMap) bs
 
 buildIntervals :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->
-                  (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> (IntMap.IntMap
-                  LiveSets.BlockLiveSets) -> Prelude.Either Morph.SSError
-                  ScanState.ScanStateSig
-buildIntervals maxReg binfo oinfo blocks liveSets =
+                  (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> Loops.LoopState ->
+                  (IntMap.IntMap LiveSets.BlockLiveSets) -> Prelude.Either
+                  Morph.SSError ScanState.ScanStateSig
+buildIntervals maxReg binfo oinfo blocks loops liveSets =
   let {
-   handleVar = \ss i ->
+   add_unhandled_interval = \ss i ->
     ScanState.packScanState maxReg ScanState.Pending
       (ScanState.Build_ScanStateDesc ((Prelude.succ)
       (ScanState.nextInterval maxReg ( ss)))
@@ -393,8 +506,14 @@
       (ScanState.Build_ScanStateDesc 0 []
       (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []));
    (:) b bs ->
-    let {bs0 = reduceBlocks maxReg binfo oinfo ((:) b bs) liveSets 0} in
-    case compileIntervals maxReg 0 bs0 of {
+    let {
+     varUses = Loops.computeVarReferences maxReg binfo oinfo ((:) b bs) loops}
+    in
+    let {
+     reduced = reduceBlocks maxReg binfo oinfo ((:) b bs) loops varUses
+                 liveSets 0}
+    in
+    case compileIntervals maxReg 0 reduced of {
      (,) regs vars ->
       let {
        s2 = ScanState.packScanState maxReg ScanState.Pending
@@ -413,6 +532,6 @@
               (ScanState.handled maxReg (ScanState.Build_ScanStateDesc 0 []
                 (Data.List.replicate maxReg Prelude.Nothing) [] [] [] [])))}
       in
-      let {s3 = IntMap.coq_IntMap_foldl handleVar s2 vars} in
+      let {s3 = IntMap.coq_IntMap_foldl add_unhandled_interval s2 vars} in
       Prelude.Right (ScanState.packScanState maxReg ScanState.InUse ( s3))}}
 
diff --git a/LinearScan/Eqtype.hs b/LinearScan/Eqtype.hs
--- a/LinearScan/Eqtype.hs
+++ b/LinearScan/Eqtype.hs
@@ -119,11 +119,6 @@
 s2val u =
   u
 
-sig_subType :: (Ssrbool.Coq_pred a1) -> Coq_subType a1
-sig_subType p =
-  SubType (unsafeCoerce ) (unsafeCoerce (\x _ -> x)) (\_ k_S u ->
-    k_S (unsafeCoerce u) __)
-
 inj_eqAxiom :: Equality__Coq_type -> (a1 -> Equality__Coq_sort) ->
                Equality__Coq_axiom a1
 inj_eqAxiom eT f x y =
@@ -145,17 +140,6 @@
            (Coq_sub_sort Equality__Coq_sort)
 val_eqP t p sT =
   inj_eqAxiom t (val p sT)
-
-sig_eqMixin :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) ->
-               Equality__Coq_mixin_of Equality__Coq_sort
-sig_eqMixin t p =
-  Equality__Mixin (\x y -> eq_op t ( x) ( y))
-    (unsafeCoerce (val_eqP t (\x -> p x) (sig_subType p)))
-
-sig_eqType :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) ->
-              Equality__Coq_type
-sig_eqType t p =
-  unsafeCoerce (sig_eqMixin t p)
 
 pair_eq :: Equality__Coq_type -> Equality__Coq_type -> Ssrbool.Coq_simpl_rel
            ((,) Equality__Coq_sort Equality__Coq_sort)
diff --git a/LinearScan/IntMap.hs b/LinearScan/IntMap.hs
--- a/LinearScan/IntMap.hs
+++ b/LinearScan/IntMap.hs
@@ -42,6 +42,14 @@
 emptyIntMap =
   []
 
+coq_IntMap_fromList :: ([] ((,) Prelude.Int a1)) -> IntMap a1
+coq_IntMap_fromList x =
+  x
+
+coq_IntMap_size :: (IntMap a1) -> Prelude.Int
+coq_IntMap_size m =
+  Data.List.length m
+
 coq_IntMap_lookup :: Prelude.Int -> (IntMap a1) -> Prelude.Maybe a1
 coq_IntMap_lookup k m =
   Lib.maybeLookup Ssrnat.nat_eqType (unsafeCoerce m) (unsafeCoerce k)
@@ -91,6 +99,10 @@
 coq_IntMap_foldlWithKey f z m =
   Data.List.foldl' (\acc x -> f acc (Prelude.fst x) (Prelude.snd x)) z m
 
+coq_IntMap_toList :: (IntMap a1) -> [] ((,) Prelude.Int a1)
+coq_IntMap_toList m =
+  m
+
 eqIntMap :: Eqtype.Equality__Coq_type -> (IntMap Eqtype.Equality__Coq_sort)
             -> (IntMap Eqtype.Equality__Coq_sort) -> Prelude.Bool
 eqIntMap a s1 s2 =
@@ -134,11 +146,19 @@
 emptyIntSet =
   []
 
+coq_IntSet_singleton :: Prelude.Int -> IntSet
+coq_IntSet_singleton x =
+  (:) x []
+
 coq_IntSet_member :: Prelude.Int -> IntSet -> Prelude.Bool
 coq_IntSet_member k m =
   Ssrbool.in_mem (unsafeCoerce k)
     (Ssrbool.mem (Seq.seq_predType Ssrnat.nat_eqType) (unsafeCoerce m))
 
+coq_IntSet_size :: IntSet -> Prelude.Int
+coq_IntSet_size m =
+  Data.List.length m
+
 coq_IntSet_insert :: Prelude.Int -> IntSet -> IntSet
 coq_IntSet_insert k m =
   case Ssrbool.in_mem (unsafeCoerce k)
@@ -146,6 +166,10 @@
    Prelude.True -> m;
    Prelude.False -> (:) k m}
 
+coq_IntSet_delete :: Prelude.Int -> IntSet -> IntSet
+coq_IntSet_delete k m =
+  unsafeCoerce (Seq.rem Ssrnat.nat_eqType (unsafeCoerce k) (unsafeCoerce m))
+
 coq_IntSet_union :: IntSet -> IntSet -> IntSet
 coq_IntSet_union m1 m2 =
   unsafeCoerce
@@ -168,6 +192,10 @@
 coq_IntSet_forFold z m f =
   coq_IntSet_foldl f z m
 
+coq_IntSet_toList :: IntSet -> [] Prelude.Int
+coq_IntSet_toList m =
+  m
+
 eqIntSet :: IntSet -> IntSet -> Prelude.Bool
 eqIntSet s1 s2 =
   Eqtype.eq_op (Seq.seq_eqType Ssrnat.nat_eqType) (unsafeCoerce s1)
@@ -205,5 +233,5 @@
     coq_IntMap_alter (\mxs ->
       case mxs of {
        Prelude.Just xs -> Prelude.Just ((:) x xs);
-       Prelude.Nothing -> Prelude.Just ((:) x [])}) n acc)
+       Prelude.Nothing -> Prelude.Just ((:[]) x)}) n acc)
 
diff --git a/LinearScan/Interval.hs b/LinearScan/Interval.hs
--- a/LinearScan/Interval.hs
+++ b/LinearScan/Interval.hs
@@ -12,55 +12,40 @@
 
 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.UsePos as UsePos
+import qualified LinearScan.Seq as Seq
+import qualified LinearScan.Ssrnat as Ssrnat
 
 
 __ :: 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 IntervalKind 
- ([] Range.RangeDesc)
+   Build_IntervalDesc Prelude.Int Prelude.Int Prelude.Int ([]
+                                                          Range.RangeDesc)
 
 ivar :: IntervalDesc -> Prelude.Int
 ivar i =
   case i of {
-   Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> ivar0}
+   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> ivar0}
 
 ibeg :: IntervalDesc -> Prelude.Int
 ibeg i =
   case i of {
-   Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> ibeg0}
+   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> ibeg0}
 
 iend :: IntervalDesc -> Prelude.Int
 iend i =
   case i of {
-   Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> iend0}
-
-iknd :: IntervalDesc -> IntervalKind
-iknd i =
-  case i of {
-   Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> iknd0}
+   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> iend0}
 
 rds :: IntervalDesc -> [] Range.RangeDesc
 rds i =
   case i of {
-   Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 -> rds0}
+   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> rds0}
 
 getIntervalDesc :: IntervalDesc -> IntervalDesc
 getIntervalDesc d =
@@ -78,8 +63,8 @@
 intervalEnd i =
   iend i
 
-intervalCoversPos :: IntervalDesc -> Prelude.Int -> Prelude.Bool
-intervalCoversPos d pos =
+posWithinInterval :: IntervalDesc -> Prelude.Int -> Prelude.Bool
+posWithinInterval d pos =
   (Prelude.&&) ((Prelude.<=) (intervalStart d) pos)
     ((Prelude.<=) ((Prelude.succ) pos) (intervalEnd d))
 
@@ -91,37 +76,53 @@
 intervalIntersectionPoint :: IntervalDesc -> IntervalDesc -> Prelude.Maybe
                              Lib.Coq_oddnum
 intervalIntersectionPoint i j =
-  Data.List.foldl' (\acc rd ->
-    case acc of {
-     Prelude.Just x -> Prelude.Just x;
-     Prelude.Nothing ->
-      Data.List.foldl' (\acc' rd' ->
-        case acc' of {
-         Prelude.Just x -> Prelude.Just x;
-         Prelude.Nothing -> Range.rangeIntersectionPoint ( rd) ( rd')})
-        Prelude.Nothing (rds j)}) Prelude.Nothing (rds i)
+  Data.List.foldl' (\mx rd ->
+    Lib.option_choose mx
+      (Data.List.foldl' (\mx' rd' ->
+        Lib.option_choose mx (Range.rangeIntersectionPoint ( rd) ( rd')))
+        Prelude.Nothing (rds j))) Prelude.Nothing (rds i)
 
 searchInRange :: Range.RangeDesc -> (UsePos.UsePos -> Prelude.Bool) ->
-                 Prelude.Maybe ((,) Range.RangeDesc UsePos.UsePos)
+                 Prelude.Maybe UsePos.UsePos
 searchInRange r f =
-  let {_evar_0_ = \x -> Prelude.Just ((,) r x)} in
+  let {_evar_0_ = \x -> Prelude.Just x} in
   let {_evar_0_0 = Prelude.Nothing} in
   case Range.findRangeUsePos ( r) f of {
    Prelude.Just x -> _evar_0_ x;
    Prelude.Nothing -> _evar_0_0}
 
 findIntervalUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) ->
-                      Prelude.Maybe ((,) Range.RangeDesc UsePos.UsePos)
+                      Prelude.Maybe
+                      ((,) Range.RangeDesc (Specif.Coq_sig2 UsePos.UsePos))
 findIntervalUsePos d f =
-  let {
-   go rs =
-     (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
-       (\r ->
-       searchInRange r f)
-       (\r rs' ->
-       Lib.option_choose (searchInRange r f) (go rs'))
-       rs}
-  in go (rds d)
+  case d of {
+   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 ->
+    let {
+     _evar_0_ = \r ->
+      let {_top_assumption_ = searchInRange r f} in
+      let {
+       _evar_0_ = \_top_assumption_0 -> Prelude.Just ((,) r
+        _top_assumption_0)}
+      in
+      let {_evar_0_0 = Prelude.Nothing} in
+      case _top_assumption_ of {
+       Prelude.Just x -> _evar_0_ x;
+       Prelude.Nothing -> _evar_0_0}}
+    in
+    let {
+     _evar_0_0 = \r rs iHrs ->
+      let {_top_assumption_ = searchInRange r f} in
+      let {
+       _evar_0_0 = \_top_assumption_0 -> Prelude.Just ((,) r
+        _top_assumption_0)}
+      in
+      let {_evar_0_1 = iHrs __ __ __} in
+      case _top_assumption_ of {
+       Prelude.Just x -> _evar_0_0 x;
+       Prelude.Nothing -> _evar_0_1}}
+    in
+    NonEmpty0.coq_NonEmpty_rec (\r _ _ _ -> _evar_0_ r) (\r rs iHrs _ _ _ ->
+      _evar_0_0 r rs iHrs) rds0 __ __ __}
 
 lookupUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) ->
                 Prelude.Maybe Lib.Coq_oddnum
@@ -142,318 +143,286 @@
 
 nextUseAfter :: IntervalDesc -> Prelude.Int -> Prelude.Maybe Lib.Coq_oddnum
 nextUseAfter d pos =
-  lookupUsePos d (\u -> (Prelude.<=) ((Prelude.succ) pos) (UsePos.uloc u))
+  case lookupUsePos d (\u ->
+         (Prelude.<=) ((Prelude.succ) pos) (UsePos.uloc u)) of {
+   Prelude.Just s -> Prelude.Just s;
+   Prelude.Nothing -> Prelude.Nothing}
 
-firstUsePos :: IntervalDesc -> Prelude.Maybe Prelude.Int
-firstUsePos d =
-  case Range.ups ( (Prelude.head (rds d))) of {
+rangeFirstUsePos :: Range.RangeDesc -> Prelude.Maybe UsePos.UsePos
+rangeFirstUsePos rd =
+  case Range.ups rd of {
    [] -> Prelude.Nothing;
-   (:) u l -> Prelude.Just (UsePos.uloc u)}
+   (:) u l -> Prelude.Just u}
 
+firstUsePos :: IntervalDesc -> Prelude.Maybe UsePos.UsePos
+firstUsePos d =
+  let {
+   go xs =
+     (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
+       (\x ->
+       rangeFirstUsePos ( x))
+       (\x xs0 ->
+       Lib.option_choose (rangeFirstUsePos ( x)) (go xs0))
+       xs}
+  in go (rds d)
+
+lastUsePos :: IntervalDesc -> Prelude.Maybe UsePos.UsePos
+lastUsePos d =
+  let {
+   go xs =
+     (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
+       (\x ->
+       Lib.olast (Range.ups ( x)))
+       (\x xs0 ->
+       Lib.option_choose (go xs0) (Lib.olast (Range.ups ( x))))
+       xs}
+  in go (rds d)
+
+afterLifetimeHole :: IntervalDesc -> Lib.Coq_oddnum -> Lib.Coq_oddnum
+afterLifetimeHole d pos =
+  let {
+   f = \x k ->
+    case (Prelude.<=) ((Prelude.succ) ( pos)) (Range.rbeg ( x)) of {
+     Prelude.True -> Range.rbeg ( x);
+     Prelude.False -> k}}
+  in
+  let {
+   go xs =
+     (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
+       (\x ->
+       f x pos)
+       (\x xs0 ->
+       f x (go xs0))
+       xs}
+  in go (rds d)
+
 firstUseReqReg :: IntervalDesc -> Prelude.Maybe Lib.Coq_oddnum
 firstUseReqReg d =
   lookupUsePos d UsePos.regReq
 
-intervalSpan :: ([] Range.RangeDesc) -> Prelude.Int -> Prelude.Int ->
-                Prelude.Int -> Prelude.Int -> IntervalKind ->
-                ((,) (Prelude.Maybe IntervalDesc)
-                (Prelude.Maybe IntervalDesc))
-intervalSpan rs before iv ib ie knd =
+firstUseReqRegOrEnd :: IntervalDesc -> Lib.Coq_oddnum
+firstUseReqRegOrEnd d =
+  let {filtered_var = firstUseReqReg d} in
+  case filtered_var of {
+   Prelude.Just n ->  n;
+   Prelude.Nothing ->
+    case Ssrnat.odd (iend d) of {
+     Prelude.True -> iend d;
+     Prelude.False -> Prelude.pred (iend d)}}
+
+divideIntervalRanges :: IntervalDesc -> Prelude.Int ->
+                        ((,) Range.SortedRanges Range.SortedRanges)
+divideIntervalRanges d before =
   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
+   _evar_0_ = \_top_assumption_ ->
+    let {
+     _evar_0_ = \_top_assumption_0 ->
       let {
-       _evar_0_ = \_top_assumption_0 ->
+       _evar_0_ = \_ ->
         let {
-         _evar_0_ = \r0 _top_assumption_1 ->
-          let {
-           _evar_0_ = \r1 ->
-            let {
-             _evar_0_ = let {
-                         _evar_0_ = \_ _ -> (,) (Prelude.Just
-                          (packInterval (Build_IntervalDesc iv
-                            (Range.rbeg ( r0)) (Range.rend ( r0)) lknd ((:[])
-                            ( r0))))) (Prelude.Just
-                          (packInterval (Build_IntervalDesc iv
-                            (Range.rbeg ( r1)) (Range.rend ( r1)) rknd ((:[])
-                            ( r1)))))}
-                        in
-                         _evar_0_}
-            in
-             _evar_0_ __ __}
-          in
+         _evar_0_ = \_ _ ->
           let {
-           _evar_0_0 = let {
-                        _evar_0_0 = let {
-                                     _evar_0_0 = \_ -> (,) (Prelude.Just
-                                      (packInterval (Build_IntervalDesc iv
-                                        (Range.rbeg ( r0)) (Range.rend ( r0))
-                                        knd ((:[]) ( r0))))) Prelude.Nothing}
-                                    in
-                                     _evar_0_0}
-                       in
-                        _evar_0_0}
+           _evar_0_ = \_ ->
+            let {_evar_0_ = let {_evar_0_ = \_ -> (,) [] []} in  _evar_0_} in
+             _evar_0_ __}
           in
-          case _top_assumption_1 of {
-           Prelude.Just x -> (\_ -> _evar_0_ x);
-           Prelude.Nothing -> _evar_0_0}}
+           _evar_0_ __}
         in
+         _evar_0_ __ __}
+      in
+      let {
+       _evar_0_0 = \r2 rs2 ->
         let {
-         _evar_0_0 = \_top_assumption_1 ->
+         _evar_0_0 = \_ ->
           let {
-           _evar_0_0 = \r1 ->
+           _evar_0_0 = \_ _ ->
             let {
-             _evar_0_0 = let {
-                          _evar_0_0 = \_ -> (,) Prelude.Nothing (Prelude.Just
-                           (packInterval (Build_IntervalDesc iv
-                             (Range.rbeg ( r1)) (Range.rend ( r1)) knd ((:[])
-                             ( r1)))))}
-                         in
-                          _evar_0_0}
+             _evar_0_0 = \_ ->
+              let {
+               _evar_0_0 = let {
+                            _evar_0_0 = let {
+                                         _evar_0_0 = \_ _ ->
+                                          let {
+                                           _evar_0_0 = let {
+                                                        _evar_0_0 = \_ -> (,)
+                                                         [] ((:) r2 rs2)}
+                                                       in
+                                                        _evar_0_0}
+                                          in
+                                           _evar_0_0 __}
+                                        in
+                                         _evar_0_0}
+                           in
+                            _evar_0_0}
+              in
+               _evar_0_0 __ __}
             in
-             _evar_0_0}
+             _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}}
+           _evar_0_0 __ __}
         in
-        case _top_assumption_0 of {
-         Prelude.Just x -> _evar_0_ x;
-         Prelude.Nothing -> _evar_0_0}}
+         _evar_0_0 __}
       in
-      case _top_assumption_ of {
-       (,) x x0 -> _evar_0_ x x0 __})
-      (\r rs0 ->
-      let {_top_assumption_ = Range.rangeSpan before ( r)} in
+      case _top_assumption_0 of {
+       [] -> _evar_0_;
+       (:) x x0 -> (\_ -> _evar_0_0 x x0)}}
+    in
+    let {
+     _evar_0_0 = \r1 rs1 _top_assumption_0 ->
       let {
-       _evar_0_ = \_top_assumption_0 ->
+       _evar_0_0 = \_ ->
         let {
-         _evar_0_ = \r0 _top_assumption_1 ->
-          let {
-           _evar_0_ = \r1 ->
-            let {
-             _evar_0_ = \_ ->
-              (Prelude.flip (Prelude.$)) __ (\_ ->
-                let {
-                 _evar_0_ = \_ -> (,) (Prelude.Just
-                  (packInterval (Build_IntervalDesc iv (Range.rbeg ( r0))
-                    (Range.rend ( r0)) lknd ((:[]) ( r0))))) (Prelude.Just
-                  (packInterval (Build_IntervalDesc iv (Range.rbeg ( r1))
-                    (Range.rend ( (Prelude.last rs0))) rknd ((:) r1 rs0))))}
-                in
-                 _evar_0_ __)}
-            in
-             _evar_0_ __}
-          in
+         _evar_0_0 = \_ _ ->
           let {
            _evar_0_0 = \_ ->
             let {
-             _evar_0_0 = \_ ->
-              let {
-               _top_assumption_2 = intervalSpan rs0 before iv
-                                     (Range.rbeg ( (Prelude.head rs0)))
-                                     (Range.rend ( (Prelude.last rs0))) knd}
-              in
-              let {
-               _evar_0_0 = \_top_assumption_3 ->
-                let {
-                 _evar_0_0 = \i1_1 _top_assumption_4 ->
-                  let {
-                   _evar_0_0 = \i1_2 ->
-                    case i1_1 of {
-                     Build_IntervalDesc ivar0 ibeg0 iend0 iknd0 rds0 ->
-                      let {
-                       _evar_0_0 = let {
-                                    _evar_0_0 = \_ ->
-                                     let {
-                                      _evar_0_0 = \_ ->
-                                       let {
-                                        _evar_0_0 = \_ ->
-                                         (Prelude.flip (Prelude.$)) __ (\_ ->
-                                           let {
-                                            _evar_0_0 = let {
-                                                         _evar_0_0 = \_ _ _ ->
-                                                          (,) (Prelude.Just
-                                                          (packInterval
-                                                            (Build_IntervalDesc
-                                                            ivar0
-                                                            (Range.rbeg ( r))
-                                                            iend0 lknd ((:) r
-                                                            rds0))))
-                                                          (Prelude.Just
-                                                          (packInterval
-                                                            (Build_IntervalDesc
-                                                            (ivar ( i1_2))
-                                                            (ibeg ( i1_2))
-                                                            (iend ( i1_2))
-                                                            rknd
-                                                            (rds ( i1_2)))))}
-                                                        in
-                                                         _evar_0_0 __}
-                                           in
-                                            _evar_0_0)}
-                                       in
-                                        _evar_0_0 __}
-                                     in
-                                      _evar_0_0 __}
-                                   in
-                                    _evar_0_0}
-                      in
-                       _evar_0_0 __}}
-                  in
-                  let {
-                   _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
-                                             (packInterval
-                                               (Build_IntervalDesc ivar0
-                                               (Range.rbeg ( r)) iend0 lknd
-                                               ((:) 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.Nothing -> _evar_0_1}}
-                in
-                let {
-                 _evar_0_1 = \_top_assumption_4 ->
-                  let {
-                   _evar_0_1 = \i1_2 ->
-                    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
-                                               (packInterval
-                                                 (Build_IntervalDesc iv
-                                                 (Range.rbeg ( r0))
-                                                 (Range.rend ( r0)) lknd
-                                                 ((:[]) ( r0)))))
-                                               (Prelude.Just
-                                               (packInterval
-                                                 (Build_IntervalDesc
-                                                 (ivar (Build_IntervalDesc
-                                                   ivar0
-                                                   (Range.rbeg
-                                                     ( (Prelude.head rds0)))
-                                                   (Range.rend
-                                                     ( (Prelude.last rds0)))
-                                                   iknd0 rds0))
-                                                 (ibeg (Build_IntervalDesc
-                                                   ivar0
-                                                   (Range.rbeg
-                                                     ( (Prelude.head rds0)))
-                                                   (Range.rend
-                                                     ( (Prelude.last rds0)))
-                                                   iknd0 rds0))
-                                                 (iend (Build_IntervalDesc
-                                                   ivar0
-                                                   (Range.rbeg
-                                                     ( (Prelude.head rds0)))
-                                                   (Range.rend
-                                                     ( (Prelude.last rds0)))
-                                                   iknd0 rds0)) rknd
-                                                 (rds (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.Nothing -> _evar_0_2}}
-                in
-                case _top_assumption_3 of {
-                 Prelude.Just x -> _evar_0_0 x;
-                 Prelude.Nothing -> _evar_0_1}}
-              in
-              case _top_assumption_2 of {
-               (,) x x0 -> _evar_0_0 x x0 __ __ __}}
+             _evar_0_0 = let {
+                          _evar_0_0 = let {
+                                       _evar_0_0 = \_ _ ->
+                                        let {
+                                         _evar_0_0 = let {
+                                                      _evar_0_0 = \_ -> (,)
+                                                       ((:) r1 rs1) []}
+                                                     in
+                                                      _evar_0_0}
+                                        in
+                                         _evar_0_0 __}
+                                      in
+                                       _evar_0_0}
+                         in
+                          _evar_0_0}
             in
-             _evar_0_0 __}
+             _evar_0_0 __ __}
           in
-          case _top_assumption_1 of {
-           Prelude.Just x -> (\_ -> _evar_0_ x);
-           Prelude.Nothing -> _evar_0_0}}
+           _evar_0_0 __}
         in
+         _evar_0_0 __ __}
+      in
+      let {
+       _evar_0_1 = \r2 rs2 ->
         let {
-         _evar_0_0 = \_top_assumption_1 ->
+         _evar_0_1 = \_ ->
           let {
-           _evar_0_0 = \r1 ->
+           _evar_0_1 = \_ ->
             let {
-             _evar_0_0 = \_ ->
-              let {
-               _evar_0_0 = \_ ->
-                let {
-                 _evar_0_0 = \_ -> (,) Prelude.Nothing (Prelude.Just
-                  (packInterval (Build_IntervalDesc iv (Range.rbeg ( r1))
-                    (Range.rend ( (Prelude.last rs0))) knd ((:) r1 rs0))))}
-                in
-                 _evar_0_0 __}
-              in
-               _evar_0_0 __}
+             _evar_0_1 = let {
+                          _evar_0_1 = let {
+                                       _evar_0_1 = \_ _ ->
+                                        let {
+                                         _evar_0_1 = let {
+                                                      _evar_0_1 = \_ -> (,)
+                                                       ((:) r1 rs1) ((:) r2
+                                                       rs2)}
+                                                     in
+                                                      _evar_0_1}
+                                        in
+                                         _evar_0_1 __}
+                                      in
+                                       _evar_0_1}
+                         in
+                          _evar_0_1}
             in
-             _evar_0_0 __}
+             _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}}
+           _evar_0_1 __}
         in
-        case _top_assumption_0 of {
-         Prelude.Just x -> _evar_0_ x;
-         Prelude.Nothing -> _evar_0_0}}
+         _evar_0_1 __}
       in
-      case _top_assumption_ of {
-       (,) x x0 -> _evar_0_ x x0 __})
-      rs}
+      case _top_assumption_0 of {
+       [] -> _evar_0_0;
+       (:) x x0 -> (\_ -> _evar_0_1 x x0)}}
+    in
+    case _top_assumption_ of {
+     [] -> _evar_0_;
+     (:) x x0 -> _evar_0_0 x x0}}
   in
-  case splitKind knd of {
-   (,) x x0 -> _evar_0_ x x0}
+  case Lib.span (\rd ->
+         (Prelude.<=) ((Prelude.succ) (Range.rend ( rd))) before) ( (rds d)) of {
+   (,) x x0 -> _evar_0_ x x0 __}
+
+splitIntervalRanges :: IntervalDesc -> Prelude.Int ->
+                       ((,) Range.SortedRanges Range.SortedRanges)
+splitIntervalRanges d before =
+  let {_top_assumption_ = divideIntervalRanges d before} in
+  let {
+   _evar_0_ = \_top_assumption_0 _top_assumption_1 ->
+    let {
+     _evar_0_ = \_ _ _ ->
+      let {_evar_0_ = \_ -> Logic.coq_False_rec} in
+      let {_evar_0_0 = \_a_ _l_ -> Logic.coq_False_rec} in
+      case _top_assumption_0 of {
+       [] -> _evar_0_ __;
+       (:) x x0 -> _evar_0_0 x x0}}
+    in
+    let {
+     _evar_0_0 = \r2 rs2 ->
+      let {_evar_0_0 = \_ -> (,) _top_assumption_0 ((:) r2 rs2)} in
+      let {
+       _evar_0_1 = \_ ->
+        (Prelude.flip (Prelude.$)) __ (\_ ->
+          let {_top_assumption_2 = Range.rangeSpan ( r2) before} in
+          let {
+           _evar_0_1 = \r2a r2b -> (,) (Seq.rcons _top_assumption_0 r2a) ((:)
+            r2b rs2)}
+          in
+          case _top_assumption_2 of {
+           (,) x x0 -> _evar_0_1 x x0})}
+      in
+      case (Prelude.<=) before (Range.rbeg ( r2)) of {
+       Prelude.True -> _evar_0_0 __;
+       Prelude.False -> _evar_0_1 __}}
+    in
+    case _top_assumption_1 of {
+     [] -> _evar_0_ __ __;
+     (:) x x0 -> (\_ -> _evar_0_0 x x0)}}
+  in
+  case _top_assumption_ of {
+   (,) x x0 -> _evar_0_ x x0 __}
+
+type SubIntervalsOf = ((,) IntervalDesc IntervalDesc)
+
+splitInterval :: IntervalDesc -> Prelude.Int -> SubIntervalsOf
+splitInterval d before =
+  let {_top_assumption_ = splitIntervalRanges d before} in
+  let {
+   _evar_0_ = \_top_assumption_0 ->
+    let {
+     _evar_0_ = \_top_assumption_1 ->
+      let {_evar_0_ = \_ _ _ -> Logic.coq_False_rec} in
+      let {_evar_0_0 = \r2 rs2 -> Logic.coq_False_rec} in
+      case _top_assumption_1 of {
+       [] -> _evar_0_ __ __;
+       (:) x x0 -> (\_ -> _evar_0_0 x x0)}}
+    in
+    let {
+     _evar_0_0 = \r1 rs1 _top_assumption_1 ->
+      let {_evar_0_0 = \_ _ _ -> Logic.coq_False_rec} in
+      let {
+       _evar_0_1 = \r2 rs2 ->
+        (Prelude.flip (Prelude.$)) __ (\_ ->
+          (Prelude.flip (Prelude.$)) __ (\_ -> (,)
+            (packInterval (Build_IntervalDesc (ivar (getIntervalDesc d))
+              (Range.rbeg
+                ( (Prelude.head (NonEmpty0.coq_NE_from_list r1 rs1))))
+              (Range.rend
+                ( (Prelude.last (NonEmpty0.coq_NE_from_list r1 rs1))))
+              (NonEmpty0.coq_NE_from_list r1 rs1)))
+            (packInterval (Build_IntervalDesc (ivar (getIntervalDesc d))
+              (Range.rbeg
+                ( (Prelude.head (NonEmpty0.coq_NE_from_list r2 rs2))))
+              (Range.rend
+                ( (Prelude.last (NonEmpty0.coq_NE_from_list r2 rs2))))
+              (NonEmpty0.coq_NE_from_list r2 rs2)))))}
+      in
+      case _top_assumption_1 of {
+       [] -> _evar_0_0 __ __;
+       (:) x x0 -> (\_ -> _evar_0_1 x x0)}}
+    in
+    (\_top_assumption_1 ->
+    case _top_assumption_0 of {
+     [] -> _evar_0_ _top_assumption_1;
+     (:) x x0 -> _evar_0_0 x x0 _top_assumption_1})}
+  in
+  case _top_assumption_ 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
@@ -12,7 +12,6 @@
 
 import qualified LinearScan.Specif as Specif
 import qualified LinearScan.Eqtype as Eqtype
-import qualified LinearScan.Ssrbool as Ssrbool
 
 
 __ :: any
@@ -24,6 +23,15 @@
    Prelude.Just a -> x;
    Prelude.Nothing -> y}
 
+olast :: ([] a1) -> Prelude.Maybe a1
+olast l =
+  let {
+   go res xs =
+     case xs of {
+      [] -> res;
+      (:) x xs0 -> go (Prelude.Just x) xs0}}
+  in go Prelude.Nothing l
+
 maybeLookup :: Eqtype.Equality__Coq_type -> ([]
                ((,) Eqtype.Equality__Coq_sort a1)) ->
                Eqtype.Equality__Coq_sort -> Prelude.Maybe a1
@@ -55,6 +63,13 @@
 forFoldr b v f =
   Prelude.foldr f b v
 
+catMaybes :: ([] (Prelude.Maybe a1)) -> [] a1
+catMaybes l =
+  forFoldr [] l (\mx rest ->
+    case mx of {
+     Prelude.Just x -> (:) x rest;
+     Prelude.Nothing -> rest})
+
 span :: (a1 -> Prelude.Bool) -> ([] a1) -> (,) ([] a1) ([] a1)
 span p l =
   case l of {
@@ -74,7 +89,7 @@
      Prelude.False -> (,) (Prelude.fst acc) ((:) x (Prelude.snd acc))}) ((,)
     [] [])
 
-insert :: (Ssrbool.Coq_rel a1) -> a1 -> ([] a1) -> [] a1
+insert :: (a1 -> a1 -> Prelude.Bool) -> a1 -> ([] a1) -> [] a1
 insert p z l =
   case l of {
    [] -> (:) z [];
diff --git a/LinearScan/LiveSets.hs b/LinearScan/LiveSets.hs
--- a/LinearScan/LiveSets.hs
+++ b/LinearScan/LiveSets.hs
@@ -16,6 +16,7 @@
 import qualified LinearScan.Blocks as Blocks
 import qualified LinearScan.IntMap as IntMap
 import qualified LinearScan.Lib as Lib
+import qualified LinearScan.UsePos as UsePos
 import qualified LinearScan.Eqtype as Eqtype
 import qualified LinearScan.Ssrbool as Ssrbool
 import qualified LinearScan.Ssrnat as Ssrnat
@@ -233,9 +234,9 @@
                     (,) lastIdx liveSet1 -> (,) ((Prelude.succ)
                      ((Prelude.succ) lastIdx))
                      (case Lib.partition (\v ->
-                             Eqtype.eq_op Blocks.coq_VarKind_eqType
+                             Eqtype.eq_op UsePos.coq_VarKind_eqType
                                (unsafeCoerce (Blocks.varKind maxReg v))
-                               (unsafeCoerce Blocks.Input))
+                               (unsafeCoerce UsePos.Input))
                              (Blocks.opRefs maxReg oinfo o) of {
                        (,) inputs others ->
                         let {
diff --git a/LinearScan/Loops.hs b/LinearScan/Loops.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/Loops.hs
@@ -0,0 +1,412 @@
+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}
+{- For Hugs, use the option -F"cpp -P -traditional" -}
+
+module LinearScan.Loops where
+
+
+import Debug.Trace (trace, traceShow)
+import qualified Prelude
+import qualified Data.IntMap
+import qualified Data.IntSet
+import qualified Data.List
+import qualified Data.Ord
+import qualified Data.Functor.Identity
+import qualified LinearScan.Utils
+
+import qualified LinearScan.Blocks as Blocks
+import qualified LinearScan.IntMap as IntMap
+import qualified LinearScan.Lib as Lib
+import qualified LinearScan.State as State
+import qualified LinearScan.Eqtype as Eqtype
+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
+
+data LoopState =
+   Build_LoopState IntMap.IntSet IntMap.IntSet ([] Blocks.BlockId) IntMap.IntSet 
+ (IntMap.IntMap IntMap.IntSet) (IntMap.IntMap IntMap.IntSet) (IntMap.IntMap
+                                                             IntMap.IntSet) 
+ (IntMap.IntMap ((,) Prelude.Int Prelude.Int))
+
+activeBlocks :: LoopState -> IntMap.IntSet
+activeBlocks l =
+  case l of {
+   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
+    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
+    loopDepths0 -> activeBlocks0}
+
+visitedBlocks :: LoopState -> IntMap.IntSet
+visitedBlocks l =
+  case l of {
+   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
+    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
+    loopDepths0 -> visitedBlocks0}
+
+loopHeaderBlocks :: LoopState -> [] Blocks.BlockId
+loopHeaderBlocks l =
+  case l of {
+   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
+    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
+    loopDepths0 -> loopHeaderBlocks0}
+
+loopEndBlocks :: LoopState -> IntMap.IntSet
+loopEndBlocks l =
+  case l of {
+   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
+    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
+    loopDepths0 -> loopEndBlocks0}
+
+forwardBranches :: LoopState -> IntMap.IntMap IntMap.IntSet
+forwardBranches l =
+  case l of {
+   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
+    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
+    loopDepths0 -> forwardBranches0}
+
+backwardBranches :: LoopState -> IntMap.IntMap IntMap.IntSet
+backwardBranches l =
+  case l of {
+   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
+    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
+    loopDepths0 -> backwardBranches0}
+
+loopIndices :: LoopState -> IntMap.IntMap IntMap.IntSet
+loopIndices l =
+  case l of {
+   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
+    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
+    loopDepths0 -> loopIndices0}
+
+loopDepths :: LoopState -> IntMap.IntMap ((,) Prelude.Int Prelude.Int)
+loopDepths l =
+  case l of {
+   Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
+    loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
+    loopDepths0 -> loopDepths0}
+
+emptyLoopState :: LoopState
+emptyLoopState =
+  Build_LoopState IntMap.emptyIntSet IntMap.emptyIntSet [] IntMap.emptyIntSet
+    IntMap.emptyIntMap IntMap.emptyIntMap IntMap.emptyIntMap
+    IntMap.emptyIntMap
+
+modifyActiveBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> State.State
+                      LoopState ()
+modifyActiveBlocks f =
+  State.modify (\st -> Build_LoopState (f (activeBlocks st))
+    (visitedBlocks st) (loopHeaderBlocks st) (loopEndBlocks st)
+    (forwardBranches st) (backwardBranches st) (loopIndices st)
+    (loopDepths st))
+
+modifyVisitedBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> State.State
+                       LoopState ()
+modifyVisitedBlocks f =
+  State.modify (\st -> Build_LoopState (activeBlocks st)
+    (f (visitedBlocks st)) (loopHeaderBlocks st) (loopEndBlocks st)
+    (forwardBranches st) (backwardBranches st) (loopIndices st)
+    (loopDepths st))
+
+modifyLoopHeaderBlocks :: (([] Blocks.BlockId) -> [] Blocks.BlockId) ->
+                          State.State LoopState ()
+modifyLoopHeaderBlocks f =
+  State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
+    (f (loopHeaderBlocks st)) (loopEndBlocks st) (forwardBranches st)
+    (backwardBranches st) (loopIndices st) (loopDepths st))
+
+modifyLoopEndBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> State.State
+                       LoopState ()
+modifyLoopEndBlocks f =
+  State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
+    (loopHeaderBlocks st) (f (loopEndBlocks st)) (forwardBranches st)
+    (backwardBranches st) (loopIndices st) (loopDepths st))
+
+modifyForwardBranches :: ((IntMap.IntMap IntMap.IntSet) -> IntMap.IntMap
+                         IntMap.IntSet) -> State.State LoopState ()
+modifyForwardBranches f =
+  State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
+    (loopHeaderBlocks st) (loopEndBlocks st) (f (forwardBranches st))
+    (backwardBranches st) (loopIndices st) (loopDepths st))
+
+modifyBackwardBranches :: ((IntMap.IntMap IntMap.IntSet) -> IntMap.IntMap
+                          IntMap.IntSet) -> State.State LoopState ()
+modifyBackwardBranches f =
+  State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
+    (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st)
+    (f (backwardBranches st)) (loopIndices st) (loopDepths st))
+
+setLoopIndices :: (IntMap.IntMap IntMap.IntSet) -> State.State LoopState ()
+setLoopIndices indices =
+  State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
+    (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st)
+    (backwardBranches st) indices (loopDepths st))
+
+setLoopDepths :: (IntMap.IntMap ((,) Prelude.Int Prelude.Int)) -> State.State
+                 LoopState ()
+setLoopDepths depths =
+  State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
+    (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st)
+    (backwardBranches st) (loopIndices st) depths)
+
+addReference :: Prelude.Int -> Prelude.Int -> (IntMap.IntMap IntMap.IntSet)
+                -> IntMap.IntMap IntMap.IntSet
+addReference i x =
+  IntMap.coq_IntMap_alter (\macc ->
+    case macc of {
+     Prelude.Just acc -> Prelude.Just (IntMap.coq_IntSet_insert x acc);
+     Prelude.Nothing -> Prelude.Just (IntMap.coq_IntSet_singleton x)}) i
+
+pathToLoopHeader :: Blocks.BlockId -> Prelude.Int -> LoopState ->
+                    Prelude.Maybe IntMap.IntSet
+pathToLoopHeader b header st =
+  let {
+   go fuel visited b0 =
+     (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
+       (\_ ->
+       Prelude.Nothing)
+       (\n ->
+       let {visited' = IntMap.coq_IntSet_insert b0 visited} in
+       let {
+        forwardPreds = case IntMap.coq_IntMap_lookup b0 (forwardBranches st) of {
+                        Prelude.Just preds -> IntMap.coq_IntSet_toList preds;
+                        Prelude.Nothing -> []}}
+       in
+       let {
+        backwardPreds = case IntMap.coq_IntMap_lookup b0
+                               (backwardBranches st) of {
+                         Prelude.Just preds -> IntMap.coq_IntSet_toList preds;
+                         Prelude.Nothing -> []}}
+       in
+       let {preds = (Prelude.++) forwardPreds backwardPreds} in
+       Lib.forFold (Prelude.Just (IntMap.coq_IntSet_singleton b0))
+         (unsafeCoerce preds) (\mxs pred ->
+         case mxs of {
+          Prelude.Just xs ->
+           case Eqtype.eq_op Ssrnat.nat_eqType pred (unsafeCoerce header) of {
+            Prelude.True -> Prelude.Just
+             (IntMap.coq_IntSet_union xs
+               (IntMap.coq_IntSet_singleton (unsafeCoerce pred)));
+            Prelude.False ->
+             case IntMap.coq_IntSet_member (unsafeCoerce pred) visited' of {
+              Prelude.True -> Prelude.Just xs;
+              Prelude.False ->
+               case unsafeCoerce go n visited' pred of {
+                Prelude.Just ys -> Prelude.Just
+                 (IntMap.coq_IntSet_union xs ys);
+                Prelude.Nothing -> Prelude.Nothing}}};
+          Prelude.Nothing -> Prelude.Nothing}))
+       fuel}
+  in go (IntMap.coq_IntSet_size (visitedBlocks st)) IntMap.emptyIntSet b
+
+computeLoopDepths :: (Blocks.BlockInfo a1 a2 a3 a4) -> (IntMap.IntMap 
+                     a1) -> State.State LoopState ()
+computeLoopDepths binfo bs =
+  State.bind (\st ->
+    let {
+     m = Lib.forFold IntMap.emptyIntMap
+           (IntMap.coq_IntSet_toList (loopEndBlocks st)) (\m endBlock ->
+           case IntMap.coq_IntMap_lookup endBlock bs of {
+            Prelude.Just b ->
+             Lib.forFold m (unsafeCoerce (Blocks.blockSuccessors binfo b))
+               (\m' sux ->
+               let {
+                loopIndex = Seq.find (\x ->
+                              Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce x)
+                                sux) (loopHeaderBlocks st)}
+               in
+               case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce loopIndex)
+                      (unsafeCoerce (Data.List.length (loopHeaderBlocks st))) of {
+                Prelude.True -> m';
+                Prelude.False ->
+                 let {mres = pathToLoopHeader endBlock (unsafeCoerce sux) st}
+                 in
+                 case mres of {
+                  Prelude.Just path ->
+                   Lib.forFold m' (IntMap.coq_IntSet_toList path)
+                     (\m'' blk -> addReference loopIndex blk m'');
+                  Prelude.Nothing -> m'}});
+            Prelude.Nothing -> m})}
+    in
+    let {
+     f = \acc loopIndex refs ->
+      IntMap.coq_IntSet_forFold acc refs (\m' blk ->
+        let {
+         f = \mx ->
+          case mx of {
+           Prelude.Just y ->
+            case y of {
+             (,) idx depth -> Prelude.Just ((,) (Prelude.min idx loopIndex)
+              ((Prelude.succ) depth))};
+           Prelude.Nothing -> Prelude.Just ((,) loopIndex ((Prelude.succ) 0))}}
+        in
+        IntMap.coq_IntMap_alter f blk m')}
+    in
+    State.bind (\x ->
+      setLoopDepths (IntMap.coq_IntMap_foldlWithKey f IntMap.emptyIntMap m))
+      (setLoopIndices m)) State.get
+
+computeVarReferences :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->
+                        (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> LoopState ->
+                        IntMap.IntMap IntMap.IntSet
+computeVarReferences maxReg binfo oinfo bs st =
+  Lib.forFold IntMap.emptyIntMap bs (\acc b ->
+    let {bid = Blocks.blockId binfo b} in
+    let {
+     g = \acc1 loopIndex blks ->
+      case Prelude.not (IntMap.coq_IntSet_member bid blks) of {
+       Prelude.True -> acc1;
+       Prelude.False ->
+        case Blocks.blockOps binfo b of {
+         (,) p zs ->
+          case p of {
+           (,) xs ys ->
+            Lib.forFold acc1 ((Prelude.++) xs ((Prelude.++) ys zs))
+              (\acc2 op ->
+              Lib.forFold acc2 (Blocks.opRefs maxReg oinfo op) (\acc3 v ->
+                case Blocks.varId maxReg v of {
+                 Prelude.Left p0 -> acc3;
+                 Prelude.Right vid -> addReference loopIndex vid acc3}))}}}}
+    in
+    IntMap.coq_IntMap_foldlWithKey g acc (loopIndices st))
+
+findLoopEnds :: (Blocks.BlockInfo a1 a2 a3 a4) -> (IntMap.IntMap a1) ->
+                State.State LoopState ()
+findLoopEnds binfo bs =
+  let {
+   go = let {
+         go n b =
+           (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
+             (\_ ->
+             State.pure ())
+             (\n0 ->
+             let {bid = Blocks.blockId binfo b} in
+             State.bind (\x ->
+               State.bind (\x0 ->
+                 State.bind (\x1 ->
+                   modifyActiveBlocks (IntMap.coq_IntSet_delete bid))
+                   (State.forM_ (Blocks.blockSuccessors binfo b) (\sux ->
+                     State.bind (\active ->
+                       State.bind (\x1 ->
+                         State.bind (\visited ->
+                           case IntMap.coq_IntSet_member sux visited of {
+                            Prelude.True -> State.pure ();
+                            Prelude.False ->
+                             case IntMap.coq_IntMap_lookup sux bs of {
+                              Prelude.Just x2 -> go n0 x2;
+                              Prelude.Nothing -> State.pure ()}})
+                           (State.gets visitedBlocks))
+                         (case IntMap.coq_IntSet_member sux active of {
+                           Prelude.True ->
+                            State.bind (\x1 ->
+                              State.bind (\x2 ->
+                                modifyBackwardBranches (addReference sux bid))
+                                (modifyLoopEndBlocks
+                                  (IntMap.coq_IntSet_insert bid)))
+                              (modifyLoopHeaderBlocks (\l ->
+                                case Prelude.not
+                                       (Ssrbool.in_mem (unsafeCoerce sux)
+                                         (Ssrbool.mem
+                                           (Seq.seq_predType
+                                             Ssrnat.nat_eqType)
+                                           (unsafeCoerce l))) of {
+                                 Prelude.True -> (:) sux l;
+                                 Prelude.False -> l}));
+                           Prelude.False ->
+                            modifyForwardBranches (addReference sux bid)}))
+                       (State.gets activeBlocks))))
+                 (modifyActiveBlocks (IntMap.coq_IntSet_insert bid)))
+               (modifyVisitedBlocks (IntMap.coq_IntSet_insert bid)))
+             n}
+        in go}
+  in
+  case IntMap.coq_IntMap_toList bs of {
+   [] -> State.pure ();
+   (:) p l ->
+    case p of {
+     (,) n b ->
+      State.bind (\x -> computeLoopDepths binfo bs)
+        (go (IntMap.coq_IntMap_size bs) b)}}
+
+computeBlockOrder :: (Blocks.BlockInfo a1 a2 a3 a4) -> ([] a1) -> (,)
+                     LoopState ([] a1)
+computeBlockOrder binfo blocks =
+  case blocks of {
+   [] -> (,) emptyLoopState [];
+   (:) b bs ->
+    let {
+     blockMap = IntMap.coq_IntMap_fromList
+                  (Prelude.map (\x -> (,) (Blocks.blockId binfo x) x) blocks)}
+    in
+    case findLoopEnds binfo blockMap emptyLoopState of {
+     (,) u st ->
+      let {
+       isHeavier = \x y ->
+        let {x_id = Blocks.blockId binfo x} in
+        let {y_id = Blocks.blockId binfo y} in
+        let {
+         x_depth = case IntMap.coq_IntMap_lookup x_id (loopDepths st) of {
+                    Prelude.Just p ->
+                     case p of {
+                      (,) idx depth -> depth};
+                    Prelude.Nothing -> 0}}
+        in
+        let {
+         y_depth = case IntMap.coq_IntMap_lookup y_id (loopDepths st) of {
+                    Prelude.Just p ->
+                     case p of {
+                      (,) idx depth -> depth};
+                    Prelude.Nothing -> 0}}
+        in
+        (Prelude.<=) ((Prelude.succ) y_depth) x_depth}
+      in
+      let {
+       go = let {
+             go n branches work_list =
+               (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
+                 (\_ ->
+                 [])
+                 (\n0 ->
+                 case work_list of {
+                  [] -> [];
+                  (:) w ws ->
+                   case let {bid = Blocks.blockId binfo w} in
+                        let {suxs = Blocks.blockSuccessors binfo w} in
+                        Lib.forFoldr ((,) branches ws) suxs (\sux acc ->
+                          case acc of {
+                           (,) branches' ws' ->
+                            let {
+                             insertion = case IntMap.coq_IntMap_lookup sux
+                                                blockMap of {
+                                          Prelude.Just s ->
+                                           Lib.insert isHeavier s ws';
+                                          Prelude.Nothing -> ws'}}
+                            in
+                            case IntMap.coq_IntMap_lookup sux branches' of {
+                             Prelude.Just incs -> (,)
+                              (IntMap.coq_IntMap_insert sux
+                                (IntMap.coq_IntSet_delete bid incs)
+                                branches')
+                              (case Eqtype.eq_op Ssrnat.nat_eqType
+                                      (unsafeCoerce
+                                        (IntMap.coq_IntSet_size incs))
+                                      (unsafeCoerce ((Prelude.succ) 0)) of {
+                                Prelude.True -> insertion;
+                                Prelude.False -> ws'});
+                             Prelude.Nothing -> (,) branches' insertion}}) of {
+                    (,) branches' ws' -> (:) w (go n0 branches' ws')}})
+                 n}
+            in go}
+      in
+      (,) st (go (Data.List.length blocks) (forwardBranches st) ((:) b []))}}
+
diff --git a/LinearScan/Main.hs b/LinearScan/Main.hs
--- a/LinearScan/Main.hs
+++ b/LinearScan/Main.hs
@@ -14,35 +14,65 @@
 import qualified LinearScan.Assign as Assign
 import qualified LinearScan.Blocks as Blocks
 import qualified LinearScan.Build as Build
+import qualified LinearScan.IntMap as IntMap
 import qualified LinearScan.LiveSets as LiveSets
+import qualified LinearScan.Loops as Loops
 import qualified LinearScan.Morph as Morph
-import qualified LinearScan.Order as Order
 import qualified LinearScan.Resolve as Resolve
+import qualified LinearScan.ScanState as ScanState
+import qualified LinearScan.Ssrnat as Ssrnat
 
 
+data FinalStage =
+   BuildingIntervalsFailed
+ | AllocatingRegistersFailed
+
+data Details blockType1 blockType2 opType1 opType2 accType =
+   Build_Details (Prelude.Maybe ((,) Morph.SSError FinalStage)) (IntMap.IntMap
+                                                                LiveSets.BlockLiveSets) 
+ ([] blockType1) ([] blockType2) accType (Prelude.Maybe
+                                         ScanState.ScanStateDesc) (Prelude.Maybe
+                                                                  ScanState.ScanStateDesc) 
+ (Blocks.BlockInfo blockType1 blockType2 opType1 opType2) (Blocks.OpInfo
+                                                          accType opType1
+                                                          opType2) Loops.LoopState
+
 linearScan :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) -> (Blocks.OpInfo
-              a5 a3 a4) -> ([] a1) -> a5 -> Prelude.Either Morph.SSError
-              ((,) ([] a2) a5)
+              a5 a3 a4) -> ([] a1) -> a5 -> Details a1 a2 a3 a4 a5
 linearScan maxReg binfo oinfo blocks accum =
-  let {blocks' = Order.computeBlockOrder blocks} in
-  let {liveSets = LiveSets.computeLocalLiveSets maxReg binfo oinfo blocks'}
-  in
-  let {
-   liveSets' = LiveSets.computeGlobalLiveSetsRecursively binfo blocks'
-                 liveSets}
-  in
-  case Build.buildIntervals maxReg binfo oinfo blocks liveSets' of {
-   Prelude.Left err -> Prelude.Left err;
-   Prelude.Right ssig ->
-    case Allocate.walkIntervals maxReg ( ssig) ((Prelude.succ)
-           (Blocks.countOps binfo blocks)) of {
-     Prelude.Left err -> Prelude.Left err;
-     Prelude.Right ssig' ->
-      let {
-       mappings = Resolve.resolveDataFlow maxReg binfo ( ssig') blocks
-                    liveSets'}
-      in
-      Prelude.Right
-      (Assign.assignRegNum maxReg binfo oinfo ( ssig') liveSets' mappings
-        blocks accum)}}
+  case Loops.computeBlockOrder binfo blocks of {
+   (,) loops blocks1 ->
+    let {liveSets = LiveSets.computeLocalLiveSets maxReg binfo oinfo blocks1}
+    in
+    let {
+     liveSets' = LiveSets.computeGlobalLiveSetsRecursively binfo blocks1
+                   liveSets}
+    in
+    case Build.buildIntervals maxReg binfo oinfo blocks1 loops liveSets' of {
+     Prelude.Left err -> Build_Details (Prelude.Just ((,) err
+      BuildingIntervalsFailed)) liveSets' blocks1 [] accum Prelude.Nothing
+      Prelude.Nothing binfo oinfo loops;
+     Prelude.Right ssig ->
+      let {opCount = (Prelude.succ) (Blocks.countOps binfo blocks1)} in
+      case Allocate.walkIntervals maxReg ( ssig) opCount of {
+       Prelude.Left p ->
+        case p of {
+         (,) err ssig' -> Build_Details (Prelude.Just ((,) err
+          AllocatingRegistersFailed)) liveSets' blocks1 [] accum
+          (Prelude.Just ( ssig)) (Prelude.Just ( ssig')) binfo oinfo loops};
+       Prelude.Right ssig' ->
+        let {
+         sd = Allocate.finalizeScanState maxReg ( ssig')
+                (Ssrnat.double opCount)}
+        in
+        let {allocs = Resolve.determineAllocations maxReg sd} in
+        let {
+         mappings = Resolve.resolveDataFlow maxReg binfo allocs blocks1
+                      liveSets'}
+        in
+        case Assign.assignRegNum maxReg binfo oinfo allocs liveSets' mappings
+               blocks1 accum of {
+         (,) blocks2 accum' -> Build_Details Prelude.Nothing liveSets'
+          blocks1 blocks2 accum' (Prelude.Just ( ssig)) (Prelude.Just sd)
+          binfo oinfo loops}}}}
 
diff --git a/LinearScan/Morph.hs b/LinearScan/Morph.hs
--- a/LinearScan/Morph.hs
+++ b/LinearScan/Morph.hs
@@ -40,13 +40,12 @@
 type PhysReg = Prelude.Int
 
 data SSError =
-   ECannotSplitSingleton1 Prelude.Int
+   ERegistersExhausted Prelude.Int
+ | ENoValidSplitPositionUnh Prelude.Int Prelude.Int
+ | ENoValidSplitPosition Prelude.Int Prelude.Int
+ | ECannotSplitSingleton1 Prelude.Int
  | ECannotSplitSingleton2 Prelude.Int
  | ECannotSplitSingleton3 Prelude.Int
- | ECannotSplitSingleton4 Prelude.Int
- | ECannotSplitSingleton5 Prelude.Int
- | ECannotSplitSingleton6 Prelude.Int
- | ECannotSplitSingleton7 Prelude.Int
  | ENoIntervalsToSplit
  | ERegisterAlreadyAssigned Prelude.Int
  | ERegisterAssignmentsOverlap Prelude.Int
@@ -120,12 +119,6 @@
   case _top_assumption_ of {
    Build_SSInfo x x0 -> _evar_0_ x}
 
-weakenHasLen_ :: Prelude.Int -> ScanState.ScanStateDesc -> SState () () ()
-weakenHasLen_ maxReg pre hS =
-  Prelude.Right ((,) ()
-    (case hS of {
-      Build_SSInfo thisDesc0 _ -> Build_SSInfo thisDesc0 __}))
-
 strengthenHasLen :: Prelude.Int -> ScanState.ScanStateDesc ->
                     ScanState.ScanStateDesc -> Prelude.Maybe ()
 strengthenHasLen maxReg pre sd =
@@ -135,6 +128,21 @@
    [] -> _evar_0_ __;
    (:) x x0 -> _evar_0_0 x x0}
 
+moveUnhandledToHandled :: Prelude.Int -> ScanState.ScanStateDesc -> SState 
+                          () () ()
+moveUnhandledToHandled maxReg pre x =
+  case x of {
+   Build_SSInfo thisDesc0 _ ->
+    case thisDesc0 of {
+     ScanState.Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0
+      unhandled0 active0 inactive0 handled0 ->
+      case unhandled0 of {
+       [] -> Logic.coq_False_rect;
+       (:) p unhandled1 -> Prelude.Right ((,) () (Build_SSInfo
+        (ScanState.Build_ScanStateDesc nextInterval0 intervals0
+        fixedIntervals0 unhandled1 active0 inactive0 ((:) ((,)
+        (Prelude.fst p) Prelude.Nothing) handled0)) __))}}}
+
 moveUnhandledToActive :: Prelude.Int -> ScanState.ScanStateDesc -> PhysReg ->
                          SState () () ()
 moveUnhandledToActive maxReg pre reg x =
@@ -176,7 +184,8 @@
           (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd))
           (Fintype.ordinal_eqType maxReg)) x
         (unsafeCoerce (ScanState.active maxReg sd))))
-    (ScanState.inactive maxReg sd) ((:) (unsafeCoerce x)
+    (ScanState.inactive maxReg sd) ((:) ((,) (Prelude.fst (unsafeCoerce x))
+    (Prelude.Just (Prelude.snd (unsafeCoerce x))))
     (ScanState.handled maxReg sd))
 
 moveActiveToInactive :: Prelude.Int -> ScanState.ScanStateDesc ->
@@ -222,6 +231,7 @@
         (Eqtype.prod_eqType
           (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd))
           (Fintype.ordinal_eqType maxReg)) x
-        (unsafeCoerce (ScanState.inactive maxReg sd)))) ((:) (unsafeCoerce x)
-    (ScanState.handled maxReg sd))
+        (unsafeCoerce (ScanState.inactive maxReg sd)))) ((:) ((,)
+    (Prelude.fst (unsafeCoerce x)) (Prelude.Just
+    (Prelude.snd (unsafeCoerce x)))) (ScanState.handled maxReg sd))
 
diff --git a/LinearScan/NonEmpty0.hs b/LinearScan/NonEmpty0.hs
--- a/LinearScan/NonEmpty0.hs
+++ b/LinearScan/NonEmpty0.hs
@@ -11,6 +11,21 @@
 import qualified LinearScan.Utils
 
 
+coq_NonEmpty_rect :: (a1 -> a2) -> (a1 -> ([] a1) -> a2 -> a2) -> ([] 
+                     a1) -> a2
+coq_NonEmpty_rect f f0 n =
+  (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
+    (\y ->
+    f y)
+    (\y n0 ->
+    f0 y n0 (coq_NonEmpty_rect f f0 n0))
+    n
+
+coq_NonEmpty_rec :: (a1 -> a2) -> (a1 -> ([] a1) -> a2 -> a2) -> ([] 
+                    a1) -> a2
+coq_NonEmpty_rec =
+  coq_NonEmpty_rect
+
 coq_NE_from_list :: a1 -> ([] a1) -> [] a1
 coq_NE_from_list x xs =
   case xs of {
diff --git a/LinearScan/Order.hs b/LinearScan/Order.hs
deleted file mode 100644
--- a/LinearScan/Order.hs
+++ /dev/null
@@ -1,17 +0,0 @@
-module LinearScan.Order where
-
-
-import Debug.Trace (trace, traceShow)
-import qualified Prelude
-import qualified Data.IntMap
-import qualified Data.IntSet
-import qualified Data.List
-import qualified Data.Ord
-import qualified Data.Functor.Identity
-import qualified LinearScan.Utils
-
-
-computeBlockOrder :: ([] a1) -> [] a1
-computeBlockOrder blocks =
-  blocks
-
diff --git a/LinearScan/Range.hs b/LinearScan/Range.hs
--- a/LinearScan/Range.hs
+++ b/LinearScan/Range.hs
@@ -54,6 +54,10 @@
   case r of {
    Build_RangeDesc rbeg0 rend0 ups0 -> ups0}
 
+head_or_end :: RangeDesc -> Prelude.Int
+head_or_end rd =
+  UsePos.head_or (rend rd) (ups rd)
+
 getRangeDesc :: RangeDesc -> RangeDesc
 getRangeDesc d =
   d
@@ -62,53 +66,20 @@
 packRange d =
   d
 
-newRange :: UsePos.UsePos -> RangeDesc
-newRange upos =
-  Build_RangeDesc (UsePos.uloc upos) ((Prelude.succ) (UsePos.uloc upos)) ((:)
-    upos [])
+coq_Range_shift :: RangeDesc -> Prelude.Int -> RangeDesc
+coq_Range_shift rd b =
+  Build_RangeDesc b (rend rd) (ups rd)
 
 coq_Range_cons :: UsePos.UsePos -> RangeDesc -> RangeDesc
 coq_Range_cons upos rd =
   Build_RangeDesc (rbeg rd) (rend rd) ((:) upos (ups rd))
 
-type BoundedRange = RangeDesc
-
-emptyBoundedRange :: Prelude.Int -> Prelude.Int -> BoundedRange
-emptyBoundedRange b e =
-  Build_RangeDesc b e []
+range_ltn :: RangeDesc -> RangeDesc -> Prelude.Bool
+range_ltn x y =
+  (Prelude.<=) ((Prelude.succ) (rend ( x))) (rbeg ( y))
 
 type SortedRanges = Specif.Coq_sig2 ([] RangeDesc)
 
-emptySortedRanges :: Prelude.Int -> SortedRanges
-emptySortedRanges b =
-  []
-
-prependRange :: Prelude.Int -> Prelude.Int -> BoundedRange -> SortedRanges ->
-                Prelude.Int -> SortedRanges
-prependRange b e rp ranges pos =
-  let {_evar_0_ = \_ _ -> (:) rp []} in
-  let {
-   _evar_0_0 = \x xs ->
-    let {
-     _evar_0_0 = \_ _ ->
-      let {
-       r' = packRange (Build_RangeDesc (rbeg (getRangeDesc ( rp)))
-              (rend (getRangeDesc ( x)))
-              ((Prelude.++) (ups (getRangeDesc ( rp)))
-                (ups (getRangeDesc ( x)))))}
-      in
-      (:) r' xs}
-    in
-    let {_evar_0_1 = \_ _ -> (:) rp ((:) x xs)} in
-    case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (rend ( rp)))
-           (unsafeCoerce (rbeg ( x))) of {
-     Prelude.True -> _evar_0_0 __ __;
-     Prelude.False -> _evar_0_1 __ __}}
-  in
-  case ranges of {
-   [] -> _evar_0_ __ __;
-   (:) x x0 -> _evar_0_0 x x0}
-
 coq_SortedRanges_cat :: Prelude.Int -> SortedRanges -> Prelude.Int ->
                         SortedRanges -> SortedRanges
 coq_SortedRanges_cat b xs pos ys =
@@ -156,9 +127,12 @@
 
 rangesIntersect :: RangeDesc -> RangeDesc -> Prelude.Bool
 rangesIntersect x y =
-  case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of {
-   Prelude.True -> (Prelude.<=) ((Prelude.succ) (rbeg y)) (rend x);
-   Prelude.False -> (Prelude.<=) ((Prelude.succ) (rbeg x)) (rend y)}
+  (Prelude.||)
+    (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (rend x))
+      (unsafeCoerce (rend y)))
+    (case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of {
+      Prelude.True -> (Prelude.<=) ((Prelude.succ) (rbeg y)) (rend x);
+      Prelude.False -> (Prelude.<=) ((Prelude.succ) (rbeg x)) (rend y)})
 
 rangeIntersectionPoint :: RangeDesc -> RangeDesc -> Prelude.Maybe
                           Lib.Coq_oddnum
@@ -166,8 +140,8 @@
   case rangesIntersect x y of {
    Prelude.True -> Prelude.Just
     (case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of {
-      Prelude.True -> rbeg x;
-      Prelude.False -> rbeg y});
+      Prelude.True -> rbeg y;
+      Prelude.False -> rbeg x});
    Prelude.False -> Prelude.Nothing}
 
 findRangeUsePos :: RangeDesc -> (UsePos.UsePos -> Prelude.Bool) ->
@@ -193,54 +167,44 @@
   in
   Datatypes.list_rec _evar_0_ _evar_0_0 (ups (getRangeDesc rd))
 
-rangeSpan :: Prelude.Int -> RangeDesc ->
-             ((,) (Prelude.Maybe RangeDesc) (Prelude.Maybe RangeDesc))
-rangeSpan before rd =
+type SubRangesOf = ((,) RangeDesc RangeDesc)
+
+rangeSpan :: RangeDesc -> Prelude.Int -> SubRangesOf
+rangeSpan rd before =
   (Prelude.flip (Prelude.$)) __ (\_ ->
     case rd of {
      Build_RangeDesc rbeg0 rend0 ups0 ->
       let {
        _evar_0_ = \l1 l2 ->
         let {
-         _evar_0_ = \_ ->
-          let {
-           _evar_0_ = \_ -> (,) Prelude.Nothing (Prelude.Just
-            (packRange (Build_RangeDesc rbeg0 rend0 ((Prelude.++) l1 l2))))}
-          in
+         _evar_0_ = \_ _ ->
           let {
-           _evar_0_0 = \_ ->
-            let {
-             _evar_0_0 = \_ -> (,) (Prelude.Just
-              (packRange (Build_RangeDesc rbeg0 rend0 ((Prelude.++) l1 l2))))
-              Prelude.Nothing}
-            in
-            let {
-             _evar_0_1 = \_ ->
-              let {
-               _evar_0_1 = \_ ->
-                let {
-                 _evar_0_1 = \_ ->
-                  (Prelude.flip (Prelude.$)) __ (\_ ->
-                    (Prelude.flip (Prelude.$)) __ (\_ -> (,) (Prelude.Just
-                      (packRange (Build_RangeDesc rbeg0 before l1)))
-                      (Prelude.Just
-                      (packRange (Build_RangeDesc before rend0 l2)))))}
-                in
-                 _evar_0_1 __}
-              in
-               _evar_0_1 __}
-            in
-            case (Prelude.<=) rend0 before of {
-             Prelude.True -> _evar_0_0 __;
-             Prelude.False -> _evar_0_1 __}}
+           _evar_0_ = let {
+                       _evar_0_ = let {
+                                   _evar_0_ = \_ ->
+                                    (Prelude.flip (Prelude.$)) __ (\_ ->
+                                      (Prelude.flip (Prelude.$)) __ (\_ ->
+                                        (,)
+                                        (packRange (Build_RangeDesc rbeg0
+                                          before l1))
+                                        (packRange (Build_RangeDesc before
+                                          rend0 l2))))}
+                                  in
+                                   _evar_0_}
+                      in
+                       _evar_0_}
           in
-          case (Prelude.<=) before rbeg0 of {
-           Prelude.True -> _evar_0_ __;
-           Prelude.False -> _evar_0_0 __}}
+           _evar_0_ __}
         in
-         _evar_0_ __}
+         _evar_0_ __ __}
       in
-      case Lib.span (\x ->
-             (Prelude.<=) ((Prelude.succ) (UsePos.uloc x)) before) ups0 of {
+      case Lib.span (\u ->
+             (Prelude.<=) ((Prelude.succ) (UsePos.uloc u)) before) ups0 of {
        (,) x x0 -> _evar_0_ x x0}})
+
+type BoundedRange = RangeDesc
+
+emptyBoundedRange :: Prelude.Int -> Prelude.Int -> BoundedRange
+emptyBoundedRange b e =
+  Build_RangeDesc b e []
 
diff --git a/LinearScan/Resolve.hs b/LinearScan/Resolve.hs
--- a/LinearScan/Resolve.hs
+++ b/LinearScan/Resolve.hs
@@ -16,9 +16,11 @@
 import qualified LinearScan.Blocks as Blocks
 import qualified LinearScan.Graph as Graph
 import qualified LinearScan.IntMap as IntMap
+import qualified LinearScan.Interval as Interval
 import qualified LinearScan.Lib as Lib
 import qualified LinearScan.LiveSets as LiveSets
 import qualified LinearScan.ScanState as ScanState
+import qualified LinearScan.UsePos as UsePos
 import qualified LinearScan.Eqtype as Eqtype
 import qualified LinearScan.Fintype as Fintype
 import qualified LinearScan.Ssrnat as Ssrnat
@@ -35,83 +37,199 @@
 unsafeCoerce = IOExts.unsafeCoerce
 #endif
 
-__ :: any
-__ = Prelude.error "Logical or arity value used"
+type PhysReg = Prelude.Int
 
-checkIntervalBoundary :: Prelude.Int -> ScanState.ScanStateDesc ->
-                         Prelude.Int -> Prelude.Bool ->
-                         LiveSets.BlockLiveSets -> LiveSets.BlockLiveSets ->
-                         (IntMap.IntMap ((,) Graph.Graph Graph.Graph)) ->
-                         Prelude.Int -> IntMap.IntMap
-                         ((,) Graph.Graph Graph.Graph)
-checkIntervalBoundary maxReg sd bid in_from from to mappings vid =
+data Allocation =
+   Build_Allocation Prelude.Int Interval.IntervalDesc (Prelude.Maybe PhysReg)
+
+intVal :: Prelude.Int -> Allocation -> Interval.IntervalDesc
+intVal maxReg a =
+  case a of {
+   Build_Allocation intId intVal0 intReg0 -> intVal0}
+
+intReg :: Prelude.Int -> Allocation -> Prelude.Maybe PhysReg
+intReg maxReg a =
+  case a of {
+   Build_Allocation intId intVal0 intReg0 -> intReg0}
+
+determineAllocations :: Prelude.Int -> ScanState.ScanStateDesc -> []
+                        Allocation
+determineAllocations maxReg sd =
+  Prelude.map (\x -> Build_Allocation ( (Prelude.fst x))
+    (Interval.getIntervalDesc
+      (
+        (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)
+          (ScanState.intervals maxReg sd) (Prelude.fst x)))) (Prelude.snd x))
+    (ScanState.handled maxReg sd)
+
+type RawResolvingMove = (,) (Prelude.Maybe PhysReg) (Prelude.Maybe PhysReg)
+
+data ResolvingMove =
+   Move PhysReg PhysReg
+ | Swap PhysReg PhysReg
+ | Spill PhysReg Blocks.VarId
+ | Restore Blocks.VarId PhysReg
+ | Nop
+
+prepareForGraph :: Prelude.Int -> Eqtype.Equality__Coq_sort ->
+                   RawResolvingMove -> (,)
+                   (Prelude.Maybe Eqtype.Equality__Coq_sort)
+                   (Prelude.Maybe Eqtype.Equality__Coq_sort)
+prepareForGraph maxReg vid x =
+  case x of {
+   (,) o o0 ->
+    case o of {
+     Prelude.Just x0 ->
+      case o0 of {
+       Prelude.Just y -> (,) (Prelude.Just (unsafeCoerce (Prelude.Left x0)))
+        (Prelude.Just (unsafeCoerce (Prelude.Left y)));
+       Prelude.Nothing -> (,) (Prelude.Just (unsafeCoerce (Prelude.Left x0)))
+        (Prelude.Just (unsafeCoerce (Prelude.Right vid)))};
+     Prelude.Nothing ->
+      case o0 of {
+       Prelude.Just y -> (,) (Prelude.Just
+        (unsafeCoerce (Prelude.Right vid))) (Prelude.Just
+        (unsafeCoerce (Prelude.Left y)));
+       Prelude.Nothing -> (,) (Prelude.Just
+        (unsafeCoerce (Prelude.Right vid))) (Prelude.Just
+        (unsafeCoerce (Prelude.Right vid)))}}}
+
+moveFromGraph :: Prelude.Int -> ((,)
+                 (Prelude.Maybe Eqtype.Equality__Coq_sort)
+                 (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> ResolvingMove
+moveFromGraph maxReg mv =
+  case mv of {
+   (,) o o0 ->
+    case o of {
+     Prelude.Just s ->
+      case unsafeCoerce s of {
+       Prelude.Left x ->
+        case o0 of {
+         Prelude.Just s0 ->
+          case unsafeCoerce s0 of {
+           Prelude.Left y -> Move x y;
+           Prelude.Right y -> Spill x y};
+         Prelude.Nothing -> Nop};
+       Prelude.Right x ->
+        case o0 of {
+         Prelude.Just s0 ->
+          case unsafeCoerce s0 of {
+           Prelude.Left y -> Restore x y;
+           Prelude.Right s1 -> Nop};
+         Prelude.Nothing -> Nop}};
+     Prelude.Nothing -> Nop}}
+
+determineMoves :: Prelude.Int -> (IntMap.IntMap RawResolvingMove) -> []
+                  ResolvingMove
+determineMoves maxReg moves =
   let {
-   mfrom_int = ScanState.lookupInterval maxReg sd __ vid
-                 (LiveSets.blockLastOpId from)}
+   graph = Lib.forFold
+             (Graph.emptyGraph
+               (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
+                 Ssrnat.nat_eqType))
+             (unsafeCoerce (IntMap.coq_IntMap_toList moves)) (\g mv ->
+             Graph.addEdge
+               (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
+                 Ssrnat.nat_eqType)
+               (unsafeCoerce
+                 (prepareForGraph maxReg (Prelude.fst mv) (Prelude.snd mv)))
+               g)}
   in
+  Prelude.map (moveFromGraph maxReg)
+    (Graph.topsort
+      (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType)
+      graph)
+
+resolvingMoves :: Prelude.Int -> ([] Allocation) -> Prelude.Int ->
+                  Prelude.Int -> IntMap.IntMap RawResolvingMove
+resolvingMoves maxReg allocs from to =
   let {
-   mto_int = ScanState.lookupInterval maxReg sd __ vid
-               (LiveSets.blockFirstOpId to)}
+   liveAtFrom = IntMap.coq_IntMap_fromList
+                  (Prelude.map (\i -> (,) (Interval.ivar (intVal maxReg i))
+                    i)
+                    (Prelude.filter (\i ->
+                      (Prelude.&&)
+                        ((Prelude.<=) (Interval.ibeg (intVal maxReg i)) from)
+                        ((Prelude.<=) ((Prelude.succ) from)
+                          (Interval.iend (intVal maxReg i)))) allocs))}
   in
-  case Eqtype.eq_op
-         (Eqtype.option_eqType
-           (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd)))
-         (unsafeCoerce mfrom_int) (unsafeCoerce mto_int) of {
-   Prelude.True -> mappings;
-   Prelude.False ->
+  let {
+   liveAtTo = IntMap.coq_IntMap_fromList
+                (Prelude.map (\i -> (,) (Interval.ivar (intVal maxReg i)) i)
+                  (Prelude.filter (\i ->
+                    let {int = intVal maxReg i} in
+                    (Prelude.&&) ((Prelude.<=) (Interval.ibeg int) to)
+                      (case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce to)
+                              (unsafeCoerce (Interval.iend int)) of {
+                        Prelude.True ->
+                         case Interval.lastUsePos int of {
+                          Prelude.Just u -> (Prelude.<=) to (UsePos.uloc u);
+                          Prelude.Nothing -> Prelude.False};
+                        Prelude.False ->
+                         (Prelude.<=) ((Prelude.succ) to) (Interval.iend int)}))
+                    allocs))}
+  in
+  IntMap.coq_IntMap_mergeWithKey (\vid x y ->
+    case Eqtype.eq_op (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))
+           (unsafeCoerce (intReg maxReg x)) (unsafeCoerce (intReg maxReg y)) of {
+     Prelude.True -> Prelude.Nothing;
+     Prelude.False -> Prelude.Just ((,) (intReg maxReg x) (intReg maxReg y))})
+    (\x -> IntMap.emptyIntMap) (\x -> IntMap.emptyIntMap) liveAtFrom liveAtTo
+
+checkBlockBoundary :: Prelude.Int -> ([] Allocation) -> Prelude.Int ->
+                      Prelude.Bool -> LiveSets.BlockLiveSets ->
+                      LiveSets.BlockLiveSets -> IntMap.IntSet ->
+                      (IntMap.IntMap ((,) Graph.Graph Graph.Graph)) ->
+                      IntMap.IntMap ((,) Graph.Graph Graph.Graph)
+checkBlockBoundary maxReg allocs bid in_from from to liveIn mappings =
+  let {
+   select = \acc vid x ->
+    case IntMap.coq_IntSet_member vid liveIn of {
+     Prelude.True -> (:) ((,) vid x) acc;
+     Prelude.False -> acc}}
+  in
+  let {
+   moves = IntMap.coq_IntMap_foldlWithKey select []
+             (resolvingMoves maxReg allocs (LiveSets.blockLastOpId from)
+               (LiveSets.blockFirstOpId to))}
+  in
+  Lib.forFold mappings (unsafeCoerce moves) (\ms mv ->
     let {
-     f = \mi ->
-      case mi of {
-       Prelude.Just i ->
-        case ScanState.lookupRegister maxReg sd __ i of {
-         Prelude.Just r -> Prelude.Left r;
-         Prelude.Nothing -> Prelude.Right vid};
-       Prelude.Nothing -> Prelude.Right vid}}
+     addToGraphs = \e xs ->
+      case xs of {
+       (,) gbeg gend ->
+        case in_from of {
+         Prelude.True -> (,) gbeg
+          (Graph.addEdge
+            (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
+              Ssrnat.nat_eqType) e gend);
+         Prelude.False -> (,)
+          (Graph.addEdge
+            (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
+              Ssrnat.nat_eqType) e gbeg) gend}}}
     in
-    let {sreg = unsafeCoerce f mfrom_int} in
-    let {dreg = unsafeCoerce f mto_int} in
-    case Eqtype.eq_op
-           (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
-             Ssrnat.nat_eqType) sreg dreg of {
-     Prelude.True -> mappings;
-     Prelude.False ->
-      let {
-       addToGraphs = \e xs ->
-        case xs of {
-         (,) gbeg gend ->
-          case in_from of {
-           Prelude.True -> (,) gbeg
-            (Graph.addEdge
-              (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
-                Ssrnat.nat_eqType) e gend);
-           Prelude.False -> (,)
-            (Graph.addEdge
-              (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
-                Ssrnat.nat_eqType) e gbeg) gend}}}
-      in
-      let {
-       f0 = \mxs ->
-        let {e = (,) (Prelude.Just sreg) (Prelude.Just dreg)} in
-        Prelude.Just
-        (unsafeCoerce addToGraphs e
-          (case mxs of {
-            Prelude.Just xs -> xs;
-            Prelude.Nothing -> (,)
-             (Graph.emptyGraph
-               (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
-                 Ssrnat.nat_eqType))
-             (Graph.emptyGraph
-               (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
-                 Ssrnat.nat_eqType))}))}
-      in
-      IntMap.coq_IntMap_alter f0 bid mappings}}
+    let {
+     f = \mxs ->
+      unsafeCoerce addToGraphs
+        (prepareForGraph maxReg (Prelude.fst mv) (Prelude.snd mv))
+        (case mxs of {
+          Prelude.Just xs -> xs;
+          Prelude.Nothing -> (,)
+           (Graph.emptyGraph
+             (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
+               Ssrnat.nat_eqType))
+           (Graph.emptyGraph
+             (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
+               Ssrnat.nat_eqType))})}
+    in
+    IntMap.coq_IntMap_alter ((Prelude..) (\x -> Prelude.Just x) f) bid ms)
 
 type BlockMoves = (,) Graph.Graph Graph.Graph
 
-resolveDataFlow :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->
-                   ScanState.ScanStateDesc -> ([] a1) -> (IntMap.IntMap
+resolveDataFlow :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) -> ([]
+                   Allocation) -> ([] a1) -> (IntMap.IntMap
                    LiveSets.BlockLiveSets) -> IntMap.IntMap BlockMoves
-resolveDataFlow maxReg binfo sd blocks liveSets =
+resolveDataFlow maxReg binfo allocs blocks liveSets =
   Lib.forFold IntMap.emptyIntMap blocks (\mappings b ->
     let {bid = Blocks.blockId binfo b} in
     case IntMap.coq_IntMap_lookup bid liveSets of {
@@ -129,8 +247,8 @@
                   Prelude.True -> bid;
                   Prelude.False -> s_bid}}
           in
-          IntMap.coq_IntSet_forFold ms (LiveSets.blockLiveIn to)
-            (checkIntervalBoundary maxReg sd key in_from from to);
+          checkBlockBoundary maxReg allocs key in_from from to
+            (LiveSets.blockLiveIn to) ms;
          Prelude.Nothing -> ms});
      Prelude.Nothing -> mappings})
 
diff --git a/LinearScan/ScanState.hs b/LinearScan/ScanState.hs
--- a/LinearScan/ScanState.hs
+++ b/LinearScan/ScanState.hs
@@ -1,6 +1,3 @@
-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}
-{- For Hugs, use the option -F"cpp -P -traditional" -}
-
 module LinearScan.ScanState where
 
 
@@ -15,22 +12,8 @@
 
 import qualified LinearScan.Interval as Interval
 import qualified LinearScan.Lib as Lib
-import qualified LinearScan.Eqtype as Eqtype
-import qualified LinearScan.Fintype as Fintype
-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
-
 type PhysReg = Prelude.Int
 
 type FixedIntervalsType = [] (Prelude.Maybe Interval.IntervalDesc)
@@ -41,7 +24,7 @@
                                                                    ((,)
                                                                    Prelude.Int
                                                                    PhysReg)) 
- ([] ((,) Prelude.Int PhysReg))
+ ([] ((,) Prelude.Int (Prelude.Maybe PhysReg)))
 
 nextInterval :: Prelude.Int -> ScanStateDesc -> Prelude.Int
 nextInterval maxReg s =
@@ -81,7 +64,8 @@
    Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0 unhandled0
     active0 inactive0 handled0 -> inactive0}
 
-handled :: Prelude.Int -> ScanStateDesc -> [] ((,) IntervalId PhysReg)
+handled :: Prelude.Int -> ScanStateDesc -> []
+           ((,) IntervalId (Prelude.Maybe PhysReg))
 handled maxReg s =
   case s of {
    Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0 unhandled0
@@ -103,47 +87,6 @@
          Prelude.Nothing -> (,) reg Prelude.Nothing};
        Prelude.Nothing -> (,) r Prelude.Nothing}}) ((,) ( 0) (Prelude.Just
     Lib.odd1))
-
-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 :: Prelude.Int -> ScanStateDesc -> a1 -> Prelude.Int ->
-                  Prelude.Int -> Prelude.Maybe IntervalId
-lookupInterval maxReg 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 maxReg sd) f
-    Prelude.Nothing (intervals maxReg sd)
-
-lookupRegister :: Prelude.Int -> ScanStateDesc -> a1 ->
-                  Eqtype.Equality__Coq_sort -> Prelude.Maybe PhysReg
-lookupRegister maxReg sd st intid =
-  Lib.forFold Prelude.Nothing
-    ((Prelude.++) (unsafeCoerce (handled maxReg sd))
-      ((Prelude.++) (unsafeCoerce (active maxReg sd))
-        (unsafeCoerce (inactive maxReg 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 maxReg sd))
-               xid intid of {
-         Prelude.True -> Prelude.Just reg;
-         Prelude.False -> Prelude.Nothing}}})
 
 data ScanStateStatus =
    Pending
diff --git a/LinearScan/Seq.hs b/LinearScan/Seq.hs
--- a/LinearScan/Seq.hs
+++ b/LinearScan/Seq.hs
@@ -39,6 +39,12 @@
   Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Data.List.length s))
     (unsafeCoerce 0)
 
+head :: a1 -> ([] a1) -> a1
+head x0 s =
+  case s of {
+   [] -> x0;
+   (:) x l -> x}
+
 rcons :: ([] a1) -> a1 -> [] a1
 rcons s z =
   case s of {
@@ -71,6 +77,19 @@
   case s of {
    [] -> _evar_0_;
    (:) x x0 -> _evar_0_0 x x0}
+
+last_ind :: a2 -> (([] a1) -> a1 -> a2 -> a2) -> ([] a1) -> a2
+last_ind hnil hlast s =
+  let {
+   _evar_0_ = let {_evar_0_ = \s1 hs1 ->  hs1} in
+              let {
+               _evar_0_0 = \x s2 iHs s1 hs1 ->
+                let {_evar_0_0 = iHs (rcons s1 x) (hlast s1 x hs1)} in
+                 _evar_0_0}
+              in
+              Datatypes.list_rect _evar_0_ _evar_0_0 s [] hnil}
+  in
+   _evar_0_
 
 find :: (Ssrbool.Coq_pred a1) -> ([] a1) -> Prelude.Int
 find a s =
diff --git a/LinearScan/Split.hs b/LinearScan/Split.hs
--- a/LinearScan/Split.hs
+++ b/LinearScan/Split.hs
@@ -23,6 +23,7 @@
 import qualified LinearScan.Fintype as Fintype
 import qualified LinearScan.Seq as Seq
 import qualified LinearScan.Ssrbool as Ssrbool
+import qualified LinearScan.Ssrnat as Ssrnat
 
 
 
@@ -43,393 +44,140 @@
 
 data SplitPosition =
    BeforePos Lib.Coq_oddnum
- | BeforeFirstUsePosReqReg
- | EndOfLifetimeHole
+ | EndOfLifetimeHole Lib.Coq_oddnum
 
-splitPosition :: Interval.IntervalDesc -> SplitPosition -> Prelude.Maybe
-                 Lib.Coq_oddnum
+splitPosition :: Interval.IntervalDesc -> SplitPosition -> Lib.Coq_oddnum
 splitPosition d pos =
   case pos of {
-   BeforePos x -> Prelude.Just x;
-   BeforeFirstUsePosReqReg ->
-    Interval.firstUseReqReg (Interval.getIntervalDesc d);
-   EndOfLifetimeHole -> Prelude.Nothing}
+   BeforePos n -> n;
+   EndOfLifetimeHole n ->
+    Interval.afterLifetimeHole (Interval.getIntervalDesc d) n}
 
-splitInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
-                 ScanState.IntervalId -> SplitPosition -> Prelude.Bool ->
-                 Prelude.Either Morph.SSError
-                 (Prelude.Maybe ScanState.ScanStateSig)
-splitInterval maxReg sd uid pos forCurrent =
+splitUnhandledInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
+                          ScanState.IntervalId -> Prelude.Int -> ([]
+                          ((,) ScanState.IntervalId Prelude.Int)) ->
+                          SplitPosition -> Prelude.Either Morph.SSError
+                          (Prelude.Maybe ScanState.ScanStateSig)
+splitUnhandledInterval maxReg sd uid beg us pos =
   let {
-   _evar_0_ = \_nextInterval_ ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 ->
-    let {
-     _evar_0_ = \uid1 -> Prelude.Left (Morph.ECannotSplitSingleton1 ( uid1))}
-    in
+   _evar_0_ = \_nextInterval_ ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 us0 ->
+    let {int = LinearScan.Utils.nth _nextInterval_ ints uid0} in
+    let {splitPos = splitPosition ( int) pos} in
     let {
-     _evar_0_0 = \_top_assumption_ ->
+     _evar_0_ = \_ ->
       let {
-       _evar_0_0 = \u beg us uid1 ->
-        let {int = LinearScan.Utils.nth _nextInterval_ ints uid1} in
+       _evar_0_ = \iv ib ie rds ->
         let {
-         _evar_0_0 = \_top_assumption_0 ->
+         _top_assumption_ = Interval.splitInterval
+                              (Interval.Build_IntervalDesc iv ib ie rds)
+                              splitPos}
+        in
+        let {
+         _evar_0_ = \i0 i1 ->
           let {
-           _evar_0_0 = \_ ->
-            (Prelude.flip (Prelude.$)) __ (\_ ->
-              let {
-               _evar_0_0 = \iv ib ie _iknd_ rds ->
-                let {
-                 _top_assumption_1 = Interval.intervalSpan rds
-                                       _top_assumption_0 iv ib ie _iknd_}
-                in
-                let {
-                 _evar_0_0 = \_top_assumption_2 ->
-                  let {
-                   _evar_0_0 = \_top_assumption_3 _top_assumption_4 ->
-                    let {
-                     _evar_0_0 = \_top_assumption_5 ->
-                      let {
-                       _evar_0_0 = \_ ->
+           _evar_0_ = let {
+                       _evar_0_ = \_ _ ->
                         let {
-                         _evar_0_0 = \_ ->
-                          let {
-                           set_int_desc = ScanState.Build_ScanStateDesc
-                            _nextInterval_
-                            (LinearScan.Utils.set_nth _nextInterval_ ints
-                              uid1 _top_assumption_3) _fixedIntervals_ ((:)
-                            ((,) u beg) us) _active_ _inactive_ _handled_}
-                          in
-                          let {
-                           _evar_0_0 = \_ ->
-                            (Prelude.flip (Prelude.$)) __
-                              (let {
-                                new_unhandled = ScanState.Build_ScanStateDesc
-                                 ((Prelude.succ) _nextInterval_)
-                                 (LinearScan.Utils.snoc _nextInterval_
-                                   (LinearScan.Utils.set_nth _nextInterval_
-                                     ints uid1 _top_assumption_3)
-                                   _top_assumption_5) _fixedIntervals_
-                                 (Lib.insert (Lib.lebf Prelude.snd) ((,)
-                                   ( _nextInterval_)
-                                   (Interval.ibeg _top_assumption_5)) ((:)
-                                   (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
-                               (ScanState.packScanState maxReg
-                                 ScanState.InUse new_unhandled)))}
-                          in
-                          let {
-                           _evar_0_1 = \_ ->
-                            let {
-                             _evar_0_1 = \_top_assumption_6 ->
-                              let {
-                               _evar_0_1 = \_ ->
-                                let {
-                                 _evar_0_1 = \iv1 ib1 ie1 _iknd1_ rds1 ->
-                                  let {
-                                   _top_assumption_7 = Interval.intervalSpan
-                                                         rds1
-                                                         _top_assumption_6
-                                                         iv1 ib1 ie1 _iknd1_}
-                                  in
-                                  let {
-                                   _evar_0_1 = \_top_assumption_8 ->
-                                    let {
-                                     _evar_0_1 = \_top_assumption_9 _top_assumption_10 ->
-                                      let {
-                                       _evar_0_1 = \_top_assumption_11 ->
-                                        (Prelude.flip (Prelude.$)) __
-                                          (let {
-                                            new_unhandled = ScanState.Build_ScanStateDesc
-                                             ((Prelude.succ) _nextInterval_)
-                                             (LinearScan.Utils.snoc
-                                               _nextInterval_
-                                               (LinearScan.Utils.set_nth
-                                                 _nextInterval_ ints uid1
-                                                 _top_assumption_3)
-                                               _top_assumption_11)
-                                             _fixedIntervals_
-                                             (Lib.insert
-                                               (Lib.lebf Prelude.snd) ((,)
-                                               ( _nextInterval_)
-                                               (Interval.ibeg
-                                                 _top_assumption_11)) ((:)
-                                               (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
-                                           let {
-                                            _evar_0_1 = \_ _ -> Prelude.Right
-                                             (Prelude.Just
-                                             (ScanState.packScanState maxReg
-                                               ScanState.InUse new_unhandled))}
-                                           in
-                                           let {
-                                            _evar_0_2 = \_ _ -> Prelude.Left
-                                             (Morph.ECannotSplitSingleton3
-                                             ( uid1))}
-                                           in
-                                           case (Prelude.<=) ((Prelude.succ)
-                                                  beg)
-                                                  (Interval.ibeg
-                                                    _top_assumption_11) of {
-                                            Prelude.True -> _evar_0_1 __;
-                                            Prelude.False -> _evar_0_2 __})}
-                                      in
-                                      let {
-                                       _evar_0_2 = \_ -> Prelude.Right
-                                        (Prelude.Just
-                                        (ScanState.packScanState maxReg
-                                          ScanState.InUse set_int_desc))}
-                                      in
-                                      case _top_assumption_10 of {
-                                       Prelude.Just x -> (\_ -> _evar_0_1 x);
-                                       Prelude.Nothing -> _evar_0_2}}
-                                    in
-                                    let {
-                                     _evar_0_2 = \_top_assumption_9 ->
-                                      let {
-                                       _evar_0_2 = \_top_assumption_10 ->
-                                        (Prelude.flip (Prelude.$)) __
-                                          (let {
-                                            new_unhandled = ScanState.Build_ScanStateDesc
-                                             ((Prelude.succ) _nextInterval_)
-                                             (LinearScan.Utils.snoc
-                                               _nextInterval_
-                                               (LinearScan.Utils.set_nth
-                                                 _nextInterval_ ints uid1
-                                                 _top_assumption_3)
-                                               _top_assumption_10)
-                                             _fixedIntervals_
-                                             (Lib.insert
-                                               (Lib.lebf Prelude.snd) ((,)
-                                               ( _nextInterval_)
-                                               (Interval.ibeg
-                                                 _top_assumption_10)) ((:)
-                                               (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
-                                           let {
-                                            _evar_0_2 = \_ _ -> Prelude.Right
-                                             (Prelude.Just
-                                             (ScanState.packScanState maxReg
-                                               ScanState.InUse new_unhandled))}
-                                           in
-                                           let {
-                                            _evar_0_3 = \_ _ -> Prelude.Left
-                                             (Morph.ECannotSplitSingleton3
-                                             ( uid1))}
-                                           in
-                                           case (Prelude.<=) ((Prelude.succ)
-                                                  beg)
-                                                  (Interval.ibeg
-                                                    _top_assumption_10) of {
-                                            Prelude.True -> _evar_0_2 __;
-                                            Prelude.False -> _evar_0_3 __})}
-                                      in
-                                      let {
-                                       _evar_0_3 = \_ ->
-                                        Logic.coq_False_rect}
-                                      in
-                                      case _top_assumption_9 of {
-                                       Prelude.Just x -> (\_ -> _evar_0_2 x);
-                                       Prelude.Nothing -> _evar_0_3}}
-                                    in
-                                    case _top_assumption_8 of {
-                                     Prelude.Just x -> _evar_0_1 x;
-                                     Prelude.Nothing -> _evar_0_2}}
-                                  in
-                                  case _top_assumption_7 of {
-                                   (,) x x0 -> _evar_0_1 x x0 __}}
-                                in
-                                case _top_assumption_5 of {
-                                 Interval.Build_IntervalDesc x x0 x1 x2 x3 ->
-                                  _evar_0_1 x x0 x1 x2 x3}}
-                              in
-                              let {
-                               _evar_0_2 = \_ -> Prelude.Left
-                                (Morph.ECannotSplitSingleton2 ( uid1))}
-                              in
-                              case (Prelude.&&)
-                                     ((Prelude.<=) ((Prelude.succ)
-                                       (Interval.ibeg _top_assumption_5))
-                                       _top_assumption_6)
-                                     ((Prelude.<=) ((Prelude.succ)
-                                       _top_assumption_6)
-                                       (Interval.iend _top_assumption_5)) of {
-                               Prelude.True -> _evar_0_1 __;
-                               Prelude.False -> _evar_0_2 __}}
-                            in
+                         _evar_0_ = \_discharged_uid_ _discharged_us_ ->
+                          Logic.coq_False_rect}
+                        in
+                        let {
+                         _evar_0_0 = \x xs uid1 us1 ->
+                          (Prelude.flip (Prelude.$)) __ (\_ ->
                             let {
-                             _evar_0_2 = Prelude.Right (Prelude.Just
-                              (ScanState.packScanState maxReg ScanState.InUse
-                                set_int_desc))}
+                             _evar_0_0 = \_ ->
+                              (Prelude.flip (Prelude.$)) __
+                                (let {
+                                  _evar_0_0 = let {
+                                               _evar_0_0 = (Prelude.flip (Prelude.$))
+                                                             __ (\_ _ ->
+                                                             Prelude.Right
+                                                             (Prelude.Just
+                                                             (ScanState.packScanState
+                                                               maxReg
+                                                               ScanState.InUse
+                                                               (ScanState.Build_ScanStateDesc
+                                                               ((Prelude.succ)
+                                                               _nextInterval_)
+                                                               (LinearScan.Utils.snoc
+                                                                 _nextInterval_
+                                                                 (LinearScan.Utils.set_nth
+                                                                   _nextInterval_
+                                                                   ints uid1
+                                                                   ( i0))
+                                                                 ( i1))
+                                                               _fixedIntervals_
+                                                               (Lib.insert
+                                                                 (Lib.lebf
+                                                                   Prelude.snd)
+                                                                 ((,)
+                                                                 (
+                                                                   _nextInterval_)
+                                                                 (Interval.ibeg
+                                                                   ( i1)))
+                                                                 ((:)
+                                                                 (Prelude.id
+                                                                   ((,) uid1
+                                                                   beg))
+                                                                 (Prelude.map
+                                                                   Prelude.id
+                                                                   us1)))
+                                                               (Prelude.map
+                                                                 Prelude.id
+                                                                 _active_)
+                                                               (Prelude.map
+                                                                 Prelude.id
+                                                                 _inactive_)
+                                                               (Prelude.map
+                                                                 Prelude.id
+                                                                 _handled_)))))}
+                                              in
+                                               _evar_0_0}
+                                 in
+                                  _evar_0_0)}
                             in
-                            case splitPosition _top_assumption_5
-                                   BeforeFirstUsePosReqReg of {
-                             Prelude.Just x -> _evar_0_1 x;
-                             Prelude.Nothing -> _evar_0_2}}
-                          in
-                          case (Prelude.<=) ((Prelude.succ) beg)
-                                 (Interval.ibeg _top_assumption_5) of {
-                           Prelude.True -> _evar_0_0 __;
-                           Prelude.False -> _evar_0_1 __}}
+                             _evar_0_0 __)}
                         in
-                         _evar_0_0 __}
-                      in
-                       _evar_0_0 __}
-                    in
-                    let {
-                     _evar_0_1 = \_ ->
-                      let {
-                       _evar_0_1 = Prelude.Left (Morph.ECannotSplitSingleton4
-                        ( uid1))}
-                      in
-                      let {
-                       _evar_0_2 = let {
-                                    _evar_0_2 = \_ ->
-                                     let {
-                                      _evar_0_2 = \_ ->
-                                       let {
-                                        set_int_desc = ScanState.Build_ScanStateDesc
-                                         _nextInterval_
-                                         (LinearScan.Utils.set_nth
-                                           _nextInterval_ ints uid1
-                                           _top_assumption_3)
-                                         _fixedIntervals_ ((:) ((,) u beg)
-                                         us) _active_ _inactive_ _handled_}
-                                       in
-                                       Prelude.Right (Prelude.Just
-                                       (ScanState.packScanState maxReg
-                                         ScanState.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_4 of {
-                     Prelude.Just x -> (\_ -> _evar_0_0 x);
-                     Prelude.Nothing -> _evar_0_1}}
-                  in
-                  let {
-                   _evar_0_1 = \_top_assumption_3 ->
-                    let {
-                     _evar_0_1 = \_top_assumption_4 ->
-                      let {
-                       _evar_0_1 = \_ ->
-                        (Prelude.flip (Prelude.$)) __
-                          (let {
-                            new_unhandled = ScanState.Build_ScanStateDesc
-                             ((Prelude.succ) _nextInterval_)
-                             (LinearScan.Utils.snoc _nextInterval_ ints
-                               _top_assumption_4) _fixedIntervals_
-                             (Lib.insert (Lib.lebf 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
-                           (ScanState.packScanState maxReg ScanState.InUse
-                             new_unhandled)))}
-                      in
-                      let {
-                       _evar_0_2 = \_ -> Prelude.Left
-                        (Morph.ECannotSplitSingleton5 ( uid1))}
+                        case unh of {
+                         [] -> _evar_0_ uid0 us0;
+                         (:) x x0 -> _evar_0_0 x x0 uid0 us0}}
                       in
-                      case (Prelude.<=) ((Prelude.succ) beg)
-                             (Interval.ibeg _top_assumption_4) of {
-                       Prelude.True -> _evar_0_1 __;
-                       Prelude.False -> _evar_0_2 __}}
-                    in
-                    let {_evar_0_2 = \_ -> Logic.coq_False_rect} in
-                    case _top_assumption_3 of {
-                     Prelude.Just x -> (\_ -> _evar_0_1 x);
-                     Prelude.Nothing -> _evar_0_2}}
-                  in
-                  case _top_assumption_2 of {
-                   Prelude.Just x -> _evar_0_0 x;
-                   Prelude.Nothing -> _evar_0_1}}
-                in
-                case _top_assumption_1 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 (Morph.ECannotSplitSingleton2
-            ( uid1))}
+                       _evar_0_ __}
           in
-          case (Prelude.&&)
-                 ((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int)))
-                   _top_assumption_0)
-                 ((Prelude.<=) ((Prelude.succ) _top_assumption_0)
-                   (Interval.iend ( int))) of {
-           Prelude.True -> _evar_0_0 __;
-           Prelude.False -> _evar_0_1 __}}
+           _evar_0_ __}
         in
-        let {_evar_0_1 = Prelude.Right Prelude.Nothing} in
-        case splitPosition ( int) pos of {
-         Prelude.Just x -> _evar_0_0 x;
-         Prelude.Nothing -> _evar_0_1}}
+        case _top_assumption_ of {
+         (,) x x0 -> _evar_0_ x x0}}
       in
-      (\us _ uid1 ->
-      case _top_assumption_ of {
-       (,) x x0 -> _evar_0_0 x x0 us uid1})}
+      case int of {
+       Interval.Build_IntervalDesc x x0 x1 x2 -> _evar_0_ x x0 x1 x2}}
     in
-    case unh of {
-     [] -> _evar_0_ uid0;
-     (:) x x0 -> _evar_0_0 x x0 __ uid0}}
+    let {
+     _evar_0_0 = \_ -> Prelude.Left (Morph.ENoValidSplitPositionUnh ( uid0)
+      splitPos)}
+    in
+    case (Prelude.&&)
+           ((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int))) splitPos)
+           ((Prelude.<=) splitPos (Interval.iend ( int))) of {
+     Prelude.True -> _evar_0_ __;
+     Prelude.False -> _evar_0_0 __}}
   in
   case sd of {
    ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
-    _evar_0_ x x0 x1 x2 x3 x4 x5 uid}
+    _evar_0_ x x0 x1 x2 x3 x4 x5 uid us}
 
 splitCurrentInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
                         SplitPosition -> Morph.SState () () ()
 splitCurrentInterval maxReg pre pos ssi =
   let {
    _evar_0_ = \desc ->
+    let {_evar_0_ = \_ _ _ _ _ -> Logic.coq_False_rect} in
     let {
-     _evar_0_ = \_nextInterval_ intervals0 _fixedIntervals_ unhandled0 _active_ _inactive_ _handled_ ->
-      let {_evar_0_ = \_ _ _ _ _ -> Logic.coq_False_rect} in
+     _evar_0_0 = \_top_assumption_ ->
       let {
-       _evar_0_0 = \_top_assumption_ ->
+       _evar_0_0 = \uid beg us ->
         let {
-         _evar_0_0 = \uid beg us ->
-          let {
-           desc0 = ScanState.Build_ScanStateDesc _nextInterval_ intervals0
-            _fixedIntervals_ ((:) ((,) uid beg) us) _active_ _inactive_
-            _handled_}
-          in
-          (\_ _ _ _ ->
-          let {
-           _top_assumption_0 = splitInterval maxReg desc0 uid pos
-                                 Prelude.True}
-          in
+         _evar_0_0 = \_nextInterval_ intervals0 _fixedIntervals_ unhandled0 _active_ _inactive_ _handled_ uid0 us0 _top_assumption_0 ->
           let {_evar_0_0 = \err -> Prelude.Left err} in
           let {
            _evar_0_1 = \_top_assumption_1 ->
@@ -438,7 +186,7 @@
               (Morph.Build_SSInfo _top_assumption_2 __))}
             in
             let {
-             _evar_0_2 = Prelude.Left (Morph.ECannotSplitSingleton6 ( uid))}
+             _evar_0_2 = Prelude.Left (Morph.ECannotSplitSingleton1 ( uid0))}
             in
             case _top_assumption_1 of {
              Prelude.Just x -> _evar_0_1 x;
@@ -446,23 +194,218 @@
           in
           case _top_assumption_0 of {
            Prelude.Left x -> _evar_0_0 x;
-           Prelude.Right x -> _evar_0_1 x})}
+           Prelude.Right x -> _evar_0_1 x}}
         in
-        (\us _ ->
-        case _top_assumption_ of {
-         (,) x x0 -> _evar_0_0 x x0 us})}
+        case desc of {
+         ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
+          _evar_0_0 x x0 x1 x2 x3 x4 x5 uid us
+            (splitUnhandledInterval maxReg desc uid beg us pos)}}
       in
-      case unhandled0 of {
-       [] -> _evar_0_ __;
-       (:) x x0 -> _evar_0_0 x x0 __}}
+      (\us _ _ _ _ _ ->
+      case _top_assumption_ of {
+       (,) x x0 -> _evar_0_0 x x0 us})}
     in
-    case desc of {
-     ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
-      _evar_0_ x x0 x1 x2 x3 x4 x5 __ __ __}}
+    case ScanState.unhandled maxReg desc of {
+     [] -> _evar_0_ __ __ __ __;
+     (:) x x0 -> _evar_0_0 x x0 __ __ __ __}}
   in
   case ssi of {
    Morph.Build_SSInfo x x0 -> _evar_0_ x __}
 
+splitActiveOrInactiveInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
+                                 ScanState.IntervalId -> Prelude.Int -> ([]
+                                 ((,) ScanState.IntervalId Prelude.Int)) ->
+                                 ScanState.IntervalId -> SplitPosition ->
+                                 Prelude.Either Morph.SSError
+                                 (Prelude.Maybe ScanState.ScanStateSig)
+splitActiveOrInactiveInterval maxReg sd uid beg us xid pos =
+  let {
+   _evar_0_ = \_nextInterval_ ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 us0 xid0 ->
+    let {int = LinearScan.Utils.nth _nextInterval_ ints xid0} in
+    let {splitPos = splitPosition ( int) pos} in
+    let {
+     _evar_0_ = \_ ->
+      let {
+       _evar_0_ = \iv ib ie rds ->
+        let {
+         _top_assumption_ = Interval.splitInterval
+                              (Interval.Build_IntervalDesc iv ib ie rds)
+                              splitPos}
+        in
+        let {
+         _evar_0_ = \i0 i1 ->
+          let {
+           _evar_0_ = let {
+                       _evar_0_ = \_ _ ->
+                        let {
+                         _evar_0_ = \_top_assumption_0 ->
+                          let {
+                           _evar_0_ = \_ ->
+                            (Prelude.flip (Prelude.$)) __
+                              (let {
+                                _evar_0_ = let {
+                                            _evar_0_ = \_ _ -> Prelude.Left
+                                             (Morph.ENoValidSplitPosition
+                                             ( xid0) _top_assumption_0)}
+                                           in
+                                           let {
+                                            _evar_0_0 = \_ ->
+                                             let {
+                                              _evar_0_0 = \_ _ ->
+                                               Prelude.Right (Prelude.Just
+                                               (ScanState.packScanState
+                                                 maxReg ScanState.InUse
+                                                 (ScanState.Build_ScanStateDesc
+                                                 ((Prelude.succ)
+                                                 _nextInterval_)
+                                                 (LinearScan.Utils.snoc
+                                                   _nextInterval_
+                                                   (LinearScan.Utils.set_nth
+                                                     _nextInterval_ ints xid0
+                                                     ( i0)) ( i1))
+                                                 _fixedIntervals_
+                                                 (Lib.insert
+                                                   (Lib.lebf Prelude.snd)
+                                                   ((,) ( _nextInterval_)
+                                                   (Interval.ibeg ( i1)))
+                                                   ((:)
+                                                   (Prelude.id ((,) uid0
+                                                     beg))
+                                                   (Prelude.map Prelude.id
+                                                     us0)))
+                                                 (Prelude.map Prelude.id
+                                                   _active_)
+                                                 (Prelude.map Prelude.id
+                                                   _inactive_)
+                                                 (Prelude.map Prelude.id
+                                                   _handled_))))}
+                                             in
+                                              _evar_0_0 __}
+                                           in
+                                           case (Prelude.<=)
+                                                  (Interval.ibeg ( i1)) beg of {
+                                            Prelude.True -> _evar_0_ __;
+                                            Prelude.False -> _evar_0_0 __}}
+                               in
+                                _evar_0_)}
+                          in
+                          let {
+                           _evar_0_0 = \_ ->
+                            (Prelude.flip (Prelude.$)) __ (\_ ->
+                              let {
+                               _top_assumption_1 = Interval.splitInterval
+                                                     ( i1) _top_assumption_0}
+                              in
+                              let {
+                               _evar_0_0 = \i1_0 i1_1 ->
+                                (Prelude.flip (Prelude.$)) __
+                                  (let {
+                                    _evar_0_0 = (Prelude.flip (Prelude.$)) __
+                                                  (\_ _ -> Prelude.Right
+                                                  (Prelude.Just
+                                                  (ScanState.packScanState
+                                                    maxReg ScanState.InUse
+                                                    (ScanState.Build_ScanStateDesc
+                                                    ((Prelude.succ)
+                                                    ((Prelude.succ)
+                                                    _nextInterval_))
+                                                    (LinearScan.Utils.snoc
+                                                      ((Prelude.succ)
+                                                      _nextInterval_)
+                                                      (LinearScan.Utils.snoc
+                                                        _nextInterval_
+                                                        (LinearScan.Utils.set_nth
+                                                          _nextInterval_ ints
+                                                          xid0 ( i0))
+                                                        ( i1_1)) ( i1_0))
+                                                    _fixedIntervals_
+                                                    (Prelude.map Prelude.id
+                                                      (Lib.insert
+                                                        (Lib.lebf
+                                                          Prelude.snd) ((,)
+                                                        ( _nextInterval_)
+                                                        (Interval.ibeg
+                                                          ( i1_1))) ((:)
+                                                        (Prelude.id ((,) uid0
+                                                          beg))
+                                                        (Prelude.map
+                                                          Prelude.id us0))))
+                                                    (Prelude.map Prelude.id
+                                                      (Prelude.map Prelude.id
+                                                        _active_))
+                                                    (Prelude.map Prelude.id
+                                                      (Prelude.map Prelude.id
+                                                        _inactive_)) ((:)
+                                                    ((,)
+                                                    ( ((Prelude.succ)
+                                                      _nextInterval_))
+                                                    Prelude.Nothing)
+                                                    (Prelude.map Prelude.id
+                                                      (Prelude.map Prelude.id
+                                                        _handled_)))))))}
+                                   in
+                                    _evar_0_0)}
+                              in
+                              case _top_assumption_1 of {
+                               (,) x x0 -> _evar_0_0 x x0})}
+                          in
+                          case Eqtype.eq_op Ssrnat.nat_eqType
+                                 (unsafeCoerce (Interval.ibeg ( i1)))
+                                 (unsafeCoerce _top_assumption_0) of {
+                           Prelude.True -> _evar_0_ __;
+                           Prelude.False -> _evar_0_0 __}}
+                        in
+                        let {
+                         _evar_0_0 = let {
+                                      _evar_0_0 = \_ -> Prelude.Right
+                                       (Prelude.Just
+                                       (ScanState.packScanState maxReg
+                                         ScanState.InUse
+                                         (ScanState.Build_ScanStateDesc
+                                         ((Prelude.succ) _nextInterval_)
+                                         (LinearScan.Utils.snoc
+                                           _nextInterval_
+                                           (LinearScan.Utils.set_nth
+                                             _nextInterval_ ints xid0 
+                                             ( i0)) ( i1)) _fixedIntervals_
+                                         ((:) (Prelude.id ((,) uid0 beg))
+                                         (Prelude.map Prelude.id us0))
+                                         (Prelude.map Prelude.id _active_)
+                                         (Prelude.map Prelude.id _inactive_)
+                                         ((:) ((,) ( _nextInterval_)
+                                         Prelude.Nothing)
+                                         (Prelude.map Prelude.id _handled_)))))}
+                                     in
+                                      _evar_0_0 __}
+                        in
+                        case Interval.firstUseReqReg ( i1) of {
+                         Prelude.Just x -> _evar_0_ x;
+                         Prelude.Nothing -> _evar_0_0}}
+                      in
+                       _evar_0_ __}
+          in
+           _evar_0_ __}
+        in
+        case _top_assumption_ of {
+         (,) x x0 -> _evar_0_ x x0}}
+      in
+      case int of {
+       Interval.Build_IntervalDesc x x0 x1 x2 -> _evar_0_ x x0 x1 x2}}
+    in
+    let {
+     _evar_0_0 = \_ -> Prelude.Left (Morph.ENoValidSplitPosition ( xid0)
+      splitPos)}
+    in
+    case (Prelude.&&)
+           ((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int))) splitPos)
+           ((Prelude.<=) splitPos (Interval.iend ( int))) of {
+     Prelude.True -> _evar_0_ __;
+     Prelude.False -> _evar_0_0 __}}
+  in
+  case sd of {
+   ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
+    _evar_0_ x x0 x1 x2 x3 x4 x5 uid us xid}
+
 splitAssignedIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->
                                PhysReg -> SplitPosition -> Prelude.Bool ->
                                Morph.SState () () ()
@@ -483,84 +426,140 @@
                     intlist)}
       in
       (Prelude.flip (Prelude.$)) __ (\_ ->
+        let {_evar_0_ = \intlist0 intids0 -> Logic.coq_False_rect} in
         let {
-         _evar_0_ = \_nextInterval_ intervals0 _fixedIntervals_ _unhandled_ active0 inactive0 _handled_ intlist0 intids0 ->
-          let {
-           desc0 = ScanState.Build_ScanStateDesc _nextInterval_ intervals0
-            _fixedIntervals_ _unhandled_ active0 inactive0 _handled_}
-          in
-          (\_ _ _ _ ->
-          let {_evar_0_ = \_ -> Prelude.Left Morph.ENoIntervalsToSplit} in
+         _evar_0_0 = \_top_assumption_ ->
           let {
-           _evar_0_0 = \aid aids iHaids ->
-            let {
-             _top_assumption_ = splitInterval maxReg desc0 aid pos
-                                  Prelude.False}
-            in
-            let {_evar_0_0 = \err -> Prelude.Left err} in
+           _evar_0_0 = \uid beg us ->
             let {
-             _evar_0_1 = \_top_assumption_0 ->
+             _evar_0_0 = \_nextInterval_ intervals0 _fixedIntervals_ _unhandled_ active0 inactive0 _handled_ uid0 us0 intlist0 intids0 ->
               let {
-               _evar_0_1 = \_top_assumption_1 -> Prelude.Right ((,) ()
-                (let {
-                  _evar_0_1 = \_ ->
-                   (Prelude.flip (Prelude.$)) __
-                     (let {
-                       act_to_inact = ScanState.Build_ScanStateDesc
-                        (ScanState.nextInterval maxReg _top_assumption_1)
-                        (ScanState.intervals maxReg _top_assumption_1)
-                        (ScanState.fixedIntervals maxReg _top_assumption_1)
-                        (ScanState.unhandled maxReg _top_assumption_1)
-                        (unsafeCoerce
-                          (Seq.rem
-                            (Eqtype.prod_eqType
-                              (Fintype.ordinal_eqType
-                                (ScanState.nextInterval maxReg
-                                  _top_assumption_1))
-                              (Fintype.ordinal_eqType maxReg))
-                            (unsafeCoerce ((,) ( aid) reg))
-                            (unsafeCoerce
-                              (ScanState.active maxReg _top_assumption_1))))
-                        ((:) ((,) ( aid) reg)
-                        (ScanState.inactive maxReg _top_assumption_1))
-                        (ScanState.handled maxReg _top_assumption_1)}
-                      in
-                      \_ -> Morph.Build_SSInfo act_to_inact __)}
-                 in
-                 let {
-                  _evar_0_2 = \_ -> Morph.Build_SSInfo _top_assumption_1 __}
-                 in
-                 case Ssrbool.in_mem (unsafeCoerce ((,) ( aid) reg))
-                        (Ssrbool.mem
-                          (Seq.seq_predType
-                            (Eqtype.prod_eqType
-                              (Fintype.ordinal_eqType
-                                (ScanState.nextInterval maxReg
-                                  _top_assumption_1))
-                              (Fintype.ordinal_eqType maxReg)))
-                          (unsafeCoerce
-                            (ScanState.active maxReg _top_assumption_1))) of {
-                  Prelude.True -> _evar_0_1 __;
-                  Prelude.False -> _evar_0_2 __}))}
+               _evar_0_0 = \_ -> Prelude.Right ((,) () (Morph.Build_SSInfo
+                (ScanState.Build_ScanStateDesc _nextInterval_ intervals0
+                _fixedIntervals_ _unhandled_ active0 inactive0 _handled_)
+                __))}
               in
               let {
-               _evar_0_2 = Prelude.Left (Morph.ECannotSplitSingleton7
-                ( aid))}
+               _evar_0_1 = \aid aids iHaids ->
+                let {
+                 _evar_0_1 = \_ ->
+                  let {
+                   _top_assumption_0 = \x x0 x1 x2 x3 ->
+                    splitActiveOrInactiveInterval maxReg
+                      (ScanState.Build_ScanStateDesc _nextInterval_
+                      intervals0 _fixedIntervals_ _unhandled_ active0
+                      inactive0 _handled_) x x0 x1 x2 x3}
+                  in
+                  let {
+                   _top_assumption_1 = _top_assumption_0 uid0 beg us0 aid pos}
+                  in
+                  let {_evar_0_1 = \err -> Prelude.Left err} in
+                  let {
+                   _evar_0_2 = \_top_assumption_2 ->
+                    let {
+                     _evar_0_2 = \_top_assumption_3 -> Prelude.Right ((,) ()
+                      (let {
+                        _evar_0_2 = \_ ->
+                         (Prelude.flip (Prelude.$)) __
+                           (let {
+                             act_to_inact = ScanState.Build_ScanStateDesc
+                              (ScanState.nextInterval maxReg
+                                _top_assumption_3)
+                              (ScanState.intervals maxReg _top_assumption_3)
+                              (ScanState.fixedIntervals maxReg
+                                _top_assumption_3)
+                              (ScanState.unhandled maxReg _top_assumption_3)
+                              (unsafeCoerce
+                                (Seq.rem
+                                  (Eqtype.prod_eqType
+                                    (Fintype.ordinal_eqType
+                                      (ScanState.nextInterval maxReg
+                                        _top_assumption_3))
+                                    (Fintype.ordinal_eqType maxReg))
+                                  (unsafeCoerce ((,) ( aid) reg))
+                                  (unsafeCoerce
+                                    (ScanState.active maxReg
+                                      _top_assumption_3)))) ((:) ((,) 
+                              ( aid) reg)
+                              (ScanState.inactive maxReg _top_assumption_3))
+                              (ScanState.handled maxReg _top_assumption_3)}
+                            in
+                            \_ ->
+                            let {
+                             _evar_0_2 = \_ -> Morph.Build_SSInfo
+                              act_to_inact __}
+                            in
+                             _evar_0_2 __)}
+                       in
+                       let {
+                        _evar_0_3 = \_ ->
+                         let {
+                          _evar_0_3 = \_ -> Morph.Build_SSInfo
+                           _top_assumption_3 __}
+                         in
+                          _evar_0_3 __}
+                       in
+                       case Ssrbool.in_mem (unsafeCoerce ((,) ( aid) reg))
+                              (Ssrbool.mem
+                                (Seq.seq_predType
+                                  (Eqtype.prod_eqType
+                                    (Fintype.ordinal_eqType
+                                      (ScanState.nextInterval maxReg
+                                        _top_assumption_3))
+                                    (Fintype.ordinal_eqType maxReg)))
+                                (unsafeCoerce
+                                  (ScanState.active maxReg _top_assumption_3))) of {
+                        Prelude.True -> _evar_0_2 __;
+                        Prelude.False -> _evar_0_3 __}))}
+                    in
+                    let {
+                     _evar_0_3 = Prelude.Left (Morph.ECannotSplitSingleton3
+                      ( aid))}
+                    in
+                    case _top_assumption_2 of {
+                     Prelude.Just x -> _evar_0_2 x;
+                     Prelude.Nothing -> _evar_0_3}}
+                  in
+                  case _top_assumption_1 of {
+                   Prelude.Left x -> _evar_0_1 x;
+                   Prelude.Right x -> _evar_0_2 x}}
+                in
+                let {
+                 _evar_0_2 = \_ -> Prelude.Left (Morph.ECannotSplitSingleton2
+                  ( aid))}
+                in
+                case (Prelude.<=) beg
+                       (
+                         (splitPosition
+                           (
+                             (LinearScan.Utils.nth
+                               (ScanState.nextInterval maxReg
+                                 (ScanState.Build_ScanStateDesc
+                                 _nextInterval_ intervals0 _fixedIntervals_
+                                 _unhandled_ active0 inactive0 _handled_))
+                               (ScanState.intervals maxReg
+                                 (ScanState.Build_ScanStateDesc
+                                 _nextInterval_ intervals0 _fixedIntervals_
+                                 _unhandled_ active0 inactive0 _handled_))
+                               aid)) pos)) of {
+                 Prelude.True -> _evar_0_1 __;
+                 Prelude.False -> _evar_0_2 __}}
               in
-              case _top_assumption_0 of {
-               Prelude.Just x -> _evar_0_1 x;
-               Prelude.Nothing -> _evar_0_2}}
+              Datatypes.list_rect _evar_0_0 (\aid aids iHaids _ ->
+                _evar_0_1 aid aids iHaids) intids0 __}
             in
-            case _top_assumption_ of {
-             Prelude.Left x -> _evar_0_0 x;
-             Prelude.Right x -> _evar_0_1 x}}
+            (\intlist0 _ intids0 _ _ _ _ _ ->
+            case desc of {
+             ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
+              _evar_0_0 x x0 x1 x2 x3 x4 x5 uid us intlist0 intids0})}
           in
-          Datatypes.list_rect _evar_0_ (\aid aids iHaids _ ->
-            _evar_0_0 aid aids iHaids) intids0 __)}
+          (\us _ ->
+          case _top_assumption_ of {
+           (,) x x0 -> _evar_0_0 x x0 us})}
         in
-        case desc of {
-         ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->
-          _evar_0_ x x0 x1 x2 x3 x4 x5 intlist intids})) __ __ __}
+        case ScanState.unhandled maxReg desc of {
+         [] -> (\_ _ _ _ -> _evar_0_ intlist intids);
+         (:) x x0 -> _evar_0_0 x x0 __ intlist __ intids __})) __ __ __}
   in
   case ssi of {
    Morph.Build_SSInfo x x0 -> _evar_0_ x __}
@@ -572,11 +571,12 @@
   splitAssignedIntervalForReg maxReg pre reg (BeforePos pos) Prelude.True
 
 splitAnyInactiveIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->
-                                  PhysReg -> Morph.SState () () ()
-splitAnyInactiveIntervalForReg maxReg pre reg ss =
+                                  PhysReg -> Lib.Coq_oddnum -> Morph.SState
+                                  () () ()
+splitAnyInactiveIntervalForReg maxReg pre reg pos ss =
   (Prelude.flip (Prelude.$)) (\s ->
-    splitAssignedIntervalForReg maxReg s reg EndOfLifetimeHole Prelude.False)
-    (\_top_assumption_ ->
+    splitAssignedIntervalForReg maxReg s reg (EndOfLifetimeHole pos)
+      Prelude.False) (\_top_assumption_ ->
     let {_top_assumption_0 = _top_assumption_ pre ss} in
     let {_evar_0_ = \err -> Prelude.Right ((,) () ss)} in
     let {
diff --git a/LinearScan/State.hs b/LinearScan/State.hs
--- a/LinearScan/State.hs
+++ b/LinearScan/State.hs
@@ -17,6 +17,10 @@
 get i =
   (,) i i
 
+gets :: (a1 -> a2) -> State a1 a2
+gets f s =
+  (,) (f s) s
+
 put :: a1 -> State a1 ()
 put x x0 =
   (,) () x
@@ -60,15 +64,25 @@
    [] -> 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 =
+mapM_ :: (a2 -> State a1 a3) -> ([] a2) -> State a1 ()
+mapM_ f l =
   case l of {
+   [] -> pure ();
+   (:) x xs -> bind (\x0 -> mapM_ f xs) (f x)}
+
+forM_ :: ([] a2) -> (a2 -> State a1 a3) -> State a1 ()
+forM_ l f =
+  mapM_ f l
+
+foldrM :: (a3 -> a2 -> State a1 a2) -> a2 -> ([] a3) -> State a1 a2
+foldrM f s l =
+  case l of {
    [] -> pure s;
-   (:) y ys -> bind (\x -> foldM f x ys) (f s y)}
+   (:) y ys -> bind (f y) (foldrM f s ys)}
 
-forFoldM :: a2 -> ([] a3) -> (a2 -> a3 -> State a1 a2) -> State a1 a2
-forFoldM s l f =
-  foldM f s l
+forFoldrM :: a2 -> ([] a3) -> (a3 -> a2 -> State a1 a2) -> State a1 a2
+forFoldrM s l f =
+  foldrM f s l
 
 concat :: ([] ([] a1)) -> [] a1
 concat l =
diff --git a/LinearScan/UsePos.hs b/LinearScan/UsePos.hs
--- a/LinearScan/UsePos.hs
+++ b/LinearScan/UsePos.hs
@@ -1,3 +1,6 @@
+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}
+{- For Hugs, use the option -F"cpp -P -traditional" -}
+
 module LinearScan.UsePos where
 
 
@@ -10,17 +13,108 @@
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
+import qualified LinearScan.Eqtype as Eqtype
+import qualified LinearScan.Seq as Seq
+import qualified LinearScan.Ssrbool as Ssrbool
 
+
+
+--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
+
+data VarKind =
+   Input
+ | Temp
+ | Output
+
+eqVarKind :: VarKind -> VarKind -> Prelude.Bool
+eqVarKind s1 s2 =
+  case s1 of {
+   Input ->
+    case s2 of {
+     Input -> Prelude.True;
+     _ -> Prelude.False};
+   Temp ->
+    case s2 of {
+     Temp -> Prelude.True;
+     _ -> Prelude.False};
+   Output ->
+    case s2 of {
+     Output -> Prelude.True;
+     _ -> Prelude.False}}
+
+eqVarKindP :: Eqtype.Equality__Coq_axiom VarKind
+eqVarKindP b1 b2 =
+  let {
+   _evar_0_ = let {_evar_0_ = Ssrbool.ReflectT} in
+              let {_evar_0_0 = Ssrbool.ReflectF} in
+              let {_evar_0_1 = Ssrbool.ReflectF} in
+              case b2 of {
+               Input -> _evar_0_;
+               Temp -> _evar_0_0;
+               Output -> _evar_0_1}}
+  in
+  let {
+   _evar_0_0 = let {_evar_0_0 = Ssrbool.ReflectF} in
+               let {_evar_0_1 = Ssrbool.ReflectT} in
+               let {_evar_0_2 = Ssrbool.ReflectF} in
+               case b2 of {
+                Input -> _evar_0_0;
+                Temp -> _evar_0_1;
+                Output -> _evar_0_2}}
+  in
+  let {
+   _evar_0_1 = let {_evar_0_1 = Ssrbool.ReflectF} in
+               let {_evar_0_2 = Ssrbool.ReflectF} in
+               let {_evar_0_3 = Ssrbool.ReflectT} in
+               case b2 of {
+                Input -> _evar_0_1;
+                Temp -> _evar_0_2;
+                Output -> _evar_0_3}}
+  in
+  case b1 of {
+   Input -> _evar_0_;
+   Temp -> _evar_0_0;
+   Output -> _evar_0_1}
+
+coq_VarKind_eqMixin :: Eqtype.Equality__Coq_mixin_of VarKind
+coq_VarKind_eqMixin =
+  Eqtype.Equality__Mixin eqVarKind eqVarKindP
+
+coq_VarKind_eqType :: Eqtype.Equality__Coq_type
+coq_VarKind_eqType =
+  unsafeCoerce coq_VarKind_eqMixin
+
 data UsePos =
-   Build_UsePos Prelude.Int Prelude.Bool
+   Build_UsePos Prelude.Int Prelude.Bool VarKind
 
 uloc :: UsePos -> Prelude.Int
 uloc u =
   case u of {
-   Build_UsePos uloc0 regReq0 -> uloc0}
+   Build_UsePos uloc0 regReq0 uvar0 -> uloc0}
 
 regReq :: UsePos -> Prelude.Bool
 regReq u =
   case u of {
-   Build_UsePos uloc0 regReq0 -> regReq0}
+   Build_UsePos uloc0 regReq0 uvar0 -> regReq0}
+
+uvar :: UsePos -> VarKind
+uvar u =
+  case u of {
+   Build_UsePos uloc0 regReq0 uvar0 -> uvar0}
+
+upos_le :: UsePos -> UsePos -> Prelude.Bool
+upos_le x y =
+  (Prelude.<=) (uloc x) (uloc y)
+
+head_or :: Prelude.Int -> ([] UsePos) -> Prelude.Int
+head_or x xs =
+  Seq.head x (Prelude.map (\u -> uloc u) xs)
 
diff --git a/linearscan.cabal b/linearscan.cabal
--- a/linearscan.cabal
+++ b/linearscan.cabal
@@ -1,5 +1,5 @@
 name:          linearscan
-version:       0.3.1.0
+version:       0.4.0.0
 synopsis:      Linear scan register allocator, formally verified in Coq
 homepage:      http://github.com/jwiegley/linearscan
 license:       BSD3
@@ -65,10 +65,10 @@
     LinearScan.List0
     LinearScan.LiveSets
     LinearScan.Logic
+    LinearScan.Loops
     LinearScan.Main
     LinearScan.Morph
     LinearScan.NonEmpty0
-    LinearScan.Order
     LinearScan.Range
     LinearScan.Resolve
     LinearScan.ScanState
@@ -88,22 +88,4 @@
   build-depends:    base >=4.7 && <4.8
                   , containers
                   , transformers
-
-test-suite test
-  default-language: Haskell2010
-  type:             exitcode-stdio-1.0
-  ghc-options:      -fno-warn-deprecated-flags
-  hs-source-dirs:   test
-  main-is:          Main.hs
-  other-modules:    Tempest
-  build-depends: 
-        base >=3
-      , linearscan
-      , hspec              >= 1.4.4
-      , hspec-expectations >= 0.3
-      , containers         >= 0.5.5
-      , transformers       >= 0.3.0.0
-      , hoopl              >= 3.10.0.1
-      , lens               >= 4.2
-      , mtl
-      , free
+                  , mtl
diff --git a/test/Main.hs b/test/Main.hs
deleted file mode 100644
--- a/test/Main.hs
+++ /dev/null
@@ -1,445 +0,0 @@
-{-# OPTIONS_GHC -Wall -Werror #-}
-
-module Main where
-
-{-
-The objective of these tests is to present a real world instruction stream to
-the register allocator algorithm, and verify that for certain inputs we get
-the expected outputs.  I've extracted several of the types from the Tempest
-compiler for which this algorithm was originally developed.  We link from this
-module to the Haskell interface code (LinearScan), which calls into the
-Haskell code that was extracted from Coq.
--}
-
-import Tempest
-import Test.Hspec
-
-main :: IO ()
-main = hspec $ do
-  describe "Sanity tests" sanityTests
-  describe "Block tests" blockTests
-
-sanityTests :: SpecWith ()
-sanityTests = do
-  it "Single instruction" $ asmTest 32
-    (label "entry"
-        (add v0 v1 v2)
-        return_) $
-
-    label "entry"
-        (add r0 r1 r2)
-        return_
-
-  it "Single, repeated instruction" $ asmTest 32
-    (label "entry"
-        (do add v0 v1 v2
-            add v0 v1 v2
-            add v0 v1 v2)
-        return_) $
-
-    label "entry"
-        (do add r0 r1 r2
-            add r0 r1 r2
-            add r0 r1 r2)
-        return_
-
-  it "Multiple instructions" $ asmTest 32
-    (label "entry"
-        (do add v0 v1 v2
-            add v0 v1 v3
-            add v0 v1 v2)
-        return_) $
-
-    label "entry"
-        (do add r0 r1 r2
-            add r0 r1 r3
-            add r0 r1 r2)
-        return_
-
-  it "More variables used than registers" $ asmTest 32
-    (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_) $
-
-    label "entry"
-        (do add r0 r1 r24
-            add r2 r3 r0
-            add r4 r5 r1
-            add r6 r7 r2
-            add r8 r9 r3
-            add r10 r11 r4
-            add r12 r13 r5
-            add r14 r15 r6
-            add r16 r17 r7
-            add r18 r19 r8
-            add r20 r21 r9
-            add r22 r23 r10)
-        return_
-
-  it "Single long-lived variable" $ asmTest 32
-    (label "entry"
-        (do add v0 v1 v2
-            add v0 v4 v5
-            add v0 v7 v8
-            add v0 v10 v11)
-        return_) $
-
-    label "entry"
-        (do add r0 r1 r5
-            add r0 r2 r1
-            add r0 r3 r2
-            add r0 r4 r3)
-        return_
-
-  it "Two long-lived variables" $ asmTest 32
-    (label "entry"
-        (do add v0 v1 v2
-            add v0 v4 v5
-            add v0 v4 v8
-            add v0 v4 v11)
-        return_) $
-
-    label "entry"
-        (do add r0 r1 r3
-            add r0 r2 r1
-            add r0 r2 r4
-            add r0 r2 r5)
-        return_
-
-  it "One variable with a long interval" $ asmTest 32
-    (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_) $
-
-    label "entry"
-        (do add r0 r1 r23
-            add r2 r3 r1
-            add r4 r5 r2
-            add r6 r7 r3
-            add r8 r9 r4
-            add r10 r11 r5
-            add r12 r13 r6
-            add r14 r15 r7
-            add r16 r17 r8
-            add r18 r19 r9
-            add r20 r21 r10
-            add r0 r22 r11)
-        return_
-
-  it "Many variables with long intervals" $ asmTest 32
-    (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_) $
-
-    label "entry"
-        (do add r0 r1 r20
-            add r2 r3 r21
-            add r4 r5 r22
-            add r6 r7 r23
-            add r8 r9 r24
-            add r10 r11 r25
-            add r12 r13 r26
-            add r14 r15 r27
-            add r16 r17 r28
-            add r18 r19 r29
-            add r0 r1 r20
-            add r2 r3 r21
-            add r4 r5 r22
-            add r6 r7 r23
-            add r8 r9 r24
-            add r10 r11 r25
-            add r12 r13 r26
-            add r14 r15 r27
-            add r16 r17 r28
-            add r18 r19 r29)
-        return_
-
-  it "Spilling one variable" $ asmTest 32
-    (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_) $
-
-    label "entry"
-        (do {-  1 -} add r0 r1 r22
-            {-  3 -} add r2 r3 r23
-            {-  5 -} add r4 r5 r24
-            {-  7 -} add r6 r7 r25
-            {-  9 -} add r8 r9 r26
-            {- 11 -} add r10 r11 r27
-            {- 13 -} add r12 r13 r28
-            {- 15 -} add r14 r15 r29
-            {- 17 -} add r16 r17 r30
-            {- 19 -} add r18 r19 r31
-
-            -- 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 r18, which is next used at position 41.
-                     save r18 0
-            {- 21 -} add r20 r21 r18
-            {- 23 -} add r0 r1 r22
-            {- 25 -} add r2 r3 r23
-            {- 27 -} add r4 r5 r24
-            {- 29 -} add r6 r7 r25
-            {- 31 -} add r8 r9 r26
-            {- 33 -} add r10 r11 r27
-            {- 35 -} add r12 r13 r28
-            {- 37 -} add r14 r15 r29
-            {- 39 -} add r16 r17 r30
-
-            -- When it comes time to reload v29 (which had been allocated
-            -- to r18), we pick the first available register which happens
-            -- to be r0 in this case.
-                     restore 0 r0
-            {- 41 -} add r0 r19 r31
-            {- 43 -} add r20 r21 r18)
-        return_
-
-  it "Inserts only necessary saves and restores" $ asmTest 4
-    (label "entry"
-        (do {-  3 -} add v0   v1  v2
-            {-  5 -} add v2   v1  v3
-            {-  7 -} add v3   v2  v4
-            {-  9 -} add v4   v1  v0)
-        return_) $
-
-    label "entry"
-        (do {-  3 -} add r1 r0 r2
-            {-  5 -} add r2 r0 r3
-                     save r0 0
-            {-  7 -} add r3 r2 r0
-                     restore 0 r2
-            {-  9 -} add r0 r2 r1)
-        return_
-
-blockTests :: SpecWith ()
-blockTests = do
-  it "Allocates across blocks" $ asmTest 32
-    (do label "entry"
-            (add v0 v1 v2)
-            (jump "skipped")
-        label "skipped"
-            (do add v2 v3 v4
-                add v2 v4 v5)
-            (jump "next")
-        label "next"
-            (do add v2 v5 v6
-                add v2 v6 v7
-                add v2 v7 v8)
-            return_)
-
-    (do label "entry"
-            (add r0 r1 r3)
-            (jump "skipped")
-        label "skipped"
-            (do add r3 r2 r0
-                add r3 r0 r1)
-            (jump "next")
-        label "next"
-            (do add r3 r1 r0
-                add r3 r0 r1
-                add r3 r1 r0)
-            return_)
-
-  it "Inserts resolving moves" $ asmTest 4
-    (do label "entry"                           -- 1
-            (add v0 v1 v2)                      -- 3
-            (branch Zero v2 "B3" "B2")          -- 5
-        label "B2"                              -- 7
-            (do add v1 v2 v3                    -- 9
-                add v0 v0 v4                    -- 11
-                add v0 v0 v5                    -- 13
-                add v0 v4 v6                    -- 15
-                add v0 v5 v6)                   -- 17
-            (jump "B4")                         -- 19
-        label "B3"                              -- 21
-            (add v1 v2 v3)                      -- 23
-            (jump "B4")                         -- 25
-        label "B4"                              -- 27
-            (add v3 v3 v0)                      -- 29
-            return_)                            -- 31
-
-    (do label "entry"
-            (add r0 r1 r2)
-            (branch Zero r2 "B2" "B3")
-        label "B2"
-            (add r1 r2 r3)
-            (jump "B4")
-        label "B3"
-            (do add r1 r2 r3
-                save r3 16
-                save r2 8
-                save r1 0
-                add r0 r0 r1
-                add r0 r0 r2
-                add r0 r1 r3
-                add r0 r2 r3
-                restore 16 r3)
-            (jump "B4")
-        label "B4"
-            (add r3 r3 r0)
-            return_)
-
-  it "Inserts resolving moves another way" $ asmTest 4
-    (do label "entry"                           -- 1
-            (add v0 v1 v2)                      -- 3
-            (branch Zero v2 "B3" "B2")          -- 5
-        label "B2"                              -- 7
-            (add v1 v2 v3)                      -- 9
-            (jump "B4")                         -- 11
-        label "B3"                              -- 13
-            (do add v1 v2 v3                    -- 15
-                add v0 v0 v4                    -- 17
-                add v0 v0 v5                    -- 19
-                add v0 v4 v6                    -- 21
-                add v0 v5 v6)                   -- 23
-            (jump "B4")                         -- 25
-        label "B4"                              -- 27
-            (add v3 v3 v0)                      -- 29
-            return_)                            -- 31
-
-    (do label "entry"
-            (add r0 r1 r2)
-            (branch Zero r2 "B2" "B3")
-        label "B2"
-            (do add r1 r2 r3
-                save r3 0
-                add r0 r0 r1
-                add r0 r0 r2
-                add r0 r1 r3
-                add r0 r2 r3
-                restore 0 r1)
-            (jump "B4")
-        label "B3"
-            (do add r1 r2 r3
-                move r3 r1)
-            (jump "B4")
-        label "B4"
-            (add r1 r1 r0)
-            return_)
-
-  it "Another resolution case" $ asmTest 4
-    (do label "entry"           -- 1
-            (do lc v3           -- 3
-                lc v4           -- 5
-                lc v15          -- 7
-                lc v20)         -- 9
-            (jump "L3")         -- 11
-        label "L3"              -- 13
-            (do move v3 v9      -- 15
-                move v9 v11     -- 17
-                move v11 v10    -- 19
-                move v10 v12    -- 21
-                move v12 v13    -- 23
-                lc v14          -- 25
-                move v15 v5)    -- 27
-            (jump "L6")         -- 29
-        label_ "L6"             -- 31
-	    (branch Zero v4 "L3" "L2") -- 33
-        label "L2"                     -- 35
-            (do lc v21                 -- 37
-                move v21 v18           -- 39
-                move v5 v4             -- 41
-                lc v19                 -- 43
-                move v20 v17)          -- 45
-            (jump "L6"))               -- 47
-
-    (do label "entry"           -- 1
-            (do lc r0           -- 3
-                lc r1           -- 5
-                lc r2           -- 7
-                lc r3           -- 9
-                save r3 0)
-            (jump "L3")         -- 11
-        label "L3"              -- 13
-            (do restore 8 r0
-                move r0 r3      -- 15
-                save r0 8
-                move r3 r0      -- 17
-                move r0 r3      -- 19
-                move r3 r0      -- 21
-                move r0 r3      -- 23
-                lc r0           -- 25
-                save r0 16
-                move r2 r0
-                save r2 24)     -- 27
-            (jump "L6")         -- 29
-        label_ "L6"             -- 31
-	    (branch Zero r1 "L3" "L2") -- 33
-        label "L2"                     -- 35
-            (do lc r3                  -- 37
-                move r3 r2             -- 39
-                move r0 r1             -- 41
-                save r1 40
-                save r0 32
-                lc r3                  -- 43
-                restore 0 r1
-                move r1 r0
-                restore 40 r1
-                restore 32 r0
-                restore 24 r2
-                save r1 0)             -- 45
-            (jump "L6"))
diff --git a/test/Tempest.hs b/test/Tempest.hs
deleted file mode 100644
--- a/test/Tempest.hs
+++ /dev/null
@@ -1,575 +0,0 @@
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE ConstraintKinds #-}
-
-{-# OPTIONS_GHC -Wall -Werror #-}
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-
-module Tempest where
-
-import           Compiler.Hoopl as Hoopl hiding ((<*>))
-import           Control.Applicative
-import           Control.Exception
-import           Control.Lens
-import           Control.Monad.Free
-import           Control.Monad.State.Class
-import           Control.Monad.Trans.Class
-import qualified Control.Monad.Trans.Free as TF
-import           Control.Monad.Trans.Free hiding (FreeF(..), Free)
-import           Control.Monad.Trans.State (StateT, evalStateT, evalState)
-import           Data.Foldable
-import qualified Data.List
-import qualified Data.Map as M
-import           Data.Maybe (fromMaybe)
-import           Data.Monoid
--- import           Debug.Trace
-import           LinearScan
-import           Test.Hspec
-
-------------------------------------------------------------------------------
--- The input from the Tempest compiler has the following shape: 'Procedure a
--- IRVar', which means that instructions ultimately refer to either physical
--- registers, or virtual variables (by index).
---
--- The output from the register allocator should be as close to the input as
--- possible, with the difference that it has type 'Procedure a Reg', meaning
--- that only physical registers are referenced.
---
--- So the main allocation algorithm roughly has this type at present:
---
---     regAlloc :: Procedure a IRVar -> Procedure a Reg
-------------------------------------------------------------------------------
-
-data AtomicGroup = AtomicGroup deriving (Eq, Show)
-type Name = String
-
-newtype Linearity = Linearity { isLinear :: Bool }
-  deriving (Eq, Show)
-
--- | Tests used for branching (correspond to branching instructions)
-data Test
-  -- | beq
-  = Zero
-  -- | bne
-  | NonZero
-  -- | bgt
-  | Positive
-  -- | blt
-  | Negative
-  deriving (Eq, Show)
-
-data CConv
-  = CConvC {
-      ccArgs     :: [Reg],
-      ccResults  :: [Reg],
-      ccIsBrack  :: Bool
-    }
-  | InlineC
-  deriving (Eq, Show)
-
-data Constant = Constant deriving (Eq, Show)
-
-type Src a      = a
-
--- | Type synonym for indicating destination operands
-type Dst a      = a
-
--- | Type synonym for indicating success or true branch
-type Success a  = a
-
--- | Type synonym for indicating failure or false branch
-type Failure a  = a
-
--- | Type synonym for indicating an external name
-type Imported a = a
-
-type Reg = Int
-
-data Instruction reg
-  = Add          reg reg reg
-  | Nop
-  deriving (Eq, Show, Functor, Foldable, Traversable)
-
-data IRInstr v e x where
-  Label         :: Label -> IRInstr v C O
-  Alloc         :: AtomicGroup -> Maybe (Src v) -> Dst v -> IRInstr v O O
-  Reclaim       :: Src v -> IRInstr v O O
-  Instr         :: Instruction v -> IRInstr v O O
-  Call          :: CConv -> Instruction v -> IRInstr v O O
-  LoadConst     :: Constant -> Dst v -> IRInstr v O O
-  Move          :: Src v -> Dst v -> IRInstr v O O
-  Copy          :: Src v -> Dst v -> IRInstr v O O
-  Save          :: Linearity -> Src v -> Dst Int -> IRInstr v O O
-  Restore       :: Linearity -> Src Int -> Dst v -> IRInstr v O O
-  SaveOffset    :: Linearity -> Int -> Src v -> Dst Int -> IRInstr v O O
-  RestoreOffset :: Linearity -> Int -> Src Int -> Dst v -> IRInstr v O O
-  Jump          :: Label -> IRInstr v O C
-  Branch        :: Test -> v -> Success Label -> Failure Label
-                -> IRInstr v O C
-  Stwb          :: Linearity -> Src v -> Dst v
-                -> Success Label -> Failure Label -> IRInstr v O C
-  Strb          :: Src v -> Dst v -> Success Label -> Failure Label
-                -> IRInstr v O C
-  ReturnInstr   :: [Reg] -> Instruction v -> IRInstr v O C
-
-deriving instance Eq v => Eq (IRInstr v e x)
-
-instance Show v => Show (IRInstr v e x) where
-  show (Label l)        = show l ++ ":"
-  show (Alloc g x1 x2)  = "\t@alloc " ++ show g ++
-                          (case x1 of Just v -> " " ++ show v ; _ -> " _")
-                          ++ " " ++ show x2
-  show (Reclaim v)      = "\t@reclaim " ++ show v
-  show (Instr i)        = "\t" ++ show i
-  show (Call c i)       = "\t@call " ++ show c ++ " " ++ show i
-  show (LoadConst c v)  = "\t@lc " ++ show v ++ " " ++ show c
-  show (Move x1 x2)     = "\t@mvrr " ++ show x1 ++ " " ++ show x2
-  show (Copy x1 x2)     = "\t@cprr " ++ show x1 ++ " " ++ show x2
-  show (Save (Linearity l) src dst)
-                        = "\t@save " ++ show l ++ " " ++ show src ++ " " ++ show dst
-  show (Restore (Linearity l) src dst)
-                        = "\t@restore " ++ show l ++ " " ++ show src ++ " " ++ show dst
-  show (SaveOffset (Linearity l) off src dst)
-                        = unwords ["\t@saveoff", show l, show off, show src, show dst]
-  show (RestoreOffset (Linearity l) off src dst)
-                        = unwords ["\t@restoreoff", show l, show off, show src, show dst]
-  show (Jump l)         = "\t@jmp " ++ show l
-  show (Branch tst v t f)
-                        = "\t@b" ++ show tst ++ " " ++ show v
-                            ++ " " ++ show t
-                            ++ "; @jmp " ++ show f
-  show (Stwb lin x1 x2 t f)
-                        = (if isLinear lin then "\t@stwlb " else "\t@stwb ")
-                            ++ show x1 ++ " " ++ show x2
-                            ++ " " ++ show f ++ "; @jmp " ++ show t
-  show (Strb x1 x2 t f) = "\t@strb " ++ show x1 ++ " " ++ show x2
-                            ++ " " ++ show f ++ "; @jmp " ++ show t
-  show (ReturnInstr liveRegs i)   = "\t@return " ++ show liveRegs ++ " " ++ show i
-
-data Node a v e x = Node
-  { _nodeIRInstr :: IRInstr v e x
-  , _nodeMeta    :: a
-  } deriving Eq
-
-instance Show v => Show (Node a v e x) where
-    show (Node i _) = show i
-
-instance NonLocal (Node a v) where
-  entryLabel (Node (Label l)         _) = l
-  successors (Node (Jump l)          _) = [l]
-  successors (Node (Branch _ _ t f)  _) = [t, f]
-  successors (Node (Stwb _ _ _ s f)  _) = [s, f]
-  successors (Node (Strb _ _ s f)    _) = [s, f]
-  successors (Node (ReturnInstr _ _) _) = []
-
-data AtomKind = Atom deriving (Eq, Show)
-data Var = Var deriving (Eq, Show)
-
-data IRVar' = PhysicalIV !PhysReg
-            | VirtualIV !Int !AtomKind
-            deriving Eq
-
-instance Show IRVar' where
-    show (PhysicalIV r)  = "r" ++ show r
-    show (VirtualIV n _) = "v" ++ show n
-
--- | Virtual IR variable together with an optional AST variable
-data IRVar =
-  IRVar
-  { _ivVar :: !IRVar' -- ^ The virtual or physical register
-  , _ivSrc :: !(Maybe Var) -- ^ An optional corresponding AST variable for
-                       -- informational purposes.
-  }
-  deriving Eq
-
-instance Show IRVar where
-    show (IRVar x _) = show x
-
-type Engine m = (UniqueMonad m, MonadState Labels m)
-
-instance UniqueMonad (StateT Labels SimpleUniqueMonad) where
-    freshUnique = lift freshUnique
-
-asmTest :: (Engine m, m ~ StateT Labels SimpleUniqueMonad)
-        => Int -> Program IRVar m () -> Program Reg m ()
-        -> Expectation
-asmTest regs (compile -> (prog, entry)) (compile -> (result, _)) =
-    go $ M.fromList $ zip (Prelude.map entryLabel blocks) [(1 :: Int)..]
-  where
-    GMany NothingO body NothingO = prog
-    blocks = postorder_dfs_from body entry
-
-    go blockIds =
-        case evalState
-                 (allocate regs (blockInfo getBlockId) opInfo blocks)
-                 (newSpillStack 0) of
-            Left e -> error $ "Allocation failed: " ++ e
-            Right blks -> do
-                let graph' = newGraph blks
-                catch
-                    (showGraph show graph' `shouldBe` showGraph show result)
-                    (\e -> do
-                          putStrLn "---- Expecting ----"
-                          putStr $ showGraph show result
-                          putStrLn "---- Compiled  ----"
-                          putStr $ showGraph show graph'
-                          putStrLn "-------------------"
-                          throwIO (e :: SomeException))
-      where
-        newBody = Data.Foldable.foldl' (flip addBlock) emptyBody
-        newGraph xs = GMany NothingO (newBody xs) NothingO
-
-        getBlockId :: Hoopl.Label -> Int
-        getBlockId lbl =
-            fromMaybe (error "The impossible happened")
-                      (M.lookup lbl blockIds)
-
-variables :: Traversal (IRInstr v1 e x) (IRInstr v2 e x) v1 v2
-variables f = go
-  where
-    go (Alloc ag msrc dst)           = Alloc ag <$> traverse f msrc <*> f dst
-    go (Reclaim src)                 = Reclaim <$> f src
-    go (Instr i)                     = Instr <$> traverse f i
-    go (LoadConst c dst)             = LoadConst c <$> f dst
-    go (Move src dst)                = Move <$> f src <*> f dst
-    go (Copy src dst)                = Copy <$> f src <*> f dst
-    go (Save lin src x)              = Save lin <$> f src <*> pure x
-    go (Restore x1 x2 dst)           = Restore x1 x2 <$> f dst
-    go (SaveOffset lin off src x)    = SaveOffset lin off <$> f src <*> pure x
-    go (RestoreOffset lin off x dst) = RestoreOffset lin off x <$> f dst
-    go (Branch x1 cond x2 x3)        = Branch x1 <$> f cond
-                                                 <*> pure x2 <*> pure x3
-    go (Stwb x1 src dst x2 x3)       = Stwb x1 <$> f src <*> f dst
-                                               <*> pure x2 <*> pure x3
-    go (Strb src dst x2 x3)          = Strb <$> f src <*> f dst
-                                            <*> pure x2 <*> pure x3
-    go (Call cc i)                   = Call cc <$> traverse f i
-    go (ReturnInstr liveInRegs i)    = ReturnInstr liveInRegs <$> traverse f i
-    go (Label x)                     = pure $ Label x
-    go (Jump x)                      = pure $ Jump x
-
-metadata :: Lens (Node a1 v e x) (Node a2 v e x) a1 a2
-metadata f (Node instr meta) = Node instr <$> f meta
-
-irinstr :: Traversal (Node a v1 e x) (Node a v2 e x)
-                  (IRInstr v1 e x) (IRInstr v2 e x)
-irinstr f (Node instr meta) = Node <$> f instr <*> pure meta
-
-data NodeV a v = NodeCO { getNodeCO :: Node a v C O }
-               | NodeOO { getNodeOO :: Node a v O O }
-               | NodeOC { getNodeOC :: Node a v O C }
-
-instance Functor (NodeV v) where
-    fmap f (NodeCO n) = NodeCO (over (irinstr.variables) f n)
-    fmap f (NodeOO n) = NodeOO (over (irinstr.variables) f n)
-    fmap f (NodeOC n) = NodeOC (over (irinstr.variables) f n)
-
-blockInfo :: (Hoopl.Label -> Int)
-          -> BlockInfo (Block (Node a IRVar) C C)
-                      (Block (Node a Reg) C C)
-                      (NodeV a IRVar)
-                      (NodeV a Reg)
-blockInfo getBlockId = BlockInfo
-    { blockId = getBlockId . entryLabel
-
-    , blockSuccessors = Prelude.map getBlockId . successors
-
-    , blockOps = \(BlockCC a b z) ->
-        ([NodeCO a], Prelude.map NodeOO (blockToList b), [NodeOC z])
-
-    , setBlockOps = \_ [a] b [z] ->
-        BlockCC
-            (getNodeCO a)
-            (blockFromList (Prelude.map getNodeOO b))
-            (getNodeOC z)
-    }
-
-data StackInfo = StackInfo
-    { stackPtr   :: Int
-    , stackSlots :: M.Map (Maybe Int) Int
-    }
-    deriving (Eq, Show)
-
-newSpillStack :: Int -> StackInfo
-newSpillStack offset = StackInfo
-    { stackPtr   = offset
-    , stackSlots = mempty
-    }
-
-opInfo :: OpInfo StackInfo (NodeV a IRVar) (NodeV a Reg)
-opInfo = OpInfo
-    { opKind = \n -> case n of
-           NodeOO (Node i _) -> case i of
-               Call {} -> IsCall
-               -- jww (2015-01-18): Identification of loop boundaries allows
-               -- the allocator to perform a block ordering optimization to
-               -- avoid excessive saves and restores, but it is optional.
-               -- ?       -> LoopBegin
-               -- ?       -> LoopEnd
-               _ -> IsNormal
-           NodeOC (Node i _) -> case i of
-               Jump {}   -> IsBranch
-               Branch {} -> IsBranch
-               Strb {}   -> IsBranch
-               Stwb {}   -> IsBranch
-               _ -> IsNormal
-           _ -> IsNormal
-
-    , opRefs = \n -> let f = getReferences in case n of
-           NodeCO o -> f o
-           NodeOO o -> f o
-           NodeOC o -> f o
-
-    , moveOp = \sr dr -> do
-        let mv = Move sr dr
-        return [NodeOO (Node mv (error "no move meta"))]
-
-    , swapOp = \sr dr ->
-        liftA2 (++) (mkRestoreOp Nothing dr)
-                    (mkSaveOp sr Nothing)
-
-    , saveOp = mkSaveOp
-    , restoreOp = mkRestoreOp
-
-      -- Apply allocations, which changes IRVar's into Reg's.
-    , applyAllocs = \node m -> [fmap (setRegister m) node]
-    }
-  where
-    go :: Instruction IRVar -> [VarInfo]
-    go Nop = mempty
-    go (Add s1 s2 d1) =
-        mkv Input s1 <> mkv Input s2 <> mkv Output d1
-
-    mkv :: VarKind -> IRVar -> [VarInfo]
-    mkv k (IRVar (PhysicalIV n) _)  = [vinfo k (Left n)]
-    mkv k (IRVar (VirtualIV n _) _) = [vinfo k (Right n)]
-
-    vinfo k en = VarInfo
-        { varId   = en
-        , varKind = k
-          -- If there are variables which can be used directly from
-          -- memory, then this can be False, which relaxes some
-          -- requirements.
-        , regRequired = True
-        }
-
-    getReferences :: Node a IRVar e x -> [VarInfo]
-    getReferences (Node (Label _) _)         = mempty
-    getReferences (Node (Instr i) _)         = go i
-    getReferences (Node (Jump _) _)          = mempty
-    getReferences (Node (Move src dst) _)    = mkv Input src <> mkv Output dst
-    getReferences (Node (LoadConst _ v) _)   = mkv Output v
-    getReferences (Node (Branch _ v _ _) _)  = mkv Input v
-    getReferences (Node (ReturnInstr _ i) _) = go i
-    getReferences n = error $ "getReferences: unhandled node: " ++ show n
-
-    setRegister :: [(Int, PhysReg)] -> IRVar -> Reg
-    setRegister _ (IRVar (PhysicalIV r) _)  = r
-    setRegister m (IRVar (VirtualIV n _) _) =
-        fromMaybe (error $ "Allocation failed for variable " ++ show n)
-                  (Data.List.lookup n m)
-
-getStackSlot vid = do
-    stack <- get
-    case M.lookup vid (stackSlots stack) of
-        Just off -> return off
-        Nothing -> do
-            let off = stackPtr stack
-            put StackInfo
-                 { stackPtr   = off + 8
-                 , stackSlots =
-                     M.insert vid off (stackSlots stack)
-                 }
-            return off
-
-mkSaveOp r vid = do
-    off <- getStackSlot vid
-    let sv = Save (Linearity False) r off
-    return [NodeOO (Node sv (error "no save meta"))]
-
-mkRestoreOp vid r = do
-    off <- getStackSlot vid
-    let rs  = Restore (Linearity False) off r
-    return [NodeOO (Node rs (error "no restore meta"))]
-
-var :: Int -> IRVar
-var i = IRVar { _ivVar = VirtualIV i Atom
-              , _ivSrc = Nothing
-              }
-
-fixed :: Int -> IRVar
-fixed i = IRVar { _ivVar = PhysicalIV i
-                , _ivSrc = Nothing
-                }
-
-reg :: PhysReg -> PhysReg
-reg r = r
-
-v0  = var 0
-v1  = var 1
-v2  = var 2
-v3  = var 3
-v4  = var 4
-v5  = var 5
-v6  = var 6
-v7  = var 7
-v8  = var 8
-v9  = var 9
-v10 = var 10
-v11 = var 11
-v12 = var 12
-v13 = var 13
-v14 = var 14
-v15 = var 15
-v16 = var 16
-v17 = var 17
-v18 = var 18
-v19 = var 19
-v20 = var 20
-v21 = var 21
-v22 = var 22
-v23 = var 23
-v24 = var 24
-v25 = var 25
-v26 = var 26
-v27 = var 27
-v28 = var 28
-v29 = var 29
-v30 = var 30
-v31 = var 31
-v32 = var 32
-v33 = var 33
-v34 = var 34
-v35 = var 35
-
-r0  = reg 0
-r1  = reg 1
-r2  = reg 2
-r3  = reg 3
-r4  = reg 4
-r5  = reg 5
-r6  = reg 6
-r7  = reg 7
-r8  = reg 8
-r9  = reg 9
-r10 = reg 10
-r11 = reg 11
-r12 = reg 12
-r13 = reg 13
-r14 = reg 14
-r15 = reg 15
-r16 = reg 16
-r17 = reg 17
-r18 = reg 18
-r19 = reg 19
-r20 = reg 20
-r21 = reg 21
-r22 = reg 22
-r23 = reg 23
-r24 = reg 24
-r25 = reg 25
-r26 = reg 26
-r27 = reg 27
-r28 = reg 28
-r29 = reg 29
-r30 = reg 30
-r31 = reg 31
-r32 = reg 32
-r33 = reg 33
-r34 = reg 34
-r35 = reg 35
-
-type BodyF v = Free ((,) (Node () v O O)) ()
-
-nodesToList :: BodyF v -> [Node () v O O]
-nodesToList (Pure ()) = []
-nodesToList (Free (Node n meta, xs)) = Node n meta : nodesToList xs
-
-data ProgramF m v
-    = FreeLabel
-      { labelEntry :: Label
-      , labelBody  :: BodyF v
-      , labelClose :: m (Node () v O C)
-      }
-
-type Program v m a = FreeT ((,) (ProgramF m v)) m a
-
-type Labels = M.Map String Label
-
-getLabel :: Engine m => String -> m Label
-getLabel str = do
-    l <- use (at str)
-    case l of
-        Just lbl -> return lbl
-        Nothing -> do
-            lbl <- freshLabel
-            at str .= Just lbl
-            return lbl
-
-label :: Engine m => String -> BodyF v -> m (Node () v O C) -> Program v m ()
-label str body close = do
-    lbl <- lift $ getLabel str
-    liftF (FreeLabel lbl body close, ())
-
-label_ :: Engine m => String -> m (Node () v O C) -> Program v m ()
-label_ str close = do
-    lbl <- lift $ getLabel str
-    liftF (FreeLabel lbl (Pure ()) close, ())
-
-compile :: (Engine m, m ~ StateT Labels SimpleUniqueMonad, NonLocal (Node () v))
-        => Program v m () -> (Graph (Node () v) C C, Hoopl.Label)
-compile prog = runSimpleUniqueMonad $
-    flip evalStateT (mempty :: M.Map String Label) $ do
-        body  <- go prog
-        entry <- use (at "entry")
-        case entry of
-            Nothing -> error "Missing 'entry' label"
-            Just lbl -> return (bodyGraph body, lbl)
-  where
-    go m = do
-        p <- runFreeT m
-        case p of
-            TF.Pure ()        -> return emptyBody
-            TF.Free (blk, xs) -> addBlock <$> comp blk <*> go xs
-
-    comp (FreeLabel lbl body close) = do
-        close' <- close
-        return $ BlockCC (Node (Label lbl) ())
-                         (blockFromList (nodesToList body)) close'
-
-add :: v -> v -> v -> BodyF v
-add x0 x1 x2 = Free (Node (Instr (Add x0 x1 x2)) (), Pure ())
-
-move :: v -> v -> BodyF v
-move x0 x1 = Free (Node (Move x0 x1) (), Pure ())
-
-lc :: v -> BodyF v
-lc x0 = Free (Node (LoadConst Constant x0) (), Pure ())
-
-return_ :: Monad m => m (Node () v O C)
-return_ = return $ Node (ReturnInstr [] Nop) ()
-
-branch :: Engine m => Test -> v -> String -> String -> m (Node () v O C)
-branch tst v good bad = do
-    lblg <- getLabel good
-    lblb <- getLabel bad
-    return $ Node (Branch tst v lblg lblb) ()
-
-jump :: Engine m => String -> m (Node () v O C)
-jump dest = do
-    lbl <- getLabel dest
-    return $ Node (Jump lbl) ()
-
-save :: PhysReg -> Dst Reg -> BodyF Reg
-save r dst = Free (Node (Save (Linearity False) r dst) (), Pure ())
-
-restore :: Src Reg -> PhysReg -> BodyF Reg
-restore src r = Free (Node (Restore (Linearity False) src r) (), Pure ())