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