diff --git a/Hask/haskell/Hask/Utils.hs b/Hask/haskell/Hask/Utils.hs new file mode 100644 --- /dev/null +++ b/Hask/haskell/Hask/Utils.hs @@ -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" diff --git a/LinearScan.hs b/LinearScan.hs --- a/LinearScan.hs +++ b/LinearScan.hs @@ -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) = "" + -- show (LS.RSFreeStack 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 -> diff --git a/LinearScan/Allocate.hs b/LinearScan/Allocate.hs --- a/LinearScan/Allocate.hs +++ b/LinearScan/Allocate.hs @@ -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) diff --git a/LinearScan/Applicative.hs b/LinearScan/Applicative.hs --- a/LinearScan/Applicative.hs +++ b/LinearScan/Applicative.hs @@ -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} diff --git a/LinearScan/Ascii.hs b/LinearScan/Ascii.hs --- a/LinearScan/Ascii.hs +++ b/LinearScan/Ascii.hs @@ -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 = diff --git a/LinearScan/Assign.hs b/LinearScan/Assign.hs --- a/LinearScan/Assign.hs +++ b/LinearScan/Assign.hs @@ -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)) diff --git a/LinearScan/Blocks.hs b/LinearScan/Blocks.hs --- a/LinearScan/Blocks.hs +++ b/LinearScan/Blocks.hs @@ -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) diff --git a/LinearScan/Build.hs b/LinearScan/Build.hs --- a/LinearScan/Build.hs +++ b/LinearScan/Build.hs @@ -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 diff --git a/LinearScan/Choice.hs b/LinearScan/Choice.hs --- a/LinearScan/Choice.hs +++ b/LinearScan/Choice.hs @@ -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 diff --git a/LinearScan/Class.hs b/LinearScan/Class.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Class.hs @@ -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 + diff --git a/LinearScan/Const.hs b/LinearScan/Const.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Const.hs @@ -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 + diff --git a/LinearScan/Context.hs b/LinearScan/Context.hs --- a/LinearScan/Context.hs +++ b/LinearScan/Context.hs @@ -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 = diff --git a/LinearScan/Cursor.hs b/LinearScan/Cursor.hs --- a/LinearScan/Cursor.hs +++ b/LinearScan/Cursor.hs @@ -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 diff --git a/LinearScan/Datatypes.hs b/LinearScan/Datatypes.hs --- a/LinearScan/Datatypes.hs +++ b/LinearScan/Datatypes.hs @@ -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 = diff --git a/LinearScan/Eqtype.hs b/LinearScan/Eqtype.hs --- a/LinearScan/Eqtype.hs +++ b/LinearScan/Eqtype.hs @@ -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 = diff --git a/LinearScan/Fintype.hs b/LinearScan/Fintype.hs --- a/LinearScan/Fintype.hs +++ b/LinearScan/Fintype.hs @@ -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) diff --git a/LinearScan/Functor.hs b/LinearScan/Functor.hs --- a/LinearScan/Functor.hs +++ b/LinearScan/Functor.hs @@ -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 diff --git a/LinearScan/Graph.hs b/LinearScan/Graph.hs --- a/LinearScan/Graph.hs +++ b/LinearScan/Graph.hs @@ -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 diff --git a/LinearScan/Identity.hs b/LinearScan/Identity.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Identity.hs @@ -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 + diff --git a/LinearScan/IntMap.hs b/LinearScan/IntMap.hs --- a/LinearScan/IntMap.hs +++ b/LinearScan/IntMap.hs @@ -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 = diff --git a/LinearScan/IntSet.hs b/LinearScan/IntSet.hs --- a/LinearScan/IntSet.hs +++ b/LinearScan/IntSet.hs @@ -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 diff --git a/LinearScan/Interval.hs b/LinearScan/Interval.hs --- a/LinearScan/Interval.hs +++ b/LinearScan/Interval.hs @@ -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) diff --git a/LinearScan/Iso.hs b/LinearScan/Iso.hs deleted file mode 100644 --- a/LinearScan/Iso.hs +++ /dev/null @@ -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} - diff --git a/LinearScan/Lens.hs b/LinearScan/Lens.hs --- a/LinearScan/Lens.hs +++ b/LinearScan/Lens.hs @@ -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) diff --git a/LinearScan/Lib.hs b/LinearScan/Lib.hs --- a/LinearScan/Lib.hs +++ b/LinearScan/Lib.hs @@ -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 diff --git a/LinearScan/List0.hs b/LinearScan/List0.hs --- a/LinearScan/List0.hs +++ b/LinearScan/List0.hs @@ -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 diff --git a/LinearScan/List1.hs b/LinearScan/List1.hs --- a/LinearScan/List1.hs +++ b/LinearScan/List1.hs @@ -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 = diff --git a/LinearScan/LiveSets.hs b/LinearScan/LiveSets.hs --- a/LinearScan/LiveSets.hs +++ b/LinearScan/LiveSets.hs @@ -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) -> diff --git a/LinearScan/Logic.hs b/LinearScan/Logic.hs --- a/LinearScan/Logic.hs +++ b/LinearScan/Logic.hs @@ -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 diff --git a/LinearScan/Loops.hs b/LinearScan/Loops.hs --- a/LinearScan/Loops.hs +++ b/LinearScan/Loops.hs @@ -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)} diff --git a/LinearScan/Main.hs b/LinearScan/Main.hs --- a/LinearScan/Main.hs +++ b/LinearScan/Main.hs @@ -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 diff --git a/LinearScan/Monad.hs b/LinearScan/Monad.hs --- a/LinearScan/Monad.hs +++ b/LinearScan/Monad.hs @@ -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 = diff --git a/LinearScan/Morph.hs b/LinearScan/Morph.hs --- a/LinearScan/Morph.hs +++ b/LinearScan/Morph.hs @@ -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 __}}}}} diff --git a/LinearScan/Nat.hs b/LinearScan/Nat.hs --- a/LinearScan/Nat.hs +++ b/LinearScan/Nat.hs @@ -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 diff --git a/LinearScan/NonEmpty.hs b/LinearScan/NonEmpty.hs --- a/LinearScan/NonEmpty.hs +++ b/LinearScan/NonEmpty.hs @@ -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) -> ([] diff --git a/LinearScan/Prelude0.hs b/LinearScan/Prelude0.hs --- a/LinearScan/Prelude0.hs +++ b/LinearScan/Prelude0.hs @@ -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 = diff --git a/LinearScan/Range.hs b/LinearScan/Range.hs --- a/LinearScan/Range.hs +++ b/LinearScan/Range.hs @@ -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; diff --git a/LinearScan/Resolve.hs b/LinearScan/Resolve.hs --- a/LinearScan/Resolve.hs +++ b/LinearScan/Resolve.hs @@ -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)})) diff --git a/LinearScan/ScanState.hs b/LinearScan/ScanState.hs --- a/LinearScan/ScanState.hs +++ b/LinearScan/ScanState.hs @@ -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) diff --git a/LinearScan/Seq.hs b/LinearScan/Seq.hs --- a/LinearScan/Seq.hs +++ b/LinearScan/Seq.hs @@ -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 diff --git a/LinearScan/Specif.hs b/LinearScan/Specif.hs --- a/LinearScan/Specif.hs +++ b/LinearScan/Specif.hs @@ -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 = diff --git a/LinearScan/Spill.hs b/LinearScan/Spill.hs --- a/LinearScan/Spill.hs +++ b/LinearScan/Spill.hs @@ -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; diff --git a/LinearScan/Split.hs b/LinearScan/Split.hs --- a/LinearScan/Split.hs +++ b/LinearScan/Split.hs @@ -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_ diff --git a/LinearScan/Ssr.hs b/LinearScan/Ssr.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Ssr.hs @@ -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} + diff --git a/LinearScan/Ssrbool.hs b/LinearScan/Ssrbool.hs --- a/LinearScan/Ssrbool.hs +++ b/LinearScan/Ssrbool.hs @@ -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 diff --git a/LinearScan/Ssreflect.hs b/LinearScan/Ssreflect.hs --- a/LinearScan/Ssreflect.hs +++ b/LinearScan/Ssreflect.hs @@ -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 diff --git a/LinearScan/Ssrfun.hs b/LinearScan/Ssrfun.hs --- a/LinearScan/Ssrfun.hs +++ b/LinearScan/Ssrfun.hs @@ -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 diff --git a/LinearScan/Ssrnat.hs b/LinearScan/Ssrnat.hs --- a/LinearScan/Ssrnat.hs +++ b/LinearScan/Ssrnat.hs @@ -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 diff --git a/LinearScan/State.hs b/LinearScan/State.hs --- a/LinearScan/State.hs +++ b/LinearScan/State.hs @@ -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 diff --git a/LinearScan/State0.hs b/LinearScan/State0.hs --- a/LinearScan/State0.hs +++ b/LinearScan/State0.hs @@ -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 = diff --git a/LinearScan/String0.hs b/LinearScan/String0.hs --- a/LinearScan/String0.hs +++ b/LinearScan/String0.hs @@ -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 diff --git a/LinearScan/Trace.hs b/LinearScan/Trace.hs --- a/LinearScan/Trace.hs +++ b/LinearScan/Trace.hs @@ -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 diff --git a/LinearScan/Tuple.hs b/LinearScan/Tuple.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Tuple.hs @@ -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} + diff --git a/LinearScan/UsePos.hs b/LinearScan/UsePos.hs --- a/LinearScan/UsePos.hs +++ b/LinearScan/UsePos.hs @@ -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 = diff --git a/LinearScan/Utils.hs b/LinearScan/Utils.hs deleted file mode 100644 --- a/LinearScan/Utils.hs +++ /dev/null @@ -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) diff --git a/LinearScan/Vector0.hs b/LinearScan/Vector0.hs --- a/LinearScan/Vector0.hs +++ b/LinearScan/Vector0.hs @@ -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 diff --git a/LinearScan/Verify.hs b/LinearScan/Verify.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Verify.hs @@ -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)))} + diff --git a/LinearScan/Yoneda.hs b/LinearScan/Yoneda.hs deleted file mode 100644 --- a/LinearScan/Yoneda.hs +++ /dev/null @@ -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)) - diff --git a/linearscan.cabal b/linearscan.cabal --- a/linearscan.cabal +++ b/linearscan.cabal @@ -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