linearscan 0.4.0.0 → 0.5.0.0

raw patch · 39 files changed

+2759/−1675 lines, 39 filesdep +ghc-primdep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: ghc-prim

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• LinearScan.hs +138/−120
• LinearScan/Allocate.hs +48/−16
• LinearScan/Assign.hs +238/−164
• LinearScan/Blocks.hs +118/−69
• LinearScan/Build.hs +144/−93
• LinearScan/Choice.hs +22/−154
• LinearScan/Cursor.hs +2/−0
• LinearScan/Datatypes.hs +2/−0
• LinearScan/Eqtype.hs +38/−52
• LinearScan/Fintype.hs +26/−106
• LinearScan/Graph.hs +11/−3
• LinearScan/IState.hs +2/−0
• LinearScan/IntMap.hs +11/−3
• LinearScan/Interval.hs +30/−42
• LinearScan/Lens.hs +72/−0
• LinearScan/Lib.hs +8/−0
• LinearScan/List0.hs +2/−0
• LinearScan/LiveSets.hs +142/−107
• LinearScan/Logic.hs +2/−0
• LinearScan/Loops.hs +467/−240
• LinearScan/Main.hs +92/−45
• LinearScan/Monad.hs +251/−0
• LinearScan/Morph.hs +87/−24
• LinearScan/NonEmpty0.hs +2/−0
• LinearScan/Range.hs +11/−3
• LinearScan/Resolve.hs +67/−64
• LinearScan/ScanState.hs +2/−0
• LinearScan/Seq.hs +11/−3
• LinearScan/Specif.hs +2/−0
• LinearScan/Split.hs +554/−225
• LinearScan/Ssrbool.hs +21/−5
• LinearScan/Ssreflect.hs +2/−0
• LinearScan/Ssrfun.hs +2/−4
• LinearScan/Ssrnat.hs +11/−28
• LinearScan/State.hs +0/−96
• LinearScan/UsePos.hs +11/−3
• LinearScan/Vector0.hs +19/−3
• LinearScan/Yoneda.hs +85/−0
• linearscan.cabal +6/−3

