diff --git a/LinearScan.hs b/LinearScan.hs
--- a/LinearScan.hs
+++ b/LinearScan.hs
@@ -4,7 +4,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 
-{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}
+{-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
 
 module LinearScan
     ( -- * Main entry point
@@ -29,16 +29,18 @@
 import qualified Data.IntSet as S
 import qualified Data.List as L
 import           Debug.Trace
+import qualified LinearScan.Applicative as LS
 import qualified LinearScan.Blocks as LS
 import           LinearScan.Blocks as LS
 import qualified LinearScan.IntMap as LS
+import qualified LinearScan.IntSet 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.Monad as LS
-import qualified LinearScan.Morph as LS
 import qualified LinearScan.Range as LS
+import qualified LinearScan.Trace as LS
 import qualified LinearScan.UsePos as LS
 import qualified LinearScan.Utils as LS
 import           LinearScan.Yoneda (Any)
@@ -134,9 +136,6 @@
 deriving instance Show LS.IntervalDesc
 deriving instance Show LS.RangeDesc
 deriving instance Show LS.UsePos
-deriving instance Show LS.SplitReason
-deriving instance Show LS.SpillDetails
-deriving instance Show LS.SplitPosition
 
 instance Show ScanStateDesc where
     show sd =
@@ -262,21 +261,21 @@
              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 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
+    -- 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
 
 -- | From the point of view of this library, a basic block is nothing more
@@ -322,7 +321,7 @@
         (\blk -> let (x, y, z) = d blk in ((x, y), z)) e
 
 data Details m blk1 blk2 op1 op2 = Details
-    { reason          :: Maybe (LS.SSError, LS.FinalStage)
+    { reason          :: Maybe ([LS.SSTrace], LS.FinalStage)
     , liveSets        :: [(Int, LS.BlockLiveSets)]
     , _inputBlocks    :: [blk1]
     , orderedBlocks   :: [blk1]
@@ -360,10 +359,24 @@
                          (liveSets err) (orderedBlocks err))
             (return ("\n" ++ show sd))
 
-deriving instance Show LS.SSError
 deriving instance Show LS.FinalStage
 deriving instance Show LS.BlockLiveSets
 
+instance Show LS.SpillConditionT where
+    show (LS.NewToHandledT uid) = "new interval " ++ show uid
+    show (LS.UnhandledToHandledT uid) = "unhandled interval " ++ show uid
+    show (LS.ActiveToHandledT xid reg) =
+        "active interval "++ show xid ++ " for register " ++ show reg
+    show (LS.InactiveToHandledT xid reg) =
+        "inactive interval "++ show xid ++ " for register " ++ show reg
+
+instance Show LS.SplitPositionT where
+    show (LS.BeforePosT pos)         = "before " ++ show pos
+    show (LS.EndOfLifetimeHoleT pos) =
+        "at end of lifetime hole after " ++ show pos
+
+deriving instance Show LS.SSTrace
+
 toDetails :: LS.Details blk1 blk2
           -> LinearScan.BlockInfo m blk1 blk2 op1 op2
           -> LinearScan.OpInfo m op1 op2
@@ -387,17 +400,17 @@
          => Int        -- ^ Maximum number of registers to use
          -> LinearScan.BlockInfo m blk1 blk2 op1 op2
          -> LinearScan.OpInfo m op1 op2
-         -> [blk1] -> m (Either String [blk2])
-allocate 0 _ _ _  = return $ Left "Cannot allocate with no registers"
-allocate _ _ _ [] = return $ Left "No basic blocks were provided"
+         -> [blk1] -> m (Either [String] [blk2])
+allocate 0 _ _ _  = return $ Left ["Cannot allocate with no registers"]
+allocate _ _ _ [] = return $ Left ["No basic blocks were provided"]
 allocate maxReg binfo oinfo blocks = do
     x <- LS.linearScan dict maxReg
        (fromBlockInfo binfo) (fromOpInfo oinfo) blocks $ \res ->
        toDetails res binfo oinfo
     let res' = U.unsafeCoerce (x :: Any) :: Details m blk1 blk2 op1 op2
     dets <- showDetails res'
-    return $ tracer dets $ case reason res' of
-        Just (err, _) -> Left  $ reasonToStr err
+    return $ case reason res' of
+        Just (err, _) -> Left  $ tracer dets $ map reasonToStr err
         Nothing       -> Right $ allocatedBlocks res'
   where
     dict :: LS.Monad (m Any)
@@ -412,20 +425,49 @@
           U.unsafeCoerce (join (U.unsafeCoerce x :: m (m Any)) :: m Any))
 
     reasonToStr r = case r of
-        LS.ECannotInsertUnhAtPos spillDets pos ->
-            "Cannot insert interval " ++ show spillDets
-              ++ " onto unhandled list (use at position "
-              ++ show pos ++ ")"
+        LS.EIntersectsWithFixedInterval pos reg ->
+            "Current interval intersects with " ++
+            "fixed interval for register " ++ show reg ++ " at " ++ show pos
+        LS.ESplitAssignedIntervalForReg reg ->
+            "Splitting assigned interval for register " ++ show reg
+        LS.ESplitActiveOrInactiveInterval b ->
+            "Splitting " ++ (if b then "active" else "inactive") ++ " interval"
+        LS.ESpillInterval cond ->
+            "Spilling " ++ show cond
+        LS.ESplitUnhandledInterval ->
+            "Splitting unhandled interval"
+        LS.EIntervalHasUsePosReqReg pos ->
+            "Interval has use position requiring register at " ++ show pos
+        LS.EIntervalBeginsAtSplitPosition ->
+            "Interval begins at split position"
+        LS.EMoveUnhandledToActive reg ->
+            "Allocating unhandled interval at register " ++ show reg
+        LS.ESplitActiveIntervalForReg reg ->
+            "Splitting active interval for register " ++ show reg
+        LS.ESplitAnyInactiveIntervalForReg reg ->
+            "Splitting any inactive interval for register " ++ show reg
+        LS.ESpillCurrentInterval ->
+            "Spilling current interval"
+        LS.ESplitCurrentInterval pos ->
+            "Splitting current interval " ++ show pos
+        LS.ETryAllocateFreeReg reg mpos xid ->
+            "Trying to allocate register " ++ show reg
+                ++ " at " ++ show mpos ++ " for interval " ++ show xid
+        LS.EAllocateBlockedReg reg mpos xid ->
+            "Allocating blocked register " ++ show reg
+                ++ " at " ++ show mpos ++ " for interval " ++ show xid
+        LS.ERemoveUnhandledInterval xid ->
+            "Removing unhandled interval " ++ show xid
+
+        LS.ECannotInsertUnhandled ->
+            "Cannot insert interval onto unhandled list"
         LS.EIntervalBeginsBeforeUnhandled xid ->
             "Cannot spill interval " ++ show xid
                 ++ " (begins before current position)"
-        LS.ENoValidSplitPositionUnh splitPos xid ->
-            "No split position found for unhandled interval " ++ show xid
-                ++ " @ " ++ show splitPos
-        LS.ENoValidSplitPosition splitPos xid ->
-            "No split position found for " ++ show xid ++ " @ " ++ show splitPos
-        LS.ECannotSplitSingleton splitPos xid ->
-            "Interval " ++ show xid ++ " is a singleton @ " ++ show splitPos
+        LS.ENoValidSplitPosition xid ->
+            "No split position found for " ++ show xid
+        LS.ECannotSplitSingleton xid ->
+            "Interval " ++ show xid ++ " is a singleton"
         LS.ERegisterAlreadyAssigned reg ->
             "Register " ++ show reg ++ " already assigned"
         LS.ERegisterAssignmentsOverlap reg ->
diff --git a/LinearScan/Allocate.hs b/LinearScan/Allocate.hs
--- a/LinearScan/Allocate.hs
+++ b/LinearScan/Allocate.hs
@@ -13,14 +13,17 @@
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
+import qualified LinearScan.Context as Context
 import qualified LinearScan.Cursor as Cursor
-import qualified LinearScan.IState as IState
 import qualified LinearScan.Interval as Interval
 import qualified LinearScan.Lib as Lib
 import qualified LinearScan.Morph as Morph
+import qualified LinearScan.Prelude0 as Prelude0
 import qualified LinearScan.ScanState as ScanState
 import qualified LinearScan.Specif as Specif
+import qualified LinearScan.Spill as Spill
 import qualified LinearScan.Split as Split
+import qualified LinearScan.Trace as Trace
 import qualified LinearScan.UsePos as UsePos
 import qualified LinearScan.Eqtype as Eqtype
 import qualified LinearScan.Fintype as Fintype
@@ -55,19 +58,19 @@
 
 intersectsWithFixedInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
                                PhysReg -> Morph.SState () ()
-                               (Prelude.Maybe Lib.Coq_oddnum)
+                               (Prelude.Maybe Prelude0.Coq_oddnum)
 intersectsWithFixedInterval maxReg pre reg =
   Cursor.withCursor maxReg pre (\sd _ ->
     let {int = Cursor.curIntDetails maxReg sd} in
-    Morph.return_
+    Context.ipure
       (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) -> []
-                     (Prelude.Maybe Lib.Coq_oddnum)
+updateRegisterPos :: Prelude.Int -> ([] (Prelude.Maybe Prelude0.Coq_oddnum))
+                     -> Prelude.Int -> (Prelude.Maybe Prelude0.Coq_oddnum) ->
+                     [] (Prelude.Maybe Prelude0.Coq_oddnum)
 updateRegisterPos n v r p =
   case p of {
    Prelude.Just x ->
@@ -80,6 +83,39 @@
         Prelude.Nothing -> x}));
    Prelude.Nothing -> v}
 
+convert_oddnum :: (Prelude.Maybe Prelude0.Coq_oddnum) -> Prelude.Maybe
+                  Prelude.Int
+convert_oddnum x =
+  case x of {
+   Prelude.Just x0 -> Prelude.Just ( x0);
+   Prelude.Nothing -> Prelude.Nothing}
+
+findEligibleRegister :: Prelude.Int -> ScanState.ScanStateDesc ->
+                        Interval.IntervalDesc -> ([]
+                        (Prelude.Maybe Prelude0.Coq_oddnum)) -> (,) PhysReg
+                        (Prelude.Maybe Prelude0.Coq_oddnum)
+findEligibleRegister maxReg sd d xs =
+  case (LinearScan.Utils.vfoldl'_with_index) maxReg (\reg acc mint ->
+         case acc of {
+          (,) fup fai ->
+           case mint of {
+            Prelude.Just int ->
+             let {ip = Interval.intervalIntersectionPoint ( int) d} in
+             let {
+              intersects = case ip of {
+                            Prelude.Just o -> Prelude.True;
+                            Prelude.Nothing -> Prelude.False}}
+             in
+             (,)
+             (updateRegisterPos maxReg fup reg
+               (Interval.intervalIntersectionPoint ( int) d))
+             (LinearScan.Utils.set_nth maxReg fai reg intersects);
+            Prelude.Nothing -> acc}}) ((,) xs
+         (Data.List.replicate maxReg Prelude.False))
+         (ScanState.fixedIntervals maxReg sd) of {
+   (,) xs0 fixedAndIntersects ->
+    ScanState.registerWithHighestPos maxReg fixedAndIntersects xs0}
+
 tryAllocateFreeReg :: Prelude.Int -> ScanState.ScanStateDesc -> Morph.SState
                       () () (Prelude.Maybe (Morph.SState () () PhysReg))
 tryAllocateFreeReg maxReg pre =
@@ -91,7 +127,7 @@
        (,) i r -> updateRegisterPos maxReg v r (f i)}}
     in
     let {
-     freeUntilPos' = Data.List.foldl' (go (\x -> Prelude.Just Lib.odd1))
+     freeUntilPos' = Data.List.foldl' (go (\x -> Prelude.Just Prelude0.odd1))
                        (Data.List.replicate maxReg Prelude.Nothing)
                        (ScanState.active maxReg sd)}
     in
@@ -117,39 +153,31 @@
                             ( (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 {
+    case findEligibleRegister maxReg sd ( (Cursor.curIntDetails maxReg sd))
+           freeUntilPos'' of {
      (,) reg mres ->
       let {
-       success = Morph.stbind (\x -> Morph.return_ reg)
+       success = Context.ibind (\x -> Context.ipure reg)
                    (Morph.moveUnhandledToActive maxReg pre reg)}
       in
-      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 (Morph.BeforePos n
-                    (Morph.AvailableForPart
-                    ( (Prelude.fst (Cursor.curId maxReg sd))))))})};
-          Prelude.Nothing -> Prelude.Just success})})
+      let {cid = Cursor.curId maxReg sd} in
+      Context.context (Trace.ETryAllocateFreeReg ( reg) (convert_oddnum mres)
+        ( (Prelude.fst cid)))
+        (Context.ipure
+          (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 ->
+                  Context.ibind (\x -> success)
+                    (Split.splitCurrentInterval maxReg pre (Split.BeforePos
+                      n))})};
+            Prelude.Nothing -> Prelude.Just success}))})
 
 allocateBlockedReg :: Prelude.Int -> ScanState.ScanStateDesc -> Morph.SState
                       () () (Prelude.Maybe PhysReg)
@@ -170,7 +198,7 @@
         in
         let {
          pos' = case Interval.findIntervalUsePos ( int) atPos of {
-                 Prelude.Just s -> Prelude.Just Lib.odd1;
+                 Prelude.Just s -> Prelude.Just Prelude0.odd1;
                  Prelude.Nothing -> Interval.nextUseAfter ( int) start}}
         in
         updateRegisterPos n v r pos'}}
@@ -190,58 +218,52 @@
                      (resolve (ScanState.active maxReg sd))}
     in
     let {
-     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))}
+     intersectingIntervals = Prelude.filter (\x ->
+                               Interval.intervalsIntersect
+                                 ( (Cursor.curIntDetails maxReg sd))
+                                 ( (Prelude.fst x)))
+                               (resolve (ScanState.inactive maxReg sd))}
     in
     let {
-     nextUsePos = Data.List.foldl' (go maxReg) nextUsePos'
-                    intersectingIntervals}
+     nextUsePos'' = Data.List.foldl' (go maxReg) nextUsePos'
+                      intersectingIntervals}
     in
-    case ScanState.registerWithHighestPos maxReg nextUsePos of {
+    case findEligibleRegister maxReg sd ( (Cursor.curIntDetails maxReg sd))
+           nextUsePos'' of {
      (,) reg mres ->
-      case case mres of {
-            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 ->
-        Morph.stbind (\x -> Morph.return_ Prelude.Nothing)
-          (Split.spillCurrentInterval maxReg pre);
-       Prelude.False ->
-        Morph.stbind (\x ->
-          Morph.stbind (\x0 ->
-            Morph.stbind (\mloc ->
-              Morph.stbind (\x1 ->
-                Morph.stbind (\x2 -> Morph.return_ (Prelude.Just reg))
-                  (Morph.moveUnhandledToActive maxReg pre reg))
-                (case mloc of {
-                  Prelude.Just n ->
-                   Split.splitCurrentInterval maxReg pre (Morph.BeforePos n
-                     (Morph.IntersectsWithFixed ( reg)));
-                  Prelude.Nothing -> Morph.return_ ()}))
-              (intersectsWithFixedInterval maxReg pre reg))
-            (Split.splitActiveIntervalForReg maxReg pre reg pos))
-          (Split.splitAnyInactiveIntervalForReg maxReg pre reg pos)}})
+      let {cid = Cursor.curId maxReg sd} in
+      Context.context (Trace.EAllocateBlockedReg ( reg) (convert_oddnum mres)
+        ( (Prelude.fst cid)))
+        (case case mres of {
+               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 ->
+           Context.ibind (\x -> Context.ipure Prelude.Nothing)
+             (Spill.spillCurrentInterval maxReg pre);
+          Prelude.False ->
+           Context.ibind (\x ->
+             Context.ibind (\x0 ->
+               Context.ibind (\mloc ->
+                 Context.ibind (\x1 ->
+                   Context.ibind (\x2 -> Context.ipure (Prelude.Just reg))
+                     (Morph.moveUnhandledToActive maxReg pre reg))
+                   (case mloc of {
+                     Prelude.Just n ->
+                      Context.context (Trace.EIntersectsWithFixedInterval
+                        ( n) ( reg))
+                        (Split.splitCurrentInterval maxReg pre
+                          (Split.BeforePos n));
+                     Prelude.Nothing -> Context.ipure ()}))
+                 (intersectsWithFixedInterval maxReg pre reg))
+               (Split.splitActiveIntervalForReg maxReg pre reg pos))
+             (Split.splitAnyInactiveIntervalForReg maxReg pre reg pos)})})
 
 morphlen_transport :: Prelude.Int -> ScanState.ScanStateDesc ->
                       ScanState.ScanStateDesc -> ScanState.IntervalId ->
@@ -295,13 +317,14 @@
              (unsafeCoerce (\x x0 _ -> mt_fst maxReg x x0))
              (unsafeCoerce (\x _ x0 x1 _ -> goActive maxReg pos sd x x0 x1))}
     in
-    IState.iput (Morph.Build_SSInfo res __))
+    Context.iput (Morph.Build_SSInfo res __))
 
 moveInactiveToActive' :: Prelude.Int -> ScanState.ScanStateDesc -> ((,)
                          ScanState.IntervalId PhysReg) -> Coq_int_reg_seq ->
-                         Prelude.Either Morph.SSError
+                         ([] Trace.SSTrace) -> Prelude.Either
+                         ([] Trace.SSTrace)
                          (Specif.Coq_sig2 ScanState.ScanStateDesc)
-moveInactiveToActive' maxReg z x xs =
+moveInactiveToActive' maxReg z x xs e =
   let {
    filtered_var = Prelude.not
                     (Ssrbool.in_mem (Prelude.snd (unsafeCoerce x))
@@ -317,14 +340,14 @@
      filtered_var0 = Morph.moveInactiveToActive maxReg z (unsafeCoerce x)}
     in
     Prelude.Right filtered_var0;
-   Prelude.False -> Prelude.Left (Morph.ERegisterAssignmentsOverlap
-    ( (Prelude.snd x)))}
+   Prelude.False -> Prelude.Left ((:) (Trace.ERegisterAssignmentsOverlap
+    ( (Prelude.snd x))) e)}
 
