linearscan 0.2.0.0 → 0.3.0.0
raw patch · 37 files changed
+4453/−2897 lines, 37 filesdep +mtldep −HUnitPVP ok
version bump matches the API change (PVP)
Dependencies added: mtl
Dependencies removed: HUnit
API changes (from Hackage documentation)
- LinearScan: instance Show VarKind
+ LinearScan: moveOp :: OpInfo accType op1 op2 -> PhysReg -> PhysReg -> State accType [op2]
+ LinearScan: swapOp :: OpInfo accType op1 op2 -> PhysReg -> PhysReg -> State accType [op2]
+ LinearScan: type VarId = Int
- LinearScan: BlockInfo :: (blk a -> Int) -> (blk a -> [Int]) -> (blk a -> [o a]) -> (blk a -> [o b] -> blk b) -> BlockInfo blk o a b
+ LinearScan: BlockInfo :: (blk1 -> Int) -> (blk1 -> [Int]) -> (blk1 -> ([op1], [op1], [op1])) -> (blk1 -> [op2] -> [op2] -> [op2] -> blk2) -> BlockInfo blk1 blk2 op1 op2
- 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: OpInfo :: (op1 -> OpKind) -> (op1 -> [VarInfo]) -> (PhysReg -> PhysReg -> State accType [op2]) -> (PhysReg -> PhysReg -> State accType [op2]) -> (PhysReg -> Maybe Int -> State accType [op2]) -> (Maybe Int -> PhysReg -> State accType [op2]) -> (op1 -> [(Int, PhysReg)] -> [op2]) -> OpInfo accType op1 op2
- LinearScan: VarInfo :: (v -> Int) -> (v -> VarKind) -> (v -> Bool) -> VarInfo v
+ LinearScan: VarInfo :: Either PhysReg VarId -> VarKind -> Bool -> VarInfo
- LinearScan: allocate :: BlockInfo blk o a b -> OpInfo accType o v a b -> VarInfo v -> [blk a] -> accType -> Either String ([blk b], accType)
+ LinearScan: allocate :: Int -> BlockInfo blk1 blk2 op1 op2 -> OpInfo accType op1 op2 -> [blk1] -> State accType (Either String [blk2])
- LinearScan: applyAllocs :: OpInfo accType o v a b -> o a -> [(Int, PhysReg)] -> o b
+ LinearScan: applyAllocs :: OpInfo accType op1 op2 -> op1 -> [(Int, PhysReg)] -> [op2]
- LinearScan: blockId :: BlockInfo blk o a b -> blk a -> Int
+ LinearScan: blockId :: BlockInfo blk1 blk2 op1 op2 -> blk1 -> Int
- LinearScan: blockOps :: BlockInfo blk o a b -> blk a -> [o a]
+ LinearScan: blockOps :: BlockInfo blk1 blk2 op1 op2 -> blk1 -> ([op1], [op1], [op1])
- LinearScan: blockSuccessors :: BlockInfo blk o a b -> blk a -> [Int]
+ LinearScan: blockSuccessors :: BlockInfo blk1 blk2 op1 op2 -> blk1 -> [Int]
- LinearScan: data BlockInfo blk o a b
+ LinearScan: data BlockInfo blk1 blk2 op1 op2
- LinearScan: data OpInfo accType o v a b
+ LinearScan: data OpInfo accType op1 op2
- LinearScan: data VarInfo v
+ LinearScan: data VarInfo
- LinearScan: opKind :: OpInfo accType o v a b -> o a -> OpKind
+ LinearScan: opKind :: OpInfo accType op1 op2 -> op1 -> OpKind
- LinearScan: opRefs :: OpInfo accType o v a b -> o a -> ([v], [PhysReg])
+ LinearScan: opRefs :: OpInfo accType op1 op2 -> op1 -> [VarInfo]
- LinearScan: regRequired :: VarInfo v -> v -> Bool
+ LinearScan: regRequired :: VarInfo -> Bool
- LinearScan: restoreOp :: OpInfo accType o v a b -> Int -> PhysReg -> accType -> (o b, accType)
+ LinearScan: restoreOp :: OpInfo accType op1 op2 -> Maybe Int -> PhysReg -> State accType [op2]
- LinearScan: saveOp :: OpInfo accType o v a b -> Int -> PhysReg -> accType -> (o b, accType)
+ LinearScan: saveOp :: OpInfo accType op1 op2 -> PhysReg -> Maybe Int -> State accType [op2]
- LinearScan: setBlockOps :: BlockInfo blk o a b -> blk a -> [o b] -> blk b
+ LinearScan: setBlockOps :: BlockInfo blk1 blk2 op1 op2 -> blk1 -> [op2] -> [op2] -> [op2] -> blk2
- LinearScan: varId :: VarInfo v -> v -> Int
+ LinearScan: varId :: VarInfo -> Either PhysReg VarId
- LinearScan: varKind :: VarInfo v -> v -> VarKind
+ LinearScan: varKind :: VarInfo -> VarKind
Files
- LinearScan.hs +65/−35
- LinearScan/Allocate.hs +420/−0
- LinearScan/Assign.hs +349/−0
- LinearScan/Blocks.hs +244/−0
- LinearScan/Build.hs +419/−0
- LinearScan/Choice.hs +323/−0
- LinearScan/Cursor.hs +43/−0
- LinearScan/Datatypes.hs +6/−0
- LinearScan/Eqtype.hs +93/−0
- LinearScan/Fintype.hs +193/−0
- LinearScan/Graph.hs +198/−0
- LinearScan/IState.hs +2/−8
- LinearScan/IntMap.hs +48/−0
- LinearScan/Interval.hs +115/−67
- LinearScan/Lib.hs +38/−14
- LinearScan/List0.hs +13/−0
- LinearScan/LiveSets.hs +134/−0
- LinearScan/Logic.hs +2/−0
- LinearScan/Main.hs +43/−2397
- LinearScan/Morph.hs +227/−0
- LinearScan/NonEmpty0.hs +8/−0
- LinearScan/Order.hs +17/−0
- LinearScan/Range.hs +207/−104
- LinearScan/Resolve.hs +136/−0
- LinearScan/ScanState.hs +158/−0
- LinearScan/Seq.hs +47/−35
- LinearScan/Specif.hs +2/−0
- LinearScan/Split.hs +426/−0
- LinearScan/Ssrbool.hs +16/−0
- LinearScan/Ssreflect.hs +13/−0
- LinearScan/Ssrfun.hs +17/−0
- LinearScan/Ssrnat.hs +35/−8
- LinearScan/State.hs +2/−0
- LinearScan/UsePos.hs +26/−0
- LinearScan/Vector0.hs +2/−0
- linearscan.cabal +25/−11
- test/Main.hs +341/−218
LinearScan.hs view
@@ -14,14 +14,19 @@ , OpInfo(..) , OpKind(..) -- * Variables+ , VarId , VarInfo(..) , VarKind(..) , PhysReg ) where +import Control.Monad.Trans.State+import qualified LinearScan.Blocks as LS import qualified LinearScan.Main as LS-import LinearScan.Main- ( VarKind(..)+import qualified LinearScan.Morph as LS+import LinearScan.Blocks+ ( VarId+ , VarKind(..) , OpKind(..) , PhysReg )@@ -32,16 +37,16 @@ -- 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 v = VarInfo- { varId :: v -> Int- , varKind :: v -> VarKind- , regRequired :: v -> Bool+data VarInfo = VarInfo+ { varId :: Either PhysReg VarId+ , varKind :: VarKind+ , regRequired :: Bool } deriving instance Eq VarKind-deriving instance Show VarKind+-- deriving instance Show VarKind -fromVarInfo :: VarInfo v -> LS.VarInfo v+fromVarInfo :: VarInfo -> LS.VarInfo fromVarInfo (VarInfo a b c) = LS.Build_VarInfo a b c -- | Every operation may reference multiple variables and/or specific physical@@ -55,31 +60,42 @@ -- and restore all registers around a call, but indication of loops is -- optional, as it's merely avoids reloading of spilled variables inside -- loop bodies.-data OpInfo accType 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+data OpInfo accType op1 op2 = OpInfo+ { opKind :: op1 -> OpKind+ , opRefs :: op1 -> [VarInfo]+ , moveOp :: PhysReg -> PhysReg -> State accType [op2]+ , swapOp :: PhysReg -> PhysReg -> State accType [op2]+ , saveOp :: PhysReg -> Maybe Int -> State accType [op2]+ , restoreOp :: Maybe Int -> PhysReg -> State accType [op2]+ , applyAllocs :: op1 -> [(Int, PhysReg)] -> [op2] } deriving instance Eq OpKind deriving instance Show OpKind -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+fromOpInfo :: OpInfo accType op1 op2 -> LS.OpInfo accType op1 op2+fromOpInfo (OpInfo a b c d e f g) =+ LS.Build_OpInfo a+ (map fromVarInfo . b)+ ((runState .) . c)+ ((runState .) . d)+ ((runState .) . e)+ ((runState .) . f) g -- | From the point of view of this library, a basic block is nothing more -- than an ordered sequence of operations.-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+data BlockInfo blk1 blk2 op1 op2 = BlockInfo+ { blockId :: blk1 -> Int+ , blockSuccessors :: blk1 -> [Int]+ , blockOps :: blk1 -> ([op1], [op1], [op1])+ , setBlockOps :: blk1 -> [op2] -> [op2] -> [op2] -> blk2 } -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+fromBlockInfo :: BlockInfo blk1 blk2 op1 op2+ -> LS.BlockInfo blk1 blk2 op1 op2+fromBlockInfo (BlockInfo a b c d) =+ LS.Build_BlockInfo a b+ (\blk -> let (x, y, z) = c blk in ((x, y), z)) d -- | Transform a list of basic blocks containing variable references, into an -- equivalent list where each reference is associated with a register@@ -92,17 +108,31 @@ -- 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 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 ++ ")"- LS.ECannotSplitAssignedSingleton n ->- "Current interval is an assigned singleton (" ++ show n ++ ")"+allocate :: Int -- ^ Maximum number of registers to use+ -> BlockInfo blk1 blk2 op1 op2+ -> OpInfo accType op1 op2+ -> [blk1]+ -> State accType (Either String [blk2])+allocate 0 _ _ _ = return $ Left "Cannot allocate with no registers"+allocate _ _ _ [] = return $ Left "No basic blocks were provided"+allocate maxReg (fromBlockInfo -> binfo) (fromOpInfo -> oinfo) blocks = do+ eres <- gets (LS.linearScan maxReg binfo oinfo blocks)+ case eres of+ Left x -> return $ Left $ case x of+ LS.ECannotSplitSingleton1 n ->+ "Current interval is a singleton (err#1) (" ++ show n ++ ")"+ LS.ECannotSplitSingleton2 n ->+ "Current interval is a singleton (err#2) (" ++ show n ++ ")"+ LS.ECannotSplitSingleton3 n ->+ "Current interval is a singleton (err#3) (" ++ show n ++ ")"+ LS.ECannotSplitSingleton4 n ->+ "Current interval is a singleton (err#4) (" ++ show n ++ ")"+ LS.ECannotSplitSingleton5 n ->+ "Current interval is a singleton (err#5) (" ++ show n ++ ")"+ LS.ECannotSplitSingleton6 n ->+ "Current interval is a singleton (err#6) (" ++ show n ++ ")"+ LS.ECannotSplitSingleton7 n ->+ "Current interval is a singleton (err#7) (" ++ show n ++ ")" LS.ENoIntervalsToSplit -> "There are no intervals to split" LS.ERegisterAlreadyAssigned n ->@@ -112,4 +142,4 @@ LS.EFuelExhausted -> "Fuel was exhausted" LS.EUnexpectedNoMoreUnhandled -> "The unexpected happened: no more unhandled intervals"- Right z -> Right z+ Right (z, acc) -> put acc >> return (Right z)
+ LinearScan/Allocate.hs view
@@ -0,0 +1,420 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Allocate where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Cursor as Cursor+import qualified LinearScan.IState as IState+import qualified LinearScan.Interval as Interval+import qualified LinearScan.Lib as Lib+import qualified LinearScan.Morph as Morph+import qualified LinearScan.ScanState as ScanState+import qualified LinearScan.Specif as Specif+import qualified LinearScan.Split as Split+import qualified LinearScan.UsePos as UsePos+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Fintype as Fintype+import qualified LinearScan.Seq as Seq+import qualified LinearScan.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"++type PhysReg = Prelude.Int++intersectsWithFixedInterval :: Prelude.Int -> ScanState.ScanStateDesc ->+ PhysReg -> Morph.SState () ()+ (Prelude.Maybe Lib.Coq_oddnum)+intersectsWithFixedInterval maxReg pre reg =+ Cursor.withCursor maxReg pre (\sd _ ->+ let {int = Cursor.curIntDetails maxReg sd} in+ Morph.return_+ (LinearScan.Utils.vfoldl' maxReg (\mx v ->+ Lib.option_choose mx+ (case v of {+ Prelude.Just i -> Interval.intervalIntersectionPoint ( int) ( i);+ Prelude.Nothing -> Prelude.Nothing})) Prelude.Nothing+ (ScanState.fixedIntervals maxReg sd)))++updateRegisterPos :: Prelude.Int -> ([] (Prelude.Maybe Lib.Coq_oddnum)) ->+ Prelude.Int -> (Prelude.Maybe Lib.Coq_oddnum) -> []+ (Prelude.Maybe Lib.Coq_oddnum)+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 ->+ case (Prelude.<=) ((Prelude.succ) ( n0)) ( x) of {+ Prelude.True -> n0;+ Prelude.False -> x};+ Prelude.Nothing -> x}));+ Prelude.Nothing -> v}++tryAllocateFreeReg :: Prelude.Int -> ScanState.ScanStateDesc -> Morph.SState+ () () (Prelude.Maybe (Morph.SState () () PhysReg))+tryAllocateFreeReg maxReg pre =+ Cursor.withCursor maxReg 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 Lib.odd1))+ (Data.List.replicate maxReg Prelude.Nothing)+ (ScanState.active maxReg sd)}+ in+ let {+ intersectingIntervals = Prelude.filter (\x ->+ Interval.intervalsIntersect+ ( (Cursor.curIntDetails maxReg sd))+ (+ (LinearScan.Utils.nth+ (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd)+ (Prelude.fst x))))+ (ScanState.inactive maxReg sd)}+ in+ let {+ freeUntilPos = Data.List.foldl'+ (go (\i ->+ Interval.intervalIntersectionPoint+ (+ (LinearScan.Utils.nth+ (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd) i))+ ( (Cursor.curIntDetails maxReg sd)))) freeUntilPos'+ intersectingIntervals}+ in+ case ScanState.registerWithHighestPos maxReg freeUntilPos of {+ (,) reg mres ->+ let {+ success = Morph.stbind (\x -> Morph.return_ reg)+ (Morph.moveUnhandledToActive maxReg pre reg)}+ in+ let {+ maction = case mres of {+ Prelude.Just n ->+ case Eqtype.eq_op Ssrnat.nat_eqType ( (unsafeCoerce n))+ (unsafeCoerce ((Prelude.succ) 0)) of {+ Prelude.True -> Prelude.Nothing;+ Prelude.False -> Prelude.Just+ (case (Prelude.<=) ((Prelude.succ)+ (Interval.intervalEnd+ ( (Cursor.curIntDetails maxReg sd)))) + ( n) of {+ Prelude.True -> success;+ Prelude.False ->+ Morph.stbind (\x ->+ Morph.stbind (\x0 -> Morph.return_ reg)+ (Morph.moveUnhandledToActive maxReg pre reg))+ (Split.splitCurrentInterval maxReg pre+ (Split.BeforePos n))})};+ Prelude.Nothing -> Prelude.Just success}}+ in+ Morph.return_ maction})++allocateBlockedReg :: Prelude.Int -> ScanState.ScanStateDesc -> Morph.SState+ () () (Prelude.Maybe PhysReg)+allocateBlockedReg maxReg pre =+ Cursor.withCursor maxReg pre (\sd _ ->+ let {start = Interval.intervalStart ( (Cursor.curIntDetails maxReg sd))}+ in+ let {pos = Cursor.curPosition maxReg sd} in+ let {+ go = \v p ->+ case p of {+ (,) i r ->+ let {+ atPos = \u ->+ Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos)+ (unsafeCoerce (UsePos.uloc u))}+ in+ let {+ pos' = case Interval.findIntervalUsePos+ (Interval.getIntervalDesc+ (+ (LinearScan.Utils.nth+ (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd) i))) atPos of {+ Prelude.Just s -> Prelude.Just Lib.odd1;+ Prelude.Nothing ->+ Interval.nextUseAfter+ (Interval.getIntervalDesc+ (+ (LinearScan.Utils.nth+ (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd) i))) start}}+ in+ updateRegisterPos maxReg v r pos'}}+ in+ let {+ nextUsePos' = Data.List.foldl' go+ (Data.List.replicate maxReg Prelude.Nothing)+ (ScanState.active maxReg sd)}+ in+ let {+ intersectingIntervals = Prelude.filter (\x ->+ Interval.intervalsIntersect+ ( (Cursor.curIntDetails maxReg sd))+ (+ (LinearScan.Utils.nth+ (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd)+ (Prelude.fst x))))+ (ScanState.inactive maxReg sd)}+ in+ let {nextUsePos = Data.List.foldl' go nextUsePos' intersectingIntervals}+ in+ case ScanState.registerWithHighestPos maxReg nextUsePos of {+ (,) reg mres ->+ case case mres of {+ Prelude.Just n -> (Prelude.<=) ((Prelude.succ) ( n)) start;+ Prelude.Nothing -> Prelude.False} of {+ Prelude.True ->+ Morph.stbind (\x ->+ Morph.stbind (\mloc ->+ Morph.stbind (\x0 ->+ Morph.stbind (\x1 -> Morph.return_ Prelude.Nothing)+ (Morph.weakenHasLen_ maxReg pre))+ (case mloc of {+ Prelude.Just n ->+ Split.splitCurrentInterval maxReg pre (Split.BeforePos n);+ Prelude.Nothing -> Morph.return_ ()}))+ (intersectsWithFixedInterval maxReg pre reg))+ (Split.splitCurrentInterval maxReg pre+ Split.BeforeFirstUsePosReqReg);+ Prelude.False ->+ Morph.stbind (\x ->+ Morph.stbind (\x0 ->+ Morph.stbind (\mloc ->+ Morph.stbind (\x1 ->+ Morph.stbind (\x2 -> Morph.return_ (Prelude.Just reg))+ (Morph.moveUnhandledToActive maxReg pre reg))+ (case mloc of {+ Prelude.Just n ->+ Split.splitCurrentInterval maxReg pre (Split.BeforePos n);+ Prelude.Nothing -> Morph.return_ ()}))+ (intersectsWithFixedInterval maxReg pre reg))+ (Split.splitActiveIntervalForReg maxReg pre reg pos))+ (Split.splitAnyInactiveIntervalForReg maxReg pre reg)}})++morphlen_transport :: Prelude.Int -> ScanState.ScanStateDesc ->+ ScanState.ScanStateDesc -> ScanState.IntervalId ->+ ScanState.IntervalId+morphlen_transport maxReg b b' = GHC.Base.id+ ++mt_fst :: Prelude.Int -> ScanState.ScanStateDesc -> ScanState.ScanStateDesc+ -> ((,) ScanState.IntervalId PhysReg) -> (,) ScanState.IntervalId+ PhysReg+mt_fst maxReg b b' x =+ case x of {+ (,) xid reg -> (,) (morphlen_transport maxReg b b' xid) reg}++type Coq_int_reg_seq = [] ((,) ScanState.IntervalId PhysReg)++type Coq_intermediate_result = Specif.Coq_sig2 ScanState.ScanStateDesc++goActive :: Prelude.Int -> Prelude.Int -> ScanState.ScanStateDesc ->+ ScanState.ScanStateDesc -> ((,) ScanState.IntervalId PhysReg) ->+ Coq_int_reg_seq -> Coq_intermediate_result+goActive maxReg pos sd z x xs =+ case (Prelude.<=) ((Prelude.succ)+ (Interval.intervalEnd+ (+ (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)+ (ScanState.intervals maxReg z) (Prelude.fst x))))) pos of {+ Prelude.True -> Morph.moveActiveToHandled maxReg z (unsafeCoerce x);+ Prelude.False ->+ case Prelude.not+ (Interval.intervalCoversPos+ (+ (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)+ (ScanState.intervals maxReg z) (Prelude.fst x))) pos) of {+ Prelude.True -> Morph.moveActiveToInactive maxReg z (unsafeCoerce x);+ Prelude.False -> z}}++checkActiveIntervals :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int+ -> Morph.SState () () ()+checkActiveIntervals maxReg pre pos =+ Morph.withScanStatePO maxReg pre (\sd _ ->+ let {+ res = Lib.dep_foldl_inv (\s ->+ Eqtype.prod_eqType+ (Fintype.ordinal_eqType (ScanState.nextInterval maxReg s))+ (Fintype.ordinal_eqType maxReg)) sd+ (unsafeCoerce (ScanState.active maxReg sd))+ (Data.List.length (ScanState.active maxReg sd))+ (unsafeCoerce (ScanState.active maxReg))+ (unsafeCoerce (\x x0 _ -> mt_fst maxReg x x0))+ (unsafeCoerce (\x _ x0 x1 _ -> goActive maxReg pos sd x x0 x1))}+ in+ IState.iput (Morph.Build_SSInfo res __))++moveInactiveToActive' :: Prelude.Int -> ScanState.ScanStateDesc -> ((,)+ ScanState.IntervalId PhysReg) -> Coq_int_reg_seq ->+ Prelude.Either Morph.SSError+ (Specif.Coq_sig2 ScanState.ScanStateDesc)+moveInactiveToActive' maxReg 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)+ (ScanState.active maxReg z)))))}+ in+ case filtered_var of {+ Prelude.True ->+ let {+ filtered_var0 = Morph.moveInactiveToActive maxReg z (unsafeCoerce x)}+ in+ Prelude.Right filtered_var0;+ Prelude.False -> Prelude.Left (Morph.ERegisterAssignmentsOverlap+ ( (Prelude.snd x)))}++goInactive :: Prelude.Int -> Prelude.Int -> ScanState.ScanStateDesc ->+ ScanState.ScanStateDesc -> ((,) ScanState.IntervalId PhysReg)+ -> Coq_int_reg_seq -> Prelude.Either Morph.SSError+ Coq_intermediate_result+goInactive maxReg pos sd z x xs =+ let {f = \sd' -> Prelude.Right sd'} in+ case (Prelude.<=) ((Prelude.succ)+ (Interval.intervalEnd+ (+ (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)+ (ScanState.intervals maxReg z) (Prelude.fst x))))) pos of {+ Prelude.True ->+ let {+ filtered_var = Morph.moveInactiveToHandled maxReg z (unsafeCoerce x)}+ in+ f filtered_var;+ Prelude.False ->+ case Interval.intervalCoversPos+ (+ (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)+ (ScanState.intervals maxReg z) (Prelude.fst x))) pos of {+ Prelude.True ->+ let {filtered_var = moveInactiveToActive' maxReg z x xs} in+ case filtered_var of {+ Prelude.Left err -> Prelude.Left err;+ Prelude.Right s -> f s};+ Prelude.False -> f z}}++checkInactiveIntervals :: Prelude.Int -> ScanState.ScanStateDesc ->+ Prelude.Int -> Morph.SState () () ()+checkInactiveIntervals maxReg pre pos =+ Morph.withScanStatePO maxReg pre (\sd _ ->+ let {+ eres = Lib.dep_foldl_invE (\s ->+ Eqtype.prod_eqType+ (Fintype.ordinal_eqType (ScanState.nextInterval maxReg s))+ (Fintype.ordinal_eqType maxReg)) sd+ (unsafeCoerce (ScanState.inactive maxReg sd))+ (Data.List.length (ScanState.inactive maxReg sd))+ (unsafeCoerce (ScanState.inactive maxReg))+ (unsafeCoerce (\x x0 _ -> mt_fst maxReg x x0))+ (unsafeCoerce (\x _ x0 x1 _ ->+ goInactive maxReg pos sd x x0 x1))}+ in+ case eres of {+ Prelude.Left err -> Morph.error_ err;+ Prelude.Right s -> IState.iput (Morph.Build_SSInfo s __)})++handleInterval :: Prelude.Int -> ScanState.ScanStateDesc -> Morph.SState + () () (Prelude.Maybe PhysReg)+handleInterval maxReg pre =+ Cursor.withCursor maxReg pre (\sd _ ->+ let {position = Cursor.curPosition maxReg sd} in+ Morph.stbind (\x ->+ Morph.stbind (\x0 ->+ Morph.stbind (\mres ->+ case mres of {+ Prelude.Just x1 -> IState.imap (\x2 -> Prelude.Just x2) x1;+ Prelude.Nothing -> allocateBlockedReg maxReg pre})+ (tryAllocateFreeReg maxReg pre))+ (Morph.liftLen maxReg pre (\sd0 ->+ checkInactiveIntervals maxReg sd0 position)))+ (Morph.liftLen maxReg pre (\sd0 ->+ checkActiveIntervals maxReg sd0 position)))++walkIntervals :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int ->+ Prelude.Either Morph.SSError ScanState.ScanStateSig+walkIntervals maxReg sd positions =+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ -> Prelude.Left+ Morph.EFuelExhausted)+ (\n ->+ let {+ go = let {+ go count0 ss =+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ -> Prelude.Right (Morph.Build_SSInfo+ (Morph.thisDesc maxReg sd ss)+ __))+ (\cnt ->+ case handleInterval maxReg sd ss of {+ Prelude.Left err -> Prelude.Left err;+ Prelude.Right p ->+ case p of {+ (,) o ss' ->+ case Morph.strengthenHasLen maxReg sd+ (Morph.thisDesc maxReg sd ss') of {+ Prelude.Just _ ->+ go cnt (Morph.Build_SSInfo+ (Morph.thisDesc maxReg sd ss') __);+ Prelude.Nothing ->+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ -> Prelude.Right+ ss')+ (\n0 -> Prelude.Left+ Morph.EUnexpectedNoMoreUnhandled)+ cnt}}})+ count0}+ in go}+ in+ case LinearScan.Utils.uncons (ScanState.unhandled maxReg 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))+ (ScanState.unhandled maxReg sd)) (Morph.Build_SSInfo sd+ __) of {+ Prelude.Left err -> Prelude.Left err;+ Prelude.Right ss ->+ walkIntervals maxReg (Morph.thisDesc maxReg sd ss) n}}};+ Prelude.Nothing -> Prelude.Right+ (ScanState.packScanState maxReg ScanState.InUse sd)})+ positions+
+ LinearScan/Assign.hs view
@@ -0,0 +1,349 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Assign where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Blocks as Blocks+import qualified LinearScan.Graph as Graph+import qualified LinearScan.Interval as Interval+import qualified LinearScan.Resolve as Resolve+import qualified LinearScan.ScanState as ScanState+import qualified LinearScan.State as State+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Fintype as Fintype+import qualified LinearScan.Ssrnat as Ssrnat++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++type PhysReg = Prelude.Int++data AssnStateInfo accType =+ Build_AssnStateInfo Blocks.OpId Blocks.OpId Blocks.OpId accType++assnOpId :: (AssnStateInfo a1) -> Blocks.OpId+assnOpId a =+ case a of {+ Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAcc0 ->+ assnOpId0}++assnBlockBeg :: (AssnStateInfo a1) -> Blocks.OpId+assnBlockBeg a =+ case a of {+ Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAcc0 ->+ assnBlockBeg0}++assnBlockEnd :: (AssnStateInfo a1) -> Blocks.OpId+assnBlockEnd a =+ case a of {+ Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAcc0 ->+ assnBlockEnd0}++assnAcc :: (AssnStateInfo a1) -> a1+assnAcc a =+ case a of {+ Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAcc0 ->+ assnAcc0}++type AssnState accType a = State.State (AssnStateInfo accType) a++moveOpM :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Blocks.PhysReg ->+ Blocks.PhysReg -> AssnState a3 ([] a2)+moveOpM maxReg oinfo sreg dreg =+ State.bind (\assn ->+ case Blocks.moveOp maxReg oinfo sreg dreg (assnAcc assn) of {+ (,) mop acc' ->+ State.bind (\x -> State.pure mop)+ (State.put (Build_AssnStateInfo (assnOpId assn) (assnBlockBeg assn)+ (assnBlockEnd assn) acc'))}) State.get++saveOpM :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Blocks.PhysReg ->+ (Prelude.Maybe Blocks.VarId) -> AssnState a3 ([] a2)+saveOpM maxReg oinfo vid reg =+ State.bind (\assn ->+ case Blocks.saveOp maxReg oinfo vid reg (assnAcc assn) of {+ (,) sop acc' ->+ State.bind (\x -> State.pure sop)+ (State.put (Build_AssnStateInfo (assnOpId assn) (assnBlockBeg assn)+ (assnBlockEnd assn) acc'))}) State.get++restoreOpM :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> (Prelude.Maybe+ Blocks.VarId) -> Blocks.PhysReg -> AssnState a3 ([] a2)+restoreOpM maxReg oinfo vid reg =+ State.bind (\assn ->+ case Blocks.restoreOp maxReg oinfo vid reg (assnAcc assn) of {+ (,) rop acc' ->+ State.bind (\x -> State.pure rop)+ (State.put (Build_AssnStateInfo (assnOpId assn) (assnBlockBeg assn)+ (assnBlockEnd assn) acc'))}) State.get++pairM :: (AssnState a1 a2) -> (AssnState a1 a3) -> AssnState a1 ((,) a2 a3)+pairM x y =+ State.bind (\x' -> State.bind (\y' -> State.pure ((,) x' y')) y) x++savesAndRestores :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Blocks.OpId ->+ Blocks.VarInfo -> Blocks.PhysReg -> Interval.IntervalDesc+ -> AssnState a3 ((,) ([] a2) ([] a2))+savesAndRestores maxReg oinfo opid v reg int =+ case Blocks.varId maxReg v of {+ Prelude.Left p -> State.pure ((,) [] []);+ Prelude.Right vid ->+ State.bind (\assn ->+ let {knd = Blocks.varKind maxReg v} in+ let {+ atBoundary = (Prelude.||)+ ((Prelude.&&)+ (Eqtype.eq_op Blocks.coq_VarKind_eqType+ (unsafeCoerce knd) (unsafeCoerce Blocks.Input))+ (Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce (assnBlockBeg assn))+ (unsafeCoerce opid)))+ ((Prelude.&&)+ (Eqtype.eq_op Blocks.coq_VarKind_eqType+ (unsafeCoerce knd) (unsafeCoerce Blocks.Output))+ (Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce ((Prelude.succ) ((Prelude.succ)+ opid))) (unsafeCoerce (assnBlockEnd assn))))}+ in+ case atBoundary of {+ Prelude.True -> State.pure ((,) [] []);+ Prelude.False ->+ let {+ isFirst = Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)+ (unsafeCoerce (Interval.firstUsePos int))+ (unsafeCoerce (Prelude.Just opid))}+ in+ let {+ isLast = Eqtype.eq_op+ (Eqtype.option_eqType+ (Eqtype.sig_eqType Ssrnat.nat_eqType+ (unsafeCoerce Ssrnat.odd)))+ (unsafeCoerce (Interval.nextUseAfter int opid))+ (unsafeCoerce Prelude.Nothing)}+ in+ let {save = saveOpM maxReg oinfo reg (Prelude.Just vid)} in+ let {restore = restoreOpM maxReg oinfo (Prelude.Just vid) reg} in+ case knd of {+ Blocks.Input ->+ case Interval.iknd int of {+ Interval.Whole -> State.pure ((,) [] []);+ Interval.LeftMost ->+ case isLast of {+ Prelude.True -> pairM (State.pure []) save;+ Prelude.False -> State.pure ((,) [] [])};+ Interval.Middle ->+ case isFirst of {+ Prelude.True ->+ case isLast of {+ Prelude.True -> pairM 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 ((,) [] [])}};+ Blocks.Temp -> State.pure ((,) [] []);+ Blocks.Output ->+ case Interval.iknd int of {+ Interval.LeftMost ->+ case isLast of {+ Prelude.True -> pairM (State.pure []) save;+ Prelude.False -> State.pure ((,) [] [])};+ Interval.Middle ->+ case isLast of {+ Prelude.True -> pairM (State.pure []) save;+ Prelude.False -> State.pure ((,) [] [])};+ _ -> State.pure ((,) [] [])}}}) State.get}++collectAllocs :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Prelude.Int ->+ ([] ((,) Interval.IntervalDesc PhysReg)) -> ((,)+ ((,) ([] ((,) Blocks.VarId PhysReg)) ([] a2)) ([] a2)) ->+ Blocks.VarInfo -> State.State (AssnStateInfo a3)+ ((,) ((,) ([] ((,) Blocks.VarId PhysReg)) ([] a2)) ([] a2))+collectAllocs maxReg oinfo opid ints acc v =+ case Blocks.varId maxReg v of {+ Prelude.Left p -> State.pure acc;+ Prelude.Right vid ->+ let {+ v_ints = Prelude.filter (\x ->+ ScanState.isWithin (Prelude.fst x) vid opid) ints}+ in+ State.forFoldM acc v_ints (\acc' x ->+ case x of {+ (,) int reg ->+ case acc' of {+ (,) p saves' ->+ case p of {+ (,) allocs' restores' ->+ State.bind (\res ->+ case res of {+ (,) rs ss ->+ State.pure ((,) ((,) ((:) ((,) vid reg) allocs')+ ((Prelude.++) rs restores')) ((Prelude.++) ss saves'))})+ (savesAndRestores maxReg oinfo opid v reg int)}}})}++doAllocations :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> ([]+ ((,) Interval.IntervalDesc PhysReg)) -> a1 -> AssnState + a3 ([] a2)+doAllocations maxReg oinfo ints op =+ State.bind (\assn ->+ let {opid = assnOpId assn} in+ let {vars = Blocks.opRefs maxReg oinfo op} in+ State.bind (\res ->+ case res of {+ (,) y saves ->+ case y of {+ (,) allocs restores ->+ let {op' = Blocks.applyAllocs maxReg oinfo op allocs} in+ State.bind (\x ->+ State.pure ((Prelude.++) restores ((Prelude.++) op' saves)))+ (State.modify (\assn' -> Build_AssnStateInfo ((Prelude.succ)+ ((Prelude.succ) opid)) (assnBlockBeg assn')+ (assnBlockEnd assn') (assnAcc assn')))}})+ (State.forFoldM ((,) ((,) [] []) []) vars+ (collectAllocs maxReg oinfo opid ints))) State.get++generateMoves :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> ([]+ ((,) (Prelude.Maybe (Prelude.Either PhysReg Prelude.Int))+ (Prelude.Maybe (Prelude.Either PhysReg Prelude.Int)))) ->+ AssnState a3 ([] a2)+generateMoves maxReg oinfo moves =+ State.forFoldM [] moves (\acc mv ->+ State.bind (\mops ->+ State.pure+ (case mops of {+ Prelude.Just ops -> (Prelude.++) ops acc;+ Prelude.Nothing -> acc}))+ (case mv of {+ (,) o o0 ->+ case o of {+ Prelude.Just s ->+ case s of {+ Prelude.Left sreg ->+ case o0 of {+ Prelude.Just s0 ->+ case s0 of {+ Prelude.Left dreg ->+ State.fmap (\x -> Prelude.Just x)+ (moveOpM maxReg oinfo sreg dreg);+ Prelude.Right vid ->+ State.fmap (\x -> Prelude.Just x)+ (saveOpM maxReg oinfo sreg (Prelude.Just vid))};+ Prelude.Nothing ->+ State.fmap (\x -> Prelude.Just x)+ (saveOpM maxReg oinfo sreg Prelude.Nothing)};+ Prelude.Right vid ->+ case o0 of {+ Prelude.Just s0 ->+ case s0 of {+ Prelude.Left dreg ->+ State.fmap (\x -> Prelude.Just x)+ (restoreOpM maxReg oinfo (Prelude.Just vid) dreg);+ Prelude.Right n -> State.pure Prelude.Nothing};+ Prelude.Nothing -> State.pure Prelude.Nothing}};+ Prelude.Nothing ->+ case o0 of {+ Prelude.Just s ->+ case s of {+ Prelude.Left dreg ->+ State.fmap (\x -> Prelude.Just x)+ (restoreOpM maxReg oinfo Prelude.Nothing dreg);+ Prelude.Right n -> State.pure Prelude.Nothing};+ Prelude.Nothing -> State.pure Prelude.Nothing}}}))++resolveMappings :: Prelude.Int -> (Blocks.OpInfo a3 a1 a2) -> Prelude.Int ->+ ([] a2) -> (Data.IntMap.IntMap+ ((,) Graph.Graph Graph.Graph)) -> AssnState a3 ([] a2)+resolveMappings maxReg oinfo bid opsm mappings =+ case Data.IntMap.lookup bid mappings of {+ Prelude.Just graphs ->+ case graphs of {+ (,) gbeg gend ->+ State.bind (\bmoves ->+ let {opsm' = (Prelude.++) bmoves opsm} in+ State.bind (\emoves ->+ let {opsm'' = (Prelude.++) opsm' emoves} in State.pure opsm'')+ (generateMoves maxReg oinfo+ (unsafeCoerce+ (Graph.topsort+ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)+ Ssrnat.nat_eqType) gend))))+ (generateMoves maxReg oinfo+ (unsafeCoerce+ (Graph.topsort+ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)+ Ssrnat.nat_eqType) gbeg)))};+ Prelude.Nothing -> State.pure opsm}++considerOps :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->+ (Blocks.OpInfo a5 a3 a4) -> (a3 -> AssnState a5 ([] a4)) ->+ (Data.IntMap.IntMap ((,) Graph.Graph Graph.Graph)) -> ([] + a1) -> State.State (AssnStateInfo a5) ([] a2)+considerOps maxReg binfo oinfo f mappings =+ State.mapM (\blk ->+ let {ops = Blocks.blockOps binfo blk} in+ case ops of {+ (,) p opse ->+ case p of {+ (,) opsb opsm ->+ State.bind (\x ->+ State.bind (\opsb' ->+ State.bind (\opsm' ->+ State.bind (\opse' ->+ let {bid = Blocks.blockId binfo blk} in+ State.bind (\opsm'' ->+ State.pure+ (Blocks.setBlockOps binfo blk opsb' opsm'' opse'))+ (resolveMappings maxReg oinfo bid opsm' mappings))+ (State.concatMapM f opse)) (State.concatMapM f opsm))+ (State.concatMapM f opsb))+ (State.modify (\assn -> Build_AssnStateInfo (assnOpId assn)+ ((Prelude.+) (assnOpId assn)+ (Ssrnat.double (Data.List.length opsb)))+ ((Prelude.+) (assnOpId assn)+ (Ssrnat.double+ ((Prelude.+) (Data.List.length opsb) (Data.List.length opsm))))+ (assnAcc assn)))}})++assignRegNum :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->+ (Blocks.OpInfo a5 a3 a4) -> ScanState.ScanStateDesc ->+ (Data.IntMap.IntMap Resolve.BlockMoves) -> ([] a1) -> a5 ->+ (,) ([] a2) a5+assignRegNum maxReg binfo oinfo sd mappings blocks acc =+ case considerOps maxReg binfo oinfo+ (doAllocations maxReg oinfo+ (Prelude.map (\x -> (,)+ (Interval.getIntervalDesc+ (+ (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd) (Prelude.fst x))))+ (Prelude.snd x))+ ((Prelude.++) (ScanState.handled maxReg sd)+ ((Prelude.++) (ScanState.active maxReg sd)+ (ScanState.inactive maxReg sd))))) mappings blocks+ (Build_AssnStateInfo ((Prelude.succ) 0) ((Prelude.succ) 0)+ ((Prelude.succ) 0) acc) of {+ (,) blocks' assn -> (,) blocks' (assnAcc assn)}+
+ LinearScan/Blocks.hs view
@@ -0,0 +1,244 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Blocks where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Ssrbool as Ssrbool++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++type PhysReg = Prelude.Int++data VarKind =+ Input+ | Temp+ | Output++eqVarKind :: VarKind -> VarKind -> Prelude.Bool+eqVarKind s1 s2 =+ case s1 of {+ Input ->+ case s2 of {+ Input -> Prelude.True;+ _ -> Prelude.False};+ Temp ->+ case s2 of {+ Temp -> Prelude.True;+ _ -> Prelude.False};+ Output ->+ case s2 of {+ Output -> Prelude.True;+ _ -> Prelude.False}}++eqVarKindP :: Eqtype.Equality__Coq_axiom VarKind+eqVarKindP b1 b2 =+ let {+ _evar_0_ = let {_evar_0_ = Ssrbool.ReflectT} in+ let {_evar_0_0 = Ssrbool.ReflectF} in+ let {_evar_0_1 = Ssrbool.ReflectF} in+ case b2 of {+ Input -> _evar_0_;+ Temp -> _evar_0_0;+ Output -> _evar_0_1}}+ in+ let {+ _evar_0_0 = let {_evar_0_0 = Ssrbool.ReflectF} in+ let {_evar_0_1 = Ssrbool.ReflectT} in+ let {_evar_0_2 = Ssrbool.ReflectF} in+ case b2 of {+ Input -> _evar_0_0;+ Temp -> _evar_0_1;+ Output -> _evar_0_2}}+ in+ let {+ _evar_0_1 = let {_evar_0_1 = Ssrbool.ReflectF} in+ let {_evar_0_2 = Ssrbool.ReflectF} in+ let {_evar_0_3 = Ssrbool.ReflectT} in+ case b2 of {+ Input -> _evar_0_1;+ Temp -> _evar_0_2;+ Output -> _evar_0_3}}+ in+ case b1 of {+ Input -> _evar_0_;+ Temp -> _evar_0_0;+ Output -> _evar_0_1}++coq_VarKind_eqMixin :: Eqtype.Equality__Coq_mixin_of VarKind+coq_VarKind_eqMixin =+ Eqtype.Equality__Mixin eqVarKind eqVarKindP++coq_VarKind_eqType :: Eqtype.Equality__Coq_type+coq_VarKind_eqType =+ unsafeCoerce coq_VarKind_eqMixin++type VarId = Prelude.Int++data VarInfo =+ Build_VarInfo (Prelude.Either PhysReg VarId) VarKind Prelude.Bool++varId :: Prelude.Int -> VarInfo -> Prelude.Either PhysReg VarId+varId maxReg v =+ case v of {+ Build_VarInfo varId0 varKind0 regRequired0 -> varId0}++varKind :: Prelude.Int -> VarInfo -> VarKind+varKind maxReg v =+ case v of {+ Build_VarInfo varId0 varKind0 regRequired0 -> varKind0}++regRequired :: Prelude.Int -> VarInfo -> Prelude.Bool+regRequired maxReg v =+ case v of {+ Build_VarInfo varId0 varKind0 regRequired0 -> regRequired0}++nat_of_varId :: Prelude.Int -> VarInfo -> Prelude.Int+nat_of_varId maxReg v =+ case varId maxReg v of {+ Prelude.Left n -> n;+ Prelude.Right v0 -> (Prelude.+) v0 maxReg}++data OpKind =+ IsNormal+ | IsCall+ | IsBranch+ | IsLoopBegin+ | IsLoopEnd++data OpInfo accType opType1 opType2 =+ Build_OpInfo (opType1 -> OpKind) (opType1 -> [] VarInfo) (PhysReg ->+ PhysReg ->+ accType -> (,)+ ([] opType2)+ accType) + (PhysReg -> PhysReg -> accType -> (,) ([] opType2) accType) (PhysReg ->+ (Prelude.Maybe+ VarId) ->+ accType -> (,)+ ([] opType2)+ accType) + ((Prelude.Maybe VarId) -> PhysReg -> accType -> (,) ([] opType2) accType) + (opType1 -> ([] ((,) VarId PhysReg)) -> [] opType2)++opKind :: Prelude.Int -> (OpInfo a1 a2 a3) -> a2 -> OpKind+opKind maxReg o =+ case o of {+ Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0+ applyAllocs0 -> opKind0}++opRefs :: Prelude.Int -> (OpInfo a1 a2 a3) -> a2 -> [] VarInfo+opRefs maxReg o =+ case o of {+ Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0+ applyAllocs0 -> opRefs0}++moveOp :: Prelude.Int -> (OpInfo a1 a2 a3) -> PhysReg -> PhysReg -> a1 -> (,)+ ([] a3) a1+moveOp maxReg o =+ case o of {+ Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0+ applyAllocs0 -> moveOp0}++saveOp :: Prelude.Int -> (OpInfo a1 a2 a3) -> PhysReg -> (Prelude.Maybe+ VarId) -> a1 -> (,) ([] a3) a1+saveOp maxReg o =+ case o of {+ Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0+ applyAllocs0 -> saveOp0}++restoreOp :: Prelude.Int -> (OpInfo a1 a2 a3) -> (Prelude.Maybe VarId) ->+ PhysReg -> a1 -> (,) ([] a3) a1+restoreOp maxReg o =+ case o of {+ Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0+ applyAllocs0 -> restoreOp0}++applyAllocs :: Prelude.Int -> (OpInfo a1 a2 a3) -> a2 -> ([]+ ((,) VarId PhysReg)) -> [] a3+applyAllocs maxReg o =+ case o of {+ Build_OpInfo opKind0 opRefs0 moveOp0 swapOp saveOp0 restoreOp0+ applyAllocs0 -> applyAllocs0}++type BlockId = Prelude.Int++data BlockInfo blockType1 blockType2 opType1 opType2 =+ Build_BlockInfo (blockType1 -> BlockId) (blockType1 -> [] BlockId) + (blockType1 -> (,) ((,) ([] opType1) ([] opType1)) ([] opType1)) (blockType1+ -> ([]+ opType2) ->+ ([]+ opType2) ->+ ([]+ opType2) ->+ blockType2)++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) ([] a3))+ ([] a3)+blockOps b =+ case b of {+ Build_BlockInfo blockId0 blockSuccessors0 blockOps0 setBlockOps0 ->+ blockOps0}++setBlockOps :: (BlockInfo a1 a2 a3 a4) -> a1 -> ([] a4) -> ([] a4) -> ([] + a4) -> a2+setBlockOps b =+ case b of {+ Build_BlockInfo blockId0 blockSuccessors0 blockOps0 setBlockOps0 ->+ setBlockOps0}++allBlockOps :: (BlockInfo a1 a2 a3 a4) -> a1 -> [] a3+allBlockOps binfo block =+ case blockOps binfo block of {+ (,) p c ->+ case p of {+ (,) a b -> (Prelude.++) a ((Prelude.++) b c)}}++blockSize :: (BlockInfo a1 a2 a3 a4) -> a1 -> Prelude.Int+blockSize binfo block =+ Data.List.length (allBlockOps binfo block)++type OpId = Prelude.Int++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 (allBlockOps binfo blk)) z++countOps :: (BlockInfo a1 a2 a3 a4) -> ([] a1) -> Prelude.Int+countOps binfo =+ foldOps binfo (\acc x -> (Prelude.succ) acc) 0+
+ LinearScan/Build.hs view
@@ -0,0 +1,419 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Build where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Blocks as Blocks+import qualified LinearScan.Datatypes as Datatypes+import qualified LinearScan.IntMap as IntMap+import qualified LinearScan.Interval as Interval+import qualified LinearScan.Lib as Lib+import qualified LinearScan.LiveSets as LiveSets+import qualified LinearScan.Morph as Morph+import qualified LinearScan.NonEmpty0 as NonEmpty0+import qualified LinearScan.Range as Range+import qualified LinearScan.ScanState as ScanState+import qualified LinearScan.UsePos as UsePos+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Fintype as Fintype+import qualified LinearScan.Seq as Seq+import qualified LinearScan.Ssrbool as Ssrbool+import qualified LinearScan.Ssrfun as Ssrfun+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"++type BuildState = Data.IntMap.IntMap Range.SortedRanges++newBuildState :: Prelude.Int -> BuildState+newBuildState n =+ IntMap.emptyIntMap++data RangeCursor =+ Build_RangeCursor Prelude.Int Range.BoundedRange Range.SortedRanges++emptyRangeCursor :: Prelude.Int -> Prelude.Int -> Prelude.Int -> RangeCursor+emptyRangeCursor b pos e =+ (Prelude.flip (Prelude.$)) __ (\_ -> Build_RangeCursor pos+ (Range.emptyBoundedRange ((Prelude.succ) (Ssrnat.double b))+ ((Prelude.succ) (Ssrnat.double pos)))+ (Range.emptySortedRanges ((Prelude.succ) (Ssrnat.double pos))))++transportRangeCursor :: Prelude.Int -> Prelude.Int -> Prelude.Int ->+ Prelude.Int -> RangeCursor -> RangeCursor+transportRangeCursor b prev base e c =+ let {_evar_0_ = \mid r rs -> Build_RangeCursor mid r rs} in+ case c of {+ Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1}++type PendingRanges = (Data.IntMap.IntMap RangeCursor)++emptyPendingRanges :: Prelude.Int -> Prelude.Int -> Prelude.Int ->+ Prelude.Int -> Data.IntSet.IntSet -> PendingRanges+emptyPendingRanges maxReg b pos e liveOuts =+ (Prelude.flip (Prelude.$)) (emptyRangeCursor b pos e) (\empty ->+ (Prelude.flip (Prelude.$)) (\xs vid ->+ Data.IntMap.insert ((Prelude.+) vid maxReg) empty xs) (\f ->+ Data.IntSet.foldl' f IntMap.emptyIntMap liveOuts))++mergeIntoSortedRanges :: Prelude.Int -> Prelude.Int -> PendingRanges ->+ (Data.IntMap.IntMap Range.SortedRanges) ->+ Data.IntMap.IntMap Range.SortedRanges+mergeIntoSortedRanges b pos pmap rmap =+ Data.IntMap.mergeWithKey (\_the_1st_wildcard_ _top_assumption_ ->+ let {+ _evar_0_ = \mid br ps rs ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ let {+ ps' = Range.prependRange ((Prelude.succ) (Ssrnat.double b))+ ((Prelude.succ) (Ssrnat.double mid)) br ps ((Prelude.succ)+ (Ssrnat.double b))}+ in+ Prelude.Just+ (Range.coq_SortedRanges_cat ((Prelude.succ) (Ssrnat.double b)) ps'+ ((Prelude.succ) (Ssrnat.double pos)) rs))}+ in+ (\rs ->+ case _top_assumption_ of {+ Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1 rs}))+ (Data.IntMap.map (\_top_assumption_ ->+ let {+ _evar_0_ = \_cursorMid_ br rs ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ + (Range.prependRange ((Prelude.succ) (Ssrnat.double b))+ ((Prelude.succ) (Ssrnat.double _cursorMid_)) br rs+ ((Prelude.succ) (Ssrnat.double b))))}+ in+ case _top_assumption_ of {+ Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1}))+ (Data.IntMap.map+ (Range.transportSortedRanges ((Prelude.succ) (Ssrnat.double b))+ ((Prelude.succ) (Ssrnat.double pos)))) ( pmap) rmap++varKindLtn :: Blocks.VarKind -> Blocks.VarKind -> Prelude.Bool+varKindLtn x y =+ case x of {+ Blocks.Input ->+ case y of {+ Blocks.Input -> Prelude.False;+ _ -> Prelude.True};+ Blocks.Temp ->+ case y of {+ Blocks.Output -> Prelude.True;+ _ -> Prelude.False};+ Blocks.Output -> Prelude.False}++handleVars_combine :: Prelude.Int -> Prelude.Int -> Prelude.Int ->+ Prelude.Int -> RangeCursor -> ((,) Prelude.Bool+ ([] Blocks.VarKind)) -> Prelude.Maybe RangeCursor+handleVars_combine b pos e vid range vars =+ let {+ _evar_0_ = \mid br srs ->+ let {+ _evar_0_ = \req kinds ->+ let {+ upos = UsePos.Build_UsePos ((Prelude.succ) (Ssrnat.double pos)) req}+ in+ (Prelude.flip (Prelude.$)) __ (\_ ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ let {+ _evar_0_ = \_ ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ let {+ r2 = Range.coq_Range_cons upos (Range.Build_RangeDesc+ ((Prelude.succ) (Ssrnat.double pos))+ (Range.rend ( br)) (Range.ups ( br)))}+ in+ Prelude.Just (Build_RangeCursor mid r2 srs))}+ in+ let {+ _evar_0_0 = \_ ->+ let {+ _evar_0_0 = \_ ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ let {r1 = Range.coq_Range_cons upos ( ( br))} in+ Prelude.Just (Build_RangeCursor mid r1 srs))}+ in+ let {+ _evar_0_1 = \_ ->+ let {r1 = Range.newRange upos} in+ let {+ _evar_0_1 = \_ ->+ (Prelude.flip (Prelude.$)) __ (\_ -> Prelude.Just+ (Build_RangeCursor ((Prelude.succ) pos) r1+ (+ (Range.prependRange ((Prelude.succ) (Ssrnat.double b))+ ((Prelude.succ) (Ssrnat.double mid)) br srs+ ((Prelude.succ)+ (Ssrnat.double ((Prelude.succ) pos)))))))}+ in+ _evar_0_1 __}+ in+ case (Prelude.<=) (Range.rbeg ( ( br))) (UsePos.uloc upos) of {+ Prelude.True -> _evar_0_0 __;+ Prelude.False -> _evar_0_1 __}}+ in+ case (Prelude.&&)+ (Ssrbool.in_mem (unsafeCoerce Blocks.Output)+ (Ssrbool.mem+ (Seq.seq_predType Blocks.coq_VarKind_eqType) kinds))+ (Prelude.not+ (Ssrbool.in_mem (unsafeCoerce Blocks.Input)+ (Ssrbool.mem+ (Seq.seq_predType Blocks.coq_VarKind_eqType) kinds))) of {+ Prelude.True -> _evar_0_ __;+ Prelude.False -> _evar_0_0 __})))}+ in+ case vars of {+ (,) x x0 -> unsafeCoerce _evar_0_ x x0}}+ in+ case range of {+ Build_RangeCursor x x0 x1 -> _evar_0_ x x0 x1}++handleVars_onlyRanges :: Prelude.Int -> Prelude.Int -> Prelude.Int ->+ (Data.IntMap.IntMap RangeCursor) ->+ Data.IntMap.IntMap RangeCursor+handleVars_onlyRanges b pos e =+ Data.IntMap.map (transportRangeCursor b ((Prelude.succ) pos) pos e)++handleVars_onlyVars :: Prelude.Int -> Prelude.Int -> Prelude.Int ->+ (Data.IntMap.IntMap+ ((,) Prelude.Bool ([] Blocks.VarKind))) ->+ Data.IntMap.IntMap RangeCursor+handleVars_onlyVars b pos e =+ Data.IntMap.map (\_top_assumption_ ->+ let {+ _evar_0_ = \req kinds ->+ let {+ rd = Range.Build_RangeDesc+ (case Ssrbool.in_mem (unsafeCoerce Blocks.Input)+ (Ssrbool.mem (Seq.seq_predType Blocks.coq_VarKind_eqType)+ kinds) of {+ Prelude.True -> (Prelude.succ) (Ssrnat.double b);+ Prelude.False -> (Prelude.succ) (Ssrnat.double pos)})+ (case Ssrbool.in_mem (unsafeCoerce Blocks.Output)+ (Ssrbool.mem (Seq.seq_predType Blocks.coq_VarKind_eqType)+ kinds) of {+ Prelude.True -> (Prelude.succ) (Ssrnat.double e);+ Prelude.False -> (Prelude.succ) ((Prelude.succ)+ (Ssrnat.double pos))}) ((:) (UsePos.Build_UsePos ((Prelude.succ)+ (Ssrnat.double pos)) req) [])}+ in+ Build_RangeCursor e rd []}+ in+ case _top_assumption_ of {+ (,) x x0 -> unsafeCoerce _evar_0_ x x0})++extractVarInfo :: Prelude.Int -> ([] Blocks.VarInfo) -> (,) Prelude.Bool+ ([] Blocks.VarKind)+extractVarInfo maxReg xs =+ (,)+ (Prelude.not+ (Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce (Seq.find (Blocks.regRequired maxReg) xs))+ (unsafeCoerce (Data.List.length xs))))+ (Lib.sortBy varKindLtn (Prelude.map (\v -> Blocks.varKind maxReg v) xs))++handleVars :: Prelude.Int -> ([] Blocks.VarInfo) -> Prelude.Int ->+ Prelude.Int -> Prelude.Int -> PendingRanges -> PendingRanges+handleVars maxReg varRefs b pos e ranges =+ let {+ vars = Data.IntMap.map (extractVarInfo maxReg)+ (IntMap.coq_IntMap_groupOn (Blocks.nat_of_varId maxReg) varRefs)}+ in+ Data.IntMap.mergeWithKey (handleVars_combine b pos e)+ (handleVars_onlyRanges b pos e) (handleVars_onlyVars b pos e) ( ranges)+ vars++reduceOp :: Prelude.Int -> (Blocks.OpInfo a4 a2 a3) -> Prelude.Int ->+ Prelude.Int -> Prelude.Int -> a1 -> a2 -> PendingRanges ->+ PendingRanges+reduceOp maxReg oinfo b pos e block op ranges =+ let {refs = Blocks.opRefs maxReg oinfo op} in+ let {+ refs' = case Blocks.opKind maxReg oinfo op of {+ Blocks.IsCall ->+ (Prelude.++)+ (Fintype.image_mem (Fintype.ordinal_finType maxReg) (\n ->+ Blocks.Build_VarInfo (Prelude.Left (unsafeCoerce n))+ Blocks.Temp Prelude.True)+ (Ssrbool.mem+ (Seq.seq_predType (Fintype.ordinal_eqType maxReg))+ (unsafeCoerce (Fintype.ord_enum maxReg)))) refs;+ _ -> refs}}+ in+ handleVars maxReg refs' b pos e ranges++reduceBlock :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->+ (Blocks.OpInfo a5 a3 a4) -> Prelude.Int -> a1 -> PendingRanges+ -> PendingRanges+reduceBlock maxReg binfo oinfo pos block =+ let {sz = Blocks.blockSize binfo block} in+ let {e = (Prelude.+) pos sz} in+ let {ops = Blocks.allBlockOps binfo block} in+ let {+ _evar_0_ = let {_evar_0_ = let {_evar_0_ = \h -> h} in _evar_0_} in+ let {+ _evar_0_0 = \o os iHos ->+ let {+ _evar_0_0 = \ranges ->+ iHos+ (reduceOp maxReg oinfo pos+ ((Prelude.+) pos (Data.List.length os)) e block o+ ranges)}+ in+ _evar_0_0}+ in+ Datatypes.list_rec _evar_0_ _evar_0_0 (Seq.rev ops)}+ in+ _evar_0_++reduceBlocks :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->+ (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> (Data.IntMap.IntMap+ LiveSets.BlockLiveSets) -> Prelude.Int -> BuildState+reduceBlocks maxReg binfo oinfo blocks liveSets pos =+ let {_evar_0_ = \pos0 -> newBuildState pos0} in+ let {+ _evar_0_0 = \b blocks0 iHbs pos0 ->+ (Prelude.flip (Prelude.$)) (Blocks.blockId binfo b) (\bid ->+ (Prelude.flip (Prelude.$))+ (case Data.IntMap.lookup bid liveSets of {+ Prelude.Just ls -> LiveSets.blockLiveOut ls;+ Prelude.Nothing -> Data.IntSet.empty}) (\outs ->+ let {sz = Blocks.blockSize binfo b} in+ let {+ _evar_0_0 = \_ ->+ let {endpos = (Prelude.+) pos0 sz} in+ (Prelude.flip (Prelude.$)) __ (\_ ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ (Prelude.flip (Prelude.$))+ (reduceBlock maxReg binfo oinfo pos0 b+ (emptyPendingRanges maxReg pos0 endpos endpos outs))+ (\pending ->+ mergeIntoSortedRanges pos0 endpos pending (iHbs endpos))))}+ in+ let {_evar_0_1 = \_ -> iHbs pos0} in+ case (Prelude.<=) ((Prelude.succ) 0) sz of {+ Prelude.True -> _evar_0_0 __;+ Prelude.False -> _evar_0_1 __}))}+ in+ Datatypes.list_rec _evar_0_ _evar_0_0 blocks pos++compileIntervals :: Prelude.Int -> Prelude.Int -> BuildState -> (,)+ ScanState.FixedIntervalsType+ (Data.IntMap.IntMap Interval.IntervalDesc)+compileIntervals maxReg pos bs =+ Data.IntMap.foldlWithKey (\_top_assumption_ ->+ let {+ _evar_0_ = \regs vars vid rs ->+ let {_evar_0_ = \_ -> (,) regs vars} in+ let {+ _evar_0_0 = \_a_ _l_ ->+ let {+ _evar_0_0 = \_ -> (,)+ (LinearScan.Utils.set_nth maxReg regs ( vid) (Prelude.Just+ (Interval.packInterval (Interval.Build_IntervalDesc vid+ (Range.rbeg+ ( (Prelude.head (NonEmpty0.coq_NE_from_list _a_ _l_))))+ (Range.rend+ ( (Prelude.last (NonEmpty0.coq_NE_from_list _a_ _l_))))+ Interval.Whole (NonEmpty0.coq_NE_from_list _a_ _l_))))) vars}+ in+ let {+ _evar_0_1 = \_ ->+ (Prelude.flip (Prelude.$)) ((Prelude.-) vid maxReg) (\vid' -> (,)+ regs+ (Data.IntMap.insert vid'+ (Interval.packInterval (Interval.Build_IntervalDesc vid'+ (Range.rbeg+ ( (Prelude.head (NonEmpty0.coq_NE_from_list _a_ _l_))))+ (Range.rend+ ( (Prelude.last (NonEmpty0.coq_NE_from_list _a_ _l_))))+ Interval.Whole (NonEmpty0.coq_NE_from_list _a_ _l_))) vars))}+ in+ case (Prelude.<=) ((Prelude.succ) vid) maxReg of {+ Prelude.True -> _evar_0_0 __;+ Prelude.False -> _evar_0_1 __}}+ in+ case (Ssrfun.sig_of_sig2 rs) of {+ [] -> _evar_0_ __;+ (:) x x0 -> _evar_0_0 x x0}}+ in+ case _top_assumption_ of {+ (,) x x0 -> _evar_0_ x x0}) ((,)+ (Data.List.replicate maxReg Prelude.Nothing) IntMap.emptyIntMap) bs++buildIntervals :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->+ (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> (Data.IntMap.IntMap+ LiveSets.BlockLiveSets) -> Prelude.Either Morph.SSError+ ScanState.ScanStateSig+buildIntervals maxReg binfo oinfo blocks liveSets =+ let {+ handleVar = \ss i ->+ ScanState.packScanState maxReg ScanState.Pending+ (ScanState.Build_ScanStateDesc ((Prelude.succ)+ (ScanState.nextInterval maxReg ( ss)))+ (LinearScan.Utils.snoc (ScanState.nextInterval maxReg ( ss))+ (ScanState.intervals maxReg ( ss)) ( i))+ (ScanState.fixedIntervals maxReg ( ss))+ (Lib.insert (Lib.lebf Prelude.snd) ((,)+ ( (ScanState.nextInterval maxReg ( ss))) (Interval.ibeg ( i)))+ (Prelude.map Prelude.id (ScanState.unhandled maxReg ( ss))))+ (Prelude.map Prelude.id (ScanState.active maxReg ( ss)))+ (Prelude.map Prelude.id (ScanState.inactive maxReg ( ss)))+ (Prelude.map Prelude.id (ScanState.handled maxReg ( ss))))}+ in+ case blocks of {+ [] -> Prelude.Right+ (ScanState.packScanState maxReg ScanState.InUse+ (ScanState.Build_ScanStateDesc 0 []+ (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []));+ (:) b bs ->+ let {bs0 = reduceBlocks maxReg binfo oinfo ((:) b bs) liveSets 0} in+ case compileIntervals maxReg 0 bs0 of {+ (,) regs vars ->+ let {+ s2 = ScanState.packScanState maxReg ScanState.Pending+ (ScanState.Build_ScanStateDesc+ (ScanState.nextInterval maxReg (ScanState.Build_ScanStateDesc 0+ [] (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []))+ (ScanState.intervals maxReg (ScanState.Build_ScanStateDesc 0 []+ (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []))+ regs+ (ScanState.unhandled maxReg (ScanState.Build_ScanStateDesc 0 []+ (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []))+ (ScanState.active maxReg (ScanState.Build_ScanStateDesc 0 []+ (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []))+ (ScanState.inactive maxReg (ScanState.Build_ScanStateDesc 0 []+ (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []))+ (ScanState.handled maxReg (ScanState.Build_ScanStateDesc 0 []+ (Data.List.replicate maxReg Prelude.Nothing) [] [] [] [])))}+ in+ let {s3 = Data.IntMap.foldl handleVar s2 vars} in+ Prelude.Right (ScanState.packScanState maxReg ScanState.InUse ( s3))}}+
+ LinearScan/Choice.hs view
@@ -0,0 +1,323 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Choice where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Logic as Logic+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Ssrbool as Ssrbool+import qualified LinearScan.Ssrfun as Ssrfun+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"++type Choice__Coq_mixin_of t =+ (Ssrbool.Coq_pred t) -> Prelude.Int -> Prelude.Maybe t+ -- singleton inductive, whose constructor was Mixin+ +_Choice__mixin_of_rect :: (((Ssrbool.Coq_pred a1) -> Prelude.Int ->+ Prelude.Maybe a1) -> () -> () -> () -> a2) ->+ (Choice__Coq_mixin_of a1) -> a2+_Choice__mixin_of_rect f m =+ f m __ __ __++_Choice__mixin_of_rec :: (((Ssrbool.Coq_pred a1) -> Prelude.Int ->+ Prelude.Maybe a1) -> () -> () -> () -> a2) ->+ (Choice__Coq_mixin_of a1) -> a2+_Choice__mixin_of_rec =+ _Choice__mixin_of_rect++_Choice__find :: (Choice__Coq_mixin_of a1) -> (Ssrbool.Coq_pred a1) ->+ Prelude.Int -> Prelude.Maybe a1+_Choice__find m =+ m++data Choice__Coq_class_of t =+ Choice__Class (Eqtype.Equality__Coq_mixin_of t) (Choice__Coq_mixin_of t)++_Choice__class_of_rect :: ((Eqtype.Equality__Coq_mixin_of a1) ->+ (Choice__Coq_mixin_of a1) -> a2) ->+ (Choice__Coq_class_of a1) -> a2+_Choice__class_of_rect f c =+ case c of {+ Choice__Class x x0 -> f x x0}++_Choice__class_of_rec :: ((Eqtype.Equality__Coq_mixin_of a1) ->+ (Choice__Coq_mixin_of a1) -> a2) ->+ (Choice__Coq_class_of a1) -> a2+_Choice__class_of_rec =+ _Choice__class_of_rect++_Choice__base :: (Choice__Coq_class_of a1) -> Eqtype.Equality__Coq_mixin_of+ a1+_Choice__base c =+ case c of {+ Choice__Class base0 mixin0 -> base0}++_Choice__mixin :: (Choice__Coq_class_of a1) -> Choice__Coq_mixin_of a1+_Choice__mixin c =+ case c of {+ Choice__Class base0 mixin0 -> mixin0}++type Choice__Coq_type =+ Choice__Coq_class_of ()+ -- singleton inductive, whose constructor was Pack+ +_Choice__type_rect :: (() -> (Choice__Coq_class_of ()) -> () -> a1) ->+ Choice__Coq_type -> a1+_Choice__type_rect f t =+ f __ t __++_Choice__type_rec :: (() -> (Choice__Coq_class_of ()) -> () -> a1) ->+ Choice__Coq_type -> a1+_Choice__type_rec =+ _Choice__type_rect++type Choice__Coq_sort = ()++_Choice__coq_class :: Choice__Coq_type -> Choice__Coq_class_of+ Choice__Coq_sort+_Choice__coq_class cT =+ cT++_Choice__clone :: Choice__Coq_type -> (Choice__Coq_class_of a1) ->+ Choice__Coq_type+_Choice__clone cT c =+ unsafeCoerce c++_Choice__pack :: (Choice__Coq_mixin_of a1) -> (Eqtype.Equality__Coq_mixin_of+ a1) -> Eqtype.Equality__Coq_type -> Choice__Coq_type+_Choice__pack m b bT =+ Choice__Class (unsafeCoerce b) (unsafeCoerce m)++_Choice__eqType :: Choice__Coq_type -> Eqtype.Equality__Coq_type+_Choice__eqType cT =+ _Choice__base (_Choice__coq_class cT)++_Choice__InternalTheory__find :: Choice__Coq_type -> (Ssrbool.Coq_pred+ Choice__Coq_sort) -> Prelude.Int ->+ Prelude.Maybe Choice__Coq_sort+_Choice__InternalTheory__find t =+ _Choice__find (_Choice__mixin (_Choice__coq_class t))++_Choice__InternalTheory__xchoose_subproof :: Choice__Coq_type ->+ (Ssrbool.Coq_pred+ Choice__Coq_sort) ->+ Choice__Coq_sort+_Choice__InternalTheory__xchoose_subproof t p =+ let {+ n = Ssrnat.ex_minnP (\n ->+ Ssrbool.isSome (_Choice__InternalTheory__find t p n))}+ in+ let {_evar_0_ = \x -> x} in+ let {_evar_0_0 = \_ _ -> Logic.coq_False_rect} in+ case _Choice__InternalTheory__find t p n of {+ Prelude.Just x -> _evar_0_ x;+ Prelude.Nothing -> _evar_0_0 __ __}++coq_PcanChoiceMixin :: Choice__Coq_type -> (a1 -> Choice__Coq_sort) ->+ (Choice__Coq_sort -> Prelude.Maybe a1) ->+ Choice__Coq_mixin_of a1+coq_PcanChoiceMixin t f f' =+ let {+ liftP = \sP ->+ Ssrbool.coq_SimplPred (\x ->+ Ssrfun._Option__apply sP Prelude.False (f' x))}+ in+ let {+ sf = \sP -> (\n ->+ Ssrfun._Option__bind f'+ (_Choice__InternalTheory__find t (Ssrbool.pred_of_simpl (liftP sP)) n))}+ in+ (\sP -> (Prelude.$) (sf sP))++sub_choiceMixin :: Choice__Coq_type -> (Ssrbool.Coq_pred Choice__Coq_sort) ->+ (Eqtype.Coq_subType Choice__Coq_sort) ->+ Choice__Coq_mixin_of+ (Eqtype.Coq_sub_sort Choice__Coq_sort)+sub_choiceMixin t p sT =+ coq_PcanChoiceMixin t (Eqtype.val p sT) (Eqtype.insub p sT)++nat_choiceMixin :: Choice__Coq_mixin_of Prelude.Int+nat_choiceMixin =+ let {+ f = \p -> (\n ->+ case p n of {+ Prelude.True -> Prelude.Just n;+ Prelude.False -> Prelude.Nothing})}+ in+ (\p -> (Prelude.$) (f p))++nat_choiceType :: Choice__Coq_type+nat_choiceType =+ Choice__Class (Eqtype._Equality__coq_class Ssrnat.nat_eqType)+ (unsafeCoerce nat_choiceMixin)++data Countable__Coq_mixin_of t =+ Countable__Mixin (t -> Prelude.Int) (Prelude.Int -> Prelude.Maybe t)++_Countable__mixin_of_rect :: ((a1 -> Prelude.Int) -> (Prelude.Int ->+ Prelude.Maybe a1) -> () -> a2) ->+ (Countable__Coq_mixin_of a1) -> a2+_Countable__mixin_of_rect f m =+ case m of {+ Countable__Mixin x x0 -> f x x0 __}++_Countable__mixin_of_rec :: ((a1 -> Prelude.Int) -> (Prelude.Int ->+ Prelude.Maybe a1) -> () -> a2) ->+ (Countable__Coq_mixin_of a1) -> a2+_Countable__mixin_of_rec =+ _Countable__mixin_of_rect++_Countable__pickle :: (Countable__Coq_mixin_of a1) -> a1 -> Prelude.Int+_Countable__pickle m =+ case m of {+ Countable__Mixin pickle0 unpickle0 -> pickle0}++_Countable__unpickle :: (Countable__Coq_mixin_of a1) -> Prelude.Int ->+ Prelude.Maybe a1+_Countable__unpickle m =+ case m of {+ Countable__Mixin pickle0 unpickle0 -> unpickle0}++_Countable__coq_EqMixin :: (Countable__Coq_mixin_of a1) ->+ Eqtype.Equality__Coq_mixin_of a1+_Countable__coq_EqMixin m =+ Eqtype.coq_PcanEqMixin Ssrnat.nat_eqType+ (unsafeCoerce (_Countable__pickle m))+ (unsafeCoerce (_Countable__unpickle m))++_Countable__coq_ChoiceMixin :: (Countable__Coq_mixin_of a1) ->+ Choice__Coq_mixin_of a1+_Countable__coq_ChoiceMixin m =+ coq_PcanChoiceMixin nat_choiceType (unsafeCoerce (_Countable__pickle m))+ (unsafeCoerce (_Countable__unpickle m))++data Countable__Coq_class_of t =+ Countable__Class (Choice__Coq_class_of t) (Countable__Coq_mixin_of t)++_Countable__class_of_rect :: ((Choice__Coq_class_of a1) ->+ (Countable__Coq_mixin_of a1) -> a2) ->+ (Countable__Coq_class_of a1) -> a2+_Countable__class_of_rect f c =+ case c of {+ Countable__Class x x0 -> f x x0}++_Countable__class_of_rec :: ((Choice__Coq_class_of a1) ->+ (Countable__Coq_mixin_of a1) -> a2) ->+ (Countable__Coq_class_of a1) -> a2+_Countable__class_of_rec =+ _Countable__class_of_rect++_Countable__base :: (Countable__Coq_class_of a1) -> Choice__Coq_class_of a1+_Countable__base c =+ case c of {+ Countable__Class base0 mixin0 -> base0}++_Countable__mixin :: (Countable__Coq_class_of a1) -> Countable__Coq_mixin_of+ a1+_Countable__mixin c =+ case c of {+ Countable__Class base0 mixin0 -> mixin0}++type Countable__Coq_type =+ Countable__Coq_class_of ()+ -- singleton inductive, whose constructor was Pack+ +_Countable__type_rect :: (() -> (Countable__Coq_class_of ()) -> () -> a1) ->+ Countable__Coq_type -> a1+_Countable__type_rect f t =+ f __ t __++_Countable__type_rec :: (() -> (Countable__Coq_class_of ()) -> () -> a1) ->+ Countable__Coq_type -> a1+_Countable__type_rec =+ _Countable__type_rect++type Countable__Coq_sort = ()++_Countable__coq_class :: Countable__Coq_type -> Countable__Coq_class_of+ Countable__Coq_sort+_Countable__coq_class cT =+ cT++_Countable__clone :: Countable__Coq_type -> (Countable__Coq_class_of + a1) -> Countable__Coq_type+_Countable__clone cT c =+ unsafeCoerce c++_Countable__pack :: (Countable__Coq_mixin_of a1) -> Choice__Coq_type ->+ (Choice__Coq_class_of a1) -> Countable__Coq_type+_Countable__pack m bT b =+ Countable__Class (unsafeCoerce b) (unsafeCoerce m)++_Countable__eqType :: Countable__Coq_type -> Eqtype.Equality__Coq_type+_Countable__eqType cT =+ _Choice__base (_Countable__base (_Countable__coq_class cT))++_Countable__choiceType :: Countable__Coq_type -> Choice__Coq_type+_Countable__choiceType cT =+ _Countable__base (_Countable__coq_class cT)++unpickle :: Countable__Coq_type -> Prelude.Int -> Prelude.Maybe+ Countable__Coq_sort+unpickle t =+ _Countable__unpickle (_Countable__mixin (_Countable__coq_class t))++pickle :: Countable__Coq_type -> Countable__Coq_sort -> Prelude.Int+pickle t =+ _Countable__pickle (_Countable__mixin (_Countable__coq_class t))++pickle_inv :: Countable__Coq_type -> Eqtype.Equality__Coq_sort ->+ Prelude.Maybe Countable__Coq_sort+pickle_inv t n =+ Ssrfun._Option__bind (\x ->+ case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (pickle t x)) n of {+ Prelude.True -> Prelude.Just x;+ Prelude.False -> Prelude.Nothing}) (unpickle t (unsafeCoerce n))++coq_PcanCountMixin :: Countable__Coq_type -> (a1 -> Countable__Coq_sort) ->+ (Countable__Coq_sort -> Prelude.Maybe a1) ->+ Countable__Coq_mixin_of a1+coq_PcanCountMixin t f f' =+ Countable__Mixin ((Prelude..) (pickle t) f) (Ssrfun.pcomp f' (unpickle t))++sub_countMixin :: Countable__Coq_type -> (Ssrbool.Coq_pred+ Countable__Coq_sort) -> (Eqtype.Coq_subType+ Countable__Coq_sort) -> Countable__Coq_mixin_of+ (Eqtype.Coq_sub_sort Countable__Coq_sort)+sub_countMixin t p sT =+ coq_PcanCountMixin t (Eqtype.val p sT) (Eqtype.insub p sT)++nat_countMixin :: Countable__Coq_mixin_of Prelude.Int+nat_countMixin =+ Countable__Mixin (\x -> x) (\x -> Prelude.Just x)++nat_countType :: Countable__Coq_type+nat_countType =+ Countable__Class (_Choice__coq_class nat_choiceType)+ (unsafeCoerce nat_countMixin)+
+ LinearScan/Cursor.hs view
@@ -0,0 +1,43 @@+module LinearScan.Cursor where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Interval as Interval+import qualified LinearScan.Morph as Morph+import qualified LinearScan.ScanState as ScanState+++__ :: any+__ = Prelude.error "Logical or arity value used"++curId :: Prelude.Int -> ScanState.ScanStateDesc -> (,) ScanState.IntervalId+ Prelude.Int+curId maxReg sd =+ Prelude.head (ScanState.unhandled maxReg sd)++curIntDetails :: Prelude.Int -> ScanState.ScanStateDesc ->+ Interval.IntervalDesc+curIntDetails maxReg sd =+ LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd) (Prelude.fst (curId maxReg sd))++curPosition :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int+curPosition maxReg sd =+ Interval.intervalStart ( (curIntDetails maxReg sd))++withCursor :: Prelude.Int -> ScanState.ScanStateDesc ->+ (ScanState.ScanStateDesc -> () -> Morph.SState () a1 a2) ->+ Morph.SState () a1 a2+withCursor maxReg pre f x =+ case x of {+ Morph.Build_SSInfo thisDesc _ ->+ f thisDesc __ (Morph.Build_SSInfo thisDesc __)}+
LinearScan/Datatypes.hs view
@@ -1,8 +1,10 @@ module LinearScan.Datatypes where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity@@ -14,4 +16,8 @@ case l of { [] -> f; (:) y l0 -> f0 y l0 (list_rect f f0 l0)}++list_rec :: a2 -> (a1 -> ([] a1) -> a2 -> a2) -> ([] a1) -> a2+list_rec =+ list_rect
LinearScan/Eqtype.hs view
@@ -4,13 +4,16 @@ module LinearScan.Eqtype where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity import qualified LinearScan.Utils +import qualified LinearScan.Specif as Specif import qualified LinearScan.Ssrbool as Ssrbool import qualified LinearScan.Ssrfun as Ssrfun @@ -100,17 +103,60 @@ case s of { SubType val0 sub x -> val0} +coq_Sub :: (Ssrbool.Coq_pred a1) -> (Coq_subType a1) -> a1 -> Coq_sub_sort a1+coq_Sub p s x =+ case s of {+ SubType val0 sub x0 -> sub x __}++insub :: (Ssrbool.Coq_pred a1) -> (Coq_subType a1) -> a1 -> Prelude.Maybe+ (Coq_sub_sort a1)+insub p sT x =+ case Ssrbool.idP (p x) of {+ Ssrbool.ReflectT -> Prelude.Just (coq_Sub p sT x);+ Ssrbool.ReflectF -> Prelude.Nothing}++s2val :: (Specif.Coq_sig2 a1) -> a1+s2val u =+ u++sig_subType :: (Ssrbool.Coq_pred a1) -> Coq_subType a1+sig_subType p =+ SubType (unsafeCoerce ) (unsafeCoerce (\x _ -> x)) (\_ k_S u ->+ k_S (unsafeCoerce u) __)+ inj_eqAxiom :: Equality__Coq_type -> (a1 -> Equality__Coq_sort) -> Equality__Coq_axiom a1 inj_eqAxiom eT f x y = Ssrbool.iffP (eq_op eT (f x) (f y)) (eqP eT (f x) (f y)) +coq_InjEqMixin :: Equality__Coq_type -> (a1 -> Equality__Coq_sort) ->+ Equality__Coq_mixin_of a1+coq_InjEqMixin eT f =+ Equality__Mixin (\x y -> eq_op eT (f x) (f y)) (inj_eqAxiom eT f)++coq_PcanEqMixin :: Equality__Coq_type -> (a1 -> Equality__Coq_sort) ->+ (Equality__Coq_sort -> Prelude.Maybe a1) ->+ Equality__Coq_mixin_of a1+coq_PcanEqMixin eT f g =+ coq_InjEqMixin eT f+ val_eqP :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) -> (Coq_subType Equality__Coq_sort) -> Equality__Coq_axiom (Coq_sub_sort Equality__Coq_sort) val_eqP t p sT = inj_eqAxiom t (val p sT) +sig_eqMixin :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) ->+ Equality__Coq_mixin_of Equality__Coq_sort+sig_eqMixin t p =+ Equality__Mixin (\x y -> eq_op t ( x) ( y))+ (unsafeCoerce (val_eqP t (\x -> p x) (sig_subType p)))++sig_eqType :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) ->+ Equality__Coq_type+sig_eqType t p =+ unsafeCoerce (sig_eqMixin t p)+ pair_eq :: Equality__Coq_type -> Equality__Coq_type -> Ssrbool.Coq_simpl_rel ((,) Equality__Coq_sort Equality__Coq_sort) pair_eq t1 t2 =@@ -182,4 +228,51 @@ option_eqType :: Equality__Coq_type -> Equality__Coq_type option_eqType t = unsafeCoerce (option_eqMixin t)++sum_eq :: Equality__Coq_type -> Equality__Coq_type -> (Prelude.Either+ Equality__Coq_sort Equality__Coq_sort) -> (Prelude.Either+ Equality__Coq_sort Equality__Coq_sort) -> Prelude.Bool+sum_eq t1 t2 u v =+ case u of {+ Prelude.Left x ->+ case v of {+ Prelude.Left y -> eq_op t1 x y;+ Prelude.Right s -> Prelude.False};+ Prelude.Right x ->+ case v of {+ Prelude.Left s -> Prelude.False;+ Prelude.Right y -> eq_op t2 x y}}++sum_eqP :: Equality__Coq_type -> Equality__Coq_type -> Equality__Coq_axiom+ (Prelude.Either Equality__Coq_sort Equality__Coq_sort)+sum_eqP t1 t2 _top_assumption_ =+ let {+ _evar_0_ = \x _top_assumption_0 ->+ let {_evar_0_ = \y -> Ssrbool.iffP (eq_op t1 x y) (eqP t1 x y)} in+ let {_evar_0_0 = \y -> Ssrbool.ReflectF} in+ case _top_assumption_0 of {+ Prelude.Left x0 -> _evar_0_ x0;+ Prelude.Right x0 -> _evar_0_0 x0}}+ in+ let {+ _evar_0_0 = \x _top_assumption_0 ->+ let {_evar_0_0 = \y -> Ssrbool.ReflectF} in+ let {_evar_0_1 = \y -> Ssrbool.iffP (eq_op t2 x y) (eqP t2 x y)} in+ case _top_assumption_0 of {+ Prelude.Left x0 -> _evar_0_0 x0;+ Prelude.Right x0 -> _evar_0_1 x0}}+ in+ case _top_assumption_ of {+ Prelude.Left x -> _evar_0_ x;+ Prelude.Right x -> _evar_0_0 x}++sum_eqMixin :: Equality__Coq_type -> Equality__Coq_type ->+ Equality__Coq_mixin_of+ (Prelude.Either Equality__Coq_sort Equality__Coq_sort)+sum_eqMixin t1 t2 =+ Equality__Mixin (sum_eq t1 t2) (sum_eqP t1 t2)++sum_eqType :: Equality__Coq_type -> Equality__Coq_type -> Equality__Coq_type+sum_eqType t1 t2 =+ unsafeCoerce (sum_eqMixin t1 t2)
LinearScan/Fintype.hs view
@@ -4,14 +4,19 @@ module LinearScan.Fintype where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity import qualified LinearScan.Utils +import qualified LinearScan.Choice as Choice import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Seq as Seq+import qualified LinearScan.Ssrbool as Ssrbool import qualified LinearScan.Ssrnat as Ssrnat @@ -29,6 +34,157 @@ __ :: any __ = Prelude.error "Logical or arity value used" +data Finite__Coq_mixin_of =+ Finite__Mixin (Choice.Countable__Coq_mixin_of Eqtype.Equality__Coq_sort) + ([] Eqtype.Equality__Coq_sort)++_Finite__mixin_of_rect :: Eqtype.Equality__Coq_type ->+ ((Choice.Countable__Coq_mixin_of+ Eqtype.Equality__Coq_sort) -> ([]+ Eqtype.Equality__Coq_sort) -> () -> a1) ->+ Finite__Coq_mixin_of -> a1+_Finite__mixin_of_rect t f m =+ case m of {+ Finite__Mixin x x0 -> f x x0 __}++_Finite__mixin_of_rec :: Eqtype.Equality__Coq_type ->+ ((Choice.Countable__Coq_mixin_of+ Eqtype.Equality__Coq_sort) -> ([]+ Eqtype.Equality__Coq_sort) -> () -> a1) ->+ Finite__Coq_mixin_of -> a1+_Finite__mixin_of_rec t =+ _Finite__mixin_of_rect t++_Finite__mixin_base :: Eqtype.Equality__Coq_type -> Finite__Coq_mixin_of ->+ Choice.Countable__Coq_mixin_of+ Eqtype.Equality__Coq_sort+_Finite__mixin_base t m =+ case m of {+ Finite__Mixin mixin_base0 mixin_enum0 -> mixin_base0}++_Finite__mixin_enum :: Eqtype.Equality__Coq_type -> Finite__Coq_mixin_of ->+ [] Eqtype.Equality__Coq_sort+_Finite__mixin_enum t m =+ case m of {+ Finite__Mixin mixin_base0 mixin_enum0 -> mixin_enum0}++_Finite__coq_EnumMixin :: Choice.Countable__Coq_type -> ([]+ Choice.Countable__Coq_sort) -> Finite__Coq_mixin_of+_Finite__coq_EnumMixin t e =+ case t of {+ Choice.Countable__Class base0 m -> Finite__Mixin m e}++_Finite__coq_UniqMixin :: Choice.Countable__Coq_type -> ([]+ Choice.Countable__Coq_sort) -> Finite__Coq_mixin_of+_Finite__coq_UniqMixin t e =+ _Finite__coq_EnumMixin t e++_Finite__count_enum :: Choice.Countable__Coq_type -> Prelude.Int -> []+ Choice.Countable__Coq_sort+_Finite__count_enum t n =+ Seq.pmap (unsafeCoerce (Choice.pickle_inv t)) (Seq.iota 0 n)++_Finite__coq_CountMixin :: Choice.Countable__Coq_type -> Prelude.Int ->+ Finite__Coq_mixin_of+_Finite__coq_CountMixin t n =+ _Finite__coq_EnumMixin t (_Finite__count_enum t n)++data Finite__Coq_class_of t =+ Finite__Class (Choice.Choice__Coq_class_of t) Finite__Coq_mixin_of++_Finite__class_of_rect :: ((Choice.Choice__Coq_class_of a1) ->+ Finite__Coq_mixin_of -> a2) ->+ (Finite__Coq_class_of a1) -> a2+_Finite__class_of_rect f c =+ case c of {+ Finite__Class x x0 -> f x x0}++_Finite__class_of_rec :: ((Choice.Choice__Coq_class_of a1) ->+ Finite__Coq_mixin_of -> a2) -> (Finite__Coq_class_of+ a1) -> a2+_Finite__class_of_rec =+ _Finite__class_of_rect++_Finite__base :: (Finite__Coq_class_of a1) -> Choice.Choice__Coq_class_of a1+_Finite__base c =+ case c of {+ Finite__Class base0 mixin0 -> base0}++_Finite__mixin :: (Finite__Coq_class_of a1) -> Finite__Coq_mixin_of+_Finite__mixin c =+ case c of {+ Finite__Class base0 mixin0 -> mixin0}++_Finite__base2 :: (Finite__Coq_class_of a1) -> Choice.Countable__Coq_class_of+ a1+_Finite__base2 c =+ Choice.Countable__Class (_Finite__base c)+ (unsafeCoerce+ (_Finite__mixin_base+ (Choice._Choice__base (_Finite__base (unsafeCoerce c)))+ (_Finite__mixin c)))++type Finite__Coq_type =+ Finite__Coq_class_of ()+ -- singleton inductive, whose constructor was Pack+ +_Finite__type_rect :: (() -> (Finite__Coq_class_of ()) -> () -> a1) ->+ Finite__Coq_type -> a1+_Finite__type_rect f t =+ f __ t __++_Finite__type_rec :: (() -> (Finite__Coq_class_of ()) -> () -> a1) ->+ Finite__Coq_type -> a1+_Finite__type_rec =+ _Finite__type_rect++type Finite__Coq_sort = ()++_Finite__coq_class :: Finite__Coq_type -> Finite__Coq_class_of+ Finite__Coq_sort+_Finite__coq_class cT =+ cT++_Finite__clone :: Finite__Coq_type -> (Finite__Coq_class_of a1) ->+ Finite__Coq_type+_Finite__clone cT c =+ unsafeCoerce c++_Finite__pack :: (Eqtype.Equality__Coq_mixin_of a1) -> Finite__Coq_mixin_of+ -> Choice.Choice__Coq_type -> (Choice.Choice__Coq_class_of+ a1) -> Finite__Coq_mixin_of -> Finite__Coq_type+_Finite__pack b0 m0 bT b m =+ Finite__Class (unsafeCoerce b) m++_Finite__eqType :: Finite__Coq_type -> Eqtype.Equality__Coq_type+_Finite__eqType cT =+ Choice._Choice__base (_Finite__base (_Finite__coq_class cT))++_Finite__choiceType :: Finite__Coq_type -> Choice.Choice__Coq_type+_Finite__choiceType cT =+ _Finite__base (_Finite__coq_class cT)++_Finite__countType :: Finite__Coq_type -> Choice.Countable__Coq_type+_Finite__countType cT =+ _Finite__base2 (_Finite__coq_class cT)++_Finite__EnumDef__enum :: Finite__Coq_type -> [] Finite__Coq_sort+_Finite__EnumDef__enum cT =+ _Finite__mixin_enum+ (Choice._Choice__base (_Finite__base (_Finite__coq_class cT)))+ (_Finite__mixin (_Finite__coq_class cT))++enum_mem :: Finite__Coq_type -> (Ssrbool.Coq_mem_pred Finite__Coq_sort) -> []+ Finite__Coq_sort+enum_mem t mA =+ Prelude.filter (Ssrbool.pred_of_simpl (Ssrbool.pred_of_mem_pred mA))+ (_Finite__EnumDef__enum t)++image_mem :: Finite__Coq_type -> (Finite__Coq_sort -> a1) ->+ (Ssrbool.Coq_mem_pred Finite__Coq_sort) -> [] a1+image_mem t f mA =+ Prelude.map f (enum_mem t mA)+ ordinal_subType :: Prelude.Int -> Eqtype.Coq_subType Prelude.Int ordinal_subType n = Eqtype.SubType (unsafeCoerce ) (unsafeCoerce (\x _ -> x)) (\_ k_S u ->@@ -47,4 +203,41 @@ ordinal_eqType :: Prelude.Int -> Eqtype.Equality__Coq_type ordinal_eqType n = unsafeCoerce (ordinal_eqMixin n)++ordinal_choiceMixin :: Prelude.Int -> Choice.Choice__Coq_mixin_of Prelude.Int+ordinal_choiceMixin n =+ unsafeCoerce+ (Choice.sub_choiceMixin Choice.nat_choiceType (\x ->+ (Prelude.<=) ((Prelude.succ) (unsafeCoerce x)) n)+ (unsafeCoerce (ordinal_subType n)))++ordinal_choiceType :: Prelude.Int -> Choice.Choice__Coq_type+ordinal_choiceType n =+ Choice.Choice__Class (Eqtype._Equality__coq_class (ordinal_eqType n))+ (unsafeCoerce (ordinal_choiceMixin n))++ordinal_countMixin :: Prelude.Int -> Choice.Countable__Coq_mixin_of+ Prelude.Int+ordinal_countMixin n =+ unsafeCoerce+ (Choice.sub_countMixin Choice.nat_countType (\x ->+ (Prelude.<=) ((Prelude.succ) (unsafeCoerce x)) n)+ (unsafeCoerce (ordinal_subType n)))++ord_enum :: Prelude.Int -> [] Prelude.Int+ord_enum n =+ Seq.pmap+ (unsafeCoerce+ (Eqtype.insub (\x -> (Prelude.<=) ((Prelude.succ) x) n)+ (ordinal_subType n))) (Seq.iota 0 n)++ordinal_finMixin :: Prelude.Int -> Finite__Coq_mixin_of+ordinal_finMixin n =+ Finite__Mixin (unsafeCoerce (ordinal_countMixin n))+ (unsafeCoerce (ord_enum n))++ordinal_finType :: Prelude.Int -> Finite__Coq_type+ordinal_finType n =+ Finite__Class (Choice._Choice__coq_class (ordinal_choiceType n))+ (ordinal_finMixin n)
+ LinearScan/Graph.hs view
@@ -0,0 +1,198 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Graph where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Seq as Seq+import qualified LinearScan.Ssrbool as Ssrbool++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++data Graph =+ Build_Graph ([] (Prelude.Maybe Eqtype.Equality__Coq_sort)) ([]+ ((,)+ (Prelude.Maybe+ Eqtype.Equality__Coq_sort)+ (Prelude.Maybe+ Eqtype.Equality__Coq_sort)))++vertices :: Eqtype.Equality__Coq_type -> Graph -> []+ (Prelude.Maybe Eqtype.Equality__Coq_sort)+vertices a g =+ case g of {+ Build_Graph vertices0 edges0 -> vertices0}++edges :: Eqtype.Equality__Coq_type -> Graph -> []+ ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)+ (Prelude.Maybe Eqtype.Equality__Coq_sort))+edges a g =+ case g of {+ Build_Graph vertices0 edges0 -> edges0}++emptyGraph :: Eqtype.Equality__Coq_type -> Graph+emptyGraph a =+ Build_Graph [] []++addVertex :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> Graph+ -> Graph+addVertex a v g =+ let {vg = vertices a g} in+ Build_Graph+ (case Ssrbool.in_mem v+ (Ssrbool.mem (Seq.seq_predType (Eqtype.option_eqType a))+ (unsafeCoerce vg)) of {+ Prelude.True -> vg;+ Prelude.False -> (:) (unsafeCoerce v) vg}) (edges a g)++addEdge :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> Graph ->+ Graph+addEdge a e g =+ let {+ g' = let {eg = edges a g} in+ Build_Graph (vertices a g)+ (case Ssrbool.in_mem e+ (Ssrbool.mem+ (Seq.seq_predType+ (Eqtype.prod_eqType (Eqtype.option_eqType a)+ (Eqtype.option_eqType a))) (unsafeCoerce eg)) of {+ Prelude.True -> eg;+ Prelude.False -> (:) (unsafeCoerce e) eg})}+ in+ addVertex a (Prelude.fst (unsafeCoerce e))+ (addVertex a (Prelude.snd (unsafeCoerce e)) g')++removeEdge :: Eqtype.Equality__Coq_type -> ((,)+ (Prelude.Maybe Eqtype.Equality__Coq_sort)+ (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> Graph -> Graph+removeEdge a x g =+ Build_Graph (vertices a g)+ (Prelude.filter (\y ->+ Prelude.not+ (Eqtype.eq_op+ (Eqtype.prod_eqType (Eqtype.option_eqType a)+ (Eqtype.option_eqType a)) (unsafeCoerce y) (unsafeCoerce x)))+ (edges a g))++connections :: Eqtype.Equality__Coq_type -> (((,)+ (Prelude.Maybe Eqtype.Equality__Coq_sort)+ (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> Prelude.Maybe+ Eqtype.Equality__Coq_sort) -> (Prelude.Maybe+ Eqtype.Equality__Coq_sort) -> Graph -> []+ ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)+ (Prelude.Maybe Eqtype.Equality__Coq_sort))+connections a f x g =+ Prelude.filter+ ((Prelude..) (\y ->+ Eqtype.eq_op (Eqtype.option_eqType a) (unsafeCoerce y) (unsafeCoerce x))+ f) (edges a g)++outbound :: Eqtype.Equality__Coq_type -> (Prelude.Maybe+ Eqtype.Equality__Coq_sort) -> Graph -> []+ ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)+ (Prelude.Maybe Eqtype.Equality__Coq_sort))+outbound a =+ connections a Prelude.fst++inbound :: Eqtype.Equality__Coq_type -> (Prelude.Maybe+ Eqtype.Equality__Coq_sort) -> Graph -> []+ ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)+ (Prelude.Maybe Eqtype.Equality__Coq_sort))+inbound a =+ connections a Prelude.snd++tsort' :: Eqtype.Equality__Coq_type -> Prelude.Int -> ([]+ ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)+ (Prelude.Maybe Eqtype.Equality__Coq_sort))) -> ([]+ (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> Graph -> []+ ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)+ (Prelude.Maybe Eqtype.Equality__Coq_sort))+tsort' a fuel l roots g =+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ ->+ Seq.rev l)+ (\fuel0 ->+ case edges a g of {+ [] -> Seq.rev l;+ (:) p es ->+ case p of {+ (,) se de ->+ case roots of {+ [] ->+ let {l0 = (:) de []} in+ let {+ g' = addEdge a (unsafeCoerce ((,) se Prelude.Nothing))+ (removeEdge a ((,) se de) g)}+ in+ case l0 of {+ [] -> [];+ (:) n s ->+ let {outEdges = outbound a n g'} in+ case Data.List.foldl' (\acc e ->+ case acc of {+ (,) res g'' -> (,) ((:) e res) (removeEdge a e g'')})+ ((,) [] g') outEdges of {+ (,) res g'' ->+ let {outNodes = Prelude.map Prelude.snd outEdges} in+ let {+ s' = (Prelude.++) s+ (Prelude.filter+ ((Prelude..) Seq.nilp (\x -> inbound a x g''))+ outNodes)}+ in+ tsort' a fuel0 ((Prelude.++) l res) s' g''}};+ (:) n s ->+ let {l0 = (:) n s} in+ case l0 of {+ [] -> [];+ (:) n0 s0 ->+ let {outEdges = outbound a n0 g} in+ case Data.List.foldl' (\acc e ->+ case acc of {+ (,) res g'' -> (,) ((:) e res) (removeEdge a e g'')})+ ((,) [] g) outEdges of {+ (,) res g'' ->+ let {outNodes = Prelude.map Prelude.snd outEdges} in+ let {+ s' = (Prelude.++) s0+ (Prelude.filter+ ((Prelude..) Seq.nilp (\x -> inbound a x g''))+ outNodes)}+ in+ tsort' a fuel0 ((Prelude.++) l res) s' g''}}}}})+ fuel++topsort :: Eqtype.Equality__Coq_type -> Graph -> []+ ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)+ (Prelude.Maybe Eqtype.Equality__Coq_sort))+topsort a g =+ let {+ noInbound = let {xs = Prelude.map Prelude.snd (edges a g)} in+ Prelude.filter (\x ->+ Prelude.not+ (Ssrbool.in_mem (unsafeCoerce x)+ (Ssrbool.mem (Seq.seq_predType (Eqtype.option_eqType a))+ (unsafeCoerce xs)))) (vertices a g)}+ in+ tsort' a ((Prelude.succ) (Data.List.length (vertices a g))) [] noInbound g+
LinearScan/IState.hs view
@@ -1,8 +1,10 @@ module LinearScan.IState where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity@@ -10,14 +12,6 @@ type IState errType i o a = i -> Prelude.Either errType ((,) a o)--ierr :: a1 -> IState a1 a2 a3 a4-ierr err x =- Prelude.Left err--iget :: IState a1 a2 a2 a2-iget i =- Prelude.Right ((,) i i) iput :: a3 -> IState a1 a2 a3 () iput x x0 =
+ LinearScan/IntMap.hs view
@@ -0,0 +1,48 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.IntMap where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Lib as Lib++++--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++emptyIntMap :: Data.IntMap.IntMap a1+emptyIntMap =+ Data.IntMap.fromList []++coq_IntSet_forFold :: a1 -> Data.IntSet.IntSet -> (a1 -> Prelude.Int -> a1)+ -> a1+coq_IntSet_forFold z m f =+ Data.IntSet.foldl' f z m++coq_IntMap_groupOn :: (a1 -> Prelude.Int) -> ([] a1) -> Data.IntMap.IntMap+ ([] a1)+coq_IntMap_groupOn p l =+ Lib.forFold emptyIntMap l (\acc x ->+ let {n = p x} in+ Data.IntMap.alter (\mxs ->+ case mxs of {+ Prelude.Just xs -> Prelude.Just ((:) x xs);+ Prelude.Nothing -> Prelude.Just ((:) x [])}) n acc)+
LinearScan/Interval.hs view
@@ -1,8 +1,10 @@ module LinearScan.Interval where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity@@ -11,6 +13,7 @@ import qualified LinearScan.Lib as Lib import qualified LinearScan.Logic as Logic import qualified LinearScan.Range as Range+import qualified LinearScan.UsePos as UsePos __ :: any@@ -86,7 +89,7 @@ Data.List.any (\x -> Data.List.any (f x) ( (rds j))) ( (rds i)) intervalIntersectionPoint :: IntervalDesc -> IntervalDesc -> Prelude.Maybe- Prelude.Int+ Lib.Coq_oddnum intervalIntersectionPoint i j = Data.List.foldl' (\acc rd -> case acc of {@@ -98,51 +101,58 @@ Prelude.Nothing -> Range.rangeIntersectionPoint ( rd) ( rd')}) Prelude.Nothing (rds j)}) Prelude.Nothing (rds i) -findIntervalUsePos :: IntervalDesc -> (Range.UsePos -> Prelude.Bool) ->- Prelude.Maybe ((,) Range.RangeDesc Range.UsePos)+searchInRange :: Range.RangeDesc -> (UsePos.UsePos -> Prelude.Bool) ->+ Prelude.Maybe ((,) Range.RangeDesc UsePos.UsePos)+searchInRange r f =+ let {_evar_0_ = \x -> Prelude.Just ((,) r x)} in+ let {_evar_0_0 = Prelude.Nothing} in+ case Range.findRangeUsePos ( r) f of {+ Prelude.Just x -> _evar_0_ x;+ Prelude.Nothing -> _evar_0_0}++findIntervalUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) ->+ Prelude.Maybe ((,) Range.RangeDesc UsePos.UsePos) findIntervalUsePos d f = let {- f0 = \r ->- case Range.findRangeUsePos r f of {- Prelude.Just pos -> Prelude.Just ((,) r pos);- Prelude.Nothing -> Prelude.Nothing}}- in- let { go rs = (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs) (\r ->- f0 r)+ searchInRange r f) (\r rs' ->- Lib.option_choose (f0 r) (go rs'))+ Lib.option_choose (searchInRange r f) (go rs')) rs} in go (rds d) -nextUseAfter :: IntervalDesc -> Prelude.Int -> Prelude.Maybe Prelude.Int+lookupUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) ->+ Prelude.Maybe Lib.Coq_oddnum+lookupUsePos d f =+ let {+ _evar_0_ = \_top_assumption_ ->+ let {+ _evar_0_ = \r _top_assumption_0 -> Prelude.Just+ (UsePos.uloc _top_assumption_0)}+ in+ case _top_assumption_ of {+ (,) x x0 -> _evar_0_ x x0}}+ in+ let {_evar_0_0 = Prelude.Nothing} in+ case findIntervalUsePos d f of {+ Prelude.Just x -> _evar_0_ x;+ Prelude.Nothing -> _evar_0_0}++nextUseAfter :: IntervalDesc -> Prelude.Int -> Prelude.Maybe Lib.Coq_oddnum nextUseAfter d pos =- Lib.option_map ((Prelude..) Range.uloc Prelude.snd)- (findIntervalUsePos d (\u ->- (Prelude.<=) ((Prelude.succ) pos) (Range.uloc u)))+ lookupUsePos d (\u -> (Prelude.<=) ((Prelude.succ) pos) (UsePos.uloc u)) -firstUsePos :: IntervalDesc -> Prelude.Int+firstUsePos :: IntervalDesc -> Prelude.Maybe Prelude.Int firstUsePos d =- Range.uloc (Prelude.head (Range.ups ( (Prelude.head (rds d)))))+ case Range.ups ( (Prelude.head (rds d))) of {+ [] -> Prelude.Nothing;+ (:) u l -> Prelude.Just (UsePos.uloc u)} -firstUseReqReg :: IntervalDesc -> Prelude.Maybe Prelude.Int+firstUseReqReg :: IntervalDesc -> Prelude.Maybe Lib.Coq_oddnum firstUseReqReg d =- Lib.option_map ((Prelude..) Range.uloc Prelude.snd)- (findIntervalUsePos d Range.regReq)--data SplitPosition =- BeforePos Prelude.Int- | BeforeFirstUsePosReqReg- | EndOfLifetimeHole--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}+ lookupUsePos d UsePos.regReq intervalSpan :: ([] Range.RangeDesc) -> Prelude.Int -> Prelude.Int -> Prelude.Int -> Prelude.Int -> IntervalKind ->@@ -163,11 +173,12 @@ 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))))}+ (packInterval (Build_IntervalDesc iv+ (Range.rbeg ( r0)) (Range.rend ( r0)) lknd ((:[])+ ( r0))))) (Prelude.Just+ (packInterval (Build_IntervalDesc iv+ (Range.rbeg ( r1)) (Range.rend ( r1)) rknd ((:[])+ ( r1)))))} in _evar_0_} in@@ -177,9 +188,9 @@ _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}+ (packInterval (Build_IntervalDesc iv+ (Range.rbeg ( r0)) (Range.rend ( r0))+ knd ((:[]) ( r0))))) Prelude.Nothing} in _evar_0_0} in@@ -196,8 +207,9 @@ let { _evar_0_0 = let { _evar_0_0 = \_ -> (,) Prelude.Nothing (Prelude.Just- (Build_IntervalDesc iv (Range.rbeg ( r1))- (Range.rend ( r1)) knd ((:[]) ( r1))))}+ (packInterval (Build_IntervalDesc iv+ (Range.rbeg ( r1)) (Range.rend ( r1)) knd ((:[])+ ( r1)))))} in _evar_0_0} in@@ -226,10 +238,11 @@ _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)))}+ _evar_0_ = \_ -> (,) (Prelude.Just+ (packInterval (Build_IntervalDesc iv (Range.rbeg ( r0))+ (Range.rend ( r0)) lknd ((:[]) ( r0))))) (Prelude.Just+ (packInterval (Build_IntervalDesc iv (Range.rbeg ( r1))+ (Range.rend ( (Prelude.last rs0))) rknd ((:) r1 rs0))))} in _evar_0_ __)} in@@ -264,13 +277,20 @@ _evar_0_0 = let { _evar_0_0 = \_ _ _ -> (,) (Prelude.Just- (Build_IntervalDesc- ivar0- (Range.rbeg ( r))- iend0 iknd0 ((:) r- rds0)))+ (packInterval+ (Build_IntervalDesc+ ivar0+ (Range.rbeg ( r))+ iend0 lknd ((:) r+ rds0)))) (Prelude.Just- i1_2)}+ (packInterval+ (Build_IntervalDesc+ (ivar ( i1_2))+ (ibeg ( i1_2))+ (iend ( i1_2))+ rknd+ (rds ( i1_2)))))} in _evar_0_0 __} in@@ -298,9 +318,11 @@ let { _evar_0_1 = \_ -> (,) (Prelude.Just- (Build_IntervalDesc ivar0- (Range.rbeg ( r)) iend0 iknd0- ((:) r rds0))) Prelude.Nothing}+ (packInterval+ (Build_IntervalDesc ivar0+ (Range.rbeg ( r)) iend0 lknd+ ((:) r rds0))))+ Prelude.Nothing} in _evar_0_1 __} in@@ -333,16 +355,42 @@ _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)))}+ (packInterval+ (Build_IntervalDesc iv+ (Range.rbeg ( r0))+ (Range.rend ( r0)) lknd+ ((:[]) ( r0)))))+ (Prelude.Just+ (packInterval+ (Build_IntervalDesc+ (ivar (Build_IntervalDesc+ ivar0+ (Range.rbeg+ ( (Prelude.head rds0)))+ (Range.rend+ ( (Prelude.last rds0)))+ iknd0 rds0))+ (ibeg (Build_IntervalDesc+ ivar0+ (Range.rbeg+ ( (Prelude.head rds0)))+ (Range.rend+ ( (Prelude.last rds0)))+ iknd0 rds0))+ (iend (Build_IntervalDesc+ ivar0+ (Range.rbeg+ ( (Prelude.head rds0)))+ (Range.rend+ ( (Prelude.last rds0)))+ iknd0 rds0)) rknd+ (rds (Build_IntervalDesc+ ivar0+ (Range.rbeg+ ( (Prelude.head rds0)))+ (Range.rend+ ( (Prelude.last rds0)))+ iknd0 rds0))))))} in _evar_0_1 __} in@@ -384,8 +432,8 @@ _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)))}+ (packInterval (Build_IntervalDesc iv (Range.rbeg ( r1))+ (Range.rend ( (Prelude.last rs0))) knd ((:) r1 rs0))))} in _evar_0_0 __} in
LinearScan/Lib.hs view
@@ -1,8 +1,10 @@ module LinearScan.Lib where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity@@ -10,35 +12,57 @@ import qualified LinearScan.Specif as Specif import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Ssrbool as Ssrbool __ :: any __ = Prelude.error "Logical or arity value used" -option_map :: (a1 -> a2) -> (Prelude.Maybe a1) -> Prelude.Maybe a2-option_map f x =- case x of {- Prelude.Just x0 -> Prelude.Just (f x0);- Prelude.Nothing -> Prelude.Nothing}- option_choose :: (Prelude.Maybe a1) -> (Prelude.Maybe a1) -> Prelude.Maybe a1 option_choose x y = case x of { Prelude.Just a -> x; Prelude.Nothing -> y} +lebf :: (a1 -> Prelude.Int) -> a1 -> a1 -> Prelude.Bool+lebf f n m =+ (Prelude.<=) (f n) (f m)++type Coq_oddnum = Prelude.Int++odd1 :: Prelude.Int+odd1 =+ (Prelude.succ) 0+ forFold :: a2 -> ([] a1) -> (a2 -> a1 -> a2) -> a2 forFold b v f = Data.List.foldl' f b v -foldl_with_index :: (Prelude.Int -> a2 -> a1 -> a2) -> a2 -> ([] a1) -> a2-foldl_with_index f b v =- let {- go n xs z =- case xs of {- [] -> z;- (:) y ys -> go ((Prelude.succ) n) ys (f n z y)}}- in go 0 v b+span :: (a1 -> Prelude.Bool) -> ([] a1) -> (,) ([] a1) ([] a1)+span p l =+ case l of {+ [] -> (,) [] [];+ (:) x xs ->+ case p x of {+ Prelude.True ->+ case span p xs of {+ (,) ys zs -> (,) ((:) x ys) zs};+ Prelude.False -> (,) [] l}}++insert :: (Ssrbool.Coq_rel a1) -> a1 -> ([] a1) -> [] a1+insert p z l =+ case l of {+ [] -> (:) z [];+ (:) x xs ->+ case p x z of {+ Prelude.True -> (:) x (insert p z xs);+ Prelude.False -> (:) z ((:) x xs)}}++sortBy :: (a1 -> a1 -> Prelude.Bool) -> ([] a1) -> [] a1+sortBy p l =+ case l of {+ [] -> [];+ (:) x xs -> insert p x (sortBy p xs)} dep_foldl_inv :: (a1 -> Eqtype.Equality__Coq_type) -> a1 -> ([] Eqtype.Equality__Coq_sort) -> Prelude.Int -> (a1 -> []
+ LinearScan/List0.hs view
@@ -0,0 +1,13 @@+module LinearScan.List0 where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++
+ LinearScan/LiveSets.hs view
@@ -0,0 +1,134 @@+module LinearScan.LiveSets where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Blocks as Blocks+import qualified LinearScan.IntMap as IntMap+import qualified LinearScan.Lib as Lib+import qualified LinearScan.Seq as Seq+import qualified LinearScan.Ssrnat as Ssrnat+++data BlockLiveSets =+ Build_BlockLiveSets Data.IntSet.IntSet Data.IntSet.IntSet Data.IntSet.IntSet + Data.IntSet.IntSet Blocks.OpId Blocks.OpId++blockLiveGen :: BlockLiveSets -> Data.IntSet.IntSet+blockLiveGen b =+ case b of {+ Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0+ blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveGen0}++blockLiveKill :: BlockLiveSets -> Data.IntSet.IntSet+blockLiveKill b =+ case b of {+ Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0+ blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveKill0}++blockLiveIn :: BlockLiveSets -> Data.IntSet.IntSet+blockLiveIn b =+ case b of {+ Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0+ blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveIn0}++blockLiveOut :: BlockLiveSets -> Data.IntSet.IntSet+blockLiveOut b =+ case b of {+ Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0+ blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLiveOut0}++blockFirstOpId :: BlockLiveSets -> Blocks.OpId+blockFirstOpId b =+ case b of {+ Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0+ blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockFirstOpId0}++blockLastOpId :: BlockLiveSets -> Blocks.OpId+blockLastOpId b =+ case b of {+ Build_BlockLiveSets blockLiveGen0 blockLiveKill0 blockLiveIn0+ blockLiveOut0 blockFirstOpId0 blockLastOpId0 -> blockLastOpId0}++computeLocalLiveSets :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->+ (Blocks.OpInfo a5 a3 a4) -> ([] a1) ->+ Data.IntMap.IntMap BlockLiveSets+computeLocalLiveSets maxReg binfo oinfo blocks =+ Prelude.snd+ (Lib.forFold ((,) ((Prelude.succ) 0) IntMap.emptyIntMap) blocks+ (\acc b ->+ case acc of {+ (,) idx m ->+ case Blocks.blockOps binfo b of {+ (,) p opse ->+ case p of {+ (,) opsb opsm ->+ let {+ liveSet = Build_BlockLiveSets Data.IntSet.empty+ Data.IntSet.empty Data.IntSet.empty Data.IntSet.empty+ ((Prelude.+) idx (Ssrnat.double (Data.List.length opsb))) idx}+ in+ case Lib.forFold ((,) idx liveSet)+ ((Prelude.++) opsb ((Prelude.++) opsm opse)) (\acc0 o ->+ case acc0 of {+ (,) lastIdx liveSet1 -> (,) ((Prelude.succ)+ ((Prelude.succ) lastIdx))+ (Lib.forFold liveSet1 (Blocks.opRefs maxReg oinfo o)+ (\liveSet2 v ->+ case Blocks.varId maxReg v of {+ Prelude.Left p0 -> liveSet2;+ Prelude.Right vid ->+ case Blocks.varKind maxReg v of {+ Blocks.Input ->+ case Prelude.not+ (Data.IntSet.member vid+ (blockLiveKill liveSet2)) of {+ Prelude.True -> Build_BlockLiveSets+ (Data.IntSet.insert vid (blockLiveGen liveSet2))+ (blockLiveKill liveSet2) (blockLiveIn liveSet2)+ (blockLiveOut liveSet2)+ (blockFirstOpId liveSet2) lastIdx;+ Prelude.False -> liveSet2};+ _ -> Build_BlockLiveSets (blockLiveGen liveSet2)+ (Data.IntSet.insert vid (blockLiveKill liveSet2))+ (blockLiveIn liveSet2) (blockLiveOut liveSet2)+ (blockFirstOpId liveSet2) lastIdx}}))}) of {+ (,) lastIdx' liveSet3 -> (,) lastIdx'+ (Data.IntMap.insert (Blocks.blockId binfo b) liveSet3 m)}}}}))++computeGlobalLiveSets :: (Blocks.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 = Blocks.blockId binfo b} in+ case Data.IntMap.lookup bid liveSets1 of {+ Prelude.Just liveSet ->+ let {+ liveSet2 = Lib.forFold liveSet (Blocks.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)+ (Data.IntSet.union (blockLiveOut liveSet1)+ (blockLiveIn sux)) (blockFirstOpId liveSet1)+ (blockLastOpId liveSet1);+ Prelude.Nothing -> liveSet1})}+ in+ Data.IntMap.insert bid (Build_BlockLiveSets (blockLiveGen liveSet2)+ (blockLiveKill liveSet2)+ (Data.IntSet.union+ (Data.IntSet.difference (blockLiveOut liveSet2)+ (blockLiveKill liveSet2)) (blockLiveGen liveSet2))+ (blockLiveOut liveSet2) (blockFirstOpId liveSet2)+ (blockLastOpId liveSet2)) liveSets1;+ Prelude.Nothing -> liveSets1})+
LinearScan/Logic.hs view
@@ -1,8 +1,10 @@ module LinearScan.Logic where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity
LinearScan/Main.hs view
@@ -1,2398 +1,44 @@-{-# OPTIONS_GHC -cpp -fglasgow-exts #-}-{- For Hugs, use the option -F"cpp -P -traditional" -}--module LinearScan.Main 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.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)}+module LinearScan.Main where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Allocate as Allocate+import qualified LinearScan.Assign as Assign+import qualified LinearScan.Blocks as Blocks+import qualified LinearScan.Build as Build+import qualified LinearScan.LiveSets as LiveSets+import qualified LinearScan.Morph as Morph+import qualified LinearScan.Order as Order+import qualified LinearScan.Resolve as Resolve+++linearScan :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) -> (Blocks.OpInfo+ a5 a3 a4) -> ([] a1) -> a5 -> Prelude.Either Morph.SSError+ ((,) ([] a2) a5)+linearScan maxReg binfo oinfo blocks accum =+ let {blocks' = Order.computeBlockOrder blocks} in+ let {liveSets = LiveSets.computeLocalLiveSets maxReg binfo oinfo blocks'}+ in+ let {liveSets' = LiveSets.computeGlobalLiveSets binfo blocks' liveSets} in+ case Build.buildIntervals maxReg binfo oinfo blocks liveSets' of {+ Prelude.Left err -> Prelude.Left err;+ Prelude.Right ssig ->+ case Allocate.walkIntervals maxReg ( ssig) ((Prelude.succ)+ (Blocks.countOps binfo blocks)) of {+ Prelude.Left err -> Prelude.Left err;+ Prelude.Right ssig' ->+ let {+ mappings = Resolve.resolveDataFlow maxReg binfo ( ssig') blocks+ liveSets'}+ in+ Prelude.Right+ (Assign.assignRegNum maxReg binfo oinfo ( ssig') mappings blocks accum)}}
+ LinearScan/Morph.hs view
@@ -0,0 +1,227 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Morph where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.IState as IState+import qualified LinearScan.Logic as Logic+import qualified LinearScan.ScanState as ScanState+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++++--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 PhysReg = Prelude.Int++data SSError =+ ECannotSplitSingleton1 Prelude.Int+ | ECannotSplitSingleton2 Prelude.Int+ | ECannotSplitSingleton3 Prelude.Int+ | ECannotSplitSingleton4 Prelude.Int+ | ECannotSplitSingleton5 Prelude.Int+ | ECannotSplitSingleton6 Prelude.Int+ | ECannotSplitSingleton7 Prelude.Int+ | ENoIntervalsToSplit+ | ERegisterAlreadyAssigned Prelude.Int+ | ERegisterAssignmentsOverlap Prelude.Int+ | EFuelExhausted+ | EUnexpectedNoMoreUnhandled++stbind :: (a4 -> IState.IState SSError a2 a3 a5) -> (IState.IState SSError + a1 a2 a4) -> IState.IState SSError a1 a3 a5+stbind f x =+ IState.ijoin (IState.imap f x)++error_ :: SSError -> IState.IState SSError a1 a2 a3+error_ err x =+ Prelude.Left err++return_ :: a3 -> IState.IState a1 a2 a2 a3+return_ =+ IState.ipure++data SSInfo p =+ Build_SSInfo ScanState.ScanStateDesc p++thisDesc :: Prelude.Int -> ScanState.ScanStateDesc -> (SSInfo a1) ->+ ScanState.ScanStateDesc+thisDesc maxReg startDesc s =+ case s of {+ Build_SSInfo thisDesc0 thisHolds -> thisDesc0}++type SState p q a = IState.IState SSError (SSInfo p) (SSInfo q) a++withScanStatePO :: Prelude.Int -> ScanState.ScanStateDesc ->+ (ScanState.ScanStateDesc -> () -> SState () () a1) ->+ SState () () a1+withScanStatePO maxReg 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 :: Prelude.Int -> ScanState.ScanStateDesc -> (ScanState.ScanStateDesc+ -> SState () () a1) -> SState () () a1+liftLen maxReg 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_ :: Prelude.Int -> ScanState.ScanStateDesc -> SState () () ()+weakenHasLen_ maxReg pre hS =+ Prelude.Right ((,) ()+ (case hS of {+ Build_SSInfo thisDesc0 _ -> Build_SSInfo thisDesc0 __}))++strengthenHasLen :: Prelude.Int -> ScanState.ScanStateDesc ->+ ScanState.ScanStateDesc -> Prelude.Maybe ()+strengthenHasLen maxReg pre sd =+ let {_evar_0_ = \_ -> Prelude.Nothing} in+ let {_evar_0_0 = \_a_ _l_ -> Prelude.Just __} in+ case ScanState.unhandled maxReg sd of {+ [] -> _evar_0_ __;+ (:) x x0 -> _evar_0_0 x x0}++moveUnhandledToActive :: Prelude.Int -> ScanState.ScanStateDesc -> PhysReg ->+ SState () () ()+moveUnhandledToActive maxReg pre reg x =+ case x of {+ Build_SSInfo thisDesc0 _ ->+ case thisDesc0 of {+ ScanState.Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0+ unhandled0 active0 inactive0 handled0 ->+ case unhandled0 of {+ [] -> Logic.coq_False_rect;+ (:) p unhandled1 ->+ let {+ _evar_0_ = \_ -> Prelude.Right ((,) () (Build_SSInfo+ (ScanState.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 :: Prelude.Int -> ScanState.ScanStateDesc ->+ Eqtype.Equality__Coq_sort -> Specif.Coq_sig2+ ScanState.ScanStateDesc+moveActiveToHandled maxReg sd x =+ ScanState.Build_ScanStateDesc (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd) (ScanState.fixedIntervals maxReg sd)+ (ScanState.unhandled maxReg sd)+ (unsafeCoerce+ (Seq.rem+ (Eqtype.prod_eqType+ (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd))+ (Fintype.ordinal_eqType maxReg)) x+ (unsafeCoerce (ScanState.active maxReg sd))))+ (ScanState.inactive maxReg sd) ((:) (unsafeCoerce x)+ (ScanState.handled maxReg sd))++moveActiveToInactive :: Prelude.Int -> ScanState.ScanStateDesc ->+ Eqtype.Equality__Coq_sort -> Specif.Coq_sig2+ ScanState.ScanStateDesc+moveActiveToInactive maxReg sd x =+ ScanState.Build_ScanStateDesc (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd) (ScanState.fixedIntervals maxReg sd)+ (ScanState.unhandled maxReg sd)+ (unsafeCoerce+ (Seq.rem+ (Eqtype.prod_eqType+ (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd))+ (Fintype.ordinal_eqType maxReg)) x+ (unsafeCoerce (ScanState.active maxReg sd)))) ((:) (unsafeCoerce x)+ (ScanState.inactive maxReg sd)) (ScanState.handled maxReg sd)++moveInactiveToActive :: Prelude.Int -> ScanState.ScanStateDesc ->+ Eqtype.Equality__Coq_sort -> Specif.Coq_sig2+ ScanState.ScanStateDesc+moveInactiveToActive maxReg sd x =+ ScanState.Build_ScanStateDesc (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd) (ScanState.fixedIntervals maxReg sd)+ (ScanState.unhandled maxReg sd) ((:) (unsafeCoerce x)+ (ScanState.active maxReg sd))+ (unsafeCoerce+ (Seq.rem+ (Eqtype.prod_eqType+ (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd))+ (Fintype.ordinal_eqType maxReg)) x+ (unsafeCoerce (ScanState.inactive maxReg sd))))+ (ScanState.handled maxReg sd)++moveInactiveToHandled :: Prelude.Int -> ScanState.ScanStateDesc ->+ Eqtype.Equality__Coq_sort -> Specif.Coq_sig2+ ScanState.ScanStateDesc+moveInactiveToHandled maxReg sd x =+ ScanState.Build_ScanStateDesc (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd) (ScanState.fixedIntervals maxReg sd)+ (ScanState.unhandled maxReg sd) (ScanState.active maxReg sd)+ (unsafeCoerce+ (Seq.rem+ (Eqtype.prod_eqType+ (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd))+ (Fintype.ordinal_eqType maxReg)) x+ (unsafeCoerce (ScanState.inactive maxReg sd)))) ((:) (unsafeCoerce x)+ (ScanState.handled maxReg sd))+
LinearScan/NonEmpty0.hs view
@@ -1,11 +1,19 @@ module LinearScan.NonEmpty0 where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity import qualified LinearScan.Utils ++coq_NE_from_list :: a1 -> ([] a1) -> [] a1+coq_NE_from_list x xs =+ case xs of {+ [] -> (:[]) x;+ (:) y ys -> (:) x (coq_NE_from_list y ys)}
+ LinearScan/Order.hs view
@@ -0,0 +1,17 @@+module LinearScan.Order where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils+++computeBlockOrder :: ([] a1) -> [] a1+computeBlockOrder blocks =+ blocks+
LinearScan/Range.hs view
@@ -1,62 +1,43 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}+ module LinearScan.Range where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity import qualified LinearScan.Utils +import qualified LinearScan.Datatypes as Datatypes+import qualified LinearScan.Lib as Lib+import qualified LinearScan.Specif as Specif+import qualified LinearScan.UsePos as UsePos+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Seq as Seq+import qualified LinearScan.Ssrnat as Ssrnat -__ :: any-__ = Prelude.error "Logical or arity value used" -data UsePos =- Build_UsePos Prelude.Int Prelude.Bool -uloc :: UsePos -> Prelude.Int-uloc u =- case u of {- Build_UsePos uloc0 regReq0 -> uloc0}--regReq :: UsePos -> Prelude.Bool-regReq u =- case u of {- Build_UsePos uloc0 regReq0 -> regReq0}--type UsePosSublistsOf =- ((,) (Prelude.Maybe ([] UsePos)) (Prelude.Maybe ([] UsePos)))+--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif -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 = (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 = (Prelude.<=) ((Prelude.succ) (uloc x)) before} in- case b of {- Prelude.True ->- let {u = \_ -> usePosSpan before xs} in- case u __ of {- (,) o x0 ->- case o of {- Prelude.Just l1 ->- case x0 of {- Prelude.Just l2 -> (,) (Prelude.Just ((:) x l1)) (Prelude.Just l2);- Prelude.Nothing -> (,) (Prelude.Just ((:) x l1)) Prelude.Nothing};- Prelude.Nothing ->- case x0 of {- Prelude.Just l2 -> (,) (Prelude.Just ((:[]) x)) (Prelude.Just l2);- Prelude.Nothing -> Prelude.error "absurd case"}}};- Prelude.False -> (,) Prelude.Nothing (Prelude.Just ((:) x xs))})- l+__ :: any+__ = Prelude.error "Logical or arity value used" data RangeDesc =- Build_RangeDesc Prelude.Int Prelude.Int ([] UsePos)+ Build_RangeDesc Prelude.Int Prelude.Int ([] UsePos.UsePos) rbeg :: RangeDesc -> Prelude.Int rbeg r =@@ -68,88 +49,210 @@ case r of { Build_RangeDesc rbeg0 rend0 ups0 -> rend0} -ups :: RangeDesc -> [] UsePos+ups :: RangeDesc -> [] UsePos.UsePos ups r = case r of { Build_RangeDesc rbeg0 rend0 ups0 -> ups0} +getRangeDesc :: RangeDesc -> RangeDesc+getRangeDesc d =+ d++packRange :: RangeDesc -> RangeDesc+packRange d =+ d++newRange :: UsePos.UsePos -> RangeDesc+newRange upos =+ Build_RangeDesc (UsePos.uloc upos) ((Prelude.succ) (UsePos.uloc upos)) ((:)+ upos [])++coq_Range_cons :: UsePos.UsePos -> RangeDesc -> RangeDesc+coq_Range_cons upos rd =+ Build_RangeDesc (rbeg rd) (rend rd) ((:) upos (ups rd))++type BoundedRange = RangeDesc++emptyBoundedRange :: Prelude.Int -> Prelude.Int -> BoundedRange+emptyBoundedRange b e =+ Build_RangeDesc b e []++type SortedRanges = Specif.Coq_sig2 ([] RangeDesc)++emptySortedRanges :: Prelude.Int -> SortedRanges+emptySortedRanges b =+ []++prependRange :: Prelude.Int -> Prelude.Int -> BoundedRange -> SortedRanges ->+ Prelude.Int -> SortedRanges+prependRange b e rp ranges pos =+ let {_evar_0_ = \_ _ -> (:) rp []} in+ let {+ _evar_0_0 = \x xs ->+ let {+ _evar_0_0 = \_ _ ->+ let {+ r' = packRange (Build_RangeDesc (rbeg (getRangeDesc ( rp)))+ (rend (getRangeDesc ( x)))+ ((Prelude.++) (ups (getRangeDesc ( rp)))+ (ups (getRangeDesc ( x)))))}+ in+ (:) r' xs}+ in+ let {_evar_0_1 = \_ _ -> (:) rp ((:) x xs)} in+ case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (rend ( rp)))+ (unsafeCoerce (rbeg ( x))) of {+ Prelude.True -> _evar_0_0 __ __;+ Prelude.False -> _evar_0_1 __ __}}+ in+ case ranges of {+ [] -> _evar_0_ __ __;+ (:) x x0 -> _evar_0_0 x x0}++coq_SortedRanges_cat :: Prelude.Int -> SortedRanges -> Prelude.Int ->+ SortedRanges -> SortedRanges+coq_SortedRanges_cat b xs pos ys =+ let {+ _evar_0_ = \_ _ _ ->+ let {_evar_0_ = \_ _ _ -> []} in+ let {_evar_0_0 = \r rs -> (:) r rs} in+ case ys of {+ [] -> _evar_0_ __ __ __;+ (:) x x0 -> _evar_0_0 x x0}}+ in+ let {+ _evar_0_0 = \ps p ->+ let {_evar_0_0 = \_ _ _ -> Seq.rcons ps p} in+ let {+ _evar_0_1 = \r rs ->+ let {+ _evar_0_1 = \_ ->+ let {+ r' = packRange (Build_RangeDesc (rbeg (getRangeDesc ( p)))+ (rend (getRangeDesc ( r)))+ ((Prelude.++) (ups (getRangeDesc ( p)))+ (ups (getRangeDesc ( r)))))}+ in+ (Prelude.++) ps ((:) r' rs)}+ in+ let {_evar_0_2 = \_ -> (Prelude.++) (Seq.rcons ps p) ((:) r rs)} in+ case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (rend ( p)))+ (unsafeCoerce (rbeg ( r))) of {+ Prelude.True -> _evar_0_1 __;+ Prelude.False -> _evar_0_2 __}}+ in+ case ys of {+ [] -> _evar_0_0 __ __ __;+ (:) x x0 -> _evar_0_1 x x0}}+ in+ case Seq.lastP xs of {+ Seq.LastNil -> _evar_0_ __ __ __;+ Seq.LastRcons x x0 -> _evar_0_0 x x0}++transportSortedRanges :: Prelude.Int -> Prelude.Int -> SortedRanges ->+ SortedRanges+transportSortedRanges b pos rp =+ rp+ rangesIntersect :: RangeDesc -> RangeDesc -> Prelude.Bool rangesIntersect x y = case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of { Prelude.True -> (Prelude.<=) ((Prelude.succ) (rbeg y)) (rend x); Prelude.False -> (Prelude.<=) ((Prelude.succ) (rbeg x)) (rend y)} -rangeIntersectionPoint :: RangeDesc -> RangeDesc -> Prelude.Maybe Prelude.Int+rangeIntersectionPoint :: RangeDesc -> RangeDesc -> Prelude.Maybe+ Lib.Coq_oddnum rangeIntersectionPoint x y = case rangesIntersect x y of {- Prelude.True -> Prelude.Just (Prelude.min (rbeg x) (rbeg y));+ Prelude.True -> Prelude.Just+ (case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of {+ Prelude.True -> rbeg x;+ Prelude.False -> rbeg y}); Prelude.False -> Prelude.Nothing} -findRangeUsePos :: RangeDesc -> (UsePos -> Prelude.Bool) -> Prelude.Maybe- UsePos-findRangeUsePos r f =+findRangeUsePos :: RangeDesc -> (UsePos.UsePos -> Prelude.Bool) ->+ Prelude.Maybe UsePos.UsePos+findRangeUsePos rd f =+ let {_evar_0_ = Prelude.Nothing} in let {- go xs =- (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)- (\x ->- case f x of {- Prelude.True -> Prelude.Just x;- Prelude.False -> Prelude.Nothing})- (\x xs0 ->- case f x of {- Prelude.True -> Prelude.Just x;- Prelude.False -> go xs0})- xs}- in go (ups r)--makeDividedRange :: RangeDesc -> Prelude.Int -> ([] UsePos) -> ([] UsePos) ->- ((,) (Prelude.Maybe RangeDesc) (Prelude.Maybe RangeDesc))-makeDividedRange rd before l1 l2 =- case rd of {- Build_RangeDesc rbeg0 rend0 ups0 ->- (\_ -> (,) (Prelude.Just (Build_RangeDesc rbeg0 before l1))- (Prelude.Just (Build_RangeDesc (uloc (Prelude.head l2)) rend0 l2))) __}+ _evar_0_0 = \u us iHxs ->+ let {_evar_0_0 = Prelude.Just u} in+ let {+ _evar_0_1 = let {+ _evar_0_1 = \_top_assumption_ -> Prelude.Just+ _top_assumption_}+ in+ let {_evar_0_2 = Prelude.Nothing} in+ case iHxs of {+ Prelude.Just x -> _evar_0_1 x;+ Prelude.Nothing -> _evar_0_2}}+ in+ case f u of {+ Prelude.True -> _evar_0_0;+ Prelude.False -> _evar_0_1}}+ in+ Datatypes.list_rec _evar_0_ _evar_0_0 (ups (getRangeDesc rd)) rangeSpan :: Prelude.Int -> RangeDesc -> ((,) (Prelude.Maybe RangeDesc) (Prelude.Maybe RangeDesc)) rangeSpan before rd =- 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 ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ case rd of {+ Build_RangeDesc rbeg0 rend0 ups0 -> let {- _evar_0_0 = \o2 ->+ _evar_0_ = \l1 l2 -> let {- rd' = Build_RangeDesc (Prelude.max before (rbeg rd)) (rend rd)- (ups rd)}+ _evar_0_ = \_ ->+ let {+ _evar_0_ = \_ -> (,) Prelude.Nothing (Prelude.Just+ (packRange (Build_RangeDesc rbeg0 rend0 ((Prelude.++) l1 l2))))}+ in+ let {+ _evar_0_0 = \_ ->+ let {+ _evar_0_0 = \_ -> (,) (Prelude.Just+ (packRange (Build_RangeDesc rbeg0 rend0 ((Prelude.++) l1 l2))))+ Prelude.Nothing}+ in+ let {+ _evar_0_1 = \_ ->+ let {+ _evar_0_1 = \_ ->+ let {+ _evar_0_1 = \_ ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ let {+ _evar_0_1 = \_ _ _ _ -> (,) (Prelude.Just+ (packRange (Build_RangeDesc rbeg0 before l1)))+ Prelude.Nothing}+ in+ let {+ _evar_0_2 = \u us ->+ (Prelude.flip (Prelude.$)) __ (\_ -> (,) (Prelude.Just+ (packRange (Build_RangeDesc rbeg0 before l1)))+ (Prelude.Just+ (packRange (Build_RangeDesc (UsePos.uloc u) rend0+ ((:) u us)))))}+ in+ case l2 of {+ [] -> _evar_0_1 __ __ __ __;+ (:) x x0 -> _evar_0_2 x x0})}+ in+ _evar_0_1 __}+ in+ _evar_0_1 __}+ in+ case (Prelude.<=) rend0 before of {+ Prelude.True -> _evar_0_0 __;+ Prelude.False -> _evar_0_1 __}}+ in+ case (Prelude.<=) before rbeg0 of {+ Prelude.True -> _evar_0_ __;+ Prelude.False -> _evar_0_0 __}} in- (,) Prelude.Nothing (Prelude.Just rd')}+ _evar_0_ __} 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 __}+ case Lib.span (\x ->+ (Prelude.<=) ((Prelude.succ) (UsePos.uloc x)) before) ups0 of {+ (,) x x0 -> _evar_0_ x x0}})
+ LinearScan/Resolve.hs view
@@ -0,0 +1,136 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Resolve where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Blocks as Blocks+import qualified LinearScan.Graph as Graph+import qualified LinearScan.IntMap as IntMap+import qualified LinearScan.Lib as Lib+import qualified LinearScan.LiveSets as LiveSets+import qualified LinearScan.ScanState as ScanState+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Fintype as Fintype+import qualified LinearScan.Ssrnat as Ssrnat++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++__ :: any+__ = Prelude.error "Logical or arity value used"++checkIntervalBoundary :: Prelude.Int -> ScanState.ScanStateDesc ->+ Prelude.Int -> Prelude.Bool ->+ LiveSets.BlockLiveSets -> LiveSets.BlockLiveSets ->+ (Data.IntMap.IntMap ((,) Graph.Graph Graph.Graph))+ -> Prelude.Int -> Data.IntMap.IntMap+ ((,) Graph.Graph Graph.Graph)+checkIntervalBoundary maxReg sd bid in_from from to mappings vid =+ let {+ mfrom_int = ScanState.lookupInterval maxReg sd __ vid+ (LiveSets.blockLastOpId from)}+ in+ let {+ mto_int = ScanState.lookupInterval maxReg sd __ vid+ (LiveSets.blockFirstOpId to)}+ in+ case Eqtype.eq_op+ (Eqtype.option_eqType+ (Fintype.ordinal_eqType (ScanState.nextInterval maxReg sd)))+ (unsafeCoerce mfrom_int) (unsafeCoerce mto_int) of {+ Prelude.True -> mappings;+ Prelude.False ->+ let {+ f = \mi ->+ case mi of {+ Prelude.Just i ->+ case ScanState.lookupRegister maxReg sd __ i of {+ Prelude.Just r -> Prelude.Left r;+ Prelude.Nothing -> Prelude.Right vid};+ Prelude.Nothing -> Prelude.Right vid}}+ in+ let {sreg = unsafeCoerce f mfrom_int} in+ let {dreg = unsafeCoerce f mto_int} in+ case Eqtype.eq_op+ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)+ Ssrnat.nat_eqType) sreg dreg of {+ Prelude.True -> mappings;+ Prelude.False ->+ let {+ addToGraphs = \e xs ->+ case xs of {+ (,) gbeg gend ->+ case in_from of {+ Prelude.True -> (,) gbeg+ (Graph.addEdge+ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)+ Ssrnat.nat_eqType) e gend);+ Prelude.False -> (,)+ (Graph.addEdge+ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)+ Ssrnat.nat_eqType) e gbeg) gend}}}+ in+ let {+ f0 = \mxs ->+ let {e = (,) (Prelude.Just sreg) (Prelude.Just dreg)} in+ Prelude.Just+ (unsafeCoerce addToGraphs e+ (case mxs of {+ Prelude.Just xs -> xs;+ Prelude.Nothing -> (,)+ (Graph.emptyGraph+ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)+ Ssrnat.nat_eqType))+ (Graph.emptyGraph+ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)+ Ssrnat.nat_eqType))}))}+ in+ Data.IntMap.alter f0 bid mappings}}++type BlockMoves = (,) Graph.Graph Graph.Graph++resolveDataFlow :: Prelude.Int -> (Blocks.BlockInfo a1 a2 a3 a4) ->+ ScanState.ScanStateDesc -> ([] a1) -> (Data.IntMap.IntMap+ LiveSets.BlockLiveSets) -> Data.IntMap.IntMap BlockMoves+resolveDataFlow maxReg binfo sd blocks liveSets =+ Lib.forFold IntMap.emptyIntMap blocks (\mappings b ->+ let {bid = Blocks.blockId binfo b} in+ case Data.IntMap.lookup bid liveSets of {+ Prelude.Just from ->+ let {successors = Blocks.blockSuccessors binfo b} in+ let {+ in_from = (Prelude.<=) (Data.List.length successors) ((Prelude.succ)+ 0)}+ in+ Lib.forFold mappings successors (\ms s_bid ->+ case Data.IntMap.lookup s_bid liveSets of {+ Prelude.Just to ->+ let {+ key = case in_from of {+ Prelude.True -> bid;+ Prelude.False -> s_bid}}+ in+ IntMap.coq_IntSet_forFold ms (LiveSets.blockLiveIn to)+ (checkIntervalBoundary maxReg sd key in_from from to);+ Prelude.Nothing -> ms});+ Prelude.Nothing -> mappings})+
+ LinearScan/ScanState.hs view
@@ -0,0 +1,158 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.ScanState where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Interval as Interval+import qualified LinearScan.Lib as Lib+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Fintype as Fintype+import qualified LinearScan.Ssrnat as Ssrnat++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++type PhysReg = Prelude.Int++type FixedIntervalsType = [] (Prelude.Maybe Interval.IntervalDesc)++data ScanStateDesc =+ Build_ScanStateDesc Prelude.Int ([] Interval.IntervalDesc) FixedIntervalsType + ([] ((,) Prelude.Int Prelude.Int)) ([] ((,) Prelude.Int PhysReg)) ([]+ ((,)+ Prelude.Int+ PhysReg)) + ([] ((,) Prelude.Int PhysReg))++nextInterval :: Prelude.Int -> ScanStateDesc -> Prelude.Int+nextInterval maxReg s =+ case s of {+ Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0 unhandled0+ active0 inactive0 handled0 -> nextInterval0}++type IntervalId = Prelude.Int++intervals :: Prelude.Int -> ScanStateDesc -> [] Interval.IntervalDesc+intervals maxReg s =+ case s of {+ Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0 unhandled0+ active0 inactive0 handled0 -> intervals0}++fixedIntervals :: Prelude.Int -> ScanStateDesc -> FixedIntervalsType+fixedIntervals maxReg s =+ case s of {+ Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0 unhandled0+ active0 inactive0 handled0 -> fixedIntervals0}++unhandled :: Prelude.Int -> ScanStateDesc -> [] ((,) IntervalId Prelude.Int)+unhandled maxReg s =+ case s of {+ Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0 unhandled0+ active0 inactive0 handled0 -> unhandled0}++active :: Prelude.Int -> ScanStateDesc -> [] ((,) IntervalId PhysReg)+active maxReg s =+ case s of {+ Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0 unhandled0+ active0 inactive0 handled0 -> active0}++inactive :: Prelude.Int -> ScanStateDesc -> [] ((,) IntervalId PhysReg)+inactive maxReg s =+ case s of {+ Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0 unhandled0+ active0 inactive0 handled0 -> inactive0}++handled :: Prelude.Int -> ScanStateDesc -> [] ((,) IntervalId PhysReg)+handled maxReg s =+ case s of {+ Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0 unhandled0+ active0 inactive0 handled0 -> handled0}++registerWithHighestPos :: Prelude.Int -> ([] (Prelude.Maybe Lib.Coq_oddnum))+ -> (,) Prelude.Int (Prelude.Maybe Lib.Coq_oddnum)+registerWithHighestPos maxReg =+ (LinearScan.Utils.vfoldl'_with_index) maxReg (\reg res x ->+ case res of {+ (,) r o ->+ case o of {+ Prelude.Just n ->+ case x of {+ Prelude.Just m ->+ case (Prelude.<=) ((Prelude.succ) ( n)) ( m) of {+ Prelude.True -> (,) reg (Prelude.Just m);+ Prelude.False -> (,) r (Prelude.Just n)};+ Prelude.Nothing -> (,) reg Prelude.Nothing};+ Prelude.Nothing -> (,) r Prelude.Nothing}}) ((,) ( 0) (Prelude.Just+ Lib.odd1))++isWithin :: Interval.IntervalDesc -> Prelude.Int -> Prelude.Int ->+ Prelude.Bool+isWithin int vid opid =+ (Prelude.&&)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Interval.ivar int))+ (unsafeCoerce vid))+ ((Prelude.&&) ((Prelude.<=) (Interval.ibeg int) opid)+ ((Prelude.<=) ((Prelude.succ) opid) (Interval.iend int)))++lookupInterval :: Prelude.Int -> ScanStateDesc -> a1 -> Prelude.Int ->+ Prelude.Int -> Prelude.Maybe IntervalId+lookupInterval maxReg sd st vid opid =+ let {+ f = \idx acc int ->+ case acc of {+ Prelude.Just x -> Prelude.Just x;+ Prelude.Nothing ->+ case isWithin ( int) vid opid of {+ Prelude.True -> Prelude.Just idx;+ Prelude.False -> Prelude.Nothing}}}+ in+ (LinearScan.Utils.vfoldl'_with_index) (nextInterval maxReg sd) f+ Prelude.Nothing (intervals maxReg sd)++lookupRegister :: Prelude.Int -> ScanStateDesc -> a1 ->+ Eqtype.Equality__Coq_sort -> Prelude.Maybe PhysReg+lookupRegister maxReg sd st intid =+ Lib.forFold Prelude.Nothing+ ((Prelude.++) (unsafeCoerce (handled maxReg sd))+ ((Prelude.++) (unsafeCoerce (active maxReg sd))+ (unsafeCoerce (inactive maxReg sd)))) (\acc x ->+ case x of {+ (,) xid reg ->+ case acc of {+ Prelude.Just r -> Prelude.Just r;+ Prelude.Nothing ->+ case Eqtype.eq_op (Fintype.ordinal_eqType (nextInterval maxReg sd))+ xid intid of {+ Prelude.True -> Prelude.Just reg;+ Prelude.False -> Prelude.Nothing}}})++data ScanStateStatus =+ Pending+ | InUse++type ScanStateSig = ScanStateDesc++packScanState :: Prelude.Int -> ScanStateStatus -> ScanStateDesc ->+ ScanStateDesc+packScanState maxReg b sd =+ sd+
LinearScan/Seq.hs view
@@ -4,8 +4,10 @@ module LinearScan.Seq where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity@@ -13,6 +15,7 @@ import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Ssrbool as Ssrbool+import qualified LinearScan.Ssrfun as Ssrfun import qualified LinearScan.Ssrnat as Ssrnat @@ -27,13 +30,16 @@ unsafeCoerce = IOExts.unsafeCoerce #endif -ncons :: Prelude.Int -> a1 -> ([] a1) -> [] a1-ncons n x =- Ssrnat.iter n (\x0 -> (:) x x0)+nilp :: ([] a1) -> Prelude.Bool+nilp s =+ Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Data.List.length s))+ (unsafeCoerce 0) -nseq :: Prelude.Int -> a1 -> [] a1-nseq n x =- ncons n x []+rcons :: ([] a1) -> a1 -> [] a1+rcons s z =+ case s of {+ [] -> (:) z [];+ (:) x s' -> (:) x (rcons s' z)} last :: a1 -> ([] a1) -> a1 last x s =@@ -47,29 +53,29 @@ [] -> []; (:) x' s' -> (:) x (belast x' s')} -nth :: a1 -> ([] a1) -> Prelude.Int -> a1-nth x0 s n =+data Coq_last_spec t =+ LastNil+ | LastRcons ([] t) t++lastP :: ([] a1) -> Coq_last_spec a1+lastP s =+ let {_evar_0_ = LastNil} in+ let {+ _evar_0_0 = \x s0 ->+ let {_evar_0_0 = LastRcons (belast x s0) (last x s0)} in _evar_0_0}+ in case s of {- [] -> x0;- (:) x s' ->- (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))- (\_ ->- x)- (\n' ->- nth x0 s' n')- n}+ [] -> _evar_0_;+ (:) x x0 -> _evar_0_0 x x0} -set_nth :: a1 -> ([] a1) -> Prelude.Int -> a1 -> [] a1-set_nth x0 s n y =+find :: (Ssrbool.Coq_pred a1) -> ([] a1) -> Prelude.Int+find a s = case s of {- [] -> ncons n x0 ((:) y []);+ [] -> 0; (:) x s' ->- (\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}+ case a x of {+ Prelude.True -> 0;+ Prelude.False -> (Prelude.succ) (find a s')}} count :: (Ssrbool.Coq_pred a1) -> ([] a1) -> Prelude.Int count a s =@@ -107,16 +113,6 @@ 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 rem t x s =@@ -126,4 +122,20 @@ case Eqtype.eq_op t y x of { Prelude.True -> t0; Prelude.False -> (:) y (rem t x t0)}}++pmap :: (a1 -> Prelude.Maybe a2) -> ([] a1) -> [] a2+pmap f s =+ case s of {+ [] -> [];+ (:) x s' ->+ let {r = pmap f s'} in Ssrfun._Option__apply (\x0 -> (:) x0 r) r (f x)}++iota :: Prelude.Int -> Prelude.Int -> [] Prelude.Int+iota m n =+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ ->+ [])+ (\n' -> (:) m+ (iota ((Prelude.succ) m) n'))+ n
LinearScan/Specif.hs view
@@ -1,8 +1,10 @@ module LinearScan.Specif where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity
+ LinearScan/Split.hs view
@@ -0,0 +1,426 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Split where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Datatypes as Datatypes+import qualified LinearScan.Interval as Interval+import qualified LinearScan.Lib as Lib+import qualified LinearScan.Logic as Logic+import qualified LinearScan.Morph as Morph+import qualified LinearScan.ScanState as ScanState+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Fintype as Fintype+import qualified LinearScan.Seq as Seq+import qualified LinearScan.Ssrbool as Ssrbool++++--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 PhysReg = Prelude.Int++data SplitPosition =+ BeforePos Lib.Coq_oddnum+ | BeforeFirstUsePosReqReg+ | EndOfLifetimeHole++splitPosition :: Interval.IntervalDesc -> SplitPosition -> Prelude.Maybe+ Lib.Coq_oddnum+splitPosition d pos =+ case pos of {+ BeforePos x -> Prelude.Just x;+ BeforeFirstUsePosReqReg ->+ Interval.firstUseReqReg (Interval.getIntervalDesc d);+ EndOfLifetimeHole -> Prelude.Nothing}++splitInterval :: Prelude.Int -> ScanState.ScanStateDesc ->+ ScanState.IntervalId -> SplitPosition -> Prelude.Bool ->+ Prelude.Either Morph.SSError+ (Prelude.Maybe ScanState.ScanStateSig)+splitInterval maxReg sd uid pos forCurrent =+ let {+ _evar_0_ = \_nextInterval_ ints _fixedIntervals_ unh _active_ _inactive_ _handled_ uid0 ->+ let {+ _evar_0_ = \uid1 -> Prelude.Left (Morph.ECannotSplitSingleton1 ( uid1))}+ in+ let {+ _evar_0_0 = \_top_assumption_ ->+ let {+ _evar_0_0 = \u beg us uid1 ->+ let {int = LinearScan.Utils.nth _nextInterval_ ints uid1} in+ let {+ _evar_0_0 = \_top_assumption_0 ->+ let {+ _evar_0_0 = \_ ->+ (Prelude.flip (Prelude.$)) __ (\_ ->+ let {+ _evar_0_0 = \iv ib ie _iknd_ rds ->+ let {+ _top_assumption_1 = Interval.intervalSpan rds+ _top_assumption_0 iv ib ie _iknd_}+ in+ let {+ _evar_0_0 = \_top_assumption_2 ->+ let {+ _evar_0_0 = \_top_assumption_3 _top_assumption_4 ->+ let {+ _evar_0_0 = \_top_assumption_5 ->+ let {+ _evar_0_0 = \_ ->+ let {+ _evar_0_0 = \_ ->+ let {+ _evar_0_0 = \_ ->+ (Prelude.flip (Prelude.$)) __+ (let {+ new_unhandled = ScanState.Build_ScanStateDesc+ ((Prelude.succ) _nextInterval_)+ (LinearScan.Utils.snoc _nextInterval_+ (LinearScan.Utils.set_nth _nextInterval_+ ints uid1 _top_assumption_3)+ _top_assumption_5) _fixedIntervals_+ (Lib.insert (Lib.lebf Prelude.snd) ((,)+ ( _nextInterval_)+ (Interval.ibeg _top_assumption_5)) ((:)+ (Prelude.id ((,) u beg))+ (Prelude.map Prelude.id us)))+ (Prelude.map Prelude.id _active_)+ (Prelude.map Prelude.id _inactive_)+ (Prelude.map Prelude.id _handled_)}+ in+ \_ -> Prelude.Right (Prelude.Just+ (ScanState.packScanState maxReg+ ScanState.InUse new_unhandled)))}+ in+ _evar_0_0 __}+ in+ _evar_0_0 __}+ in+ let {+ _evar_0_1 = \_ -> Prelude.Left+ (Morph.ECannotSplitSingleton3 ( uid1))}+ in+ case (Prelude.<=) ((Prelude.succ) beg)+ (Interval.ibeg _top_assumption_5) of {+ Prelude.True -> _evar_0_0 __;+ Prelude.False -> _evar_0_1 __}}+ in+ let {+ _evar_0_1 = \_ ->+ let {+ _evar_0_1 = Prelude.Left (Morph.ECannotSplitSingleton4+ ( uid1))}+ in+ let {+ _evar_0_2 = let {+ _evar_0_2 = \_ ->+ let {+ _evar_0_2 = \_ ->+ let {+ set_int_desc = ScanState.Build_ScanStateDesc+ _nextInterval_+ (LinearScan.Utils.set_nth+ _nextInterval_ ints uid1+ _top_assumption_3)+ _fixedIntervals_ ((:) ((,) u beg)+ us) _active_ _inactive_ _handled_}+ in+ Prelude.Right (Prelude.Just+ (ScanState.packScanState maxReg+ ScanState.InUse set_int_desc))}+ in+ _evar_0_2 __}+ in+ _evar_0_2 __}+ in+ case forCurrent of {+ Prelude.True -> _evar_0_1;+ Prelude.False -> _evar_0_2}}+ in+ case _top_assumption_4 of {+ Prelude.Just x -> (\_ -> _evar_0_0 x);+ Prelude.Nothing -> _evar_0_1}}+ in+ let {+ _evar_0_1 = \_top_assumption_3 ->+ let {+ _evar_0_1 = \_top_assumption_4 ->+ let {+ _evar_0_1 = \_ ->+ (Prelude.flip (Prelude.$)) __+ (let {+ new_unhandled = ScanState.Build_ScanStateDesc+ ((Prelude.succ) _nextInterval_)+ (LinearScan.Utils.snoc _nextInterval_ ints+ _top_assumption_4) _fixedIntervals_+ (Lib.insert (Lib.lebf Prelude.snd) ((,)+ ( _nextInterval_)+ (Interval.ibeg _top_assumption_4)) ((:)+ (Prelude.id ((,) u beg))+ (Prelude.map Prelude.id us)))+ (Prelude.map Prelude.id _active_)+ (Prelude.map Prelude.id _inactive_)+ (Prelude.map Prelude.id _handled_)}+ in+ \_ -> Prelude.Right (Prelude.Just+ (ScanState.packScanState maxReg ScanState.InUse+ new_unhandled)))}+ in+ let {+ _evar_0_2 = \_ -> Prelude.Left+ (Morph.ECannotSplitSingleton5 ( uid1))}+ in+ case (Prelude.<=) ((Prelude.succ) beg)+ (Interval.ibeg _top_assumption_4) of {+ Prelude.True -> _evar_0_1 __;+ Prelude.False -> _evar_0_2 __}}+ in+ let {_evar_0_2 = \_ -> Logic.coq_False_rect} in+ case _top_assumption_3 of {+ Prelude.Just x -> (\_ -> _evar_0_1 x);+ Prelude.Nothing -> _evar_0_2}}+ in+ case _top_assumption_2 of {+ Prelude.Just x -> _evar_0_0 x;+ Prelude.Nothing -> _evar_0_1}}+ in+ case _top_assumption_1 of {+ (,) x x0 -> _evar_0_0 x x0 __}}+ in+ case int of {+ Interval.Build_IntervalDesc x x0 x1 x2 x3 ->+ _evar_0_0 x x0 x1 x2 x3})}+ in+ let {+ _evar_0_1 = \_ -> Prelude.Left (Morph.ECannotSplitSingleton2+ ( uid1))}+ in+ case (Prelude.&&)+ ((Prelude.<=) ((Prelude.succ) (Interval.ibeg ( int)))+ _top_assumption_0)+ ((Prelude.<=) ((Prelude.succ) _top_assumption_0)+ (Interval.iend ( int))) of {+ Prelude.True -> _evar_0_0 __;+ Prelude.False -> _evar_0_1 __}}+ in+ let {_evar_0_1 = Prelude.Right Prelude.Nothing} in+ case splitPosition ( int) pos of {+ Prelude.Just x -> _evar_0_0 x;+ Prelude.Nothing -> _evar_0_1}}+ in+ (\us _ uid1 ->+ case _top_assumption_ of {+ (,) x x0 -> _evar_0_0 x x0 us uid1})}+ in+ case unh of {+ [] -> _evar_0_ uid0;+ (:) x x0 -> _evar_0_0 x x0 __ uid0}}+ in+ case sd of {+ ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->+ _evar_0_ x x0 x1 x2 x3 x4 x5 uid}++splitCurrentInterval :: Prelude.Int -> ScanState.ScanStateDesc ->+ SplitPosition -> Morph.SState () () ()+splitCurrentInterval maxReg 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 = ScanState.Build_ScanStateDesc _nextInterval_ intervals0+ _fixedIntervals_ ((:) ((,) uid beg) us) _active_ _inactive_+ _handled_}+ in+ (\_ _ _ _ ->+ let {+ _top_assumption_0 = splitInterval maxReg desc0 uid pos+ Prelude.True}+ in+ let {_evar_0_0 = \err -> Prelude.Left err} in+ let {+ _evar_0_1 = \_top_assumption_1 ->+ let {+ _evar_0_1 = \_top_assumption_2 -> Prelude.Right ((,) ()+ (Morph.Build_SSInfo _top_assumption_2 __))}+ in+ let {+ _evar_0_2 = Prelude.Left (Morph.ECannotSplitSingleton6 ( 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 {+ ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->+ _evar_0_ x x0 x1 x2 x3 x4 x5 __ __ __}}+ in+ case ssi of {+ Morph.Build_SSInfo x x0 -> _evar_0_ x __}++splitAssignedIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->+ PhysReg -> SplitPosition -> Prelude.Bool ->+ Morph.SState () () ()+splitAssignedIntervalForReg maxReg pre reg pos trueForActives ssi =+ let {+ _evar_0_ = \desc ->+ let {+ intlist = case trueForActives of {+ Prelude.True -> ScanState.active maxReg desc;+ Prelude.False -> ScanState.inactive maxReg desc}}+ in+ (Prelude.flip (Prelude.$)) __ (\_ ->+ let {+ intids = Prelude.map (\i -> Prelude.fst i)+ (Prelude.filter (\i ->+ Eqtype.eq_op (Fintype.ordinal_eqType maxReg)+ (Prelude.snd (unsafeCoerce i)) (unsafeCoerce reg))+ intlist)}+ in+ (Prelude.flip (Prelude.$)) __ (\_ ->+ let {+ _evar_0_ = \_nextInterval_ intervals0 _fixedIntervals_ _unhandled_ active0 inactive0 _handled_ intlist0 intids0 ->+ let {+ desc0 = ScanState.Build_ScanStateDesc _nextInterval_ intervals0+ _fixedIntervals_ _unhandled_ active0 inactive0 _handled_}+ in+ (\_ _ _ _ ->+ let {_evar_0_ = \_ -> Prelude.Left Morph.ENoIntervalsToSplit} in+ let {+ _evar_0_0 = \aid aids iHaids ->+ let {+ _top_assumption_ = splitInterval maxReg desc0 aid pos+ Prelude.False}+ in+ let {_evar_0_0 = \err -> Prelude.Left err} in+ 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 = ScanState.Build_ScanStateDesc+ (ScanState.nextInterval maxReg _top_assumption_1)+ (ScanState.intervals maxReg _top_assumption_1)+ (ScanState.fixedIntervals maxReg _top_assumption_1)+ (ScanState.unhandled maxReg _top_assumption_1)+ (unsafeCoerce+ (Seq.rem+ (Eqtype.prod_eqType+ (Fintype.ordinal_eqType+ (ScanState.nextInterval maxReg+ _top_assumption_1))+ (Fintype.ordinal_eqType maxReg))+ (unsafeCoerce ((,) ( aid) reg))+ (unsafeCoerce+ (ScanState.active maxReg _top_assumption_1))))+ ((:) ((,) ( aid) reg)+ (ScanState.inactive maxReg _top_assumption_1))+ (ScanState.handled maxReg _top_assumption_1)}+ in+ \_ -> Morph.Build_SSInfo act_to_inact __)}+ in+ let {+ _evar_0_2 = \_ -> Morph.Build_SSInfo _top_assumption_1 __}+ in+ case Ssrbool.in_mem (unsafeCoerce ((,) ( aid) reg))+ (Ssrbool.mem+ (Seq.seq_predType+ (Eqtype.prod_eqType+ (Fintype.ordinal_eqType+ (ScanState.nextInterval maxReg+ _top_assumption_1))+ (Fintype.ordinal_eqType maxReg)))+ (unsafeCoerce+ (ScanState.active maxReg _top_assumption_1))) of {+ Prelude.True -> _evar_0_1 __;+ Prelude.False -> _evar_0_2 __}))}+ in+ let {+ _evar_0_2 = Prelude.Left (Morph.ECannotSplitSingleton7+ ( 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 {+ ScanState.Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->+ _evar_0_ x x0 x1 x2 x3 x4 x5 intlist intids})) __ __ __}+ in+ case ssi of {+ Morph.Build_SSInfo x x0 -> _evar_0_ x __}++splitActiveIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->+ PhysReg -> Lib.Coq_oddnum -> Morph.SState + () () ()+splitActiveIntervalForReg maxReg pre reg pos =+ splitAssignedIntervalForReg maxReg pre reg (BeforePos pos) Prelude.True++splitAnyInactiveIntervalForReg :: Prelude.Int -> ScanState.ScanStateDesc ->+ PhysReg -> Morph.SState () () ()+splitAnyInactiveIntervalForReg maxReg pre reg ss =+ (Prelude.flip (Prelude.$)) (\s ->+ splitAssignedIntervalForReg maxReg s reg 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})+
LinearScan/Ssrbool.hs view
@@ -4,8 +4,10 @@ module LinearScan.Ssrbool where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity@@ -63,6 +65,16 @@ type Coq_rel t = t -> Coq_pred t +type Coq_simpl_pred t = (->) t Prelude.Bool++coq_SimplPred :: (Coq_pred a1) -> Coq_simpl_pred a1+coq_SimplPred p =+ p++pred_of_simpl :: (Coq_simpl_pred a1) -> Coq_pred a1+pred_of_simpl p =+ (Prelude.$) p+ type Coq_simpl_rel t = (->) t (Coq_pred t) rel_of_simpl_rel :: (Coq_simpl_rel a1) -> Coq_rel a1@@ -94,4 +106,8 @@ in_mem :: a1 -> (Coq_mem_pred a1) -> Prelude.Bool in_mem x mp = unsafeCoerce (\_ -> pred_of_mem) __ mp x++pred_of_mem_pred :: (Coq_mem_pred a1) -> Coq_simpl_pred a1+pred_of_mem_pred mp =+ coq_SimplPred (\x -> in_mem x mp)
+ LinearScan/Ssreflect.hs view
@@ -0,0 +1,13 @@+module LinearScan.Ssreflect where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++
LinearScan/Ssrfun.hs view
@@ -1,14 +1,18 @@ module LinearScan.Ssrfun where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity import qualified LinearScan.Utils +import qualified LinearScan.Specif as Specif + _Option__apply :: (a1 -> a2) -> a2 -> (Prelude.Maybe a1) -> a2 _Option__apply f x u = case u of {@@ -27,4 +31,17 @@ _Option__map :: (a1 -> a2) -> (Prelude.Maybe a1) -> Prelude.Maybe a2 _Option__map f = _Option__bind (\x -> Prelude.Just (f x))++pcomp :: (a2 -> Prelude.Maybe a1) -> (a3 -> Prelude.Maybe a2) -> a3 ->+ Prelude.Maybe a1+pcomp f g x =+ _Option__bind f (g x)++s2val :: (Specif.Coq_sig2 a1) -> a1+s2val u =+ u++sig_of_sig2 :: (Specif.Coq_sig2 a1) -> a1+sig_of_sig2 u =+ s2val u
LinearScan/Ssrnat.hs view
@@ -4,13 +4,16 @@ module LinearScan.Ssrnat where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity import qualified LinearScan.Utils +import qualified LinearScan.Specif as Specif import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Ssrbool as Ssrbool @@ -26,6 +29,9 @@ unsafeCoerce = IOExts.unsafeCoerce #endif +__ :: any+__ = Prelude.error "Logical or arity value used"+ eqnP :: Eqtype.Equality__Coq_axiom Prelude.Int eqnP n m = Ssrbool.iffP ((Prelude.==) n m) (Ssrbool.idP ((Prelude.==) n m))@@ -38,20 +44,41 @@ nat_eqType = unsafeCoerce nat_eqMixin -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))- (\_ ->- x)- (\i ->- f (iter i f x))- n+find_ex_minn :: (Ssrbool.Coq_pred Prelude.Int) -> Specif.Coq_sig2 Prelude.Int+find_ex_minn p =+ (Prelude.flip (Prelude.$)) __+ ((Prelude.flip (Prelude.$)) __ (\_ _ ->+ let {+ find_ex_minn0 m =+ let {_evar_0_ = \_ -> m} in+ let {_evar_0_0 = \_ -> find_ex_minn0 ((Prelude.succ) m)} in+ case p m of {+ Prelude.True -> _evar_0_ __;+ Prelude.False -> _evar_0_0 __}}+ in find_ex_minn0 0)) +type Coq_ex_minn_spec =+ Prelude.Int+ -- singleton inductive, whose constructor was ExMinnSpec+ +ex_minnP :: (Ssrbool.Coq_pred Prelude.Int) -> Coq_ex_minn_spec+ex_minnP p =+ let {x = find_ex_minn p} in Eqtype.s2val x+ nat_of_bool :: Prelude.Bool -> Prelude.Int nat_of_bool b = case b of { Prelude.True -> (Prelude.succ) 0; Prelude.False -> 0}++odd :: Prelude.Int -> Prelude.Bool+odd n =+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ ->+ Prelude.False)+ (\n' ->+ Prelude.not (odd n'))+ n double_rec :: Prelude.Int -> Prelude.Int double_rec n =
LinearScan/State.hs view
@@ -1,8 +1,10 @@ module LinearScan.State where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity
+ LinearScan/UsePos.hs view
@@ -0,0 +1,26 @@+module LinearScan.UsePos where+++import Debug.Trace (trace, traceShow)+import qualified Prelude+import qualified Data.IntMap+import qualified Data.IntSet+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils+++data UsePos =+ Build_UsePos Prelude.Int Prelude.Bool++uloc :: UsePos -> Prelude.Int+uloc u =+ case u of {+ Build_UsePos uloc0 regReq0 -> uloc0}++regReq :: UsePos -> Prelude.Bool+regReq u =+ case u of {+ Build_UsePos uloc0 regReq0 -> regReq0}+
LinearScan/Vector0.hs view
@@ -4,8 +4,10 @@ module LinearScan.Vector0 where +import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap+import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity
linearscan.cabal view
@@ -1,5 +1,5 @@ name: linearscan-version: 0.2.0.0+version: 0.3.0.0 synopsis: Linear scan register allocator, formally verified in Coq homepage: http://github.com/jwiegley/linearscan license: BSD3@@ -48,27 +48,41 @@ exposed-modules: LinearScan other-modules:+ LinearScan.Allocate+ LinearScan.Assign+ LinearScan.Blocks+ LinearScan.Build+ LinearScan.Choice+ LinearScan.Cursor LinearScan.Datatypes+ LinearScan.Eqtype+ LinearScan.Fintype+ LinearScan.Graph LinearScan.IState- LinearScan.State+ LinearScan.IntMap LinearScan.Interval LinearScan.Lib- -- LinearScan.List0+ LinearScan.List0+ LinearScan.LiveSets LinearScan.Logic LinearScan.Main+ LinearScan.Morph LinearScan.NonEmpty0- -- LinearScan.Peano+ LinearScan.Order LinearScan.Range- LinearScan.Specif- LinearScan.Utils- LinearScan.Vector0- LinearScan.Eqtype- LinearScan.Fintype+ LinearScan.Resolve+ LinearScan.ScanState LinearScan.Seq+ LinearScan.Specif+ LinearScan.Split LinearScan.Ssrbool- -- LinearScan.Ssreflect+ LinearScan.Ssreflect LinearScan.Ssrfun LinearScan.Ssrnat+ LinearScan.State+ LinearScan.UsePos+ LinearScan.Utils+ LinearScan.Vector0 cpp-options: -DMAX_REG=4 -DREG_SIZE=8 ghc-options: -fno-warn-deprecated-flags build-depends: base >=4.7 && <4.8@@ -84,11 +98,11 @@ build-depends: base >=3 , linearscan- , HUnit >= 1.2.5 , hspec >= 1.4.4 , hspec-expectations >= 0.3 , containers >= 0.5.5 , transformers >= 0.3.0.0 , hoopl >= 3.10.0.1 , lens >= 4.2+ , mtl , free
test/Main.hs view
@@ -16,242 +16,365 @@ main :: IO () main = hspec $ do- describe "Sanity tests" $ do- it "Single instruction" $ asmTest- (label "entry"- (add v0 v1 v2)- return_) $+ describe "Sanity tests" sanityTests+ describe "Block tests" blockTests - label "entry"- (add r2 r1 r0)- return_+sanityTests :: SpecWith ()+sanityTests = do+ it "Single instruction" $ asmTest 32+ (label "entry"+ (add v0 v1 v2)+ return_) $ - it "Single, repeated instruction" $ asmTest- (label "entry"- (do add v0 v1 v2- add v0 v1 v2- add v0 v1 v2)- return_) $+ label "entry"+ (add r0 r1 r2)+ return_ - label "entry"- (do add r2 r1 r0- add r2 r1 r0- add r2 r1 r0)- return_+ it "Single, repeated instruction" $ asmTest 32+ (label "entry"+ (do add v0 v1 v2+ add v0 v1 v2+ add v0 v1 v2)+ return_) $ - it "Multiple instructions" $ asmTest- (label "entry"- (do add v0 v1 v2- add v0 v1 v3- add v0 v1 v2)- return_) $+ label "entry"+ (do add r0 r1 r2+ add r0 r1 r2+ add r0 r1 r2)+ return_ - label "entry"- (do add r2 r1 r0- add r2 r1 r3- add r2 r1 r0)- return_+ it "Multiple instructions" $ asmTest 32+ (label "entry"+ (do add v0 v1 v2+ add v0 v1 v3+ add v0 v1 v2)+ return_) $ - it "More variables used than registers" $ 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 v33 v34 v35)- return_) $+ label "entry"+ (do add r0 r1 r2+ add r0 r1 r3+ add r0 r1 r2)+ return_ - 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 "More variables used than registers" $ asmTest 32+ (label "entry"+ (do add v0 v1 v2+ add v3 v4 v5+ add v6 v7 v8+ add v9 v10 v11+ add v12 v13 v14+ add v15 v16 v17+ add v18 v19 v20+ add v21 v22 v23+ add v24 v25 v26+ add v27 v28 v29+ add v30 v31 v32+ add v33 v34 v35)+ return_) $ - 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_) $+ label "entry"+ (do add r0 r1 r24+ add r2 r3 r0+ add r4 r5 r1+ add r6 r7 r2+ add r8 r9 r3+ add r10 r11 r4+ add r12 r13 r5+ add r14 r15 r6+ add r16 r17 r7+ add r18 r19 r8+ add r20 r21 r9+ add r22 r23 r10)+ return_ - label "entry"- (do add r2 r1 r0- add r2 r1 r0- add r2 r1 r0- add r2 r1 r0)- return_+ it "Single long-lived variable" $ asmTest 32+ (label "entry"+ (do add v0 v1 v2+ add v0 v4 v5+ add v0 v7 v8+ add v0 v10 v11)+ return_) $ - 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_) $+ label "entry"+ (do add r0 r1 r5+ add r0 r2 r1+ add r0 r3 r2+ add r0 r4 r3)+ return_ - 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 32+ (label "entry"+ (do add v0 v1 v2+ add v0 v4 v5+ add v0 v4 v8+ add v0 v4 v11)+ return_) $ - 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_) $+ label "entry"+ (do add r0 r1 r3+ add r0 r2 r1+ add r0 r2 r4+ add r0 r2 r5)+ return_ - 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 "One variable with a long interval" $ asmTest 32+ (label "entry"+ (do add v0 v1 v2+ add v3 v4 v5+ add v6 v7 v8+ add v9 v10 v11+ add v12 v13 v14+ add v15 v16 v17+ add v18 v19 v20+ add v21 v22 v23+ add v24 v25 v26+ add v27 v28 v29+ add v30 v31 v32+ add v0 v34 v35)+ return_) $ - 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_) $+ label "entry"+ (do add r0 r1 r23+ add r2 r3 r1+ add r4 r5 r2+ add r6 r7 r3+ add r8 r9 r4+ add r10 r11 r5+ add r12 r13 r6+ add r14 r15 r7+ add r16 r17 r8+ add r18 r19 r9+ add r20 r21 r10+ add r0 r22 r11)+ return_ - 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 "Many variables with long intervals" $ asmTest 32+ (label "entry"+ (do add v0 v1 v2+ add v3 v4 v5+ add v6 v7 v8+ add v9 v10 v11+ add v12 v13 v14+ add v15 v16 v17+ add v18 v19 v20+ add v21 v22 v23+ add v24 v25 v26+ add v27 v28 v29+ add v0 v1 v2+ add v3 v4 v5+ add v6 v7 v8+ add v9 v10 v11+ add v12 v13 v14+ add v15 v16 v17+ add v18 v19 v20+ add v21 v22 v23+ add v24 v25 v26+ add v27 v28 v29)+ return_) $ - it "Spilling one variable" $ asmTest- (label "entry"- (do {- 1 -} add v0 v1 v2- {- 3 -} add v3 v4 v5- {- 5 -} add v6 v7 v8- {- 7 -} add v9 v10 v11- {- 9 -} add v12 v13 v14- {- 11 -} add v15 v16 v17- {- 13 -} add v18 v19 v20- {- 15 -} add v21 v22 v23- {- 17 -} add v24 v25 v26- {- 19 -} add v27 v28 v29- {- 21 -} add v30 v31 v32- {- 23 -} add v0 v1 v2- {- 25 -} add v3 v4 v5- {- 27 -} add v6 v7 v8- {- 29 -} add v9 v10 v11- {- 31 -} add v12 v13 v14- {- 33 -} add v15 v16 v17- {- 35 -} add v18 v19 v20- {- 37 -} add v21 v22 v23- {- 39 -} add v24 v25 v26- {- 41 -} add v27 v28 v29- {- 43 -} add v30 v31 v32)- return_) $+ label "entry"+ (do add r0 r1 r20+ add r2 r3 r21+ add r4 r5 r22+ add r6 r7 r23+ add r8 r9 r24+ add r10 r11 r25+ add r12 r13 r26+ add r14 r15 r27+ add r16 r17 r28+ add r18 r19 r29+ add r0 r1 r20+ add r2 r3 r21+ add r4 r5 r22+ add r6 r7 r23+ add r8 r9 r24+ add r10 r11 r25+ add r12 r13 r26+ add r14 r15 r27+ add r16 r17 r28+ add r18 r19 r29)+ return_ - 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+ it "Spilling one variable" $ asmTest 32+ (label "entry"+ (do {- 1 -} add v0 v1 v2+ {- 3 -} add v3 v4 v5+ {- 5 -} add v6 v7 v8+ {- 7 -} add v9 v10 v11+ {- 9 -} add v12 v13 v14+ {- 11 -} add v15 v16 v17+ {- 13 -} add v18 v19 v20+ {- 15 -} add v21 v22 v23+ {- 17 -} add v24 v25 v26+ {- 19 -} add v27 v28 v29+ {- 21 -} add v30 v31 v32+ {- 23 -} add v0 v1 v2+ {- 25 -} add v3 v4 v5+ {- 27 -} add v6 v7 v8+ {- 29 -} add v9 v10 v11+ {- 31 -} add v12 v13 v14+ {- 33 -} add v15 v16 v17+ {- 35 -} add v18 v19 v20+ {- 37 -} add v21 v22 v23+ {- 39 -} add v24 v25 v26+ {- 41 -} add v27 v28 v29+ {- 43 -} add v30 v31 v32)+ return_) $ - -- 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+ label "entry"+ (do {- 1 -} add r0 r1 r22+ {- 3 -} add r2 r3 r23+ {- 5 -} add r4 r5 r24+ {- 7 -} add r6 r7 r25+ {- 9 -} add r8 r9 r26+ {- 11 -} add r10 r11 r27+ {- 13 -} add r12 r13 r28+ {- 15 -} add r14 r15 r29+ {- 17 -} add r16 r17 r30+ {- 19 -} add r18 r19 r31 - {- 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 we reach the 32nd variable considered (which happens+ -- to be v30), we must spill a register because there are not 32+ -- registers. So we pick the first register, counting from 0,+ -- whose next use position is the furthest from this position.+ -- That happens to be r18, which is next used at position 41.+ save r18 0+ {- 21 -} add r20 r21 r18+ {- 23 -} add r0 r1 r22+ {- 25 -} add r2 r3 r23+ {- 27 -} add r4 r5 r24+ {- 29 -} add r6 r7 r25+ {- 31 -} add r8 r9 r26+ {- 33 -} add r10 r11 r27+ {- 35 -} add r12 r13 r28+ {- 37 -} add r14 r15 r29+ {- 39 -} add r16 r17 r30 - -- When it comes time to reload v29 (which had been allocated- -- to r27), we pick the first available register which happens- -- to be r0 in this case.- restore 0 0- {- 41 -} add r29 r28 r0+ -- When it comes time to reload v29 (which had been allocated+ -- to r18), we pick the first available register which happens+ -- to be r0 in this case.+ restore 0 r0+ {- 41 -} add r0 r19 r31+ {- 43 -} add r20 r21 r18)+ return_ - {- 43 -} add r27 r31 r30)- return_+ it "Inserts only necessary saves and restores" $ asmTest 4+ (label "entry"+ (do {- 3 -} add v0 v1 v2+ {- 5 -} add v2 v1 v3+ {- 7 -} add v3 v2 v4+ {- 9 -} add v4 v1 v0)+ return_) $++ label "entry"+ (do {- 3 -} add r1 r0 r2+ {- 5 -} add r2 r0 r3+ save r0 0+ {- 7 -} add r3 r2 r0+ restore 0 r2+ {- 9 -} add r0 r2 r1)+ return_++blockTests :: SpecWith ()+blockTests = do+ it "Allocates across blocks" $ asmTest 32+ (do label "entry"+ (add v0 v1 v2)+ (jump "skipped")+ label "skipped"+ (do add v2 v3 v4+ add v2 v4 v5)+ (jump "next")+ label "next"+ (do add v2 v5 v6+ add v2 v6 v7+ add v2 v7 v8)+ return_)++ (do label "entry"+ (add r0 r1 r3)+ (jump "skipped")+ label "skipped"+ (do add r3 r2 r0+ add r3 r0 r1)+ (jump "next")+ label "next"+ (do add r3 r1 r0+ add r3 r0 r1+ add r3 r1 r0)+ return_)++ it "Inserts resolving moves" $ asmTest 4+ (do label "entry" -- 1+ (add v0 v1 v2) -- 3+ (branch Zero v2 "B3" "B2") -- 5+ label "B2" -- 7+ (do add v1 v2 v3 -- 9+ add v0 v0 v4 -- 11+ add v0 v0 v5 -- 13+ add v0 v4 v6 -- 15+ add v0 v5 v6) -- 17+ (jump "B4") -- 19+ label "B3" -- 21+ (add v1 v2 v3) -- 23+ (jump "B4") -- 25+ label "B4" -- 27+ (add v3 v3 v0) -- 29+ return_) -- 31++ (do label "entry"+ (add r0 r1 r2)+ (branch Zero r2 "B2" "B3")+ label "B2"+ (add r1 r2 r3)+ (jump "B4")+ label "B3"+ (do add r1 r2 r3+ save r3 0+ add r0 r0 r1+ add r0 r0 r2+ add r0 r1 r3+ add r0 r2 r3+ restore 0 r3)+ (jump "B4")+ label "B4"+ (add r3 r3 r0)+ return_)++ it "Inserts resolving moves another way" $ asmTest 4+ (do label "entry" -- 1+ (add v0 v1 v2) -- 3+ (branch Zero v2 "B3" "B2") -- 5+ label "B2" -- 7+ (add v1 v2 v3) -- 9+ (jump "B4") -- 11+ label "B3" -- 13+ (do add v1 v2 v3 -- 15+ add v0 v0 v4 -- 17+ add v0 v0 v5 -- 19+ add v0 v4 v6 -- 21+ add v0 v5 v6) -- 23+ (jump "B4") -- 25+ label "B4" -- 27+ (add v3 v3 v0) -- 29+ return_) -- 31++ (do label "entry"+ (add r0 r1 r2)+ (branch Zero r2 "B2" "B3")+ label "B2"+ (do add r1 r2 r3+ save r3 0+ add r0 r0 r1+ add r0 r0 r2+ add r0 r1 r3+ add r0 r2 r3+ restore 0 r1)+ (jump "B4")+ label "B3"+ (do add r1 r2 r3+ move r3 r1)+ (jump "B4")+ label "B4"+ (add r1 r1 r0)+ return_)