@@ -1,8 +1,8 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE ViewPatterns #-}  {-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-} @@ -21,14 +21,14 @@     , PhysReg     ) where +import           Control.Applicative import           Control.Monad.State-import           Data.Functor.Identity import           Data.IntMap (IntMap) import qualified Data.IntMap as M import           Data.IntSet (IntSet) import qualified Data.IntSet as S import qualified Data.List as L--- import           Debug.Trace+import           Debug.Trace import qualified LinearScan.Blocks as LS import           LinearScan.Blocks as LS import qualified LinearScan.IntMap as LS@@ -36,11 +36,13 @@ 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.ScanState as LS import qualified LinearScan.UsePos as LS import qualified LinearScan.Utils as LS+import           LinearScan.Yoneda (Any)+import qualified Unsafe.Coerce as U  -- | Each variable has associated allocation details, and a flag to indicate --   whether it must be loaded into a register at its point of use.  Variables@@ -60,9 +62,6 @@ fromVarInfo :: LinearScan.VarInfo -> LS.VarInfo fromVarInfo (VarInfo a b c) = LS.Build_VarInfo a b c -toVarInfo :: LS.VarInfo -> LinearScan.VarInfo-toVarInfo (LS.Build_VarInfo a b c) = VarInfo a b c- -- | Every operation may reference multiple variables and/or specific physical --   registers.  If a physical register is referenced, then that register is --   considered unavailable for allocation over the range of such references.@@ -74,14 +73,14 @@ --   and restore all registers around a call, but indication of loops is --   optional, as it's merely avoids reloading of spilled variables inside --   loop bodies.-data OpInfo accType op1 op2 = OpInfo+data OpInfo m op1 op2 = OpInfo     { opKind      :: op1 -> OpKind     , opRefs      :: op1 -> [LinearScan.VarInfo]-    , moveOp      :: PhysReg   -> PhysReg   -> State accType [op2]-    , swapOp      :: PhysReg   -> PhysReg   -> State accType [op2]-    , saveOp      :: PhysReg   -> Maybe Int -> State accType [op2]-    , restoreOp   :: Maybe Int -> PhysReg   -> State accType [op2]-    , applyAllocs :: op1 -> [(Int, PhysReg)] -> [op2]+    , moveOp      :: PhysReg   -> PhysReg   -> m [op2]+    , swapOp      :: PhysReg   -> PhysReg   -> m [op2]+    , saveOp      :: PhysReg   -> Maybe Int -> m [op2]+    , restoreOp   :: Maybe Int -> PhysReg   -> m [op2]+    , applyAllocs :: op1 -> [(Int, PhysReg)] -> m [op2]     , showOp1     :: op1 -> String     } @@ -109,30 +108,15 @@ deriving instance Eq OpKind deriving instance Show OpKind -fromOpInfo :: LinearScan.OpInfo accType op1 op2 -> LS.OpInfo accType op1 op2+fromOpInfo :: Monad m+           => LinearScan.OpInfo m op1 op2 -> LS.OpInfo (m Any) op1 op2 fromOpInfo (OpInfo a b c d e f g h) =     LS.Build_OpInfo a (map fromVarInfo . b)-        ((runState .) . c)-        ((runState .) . d)-        ((runState .) . e)-        ((runState .) . f) g h--toOpInfo :: LS.OpInfo accType op1 op2 -> LinearScan.OpInfo accType op1 op2-toOpInfo (LS.Build_OpInfo a b c d e f g h) =-    OpInfo a (map toVarInfo . b)-        ((StateT .) . fmap (fmap (fmap Identity)) c)-        ((StateT .) . fmap (fmap (fmap Identity)) d)-        ((StateT .) . fmap (fmap (fmap Identity)) e)-        ((StateT .) . fmap (fmap (fmap Identity)) f) g h---- | From the point of view of this library, a basic block is nothing more---   than an ordered sequence of operations.-data BlockInfo blk1 blk2 op1 op2 = BlockInfo-    { blockId         :: blk1 -> Int-    , blockSuccessors :: blk1 -> [Int]-    , blockOps        :: blk1 -> ([op1], [op1], [op1])-    , setBlockOps     :: blk1 -> [op2] -> [op2] -> [op2] -> blk2-    }+        (\r1 r2 _ k -> liftM k (c r1 r2))+        (\r1 r2 _ k -> liftM k (d r1 r2))+        (\r1 r2 _ k -> liftM k (e r1 r2))+        (\r1 r2 _ k -> liftM k (f r1 r2))+        (\r1 r2 _ k -> liftM k (g r1 r2)) h  type IntervalId = Int @@ -150,6 +134,9 @@ 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 =@@ -167,7 +154,13 @@         "Handled:\n"             ++ concatMap (\(i, r) ->                            "  " ++ showReg r ++ showInterval i ++ "\n")-                         (handled sd)+                         (handled sd) +++        "Fixed:\n"+            ++ concatMap (\(reg, mi) ->+                           case mi of+                           Nothing -> ""+                           Just i -> "  " ++ showIntervalDesc reg i ++ "\n")+                         (zip [0..] (fixedIntervals sd))       where         showInterval i = showIntervalDesc i (intervals sd !! i) @@ -197,8 +190,8 @@   where     go (LS.Build_UsePos n req _v) = show n ++ (if req then "" else "?") -toScanStateDesc :: LS.ScanStateDesc -> ScanStateDesc-toScanStateDesc (LS.Build_ScanStateDesc a b c d e f g) =+toScanStateDesc :: LS.ScanStateDescSet -> ScanStateDesc+toScanStateDesc (LS.Build_ScanStateDescSet a b c d e f g) =     let rs = L.foldl' (\m (k, mx) -> case mx of                             Nothing -> m                             Just r -> M.insert k r m)@@ -239,8 +232,8 @@         (M.fromList (map (fmap S.fromList) g))         (M.fromList h) --- tracer :: String -> a -> a--- tracer x = Debug.Trace.trace ("====================\n" ++ x)+tracer :: String -> a -> a+tracer x = Debug.Trace.trace ("====================\n" ++ x)  showBlock1 :: (blk1 -> [op1])            -> LS.BlockId@@ -286,72 +279,89 @@     showOp1' (showOp1 oinfo) (pos*2+1) begs' ends' o         ++ showOps1 oinfo sd (pos+1) os -showBlocks1 :: LinearScan.BlockInfo blk1 blk2 op1 op2-            -> LinearScan.OpInfo accType op1 op2+-- | From the point of view of this library, a basic block is nothing more+--   than an ordered sequence of operations.+data BlockInfo m blk1 blk2 op1 op2 = BlockInfo+    { blockId           :: blk1 -> m Int+    , blockSuccessors   :: blk1 -> m [Int]+    , splitCriticalEdge :: blk1 -> blk1 -> m (blk1, blk1)+    , blockOps          :: blk1 -> ([op1], [op1], [op1])+    , setBlockOps       :: blk1 -> [op2] -> [op2] -> [op2] -> blk2+    }++showBlocks1 :: Monad m+            => LinearScan.BlockInfo m blk1 blk2 op1 op2+            -> LinearScan.OpInfo m op1 op2             -> ScanStateDesc             -> LS.IntMap LS.BlockLiveSets             -> [blk1]-            -> String+            -> m String showBlocks1 binfo oinfo sd ls = go 0   where-    go _ [] = ""-    go pos (b:bs) =-        let bid = LinearScan.blockId binfo b in+    go _ [] = return ""+    go pos (b:bs) = do+        bid <- LinearScan.blockId binfo b         let (liveIn, liveOut) =                  case LS.coq_IntMap_lookup bid ls of                      Nothing -> (LS.emptyIntSet, LS.emptyIntSet)-                     Just s  -> (LS.blockLiveIn s, LS.blockLiveOut s) in-        let allops blk = let (x, y, z) = LinearScan.blockOps binfo blk in-                         x ++ y ++ z in-        showBlock1 allops bid pos liveIn liveOut (showOps1 oinfo sd) b-            ++ go (pos + length (allops b)) bs--fromBlockInfo :: LinearScan.BlockInfo blk1 blk2 op1 op2-              -> LS.BlockInfo blk1 blk2 op1 op2-fromBlockInfo (BlockInfo a b c d) =-    LS.Build_BlockInfo a b (\blk -> let (x, y, z) = c blk in ((x, y), z)) d+                     Just s  -> (LS.blockLiveIn s, LS.blockLiveOut s)+        let allops blk =+                let (x, y, z) = LinearScan.blockOps binfo blk in+                x ++ y ++ z+        (showBlock1 allops bid pos liveIn liveOut (showOps1 oinfo sd) b ++)+            `liftM` go (pos + length (allops b)) bs -toBlockInfo :: LS.BlockInfo blk1 blk2 op1 op2-            -> LinearScan.BlockInfo blk1 blk2 op1 op2-toBlockInfo (LS.Build_BlockInfo a b c d) =-    BlockInfo a b (\blk -> let ((x, y), z) = c blk in (x, y, z)) d+fromBlockInfo :: Monad m+              => LinearScan.BlockInfo m blk1 blk2 op1 op2+              -> LS.BlockInfo (m Any) blk1 blk2 op1 op2+fromBlockInfo (BlockInfo a b c d e) =+    LS.Build_BlockInfo+        (\r1 _ k -> liftM k (a r1))+        (\r1 _ k -> liftM k (b r1))+        (\r1 r2 _ k -> liftM k (c r1 r2))+        (\blk -> let (x, y, z) = d blk in ((x, y), z)) e -data Details blk1 blk2 op1 op2 accType = Details+data Details m blk1 blk2 op1 op2 = Details     { reason          :: Maybe (LS.SSError, LS.FinalStage)     , liveSets        :: [(Int, LS.BlockLiveSets)]     , inputBlocks     :: [blk1]     , allocatedBlocks :: [blk2]-    , accumulator     :: accType     , scanStatePre    :: Maybe ScanStateDesc     , scanStatePost   :: Maybe ScanStateDesc-    , blockInfo       :: LinearScan.BlockInfo blk1 blk2 op1 op2-    , opInfo          :: LinearScan.OpInfo accType op1 op2+    , blockInfo       :: LinearScan.BlockInfo m blk1 blk2 op1 op2+    , opInfo          :: LinearScan.OpInfo m op1 op2     , loopState       :: LoopState     } -instance Show (Details blk1 blk2 op1 op2 accType) where-    show err = "Reason: " ++ show (reason err) ++ "\n\n"-               ++ ">>> ScanState before allocation:\n"-               ++ showScanStateDesc (scanStatePre err) ++ "\n"-               ++ ">>> ScanState after allocation:\n"-               ++ showScanStateDesc (scanStatePost err) ++ "\n"-               ++ ">>> " ++ show (loopState err) ++ "\n"-      where-        showScanStateDesc Nothing = ""-        showScanStateDesc (Just sd) =-            showBlocks1 (blockInfo err) (opInfo err) sd-                        (liveSets err) (inputBlocks err)-                ++ "\n" ++ show sd+showDetails :: Monad m => Details m blk1 blk2 op1 op2 -> m String+showDetails err = do+    pre  <- showScanStateDesc (scanStatePre err)+    post <- showScanStateDesc (scanStatePost err)+    return $ "Reason: " ++ show (reason err) ++ "\n\n"+          ++ ">>> ScanState before allocation:\n"+          ++ pre ++ "\n"+          ++ ">>> ScanState after allocation:\n"+          ++ post ++ "\n"+          ++ ">>> " ++ show (loopState err) ++ "\n"+  where+    showScanStateDesc Nothing = return ""+    showScanStateDesc (Just sd) =+        liftM2 (++)+            (showBlocks1 (blockInfo err) (opInfo err) sd+                         (liveSets err) (inputBlocks err))+            (return ("\n" ++ show sd))  deriving instance Show LS.SSError deriving instance Show LS.FinalStage deriving instance Show LS.BlockLiveSets -toDetails :: LS.Details blk1 blk2 op1 op2 accType-               -> Details blk1 blk2 op1 op2 accType-toDetails (LS.Build_Details a b c d e f g h i j) =-    Details a b c d e (fmap toScanStateDesc f) (fmap toScanStateDesc g)-                 (toBlockInfo h) (toOpInfo i) (toLoopState j)+toDetails :: LS.Details blk1 blk2+          -> LinearScan.BlockInfo m blk1 blk2 op1 op2+          -> LinearScan.OpInfo m op1 op2+          -> Details m blk1 blk2 op1 op2+toDetails (LS.Build_Details a b c d e f g) binfo oinfo =+    Details a b c d (fmap toScanStateDesc e) (fmap toScanStateDesc f)+            binfo oinfo (toLoopState g)  -- | Transform a list of basic blocks containing variable references, into an --   equivalent list where each reference is associated with a register@@ -364,49 +374,57 @@ --   If allocation is found to be impossible -- for example if there are --   simply not enough registers -- a 'Left' value is returned, with a string --   describing the error.-allocate :: Int                  -- ^ Maximum number of registers to use-         -> LinearScan.BlockInfo blk1 blk2 op1 op2-         -> LinearScan.OpInfo accType op1 op2-         -> [blk1]-         -> State accType (Either String [blk2])+allocate :: forall m blk1 blk2 op1 op2. (Functor m, Applicative m, Monad m)+         => 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"-allocate maxReg (fromBlockInfo -> binfo) (fromOpInfo -> oinfo) blocks = do-    res <- gets (LS.linearScan maxReg binfo oinfo blocks)-    let res' = toDetails res-    put $ accumulator res'-    case reason res' of-        Just (err, _) -> reportError res' err-        Nothing ->-            -- tracer (show res') $-            return $ Right (allocatedBlocks res')+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+        Nothing       -> Right $ allocatedBlocks res'   where-    -- reportError res err =-    --     return $ Left $ tracer (show res) $ reasonToStr err-    reportError _res err =-        return $ Left $ reasonToStr err+    dict :: LS.Monad (m Any)+    dict = LS.Build_Monad+        (LS.Build_Applicative+         (\(_ :: ()) (_ :: ()) (f :: Any -> Any) x ->+           U.unsafeCoerce (fmap f (U.unsafeCoerce x :: m Any)))+         (\(_ :: ()) -> pure)+         (\(_ :: ()) (_ :: ()) f x ->+           U.unsafeCoerce (U.unsafeCoerce f <*> U.unsafeCoerce x :: m Any)))+        (\(_ :: ()) x ->+          U.unsafeCoerce (join (U.unsafeCoerce x :: m (m Any)) :: m Any))      reasonToStr r = case r of-        LS.ERegistersExhausted _ ->-            "No registers available for allocation"-        LS.ENoValidSplitPositionUnh xid splitPos ->-            "No split position could be found for unhandled interval "-                ++ show xid ++ " @ " ++ show splitPos-        LS.ENoValidSplitPosition xid splitPos ->-            "No split position could be found for " ++ show xid+        LS.ECannotInsertUnhAtPos spillDets pos ->+            "Cannot insert interval " ++ show spillDets+              ++ " onto unhandled list (use at position "+              ++ show pos ++ ")"+        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.ECannotSplitSingleton1 n ->-            "Current interval is a singleton (err#1) (" ++ show n ++ ")"-        LS.ECannotSplitSingleton2 n ->-            "Current interval is a singleton (err#2) (" ++ show n ++ ")"-        LS.ECannotSplitSingleton3 n ->-            "Current interval is a singleton (err#3) (" ++ show n ++ ")"-        LS.ENoIntervalsToSplit ->-            "There are no intervals to split"-        LS.ERegisterAlreadyAssigned n ->-            "Register is already assigned (" ++ show n ++ ")"-        LS.ERegisterAssignmentsOverlap n ->-            "Register assignments overlap (" ++ show n ++ ")"-        LS.EFuelExhausted -> "Fuel was exhausted"+        LS.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.ERegisterAlreadyAssigned reg ->+            "Register " ++ show reg ++ " already assigned"+        LS.ERegisterAssignmentsOverlap reg ->+            "Register assignments overlap at " ++ show reg         LS.EUnexpectedNoMoreUnhandled ->             "The unexpected happened: no more unhandled intervals"+        LS.ECannotSpillIfRegisterRequired i ->+            "Cannot spill interval " ++ show i+                ++ " with use positions requiring registers"+        LS.EFuelExhausted -> "Fuel was exhausted"+        LS.ENotYetImplemented n -> "Not Yet Implemented (#" ++ show n ++ ")"

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Allocate where@@ -30,13 +30,21 @@   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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 @@ -138,7 +146,9 @@                Prelude.True -> success;                Prelude.False ->                 Morph.stbind (\x -> success)-                  (Split.splitCurrentInterval maxReg pre (Split.BeforePos n))})};+                  (Split.splitCurrentInterval maxReg pre (Morph.BeforePos n+                    (Morph.AvailableForPart+                    ( (Prelude.fst (Cursor.curId maxReg sd))))))})};           Prelude.Nothing -> Prelude.Just success})})  allocateBlockedReg :: Prelude.Int -> ScanState.ScanStateDesc -> Morph.SState@@ -154,8 +164,9 @@        (,) int r ->         let {          atPos = \u ->-          Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos)-            (unsafeCoerce (UsePos.uloc u))}+          (Prelude.&&)+            (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos)+              (unsafeCoerce (UsePos.uloc u))) (UsePos.regReq u)}         in         let {          pos' = case Interval.findIntervalUsePos ( int) atPos of {@@ -214,13 +225,8 @@                   Interval.intervalEnd ( (Cursor.curIntDetails maxReg sd))});             Prelude.Nothing -> Prelude.False} of {        Prelude.True ->-        let {-         p = Interval.firstUseReqRegOrEnd ( (Cursor.curIntDetails maxReg sd))}-        in-        Morph.stbind (\x ->-          Morph.stbind (\x0 -> Morph.return_ Prelude.Nothing)-            (Morph.moveUnhandledToHandled maxReg pre))-          (Split.splitCurrentInterval maxReg pre (Split.BeforePos p));+        Morph.stbind (\x -> Morph.return_ Prelude.Nothing)+          (Split.spillCurrentInterval maxReg pre);        Prelude.False ->         Morph.stbind (\x ->           Morph.stbind (\x0 ->@@ -230,7 +236,8 @@                   (Morph.moveUnhandledToActive maxReg pre reg))                 (case mloc of {                   Prelude.Just n ->-                   Split.splitCurrentInterval maxReg pre (Split.BeforePos 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))@@ -262,7 +269,8 @@            (              (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)                (ScanState.intervals maxReg z) (Prelude.fst x))))) pos of {-   Prelude.True -> Morph.moveActiveToHandled maxReg z (unsafeCoerce x);+   Prelude.True ->+    Morph.moveActiveToHandled maxReg z Prelude.False (unsafeCoerce x);    Prelude.False ->     case Prelude.not            (Interval.posWithinInterval@@ -325,7 +333,8 @@                (ScanState.intervals maxReg z) (Prelude.fst x))))) pos of {    Prelude.True ->     let {-     filtered_var = Morph.moveInactiveToHandled maxReg z (unsafeCoerce x)}+     filtered_var = Morph.moveInactiveToHandled maxReg z Prelude.False+                      (unsafeCoerce x)}     in     f filtered_var;    Prelude.False ->@@ -451,4 +460,27 @@      Prelude.Nothing -> Prelude.Right       (ScanState.packScanState maxReg ScanState.InUse sd)})     positions++data Allocation =+   Build_Allocation Prelude.Int Interval.IntervalDesc (Prelude.Maybe PhysReg)++intVal :: Prelude.Int -> Allocation -> Interval.IntervalDesc+intVal maxReg a =+  case a of {+   Build_Allocation intId intVal0 intReg0 -> intVal0}++intReg :: Prelude.Int -> Allocation -> Prelude.Maybe PhysReg+intReg maxReg a =+  case a of {+   Build_Allocation intId intVal0 intReg0 -> intReg0}++determineAllocations :: Prelude.Int -> ScanState.ScanStateDesc -> []+                        Allocation+determineAllocations maxReg sd =+  Prelude.map (\x -> Build_Allocation ( (Prelude.fst x))+    (Interval.getIntervalDesc+      (+        (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)+          (ScanState.intervals maxReg sd) (Prelude.fst x)))) (Prelude.snd x))+    (ScanState.handled maxReg sd) 

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Assign where@@ -13,15 +13,18 @@ import qualified Data.Functor.Identity import qualified LinearScan.Utils +import qualified LinearScan.Allocate as Allocate import qualified LinearScan.Blocks as Blocks import qualified LinearScan.Graph as Graph import qualified LinearScan.IntMap as IntMap import qualified LinearScan.Interval as Interval+import qualified LinearScan.Lens as Lens import qualified LinearScan.Lib as Lib import qualified LinearScan.LiveSets as LiveSets+import qualified LinearScan.Monad as Monad import qualified LinearScan.Resolve as Resolve-import qualified LinearScan.State as State import qualified LinearScan.UsePos as UsePos+import qualified LinearScan.Yoneda as Yoneda import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Fintype as Fintype import qualified LinearScan.Seq as Seq@@ -29,88 +32,151 @@   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+import qualified GHC.Prim as GHC.Prim #else -- HUGS import qualified LinearScan.IOExts as IOExts+#endif+++#ifdef __GLASGOW_HASKELL__+--unsafeCoerce :: a -> b+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+--unsafeCoerce :: a -> b unsafeCoerce = IOExts.unsafeCoerce #endif  type PhysReg = Prelude.Int -data AssnStateInfo accType =-   Build_AssnStateInfo Blocks.OpId Blocks.OpId Blocks.OpId accType+data AllocState =+   Build_AllocState ([] (Prelude.Maybe Prelude.Int)) (IntMap.IntMap+                                                     (Prelude.Maybe PhysReg)) -assnOpId :: (AssnStateInfo a1) -> Blocks.OpId-assnOpId a =+newAllocState :: Prelude.Int -> AllocState+newAllocState maxReg =+  Build_AllocState (Data.List.replicate maxReg Prelude.Nothing)+    IntMap.emptyIntMap++data AllocError =+   Build_AllocError Prelude.Int (Prelude.Maybe PhysReg) (Prelude.Maybe+                                                        PhysReg) Blocks.BlockId++data AssnStateInfo =+   Build_AssnStateInfo Blocks.OpId Blocks.OpId Blocks.OpId AllocState + (IntMap.IntMap AllocState) (IntMap.IntMap AllocState) ([] AllocError)++assnOpId :: Prelude.Int -> AssnStateInfo -> Blocks.OpId+assnOpId maxReg a =   case a of {-   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAcc0 ->-    assnOpId0}+   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0+    assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 -> assnOpId0} -assnBlockBeg :: (AssnStateInfo a1) -> Blocks.OpId-assnBlockBeg a =+assnBlockBeg :: Prelude.Int -> AssnStateInfo -> Blocks.OpId+assnBlockBeg maxReg a =   case a of {-   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAcc0 ->-    assnBlockBeg0}+   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0+    assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 -> assnBlockBeg0} -assnBlockEnd :: (AssnStateInfo a1) -> Blocks.OpId-assnBlockEnd a =+assnBlockEnd :: Prelude.Int -> AssnStateInfo -> Blocks.OpId+assnBlockEnd maxReg a =   case a of {-   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAcc0 ->-    assnBlockEnd0}+   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0+    assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 -> assnBlockEnd0} -assnAcc :: (AssnStateInfo a1) -> a1-assnAcc a =+assnAllocState :: Prelude.Int -> AssnStateInfo -> AllocState+assnAllocState maxReg a =   case a of {-   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAcc0 ->-    assnAcc0}+   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0+    assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 -> assnAllocState0} -type AssnState accType a = State.State (AssnStateInfo accType) a+assnBlockEntryAllocs :: Prelude.Int -> AssnStateInfo -> IntMap.IntMap+                        AllocState+assnBlockEntryAllocs maxReg a =+  case a of {+   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0+    assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 ->+    assnBlockEntryAllocs0} -swapOpM :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Blocks.PhysReg ->-           Blocks.PhysReg -> AssnState a3 ([] a2)-swapOpM maxReg oinfo sreg dreg =-  State.bind (\assn ->-    case Blocks.swapOp maxReg oinfo sreg dreg (assnAcc assn) of {-     (,) mop acc' ->-      State.bind (\x -> State.pure mop)-        (State.put (Build_AssnStateInfo (assnOpId assn) (assnBlockBeg assn)-          (assnBlockEnd assn) acc'))}) State.get+assnBlockExitAllocs :: Prelude.Int -> AssnStateInfo -> IntMap.IntMap+                       AllocState+assnBlockExitAllocs maxReg a =+  case a of {+   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0+    assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 ->+    assnBlockExitAllocs0} -moveOpM :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Blocks.PhysReg ->-           Blocks.PhysReg -> AssnState a3 ([] a2)-moveOpM maxReg oinfo sreg dreg =-  State.bind (\assn ->-    case Blocks.moveOp maxReg oinfo sreg dreg (assnAcc assn) of {-     (,) mop acc' ->-      State.bind (\x -> State.pure mop)-        (State.put (Build_AssnStateInfo (assnOpId assn) (assnBlockBeg assn)-          (assnBlockEnd assn) acc'))}) State.get+assnErrors :: Prelude.Int -> AssnStateInfo -> [] AllocError+assnErrors maxReg a =+  case a of {+   Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0+    assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 -> assnErrors0} -saveOpM :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Blocks.PhysReg ->-           (Prelude.Maybe Blocks.VarId) -> AssnState a3 ([] a2)-saveOpM maxReg oinfo vid reg =-  State.bind (\assn ->-    case Blocks.saveOp maxReg oinfo vid reg (assnAcc assn) of {-     (,) sop acc' ->-      State.bind (\x -> State.pure sop)-        (State.put (Build_AssnStateInfo (assnOpId assn) (assnBlockBeg assn)-          (assnBlockEnd assn) acc'))}) State.get+newAssnStateInfo :: Prelude.Int -> AssnStateInfo+newAssnStateInfo maxReg =+  Build_AssnStateInfo ((Prelude.succ) 0) ((Prelude.succ) 0) ((Prelude.succ)+    0) (newAllocState maxReg) IntMap.emptyIntMap IntMap.emptyIntMap [] -restoreOpM :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> (Prelude.Maybe-              Blocks.VarId) -> Blocks.PhysReg -> AssnState a3 ([] a2)-restoreOpM maxReg oinfo vid reg =-  State.bind (\assn ->-    case Blocks.restoreOp maxReg oinfo vid reg (assnAcc assn) of {-     (,) rop acc' ->-      State.bind (\x -> State.pure rop)-        (State.put (Build_AssnStateInfo (assnOpId assn) (assnBlockBeg assn)-          (assnBlockEnd assn) acc'))}) State.get+_assnOpId :: Prelude.Int -> (Monad.Functor a1) -> (Blocks.OpId -> a1) ->+             AssnStateInfo -> a1+_assnOpId maxReg h f s =+  Monad.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)) -varAllocs :: Prelude.Int -> Prelude.Int -> ([] Resolve.Allocation) ->+_assnBlockBeg :: Prelude.Int -> (Monad.Functor a1) -> (Blocks.OpId -> a1) ->+                 AssnStateInfo -> a1+_assnBlockBeg maxReg h f s =+  Monad.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 maxReg h f s =+  Monad.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++generateMoves :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo a3 +                 a1 a2) -> ([] Resolve.ResolvingMove) -> a3+generateMoves maxReg mDict oinfo moves =+  Monad.forFoldrM mDict [] moves (\mv acc ->+    let {+     k = (Prelude..)+           (Monad.fmap (Monad.is_functor (Monad.is_applicative mDict)) (\x ->+             Prelude.Just x))+           (Yoneda.iso_to+             (Yoneda.coq_Yoneda_lemma+               (Monad.is_functor (Monad.is_applicative mDict))))}+    in+    Monad.bind mDict (\mops ->+      Monad.pure (Monad.is_applicative mDict)+        (case mops of {+          Prelude.Just ops -> (Prelude.++) ops acc;+          Prelude.Nothing -> acc}))+      (case mv of {+        Resolve.Move sreg dreg ->+         k (\_ -> Blocks.moveOp maxReg mDict oinfo sreg dreg);+        Resolve.Swap sreg dreg ->+         k (\_ -> Blocks.swapOp maxReg mDict oinfo sreg dreg);+        Resolve.Spill sreg vid ->+         k (\_ -> Blocks.saveOp maxReg mDict oinfo sreg (Prelude.Just vid));+        Resolve.Restore vid dreg ->+         k (\_ ->+           Blocks.restoreOp maxReg mDict oinfo (Prelude.Just vid) dreg);+        Resolve.Nop ->+         Monad.pure (Monad.is_applicative mDict) Prelude.Nothing}))++varAllocs :: Prelude.Int -> Prelude.Int -> ([] Allocate.Allocation) ->              Blocks.VarInfo -> [] ((,) Blocks.VarId PhysReg) varAllocs maxReg opid allocs v =   case Blocks.varId maxReg v of {@@ -118,9 +184,9 @@    Prelude.Right vid ->     Prelude.map (\x -> (,) vid x)       (Lib.catMaybes-        (Prelude.map (\i -> Resolve.intReg maxReg i)+        (Prelude.map (\i -> Allocate.intReg maxReg i)           (Prelude.filter (\i ->-            let {int = Resolve.intVal maxReg i} in+            let {int = Allocate.intVal maxReg i} in             (Prelude.&&)               (Eqtype.eq_op Ssrnat.nat_eqType                 (unsafeCoerce (Interval.ivar int)) (unsafeCoerce vid))@@ -130,127 +196,135 @@                   _ -> (Prelude.<=) ((Prelude.succ) opid) (Interval.iend int)})))             allocs)))} -generateMoves :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> ([]-                 Resolve.ResolvingMove) -> AssnState a3 ([] a2)-generateMoves maxReg oinfo moves =-  State.forFoldrM [] moves (\mv acc ->-    State.bind (\mops ->-      State.pure-        (case mops of {-          Prelude.Just ops -> (Prelude.++) ops acc;-          Prelude.Nothing -> acc}))-      (case mv of {-        Resolve.Move sreg dreg ->-         State.fmap (\x -> Prelude.Just x) (moveOpM maxReg oinfo sreg dreg);-        Resolve.Swap sreg dreg ->-         State.fmap (\x -> Prelude.Just x) (swapOpM maxReg oinfo sreg dreg);-        Resolve.Spill sreg vid ->-         State.fmap (\x -> Prelude.Just x)-           (saveOpM maxReg oinfo sreg (Prelude.Just vid));-        Resolve.Restore vid dreg ->-         State.fmap (\x -> Prelude.Just x)-           (restoreOpM maxReg oinfo (Prelude.Just vid) dreg);-        Resolve.Nop -> State.pure Prelude.Nothing}))--doAllocations :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> ([]-                 Resolve.Allocation) -> a1 -> AssnState a3 ([] a2)-doAllocations maxReg oinfo allocs op =-  State.bind (\assn ->-    let {opid = assnOpId assn} in-    let {vars = Blocks.opRefs maxReg oinfo op} in+setAllocations :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo a3 +                  a1 a2) -> ([] Allocate.Allocation) -> a1 -> AssnState +                  a3 ([] a2)+setAllocations maxReg mDict oinfo allocs op =+  Monad.bind (Monad.coq_StateT_Monad mDict) (\assn ->+    let {opid = assnOpId maxReg assn} in+    let {vars = Blocks.opRefs maxReg mDict oinfo op} in     let {-     regs = State.concat (Prelude.map (varAllocs maxReg opid allocs) vars)}+     regs = Monad.concat (Prelude.map (varAllocs maxReg opid allocs) vars)}     in-    let {ops = Blocks.applyAllocs maxReg oinfo op regs} in-    State.bind (\transitions ->-      State.bind (\x -> State.pure ((Prelude.++) ops transitions))-        (State.modify (\assn' -> Build_AssnStateInfo ((Prelude.succ)-          ((Prelude.succ) opid)) (assnBlockBeg assn') (assnBlockEnd assn')-          (assnAcc assn'))))-      (case (Prelude.&&) ((Prelude.<=) (assnBlockBeg assn) opid)-              ((Prelude.<=) ((Prelude.succ) opid) (assnBlockEnd assn)) of {-        Prelude.True ->-         generateMoves maxReg oinfo-           (Resolve.determineMoves maxReg-             (Resolve.resolvingMoves maxReg allocs opid ((Prelude.succ)-               ((Prelude.succ) opid))));-        Prelude.False -> State.pure []})) State.get+    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)+            ((Prelude.++) ops transitions))+          (Monad.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+             (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+          (Yoneda.coq_Yoneda_lemma+            (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->+          Blocks.applyAllocs maxReg mDict oinfo op regs))))+    (Monad.getT (Monad.is_applicative mDict)) -resolveMappings :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Prelude.Int ->-                   ([] a2) -> (IntMap.IntMap ((,) Graph.Graph Graph.Graph))-                   -> AssnState a3 ([] a2)-resolveMappings maxReg oinfo bid opsm mappings =+resolveMappings :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo +                   a3 a1 a2) -> Prelude.Int -> ([] a2) -> (IntMap.IntMap+                   ((,) Graph.Graph Graph.Graph)) -> a3+resolveMappings maxReg mDict oinfo bid opsm mappings =   case IntMap.coq_IntMap_lookup bid mappings of {    Prelude.Just graphs ->     case graphs of {      (,) gbeg gend ->-      State.bind (\bmoves ->-        let {opsm' = (Prelude.++) bmoves opsm} in-        State.bind (\emoves ->-          let {opsm'' = (Prelude.++) opsm' emoves} in State.pure opsm'')-          (generateMoves maxReg oinfo+      Monad.bind mDict (\bmoves ->+        Monad.bind mDict (\emoves ->+          Monad.pure (Monad.is_applicative mDict)+            ((Prelude.++) bmoves ((Prelude.++) opsm emoves)))+          (generateMoves maxReg mDict oinfo             (Prelude.map (Resolve.moveFromGraph maxReg)               (Graph.topsort                 (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)                   Ssrnat.nat_eqType) gend))))-        (generateMoves maxReg oinfo+        (generateMoves maxReg mDict oinfo           (Prelude.map (Resolve.moveFromGraph maxReg)             (Graph.topsort               (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)                 Ssrnat.nat_eqType) gbeg)))};-   Prelude.Nothing -> State.pure opsm}+   Prelude.Nothing -> Monad.pure (Monad.is_applicative mDict) opsm} -considerOps :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->-               (Blocks.OpInfo a5 a3 a4) -> (a3 -> AssnState a5 ([] a4)) ->-               (IntMap.IntMap LiveSets.BlockLiveSets) -> (IntMap.IntMap-               ((,) Graph.Graph Graph.Graph)) -> ([] a1) -> State.State-               (AssnStateInfo a5) ([] a2)-considerOps maxReg binfo oinfo f liveSets mappings =-  State.mapM (\blk ->-    let {ops = Blocks.blockOps binfo blk} in-    let {bid = Blocks.blockId binfo blk} in-    case ops of {+considerOps :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 +               a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([]+               Allocate.Allocation) -> (IntMap.IntMap LiveSets.BlockLiveSets)+               -> (IntMap.IntMap Resolve.BlockMoves) -> ([] a1) -> AssnState+               a5 ([] a2)+considerOps maxReg mDict binfo oinfo allocs liveSets mappings =+  Monad.mapM (Monad.coq_StateT_Applicative mDict) (\blk ->+    case Blocks.blockOps mDict binfo blk of {      (,) p opse ->       case p of {        (,) opsb opsm ->-        State.bind (\x ->-          State.bind (\opsb' ->-            State.bind (\opsm' ->-              State.bind (\opse' ->-                State.bind (\opsm'' ->-                  case opsb' of {-                   [] ->-                    State.pure-                      (Blocks.setBlockOps binfo blk opsb' opsm'' opse');-                   (:) b bs ->-                    case opse' of {+        Monad.bind (Monad.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'' ->+                    case opsb' of {                      [] ->-                      State.pure-                        (Blocks.setBlockOps binfo blk opsb' opsm'' opse');-                     (:) e es ->-                      State.pure-                        (Blocks.setBlockOps binfo blk ((:) b [])-                          ((Prelude.++) bs-                            ((Prelude.++) opsm'' (Seq.belast e es))) ((:)-                          (Seq.last e es) []))}})-                  (resolveMappings maxReg oinfo bid opsm' mappings))-                (State.concatMapM f opse)) (State.concatMapM f opsm))-            (State.concatMapM f opsb))-          (State.modify (\assn -> Build_AssnStateInfo (assnOpId assn)-            ((Prelude.+) (assnOpId assn)-              (Ssrnat.double (Data.List.length opsb)))-            ((Prelude.+) (assnOpId assn)-              (Ssrnat.double-                ((Prelude.+) (Data.List.length opsb) (Data.List.length opsm))))-            (assnAcc assn)))}})+                      case opse' of {+                       [] ->+                        Monad.pure (Monad.coq_StateT_Applicative mDict)+                          (Blocks.setBlockOps mDict binfo blk [] opsm'' []);+                       (:) e es ->+                        Monad.pure (Monad.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)+                          (Blocks.setBlockOps mDict binfo blk ((:) b [])+                            ((Prelude.++) bs opsm'') []);+                       (:) e es ->+                        Monad.pure (Monad.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+                      (resolveMappings maxReg mDict oinfo bid opsm' mappings)))+                  (Monad.lift mDict+                    (Yoneda.iso_to+                      (Yoneda.coq_Yoneda_lemma+                        (Monad.is_functor (Monad.is_applicative mDict)))+                      (\_ -> Blocks.blockId mDict binfo blk))))+                (Monad.concatMapM (Monad.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 ->+            let {opid = Lens.view (\_ -> _assnOpId maxReg) assn} in+            Lens.set (\_ -> _assnBlockEnd maxReg)+              ((Prelude.+) opid+                (Ssrnat.double+                  ((Prelude.+) (Data.List.length opsb)+                    (Data.List.length opsm))))+              (Lens.set (\_ -> _assnBlockBeg maxReg)+                ((Prelude.+) opid (Ssrnat.double (Data.List.length opsb)))+                assn)))}}) -assignRegNum :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->-                (Blocks.OpInfo a5 a3 a4) -> ([] Resolve.Allocation) ->-                (IntMap.IntMap LiveSets.BlockLiveSets) -> (IntMap.IntMap-                Resolve.BlockMoves) -> ([] a1) -> a5 -> (,) ([] a2) a5-assignRegNum maxReg binfo oinfo allocs liveSets mappings blocks acc =-  case considerOps maxReg binfo oinfo (doAllocations maxReg oinfo allocs)-         liveSets mappings blocks (Build_AssnStateInfo ((Prelude.succ) 0)-         ((Prelude.succ) 0) ((Prelude.succ) 0) acc) of {-   (,) blocks' assn -> (,) blocks' (assnAcc assn)}+assignRegNum :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo +                a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([]+                Allocate.Allocation) -> (IntMap.IntMap+                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+    (considerOps maxReg mDict binfo oinfo allocs liveSets mappings blocks+      (newAssnStateInfo maxReg)) 

@@ -1,3 +1,6 @@+{-# OPTIONS_GHC -cpp -XMagicHash #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}+ module LinearScan.Blocks where  @@ -10,9 +13,33 @@ import qualified Data.Functor.Identity import qualified LinearScan.Utils +import qualified LinearScan.Monad as Monad import qualified LinearScan.UsePos as UsePos+import qualified LinearScan.Yoneda as Yoneda  ++#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  type VarId = Prelude.Int@@ -48,73 +75,83 @@  type OpId = Prelude.Int -data OpInfo accType opType1 opType2 =+data OpInfo m opType1 opType2 =    Build_OpInfo (opType1 -> OpKind) (opType1 -> [] VarInfo) (PhysReg ->                                                             PhysReg ->-                                                            accType -> (,)-                                                            ([] opType2)-                                                            accType) - (PhysReg -> PhysReg -> accType -> (,) ([] opType2) accType) (PhysReg ->-                                                             (Prelude.Maybe-                                                             VarId) ->-                                                             accType -> (,)-                                                             ([] opType2)-                                                             accType) - ((Prelude.Maybe VarId) -> PhysReg -> accType -> (,) ([] opType2) accType) - (opType1 -> ([] ((,) VarId PhysReg)) -> [] opType2) (opType1 ->-                                                     Prelude.String)+                                                            Yoneda.Yoneda +                                                            m ([] opType2)) + (PhysReg -> PhysReg -> Yoneda.Yoneda m ([] opType2)) (PhysReg ->+                                                      (Prelude.Maybe +                                                      VarId) -> Yoneda.Yoneda+                                                      m ([] opType2)) + ((Prelude.Maybe VarId) -> PhysReg -> Yoneda.Yoneda m ([] opType2)) (opType1+                                                                    -> ([]+                                                                    ((,)+                                                                    VarId+                                                                    PhysReg))+                                                                    ->+                                                                    Yoneda.Yoneda+                                                                    m+                                                                    ([]+                                                                    opType2)) + (opType1 -> Prelude.String) -opKind :: Prelude.Int -> (OpInfo a1 a2 a3) -> a2 -> OpKind-opKind maxReg o =+opKind :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> a2 ->+          OpKind+opKind maxReg h o =   case o of {    Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0     applyAllocs0 showOp -> opKind0} -opRefs :: Prelude.Int -> (OpInfo a1 a2 a3) -> a2 -> [] VarInfo-opRefs maxReg o =+opRefs :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> a2 -> []+          VarInfo+opRefs maxReg h o =   case o of {    Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0     applyAllocs0 showOp -> opRefs0} -moveOp :: Prelude.Int -> (OpInfo a1 a2 a3) -> PhysReg -> PhysReg -> a1 -> (,)-          ([] a3) a1-moveOp maxReg o =+moveOp :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> PhysReg ->+          PhysReg -> (([] a3) -> a4) -> a1+moveOp maxReg h o x x0 x1 =   case o of {    Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0-    applyAllocs0 showOp -> moveOp0}+    applyAllocs0 showOp -> unsafeCoerce moveOp0 x x0 __ x1} -swapOp :: Prelude.Int -> (OpInfo a1 a2 a3) -> PhysReg -> PhysReg -> a1 -> (,)-          ([] a3) a1-swapOp maxReg o =+swapOp :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> PhysReg ->+          PhysReg -> (([] a3) -> a4) -> a1+swapOp maxReg h o x x0 x1 =   case o of {    Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0-    applyAllocs0 showOp -> swapOp0}+    applyAllocs0 showOp -> unsafeCoerce swapOp0 x x0 __ x1} -saveOp :: Prelude.Int -> (OpInfo a1 a2 a3) -> PhysReg -> (Prelude.Maybe-          VarId) -> a1 -> (,) ([] a3) a1-saveOp maxReg o =+saveOp :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> PhysReg ->+          (Prelude.Maybe VarId) -> (([] a3) -> a4) -> a1+saveOp maxReg h o x x0 x1 =   case o of {    Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0-    applyAllocs0 showOp -> saveOp0}+    applyAllocs0 showOp -> unsafeCoerce saveOp0 x x0 __ x1} -restoreOp :: Prelude.Int -> (OpInfo a1 a2 a3) -> (Prelude.Maybe VarId) ->-             PhysReg -> a1 -> (,) ([] a3) a1-restoreOp maxReg o =+restoreOp :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) ->+             (Prelude.Maybe VarId) -> PhysReg -> (([] a3) -> a4) -> a1+restoreOp maxReg h o x x0 x1 =   case o of {    Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0-    applyAllocs0 showOp -> restoreOp0}+    applyAllocs0 showOp -> unsafeCoerce restoreOp0 x x0 __ x1} -applyAllocs :: Prelude.Int -> (OpInfo a1 a2 a3) -> a2 -> ([]-               ((,) VarId PhysReg)) -> [] a3-applyAllocs maxReg o =+applyAllocs :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> a2 ->+               ([] ((,) VarId PhysReg)) -> (([] a3) -> a4) -> a1+applyAllocs maxReg h o x x0 x1 =   case o of {    Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0-    applyAllocs0 showOp -> applyAllocs0}+    applyAllocs0 showOp -> unsafeCoerce applyAllocs0 x x0 __ x1}  type BlockId = Prelude.Int -data BlockInfo blockType1 blockType2 opType1 opType2 =-   Build_BlockInfo (blockType1 -> BlockId) (blockType1 -> [] BlockId) +data BlockInfo m blockType1 blockType2 opType1 opType2 =+   Build_BlockInfo (blockType1 -> Yoneda.Yoneda m BlockId) (blockType1 ->+                                                           Yoneda.Yoneda +                                                           m ([] BlockId)) + (blockType1 -> blockType1 -> Yoneda.Yoneda m ((,) blockType1 blockType1))   (blockType1 -> (,) ((,) ([] opType1) ([] opType1)) ([] opType1)) (blockType1                                                                   -> ([]                                                                   opType2) ->@@ -124,49 +161,61 @@                                                                   opType2) ->                                                                   blockType2) -blockId :: (BlockInfo a1 a2 a3 a4) -> a1 -> BlockId-blockId b =+blockId :: (Monad.Monad a1) -> (BlockInfo a1 a2 a3 a4 a5) -> a2 -> (BlockId+           -> a6) -> a1+blockId h b x x0 =   case b of {-   Build_BlockInfo blockId0 blockSuccessors0 blockOps0 setBlockOps0 ->-    blockId0}+   Build_BlockInfo blockId0 blockSuccessors0 splitCriticalEdge0 blockOps0+    setBlockOps0 -> unsafeCoerce blockId0 x __ x0} -blockSuccessors :: (BlockInfo a1 a2 a3 a4) -> a1 -> [] BlockId-blockSuccessors b =+blockSuccessors :: (Monad.Monad a1) -> (BlockInfo a1 a2 a3 a4 a5) -> a2 ->+                   (([] BlockId) -> a6) -> a1+blockSuccessors h b x x0 =   case b of {-   Build_BlockInfo blockId0 blockSuccessors0 blockOps0 setBlockOps0 ->-    blockSuccessors0}+   Build_BlockInfo blockId0 blockSuccessors0 splitCriticalEdge0 blockOps0+    setBlockOps0 -> unsafeCoerce blockSuccessors0 x __ x0} -blockOps :: (BlockInfo a1 a2 a3 a4) -> a1 -> (,) ((,) ([] a3) ([] a3))-            ([] a3)-blockOps b =+splitCriticalEdge :: (Monad.Monad a1) -> (BlockInfo a1 a2 a3 a4 a5) -> a2 ->+                     a2 -> (((,) a2 a2) -> a6) -> a1+splitCriticalEdge h b x x0 x1 =   case b of {-   Build_BlockInfo blockId0 blockSuccessors0 blockOps0 setBlockOps0 ->-    blockOps0}+   Build_BlockInfo blockId0 blockSuccessors0 splitCriticalEdge0 blockOps0+    setBlockOps0 -> unsafeCoerce splitCriticalEdge0 x x0 __ x1} -setBlockOps :: (BlockInfo a1 a2 a3 a4) -> a1 -> ([] a4) -> ([] a4) -> ([] -               a4) -> a2-setBlockOps b =+blockOps :: (Monad.Monad a1) -> (BlockInfo a1 a2 a3 a4 a5) -> a2 -> (,)+            ((,) ([] a4) ([] a4)) ([] a4)+blockOps h b =   case b of {-   Build_BlockInfo blockId0 blockSuccessors0 blockOps0 setBlockOps0 ->-    setBlockOps0}+   Build_BlockInfo blockId0 blockSuccessors0 splitCriticalEdge0 blockOps0+    setBlockOps0 -> blockOps0} -allBlockOps :: (BlockInfo a1 a2 a3 a4) -> a1 -> [] a3-allBlockOps binfo block =-  case blockOps binfo block of {+setBlockOps :: (Monad.Monad a1) -> (BlockInfo a1 a2 a3 a4 a5) -> a2 -> ([]+               a5) -> ([] a5) -> ([] a5) -> a3+setBlockOps h b =+  case b of {+   Build_BlockInfo blockId0 blockSuccessors0 splitCriticalEdge0 blockOps0+    setBlockOps0 -> setBlockOps0}++allBlockOps :: (Monad.Monad a5) -> (BlockInfo a5 a1 a2 a3 a4) -> a1 -> [] a3+allBlockOps mDict binfo block =+  case blockOps mDict binfo block of {    (,) p c ->     case p of {      (,) a b -> (Prelude.++) a ((Prelude.++) b c)}} -blockSize :: (BlockInfo a1 a2 a3 a4) -> a1 -> Prelude.Int-blockSize binfo block =-  Data.List.length (allBlockOps binfo block)+blockSize :: (Monad.Monad a5) -> (BlockInfo a5 a1 a2 a3 a4) -> a1 ->+             Prelude.Int+blockSize mDict binfo block =+  Data.List.length (allBlockOps mDict binfo block) -foldOps :: (BlockInfo a1 a2 a3 a4) -> (a5 -> a3 -> a5) -> a5 -> ([] a1) -> a5-foldOps binfo f z =+foldOps :: (Monad.Monad a5) -> (BlockInfo a5 a1 a2 a3 a4) -> (a6 -> a3 -> a6)+           -> a6 -> ([] a1) -> a6+foldOps mDict binfo f z =   Data.List.foldl' (\bacc blk ->-    Data.List.foldl' f bacc (allBlockOps binfo blk)) z+    Data.List.foldl' f bacc (allBlockOps mDict binfo blk)) z -countOps :: (BlockInfo a1 a2 a3 a4) -> ([] a1) -> Prelude.Int-countOps binfo =-  foldOps binfo (\acc x -> (Prelude.succ) acc) 0+countOps :: (Monad.Monad a5) -> (BlockInfo a5 a1 a2 a3 a4) -> ([] a1) ->+            Prelude.Int+countOps mDict binfo =+  foldOps mDict binfo (\acc x -> (Prelude.succ) acc) 0 

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Build where@@ -21,12 +21,13 @@ import qualified LinearScan.LiveSets as LiveSets import qualified LinearScan.Logic as Logic import qualified LinearScan.Loops as Loops-import qualified LinearScan.Morph as Morph+import qualified LinearScan.Monad as Monad import qualified LinearScan.NonEmpty0 as NonEmpty0 import qualified LinearScan.Range as Range import qualified LinearScan.ScanState as ScanState import qualified LinearScan.Specif as Specif import qualified LinearScan.UsePos as UsePos+import qualified LinearScan.Yoneda as Yoneda import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Fintype as Fintype import qualified LinearScan.Seq as Seq@@ -36,13 +37,21 @@   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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 @@ -365,13 +374,13 @@     (handleVars_onlyVars maxReg b pos e) (handleVars_onlyRanges b pos e) vars     ranges -reduceOp :: Prelude.Int -> (Blocks.OpInfo a4 a2 a3) -> Prelude.Int ->-            Prelude.Int -> Prelude.Int -> a1 -> a2 -> (IntMap.IntMap-            PendingRanges) -> IntMap.IntMap PendingRanges-reduceOp maxReg oinfo b pos e block op ranges =-  let {refs = Blocks.opRefs maxReg oinfo op} in+reduceOp :: Prelude.Int -> (Monad.Monad a4) -> (Blocks.OpInfo a4 a2 a3) ->+            Prelude.Int -> Prelude.Int -> Prelude.Int -> a1 -> a2 ->+            (IntMap.IntMap PendingRanges) -> IntMap.IntMap PendingRanges+reduceOp maxReg mDict oinfo b pos e block op ranges =+  let {refs = Blocks.opRefs maxReg mDict oinfo op} in   let {-   refs' = case Blocks.opKind maxReg oinfo op of {+   refs' = case Blocks.opKind maxReg mDict oinfo op of {             Blocks.IsCall ->              (Prelude.++)                (Fintype.image_mem (Fintype.ordinal_finType maxReg) (\n ->@@ -384,57 +393,92 @@   in   handleVars maxReg refs' b pos e ranges -reduceBlock :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->-               (Blocks.OpInfo a5 a3 a4) -> Prelude.Int -> Blocks.BlockId ->-               a1 -> Loops.LoopState -> (IntMap.IntMap IntMap.IntSet) ->-               (IntMap.IntMap PendingRanges) -> IntMap.IntMap PendingRanges-reduceBlock maxReg binfo oinfo pos bid block loops varUses =-  let {sz = Blocks.blockSize binfo block} in+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) ->+               IntMap.IntMap PendingRanges+reduceBlock maxReg mDict binfo oinfo pos bid block loops varUses =+  let {sz = Blocks.blockSize mDict binfo block} in   let {e = (Prelude.+) pos sz} in-  let {ops = Blocks.allBlockOps binfo block} in-  (Prelude.flip (Prelude.$)) __ (\_ ->-    (Prelude.flip (Prelude.$)) __ (\_ ->-      let {_evar_0_ = \h0 -> h0} in-      let {-       _evar_0_0 = \os o iHos ranges ->-        (Prelude.flip (Prelude.$)) __ (\_ ->-          (Prelude.flip (Prelude.$)) __ iHos-            (reduceOp maxReg oinfo pos-              ((Prelude.+) pos (Data.List.length os)) e block o ranges))}-      in-      Seq.last_ind (\_ h0 -> _evar_0_ h0) (\os o iHos _ ranges ->-        _evar_0_0 os o iHos ranges) ops __))--reduceBlocks :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->-                (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> Loops.LoopState ->-                (IntMap.IntMap IntMap.IntSet) -> (IntMap.IntMap-                LiveSets.BlockLiveSets) -> Prelude.Int -> BuildState-reduceBlocks maxReg binfo oinfo blocks loops varUses liveSets pos =-  let {_evar_0_ = \pos0 -> newBuildState pos0} in-  let {-   _evar_0_0 = \b blocks0 iHbs pos0 ->-    (Prelude.flip (Prelude.$)) (Blocks.blockId binfo b) (\bid ->-      (Prelude.flip (Prelude.$))-        (case IntMap.coq_IntMap_lookup bid liveSets of {-          Prelude.Just ls -> LiveSets.blockLiveOut ls;-          Prelude.Nothing -> IntMap.emptyIntSet}) (\outs ->-        let {sz = Blocks.blockSize binfo b} in+  let {ops = Blocks.allBlockOps mDict binfo block} in+  (Prelude.flip (Prelude.$)) __ (\_ ranges ->+    (Prelude.flip (Prelude.$))+      (case Prelude.not+              (IntMap.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 {+            Prelude.True -> acc;+            Prelude.False ->+             case IntMap.coq_IntMap_lookup loopIndex varUses of {+              Prelude.Just uses -> IntMap.coq_IntSet_union acc uses;+              Prelude.Nothing -> acc}}}+         in+         let {+          uses = IntMap.coq_IntMap_foldlWithKey f IntMap.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+           (Prelude.pred ((Prelude.+) pos sz)) ((Prelude.+) pos sz) ranges})+      ((Prelude.flip (Prelude.$)) __ (\_ ->+        let {_evar_0_ = \x -> x} in         let {-         _evar_0_0 = \_ ->+         _evar_0_0 = \os o iHos ranges0 ->           (Prelude.flip (Prelude.$)) __ (\_ ->-            (Prelude.flip (Prelude.$))-              (reduceBlock maxReg binfo oinfo pos0 bid b loops varUses-                (emptyPendingRanges maxReg pos0 ((Prelude.+) pos0 sz) outs))-              (\pending ->-              mergeIntoSortedRanges pos0 ((Prelude.+) pos0 sz) pending-                (iHbs ((Prelude.+) pos0 sz))))}+            (Prelude.flip (Prelude.$)) __ iHos+              (reduceOp maxReg mDict oinfo pos+                ((Prelude.+) pos (Data.List.length os)) e block o ranges0))}         in-        let {_evar_0_1 = \_ -> iHbs pos0} in-        case (Prelude.<=) ((Prelude.succ) 0) sz of {-         Prelude.True -> _evar_0_0 __;-         Prelude.False -> _evar_0_1 __}))}+        Seq.last_ind (\_ x -> _evar_0_ x) (\os o iHos _ ranges0 ->+          _evar_0_0 os o iHos ranges0) ops __)))++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) ->+                (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)}   in-  Datatypes.list_rec _evar_0_ _evar_0_0 blocks pos+  let {+   _evar_0_0 = \b blocks0 iHbs pos0 ->+    let {sz = Blocks.blockSize mDict binfo b} in+    let {+     _evar_0_0 = \_ ->+      (Prelude.flip (Prelude.$)) __ (\_ ->+        Monad.bind mDict (\bid ->+          let {+           outs = case IntMap.coq_IntMap_lookup bid liveSets of {+                   Prelude.Just ls -> LiveSets.blockLiveOut ls;+                   Prelude.Nothing -> IntMap.emptyIntSet}}+          in+          let {+           ranges = emptyPendingRanges maxReg pos0 ((Prelude.+) pos0 sz) outs}+          in+          let {+           pending = reduceBlock maxReg mDict binfo oinfo pos0 bid b loops+                       varUses ranges}+          in+          Monad.fmap (Monad.is_functor (Monad.is_applicative mDict))+            (mergeIntoSortedRanges pos0 ((Prelude.+) pos0 sz) pending)+            (iHbs ((Prelude.+) pos0 sz)))+          (Yoneda.iso_to+            (Yoneda.coq_Yoneda_lemma+              (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->+            Blocks.blockId mDict binfo b)))}+    in+    let {_evar_0_1 = \_ -> iHbs pos0} in+    case (Prelude.<=) ((Prelude.succ) 0) sz of {+     Prelude.True -> _evar_0_0 __;+     Prelude.False -> _evar_0_1 __}}+  in+  Datatypes.list_rect _evar_0_ _evar_0_0 blocks pos  compileIntervals :: Prelude.Int -> Prelude.Int -> BuildState -> (,)                     ScanState.FixedIntervalsType@@ -480,11 +524,11 @@      (,) x x0 -> _evar_0_ x x0}) ((,)     (Data.List.replicate maxReg Prelude.Nothing) IntMap.emptyIntMap) bs -buildIntervals :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->-                  (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> Loops.LoopState ->-                  (IntMap.IntMap LiveSets.BlockLiveSets) -> Prelude.Either-                  Morph.SSError ScanState.ScanStateSig-buildIntervals maxReg binfo oinfo blocks loops liveSets =+buildIntervals :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo +                  a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([] +                  a1) -> Loops.LoopState -> (IntMap.IntMap+                  LiveSets.BlockLiveSets) -> a5+buildIntervals maxReg mDict binfo oinfo blocks loops liveSets =   let {    add_unhandled_interval = \ss i ->     ScanState.packScanState maxReg ScanState.Pending@@ -501,37 +545,44 @@       (Prelude.map Prelude.id (ScanState.handled maxReg ( ss))))}   in   case blocks of {-   [] -> Prelude.Right-    (ScanState.packScanState maxReg ScanState.InUse-      (ScanState.Build_ScanStateDesc 0 []-      (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []));+   [] ->+    Monad.pure (Monad.is_applicative mDict) (Prelude.Right+      (ScanState.packScanState maxReg ScanState.InUse+        (ScanState.Build_ScanStateDesc 0 []+        (Data.List.replicate maxReg Prelude.Nothing) [] [] [] [])));    (:) b bs ->-    let {-     varUses = Loops.computeVarReferences maxReg binfo oinfo ((:) b bs) loops}-    in-    let {-     reduced = reduceBlocks maxReg binfo oinfo ((:) b bs) loops varUses-                 liveSets 0}-    in-    case compileIntervals maxReg 0 reduced of {-     (,) regs vars ->-      let {-       s2 = ScanState.packScanState maxReg ScanState.Pending-              (ScanState.Build_ScanStateDesc-              (ScanState.nextInterval maxReg (ScanState.Build_ScanStateDesc 0-                [] (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []))-              (ScanState.intervals maxReg (ScanState.Build_ScanStateDesc 0 []-                (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []))-              regs-              (ScanState.unhandled maxReg (ScanState.Build_ScanStateDesc 0 []-                (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []))-              (ScanState.active maxReg (ScanState.Build_ScanStateDesc 0 []-                (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []))-              (ScanState.inactive maxReg (ScanState.Build_ScanStateDesc 0 []-                (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []))-              (ScanState.handled maxReg (ScanState.Build_ScanStateDesc 0 []-                (Data.List.replicate maxReg Prelude.Nothing) [] [] [] [])))}-      in-      let {s3 = IntMap.coq_IntMap_foldl add_unhandled_interval s2 vars} in-      Prelude.Right (ScanState.packScanState maxReg ScanState.InUse ( s3))}}+    Monad.bind mDict (\varUses ->+      Monad.bind mDict (\reduced ->+        case compileIntervals maxReg 0 reduced of {+         (,) regs vars ->+          let {+           s2 = ScanState.packScanState maxReg ScanState.Pending+                  (ScanState.Build_ScanStateDesc+                  (ScanState.nextInterval maxReg+                    (ScanState.Build_ScanStateDesc 0 []+                    (Data.List.replicate maxReg Prelude.Nothing) [] [] []+                    []))+                  (ScanState.intervals maxReg (ScanState.Build_ScanStateDesc+                    0 [] (Data.List.replicate maxReg Prelude.Nothing) [] []+                    [] [])) regs+                  (ScanState.unhandled maxReg (ScanState.Build_ScanStateDesc+                    0 [] (Data.List.replicate maxReg Prelude.Nothing) [] []+                    [] []))+                  (ScanState.active maxReg (ScanState.Build_ScanStateDesc 0+                    [] (Data.List.replicate maxReg Prelude.Nothing) [] [] []+                    []))+                  (ScanState.inactive maxReg (ScanState.Build_ScanStateDesc 0+                    [] (Data.List.replicate maxReg Prelude.Nothing) [] [] []+                    []))+                  (ScanState.handled maxReg (ScanState.Build_ScanStateDesc 0+                    [] (Data.List.replicate maxReg Prelude.Nothing) [] [] []+                    [])))}+          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)))})+        (reduceBlocks maxReg mDict binfo oinfo ((:) b bs) loops varUses+          liveSets 0))+      (Loops.computeVarReferences maxReg mDict binfo oinfo ((:) b bs) loops)} 

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Choice where@@ -13,7 +13,6 @@ import qualified Data.Functor.Identity import qualified LinearScan.Utils -import qualified LinearScan.Logic as Logic import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Ssrbool as Ssrbool import qualified LinearScan.Ssrfun as Ssrfun@@ -21,35 +20,36 @@   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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" +#ifdef __GLASGOW_HASKELL__+type Any = GHC.Prim.Any+#else+-- HUGS+type Any = ()+#endif+ type Choice__Coq_mixin_of t =   (Ssrbool.Coq_pred t) -> Prelude.Int -> Prelude.Maybe t   -- singleton inductive, whose constructor was Mixin   -_Choice__mixin_of_rect :: (((Ssrbool.Coq_pred a1) -> Prelude.Int ->-                          Prelude.Maybe a1) -> () -> () -> () -> a2) ->-                          (Choice__Coq_mixin_of a1) -> a2-_Choice__mixin_of_rect f m =-  f m __ __ __--_Choice__mixin_of_rec :: (((Ssrbool.Coq_pred a1) -> Prelude.Int ->-                         Prelude.Maybe a1) -> () -> () -> () -> a2) ->-                         (Choice__Coq_mixin_of a1) -> a2-_Choice__mixin_of_rec =-  _Choice__mixin_of_rect- _Choice__find :: (Choice__Coq_mixin_of a1) -> (Ssrbool.Coq_pred a1) ->                  Prelude.Int -> Prelude.Maybe a1 _Choice__find m =@@ -58,19 +58,6 @@ data Choice__Coq_class_of t =    Choice__Class (Eqtype.Equality__Coq_mixin_of t) (Choice__Coq_mixin_of t) -_Choice__class_of_rect :: ((Eqtype.Equality__Coq_mixin_of a1) ->-                          (Choice__Coq_mixin_of a1) -> a2) ->-                          (Choice__Coq_class_of a1) -> a2-_Choice__class_of_rect f c =-  case c of {-   Choice__Class x x0 -> f x x0}--_Choice__class_of_rec :: ((Eqtype.Equality__Coq_mixin_of a1) ->-                         (Choice__Coq_mixin_of a1) -> a2) ->-                         (Choice__Coq_class_of a1) -> a2-_Choice__class_of_rec =-  _Choice__class_of_rect- _Choice__base :: (Choice__Coq_class_of a1) -> Eqtype.Equality__Coq_mixin_of                  a1 _Choice__base c =@@ -83,61 +70,22 @@    Choice__Class base0 mixin0 -> mixin0}  type Choice__Coq_type =-  Choice__Coq_class_of ()+  Choice__Coq_class_of Any   -- singleton inductive, whose constructor was Pack   -_Choice__type_rect :: (() -> (Choice__Coq_class_of ()) -> () -> a1) ->-                      Choice__Coq_type -> a1-_Choice__type_rect f t =-  f __ t __--_Choice__type_rec :: (() -> (Choice__Coq_class_of ()) -> () -> a1) ->-                     Choice__Coq_type -> a1-_Choice__type_rec =-  _Choice__type_rect--type Choice__Coq_sort = ()+type Choice__Coq_sort = Any  _Choice__coq_class :: Choice__Coq_type -> Choice__Coq_class_of                       Choice__Coq_sort _Choice__coq_class cT =   cT -_Choice__clone :: Choice__Coq_type -> (Choice__Coq_class_of a1) ->-                  Choice__Coq_type-_Choice__clone cT c =-  unsafeCoerce c--_Choice__pack :: (Choice__Coq_mixin_of a1) -> (Eqtype.Equality__Coq_mixin_of-                 a1) -> Eqtype.Equality__Coq_type -> Choice__Coq_type-_Choice__pack m b bT =-  Choice__Class (unsafeCoerce b) (unsafeCoerce m)--_Choice__eqType :: Choice__Coq_type -> Eqtype.Equality__Coq_type-_Choice__eqType cT =-  _Choice__base (_Choice__coq_class cT)- _Choice__InternalTheory__find :: Choice__Coq_type -> (Ssrbool.Coq_pred                                  Choice__Coq_sort) -> Prelude.Int ->                                  Prelude.Maybe Choice__Coq_sort _Choice__InternalTheory__find t =   _Choice__find (_Choice__mixin (_Choice__coq_class t)) -_Choice__InternalTheory__xchoose_subproof :: Choice__Coq_type ->-                                             (Ssrbool.Coq_pred-                                             Choice__Coq_sort) ->-                                             Choice__Coq_sort-_Choice__InternalTheory__xchoose_subproof t p =-  let {-   n = Ssrnat.ex_minnP (\n ->-         Ssrbool.isSome (_Choice__InternalTheory__find t p n))}-  in-  let {_evar_0_ = \x -> x} in-  let {_evar_0_0 = \_ _ -> Logic.coq_False_rect} in-  case _Choice__InternalTheory__find t p n of {-   Prelude.Just x -> _evar_0_ x;-   Prelude.Nothing -> _evar_0_0 __ __}- coq_PcanChoiceMixin :: Choice__Coq_type -> (a1 -> Choice__Coq_sort) ->                        (Choice__Coq_sort -> Prelude.Maybe a1) ->                        Choice__Coq_mixin_of a1@@ -179,19 +127,6 @@ data Countable__Coq_mixin_of t =    Countable__Mixin (t -> Prelude.Int) (Prelude.Int -> Prelude.Maybe t) -_Countable__mixin_of_rect :: ((a1 -> Prelude.Int) -> (Prelude.Int ->-                             Prelude.Maybe a1) -> () -> a2) ->-                             (Countable__Coq_mixin_of a1) -> a2-_Countable__mixin_of_rect f m =-  case m of {-   Countable__Mixin x x0 -> f x x0 __}--_Countable__mixin_of_rec :: ((a1 -> Prelude.Int) -> (Prelude.Int ->-                            Prelude.Maybe a1) -> () -> a2) ->-                            (Countable__Coq_mixin_of a1) -> a2-_Countable__mixin_of_rec =-  _Countable__mixin_of_rect- _Countable__pickle :: (Countable__Coq_mixin_of a1) -> a1 -> Prelude.Int _Countable__pickle m =   case m of {@@ -203,40 +138,9 @@   case m of {    Countable__Mixin pickle0 unpickle0 -> unpickle0} -_Countable__coq_EqMixin :: (Countable__Coq_mixin_of a1) ->-                           Eqtype.Equality__Coq_mixin_of a1-_Countable__coq_EqMixin m =-  Eqtype.coq_PcanEqMixin Ssrnat.nat_eqType-    (unsafeCoerce (_Countable__pickle m))-    (unsafeCoerce (_Countable__unpickle m))--_Countable__coq_ChoiceMixin :: (Countable__Coq_mixin_of a1) ->-                               Choice__Coq_mixin_of a1-_Countable__coq_ChoiceMixin m =-  coq_PcanChoiceMixin nat_choiceType (unsafeCoerce (_Countable__pickle m))-    (unsafeCoerce (_Countable__unpickle m))- data Countable__Coq_class_of t =    Countable__Class (Choice__Coq_class_of t) (Countable__Coq_mixin_of t) -_Countable__class_of_rect :: ((Choice__Coq_class_of a1) ->-                             (Countable__Coq_mixin_of a1) -> a2) ->-                             (Countable__Coq_class_of a1) -> a2-_Countable__class_of_rect f c =-  case c of {-   Countable__Class x x0 -> f x x0}--_Countable__class_of_rec :: ((Choice__Coq_class_of a1) ->-                            (Countable__Coq_mixin_of a1) -> a2) ->-                            (Countable__Coq_class_of a1) -> a2-_Countable__class_of_rec =-  _Countable__class_of_rect--_Countable__base :: (Countable__Coq_class_of a1) -> Choice__Coq_class_of a1-_Countable__base c =-  case c of {-   Countable__Class base0 mixin0 -> base0}- _Countable__mixin :: (Countable__Coq_class_of a1) -> Countable__Coq_mixin_of                      a1 _Countable__mixin c =@@ -244,44 +148,16 @@    Countable__Class base0 mixin0 -> mixin0}  type Countable__Coq_type =-  Countable__Coq_class_of ()+  Countable__Coq_class_of Any   -- singleton inductive, whose constructor was Pack   -_Countable__type_rect :: (() -> (Countable__Coq_class_of ()) -> () -> a1) ->-                         Countable__Coq_type -> a1-_Countable__type_rect f t =-  f __ t __--_Countable__type_rec :: (() -> (Countable__Coq_class_of ()) -> () -> a1) ->-                        Countable__Coq_type -> a1-_Countable__type_rec =-  _Countable__type_rect--type Countable__Coq_sort = ()+type Countable__Coq_sort = Any  _Countable__coq_class :: Countable__Coq_type -> Countable__Coq_class_of                          Countable__Coq_sort _Countable__coq_class cT =   cT -_Countable__clone :: Countable__Coq_type -> (Countable__Coq_class_of -                     a1) -> Countable__Coq_type-_Countable__clone cT c =-  unsafeCoerce c--_Countable__pack :: (Countable__Coq_mixin_of a1) -> Choice__Coq_type ->-                    (Choice__Coq_class_of a1) -> Countable__Coq_type-_Countable__pack m bT b =-  Countable__Class (unsafeCoerce b) (unsafeCoerce m)--_Countable__eqType :: Countable__Coq_type -> Eqtype.Equality__Coq_type-_Countable__eqType cT =-  _Choice__base (_Countable__base (_Countable__coq_class cT))--_Countable__choiceType :: Countable__Coq_type -> Choice__Coq_type-_Countable__choiceType cT =-  _Countable__base (_Countable__coq_class cT)- unpickle :: Countable__Coq_type -> Prelude.Int -> Prelude.Maybe             Countable__Coq_sort unpickle t =@@ -290,14 +166,6 @@ pickle :: Countable__Coq_type -> Countable__Coq_sort -> Prelude.Int pickle t =   _Countable__pickle (_Countable__mixin (_Countable__coq_class t))--pickle_inv :: Countable__Coq_type -> Eqtype.Equality__Coq_sort ->-              Prelude.Maybe Countable__Coq_sort-pickle_inv t n =-  Ssrfun._Option__bind (\x ->-    case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (pickle t x)) n of {-     Prelude.True -> Prelude.Just x;-     Prelude.False -> Prelude.Nothing}) (unpickle t (unsafeCoerce n))  coq_PcanCountMixin :: Countable__Coq_type -> (a1 -> Countable__Coq_sort) ->                       (Countable__Coq_sort -> Prelude.Maybe a1) ->

@@ -1,3 +1,5 @@++ module LinearScan.Cursor where  

@@ -1,3 +1,5 @@++ module LinearScan.Datatypes where  

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Eqtype where@@ -13,22 +13,37 @@ import qualified Data.Functor.Identity import qualified LinearScan.Utils -import qualified LinearScan.Specif as Specif import qualified LinearScan.Ssrbool as Ssrbool import qualified LinearScan.Ssrfun as Ssrfun   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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" @@ -37,52 +52,22 @@ data Equality__Coq_mixin_of t =    Equality__Mixin (Ssrbool.Coq_rel t) (Equality__Coq_axiom t) -_Equality__mixin_of_rect :: ((Ssrbool.Coq_rel a1) -> (Equality__Coq_axiom -                            a1) -> a2) -> (Equality__Coq_mixin_of a1) -> a2-_Equality__mixin_of_rect f m =-  case m of {-   Equality__Mixin x x0 -> f x x0}--_Equality__mixin_of_rec :: ((Ssrbool.Coq_rel a1) -> (Equality__Coq_axiom -                           a1) -> a2) -> (Equality__Coq_mixin_of a1) -> a2-_Equality__mixin_of_rec =-  _Equality__mixin_of_rect- _Equality__op :: (Equality__Coq_mixin_of a1) -> Ssrbool.Coq_rel a1 _Equality__op m =   case m of {    Equality__Mixin op0 x -> op0}  type Equality__Coq_type =-  Equality__Coq_mixin_of ()+  Equality__Coq_mixin_of Any   -- singleton inductive, whose constructor was Pack   -_Equality__type_rect :: (() -> (Equality__Coq_mixin_of ()) -> () -> a1) ->-                        Equality__Coq_type -> a1-_Equality__type_rect f t =-  f __ t __--_Equality__type_rec :: (() -> (Equality__Coq_mixin_of ()) -> () -> a1) ->-                       Equality__Coq_type -> a1-_Equality__type_rec =-  _Equality__type_rect--type Equality__Coq_sort = ()+type Equality__Coq_sort = Any  _Equality__coq_class :: Equality__Coq_type -> Equality__Coq_mixin_of                         Equality__Coq_sort _Equality__coq_class cT =   cT -_Equality__pack :: (Equality__Coq_mixin_of a1) -> Equality__Coq_type-_Equality__pack c =-  unsafeCoerce c--_Equality__clone :: Equality__Coq_type -> (Equality__Coq_mixin_of a1) ->-                    (Equality__Coq_sort -> a1) -> Equality__Coq_type-_Equality__clone cT c x =-  _Equality__pack c- eq_op :: Equality__Coq_type -> Ssrbool.Coq_rel Equality__Coq_sort eq_op t =   _Equality__op (_Equality__coq_class t)@@ -94,9 +79,9 @@    Equality__Mixin x x0 -> _evar_0_ x x0}  data Coq_subType t =-   SubType (() -> t) (t -> () -> ()) (() -> (t -> () -> ()) -> () -> ())+   SubType (Any -> t) (t -> () -> Any) (() -> (t -> () -> Any) -> Any -> Any) -type Coq_sub_sort t = ()+type Coq_sub_sort t = Any  val :: (Ssrbool.Coq_pred a1) -> (Coq_subType a1) -> (Coq_sub_sort a1) -> a1 val p s =@@ -115,31 +100,32 @@    Ssrbool.ReflectT -> Prelude.Just (coq_Sub p sT x);    Ssrbool.ReflectF -> Prelude.Nothing} -s2val :: (Specif.Coq_sig2 a1) -> a1-s2val u =-  u+sig_subType :: (Ssrbool.Coq_pred a1) -> Coq_subType a1+sig_subType p =+  SubType (unsafeCoerce ) (unsafeCoerce (\x _ -> x)) (\_ k_S u ->+    k_S (unsafeCoerce u) __)  inj_eqAxiom :: Equality__Coq_type -> (a1 -> Equality__Coq_sort) ->                Equality__Coq_axiom a1 inj_eqAxiom eT f x y =   Ssrbool.iffP (eq_op eT (f x) (f y)) (eqP eT (f x) (f y)) -coq_InjEqMixin :: Equality__Coq_type -> (a1 -> Equality__Coq_sort) ->-                  Equality__Coq_mixin_of a1-coq_InjEqMixin eT f =-  Equality__Mixin (\x y -> eq_op eT (f x) (f y)) (inj_eqAxiom eT f)--coq_PcanEqMixin :: Equality__Coq_type -> (a1 -> Equality__Coq_sort) ->-                   (Equality__Coq_sort -> Prelude.Maybe a1) ->-                   Equality__Coq_mixin_of a1-coq_PcanEqMixin eT f g =-  coq_InjEqMixin eT f- val_eqP :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) ->            (Coq_subType Equality__Coq_sort) -> Equality__Coq_axiom            (Coq_sub_sort Equality__Coq_sort) val_eqP t p sT =   inj_eqAxiom t (val p sT)++sig_eqMixin :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) ->+               Equality__Coq_mixin_of Equality__Coq_sort+sig_eqMixin t p =+  Equality__Mixin (\x y -> eq_op t ( x) ( y))+    (unsafeCoerce (val_eqP t (\x -> p x) (sig_subType p)))++sig_eqType :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) ->+              Equality__Coq_type+sig_eqType t p =+  unsafeCoerce (sig_eqMixin t p)  pair_eq :: Equality__Coq_type -> Equality__Coq_type -> Ssrbool.Coq_simpl_rel            ((,) Equality__Coq_sort Equality__Coq_sort)

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Fintype where@@ -21,16 +21,32 @@   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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" @@ -38,73 +54,15 @@    Finite__Mixin (Choice.Countable__Coq_mixin_of Eqtype.Equality__Coq_sort)   ([] Eqtype.Equality__Coq_sort) -_Finite__mixin_of_rect :: Eqtype.Equality__Coq_type ->-                          ((Choice.Countable__Coq_mixin_of-                          Eqtype.Equality__Coq_sort) -> ([]-                          Eqtype.Equality__Coq_sort) -> () -> a1) ->-                          Finite__Coq_mixin_of -> a1-_Finite__mixin_of_rect t f m =-  case m of {-   Finite__Mixin x x0 -> f x x0 __}--_Finite__mixin_of_rec :: Eqtype.Equality__Coq_type ->-                         ((Choice.Countable__Coq_mixin_of-                         Eqtype.Equality__Coq_sort) -> ([]-                         Eqtype.Equality__Coq_sort) -> () -> a1) ->-                         Finite__Coq_mixin_of -> a1-_Finite__mixin_of_rec t =-  _Finite__mixin_of_rect t--_Finite__mixin_base :: Eqtype.Equality__Coq_type -> Finite__Coq_mixin_of ->-                       Choice.Countable__Coq_mixin_of-                       Eqtype.Equality__Coq_sort-_Finite__mixin_base t m =-  case m of {-   Finite__Mixin mixin_base0 mixin_enum0 -> mixin_base0}- _Finite__mixin_enum :: Eqtype.Equality__Coq_type -> Finite__Coq_mixin_of ->                        [] Eqtype.Equality__Coq_sort _Finite__mixin_enum t m =   case m of {-   Finite__Mixin mixin_base0 mixin_enum0 -> mixin_enum0}--_Finite__coq_EnumMixin :: Choice.Countable__Coq_type -> ([]-                          Choice.Countable__Coq_sort) -> Finite__Coq_mixin_of-_Finite__coq_EnumMixin t e =-  case t of {-   Choice.Countable__Class base0 m -> Finite__Mixin m e}--_Finite__coq_UniqMixin :: Choice.Countable__Coq_type -> ([]-                          Choice.Countable__Coq_sort) -> Finite__Coq_mixin_of-_Finite__coq_UniqMixin t e =-  _Finite__coq_EnumMixin t e--_Finite__count_enum :: Choice.Countable__Coq_type -> Prelude.Int -> []-                       Choice.Countable__Coq_sort-_Finite__count_enum t n =-  Seq.pmap (unsafeCoerce (Choice.pickle_inv t)) (Seq.iota 0 n)--_Finite__coq_CountMixin :: Choice.Countable__Coq_type -> Prelude.Int ->-                           Finite__Coq_mixin_of-_Finite__coq_CountMixin t n =-  _Finite__coq_EnumMixin t (_Finite__count_enum t n)+   Finite__Mixin mixin_base mixin_enum0 -> mixin_enum0}  data Finite__Coq_class_of t =    Finite__Class (Choice.Choice__Coq_class_of t) Finite__Coq_mixin_of -_Finite__class_of_rect :: ((Choice.Choice__Coq_class_of a1) ->-                          Finite__Coq_mixin_of -> a2) ->-                          (Finite__Coq_class_of a1) -> a2-_Finite__class_of_rect f c =-  case c of {-   Finite__Class x x0 -> f x x0}--_Finite__class_of_rec :: ((Choice.Choice__Coq_class_of a1) ->-                         Finite__Coq_mixin_of -> a2) -> (Finite__Coq_class_of-                         a1) -> a2-_Finite__class_of_rec =-  _Finite__class_of_rect- _Finite__base :: (Finite__Coq_class_of a1) -> Choice.Choice__Coq_class_of a1 _Finite__base c =   case c of {@@ -115,64 +73,26 @@   case c of {    Finite__Class base0 mixin0 -> mixin0} -_Finite__base2 :: (Finite__Coq_class_of a1) -> Choice.Countable__Coq_class_of-                  a1-_Finite__base2 c =-  Choice.Countable__Class (_Finite__base c)-    (unsafeCoerce-      (_Finite__mixin_base-        (Choice._Choice__base (_Finite__base (unsafeCoerce c)))-        (_Finite__mixin c)))- type Finite__Coq_type =-  Finite__Coq_class_of ()+  Finite__Coq_class_of Any   -- singleton inductive, whose constructor was Pack   -_Finite__type_rect :: (() -> (Finite__Coq_class_of ()) -> () -> a1) ->-                      Finite__Coq_type -> a1-_Finite__type_rect f t =-  f __ t __--_Finite__type_rec :: (() -> (Finite__Coq_class_of ()) -> () -> a1) ->-                     Finite__Coq_type -> a1-_Finite__type_rec =-  _Finite__type_rect--type Finite__Coq_sort = ()+type Finite__Coq_sort = Any  _Finite__coq_class :: Finite__Coq_type -> Finite__Coq_class_of                       Finite__Coq_sort _Finite__coq_class cT =   cT -_Finite__clone :: Finite__Coq_type -> (Finite__Coq_class_of a1) ->-                  Finite__Coq_type-_Finite__clone cT c =-  unsafeCoerce c--_Finite__pack :: (Eqtype.Equality__Coq_mixin_of a1) -> Finite__Coq_mixin_of-                 -> Choice.Choice__Coq_type -> (Choice.Choice__Coq_class_of-                 a1) -> Finite__Coq_mixin_of -> Finite__Coq_type-_Finite__pack b0 m0 bT b m =-  Finite__Class (unsafeCoerce b) m--_Finite__eqType :: Finite__Coq_type -> Eqtype.Equality__Coq_type-_Finite__eqType cT =-  Choice._Choice__base (_Finite__base (_Finite__coq_class cT))--_Finite__choiceType :: Finite__Coq_type -> Choice.Choice__Coq_type-_Finite__choiceType cT =-  _Finite__base (_Finite__coq_class cT)--_Finite__countType :: Finite__Coq_type -> Choice.Countable__Coq_type-_Finite__countType cT =-  _Finite__base2 (_Finite__coq_class cT)- _Finite__EnumDef__enum :: Finite__Coq_type -> [] Finite__Coq_sort _Finite__EnumDef__enum cT =   _Finite__mixin_enum     (Choice._Choice__base (_Finite__base (_Finite__coq_class cT)))     (_Finite__mixin (_Finite__coq_class cT))++_Finite__EnumDef__enumDef :: ()+_Finite__EnumDef__enumDef =+  __  enum_mem :: Finite__Coq_type -> (Ssrbool.Coq_mem_pred Finite__Coq_sort) -> []             Finite__Coq_sort

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Graph where@@ -19,13 +19,21 @@   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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 

@@ -1,3 +1,5 @@++ module LinearScan.IState where  

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.IntMap where@@ -21,13 +21,21 @@   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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 

@@ -1,3 +1,5 @@++ module LinearScan.Interval where  @@ -17,7 +19,6 @@ import qualified LinearScan.Specif as Specif import qualified LinearScan.UsePos as UsePos import qualified LinearScan.Seq as Seq-import qualified LinearScan.Ssrnat as Ssrnat   __ :: any@@ -82,47 +83,44 @@         Lib.option_choose mx (Range.rangeIntersectionPoint ( rd) ( rd')))         Prelude.Nothing (rds j))) Prelude.Nothing (rds i) -searchInRange :: Range.RangeDesc -> (UsePos.UsePos -> Prelude.Bool) ->-                 Prelude.Maybe UsePos.UsePos-searchInRange r f =-  let {_evar_0_ = \x -> Prelude.Just x} in-  let {_evar_0_0 = Prelude.Nothing} in-  case Range.findRangeUsePos ( r) f of {-   Prelude.Just x -> _evar_0_ x;-   Prelude.Nothing -> _evar_0_0}- findIntervalUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) ->                       Prelude.Maybe                       ((,) Range.RangeDesc (Specif.Coq_sig2 UsePos.UsePos)) findIntervalUsePos d f =-  case d of {-   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 ->+  let {+   _evar_0_ = \_ ->     let {-     _evar_0_ = \r ->-      let {_top_assumption_ = searchInRange r f} in+     _evar_0_ = \_ ->       let {-       _evar_0_ = \_top_assumption_0 -> Prelude.Just ((,) r-        _top_assumption_0)}+       _evar_0_ = \r ->+        let {_top_assumption_ = Range.findRangeUsePos ( r) f} in+        let {+         _evar_0_ = \_top_assumption_0 -> Prelude.Just ((,) r+          _top_assumption_0)}+        in+        let {_evar_0_0 = Prelude.Nothing} in+        case _top_assumption_ of {+         Prelude.Just x -> _evar_0_ x;+         Prelude.Nothing -> _evar_0_0}}       in-      let {_evar_0_0 = Prelude.Nothing} in-      case _top_assumption_ of {-       Prelude.Just x -> _evar_0_ x;-       Prelude.Nothing -> _evar_0_0}}-    in-    let {-     _evar_0_0 = \r rs iHrs ->-      let {_top_assumption_ = searchInRange r f} in       let {-       _evar_0_0 = \_top_assumption_0 -> Prelude.Just ((,) r-        _top_assumption_0)}+       _evar_0_0 = \r rs iHrs ->+        let {_top_assumption_ = Range.findRangeUsePos ( r) f} in+        let {+         _evar_0_0 = \_top_assumption_0 -> Prelude.Just ((,) r+          _top_assumption_0)}+        in+        let {_evar_0_1 = iHrs __ __ __} in+        case _top_assumption_ of {+         Prelude.Just x -> _evar_0_0 x;+         Prelude.Nothing -> _evar_0_1}}       in-      let {_evar_0_1 = iHrs __ __ __} in-      case _top_assumption_ of {-       Prelude.Just x -> _evar_0_0 x;-       Prelude.Nothing -> _evar_0_1}}+      NonEmpty0.coq_NonEmpty_rec (\r _ _ _ -> _evar_0_ r)+        (\r rs iHrs _ _ _ -> _evar_0_0 r rs iHrs) (rds d) __ __ __}     in-    NonEmpty0.coq_NonEmpty_rec (\r _ _ _ -> _evar_0_ r) (\r rs iHrs _ _ _ ->-      _evar_0_0 r rs iHrs) rds0 __ __ __}+     _evar_0_ __}+  in+   _evar_0_ __  lookupUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) ->                 Prelude.Maybe Lib.Coq_oddnum@@ -199,16 +197,6 @@ firstUseReqReg :: IntervalDesc -> Prelude.Maybe Lib.Coq_oddnum firstUseReqReg d =   lookupUsePos d UsePos.regReq--firstUseReqRegOrEnd :: IntervalDesc -> Lib.Coq_oddnum-firstUseReqRegOrEnd d =-  let {filtered_var = firstUseReqReg d} in-  case filtered_var of {-   Prelude.Just n ->  n;-   Prelude.Nothing ->-    case Ssrnat.odd (iend d) of {-     Prelude.True -> iend d;-     Prelude.False -> Prelude.pred (iend d)}}  divideIntervalRanges :: IntervalDesc -> Prelude.Int ->                         ((,) Range.SortedRanges Range.SortedRanges)

@@ -0,0 +1,72 @@+{-# OPTIONS_GHC -cpp -XMagicHash #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Lens 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.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 Identity a = a++coq_Identity_Functor :: Monad.Functor (Identity Any)+coq_Identity_Functor _ _ x =+  x++type Const c a = c++coq_Const_Functor :: Monad.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 a = Lens s s a a++set :: (Lens a1 a2 a3 a4) -> a4 -> a1 -> a2+set l x =+  unsafeCoerce l __ coq_Identity_Functor (\x0 -> x)++view :: (Lens' a1 a2) -> a1 -> a2+view f =+  unsafeCoerce f __ coq_Const_Functor (\x -> x)+

@@ -1,3 +1,5 @@++ module LinearScan.Lib where  @@ -16,6 +18,12 @@  __ :: 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 =

@@ -1,3 +1,5 @@++ module LinearScan.List0 where  

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.LiveSets where@@ -16,20 +16,30 @@ import qualified LinearScan.Blocks as Blocks import qualified LinearScan.IntMap as IntMap import qualified LinearScan.Lib as Lib+import qualified LinearScan.Monad as Monad import qualified LinearScan.UsePos as UsePos+import qualified LinearScan.Yoneda as Yoneda import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Ssrbool as Ssrbool import qualified LinearScan.Ssrnat as Ssrnat   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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 @@ -210,118 +220,143 @@ coq_BlockLiveSets_eqType =   unsafeCoerce coq_BlockLiveSets_eqMixin -computeLocalLiveSets :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->-                        (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> IntMap.IntMap-                        BlockLiveSets-computeLocalLiveSets maxReg binfo oinfo blocks =-  Prelude.snd-    (Lib.forFold ((,) ((Prelude.succ) 0) IntMap.emptyIntMap) blocks-      (\acc b ->-      case acc of {-       (,) idx m ->-        case Blocks.blockOps binfo b of {-         (,) p opse ->-          case p of {-           (,) opsb opsm ->-            let {-             liveSet = Build_BlockLiveSets IntMap.emptyIntSet-              IntMap.emptyIntSet IntMap.emptyIntSet IntMap.emptyIntSet-              ((Prelude.+) idx (Ssrnat.double (Data.List.length opsb))) idx}-            in-            case Lib.forFold ((,) idx liveSet)-                   ((Prelude.++) opsb ((Prelude.++) opsm opse)) (\acc0 o ->-                   case acc0 of {-                    (,) lastIdx liveSet1 -> (,) ((Prelude.succ)-                     ((Prelude.succ) lastIdx))-                     (case Lib.partition (\v ->-                             Eqtype.eq_op UsePos.coq_VarKind_eqType-                               (unsafeCoerce (Blocks.varKind maxReg v))-                               (unsafeCoerce UsePos.Input))-                             (Blocks.opRefs maxReg oinfo o) of {-                       (,) inputs others ->-                        let {-                         liveSet2 = Lib.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 vid-                                                 (blockLiveKill liveSet2)) of {-                                         Prelude.True -> Build_BlockLiveSets+computeLocalLiveSets :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo+                        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+      (Monad.forFoldM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) ((,)+        ((Prelude.succ) 0) IntMap.emptyIntMap) blocks (\acc b ->+        case acc of {+         (,) idx m ->+          case Blocks.blockOps mDict binfo b of {+           (,) p opse ->+            case p of {+             (,) opsb opsm ->+              let {+               liveSet = Build_BlockLiveSets IntMap.emptyIntSet+                IntMap.emptyIntSet IntMap.emptyIntSet IntMap.emptyIntSet+                ((Prelude.+) idx (Ssrnat.double (Data.List.length opsb)))+                idx}+              in+              case Lib.forFold ((,) idx liveSet)+                     ((Prelude.++) opsb ((Prelude.++) opsm opse)) (\acc0 o ->+                     case acc0 of {+                      (,) lastIdx liveSet1 -> (,) ((Prelude.succ)+                       ((Prelude.succ) lastIdx))+                       (case Lib.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 v ->+                                        case Blocks.varId maxReg v of {+                                         Prelude.Left p0 -> liveSet2;+                                         Prelude.Right vid ->+                                          case Prelude.not+                                                 (IntMap.coq_IntSet_member+                                                   vid+                                                   (blockLiveKill liveSet2)) of {+                                           Prelude.True ->+                                            Build_BlockLiveSets+                                            (IntMap.coq_IntSet_insert vid+                                              (blockLiveGen liveSet2))+                                            (blockLiveKill liveSet2)+                                            (blockLiveIn liveSet2)+                                            (blockLiveOut liveSet2)+                                            (blockFirstOpId liveSet2) lastIdx;+                                           Prelude.False -> liveSet2}})}+                          in+                          let {+                           liveSet3 = Lib.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-                                            (blockLiveGen liveSet2))-                                          (blockLiveKill liveSet2)-                                          (blockLiveIn liveSet2)-                                          (blockLiveOut liveSet2)-                                          (blockFirstOpId liveSet2) lastIdx;-                                         Prelude.False -> liveSet2}})}-                        in-                        let {-                         liveSet3 = Lib.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-                                          (blockLiveKill liveSet3))-                                        (blockLiveIn liveSet3)-                                        (blockLiveOut liveSet3)-                                        (blockFirstOpId liveSet3) lastIdx})}-                        in-                        Build_BlockLiveSets (blockLiveGen liveSet3)-                        (blockLiveKill liveSet3) (blockLiveIn liveSet3)-                        (blockLiveOut liveSet3) (blockFirstOpId liveSet3)-                        lastIdx})}) of {-             (,) lastIdx' liveSet3 -> (,) lastIdx'-              (IntMap.coq_IntMap_insert (Blocks.blockId binfo b) liveSet3 m)}}}}))+                                            (blockLiveKill liveSet3))+                                          (blockLiveIn liveSet3)+                                          (blockLiveOut liveSet3)+                                          (blockFirstOpId liveSet3) lastIdx})}+                          in+                          Build_BlockLiveSets (blockLiveGen liveSet3)+                          (blockLiveKill liveSet3) (blockLiveIn liveSet3)+                          (blockLiveOut liveSet3) (blockFirstOpId liveSet3)+                          lastIdx})}) of {+               (,) lastIdx' liveSet3 ->+                Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict))+                  (\k ->+                  Monad.pure+                    (unsafeCoerce+                      (Yoneda.coq_Yoneda_Applicative+                        (Monad.is_applicative mDict))) ((,) lastIdx'+                    (IntMap.coq_IntMap_insert k liveSet3 m))) (\_ ->+                  Blocks.blockId mDict binfo b)}}}}))) -computeGlobalLiveSets :: (Blocks.BlockInfo a1 a2 a3 a4) -> ([] a1) ->-                         (IntMap.IntMap BlockLiveSets) -> IntMap.IntMap-                         BlockLiveSets-computeGlobalLiveSets binfo blocks liveSets =-  Lib.forFoldr liveSets blocks (\b liveSets1 ->-    let {bid = Blocks.blockId binfo b} in-    case IntMap.coq_IntMap_lookup bid liveSets1 of {-     Prelude.Just liveSet ->-      let {-       liveSet2 = Lib.forFold liveSet (Blocks.blockSuccessors binfo b)-                    (\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)-                        (blockLiveIn sux)) (blockFirstOpId liveSet2)-                      (blockLastOpId liveSet2);-                     Prelude.Nothing -> liveSet2})}-      in-      IntMap.coq_IntMap_insert bid (Build_BlockLiveSets-        (blockLiveGen liveSet2) (blockLiveKill liveSet2)-        (IntMap.coq_IntSet_union-          (IntMap.coq_IntSet_difference (blockLiveOut liveSet2)-            (blockLiveKill liveSet2)) (blockLiveGen liveSet2))-        (blockLiveOut liveSet2) (blockFirstOpId liveSet2)-        (blockLastOpId liveSet2)) liveSets1;-     Prelude.Nothing -> liveSets1})+computeGlobalLiveSets :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 +                         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)))+    (Monad.forFoldrM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) liveSets+      blocks (\b liveSets1 ->+      Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\bid ->+        case IntMap.coq_IntMap_lookup bid liveSets1 of {+         Prelude.Just liveSet ->+          Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\suxs ->+            let {+             liveSet2 = Lib.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)+                              (blockLiveIn sux)) (blockFirstOpId liveSet2)+                            (blockLastOpId liveSet2);+                           Prelude.Nothing -> liveSet2})}+            in+            Monad.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)+                    (blockLiveKill liveSet2)) (blockLiveGen liveSet2))+                (blockLiveOut liveSet2) (blockFirstOpId liveSet2)+                (blockLastOpId liveSet2)) liveSets1))+            (unsafeCoerce (\_ -> Blocks.blockSuccessors mDict binfo b));+         Prelude.Nothing ->+          Monad.pure+            (unsafeCoerce+              (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))+            liveSets1}) (\_ -> Blocks.blockId mDict binfo b))) -computeGlobalLiveSetsRecursively :: (Blocks.BlockInfo a1 a2 a3 a4) -> ([] -                                    a1) -> (IntMap.IntMap BlockLiveSets) ->-                                    IntMap.IntMap BlockLiveSets-computeGlobalLiveSetsRecursively binfo blocks liveSets =+computeGlobalLiveSetsRecursively :: (Monad.Monad a5) -> (Blocks.BlockInfo +                                    a5 a1 a2 a3 a4) -> ([] a1) ->+                                    (IntMap.IntMap BlockLiveSets) -> a5+computeGlobalLiveSetsRecursively mDict binfo blocks liveSets =   let {    go n previous =      (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))        (\_ ->-       previous)+       Monad.pure (Monad.is_applicative mDict) previous)        (\n0 ->-       let {computed = computeGlobalLiveSets binfo blocks previous} in-       case Eqtype.eq_op (IntMap.coq_IntMap_eqType coq_BlockLiveSets_eqType)-              (unsafeCoerce previous) (unsafeCoerce computed) of {-        Prelude.True -> computed;-        Prelude.False -> go n0 computed})+       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.False -> unsafeCoerce go n0 computed})+         (computeGlobalLiveSets mDict binfo blocks previous))        n}   in go (Data.List.length blocks) liveSets 

