linearscan 0.6.0.0 → 0.7.0
raw patch · 59 files changed
+3333/−1458 lines, 59 files
Files
- Hask/haskell/Hask/Utils.hs +65/−0
- LinearScan.hs +152/−103
- LinearScan/Allocate.hs +35/−39
- LinearScan/Applicative.hs +9/−1
- LinearScan/Ascii.hs +1/−1
- LinearScan/Assign.hs +417/−234
- LinearScan/Blocks.hs +34/−75
- LinearScan/Build.hs +35/−38
- LinearScan/Choice.hs +1/−1
- LinearScan/Class.hs +56/−0
- LinearScan/Const.hs +46/−0
- LinearScan/Context.hs +1/−1
- LinearScan/Cursor.hs +3/−2
- LinearScan/Datatypes.hs +10/−1
- LinearScan/Eqtype.hs +36/−1
- LinearScan/Fintype.hs +12/−1
- LinearScan/Functor.hs +1/−1
- LinearScan/Graph.hs +129/−126
- LinearScan/Identity.hs +41/−0
- LinearScan/IntMap.hs +2/−2
- LinearScan/IntSet.hs +1/−1
- LinearScan/Interval.hs +49/−13
- LinearScan/Iso.hs +0/−23
- LinearScan/Lens.hs +61/−16
- LinearScan/Lib.hs +1/−1
- LinearScan/List0.hs +1/−1
- LinearScan/List1.hs +6/−7
- LinearScan/LiveSets.hs +95/−114
- LinearScan/Logic.hs +1/−1
- LinearScan/Loops.hs +67/−122
- LinearScan/Main.hs +34/−25
- LinearScan/Monad.hs +17/−1
- LinearScan/Morph.hs +6/−8
- LinearScan/Nat.hs +1/−1
- LinearScan/NonEmpty.hs +1/−1
- LinearScan/Prelude0.hs +9/−23
- LinearScan/Range.hs +4/−5
- LinearScan/Resolve.hs +975/−247
- LinearScan/ScanState.hs +20/−16
- LinearScan/Seq.hs +1/−1
- LinearScan/Specif.hs +1/−1
- LinearScan/Spill.hs +45/−38
- LinearScan/Split.hs +10/−8
- LinearScan/Ssr.hs +24/−0
- LinearScan/Ssrbool.hs +1/−1
- LinearScan/Ssreflect.hs +1/−1
- LinearScan/Ssrfun.hs +1/−1
- LinearScan/Ssrnat.hs +1/−1
- LinearScan/State.hs +1/−1
- LinearScan/State0.hs +10/−8
- LinearScan/String0.hs +1/−1
- LinearScan/Trace.hs +1/−1
- LinearScan/Tuple.hs +25/−0
- LinearScan/UsePos.hs +14/−1
- LinearScan/Utils.hs +0/−49
- LinearScan/Vector0.hs +177/−1
- LinearScan/Verify.hs +566/−0
- LinearScan/Yoneda.hs +0/−80
- linearscan.cabal +18/−11
+ Hask/haskell/Hask/Utils.hs view
@@ -0,0 +1,65 @@+module Hask.Utils where++import Data.Char+import Data.List as L+import Data.IntMap as M+import Debug.Trace++trace :: [Int] -> a -> a+trace = Debug.Trace.trace . L.map chr++intMap_mergeWithKey'+ :: (Int -> a -> b -> Maybe c)+ -> ([(Int, a)] -> [(Int, c)])+ -> ([(Int, b)] -> [(Int, c)])+ -> [(Int, a)]+ -> [(Int, b)]+ -> [(Int, c)]+intMap_mergeWithKey' combine only1 only2 m1 m2 =+ M.toList $ M.mergeWithKey combine+ (M.fromList . only1 . M.toList)+ (M.fromList . only2 . M.toList)+ (M.fromList m1) (M.fromList m2)++uncons :: [a] -> Maybe (a, [a])+uncons [] = Nothing+uncons (x:xs) = Just (x, xs)++-- Used for conversions between vectors and seq, which are the same in Haskell+vec_id :: Int -> a -> a+vec_id _ = id++vshiftin :: Int -> [a] -> a -> [a]+vshiftin _ xs x = xs ++ [x]++vreplace :: Int -> [a] -> Int -> a -> [a]+vreplace _ xs n x = take n xs ++ x : drop (n+1) xs++vmap :: Int -> (a -> b) -> [a] -> [b]+vmap _ = L.map++vfoldl' :: Int -> (b -> a -> b) -> b -> [a] -> b+vfoldl' _ = L.foldl'++vfoldl'_with_index :: Int -> (Int -> b -> a -> b) -> b -> [a] -> b+vfoldl'_with_index _ f = go 0+ where+ go _ z [] = z+ go n z (x:xs) = go (n+1) (f n z x) xs++vmap_with_index :: Int -> (Int -> a -> b) -> [a] -> [b]+vmap_with_index _ f = go 0+ where+ go _ [] = []+ go n (x:xs) = f n x : go (n+1) xs++vnth :: Int -> [a] -> Int -> a+vnth _ = (!!)++vec_rect :: b -> (Int -> a -> [a] -> b -> b) -> Int -> [a] -> b+vec_rect z f _ = go z+ where+ go z [] = z+ go z (x:xs) = go (f err x xs z) xs++ err = error "list_rect: attempt to use size"
LinearScan.hs view
@@ -11,6 +11,7 @@ allocate -- * Blocks , LinearScan.BlockInfo(..)+ , LS.UseVerifier(..) -- * Operations , LinearScan.OpInfo(..) , OpKind(..)@@ -28,24 +29,40 @@ import Data.IntSet (IntSet) import qualified Data.IntSet as S import qualified Data.List as L-import Debug.Trace-import qualified LinearScan.Applicative as LS+import Data.Maybe (fromMaybe)+import qualified Hask.Utils as LS+import qualified LinearScan.Applicative as Coq+import LinearScan.Blocks 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.Functor as Coq+import qualified LinearScan.Functor as Functor 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.Monad as Coq import qualified LinearScan.Range as LS+import qualified LinearScan.Resolve as LS import qualified LinearScan.Trace as LS import qualified LinearScan.UsePos as LS-import qualified LinearScan.Utils as LS-import LinearScan.Yoneda (Any)+import qualified LinearScan.Verify as LS import qualified Unsafe.Coerce as U +type Any = Functor.Any++coqFunctor :: forall f. Functor f => Coq.Functor (f Any)+coqFunctor _ _ g x =+ U.unsafeCoerce (fmap g (U.unsafeCoerce x :: f Any))++coqApplicative :: forall f. Applicative f => Coq.Applicative (f Any)+coqApplicative = Coq.Build_Applicative coqFunctor (const pure)+ (\_ _ g x ->+ U.unsafeCoerce (U.unsafeCoerce g <*> U.unsafeCoerce x :: f Any))++coqMonad :: forall m. (Monad m, Applicative m) => Coq.Monad (m Any)+coqMonad = Coq.Build_Monad coqApplicative+ (\_ x -> U.unsafeCoerce (join (U.unsafeCoerce x :: m (m Any)) :: m Any))+ -- | Each variable has associated allocation details, and a flag to indicate -- whether it must be loaded into a register at its point of use. Variables -- are also distinguished by their kind, which allows for restricting the@@ -59,7 +76,7 @@ } deriving instance Eq LS.VarKind-deriving instance Show LS.VarKind+-- deriving instance Show LS.VarKind fromVarInfo :: LinearScan.VarInfo -> LS.VarInfo fromVarInfo (VarInfo a b c) = LS.Build_VarInfo a b c@@ -78,11 +95,11 @@ data OpInfo m op1 op2 = OpInfo { opKind :: op1 -> OpKind , opRefs :: op1 -> [LinearScan.VarInfo]- , moveOp :: PhysReg -> PhysReg -> m [op2]- , swapOp :: PhysReg -> PhysReg -> m [op2]- , saveOp :: PhysReg -> Maybe Int -> m [op2]- , restoreOp :: Maybe Int -> PhysReg -> m [op2]- , applyAllocs :: op1 -> [(Int, PhysReg)] -> m [op2]+ , moveOp :: PhysReg -> LS.VarId -> PhysReg -> m [op2]+ , swapOp :: PhysReg -> LS.VarId -> PhysReg -> LS.VarId -> m [op2]+ , saveOp :: PhysReg -> LS.VarId -> m [op2]+ , restoreOp :: LS.VarId -> PhysReg -> m [op2]+ , applyAllocs :: op1 -> [(LS.VarId, PhysReg)] -> m [op2] , showOp1 :: op1 -> String } @@ -91,9 +108,10 @@ -- Interval Id, it's identity, and possible assigned reg -> [(Int, Either PhysReg LS.VarId, Maybe PhysReg)] -> [(Int, Either PhysReg LS.VarId, Maybe PhysReg)]+ -> [LS.ResolvingMoveSet] -> op1 -> String-showOp1' showop pos ins outs o =+showOp1' showop pos ins outs rms o = let showerv (Left r) = "r" ++ show r showerv (Right v) = "v" ++ show v in let render Nothing = ""@@ -103,9 +121,13 @@ (if i == either id id erv then "" else "[" ++ show i ++ "]") ++ render reg ++ ">\n" in+ let leader = show pos ++ ": " in+ let width = length leader in concatMap (marker "End") outs ++ concatMap (marker "Beg") ins ++- show pos ++ ": " ++ showop o ++ "\n"+ leader ++ showop o ++ "\n" +++ concatMap (\x -> replicate width ' ' +++ replicate 8 ' ' ++ show x ++ "\n") rms deriving instance Eq OpKind deriving instance Show OpKind@@ -114,46 +136,44 @@ => LinearScan.OpInfo m op1 op2 -> LS.OpInfo (m Any) op1 op2 fromOpInfo (OpInfo a b c d e f g h) = LS.Build_OpInfo a (map fromVarInfo . b)- (\r1 r2 _ k -> liftM k (c r1 r2))- (\r1 r2 _ k -> liftM k (d r1 r2))- (\r1 r2 _ k -> liftM k (e r1 r2))- (\r1 r2 _ k -> liftM k (f r1 r2))- (\r1 r2 _ k -> liftM k (g r1 r2)) h--type IntervalId = Int+ (\r1 r2 -> U.unsafeCoerce (c r1 r2))+ (\r1 r2 -> U.unsafeCoerce (d r1 r2))+ (\r1 r2 -> U.unsafeCoerce (e r1 r2))+ (\r1 r2 -> U.unsafeCoerce (f r1 r2))+ (\r1 r2 -> U.unsafeCoerce (g r1 r2)) h data ScanStateDesc = ScanStateDesc { _nextInterval :: Int , intervals :: [LS.IntervalDesc] , fixedIntervals :: [Maybe LS.IntervalDesc]- , unhandled :: [(IntervalId, Int)]- , active :: [(IntervalId, PhysReg)]- , inactive :: [(IntervalId, PhysReg)]- , handled :: [(IntervalId, Maybe PhysReg)]+ , unhandled :: IntMap Int+ , active :: IntMap PhysReg+ , inactive :: IntMap PhysReg+ , handled :: IntMap (Maybe PhysReg) , allocations :: IntMap PhysReg } -deriving instance Show LS.IntervalDesc-deriving instance Show LS.RangeDesc-deriving instance Show LS.UsePos+-- deriving instance Show LS.IntervalDesc+-- deriving instance Show LS.RangeDesc+-- deriving instance Show LS.UsePos instance Show ScanStateDesc where show sd = "Unhandled:\n" ++ concatMap (\(i, _) -> " " ++ showInterval i ++ "\n")- (unhandled sd) +++ (M.toList (unhandled sd)) ++ "Active:\n" ++ concatMap (\(i, r) -> " r" ++ show r ++ showInterval i ++ "\n")- (active sd) +++ (M.toList (active sd)) ++ "Inactive:\n" ++ concatMap (\(i, r) -> " r" ++ show r ++ showInterval i ++ "\n")- (inactive sd) +++ (M.toList (inactive sd)) ++ "Handled:\n" ++ concatMap (\(i, r) -> " " ++ showReg r ++ showInterval i ++ "\n")- (handled sd) +++ (M.toList (handled sd)) ++ "Fixed:\n" ++ concatMap (\(reg, mi) -> case mi of@@ -196,7 +216,8 @@ Just r -> M.insert k r m) M.empty g in let xs = L.foldl' (\m (k, r) -> M.insert k r m) rs (e ++ f) in- ScanStateDesc a b c d e f g xs+ ScanStateDesc a b c+ (M.fromList d) (M.fromList e) (M.fromList f) (M.fromList g) xs data LoopState = LoopState { activeBlocks :: IntSet@@ -231,14 +252,11 @@ (M.fromList (map (fmap S.fromList) g)) (M.fromList h) -tracer :: String -> a -> a-tracer x = Debug.Trace.trace ("====================\n" ++ x)- showBlock1 :: (blk1 -> [op1]) -> LS.BlockId -> LS.OpId- -> [Int]- -> [Int]+ -> IntSet+ -> IntSet -> (LS.OpId -> [op1] -> String) -> blk1 -> String@@ -247,10 +265,14 @@ " => IN:" ++ show liveIns ++ " OUT:" ++ show liveOuts ++ "\n" ++ showops pos (getops b) -showOps1 :: LinearScan.OpInfo accType op1 op2 -> ScanStateDesc -> Int -> [op1]+showOps1 :: LinearScan.OpInfo accType op1 op2+ -> ScanStateDesc+ -> IntMap [LS.ResolvingMoveSet]+ -> Int+ -> [op1] -> String-showOps1 _ _ _ [] = ""-showOps1 oinfo sd pos (o:os) =+showOps1 _ _ _ _ [] = ""+showOps1 oinfo sd rms pos (o:os) = let here = pos*2+1 in let allocs = allocations sd in let k idx (bacc, eacc) i =@@ -271,12 +293,13 @@ -- then (idx, Left idx, mreg) : eacc -- else eacc) in let (begs, ends) =- LS.vfoldl'_with_index (0 :: Int) k ([], []) (intervals sd) in+ LS.vfoldl'_with_index 0 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- ++ showOps1 oinfo sd (pos+1) os+ showOp1' (showOp1 oinfo) (pos*2+1) begs ends+ (fromMaybe [] (M.lookup (pos*2+1) rms)) o+ ++ showOps1 oinfo sd rms (pos+1) os -- | From the point of view of this library, a basic block is nothing more -- than an ordered sequence of operations.@@ -292,22 +315,24 @@ => LinearScan.BlockInfo m blk1 blk2 op1 op2 -> LinearScan.OpInfo m op1 op2 -> ScanStateDesc- -> LS.IntMap LS.BlockLiveSets+ -> IntMap LS.BlockLiveSets+ -> IntMap [LS.ResolvingMoveSet] -> [blk1] -> m String-showBlocks1 binfo oinfo sd ls = go 0+showBlocks1 binfo oinfo sd ls rms = go 0 where go _ [] = return "" go pos (b:bs) = do bid <- LinearScan.blockId binfo b let (liveIn, liveOut) =- case LS.coq_IntMap_lookup bid ls of- Nothing -> (LS.emptyIntSet, LS.emptyIntSet)- Just s -> (LS.blockLiveIn s, LS.blockLiveOut s)+ case M.lookup bid ls of+ Nothing -> (S.empty, S.empty)+ Just s -> (S.fromList (LS.blockLiveIn s),+ S.fromList (LS.blockLiveOut s)) let allops blk = let (x, y, z) = LinearScan.blockOps binfo blk in x ++ y ++ z- (showBlock1 allops bid pos liveIn liveOut (showOps1 oinfo sd) b ++)+ (showBlock1 allops bid pos liveIn liveOut (showOps1 oinfo sd rms) b ++) `liftM` go (pos + length (allops b)) bs fromBlockInfo :: Monad m@@ -315,49 +340,74 @@ -> LS.BlockInfo (m Any) blk1 blk2 op1 op2 fromBlockInfo (BlockInfo a b c d e) = LS.Build_BlockInfo- (\r1 _ k -> liftM k (a r1))- (\r1 _ k -> liftM k (b r1))- (\r1 r2 _ k -> liftM k (c r1 r2))+ (\r1 -> U.unsafeCoerce (a r1))+ (\r1 -> U.unsafeCoerce (b r1))+ (\r1 r2 -> U.unsafeCoerce (c r1 r2)) (\blk -> let (x, y, z) = d blk in ((x, y), z)) e data Details m blk1 blk2 op1 op2 = Details { reason :: Maybe ([LS.SSTrace], LS.FinalStage)- , liveSets :: [(Int, LS.BlockLiveSets)]+ , liveSets :: IntMap LS.BlockLiveSets+ , resolvingMoves :: IntMap [LS.ResolvingMoveSet] , _inputBlocks :: [blk1] , orderedBlocks :: [blk1]- , allocatedBlocks :: [blk2]- , scanStatePre :: Maybe ScanStateDesc+ , allocatedBlocks :: Either (IntMap [LS.AllocError]) [blk2]+ , _scanStatePre :: Maybe ScanStateDesc , scanStatePost :: Maybe ScanStateDesc , blockInfo :: LinearScan.BlockInfo m blk1 blk2 op1 op2 , opInfo :: LinearScan.OpInfo m op1 op2 , loopState :: LoopState } +deriving instance Show LS.AllocError++instance Show LS.ResolvingMoveSet where+ show (LS.RSMove fr fv tr) =+ "move (r" ++ show fr ++ " v" ++ show fv ++ ") " +++ "(r" ++ show tr ++ " v" ++ show fv ++ ")"+ show (LS.RSSwap fr fv tr tv) =+ "swap (r" ++ show fr ++ " v" ++ show fv ++ ") " +++ "(r" ++ show tr ++ " v" ++ show tv ++ ")"+ show (LS.RSSpill fr tv) =+ "spill (r" ++ show fr ++ " v" ++ show tv ++ ")"+ show (LS.RSRestore fv tr) =+ "restore (r" ++ show tr ++ " v" ++ show fv ++ ")"+ show (LS.RSAllocReg fv tr) =+ "reserve (r" ++ show tr ++ " v" ++ show fv ++ ")"+ show (LS.RSFreeReg fr tv) =+ "release (r" ++ show fr ++ " v" ++ show tv ++ ")"+ show (LS.RSAssignReg fv tr) =+ "assign (r" ++ show tr ++ " v" ++ show fv ++ ")"+ show (LS.RSClearReg fr tv) =+ "clear (r" ++ show fr ++ " v" ++ show tv ++ ")"+ -- show (LS.RSAllocStack tv) = "<AllocStack (v" ++ show tv ++ ")>"+ -- show (LS.RSFreeStack fv) = "<FreeStack (v" ++ show fv ++ ")>"++-- showResolvingMoves :: IntMap [LS.ResolvingMoveSet] -> String+-- showResolvingMoves =+-- M.foldlWithKey' (\acc k mv ->+-- acc ++ " " ++ show k ++ " => "+-- ++ L.intercalate "\n " (map show mv) ++ "\n") ""+ showDetails :: Monad m => Details m blk1 blk2 op1 op2 -> m String showDetails err = do- pre <- showPreScanStateDesc (scanStatePre err)- post <- showPostScanStateDesc (scanStatePost err)+ -- pre <- showScanStateDesc (scanStatePre err)+ post <- showScanStateDesc (scanStatePost err) return $ "Reason: " ++ show (reason err) ++ "\n\n"- ++ ">>> ScanState before allocation:\n"- ++ pre ++ "\n"+ -- ++ ">>> ScanState before allocation:\n"+ -- ++ pre ++ "\n" ++ ">>> ScanState after allocation:\n" ++ post ++ "\n"+ -- ++ ">>> ResolvingMoves =\n"+ -- ++ showResolvingMoves (resolvingMoves err) ++ "\n" ++ ">>> " ++ show (loopState err) ++ "\n" where- showPreScanStateDesc Nothing = return ""- showPreScanStateDesc (Just sd) =- liftM2 (++)- (showBlocks1 (blockInfo err) (opInfo err) sd- (liveSets err) (orderedBlocks err))- (return ("\n" ++ show sd))-- -- jww (2015-05-23): Show allocatedBlocks here?- showPostScanStateDesc Nothing = return ""- showPostScanStateDesc (Just sd) =- liftM2 (++)- (showBlocks1 (blockInfo err) (opInfo err) sd- (liveSets err) (orderedBlocks err))- (return ("\n" ++ show sd))+ showScanStateDesc Nothing = return ""+ showScanStateDesc (Just sd) =+ liftM2 (++) (showBlocks1 (blockInfo err) (opInfo err) sd+ (liveSets err) (resolvingMoves err)+ (orderedBlocks err))+ (return ("\n" ++ show sd)) deriving instance Show LS.FinalStage deriving instance Show LS.BlockLiveSets@@ -381,9 +431,11 @@ -> LinearScan.BlockInfo m blk1 blk2 op1 op2 -> LinearScan.OpInfo m op1 op2 -> Details m blk1 blk2 op1 op2-toDetails (LS.Build_Details a b c d e f g h) binfo oinfo =- Details a b c d e (fmap toScanStateDesc f) (fmap toScanStateDesc g)- binfo oinfo (toLoopState h)+toDetails (LS.Build_Details a b c d e f g h i) binfo oinfo =+ Details a (M.fromList b) (M.fromList c) d e+ (either (Left . M.fromList) Right f)+ (fmap toScanStateDesc g) (fmap toScanStateDesc h)+ binfo oinfo (toLoopState i) -- | Transform a list of basic blocks containing variable references, into an -- equivalent list where each reference is associated with a register@@ -400,30 +452,28 @@ => Int -- ^ Maximum number of registers to use -> LinearScan.BlockInfo m blk1 blk2 op1 op2 -> LinearScan.OpInfo m op1 op2- -> [blk1] -> m (Either [String] [blk2])-allocate 0 _ _ _ = return $ Left ["Cannot allocate with no registers"]-allocate _ _ _ [] = return $ Left ["No basic blocks were provided"]-allocate maxReg 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 $ case reason res' of- Just (err, _) -> Left $ tracer dets $ map reasonToStr err- Nothing -> Right $ allocatedBlocks res'+ -> LS.UseVerifier+ -> [blk1] -> m (Either (String, [String]) [blk2])+allocate 0 _ _ _ _ = return $ Left ("", ["Cannot allocate with no registers"])+allocate _ _ _ _ [] = return $ Left ("", ["No basic blocks were provided"])+allocate maxReg binfo oinfo useVerifier blocks = do+ res <- U.unsafeCoerce $ LS.linearScan coqMonad maxReg+ (fromBlockInfo binfo) (fromOpInfo oinfo) useVerifier blocks+ let res' = toDetails res binfo oinfo+ case reason res' of+ Just (err, _) -> do+ dets <- showDetails res'+ return $ Left (dets, map reasonToStr err)+ Nothing -> case allocatedBlocks res' of+ Left m -> do+ dets <- showDetails res'+ return $ Left (dets,+ -- jww (2015-07-02): NYI+ concatMap (\(pos, es) ->+ ("At position " ++ show pos) : map show es)+ (M.toList m))+ Right blks -> return $ Right blks where- dict :: LS.Monad (m Any)- dict = LS.Build_Monad- (LS.Build_Applicative- (\(_ :: ()) (_ :: ()) (f :: Any -> Any) x ->- U.unsafeCoerce (fmap f (U.unsafeCoerce x :: m Any)))- (\(_ :: ()) -> pure)- (\(_ :: ()) (_ :: ()) f x ->- U.unsafeCoerce (U.unsafeCoerce f <*> U.unsafeCoerce x :: m Any)))- (\(_ :: ()) x ->- U.unsafeCoerce (join (U.unsafeCoerce x :: m (m Any)) :: m Any))- reasonToStr r = case r of LS.EIntersectsWithFixedInterval pos reg -> "Current interval intersects with " ++@@ -458,7 +508,6 @@ ++ " 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 ->
LinearScan/Allocate.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Context as Context import qualified LinearScan.Cursor as Cursor@@ -25,6 +25,7 @@ import qualified LinearScan.Split as Split import qualified LinearScan.Trace as Trace import qualified LinearScan.UsePos as UsePos+import qualified LinearScan.Vector0 as Vector0 import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Fintype as Fintype import qualified LinearScan.Seq as Seq@@ -63,19 +64,19 @@ Cursor.withCursor maxReg pre (\sd _ -> let {int = Cursor.curIntDetails maxReg sd} in Context.ipure- (case LinearScan.Utils.nth maxReg (ScanState.fixedIntervals maxReg sd)- reg of {- Prelude.Just i -> Interval.intervalIntersectionPoint ( int) ( i);+ (case Vector0.vnth maxReg (ScanState.fixedIntervals maxReg sd) reg of {+ Prelude.Just i -> Interval.intervalOverlapPoint ( int) ( i); Prelude.Nothing -> Prelude.Nothing})) -updateRegisterPos :: Prelude.Int -> ([] (Prelude.Maybe Prelude0.Coq_oddnum))- -> Prelude.Int -> (Prelude.Maybe Prelude0.Coq_oddnum) ->- [] (Prelude.Maybe Prelude0.Coq_oddnum)+updateRegisterPos :: Prelude.Int -> (Vector0.Vec+ (Prelude.Maybe Prelude0.Coq_oddnum)) -> Prelude.Int ->+ (Prelude.Maybe Prelude0.Coq_oddnum) -> Vector0.Vec+ (Prelude.Maybe Prelude0.Coq_oddnum) updateRegisterPos n v r p = case p of { Prelude.Just x ->- LinearScan.Utils.set_nth n v r (Prelude.Just- (case LinearScan.Utils.nth n v r of {+ Vector0.vreplace n v r (Prelude.Just+ (case Vector0.vnth n v r of { Prelude.Just n0 -> case (Prelude.<=) ((Prelude.succ) ( n0)) ( x) of { Prelude.True -> n0;@@ -91,11 +92,11 @@ Prelude.Nothing -> Prelude.Nothing} findEligibleRegister :: Prelude.Int -> ScanState.ScanStateDesc ->- Interval.IntervalDesc -> ([]+ Interval.IntervalDesc -> (Vector0.Vec (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 Vector0.vfoldl_with_index maxReg (\reg acc mint -> case acc of { (,) fup fai -> case mint of {@@ -109,9 +110,9 @@ (,) (updateRegisterPos maxReg fup reg (Interval.intervalIntersectionPoint ( int) d))- (LinearScan.Utils.set_nth maxReg fai reg intersects);+ (Vector0.vreplace maxReg fai reg intersects); Prelude.Nothing -> acc}}) ((,) xs- (Data.List.replicate maxReg Prelude.False))+ (Vector0.vconst maxReg Prelude.False)) (ScanState.fixedIntervals maxReg sd) of { (,) xs0 fixedAndIntersects -> ScanState.registerWithHighestPos maxReg fixedAndIntersects xs0}@@ -128,18 +129,20 @@ in let { freeUntilPos' = Data.List.foldl' (go (\x -> Prelude.Just Prelude0.odd1))- (Data.List.replicate maxReg Prelude.Nothing)+ (Vector0.vconst maxReg Prelude.Nothing) (ScanState.active maxReg sd)} in let { intersectingIntervals = Prelude.filter (\x -> Interval.intervalsIntersect- ( (Cursor.curIntDetails maxReg sd))- (- (LinearScan.Utils.nth- (ScanState.nextInterval maxReg sd)- (ScanState.intervals maxReg sd)- (Prelude.fst x))))+ (Interval.getIntervalDesc+ ( (Cursor.curIntDetails maxReg sd)))+ (Interval.getIntervalDesc+ (+ (Vector0.vnth+ (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd)+ (Prelude.fst x))))) (ScanState.inactive maxReg sd)} in let {@@ -147,7 +150,7 @@ (go (\i -> Interval.intervalIntersectionPoint (- (LinearScan.Utils.nth+ (Vector0.vnth (ScanState.nextInterval maxReg sd) (ScanState.intervals maxReg sd) i)) ( (Cursor.curIntDetails maxReg sd))))@@ -208,19 +211,20 @@ Prelude.map (\i -> (,) (Interval.packInterval (- (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)+ (Vector0.vnth (ScanState.nextInterval maxReg sd) (ScanState.intervals maxReg sd) (Prelude.fst i)))) (Prelude.snd i)) xs} in let { nextUsePos' = Data.List.foldl' (go maxReg)- (Data.List.replicate maxReg Prelude.Nothing)+ (Vector0.vconst maxReg Prelude.Nothing) (resolve (ScanState.active maxReg sd))} in let { intersectingIntervals = Prelude.filter (\x -> Interval.intervalsIntersect- ( (Cursor.curIntDetails maxReg sd))+ (Interval.getIntervalDesc+ ( (Cursor.curIntDetails maxReg sd))) ( (Prelude.fst x))) (resolve (ScanState.inactive maxReg sd))} in@@ -289,7 +293,7 @@ case (Prelude.<=) ((Prelude.succ) (Interval.intervalEnd (- (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)+ (Vector0.vnth (ScanState.nextInterval maxReg z) (ScanState.intervals maxReg z) (Prelude.fst x))))) pos of { Prelude.True -> Morph.moveActiveToHandled maxReg z Prelude.False (unsafeCoerce x);@@ -297,7 +301,7 @@ case Prelude.not (Interval.posWithinInterval (- (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)+ (Vector0.vnth (ScanState.nextInterval maxReg z) (ScanState.intervals maxReg z) (Prelude.fst x))) pos) of { Prelude.True -> Morph.moveActiveToInactive maxReg z (unsafeCoerce x); Prelude.False -> z}}@@ -352,7 +356,7 @@ case (Prelude.<=) ((Prelude.succ) (Interval.intervalEnd (- (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)+ (Vector0.vnth (ScanState.nextInterval maxReg z) (ScanState.intervals maxReg z) (Prelude.fst x))))) pos of { Prelude.True -> let {@@ -363,7 +367,7 @@ Prelude.False -> case Interval.posWithinInterval (- (LinearScan.Utils.nth (ScanState.nextInterval maxReg z)+ (Vector0.vnth (ScanState.nextInterval maxReg z) (ScanState.intervals maxReg z) (Prelude.fst x))) pos of { Prelude.True -> let {filtered_var = moveInactiveToActive' maxReg z x xs e} in@@ -457,19 +461,11 @@ Prelude.Just _ -> go cnt (Morph.Build_SSInfo (Morph.thisDesc maxReg sd ss') __);- Prelude.Nothing ->- (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))- (\_ -> Prelude.Right- ss')- (\n0 -> Prelude.Left ((,) ((:)- Trace.EUnexpectedNoMoreUnhandled [])- (ScanState.packScanState maxReg ScanState.InUse- (Morph.thisDesc maxReg sd ss'))))- cnt}}})+ Prelude.Nothing -> Prelude.Right ss'}}}) count0} in go} in- case LinearScan.Utils.uncons (ScanState.unhandled maxReg sd) of {+ case Hask.Utils.uncons (ScanState.unhandled maxReg sd) of { Prelude.Just s -> case s of { (,) x s0 ->@@ -507,7 +503,7 @@ Prelude.map (\x -> Build_Allocation ( (Prelude.fst x)) (Interval.getIntervalDesc (- (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)+ (Vector0.vnth (ScanState.nextInterval maxReg sd) (ScanState.intervals maxReg sd) (Prelude.fst x)))) (Prelude.snd x)) (ScanState.handled maxReg sd)
LinearScan/Applicative.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Functor as Functor @@ -68,4 +68,12 @@ liftA2 :: (Applicative a1) -> (a2 -> a3 -> a4) -> a1 -> a1 -> a1 liftA2 h f x y = ap h (Functor.fmap (is_functor h) f x) y++data Alternative f =+ Build_Alternative (Applicative f) (() -> f) (() -> f -> f -> f)++choose :: (Alternative a1) -> a1 -> a1 -> a1+choose alternative x x0 =+ case alternative of {+ Build_Alternative alt_is_applicative empty choose0 -> choose0 __ x x0}
LinearScan/Ascii.hs view
@@ -10,7 +10,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils data Coq_ascii =
LinearScan/Assign.hs view
@@ -11,26 +11,27 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Allocate as Allocate import qualified LinearScan.Applicative as Applicative import qualified LinearScan.Blocks as Blocks+import qualified LinearScan.Class as Class import qualified LinearScan.Functor as Functor 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.Iso as Iso import qualified LinearScan.Lens as Lens import qualified LinearScan.List1 as List1 import qualified LinearScan.LiveSets as LiveSets+import qualified LinearScan.Loops as Loops 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.Verify as Verify import qualified LinearScan.Eqtype as Eqtype-import qualified LinearScan.Fintype as Fintype import qualified LinearScan.Seq as Seq import qualified LinearScan.Ssrnat as Ssrnat @@ -56,112 +57,54 @@ type PhysReg = Prelude.Int -data AllocState =- Build_AllocState ([] (Prelude.Maybe Prelude.Int)) (IntMap.IntMap- (Prelude.Maybe PhysReg))--newAllocState :: Prelude.Int -> AllocState-newAllocState maxReg =- Build_AllocState (Data.List.replicate maxReg Prelude.Nothing)- IntMap.emptyIntMap--data AllocError =- Build_AllocError Prelude.Int (Prelude.Maybe PhysReg) (Prelude.Maybe- PhysReg) Blocks.BlockId--data AssnStateInfo =- Build_AssnStateInfo Blocks.OpId Blocks.OpId Blocks.OpId AllocState - (IntMap.IntMap AllocState) (IntMap.IntMap AllocState) ([] AllocError)--assnOpId :: Prelude.Int -> AssnStateInfo -> Blocks.OpId-assnOpId maxReg a =- case a of {- Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0- assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 -> assnOpId0}--assnBlockBeg :: Prelude.Int -> AssnStateInfo -> Blocks.OpId-assnBlockBeg maxReg a =- case a of {- Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0- assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 -> assnBlockBeg0}--assnBlockEnd :: Prelude.Int -> AssnStateInfo -> Blocks.OpId-assnBlockEnd maxReg a =- case a of {- Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0- assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 -> assnBlockEnd0}--assnAllocState :: Prelude.Int -> AssnStateInfo -> AllocState-assnAllocState maxReg a =- case a of {- Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0- assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 -> assnAllocState0}+data AssnStateDesc =+ Build_AssnStateDesc Blocks.OpId Blocks.OpId Blocks.OpId -assnBlockEntryAllocs :: Prelude.Int -> AssnStateInfo -> IntMap.IntMap- AllocState-assnBlockEntryAllocs maxReg a =+assnOpId :: AssnStateDesc -> Blocks.OpId+assnOpId a = case a of {- Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0- assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 ->- assnBlockEntryAllocs0}+ Build_AssnStateDesc assnOpId0 assnBlockBeg0 assnBlockEnd0 -> assnOpId0} -assnBlockExitAllocs :: Prelude.Int -> AssnStateInfo -> IntMap.IntMap- AllocState-assnBlockExitAllocs maxReg a =+assnBlockBeg :: AssnStateDesc -> Blocks.OpId+assnBlockBeg a = case a of {- Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0- assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 ->- assnBlockExitAllocs0}+ Build_AssnStateDesc assnOpId0 assnBlockBeg0 assnBlockEnd0 -> assnBlockBeg0} -assnErrors :: Prelude.Int -> AssnStateInfo -> [] AllocError-assnErrors maxReg a =+assnBlockEnd :: AssnStateDesc -> Blocks.OpId+assnBlockEnd a = case a of {- Build_AssnStateInfo assnOpId0 assnBlockBeg0 assnBlockEnd0 assnAllocState0- assnBlockEntryAllocs0 assnBlockExitAllocs0 assnErrors0 -> assnErrors0}--newAssnStateInfo :: Prelude.Int -> AssnStateInfo-newAssnStateInfo maxReg =- Build_AssnStateInfo ((Prelude.succ) 0) ((Prelude.succ) 0) ((Prelude.succ)- 0) (newAllocState maxReg) IntMap.emptyIntMap IntMap.emptyIntMap []+ Build_AssnStateDesc assnOpId0 assnBlockBeg0 assnBlockEnd0 -> assnBlockEnd0} -_assnOpId :: Prelude.Int -> (Functor.Functor a1) -> (Blocks.OpId -> a1) ->- AssnStateInfo -> a1-_assnOpId maxReg h f 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))+newAssnStateDesc :: AssnStateDesc+newAssnStateDesc =+ Build_AssnStateDesc ((Prelude.succ) 0) ((Prelude.succ) 0) ((Prelude.succ)+ 0) -_assnBlockBeg :: Prelude.Int -> (Functor.Functor a1) -> (Blocks.OpId -> a1)- -> AssnStateInfo -> a1-_assnBlockBeg maxReg h f s =- 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))+_assnOpId :: (Functor.Functor a1) -> (Blocks.OpId -> a1) -> AssnStateDesc ->+ a1+_assnOpId h f s =+ Functor.fmap h (\x -> Build_AssnStateDesc x (assnBlockBeg s)+ (assnBlockEnd s)) (f (assnOpId s)) -_assnBlockEnd :: Prelude.Int -> (Functor.Functor a1) -> (Blocks.OpId -> a1)- -> AssnStateInfo -> a1-_assnBlockEnd maxReg h f 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))+_assnBlockBeg :: (Functor.Functor a1) -> (Blocks.OpId -> a1) -> AssnStateDesc+ -> a1+_assnBlockBeg h f s =+ Functor.fmap h (\x -> Build_AssnStateDesc (assnOpId s) x (assnBlockEnd s))+ (f (assnBlockBeg s)) -type AssnState mType a = State0.StateT AssnStateInfo mType a+_assnBlockEnd :: (Functor.Functor a1) -> (Blocks.OpId -> a1) -> AssnStateDesc+ -> a1+_assnBlockEnd h f s =+ Functor.fmap h (\x -> Build_AssnStateDesc (assnOpId s) (assnBlockBeg s) x)+ (f (assnBlockEnd s)) generateMoves :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo a3 a1 a2) -> ([] Resolve.ResolvingMove) -> a3 generateMoves maxReg mDict oinfo moves = Monad.forFoldrM mDict [] moves (\mv acc -> let {- k = (Prelude..)- (Functor.fmap- (Applicative.is_functor (Monad.is_applicative mDict)) (\x ->- Prelude.Just x))- (Iso.iso_to- (Yoneda.coq_Yoneda_lemma- (Applicative.is_functor (Monad.is_applicative mDict))))}+ k = Functor.fmap (Applicative.is_functor (Monad.is_applicative mDict))+ (\x -> Prelude.Just x)} in Monad.bind mDict (\mops -> Applicative.pure (Monad.is_applicative mDict)@@ -169,173 +112,413 @@ Prelude.Just ops -> (Prelude.++) ops acc; Prelude.Nothing -> acc})) (case mv of {- Resolve.Move sreg dreg ->- k (\_ -> Blocks.moveOp maxReg mDict oinfo sreg dreg);- Resolve.Swap sreg dreg ->- k (\_ -> Blocks.swapOp maxReg mDict oinfo sreg dreg);- Resolve.Spill sreg vid ->- k (\_ -> Blocks.saveOp maxReg mDict oinfo sreg (Prelude.Just vid));- Resolve.Restore vid dreg ->- k (\_ ->- Blocks.restoreOp maxReg mDict oinfo (Prelude.Just vid) dreg);- Resolve.Nop ->+ Resolve.Move sreg svid dreg ->+ k (Blocks.moveOp maxReg mDict oinfo sreg svid dreg);+ Resolve.Swap sreg svid dreg dvid ->+ k (Blocks.swapOp maxReg mDict oinfo sreg svid dreg dvid);+ Resolve.Spill sreg svid ->+ k (Blocks.saveOp maxReg mDict oinfo sreg svid);+ Resolve.Restore dvid dreg ->+ k (Blocks.restoreOp maxReg mDict oinfo dvid dreg);+ Resolve.AllocReg v p ->+ Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing;+ Resolve.FreeReg p v -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing})) varAllocs :: Prelude.Int -> Prelude.Int -> ([] Allocate.Allocation) ->- Blocks.VarInfo -> [] ((,) Blocks.VarId PhysReg)-varAllocs maxReg opid allocs v =+ UsePos.VarKind -> Eqtype.Equality__Coq_sort -> []+ ((,) Blocks.VarId PhysReg)+varAllocs maxReg opid allocs kind vid =+ Prelude.map (\x -> (,) (unsafeCoerce vid) x)+ (List1.catMaybes+ (Prelude.map (\i -> Allocate.intReg maxReg i)+ (Prelude.filter (\i ->+ let {int = Allocate.intVal maxReg i} in+ (Prelude.&&)+ (Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce (Interval.ivar int)) vid)+ ((Prelude.&&) ((Prelude.<=) (Interval.ibeg int) opid)+ (case kind of {+ UsePos.Input -> (Prelude.<=) opid (Interval.iend int);+ _ -> (Prelude.<=) ((Prelude.succ) opid) (Interval.iend int)})))+ allocs)))++varInfoAllocs :: Prelude.Int -> Prelude.Int -> ([] Allocate.Allocation) ->+ Blocks.VarInfo -> [] ((,) Blocks.VarId PhysReg)+varInfoAllocs maxReg opid allocs v = case Blocks.varId maxReg v of { Prelude.Left p -> []; Prelude.Right vid ->- Prelude.map (\x -> (,) vid x)- (List1.catMaybes- (Prelude.map (\i -> Allocate.intReg maxReg i)- (Prelude.filter (\i ->- let {int = Allocate.intVal maxReg i} in- (Prelude.&&)- (Eqtype.eq_op Ssrnat.nat_eqType- (unsafeCoerce (Interval.ivar int)) (unsafeCoerce vid))- ((Prelude.&&) ((Prelude.<=) (Interval.ibeg int) opid)- (case Blocks.varKind maxReg v of {- UsePos.Input -> (Prelude.<=) opid (Interval.iend int);- _ -> (Prelude.<=) ((Prelude.succ) opid) (Interval.iend int)})))- allocs)))}+ varAllocs maxReg opid allocs (Blocks.varKind maxReg v) (unsafeCoerce vid)} +type Verified mType a = Verify.Verified mType AssnStateDesc a++_verExt :: Prelude.Int -> (Functor.Functor a1) -> (AssnStateDesc -> a1) ->+ (Verify.VerifiedSig AssnStateDesc) -> a1+_verExt maxReg h x x0 =+ Verify._verExt maxReg h x x0+ setAllocations :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo a3 - a1 a2) -> ([] Allocate.Allocation) -> a1 -> AssnState - a3 ([] a2)-setAllocations maxReg mDict oinfo allocs op =+ a1 a2) -> Verify.UseVerifier -> ([] Allocate.Allocation) ->+ a1 -> Verified a3 ([] a2)+setAllocations maxReg mDict oinfo useVerifier allocs op = Monad.bind (State0.coq_StateT_Monad mDict) (\assn ->- let {opid = assnOpId maxReg assn} in+ let {opid = assnOpId assn} in let {vars = Blocks.opRefs maxReg mDict oinfo op} in let {- regs = List1.concat (Prelude.map (varAllocs maxReg opid allocs) vars)}+ regs = List1.concat+ (Prelude.map (varInfoAllocs maxReg opid allocs) vars)} in 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))- (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 {+ (Lens.plusStateT (\_ y ->+ (Prelude..) (_verExt maxReg y) (_assnOpId y)) ((Prelude.succ)+ ((Prelude.succ) 0)) mDict))+ (case (Prelude.&&) ((Prelude.<=) (assnBlockBeg assn) opid)+ ((Prelude.<=) ((Prelude.succ) opid) (assnBlockEnd assn)) of { Prelude.True ->- State0.lift mDict- (generateMoves maxReg mDict oinfo- (Resolve.determineMoves maxReg- (Resolve.resolvingMoves maxReg allocs opid ((Prelude.succ)- ((Prelude.succ) opid)))));+ let {+ moves = Resolve.determineMoves maxReg+ (Resolve.resolvingMoves maxReg allocs opid+ ((Prelude.succ) ((Prelude.succ) opid)))}+ in+ Monad.bind (State0.coq_StateT_Monad mDict) (\moves' ->+ Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict+ (State0.coq_StateT_Monad mDict)+ (generateMoves maxReg mDict oinfo moves'))+ (Verify.verifyResolutions maxReg mDict opid useVerifier moves); Prelude.False -> Applicative.pure (State0.coq_StateT_Applicative mDict) []}))- (State0.lift mDict- (Iso.iso_to- (Yoneda.coq_Yoneda_lemma- (Applicative.is_functor (Monad.is_applicative mDict))) (\_ ->- Blocks.applyAllocs maxReg mDict oinfo op regs))))- (State0.getT (Monad.is_applicative mDict))--resolveMappings :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo - a3 a1 a2) -> Prelude.Int -> ([] a2) -> (IntMap.IntMap- ((,) Graph.Graph Graph.Graph)) -> a3-resolveMappings maxReg mDict oinfo bid opsm mappings =- case IntMap.coq_IntMap_lookup bid mappings of {- Prelude.Just graphs ->- case graphs of {- (,) gbeg gend ->- Monad.bind mDict (\bmoves ->- Monad.bind mDict (\emoves ->- Applicative.pure (Monad.is_applicative mDict)- ((Prelude.++) bmoves ((Prelude.++) opsm emoves)))- (generateMoves maxReg mDict oinfo- (Prelude.map (Resolve.moveFromGraph maxReg)- (Graph.topsort- (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)- Ssrnat.nat_eqType) gend))))- (generateMoves maxReg mDict oinfo- (Prelude.map (Resolve.moveFromGraph maxReg)- (Graph.topsort- (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)- Ssrnat.nat_eqType) gbeg)))};- Prelude.Nothing -> Applicative.pure (Monad.is_applicative mDict) opsm}+ (Verify.verifyApplyAllocs maxReg mDict oinfo opid useVerifier op regs))+ (Lens.use (Lens.stepdownl' (\_ -> _verExt maxReg)) mDict) considerOps :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 - a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([]- Allocate.Allocation) -> (IntMap.IntMap LiveSets.BlockLiveSets)- -> (IntMap.IntMap Resolve.BlockMoves) -> ([] a1) -> AssnState- a5 ([] a2)-considerOps maxReg mDict binfo oinfo allocs liveSets mappings =+ a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> Verify.UseVerifier+ -> ([] Allocate.Allocation) -> (IntMap.IntMap+ LiveSets.BlockLiveSets) -> (IntMap.IntMap Resolve.BlockMoves)+ -> Loops.LoopState -> ([] a1) -> Verified a5 ([] a2)+considerOps maxReg mDict binfo oinfo useVerifier allocs liveSets mappings loops = Monad.mapM (State0.coq_StateT_Applicative mDict) (\blk -> case Blocks.blockOps mDict binfo blk of { (,) p opse -> case p of { (,) opsb opsm ->- Monad.bind (State0.coq_StateT_Monad mDict) (\x ->- let {k = setAllocations maxReg mDict oinfo allocs} in- 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 {- [] ->- Applicative.pure- (State0.coq_StateT_Applicative mDict)- (Blocks.setBlockOps mDict binfo blk [] opsm'' []);- (:) e es ->- 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 {- [] ->- Applicative.pure- (State0.coq_StateT_Applicative mDict)- (Blocks.setBlockOps mDict binfo blk ((:) b [])- ((Prelude.++) bs opsm'') []);- (:) e es ->- 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) []))}})- (State0.lift mDict- (resolveMappings maxReg mDict oinfo bid opsm' mappings)))- (State0.lift mDict- (Iso.iso_to- (Yoneda.coq_Yoneda_lemma- (Applicative.is_functor (Monad.is_applicative mDict)))- (\_ -> Blocks.blockId mDict binfo blk))))- (Monad.concatMapM (State0.coq_StateT_Applicative mDict) k- opse))- (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- (Ssrnat.double- ((Prelude.+) (Data.List.length opsb)- (Data.List.length opsm))))- (Lens.set (\_ -> _assnBlockBeg maxReg)- ((Prelude.+) opid (Ssrnat.double (Data.List.length opsb)))- assn)))}})+ Monad.bind (State0.coq_StateT_Monad mDict) (\opid ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\bid ->+ case IntMap.coq_IntMap_lookup bid liveSets of {+ Prelude.Just bls ->+ let {liveIns = LiveSets.blockLiveIn bls} in+ let {liveOuts = LiveSets.blockLiveOut bls} in+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ let {+ eg = Graph.emptyGraph (Resolve.coq_ResGraphNode maxReg)+ (Resolve.coq_ResGraphEdge_eqType maxReg)+ (unsafeCoerce (Resolve.determineEdge maxReg))}+ in+ case case IntMap.coq_IntMap_lookup bid mappings of {+ Prelude.Just graphs -> graphs;+ Prelude.Nothing -> (,) eg eg} of {+ (,) gbeg gend ->+ let {+ k = setAllocations maxReg mDict oinfo useVerifier+ allocs}+ in+ Monad.bind (State0.coq_StateT_Monad mDict) (\opsb' ->+ let {+ begMoves = Graph.topsort+ (Resolve.coq_ResGraphNode maxReg)+ (Resolve.coq_ResGraphEdge_eqType+ maxReg) gbeg+ (unsafeCoerce+ (Resolve.splitEdge maxReg))}+ in+ Monad.bind (State0.coq_StateT_Monad mDict) (\opid0 ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\begMoves' ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\bmoves ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\opsm' ->+ let {+ endMoves = Graph.topsort+ (Resolve.coq_ResGraphNode+ maxReg)+ (Resolve.coq_ResGraphEdge_eqType+ maxReg) gend+ (unsafeCoerce+ (Resolve.splitEdge maxReg))}+ in+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\opid1 ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\endMoves' ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\emoves ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\opse' ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\x2 ->+ case opsb' of {+ [] ->+ let {+ opsm'' = (Prelude.++) bmoves+ ((Prelude.++) opsm'+ emoves)}+ in+ case opse' of {+ [] ->+ Applicative.pure+ (State0.coq_StateT_Applicative+ mDict)+ (Blocks.setBlockOps mDict+ binfo blk [] opsm'' []);+ (:) e es ->+ Applicative.pure+ (State0.coq_StateT_Applicative+ mDict)+ (Blocks.setBlockOps mDict+ binfo blk []+ ((Prelude.++) opsm''+ (Seq.belast e es)) ((:)+ (Seq.last e es) []))};+ (:) b bs ->+ let {+ opsm'' = (Prelude.++) bmoves+ ((Prelude.++) opsm'+ emoves)}+ in+ case opse' of {+ [] ->+ Applicative.pure+ (State0.coq_StateT_Applicative+ mDict)+ (Blocks.setBlockOps mDict+ binfo blk ((:) b [])+ ((Prelude.++) bs opsm'')+ []);+ (:) e es ->+ 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) []))}})+ (Verify.verifyBlockEnd maxReg mDict+ opid1 useVerifier bid liveOuts))+ (Monad.concatMapM+ (State0.coq_StateT_Applicative+ mDict) k opse))+ (Class.lift+ (unsafeCoerce+ State0.coq_StateT_MonadTrans) mDict+ (State0.coq_StateT_Monad mDict)+ (generateMoves maxReg mDict oinfo+ endMoves')))+ (Verify.verifyResolutions maxReg mDict+ (Prelude.pred (Prelude.pred opid1))+ useVerifier (unsafeCoerce endMoves)))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y)+ (_assnOpId y))) mDict))+ (Monad.concatMapM+ (State0.coq_StateT_Applicative mDict) k+ opsm))+ (Class.lift+ (unsafeCoerce State0.coq_StateT_MonadTrans)+ mDict (State0.coq_StateT_Monad mDict)+ (generateMoves maxReg mDict oinfo begMoves')))+ (Verify.verifyResolutions maxReg mDict+ (Prelude.pred (Prelude.pred opid0)) useVerifier+ (unsafeCoerce begMoves)))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y) (_assnOpId y)))+ mDict))+ (Monad.concatMapM+ (State0.coq_StateT_Applicative mDict) k opsb)})+ (Verify.verifyBlockBegin maxReg mDict opid useVerifier+ bid liveIns loops);+ Prelude.Nothing ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ let {+ eg = Graph.emptyGraph (Resolve.coq_ResGraphNode maxReg)+ (Resolve.coq_ResGraphEdge_eqType maxReg)+ (unsafeCoerce (Resolve.determineEdge maxReg))}+ in+ case case IntMap.coq_IntMap_lookup bid mappings of {+ Prelude.Just graphs -> graphs;+ Prelude.Nothing -> (,) eg eg} of {+ (,) gbeg gend ->+ let {+ k = setAllocations maxReg mDict oinfo useVerifier+ allocs}+ in+ Monad.bind (State0.coq_StateT_Monad mDict) (\opsb' ->+ let {+ begMoves = Graph.topsort+ (Resolve.coq_ResGraphNode maxReg)+ (Resolve.coq_ResGraphEdge_eqType+ maxReg) gbeg+ (unsafeCoerce+ (Resolve.splitEdge maxReg))}+ in+ Monad.bind (State0.coq_StateT_Monad mDict) (\opid0 ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\begMoves' ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\bmoves ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\opsm' ->+ let {+ endMoves = Graph.topsort+ (Resolve.coq_ResGraphNode+ maxReg)+ (Resolve.coq_ResGraphEdge_eqType+ maxReg) gend+ (unsafeCoerce+ (Resolve.splitEdge maxReg))}+ in+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\opid1 ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\endMoves' ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\emoves ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\opse' ->+ Monad.bind+ (State0.coq_StateT_Monad mDict)+ (\x2 ->+ case opsb' of {+ [] ->+ let {+ opsm'' = (Prelude.++) bmoves+ ((Prelude.++) opsm'+ emoves)}+ in+ case opse' of {+ [] ->+ Applicative.pure+ (State0.coq_StateT_Applicative+ mDict)+ (Blocks.setBlockOps mDict+ binfo blk [] opsm'' []);+ (:) e es ->+ Applicative.pure+ (State0.coq_StateT_Applicative+ mDict)+ (Blocks.setBlockOps mDict+ binfo blk []+ ((Prelude.++) opsm''+ (Seq.belast e es)) ((:)+ (Seq.last e es) []))};+ (:) b bs ->+ let {+ opsm'' = (Prelude.++) bmoves+ ((Prelude.++) opsm'+ emoves)}+ in+ case opse' of {+ [] ->+ Applicative.pure+ (State0.coq_StateT_Applicative+ mDict)+ (Blocks.setBlockOps mDict+ binfo blk ((:) b [])+ ((Prelude.++) bs opsm'')+ []);+ (:) e es ->+ 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) []))}})+ (Verify.verifyBlockEnd maxReg mDict+ opid1 useVerifier bid+ IntSet.emptyIntSet))+ (Monad.concatMapM+ (State0.coq_StateT_Applicative+ mDict) k opse))+ (Class.lift+ (unsafeCoerce+ State0.coq_StateT_MonadTrans) mDict+ (State0.coq_StateT_Monad mDict)+ (generateMoves maxReg mDict oinfo+ endMoves')))+ (Verify.verifyResolutions maxReg mDict+ (Prelude.pred (Prelude.pred opid1))+ useVerifier (unsafeCoerce endMoves)))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y)+ (_assnOpId y))) mDict))+ (Monad.concatMapM+ (State0.coq_StateT_Applicative mDict) k+ opsm))+ (Class.lift+ (unsafeCoerce State0.coq_StateT_MonadTrans)+ mDict (State0.coq_StateT_Monad mDict)+ (generateMoves maxReg mDict oinfo begMoves')))+ (Verify.verifyResolutions maxReg mDict+ (Prelude.pred (Prelude.pred opid0)) useVerifier+ (unsafeCoerce begMoves)))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y) (_assnOpId y)))+ mDict))+ (Monad.concatMapM+ (State0.coq_StateT_Applicative mDict) k opsb)})+ (Verify.verifyBlockBegin maxReg mDict opid useVerifier+ bid IntSet.emptyIntSet loops)})+ (Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict+ (State0.coq_StateT_Monad mDict)+ (Blocks.blockId mDict binfo blk)))+ (Lens.modifyStateT (\_ y ->+ (Prelude..) (_verExt maxReg y) (_assnBlockEnd y))+ ((Prelude.+) opid+ (Ssrnat.double+ ((Prelude.+) (Data.List.length opsb)+ (Data.List.length opsm)))) mDict))+ (Lens.modifyStateT (\_ y ->+ (Prelude..) (_verExt maxReg y) (_assnBlockBeg y))+ ((Prelude.+) opid (Ssrnat.double (Data.List.length opsb)))+ mDict))+ (Lens.use+ (Lens.stepdownl' (\_ y ->+ (Prelude..) (_verExt maxReg y) (_assnOpId y))) mDict)}}) assignRegNum :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo - a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([]- Allocate.Allocation) -> (IntMap.IntMap- LiveSets.BlockLiveSets) -> (IntMap.IntMap Resolve.BlockMoves)- -> ([] a1) -> a5-assignRegNum maxReg mDict binfo oinfo allocs liveSets mappings blocks =- Functor.fmap (Applicative.is_functor (Monad.is_applicative mDict))- Prelude.fst- (considerOps maxReg mDict binfo oinfo allocs liveSets mappings blocks- (newAssnStateInfo maxReg))+ a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) ->+ Verify.UseVerifier -> ([] Allocate.Allocation) ->+ (IntMap.IntMap LiveSets.BlockLiveSets) -> (IntMap.IntMap+ Resolve.BlockMoves) -> Loops.LoopState -> ([] a1) -> a5+assignRegNum maxReg mDict binfo oinfo useVerifier allocs liveSets mappings loops blocks =+ Monad.bind mDict (\res ->+ case res of {+ (,) bs st ->+ Applicative.pure (Monad.is_applicative mDict) ((,)+ (Verify.verMoves maxReg st)+ (case IntMap.coq_IntMap_toList (Verify.verErrors maxReg st) of {+ [] -> Prelude.Right bs;+ (:) p l -> Prelude.Left (Verify.verErrors maxReg st)}))})+ (considerOps maxReg mDict binfo oinfo useVerifier allocs liveSets+ mappings loops blocks (Verify.newVerifiedSig maxReg newAssnStateDesc))
LinearScan/Blocks.hs view
@@ -1,6 +1,5 @@-{-# OPTIONS_GHC -cpp -XMagicHash #-}-{- For Hugs, use the option -F"cpp -P -traditional" -} + module LinearScan.Blocks where @@ -11,35 +10,12 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Monad as Monad import qualified LinearScan.UsePos as UsePos-import qualified LinearScan.Yoneda as Yoneda --#ifdef __GLASGOW_HASKELL__-import qualified GHC.Base as GHC.Base-import qualified GHC.Prim as GHC.Prim-#else--- HUGS-import qualified LinearScan.IOExts as IOExts-#endif---#ifdef __GLASGOW_HASKELL__---unsafeCoerce :: a -> b-unsafeCoerce = GHC.Base.unsafeCoerce#-#else--- HUGS---unsafeCoerce :: a -> b-unsafeCoerce = IOExts.unsafeCoerce-#endif--__ :: any-__ = Prelude.error "Logical or arity value used"- type PhysReg = Prelude.Int type VarId = Prelude.Int@@ -76,25 +52,12 @@ type OpId = Prelude.Int data OpInfo m opType1 opType2 =- Build_OpInfo (opType1 -> OpKind) (opType1 -> [] VarInfo) (PhysReg ->- PhysReg ->- Yoneda.Yoneda - m ([] opType2)) - (PhysReg -> PhysReg -> Yoneda.Yoneda m ([] opType2)) (PhysReg ->- (Prelude.Maybe - VarId) -> Yoneda.Yoneda- m ([] opType2)) - ((Prelude.Maybe VarId) -> PhysReg -> Yoneda.Yoneda m ([] opType2)) (opType1- -> ([]- ((,)- VarId- PhysReg))+ Build_OpInfo (opType1 -> OpKind) (opType1 -> [] VarInfo) (PhysReg -> VarId+ -> PhysReg -> m) + (PhysReg -> VarId -> PhysReg -> VarId -> m) (PhysReg -> VarId -> m) + (VarId -> PhysReg -> m) (opType1 -> ([] ((,) VarId PhysReg)) -> m) (opType1 ->- Yoneda.Yoneda- m- ([]- opType2)) - (opType1 -> Prelude.String)+ Prelude.String) opKind :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> a2 -> OpKind@@ -111,47 +74,45 @@ applyAllocs0 showOp -> opRefs0} moveOp :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> PhysReg ->- PhysReg -> (([] a3) -> a4) -> a1-moveOp maxReg h o x x0 x1 =+ VarId -> PhysReg -> a1+moveOp maxReg h o = case o of { Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0- applyAllocs0 showOp -> unsafeCoerce moveOp0 x x0 __ x1}+ applyAllocs0 showOp -> moveOp0} swapOp :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> PhysReg ->- PhysReg -> (([] a3) -> a4) -> a1-swapOp maxReg h o x x0 x1 =+ VarId -> PhysReg -> VarId -> a1+swapOp maxReg h o = case o of { Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0- applyAllocs0 showOp -> unsafeCoerce swapOp0 x x0 __ x1}+ applyAllocs0 showOp -> swapOp0} saveOp :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> PhysReg ->- (Prelude.Maybe VarId) -> (([] a3) -> a4) -> a1-saveOp maxReg h o x x0 x1 =+ VarId -> a1+saveOp maxReg h o = case o of { Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0- applyAllocs0 showOp -> unsafeCoerce saveOp0 x x0 __ x1}+ applyAllocs0 showOp -> saveOp0} -restoreOp :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) ->- (Prelude.Maybe VarId) -> PhysReg -> (([] a3) -> a4) -> a1-restoreOp maxReg h o x x0 x1 =+restoreOp :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> VarId ->+ PhysReg -> a1+restoreOp maxReg h o = case o of { Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0- applyAllocs0 showOp -> unsafeCoerce restoreOp0 x x0 __ x1}+ applyAllocs0 showOp -> restoreOp0} applyAllocs :: Prelude.Int -> (Monad.Monad a1) -> (OpInfo a1 a2 a3) -> a2 ->- ([] ((,) VarId PhysReg)) -> (([] a3) -> a4) -> a1-applyAllocs maxReg h o x x0 x1 =+ ([] ((,) VarId PhysReg)) -> a1+applyAllocs maxReg h o = case o of { Build_OpInfo opKind0 opRefs0 moveOp0 swapOp0 saveOp0 restoreOp0- applyAllocs0 showOp -> unsafeCoerce applyAllocs0 x x0 __ x1}+ applyAllocs0 showOp -> applyAllocs0} type BlockId = Prelude.Int data BlockInfo m blockType1 blockType2 opType1 opType2 =- Build_BlockInfo (blockType1 -> Yoneda.Yoneda m BlockId) (blockType1 ->- Yoneda.Yoneda - m ([] BlockId)) - (blockType1 -> blockType1 -> Yoneda.Yoneda m ((,) blockType1 blockType1)) + Build_BlockInfo (blockType1 -> m) (blockType1 -> m) (blockType1 ->+ blockType1 -> m) (blockType1 -> (,) ((,) ([] opType1) ([] opType1)) ([] opType1)) (blockType1 -> ([] opType2) ->@@ -161,26 +122,24 @@ opType2) -> blockType2) -blockId :: (Monad.Monad a1) -> (BlockInfo a1 a2 a3 a4 a5) -> a2 -> (BlockId- -> a6) -> a1-blockId h b x x0 =+blockId :: (Monad.Monad a1) -> (BlockInfo a1 a2 a3 a4 a5) -> a2 -> a1+blockId h b = case b of { Build_BlockInfo blockId0 blockSuccessors0 splitCriticalEdge0 blockOps0- setBlockOps0 -> unsafeCoerce blockId0 x __ x0}+ setBlockOps0 -> blockId0} -blockSuccessors :: (Monad.Monad a1) -> (BlockInfo a1 a2 a3 a4 a5) -> a2 ->- (([] BlockId) -> a6) -> a1-blockSuccessors h b x x0 =+blockSuccessors :: (Monad.Monad a1) -> (BlockInfo a1 a2 a3 a4 a5) -> a2 -> a1+blockSuccessors h b = case b of { Build_BlockInfo blockId0 blockSuccessors0 splitCriticalEdge0 blockOps0- setBlockOps0 -> unsafeCoerce blockSuccessors0 x __ x0}+ setBlockOps0 -> blockSuccessors0} splitCriticalEdge :: (Monad.Monad a1) -> (BlockInfo a1 a2 a3 a4 a5) -> a2 ->- a2 -> (((,) a2 a2) -> a6) -> a1-splitCriticalEdge h b x x0 x1 =+ a2 -> a1+splitCriticalEdge h b = case b of { Build_BlockInfo blockId0 blockSuccessors0 splitCriticalEdge0 blockOps0- setBlockOps0 -> unsafeCoerce splitCriticalEdge0 x x0 __ x1}+ setBlockOps0 -> splitCriticalEdge0} blockOps :: (Monad.Monad a1) -> (BlockInfo a1 a2 a3 a4 a5) -> a2 -> (,) ((,) ([] a4) ([] a4)) ([] a4)
LinearScan/Build.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Applicative as Applicative import qualified LinearScan.Blocks as Blocks@@ -20,7 +20,6 @@ import qualified LinearScan.IntMap as IntMap import qualified LinearScan.IntSet as IntSet import qualified LinearScan.Interval as Interval-import qualified LinearScan.Iso as Iso import qualified LinearScan.List1 as List1 import qualified LinearScan.LiveSets as LiveSets import qualified LinearScan.Logic as Logic@@ -32,7 +31,7 @@ import qualified LinearScan.ScanState as ScanState import qualified LinearScan.Specif as Specif import qualified LinearScan.UsePos as UsePos-import qualified LinearScan.Yoneda as Yoneda+import qualified LinearScan.Vector0 as Vector0 import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Fintype as Fintype import qualified LinearScan.Seq as Seq@@ -394,16 +393,16 @@ Prelude.Right v -> Prelude.True}) refs} in (Prelude.++)- (Prelude.filter (\x ->- Prelude.not- (Ssrbool.in_mem (unsafeCoerce (Blocks.varId maxReg x))- (Ssrbool.mem- (Seq.seq_predType- (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)- Ssrnat.nat_eqType))- (unsafeCoerce- (Prelude.map (Blocks.varId maxReg) refs)))))- (Seq.drop regsNeeded+ (Seq.drop regsNeeded+ (Prelude.filter (\x ->+ Prelude.not+ (Ssrbool.in_mem (unsafeCoerce (Blocks.varId maxReg x))+ (Ssrbool.mem+ (Seq.seq_predType+ (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)+ 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)@@ -488,11 +487,7 @@ in Functor.fmap (Applicative.is_functor (Monad.is_applicative mDict)) (mergeIntoSortedRanges pos0 ((Prelude.+) pos0 sz) pending)- (iHbs ((Prelude.+) pos0 sz)))- (Iso.iso_to- (Yoneda.coq_Yoneda_lemma- (Applicative.is_functor (Monad.is_applicative mDict))) (\_ ->- Blocks.blockId mDict binfo b)))}+ (iHbs ((Prelude.+) pos0 sz))) (Blocks.blockId mDict binfo b))} in let {_evar_0_1 = \_ -> iHbs pos0} in case (Prelude.<=) ((Prelude.succ) 0) sz of {@@ -513,7 +508,7 @@ _evar_0_0 = \_a_ _l_ -> let { _evar_0_0 = \_ -> (,)- (LinearScan.Utils.set_nth maxReg regs ( vid) (Prelude.Just+ (Vector0.vreplace maxReg regs ( vid) (Prelude.Just (Interval.packInterval (Interval.Build_IntervalDesc vid (Range.rbeg ( (Prelude.head (NonEmpty.coq_NE_from_list _a_ _l_))))@@ -542,8 +537,8 @@ (:) x x0 -> _evar_0_0 x x0}} in case _top_assumption_ of {- (,) x x0 -> _evar_0_ x x0}) ((,)- (Data.List.replicate maxReg Prelude.Nothing) IntMap.emptyIntMap) bs+ (,) x x0 -> _evar_0_ x x0}) ((,) (Vector0.vconst maxReg Prelude.Nothing)+ IntMap.emptyIntMap) bs buildIntervals :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([] @@ -555,8 +550,9 @@ ScanState.packScanState maxReg ScanState.Pending (ScanState.Build_ScanStateDesc ((Prelude.succ) (ScanState.nextInterval maxReg ( ss)))- (LinearScan.Utils.snoc (ScanState.nextInterval maxReg ( ss))- (ScanState.intervals maxReg ( ss)) ( i))+ (unsafeCoerce+ (Vector0.vshiftin (ScanState.nextInterval maxReg ( ss))+ (ScanState.intervals maxReg ( ss)) ( i))) (ScanState.fixedIntervals maxReg ( ss)) (List1.insert (Prelude0.lebf Prelude.snd) ((,) ( (ScanState.nextInterval maxReg ( ss))) (Interval.ibeg ( i)))@@ -569,8 +565,8 @@ [] -> Applicative.pure (Monad.is_applicative mDict) (ScanState.packScanState maxReg ScanState.InUse- (ScanState.Build_ScanStateDesc 0 []- (Data.List.replicate maxReg Prelude.Nothing) [] [] [] []));+ (ScanState.Build_ScanStateDesc 0 (unsafeCoerce Vector0.vnil)+ (Vector0.vconst maxReg Prelude.Nothing) [] [] [] [])); (:) b bs -> Monad.bind mDict (\varUses -> Monad.bind mDict (\reduced ->@@ -580,24 +576,25 @@ s2 = ScanState.packScanState maxReg ScanState.Pending (ScanState.Build_ScanStateDesc (ScanState.nextInterval maxReg- (ScanState.Build_ScanStateDesc 0 []- (Data.List.replicate maxReg Prelude.Nothing) [] [] []- []))+ (ScanState.Build_ScanStateDesc 0+ (unsafeCoerce Vector0.vnil)+ (Vector0.vconst maxReg Prelude.Nothing) [] [] [] [])) (ScanState.intervals maxReg (ScanState.Build_ScanStateDesc- 0 [] (Data.List.replicate maxReg Prelude.Nothing) [] []- [] [])) regs+ 0 (unsafeCoerce Vector0.vnil)+ (Vector0.vconst maxReg Prelude.Nothing) [] [] [] []))+ regs (ScanState.unhandled maxReg (ScanState.Build_ScanStateDesc- 0 [] (Data.List.replicate maxReg Prelude.Nothing) [] []- [] []))+ 0 (unsafeCoerce Vector0.vnil)+ (Vector0.vconst maxReg Prelude.Nothing) [] [] [] [])) (ScanState.active maxReg (ScanState.Build_ScanStateDesc 0- [] (Data.List.replicate maxReg Prelude.Nothing) [] [] []- []))+ (unsafeCoerce Vector0.vnil)+ (Vector0.vconst maxReg Prelude.Nothing) [] [] [] [])) (ScanState.inactive maxReg (ScanState.Build_ScanStateDesc 0- [] (Data.List.replicate maxReg Prelude.Nothing) [] [] []- []))+ (unsafeCoerce Vector0.vnil)+ (Vector0.vconst maxReg Prelude.Nothing) [] [] [] [])) (ScanState.handled maxReg (ScanState.Build_ScanStateDesc 0- [] (Data.List.replicate maxReg Prelude.Nothing) [] [] []- [])))}+ (unsafeCoerce Vector0.vnil)+ (Vector0.vconst maxReg Prelude.Nothing) [] [] [] [])))} in let {s3 = IntMap.coq_IntMap_foldl add_unhandled_interval s2 vars} in
LinearScan/Choice.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Ssrbool as Ssrbool
+ LinearScan/Class.hs view
@@ -0,0 +1,56 @@+{-# OPTIONS_GHC -cpp -XMagicHash #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Class 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 Hask.Utils++import qualified LinearScan.Monad as Monad++++#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+import qualified GHC.Prim as GHC.Prim+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+#endif+++#ifdef __GLASGOW_HASKELL__+--unsafeCoerce :: a -> b+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+--unsafeCoerce :: a -> b+unsafeCoerce = IOExts.unsafeCoerce+#endif+++#ifdef __GLASGOW_HASKELL__+type Any = GHC.Prim.Any+#else+-- HUGS+type Any = ()+#endif++__ :: any+__ = Prelude.error "Logical or arity value used"++type MonadTrans t =+ () -> (Monad.Monad Any) -> (Monad.Monad t) -> () -> Any -> t+ -- singleton inductive, whose constructor was Build_MonadTrans+ +lift :: (MonadTrans a1) -> (Monad.Monad a2) -> (Monad.Monad a1) -> a2 -> a1+lift monadTrans h h0 x =+ unsafeCoerce monadTrans __ h h0 __ x+
+ LinearScan/Const.hs view
@@ -0,0 +1,46 @@+{-# OPTIONS_GHC -cpp -XMagicHash #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Const 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 Hask.Utils++import qualified LinearScan.Contravariant as Contravariant+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__+type Any = GHC.Prim.Any+#else+-- HUGS+type Any = ()+#endif++type Const c a = c++coq_Const_Functor :: Functor.Functor (Const a1 Any)+coq_Const_Functor _ _ x x0 =+ x0++coq_Const_Contravariant :: Contravariant.Contravariant (Const a1 Any)+coq_Const_Contravariant _ _ x x0 =+ x0+
LinearScan/Context.hs view
@@ -10,7 +10,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils type Context errType i o a =
LinearScan/Cursor.hs view
@@ -10,11 +10,12 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Interval as Interval import qualified LinearScan.Morph as Morph import qualified LinearScan.ScanState as ScanState+import qualified LinearScan.Vector0 as Vector0 __ :: any@@ -28,7 +29,7 @@ curIntDetails :: Prelude.Int -> ScanState.ScanStateDesc -> Interval.IntervalDesc curIntDetails maxReg sd =- LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)+ Vector0.vnth (ScanState.nextInterval maxReg sd) (ScanState.intervals maxReg sd) (Prelude.fst (curId maxReg sd)) curPosition :: Prelude.Int -> ScanState.ScanStateDesc -> Prelude.Int
LinearScan/Datatypes.hs view
@@ -10,8 +10,17 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils ++nat_rect :: a1 -> (Prelude.Int -> a1 -> a1) -> Prelude.Int -> a1+nat_rect f f0 n =+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ ->+ f)+ (\n0 ->+ f0 n0 (nat_rect f f0 n0))+ n list_rect :: a2 -> (a1 -> ([] a1) -> a2 -> a2) -> ([] a1) -> a2 list_rect f f0 l =
LinearScan/Eqtype.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Ssrbool as Ssrbool import qualified LinearScan.Ssrfun as Ssrfun@@ -78,6 +78,36 @@ case t of { Equality__Mixin x x0 -> _evar_0_ x x0} +eqbP :: Equality__Coq_axiom Prelude.Bool+eqbP _top_assumption_ =+ let {+ _evar_0_ = \_top_assumption_0 ->+ let {_evar_0_ = Ssrbool.ReflectT} in+ let {_evar_0_0 = Ssrbool.ReflectF} in+ case _top_assumption_0 of {+ Prelude.True -> _evar_0_;+ Prelude.False -> _evar_0_0}}+ in+ let {+ _evar_0_0 = \_top_assumption_0 ->+ let {_evar_0_0 = Ssrbool.ReflectF} in+ let {_evar_0_1 = Ssrbool.ReflectT} in+ case _top_assumption_0 of {+ Prelude.True -> _evar_0_0;+ Prelude.False -> _evar_0_1}}+ in+ case _top_assumption_ of {+ Prelude.True -> _evar_0_;+ Prelude.False -> _evar_0_0}++bool_eqMixin :: Equality__Coq_mixin_of Prelude.Bool+bool_eqMixin =+ Equality__Mixin (Prelude.==) eqbP++bool_eqType :: Equality__Coq_type+bool_eqType =+ unsafeCoerce bool_eqMixin+ data Coq_subType t = SubType (Any -> t) (t -> () -> Any) (() -> (t -> () -> Any) -> Any -> Any) @@ -99,6 +129,11 @@ case Ssrbool.idP (p x) of { Ssrbool.ReflectT -> Prelude.Just (coq_Sub p sT x); Ssrbool.ReflectF -> Prelude.Nothing}++insubd :: (Ssrbool.Coq_pred a1) -> (Coq_subType a1) -> (Coq_sub_sort + a1) -> a1 -> Coq_sub_sort a1+insubd p sT u0 x =+ Ssrfun._Option__coq_default u0 (insub p sT x) sig_subType :: (Ssrbool.Coq_pred a1) -> Coq_subType a1 sig_subType p =
LinearScan/Fintype.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Choice as Choice import qualified LinearScan.Eqtype as Eqtype@@ -160,4 +160,15 @@ ordinal_finType n = Finite__Class (Choice._Choice__coq_class (ordinal_choiceType n)) (ordinal_finMixin n)++ord0 :: Prelude.Int -> Prelude.Int+ord0 n' =+ 0++inord :: Prelude.Int -> Prelude.Int -> Prelude.Int+inord n' m =+ unsafeCoerce+ (Eqtype.insubd (\x ->+ (Prelude.<=) ((Prelude.succ) x) ((Prelude.succ) n'))+ (ordinal_subType ((Prelude.succ) n')) (unsafeCoerce (ord0 n')) m)
LinearScan/Functor.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils
LinearScan/Graph.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Seq as Seq@@ -39,168 +39,171 @@ data Graph = Build_Graph ([] (Prelude.Maybe Eqtype.Equality__Coq_sort)) ([]- ((,)- (Prelude.Maybe- Eqtype.Equality__Coq_sort)- (Prelude.Maybe- Eqtype.Equality__Coq_sort)))+ Eqtype.Equality__Coq_sort) + (Eqtype.Equality__Coq_sort -> (,) (Prelude.Maybe Eqtype.Equality__Coq_sort)+ (Prelude.Maybe Eqtype.Equality__Coq_sort)) -vertices :: Eqtype.Equality__Coq_type -> Graph -> []- (Prelude.Maybe Eqtype.Equality__Coq_sort)-vertices a g =+vertices :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Graph+ -> [] (Prelude.Maybe Eqtype.Equality__Coq_sort)+vertices a b g = case g of {- Build_Graph vertices0 edges0 -> vertices0}+ Build_Graph vertices0 edges0 edge_f0 -> vertices0} -edges :: Eqtype.Equality__Coq_type -> Graph -> []- ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)- (Prelude.Maybe Eqtype.Equality__Coq_sort))-edges a g =+edges :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Graph ->+ [] Eqtype.Equality__Coq_sort+edges a b g = case g of {- Build_Graph vertices0 edges0 -> edges0}+ Build_Graph vertices0 edges0 edge_f0 -> edges0} -emptyGraph :: Eqtype.Equality__Coq_type -> Graph-emptyGraph a =- Build_Graph [] []+edge_f :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Graph ->+ Eqtype.Equality__Coq_sort -> (,)+ (Prelude.Maybe Eqtype.Equality__Coq_sort)+ (Prelude.Maybe Eqtype.Equality__Coq_sort)+edge_f a b g =+ case g of {+ Build_Graph vertices0 edges0 edge_f0 -> edge_f0} -addVertex :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> Graph- -> Graph-addVertex a v g =- let {vg = vertices a g} in+emptyGraph :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->+ (Eqtype.Equality__Coq_sort -> (,)+ (Prelude.Maybe Eqtype.Equality__Coq_sort)+ (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> Graph+emptyGraph a b f =+ Build_Graph [] [] f++addVertex :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->+ Eqtype.Equality__Coq_sort -> Graph -> Graph+addVertex a b v g =+ let {vg = vertices a b g} in Build_Graph (case Ssrbool.in_mem v (Ssrbool.mem (Seq.seq_predType (Eqtype.option_eqType a)) (unsafeCoerce vg)) of { Prelude.True -> vg;- Prelude.False -> (:) (unsafeCoerce v) vg}) (edges a g)+ Prelude.False -> (:) (unsafeCoerce v) vg}) (edges a b g) (edge_f a b g) -addEdge :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> Graph ->- Graph-addEdge a e g =+addEdge :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->+ Eqtype.Equality__Coq_sort -> Graph -> Graph+addEdge a b e g = let {- g' = let {eg = edges a g} in- Build_Graph (vertices a g)+ g' = let {eg = edges a b g} in+ Build_Graph (vertices a b g) (case Ssrbool.in_mem e- (Ssrbool.mem- (Seq.seq_predType- (Eqtype.prod_eqType (Eqtype.option_eqType a)- (Eqtype.option_eqType a))) (unsafeCoerce eg)) of {+ (Ssrbool.mem (Seq.seq_predType b) (unsafeCoerce eg)) of { Prelude.True -> eg;- Prelude.False -> (:) (unsafeCoerce e) eg})}+ Prelude.False -> (:) e eg}) (edge_f a b g)} in- addVertex a (Prelude.fst (unsafeCoerce e))- (addVertex a (Prelude.snd (unsafeCoerce e)) g')+ case edge_f a b g' e of {+ (,) a0 z ->+ addVertex a b (unsafeCoerce a0) (addVertex a b (unsafeCoerce z) g')} -removeEdge :: Eqtype.Equality__Coq_type -> ((,)- (Prelude.Maybe Eqtype.Equality__Coq_sort)- (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> Graph -> Graph-removeEdge a x g =- Build_Graph (vertices a g)- (Prelude.filter (\y ->- Prelude.not- (Eqtype.eq_op- (Eqtype.prod_eqType (Eqtype.option_eqType a)- (Eqtype.option_eqType a)) (unsafeCoerce y) (unsafeCoerce x)))- (edges a g))+removeEdge :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->+ Eqtype.Equality__Coq_sort -> Graph -> Graph+removeEdge a b x g =+ Build_Graph (vertices a b g)+ (Prelude.filter (\y -> Prelude.not (Eqtype.eq_op b y x)) (edges a b g))+ (edge_f a b g) -connections :: Eqtype.Equality__Coq_type -> (((,)- (Prelude.Maybe Eqtype.Equality__Coq_sort)+connections :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->+ (((,) (Prelude.Maybe Eqtype.Equality__Coq_sort) (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> Prelude.Maybe Eqtype.Equality__Coq_sort) -> (Prelude.Maybe Eqtype.Equality__Coq_sort) -> Graph -> []- ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)- (Prelude.Maybe Eqtype.Equality__Coq_sort))-connections a f x g =+ Eqtype.Equality__Coq_sort+connections a b f x g = Prelude.filter- ((Prelude..) (\y ->- Eqtype.eq_op (Eqtype.option_eqType a) (unsafeCoerce y) (unsafeCoerce x))- f) (edges a g)+ ((Prelude..)+ ((Prelude..) (\y ->+ Eqtype.eq_op (Eqtype.option_eqType a) (unsafeCoerce y)+ (unsafeCoerce x)) f) (edge_f a b g)) (edges a b g) -outbound :: Eqtype.Equality__Coq_type -> (Prelude.Maybe- Eqtype.Equality__Coq_sort) -> Graph -> []- ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)- (Prelude.Maybe Eqtype.Equality__Coq_sort))-outbound a =- connections a Prelude.fst+outbound :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->+ (Prelude.Maybe Eqtype.Equality__Coq_sort) -> Graph -> []+ Eqtype.Equality__Coq_sort+outbound a b =+ connections a b Prelude.fst -inbound :: Eqtype.Equality__Coq_type -> (Prelude.Maybe- Eqtype.Equality__Coq_sort) -> Graph -> []- ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)- (Prelude.Maybe Eqtype.Equality__Coq_sort))-inbound a =- connections a Prelude.snd+inbound :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->+ (Prelude.Maybe Eqtype.Equality__Coq_sort) -> Graph -> []+ Eqtype.Equality__Coq_sort+inbound a b =+ connections a b Prelude.snd -tsort' :: Eqtype.Equality__Coq_type -> Prelude.Int -> ([]- ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)- (Prelude.Maybe Eqtype.Equality__Coq_sort))) -> ([]- (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> Graph -> []- ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)- (Prelude.Maybe Eqtype.Equality__Coq_sort))-tsort' a fuel l roots g =+tsort' :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type ->+ Prelude.Int -> ([] Eqtype.Equality__Coq_sort) -> ([]+ (Prelude.Maybe Eqtype.Equality__Coq_sort)) ->+ (Eqtype.Equality__Coq_sort -> [] Eqtype.Equality__Coq_sort) ->+ Graph -> [] Eqtype.Equality__Coq_sort+tsort' a b fuel l roots k g = (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1)) (\_ -> Seq.rev l) (\fuel0 ->- case edges a g of {+ case edges a b g of { [] -> Seq.rev l;- (:) p es ->- case p of {- (,) se de ->- case roots of {- [] ->- let {l0 = (:) de []} in- let {- g' = addEdge a (unsafeCoerce ((,) se Prelude.Nothing))- (removeEdge a ((,) se de) g)}- in- case l0 of {- [] -> [];- (:) n s ->- let {outEdges = outbound a n g'} in- case Data.List.foldl' (\acc e ->- case acc of {- (,) res g'' -> (,) ((:) e res) (removeEdge a e g'')})- ((,) [] g') outEdges of {- (,) res g'' ->- let {outNodes = Prelude.map Prelude.snd outEdges} in- let {- s' = (Prelude.++) s- (Prelude.filter- ((Prelude..) Seq.nilp (\x -> inbound a x g''))- outNodes)}- in- tsort' a fuel0 ((Prelude.++) l res) s' g''}};+ (:) e es ->+ case roots of {+ [] ->+ let {l0 = (:) (Prelude.snd (edge_f a b g e)) []} in+ let {g' = Prelude.foldr (addEdge a b) (removeEdge a b e g) (k e)} in+ case l0 of {+ [] -> []; (:) n s ->- let {l0 = (:) n s} in- case l0 of {- [] -> [];- (:) n0 s0 ->- let {outEdges = outbound a n0 g} in- case Data.List.foldl' (\acc e ->- case acc of {- (,) res g'' -> (,) ((:) e res) (removeEdge a e g'')})- ((,) [] g) outEdges of {- (,) res g'' ->- let {outNodes = Prelude.map Prelude.snd outEdges} in- let {- s' = (Prelude.++) s0- (Prelude.filter- ((Prelude..) Seq.nilp (\x -> inbound a x g''))- outNodes)}- in- tsort' a fuel0 ((Prelude.++) l res) s' g''}}}}})+ let {outEdges = outbound a b n g'} in+ case Data.List.foldl' (\acc e0 ->+ case acc of {+ (,) res g'' -> (,) ((:) e0 res) (removeEdge a b e0 g'')})+ ((,) [] g') outEdges of {+ (,) res g'' ->+ let {+ outNodes = Prelude.map ((Prelude..) Prelude.snd (edge_f a b g))+ outEdges}+ in+ let {+ s' = (Prelude.++) s+ (Prelude.filter+ ((Prelude..) Seq.nilp (\x -> inbound a b x g''))+ outNodes)}+ in+ tsort' a b fuel0 ((Prelude.++) l res) s' k g''}};+ (:) n s ->+ let {l0 = (:) n s} in+ case l0 of {+ [] -> [];+ (:) n0 s0 ->+ let {outEdges = outbound a b n0 g} in+ case Data.List.foldl' (\acc e0 ->+ case acc of {+ (,) res g'' -> (,) ((:) e0 res) (removeEdge a b e0 g'')})+ ((,) [] g) outEdges of {+ (,) res g'' ->+ let {+ outNodes = Prelude.map ((Prelude..) Prelude.snd (edge_f a b g))+ outEdges}+ in+ let {+ s' = (Prelude.++) s0+ (Prelude.filter+ ((Prelude..) Seq.nilp (\x -> inbound a b x g''))+ outNodes)}+ in+ tsort' a b fuel0 ((Prelude.++) l res) s' k g''}}}}) fuel -topsort :: Eqtype.Equality__Coq_type -> Graph -> []- ((,) (Prelude.Maybe Eqtype.Equality__Coq_sort)- (Prelude.Maybe Eqtype.Equality__Coq_sort))-topsort a g =+topsort :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Graph ->+ (Eqtype.Equality__Coq_sort -> [] Eqtype.Equality__Coq_sort) -> []+ Eqtype.Equality__Coq_sort+topsort a b g k = let {- noInbound = let {xs = Prelude.map Prelude.snd (edges a g)} in+ noInbound = let {+ xs = Prelude.map ((Prelude..) Prelude.snd (edge_f a b g))+ (edges a b g)}+ in Prelude.filter (\x -> Prelude.not (Ssrbool.in_mem (unsafeCoerce x) (Ssrbool.mem (Seq.seq_predType (Eqtype.option_eqType a))- (unsafeCoerce xs)))) (vertices a g)}+ (unsafeCoerce xs)))) (vertices a b g)} in- tsort' a ((Prelude.succ) (Data.List.length (vertices a g))) [] noInbound g+ tsort' a b ((Prelude.succ) (Data.List.length (vertices a b g))) []+ noInbound k g
+ LinearScan/Identity.hs view
@@ -0,0 +1,41 @@+{-# OPTIONS_GHC -cpp -XMagicHash #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Identity 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 Hask.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__+type Any = GHC.Prim.Any+#else+-- HUGS+type Any = ()+#endif++type Identity a = a++coq_Identity_Functor :: Functor.Functor (Identity Any)+coq_Identity_Functor _ _ x =+ x+
LinearScan/IntMap.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.List1 as List1 import qualified LinearScan.Eqtype as Eqtype@@ -96,7 +96,7 @@ coq_IntMap_mergeWithKey combine only1 only2 m1 m2 = let {only1' = \xs -> only1 xs} in let {only2' = \xs -> only2 xs} in- LinearScan.Utils.intMap_mergeWithKey' combine only1' only2' m1 m2+ Hask.Utils.intMap_mergeWithKey' combine only1' only2' m1 m2 coq_IntMap_foldl :: (a1 -> a2 -> a1) -> a1 -> (IntMap a2) -> a1 coq_IntMap_foldl f z m =
LinearScan/IntSet.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Seq as Seq
LinearScan/Interval.hs view
@@ -1,4 +1,5 @@-+{-# OPTIONS_GHC -cpp -XMagicHash #-}+{- For Hugs, use the option -F"cpp -P -traditional" -} module LinearScan.Interval where @@ -10,18 +11,40 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.List1 as List1 import qualified LinearScan.Logic as Logic+import qualified LinearScan.Maybe as Maybe 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+import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Seq as Seq+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" @@ -70,19 +93,32 @@ (Prelude.&&) ((Prelude.<=) (intervalStart d) pos) ((Prelude.<=) ((Prelude.succ) pos) (intervalEnd d)) +intervalOverlapPoint :: IntervalDesc -> IntervalDesc -> Prelude.Maybe+ Prelude0.Coq_oddnum+intervalOverlapPoint x y =+ Data.List.foldl' (\mx rd ->+ Maybe.option_choose mx+ (Data.List.foldl' (\mx' rd' ->+ Maybe.option_choose mx (Range.rangeIntersectionPoint ( rd) ( rd')))+ Prelude.Nothing (rds y))) Prelude.Nothing (rds x)+ intervalsIntersect :: IntervalDesc -> IntervalDesc -> Prelude.Bool-intervalsIntersect i j =- let {f = \x y -> Range.rangesIntersect ( x) ( y)} in- Data.List.any (\x -> Data.List.any (f x) ( (rds j))) ( (rds i))+intervalsIntersect x y =+ (Prelude.||)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (iend x))+ (unsafeCoerce (iend y)))+ ((Prelude.&&) ((Prelude.<=) ((Prelude.succ) (ibeg x)) (iend y))+ ((Prelude.<=) ((Prelude.succ) (ibeg y)) (iend x))) intervalIntersectionPoint :: IntervalDesc -> IntervalDesc -> Prelude.Maybe Prelude0.Coq_oddnum-intervalIntersectionPoint i j =- Data.List.foldl' (\mx rd ->- Prelude0.option_choose mx- (Data.List.foldl' (\mx' rd' ->- Prelude0.option_choose mx (Range.rangeIntersectionPoint ( rd) ( rd')))- Prelude.Nothing (rds j))) Prelude.Nothing (rds i)+intervalIntersectionPoint x y =+ case intervalsIntersect (getIntervalDesc x) (getIntervalDesc y) of {+ Prelude.True -> Prelude.Just+ (case (Prelude.<=) ((Prelude.succ) (ibeg x)) (ibeg y) of {+ Prelude.True -> ibeg y;+ Prelude.False -> ibeg x});+ Prelude.False -> Prelude.Nothing} findIntervalUsePos :: IntervalDesc -> (UsePos.UsePos -> Prelude.Bool) -> Prelude.Maybe@@ -162,7 +198,7 @@ (\x -> rangeFirstUsePos ( x)) (\x xs0 ->- Prelude0.option_choose (rangeFirstUsePos ( x)) (go xs0))+ Maybe.option_choose (rangeFirstUsePos ( x)) (go xs0)) xs} in go (rds d) @@ -174,7 +210,7 @@ (\x -> List1.olast (Range.ups ( x))) (\x xs0 ->- Prelude0.option_choose (go xs0) (List1.olast (Range.ups ( x))))+ Maybe.option_choose (go xs0) (List1.olast (Range.ups ( x)))) xs} in go (rds d)
− LinearScan/Iso.hs
@@ -1,23 +0,0 @@---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
@@ -11,9 +11,16 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils +import qualified LinearScan.Applicative as Applicative+import qualified LinearScan.Const as Const+import qualified LinearScan.Contravariant as Contravariant import qualified LinearScan.Functor as Functor+import qualified LinearScan.Identity as Identity+import qualified LinearScan.Monad as Monad+import qualified LinearScan.Prelude0 as Prelude0+import qualified LinearScan.State0 as State0 @@ -46,27 +53,65 @@ __ :: any __ = Prelude.error "Logical or arity value used" -type Identity a = a--coq_Identity_Functor :: Functor.Functor (Identity Any)-coq_Identity_Functor _ _ x =- x--type Const c a = c--coq_Const_Functor :: Functor.Functor (Const a1 Any)-coq_Const_Functor _ _ x x0 =- x0- type Lens s t a b = () -> (Functor.Functor Any) -> (a -> Any) -> s -> Any type Lens' s a = Lens s s a a +type Getter s a =+ () -> (Functor.Functor Any) -> (Contravariant.Contravariant Any) -> (a ->+ Any) -> s -> Any++type Getting r s a = (a -> Const.Const r a) -> s -> Const.Const r s+ set :: (Lens a1 a2 a3 a4) -> a4 -> a1 -> a2 set l x =- unsafeCoerce l __ coq_Identity_Functor (\x0 -> x)+ unsafeCoerce l __ Identity.coq_Identity_Functor (Prelude0.const x) -view :: (Lens' a1 a2) -> a1 -> a2+over :: (Lens a1 a2 a3 a4) -> (a3 -> a4) -> a1 -> a2+over l x =+ unsafeCoerce l __ Identity.coq_Identity_Functor x++view :: (Getting a1 a2 a1) -> a2 -> a1 view f =- unsafeCoerce f __ coq_Const_Functor (\x -> x)+ f (\x -> x)++stepdownl' :: (Lens' a1 a2) -> Getting a2 a1 a2+stepdownl' l =+ unsafeCoerce l __ Const.coq_Const_Functor++stepdowng :: (Getter a1 a2) -> Getting a2 a1 a2+stepdowng l =+ unsafeCoerce l __ Const.coq_Const_Functor Const.coq_Const_Contravariant++_1 :: (Functor.Functor a3) -> (a1 -> a3) -> ((,) a1 a2) -> a3+_1 h f s =+ case s of {+ (,) x y -> Functor.fmap h (\z -> (,) z y) (f x)}++_2 :: (Functor.Functor a3) -> (a2 -> a3) -> ((,) a1 a2) -> a3+_2 h f s =+ case s of {+ (,) x y -> Functor.fmap h (\z -> (,) x z) (f y)}++use :: (Getting a1 a2 a1) -> (Monad.Monad a3) -> State0.StateT a2 a3 a1+use l h =+ Functor.fmap+ (State0.coq_StateT_Functor+ (Applicative.is_functor (Monad.is_applicative h))) (view l)+ (State0.getT (Monad.is_applicative h))++plusStateT :: (Lens' a1 Prelude.Int) -> Prelude.Int -> (Monad.Monad a2) ->+ State0.StateT a1 a2 ()+plusStateT l n h =+ State0.modifyT (Monad.is_applicative h) (over l ((Prelude.+) n))++modifyStateT :: (Lens' a1 a2) -> a2 -> (Monad.Monad a3) -> State0.StateT + a1 a3 ()+modifyStateT l x h =+ State0.modifyT (Monad.is_applicative h) (set l x)++applyStateT :: (Lens' a1 a2) -> (a2 -> a2) -> (Monad.Monad a3) ->+ State0.StateT a1 a3 ()+applyStateT l f h =+ State0.modifyT (Monad.is_applicative h) (over l f)
LinearScan/Lib.hs view
@@ -10,7 +10,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Specif as Specif import qualified LinearScan.Eqtype as Eqtype
LinearScan/List0.hs view
@@ -10,6 +10,6 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils
LinearScan/List1.hs view
@@ -10,7 +10,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Eqtype as Eqtype @@ -50,16 +50,15 @@ 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 ->+ let {+ f = \mx rest -> case mx of { Prelude.Just x -> (:) x rest;- Prelude.Nothing -> rest})+ Prelude.Nothing -> rest}}+ in+ Prelude.foldr f [] l span :: (a1 -> Prelude.Bool) -> ([] a1) -> (,) ([] a1) ([] a1) span p l =
LinearScan/LiveSets.hs view
@@ -11,18 +11,16 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.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.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 import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Ssrbool as Ssrbool import qualified LinearScan.Ssrnat as Ssrnat@@ -228,123 +226,106 @@ a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> a5 computeLocalLiveSets maxReg mDict binfo oinfo blocks =- 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 {- (,) idx m ->- case Blocks.blockOps mDict binfo b of {- (,) p opse ->- case p of {- (,) opsb opsm ->- let {- liveSet = Build_BlockLiveSets IntSet.emptyIntSet- IntSet.emptyIntSet IntSet.emptyIntSet IntSet.emptyIntSet- ((Prelude.+) idx (Ssrnat.double (Data.List.length opsb)))- idx}- in- case List1.forFold ((,) idx liveSet)- ((Prelude.++) opsb ((Prelude.++) opsm opse)) (\acc0 o ->- case acc0 of {- (,) lastIdx liveSet1 -> (,) ((Prelude.succ)- ((Prelude.succ) lastIdx))- (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 = List1.forFold liveSet1 inputs- (\liveSet2 v ->- case Blocks.varId maxReg v of {- Prelude.Left p0 -> liveSet2;- Prelude.Right vid ->- case Prelude.not- (IntSet.coq_IntSet_member- vid- (blockLiveKill liveSet2)) of {- Prelude.True ->- Build_BlockLiveSets- (IntSet.coq_IntSet_insert vid- (blockLiveGen liveSet2))- (blockLiveKill liveSet2)- (blockLiveIn liveSet2)- (blockLiveOut liveSet2)- (blockFirstOpId liveSet2) lastIdx;- Prelude.False -> liveSet2}})}- in- let {- liveSet3 = List1.forFold liveSet2 others- (\liveSet3 v ->- case Blocks.varId maxReg v of {- Prelude.Left p0 -> liveSet3;- Prelude.Right vid ->- Build_BlockLiveSets- (blockLiveGen liveSet3)+ Functor.fmap (Applicative.is_functor (Monad.is_applicative mDict))+ Prelude.snd+ (Monad.forFoldM mDict ((,) ((Prelude.succ) 0) IntMap.emptyIntMap) blocks+ (\acc b ->+ case acc of {+ (,) idx m ->+ case Blocks.blockOps mDict binfo b of {+ (,) p opse ->+ case p of {+ (,) opsb opsm ->+ let {+ liveSet = Build_BlockLiveSets IntSet.emptyIntSet+ IntSet.emptyIntSet IntSet.emptyIntSet IntSet.emptyIntSet+ ((Prelude.+) idx (Ssrnat.double (Data.List.length opsb))) idx}+ in+ case List1.forFold ((,) idx liveSet)+ ((Prelude.++) opsb ((Prelude.++) opsm opse)) (\acc0 o ->+ case acc0 of {+ (,) lastIdx liveSet1 -> (,) ((Prelude.succ)+ ((Prelude.succ) lastIdx))+ (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 = List1.forFold liveSet1 inputs+ (\liveSet2 v ->+ case Blocks.varId maxReg v of {+ Prelude.Left p0 -> liveSet2;+ Prelude.Right vid ->+ case Prelude.not+ (IntSet.coq_IntSet_member vid+ (blockLiveKill liveSet2)) of {+ Prelude.True -> Build_BlockLiveSets (IntSet.coq_IntSet_insert vid- (blockLiveKill liveSet3))- (blockLiveIn liveSet3)- (blockLiveOut liveSet3)- (blockFirstOpId liveSet3) lastIdx})}- in- Build_BlockLiveSets (blockLiveGen liveSet3)- (blockLiveKill liveSet3) (blockLiveIn liveSet3)- (blockLiveOut liveSet3) (blockFirstOpId liveSet3)- lastIdx})}) of {- (,) lastIdx' liveSet3 ->- Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict))- (\k ->- Applicative.pure- (unsafeCoerce- (Yoneda.coq_Yoneda_Applicative- (Monad.is_applicative mDict))) ((,) lastIdx'- (IntMap.coq_IntMap_insert k liveSet3 m))) (\_ ->- Blocks.blockId mDict binfo b)}}}})))+ (blockLiveGen liveSet2))+ (blockLiveKill liveSet2)+ (blockLiveIn liveSet2)+ (blockLiveOut liveSet2)+ (blockFirstOpId liveSet2) lastIdx;+ Prelude.False -> liveSet2}})}+ in+ let {+ liveSet3 = List1.forFold liveSet2 others+ (\liveSet3 v ->+ case Blocks.varId maxReg v of {+ Prelude.Left p0 -> liveSet3;+ Prelude.Right vid ->+ Build_BlockLiveSets+ (blockLiveGen liveSet3)+ (IntSet.coq_IntSet_insert vid+ (blockLiveKill liveSet3))+ (blockLiveIn liveSet3)+ (blockLiveOut liveSet3)+ (blockFirstOpId liveSet3) lastIdx})}+ in+ Build_BlockLiveSets (blockLiveGen liveSet3)+ (blockLiveKill liveSet3) (blockLiveIn liveSet3)+ (blockLiveOut liveSet3) (blockFirstOpId liveSet3)+ lastIdx})}) of {+ (,) lastIdx' liveSet3 ->+ Monad.bind mDict (\k ->+ Applicative.pure (Monad.is_applicative mDict) ((,) lastIdx'+ (IntMap.coq_IntMap_insert k liveSet3 m)))+ (Blocks.blockId mDict binfo b)}}}})) computeGlobalLiveSets :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> ([] a1) -> (IntMap.IntMap BlockLiveSets) -> a5 computeGlobalLiveSets mDict binfo blocks liveSets =- 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 ->- case IntMap.coq_IntMap_lookup bid liveSets1 of {- Prelude.Just liveSet ->- Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\suxs ->- let {- 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)- (IntSet.coq_IntSet_union (blockLiveOut liveSet2)- (blockLiveIn sux)) (blockFirstOpId liveSet2)- (blockLastOpId liveSet2);- Prelude.Nothing -> liveSet2})}- in- Applicative.pure- (unsafeCoerce- (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))- (IntMap.coq_IntMap_insert bid (Build_BlockLiveSets- (blockLiveGen liveSet2) (blockLiveKill 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 ->- Applicative.pure- (unsafeCoerce- (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))- liveSets1}) (\_ -> Blocks.blockId mDict binfo b)))+ Monad.forFoldrM mDict liveSets blocks (\b liveSets1 ->+ Monad.bind mDict (\bid ->+ case IntMap.coq_IntMap_lookup bid liveSets1 of {+ Prelude.Just liveSet ->+ Monad.bind mDict (\suxs ->+ let {+ 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)+ (IntSet.coq_IntSet_union (blockLiveOut liveSet2)+ (blockLiveIn sux)) (blockFirstOpId liveSet2)+ (blockLastOpId liveSet2);+ Prelude.Nothing -> liveSet2})}+ in+ Applicative.pure (Monad.is_applicative mDict)+ (IntMap.coq_IntMap_insert bid (Build_BlockLiveSets+ (blockLiveGen liveSet2) (blockLiveKill liveSet2)+ (IntSet.coq_IntSet_union+ (IntSet.coq_IntSet_difference (blockLiveOut liveSet2)+ (blockLiveKill liveSet2)) (blockLiveGen liveSet2))+ (blockLiveOut liveSet2) (blockFirstOpId liveSet2)+ (blockLastOpId liveSet2)) liveSets1))+ (Blocks.blockSuccessors mDict binfo b);+ Prelude.Nothing ->+ Applicative.pure (Monad.is_applicative mDict) liveSets1})+ (Blocks.blockId mDict binfo b)) computeGlobalLiveSetsRecursively :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> ([] a1) ->
LinearScan/Logic.hs view
@@ -10,7 +10,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils coq_False_rect :: a1
LinearScan/Loops.hs view
@@ -11,19 +11,18 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Applicative as Applicative import qualified LinearScan.Blocks as Blocks+import qualified LinearScan.Class as Class import qualified LinearScan.Functor as Functor import qualified LinearScan.IntMap as IntMap 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 import qualified LinearScan.Ssrbool as Ssrbool@@ -263,81 +262,64 @@ setLoopDepths (IntMap.coq_IntMap_foldlWithKey f IntMap.emptyIntMap m)) (setLoopIndices m)))- (State0.lift 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 (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 ->- Applicative.pure- (unsafeCoerce- (Yoneda.coq_Yoneda_Applicative- (Monad.is_applicative mDict)))- (List1.forFold m suxs (\m' sux ->- let {headers = loopHeaderBlocks st} in+ (Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict+ (State0.coq_StateT_Monad mDict)+ (Monad.forFoldM mDict IntMap.emptyIntMap+ (IntSet.coq_IntSet_toList (loopEndBlocks st)) (\m endBlock ->+ case IntMap.coq_IntMap_lookup endBlock bs of {+ Prelude.Just b ->+ Monad.bind mDict (\suxs ->+ Applicative.pure (Monad.is_applicative mDict)+ (List1.forFold m suxs (\m' sux ->+ let {headers = loopHeaderBlocks st} in+ let {+ loopIndex = Seq.find (\x ->+ Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce x) sux) headers}+ in+ case Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce loopIndex)+ (unsafeCoerce (Data.List.length headers)) of {+ Prelude.True -> m';+ Prelude.False -> let {- loopIndex = Seq.find (\x ->- Eqtype.eq_op Ssrnat.nat_eqType- (unsafeCoerce x) sux) headers}+ mres = pathToLoopHeader endBlock (unsafeCoerce sux) st} in- case Eqtype.eq_op Ssrnat.nat_eqType- (unsafeCoerce loopIndex)- (unsafeCoerce (Data.List.length headers)) of {- Prelude.True -> m';- Prelude.False ->- let {- mres = pathToLoopHeader endBlock (unsafeCoerce sux) st}- in- case mres of {- Prelude.Just path ->- List1.forFold m' (IntSet.coq_IntSet_toList path)- (\m'' blk -> addReference loopIndex blk m'');- Prelude.Nothing -> m'}}))) (\_ ->- Blocks.blockSuccessors mDict binfo b);- Prelude.Nothing ->- Applicative.pure- (unsafeCoerce- (Yoneda.coq_Yoneda_Applicative- (Monad.is_applicative mDict))) m})))))+ case mres of {+ Prelude.Just 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 -> Applicative.pure (Monad.is_applicative mDict) m})))) (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 =- 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 (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 ->- List1.forFold acc1 ((Prelude.++) xs ((Prelude.++) ys zs))- (\acc2 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- Applicative.pure- (unsafeCoerce- (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))- (IntMap.coq_IntMap_foldlWithKey g acc (loopIndices st))) (\_ ->- Blocks.blockId mDict binfo b)))+ Monad.forFoldM mDict IntMap.emptyIntMap bs (\acc b ->+ Monad.bind mDict (\bid ->+ let {+ g = \acc1 loopIndex blks ->+ 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 ->+ List1.forFold acc1 ((Prelude.++) xs ((Prelude.++) ys zs))+ (\acc2 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+ Applicative.pure (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) -> State0.StateT LoopState a5 ()@@ -399,21 +381,16 @@ modifyForwardBranches (addReference sux bid)}))) (State0.getsT (Monad.is_applicative mDict) activeBlocks))))- (State0.lift mDict- (Iso.iso_to- (Yoneda.coq_Yoneda_lemma- (Applicative.is_functor- (Monad.is_applicative mDict))) (\_ ->- Blocks.blockSuccessors mDict binfo b))))+ (Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans)+ mDict (State0.coq_StateT_Monad 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- (Applicative.is_functor (Monad.is_applicative mDict)))- (\_ -> Blocks.blockId mDict binfo b))))+ (Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict+ (State0.coq_StateT_Monad mDict)+ (Blocks.blockId mDict binfo b))) n} in go} in@@ -471,17 +448,8 @@ in Applicative.pure (Monad.is_applicative mDict) ((Prelude.<=) ((Prelude.succ) y_depth)- x_depth))- (Iso.iso_to- (Yoneda.coq_Yoneda_lemma- (Applicative.is_functor- (Monad.is_applicative mDict))) (\_ ->- Blocks.blockId mDict binfo y2)))- (Iso.iso_to- (Yoneda.coq_Yoneda_lemma- (Applicative.is_functor- (Monad.is_applicative mDict))) (\_ ->- Blocks.blockId mDict binfo x))}+ x_depth)) (Blocks.blockId mDict binfo y2))+ (Blocks.blockId mDict binfo x)} in let { go = let {@@ -545,19 +513,9 @@ Applicative.pure (Monad.is_applicative mDict) ws'})})))- (Iso.iso_to- (Yoneda.coq_Yoneda_lemma- (Applicative.is_functor- (Monad.is_applicative mDict)))- (\_ ->- Blocks.blockSuccessors mDict binfo- w0)))- (Iso.iso_to- (Yoneda.coq_Yoneda_lemma- (Applicative.is_functor- (Monad.is_applicative mDict)))- (\_ ->- Blocks.blockId mDict binfo w0))})+ (Blocks.blockSuccessors mDict binfo+ w0))+ (Blocks.blockId mDict binfo w0)}) n} in go} in@@ -571,10 +529,7 @@ (Monad.mapM (Monad.is_applicative mDict) (\x -> Monad.bind mDict (\bid -> Applicative.pure (Monad.is_applicative mDict) ((,) bid x))- (Iso.iso_to- (Yoneda.coq_Yoneda_lemma- (Applicative.is_functor (Monad.is_applicative mDict)))- (\_ -> Blocks.blockId mDict binfo x))) blocks'))+ (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 {@@ -616,24 +571,14 @@ (,) b'' sux'' -> Applicative.pure (Monad.is_applicative mDict) ((,) b'' ((:) sux'' rest'))})- (Iso.iso_to- (Yoneda.coq_Yoneda_lemma- (Applicative.is_functor- (Monad.is_applicative mDict))) (\_ ->- Blocks.splitCriticalEdge mDict binfo b' sux'));+ (Blocks.splitCriticalEdge mDict binfo b' sux'); Prelude.Nothing -> Applicative.pure (Monad.is_applicative mDict) ((,) b' rest')}}}))})- (Iso.iso_to- (Yoneda.coq_Yoneda_lemma- (Applicative.is_functor (Monad.is_applicative mDict)))- (\_ -> Blocks.blockSuccessors mDict binfo b0))))})+ (Blocks.blockSuccessors mDict binfo b0)))}) (findLoopEnds mDict binfo blockMap emptyLoopState)) (Monad.mapM (Monad.is_applicative mDict) (\x -> Monad.bind mDict (\bid -> Applicative.pure (Monad.is_applicative mDict) ((,) bid x))- (Iso.iso_to- (Yoneda.coq_Yoneda_lemma- (Applicative.is_functor (Monad.is_applicative mDict))) (\_ ->- Blocks.blockId mDict binfo x))) blocks)}+ (Blocks.blockId mDict binfo x)) blocks)}
LinearScan/Main.hs view
@@ -10,7 +10,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Allocate as Allocate import qualified LinearScan.Applicative as Applicative@@ -21,11 +21,13 @@ import qualified LinearScan.Interval as Interval import qualified LinearScan.LiveSets as LiveSets import qualified LinearScan.Loops as Loops+import qualified LinearScan.Maybe as Maybe import qualified LinearScan.Monad as Monad-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.Vector0 as Vector0+import qualified LinearScan.Verify as Verify import qualified LinearScan.Ssrnat as Ssrnat @@ -46,13 +48,14 @@ ScanStateDescSet toScanStateDescSet maxReg sd = Build_ScanStateDescSet (ScanState.nextInterval maxReg sd)- (LinearScan.Utils.vmap (ScanState.nextInterval maxReg sd) (\x ->- Interval.getIntervalDesc ( x)) (ScanState.intervals maxReg sd))- (LinearScan.Utils.vmap maxReg (\mx ->+ (Prelude.map (\x -> Interval.getIntervalDesc ( x))+ (Vector0.vec_to_seq (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd)))+ (Prelude.map (\mx -> case mx of { Prelude.Just x -> Prelude.Just (Interval.getIntervalDesc ( x)); Prelude.Nothing -> Prelude.Nothing})- (ScanState.fixedIntervals maxReg sd))+ (Vector0.vec_to_seq maxReg (ScanState.fixedIntervals maxReg sd))) (Prelude.map (\i -> (,) ( (Prelude.fst i)) (Prelude.snd i)) (ScanState.unhandled maxReg sd)) (Prelude.map (\i -> (,) ( (Prelude.fst i)) ( (Prelude.snd i)))@@ -60,19 +63,24 @@ (Prelude.map (\i -> (,) ( (Prelude.fst i)) ( (Prelude.snd i))) (ScanState.inactive maxReg sd)) (Prelude.map (\i -> (,) ( (Prelude.fst i))- (Prelude0.option_map (\x -> x) (Prelude.snd i)))+ (Maybe.option_map (\x -> x) (Prelude.snd i))) (ScanState.handled maxReg sd)) data Details blockType1 blockType2 = Build_Details (Prelude.Maybe ((,) ([] Trace.SSTrace) FinalStage)) - (IntMap.IntMap LiveSets.BlockLiveSets) ([] blockType1) ([] blockType1) - ([] blockType2) (Prelude.Maybe ScanStateDescSet) (Prelude.Maybe- ScanStateDescSet) Loops.LoopState+ (IntMap.IntMap LiveSets.BlockLiveSets) (IntMap.IntMap+ ([] Resolve.ResolvingMoveSet)) + ([] blockType1) ([] blockType1) (Prelude.Either+ (IntMap.IntMap ([] Verify.AllocError))+ ([] 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) ->- ((Details a2 a3) -> a6) -> a1-linearScan dict maxReg binfo oinfo blocks k =+ a2 a3 a4 a5) -> (Blocks.OpInfo a1 a4 a5) -> Verify.UseVerifier+ -> ([] a2) -> a1+linearScan dict maxReg binfo oinfo useVerifier blocks = Monad.bind dict (\z -> case z of { (,) loops blocks1 ->@@ -86,12 +94,11 @@ 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))};+ Applicative.pure (Monad.is_applicative dict) (Build_Details+ (Prelude.Just ((,) err AllocatingRegistersFailed))+ liveSets' IntMap.emptyIntMap blocks blocks1 (Prelude.Right+ []) (Prelude.Just (toScanStateDescSet maxReg ( ssig)))+ (Prelude.Just (toScanStateDescSet maxReg ( ssig'))) loops)}; Prelude.Right ssig' -> let { sd = Allocate.finalizeScanState maxReg ( ssig')@@ -99,14 +106,16 @@ in 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+ Monad.bind dict (\res ->+ case res of {+ (,) moves blocks2 ->+ Applicative.pure (Monad.is_applicative dict)+ (Build_Details Prelude.Nothing liveSets' moves blocks blocks1 blocks2 (Prelude.Just (toScanStateDescSet maxReg ( ssig))) (Prelude.Just- (toScanStateDescSet maxReg sd)) loops)))- (Assign.assignRegNum maxReg dict binfo oinfo allocs- liveSets' mappings blocks1))+ (toScanStateDescSet maxReg sd)) loops)})+ (Assign.assignRegNum maxReg dict binfo oinfo useVerifier+ allocs liveSets' mappings loops blocks1)) (Resolve.resolveDataFlow maxReg dict binfo allocs blocks1 liveSets')}) (Build.buildIntervals maxReg dict binfo oinfo blocks1 loops
LinearScan/Monad.hs view
@@ -10,7 +10,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Applicative as Applicative import qualified LinearScan.Functor as Functor@@ -37,6 +37,22 @@ bind h f = (Prelude..) (join h) (Functor.fmap (Applicative.is_functor (is_applicative h)) f)++return_ :: (Monad a1) -> a2 -> a1+return_ h =+ Applicative.pure (is_applicative h)++when :: (Monad a1) -> Prelude.Bool -> a1 -> a1+when h b x =+ case b of {+ Prelude.True -> x;+ Prelude.False -> return_ h ()}++unless :: (Monad a1) -> Prelude.Bool -> a1 -> a1+unless h b x =+ case Prelude.not b of {+ Prelude.True -> x;+ Prelude.False -> return_ h ()} mapM :: (Applicative.Applicative a1) -> (a2 -> a1) -> ([] a2) -> a1 mapM h f l =
LinearScan/Morph.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Context as Context import qualified LinearScan.Interval as Interval@@ -19,6 +19,7 @@ import qualified LinearScan.ScanState as ScanState import qualified LinearScan.Specif as Specif import qualified LinearScan.Trace as Trace+import qualified LinearScan.Vector0 as Vector0 import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Fintype as Fintype import qualified LinearScan.Seq as Seq@@ -149,17 +150,14 @@ (Prelude.&&) ((Prelude.<=) (Interval.ibeg- (- (LinearScan.Utils.nth nextInterval0 intervals0- i))) ( (unsafeCoerce u)))+ ( (Vector0.vnth nextInterval0 intervals0 i)))+ ( (unsafeCoerce u))) ((Prelude.<=) ( (unsafeCoerce u)) (Interval.iend- (- (LinearScan.Utils.nth nextInterval0 intervals0- i)))))))+ ( (Vector0.vnth nextInterval0 intervals0 i))))))) (unsafeCoerce (Interval.firstUseReqReg- ( (LinearScan.Utils.nth nextInterval0 intervals0 i))))+ ( (Vector0.vnth nextInterval0 intervals0 i)))) (unsafeCoerce Prelude.Nothing) of { Prelude.True -> _evar_0_ __; Prelude.False -> _evar_0_0 __}}}}}
LinearScan/Nat.hs view
@@ -10,6 +10,6 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils
LinearScan/NonEmpty.hs view
@@ -10,7 +10,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils coq_NonEmpty_rect :: (a1 -> a2) -> (a1 -> ([] a1) -> a2 -> a2) -> ([]
LinearScan/Prelude0.hs view
@@ -10,34 +10,20 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils +flip :: (a1 -> a2 -> a3) -> a2 -> a1 -> a3+flip f y x =+ f x y++const :: a2 -> a1 -> a2+const x x0 =+ x+ 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 =
LinearScan/Range.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Datatypes as Datatypes import qualified LinearScan.List1 as List1@@ -139,14 +139,13 @@ (Prelude.||) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (rend x)) (unsafeCoerce (rend y)))- (case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of {- Prelude.True -> (Prelude.<=) ((Prelude.succ) (rbeg y)) (rend x);- Prelude.False -> (Prelude.<=) ((Prelude.succ) (rbeg x)) (rend y)})+ ((Prelude.&&) ((Prelude.<=) ((Prelude.succ) (rbeg x)) (rend y))+ ((Prelude.<=) ((Prelude.succ) (rbeg y)) (rend x))) rangeIntersectionPoint :: RangeDesc -> RangeDesc -> Prelude.Maybe Prelude0.Coq_oddnum rangeIntersectionPoint x y =- case rangesIntersect x y of {+ case rangesIntersect (getRangeDesc x) (getRangeDesc y) of { Prelude.True -> Prelude.Just (case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of { Prelude.True -> rbeg y;
LinearScan/Resolve.hs view
@@ -11,251 +11,979 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils--import qualified LinearScan.Allocate as Allocate-import qualified LinearScan.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.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-import qualified LinearScan.Yoneda as Yoneda-import qualified LinearScan.Eqtype as Eqtype-import qualified LinearScan.Fintype as Fintype-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--type PhysReg = Prelude.Int--type RawResolvingMove = (,) (Prelude.Maybe PhysReg) (Prelude.Maybe PhysReg)--data ResolvingMove =- Move PhysReg PhysReg- | Swap PhysReg PhysReg- | Spill PhysReg Blocks.VarId- | Restore Blocks.VarId PhysReg- | Nop--prepareForGraph :: Prelude.Int -> Eqtype.Equality__Coq_sort ->- RawResolvingMove -> (,)- (Prelude.Maybe Eqtype.Equality__Coq_sort)- (Prelude.Maybe Eqtype.Equality__Coq_sort)-prepareForGraph maxReg vid x =- case x of {- (,) o o0 ->- case o of {- Prelude.Just x0 ->- case o0 of {- Prelude.Just y -> (,) (Prelude.Just (unsafeCoerce (Prelude.Left x0)))- (Prelude.Just (unsafeCoerce (Prelude.Left y)));- Prelude.Nothing -> (,) (Prelude.Just (unsafeCoerce (Prelude.Left x0)))- (Prelude.Just (unsafeCoerce (Prelude.Right vid)))};- Prelude.Nothing ->- case o0 of {- Prelude.Just y -> (,) (Prelude.Just- (unsafeCoerce (Prelude.Right vid))) (Prelude.Just- (unsafeCoerce (Prelude.Left y)));- Prelude.Nothing -> (,) (Prelude.Just- (unsafeCoerce (Prelude.Right vid))) (Prelude.Just- (unsafeCoerce (Prelude.Right vid)))}}}--moveFromGraph :: Prelude.Int -> ((,)- (Prelude.Maybe Eqtype.Equality__Coq_sort)- (Prelude.Maybe Eqtype.Equality__Coq_sort)) -> ResolvingMove-moveFromGraph maxReg mv =- case mv of {- (,) o o0 ->- case o of {- Prelude.Just s ->- case unsafeCoerce s of {- Prelude.Left x ->- case o0 of {- Prelude.Just s0 ->- case unsafeCoerce s0 of {- Prelude.Left y -> Move x y;- Prelude.Right y -> Spill x y};- Prelude.Nothing -> Nop};- Prelude.Right x ->- case o0 of {- Prelude.Just s0 ->- case unsafeCoerce s0 of {- Prelude.Left y -> Restore x y;- Prelude.Right s1 -> Nop};- Prelude.Nothing -> Nop}};- Prelude.Nothing -> Nop}}--determineMoves :: Prelude.Int -> (IntMap.IntMap RawResolvingMove) -> []- ResolvingMove-determineMoves maxReg moves =- let {- graph = List1.forFold- (Graph.emptyGraph- (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)- Ssrnat.nat_eqType))- (unsafeCoerce (IntMap.coq_IntMap_toList moves)) (\g mv ->- Graph.addEdge- (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)- Ssrnat.nat_eqType)- (unsafeCoerce- (prepareForGraph maxReg (Prelude.fst mv) (Prelude.snd mv)))- g)}- in- Prelude.map (moveFromGraph maxReg)- (Graph.topsort- (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType)- graph)--resolvingMoves :: Prelude.Int -> ([] Allocate.Allocation) -> Prelude.Int ->- Prelude.Int -> IntMap.IntMap RawResolvingMove-resolvingMoves maxReg allocs from to =- let {- liveAtFrom = IntMap.coq_IntMap_fromList- (Prelude.map (\i -> (,)- (Interval.ivar (Allocate.intVal maxReg i)) i)- (Prelude.filter (\i ->- (Prelude.&&)- ((Prelude.<=)- (Interval.ibeg (Allocate.intVal maxReg i)) from)- ((Prelude.<=) ((Prelude.succ) from)- (Interval.iend (Allocate.intVal maxReg i))))- allocs))}- in- let {- liveAtTo = IntMap.coq_IntMap_fromList- (Prelude.map (\i -> (,)- (Interval.ivar (Allocate.intVal maxReg i)) i)- (Prelude.filter (\i ->- let {int = Allocate.intVal maxReg i} in- (Prelude.&&) ((Prelude.<=) (Interval.ibeg int) to)- (case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce to)- (unsafeCoerce (Interval.iend int)) of {- Prelude.True ->- case Interval.lastUsePos int of {- Prelude.Just u -> (Prelude.<=) to (UsePos.uloc u);- Prelude.Nothing -> Prelude.False};- Prelude.False ->- (Prelude.<=) ((Prelude.succ) to) (Interval.iend int)}))- allocs))}- in- IntMap.coq_IntMap_mergeWithKey (\vid x y ->- case Eqtype.eq_op (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))- (unsafeCoerce (Allocate.intReg maxReg x))- (unsafeCoerce (Allocate.intReg maxReg y)) of {- Prelude.True -> Prelude.Nothing;- Prelude.False -> Prelude.Just ((,) (Allocate.intReg maxReg x)- (Allocate.intReg maxReg y))}) (\x -> IntMap.emptyIntMap) (\x ->- IntMap.emptyIntMap) liveAtFrom liveAtTo--checkBlockBoundary :: Prelude.Int -> ([] Allocate.Allocation) -> Prelude.Int- -> Prelude.Bool -> LiveSets.BlockLiveSets ->- 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 IntSet.coq_IntSet_member vid liveIn of {- Prelude.True -> (:) ((,) vid x) acc;- Prelude.False -> acc}}- in- let {- moves = IntMap.coq_IntMap_foldlWithKey select []- (resolvingMoves maxReg allocs (LiveSets.blockLastOpId from)- (LiveSets.blockFirstOpId to))}- in- List1.forFold mappings (unsafeCoerce moves) (\ms mv ->- let {- addToGraphs = \e xs ->- case xs of {- (,) gbeg gend ->- case in_from of {- Prelude.True -> (,) gbeg- (Graph.addEdge- (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)- Ssrnat.nat_eqType) e gend);- Prelude.False -> (,)- (Graph.addEdge- (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)- Ssrnat.nat_eqType) e gbeg) gend}}}- in- let {- f = \mxs ->- unsafeCoerce addToGraphs- (prepareForGraph maxReg (Prelude.fst mv) (Prelude.snd mv))- (case mxs of {- Prelude.Just xs -> xs;- Prelude.Nothing -> (,)- (Graph.emptyGraph- (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)- Ssrnat.nat_eqType))- (Graph.emptyGraph- (Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg)- Ssrnat.nat_eqType))})}- in- IntMap.coq_IntMap_alter ((Prelude..) (\x -> Prelude.Just x) f) bid ms)--type BlockMoves = (,) Graph.Graph Graph.Graph--resolveDataFlow :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo - a5 a1 a2 a3 a4) -> ([] Allocate.Allocation) -> ([] - a1) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> a5-resolveDataFlow maxReg mDict binfo allocs blocks liveSets =- 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 ->- case IntMap.coq_IntMap_lookup bid liveSets of {- Prelude.Just from ->- Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\suxs ->- let {- in_from = (Prelude.<=) (Data.List.length suxs) ((Prelude.succ)- 0)}- in- Applicative.pure- (unsafeCoerce- (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))- (List1.forFold mappings suxs (\ms s_bid ->- case IntMap.coq_IntMap_lookup s_bid liveSets of {- Prelude.Just to ->- let {- key = case in_from of {- Prelude.True -> bid;- Prelude.False -> s_bid}}- in- checkBlockBoundary maxReg allocs key in_from from to- (LiveSets.blockLiveIn to) ms;- Prelude.Nothing -> ms})))- (unsafeCoerce (\_ -> Blocks.blockSuccessors mDict binfo b));- Prelude.Nothing ->- Applicative.pure- (unsafeCoerce- (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict)))- mappings}) (\_ -> Blocks.blockId mDict binfo b)))+import qualified Hask.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.IntSet as IntSet+import qualified LinearScan.Interval as Interval+import qualified LinearScan.List1 as List1+import qualified LinearScan.LiveSets as LiveSets+import qualified LinearScan.Maybe as Maybe+import qualified LinearScan.Monad as Monad+import qualified LinearScan.Prelude0 as Prelude0+import qualified LinearScan.UsePos as UsePos+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Fintype as Fintype+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++data ResolvingMove =+ Move PhysReg Blocks.VarId PhysReg+ | Swap PhysReg Blocks.VarId PhysReg Blocks.VarId+ | Spill PhysReg Blocks.VarId+ | Restore Blocks.VarId PhysReg+ | AllocReg Blocks.VarId PhysReg+ | FreeReg PhysReg Blocks.VarId++data ResolvingMoveSet =+ RSMove Prelude.Int Blocks.VarId Prelude.Int+ | RSSwap Prelude.Int Blocks.VarId Prelude.Int Blocks.VarId+ | RSSpill Prelude.Int Blocks.VarId+ | RSRestore Blocks.VarId Prelude.Int+ | RSAllocReg Blocks.VarId Prelude.Int+ | RSFreeReg Prelude.Int Blocks.VarId+ | RSAssignReg Prelude.Int Blocks.VarId+ | RSClearReg Prelude.Int Blocks.VarId++weakenResolvingMove :: Prelude.Int -> ResolvingMove -> ResolvingMoveSet+weakenResolvingMove maxReg x =+ case x of {+ Move fr fv tr -> RSMove ( fr) fv ( tr);+ Swap fr fv tr tv -> RSSwap ( fr) fv ( tr) tv;+ Spill fr tv -> RSSpill ( fr) tv;+ Restore fv tr -> RSRestore fv ( tr);+ AllocReg fv tr -> RSAllocReg fv ( tr);+ FreeReg fr tv -> RSFreeReg ( fr) tv}++eqResolvingMove :: Prelude.Int -> ResolvingMove -> ResolvingMove ->+ Prelude.Bool+eqResolvingMove maxReg s1 s2 =+ case s1 of {+ Move fr1 fv1 tr1 ->+ case s2 of {+ Move fr2 fv2 tr2 ->+ (Prelude.&&)+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1)+ (unsafeCoerce fr2))+ ((Prelude.&&)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1)+ (unsafeCoerce fv2))+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)+ (unsafeCoerce tr2)));+ _ -> Prelude.False};+ Swap fr1 fv1 tr1 tv1 ->+ case s2 of {+ Swap fr2 fv2 tr2 tv2 ->+ (Prelude.&&)+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1)+ (unsafeCoerce fr2))+ ((Prelude.&&)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1)+ (unsafeCoerce fv2))+ ((Prelude.&&)+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)+ (unsafeCoerce tr2))+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1)+ (unsafeCoerce tv2))));+ _ -> Prelude.False};+ Spill fr1 fv1 ->+ case s2 of {+ Spill fr2 fv2 ->+ (Prelude.&&)+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1)+ (unsafeCoerce fr2))+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1)+ (unsafeCoerce fv2));+ _ -> Prelude.False};+ Restore tv1 tr1 ->+ case s2 of {+ Restore tv2 tr2 ->+ (Prelude.&&)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1)+ (unsafeCoerce tv2))+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)+ (unsafeCoerce tr2));+ _ -> Prelude.False};+ AllocReg fv1 tr1 ->+ case s2 of {+ AllocReg fv2 tr2 ->+ (Prelude.&&)+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1)+ (unsafeCoerce fv2))+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)+ (unsafeCoerce tr2));+ _ -> Prelude.False};+ FreeReg fr1 tv1 ->+ case s2 of {+ FreeReg fr2 tv2 ->+ (Prelude.&&)+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1)+ (unsafeCoerce fr2))+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1)+ (unsafeCoerce tv2));+ _ -> Prelude.False}}++eqResolvingMoveP :: Prelude.Int -> Eqtype.Equality__Coq_axiom ResolvingMove+eqResolvingMoveP maxReg _top_assumption_ =+ let {+ _evar_0_ = \fr1 fv1 tr1 _top_assumption_0 ->+ let {+ _evar_0_ = \fr2 fv2 tr2 ->+ let {+ _evar_0_ = \_ ->+ let {+ _evar_0_ = let {+ _evar_0_ = \_ ->+ let {+ _evar_0_ = let {+ _evar_0_ = \_ ->+ let {_evar_0_ = Ssrbool.ReflectT} in+ _evar_0_}+ in+ let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP+ (Fintype.ordinal_eqType maxReg) tr1+ tr2 of {+ Ssrbool.ReflectT -> _evar_0_ __;+ Ssrbool.ReflectF -> _evar_0_0 __}}+ in+ _evar_0_}+ in+ let {+ _evar_0_0 = \_ ->+ let {+ _evar_0_0 = \_ ->+ let {_evar_0_0 = Ssrbool.ReflectF} in _evar_0_0}+ in+ let {_evar_0_1 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of {+ Ssrbool.ReflectT -> _evar_0_0 __;+ Ssrbool.ReflectF -> _evar_0_1 __}}+ in+ case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {+ Ssrbool.ReflectT -> _evar_0_ __;+ Ssrbool.ReflectF -> _evar_0_0 __}}+ in+ _evar_0_}+ in+ let {+ _evar_0_0 = \_ ->+ let {+ _evar_0_0 = \_ ->+ let {+ _evar_0_0 = let {+ _evar_0_0 = \_ ->+ let {_evar_0_0 = Ssrbool.ReflectF} in _evar_0_0}+ in+ let {_evar_0_1 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1+ tr2 of {+ Ssrbool.ReflectT -> _evar_0_0 __;+ Ssrbool.ReflectF -> _evar_0_1 __}}+ in+ _evar_0_0}+ in+ let {+ _evar_0_1 = \_ ->+ let {+ _evar_0_1 = \_ ->+ let {_evar_0_1 = Ssrbool.ReflectF} in _evar_0_1}+ in+ let {_evar_0_2 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of {+ Ssrbool.ReflectT -> _evar_0_1 __;+ Ssrbool.ReflectF -> _evar_0_2 __}}+ in+ case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {+ Ssrbool.ReflectT -> _evar_0_0 __;+ Ssrbool.ReflectF -> _evar_0_1 __}}+ in+ case Eqtype.eqP (Fintype.ordinal_eqType maxReg) fr1 fr2 of {+ Ssrbool.ReflectT -> _evar_0_ __;+ Ssrbool.ReflectF -> _evar_0_0 __}}+ in+ let {_evar_0_0 = \fr2 fv2 tr2 tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_1 = \fr2 fv2 -> Ssrbool.ReflectF} in+ let {_evar_0_2 = \tv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_3 = \fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_4 = \fr2 tv2 -> Ssrbool.ReflectF} in+ case _top_assumption_0 of {+ Move x x0 x1 -> unsafeCoerce _evar_0_ x x0 x1;+ Swap x x0 x1 x2 -> _evar_0_0 x x0 x1 x2;+ Spill x x0 -> _evar_0_1 x x0;+ Restore x x0 -> _evar_0_2 x x0;+ AllocReg x x0 -> _evar_0_3 x x0;+ FreeReg x x0 -> _evar_0_4 x x0}}+ in+ let {+ _evar_0_0 = \fr1 fv1 tr1 tv1 _top_assumption_0 ->+ let {_evar_0_0 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in+ let {+ _evar_0_1 = \fr2 fv2 tr2 tv2 ->+ let {+ _evar_0_1 = \_ ->+ let {+ _evar_0_1 = let {+ _evar_0_1 = \_ ->+ let {+ _evar_0_1 = let {+ _evar_0_1 = \_ ->+ let {+ _evar_0_1 = let {+ _evar_0_1 = \_ ->+ let {+ _evar_0_1 = Ssrbool.ReflectT}+ in+ _evar_0_1}+ in+ let {+ _evar_0_2 = \_ ->+ Ssrbool.ReflectF}+ in+ case Eqtype.eqP+ Ssrnat.nat_eqType+ tv1 tv2 of {+ Ssrbool.ReflectT ->+ _evar_0_1 __;+ Ssrbool.ReflectF ->+ _evar_0_2 __}}+ in+ _evar_0_1}+ in+ let {+ _evar_0_2 = \_ ->+ let {+ _evar_0_2 = \_ ->+ let {_evar_0_2 = Ssrbool.ReflectF} in+ _evar_0_2}+ in+ let {+ _evar_0_3 = \_ -> Ssrbool.ReflectF}+ in+ case Eqtype.eqP Ssrnat.nat_eqType tv1+ tv2 of {+ Ssrbool.ReflectT -> _evar_0_2 __;+ Ssrbool.ReflectF -> _evar_0_3 __}}+ in+ case Eqtype.eqP+ (Fintype.ordinal_eqType maxReg)+ tr1 tr2 of {+ Ssrbool.ReflectT -> _evar_0_1 __;+ Ssrbool.ReflectF -> _evar_0_2 __}}+ in+ _evar_0_1}+ in+ let {+ _evar_0_2 = \_ ->+ let {+ _evar_0_2 = \_ ->+ let {+ _evar_0_2 = let {+ _evar_0_2 = \_ ->+ let {_evar_0_2 = Ssrbool.ReflectF} in+ _evar_0_2}+ in+ let {+ _evar_0_3 = \_ -> Ssrbool.ReflectF}+ in+ case Eqtype.eqP Ssrnat.nat_eqType tv1+ tv2 of {+ Ssrbool.ReflectT -> _evar_0_2 __;+ Ssrbool.ReflectF -> _evar_0_3 __}}+ in+ _evar_0_2}+ in+ let {+ _evar_0_3 = \_ ->+ let {+ _evar_0_3 = \_ ->+ let {_evar_0_3 = Ssrbool.ReflectF} in _evar_0_3}+ in+ let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of {+ Ssrbool.ReflectT -> _evar_0_3 __;+ Ssrbool.ReflectF -> _evar_0_4 __}}+ in+ case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1+ tr2 of {+ Ssrbool.ReflectT -> _evar_0_2 __;+ Ssrbool.ReflectF -> _evar_0_3 __}}+ in+ case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {+ Ssrbool.ReflectT -> _evar_0_1 __;+ Ssrbool.ReflectF -> _evar_0_2 __}}+ in+ _evar_0_1}+ in+ let {+ _evar_0_2 = \_ ->+ let {+ _evar_0_2 = \_ ->+ let {+ _evar_0_2 = let {+ _evar_0_2 = \_ ->+ let {+ _evar_0_2 = let {+ _evar_0_2 = \_ ->+ let {_evar_0_2 = Ssrbool.ReflectF} in+ _evar_0_2}+ in+ let {+ _evar_0_3 = \_ -> Ssrbool.ReflectF}+ in+ case Eqtype.eqP Ssrnat.nat_eqType tv1+ tv2 of {+ Ssrbool.ReflectT -> _evar_0_2 __;+ Ssrbool.ReflectF -> _evar_0_3 __}}+ in+ _evar_0_2}+ in+ let {+ _evar_0_3 = \_ ->+ let {+ _evar_0_3 = \_ ->+ let {_evar_0_3 = Ssrbool.ReflectF} in _evar_0_3}+ in+ let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of {+ Ssrbool.ReflectT -> _evar_0_3 __;+ Ssrbool.ReflectF -> _evar_0_4 __}}+ in+ case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1+ tr2 of {+ Ssrbool.ReflectT -> _evar_0_2 __;+ Ssrbool.ReflectF -> _evar_0_3 __}}+ in+ _evar_0_2}+ in+ let {+ _evar_0_3 = \_ ->+ let {+ _evar_0_3 = \_ ->+ let {+ _evar_0_3 = let {+ _evar_0_3 = \_ ->+ let {_evar_0_3 = Ssrbool.ReflectF} in _evar_0_3}+ in+ let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of {+ Ssrbool.ReflectT -> _evar_0_3 __;+ Ssrbool.ReflectF -> _evar_0_4 __}}+ in+ _evar_0_3}+ in+ let {+ _evar_0_4 = \_ ->+ let {+ _evar_0_4 = \_ ->+ let {_evar_0_4 = Ssrbool.ReflectF} in _evar_0_4}+ in+ let {_evar_0_5 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of {+ Ssrbool.ReflectT -> _evar_0_4 __;+ Ssrbool.ReflectF -> _evar_0_5 __}}+ in+ case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of {+ Ssrbool.ReflectT -> _evar_0_3 __;+ Ssrbool.ReflectF -> _evar_0_4 __}}+ in+ case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {+ Ssrbool.ReflectT -> _evar_0_2 __;+ Ssrbool.ReflectF -> _evar_0_3 __}}+ in+ case Eqtype.eqP (Fintype.ordinal_eqType maxReg) fr1 fr2 of {+ Ssrbool.ReflectT -> _evar_0_1 __;+ Ssrbool.ReflectF -> _evar_0_2 __}}+ in+ let {_evar_0_2 = \fr2 fv2 -> Ssrbool.ReflectF} in+ let {_evar_0_3 = \tv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_4 = \fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_5 = \fr2 tv2 -> Ssrbool.ReflectF} in+ case _top_assumption_0 of {+ Move x x0 x1 -> _evar_0_0 x x0 x1;+ Swap x x0 x1 x2 -> unsafeCoerce _evar_0_1 x x0 x1 x2;+ Spill x x0 -> _evar_0_2 x x0;+ Restore x x0 -> _evar_0_3 x x0;+ AllocReg x x0 -> _evar_0_4 x x0;+ FreeReg x x0 -> _evar_0_5 x x0}}+ in+ let {+ _evar_0_1 = \fr1 fv1 _top_assumption_0 ->+ let {_evar_0_1 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_2 = \fr2 fv2 tr2 tv2 -> Ssrbool.ReflectF} in+ let {+ _evar_0_3 = \fr2 fv2 ->+ let {+ _evar_0_3 = \_ ->+ let {+ _evar_0_3 = let {+ _evar_0_3 = \_ ->+ let {_evar_0_3 = Ssrbool.ReflectT} in _evar_0_3}+ in+ let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {+ Ssrbool.ReflectT -> _evar_0_3 __;+ Ssrbool.ReflectF -> _evar_0_4 __}}+ in+ _evar_0_3}+ in+ let {+ _evar_0_4 = \_ ->+ let {+ _evar_0_4 = \_ -> let {_evar_0_4 = Ssrbool.ReflectF} in _evar_0_4}+ in+ let {_evar_0_5 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {+ Ssrbool.ReflectT -> _evar_0_4 __;+ Ssrbool.ReflectF -> _evar_0_5 __}}+ in+ case Eqtype.eqP (Fintype.ordinal_eqType maxReg) fr1 fr2 of {+ Ssrbool.ReflectT -> _evar_0_3 __;+ Ssrbool.ReflectF -> _evar_0_4 __}}+ in+ let {_evar_0_4 = \tv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_5 = \fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_6 = \fr2 tv2 -> Ssrbool.ReflectF} in+ case _top_assumption_0 of {+ Move x x0 x1 -> _evar_0_1 x x0 x1;+ Swap x x0 x1 x2 -> _evar_0_2 x x0 x1 x2;+ Spill x x0 -> unsafeCoerce _evar_0_3 x x0;+ Restore x x0 -> _evar_0_4 x x0;+ AllocReg x x0 -> _evar_0_5 x x0;+ FreeReg x x0 -> _evar_0_6 x x0}}+ in+ let {+ _evar_0_2 = \tv1 tr1 _top_assumption_0 ->+ let {_evar_0_2 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_3 = \fr2 fv2 tr2 tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_4 = \fr2 fv2 -> Ssrbool.ReflectF} in+ let {+ _evar_0_5 = \tv2 tr2 ->+ let {+ _evar_0_5 = \_ ->+ let {+ _evar_0_5 = let {+ _evar_0_5 = \_ ->+ let {_evar_0_5 = Ssrbool.ReflectT} in _evar_0_5}+ in+ let {_evar_0_6 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of {+ Ssrbool.ReflectT -> _evar_0_5 __;+ Ssrbool.ReflectF -> _evar_0_6 __}}+ in+ _evar_0_5}+ in+ let {+ _evar_0_6 = \_ ->+ let {+ _evar_0_6 = \_ -> let {_evar_0_6 = Ssrbool.ReflectF} in _evar_0_6}+ in+ let {_evar_0_7 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of {+ Ssrbool.ReflectT -> _evar_0_6 __;+ Ssrbool.ReflectF -> _evar_0_7 __}}+ in+ case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of {+ Ssrbool.ReflectT -> _evar_0_5 __;+ Ssrbool.ReflectF -> _evar_0_6 __}}+ in+ let {_evar_0_6 = \fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_7 = \fr2 tv2 -> Ssrbool.ReflectF} in+ case _top_assumption_0 of {+ Move x x0 x1 -> _evar_0_2 x x0 x1;+ Swap x x0 x1 x2 -> _evar_0_3 x x0 x1 x2;+ Spill x x0 -> _evar_0_4 x x0;+ Restore x x0 -> unsafeCoerce _evar_0_5 x x0;+ AllocReg x x0 -> _evar_0_6 x x0;+ FreeReg x x0 -> _evar_0_7 x x0}}+ in+ let {+ _evar_0_3 = \fv1 tr1 _top_assumption_0 ->+ let {_evar_0_3 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_4 = \fr2 fv2 tr2 tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_5 = \fr2 fv2 -> Ssrbool.ReflectF} in+ let {_evar_0_6 = \tv2 tr2 -> Ssrbool.ReflectF} in+ let {+ _evar_0_7 = \fv2 tr2 ->+ let {+ _evar_0_7 = \_ ->+ let {+ _evar_0_7 = let {+ _evar_0_7 = \_ ->+ let {_evar_0_7 = Ssrbool.ReflectT} in _evar_0_7}+ in+ let {_evar_0_8 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of {+ Ssrbool.ReflectT -> _evar_0_7 __;+ Ssrbool.ReflectF -> _evar_0_8 __}}+ in+ _evar_0_7}+ in+ let {+ _evar_0_8 = \_ ->+ let {+ _evar_0_8 = \_ -> let {_evar_0_8 = Ssrbool.ReflectF} in _evar_0_8}+ in+ let {_evar_0_9 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of {+ Ssrbool.ReflectT -> _evar_0_8 __;+ Ssrbool.ReflectF -> _evar_0_9 __}}+ in+ case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {+ Ssrbool.ReflectT -> _evar_0_7 __;+ Ssrbool.ReflectF -> _evar_0_8 __}}+ in+ let {_evar_0_8 = \fr2 tv2 -> Ssrbool.ReflectF} in+ case _top_assumption_0 of {+ Move x x0 x1 -> _evar_0_3 x x0 x1;+ Swap x x0 x1 x2 -> _evar_0_4 x x0 x1 x2;+ Spill x x0 -> _evar_0_5 x x0;+ Restore x x0 -> _evar_0_6 x x0;+ AllocReg x x0 -> unsafeCoerce _evar_0_7 x x0;+ FreeReg x x0 -> _evar_0_8 x x0}}+ in+ let {+ _evar_0_4 = \fr1 tv1 _top_assumption_0 ->+ let {_evar_0_4 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_5 = \fr2 fv2 tr2 tv2 -> Ssrbool.ReflectF} in+ let {_evar_0_6 = \fr2 fv2 -> Ssrbool.ReflectF} in+ let {_evar_0_7 = \tv2 tr2 -> Ssrbool.ReflectF} in+ let {_evar_0_8 = \fv2 tr2 -> Ssrbool.ReflectF} in+ let {+ _evar_0_9 = \fr2 tv2 ->+ let {+ _evar_0_9 = \_ ->+ let {+ _evar_0_9 = let {+ _evar_0_9 = \_ ->+ let {_evar_0_9 = Ssrbool.ReflectT} in _evar_0_9}+ in+ let {_evar_0_10 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of {+ Ssrbool.ReflectT -> _evar_0_9 __;+ Ssrbool.ReflectF -> _evar_0_10 __}}+ in+ _evar_0_9}+ in+ let {+ _evar_0_10 = \_ ->+ let {+ _evar_0_10 = \_ ->+ let {_evar_0_10 = Ssrbool.ReflectF} in _evar_0_10}+ in+ let {_evar_0_11 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of {+ Ssrbool.ReflectT -> _evar_0_10 __;+ Ssrbool.ReflectF -> _evar_0_11 __}}+ in+ case Eqtype.eqP (Fintype.ordinal_eqType maxReg) fr1 fr2 of {+ Ssrbool.ReflectT -> _evar_0_9 __;+ Ssrbool.ReflectF -> _evar_0_10 __}}+ in+ case _top_assumption_0 of {+ Move x x0 x1 -> _evar_0_4 x x0 x1;+ Swap x x0 x1 x2 -> _evar_0_5 x x0 x1 x2;+ Spill x x0 -> _evar_0_6 x x0;+ Restore x x0 -> _evar_0_7 x x0;+ AllocReg x x0 -> _evar_0_8 x x0;+ FreeReg x x0 -> unsafeCoerce _evar_0_9 x x0}}+ in+ case _top_assumption_ of {+ Move x x0 x1 -> unsafeCoerce _evar_0_ x x0 x1;+ Swap x x0 x1 x2 -> unsafeCoerce _evar_0_0 x x0 x1 x2;+ Spill x x0 -> unsafeCoerce _evar_0_1 x x0;+ Restore x x0 -> unsafeCoerce _evar_0_2 x x0;+ AllocReg x x0 -> unsafeCoerce _evar_0_3 x x0;+ FreeReg x x0 -> unsafeCoerce _evar_0_4 x x0}++coq_ResolvingMove_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of+ ResolvingMove+coq_ResolvingMove_eqMixin maxReg =+ Eqtype.Equality__Mixin (eqResolvingMove maxReg) (eqResolvingMoveP maxReg)++coq_ResolvingMove_eqType :: Prelude.Int -> Eqtype.Equality__Coq_type+coq_ResolvingMove_eqType maxReg =+ unsafeCoerce (coq_ResolvingMove_eqMixin maxReg)++coq_ResGraphNode :: Prelude.Int -> Eqtype.Equality__Coq_type+coq_ResGraphNode maxReg =+ Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType++data ResGraphEdge =+ Build_ResGraphEdge ResolvingMove Prelude.Bool (Prelude.Maybe+ Eqtype.Equality__Coq_sort) + (Prelude.Maybe Eqtype.Equality__Coq_sort)++resMove :: Prelude.Int -> ResGraphEdge -> ResolvingMove+resMove maxReg r =+ case r of {+ Build_ResGraphEdge resMove0 resGhost0 resBeg0 resEnd0 -> resMove0}++resGhost :: Prelude.Int -> ResGraphEdge -> Prelude.Bool+resGhost maxReg r =+ case r of {+ Build_ResGraphEdge resMove0 resGhost0 resBeg0 resEnd0 -> resGhost0}++resBeg :: Prelude.Int -> ResGraphEdge -> Prelude.Maybe+ Eqtype.Equality__Coq_sort+resBeg maxReg r =+ case r of {+ Build_ResGraphEdge resMove0 resGhost0 resBeg0 resEnd0 -> resBeg0}++resEnd :: Prelude.Int -> ResGraphEdge -> Prelude.Maybe+ Eqtype.Equality__Coq_sort+resEnd maxReg r =+ case r of {+ Build_ResGraphEdge resMove0 resGhost0 resBeg0 resEnd0 -> resEnd0}++eqResGraphEdge :: Prelude.Int -> ResGraphEdge -> ResGraphEdge -> Prelude.Bool+eqResGraphEdge maxReg s1 s2 =+ case s1 of {+ Build_ResGraphEdge a1 b1 c1 d1 ->+ case s2 of {+ Build_ResGraphEdge a2 b2 c2 d2 ->+ (Prelude.&&)+ (Eqtype.eq_op (coq_ResolvingMove_eqType maxReg) (unsafeCoerce a1)+ (unsafeCoerce a2))+ ((Prelude.&&)+ (Eqtype.eq_op Eqtype.bool_eqType (unsafeCoerce b1)+ (unsafeCoerce b2))+ ((Prelude.&&)+ (Eqtype.eq_op (Eqtype.option_eqType (coq_ResGraphNode maxReg))+ (unsafeCoerce c1) (unsafeCoerce c2))+ (Eqtype.eq_op (Eqtype.option_eqType (coq_ResGraphNode maxReg))+ (unsafeCoerce d1) (unsafeCoerce d2))))}}++eqResGraphEdgeP :: Prelude.Int -> Eqtype.Equality__Coq_axiom ResGraphEdge+eqResGraphEdgeP maxReg _top_assumption_ =+ let {+ _evar_0_ = \a1 b1 c1 d1 _top_assumption_0 ->+ let {+ _evar_0_ = \a2 b2 c2 d2 ->+ let {+ _evar_0_ = \_ ->+ let {+ _evar_0_ = let {+ _evar_0_ = \_ ->+ let {+ _evar_0_ = let {+ _evar_0_ = \_ ->+ let {+ _evar_0_ = let {+ _evar_0_ = \_ ->+ let {+ _evar_0_ = Ssrbool.ReflectT}+ in+ _evar_0_}+ in+ let {+ _evar_0_0 = \_ ->+ Ssrbool.ReflectF}+ in+ case Eqtype.eqP+ (Eqtype.option_eqType+ (coq_ResGraphNode+ maxReg)) d1 d2 of {+ Ssrbool.ReflectT ->+ _evar_0_ __;+ Ssrbool.ReflectF ->+ _evar_0_0 __}}+ in+ _evar_0_}+ in+ let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP+ (Eqtype.option_eqType+ (coq_ResGraphNode maxReg)) c1 c2 of {+ Ssrbool.ReflectT -> _evar_0_ __;+ Ssrbool.ReflectF -> _evar_0_0 __}}+ in+ _evar_0_}+ in+ let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {+ Ssrbool.ReflectT -> _evar_0_ __;+ Ssrbool.ReflectF -> _evar_0_0 __}}+ in+ _evar_0_}+ in+ let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in+ case Eqtype.eqP (coq_ResolvingMove_eqType maxReg) a1 a2 of {+ Ssrbool.ReflectT -> _evar_0_ __;+ Ssrbool.ReflectF -> _evar_0_0 __}}+ in+ case _top_assumption_0 of {+ Build_ResGraphEdge x x0 x1 x2 -> unsafeCoerce _evar_0_ x x0 x1 x2}}+ in+ case _top_assumption_ of {+ Build_ResGraphEdge x x0 x1 x2 -> unsafeCoerce _evar_0_ x x0 x1 x2}++coq_ResGraphEdge_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of+ ResGraphEdge+coq_ResGraphEdge_eqMixin maxReg =+ Eqtype.Equality__Mixin (eqResGraphEdge maxReg) (eqResGraphEdgeP maxReg)++coq_ResGraphEdge_eqType :: Prelude.Int -> Eqtype.Equality__Coq_type+coq_ResGraphEdge_eqType maxReg =+ unsafeCoerce (coq_ResGraphEdge_eqMixin maxReg)++determineEdge :: Prelude.Int -> ResGraphEdge -> (,)+ (Prelude.Maybe Eqtype.Equality__Coq_sort)+ (Prelude.Maybe Eqtype.Equality__Coq_sort)+determineEdge maxReg x =+ (,) (resBeg maxReg x) (resEnd maxReg x)++splitEdge :: Prelude.Int -> ResGraphEdge -> [] ResGraphEdge+splitEdge maxReg x =+ case resMove maxReg x of {+ Move fr fv tr -> (:) (Build_ResGraphEdge (Spill fr fv) Prelude.False+ (resBeg maxReg x) Prelude.Nothing) ((:) (Build_ResGraphEdge (Restore fv+ tr) (resGhost maxReg x) Prelude.Nothing (resEnd maxReg x)) []);+ Swap fr fv tr tv -> (:) (Build_ResGraphEdge (Swap tr tv fr fv)+ (resGhost maxReg x) (resEnd maxReg x) (resBeg maxReg x)) [];+ _ -> []}++determineMoves :: Prelude.Int -> (IntMap.IntMap ResGraphEdge) -> []+ ResGraphEdge+determineMoves maxReg moves =+ unsafeCoerce+ (Graph.topsort (coq_ResGraphNode maxReg) (coq_ResGraphEdge_eqType maxReg)+ (IntMap.coq_IntMap_foldl+ (Prelude0.flip+ (unsafeCoerce+ (Graph.addEdge (coq_ResGraphNode maxReg)+ (coq_ResGraphEdge_eqType maxReg))))+ (Graph.emptyGraph (coq_ResGraphNode maxReg)+ (coq_ResGraphEdge_eqType maxReg)+ (unsafeCoerce (determineEdge maxReg))) moves)+ (unsafeCoerce (splitEdge maxReg)))++resolvingMoves :: Prelude.Int -> ([] Allocate.Allocation) -> Prelude.Int ->+ Prelude.Int -> IntMap.IntMap ResGraphEdge+resolvingMoves maxReg allocs from to =+ let {+ liveAtFrom = IntMap.coq_IntMap_fromList+ (Prelude.map (\i -> (,)+ (Interval.ivar (Allocate.intVal maxReg i)) i)+ (Prelude.filter (\i ->+ (Prelude.&&)+ ((Prelude.<=)+ (Interval.ibeg (Allocate.intVal maxReg i)) from)+ ((Prelude.<=) ((Prelude.succ) from)+ (Interval.iend (Allocate.intVal maxReg i))))+ allocs))}+ in+ let {+ shouldKeep = \int pos ->+ case (Prelude.<=) (Interval.ibeg int) pos of {+ Prelude.True ->+ case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos)+ (unsafeCoerce (Interval.iend int)) of {+ Prelude.True -> (,)+ (case Interval.lastUsePos int of {+ Prelude.Just u -> (Prelude.<=) to (UsePos.uloc u);+ Prelude.Nothing -> Prelude.False}) Prelude.True;+ Prelude.False -> (,)+ ((Prelude.<=) ((Prelude.succ) to) (Interval.iend int)) Prelude.False};+ Prelude.False -> (,) Prelude.False Prelude.False}}+ in+ let {+ liveAtTo = IntMap.coq_IntMap_fromList+ (Prelude.map (\i -> (,)+ (Interval.ivar (Allocate.intVal maxReg i)) ((,) i+ (Prelude.snd (shouldKeep (Allocate.intVal maxReg i) to))))+ (Prelude.filter (\i ->+ Prelude.fst (shouldKeep (Allocate.intVal maxReg i) to))+ allocs))}+ in+ IntMap.coq_IntMap_mergeWithKey (\vid x yp ->+ case yp of {+ (,) y ghost ->+ case Eqtype.eq_op+ (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))+ (unsafeCoerce (Allocate.intReg maxReg x))+ (unsafeCoerce (Allocate.intReg maxReg y)) of {+ Prelude.True ->+ case Allocate.intReg maxReg y of {+ Prelude.Just reg ->+ case ghost of {+ Prelude.True -> Prelude.Just (Build_ResGraphEdge (FreeReg reg vid)+ Prelude.True (Prelude.Just (unsafeCoerce (Prelude.Left reg)))+ (Prelude.Just (unsafeCoerce (Prelude.Right vid))));+ Prelude.False -> Prelude.Nothing};+ Prelude.Nothing -> Prelude.Nothing};+ Prelude.False ->+ let {+ mmv = case Allocate.intReg maxReg x of {+ Prelude.Just xr ->+ case Allocate.intReg maxReg y of {+ Prelude.Just yr -> Prelude.Just (Move xr vid yr);+ Prelude.Nothing -> Prelude.Just (Spill xr vid)};+ Prelude.Nothing ->+ case Allocate.intReg maxReg y of {+ Prelude.Just xr -> Prelude.Just (Restore vid xr);+ Prelude.Nothing -> Prelude.Nothing}}}+ in+ let {+ anchor = \x0 ->+ Applicative.choose (unsafeCoerce Maybe.option_Alternative)+ (Functor.fmap (unsafeCoerce Maybe.coq_Maybe_Functor) (\x1 ->+ Prelude.Left x1) (unsafeCoerce (Allocate.intReg maxReg x0)))+ (Prelude.Just (Prelude.Right vid))}+ in+ case mmv of {+ Prelude.Just mv -> Prelude.Just (Build_ResGraphEdge mv ghost+ (unsafeCoerce anchor x) (unsafeCoerce anchor y));+ Prelude.Nothing -> Prelude.Nothing}}})+ (IntMap.coq_IntMap_foldlWithKey (\acc vid x ->+ case Allocate.intReg maxReg x of {+ Prelude.Just r ->+ IntMap.coq_IntMap_insert vid (Build_ResGraphEdge (FreeReg r vid)+ Prelude.False (Prelude.Just (unsafeCoerce (Prelude.Left r)))+ (Prelude.Just (unsafeCoerce (Prelude.Right vid)))) acc;+ Prelude.Nothing -> acc}) IntMap.emptyIntMap)+ (IntMap.coq_IntMap_foldlWithKey (\acc vid yp ->+ case yp of {+ (,) y ghost ->+ case Allocate.intReg maxReg y of {+ Prelude.Just r ->+ IntMap.coq_IntMap_insert vid (Build_ResGraphEdge (AllocReg vid r)+ ghost (Prelude.Just (unsafeCoerce (Prelude.Right vid)))+ (Prelude.Just (unsafeCoerce (Prelude.Left r)))) acc;+ Prelude.Nothing -> acc}}) IntMap.emptyIntMap) liveAtFrom liveAtTo++type BlockMoves = (,) Graph.Graph Graph.Graph++movesBetween :: Prelude.Int -> ([] Allocate.Allocation) -> Prelude.Int ->+ Prelude.Int -> [] ResGraphEdge+movesBetween maxReg allocs from to =+ IntMap.coq_IntMap_foldl (Prelude0.flip (\x x0 -> (:) x x0)) []+ (resolvingMoves maxReg allocs from to)++applyMappings :: Prelude.Int -> Blocks.BlockId -> (IntMap.IntMap BlockMoves)+ -> Prelude.Bool -> ([] ResGraphEdge) -> IntMap.IntMap+ BlockMoves+applyMappings maxReg bid mappings in_from moves =+ List1.forFold mappings (unsafeCoerce moves) (\ms mv ->+ let {+ addToGraphs = \e xs ->+ case xs of {+ (,) gbeg gend ->+ case in_from of {+ Prelude.True -> (,) gbeg+ (Graph.addEdge (coq_ResGraphNode maxReg)+ (coq_ResGraphEdge_eqType maxReg) e gend);+ Prelude.False -> (,)+ (Graph.addEdge (coq_ResGraphNode maxReg)+ (coq_ResGraphEdge_eqType maxReg) e gbeg) gend}}}+ in+ let {+ eg = Graph.emptyGraph (coq_ResGraphNode maxReg)+ (coq_ResGraphEdge_eqType maxReg)+ (unsafeCoerce (determineEdge maxReg))}+ in+ let {+ f = \mxs ->+ addToGraphs mv+ (case mxs of {+ Prelude.Just xs -> xs;+ Prelude.Nothing -> (,) eg eg})}+ in+ IntMap.coq_IntMap_alter ((Prelude..) (\x -> Prelude.Just x) f) bid ms)++checkBlockBoundary :: Prelude.Int -> ([] Allocate.Allocation) ->+ Blocks.BlockId -> Prelude.Bool ->+ LiveSets.BlockLiveSets -> LiveSets.BlockLiveSets ->+ IntSet.IntSet -> (IntMap.IntMap BlockMoves) ->+ IntMap.IntMap BlockMoves+checkBlockBoundary maxReg allocs bid in_from from to liveIn mappings =+ applyMappings maxReg bid mappings in_from+ (movesBetween maxReg allocs (LiveSets.blockLastOpId from)+ (LiveSets.blockFirstOpId to))++resolveDataFlow :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo + a5 a1 a2 a3 a4) -> ([] Allocate.Allocation) -> ([] + a1) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> a5+resolveDataFlow maxReg mDict binfo allocs blocks liveSets =+ Functor.fmap (Applicative.is_functor (Monad.is_applicative mDict))+ Prelude.fst+ (Monad.forFoldM mDict ((,) IntMap.emptyIntMap Prelude.True) blocks+ (\z b ->+ case z of {+ (,) mappings isFirst ->+ Monad.bind mDict (\bid ->+ case IntMap.coq_IntMap_lookup bid liveSets of {+ Prelude.Just from ->+ let {+ mappings' = case isFirst of {+ Prelude.True ->+ applyMappings maxReg bid mappings Prelude.False+ (movesBetween maxReg allocs ((Prelude.succ) 0)+ (LiveSets.blockFirstOpId from));+ Prelude.False -> mappings}}+ in+ Monad.bind mDict (\suxs ->+ let {+ in_from = (Prelude.<=) (Data.List.length suxs) ((Prelude.succ)+ 0)}+ in+ let {+ mappings'' = case Eqtype.eq_op Ssrnat.nat_eqType+ (unsafeCoerce (Data.List.length suxs))+ (unsafeCoerce 0) of {+ Prelude.True ->+ applyMappings maxReg bid mappings' Prelude.True+ (movesBetween maxReg allocs+ (LiveSets.blockLastOpId from)+ ((Prelude.succ) ((Prelude.succ)+ (LiveSets.blockLastOpId from))));+ Prelude.False ->+ List1.forFold mappings' suxs (\ms s_bid ->+ case IntMap.coq_IntMap_lookup s_bid liveSets of {+ Prelude.Just to ->+ let {+ key = case in_from of {+ Prelude.True -> bid;+ Prelude.False -> s_bid}}+ in+ checkBlockBoundary maxReg allocs key+ in_from from to (LiveSets.blockLiveIn to)+ ms;+ Prelude.Nothing -> ms})}}+ in+ Applicative.pure (Monad.is_applicative mDict) ((,) mappings''+ Prelude.False)) (Blocks.blockSuccessors mDict binfo b);+ Prelude.Nothing ->+ Applicative.pure (Monad.is_applicative mDict) ((,) mappings+ Prelude.False)}) (Blocks.blockId mDict binfo b)}))
LinearScan/ScanState.hs view
@@ -10,24 +10,27 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Interval as Interval import qualified LinearScan.List1 as List1 import qualified LinearScan.Prelude0 as Prelude0+import qualified LinearScan.Vector0 as Vector0 import qualified LinearScan.Seq as Seq type PhysReg = Prelude.Int -type FixedIntervalsType = [] (Prelude.Maybe Interval.IntervalDesc)+type FixedIntervalsType = Vector0.Vec (Prelude.Maybe Interval.IntervalDesc) data ScanStateDesc =- Build_ScanStateDesc Prelude.Int ([] Interval.IntervalDesc) FixedIntervalsType - ([] ((,) Prelude.Int Prelude.Int)) ([] ((,) Prelude.Int PhysReg)) ([]- ((,)- Prelude.Int- PhysReg)) + Build_ScanStateDesc Prelude.Int (Vector0.Vec Interval.IntervalDesc) + FixedIntervalsType ([] ((,) Prelude.Int Prelude.Int)) ([]+ ((,) Prelude.Int+ PhysReg)) ([]+ ((,)+ Prelude.Int+ PhysReg)) ([] ((,) Prelude.Int (Prelude.Maybe PhysReg))) nextInterval :: Prelude.Int -> ScanStateDesc -> Prelude.Int@@ -38,7 +41,8 @@ type IntervalId = Prelude.Int -intervals :: Prelude.Int -> ScanStateDesc -> [] Interval.IntervalDesc+intervals :: Prelude.Int -> ScanStateDesc -> Vector0.Vec+ Interval.IntervalDesc intervals maxReg s = case s of { Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0 unhandled0@@ -75,19 +79,19 @@ Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0 unhandled0 active0 inactive0 handled0 -> handled0} -sortRegisterVector :: Prelude.Int -> ([] Prelude.Bool) -> ([]- (Prelude.Maybe Prelude0.Coq_oddnum)) -> []+sortRegisterVector :: Prelude.Int -> (Vector0.Vec Prelude.Bool) ->+ (Vector0.Vec (Prelude.Maybe Prelude0.Coq_oddnum)) -> [] ((,) PhysReg (Prelude.Maybe Prelude0.Coq_oddnum)) sortRegisterVector maxReg fixedAndIntersects =- (LinearScan.Utils.vfoldl'_with_index) maxReg (\reg acc mpos ->+ Vector0.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+ let {xfi = Vector0.vnth maxReg fixedAndIntersects xreg} in+ let {yfi = Vector0.vnth maxReg fixedAndIntersects yreg} in case (Prelude.&&) xfi (Prelude.not yfi) of { Prelude.True -> Prelude.False; Prelude.False ->@@ -100,9 +104,9 @@ in List1.insert f ((,) reg mpos) acc) [] -registerWithHighestPos :: Prelude.Int -> ([] Prelude.Bool) -> ([]- (Prelude.Maybe Prelude0.Coq_oddnum)) -> (,) - PhysReg (Prelude.Maybe Prelude0.Coq_oddnum)+registerWithHighestPos :: Prelude.Int -> (Vector0.Vec Prelude.Bool) ->+ (Vector0.Vec (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)
LinearScan/Seq.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Datatypes as Datatypes import qualified LinearScan.Eqtype as Eqtype
LinearScan/Specif.hs view
@@ -10,7 +10,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils type Coq_sig a =
LinearScan/Spill.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Interval as Interval import qualified LinearScan.List1 as List1@@ -20,6 +20,7 @@ import qualified LinearScan.Prelude0 as Prelude0 import qualified LinearScan.ScanState as ScanState import qualified LinearScan.Trace as Trace+import qualified LinearScan.Vector0 as Vector0 import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Ssrnat as Ssrnat @@ -86,8 +87,9 @@ (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))+ (unsafeCoerce+ (Vector0.vshiftin (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd) ( i1))) (ScanState.fixedIntervals maxReg sd) (List1.insert (Prelude0.lebf Prelude.snd) ((,) ( (ScanState.nextInterval maxReg sd))@@ -143,10 +145,11 @@ sd' = ScanState.Build_ScanStateDesc ((Prelude.succ) (ScanState.nextInterval maxReg sd))- (LinearScan.Utils.snoc- (ScanState.nextInterval maxReg sd)- (ScanState.intervals maxReg sd)- ( i1_1))+ (unsafeCoerce+ (Vector0.vshiftin+ (ScanState.nextInterval maxReg sd)+ (ScanState.intervals maxReg sd)+ ( i1_1))) (ScanState.fixedIntervals maxReg sd) unh' (Prelude.map Prelude.id@@ -165,12 +168,13 @@ ((Prelude.succ) (ScanState.nextInterval maxReg sd'))- (LinearScan.Utils.snoc- (ScanState.nextInterval- maxReg sd')- (ScanState.intervals- maxReg sd') - ( i1_0))+ (unsafeCoerce+ (Vector0.vshiftin+ (ScanState.nextInterval+ maxReg sd')+ (ScanState.intervals+ maxReg sd')+ ( i1_0))) (ScanState.fixedIntervals maxReg sd') (Prelude.map Prelude.id@@ -229,15 +233,16 @@ ((Prelude.succ) (ScanState.nextInterval maxReg sd))- (LinearScan.Utils.set_nth+ (Vector0.vreplace ((Prelude.succ) (ScanState.nextInterval maxReg sd))- (LinearScan.Utils.snoc- (ScanState.nextInterval- maxReg sd)- (ScanState.intervals- maxReg sd) ( i1_1))+ (unsafeCoerce+ (Vector0.vshiftin+ (ScanState.nextInterval+ maxReg sd)+ (ScanState.intervals+ maxReg sd) ( i1_1))) ( uid) ( i1_0)) (ScanState.fixedIntervals maxReg sd) us'@@ -267,16 +272,17 @@ ((Prelude.succ) (ScanState.nextInterval maxReg sd))- (LinearScan.Utils.set_nth+ (Vector0.vreplace ((Prelude.succ) (ScanState.nextInterval maxReg sd))- (LinearScan.Utils.snoc- (ScanState.nextInterval- maxReg sd)- (ScanState.intervals maxReg- sd) ( i1_1)) ( xid)- ( i1_0))+ (unsafeCoerce+ (Vector0.vshiftin+ (ScanState.nextInterval+ maxReg sd)+ (ScanState.intervals+ maxReg sd) ( i1_1)))+ ( xid) ( i1_0)) (ScanState.fixedIntervals maxReg sd) unh' (Prelude.map Prelude.id@@ -321,16 +327,17 @@ ((Prelude.succ) (ScanState.nextInterval maxReg sd))- (LinearScan.Utils.set_nth+ (Vector0.vreplace ((Prelude.succ) (ScanState.nextInterval maxReg sd))- (LinearScan.Utils.snoc- (ScanState.nextInterval- maxReg sd)- (ScanState.intervals maxReg- sd) ( i1_1)) ( xid)- ( i1_0))+ (unsafeCoerce+ (Vector0.vshiftin+ (ScanState.nextInterval+ maxReg sd)+ (ScanState.intervals+ maxReg sd) ( i1_1)))+ ( xid) ( i1_0)) (ScanState.fixedIntervals maxReg sd) unh' (Prelude.map Prelude.id@@ -394,8 +401,9 @@ 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))+ (unsafeCoerce+ (Vector0.vshiftin (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))@@ -463,7 +471,7 @@ (Prelude.flip (Prelude.$)) __ (let { d = - (LinearScan.Utils.nth (ScanState.nextInterval maxReg sd)+ (Vector0.vnth (ScanState.nextInterval maxReg sd) (ScanState.intervals maxReg sd) uid)} in \_ _ ->@@ -475,8 +483,7 @@ (Morph.Build_SSInfo _top_assumption_0 __))} in case spillInterval maxReg sd- (LinearScan.Utils.nth- (ScanState.nextInterval maxReg sd)+ (Vector0.vnth (ScanState.nextInterval maxReg sd) (ScanState.intervals maxReg sd) uid) uid beg us UnhandledToHandled e of { Prelude.Left x -> _evar_0_0 x;
LinearScan/Split.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Context as Context import qualified LinearScan.Datatypes as Datatypes@@ -23,6 +23,7 @@ import qualified LinearScan.ScanState as ScanState import qualified LinearScan.Spill as Spill import qualified LinearScan.Trace as Trace+import qualified LinearScan.Vector0 as Vector0 import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Fintype as Fintype import qualified LinearScan.Seq as Seq@@ -81,7 +82,7 @@ (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 {int = Vector0.vnth _nextInterval_ ints uid0} in let {splitPos = splitPosition ( int) pos} in let { _evar_0_ = \_ ->@@ -119,13 +120,14 @@ (ScanState.Build_ScanStateDesc ((Prelude.succ) _nextInterval_)- (LinearScan.Utils.snoc+ (unsafeCoerce+ (Vector0.vshiftin _nextInterval_- (LinearScan.Utils.set_nth+ (Vector0.vreplace _nextInterval_ ints uid1 ( i0))- ( i1))+ ( i1))) _fixedIntervals_ (List1.insert (Prelude0.lebf@@ -280,7 +282,7 @@ 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 {int = Vector0.vnth ni ints xid0} in let {splitPos = splitPosition ( int) pos} in let { sd0 = ScanState.Build_ScanStateDesc ni ints _fixedIntervals_ unh@@ -304,7 +306,7 @@ (Prelude.flip (Prelude.$)) __ (\_ _ -> let { sd1 = ScanState.Build_ScanStateDesc ni- (LinearScan.Utils.set_nth ni ints xid0 ( i0))+ (Vector0.vreplace ni ints xid0 ( i0)) _fixedIntervals_ unh _active_ _inactive_ _handled_} in@@ -518,7 +520,7 @@ ( (splitPosition (- (LinearScan.Utils.nth+ (Vector0.vnth (ScanState.nextInterval maxReg (ScanState.Build_ScanStateDesc _nextInterval_ intervals0 _fixedIntervals_
+ LinearScan/Ssr.hs view
@@ -0,0 +1,24 @@+++module LinearScan.Ssr 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 Hask.Utils+++__ :: any+__ = Prelude.error "Logical or arity value used"++prop :: Prelude.Bool -> Prelude.Maybe ()+prop b =+ case b of {+ Prelude.True -> Prelude.Just __;+ Prelude.False -> Prelude.Nothing}+
LinearScan/Ssrbool.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils
LinearScan/Ssreflect.hs view
@@ -10,6 +10,6 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils
LinearScan/Ssrfun.hs view
@@ -10,7 +10,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Specif as Specif
LinearScan/Ssrnat.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Ssrbool as Ssrbool
LinearScan/State.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Applicative as Applicative import qualified LinearScan.Functor as Functor
LinearScan/State0.hs view
@@ -11,13 +11,15 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Applicative as Applicative+import qualified LinearScan.Class as Class import qualified LinearScan.Functor as Functor import qualified LinearScan.Monad as Monad import qualified LinearScan.Prelude0 as Prelude0 import qualified LinearScan.State as State+import qualified LinearScan.Tuple as Tuple @@ -58,7 +60,7 @@ 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)+ Functor.fmap h (Tuple.first f) (x st) coq_StateT_ap :: (Monad.Monad a1) -> (StateT a2 a1 (a3 -> a4)) -> (StateT a2 a1 a3) -> StateT a2 a1 a4@@ -68,7 +70,7 @@ case z of { (,) f' st' -> Functor.fmap (Applicative.is_functor (Monad.is_applicative h))- (Prelude0.first f') (x st')}) (f st))+ (Tuple.first f') (x st')}) (f st)) coq_StateT_Applicative :: (Monad.Monad a1) -> Applicative.Applicative (StateT a2 a1 Any)@@ -84,16 +86,16 @@ (Prelude..) ((Prelude..) (Monad.join h) (Functor.fmap (Applicative.is_functor (Monad.is_applicative h))- (Prelude0.curry Prelude0.apply))) x+ (Tuple.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+coq_StateT_MonadTrans :: Class.MonadTrans (StateT a1 Any Any)+coq_StateT_MonadTrans _ h h0 _ x s =+ Functor.fmap (Applicative.is_functor (Monad.is_applicative h)) (\k -> (,) k+ s) x liftStateT :: (Monad.Monad a1) -> (State.State a2 a3) -> StateT a2 a1 a3 liftStateT h x =
LinearScan/String0.hs view
@@ -10,6 +10,6 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils
LinearScan/Trace.hs view
@@ -10,7 +10,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils type IntervalIdT = Prelude.Int
+ LinearScan/Tuple.hs view
@@ -0,0 +1,25 @@+++module LinearScan.Tuple 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 Hask.Utils+++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}+
LinearScan/UsePos.hs view
@@ -11,7 +11,7 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Seq as Seq@@ -41,6 +41,19 @@ Input | Temp | Output++coq_VarKind_leq :: VarKind -> VarKind -> Prelude.Bool+coq_VarKind_leq x y =+ case x of {+ Input -> Prelude.True;+ Temp ->+ case y of {+ Input -> Prelude.False;+ _ -> Prelude.True};+ Output ->+ case y of {+ Output -> Prelude.True;+ _ -> Prelude.False}} eqVarKind :: VarKind -> VarKind -> Prelude.Bool eqVarKind s1 s2 =
− LinearScan/Utils.hs
@@ -1,49 +0,0 @@-module LinearScan.Utils where--import Data.Char-import Data.List as L-import Data.IntMap as M-import Debug.Trace--trace = Debug.Trace.trace . L.map chr--boundedTransport' pos n _top_assumption_ = _top_assumption_--snoc _ xs x = xs ++ [x]--set_nth _ xs n x = take n xs ++ x : drop (n+1) xs--vmap _ = L.map--vfoldl' _ = L.foldl'--vfoldl'_with_index _ f = go 0- where- go _ z [] = z- go n z (x:xs) = go (n+1) (f n z x) xs--nth _ = (!!)--list_rect :: b -> (Int -> a -> [a] -> b -> b) -> Int -> [a] -> b-list_rect z f _ = go z- where- go z [] = z- go z (x:xs) = go (f err x xs z) xs-- err = error "list_rect: attempt to use size"--uncons :: [a] -> Maybe (a, [a])-uncons [] = Nothing-uncons (x:xs) = Just (x, xs)--intMap_mergeWithKey'- :: (Int -> a -> b -> Maybe c)- -> ([(Int, a)] -> [(Int, c)])- -> ([(Int, b)] -> [(Int, c)])- -> ([(Int, a)]) -> ([(Int, b)])- -> [(Int, c)]-intMap_mergeWithKey' combine only1 only2 m1 m2 =- M.toList $ M.mergeWithKey combine- (M.fromList . only1 . M.toList)- (M.fromList . only2 . M.toList)- (M.fromList m1) (M.fromList m2)
LinearScan/Vector0.hs view
@@ -11,10 +11,14 @@ import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity-import qualified LinearScan.Utils+import qualified Hask.Utils +import qualified LinearScan.Datatypes as Datatypes+import qualified LinearScan.Logic as Logic+import qualified LinearScan.Fintype as Fintype + #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base import qualified GHC.Prim as GHC.Prim@@ -40,4 +44,176 @@ -- HUGS type Any = () #endif++__ :: any+__ = Prelude.error "Logical or arity value used"++type Vec a = Any++vnil :: ()+vnil =+ ()++vsing :: a1 -> (,) a1 ()+vsing x =+ (,) x ()++vcons :: Prelude.Int -> a1 -> (Vec a1) -> (,) a1 Any+vcons n x v =+ (,) x v++fin_contra :: Prelude.Int -> a1+fin_contra _top_assumption_ =+ let {_evar_0_ = \m -> Logic.coq_False_rect} in+ case _top_assumption_ of {+ x -> _evar_0_ x}++fin_rect :: Prelude.Int -> (() -> a1) -> (Prelude.Int -> () -> a1 -> a1) ->+ Prelude.Int -> a1+fin_rect n hz hSn _top_assumption_ =+ let {+ _evar_0_ = \m ->+ let {_evar_0_ = \_ -> hz __} in+ let {+ _evar_0_0 = \m0 iHm -> let {_evar_0_0 = iHm __} in hSn m0 __ _evar_0_0}+ in+ Datatypes.nat_rect _evar_0_ (\m0 iHm _ -> _evar_0_0 m0 iHm) m __}+ in+ case _top_assumption_ of {+ x -> _evar_0_ x}++vec_rect :: a2 -> (Prelude.Int -> a1 -> (Vec a1) -> a2 -> a2) -> Prelude.Int+ -> (Vec a1) -> a2+vec_rect hnil hcons n v =+ let {_evar_0_ = \hnil0 hcons0 v0 -> hnil0} in+ let {+ _evar_0_0 = \n0 iHn hnil0 hcons0 v0 ->+ let {+ _evar_0_0 = \_a_ _b_ ->+ let {_evar_0_0 = iHn hnil0 hcons0 _b_} in hcons0 n0 _a_ _b_ _evar_0_0}+ in+ case v0 of {+ (,) x x0 -> _evar_0_0 x x0}}+ in+ Datatypes.nat_rect (unsafeCoerce _evar_0_) (unsafeCoerce _evar_0_0) n hnil+ hcons v++vecn_rect :: (a1 -> a2) -> (Prelude.Int -> a1 -> ((,) a1 Any) -> a2 -> a2) ->+ Prelude.Int -> ((,) a1 Any) -> a2+vecn_rect hsing hcons n v =+ let {+ _evar_0_ = \hsing0 hcons0 v0 ->+ let {_evar_0_ = \a b -> hsing0 a} in+ case v0 of {+ (,) x x0 -> _evar_0_ x x0}}+ in+ let {+ _evar_0_0 = \n0 iHn hsing0 hcons0 v0 ->+ let {+ _evar_0_0 = \_a_ _b_ ->+ let {_evar_0_0 = iHn hsing0 hcons0 _b_} in hcons0 n0 _a_ _b_ _evar_0_0}+ in+ case v0 of {+ (,) x x0 -> _evar_0_0 x x0}}+ in+ Datatypes.nat_rect (unsafeCoerce _evar_0_) (unsafeCoerce _evar_0_0) n hsing+ hcons v++vec_to_seq :: Prelude.Int -> (Vec a1) -> [] a1+vec_to_seq n v =+ let {_evar_0_ = \v0 -> []} in+ let {+ _evar_0_0 = \n0 v0 ->+ let {_evar_0_0 = \x -> (:) x []} in+ let {_evar_0_1 = \sz x _v_ iHxs -> (:) x iHxs} in+ vecn_rect _evar_0_0 _evar_0_1 n0 v0}+ in+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ ->+ _evar_0_ v)+ (\x ->+ unsafeCoerce _evar_0_0 x v)+ n++vfoldl_with_index :: Prelude.Int -> (Prelude.Int -> a2 -> a1 -> a2) -> a2 ->+ (Vec a1) -> a2+vfoldl_with_index n f b v =+ let {_evar_0_ = \_discharged_f_ _discharged_v_ -> b} in+ let {+ _evar_0_0 = \n0 f0 v0 ->+ let {_evar_0_0 = \x b0 -> f0 (Fintype.inord n0 n0) b0 x} in+ let {+ _evar_0_1 = \sz x xs iHxs b0 ->+ iHxs (f0 (Fintype.inord n0 ((Prelude.-) n0 ((Prelude.succ) sz))) b0 x)}+ in+ vecn_rect _evar_0_0 _evar_0_1 n0 v0 b}+ in+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ ->+ _evar_0_ f v)+ (\x ->+ unsafeCoerce _evar_0_0 x f v)+ n++vconst :: Prelude.Int -> a1 -> Vec a1+vconst n i =+ let {_evar_0_ = \n0 iHn -> vcons n0 i iHn} in+ Datatypes.nat_rect (unsafeCoerce vnil) (unsafeCoerce _evar_0_) n++vreplace :: Prelude.Int -> (Vec a1) -> Prelude.Int -> a1 -> Vec a1+vreplace n v p i =+ let {_evar_0_ = \v0 p0 -> fin_contra p0} in+ let {+ _evar_0_0 = \n0 v0 p0 ->+ let {_evar_0_0 = \x p1 -> vsing i} in+ let {+ _evar_0_1 = \_n_ x xs iHxs p1 ->+ let {_evar_0_1 = \_ -> vcons ((Prelude.succ) _n_) i xs} in+ let {+ _evar_0_2 = \p2 _the_2nd_wildcard_ ->+ vcons ((Prelude.succ) _n_) x (iHxs ( p2))}+ in+ fin_rect ((Prelude.succ) _n_) _evar_0_1 (\p2 _ _the_2nd_wildcard_ ->+ _evar_0_2 p2 _the_2nd_wildcard_) p1}+ in+ vecn_rect _evar_0_0 (unsafeCoerce _evar_0_1) n0 v0 p0}+ in+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ ->+ _evar_0_ v p)+ (\x ->+ unsafeCoerce _evar_0_0 x v p)+ n++vnth :: Prelude.Int -> (Vec a1) -> Prelude.Int -> a1+vnth n v p =+ let {_evar_0_ = \v0 p0 -> fin_contra p0} in+ let {+ _evar_0_0 = \n0 v0 p0 ->+ let {_evar_0_0 = \x p1 -> x} in+ let {+ _evar_0_1 = \_n_ x _the_1st_wildcard_ iHxs p1 ->+ let {_evar_0_1 = \_ -> x} in+ let {_evar_0_2 = \p2 _the_2nd_wildcard_ -> iHxs ( p2)} in+ fin_rect ((Prelude.succ) _n_) _evar_0_1 (\p2 _ _the_2nd_wildcard_ ->+ _evar_0_2 p2 _the_2nd_wildcard_) p1}+ in+ vecn_rect _evar_0_0 _evar_0_1 n0 v0 p0}+ in+ (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))+ (\_ ->+ _evar_0_ v p)+ (\x ->+ unsafeCoerce _evar_0_0 x v p)+ n++vmodify :: Prelude.Int -> (Vec a1) -> Prelude.Int -> (a1 -> a1) -> Vec a1+vmodify n v p f =+ vreplace n v p (f (vnth n v p))++vshiftin :: Prelude.Int -> (Vec a1) -> a1 -> (,) a1 Any+vshiftin n v i =+ let {_evar_0_ = vsing i} in+ let {_evar_0_0 = \_n_ x _v_ iHxs -> (,) x iHxs} in+ vec_rect (unsafeCoerce _evar_0_) (unsafeCoerce _evar_0_0) n v
+ LinearScan/Verify.hs view
@@ -0,0 +1,566 @@+{-# OPTIONS_GHC -cpp -XMagicHash #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Verify 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 Hask.Utils++import qualified LinearScan.Applicative as Applicative+import qualified LinearScan.Blocks as Blocks+import qualified LinearScan.Class as Class+import qualified LinearScan.Contravariant as Contravariant+import qualified LinearScan.Functor as Functor+import qualified LinearScan.IntMap as IntMap+import qualified LinearScan.IntSet as IntSet+import qualified LinearScan.Lens as Lens+import qualified LinearScan.List1 as List1+import qualified LinearScan.Loops as Loops+import qualified LinearScan.Monad as Monad+import qualified LinearScan.Prelude0 as Prelude0+import qualified LinearScan.Resolve as Resolve+import qualified LinearScan.Ssr as Ssr+import qualified LinearScan.State0 as State0+import qualified LinearScan.UsePos as UsePos+import qualified LinearScan.Vector0 as Vector0+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Fintype as Fintype+import qualified LinearScan.Seq as Seq+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++type PhysReg = Prelude.Int++data UseVerifier =+ VerifyDisabled+ | VerifyEnabled++type RegAllocations =+ Vector0.Vec ((,) (Prelude.Maybe Blocks.VarId) (Prelude.Maybe Blocks.VarId))++data RegStateDesc =+ Build_RegStateDesc RegAllocations IntSet.IntSet++rsAllocs :: Prelude.Int -> RegStateDesc -> RegAllocations+rsAllocs maxReg r =+ case r of {+ Build_RegStateDesc rsAllocs0 rsStack0 -> rsAllocs0}++rsStack :: Prelude.Int -> RegStateDesc -> IntSet.IntSet+rsStack maxReg r =+ case r of {+ Build_RegStateDesc rsAllocs0 rsStack0 -> rsStack0}++residency :: (Functor.Functor a1) -> ((Prelude.Maybe Blocks.VarId) -> a1) ->+ ((,) (Prelude.Maybe Blocks.VarId) (Prelude.Maybe Blocks.VarId))+ -> a1+residency h x x0 =+ Lens._1 h x x0++reservation :: (Functor.Functor a1) -> ((Prelude.Maybe Blocks.VarId) -> a1)+ -> ((,) (Prelude.Maybe Blocks.VarId)+ (Prelude.Maybe Blocks.VarId)) -> a1+reservation h x x0 =+ Lens._2 h x x0++newRegStateDesc :: Prelude.Int -> RegStateDesc+newRegStateDesc maxReg =+ Build_RegStateDesc+ (Vector0.vconst maxReg ((,) Prelude.Nothing Prelude.Nothing))+ IntSet.emptyIntSet++data AllocError =+ VarNotAllocated Blocks.VarId+ | VarNotResident Blocks.VarId+ | VarNotResidentForReg Blocks.VarId Prelude.Int (Prelude.Maybe Blocks.VarId)+ | VarNotReservedForReg Blocks.VarId Prelude.Int (Prelude.Maybe Blocks.VarId)+ | PhysRegAlreadyResidentForVar Prelude.Int Blocks.VarId+ | PhysRegAlreadyReservedForVar Prelude.Int Blocks.VarId+ | RegAlreadyReservedToVar Prelude.Int Blocks.VarId Blocks.VarId+ | BlockWithoutPredecessors Blocks.BlockId+ | UnknownPredecessorBlock Blocks.BlockId Blocks.BlockId+ | ErrorAtBlockEnd Blocks.BlockId++type RegStateSig = RegStateDesc++packRegState :: Prelude.Int -> RegStateDesc -> RegStateDesc+packRegState maxReg rd =+ rd++data VerifiedSig a =+ Build_VerifiedSig RegStateDesc (IntMap.IntMap RegStateSig) (IntMap.IntMap+ ([]+ Resolve.ResolvingMoveSet)) + (IntMap.IntMap ([] AllocError)) a++verDesc :: Prelude.Int -> (VerifiedSig a1) -> RegStateDesc+verDesc maxReg v =+ case v of {+ Build_VerifiedSig verDesc0 verBlocks0 verMoves0 verErrors0 verExt0 ->+ verDesc0}++verBlocks :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap RegStateSig+verBlocks maxReg v =+ case v of {+ Build_VerifiedSig verDesc0 verBlocks0 verMoves0 verErrors0 verExt0 ->+ verBlocks0}++verMoves :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap+ ([] Resolve.ResolvingMoveSet)+verMoves maxReg v =+ case v of {+ Build_VerifiedSig verDesc0 verBlocks0 verMoves0 verErrors0 verExt0 ->+ verMoves0}++verErrors :: Prelude.Int -> (VerifiedSig a1) -> IntMap.IntMap ([] AllocError)+verErrors maxReg v =+ case v of {+ Build_VerifiedSig verDesc0 verBlocks0 verMoves0 verErrors0 verExt0 ->+ verErrors0}++verExt :: Prelude.Int -> (VerifiedSig a1) -> a1+verExt maxReg v =+ case v of {+ Build_VerifiedSig verDesc0 verBlocks0 verMoves0 verErrors0 verExt0 ->+ verExt0}++newVerifiedSig :: Prelude.Int -> a1 -> VerifiedSig a1+newVerifiedSig maxReg i =+ Build_VerifiedSig (newRegStateDesc maxReg) IntMap.emptyIntMap+ IntMap.emptyIntMap IntMap.emptyIntMap i++_verDesc :: Prelude.Int -> (Functor.Functor a2) ->+ (Contravariant.Contravariant a2) -> (RegStateDesc -> a2) ->+ (VerifiedSig a1) -> a2+_verDesc maxReg h h0 f s =+ Functor.fmap h (Prelude0.const s) (f (verDesc maxReg s))++_verState :: Prelude.Int -> (Functor.Functor a2) -> (RegStateDesc -> a2) ->+ (VerifiedSig a1) -> a2+_verState maxReg h f s =+ Functor.fmap h (\x -> Build_VerifiedSig ( x) (verBlocks maxReg s)+ (verMoves maxReg s) (verErrors maxReg s) (verExt maxReg s))+ (f (verDesc maxReg s))++_verBlocks :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap+ RegStateSig) -> a2) -> (VerifiedSig a1) -> a2+_verBlocks maxReg h f s =+ Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s) x+ (verMoves maxReg s) (verErrors maxReg s) (verExt maxReg s))+ (f (verBlocks maxReg s))++_verMoves :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap+ ([] Resolve.ResolvingMoveSet)) -> a2) -> (VerifiedSig a1) -> a2+_verMoves maxReg h f s =+ Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s)+ (verBlocks maxReg s) x (verErrors maxReg s) (verExt maxReg s))+ (f (verMoves maxReg s))++_verErrors :: Prelude.Int -> (Functor.Functor a2) -> ((IntMap.IntMap+ ([] AllocError)) -> a2) -> (VerifiedSig a1) -> a2+_verErrors maxReg h f s =+ Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s)+ (verBlocks maxReg s) (verMoves maxReg s) x (verExt maxReg s))+ (f (verErrors maxReg s))++_verExt :: Prelude.Int -> (Functor.Functor a2) -> (a1 -> a2) -> (VerifiedSig+ a1) -> a2+_verExt maxReg h f s =+ Functor.fmap h (\x -> Build_VerifiedSig (verDesc maxReg s)+ (verBlocks maxReg s) (verMoves maxReg s) (verErrors maxReg s) x)+ (f (verExt maxReg s))++type Verified mType a a0 = State0.StateT (VerifiedSig a) mType a0++errorsT :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> ([] AllocError)+ -> Verified a1 a2 ()+errorsT maxReg mDict pc errs =+ Lens.applyStateT (\_ -> _verErrors maxReg)+ (IntMap.coq_IntMap_insert pc errs) mDict++errorT :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> AllocError ->+ Verified a1 a2 ()+errorT maxReg mDict pc err =+ errorsT maxReg mDict pc ((:) err [])++addMove :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->+ Resolve.ResolvingMoveSet -> Verified a1 a2 ()+addMove maxReg mDict pc mv =+ Lens.applyStateT (\_ -> _verMoves maxReg)+ (IntMap.coq_IntMap_alter (\mxs -> Prelude.Just+ (case mxs of {+ Prelude.Just xs -> Seq.rcons xs mv;+ Prelude.Nothing -> (:) mv []})) pc) mDict++reserveReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg ->+ Blocks.VarId -> Verified a1 a2 ()+reserveReg maxReg mDict pc reg var =+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ case Ssr.prop+ (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)+ (Lens.view+ (Lens.stepdownl' (unsafeCoerce (\_ -> reservation)))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg))+ (unsafeCoerce Prelude.Nothing)) of {+ Prelude.Just _ ->+ Lens.modifyStateT (\_ -> _verState maxReg)+ (packRegState maxReg (Build_RegStateDesc+ (Vector0.vmodify maxReg (rsAllocs maxReg st) reg+ (Lens.set (\_ -> reservation) (Prelude.Just var)))+ (rsStack maxReg st))) mDict;+ Prelude.Nothing ->+ case Lens.view (Lens.stepdownl' (\_ -> reservation))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {+ Prelude.Just v ->+ Monad.when (State0.coq_StateT_Monad mDict)+ (Prelude.not+ (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce v)+ (unsafeCoerce var)))+ (errorT maxReg mDict pc (RegAlreadyReservedToVar ( reg) v var));+ Prelude.Nothing ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))+ (addMove maxReg mDict pc (Resolve.RSAllocReg var ( reg)))++isReserved :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Blocks.VarId ->+ Verified a1 a2 Prelude.Bool+isReserved maxReg mDict reg var =+ Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ Applicative.pure (State0.coq_StateT_Applicative mDict)+ (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)+ (Lens.view (Lens.stepdownl' (unsafeCoerce (\_ -> reservation)))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg))+ (unsafeCoerce (Prelude.Just var))))+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)++checkReservation :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg+ -> Blocks.VarId -> Verified a1 a2 ()+checkReservation maxReg mDict pc reg var =+ Monad.bind (State0.coq_StateT_Monad mDict) (\b ->+ Monad.unless (State0.coq_StateT_Monad mDict) b+ (Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ errorT maxReg mDict pc (VarNotReservedForReg var ( reg)+ (Lens.view (Lens.stepdownl' (\_ -> reservation))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg))))+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)))+ (isReserved maxReg mDict reg var)++releaseReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg ->+ Blocks.VarId -> Verified a1 a2 ()+releaseReg maxReg mDict pc reg var =+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ case Ssr.prop+ (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)+ (Lens.view+ (Lens.stepdownl' (unsafeCoerce (\_ -> reservation)))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg))+ (unsafeCoerce (Prelude.Just var))) of {+ Prelude.Just _ ->+ Lens.modifyStateT (\_ -> _verState maxReg)+ (packRegState maxReg (Build_RegStateDesc+ (Vector0.vmodify maxReg (rsAllocs maxReg st) reg+ (Lens.set (\_ -> reservation) Prelude.Nothing))+ (rsStack maxReg st))) mDict;+ Prelude.Nothing ->+ errorT maxReg mDict pc (VarNotReservedForReg var ( reg)+ (Lens.view (Lens.stepdownl' (\_ -> reservation))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg)))})+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))+ (addMove maxReg mDict pc (Resolve.RSFreeReg ( reg) var))++assignReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg ->+ Blocks.VarId -> Verified a1 a2 ()+assignReg maxReg mDict pc reg var =+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ case Ssr.prop+ (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)+ (Lens.view+ (Lens.stepdownl' (unsafeCoerce (\_ -> reservation)))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg))+ (unsafeCoerce (Prelude.Just var))) of {+ Prelude.Just _ ->+ Lens.modifyStateT (\_ -> _verState maxReg)+ (packRegState maxReg (Build_RegStateDesc+ (Vector0.vmodify maxReg (rsAllocs maxReg st) reg+ (Lens.set (\_ -> residency) (Prelude.Just var)))+ (rsStack maxReg st))) mDict;+ Prelude.Nothing ->+ errorT maxReg mDict pc (VarNotReservedForReg ( reg) var+ (Lens.view (Lens.stepdownl' (\_ -> reservation))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg)))})+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))+ (addMove maxReg mDict pc (Resolve.RSAssignReg var ( reg)))++isResident :: Prelude.Int -> (Monad.Monad a1) -> PhysReg -> Blocks.VarId ->+ Verified a1 a2 Prelude.Bool+isResident maxReg mDict reg var =+ Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ Applicative.pure (State0.coq_StateT_Applicative mDict)+ (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)+ (Lens.view (Lens.stepdownl' (unsafeCoerce (\_ -> residency)))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg))+ (unsafeCoerce (Prelude.Just var))))+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)++checkResidency :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg+ -> Blocks.VarId -> Verified a1 a2 ()+checkResidency maxReg mDict pc reg var =+ Monad.bind (State0.coq_StateT_Monad mDict) (\b ->+ Monad.unless (State0.coq_StateT_Monad mDict) b+ (Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ errorT maxReg mDict pc (VarNotResidentForReg var ( reg)+ (Lens.view (Lens.stepdownl' (\_ -> residency))+ (Vector0.vnth maxReg (rsAllocs maxReg st) reg))))+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)))+ (isResident maxReg mDict reg var)++checkLiveness :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->+ IntSet.IntSet -> Verified a1 a2 ()+checkLiveness maxReg mDict pc vars =+ Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ Monad.forM_ (State0.coq_StateT_Monad mDict)+ (IntSet.coq_IntSet_toList vars) (\var ->+ Monad.unless (State0.coq_StateT_Monad mDict)+ (Vector0.vfoldl_with_index maxReg (\reg b p ->+ (Prelude.||) b+ (case Lens.view (Lens.stepdownl' (\_ -> residency)) p of {+ Prelude.Just var0 -> Prelude.True;+ Prelude.Nothing -> Prelude.False})) Prelude.False+ (rsAllocs maxReg st)) (errorT maxReg mDict pc (VarNotResident var))))+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)++verifyBlockBegin :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->+ UseVerifier -> Prelude.Int -> IntSet.IntSet ->+ Loops.LoopState -> Verified a1 a2 ()+verifyBlockBegin maxReg mDict pc useVerifier bid liveIns loops =+ case useVerifier of {+ VerifyDisabled ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ();+ VerifyEnabled ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ checkLiveness maxReg mDict pc liveIns)+ (case IntMap.coq_IntMap_lookup bid (Loops.forwardBranches loops) of {+ Prelude.Just fwds ->+ Monad.forM_ (State0.coq_StateT_Monad mDict)+ (IntSet.coq_IntSet_toList fwds) (\pred ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\exits ->+ case IntMap.coq_IntMap_lookup pred exits of {+ Prelude.Just allocs ->+ Lens.modifyStateT (\_ -> _verState maxReg) allocs mDict;+ Prelude.Nothing ->+ errorT maxReg mDict pc (UnknownPredecessorBlock bid pred)})+ (Lens.use (Lens.stepdownl' (\_ -> _verBlocks maxReg)) mDict));+ Prelude.Nothing ->+ Monad.when (State0.coq_StateT_Monad mDict)+ ((Prelude.<=) ((Prelude.succ) 0) (IntSet.coq_IntSet_size liveIns))+ (errorT maxReg mDict pc (BlockWithoutPredecessors bid))})}++verifyBlockEnd :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->+ UseVerifier -> Prelude.Int -> IntSet.IntSet -> Verified + a1 a2 ()+verifyBlockEnd maxReg mDict pc useVerifier bid liveOuts =+ case useVerifier of {+ VerifyDisabled ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ();+ VerifyEnabled ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\allocs ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ Lens.applyStateT (\_ -> _verBlocks maxReg)+ (IntMap.coq_IntMap_insert bid allocs) mDict)+ (Lens.modifyStateT (\_ -> _verState maxReg)+ (packRegState maxReg (newRegStateDesc maxReg)) mDict))+ (Lens.use (Lens.stepdownl' (\_ -> _verState maxReg)) mDict))+ (checkLiveness maxReg mDict pc liveOuts)}++verifyApplyAllocs :: Prelude.Int -> (Monad.Monad a3) -> (Blocks.OpInfo + a3 a1 a2) -> Blocks.OpId -> UseVerifier -> a1 -> ([]+ ((,) Blocks.VarId PhysReg)) -> Verified a3 a4 ([] a2)+verifyApplyAllocs maxReg mDict oinfo pc useVerifier op allocs =+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Class.lift (unsafeCoerce State0.coq_StateT_MonadTrans) mDict+ (State0.coq_StateT_Monad mDict)+ (Blocks.applyAllocs maxReg mDict oinfo op allocs))+ (case useVerifier of {+ VerifyDisabled ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ();+ VerifyEnabled ->+ Monad.forM_ (State0.coq_StateT_Monad mDict)+ (List1.sortBy (\x y ->+ UsePos.coq_VarKind_leq (Blocks.varKind maxReg x)+ (Blocks.varKind maxReg y))+ (Blocks.opRefs maxReg mDict oinfo op)) (\ref ->+ case Blocks.varId maxReg ref of {+ Prelude.Left reg ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ case Blocks.varKind maxReg ref of {+ UsePos.Input ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ();+ UsePos.Temp ->+ case Vector0.vnth maxReg (rsAllocs maxReg st) reg of {+ (,) o o0 ->+ case o0 of {+ Prelude.Just v ->+ errorT maxReg mDict pc (PhysRegAlreadyReservedForVar+ ( reg) v);+ Prelude.Nothing ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ()}};+ UsePos.Output ->+ case Vector0.vnth maxReg (rsAllocs maxReg st) reg of {+ (,) o o0 ->+ case o0 of {+ Prelude.Just v ->+ errorT maxReg mDict pc (PhysRegAlreadyReservedForVar+ ( reg) v);+ Prelude.Nothing ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}})+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict);+ Prelude.Right var ->+ case List1.maybeLookup Ssrnat.nat_eqType (unsafeCoerce allocs)+ (unsafeCoerce var) of {+ Prelude.Just reg ->+ case Blocks.varKind maxReg ref of {+ UsePos.Input -> checkResidency maxReg mDict pc reg var;+ UsePos.Temp -> checkReservation maxReg mDict pc reg var;+ UsePos.Output ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ assignReg maxReg mDict pc reg var)+ (checkReservation maxReg mDict pc reg var)};+ Prelude.Nothing -> errorT maxReg mDict pc (VarNotAllocated var)}})})++verifyResolutions :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->+ UseVerifier -> ([] Resolve.ResGraphEdge) -> Verified + a1 a2 ([] Resolve.ResolvingMove)+verifyResolutions maxReg mDict pc useVerifier moves =+ case useVerifier of {+ VerifyDisabled ->+ Applicative.pure (State0.coq_StateT_Applicative mDict)+ (Prelude.map (Resolve.resMove maxReg) moves);+ VerifyEnabled ->+ Functor.fmap+ (State0.coq_StateT_Functor+ (Applicative.is_functor (Monad.is_applicative mDict))) Seq.rev+ (Monad.forFoldM (State0.coq_StateT_Monad mDict) [] moves (\acc mv ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\st ->+ case Resolve.resMove maxReg mv of {+ Resolve.Move fromReg fromVar toReg ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x3 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x4 ->+ Applicative.pure+ (State0.coq_StateT_Applicative mDict) ((:)+ (Resolve.resMove maxReg mv) acc))+ (Monad.when (State0.coq_StateT_Monad mDict)+ (Resolve.resGhost maxReg mv)+ (releaseReg maxReg mDict pc toReg fromVar)))+ (assignReg maxReg mDict pc toReg fromVar))+ (addMove maxReg mDict pc+ (Resolve.weakenResolvingMove maxReg+ (Resolve.resMove maxReg mv))))+ (reserveReg maxReg mDict pc toReg fromVar))+ (Monad.unless (State0.coq_StateT_Monad mDict)+ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg)+ (unsafeCoerce fromReg) (unsafeCoerce toReg))+ (releaseReg maxReg mDict pc fromReg fromVar)))+ (checkResidency maxReg mDict pc fromReg fromVar);+ Resolve.Swap fromReg fromVar toReg toVar ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x3 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x4 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x5 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x6 ->+ Monad.bind (State0.coq_StateT_Monad mDict)+ (\x7 ->+ Applicative.pure+ (State0.coq_StateT_Applicative mDict) ((:)+ (Resolve.resMove maxReg mv) acc))+ (assignReg maxReg mDict pc toReg fromVar))+ (assignReg maxReg mDict pc fromReg toVar))+ (reserveReg maxReg mDict pc toReg fromVar))+ (reserveReg maxReg mDict pc fromReg toVar))+ (addMove maxReg mDict pc+ (Resolve.weakenResolvingMove maxReg+ (Resolve.resMove maxReg mv))))+ (releaseReg maxReg mDict pc toReg toVar))+ (releaseReg maxReg mDict pc fromReg fromVar))+ (checkResidency maxReg mDict pc toReg toVar))+ (checkResidency maxReg mDict pc fromReg fromVar);+ Resolve.Spill fromReg toSpillSlot ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\check ->+ case check of {+ Prelude.True ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ Applicative.pure (State0.coq_StateT_Applicative mDict)+ ((:) (Resolve.resMove maxReg mv) acc))+ (addMove maxReg mDict pc+ (Resolve.weakenResolvingMove maxReg+ (Resolve.resMove maxReg mv)));+ Prelude.False ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) acc})+ (isResident maxReg mDict fromReg toSpillSlot))+ (releaseReg maxReg mDict pc fromReg toSpillSlot);+ Resolve.Restore fromSpillSlot toReg ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->+ Applicative.pure (State0.coq_StateT_Applicative mDict)+ ((:) (Resolve.resMove maxReg mv) acc))+ (Monad.when (State0.coq_StateT_Monad mDict)+ (Resolve.resGhost maxReg mv)+ (releaseReg maxReg mDict pc toReg fromSpillSlot)))+ (assignReg maxReg mDict pc toReg fromSpillSlot))+ (addMove maxReg mDict pc+ (Resolve.weakenResolvingMove maxReg+ (Resolve.resMove maxReg mv))))+ (reserveReg maxReg mDict pc toReg fromSpillSlot);+ Resolve.AllocReg toVar toReg ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) acc)+ (Monad.when (State0.coq_StateT_Monad mDict)+ (Resolve.resGhost maxReg mv)+ (releaseReg maxReg mDict pc toReg toVar)))+ (reserveReg maxReg mDict pc toReg toVar);+ Resolve.FreeReg fromReg fromVar ->+ Monad.bind (State0.coq_StateT_Monad mDict) (\x ->+ Applicative.pure (State0.coq_StateT_Applicative mDict) acc)+ (releaseReg maxReg mDict pc fromReg fromVar)})+ (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)))}+
− LinearScan/Yoneda.hs
@@ -1,80 +0,0 @@-{-# OPTIONS_GHC -cpp -XMagicHash #-}-{- For Hugs, use the option -F"cpp -P -traditional" -}--module LinearScan.Yoneda where---import Debug.Trace (trace, traceShow)-import qualified Prelude-import qualified Data.IntMap-import qualified Data.IntSet-import qualified Data.List-import qualified Data.Ord-import qualified Data.Functor.Identity-import qualified LinearScan.Utils--import qualified LinearScan.Applicative as Applicative-import qualified LinearScan.Functor as Functor-import qualified LinearScan.Iso as Iso-import qualified LinearScan.Monad as Monad----#ifdef __GLASGOW_HASKELL__-import qualified GHC.Base as GHC.Base-import qualified GHC.Prim as GHC.Prim-#else--- HUGS-import qualified LinearScan.IOExts as IOExts-#endif---#ifdef __GLASGOW_HASKELL__---unsafeCoerce :: a -> b-unsafeCoerce = GHC.Base.unsafeCoerce#-#else--- HUGS---unsafeCoerce :: a -> b-unsafeCoerce = IOExts.unsafeCoerce-#endif---#ifdef __GLASGOW_HASKELL__-type Any = GHC.Prim.Any-#else--- HUGS-type Any = ()-#endif--__ :: any-__ = Prelude.error "Logical or arity value used"--type Yoneda f a = () -> (a -> Any) -> f--coq_Yoneda_lemma :: (Functor.Functor a1) -> Iso.Isomorphism (Yoneda a1 a2) a1-coq_Yoneda_lemma h =- Iso.Build_Isomorphism (\x -> unsafeCoerce x __ (\x0 -> x0)) (\x _ k ->- Functor.fmap h k x)--coq_Yoneda_Functor :: Functor.Functor (Yoneda a1 Any)-coq_Yoneda_Functor _ _ g k _ h =- k __ ((Prelude..) h g)--coq_Yoneda_Applicative :: (Applicative.Applicative a1) ->- Applicative.Applicative (Yoneda a1 Any)-coq_Yoneda_Applicative h =- 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-coq_Yoneda_join h k h0 =- Monad.join h (unsafeCoerce k __ (\y -> y __ h0))--coq_Yoneda_Monad :: (Monad.Monad a1) -> Monad.Monad (Yoneda a1 Any)-coq_Yoneda_Monad h =- Monad.Build_Monad (coq_Yoneda_Applicative (Monad.is_applicative h))- (unsafeCoerce (\_ x _ -> coq_Yoneda_join h x))-
linearscan.cabal view
@@ -1,5 +1,5 @@ name: linearscan-version: 0.6.0.0+version: 0.7.0 synopsis: Linear scan register allocator, formally verified in Coq homepage: http://github.com/jwiegley/linearscan license: BSD3@@ -55,17 +55,21 @@ LinearScan.Blocks LinearScan.Build LinearScan.Choice+ LinearScan.Class LinearScan.Context+ LinearScan.Const LinearScan.Cursor LinearScan.Datatypes+ -- LinearScan.Either+ -- LinearScan.Either0 LinearScan.Eqtype LinearScan.Fintype LinearScan.Functor LinearScan.Graph+ LinearScan.Identity LinearScan.IntMap LinearScan.IntSet LinearScan.Interval- LinearScan.Iso LinearScan.Lens LinearScan.Lib LinearScan.List0@@ -86,6 +90,7 @@ LinearScan.Specif LinearScan.Spill LinearScan.Split+ LinearScan.Ssr LinearScan.Ssrbool LinearScan.Ssreflect LinearScan.Ssrfun@@ -94,14 +99,16 @@ LinearScan.State0 LinearScan.String0 LinearScan.Trace+ LinearScan.Tuple LinearScan.UsePos- LinearScan.Utils LinearScan.Vector0- LinearScan.Yoneda- cpp-options: -DMAX_REG=4 -DREG_SIZE=8- ghc-options: -fno-warn-deprecated-flags- build-depends: base >=4.7 && <5.0- , containers- , transformers- , mtl- , ghc-prim+ LinearScan.Verify+ Hask.Utils+ cpp-options: -DMAX_REG=4 -DREG_SIZE=8+ ghc-options: -fno-warn-deprecated-flags+ hs-source-dirs: . Hask/haskell+ build-depends: base >=4.7 && <5.0+ , containers+ , transformers+ , mtl+ , ghc-prim