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