@@ -1,3 +1,5 @@++ module LinearScan.Logic where  

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Loops where@@ -16,7 +16,8 @@ import qualified LinearScan.Blocks as Blocks import qualified LinearScan.IntMap as IntMap import qualified LinearScan.Lib as Lib-import qualified LinearScan.State as State+import qualified LinearScan.Monad as Monad+import qualified LinearScan.Yoneda as Yoneda import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Seq as Seq import qualified LinearScan.Ssrbool as Ssrbool@@ -24,13 +25,21 @@   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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 @@ -102,60 +111,60 @@     IntMap.emptyIntMap IntMap.emptyIntMap IntMap.emptyIntMap     IntMap.emptyIntMap -modifyActiveBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> State.State+modifyActiveBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> Monad.State                       LoopState () modifyActiveBlocks f =-  State.modify (\st -> Build_LoopState (f (activeBlocks st))+  Monad.modify (\st -> Build_LoopState (f (activeBlocks st))     (visitedBlocks st) (loopHeaderBlocks st) (loopEndBlocks st)     (forwardBranches st) (backwardBranches st) (loopIndices st)     (loopDepths st)) -modifyVisitedBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> State.State+modifyVisitedBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> Monad.State                        LoopState () modifyVisitedBlocks f =-  State.modify (\st -> Build_LoopState (activeBlocks st)+  Monad.modify (\st -> Build_LoopState (activeBlocks st)     (f (visitedBlocks st)) (loopHeaderBlocks st) (loopEndBlocks st)     (forwardBranches st) (backwardBranches st) (loopIndices st)     (loopDepths st))  modifyLoopHeaderBlocks :: (([] Blocks.BlockId) -> [] Blocks.BlockId) ->-                          State.State LoopState ()+                          Monad.State LoopState () modifyLoopHeaderBlocks f =-  State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)+  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)     (f (loopHeaderBlocks st)) (loopEndBlocks st) (forwardBranches st)     (backwardBranches st) (loopIndices st) (loopDepths st)) -modifyLoopEndBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> State.State+modifyLoopEndBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> Monad.State                        LoopState () modifyLoopEndBlocks f =-  State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)+  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)     (loopHeaderBlocks st) (f (loopEndBlocks st)) (forwardBranches st)     (backwardBranches st) (loopIndices st) (loopDepths st))  modifyForwardBranches :: ((IntMap.IntMap IntMap.IntSet) -> IntMap.IntMap-                         IntMap.IntSet) -> State.State LoopState ()+                         IntMap.IntSet) -> Monad.State LoopState () modifyForwardBranches f =-  State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)+  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)     (loopHeaderBlocks st) (loopEndBlocks st) (f (forwardBranches st))     (backwardBranches st) (loopIndices st) (loopDepths st))  modifyBackwardBranches :: ((IntMap.IntMap IntMap.IntSet) -> IntMap.IntMap-                          IntMap.IntSet) -> State.State LoopState ()+                          IntMap.IntSet) -> Monad.State LoopState () modifyBackwardBranches f =-  State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)+  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)     (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st)     (f (backwardBranches st)) (loopIndices st) (loopDepths st)) -setLoopIndices :: (IntMap.IntMap IntMap.IntSet) -> State.State LoopState ()+setLoopIndices :: (IntMap.IntMap IntMap.IntSet) -> Monad.State LoopState () setLoopIndices indices =-  State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)+  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)     (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st)     (backwardBranches st) indices (loopDepths st)) -setLoopDepths :: (IntMap.IntMap ((,) Prelude.Int Prelude.Int)) -> State.State+setLoopDepths :: (IntMap.IntMap ((,) Prelude.Int Prelude.Int)) -> Monad.State                  LoopState () setLoopDepths depths =-  State.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)+  Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st)     (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st)     (backwardBranches st) (loopIndices st) depths) @@ -169,244 +178,462 @@  pathToLoopHeader :: Blocks.BlockId -> Prelude.Int -> LoopState ->                     Prelude.Maybe IntMap.IntSet-pathToLoopHeader b header st =+pathToLoopHeader blk header st =   let {-   go fuel visited b0 =-     (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))-       (\_ ->-       Prelude.Nothing)-       (\n ->-       let {visited' = IntMap.coq_IntSet_insert b0 visited} in-       let {-        forwardPreds = case IntMap.coq_IntMap_lookup b0 (forwardBranches st) of {-                        Prelude.Just preds -> IntMap.coq_IntSet_toList preds;-                        Prelude.Nothing -> []}}-       in-       let {-        backwardPreds = case IntMap.coq_IntMap_lookup b0-                               (backwardBranches st) of {-                         Prelude.Just preds -> IntMap.coq_IntSet_toList preds;-                         Prelude.Nothing -> []}}-       in-       let {preds = (Prelude.++) forwardPreds backwardPreds} in-       Lib.forFold (Prelude.Just (IntMap.coq_IntSet_singleton b0))-         (unsafeCoerce preds) (\mxs pred ->-         case mxs of {-          Prelude.Just xs ->-           case Eqtype.eq_op Ssrnat.nat_eqType pred (unsafeCoerce header) of {-            Prelude.True -> Prelude.Just-             (IntMap.coq_IntSet_union xs-               (IntMap.coq_IntSet_singleton (unsafeCoerce pred)));-            Prelude.False ->-             case IntMap.coq_IntSet_member (unsafeCoerce pred) visited' of {-              Prelude.True -> Prelude.Just xs;-              Prelude.False ->-               case unsafeCoerce go n visited' pred of {-                Prelude.Just ys -> Prelude.Just-                 (IntMap.coq_IntSet_union xs ys);-                Prelude.Nothing -> Prelude.Nothing}}};-          Prelude.Nothing -> Prelude.Nothing}))-       fuel}-  in go (IntMap.coq_IntSet_size (visitedBlocks st)) IntMap.emptyIntSet b+   go = let {+         go fuel visited b =+           (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+             (\_ -> (,) visited+             Prelude.Nothing)+             (\n ->+             let {visited' = IntMap.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;+                              Prelude.Nothing -> []}}+             in+             let {+              backwardPreds = case IntMap.coq_IntMap_lookup b+                                     (backwardBranches st) of {+                               Prelude.Just preds ->+                                IntMap.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)+               (\mxs pred ->+               case mxs of {+                (,) vis o ->+                 case o of {+                  Prelude.Just xs ->+                   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))));+                    Prelude.False ->+                     case IntMap.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));+                          Prelude.Nothing -> (,) vis Prelude.Nothing}}}};+                  Prelude.Nothing -> mxs}}))+             fuel}+        in go}+  in+  Prelude.snd+    (go (IntMap.coq_IntSet_size (visitedBlocks st)) IntMap.emptyIntSet blk) -computeLoopDepths :: (Blocks.BlockInfo a1 a2 a3 a4) -> (IntMap.IntMap -                     a1) -> State.State LoopState ()-computeLoopDepths binfo bs =-  State.bind (\st ->-    let {-     m = Lib.forFold IntMap.emptyIntMap-           (IntMap.coq_IntSet_toList (loopEndBlocks st)) (\m endBlock ->-           case IntMap.coq_IntMap_lookup endBlock bs of {-            Prelude.Just b ->-             Lib.forFold m (unsafeCoerce (Blocks.blockSuccessors binfo b))-               (\m' sux ->-               let {-                loopIndex = Seq.find (\x ->-                              Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce x)-                                sux) (loopHeaderBlocks st)}-               in-               case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce loopIndex)-                      (unsafeCoerce (Data.List.length (loopHeaderBlocks st))) of {-                Prelude.True -> m';-                Prelude.False ->-                 let {mres = pathToLoopHeader endBlock (unsafeCoerce sux) st}-                 in-                 case mres of {-                  Prelude.Just path ->-                   Lib.forFold m' (IntMap.coq_IntSet_toList path)-                     (\m'' blk -> addReference loopIndex blk m'');-                  Prelude.Nothing -> m'}});-            Prelude.Nothing -> m})}-    in-    let {-     f = \acc loopIndex refs ->-      IntMap.coq_IntSet_forFold acc refs (\m' blk ->+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))++computeLoopDepths :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 +                     a4) -> (IntMap.IntMap a1) -> Monad.StateT LoopState +                     a5 ()+computeLoopDepths mDict binfo bs =+  Monad.bind (Monad.coq_StateT_Monad mDict) (\st ->+    Monad.bind (Monad.coq_StateT_Monad mDict) (\m ->+      let {+       f = \acc loopIndex refs ->+        IntMap.coq_IntSet_forFold acc refs (\m' blk ->+          let {+           f = \mx ->+            case mx of {+             Prelude.Just y ->+              case y of {+               (,) idx depth -> Prelude.Just ((,) (Prelude.min idx loopIndex)+                ((Prelude.succ) depth))};+             Prelude.Nothing -> Prelude.Just ((,) loopIndex ((Prelude.succ)+              0))}}+          in+          IntMap.coq_IntMap_alter f blk m')}+      in+      liftStateT mDict+        (Monad.bind (unsafeCoerce Monad.coq_State_Monad) (\x ->+          setLoopDepths+            (IntMap.coq_IntMap_foldlWithKey f IntMap.emptyIntMap m))+          (setLoopIndices m)))+      (Monad.lift mDict+        (Yoneda.iso_to+          (Yoneda.coq_Yoneda_lemma+            (Monad.is_functor (Monad.is_applicative mDict)))+          (Monad.forFoldM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict))+            IntMap.emptyIntMap (IntMap.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+                  (unsafeCoerce+                    (Yoneda.coq_Yoneda_Applicative+                      (Monad.is_applicative mDict)))+                  (Lib.forFold m suxs (\m' sux ->+                    let {headers = loopHeaderBlocks st} in+                    let {+                     loopIndex = Seq.find (\x ->+                                   Eqtype.eq_op Ssrnat.nat_eqType+                                     (unsafeCoerce x) sux) headers}+                    in+                    case Eqtype.eq_op Ssrnat.nat_eqType+                           (unsafeCoerce loopIndex)+                           (unsafeCoerce (Data.List.length headers)) of {+                     Prelude.True -> m';+                     Prelude.False ->+                      let {+                       mres = pathToLoopHeader endBlock (unsafeCoerce sux) st}+                      in+                      case mres of {+                       Prelude.Just path ->+                        Lib.forFold m' (IntMap.coq_IntSet_toList path)+                          (\m'' blk -> addReference loopIndex blk m'');+                       Prelude.Nothing -> m'}}))) (\_ ->+                Blocks.blockSuccessors mDict binfo b);+             Prelude.Nothing ->+              Monad.pure+                (unsafeCoerce+                  (Yoneda.coq_Yoneda_Applicative+                    (Monad.is_applicative mDict))) m})))))+    (Monad.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)))+    (Monad.forFoldM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict))+      IntMap.emptyIntMap bs (\acc b ->+      Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\bid ->         let {-         f = \mx ->-          case mx of {-           Prelude.Just y ->-            case y of {-             (,) idx depth -> Prelude.Just ((,) (Prelude.min idx loopIndex)-              ((Prelude.succ) depth))};-           Prelude.Nothing -> Prelude.Just ((,) loopIndex ((Prelude.succ) 0))}}+         g = \acc1 loopIndex blks ->+          case Prelude.not (IntMap.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))+                  (\acc2 op ->+                  Lib.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-        IntMap.coq_IntMap_alter f blk m')}-    in-    State.bind (\x ->-      setLoopDepths (IntMap.coq_IntMap_foldlWithKey f IntMap.emptyIntMap m))-      (setLoopIndices m)) State.get--computeVarReferences :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->-                        (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> LoopState ->-                        IntMap.IntMap IntMap.IntSet-computeVarReferences maxReg binfo oinfo bs st =-  Lib.forFold IntMap.emptyIntMap bs (\acc b ->-    let {bid = Blocks.blockId binfo b} in-    let {-     g = \acc1 loopIndex blks ->-      case Prelude.not (IntMap.coq_IntSet_member bid blks) of {-       Prelude.True -> acc1;-       Prelude.False ->-        case Blocks.blockOps binfo b of {-         (,) p zs ->-          case p of {-           (,) xs ys ->-            Lib.forFold acc1 ((Prelude.++) xs ((Prelude.++) ys zs))-              (\acc2 op ->-              Lib.forFold acc2 (Blocks.opRefs maxReg oinfo op) (\acc3 v ->-                case Blocks.varId maxReg v of {-                 Prelude.Left p0 -> acc3;-                 Prelude.Right vid -> addReference loopIndex vid acc3}))}}}}-    in-    IntMap.coq_IntMap_foldlWithKey g acc (loopIndices st))+        Monad.pure+          (unsafeCoerce+            (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))+          (IntMap.coq_IntMap_foldlWithKey g acc (loopIndices st))) (\_ ->+        Blocks.blockId mDict binfo b))) -findLoopEnds :: (Blocks.BlockInfo a1 a2 a3 a4) -> (IntMap.IntMap a1) ->-                State.State LoopState ()-findLoopEnds binfo bs =+findLoopEnds :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) ->+                (IntMap.IntMap a1) -> Monad.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))              (\_ ->-             State.pure ())+             Monad.pure (Monad.coq_StateT_Applicative mDict) ())              (\n0 ->-             let {bid = Blocks.blockId binfo b} in-             State.bind (\x ->-               State.bind (\x0 ->-                 State.bind (\x1 ->-                   modifyActiveBlocks (IntMap.coq_IntSet_delete bid))-                   (State.forM_ (Blocks.blockSuccessors binfo b) (\sux ->-                     State.bind (\active ->-                       State.bind (\x1 ->-                         State.bind (\visited ->-                           case IntMap.coq_IntSet_member sux visited of {-                            Prelude.True -> State.pure ();-                            Prelude.False ->-                             case IntMap.coq_IntMap_lookup sux bs of {-                              Prelude.Just x2 -> go n0 x2;-                              Prelude.Nothing -> State.pure ()}})-                           (State.gets visitedBlocks))-                         (case IntMap.coq_IntSet_member sux active of {-                           Prelude.True ->-                            State.bind (\x1 ->-                              State.bind (\x2 ->-                                modifyBackwardBranches (addReference sux bid))-                                (modifyLoopEndBlocks-                                  (IntMap.coq_IntSet_insert bid)))-                              (modifyLoopHeaderBlocks (\l ->-                                case Prelude.not-                                       (Ssrbool.in_mem (unsafeCoerce sux)-                                         (Ssrbool.mem-                                           (Seq.seq_predType-                                             Ssrnat.nat_eqType)-                                           (unsafeCoerce l))) of {-                                 Prelude.True -> (:) sux l;-                                 Prelude.False -> l}));-                           Prelude.False ->-                            modifyForwardBranches (addReference sux bid)}))-                       (State.gets activeBlocks))))-                 (modifyActiveBlocks (IntMap.coq_IntSet_insert bid)))-               (modifyVisitedBlocks (IntMap.coq_IntSet_insert bid)))+             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+                       (\sux ->+                       Monad.bind (Monad.coq_StateT_Monad mDict) (\active ->+                         Monad.bind (Monad.coq_StateT_Monad mDict) (\x0 ->+                           Monad.bind (Monad.coq_StateT_Monad mDict)+                             (\visited ->+                             case IntMap.coq_IntSet_member sux visited of {+                              Prelude.True ->+                               Monad.pure+                                 (Monad.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)+                               visitedBlocks))+                           (liftStateT mDict+                             (case IntMap.coq_IntSet_member sux active of {+                               Prelude.True ->+                                Monad.bind+                                  (unsafeCoerce Monad.coq_State_Monad)+                                  (\x0 ->+                                  Monad.bind+                                    (unsafeCoerce Monad.coq_State_Monad)+                                    (\x1 ->+                                    modifyBackwardBranches+                                      (addReference sux bid))+                                    (modifyLoopEndBlocks+                                      (IntMap.coq_IntSet_insert bid)))+                                  (modifyLoopHeaderBlocks (\l ->+                                    case Prelude.not+                                           (Ssrbool.in_mem (unsafeCoerce sux)+                                             (Ssrbool.mem+                                               (Seq.seq_predType+                                                 Ssrnat.nat_eqType)+                                               (unsafeCoerce l))) of {+                                     Prelude.True -> (:) sux l;+                                     Prelude.False -> l}));+                               Prelude.False ->+                                modifyForwardBranches (addReference sux bid)})))+                         (Monad.getsT (Monad.is_applicative mDict)+                           activeBlocks))))+                   (Monad.lift mDict+                     (Yoneda.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+                   (Yoneda.coq_Yoneda_lemma+                     (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->+                   Blocks.blockId mDict binfo b))))              n}         in go}   in   case IntMap.coq_IntMap_toList bs of {-   [] -> State.pure ();+   [] -> Monad.pure (Monad.coq_StateT_Applicative mDict) ();    (:) p l ->     case p of {-     (,) n b ->-      State.bind (\x -> computeLoopDepths binfo bs)-        (go (IntMap.coq_IntMap_size bs) b)}}+     (,) n b -> go (IntMap.coq_IntMap_size bs) b}} -computeBlockOrder :: (Blocks.BlockInfo a1 a2 a3 a4) -> ([] a1) -> (,)-                     LoopState ([] a1)-computeBlockOrder binfo blocks =+computeBlockOrder :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 +                     a4) -> ([] a1) -> a5+computeBlockOrder mDict binfo blocks =   case blocks of {-   [] -> (,) emptyLoopState [];+   [] -> Monad.pure (Monad.is_applicative mDict) ((,) emptyLoopState []);    (:) b bs ->-    let {-     blockMap = IntMap.coq_IntMap_fromList-                  (Prelude.map (\x -> (,) (Blocks.blockId binfo x) x) blocks)}-    in-    case findLoopEnds binfo blockMap emptyLoopState of {-     (,) u st ->-      let {-       isHeavier = \x y ->-        let {x_id = Blocks.blockId binfo x} in-        let {y_id = Blocks.blockId binfo y} in-        let {-         x_depth = case IntMap.coq_IntMap_lookup x_id (loopDepths st) of {-                    Prelude.Just p ->-                     case p of {-                      (,) idx depth -> depth};-                    Prelude.Nothing -> 0}}-        in-        let {-         y_depth = case IntMap.coq_IntMap_lookup y_id (loopDepths st) of {-                    Prelude.Just p ->-                     case p of {-                      (,) idx depth -> depth};-                    Prelude.Nothing -> 0}}-        in-        (Prelude.<=) ((Prelude.succ) y_depth) x_depth}-      in-      let {-       go = let {-             go n branches work_list =-               (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))-                 (\_ ->-                 [])-                 (\n0 ->-                 case work_list of {-                  [] -> [];-                  (:) w ws ->-                   case let {bid = Blocks.blockId binfo w} in-                        let {suxs = Blocks.blockSuccessors binfo w} in-                        Lib.forFoldr ((,) branches ws) suxs (\sux acc ->-                          case acc of {-                           (,) branches' ws' ->-                            let {-                             insertion = case IntMap.coq_IntMap_lookup sux-                                                blockMap of {-                                          Prelude.Just s ->-                                           Lib.insert isHeavier s ws';-                                          Prelude.Nothing -> ws'}}-                            in-                            case IntMap.coq_IntMap_lookup sux branches' of {-                             Prelude.Just incs -> (,)-                              (IntMap.coq_IntMap_insert sux-                                (IntMap.coq_IntSet_delete bid incs)-                                branches')-                              (case Eqtype.eq_op Ssrnat.nat_eqType-                                      (unsafeCoerce-                                        (IntMap.coq_IntSet_size incs))-                                      (unsafeCoerce ((Prelude.succ) 0)) of {-                                Prelude.True -> insertion;-                                Prelude.False -> ws'});-                             Prelude.Nothing -> (,) branches' insertion}}) of {-                    (,) branches' ws' -> (:) w (go n0 branches' ws')}})-                 n}-            in go}-      in-      (,) st (go (Data.List.length blocks) (forwardBranches st) ((:) b []))}}+    Monad.bind mDict (\keys ->+      let {blockMap = IntMap.coq_IntMap_fromList keys} in+      Monad.bind mDict (\z ->+        case z of {+         (,) y st0 ->+          Monad.bind mDict (\blocks' ->+            Monad.bind mDict (\keys' ->+              let {blockMap' = IntMap.coq_IntMap_fromList keys'} in+              Monad.bind mDict (\z' ->+                case z' of {+                 (,) y0 st1 ->+                  case blocks' of {+                   [] ->+                    Monad.pure (Monad.is_applicative mDict) ((,)+                      emptyLoopState []);+                   (:) b' bs' ->+                    Monad.bind mDict (\w ->+                      case w of {+                       (,) y1 st2 ->+                        let {+                         isHeavier = \x y2 ->+                          Monad.bind mDict (\x_id ->+                            Monad.bind mDict (\y_id ->+                              let {+                               x_depth = case IntMap.coq_IntMap_lookup x_id+                                                (loopDepths st2) of {+                                          Prelude.Just p ->+                                           case p of {+                                            (,) idx depth -> depth};+                                          Prelude.Nothing -> 0}}+                              in+                              let {+                               y_depth = case IntMap.coq_IntMap_lookup y_id+                                                (loopDepths st2) of {+                                          Prelude.Just p ->+                                           case p of {+                                            (,) idx depth -> depth};+                                          Prelude.Nothing -> 0}}+                              in+                              Monad.pure (Monad.is_applicative mDict)+                                ((Prelude.<=) ((Prelude.succ) y_depth)+                                  x_depth))+                              (Yoneda.iso_to+                                (Yoneda.coq_Yoneda_lemma+                                  (Monad.is_functor+                                    (Monad.is_applicative mDict))) (\_ ->+                                Blocks.blockId mDict binfo y2)))+                            (Yoneda.iso_to+                              (Yoneda.coq_Yoneda_lemma+                                (Monad.is_functor+                                  (Monad.is_applicative mDict))) (\_ ->+                              Blocks.blockId mDict binfo x))}+                        in+                        let {+                         go = let {+                               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) [])+                                   (\n0 ->+                                   case work_list of {+                                    [] ->+                                     Monad.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+                                                 (Monad.is_applicative mDict))+                                               (\x0 -> (:) w0 x0)+                                               (go n0 branches' ws')})+                                           (Monad.forFoldM mDict ((,)+                                             branches ws) suxs (\acc sux ->+                                             case acc of {+                                              (,) branches' ws' ->+                                               Monad.bind mDict+                                                 (\insertion ->+                                                 Monad.pure+                                                   (Monad.is_applicative+                                                     mDict)+                                                   (case IntMap.coq_IntMap_lookup+                                                           sux branches' of {+                                                     Prelude.Just incs -> (,)+                                                      (IntMap.coq_IntMap_insert+                                                        sux+                                                        (IntMap.coq_IntSet_delete+                                                          bid incs)+                                                        branches')+                                                      (case Eqtype.eq_op+                                                              Ssrnat.nat_eqType+                                                              (unsafeCoerce+                                                                (IntMap.coq_IntSet_size+                                                                  incs))+                                                              (unsafeCoerce+                                                                ((Prelude.succ)+                                                                0)) of {+                                                        Prelude.True ->+                                                         insertion;+                                                        Prelude.False -> ws'});+                                                     Prelude.Nothing -> (,)+                                                      branches' insertion}))+                                                 (case IntMap.coq_IntMap_lookup+                                                         sux blockMap' of {+                                                   Prelude.Just s ->+                                                    Monad.insertM mDict+                                                      isHeavier s ws';+                                                   Prelude.Nothing ->+                                                    Monad.pure+                                                      (Monad.is_applicative+                                                        mDict) ws'})})))+                                         (Yoneda.iso_to+                                           (Yoneda.coq_Yoneda_lemma+                                             (Monad.is_functor+                                               (Monad.is_applicative mDict)))+                                           (\_ ->+                                           Blocks.blockSuccessors mDict binfo+                                             w0)))+                                       (Yoneda.iso_to+                                         (Yoneda.coq_Yoneda_lemma+                                           (Monad.is_functor+                                             (Monad.is_applicative mDict)))+                                         (\_ ->+                                         Blocks.blockId mDict binfo w0))})+                                   n}+                              in go}+                        in+                        Monad.bind mDict (\res ->+                          Monad.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+                    (Yoneda.coq_Yoneda_lemma+                      (Monad.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);+                 Prelude.False ->+                  Monad.fmap (Monad.is_functor (Monad.is_applicative mDict))+                    (\x ->+                    case x of {+                     (,) b' rest' -> (:) b' rest'})+                    (Monad.forFoldrM mDict ((,) b0 rest) suxs (\sux x ->+                      case x of {+                       (,) b' rest' ->+                        let {+                         fsz = case IntMap.coq_IntMap_lookup sux+                                      (forwardBranches st0) of {+                                Prelude.Just fwds ->+                                 IntMap.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;+                                Prelude.Nothing -> 0}}+                        in+                        case (Prelude.<=) ((Prelude.+) fsz bsz)+                               ((Prelude.succ) 0) of {+                         Prelude.True ->+                          Monad.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+                                (Yoneda.coq_Yoneda_lemma+                                  (Monad.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+                  (Yoneda.coq_Yoneda_lemma+                    (Monad.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+            (Yoneda.coq_Yoneda_lemma+              (Monad.is_functor (Monad.is_applicative mDict))) (\_ ->+            Blocks.blockId mDict binfo x))) blocks)} 

@@ -1,3 +1,5 @@++ module LinearScan.Main where  @@ -15,8 +17,11 @@ 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.Resolve as Resolve import qualified LinearScan.ScanState as ScanState@@ -27,52 +32,94 @@    BuildingIntervalsFailed  | AllocatingRegistersFailed -data Details blockType1 blockType2 opType1 opType2 accType =+data ScanStateDescSet =+   Build_ScanStateDescSet Prelude.Int ([] Interval.IntervalDesc) ([]+                                                                 (Prelude.Maybe+                                                                 Interval.IntervalDesc)) + ([] ((,) Prelude.Int Prelude.Int)) ([] ((,) Prelude.Int Prelude.Int)) + ([] ((,) Prelude.Int Prelude.Int)) ([]+                                    ((,) Prelude.Int+                                    (Prelude.Maybe Prelude.Int)))++toScanStateDescSet :: Prelude.Int -> ScanState.ScanStateDesc ->+                      ScanStateDescSet+toScanStateDescSet maxReg sd =+  Build_ScanStateDescSet (ScanState.nextInterval maxReg sd)+    (LinearScan.Utils.vmap (ScanState.nextInterval maxReg sd) (\x ->+      Interval.getIntervalDesc ( x)) (ScanState.intervals maxReg sd))+    (LinearScan.Utils.vmap maxReg (\mx ->+      case mx of {+       Prelude.Just x -> Prelude.Just (Interval.getIntervalDesc ( x));+       Prelude.Nothing -> Prelude.Nothing})+      (ScanState.fixedIntervals maxReg sd))+    (Prelude.map (\i -> (,) ( (Prelude.fst i)) (Prelude.snd i))+      (ScanState.unhandled maxReg sd))+    (Prelude.map (\i -> (,) ( (Prelude.fst i)) ( (Prelude.snd i)))+      (ScanState.active maxReg sd))+    (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)))+      (ScanState.handled maxReg sd))++data Details blockType1 blockType2 =    Build_Details (Prelude.Maybe ((,) Morph.SSError FinalStage)) (IntMap.IntMap                                                                 LiveSets.BlockLiveSets) - ([] blockType1) ([] blockType2) accType (Prelude.Maybe-                                         ScanState.ScanStateDesc) (Prelude.Maybe-                                                                  ScanState.ScanStateDesc) - (Blocks.BlockInfo blockType1 blockType2 opType1 opType2) (Blocks.OpInfo-                                                          accType opType1-                                                          opType2) Loops.LoopState+ ([] blockType1) ([] blockType2) (Prelude.Maybe ScanStateDescSet) (Prelude.Maybe+                                                                  ScanStateDescSet) + Loops.LoopState -linearScan :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) -> (Blocks.OpInfo-              a5 a3 a4) -> ([] a1) -> a5 -> Details a1 a2 a3 a4 a5-linearScan maxReg binfo oinfo blocks accum =-  case Loops.computeBlockOrder binfo blocks of {-   (,) loops blocks1 ->-    let {liveSets = LiveSets.computeLocalLiveSets maxReg binfo oinfo blocks1}-    in-    let {-     liveSets' = LiveSets.computeGlobalLiveSetsRecursively binfo blocks1-                   liveSets}-    in-    case Build.buildIntervals maxReg binfo oinfo blocks1 loops liveSets' of {-     Prelude.Left err -> Build_Details (Prelude.Just ((,) err-      BuildingIntervalsFailed)) liveSets' blocks1 [] accum Prelude.Nothing-      Prelude.Nothing binfo oinfo loops;-     Prelude.Right ssig ->-      let {opCount = (Prelude.succ) (Blocks.countOps binfo blocks1)} in-      case Allocate.walkIntervals maxReg ( ssig) opCount of {-       Prelude.Left p ->-        case p of {-         (,) err ssig' -> Build_Details (Prelude.Just ((,) err-          AllocatingRegistersFailed)) liveSets' blocks1 [] accum-          (Prelude.Just ( ssig)) (Prelude.Just ( ssig')) binfo oinfo loops};-       Prelude.Right ssig' ->-        let {-         sd = Allocate.finalizeScanState maxReg ( ssig')-                (Ssrnat.double opCount)}-        in-        let {allocs = Resolve.determineAllocations maxReg sd} in-        let {-         mappings = Resolve.resolveDataFlow maxReg binfo allocs blocks1-                      liveSets'}-        in-        case Assign.assignRegNum maxReg binfo oinfo allocs liveSets' mappings-               blocks1 accum of {-         (,) blocks2 accum' -> Build_Details Prelude.Nothing liveSets'-          blocks1 blocks2 accum' (Prelude.Just ( ssig)) (Prelude.Just sd)-          binfo oinfo loops}}}}+linearScan :: (Monad.Monad a1) -> Prelude.Int -> (Blocks.BlockInfo a1 +              a2 a3 a4 a5) -> (Blocks.OpInfo a1 a4 a5) -> ([] a2) ->+              ((Details a2 a3) -> a6) -> a1+linearScan dict maxReg binfo oinfo blocks k =+  Monad.bind dict (\z ->+    case z of {+     (,) 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' blocks1 []+                  Prelude.Nothing Prelude.Nothing loops));+             Prelude.Right 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' ->+                  Monad.pure (Monad.is_applicative dict)+                    (k (Build_Details (Prelude.Just ((,) err+                      AllocatingRegistersFailed)) liveSets' 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' 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+            liveSets))+        (LiveSets.computeLocalLiveSets maxReg dict binfo oinfo blocks1)})+    (Loops.computeBlockOrder dict binfo blocks) 