-goInactive :: Prelude.Int -> Prelude.Int -> ScanState.ScanStateDesc ->
-              ScanState.ScanStateDesc -> ((,) ScanState.IntervalId PhysReg)
-              -> Coq_int_reg_seq -> Prelude.Either Morph.SSError
-              Coq_intermediate_result
-goInactive maxReg pos sd z x xs =
+goInactive :: Prelude.Int -> Prelude.Int -> ScanState.ScanStateDesc -> ([]
+              Trace.SSTrace) -> ScanState.ScanStateDesc -> ((,)
+              ScanState.IntervalId PhysReg) -> Coq_int_reg_seq ->
+              Prelude.Either ([] Trace.SSTrace) Coq_intermediate_result
+goInactive maxReg pos sd e z x xs =
   let {f = \sd' -> Prelude.Right sd'} in
   case (Prelude.<=) ((Prelude.succ)
          (Interval.intervalEnd
@@ -343,7 +366,7 @@
              (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)
                (ScanState.intervals maxReg z) (Prelude.fst x))) pos of {
      Prelude.True ->
-      let {filtered_var = moveInactiveToActive' maxReg z x xs} in
+      let {filtered_var = moveInactiveToActive' maxReg z x xs e} in
       case filtered_var of {
        Prelude.Left err -> Prelude.Left err;
        Prelude.Right s -> f s};
@@ -353,21 +376,23 @@
                           Prelude.Int -> Morph.SState () () ()
 checkInactiveIntervals maxReg pre pos =
   Morph.withScanStatePO maxReg pre (\sd _ ->
-    let {
-     eres = Lib.dep_foldl_invE (\s ->
-              Eqtype.prod_eqType
-                (Fintype.ordinal_eqType (ScanState.nextInterval maxReg s))
-                (Fintype.ordinal_eqType maxReg)) sd
-              (unsafeCoerce (ScanState.inactive maxReg sd))
-              (Data.List.length (ScanState.inactive maxReg sd))
-              (unsafeCoerce (ScanState.inactive maxReg))
-              (unsafeCoerce (\x x0 _ -> mt_fst maxReg x x0))
-              (unsafeCoerce (\x _ x0 x1 _ ->
-                goInactive maxReg pos sd x x0 x1))}
-    in
-    case eres of {
-     Prelude.Left err -> Morph.error_ err;
-     Prelude.Right s -> IState.iput (Morph.Build_SSInfo s __)})
+    Context.ibind (\e ->
+      let {
+       eres = Lib.dep_foldl_invE (\s ->
+                Eqtype.prod_eqType
+                  (Fintype.ordinal_eqType (ScanState.nextInterval maxReg s))
+                  (Fintype.ordinal_eqType maxReg)) sd
+                (unsafeCoerce (ScanState.inactive maxReg sd))
+                (Data.List.length (ScanState.inactive maxReg sd))
+                (unsafeCoerce (ScanState.inactive maxReg))
+                (unsafeCoerce (\x x0 _ -> mt_fst maxReg x x0))
+                (unsafeCoerce (\x _ x0 x1 _ ->
+                  goInactive maxReg pos sd e x x0 x1))}
+      in
+      case eres of {
+       Prelude.Left err -> Morph.error_ maxReg sd err;
+       Prelude.Right s -> Context.iput (Morph.Build_SSInfo s __)})
+      Context.iask)
 
 handleInterval :: Prelude.Int -> ScanState.ScanStateDesc -> Morph.SState 
                   () () (Prelude.Maybe PhysReg)
@@ -377,11 +402,11 @@
     case Interval.firstUsePos
            (Interval.getIntervalDesc ( (Cursor.curIntDetails maxReg sd))) of {
      Prelude.Just u ->
-      Morph.stbind (\x ->
-        Morph.stbind (\x0 ->
-          Morph.stbind (\mres ->
+      Context.ibind (\x ->
+        Context.ibind (\x0 ->
+          Context.ibind (\mres ->
             case mres of {
-             Prelude.Just x1 -> IState.imap (\x2 -> Prelude.Just x2) x1;
+             Prelude.Just x1 -> Context.imap (\x2 -> Prelude.Just x2) x1;
              Prelude.Nothing -> allocateBlockedReg maxReg pre})
             (tryAllocateFreeReg maxReg pre))
           (Morph.liftLen maxReg pre (\sd0 ->
@@ -389,25 +414,27 @@
         (Morph.liftLen maxReg pre (\sd0 ->
           checkActiveIntervals maxReg sd0 position));
      Prelude.Nothing ->
-      Morph.stbind (\x -> Morph.return_ Prelude.Nothing)
+      Context.ibind (\x -> Context.ipure 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;
+  case Context.ibind (\x -> checkInactiveIntervals maxReg sd finalPos)
+         (checkActiveIntervals maxReg sd finalPos) [] (Morph.Build_SSInfo sd
+         __) of {
+   Prelude.Left l -> 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
+                 ((,) ([] Trace.SSTrace) 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 ((,) ((:) Trace.EFuelExhausted [])
     (ScanState.packScanState maxReg ScanState.InUse sd)))
     (\n ->
     let {
@@ -418,7 +445,7 @@
                (Morph.thisDesc maxReg sd ss)
                __))
                (\cnt ->
-               case handleInterval maxReg sd ss of {
+               case handleInterval maxReg sd [] ss of {
                 Prelude.Left err -> Prelude.Left ((,) err
                  (ScanState.packScanState maxReg ScanState.InUse
                    (Morph.thisDesc maxReg sd ss)));
@@ -434,8 +461,8 @@
                      (\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 ((,) ((:)
+                       Trace.EUnexpectedNoMoreUnhandled [])
                        (ScanState.packScanState maxReg ScanState.InUse
                          (Morph.thisDesc maxReg sd ss'))))
                        cnt}}})
diff --git a/LinearScan/Applicative.hs b/LinearScan/Applicative.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/Applicative.hs
@@ -0,0 +1,71 @@
+{-# OPTIONS_GHC -cpp -XMagicHash #-}
+{- For Hugs, use the option -F"cpp -P -traditional" -}
+
+module LinearScan.Applicative 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.Functor as Functor
+
+
+
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base as GHC.Base
+import qualified GHC.Prim as GHC.Prim
+#else
+-- HUGS
+import qualified LinearScan.IOExts as IOExts
+#endif
+
+
+#ifdef __GLASGOW_HASKELL__
+--unsafeCoerce :: a -> b
+unsafeCoerce = GHC.Base.unsafeCoerce#
+#else
+-- HUGS
+--unsafeCoerce :: a -> b
+unsafeCoerce = IOExts.unsafeCoerce
+#endif
+
+
+#ifdef __GLASGOW_HASKELL__
+type Any = GHC.Prim.Any
+#else
+-- HUGS
+type Any = ()
+#endif
+
+__ :: any
+__ = Prelude.error "Logical or arity value used"
+
+data Applicative f =
+   Build_Applicative (Functor.Functor f) (() -> Any -> f) (() -> () -> f -> f
+                                                          -> f)
+
+is_functor :: (Applicative a1) -> Functor.Functor a1
+is_functor applicative =
+  case applicative of {
+   Build_Applicative is_functor0 pure0 ap0 -> is_functor0}
+
+pure :: (Applicative a1) -> a2 -> a1
+pure applicative x =
+  case applicative of {
+   Build_Applicative is_functor0 pure0 ap0 -> unsafeCoerce pure0 __ x}
+
+ap :: (Applicative a1) -> a1 -> a1 -> a1
+ap applicative x x0 =
+  case applicative of {
+   Build_Applicative is_functor0 pure0 ap0 -> ap0 __ __ x x0}
+
+liftA2 :: (Applicative a1) -> (a2 -> a3 -> a4) -> a1 -> a1 -> a1
+liftA2 h f x y =
+  ap h (Functor.fmap (is_functor h) f x) y
+
diff --git a/LinearScan/Ascii.hs b/LinearScan/Ascii.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/Ascii.hs
@@ -0,0 +1,19 @@
+
+
+module LinearScan.Ascii 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
+
+
+data Coq_ascii =
+   Ascii Prelude.Bool Prelude.Bool Prelude.Bool Prelude.Bool Prelude.Bool 
+ Prelude.Bool Prelude.Bool Prelude.Bool
+
diff --git a/LinearScan/Assign.hs b/LinearScan/Assign.hs
--- a/LinearScan/Assign.hs
+++ b/LinearScan/Assign.hs
@@ -14,15 +14,19 @@
 import qualified LinearScan.Utils
 
 import qualified LinearScan.Allocate as Allocate
+import qualified LinearScan.Applicative as Applicative
 import qualified LinearScan.Blocks as Blocks
+import qualified LinearScan.Functor as Functor
 import qualified LinearScan.Graph as Graph
 import qualified LinearScan.IntMap as IntMap
 import qualified LinearScan.Interval as Interval
+import qualified LinearScan.Iso as Iso
 import qualified LinearScan.Lens as Lens
-import qualified LinearScan.Lib as Lib
+import qualified LinearScan.List1 as List1
 import qualified LinearScan.LiveSets as LiveSets
 import qualified LinearScan.Monad as Monad
 import qualified LinearScan.Resolve as Resolve
+import qualified LinearScan.State0 as State0
 import qualified LinearScan.UsePos as UsePos
 import qualified LinearScan.Yoneda as Yoneda
 import qualified LinearScan.Eqtype as Eqtype
@@ -120,31 +124,31 @@
   Build_AssnStateInfo ((Prelude.succ) 0) ((Prelude.succ) 0) ((Prelude.succ)
     0) (newAllocState maxReg) IntMap.emptyIntMap IntMap.emptyIntMap []
 
-_assnOpId :: Prelude.Int -> (Monad.Functor a1) -> (Blocks.OpId -> a1) ->
+_assnOpId :: Prelude.Int -> (Functor.Functor a1) -> (Blocks.OpId -> a1) ->
              AssnStateInfo -> a1
 _assnOpId maxReg h f s =
-  Monad.fmap h (\x -> Build_AssnStateInfo x (assnBlockBeg maxReg s)
+  Functor.fmap h (\x -> Build_AssnStateInfo x (assnBlockBeg maxReg s)
     (assnBlockEnd maxReg s) (assnAllocState maxReg s)
     (assnBlockEntryAllocs maxReg s) (assnBlockExitAllocs maxReg s)
     (assnErrors maxReg s)) (f (assnOpId maxReg s))
 
-_assnBlockBeg :: Prelude.Int -> (Monad.Functor a1) -> (Blocks.OpId -> a1) ->
-                 AssnStateInfo -> a1
+_assnBlockBeg :: Prelude.Int -> (Functor.Functor a1) -> (Blocks.OpId -> a1)
+                 -> AssnStateInfo -> a1
 _assnBlockBeg maxReg h f s =
-  Monad.fmap h (\x -> Build_AssnStateInfo (assnOpId maxReg s) x
+  Functor.fmap h (\x -> Build_AssnStateInfo (assnOpId maxReg s) x
     (assnBlockEnd maxReg s) (assnAllocState maxReg s)
     (assnBlockEntryAllocs maxReg s) (assnBlockExitAllocs maxReg s)
     (assnErrors maxReg s)) (f (assnBlockBeg maxReg s))
 
-_assnBlockEnd :: Prelude.Int -> (Monad.Functor a1) -> (Blocks.OpId -> a1) ->
-                 AssnStateInfo -> a1
+_assnBlockEnd :: Prelude.Int -> (Functor.Functor a1) -> (Blocks.OpId -> a1)
+                 -> AssnStateInfo -> a1
 _assnBlockEnd maxReg h f s =
-  Monad.fmap h (\x -> Build_AssnStateInfo (assnOpId maxReg s)
+  Functor.fmap h (\x -> Build_AssnStateInfo (assnOpId maxReg s)
     (assnBlockBeg maxReg s) x (assnAllocState maxReg s)
     (assnBlockEntryAllocs maxReg s) (assnBlockExitAllocs maxReg s)
     (assnErrors maxReg s)) (f (assnBlockEnd maxReg s))
 
-type AssnState mType a = Monad.StateT AssnStateInfo mType a
+type AssnState mType a = State0.StateT AssnStateInfo mType a
 
 generateMoves :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo a3 
                  a1 a2) -> ([] Resolve.ResolvingMove) -> a3
@@ -152,14 +156,15 @@
   Monad.forFoldrM mDict [] moves (\mv acc ->
     let {
      k = (Prelude..)
-           (Monad.fmap (Monad.is_functor (Monad.is_applicative mDict)) (\x ->
+           (Functor.fmap
+             (Applicative.is_functor (Monad.is_applicative mDict)) (\x ->
              Prelude.Just x))
-           (Yoneda.iso_to
+           (Iso.iso_to
              (Yoneda.coq_Yoneda_lemma
-               (Monad.is_functor (Monad.is_applicative mDict))))}
+               (Applicative.is_functor (Monad.is_applicative mDict))))}
     in
     Monad.bind mDict (\mops ->
-      Monad.pure (Monad.is_applicative mDict)
+      Applicative.pure (Monad.is_applicative mDict)
         (case mops of {
           Prelude.Just ops -> (Prelude.++) ops acc;
           Prelude.Nothing -> acc}))
@@ -174,7 +179,7 @@
          k (\_ ->
            Blocks.restoreOp maxReg mDict oinfo (Prelude.Just vid) dreg);
         Resolve.Nop ->
-         Monad.pure (Monad.is_applicative mDict) Prelude.Nothing}))
+         Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing}))
 
 varAllocs :: Prelude.Int -> Prelude.Int -> ([] Allocate.Allocation) ->
              Blocks.VarInfo -> [] ((,) Blocks.VarId PhysReg)
@@ -183,7 +188,7 @@
    Prelude.Left p -> [];
    Prelude.Right vid ->
     Prelude.map (\x -> (,) vid x)
-      (Lib.catMaybes
+      (List1.catMaybes
         (Prelude.map (\i -> Allocate.intReg maxReg i)
           (Prelude.filter (\i ->
             let {int = Allocate.intVal maxReg i} in
@@ -200,36 +205,37 @@
                   a1 a2) -> ([] Allocate.Allocation) -> a1 -> AssnState 
                   a3 ([] a2)
 setAllocations maxReg mDict oinfo allocs op =
-  Monad.bind (Monad.coq_StateT_Monad mDict) (\assn ->
+  Monad.bind (State0.coq_StateT_Monad mDict) (\assn ->
     let {opid = assnOpId maxReg assn} in
     let {vars = Blocks.opRefs maxReg mDict oinfo op} in
     let {
-     regs = Monad.concat (Prelude.map (varAllocs maxReg opid allocs) vars)}
+     regs = List1.concat (Prelude.map (varAllocs maxReg opid allocs) vars)}
     in
-    Monad.bind (Monad.coq_StateT_Monad mDict) (\ops ->
-      Monad.bind (Monad.coq_StateT_Monad mDict) (\transitions ->
-        Monad.bind (Monad.coq_StateT_Monad mDict) (\x ->
-          Monad.pure (Monad.coq_StateT_Applicative mDict)
+    Monad.bind (State0.coq_StateT_Monad mDict) (\ops ->
+      Monad.bind (State0.coq_StateT_Monad mDict) (\transitions ->
+        Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
+          Applicative.pure (State0.coq_StateT_Applicative mDict)
             ((Prelude.++) ops transitions))
-          (Monad.modifyT (Monad.is_applicative mDict)
+          (State0.modifyT (Monad.is_applicative mDict)
             (Lens.set (\_ -> _assnOpId maxReg) ((Prelude.succ)
               ((Prelude.succ) opid)))))
         (case (Prelude.&&) ((Prelude.<=) (assnBlockBeg maxReg assn) opid)
                 ((Prelude.<=) ((Prelude.succ) opid)
                   (assnBlockEnd maxReg assn)) of {
           Prelude.True ->
-           Monad.lift mDict
+           State0.lift mDict
              (generateMoves maxReg mDict oinfo
                (Resolve.determineMoves maxReg
                  (Resolve.resolvingMoves maxReg allocs opid ((Prelude.succ)
                    ((Prelude.succ) opid)))));
-          Prelude.False -> Monad.pure (Monad.coq_StateT_Applicative mDict) []}))
-      (Monad.lift mDict
-        (Yoneda.iso_to
+          Prelude.False ->
+           Applicative.pure (State0.coq_StateT_Applicative mDict) []}))
+      (State0.lift mDict
+        (Iso.iso_to
           (Yoneda.coq_Yoneda_lemma
-            (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->
+            (Applicative.is_functor (Monad.is_applicative mDict))) (\_ ->
           Blocks.applyAllocs maxReg mDict oinfo op regs))))
-    (Monad.getT (Monad.is_applicative mDict))
+    (State0.getT (Monad.is_applicative mDict))
 
 resolveMappings :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo 
                    a3 a1 a2) -> Prelude.Int -> ([] a2) -> (IntMap.IntMap
@@ -241,7 +247,7 @@
      (,) gbeg gend ->
       Monad.bind mDict (\bmoves ->
         Monad.bind mDict (\emoves ->
-          Monad.pure (Monad.is_applicative mDict)
+          Applicative.pure (Monad.is_applicative mDict)
             ((Prelude.++) bmoves ((Prelude.++) opsm emoves)))
           (generateMoves maxReg mDict oinfo
             (Prelude.map (Resolve.moveFromGraph maxReg)
@@ -253,7 +259,7 @@
             (Graph.topsort
               (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
                 Ssrnat.nat_eqType) gbeg)))};
-   Prelude.Nothing -> Monad.pure (Monad.is_applicative mDict) opsm}
+   Prelude.Nothing -> Applicative.pure (Monad.is_applicative mDict) opsm}
 
 considerOps :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 
                a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([]
@@ -261,53 +267,57 @@
                -> (IntMap.IntMap Resolve.BlockMoves) -> ([] a1) -> AssnState
                a5 ([] a2)
 considerOps maxReg mDict binfo oinfo allocs liveSets mappings =
-  Monad.mapM (Monad.coq_StateT_Applicative mDict) (\blk ->
+  Monad.mapM (State0.coq_StateT_Applicative mDict) (\blk ->
     case Blocks.blockOps mDict binfo blk of {
      (,) p opse ->
       case p of {
        (,) opsb opsm ->
-        Monad.bind (Monad.coq_StateT_Monad mDict) (\x ->
+        Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
           let {k = setAllocations maxReg mDict oinfo allocs} in
-          Monad.bind (Monad.coq_StateT_Monad mDict) (\opsb' ->
-            Monad.bind (Monad.coq_StateT_Monad mDict) (\opsm' ->
-              Monad.bind (Monad.coq_StateT_Monad mDict) (\opse' ->
-                Monad.bind (Monad.coq_StateT_Monad mDict) (\bid ->
-                  Monad.bind (Monad.coq_StateT_Monad mDict) (\opsm'' ->
+          Monad.bind (State0.coq_StateT_Monad mDict) (\opsb' ->
+            Monad.bind (State0.coq_StateT_Monad mDict) (\opsm' ->
+              Monad.bind (State0.coq_StateT_Monad mDict) (\opse' ->
+                Monad.bind (State0.coq_StateT_Monad mDict) (\bid ->
+                  Monad.bind (State0.coq_StateT_Monad mDict) (\opsm'' ->
                     case opsb' of {
                      [] ->
                       case opse' of {
                        [] ->
-                        Monad.pure (Monad.coq_StateT_Applicative mDict)
+                        Applicative.pure
+                          (State0.coq_StateT_Applicative mDict)
                           (Blocks.setBlockOps mDict binfo blk [] opsm'' []);
                        (:) e es ->
-                        Monad.pure (Monad.coq_StateT_Applicative mDict)
+                        Applicative.pure
+                          (State0.coq_StateT_Applicative mDict)
                           (Blocks.setBlockOps mDict binfo blk []
                             ((Prelude.++) opsm'' (Seq.belast e es)) ((:)
                             (Seq.last e es) []))};
                      (:) b bs ->
                       case opse' of {
                        [] ->
-                        Monad.pure (Monad.coq_StateT_Applicative mDict)
+                        Applicative.pure
+                          (State0.coq_StateT_Applicative mDict)
                           (Blocks.setBlockOps mDict binfo blk ((:) b [])
                             ((Prelude.++) bs opsm'') []);
                        (:) e es ->
-                        Monad.pure (Monad.coq_StateT_Applicative mDict)
+                        Applicative.pure
+                          (State0.coq_StateT_Applicative mDict)
                           (Blocks.setBlockOps mDict binfo blk ((:) b [])
                             ((Prelude.++) bs
                               ((Prelude.++) opsm'' (Seq.belast e es))) ((:)
                             (Seq.last e es) []))}})
-                    (Monad.lift mDict
+                    (State0.lift mDict
                       (resolveMappings maxReg mDict oinfo bid opsm' mappings)))
-                  (Monad.lift mDict
-                    (Yoneda.iso_to
+                  (State0.lift mDict
+                    (Iso.iso_to
                       (Yoneda.coq_Yoneda_lemma
-                        (Monad.is_functor (Monad.is_applicative mDict)))
+                        (Applicative.is_functor (Monad.is_applicative mDict)))
                       (\_ -> Blocks.blockId mDict binfo blk))))
-                (Monad.concatMapM (Monad.coq_StateT_Applicative mDict) k
+                (Monad.concatMapM (State0.coq_StateT_Applicative mDict) k
                   opse))
-              (Monad.concatMapM (Monad.coq_StateT_Applicative mDict) k opsm))
-            (Monad.concatMapM (Monad.coq_StateT_Applicative mDict) k opsb))
-          (Monad.modifyT (Monad.is_applicative mDict) (\assn ->
+              (Monad.concatMapM (State0.coq_StateT_Applicative mDict) k opsm))
+            (Monad.concatMapM (State0.coq_StateT_Applicative mDict) k opsb))
+          (State0.modifyT (Monad.is_applicative mDict) (\assn ->
             let {opid = Lens.view (\_ -> _assnOpId maxReg) assn} in
             Lens.set (\_ -> _assnBlockEnd maxReg)
               ((Prelude.+) opid
@@ -324,7 +334,8 @@
                 LiveSets.BlockLiveSets) -> (IntMap.IntMap Resolve.BlockMoves)
                 -> ([] a1) -> a5
 assignRegNum maxReg mDict binfo oinfo allocs liveSets mappings blocks =
-  Monad.fmap (Monad.is_functor (Monad.is_applicative mDict)) Prelude.fst
+  Functor.fmap (Applicative.is_functor (Monad.is_applicative mDict))
+    Prelude.fst
     (considerOps maxReg mDict binfo oinfo allocs liveSets mappings blocks
       (newAssnStateInfo maxReg))
 
diff --git a/LinearScan/Build.hs b/LinearScan/Build.hs
--- a/LinearScan/Build.hs
+++ b/LinearScan/Build.hs
@@ -13,16 +13,21 @@
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
+import qualified LinearScan.Applicative as Applicative
 import qualified LinearScan.Blocks as Blocks
 import qualified LinearScan.Datatypes as Datatypes
+import qualified LinearScan.Functor as Functor
 import qualified LinearScan.IntMap as IntMap
+import qualified LinearScan.IntSet as IntSet
 import qualified LinearScan.Interval as Interval
-import qualified LinearScan.Lib as Lib
+import qualified LinearScan.Iso as Iso
+import qualified LinearScan.List1 as List1
 import qualified LinearScan.LiveSets as LiveSets
 import qualified LinearScan.Logic as Logic
 import qualified LinearScan.Loops as Loops
 import qualified LinearScan.Monad as Monad
-import qualified LinearScan.NonEmpty0 as NonEmpty0
+import qualified LinearScan.NonEmpty as NonEmpty
+import qualified LinearScan.Prelude0 as Prelude0
 import qualified LinearScan.Range as Range
 import qualified LinearScan.ScanState as ScanState
 import qualified LinearScan.Specif as Specif
@@ -67,7 +72,7 @@
 type PendingRanges = [] Range.BoundedRange
 
 emptyPendingRanges :: Prelude.Int -> Prelude.Int -> Prelude.Int ->
-                      IntMap.IntSet -> IntMap.IntMap PendingRanges
+                      IntSet.IntSet -> IntMap.IntMap PendingRanges
 emptyPendingRanges maxReg b e liveOuts =
   (Prelude.flip (Prelude.$)) __ (\_ ->
     (Prelude.flip (Prelude.$))
@@ -75,7 +80,7 @@
         ((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)))
+        (\f -> IntSet.coq_IntSet_foldl f IntMap.emptyIntMap liveOuts)))
 
 coq_BoundedRange_leq :: Prelude.Int -> Prelude.Int -> Range.BoundedRange ->
                         Range.BoundedRange -> Prelude.Bool
@@ -109,7 +114,7 @@
                 (Range.rbeg (Range.getRangeDesc r2')))
               (Prelude.max (Range.rend (Range.getRangeDesc r1))
                 (Range.rend (Range.getRangeDesc r2')))
-              (Lib.sortBy UsePos.upos_le
+              (List1.sortBy UsePos.upos_le
                 ((Prelude.++) (Range.ups (Range.getRangeDesc r1))
                   (Range.ups (Range.getRangeDesc r2')))))) rs2'}
           in
@@ -141,8 +146,8 @@
      _evar_0_0 = \_ ->
       let {
        _top_assumption_ = compilePendingRanges b e
-                            (Lib.insert (coq_BoundedRange_leq b e) r
-                              (Lib.sortBy (coq_BoundedRange_leq b e) ( rs)))}
+                            (List1.insert (coq_BoundedRange_leq b e) r
+                              (List1.sortBy (coq_BoundedRange_leq b e) ( rs)))}
       in
       let {
        _evar_0_0 = \_ _ ->
@@ -155,8 +160,8 @@
          [] -> 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 {
+      case List1.insert (coq_BoundedRange_leq b e) r
+             (List1.sortBy (coq_BoundedRange_leq b e) ( rs)) of {
        [] -> _evar_0_0 __ __;
        (:) x x0 -> _evar_0_1 x x0}}
     in
@@ -176,14 +181,14 @@
   IntMap.coq_IntMap_mergeWithKey (\_the_1st_wildcard_ brs srs2 ->
     let {
      _top_assumption_ = compilePendingRanges b e
-                          (Lib.sortBy (coq_BoundedRange_leq b e) ( brs))}
+                          (List1.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 ->
+      compilePendingRanges b e
+        (List1.sortBy (coq_BoundedRange_leq b e) ( brs)))) (\sr ->
     (Prelude.flip (Prelude.$)) __ (\_ ->
       IntMap.coq_IntMap_map
         (Range.transportSortedRanges ((Prelude.succ) (Ssrnat.double b))
@@ -260,7 +265,7 @@
           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))}
+            (NonEmpty.coq_NE_from_list br ( rs))}
           in
           (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
             (\x ->
@@ -271,7 +276,7 @@
       in
       let {
        _evar_0_0 = \_ -> Prelude.Just
-        (NonEmpty0.coq_NE_from_list (makeNewRange b pos e _top_assumption_)
+        (NonEmpty.coq_NE_from_list (makeNewRange b pos e _top_assumption_)
           ( range0))}
       in
       case upos_before_rend ( res) _top_assumption_ of {
@@ -292,7 +297,7 @@
   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_)
+    (NonEmpty.coq_NE_from_list (makeNewRange b pos e _top_assumption_)
       ( range0))}
   in
   let {
@@ -382,6 +387,12 @@
   let {
    refs' = case Blocks.opKind maxReg mDict oinfo op of {
             Blocks.IsCall ->
+             let {
+              regsNeeded = Seq.count (\r ->
+                             case Blocks.varId maxReg r of {
+                              Prelude.Left p -> Prelude.False;
+                              Prelude.Right v -> Prelude.True}) refs}
+             in
              (Prelude.++)
                (Prelude.filter (\x ->
                  Prelude.not
@@ -392,12 +403,13 @@
                            Ssrnat.nat_eqType))
                        (unsafeCoerce
                          (Prelude.map (Blocks.varId maxReg) refs)))))
-                 (Fintype.image_mem (Fintype.ordinal_finType maxReg) (\n ->
-                   Blocks.Build_VarInfo (Prelude.Left (unsafeCoerce n))
-                   UsePos.Temp Prelude.True)
-                   (Ssrbool.mem
-                     (Seq.seq_predType (Fintype.ordinal_eqType maxReg))
-                     (unsafeCoerce (Fintype.ord_enum maxReg))))) refs;
+                 (Seq.drop regsNeeded
+                   (Fintype.image_mem (Fintype.ordinal_finType maxReg) (\n ->
+                     Blocks.Build_VarInfo (Prelude.Left (unsafeCoerce n))
+                     UsePos.Temp Prelude.True)
+                     (Ssrbool.mem
+                       (Seq.seq_predType (Fintype.ordinal_eqType maxReg))
+                       (unsafeCoerce (Fintype.ord_enum maxReg)))))) refs;
             _ -> refs}}
   in
   handleVars maxReg refs' b pos e ranges
@@ -405,7 +417,7 @@
 reduceBlock :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 
                a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> Prelude.Int ->
                Blocks.BlockId -> a1 -> Loops.LoopState -> (IntMap.IntMap
-               IntMap.IntSet) -> (IntMap.IntMap PendingRanges) ->
+               IntSet.IntSet) -> (IntMap.IntMap PendingRanges) ->
                IntMap.IntMap PendingRanges
 reduceBlock maxReg mDict binfo oinfo pos bid block loops varUses =
   let {sz = Blocks.blockSize mDict binfo block} in
@@ -414,25 +426,25 @@
   (Prelude.flip (Prelude.$)) __ (\_ ranges ->
     (Prelude.flip (Prelude.$))
       (case Prelude.not
-              (IntMap.coq_IntSet_member bid (Loops.loopEndBlocks loops)) of {
+              (IntSet.coq_IntSet_member bid (Loops.loopEndBlocks loops)) of {
         Prelude.True -> ranges;
         Prelude.False ->
          let {
           f = \acc loopIndex blks ->
-           case Prelude.not (IntMap.coq_IntSet_member bid blks) of {
+           case Prelude.not (IntSet.coq_IntSet_member bid blks) of {
             Prelude.True -> acc;
             Prelude.False ->
              case IntMap.coq_IntMap_lookup loopIndex varUses of {
-              Prelude.Just uses -> IntMap.coq_IntSet_union acc uses;
+              Prelude.Just uses -> IntSet.coq_IntSet_union acc uses;
               Prelude.Nothing -> acc}}}
          in
          let {
-          uses = IntMap.coq_IntMap_foldlWithKey f IntMap.emptyIntSet
+          uses = IntMap.coq_IntMap_foldlWithKey f IntSet.emptyIntSet
                    (Loops.loopIndices loops)}
          in
          handleVars maxReg
            (Prelude.map (\u -> Blocks.Build_VarInfo (Prelude.Right u)
-             UsePos.Input Prelude.False) (IntMap.coq_IntSet_toList uses)) pos
+             UsePos.Input Prelude.False) (IntSet.coq_IntSet_toList uses)) pos
            (Prelude.pred ((Prelude.+) pos sz)) ((Prelude.+) pos sz) ranges})
       ((Prelude.flip (Prelude.$)) __ (\_ ->
         let {_evar_0_ = \x -> x} in
@@ -448,12 +460,12 @@
 
 reduceBlocks :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo 
                 a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([] a1) ->
-                Loops.LoopState -> (IntMap.IntMap IntMap.IntSet) ->
+                Loops.LoopState -> (IntMap.IntMap IntSet.IntSet) ->
                 (IntMap.IntMap LiveSets.BlockLiveSets) -> Prelude.Int -> a5
 reduceBlocks maxReg mDict binfo oinfo blocks loops varUses liveSets pos =
   let {
    _evar_0_ = \pos0 ->
-    Monad.pure (Monad.is_applicative mDict) (newBuildState pos0)}
+    Applicative.pure (Monad.is_applicative mDict) (newBuildState pos0)}
   in
   let {
    _evar_0_0 = \b blocks0 iHbs pos0 ->
@@ -465,7 +477,7 @@
           let {
            outs = case IntMap.coq_IntMap_lookup bid liveSets of {
                    Prelude.Just ls -> LiveSets.blockLiveOut ls;
-                   Prelude.Nothing -> IntMap.emptyIntSet}}
+                   Prelude.Nothing -> IntSet.emptyIntSet}}
           in
           let {
            ranges = emptyPendingRanges maxReg pos0 ((Prelude.+) pos0 sz) outs}
@@ -474,12 +486,12 @@
            pending = reduceBlock maxReg mDict binfo oinfo pos0 bid b loops
                        varUses ranges}
           in
-          Monad.fmap (Monad.is_functor (Monad.is_applicative mDict))
+          Functor.fmap (Applicative.is_functor (Monad.is_applicative mDict))
             (mergeIntoSortedRanges pos0 ((Prelude.+) pos0 sz) pending)
             (iHbs ((Prelude.+) pos0 sz)))
-          (Yoneda.iso_to
+          (Iso.iso_to
             (Yoneda.coq_Yoneda_lemma
-              (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->
+              (Applicative.is_functor (Monad.is_applicative mDict))) (\_ ->
             Blocks.blockId mDict binfo b)))}
     in
     let {_evar_0_1 = \_ -> iHbs pos0} in
@@ -504,10 +516,10 @@
           (LinearScan.Utils.set_nth maxReg regs ( vid) (Prelude.Just
             (Interval.packInterval (Interval.Build_IntervalDesc vid
               (Range.rbeg
-                ( (Prelude.head (NonEmpty0.coq_NE_from_list _a_ _l_))))
+                ( (Prelude.head (NonEmpty.coq_NE_from_list _a_ _l_))))
               (Range.rend
-                ( (Prelude.last (NonEmpty0.coq_NE_from_list _a_ _l_))))
-              (NonEmpty0.coq_NE_from_list _a_ _l_))))) vars}
+                ( (Prelude.last (NonEmpty.coq_NE_from_list _a_ _l_))))
+              (NonEmpty.coq_NE_from_list _a_ _l_))))) vars}
         in
         let {
          _evar_0_1 = \_ ->
@@ -516,10 +528,10 @@
             (IntMap.coq_IntMap_insert vid'
               (Interval.packInterval (Interval.Build_IntervalDesc vid'
                 (Range.rbeg
-                  ( (Prelude.head (NonEmpty0.coq_NE_from_list _a_ _l_))))
+                  ( (Prelude.head (NonEmpty.coq_NE_from_list _a_ _l_))))
                 (Range.rend
-                  ( (Prelude.last (NonEmpty0.coq_NE_from_list _a_ _l_))))
-                (NonEmpty0.coq_NE_from_list _a_ _l_))) vars))}
+                  ( (Prelude.last (NonEmpty.coq_NE_from_list _a_ _l_))))
+                (NonEmpty.coq_NE_from_list _a_ _l_))) vars))}
         in
         case (Prelude.<=) ((Prelude.succ) vid) maxReg of {
          Prelude.True -> _evar_0_0 __;
@@ -546,7 +558,7 @@
       (LinearScan.Utils.snoc (ScanState.nextInterval maxReg ( ss))
         (ScanState.intervals maxReg ( ss)) ( i))
       (ScanState.fixedIntervals maxReg ( ss))
-      (Lib.insert (Lib.lebf Prelude.snd) ((,)
+      (List1.insert (Prelude0.lebf Prelude.snd) ((,)
         ( (ScanState.nextInterval maxReg ( ss))) (Interval.ibeg ( i)))
         (Prelude.map Prelude.id (ScanState.unhandled maxReg ( ss))))
       (Prelude.map Prelude.id (ScanState.active maxReg ( ss)))
@@ -555,10 +567,10 @@
   in
   case blocks of {
    [] ->
-    Monad.pure (Monad.is_applicative mDict) (Prelude.Right
+    Applicative.pure (Monad.is_applicative mDict)
       (ScanState.packScanState maxReg ScanState.InUse
         (ScanState.Build_ScanStateDesc 0 []
-        (Data.List.replicate maxReg Prelude.Nothing) [] [] [] [])));
+        (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []));
    (:) b bs ->
     Monad.bind mDict (\varUses ->
       Monad.bind mDict (\reduced ->
@@ -589,8 +601,8 @@
           in
           let {s3 = IntMap.coq_IntMap_foldl add_unhandled_interval s2 vars}
           in
-          Monad.pure (Monad.is_applicative mDict) (Prelude.Right
-            (ScanState.packScanState maxReg ScanState.InUse ( s3)))})
+          Applicative.pure (Monad.is_applicative mDict)
+            (ScanState.packScanState maxReg ScanState.InUse ( s3))})
         (reduceBlocks maxReg mDict binfo oinfo ((:) b bs) loops varUses
           liveSets 0))
       (Loops.computeVarReferences maxReg mDict binfo oinfo ((:) b bs) loops)}
diff --git a/LinearScan/Context.hs b/LinearScan/Context.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/Context.hs
@@ -0,0 +1,55 @@
+
+
+module LinearScan.Context 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
+
+
+type Context errType i o a =
+  ([] errType) -> i -> Prelude.Either ([] errType) ((,) a o)
+
+iask :: Context a1 a2 a2 ([] a1)
+iask e i =
+  Prelude.Right ((,) e i)
+
+context :: a1 -> (Context a1 a2 a3 a4) -> Context a1 a2 a3 a4
+context c x e =
+  x ((:) c e)
+
+iput :: a3 -> Context a1 a2 a3 ()
+iput x x0 x1 =
+  Prelude.Right ((,) () x)
+
+imap :: (a4 -> a5) -> (Context a1 a2 a3 a4) -> Context a1 a2 a3 a5
+imap f x e st =
+  case x e st of {
+   Prelude.Left err -> Prelude.Left err;
+   Prelude.Right p ->
+    case p of {
+     (,) a st' -> Prelude.Right ((,) (f a) st')}}
+
+ipure :: a3 -> Context a1 a2 a2 a3
+ipure x x0 st =
+  Prelude.Right ((,) x st)
+
+ijoin :: (Context a1 a2 a3 (Context a1 a3 a4 a5)) -> Context a1 a2 a4 a5
+ijoin x e st =
+  case x e st of {
+   Prelude.Left err -> Prelude.Left err;
+   Prelude.Right p ->
+    case p of {
+     (,) y st' -> y e st'}}
+
+ibind :: (a5 -> Context a1 a3 a4 a6) -> (Context a1 a2 a3 a5) -> Context 
+         a1 a2 a4 a6
+ibind f x =
+  ijoin (imap f x)
+
diff --git a/LinearScan/Cursor.hs b/LinearScan/Cursor.hs
--- a/LinearScan/Cursor.hs
+++ b/LinearScan/Cursor.hs
@@ -38,8 +38,8 @@
 withCursor :: Prelude.Int -> ScanState.ScanStateDesc ->
               (ScanState.ScanStateDesc -> () -> Morph.SState () a1 a2) ->
               Morph.SState () a1 a2
-withCursor maxReg pre f x =
+withCursor maxReg pre f e x =
   case x of {
    Morph.Build_SSInfo thisDesc _ ->
-    f thisDesc __ (Morph.Build_SSInfo thisDesc __)}
+    f thisDesc __ e (Morph.Build_SSInfo thisDesc __)}
 
diff --git a/LinearScan/Functor.hs b/LinearScan/Functor.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/Functor.hs
@@ -0,0 +1,54 @@
+{-# OPTIONS_GHC -cpp -XMagicHash #-}
+{- For Hugs, use the option -F"cpp -P -traditional" -}
+
+module LinearScan.Functor 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
+
+
+
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base as GHC.Base
+import qualified GHC.Prim as GHC.Prim
+#else
+-- HUGS
+import qualified LinearScan.IOExts as IOExts
+#endif
+
+
+#ifdef __GLASGOW_HASKELL__
+--unsafeCoerce :: a -> b
+unsafeCoerce = GHC.Base.unsafeCoerce#
+#else
+-- HUGS
+--unsafeCoerce :: a -> b
+unsafeCoerce = IOExts.unsafeCoerce
+#endif
+
+
+#ifdef __GLASGOW_HASKELL__
+type Any = GHC.Prim.Any
+#else
+-- HUGS
+type Any = ()
+#endif
+
+__ :: any
+__ = Prelude.error "Logical or arity value used"
+
+type Functor f =
+  () -> () -> (Any -> Any) -> f -> f
+  -- singleton inductive, whose constructor was Build_Functor
+  
+fmap :: (Functor a1) -> (a2 -> a3) -> a1 -> a1
+fmap functor x x0 =
+  unsafeCoerce functor __ __ x x0
+
diff --git a/LinearScan/IState.hs b/LinearScan/IState.hs
deleted file mode 100644
--- a/LinearScan/IState.hs
+++ /dev/null
@@ -1,41 +0,0 @@
-
-
-module LinearScan.IState 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
-
-
-type IState errType i o a = i -> Prelude.Either errType ((,) a o)
-
-iput :: a3 -> IState a1 a2 a3 ()
-iput x x0 =
-  Prelude.Right ((,) () x)
-
-imap :: (a4 -> a5) -> (IState a1 a2 a3 a4) -> IState a1 a2 a3 a5
-imap f x st =
-  case x st of {
-   Prelude.Left err -> Prelude.Left err;
-   Prelude.Right p ->
-    case p of {
-     (,) a st' -> Prelude.Right ((,) (f a) st')}}
-
-ipure :: a3 -> IState a1 a2 a2 a3
-ipure x st =
-  Prelude.Right ((,) x st)
-
-ijoin :: (IState a1 a2 a3 (IState a1 a3 a4 a5)) -> IState a1 a2 a4 a5
-ijoin x st =
-  case x st of {
-   Prelude.Left err -> Prelude.Left err;
-   Prelude.Right p ->
-    case p of {
-     (,) y st' -> y st'}}
-
diff --git a/LinearScan/IntMap.hs b/LinearScan/IntMap.hs
--- a/LinearScan/IntMap.hs
+++ b/LinearScan/IntMap.hs
@@ -13,7 +13,7 @@
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
-import qualified LinearScan.Lib as Lib
+import qualified LinearScan.List1 as List1
 import qualified LinearScan.Eqtype as Eqtype
 import qualified LinearScan.Seq as Seq
 import qualified LinearScan.Ssrbool as Ssrbool
@@ -60,7 +60,7 @@
 
 coq_IntMap_lookup :: Prelude.Int -> (IntMap a1) -> Prelude.Maybe a1
 coq_IntMap_lookup k m =
-  Lib.maybeLookup Ssrnat.nat_eqType (unsafeCoerce m) (unsafeCoerce k)
+  List1.maybeLookup Ssrnat.nat_eqType (unsafeCoerce m) (unsafeCoerce k)
 
 coq_IntMap_alter :: ((Prelude.Maybe a1) -> Prelude.Maybe a1) -> Prelude.Int
                     -> (IntMap a1) -> IntMap a1
@@ -146,97 +146,9 @@
 coq_IntMap_eqType a =
   unsafeCoerce (coq_IntMap_eqMixin a)
 
-type IntSet =
-  [] Prelude.Int
-  -- singleton inductive, whose constructor was getIntSet
-  
-emptyIntSet :: IntSet
-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)
-         (Ssrbool.mem (Seq.seq_predType Ssrnat.nat_eqType) (unsafeCoerce m)) of {
-   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
-    (Seq.undup Ssrnat.nat_eqType
-      ((Prelude.++) (unsafeCoerce m1) (unsafeCoerce m2)))
-
-coq_IntSet_difference :: IntSet -> IntSet -> IntSet
-coq_IntSet_difference m1 m2 =
-  Prelude.filter (\k ->
-    Prelude.not
-      (Ssrbool.in_mem (unsafeCoerce k)
-        (Ssrbool.mem (Seq.seq_predType Ssrnat.nat_eqType) (unsafeCoerce m2))))
-    m1
-
-coq_IntSet_foldl :: (a1 -> Prelude.Int -> a1) -> a1 -> IntSet -> a1
-coq_IntSet_foldl f z m =
-  Data.List.foldl' f z m
-
-coq_IntSet_forFold :: a1 -> IntSet -> (a1 -> Prelude.Int -> a1) -> a1
-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)
-    (unsafeCoerce s2)
-
-eqIntSetP :: Eqtype.Equality__Coq_axiom IntSet
-eqIntSetP _top_assumption_ =
-  let {
-   _evar_0_ = \s1 _top_assumption_0 ->
-    let {
-     _evar_0_ = \s2 ->
-      let {_evar_0_ = \_ -> let {_evar_0_ = Ssrbool.ReflectT} in  _evar_0_}
-      in
-      let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
-      case Eqtype.eqP (Seq.seq_eqType Ssrnat.nat_eqType) s1 s2 of {
-       Ssrbool.ReflectT -> _evar_0_ __;
-       Ssrbool.ReflectF -> _evar_0_0 __}}
-    in
-    unsafeCoerce _evar_0_ _top_assumption_0}
-  in
-  unsafeCoerce _evar_0_ _top_assumption_
-
-coq_IntSet_eqMixin :: Eqtype.Equality__Coq_mixin_of IntSet
-coq_IntSet_eqMixin =
-  Eqtype.Equality__Mixin eqIntSet eqIntSetP
-
-coq_IntSet_eqType :: Eqtype.Equality__Coq_type
-coq_IntSet_eqType =
-  unsafeCoerce coq_IntSet_eqMixin
-
 coq_IntMap_groupOn :: (a1 -> Prelude.Int) -> ([] a1) -> IntMap ([] a1)
 coq_IntMap_groupOn p l =
-  Lib.forFold emptyIntMap l (\acc x ->
+  List1.forFold emptyIntMap l (\acc x ->
     let {n = p x} in
     coq_IntMap_alter (\mxs ->
       case mxs of {
diff --git a/LinearScan/IntSet.hs b/LinearScan/IntSet.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/IntSet.hs
@@ -0,0 +1,131 @@
+{-# OPTIONS_GHC -cpp -XMagicHash #-}
+{- For Hugs, use the option -F"cpp -P -traditional" -}
+
+module LinearScan.IntSet 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.Eqtype as Eqtype
+import qualified LinearScan.Seq as Seq
+import qualified LinearScan.Ssrbool as Ssrbool
+import qualified LinearScan.Ssrnat as Ssrnat
+
+
+
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base as GHC.Base
+import qualified GHC.Prim as GHC.Prim
+#else
+-- HUGS
+import qualified LinearScan.IOExts as IOExts
+#endif
+
+
+#ifdef __GLASGOW_HASKELL__
+--unsafeCoerce :: a -> b
+unsafeCoerce = GHC.Base.unsafeCoerce#
+#else
+-- HUGS
+--unsafeCoerce :: a -> b
+unsafeCoerce = IOExts.unsafeCoerce
+#endif
+
+__ :: any
+__ = Prelude.error "Logical or arity value used"
+
+type IntSet =
+  [] Prelude.Int
+  -- singleton inductive, whose constructor was getIntSet
+  
+emptyIntSet :: IntSet
+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)
+         (Ssrbool.mem (Seq.seq_predType Ssrnat.nat_eqType) (unsafeCoerce m)) of {
+   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
+    (Seq.undup Ssrnat.nat_eqType
+      ((Prelude.++) (unsafeCoerce m1) (unsafeCoerce m2)))
+
+coq_IntSet_difference :: IntSet -> IntSet -> IntSet
+coq_IntSet_difference m1 m2 =
+  Prelude.filter (\k ->
+    Prelude.not
+      (Ssrbool.in_mem (unsafeCoerce k)
+        (Ssrbool.mem (Seq.seq_predType Ssrnat.nat_eqType) (unsafeCoerce m2))))
+    m1
+
+coq_IntSet_foldl :: (a1 -> Prelude.Int -> a1) -> a1 -> IntSet -> a1
+coq_IntSet_foldl f z m =
+  Data.List.foldl' f z m
+
+coq_IntSet_forFold :: a1 -> IntSet -> (a1 -> Prelude.Int -> a1) -> a1
+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)
+    (unsafeCoerce s2)
+
+eqIntSetP :: Eqtype.Equality__Coq_axiom IntSet
+eqIntSetP _top_assumption_ =
+  let {
+   _evar_0_ = \s1 _top_assumption_0 ->
+    let {
+     _evar_0_ = \s2 ->
+      let {_evar_0_ = \_ -> let {_evar_0_ = Ssrbool.ReflectT} in  _evar_0_}
+      in
+      let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
+      case Eqtype.eqP (Seq.seq_eqType Ssrnat.nat_eqType) s1 s2 of {
+       Ssrbool.ReflectT -> _evar_0_ __;
+       Ssrbool.ReflectF -> _evar_0_0 __}}
+    in
+    unsafeCoerce _evar_0_ _top_assumption_0}
+  in
+  unsafeCoerce _evar_0_ _top_assumption_
+
+coq_IntSet_eqMixin :: Eqtype.Equality__Coq_mixin_of IntSet
+coq_IntSet_eqMixin =
+  Eqtype.Equality__Mixin eqIntSet eqIntSetP
+
+coq_IntSet_eqType :: Eqtype.Equality__Coq_type
+coq_IntSet_eqType =
+  unsafeCoerce coq_IntSet_eqMixin
+
diff --git a/LinearScan/Interval.hs b/LinearScan/Interval.hs
--- a/LinearScan/Interval.hs
+++ b/LinearScan/Interval.hs
@@ -12,9 +12,10 @@
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
-import qualified LinearScan.Lib as Lib
+import qualified LinearScan.List1 as List1
 import qualified LinearScan.Logic as Logic
-import qualified LinearScan.NonEmpty0 as NonEmpty0
+import qualified LinearScan.NonEmpty as NonEmpty
+import qualified LinearScan.Prelude0 as Prelude0
 import qualified LinearScan.Range as Range
 import qualified LinearScan.Specif as Specif
 import qualified LinearScan.UsePos as UsePos
@@ -75,12 +76,12 @@
   Data.List.any (\x -> Data.List.any (f x) ( (rds j))) ( (rds i))
 
 intervalIntersectionPoint :: IntervalDesc -> IntervalDesc -> Prelude.Maybe
-                             Lib.Coq_oddnum
+                             Prelude0.Coq_oddnum
 intervalIntersectionPoint i j =
   Data.List.foldl' (\mx rd ->
-    Lib.option_choose mx
+    Prelude0.option_choose mx
       (Data.List.foldl' (\mx' rd' ->
-        Lib.option_choose mx (Range.rangeIntersectionPoint ( rd) ( rd')))
+        Prelude0.option_choose mx (Range.rangeIntersectionPoint ( rd) ( rd')))
         Prelude.Nothing (rds j))) Prelude.Nothing (rds i)
 
 findIntervalUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) ->
@@ -115,15 +116,15 @@
          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) (rds d) __ __ __}
+      NonEmpty.coq_NonEmpty_rec (\r _ _ _ -> _evar_0_ r) (\r rs iHrs _ _ _ ->
+        _evar_0_0 r rs iHrs) (rds d) __ __ __}
     in
      _evar_0_ __}
   in
    _evar_0_ __
 
 lookupUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) ->
-                Prelude.Maybe Lib.Coq_oddnum
+                Prelude.Maybe Prelude0.Coq_oddnum
 lookupUsePos d f =
   let {
    _evar_0_ = \_top_assumption_ ->
@@ -139,7 +140,8 @@
    Prelude.Just x -> _evar_0_ x;
    Prelude.Nothing -> _evar_0_0}
 
-nextUseAfter :: IntervalDesc -> Prelude.Int -> Prelude.Maybe Lib.Coq_oddnum
+nextUseAfter :: IntervalDesc -> Prelude.Int -> Prelude.Maybe
+                Prelude0.Coq_oddnum
 nextUseAfter d pos =
   case lookupUsePos d (\u ->
          (Prelude.<=) ((Prelude.succ) pos) (UsePos.uloc u)) of {
@@ -160,7 +162,7 @@
        (\x ->
        rangeFirstUsePos ( x))
        (\x xs0 ->
-       Lib.option_choose (rangeFirstUsePos ( x)) (go xs0))
+       Prelude0.option_choose (rangeFirstUsePos ( x)) (go xs0))
        xs}
   in go (rds d)
 
@@ -170,13 +172,14 @@
    go xs =
      (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)
        (\x ->
-       Lib.olast (Range.ups ( x)))
+       List1.olast (Range.ups ( x)))
        (\x xs0 ->
-       Lib.option_choose (go xs0) (Lib.olast (Range.ups ( x))))
+       Prelude0.option_choose (go xs0) (List1.olast (Range.ups ( x))))
        xs}
   in go (rds d)
 
-afterLifetimeHole :: IntervalDesc -> Lib.Coq_oddnum -> Lib.Coq_oddnum
+afterLifetimeHole :: IntervalDesc -> Prelude0.Coq_oddnum ->
+                     Prelude0.Coq_oddnum
 afterLifetimeHole d pos =
   let {
    f = \x k ->
@@ -194,7 +197,7 @@
        xs}
   in go (rds d)
 
-firstUseReqReg :: IntervalDesc -> Prelude.Maybe Lib.Coq_oddnum
+firstUseReqReg :: IntervalDesc -> Prelude.Maybe Prelude0.Coq_oddnum
 firstUseReqReg d =
   lookupUsePos d UsePos.regReq
 
@@ -324,7 +327,7 @@
      [] -> _evar_0_;
      (:) x x0 -> _evar_0_0 x x0}}
   in
-  case Lib.span (\rd ->
+  case List1.span (\rd ->
          (Prelude.<=) ((Prelude.succ) (Range.rend ( rd))) before) ( (rds d)) of {
    (,) x x0 -> _evar_0_ x x0 __}
 
@@ -391,16 +394,16 @@
           (Prelude.flip (Prelude.$)) __ (\_ -> (,)
             (packInterval (Build_IntervalDesc (ivar (getIntervalDesc d))
               (Range.rbeg
-                ( (Prelude.head (NonEmpty0.coq_NE_from_list r1 rs1))))
+                ( (Prelude.head (NonEmpty.coq_NE_from_list r1 rs1))))
               (Range.rend
-                ( (Prelude.last (NonEmpty0.coq_NE_from_list r1 rs1))))
-              (NonEmpty0.coq_NE_from_list r1 rs1)))
+                ( (Prelude.last (NonEmpty.coq_NE_from_list r1 rs1))))
+              (NonEmpty.coq_NE_from_list r1 rs1)))
             (packInterval (Build_IntervalDesc (ivar (getIntervalDesc d))
               (Range.rbeg
-                ( (Prelude.head (NonEmpty0.coq_NE_from_list r2 rs2))))
+                ( (Prelude.head (NonEmpty.coq_NE_from_list r2 rs2))))
               (Range.rend
-                ( (Prelude.last (NonEmpty0.coq_NE_from_list r2 rs2))))
-              (NonEmpty0.coq_NE_from_list r2 rs2)))))}
+                ( (Prelude.last (NonEmpty.coq_NE_from_list r2 rs2))))
+              (NonEmpty.coq_NE_from_list r2 rs2)))))}
       in
       case _top_assumption_1 of {
        [] -> _evar_0_0 __ __;
diff --git a/LinearScan/Iso.hs b/LinearScan/Iso.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/Iso.hs
@@ -0,0 +1,23 @@
+
+
+module LinearScan.Iso 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
+
+
+data Isomorphism a b =
+   Build_Isomorphism (a -> b) (b -> a)
+
+iso_to :: (Isomorphism a1 a2) -> a1 -> a2
+iso_to isomorphism =
+  case isomorphism of {
+   Build_Isomorphism iso_to0 iso_from -> iso_to0}
+
diff --git a/LinearScan/Lens.hs b/LinearScan/Lens.hs
--- a/LinearScan/Lens.hs
+++ b/LinearScan/Lens.hs
@@ -13,7 +13,7 @@
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
-import qualified LinearScan.Monad as Monad
+import qualified LinearScan.Functor as Functor
 
 
 
@@ -48,17 +48,17 @@
 
 type Identity a = a
 
-coq_Identity_Functor :: Monad.Functor (Identity Any)
+coq_Identity_Functor :: Functor.Functor (Identity Any)
 coq_Identity_Functor _ _ x =
   x
 
 type Const c a = c
 
-coq_Const_Functor :: Monad.Functor (Const a1 Any)
+coq_Const_Functor :: Functor.Functor (Const a1 Any)
 coq_Const_Functor _ _ x x0 =
   x0
 
-type Lens s t a b = () -> (Monad.Functor Any) -> (a -> Any) -> s -> Any
+type Lens s t a b = () -> (Functor.Functor Any) -> (a -> Any) -> s -> Any
 
 type Lens' s a = Lens s s a a
 
diff --git a/LinearScan/Lib.hs b/LinearScan/Lib.hs
--- a/LinearScan/Lib.hs
+++ b/LinearScan/Lib.hs
@@ -19,99 +19,6 @@
 __ :: any
 __ = Prelude.error "Logical or arity value used"
 
-option_map :: (a1 -> a2) -> (Prelude.Maybe a1) -> Prelude.Maybe a2
-option_map f x =
-  case x of {
-   Prelude.Just x0 -> Prelude.Just (f x0);
-   Prelude.Nothing -> Prelude.Nothing}
-
-option_choose :: (Prelude.Maybe a1) -> (Prelude.Maybe a1) -> Prelude.Maybe a1
-option_choose x y =
-  case x of {
-   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
-maybeLookup a v x =
-  case v of {
-   [] -> Prelude.Nothing;
-   (:) p xs ->
-    case p of {
-     (,) k v0 ->
-      case Eqtype.eq_op a k x of {
-       Prelude.True -> Prelude.Just v0;
-       Prelude.False -> maybeLookup a xs x}}}
-
-lebf :: (a1 -> Prelude.Int) -> a1 -> a1 -> Prelude.Bool
-lebf f n m =
-  (Prelude.<=) (f n) (f m)
-
-type Coq_oddnum = Prelude.Int
-
-odd1 :: Prelude.Int
-odd1 =
-  (Prelude.succ) 0
-
-forFold :: a2 -> ([] a1) -> (a2 -> a1 -> a2) -> a2
-forFold b v f =
-  Data.List.foldl' f b v
-
-forFoldr :: a2 -> ([] a1) -> (a1 -> a2 -> a2) -> a2
-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 {
-   [] -> (,) [] [];
-   (:) x xs ->
-    case p x of {
-     Prelude.True ->
-      case span p xs of {
-       (,) ys zs -> (,) ((:) x ys) zs};
-     Prelude.False -> (,) [] l}}
-
-partition :: (a1 -> Prelude.Bool) -> ([] a1) -> (,) ([] a1) ([] a1)
-partition p =
-  Prelude.foldr (\x acc ->
-    case p x of {
-     Prelude.True -> (,) ((:) x (Prelude.fst acc)) (Prelude.snd acc);
-     Prelude.False -> (,) (Prelude.fst acc) ((:) x (Prelude.snd acc))}) ((,)
-    [] [])
-
-insert :: (a1 -> a1 -> Prelude.Bool) -> a1 -> ([] a1) -> [] a1
-insert p z l =
-  case l of {
-   [] -> (:) z [];
-   (:) x xs ->
-    case p x z of {
-     Prelude.True -> (:) x (insert p z xs);
-     Prelude.False -> (:) z ((:) x xs)}}
-
-sortBy :: (a1 -> a1 -> Prelude.Bool) -> ([] a1) -> [] a1
-sortBy p l =
-  case l of {
-   [] -> [];
-   (:) x xs -> insert p x (sortBy p xs)}
-
 dep_foldl_inv :: (a1 -> Eqtype.Equality__Coq_type) -> a1 -> ([]
                  Eqtype.Equality__Coq_sort) -> Prelude.Int -> (a1 -> []
                  Eqtype.Equality__Coq_sort) -> (a1 -> a1 -> () ->
diff --git a/LinearScan/List1.hs b/LinearScan/List1.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/List1.hs
@@ -0,0 +1,97 @@
+
+
+module LinearScan.List1 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.Eqtype as Eqtype
+
+
+__ :: any
+__ = Prelude.error "Logical or arity value used"
+
+concat :: ([] ([] a1)) -> [] a1
+concat l =
+  case l of {
+   [] -> [];
+   (:) x xs -> (Prelude.++) x (concat xs)}
+
+maybeLookup :: Eqtype.Equality__Coq_type -> ([]
+               ((,) Eqtype.Equality__Coq_sort a1)) ->
+               Eqtype.Equality__Coq_sort -> Prelude.Maybe a1
+maybeLookup a v x =
+  case v of {
+   [] -> Prelude.Nothing;
+   (:) p xs ->
+    case p of {
+     (,) k v0 ->
+      case Eqtype.eq_op a k x of {
+       Prelude.True -> Prelude.Just v0;
+       Prelude.False -> maybeLookup a xs x}}}
+
+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
+
+forFold :: a2 -> ([] a1) -> (a2 -> a1 -> a2) -> a2
+forFold b v f =
+  Data.List.foldl' f b v
+
+forFoldr :: a2 -> ([] a1) -> (a1 -> a2 -> a2) -> a2
+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 {
+   [] -> (,) [] [];
+   (:) x xs ->
+    case p x of {
+     Prelude.True ->
+      case span p xs of {
+       (,) ys zs -> (,) ((:) x ys) zs};
+     Prelude.False -> (,) [] l}}
+
+partition :: (a1 -> Prelude.Bool) -> ([] a1) -> (,) ([] a1) ([] a1)
+partition p =
+  Prelude.foldr (\x acc ->
+    case p x of {
+     Prelude.True -> (,) ((:) x (Prelude.fst acc)) (Prelude.snd acc);
+     Prelude.False -> (,) (Prelude.fst acc) ((:) x (Prelude.snd acc))}) ((,)
+    [] [])
+
+insert :: (a1 -> a1 -> Prelude.Bool) -> a1 -> ([] a1) -> [] a1
+insert p z l =
+  case l of {
+   [] -> (:) z [];
+   (:) x xs ->
+    case p x z of {
+     Prelude.True -> (:) x (insert p z xs);
+     Prelude.False -> (:) z ((:) x xs)}}
+
+sortBy :: (a1 -> a1 -> Prelude.Bool) -> ([] a1) -> [] a1
+sortBy p l =
+  case l of {
+   [] -> [];
+   (:) x xs -> insert p x (sortBy p xs)}
+
diff --git a/LinearScan/LiveSets.hs b/LinearScan/LiveSets.hs
--- a/LinearScan/LiveSets.hs
+++ b/LinearScan/LiveSets.hs
@@ -13,9 +13,13 @@
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
+import qualified LinearScan.Applicative as Applicative
 import qualified LinearScan.Blocks as Blocks
+import qualified LinearScan.Functor as Functor
 import qualified LinearScan.IntMap as IntMap
-import qualified LinearScan.Lib as Lib
+import qualified LinearScan.IntSet as IntSet
+import qualified LinearScan.Iso as Iso
+import qualified LinearScan.List1 as List1
 import qualified LinearScan.Monad as Monad
 import qualified LinearScan.UsePos as UsePos
 import qualified LinearScan.Yoneda as Yoneda
@@ -47,28 +51,28 @@
 __ = Prelude.error "Logical or arity value used"
 
 data BlockLiveSets =
-   Build_BlockLiveSets IntMap.IntSet IntMap.IntSet IntMap.IntSet IntMap.IntSet 
+   Build_BlockLiveSets IntSet.IntSet IntSet.IntSet IntSet.IntSet IntSet.IntSet 
  Blocks.OpId Blocks.OpId
 
-blockLiveGen :: BlockLiveSets -> IntMap.IntSet
+blockLiveGen :: BlockLiveSets -> IntSet.IntSet
 blockLiveGen b =
   case b of {
    Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
     blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveGen0}
 
-blockLiveKill :: BlockLiveSets -> IntMap.IntSet
+blockLiveKill :: BlockLiveSets -> IntSet.IntSet
 blockLiveKill b =
   case b of {
    Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
     blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveKill0}
 
-blockLiveIn :: BlockLiveSets -> IntMap.IntSet
+blockLiveIn :: BlockLiveSets -> IntSet.IntSet
 blockLiveIn b =
   case b of {
    Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
     blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveIn0}
 
-blockLiveOut :: BlockLiveSets -> IntMap.IntSet
+blockLiveOut :: BlockLiveSets -> IntSet.IntSet
 blockLiveOut b =
   case b of {
    Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0
@@ -93,16 +97,16 @@
     case s2 of {
      Build_BlockLiveSets lg2 lk2 li2 lo2 fi2 la2 ->
       (Prelude.&&)
-        (Eqtype.eq_op IntMap.coq_IntSet_eqType (unsafeCoerce lg1)
+        (Eqtype.eq_op IntSet.coq_IntSet_eqType (unsafeCoerce lg1)
           (unsafeCoerce lg2))
         ((Prelude.&&)
-          (Eqtype.eq_op IntMap.coq_IntSet_eqType (unsafeCoerce lk1)
+          (Eqtype.eq_op IntSet.coq_IntSet_eqType (unsafeCoerce lk1)
             (unsafeCoerce lk2))
           ((Prelude.&&)
-            (Eqtype.eq_op IntMap.coq_IntSet_eqType (unsafeCoerce li1)
+            (Eqtype.eq_op IntSet.coq_IntSet_eqType (unsafeCoerce li1)
               (unsafeCoerce li2))
             ((Prelude.&&)
-              (Eqtype.eq_op IntMap.coq_IntSet_eqType (unsafeCoerce lo1)
+              (Eqtype.eq_op IntSet.coq_IntSet_eqType (unsafeCoerce lo1)
                 (unsafeCoerce lo2))
               ((Prelude.&&)
                 (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fi1)
@@ -175,7 +179,7 @@
                                                   Ssrbool.ReflectF}
                                                 in
                                                 case Eqtype.eqP
-                                                       IntMap.coq_IntSet_eqType
+                                                       IntSet.coq_IntSet_eqType
                                                        lo1 lo2 of {
                                                  Ssrbool.ReflectT ->
                                                   _evar_0_ __;
@@ -185,7 +189,7 @@
                                      _evar_0_}
                                   in
                                   let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
-                                  case Eqtype.eqP IntMap.coq_IntSet_eqType
+                                  case Eqtype.eqP IntSet.coq_IntSet_eqType
                                          li1 li2 of {
                                    Ssrbool.ReflectT -> _evar_0_ __;
                                    Ssrbool.ReflectF -> _evar_0_0 __}}
@@ -193,14 +197,14 @@
                        _evar_0_}
                     in
                     let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
-                    case Eqtype.eqP IntMap.coq_IntSet_eqType lk1 lk2 of {
+                    case Eqtype.eqP IntSet.coq_IntSet_eqType lk1 lk2 of {
                      Ssrbool.ReflectT -> _evar_0_ __;
                      Ssrbool.ReflectF -> _evar_0_0 __}}
         in
          _evar_0_}
       in
       let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
-      case Eqtype.eqP IntMap.coq_IntSet_eqType lg1 lg2 of {
+      case Eqtype.eqP IntSet.coq_IntSet_eqType lg1 lg2 of {
        Ssrbool.ReflectT -> _evar_0_ __;
        Ssrbool.ReflectF -> _evar_0_0 __}}
     in
@@ -224,9 +228,10 @@
                         a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([]
                         a1) -> a5
 computeLocalLiveSets maxReg mDict binfo oinfo blocks =
-  Yoneda.iso_to
-    (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict)))
-    (Monad.fmap (unsafeCoerce Yoneda.coq_Yoneda_Functor) Prelude.snd
+  Iso.iso_to
+    (Yoneda.coq_Yoneda_lemma
+      (Applicative.is_functor (Monad.is_applicative mDict)))
+    (Functor.fmap (unsafeCoerce Yoneda.coq_Yoneda_Functor) Prelude.snd
       (Monad.forFoldM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) ((,)
         ((Prelude.succ) 0) IntMap.emptyIntMap) blocks (\acc b ->
         case acc of {
@@ -236,35 +241,35 @@
             case p of {
              (,) opsb opsm ->
               let {
-               liveSet = Build_BlockLiveSets IntMap.emptyIntSet
-                IntMap.emptyIntSet IntMap.emptyIntSet IntMap.emptyIntSet
+               liveSet = Build_BlockLiveSets IntSet.emptyIntSet
+                IntSet.emptyIntSet IntSet.emptyIntSet IntSet.emptyIntSet
                 ((Prelude.+) idx (Ssrnat.double (Data.List.length opsb)))
                 idx}
               in
-              case Lib.forFold ((,) idx liveSet)
+              case List1.forFold ((,) idx liveSet)
                      ((Prelude.++) opsb ((Prelude.++) opsm opse)) (\acc0 o ->
                      case acc0 of {
                       (,) lastIdx liveSet1 -> (,) ((Prelude.succ)
                        ((Prelude.succ) lastIdx))
-                       (case Lib.partition (\v ->
+                       (case List1.partition (\v ->
                                Eqtype.eq_op UsePos.coq_VarKind_eqType
                                  (unsafeCoerce (Blocks.varKind maxReg v))
                                  (unsafeCoerce UsePos.Input))
                                (Blocks.opRefs maxReg mDict oinfo o) of {
                          (,) inputs others ->
                           let {
-                           liveSet2 = Lib.forFold liveSet1 inputs
+                           liveSet2 = List1.forFold liveSet1 inputs
                                         (\liveSet2 v ->
                                         case Blocks.varId maxReg v of {
                                          Prelude.Left p0 -> liveSet2;
                                          Prelude.Right vid ->
                                           case Prelude.not
-                                                 (IntMap.coq_IntSet_member
+                                                 (IntSet.coq_IntSet_member
                                                    vid
                                                    (blockLiveKill liveSet2)) of {
                                            Prelude.True ->
                                             Build_BlockLiveSets
-                                            (IntMap.coq_IntSet_insert vid
+                                            (IntSet.coq_IntSet_insert vid
                                               (blockLiveGen liveSet2))
                                             (blockLiveKill liveSet2)
                                             (blockLiveIn liveSet2)
@@ -273,14 +278,14 @@
                                            Prelude.False -> liveSet2}})}
                           in
                           let {
-                           liveSet3 = Lib.forFold liveSet2 others
+                           liveSet3 = List1.forFold liveSet2 others
                                         (\liveSet3 v ->
                                         case Blocks.varId maxReg v of {
                                          Prelude.Left p0 -> liveSet3;
                                          Prelude.Right vid ->
                                           Build_BlockLiveSets
                                           (blockLiveGen liveSet3)
-                                          (IntMap.coq_IntSet_insert vid
+                                          (IntSet.coq_IntSet_insert vid
                                             (blockLiveKill liveSet3))
                                           (blockLiveIn liveSet3)
                                           (blockLiveOut liveSet3)
@@ -293,7 +298,7 @@
                (,) lastIdx' liveSet3 ->
                 Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict))
                   (\k ->
-                  Monad.pure
+                  Applicative.pure
                     (unsafeCoerce
                       (Yoneda.coq_Yoneda_Applicative
                         (Monad.is_applicative mDict))) ((,) lastIdx'
@@ -304,8 +309,9 @@
                          a2 a3 a4) -> ([] a1) -> (IntMap.IntMap
                          BlockLiveSets) -> a5
 computeGlobalLiveSets mDict binfo blocks liveSets =
-  Yoneda.iso_to
-    (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict)))
+  Iso.iso_to
+    (Yoneda.coq_Yoneda_lemma
+      (Applicative.is_functor (Monad.is_applicative mDict)))
     (Monad.forFoldrM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) liveSets
       blocks (\b liveSets1 ->
       Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\bid ->
@@ -313,29 +319,29 @@
          Prelude.Just liveSet ->
           Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\suxs ->
             let {
-             liveSet2 = Lib.forFold liveSet suxs (\liveSet2 s_bid ->
+             liveSet2 = List1.forFold liveSet suxs (\liveSet2 s_bid ->
                           case IntMap.coq_IntMap_lookup s_bid liveSets1 of {
                            Prelude.Just sux -> Build_BlockLiveSets
                             (blockLiveGen liveSet2) (blockLiveKill liveSet2)
                             (blockLiveIn liveSet2)
-                            (IntMap.coq_IntSet_union (blockLiveOut liveSet2)
+                            (IntSet.coq_IntSet_union (blockLiveOut liveSet2)
                               (blockLiveIn sux)) (blockFirstOpId liveSet2)
                             (blockLastOpId liveSet2);
                            Prelude.Nothing -> liveSet2})}
             in
-            Monad.pure
+            Applicative.pure
               (unsafeCoerce
                 (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))
               (IntMap.coq_IntMap_insert bid (Build_BlockLiveSets
                 (blockLiveGen liveSet2) (blockLiveKill liveSet2)
-                (IntMap.coq_IntSet_union
-                  (IntMap.coq_IntSet_difference (blockLiveOut liveSet2)
+                (IntSet.coq_IntSet_union
+                  (IntSet.coq_IntSet_difference (blockLiveOut liveSet2)
                     (blockLiveKill liveSet2)) (blockLiveGen liveSet2))
                 (blockLiveOut liveSet2) (blockFirstOpId liveSet2)
                 (blockLastOpId liveSet2)) liveSets1))
             (unsafeCoerce (\_ -> Blocks.blockSuccessors mDict binfo b));
          Prelude.Nothing ->
-          Monad.pure
+          Applicative.pure
             (unsafeCoerce
               (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))
             liveSets1}) (\_ -> Blocks.blockId mDict binfo b)))
@@ -348,13 +354,14 @@
    go n previous =
      (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
        (\_ ->
-       Monad.pure (Monad.is_applicative mDict) previous)
+       Applicative.pure (Monad.is_applicative mDict) previous)
        (\n0 ->
        Monad.bind mDict (\computed ->
          case Eqtype.eq_op
                 (IntMap.coq_IntMap_eqType coq_BlockLiveSets_eqType)
                 (unsafeCoerce previous) computed of {
-          Prelude.True -> Monad.pure (Monad.is_applicative mDict) computed;
+          Prelude.True ->
+           Applicative.pure (Monad.is_applicative mDict) computed;
           Prelude.False -> unsafeCoerce go n0 computed})
          (computeGlobalLiveSets mDict binfo blocks previous))
        n}
diff --git a/LinearScan/Loops.hs b/LinearScan/Loops.hs
--- a/LinearScan/Loops.hs
+++ b/LinearScan/Loops.hs
@@ -13,10 +13,16 @@
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
+import qualified LinearScan.Applicative as Applicative
 import qualified LinearScan.Blocks as Blocks
+import qualified LinearScan.Functor as Functor
 import qualified LinearScan.IntMap as IntMap
-import qualified LinearScan.Lib as Lib
+import qualified LinearScan.IntSet as IntSet
+import qualified LinearScan.Iso as Iso
+import qualified LinearScan.List1 as List1
 import qualified LinearScan.Monad as Monad
+import qualified LinearScan.State as State
+import qualified LinearScan.State0 as State0
 import qualified LinearScan.Yoneda as Yoneda
 import qualified LinearScan.Eqtype as Eqtype
 import qualified LinearScan.Seq as Seq
@@ -44,19 +50,19 @@
 #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) 
+   Build_LoopState IntSet.IntSet IntSet.IntSet ([] Blocks.BlockId) IntSet.IntSet 
+ (IntMap.IntMap IntSet.IntSet) (IntMap.IntMap IntSet.IntSet) (IntMap.IntMap
+                                                             IntSet.IntSet) 
  (IntMap.IntMap ((,) Prelude.Int Prelude.Int))
 
-activeBlocks :: LoopState -> IntMap.IntSet
+activeBlocks :: LoopState -> IntSet.IntSet
 activeBlocks l =
   case l of {
    Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
     loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
     loopDepths0 -> activeBlocks0}
 
-visitedBlocks :: LoopState -> IntMap.IntSet
+visitedBlocks :: LoopState -> IntSet.IntSet
 visitedBlocks l =
   case l of {
    Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
@@ -70,28 +76,28 @@
     loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
     loopDepths0 -> loopHeaderBlocks0}
 
-loopEndBlocks :: LoopState -> IntMap.IntSet
+loopEndBlocks :: LoopState -> IntSet.IntSet
 loopEndBlocks l =
   case l of {
    Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
     loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
     loopDepths0 -> loopEndBlocks0}
 
-forwardBranches :: LoopState -> IntMap.IntMap IntMap.IntSet
+forwardBranches :: LoopState -> IntMap.IntMap IntSet.IntSet
 forwardBranches l =
   case l of {
    Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
     loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
     loopDepths0 -> forwardBranches0}
 
-backwardBranches :: LoopState -> IntMap.IntMap IntMap.IntSet
+backwardBranches :: LoopState -> IntMap.IntMap IntSet.IntSet
 backwardBranches l =
   case l of {
    Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
     loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0
     loopDepths0 -> backwardBranches0}
 
-loopIndices :: LoopState -> IntMap.IntMap IntMap.IntSet
+loopIndices :: LoopState -> IntMap.IntMap IntSet.IntSet
 loopIndices l =
   case l of {
    Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0
@@ -107,77 +113,77 @@
 
 emptyLoopState :: LoopState
 emptyLoopState =
-  Build_LoopState IntMap.emptyIntSet IntMap.emptyIntSet [] IntMap.emptyIntSet
+  Build_LoopState IntSet.emptyIntSet IntSet.emptyIntSet [] IntSet.emptyIntSet
     IntMap.emptyIntMap IntMap.emptyIntMap IntMap.emptyIntMap
     IntMap.emptyIntMap
 
-modifyActiveBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> Monad.State
+modifyActiveBlocks :: (IntSet.IntSet -> IntSet.IntSet) -> State.State
                       LoopState ()
 modifyActiveBlocks f =
-  Monad.modify (\st -> Build_LoopState (f (activeBlocks st))
+  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) -> Monad.State
+modifyVisitedBlocks :: (IntSet.IntSet -> IntSet.IntSet) -> State.State
                        LoopState ()
 modifyVisitedBlocks f =
-  Monad.modify (\st -> Build_LoopState (activeBlocks st)
+  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) ->
-                          Monad.State LoopState ()
+                          State.State LoopState ()
 modifyLoopHeaderBlocks f =
-  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
+  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) -> Monad.State
+modifyLoopEndBlocks :: (IntSet.IntSet -> IntSet.IntSet) -> State.State
                        LoopState ()
 modifyLoopEndBlocks f =
-  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
+  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) -> Monad.State LoopState ()
+modifyForwardBranches :: ((IntMap.IntMap IntSet.IntSet) -> IntMap.IntMap
+                         IntSet.IntSet) -> State.State LoopState ()
 modifyForwardBranches f =
-  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
+  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) -> Monad.State LoopState ()
+modifyBackwardBranches :: ((IntMap.IntMap IntSet.IntSet) -> IntMap.IntMap
+                          IntSet.IntSet) -> State.State LoopState ()
 modifyBackwardBranches f =
-  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
+  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) -> Monad.State LoopState ()
+setLoopIndices :: (IntMap.IntMap IntSet.IntSet) -> State.State LoopState ()
 setLoopIndices indices =
-  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
+  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)) -> Monad.State
+setLoopDepths :: (IntMap.IntMap ((,) Prelude.Int Prelude.Int)) -> State.State
                  LoopState ()
 setLoopDepths depths =
-  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)
+  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 :: Prelude.Int -> Prelude.Int -> (IntMap.IntMap IntSet.IntSet)
+                -> IntMap.IntMap IntSet.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
+     Prelude.Just acc -> Prelude.Just (IntSet.coq_IntSet_insert x acc);
+     Prelude.Nothing -> Prelude.Just (IntSet.coq_IntSet_singleton x)}) i
 
 pathToLoopHeader :: Blocks.BlockId -> Prelude.Int -> LoopState ->
-                    Prelude.Maybe IntMap.IntSet
+                    Prelude.Maybe IntSet.IntSet
 pathToLoopHeader blk header st =
   let {
    go = let {
@@ -186,24 +192,24 @@
              (\_ -> (,) visited
              Prelude.Nothing)
              (\n ->
-             let {visited' = IntMap.coq_IntSet_insert b visited} in
+             let {visited' = IntSet.coq_IntSet_insert b visited} in
              let {
               forwardPreds = case IntMap.coq_IntMap_lookup b
                                     (forwardBranches st) of {
                               Prelude.Just preds ->
-                               IntMap.coq_IntSet_toList preds;
+                               IntSet.coq_IntSet_toList preds;
                               Prelude.Nothing -> []}}
              in
              let {
               backwardPreds = case IntMap.coq_IntMap_lookup b
                                      (backwardBranches st) of {
                                Prelude.Just preds ->
-                                IntMap.coq_IntSet_toList preds;
+                                IntSet.coq_IntSet_toList preds;
                                Prelude.Nothing -> []}}
              in
              let {preds = (Prelude.++) forwardPreds backwardPreds} in
-             Lib.forFold ((,) visited' (Prelude.Just
-               (IntMap.coq_IntSet_singleton b))) (unsafeCoerce preds)
+             List1.forFold ((,) visited' (Prelude.Just
+               (IntSet.coq_IntSet_singleton b))) (unsafeCoerce preds)
                (\mxs pred ->
                case mxs of {
                 (,) vis o ->
@@ -212,45 +218,34 @@
                    case Eqtype.eq_op Ssrnat.nat_eqType pred
                           (unsafeCoerce header) of {
                     Prelude.True -> (,) vis (Prelude.Just
-                     (IntMap.coq_IntSet_union xs
-                       (IntMap.coq_IntSet_singleton (unsafeCoerce pred))));
+                     (IntSet.coq_IntSet_union xs
+                       (IntSet.coq_IntSet_singleton (unsafeCoerce pred))));
                     Prelude.False ->
-                     case IntMap.coq_IntSet_member (unsafeCoerce pred) vis of {
+                     case IntSet.coq_IntSet_member (unsafeCoerce pred) vis of {
                       Prelude.True -> (,) vis (Prelude.Just xs);
                       Prelude.False ->
                        case unsafeCoerce go n vis pred of {
                         (,) vis' o0 ->
                          case o0 of {
                           Prelude.Just ys -> (,) vis' (Prelude.Just
-                           (IntMap.coq_IntSet_union xs ys));
+                           (IntSet.coq_IntSet_union xs ys));
                           Prelude.Nothing -> (,) vis Prelude.Nothing}}}};
                   Prelude.Nothing -> mxs}}))
              fuel}
         in go}
   in
   Prelude.snd
-    (go (IntMap.coq_IntSet_size (visitedBlocks st)) IntMap.emptyIntSet blk)
-
-liftStateT :: (Monad.Monad a1) -> (Monad.State a2 a3) -> Monad.StateT 
-              a2 a1 a3
-liftStateT h x =
-  Monad.bind (Monad.coq_StateT_Monad h) (\st ->
-    case x st of {
-     (,) a st' ->
-      Monad.bind (Monad.coq_StateT_Monad h) (\x0 ->
-        Monad.pure (Monad.coq_StateT_Applicative h) a)
-        (Monad.putT (Monad.is_applicative h) st')})
-    (Monad.getT (Monad.is_applicative h))
+    (go (IntSet.coq_IntSet_size (visitedBlocks st)) IntSet.emptyIntSet blk)
 
 computeLoopDepths :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 
-                     a4) -> (IntMap.IntMap a1) -> Monad.StateT LoopState 
+                     a4) -> (IntMap.IntMap a1) -> State0.StateT LoopState 
                      a5 ()
 computeLoopDepths mDict binfo bs =
-  Monad.bind (Monad.coq_StateT_Monad mDict) (\st ->
-    Monad.bind (Monad.coq_StateT_Monad mDict) (\m ->
+  Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
+    Monad.bind (State0.coq_StateT_Monad mDict) (\m ->
       let {
        f = \acc loopIndex refs ->
-        IntMap.coq_IntSet_forFold acc refs (\m' blk ->
+        IntSet.coq_IntSet_forFold acc refs (\m' blk ->
           let {
            f = \mx ->
             case mx of {
@@ -263,27 +258,27 @@
           in
           IntMap.coq_IntMap_alter f blk m')}
       in
-      liftStateT mDict
-        (Monad.bind (unsafeCoerce Monad.coq_State_Monad) (\x ->
+      State0.liftStateT mDict
+        (Monad.bind (unsafeCoerce State.coq_State_Monad) (\x ->
           setLoopDepths
             (IntMap.coq_IntMap_foldlWithKey f IntMap.emptyIntMap m))
           (setLoopIndices m)))
-      (Monad.lift mDict
-        (Yoneda.iso_to
+      (State0.lift mDict
+        (Iso.iso_to
           (Yoneda.coq_Yoneda_lemma
-            (Monad.is_functor (Monad.is_applicative mDict)))
+            (Applicative.is_functor (Monad.is_applicative mDict)))
           (Monad.forFoldM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict))
-            IntMap.emptyIntMap (IntMap.coq_IntSet_toList (loopEndBlocks st))
+            IntMap.emptyIntMap (IntSet.coq_IntSet_toList (loopEndBlocks st))
             (\m endBlock ->
             case IntMap.coq_IntMap_lookup endBlock bs of {
              Prelude.Just b ->
               Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict))
                 (\suxs ->
-                Monad.pure
+                Applicative.pure
                   (unsafeCoerce
                     (Yoneda.coq_Yoneda_Applicative
                       (Monad.is_applicative mDict)))
-                  (Lib.forFold m suxs (\m' sux ->
+                  (List1.forFold m suxs (\m' sux ->
                     let {headers = loopHeaderBlocks st} in
                     let {
                      loopIndex = Seq.find (\x ->
@@ -300,96 +295,97 @@
                       in
                       case mres of {
                        Prelude.Just path ->
-                        Lib.forFold m' (IntMap.coq_IntSet_toList path)
+                        List1.forFold m' (IntSet.coq_IntSet_toList path)
                           (\m'' blk -> addReference loopIndex blk m'');
                        Prelude.Nothing -> m'}}))) (\_ ->
                 Blocks.blockSuccessors mDict binfo b);
              Prelude.Nothing ->
-              Monad.pure
+              Applicative.pure
                 (unsafeCoerce
                   (Yoneda.coq_Yoneda_Applicative
                     (Monad.is_applicative mDict))) m})))))
-    (Monad.getT (Monad.is_applicative mDict))
+    (State0.getT (Monad.is_applicative mDict))
 
 computeVarReferences :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo
                         a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([]
                         a1) -> LoopState -> a5
 computeVarReferences maxReg mDict binfo oinfo bs st =
-  Yoneda.iso_to
-    (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict)))
+  Iso.iso_to
+    (Yoneda.coq_Yoneda_lemma
+      (Applicative.is_functor (Monad.is_applicative mDict)))
     (Monad.forFoldM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict))
       IntMap.emptyIntMap bs (\acc b ->
       Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\bid ->
         let {
          g = \acc1 loopIndex blks ->
-          case Prelude.not (IntMap.coq_IntSet_member bid blks) of {
+          case Prelude.not (IntSet.coq_IntSet_member bid blks) of {
            Prelude.True -> acc1;
            Prelude.False ->
             case Blocks.blockOps mDict binfo b of {
              (,) p zs ->
               case p of {
                (,) xs ys ->
-                Lib.forFold acc1 ((Prelude.++) xs ((Prelude.++) ys zs))
+                List1.forFold acc1 ((Prelude.++) xs ((Prelude.++) ys zs))
                   (\acc2 op ->
-                  Lib.forFold acc2 (Blocks.opRefs maxReg mDict oinfo op)
+                  List1.forFold acc2 (Blocks.opRefs maxReg mDict oinfo op)
                     (\acc3 v ->
                     case Blocks.varId maxReg v of {
                      Prelude.Left p0 -> acc3;
                      Prelude.Right vid -> addReference loopIndex vid acc3}))}}}}
         in
-        Monad.pure
+        Applicative.pure
           (unsafeCoerce
             (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))
           (IntMap.coq_IntMap_foldlWithKey g acc (loopIndices st))) (\_ ->
         Blocks.blockId mDict binfo b)))
 
 findLoopEnds :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) ->
-                (IntMap.IntMap a1) -> Monad.StateT LoopState a5 ()
+                (IntMap.IntMap a1) -> State0.StateT LoopState a5 ()
 findLoopEnds mDict binfo bs =
   let {
    go = let {
          go n b =
            (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
              (\_ ->
-             Monad.pure (Monad.coq_StateT_Applicative mDict) ())
+             Applicative.pure (State0.coq_StateT_Applicative mDict) ())
              (\n0 ->
-             Monad.bind (Monad.coq_StateT_Monad mDict) (\bid ->
-               Monad.bind (Monad.coq_StateT_Monad mDict) (\x ->
-                 Monad.bind (Monad.coq_StateT_Monad mDict) (\suxs ->
-                   Monad.bind (Monad.coq_StateT_Monad mDict) (\x0 ->
-                     liftStateT mDict
-                       (modifyActiveBlocks (IntMap.coq_IntSet_delete bid)))
-                     (Monad.forM_ (Monad.coq_StateT_Monad mDict) suxs
+             Monad.bind (State0.coq_StateT_Monad mDict) (\bid ->
+               Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
+                 Monad.bind (State0.coq_StateT_Monad mDict) (\suxs ->
+                   Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
+                     State0.liftStateT mDict
+                       (modifyActiveBlocks (IntSet.coq_IntSet_delete bid)))
+                     (Monad.forM_ (State0.coq_StateT_Monad mDict) suxs
                        (\sux ->
-                       Monad.bind (Monad.coq_StateT_Monad mDict) (\active ->
-                         Monad.bind (Monad.coq_StateT_Monad mDict) (\x0 ->
-                           Monad.bind (Monad.coq_StateT_Monad mDict)
+                       Monad.bind (State0.coq_StateT_Monad mDict) (\active ->
+                         Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
+                           Monad.bind (State0.coq_StateT_Monad mDict)
                              (\visited ->
-                             case IntMap.coq_IntSet_member sux visited of {
+                             case IntSet.coq_IntSet_member sux visited of {
                               Prelude.True ->
-                               Monad.pure
-                                 (Monad.coq_StateT_Applicative mDict) ();
+                               Applicative.pure
+                                 (State0.coq_StateT_Applicative mDict) ();
                               Prelude.False ->
                                case IntMap.coq_IntMap_lookup sux bs of {
                                 Prelude.Just x1 -> go n0 x1;
                                 Prelude.Nothing ->
-                                 Monad.pure
-                                   (Monad.coq_StateT_Applicative mDict) ()}})
-                             (Monad.getsT (Monad.is_applicative mDict)
+                                 Applicative.pure
+                                   (State0.coq_StateT_Applicative mDict) ()}})
+                             (State0.getsT (Monad.is_applicative mDict)
                                visitedBlocks))
-                           (liftStateT mDict
-                             (case IntMap.coq_IntSet_member sux active of {
+                           (State0.liftStateT mDict
+                             (case IntSet.coq_IntSet_member sux active of {
                                Prelude.True ->
                                 Monad.bind
-                                  (unsafeCoerce Monad.coq_State_Monad)
+                                  (unsafeCoerce State.coq_State_Monad)
                                   (\x0 ->
                                   Monad.bind
-                                    (unsafeCoerce Monad.coq_State_Monad)
+                                    (unsafeCoerce State.coq_State_Monad)
                                     (\x1 ->
                                     modifyBackwardBranches
                                       (addReference sux bid))
                                     (modifyLoopEndBlocks
-                                      (IntMap.coq_IntSet_insert bid)))
+                                      (IntSet.coq_IntSet_insert bid)))
                                   (modifyLoopHeaderBlocks (\l ->
                                     case Prelude.not
                                            (Ssrbool.in_mem (unsafeCoerce sux)
@@ -401,27 +397,28 @@
                                      Prelude.False -> l}));
                                Prelude.False ->
                                 modifyForwardBranches (addReference sux bid)})))
-                         (Monad.getsT (Monad.is_applicative mDict)
+                         (State0.getsT (Monad.is_applicative mDict)
                            activeBlocks))))
-                   (Monad.lift mDict
-                     (Yoneda.iso_to
+                   (State0.lift mDict
+                     (Iso.iso_to
                        (Yoneda.coq_Yoneda_lemma
-                         (Monad.is_functor (Monad.is_applicative mDict)))
-                       (\_ -> Blocks.blockSuccessors mDict binfo b))))
-                 (liftStateT mDict
-                   (Monad.bind (unsafeCoerce Monad.coq_State_Monad) (\x ->
-                     modifyActiveBlocks (IntMap.coq_IntSet_insert bid))
-                     (modifyVisitedBlocks (IntMap.coq_IntSet_insert bid)))))
-               (Monad.lift mDict
-                 (Yoneda.iso_to
+                         (Applicative.is_functor
+                           (Monad.is_applicative mDict))) (\_ ->
+                       Blocks.blockSuccessors mDict binfo b))))
+                 (State0.liftStateT mDict
+                   (Monad.bind (unsafeCoerce State.coq_State_Monad) (\x ->
+                     modifyActiveBlocks (IntSet.coq_IntSet_insert bid))
+                     (modifyVisitedBlocks (IntSet.coq_IntSet_insert bid)))))
+               (State0.lift mDict
+                 (Iso.iso_to
                    (Yoneda.coq_Yoneda_lemma
-                     (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->
-                   Blocks.blockId mDict binfo b))))
+                     (Applicative.is_functor (Monad.is_applicative mDict)))
+                   (\_ -> Blocks.blockId mDict binfo b))))
              n}
         in go}
   in
   case IntMap.coq_IntMap_toList bs of {
-   [] -> Monad.pure (Monad.coq_StateT_Applicative mDict) ();
+   [] -> Applicative.pure (State0.coq_StateT_Applicative mDict) ();
    (:) p l ->
     case p of {
      (,) n b -> go (IntMap.coq_IntMap_size bs) b}}
@@ -430,7 +427,8 @@
                      a4) -> ([] a1) -> a5
 computeBlockOrder mDict binfo blocks =
   case blocks of {
-   [] -> Monad.pure (Monad.is_applicative mDict) ((,) emptyLoopState []);
+   [] ->
+    Applicative.pure (Monad.is_applicative mDict) ((,) emptyLoopState []);
    (:) b bs ->
     Monad.bind mDict (\keys ->
       let {blockMap = IntMap.coq_IntMap_fromList keys} in
@@ -445,7 +443,7 @@
                  (,) y0 st1 ->
                   case blocks' of {
                    [] ->
-                    Monad.pure (Monad.is_applicative mDict) ((,)
+                    Applicative.pure (Monad.is_applicative mDict) ((,)
                       emptyLoopState []);
                    (:) b' bs' ->
                     Monad.bind mDict (\w ->
@@ -471,17 +469,17 @@
                                             (,) idx depth -> depth};
                                           Prelude.Nothing -> 0}}
                               in
-                              Monad.pure (Monad.is_applicative mDict)
+                              Applicative.pure (Monad.is_applicative mDict)
                                 ((Prelude.<=) ((Prelude.succ) y_depth)
                                   x_depth))
-                              (Yoneda.iso_to
+                              (Iso.iso_to
                                 (Yoneda.coq_Yoneda_lemma
-                                  (Monad.is_functor
+                                  (Applicative.is_functor
                                     (Monad.is_applicative mDict))) (\_ ->
                                 Blocks.blockId mDict binfo y2)))
-                            (Yoneda.iso_to
+                            (Iso.iso_to
                               (Yoneda.coq_Yoneda_lemma
-                                (Monad.is_functor
+                                (Applicative.is_functor
                                   (Monad.is_applicative mDict))) (\_ ->
                               Blocks.blockId mDict binfo x))}
                         in
@@ -490,20 +488,21 @@
                                go n branches work_list =
                                  (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
                                    (\_ ->
-                                   Monad.pure (Monad.is_applicative mDict) [])
+                                   Applicative.pure
+                                     (Monad.is_applicative mDict) [])
                                    (\n0 ->
                                    case work_list of {
                                     [] ->
-                                     Monad.pure (Monad.is_applicative mDict)
-                                       [];
+                                     Applicative.pure
+                                       (Monad.is_applicative mDict) [];
                                     (:) w0 ws ->
                                      Monad.bind mDict (\bid ->
                                        Monad.bind mDict (\suxs ->
                                          Monad.bind mDict (\x ->
                                            case x of {
                                             (,) branches' ws' ->
-                                             Monad.fmap
-                                               (Monad.is_functor
+                                             Functor.fmap
+                                               (Applicative.is_functor
                                                  (Monad.is_applicative mDict))
                                                (\x0 -> (:) w0 x0)
                                                (go n0 branches' ws')})
@@ -513,7 +512,7 @@
                                               (,) branches' ws' ->
                                                Monad.bind mDict
                                                  (\insertion ->
-                                                 Monad.pure
+                                                 Applicative.pure
                                                    (Monad.is_applicative
                                                      mDict)
                                                    (case IntMap.coq_IntMap_lookup
@@ -521,13 +520,13 @@
                                                      Prelude.Just incs -> (,)
                                                       (IntMap.coq_IntMap_insert
                                                         sux
-                                                        (IntMap.coq_IntSet_delete
+                                                        (IntSet.coq_IntSet_delete
                                                           bid incs)
                                                         branches')
                                                       (case Eqtype.eq_op
                                                               Ssrnat.nat_eqType
                                                               (unsafeCoerce
-                                                                (IntMap.coq_IntSet_size
+                                                                (IntSet.coq_IntSet_size
                                                                   incs))
                                                               (unsafeCoerce
                                                                 ((Prelude.succ)
@@ -543,19 +542,19 @@
                                                     Monad.insertM mDict
                                                       isHeavier s ws';
                                                    Prelude.Nothing ->
-                                                    Monad.pure
+                                                    Applicative.pure
                                                       (Monad.is_applicative
                                                         mDict) ws'})})))
-                                         (Yoneda.iso_to
+                                         (Iso.iso_to
                                            (Yoneda.coq_Yoneda_lemma
-                                             (Monad.is_functor
+                                             (Applicative.is_functor
                                                (Monad.is_applicative mDict)))
                                            (\_ ->
                                            Blocks.blockSuccessors mDict binfo
                                              w0)))
-                                       (Yoneda.iso_to
+                                       (Iso.iso_to
                                          (Yoneda.coq_Yoneda_lemma
-                                           (Monad.is_functor
+                                           (Applicative.is_functor
                                              (Monad.is_applicative mDict)))
                                          (\_ ->
                                          Blocks.blockId mDict binfo w0))})
@@ -563,26 +562,27 @@
                               in go}
                         in
                         Monad.bind mDict (\res ->
-                          Monad.pure (Monad.is_applicative mDict) ((,) st2
-                            res))
+                          Applicative.pure (Monad.is_applicative mDict) ((,)
+                            st2 res))
                           (go (Data.List.length blocks')
                             (forwardBranches st2) ((:) b' []))})
                       (computeLoopDepths mDict binfo blockMap st1)}})
                 (findLoopEnds mDict binfo blockMap' emptyLoopState))
               (Monad.mapM (Monad.is_applicative mDict) (\x ->
                 Monad.bind mDict (\bid ->
-                  Monad.pure (Monad.is_applicative mDict) ((,) bid x))
-                  (Yoneda.iso_to
+                  Applicative.pure (Monad.is_applicative mDict) ((,) bid x))
+                  (Iso.iso_to
                     (Yoneda.coq_Yoneda_lemma
-                      (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->
-                    Blocks.blockId mDict binfo x))) blocks'))
+                      (Applicative.is_functor (Monad.is_applicative mDict)))
+                    (\_ -> Blocks.blockId mDict binfo x))) blocks'))
             (Monad.forFoldrM mDict [] blocks (\b0 rest ->
               Monad.bind mDict (\suxs ->
                 case (Prelude.<=) (Data.List.length suxs) ((Prelude.succ) 0) of {
                  Prelude.True ->
-                  Monad.pure (Monad.is_applicative mDict) ((:) b0 rest);
+                  Applicative.pure (Monad.is_applicative mDict) ((:) b0 rest);
                  Prelude.False ->
-                  Monad.fmap (Monad.is_functor (Monad.is_applicative mDict))
+                  Functor.fmap
+                    (Applicative.is_functor (Monad.is_applicative mDict))
                     (\x ->
                     case x of {
                      (,) b' rest' -> (:) b' rest'})
@@ -593,47 +593,47 @@
                          fsz = case IntMap.coq_IntMap_lookup sux
                                       (forwardBranches st0) of {
                                 Prelude.Just fwds ->
-                                 IntMap.coq_IntSet_size fwds;
+                                 IntSet.coq_IntSet_size fwds;
                                 Prelude.Nothing -> 0}}
                         in
                         let {
                          bsz = case IntMap.coq_IntMap_lookup sux
                                       (backwardBranches st0) of {
                                 Prelude.Just bwds ->
-                                 IntMap.coq_IntSet_size bwds;
+                                 IntSet.coq_IntSet_size bwds;
                                 Prelude.Nothing -> 0}}
                         in
                         case (Prelude.<=) ((Prelude.+) fsz bsz)
                                ((Prelude.succ) 0) of {
                          Prelude.True ->
-                          Monad.pure (Monad.is_applicative mDict) ((,) b'
-                            rest');
+                          Applicative.pure (Monad.is_applicative mDict) ((,)
+                            b' rest');
                          Prelude.False ->
                           case IntMap.coq_IntMap_lookup sux blockMap of {
                            Prelude.Just sux' ->
                             Monad.bind mDict (\z0 ->
                               case z0 of {
                                (,) b'' sux'' ->
-                                Monad.pure (Monad.is_applicative mDict) ((,)
-                                  b'' ((:) sux'' rest'))})
-                              (Yoneda.iso_to
+                                Applicative.pure (Monad.is_applicative mDict)
+                                  ((,) b'' ((:) sux'' rest'))})
+                              (Iso.iso_to
                                 (Yoneda.coq_Yoneda_lemma
-                                  (Monad.is_functor
+                                  (Applicative.is_functor
                                     (Monad.is_applicative mDict))) (\_ ->
                                 Blocks.splitCriticalEdge mDict binfo b' sux'));
                            Prelude.Nothing ->
-                            Monad.pure (Monad.is_applicative mDict) ((,) b'
-                              rest')}}}))})
-                (Yoneda.iso_to
+                            Applicative.pure (Monad.is_applicative mDict)
+                              ((,) b' rest')}}}))})
+                (Iso.iso_to
                   (Yoneda.coq_Yoneda_lemma
-                    (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->
-                  Blocks.blockSuccessors mDict binfo b0))))})
+                    (Applicative.is_functor (Monad.is_applicative mDict)))
+                  (\_ -> Blocks.blockSuccessors mDict binfo b0))))})
         (findLoopEnds mDict binfo blockMap emptyLoopState))
       (Monad.mapM (Monad.is_applicative mDict) (\x ->
         Monad.bind mDict (\bid ->
-          Monad.pure (Monad.is_applicative mDict) ((,) bid x))
-          (Yoneda.iso_to
+          Applicative.pure (Monad.is_applicative mDict) ((,) bid x))
+          (Iso.iso_to
             (Yoneda.coq_Yoneda_lemma
-              (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->
+              (Applicative.is_functor (Monad.is_applicative mDict))) (\_ ->
             Blocks.blockId mDict binfo x))) blocks)}
 
diff --git a/LinearScan/Main.hs b/LinearScan/Main.hs
--- a/LinearScan/Main.hs
+++ b/LinearScan/Main.hs
@@ -13,18 +13,19 @@
 import qualified LinearScan.Utils
 
 import qualified LinearScan.Allocate as Allocate
+import qualified LinearScan.Applicative as Applicative
 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.Interval as Interval
-import qualified LinearScan.Lib as Lib
 import qualified LinearScan.LiveSets as LiveSets
 import qualified LinearScan.Loops as Loops
 import qualified LinearScan.Monad as Monad
-import qualified LinearScan.Morph as Morph
+import qualified LinearScan.Prelude0 as Prelude0
 import qualified LinearScan.Resolve as Resolve
 import qualified LinearScan.ScanState as ScanState
+import qualified LinearScan.Trace as Trace
 import qualified LinearScan.Ssrnat as Ssrnat
 
 
@@ -59,16 +60,14 @@
     (Prelude.map (\i -> (,) ( (Prelude.fst i)) ( (Prelude.snd i)))
       (ScanState.inactive maxReg sd))
     (Prelude.map (\i -> (,) ( (Prelude.fst i))
-      (Lib.option_map (\x ->  x) (Prelude.snd i)))
+      (Prelude0.option_map (\x ->  x) (Prelude.snd i)))
       (ScanState.handled maxReg sd))
 
 data Details blockType1 blockType2 =
-   Build_Details (Prelude.Maybe ((,) Morph.SSError FinalStage)) (IntMap.IntMap
-                                                                LiveSets.BlockLiveSets) 
- ([] blockType1) ([] blockType1) ([] blockType2) (Prelude.Maybe
-                                                 ScanStateDescSet) (Prelude.Maybe
-                                                                   ScanStateDescSet) 
- Loops.LoopState
+   Build_Details (Prelude.Maybe ((,) ([] Trace.SSTrace) FinalStage)) 
+ (IntMap.IntMap LiveSets.BlockLiveSets) ([] blockType1) ([] blockType1) 
+ ([] blockType2) (Prelude.Maybe ScanStateDescSet) (Prelude.Maybe
+                                                  ScanStateDescSet) Loops.LoopState
 
 linearScan :: (Monad.Monad a1) -> Prelude.Int -> (Blocks.BlockInfo a1 
               a2 a3 a4 a5) -> (Blocks.OpInfo a1 a4 a5) -> ([] a2) ->
@@ -79,44 +78,37 @@
      (,) loops blocks1 ->
       Monad.bind dict (\liveSets ->
         Monad.bind dict (\liveSets' ->
-          Monad.bind dict (\ints ->
-            case ints of {
-             Prelude.Left err ->
-              Monad.pure (Monad.is_applicative dict)
-                (k (Build_Details (Prelude.Just ((,) err
-                  BuildingIntervalsFailed)) liveSets' blocks blocks1 []
-                  Prelude.Nothing Prelude.Nothing loops));
-             Prelude.Right ssig ->
+          Monad.bind dict (\ssig ->
+            let {
+             opCount = (Prelude.succ) (Blocks.countOps dict binfo blocks1)}
+            in
+            case Allocate.walkIntervals maxReg ( ssig) opCount of {
+             Prelude.Left p ->
+              case p of {
+               (,) err ssig' ->
+                Applicative.pure (Monad.is_applicative dict)
+                  (k (Build_Details (Prelude.Just ((,) err
+                    AllocatingRegistersFailed)) liveSets' blocks blocks1 []
+                    (Prelude.Just (toScanStateDescSet maxReg ( ssig)))
+                    (Prelude.Just (toScanStateDescSet maxReg ( ssig')))
+                    loops))};
+             Prelude.Right ssig' ->
               let {
-               opCount = (Prelude.succ) (Blocks.countOps dict binfo blocks1)}
+               sd = Allocate.finalizeScanState maxReg ( ssig')
+                      (Ssrnat.double opCount)}
               in
-              case Allocate.walkIntervals maxReg ( ssig) opCount of {
-               Prelude.Left p ->
-                case p of {
-                 (,) err ssig' ->
-                  Monad.pure (Monad.is_applicative dict)
-                    (k (Build_Details (Prelude.Just ((,) err
-                      AllocatingRegistersFailed)) liveSets' blocks blocks1 []
-                      (Prelude.Just (toScanStateDescSet maxReg ( ssig)))
-                      (Prelude.Just (toScanStateDescSet maxReg ( ssig')))
-                      loops))};
-               Prelude.Right ssig' ->
-                let {
-                 sd = Allocate.finalizeScanState maxReg ( ssig')
-                        (Ssrnat.double opCount)}
-                in
-                let {allocs = Allocate.determineAllocations maxReg sd} in
-                Monad.bind dict (\mappings ->
-                  Monad.bind dict (\blocks2 ->
-                    Monad.pure (Monad.is_applicative dict)
-                      (k (Build_Details Prelude.Nothing liveSets' blocks
-                        blocks1 blocks2 (Prelude.Just
-                        (toScanStateDescSet maxReg ( ssig))) (Prelude.Just
-                        (toScanStateDescSet maxReg sd)) loops)))
-                    (Assign.assignRegNum maxReg dict binfo oinfo allocs
-                      liveSets' mappings blocks1))
-                  (Resolve.resolveDataFlow maxReg dict binfo allocs blocks1
-                    liveSets')}})
+              let {allocs = Allocate.determineAllocations maxReg sd} in
+              Monad.bind dict (\mappings ->
+                Monad.bind dict (\blocks2 ->
+                  Applicative.pure (Monad.is_applicative dict)
+                    (k (Build_Details Prelude.Nothing liveSets' blocks
+                      blocks1 blocks2 (Prelude.Just
+                      (toScanStateDescSet maxReg ( ssig))) (Prelude.Just
+                      (toScanStateDescSet maxReg sd)) loops)))
+                  (Assign.assignRegNum maxReg dict binfo oinfo allocs
+                    liveSets' mappings blocks1))
+                (Resolve.resolveDataFlow maxReg dict binfo allocs blocks1
+                  liveSets')})
             (Build.buildIntervals maxReg dict binfo oinfo blocks1 loops
               liveSets'))
           (LiveSets.computeGlobalLiveSetsRecursively dict binfo blocks1
diff --git a/LinearScan/Monad.hs b/LinearScan/Monad.hs
--- a/LinearScan/Monad.hs
+++ b/LinearScan/Monad.hs
@@ -1,6 +1,5 @@
-{-# OPTIONS_GHC -cpp -XMagicHash #-}
-{- For Hugs, use the option -F"cpp -P -traditional" -}
 
+
 module LinearScan.Monad where
 
 
@@ -13,81 +12,18 @@
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
-
-
-#ifdef __GLASGOW_HASKELL__
-import qualified GHC.Base as GHC.Base
-import qualified GHC.Prim as GHC.Prim
-#else
--- HUGS
-import qualified LinearScan.IOExts as IOExts
-#endif
-
-
-#ifdef __GLASGOW_HASKELL__
---unsafeCoerce :: a -> b
-unsafeCoerce = GHC.Base.unsafeCoerce#
-#else
--- HUGS
---unsafeCoerce :: a -> b
-unsafeCoerce = IOExts.unsafeCoerce
-#endif
+import qualified LinearScan.Applicative as Applicative
+import qualified LinearScan.Functor as Functor
+import qualified LinearScan.List1 as List1
 
 
-#ifdef __GLASGOW_HASKELL__
-type Any = GHC.Prim.Any
-#else
--- HUGS
-type Any = ()
-#endif
-
 __ :: any
 __ = Prelude.error "Logical or arity value used"
 
-type Functor f =
-  () -> () -> (Any -> Any) -> f -> f
-  -- singleton inductive, whose constructor was Build_Functor
-  
-fmap :: (Functor a1) -> (a2 -> a3) -> a1 -> a1
-fmap functor x x0 =
-  unsafeCoerce functor __ __ x x0
-
-apply :: (a1 -> a2) -> a1 -> a2
-apply f x =
-  f x
-
-first :: (a1 -> a2) -> ((,) a1 a3) -> (,) a2 a3
-first f x =
-  case x of {
-   (,) a z -> (,) (f a) z}
-
-curry :: (a1 -> a2 -> a3) -> ((,) a1 a2) -> a3
-curry f x =
-  case x of {
-   (,) a b -> f a b}
-
-data Applicative f =
-   Build_Applicative (Functor f) (() -> Any -> f) (() -> () -> f -> f -> f)
-
-is_functor :: (Applicative a1) -> Functor a1
-is_functor applicative =
-  case applicative of {
-   Build_Applicative is_functor0 pure0 ap0 -> is_functor0}
-
-pure :: (Applicative a1) -> a2 -> a1
-pure applicative x =
-  case applicative of {
-   Build_Applicative is_functor0 pure0 ap0 -> unsafeCoerce pure0 __ x}
-
-ap :: (Applicative a1) -> a1 -> a1 -> a1
-ap applicative x x0 =
-  case applicative of {
-   Build_Applicative is_functor0 pure0 ap0 -> ap0 __ __ x x0}
-
 data Monad m =
-   Build_Monad (Applicative m) (() -> m -> m)
+   Build_Monad (Applicative.Applicative m) (() -> m -> m)
 
-is_applicative :: (Monad a1) -> Applicative a1
+is_applicative :: (Monad a1) -> Applicative.Applicative a1
 is_applicative monad =
   case monad of {
    Build_Monad is_applicative0 join0 -> is_applicative0}
@@ -97,24 +33,21 @@
   case monad of {
    Build_Monad is_applicative0 join0 -> join0 __ x}
 
-liftA2 :: (Applicative a1) -> (a2 -> a3 -> a4) -> a1 -> a1 -> a1
-liftA2 h f x y =
-  ap h (fmap (is_functor h) f x) y
-
 bind :: (Monad a1) -> (a2 -> a1) -> a1 -> a1
 bind h f =
-  (Prelude..) (join h) (fmap (is_functor (is_applicative h)) f)
+  (Prelude..) (join h)
+    (Functor.fmap (Applicative.is_functor (is_applicative h)) f)
 
-mapM :: (Applicative a1) -> (a2 -> a1) -> ([] a2) -> a1
+mapM :: (Applicative.Applicative a1) -> (a2 -> a1) -> ([] a2) -> a1
 mapM h f l =
   case l of {
-   [] -> pure h [];
-   (:) x xs -> liftA2 h (\x0 x1 -> (:) x0 x1) (f x) (mapM h f xs)}
+   [] -> Applicative.pure h [];
+   (:) x xs -> Applicative.liftA2 h (\x0 x1 -> (:) x0 x1) (f x) (mapM h f xs)}
 
 mapM_ :: (Monad a1) -> (a2 -> a1) -> ([] a2) -> a1
 mapM_ h f l =
   case l of {
-   [] -> pure (is_applicative h) ();
+   [] -> Applicative.pure (is_applicative h) ();
    (:) x xs -> bind h (\x0 -> mapM_ h f xs) (f x)}
 
 forM_ :: (Monad a1) -> ([] a2) -> (a2 -> a1) -> a1
@@ -124,7 +57,7 @@
 foldM :: (Monad a1) -> (a2 -> a3 -> a1) -> a2 -> ([] a3) -> a1
 foldM h f s l =
   case l of {
-   [] -> pure (is_applicative h) s;
+   [] -> Applicative.pure (is_applicative h) s;
    (:) y ys -> bind h (\x -> foldM h f x ys) (f s y)}
 
 forFoldM :: (Monad a1) -> a2 -> ([] a3) -> (a2 -> a3 -> a1) -> a1
@@ -134,118 +67,27 @@
 foldrM :: (Monad a1) -> (a3 -> a2 -> a1) -> a2 -> ([] a3) -> a1
 foldrM h f s l =
   case l of {
-   [] -> pure (is_applicative h) s;
+   [] -> Applicative.pure (is_applicative h) s;
    (:) y ys -> bind h (f y) (foldrM h f s ys)}
 
 forFoldrM :: (Monad a1) -> a2 -> ([] a3) -> (a3 -> a2 -> a1) -> a1
 forFoldrM h s l f =
   foldrM h f s l
 
-concat :: ([] ([] a1)) -> [] a1
-concat l =
-  case l of {
-   [] -> [];
-   (:) x xs -> (Prelude.++) x (concat xs)}
-
-concatMapM :: (Applicative a1) -> (a2 -> a1) -> ([] a2) -> a1
+concatMapM :: (Applicative.Applicative a1) -> (a2 -> a1) -> ([] a2) -> a1
 concatMapM h f l =
-  fmap (is_functor h) concat (mapM h f l)
+  Functor.fmap (Applicative.is_functor h) List1.concat (mapM h f l)
 
 insertM :: (Monad a1) -> (a2 -> a2 -> a1) -> a2 -> ([] a2) -> a1
 insertM h p z l =
   case l of {
-   [] -> pure (is_applicative h) ((:) z []);
+   [] -> Applicative.pure (is_applicative h) ((:) z []);
    (:) x xs ->
     bind h (\b ->
       case b of {
        Prelude.True ->
-        fmap (is_functor (is_applicative h)) (\x0 -> (:) x x0)
-          (insertM h p z xs);
-       Prelude.False -> pure (is_applicative h) ((:) z ((:) x xs))}) 
-      (p x z)}
-
-type State s a = s -> (,) a s
-
-modify :: (a1 -> a1) -> State a1 ()
-modify f i =
-  (,) () (f i)
-
-coq_State_Functor :: Functor (State a1 Any)
-coq_State_Functor _ _ f x st =
-  let {filtered_var = x st} in
-  case filtered_var of {
-   (,) a st' -> (,) (f a) st'}
-
-coq_State_Applicative :: Applicative (State a1 Any)
-coq_State_Applicative =
-  Build_Applicative coq_State_Functor (\_ x st -> (,) x st) (\_ _ f x st ->
-    let {filtered_var = f st} in
-    case filtered_var of {
-     (,) f' st' ->
-      unsafeCoerce (\f'0 st'0 _ ->
-        let {filtered_var0 = x st'0} in
-        case filtered_var0 of {
-         (,) x' st'' -> (,) (f'0 x') st''}) f' st' __})
-
-coq_State_Monad :: Monad (State a1 Any)
-coq_State_Monad =
-  Build_Monad coq_State_Applicative (\_ x st ->
-    let {filtered_var = x st} in
-    case filtered_var of {
-     (,) y st' ->
-      unsafeCoerce (\y0 st'0 _ ->
-        let {filtered_var0 = y0 st'0} in
-        case filtered_var0 of {
-         (,) a st'' -> (,) a st''}) y st' __})
-
-type StateT s m a = s -> m
-
-getT :: (Applicative a1) -> StateT a2 a1 a2
-getT h i =
-  pure h ((,) i i)
-
-getsT :: (Applicative a1) -> (a2 -> a3) -> StateT a2 a1 a3
-getsT h f s =
-  pure h ((,) (f s) s)
-
-putT :: (Applicative a1) -> a2 -> StateT a2 a1 ()
-putT h x x0 =
-  pure h ((,) () x)
-
-modifyT :: (Applicative a1) -> (a2 -> a2) -> StateT a2 a1 ()
-modifyT h f i =
-  pure h ((,) () (f i))
-
-coq_StateT_Functor :: (Functor a2) -> Functor (StateT a1 a2 Any)
-coq_StateT_Functor h _ _ f x st =
-  fmap h (first f) (x st)
-
-coq_StateT_ap :: (Monad a1) -> (StateT a2 a1 (a3 -> a4)) -> (StateT a2 
-                 a1 a3) -> StateT a2 a1 a4
-coq_StateT_ap h f x st =
-  join h
-    (fmap (is_functor (is_applicative h)) (\z ->
-      case z of {
-       (,) f' st' -> fmap (is_functor (is_applicative h)) (first f') (x st')})
-      (f st))
-
-coq_StateT_Applicative :: (Monad a1) -> Applicative (StateT a2 a1 Any)
-coq_StateT_Applicative h =
-  Build_Applicative (coq_StateT_Functor (is_functor (is_applicative h)))
-    (\_ x st -> pure (is_applicative h) ((,) x st)) (\_ _ -> coq_StateT_ap h)
-
-coq_StateT_join :: (Monad a1) -> (StateT a2 a1 (StateT a2 a1 a3)) -> StateT
-                   a2 a1 a3
-coq_StateT_join h x =
-  (Prelude..)
-    ((Prelude..) (join h)
-      (fmap (is_functor (is_applicative h)) (curry apply))) x
-
-coq_StateT_Monad :: (Monad a1) -> Monad (StateT a2 a1 Any)
-coq_StateT_Monad h =
-  Build_Monad (coq_StateT_Applicative h) (\_ -> coq_StateT_join h)
-
-lift :: (Monad a1) -> a1 -> StateT a2 a1 a3
-lift h x st =
-  fmap (is_functor (is_applicative h)) (\z -> (,) z st) x
+        Functor.fmap (Applicative.is_functor (is_applicative h)) (\x0 -> (:)
+          x x0) (insertM h p z xs);
+       Prelude.False ->
+        Applicative.pure (is_applicative h) ((:) z ((:) x xs))}) (p x z)}
 
diff --git a/LinearScan/Morph.hs b/LinearScan/Morph.hs
--- a/LinearScan/Morph.hs
+++ b/LinearScan/Morph.hs
@@ -13,12 +13,12 @@
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
-import qualified LinearScan.IState as IState
+import qualified LinearScan.Context as Context
 import qualified LinearScan.Interval as Interval
-import qualified LinearScan.Lib as Lib
 import qualified LinearScan.Logic as Logic
 import qualified LinearScan.ScanState as ScanState
 import qualified LinearScan.Specif as Specif
+import qualified LinearScan.Trace as Trace
 import qualified LinearScan.Eqtype as Eqtype
 import qualified LinearScan.Fintype as Fintype
 import qualified LinearScan.Seq as Seq
@@ -50,48 +50,6 @@
 
 type PhysReg = Prelude.Int
 
-data SplitReason =
-   AvailableForPart Prelude.Int
- | IntersectsWithFixed Prelude.Int
- | SplittingActive Prelude.Int
- | SplittingInactive Prelude.Int
-
-data SplitPosition =
-   BeforePos Lib.Coq_oddnum SplitReason
- | EndOfLifetimeHole Lib.Coq_oddnum
-
-data SpillDetails =
-   SD_NewToHandled
- | SD_UnhandledToHandled Prelude.Int
- | SD_ActiveToHandled Prelude.Int Prelude.Int
- | SD_InactiveToHandled Prelude.Int Prelude.Int
-
-data SSError =
-   ECannotInsertUnhAtPos SpillDetails Prelude.Int
- | EIntervalBeginsBeforeUnhandled Prelude.Int
- | ENoValidSplitPositionUnh SplitPosition Prelude.Int
- | ENoValidSplitPosition SplitPosition Prelude.Int
- | ECannotSplitSingleton SplitPosition Prelude.Int
- | ERegisterAlreadyAssigned Prelude.Int
- | ERegisterAssignmentsOverlap Prelude.Int
- | EUnexpectedNoMoreUnhandled
- | ECannotSpillIfRegisterRequired Prelude.Int
- | EFuelExhausted
- | ENotYetImplemented Prelude.Int
-
-stbind :: (a4 -> IState.IState SSError a2 a3 a5) -> (IState.IState SSError 
-          a1 a2 a4) -> IState.IState SSError a1 a3 a5
-stbind f x =
-  IState.ijoin (IState.imap f x)
-
-error_ :: SSError -> IState.IState SSError a1 a2 a3
-error_ err x =
-  Prelude.Left err
-
-return_ :: a3 -> IState.IState a1 a2 a2 a3
-return_ =
-  IState.ipure
-
 data SSInfo p =
    Build_SSInfo ScanState.ScanStateDesc p
 
@@ -101,19 +59,24 @@
   case s of {
    Build_SSInfo thisDesc0 thisHolds -> thisDesc0}
 
-type SState p q a = IState.IState SSError (SSInfo p) (SSInfo q) a
+type SState p q a = Context.Context Trace.SSTrace (SSInfo p) (SSInfo q) a
 
+error_ :: Prelude.Int -> ScanState.ScanStateDesc -> ([] Trace.SSTrace) ->
+          SState a1 a2 a3
+error_ maxReg sd err x x0 =
+  Prelude.Left err
+
 withScanStatePO :: Prelude.Int -> ScanState.ScanStateDesc ->
                    (ScanState.ScanStateDesc -> () -> SState () () a1) ->
                    SState () () a1
-withScanStatePO maxReg pre f i =
+withScanStatePO maxReg pre f e i =
   case i of {
    Build_SSInfo thisDesc0 _ ->
     let {f0 = f thisDesc0 __} in
     let {x = Build_SSInfo thisDesc0 __} in
-    let {x0 = f0 x} in
+    let {x0 = f0 e x} in
     case x0 of {
-     Prelude.Left s -> Prelude.Left s;
+     Prelude.Left err -> Prelude.Left err;
      Prelude.Right p -> Prelude.Right
       (case p of {
         (,) a0 s -> (,) a0
@@ -122,7 +85,7 @@
 
 liftLen :: Prelude.Int -> ScanState.ScanStateDesc -> (ScanState.ScanStateDesc
            -> SState () () a1) -> SState () () a1
-liftLen maxReg pre f _top_assumption_ =
+liftLen maxReg pre f e _top_assumption_ =
   let {
    _evar_0_ = \sd ->
     let {ss = Build_SSInfo sd __} in
@@ -139,7 +102,7 @@
       case _top_assumption_0 of {
        (,) x x0 -> _evar_0_0 x x0}}
     in
-    case f sd ss of {
+    case f sd e ss of {
      Prelude.Left x -> _evar_0_ x;
      Prelude.Right x -> _evar_0_0 x}}
   in
@@ -157,7 +120,7 @@
 
 moveUnhandledToHandled :: Prelude.Int -> ScanState.ScanStateDesc -> SState 
                           () () ()
-moveUnhandledToHandled maxReg pre x =
+moveUnhandledToHandled maxReg pre e x =
   case x of {
    Build_SSInfo thisDesc0 _ ->
     case thisDesc0 of {
@@ -175,8 +138,8 @@
             (Prelude.fst ((,) i n)) Prelude.Nothing) handled0)) __))}
           in
           let {
-           _evar_0_0 = \_ -> Prelude.Left (ECannotSpillIfRegisterRequired
-            ( i))}
+           _evar_0_0 = \_ -> Prelude.Left ((:)
+            (Trace.ECannotSpillIfRegisterRequired ( i)) e)}
           in
           case Eqtype.eq_op
                  (Eqtype.option_eqType
@@ -203,7 +166,7 @@
 
 moveUnhandledToActive :: Prelude.Int -> ScanState.ScanStateDesc -> PhysReg ->
                          SState () () ()
-moveUnhandledToActive maxReg pre reg x =
+moveUnhandledToActive maxReg pre reg e x =
   case x of {
    Build_SSInfo thisDesc0 _ ->
     case thisDesc0 of {
@@ -219,7 +182,8 @@
           inactive0 handled0) __))}
         in
         let {
-         _evar_0_0 = \_ -> Prelude.Left (ERegisterAlreadyAssigned ( reg))}
+         _evar_0_0 = \_ -> Prelude.Left ((:) (Trace.ERegisterAlreadyAssigned
+          ( reg)) e)}
         in
         case Prelude.not
                (Ssrbool.in_mem (unsafeCoerce reg)
diff --git a/LinearScan/Nat.hs b/LinearScan/Nat.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/Nat.hs
@@ -0,0 +1,15 @@
+
+
+module LinearScan.Nat 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
+
+
diff --git a/LinearScan/NonEmpty.hs b/LinearScan/NonEmpty.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/NonEmpty.hs
@@ -0,0 +1,36 @@
+
+
+module LinearScan.NonEmpty 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
+
+
+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 {
+   [] -> (:[]) x;
+   (:) y ys -> (:) x (coq_NE_from_list y ys)}
+
diff --git a/LinearScan/NonEmpty0.hs b/LinearScan/NonEmpty0.hs
deleted file mode 100644
--- a/LinearScan/NonEmpty0.hs
+++ /dev/null
@@ -1,36 +0,0 @@
-
-
-module LinearScan.NonEmpty0 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
-
-
-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 {
-   [] -> (:[]) x;
-   (:) y ys -> (:) x (coq_NE_from_list y ys)}
-
diff --git a/LinearScan/Prelude0.hs b/LinearScan/Prelude0.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/Prelude0.hs
@@ -0,0 +1,51 @@
+
+
+module LinearScan.Prelude0 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
+
+
+apply :: (a1 -> a2) -> a1 -> a2
+apply f x =
+  f x
+
+first :: (a1 -> a2) -> ((,) a1 a3) -> (,) a2 a3
+first f x =
+  case x of {
+   (,) a z -> (,) (f a) z}
+
+curry :: (a1 -> a2 -> a3) -> ((,) a1 a2) -> a3
+curry f x =
+  case x of {
+   (,) a b -> f a b}
+
+option_map :: (a1 -> a2) -> (Prelude.Maybe a1) -> Prelude.Maybe a2
+option_map f x =
+  case x of {
+   Prelude.Just x0 -> Prelude.Just (f x0);
+   Prelude.Nothing -> Prelude.Nothing}
+
+option_choose :: (Prelude.Maybe a1) -> (Prelude.Maybe a1) -> Prelude.Maybe a1
+option_choose x y =
+  case x of {
+   Prelude.Just a -> x;
+   Prelude.Nothing -> y}
+
+lebf :: (a1 -> Prelude.Int) -> a1 -> a1 -> Prelude.Bool
+lebf f n m =
+  (Prelude.<=) (f n) (f m)
+
+type Coq_oddnum = Prelude.Int
+
+odd1 :: Prelude.Int
+odd1 =
+  (Prelude.succ) 0
+
diff --git a/LinearScan/Range.hs b/LinearScan/Range.hs
--- a/LinearScan/Range.hs
+++ b/LinearScan/Range.hs
@@ -14,7 +14,8 @@
 import qualified LinearScan.Utils
 
 import qualified LinearScan.Datatypes as Datatypes
-import qualified LinearScan.Lib as Lib
+import qualified LinearScan.List1 as List1
+import qualified LinearScan.Prelude0 as Prelude0
 import qualified LinearScan.Specif as Specif
 import qualified LinearScan.UsePos as UsePos
 import qualified LinearScan.Eqtype as Eqtype
@@ -143,7 +144,7 @@
       Prelude.False -> (Prelude.<=) ((Prelude.succ) (rbeg x)) (rend y)})
 
 rangeIntersectionPoint :: RangeDesc -> RangeDesc -> Prelude.Maybe
-                          Lib.Coq_oddnum
+                          Prelude0.Coq_oddnum
 rangeIntersectionPoint x y =
   case rangesIntersect x y of {
    Prelude.True -> Prelude.Just
@@ -206,7 +207,7 @@
         in
          _evar_0_ __ __}
       in
-      case Lib.span (\u ->
+      case List1.span (\u ->
              (Prelude.<=) ((Prelude.succ) (UsePos.uloc u)) before) ups0 of {
        (,) x x0 -> _evar_0_ x x0}})
 
diff --git a/LinearScan/Resolve.hs b/LinearScan/Resolve.hs
--- a/LinearScan/Resolve.hs
+++ b/LinearScan/Resolve.hs
@@ -14,11 +14,14 @@
 import qualified LinearScan.Utils
 
 import qualified LinearScan.Allocate as Allocate
+import qualified LinearScan.Applicative as Applicative
 import qualified LinearScan.Blocks as Blocks
 import qualified LinearScan.Graph as Graph
 import qualified LinearScan.IntMap as IntMap
+import qualified LinearScan.IntSet as IntSet
 import qualified LinearScan.Interval as Interval
-import qualified LinearScan.Lib as Lib
+import qualified LinearScan.Iso as Iso
+import qualified LinearScan.List1 as List1
 import qualified LinearScan.LiveSets as LiveSets
 import qualified LinearScan.Monad as Monad
 import qualified LinearScan.UsePos as UsePos
@@ -110,7 +113,7 @@
                   ResolvingMove
 determineMoves maxReg moves =
   let {
-   graph = Lib.forFold
+   graph = List1.forFold
              (Graph.emptyGraph
                (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)
                  Ssrnat.nat_eqType))
@@ -170,13 +173,13 @@
 
 checkBlockBoundary :: Prelude.Int -> ([] Allocate.Allocation) -> Prelude.Int
                       -> Prelude.Bool -> LiveSets.BlockLiveSets ->
-                      LiveSets.BlockLiveSets -> IntMap.IntSet ->
+                      LiveSets.BlockLiveSets -> IntSet.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 {
+    case IntSet.coq_IntSet_member vid liveIn of {
      Prelude.True -> (:) ((,) vid x) acc;
      Prelude.False -> acc}}
   in
@@ -185,7 +188,7 @@
              (resolvingMoves maxReg allocs (LiveSets.blockLastOpId from)
                (LiveSets.blockFirstOpId to))}
   in
-  Lib.forFold mappings (unsafeCoerce moves) (\ms mv ->
+  List1.forFold mappings (unsafeCoerce moves) (\ms mv ->
     let {
      addToGraphs = \e xs ->
       case xs of {
@@ -222,8 +225,9 @@
                    a5 a1 a2 a3 a4) -> ([] Allocate.Allocation) -> ([] 
                    a1) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> a5
 resolveDataFlow maxReg mDict binfo allocs blocks liveSets =
-  Yoneda.iso_to
-    (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict)))
+  Iso.iso_to
+    (Yoneda.coq_Yoneda_lemma
+      (Applicative.is_functor (Monad.is_applicative mDict)))
     (Monad.forFoldM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict))
       IntMap.emptyIntMap blocks (\mappings b ->
       Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\bid ->
@@ -234,10 +238,10 @@
              in_from = (Prelude.<=) (Data.List.length suxs) ((Prelude.succ)
                          0)}
             in
-            Monad.pure
+            Applicative.pure
               (unsafeCoerce
                 (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))
-              (Lib.forFold mappings suxs (\ms s_bid ->
+              (List1.forFold mappings suxs (\ms s_bid ->
                 case IntMap.coq_IntMap_lookup s_bid liveSets of {
                  Prelude.Just to ->
                   let {
@@ -250,7 +254,7 @@
                  Prelude.Nothing -> ms})))
             (unsafeCoerce (\_ -> Blocks.blockSuccessors mDict binfo b));
          Prelude.Nothing ->
-          Monad.pure
+          Applicative.pure
             (unsafeCoerce
               (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))
             mappings}) (\_ -> Blocks.blockId mDict binfo b)))
diff --git a/LinearScan/ScanState.hs b/LinearScan/ScanState.hs
--- a/LinearScan/ScanState.hs
+++ b/LinearScan/ScanState.hs
@@ -13,7 +13,9 @@
 import qualified LinearScan.Utils
 
 import qualified LinearScan.Interval as Interval
-import qualified LinearScan.Lib as Lib
+import qualified LinearScan.List1 as List1
+import qualified LinearScan.Prelude0 as Prelude0
+import qualified LinearScan.Seq as Seq
 
 
 type PhysReg = Prelude.Int
@@ -73,22 +75,37 @@
    Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0 unhandled0
     active0 inactive0 handled0 -> handled0}
 
-registerWithHighestPos :: Prelude.Int -> ([] (Prelude.Maybe Lib.Coq_oddnum))
-                          -> (,) Prelude.Int (Prelude.Maybe Lib.Coq_oddnum)
-registerWithHighestPos maxReg =
-  (LinearScan.Utils.vfoldl'_with_index) maxReg (\reg res x ->
-    case res of {
-     (,) r o ->
-      case o of {
-       Prelude.Just n ->
-        case x of {
-         Prelude.Just m ->
-          case (Prelude.<=) ((Prelude.succ) ( n)) ( m) of {
-           Prelude.True -> (,) reg (Prelude.Just m);
-           Prelude.False -> (,) r (Prelude.Just n)};
-         Prelude.Nothing -> (,) reg Prelude.Nothing};
-       Prelude.Nothing -> (,) r Prelude.Nothing}}) ((,) ( 0) (Prelude.Just
-    Lib.odd1))
+sortRegisterVector :: Prelude.Int -> ([] Prelude.Bool) -> ([]
+                      (Prelude.Maybe Prelude0.Coq_oddnum)) -> []
+                      ((,) PhysReg (Prelude.Maybe Prelude0.Coq_oddnum))
+sortRegisterVector maxReg fixedAndIntersects =
+  (LinearScan.Utils.vfoldl'_with_index) maxReg (\reg acc mpos ->
+    let {
+     f = \x y ->
+      case x of {
+       (,) xreg xmpos ->
+        case y of {
+         (,) yreg ympos ->
+          let {xfi = LinearScan.Utils.nth maxReg fixedAndIntersects xreg} in
+          let {yfi = LinearScan.Utils.nth maxReg fixedAndIntersects yreg} in
+          case (Prelude.&&) xfi (Prelude.not yfi) of {
+           Prelude.True -> Prelude.False;
+           Prelude.False ->
+            case xmpos of {
+             Prelude.Just xn ->
+              case ympos of {
+               Prelude.Just yn -> (Prelude.<=) ((Prelude.succ) ( yn)) ( xn);
+               Prelude.Nothing -> Prelude.False};
+             Prelude.Nothing -> Prelude.True}}}}}
+    in
+    List1.insert f ((,) reg mpos) acc) []
+
+registerWithHighestPos :: Prelude.Int -> ([] Prelude.Bool) -> ([]
+                          (Prelude.Maybe Prelude0.Coq_oddnum)) -> (,) 
+                          PhysReg (Prelude.Maybe Prelude0.Coq_oddnum)
+registerWithHighestPos maxReg fixedAndIntersects =
+  (Prelude..) (Seq.head ((,) ( 0) (Prelude.Just Prelude0.odd1)))
+    (sortRegisterVector maxReg fixedAndIntersects)
 
 data ScanStateStatus =
    Pending
diff --git a/LinearScan/Seq.hs b/LinearScan/Seq.hs
--- a/LinearScan/Seq.hs
+++ b/LinearScan/Seq.hs
@@ -114,6 +114,18 @@
    [] -> 0;
    (:) x s' -> (Prelude.+) (Ssrnat.nat_of_bool (a x)) (count a s')}
 
+drop :: Prelude.Int -> ([] a1) -> [] a1
+drop n s =
+  case s of {
+   [] -> s;
+   (:) t s' ->
+    (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
+      (\_ ->
+      s)
+      (\n' ->
+      drop n' s')
+      n}
+
 catrev :: ([] a1) -> ([] a1) -> [] a1
 catrev s1 s2 =
   case s1 of {
diff --git a/LinearScan/Spill.hs b/LinearScan/Spill.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/Spill.hs
@@ -0,0 +1,503 @@
+{-# OPTIONS_GHC -cpp -XMagicHash #-}
+{- For Hugs, use the option -F"cpp -P -traditional" -}
+
+module LinearScan.Spill 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.Interval as Interval
+import qualified LinearScan.List1 as List1
+import qualified LinearScan.Logic as Logic
+import qualified LinearScan.Morph as Morph
+import qualified LinearScan.Prelude0 as Prelude0
+import qualified LinearScan.ScanState as ScanState
+import qualified LinearScan.Trace as Trace
+import qualified LinearScan.Eqtype as Eqtype
+import qualified LinearScan.Ssrnat as Ssrnat
+
+
+
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base as GHC.Base
+import qualified GHC.Prim as GHC.Prim
+#else
+-- HUGS
+import qualified LinearScan.IOExts as IOExts
+#endif
+
+
+#ifdef __GLASGOW_HASKELL__
+--unsafeCoerce :: a -> b
+unsafeCoerce = GHC.Base.unsafeCoerce#
+#else
+-- HUGS
+--unsafeCoerce :: a -> b
+unsafeCoerce = IOExts.unsafeCoerce
+#endif
+
+__ :: any
+__ = Prelude.error "Logical or arity value used"
+
+data SpillCondition =
+   NewToHandled
+ | UnhandledToHandled
+ | ActiveToHandled Prelude.Int Eqtype.Equality__Coq_sort
+ | InactiveToHandled Prelude.Int Eqtype.Equality__Coq_sort
+
+coq_SpillConditionToT :: Prelude.Int -> ScanState.ScanStateDesc ->
+                         ScanState.IntervalId -> Interval.IntervalDesc ->
+                         SpillCondition -> Trace.SpillConditionT
+coq_SpillConditionToT maxReg sd uid i x =
+  case x of {
+   NewToHandled -> Trace.NewToHandledT ( uid);
+   UnhandledToHandled -> Trace.UnhandledToHandledT ( uid);
+   ActiveToHandled xid reg -> Trace.ActiveToHandledT ( xid)
+    ( (unsafeCoerce reg));
+   InactiveToHandled xid reg -> Trace.InactiveToHandledT ( xid)
+    ( (unsafeCoerce reg))}
+
+spillInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
+                 Interval.IntervalDesc -> ScanState.IntervalId -> Prelude.Int
+                 -> ([] ((,) ScanState.IntervalId Prelude.Int)) ->
+                 SpillCondition -> ([] Trace.SSTrace) -> Prelude.Either
+                 ([] Trace.SSTrace) ScanState.ScanStateSig
+spillInterval maxReg sd i1 uid beg us spill e =
+  (Prelude.flip (Prelude.$)) ((:) (Trace.ESpillInterval
+    (coq_SpillConditionToT maxReg sd uid i1 spill)) e) (\e2 ->
+    let {
+     _evar_0_ = \_top_assumption_ ->
+      (Prelude.flip (Prelude.$)) ((:) (Trace.EIntervalHasUsePosReqReg
+        _top_assumption_) e2) (\e3 ->
+        let {
+         _evar_0_ = \_ ->
+          let {
+           _evar_0_ = \_ ->
+            (Prelude.flip (Prelude.$)) __
+              (let {
+                _evar_0_ = \_ -> Prelude.Right
+                 (ScanState.packScanState maxReg ScanState.InUse
+                   (ScanState.Build_ScanStateDesc ((Prelude.succ)
+                   (ScanState.nextInterval maxReg sd))
+                   (LinearScan.Utils.snoc (ScanState.nextInterval maxReg sd)
+                     (ScanState.intervals maxReg sd) ( i1))
+                   (ScanState.fixedIntervals maxReg sd)
+                   (List1.insert (Prelude0.lebf Prelude.snd) ((,)
+                     ( (ScanState.nextInterval maxReg sd))
+                     (Interval.ibeg ( i1))) ((:) (Prelude.id ((,) uid beg))
+                     (Prelude.map Prelude.id us)))
+                   (Prelude.map Prelude.id (ScanState.active maxReg sd))
+                   (Prelude.map Prelude.id (ScanState.inactive maxReg sd))
+                   (Prelude.map Prelude.id (ScanState.handled maxReg sd))))}
+               in
+                _evar_0_)}
+          in
+          let {
+           _evar_0_0 = \_ -> Prelude.Left ((:) Trace.ECannotInsertUnhandled
+            ((:) Trace.EIntervalBeginsAtSplitPosition e3))}
+          in
+          case (Prelude.<=) ((Prelude.succ) beg) (Interval.ibeg ( i1)) of {
+           Prelude.True -> _evar_0_ __;
+           Prelude.False -> _evar_0_0 __}}
+        in
+        let {
+         _evar_0_0 = \_ ->
+          (Prelude.flip (Prelude.$)) __ (\_ ->
+            let {
+             _top_assumption_0 = Interval.splitInterval ( i1)
+                                   _top_assumption_}
+            in
+            let {
+             _evar_0_0 = \i1_0 i1_1 ->
+              let {
+               _evar_0_0 = \_top_assumption_1 -> Prelude.Left ((:)
+                (Trace.ECannotSpillIfRegisterRequired ( _top_assumption_1))
+                e3)}
+              in
+              let {
+               _evar_0_1 = \_ ->
+                let {
+                 _evar_0_1 = \_ ->
+                  (Prelude.flip (Prelude.$)) __
+                    (let {
+                      _evar_0_1 = (Prelude.flip (Prelude.$)) __ (\_ _ ->
+                                    let {
+                                     unh' = List1.insert
+                                              (Prelude0.lebf Prelude.snd)
+                                              ((,)
+                                              (
+                                                (ScanState.nextInterval
+                                                  maxReg sd))
+                                              (Interval.ibeg ( i1_1))) ((:)
+                                              (Prelude.id ((,) uid beg))
+                                              (Prelude.map Prelude.id us))}
+                                    in
+                                    let {
+                                     sd' = ScanState.Build_ScanStateDesc
+                                      ((Prelude.succ)
+                                      (ScanState.nextInterval maxReg sd))
+                                      (LinearScan.Utils.snoc
+                                        (ScanState.nextInterval maxReg sd)
+                                        (ScanState.intervals maxReg sd)
+                                        ( i1_1))
+                                      (ScanState.fixedIntervals maxReg sd)
+                                      unh'
+                                      (Prelude.map Prelude.id
+                                        (ScanState.active maxReg sd))
+                                      (Prelude.map Prelude.id
+                                        (ScanState.inactive maxReg sd))
+                                      (Prelude.map Prelude.id
+                                        (ScanState.handled maxReg sd))}
+                                    in
+                                    (Prelude.flip (Prelude.$)) __ (\_ ->
+                                      let {
+                                       _evar_0_1 = let {
+                                                    _evar_0_1 = \_ ->
+                                                     Prelude.Right
+                                                     (ScanState.Build_ScanStateDesc
+                                                     ((Prelude.succ)
+                                                     (ScanState.nextInterval
+                                                       maxReg sd'))
+                                                     (LinearScan.Utils.snoc
+                                                       (ScanState.nextInterval
+                                                         maxReg sd')
+                                                       (ScanState.intervals
+                                                         maxReg sd') 
+                                                       ( i1_0))
+                                                     (ScanState.fixedIntervals
+                                                       maxReg sd')
+                                                     (Prelude.map Prelude.id
+                                                       (ScanState.unhandled
+                                                         maxReg sd'))
+                                                     (Prelude.map Prelude.id
+                                                       (ScanState.active
+                                                         maxReg sd'))
+                                                     (Prelude.map Prelude.id
+                                                       (ScanState.inactive
+                                                         maxReg sd')) ((:)
+                                                     ((,)
+                                                     (
+                                                       (ScanState.nextInterval
+                                                         maxReg sd'))
+                                                     Prelude.Nothing)
+                                                     (Prelude.map Prelude.id
+                                                       (ScanState.handled
+                                                         maxReg sd'))))}
+                                                   in
+                                                    _evar_0_1 __}
+                                      in
+                                      let {
+                                       _evar_0_2 = \_ ->
+                                        (Prelude.flip (Prelude.$)) __ (\_ ->
+                                          (Prelude.flip (Prelude.$)) __
+                                            (\_ _ ->
+                                            let {
+                                             _evar_0_2 = \_ _ _ ->
+                                              let {
+                                               b = Prelude0.lebf Prelude.snd
+                                                     (Prelude.id ((,) uid
+                                                       beg)) ((,)
+                                                     (
+                                                       (ScanState.nextInterval
+                                                         maxReg sd))
+                                                     (Interval.ibeg ( i1_1)))}
+                                              in
+                                              let {
+                                               _evar_0_2 = \_ ->
+                                                Logic.coq_False_rect}
+                                              in
+                                              let {
+                                               _evar_0_3 = \_ ->
+                                                Logic.coq_False_rect}
+                                              in
+                                              case b of {
+                                               Prelude.True -> _evar_0_2 __;
+                                               Prelude.False -> _evar_0_3 __}}
+                                            in
+                                            let {
+                                             _evar_0_3 = \u' us' ->
+                                              (Prelude.flip (Prelude.$)) __
+                                                (\_ -> Prelude.Right
+                                                (ScanState.Build_ScanStateDesc
+                                                ((Prelude.succ)
+                                                (ScanState.nextInterval
+                                                  maxReg sd))
+                                                (LinearScan.Utils.set_nth
+                                                  ((Prelude.succ)
+                                                  (ScanState.nextInterval
+                                                    maxReg sd))
+                                                  (LinearScan.Utils.snoc
+                                                    (ScanState.nextInterval
+                                                      maxReg sd)
+                                                    (ScanState.intervals
+                                                      maxReg sd) ( i1_1))
+                                                  ( uid) ( i1_0))
+                                                (ScanState.fixedIntervals
+                                                  maxReg sd) us'
+                                                (Prelude.map Prelude.id
+                                                  (ScanState.active maxReg
+                                                    sd))
+                                                (Prelude.map Prelude.id
+                                                  (ScanState.inactive maxReg
+                                                    sd)) ((:) ((,)
+                                                (Prelude.fst u')
+                                                Prelude.Nothing)
+                                                (Prelude.map Prelude.id
+                                                  (ScanState.handled maxReg
+                                                    sd)))))}
+                                            in
+                                            case unh' of {
+                                             [] -> _evar_0_2 __ __ __;
+                                             (:) x x0 -> _evar_0_3 x x0})) __}
+                                      in
+                                      let {
+                                       _evar_0_3 = \xid reg ->
+                                        (Prelude.flip (Prelude.$)) __ (\_ ->
+                                          (Prelude.flip (Prelude.$)) __
+                                            (\_ _ ->
+                                            let {
+                                             sd'' = ScanState.Build_ScanStateDesc
+                                              ((Prelude.succ)
+                                              (ScanState.nextInterval maxReg
+                                                sd))
+                                              (LinearScan.Utils.set_nth
+                                                ((Prelude.succ)
+                                                (ScanState.nextInterval
+                                                  maxReg sd))
+                                                (LinearScan.Utils.snoc
+                                                  (ScanState.nextInterval
+                                                    maxReg sd)
+                                                  (ScanState.intervals maxReg
+                                                    sd) ( i1_1)) ( xid)
+                                                ( i1_0))
+                                              (ScanState.fixedIntervals
+                                                maxReg sd) unh'
+                                              (Prelude.map Prelude.id
+                                                (ScanState.active maxReg sd))
+                                              (Prelude.map Prelude.id
+                                                (ScanState.inactive maxReg
+                                                  sd))
+                                              (Prelude.map Prelude.id
+                                                (ScanState.handled maxReg sd))}
+                                            in
+                                            let {
+                                             elem = Prelude.id ((,) xid reg)}
+                                            in
+                                            (Prelude.flip (Prelude.$)) __
+                                              (\_ ->
+                                              let {
+                                               _evar_0_3 = \a b ->
+                                                (Prelude.flip (Prelude.$)) __
+                                                  (\_ ->
+                                                  let {
+                                                   _top_assumption_1 = 
+                                                    Morph.moveActiveToHandled
+                                                      maxReg sd''
+                                                      Prelude.True
+                                                      (unsafeCoerce ((,) a
+                                                        b))}
+                                                  in
+                                                  Prelude.Right
+                                                  _top_assumption_1)}
+                                              in
+                                              case elem of {
+                                               (,) x x0 -> _evar_0_3 x x0})))
+                                          __}
+                                      in
+                                      let {
+                                       _evar_0_4 = \xid reg ->
+                                        (Prelude.flip (Prelude.$)) __ (\_ ->
+                                          (Prelude.flip (Prelude.$)) __
+                                            (\_ _ ->
+                                            let {
+                                             sd'' = ScanState.Build_ScanStateDesc
+                                              ((Prelude.succ)
+                                              (ScanState.nextInterval maxReg
+                                                sd))
+                                              (LinearScan.Utils.set_nth
+                                                ((Prelude.succ)
+                                                (ScanState.nextInterval
+                                                  maxReg sd))
+                                                (LinearScan.Utils.snoc
+                                                  (ScanState.nextInterval
+                                                    maxReg sd)
+                                                  (ScanState.intervals maxReg
+                                                    sd) ( i1_1)) ( xid)
+                                                ( i1_0))
+                                              (ScanState.fixedIntervals
+                                                maxReg sd) unh'
+                                              (Prelude.map Prelude.id
+                                                (ScanState.active maxReg sd))
+                                              (Prelude.map Prelude.id
+                                                (ScanState.inactive maxReg
+                                                  sd))
+                                              (Prelude.map Prelude.id
+                                                (ScanState.handled maxReg sd))}
+                                            in
+                                            let {
+                                             elem = Prelude.id ((,) xid reg)}
+                                            in
+                                            (Prelude.flip (Prelude.$)) __
+                                              (\_ ->
+                                              let {
+                                               _evar_0_4 = \a b ->
+                                                (Prelude.flip (Prelude.$)) __
+                                                  (\_ ->
+                                                  let {
+                                                   _top_assumption_1 = 
+                                                    Morph.moveInactiveToHandled
+                                                      maxReg sd''
+                                                      Prelude.True
+                                                      (unsafeCoerce ((,) a
+                                                        b))}
+                                                  in
+                                                  Prelude.Right
+                                                  _top_assumption_1)}
+                                              in
+                                              case elem of {
+                                               (,) x x0 -> _evar_0_4 x x0})))
+                                          __}
+                                      in
+                                      case spill of {
+                                       NewToHandled -> _evar_0_1;
+                                       UnhandledToHandled -> _evar_0_2 __;
+                                       ActiveToHandled x x0 -> _evar_0_3 x x0;
+                                       InactiveToHandled x x0 ->
+                                        _evar_0_4 x x0}))}
+                     in
+                      _evar_0_1)}
+                in
+                 _evar_0_1 __}
+              in
+              case Interval.firstUseReqReg ( i1_0) of {
+               Prelude.Just x -> _evar_0_0 x;
+               Prelude.Nothing -> _evar_0_1 __}}
+            in
+            case _top_assumption_0 of {
+             (,) x x0 -> _evar_0_0 x x0})}
+        in
+        case Eqtype.eq_op Ssrnat.nat_eqType
+               (unsafeCoerce (Interval.ibeg ( i1)))
+               (unsafeCoerce _top_assumption_) of {
+         Prelude.True -> _evar_0_ __;
+         Prelude.False -> _evar_0_0 __})}
+    in
+    let {
+     _evar_0_0 = \_ ->
+      let {
+       _evar_0_0 = Prelude.Right (ScanState.Build_ScanStateDesc
+        ((Prelude.succ) (ScanState.nextInterval maxReg sd))
+        (LinearScan.Utils.snoc (ScanState.nextInterval maxReg sd)
+          (ScanState.intervals maxReg sd) ( i1))
+        (ScanState.fixedIntervals maxReg sd)
+        (Prelude.map Prelude.id (ScanState.unhandled maxReg sd))
+        (Prelude.map Prelude.id (ScanState.active maxReg sd))
+        (Prelude.map Prelude.id (ScanState.inactive maxReg sd)) ((:) ((,)
+        ( (ScanState.nextInterval maxReg sd)) Prelude.Nothing)
+        (Prelude.map Prelude.id (ScanState.handled maxReg sd))))}
+      in
+      let {
+       _evar_0_1 = \_ ->
+        let {
+         _evar_0_1 = \_ ->
+          case sd of {
+           ScanState.Build_ScanStateDesc nextInterval0 intervals0
+            fixedIntervals0 unhandled0 active0 inactive0 handled0 ->
+            let {
+             _evar_0_1 = \_ ->
+              (Prelude.flip (Prelude.$)) __ (\_ -> Prelude.Right
+                (ScanState.Build_ScanStateDesc nextInterval0 intervals0
+                fixedIntervals0 us active0 inactive0 ((:) ((,)
+                (Prelude.fst ((,) uid beg)) Prelude.Nothing) handled0)))}
+            in
+             _evar_0_1 __}}
+        in
+         _evar_0_1 __}
+      in
+      let {
+       _evar_0_2 = \xid _reg_ ->
+        (Prelude.flip (Prelude.$)) __ (\_ ->
+          let {
+           _top_assumption_ = Morph.moveActiveToHandled maxReg sd
+                                Prelude.True (unsafeCoerce ((,) xid _reg_))}
+          in
+          Prelude.Right _top_assumption_)}
+      in
+      let {
+       _evar_0_3 = \xid _reg_ ->
+        (Prelude.flip (Prelude.$)) __ (\_ ->
+          let {
+           _top_assumption_ = Morph.moveInactiveToHandled maxReg sd
+                                Prelude.True (unsafeCoerce ((,) xid _reg_))}
+          in
+          Prelude.Right _top_assumption_)}
+      in
+      case spill of {
+       NewToHandled -> _evar_0_0;
+       UnhandledToHandled -> _evar_0_1 __;
+       ActiveToHandled x x0 -> _evar_0_2 x x0;
+       InactiveToHandled x x0 -> _evar_0_3 x x0}}
+    in
+    case Interval.firstUseReqReg ( i1) of {
+     Prelude.Just x -> _evar_0_ x;
+     Prelude.Nothing -> _evar_0_0 __})
+
+spillCurrentInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
+                        Morph.SState () () ()
+spillCurrentInterval maxReg pre e ssi =
+  (Prelude.flip (Prelude.$)) ((:) Trace.ESpillCurrentInterval e) (\e2 ->
+    let {
+     _evar_0_ = \sd ->
+      let {_evar_0_ = \_ _ _ _ _ -> Logic.coq_False_rect} in
+      let {
+       _evar_0_0 = \_top_assumption_ ->
+        let {
+         _evar_0_0 = \uid beg us ->
+          (Prelude.flip (Prelude.$)) __
+            (let {
+              d = 
+                    (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)
+                      (ScanState.intervals maxReg sd) uid)}
+             in
+             \_ _ ->
+             let {
+              _evar_0_0 = \_ ->
+               let {_evar_0_0 = \err -> Prelude.Left err} in
+               let {
+                _evar_0_1 = \_top_assumption_0 -> Prelude.Right ((,) ()
+                 (Morph.Build_SSInfo _top_assumption_0 __))}
+               in
+               case spillInterval maxReg sd
+                      (LinearScan.Utils.nth
+                        (ScanState.nextInterval maxReg sd)
+                        (ScanState.intervals maxReg sd) uid) uid beg us
+                      UnhandledToHandled e of {
+                Prelude.Left x -> _evar_0_0 x;
+                Prelude.Right x -> _evar_0_1 x}}
+             in
+             let {
+              _evar_0_1 = \_ -> Prelude.Left ((:)
+               (Trace.EIntervalBeginsBeforeUnhandled ( uid)) e)}
+             in
+             case (Prelude.<=) beg (Interval.ibeg d) of {
+              Prelude.True -> _evar_0_0 __;
+              Prelude.False -> _evar_0_1 __})}
+        in
+        (\us _ _ _ _ ->
+        case _top_assumption_ of {
+         (,) x x0 -> _evar_0_0 x x0 us})}
+      in
+      case ScanState.unhandled maxReg sd of {
+       [] -> _evar_0_ __ __ __ __;
+       (:) x x0 -> _evar_0_0 x x0 __ __ __ __}}
+    in
+    case ssi of {
+     Morph.Build_SSInfo x x0 -> _evar_0_ x __})
+
diff --git a/LinearScan/Split.hs b/LinearScan/Split.hs
--- a/LinearScan/Split.hs
+++ b/LinearScan/Split.hs
@@ -13,919 +13,570 @@
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
-import qualified LinearScan.Datatypes as Datatypes
-import qualified LinearScan.Interval as Interval
-import qualified LinearScan.Lib as Lib
-import qualified LinearScan.Logic as Logic
-import qualified LinearScan.Morph as Morph
-import qualified LinearScan.ScanState as ScanState
-import qualified LinearScan.Eqtype as Eqtype
-import qualified LinearScan.Fintype as Fintype
-import qualified LinearScan.Seq as Seq
-import qualified LinearScan.Ssrbool as Ssrbool
-import qualified LinearScan.Ssrnat as Ssrnat
-
-
-
-#ifdef __GLASGOW_HASKELL__
-import qualified GHC.Base as GHC.Base
-import qualified GHC.Prim as GHC.Prim
-#else
--- HUGS
-import qualified LinearScan.IOExts as IOExts
-#endif
-
-
-#ifdef __GLASGOW_HASKELL__
---unsafeCoerce :: a -> b
-unsafeCoerce = GHC.Base.unsafeCoerce#
-#else
--- HUGS
---unsafeCoerce :: a -> b
-unsafeCoerce = IOExts.unsafeCoerce
-#endif
-
-__ :: any
-__ = Prelude.error "Logical or arity value used"
-
-type PhysReg = Prelude.Int
-
-splitPosition :: Interval.IntervalDesc -> Morph.SplitPosition ->
-                 Lib.Coq_oddnum
-splitPosition d pos =
-  case pos of {
-   Morph.BeforePos n wildcard' -> n;
-   Morph.EndOfLifetimeHole n ->
-    Interval.afterLifetimeHole (Interval.getIntervalDesc d) n}
-
-data SpillCondition =
-   NewToHandled
- | UnhandledToHandled
- | ActiveToHandled Prelude.Int Eqtype.Equality__Coq_sort
- | InactiveToHandled Prelude.Int Eqtype.Equality__Coq_sort
-
-spillConditionToDetails :: Prelude.Int -> ScanState.ScanStateDesc ->
-                           ScanState.IntervalId -> Interval.IntervalDesc ->
-                           SpillCondition -> Morph.SpillDetails
-spillConditionToDetails maxReg sd uid i spill =
-  case spill of {
-   NewToHandled -> Morph.SD_NewToHandled;
-   UnhandledToHandled -> Morph.SD_UnhandledToHandled ( uid);
-   ActiveToHandled xid reg -> Morph.SD_ActiveToHandled ( xid)
-    ( (unsafeCoerce reg));
-   InactiveToHandled xid reg -> Morph.SD_InactiveToHandled ( xid)
-    ( (unsafeCoerce reg))}
-
-spillInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
-                 Interval.IntervalDesc -> ScanState.IntervalId -> Prelude.Int
-                 -> ([] ((,) ScanState.IntervalId Prelude.Int)) ->
-                 SpillCondition -> Prelude.Either Morph.SSError
-                 ScanState.ScanStateSig
-spillInterval maxReg sd i1 uid beg us spill =
-  let {
-   _evar_0_ = \_top_assumption_ ->
-    let {
-     _evar_0_ = \_ ->
-      let {
-       _evar_0_ = \_ ->
-        (Prelude.flip (Prelude.$)) __
-          (let {
-            _evar_0_ = \_ -> Prelude.Right
-             (ScanState.packScanState maxReg ScanState.InUse
-               (ScanState.Build_ScanStateDesc ((Prelude.succ)
-               (ScanState.nextInterval maxReg sd))
-               (LinearScan.Utils.snoc (ScanState.nextInterval maxReg sd)
-                 (ScanState.intervals maxReg sd) ( i1))
-               (ScanState.fixedIntervals maxReg sd)
-               (Lib.insert (Lib.lebf Prelude.snd) ((,)
-                 ( (ScanState.nextInterval maxReg sd)) (Interval.ibeg ( i1)))
-                 ((:) (Prelude.id ((,) uid beg))
-                 (Prelude.map Prelude.id us)))
-               (Prelude.map Prelude.id (ScanState.active maxReg sd))
-               (Prelude.map Prelude.id (ScanState.inactive maxReg sd))
-               (Prelude.map Prelude.id (ScanState.handled maxReg sd))))}
-           in
-            _evar_0_)}
-      in
-      let {
-       _evar_0_0 = \_ ->
-        let {det = spillConditionToDetails maxReg sd uid i1 spill} in
-        Prelude.Left (Morph.ECannotInsertUnhAtPos det beg)}
-      in
-      case (Prelude.<=) ((Prelude.succ) beg) (Interval.ibeg ( i1)) of {
-       Prelude.True -> _evar_0_ __;
-       Prelude.False -> _evar_0_0 __}}
-    in
-    let {
-     _evar_0_0 = \_ ->
-      (Prelude.flip (Prelude.$)) __ (\_ ->
-        let {
-         _top_assumption_0 = Interval.splitInterval ( i1) _top_assumption_}
-        in
-        let {
-         _evar_0_0 = \i1_0 i1_1 ->
-          let {
-           _evar_0_0 = \_top_assumption_1 -> Prelude.Left
-            (Morph.ECannotSpillIfRegisterRequired ( _top_assumption_1))}
-          in
-          let {
-           _evar_0_1 = \_ ->
-            let {
-             _evar_0_1 = \_ ->
-              (Prelude.flip (Prelude.$)) __
-                (let {
-                  _evar_0_1 = (Prelude.flip (Prelude.$)) __ (\_ _ ->
-                                let {
-                                 unh' = Lib.insert (Lib.lebf Prelude.snd)
-                                          ((,)
-                                          (
-                                            (ScanState.nextInterval maxReg
-                                              sd)) (Interval.ibeg ( i1_1)))
-                                          ((:) (Prelude.id ((,) uid beg))
-                                          (Prelude.map Prelude.id us))}
-                                in
-                                let {
-                                 sd' = ScanState.Build_ScanStateDesc
-                                  ((Prelude.succ)
-                                  (ScanState.nextInterval maxReg sd))
-                                  (LinearScan.Utils.snoc
-                                    (ScanState.nextInterval maxReg sd)
-                                    (ScanState.intervals maxReg sd) ( i1_1))
-                                  (ScanState.fixedIntervals maxReg sd) unh'
-                                  (Prelude.map Prelude.id
-                                    (ScanState.active maxReg sd))
-                                  (Prelude.map Prelude.id
-                                    (ScanState.inactive maxReg sd))
-                                  (Prelude.map Prelude.id
-                                    (ScanState.handled maxReg sd))}
-                                in
-                                (Prelude.flip (Prelude.$)) __ (\_ ->
-                                  let {
-                                   _evar_0_1 = let {
-                                                _evar_0_1 = \_ ->
-                                                 Prelude.Right
-                                                 (ScanState.Build_ScanStateDesc
-                                                 ((Prelude.succ)
-                                                 (ScanState.nextInterval
-                                                   maxReg sd'))
-                                                 (LinearScan.Utils.snoc
-                                                   (ScanState.nextInterval
-                                                     maxReg sd')
-                                                   (ScanState.intervals
-                                                     maxReg sd') ( i1_0))
-                                                 (ScanState.fixedIntervals
-                                                   maxReg sd')
-                                                 (Prelude.map Prelude.id
-                                                   (ScanState.unhandled
-                                                     maxReg sd'))
-                                                 (Prelude.map Prelude.id
-                                                   (ScanState.active maxReg
-                                                     sd'))
-                                                 (Prelude.map Prelude.id
-                                                   (ScanState.inactive maxReg
-                                                     sd')) ((:) ((,)
-                                                 (
-                                                   (ScanState.nextInterval
-                                                     maxReg sd'))
-                                                 Prelude.Nothing)
-                                                 (Prelude.map Prelude.id
-                                                   (ScanState.handled maxReg
-                                                     sd'))))}
-                                               in
-                                                _evar_0_1 __}
-                                  in
-                                  let {
-                                   _evar_0_2 = \_ ->
-                                    (Prelude.flip (Prelude.$)) __ (\_ ->
-                                      (Prelude.flip (Prelude.$)) __ (\_ _ ->
-                                        let {
-                                         _evar_0_2 = \_ _ _ ->
-                                          let {
-                                           b = Lib.lebf Prelude.snd
-                                                 (Prelude.id ((,) uid beg))
-                                                 ((,)
-                                                 (
-                                                   (ScanState.nextInterval
-                                                     maxReg sd))
-                                                 (Interval.ibeg ( i1_1)))}
-                                          in
-                                          let {
-                                           _evar_0_2 = \_ ->
-                                            Logic.coq_False_rect}
-                                          in
-                                          let {
-                                           _evar_0_3 = \_ ->
-                                            Logic.coq_False_rect}
-                                          in
-                                          case b of {
-                                           Prelude.True -> _evar_0_2 __;
-                                           Prelude.False -> _evar_0_3 __}}
-                                        in
-                                        let {
-                                         _evar_0_3 = \u' us' ->
-                                          (Prelude.flip (Prelude.$)) __
-                                            (\_ -> Prelude.Right
-                                            (ScanState.Build_ScanStateDesc
-                                            ((Prelude.succ)
-                                            (ScanState.nextInterval maxReg
-                                              sd))
-                                            (LinearScan.Utils.set_nth
-                                              ((Prelude.succ)
-                                              (ScanState.nextInterval maxReg
-                                                sd))
-                                              (LinearScan.Utils.snoc
-                                                (ScanState.nextInterval
-                                                  maxReg sd)
-                                                (ScanState.intervals maxReg
-                                                  sd) ( i1_1)) ( uid)
-                                              ( i1_0))
-                                            (ScanState.fixedIntervals maxReg
-                                              sd) us'
-                                            (Prelude.map Prelude.id
-                                              (ScanState.active maxReg sd))
-                                            (Prelude.map Prelude.id
-                                              (ScanState.inactive maxReg sd))
-                                            ((:) ((,) (Prelude.fst u')
-                                            Prelude.Nothing)
-                                            (Prelude.map Prelude.id
-                                              (ScanState.handled maxReg sd)))))}
-                                        in
-                                        case unh' of {
-                                         [] -> _evar_0_2 __ __ __;
-                                         (:) x x0 -> _evar_0_3 x x0})) __}
-                                  in
-                                  let {
-                                   _evar_0_3 = \xid reg ->
-                                    (Prelude.flip (Prelude.$)) __ (\_ ->
-                                      (Prelude.flip (Prelude.$)) __ (\_ _ ->
-                                        let {
-                                         sd'' = ScanState.Build_ScanStateDesc
-                                          ((Prelude.succ)
-                                          (ScanState.nextInterval maxReg sd))
-                                          (LinearScan.Utils.set_nth
-                                            ((Prelude.succ)
-                                            (ScanState.nextInterval maxReg
-                                              sd))
-                                            (LinearScan.Utils.snoc
-                                              (ScanState.nextInterval maxReg
-                                                sd)
-                                              (ScanState.intervals maxReg sd)
-                                              ( i1_1)) ( xid) ( i1_0))
-                                          (ScanState.fixedIntervals maxReg
-                                            sd) unh'
-                                          (Prelude.map Prelude.id
-                                            (ScanState.active maxReg sd))
-                                          (Prelude.map Prelude.id
-                                            (ScanState.inactive maxReg sd))
-                                          (Prelude.map Prelude.id
-                                            (ScanState.handled maxReg sd))}
-                                        in
-                                        let {elem = Prelude.id ((,) xid reg)}
-                                        in
-                                        (Prelude.flip (Prelude.$)) __ (\_ ->
-                                          let {
-                                           _evar_0_3 = \a b ->
-                                            (Prelude.flip (Prelude.$)) __
-                                              (\_ ->
-                                              let {
-                                               _top_assumption_1 = Morph.moveActiveToHandled
-                                                                    maxReg
-                                                                    sd''
-                                                                    Prelude.True
-                                                                    (unsafeCoerce
-                                                                    ((,) a
-                                                                    b))}
-                                              in
-                                              Prelude.Right _top_assumption_1)}
-                                          in
-                                          case elem of {
-                                           (,) x x0 -> _evar_0_3 x x0}))) __}
-                                  in
-                                  let {
-                                   _evar_0_4 = \xid reg ->
-                                    (Prelude.flip (Prelude.$)) __ (\_ ->
-                                      (Prelude.flip (Prelude.$)) __ (\_ _ ->
-                                        let {
-                                         sd'' = ScanState.Build_ScanStateDesc
-                                          ((Prelude.succ)
-                                          (ScanState.nextInterval maxReg sd))
-                                          (LinearScan.Utils.set_nth
-                                            ((Prelude.succ)
-                                            (ScanState.nextInterval maxReg
-                                              sd))
-                                            (LinearScan.Utils.snoc
-                                              (ScanState.nextInterval maxReg
-                                                sd)
-                                              (ScanState.intervals maxReg sd)
-                                              ( i1_1)) ( xid) ( i1_0))
-                                          (ScanState.fixedIntervals maxReg
-                                            sd) unh'
-                                          (Prelude.map Prelude.id
-                                            (ScanState.active maxReg sd))
-                                          (Prelude.map Prelude.id
-                                            (ScanState.inactive maxReg sd))
-                                          (Prelude.map Prelude.id
-                                            (ScanState.handled maxReg sd))}
-                                        in
-                                        let {elem = Prelude.id ((,) xid reg)}
-                                        in
-                                        (Prelude.flip (Prelude.$)) __ (\_ ->
-                                          let {
-                                           _evar_0_4 = \a b ->
-                                            (Prelude.flip (Prelude.$)) __
-                                              (\_ ->
-                                              let {
-                                               _top_assumption_1 = Morph.moveInactiveToHandled
-                                                                    maxReg
-                                                                    sd''
-                                                                    Prelude.True
-                                                                    (unsafeCoerce
-                                                                    ((,) a
-                                                                    b))}
-                                              in
-                                              Prelude.Right _top_assumption_1)}
-                                          in
-                                          case elem of {
-                                           (,) x x0 -> _evar_0_4 x x0}))) __}
-                                  in
-                                  case spill of {
-                                   NewToHandled -> _evar_0_1;
-                                   UnhandledToHandled -> _evar_0_2 __;
-                                   ActiveToHandled x x0 -> _evar_0_3 x x0;
-                                   InactiveToHandled x x0 -> _evar_0_4 x x0}))}
-                 in
-                  _evar_0_1)}
-            in
-             _evar_0_1 __}
-          in
-          case Interval.firstUseReqReg ( i1_0) of {
-           Prelude.Just x -> _evar_0_0 x;
-           Prelude.Nothing -> _evar_0_1 __}}
-        in
-        case _top_assumption_0 of {
-         (,) x x0 -> _evar_0_0 x x0})}
-    in
-    case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Interval.ibeg ( i1)))
-           (unsafeCoerce _top_assumption_) of {
-     Prelude.True -> _evar_0_ __;
-     Prelude.False -> _evar_0_0 __}}
-  in
-  let {
-   _evar_0_0 = \_ ->
-    let {
-     _evar_0_0 = Prelude.Right (ScanState.Build_ScanStateDesc ((Prelude.succ)
-      (ScanState.nextInterval maxReg sd))
-      (LinearScan.Utils.snoc (ScanState.nextInterval maxReg sd)
-        (ScanState.intervals maxReg sd) ( i1))
-      (ScanState.fixedIntervals maxReg sd)
-      (Prelude.map Prelude.id (ScanState.unhandled maxReg sd))
-      (Prelude.map Prelude.id (ScanState.active maxReg sd))
-      (Prelude.map Prelude.id (ScanState.inactive maxReg sd)) ((:) ((,)
-      ( (ScanState.nextInterval maxReg sd)) Prelude.Nothing)
-      (Prelude.map Prelude.id (ScanState.handled maxReg sd))))}
-    in
-    let {
-     _evar_0_1 = \_ ->
-      let {
-       _evar_0_1 = \_ ->
-        case sd of {
-         ScanState.Build_ScanStateDesc nextInterval0 intervals0
-          fixedIntervals0 unhandled0 active0 inactive0 handled0 ->
-          let {
-           _evar_0_1 = \_ ->
-            (Prelude.flip (Prelude.$)) __ (\_ -> Prelude.Right
-              (ScanState.Build_ScanStateDesc nextInterval0 intervals0
-              fixedIntervals0 us active0 inactive0 ((:) ((,)
-              (Prelude.fst ((,) uid beg)) Prelude.Nothing) handled0)))}
-          in
-           _evar_0_1 __}}
-      in
-       _evar_0_1 __}
-    in
-    let {
-     _evar_0_2 = \xid _reg_ ->
-      (Prelude.flip (Prelude.$)) __ (\_ ->
-        let {
-         _top_assumption_ = Morph.moveActiveToHandled maxReg sd Prelude.True
-                              (unsafeCoerce ((,) xid _reg_))}
-        in
-        Prelude.Right _top_assumption_)}
-    in
-    let {
-     _evar_0_3 = \xid _reg_ ->
-      (Prelude.flip (Prelude.$)) __ (\_ ->
-        let {
-         _top_assumption_ = Morph.moveInactiveToHandled maxReg sd
-                              Prelude.True (unsafeCoerce ((,) xid _reg_))}
-        in
-        Prelude.Right _top_assumption_)}
-    in
-    case spill of {
-     NewToHandled -> _evar_0_0;
-     UnhandledToHandled -> _evar_0_1 __;
-     ActiveToHandled x x0 -> _evar_0_2 x x0;
-     InactiveToHandled x x0 -> _evar_0_3 x x0}}
-  in
-  case Interval.firstUseReqReg ( i1) of {
-   Prelude.Just x -> _evar_0_ x;
-   Prelude.Nothing -> _evar_0_0 __}
-
-spillCurrentInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
-                        Morph.SState () () ()
-spillCurrentInterval maxReg pre ssi =
-  let {
-   _evar_0_ = \sd ->
-    let {_evar_0_ = \_ _ _ _ _ -> Logic.coq_False_rect} in
-    let {
-     _evar_0_0 = \_top_assumption_ ->
-      let {
-       _evar_0_0 = \uid beg us ->
-        (Prelude.flip (Prelude.$)) __
-          (let {
-            d = 
-                  (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)
-                    (ScanState.intervals maxReg sd) uid)}
-           in
-           \_ _ ->
-           let {
-            _evar_0_0 = \_ ->
-             let {_evar_0_0 = \err -> Prelude.Left err} in
-             let {
-              _evar_0_1 = \_top_assumption_0 -> Prelude.Right ((,) ()
-               (Morph.Build_SSInfo _top_assumption_0 __))}
-             in
-             case spillInterval maxReg sd
-                    (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)
-                      (ScanState.intervals maxReg sd) uid) uid beg us
-                    UnhandledToHandled of {
-              Prelude.Left x -> _evar_0_0 x;
-              Prelude.Right x -> _evar_0_1 x}}
-           in
-           let {
-            _evar_0_1 = \_ -> Prelude.Left
-             (Morph.EIntervalBeginsBeforeUnhandled ( uid))}
-           in
-           case (Prelude.<=) beg (Interval.ibeg d) of {
-            Prelude.True -> _evar_0_0 __;
-            Prelude.False -> _evar_0_1 __})}
-      in
-      (\us _ _ _ _ ->
-      case _top_assumption_ of {
-       (,) x x0 -> _evar_0_0 x x0 us})}
-    in
-    case ScanState.unhandled maxReg sd of {
-     [] -> _evar_0_ __ __ __ __;
-     (:) x x0 -> _evar_0_0 x x0 __ __ __ __}}
-  in
-  case ssi of {
-   Morph.Build_SSInfo x x0 -> _evar_0_ x __}
-
-splitUnhandledInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
-                          ScanState.IntervalId -> Prelude.Int -> ([]
-                          ((,) ScanState.IntervalId Prelude.Int)) ->
-                          Morph.SplitPosition -> Prelude.Either Morph.SSError
-                          ScanState.ScanStateSig
-splitUnhandledInterval maxReg sd uid beg us pos =
-  let {
-   _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_ = \_ ->
-      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_ = \_ _ ->
-                        (Prelude.flip (Prelude.$)) __ (\_ _ ->
-                          let {
-                           _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_0 = \_ ->
-                                (Prelude.flip (Prelude.$)) __
-                                  (let {
-                                    _evar_0_0 = let {
-                                                 _evar_0_0 = (Prelude.flip (Prelude.$))
-                                                               __ (\_ _ ->
-                                                               Prelude.Right
-                                                               (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
-                               _evar_0_0 __)}
-                          in
-                          case unh of {
-                           [] -> _evar_0_ uid0 us0;
-                           (:) x x0 -> _evar_0_0 x x0 uid0 us0}) __}
-                      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.ENoValidSplitPositionUnh pos
-      ( uid0))}
-    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}
-
-splitCurrentInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
-                        Morph.SplitPosition -> Morph.SState () () ()
-splitCurrentInterval maxReg pre pos ssi =
-  let {
-   _evar_0_ = \desc ->
-    let {_evar_0_ = \_ _ _ _ _ -> Logic.coq_False_rect} in
-    let {
-     _evar_0_0 = \_top_assumption_ ->
-      let {
-       _evar_0_0 = \uid beg us ->
-        let {
-         _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 -> Prelude.Right ((,) ()
-            (Morph.Build_SSInfo _top_assumption_1 __))}
-          in
-          case _top_assumption_0 of {
-           Prelude.Left x -> _evar_0_0 x;
-           Prelude.Right x -> _evar_0_1 x}}
-        in
-        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
-      (\us _ _ _ _ _ ->
-      case _top_assumption_ of {
-       (,) x x0 -> _evar_0_0 x x0 us})}
-    in
-    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 -> Morph.SplitPosition
-                                 -> PhysReg -> (Prelude.Either () ()) ->
-                                 Prelude.Either Morph.SSError
-                                 ScanState.ScanStateSig
-splitActiveOrInactiveInterval maxReg sd uid beg us xid pos reg hin =
-  let {
-   _evar_0_ = \ni ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 us0 xid0 hin0 ->
-    let {int = LinearScan.Utils.nth ni ints xid0} in
-    let {splitPos = splitPosition ( int) pos} in
-    let {
-     sd0 = ScanState.Build_ScanStateDesc ni ints _fixedIntervals_ unh
-      _active_ _inactive_ _handled_}
-    in
-    (Prelude.flip (Prelude.$)) __ (\_ ->
-      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_ = \_ _ ->
-                          (Prelude.flip (Prelude.$)) __ (\_ _ ->
-                            let {
-                             sd1 = ScanState.Build_ScanStateDesc ni
-                              (LinearScan.Utils.set_nth ni ints xid0 ( i0))
-                              _fixedIntervals_ unh _active_ _inactive_
-                              _handled_}
-                            in
-                            (Prelude.flip (Prelude.$)) __ (\_ ->
-                              (Prelude.flip (Prelude.$)) __ (\_ ->
-                                (Prelude.flip (Prelude.$)) __ (\_ ->
-                                  let {_evar_0_ = \err -> Prelude.Left err}
-                                  in
-                                  let {
-                                   _evar_0_0 = \_top_assumption_0 ->
-                                    Prelude.Right _top_assumption_0}
-                                  in
-                                  case spillInterval maxReg sd1 i1 uid0 beg
-                                         us0 NewToHandled of {
-                                   Prelude.Left x -> _evar_0_ x;
-                                   Prelude.Right x -> _evar_0_0 x})))) __}
-                        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 = \_ ->
-        let {
-         _evar_0_0 = \_ ->
-          let {
-           _evar_0_0 = \_ ->
-            let {_evar_0_0 = \err -> Prelude.Left err} in
-            let {
-             _evar_0_1 = \_top_assumption_ -> Prelude.Right _top_assumption_}
-            in
-            case spillInterval maxReg sd0 int uid0 beg us0 (ActiveToHandled
-                   xid0 (unsafeCoerce reg)) of {
-             Prelude.Left x -> _evar_0_0 x;
-             Prelude.Right x -> _evar_0_1 x}}
-          in
-          let {
-           _evar_0_1 = \_ ->
-            let {_evar_0_1 = \err -> Prelude.Left err} in
-            let {
-             _evar_0_2 = \_top_assumption_ -> Prelude.Right _top_assumption_}
-            in
-            case spillInterval maxReg sd0 int uid0 beg us0 (InactiveToHandled
-                   xid0 (unsafeCoerce reg)) of {
-             Prelude.Left x -> _evar_0_1 x;
-             Prelude.Right x -> _evar_0_2 x}}
-          in
-          case hin0 of {
-           Prelude.Left x -> _evar_0_0 x;
-           Prelude.Right x -> _evar_0_1 x}}
-        in
-        let {
-         _evar_0_1 = \_ -> Prelude.Left (Morph.ENoValidSplitPosition pos
-          ( xid0))}
-        in
-        case (Prelude.<=) beg (Interval.ibeg ( int)) of {
-         Prelude.True -> _evar_0_0 __;
-         Prelude.False -> _evar_0_1 __}}
-      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 hin}
-
-splitAssignedIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->
-                               PhysReg -> Morph.SplitPosition -> Prelude.Bool
-                               -> Morph.SState () () ()
-splitAssignedIntervalForReg maxReg pre reg pos trueForActives ssi =
-  let {
-   _evar_0_ = \desc ->
-    let {
-     intlist = case trueForActives of {
-                Prelude.True -> ScanState.active maxReg desc;
-                Prelude.False -> ScanState.inactive maxReg desc}}
-    in
-    (Prelude.flip (Prelude.$)) __ (\_ ->
-      let {
-       intids = Prelude.map (\i -> Prelude.fst i)
-                  (Prelude.filter (\i ->
-                    Eqtype.eq_op (Fintype.ordinal_eqType maxReg)
-                      (Prelude.snd (unsafeCoerce i)) (unsafeCoerce reg))
-                    intlist)}
-      in
-      (Prelude.flip (Prelude.$)) __ (\_ ->
-        let {_evar_0_ = \intlist0 intids0 -> Logic.coq_False_rect} in
-        let {
-         _evar_0_0 = \_top_assumption_ ->
-          let {
-           _evar_0_0 = \uid beg us ->
-            let {
-             _evar_0_0 = \_nextInterval_ intervals0 _fixedIntervals_ _unhandled_ active0 inactive0 _handled_ uid0 us0 intlist0 intids0 ->
-              let {
-               _evar_0_0 = \_ -> Prelude.Right ((,) () (Morph.Build_SSInfo
-                (ScanState.Build_ScanStateDesc _nextInterval_ intervals0
-                _fixedIntervals_ _unhandled_ active0 inactive0 _handled_)
-                __))}
-              in
-              let {
-               _evar_0_1 = \aid aids iHaids ->
-                let {
-                 _evar_0_1 = \_ ->
-                  let {
-                   _top_assumption_0 = \x x0 x1 x2 x3 x4 ->
-                    splitActiveOrInactiveInterval maxReg
-                      (ScanState.Build_ScanStateDesc _nextInterval_
-                      intervals0 _fixedIntervals_ _unhandled_ active0
-                      inactive0 _handled_) x x0 x1 x2 x3 x4}
-                  in
-                  (Prelude.flip (Prelude.$))
-                    (let {
-                      _evar_0_1 = \_ ->
-                       let {_evar_0_1 = \_ -> Prelude.Left __} in
-                        _evar_0_1 __}
-                     in
-                     let {
-                      _evar_0_2 = \_ ->
-                       let {_evar_0_2 = \_ -> Prelude.Right __} in
-                        _evar_0_2 __}
-                     in
-                     case trueForActives of {
-                      Prelude.True -> _evar_0_1 __;
-                      Prelude.False -> _evar_0_2 __})
-                    (\hin' _top_assumption_1 ->
-                    let {_top_assumption_2 = _top_assumption_1 hin'} in
-                    let {_evar_0_1 = \err -> Prelude.Left err} in
-                    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
-                    case _top_assumption_2 of {
-                     Prelude.Left x -> _evar_0_1 x;
-                     Prelude.Right x -> _evar_0_2 x})
-                    (_top_assumption_0 uid0 beg us0 aid pos reg)}
-                in
-                let {
-                 _evar_0_2 = \_ -> Prelude.Left (Morph.ECannotSplitSingleton
-                  pos ( 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
-              Datatypes.list_rect _evar_0_0 (\aid aids iHaids _ ->
-                _evar_0_1 aid aids iHaids) intids0 __}
-            in
-            (\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
-          (\us _ ->
-          case _top_assumption_ of {
-           (,) x x0 -> _evar_0_0 x x0 us})}
-        in
-        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 __}
-
-splitActiveIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->
-                             PhysReg -> Lib.Coq_oddnum -> Morph.SState 
-                             () () ()
-splitActiveIntervalForReg maxReg pre reg pos =
-  splitAssignedIntervalForReg maxReg pre reg (Morph.BeforePos pos
-    (Morph.SplittingActive ( reg))) Prelude.True
-
-splitAnyInactiveIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->
-                                  PhysReg -> Lib.Coq_oddnum -> Morph.SState
-                                  () () ()
-splitAnyInactiveIntervalForReg maxReg pre reg pos ss =
-  (Prelude.flip (Prelude.$)) (\s ->
-    splitAssignedIntervalForReg maxReg s reg (Morph.EndOfLifetimeHole pos)
-      Prelude.False) (\_top_assumption_ ->
-    let {_top_assumption_0 = _top_assumption_ pre ss} in
-    let {_evar_0_ = \err -> Prelude.Right ((,) () ss)} in
-    let {
-     _evar_0_0 = \_top_assumption_1 ->
-      let {_evar_0_0 = \_the_1st_wildcard_ ss' -> Prelude.Right ((,) () ss')}
-      in
-      case _top_assumption_1 of {
-       (,) x x0 -> _evar_0_0 x x0}}
-    in
-    case _top_assumption_0 of {
-     Prelude.Left x -> _evar_0_ x;
-     Prelude.Right x -> _evar_0_0 x})
+import qualified LinearScan.Context as Context
+import qualified LinearScan.Datatypes as Datatypes
+import qualified LinearScan.Interval as Interval
+import qualified LinearScan.List1 as List1
+import qualified LinearScan.Logic as Logic
+import qualified LinearScan.Morph as Morph
+import qualified LinearScan.Prelude0 as Prelude0
+import qualified LinearScan.ScanState as ScanState
+import qualified LinearScan.Spill as Spill
+import qualified LinearScan.Trace as Trace
+import qualified LinearScan.Eqtype as Eqtype
+import qualified LinearScan.Fintype as Fintype
+import qualified LinearScan.Seq as Seq
+import qualified LinearScan.Ssrbool as Ssrbool
+
+
+
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base as GHC.Base
+import qualified GHC.Prim as GHC.Prim
+#else
+-- HUGS
+import qualified LinearScan.IOExts as IOExts
+#endif
+
+
+#ifdef __GLASGOW_HASKELL__
+--unsafeCoerce :: a -> b
+unsafeCoerce = GHC.Base.unsafeCoerce#
+#else
+-- HUGS
+--unsafeCoerce :: a -> b
+unsafeCoerce = IOExts.unsafeCoerce
+#endif
+
+__ :: any
+__ = Prelude.error "Logical or arity value used"
+
+type PhysReg = Prelude.Int
+
+data SplitPosition =
+   BeforePos Prelude0.Coq_oddnum
+ | EndOfLifetimeHole Prelude0.Coq_oddnum
+
+coq_SplitPositionToT :: SplitPosition -> Trace.SplitPositionT
+coq_SplitPositionToT x =
+  case x of {
+   BeforePos n -> Trace.BeforePosT ( n);
+   EndOfLifetimeHole n -> Trace.EndOfLifetimeHoleT ( n)}
+
+splitPosition :: Interval.IntervalDesc -> SplitPosition ->
+                 Prelude0.Coq_oddnum
+splitPosition d pos =
+  case pos of {
+   BeforePos n -> n;
+   EndOfLifetimeHole n ->
+    Interval.afterLifetimeHole (Interval.getIntervalDesc d) n}
+
+splitUnhandledInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
+                          ScanState.IntervalId -> Prelude.Int -> ([]
+                          ((,) ScanState.IntervalId Prelude.Int)) ->
+                          SplitPosition -> ([] Trace.SSTrace) ->
+                          Prelude.Either ([] Trace.SSTrace)
+                          ScanState.ScanStateSig
+splitUnhandledInterval maxReg sd uid beg us pos e =
+  (Prelude.flip (Prelude.$)) ((:) Trace.ESplitUnhandledInterval e) (\e2 ->
+    let {
+     _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_ = \_ ->
+        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_ = \_ _ ->
+                          (Prelude.flip (Prelude.$)) __ (\_ _ ->
+                            let {
+                             _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_0 = \_ ->
+                                  (Prelude.flip (Prelude.$)) __
+                                    (let {
+                                      _evar_0_0 = let {
+                                                   _evar_0_0 = (Prelude.flip (Prelude.$))
+                                                                 __ (\_ _ ->
+                                                                 Prelude.Right
+                                                                 (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_
+                                                                   (List1.insert
+                                                                    (Prelude0.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
+                                 _evar_0_0 __)}
+                            in
+                            case unh of {
+                             [] -> _evar_0_ uid0 us0;
+                             (:) x x0 -> _evar_0_0 x x0 uid0 us0}) __}
+                        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 = \_ ->
+        let {
+         _evar_0_0 = \_ ->
+          let {
+           sd0 = ScanState.Build_ScanStateDesc _nextInterval_ ints
+            _fixedIntervals_ unh _active_ _inactive_ _handled_}
+          in
+          let {_evar_0_0 = \err -> Prelude.Left err} in
+          let {
+           _evar_0_1 = \_top_assumption_ ->
+            let {
+             _evar_0_1 = \_top_assumption_0 -> Prelude.Right
+              _top_assumption_}
+            in
+            let {
+             _evar_0_2 = \_ ->
+              let {_evar_0_2 = \_ -> Prelude.Right _top_assumption_} in
+              let {
+               _evar_0_3 = \_ -> Prelude.Left ((:)
+                (Trace.ENoValidSplitPosition ( uid0)) e)}
+              in
+              case (Prelude.<=) ((Prelude.succ) 0)
+                     (Data.List.length
+                       (ScanState.unhandled maxReg ( _top_assumption_))) of {
+               Prelude.True -> _evar_0_2 __;
+               Prelude.False -> _evar_0_3 __}}
+            in
+            case Interval.firstUseReqReg ( int) of {
+             Prelude.Just x -> _evar_0_1 x;
+             Prelude.Nothing -> _evar_0_2 __}}
+          in
+          case Spill.spillInterval maxReg sd0 int uid0 beg us0
+                 Spill.UnhandledToHandled e of {
+           Prelude.Left x -> _evar_0_0 x;
+           Prelude.Right x -> _evar_0_1 x}}
+        in
+        let {
+         _evar_0_1 = \_ -> Prelude.Left ((:) (Trace.ENoValidSplitPosition
+          ( uid0)) e)}
+        in
+        case (Prelude.<=) beg (Interval.ibeg ( int)) of {
+         Prelude.True -> _evar_0_0 __;
+         Prelude.False -> _evar_0_1 __}}
+      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})
+
+splitCurrentInterval :: Prelude.Int -> ScanState.ScanStateDesc ->
+                        SplitPosition -> Morph.SState () () ()
+splitCurrentInterval maxReg pre pos e ssi =
+  (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitCurrentInterval
+    (coq_SplitPositionToT pos)) e) (\e2 ->
+    let {
+     _evar_0_ = \desc ->
+      let {_evar_0_ = \_ _ _ _ _ -> Logic.coq_False_rect} in
+      let {
+       _evar_0_0 = \_top_assumption_ ->
+        let {
+         _evar_0_0 = \uid beg us ->
+          let {
+           _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 -> Prelude.Right ((,) ()
+              (Morph.Build_SSInfo _top_assumption_1 __))}
+            in
+            case _top_assumption_0 of {
+             Prelude.Left x -> _evar_0_0 x;
+             Prelude.Right x -> _evar_0_1 x}}
+          in
+          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 e2)}}
+        in
+        (\us _ _ _ _ _ ->
+        case _top_assumption_ of {
+         (,) x x0 -> _evar_0_0 x x0 us})}
+      in
+      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 ->
+                                 PhysReg -> (Prelude.Either () ()) -> ([]
+                                 Trace.SSTrace) -> Prelude.Either
+                                 ([] Trace.SSTrace) ScanState.ScanStateSig
+splitActiveOrInactiveInterval maxReg sd uid beg us xid pos reg hin e =
+  (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitActiveOrInactiveInterval
+    (case hin of {
+      Prelude.Left _ -> Prelude.True;
+      Prelude.Right _ -> Prelude.False})) e) (\e2 ->
+    let {
+     _evar_0_ = \ni ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 us0 xid0 hin0 ->
+      let {int = LinearScan.Utils.nth ni ints xid0} in
+      let {splitPos = splitPosition ( int) pos} in
+      let {
+       sd0 = ScanState.Build_ScanStateDesc ni ints _fixedIntervals_ unh
+        _active_ _inactive_ _handled_}
+      in
+      (Prelude.flip (Prelude.$)) __ (\_ ->
+        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_ = \_ _ ->
+                            (Prelude.flip (Prelude.$)) __ (\_ _ ->
+                              let {
+                               sd1 = ScanState.Build_ScanStateDesc ni
+                                (LinearScan.Utils.set_nth ni ints xid0 ( i0))
+                                _fixedIntervals_ unh _active_ _inactive_
+                                _handled_}
+                              in
+                              (Prelude.flip (Prelude.$)) __ (\_ ->
+                                (Prelude.flip (Prelude.$)) __ (\_ ->
+                                  (Prelude.flip (Prelude.$)) __ (\_ ->
+                                    let {_evar_0_ = \err -> Prelude.Left err}
+                                    in
+                                    let {
+                                     _evar_0_0 = \_top_assumption_0 ->
+                                      Prelude.Right _top_assumption_0}
+                                    in
+                                    case Spill.spillInterval maxReg sd1 i1
+                                           uid0 beg us0 Spill.NewToHandled e2 of {
+                                     Prelude.Left x -> _evar_0_ x;
+                                     Prelude.Right x -> _evar_0_0 x})))) __}
+                          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 = \_ ->
+          let {
+           _evar_0_0 = \_ ->
+            let {
+             _evar_0_0 = \_ ->
+              let {_evar_0_0 = \err -> Prelude.Left err} in
+              let {
+               _evar_0_1 = \_top_assumption_ -> Prelude.Right
+                _top_assumption_}
+              in
+              case Spill.spillInterval maxReg sd0 int uid0 beg us0
+                     (Spill.ActiveToHandled xid0 (unsafeCoerce reg)) e2 of {
+               Prelude.Left x -> _evar_0_0 x;
+               Prelude.Right x -> _evar_0_1 x}}
+            in
+            let {
+             _evar_0_1 = \_ ->
+              let {_evar_0_1 = \err -> Prelude.Left err} in
+              let {
+               _evar_0_2 = \_top_assumption_ -> Prelude.Right
+                _top_assumption_}
+              in
+              case Spill.spillInterval maxReg sd0 int uid0 beg us0
+                     (Spill.InactiveToHandled xid0 (unsafeCoerce reg)) e2 of {
+               Prelude.Left x -> _evar_0_1 x;
+               Prelude.Right x -> _evar_0_2 x}}
+            in
+            case hin0 of {
+             Prelude.Left x -> _evar_0_0 x;
+             Prelude.Right x -> _evar_0_1 x}}
+          in
+          let {
+           _evar_0_1 = \_ -> Prelude.Left ((:) (Trace.ENoValidSplitPosition
+            ( xid0)) e2)}
+          in
+          case (Prelude.<=) beg (Interval.ibeg ( int)) of {
+           Prelude.True -> _evar_0_0 __;
+           Prelude.False -> _evar_0_1 __}}
+        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 hin})
+
+splitAssignedIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->
+                               PhysReg -> SplitPosition -> Prelude.Bool ->
+                               Morph.SState () () ()
+splitAssignedIntervalForReg maxReg pre reg pos trueForActives e ssi =
+  (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitAssignedIntervalForReg 
+    ( reg)) e) (\e2 ->
+    let {
+     _evar_0_ = \desc ->
+      let {
+       intlist = case trueForActives of {
+                  Prelude.True -> ScanState.active maxReg desc;
+                  Prelude.False -> ScanState.inactive maxReg desc}}
+      in
+      (Prelude.flip (Prelude.$)) __ (\_ ->
+        let {
+         intids = Prelude.map (\i -> Prelude.fst i)
+                    (Prelude.filter (\i ->
+                      Eqtype.eq_op (Fintype.ordinal_eqType maxReg)
+                        (Prelude.snd (unsafeCoerce i)) (unsafeCoerce reg))
+                      intlist)}
+        in
+        (Prelude.flip (Prelude.$)) __ (\_ ->
+          let {_evar_0_ = \intlist0 intids0 -> Logic.coq_False_rect} in
+          let {
+           _evar_0_0 = \_top_assumption_ ->
+            let {
+             _evar_0_0 = \uid beg us ->
+              let {
+               _evar_0_0 = \_nextInterval_ intervals0 _fixedIntervals_ _unhandled_ active0 inactive0 _handled_ uid0 us0 intlist0 intids0 ->
+                let {
+                 _evar_0_0 = \_ -> Prelude.Right ((,) () (Morph.Build_SSInfo
+                  (ScanState.Build_ScanStateDesc _nextInterval_ intervals0
+                  _fixedIntervals_ _unhandled_ active0 inactive0 _handled_)
+                  __))}
+                in
+                let {
+                 _evar_0_1 = \aid aids iHaids ->
+                  let {
+                   _evar_0_1 = \_ ->
+                    let {
+                     _top_assumption_0 = \x x0 x1 x2 x3 x4 ->
+                      splitActiveOrInactiveInterval maxReg
+                        (ScanState.Build_ScanStateDesc _nextInterval_
+                        intervals0 _fixedIntervals_ _unhandled_ active0
+                        inactive0 _handled_) x x0 x1 x2 x3 x4}
+                    in
+                    (Prelude.flip (Prelude.$))
+                      (let {
+                        _evar_0_1 = \_ ->
+                         let {_evar_0_1 = \_ -> Prelude.Left __} in
+                          _evar_0_1 __}
+                       in
+                       let {
+                        _evar_0_2 = \_ ->
+                         let {_evar_0_2 = \_ -> Prelude.Right __} in
+                          _evar_0_2 __}
+                       in
+                       case trueForActives of {
+                        Prelude.True -> _evar_0_1 __;
+                        Prelude.False -> _evar_0_2 __})
+                      (\hin' _top_assumption_1 ->
+                      let {_top_assumption_2 = _top_assumption_1 hin' e2} in
+                      let {_evar_0_1 = \err -> Prelude.Left err} in
+                      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
+                      case _top_assumption_2 of {
+                       Prelude.Left x -> _evar_0_1 x;
+                       Prelude.Right x -> _evar_0_2 x})
+                      (_top_assumption_0 uid0 beg us0 aid pos reg)}
+                  in
+                  let {
+                   _evar_0_2 = \_ -> Prelude.Left ((:)
+                    (Trace.ECannotSplitSingleton ( aid)) e2)}
+                  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
+                Datatypes.list_rect _evar_0_0 (\aid aids iHaids _ ->
+                  _evar_0_1 aid aids iHaids) intids0 __}
+              in
+              (\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
+            (\us _ ->
+            case _top_assumption_ of {
+             (,) x x0 -> _evar_0_0 x x0 us})}
+          in
+          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 __})
+
+splitActiveIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->
+                             PhysReg -> Prelude0.Coq_oddnum -> Morph.SState
+                             () () ()
+splitActiveIntervalForReg maxReg pre reg pos =
+  Context.context (Trace.ESplitActiveIntervalForReg ( reg))
+    (splitAssignedIntervalForReg maxReg pre reg (BeforePos pos) Prelude.True)
+
+splitAnyInactiveIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->
+                                  PhysReg -> Prelude0.Coq_oddnum ->
+                                  Morph.SState () () ()
+splitAnyInactiveIntervalForReg maxReg pre reg pos e ss =
+  (Prelude.flip (Prelude.$)) ((:) (Trace.ESplitAnyInactiveIntervalForReg
+    ( reg)) e) (\e2 ->
+    (Prelude.flip (Prelude.$)) (\s ->
+      splitAssignedIntervalForReg maxReg s reg (EndOfLifetimeHole pos)
+        Prelude.False) (\_top_assumption_ ->
+      let {_top_assumption_0 = _top_assumption_ pre e2 ss} in
+      let {_evar_0_ = \err -> Prelude.Right ((,) () ss)} in
+      let {
+       _evar_0_0 = \_top_assumption_1 ->
+        let {
+         _evar_0_0 = \_the_1st_wildcard_ ss' -> Prelude.Right ((,) () ss')}
+        in
+        case _top_assumption_1 of {
+         (,) x x0 -> _evar_0_0 x x0}}
+      in
+      case _top_assumption_0 of {
+       Prelude.Left x -> _evar_0_ x;
+       Prelude.Right x -> _evar_0_0 x}))
 
diff --git a/LinearScan/State.hs b/LinearScan/State.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/State.hs
@@ -0,0 +1,85 @@
+{-# OPTIONS_GHC -cpp -XMagicHash #-}
+{- For Hugs, use the option -F"cpp -P -traditional" -}
+
+module LinearScan.State 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.Applicative as Applicative
+import qualified LinearScan.Functor as Functor
+import qualified LinearScan.Monad as Monad
+
+
+
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base as GHC.Base
+import qualified GHC.Prim as GHC.Prim
+#else
+-- HUGS
+import qualified LinearScan.IOExts as IOExts
+#endif
+
+
+#ifdef __GLASGOW_HASKELL__
+--unsafeCoerce :: a -> b
+unsafeCoerce = GHC.Base.unsafeCoerce#
+#else
+-- HUGS
+--unsafeCoerce :: a -> b
+unsafeCoerce = IOExts.unsafeCoerce
+#endif
+
+
+#ifdef __GLASGOW_HASKELL__
+type Any = GHC.Prim.Any
+#else
+-- HUGS
+type Any = ()
+#endif
+
+__ :: any
+__ = Prelude.error "Logical or arity value used"
+
+type State s a = s -> (,) a s
+
+modify :: (a1 -> a1) -> State a1 ()
+modify f i =
+  (,) () (f i)
+
+coq_State_Functor :: Functor.Functor (State a1 Any)
+coq_State_Functor _ _ f x st =
+  let {filtered_var = x st} in
+  case filtered_var of {
+   (,) a st' -> (,) (f a) st'}
+
+coq_State_Applicative :: Applicative.Applicative (State a1 Any)
+coq_State_Applicative =
+  Applicative.Build_Applicative coq_State_Functor (\_ x st -> (,) x st)
+    (\_ _ f x st ->
+    let {filtered_var = f st} in
+    case filtered_var of {
+     (,) f' st' ->
+      unsafeCoerce (\f'0 st'0 _ ->
+        let {filtered_var0 = x st'0} in
+        case filtered_var0 of {
+         (,) x' st'' -> (,) (f'0 x') st''}) f' st' __})
+
+coq_State_Monad :: Monad.Monad (State a1 Any)
+coq_State_Monad =
+  Monad.Build_Monad coq_State_Applicative (\_ x st ->
+    let {filtered_var = x st} in
+    case filtered_var of {
+     (,) y st' ->
+      unsafeCoerce (\y0 st'0 _ ->
+        let {filtered_var0 = y0 st'0} in
+        case filtered_var0 of {
+         (,) a st'' -> (,) a st''}) y st' __})
+
diff --git a/LinearScan/State0.hs b/LinearScan/State0.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/State0.hs
@@ -0,0 +1,106 @@
+{-# OPTIONS_GHC -cpp -XMagicHash #-}
+{- For Hugs, use the option -F"cpp -P -traditional" -}
+
+module LinearScan.State0 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.Applicative as Applicative
+import qualified LinearScan.Functor as Functor
+import qualified LinearScan.Monad as Monad
+import qualified LinearScan.Prelude0 as Prelude0
+import qualified LinearScan.State as State
+
+
+
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base as GHC.Base
+import qualified GHC.Prim as GHC.Prim
+#else
+-- HUGS
+import qualified LinearScan.IOExts as IOExts
+#endif
+
+
+#ifdef __GLASGOW_HASKELL__
+type Any = GHC.Prim.Any
+#else
+-- HUGS
+type Any = ()
+#endif
+
+type StateT s m a = s -> m
+
+getT :: (Applicative.Applicative a1) -> StateT a2 a1 a2
+getT h i =
+  Applicative.pure h ((,) i i)
+
+getsT :: (Applicative.Applicative a1) -> (a2 -> a3) -> StateT a2 a1 a3
+getsT h f s =
+  Applicative.pure h ((,) (f s) s)
+
+putT :: (Applicative.Applicative a1) -> a2 -> StateT a2 a1 ()
+putT h x x0 =
+  Applicative.pure h ((,) () x)
+
+modifyT :: (Applicative.Applicative a1) -> (a2 -> a2) -> StateT a2 a1 ()
+modifyT h f i =
+  Applicative.pure h ((,) () (f i))
+
+coq_StateT_Functor :: (Functor.Functor a2) -> Functor.Functor
+                      (StateT a1 a2 Any)
+coq_StateT_Functor h _ _ f x st =
+  Functor.fmap h (Prelude0.first f) (x st)
+
+coq_StateT_ap :: (Monad.Monad a1) -> (StateT a2 a1 (a3 -> a4)) -> (StateT 
+                 a2 a1 a3) -> StateT a2 a1 a4
+coq_StateT_ap h f x st =
+  Monad.join h
+    (Functor.fmap (Applicative.is_functor (Monad.is_applicative h)) (\z ->
+      case z of {
+       (,) f' st' ->
+        Functor.fmap (Applicative.is_functor (Monad.is_applicative h))
+          (Prelude0.first f') (x st')}) (f st))
+
+coq_StateT_Applicative :: (Monad.Monad a1) -> Applicative.Applicative
+                          (StateT a2 a1 Any)
+coq_StateT_Applicative h =
+  Applicative.Build_Applicative
+    (coq_StateT_Functor (Applicative.is_functor (Monad.is_applicative h)))
+    (\_ x st -> Applicative.pure (Monad.is_applicative h) ((,) x st))
+    (\_ _ -> coq_StateT_ap h)
+
+coq_StateT_join :: (Monad.Monad a1) -> (StateT a2 a1 (StateT a2 a1 a3)) ->
+                   StateT a2 a1 a3
+coq_StateT_join h x =
+  (Prelude..)
+    ((Prelude..) (Monad.join h)
+      (Functor.fmap (Applicative.is_functor (Monad.is_applicative h))
+        (Prelude0.curry Prelude0.apply))) x
+
+coq_StateT_Monad :: (Monad.Monad a1) -> Monad.Monad (StateT a2 a1 Any)
+coq_StateT_Monad h =
+  Monad.Build_Monad (coq_StateT_Applicative h) (\_ -> coq_StateT_join h)
+
+lift :: (Monad.Monad a1) -> a1 -> StateT a2 a1 a3
+lift h x st =
+  Functor.fmap (Applicative.is_functor (Monad.is_applicative h)) (\z -> (,) z
+    st) x
+
+liftStateT :: (Monad.Monad a1) -> (State.State a2 a3) -> StateT a2 a1 a3
+liftStateT h x =
+  Monad.bind (coq_StateT_Monad h) (\st ->
+    case x st of {
+     (,) a st' ->
+      Monad.bind (coq_StateT_Monad h) (\x0 ->
+        Applicative.pure (coq_StateT_Applicative h) a)
+        (putT (Monad.is_applicative h) st')}) (getT (Monad.is_applicative h))
+
diff --git a/LinearScan/String0.hs b/LinearScan/String0.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/String0.hs
@@ -0,0 +1,15 @@
+
+
+module LinearScan.String0 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
+
+
diff --git a/LinearScan/Trace.hs b/LinearScan/Trace.hs
new file mode 100644
--- /dev/null
+++ b/LinearScan/Trace.hs
@@ -0,0 +1,58 @@
+
+
+module LinearScan.Trace 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
+
+
+type IntervalIdT = Prelude.Int
+
+type PhysRegT = Prelude.Int
+
+data SpillConditionT =
+   NewToHandledT IntervalIdT
+ | UnhandledToHandledT IntervalIdT
+ | ActiveToHandledT IntervalIdT PhysRegT
+ | InactiveToHandledT IntervalIdT PhysRegT
+
+data SplitPositionT =
+   BeforePosT Prelude.Int
+ | EndOfLifetimeHoleT Prelude.Int
+
+type TrueIfActiveT = Prelude.Bool
+
+data SSTrace =
+   EIntersectsWithFixedInterval Prelude.Int PhysRegT
+ | ESplitAssignedIntervalForReg PhysRegT
+ | ESplitActiveOrInactiveInterval TrueIfActiveT
+ | EIntervalHasUsePosReqReg IntervalIdT
+ | EIntervalBeginsAtSplitPosition
+ | EMoveUnhandledToActive PhysRegT
+ | ESplitActiveIntervalForReg PhysRegT
+ | ESplitAnyInactiveIntervalForReg PhysRegT
+ | ESpillInterval SpillConditionT
+ | ESpillCurrentInterval
+ | ESplitUnhandledInterval
+ | ESplitCurrentInterval SplitPositionT
+ | ETryAllocateFreeReg PhysRegT (Prelude.Maybe Prelude.Int) IntervalIdT
+ | EAllocateBlockedReg PhysRegT (Prelude.Maybe Prelude.Int) IntervalIdT
+ | ERemoveUnhandledInterval IntervalIdT
+ | ECannotInsertUnhandled
+ | EIntervalBeginsBeforeUnhandled IntervalIdT
+ | ENoValidSplitPosition IntervalIdT
+ | ECannotSplitSingleton IntervalIdT
+ | ERegisterAlreadyAssigned PhysRegT
+ | ERegisterAssignmentsOverlap PhysRegT
+ | EUnexpectedNoMoreUnhandled
+ | ECannotSpillIfRegisterRequired PhysRegT
+ | EFuelExhausted
+ | ENotYetImplemented Prelude.Int
+
diff --git a/LinearScan/Yoneda.hs b/LinearScan/Yoneda.hs
--- a/LinearScan/Yoneda.hs
+++ b/LinearScan/Yoneda.hs
@@ -13,6 +13,9 @@
 import qualified Data.Functor.Identity
 import qualified LinearScan.Utils
 
+import qualified LinearScan.Applicative as Applicative
+import qualified LinearScan.Functor as Functor
+import qualified LinearScan.Iso as Iso
 import qualified LinearScan.Monad as Monad
 
 
@@ -48,30 +51,22 @@
 
 type Yoneda f a = () -> (a -> Any) -> f
 
-data Isomorphism a b =
-   Build_Isomorphism (a -> b) (b -> a)
-
-iso_to :: (Isomorphism a1 a2) -> a1 -> a2
-iso_to isomorphism =
-  case isomorphism of {
-   Build_Isomorphism iso_to0 iso_from -> iso_to0}
-
-coq_Yoneda_lemma :: (Monad.Functor a1) -> Isomorphism (Yoneda a1 a2) a1
+coq_Yoneda_lemma :: (Functor.Functor a1) -> Iso.Isomorphism (Yoneda a1 a2) a1
 coq_Yoneda_lemma h =
-  Build_Isomorphism (\x -> unsafeCoerce x __ (\x0 -> x0)) (\x _ k ->
-    Monad.fmap h k x)
+  Iso.Build_Isomorphism (\x -> unsafeCoerce x __ (\x0 -> x0)) (\x _ k ->
+    Functor.fmap h k x)
 
-coq_Yoneda_Functor :: Monad.Functor (Yoneda a1 Any)
+coq_Yoneda_Functor :: Functor.Functor (Yoneda a1 Any)
 coq_Yoneda_Functor _ _ g k _ h =
   k __ ((Prelude..) h g)
 
-coq_Yoneda_Applicative :: (Monad.Applicative a1) -> Monad.Applicative
-                          (Yoneda a1 Any)
+coq_Yoneda_Applicative :: (Applicative.Applicative a1) ->
+                          Applicative.Applicative (Yoneda a1 Any)
 coq_Yoneda_Applicative h =
-  Monad.Build_Applicative coq_Yoneda_Functor (\_ x _ k -> Monad.pure h (k x))
-    (\_ _ g x _ k ->
-    Monad.ap h (unsafeCoerce g __ ((Prelude..) k))
-      (iso_to (coq_Yoneda_lemma (Monad.is_functor h)) x))
+  Applicative.Build_Applicative coq_Yoneda_Functor (\_ x _ k ->
+    Applicative.pure h (k x)) (\_ _ g x _ k ->
+    Applicative.ap h (unsafeCoerce g __ ((Prelude..) k))
+      (Iso.iso_to (coq_Yoneda_lemma (Applicative.is_functor h)) x))
 
 coq_Yoneda_join :: (Monad.Monad a1) -> (Yoneda a1 (Yoneda a1 a2)) -> (a2 ->
                    a3) -> a1
diff --git a/linearscan.cabal b/linearscan.cabal
--- a/linearscan.cabal
+++ b/linearscan.cabal
@@ -1,5 +1,5 @@
 name:          linearscan
-version:       0.5.1.0
+version:       0.6.0.0
 synopsis:      Linear scan register allocator, formally verified in Coq
 homepage:      http://github.com/jwiegley/linearscan
 license:       BSD3
@@ -49,38 +49,51 @@
     LinearScan
   other-modules:
     LinearScan.Allocate
+    LinearScan.Applicative
+    LinearScan.Ascii
     LinearScan.Assign
     LinearScan.Blocks
     LinearScan.Build
     LinearScan.Choice
+    LinearScan.Context
     LinearScan.Cursor
     LinearScan.Datatypes
     LinearScan.Eqtype
     LinearScan.Fintype
+    LinearScan.Functor
     LinearScan.Graph
-    LinearScan.IState
     LinearScan.IntMap
+    LinearScan.IntSet
     LinearScan.Interval
+    LinearScan.Iso
     LinearScan.Lens
     LinearScan.Lib
     LinearScan.List0
+    LinearScan.List1
     LinearScan.LiveSets
     LinearScan.Logic
     LinearScan.Loops
     LinearScan.Main
     LinearScan.Monad
     LinearScan.Morph
-    LinearScan.NonEmpty0
+    LinearScan.Nat
+    LinearScan.NonEmpty
+    LinearScan.Prelude0
     LinearScan.Range
     LinearScan.Resolve
     LinearScan.ScanState
     LinearScan.Seq
     LinearScan.Specif
+    LinearScan.Spill
     LinearScan.Split
     LinearScan.Ssrbool
     LinearScan.Ssreflect
     LinearScan.Ssrfun
     LinearScan.Ssrnat
+    LinearScan.State
+    LinearScan.State0
+    LinearScan.String0
+    LinearScan.Trace
     LinearScan.UsePos
     LinearScan.Utils
     LinearScan.Vector0