@@ -0,0 +1,251 @@+{-# OPTIONS_GHC -cpp -XMagicHash #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Monad 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++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)++is_applicative :: (Monad a1) -> Applicative a1+is_applicative monad =+  case monad of {+   Build_Monad is_applicative0 join0 -> is_applicative0}++join :: (Monad a1) -> a1 -> a1+join monad x =+  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)++mapM :: (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)}++mapM_ :: (Monad a1) -> (a2 -> a1) -> ([] a2) -> a1+mapM_ h f l =+  case l of {+   [] -> pure (is_applicative h) ();+   (:) x xs -> bind h (\x0 -> mapM_ h f xs) (f x)}++forM_ :: (Monad a1) -> ([] a2) -> (a2 -> a1) -> a1+forM_ h l f =+  mapM_ h f l++foldM :: (Monad a1) -> (a2 -> a3 -> a1) -> a2 -> ([] a3) -> a1+foldM h f s l =+  case l of {+   [] -> 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+forFoldM h s l f =+  foldM h f s l++foldrM :: (Monad a1) -> (a3 -> a2 -> a1) -> a2 -> ([] a3) -> a1+foldrM h f s l =+  case l of {+   [] -> 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 h f l =+  fmap (is_functor h) 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 []);+   (:) 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+

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Morph where@@ -14,6 +14,8 @@ import qualified LinearScan.Utils  import qualified LinearScan.IState as IState+import qualified LinearScan.Interval as Interval+import qualified LinearScan.Lib as Lib import qualified LinearScan.Logic as Logic import qualified LinearScan.ScanState as ScanState import qualified LinearScan.Specif as Specif@@ -21,16 +23,25 @@ import qualified LinearScan.Fintype as Fintype import qualified LinearScan.Seq as Seq import qualified LinearScan.Ssrbool as Ssrbool+import qualified LinearScan.Ssrnat as Ssrnat   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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 @@ -39,18 +50,34 @@  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 =-   ERegistersExhausted Prelude.Int- | ENoValidSplitPositionUnh Prelude.Int Prelude.Int- | ENoValidSplitPosition Prelude.Int Prelude.Int- | ECannotSplitSingleton1 Prelude.Int- | ECannotSplitSingleton2 Prelude.Int- | ECannotSplitSingleton3 Prelude.Int- | ENoIntervalsToSplit+   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- | EFuelExhausted  | 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@@ -138,10 +165,41 @@       unhandled0 active0 inactive0 handled0 ->       case unhandled0 of {        [] -> Logic.coq_False_rect;-       (:) p unhandled1 -> Prelude.Right ((,) () (Build_SSInfo-        (ScanState.Build_ScanStateDesc nextInterval0 intervals0-        fixedIntervals0 unhandled1 active0 inactive0 ((:) ((,)-        (Prelude.fst p) Prelude.Nothing) handled0)) __))}}}+       (:) p unhandled1 ->+        case p of {+         (,) i n ->+          let {+           _evar_0_ = \_ -> Prelude.Right ((,) () (Build_SSInfo+            (ScanState.Build_ScanStateDesc nextInterval0 intervals0+            fixedIntervals0 unhandled1 active0 inactive0 ((:) ((,)+            (Prelude.fst ((,) i n)) Prelude.Nothing) handled0)) __))}+          in+          let {+           _evar_0_0 = \_ -> Prelude.Left (ECannotSpillIfRegisterRequired+            ( i))}+          in+          case Eqtype.eq_op+                 (Eqtype.option_eqType+                   (Eqtype.sig_eqType+                     (Eqtype.sig_eqType Ssrnat.nat_eqType+                       (unsafeCoerce Ssrnat.odd)) (\u ->+                     (Prelude.&&)+                       ((Prelude.<=)+                         (Interval.ibeg+                           (+                             (LinearScan.Utils.nth nextInterval0 intervals0+                               i))) ( (unsafeCoerce u)))+                       ((Prelude.<=) ( (unsafeCoerce u))+                         (Interval.iend+                           (+                             (LinearScan.Utils.nth nextInterval0 intervals0+                               i)))))))+                 (unsafeCoerce+                   (Interval.firstUseReqReg+                     ( (LinearScan.Utils.nth nextInterval0 intervals0 i))))+                 (unsafeCoerce Prelude.Nothing) of {+           Prelude.True -> _evar_0_ __;+           Prelude.False -> _evar_0_0 __}}}}}  moveUnhandledToActive :: Prelude.Int -> ScanState.ScanStateDesc -> PhysReg ->                          SState () () ()@@ -171,10 +229,10 @@          Prelude.True -> _evar_0_ __;          Prelude.False -> _evar_0_0 __}}}} -moveActiveToHandled :: Prelude.Int -> ScanState.ScanStateDesc ->-                       Eqtype.Equality__Coq_sort -> Specif.Coq_sig2+moveActiveToHandled :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Bool+                       -> Eqtype.Equality__Coq_sort -> Specif.Coq_sig2                        ScanState.ScanStateDesc-moveActiveToHandled maxReg sd x =+moveActiveToHandled maxReg sd spilled x =   ScanState.Build_ScanStateDesc (ScanState.nextInterval maxReg sd)     (ScanState.intervals maxReg sd) (ScanState.fixedIntervals maxReg sd)     (ScanState.unhandled maxReg sd)@@ -185,7 +243,9 @@           (Fintype.ordinal_eqType maxReg)) x         (unsafeCoerce (ScanState.active maxReg sd))))     (ScanState.inactive maxReg sd) ((:) ((,) (Prelude.fst (unsafeCoerce x))-    (Prelude.Just (Prelude.snd (unsafeCoerce x))))+    (case spilled of {+      Prelude.True -> Prelude.Nothing;+      Prelude.False -> Prelude.Just (Prelude.snd (unsafeCoerce x))}))     (ScanState.handled maxReg sd))  moveActiveToInactive :: Prelude.Int -> ScanState.ScanStateDesc ->@@ -220,9 +280,9 @@     (ScanState.handled maxReg sd)  moveInactiveToHandled :: Prelude.Int -> ScanState.ScanStateDesc ->-                         Eqtype.Equality__Coq_sort -> Specif.Coq_sig2-                         ScanState.ScanStateDesc-moveInactiveToHandled maxReg sd x =+                         Prelude.Bool -> Eqtype.Equality__Coq_sort ->+                         Specif.Coq_sig2 ScanState.ScanStateDesc+moveInactiveToHandled maxReg sd spilled x =   ScanState.Build_ScanStateDesc (ScanState.nextInterval maxReg sd)     (ScanState.intervals maxReg sd) (ScanState.fixedIntervals maxReg sd)     (ScanState.unhandled maxReg sd) (ScanState.active maxReg sd)@@ -232,6 +292,9 @@           (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd))           (Fintype.ordinal_eqType maxReg)) x         (unsafeCoerce (ScanState.inactive maxReg sd)))) ((:) ((,)-    (Prelude.fst (unsafeCoerce x)) (Prelude.Just-    (Prelude.snd (unsafeCoerce x)))) (ScanState.handled maxReg sd))+    (Prelude.fst (unsafeCoerce x))+    (case spilled of {+      Prelude.True -> Prelude.Nothing;+      Prelude.False -> Prelude.Just (Prelude.snd (unsafeCoerce x))}))+    (ScanState.handled maxReg sd)) 

@@ -1,3 +1,5 @@++ module LinearScan.NonEmpty0 where  

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Range where@@ -23,13 +23,21 @@   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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 

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Resolve where@@ -13,54 +13,41 @@ import qualified Data.Functor.Identity import qualified LinearScan.Utils +import qualified LinearScan.Allocate as Allocate import qualified LinearScan.Blocks as Blocks import qualified LinearScan.Graph as Graph import qualified LinearScan.IntMap as IntMap import qualified LinearScan.Interval as Interval import qualified LinearScan.Lib as Lib import qualified LinearScan.LiveSets as LiveSets-import qualified LinearScan.ScanState as ScanState+import qualified LinearScan.Monad as Monad import qualified LinearScan.UsePos as UsePos+import qualified LinearScan.Yoneda as Yoneda import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Fintype as Fintype import qualified LinearScan.Ssrnat as Ssrnat   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+import qualified GHC.Prim as GHC.Prim #else -- HUGS import qualified LinearScan.IOExts as IOExts-unsafeCoerce = IOExts.unsafeCoerce #endif -type PhysReg = Prelude.Int -data Allocation =-   Build_Allocation Prelude.Int Interval.IntervalDesc (Prelude.Maybe PhysReg)--intVal :: Prelude.Int -> Allocation -> Interval.IntervalDesc-intVal maxReg a =-  case a of {-   Build_Allocation intId intVal0 intReg0 -> intVal0}--intReg :: Prelude.Int -> Allocation -> Prelude.Maybe PhysReg-intReg maxReg a =-  case a of {-   Build_Allocation intId intVal0 intReg0 -> intReg0}+#ifdef __GLASGOW_HASKELL__+--unsafeCoerce :: a -> b+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+--unsafeCoerce :: a -> b+unsafeCoerce = IOExts.unsafeCoerce+#endif -determineAllocations :: Prelude.Int -> ScanState.ScanStateDesc -> []-                        Allocation-determineAllocations maxReg sd =-  Prelude.map (\x -> Build_Allocation ( (Prelude.fst x))-    (Interval.getIntervalDesc-      (-        (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)-          (ScanState.intervals maxReg sd) (Prelude.fst x)))) (Prelude.snd x))-    (ScanState.handled maxReg sd)+type PhysReg = Prelude.Int  type RawResolvingMove = (,) (Prelude.Maybe PhysReg) (Prelude.Maybe PhysReg) @@ -140,24 +127,27 @@       (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType)       graph) -resolvingMoves :: Prelude.Int -> ([] Allocation) -> Prelude.Int ->+resolvingMoves :: Prelude.Int -> ([] Allocate.Allocation) -> Prelude.Int ->                   Prelude.Int -> IntMap.IntMap RawResolvingMove resolvingMoves maxReg allocs from to =   let {    liveAtFrom = IntMap.coq_IntMap_fromList-                  (Prelude.map (\i -> (,) (Interval.ivar (intVal maxReg i))-                    i)+                  (Prelude.map (\i -> (,)+                    (Interval.ivar (Allocate.intVal maxReg i)) i)                     (Prelude.filter (\i ->                       (Prelude.&&)-                        ((Prelude.<=) (Interval.ibeg (intVal maxReg i)) from)+                        ((Prelude.<=)+                          (Interval.ibeg (Allocate.intVal maxReg i)) from)                         ((Prelude.<=) ((Prelude.succ) from)-                          (Interval.iend (intVal maxReg i)))) allocs))}+                          (Interval.iend (Allocate.intVal maxReg i))))+                      allocs))}   in   let {    liveAtTo = IntMap.coq_IntMap_fromList-                (Prelude.map (\i -> (,) (Interval.ivar (intVal maxReg i)) i)+                (Prelude.map (\i -> (,)+                  (Interval.ivar (Allocate.intVal maxReg i)) i)                   (Prelude.filter (\i ->-                    let {int = intVal maxReg i} in+                    let {int = Allocate.intVal maxReg i} in                     (Prelude.&&) ((Prelude.<=) (Interval.ibeg int) to)                       (case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce to)                               (unsafeCoerce (Interval.iend int)) of {@@ -171,13 +161,15 @@   in   IntMap.coq_IntMap_mergeWithKey (\vid x y ->     case Eqtype.eq_op (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))-           (unsafeCoerce (intReg maxReg x)) (unsafeCoerce (intReg maxReg y)) of {+           (unsafeCoerce (Allocate.intReg maxReg x))+           (unsafeCoerce (Allocate.intReg maxReg y)) of {      Prelude.True -> Prelude.Nothing;-     Prelude.False -> Prelude.Just ((,) (intReg maxReg x) (intReg maxReg y))})-    (\x -> IntMap.emptyIntMap) (\x -> IntMap.emptyIntMap) liveAtFrom liveAtTo+     Prelude.False -> Prelude.Just ((,) (Allocate.intReg maxReg x)+      (Allocate.intReg maxReg y))}) (\x -> IntMap.emptyIntMap) (\x ->+    IntMap.emptyIntMap) liveAtFrom liveAtTo -checkBlockBoundary :: Prelude.Int -> ([] Allocation) -> Prelude.Int ->-                      Prelude.Bool -> LiveSets.BlockLiveSets ->+checkBlockBoundary :: Prelude.Int -> ([] Allocate.Allocation) -> Prelude.Int+                      -> Prelude.Bool -> LiveSets.BlockLiveSets ->                       LiveSets.BlockLiveSets -> IntMap.IntSet ->                       (IntMap.IntMap ((,) Graph.Graph Graph.Graph)) ->                       IntMap.IntMap ((,) Graph.Graph Graph.Graph)@@ -226,29 +218,40 @@  type BlockMoves = (,) Graph.Graph Graph.Graph -resolveDataFlow :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) -> ([]-                   Allocation) -> ([] a1) -> (IntMap.IntMap-                   LiveSets.BlockLiveSets) -> IntMap.IntMap BlockMoves-resolveDataFlow maxReg binfo allocs blocks liveSets =-  Lib.forFold IntMap.emptyIntMap blocks (\mappings b ->-    let {bid = Blocks.blockId binfo b} in-    case IntMap.coq_IntMap_lookup bid liveSets of {-     Prelude.Just from ->-      let {successors = Blocks.blockSuccessors binfo b} in-      let {-       in_from = (Prelude.<=) (Data.List.length successors) ((Prelude.succ)-                   0)}-      in-      Lib.forFold mappings successors (\ms s_bid ->-        case IntMap.coq_IntMap_lookup s_bid liveSets of {-         Prelude.Just to ->-          let {-           key = case in_from of {-                  Prelude.True -> bid;-                  Prelude.False -> s_bid}}-          in-          checkBlockBoundary maxReg allocs key in_from from to-            (LiveSets.blockLiveIn to) ms;-         Prelude.Nothing -> ms});-     Prelude.Nothing -> mappings})+resolveDataFlow :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo +                   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)))+    (Monad.forFoldM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict))+      IntMap.emptyIntMap blocks (\mappings b ->+      Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\bid ->+        case IntMap.coq_IntMap_lookup bid liveSets of {+         Prelude.Just from ->+          Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\suxs ->+            let {+             in_from = (Prelude.<=) (Data.List.length suxs) ((Prelude.succ)+                         0)}+            in+            Monad.pure+              (unsafeCoerce+                (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))+              (Lib.forFold mappings suxs (\ms s_bid ->+                case IntMap.coq_IntMap_lookup s_bid liveSets of {+                 Prelude.Just to ->+                  let {+                   key = case in_from of {+                          Prelude.True -> bid;+                          Prelude.False -> s_bid}}+                  in+                  checkBlockBoundary maxReg allocs key in_from from to+                    (LiveSets.blockLiveIn to) ms;+                 Prelude.Nothing -> ms})))+            (unsafeCoerce (\_ -> Blocks.blockSuccessors mDict binfo b));+         Prelude.Nothing ->+          Monad.pure+            (unsafeCoerce+              (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))+            mappings}) (\_ -> Blocks.blockId mDict binfo b))) 

@@ -1,3 +1,5 @@++ module LinearScan.ScanState where  

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Seq where@@ -21,13 +21,21 @@   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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 

@@ -1,3 +1,5 @@++ module LinearScan.Specif where  

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Split where@@ -27,13 +27,21 @@   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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 @@ -42,22 +50,434 @@  type PhysReg = Prelude.Int -data SplitPosition =-   BeforePos Lib.Coq_oddnum- | EndOfLifetimeHole Lib.Coq_oddnum--splitPosition :: Interval.IntervalDesc -> SplitPosition -> Lib.Coq_oddnum+splitPosition :: Interval.IntervalDesc -> Morph.SplitPosition ->+                 Lib.Coq_oddnum splitPosition d pos =   case pos of {-   BeforePos n -> n;-   EndOfLifetimeHole n ->+   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.$)) __ (\_ _ ->+                                      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.$)) __ (\_ _ ->+                                      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.$)) __ (\_ _ ->+                                      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)) ->-                          SplitPosition -> Prelude.Either Morph.SSError-                          (Prelude.Maybe ScanState.ScanStateSig)+                          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 ->@@ -92,7 +512,6 @@                                                _evar_0_0 = (Prelude.flip (Prelude.$))                                                              __ (\_ _ ->                                                              Prelude.Right-                                                             (Prelude.Just                                                              (ScanState.packScanState                                                                maxReg                                                                ScanState.InUse@@ -130,7 +549,7 @@                                                                  _inactive_)                                                                (Prelude.map                                                                  Prelude.id-                                                                 _handled_)))))}+                                                                 _handled_))))}                                               in                                                _evar_0_0}                                  in@@ -153,8 +572,8 @@        Interval.Build_IntervalDesc x x0 x1 x2 -> _evar_0_ x x0 x1 x2}}     in     let {-     _evar_0_0 = \_ -> Prelude.Left (Morph.ENoValidSplitPositionUnh ( uid0)-      splitPos)}+     _evar_0_0 = \_ -> Prelude.Left (Morph.ENoValidSplitPositionUnh pos+      ( uid0))}     in     case (Prelude.&&)            ((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int))) splitPos)@@ -167,7 +586,7 @@     _evar_0_ x x0 x1 x2 x3 x4 x5 uid us}  splitCurrentInterval :: Prelude.Int -> ScanState.ScanStateDesc ->-                        SplitPosition -> Morph.SState () () ()+                        Morph.SplitPosition -> Morph.SState () () () splitCurrentInterval maxReg pre pos ssi =   let {    _evar_0_ = \desc ->@@ -180,17 +599,8 @@          _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 ->-            let {-             _evar_0_1 = \_top_assumption_2 -> Prelude.Right ((,) ()-              (Morph.Build_SSInfo _top_assumption_2 __))}-            in-            let {-             _evar_0_2 = Prelude.Left (Morph.ECannotSplitSingleton1 ( uid0))}-            in-            case _top_assumption_1 of {-             Prelude.Just x -> _evar_0_1 x;-             Prelude.Nothing -> _evar_0_2}}+           _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;@@ -215,200 +625,114 @@ splitActiveOrInactiveInterval :: Prelude.Int -> ScanState.ScanStateDesc ->                                  ScanState.IntervalId -> Prelude.Int -> ([]                                  ((,) ScanState.IntervalId Prelude.Int)) ->-                                 ScanState.IntervalId -> SplitPosition ->+                                 ScanState.IntervalId -> Morph.SplitPosition+                                 -> PhysReg -> (Prelude.Either () ()) ->                                  Prelude.Either Morph.SSError-                                 (Prelude.Maybe ScanState.ScanStateSig)-splitActiveOrInactiveInterval maxReg sd uid beg us xid pos =+                                 ScanState.ScanStateSig+splitActiveOrInactiveInterval maxReg sd uid beg us xid pos reg hin =   let {-   _evar_0_ = \_nextInterval_ ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 us0 xid0 ->-    let {int = LinearScan.Utils.nth _nextInterval_ ints xid0} in+   _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 {-     _evar_0_ = \_ ->+     sd0 = ScanState.Build_ScanStateDesc ni ints _fixedIntervals_ unh+      _active_ _inactive_ _handled_}+    in+    (Prelude.flip (Prelude.$)) __ (\_ ->       let {-       _evar_0_ = \iv ib ie rds ->-        let {-         _top_assumption_ = Interval.splitInterval-                              (Interval.Build_IntervalDesc iv ib ie rds)-                              splitPos}-        in+       _evar_0_ = \_ ->         let {-         _evar_0_ = \i0 i1 ->+         _evar_0_ = \iv ib ie rds ->           let {-           _evar_0_ = let {-                       _evar_0_ = \_ _ ->-                        let {-                         _evar_0_ = \_top_assumption_0 ->+           _top_assumption_ = Interval.splitInterval+                                (Interval.Build_IntervalDesc iv ib ie rds)+                                splitPos}+          in+          let {+           _evar_0_ = \i0 i1 ->+            let {+             _evar_0_ = let {+                         _evar_0_ = \_ _ ->                           let {-                           _evar_0_ = \_ ->-                            (Prelude.flip (Prelude.$)) __-                              (let {-                                _evar_0_ = let {-                                            _evar_0_ = \_ _ -> Prelude.Left-                                             (Morph.ENoValidSplitPosition-                                             ( xid0) _top_assumption_0)}-                                           in-                                           let {-                                            _evar_0_0 = \_ ->-                                             let {-                                              _evar_0_0 = \_ _ ->-                                               Prelude.Right (Prelude.Just-                                               (ScanState.packScanState-                                                 maxReg ScanState.InUse-                                                 (ScanState.Build_ScanStateDesc-                                                 ((Prelude.succ)-                                                 _nextInterval_)-                                                 (LinearScan.Utils.snoc-                                                   _nextInterval_-                                                   (LinearScan.Utils.set_nth-                                                     _nextInterval_ ints xid0-                                                     ( i0)) ( i1))-                                                 _fixedIntervals_-                                                 (Lib.insert-                                                   (Lib.lebf Prelude.snd)-                                                   ((,) ( _nextInterval_)-                                                   (Interval.ibeg ( i1)))-                                                   ((:)-                                                   (Prelude.id ((,) uid0-                                                     beg))-                                                   (Prelude.map Prelude.id-                                                     us0)))-                                                 (Prelude.map Prelude.id-                                                   _active_)-                                                 (Prelude.map Prelude.id-                                                   _inactive_)-                                                 (Prelude.map Prelude.id-                                                   _handled_))))}-                                             in-                                              _evar_0_0 __}-                                           in-                                           case (Prelude.<=)-                                                  (Interval.ibeg ( i1)) beg of {-                                            Prelude.True -> _evar_0_ __;-                                            Prelude.False -> _evar_0_0 __}}-                               in-                                _evar_0_)}+                           sd1 = ScanState.Build_ScanStateDesc ni+                            (LinearScan.Utils.set_nth ni ints xid0 ( i0))+                            _fixedIntervals_ unh _active_ _inactive_+                            _handled_}                           in-                          let {-                           _evar_0_0 = \_ ->+                          (Prelude.flip (Prelude.$)) __ (\_ ->                             (Prelude.flip (Prelude.$)) __ (\_ ->-                              let {-                               _top_assumption_1 = Interval.splitInterval-                                                     ( i1) _top_assumption_0}-                              in-                              let {-                               _evar_0_0 = \i1_0 i1_1 ->-                                (Prelude.flip (Prelude.$)) __-                                  (let {-                                    _evar_0_0 = (Prelude.flip (Prelude.$)) __-                                                  (\_ _ -> Prelude.Right-                                                  (Prelude.Just-                                                  (ScanState.packScanState-                                                    maxReg ScanState.InUse-                                                    (ScanState.Build_ScanStateDesc-                                                    ((Prelude.succ)-                                                    ((Prelude.succ)-                                                    _nextInterval_))-                                                    (LinearScan.Utils.snoc-                                                      ((Prelude.succ)-                                                      _nextInterval_)-                                                      (LinearScan.Utils.snoc-                                                        _nextInterval_-                                                        (LinearScan.Utils.set_nth-                                                          _nextInterval_ ints-                                                          xid0 ( i0))-                                                        ( i1_1)) ( i1_0))-                                                    _fixedIntervals_-                                                    (Prelude.map Prelude.id-                                                      (Lib.insert-                                                        (Lib.lebf-                                                          Prelude.snd) ((,)-                                                        ( _nextInterval_)-                                                        (Interval.ibeg-                                                          ( i1_1))) ((:)-                                                        (Prelude.id ((,) uid0-                                                          beg))-                                                        (Prelude.map-                                                          Prelude.id us0))))-                                                    (Prelude.map Prelude.id-                                                      (Prelude.map Prelude.id-                                                        _active_))-                                                    (Prelude.map Prelude.id-                                                      (Prelude.map Prelude.id-                                                        _inactive_)) ((:)-                                                    ((,)-                                                    ( ((Prelude.succ)-                                                      _nextInterval_))-                                                    Prelude.Nothing)-                                                    (Prelude.map Prelude.id-                                                      (Prelude.map Prelude.id-                                                        _handled_)))))))}-                                   in-                                    _evar_0_0)}-                              in-                              case _top_assumption_1 of {-                               (,) x x0 -> _evar_0_0 x x0})}-                          in-                          case Eqtype.eq_op Ssrnat.nat_eqType-                                 (unsafeCoerce (Interval.ibeg ( i1)))-                                 (unsafeCoerce _top_assumption_0) of {-                           Prelude.True -> _evar_0_ __;-                           Prelude.False -> _evar_0_0 __}}-                        in-                        let {-                         _evar_0_0 = let {-                                      _evar_0_0 = \_ -> Prelude.Right-                                       (Prelude.Just-                                       (ScanState.packScanState maxReg-                                         ScanState.InUse-                                         (ScanState.Build_ScanStateDesc-                                         ((Prelude.succ) _nextInterval_)-                                         (LinearScan.Utils.snoc-                                           _nextInterval_-                                           (LinearScan.Utils.set_nth-                                             _nextInterval_ ints xid0 -                                             ( i0)) ( i1)) _fixedIntervals_-                                         ((:) (Prelude.id ((,) uid0 beg))-                                         (Prelude.map Prelude.id us0))-                                         (Prelude.map Prelude.id _active_)-                                         (Prelude.map Prelude.id _inactive_)-                                         ((:) ((,) ( _nextInterval_)-                                         Prelude.Nothing)-                                         (Prelude.map Prelude.id _handled_)))))}-                                     in-                                      _evar_0_0 __}+                              (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-                        case Interval.firstUseReqReg ( i1) of {-                         Prelude.Just x -> _evar_0_ x;-                         Prelude.Nothing -> _evar_0_0}}-                      in-                       _evar_0_ __}+                         _evar_0_ __}+            in+             _evar_0_ __}           in-           _evar_0_ __}+          case _top_assumption_ of {+           (,) x x0 -> _evar_0_ x x0}}         in-        case _top_assumption_ of {-         (,) x x0 -> _evar_0_ x x0}}+        case int of {+         Interval.Build_IntervalDesc x x0 x1 x2 -> _evar_0_ x x0 x1 x2}}       in-      case int of {-       Interval.Build_IntervalDesc x x0 x1 x2 -> _evar_0_ x x0 x1 x2}}-    in-    let {-     _evar_0_0 = \_ -> Prelude.Left (Morph.ENoValidSplitPosition ( xid0)-      splitPos)}-    in-    case (Prelude.&&)-           ((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int))) splitPos)-           ((Prelude.<=) splitPos (Interval.iend ( int))) of {-     Prelude.True -> _evar_0_ __;-     Prelude.False -> _evar_0_0 __}}+      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}+    _evar_0_ x x0 x1 x2 x3 x4 x5 uid us xid hin}  splitAssignedIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->-                               PhysReg -> SplitPosition -> Prelude.Bool ->-                               Morph.SState () () ()+                               PhysReg -> Morph.SplitPosition -> Prelude.Bool+                               -> Morph.SState () () () splitAssignedIntervalForReg maxReg pre reg pos trueForActives ssi =   let {    _evar_0_ = \desc ->@@ -444,18 +768,29 @@                 let {                  _evar_0_1 = \_ ->                   let {-                   _top_assumption_0 = \x x0 x1 x2 x3 ->+                   _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}-                  in-                  let {-                   _top_assumption_1 = _top_assumption_0 uid0 beg us0 aid pos}+                      inactive0 _handled_) x x0 x1 x2 x3 x4}                   in-                  let {_evar_0_1 = \err -> Prelude.Left err} in-                  let {-                   _evar_0_2 = \_top_assumption_2 ->+                  (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 {@@ -512,21 +847,14 @@                         Prelude.True -> _evar_0_2 __;                         Prelude.False -> _evar_0_3 __}))}                     in-                    let {-                     _evar_0_3 = Prelude.Left (Morph.ECannotSplitSingleton3-                      ( aid))}-                    in                     case _top_assumption_2 of {-                     Prelude.Just x -> _evar_0_2 x;-                     Prelude.Nothing -> _evar_0_3}}-                  in-                  case _top_assumption_1 of {-                   Prelude.Left x -> _evar_0_1 x;-                   Prelude.Right x -> _evar_0_2 x}}+                     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.ECannotSplitSingleton2-                  ( aid))}+                 _evar_0_2 = \_ -> Prelude.Left (Morph.ECannotSplitSingleton+                  pos ( aid))}                 in                 case (Prelude.<=) beg                        (@@ -568,14 +896,15 @@                              PhysReg -> Lib.Coq_oddnum -> Morph.SState                               () () () splitActiveIntervalForReg maxReg pre reg pos =-  splitAssignedIntervalForReg maxReg pre reg (BeforePos pos) Prelude.True+  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 (EndOfLifetimeHole pos)+    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

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Ssrbool where@@ -15,16 +15,32 @@   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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" @@ -85,9 +101,9 @@    Mem (Coq_pred t)  data Coq_predType t =-   PredType (() -> Coq_pred t) (() -> Coq_mem_pred t)+   PredType (Any -> Coq_pred t) (Any -> Coq_mem_pred t) -type Coq_pred_sort t = ()+type Coq_pred_sort t = Any  mkPredType :: (a2 -> a1 -> Prelude.Bool) -> Coq_predType a1 mkPredType toP =

@@ -1,3 +1,5 @@++ module LinearScan.Ssreflect where  

@@ -1,3 +1,5 @@++ module LinearScan.Ssrfun where  @@ -27,10 +29,6 @@                  Prelude.Maybe a2 _Option__bind f =   _Option__apply f Prelude.Nothing--_Option__map :: (a1 -> a2) -> (Prelude.Maybe a1) -> Prelude.Maybe a2-_Option__map f =-  _Option__bind (\x -> Prelude.Just (f x))  pcomp :: (a2 -> Prelude.Maybe a1) -> (a3 -> Prelude.Maybe a2) -> a3 ->          Prelude.Maybe a1

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Ssrnat where@@ -13,25 +13,29 @@ import qualified Data.Functor.Identity import qualified LinearScan.Utils -import qualified LinearScan.Specif as Specif import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Ssrbool as Ssrbool   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+import qualified GHC.Prim as GHC.Prim #else -- HUGS import qualified LinearScan.IOExts as IOExts-unsafeCoerce = IOExts.unsafeCoerce #endif -__ :: any-__ = Prelude.error "Logical or arity value used" +#ifdef __GLASGOW_HASKELL__+--unsafeCoerce :: a -> b+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+--unsafeCoerce :: a -> b+unsafeCoerce = IOExts.unsafeCoerce+#endif+ eqnP :: Eqtype.Equality__Coq_axiom Prelude.Int eqnP n m =   Ssrbool.iffP ((Prelude.==) n m) (Ssrbool.idP ((Prelude.==) n m))@@ -43,27 +47,6 @@ nat_eqType :: Eqtype.Equality__Coq_type nat_eqType =   unsafeCoerce nat_eqMixin--find_ex_minn :: (Ssrbool.Coq_pred Prelude.Int) -> Specif.Coq_sig2 Prelude.Int-find_ex_minn p =-  (Prelude.flip (Prelude.$)) __-    ((Prelude.flip (Prelude.$)) __ (\_ _ ->-      let {-       find_ex_minn0 m =-         let {_evar_0_ = \_ -> m} in-         let {_evar_0_0 = \_ -> find_ex_minn0 ((Prelude.succ) m)} in-         case p m of {-          Prelude.True -> _evar_0_ __;-          Prelude.False -> _evar_0_0 __}}-      in find_ex_minn0 0))--type Coq_ex_minn_spec =-  Prelude.Int-  -- singleton inductive, whose constructor was ExMinnSpec-  -ex_minnP :: (Ssrbool.Coq_pred Prelude.Int) -> Coq_ex_minn_spec-ex_minnP p =-  let {x = find_ex_minn p} in Eqtype.s2val x  nat_of_bool :: Prelude.Bool -> Prelude.Int nat_of_bool b =

@@ -1,96 +0,0 @@-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---type State s a = s -> (,) a s--get :: State a1 a1-get i =-  (,) i i--gets :: (a1 -> a2) -> State a1 a2-gets f s =-  (,) (f s) s--put :: a1 -> State a1 ()-put x x0 =-  (,) () x--modify :: (a1 -> a1) -> State a1 ()-modify f i =-  (,) () (f i)--join :: (State a1 (State a1 a2)) -> State a1 a2-join x st =-  case x st of {-   (,) y st' -> y st'}--fmap :: (a2 -> a3) -> (State a1 a2) -> State a1 a3-fmap f x st =-  case x st of {-   (,) a st' -> (,) (f a) st'}--bind :: (a2 -> State a1 a3) -> (State a1 a2) -> State a1 a3-bind f x =-  join (fmap f x)--pure :: a2 -> State a1 a2-pure x st =-  (,) x st--ap :: (State a1 (a2 -> a3)) -> (State a1 a2) -> State a1 a3-ap f x st =-  case f st of {-   (,) f' st' ->-    case x st' of {-     (,) x' st'' -> (,) (f' x') st''}}--liftA2 :: (a2 -> a3 -> a4) -> (State a1 a2) -> (State a1 a3) -> State a1 a4-liftA2 f x y =-  ap (fmap f x) y--mapM :: (a2 -> State a1 a3) -> ([] a2) -> State a1 ([] a3)-mapM f l =-  case l of {-   [] -> pure [];-   (:) x xs -> liftA2 (\x0 x1 -> (:) x0 x1) (f x) (mapM f xs)}--mapM_ :: (a2 -> State a1 a3) -> ([] a2) -> State a1 ()-mapM_ f l =-  case l of {-   [] -> pure ();-   (:) x xs -> bind (\x0 -> mapM_ f xs) (f x)}--forM_ :: ([] a2) -> (a2 -> State a1 a3) -> State a1 ()-forM_ l f =-  mapM_ f l--foldrM :: (a3 -> a2 -> State a1 a2) -> a2 -> ([] a3) -> State a1 a2-foldrM f s l =-  case l of {-   [] -> pure s;-   (:) y ys -> bind (f y) (foldrM f s ys)}--forFoldrM :: a2 -> ([] a3) -> (a3 -> a2 -> State a1 a2) -> State a1 a2-forFoldrM s l f =-  foldrM f s l--concat :: ([] ([] a1)) -> [] a1-concat l =-  case l of {-   [] -> [];-   (:) x xs -> (Prelude.++) x (concat xs)}--concatMapM :: (a2 -> State a1 ([] a3)) -> ([] a2) -> State a1 ([] a3)-concatMapM f l =-  fmap concat (mapM f l)-

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.UsePos where@@ -19,13 +19,21 @@   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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 

@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -}  module LinearScan.Vector0 where@@ -15,13 +15,29 @@   ---unsafeCoerce :: a -> b #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base-unsafeCoerce = GHC.Base.unsafeCoerce#+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 

@@ -0,0 +1,85 @@+{-# OPTIONS_GHC -cpp -XMagicHash #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Yoneda 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.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 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 h =+  Build_Isomorphism (\x -> unsafeCoerce x __ (\x0 -> x0)) (\x _ k ->+    Monad.fmap h k x)++coq_Yoneda_Functor :: Monad.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 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))++coq_Yoneda_join :: (Monad.Monad a1) -> (Yoneda a1 (Yoneda a1 a2)) -> (a2 ->+                   a3) -> a1+coq_Yoneda_join h k h0 =+  Monad.join h (unsafeCoerce k __ (\y -> y __ h0))++coq_Yoneda_Monad :: (Monad.Monad a1) -> Monad.Monad (Yoneda a1 Any)+coq_Yoneda_Monad h =+  Monad.Build_Monad (coq_Yoneda_Applicative (Monad.is_applicative h))+    (unsafeCoerce (\_ x _ -> coq_Yoneda_join h x))+

@@ -1,5 +1,5 @@ name:          linearscan-version:       0.4.0.0+version:       0.5.0.0 synopsis:      Linear scan register allocator, formally verified in Coq homepage:      http://github.com/jwiegley/linearscan license:       BSD3@@ -61,12 +61,14 @@     LinearScan.IState     LinearScan.IntMap     LinearScan.Interval+    LinearScan.Lens     LinearScan.Lib     LinearScan.List0     LinearScan.LiveSets     LinearScan.Logic     LinearScan.Loops     LinearScan.Main+    LinearScan.Monad     LinearScan.Morph     LinearScan.NonEmpty0     LinearScan.Range@@ -79,13 +81,14 @@     LinearScan.Ssreflect     LinearScan.Ssrfun     LinearScan.Ssrnat-    LinearScan.State     LinearScan.UsePos     LinearScan.Utils     LinearScan.Vector0+    LinearScan.Yoneda   cpp-options:      -DMAX_REG=4 -DREG_SIZE=8   ghc-options:      -fno-warn-deprecated-flags-  build-depends:    base >=4.7 && <4.8+  build-depends:    base >=4.7 && <5.0                   , containers                   , transformers                   , mtl+                  , ghc-prim